diff options
| -rw-r--r-- | src/theory/strings/core_solver.cpp | 64 | ||||
| -rw-r--r-- | src/theory/strings/extf_solver.cpp | 61 | ||||
| -rw-r--r-- | src/theory/strings/extf_solver.h | 4 | ||||
| -rw-r--r-- | src/theory/strings/infer_info.cpp | 17 | ||||
| -rw-r--r-- | src/theory/strings/infer_info.h | 17 | ||||
| -rw-r--r-- | src/theory/strings/inference_manager.cpp | 41 | ||||
| -rw-r--r-- | src/theory/strings/inference_manager.h | 48 | ||||
| -rw-r--r-- | src/theory/strings/regexp_solver.cpp | 61 | ||||
| -rw-r--r-- | src/theory/strings/theory_strings.cpp | 12 |
9 files changed, 198 insertions, 127 deletions
diff --git a/src/theory/strings/core_solver.cpp b/src/theory/strings/core_solver.cpp index 438a559b8..371bb020f 100644 --- a/src/theory/strings/core_solver.cpp +++ b/src/theory/strings/core_solver.cpp @@ -440,7 +440,7 @@ void CoreSolver::checkFlatForm(std::vector<Node>& eqc, // is conflicting by arithmetic len(a.b)=len(a)+len(b)!=len(a) // when len(b)!=0. Although if we do not infer this conflict eagerly, // it may be applied (see #3272). - d_im.sendInference(exp, conc, infType); + d_im.sendInference(exp, conc, infType, isRev); if (d_state.isInConflict()) { return; @@ -1269,7 +1269,7 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi, // can infer that this string must be empty 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); + d_im.sendInference(curr_exp, eq, Inference::N_ENDPOINT_EMP, isRev); index_k++; } break; @@ -1312,7 +1312,7 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi, if (x.isConst() && y.isConst()) { // if both are constant, it's just a constant conflict - d_im.sendInference(ant, d_false, Inference::N_CONST, true); + d_im.sendInference(ant, d_false, Inference::N_CONST, isRev, true); return; } // `x` and `y` have the same length. We infer that the two components @@ -1327,7 +1327,7 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi, // set the explanation for length Node lant = utils::mkAnd(lenExp); ant.push_back(lant); - d_im.sendInference(ant, eq, Inference::N_UNIFY); + d_im.sendInference(ant, eq, Inference::N_UNIFY, isRev); break; } else if ((!x.isConst() && index == nfiv.size() - rproc - 1) @@ -1363,8 +1363,11 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi, { std::vector<Node> antec; NormalForm::getExplanationForPrefixEq(nfi, nfj, -1, -1, antec); - d_im.sendInference( - antec, eqn[0].eqNode(eqn[1]), Inference::N_ENDPOINT_EQ, true); + d_im.sendInference(antec, + eqn[0].eqNode(eqn[1]), + Inference::N_ENDPOINT_EQ, + isRev, + true); } else { @@ -1424,7 +1427,7 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi, // E.g. "abc" ++ ... = "bc" ++ ... ---> conflict std::vector<Node> antec; NormalForm::getExplanationForPrefixEq(nfi, nfj, index, index, antec); - d_im.sendInference(antec, d_false, Inference::N_CONST, true); + d_im.sendInference(antec, d_false, Inference::N_CONST, isRev, true); break; } } @@ -1466,8 +1469,11 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi, if (detectLoop(nfi, nfj, index, lhsLoopIdx, rhsLoopIdx, rproc)) { // We are dealing with a looping word equation. + // Note we could make this code also run in the reverse direction, but + // this is not implemented currently. if (!isRev) - { // FIXME + { + // add temporarily to the antecedant of iinfo. NormalForm::getExplanationForPrefixEq(nfi, nfj, -1, -1, iinfo.d_ant); ProcessLoopResult plr = processLoop(lhsLoopIdx != -1 ? nfi : nfj, @@ -1485,6 +1491,8 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi, break; } Assert(plr == ProcessLoopResult::SKIPPED); + // not processing an inference here, undo changes to ant + iinfo.d_ant.clear(); } } @@ -1637,13 +1645,20 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi, << " explanation was : " << et.second << std::endl; lentTestSuccess = e; lenConstraint = entLit; - // its not explained by the equality engine of this class - iinfo.d_antn.push_back(lenConstraint); + // Its not explained by the equality engine of this class, so its + // marked as not being explained. The length constraint is + // additionally being saved and added to the length constraint + // vector lcVec below, which is added to iinfo.d_ant below. Length + // constraints are being added as the last antecedant for the sake + // of proof reconstruction, which expect length constraints to come + // last. + iinfo.d_noExplain.push_back(lenConstraint); break; } } } } + // lcVec stores the length constraint portion of the antecedant. std::vector<Node> lcVec; if (lenConstraint.isNull()) { @@ -1651,6 +1666,10 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi, lenConstraint = nm->mkNode(EQUAL, xLenTerm, yLenTerm).negate(); lcVec.push_back(lenConstraint); } + else + { + utils::flattenOp(AND, lenConstraint, lcVec); + } NormalForm::getExplanationForPrefixEq(nfi, nfj, index, index, iinfo.d_ant); // Add premises for x != "" ^ y != "" @@ -1665,8 +1684,8 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi, else { tnz = x.eqNode(emp).negate(); - // lcVec.push_back(tnz); - iinfo.d_antn.push_back(tnz); + lcVec.push_back(tnz); + iinfo.d_noExplain.push_back(tnz); } } SkolemCache* skc = d_termReg.getSkolemCache(); @@ -1696,6 +1715,7 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi, iinfo.d_conc = getConclusion(y, x, PfRule::CONCAT_LPROP, isRev, skc, newSkolems); } + // add the length constraint(s) as the last antecedant Node lc = utils::mkAnd(lcVec); iinfo.d_ant.push_back(lc); iinfo.d_idRev = isRev; @@ -1804,7 +1824,8 @@ CoreSolver::ProcessLoopResult CoreSolver::processLoop(NormalForm& nfi, { Trace("strings-loop") << "Strings::Loop: tails are different." << std::endl; - d_im.sendInference(iinfo.d_ant, conc, Inference::FLOOP_CONFLICT, true); + d_im.sendInference( + iinfo.d_ant, conc, Inference::FLOOP_CONFLICT, false, true); return ProcessLoopResult::CONFLICT; } } @@ -1821,6 +1842,8 @@ CoreSolver::ProcessLoopResult CoreSolver::processLoop(NormalForm& nfi, Node expNonEmpty = d_state.explainNonEmpty(t); if (expNonEmpty.isNull()) { + // no antecedants necessary + iinfo.d_ant.clear(); // try to make t equal to empty to avoid loop iinfo.d_conc = nm->mkNode(kind::OR, split_eq, split_eq.negate()); iinfo.d_id = Inference::LEN_SPLIT_EMP; @@ -2098,10 +2121,11 @@ void CoreSolver::processDeq(Node ni, Node nj) } std::vector<Node> antecLen; antecLen.push_back(nm->mkNode(GEQ, nckLenTerm, d_one)); - d_im.sendInference({}, + d_im.sendInference(antecLen, antecLen, conc, Inference::DEQ_DISL_FIRST_CHAR_STRING_SPLIT, + false, true); return; } @@ -2142,8 +2166,12 @@ void CoreSolver::processDeq(Node ni, Node nj) d_termReg.registerTermAtomic(newSkolems[1], LENGTH_GEQ_ONE); std::vector<Node> antecLen; antecLen.push_back(nm->mkNode(GT, uxLen, uyLen)); - d_im.sendInference( - {}, antecLen, conc, Inference::DEQ_DISL_STRINGS_SPLIT, true); + d_im.sendInference(antecLen, + antecLen, + conc, + Inference::DEQ_DISL_STRINGS_SPLIT, + false, + true); } return; @@ -2238,7 +2266,7 @@ bool CoreSolver::processSimpleDeq(std::vector<Node>& nfi, Node conc = cc.size() == 1 ? cc[0] : NodeManager::currentNM()->mkNode(kind::AND, cc); - d_im.sendInference(ant, conc, Inference::DEQ_NORM_EMP, true); + d_im.sendInference(ant, conc, Inference::DEQ_NORM_EMP, isRev, true); return true; } @@ -2523,7 +2551,7 @@ void CoreSolver::checkLengthsEqc() { { Node eq = llt.eqNode(lc); ei->d_normalizedLength.set(eq); - d_im.sendInference(ant, eq, Inference::LEN_NORM, true); + d_im.sendInference(ant, eq, Inference::LEN_NORM, false, true); } } } diff --git a/src/theory/strings/extf_solver.cpp b/src/theory/strings/extf_solver.cpp index eff0b3d74..b028da38a 100644 --- a/src/theory/strings/extf_solver.cpp +++ b/src/theory/strings/extf_solver.cpp @@ -27,9 +27,7 @@ namespace CVC4 { namespace theory { namespace strings { -ExtfSolver::ExtfSolver(context::Context* c, - context::UserContext* u, - SolverState& s, +ExtfSolver::ExtfSolver(SolverState& s, InferenceManager& im, TermRegistry& tr, StringsRewriter& rewriter, @@ -45,10 +43,10 @@ ExtfSolver::ExtfSolver(context::Context* c, d_csolver(cs), d_extt(et), d_statistics(statistics), - d_preproc(d_termReg.getSkolemCache(), u, statistics), - d_hasExtf(c, false), - d_extfInferCache(c), - d_reduced(u) + d_preproc(d_termReg.getSkolemCache(), s.getUserContext(), statistics), + d_hasExtf(s.getSatContext(), false), + d_extfInferCache(s.getSatContext()), + d_reduced(s.getUserContext()) { d_extt.addFunctionKind(kind::STRING_SUBSTR); d_extt.addFunctionKind(kind::STRING_UPDATE); @@ -128,7 +126,8 @@ bool ExtfSolver::doReduction(int effort, Node n) lexp.push_back(lenx.eqNode(lens)); lexp.push_back(n.negate()); Node xneqs = x.eqNode(s).negate(); - d_im.sendInference(lexp, xneqs, Inference::CTN_NEG_EQUAL, true); + d_im.sendInference( + lexp, xneqs, Inference::CTN_NEG_EQUAL, false, true); } // this depends on the current assertions, so this // inference is context-dependent @@ -169,12 +168,13 @@ bool ExtfSolver::doReduction(int effort, Node n) Node s = n[1]; // positive contains reduces to a equality SkolemCache* skc = d_termReg.getSkolemCache(); - Node sk1 = skc->mkSkolemCached(x, s, SkolemCache::SK_FIRST_CTN_PRE, "sc1"); - Node sk2 = skc->mkSkolemCached(x, s, SkolemCache::SK_FIRST_CTN_POST, "sc2"); - Node eq = Rewriter::rewrite(x.eqNode(utils::mkNConcat(sk1, s, sk2))); - std::vector<Node> exp_vec; - exp_vec.push_back(n); - d_im.sendInference(d_emptyVec, exp_vec, eq, Inference::CTN_POS, true); + Node eq = d_termReg.eagerReduce(n, skc); + Assert(!eq.isNull()); + Assert(eq.getKind() == ITE && eq[0] == n); + eq = eq[1]; + std::vector<Node> expn; + expn.push_back(n); + d_im.sendInference(expn, expn, eq, Inference::CTN_POS, false, true); Trace("strings-extf-debug") << " resolve extf : " << n << " based on positive contain reduction." << std::endl; @@ -195,14 +195,13 @@ bool ExtfSolver::doReduction(int effort, Node n) std::vector<Node> new_nodes; Node res = d_preproc.simplify(n, new_nodes); Assert(res != n); - new_nodes.push_back(res.eqNode(n)); + new_nodes.push_back(n.eqNode(res)); Node nnlem = new_nodes.size() == 1 ? new_nodes[0] : nm->mkNode(AND, new_nodes); - nnlem = Rewriter::rewrite(nnlem); Trace("strings-red-lemma") << "Reduction_" << effort << " lemma : " << nnlem << std::endl; Trace("strings-red-lemma") << "...from " << n << std::endl; - d_im.sendInference(d_emptyVec, nnlem, Inference::REDUCTION, true); + d_im.sendInference(d_emptyVec, nnlem, Inference::REDUCTION, false, true); Trace("strings-extf-debug") << " resolve extf : " << n << " based on reduction." << std::endl; // add as reduction lemma @@ -277,7 +276,8 @@ void ExtfSolver::checkExtfEval(int effort) } // If there is information involving the children, attempt to do an // inference and/or mark n as reduced. - Node to_reduce; + bool reduced = false; + Node to_reduce = n; if (schanged) { Node sn = nm->mkNode(n.getKind(), schildren); @@ -383,7 +383,7 @@ void ExtfSolver::checkExtfEval(int effort) Trace("strings-extf") << " resolve extf : " << sn << " -> " << nrc << std::endl; Inference inf = effort == 0 ? Inference::EXTF : Inference::EXTF_N; - d_im.sendInference(einfo.d_exp, conc, inf, true); + d_im.sendInference(einfo.d_exp, conc, inf, false, true); d_statistics.d_cdSimplifications << n.getKind(); if (d_state.isInConflict()) { @@ -404,6 +404,7 @@ void ExtfSolver::checkExtfEval(int effort) einfo.d_modelActive = false; } } + reduced = true; } else { @@ -427,28 +428,26 @@ void ExtfSolver::checkExtfEval(int effort) effort == 0 ? Inference::EXTF_D : Inference::EXTF_D_N; d_im.sendInternalInference(einfo.d_exp, nrcAssert, infer); } - // We must use the original n here to avoid circular justifications for - // why extended functions are reduced below. In particular, to_reduce - // should never be a duplicate of another term considered in the block - // of code for checkExtfInference below. - to_reduce = n; + to_reduce = nrc; } } - else - { - to_reduce = n; - } + // We must use the original n here to avoid circular justifications for + // why extended functions are reduced. In particular, n should never be a + // duplicate of another term considered in the block of code for + // checkExtfInference below. // if not reduced and not processed - if (!to_reduce.isNull() - && inferProcessed.find(to_reduce) == inferProcessed.end()) + if (!reduced && !n.isNull() + && inferProcessed.find(n) == inferProcessed.end()) { - inferProcessed.insert(to_reduce); + inferProcessed.insert(n); Assert(effort < 3); if (effort == 1) { Trace("strings-extf") << " cannot rewrite extf : " << to_reduce << std::endl; } + // we take to_reduce to be the (partially) reduced version of n, which + // is justified by the explanation in einfo. checkExtfInference(n, to_reduce, einfo, effort); if (Trace.isOn("strings-extf-list")) { diff --git a/src/theory/strings/extf_solver.h b/src/theory/strings/extf_solver.h index 80921550e..4ba38bfc6 100644 --- a/src/theory/strings/extf_solver.h +++ b/src/theory/strings/extf_solver.h @@ -83,9 +83,7 @@ class ExtfSolver typedef context::CDHashSet<Node, NodeHashFunction> NodeSet; public: - ExtfSolver(context::Context* c, - context::UserContext* u, - SolverState& s, + ExtfSolver(SolverState& s, InferenceManager& im, TermRegistry& tr, StringsRewriter& rewriter, diff --git a/src/theory/strings/infer_info.cpp b/src/theory/strings/infer_info.cpp index 174bbe2b7..ca5e8320d 100644 --- a/src/theory/strings/infer_info.cpp +++ b/src/theory/strings/infer_info.cpp @@ -14,6 +14,8 @@ #include "theory/strings/infer_info.h" +#include "theory/strings/theory_strings_utils.h" + namespace CVC4 { namespace theory { namespace strings { @@ -85,6 +87,7 @@ const char* toString(Inference i) case Inference::CTN_NEG_EQUAL: return "CTN_NEG_EQUAL"; case Inference::CTN_POS: return "CTN_POS"; case Inference::REDUCTION: return "REDUCTION"; + case Inference::PREFIX_CONFLICT: return "PREFIX_CONFLICT"; default: return "?"; } } @@ -106,14 +109,20 @@ bool InferInfo::isTrivial() const bool InferInfo::isConflict() const { Assert(!d_conc.isNull()); - return d_conc.isConst() && !d_conc.getConst<bool>() && d_antn.empty(); + return d_conc.isConst() && !d_conc.getConst<bool>() && d_noExplain.empty(); } bool InferInfo::isFact() const { Assert(!d_conc.isNull()); TNode atom = d_conc.getKind() == kind::NOT ? d_conc[0] : d_conc; - return !atom.isConst() && atom.getKind() != kind::OR && d_antn.empty(); + return !atom.isConst() && atom.getKind() != kind::OR && d_noExplain.empty(); +} + +Node InferInfo::getAntecedant() const +{ + // d_noExplain is a subset of d_ant + return utils::mkAnd(d_ant); } std::ostream& operator<<(std::ostream& out, const InferInfo& ii) @@ -127,9 +136,9 @@ std::ostream& operator<<(std::ostream& out, const InferInfo& ii) { out << " :ant (" << ii.d_ant << ")"; } - if (!ii.d_antn.empty()) + if (!ii.d_noExplain.empty()) { - out << " :antn (" << ii.d_antn << ")"; + out << " :no-explain (" << ii.d_noExplain << ")"; } out << ")"; return out; diff --git a/src/theory/strings/infer_info.h b/src/theory/strings/infer_info.h index 7d41dca98..31a74784e 100644 --- a/src/theory/strings/infer_info.h +++ b/src/theory/strings/infer_info.h @@ -38,6 +38,7 @@ namespace strings { */ enum class Inference : uint32_t { + BEGIN, //-------------------------------------- base solver // initial normalize singular // x1 = "" ^ ... ^ x_{i-1} = "" ^ x_{i+1} = "" ^ ... ^ xn = "" => @@ -295,6 +296,10 @@ enum class Inference : uint32_t // (see theory_strings_preprocess). REDUCTION, //-------------------------------------- end extended function solver + //-------------------------------------- prefix conflict + // prefix conflict (coarse-grained) + PREFIX_CONFLICT, + //-------------------------------------- end prefix conflict NONE, }; @@ -359,9 +364,11 @@ class InferInfo /** * The "new literal" antecedant(s) of the inference, interpreted * conjunctively. These are literals that were needed to show the conclusion - * but do not currently hold in the equality engine. + * but do not currently hold in the equality engine. These should be a subset + * of d_ant. In other words, antecedants that are not explained are stored + * in *both* d_ant and d_noExplain. */ - std::vector<Node> d_antn; + std::vector<Node> d_noExplain; /** * A list of new skolems introduced as a result of this inference. They * are mapped to by a length status, indicating the length constraint that @@ -372,15 +379,17 @@ class InferInfo bool isTrivial() const; /** * Does this infer info correspond to a conflict? True if d_conc is false - * and it has no new antecedants (d_antn). + * and it has no new antecedants (d_noExplain). */ bool isConflict() const; /** * Does this infer info correspond to a "fact". A fact is an inference whose * conclusion should be added as an equality or predicate to the equality - * engine with no new external antecedants (d_antn). + * engine with no new external antecedants (d_noExplain). */ bool isFact() const; + /** Get antecedant */ + Node getAntecedant() const; }; /** diff --git a/src/theory/strings/inference_manager.cpp b/src/theory/strings/inference_manager.cpp index 91af2a434..88cf6d958 100644 --- a/src/theory/strings/inference_manager.cpp +++ b/src/theory/strings/inference_manager.cpp @@ -117,9 +117,10 @@ bool InferenceManager::sendInternalInference(std::vector<Node>& exp, } void InferenceManager::sendInference(const std::vector<Node>& exp, - const std::vector<Node>& expn, + const std::vector<Node>& noExplain, Node eq, Inference infer, + bool isRev, bool asLemma) { eq = eq.isNull() ? d_false : Rewriter::rewrite(eq); @@ -130,19 +131,21 @@ void InferenceManager::sendInference(const std::vector<Node>& exp, // wrap in infer info and send below InferInfo ii; ii.d_id = infer; + ii.d_idRev = isRev; ii.d_conc = eq; ii.d_ant = exp; - ii.d_antn = expn; + ii.d_noExplain = noExplain; sendInference(ii, asLemma); } void InferenceManager::sendInference(const std::vector<Node>& exp, Node eq, Inference infer, + bool isRev, bool asLemma) { - std::vector<Node> expn; - sendInference(exp, expn, eq, infer, asLemma); + std::vector<Node> noExplain; + sendInference(exp, noExplain, eq, infer, isRev, asLemma); } void InferenceManager::sendInference(const InferInfo& ii, bool asLemma) @@ -277,7 +280,7 @@ void InferenceManager::doPendingFacts() InferInfo& ii = d_pending[i]; // At this point, ii should be a "fact", i.e. something whose conclusion // should be added as a normal equality or predicate to the equality engine - // with no new external assumptions (ii.d_antn). + // with no new external assumptions (ii.d_noExplain). Assert(ii.isFact()); Node facts = ii.d_conc; Node exp = utils::mkAnd(ii.d_ant); @@ -336,13 +339,12 @@ void InferenceManager::doPendingLemmas() Node eqExp; if (options::stringRExplainLemmas()) { - eqExp = mkExplain(ii.d_ant, ii.d_antn); + eqExp = mkExplain(ii.d_ant, ii.d_noExplain); } else { std::vector<Node> ev; ev.insert(ev.end(), ii.d_ant.begin(), ii.d_ant.end()); - ev.insert(ev.end(), ii.d_antn.begin(), ii.d_antn.end()); eqExp = utils::mkAnd(ev); } // make the lemma node @@ -455,12 +457,12 @@ bool InferenceManager::hasProcessed() const Node InferenceManager::mkExplain(const std::vector<Node>& a) const { - std::vector<Node> an; - return mkExplain(a, an); + std::vector<Node> noExplain; + return mkExplain(a, noExplain); } Node InferenceManager::mkExplain(const std::vector<Node>& a, - const std::vector<Node>& an) const + const std::vector<Node>& noExplain) const { std::vector<TNode> antec_exp; // copy to processing vector @@ -472,6 +474,16 @@ Node InferenceManager::mkExplain(const std::vector<Node>& a, eq::EqualityEngine* ee = d_state.getEqualityEngine(); for (const Node& apc : aconj) { + if (std::find(noExplain.begin(), noExplain.end(), apc) != noExplain.end()) + { + if (std::find(antec_exp.begin(), antec_exp.end(), apc) == antec_exp.end()) + { + Debug("strings-explain") + << "Add to explanation (new literal) " << apc << std::endl; + antec_exp.push_back(apc); + } + continue; + } Assert(apc.getKind() != AND); Debug("strings-explain") << "Add to explanation " << apc << std::endl; if (apc.getKind() == NOT && apc[0].getKind() == EQUAL) @@ -485,15 +497,6 @@ Node InferenceManager::mkExplain(const std::vector<Node>& a, // now, explain explain(apc, antec_exp); } - for (const Node& anc : an) - { - if (std::find(antec_exp.begin(), antec_exp.end(), anc) == antec_exp.end()) - { - Debug("strings-explain") - << "Add to explanation (new literal) " << anc << std::endl; - antec_exp.push_back(anc); - } - } Node ant; if (antec_exp.empty()) { diff --git a/src/theory/strings/inference_manager.h b/src/theory/strings/inference_manager.h index 4e50a6cb7..016891737 100644 --- a/src/theory/strings/inference_manager.h +++ b/src/theory/strings/inference_manager.h @@ -109,26 +109,27 @@ class InferenceManager bool sendInternalInference(std::vector<Node>& exp, Node conc, Inference infer); + /** send inference * - * This function should be called when ( exp ^ exp_n ) => eq. The set exp + * This function should be called when exp => eq. The set exp * contains literals that are explainable, i.e. those that hold in the * equality engine of the theory of strings. On the other hand, the set - * exp_n ("explanations new") contain nodes that are not explainable by the - * theory of strings. This method may call sendLemma or otherwise add a - * InferInfo to d_pending, indicating a fact should be asserted to the - * equality engine. Overall, the result of this method is one of the - * following: + * noExplain contains nodes that are not explainable by the theory of strings. + * This method may call sendLemma or otherwise add a InferInfo to d_pending, + * indicating a fact should be asserted to the equality engine. Overall, the + * result of this method is one of the following: * - * [1] (No-op) Do nothing if eq is true, + * [1] (No-op) Do nothing if eq is equivalent to true, * * [2] (Infer) Indicate that eq should be added to the equality engine of this * class with explanation exp, where exp is a set of literals that currently * hold in the equality engine. We add this to the pending vector d_pending. * - * [3] (Lemma) Indicate that the lemma ( EXPLAIN(exp) ^ exp_n ) => eq should - * be sent on the output channel of the theory of strings, where EXPLAIN - * returns the explanation of the node in exp in terms of the literals + * [3] (Lemma) Indicate that the lemma + * ( EXPLAIN(exp \ noExplain) ^ noExplain ) => eq + * should be sent on the output channel of the theory of strings, where + * EXPLAIN returns the explanation of the node in exp in terms of the literals * asserted to the theory of strings, as computed by the equality engine. * This is also added to a pending vector, d_pendingLem. * @@ -136,25 +137,33 @@ class InferenceManager * channel of the theory of strings. * * Determining which case to apply depends on the form of eq and whether - * exp_n is empty. In particular, lemmas must be used whenever exp_n is - * non-empty, conflicts are used when exp_n is empty and eq is false. + * noExplain is empty. In particular, lemmas must be used whenever noExplain + * is non-empty, conflicts are used when noExplain is empty and eq is false. * - * The argument infer identifies the reason for inference, used for + * @param exp The explanation of eq. + * @param noExplain The subset of exp that cannot be explained by the + * equality engine. This may impact whether we are processing this call as a + * fact or as a lemma. + * @param eq The conclusion. + * @param infer Identifies the reason for inference, used for * debugging. This updates the statistics about the number of inferences made * of each type. - * - * If the flag asLemma is true, then this method will send a lemma instead + * @param isRev Whether this is the "reverse variant" of the inference, which + * is used as a hint for proof reconstruction. + * @param asLemma If true, then this method will send a lemma instead * of a fact whenever applicable. */ void sendInference(const std::vector<Node>& exp, - const std::vector<Node>& exp_n, + const std::vector<Node>& noExplain, Node eq, Inference infer, + bool isRev = false, bool asLemma = false); - /** same as above, but where exp_n is empty */ + /** same as above, but where noExplain is empty */ void sendInference(const std::vector<Node>& exp, Node eq, Inference infer, + bool isRev = false, bool asLemma = false); /** Send inference @@ -258,8 +267,9 @@ class InferenceManager * that have been asserted to the equality engine. */ Node mkExplain(const std::vector<Node>& a) const; - /** Same as above, but the new literals an are append to the result */ - Node mkExplain(const std::vector<Node>& a, const std::vector<Node>& an) const; + /** Same as above, but with a subset noExplain that should not be explained */ + Node mkExplain(const std::vector<Node>& a, + const std::vector<Node>& noExplain) const; /** * Explain literal l, add conjuncts to assumptions vector instead of making * the node corresponding to their conjunction. diff --git a/src/theory/strings/regexp_solver.cpp b/src/theory/strings/regexp_solver.cpp index c5d6df601..62127d5c0 100644 --- a/src/theory/strings/regexp_solver.cpp +++ b/src/theory/strings/regexp_solver.cpp @@ -221,10 +221,13 @@ void RegExpSolver::check(const std::map<Node, std::vector<Node> >& mems) else { // we have a conflict - std::vector<Node> exp_n; - exp_n.push_back(assertion); + std::vector<Node> iexp = nfexp; + std::vector<Node> noExplain; + iexp.push_back(assertion); + noExplain.push_back(assertion); Node conc = Node::null(); - d_im.sendInference(nfexp, exp_n, conc, Inference::RE_NF_CONFLICT); + d_im.sendInference( + iexp, noExplain, conc, Inference::RE_NF_CONFLICT); addedLemma = true; break; } @@ -266,8 +269,10 @@ void RegExpSolver::check(const std::map<Node, std::vector<Node> >& mems) // if simplifying successfully generated a lemma if (!conc.isNull()) { - std::vector<Node> exp_n; - exp_n.push_back(assertion); + std::vector<Node> iexp = rnfexp; + std::vector<Node> noExplain; + iexp.push_back(assertion); + noExplain.push_back(assertion); Assert(atom.getKind() == STRING_IN_REGEXP); if (polarity) { @@ -279,7 +284,7 @@ void RegExpSolver::check(const std::map<Node, std::vector<Node> >& mems) } Inference inf = polarity ? Inference::RE_UNFOLD_POS : Inference::RE_UNFOLD_NEG; - d_im.sendInference(rnfexp, exp_n, conc, inf); + d_im.sendInference(iexp, noExplain, conc, inf); addedLemma = true; if (changed) { @@ -399,7 +404,7 @@ bool RegExpSolver::checkEqcInclusion(std::vector<Node>& mems) Node conc; d_im.sendInference( - vec_nodes, conc, Inference::RE_INTER_INCLUDE, true); + vec_nodes, conc, Inference::RE_INTER_INCLUDE, false, true); return false; } } @@ -480,19 +485,21 @@ bool RegExpSolver::checkEqcIntersect(const std::vector<Node>& mems) vec_nodes.push_back(mi[0].eqNode(m[0])); } Node conc; - d_im.sendInference(vec_nodes, conc, Inference::RE_INTER_CONF, true); + d_im.sendInference( + vec_nodes, conc, Inference::RE_INTER_CONF, false, true); // conflict, return return false; } // rewrite to ensure the equality checks below are precise - Node mres = Rewriter::rewrite(nm->mkNode(STRING_IN_REGEXP, mi[0], resR)); - if (mres == mi) + Node mres = nm->mkNode(STRING_IN_REGEXP, mi[0], resR); + Node mresr = Rewriter::rewrite(mres); + if (mresr == mi) { // if R1 = intersect( R1, R2 ), then x in R1 ^ x in R2 is equivalent // to x in R1, hence x in R2 can be marked redundant. d_im.markReduced(m); } - else if (mres == m) + else if (mresr == m) { // same as above, opposite direction d_im.markReduced(mi); @@ -508,7 +515,8 @@ bool RegExpSolver::checkEqcIntersect(const std::vector<Node>& mems) { vec_nodes.push_back(mi[0].eqNode(m[0])); } - d_im.sendInference(vec_nodes, mres, Inference::RE_INTER_INFER, true); + d_im.sendInference( + vec_nodes, mres, Inference::RE_INTER_INFER, false, true); // both are reduced d_im.markReduced(m); d_im.markReduced(mi); @@ -529,10 +537,12 @@ bool RegExpSolver::checkPDerivative( { case 0: { - std::vector<Node> exp_n; - exp_n.push_back(atom); - exp_n.push_back(x.eqNode(d_emptyString)); - d_im.sendInference(nf_exp, exp_n, exp, Inference::RE_DELTA); + std::vector<Node> noExplain; + noExplain.push_back(atom); + noExplain.push_back(x.eqNode(d_emptyString)); + std::vector<Node> iexp = nf_exp; + iexp.insert(iexp.end(), noExplain.begin(), noExplain.end()); + d_im.sendInference(iexp, noExplain, exp, Inference::RE_DELTA); addedLemma = true; d_regexp_ccached.insert(atom); return false; @@ -544,11 +554,12 @@ bool RegExpSolver::checkPDerivative( } case 2: { - std::vector<Node> exp_n; - exp_n.push_back(atom); - exp_n.push_back(x.eqNode(d_emptyString)); - Node conc; - d_im.sendInference(nf_exp, exp_n, conc, Inference::RE_DELTA_CONF); + std::vector<Node> noExplain; + noExplain.push_back(atom); + noExplain.push_back(x.eqNode(d_emptyString)); + std::vector<Node> iexp = nf_exp; + iexp.insert(iexp.end(), noExplain.begin(), noExplain.end()); + d_im.sendInference(iexp, noExplain, d_false, Inference::RE_DELTA_CONF); addedLemma = true; d_regexp_ccached.insert(atom); return false; @@ -637,9 +648,11 @@ bool RegExpSolver::deriveRegExp(Node x, conc = NodeManager::currentNM()->mkNode(STRING_IN_REGEXP, left, dc); } } - std::vector<Node> exp_n; - exp_n.push_back(atom); - d_im.sendInference(ant, exp_n, conc, Inference::RE_DERIVE); + std::vector<Node> iexp = ant; + std::vector<Node> noExplain; + noExplain.push_back(atom); + iexp.push_back(atom); + d_im.sendInference(iexp, noExplain, conc, Inference::RE_DERIVE); return true; } return false; diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 142b0006b..0ad887d2f 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -51,9 +51,7 @@ TheoryStrings::TheoryStrings(context::Context* c, d_rewriter(&d_statistics.d_rewrites), d_bsolver(d_state, d_im), d_csolver(d_state, d_im, d_termReg, d_bsolver), - d_esolver(c, - u, - d_state, + d_esolver(d_state, d_im, d_termReg, d_rewriter, @@ -61,8 +59,12 @@ TheoryStrings::TheoryStrings(context::Context* c, d_csolver, d_extTheory, d_statistics), - d_rsolver(d_state, d_im, d_termReg.getSkolemCache(), - d_csolver, d_esolver, d_statistics), + d_rsolver(d_state, + d_im, + d_termReg.getSkolemCache(), + d_csolver, + d_esolver, + d_statistics), d_stringsFmf(c, u, valuation, d_termReg) { bool eagerEval = options::stringEagerEval(); |