diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-02-04 15:18:05 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-02-04 15:18:05 -0600 |
| commit | c8d7db69e6b5274c21029f231a1d312518d658e7 (patch) | |
| tree | e169a3b7504b8942d4cd859c666dea9ce83f1c6e /src/theory/quantifiers/equality_query.cpp | |
| parent | 18e8b81b8eb4c4e313b03f4616271a0ea8e65e9b (diff) | |
Eliminate equality query dependence on quantifiers engine (#5831)
This class will be renamed "RepSelector" on a future PR. It no longer needs to depend on quantifiers engine and can be initialized after the modules it depends on.
Diffstat (limited to 'src/theory/quantifiers/equality_query.cpp')
| -rw-r--r-- | src/theory/quantifiers/equality_query.cpp | 20 |
1 files changed, 11 insertions, 9 deletions
diff --git a/src/theory/quantifiers/equality_query.cpp b/src/theory/quantifiers/equality_query.cpp index 08741ef0f..c60c98d70 100644 --- a/src/theory/quantifiers/equality_query.cpp +++ b/src/theory/quantifiers/equality_query.cpp @@ -19,9 +19,6 @@ #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_util.h" -#include "theory/quantifiers_engine.h" -#include "theory/theory_engine.h" -#include "theory/uf/equality_engine.h" using namespace std; using namespace CVC4::kind; @@ -32,9 +29,10 @@ namespace theory { namespace quantifiers { EqualityQueryQuantifiersEngine::EqualityQueryQuantifiersEngine( - QuantifiersState& qs, QuantifiersEngine* qe) - : d_qe(qe), - d_qstate(qs), + QuantifiersState& qs, TermDb* tdb, FirstOrderModel* m) + : d_qstate(qs), + d_tdb(tdb), + d_model(m), d_eqi_counter(qs.getSatContext()), d_reset_count(0) { @@ -58,8 +56,9 @@ Node EqualityQueryQuantifiersEngine::getInternalRepresentative(Node a, if( options::finiteModelFind() ){ if( r.isConst() && quantifiers::TermUtil::containsUninterpretedConstant( r ) ){ //map back from values assigned by model, if any - if( d_qe->getModel() ){ - Node tr = d_qe->getModel()->getRepSet()->getTermForRepresentative(r); + if (d_model != nullptr) + { + Node tr = d_model->getRepSet()->getTermForRepresentative(r); if (!tr.isNull()) { r = tr; @@ -173,7 +172,10 @@ int EqualityQueryQuantifiersEngine::getRepScore(Node n, return -2; }else if( !n.getType().isSubtypeOf( v_tn ) ){ //reject if incorrect type return -2; - }else if( options::lteRestrictInstClosure() && ( !d_qe->getTermDatabase()->isInstClosure( n ) || !d_qe->getTermDatabase()->hasTermCurrent( n, false ) ) ){ + } + else if (options::lteRestrictInstClosure() + && (!d_tdb->isInstClosure(n) || !d_tdb->hasTermCurrent(n, false))) + { return -1; }else if( options::instMaxLevel()!=-1 ){ //score prefer lowest instantiation level |