diff options
Diffstat (limited to 'src/theory/quantifiers/inst_strategy_enumerative.cpp')
-rw-r--r-- | src/theory/quantifiers/inst_strategy_enumerative.cpp | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/src/theory/quantifiers/inst_strategy_enumerative.cpp b/src/theory/quantifiers/inst_strategy_enumerative.cpp index 1dff5e000..d1c09a9e8 100644 --- a/src/theory/quantifiers/inst_strategy_enumerative.cpp +++ b/src/theory/quantifiers/inst_strategy_enumerative.cpp @@ -80,7 +80,7 @@ void InstStrategyEnum::check(Theory::Effort e, QEffort quant_e) } if (options::fullSaturateQuant() && !doCheck) { - if (!d_quantEngine->theoryEngineNeedsCheck()) + if (!d_qstate.getValuation().needCheck()) { doCheck = quant_e == QEFFORT_LAST_CALL; fullEffort = true; @@ -91,7 +91,7 @@ void InstStrategyEnum::check(Theory::Effort e, QEffort quant_e) { return; } - Assert(!d_quantEngine->inConflict()); + Assert(!d_qstate.isInConflict()); double clSet = 0; if (Trace.isOn("fs-engine")) { @@ -145,13 +145,13 @@ void InstStrategyEnum::check(Theory::Effort e, QEffort quant_e) // added lemma addedLemmas++; } - if (d_quantEngine->inConflict()) + if (d_qstate.isInConflict()) { break; } } } - if (d_quantEngine->inConflict() + if (d_qstate.isInConflict() || (addedLemmas > 0 && options::fullSaturateStratify())) { // we break if we are in conflict, or if we added any lemma at this @@ -331,7 +331,7 @@ bool InstStrategyEnum::process(Node f, bool fullEffort, bool isRd) { index--; } - if (d_quantEngine->inConflict()) + if (d_qstate.isInConflict()) { // could be conflicting for an internal reason (such as term // indices computed in above calls) |