diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-08-17 14:38:16 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-08-17 12:38:16 -0700 |
commit | 4f82b6eb7cc921ba2c6470a5ca0027be8dfc04e9 (patch) | |
tree | 4060becc52568fce247e9bd4e1660dfed33700dc /src/theory/uf/theory_uf.cpp | |
parent | 5c78f336b8276a2ed8916e2a9447a29a2caca069 (diff) |
Dynamic allocation of equality engine in Theory (#4890)
This commit updates Theory so that equality engines are allocated dynamically. The plan is to make this configurable based on the theory combination method.
The fundamental changes include:
- Add `d_equalityEngine` (raw) pointer to Theory, which is the "official" equality engine of the theory.
- Standardize methods for initializing Theory. This is now made more explicit in the documentation in theory.h, and includes a method `finishInitStandalone` for users of Theory that don't have an associated TheoryEngine.
- Refactor TheoryEngine::finishInit, including how Theory is initialized to incorporate the new policy.
- Things related to master equality engine are now specific to EqEngineManagerDistributed and hence can be removed from TheoryEngine. This will be further refactored in forthcoming PRs.
Note that the majority of changes are due to changing `d_equalityEngine.` to `d_equalityEngine->` throughout.
Diffstat (limited to 'src/theory/uf/theory_uf.cpp')
-rw-r--r-- | src/theory/uf/theory_uf.cpp | 95 |
1 files changed, 57 insertions, 38 deletions
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index 862a906a0..4f9c3bed5 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -54,16 +54,12 @@ TheoryUF::TheoryUF(context::Context* c, * so make sure it's initialized first. */ d_thss(nullptr), d_ho(nullptr), - d_equalityEngine(d_notify, c, instanceName + "theory::uf::ee", true), d_conflict(c, false), d_functionsTerms(c), d_symb(u, instanceName) { d_true = NodeManager::currentNM()->mkConst( true ); - // The kinds we are treating as function application in congruence - d_equalityEngine.addFunctionKind(kind::APPLY_UF, false, options::ufHo()); - ProofChecker* pc = pnm != nullptr ? pnm->getChecker() : nullptr; if (pc != nullptr) { @@ -74,11 +70,17 @@ TheoryUF::TheoryUF(context::Context* c, TheoryUF::~TheoryUF() { } -void TheoryUF::setMasterEqualityEngine(eq::EqualityEngine* eq) { - d_equalityEngine.setMasterEqualityEngine(eq); +TheoryRewriter* TheoryUF::getTheoryRewriter() { return &d_rewriter; } + +bool TheoryUF::needsEqualityEngine(EeSetupInfo& esi) +{ + esi.d_notify = &d_notify; + esi.d_name = d_instanceName + "theory::uf::ee"; + return true; } void TheoryUF::finishInit() { + Assert(d_equalityEngine != nullptr); // combined cardinality constraints are not evaluated in getModelValue d_valuation.setUnevaluatedKind(kind::COMBINED_CARDINALITY_CONSTRAINT); // Initialize the cardinality constraints solver if the logic includes UF, @@ -90,9 +92,11 @@ void TheoryUF::finishInit() { d_thss.reset(new CardinalityExtension( getSatContext(), getUserContext(), *d_out, this)); } + // The kinds we are treating as function application in congruence + d_equalityEngine->addFunctionKind(kind::APPLY_UF, false, options::ufHo()); if (options::ufHo()) { - d_equalityEngine.addFunctionKind(kind::HO_APPLY); + d_equalityEngine->addFunctionKind(kind::HO_APPLY); d_ho.reset(new HoExtension(*this, getSatContext(), getUserContext())); } } @@ -148,7 +152,7 @@ void TheoryUF::check(Effort level) { bool polarity = fact.getKind() != kind::NOT; TNode atom = polarity ? fact : fact[0]; if (atom.getKind() == kind::EQUAL) { - d_equalityEngine.assertEquality(atom, polarity, fact); + d_equalityEngine->assertEquality(atom, polarity, fact); if( options::ufHo() && options::ufHoExt() ){ if( !polarity && !d_conflict && atom[0].getType().isFunction() ){ // apply extensionality eagerly using the ho extension @@ -169,10 +173,10 @@ void TheoryUF::check(Effort level) { } //needed for models if( options::produceModels() ){ - d_equalityEngine.assertPredicate(atom, polarity, fact); + d_equalityEngine->assertPredicate(atom, polarity, fact); } } else { - d_equalityEngine.assertPredicate(atom, polarity, fact); + d_equalityEngine->assertPredicate(atom, polarity, fact); } } @@ -198,7 +202,7 @@ Node TheoryUF::getOperatorForApplyTerm( TNode node ) { if( node.getKind()==kind::APPLY_UF ){ return node.getOperator(); }else{ - return d_equalityEngine.getRepresentative( node[0] ); + return d_equalityEngine->getRepresentative(node[0]); } } @@ -242,17 +246,17 @@ void TheoryUF::preRegisterTerm(TNode node) { switch (node.getKind()) { case kind::EQUAL: // Add the trigger for equality - d_equalityEngine.addTriggerEquality(node); + d_equalityEngine->addTriggerEquality(node); break; case kind::APPLY_UF: case kind::HO_APPLY: // Maybe it's a predicate if (node.getType().isBoolean()) { // Get triggered for both equal and dis-equal - d_equalityEngine.addTriggerPredicate(node); + d_equalityEngine->addTriggerPredicate(node); } else { // Function applications/predicates - d_equalityEngine.addTerm(node); + d_equalityEngine->addTerm(node); } // Remember the function and predicate terms d_functionsTerms.push_back(node); @@ -263,7 +267,7 @@ void TheoryUF::preRegisterTerm(TNode node) { break; default: // Variables etc - d_equalityEngine.addTerm(node); + d_equalityEngine->addTerm(node); break; } }/* TheoryUF::preRegisterTerm() */ @@ -294,9 +298,10 @@ void TheoryUF::explain(TNode literal, std::vector<TNode>& assumptions, eq::EqPro bool polarity = literal.getKind() != kind::NOT; TNode atom = polarity ? literal : literal[0]; if (atom.getKind() == kind::EQUAL) { - d_equalityEngine.explainEquality(atom[0], atom[1], polarity, assumptions, pf); + d_equalityEngine->explainEquality( + atom[0], atom[1], polarity, assumptions, pf); } else { - d_equalityEngine.explainPredicate(atom, polarity, assumptions, pf); + d_equalityEngine->explainPredicate(atom, polarity, assumptions, pf); } if( pf ){ Debug("pf::uf") << std::endl; @@ -331,7 +336,7 @@ bool TheoryUF::collectModelInfo(TheoryModel* m) // Compute terms appearing in assertions and shared terms computeRelevantTerms(termSet); - if (!m->assertEqualityEngine(&d_equalityEngine, &termSet)) + if (!m->assertEqualityEngine(d_equalityEngine, &termSet)) { Trace("uf") << "Collect model info fail UF" << std::endl; return false; @@ -495,13 +500,15 @@ void TheoryUF::ppStaticLearn(TNode n, NodeBuilder<>& learned) { EqualityStatus TheoryUF::getEqualityStatus(TNode a, TNode b) { // Check for equality (simplest) - if (d_equalityEngine.areEqual(a, b)) { + if (d_equalityEngine->areEqual(a, b)) + { // The terms are implied to be equal return EQUALITY_TRUE; } // Check for disequality - if (d_equalityEngine.areDisequal(a, b, false)) { + if (d_equalityEngine->areDisequal(a, b, false)) + { // The terms are implied to be dis-equal return EQUALITY_FALSE; } @@ -512,15 +519,19 @@ EqualityStatus TheoryUF::getEqualityStatus(TNode a, TNode b) { void TheoryUF::addSharedTerm(TNode t) { Debug("uf::sharing") << "TheoryUF::addSharedTerm(" << t << ")" << std::endl; - d_equalityEngine.addTriggerTerm(t, THEORY_UF); + d_equalityEngine->addTriggerTerm(t, THEORY_UF); } bool TheoryUF::areCareDisequal(TNode x, TNode y){ - Assert(d_equalityEngine.hasTerm(x)); - Assert(d_equalityEngine.hasTerm(y)); - if( d_equalityEngine.isTriggerTerm(x, THEORY_UF) && d_equalityEngine.isTriggerTerm(y, THEORY_UF) ){ - TNode x_shared = d_equalityEngine.getTriggerTermRepresentative(x, THEORY_UF); - TNode y_shared = d_equalityEngine.getTriggerTermRepresentative(y, THEORY_UF); + Assert(d_equalityEngine->hasTerm(x)); + Assert(d_equalityEngine->hasTerm(y)); + if (d_equalityEngine->isTriggerTerm(x, THEORY_UF) + && d_equalityEngine->isTriggerTerm(y, THEORY_UF)) + { + TNode x_shared = + d_equalityEngine->getTriggerTermRepresentative(x, THEORY_UF); + TNode y_shared = + d_equalityEngine->getTriggerTermRepresentative(y, THEORY_UF); EqualityStatus eqStatus = d_valuation.getEqualityStatus(x_shared, y_shared); if( eqStatus==EQUALITY_FALSE_AND_PROPAGATED || eqStatus==EQUALITY_FALSE || eqStatus==EQUALITY_FALSE_IN_MODEL ){ return true; @@ -538,21 +549,27 @@ void TheoryUF::addCarePairs(TNodeTrie* t1, if( t2!=NULL ){ Node f1 = t1->getData(); Node f2 = t2->getData(); - if( !d_equalityEngine.areEqual( f1, f2 ) ){ + if (!d_equalityEngine->areEqual(f1, f2)) + { Debug("uf::sharing") << "TheoryUf::computeCareGraph(): checking function " << f1 << " and " << f2 << std::endl; vector< pair<TNode, TNode> > currentPairs; unsigned arg_start_index = getArgumentStartIndexForApplyTerm( f1 ); for (unsigned k = arg_start_index; k < f1.getNumChildren(); ++ k) { TNode x = f1[k]; TNode y = f2[k]; - Assert(d_equalityEngine.hasTerm(x)); - Assert(d_equalityEngine.hasTerm(y)); - Assert(!d_equalityEngine.areDisequal(x, y, false)); + Assert(d_equalityEngine->hasTerm(x)); + Assert(d_equalityEngine->hasTerm(y)); + Assert(!d_equalityEngine->areDisequal(x, y, false)); Assert(!areCareDisequal(x, y)); - if( !d_equalityEngine.areEqual( x, y ) ){ - if( d_equalityEngine.isTriggerTerm(x, THEORY_UF) && d_equalityEngine.isTriggerTerm(y, THEORY_UF) ){ - TNode x_shared = d_equalityEngine.getTriggerTermRepresentative(x, THEORY_UF); - TNode y_shared = d_equalityEngine.getTriggerTermRepresentative(y, THEORY_UF); + if (!d_equalityEngine->areEqual(x, y)) + { + if (d_equalityEngine->isTriggerTerm(x, THEORY_UF) + && d_equalityEngine->isTriggerTerm(y, THEORY_UF)) + { + TNode x_shared = + d_equalityEngine->getTriggerTermRepresentative(x, THEORY_UF); + TNode y_shared = + d_equalityEngine->getTriggerTermRepresentative(y, THEORY_UF); currentPairs.push_back(make_pair(x_shared, y_shared)); } } @@ -580,7 +597,8 @@ void TheoryUF::addCarePairs(TNodeTrie* t1, std::map<TNode, TNodeTrie>::iterator it2 = it; ++it2; for( ; it2 != t1->d_data.end(); ++it2 ){ - if( !d_equalityEngine.areDisequal(it->first, it2->first, false) ){ + if (!d_equalityEngine->areDisequal(it->first, it2->first, false)) + { if( !areCareDisequal(it->first, it2->first) ){ addCarePairs( &it->second, &it2->second, arity, depth+1 ); } @@ -593,7 +611,7 @@ void TheoryUF::addCarePairs(TNodeTrie* t1, { for (std::pair<const TNode, TNodeTrie>& tt2 : t2->d_data) { - if (!d_equalityEngine.areDisequal(tt1.first, tt2.first, false)) + if (!d_equalityEngine->areDisequal(tt1.first, tt2.first, false)) { if (!areCareDisequal(tt1.first, tt2.first)) { @@ -621,8 +639,9 @@ void TheoryUF::computeCareGraph() { std::vector< TNode > reps; bool has_trigger_arg = false; for( unsigned j=arg_start_index; j<f1.getNumChildren(); j++ ){ - reps.push_back( d_equalityEngine.getRepresentative( f1[j] ) ); - if( d_equalityEngine.isTriggerTerm( f1[j], THEORY_UF ) ){ + reps.push_back(d_equalityEngine->getRepresentative(f1[j])); + if (d_equalityEngine->isTriggerTerm(f1[j], THEORY_UF)) + { has_trigger_arg = true; } } |