diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-04-15 01:28:18 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-04-15 01:28:18 -0500 |
commit | c808605ef15eb79f9ddc2d1a2b4f6dd052530877 (patch) | |
tree | b2aa5750a536fe979da32d2e755c3dbac3a389ce /src | |
parent | 617f1b0fe93e077d6e76e03dcf1a75730740fe27 (diff) |
Abort if in conflict in enumerative instantiation (#4298)
In very rare cases, quantifiers engine can be the first to detect a quantifier-free conflict while constructing term indices. When this occurs, instantiation modules can quit immediately. This was not happening in a case of enumerative instantiation.
Fixes #4293.
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/quantifiers/inst_strategy_enumerative.cpp | 15 | ||||
-rw-r--r-- | src/theory/quantifiers_engine.cpp | 2 |
2 files changed, 13 insertions, 4 deletions
diff --git a/src/theory/quantifiers/inst_strategy_enumerative.cpp b/src/theory/quantifiers/inst_strategy_enumerative.cpp index ce024fe8b..81ade68fc 100644 --- a/src/theory/quantifiers/inst_strategy_enumerative.cpp +++ b/src/theory/quantifiers/inst_strategy_enumerative.cpp @@ -88,6 +88,7 @@ void InstStrategyEnum::check(Theory::Effort e, QEffort quant_e) { return; } + Assert(!d_quantEngine->inConflict()); double clSet = 0; if (Trace.isOn("fs-engine")) { @@ -140,10 +141,10 @@ void InstStrategyEnum::check(Theory::Effort e, QEffort quant_e) } // added lemma addedLemmas++; - if (d_quantEngine->inConflict()) - { - break; - } + } + if (d_quantEngine->inConflict()) + { + break; } } } @@ -324,6 +325,12 @@ bool InstStrategyEnum::process(Node f, bool fullEffort, bool isRd) { index--; } + if (d_quantEngine->inConflict()) + { + // could be conflicting for an internal reason (such as term + // indices computed in above calls) + return false; + } } } while (success); max_i++; diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 4339ee75f..6e60780d6 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -601,6 +601,8 @@ void QuantifiersEngine::check( Theory::Effort e ){ << " Theory engine finished : " << !theoryEngineNeedsCheck() << std::endl; Trace("quant-engine-debug") << " Needs model effort : " << needsModelE << std::endl; + Trace("quant-engine-debug") + << " In conflict : " << d_conflict << std::endl; } if( Trace.isOn("quant-engine-ee-pre") ){ Trace("quant-engine-ee-pre") << "Equality engine (pre-inference): " << std::endl; |