changes

4 files changed, 27 insertions, 12 deletions

diff --git a/src/theory/strings/skolem_cache.cpp b/src/theory/strings/skolem_cache.cpp
index fc5a9fb03..0a7e06bdd 100644
--- a/src/theory/strings/skolem_cache.cpp
+++ b/src/theory/strings/skolem_cache.cpp
@@ -15,6 +15,7 @@
 #include "theory/strings/skolem_cache.h"
 
 #include "theory/rewriter.h"
+#include "theory/strings/theory_strings.h"
 #include "theory/strings/theory_strings_rewriter.h"
 #include "util/rational.h"
 
@@ -24,9 +25,10 @@ namespace CVC4 {
 namespace theory {
 namespace strings {
 
-SkolemCache::SkolemCache()
+SkolemCache::SkolemCache(TheoryStrings* ts)
 {
   NodeManager* nm = NodeManager::currentNM();
+  d_ts = ts;
   d_strType = nm->stringType();
   d_zero = nm->mkConst(Rational(0));
 }
@@ -57,6 +59,19 @@ Node SkolemCache::mkTypedSkolemCached(
   {
     Node sk = mkTypedSkolem(tn, c);
     d_skolemCache[a][b][id] = sk;
+
+    if (id == SK_FIRST_CTN_POST && a.getKind() == STRING_SUBSTR) {
+      NodeManager* nm = NodeManager::currentNM();
+      Node aLen = nm->mkNode(STRING_LENGTH, a[0]);
+      Node sum = nm->mkNode(PLUS, a[1], a[2]);
+
+      if (TheoryStringsRewriter::checkEntailArith(sum, aLen))  {
+        Node skLen = nm->mkNode(STRING_LENGTH, sk);
+        Node sk2Len = nm->mkNode(STRING_LENGTH, mkSkolemCached(a[0], b, SK_FIRST_CTN_POST, "foo"));
+        d_ts->sendLemma(nm->mkConst(true), nm->mkNode(GEQ, sk2Len, skLen), "foo");
+      }
+    }
+
     return sk;
   }
   return it->second;
@@ -94,18 +109,9 @@ SkolemCache::normalizeStringSkolem(SkolemId id, Node a, Node b)
 
   NodeManager* nm = NodeManager::currentNM();
 
+  /*
   if (id == SK_FIRST_CTN_POST)
   {
-    // SK_FIRST_CTN_PRE((str.substr x 0 n), y) ---> SK_FIRST_CTN_PRE(x, y)
-    while (
-        a.getKind() == kind::STRING_SUBSTR
-        && TheoryStringsRewriter::checkEntailArith(
-               nm->mkNode(PLUS, a[1], a[2]), nm->mkNode(STRING_LENGTH, a[0])))
-    {
-      std::cout << a << " ---> " << a[0] << std::endl;
-      a = a[0];
-    }
-
     // SK_FIRST_CTN_POST(x, y) --->
     //   SK_SUFFIX_REM(x, (+ (str.len SK_FIRST_CTN_PRE(x, y)) (str.len y)))
     id = SK_SUFFIX_REM;
@@ -113,6 +119,7 @@ SkolemCache::normalizeStringSkolem(SkolemId id, Node a, Node b)
     b = Rewriter::rewrite(nm->mkNode(
         PLUS, nm->mkNode(STRING_LENGTH, pre), nm->mkNode(STRING_LENGTH, b)));
   }
+  */
 
   // SK_PURIFY(str.substr x 0 (str.indexof x y 0)) ---> SK_FIRST_CTN_PRE(x, y)
   if (id == SK_PURIFY && a.getKind() == kind::STRING_SUBSTR)
diff --git a/src/theory/strings/skolem_cache.h b/src/theory/strings/skolem_cache.h
index a6e91a246..e227a4263 100644
--- a/src/theory/strings/skolem_cache.h
+++ b/src/theory/strings/skolem_cache.h
@@ -27,6 +27,8 @@ namespace CVC4 {
 namespace theory {
 namespace strings {
 
+class TheoryStrings;
+
 /**
  * A cache of all string skolems generated by the TheoryStrings class. This
  * cache is used to ensure that duplicate skolems are not generated when
@@ -35,7 +37,8 @@ namespace strings {
 class SkolemCache
 {
  public:
-  SkolemCache();
+  SkolemCache(TheoryStrings* ts);
+
   /** Identifiers for skolem types
    *
    * The comments below document the properties of each skolem introduced by
@@ -136,6 +139,8 @@ class SkolemCache
   bool isSkolem(Node n) const;
 
  private:
+  TheoryStrings* d_ts;
+
   /**
    * Simplifies the arguments for a string skolem used for indexing into the
    * cache. In certain cases, we can share skolems with similar arguments e.g.
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 9da6fd277..77be51ce6 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -121,6 +121,7 @@ TheoryStrings::TheoryStrings(context::Context* c,
       d_functionsTerms(c),
       d_has_extf(c, false),
       d_has_str_code(false),
+      d_sk_cache(this),
       d_regexp_memberships(c),
       d_regexp_ucached(u),
       d_regexp_ccached(c),
diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index aa86f1bc1..cfa4abbb4 100644
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -133,6 +133,8 @@ struct StringsProxyVarAttributeId {};
 typedef expr::Attribute< StringsProxyVarAttributeId, bool > StringsProxyVarAttribute;
 
 class TheoryStrings : public Theory {
+  friend SkolemCache;
+
   typedef context::CDList<Node> NodeList;
   typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;
   typedef context::CDHashMap<Node, int, NodeHashFunction> NodeIntMap;