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") ){
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;
}
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)
{
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)
{
--- /dev/null
+; 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)
projects / cvc5.git / commitdiff