From c6a9ab9da205df7cbf192edc142ee151404dcb1b Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 19 Feb 2020 15:15:22 -0600 Subject: [PATCH] Delay enumerative instantiation if theory engine does not need check (#3774) --- .../quantifiers/inst_strategy_enumerative.cpp | 7 +- src/theory/quantifiers/sygus/synth_engine.cpp | 2 +- src/theory/quantifiers/term_database.cpp | 2 +- src/theory/quantifiers_engine.cpp | 18 +- src/theory/quantifiers_engine.h | 9 +- test/regress/CMakeLists.txt | 1 + .../quantifiers/issue3481-unsat1.smt2 | 270 ++++++++++++++++++ 7 files changed, 301 insertions(+), 8 deletions(-) create mode 100644 test/regress/regress1/quantifiers/issue3481-unsat1.smt2 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) -- 2.30.2