From 8d636777da8acb6ac4afb9d5c97e0cc79c428686 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Fri, 27 Aug 2021 21:38:06 +0200
Subject: [PATCH 1/4] Regression tests for #41 #42
---
tests/sat/issue_42.smt2 | 9 +
tests/sat/issue_42_bis.smt2 | 5 +
tests/unsat/issue_41.smt2 | 339 ++++++++++++++++++++++++++++++++++++
3 files changed, 353 insertions(+)
create mode 100644 tests/sat/issue_42.smt2
create mode 100644 tests/sat/issue_42_bis.smt2
create mode 100644 tests/unsat/issue_41.smt2
diff --git a/tests/sat/issue_42.smt2 b/tests/sat/issue_42.smt2
new file mode 100644
index 000000000..2fa6ad2cf
--- /dev/null
+++ b/tests/sat/issue_42.smt2
@@ -0,0 +1,9 @@
+;; produced by colibri.drv ;;
+(set-logic ALL)
+(set-info :smt-lib-version 2.6)
+
+(declare-const a Int)
+(assert (and (< 1 a) (< a 100)))
+
+(assert (= (colibri_crem 100 a) 0))
+(check-sat)
diff --git a/tests/sat/issue_42_bis.smt2 b/tests/sat/issue_42_bis.smt2
new file mode 100644
index 000000000..1e1fad154
--- /dev/null
+++ b/tests/sat/issue_42_bis.smt2
@@ -0,0 +1,5 @@
+(set-logic ALL)
+(set-info :smt-lib-version 2.6)
+
+(assert (not (= (colibri_crem (- 1) (- 1)) (- 1))))
+(check-sat)
diff --git a/tests/unsat/issue_41.smt2 b/tests/unsat/issue_41.smt2
new file mode 100644
index 000000000..f41a485b8
--- /dev/null
+++ b/tests/unsat/issue_41.smt2
@@ -0,0 +1,339 @@
+;; 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 match_bool (par (a) (Bool a a) a))
+
+;; match_bool_True
+ (assert (par (a) (forall ((z a) (z1 a)) (= (match_bool true z z1) z))))
+
+;; match_bool_False
+ (assert (par (a) (forall ((z a) (z1 a)) (= (match_bool false z z1) z1))))
+
+(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))
+
+(define-fun length ((x Int) (y Int)) Int (ite (<= x y) (+ (- y x) 1) 0))
+
+;; Abs_le
+ (assert
+ (forall ((x Int) (y Int))
+ (= (<= (colibri_abs_int x) y) (and (<= (- y) x) (<= x y)))))
+
+;; Abs_pos
+ (assert (forall ((x Int)) (<= 0 (colibri_abs_int x))))
+
+;; Div_bound
+ (assert
+ (forall ((x Int) (y Int))
+ (=> (and (<= 0 x) (< 0 y))
+ (and (<= 0 (colibri_cdiv x y)) (<= (colibri_cdiv x y) x)))))
+
+;; Div_sign_pos
+ (assert
+ (forall ((x Int) (y Int))
+ (=> (and (<= 0 x) (< 0 y)) (<= 0 (colibri_cdiv x y)))))
+
+;; Div_sign_neg
+ (assert
+ (forall ((x Int) (y Int))
+ (=> (and (<= x 0) (< 0 y)) (<= (colibri_cdiv x y) 0))))
+
+;; Mod_sign_pos
+ (assert
+ (forall ((x Int) (y Int))
+ (=> (and (<= 0 x) (not (= y 0))) (<= 0 (colibri_crem x y)))))
+
+;; Mod_sign_neg
+ (assert
+ (forall ((x Int) (y Int))
+ (=> (and (<= x 0) (not (= y 0))) (<= (colibri_crem x y) 0))))
+
+;; Rounds_toward_zero
+ (assert
+ (forall ((x Int) (y Int))
+ (=> (not (= y 0))
+ (<= (colibri_abs_int (* (colibri_cdiv x y) y)) (colibri_abs_int x)))))
+
+;; Div_inf
+ (assert
+ (forall ((x Int) (y Int))
+ (=> (and (<= 0 x) (< x y)) (= (colibri_cdiv x y) 0))))
+
+;; Mod_inf
+ (assert
+ (forall ((x Int) (y Int))
+ (=> (and (<= 0 x) (< x y)) (= (colibri_crem x y) x))))
+
+;; Div_mult
+ (assert
+ (forall ((x Int) (y Int) (z Int))
+ (! (=> (and (< 0 x) (and (<= 0 y) (<= 0 z)))
+ (= (colibri_cdiv (+ (* x y) z) x) (+ y (colibri_cdiv z x)))) :pattern ((colibri_cdiv (+ (* x y) z) x)) )))
+
+;; Mod_mult
+ (assert
+ (forall ((x Int) (y Int) (z Int))
+ (! (=> (and (< 0 x) (and (<= 0 y) (<= 0 z)))
+ (= (colibri_crem (+ (* x y) z) x) (colibri_crem z x))) :pattern ((colibri_crem (+ (* x y) z) x)) )))
+
+;; Div_unique
+ (assert
+ (forall ((x Int) (y Int) (q Int))
+ (=> (< 0 y) (=> (and (<= (* q y) x) (< x (+ (* q y) y))) (= (div x y) q)))))
+
+;; Div_bound
+ (assert
+ (forall ((x Int) (y Int))
+ (=> (and (<= 0 x) (< 0 y)) (and (<= 0 (div x y)) (<= (div x y) x)))))
+
+;; Div_inf
+ (assert
+ (forall ((x Int) (y Int)) (=> (and (<= 0 x) (< x y)) (= (div x y) 0))))
+
+;; Div_inf_neg
+ (assert
+ (forall ((x Int) (y Int))
+ (=> (and (< 0 x) (<= x y)) (= (div (- x) y) (- 1)))))
+
+;; Mod_0
+ (assert (forall ((y Int)) (=> (not (= y 0)) (= (mod 0 y) 0))))
+
+;; Div_1_left
+ (assert (forall ((y Int)) (=> (< 1 y) (= (div 1 y) 0))))
+
+;; Div_minus1_left
+ (assert (forall ((y Int)) (=> (< 1 y) (= (div (- 1) y) (- 1)))))
+
+;; Mod_1_left
+ (assert (forall ((y Int)) (=> (< 1 y) (= (mod 1 y) 1))))
+
+;; Mod_minus1_left
+ (assert
+ (forall ((y Int))
+ (! (=> (< 1 y) (= (mod (- 1) y) (- y 1))) :pattern ((mod (- 1) y)) )))
+
+;; Div_mult
+ (assert
+ (forall ((x Int) (y Int) (z Int))
+ (! (=> (< 0 x) (= (div (+ (* x y) z) x) (+ y (div z x)))) :pattern ((div (+ (* x y) z) x)) )))
+
+;; Mod_mult
+ (assert
+ (forall ((x Int) (y Int) (z Int))
+ (! (=> (< 0 x) (= (mod (+ (* x y) z) x) (mod z x))) :pattern ((mod (+ (* x y) z) x)) )))
+
+(define-fun 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))))
+
+(declare-fun bool_eq (Int Int) Bool)
+
+(declare-const value__size Int)
+
+(declare-const object__size Int)
+
+(declare-const alignment Int)
+
+;; value__size_axiom
+ (assert (<= 0 value__size))
+
+;; object__size_axiom
+ (assert (<= 0 object__size))
+
+;; alignment_axiom
+ (assert (<= 0 alignment))
+
+(declare-fun user_eq (Int Int) Bool)
+
+(declare-const dummy Int)
+
+(declare-sort big_integer__ref 0)
+
+(declare-fun big_integer__refqtmk (Int) big_integer__ref)
+
+(declare-fun big_integer__content (big_integer__ref) Int)
+
+;; big_integer__content'def
+ (assert
+ (forall ((u Int)) (= (big_integer__content (big_integer__refqtmk u)) u)))
+
+;; big_integer__ref_inversion
+ (assert
+ (forall ((u big_integer__ref))
+ (! (= u (big_integer__refqtmk (big_integer__content u))) :pattern (
+ (big_integer__content u)) )))
+
+(define-fun big_integer__ref_big_integer__content__projection ((a1 big_integer__ref)) Int
+ (big_integer__content a1))
+
+(declare-sort valid_big_integer__ref 0)
+
+(declare-fun valid_big_integer__refqtmk (Int) valid_big_integer__ref)
+
+(declare-fun valid_big_integer__content (valid_big_integer__ref) Int)
+
+;; valid_big_integer__content'def
+ (assert
+ (forall ((u Int))
+ (= (valid_big_integer__content (valid_big_integer__refqtmk u)) u)))
+
+;; valid_big_integer__ref_inversion
+ (assert
+ (forall ((u valid_big_integer__ref))
+ (! (= u (valid_big_integer__refqtmk (valid_big_integer__content u))) :pattern (
+ (valid_big_integer__content u)) )))
+
+(define-fun valid_big_integer__ref_valid_big_integer__content__projection ((a1 valid_big_integer__ref)) Int
+ (valid_big_integer__content a1))
+
+(declare-const x Int)
+
+(declare-const y Int)
+
+(define-fun dynamic_invariant ((temp___expr_227 Int)
+ (temp___is_init_223 Bool) (temp___skip_constant_224 Bool)
+ (temp___do_toplevel_225 Bool) (temp___do_typ_inv_226 Bool)) Bool true)
+
+(define-fun dynamic_predicate ((temp___231 Int)) Bool true)
+
+;; Assume
+ (assert (not (= (= y 0) true)))
+
+(assert
+;; defqtvc
+ (not (= (= (colibri_crem x y) (colibri_crem x (- y))) true)))
+(check-sat)
--
GitLab
From 77c9d3909708a2e7e6f9defc0017ccb03ab3c582 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Tue, 31 Aug 2021 09:46:35 +0200
Subject: [PATCH 2/4] Import from Bin:a1af7a0 Src:908536735 farith:a93db57
---
Src/COLIBRI/col_solve.pl | 19 ++++--
Src/COLIBRI/realarith.pl | 136 ++++++++++++++++++++------------------
Src/COLIBRI/smt_import.pl | 51 +++++++++++++-
Src/COLIBRI/solve.pl | 44 +++++++++---
4 files changed, 165 insertions(+), 85 deletions(-)
diff --git a/Src/COLIBRI/col_solve.pl b/Src/COLIBRI/col_solve.pl
index 48ac3a80c..066b291bb 100644
--- a/Src/COLIBRI/col_solve.pl
+++ b/Src/COLIBRI/col_solve.pl
@@ -520,6 +520,10 @@ smt_comp_solve(FILE) :-
exit(Code).
smt_solve(FILE) :-
+ % Pas de désactivation du simples apres DDSteps
+ DDSteps = 0,
+ setval(simplex_delay_deactivation,DDSteps)@eclipse,
+ % Pas de comptage de steps
setval(step_stats,0)@eclipse,
setval(step_limit,0)@eclipse,
setval(nb_steps,0)@eclipse,
@@ -733,10 +737,11 @@ smt_test :-
smt_test0(5,1000,StrDir).
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/",
+ StrDir = "./colibri-master/tests/sat/", %0 (sans real/float-> int!)
+ %StrDir = "./colibri-master/tests/unsat/", %0
+ %StrDir = "./colibri-master/tests/unknown/",
+ %StrDir = "./colibri-master/tests/timeout/",
%StrDir = "./smt/",
%StrDir = "./AdaCore/",
@@ -841,7 +846,7 @@ smt_test(TO,Size) :-
%StrDir = "./QF_ABVFP/20170428-Liew-KLEE/aachen_real_gmp_gmp_klee_mul.x86_64/", % 3 (bitwuzla 0)
%StrDir = "QF_ABVFP/20170428-Liew-KLEE/aachen_real_numerical_recipes_qrdcmp.x86_64/",
- %StrDir = "./QF_ABVFP/20170428-Liew-KLEE/", % 106 (177 unsupported) (cvc4 55)
+ %StrDir = "./QF_ABVFP/20170428-Liew-KLEE/", % 105 (177 unsupported) (cvc4 55)
%StrDir = "./QF_ABVFP/20170501-Heizmann-UltimateAutomizer/", % 0 min_solve (cvc4 0) OK
%----------------------------------------------------------------------
%StrDir = "./QF_ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/",% 0 (cvc4 1|2)!
@@ -851,7 +856,7 @@ smt_test(TO,Size) :-
%StrDir = "./QF_BVFP/20170428-Liew-KLEE/imperial_synthetic_sqrt_klee.x86_64/", % 3 (bitwuzla 3)
%StrDir = "./QF_BVFP/20170428-Liew-KLEE/aachen_syn_halve_longdouble-flow.x86_64/",% 4u
- %StrDir = "./QF_BVFP/20170428-Liew-KLEE/", % 17 (cvc4 50)(bitwuzla
+ %StrDir = "./QF_BVFP/20170428-Liew-KLEE/", % 16 (cvc4 50)(bitwuzla
% 15)(89 u)(11 20mn)
%StrDir = "./QF_BVFP/20170501-Heizmann-UltimateAutomizer/", % 0 (bitwuzla 0)
%StrDir = "./QF_BVFP/ramalho/", % 0 TO (bitwuzla 0)
@@ -870,7 +875,7 @@ smt_test(TO,Size) :-
%----------------------------------------------------------------
%StrDir = "./QF_FP/20170501-Heizmann-UltimateAutomizer/", % 0
%StrDir = "./QF_FP/20190429-UltimateAutomizerSvcomp2019/",% 0 (bitwuzla 0)
- %StrDir = "./QF_FP/ramalho/", % 0! (cvc4 19)(bitwuzla 17)
+ %StrDir = "./QF_FP/ramalho/", % 0 (cvc4 19)(bitwuzla 17)
%StrDir = "./QF_FP/griggio/", % 50 (min_solve, sans lin_solve ni ls_reduce..)(39)
%(cvc4 89)(bitwuzla 74) LES DD DEMARRENT TROP VITE ?
%StrDir = "./QF_FP/schanda/spark/", % 6 (min_solve avec X =< (X+Y)/2 =< Y) (ncvc4 8)(bitwuzla 3)
diff --git a/Src/COLIBRI/realarith.pl b/Src/COLIBRI/realarith.pl
index e5f78c018..177ca70b3 100755
--- a/Src/COLIBRI/realarith.pl
+++ b/Src/COLIBRI/realarith.pl
@@ -12827,76 +12827,84 @@ div_real_float_intervals1(Type,ValInter1,ValInter2,L,EndL) :-
idiv_mod_real(A,B,Q,R) :-
% version integrale de mod_real
% pour la simulation des entiers non bornes par des reels
- set_lazy_domain(real,A),
- set_lazy_domain(real,B),
- 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(Q),
- launch_float_int_number(BQ),
- launch_float_int_number(R),
- ensure_not_NaN([A,B,Q,BQ,R]),
- diff_real(real,B,0.0),
+ get_priority(P),
+ set_priority(1),
+ save_cstr_suspensions((A,B)),
+ get_saved_cstr_suspensions(LSusp),
+ ((member((_,check_diff_real(BB,AA,QQ,RR)),LSusp),
+ BB == B,
+ AA == A)
+ ->
+ protected_unify(Q,QQ),
+ protected_unify(R,RR)
+ ; set_lazy_domain(real,A),
+ set_lazy_domain(real,B),
+ 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(Q),
+ launch_float_int_number(BQ),
+ launch_float_int_number(R),
+ ensure_not_NaN([A,B,Q,BQ,R]),
+ diff_real(real,B,0.0),
- 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),
- 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
- check_divides_real(B,A,R).
+ % R est borné par B en valeur absolue
+ as(R,real) $< abs(as(B,real)),
+ % R = A-BQ, mais de lien direct sur A et B ?
+ mult_real(real,B,Q,BQ),
+ minus_real(real,A,BQ,R),
+ % on teste la divisibilite pour forcer R Ã 0 ou <> 0
+ % et on garde une trace de idiv_mod_real
+ check_divides_real(B,A,Q,R)),
+ set_priority(P),
+ wake_if_other_scheduled(P).
-%check_divides_real(Y,X,R) :- !.
-check_divides_real(X,X,R) ?- !,
+%check_divides_real(Y,X,Q,R) :- !.
+check_divides_real(X,X,Q,R) ?- !,
+ protected_unify(Q,1.0),
protected_unify(R,0.0).
-check_divides_real(Y,X,R) :-
- nonvar(R),
- !.
-check_divides_real(Y,X,R) :-
- not_unify(R,0.0),
- !.
-check_divides_real(Y,X,R) :-
- %is_float_int_number(Y),
- %is_float_int_number(X),
- %not_unify(Y,0.0),
- (((nonvar(Y),
- integer(Y,IY);
- is_real_box_rat(Y,RY),
- integer(RY,IY)),
- (nonvar(X),
- integer(X,IX);
- is_real_box_rat(X,RX),
- integer(RX,IX)))
+check_divides_real(Y,X,Q,R) :-
+ get_priority(P),
+ set_priority(1),
+ save_cstr_suspensions((X,Y)),
+ ((nonvar(Y),
+ nonvar(X))
->
- (IX mod IY =:= 0 ->
- protected_unify(R,0.0)
- ; launch_diff_real(real,R,0.0))
- ; (divides_real_vars(Y,X,[]) ->
+ rational(X,RX),
+ rational(Y,RY),
+ (RY > 0 ->
+ Q is float(floor(RX/RY))
+ ; Q is float(ceiling(RX/RY))),
+ R is float(RX - (RY*rational(Q)))
+ ; % X et/ou Y variable
+ ((var(R),
+ divides_real_vars(Y,X,[]))
+ ->
protected_unify(R,0.0)
- ; my_suspend(check_divides_real(Y,X,R),0,(Y,X,R)->suspend:constrained))).
+ ; true)),
+ ((var(X);
+ var(Y))
+ ->
+ get_saved_cstr_suspensions(LSusp),
+ ((member((_,check_divides_real(YY,XX,QQ,RR)),LSusp),
+ once (YY == Y,
+ OO = XX,
+ O = X;
+ XX == X,
+ OO = YY,
+ O = Y),
+ (exists_diff_Rel(QQ,Q);
+ exists_diff_Rel(RR,R)))
+ ->
+ launch_diff_real(real,OO,O)
+ ; true),
+ my_suspend(check_divides_real(Y,X,Q,R),0,(Y,X)->suspend:constrained)
+ ; true),
+ set_priority(P),
+ wake_if_other_scheduled(P).
divides_real_vars(X,X,_) ?- !.
divides_real_vars(Y,X,Seen) :-
diff --git a/Src/COLIBRI/smt_import.pl b/Src/COLIBRI/smt_import.pl
index 3f70dce4d..238293d06 100644
--- a/Src/COLIBRI/smt_import.pl
+++ b/Src/COLIBRI/smt_import.pl
@@ -1597,7 +1597,51 @@ match_isObvious_tests(['fp.isNormal'(Arg),
Res) ?- !,
Res = Arg.
+% Inhibé car trop lent !!!
+try_factorize_in_let(Expr,Expr) :- !.
+try_factorize_in_let(Expr,NExpr) :-
+ (cgiveInstancePath(let(_,_),Expr,_) ->
+ % a priori déjà fait
+ NExpr = Expr
+ ; try_factorize_in_let1(Expr,NExpr)).
+
+try_factorize_in_let1(Expr,NExpr) :-
+ (find_mult_occ_compound_subterm(Expr,ST,LP) ->
+ %call(spy_here)@eclipse,
+ new_let_var(VId),
+ (ST = as(_,Type) ->
+ TVId = as(VId,Type)
+ ; TVId = VId),
+ (foreach(P,LP),
+ fromto(Expr,IE,OE,Expr1),
+ param(TVId) do
+ creplace_at_path_in_term(P,IE,TVId,OE)),
+ NExpr = let([(VId,ST)],NExpr1),
+ try_factorize_in_let1(Expr1,NExpr1)
+ ; NExpr = Expr).
+
+find_mult_occ_compound_subterm(Expr,ST,LP) :-
+ my_subterm(Expr,ST),
+ compound(ST),
+ (ST = as(SST,_) ->
+ compound(SST)
+ ; SST = ST),
+ functor(SST,FST,_),
+ FST \== 'Array',
+ FST \== '.',
+ (FST == '_' ->
+ arg(1,SST,T),
+ not member(T,['BitVec','FloatingPoint'])
+ ; true),
+ findall(P,cgiveInstancePath(ST,Expr,P),LP),
+ LP = [_,_|_].
+new_let_var(VId) :-
+ % Pas de collision possible avec les id smt_lib
+ set_var_name(V,"ColId"),
+ get_var_name(V,SVId),
+ concat_string(["\"",SVId,"\""],Str),
+ atom_string(VId,Str).
smt_interp(Expr,IExpr,Type) :-
(check_seen_expr(Expr,IExpr,Type) ->
@@ -1810,8 +1854,10 @@ smt_interp0('define-fun'(F,TypedVars,Sort,Expr),Decl,bool) :- !,
; (match_isObvious(Expr,Arg) ->
smt_interp(Arg,IArg,VType),
IExpr = isFinite(IArg) and neg(isSubnormal(IArg))
- ; smt_interp(Expr,IExpr,Type)))
- ; smt_interp(Expr,IExpr,Type)),
+ ; try_factorize_in_let(Expr,NExpr),
+ smt_interp(NExpr,IExpr,Type)))
+ ; try_factorize_in_let(Expr,NExpr),
+ smt_interp(NExpr,IExpr,Type)),
setval(seen_expr,OSE),
reset_let_vars,
Decl = true,
@@ -1823,7 +1869,6 @@ smt_interp0('define-fun'(F,TypedVars,Sort,Expr),Decl,bool) :- !,
add_binding(F,Type,Res)
; define_smt_func(F,TypedArgs,Type,IExpr))).
-
smt_interp0('define-const'(F,Sort,Expr),Decl,bool) :- !,
reset_let_vars,
smt_interp0('declare-var'(F,Sort),Decl0,bool),
diff --git a/Src/COLIBRI/solve.pl b/Src/COLIBRI/solve.pl
index 3d18795f6..de828fcfe 100644
--- a/Src/COLIBRI/solve.pl
+++ b/Src/COLIBRI/solve.pl
@@ -6928,7 +6928,7 @@ unfold_real_expr(EA * EB,D,Cstr,Type,R) ?-
(real_type(Type,real) ->
make_conj(CAB,mult_real(real,A,B,R),Cstr)
; make_conj(CAB,(ensure_not_NaN((A,B,R)),mult_real(Type,A,B,R)),Cstr)).
-unfold_real_expr(fp_mul(EA,EB),D,Cstr,Type,R) ?-
+unfold_real_expr(fp_mul(EA,EB),D,Cstr,Type,R) ?- !,
unfold_real_expr(fp_mul(rne,EA,EB),D,Cstr,Type,R).
unfold_real_expr(fp_mul(Rnd0,EA,EB),D,Cstr,Type,R) ?-
ND is D + 1,
@@ -10245,12 +10245,16 @@ cdiv_crem(A,B,Q,R) :-
(A == R ->
protected_unify(Q,0.0)
; true),
- (get_sign(R,SR) ->
+ ((not_zero(R),
+ get_sign(R,SR))
+ ->
% A est du signe de R
SA = SR,
set_sign(real,A,SA)
; true),
- (get_sign(A,SA) ->
+ ((not_zero(A),
+ get_sign(A,SA))
+ ->
% R est du signe de A
SR = SA,
set_sign(real,R,SR)
@@ -10262,13 +10266,16 @@ cdiv_crem(A,B,Q,R) :-
SQ = pos
; SQ = neg),
set_sign(real,Q,SQ)
- ; (get_sign(Q,SQ) ->
+ ; ((not_zero(Q),
+ get_sign(Q,SQ))
+ ->
(SQ == pos ->
SB = SA
; op_sign(SA,SB)),
set_sign(real,B,SB)
; true))
; ((get_sign(B,SB),
+ not_zero(Q),
get_sign(Q,SQ))
->
(SQ == pos ->
@@ -10319,17 +10326,14 @@ cdiv_crem_inst_free(A,B,Q,R,Continue) :-
abs_val_real(real,B,AbsB),
gt_real(real,AbsB,AbsA),
protected_unify(Q,0.0)
- ; % saturations
- %Continue = 1,
- (Q == 0.0 ->
+ ; (Q == 0.0 ->
+ % saturations
+ Continue = 1,
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))))))).
@@ -11146,7 +11150,15 @@ get_most_constrained_bool_var([(V,D,Adj)|UseList],VN,NUseList,Seen,OVar,ONb,Var,
get_type(E,Type),
(Type == int ->
mfd:get_intervals(E,[0,1])
- ; Type == rnd),
+ ; (Type == rnd ->
+ true
+ ; % A ANALYSER/GENERALISER AUX AUTRES TYPES
+ % Bon sur ramalho +1
+ % Mauvais sur les sat de colibri_test
+ fail,
+ real_type(Type,_),
+ mreal:dvar_size(E,2),
+ call(spy_here)@eclipse)),
not occurs(E,ISeen))
->
(get_var_name(E,_) ->
@@ -12506,3 +12518,13 @@ smt_check_disabled_delta :-
; true)
; true).
+
+% pour énumérer les sous termes de T
+my_subterm(T,ST) :-
+ my_subterm_list([T],ST).
+my_subterm_list([T|L],ST) :-
+ (ST = T;
+ compound(T),
+ T =.. [_|LT],
+ (my_subterm_list(LT,ST);
+ my_subterm_list(L,ST))).
\ No newline at end of file
--
GitLab
From 7e2f0b78b4b53326f5c3be655f3e1c4baf8edf91 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Tue, 31 Aug 2021 23:53:04 +0200
Subject: [PATCH 3/4] Import from Bin:a1af7a0 Src:dda2e1805 farith:a93db57
---
Src/COLIBRI/col_solve.pl | 69 ++++++++++++++++++----------------------
Src/COLIBRI/solve.pl | 9 ++++--
2 files changed, 37 insertions(+), 41 deletions(-)
diff --git a/Src/COLIBRI/col_solve.pl b/Src/COLIBRI/col_solve.pl
index 066b291bb..baa838df3 100644
--- a/Src/COLIBRI/col_solve.pl
+++ b/Src/COLIBRI/col_solve.pl
@@ -449,35 +449,8 @@ test_colibri :-
writeln(output,"NbSimplex":NbS).
-smt_solve_get_stat(FILE) :-
- % On passe en mode comptage du nombre de steps
- setval(step_stats,1)@eclipse,
- % Si on a une limite elle est donnée dans la ligne de commande
- (current_array(step_limit,_) ->
- true
- ; setval(step_limit,0)@eclipse),
- setval(nb_steps,0)@eclipse,
- setval(simplex_steps,0)@eclipse,
- smt_solve(_,FILE,0,Code),
- (getval(show_steps,1)@eclipse ->
- getval(nb_steps,Steps)@eclipse,
- writeln(output,"Steps":Steps)
- ; true),
- exit(Code).
-
-smt_solve_with_step_limit(FILE) :-
- % On passe en mode comptage du nombre de steps
- setval(step_stats,1)@eclipse,
- setval(show_steps,1)@eclipse,
- % Si on a une limite elle est donnée dans la ligne de commande
- (current_array(step_limit,_) ->
- true
- ; setval(step_limit,0)@eclipse),
- setval(nb_steps,0)@eclipse,
- setval(simplex_steps,0)@eclipse,
- smt_solve(_,FILE,0,Code),
- exit(Code).
+/*
smt_solve_count_steps(FILE,TO) :-
setval(show_steps,1)@eclipse,
getval(use_delta,UD)@eclipse,
@@ -502,7 +475,7 @@ smt_solve_count_steps(FILE,TO) :-
exit_block(Tag))),
setval(use_delta,UD)@eclipse,
setval(use_simplex,US)@eclipse.
-
+*/
smt_comp_solve(FILE) :-
% pas de message sur error pour la smtcomp
@@ -521,11 +494,16 @@ smt_comp_solve(FILE) :-
smt_solve(FILE) :-
% Pas de désactivation du simples apres DDSteps
- DDSteps = 0,
- setval(simplex_delay_deactivation,DDSteps)@eclipse,
- % Pas de comptage de steps
- setval(step_stats,0)@eclipse,
- setval(step_limit,0)@eclipse,
+ % (5000 par défaut dans colibri.pl)
+ % DDSteps = 0,
+ % setval(simplex_delay_deactivation,DDSteps)@eclipse,
+
+ % On passe en mode comptage du nombre de steps
+ setval(step_stats,1)@eclipse,
+ % Si on a une limite elle est donnée dans la ligne de commande
+ (current_array(step_limit,_) ->
+ true
+ ; setval(step_limit,0)@eclipse),
setval(nb_steps,0)@eclipse,
setval(simplex_steps,0)@eclipse,
% on active les warning de dolmen
@@ -533,6 +511,20 @@ smt_solve(FILE) :-
smt_solve(_,FILE,0,Code),
exit(Code).
+smt_solve_get_stat(FILE) :-
+ % On passe en mode comptage du nombre de steps
+ setval(step_stats,1)@eclipse,
+ % Si on a une limite elle est donnée dans la ligne de commande
+ (current_array(step_limit,_) ->
+ true
+ ; setval(step_limit,0)@eclipse),
+ setval(nb_steps,0)@eclipse,
+ setval(simplex_steps,0)@eclipse,
+ smt_solve(_,FILE,0,Code),
+ getval(nb_steps,Steps)@eclipse,
+ writeln(output,"Steps":Steps),
+ exit(Code).
+
smt_solve(Test,FILE,TO,Code) :-
no_3B,
set_threshold(1e-3),
@@ -738,10 +730,10 @@ smt_test :-
smt_test(TO,Size) :-
%StrDir = "./colibri-master/tests/",
- StrDir = "./colibri-master/tests/sat/", %0 (sans real/float-> int!)
+ %StrDir = "./colibri-master/tests/sat/", %0 (sans real/float-> int!)
%StrDir = "./colibri-master/tests/unsat/", %0
%StrDir = "./colibri-master/tests/unknown/",
- %StrDir = "./colibri-master/tests/timeout/",
+ StrDir = "./colibri-master/tests/timeout/",
%StrDir = "./smt/",
%StrDir = "./AdaCore/",
@@ -876,9 +868,9 @@ smt_test(TO,Size) :-
%StrDir = "./QF_FP/20170501-Heizmann-UltimateAutomizer/", % 0
%StrDir = "./QF_FP/20190429-UltimateAutomizerSvcomp2019/",% 0 (bitwuzla 0)
%StrDir = "./QF_FP/ramalho/", % 0 (cvc4 19)(bitwuzla 17)
- %StrDir = "./QF_FP/griggio/", % 50 (min_solve, sans lin_solve ni ls_reduce..)(39)
+ %StrDir = "./QF_FP/griggio/", % 49 (min_solve, sans lin_solve ni ls_reduce..)(39)
%(cvc4 89)(bitwuzla 74) LES DD DEMARRENT TROP VITE ?
- %StrDir = "./QF_FP/schanda/spark/", % 6 (min_solve avec X =< (X+Y)/2 =< Y) (ncvc4 8)(bitwuzla 3)
+ %StrDir = "./QF_FP/schanda/spark/", % 6! (min_solve avec X =< (X+Y)/2 =< Y) (ncvc4 8)(bitwuzla 3)
%StrDir = "./QF_FP/wintersteiger/", % tout OK
%-----------------------------------------------------------------------
%StrDir = "./QF_UFFP/schanda/",% 0
@@ -1001,6 +993,7 @@ smt_test0(TO,Size,StrDir) :-
os_file_name(OF,F),
concat_string(["cmd.exe /D /C smt_test_file ",OF," ",TO],Com)
; concat_string(["timeout --signal=KILL --kill-after=0.1 ",TO,"s ",ECLIPSE," -b ",COL," -g ",SizeM," -e \"seed(0),use_delta,use_simplex,setval(def_real_for_int,1)@colibri,setval(step_limit,0),setval(no_dolmen_warning,1)@eclipse,setval(show_steps,1),smt_solve_get_stat(\'",F,"\')\""],Com)),
+
% ; concat_string(["timeout --signal=KILL --kill-after=0.1 ",TO,"s ",ECLIPSE," -b ",COL," -g ",SizeM," -e \"seed(0),smt_comp_solve(\'",F,"\')\""],Com)),
%; concat_string(["timeout --signal=KILL --kill-after=0.1 ",TO,"s cvc4 ",F],Com)),
diff --git a/Src/COLIBRI/solve.pl b/Src/COLIBRI/solve.pl
index de828fcfe..e8e1313ac 100644
--- a/Src/COLIBRI/solve.pl
+++ b/Src/COLIBRI/solve.pl
@@ -11153,10 +11153,13 @@ get_most_constrained_bool_var([(V,D,Adj)|UseList],VN,NUseList,Seen,OVar,ONb,Var,
; (Type == rnd ->
true
; % A ANALYSER/GENERALISER AUX AUTRES TYPES
- % Bon sur ramalho +1
- % Mauvais sur les sat de colibri_test
- fail,
+ % pas d'effet visible !
+ % fail,
real_type(Type,_),
+ mreal:get_intervals(E,EI),
+ EI = [L,H],
+ number(L),
+ number(H),
mreal:dvar_size(E,2),
call(spy_here)@eclipse)),
not occurs(E,ISeen))
--
GitLab
From 843a87d14579fcfa7515fe2707d3fc0555a5406d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Wed, 1 Sep 2021 00:17:10 +0200
Subject: [PATCH 4/4] Fix step number after set_step fix
---
test.sh | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/test.sh b/test.sh
index 0f213488d..b648399d3 100755
--- a/test.sh
+++ b/test.sh
@@ -1,6 +1,6 @@
#!/bin/sh -eu
-STEPS=100
+STEPS=100000
FAIL=false
--
GitLab