diff options
| -rw-r--r-- | src/theory/strings/core_solver.cpp | 3 | ||||
| -rw-r--r-- | src/theory/strings/infer_info.cpp | 14 | ||||
| -rw-r--r-- | src/theory/strings/infer_info.h | 9 | ||||
| -rw-r--r-- | src/theory/strings/inference_manager.cpp | 396 | ||||
| -rw-r--r-- | src/theory/strings/inference_manager.h | 105 | ||||
| -rw-r--r-- | src/theory/strings/sequences_stats.cpp | 6 | ||||
| -rw-r--r-- | src/theory/strings/sequences_stats.h | 4 | ||||
| -rw-r--r-- | src/theory/strings/solver_state.cpp | 40 | ||||
| -rw-r--r-- | src/theory/strings/solver_state.h | 19 | ||||
| -rw-r--r-- | src/theory/strings/theory_strings.cpp | 88 |
10 files changed, 316 insertions, 368 deletions
diff --git a/src/theory/strings/core_solver.cpp b/src/theory/strings/core_solver.cpp index ef3b978ef..edd00c954 100644 --- a/src/theory/strings/core_solver.cpp +++ b/src/theory/strings/core_solver.cpp @@ -2577,7 +2577,8 @@ bool CoreSolver::processInferInfo(CoreInferInfo& cii) // send phase requirements for (const std::pair<const Node, bool> pp : cii.d_pendingPhase) { - d_im.sendPhaseRequirement(pp.first, pp.second); + Node ppr = Rewriter::rewrite(pp.first); + d_im.addPendingPhaseRequirement(ppr, pp.second); } // send the inference, which is a lemma diff --git a/src/theory/strings/infer_info.cpp b/src/theory/strings/infer_info.cpp index c4514a33b..0d2f94f91 100644 --- a/src/theory/strings/infer_info.cpp +++ b/src/theory/strings/infer_info.cpp @@ -14,6 +14,7 @@ #include "theory/strings/infer_info.h" +#include "theory/strings/inference_manager.h" #include "theory/strings/theory_strings_utils.h" namespace CVC4 { @@ -98,7 +99,18 @@ std::ostream& operator<<(std::ostream& out, Inference i) return out; } -InferInfo::InferInfo() : d_id(Inference::NONE), d_idRev(false) {} +InferInfo::InferInfo() : d_sim(nullptr), d_id(Inference::NONE), d_idRev(false) +{ +} + +bool InferInfo::process(TheoryInferenceManager* im, bool asLemma) +{ + if (asLemma) + { + return d_sim->processLemma(*this); + } + return d_sim->processFact(*this); +} bool InferInfo::isTrivial() const { diff --git a/src/theory/strings/infer_info.h b/src/theory/strings/infer_info.h index 13e9a3f64..4c5674d2b 100644 --- a/src/theory/strings/infer_info.h +++ b/src/theory/strings/infer_info.h @@ -21,6 +21,7 @@ #include <vector> #include "expr/node.h" +#include "theory/theory_inference.h" #include "util/safe_print.h" namespace CVC4 { @@ -347,6 +348,8 @@ enum LengthStatus LENGTH_GEQ_ONE }; +class InferenceManager; + /** * An inference. This is a class to track an unprocessed call to either * send a fact, lemma, or conflict that is waiting to be asserted to the @@ -368,11 +371,15 @@ enum LengthStatus * - (main equality) x ++ y ++ v1 = z ++ w ++ v2, * - (length constraint) len(y) = len(w). */ -class InferInfo +class InferInfo : public TheoryInference { public: InferInfo(); ~InferInfo() {} + /** Process this inference */ + bool process(TheoryInferenceManager* im, bool asLemma) override; + /** Pointer to the class used for processing this info */ + InferenceManager* d_sim; /** The inference identifier */ Inference d_id; /** Whether it is the reverse form of the above id */ diff --git a/src/theory/strings/inference_manager.cpp b/src/theory/strings/inference_manager.cpp index a465916e4..e324689f5 100644 --- a/src/theory/strings/inference_manager.cpp +++ b/src/theory/strings/inference_manager.cpp @@ -34,11 +34,13 @@ InferenceManager::InferenceManager(Theory& t, ExtTheory& e, SequencesStatistics& statistics, ProofNodeManager* pnm) - : TheoryInferenceManager(t, s, pnm), + : InferenceManagerBuffered(t, s, pnm), d_state(s), d_termReg(tr), d_extt(e), - d_statistics(statistics) + d_statistics(statistics), + d_ipc(pnm ? new InferProofCons(d_state.getSatContext(), pnm, d_statistics) + : nullptr) { NodeManager* nm = NodeManager::currentNM(); d_zero = nm->mkConst(Rational(0)); @@ -47,6 +49,20 @@ InferenceManager::InferenceManager(Theory& t, d_false = nm->mkConst(false); } +void InferenceManager::doPending() +{ + doPendingFacts(); + if (d_state.isInConflict()) + { + // just clear the pending vectors, nothing else to do + clearPendingLemmas(); + clearPendingPhaseRequirements(); + return; + } + doPendingLemmas(); + doPendingPhaseRequirements(); +} + bool InferenceManager::sendInternalInference(std::vector<Node>& exp, Node conc, Inference infer) @@ -106,17 +122,21 @@ bool InferenceManager::sendInternalInference(std::vector<Node>& exp, return true; } -void InferenceManager::sendInference(const std::vector<Node>& exp, +bool InferenceManager::sendInference(const std::vector<Node>& exp, const std::vector<Node>& noExplain, Node eq, Inference infer, bool isRev, bool asLemma) { - eq = eq.isNull() ? d_false : Rewriter::rewrite(eq); - if (eq == d_true) + if (eq.isNull()) { - return; + eq = d_false; + } + else if (Rewriter::rewrite(eq) == d_true) + { + // if trivial, return + return false; } // wrap in infer info and send below InferInfo ii; @@ -126,46 +146,43 @@ void InferenceManager::sendInference(const std::vector<Node>& exp, ii.d_ant = exp; ii.d_noExplain = noExplain; sendInference(ii, asLemma); + return true; } -void InferenceManager::sendInference(const std::vector<Node>& exp, +bool InferenceManager::sendInference(const std::vector<Node>& exp, Node eq, Inference infer, bool isRev, bool asLemma) { std::vector<Node> noExplain; - sendInference(exp, noExplain, eq, infer, isRev, asLemma); + return sendInference(exp, noExplain, eq, infer, isRev, asLemma); } -void InferenceManager::sendInference(const InferInfo& ii, bool asLemma) +void InferenceManager::sendInference(InferInfo& ii, bool asLemma) { Assert(!ii.isTrivial()); + // set that this inference manager will be processing this inference + ii.d_sim = this; Trace("strings-infer-debug") << "sendInference: " << ii << ", asLemma = " << asLemma << std::endl; // check if we should send a conflict, lemma or a fact - if (asLemma || options::stringInferAsLemmas() || !ii.isFact()) + if (ii.isConflict()) + { + Trace("strings-infer-debug") << "...as conflict" << std::endl; + Trace("strings-lemma") << "Strings::Conflict: " << ii.d_ant << " by " + << ii.d_id << std::endl; + Trace("strings-conflict") << "CONFLICT: inference conflict " << ii.d_ant + << " by " << ii.d_id << std::endl; + ++(d_statistics.d_conflictsInfer); + // process the conflict immediately + processConflict(ii); + return; + } + else if (asLemma || options::stringInferAsLemmas() || !ii.isFact()) { - if (ii.isConflict()) - { - Trace("strings-infer-debug") << "...as conflict" << std::endl; - Trace("strings-lemma") << "Strings::Conflict: " << ii.d_ant << " by " - << ii.d_id << std::endl; - Trace("strings-conflict") << "CONFLICT: inference conflict " << ii.d_ant - << " by " << ii.d_id << std::endl; - // we must fully explain it - Node conf = mkExplain(ii.d_ant); - Trace("strings-assert") << "(assert (not " << conf << ")) ; conflict " - << ii.d_id << std::endl; - ++(d_statistics.d_conflictsInfer); - // only keep stats if we process it here - d_statistics.d_inferences << ii.d_id; - d_out.conflict(conf); - d_state.notifyInConflict(); - return; - } Trace("strings-infer-debug") << "...as lemma" << std::endl; - d_pendingLem.push_back(ii); + addPendingLemma(std::unique_ptr<InferInfo>(new InferInfo(ii))); return; } if (options::stringInferSym()) @@ -182,6 +199,7 @@ void InferenceManager::sendInference(const InferInfo& ii, bool asLemma) Node eqs = ii.d_conc.substitute( vars.begin(), vars.end(), subs.begin(), subs.end()); InferInfo iiSubsLem; + iiSubsLem.d_sim = this; // keep the same id for now, since we are transforming the form of the // inference, not the root reason. iiSubsLem.d_id = ii.d_id; @@ -199,7 +217,7 @@ void InferenceManager::sendInference(const InferInfo& ii, bool asLemma) } } Trace("strings-infer-debug") << "...as symbolic lemma" << std::endl; - d_pendingLem.push_back(iiSubsLem); + addPendingLemma(std::unique_ptr<InferInfo>(new InferInfo(iiSubsLem))); return; } if (Trace.isOn("strings-lemma-debug")) @@ -207,13 +225,13 @@ void InferenceManager::sendInference(const InferInfo& ii, bool asLemma) for (const Node& u : unproc) { Trace("strings-lemma-debug") - << " non-trivial exp : " << u << std::endl; + << " non-trivial explanation : " << u << std::endl; } } } Trace("strings-infer-debug") << "...as fact" << std::endl; - // add to pending, to be processed as a fact - d_pending.push_back(ii); + // add to pending to be processed as a fact + addPendingFact(std::unique_ptr<InferInfo>(new InferInfo(ii))); } bool InferenceManager::sendSplit(Node a, Node b, Inference infer, bool preq) @@ -226,19 +244,15 @@ bool InferenceManager::sendSplit(Node a, Node b, Inference infer, bool preq) } NodeManager* nm = NodeManager::currentNM(); InferInfo iiSplit; + iiSplit.d_sim = this; iiSplit.d_id = infer; iiSplit.d_conc = nm->mkNode(OR, eq, nm->mkNode(NOT, eq)); - sendPhaseRequirement(eq, preq); - d_pendingLem.push_back(iiSplit); + eq = Rewriter::rewrite(eq); + addPendingPhaseRequirement(eq, preq); + addPendingLemma(std::unique_ptr<InferInfo>(new InferInfo(iiSplit))); return true; } -void InferenceManager::sendPhaseRequirement(Node lit, bool pol) -{ - lit = Rewriter::rewrite(lit); - d_pendingReqPhase[lit] = pol; -} - void InferenceManager::setIncomplete() { d_out.setIncomplete(); } void InferenceManager::addToExplanation(Node a, @@ -258,239 +272,167 @@ void InferenceManager::addToExplanation(Node lit, std::vector<Node>& exp) const { if (!lit.isNull()) { + Assert(!lit.isConst()); exp.push_back(lit); } } -void InferenceManager::doPendingFacts() +bool InferenceManager::hasProcessed() const { - size_t i = 0; - while (!d_state.isInConflict() && i < d_pending.size()) - { - 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_noExplain). - Assert(ii.isFact()); - Node facts = ii.d_conc; - Node exp = utils::mkAnd(ii.d_ant); - Trace("strings-assert") << "(assert (=> " << exp << " " << facts - << ")) ; fact " << ii.d_id << std::endl; - // only keep stats if we process it here - Trace("strings-lemma") << "Strings::Fact: " << facts << " from " << exp - << " by " << ii.d_id << std::endl; - d_statistics.d_inferences << ii.d_id; - // assert it as a pending fact - if (facts.getKind() == AND) - { - for (const Node& fact : facts) - { - bool polarity = fact.getKind() != NOT; - TNode atom = polarity ? fact : fact[0]; - // no double negation or double (conjunctive) conclusions - Assert(atom.getKind() != NOT && atom.getKind() != AND); - assertInternalFact(atom, polarity, exp); - } - } - else - { - bool polarity = facts.getKind() != NOT; - TNode atom = polarity ? facts : facts[0]; - // no double negation or double (conjunctive) conclusions - Assert(atom.getKind() != NOT && atom.getKind() != AND); - assertInternalFact(atom, polarity, exp); - } - i++; - } - d_pending.clear(); + return d_state.isInConflict() || hasPending(); } -void InferenceManager::doPendingLemmas() +void InferenceManager::markCongruent(Node a, Node b) { - if (d_state.isInConflict()) - { - // just clear the pending vectors, nothing else to do - d_pendingLem.clear(); - d_pendingReqPhase.clear(); - return; - } - NodeManager* nm = NodeManager::currentNM(); - for (unsigned i = 0, psize = d_pendingLem.size(); i < psize; i++) - { - InferInfo& ii = d_pendingLem[i]; - Assert(!ii.isTrivial()); - Assert(!ii.isConflict()); - // get the explanation - Node eqExp; - if (options::stringRExplainLemmas()) - { - 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()); - eqExp = utils::mkAnd(ev); - } - // make the lemma node - Node lem = ii.d_conc; - if (eqExp != d_true) - { - lem = nm->mkNode(IMPLIES, eqExp, lem); - } - Trace("strings-pending") << "Process pending lemma : " << lem << std::endl; - Trace("strings-assert") - << "(assert " << lem << ") ; lemma " << ii.d_id << std::endl; - Trace("strings-lemma") << "Strings::Lemma: " << lem << " by " << ii.d_id - << std::endl; - // only keep stats if we process it here - d_statistics.d_inferences << ii.d_id; - ++(d_statistics.d_lemmasInfer); - - // Process the side effects of the inference info. - // Register the new skolems from this inference. We register them here - // (lazily), since this is the moment when we have decided to process the - // inference. - for (const std::pair<const LengthStatus, std::vector<Node> >& sks : - ii.d_new_skolem) - { - for (const Node& n : sks.second) - { - d_termReg.registerTermAtomic(n, sks.first); - } - } - LemmaProperty p = LemmaProperty::NONE; - if (ii.d_id == Inference::REDUCTION) - { - p |= LemmaProperty::NEEDS_JUSTIFY; - } - d_out.lemma(lem, p); - } - // process the pending require phase calls - for (const std::pair<const Node, bool>& prp : d_pendingReqPhase) + Assert(a.getKind() == b.getKind()); + if (d_extt.hasFunctionKind(a.getKind())) { - Trace("strings-pending") << "Require phase : " << prp.first - << ", polarity = " << prp.second << std::endl; - d_out.requirePhase(prp.first, prp.second); + d_extt.markCongruent(a, b); } - d_pendingLem.clear(); - d_pendingReqPhase.clear(); } -bool InferenceManager::hasProcessed() const +void InferenceManager::markReduced(Node n, bool contextDepend) { - return d_state.isInConflict() || !d_pendingLem.empty() || !d_pending.empty(); + d_extt.markReduced(n, contextDepend); } -Node InferenceManager::mkExplain(const std::vector<Node>& a) const +void InferenceManager::processConflict(const InferInfo& ii) { - std::vector<Node> noExplain; - return mkExplain(a, noExplain); + Assert(!d_state.isInConflict()); + // setup the fact to reproduce the proof in the call below + d_statistics.d_inferences << ii.d_id; + if (d_ipc != nullptr) + { + d_ipc->notifyFact(ii); + } + // make the trust node + TrustNode tconf = mkConflictExp(ii.d_ant, d_ipc.get()); + Assert(tconf.getKind() == TrustNodeKind::CONFLICT); + Trace("strings-assert") << "(assert (not " << tconf.getNode() + << ")) ; conflict " << ii.d_id << std::endl; + // send the trusted conflict + trustedConflict(tconf); } -Node InferenceManager::mkExplain(const std::vector<Node>& a, - const std::vector<Node>& noExplain) const +bool InferenceManager::processFact(InferInfo& ii) { - std::vector<TNode> antec_exp; - // copy to processing vector - std::vector<Node> aconj; - for (const Node& ac : a) - { - utils::flattenOp(AND, ac, aconj); - } - for (const Node& apc : aconj) + // Get the fact(s). There are multiple facts if the conclusion is an AND + std::vector<Node> facts; + if (ii.d_conc.getKind() == AND) { - if (std::find(noExplain.begin(), noExplain.end(), apc) != noExplain.end()) + for (const Node& cc : ii.d_conc) { - 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; + facts.push_back(cc); } - Assert(apc.getKind() != AND); - Debug("strings-explain") << "Add to explanation " << apc << std::endl; - if (apc.getKind() == NOT && apc[0].getKind() == EQUAL) - { - Assert(d_ee->hasTerm(apc[0][0])); - Assert(d_ee->hasTerm(apc[0][1])); - // ensure that we are ready to explain the disequality - AlwaysAssert(d_ee->areDisequal(apc[0][0], apc[0][1], true)); - } - Assert(apc.getKind() != EQUAL || d_ee->areEqual(apc[0], apc[1])); - // now, explain - explain(apc, antec_exp); } - Node ant; - if (antec_exp.empty()) + else { - ant = d_true; + facts.push_back(ii.d_conc); } - else if (antec_exp.size() == 1) + Trace("strings-assert") << "(assert (=> " << ii.getAntecedant() << " " + << ii.d_conc << ")) ; fact " << ii.d_id << std::endl; + Trace("strings-lemma") << "Strings::Fact: " << ii.d_conc << " from " + << ii.getAntecedant() << " by " << ii.d_id + << std::endl; + std::vector<Node> exp; + for (const Node& ec : ii.d_ant) { - ant = antec_exp[0]; + utils::flattenOp(AND, ec, exp); } - else + bool ret = false; + // convert for each fact + for (const Node& fact : facts) { - ant = NodeManager::currentNM()->mkNode(AND, antec_exp); + ii.d_conc = fact; + d_statistics.d_inferences << ii.d_id; + bool polarity = fact.getKind() != NOT; + TNode atom = polarity ? fact : fact[0]; + bool curRet = false; + if (d_ipc != nullptr) + { + // ensure the proof generator is ready to explain this fact in the + // current SAT context + d_ipc->notifyFact(ii); + // now, assert the internal fact with d_ipc as proof generator + curRet = assertInternalFact(atom, polarity, exp, d_ipc.get()); + } + else + { + Node cexp = utils::mkAnd(exp); + // without proof generator + curRet = assertInternalFact(atom, polarity, cexp); + } + ret = ret || curRet; + // may be in conflict + if (d_state.isInConflict()) + { + break; + } } - return ant; + return ret; } -void InferenceManager::explain(TNode literal, - std::vector<TNode>& assumptions) const +bool InferenceManager::processLemma(InferInfo& ii) { - Debug("strings-explain") << "Explain " << literal << " " - << d_state.isInConflict() << std::endl; - bool polarity = literal.getKind() != NOT; - TNode atom = polarity ? literal : literal[0]; - std::vector<TNode> tassumptions; - if (atom.getKind() == EQUAL) + Assert(!ii.isTrivial()); + Assert(!ii.isConflict()); + // set up the explanation and no-explanation + std::vector<Node> exp; + for (const Node& ec : ii.d_ant) { - if (atom[0] != atom[1]) - { - Assert(d_ee->hasTerm(atom[0])); - Assert(d_ee->hasTerm(atom[1])); - d_ee->explainEquality(atom[0], atom[1], polarity, tassumptions); - } + utils::flattenOp(AND, ec, exp); } - else + std::vector<Node> noExplain; + if (!options::stringRExplainLemmas()) { - d_ee->explainPredicate(atom, polarity, tassumptions); + // if we aren't regressing the explanation, we add all literals to + // noExplain and ignore ii.d_ant. + noExplain.insert(noExplain.end(), exp.begin(), exp.end()); } - for (const TNode a : tassumptions) + else { - if (std::find(assumptions.begin(), assumptions.end(), a) - == assumptions.end()) + // otherwise, the no-explain literals are those provided + for (const Node& ecn : ii.d_noExplain) { - assumptions.push_back(a); + utils::flattenOp(AND, ecn, noExplain); } } - if (Debug.isOn("strings-explain-debug")) + // ensure that the proof generator is ready to explain the final conclusion + // of the lemma (ii.d_conc). + d_statistics.d_inferences << ii.d_id; + if (d_ipc != nullptr) + { + d_ipc->notifyFact(ii); + } + TrustNode tlem = mkLemmaExp(ii.d_conc, exp, noExplain, d_ipc.get()); + Trace("strings-pending") << "Process pending lemma : " << tlem.getNode() + << std::endl; + + // Process the side effects of the inference info. + // Register the new skolems from this inference. We register them here + // (lazily), since this is the moment when we have decided to process the + // inference. + for (const std::pair<const LengthStatus, std::vector<Node> >& sks : + ii.d_new_skolem) { - Debug("strings-explain-debug") - << "Explanation for " << literal << " was " << std::endl; - for (const TNode a : tassumptions) + for (const Node& n : sks.second) { - Debug("strings-explain-debug") << " " << a << std::endl; + d_termReg.registerTermAtomic(n, sks.first); } } -} - -void InferenceManager::markCongruent(Node a, Node b) -{ - Assert(a.getKind() == b.getKind()); - if (d_extt.hasFunctionKind(a.getKind())) + LemmaProperty p = LemmaProperty::NONE; + if (ii.d_id == Inference::REDUCTION) { - d_extt.markCongruent(a, b); + p |= LemmaProperty::NEEDS_JUSTIFY; } -} + Trace("strings-assert") << "(assert " << tlem.getNode() << ") ; lemma " + << ii.d_id << std::endl; + Trace("strings-lemma") << "Strings::Lemma: " << tlem.getNode() << " by " + << ii.d_id << std::endl; + ++(d_statistics.d_lemmasInfer); -void InferenceManager::markReduced(Node n, bool contextDepend) -{ - d_extt.markReduced(n, contextDepend); + // call the trusted lemma, without caching + return trustedLemma(tlem, p, false); } } // namespace strings diff --git a/src/theory/strings/inference_manager.h b/src/theory/strings/inference_manager.h index 9abc776e6..3280281bd 100644 --- a/src/theory/strings/inference_manager.h +++ b/src/theory/strings/inference_manager.h @@ -23,9 +23,12 @@ #include "context/cdhashset.h" #include "context/context.h" #include "expr/node.h" +#include "expr/proof_node_manager.h" #include "theory/ext_theory.h" +#include "theory/inference_manager_buffered.h" #include "theory/output_channel.h" #include "theory/strings/infer_info.h" +#include "theory/strings/infer_proof_cons.h" #include "theory/strings/sequences_stats.h" #include "theory/strings/solver_state.h" #include "theory/strings/term_registry.h" @@ -66,10 +69,11 @@ namespace strings { * theory of strings, e.g. sendPhaseRequirement, setIncomplete, and * with the extended theory object e.g. markCongruent. */ -class InferenceManager : public TheoryInferenceManager +class InferenceManager : public InferenceManagerBuffered { typedef context::CDHashSet<Node, NodeHashFunction> NodeSet; typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap; + friend class InferInfo; public: InferenceManager(Theory& t, @@ -80,6 +84,15 @@ class InferenceManager : public TheoryInferenceManager ProofNodeManager* pnm); ~InferenceManager() {} + /** + * Do pending method. This processes all pending facts, lemmas and pending + * phase requests based on the policy of this manager. This means that + * we process the pending facts first and abort if in conflict. Otherwise, we + * process the pending lemmas and then the pending phase requirements. + * Notice that we process the pending lemmas even if there were facts. + */ + void doPending(); + /** send internal inferences * * This is called when we have inferred exp => conc, where exp is a set @@ -145,15 +158,17 @@ class InferenceManager : public TheoryInferenceManager * 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. + * @return true if the inference was not trivial (e.g. its conclusion did + * not rewrite to true). */ - void sendInference(const std::vector<Node>& exp, + bool sendInference(const std::vector<Node>& exp, const std::vector<Node>& noExplain, Node eq, Inference infer, bool isRev = false, bool asLemma = false); /** same as above, but where noExplain is empty */ - void sendInference(const std::vector<Node>& exp, + bool sendInference(const std::vector<Node>& exp, Node eq, Inference infer, bool isRev = false, @@ -171,7 +186,7 @@ class InferenceManager : public TheoryInferenceManager * If the flag asLemma is true, then this method will send a lemma instead * of a fact whenever applicable. */ - void sendInference(const InferInfo& ii, bool asLemma = false); + void sendInference(InferInfo& ii, bool asLemma = false); /** Send split * * This requests that ( a = b V a != b ) is sent on the output channel as a @@ -186,17 +201,6 @@ class InferenceManager : public TheoryInferenceManager * otherwise. A split is trivial if a=b rewrites to a constant. */ bool sendSplit(Node a, Node b, Inference infer, bool preq = true); - - /** Send phase requirement - * - * This method is called to indicate this class should send a phase - * requirement request to the output channel for literal lit to be - * decided with polarity pol. This requirement is processed at the same time - * lemmas are sent on the output channel of this class during this call to - * check. This means if the current lemmas of this class are abandoned (due - * to a conflict), the phase requirement is not processed. - */ - void sendPhaseRequirement(Node lit, bool pol); /** * Set that we are incomplete for the current set of assertions (in other * words, we must answer "unknown" instead of "sat"); this calls the output @@ -213,61 +217,13 @@ class InferenceManager : public TheoryInferenceManager /** Adds lit to the vector exp if it is non-null */ void addToExplanation(Node lit, std::vector<Node>& exp) const; //----------------------------end constructing antecedants - /** Do pending facts - * - * This method asserts pending facts (d_pending) with explanations - * (d_pendingExp) to the equality engine of the theory of strings via calls - * to assertPendingFact. - * - * It terminates early if a conflict is encountered, for instance, by - * equality reasoning within the equality engine. - * - * Regardless of whether a conflict is encountered, the vector d_pending - * and map d_pendingExp are cleared. - */ - void doPendingFacts(); - /** Do pending lemmas - * - * This method flushes all pending lemmas (d_pending_lem) to the output - * channel of theory of strings. - * - * Like doPendingFacts, this function will terminate early if a conflict - * has already been encountered by the theory of strings. The vector - * d_pending_lem is cleared regardless of whether a conflict is discovered. - * - * Notice that as a result of the above design, some lemmas may be "dropped" - * if a conflict is discovered in between when a lemma is added to the - * pending vector of this class (via a sendInference call). Lemmas - * e.g. those that are required for initialization should not be sent via - * this class, since they should never be dropped. - */ - void doPendingLemmas(); /** * Have we processed an inference during this call to check? In particular, * this returns true if we have a pending fact or lemma, or have encountered * a conflict. */ bool hasProcessed() const; - /** Do we have a pending fact to add to the equality engine? */ - bool hasPendingFact() const { return !d_pending.empty(); } - /** Do we have a pending lemma to send on the output channel? */ - bool hasPendingLemma() const { return !d_pendingLem.empty(); } - /** make explanation - * - * This returns a node corresponding to the explanation of formulas in a, - * interpreted conjunctively. The returned node is a conjunction of literals - * that have been asserted to the equality engine. - */ - Node mkExplain(const std::vector<Node>& a) 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. - */ - void explain(TNode literal, std::vector<TNode>& assumptions) const; // ------------------------------------------------- extended theory /** * Mark that terms a and b are congruent in the current context. @@ -284,7 +240,18 @@ class InferenceManager : public TheoryInferenceManager void markReduced(Node n, bool contextDepend = true); // ------------------------------------------------- end extended theory + /** + * Called when ii is ready to be processed as a conflict. This makes a + * trusted node whose generator is the underlying proof equality engine + * (if it exists), and sends it on the output channel. + */ + void processConflict(const InferInfo& ii); + private: + /** Called when ii is ready to be processed as a fact */ + bool processFact(InferInfo& ii); + /** Called when ii is ready to be processed as a lemma */ + bool processLemma(InferInfo& ii); /** Reference to the solver state of the theory of strings. */ SolverState& d_state; /** Reference to the term registry of theory of strings */ @@ -293,21 +260,13 @@ class InferenceManager : public TheoryInferenceManager ExtTheory& d_extt; /** Reference to the statistics for the theory of strings/sequences. */ SequencesStatistics& d_statistics; - + /** Conversion from inferences to proofs */ + std::unique_ptr<InferProofCons> d_ipc; /** Common constants */ Node d_true; Node d_false; Node d_zero; Node d_one; - /** - * The list of pending literals to assert to the equality engine along with - * their explanation. - */ - std::vector<InferInfo> d_pending; - /** A map from literals to their pending phase requirement */ - std::map<Node, bool> d_pendingReqPhase; - /** A list of pending lemmas to be sent on the output channel. */ - std::vector<InferInfo> d_pendingLem; }; } // namespace strings diff --git a/src/theory/strings/sequences_stats.cpp b/src/theory/strings/sequences_stats.cpp index 80221cbcc..fe6bc548e 100644 --- a/src/theory/strings/sequences_stats.cpp +++ b/src/theory/strings/sequences_stats.cpp @@ -32,7 +32,7 @@ SequencesStatistics::SequencesStatistics() d_regexpUnfoldingsNeg("theory::strings::regexpUnfoldingsNeg"), d_rewrites("theory::strings::rewrites"), d_conflictsEqEngine("theory::strings::conflictsEqEngine", 0), - d_conflictsEagerPrefix("theory::strings::conflictsEagerPrefix", 0), + d_conflictsEager("theory::strings::conflictsEager", 0), d_conflictsInfer("theory::strings::conflictsInfer", 0), d_lemmasEagerPreproc("theory::strings::lemmasEagerPreproc", 0), d_lemmasCmiSplit("theory::strings::lemmasCmiSplit", 0), @@ -51,7 +51,7 @@ SequencesStatistics::SequencesStatistics() smtStatisticsRegistry()->registerStat(&d_regexpUnfoldingsNeg); smtStatisticsRegistry()->registerStat(&d_rewrites); smtStatisticsRegistry()->registerStat(&d_conflictsEqEngine); - smtStatisticsRegistry()->registerStat(&d_conflictsEagerPrefix); + smtStatisticsRegistry()->registerStat(&d_conflictsEager); smtStatisticsRegistry()->registerStat(&d_conflictsInfer); smtStatisticsRegistry()->registerStat(&d_lemmasEagerPreproc); smtStatisticsRegistry()->registerStat(&d_lemmasCmiSplit); @@ -72,7 +72,7 @@ SequencesStatistics::~SequencesStatistics() smtStatisticsRegistry()->unregisterStat(&d_regexpUnfoldingsNeg); smtStatisticsRegistry()->unregisterStat(&d_rewrites); smtStatisticsRegistry()->unregisterStat(&d_conflictsEqEngine); - smtStatisticsRegistry()->unregisterStat(&d_conflictsEagerPrefix); + smtStatisticsRegistry()->unregisterStat(&d_conflictsEager); smtStatisticsRegistry()->unregisterStat(&d_conflictsInfer); smtStatisticsRegistry()->unregisterStat(&d_lemmasEagerPreproc); smtStatisticsRegistry()->unregisterStat(&d_lemmasCmiSplit); diff --git a/src/theory/strings/sequences_stats.h b/src/theory/strings/sequences_stats.h index b205310ed..e35d951f7 100644 --- a/src/theory/strings/sequences_stats.h +++ b/src/theory/strings/sequences_stats.h @@ -92,8 +92,8 @@ class SequencesStatistics //--------------- conflicts, partition of calls to OutputChannel::conflict /** Number of equality engine conflicts */ IntStat d_conflictsEqEngine; - /** Number of eager prefix conflicts */ - IntStat d_conflictsEagerPrefix; + /** Number of eager conflicts */ + IntStat d_conflictsEager; /** Number of inference conflicts */ IntStat d_conflictsInfer; //--------------- end of conflicts diff --git a/src/theory/strings/solver_state.cpp b/src/theory/strings/solver_state.cpp index 426d37392..40edb88cf 100644 --- a/src/theory/strings/solver_state.cpp +++ b/src/theory/strings/solver_state.cpp @@ -28,9 +28,10 @@ namespace strings { SolverState::SolverState(context::Context* c, context::UserContext* u, Valuation& v) - : TheoryState(c, u, v), d_eeDisequalities(c), d_pendingConflict(c) + : TheoryState(c, u, v), d_eeDisequalities(c), d_pendingConflictSet(c, false) { d_zero = NodeManager::currentNM()->mkConst(Rational(0)); + d_false = NodeManager::currentNM()->mkConst(false); } SolverState::~SolverState() @@ -95,12 +96,12 @@ void SolverState::eqNotifyMerge(TNode t1, TNode t2) } if (!e2->d_prefixC.get().isNull()) { - setPendingConflictWhen( + setPendingPrefixConflictWhen( e1->addEndpointConst(e2->d_prefixC, Node::null(), false)); } if (!e2->d_suffixC.get().isNull()) { - setPendingConflictWhen( + setPendingPrefixConflictWhen( e1->addEndpointConst(e2->d_suffixC, Node::null(), true)); } if (e2->d_cardinalityLemK.get() > e1->d_cardinalityLemK.get()) @@ -161,7 +162,7 @@ void SolverState::addEndpointsToEqcInfo(Node t, Node concat, Node eqc) Trace("strings-eager-pconf-debug") << "New term: " << concat << " for " << t << " with prefix " << c << " (" << (r == 1) << ")" << std::endl; - setPendingConflictWhen(ei->addEndpointConst(t, c, r == 1)); + setPendingPrefixConflictWhen(ei->addEndpointConst(t, c, r == 1)); } } } @@ -227,15 +228,38 @@ bool SolverState::isEqualEmptyWord(Node s, Node& emps) return false; } -void SolverState::setPendingConflictWhen(Node conf) +void SolverState::setPendingPrefixConflictWhen(Node conf) { - if (!conf.isNull() && d_pendingConflict.get().isNull()) + if (conf.isNull() || d_pendingConflictSet.get()) { - d_pendingConflict = conf; + return; } + InferInfo iiPrefixConf; + iiPrefixConf.d_id = Inference::PREFIX_CONFLICT; + iiPrefixConf.d_conc = d_false; + utils::flattenOp(AND, conf, iiPrefixConf.d_ant); + setPendingConflict(iiPrefixConf); } -Node SolverState::getPendingConflict() const { return d_pendingConflict; } +void SolverState::setPendingConflict(InferInfo& ii) +{ + if (!d_pendingConflictSet.get()) + { + d_pendingConflict = ii; + } +} + +bool SolverState::hasPendingConflict() const { return d_pendingConflictSet; } + +bool SolverState::getPendingConflict(InferInfo& ii) const +{ + if (d_pendingConflictSet) + { + ii = d_pendingConflict; + return true; + } + return false; +} std::pair<bool, Node> SolverState::entailmentCheck(options::TheoryOfMode mode, TNode lit) diff --git a/src/theory/strings/solver_state.h b/src/theory/strings/solver_state.h index e6839760f..291a15feb 100644 --- a/src/theory/strings/solver_state.h +++ b/src/theory/strings/solver_state.h @@ -23,6 +23,7 @@ #include "context/context.h" #include "expr/node.h" #include "theory/strings/eqc_info.h" +#include "theory/strings/infer_info.h" #include "theory/theory_model.h" #include "theory/theory_state.h" #include "theory/uf/equality_engine.h" @@ -66,7 +67,7 @@ class SolverState : public TheoryState void eqNotifyDisequal(TNode t1, TNode t2, TNode reason); //-------------------------------------- end notifications for equalities //------------------------------------------ conflicts - /** set pending conflict + /** set pending prefix conflict * * If conf is non-null, this is called when conf is a conjunction of literals * that hold in the current context that are unsatisfiable. It is set as the @@ -76,9 +77,16 @@ class SolverState : public TheoryState * during a merge operation, when the equality engine is not in a state to * provide explanations. */ - void setPendingConflictWhen(Node conf); + void setPendingPrefixConflictWhen(Node conf); + /** + * Set pending conflict, infer info version. Called when we are in conflict + * based on the inference ii. This generalizes the above method. + */ + void setPendingConflict(InferInfo& ii); + /** return true if we have a pending conflict */ + bool hasPendingConflict() const; /** get the pending conflict, or null if none exist */ - Node getPendingConflict() const; + bool getPendingConflict(InferInfo& ii) const; //------------------------------------------ end conflicts /** get length with explanation * @@ -152,13 +160,16 @@ class SolverState : public TheoryState private: /** Common constants */ Node d_zero; + Node d_false; /** * The (SAT-context-dependent) list of disequalities that have been asserted * to the equality engine above. */ NodeList d_eeDisequalities; /** The pending conflict if one exists */ - context::CDO<Node> d_pendingConflict; + context::CDO<bool> d_pendingConflictSet; + /** The pending conflict, valid if the above flag is true */ + InferInfo d_pendingConflict; /** Map from representatives to their equivalence class information */ std::map<Node, EqcInfo*> d_eqcInfo; }; /* class TheoryStrings */ diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 2b2c25333..1dc19deb1 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -15,6 +15,7 @@ #include "theory/strings/theory_strings.h" #include "expr/kind.h" +#include "options/smt_options.h" #include "options/strings_options.h" #include "options/theory_options.h" #include "smt/logic_exception.h" @@ -44,7 +45,7 @@ TheoryStrings::TheoryStrings(context::Context* c, d_notify(*this), d_statistics(), d_state(c, u, d_valuation), - d_termReg(d_state, out, d_statistics, nullptr), + d_termReg(d_state, out, d_statistics, pnm), d_extTheoryCb(), d_extTheory(d_extTheoryCb, c, u, out), d_im(*this, d_state, d_termReg, d_extTheory, d_statistics, pnm), @@ -194,17 +195,7 @@ bool TheoryStrings::propagateLit(TNode literal) TrustNode TheoryStrings::explain(TNode literal) { Debug("strings-explain") << "explain called on " << literal << std::endl; - std::vector< TNode > assumptions; - d_im.explain(literal, assumptions); - Node ret; - if( assumptions.empty() ){ - ret = d_true; - }else if( assumptions.size()==1 ){ - ret = assumptions[0]; - }else{ - ret = NodeManager::currentNM()->mkNode(kind::AND, assumptions); - } - return TrustNode::mkTrustPropExp(literal, ret, nullptr); + return d_im.explainLit(literal); } void TheoryStrings::presolve() { @@ -618,22 +609,18 @@ void TheoryStrings::notifyFact(TNode atom, } } // process pending conflicts due to reasoning about endpoints - if (!d_state.isInConflict()) + if (!d_state.isInConflict() && d_state.hasPendingConflict()) { - Node pc = d_state.getPendingConflict(); - if (!pc.isNull()) - { - std::vector<Node> a; - a.push_back(pc); - Trace("strings-pending") - << "Process pending conflict " << pc << std::endl; - Node conflictNode = d_im.mkExplain(a); - Trace("strings-conflict") - << "CONFLICT: Eager prefix : " << conflictNode << std::endl; - ++(d_statistics.d_conflictsEagerPrefix); - d_im.conflict(conflictNode); - return; - } + InferInfo iiPendingConf; + d_state.getPendingConflict(iiPendingConf); + Trace("strings-pending") + << "Process pending conflict " << iiPendingConf.d_ant << std::endl; + Trace("strings-conflict") + << "CONFLICT: Eager : " << iiPendingConf.d_ant << std::endl; + ++(d_statistics.d_conflictsEager); + // call the inference manager to send the conflict + d_im.processConflict(iiPendingConf); + return; } Trace("strings-pending-debug") << " Now collect terms" << std::endl; // Collect extended function terms in the atom. Notice that we must register @@ -693,34 +680,41 @@ void TheoryStrings::postCheck(Effort e) Trace("strings-eqc") << std::endl; } ++(d_statistics.d_checkRuns); - bool addedLemma = false; - bool addedFact; + bool sentLemma = false; + bool hadPending = false; Trace("strings-check") << "Full effort check..." << std::endl; do{ + d_im.reset(); ++(d_statistics.d_strategyRuns); Trace("strings-check") << " * Run strategy..." << std::endl; runStrategy(e); + // remember if we had pending facts or lemmas + hadPending = d_im.hasPending(); // Send the facts *and* the lemmas. We send lemmas regardless of whether // we send facts since some lemmas cannot be dropped. Other lemmas are // otherwise avoided by aborting the strategy when a fact is ready. - addedFact = d_im.hasPendingFact(); - addedLemma = d_im.hasPendingLemma(); - d_im.doPendingFacts(); - d_im.doPendingLemmas(); + d_im.doPending(); + // Did we successfully send a lemma? Notice that if hasPending = true + // and sentLemma = false, then the above call may have: + // (1) had no pending lemmas, but successfully processed pending facts, + // (2) unsuccessfully processed pending lemmas. + // In either case, we repeat the strategy if we are not in conflict. + sentLemma = d_im.hasSentLemma(); if (Trace.isOn("strings-check")) { Trace("strings-check") << " ...finish run strategy: "; - Trace("strings-check") << (addedFact ? "addedFact " : ""); - Trace("strings-check") << (addedLemma ? "addedLemma " : ""); + Trace("strings-check") << (hadPending ? "hadPending " : ""); + Trace("strings-check") << (sentLemma ? "sentLemma " : ""); Trace("strings-check") << (d_state.isInConflict() ? "conflict " : ""); - if (!addedFact && !addedLemma && !d_state.isInConflict()) + if (!hadPending && !sentLemma && !d_state.isInConflict()) { Trace("strings-check") << "(none)"; } Trace("strings-check") << std::endl; } - // repeat if we did not add a lemma or conflict - } while (!d_state.isInConflict() && !addedLemma && addedFact); + // repeat if we did not add a lemma or conflict, and we had pending + // facts or lemmas. + } while (!d_state.isInConflict() && !sentLemma && hadPending); } Trace("strings-check") << "Theory of strings, done check : " << e << std::endl; Assert(!d_im.hasPendingFact()); @@ -736,17 +730,14 @@ bool TheoryStrings::needsCheckLastEffort() { /** Conflict when merging two constants */ void TheoryStrings::conflict(TNode a, TNode b){ - if (!d_state.isInConflict()) + if (d_state.isInConflict()) { - Debug("strings-conflict") << "Making conflict..." << std::endl; - d_state.notifyInConflict(); - TrustNode conflictNode = explain(a.eqNode(b)); - Trace("strings-conflict") - << "CONFLICT: Eq engine conflict : " << conflictNode.getNode() - << std::endl; - ++(d_statistics.d_conflictsEqEngine); - d_out->conflict(conflictNode.getNode()); + // already in conflict + return; } + d_im.conflictEqConstantMerge(a, b); + Trace("strings-conflict") << "CONFLICT: Eq engine conflict" << std::endl; + ++(d_statistics.d_conflictsEqEngine); } void TheoryStrings::eqNotifyNewClass(TNode t){ @@ -967,7 +958,8 @@ void TheoryStrings::checkCodes() Node eqn = c1[0].eqNode(c2[0]); // str.code(x)==-1 V str.code(x)!=str.code(y) V x==y Node inj_lem = nm->mkNode(kind::OR, eq_no, deq, eqn); - d_im.sendPhaseRequirement(deq, false); + deq = Rewriter::rewrite(deq); + d_im.addPendingPhaseRequirement(deq, false); std::vector<Node> emptyVec; d_im.sendInference(emptyVec, inj_lem, Inference::CODE_INJ); } |