diff options
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 ){ |