diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-01-28 13:27:27 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-01-28 13:27:27 -0600 |
commit | 3234db430074e278258e6d687c07146a59769a92 (patch) | |
tree | 17db55e1ff335c3998e1c4e172d174dc9f6e3b21 /src/theory/quantifiers/equality_query.cpp | |
parent | 4cd2d73366aba081a38900ddc2f4f172ce9ed2f8 (diff) |
Use standard equality engine information in quantifiers state (#5824)
This refactors quantifiers so that it uses the standard interfaces for setting up an equality engine and using it via TheoryState.
This eliminates the need for several special interfaces including getMasterEqualityEngine, CombinationEngine::getCoreEqualityEngine, and most uses of EqualityQuery.
Diffstat (limited to 'src/theory/quantifiers/equality_query.cpp')
-rw-r--r-- | src/theory/quantifiers/equality_query.cpp | 74 |
1 files changed, 7 insertions, 67 deletions
diff --git a/src/theory/quantifiers/equality_query.cpp b/src/theory/quantifiers/equality_query.cpp index b8515df91..08741ef0f 100644 --- a/src/theory/quantifiers/equality_query.cpp +++ b/src/theory/quantifiers/equality_query.cpp @@ -33,7 +33,10 @@ namespace quantifiers { EqualityQueryQuantifiersEngine::EqualityQueryQuantifiersEngine( QuantifiersState& qs, QuantifiersEngine* qe) - : d_qe(qe), d_eqi_counter(qs.getSatContext()), d_reset_count(0) + : d_qe(qe), + d_qstate(qs), + d_eqi_counter(qs.getSatContext()), + d_reset_count(0) { } @@ -46,51 +49,12 @@ bool EqualityQueryQuantifiersEngine::reset( Theory::Effort e ){ return true; } -bool EqualityQueryQuantifiersEngine::hasTerm( Node a ){ - return getEngine()->hasTerm( a ); -} - -Node EqualityQueryQuantifiersEngine::getRepresentative( Node a ){ - eq::EqualityEngine* ee = getEngine(); - if( ee->hasTerm( a ) ){ - return ee->getRepresentative( a ); - }else{ - return a; - } -} - -bool EqualityQueryQuantifiersEngine::areEqual( Node a, Node b ){ - if( a==b ){ - return true; - }else{ - eq::EqualityEngine* ee = getEngine(); - if( ee->hasTerm( a ) && ee->hasTerm( b ) ){ - return ee->areEqual( a, b ); - }else{ - return false; - } - } -} - -bool EqualityQueryQuantifiersEngine::areDisequal( Node a, Node b ){ - if( a==b ){ - return false; - }else{ - eq::EqualityEngine* ee = getEngine(); - if( ee->hasTerm( a ) && ee->hasTerm( b ) ){ - return ee->areDisequal( a, b, false ); - }else{ - return a.isConst() && b.isConst(); - } - } -} - Node EqualityQueryQuantifiersEngine::getInternalRepresentative(Node a, Node q, int index) { Assert(q.isNull() || q.getKind() == FORALL); - Node r = getRepresentative( a ); + Node r = d_qstate.getRepresentative(a); if( options::finiteModelFind() ){ if( r.isConst() && quantifiers::TermUtil::containsUninterpretedConstant( r ) ){ //map back from values assigned by model, if any @@ -99,7 +63,7 @@ Node EqualityQueryQuantifiersEngine::getInternalRepresentative(Node a, if (!tr.isNull()) { r = tr; - r = getRepresentative( r ); + r = d_qstate.getRepresentative(r); }else{ if( r.getType().isSort() ){ Trace("internal-rep-warn") << "No representative for UF constant." << std::endl; @@ -129,7 +93,7 @@ Node EqualityQueryQuantifiersEngine::getInternalRepresentative(Node a, // find best selection for representative Node r_best; std::vector<Node> eqc; - getEquivalenceClass(r, eqc); + d_qstate.getEquivalenceClass(r, eqc); Trace("internal-rep-select") << "Choose representative for equivalence class : " << eqc << ", type = " << v_tn << std::endl; @@ -180,30 +144,6 @@ Node EqualityQueryQuantifiersEngine::getInternalRepresentative(Node a, return r_best; } -eq::EqualityEngine* EqualityQueryQuantifiersEngine::getEngine(){ - return d_qe->getMasterEqualityEngine(); -} - -void EqualityQueryQuantifiersEngine::getEquivalenceClass( Node a, std::vector< Node >& eqc ){ - eq::EqualityEngine* ee = getEngine(); - if( ee->hasTerm( a ) ){ - Node rep = ee->getRepresentative( a ); - eq::EqClassIterator eqc_iter( rep, ee ); - while( !eqc_iter.isFinished() ){ - eqc.push_back( *eqc_iter ); - eqc_iter++; - } - }else{ - eqc.push_back( a ); - } - //a should be in its equivalence class - Assert(std::find(eqc.begin(), eqc.end(), a) != eqc.end()); -} - -TNode EqualityQueryQuantifiersEngine::getCongruentTerm( Node f, std::vector< TNode >& args ) { - return d_qe->getTermDatabase()->getCongruentTerm( f, args ); -} - //helper functions Node EqualityQueryQuantifiersEngine::getInstance( Node n, const std::vector< Node >& eqc, std::unordered_map<TNode, Node, TNodeHashFunction>& cache ){ |