Delay enumerative instantiation if theory engine does not need check (#3774)

7 files changed, 301 insertions, 8 deletions

diff --git a/src/theory/quantifiers/inst_strategy_enumerative.cpp b/src/theory/quantifiers/inst_strategy_enumerative.cpp
index 1e2e34aa2..47e4a9228 100644
--- a/src/theory/quantifiers/inst_strategy_enumerative.cpp
+++ b/src/theory/quantifiers/inst_strategy_enumerative.cpp
@@ -77,8 +77,11 @@ void InstStrategyEnum::check(Theory::Effort e, QEffort quant_e)
     }
     if (options::fullSaturateQuant() && !doCheck)
     {
-      doCheck = quant_e == QEFFORT_LAST_CALL;
-      fullEffort = !d_quantEngine->hasAddedLemma();
+      if (!d_quantEngine->theoryEngineNeedsCheck())
+      {
+        doCheck = quant_e == QEFFORT_LAST_CALL;
+        fullEffort = true;
+      }
     }
   }
   if (!doCheck)
diff --git a/src/theory/quantifiers/sygus/synth_engine.cpp b/src/theory/quantifiers/sygus/synth_engine.cpp
index 2b621f6dd..c9ed16a5f 100644
--- a/src/theory/quantifiers/sygus/synth_engine.cpp
+++ b/src/theory/quantifiers/sygus/synth_engine.cpp
@@ -133,7 +133,7 @@ void SynthEngine::check(Theory::Effort e, QEffort quant_e)
     activeCheckConj = acnext;
     acnext.clear();
   } while (!activeCheckConj.empty()
-           && !d_quantEngine->getTheoryEngine()->needCheck());
+           && !d_quantEngine->theoryEngineNeedsCheck());
   Trace("cegqi-engine")
       << "Finished Counterexample Guided Instantiation engine." << std::endl;
 }
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 524c440ba..b78263f0e 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -403,7 +403,7 @@ void TermDb::computeUfTerms( TNode f ) {
           {
             Trace("term-db-lemma") << "Disequal congruent terms : " << at << " "
                                    << n << "!!!!" << std::endl;
-            if (!d_quantEngine->getTheoryEngine()->needCheck())
+            if (!d_quantEngine->theoryEngineNeedsCheck())
             {
               Trace("term-db-lemma") << "  all theories passed with no lemmas."
                                      << std::endl;
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 80a493496..1db0937ff 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -617,7 +617,9 @@ void QuantifiersEngine::check( Theory::Effort e ){
       if( !d_lemmas_waiting.empty() ){
         Trace("quant-engine-debug") << "  lemmas waiting = " << d_lemmas_waiting.size() << std::endl;
       }
-      Trace("quant-engine-debug") << "  Theory engine finished : " << !d_te->needCheck() << std::endl;
+      Trace("quant-engine-debug")
+          << "  Theory engine finished : " << !theoryEngineNeedsCheck()
+          << std::endl;
       Trace("quant-engine-debug") << "  Needs model effort : " << needsModelE << std::endl;
     }
     if( Trace.isOn("quant-engine-ee-pre") ){
@@ -1053,6 +1055,14 @@ void QuantifiersEngine::addRequirePhase( Node lit, bool req ){
 void QuantifiersEngine::markRelevant( Node q ) {
   d_model->markRelevant( q );
 }
+bool QuantifiersEngine::hasAddedLemma() const
+{
+  return !d_lemmas_waiting.empty() || d_hasAddedLemma;
+}
+bool QuantifiersEngine::theoryEngineNeedsCheck() const
+{
+  return d_te->needCheck();
+}
 
 void QuantifiersEngine::setConflict() { 
   d_conflict = true; 
@@ -1069,7 +1079,7 @@ bool QuantifiersEngine::getInstWhenNeedsCheck( Theory::Effort e ) {
   }
   else if (options::instWhenMode() == options::InstWhenMode::FULL_DELAY)
   {
-    performCheck = ( e >= Theory::EFFORT_FULL ) && !getTheoryEngine()->needCheck();
+    performCheck = (e >= Theory::EFFORT_FULL) && !theoryEngineNeedsCheck();
   }
   else if (options::instWhenMode() == options::InstWhenMode::FULL_LAST_CALL)
   {
@@ -1078,7 +1088,9 @@ bool QuantifiersEngine::getInstWhenNeedsCheck( Theory::Effort e ) {
   else if (options::instWhenMode()
            == options::InstWhenMode::FULL_DELAY_LAST_CALL)
   {
-    performCheck = ( ( e==Theory::EFFORT_FULL && !getTheoryEngine()->needCheck() && d_ierCounter%d_inst_when_phase!=0 ) || e==Theory::EFFORT_LAST_CALL );
+    performCheck = ((e == Theory::EFFORT_FULL && !theoryEngineNeedsCheck()
+                     && d_ierCounter % d_inst_when_phase != 0)
+                    || e == Theory::EFFORT_LAST_CALL);
   }
   else if (options::instWhenMode() == options::InstWhenMode::LAST_CALL)
   {
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index 380e0896e..5172c1554 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -202,7 +202,14 @@ public:
   /** mark relevant quantified formula, this will indicate it should be checked before the others */
   void markRelevant( Node q );
   /** has added lemma */
-  bool hasAddedLemma() { return !d_lemmas_waiting.empty() || d_hasAddedLemma; }
+  bool hasAddedLemma() const;
+  /** theory engine needs check
+   *
+   * This is true if the theory engine has more constraints to process. When
+   * it is false, we are tentatively going to terminate solving with
+   * sat/unknown. For details, see TheoryEngine::needCheck.
+   */
+  bool theoryEngineNeedsCheck() const;
   /** is in conflict */
   bool inConflict() { return d_conflict; }
   /** set conflict */
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 1437baae1..159f87037 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1442,6 +1442,7 @@ set(regress_1_tests
   regress1/quantifiers/issue3316.smt2
   regress1/quantifiers/issue3317.smt2
   regress1/quantifiers/issue3481.smt2
+  regress1/quantifiers/issue3481-unsat1.smt2
   regress1/quantifiers/issue3537.smt2
   regress1/quantifiers/issue3628.smt2
   regress1/quantifiers/issue3664.smt2
diff --git a/test/regress/regress1/quantifiers/issue3481-unsat1.smt2 b/test/regress/regress1/quantifiers/issue3481-unsat1.smt2
new file mode 100644
index 000000000..fb7ff5485
--- /dev/null
+++ b/test/regress/regress1/quantifiers/issue3481-unsat1.smt2
@@ -0,0 +1,270 @@
+; COMMAND-LINE: --full-saturate-quant
+; EXPECT: unsat
+
+;; produced by cvc4_16.drv ;;
+(set-logic AUFBVFPDTNIRA)
+(set-info :smt-lib-version 2.6)
+;;; generated by SMT-LIB2 driver
+;;; SMT-LIB2 driver: bit-vectors, common part
+;;; SMT-LIB2: integer arithmetic
+(declare-sort string 0)
+
+(declare-datatypes ((tuple0 0))
+(((Tuple0))))
+(declare-sort us_private 0)
+
+(declare-fun private__bool_eq (us_private us_private) Bool)
+
+(declare-const us_null_ext__ us_private)
+
+(declare-sort us_type_of_heap 0)
+
+(declare-datatypes ((us_type_of_heap__ref 0))
+(((us_type_of_heap__refqtmk (us_type_of_heap__content us_type_of_heap)))))
+(declare-sort us_image 0)
+
+(declare-datatypes ((int__ref 0))
+(((int__refqtmk (int__content Int)))))
+(declare-datatypes ((bool__ref 0))
+(((bool__refqtmk (bool__content Bool)))))
+(declare-datatypes ((us_fixed__ref 0))
+(((us_fixed__refqtmk (us_fixed__content Int)))))
+(declare-datatypes ((real__ref 0))
+(((real__refqtmk (real__content Real)))))
+(declare-datatypes ((us_private__ref 0))
+(((us_private__refqtmk (us_private__content us_private)))))
+(define-fun int__ref___projection ((a int__ref)) Int (int__content a))
+
+(define-fun us_fixed__ref___projection ((a us_fixed__ref)) Int (us_fixed__content
+                                                               a))
+
+(define-fun bool__ref___projection ((a bool__ref)) Bool (bool__content a))
+
+(define-fun real__ref___projection ((a real__ref)) Real (real__content a))
+
+(define-fun us_private__ref___projection ((a us_private__ref)) us_private 
+  (us_private__content a))
+
+(define-fun abs1 ((x Int)) Int (ite (<= 0 x) x (- x)))
+
+;; Abs_le
+  (assert
+  (forall ((x Int) (y Int)) (= (<= (abs1 x) y) (and (<= (- y) x) (<= x y)))))
+
+;; Abs_pos
+  (assert (forall ((x Int)) (<= 0 (abs1 x))))
+
+(declare-fun div1 (Int Int) Int)
+
+(declare-fun mod1 (Int Int) Int)
+
+;; Div_mod
+  (assert
+  (forall ((x Int) (y Int))
+  (=> (not (= y 0)) (= x (+ (* y (div1 x y)) (mod1 x y))))))
+
+;; Div_bound
+  (assert
+  (forall ((x Int) (y Int))
+  (=> (and (<= 0 x) (< 0 y)) (and (<= 0 (div1 x y)) (<= (div1 x y) x)))))
+
+;; Mod_bound
+  (assert
+  (forall ((x Int) (y Int))
+  (=> (not (= y 0))
+  (and (< (- (abs1 y)) (mod1 x y)) (< (mod1 x y) (abs1 y))))))
+
+;; Div_sign_pos
+  (assert
+  (forall ((x Int) (y Int)) (=> (and (<= 0 x) (< 0 y)) (<= 0 (div1 x y)))))
+
+;; Div_sign_neg
+  (assert
+  (forall ((x Int) (y Int)) (=> (and (<= x 0) (< 0 y)) (<= (div1 x y) 0))))
+
+;; Mod_sign_pos
+  (assert
+  (forall ((x Int) (y Int))
+  (=> (and (<= 0 x) (not (= y 0))) (<= 0 (mod1 x y)))))
+
+;; Mod_sign_neg
+  (assert
+  (forall ((x Int) (y Int))
+  (=> (and (<= x 0) (not (= y 0))) (<= (mod1 x y) 0))))
+
+;; Rounds_toward_zero
+  (assert
+  (forall ((x Int) (y Int))
+  (=> (not (= y 0)) (<= (abs1 (* (div1 x y) y)) (abs1 x)))))
+
+;; Div_1
+  (assert (forall ((x Int)) (= (div1 x 1) x)))
+
+;; Mod_1
+  (assert (forall ((x Int)) (= (mod1 x 1) 0)))
+
+;; Div_inf
+  (assert
+  (forall ((x Int) (y Int)) (=> (and (<= 0 x) (< x y)) (= (div1 x y) 0))))
+
+;; Mod_inf
+  (assert
+  (forall ((x Int) (y Int)) (=> (and (<= 0 x) (< x y)) (= (mod1 x y) x))))
+
+;; Div_mult
+  (assert
+  (forall ((x Int) (y Int) (z Int))
+  (! (=> (and (< 0 x) (and (<= 0 y) (<= 0 z)))
+     (= (div1 (+ (* x y) z) x) (+ y (div1 z x)))) :pattern ((div1
+                                                            (+ (* x y) z) x)) )))
+
+;; Mod_mult
+  (assert
+  (forall ((x Int) (y Int) (z Int))
+  (! (=> (and (< 0 x) (and (<= 0 y) (<= 0 z)))
+     (= (mod1 (+ (* x y) z) x) (mod1 z x))) :pattern ((mod1 (+ (* x y) z) x)) )))
+
+;; Div_unique
+  (assert
+  (forall ((x Int) (y Int) (q Int))
+  (=> (< 0 y) (=> (and (<= (* q y) x) (< x (+ (* q y) y))) (= (div x y) q)))))
+
+;; Div_bound
+  (assert
+  (forall ((x Int) (y Int))
+  (=> (and (<= 0 x) (< 0 y)) (and (<= 0 (div x y)) (<= (div x y) x)))))
+
+;; Div_inf
+  (assert
+  (forall ((x Int) (y Int)) (=> (and (<= 0 x) (< x y)) (= (div x y) 0))))
+
+;; Div_inf_neg
+  (assert
+  (forall ((x Int) (y Int))
+  (=> (and (< 0 x) (<= x y)) (= (div (- x) y) (- 1)))))
+
+;; Mod_0
+  (assert (forall ((y Int)) (=> (not (= y 0)) (= (mod 0 y) 0))))
+
+;; Div_1_left
+  (assert (forall ((y Int)) (=> (< 1 y) (= (div 1 y) 0))))
+
+;; Div_minus1_left
+  (assert (forall ((y Int)) (=> (< 1 y) (= (div (- 1) y) (- 1)))))
+
+;; Mod_1_left
+  (assert (forall ((y Int)) (=> (< 1 y) (= (mod 1 y) 1))))
+
+;; Mod_minus1_left
+  (assert
+  (forall ((y Int))
+  (! (=> (< 1 y) (= (mod (- 1) y) (- y 1))) :pattern ((mod (- 1) y)) )))
+
+;; Div_mult
+  (assert
+  (forall ((x Int) (y Int) (z Int))
+  (! (=> (< 0 x) (= (div (+ (* x y) z) x) (+ y (div z x)))) :pattern ((div (+ (* x y) z) x)) )))
+
+;; Mod_mult
+  (assert
+  (forall ((x Int) (y Int) (z Int))
+  (! (=> (< 0 x) (= (mod (+ (* x y) z) x) (mod z x))) :pattern ((mod (+ (* x y) z) x)) )))
+
+(define-fun mod2 ((x Int)
+  (y Int)) Int (ite (< 0 y) (mod x y) (+ (mod x y) y)))
+
+(declare-sort integer 0)
+
+(declare-fun integerqtint (integer) Int)
+
+;; integer'axiom
+  (assert
+  (forall ((i integer))
+  (and (<= (- 2147483648) (integerqtint i)) (<= (integerqtint i) 2147483647))))
+
+(define-fun in_range ((x Int)) Bool (and (<= (- 2147483648) x)
+                                    (<= x 2147483647)))
+
+(declare-fun attr__ATTRIBUTE_IMAGE (Int) us_image)
+
+(declare-fun attr__ATTRIBUTE_VALUE__pre_check (us_image) Bool)
+
+(declare-fun attr__ATTRIBUTE_VALUE (us_image) Int)
+
+(declare-fun user_eq (integer integer) Bool)
+
+(declare-const dummy integer)
+
+(declare-datatypes ((integer__ref 0))
+(((integer__refqtmk (integer__content integer)))))
+(define-fun integer__ref_integer__content__projection ((a integer__ref)) integer 
+  (integer__content a))
+
+(define-fun dynamic_invariant ((temp___expr_18 Int) (temp___is_init_14 Bool)
+  (temp___skip_constant_15 Bool) (temp___do_toplevel_16 Bool)
+  (temp___do_typ_inv_17 Bool)) Bool (=>
+                                    (or (= temp___is_init_14 true)
+                                    (<= (- 2147483648) 2147483647)) (in_range
+                                    temp___expr_18)))
+
+(declare-const input Int)
+
+(declare-const attr__ATTRIBUTE_ADDRESS Int)
+
+(declare-const attr__ATTRIBUTE_ADDRESS1 Int)
+
+(declare-const attr__ATTRIBUTE_ADDRESS2 Int)
+
+(declare-const attr__ATTRIBUTE_ADDRESS3 Int)
+
+(assert
+;; defqtvc
+ ;; File "where_are_the_run_time_errors.adb", line 2, characters 0-0
+  (not
+  (forall ((x Int) (y Int) (k Int) (k1 Int) (x1 Int))
+  (=> (dynamic_invariant input true false true true)
+  (=> (dynamic_invariant x false false true true)
+  (=> (dynamic_invariant y false false true true)
+  (=> (dynamic_invariant k false false true true)
+  (=> (= k1 (div1 input 100))
+  (=> (= x1 2)
+  (let ((o (+ k1 5)))
+  (=> (in_range o)
+  (forall ((y1 Int))
+  (=> (= y1 o)
+  (forall ((x2 Int) (y2 Int))
+  (=>
+  (ite (< x1 10)
+  (exists ((temp___loop_entry_159 Int))
+  (and (= temp___loop_entry_159 y1)
+  (let ((o1 (+ y1 3)))
+  (and (in_range o1)
+  (exists ((y3 Int))
+  (and (= y3 o1)
+  (let ((o2 (+ x1 1)))
+  (and (in_range o2)
+  (exists ((x3 Int))
+  (and (= x3 o2)
+  (let ((o3 (- x3 2)))
+  (and (in_range o3)
+  (let ((o4 (* 3 o3)))
+  (and (in_range o4)
+  (and (in_range (+ temp___loop_entry_159 o4))
+  (and (and (= y2 (+ temp___loop_entry_159 (* 3 (- x2 2)))) (<= 3 x2))
+  (and
+  (and (dynamic_invariant x2 false true true true) (dynamic_invariant y2
+  false true true true)) (not (< x2 10)))))))))))))))))))
+  (and (= x2 x1) (= y2 y1)))
+  (let ((o1 (* 3 k1)))
+  (=> (in_range o1)
+  (let ((o2 (+ o1 100)))
+  (=> (in_range o2)
+  (forall ((spark__branch Bool))
+  (=> (= spark__branch (ite (< 43 o2) true false))
+  (=> (= spark__branch true)
+  (let ((o3 (+ y2 1)))
+  (=> (in_range o3)
+  (forall ((y3 Int))
+  (=> (= y3 o3)
+  (let ((o4 (- x2 y3))) (=> (in_range o4) (in_range (div1 x2 o4))))))))))))))))))))))))))))))
+(check-sat)