regexp skolems

7 files changed, 64 insertions, 15 deletions

diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp
index 8707593c7..5d4131465 100644
--- a/src/theory/strings/regexp_operation.cpp
+++ b/src/theory/strings/regexp_operation.cpp
@@ -28,8 +28,9 @@ namespace CVC4 {
 namespace theory {
 namespace strings {
 
-RegExpOpr::RegExpOpr()
-    : d_emptyString(NodeManager::currentNM()->mkConst(::CVC4::String(""))),
+RegExpOpr::RegExpOpr(SkolemCache* sc)
+    : d_sc(sc),
+      d_emptyString(NodeManager::currentNM()->mkConst(::CVC4::String(""))),
       d_true(NodeManager::currentNM()->mkConst(true)),
       d_false(NodeManager::currentNM()->mkConst(false)),
       d_emptySingleton(NodeManager::currentNM()->mkNode(kind::STRING_TO_REGEXP,
@@ -1171,12 +1172,12 @@ void RegExpOpr::simplifyPRegExp( Node s, Node r, std::vector< Node > &new_nodes
           NodeManager* nm = NodeManager::currentNM();
           Node se = s.eqNode(d_emptyString);
           Node sinr = nm->mkNode(kind::STRING_IN_REGEXP, s, r[0]);
-          Node sk1 = nm->mkSkolem(
-              "rs", s.getType(), "created for regular expression star");
-          Node sk2 = nm->mkSkolem(
-              "rs", s.getType(), "created for regular expression star");
-          Node sk3 = nm->mkSkolem(
-              "rs", s.getType(), "created for regular expression star");
+          Node sk1 =
+              d_sc->mkSkolemCached(s, r[0], SkolemCache::SK_STAR_PREFIX, "rs1");
+          Node sk2 =
+              d_sc->mkSkolemCached(s, r[0], SkolemCache::SK_STAR_MID, "rs2");
+          Node sk3 =
+              d_sc->mkSkolemCached(s, r[0], SkolemCache::SK_STAR_SUFFIX, "rs3");
 
           NodeBuilder<> nb(kind::AND);
           nb << sk1.eqNode(d_emptyString).negate();
diff --git a/src/theory/strings/regexp_operation.h b/src/theory/strings/regexp_operation.h
index c7464760d..0d84f13a5 100644
--- a/src/theory/strings/regexp_operation.h
+++ b/src/theory/strings/regexp_operation.h
@@ -19,14 +19,16 @@
 #ifndef CVC4__THEORY__STRINGS__REGEXP__OPERATION_H
 #define CVC4__THEORY__STRINGS__REGEXP__OPERATION_H
 
-#include <vector>
-#include <set>
 #include <algorithm>
 #include <climits>
+#include <set>
+#include <vector>
+
+#include "theory/rewriter.h"
+#include "theory/strings/skolem_cache.h"
+#include "theory/theory.h"
 #include "util/hash.h"
 #include "util/regexp.h"
-#include "theory/theory.h"
-#include "theory/rewriter.h"
 //#include "context/cdhashmap.h"
 
 namespace CVC4 {
@@ -58,6 +60,7 @@ class RegExpOpr {
   typedef std::pair< Node, Node > PairNodes;
 
  private:
+  SkolemCache* d_sc;
   /** the code point of the last character in the alphabet we are using */
   unsigned d_lastchar;
   Node d_emptyString;
@@ -108,7 +111,7 @@ class RegExpOpr {
   void firstChars(Node r, std::set<unsigned> &pcset, SetNodes &pvset);
 
  public:
-  RegExpOpr();
+  RegExpOpr(SkolemCache* sc);
   ~RegExpOpr();
 
   /**
diff --git a/src/theory/strings/regexp_solver.cpp b/src/theory/strings/regexp_solver.cpp
index e4fe2cf17..801dfd99e 100644
--- a/src/theory/strings/regexp_solver.cpp
+++ b/src/theory/strings/regexp_solver.cpp
@@ -36,6 +36,7 @@ namespace strings {
 RegExpSolver::RegExpSolver(TheoryStrings& p,
                            SolverState& s,
                            InferenceManager& im,
+                           SkolemCache* sc,
                            context::Context* c,
                            context::UserContext* u)
     : d_parent(p),
@@ -43,7 +44,8 @@ RegExpSolver::RegExpSolver(TheoryStrings& p,
       d_im(im),
       d_regexp_ucached(u),
       d_regexp_ccached(c),
-      d_processed_memberships(c)
+      d_processed_memberships(c),
+      d_regexp_opr(sc)
 {
   d_emptyString = NodeManager::currentNM()->mkConst(::CVC4::String(""));
   std::vector<Node> nvec;
diff --git a/src/theory/strings/regexp_solver.h b/src/theory/strings/regexp_solver.h
index a43ea516a..cd7fc3014 100644
--- a/src/theory/strings/regexp_solver.h
+++ b/src/theory/strings/regexp_solver.h
@@ -19,12 +19,14 @@
 #define CVC4__THEORY__STRINGS__REGEXP_SOLVER_H
 
 #include <map>
+
 #include "context/cdhashset.h"
 #include "context/cdlist.h"
 #include "context/context.h"
 #include "expr/node.h"
 #include "theory/strings/inference_manager.h"
 #include "theory/strings/regexp_operation.h"
+#include "theory/strings/skolem_cache.h"
 #include "theory/strings/solver_state.h"
 #include "util/regexp.h"
 
@@ -47,6 +49,7 @@ class RegExpSolver
   RegExpSolver(TheoryStrings& p,
                SolverState& s,
                InferenceManager& im,
+               SkolemCache* sc,
                context::Context* c,
                context::UserContext* u);
   ~RegExpSolver() {}
diff --git a/src/theory/strings/skolem_cache.cpp b/src/theory/strings/skolem_cache.cpp
index 354c286ac..8b9ec5856 100644
--- a/src/theory/strings/skolem_cache.cpp
+++ b/src/theory/strings/skolem_cache.cpp
@@ -202,6 +202,41 @@ SkolemCache::normalizeStringSkolem(SkolemId id, Node a, Node b)
     b = Rewriter::rewrite(nm->mkNode(STRING_LENGTH, b));
   }
 
+  if (id == SK_STAR_PREFIX)
+  {
+    Node len = TheoryStringsRewriter::getFixedLengthForRegexp(b);
+    if (!len.isNull())
+    {
+      id = SK_PREFIX;
+      b = len;
+    }
+  }
+  else if (id == SK_STAR_MID)
+  {
+    Node len = TheoryStringsRewriter::getFixedLengthForRegexp(b);
+    if (!len.isNull())
+    {
+      id = SK_PURIFY;
+      a = nm->mkNode(
+          STRING_SUBSTR,
+          a,
+          len,
+          nm->mkNode(
+              MINUS, nm->mkNode(STRING_LENGTH, a), nm->mkNode(PLUS, len, len)));
+      b = Node::null();
+    }
+  }
+  else if (id == SK_STAR_SUFFIX)
+  {
+    Node len = TheoryStringsRewriter::getFixedLengthForRegexp(b);
+    if (!len.isNull())
+    {
+      id = SK_SUFFIX_REM;
+      b = Rewriter::rewrite(
+          nm->mkNode(MINUS, nm->mkNode(STRING_LENGTH, a), len));
+    }
+  }
+
   if (id == SK_PURIFY && a.getKind() == kind::STRING_SUBSTR)
   {
     Node s = a[0];
diff --git a/src/theory/strings/skolem_cache.h b/src/theory/strings/skolem_cache.h
index 1b00d7070..6f296255b 100644
--- a/src/theory/strings/skolem_cache.h
+++ b/src/theory/strings/skolem_cache.h
@@ -105,6 +105,11 @@ class SkolemCache
     // b > 0 =>
     //    exists k. a = a' ++ k ^ len( a ) = b
     SK_SUFFIX_REM,
+
+    SK_STAR_PREFIX,
+    SK_STAR_MID,
+    SK_STAR_SUFFIX,
+
     // --------------- integer skolems
     // exists k. ( b occurs k times in a )
     SK_NUM_OCCUR,
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 1e4f13f74..4eaa9c3aa 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -108,7 +108,7 @@ TheoryStrings::TheoryStrings(context::Context* c,
       d_functionsTerms(c),
       d_has_extf(c, false),
       d_has_str_code(false),
-      d_regexp_solver(*this, d_state, d_im, c, u),
+      d_regexp_solver(*this, d_state, d_im, &d_sk_cache, c, u),
       d_input_vars(u),
       d_input_var_lsum(u),
       d_cardinality_lits(u),