diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-02-04 16:55:00 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-02-04 16:55:00 -0600 |
commit | 0bcaeb9cd75ec2268b6fe237bc037865d5122b5a (patch) | |
tree | f0d5efa61e6c839720d5494b33113520e59a5cd8 /src/theory/quantifiers/fmf/model_engine.cpp | |
parent | d89ff37c2dfbd91dd89169ad5dda06b5cc8f0a7b (diff) |
Introduce quantifiers registry utility (#5829)
This is a simple module for determining which quantifiers module has ownership of quantified formulas.
This is work towards eliminating dependencies of quantifiers modules.
Note that quantifiers attributes module (which no longer has a dependency on QuantifiersEngine after this PR) will be embedded into this module in a later PR.
Diffstat (limited to 'src/theory/quantifiers/fmf/model_engine.cpp')
-rw-r--r-- | src/theory/quantifiers/fmf/model_engine.cpp | 14 |
1 files changed, 9 insertions, 5 deletions
diff --git a/src/theory/quantifiers/fmf/model_engine.cpp b/src/theory/quantifiers/fmf/model_engine.cpp index 715002f7b..618a72047 100644 --- a/src/theory/quantifiers/fmf/model_engine.cpp +++ b/src/theory/quantifiers/fmf/model_engine.cpp @@ -35,8 +35,9 @@ using namespace CVC4::theory::inst; //Model Engine constructor ModelEngine::ModelEngine(QuantifiersEngine* qe, QuantifiersState& qs, - QuantifiersInferenceManager& qim) - : QuantifiersModule(qs, qim, qe), + QuantifiersInferenceManager& qim, + QuantifiersRegistry& qr) + : QuantifiersModule(qs, qim, qr, qe), d_incomplete_check(true), d_addedLemmas(0), d_triedLemmas(0), @@ -187,7 +188,8 @@ int ModelEngine::checkModel(){ if( Trace.isOn("model-engine") ){ for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){ Node f = fm->getAssertedQuantifier( i ); - if( d_quantEngine->getModel()->isQuantifierActive( f ) && d_quantEngine->hasOwnership( f, this ) ){ + if (fm->isQuantifierActive(f) && d_qreg.hasOwnership(f, this)) + { int totalInst = 1; for( unsigned j=0; j<f[0].getNumChildren(); j++ ){ TypeNode tn = f[0][j].getType(); @@ -213,7 +215,8 @@ int ModelEngine::checkModel(){ Node q = fm->getAssertedQuantifier( i, true ); Trace("fmf-exh-inst") << "-> Exhaustive instantiate " << q << ", effort = " << e << "..." << std::endl; //determine if we should check this quantifier - if( d_quantEngine->getModel()->isQuantifierActive( q ) && d_quantEngine->hasOwnership( q, this ) ){ + if (fm->isQuantifierActive(q) && d_qreg.hasOwnership(q, this)) + { exhaustiveInstantiate( q, e ); if (d_qstate.isInConflict()) { @@ -318,7 +321,8 @@ void ModelEngine::debugPrint( const char* c ){ Trace( c ) << "Quantifiers: " << std::endl; for( unsigned i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){ Node q = d_quantEngine->getModel()->getAssertedQuantifier( i ); - if( d_quantEngine->hasOwnership( q, this ) ){ + if (d_qreg.hasOwnership(q, this)) + { Trace( c ) << " "; if( !d_quantEngine->getModel()->isQuantifierActive( q ) ){ Trace( c ) << "*Inactive* "; |