diff options
Diffstat (limited to 'src/theory/strings')
-rw-r--r-- | src/theory/strings/array_core_solver.cpp | 1 | ||||
-rw-r--r-- | src/theory/strings/base_solver.cpp | 11 | ||||
-rw-r--r-- | src/theory/strings/base_solver.h | 4 | ||||
-rw-r--r-- | src/theory/strings/core_solver.cpp | 32 | ||||
-rw-r--r-- | src/theory/strings/regexp_elim.cpp | 9 | ||||
-rw-r--r-- | src/theory/strings/regexp_entail.cpp | 19 | ||||
-rw-r--r-- | src/theory/strings/regexp_entail.h | 2 | ||||
-rw-r--r-- | src/theory/strings/regexp_solver.cpp | 2 | ||||
-rw-r--r-- | src/theory/strings/sequences_rewriter.cpp | 26 | ||||
-rw-r--r-- | src/theory/strings/sequences_rewriter.h | 7 | ||||
-rw-r--r-- | src/theory/strings/solver_state.cpp | 6 | ||||
-rw-r--r-- | src/theory/strings/term_registry.cpp | 20 | ||||
-rw-r--r-- | src/theory/strings/term_registry.h | 16 | ||||
-rw-r--r-- | src/theory/strings/theory_strings.cpp | 25 | ||||
-rw-r--r-- | src/theory/strings/theory_strings.h | 2 | ||||
-rw-r--r-- | src/theory/strings/theory_strings_utils.cpp | 22 | ||||
-rw-r--r-- | src/theory/strings/theory_strings_utils.h | 21 |
17 files changed, 112 insertions, 113 deletions
diff --git a/src/theory/strings/array_core_solver.cpp b/src/theory/strings/array_core_solver.cpp index 3b8fdeff4..9e3921e29 100644 --- a/src/theory/strings/array_core_solver.cpp +++ b/src/theory/strings/array_core_solver.cpp @@ -116,7 +116,6 @@ void ArrayCoreSolver::checkUpdate(const std::vector<Node>& updateTerms) Node left = nm->mkNode(SEQ_NTH, termProxy, n[1]); Node right = nm->mkNode(SEQ_NTH, n[2], nm->mkConstInt(Rational(0))); // n[2][0] - right = Rewriter::rewrite(right); Node lem = nm->mkNode(EQUAL, left, right); Trace("seq-array-debug") << "enter" << std::endl; sendInference(exp, lem, InferenceId::STRINGS_ARRAY_NTH_UPDATE); diff --git a/src/theory/strings/base_solver.cpp b/src/theory/strings/base_solver.cpp index 2d25a0d1e..f5864bdd3 100644 --- a/src/theory/strings/base_solver.cpp +++ b/src/theory/strings/base_solver.cpp @@ -32,8 +32,11 @@ namespace cvc5 { namespace theory { namespace strings { -BaseSolver::BaseSolver(Env& env, SolverState& s, InferenceManager& im) - : EnvObj(env), d_state(s), d_im(im), d_congruent(context()) +BaseSolver::BaseSolver(Env& env, + SolverState& s, + InferenceManager& im, + TermRegistry& tr) + : EnvObj(env), d_state(s), d_im(im), d_termReg(tr), d_congruent(context()) { d_false = NodeManager::currentNM()->mkConst(false); d_cardSize = options().strings.stringsAlphaCard; @@ -344,7 +347,7 @@ void BaseSolver::checkConstantEquivalenceClasses(TermIndex* ti, Node c; if (isConst) { - c = utils::mkNConcat(vecc, n.getType()); + c = d_termReg.mkNConcat(vecc, n.getType()); } if (!isConst || !d_state.areEqual(n, c)) { @@ -421,7 +424,7 @@ void BaseSolver::checkConstantEquivalenceClasses(TermIndex* ti, { // The equivalence class is not entailed to be equal to a constant // and we found a better concatenation - Node nct = utils::mkNConcat(vecnc, n.getType()); + Node nct = d_termReg.mkNConcat(vecnc, n.getType()); Assert(!nct.isConst()); bei.d_bestContent = nct; bei.d_bestScore = contentSize; diff --git a/src/theory/strings/base_solver.h b/src/theory/strings/base_solver.h index 96d275cd5..d4b0ebe0d 100644 --- a/src/theory/strings/base_solver.h +++ b/src/theory/strings/base_solver.h @@ -44,7 +44,7 @@ class BaseSolver : protected EnvObj using NodeSet = context::CDHashSet<Node>; public: - BaseSolver(Env& env, SolverState& s, InferenceManager& im); + BaseSolver(Env& env, SolverState& s, InferenceManager& im, TermRegistry& tr); ~BaseSolver(); //-----------------------inference steps @@ -217,6 +217,8 @@ class BaseSolver : protected EnvObj SolverState& d_state; /** The (custom) output channel of the theory of strings */ InferenceManager& d_im; + /** Reference to the term registry of theory of strings */ + TermRegistry& d_termReg; /** Commonly used constants */ Node d_emptyString; Node d_false; diff --git a/src/theory/strings/core_solver.cpp b/src/theory/strings/core_solver.cpp index ab214c9ce..868e855ab 100644 --- a/src/theory/strings/core_solver.cpp +++ b/src/theory/strings/core_solver.cpp @@ -562,7 +562,7 @@ void CoreSolver::checkNormalFormsEq() return; } NormalForm& nfe = getNormalForm(eqc); - Node nf_term = utils::mkNConcat(nfe.d_nf, stype); + Node nf_term = d_termReg.mkNConcat(nfe.d_nf, stype); std::map<Node, Node>::iterator itn = nf_to_eqc.find(nf_term); if (itn != nf_to_eqc.end()) { @@ -690,7 +690,7 @@ Node CoreSolver::getNormalString(Node x, std::vector<Node>& nf_exp) if (it != d_normal_form.end()) { NormalForm& nf = it->second; - Node ret = utils::mkNConcat(nf.d_nf, stype); + Node ret = d_termReg.mkNConcat(nf.d_nf, stype); nf_exp.insert(nf_exp.end(), nf.d_exp.begin(), nf.d_exp.end()); d_im.addToExplanation(x, nf.d_base, nf_exp); Trace("strings-debug") @@ -708,7 +708,7 @@ Node CoreSolver::getNormalString(Node x, std::vector<Node>& nf_exp) Node nc = getNormalString(x[i], nf_exp); vec_nodes.push_back(nc); } - return utils::mkNConcat(vec_nodes, stype); + return d_termReg.mkNConcat(vec_nodes, stype); } } return x; @@ -1090,7 +1090,7 @@ void CoreSolver::processNEqc(Node eqc, for (size_t i = 0, nnforms = normal_forms.size(); i < nnforms; i++) { NormalForm& nfi = normal_forms[i]; - Node ni = utils::mkNConcat(nfi.d_nf, stype); + Node ni = d_termReg.mkNConcat(nfi.d_nf, stype); if (nfCache.find(ni) == nfCache.end()) { // If the equivalence class is entailed to be constant, check @@ -1369,7 +1369,7 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi, eqnc.push_back(nfkv[i]); } } - eqn[r] = utils::mkNConcat(eqnc, stype); + eqn[r] = d_termReg.mkNConcat(eqnc, stype); } Trace("strings-solve-debug") << "Endpoint eq check: " << eqn[0] << " " << eqn[1] << std::endl; @@ -1805,15 +1805,15 @@ CoreSolver::ProcessLoopResult CoreSolver::processLoop(NormalForm& nfi, Trace("strings-loop") << " ... (X)= " << vecoi[index] << std::endl; Trace("strings-loop") << " ... T(Y.Z)= "; std::vector<Node> vec_t(veci.begin() + index, veci.begin() + loop_index); - Node t_yz = utils::mkNConcat(vec_t, stype); + Node t_yz = d_termReg.mkNConcat(vec_t, stype); Trace("strings-loop") << " (" << t_yz << ")" << std::endl; Trace("strings-loop") << " ... S(Z.Y)= "; std::vector<Node> vec_s(vecoi.begin() + index + 1, vecoi.end()); - Node s_zy = utils::mkNConcat(vec_s, stype); + Node s_zy = d_termReg.mkNConcat(vec_s, stype); Trace("strings-loop") << s_zy << std::endl; Trace("strings-loop") << " ... R= "; std::vector<Node> vec_r(veci.begin() + loop_index + 1, veci.end()); - Node r = utils::mkNConcat(vec_r, stype); + Node r = d_termReg.mkNConcat(vec_r, stype); Trace("strings-loop") << r << std::endl; Node emp = Word::mkEmptyWord(stype); @@ -1907,12 +1907,12 @@ CoreSolver::ProcessLoopResult CoreSolver::processLoop(NormalForm& nfi, std::vector<Node> v2(vec_r); v2.insert(v2.begin(), y); v2.insert(v2.begin(), z); - restr = utils::mkNConcat(z, y); - cc = rewrite(s_zy.eqNode(utils::mkNConcat(v2, stype))); + restr = d_termReg.mkNConcat(z, y); + cc = rewrite(s_zy.eqNode(d_termReg.mkNConcat(v2, stype))); } else { - cc = rewrite(s_zy.eqNode(utils::mkNConcat(z, y))); + cc = rewrite(s_zy.eqNode(d_termReg.mkNConcat(z, y))); } if (cc == d_false) { @@ -1955,13 +1955,13 @@ CoreSolver::ProcessLoopResult CoreSolver::processLoop(NormalForm& nfi, iinfo.d_skolems[LENGTH_GEQ_ONE].push_back(sk_y); Node sk_z = skc->mkSkolem("z_loop"); // t1 * ... * tn = y * z - Node conc1 = t_yz.eqNode(utils::mkNConcat(sk_y, sk_z)); + Node conc1 = t_yz.eqNode(d_termReg.mkNConcat(sk_y, sk_z)); // s1 * ... * sk = z * y * r vec_r.insert(vec_r.begin(), sk_y); vec_r.insert(vec_r.begin(), sk_z); - Node conc2 = s_zy.eqNode(utils::mkNConcat(vec_r, stype)); - Node conc3 = vecoi[index].eqNode(utils::mkNConcat(sk_y, sk_w)); - Node restr = r == emp ? s_zy : utils::mkNConcat(sk_z, sk_y); + Node conc2 = s_zy.eqNode(d_termReg.mkNConcat(vec_r, stype)); + Node conc3 = vecoi[index].eqNode(d_termReg.mkNConcat(sk_y, sk_w)); + Node restr = r == emp ? s_zy : d_termReg.mkNConcat(sk_z, sk_y); str_in_re = nm->mkNode(kind::STRING_IN_REGEXP, sk_w, @@ -2653,7 +2653,7 @@ void CoreSolver::checkLengthsEqc() { // now, check if length normalization has occurred if (ei->d_normalizedLength.get().isNull()) { - Node nf = utils::mkNConcat(nfi.d_nf, stype); + Node nf = d_termReg.mkNConcat(nfi.d_nf, stype); if (Trace.isOn("strings-process-debug")) { Trace("strings-process-debug") diff --git a/src/theory/strings/regexp_elim.cpp b/src/theory/strings/regexp_elim.cpp index 477533bee..a638d6009 100644 --- a/src/theory/strings/regexp_elim.cpp +++ b/src/theory/strings/regexp_elim.cpp @@ -21,6 +21,7 @@ #include "theory/rewriter.h" #include "theory/strings/regexp_entail.h" #include "theory/strings/theory_strings_utils.h" +#include "theory/strings/word.h" #include "util/rational.h" #include "util/string.h" @@ -173,7 +174,6 @@ Node RegExpElimination::eliminateConcat(Node atom, bool isAgg) conc.push_back(currMem); } currEnd = nm->mkNode(PLUS, currEnd, childLengths[i]); - currEnd = Rewriter::rewrite(currEnd); } } Node res = nm->mkNode(AND, conc); @@ -560,7 +560,6 @@ Node RegExpElimination::eliminateStar(Node atom, bool isAgg) Node index = bvm->mkBoundVar<ReElimStarIndexAttribute>(atom, intType); Node substr_ch = nm->mkNode(STRING_SUBSTR, x, index, nm->mkConstInt(Rational(1))); - substr_ch = Rewriter::rewrite(substr_ch); // handle the case where it is purely characters for (const Node& r : disj) { @@ -588,8 +587,6 @@ Node RegExpElimination::eliminateStar(Node atom, bool isAgg) else { Node regexp_ch = nm->mkNode(STRING_IN_REGEXP, substr_ch, r); - regexp_ch = Rewriter::rewrite(regexp_ch); - Assert(regexp_ch.getKind() != STRING_IN_REGEXP); char_constraints.push_back(regexp_ch); } } @@ -617,9 +614,7 @@ Node RegExpElimination::eliminateStar(Node atom, bool isAgg) Node s = r[0]; if (s.isConst()) { - Node lens = nm->mkNode(STRING_LENGTH, s); - lens = Rewriter::rewrite(lens); - Assert(lens.isConst()); + Node lens = nm->mkConstInt(Word::getLength(s)); Assert(lens.getConst<Rational>().sgn() > 0); std::vector<Node> conj; // lens is a positive constant, so it is safe to use total div/mod here. diff --git a/src/theory/strings/regexp_entail.cpp b/src/theory/strings/regexp_entail.cpp index aa69f9ecf..c2ee079db 100644 --- a/src/theory/strings/regexp_entail.cpp +++ b/src/theory/strings/regexp_entail.cpp @@ -28,7 +28,7 @@ namespace cvc5 { namespace theory { namespace strings { -RegExpEntail::RegExpEntail(Rewriter* r) : d_rewriter(r), d_aent(r) +RegExpEntail::RegExpEntail(Rewriter* r) : d_aent(r) { d_zero = NodeManager::currentNM()->mkConstInt(Rational(0)); d_one = NodeManager::currentNM()->mkConstInt(Rational(1)); @@ -659,11 +659,9 @@ Node RegExpEntail::getFixedLengthForRegexp(TNode n) Kind k = n.getKind(); if (k == STRING_TO_REGEXP) { - Node ret = nm->mkNode(STRING_LENGTH, n[0]); - ret = Rewriter::rewrite(ret); - if (ret.isConst()) + if (n[0].isConst()) { - return ret; + return nm->mkConstInt(Rational(Word::getLength(n[0]))); } } else if (k == REGEXP_ALLCHAR || k == REGEXP_RANGE) @@ -690,7 +688,7 @@ Node RegExpEntail::getFixedLengthForRegexp(TNode n) } else if (k == REGEXP_CONCAT) { - NodeBuilder nb(PLUS); + Rational sum(0); for (const Node& nc : n) { Node flc = getFixedLengthForRegexp(nc); @@ -698,11 +696,10 @@ Node RegExpEntail::getFixedLengthForRegexp(TNode n) { return flc; } - nb << flc; + Assert(flc.isConst() && flc.getType().isInteger()); + sum += flc.getConst<Rational>(); } - Node ret = nb.constructNode(); - ret = Rewriter::rewrite(ret); - return ret; + return nm->mkConstInt(sum); } return Node::null(); } @@ -785,8 +782,6 @@ Node RegExpEntail::getConstantBoundLengthForRegexp(TNode n, bool isLower) const bool RegExpEntail::regExpIncludes(Node r1, Node r2) { - Assert(Rewriter::rewrite(r1) == r1); - Assert(Rewriter::rewrite(r2) == r2); if (r1 == r2) { return true; diff --git a/src/theory/strings/regexp_entail.h b/src/theory/strings/regexp_entail.h index b0511bd53..62cb5a725 100644 --- a/src/theory/strings/regexp_entail.h +++ b/src/theory/strings/regexp_entail.h @@ -146,8 +146,6 @@ class RegExpEntail * computed. Used for getConstantBoundLengthForRegexp. */ static bool getConstantBoundCache(TNode n, bool isLower, Node& c); - /** The underlying rewriter */ - Rewriter* d_rewriter; /** Arithmetic entailment module */ ArithEntail d_aent; /** Common constants */ diff --git a/src/theory/strings/regexp_solver.cpp b/src/theory/strings/regexp_solver.cpp index 24ce64842..9a13aeab3 100644 --- a/src/theory/strings/regexp_solver.cpp +++ b/src/theory/strings/regexp_solver.cpp @@ -115,7 +115,7 @@ bool RegExpSolver::checkInclInter( std::vector<Node> mems2 = mr.second; Trace("regexp-process") << "Memberships(" << mr.first << ") = " << mr.second << std::endl; - if (!checkEqcInclusion(mems2)) + if (options().strings.stringRegexpInclusion && !checkEqcInclusion(mems2)) { // conflict discovered, return return true; diff --git a/src/theory/strings/sequences_rewriter.cpp b/src/theory/strings/sequences_rewriter.cpp index 634f27294..aadca9904 100644 --- a/src/theory/strings/sequences_rewriter.cpp +++ b/src/theory/strings/sequences_rewriter.cpp @@ -40,6 +40,7 @@ namespace strings { SequencesRewriter::SequencesRewriter(Rewriter* r, HistogramStat<Rewrite>* statistics) : d_statistics(statistics), + d_rr(r), d_arithEntail(r), d_stringsEntail(r, d_arithEntail, *this) { @@ -135,7 +136,7 @@ Node SequencesRewriter::rewriteStrEqualityExt(Node node) Node len0 = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, node[0]); Node len1 = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, node[1]); Node len_eq = len0.eqNode(len1); - len_eq = Rewriter::rewrite(len_eq); + len_eq = d_rr->rewrite(len_eq); if (len_eq.isConst() && !len_eq.getConst<bool>()) { return returnRewrite(node, len_eq, Rewrite::EQ_LEN_DEQ); @@ -406,7 +407,7 @@ Node SequencesRewriter::rewriteStrEqualityExt(Node node) // (= x (str.replace x "A" "B")) ---> (not (str.contains x "A")) if (x == repl[0]) { - Node eq = Rewriter::rewrite(nm->mkNode(EQUAL, repl[1], repl[2])); + Node eq = rewriteEquality(nm->mkNode(EQUAL, repl[1], repl[2])); if (eq.isConst() && !eq.getConst<bool>()) { Node ret = nm->mkNode(NOT, nm->mkNode(STRING_CONTAINS, x, repl[1])); @@ -614,9 +615,9 @@ Node SequencesRewriter::rewriteLength(Node node) } else if (nk0 == STRING_REPLACE || nk0 == STRING_REPLACE_ALL) { - Node len1 = Rewriter::rewrite(nm->mkNode(STRING_LENGTH, node[0][1])); - Node len2 = Rewriter::rewrite(nm->mkNode(STRING_LENGTH, node[0][2])); - if (len1 == len2) + Node len1 = nm->mkNode(STRING_LENGTH, node[0][1]); + Node len2 = nm->mkNode(STRING_LENGTH, node[0][2]); + if (d_arithEntail.checkEq(len1, len2)) { // len( y ) == len( z ) => len( str.replace( x, y, z ) ) ---> len( x ) Node retNode = nm->mkNode(STRING_LENGTH, node[0][0]); @@ -2555,7 +2556,7 @@ Node SequencesRewriter::rewriteIndexof(Node node) if (!node[2].isConst() || node[2].getConst<Rational>().sgn() != 0) { fstr = nm->mkNode(kind::STRING_SUBSTR, node[0], node[2], len0); - fstr = Rewriter::rewrite(fstr); + fstr = d_rr->rewrite(fstr); } Node cmp_conr = d_stringsEntail.checkContains(fstr, node[1]); @@ -2801,8 +2802,8 @@ Node SequencesRewriter::rewriteReplace(Node node) if (d_stringsEntail.checkLengthOne(node[0])) { Node empty = Word::mkEmptyWord(stype); - Node rn1 = Rewriter::rewrite( - rewriteEqualityExt(nm->mkNode(EQUAL, node[1], empty))); + Node rn1 = + d_rr->rewrite(rewriteEqualityExt(nm->mkNode(EQUAL, node[1], empty))); if (rn1 != node[1]) { std::vector<Node> emptyNodes; @@ -2827,7 +2828,7 @@ Node SequencesRewriter::rewriteReplace(Node node) // check if contains definitely does (or does not) hold Node cmp_con = nm->mkNode(kind::STRING_CONTAINS, node[0], node[1]); - Node cmp_conr = Rewriter::rewrite(cmp_con); + Node cmp_conr = d_rr->rewrite(cmp_con); if (cmp_conr.isConst()) { if (cmp_conr.getConst<bool>()) @@ -3033,8 +3034,7 @@ Node SequencesRewriter::rewriteReplace(Node node) if (d_arithEntail.check(wlen, zlen)) { // w != z - Node wEqZ = Rewriter::rewrite(nm->mkNode(kind::EQUAL, w, z)); - if (wEqZ.isConst() && !wEqZ.getConst<bool>()) + if (w != z && w.isConst() && z.isConst()) { Node ret = nm->mkNode(kind::STRING_REPLACE, nm->mkNode(kind::STRING_REPLACE, y, w, z), @@ -3346,7 +3346,7 @@ Node SequencesRewriter::rewriteReplaceReAll(Node node) // "Z" ++ y ++ "Z" ++ y TypeNode t = x.getType(); Node emp = Word::mkEmptyWord(t); - Node yp = Rewriter::rewrite( + Node yp = d_rr->rewrite( nm->mkNode(REGEXP_DIFF, y, nm->mkNode(STRING_TO_REGEXP, emp))); std::vector<Node> res; String rem = x.getConst<String>(); @@ -3524,7 +3524,7 @@ Node SequencesRewriter::rewritePrefixSuffix(Node n) Node SequencesRewriter::lengthPreserveRewrite(Node n) { NodeManager* nm = NodeManager::currentNM(); - Node len = Rewriter::rewrite(nm->mkNode(kind::STRING_LENGTH, n)); + Node len = d_rr->rewrite(nm->mkNode(kind::STRING_LENGTH, n)); Node res = canonicalStrForSymbolicLength(len, n.getType()); return res.isNull() ? n : res; } diff --git a/src/theory/strings/sequences_rewriter.h b/src/theory/strings/sequences_rewriter.h index 854e3fb81..850acfb2a 100644 --- a/src/theory/strings/sequences_rewriter.h +++ b/src/theory/strings/sequences_rewriter.h @@ -284,7 +284,7 @@ class SequencesRewriter : public TheoryRewriter * We apply certain normalizations to n', such as replacing all constants * that are not relevant to length by "A". */ - static Node lengthPreserveRewrite(Node n); + Node lengthPreserveRewrite(Node n); /** * Given a symbolic length n, returns the canonical string (of type stype) @@ -305,6 +305,11 @@ class SequencesRewriter : public TheoryRewriter Node postProcessRewrite(Node node, Node ret); /** Reference to the rewriter statistics. */ HistogramStat<Rewrite>* d_statistics; + /** + * Pointer to the rewriter. NOTE this is a cyclic dependency, and should + * be removed. + */ + Rewriter* d_rr; /** The arithmetic entailment module */ ArithEntail d_arithEntail; /** Instance of the entailment checker for strings. */ diff --git a/src/theory/strings/solver_state.cpp b/src/theory/strings/solver_state.cpp index 6b7fc699b..96e143244 100644 --- a/src/theory/strings/solver_state.cpp +++ b/src/theory/strings/solver_state.cpp @@ -77,7 +77,8 @@ TheoryModel* SolverState::getModel() { return d_valuation.getModel(); } Node SolverState::getLengthExp(Node t, std::vector<Node>& exp, Node te) { Assert(areEqual(t, te)); - Node lt = utils::mkNLength(te); + Node lt = NodeManager::currentNM()->mkNode(STRING_LENGTH, t); + lt = rewrite(lt); if (hasTerm(lt)) { // use own length if it exists, leads to shorter explanation @@ -116,7 +117,8 @@ Node SolverState::explainNonEmpty(Node s) { return s.eqNode(emp).negate(); } - Node sLen = utils::mkNLength(s); + Node sLen = NodeManager::currentNM()->mkNode(STRING_LENGTH, s); + sLen = rewrite(sLen); if (areDisequal(sLen, d_zero)) { return sLen.eqNode(d_zero).negate(); diff --git a/src/theory/strings/term_registry.cpp b/src/theory/strings/term_registry.cpp index d2d723276..85ec680ac 100644 --- a/src/theory/strings/term_registry.cpp +++ b/src/theory/strings/term_registry.cpp @@ -81,7 +81,8 @@ Node TermRegistry::eagerReduce(Node t, SkolemCache* sc, uint32_t alphaCard) if (tk == STRING_TO_CODE) { // ite( str.len(s)==1, 0 <= str.code(s) < |A|, str.code(s)=-1 ) - Node code_len = utils::mkNLength(t[0]).eqNode(nm->mkConstInt(Rational(1))); + Node len = nm->mkNode(STRING_LENGTH, t[0]); + Node code_len = len.eqNode(nm->mkConstInt(Rational(1))); Node code_eq_neg1 = t.eqNode(nm->mkConstInt(Rational(-1))); Node code_range = nm->mkNode(AND, @@ -115,7 +116,7 @@ Node TermRegistry::eagerReduce(Node t, SkolemCache* sc, uint32_t alphaCard) sc->mkSkolemCached(t[0], t[1], SkolemCache::SK_FIRST_CTN_PRE, "sc1"); Node sk2 = sc->mkSkolemCached(t[0], t[1], SkolemCache::SK_FIRST_CTN_POST, "sc2"); - lemma = t[0].eqNode(utils::mkNConcat(sk1, t[1], sk2)); + lemma = t[0].eqNode(nm->mkNode(STRING_CONCAT, sk1, t[1], sk2)); lemma = nm->mkNode(ITE, t, lemma, t[0].eqNode(t[1]).notNode()); } return lemma; @@ -669,6 +670,21 @@ void TermRegistry::removeProxyEqs(Node n, std::vector<Node>& unproc) const } } +Node TermRegistry::mkNConcat(Node n1, Node n2) const +{ + return rewrite(NodeManager::currentNM()->mkNode(STRING_CONCAT, n1, n2)); +} + +Node TermRegistry::mkNConcat(Node n1, Node n2, Node n3) const +{ + return rewrite(NodeManager::currentNM()->mkNode(STRING_CONCAT, n1, n2, n3)); +} + +Node TermRegistry::mkNConcat(const std::vector<Node>& c, TypeNode tn) const +{ + return rewrite(utils::mkConcat(c, tn)); +} + } // namespace strings } // namespace theory } // namespace cvc5 diff --git a/src/theory/strings/term_registry.h b/src/theory/strings/term_registry.h index 1de5def9e..338e528fe 100644 --- a/src/theory/strings/term_registry.h +++ b/src/theory/strings/term_registry.h @@ -213,6 +213,22 @@ class TermRegistry : protected EnvObj */ void removeProxyEqs(Node n, std::vector<Node>& unproc) const; //---------------------------- end proxy variables + /** + * Returns the rewritten form of the string concatenation of n1 and n2. + */ + Node mkNConcat(Node n1, Node n2) const; + + /** + * Returns the rewritten form of the string concatenation of n1, n2 and n3. + */ + Node mkNConcat(Node n1, Node n2, Node n3) const; + + /** + * Returns the rewritten form of the concatentation from vector c of + * (string-like) type tn. + */ + Node mkNConcat(const std::vector<Node>& c, TypeNode tn) const; + private: /** Common constants */ Node d_zero; diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 8b496b725..ee068fe16 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -59,13 +59,15 @@ TheoryStrings::TheoryStrings(Env& env, OutputChannel& out, Valuation valuation) d_rewriter(env.getRewriter(), &d_statistics.d_rewrites, d_termReg.getAlphabetCardinality()), - d_eagerSolver(env, d_state, d_termReg), + d_eagerSolver(options().strings.stringEagerSolver + ? new EagerSolver(env, d_state, d_termReg) + : nullptr), d_extTheoryCb(), d_im(env, *this, d_state, d_termReg, d_extTheory, d_statistics), d_extTheory(env, d_extTheoryCb, d_im), // the checker depends on the cardinality of the alphabet d_checker(d_termReg.getAlphabetCardinality()), - d_bsolver(env, d_state, d_im), + d_bsolver(env, d_state, d_im, d_termReg), d_csolver(env, d_state, d_im, d_termReg, d_bsolver), d_esolver(env, d_state, @@ -588,7 +590,7 @@ bool TheoryStrings::collectModelInfoType( Assert(r.isConst() || processed.find(r) != processed.end()); nc.push_back(r.isConst() ? r : processed[r]); } - Node cc = utils::mkNConcat(nc, tn); + Node cc = d_termReg.mkNConcat(nc, tn); Trace("strings-model") << "*** Determined constant " << cc << " for " << rn << std::endl; processed[rn] = cc; @@ -651,7 +653,10 @@ void TheoryStrings::notifyFact(TNode atom, TNode fact, bool isInternal) { - d_eagerSolver.notifyFact(atom, polarity, fact, isInternal); + if (d_eagerSolver) + { + d_eagerSolver->notifyFact(atom, polarity, fact, isInternal); + } // process pending conflicts due to reasoning about endpoints if (!d_state.isInConflict() && d_state.hasPendingConflict()) { @@ -769,7 +774,10 @@ void TheoryStrings::eqNotifyNewClass(TNode t){ ei->d_codeTerm = t[0]; } } - d_eagerSolver.eqNotifyNewClass(t); + if (d_eagerSolver) + { + d_eagerSolver->eqNotifyNewClass(t); + } } void TheoryStrings::eqNotifyMerge(TNode t1, TNode t2) @@ -782,7 +790,10 @@ void TheoryStrings::eqNotifyMerge(TNode t1, TNode t2) // always create it if e2 was non-null EqcInfo* e1 = d_state.getOrMakeEqcInfo(t1); - d_eagerSolver.eqNotifyMerge(e1, t1, e2, t2); + if (d_eagerSolver) + { + d_eagerSolver->eqNotifyMerge(e1, t1, e2, t2); + } // add information from e2 to e1 if (!e2->d_lengthTerm.get().isNull()) @@ -1046,7 +1057,7 @@ void TheoryStrings::checkRegisterTermsNormalForms() Node lt = ei ? ei->d_lengthTerm : Node::null(); if (lt.isNull()) { - Node c = utils::mkNConcat(nfi.d_nf, eqc.getType()); + Node c = d_termReg.mkNConcat(nfi.d_nf, eqc.getType()); d_termReg.registerTerm(c, 3); } } diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index 21db7da0c..dd15e08ec 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -259,7 +259,7 @@ class TheoryStrings : public Theory { /** The theory rewriter for this theory. */ StringsRewriter d_rewriter; /** The eager solver */ - EagerSolver d_eagerSolver; + std::unique_ptr<EagerSolver> d_eagerSolver; /** The extended theory callback */ StringsExtfCallback d_extTheoryCb; /** The (custom) output channel of the theory of strings */ diff --git a/src/theory/strings/theory_strings_utils.cpp b/src/theory/strings/theory_strings_utils.cpp index 0ee2e906d..abac46d37 100644 --- a/src/theory/strings/theory_strings_utils.cpp +++ b/src/theory/strings/theory_strings_utils.cpp @@ -140,28 +140,6 @@ Node mkConcat(const std::vector<Node>& c, TypeNode tn) return NodeManager::currentNM()->mkNode(k, c); } -Node mkNConcat(Node n1, Node n2) -{ - return Rewriter::rewrite( - NodeManager::currentNM()->mkNode(STRING_CONCAT, n1, n2)); -} - -Node mkNConcat(Node n1, Node n2, Node n3) -{ - return Rewriter::rewrite( - NodeManager::currentNM()->mkNode(STRING_CONCAT, n1, n2, n3)); -} - -Node mkNConcat(const std::vector<Node>& c, TypeNode tn) -{ - return Rewriter::rewrite(mkConcat(c, tn)); -} - -Node mkNLength(Node t) -{ - return Rewriter::rewrite(NodeManager::currentNM()->mkNode(STRING_LENGTH, t)); -} - Node mkPrefix(Node t, Node n) { NodeManager* nm = NodeManager::currentNM(); diff --git a/src/theory/strings/theory_strings_utils.h b/src/theory/strings/theory_strings_utils.h index 0cfcd64d0..f97391df8 100644 --- a/src/theory/strings/theory_strings_utils.h +++ b/src/theory/strings/theory_strings_utils.h @@ -61,27 +61,6 @@ void getConcat(Node n, std::vector<Node>& c); Node mkConcat(const std::vector<Node>& c, TypeNode tn); /** - * Returns the rewritten form of the string concatenation of n1 and n2. - */ -Node mkNConcat(Node n1, Node n2); - -/** - * Returns the rewritten form of the string concatenation of n1, n2 and n3. - */ -Node mkNConcat(Node n1, Node n2, Node n3); - -/** - * Returns the rewritten form of the concatentation from vector c of - * (string-like) type tn. - */ -Node mkNConcat(const std::vector<Node>& c, TypeNode tn); - -/** - * Returns the rewritten form of the length of string term t. - */ -Node mkNLength(Node t); - -/** * Returns (pre t n), which is (str.substr t 0 n). */ Node mkPrefix(Node t, Node n); |