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/inst_strategy_enumerative.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/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) |