diff options
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/strings/inference_manager.cpp | 111 | ||||
-rw-r--r-- | src/theory/strings/inference_manager.h | 35 | ||||
-rw-r--r-- | src/theory/strings/theory_strings.cpp | 124 | ||||
-rw-r--r-- | src/theory/strings/theory_strings.h | 28 |
4 files changed, 108 insertions, 190 deletions
diff --git a/src/theory/strings/inference_manager.cpp b/src/theory/strings/inference_manager.cpp index dce038fbf..811c040f3 100644 --- a/src/theory/strings/inference_manager.cpp +++ b/src/theory/strings/inference_manager.cpp @@ -28,19 +28,17 @@ namespace CVC4 { namespace theory { namespace strings { -InferenceManager::InferenceManager(context::Context* c, - context::UserContext* u, +InferenceManager::InferenceManager(Theory& t, SolverState& s, TermRegistry& tr, ExtTheory& e, - OutputChannel& out, - SequencesStatistics& statistics) - : d_state(s), + SequencesStatistics& statistics, + ProofNodeManager* pnm) + : TheoryInferenceManager(t, s, pnm), + d_state(s), d_termReg(tr), d_extt(e), - d_out(out), - d_statistics(statistics), - d_keep(c) + d_statistics(statistics) { NodeManager* nm = NodeManager::currentNM(); d_zero = nm->mkConst(Rational(0)); @@ -49,14 +47,6 @@ InferenceManager::InferenceManager(context::Context* c, d_false = nm->mkConst(false); } -void InferenceManager::sendAssumption(TNode lit) -{ - bool polarity = lit.getKind() != kind::NOT; - TNode atom = polarity ? lit : lit[0]; - // assert pending fact - assertPendingFact(atom, polarity, lit); -} - bool InferenceManager::sendInternalInference(std::vector<Node>& exp, Node conc, Inference infer) @@ -299,7 +289,7 @@ void InferenceManager::doPendingFacts() TNode atom = polarity ? fact : fact[0]; // no double negation or double (conjunctive) conclusions Assert(atom.getKind() != NOT && atom.getKind() != AND); - assertPendingFact(atom, polarity, exp); + assertInternalFact(atom, polarity, exp); } } else @@ -308,13 +298,8 @@ void InferenceManager::doPendingFacts() TNode atom = polarity ? facts : facts[0]; // no double negation or double (conjunctive) conclusions Assert(atom.getKind() != NOT && atom.getKind() != AND); - assertPendingFact(atom, polarity, exp); + assertInternalFact(atom, polarity, exp); } - // Must reference count the equality and its explanation, which is not done - // by the equality engine. Notice that we do not need to do this for - // external assertions, which enter as facts through sendAssumption. - d_keep.insert(facts); - d_keep.insert(exp); i++; } d_pending.clear(); @@ -392,68 +377,6 @@ void InferenceManager::doPendingLemmas() d_pendingReqPhase.clear(); } -void InferenceManager::assertPendingFact(Node atom, bool polarity, Node exp) -{ - eq::EqualityEngine* ee = d_state.getEqualityEngine(); - Trace("strings-pending") << "Assert pending fact : " << atom << " " - << polarity << " from " << exp << std::endl; - Assert(atom.getKind() != OR) << "Infer error: a split."; - if (atom.getKind() == EQUAL) - { - // we must ensure these terms are registered - Trace("strings-pending-debug") << " Register term" << std::endl; - for (const Node& t : atom) - { - // terms in the equality engine are already registered, hence skip - // currently done for only string-like terms, but this could potentially - // be avoided. - if (!ee->hasTerm(t) && t.getType().isStringLike()) - { - d_termReg.registerTerm(t, 0); - } - } - Trace("strings-pending-debug") << " Now assert equality" << std::endl; - ee->assertEquality(atom, polarity, exp); - Trace("strings-pending-debug") << " Finished assert equality" << std::endl; - } - else - { - ee->assertPredicate(atom, polarity, exp); - if (atom.getKind() == STRING_IN_REGEXP) - { - if (polarity && atom[1].getKind() == REGEXP_CONCAT) - { - Node eqc = ee->getRepresentative(atom[0]); - d_state.addEndpointsToEqcInfo(atom, atom[1], eqc); - } - } - } - // process the conflict - if (!d_state.isInConflict()) - { - 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 = mkExplain(a); - d_state.notifyInConflict(); - Trace("strings-conflict") - << "CONFLICT: Eager prefix : " << conflictNode << std::endl; - ++(d_statistics.d_conflictsEagerPrefix); - d_out.conflict(conflictNode); - } - } - Trace("strings-pending-debug") << " Now collect terms" << std::endl; - // Collect extended function terms in the atom. Notice that we must register - // all extended functions occurring in assertions and shared terms. We - // make a similar call to registerTermRec in TheoryStrings::addSharedTerm. - d_extt.registerTermRec(atom); - Trace("strings-pending-debug") << " Finished collect terms" << std::endl; -} - bool InferenceManager::hasProcessed() const { return d_state.isInConflict() || !d_pendingLem.empty() || !d_pending.empty(); @@ -475,7 +398,6 @@ Node InferenceManager::mkExplain(const std::vector<Node>& a, { utils::flattenOp(AND, ac, aconj); } - eq::EqualityEngine* ee = d_state.getEqualityEngine(); for (const Node& apc : aconj) { if (std::find(noExplain.begin(), noExplain.end(), apc) != noExplain.end()) @@ -492,12 +414,12 @@ Node InferenceManager::mkExplain(const std::vector<Node>& a, Debug("strings-explain") << "Add to explanation " << apc << std::endl; if (apc.getKind() == NOT && apc[0].getKind() == EQUAL) { - Assert(ee->hasTerm(apc[0][0])); - Assert(ee->hasTerm(apc[0][1])); + Assert(d_ee->hasTerm(apc[0][0])); + Assert(d_ee->hasTerm(apc[0][1])); // ensure that we are ready to explain the disequality - AlwaysAssert(ee->areDisequal(apc[0][0], apc[0][1], true)); + AlwaysAssert(d_ee->areDisequal(apc[0][0], apc[0][1], true)); } - Assert(apc.getKind() != EQUAL || ee->areEqual(apc[0], apc[1])); + Assert(apc.getKind() != EQUAL || d_ee->areEqual(apc[0], apc[1])); // now, explain explain(apc, antec_exp); } @@ -522,7 +444,6 @@ void InferenceManager::explain(TNode literal, { Debug("strings-explain") << "Explain " << literal << " " << d_state.isInConflict() << std::endl; - eq::EqualityEngine* ee = d_state.getEqualityEngine(); bool polarity = literal.getKind() != NOT; TNode atom = polarity ? literal : literal[0]; std::vector<TNode> tassumptions; @@ -530,14 +451,14 @@ void InferenceManager::explain(TNode literal, { if (atom[0] != atom[1]) { - Assert(ee->hasTerm(atom[0])); - Assert(ee->hasTerm(atom[1])); - ee->explainEquality(atom[0], atom[1], polarity, tassumptions); + Assert(d_ee->hasTerm(atom[0])); + Assert(d_ee->hasTerm(atom[1])); + d_ee->explainEquality(atom[0], atom[1], polarity, tassumptions); } } else { - ee->explainPredicate(atom, polarity, tassumptions); + d_ee->explainPredicate(atom, polarity, tassumptions); } for (const TNode a : tassumptions) { diff --git a/src/theory/strings/inference_manager.h b/src/theory/strings/inference_manager.h index 016891737..dc46f1683 100644 --- a/src/theory/strings/inference_manager.h +++ b/src/theory/strings/inference_manager.h @@ -29,6 +29,7 @@ #include "theory/strings/sequences_stats.h" #include "theory/strings/solver_state.h" #include "theory/strings/term_registry.h" +#include "theory/theory_inference_manager.h" #include "theory/uf/equality_engine.h" namespace CVC4 { @@ -65,28 +66,20 @@ namespace strings { * theory of strings, e.g. sendPhaseRequirement, setIncomplete, and * with the extended theory object e.g. markCongruent. */ -class InferenceManager +class InferenceManager : public TheoryInferenceManager { typedef context::CDHashSet<Node, NodeHashFunction> NodeSet; typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap; public: - InferenceManager(context::Context* c, - context::UserContext* u, + InferenceManager(Theory& t, SolverState& s, TermRegistry& tr, ExtTheory& e, - OutputChannel& out, - SequencesStatistics& statistics); + SequencesStatistics& statistics, + ProofNodeManager* pnm); ~InferenceManager() {} - /** send assumption - * - * This is called when a fact is asserted to TheoryStrings. It adds lit - * to the equality engine maintained by this class immediately. - */ - void sendAssumption(TNode lit); - /** send internal inferences * * This is called when we have inferred exp => conc, where exp is a set @@ -292,23 +285,12 @@ class InferenceManager // ------------------------------------------------- end extended theory private: - /** assert pending fact - * - * This asserts atom with polarity to the equality engine of this class, - * where exp is the explanation of why (~) atom holds. - * - * This call may trigger further initialization steps involving the terms - * of atom, including calls to registerTerm. - */ - void assertPendingFact(Node atom, bool polarity, Node exp); /** Reference to the solver state of the theory of strings. */ SolverState& d_state; /** Reference to the term registry of theory of strings */ TermRegistry& d_termReg; /** the extended theory object for the theory of strings */ ExtTheory& d_extt; - /** A reference to the output channel of the theory of strings. */ - OutputChannel& d_out; /** Reference to the statistics for the theory of strings/sequences. */ SequencesStatistics& d_statistics; @@ -326,13 +308,6 @@ class InferenceManager std::map<Node, bool> d_pendingReqPhase; /** A list of pending lemmas to be sent on the output channel. */ std::vector<InferInfo> d_pendingLem; - /** - * The keep set of this class. This set is maintained to ensure that - * facts and their explanations are ref-counted. Since facts and their - * explanations are SAT-context-dependent, this set is also - * SAT-context-dependent. - */ - NodeSet d_keep; }; } // namespace strings diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 846f9240d..3e60cbc44 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -46,7 +46,7 @@ TheoryStrings::TheoryStrings(context::Context* c, d_state(c, u, d_valuation), d_termReg(d_state, out, d_statistics, nullptr), d_extTheory(this), - d_im(c, u, d_state, d_termReg, d_extTheory, out, d_statistics), + d_im(*this, d_state, d_termReg, d_extTheory, d_statistics, pnm), d_rewriter(&d_statistics.d_rewrites), d_bsolver(d_state, d_im), d_csolver(d_state, d_im, d_termReg, d_bsolver), @@ -83,6 +83,8 @@ TheoryStrings::TheoryStrings(context::Context* c, } // use the state object as the official theory state d_theoryState = &d_state; + // use the inference manager as the official inference manager + d_inferManager = &d_im; } TheoryStrings::~TheoryStrings() { @@ -165,23 +167,6 @@ void TheoryStrings::notifySharedTerm(TNode t) Debug("strings") << "TheoryStrings::notifySharedTerm() finished" << std::endl; } -EqualityStatus TheoryStrings::getEqualityStatus(TNode a, TNode b) { - if (d_equalityEngine->hasTerm(a) && d_equalityEngine->hasTerm(b)) - { - if (d_equalityEngine->areEqual(a, b)) - { - // The terms are implied to be equal - return EQUALITY_TRUE; - } - if (d_equalityEngine->areDisequal(a, b, false)) - { - // The terms are implied to be dis-equal - return EQUALITY_FALSE; - } - } - return EQUALITY_UNKNOWN; -} - bool TheoryStrings::propagateLit(TNode literal) { Debug("strings-propagate") @@ -252,24 +237,10 @@ void TheoryStrings::presolve() { // MODEL GENERATION ///////////////////////////////////////////////////////////////////////////// -bool TheoryStrings::collectModelInfo(TheoryModel* m) +bool TheoryStrings::collectModelValues(TheoryModel* m, + const std::set<Node>& termSet) { - Trace("strings-model") << "TheoryStrings : Collect model info" << std::endl; - Trace("strings-model") << "TheoryStrings : assertEqualityEngine." << std::endl; - - std::set<Node> termSet; - - // Compute terms appearing in assertions and shared terms - const std::set<Kind>& irrKinds = m->getIrrelevantKinds(); - computeAssertedTerms(termSet, irrKinds); - // assert the (relevant) portion of the equality engine to the model - if (!m->assertEqualityEngine(d_equalityEngine, &termSet)) - { - Unreachable() - << "TheoryStrings::collectModelInfo: failed to assert equality engine" - << std::endl; - return false; - } + Trace("strings-model") << "TheoryStrings : Collect model values" << std::endl; std::map<TypeNode, std::unordered_set<Node, NodeHashFunction> > repSet; // Generate model @@ -654,25 +625,68 @@ TrustNode TheoryStrings::expandDefinition(Node node) return TrustNode::null(); } -void TheoryStrings::check(Effort e) { - if (done() && e<EFFORT_FULL) { - return; +bool TheoryStrings::preNotifyFact( + TNode atom, bool pol, TNode fact, bool isPrereg, bool isInternal) +{ + // this is only required for internal facts, others are already registered + if (isInternal && atom.getKind() == EQUAL) + { + // we must ensure these terms are registered + for (const Node& t : atom) + { + // terms in the equality engine are already registered, hence skip + // currently done for only string-like terms, but this could potentially + // be avoided. + if (!d_equalityEngine->hasTerm(t) && t.getType().isStringLike()) + { + d_termReg.registerTerm(t, 0); + } + } } + return false; +} - TimerStat::CodeTimer checkTimer(d_checkTime); - - // Trace("strings-process") << "Theory of strings, check : " << e << std::endl; - Trace("strings-check-debug") - << "Theory of strings, check : " << e << std::endl; - while (!done() && !d_state.isInConflict()) +void TheoryStrings::notifyFact(TNode atom, + bool polarity, + TNode fact, + bool isInternal) +{ + if (atom.getKind() == STRING_IN_REGEXP) { - // Get all the assertions - Assertion assertion = get(); - TNode fact = assertion.d_assertion; - - Trace("strings-assertion") << "get assertion: " << fact << endl; - d_im.sendAssumption(fact); + if (polarity && atom[1].getKind() == REGEXP_CONCAT) + { + Node eqc = d_equalityEngine->getRepresentative(atom[0]); + d_state.addEndpointsToEqcInfo(atom, atom[1], eqc); + } } + // process pending conflicts due to reasoning about endpoints + if (!d_state.isInConflict()) + { + 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; + } + } + Trace("strings-pending-debug") << " Now collect terms" << std::endl; + // Collect extended function terms in the atom. Notice that we must register + // all extended functions occurring in assertions and shared terms. We + // make a similar call to registerTermRec in TheoryStrings::addSharedTerm. + d_extTheory.registerTermRec(atom); + Trace("strings-pending-debug") << " Finished collect terms" << std::endl; +} + +void TheoryStrings::postCheck(Effort e) +{ d_im.doPendingFacts(); Assert(d_strat.isStrategyInit()); @@ -681,8 +695,10 @@ void TheoryStrings::check(Effort e) { { Trace("strings-check-debug") << "Theory of strings " << e << " effort check " << std::endl; - if(Trace.isOn("strings-eqc")) { - for( unsigned t=0; t<2; t++ ) { + if (Trace.isOn("strings-eqc")) + { + for (unsigned t = 0; t < 2; t++) + { eq::EqClassesIterator eqcs2_i = eq::EqClassesIterator(d_equalityEngine); Trace("strings-eqc") << (t==0 ? "STRINGS:" : "OTHER:") << std::endl; while( !eqcs2_i.isFinished() ){ @@ -726,7 +742,9 @@ void TheoryStrings::check(Effort e) { ++(d_statistics.d_strategyRuns); Trace("strings-check") << " * Run strategy..." << std::endl; runStrategy(e); - // flush the facts + // 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(); diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index f4aa0675c..0f59e73dc 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -97,27 +97,33 @@ class TheoryStrings : public Theory { void shutdown() override {} /** add shared term */ void notifySharedTerm(TNode n) override; - /** get equality status */ - EqualityStatus getEqualityStatus(TNode a, TNode b) override; /** preregister term */ void preRegisterTerm(TNode n) override; /** Expand definition */ TrustNode expandDefinition(Node n) override; - /** Check at effort e */ - void check(Effort e) override; - /** needs check last effort */ + //--------------------------------- standard check + /** Do we need a check call at last call effort? */ bool needsCheckLastEffort() override; + bool preNotifyFact(TNode atom, + bool pol, + TNode fact, + bool isPrereg, + bool isInternal) override; + void notifyFact(TNode atom, bool pol, TNode fact, bool isInternal) override; + /** Post-check, called after the fact queue of the theory is processed. */ + void postCheck(Effort level) override; + //--------------------------------- end standard check + /** propagate method */ + bool propagateLit(TNode literal); /** Conflict when merging two constants */ void conflict(TNode a, TNode b); /** called when a new equivalence class is created */ void eqNotifyNewClass(TNode t); /** preprocess rewrite */ TrustNode ppRewrite(TNode atom) override; - /** - * Get all relevant information in this theory regarding the current - * model. Return false if a contradiction is discovered. - */ - bool collectModelInfo(TheoryModel* m) override; + /** Collect model values in m based on the relevant terms given by termSet */ + bool collectModelValues(TheoryModel* m, + const std::set<Node>& termSet) override; private: /** NotifyClass for equality engine */ @@ -171,8 +177,6 @@ class TheoryStrings : public Theory { /** The solver state of the theory of strings */ SolverState& d_state; };/* class TheoryStrings::NotifyClass */ - /** propagate method */ - bool propagateLit(TNode literal); /** compute care graph */ void computeCareGraph() override; /** |