From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 25 Feb 2022 07:13:43 +0000 (-0600)
Subject: Make quantifiers terminate if it detects a (duplicate) quantifier-free conflict ... 
X-Git-Tag: cvc5-1.0.0~379
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=31852631ba7fb56eac1f4a74df1ffd71735af272;p=cvc5.git

Make quantifiers terminate if it detects a (duplicate) quantifier-free conflict (#8157)

Fixes #6859.

The benchmark is now unknown.
---

diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 1098cd9fe..124198883 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -392,12 +392,18 @@ void QuantifiersEngine::check( Theory::Effort e ){
         //flush all current lemmas
         d_qim.doPending();
       }
-      //if we have added one, stop
-      if (d_qim.hasSentLemma())
+      // If we have added a lemma, stop. We also stop if we are in conflict.
+      // In very rare cases, it may be the case that quantifiers knows there
+      // is a conflict without adding a lemma, e.g. if it sent a duplicate
+      // QUANTIFIERS_TDB_DEQ_CONG lemma, which can occur if it has detected
+      // a quantifier-free conflict during term indexing but the quantifier
+      // free theories haven't caused a backtrack yet. This should never happen
+      // at LAST_CALL effort.
+      if (d_qim.hasSentLemma() || d_qstate.isInConflict())
       {
+        Assert(d_qim.hasSentLemma() || e != Theory::EFFORT_LAST_CALL);
         break;
       }else{
-        Assert(!d_qstate.isInConflict());
         if (quant_e == QuantifiersModule::QEFFORT_CONFLICT)
         {
           d_qstate.incrementInstRoundCounters(e);
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index fd3e7dd3a..3afba62b7 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -2125,6 +2125,7 @@ set(regress_1_tests
   regress1/quantifiers/issue6845-nl-lemma-tc.smt2
   regress1/quantifiers/issue7385-sygus-inst-i.smt2
   regress1/quantifiers/issue7537-cegqi-comp-types.smt2
+  regress1/quantifiers/issue8157-duplicate-conflicts.smt2
   regress1/quantifiers/issue993.smt2
   regress1/quantifiers/javafe.ast.StmtVec.009.smt2
   regress1/quantifiers/lia-witness-div-pp.smt2
diff --git a/test/regress/regress1/quantifiers/issue8157-duplicate-conflicts.smt2 b/test/regress/regress1/quantifiers/issue8157-duplicate-conflicts.smt2
new file mode 100644
index 000000000..c234bec9b
--- /dev/null
+++ b/test/regress/regress1/quantifiers/issue8157-duplicate-conflicts.smt2
@@ -0,0 +1,18 @@
+; EXPECT: unknown
+(set-logic ALL)
+(declare-const x Int)
+(declare-const x2 Bool)
+(declare-const x5 Int)
+(declare-fun T (Int) Bool)
+(declare-fun w (Int) Bool)
+(declare-fun W () Int)
+(declare-fun A ((_ BitVec 2)) Bool)
+(declare-fun B (Int) (_ BitVec 2))
+(declare-fun b ((Array Int Int) Int (Array Int Int) Int Int Int Int Int) Bool)
+(assert (forall ((i0 Int) (@ (Array Int Int)) (@@ (Array Int Int))) (! (= (b @ 0 @@ 0 x5 x5 x5 x5) (forall ((i Int)) (or (not (T i)) (not (A (B x5))) (not (w (- i i0))) (= (B (select @ (- i i0))) (bvand (B 0) (_ bv1 2)))))) :qid |BitVecto.26:19| :pattern ((b @ 0 @@ i0 x5 x5 x5 x5)))))
+(assert (forall ((i Int) (i2 Int)) (or (not (w i)) (not (w i2)) (= x2 (= (B i) (B i2))))))
+(declare-fun a () (Array Int Int))
+(declare-fun r () (Array Int Int))
+(declare-fun $ () (Array Int Int))
+(assert (and (b a 0 $ W x5 x5 x5 x5) (not (b r 0 r 0 x5 x5 x5 x))))
+(check-sat)