diff options
Diffstat (limited to 'src/theory/sets/theory_sets.cpp')
-rw-r--r-- | src/theory/sets/theory_sets.cpp | 41 |
1 files changed, 22 insertions, 19 deletions
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])) { |