From: Andrew Reynolds Date: Mon, 17 Aug 2020 18:07:13 +0000 (-0500) Subject: (proof-new) Prepare the theory of strings for proof reconstruction (#4885) X-Git-Tag: cvc5-1.0.0~2995 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=5c78f336b8276a2ed8916e2a9447a29a2caca069;p=cvc5.git (proof-new) Prepare the theory of strings for proof reconstruction (#4885) This updates the internal data structure for strings inferences "InferInfo" such that it is amenable to proof reconstruction. Currently, the explanation for a conclusion is in two parts: (1) d_ant, the antecedents that can be explained by the current equality engine, (2) d_antn, the antecedents that cannot. For proof reconstruction, the order of some antecedents matters. This is difficult with the above data structure since elements in these two vectors are not given an ordering relative to each other. After this PR, we store: (1) d_ant, all antecedants, which are ordered in a way that is amenable to proofs (to be introduced on following PRs), (2) d_noExplain, the subset of d_ant that cannot be explained by the current equality engine. This PR modifies calls to InferenceManager in preparation for extending it with a proof reconstructor InferProofCons which will convert strings::InferInfo into instructions for building ProofNode. --- 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& 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 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 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 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 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 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& 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 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 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 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 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() && d_antn.empty(); + return d_conc.isConst() && !d_conc.getConst() && 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 d_antn; + std::vector 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& exp, } void InferenceManager::sendInference(const std::vector& exp, - const std::vector& expn, + const std::vector& 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& 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& exp, Node eq, Inference infer, + bool isRev, bool asLemma) { - std::vector expn; - sendInference(exp, expn, eq, infer, asLemma); + std::vector 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 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& a) const { - std::vector an; - return mkExplain(a, an); + std::vector noExplain; + return mkExplain(a, noExplain); } Node InferenceManager::mkExplain(const std::vector& a, - const std::vector& an) const + const std::vector& noExplain) const { std::vector antec_exp; // copy to processing vector @@ -472,6 +474,16 @@ Node InferenceManager::mkExplain(const std::vector& 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& 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& 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& exp, - const std::vector& exp_n, + const std::vector& 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& 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& a) const; - /** Same as above, but the new literals an are append to the result */ - Node mkExplain(const std::vector& a, const std::vector& an) const; + /** Same as above, but with a subset noExplain that should not be explained */ + Node mkExplain(const std::vector& a, + const std::vector& 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 >& mems) else { // we have a conflict - std::vector exp_n; - exp_n.push_back(assertion); + std::vector iexp = nfexp; + std::vector 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 >& mems) // if simplifying successfully generated a lemma if (!conc.isNull()) { - std::vector exp_n; - exp_n.push_back(assertion); + std::vector iexp = rnfexp; + std::vector 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 >& 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& 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& 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& 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 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 noExplain; + noExplain.push_back(atom); + noExplain.push_back(x.eqNode(d_emptyString)); + std::vector 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 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 noExplain; + noExplain.push_back(atom); + noExplain.push_back(x.eqNode(d_emptyString)); + std::vector 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 exp_n; - exp_n.push_back(atom); - d_im.sendInference(ant, exp_n, conc, Inference::RE_DERIVE); + std::vector iexp = ant; + std::vector 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();