From: Andrew Reynolds Date: Thu, 3 Sep 2020 23:31:36 +0000 (-0500) Subject: Update sets inference manager to inherit from InferenceManagerBuffered (#5007) X-Git-Tag: cvc5-1.0.0~2899 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=0fe081a56db369372584a5fcd35a4c4e4fb1c23f;p=cvc5.git Update sets inference manager to inherit from InferenceManagerBuffered (#5007) This updates the inference manager of sets to inherit from the standard base class InferenceManagerBuffered. It matches that base class almost exactly, with cosmetic changes. Notice that sets currently has a design issue: the state object sends lemmas and hence currently requires a pointer to the theory. This will be untangled in a future PR. This PR makes a few very minor changes to the behavior, including not to use the "preprocess" property for subtype lemmas. --- diff --git a/src/theory/inference_manager_buffered.cpp b/src/theory/inference_manager_buffered.cpp index 8a7713121..3ba41a431 100644 --- a/src/theory/inference_manager_buffered.cpp +++ b/src/theory/inference_manager_buffered.cpp @@ -29,10 +29,9 @@ InferenceManagerBuffered::InferenceManagerBuffered(Theory& t, { } -bool InferenceManagerBuffered::hasProcessed() const +bool InferenceManagerBuffered::hasPending() const { - return d_theoryState.isInConflict() || !d_pendingLem.empty() - || !d_pendingFact.empty(); + return hasPendingFact() || hasPendingLemma(); } bool InferenceManagerBuffered::hasPendingFact() const diff --git a/src/theory/inference_manager_buffered.h b/src/theory/inference_manager_buffered.h index 62c3c9b55..e5ad4cb0a 100644 --- a/src/theory/inference_manager_buffered.h +++ b/src/theory/inference_manager_buffered.h @@ -37,11 +37,9 @@ class InferenceManagerBuffered : public TheoryInferenceManager ProofNodeManager* pnm); virtual ~InferenceManagerBuffered() {} /** - * 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. + * Do we have a pending fact or lemma? */ - bool hasProcessed() const; + bool hasPending() const; /** * Do we have a pending fact to add as an internal fact to the equality * engine? diff --git a/src/theory/sets/cardinality_extension.cpp b/src/theory/sets/cardinality_extension.cpp index 08410943f..a51cee2c3 100644 --- a/src/theory/sets/cardinality_extension.cpp +++ b/src/theory/sets/cardinality_extension.cpp @@ -30,13 +30,10 @@ namespace CVC4 { namespace theory { namespace sets { -CardinalityExtension::CardinalityExtension(SolverState& s, - InferenceManager& im, - context::Context* c, - context::UserContext* u) +CardinalityExtension::CardinalityExtension(SolverState& s, InferenceManager& im) : d_state(s), d_im(im), - d_card_processed(u), + d_card_processed(s.getUserContext()), d_finite_type_constants_processed(false) { d_true = NodeManager::currentNM()->mkConst(true); @@ -288,7 +285,7 @@ void CardinalityExtension::registerCardinalityTerm(Node n) d_im.assertInference(lem, d_emp_exp, "card", 1); } } - d_im.flushPendingLemmas(); + d_im.doPendingLemmas(); } void CardinalityExtension::checkCardCycles() @@ -340,7 +337,7 @@ void CardinalityExtension::checkCardCyclesRec(Node eqc, Trace("sets-cycle-debug") << "CYCLE: " << fact << " from " << exp << std::endl; d_im.assertInference(fact, exp, "card_cycle"); - d_im.flushPendingLemmas(); + d_im.doPendingLemmas(); } else { @@ -416,7 +413,7 @@ void CardinalityExtension::checkCardCyclesRec(Node eqc, } } d_im.assertInference(conc, n.eqNode(emp_set), "cg_emp"); - d_im.flushPendingLemmas(); + d_im.doPendingLemmas(); if (d_im.hasProcessed()) { return; @@ -448,7 +445,7 @@ void CardinalityExtension::checkCardCyclesRec(Node eqc, Trace("sets-debug") << " it is empty..." << std::endl; Assert(!d_state.areEqual(n, emp_set)); d_im.assertInference(n.eqNode(emp_set), p.eqNode(emp_set), "cg_emppar"); - d_im.flushPendingLemmas(); + d_im.doPendingLemmas(); if (d_im.hasProcessed()) { return; @@ -495,7 +492,7 @@ void CardinalityExtension::checkCardCyclesRec(Node eqc, Trace("sets-debug") << "...derived " << conc.size() << " conclusions" << std::endl; d_im.assertInference(conc, n.eqNode(p), "cg_eqpar"); - d_im.flushPendingLemmas(); + d_im.doPendingLemmas(); if (d_im.hasProcessed()) { return; @@ -547,7 +544,7 @@ void CardinalityExtension::checkCardCyclesRec(Node eqc, { Node conc = n.eqNode(cpk); d_im.assertInference(conc, exps, "cg_par_sing"); - d_im.flushPendingLemmas(); + d_im.doPendingLemmas(); } else { @@ -602,7 +599,7 @@ void CardinalityExtension::checkCardCyclesRec(Node eqc, } } d_im.assertInference(conc, cpk.eqNode(cpnl), "cg_pareq"); - d_im.flushPendingLemmas(); + d_im.doPendingLemmas(); if (d_im.hasProcessed()) { return; @@ -973,7 +970,7 @@ void CardinalityExtension::checkMinCard() } } // flush the lemmas - d_im.flushPendingLemmas(); + d_im.doPendingLemmas(); } bool CardinalityExtension::isModelValueBasic(Node eqc) diff --git a/src/theory/sets/cardinality_extension.h b/src/theory/sets/cardinality_extension.h index b71af8a43..c257f45c5 100644 --- a/src/theory/sets/cardinality_extension.h +++ b/src/theory/sets/cardinality_extension.h @@ -67,10 +67,7 @@ class CardinalityExtension * Constructs a new instance of the cardinality solver w.r.t. the provided * contexts. */ - CardinalityExtension(SolverState& s, - InferenceManager& im, - context::Context* c, - context::UserContext* u); + CardinalityExtension(SolverState& s, InferenceManager& im); ~CardinalityExtension() {} /** reset diff --git a/src/theory/sets/inference_manager.cpp b/src/theory/sets/inference_manager.cpp index 8f25f6511..6f0d80b3a 100644 --- a/src/theory/sets/inference_manager.cpp +++ b/src/theory/sets/inference_manager.cpp @@ -15,8 +15,6 @@ #include "theory/sets/inference_manager.h" #include "options/sets_options.h" -#include "theory/sets/theory_sets.h" -#include "theory/sets/theory_sets_private.h" using namespace std; using namespace CVC4::kind; @@ -25,28 +23,15 @@ namespace CVC4 { namespace theory { namespace sets { -InferenceManager::InferenceManager(TheorySetsPrivate& p, +InferenceManager::InferenceManager(Theory& t, SolverState& s, - context::Context* c, - context::UserContext* u) - : d_parent(p), - d_state(s), - d_sentLemma(false), - d_addedFact(false), - d_lemmas_produced(u), - d_keep(c) + ProofNodeManager* pnm) + : InferenceManagerBuffered(t, s, pnm), d_state(s) { d_true = NodeManager::currentNM()->mkConst(true); d_false = NodeManager::currentNM()->mkConst(false); } -void InferenceManager::reset() -{ - d_sentLemma = false; - d_addedFact = false; - d_pendingLemmas.clear(); -} - bool InferenceManager::assertFactRec(Node fact, Node exp, int inferType) { // should we send this fact out as a lemma? @@ -61,7 +46,7 @@ bool InferenceManager::assertFactRec(Node fact, Node exp, int inferType) { lem = NodeManager::currentNM()->mkNode(IMPLIES, exp, fact); } - d_pendingLemmas.push_back(lem); + addPendingLemma(lem); return true; } Trace("sets-fact") << "Assert fact rec : " << fact << ", exp = " << exp @@ -96,18 +81,22 @@ bool InferenceManager::assertFactRec(Node fact, Node exp, int inferType) } bool polarity = fact.getKind() != NOT; TNode atom = polarity ? fact : fact[0]; + if (d_state.isEntailed(atom, polarity)) + { + return false; + } // things we can assert to equality engine if (atom.getKind() == MEMBER || (atom.getKind() == EQUAL && atom[0].getType().isSet())) { // send to equality engine - if (d_parent.assertFact(fact, exp)) + if (assertInternalFact(atom, polarity, exp)) { - d_addedFact = true; + // return true if this wasn't redundant return true; } } - else if (!d_state.isEntailed(fact, true)) + else { // must send as lemma Node lem = fact; @@ -115,7 +104,7 @@ bool InferenceManager::assertFactRec(Node fact, Node exp, int inferType) { lem = NodeManager::currentNM()->mkNode(IMPLIES, exp, fact); } - d_pendingLemmas.push_back(lem); + addPendingLemma(lem); return true; } return false; @@ -125,8 +114,6 @@ void InferenceManager::assertInference(Node fact, const char* c, int inferType) { - d_keep.insert(exp); - d_keep.insert(fact); if (assertFactRec(fact, exp, inferType)) { Trace("sets-lemma") << "Sets::Lemma : " << fact << " from " << exp << " by " @@ -176,67 +163,15 @@ void InferenceManager::split(Node n, int reqPol) { n = Rewriter::rewrite(n); Node lem = NodeManager::currentNM()->mkNode(OR, n, n.negate()); - flushLemma(lem); + // send the lemma + lemma(lem); Trace("sets-lemma") << "Sets::Lemma split : " << lem << std::endl; if (reqPol != 0) { Trace("sets-lemma") << "Sets::Require phase " << n << " " << (reqPol > 0) << std::endl; - d_parent.getOutputChannel()->requirePhase(n, reqPol > 0); - } -} -void InferenceManager::flushLemmas(std::vector& lemmas, bool preprocess) -{ - if (!d_state.isInConflict()) - { - for (const Node& l : lemmas) - { - flushLemma(l, preprocess); - } + requirePhase(n, reqPol > 0); } - lemmas.clear(); -} - -void InferenceManager::flushLemma(Node lem, bool preprocess) -{ - if (d_state.isInConflict()) - { - return; - } - if (d_lemmas_produced.find(lem) != d_lemmas_produced.end()) - { - Trace("sets-lemma-debug") << "Already sent lemma : " << lem << std::endl; - return; - } - Trace("sets-lemma-debug") << "Send lemma : " << lem << std::endl; - d_lemmas_produced.insert(lem); - LemmaProperty p = - preprocess ? LemmaProperty::PREPROCESS : LemmaProperty::NONE; - d_parent.getOutputChannel()->lemma(lem, p); - d_sentLemma = true; -} - -void InferenceManager::flushPendingLemmas(bool preprocess) -{ - flushLemmas(d_pendingLemmas, preprocess); -} - -bool InferenceManager::hasLemmaCached(Node lem) const -{ - return d_lemmas_produced.find(lem) != d_lemmas_produced.end(); -} - -bool InferenceManager::hasProcessed() const -{ - return d_state.isInConflict() || d_sentLemma || d_addedFact; -} -bool InferenceManager::hasSentLemma() const { return d_sentLemma; } -bool InferenceManager::hasAddedFact() const { return d_addedFact; } - -void InferenceManager::conflict(Node conf) -{ - d_parent.getOutputChannel()->conflict(conf); - d_state.notifyInConflict(); } } // namespace sets diff --git a/src/theory/sets/inference_manager.h b/src/theory/sets/inference_manager.h index 3278b848e..cc60ea4db 100644 --- a/src/theory/sets/inference_manager.h +++ b/src/theory/sets/inference_manager.h @@ -17,8 +17,8 @@ #ifndef CVC4__THEORY__SETS__INFERENCE_MANAGER_H #define CVC4__THEORY__SETS__INFERENCE_MANAGER_H +#include "theory/inference_manager_buffered.h" #include "theory/sets/solver_state.h" -#include "theory/uf/equality_engine.h" namespace CVC4 { namespace theory { @@ -33,22 +33,12 @@ class TheorySetsPrivate; * of theory of sets or internally as literals asserted to the equality engine * of theory of sets. The latter literals are referred to as "facts". */ -class InferenceManager +class InferenceManager : public InferenceManagerBuffered { typedef context::CDHashSet NodeSet; public: - InferenceManager(TheorySetsPrivate& p, - SolverState& s, - context::Context* c, - context::UserContext* u); - /** reset - * - * Called at the beginning of a full effort check. Resets the information - * related to this class regarding whether facts and lemmas have been - * processed. - */ - void reset(); + InferenceManager(Theory& t, SolverState& s, ProofNodeManager* pnm); /** * Add facts corresponding to ( exp => fact ) via calls to the assertFact * method of TheorySetsPrivate. @@ -80,71 +70,23 @@ class InferenceManager const char* c, int inferType = 0); - /** Flush lemmas - * - * This sends lemmas on the output channel of the theory of sets. - * - * The argument preprocess indicates whether preprocessing should be applied - * (by TheoryEngine) on each of lemmas. - */ - void flushLemmas(std::vector& lemmas, bool preprocess = false); - /** singular version of above */ - void flushLemma(Node lem, bool preprocess = false); - /** Do we have pending lemmas? */ - bool hasPendingLemmas() const { return !d_pendingLemmas.empty(); } - /** Applies flushLemmas on d_pendingLemmas */ - void flushPendingLemmas(bool preprocess = false); /** flush the splitting lemma ( n OR (NOT n) ) * * If reqPol is not 0, then a phase requirement for n is requested with * polarity ( reqPol>0 ). */ void split(Node n, int reqPol = 0); - /** Have we sent a lemma during the current call to a full effort check? */ - bool hasSentLemma() const; - /** Have we added a fact during the current call to a full effort check? */ - bool hasAddedFact() const; - /** Have we processed an inference (fact, lemma, or conflict)? */ - bool hasProcessed() const; - /** Have we sent lem as a lemma in the current user context? */ - bool hasLemmaCached(Node lem) const; - - /** - * Send conflict. - * @param conf The conflict node to be sent on the output channel - */ - void conflict(Node conf); private: /** constants */ Node d_true; Node d_false; - /** the theory of sets which owns this */ - TheorySetsPrivate& d_parent; - /** Reference to the state object for the theory of sets */ - SolverState& d_state; - /** pending lemmas */ - std::vector d_pendingLemmas; - /** sent lemma - * - * This flag is set to true during a full effort check if this theory - * called d_out->lemma(...). - */ - bool d_sentLemma; - /** added fact - * - * This flag is set to true during a full effort check if this theory - * added an internal fact to its equality engine. - */ - bool d_addedFact; - /** A user-context-dependent cache of all lemmas produced */ - NodeSet d_lemmas_produced; /** - * A set of nodes to ref-count. Nodes that are facts or are explanations of - * facts must be added to this set since the equality engine does not - * ref count nodes. + * Reference to the state object for the theory of sets. We store the + * (derived) state here, since it has additional methods required in this + * class. */ - NodeSet d_keep; + SolverState& d_state; /** Assert fact recursive * * This is a helper function for assertInference, which calls assertFact diff --git a/src/theory/sets/solver_state.cpp b/src/theory/sets/solver_state.cpp index 5e5e9d22a..7254bca78 100644 --- a/src/theory/sets/solver_state.cpp +++ b/src/theory/sets/solver_state.cpp @@ -25,16 +25,17 @@ namespace CVC4 { namespace theory { namespace sets { -SolverState::SolverState(TheorySetsPrivate& p, - context::Context* c, +SolverState::SolverState(context::Context* c, context::UserContext* u, Valuation val) - : TheoryState(c, u, val), d_parent(p), d_proxy(u), d_proxy_to_term(u) + : TheoryState(c, u, val), d_parent(nullptr), d_proxy(u), d_proxy_to_term(u) { d_true = NodeManager::currentNM()->mkConst(true); d_false = NodeManager::currentNM()->mkConst(false); } +void SolverState::setParent(TheorySetsPrivate* p) { d_parent = p; } + void SolverState::reset() { d_set_eqc.clear(); @@ -249,7 +250,7 @@ bool SolverState::isEntailed(Node n, bool polarity) const if (polarity && d_ee->hasTerm(n[1])) { Node r = d_ee->getRepresentative(n[1]); - if (d_parent.isMember(n[0], r)) + if (d_parent->isMember(n[0], r)) { return true; } @@ -387,13 +388,13 @@ Node SolverState::getProxy(Node n) d_proxy_to_term[k] = n; Node eq = k.eqNode(n); Trace("sets-lemma") << "Sets::Lemma : " << eq << " by proxy" << std::endl; - d_parent.getOutputChannel()->lemma(eq); + d_parent->getOutputChannel()->lemma(eq); if (nk == SINGLETON) { Node slem = nm->mkNode(MEMBER, n[0], k); Trace("sets-lemma") << "Sets::Lemma : " << slem << " by singleton" << std::endl; - d_parent.getOutputChannel()->lemma(slem); + d_parent->getOutputChannel()->lemma(slem); } return k; } @@ -452,7 +453,7 @@ Node SolverState::getUnivSet(TypeNode tn) Node ulem = nm->mkNode(SUBSET, n1, n2); Trace("sets-lemma") << "Sets::Lemma : " << ulem << " by univ-type" << std::endl; - d_parent.getOutputChannel()->lemma(ulem); + d_parent->getOutputChannel()->lemma(ulem); } } d_univset[tn] = n; diff --git a/src/theory/sets/solver_state.h b/src/theory/sets/solver_state.h index 3a40befbd..1786c414b 100644 --- a/src/theory/sets/solver_state.h +++ b/src/theory/sets/solver_state.h @@ -48,10 +48,9 @@ class SolverState : public TheoryState typedef context::CDHashMap NodeMap; public: - SolverState(TheorySetsPrivate& p, - context::Context* c, - context::UserContext* u, - Valuation val); + SolverState(context::Context* c, context::UserContext* u, Valuation val); + /** Set parent */ + void setParent(TheorySetsPrivate* p); //-------------------------------- initialize per check /** reset, clears the data structures maintained by this class. */ void reset(); @@ -204,8 +203,8 @@ class SolverState : public TheoryState /** the empty vector and map */ std::vector d_emptyVec; std::map d_emptyMap; - /** Reference to the parent theory of sets */ - TheorySetsPrivate& d_parent; + /** Pointer to the parent theory of sets */ + TheorySetsPrivate* d_parent; /** The list of all equivalence classes of type set in the current context */ std::vector d_set_eqc; /** Maps types to the equivalence class containing empty set of that type */ diff --git a/src/theory/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp index cb42f09d5..8b969de39 100644 --- a/src/theory/sets/theory_sets.cpp +++ b/src/theory/sets/theory_sets.cpp @@ -34,16 +34,21 @@ TheorySets::TheorySets(context::Context* c, const LogicInfo& logicInfo, ProofNodeManager* pnm) : Theory(THEORY_SETS, c, u, out, valuation, logicInfo, pnm), - d_internal(new TheorySetsPrivate(*this, c, u, valuation)), + d_state(c, u, valuation), + d_im(*this, d_state, pnm), + d_internal(new TheorySetsPrivate(*this, d_state, d_im)), d_notify(*d_internal.get()) { - // use the state object as the official theory state - d_theoryState = d_internal->getSolverState(); + // use the official theory state and inference manager objects + d_theoryState = &d_state; + d_inferManager = &d_im; + + // TODO: remove this + d_state.setParent(d_internal.get()); } TheorySets::~TheorySets() { - // Do not move me to the header. See explanation in the constructor. } TheoryRewriter* TheorySets::getTheoryRewriter() @@ -90,12 +95,6 @@ void TheorySets::finishInit() void TheorySets::postCheck(Effort level) { d_internal->postCheck(level); } -bool TheorySets::preNotifyFact( - TNode atom, bool polarity, TNode fact, bool isPrereg, bool isInternal) -{ - return d_internal->preNotifyFact(atom, polarity, fact); -} - void TheorySets::notifyFact(TNode atom, bool polarity, TNode fact, diff --git a/src/theory/sets/theory_sets.h b/src/theory/sets/theory_sets.h index 7787c0f9b..fed74b1bb 100644 --- a/src/theory/sets/theory_sets.h +++ b/src/theory/sets/theory_sets.h @@ -21,6 +21,8 @@ #include +#include "theory/sets/inference_manager.h" +#include "theory/sets/solver_state.h" #include "theory/theory.h" #include "theory/uf/equality_engine.h" @@ -61,12 +63,6 @@ class TheorySets : public Theory //--------------------------------- standard check /** Post-check, called after the fact queue of the theory is processed. */ void postCheck(Effort level) override; - /** Pre-notify fact, return true if processed. */ - bool preNotifyFact(TNode atom, - bool pol, - TNode fact, - bool isPrereg, - bool isInternal) override; /** Notify fact */ void notifyFact(TNode atom, bool pol, TNode fact, bool isInternal) override; //--------------------------------- end standard check @@ -102,6 +98,10 @@ class TheorySets : public Theory private: TheorySetsPrivate& d_theory; }; + /** The state of the sets solver at full effort */ + SolverState d_state; + /** The inference manager */ + InferenceManager d_im; /** The internal theory */ std::unique_ptr d_internal; /** Instance of the above class */ diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index c432c8039..7d498a798 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -35,19 +35,17 @@ namespace theory { namespace sets { TheorySetsPrivate::TheorySetsPrivate(TheorySets& external, - context::Context* c, - context::UserContext* u, - Valuation valuation) - : d_members(c), - d_deq(c), - d_termProcessed(u), - d_keep(c), + SolverState& state, + InferenceManager& im) + : d_members(state.getSatContext()), + d_deq(state.getSatContext()), + d_termProcessed(state.getUserContext()), d_full_check_incomplete(false), d_external(external), - d_state(*this, c, u, valuation), - d_im(*this, d_state, c, u), - d_rels(new TheorySetsRels(d_state, d_im, u)), - d_cardSolver(new CardinalityExtension(d_state, d_im, c, u)), + d_state(state), + d_im(im), + d_rels(new TheorySetsRels(d_state, d_im)), + d_cardSolver(new CardinalityExtension(d_state, d_im)), d_rels_enabled(false), d_card_enabled(false) { @@ -104,9 +102,7 @@ void TheorySetsPrivate::eqNotifyMerge(TNode t1, TNode t2) // infer equality between elements of singleton Node exp = s1.eqNode(s2); Node eq = s1[0].eqNode(s2[0]); - d_keep.insert(exp); - d_keep.insert(eq); - assertFact(eq, exp); + d_im.assertInternalFact(eq, true, exp); } else { @@ -166,11 +162,9 @@ void TheorySetsPrivate::eqNotifyMerge(TNode t1, TNode t2) if (s1[0] != m2[0]) { Node eq = s1[0].eqNode(m2[0]); - d_keep.insert(exp); - d_keep.insert(eq); Trace("sets-prop") << "Propagate eq-mem eq inference : " << exp << " => " << eq << std::endl; - assertFact(eq, exp); + d_im.assertInternalFact(eq, true, exp); } } else @@ -270,29 +264,6 @@ bool TheorySetsPrivate::isMember(Node x, Node s) return false; } -bool TheorySetsPrivate::assertFact(Node fact, Node exp) -{ - Trace("sets-assert") << "TheorySets::assertFact : " << fact - << ", exp = " << exp << std::endl; - bool polarity = fact.getKind() != kind::NOT; - TNode atom = polarity ? fact : fact[0]; - if (d_state.isEntailed(atom, polarity)) - { - return false; - } - if (atom.getKind() == kind::EQUAL) - { - d_equalityEngine->assertEquality(atom, polarity, exp); - } - else - { - d_equalityEngine->assertPredicate(atom, polarity, exp); - } - // call the notify new fact method - notifyFact(atom, polarity, exp); - return true; -} - void TheorySetsPrivate::fullEffortReset() { Assert(d_equalityEngine->consistent()); @@ -305,6 +276,7 @@ void TheorySetsPrivate::fullEffortReset() d_state.reset(); // reset the inference manager d_im.reset(); + d_im.clearPendingLemmas(); // reset the cardinality solver d_cardSolver->reset(); } @@ -314,7 +286,7 @@ void TheorySetsPrivate::fullEffortCheck() Trace("sets") << "----- Full effort check ------" << std::endl; do { - Assert(!d_im.hasPendingLemmas() || d_im.hasProcessed()); + Assert(!d_im.hasPendingLemma() || d_im.hasProcessed()); Trace("sets") << "...iterate full effort check..." << std::endl; fullEffortReset(); @@ -448,35 +420,35 @@ void TheorySetsPrivate::fullEffortCheck() } // check subtypes checkSubtypes(); - d_im.flushPendingLemmas(true); + d_im.doPendingLemmas(); if (d_im.hasProcessed()) { continue; } // check downwards closure checkDownwardsClosure(); - d_im.flushPendingLemmas(); + d_im.doPendingLemmas(); if (d_im.hasProcessed()) { continue; } // check upwards closure checkUpwardsClosure(); - d_im.flushPendingLemmas(); + d_im.doPendingLemmas(); if (d_im.hasProcessed()) { continue; } // check disequalities checkDisequalities(); - d_im.flushPendingLemmas(); + d_im.doPendingLemmas(); if (d_im.hasProcessed()) { continue; } // check reduce comprehensions checkReduceComprehensions(); - d_im.flushPendingLemmas(); + d_im.doPendingLemmas(); if (d_im.hasProcessed()) { continue; @@ -496,8 +468,8 @@ void TheorySetsPrivate::fullEffortCheck() d_rels->check(Theory::EFFORT_FULL); } } while (!d_im.hasSentLemma() && !d_state.isInConflict() - && d_im.hasAddedFact()); - Assert(!d_im.hasPendingLemmas() || d_im.hasProcessed()); + && d_im.hasSentFact()); + Assert(!d_im.hasPendingLemma() || d_im.hasProcessed()); Trace("sets") << "----- End full effort check, conflict=" << d_state.isInConflict() << ", lemma=" << d_im.hasSentLemma() << std::endl; @@ -854,7 +826,7 @@ void TheorySetsPrivate::checkDisequalities() Node lem = nm->mkNode(OR, deq, nm->mkNode(EQUAL, mem1, mem2).negate()); lem = Rewriter::rewrite(lem); d_im.assertInference(lem, d_true, "diseq", 1); - d_im.flushPendingLemmas(); + d_im.doPendingLemmas(); if (d_im.hasProcessed()) { return; @@ -893,7 +865,7 @@ void TheorySetsPrivate::checkReduceComprehensions() nm->mkNode(FORALL, nm->mkNode(BOUND_VAR_LIST, v), body.eqNode(mem)); Trace("sets-comprehension") << "Comprehension reduction: " << lem << std::endl; - d_im.flushLemma(lem); + d_im.lemma(lem); } } @@ -922,12 +894,6 @@ void TheorySetsPrivate::postCheck(Theory::Effort level) Trace("sets-check") << "Sets finish Check effort " << level << std::endl; } -bool TheorySetsPrivate::preNotifyFact(TNode atom, bool polarity, TNode fact) -{ - // use entailment check (is this necessary?) - return d_state.isEntailed(atom, polarity); -} - void TheorySetsPrivate::notifyFact(TNode atom, bool polarity, TNode fact) { if (d_state.isInConflict()) @@ -946,16 +912,14 @@ void TheorySetsPrivate::notifyFact(TNode atom, bool polarity, TNode fact) { Node pexp = NodeManager::currentNM()->mkNode( kind::AND, atom, atom[1].eqNode(s)); - d_keep.insert(pexp); if (s.getKind() == kind::SINGLETON) { if (s[0] != atom[0]) { Trace("sets-prop") << "Propagate mem-eq : " << pexp << std::endl; Node eq = s[0].eqNode(atom[0]); - d_keep.insert(eq); // triggers an internal inference - assertFact(eq, pexp); + d_im.assertInternalFact(eq, true, pexp); } } else diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h index 0df1eabc5..bd1d5f058 100644 --- a/src/theory/sets/theory_sets_private.h +++ b/src/theory/sets/theory_sets_private.h @@ -46,12 +46,6 @@ class TheorySetsPrivate { void eqNotifyNewClass(TNode t); void eqNotifyMerge(TNode t1, TNode t2); void eqNotifyDisequal(TNode t1, TNode t2, TNode reason); - /** Assert fact holds in the current context with explanation exp. - * - * exp should be explainable by the equality engine of this class, and fact - * should be a literal. - */ - bool assertFact(Node fact, Node exp); private: /** Are a and b trigger terms in the equality engine that may be disequal? */ @@ -122,7 +116,6 @@ class TheorySetsPrivate { * context. */ NodeSet d_termProcessed; - NodeSet d_keep; //propagation class EqcInfo @@ -155,9 +148,8 @@ class TheorySetsPrivate { * contexts. */ TheorySetsPrivate(TheorySets& external, - context::Context* c, - context::UserContext* u, - Valuation valuation); + SolverState& state, + InferenceManager& im); ~TheorySetsPrivate(); @@ -175,8 +167,6 @@ class TheorySetsPrivate { //--------------------------------- standard check /** Post-check, called after the fact queue of the theory is processed. */ void postCheck(Theory::Effort level); - /** Preprocess fact, return true if processed. */ - bool preNotifyFact(TNode atom, bool polarity, TNode fact); /** Notify new fact */ void notifyFact(TNode atom, bool polarity, TNode fact); //--------------------------------- end standard check @@ -237,6 +227,10 @@ class TheorySetsPrivate { private: TheorySets& d_external; + /** The state of the sets solver at full effort */ + SolverState& d_state; + /** The inference manager of the sets solver */ + InferenceManager& d_im; /** Pointer to the equality engine of theory of sets */ eq::EqualityEngine* d_equalityEngine; @@ -256,10 +250,6 @@ class TheorySetsPrivate { * given set type, or creates a new one if it does not exist. */ Node getChooseFunction(const TypeNode& setType); - /** The state of the sets solver at full effort */ - SolverState d_state; - /** The inference manager of the sets solver */ - InferenceManager d_im; /** subtheory solver for the theory of relations */ std::unique_ptr d_rels; /** subtheory solver for the theory of sets with cardinality */ diff --git a/src/theory/sets/theory_sets_rels.cpp b/src/theory/sets/theory_sets_rels.cpp index c8eeece4a..838d29045 100644 --- a/src/theory/sets/theory_sets_rels.cpp +++ b/src/theory/sets/theory_sets_rels.cpp @@ -31,10 +31,8 @@ typedef std::map< Node, std::unordered_set< Node, NodeHashFunction > >::iterator typedef std::map< Node, std::map< kind::Kind_t, std::vector< Node > > >::iterator TERM_IT; typedef std::map< Node, std::map< Node, std::unordered_set< Node, NodeHashFunction > > >::iterator TC_IT; -TheorySetsRels::TheorySetsRels(SolverState& s, - InferenceManager& im, - context::UserContext* u) - : d_state(s), d_im(im), d_shared_terms(u) +TheorySetsRels::TheorySetsRels(SolverState& s, InferenceManager& im) + : d_state(s), d_im(im), d_shared_terms(s.getUserContext()) { d_trueNode = NodeManager::currentNM()->mkConst(true); d_falseNode = NodeManager::currentNM()->mkConst(false); @@ -1103,7 +1101,7 @@ void TheorySetsRels::check(Theory::Effort level) // if we are still not in conflict, send lemmas if (!d_state.isInConflict()) { - d_im.flushPendingLemmas(); + d_im.doPendingLemmas(); } } d_pending.clear(); diff --git a/src/theory/sets/theory_sets_rels.h b/src/theory/sets/theory_sets_rels.h index 60715ff57..f48aaf9c5 100644 --- a/src/theory/sets/theory_sets_rels.h +++ b/src/theory/sets/theory_sets_rels.h @@ -65,9 +65,7 @@ class TheorySetsRels { typedef context::CDHashMap< Node, Node, NodeHashFunction > NodeMap; public: - TheorySetsRels(SolverState& s, - InferenceManager& im, - context::UserContext* u); + TheorySetsRels(SolverState& s, InferenceManager& im); ~TheorySetsRels(); /** diff --git a/src/theory/theory_inference_manager.cpp b/src/theory/theory_inference_manager.cpp index 9405a8162..330613e2e 100644 --- a/src/theory/theory_inference_manager.cpp +++ b/src/theory/theory_inference_manager.cpp @@ -56,6 +56,12 @@ void TheoryInferenceManager::reset() d_numCurrentFacts = 0; } +bool TheoryInferenceManager::hasProcessed() const +{ + return d_theoryState.isInConflict() || d_numCurrentLemmas > 0 + || d_numCurrentFacts > 0; +} + void TheoryInferenceManager::conflictEqConstantMerge(TNode a, TNode b) { if (!d_theoryState.isInConflict()) diff --git a/src/theory/theory_inference_manager.h b/src/theory/theory_inference_manager.h index 7e5ef6dec..080a09ba8 100644 --- a/src/theory/theory_inference_manager.h +++ b/src/theory/theory_inference_manager.h @@ -87,6 +87,11 @@ class TheoryInferenceManager * beginning of this loop and repeat its strategy while hasAddedFact is true. */ void reset(); + /** + * Returns true if we are in conflict, or if we have sent a lemma or fact + * since the last call to reset. + */ + bool hasProcessed() const; //--------------------------------------- propagations /** * T-propagate literal lit, possibly encountered by equality engine,