From 9523b4248da9764fa14f078659b42085a7fe2654 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 26 Mar 2020 08:37:13 -0500 Subject: [PATCH] Generalize more string-specific functions (#4152) Towards theory of sequences. Note this PR also changes design in core/base solver. Previously I had estimated that we should have separate instances per type for these solvers, but I think it is better to have these classes handle all string-like types simultaneously. This means they should not have a d_type field. --- src/theory/strings/base_solver.cpp | 3 +- src/theory/strings/base_solver.h | 2 - src/theory/strings/core_solver.cpp | 196 +++++++++++--------- src/theory/strings/core_solver.h | 21 ++- src/theory/strings/eqc_info.cpp | 15 +- src/theory/strings/normal_form.cpp | 3 +- src/theory/strings/theory_strings_utils.cpp | 7 +- 7 files changed, 135 insertions(+), 112 deletions(-) diff --git a/src/theory/strings/base_solver.cpp b/src/theory/strings/base_solver.cpp index 128893cf0..af0e7cc37 100644 --- a/src/theory/strings/base_solver.cpp +++ b/src/theory/strings/base_solver.cpp @@ -35,7 +35,6 @@ BaseSolver::BaseSolver(context::Context* c, d_emptyString = NodeManager::currentNM()->mkConst(::CVC4::String("")); d_false = NodeManager::currentNM()->mkConst(false); d_cardSize = utils::getAlphabetCardinality(); - d_type = NodeManager::currentNM()->stringType(); } BaseSolver::~BaseSolver() {} @@ -254,7 +253,7 @@ void BaseSolver::checkConstantEquivalenceClasses(TermIndex* ti, if (!n.isNull()) { // construct the constant - Node c = utils::mkNConcat(vecc, d_type); + Node c = utils::mkNConcat(vecc, n.getType()); if (!d_state.areEqual(n, c)) { if (Trace.isOn("strings-debug")) diff --git a/src/theory/strings/base_solver.h b/src/theory/strings/base_solver.h index bf223bc0a..3681b49a4 100644 --- a/src/theory/strings/base_solver.h +++ b/src/theory/strings/base_solver.h @@ -191,8 +191,6 @@ class BaseSolver std::map d_termIndex; /** the cardinality of the alphabet */ uint32_t d_cardSize; - /** The string-like type for this base solver */ - TypeNode d_type; }; /* class BaseSolver */ } // namespace strings diff --git a/src/theory/strings/core_solver.cpp b/src/theory/strings/core_solver.cpp index 876984503..ab3270016 100644 --- a/src/theory/strings/core_solver.cpp +++ b/src/theory/strings/core_solver.cpp @@ -37,10 +37,8 @@ d_nf_pairs(c) d_zero = NodeManager::currentNM()->mkConst( Rational( 0 ) ); d_one = NodeManager::currentNM()->mkConst( Rational( 1 ) ); d_neg_one = NodeManager::currentNM()->mkConst(Rational(-1)); - d_emptyString = Word::mkEmptyWord(CONST_STRING); d_true = NodeManager::currentNM()->mkConst( true ); d_false = NodeManager::currentNM()->mkConst( false ); - d_type = NodeManager::currentNM()->stringType(); } CoreSolver::~CoreSolver() { @@ -286,10 +284,11 @@ void CoreSolver::checkFlatForm(std::vector& eqc, << "Found endpoint (in a) with non-empty b = " << b << ", whose flat form is " << d_flat_form[b] << std::endl; // endpoint + Node emp = Word::mkEmptyWord(a.getType()); std::vector conc_c; for (unsigned j = count; j < bsize; j++) { - conc_c.push_back(b[d_flat_form_index[b][j]].eqNode(d_emptyString)); + conc_c.push_back(b[d_flat_form_index[b][j]].eqNode(emp)); } Assert(!conc_c.empty()); conc = utils::mkAnd(conc_c); @@ -325,10 +324,11 @@ void CoreSolver::checkFlatForm(std::vector& eqc, << "Found endpoint in b = " << b << ", whose flat form is " << d_flat_form[b] << std::endl; // endpoint + Node emp = Word::mkEmptyWord(a.getType()); std::vector conc_c; for (size_t j = count; j < asize; j++) { - conc_c.push_back(a[d_flat_form_index[a][j]].eqNode(d_emptyString)); + conc_c.push_back(a[d_flat_form_index[a][j]].eqNode(emp)); } Assert(!conc_c.empty()); conc = utils::mkAnd(conc_c); @@ -438,11 +438,12 @@ void CoreSolver::checkFlatForm(std::vector& eqc, } ssize_t startj = isRev ? jj + 1 : 0; ssize_t endj = isRev ? c.getNumChildren() : jj; + Node emp = Word::mkEmptyWord(a.getType()); for (ssize_t j = startj; j < endj; j++) { - if (d_state.areEqual(c[j], d_emptyString)) + if (d_state.areEqual(c[j], emp)) { - d_im.addToExplanation(c[j], d_emptyString, exp); + d_im.addToExplanation(c[j], emp, exp); } } } @@ -470,6 +471,7 @@ Node CoreSolver::checkCycles( Node eqc, std::vector< Node >& curr, std::vector< return eqc; }else if( std::find( d_strings_eqc.begin(), d_strings_eqc.end(), eqc )==d_strings_eqc.end() ){ curr.push_back( eqc ); + Node emp = Word::mkEmptyWord(eqc.getType()); //look at all terms in this equivalence class eq::EqualityEngine* ee = d_state.getEqualityEngine(); eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, ee ); @@ -478,22 +480,25 @@ Node CoreSolver::checkCycles( Node eqc, std::vector< Node >& curr, std::vector< if( !d_bsolver.isCongruent(n) ){ if( n.getKind() == kind::STRING_CONCAT ){ Trace("strings-cycle") << eqc << " check term : " << n << " in " << eqc << std::endl; - if( eqc!=d_emptyString ){ + if (eqc != emp) + { d_eqc[eqc].push_back( n ); } for( unsigned i=0; i exps; - exps.push_back(n.eqNode(d_emptyString)); - d_im.sendInference( - exps, n[i].eqNode(d_emptyString), "I_CYCLE_E"); + exps.push_back(n.eqNode(emp)); + d_im.sendInference(exps, n[i].eqNode(emp), "I_CYCLE_E"); return Node::null(); } }else{ - if( nr!=d_emptyString ){ + if (nr != emp) + { d_flat_form[n].push_back( nr ); d_flat_form_index[n].push_back( i ); } @@ -507,10 +512,9 @@ Node CoreSolver::checkCycles( Node eqc, std::vector< Node >& curr, std::vector< //can infer all other components must be empty for( unsigned j=0; j eqc_to_exp; for (const Node& eqc : d_strings_eqc) { + TypeNode stype = eqc.getType(); Trace("strings-process-debug") << "- Verify normal forms are the same for " << eqc << std::endl; - normalizeEquivalenceClass(eqc); + normalizeEquivalenceClass(eqc, stype); Trace("strings-debug") << "Finished normalizing eqc..." << std::endl; if (d_im.hasProcessed()) { return; } NormalForm& nfe = getNormalForm(eqc); - Node nf_term = utils::mkNConcat(nfe.d_nf, d_type); + Node nf_term = utils::mkNConcat(nfe.d_nf, stype); std::map::iterator itn = nf_to_eqc.find(nf_term); if (itn != nf_to_eqc.end()) { @@ -602,21 +607,23 @@ void CoreSolver::checkNormalFormsEq() } //compute d_normal_forms_(base,exp,exp_depend)[eqc] -void CoreSolver::normalizeEquivalenceClass( Node eqc ) { +void CoreSolver::normalizeEquivalenceClass(Node eqc, TypeNode stype) +{ Trace("strings-process-debug") << "Process equivalence class " << eqc << std::endl; - if (d_state.areEqual(eqc, d_emptyString)) + Node emp = Word::mkEmptyWord(stype); + if (d_state.areEqual(eqc, emp)) { #ifdef CVC4_ASSERTIONS for( unsigned j=0; j term_to_nf_index; // get the normal forms - getNormalForms(eqc, normal_forms, term_to_nf_index); + getNormalForms(eqc, normal_forms, term_to_nf_index, stype); if (d_im.hasProcessed()) { return; } // process the normal forms - processNEqc(normal_forms); + processNEqc(normal_forms, stype); if (d_im.hasProcessed()) { return; @@ -679,11 +686,12 @@ Node CoreSolver::getNormalString(Node x, std::vector& nf_exp) if (!x.isConst()) { Node xr = d_state.getRepresentative(x); + TypeNode stype = xr.getType(); std::map::iterator it = d_normal_form.find(xr); if (it != d_normal_form.end()) { NormalForm& nf = it->second; - Node ret = utils::mkNConcat(nf.d_nf, d_type); + Node ret = utils::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") @@ -701,16 +709,18 @@ Node CoreSolver::getNormalString(Node x, std::vector& nf_exp) Node nc = getNormalString(x[i], nf_exp); vec_nodes.push_back(nc); } - return utils::mkNConcat(vec_nodes, d_type); + return utils::mkNConcat(vec_nodes, stype); } } return x; } void CoreSolver::getNormalForms(Node eqc, - std::vector& normal_forms, - std::map& term_to_nf_index) + std::vector& normal_forms, + std::map& term_to_nf_index, + TypeNode stype) { + Node emp = Word::mkEmptyWord(stype); //constant for equivalence class Node eqc_non_c = eqc; Trace("strings-process-debug") << "Get normal forms " << eqc << std::endl; @@ -826,7 +836,7 @@ void CoreSolver::getNormalForms(Node eqc, normal_forms.push_back(nf_curr); }else{ //this was redundant: combination of self + empty string(s) - Node nn = currv.size() == 0 ? d_emptyString : currv[0]; + Node nn = currv.size() == 0 ? emp : currv[0]; Assert(d_state.areEqual(nn, eqc)); } }else{ @@ -925,7 +935,8 @@ void CoreSolver::getNormalForms(Node eqc, } } -void CoreSolver::processNEqc(std::vector& normal_forms) +void CoreSolver::processNEqc(std::vector& normal_forms, + TypeNode stype) { //the possible inferences std::vector< InferInfo > pinfer; @@ -945,7 +956,7 @@ void CoreSolver::processNEqc(std::vector& normal_forms) unsigned rindex = 0; nfi.reverse(); nfj.reverse(); - processSimpleNEq(nfi, nfj, rindex, true, 0, pinfer); + processSimpleNEq(nfi, nfj, rindex, true, 0, pinfer, stype); nfi.reverse(); nfj.reverse(); if (d_im.hasProcessed()) @@ -956,7 +967,7 @@ void CoreSolver::processNEqc(std::vector& normal_forms) //rindex = 0; unsigned index = 0; - processSimpleNEq(nfi, nfj, index, false, rindex, pinfer); + processSimpleNEq(nfi, nfj, index, false, rindex, pinfer, stype); if (d_im.hasProcessed()) { return; @@ -1000,10 +1011,12 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi, unsigned& index, bool isRev, unsigned rproc, - std::vector& pinfer) + std::vector& pinfer, + TypeNode stype) { NodeManager* nm = NodeManager::currentNM(); eq::EqualityEngine* ee = d_state.getEqualityEngine(); + Node emp = Word::mkEmptyWord(stype); const std::vector& nfiv = nfi.d_nf; const std::vector& nfjv = nfj.d_nf; @@ -1028,8 +1041,8 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi, while (!d_state.isInConflict() && index_k < (nfkv.size() - rproc)) { // can infer that this string must be empty - Node eq = nfkv[index_k].eqNode(d_emptyString); - Assert(!d_state.areEqual(d_emptyString, nfkv[index_k])); + Node eq = nfkv[index_k].eqNode(emp); + Assert(!d_state.areEqual(emp, nfkv[index_k])); d_im.sendInference(curr_exp, eq, Inference::N_ENDPOINT_EMP); index_k++; } @@ -1108,7 +1121,7 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi, eqnc.push_back(nfkv[i]); } } - eqn[r] = utils::mkNConcat(eqnc, d_type); + eqn[r] = utils::mkNConcat(eqnc, stype); } if (!d_state.areEqual(eqn[0], eqn[1])) { @@ -1253,13 +1266,13 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi, Node nc = nfncv[index]; Assert(!nc.isConst()) << "Other string is not constant."; Assert(nc.getKind() != STRING_CONCAT) << "Other string is not CONCAT."; - if (!ee->areDisequal(nc, d_emptyString, true)) + if (!ee->areDisequal(nc, emp, true)) { // The non-constant side may be equal to the empty string. Split on // whether it is. // // E.g. "abc" ++ ... = nc ++ ... ---> (nc = "") v (nc != "") - Node eq = nc.eqNode(d_emptyString); + Node eq = nc.eqNode(emp); eq = Rewriter::rewrite(eq); if (eq.isConst()) { @@ -1267,7 +1280,7 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi, // purify variable for this string to communicate that // we have inferred whether it is empty. Node p = d_skCache.mkSkolemCached(nc, SkolemCache::SK_PURIFY, "lsym"); - Node pEq = p.eqNode(d_emptyString); + Node pEq = p.eqNode(emp); // should not be constant Assert(!Rewriter::rewrite(pEq).isConst()); // infer the purification equality, and the (dis)equality @@ -1288,7 +1301,7 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi, // At this point, we know that `nc` is non-empty, so we add that to our // explanation. - Node ncnz = nc.eqNode(d_emptyString).negate(); + Node ncnz = nc.eqNode(emp).negate(); info.d_ant.push_back(ncnz); size_t ncIndex = index + 1; @@ -1300,19 +1313,19 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi, // // E.g. "abc" ++ ... = nc ++ "b" ++ ... ---> nc = "a" ++ k size_t cIndex = index; - Node constStr = nfc.collectConstantStringAt(cIndex); - Assert(!constStr.isNull()); - CVC4::String stra = constStr.getConst(); - CVC4::String strb = nextConstStr.getConst(); + Node stra = nfc.collectConstantStringAt(cIndex); + size_t straLen = Word::getLength(stra); + Assert(!stra.isNull()); + Node strb = nextConstStr; // Since `nc` is non-empty, we start with character 1 size_t p; if (isRev) { - CVC4::String stra1 = stra.prefix(stra.size() - 1); - p = stra.size() - stra1.roverlap(strb); - Trace("strings-csp-debug") << "Compute roverlap : " << constStr << " " - << nextConstStr << std::endl; - size_t p2 = stra1.rfind(strb); + Node stra1 = Word::prefix(stra, straLen - 1); + p = straLen - Word::roverlap(stra1, strb); + Trace("strings-csp-debug") + << "Compute roverlap : " << stra1 << " " << strb << std::endl; + size_t p2 = Word::rfind(stra1, strb); p = p2 == std::string::npos ? p : (p > p2 + 1 ? p2 + 1 : p); Trace("strings-csp-debug") << "roverlap : " << stra1 << " " << strb << " returned " << p @@ -1320,11 +1333,11 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi, } else { - CVC4::String stra1 = stra.substr(1); - p = stra.size() - stra1.overlap(strb); - Trace("strings-csp-debug") << "Compute overlap : " << constStr << " " - << nextConstStr << std::endl; - size_t p2 = stra1.find(strb); + Node stra1 = Word::substr(stra, 1); + p = straLen - Word::overlap(stra1, strb); + Trace("strings-csp-debug") + << "Compute overlap : " << stra1 << " " << strb << std::endl; + size_t p2 = Word::find(stra1, strb); p = p2 == std::string::npos ? p : (p > p2 + 1 ? p2 + 1 : p); Trace("strings-csp-debug") << "overlap : " << stra1 << " " << strb << " returned " << p @@ -1338,9 +1351,9 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi, { NormalForm::getExplanationForPrefixEq( nfc, nfnc, cIndex, ncIndex, info.d_ant); - Node prea = p == stra.size() ? constStr - : nm->mkConst(isRev ? stra.suffix(p) - : stra.prefix(p)); + Node prea = p == straLen ? stra + : (isRev ? Word::suffix(stra, p) + : Word::prefix(stra, p)); Node sk = d_skCache.mkSkolemCached( nc, prea, @@ -1362,17 +1375,17 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi, // to start with the first character of the constant. // // E.g. "abc" ++ ... = nc ++ ... ---> nc = "a" ++ k - Node constStr = nfcv[index]; - CVC4::String stra = constStr.getConst(); - Node firstChar = stra.size() == 1 ? constStr - : nm->mkConst(isRev ? stra.suffix(1) - : stra.prefix(1)); + Node stra = nfcv[index]; + size_t straLen = Word::getLength(stra); + Node firstChar = straLen == 1 ? stra + : (isRev ? Word::suffix(stra, 1) + : Word::prefix(stra, 1)); Node sk = d_skCache.mkSkolemCached( nc, isRev ? SkolemCache::SK_ID_VC_SPT_REV : SkolemCache::SK_ID_VC_SPT, "c_spt"); Trace("strings-csp") << "Const Split: " << firstChar - << " is removed from " << constStr << " (serial) " + << " is removed from " << stra << " (serial) " << std::endl; NormalForm::getExplanationForPrefixEq(nfi, nfj, index, index, info.d_ant); info.d_conc = nc.eqNode(isRev ? utils::mkNConcat(sk, firstChar) @@ -1429,8 +1442,8 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi, for (unsigned xory = 0; xory < 2; xory++) { Node t = xory == 0 ? x : y; - Node tnz = x.eqNode(d_emptyString).negate(); - if (ee->areDisequal(x, d_emptyString, true)) + Node tnz = x.eqNode(emp).negate(); + if (ee->areDisequal(x, emp, true)) { info.d_ant.push_back(tnz); } @@ -1527,23 +1540,27 @@ CoreSolver::ProcessLoopResult CoreSolver::processLoop(NormalForm& nfi, const std::vector& veci = nfi.d_nf; const std::vector& vecoi = nfj.d_nf; + TypeNode stype = veci[loop_index].getType(); + Trace("strings-loop") << "Detected possible loop for " << veci[loop_index] << std::endl; Trace("strings-loop") << " ... (X)= " << vecoi[index] << std::endl; Trace("strings-loop") << " ... T(Y.Z)= "; std::vector vec_t(veci.begin() + index, veci.begin() + loop_index); - Node t_yz = utils::mkNConcat(vec_t, d_type); + Node t_yz = utils::mkNConcat(vec_t, stype); Trace("strings-loop") << " (" << t_yz << ")" << std::endl; Trace("strings-loop") << " ... S(Z.Y)= "; std::vector vec_s(vecoi.begin() + index + 1, vecoi.end()); - Node s_zy = utils::mkNConcat(vec_s, d_type); + Node s_zy = utils::mkNConcat(vec_s, stype); Trace("strings-loop") << s_zy << std::endl; Trace("strings-loop") << " ... R= "; std::vector vec_r(veci.begin() + loop_index + 1, veci.end()); - Node r = utils::mkNConcat(vec_r, d_type); + Node r = utils::mkNConcat(vec_r, stype); Trace("strings-loop") << r << std::endl; - if (s_zy.isConst() && r.isConst() && r != d_emptyString) + Node emp = Word::mkEmptyWord(stype); + + if (s_zy.isConst() && r.isConst() && r != emp) { int c; bool flag = true; @@ -1551,8 +1568,8 @@ CoreSolver::ProcessLoopResult CoreSolver::processLoop(NormalForm& nfi, { if (c >= 0) { - s_zy = nm->mkConst(s_zy.getConst().substr(0, c)); - r = d_emptyString; + s_zy = Word::substr(s_zy, 0, c); + r = emp; vec_r.clear(); Trace("strings-loop") << "Strings::Loop: Refactor S(Z.Y)= " << s_zy << ", c=" << c << std::endl; @@ -1572,12 +1589,12 @@ CoreSolver::ProcessLoopResult CoreSolver::processLoop(NormalForm& nfi, for (unsigned i = 0; i < 2; i++) { Node t = i == 0 ? veci[loop_index] : t_yz; - split_eq = t.eqNode(d_emptyString); + split_eq = t.eqNode(emp); Node split_eqr = Rewriter::rewrite(split_eq); // the equality could rewrite to false if (!split_eqr.isConst()) { - if (!d_state.areDisequal(t, d_emptyString)) + if (!d_state.areDisequal(t, emp)) { // try to make t equal to empty to avoid loop info.d_conc = nm->mkNode(kind::OR, split_eq, split_eq.negate()); @@ -1600,10 +1617,10 @@ CoreSolver::ProcessLoopResult CoreSolver::processLoop(NormalForm& nfi, info.d_antn.push_back(ant); Node str_in_re; - if (s_zy == t_yz && r == d_emptyString && s_zy.isConst() + if (s_zy == t_yz && r == emp && s_zy.isConst() && s_zy.getConst().isRepeated()) { - Node rep_c = nm->mkConst(s_zy.getConst().substr(0, 1)); + Node rep_c = Word::substr(s_zy, 0, 1); Trace("strings-loop") << "Special case (X)=" << vecoi[index] << " " << std::endl; Trace("strings-loop") << "... (C)=" << rep_c << " " << std::endl; @@ -1626,13 +1643,13 @@ CoreSolver::ProcessLoopResult CoreSolver::processLoop(NormalForm& nfi, Node z = Word::substr(t_yz, len, size - len); Node restr = s_zy; Node cc; - if (r != d_emptyString) + if (r != emp) { std::vector v2(vec_r); v2.insert(v2.begin(), y); v2.insert(v2.begin(), z); restr = utils::mkNConcat(z, y); - cc = Rewriter::rewrite(s_zy.eqNode(utils::mkNConcat(v2, d_type))); + cc = Rewriter::rewrite(s_zy.eqNode(utils::mkNConcat(v2, stype))); } else { @@ -1682,9 +1699,9 @@ CoreSolver::ProcessLoopResult CoreSolver::processLoop(NormalForm& nfi, // 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, d_type)); + Node conc2 = s_zy.eqNode(utils::mkNConcat(vec_r, stype)); Node conc3 = vecoi[index].eqNode(utils::mkNConcat(sk_y, sk_w)); - Node restr = r == d_emptyString ? s_zy : utils::mkNConcat(sk_z, sk_y); + Node restr = r == emp ? s_zy : utils::mkNConcat(sk_z, sk_y); str_in_re = nm->mkNode(kind::STRING_IN_REGEXP, sk_w, @@ -1696,7 +1713,6 @@ CoreSolver::ProcessLoopResult CoreSolver::processLoop(NormalForm& nfi, vec_conc.push_back(conc2); vec_conc.push_back(conc3); vec_conc.push_back(str_in_re); - // vec_conc.push_back(sk_y.eqNode(d_emptyString).negate());//by mkskolems conc = nm->mkNode(kind::AND, vec_conc); } // normal case @@ -1755,8 +1771,10 @@ void CoreSolver::processDeq( Node ni, Node nj ) { Node const_k = i.isConst() ? i : j; Node nconst_k = i.isConst() ? j : i; Node lnck = i.isConst() ? lj : li; - if( !ee->areDisequal( nconst_k, d_emptyString, true ) ){ - Node eq = nconst_k.eqNode( d_emptyString ); + Node emp = Word::mkEmptyWord(nconst_k.getType()); + if (!ee->areDisequal(nconst_k, emp, true)) + { + Node eq = nconst_k.eqNode(emp); Node conc = NodeManager::currentNM()->mkNode( kind::OR, eq, eq.negate() ); d_im.sendInference(d_emptyVec, conc, "D-DISL-Emp-Split"); return; @@ -1798,7 +1816,7 @@ void CoreSolver::processDeq( Node ni, Node nj ) { antec.end(), nfni.d_exp.begin(), nfni.d_exp.end()); antec.insert( antec.end(), nfnj.d_exp.begin(), nfnj.d_exp.end()); - antec.push_back( nconst_k.eqNode( d_emptyString ).negate() ); + antec.push_back(nconst_k.eqNode(emp).negate()); d_im.sendInference( antec, nm->mkNode( @@ -1835,8 +1853,6 @@ void CoreSolver::processDeq( Node ni, Node nj ) { Node sk3 = d_skCache.mkSkolemCached( i, j, SkolemCache::SK_ID_DEQ_Z, "z_dsplit"); d_im.registerLength(sk3, LENGTH_GEQ_ONE); - //Node nemp = sk3.eqNode(d_emptyString).negate(); - //conc.push_back(nemp); Node lsk1 = utils::mkNLength(sk1); conc.push_back( lsk1.eqNode( li ) ); Node lsk2 = utils::mkNLength(sk2); @@ -1912,6 +1928,8 @@ int CoreSolver::processSimpleDeq( std::vector< Node >& nfi, std::vector< Node >& } } } + TypeNode stype = ni.getType(); + Node emp = Word::mkEmptyWord(stype); NormalForm& nfni = getNormalForm(ni); NormalForm& nfnj = getNormalForm(nj); while( index& nfi, std::vector< Node >& std::vector< Node > cc; std::vector< Node >& nfk = index>=nfi.size() ? nfj : nfi; for( unsigned index_k=index; index_kmkNode( kind::AND, cc ); conc = Rewriter::rewrite( conc ); @@ -1944,7 +1962,8 @@ int CoreSolver::processSimpleDeq( std::vector< Node >& nfi, std::vector< Node >& size_t lenI = Word::getLength(i); size_t lenJ = Word::getLength(j); unsigned int len_short = lenI < lenJ ? lenI : lenJ; - bool isSameFix = isRev ? i.getConst().rstrncmp(j.getConst(), len_short): i.getConst().strncmp(j.getConst(), len_short); + bool isSameFix = isRev ? Word::rstrncmp(i, j, len_short) + : Word::strncmp(i, j, len_short); if( isSameFix ) { //same prefix/suffix //k is the index of the string that is shorter @@ -2124,6 +2143,7 @@ void CoreSolver::checkNormalFormsDeq() void CoreSolver::checkLengthsEqc() { for (unsigned i = 0; i < d_strings_eqc.size(); i++) { + TypeNode stype = d_strings_eqc[i].getType(); NormalForm& nfi = getNormalForm(d_strings_eqc[i]); Trace("strings-process-debug") << "Process length constraints for " << d_strings_eqc[i] << std::endl; @@ -2140,7 +2160,7 @@ void CoreSolver::checkLengthsEqc() { // now, check if length normalization has occurred if (ei->d_normalizedLength.get().isNull()) { - Node nf = utils::mkNConcat(nfi.d_nf, d_type); + Node nf = utils::mkNConcat(nfi.d_nf, stype); if (Trace.isOn("strings-process-debug")) { Trace("strings-process-debug") diff --git a/src/theory/strings/core_solver.h b/src/theory/strings/core_solver.h index c549fa886..3fea5e8de 100644 --- a/src/theory/strings/core_solver.h +++ b/src/theory/strings/core_solver.h @@ -218,16 +218,21 @@ class CoreSolver * current normal form for each term in this equivalence class is identical. * If it is not, then we add an inference via sendInference and abort the * call. + * + * stype is the string-like type of the equivalence class we are processing. */ - void normalizeEquivalenceClass(Node n); + void normalizeEquivalenceClass(Node n, TypeNode stype); /** * For each term in the equivalence class of eqc, this adds data regarding its * normal form to normal_forms. The map term_to_nf_index maps terms to the * index in normal_forms where their normal form data is located. + * + * stype is the string-like type of the equivalence class we are processing. */ void getNormalForms(Node eqc, std::vector& normal_forms, - std::map& term_to_nf_index); + std::map& term_to_nf_index, + TypeNode stype); /** process normalize equivalence class * * This is called when an equivalence class contains a set of terms that @@ -240,8 +245,10 @@ class CoreSolver * corresponding to processing the normal form pair in the (forward, reverse) * directions. Once all possible inferences are recorded, it executes the * one with highest priority based on the enumeration type Inference. + * + * stype is the string-like type of the equivalence class we are processing. */ - void processNEqc(std::vector& normal_forms); + void processNEqc(std::vector& normal_forms, TypeNode stype); /** process simple normal equality * * This method is called when two equal terms have normal forms nfi and nfj. @@ -265,13 +272,16 @@ class CoreSolver * fowards/backwards traversals of normal forms to ensure that duplicate * inferences are not processed. * pinfer: the set of possible inferences we add to. + * + * stype is the string-like type of the equivalence class we are processing. */ void processSimpleNEq(NormalForm& nfi, NormalForm& nfj, unsigned& index, bool isRev, unsigned rproc, - std::vector& pinfer); + std::vector& pinfer, + TypeNode stype); //--------------------------end for checkNormalFormsEq //--------------------------for checkNormalFormsEq with loops @@ -325,7 +335,6 @@ class CoreSolver /** reference to the base solver, used for certain queries */ BaseSolver& d_bsolver; /** Commonly used constants */ - Node d_emptyString; Node d_true; Node d_false; Node d_zero; @@ -368,8 +377,6 @@ class CoreSolver * the argument number of the t1 ... tn they were generated from. */ std::map > d_flat_form_index; - /** The string-like type for this solver */ - TypeNode d_type; }; /* class CoreSolver */ } // namespace strings diff --git a/src/theory/strings/eqc_info.cpp b/src/theory/strings/eqc_info.cpp index 4e9b0f8cd..3c0dbc2a7 100644 --- a/src/theory/strings/eqc_info.cpp +++ b/src/theory/strings/eqc_info.cpp @@ -15,6 +15,7 @@ #include "theory/strings/eqc_info.h" #include "theory/strings/theory_strings_utils.h" +#include "theory/strings/word.h" using namespace std; using namespace CVC4::context; @@ -59,10 +60,8 @@ Node EqcInfo::addEndpointConst(Node t, Node c, bool isSuf) Assert(!t.isConst() || !prev.isConst()); Trace("strings-eager-pconf-debug") << "Check conflict constants " << prevC << ", " << c << std::endl; - const String& ps = prevC.getConst(); - const String& cs = c.getConst(); - unsigned pvs = ps.size(); - unsigned cvs = cs.size(); + size_t pvs = Word::getLength(prevC); + size_t cvs = Word::getLength(c); if (pvs == cvs || (pvs > cvs && t.isConst()) || (cvs > pvs && prev.isConst())) { @@ -73,15 +72,15 @@ Node EqcInfo::addEndpointConst(Node t, Node c, bool isSuf) } else { - const String& larges = pvs > cvs ? ps : cs; - const String& smalls = pvs > cvs ? cs : ps; + Node larges = pvs > cvs ? prevC : c; + Node smalls = pvs > cvs ? c : prevC; if (isSuf) { - conflict = !larges.hasSuffix(smalls); + conflict = !Word::hasSuffix(larges, smalls); } else { - conflict = !larges.hasPrefix(smalls); + conflict = !Word::hasPrefix(larges, smalls); } } if (!conflict && (pvs > cvs || prev.isConst())) diff --git a/src/theory/strings/normal_form.cpp b/src/theory/strings/normal_form.cpp index 4dd273eff..05be5f12a 100644 --- a/src/theory/strings/normal_form.cpp +++ b/src/theory/strings/normal_form.cpp @@ -18,6 +18,7 @@ #include "options/strings_options.h" #include "theory/rewriter.h" #include "theory/strings/theory_strings_utils.h" +#include "theory/strings/word.h" using namespace std; using namespace CVC4::kind; @@ -37,7 +38,7 @@ void NormalForm::init(Node base) d_expDep.clear(); // add to normal form - if (!base.isConst() || !base.getConst().isEmptyString()) + if (!base.isConst() || Word::getLength(base) > 0) { d_nf.push_back(base); } diff --git a/src/theory/strings/theory_strings_utils.cpp b/src/theory/strings/theory_strings_utils.cpp index 74cd6c4a3..a3f6f4255 100644 --- a/src/theory/strings/theory_strings_utils.cpp +++ b/src/theory/strings/theory_strings_utils.cpp @@ -232,11 +232,10 @@ void getRegexpComponents(Node r, std::vector& result) } else if (r.getKind() == STRING_TO_REGEXP && r[0].isConst()) { - String s = r[0].getConst(); - for (size_t i = 0, size = s.size(); i < size; i++) + size_t rlen = Word::getLength(r[0]); + for (size_t i = 0; i < rlen; i++) { - result.push_back( - nm->mkNode(STRING_TO_REGEXP, nm->mkConst(s.substr(i, 1)))); + result.push_back(nm->mkNode(STRING_TO_REGEXP, Word::substr(r[0], i, 1))); } } else -- 2.30.2