From e0cb8bb45344e9579a520b4b49a79a58671b71d9 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Tue, 20 Jul 2021 11:23:56 +0200
Subject: [PATCH 1/2] Add regression tests for #33 #35 #36 #37
---
tests/sat/bug36.smt2 | 11 +
tests/unsat/bug37.smt2 | 1234 ++++++++++++++++++++++++++++++++++++++
tests/unsat/issue33.smt2 | 9 +
tests/unsat/issue35.smt2 | 17 +
4 files changed, 1271 insertions(+)
create mode 100644 tests/sat/bug36.smt2
create mode 100644 tests/unsat/bug37.smt2
create mode 100644 tests/unsat/issue33.smt2
create mode 100644 tests/unsat/issue35.smt2
diff --git a/tests/sat/bug36.smt2 b/tests/sat/bug36.smt2
new file mode 100644
index 000000000..050585122
--- /dev/null
+++ b/tests/sat/bug36.smt2
@@ -0,0 +1,11 @@
+;; produced by colibri.drv ;;
+(set-logic ALL)
+
+(declare-fun bool_eq (Real Real) Bool)
+(declare-const x Int)
+(declare-fun to_big_real (Int) Real)
+
+(assert
+ (not
+ (= (bool_eq (to_big_real x) (fp.to_real ((_ to_fp 11 53) RNE (to_real x)))) true)))
+(check-sat)
diff --git a/tests/unsat/bug37.smt2 b/tests/unsat/bug37.smt2
new file mode 100644
index 000000000..6b8d3bd7c
--- /dev/null
+++ b/tests/unsat/bug37.smt2
@@ -0,0 +1,1234 @@
+;; produced by colibri.drv ;;
+(set-logic ALL)
+(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-fun index_bool (Bool) Int)
+
+;; index_bool_True
+ (assert (= (index_bool true) 0))
+
+;; index_bool_False
+ (assert (= (index_bool false) 1))
+
+;; bool_inversion
+ (assert (forall ((u Bool)) (or (= u true) (= u false))))
+
+(declare-sort tuple0 0)
+
+(declare-const Tuple0 tuple0)
+
+;; tuple0_inversion
+ (assert (forall ((u tuple0)) (= u 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-sort us_type_of_heap__ref 0)
+
+(declare-fun us_type_of_heap__refqtmk (us_type_of_heap) us_type_of_heap__ref)
+
+(declare-fun us_type_of_heap__content (us_type_of_heap__ref) us_type_of_heap)
+
+;; __type_of_heap__content'def
+ (assert
+ (forall ((u us_type_of_heap))
+ (= (us_type_of_heap__content (us_type_of_heap__refqtmk u)) u)))
+
+;; __type_of_heap__ref_inversion
+ (assert
+ (forall ((u us_type_of_heap__ref))
+ (! (= u (us_type_of_heap__refqtmk (us_type_of_heap__content u))) :pattern (
+ (us_type_of_heap__content u)) )))
+
+(declare-sort us_image 0)
+
+(declare-sort int__ref 0)
+
+(declare-fun int__refqtmk (Int) int__ref)
+
+(declare-fun int__content (int__ref) Int)
+
+;; int__content'def
+ (assert (forall ((u Int)) (= (int__content (int__refqtmk u)) u)))
+
+;; int__ref_inversion
+ (assert
+ (forall ((u int__ref))
+ (! (= u (int__refqtmk (int__content u))) :pattern ((int__content u)) )))
+
+(declare-sort bool__ref 0)
+
+(declare-fun bool__refqtmk (Bool) bool__ref)
+
+(declare-fun bool__content (bool__ref) Bool)
+
+;; bool__content'def
+ (assert (forall ((u Bool)) (= (bool__content (bool__refqtmk u)) u)))
+
+;; bool__ref_inversion
+ (assert
+ (forall ((u bool__ref))
+ (! (= u (bool__refqtmk (bool__content u))) :pattern ((bool__content u)) )))
+
+(declare-sort us_fixed__ref 0)
+
+(declare-fun us_fixed__refqtmk (Int) us_fixed__ref)
+
+(declare-fun us_fixed__content (us_fixed__ref) Int)
+
+;; __fixed__content'def
+ (assert (forall ((u Int)) (= (us_fixed__content (us_fixed__refqtmk u)) u)))
+
+;; __fixed__ref_inversion
+ (assert
+ (forall ((u us_fixed__ref))
+ (! (= u (us_fixed__refqtmk (us_fixed__content u))) :pattern ((us_fixed__content
+ u)) )))
+
+(declare-sort real__ref 0)
+
+(declare-fun real__refqtmk (Real) real__ref)
+
+(declare-fun real__content (real__ref) Real)
+
+;; real__content'def
+ (assert (forall ((u Real)) (= (real__content (real__refqtmk u)) u)))
+
+;; real__ref_inversion
+ (assert
+ (forall ((u real__ref))
+ (! (= u (real__refqtmk (real__content u))) :pattern ((real__content u)) )))
+
+(declare-sort us_private__ref 0)
+
+(declare-fun us_private__refqtmk (us_private) us_private__ref)
+
+(declare-fun us_private__content (us_private__ref) us_private)
+
+;; __private__content'def
+ (assert
+ (forall ((u us_private))
+ (= (us_private__content (us_private__refqtmk u)) u)))
+
+;; __private__ref_inversion
+ (assert
+ (forall ((u us_private__ref))
+ (! (= u (us_private__refqtmk (us_private__content u))) :pattern ((us_private__content
+ u)) )))
+
+(define-fun int__ref___projection ((a1 int__ref)) Int (int__content a1))
+
+(define-fun us_fixed__ref___projection ((a1 us_fixed__ref)) Int (us_fixed__content
+ a1))
+
+(define-fun bool__ref___projection ((a1 bool__ref)) Bool (bool__content a1))
+
+(define-fun real__ref___projection ((a1 real__ref)) Real (real__content a1))
+
+(define-fun us_private__ref___projection ((a1 us_private__ref)) us_private
+ (us_private__content a1))
+
+(declare-fun nth ((_ BitVec 8) Int) Bool)
+
+(declare-fun lsr ((_ BitVec 8) Int) (_ BitVec 8))
+
+(declare-fun asr ((_ BitVec 8) Int) (_ BitVec 8))
+
+(declare-fun lsl ((_ BitVec 8) Int) (_ BitVec 8))
+
+;; 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)) )))
+
+(declare-fun rotate_right1 ((_ BitVec 8) Int) (_ BitVec 8))
+
+(declare-fun rotate_left1 ((_ BitVec 8) Int) (_ BitVec 8))
+
+(declare-fun pow2 (Int) Int)
+
+(declare-const two_power_size_minus_one Int)
+
+;; two_power_size_minus_one_val
+ (assert (= two_power_size_minus_one (pow2 (- 8 1))))
+
+(define-fun to_int1 ((x (_ BitVec 8))) Int (ite (bvsge x (_ bv0 8))
+ (bv2nat x) (- (- 256 (bv2nat x)))))
+
+(define-fun uint_in_range ((i Int)) Bool (and (<= 0 i) (<= i 255)))
+
+;; lsr_bv_is_lsr
+ (assert
+ (forall ((x (_ BitVec 8)) (n (_ BitVec 8)))
+ (= (bvlshr x n) (lsr x (bv2nat n)))))
+
+;; asr_bv_is_asr
+ (assert
+ (forall ((x (_ BitVec 8)) (n (_ BitVec 8)))
+ (= (bvashr x n) (asr x (bv2nat n)))))
+
+;; lsl_bv_is_lsl
+ (assert
+ (forall ((x (_ BitVec 8)) (n (_ BitVec 8)))
+ (= (bvshl x n) (lsl x (bv2nat n)))))
+
+;; rotate_left_bv_is_rotate_left
+ (assert
+ (forall ((v (_ BitVec 8)) (n (_ BitVec 8)))
+ (= (bvor (bvshl v (bvurem n (_ bv8 8))) (bvlshr v (bvsub (_ bv8 8) (bvurem n (_ bv8 8)))))
+ (rotate_left1 v (bv2nat n)))))
+
+;; rotate_right_bv_is_rotate_right
+ (assert
+ (forall ((v (_ BitVec 8)) (n (_ BitVec 8)))
+ (= (bvor (bvlshr v (bvurem n (_ bv8 8))) (bvshl v (bvsub (_ bv8 8) (bvurem n (_ bv8 8)))))
+ (rotate_right1 v (bv2nat n)))))
+
+(declare-fun nth_bv ((_ BitVec 8) (_ BitVec 8)) Bool)
+
+;; nth_bv_def
+ (assert
+ (forall ((x (_ BitVec 8)) (i (_ BitVec 8)))
+ (= (= (nth_bv x i) true) (not (= (bvand (bvlshr x i) #x01) #x00)))))
+
+;; Nth_bv_is_nth
+ (assert
+ (forall ((x (_ BitVec 8)) (i (_ BitVec 8)))
+ (= (nth x (bv2nat i)) (nth_bv x i))))
+
+;; Nth_bv_is_nth2
+ (assert
+ (forall ((x (_ BitVec 8)) (i Int))
+ (=> (and (<= 0 i) (< i 256)) (= (nth_bv x ((_ int2bv 8) i)) (nth x i)))))
+
+(declare-fun eq_sub_bv ((_ BitVec 8) (_ BitVec 8) (_ BitVec 8)
+ (_ BitVec 8)) Bool)
+
+;; eq_sub_bv_def
+ (assert
+ (forall ((a1 (_ BitVec 8)) (b (_ BitVec 8)) (i (_ BitVec 8))
+ (n (_ BitVec 8)))
+ (let ((mask (bvshl (bvsub (bvshl #x01 n) #x01) i)))
+ (= (eq_sub_bv a1 b i n) (= (bvand b mask) (bvand a1 mask))))))
+
+(define-fun eq_sub ((a1 (_ BitVec 8)) (b (_ BitVec 8)) (i Int)
+ (n Int)) Bool (forall ((j Int))
+ (=> (and (<= i j) (< j (+ i n))) (= (nth a1 j) (nth b j)))))
+
+;; eq_sub_equiv
+ (assert
+ (forall ((a1 (_ BitVec 8)) (b (_ BitVec 8)) (i (_ BitVec 8))
+ (n (_ BitVec 8)))
+ (= (eq_sub a1 b (bv2nat i) (bv2nat n)) (eq_sub_bv a1 b i n))))
+
+(declare-sort t__ref 0)
+
+(declare-fun t__refqtmk ((_ BitVec 8)) t__ref)
+
+(declare-fun t__content (t__ref) (_ BitVec 8))
+
+;; t__content'def
+ (assert (forall ((u (_ BitVec 8))) (= (t__content (t__refqtmk u)) u)))
+
+;; t__ref_inversion
+ (assert
+ (forall ((u t__ref))
+ (! (= u (t__refqtmk (t__content u))) :pattern ((t__content u)) )))
+
+(declare-fun power ((_ BitVec 8) Int) (_ BitVec 8))
+
+(define-fun bv_min ((x (_ BitVec 8))
+ (y (_ BitVec 8))) (_ BitVec 8) (ite (bvule x y) x y))
+
+(define-fun bv_max ((x (_ BitVec 8))
+ (y (_ BitVec 8))) (_ BitVec 8) (ite (bvule x y) y x))
+
+(define-fun uc_of_int ((x Int)) (_ BitVec 8) (ite (<= 0 x) ((_ int2bv 8) x)
+ (bvneg ((_ int2bv 8) (- x)))))
+
+(define-fun uc_to_int ((x (_ BitVec 8))) Int (ite (= (bvult x ((_ int2bv 8)
+ two_power_size_minus_one)) true)
+ (bv2nat x)
+ (- (bv2nat (bvneg x)))))
+
+(define-fun in_range ((x Int)) Bool (or (= x 0) (= x 1)))
+
+(declare-fun attr__ATTRIBUTE_IMAGE (Bool) us_image)
+
+(declare-fun attr__ATTRIBUTE_VALUE__pre_check (us_image) Bool)
+
+(declare-fun attr__ATTRIBUTE_VALUE (us_image) Bool)
+
+(declare-sort byte 0)
+
+(declare-const attr__ATTRIBUTE_MODULUS (_ BitVec 8))
+
+(declare-fun attr__ATTRIBUTE_IMAGE1 ((_ BitVec 8)) us_image)
+
+(declare-fun attr__ATTRIBUTE_VALUE__pre_check1 (us_image) Bool)
+
+(declare-fun attr__ATTRIBUTE_VALUE1 (us_image) (_ BitVec 8))
+
+(declare-fun user_eq (byte byte) Bool)
+
+(declare-const dummy byte)
+
+(declare-sort byte__ref 0)
+
+(declare-fun byte__refqtmk (byte) byte__ref)
+
+(declare-fun byte__content (byte__ref) byte)
+
+;; byte__content'def
+ (assert (forall ((u byte)) (= (byte__content (byte__refqtmk u)) u)))
+
+;; byte__ref_inversion
+ (assert
+ (forall ((u byte__ref))
+ (! (= u (byte__refqtmk (byte__content u))) :pattern ((byte__content u)) )))
+
+(define-fun byte__ref_byte__content__projection ((a1 byte__ref)) byte
+ (byte__content a1))
+
+(declare-fun to_rep (byte) (_ BitVec 8))
+
+(declare-fun of_rep ((_ BitVec 8)) byte)
+
+;; inversion_axiom
+ (assert
+ (forall ((x byte)) (! (= (of_rep (to_rep x)) x) :pattern ((to_rep x)) )))
+
+;; range_axiom
+ (assert true)
+
+;; coerce_axiom
+ (assert
+ (forall ((x (_ BitVec 8)))
+ (! (= (to_rep (of_rep x)) x) :pattern ((to_rep (of_rep x))) )))
+
+(define-fun to_int2 ((x byte)) Int (bv2nat (to_rep x)))
+
+;; range_int_axiom
+ (assert
+ (forall ((x byte)) (! (uint_in_range (to_int2 x)) :pattern ((to_int2 x)) )))
+
+(declare-sort map__ref 0)
+
+(declare-fun map__refqtmk ((Array Int byte)) map__ref)
+
+(declare-fun map__content (map__ref) (Array Int byte))
+
+;; map__content'def
+ (assert
+ (forall ((u (Array Int byte))) (= (map__content (map__refqtmk u)) u)))
+
+;; map__ref_inversion
+ (assert
+ (forall ((u map__ref))
+ (! (= u (map__refqtmk (map__content u))) :pattern ((map__content u)) )))
+
+(declare-fun slide ((Array Int byte) Int Int) (Array Int byte))
+
+;; slide_eq
+ (assert
+ (forall ((a1 (Array Int byte)))
+ (forall ((first Int))
+ (! (= (slide a1 first first) a1) :pattern ((slide a1 first first)) ))))
+
+;; slide_def
+ (assert
+ (forall ((a1 (Array Int byte)))
+ (forall ((old_first Int))
+ (forall ((new_first Int))
+ (forall ((i Int))
+ (! (= (select (slide a1 old_first new_first) i) (select a1 (- i (- new_first old_first)))) :pattern ((select
+ (slide a1 old_first new_first) i)) ))))))
+
+(define-fun bool_eq ((a1 (Array Int byte)) (a__first Int) (a__last Int)
+ (b (Array Int byte)) (b__first Int)
+ (b__last Int)) Bool (ite (and
+ (ite (<= a__first a__last)
+ (and (<= b__first b__last)
+ (= (- a__last a__first) (- b__last b__first)))
+ (< b__last b__first))
+ (forall ((temp___idx_161 Int))
+ (=>
+ (and (<= a__first temp___idx_161)
+ (<= temp___idx_161 a__last))
+ (= (to_rep (select a1 temp___idx_161)) (to_rep
+ (select b (+ (- b__first a__first) temp___idx_161)))))))
+ true false))
+
+;; bool_eq_rev
+ (assert
+ (forall ((a1 (Array Int byte)) (b (Array Int byte)))
+ (forall ((a__first Int) (a__last Int) (b__first Int) (b__last Int))
+ (=> (= (bool_eq b b__first b__last a1 a__first a__last) true)
+ (and
+ (ite (<= a__first a__last)
+ (and (<= b__first b__last) (= (- a__last a__first) (- b__last b__first)))
+ (< b__last b__first))
+ (forall ((temp___idx_161 Int))
+ (=> (and (<= a__first temp___idx_161) (<= temp___idx_161 a__last))
+ (= (to_rep (select a1 temp___idx_161)) (to_rep
+ (select b (+ (- b__first a__first) temp___idx_161)))))))))))
+
+(declare-const d (Array Int byte))
+
+(declare-sort bit_count 0)
+
+(declare-fun bit_countqtint (bit_count) Int)
+
+;; bit_count'axiom
+ (assert
+ (forall ((i bit_count))
+ (and (<= 0 (bit_countqtint i)) (<= (bit_countqtint i) 8))))
+
+(define-fun in_range1 ((x Int)) Bool (and (<= 0 x) (<= x 8)))
+
+(declare-fun attr__ATTRIBUTE_IMAGE2 (Int) us_image)
+
+(declare-fun attr__ATTRIBUTE_VALUE__pre_check2 (us_image) Bool)
+
+(declare-fun attr__ATTRIBUTE_VALUE2 (us_image) Int)
+
+(declare-fun user_eq1 (bit_count bit_count) Bool)
+
+(declare-const dummy1 bit_count)
+
+(declare-sort bit_count__ref 0)
+
+(declare-fun bit_count__refqtmk (bit_count) bit_count__ref)
+
+(declare-fun bit_count__content (bit_count__ref) bit_count)
+
+;; bit_count__content'def
+ (assert
+ (forall ((u bit_count)) (= (bit_count__content (bit_count__refqtmk u)) u)))
+
+;; bit_count__ref_inversion
+ (assert
+ (forall ((u bit_count__ref))
+ (! (= u (bit_count__refqtmk (bit_count__content u))) :pattern ((bit_count__content
+ u)) )))
+
+(define-fun bit_count__ref_bit_count__content__projection ((a1 bit_count__ref)) bit_count
+ (bit_count__content a1))
+
+(define-fun to_rep1 ((x bit_count)) Int (bit_countqtint x))
+
+(declare-fun of_rep1 (Int) bit_count)
+
+;; inversion_axiom
+ (assert
+ (forall ((x bit_count))
+ (! (= (of_rep1 (to_rep1 x)) x) :pattern ((to_rep1 x)) )))
+
+;; range_axiom
+ (assert
+ (forall ((x bit_count)) (! (in_range1
+ (to_rep1 x)) :pattern ((to_rep1 x)) )))
+
+;; coerce_axiom
+ (assert
+ (forall ((x Int))
+ (! (=> (in_range1 x) (= (to_rep1 (of_rep1 x)) x)) :pattern ((to_rep1
+ (of_rep1 x))) )))
+
+(declare-sort map__ref1 0)
+
+(declare-fun map__refqtmk1 ((Array (_ BitVec 8) bit_count)) map__ref1)
+
+(declare-fun map__content1 (map__ref1) (Array (_ BitVec 8) bit_count))
+
+;; map__content'def
+ (assert
+ (forall ((u (Array (_ BitVec 8) bit_count)))
+ (= (map__content1 (map__refqtmk1 u)) u)))
+
+;; map__ref_inversion
+ (assert
+ (forall ((u map__ref1))
+ (! (= u (map__refqtmk1 (map__content1 u))) :pattern ((map__content1 u)) )))
+
+(declare-fun slide1 ((Array (_ BitVec 8) bit_count) (_ BitVec 8)
+ (_ BitVec 8)) (Array (_ BitVec 8) bit_count))
+
+;; slide_eq
+ (assert
+ (forall ((a1 (Array (_ BitVec 8) bit_count)))
+ (forall ((first (_ BitVec 8)))
+ (! (= (slide1 a1 first first) a1) :pattern ((slide1 a1 first first)) ))))
+
+;; slide_def
+ (assert
+ (forall ((a1 (Array (_ BitVec 8) bit_count)))
+ (forall ((old_first (_ BitVec 8)))
+ (forall ((new_first (_ BitVec 8)))
+ (forall ((i (_ BitVec 8)))
+ (! (= (select (slide1 a1 old_first new_first) i) (select a1 (bvsub i (bvsub new_first old_first)))) :pattern ((select
+ (slide1 a1 old_first new_first) i)) ))))))
+
+(define-fun bool_eq1 ((a1 (Array (_ BitVec 8) bit_count))
+ (a__first (_ BitVec 8)) (a__last (_ BitVec 8))
+ (b (Array (_ BitVec 8) bit_count)) (b__first (_ BitVec 8))
+ (b__last (_ BitVec 8))) Bool (ite (and
+ (ite (bvule a__first a__last)
+ (and (bvule b__first b__last)
+ (= (bvsub a__last a__first) (bvsub b__last b__first)))
+ (bvugt b__first b__last))
+ (forall ((temp___idx_163 (_ BitVec 8)))
+ (=>
+ (and (bvule a__first temp___idx_163)
+ (bvule temp___idx_163 a__last))
+ (= (to_rep1 (select a1 temp___idx_163))
+ (to_rep1
+ (select b (bvadd (bvsub b__first a__first) temp___idx_163)))))))
+ true false))
+
+;; bool_eq_rev
+ (assert
+ (forall ((a1 (Array (_ BitVec 8) bit_count))
+ (b (Array (_ BitVec 8) bit_count)))
+ (forall ((a__first (_ BitVec 8)) (a__last (_ BitVec 8))
+ (b__first (_ BitVec 8)) (b__last (_ BitVec 8)))
+ (=> (= (bool_eq1 b b__first b__last a1 a__first a__last) true)
+ (and
+ (ite (bvule a__first a__last)
+ (and (bvule b__first b__last)
+ (= (bvsub a__last a__first) (bvsub b__last b__first)))
+ (bvugt b__first b__last))
+ (forall ((temp___idx_163 (_ BitVec 8)))
+ (=> (and (bvule a__first temp___idx_163) (bvule temp___idx_163 a__last))
+ (= (to_rep1 (select a1 temp___idx_163)) (to_rep1
+ (select b (bvadd (bvsub b__first a__first) temp___idx_163)))))))))))
+
+(declare-const bit_count_c (Array (_ BitVec 8) bit_count))
+
+(declare-sort seq_bit_count 0)
+
+(declare-fun seq_bit_countqtint (seq_bit_count) Int)
+
+;; seq_bit_count'axiom
+ (assert
+ (forall ((i seq_bit_count))
+ (and (<= 0 (seq_bit_countqtint i)) (<= (seq_bit_countqtint i) 20000))))
+
+(define-fun in_range2 ((x Int)) Bool (and (<= 0 x) (<= x 20000)))
+
+(declare-fun attr__ATTRIBUTE_IMAGE3 (Int) us_image)
+
+(declare-fun attr__ATTRIBUTE_VALUE__pre_check3 (us_image) Bool)
+
+(declare-fun attr__ATTRIBUTE_VALUE3 (us_image) Int)
+
+(declare-fun user_eq2 (seq_bit_count seq_bit_count) Bool)
+
+(declare-const dummy2 seq_bit_count)
+
+(declare-sort seq_bit_count__ref 0)
+
+(declare-fun seq_bit_count__refqtmk (seq_bit_count) seq_bit_count__ref)
+
+(declare-fun seq_bit_count__content (seq_bit_count__ref) seq_bit_count)
+
+;; seq_bit_count__content'def
+ (assert
+ (forall ((u seq_bit_count))
+ (= (seq_bit_count__content (seq_bit_count__refqtmk u)) u)))
+
+;; seq_bit_count__ref_inversion
+ (assert
+ (forall ((u seq_bit_count__ref))
+ (! (= u (seq_bit_count__refqtmk (seq_bit_count__content u))) :pattern (
+ (seq_bit_count__content u)) )))
+
+(define-fun seq_bit_count__ref_seq_bit_count__content__projection ((a1 seq_bit_count__ref)) seq_bit_count
+ (seq_bit_count__content a1))
+
+(define-fun dynamic_invariant ((temp___expr_459 Int)
+ (temp___is_init_455 Bool) (temp___skip_constant_456 Bool)
+ (temp___do_toplevel_457 Bool)
+ (temp___do_typ_inv_458 Bool)) Bool (=>
+ (or (= temp___is_init_455 true)
+ (<= 0 20000)) (in_range2
+ temp___expr_459)))
+
+(declare-fun temp_____aggregate_def_164 (Int Int Int Int Int Int Int Int Int
+ Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int
+ Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int
+ Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int
+ Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int
+ Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int
+ Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int
+ Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int
+ Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int
+ Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int
+ Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int
+ Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int
+ Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int
+ Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int Int
+ Int) (Array (_ BitVec 8) bit_count))
+
+(define-fun dynamic_invariant1 ((temp___expr_468 Int)
+ (temp___is_init_464 Bool) (temp___skip_constant_465 Bool)
+ (temp___do_toplevel_466 Bool)
+ (temp___do_typ_inv_467 Bool)) Bool (=>
+ (or (= temp___is_init_464 true)
+ (<= 0 8)) (in_range1 temp___expr_468)))
+
+;; bit_count_c__def_axiom
+ (assert
+ (= bit_count_c (let ((temp___423 (temp_____aggregate_def_164 0 1 1 2 1 2 2
+ 3 1 2 2 3 2 3 3 4 1 2 2 3 2 3 3 4 2 3 3 4
+ 3 4 4 5 1 2 2 3 2 3 3 4 2 3 3 4 3 4 4 5 2
+ 3 3 4 3 4 4 5 3 4 4 5 4 5 5 6 1 2 2 3 2 3
+ 3 4 2 3 3 4 3 4 4 5 2 3 3 4 3 4 4 5 3 4 4
+ 5 4 5 5 6 2 3 3 4 3 4 4 5 3 4 4 5 4 5 5 6
+ 3 4 4 5 4 5 5 6 4 5 5 6 5 6 6 7 1 2 2 3 2
+ 3 3 4 2 3 3 4 3 4 4 5 2 3 3 4 3 4 4 5 3 4
+ 4 5 4 5 5 6 2 3 3 4 3 4 4 5 3 4 4 5 4 5 5
+ 6 3 4 4 5 4 5 5 6 4 5 5 6 5 6 6 7 2 3 3 4
+ 3 4 4 5 3 4 4 5 4 5 5 6 3 4 4 5 4 5 5 6 4
+ 5 5 6 5 6 6 7 3 4 4 5 4 5 5 6 4 5 5 6 5 6
+ 6 7 4 5 5 6 5 6 6 7 5 6 6 7 6 7 7 8)))
+ temp___423)))
+
+(declare-const rliteral bit_count)
+
+;; rliteral_axiom
+ (assert (= (bit_countqtint rliteral) 0))
+
+(declare-const rliteral1 bit_count)
+
+;; rliteral_axiom
+ (assert (= (bit_countqtint rliteral1) 1))
+
+(declare-const rliteral2 bit_count)
+
+;; rliteral_axiom
+ (assert (= (bit_countqtint rliteral2) 2))
+
+(declare-const rliteral3 bit_count)
+
+;; rliteral_axiom
+ (assert (= (bit_countqtint rliteral3) 3))
+
+(declare-const rliteral4 bit_count)
+
+;; rliteral_axiom
+ (assert (= (bit_countqtint rliteral4) 4))
+
+(declare-const rliteral5 bit_count)
+
+;; rliteral_axiom
+ (assert (= (bit_countqtint rliteral5) 5))
+
+(declare-const rliteral6 bit_count)
+
+;; rliteral_axiom
+ (assert (= (bit_countqtint rliteral6) 6))
+
+(declare-const rliteral7 bit_count)
+
+;; rliteral_axiom
+ (assert (= (bit_countqtint rliteral7) 7))
+
+(declare-const rliteral8 bit_count)
+
+;; rliteral_axiom
+ (assert (= (bit_countqtint rliteral8) 8))
+
+;; def_axiom
+ (assert
+ (forall ((temp___166 Int) (temp___167 Int) (temp___168 Int)
+ (temp___169 Int) (temp___170 Int) (temp___171 Int) (temp___172 Int)
+ (temp___173 Int) (temp___174 Int) (temp___175 Int) (temp___176 Int)
+ (temp___177 Int) (temp___178 Int) (temp___179 Int) (temp___180 Int)
+ (temp___181 Int) (temp___182 Int) (temp___183 Int) (temp___184 Int)
+ (temp___185 Int) (temp___186 Int) (temp___187 Int) (temp___188 Int)
+ (temp___189 Int) (temp___190 Int) (temp___191 Int) (temp___192 Int)
+ (temp___193 Int) (temp___194 Int) (temp___195 Int) (temp___196 Int)
+ (temp___197 Int) (temp___198 Int) (temp___199 Int) (temp___200 Int)
+ (temp___201 Int) (temp___202 Int) (temp___203 Int) (temp___204 Int)
+ (temp___205 Int) (temp___206 Int) (temp___207 Int) (temp___208 Int)
+ (temp___209 Int) (temp___210 Int) (temp___211 Int) (temp___212 Int)
+ (temp___213 Int) (temp___214 Int) (temp___215 Int) (temp___216 Int)
+ (temp___217 Int) (temp___218 Int) (temp___219 Int) (temp___220 Int)
+ (temp___221 Int) (temp___222 Int) (temp___223 Int) (temp___224 Int)
+ (temp___225 Int) (temp___226 Int) (temp___227 Int) (temp___228 Int)
+ (temp___229 Int) (temp___230 Int) (temp___231 Int) (temp___232 Int)
+ (temp___233 Int) (temp___234 Int) (temp___235 Int) (temp___236 Int)
+ (temp___237 Int) (temp___238 Int) (temp___239 Int) (temp___240 Int)
+ (temp___241 Int) (temp___242 Int) (temp___243 Int) (temp___244 Int)
+ (temp___245 Int) (temp___246 Int) (temp___247 Int) (temp___248 Int)
+ (temp___249 Int) (temp___250 Int) (temp___251 Int) (temp___252 Int)
+ (temp___253 Int) (temp___254 Int) (temp___255 Int) (temp___256 Int)
+ (temp___257 Int) (temp___258 Int) (temp___259 Int) (temp___260 Int)
+ (temp___261 Int) (temp___262 Int) (temp___263 Int) (temp___264 Int)
+ (temp___265 Int) (temp___266 Int) (temp___267 Int) (temp___268 Int)
+ (temp___269 Int) (temp___270 Int) (temp___271 Int) (temp___272 Int)
+ (temp___273 Int) (temp___274 Int) (temp___275 Int) (temp___276 Int)
+ (temp___277 Int) (temp___278 Int) (temp___279 Int) (temp___280 Int)
+ (temp___281 Int) (temp___282 Int) (temp___283 Int) (temp___284 Int)
+ (temp___285 Int) (temp___286 Int) (temp___287 Int) (temp___288 Int)
+ (temp___289 Int) (temp___290 Int) (temp___291 Int) (temp___292 Int)
+ (temp___293 Int) (temp___294 Int) (temp___295 Int) (temp___296 Int)
+ (temp___297 Int) (temp___298 Int) (temp___299 Int) (temp___300 Int)
+ (temp___301 Int) (temp___302 Int) (temp___303 Int) (temp___304 Int)
+ (temp___305 Int) (temp___306 Int) (temp___307 Int) (temp___308 Int)
+ (temp___309 Int) (temp___310 Int) (temp___311 Int) (temp___312 Int)
+ (temp___313 Int) (temp___314 Int) (temp___315 Int) (temp___316 Int)
+ (temp___317 Int) (temp___318 Int) (temp___319 Int) (temp___320 Int)
+ (temp___321 Int) (temp___322 Int) (temp___323 Int) (temp___324 Int)
+ (temp___325 Int) (temp___326 Int) (temp___327 Int) (temp___328 Int)
+ (temp___329 Int) (temp___330 Int) (temp___331 Int) (temp___332 Int)
+ (temp___333 Int) (temp___334 Int) (temp___335 Int) (temp___336 Int)
+ (temp___337 Int) (temp___338 Int) (temp___339 Int) (temp___340 Int)
+ (temp___341 Int) (temp___342 Int) (temp___343 Int) (temp___344 Int)
+ (temp___345 Int) (temp___346 Int) (temp___347 Int) (temp___348 Int)
+ (temp___349 Int) (temp___350 Int) (temp___351 Int) (temp___352 Int)
+ (temp___353 Int) (temp___354 Int) (temp___355 Int) (temp___356 Int)
+ (temp___357 Int) (temp___358 Int) (temp___359 Int) (temp___360 Int)
+ (temp___361 Int) (temp___362 Int) (temp___363 Int) (temp___364 Int)
+ (temp___365 Int) (temp___366 Int) (temp___367 Int) (temp___368 Int)
+ (temp___369 Int) (temp___370 Int) (temp___371 Int) (temp___372 Int)
+ (temp___373 Int) (temp___374 Int) (temp___375 Int) (temp___376 Int)
+ (temp___377 Int) (temp___378 Int) (temp___379 Int) (temp___380 Int)
+ (temp___381 Int) (temp___382 Int) (temp___383 Int) (temp___384 Int)
+ (temp___385 Int) (temp___386 Int) (temp___387 Int) (temp___388 Int)
+ (temp___389 Int) (temp___390 Int) (temp___391 Int) (temp___392 Int)
+ (temp___393 Int) (temp___394 Int) (temp___395 Int) (temp___396 Int)
+ (temp___397 Int) (temp___398 Int) (temp___399 Int) (temp___400 Int)
+ (temp___401 Int) (temp___402 Int) (temp___403 Int) (temp___404 Int)
+ (temp___405 Int) (temp___406 Int) (temp___407 Int) (temp___408 Int)
+ (temp___409 Int) (temp___410 Int) (temp___411 Int) (temp___412 Int)
+ (temp___413 Int) (temp___414 Int) (temp___415 Int) (temp___416 Int)
+ (temp___417 Int) (temp___418 Int) (temp___419 Int) (temp___420 Int)
+ (temp___421 Int))
+ (let ((temp___165 (temp_____aggregate_def_164 temp___166 temp___167
+ temp___168 temp___169 temp___170 temp___171 temp___172
+ temp___173 temp___174 temp___175 temp___176 temp___177
+ temp___178 temp___179 temp___180 temp___181 temp___182
+ temp___183 temp___184 temp___185 temp___186 temp___187
+ temp___188 temp___189 temp___190 temp___191 temp___192
+ temp___193 temp___194 temp___195 temp___196 temp___197
+ temp___198 temp___199 temp___200 temp___201 temp___202
+ temp___203 temp___204 temp___205 temp___206 temp___207
+ temp___208 temp___209 temp___210 temp___211 temp___212
+ temp___213 temp___214 temp___215 temp___216 temp___217
+ temp___218 temp___219 temp___220 temp___221 temp___222
+ temp___223 temp___224 temp___225 temp___226 temp___227
+ temp___228 temp___229 temp___230 temp___231 temp___232
+ temp___233 temp___234 temp___235 temp___236 temp___237
+ temp___238 temp___239 temp___240 temp___241 temp___242
+ temp___243 temp___244 temp___245 temp___246 temp___247
+ temp___248 temp___249 temp___250 temp___251 temp___252
+ temp___253 temp___254 temp___255 temp___256 temp___257
+ temp___258 temp___259 temp___260 temp___261 temp___262
+ temp___263 temp___264 temp___265 temp___266 temp___267
+ temp___268 temp___269 temp___270 temp___271 temp___272
+ temp___273 temp___274 temp___275 temp___276 temp___277
+ temp___278 temp___279 temp___280 temp___281 temp___282
+ temp___283 temp___284 temp___285 temp___286 temp___287
+ temp___288 temp___289 temp___290 temp___291 temp___292
+ temp___293 temp___294 temp___295 temp___296 temp___297
+ temp___298 temp___299 temp___300 temp___301 temp___302
+ temp___303 temp___304 temp___305 temp___306 temp___307
+ temp___308 temp___309 temp___310 temp___311 temp___312
+ temp___313 temp___314 temp___315 temp___316 temp___317
+ temp___318 temp___319 temp___320 temp___321 temp___322
+ temp___323 temp___324 temp___325 temp___326 temp___327
+ temp___328 temp___329 temp___330 temp___331 temp___332
+ temp___333 temp___334 temp___335 temp___336 temp___337
+ temp___338 temp___339 temp___340 temp___341 temp___342
+ temp___343 temp___344 temp___345 temp___346 temp___347
+ temp___348 temp___349 temp___350 temp___351 temp___352
+ temp___353 temp___354 temp___355 temp___356 temp___357
+ temp___358 temp___359 temp___360 temp___361 temp___362
+ temp___363 temp___364 temp___365 temp___366 temp___367
+ temp___368 temp___369 temp___370 temp___371 temp___372
+ temp___373 temp___374 temp___375 temp___376 temp___377
+ temp___378 temp___379 temp___380 temp___381 temp___382
+ temp___383 temp___384 temp___385 temp___386 temp___387
+ temp___388 temp___389 temp___390 temp___391 temp___392
+ temp___393 temp___394 temp___395 temp___396 temp___397
+ temp___398 temp___399 temp___400 temp___401 temp___402
+ temp___403 temp___404 temp___405 temp___406 temp___407
+ temp___408 temp___409 temp___410 temp___411 temp___412
+ temp___413 temp___414 temp___415 temp___416 temp___417
+ temp___418 temp___419 temp___420 temp___421)))
+ (and
+ (and (= (select temp___165 #x00) rliteral)
+ (= (select temp___165 #x01) rliteral1))
+ (and
+ (and
+ (and
+ (and
+ (and
+ (and
+ (and
+ (and (= (select temp___165 #x02) rliteral1)
+ (= (select temp___165 #x03) rliteral2))
+ (and (= (select temp___165 #x04) rliteral1)
+ (= (select temp___165 #x05) rliteral2)))
+ (and
+ (and (= (select temp___165 #x06) rliteral2)
+ (= (select temp___165 #x07) rliteral3))
+ (and (= (select temp___165 #x08) rliteral1)
+ (= (select temp___165 #x09) rliteral2))))
+ (and
+ (and
+ (and (= (select temp___165 #x0A) rliteral2)
+ (= (select temp___165 #x0B) rliteral3))
+ (and (= (select temp___165 #x0C) rliteral2)
+ (= (select temp___165 #x0D) rliteral3)))
+ (and
+ (and (= (select temp___165 #x0E) rliteral3)
+ (= (select temp___165 #x0F) rliteral4))
+ (and (= (select temp___165 #x10) rliteral1)
+ (= (select temp___165 #x11) rliteral2)))))
+ (and
+ (and
+ (and
+ (and (= (select temp___165 #x12) rliteral2)
+ (= (select temp___165 #x13) rliteral3))
+ (and (= (select temp___165 #x14) rliteral2)
+ (= (select temp___165 #x15) rliteral3)))
+ (and
+ (and (= (select temp___165 #x16) rliteral3)
+ (= (select temp___165 #x17) rliteral4))
+ (and (= (select temp___165 #x18) rliteral2)
+ (= (select temp___165 #x19) rliteral3))))
+ (and
+ (and
+ (and (= (select temp___165 #x1A) rliteral3)
+ (= (select temp___165 #x1B) rliteral4))
+ (and (= (select temp___165 #x1C) rliteral3)
+ (= (select temp___165 #x1D) rliteral4)))
+ (and
+ (and (= (select temp___165 #x1E) rliteral4)
+ (= (select temp___165 #x1F) rliteral5))
+ (and (= (select temp___165 #x20) rliteral1)
+ (= (select temp___165 #x21) rliteral2))))))
+ (and
+ (and
+ (and
+ (and
+ (and (= (select temp___165 #x22) rliteral2)
+ (= (select temp___165 #x23) rliteral3))
+ (and (= (select temp___165 #x24) rliteral2)
+ (= (select temp___165 #x25) rliteral3)))
+ (and
+ (and (= (select temp___165 #x26) rliteral3)
+ (= (select temp___165 #x27) rliteral4))
+ (and (= (select temp___165 #x28) rliteral2)
+ (= (select temp___165 #x29) rliteral3))))
+ (and
+ (and
+ (and (= (select temp___165 #x2A) rliteral3)
+ (= (select temp___165 #x2B) rliteral4))
+ (and (= (select temp___165 #x2C) rliteral3)
+ (= (select temp___165 #x2D) rliteral4)))
+ (and
+ (and (= (select temp___165 #x2E) rliteral4)
+ (= (select temp___165 #x2F) rliteral5))
+ (and (= (select temp___165 #x30) rliteral2)
+ (= (select temp___165 #x31) rliteral3)))))
+ (and
+ (and
+ (and
+ (and (= (select temp___165 #x32) rliteral3)
+ (= (select temp___165 #x33) rliteral4))
+ (and (= (select temp___165 #x34) rliteral3)
+ (= (select temp___165 #x35) rliteral4)))
+ (and
+ (and (= (select temp___165 #x36) rliteral4)
+ (= (select temp___165 #x37) rliteral5))
+ (and (= (select temp___165 #x38) rliteral3)
+ (= (select temp___165 #x39) rliteral4))))
+ (and
+ (and
+ (and (= (select temp___165 #x3A) rliteral4)
+ (= (select temp___165 #x3B) rliteral5))
+ (and (= (select temp___165 #x3C) rliteral4)
+ (= (select temp___165 #x3D) rliteral5)))
+ (and
+ (and (= (select temp___165 #x3E) rliteral5)
+ (= (select temp___165 #x3F) rliteral6))
+ (and (= (select temp___165 #x40) rliteral1)
+ (= (select temp___165 #x41) rliteral2)))))))
+ (and
+ (and
+ (and
+ (and
+ (and
+ (and (= (select temp___165 #x42) rliteral2)
+ (= (select temp___165 #x43) rliteral3))
+ (and (= (select temp___165 #x44) rliteral2)
+ (= (select temp___165 #x45) rliteral3)))
+ (and
+ (and (= (select temp___165 #x46) rliteral3)
+ (= (select temp___165 #x47) rliteral4))
+ (and (= (select temp___165 #x48) rliteral2)
+ (= (select temp___165 #x49) rliteral3))))
+ (and
+ (and
+ (and (= (select temp___165 #x4A) rliteral3)
+ (= (select temp___165 #x4B) rliteral4))
+ (and (= (select temp___165 #x4C) rliteral3)
+ (= (select temp___165 #x4D) rliteral4)))
+ (and
+ (and (= (select temp___165 #x4E) rliteral4)
+ (= (select temp___165 #x4F) rliteral5))
+ (and (= (select temp___165 #x50) rliteral2)
+ (= (select temp___165 #x51) rliteral3)))))
+ (and
+ (and
+ (and
+ (and (= (select temp___165 #x52) rliteral3)
+ (= (select temp___165 #x53) rliteral4))
+ (and (= (select temp___165 #x54) rliteral3)
+ (= (select temp___165 #x55) rliteral4)))
+ (and
+ (and (= (select temp___165 #x56) rliteral4)
+ (= (select temp___165 #x57) rliteral5))
+ (and (= (select temp___165 #x58) rliteral3)
+ (= (select temp___165 #x59) rliteral4))))
+ (and
+ (and
+ (and (= (select temp___165 #x5A) rliteral4)
+ (= (select temp___165 #x5B) rliteral5))
+ (and (= (select temp___165 #x5C) rliteral4)
+ (= (select temp___165 #x5D) rliteral5)))
+ (and
+ (and (= (select temp___165 #x5E) rliteral5)
+ (= (select temp___165 #x5F) rliteral6))
+ (and (= (select temp___165 #x60) rliteral2)
+ (= (select temp___165 #x61) rliteral3))))))
+ (and
+ (and
+ (and
+ (and
+ (and (= (select temp___165 #x62) rliteral3)
+ (= (select temp___165 #x63) rliteral4))
+ (and (= (select temp___165 #x64) rliteral3)
+ (= (select temp___165 #x65) rliteral4)))
+ (and
+ (and (= (select temp___165 #x66) rliteral4)
+ (= (select temp___165 #x67) rliteral5))
+ (and (= (select temp___165 #x68) rliteral3)
+ (= (select temp___165 #x69) rliteral4))))
+ (and
+ (and
+ (and (= (select temp___165 #x6A) rliteral4)
+ (= (select temp___165 #x6B) rliteral5))
+ (and (= (select temp___165 #x6C) rliteral4)
+ (= (select temp___165 #x6D) rliteral5)))
+ (and
+ (and (= (select temp___165 #x6E) rliteral5)
+ (= (select temp___165 #x6F) rliteral6))
+ (and (= (select temp___165 #x70) rliteral3)
+ (= (select temp___165 #x71) rliteral4)))))
+ (and
+ (and
+ (and
+ (and (= (select temp___165 #x72) rliteral4)
+ (= (select temp___165 #x73) rliteral5))
+ (and (= (select temp___165 #x74) rliteral4)
+ (= (select temp___165 #x75) rliteral5)))
+ (and
+ (and (= (select temp___165 #x76) rliteral5)
+ (= (select temp___165 #x77) rliteral6))
+ (and (= (select temp___165 #x78) rliteral4)
+ (= (select temp___165 #x79) rliteral5))))
+ (and
+ (and
+ (and (= (select temp___165 #x7A) rliteral5)
+ (= (select temp___165 #x7B) rliteral6))
+ (and (= (select temp___165 #x7C) rliteral5)
+ (= (select temp___165 #x7D) rliteral6)))
+ (and
+ (and (= (select temp___165 #x7E) rliteral6)
+ (= (select temp___165 #x7F) rliteral7))
+ (= (select temp___165 #x80) rliteral1)))))))
+ (and
+ (and
+ (and
+ (and
+ (and
+ (and
+ (and (= (select temp___165 #x81) rliteral2)
+ (= (select temp___165 #x82) rliteral2))
+ (and (= (select temp___165 #x83) rliteral3)
+ (= (select temp___165 #x84) rliteral2)))
+ (and
+ (and (= (select temp___165 #x85) rliteral3)
+ (= (select temp___165 #x86) rliteral3))
+ (and (= (select temp___165 #x87) rliteral4)
+ (= (select temp___165 #x88) rliteral2))))
+ (and
+ (and
+ (and (= (select temp___165 #x89) rliteral3)
+ (= (select temp___165 #x8A) rliteral3))
+ (and (= (select temp___165 #x8B) rliteral4)
+ (= (select temp___165 #x8C) rliteral3)))
+ (and
+ (and (= (select temp___165 #x8D) rliteral4)
+ (= (select temp___165 #x8E) rliteral4))
+ (and (= (select temp___165 #x8F) rliteral5)
+ (= (select temp___165 #x90) rliteral2)))))
+ (and
+ (and
+ (and
+ (and (= (select temp___165 #x91) rliteral3)
+ (= (select temp___165 #x92) rliteral3))
+ (and (= (select temp___165 #x93) rliteral4)
+ (= (select temp___165 #x94) rliteral3)))
+ (and
+ (and (= (select temp___165 #x95) rliteral4)
+ (= (select temp___165 #x96) rliteral4))
+ (and (= (select temp___165 #x97) rliteral5)
+ (= (select temp___165 #x98) rliteral3))))
+ (and
+ (and
+ (and (= (select temp___165 #x99) rliteral4)
+ (= (select temp___165 #x9A) rliteral4))
+ (and (= (select temp___165 #x9B) rliteral5)
+ (= (select temp___165 #x9C) rliteral4)))
+ (and
+ (and (= (select temp___165 #x9D) rliteral5)
+ (= (select temp___165 #x9E) rliteral5))
+ (and (= (select temp___165 #x9F) rliteral6)
+ (= (select temp___165 #xA0) rliteral2))))))
+ (and
+ (and
+ (and
+ (and
+ (and (= (select temp___165 #xA1) rliteral3)
+ (= (select temp___165 #xA2) rliteral3))
+ (and (= (select temp___165 #xA3) rliteral4)
+ (= (select temp___165 #xA4) rliteral3)))
+ (and
+ (and (= (select temp___165 #xA5) rliteral4)
+ (= (select temp___165 #xA6) rliteral4))
+ (and (= (select temp___165 #xA7) rliteral5)
+ (= (select temp___165 #xA8) rliteral3))))
+ (and
+ (and
+ (and (= (select temp___165 #xA9) rliteral4)
+ (= (select temp___165 #xAA) rliteral4))
+ (and (= (select temp___165 #xAB) rliteral5)
+ (= (select temp___165 #xAC) rliteral4)))
+ (and
+ (and (= (select temp___165 #xAD) rliteral5)
+ (= (select temp___165 #xAE) rliteral5))
+ (and (= (select temp___165 #xAF) rliteral6)
+ (= (select temp___165 #xB0) rliteral3)))))
+ (and
+ (and
+ (and
+ (and (= (select temp___165 #xB1) rliteral4)
+ (= (select temp___165 #xB2) rliteral4))
+ (and (= (select temp___165 #xB3) rliteral5)
+ (= (select temp___165 #xB4) rliteral4)))
+ (and
+ (and (= (select temp___165 #xB5) rliteral5)
+ (= (select temp___165 #xB6) rliteral5))
+ (and (= (select temp___165 #xB7) rliteral6)
+ (= (select temp___165 #xB8) rliteral4))))
+ (and
+ (and
+ (and (= (select temp___165 #xB9) rliteral5)
+ (= (select temp___165 #xBA) rliteral5))
+ (and (= (select temp___165 #xBB) rliteral6)
+ (= (select temp___165 #xBC) rliteral5)))
+ (and
+ (and (= (select temp___165 #xBD) rliteral6)
+ (= (select temp___165 #xBE) rliteral6))
+ (and (= (select temp___165 #xBF) rliteral7)
+ (= (select temp___165 #xC0) rliteral2)))))))
+ (and
+ (and
+ (and
+ (and
+ (and
+ (and (= (select temp___165 #xC1) rliteral3)
+ (= (select temp___165 #xC2) rliteral3))
+ (and (= (select temp___165 #xC3) rliteral4)
+ (= (select temp___165 #xC4) rliteral3)))
+ (and
+ (and (= (select temp___165 #xC5) rliteral4)
+ (= (select temp___165 #xC6) rliteral4))
+ (and (= (select temp___165 #xC7) rliteral5)
+ (= (select temp___165 #xC8) rliteral3))))
+ (and
+ (and
+ (and (= (select temp___165 #xC9) rliteral4)
+ (= (select temp___165 #xCA) rliteral4))
+ (and (= (select temp___165 #xCB) rliteral5)
+ (= (select temp___165 #xCC) rliteral4)))
+ (and
+ (and (= (select temp___165 #xCD) rliteral5)
+ (= (select temp___165 #xCE) rliteral5))
+ (and (= (select temp___165 #xCF) rliteral6)
+ (= (select temp___165 #xD0) rliteral3)))))
+ (and
+ (and
+ (and
+ (and (= (select temp___165 #xD1) rliteral4)
+ (= (select temp___165 #xD2) rliteral4))
+ (and (= (select temp___165 #xD3) rliteral5)
+ (= (select temp___165 #xD4) rliteral4)))
+ (and
+ (and (= (select temp___165 #xD5) rliteral5)
+ (= (select temp___165 #xD6) rliteral5))
+ (and (= (select temp___165 #xD7) rliteral6)
+ (= (select temp___165 #xD8) rliteral4))))
+ (and
+ (and
+ (and (= (select temp___165 #xD9) rliteral5)
+ (= (select temp___165 #xDA) rliteral5))
+ (and (= (select temp___165 #xDB) rliteral6)
+ (= (select temp___165 #xDC) rliteral5)))
+ (and
+ (and (= (select temp___165 #xDD) rliteral6)
+ (= (select temp___165 #xDE) rliteral6))
+ (and (= (select temp___165 #xDF) rliteral7)
+ (= (select temp___165 #xE0) rliteral3))))))
+ (and
+ (and
+ (and
+ (and
+ (and (= (select temp___165 #xE1) rliteral4)
+ (= (select temp___165 #xE2) rliteral4))
+ (and (= (select temp___165 #xE3) rliteral5)
+ (= (select temp___165 #xE4) rliteral4)))
+ (and
+ (and (= (select temp___165 #xE5) rliteral5)
+ (= (select temp___165 #xE6) rliteral5))
+ (and (= (select temp___165 #xE7) rliteral6)
+ (= (select temp___165 #xE8) rliteral4))))
+ (and
+ (and
+ (and (= (select temp___165 #xE9) rliteral5)
+ (= (select temp___165 #xEA) rliteral5))
+ (and (= (select temp___165 #xEB) rliteral6)
+ (= (select temp___165 #xEC) rliteral5)))
+ (and
+ (and (= (select temp___165 #xED) rliteral6)
+ (= (select temp___165 #xEE) rliteral6))
+ (and (= (select temp___165 #xEF) rliteral7)
+ (= (select temp___165 #xF0) rliteral4)))))
+ (and
+ (and
+ (and
+ (and (= (select temp___165 #xF1) rliteral5)
+ (= (select temp___165 #xF2) rliteral5))
+ (and (= (select temp___165 #xF3) rliteral6)
+ (= (select temp___165 #xF4) rliteral5)))
+ (and
+ (and (= (select temp___165 #xF5) rliteral6)
+ (= (select temp___165 #xF6) rliteral6))
+ (and (= (select temp___165 #xF7) rliteral7)
+ (= (select temp___165 #xF8) rliteral5))))
+ (and
+ (and
+ (and (= (select temp___165 #xF9) rliteral6)
+ (= (select temp___165 #xFA) rliteral6))
+ (and (= (select temp___165 #xFB) rliteral7)
+ (= (select temp___165 #xFC) rliteral6)))
+ (and
+ (and (= (select temp___165 #xFD) rliteral7)
+ (= (select temp___165 #xFE) rliteral7))
+ (= (select temp___165 #xFF) rliteral8))))))))))))
+
+(define-fun dynamic_invariant2 ((temp___expr_435 (_ BitVec 8))
+ (temp___is_init_431 Bool) (temp___skip_constant_432 Bool)
+ (temp___do_toplevel_433 Bool) (temp___do_typ_inv_434 Bool)) Bool true)
+
+(declare-const total_ones Int)
+
+;; Assume
+ (assert
+ (= (temp_____aggregate_def_164 0 1 1 2 1 2 2 3 1 2 2 3 2 3 3 4 1 2 2 3 2 3
+ 3 4 2 3 3 4 3 4 4 5 1 2 2 3 2 3 3 4 2 3 3 4 3 4 4 5 2 3 3 4 3 4 4 5 3 4
+ 4 5 4 5 5 6 1 2 2 3 2 3 3 4 2 3 3 4 3 4 4 5 2 3 3 4 3 4 4 5 3 4 4 5 4 5
+ 5 6 2 3 3 4 3 4 4 5 3 4 4 5 4 5 5 6 3 4 4 5 4 5 5 6 4 5 5 6 5 6 6 7 1 2
+ 2 3 2 3 3 4 2 3 3 4 3 4 4 5 2 3 3 4 3 4 4 5 3 4 4 5 4 5 5 6 2 3 3 4 3 4
+ 4 5 3 4 4 5 4 5 5 6 3 4 4 5 4 5 5 6 4 5 5 6 5 6 6 7 2 3 3 4 3 4 4 5 3 4
+ 4 5 4 5 5 6 3 4 4 5 4 5 5 6 4 5 5 6 5 6 6 7 3 4 4 5 4 5 5 6 4 5 5 6 5 6
+ 6 7 4 5 5 6 5 6 6 7 5 6 6 7 6 7 7 8) bit_count_c))
+
+;; Assume
+ (assert (dynamic_invariant total_ones false false true true))
+
+;; H
+ (assert
+ (= (and (ite (<= 1 1) true false) (ite (<= 1 2500) true false)) true))
+
+(declare-const total_ones1 Int)
+
+(declare-const i Int)
+
+;; H
+ (assert
+ (= (and (ite (dynamic_invariant total_ones1 false true true true) true
+ false) (ite (and (<= 1 i) (<= i 2500)) true false)) true))
+
+(assert
+;; defqtvc
+ ;; File "r.ads", line 13, characters 0-0
+ (not
+ (<= (+ total_ones1 (to_rep1 (select bit_count_c (to_rep (select d i))))) 20000)))
+(check-sat)
diff --git a/tests/unsat/issue33.smt2 b/tests/unsat/issue33.smt2
new file mode 100644
index 000000000..4885dcb9b
--- /dev/null
+++ b/tests/unsat/issue33.smt2
@@ -0,0 +1,9 @@
+(set-logic ALL)
+(set-info :smt-lib-version 2.6)
+
+(declare-const a Int)
+(declare-const b Int)
+
+(assert (not (= b 0)))
+(assert (not (= (colibri_cdiv (- a) b) (- (colibri_cdiv a b)))))
+(check-sat)
diff --git a/tests/unsat/issue35.smt2 b/tests/unsat/issue35.smt2
new file mode 100644
index 000000000..6ef61912f
--- /dev/null
+++ b/tests/unsat/issue35.smt2
@@ -0,0 +1,17 @@
+(set-logic ALL)
+(set-info :smt-lib-version 2.6)
+
+(declare-const a Int)
+(declare-const b Int)
+
+(define-fun mod1 ((x Int) (y Int)) Int
+ (ite (or (and (< 0 x) (< 0 y)) (and (< x 0) (< y 0)))
+ (colibri_crem x y)
+ (ite (= (colibri_crem x y) 0) 0 (+ (colibri_crem x y) y))))
+
+(define-fun same_sign ((x Int) (y Int)) Bool
+ (or (and (<= 0 x) (<= 0 y)) (and (<= x 0) (<= y 0))))
+
+(assert (not (= b 0)))
+(assert (not (= (same_sign (mod1 a b) b) true)))
+(check-sat)
--
GitLab
From 036e9ab2086327b0ff5a36af8dd3ec9e39af6279 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Tue, 20 Jul 2021 11:30:13 +0200
Subject: [PATCH 2/2] Import from Bin:a1af7a0 Src:c5147cc9e farith:a93db57
Fixes #33 #35 #36 #37
---
Src/COLIBRI/arith.pl | 863 +++++++++++++++-------------
Src/COLIBRI/col_solve.pl | 4 +-
Src/COLIBRI/lp_arith.pl | 48 +-
Src/COLIBRI/ndelta.pl | 28 +-
Src/COLIBRI/realarith.pl | 121 ++--
Src/COLIBRI/smt_import.pl | 11 +-
Src/COLIBRI/solve.pl | 314 ++++++++--
test.sh | 10 +-
tests/{unsat => unknown}/bug37.smt2 | 0
9 files changed, 905 insertions(+), 494 deletions(-)
rename tests/{unsat => unknown}/bug37.smt2 (100%)
diff --git a/Src/COLIBRI/arith.pl b/Src/COLIBRI/arith.pl
index 067f4a30d..0c9c3dba0 100755
--- a/Src/COLIBRI/arith.pl
+++ b/Src/COLIBRI/arith.pl
@@ -2108,128 +2108,132 @@ copy_delta(A,B,CA,CB) :-
%% Multiplication intervalle par intervalle de Val1 par Val2
%% Puis intersection du domaine calcule
%% avec celui de la variable resultat (Val)
+mult_interval(0,Val2,Val) ?- !,
+ protected_unify(Val,0).
+mult_interval(Val1,0,Val) ?- !,
+ protected_unify(Val,0).
mult_interval(Val1,Val2,Val) :-
- (get_type(Val,_) ->
- true
- ; % Val non initialise
- mfd:dvar_range(Val1,Low1,High1),
- mfd:dvar_range(Val2,Low2,High2),
- mult_intervals(Low1..High1,Low2..High2,Low,High),
- mfd:quiet_set_intervals(Val,[Low..High])),
- (integer(Val) ->
- true
- ; update_args_from_delta(Rel12,Delta,Val1,Val2),
- mfd:get_intervals(Val1,Inter1),
+ (get_type(Val,_) ->
+ true
+ ; % Val non initialise
+ mfd:dvar_range(Val1,Low1,High1),
+ mfd:dvar_range(Val2,Low2,High2),
+ mult_intervals(Low1..High1,Low2..High2,Low,High),
+ mfd:quiet_set_intervals(Val,[Low..High])),
+ (integer(Val) ->
+ true
+ ; update_args_from_delta(Rel12,Delta,Val1,Val2),
+ mfd:get_intervals(Val1,Inter1),
mfd:get_intervals(Val2,Inter2),
mfd:get_intervals(Val,Inter),
- ((Inter1 == Inter, number_in_interval(Inter2,1);
- Inter2 == Inter, number_in_interval(Inter1,1))
- ->
- %% Le 1 de Inter1|Inter2 copie Inter2|Inter1 dans Inter
- %% Inutile de continuer
- true
- ; ((Inter1 = [I1],
- Inter2 = [I2])
- ->
- binop_intervals_Rel(Rel12,mult,I1,I2,L,H),
- %% mult_intervals(I1,I2,L,H),
- interval_from_bounds(L,H,NInter),
- LInter = [NInter]
- ; L1 is length(Inter1),
- L2 is length(Inter2),
- getval(max_prod_intervals,MaxProd),
- (L1*L2 > MaxProd ->
- %% On ne travaille que sur les bornes
- %% en gardant le trou eventuel autour de 0
- mfd:dvar_range(Val1,Min1,Max1),
- mfd:dvar_range(Val2,Min2,Max2),
- keep_zero_hole(Inter1,Min1,Max1,NInter1),
- keep_zero_hole(Inter2,Min2,Max2,NInter2)
- ; NInter1 = Inter1,
- NInter2 = Inter2),
- mfd:dvar_range(Val,Min,Max),
- (Rel12 \== '?' ->
- %% On peut se limiter aux associations d'intervalles compatibles
- %% avec le delta, reduire ces intervalles selon le delta
- %% et synthetiser un delta a partir de ces intervalles
- (Min >= 0 ->
- %% Seules les variantes positives nous interessent
- %% Exemple: [A,B,C] #: -1000 .. 1000, gt(C, 0), lt(A, B), mult(A, B, C).
- %% --> A = A{[-1000 .. -2, 1 .. 999]}, B = B{[-500 .. -1, 1 .. 1000]}, C = C{[1 .. 1000]}
- %% et delta(A,B,+,1 .. 999)]
- split_neg_pos(NInter1,Neg1,Pos1,Z1),
- split_neg_pos(NInter2,Neg2,Pos2,Z2),
- binop_interval_list_delta(mult,Rel12,Delta,Neg1,Neg2,NNeg1,NNeg2,LInterP1,Delta1),
- binop_interval_list_delta(mult,Rel12,Delta,Pos1,Pos2,NPos1,NPos2,LInterP2,Delta2),
- min_max_inter(Delta1,LD1,HD1),min_max_inter(Delta2,LD2,HD2),
- min(LD1,LD2,Low),max(HD1,HD2,High),
- NDelta = Low..High,
- (var(Z1) ->
- append(NNeg1,NPos1,NNInter1)
- ; Zero_in_arg = 1,
- append(NNeg1,[0|NPos1],NNInter1)),
- (var(Z2) ->
- append(NNeg2,NPos2,NNInter2)
- ; Zero_in_arg = 1,
- append(NNeg2,[0|NPos2],NNInter2)),
- (var(Zero_in_arg) ->
- append(LInterP1,LInterP2,LInter)
- ; append(LInterP1,[0|LInterP2],LInter))
- ; (Max =< 0 ->
- %% Seules les variantes negatives nous interessent
- %% Exemple: [A,B,C] #: -1000 .. 1000, lt(C, 0), lt(A, B), mult(A, B, C).
- %% --> A = A{[-1000 .. -1]}, B = B{[1 .. 1000]}, C = C{[-1000 .. -1]}
- %% et delta(A,B,+,2 .. 2000), delta(C,A,+,0 .. 999)]
- split_neg_pos(NInter1,Neg1,Pos1,Z1),
- split_neg_pos(NInter2,Neg2,Pos2,Z2),
- binop_interval_list_delta(mult,Rel12,Delta,Neg1,Pos2,NNeg1,NPos2,LInterN1,Delta1),
- binop_interval_list_delta(mult,Rel12,Delta,Pos1,Neg2,NPos1,NNeg2,LInterN2,Delta2),
- min_max_inter(Delta1,LD1,HD1),min_max_inter(Delta2,LD2,HD2),
- min(LD1,LD2,Low),max(HD1,HD2,High),
- NDelta = Low..High,
- (var(Z1) ->
- append(NNeg1,NPos1,NNInter1)
- ; Zero_in_arg = 1,
- append(NNeg1,[0|NPos1],NNInter1)),
- (var(Z2) ->
- append(NNeg2,NPos2,NNInter2)
- ; Zero_in_arg = 1,
- append(NNeg2,[0|NPos2],NNInter2)),
- (var(Zero_in_arg) ->
- append(LInterN1,LInterN2,LInter)
- ; append(LInterN1,[0|LInterN2],LInter))
- ; binop_interval_list_delta(mult,Rel12,Delta,NInter1,NInter2,NNInter1,NNInter2,LInter,NDelta))),
- list_to_intervals(integer,NNInter1,NewInter1),
- mfd:quiet_set_intervals(Val1,NewInter1),
- list_to_intervals(integer,NNInter2,NewInter2),
- mfd:quiet_set_intervals(Val2,NewInter2),
- launch_delta(Val1,Val2,'+',NDelta)
- ; (Min >= 0 ->
- %% Seules les variantes positives nous interessent
- split_neg_pos(NInter1,NegL1,PosL1,Zero_in_arg),
- split_neg_pos(NInter2,NegL2,PosL2,Zero_in_arg),
- MinP is max(Min,1),
- mult_interval_list_nn(NegL1,NegL2,MinP,Max,LInterP1),
- mult_interval_list_pp(PosL1,PosL2,MinP,Max,LInterP2),
- (nonvar(Zero_in_arg) ->
- append([0|LInterP1],LInterP2,LInter)
- ; append(LInterP1,LInterP2,LInter))
- ; (Max =< 0 ->
- % Seules les variantes negatives nous interessent
- split_neg_pos(NInter1,NegL1,PosL1,Zero_in_arg),
- split_neg_pos(NInter2,NegL2,PosL2,Zero_in_arg),
- MaxN is min(Max,-1),
- mult_interval_list_np(NegL1,PosL2,Min,MaxN,LInterN1),
- mult_interval_list_np(NegL2,PosL1,Min,MaxN,LInterN2),
- (nonvar(Zero_in_arg) ->
- append([0|LInterN1],LInterN2,LInter)
- ; append(LInterN1,LInterN2,LInter))
- ; %% On calcule tout
- mult_interval_list(NInter1,NInter2,Min,Max,LInter))))),
- mfd:list_to_dom(LInter,dom(InterMult)),
- mfd:get_intervals(Val,Inter),
- mfd:dom_intersection(dom(InterMult),dom(Inter),NewDom),
- mfd:dvar_set(Val,NewDom))).
+ ((Inter1 == Inter, number_in_interval(Inter2,1);
+ Inter2 == Inter, number_in_interval(Inter1,1))
+ ->
+ % Le 1 de Inter1|Inter2 copie Inter2|Inter1 dans Inter
+ % Inutile de continuer
+ true
+ ; ((Inter1 = [I1],
+ Inter2 = [I2])
+ ->
+ binop_intervals_Rel(Rel12,mult,I1,I2,L,H),
+ % mult_intervals(I1,I2,L,H),
+ interval_from_bounds(L,H,NInter),
+ LInter = [NInter]
+ ; L1 is length(Inter1),
+ L2 is length(Inter2),
+ getval(max_prod_intervals,MaxProd),
+ (L1*L2 > MaxProd ->
+ % On ne travaille que sur les bornes
+ % en gardant le trou eventuel autour de 0
+ mfd:dvar_range(Val1,Min1,Max1),
+ mfd:dvar_range(Val2,Min2,Max2),
+ keep_zero_hole(Inter1,Min1,Max1,NInter1),
+ keep_zero_hole(Inter2,Min2,Max2,NInter2)
+ ; NInter1 = Inter1,
+ NInter2 = Inter2),
+ mfd:dvar_range(Val,Min,Max),
+ (Rel12 \== '?' ->
+ % On peut se limiter aux associations d'intervalles compatibles
+ % avec le delta, reduire ces intervalles selon le delta
+ % et synthetiser un delta a partir de ces intervalles
+ (Min >= 0 ->
+ % Seules les variantes positives nous interessent
+ % Exemple: [A,B,C] #: -1000 .. 1000, gt(C, 0), lt(A, B), mult(A, B, C).
+ % --> A = A{[-1000 .. -2, 1 .. 999]}, B = B{[-500 .. -1, 1 .. 1000]}, C = C{[1 .. 1000]}
+ % et delta(A,B,+,1 .. 999)]
+ split_neg_pos(NInter1,Neg1,Pos1,Z1),
+ split_neg_pos(NInter2,Neg2,Pos2,Z2),
+ binop_interval_list_delta(mult,Rel12,Delta,Neg1,Neg2,NNeg1,NNeg2,LInterP1,Delta1),
+ binop_interval_list_delta(mult,Rel12,Delta,Pos1,Pos2,NPos1,NPos2,LInterP2,Delta2),
+ min_max_inter(Delta1,LD1,HD1),min_max_inter(Delta2,LD2,HD2),
+ min(LD1,LD2,Low),max(HD1,HD2,High),
+ NDelta = Low..High,
+ (var(Z1) ->
+ append(NNeg1,NPos1,NNInter1)
+ ; Zero_in_arg = 1,
+ append(NNeg1,[0|NPos1],NNInter1)),
+ (var(Z2) ->
+ append(NNeg2,NPos2,NNInter2)
+ ; Zero_in_arg = 1,
+ append(NNeg2,[0|NPos2],NNInter2)),
+ (var(Zero_in_arg) ->
+ append(LInterP1,LInterP2,LInter)
+ ; append(LInterP1,[0|LInterP2],LInter))
+ ; (Max =< 0 ->
+ % Seules les variantes negatives nous interessent
+ % Exemple: [A,B,C] #: -1000 .. 1000, lt(C, 0), lt(A, B), mult(A, B, C).
+ % --> A = A{[-1000 .. -1]}, B = B{[1 .. 1000]}, C = C{[-1000 .. -1]}
+ % et delta(A,B,+,2 .. 2000), delta(C,A,+,0 .. 999)]
+ split_neg_pos(NInter1,Neg1,Pos1,Z1),
+ split_neg_pos(NInter2,Neg2,Pos2,Z2),
+ binop_interval_list_delta(mult,Rel12,Delta,Neg1,Pos2,NNeg1,NPos2,LInterN1,Delta1),
+ binop_interval_list_delta(mult,Rel12,Delta,Pos1,Neg2,NPos1,NNeg2,LInterN2,Delta2),
+ min_max_inter(Delta1,LD1,HD1),min_max_inter(Delta2,LD2,HD2),
+ min(LD1,LD2,Low),max(HD1,HD2,High),
+ NDelta = Low..High,
+ (var(Z1) ->
+ append(NNeg1,NPos1,NNInter1)
+ ; Zero_in_arg = 1,
+ append(NNeg1,[0|NPos1],NNInter1)),
+ (var(Z2) ->
+ append(NNeg2,NPos2,NNInter2)
+ ; Zero_in_arg = 1,
+ append(NNeg2,[0|NPos2],NNInter2)),
+ (var(Zero_in_arg) ->
+ append(LInterN1,LInterN2,LInter)
+ ; append(LInterN1,[0|LInterN2],LInter))
+ ; binop_interval_list_delta(mult,Rel12,Delta,NInter1,NInter2,NNInter1,NNInter2,LInter,NDelta))),
+ list_to_intervals(integer,NNInter1,NewInter1),
+ mfd:quiet_set_intervals(Val1,NewInter1),
+ list_to_intervals(integer,NNInter2,NewInter2),
+ mfd:quiet_set_intervals(Val2,NewInter2),
+ launch_delta(Val1,Val2,'+',NDelta)
+ ; (Min >= 0 ->
+ % Seules les variantes positives nous interessent
+ split_neg_pos(NInter1,NegL1,PosL1,Zero_in_arg),
+ split_neg_pos(NInter2,NegL2,PosL2,Zero_in_arg),
+ MinP is max(Min,1),
+ mult_interval_list_nn(NegL1,NegL2,MinP,Max,LInterP1),
+ mult_interval_list_pp(PosL1,PosL2,MinP,Max,LInterP2),
+ (nonvar(Zero_in_arg) ->
+ append([0|LInterP1],LInterP2,LInter)
+ ; append(LInterP1,LInterP2,LInter))
+ ; (Max =< 0 ->
+ % Seules les variantes negatives nous interessent
+ split_neg_pos(NInter1,NegL1,PosL1,Zero_in_arg),
+ split_neg_pos(NInter2,NegL2,PosL2,Zero_in_arg),
+ MaxN is min(Max,-1),
+ mult_interval_list_np(NegL1,PosL2,Min,MaxN,LInterN1),
+ mult_interval_list_np(NegL2,PosL1,Min,MaxN,LInterN2),
+ (nonvar(Zero_in_arg) ->
+ append([0|LInterN1],LInterN2,LInter)
+ ; append(LInterN1,LInterN2,LInter))
+ ; % On calcule tout
+ mult_interval_list(NInter1,NInter2,Min,Max,LInter))))),
+ mfd:list_to_dom(LInter,dom(InterMult)),
+ mfd:get_intervals(Val,Inter),
+ mfd:dom_intersection(dom(InterMult),dom(Inter),NewDom),
+ mfd:dvar_set(Val,NewDom))).
:- mode(mult_intervals(++,++,-,-)).
mult_intervals(ValInter1,ValInter2,B1,B2) :-
@@ -3327,9 +3331,9 @@ div_mod0(A, B, Q, BQ, R) :-
; MaxR = MaxA)),
mfd:set_intervals(R,[MinR..MaxR]),
ensure_absA_lt_absB(R,B),
- % minus(A,BQ,R),
+ % minus(A,BQ,R),
congr_mod_directe(A,B,R),
- congr_add_directe(BQ,R,A).
+ congr_add_directe(BQ,R,A).
div_mod_int(A, B, Q, BQ, R) :-
get_priority(Prio),
@@ -3337,6 +3341,7 @@ div_mod_int(A, B, Q, BQ, R) :-
save_cstr_suspensions((A,B,Q,BQ,R)),
(divides(B,A) ->
protected_unify(R,0),
+ protected_unify(BQ,A),
mult(B,Q,A)
; div_mod_int_bis(A, B, Q, BQ, R)),
check_dont_divide(A,B,Q,BQ,R),
@@ -3374,14 +3379,49 @@ div_mod_int_bis(A, B, Q, BQ, R) :-
check_exists_div_mod_int(A,B,Q,BQ,R) :-
get_saved_cstr_suspensions(LSusp),
- member((Susp,div_mod_int(V1,V2,Quot,V2Quot,Rem)),LSusp),
- V1==A,
- V2==B,
- !,
- kill_suspension(Susp),
- protected_unify(Quot = Q),
- protected_unify(V2Quot = BQ),
- protected_unify(Rem = R).
+ ((member((Susp,div_mod_int(V1,V2,Quot,V2Quot,RR)),LSusp),
+ once (V1 == A; V2 == B),
+ (V2 == B ->
+ (V1 == A ->
+ Fact = 1
+ ; member((_,op_int(CV1,OpCV1)),LSusp),
+ (A == CV1;
+ A == OpCV1),
+ OpR = 1)
+ ; V1 == A,
+ member((_,op_int(CV2,OpCV2)),LSusp),
+ (B == CV2;
+ B == OpCV2)))
+ ->
+ !,
+ (nonvar(Fact) ->
+ kill_suspension(Susp),
+ protected_unify(Quot = Q),
+ protected_unify(V2Quot = BQ),
+ protected_unify(Rem = R)
+ ; % A // B = Q et -A // B = -Q et R = -RR
+ % A // B = Q et A // -B = -Q et R = RR
+ % on sature
+ op_int(Q,Quot),
+ (nonvar(OpR) ->
+ op_int(R,RR)
+ ; protected_unify(R,RR)))
+ ; % A // B = Q et -A // -B = Q et R = -RR
+ once (member_begin_end((_,op_int(CV1,OpCV1)),LSusp,LSusp1,E1,E1),
+ (A == CV1, OpA = OpCV1;
+ A == OpCV1, OpA = CV1)),
+ once (member((_,op_int(CV2,OpCV2)),LSusp1),
+ (B == CV2, OpB = OpCV2;
+ B == OpCV2, OpB = CV2)),
+ save_cstr_suspensions((OpA,OpB)),
+ get_saved_cstr_suspensions(NLSusp),
+ setval(saved_suspensions,(1,LSusp)),
+ once (member((_,div_mod_int(V1,V2,Quot,_,RR)),NLSusp),
+ V1 == OpA,
+ V2 == OpB),
+ !,
+ protected_unify(Q,Quot),
+ op_int(R,RR)).
check_exists_div_mod_int(_,_,_,_,_).
@@ -3549,22 +3589,44 @@ single_var_factor_goal(power_int(U,_,P,A,_),A,Depth,Seen,NSeen,LA) ?- !,
single_var_factor_goal(_,A,Depth,Seen,[A|Seen],[A]).
+div_mod_inst_free(A, B, Q, BQ, R, Continue) :-
+ (Q == 1 ->
+ protected_unify(BQ,B)
+ ; true),
+ div_mod_inst(A, B, Q, BQ, R, Continue1),
+ (var(Continue1) ->
+ true
+ ; (number(Q) ->
+ % Q <> 0 donc A <> 0 et |A| >= |QB|
+ mfd:dvar_remove_element(A,0)
+ ; true),
+ div_mod_free(A, B, Q, BQ, R, Continue)).
+
%% On regarde les instanciations en details
% si A = 0 alors Q = R = 0
+div_mod_inst(0, B, Q, BQ, R, Continue) ?- !,
+ protected_unify(Q,0),
+ protected_unify(BQ,0),
+ protected_unify(R,0).
% si B = 1 alors Q = A et R = 0
+div_mod_inst(A, 1, Q, BQ, R, Continue) ?- !,
+ protected_unify(A,Q),
+ protected_unify(BQ,Q),
+ protected_unify(R,0).
% si B = -1 alors Q = -A et R = 0
+div_mod_inst(A, -1, Q, BQ, R, Continue) ?- !,
+ op_int(A,Q),
+ protected_unify(BQ,A),
+ protected_unify(R,0).
% si Q = 0 alors R = A et |A| < |B|
+div_mod_inst(A, B, 0, BQ, R, Continue) ?- !,
+ protected_unify(BQ,0),
+ protected_unify(R,A),
+ absA_lt_absB(A,B).
% si R = 0 alors B * Q = A
-div_mod_inst_free(A, B, Q, BQ, R, Continue) :-
- div_mod_inst(A, B, Q, BQ, R, Continue1),
- (var(Continue1) ->
- true
- ; (number(Q) ->
- %% Q <> 0 donc A <> 0 et |A| >= |QB|
- mfd:dvar_remove_element(A,0)
- ; true),
- div_mod_free(A, B, Q, BQ, R, Continue)).
-
+div_mod_inst(A, B, Q, BQ, 0, Continue) ?- !,
+ protected_unify(BQ,A),
+ mult(B,Q,A).
div_mod_inst(A, B, Q, BQ, R, Continue) :-
(integer(A) ->
(A == 0 ->
@@ -3609,7 +3671,7 @@ div_mod_inst(A, B, Q, BQ, R, Continue) :-
MinB0 is A // SQ,
(A < MinB0*SQ ->
MinB = MinB0
- ; MinB is MinB0 + 1)
+ ; MinB is MinB0 + 1)
; % A < 0
MinB is -(-A//Q),
MaxB0 is A // SQ,
@@ -3636,7 +3698,6 @@ div_mod_inst(A, B, Q, BQ, R, Continue) :-
no_lin_mult(B,Q,BQ),
no_lin_add(BQ,R,A),
absA_lt_absB(R,B)))
-
; (R == 0 ->
% si A mod B = 0 alors B * (A div B) = A
protected_unify(BQ,A),
@@ -3670,11 +3731,9 @@ div_mod_inst(A, B, Q, BQ, R, Continue) :-
absA_lt_absB(A,B)
; adjust_sign_from_Q(Q,A,B,R),
% A et R sont signes maintenant
- % On peut deleguer a A = BQ + R
- % car le add maintient |R| < [A|
BQ0 is B * Q,
protected_unify(BQ,BQ0),
- no_lin_add(BQ,R,A)))
+ Continue = 1))
; (R == 0 ->
% si A mod B = 0 alors B * (A div B) = A
protected_unify(BQ,A),
@@ -3704,39 +3763,49 @@ div_mod_inst(A, B, Q, BQ, R, Continue) :-
% si A mod B = 0 alors B * (A div B) = A
protected_unify(BQ,A),
no_lin_mult(B,Q,A)
- ; Continue = 1)))).
+ ; Continue = 1)))),
+ ((nonvar(A),
+ nonvar(B))
+ ->
+ % parano
+ QQ is A // B,
+ BQ is B*QQ,
+ protected_unify(Q,QQ),
+ RR is A rem B,
+ protected_unify(R,RR)
+ ; true).
%% Exploitation des identites et des opposes
%% - R est borne par A et du meme signe
%% - |B| > |R|
div_mod_free(A, B, Q, BQ, R, Continue) :-
- (A == B ->
- %% A = AQ + R
- protected_unify(Q = 1),
- protected_unify(R = 0),
- protected_unify(BQ = B)
- ; (A == Q ->
- %% A = AB + R (A=0 ou B=1)
- protected_unify(R = 0),
- protected_unify(BQ = A),
- no_lin_mult(B,Q,A)
- ; (A == R ->
- %% A = BQ + A alors Q = 0 et |A| < |B|
- protected_unify(Q = 0),
- protected_unify(BQ = 0),
- absA_lt_absB(A,B)
- ; (B == Q ->
- %% A = B*B + R avec A et R du meme signe et |A] >= |R]
- %% donc A et R positifs
- gt(A,0),
- geq(R,0),
- power(B,2,BQ),
- add(BQ,R,A)
- ; (B == R ->
- %% A = BQ+ B --> fail car |B| > |R|
- fail
- ; (A == BQ ->
+ (A == B ->
+ % A = AQ + R
+ protected_unify(Q = 1),
+ protected_unify(R = 0),
+ protected_unify(BQ = B)
+ ; (A == Q ->
+ % A = AB + R (A=0 ou B=1)
+ protected_unify(R = 0),
+ protected_unify(BQ = A),
+ no_lin_mult(B,Q,A)
+ ; (A == R ->
+ % A = BQ + A alors Q = 0 et |A| < |B|
+ protected_unify(Q = 0),
+ protected_unify(BQ = 0),
+ absA_lt_absB(A,B)
+ ; (B == Q ->
+ % A = B*B + R avec A et R du meme signe et |A] >= |R]
+ % donc A et R positifs
+ gt(A,0),
+ geq(R,0),
+ power(B,2,BQ),
+ add(BQ,R,A)
+ ; (B == R ->
+ % A = BQ+ B --> fail car |B| > |R|
+ fail
+ ; (A == BQ ->
mult(B,Q,A),
protected_unify(R,0)
; (check_absA_lt_absB(A,B) ->
@@ -3744,11 +3813,11 @@ div_mod_free(A, B, Q, BQ, R, Continue) :-
protected_unify(Q = 0),
protected_unify(BQ = 0),
protected_unify(R = A)
- ; (check_B_divides_A(A,B) ->
+ ; (check_B_divides_A(A,B) ->
protected_unify(R = 0),
protected_unify(BQ = A),
no_lin_mult(B,Q,A)
- ; % Exploitation des opposes
+ ; % Exploitation des opposes
check_exists_op_int_with_div_mod_args(A,B,Q,BQ,R,Continue1),
check_common_divisor(A,B,Q,R,Continue1,Continue))))))))).
@@ -3811,83 +3880,83 @@ check_common_divisor(A,B,Q,R,_,Continue) :-
%% div_mod(A,B,-B,BQ,R) --> A = - B^2 + R, R = A + B^2
%% Q <> 0, A et R negatifs, A < R
check_exists_op_int_with_div_mod_args(A,B,Q,BQ,R,_) :-
- get_saved_cstr_suspensions(LSusp),
- (member((Susp,op_int(X,Y)),LSusp),
- (((X,Y) == (A,B),VBQ = X; %% A//-A = Q, BQ = YQ = X
- (X,Y) == (B,A),VBQ = Y), %% -A//A = Q, BQ = XQ = Y
- Goal = (protected_unify(Q = -1),protected_unify(R = 0),protected_unify(BQ = VBQ));
- ((X,Y) == (A,R); %% A = BQ - A, sign(A)=sign(-A)
- (X,Y) == (R,A)), %% -A = BQ + A, sign(-A)=sign(A)
- Goal = (kill_suspension(Susp), protected_unify(A = 0),protected_unify(R = 0),protected_unify(Q = 0),protected_unify(BQ = 0));
- ((X,Y) == (B,R); %% -B = R, |B| > |R|, fail
- (X,Y) == (R,B)), %% B = -R, |B| > |R|, fail
- Goal = fail;
- ((X,Y) == (A,Q); %% A = -AB + R
- (X,Y) == (Q,A)), %% A = -AB + R
- Goal = (protected_unify(R = 0),protected_unify(A = BQ),no_lin_mult(B,Q,A));
- ((X,Y) == (B,Q); %% R = A + B^2
- (X,Y) == (Q,B)), %% R = A + B^2
- Goal = (lt(A,0),leq(R,0),power(B,2,BQ),no_lin_add(A,BQ,R)))),
- !,
- call(Goal).
+ get_saved_cstr_suspensions(LSusp),
+ (member((Susp,op_int(X,Y)),LSusp),
+ (((X,Y) == (A,B),VBQ = X; %% A//-A = Q, BQ = YQ = X
+ (X,Y) == (B,A),VBQ = Y), %% -A//A = Q, BQ = XQ = Y
+ Goal = (protected_unify(Q = -1),protected_unify(R = 0),protected_unify(BQ = VBQ));
+ ((X,Y) == (A,R); %% A = BQ - A, sign(A)=sign(-A)
+ (X,Y) == (R,A)), %% -A = BQ + A, sign(-A)=sign(A)
+ Goal = (kill_suspension(Susp), protected_unify(A = 0),protected_unify(R = 0),protected_unify(Q = 0),protected_unify(BQ = 0));
+ ((X,Y) == (B,R); %% -B = R, |B| > |R|, fail
+ (X,Y) == (R,B)), %% B = -R, |B| > |R|, fail
+ Goal = fail;
+ ((X,Y) == (A,Q); %% A = -AB + R
+ (X,Y) == (Q,A)), %% A = -AB + R
+ Goal = (protected_unify(R = 0),protected_unify(A = BQ),no_lin_mult(B,Q,A));
+ ((X,Y) == (B,Q); %% R = A + B^2
+ (X,Y) == (Q,B)), %% R = A + B^2
+ Goal = (lt(A,0),leq(R,0),power(B,2,BQ),no_lin_add(A,BQ,R)))),
+ !,
+ call(Goal).
check_exists_op_int_with_div_mod_args(A,B,Q,BQ,R,1).
%% On regarde si B divise A
%% (+/-)B*V2 = (+/-)A, A = BQ + R donc B divise A et R = 0
%% (+/-)B^N = (+/-)A, A = BQ + R donc B divise A et R = 0
check_B_divides_A(A,B) :-
- get_saved_cstr_suspensions(LSusp),
- filter_mult_pow_and_op_suspensions(LSusp,L1,L2),
- member((Goal,V),L1),
- same_or_op_int(A,V,L2),
- (Goal = mult(V1,V2),
- (same_or_op_int(V1,B,L2);
- same_or_op_int(V2,B,L2))
- ;
- Goal = pow(V1),
- same_or_op_int(V1,B,L2)).
+ get_saved_cstr_suspensions(LSusp),
+ filter_mult_pow_and_op_suspensions(LSusp,L1,L2),
+ member((Goal,V),L1),
+ same_or_op_int(A,V,L2),
+ (Goal = mult(V1,V2),
+ (same_or_op_int(V1,B,L2);
+ same_or_op_int(V2,B,L2))
+ ;
+ Goal = pow(V1),
+ same_or_op_int(V1,B,L2)).
filter_mult_pow_and_op_suspensions([],[],[]).
filter_mult_pow_and_op_suspensions([(_,Goal)|LSusp],L1,L2) :-
- (Goal = mult_int(V1,_,V2,_,V,_) ->
- L1 = [(mult(V1,V2),V)|EL1],
- filter_mult_pow_and_op_suspensions(LSusp,EL1,L2)
- ; (Goal = power_int(V1,_,_N,V,_) ->
- L1 = [(pow(V1),V)|EL1],
- filter_mult_pow_and_op_suspensions(LSusp,EL1,L2)
- ; (Goal = op_int(V1,V2) ->
- L2 = [(V1,V2)|EL2],
- filter_mult_pow_and_op_suspensions(LSusp,L1,EL2)
- ; filter_mult_pow_and_op_suspensions(LSusp,L1,L2)))).
+ (Goal = mult_int(V1,_,V2,_,V,_) ->
+ L1 = [(mult(V1,V2),V)|EL1],
+ filter_mult_pow_and_op_suspensions(LSusp,EL1,L2)
+ ; (Goal = power_int(V1,_,_N,V,_) ->
+ L1 = [(pow(V1),V)|EL1],
+ filter_mult_pow_and_op_suspensions(LSusp,EL1,L2)
+ ; (Goal = op_int(V1,V2) ->
+ L2 = [(V1,V2)|EL2],
+ filter_mult_pow_and_op_suspensions(LSusp,L1,EL2)
+ ; filter_mult_pow_and_op_suspensions(LSusp,L1,L2)))).
same_or_op_int(A,A,_) ?- !.
same_or_op_int(A,B,L) :-
- (number(A) ->
- number(B),
- B is -A
- ; (number(B) ->
- number(A),
- A is -B
- ; member((V1,V2),L),
- ((A,B) == (V1,V2);
- (A,B) == (V2,V1)))).
+ (number(A) ->
+ number(B),
+ B is -A
+ ; (number(B) ->
+ number(A),
+ A is -B
+ ; member((V1,V2),L),
+ ((A,B) == (V1,V2);
+ (A,B) == (V2,V1)))).
%% on regarde si |A| < |B|
check_absA_lt_absB(A,B) :-
- A \== B,
- (integer(A) ->
- MaxAbsA is abs(A)
- ; mfd:dvar_range(A,MinA,MaxA),
- MaxAbsA is max(abs(MinA),abs(MaxA))),
- (integer(B) ->
- MinAbsB is abs(B)
- ; mfd:get_intervals(B,IntB),
- mfd:mindomain(B,MinB),
- Abs is abs(MinB),
- abs_min(IntB,Abs,MinAbsB)),
- MaxAbsA < MinAbsB.
+ A \== B,
+ (integer(A) ->
+ MaxAbsA is abs(A)
+ ; mfd:dvar_range(A,MinA,MaxA),
+ MaxAbsA is max(abs(MinA),abs(MaxA))),
+ (integer(B) ->
+ MinAbsB is abs(B)
+ ; mfd:get_intervals(B,IntB),
+ mfd:mindomain(B,MinB),
+ Abs is abs(MinB),
+ abs_min(IntB,Abs,MinAbsB)),
+ MaxAbsA < MinAbsB.
%% Maintien des invariants dans A = BQ + R
%% - R est borne par A et du meme signe
@@ -4357,98 +4426,98 @@ check_div_int_ineqs1([S|LSusp],Seen,NSeen,A,B,Q,R,SA,SB) :-
%% Contrainte auxilliaire pour garantir |A| < |B|
absA_lt_absB(A,B) :-
- get_priority(Prio),
- set_priority(1),
- save_cstr_suspensions((A,B)),
- ensure_absA_lt_absB(A,B),
- (check_absA_lt_absB(A,B) ->
- true
- ; %% Si A et B du meme signe on peut deleguer a gt
- mfd:dvar_range(A,MinA,MaxA),
- mfd:dvar_range(B,MinB,MaxB),
- (MinA >= 0 ->
- (MinB >= 0 ->
- lin_gt_int(B,A),
+ get_priority(Prio),
+ set_priority(1),
+ save_cstr_suspensions((A,B)),
+ ensure_absA_lt_absB(A,B),
+ (check_absA_lt_absB(A,B) ->
+ true
+ ; % Si A et B du meme signe on peut deleguer a gt
+ mfd:dvar_range(A,MinA,MaxA),
+ mfd:dvar_range(B,MinB,MaxB),
+ (MinA >= 0 ->
+ (MinB >= 0 ->
+ lin_gt_int(B,A),
gt(B,A)
- ; Continue = 1)
- ; ((MaxA =< 0,
- MaxB =< 0)
- ->
- lin_gt_int(A,B),
+ ; Continue = 1)
+ ; ((MaxA =< 0,
+ MaxB =< 0)
+ ->
+ lin_gt_int(A,B),
gt(A,B)
- ; Continue = 1)),
- (var(Continue) ->
- true
- ; saturate_diff_int_inequalities(A,B,Continue1),
- (var(Continue1) ->
- %% On a delegue a add_int
- true
- ; get_saved_cstr_suspensions(LSusp),
- ((member((Susp,absA_lt_absB(CA,CB)),LSusp),
- (CA,CB) == (A,B))
- ->
- kill_suspension(Susp)
- ; true),
-
+ ; Continue = 1)),
+ (var(Continue) ->
+ true
+ ; saturate_diff_int_inequalities(A,B,Continue1),
+ (var(Continue1) ->
+ % On a delegue a add_int
+ true
+ ; get_saved_cstr_suspensions(LSusp),
+ ((member((Susp,absA_lt_absB(CA,CB)),LSusp),
+ (CA,CB) == (A,B))
+ ->
+ kill_suspension(Susp)
+ ; true),
+
my_suspend(absA_lt_absB(A,B),3,(A,B)->suspend:constrained)))),
- set_priority(Prio),
- wake_if_other_scheduled(Prio).
+ set_priority(Prio),
+ wake_if_other_scheduled(Prio).
ensure_absA_lt_absB(A,B) :-
- A \== B,
- %% B <> 0,
- (integer(A) ->
- (integer(B) ->
- abs(A) < abs(B)
- ; OpA is -A,
- (A >= 0 ->
- mfd:list_to_dom([OpA..A],ExDomB)
- ; mfd:list_to_dom([A..OpA],ExDomB)),
- mfd:dvar_domain(B,DomB),
- mfd:dom_difference(DomB,ExDomB,NDomB),
- mfd:dvar_set(B,NDomB))
- ; (integer(B) ->
- (B > 0 ->
- Bp is B - 1,
- OpBp is -Bp,
- IntA = OpBp..Bp
- ; %% B < 0,
- Bm is B + 1,
- OpBm is -Bm,
- IntA = Bm..OpBm),
- mfd:(A :: IntA)
- ; ((exists_delta_Rel(A,B,Rel,_,_),
- Rel \== '#')
- ->
- (occurs(Rel,('>','>=')) ->
- %% |A| < |B| et A >= B
- %% si B positif alors |A| >= |B| -> fail
- %% donc B negatif
- mfd:dvar_remove_greater(B,-1)
- ; %% occurs(Rel,('<','=<'))
- %% |A| < |B| et A =< B
- %% si A negatif alors B positif et
- %% si A positif alors B positif
- mfd:dvar_remove_smaller(B,1))
- ; true),
- %% On fait le menage dans A gt(abs(B),abs(A))
- %% absmin(A) < absmin(B),
- %% On peut retirer de B -MinAbsA..MinAbsA
- mfd:mindomain(A,MinA),
- mfd:get_intervals(A,IntA),
- abs_min(IntA,MinA,MinAbsA),
- OpMinAbsA is -MinAbsA,
- mfd:list_to_dom([OpMinAbsA..MinAbsA],ExDomB),
- mfd:dvar_domain(B,DomB),
- mfd:dom_difference(DomB,ExDomB,NDomB),
- mfd:dvar_set(B,NDomB),
- %% absmax(A) < absmax(B),
- %% On peut retirer de A -MaxAbsB..MaxAbsB
- mfd:dvar_range(B,MinB,MaxB),
- AbsMaxBm1 is max(abs(MinB),abs(MaxB))-1,
- OpAbsMaxBm1 is - AbsMaxBm1,
- mfd:dvar_remove_smaller(A,OpAbsMaxBm1),
- mfd:dvar_remove_greater(A,AbsMaxBm1))).
+ A \== B,
+ % B <> 0,
+ (integer(A) ->
+ (integer(B) ->
+ abs(A) < abs(B)
+ ; OpA is -A,
+ (A >= 0 ->
+ mfd:list_to_dom([OpA..A],ExDomB)
+ ; mfd:list_to_dom([A..OpA],ExDomB)),
+ mfd:dvar_domain(B,DomB),
+ mfd:dom_difference(DomB,ExDomB,NDomB),
+ mfd:dvar_set(B,NDomB))
+ ; (integer(B) ->
+ (B > 0 ->
+ Bp is B - 1,
+ OpBp is -Bp,
+ IntA = OpBp..Bp
+ ; % B < 0,
+ Bm is B + 1,
+ OpBm is -Bm,
+ IntA = Bm..OpBm),
+ mfd:(A :: IntA)
+ ; ((exists_delta_Rel(A,B,Rel,_,_),
+ Rel \== '#')
+ ->
+ (occurs(Rel,('>','>=')) ->
+ % |A| < |B| et A >= B
+ % si B positif alors |A| >= |B| -> fail
+ % donc B negatif
+ mfd:dvar_remove_greater(B,-1)
+ ; % occurs(Rel,('<','=<'))
+ % |A| < |B| et A =< B
+ % si A negatif alors B positif et
+ % si A positif alors B positif
+ mfd:dvar_remove_smaller(B,1))
+ ; true),
+ % On fait le menage dans A gt(abs(B),abs(A))
+ % absmin(A) < absmin(B),
+ % On peut retirer de B -MinAbsA..MinAbsA
+ mfd:mindomain(A,MinA),
+ mfd:get_intervals(A,IntA),
+ abs_min(IntA,MinA,MinAbsA),
+ OpMinAbsA is -MinAbsA,
+ mfd:list_to_dom([OpMinAbsA..MinAbsA],ExDomB),
+ mfd:dvar_domain(B,DomB),
+ mfd:dom_difference(DomB,ExDomB,NDomB),
+ mfd:dvar_set(B,NDomB),
+ % absmax(A) < absmax(B),
+ % On peut retirer de A -MaxAbsB..MaxAbsB
+ mfd:dvar_range(B,MinB,MaxB),
+ AbsMaxBm1 is max(abs(MinB),abs(MaxB))-1,
+ OpAbsMaxBm1 is - AbsMaxBm1,
+ mfd:dvar_remove_smaller(A,OpAbsMaxBm1),
+ mfd:dvar_remove_greater(A,AbsMaxBm1))).
abs_min([],AbsMin,AbsMin).
abs_min([Int|LInt],Abs,AbsMin) :-
@@ -4550,7 +4619,7 @@ power_int_body(A,TA,N,Mod2,B,TB,Continue) :-
check_reduced(IA,NIA,TA),
check_reduced(IB,NIB,TB),
power_int_rec(A,TA,N,Mod2,B,TB,Continue),
- launch_delta_power(A,Mod2,B)).
+ launch_delta_power(A,N,Mod2,B)).
%% On exploite un delta de difference stricte si il existe
@@ -4606,7 +4675,8 @@ check_delta_power(A,N,Mod2,B,TA,TB) :-
; TB = 1)
; true).
-launch_delta_power(A,Mod2,B) :-
+launch_delta_power(A,N,Mod2,B) :-
+ getval(use_delta,1)@eclipse,
var(A),
var(B), % donc N > 0
A \== B, % donc N > 1
@@ -4620,9 +4690,17 @@ launch_delta_power(A,Mod2,B) :-
D2 is HB - LA
; (LA < 0 ->
% A non signé
- D1 = 0,
- % HA > 0, on surapproxime
- D2 is HB-LA
+ mfd:get_intervals(A,IA),
+ split_neg_pos(IA,NA,PA,ZA),
+ ((var(ZA), % A <> 0,
+ interval_range(PA,LPA,_HA),
+ LPA > 1) % A <> 1
+ ->
+ interval_range(NA,_LA,HNA),
+ D1 is min(HNA^N - HNA,LPA^N - LPA)
+ ; D1 = 0),
+ % LA < 0 et HA > 0
+ D2 is max(LA^N-LA,HA^N-HA)
; % A pos, B pos: LA -> LB, HA -> HB
D1 is LB - LA,
D2 is HB - HA))
@@ -4635,7 +4713,7 @@ launch_delta_power(A,Mod2,B) :-
D2 is HB - HA),
sort(0,=<,[D1,D2],[MinD,MaxD]),
launch_delta(A,B,+,MinD..MaxD).
-launch_delta_power(A,Mod2,B).
+launch_delta_power(A,N,Mod2,B).
power_inst(A,N,Mod2,B,Continue) :-
(integer(A) ->
@@ -6804,69 +6882,72 @@ launch_congr1(A,C0,Mod0) :-
%% A appeler suite a une reduction d'intervalles
:- import
- replace_attribute/3
- from sepia_kernel.
+ replace_attribute/3
+ from sepia_kernel.
:- mode reduce_congr_bounds(?,++,++).
reduce_congr_bounds(A,C,Mod) :-
- mfd:get_intervals(A,LInter),
- reduce_congr_bounds_interval_list(LInter,C,Mod,NLInter),
- %% On n'utilise pas "set_intervals" pour eviter de refaire
- %% la reduction de congruence
- (LInter == NLInter ->
- true
- ; NLInter \== [],
- ((NLInter = [Value],
- integer(Value))
- ->
- protected_unify(A = Value)
- ; replace_attribute(A,dom(NLInter),mfd),
- check_constrained_var(A,Constrained),
- my_notify_constrained(A),
- wake_if_constrained(Constrained))).
+ mfd:get_intervals(A,LInter),
+ reduce_congr_bounds_interval_list(LInter,C,Mod,NLInter),
+ % On n'utilise pas "set_intervals" pour eviter de refaire
+ % la reduction de congruence
+ (LInter == NLInter ->
+ true
+ ; NLInter \== [],
+ ((NLInter = [Value],
+ integer(Value))
+ ->
+ protected_unify(A = Value)
+ ; replace_attribute(A,dom(NLInter),mfd),
+ check_constrained_var(A,Constrained),
+ my_notify_constrained(A),
+ wake_if_constrained(Constrained))).
%% Pour mfd
:- export
- reduce_congr_bounds_interval_list/4.
+ reduce_congr_bounds_interval_list/4.
%:- mode reduce_congr_bounds_interval_list(++,++,++,?).
reduce_congr_bounds_interval_list(LInter,0,1,LInter) :- !.
reduce_congr_bounds_interval_list(LInter,C,M,NLInter) :-
- reduce_congr_bounds_interval_list1(LInter,C,M,NLInter).
+ reduce_congr_bounds_interval_list1(LInter,C,M,NLInter).
reduce_congr_bounds_interval_list1([],_,_,[]).
reduce_congr_bounds_interval_list1([Inter|LInter],C,Mod,NLInter) :-
- reduce_congr_bounds_interval(Inter,C,Mod,NLInter,EndNLInter),
- reduce_congr_bounds_interval_list1(LInter,C,Mod,EndNLInter).
+ block(reduce_congr_bounds_interval(Inter,C,Mod,NLInter,EndNLInter),
+ _,
+ (call(spy_here)@eclipse,
+ reduce_congr_bounds_interval(Inter,C,Mod,NLInter,EndNLInter))),
+ reduce_congr_bounds_interval_list1(LInter,C,Mod,EndNLInter).
:- mode reduce_congr_bounds_interval(++,++,++,?,?).
reduce_congr_bounds_interval(Min..Max,C,Mod,LInter,EndLInter) :- !,
- ((%%C \== 0,
- Min < 0,
- Max > 0)
- ->
- %% On force le trou en zero pour avoir des intervalles signes
- interval_from_bounds(Min,-1,Neg),
- reduce_congr_bounds_interval(Neg,C,Mod,LInter,EndLInter1),
- reduce_congr_bounds_interval(0,C,Mod,EndLInter1,EndLInter2),
- interval_from_bounds(1,Max,Pos),
- reduce_congr_bounds_interval(Pos,C,Mod,EndLInter2,EndLInter)
- ; reduce_min_congr(Min,C,Mod,NMin),
- reduce_max_congr(Max,C,Mod,NMax),
- (NMin == NMax ->
- LInter = [NMin|EndLInter]
- ; (NMin < NMax ->
- ((NMax - NMin) div Mod > 1 ->
- %% Au moins trois valeurs
- LInter = [NMin..NMax|EndLInter]
- ; %% Deux valeurs
- LInter = [NMin,NMax|EndLInter])
- ; %% Pas de valeur compatible
- EndLInter = LInter))).
+ ((%C \== 0,
+ Min < 0,
+ Max > 0)
+ ->
+ % On force le trou en zero pour avoir des intervalles signes
+ interval_from_bounds(Min,-1,Neg),
+ reduce_congr_bounds_interval(Neg,C,Mod,LInter,EndLInter1),
+ reduce_congr_bounds_interval(0,C,Mod,EndLInter1,EndLInter2),
+ interval_from_bounds(1,Max,Pos),
+ reduce_congr_bounds_interval(Pos,C,Mod,EndLInter2,EndLInter)
+ ; reduce_min_congr(Min,C,Mod,NMin),
+ reduce_max_congr(Max,C,Mod,NMax),
+ (NMin == NMax ->
+ LInter = [NMin|EndLInter]
+ ; (NMin < NMax ->
+ ((integer(NMax) - integer(NMin)) div Mod > 1 ->
+ % Au moins trois valeurs
+ LInter = [NMin..NMax|EndLInter]
+ ; % Deux valeurs
+ LInter = [NMin,NMax|EndLInter])
+ ; % Pas de valeur compatible
+ EndLInter = LInter))).
reduce_congr_bounds_interval(Val,C,Mod,LInter,EndLInter) :-
- (C is Val mod Mod ->
- LInter = [Val|EndLInter]
- ; EndLInter = LInter).
+ (C is integer(Val) mod Mod ->
+ LInter = [Val|EndLInter]
+ ; EndLInter = LInter).
%% On cherche le plus petit NMin tel que
@@ -6874,39 +6955,47 @@ reduce_congr_bounds_interval(Val,C,Mod,LInter,EndLInter) :-
:- mode reduce_min_congr(++,++,++,-).
reduce_min_congr(Min,C,Mod,NMin) :-
- CMin is Min mod Mod,
- compare(Order,CMin,C),
- reduce_min_congr(Order,CMin,Min,C,Mod,NMin).
+ IMin is integer(Min),
+ CMin is IMin mod Mod,
+ compare(Order,CMin,C),
+ reduce_min_congr(Order,CMin,IMin,C,Mod,NMin0),
+ (rational(Min) ->
+ NMin is rational(NMin0)
+ ; NMin = NMin0).
:- mode reduce_min_congr(++,++,++,++,++,-).
-%% CMin == C
+% CMin == C
reduce_min_congr(=,_,Min,_,_,Min).
-%% CMin < C
+% CMin < C
reduce_min_congr(<,CMin,Min,C,_,NMin) :-
- NMin is Min + (C - CMin).
-%% CMin > C
+ NMin is Min + (C - CMin).
+% CMin > C
reduce_min_congr(>,CMin,Min,C,Mod,NMin) :-
- %% Min + (Mod - CMin) === O[Mod]
- NMin is Min + (Mod - CMin) + C.
+ % Min + (Mod - CMin) === O[Mod]
+ NMin is Min + (Mod - CMin) + C.
%% On cherche le plus grand NMax tel que
%% NMax =< Max et NMax mod Mod = C
:- mode reduce_max_congr(++,++,++,-).
reduce_max_congr(Max,C,Mod,NMax) :-
- CMax is Max mod Mod,
- compare(Order,CMax,C),
- reduce_max_congr(Order,CMax,Max,C,Mod,NMax).
+ IMax is integer(Max),
+ CMax is IMax mod Mod,
+ compare(Order,CMax,C),
+ reduce_max_congr(Order,CMax,IMax,C,Mod,NMax0),
+ (rational(Max) ->
+ NMax is rational(NMax0)
+ ; NMax = NMax0).
:- mode reduce_max_congr(++,++,++,++,++,-).
%% CMax == C
reduce_max_congr(=,_,Max,_,_,Max).
%% CMax > C
reduce_max_congr(>,CMax,Max,C,_,NMax) :-
- NMax is Max - (CMax - C).
+ NMax is Max - (CMax - C).
%% CMax < C
reduce_max_congr(<,CMax,Max,C,Mod,NMax) :-
- %% Max - CMax == 0[Mod]
- NMax is ((Max - CMax) - Mod) + C.
+ % Max - CMax == 0[Mod]
+ NMax is ((Max - CMax) - Mod) + C.
diff --git a/Src/COLIBRI/col_solve.pl b/Src/COLIBRI/col_solve.pl
index 26e243b8a..8ddf7328a 100644
--- a/Src/COLIBRI/col_solve.pl
+++ b/Src/COLIBRI/col_solve.pl
@@ -735,8 +735,8 @@ smt_test :-
smt_test(TO,Size) :-
%StrDir = "./colibri-master-tests/tests/",
%StrDir = "./colibri-master-tests/tests/sat/", %0 (sans real/float-> int!)
- StrDir = "./colibri-master-tests/tests/unsat/", %0
- %StrDir = "./colibri-master-tests/tests/unknown/",
+ %StrDir = "./colibri-master-tests/tests/unsat/", %0
+ StrDir = "./colibri-master-tests/tests/unknown/",
%StrDir = "./smt/",
%StrDir = "./AdaCore/",
diff --git a/Src/COLIBRI/lp_arith.pl b/Src/COLIBRI/lp_arith.pl
index 776d6e58d..e1c8c78bb 100755
--- a/Src/COLIBRI/lp_arith.pl
+++ b/Src/COLIBRI/lp_arith.pl
@@ -1674,7 +1674,10 @@ insert_lin_cstr(geq_real(A,B)) ?- !,
((var(A),
var(B))
->
- (not_inf([A,B]) ->
+ ((not_inf([A,B]);
+ is_float_int_number(A),
+ is_float_int_number(B))
+ ->
insert_lin_cstr(geq_int(A,B))
; (is_real_box_rat(A,RatA) ->
% RatA >= B
@@ -1689,27 +1692,32 @@ insert_lin_cstr(geq_real(A,B)) ?- !,
insert_lin_cstr(gt_real(A,B)) ?- !,
((var(A),
var(B),
- not_inf([A,B]))
+ (is_float_int_number(A),
+ is_float_int_number(B),
+ FI = 1;
+ not_inf([A,B])))
->
- % Pas correct si on utilise un epsilon
- ((is_real_box_rat(A,IRatA),
- denominator(IRatA,1),
- is_float_int_number(B))
- ->
- % IRatA > B --> IRatA - 1 >= B
- PIRatA is IRatA - 1_1,
- make_poly([(-1,B),(1,PIRatA)],PRA,VRA),
- assert_poly_geq_val(PRA,VRA)
- ; ((is_real_box_rat(B,IRatB),
- denominator(IRatB,1),
- is_float_int_number(A))
+ (nonvar(FI) ->
+ insert_lin_cstr(gt_int(A,B))
+ ; % Pas correct si on utilise un epsilon
+ ((is_real_box_rat(A,IRatA),
+ denominator(IRatA,1),
+ is_float_int_number(B))
->
- % A > IRatB --> A >= IRatB + 1
- SIRatB is IRatB + 1_1,
- make_poly([(1,A),(-1,SIRatB)],PRB,VRB),
- assert_poly_geq_val(PRB,VRB)
- ; % on affaiblit le probleme
- insert_lin_cstr(geq_real(A,B))))
+ % IRatA > B --> IRatA - 1 >= B
+ PIRatA is IRatA - 1_1,
+ make_poly([(-1,B),(1,PIRatA)],PRA,VRA),
+ assert_poly_geq_val(PRA,VRA)
+ ; ((is_real_box_rat(B,IRatB),
+ denominator(IRatB,1),
+ is_float_int_number(A))
+ ->
+ % A > IRatB --> A >= IRatB + 1
+ SIRatB is IRatB + 1_1,
+ make_poly([(1,A),(-1,SIRatB)],PRB,VRB),
+ assert_poly_geq_val(PRB,VRB)
+ ; % on affaiblit le probleme
+ insert_lin_cstr(geq_real(A,B)))))
; true).
insert_lin_cstr(add_int(A,B,C)) ?- !,
diff --git a/Src/COLIBRI/ndelta.pl b/Src/COLIBRI/ndelta.pl
index b2b5c1f13..d5c1375cc 100755
--- a/Src/COLIBRI/ndelta.pl
+++ b/Src/COLIBRI/ndelta.pl
@@ -513,15 +513,27 @@ match_delta_var([(Var,R,C)|Deltas],Var,Rel,Cost) ?- !,
get_type(Var,Type),
(Type == int ->
(C = L0..H0 ->
- L is integer(L0),
- H is integer(H0),
+ % on elargit si pas integral
+ L is lrnd_integer(L0),
+ H is hrnd_integer(H0),
Cost = L..H
; Cost is integer(C))
; Cost = C).
match_delta_var([_|Deltas],Var,Rel,Cost) :-
match_delta_var(Deltas,Var,Rel,Cost).
-
+lrnd_integer(V,NV) :-
+ RV is rational(V),
+ (denominator(RV) =:= 1 ->
+ NV is numerator(RV)
+ ; NV is integer(floor(RV))).
+
+hrnd_integer(V,NV) :-
+ RV is rational(V),
+ (denominator(RV) =:= 1 ->
+ NV is numerator(RV)
+ ; NV is integer(ceiling(RV))).
+
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% X contient un delta a partir de X
exists_delta_start(X{ndelta:delta(_,[_|_AfterX],_Loop,_CC)}) ?-
@@ -1221,7 +1233,7 @@ launch_delta_bis2(X,Y,S0,C,CheckCycle,LoopOnly,Abort) :-
!,
(number(C) ->
S = '='
- ; S = S0),
+ ; S = S0),
(get_deltas(X,Y,OS,OC) ->
deltas_inter(OS,OC,S,C,NS,NC,Check1),
(var(Check1) ->
@@ -1678,15 +1690,15 @@ get_delta_before_after(V{ndelta:delta(B0,A0,_,_CC)},Before,After) ?-
(foreach((B,SB,CB0),B0),
foreach((B,SB,CB),Before) do
(CB0 = LB0..HB0 ->
- integer(LB0,LB),
- integer(HB0,HB),
+ lrnd_integer(LB0,LB),
+ hrnd_integer(HB0,HB),
CB = LB..HB
; integer(CB0,CB))),
(foreach((A,SA,CA0),A0),
foreach((A,SA,CA),After) do
(CA0 = LA0..HA0 ->
- integer(LA0,LA),
- integer(HA0,HA),
+ lrnd_integer(LA0,LA),
+ hrnd_integer(HA0,HA),
CA = LA..HA
; integer(CA0,CA)))
; Before = B0,
diff --git a/Src/COLIBRI/realarith.pl b/Src/COLIBRI/realarith.pl
index 7017dd67d..8f743bfdd 100755
--- a/Src/COLIBRI/realarith.pl
+++ b/Src/COLIBRI/realarith.pl
@@ -466,6 +466,7 @@ is_integral_round(Type,IR) :-
:- import timeout/3 from timeout.
refute_ineq_round(Goal,Type,A,B,_,1) ?- !.
+%refute_ineq_round(Goal,Type,A,B,NotIntegral,Stop) :- !.
refute_ineq_round(Goal,Type,A,B,NotIntegral,Stop) :-
mreal:get_intervals(A,LIA),
mreal:get_intervals(B,LIB),
@@ -1782,20 +1783,20 @@ real_to_float_bis(Type,A,B) :-
true
; save_cstr_suspensions((A,B)),
check_exists_real_to_float_bis(Type,A,B),
- get_dvar_fintervals(A,IA),
(Type == float_simple ->
- cast_double_to_float_intervals(IA,NIB),
+ get_dvar_fintervals(A,NIA),
+ cast_double_to_float_intervals(NIA,NIB),
set_typed_intervals(B,Type,NIB),
get_dvar_fintervals(B,IB),
- inv_cast_double_to_float_intervals(IB,NIA),
- set_typed_intervals(A,real,NIA)
+ inv_cast_double_to_float_intervals(IB,NNIA),
+ set_typed_intervals(A,real,NNIA)
; % on est conservatif
mreal:dvar_range(B,LB,HB),
get_previous_float(Type,LB,PB),
get_next_float(Type,HB,NB),
mreal:set_typed_intervals(A,real,[PB..NB]),
- get_dvar_fintervals(A,IA),
- mreal:set_typed_intervals(B,Type,IA)),
+ get_dvar_fintervals(A,NIA),
+ mreal:set_typed_intervals(B,Type,NIA)),
real_to_float_ineqs(Type,A,B),
check_before_susp_real_to_float_bis(Type,A,B)),
set_priority(Prio),
@@ -3361,12 +3362,12 @@ check_2box(_,_).
clean_inf_args_from_res(real,Res,Args) ?- !.
clean_inf_args_from_res(Type,Res,Args) :-
(not_inf_bounds(Res) ->
- getval(saved_suspensions,SL),
+ get_saved_cstr_suspensions(SL),
(foreach(Arg,Args),
param(Type) do
check_gt_real(Type,1.0Inf,Arg),
check_gt_real(Type,Arg,-1.0Inf)),
- setval(saved_suspensions,SL)
+ setval(saved_suspensions,(1,SL))
; true).
% pour tester les bornes des types "reels"
@@ -5404,8 +5405,26 @@ minus_real_int_ineqs(A,B,C) :-
add_real_int_ineqs(B,C,A).
op_real_int_ineqs(A,OpA) :-
+ (get_sign(A,SA) ->
+ (SA == pos ->
+ % SOpA = neg
+ X = OpA,
+ Y = A
+ ; % neg
+ X = A,
+ Y = OpA),
+ mreal:dvar_range(X,LX,HX),
+ mreal:dvar_range(Y,LY,HY),
+ LD is rational(LY) - rational(HX),
+ ((LX == -1.0Inf;
+ HY == 1.0Inf)
+ ->
+ HD = 1.0Inf
+ ; HD is rational(HY) - rational(HX)),
+ launch_delta(X,Y,+,LD..HD)
+ ; true).
% 0 - A = OpA
- minus_real_int_ineqs(0.0,A,OpA).
+% minus_real_int_ineqs(0.0,A,OpA).
@@ -8093,7 +8112,7 @@ check_launch_op_int(Type,A,B,_,Continue) :-
->
cast_real_int(Type,A,IA),
cast_real_int(Type,B,IB),
- op_int(IA,IB)
+ op(IA,IB)
; Continue = 1).
@@ -12810,25 +12829,41 @@ idiv_mod_real(A,B,Q,R) :-
% pour la simulation des entiers non bornes par des reels
set_lazy_domain(real,A),
set_lazy_domain(real,B),
- set_lazy_domain(real,AbsB),
- set_lazy_domain(real,Q0),
set_lazy_domain(real,Q),
set_lazy_domain(real,BQ),
set_lazy_domain(real,R),
launch_float_int_number(A),
launch_float_int_number(B),
- launch_float_int_number(AbsB),
launch_float_int_number(Q),
launch_float_int_number(BQ),
launch_float_int_number(R),
- ensure_not_NaN([A,B,AbsB,Q0,Q,BQ,R]),
+ ensure_not_NaN([A,B,Q,BQ,R]),
diff_real(real,B,0.0),
- launch_geq_real(real,R,0.0),
- launch_gt_real(real,AbsB,R),
- abs_val_real(real,B,AbsB),
+
+ as(R,real) $>= 0.0,
+ % R est borné par B en valeur absolue
+ abs(as(R,real)) $< abs(as(B,real)),
+/*
+ % R est du signe de B
+ ite(as(B,real) $>= 0.0,
+ as(R,real) $>= 0.0,
+ as(R,real) $< 0),
+ % Q est du signe de A * B
+ ite(as(A,real) $>= 0.0,
+ ite(as(B,real) $> 0.0,
+ as(Q,real) $>= 0.0,
+ as(Q,real) $=< 0.0),
+ ite(as(B,real) $< 0.0,
+ as(Q,real) $>= 0.0,
+ as(Q,real) $=< 0.0)),
+*/
+/*
div_real(real,A,B,Q0),
- truncate(real,Q0,Q),
- % R = A-BQ
+ ite(as(B,real) $>= 0.0,
+ floor(as(Q0,real)) $= as(Q,real),
+ ceiling(as(Q0,real)) $= as(Q,real)),
+ %truncate(real,Q0,Q),
+*/ % R = A-BQ
mult_real(real,B,Q,BQ),
minus_real(real,A,BQ,R),
% on teste la divisibilite pour forcer R Ã 0 ou <> 0
@@ -13238,6 +13273,7 @@ div_real_ineqs(Type,A,B,C) :-
get_saved_cstr_suspensions(LSusp),
abs_val_real(Type,A,AA),
abs_val_real(Type,B,AB),
+ % on restaure
setval(saved_suspensions,(1,LSusp)),
get_cstr_suspensions(AA,LSuspV),
((member(SV,LSuspV),
@@ -15792,6 +15828,7 @@ check_other_even_power_ineqs_from_res(Type,Pow,Val,ValPow) :-
abs_val_real(Type,VV,AbsVV),
launch_real_ineq(Rel,Type,AbsVal,AbsVV)
; true)),
+
% abs(X) >= abs(Y) ==> X^2n >= Y^2n
% abs(X) > abs(Y) ==> X^2n >= Y^2n
% on ne travaille que si on a abs(Val)
@@ -19378,7 +19415,7 @@ gt_real_boxA(A,B,Continue) :-
gt_real_float_numberA(A,B,Continue) :-
(number(B) ->
- % On peut enlever B de A
+ % On peut enlever B de A (B non inf)
get_next_float(real,B,LA),
(LA < 1.0Inf ->
mreal:dvar_remove_smaller(A,LA)
@@ -19400,12 +19437,14 @@ gt_real_float_numberA(A,B,Continue) :-
set_interval_box(A,PInf,1.0Inf),
gt_real_boxA(A,B,Continue))
; % A est un "float_number"
- % MinA doit etre > a MinB
+ % MinA doit etre > a MinB (sauf si MinB = -1.0Inf)
mreal:mindomain(B,MinB),
get_next_float(real,MinB,LA),
(LA < 1.0Inf ->
Continue = 1,
- mreal:dvar_remove_smaller(A,LA),
+ (MinB == -1.0Inf ->
+ mreal:dvar_remove_smaller(A,MinB)
+ ; mreal:dvar_remove_smaller(A,LA)),
mreal:maxdomain(A,HB),
% intervalle pour B
mreal:dvar_remove_greater(B,HB)
@@ -21284,30 +21323,36 @@ sur_min_max(A,B,Min,Max) :-
get_dvar_fintervals_and_size(Var,Intervals,Size) :-
-%% var(Var),!,
- mreal:dvar_domain(Var,Dom),
- nonvar(Dom),
- mreal:dom_interval(Dom,Intervals),
- mreal:dom_size(Dom,Size).
+ (number(Var) ->
+ Intervals = [Var],
+ Size = 1
+ ; mreal:dvar_domain(Var,Dom),
+ nonvar(Dom),
+ mreal:dom_interval(Dom,Intervals),
+ mreal:dom_size(Dom,Size)).
get_dvar_fintervals(Var,Intervals) :-
- mreal:dvar_domain(Var,Dom),
- nonvar(Dom),
- mreal:dom_interval(Dom,Intervals).
+ (number(Var) ->
+ Intervals = [Var]
+ ; mreal:dvar_domain(Var,Dom),
+ nonvar(Dom),
+ mreal:dom_interval(Dom,Intervals)).
get_dvar_fsize(Var,Size) :-
- mreal:dvar_domain(Var,Dom),
- nonvar(Dom),
- mreal:dom_size(Dom,Size).
+ (number(Var) ->
+ Size = 1
+ ; mreal:dvar_domain(Var,Dom),
+ nonvar(Dom),
+ mreal:dom_size(Dom,Size)).
%check_maxprod_intervals(InterA,InterB,InterC) :- !.
check_maxprod_intervals(InterA,InterB,InterC) :-
- LA is length(InterA),
- LB is length(InterB),
- LC is length(InterC),
- getval(max_prod_intervals,MaxProd),
- one_prod_is_geq_maxprod(LA,LB,LC,MaxProd).
+ LA is length(InterA),
+ LB is length(InterB),
+ LC is length(InterC),
+ getval(max_prod_intervals,MaxProd),
+ one_prod_is_geq_maxprod(LA,LB,LC,MaxProd).
one_prod_is_geq_maxprod(LA,LB,LC,MaxProd) :-
( LA * LB > MaxProd ;
diff --git a/Src/COLIBRI/smt_import.pl b/Src/COLIBRI/smt_import.pl
index 830cb01a8..cdc395df8 100644
--- a/Src/COLIBRI/smt_import.pl
+++ b/Src/COLIBRI/smt_import.pl
@@ -5,6 +5,7 @@
% pour forcer l'utilisation des "real integral"
% a la place des entiers bornes
:- setval(def_real_for_int,1).
+%:- setval(def_real_for_int,0).
% pour indiquer une abstaction de forall/exists
:- setval(quantifier,0).
% pour activer le scrambler en mode test
@@ -2268,14 +2269,16 @@ smt_interp0(colibri_cdiv(A,B),Idiv,RIT) :- !,
add_as(RIT,IA0,IA),
smt_interp(B,IB,RIT),
(getval(real_for_int,1)@eclipse ->
- Idiv = real_from_int(int_from_real(IA) // int_from_real(IB))
+% Idiv = real_from_int(int_from_real(IA) // int_from_real(IB))
+ Idiv = colibri_cdiv(IA,IB)
; Idiv = (IA // IB)).
smt_interp0(colibri_crem(A,B),Imod,RIT) :- !,
smt_interp(A,IA0,RIT),
add_as(RIT,IA0,IA),
smt_interp(B,IB,RIT),
(getval(real_for_int,1)@eclipse ->
- Imod = real_from_int(int_from_real(IA) rem int_from_real(IB))
+% Imod = real_from_int(int_from_real(IA) rem int_from_real(IB))
+ Imod = colibri_crem(IA,IB)
; Imod = (IA rem IB)).
smt_interp0(colibri_floor(A),floor(IA),real) :- !,
smt_interp(A,IA0,real),
@@ -2832,8 +2835,8 @@ add_as(Type,I,AsI) :-
remove_upper_as(I,NI,_),
add_as0(Type,NI,AsI).
-add_as0(array(_,_),I,AsI) ?- !,
- AsI = I.
+add_as0(array(TI,TE),I,AsI) ?- !,
+ AsI = as(I,array(TI,TE)).
add_as0(Type,I,AsI) :-
nonvar(Type),
(var(I);
diff --git a/Src/COLIBRI/solve.pl b/Src/COLIBRI/solve.pl
index 5a90b2057..e57447fa5 100644
--- a/Src/COLIBRI/solve.pl
+++ b/Src/COLIBRI/solve.pl
@@ -1838,12 +1838,10 @@ unfold_int_expr(int_from_real(EA),D,Cstr,Type,R) ?-
Type = int,
(number(A) ->
cast_real_int(real,A,R0),
- to_int(Type,R0,R1),
- blocked_unify(R,R1),
+ blocked_unify(R,R0),
Cstr = CA
- ; set_int_type(Type,R),
- insert_dep_inst(dep(R,D,[A])),
- make_conj(CA,(cast_real_int(real,A,R0),to_int(Type,R0,R)),Cstr)).
+ ; insert_dep_inst(dep(R,D,[A])),
+ make_conj(CA,cast_real_int(real,A,R),Cstr)).
unfold_int_expr(int_from_float(EA),D,Cstr,Type,R) ?-
ND is D + 1,
unfold_real_expr(EA,ND,CA,float_simple,A),
@@ -1851,12 +1849,10 @@ unfold_int_expr(int_from_float(EA),D,Cstr,Type,R) ?-
Type = int,
(number(A) ->
cast_real_int(float_simple,A,R0),
- to_int(Type,R0,R1),
- blocked_unify(R,R1),
+ blocked_unify(R,R0),
Cstr = CA
- ; set_int_type(Type,R),
- insert_dep_inst(dep(R,D,[A])),
- make_conj(CA,(cast_real_int(float_simple,A,R0),to_int(Type,R0,R)),Cstr)).
+ ; insert_dep_inst(dep(R,D,[A])),
+ make_conj(CA,cast_real_int(float_simple,A,R),Cstr)).
unfold_int_expr(int_from_double(EA),D,Cstr,Type,R) ?-
ND is D + 1,
unfold_real_expr(EA,ND,CA,float_double,A),
@@ -1864,12 +1860,10 @@ unfold_int_expr(int_from_double(EA),D,Cstr,Type,R) ?-
Type = int,
(number(A) ->
cast_real_int(float_double,A,R0),
- to_int(Type,R0,R1),
- blocked_unify(R,R1),
+ blocked_unify(R,R0),
Cstr = CA
- ; set_int_type(Type,R),
- insert_dep_inst(dep(R,D,[A])),
- make_conj(CA,(cast_real_int(float_double,A,R0),to_int(Type,R0,R)),Cstr)).
+ ; insert_dep_inst(dep(R,D,[A])),
+ make_conj(CA,cast_real_int(float_double,A,R),Cstr)).
unfold_int_expr(abs(EA),D,Cstr,Type,R) ?-
ND is D + 1,
@@ -1944,14 +1938,16 @@ unfold_int_expr(EA * EB,D,Cstr,Type,R) ?-
insert_dep_inst(dep(R,D,[A,B])),
make_conj(CAB,mult(Type,D,A,B,R,UO),Cstr)).
+% Surcharge pour les Int !
unfold_int_expr(EA / EB,D,Cstr,Type,R) ?- !,
unfold_int_expr(EA // EB,D,Cstr,Type,R).
unfold_int_expr(EA // EB,D,Cstr,Type,R) ?-
+ call(spy_here)@eclipse,
ND is D + 1,
unfold_int_expr(EA,ND,CA,Type,A),
unfold_int_expr(EB,ND,CB,Type,B),
- int_vars(Type,B),
+ %int_vars(Type,B),
unfold_int_expr(as(B,Type) #= as(0,Type),D,Cond,bool,Bool),
!,
get_reif_var_depth_from_labchoice(DD),
@@ -1962,7 +1958,6 @@ unfold_int_expr(EA // EB,D,Cstr,Type,R) ?-
; true),
insert_dep_inst(dep(R,D,[A,B,Rem,Bool])),
insert_dep_inst(dep(Rem,D,[A,B,R,Bool])),
- %insert_dep_inst(inst_cstr(D,UO)),
insert_dep_inst(dep(R,D,[UO])),
insert_dep_inst(dep(A,D,[UO])),
insert_dep_inst(dep(B,D,[UO])),
@@ -1971,10 +1966,11 @@ unfold_int_expr(EA // EB,D,Cstr,Type,R) ?-
make_conj(CAB,Cond,CABCond),
make_conj(CABCond,chk_undef_div_rem(Bool,Type,A,B,R,Rem,UO),Cstr).
unfold_int_expr(EA rem EB,D,Cstr,Type,R) ?-
+ call(spy_here)@eclipse,
ND is D + 1,
unfold_int_expr(EA,ND,CA,Type,A),
unfold_int_expr(EB,ND,CB,Type,B),
- int_vars(Type,B),
+ %int_vars(Type,B),
unfold_int_expr(as(B,Type) #= as(0,Type),D,Cond,bool,Bool),
!,
get_reif_var_depth_from_labchoice(DD),
@@ -1984,8 +1980,6 @@ unfold_int_expr(EA rem EB,D,Cstr,Type,R) ?-
insert_dep_inst(inst_cstr(D,R))
; true),
insert_dep_inst(dep(R,D,[A,B,Q,Bool])),
- insert_dep_inst(dep(Q,D,[A,B,R,Bool])),
- %insert_dep_inst(inst_cstr(D,UO)),
insert_dep_inst(dep(R,D,[UO])),
insert_dep_inst(dep(A,D,[UO])),
insert_dep_inst(dep(B,D,[UO])),
@@ -1993,6 +1987,7 @@ unfold_int_expr(EA rem EB,D,Cstr,Type,R) ?-
make_conj(CA,CB,CAB),
make_conj(CAB,Cond,CABCond),
make_conj(CABCond,chk_undef_div_rem(Bool,Type,A,B,Q,R,UO),Cstr).
+
unfold_int_expr(EA div EB,D,Cstr,Type,R) ?-
ND is D + 1,
unfold_int_expr(EA,ND,CA,Type,A),
@@ -6376,7 +6371,14 @@ unfold_real_expr(- EA,D,Cstr,Type,R) ?-
!,
insert_dep_inst(dep(R,D,[A])),
real_type(Type,RType),
- make_conj(CA,(ensure_not_NaN((A,R)),op_real(RType,A,R)),Cstr).
+ ((RType == real;
+ check_not_NaN(A);
+ check_not_NaN(R))
+ ->
+ ensure_not_NaN(A),
+ ensure_not_NaN(R),
+ make_conj(CA,op_real(RType,A,R),Cstr)
+ ; make_conj(CA,(ensure_not_NaN((A,R)),op_real(RType,A,R)),Cstr)).
unfold_real_expr(fp_neg(EA),D,Cstr,Type,R) ?-
(check_not_NaN(R) ->
!,
@@ -6717,23 +6719,42 @@ unfold_real_expr(abs(EA),D,Cstr,Type,R) ?-
/*
unfold_real_expr(fp_abs(EA),D,Cstr,Type,R) ?-
ND is D + 1,
+ (check_not_NaN(R) ->
+ ensure_not_NaN(A)
+ ; true),
unfold_real_expr(EA,ND,CA,Type,A),
- unfold_int_expr(isNaN(as(A,Type)),D,Cond,bool,BCond),
!,
- int_vars(bool,BCond),
- get_reif_var_depth_from_labchoice(DD),
- insert_dep_inst(inst_cstr(DD,BCond)),
+ (check_not_NaN(A) ->
+ ensure_not_NaN(R),
+ Cond = true,
+ BCond = 0
+ ; int_vars(bool,BCond),
+ unfold_int_expr(isNaN(as(A,Type)),D,Cond,bool,BCond),
+ get_reif_var_depth_from_labchoice(DD),
+ insert_dep_inst(inst_cstr(DD,BCond))),
insert_dep_inst(dep(R,D,[A,BCond])),
insert_dep_inst(dep(A,D,[BCond])),
make_conj(CA,Cond,CACond),
make_conj(CACond,fp_abs(BCond,Type,A,R),Cstr).
*/
unfold_real_expr(fp_abs(EA),D,Cstr,Type,R) ?-
- call(spy_here)@eclipse,
+ %call(spy_here)@eclipse,
ND is D + 1,
+ (check_not_NaN(R) ->
+ ensure_not_NaN(A)
+ ; true),
unfold_real_expr(EA,ND,CA,Type,A),
!,
- unfold_real_expr(ite(isNaN(as(A,Type)),
+ (check_not_NaN(A) ->
+ ensure_not_NaN(R),
+ unfold_real_expr(ite(isPositive(as(A,Type)),
+ as(A,Type),
+ - as(A,Type)),
+ D,
+ CR,
+ Type,
+ R)
+ ; unfold_real_expr(ite(isNaN(as(A,Type)),
as(nan,Type),
ite(isPositive(as(A,Type)),
as(A,Type),
@@ -6741,7 +6762,7 @@ unfold_real_expr(fp_abs(EA),D,Cstr,Type,R) ?-
D,
CR,
Type,
- R),
+ R)),
make_conj(CA,CR,Cstr).
unfold_real_expr(EA + EB,D,Cstr,Type,R) ?-
@@ -7098,6 +7119,49 @@ unfold_real_expr(irmod(EA,EB),D,Cstr,RType,R) ?-
Goal = chk_undef_imod_real(Bool,RType,A,B,R),
make_conj(CondAB,Goal,Cstr).
+unfold_real_expr(colibri_cdiv(EA,EB),D,Cstr,RType,Q) ?-
+ ND is D + 1,
+ ensure_not_NaN((A,B,Q,R)),
+ real_vars(real_int,(A,B,Q,R)),
+ unfold_real_expr(EA,ND,CA,RType,A),
+ unfold_real_expr(EB,ND,CB,RType,B),
+ % real ou real_int
+ nonvar(RType),
+ real_type(RType,real),
+ make_conj(CA,CB,CAB),
+ unfold_int_expr(as(0.0,RType) $= as(B,RType),ND,Cond,bool,Bool),
+ !,
+ get_reif_var_depth_from_labchoice(DD),
+ insert_dep_inst(inst_cstr(DD,Bool)),
+ insert_dep_inst(dep(Q,D,[Bool,A,B])),
+ insert_dep_inst(dep(R,D,[Bool,A,B])),
+ insert_dep_inst(dep(A,D,[Bool])),
+ insert_dep_inst(dep(B,D,[Bool])),
+ make_conj(Cond,CAB,CondAB),
+ Goal = chk_undef_cdiv_crem(Bool,A,B,Q,R),
+ make_conj(CondAB,Goal,Cstr).
+unfold_real_expr(colibri_crem(EA,EB),D,Cstr,RType,R) ?-
+ ND is D + 1,
+ ensure_not_NaN((A,B,Q,R)),
+ real_vars(real_int,(A,B,Q,R)),
+ unfold_real_expr(EA,ND,CA,RType,A),
+ unfold_real_expr(EB,ND,CB,RType,B),
+ % real ou real_int
+ nonvar(RType),
+ real_type(RType,real),
+ make_conj(CA,CB,CAB),
+ unfold_int_expr(as(0.0,RType) $= as(B,RType),ND,Cond,bool,Bool),
+ !,
+ get_reif_var_depth_from_labchoice(DD),
+ insert_dep_inst(inst_cstr(DD,Bool)),
+ insert_dep_inst(dep(Q,D,[Bool,A,B])),
+ insert_dep_inst(dep(R,D,[Bool,A,B])),
+ insert_dep_inst(dep(A,D,[Bool])),
+ insert_dep_inst(dep(B,D,[Bool])),
+ make_conj(Cond,CAB,CondAB),
+ Goal = chk_undef_cdiv_crem(Bool,A,B,Q,R),
+ make_conj(CondAB,Goal,Cstr).
+
% pour la simulation des entiers non bornes
% par des "real integral" (surtout pour les uninterp)
unfold_real_expr(setIntegral(ERF),D,Cstr,RType,R) ?-
@@ -7666,9 +7730,11 @@ fp_ceiling(Cond,Type,A,R) :-
; my_suspend(fp_ceiling(Cond,Type,A,R),0,(Cond,A,R)->suspend:constrained)).
fp_abs(0,Type,A,R) ?- !,
+ ensure_not_NaN(A),
ensure_not_NaN(R),
abs_val_real(Type,A,R).
-fp_abs(1,Type,NaN,R) ?- !,
+fp_abs(1,Type,A,R) ?- !,
+ protected_unify(A,nan),
protected_unify(R,nan).
fp_abs(Cond,Type,A,nan) ?- !,
protected_unify(Cond,1),
@@ -7676,6 +7742,7 @@ fp_abs(Cond,Type,A,nan) ?- !,
fp_abs(Cond,Type,A,R) :-
check_not_NaN(R),
!,
+ ensure_not_NaN(A),
protected_unify(Cond,0),
abs_val_real(Type,A,R).
fp_abs(Cond,Type,A,R) :-
@@ -9368,10 +9435,14 @@ check_exists_gt_real_reif(Type,A,B,Bool,Continue) :-
; Continue = 1).
+geq_real_reif(Type,A,B,Bool) :-
+ not_int(Bool,NotBool),
+ gt_real_reif(Type,B,A,NotBool).
+/*
geq_real_reif(Type,A,B,Bool) :-
gt_real_reif(Type,B,A,NotBool),
not_int(NotBool,Bool).
-
+*/
% Auxiliaire pour to_fp(BV)
@@ -9701,7 +9772,6 @@ chk_undef_idiv_real(Bool,Type,A,B,R) :-
(nonvar(Bool) ->
(Bool == 0 ->
% B <> 0.0
-% idiv_real(A,B,R)
idiv_mod_real(A,B,R,_)
; protected_unify(B,0.0),
undef_idiv_real(Type,A,R))
@@ -10118,7 +10188,187 @@ undef_div_rem(Type,A,Q,R,UO) :-
protected_unify(Q,All1),
protected_unify(R,A).
-
+% colibri_cdiv|crem
+chk_undef_cdiv_crem(Bool,A,B,Q,R) :-
+ save_cstr_suspensions((A,B)),
+ ((nonvar(Bool);
+ nonvar(B))
+ ->
+ ((Bool == 1;
+ B == 0.0)
+ ->
+ protected_unify(Bool,1),
+ protected_unify(B,0.0),
+ undef_cdiv_crem(A,Q,R)
+ ; get_saved_cstr_suspensions(LSusp),
+ ((member((_,cdiv_crem(AA,BB,QQ,RR)),LSusp),
+ A == AA,
+ B == BB)
+ ->
+ protected_unify(Q,QQ),
+ protected_unify(R,RR)
+ ; protected_unify(Bool,0),
+ % invariants
+ abs(as(R,real)) $< abs(as(B,real)),
+ ite(as(A,real) $>= 0.0, as(R,real) $>= 0.0, as(R,real) $=< 0.0),
+ cdiv_crem(A,B,Q,R)))
+ ; get_saved_cstr_suspensions(LSusp),
+ ((member((_,chk_undef_cdiv_crem(BBool,AA,BB,QQ,RR)),LSusp),
+ A == AA,
+ B == BB)
+ ->
+ protected_unify(Bool,BBool),
+ protected_unify(Q,QQ),
+ protected_unify(R,RR)
+ ; my_suspend(chk_undef_cdiv_crem(Bool,A,B,Q,R),0,
+ (Bool,A,B)->suspend:constrained))).
+
+undef_cdiv_crem(A,Q,R) :-
+ uninterp_trigger(cdiv_crem,[real],real,Trigger),
+ uninterp(cdiv_crem,Trigger,[A],(Q,R)).
+
+
+cdiv_crem(A,B,Q,R) :-
+ % B <> 0.0
+ get_priority(P),
+ set_priority(1),
+ save_cstr_suspensions((A,B,Q,R)),
+ (Q == 0.0 ->
+ protected_unify(A,R)
+ ; true),
+ (A == R ->
+ protected_unify(Q,0.0)
+ ; true),
+ (get_sign(R,SR) ->
+ % A est du signe de R
+ SA = SR,
+ set_sign(real,A,SA)
+ ; true),
+ (get_sign(A,SA) ->
+ % R est du signe de A
+ SR = SA,
+ set_sign(real,R,SR)
+ ; true),
+ (nonvar(SA) ->
+ (get_sign(B,SB) ->
+ (SA == SB ->
+ % Q >= 0
+ SQ = pos
+ ; SQ = neg),
+ set_sign(real,Q,SQ)
+ ; (get_sign(Q,SQ) ->
+ (SQ == pos ->
+ SB = SA
+ ; op_sign(SA,SB)),
+ set_sign(real,B,SB)
+ ; true))
+ ; ((get_sign(B,SB),
+ get_sign(Q,SQ))
+ ->
+ (SQ == pos ->
+ SA = SB
+ ; op_sign(SB,SA)),
+ set_sign(A,SA),
+ set_sign(R,SR)
+ ; true)),
+ cdiv_crem_inst_free(A,B,Q,R,Continue),
+ (var(Continue) ->
+ true
+ ; (((not_inf_bounds(A);
+ is_real_box_rat(A,RA)),
+ (not_inf_bounds(B);
+ is_real_box_rat(B,RB)))
+ ->
+ % délégation aux entiers bornés
+ cast_real_int(real,A,IA),
+ cast_real_int(real,B,IB),
+ div_mod(IA,IB,IQ,IR),
+ cast_int_real(real,IQ,Q),
+ cast_int_real(real,IR,R)
+ ; check_exists_cdiv_crem(A,B,Q,R,Suspend),
+ (nonvar(Suspend) ->
+ my_suspend(cdiv_crem(A,B,Q,R),
+ 0,
+ (A,B,Q,R)->suspend:constrained)
+ ; true))),
+ set_priority(P),
+ wake_if_other_scheduled(P).
+
+cdiv_crem_inst_free(A,B,Q,R,Continue) :-
+ (A == 0.0 ->
+ protected_unify(Q,0.0),
+ protected_unify(R,0.0)
+ ; (B == 1.0 ->
+ protected_unify(A,Q),
+ protected_unify(R,0.0)
+ ; (B == -1.0 ->
+ op_real(real,A,Q),
+ protected_unify(R,0.0)
+ ; (A == B ->
+ protected_unify(Q,1.0),
+ protected_unify(R,0.0)
+ ; (A == R ->
+ % BQ = 0 donc Q = 0
+ abs_val_real(real,A,AbsA),
+ abs_val_real(real,B,AbsB),
+ gt_real(real,AbsB,AbsA),
+ protected_unify(Q,0.0)
+ ; % saturations
+ %Continue = 1,
+ (Q == 0.0 ->
+ abs_val_real(real,A,AbsA),
+ abs_val_real(real,B,AbsB),
+ gt_real(real,AbsB,AbsA),
+ protected_unify(A,R)
+ ; (R == 0.0 ->
+ abs_val_real(real,A,AbsA),
+ abs_val_real(real,B,AbsB),
+ gt_real(real,AbsB,AbsA),
+ mult_real(real,B,Q,A)
+ ; Continue = 1))))))).
+
+check_exists_cdiv_crem(A,B,Q,R,Suspend) :-
+ get_saved_cstr_suspensions(LSusp),
+ ((member((_,cdiv_crem(AA,BB,QQ,RR)),LSusp),
+ (AA == A; BB == B),
+ (B == BB ->
+ (A == AA ->
+ Fact = 1
+ ; member((_,op_real1(real,CA,OpCA)),LSusp),
+ (A == CA;
+ A == OpCA),
+ OpR = 1)
+ ; A == AA,
+ member((_,op_real1(real,CB,OpCB)),LSusp),
+ (B == CB;
+ B == OpCB)))
+ ->
+ (nonvar(Fact) ->
+ protected_unify(Q,QQ),
+ protected_unify(R,RR)
+ ; % A // B = Q et -A // B = -Q et R = -RR
+ % A // B = Q et A // -B = -Q et R = RR
+ op_real(real,Q,QQ),
+ (nonvar(OpR) ->
+ op_real(real,R,RR)
+ ; protected_unify(R,RR)))
+ ; ((% A // B = Q et -A // -B = Q et R = -RR
+ once (member_begin_end((_,op_real1(real,CV1,OpCV1)),LSusp,LSusp1,E1,E1),
+ (A == CV1, OpA = OpCV1;
+ A == OpCV1, OpA = CV1)),
+ once (member((_,op_real1(real,CV2,OpCV2)),LSusp1),
+ (B == CV2, OpB = OpCV2;
+ B == OpCV2, OpB = CV2)),
+ save_cstr_suspensions((OpA,OpB)),
+ get_saved_cstr_suspensions(NLSusp),
+ setval(saved_suspensions,(1,LSusp)),
+ once (member((_,cdiv_crem(V1,V2,Quot,RR)),NLSusp),
+ V1 == OpA,
+ V2 == OpB))
+ ->
+ protected_unify(Q,Quot),
+ op_real(real,R,RR)
+ ; Suspend = 1)).
chk_min_real(1,Type,A,B,R) ?- !,
protected_unify(R,nan).
diff --git a/test.sh b/test.sh
index 562d9180e..0a2183402 100755
--- a/test.sh
+++ b/test.sh
@@ -1,15 +1,19 @@
#!/bin/sh -eu
STEPS=100
+FAIL=false
+
echo check SAT tests
-find tests/sat -name "*.smt2" | parallel "$@" --timeout 200 --joblog sat.log "./neno 1 bundle/colibri --max-steps $STEPS {}" || (awk '$7 == -1' sat.log && false)
+find tests/sat -name "*.smt2" | parallel "$@" --timeout 200 --joblog sat.log "./neno 1 bundle/colibri --max-steps $STEPS {}" || (awk '$7 == -1' sat.log && FAIL=true)
echo check UNSAT tests
-find tests/unsat -name "*.smt2" | parallel "$@" --timeout 200 --joblog unsat.log "./neno 0 bundle/colibri --max-steps $STEPS {}" || (awk '$7 == -1' unsat.log && false)
+find tests/unsat -name "*.smt2" | parallel "$@" --timeout 200 --joblog unsat.log "./neno 0 bundle/colibri --max-steps $STEPS {}" || (awk '$7 == -1' unsat.log && FAIL=true)
echo check UNKNOWN tests
-find tests/unknown -name "*.smt2" | parallel "$@" --timeout 200 --joblog unknown.log "./neno 2 bundle/colibri --max-steps $STEPS {}" || (awk '$7 == -1' unknown.log && false)
+find tests/unknown -name "*.smt2" | parallel "$@" --timeout 200 --joblog unknown.log "./neno 2 bundle/colibri --max-steps $STEPS {}" || (awk '$7 == -1' unknown.log && FAIL=true)
+
+if $FAIL; then exit 1; fi
#echo check TIMEOUT tests
#find tests/timeout -name "*.smt2" | parallel "$@" --timeout 200 --joblog timeout.log "./neno 2 bundle/colibri --max-steps $STEPS {}" || (awk '$7 != -1' timeout.log && false)
diff --git a/tests/unsat/bug37.smt2 b/tests/unknown/bug37.smt2
similarity index 100%
rename from tests/unsat/bug37.smt2
rename to tests/unknown/bug37.smt2
--
GitLab