diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-01-26 19:24:58 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-01-26 19:24:58 -0600 |
| commit | 524c2d9f44a7c4297422dd1356fe3dc377166180 (patch) | |
| tree | 7cb5988f7d9feb633bb9dace3f272015ddd8300f /src/theory/quantifiers/fmf/model_engine.cpp | |
| parent | c34722f830b63bc45a38217943f061912990086d (diff) | |
Use standard conflict mechanism in quantifiers state (#5822)
Work towards eliminating dependencies on quantifiers engine, this updates quantifiers module to use the standard SAT-context dependent flag in quantifiers state instead of the one in QuantifiersEngine. It also eliminates the use of a custom call to theoryEngineNeedsCheck.
Diffstat (limited to 'src/theory/quantifiers/fmf/model_engine.cpp')
| -rw-r--r-- | src/theory/quantifiers/fmf/model_engine.cpp | 12 |
1 files changed, 7 insertions, 5 deletions
diff --git a/src/theory/quantifiers/fmf/model_engine.cpp b/src/theory/quantifiers/fmf/model_engine.cpp index 3849dc2c6..4d74c1697 100644 --- a/src/theory/quantifiers/fmf/model_engine.cpp +++ b/src/theory/quantifiers/fmf/model_engine.cpp @@ -77,7 +77,7 @@ void ModelEngine::check(Theory::Effort e, QEffort quant_e) doCheck = quant_e == QEFFORT_MODEL; } if( doCheck ){ - Assert(!d_quantEngine->inConflict()); + Assert(!d_qstate.isInConflict()); int addedLemmas = 0; //the following will test that the model satisfies all asserted universal quantifiers by @@ -217,7 +217,7 @@ int ModelEngine::checkModel(){ //determine if we should check this quantifier if( d_quantEngine->getModel()->isQuantifierActive( q ) && d_quantEngine->hasOwnership( q, this ) ){ exhaustiveInstantiate( q, e ); - if (d_quantEngine->inConflict()) + if (d_qstate.isInConflict()) { break; } @@ -228,12 +228,13 @@ int ModelEngine::checkModel(){ if( d_addedLemmas>0 ){ break; }else{ - Assert(!d_quantEngine->inConflict()); + Assert(!d_qstate.isInConflict()); } } //print debug information - if( d_quantEngine->inConflict() ){ + if (d_qstate.isInConflict()) + { Trace("model-engine") << "Conflict, added lemmas = "; }else{ Trace("model-engine") << "Added Lemmas = "; @@ -293,7 +294,8 @@ void ModelEngine::exhaustiveInstantiate( Node f, int effort ){ if (inst->addInstantiation(f, m, true)) { addedLemmas++; - if( d_quantEngine->inConflict() ){ + if (d_qstate.isInConflict()) + { break; } }else{ |