diff --git a/Src/COLIBRI/TODO_QF_BV_2020-Weber_extensions.smt2 b/Src/COLIBRI/TODO_QF_BV_2020-Weber_extensions.smt2
new file mode 100644
index 0000000000000000000000000000000000000000..6ebc6095333afcc38b0b618fd70ce57ab7146921
--- /dev/null
+++ b/Src/COLIBRI/TODO_QF_BV_2020-Weber_extensions.smt2
@@ -0,0 +1,95 @@
+(set-info :smt-lib-version 2.6)
+(set-logic QF_BV)
+(set-info :source |
+ Constructed by Tjark Weber to test that the extensions defined
+ in QF_BV are implemented according to their definition
+|)
+(set-info :license "https://creativecommons.org/licenses/by/4.0/")
+(set-info :category "check")
+(set-info :status unsat)
+; We use a (reasonably small) fixed bit width m > 0.
+(declare-fun s () (_ BitVec 5))
+(declare-fun t () (_ BitVec 5))
+(declare-fun u () (_ BitVec 5))
+(assert (not (and
+; Bitvector constants
+ (= (_ bv13 32) #b00000000000000000000000000001101)
+; Bitwise operators
+ (= (bvnand s t) (bvnot (bvand s t)))
+ (= (bvnor s t) (bvnot (bvor s t)))
+ (= (bvxor s t) (bvor (bvand s (bvnot t)) (bvand (bvnot s) t)))
+ (= (bvxnor s t) (bvor (bvand s t) (bvand (bvnot s) (bvnot t))))
+ (= (bvcomp s t) (bvand (bvxnor ((_ extract 4 4) s) ((_ extract 4 4) t))
+ (bvcomp ((_ extract 3 0) s) ((_ extract 3 0) t))))
+ (= (bvxor s t u) (bvxor (bvxor s t) u))
+; Arithmetic operators
+ (= (bvsub s t) (bvadd s (bvneg t)))
+
+ (= (bvsdiv s t) (let ((?msb_s ((_ extract 4 4) s))
+ (?msb_t ((_ extract 4 4) t)))
+ (ite (and (= ?msb_s #b0) (= ?msb_t #b0))
+ (bvudiv s t)
+ (ite (and (= ?msb_s #b1) (= ?msb_t #b0))
+ (bvneg (bvudiv (bvneg s) t))
+ (ite (and (= ?msb_s #b0) (= ?msb_t #b1))
+ (bvneg (bvudiv s (bvneg t)))
+ (bvudiv (bvneg s) (bvneg t)))))))
+
+ (= (bvsrem s t) (let ((?msb_s ((_ extract 4 4) s))
+ (?msb_t ((_ extract 4 4) t)))
+ (ite (and (= ?msb_s #b0) (= ?msb_t #b0))
+ (bvurem s t)
+ (ite (and (= ?msb_s #b1) (= ?msb_t #b0))
+ (bvneg (bvurem (bvneg s) t))
+ (ite (and (= ?msb_s #b0) (= ?msb_t #b1))
+ (bvurem s (bvneg t))
+ (bvneg (bvurem (bvneg s) (bvneg t))))))))
+
+ (= (bvsmod s t) (let ((?msb_s ((_ extract 4 4) s))
+ (?msb_t ((_ extract 4 4) t)))
+ (let ((abs_s (ite (= ?msb_s #b0) s (bvneg s)))
+ (abs_t (ite (= ?msb_t #b0) t (bvneg t))))
+ (let ((u (bvurem abs_s abs_t)))
+ (ite (= u (_ bv0 5))
+ u
+ (ite (and (= ?msb_s #b0) (= ?msb_t #b0))
+ u
+ (ite (and (= ?msb_s #b1) (= ?msb_t #b0))
+ (bvadd (bvneg u) t)
+ (ite (and (= ?msb_s #b0) (= ?msb_t #b1))
+ (bvadd u t)
+ (bvneg u)))))))))
+
+ (= (bvule s t) (or (bvult s t) (= s t)))
+ (= (bvugt s t) (bvult t s))
+ (= (bvuge s t) (or (bvult t s) (= s t)))
+ (= (bvslt s t) (or (and (= ((_ extract 4 4) s) #b1)
+ (= ((_ extract 4 4) t) #b0))
+ (and (= ((_ extract 4 4) s) ((_ extract 4 4) t))
+ (bvult s t))))
+ (= (bvsle s t) (or (and (= ((_ extract 4 4) s) #b1)
+ (= ((_ extract 4 4) t) #b0))
+ (and (= ((_ extract 4 4) s) ((_ extract 4 4) t))
+ (bvule s t))))
+ (= (bvsgt s t) (bvslt t s))
+ (= (bvsge s t) (bvsle t s))
+; Other operations
+ (= (bvashr s t) (ite (= ((_ extract 4 4) s) #b0)
+ (bvlshr s t)
+ (bvnot (bvlshr (bvnot s) t))))
+ (= ((_ repeat 1) t) t)
+ (= ((_ repeat 2) t) (concat t ((_ repeat 1) t)))
+ (= ((_ zero_extend 0) t) t)
+ (= ((_ zero_extend 1) t) (concat ((_ repeat 1) #b0) t))
+ (= ((_ sign_extend 0) t) t)
+ (= ((_ sign_extend 1) t) (concat ((_ repeat 1) ((_ extract 4 4) t)) t))
+ (= ((_ rotate_left 0) t) t)
+ (= ((_ rotate_left 1) t) ((_ rotate_left 0)
+ (concat ((_ extract 3 0) t) ((_ extract 4 4) t))))
+ (= ((_ rotate_right 0) t) t)
+ (= ((_ rotate_right 1) t) ((_ rotate_right 0)
+ (concat ((_ extract 0 0) t) ((_ extract 4 1) t))))
+)))
+(check-sat)
+(get-value (s t))
+(exit)
diff --git a/Src/COLIBRI/arith.pl b/Src/COLIBRI/arith.pl
index d6ab10e7a2e7780b01b84f3c39aabcaafd87aa2c..09d36a45a6ba879d6218e0061905d82cd384e3c5 100755
--- a/Src/COLIBRI/arith.pl
+++ b/Src/COLIBRI/arith.pl
@@ -3467,7 +3467,7 @@ single_var_factor([S|LSusp],A,Depth,Seen,NSeen,LX) ?- !,
single_var_factor([],_,_,Seen,Seen,[]).
single_var_factor_goal(op_int(U,A),A,Depth,Seen,NSeen,LA) ?- !,
- (occurs(U,Seen) ->
+ (protected_occurs_in_list(U,Seen) ->
NSeen = Seen,
LA = []
; get_cstr_suspensions(U,LSuspU),
@@ -3503,8 +3503,8 @@ single_var_factor_goal(add_int(X,_,Y,_,Z,_),A,Depth,Seen,NSeen,LA) ?- !,
; NSeen = [V|Seen1],
LV = []),
(LA0 == [] ->
- ((occurs(U,Seen),
- occurs(V,Seen))
+ ((protected_occurs_in_list(U,Seen),
+ protected_occurs_in_list(V,Seen))
->
LA = []
; LA = [A])
@@ -3527,14 +3527,14 @@ single_var_factor_goal(mult_int(U,_,V,_,A,_),A,Depth,Seen,NSeen,LA) ?- !,
; NSeen = [V|Seen1],
LV = []),
(LA0 == [] ->
- ((occurs(U,Seen),
- occurs(V,Seen))
+ ((protected_occurs_in_list(U,Seen),
+ protected_occurs_in_list(V,Seen))
->
LA = []
; LA = [A])
; LA = LA0).
single_var_factor_goal(power_int(U,_,P,A,_),A,Depth,Seen,NSeen,LA) ?- !,
- (occurs(U,Seen) ->
+ (protected_occurs_in_list(U,Seen) ->
NSeen = Seen,
LA = []
; NDepth is Depth - 1,
diff --git a/Src/COLIBRI/col_solve.pl b/Src/COLIBRI/col_solve.pl
index ecc8a96b0c839ac79b122bea9e2f1740baefa4fb..72863bc9639f3f244a8da07c71dd112f4819313e 100644
--- a/Src/COLIBRI/col_solve.pl
+++ b/Src/COLIBRI/col_solve.pl
@@ -467,6 +467,8 @@ smt_solve(FILE) :-
setval(step_stats,0)@eclipse,
setval(step_limit,0)@eclipse,
setval(nb_steps,0)@eclipse,
+ % on active les warning de dolmen
+ setval(no_dolmen_warning,0)@eclipse,
smt_solve(_,FILE,0,Code),
exit(Code).
@@ -741,16 +743,59 @@ smt_test(TO,Size) :-
%StrDir = "./QF_ABVFP/20170428-Liew-KLEE/imperial_synthetic_count_klee_bug.x86_64/", % 9 TO! (cvc4 0)
%StrDir = "./QF_ABVFP/20170428-Liew-KLEE/imperial_gsl_benchmarks_histogram2d_klee_bug.x86_64/", %OK
- StrDir = "./QF_ABVFP/20170428-Liew-KLEE/", % 80 TO! (177 unsupported) (cvc4 95)
+ %StrDir = "./QF_ABVFP/20170428-Liew-KLEE/", % 80 TO! (177 unsupported) (cvc4 95)
%StrDir = "./QF_ABVFP/20170501-Heizmann-UltimateAutomizer/", % 0 (cvc4 2 TO)
%----------------------------------------------------------------------
%StrDir = "./QF_BV/",
+ %StrDir = "./QF_BV/20170501-Heizmann-UltimateAutomizer/",
+
+ %StrDir = "./QF_BV/20170531-Hansen-Check/", %OK
+ %StrDir = "./QF_BV/2017-BuchwaldFried/",
+ %StrDir = "./QF_BV/2018-Goel-hwbench/",
+ %StrDir = "./QF_BV/2019-Mann/",
+ %StrDir = "./QF_BV/2019-Wolf-fmbench/",
+ %StrDir = "./QF_BV/20200415-Yurichev/",
+ %StrDir = "./QF_BV/bmc-bv-svcomp14/",
+ %StrDir = "./QF_BV/calypto/",
+ %StrDir = "./QF_BV/challenge/",
+ %StrDir = "./QF_BV/check2/",
+ %StrDir = "./QF_BV/dwp_formulas/",
+ %StrDir = "./QF_BV/ecc/", % NULL comparé a cvc4
+ %StrDir = "./QF_BV/float/",
+
+ %StrDir = "./QF_BV/galois/", % 2 BUGS / 4 fich (unknown)
+
+ %StrDir = "./QF_BV/gulwani-pldi08/",
+ %StrDir = "./QF_BV/log-slicing/",
+ %StrDir = "./QF_BV/mcm/",
+ %StrDir = "./QF_BV/pipe/",
+ %StrDir = "./QF_BV/pspace/",
+ %StrDir = "./QF_BV/rubik/",
+ %StrDir = "./QF_BV/RWS/",
+ %StrDir = "./QF_BV/sage/",
+
+ %StrDir = "./QF_BV/spear/",
+ StrDir = "./QF_BV/spear/samba_v3.0.24/", % des unknown !
+ %StrDir = "./QF_BV/spear/inn_v2.4.3/",
+
+ %StrDir = "./QF_BV/stp_samples/",
+ %StrDir = "./QF_BV/tacas07/",
+ %StrDir = "./QF_BV/uclid/",
+ %StrDir = "./QF_BV/uclid_contrib_smtcomp09/",
+ %StrDir = "./QF_BV/uum/",
+ %StrDir = "./QF_BV/VS3/",
+ %StrDir = "./QF_BV/wienand-cav2008/",
+
%StrDir = "./QF_BV/asp/",
%StrDir = "./QF_BV/bench_ab/",%OK
- %StrDir = "./QF_BV/bmc-bv/",%des core et TO !!
- %StrDir = "./QF_BV/bmc-bv-svcomp14/",%des core et TO !!
- %StrDir = "./QF_BV/brummayerbiere/",%des core et TO !!
+ %StrDir = "./QF_BV/bmc-bv/",
+ %StrDir = "./QF_BV/bmc-bv-svcomp14/",
+ %StrDir = "./QF_BV/brummayerbiere/",
+ %StrDir = "./QF_BV/brummayerbiere2/",
+ %StrDir = "./QF_BV/brummayerbiere3/",
+ %StrDir = "./QF_BV/brummayerbiere4/",
+ %StrDir = "./QF_BV/bruttomesso/", % plein de TO
%StrDir = "./QF_BV/crafted/",
%-----------------------------------------------------------------------
%StrDir = "./QF_BVFP/",
@@ -811,8 +856,9 @@ smt_test(TO,Size) :-
%-----------------------------------------------------------------
%StrDir = "QF_AX/",
%StrDir = "QF_AX/storeinv/",
- %StrDir = "QF_AX/swap/",
+ StrDir = "QF_AX/swap/",
%StrDir = "QF_AX/storecomm/",
+ %StrDir = "QF_AX/cvc/",
%StrDir = "QF_ALIA/qlock2/", % Des TO et core dump
%StrDir = "QF_ALIA/cvc/", % TOUT OK
@@ -886,8 +932,10 @@ smt_test0(TO,Size,StrDir) :-
initNbCodes,
get_flag(version_as_list,[Ver|_]),
((Ver == 7) ->
- ECLIPSE = eclipse7
- ; ECLIPSE = eclipse),
+ ECLIPSE = eclipse7,
+ COL = "col_solve.eco"
+ ; ECLIPSE = eclipse,
+ COL = "col_solve.pl"),
get_flag(hostarch,ARCH),
((ARCH == "i386_nt";
ARCH == "x86_64_nt")
@@ -910,8 +958,7 @@ smt_test0(TO,Size,StrDir) :-
get_flag(installation_directory,EDIR),
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_solve -g ",SizeM," -e \"seed(0),use_delta,setval(def_real_for_int,1)@colibri,smt_solve_test(\'",F,"\',",0,")\""],Com)),
- ; concat_string(["timeout --signal=KILL --kill-after=0.1 ",TO,"s ",ECLIPSE," -b col_solve -g ",SizeM," -e \"seed(0),use_delta,setval(def_real_for_int,1)@colibri,setval(step_limit,0),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),use_delta,setval(def_real_for_int,1)@colibri,setval(step_limit,0),setval(no_dolmen_warning,1)@eclipse,smt_solve_get_stat(\'",F,"\')\""],Com)),
%; concat_string(["timeout --signal=KILL --kill-after=0.1 ",TO,"s cvc4 ",F],Com)),
exec(Com,[],Pid),
@@ -1023,6 +1070,54 @@ smt_unit_test(TO) :-
%StrDir = "QF_AX/storeinv/",
%StrDir = "QF_AX/swap/",
%StrDir = "QF_AX/storecomm/",
+%----------------------------------------------------------------------
+ %StrDir = "./QF_BV/",
+ %StrDir = "./QF_BV/20170501-Heizmann-UltimateAutomizer/",
+
+ %StrDir = "./QF_BV/20170531-Hansen-Check/", %OK
+ %StrDir = "./QF_BV/2017-BuchwaldFried/",
+ %StrDir = "./QF_BV/2018-Goel-hwbench/",
+ %StrDir = "./QF_BV/2019-Mann/",
+ %StrDir = "./QF_BV/2019-Wolf-fmbench/",
+ %StrDir = "./QF_BV/20200415-Yurichev/",
+ %StrDir = "./QF_BV/bmc-bv-svcomp14/",
+ %StrDir = "./QF_BV/calypto/",
+ %StrDir = "./QF_BV/challenge/",
+ %StrDir = "./QF_BV/check2/",
+ %StrDir = "./QF_BV/dwp_formulas/",
+ %StrDir = "./QF_BV/ecc/", % NULL comparé a cvc4
+ %StrDir = "./QF_BV/float/",
+ %StrDir = "./QF_BV/galois/", % 2 BUGS / 4 fich (unknown)
+ %StrDir = "./QF_BV/gulwani-pldi08/",
+ %StrDir = "./QF_BV/log-slicing/",
+ %StrDir = "./QF_BV/mcm/",
+ %StrDir = "./QF_BV/pipe/",
+ %StrDir = "./QF_BV/pspace/",
+ %StrDir = "./QF_BV/rubik/",
+ %StrDir = "./QF_BV/RWS/",
+ %StrDir = "./QF_BV/sage/",
+ %StrDir = "./QF_BV/sage2/",
+ %StrDir = "./QF_BV/spear/",
+ %StrDir = "./QF_BV/stp/",
+ %StrDir = "./QF_BV/stp_samples/",
+ %StrDir = "./QF_BV/tacas07/",
+ %StrDir = "./QF_BV/uclid/",
+ %StrDir = "./QF_BV/uclid_contrib_smtcomp09/",
+ %StrDir = "./QF_BV/uum/",
+ %StrDir = "./QF_BV/VS3/",
+ %StrDir = "./QF_BV/wienand-cav2008/",
+
+ %StrDir = "./QF_BV/asp/",
+ %StrDir = "./QF_BV/bench_ab/",%OK
+ %StrDir = "./QF_BV/bmc-bv/",
+ %StrDir = "./QF_BV/bmc-bv-svcomp14/",
+ %StrDir = "./QF_BV/brummayerbiere/",
+ %StrDir = "./QF_BV/brummayerbiere2/",
+ %StrDir = "./QF_BV/brummayerbiere3/",
+ %StrDir = "./QF_BV/brummayerbiere4/",
+ %StrDir = "./QF_BV/bruttomesso/", % plein de TO
+ %StrDir = "./QF_BV/crafted/",
+%-----------------------------------------------------------------------
%StrDir = "QF_ABV/bench_ab/",
%StrDir = "QF_ABV/bmc-arrays/",
@@ -1059,6 +1154,7 @@ smt_unit_test(TO) :-
initNbCodes,
setval(nbFile,0),
setval(nbTO,0),
+ setval(no_dolmen_warning,1)@eclipse,
getval(use_delta,UD)@eclipse,
getval(use_simplex,US)@eclipse,
length(SmtFileList,NFs),
diff --git a/Src/COLIBRI/colibri.pl b/Src/COLIBRI/colibri.pl
index 89cbb1b85ab854e156a4c61d15165f0fec59f33a..6202947d8a2e9d935ff4cecc1c2bd9ceb8b1ee96 100755
--- a/Src/COLIBRI/colibri.pl
+++ b/Src/COLIBRI/colibri.pl
@@ -165,6 +165,8 @@ init_colibri :-
setval(step_stats,0)@eclipse,
setval(step_limit,0)@eclipse,
setval(nb_steps,0)@eclipse,
+ % pas warning pour dolmen par defaut
+ setval(no_dolmen_warning,1)@eclipse,
% Initialision des trucs de benching des BV
use_prod_bv_congr,
diff --git a/Src/COLIBRI/lib/v5/x86_64_linux/simplex_ocaml.so b/Src/COLIBRI/lib/v5/x86_64_linux/simplex_ocaml.so
index cb7f97356a5c6f02a55283acea5ae9c19e55b6c7..d52229e72fb6bd49bd9065911b84001fcbbcc355 100755
Binary files a/Src/COLIBRI/lib/v5/x86_64_linux/simplex_ocaml.so and b/Src/COLIBRI/lib/v5/x86_64_linux/simplex_ocaml.so differ
diff --git a/Src/COLIBRI/lib/v7/x86_64_linux/simplex_ocaml.so b/Src/COLIBRI/lib/v7/x86_64_linux/simplex_ocaml.so
index ca8c498f08c6e00317f18089b2f3672b72dec9d6..87e8299312dad66d8d80645a20e7df522a37bed8 100755
Binary files a/Src/COLIBRI/lib/v7/x86_64_linux/simplex_ocaml.so and b/Src/COLIBRI/lib/v7/x86_64_linux/simplex_ocaml.so differ
diff --git a/Src/COLIBRI/lib/v7/x86_64_nt/simplex_ocaml.dll b/Src/COLIBRI/lib/v7/x86_64_nt/simplex_ocaml.dll
index b5cbab234366afd9fba16028d2fb18b3a48b3d0c..625c57af47a2c08f0349b01a02001757eadc2b44 100644
Binary files a/Src/COLIBRI/lib/v7/x86_64_nt/simplex_ocaml.dll and b/Src/COLIBRI/lib/v7/x86_64_nt/simplex_ocaml.dll differ
diff --git a/Src/COLIBRI/mbv_propa.pl b/Src/COLIBRI/mbv_propa.pl
index 2ae6655e64763d9920f22e2f9ddda4caf918e759..90a270f57e708b05c4aa5ea64d4cdb87c2392bb3 100644
--- a/Src/COLIBRI/mbv_propa.pl
+++ b/Src/COLIBRI/mbv_propa.pl
@@ -156,11 +156,7 @@ launch_bveq(Sx,X,Sy,Y) :-
(Sx > Sy ->
bveq(Sy,Y,Sx,X)
; bveq(Sx,X,Sy,Y)).
-/*
-bveq(_, X, _, Y) ?-
- !,
- protected_unify(X,Y).
-*/
+
bveq(_,X,_,X) ?- !.
bveq(Size, X, Size, Y) ?-
!,
@@ -201,6 +197,13 @@ filter_bveq(Sx, X, Sy, Y, Stop) :-
% Forme normale Sx < Sy
save_cstr_suspensions((X,Y)),
get_saved_cstr_suspensions(LSusp),
+ ((member((_,bveq(Sx, XX, Sy, YY)),LSusp),
+ X == XX)
+ ->
+ Stop = 1,
+ protected_unify(Y,YY)
+ ; true).
+/*
% On peut factoriser sur les memes tailles
% quand les plus petits/grands sont egaux
((member((_,bveq(Sx, XX, Sy, YY)),LSusp),
@@ -215,7 +218,7 @@ filter_bveq(Sx, X, Sy, Y, Stop) :-
Stop = 1,
protected_unify(U1,U2)
; true).
-
+*/
% =================== And ====================
@@ -682,7 +685,7 @@ bvxor_bis(M,X,Y,Z) :-
(var(Continue) ->
true
; get_saved_cstr_suspensions(LSusp),
- ((member((S,bvxor(M,XX,YY,ZZ)),LSusp),
+ ((member((S,bvxor_bis(M,XX,YY,ZZ)),LSusp),
three_on_three([X,Y,Z],[XX,YY,ZZ],R1,R2))
->
protected_unify(R1,R2)
@@ -879,10 +882,8 @@ bvsl_bis(M,X,Y,Z) :-
set_priority(1),
save_cstr_suspensions((X,Y,Z)),
get_saved_cstr_suspensions(LSusp),
- filter_bvsl_susps(M,X,Y,Z,LSusp,Stop),
- (var(Stop) ->
- bvsl_inst_free(M,X,Y,Z,Continue)
- ; true),
+ filter_bvsl_susps(M,X,Y,Z,LSusp),
+ bvsl_inst_free(M,X,Y,Z,Continue),
(var(Continue) ->
true
; % TODO why here reduced Prod is done AFTER, while in and/or is done before
@@ -929,55 +930,15 @@ sl_interval_ON(M,X,Y,Z) :-
mfd:set_intervals(Z, ZInter)
; true).
-filter_bvsl_susps(M,X,Y,Z,LSusp, Stop) :-
-% For comments, see the bvsr counterpart
- ((member_begin_end((S,Goal),LSusp,NLSusp,End,End),
- (Goal = bvsl_bis(M,XX,YY,ZZ),
- X == XX,
- G = sl;
- Goal = check_multN(u,M,A,B,Res,C,K,UO),
- (X == A, number(B), B is 2^Y;
- X == B, number(A), A is 2^Y),
- G = mult;
- Y == 1,
- Goal = check_addN(u,M,A,B,Res,C,UO),
- Z == C,
- (X == A;
- X == B),
- G = add))
+filter_bvsl_susps(M,X,Y,Z,LSusp) :-
+ Goal = bvsl_bis(M,XX,YY,ZZ),
+ ((member((S,Goal),LSusp),
+ X == XX,
+ Y == YY)
->
- (G == sl ->
- (Y == YY ->
- % factorisation
- kill_suspension(S),
- protected_unify(Z,ZZ)
- ; (Z == ZZ ->
- protected_unify(Z,0),
- (Y < YY ->
- kill_suspension(S)
- ; Stop = 1)
- ; ((Y < YY,
- nonvar(Z))
- ->
- Diff is YY - Y,
- ZZ is Z << Diff,
- kill_suspension(S)
- ; ( YY < Y, nonvar(ZZ) ->
- Diff is Y - YY,
- Z is ZZ << Diff,
- Stop = 1
- ; true))))
- ; % G = mult ou G = add
- % on peut tuer le check_xxN mais
- % on doit garder les autres contraintes
- % car on ne sait pas si elles ont ete factorisees
- %kill_suspension(S),
- (G == mult ->
- protected_unify(Z,C)
- ; protected_unify(A,B))),
- (var(Stop) ->
- filter_bvsl_susps(M,X,Y,Z,NLSusp,Stop)
- ; true)
+ % factorisation
+ kill_suspension(S),
+ protected_unify(Z,ZZ)
; true).
% TODO : check what reactivating Continue=1 does
@@ -1076,10 +1037,8 @@ bvsr_bis(M,X,Y,Z) :-
set_priority(1),
save_cstr_suspensions((X,Y,Z)),
get_saved_cstr_suspensions(LSusp),
- filter_bvsr_susps(M,X,Y,Z,LSusp,Stop),
- (var(Stop) ->
- bvsr_inst_free(M,X,Y,Z,Continue)
- ; true),
+ filter_bvsr_susps(M,X,Y,Z,LSusp),
+ bvsr_inst_free(M,X,Y,Z,Continue),
(var(Continue) ->
true
; sr_constr(M, X, Y, Z),
@@ -1137,41 +1096,13 @@ sr_interval([C|Inter], Off, [CC|IInter]) :-
CC is (C >> Off),
sr_interval(Inter, Off, IInter).
-filter_bvsr_susps(M,X,Y,Z,LSusp,Stop) :-
- ((member_begin_end((S,bvsr_bis(MM,XX,YY,ZZ)),LSusp,NLSusp,End,End),
- X == XX)
+filter_bvsr_susps(M,X,Y,Z,LSusp) :-
+ ((member((S,bvsr_bis(M,XX,YY,ZZ)),LSusp),
+ X == XX,
+ Y == YY)
->
- (Y == YY ->
- kill_suspension(S),
- protected_unify(Z,ZZ)
- ; (Z == ZZ ->
- % le plus petit shift contient le plus
- % d'informations
- protected_unify(Z,0),
- (Y < YY ->
- kill_suspension(S)
- ; % YY < Y
- % on laisse l'autre travailler
- Stop = 1)
- ; ((Y < YY,
- nonvar(Z))
- ->
- % le plus petit shift contient le plus d'informations
- % est on certain que Z et ZZ sont compatibles ?
- % on peut le tester ici
- Diff is YY - Y,
- ZZ is Z >> Diff,
- kill_suspension(S)
- ; ((YY < Y,
- nonvar(ZZ))
- ->
- Diff is Y - YY,
- Z is ZZ >> Diff
- % Stop = 1
- ; true)))),
- (var(Stop) ->
- filter_bvsr_susps(M,X,Y,Z,NLSusp,Stop)
- ; true)
+ kill_suspension(S),
+ protected_unify(Z,ZZ)
; true).
bvsr_inst_free(M,A,B,C,Continue) :-
@@ -1416,19 +1347,12 @@ bvconcat_v2(SX,X,SY,Y,Z) :-
filter_concat_susp(SX,X,SY,Y,Z) :-
save_cstr_suspensions((X,Y,Z)),
get_saved_cstr_suspensions(LSusp),
- SZ is SX + SY,
((member((Susp,bvconcat_v2_bis(SX, XX, SY, YY, ZZ)),LSusp),
- (X == XX ->
- (Y == YY ->
- U1 = Z, U2 = ZZ
- ; Z == ZZ,%?
- U1 = Y, U2 = YY)
- ; Y == YY,
- Z == ZZ,
- U1 = X, U2 = XX))
+ X == XX,
+ Y == YY)
->
kill_suspension(Susp),
- protected_unify(U1,U2)
+ protected_unify(Z,ZZ)
; true).
:- export bvconcat_v2_bis/5.
@@ -1736,10 +1660,18 @@ bvconcat_v3_bis(SX, X, SY, Y, Z) :-
:- export bvrotater/4, bvrotatel/4. % Size, Offset, X, Result
+bvrotatel(1,I,X,Z) ?- !,
+ protected_unify(Z,X).
+bvrotatel(M,0,X,Z) ?- !,
+ protected_unify(Z,X).
bvrotatel(M,I,X,Z):-
bvrotL(M,I,X,Z),
bvrotR(M,I,Z,X).
+bvrotater(1,I,X,Z) ?- !,
+ protected_unify(Z,X).
+bvrotater(M,0,X,Z) ?- !,
+ protected_unify(Z,X).
bvrotater(M,I,X,Z):-
bvrotR(M,I,X,Z),
bvrotL(M,I,Z,X).
@@ -1986,6 +1918,7 @@ sign_extend(Sx, I, X, Y) :-
% =================== Add ====================248474
:- export bvadd/4.
+
bvadd(M, X,Y,Z) :-
bulk_lazy_doms([X,Y,Z],M),
%MM is M + 1,
diff --git a/Src/COLIBRI/simplex_ocaml/dolmen/src/standard/expr.ml b/Src/COLIBRI/simplex_ocaml/dolmen/src/standard/expr.ml
index 08d437347129a33ed68b8071226afc4c1fcea653..f0abea8560d1cfb14a060c04976b2a1a34e3273b 100644
--- a/Src/COLIBRI/simplex_ocaml/dolmen/src/standard/expr.ml
+++ b/Src/COLIBRI/simplex_ocaml/dolmen/src/standard/expr.ml
@@ -1885,7 +1885,7 @@ module Term = struct
let uge =
with_cache ~cache:(Hashtbl.create 13) (fun n ->
- Id.const ~builtin:Bitv_uge "bvsge" [] [Ty.bitv n; Ty.bitv n] Ty.prop
+ Id.const ~builtin:Bitv_uge "bvuge" [] [Ty.bitv n; Ty.bitv n] Ty.prop
)
let slt =
diff --git a/Src/COLIBRI/smt_import.pl b/Src/COLIBRI/smt_import.pl
index 1cb895d8967c7f418f076749a584e22cd9c44743..9d9cfaa7fd4e501ef6e4f2f30027f81efa9edf0c 100644
--- a/Src/COLIBRI/smt_import.pl
+++ b/Src/COLIBRI/smt_import.pl
@@ -44,7 +44,6 @@ read_dolmen_terms(PEnv,Terms) :-
; Terms = [Term|ETerms]),
read_dolmen_terms(PEnv,ETerms)).
-
dolmen_to_colibri_term(set_logic(SLog),Term) ?- !,
Term = 'set-logic'(SLog).
dolmen_to_colibri_term(exit,Term) ?- !,
@@ -77,10 +76,12 @@ dolmen_to_colibri_term(error(String),_) ?- !,
writeln(Error),
exit_block(syntax).
dolmen_to_colibri_term(warn(String),Term) ?- !,
- split_string(String,"\"","",LNString),
- join_string(LNString,"'",NString),
- concat_string(["(warning \"",NString,"\")"],Error),
- writeln(Error),
+ (getval(no_dolmen_warning,1)@eclipse ->
+ true
+ ; split_string(String,"\"","",LNString),
+ join_string(LNString,"'",NString),
+ concat_string(["(warning \"",NString,"\")"],Error),
+ writeln(Error)),
Term = 'set-info'("Info","").
dolmen_to_colibri_term(set_info(app(symbol(SFlagInfo),
[symbol(SInfo)])),Term) ?- !,
@@ -384,35 +385,66 @@ get_col_id(SExt,bitv_sign_extend,[sign_extend,S]) :- !,
number_string(S,SS).
get_col_id(_,bitv_rotate_right(N),[rotate_right,N]) :- !.
get_col_id(_,bitv_rotate_left(N),[rotate_left,N]) :- !.
-get_col_id('Bitv_not',_,bvnot) :- !.
-get_col_id('Bitv_and',_,bvand) :- !.
-get_col_id('Bitv_or',_,bvor) :- !.
-get_col_id('Bitv_xor',_,bvxor) :- !.
-get_col_id('Bitv_nand',_,bvnand) :- !.
-get_col_id('Bitv_nor',_,bvnor) :- !.
-get_col_id('Bitv_xnor',_,bvxnor) :- !.
-get_col_id('Bitv_comp',_,bvcomp) :- !.
-get_col_id('Bitv_neg',_,bvneg) :- !.
-get_col_id('Bitv_add',_,bvadd) :- !.
-get_col_id('Bitv_sub',_,bvsub) :- !.
-get_col_id('Bitv_mul',_,bvmul) :- !.
-get_col_id('Bitv_udiv',_,bvudiv) :- !.
-get_col_id('Bitv_urem',_,bvurem) :- !.
-get_col_id('Bitv_sdiv',_,bvsdiv) :- !.
-get_col_id('Bitv_srem',_,bvsrem) :- !.
-get_col_id('Bitv_smod',_,bvsmod) :- !.
-get_col_id('Bitv_shl',_,bvshl) :- !.
-get_col_id('Bitv_shr',_,bvshr) :- !.
-get_col_id('Bitv_ashr',_,bavshr) :- !.
-get_col_id('Bitv_lshr',_,bvlshr) :- !.
-get_col_id('Bitv_ult',_,bvult) :- !.
-get_col_id('Bitv_ule',_,bvule) :- !.
-get_col_id('Bitv_ugt',_,bvugt) :- !.
-get_col_id('Bitv_uge',_,bvuge) :- !.
-get_col_id('Bitv_slt',_,bvslt) :- !.
-get_col_id('Bitv_sle',_,bvsle) :- !.
-get_col_id('Bitv_sgt',_,bvsgt) :- !.
-get_col_id('Bitv_sge',_,bvsge) :- !.
+
+get_col_id(_,bitv_not,bvnot) :- !.
+%get_col_id('Bitv_not',_,bvnot) :- !.
+get_col_id(_,bitv_and,bvand) :- !.
+%get_col_id('Bitv_and',_,bvand) :- !.
+get_col_id(_,bitv_or,bvor) :- !.
+%get_col_id('Bitv_or',_,bvor) :- !.
+get_col_id(_,bitv_xor,bvxor) :- !.
+%get_col_id('Bitv_xor',_,bvxor) :- !.
+get_col_id(_,bitv_nand,bvnand) :- !.
+%get_col_id('Bitv_nand',_,bvnand) :- !.
+get_col_id(_,bitv_nor,bvnor) :- !.
+%get_col_id('Bitv_nor',_,bvnor) :- !.
+get_col_id(_,bitv_xnor,bvxnor) :- !.
+%get_col_id('Bitv_xnor',_,bvxnor) :- !.
+get_col_id(_,bitv_comp,bvcomp) :- !.
+%get_col_id('Bitv_comp',_,bvcomp) :- !.
+get_col_id(_,bitv_neg,bvneg) :- !.
+%get_col_id('Bitv_neg',_,bvneg) :- !.
+get_col_id(_,bitv_add,bvadd) :- !.
+%get_col_id('Bitv_add',_,bvadd) :- !.
+get_col_id(_,bitv_sub,bvsub) :- !.
+%get_col_id('Bitv_sub',_,bvsub) :- !.
+get_col_id(_,bitv_mul,bvmul) :- !.
+%get_col_id('Bitv_mul',_,bvmul) :- !.
+get_col_id(_,bitv_udiv,bvudiv) :- !.
+%get_col_id('Bitv_udiv',_,bvudiv) :- !.
+get_col_id(_,bitv_urem,bvurem) :- !.
+%get_col_id('Bitv_urem',_,bvurem) :- !.
+get_col_id(_,bitv_sdiv,bvsdiv) :- !.
+%get_col_id('Bitv_sdiv',_,bvsdiv) :- !.
+get_col_id(_,bitv_srem,bvsrem) :- !.
+%get_col_id('Bitv_srem',_,bvsrem) :- !.
+get_col_id(_,bitv_smod,bvsmod) :- !.
+%get_col_id('Bitv_smod',_,bvsmod) :- !.
+get_col_id(_,bitv_shl,bvshl) :- !.
+%get_col_id('Bitv_shl',_,bvshl) :- !.
+get_col_id(_,bitv_shr,bvshr) :- !.
+%get_col_id('Bitv_shr',_,bvshr) :- !.
+get_col_id(_,bitv_ashr,bvashr) :- !.
+%get_col_id('Bitv_ashr',_,bvashr) :- !.
+get_col_id(_,bitv_lshr,bvlshr) :- !.
+%get_col_id('Bitv_lshr',_,bvlshr) :- !.
+
+get_col_id(_,bitv_ult,bvult) :- !.
+%get_col_id('Bitv_ult',_,bvult) :- !.
+get_col_id(_,bitv_ule,bvule) :- !.
+%get_col_id('Bitv_ule',_,bvule) :- !.
+get_col_id(_,bitv_ugt,bvugt) :- !.
+%get_col_id('Bitv_ugt',_,bvugt) :- !.
+get_col_id(_,bitv_uge,bvuge) :- !.
+%get_col_id('Bitv_uge',_,bvuge) :- !.
+get_col_id(_,bitv_slt,bvslt) :- !.
+%get_col_id('Bitv_slt',_,bvslt) :- !.
+get_col_id(_,bitv_sle,bvsle) :- !.
+%get_col_id('Bitv_sle',_,bvsle) :- !.
+get_col_id(_,bitv_sgt,bvsgt) :- !.
+%get_col_id('Bitv_sgt',_,bvsgt) :- !.
+get_col_id(_,bitv_sge,bvsge) :- !.
+%get_col_id('Bitv_sge',_,bvsge) :- !.
get_col_id('fp.abs',_,'fp.abs') :- !.
get_col_id('fp.neg',_,'fp.neg') :- !.
@@ -1420,6 +1452,7 @@ new_index_elem_val(sort(Sort),Var) ?- !,
((atomic(Var),get_binding(Var,_,_);
nonvar(Var),Var = select(_,_))
->
+ % cas déjà traités
true
; new_sort_val(Sort)).
new_index_elem_val(_,_).
@@ -2606,11 +2639,13 @@ smt_interp0(rotate_left(I,A),rotate_left(SA,NI,IA),uint(Size)) :- !,
smt_interp(I,NI,int),
integer(NI),
NI >= 0,
+ SA = Size,
smt_interp(A,IA,uint(Size)).
smt_interp0(rotate_right(I,A),rotate_right(SA,NI,IA),uint(Size)) :- !,
smt_interp(I,NI,int),
integer(NI),
NI >= 0,
+ SA = Size,
smt_interp(A,IA,uint(Size)).
smt_interp0(zero_extend(I,A),zero_extend(SA,NI,IA),uint(S)) :- !,
smt_interp(I,NI,int),
@@ -2744,6 +2779,12 @@ new_quantifier_abstraction(Res) :-
setval(decl,ODecl-NEnd),
Res = as(NVar,bool).
+% on garde les realString
+check_eval(Type,realString(Str),RE) ?- !,
+ RE = as(realString(Str),Type).
+% on traverse les as
+check_eval(_Type,as(E,Type),RE) ?- !,
+ check_eval(Type,E,RE).
check_eval(Type,E,RE) :-
(ground(E) ->
(var(Type) ->
@@ -2764,7 +2805,8 @@ add_as0(Type,I,AsI) :-
nonvar(Type),
(var(I);
atomic(I);
- functor(I,uninterp,_)),
+ functor(I,F,_),
+ occurs(F,(uninterp,realString))),
!,
AsI = as(I,Type).
add_as0(Type,I,AsI) :-
diff --git a/Src/COLIBRI/solve.pl b/Src/COLIBRI/solve.pl
index d032e51f110966eee1e616fb1dec9e15dd5df1bb..fe28dee9258fa0f7a07ed497188e6444e9f8be7e 100644
--- a/Src/COLIBRI/solve.pl
+++ b/Src/COLIBRI/solve.pl
@@ -157,6 +157,7 @@ trans_col(or_seq_reif(X,_,Y,Z),(X or Y) #= Z).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% TODO : ajouter declaration type pour BV
unfold_int_expr_block(E,D,C,T,R) :-
+ get_priority(P),
call_priority(
block(once unfold_int_expr(E,D,C,T,R),
Tag,
@@ -165,7 +166,9 @@ unfold_int_expr_block(E,D,C,T,R) :-
; exit_block(Tag))),
1),
call(smt_check_disabled_delta)@eclipse,
- garbage_collect.
+ garbage_collect,
+ set_priority(P),
+ wake.
'#:'(L,I) :-
(I == bool ->
@@ -347,7 +350,9 @@ rnd_vars(T) :-
insert_dep_inst(inst_cstr(0,X))))).
array_vars(TypeI,TypeE0,[T|LT]) ?- !,
- (real_type(TypeE0,TypeE) ->
+ ((TypeE0 \== real_int,
+ real_type(TypeE0,TypeE))
+ ->
true
; TypeE = TypeE0),
(foreach(X,[T|LT]),
@@ -361,7 +366,9 @@ array_vars(TypeI,TypeE0,[T|LT]) ?- !,
array_vars(TypeI,TypeE0,X) :-
var(X),
!,
- (real_type(TypeE0,TypeE) ->
+ ((TypeE0 \== real_int,
+ real_type(TypeE0,TypeE))
+ ->
true
; TypeE = TypeE0),
(get_variable_type(X,array(TypeI,TypeE)) ->
@@ -1045,39 +1052,19 @@ unfold_int_expr(bvnot(Size,EA), D, Cstr, Type, R) ?-
integer(Size),
Size > 0,
Type = uint(Size),
- (bvnot_expr(Size,EA,NotEA) ->
- !,
- unfold_int_expr(NotEA,D,Cstr,Type,R)
- ; ND is D + 1,
- ((Size == 1,
- nonvar(R))
- ->
- !,
- NotR is (R+1) mod 2,
- unfold_int_expr(EA,ND,Cstr,Type,NotR)
- ; unfold_int_expr(EA,ND,CA,Type,A),
- !,
- (number(A) ->
- bvnot(Size,A,R0),
- blocked_unify(R,R0),
- Cstr = CA
- ; (fail,Size == 1 ->
- int_vars(Type,R)
- ; set_int_type(Type,R)),
- insert_dep_inst(dep(R,D,[A])),
- make_conj(CA, bvnot(Size,A,R),Cstr)))).
+ !,
+ unfold_int_expr(EA,D,CA,Type,A),
+ insert_dep_inst(dep(R,D,[A])),
+ make_conj(CA, bvnot(Size,A,R),Cstr).
unfold_int_expr(bvnand(Size,EA,EB), D, Cstr, Type, R) ?- !,
- ND is D - 1,
- unfold_int_expr(bvnot(Size,bvand(Size,EA,EB)), ND, Cstr, Type, R).
+ unfold_int_expr(bvnot(Size,bvand(Size,EA,EB)), D, Cstr, Type, R).
unfold_int_expr(bvnor(Size,EA,EB), D, Cstr, Type, R) ?- !,
- ND is D - 1,
- unfold_int_expr(bvnot(Size,bvor(Size,EA,EB)), ND, Cstr, Type, R).
+ unfold_int_expr(bvnot(Size,bvor(Size,EA,EB)), D, Cstr, Type, R).
unfold_int_expr(bvxnor(Size,EA,EB), D, Cstr, Type, R) ?- !,
- ND is D - 1,
- unfold_int_expr(bvnot(Size,bvxor(Size,EA,EB)), ND, Cstr, Type, R).
+ unfold_int_expr(bvnot(Size,bvxor(Size,EA,EB)), D, Cstr, Type, R).
unfold_int_expr(bvcomp(Size,EA,EB), D, Cstr, RType, R) ?-
ND is D + 1,
@@ -1101,43 +1088,26 @@ unfold_int_expr(bvcomp(Size,EA,EB), D, Cstr, RType, R) ?-
insert_dep_inst(dep(R,D,[A,B])),
make_conj(CAB, eq_int_reif(Type,A,B,R),Cstr)).
+/*
+Size = 6,
+int_vars(uint(Size),(A,NA)),
+DpSize is 2^Size,
+bvneg(Size,A) #= NA,
+uintN_from_int(Size,(as(DpSize,int) - int_from_uintN(Size,A)) mod DpSize) #\=
+ NA,
+solve_cstrs.
+*/
unfold_int_expr(bvneg(Size,EA), D, Cstr, Type, R) ?- !,
integer(Size),
Size > 0,
Type = uint(Size),
- %ça risque pas de fail parce qu'on est en unsigned?
+ % ça risque pas de fail parce qu'on est en unsigned?
(Size == 1 ->
get_reif_var_depth_from_labchoice(DD),
insert_dep_inst(dep(inst_cstr(DD,R)))
; true),
unfold_int_expr(-EA, D, Cstr, Type, R).
-%% unfold_int_expr(bvadd(Size,EA,EB), D, Cstr, Type, R) ?-
-%% ND is D + 1,
-%% integer(Size),
-%% Size > 0,
-%% Type = uint(Size),
-%% unfold_int_expr(EA,ND,CA,Type,A),
-%% unfold_int_expr(EB,ND,CB,Type,B),
-%% !,
-%% insert_dep_inst(dep(R,D,[A,B])),
-%% (Size == 1 ->
-%% get_reif_var_depth_from_labchoice(DD),
-%% insert_dep_inst(dep(inst_cstr(DD,R)))
-%% ; true),
-%% Mask is \ (-1 << Size),
-%% make_conj(CA,CB,CAB),
-%% %% make_conj(CAB, (add(Type,D,A,B,R,UO),
-%% %% bvand(Size, A, Mask, AA),
-%% %% bvand(Size, B, Mask, BB),
-%% %% bvand(Size, R, Mask, RR)%,
-%% %% %bvadd(Size, AA, BB, RR)
-%% %% ),
-%% %% Cstr).
-%% %make_conj(CAB, (add(Type,D,A,B,R,UO), bvadd(Size, A, B, R)),Cstr).
-%% make_conj(CAB, (add(Type,D,A,B,R,UO) ),Cstr).
-%% %make_conj(CAB, ( bvadd(Size, A, B, R)),Cstr).
-
/*
Size = 8, int_vars(uint(Size),[A,B]),
bvadd(Size,A,B) #\= uintN_from_int(Size,int_from_uintN(Size,A) + int_from_uintN(Size,B)),
@@ -1148,9 +1118,6 @@ unfold_int_expr(bvadd(Size,EA,EB), D, Cstr, Type, R) ?-
Size > 0,
!,
Type = uint(Size),
- (fail,Size == 1 ->
- int_vars(Type,R)
- ; true),
unfold_int_expr(EA + EB, D, Cstr, Type, R).
/*
@@ -1163,10 +1130,15 @@ unfold_int_expr(bvsub(Size,EA,EB), D, Cstr, Type, R) ?-
Size > 0,
!,
Type = uint(Size),
- (fail,Size == 1 ->
- int_vars(Type,R)
- ; true),
+ unfold_int_expr(bvadd(Size,EA,bvneg(Size,EB)), D, Cstr, Type, R).
+/*
+unfold_int_expr(bvsub(Size,EA,EB), D, Cstr, Type, R) ?-
+ integer(Size),
+ Size > 0,
+ !,
+ Type = uint(Size),
unfold_int_expr(EA - EB, D, Cstr, Type, R).
+*/
/*
Size = 6, int_vars(uint(Size),[A,B]),
@@ -1178,33 +1150,36 @@ unfold_int_expr(bvmul(Size,EA,EB), D, Cstr, Type, R) ?-
Size > 0,
!,
Type = uint(Size),
- (fail,Size == 1 ->
- int_vars(Type,R)
- ; true),
unfold_int_expr(EA * EB, D, Cstr, Type, R).
/*
- Size = 6, int_vars(uint(Size),[A,B]),
- bvmul(Size,A,B) #\= uintN_from_int(Size,int_from_uintN(Size,A) * int_from_uintN(Size,B)),
- solve_cstrs.
+Size = 6, int_vars(uint(Size),[A,B,Q]),
+DpSizeM1 is (2^Size)-1,
+uintN_from_int(Size,ite(B#=0,as(DpSizeM1,int),int_from_uintN(Size,A) div
+int_from_uintN(Size,B))) #= Q,
+bvudiv(Size,A,B) #\= Q,
+solve_cstrs.
*/
unfold_int_expr(bvudiv(Size,EA,EB), D, Cstr, Type, R) ?-
integer(Size),
Size > 0,
!,
Type = uint(Size),
- (fail,Size == 1 ->
- int_vars(Type,R)
- ; true),
unfold_int_expr(EA // EB, D, Cstr, Type, R).
+
+/*
+Size = 6, int_vars(uint(Size),[A,B,R]),
+DpSizeM1 is (2^Size)-1,
+uintN_from_int(Size,ite(B#=0,int_from_uintN(Size,A),int_from_uintN(Size,A) rem
+int_from_uintN(Size,B))) #= R,
+bvurem(Size,A,B) #\= R,
+solve_cstrs.
+*/
unfold_int_expr(bvurem(Size,EA,EB), D, Cstr, Type, R) ?-
integer(Size),
Size > 0,
!,
Type = uint(Size),
- (fail,Size == 1 ->
- int_vars(Type,R)
- ; true),
unfold_int_expr(EA rem EB, D, Cstr, Type, R).
@@ -1232,7 +1207,33 @@ unfold_int_expr(bvsdiv(Size,EA,EB), D, Cstr, Type, R) ?-
Size > 0,
!,
Type = uint(Size),
- unfold_int_expr(uintN_from_intN(Size,intN_from_uint(Size,EA) // intN_from_uint(Size,EB)),D,Cstr,Type,R).
+ PSize is Size - 1,
+ DDD is D + 2,
+ DD is D + 1,
+ unfold_int_expr(EA,DDD,CA,Type,A),
+ unfold_int_expr(extract(Size,PSize,PSize,A),DD,CSA,uint(1),SA),
+ make_conj(CA,CSA,CstrA0),
+ unfold_int_expr(ite(as(SA,uint(1))#=0,
+ A,
+ bvneg(Size,A)),
+ DD,CabsA,Type,AbsA),
+ make_conj(CstrA0,CabsA,CstrA),
+ unfold_int_expr(EB,DDD,CB,Type,B),
+ unfold_int_expr(extract(Size,PSize,PSize,B),DD,CSB,uint(1),SB),
+ make_conj(CB,CSB,CstrB0),
+ unfold_int_expr(ite(as(SB,uint(1))#=0,
+ B,
+ bvneg(Size,B)),
+ DD,CabsB,Type,AbsB),
+ make_conj(CstrB0,CabsB,CstrB),
+ make_conj(CstrA,CstrB,CAB),
+ unfold_int_expr(ite(as(SA,uint(1)) #= SB,
+ bvudiv(Size,AbsA,AbsB),
+ bvneg(Size,bvudiv(Size,AbsA,AbsB))),
+ D,CR,Type,R),
+ make_conj(CAB,CR,Cstr).
+% FAUX
+% unfold_int_expr(uintN_from_intN(Size,intN_from_uint(Size,EA) // intN_from_uint(Size,EB)),D,Cstr,Type,R).
/* Test definition bvsrem
Size = 8,
@@ -1258,7 +1259,35 @@ unfold_int_expr(bvsrem(Size,EA,EB), D, Cstr, Type, R) ?-
Size > 0,
!,
Type = uint(Size),
- unfold_int_expr(uintN_from_intN(Size,intN_from_uint(Size,EA) rem intN_from_uint(Size,EB)),D,Cstr,Type,R).
+ PSize is Size - 1,
+ DDD is D + 2,
+ DD is D + 1,
+ unfold_int_expr(EA,DDD,CA,Type,A),
+ unfold_int_expr(extract(Size,PSize,PSize,A),DD,CSA,uint(1),SA),
+ make_conj(CA,CSA,CstrA0),
+ unfold_int_expr(ite(as(SA,uint(1)) #= 0,
+ A,
+ bvneg(Size,A)),
+ DD,CabsA,Type,AbsA),
+ make_conj(CstrA0,CabsA,CstrA),
+ unfold_int_expr(EB,DDD,CB,Type,B),
+ unfold_int_expr(extract(Size,PSize,PSize,B),DD,CSB,uint(1),SB),
+ make_conj(CB,CSB,CstrB0),
+ unfold_int_expr(ite(as(SB,uint(1)) #= 0,
+ B,
+ bvneg(Size,B)),
+ DD,CabsB,Type,AbsB),
+ make_conj(CstrB0,CabsB,CstrB),
+ make_conj(CstrA,CstrB,CAB),
+ unfold_int_expr(bvurem(Size,AbsA,AbsB),DDD,CU,Type,U),
+ make_conj(CAB,CU,CABU),
+ unfold_int_expr(ite(as(SA,uint(1)) #= 0,
+ U,
+ bvneg(Size,U)),
+ D,CR,Type,R),
+ make_conj(CABU,CR,Cstr).
+% FAUX
+% unfold_int_expr(uintN_from_intN(Size,intN_from_uint(Size,EA) rem intN_from_uint(Size,EB)),D,Cstr,Type,R).
/* Test definition bvsmod
Size = 8,
@@ -1289,7 +1318,42 @@ unfold_int_expr(bvsmod(Size,EA,EB), D, Cstr, Type, R) ?-
Size > 0,
!,
Type = uint(Size),
- unfold_int_expr(uintN_from_intN(Size,intN_from_uint(Size,EA) mod intN_from_uint(Size,EB)),D,Cstr,Type,R).
+ PSize is Size - 1,
+ DDD is D + 2,
+ DD is D + 1,
+ unfold_int_expr(EA,DDD,CA,Type,A),
+ unfold_int_expr(extract(Size,PSize,PSize,A),DD,CSA,uint(1),SA),
+ make_conj(CA,CSA,CstrA0),
+ unfold_int_expr(ite(as(SA,uint(1)) #= 0,
+ A,
+ bvneg(Size,A)),
+ DD,CabsA,Type,AbsA),
+ make_conj(CstrA0,CabsA,CstrA),
+ unfold_int_expr(EB,DDD,CB,Type,B),
+ unfold_int_expr(extract(Size,PSize,PSize,B),DD,CSB,uint(1),SB),
+ make_conj(CB,CSB,CstrB0),
+ unfold_int_expr(ite(as(SB,uint(1)) #= 0,
+ B,
+ bvneg(Size,B)),
+ DD,CabsB,Type,AbsB),
+ make_conj(CstrB0,CabsB,CstrB),
+ make_conj(CstrA,CstrB,CAB),
+ unfold_int_expr(bvurem(Size,AbsA,AbsB),DDD,CU,Type,U),
+ make_conj(CAB,CU,CABU),
+ unfold_int_expr(ite(as(U,Type) #= 0,
+ U,
+ ite((as(SA,uint(1)) #= 0) and (as(SB,uint(1)) #= 0),
+ U,
+ ite((as(SA,uint(1)) #= 1) and (as(SB,uint(1)) #= 0),
+ bvadd(Size,bvneg(Size,U),B),
+% bvsub(Size,B,U),
+ ite((as(SA,uint(1)) #= 0) and (as(SB,uint(1)) #= 1),
+ bvadd(Size,U,B),
+ bvneg(Size,U))))),
+ D,CR,Type,R),
+ make_conj(CABU,CR,Cstr).
+% FAUX
+% unfold_int_expr(uintN_from_intN(Size,intN_from_uint(Size,EA) mod intN_from_uint(Size,EB)),D,Cstr,Type,R).
unfold_int_expr(bvashr(Size,EA,EB), D, Cstr, Type, R) ?-
ND is D + 1,
@@ -1313,6 +1377,23 @@ unfold_int_expr(bvashr(Size,EA,EB), D, Cstr, Type, R) ?-
insert_dep_inst(dep(R,D,[A,B])),
make_conj(CAB,bvasr(Size,A,B,R),Cstr)).
+/*
+% preuve bvudiv
+int_vars(uint(6),A),
+member(B,[0,1,2,3,4,5]),
+bvlshr(6,A,as(B,uint(6))) #= as(R,uint(6)),
+DpB is 2^B,
+bvudiv(6,A,as(DpB,uint(6))) #\= as(R,uint(6)),
+solve_cstrs.
+
+% preuve zero_extend/extract
+int_vars(uint(6),A),
+member(B,[0,1,2,3,4,5]),
+bvlshr(6,A,as(B,uint(6))) #= as(R,uint(6)),
+SE is 6 - B,
+zero_extend(SE,B,extract(6,5,B,A)) #\= as(R,uint(6)),
+solve_cstrs.
+*/
unfold_int_expr(bvlshr(Size,EA,EB), D, Cstr, Type, R) ?-
ND is D + 1,
integer(Size),
@@ -1321,9 +1402,6 @@ unfold_int_expr(bvlshr(Size,EA,EB), D, Cstr, Type, R) ?-
unfold_int_expr(EA,ND,CA,Type,A),
unfold_int_expr(EB,ND,CB,Type,B),
!,
- (fail,Size == 1 ->
- int_vars(Type,R)
- ; true),
make_conj(CA,CB,CAB),
((number(A),
number(B))
@@ -1335,6 +1413,26 @@ unfold_int_expr(bvlshr(Size,EA,EB), D, Cstr, Type, R) ?-
insert_dep_inst(dep(R,D,[A,B])),
make_conj(CAB,bvlsr(Size,A,B,R),Cstr)).
+/* ??????
+% preuve bvmul
+int_vars(uint(6),A),
+member(B,[0,1,2,3,4,5]),
+bvshl(6,A,as(B,uint(6))) #= as(R,uint(6)),
+DpB is 2^B,
+bvmul(6,A,as(DpB,uint(6))) #\= as(R,uint(6)),
+solve_cstrs.
+
+% preuve concat/extract
+int_vars(uint(6),A),
+member(B,[0,1,2,3,4,5]),
+bvshl(6,A,as(B,uint(6))) #= as(R,uint(6)),
+Bp1 is B + 1,
+H is 6-Bp1,
+SBeg is H+1,
+concat(SBeg,extract(6,H,0,A),B,as(0,uint(B))) #= as(R1,uint(6)),
+as(R1,uint(6)) #\= as(R,uint(6)),
+solve_cstrs.
+*/
unfold_int_expr(bvshl(Size,EA,EB), D, Cstr, Type, R) ?-
ND is D + 1,
integer(Size),
@@ -1350,43 +1448,49 @@ unfold_int_expr(bvshl(Size,EA,EB), D, Cstr, Type, R) ?-
bvsl(Size,A,B,R0),
blocked_unify(R,R0),
Cstr = CAB
- ; (fail,Size == 1 ->
- int_vars(Type,R)
- ; set_int_type(Type,R)),
- insert_dep_inst(dep(R,D,[A,B])),
+ ; insert_dep_inst(dep(R,D,[A,B])),
make_conj(CAB,bvsl(Size,A,B,R),Cstr)).
unfold_int_expr(concat(SizeA,EA,SizeB,EB), D, Cstr, Type, R) ?-
- Type = uint(Size),
- ND is D + 1,
- integer(SizeA),
- SizeA > 0,
- integer(SizeB),
- SizeB > 0,
- unfold_int_expr(EA,ND,CA,uint(SizeA),A),
- unfold_int_expr(EB,ND,CB,uint(SizeB),B),
- !,
- Size is SizeA+SizeB,
- make_conj(CA,CB,CAB),
- ((number(R) ->
- (number(A);
- number(B))
- ; (number(A),
- number(B)))
+ ((SizeA == 0,
+ AB = EB;
+ SizeB == 0,
+ AB = EA)
->
- (bvconcat(SizeA,A,SizeB,B,R) ->
- true
- ; exit_block(unsat)),
- Cstr = CAB
- ; insert_dep_inst(dep(R,D,[A,B])),
- (fail,SizeA == 1 ->
- int_vars(uint(1),A)
- ; true),
- (fail,SizeB == 1 ->
- int_vars(uint(1),B)
- ; true),
- make_conj(CAB, bvconcat(SizeA,A,SizeB,B,R),Cstr)).
+ !,
+ unfold_int_expr(AB,D,Cstr,Type,R)
+ ; Type = uint(Size),
+ ND is D + 1,
+ integer(SizeA),
+ SizeA > 0,
+ integer(SizeB),
+ SizeB > 0,
+ unfold_int_expr(EA,ND,CA,uint(SizeA),A),
+ unfold_int_expr(EB,ND,CB,uint(SizeB),B),
+ !,
+ Size is SizeA+SizeB,
+ make_conj(CA,CB,CAB),
+ ((number(R) ->
+ (number(A);
+ number(B))
+ ; (number(A),
+ number(B)))
+ ->
+ (bvconcat(SizeA,A,SizeB,B,R) ->
+ true
+ ; exit_block(unsat)),
+ Cstr = CAB
+ ; insert_dep_inst(dep(R,D,[A,B])),
+ make_conj(CAB, bvconcat(SizeA,A,SizeB,B,R),Cstr))).
+/*
+int_vars(uint(6),A),
+extract(6,5,4,A) #= as(Beg,uint(2)),
+extract(6,3,2,A) #= as(Mid,uint(2)),
+extract(6,1,0,A) #= as(End,uint(2)),
+concat(4,concat(2,Beg,2,Mid),2,End) #\= A,
+solve_cstrs.
+*/
unfold_int_expr(extract(SizeA,I,J,EA), D, Cstr, Type, R) ?-
Type = uint(N),
integer(SizeA), integer(I), integer(J),
@@ -1460,6 +1564,15 @@ unfold_int_expr(repeat(Size,I,EA), D, Cstr, Type, R) ?-
/*NoDeltaBV*/ make_conj(CA, repeat(Size,I,A,R), Cstr)).
%%/*DeltaBV*/make_conj(CA, (repeat(Size,I,A,R), launch_geq(R,A)), Cstr)).
+/*
+Size = 8,I = 3,
+SizeR is Size + I,
+int_vars(uint(Size),A),
+int_vars(uint(SizeR),R),
+concat(I,repeat(1,I,as(0,uint(1))),Size,A) #= R,
+zero_extend(Size,I,A) #\= R,
+solve_cstrs.
+*/
unfold_int_expr(zero_extend(Size,I,EA), D, Cstr, Type, R) ?-
Type = uint(SizeR),
integer(Size),
@@ -1492,6 +1605,16 @@ unfold_int_expr(zero_extend(Size,I,EA), D, Cstr, Type, R) ?-
D,Cstr,Type,R).
*/
+/*
+Size = 8,I = 3,
+SizeR is Size + I,
+int_vars(uint(Size),A),
+int_vars(uint(SizeR),R),
+extract(Size,7,7,A) #= as(SA,uint(1)),
+concat(I,repeat(1,I,SA),Size,A) #= R,
+sign_extend(Size,I,A) #\= R,
+solve_cstrs.
+*/
unfold_int_expr(sign_extend(Size,I,EA), D, Cstr, Type, R) ?-
integer(Size),
integer(I),
@@ -1537,7 +1660,19 @@ unfold_int_expr(bvugt(EA, EB), D, Cstr, Type, R) ?-
unfold_int_expr(bvuge(EA, EB), D, Cstr, Type, R) ?-
!, unfold_int_expr(EA >= EB, D, Cstr, Type, R).
-
+/*
+Size = 5,PSize is Size - 1,
+int_vars(uint(Size),(S,T)),
+int_vars(uint(1),(Ss,St)),
+extract(Size,PSize,PSize,S) #= as(Ss,uint(1)),
+extract(Size,PSize,PSize,T) #= as(St,uint(1)),
+bvslt(Size,S,T) #= as(B,bool),
+ite((Ss #= as(1,uint(1))) and (St #= as(0,uint(1))),
+ as(1,bool),
+ (Ss #= St) and bvult(S,T)) #= as(NB,bool),
+as(NB,bool) #\= as(B,bool),
+solve_cstrs.
+*/
unfold_int_expr(bvslt(N, EA, EB), D, Cstr, Type, R) ?-
!,
unfold_int_expr(intN_from_uint(N,EA) < intN_from_uint(N,EB),D,Cstr,Type,R).
@@ -1558,6 +1693,20 @@ unfold_int_expr(bvslt(N, EA, EB), D, Cstr, Type, R) ?-
bvult(as(A,uint(N)),as(B,uint(N))))),
D, Cstr, Type, R).
*/
+
+/*
+Size = 5,PSize is Size - 1,
+int_vars(uint(Size),(S,T)),
+int_vars(uint(1),(Ss,St)),
+extract(Size,PSize,PSize,S) #= as(Ss,uint(1)),
+extract(Size,PSize,PSize,T) #= as(St,uint(1)),
+bvsle(Size,S,T) #= as(B,bool),
+ite((Ss #= as(1,uint(1))) and (St #= as(0,uint(1))),
+ as(1,bool),
+ (Ss #= St) and bvule(S,T)) #= as(NB,bool),
+as(NB,bool) #\= as(B,bool),
+solve_cstrs.
+*/
unfold_int_expr(bvsle(N, EA, EB), D, Cstr, Type, R) ?-
!,
unfold_int_expr(intN_from_uint(N,EA) =< intN_from_uint(N,EB), D, Cstr, Type, R).
@@ -1825,15 +1974,7 @@ unfold_int_expr(EA // EB,D,Cstr,Type,R) ?-
insert_dep_inst(dep(Rem,D,[UO])),
make_conj(CA,CB,CAB),
make_conj(CAB,Cond,CABCond),
- ((number(A),
- number(B),
- CABCond == true)
- ->
- chk_undef_div_rem(Bool,Type,A,B,R0,Rem,UO),
- blocked_unify(R,R0),
- Cstr = CABCond
- ; make_conj(CAB,Cond,CABCond),
- make_conj(CABCond,chk_undef_div_rem(Bool,Type,A,B,R,Rem,UO),Cstr)).
+ 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) ?-
ND is D + 1,
unfold_int_expr(EA,ND,CA,Type,A),
@@ -1856,14 +1997,7 @@ unfold_int_expr(EA rem EB,D,Cstr,Type,R) ?-
insert_dep_inst(dep(Q,D,[UO])),
make_conj(CA,CB,CAB),
make_conj(CAB,Cond,CABCond),
- ((number(A),
- number(B),
- CABCond == true)
- ->
- chk_undef_div_rem(Bool,Type,A,B,Q,R0,UO),
- blocked_unify(R,R0),
- Cstr = CABCond
- ; make_conj(CABCond,chk_undef_div_rem(Bool,Type,A,B,Q,R,UO),Cstr)).
+ 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),
@@ -1881,14 +2015,7 @@ unfold_int_expr(EA div EB,D,Cstr,Type,R) ?-
insert_dep_inst(dep(Rst,D,[A,B,Bool,R])),
make_conj(CA,CB,CAB),
make_conj(CAB,Cond,CABCond),
- ((number(A),
- number(B),
- CABCond == true)
- ->
- chk_undef_ediv_mod(Bool,Type,A,B,R0,Rst),
- blocked_unify(R,R0),
- Cstr = CABCond
- ; make_conj(CABCond,chk_undef_ediv_mod(Bool,Type,A,B,R,Rst),Cstr)).
+ make_conj(CABCond,chk_undef_ediv_mod(Bool,Type,A,B,R,Rst),Cstr).
unfold_int_expr(EA mod EB,D,Cstr,Type,R) ?-
ND is D + 1,
unfold_int_expr(EA,ND,CA,Type,A),
@@ -1906,14 +2033,7 @@ unfold_int_expr(EA mod EB,D,Cstr,Type,R) ?-
insert_dep_inst(dep(Q,D,[A,B,Bool,R])),
make_conj(CA,CB,CAB),
make_conj(CAB,Cond,CABCond),
- ((number(A),
- number(B),
- CABCond == true)
- ->
- chk_undef_ediv_mod(Bool,Type,A,B,Q,R0),
- blocked_unify(R,R0),
- Cstr = CABCond
- ; make_conj(CABCond,chk_undef_ediv_mod(Bool,Type,A,B,Q,R),Cstr)).
+ make_conj(CABCond,chk_undef_ediv_mod(Bool,Type,A,B,Q,R),Cstr).
unfold_int_expr(EA ^ EN,D,Cstr,Type,R) ?-
ND is D + 1,
@@ -1975,18 +2095,7 @@ unfold_int_expr(EA #= EB,D,Cstr,Type0,R) ?-
!,
unfold_int_expr(neg(alldiff(Type,[as(A,Type),EB])),D,CEq,bool,R),
make_conj(CA,CEq,Cstr)
- ; (R == 1 ->
- A = B
- ; ((R == 0,
- number(A),
- (Type == bool;
- Type == uint(1)))
- ->
- (Type == bool ->
- not_expr(A,B)
- ; bvnot_expr(1,as(A,Type),B))
- ; true)),
- unfold_int_expr(EB,ND,CB,Type,B),
+ ; unfold_int_expr(EB,ND,CB,Type,B),
!,
(R == 1 ->
blocked_unify(A=B)
@@ -2052,18 +2161,7 @@ unfold_int_expr(EA #\= EB,D,Cstr,Type0,R) ?-
!,
unfold_int_expr(alldiff(Type,[as(A,Type),EB]),D,CDiff,bool,R),
make_conj(CA,CDiff,Cstr)
- ; (R == 0 ->
- A = B
- ; ((R == 1,
- number(A),
- (Type == bool;
- Type == uint(1)))
- ->
- (Type == bool ->
- not_expr(A,B)
- ; bvnot_expr(1,as(A,Type),B))
- ; true)),
- unfold_int_expr(EB,ND,CB,Type,B),
+ ; unfold_int_expr(EB,ND,CB,Type,B),
!,
(R == 0 ->
blocked_unify(A=B)
@@ -3012,7 +3110,7 @@ unfold_int_expr(isInfinite(ERF),D,Cstr,Type,R) ?-
make_conj(C,isInfinite(RType,RF,R),Cstr)).
unfold_int_expr(isZero(ERF),D,Cstr,Type,R) ?-
- ND is D - 1,
+ ND is D + 1,
Type = bool,
(R == 1 ->
ensure_not_NaN(RF)
@@ -3229,7 +3327,7 @@ unfold_int_expr(uninterp(Term),D,Cstr,Type,R) ?- !,
fromto(true,IC,OC,ACstrs),
param(D) do
functor(TypeArg,T,_),
- (occurs(T,(bool,int,uint,sort,rnd)) ->
+ (occurs(T,(bool,int,uint,sort,rnd,array)) ->
unfold_int_expr(Arg,D,AC,TypeArg,AR),
SetType = int_vars(TypeArg,AR)
; unfold_real_expr(Arg,D,AC,TypeArg,AR),
@@ -3294,8 +3392,10 @@ get_reif_var_depth_from_labchoice(D) :-
D = 0
; D is 2^32).
+/*
bvnot_expr(Size,bvnot(Size,EA),E) ?- !,
E = EA.
+*/
bvnot_expr(Size,bvand(Size,EA,EB),E) ?- !,
E = bvor(Size,bvnot(Size,EA),bvnot(Size,EB)).
bvnot_expr(Size,bvor(Size,EA,EB),E) ?- !,
@@ -3306,9 +3406,9 @@ bvnot_expr(1,as(1,_),R) ?- !,
blocked_unify(R,0).
not_expr(0,B) ?- !,
- blocked_unify(B = 1).
+ blocked_unify(B,1).
not_expr(1,B) ?- !,
- blocked_unify(B = 0).
+ blocked_unify(B,0).
not_expr(neg(A),NA) ?- !,
NA = A.
not_expr(A => B,E) ?-
@@ -3367,11 +3467,12 @@ not_expr(bvsge(A,B),E) ?- !,
not_expr(bvsgt(A,B),E) ?- !,
E = bvsle(A,B).
not_expr(alldiff(Type,[A,B]),E) ?-
- (Type == int ->
- E = (as(A,Type) #= as(B,Type))
- ; atomic(Type),
- occurs(Type,(real,real_int)),
- E = (as(A,Type) $= as(B,Type))),
+ nonvar(Type),
+ !,
+ functor(Type,FType,_),
+ (real_type(FType,_) ->
+ E = (as(A,Type) $= as(B,Type))
+ ; E = (as(A,Type) #= as(B,Type))),
!.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -3944,17 +4045,18 @@ smtlib_select(array(TypeI,TypeE),A,I,E) :-
smtlib_select(A,A,Sure,I,E,TypeI,TypeE).
smtlib_select(A,Start,Sure,I,E,TypeI,TypeE) :-
- get_priority(P),
+ get_priority(P0),
+ %pour scheduling v7 (mise à 2 au réveil)
+ P = 4,
+ max(P0,P,NP),
set_priority(1),
get_array_start(Start,NStart),
(var(NStart) ->
save_cstr_suspensions(NStart)
; true),
- (smtlib_select_bis(A,Sure,I,E,TypeI,TypeE) ->
- true
- ; smtlib_select_bis(A,Sure,I,E,TypeI,TypeE)),
- set_priority(P),
- wake_if_other_scheduled(P).
+ smtlib_select_bis(A,Sure,I,E,TypeI,TypeE),
+ set_priority(NP),
+ wake_if_other_scheduled(NP).
smtlib_select_bis(A,Sure,I,E,TypeI,TypeE) :-
((nonvar(I),
@@ -4373,7 +4475,10 @@ eq_array0(Type,A,B) :-
wake_if_other_scheduled(P).
eq_array(Type,Diff,A,B,Seen,SureA,SureB) :-
- get_priority(P),
+ get_priority(P0),
+ %pour la v7 (2 au réveil)
+ P = 5,
+ max(P0,P,NP),
set_priority(1),
% on garde les over-write non egaux
% et on etend les sure (index non unifiables)
@@ -4391,7 +4496,7 @@ eq_array(Type,Diff,A,B,Seen,SureA,SureB) :-
move_inst_seen(Seen,NSeen),
eq_clean_array(Type,Diff,NA,NB,NSeen,NSureA,NSureB),
set_priority(P),
- wake_if_other_scheduled(P).
+ wake_if_other_scheduled(NP).
eq_clean_array(Type,Diff,A,B,Seen,SureA,SureB) :-
% Seen contient tout les index sures de A ou B
@@ -4427,7 +4532,7 @@ eq_clean_array(Type,Diff,A,B,Seen,SureA,SureB) :-
; % DiffA et DiffB contiennent les select en attente
% on doit attendre qu'ils disparaissent pour
% unifier
- call(spy_here)@eclipse,
+ % call(spy_here)@eclipse,
(DiffA == [] ->
(foreach((I,E),DiffB),
param(Type,NA) do
@@ -4763,11 +4868,26 @@ diff_array(Type,A,B) :-
% Il existe un indice commun ou les elements sont non
% unifiables
check_diff_array(A,B)
+ ; Type = array(TI,TE),
+ (real_type(TI,_) ->
+ real_vars(TI,I)
+ ; % ok pour les "sort" aussi
+ int_vars(TI,I)),
+ (real_type(TE,_) ->
+ real_vars(TE,[EA,EB])
+ ; % ok pour les "sort/array" aussi
+ int_vars(TE,[EA,EB])),
+ smtlib_select(Type,A,I,EA),
+ smtlib_select(Type,B,I,EB),
+ diff_reif(TE,_,EA,EB,1)),
+/*
+% ANCIENNE VERSION MOINS RAPIDE QUE LES "select" !!!
; hash_create(SureA),
hash_create(SureB),
clean_array(A,NA,(SureA,[]),NSureA),
clean_array(B,NB,(SureB,[]),NSureB),
diff_clean_array(Type,NA,NB,NSureA,NSureB)),
+*/
set_priority(P),
wake_if_other_scheduled(P).
@@ -4779,7 +4899,9 @@ diff_array1(Type,const_array(TI,TE,Const),A,_,_) ?- !,
diff_array1(Type,A,const_array(TI,TE,Const),_,_) ?- !,
diff_array1(Type,const_array(TI,TE,Const),A,_,_).
diff_array1(Type,A0,B0,SureA,SureB) :-
- get_priority(P),
+ get_priority(P0),
+ % pour la v7
+ P is max(P0,5),
set_priority(1),
clean_array(A0,A,SureA,NSureA),
clean_array(B0,B,SureB,NSureB),
@@ -4814,8 +4936,8 @@ diff_clean_array(Type,A0,B0,SureA,SureB) :-
; % on est bloque sur les elements des index communs
LEAB = [_,EA,EB|_],
ite_diff_array(Type,EA,EB,NA,NB,SureA,SureB))
- ; ((var(NA),V=NA,T=NB,Sure = SureB;
- var(NB),V=NB,T=NA,Sure = SureA)
+ ; ((var(NA),T=NB,Sure = SureB;
+ var(NB),T=NA,Sure = SureA)
->
% Si un index de T n'est pas sure, il est bloquant
% ainsi que les index sures unifiables
@@ -6154,6 +6276,9 @@ real_vars(Type,T) :-
; true)
; launch_float_number(X))).
+set_real_type(real_int,V) ?- !,
+ set_lazy_domain(real,V),
+ launch_float_int_number(V).
set_real_type(Type,V) :-
set_lazy_domain(Type,V).
@@ -6422,7 +6547,10 @@ unfold_real_expr(ceiling(EA),D,Cstr,Type,R) :-
make_conj(CACond,fp_ceiling(BCond,RType,A,R),Cstr)).
% Conversions depuis int
-unfold_real_expr(real_from_int(EA),D,Cstr,real,R) :-
+unfold_real_expr(real_from_int(EA),D,Cstr,Type,R) :-
+ (var(Type) ->
+ Type = real
+ ; real_type(Type,_)),
ND is D + 1,
unfold_int_expr(EA,ND,CA,int,A),
!,
@@ -7361,7 +7489,7 @@ unfold_real_expr(uninterp(Term),D,Cstr,Type,R) ?- !,
fromto(true,IC,OC,ACstrs),
param(D) do
functor(TypeArg,T,_),
- (occurs(T,(bool,int,uint,sort,rnd)) ->
+ (occurs(T,(bool,int,uint,sort,rnd,array)) ->
unfold_int_expr(Arg,D,AC,TypeArg,AR),
SetType = int_vars(TypeArg,AR)
; unfold_real_expr(Arg,D,AC,TypeArg,AR),
@@ -9975,14 +10103,21 @@ same_sign_div_mod(A,B) :-
%% Pas vraiment un undef pour B = 0 et bvudiv/bvurem
-%% Nouvell semantique: Q tout a 1 et R a 0
+%% Nouvelle semantique: Q tout a 1 et R a 0
chk_undef_div_rem(Bool,Type,A,B,Q,R,UO) :-
% // et rem pour int,intN et uintN
check_overflow(UO),
- (nonvar(Bool) ->
- (Bool == 0 ->
+ ((nonvar(Bool);
+ nonvar(B))
+ ->
+ ((Bool == 0;
+ B \== 0)
+ ->
+ protected_unify(Bool,0),
div_mod(Type,A,B,Q,R,UO)
- ; protected_unify(B,0),
+ ; % Bool == 1 et/ou B == 0
+ protected_unify(Bool,1),
+ protected_unify(B,0),
set_int_type(Type,A),
set_int_type(Type,Q),
set_int_type(Type,R),
@@ -10005,39 +10140,14 @@ chk_undef_div_rem(Bool,Type,A,B,Q,R,UO) :-
undef_div_rem(int,A,Q,R,UO) :- !,
uninterp_trigger(div_rem_int,[int],int,Trigger),
uninterp(div_rem_int,Trigger,[A],(Q,R)).
-/*
-undef_div_rem(int,A,Q,R,UO) :- !,
- get_priority(Prio),
- set_priority(1),
- (ground(A) ->
- (check_seen_expr(undef_div_rem(A),(QQ,RR,UUO),Type) ->
- protected_unify(Q,QQ),
- protected_unify(R,RR),
- protected_unify(UO,UUO)
- ; add_seen_expr(undef_div_rem(A),(Q,R,UO),Type))
- ; save_cstr_suspensions(A),
- get_saved_cstr_suspensions(LSusp),
- ((member((Susp,undef_div_rem(Type,AA,QQ,RR,UUO)),LSusp),
- AA == A)
- ->
- protected_unify(Q,QQ),
- protected_unify(R,RR),
- protected_unify(UO,UUO)
- ; my_suspend(undef_div_rem(Type,A,Q,R,UO),0,
- A->suspend:constrained))),
- set_priority(Prio),
- wake_if_other_scheduled(Prio).
-*/
undef_div_rem(Type,A,Q,R,UO) :-
- % int(N) et uint(N)
+ % uint(N)
+ % Q = 0
arg(1,Type,N),
All1 is 2^N-1,
- protected_unify(R,A),
- protected_unify(UO,0),
- (Type = uint(N) ->
- protected_unify(Q,All1)
- ; Type = int(N),
- uintN_to_intN(N,All1,Q,_)).
+ %protected_unify(UO,0),
+ protected_unify(Q,All1),
+ protected_unify(R,A).
diff --git a/Src/COLIBRI/util.pl b/Src/COLIBRI/util.pl
index ae356bdcb012d2d69b31806baee24c1da12c72c9..b64f05c540b788f202114476694b39c67a1a7271 100755
--- a/Src/COLIBRI/util.pl
+++ b/Src/COLIBRI/util.pl
@@ -246,6 +246,16 @@ protected_unify(X,Y) :-
protected_unify(X = Y) ?-
protected_unify(X,Y).
+:- export protected_occurs_in_list/2.
+protected_occurs_in_list(X,L) :-
+ (var(X);atomic(X)),
+ nonvar(L),
+ L = [_|_],
+ once (number(X) ->
+ member(XX,L),
+ XX == X
+ ; occurs(X,L)).
+
%%:- mode unify_vars(+).
unify_vars([A|L]) :-
unify_vars(A,L).