From 763f292c2d36e54dcc5b334bba02bb211e79d200 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 4 Oct 2021 12:42:39 -0500 Subject: [PATCH] Eliminating static calls to rewriter from strings (#7302) --- src/preprocessing/passes/strings_eager_pp.cpp | 2 +- src/theory/strings/arith_entail.cpp | 2 + src/theory/strings/arith_entail.h | 5 ++ src/theory/strings/core_solver.cpp | 22 +++---- src/theory/strings/proof_checker.cpp | 14 ++--- src/theory/strings/regexp_operation.cpp | 57 +++++++++++-------- src/theory/strings/regexp_operation.h | 6 +- src/theory/strings/regexp_solver.cpp | 13 ++--- src/theory/strings/sequences_rewriter.cpp | 18 +++--- src/theory/strings/skolem_cache.cpp | 16 +++--- src/theory/strings/skolem_cache.h | 14 +++-- src/theory/strings/term_registry.cpp | 11 ++-- test/unit/theory/regexp_operation_black.cpp | 13 ++--- .../theory_strings_skolem_cache_black.cpp | 2 +- 14 files changed, 107 insertions(+), 88 deletions(-) diff --git a/src/preprocessing/passes/strings_eager_pp.cpp b/src/preprocessing/passes/strings_eager_pp.cpp index 80d6dd0e8..ee962c33b 100644 --- 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 d9cbc4c40..8950ea6fa 100644 --- 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 e2b3d0af6..2158b23b0 100644 --- 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 2dfc73756..d4d3761d8 100644 --- 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 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 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& 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 f566a4f39..3f5edbb8e 100644 --- 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 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 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 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 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 268368e7f..a37cb7936 100644 --- 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{})), @@ -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 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; imkNode(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; imkNode(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 &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(); 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 04b5a999d..75262a862 100644 --- a/src/theory/strings/regexp_operation.h +++ b/src/theory/strings/regexp_operation.h @@ -24,6 +24,7 @@ #include #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 PairNodeStr; typedef std::set< Node > SetNodes; typedef std::pair< Node, Node > PairNodes; @@ -106,7 +108,7 @@ class RegExpOpr { void firstChars(Node r, std::set &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 7d077059b..92dee215b 100644 --- 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 >& 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 >& 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& 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& 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 bd8a4d8df..76175a32f 100644 --- 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 34cb45455..0d2e9cacb 100644 --- a/src/theory/strings/skolem_cache.cpp +++ b/src/theory/strings/skolem_cache.cpp @@ -50,7 +50,7 @@ struct LengthVarAttributeId }; typedef expr::Attribute 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 dabe333ae..2b714781b 100644 --- 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 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 897d02366..9252babba 100644 --- 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 23d2bfd22..9a98b174d 100644 --- 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 d_skolemCache; - std::unique_ptr 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 62de21797..24ed0cd06 100644 --- 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: // -- 2.30.2