Eliminating static calls to rewriter from strings (#7302)

diff --git a/src/preprocessing/passes/strings_eager_pp.cpp b/src/preprocessing/passes/strings_eager_pp.cpp
index 80d6dd0e80fe6111584d9f78b28cb147893b98a3..ee962c33b2a38895dc39c20f9ec65521ea0526da 100644 (file)
--- a/src/preprocessing/passes/strings_eager_pp.cpp
+++ b/src/preprocessing/passes/strings_eager_pp.cpp
@@ -32,7 +32,7 @@ PreprocessingPassResult StringsEagerPp::applyInternal(
     AssertionPipeline* assertionsToPreprocess)
 {
   NodeManager* nm = NodeManager::currentNM();
-  theory::strings::SkolemCache skc(false);
+  theory::strings::SkolemCache skc(nullptr);
   theory::strings::StringsPreprocess pp(&skc);
   for (size_t i = 0, nasserts = assertionsToPreprocess->size(); i < nasserts;
        ++i)

diff --git a/src/theory/strings/arith_entail.cpp b/src/theory/strings/arith_entail.cpp
index d9cbc4c4048fe67b125cb7af47911a4beb5a5380..8950ea6fab387c3c99f8d98e2004025517c3328b 100644 (file)
--- a/src/theory/strings/arith_entail.cpp
+++ b/src/theory/strings/arith_entail.cpp
@@ -32,6 +32,8 @@ namespace strings {
 
 ArithEntail::ArithEntail(Rewriter* r) : d_rr(r) {}
 
+Node ArithEntail::rewrite(Node a) { return d_rr->rewrite(a); }
+
 bool ArithEntail::checkEq(Node a, Node b)
 {
   if (a == b)

diff --git a/src/theory/strings/arith_entail.h b/src/theory/strings/arith_entail.h
index e2b3d0af61d0da2a5788896aea9b5af54fbf2342..2158b23b0f60c12ff0eb8c2fd941d21bc7d03421 100644 (file)
--- a/src/theory/strings/arith_entail.h
+++ b/src/theory/strings/arith_entail.h
@@ -38,6 +38,11 @@ class ArithEntail
 {
  public:
   ArithEntail(Rewriter* r);
+  /**
+   * Returns the rewritten form a term, intended (although not enforced) to be
+   * an arithmetic term.
+   */
+  Node rewrite(Node a);
   /** check arithmetic entailment equal
    * Returns true if it is always the case that a = b.
    */

diff --git a/src/theory/strings/core_solver.cpp b/src/theory/strings/core_solver.cpp
index 2dfc73756233df65d644a18dae1ff0468a501221..d4d3761d8be1f529a60490bcb450e66094b003a5 100644 (file)
--- a/src/theory/strings/core_solver.cpp
+++ b/src/theory/strings/core_solver.cpp
@@ -1191,7 +1191,7 @@ void CoreSolver::processNEqc(Node eqc,
         continue;
       }
       Node eq = ni.first.eqNode(nj.first);
-      eq = Rewriter::rewrite(eq);
+      eq = rewrite(eq);
       if (eq == d_false)
       {
         std::vector<Node> exp;
@@ -1468,7 +1468,7 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi,
           << "Non-simple Case 1 : string lengths neither equal nor disequal"
           << std::endl;
       Node lenEq = nm->mkNode(EQUAL, xLenTerm, yLenTerm);
-      lenEq = Rewriter::rewrite(lenEq);
+      lenEq = rewrite(lenEq);
       iinfo.d_conc = nm->mkNode(OR, lenEq, lenEq.negate());
       iinfo.setId(InferenceId::STRINGS_LEN_SPLIT);
       info.d_pendingPhase[lenEq] = true;
@@ -1534,7 +1534,7 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi,
         //
         // E.g. "abc" ++ ... = nc ++ ... ---> (nc = "") v (nc != "")
         Node eq = nc.eqNode(emp);
-        eq = Rewriter::rewrite(eq);
+        eq = rewrite(eq);
         if (eq.isConst())
         {
           // If the equality rewrites to a constant, we must use the
@@ -1544,7 +1544,7 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi,
           Node p = skc->mkSkolemCached(nc, SkolemCache::SK_PURIFY, "lsym");
           Node pEq = p.eqNode(emp);
           // should not be constant
-          Assert(!Rewriter::rewrite(pEq).isConst());
+          Assert(!rewrite(pEq).isConst());
           // infer the purification equality, and the (dis)equality
           // with the empty string in the direction that the rewriter
           // inferred
@@ -1647,7 +1647,7 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi,
         {
           Node lt1 = e == 0 ? xLenTerm : yLenTerm;
           Node lt2 = e == 0 ? yLenTerm : xLenTerm;
-          Node entLit = Rewriter::rewrite(nm->mkNode(GT, lt1, lt2));
+          Node entLit = rewrite(nm->mkNode(GT, lt1, lt2));
           std::pair<bool, Node> et = d_state.entailmentCheck(
               options::TheoryOfMode::THEORY_OF_TYPE_BASED, entLit);
           if (et.first)
@@ -1848,7 +1848,7 @@ CoreSolver::ProcessLoopResult CoreSolver::processLoop(NormalForm& nfi,
   {
     Node t = i == 0 ? veci[loop_index] : t_yz;
     split_eq = t.eqNode(emp);
-    Node split_eqr = Rewriter::rewrite(split_eq);
+    Node split_eqr = rewrite(split_eq);
     // the equality could rewrite to false
     if (!split_eqr.isConst())
     {
@@ -1906,11 +1906,11 @@ CoreSolver::ProcessLoopResult CoreSolver::processLoop(NormalForm& nfi,
         v2.insert(v2.begin(), y);
         v2.insert(v2.begin(), z);
         restr = utils::mkNConcat(z, y);
-        cc = Rewriter::rewrite(s_zy.eqNode(utils::mkNConcat(v2, stype)));
+        cc = rewrite(s_zy.eqNode(utils::mkNConcat(v2, stype)));
       }
       else
       {
-        cc = Rewriter::rewrite(s_zy.eqNode(utils::mkNConcat(z, y)));
+        cc = rewrite(s_zy.eqNode(utils::mkNConcat(z, y)));
       }
       if (cc == d_false)
       {
@@ -2671,7 +2671,7 @@ void CoreSolver::checkLengthsEqc() {
       ant.insert(ant.end(), nfi.d_exp.begin(), nfi.d_exp.end());
       ant.push_back(lt.eqNode(nfi.d_base));
       Node lc = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, nf);
-      Node lcr = Rewriter::rewrite(lc);
+      Node lcr = rewrite(lc);
       Trace("strings-process-debug")
           << "Rewrote length " << lc << " to " << lcr << std::endl;
       if (!d_state.areEqual(llt, lcr))
@@ -2688,7 +2688,7 @@ bool CoreSolver::processInferInfo(CoreInferInfo& cii)
 {
   InferInfo& ii = cii.d_infer;
   // rewrite the conclusion, ensure non-trivial
-  Node concr = Rewriter::rewrite(ii.d_conc);
+  Node concr = rewrite(ii.d_conc);
 
   if (concr == d_true)
   {
@@ -2704,7 +2704,7 @@ bool CoreSolver::processInferInfo(CoreInferInfo& cii)
   // send phase requirements
   for (const std::pair<const Node, bool>& pp : cii.d_pendingPhase)
   {
-    Node ppr = Rewriter::rewrite(pp.first);
+    Node ppr = rewrite(pp.first);
     d_im.addPendingPhaseRequirement(ppr, pp.second);
   }
 

diff --git a/src/theory/strings/proof_checker.cpp b/src/theory/strings/proof_checker.cpp
index f566a4f390119017523a6d47689c0a408d74669c..3f5edbb8e6582e781c338cefc6878ed3ae51f1ac 100644 (file)
--- a/src/theory/strings/proof_checker.cpp
+++ b/src/theory/strings/proof_checker.cpp
@@ -275,7 +275,7 @@ Node StringProofRuleChecker::checkInternal(PfRule id,
       t0 = nm->mkNode(STRING_CONCAT, isRev ? w1 : t0, isRev ? t0 : w1);
     }
     // use skolem cache
-    SkolemCache skc(false);
+    SkolemCache skc(nullptr);
     std::vector<Node> newSkolems;
     Node conc = CoreSolver::getConclusion(t0, s0, id, isRev, &skc, newSkolems);
     return conc;
@@ -294,10 +294,10 @@ Node StringProofRuleChecker::checkInternal(PfRule id,
     {
       return Node::null();
     }
-    SkolemCache sc(false);
+    SkolemCache skc(nullptr);
     std::vector<Node> newSkolems;
     Node conc = CoreSolver::getConclusion(
-        atom[0][0], atom[1], id, isRev, &sc, newSkolems);
+        atom[0][0], atom[1], id, isRev, &skc, newSkolems);
     return conc;
   }
   else if (id == PfRule::STRING_REDUCTION
@@ -315,7 +315,7 @@ Node StringProofRuleChecker::checkInternal(PfRule id,
     {
       Assert(args.size() == 1);
       // we do not use optimizations
-      SkolemCache skc(false);
+      SkolemCache skc(nullptr);
       std::vector<Node> conj;
       ret = StringsPreprocess::reduce(t, conj, &skc);
       conj.push_back(t.eqNode(ret));
@@ -324,7 +324,7 @@ Node StringProofRuleChecker::checkInternal(PfRule id,
     else if (id == PfRule::STRING_EAGER_REDUCTION)
     {
       Assert(args.size() == 1);
-      SkolemCache skc(false);
+      SkolemCache skc(nullptr);
       ret = TermRegistry::eagerReduce(t, &skc);
     }
     else if (id == PfRule::STRING_LENGTH_POS)
@@ -412,8 +412,8 @@ Node StringProofRuleChecker::checkInternal(PfRule id,
     if (id == PfRule::RE_UNFOLD_POS)
     {
       std::vector<Node> newSkolems;
-      SkolemCache sc;
-      conc = RegExpOpr::reduceRegExpPos(skChild, &sc, newSkolems);
+      SkolemCache skc(nullptr);
+      conc = RegExpOpr::reduceRegExpPos(skChild, &skc, newSkolems);
     }
     else if (id == PfRule::RE_UNFOLD_NEG)
     {

diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp
index 268368e7fe4c220e6e2f0b6d7c34da494c2b827a..a37cb7936bc1b48ff67c8c50d1c5ecaed3a5ae68 100644 (file)
--- a/src/theory/strings/regexp_operation.cpp
+++ b/src/theory/strings/regexp_operation.cpp
@@ -31,8 +31,9 @@ namespace cvc5 {
 namespace theory {
 namespace strings {
 
-RegExpOpr::RegExpOpr(SkolemCache* sc)
-    : d_true(NodeManager::currentNM()->mkConst(true)),
+RegExpOpr::RegExpOpr(Env& env, SkolemCache* sc)
+    : EnvObj(env),
+      d_true(NodeManager::currentNM()->mkConst(true)),
       d_false(NodeManager::currentNM()->mkConst(false)),
       d_emptyRegexp(NodeManager::currentNM()->mkNode(kind::REGEXP_EMPTY,
                                                      std::vector<Node>{})),
@@ -79,7 +80,7 @@ RegExpConstType RegExpOpr::getRegExpConstType(Node r)
     {
       if (ck == STRING_TO_REGEXP)
       {
-        Node tmp = Rewriter::rewrite(cur[0]);
+        Node tmp = rewrite(cur[0]);
         d_constCache[cur] =
             tmp.isConst() ? RE_C_CONRETE_CONSTANT : RE_C_VARIABLE;
       }
@@ -145,7 +146,7 @@ int RegExpOpr::delta( Node r, Node &exp ) {
     }
     case STRING_TO_REGEXP:
     {
-      Node tmp = Rewriter::rewrite(r[0]);
+      Node tmp = rewrite(r[0]);
       if (tmp.isConst())
       {
         if (tmp == d_emptyString)
@@ -256,7 +257,7 @@ int RegExpOpr::delta( Node r, Node &exp ) {
   }
   if (!exp.isNull())
   {
-    exp = Rewriter::rewrite(exp);
+    exp = rewrite(exp);
   }
   std::pair<int, Node> p(ret, exp);
   d_delta_cache[r] = p;
@@ -309,7 +310,7 @@ int RegExpOpr::derivativeS(Node r, cvc5::String c, Node& retNode)
         break;
       }
       case kind::STRING_TO_REGEXP: {
-        Node tmp = Rewriter::rewrite(r[0]);
+        Node tmp = rewrite(r[0]);
         if(tmp.isConst()) {
           if(tmp == d_emptyString) {
             ret = 2;
@@ -341,7 +342,7 @@ int RegExpOpr::derivativeS(Node r, cvc5::String c, Node& retNode)
                 for(unsigned i=1; i<tmp.getNumChildren(); i++) {
                   vec_nodes.push_back(tmp[i]);
                 }
-                retNode = NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT, vec_nodes);
+                retNode = nm->mkNode(kind::REGEXP_CONCAT, vec_nodes);
                 ret = 1;
               } else {
                 ret = 2;
@@ -352,19 +353,20 @@ int RegExpOpr::derivativeS(Node r, cvc5::String c, Node& retNode)
               for(unsigned i=1; i<tmp.getNumChildren(); i++) {
                 vec_nodes.push_back(tmp[i]);
               }
-              rest = NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT, vec_nodes);
+              rest = nm->mkNode(kind::REGEXP_CONCAT, vec_nodes);
             }
           }
           if(ret == 0) {
             Node sk =
                 sm->mkDummySkolem("rsp", nm->stringType(), "Split RegExp");
-            retNode = NodeManager::currentNM()->mkNode(kind::STRING_TO_REGEXP, sk);
+            retNode = nm->mkNode(kind::STRING_TO_REGEXP, sk);
             if(!rest.isNull()) {
-              retNode = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT, retNode, rest));
+              retNode = rewrite(nm->mkNode(kind::REGEXP_CONCAT, retNode, rest));
             }
-            Node exp = tmp.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_CONCAT,
-                        NodeManager::currentNM()->mkConst(c), sk));
-            retNode = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::ITE, exp, retNode, d_emptyRegexp));
+            Node exp =
+                tmp.eqNode(nm->mkNode(kind::STRING_CONCAT, nm->mkConst(c), sk));
+            retNode =
+                rewrite(nm->mkNode(kind::ITE, exp, retNode, d_emptyRegexp));
           }
         }
         break;
@@ -393,7 +395,7 @@ int RegExpOpr::derivativeS(Node r, cvc5::String c, Node& retNode)
             Node tmp = vec_nodes2.size()==0 ? d_emptySingleton :
               vec_nodes2.size()==1 ? vec_nodes2[0] : NodeManager::currentNM()->mkNode( kind::REGEXP_CONCAT, vec_nodes2 );
             if(dnode != d_true) {
-              tmp = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::ITE, dnode, tmp, d_emptyRegexp));
+              tmp = rewrite(nm->mkNode(kind::ITE, dnode, tmp, d_emptyRegexp));
               ret = 0;
             }
             if(std::find(vec_nodes.begin(), vec_nodes.end(), tmp) == vec_nodes.end()) {
@@ -403,7 +405,7 @@ int RegExpOpr::derivativeS(Node r, cvc5::String c, Node& retNode)
           Node exp3;
           int rt2 = delta( r[i], exp3 );
           if( rt2 == 0 ) {
-            dnode = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::AND, dnode, exp3));
+            dnode = rewrite(nm->mkNode(kind::AND, dnode, exp3));
           } else if( rt2 == 2 ) {
             break;
           }
@@ -513,7 +515,7 @@ int RegExpOpr::derivativeS(Node r, cvc5::String c, Node& retNode)
       }
     }
     if(retNode != d_emptyRegexp) {
-      retNode = Rewriter::rewrite( retNode );
+      retNode = rewrite(retNode);
     }
     std::pair< Node, int > p(retNode, ret);
     d_deriv_cache[dv] = p;
@@ -695,7 +697,7 @@ Node RegExpOpr::derivativeSingle(Node r, cvc5::String c)
       }
     }
     if(retNode != d_emptyRegexp) {
-      retNode = Rewriter::rewrite( retNode );
+      retNode = rewrite(retNode);
     }
     d_dv_cache[dv] = retNode;
   }
@@ -732,7 +734,7 @@ void RegExpOpr::firstChars(Node r, std::set<unsigned> &pcset, SetNodes &pvset)
         break;
       }
       case kind::STRING_TO_REGEXP: {
-        Node st = Rewriter::rewrite(r[0]);
+        Node st = rewrite(r[0]);
         if(st.isConst()) {
           String s = st.getConst<String>();
           if(s.size() != 0) {
@@ -994,7 +996,6 @@ Node RegExpOpr::reduceRegExpNegConcatFixed(Node mem, Node reLen, size_t index)
     }
   }
   Node r2 = nvec.size() == 1 ? nvec[0] : nm->mkNode(REGEXP_CONCAT, nvec);
-  r2 = Rewriter::rewrite(r2);
   Node s2r2 = nm->mkNode(STRING_IN_REGEXP, s2, r2).negate();
   Node conc = nm->mkNode(OR, s1r1, s2r2);
   if (!b1v.isNull())
@@ -1131,7 +1132,7 @@ Node RegExpOpr::convert1(unsigned cnt, Node n) {
   Trace("regexp-debug") << "... getting r1=" << r1 << ", and r2=" << r2 << std::endl;
   Node ret = r1==d_emptySingleton ? r2 : NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT, 
      NodeManager::currentNM()->mkNode(kind::REGEXP_STAR, r1), r2);
-  ret = Rewriter::rewrite( ret );
+  ret = rewrite(ret);
   Trace("regexp-debug") << "... done convert at " << cnt << ", with return " << ret << std::endl;
   return ret;
 }
@@ -1218,6 +1219,7 @@ Node RegExpOpr::intersectInternal( Node r1, Node r2, std::map< PairNodes, Node >
     r1 = r2;
     r2 = tmpNode;
   }
+  NodeManager* nm = NodeManager::currentNM();
   Trace("regexp-int") << "Starting INTERSECT(" << cnt << "):\n  "<< mkString(r1) << ",\n  " << mkString(r2) << std::endl;
   std::pair < Node, Node > p(r1, r2);
   std::map < PairNodes, Node >::const_iterator itr = d_inter_cache.find(p);
@@ -1319,16 +1321,21 @@ Node RegExpOpr::intersectInternal( Node r1, Node r2, std::map< PairNodes, Node >
             cacheX[ pp ] = rt;
           }
 
-          rt = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT,
-            NodeManager::currentNM()->mkNode(kind::STRING_TO_REGEXP, NodeManager::currentNM()->mkConst(c)), rt) );
+          rt = rewrite(
+              nm->mkNode(kind::REGEXP_CONCAT,
+                         nm->mkNode(kind::STRING_TO_REGEXP, nm->mkConst(c)),
+                         rt));
 
           Trace("regexp-int-debug") << "  ... got p(r1,c) && p(r2,c) = " << mkString(rt) << std::endl;
           vec_nodes.push_back(rt);
         }
-        rNode = Rewriter::rewrite( vec_nodes.size()==0 ? d_emptyRegexp : vec_nodes.size()==1 ? vec_nodes[0] :
-            NodeManager::currentNM()->mkNode(kind::REGEXP_UNION, vec_nodes) );
+        rNode = rewrite(vec_nodes.size() == 0
+                            ? d_emptyRegexp
+                            : vec_nodes.size() == 1
+                                  ? vec_nodes[0]
+                                  : nm->mkNode(kind::REGEXP_UNION, vec_nodes));
         rNode = convert1(cnt, rNode);
-        rNode = Rewriter::rewrite( rNode );
+        rNode = rewrite(rNode);
       }
     }
     Trace("regexp-int-debug") << "  ... try testing no RV of " << mkString(rNode) << std::endl;

diff --git a/src/theory/strings/regexp_operation.h b/src/theory/strings/regexp_operation.h
index 04b5a999d345b01719a847ef309577182c130fe1..75262a86292a76cb3138386159b5386422727fa8 100644 (file)
--- a/src/theory/strings/regexp_operation.h
+++ b/src/theory/strings/regexp_operation.h
@@ -24,6 +24,7 @@
 #include <vector>
 
 #include "expr/node.h"
+#include "smt/env_obj.h"
 #include "theory/strings/skolem_cache.h"
 #include "util/string.h"
 
@@ -53,7 +54,8 @@ enum RegExpConstType
   RE_C_UNKNOWN,
 };
 
-class RegExpOpr {
+class RegExpOpr : protected EnvObj
+{
   typedef std::pair<Node, cvc5::String> PairNodeStr;
   typedef std::set< Node > SetNodes;
   typedef std::pair< Node, Node > PairNodes;
@@ -106,7 +108,7 @@ class RegExpOpr {
   void firstChars(Node r, std::set<unsigned> &pcset, SetNodes &pvset);
 
  public:
-  RegExpOpr(SkolemCache* sc);
+  RegExpOpr(Env& env, SkolemCache* sc);
   ~RegExpOpr();
 
   /**

diff --git a/src/theory/strings/regexp_solver.cpp b/src/theory/strings/regexp_solver.cpp
index 7d077059b49a5e618ef43b2887455c83500a11e4..92dee215b48acd5127bf1f480229d13f37b74396 100644 (file)
--- a/src/theory/strings/regexp_solver.cpp
+++ b/src/theory/strings/regexp_solver.cpp
@@ -48,7 +48,7 @@ RegExpSolver::RegExpSolver(Env& env,
       d_regexp_ucached(userContext()),
       d_regexp_ccached(context()),
       d_processed_memberships(context()),
-      d_regexp_opr(skc)
+      d_regexp_opr(env, skc)
 {
   d_emptyString = NodeManager::currentNM()->mkConst(::cvc5::String(""));
   d_emptyRegexp = NodeManager::currentNM()->mkNode(REGEXP_EMPTY);
@@ -158,7 +158,7 @@ void RegExpSolver::check(const std::map<Node, std::vector<Node> >& mems)
             << "We have regular expression assertion : " << assertion
             << std::endl;
         Node atom = assertion.getKind() == NOT ? assertion[0] : assertion;
-        Assert(atom == Rewriter::rewrite(atom));
+        Assert(atom == rewrite(atom));
         bool polarity = assertion.getKind() != NOT;
         if (polarity != (e == 0))
         {
@@ -205,7 +205,7 @@ void RegExpSolver::check(const std::map<Node, std::vector<Node> >& mems)
         if (nx != x || changed)
         {
           // We rewrite the membership nx IN r.
-          Node tmp = Rewriter::rewrite(nm->mkNode(STRING_IN_REGEXP, nx, r));
+          Node tmp = rewrite(nm->mkNode(STRING_IN_REGEXP, nx, r));
           Trace("strings-regexp-nf") << "Simplifies to " << tmp << std::endl;
           if (tmp.isConst())
           {
@@ -481,7 +481,7 @@ bool RegExpSolver::checkEqcIntersect(const std::vector<Node>& mems)
     }
     // rewrite to ensure the equality checks below are precise
     Node mres = nm->mkNode(STRING_IN_REGEXP, mi[0], resR);
-    Node mresr = Rewriter::rewrite(mres);
+    Node mresr = rewrite(mres);
     if (mresr == mi)
     {
       // if R1 = intersect( R1, R2 ), then x in R1 ^ x in R2 is equivalent
@@ -633,7 +633,7 @@ bool RegExpSolver::deriveRegExp(Node x,
           vec_nodes.push_back(x[i]);
         }
         Node left = utils::mkConcat(vec_nodes, x.getType());
-        left = Rewriter::rewrite(left);
+        left = rewrite(left);
         conc = NodeManager::currentNM()->mkNode(STRING_IN_REGEXP, left, dc);
       }
     }
@@ -678,8 +678,7 @@ Node RegExpSolver::getNormalSymRegExp(Node r, std::vector<Node>& nf_exp)
       {
         vec_nodes.push_back(getNormalSymRegExp(cr, nf_exp));
       }
-      ret = Rewriter::rewrite(
-          NodeManager::currentNM()->mkNode(r.getKind(), vec_nodes));
+      ret = rewrite(NodeManager::currentNM()->mkNode(r.getKind(), vec_nodes));
       break;
     }
     default:

diff --git a/src/theory/strings/sequences_rewriter.cpp b/src/theory/strings/sequences_rewriter.cpp
index bd8a4d8df42fbd184cc5608cb66fd79dde2df9e6..76175a32fa9ebb0728cb35e989e5f1b2b4e5104d 100644 (file)
--- a/src/theory/strings/sequences_rewriter.cpp
+++ b/src/theory/strings/sequences_rewriter.cpp
@@ -1813,8 +1813,9 @@ Node SequencesRewriter::rewriteSubstr(Node node)
     else if (r == 1)
     {
       Node tot_len =
-          Rewriter::rewrite(nm->mkNode(kind::STRING_LENGTH, node[0]));
-      Node end_pt = Rewriter::rewrite(nm->mkNode(kind::PLUS, node[1], node[2]));
+          d_arithEntail.rewrite(nm->mkNode(kind::STRING_LENGTH, node[0]));
+      Node end_pt =
+          d_arithEntail.rewrite(nm->mkNode(kind::PLUS, node[1], node[2]));
       if (node[2] != tot_len)
       {
         if (d_arithEntail.check(node[2], tot_len))
@@ -1826,13 +1827,14 @@ Node SequencesRewriter::rewriteSubstr(Node node)
         else
         {
           // strip up to ( str.len(node[0]) - end_pt ) off the end of the string
-          curr = Rewriter::rewrite(nm->mkNode(kind::MINUS, tot_len, end_pt));
+          curr =
+              d_arithEntail.rewrite(nm->mkNode(kind::MINUS, tot_len, end_pt));
         }
       }
 
       // (str.substr s x y) --> "" if x < len(s) |= 0 >= y
       Node n1_lt_tot_len =
-          Rewriter::rewrite(nm->mkNode(kind::LT, node[1], tot_len));
+          d_arithEntail.rewrite(nm->mkNode(kind::LT, node[1], tot_len));
       if (d_arithEntail.checkWithAssumption(
               n1_lt_tot_len, zero, node[2], false))
       {
@@ -1842,7 +1844,7 @@ Node SequencesRewriter::rewriteSubstr(Node node)
 
       // (str.substr s x y) --> "" if 0 < y |= x >= str.len(s)
       Node non_zero_len =
-          Rewriter::rewrite(nm->mkNode(kind::LT, zero, node[2]));
+          d_arithEntail.rewrite(nm->mkNode(kind::LT, zero, node[2]));
       if (d_arithEntail.checkWithAssumption(
               non_zero_len, node[1], tot_len, false))
       {
@@ -1852,7 +1854,7 @@ Node SequencesRewriter::rewriteSubstr(Node node)
 
       // (str.substr s x y) --> "" if x >= 0 |= 0 >= str.len(s)
       Node geq_zero_start =
-          Rewriter::rewrite(nm->mkNode(kind::GEQ, node[1], zero));
+          d_arithEntail.rewrite(nm->mkNode(kind::GEQ, node[1], zero));
       if (d_arithEntail.checkWithAssumption(
               geq_zero_start, zero, tot_len, false))
       {
@@ -1905,8 +1907,8 @@ Node SequencesRewriter::rewriteSubstr(Node node)
 
       // the length of a string from the inner substr subtracts the start point
       // of the outer substr
-      Node len_from_inner =
-          Rewriter::rewrite(nm->mkNode(kind::MINUS, node[0][2], start_outer));
+      Node len_from_inner = d_arithEntail.rewrite(
+          nm->mkNode(kind::MINUS, node[0][2], start_outer));
       Node len_from_outer = node[2];
       Node new_len;
       // take quantity that is for sure smaller than the other

diff --git a/src/theory/strings/skolem_cache.cpp b/src/theory/strings/skolem_cache.cpp
index 34cb454556ab616430866137eaa0211155fa0f29..0d2e9cacba449140da601d8ec5f85b44cbfce6a5 100644 (file)
--- a/src/theory/strings/skolem_cache.cpp
+++ b/src/theory/strings/skolem_cache.cpp
@@ -50,7 +50,7 @@ struct LengthVarAttributeId
 };
 typedef expr::Attribute<LengthVarAttributeId, Node> LengthVarAttribute;
 
-SkolemCache::SkolemCache(bool useOpts) : d_useOpts(useOpts)
+SkolemCache::SkolemCache(Rewriter* rr) : d_rr(rr)
 {
   NodeManager* nm = NodeManager::currentNM();
   d_strType = nm->stringType();
@@ -75,16 +75,16 @@ Node SkolemCache::mkTypedSkolemCached(
   SkolemId idOrig = id;
   // do not rewrite beforehand if we are not using optimizations, this is so
   // that the proof checker does not depend on the rewriter.
-  if (d_useOpts)
+  if (d_rr != nullptr)
   {
-    a = a.isNull() ? a : Rewriter::rewrite(a);
-    b = b.isNull() ? b : Rewriter::rewrite(b);
+    a = a.isNull() ? a : d_rr->rewrite(a);
+    b = b.isNull() ? b : d_rr->rewrite(b);
   }
   std::tie(id, a, b) = normalizeStringSkolem(id, a, b);
 
   // optimization: if we aren't asking for the purification skolem for constant
   // a, and the skolem is equivalent to a, then we just return a.
-  if (d_useOpts && idOrig != SK_PURIFY && id == SK_PURIFY && a.isConst())
+  if (d_rr != nullptr && idOrig != SK_PURIFY && id == SK_PURIFY && a.isConst())
   {
     Trace("skolem-cache") << "...optimization: return constant " << a
                           << std::endl;
@@ -292,10 +292,10 @@ SkolemCache::normalizeStringSkolem(SkolemId id, Node a, Node b)
     b = Node::null();
   }
 
-  if (d_useOpts)
+  if (d_rr != nullptr)
   {
-    a = a.isNull() ? a : Rewriter::rewrite(a);
-    b = b.isNull() ? b : Rewriter::rewrite(b);
+    a = a.isNull() ? a : d_rr->rewrite(a);
+    b = b.isNull() ? b : d_rr->rewrite(b);
   }
   Trace("skolem-cache") << "normalizeStringSkolem end: (" << id << ", " << a
                         << ", " << b << ")" << std::endl;

diff --git a/src/theory/strings/skolem_cache.h b/src/theory/strings/skolem_cache.h
index dabe333ae53b19df02ac895da2874a47bc5a296b..2b714781b1978bd6719691f2edbdbe080b2974af 100644 (file)
--- a/src/theory/strings/skolem_cache.h
+++ b/src/theory/strings/skolem_cache.h
@@ -27,6 +27,9 @@
 
 namespace cvc5 {
 namespace theory {
+
+class Rewriter;
+
 namespace strings {
 
 /**
@@ -40,10 +43,11 @@ class SkolemCache
   /**
    * Constructor.
    *
-   * useOpts determines if we aggressively share Skolems or return the constants
-   * they are entailed to be equal to.
+   * @param rr determines if we aggressively share Skolems based on rewriting or
+   * return the constants they are entailed to be equal to. This argument is
+   * optional.
    */
-  SkolemCache(bool useOpts = true);
+  SkolemCache(Rewriter* rr);
   /** Identifiers for skolem types
    *
    * The comments below document the properties of each skolem introduced by
@@ -216,8 +220,8 @@ class SkolemCache
   std::tuple<SkolemId, Node, Node> normalizeStringSkolem(SkolemId id,
                                                          Node a,
                                                          Node b);
-  /** whether we are using optimizations */
-  bool d_useOpts;
+  /** the optional rewriter */
+  Rewriter* d_rr;
   /** string type */
   TypeNode d_strType;
   /** Constant node zero */

diff --git a/src/theory/strings/term_registry.cpp b/src/theory/strings/term_registry.cpp
index 897d02366332df5622956ba2bcf9c58eac13f693..9252babba9111cdd7d17cdfb5e7bc984523e032f 100644 (file)
--- a/src/theory/strings/term_registry.cpp
+++ b/src/theory/strings/term_registry.cpp
@@ -49,6 +49,8 @@ TermRegistry::TermRegistry(Env& env,
       d_im(nullptr),
       d_statistics(statistics),
       d_hasStrCode(false),
+      d_hasSeqUpdate(false),
+      d_skCache(env.getRewriter()),
       d_aent(env.getRewriter()),
       d_functionsTerms(context()),
       d_inputVars(userContext()),
@@ -57,10 +59,11 @@ TermRegistry::TermRegistry(Env& env,
       d_registeredTypes(userContext()),
       d_proxyVar(userContext()),
       d_lengthLemmaTermsCache(userContext()),
-      d_epg(
-          pnm ? new EagerProofGenerator(
-              pnm, userContext(), "strings::TermRegistry::EagerProofGenerator")
-              : nullptr)
+      d_epg(pnm ? new EagerProofGenerator(
+                      pnm,
+                      userContext(),
+                      "strings::TermRegistry::EagerProofGenerator")
+                : nullptr)
 {
   NodeManager* nm = NodeManager::currentNM();
   d_zero = nm->mkConst(Rational(0));

diff --git a/test/unit/theory/regexp_operation_black.cpp b/test/unit/theory/regexp_operation_black.cpp
index 23d2bfd22f8a54c713e5c675c30e9c1e07bdcc83..9a98b174deedde0b3ef13143e104914ed3e6fd2b 100644 (file)
--- a/test/unit/theory/regexp_operation_black.cpp
+++ b/test/unit/theory/regexp_operation_black.cpp
@@ -23,8 +23,8 @@
 #include "smt/smt_engine_scope.h"
 #include "test_smt.h"
 #include "theory/rewriter.h"
-#include "theory/strings/regexp_operation.h"
-#include "theory/strings/skolem_cache.h"
+#include "theory/strings/regexp_entail.h"
+#include "util/string.h"
 
 namespace cvc5 {
 
@@ -40,8 +40,6 @@ class TestTheoryBlackRegexpOperation : public TestSmt
   void SetUp() override
   {
     TestSmt::SetUp();
-    d_skolemCache.reset(new SkolemCache());
-    d_regExpOpr.reset(new RegExpOpr(d_skolemCache.get()));
   }
 
   void includes(Node r1, Node r2)
@@ -49,7 +47,7 @@ class TestTheoryBlackRegexpOperation : public TestSmt
     r1 = Rewriter::rewrite(r1);
     r2 = Rewriter::rewrite(r2);
     std::cout << r1 << " includes " << r2 << std::endl;
-    ASSERT_TRUE(d_regExpOpr->regExpIncludes(r1, r2));
+    ASSERT_TRUE(RegExpEntail::regExpIncludes(r1, r2));
   }
 
   void doesNotInclude(Node r1, Node r2)
@@ -57,11 +55,8 @@ class TestTheoryBlackRegexpOperation : public TestSmt
     r1 = Rewriter::rewrite(r1);
     r2 = Rewriter::rewrite(r2);
     std::cout << r1 << " does not include " << r2 << std::endl;
-    ASSERT_FALSE(d_regExpOpr->regExpIncludes(r1, r2));
+    ASSERT_FALSE(RegExpEntail::regExpIncludes(r1, r2));
   }
-
-  std::unique_ptr<SkolemCache> d_skolemCache;
-  std::unique_ptr<RegExpOpr> d_regExpOpr;
 };
 
 TEST_F(TestTheoryBlackRegexpOperation, basic)

diff --git a/test/unit/theory/theory_strings_skolem_cache_black.cpp b/test/unit/theory/theory_strings_skolem_cache_black.cpp
index 62de217972c82e2adb429528cd93fab93b3e7fdd..24ed0cd06319acb446b5e26ccc871c54f490fe96 100644 (file)
--- a/test/unit/theory/theory_strings_skolem_cache_black.cpp
+++ b/test/unit/theory/theory_strings_skolem_cache_black.cpp
@@ -46,7 +46,7 @@ TEST_F(TestTheoryBlackStringsSkolemCache, mkSkolemCached)
       d_nodeManager->mkNode(kind::STRING_INDEXOF, a, b, zero));
   Node sc = d_nodeManager->mkNode(kind::STRING_SUBSTR, c, zero, n);
 
-  SkolemCache sk;
+  SkolemCache sk(nullptr);
 
   // Check that skolems are shared between:
   //