From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 15 Apr 2020 06:28:18 +0000 (-0500)
Subject: Abort if in conflict in enumerative instantiation (#4298)
X-Git-Tag: cvc5-1.0.0~3368
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c808605ef15eb79f9ddc2d1a2b4f6dd052530877;p=cvc5.git

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.
---

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;