From: Andrew Reynolds Date: Wed, 2 Sep 2020 13:17:39 +0000 (-0500) Subject: (new theory) Update TheorySets to the new interface (#4951) X-Git-Tag: cvc5-1.0.0~2922 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=78917e16f6521b0e8a074f3649fc6adf37614617;p=cvc5.git (new theory) Update TheorySets to the new interface (#4951) This updates the theory of sets to the new interface (see #4929). --- diff --git a/src/theory/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp index 0bf2ed2ea..cb42f09d5 100644 --- a/src/theory/sets/theory_sets.cpp +++ b/src/theory/sets/theory_sets.cpp @@ -67,12 +67,12 @@ void TheorySets::finishInit() d_valuation.setUnevaluatedKind(WITNESS); // functions we are doing congruence over - d_equalityEngine->addFunctionKind(kind::SINGLETON); - d_equalityEngine->addFunctionKind(kind::UNION); - d_equalityEngine->addFunctionKind(kind::INTERSECTION); - d_equalityEngine->addFunctionKind(kind::SETMINUS); - d_equalityEngine->addFunctionKind(kind::MEMBER); - d_equalityEngine->addFunctionKind(kind::SUBSET); + d_equalityEngine->addFunctionKind(SINGLETON); + d_equalityEngine->addFunctionKind(UNION); + d_equalityEngine->addFunctionKind(INTERSECTION); + d_equalityEngine->addFunctionKind(SETMINUS); + d_equalityEngine->addFunctionKind(MEMBER); + d_equalityEngine->addFunctionKind(SUBSET); // relation operators d_equalityEngine->addFunctionKind(PRODUCT); d_equalityEngine->addFunctionKind(JOIN); @@ -88,14 +88,20 @@ void TheorySets::finishInit() d_internal->finishInit(); } -void TheorySets::notifySharedTerm(TNode n) { d_internal->addSharedTerm(n); } +void TheorySets::postCheck(Effort level) { d_internal->postCheck(level); } -void TheorySets::check(Effort e) { - if (done() && e < Theory::EFFORT_FULL) { - return; - } - TimerStat::CodeTimer checkTimer(d_checkTime); - d_internal->check(e); +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, + bool isInternal) +{ + d_internal->notifyFact(atom, polarity, fact); } bool TheorySets::collectModelValues(TheoryModel* m, @@ -114,15 +120,12 @@ TrustNode TheorySets::explain(TNode node) return TrustNode::mkTrustPropExp(node, exp, nullptr); } -EqualityStatus TheorySets::getEqualityStatus(TNode a, TNode b) { - return d_internal->getEqualityStatus(a, b); -} - Node TheorySets::getModelValue(TNode node) { return Node::null(); } -void TheorySets::preRegisterTerm(TNode node) { +void TheorySets::preRegisterTerm(TNode node) +{ d_internal->preRegisterTerm(node); } @@ -158,7 +161,7 @@ Theory::PPAssertStatus TheorySets::ppAssert(TNode in, SubstitutionMap& outSubsti Theory::PPAssertStatus status = Theory::PP_ASSERT_STATUS_UNSOLVED; // this is based off of Theory::ppAssert - if (in.getKind() == kind::EQUAL) + if (in.getKind() == EQUAL) { if (in[0].isVar() && isLegalElimination(in[0], in[1])) { diff --git a/src/theory/sets/theory_sets.h b/src/theory/sets/theory_sets.h index a826a43af..7787c0f9b 100644 --- a/src/theory/sets/theory_sets.h +++ b/src/theory/sets/theory_sets.h @@ -58,13 +58,23 @@ class TheorySets : public Theory void finishInit() override; //--------------------------------- end initialization - void notifySharedTerm(TNode) override; - void check(Effort) override; + //--------------------------------- 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 + /** Collect model values in m based on the relevant terms given by termSet */ bool collectModelValues(TheoryModel* m, const std::set& termSet) override; void computeCareGraph() override; TrustNode explain(TNode) override; - EqualityStatus getEqualityStatus(TNode a, TNode b) override; Node getModelValue(TNode) override; std::string identify() const override { return "THEORY_SETS"; } void preRegisterTerm(TNode node) override; @@ -72,6 +82,7 @@ class TheorySets : public Theory PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions) override; void presolve() override; bool isEntailed(Node n, bool pol); + private: /** Functions to handle callbacks from equality engine */ class NotifyClass : public eq::EqualityEngineNotify diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index 78824636a..c432c8039 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -276,74 +276,21 @@ bool TheorySetsPrivate::assertFact(Node fact, Node exp) << ", exp = " << exp << std::endl; bool polarity = fact.getKind() != kind::NOT; TNode atom = polarity ? fact : fact[0]; - if (!d_state.isEntailed(atom, polarity)) + if (d_state.isEntailed(atom, polarity)) { - if (atom.getKind() == kind::EQUAL) - { - d_equalityEngine->assertEquality(atom, polarity, exp); - } - else - { - d_equalityEngine->assertPredicate(atom, polarity, exp); - } - if (!d_state.isInConflict()) - { - if (atom.getKind() == kind::MEMBER && polarity) - { - // check if set has a value, if so, we can propagate - Node r = d_equalityEngine->getRepresentative(atom[1]); - EqcInfo* e = getOrMakeEqcInfo(r, true); - if (e) - { - Node s = e->d_singleton; - if (!s.isNull()) - { - 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); - assertFact(eq, pexp); - } - } - else - { - Trace("sets-prop") - << "Propagate mem-eq conflict : " << pexp << std::endl; - d_im.conflict(pexp); - } - } - } - // add to membership list - NodeIntMap::iterator mem_i = d_members.find(r); - int n_members = 0; - if (mem_i != d_members.end()) - { - n_members = (*mem_i).second; - } - d_members[r] = n_members + 1; - if (n_members < (int)d_members_data[r].size()) - { - d_members_data[r][n_members] = atom; - } - else - { - d_members_data[r].push_back(atom); - } - } - } - return true; + return false; + } + if (atom.getKind() == kind::EQUAL) + { + d_equalityEngine->assertEquality(atom, polarity, exp); } else { - return false; + d_equalityEngine->assertPredicate(atom, polarity, exp); } + // call the notify new fact method + notifyFact(atom, polarity, exp); + return true; } void TheorySetsPrivate::fullEffortReset() @@ -950,26 +897,10 @@ void TheorySetsPrivate::checkReduceComprehensions() } } -/**************************** TheorySetsPrivate *****************************/ -/**************************** TheorySetsPrivate *****************************/ -/**************************** TheorySetsPrivate *****************************/ +//--------------------------------- standard check -void TheorySetsPrivate::check(Theory::Effort level) +void TheorySetsPrivate::postCheck(Theory::Effort level) { - Trace("sets-check") << "Sets check effort " << level << std::endl; - if (level == Theory::EFFORT_LAST_CALL) - { - return; - } - while (!d_external.done() && !d_state.isInConflict()) - { - // Get all the assertions - Assertion assertion = d_external.get(); - TNode fact = assertion.d_assertion; - Trace("sets-assert") << "Assert from input " << fact << std::endl; - // assert the fact - assertFact(fact, fact); - } Trace("sets-check") << "Sets finished assertions effort " << level << std::endl; // invoke full effort check, relations check @@ -989,18 +920,75 @@ void TheorySetsPrivate::check(Theory::Effort level) } } Trace("sets-check") << "Sets finish Check effort " << level << std::endl; -} /* TheorySetsPrivate::check() */ +} -/************************ Sharing ************************/ -/************************ Sharing ************************/ -/************************ Sharing ************************/ +bool TheorySetsPrivate::preNotifyFact(TNode atom, bool polarity, TNode fact) +{ + // use entailment check (is this necessary?) + return d_state.isEntailed(atom, polarity); +} -void TheorySetsPrivate::addSharedTerm(TNode n) +void TheorySetsPrivate::notifyFact(TNode atom, bool polarity, TNode fact) { - Debug("sets") << "[sets] TheorySetsPrivate::addSharedTerm( " << n << ")" - << std::endl; - d_equalityEngine->addTriggerTerm(n, THEORY_SETS); + if (d_state.isInConflict()) + { + return; + } + if (atom.getKind() == kind::MEMBER && polarity) + { + // check if set has a value, if so, we can propagate + Node r = d_equalityEngine->getRepresentative(atom[1]); + EqcInfo* e = getOrMakeEqcInfo(r, true); + if (e) + { + Node s = e->d_singleton; + if (!s.isNull()) + { + 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); + } + } + else + { + Trace("sets-prop") + << "Propagate mem-eq conflict : " << pexp << std::endl; + d_im.conflict(pexp); + } + } + } + // add to membership list + NodeIntMap::iterator mem_i = d_members.find(r); + int n_members = 0; + if (mem_i != d_members.end()) + { + n_members = (*mem_i).second; + } + d_members[r] = n_members + 1; + if (n_members < (int)d_members_data[r].size()) + { + d_members_data[r][n_members] = atom; + } + else + { + d_members_data[r].push_back(atom); + } + } } +//--------------------------------- end standard check + +/************************ Sharing ************************/ +/************************ Sharing ************************/ +/************************ Sharing ************************/ void TheorySetsPrivate::addCarePairs(TNodeTrie* t1, TNodeTrie* t2, @@ -1193,37 +1181,6 @@ bool TheorySetsPrivate::isCareArg(Node n, unsigned a) } } -EqualityStatus TheorySetsPrivate::getEqualityStatus(TNode a, TNode b) -{ - Assert(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; - /* - Node aModelValue = d_external.d_valuation.getModelValue(a); - if(aModelValue.isNull()) { return EQUALITY_UNKNOWN; } - Node bModelValue = d_external.d_valuation.getModelValue(b); - if(bModelValue.isNull()) { return EQUALITY_UNKNOWN; } - if( aModelValue == bModelValue ) { - // The term are true in current model - return EQUALITY_TRUE_IN_MODEL; - } else { - return EQUALITY_FALSE_IN_MODEL; - } - */ - // } - // //TODO: can we be more precise sometimes? - // return EQUALITY_UNKNOWN; -} - /******************** Model generation ********************/ /******************** Model generation ********************/ /******************** Model generation ********************/ @@ -1261,7 +1218,7 @@ std::string traceElements(const Node& set) bool TheorySetsPrivate::collectModelValues(TheoryModel* m, const std::set& termSet) { - Trace("sets-model") << "Set collect model info" << std::endl; + Trace("sets-model") << "Set collect model values" << std::endl; NodeManager* nm = NodeManager::currentNM(); std::map mvals; diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h index 387d56de9..0df1eabc5 100644 --- a/src/theory/sets/theory_sets_private.h +++ b/src/theory/sets/theory_sets_private.h @@ -172,18 +172,23 @@ class TheorySetsPrivate { */ void finishInit(); + //--------------------------------- 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 + + /** Collect model values in m based on the relevant terms given by termSet */ void addSharedTerm(TNode); - - void check(Theory::Effort); - bool collectModelValues(TheoryModel* m, const std::set& termSet); void computeCareGraph(); Node explain(TNode); - EqualityStatus getEqualityStatus(TNode a, TNode b); - void preRegisterTerm(TNode node); /** expandDefinition