diff --git a/Src/COLIBRI/col_solve.pl b/Src/COLIBRI/col_solve.pl
index edb8d1ab39c7e6700661754c58280a5bc1e12abf..838ef4b2633cb05b07d2e6ec87cab267b1d487b7 100644
--- a/Src/COLIBRI/col_solve.pl
+++ b/Src/COLIBRI/col_solve.pl
@@ -1,4 +1,5 @@
:- pragma(nowarnings).
+
%% Rend le compilateur silencieux
:- set_event_handler(139,true/0).
@@ -73,6 +74,7 @@ set_timeout(T) :-
; writeln(output,"Expecting timeout integer value > 0."),
exit_block(syntax)).
+/* obsolete
get_version(Num) :-
system("svn info --show-item revision > revision"),
open(revision,read,Stream),
@@ -80,13 +82,15 @@ get_version(Num) :-
close(Stream),
system("rm revision"),
split_string(Str,":"," ",[_,Num]).
+
+:- dynamic colibri_version/1.
set_version :-
get_version(Num),
assert(colibri_version(Num)).
show_version :-
colibri_version(Num),
writeln(output,Num).
-
+*/
@@ -477,6 +481,9 @@ smt_solve_count_steps(FILE,TO) :-
setval(use_simplex,US)@eclipse.
*/
+% Pas de scrambler par défaut
+:- setval(scrambler,0).
+
smt_comp_solve(FILE) :-
% pas de message sur error pour la smtcomp
get_stream(null,Snull),
@@ -493,9 +500,8 @@ smt_comp_solve(FILE) :-
exit(Code).
smt_solve(FILE) :-
- % Pas de désactivation du simples apres DDSteps
+ % Désactivation du simplex apres DDSteps
% (5000 par défaut dans colibri.pl)
- % DDSteps = 0,
% setval(simplex_delay_deactivation,DDSteps)@eclipse,
% On passe en mode comptage du nombre de steps
@@ -508,7 +514,10 @@ smt_solve(FILE) :-
setval(simplex_steps,0)@eclipse,
% on active les warning de dolmen
setval(no_dolmen_warning,0)@eclipse,
- smt_solve(_,FILE,0,Code),
+ (getval(scrambler,1) ->
+ Test = 1
+ ; true),
+ smt_solve(Test,FILE,0,Code),
exit(Code).
smt_solve_get_stat(FILE) :-
@@ -520,7 +529,10 @@ smt_solve_get_stat(FILE) :-
; setval(step_limit,0)@eclipse),
setval(nb_steps,0)@eclipse,
setval(simplex_steps,0)@eclipse,
- smt_solve(_,FILE,0,Code),
+ (getval(scrambler,1) ->
+ Test = 1
+ ; true),
+ smt_solve(Test,FILE,0,Code),
getval(nb_steps,Steps)@eclipse,
writeln(output,"Steps":Steps),
exit(Code).
@@ -532,6 +544,27 @@ smt_solve(Test,FILE,TO,Code) :-
smt_solve_bis(Test,FILE,TO,Code) :-
+ getval(def_real_for_int,RI)@colibri,
+ not not (smt_solve_bis0(Test,FILE,TO,Code0),
+ setval(init_code,Code0)),
+ getval(init_code,Code0),
+ ((nonvar(Test),
+ Code0 == 0, % unsat
+ getval(real_for_int,1)@eclipse,
+ getval(int_used,1)@eclipse)
+ ->
+ write(output,"CONFIRM UNSAT:"),
+ % on confirme le unsat sans simulation
+ setval(def_real_for_int,0)@colibri,
+ smt_solve_bis0(_,'check.smt2',TO,Code1),
+ setval(def_real_for_int,RI)@colibri,
+ (Code0 == Code1 ->
+ Code = Code0
+ ; writeln(output,unknown),
+ Code = 2)
+ ; Code = Code0).
+
+smt_solve_bis0(Test,FILE,TO,Code) :-
% seed(0),
setval(smt_status,unknown)@eclipse,
setval(nb_steps,0)@eclipse,
@@ -696,7 +729,7 @@ smt_solve_test(FILE,TO) :-
seed(0),
smt_solve_test_bis(FILE,TO,Code),
exit(Code).
-
+
smt_solve_test_bis(FILE,TO,Code) :-
set_threshold(1e-3),
setval(cpt_solve,0)@colibri,
@@ -726,12 +759,20 @@ smt_solve_test_bis(FILE,TO,Code) :-
% pour tester l'installation colibri
smt_test :-
StrDir = "./Examples/QF_FP/schanda/spark/",
- smt_test0(5,1000,StrDir).
+ smt_test0(5,1000,StrDir,0).
+% pas de CI
smt_test(TO,Size) :-
+ smt_test(TO,Size,0).
+
+smt_test_CI(TO,Size) :-
+ smt_test(TO,Size,1).
+
+smt_test(TO,Size,CI) :-
%StrDir = "./colibri_tests/colibri/tests/",
- StrDir = "./colibri_tests/colibri/tests/sat/", %0 (sans real/float-> int!)
- %StrDir = "./colibri_tests/colibri/tests/unsat/", %0
+ %StrDir = "./colibri_tests/colibri/tests/sat/", %0 (sans real/float->int!) des TOs sur
+ % newton en CI à 15s mais pas à 20s
+ StrDir = "./colibri_tests/colibri/tests/unsat/", %0
%StrDir = "./colibri_tests/colibri/tests/unknown/",
%StrDir = "./colibri_tests/colibri/tests/timeout/",
@@ -838,7 +879,8 @@ 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/", % 105 (177 unsupported) (cvc4 55)
+
+ %StrDir = "./QF_ABVFP/20170428-Liew-KLEE/", % 106 (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)!
@@ -848,7 +890,8 @@ 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/", % 16 (cvc4 50)(bitwuzla
+
+ %StrDir = "./QF_BVFP/20170428-Liew-KLEE/", % 21 (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)
@@ -857,7 +900,7 @@ smt_test(TO,Size) :-
% (bitwuzla 1) (le passage en int casse les deltas)
%----------------------------------------------------------------
%StrDir = "./QF_BVFPLRA/20170501-Heizmann-UltimateAutomizer/", % 0 (cvc4 0)
- %StrDir = "./QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/", % 9 + 11u (cvc4 17 + 11u sinon 0u avec --fp-exp?))
+ %StrDir = "./QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/", % 8 + 11u (cvc4 17 + 11u sinon 0u avec --fp-exp?))
%StrDir = "./QF_BVFPLRA/2019-Gudemann/", % 0 (cvc4 1)
%----------------------------------------------------------------
%StrDir = "./QF_FPLRA/20170501-Heizmann-UltimateAutomizer/", % 0 (cvc4 0)
@@ -868,7 +911,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/griggio/", % 49 (min_solve, sans lin_solve ni ls_reduce..)(39)
+ %StrDir = "./QF_FP/griggio/", % 54 (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/wintersteiger/", % tout OK
@@ -927,19 +970,12 @@ smt_test(TO,Size) :-
%StrDir = "QF_ABV/bmc-arrays/",
%StrDir = "QF_AFPBV/dwp_formulas/", %TRES DUR
- smt_test0(TO,Size,StrDir).
+ smt_test0(TO,Size,StrDir,CI).
:- lib(timeout).
-
-read_file_list(SmtFileList) :-
- (at_eof(tataS) ->
- close(tataS),
- SmtFileList = []
- ; SmtFileList = [F| NSmtFileList],
- read_string(tataS,end_of_line,_,F),
- read_file_list(NSmtFileList)).
-
-smt_test0(TO,Size,StrDir) :-
+:- setval(nbTryCI,2).
+
+smt_test0(TO,Size,StrDir,CI) :-
setval(bug,[]),
setval(cpt_solve,0)@colibri,
@@ -976,13 +1012,26 @@ smt_test0(TO,Size,StrDir) :-
->
Windows = 1
; true),
-/*
- open(tata,read,tataS),
- read_file_list(SmtFileList),
-*/
- length(SmtFileList,NbFiles),
+ length(SmtFileList,NbFiles0),
+ getval(use_delta,UD)@eclipse,
+ (UD == 1 ->
+ UDS = "use_delta,"
+ ; UDS = "no_delta,"),
+ getval(use_simplex,US)@eclipse,
+ (US == 1 ->
+ USS = "use_simplex,"
+ ; USS = "no_simplex,"),
+ % Nombre de tentatives en CI
+ getval(nbTryCI,NbTryCI),
+ (CI == 0 ->
+ NbFiles = NbFiles0,
+ NbTry = 1
+ ; NbFiles is NbFiles0*NbTryCI,
+ NbTry = NbTryCI),
setval(nbTO,0),
( member(F,SmtFileList),
+ setval(nb_try,NbTry),
+ repeatN,
incval(nbFile),
getval(nbFile,NumF),
getval(nbTO,NbTO),
@@ -992,7 +1041,9 @@ 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," -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)),
+ ; (CI == 0 ->
+ 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),",UDS,USS,"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,use_simplex,setval(def_real_for_int,1)@colibri,setval(step_limit,0),setval(no_dolmen_warning,1)@eclipse,setval(show_steps,1),",UDS,USS,"setval(scrambler,1)@eclipse,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)),
@@ -1060,8 +1111,26 @@ smt_test0(TO,Size,StrDir) :-
(foreach(B,Bugs) do
writeln(output,B))).
+repeatN :-
+ repeat,
+ getval(nb_try,Nb),
+ (Nb > 0 ->
+ decval(nb_try)
+ ; !,
+ fail).
+
smt_unit_test(TO) :-
+ smt_unit_test(TO,0).
+smt_unit_test_CI(TO) :-
+ smt_unit_test(TO,1).
+
+smt_unit_test(TO,CI) :-
setval(bug,[]),
+ StrDir = "./colibri_tests/colibri/tests/sat/", %0 (sans real/float->
+ % int!) des TOs sur
+ % newton en CI
+ %StrDir = "./colibri_tests/colibri/tests/unsat/", %0
+
%StrDir = "./QF_BVFP/20170428-Liew-KLEE/imperial_svcomp_float-benchs_svcomp_mea8000.x86_64/",
%StrDir = "./smtlib_schanda-master/random/", % tout OK ou unsupported
%StrDir = "./smtlib_schanda-master/random/fp.from.real/",
@@ -1105,7 +1174,7 @@ smt_unit_test(TO) :-
%StrDir = "./QF_FP/ramalho/",% 6-2 T0
%StrDir = "./QF_FP/griggio/", % 59 TO en 24s, 51 en 60s (cvc4 90 en 60s)
%StrDir = "./QF_FP/schanda/spark/",% 7 TO
- StrDir = "./QF_FP/wintersteiger/", % 0 TO
+ %StrDir = "./QF_FP/wintersteiger/", % 0 TO
%------------------------------------------------------------------------
%StrDir = "QF_AX/",
%StrDir = "QF_AX/storeinv/",
@@ -1199,8 +1268,17 @@ smt_unit_test(TO) :-
setval(no_dolmen_warning,1)@eclipse,
getval(use_delta,UD)@eclipse,
getval(use_simplex,US)@eclipse,
- length(SmtFileList,NFs),
+ length(SmtFileList,NFs0),
+ getval(nbTryCI,NbTryCI),
+ (CI == 1 ->
+ NFs is NFs0 * NbTryCI,
+ NbTry = NbTryCI,
+ Test = 1
+ ; NFs = NFs0,
+ NbTry = 1),
( member(F,SmtFileList),
+ setval(nb_try,NbTry),
+ repeatN,
incval(nbFile),
getval(nbFile,NbF),
getval(nbTO,NbTO),
@@ -1209,7 +1287,10 @@ smt_unit_test(TO) :-
setval(cpt_solve,0)@colibri,
setval(use_delta,UD)@eclipse,
setval(use_simplex,US)@eclipse,
- smt_solve_bis(1,F,TO,Code),
+ not not (seed(0),
+ smt_solve_bis(Test,F,TO,Code),
+ setval(init_code,Code)),
+ getval(init_code,Code),
incNbCode(Code),
(Code == 2 ->
getval(bug,Bugs),
@@ -1266,7 +1347,9 @@ smt_unit_test1 :-
( member(F,SmtFileList),
incval(nbFile),
writeln(output,F),
- smt_solve_test_bis(F,1,Code),
+ not not (smt_solve_test_bis(F,1,Code),
+ setval(init_code,Code)),
+ getval(init_code,Code),
incNbCode(Code),
(Code == 2 ->
getval(bug,Bugs),
diff --git a/Src/COLIBRI/colibri.pl b/Src/COLIBRI/colibri.pl
index 4bd9c1424f65530fc0f1865b5774a15557eb0d97..f54b06899590095e73d47ff7530981eeefca4127 100755
--- a/Src/COLIBRI/colibri.pl
+++ b/Src/COLIBRI/colibri.pl
@@ -1,5 +1,5 @@
-% pour le debug
:- pragma(nowarnings).
+% pour le debug
%:- pragma(debug).
% pour le debug des handlers
?- unlock(sepia_kernel,"Sepia").
@@ -275,9 +275,7 @@ init_colibri :-
dump_constraints,
smt_import,
simplex_ocaml,
-% test_mbv,
mbv_propa]).
-% zutils]). % TODO remove test_mbv
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
diff --git a/Src/COLIBRI/mbv.pl b/Src/COLIBRI/mbv.pl
index 2f3a7d90c1484f82c4bb6c2b12c5e4dcef8be972..32a70dfdf0cf7c90f45b1da64cd53014b465061b 100644
--- a/Src/COLIBRI/mbv.pl
+++ b/Src/COLIBRI/mbv.pl
@@ -24,11 +24,7 @@
:- export
and_dir_prop/3,
- singleton_bvdom/2,
- propagate_all/3,
- checkit/1,
- mk_prop_tree/3,
- prop_in_eq/1.
+ and_inv_prop/3.
:- export use_prod_bv_congr/0,
@@ -551,27 +547,6 @@ get_22_bis([B|L], T1, T0, ToOne, ToZero) :-
%Gets the number of specified positions from the lowest if possible
%plus the highest one.
-:- export get_n_positions/3.
-% Old version of June 3rd
-get_n_positions(N, Positions, Result):-
- get_lold(Positions, 1, Index), % There is at least one. Unknown != 0
- P is Positions /\ (\ Index),
- NN is N - 1,
- I is Index << 1,
- get_n_posbis(NN, P, I, [Index], Result).
-get_n_posbis(_, 0, _, Res, Res) :- !.
-get_n_posbis(N, P, I, T, [H|T]) :-
- N =< 0, !, % P is not 0 and all before Index are 0
- get_gold(P, I, H).
-get_n_posbis(N, P, I, T, R):-
- N > 0,
- get_lold(P, I, Index), % There is at least one. Position != 0
- PP is P /\ (\ Index),
- NN is N - 1,
- II is Index << 1,
- get_n_posbis(NN, PP, II, [Index|T], R).
-
-
:- export get_n_positions/5.
% TODO notice: can give back NEW LU and GU, and avoid Fill (do replace directly)
/*
@@ -624,42 +599,6 @@ simple_resol_bv(X) :-
)
; print("IMPOSSIBLE, labeling a var with no BVDOM attr"), nl, nl, fail).
-% Add : first value to pick: that of 0, to remove some multiplication and stuff.
-% CURRENT VERSION may decide twice on that value. Find ways to make it better
-% Version June 3rd.
-%% simple_resol_bv(X) :-
-%% get_bvbounds(X, bvbounds(X1, X0)),
-%% ((X1 == 0, % We don't know that there is a 1
-%% protected_unify(X = 0))
-%% ;
-%% (Unknown is xor(X1, X0),
-%% get_n_positions(3, Unknown, L),
-%% get_2one_2zero(L, T1, T0),
-%% XX1 is X1 \/ T1,
-%% XX0 is X0 /\ T0,
-%% fill_bvbounds(X, bvbounds(XX1, XX0)))
-%% ).
-
-% La meme maissans essayer zero d'abord
-%% simple_resol_bv(X) :-
-%% get_bvbounds(X, bvbounds(X1, X0)),
-%% Unknown is xor(X1, X0),
-%% get_n_positions(3, Unknown, L),
-%% get_2one_2zero(L, T1, T0),
-%% XX1 is X1 \/ T1,
-%% XX0 is X0 /\ T0,
-%% fill_bvbounds(X, bvbounds(XX1, XX0)).
-
-% Lancienne, celle qui fixe tout d'un coup
-%% simple_resol_bv(X) :-
-%% get_bvbounds(X, bvbounds(X1, X0)),
-%% Unsett is (xor(X1,X0)),
-%% numbits(Unsett, SSize),
-%% Size is SSize + 1,
-%% Mask is (-1 << Size),
-%% Unset is ((\ Mask) /\ Unsett),
-%% label_aux(Unset,Size,Result),
-%% X is (X0 /\ X1) \/ Result.
get_lold(Unknown, L, LU):-
(L /\ Unknown =:= 0 ->
@@ -674,24 +613,6 @@ get_gold(Unknown, G, GU) :-
; GG is G << 1,
get_gold(Unknown, GG, GU))).
-
-%For backward compatibility
-:- export simple_resol_bv_old/1.
-simple_resol_bv_old(X) :-
- get_bvbounds(X, bvbounds(X1, X0)),
- Unsett is (xor(X1,X0)),
- numbits(Unsett, SSize),
- Size is SSize + 1,
- Mask is (-1 << Size),
- Unset is ((\ Mask) /\ Unsett),
- label_aux(Unset,Size,Result),
- X is (X0 /\ X1) \/ Result.
-:- export labeling_bv/1.
-labeling_bv([]).
-labeling_bv([X|L]) :-
- simple_resol_bv_old(X),
- labeling_bv(L).
-
%----------------------------------------------------------------
% BV Propagation on domains
%----------------------------------------------------------------
@@ -753,8 +674,6 @@ shiftedR_ones(Size, Offset, ShOnes) :-
ShOnes is (-1 << Move) /\ \ ( - 1 << Size).
% x & y = z
-:- export and_dir_prop/3, and_inv_prop/3.
-
and_dir_prop(bvbounds(X1, X0),
bvbounds(Y1, Y0),
bvbounds(Z1, Z0)) :-
@@ -1207,663 +1126,3 @@ dom_from_string(S, bvbounds(X1, X0)) :-
charify(Lcodes, L),
tokenize(L, LL),
dom_from_list(LL, X1, X0).
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-%----------------------------------------------------------------
-%----------------------------------------------------------------
-%----------------------------------------------------------------
-%----------------------------------------------------------------
-% Graveyard
-%----------------------------------------------------------------
-%----------------------------------------------------------------
-%----------------------------------------------------------------
-%----------------------------------------------------------------
-
-
-%% :- export has_bvdom/2.
-%% has_bvdom(V,1):-
-%% get_attr_bv(V,_),
-%% !.
-%% has_bvdom(V,_).
-
-
-
-% :- export update_arith_bv_var/1.
-%% update_arith_bv_var(V) :-
-%% %is_arith_var(V),
-%% get_bvbounds(V,Dom),
-%% !,
-%% update_congruence_from_bv(V, Dom),
-%% update_intervals_from_mbv(V, Dom).
-%update_arith_bv_var(V).
-
-%% :- export update_congruence_from_bv/2.
-%% update_congruence_from_bv(X, DX) :-
-%% % OBSOLETE!!!!
-%% mk_congr(DX, C, Mod),
-%% launch_congr(X, C, Mod).
-
-
-
-%% fill_bvbounds(X, Bounds) :-
-%% (get_attr_bv(X, bvdom(X1, X0, XLU, XGU)) ->
-%% meet_bvbounds(Bounds, bvbounds(X1, X0), Meet),
-%% (bvbounds(X1, X0) == Meet ->
-%% true
-%% ; (singleton_bvbounds(Meet, M) ->
-%% protected_unify(X = M)
-%% ; valid_bvbounds(Meet),
-%% %Meet = bvbounds(M1, M0),
-
-%% fill_bvbounds(X, Bounds) :-
-%% (get_attr_bv(X, bvdom(X1, X0, XLU, XGU)) ->
-%% meet_bvbounds(Bounds, bvbounds(X1, X0), Meet),
-%% (bvbounds(X1, X0) == Meet ->
-%% true
-%% ; (singleton_bvbounds(Meet, M) ->
-%% protected_unify(X = M)
-%% ; valid_bvbounds(Meet),
-%% %Meet = bvbounds(M1, M0),
-
-%% Meet = bvbounds(M1, MM0),
-%% % Essayons le Int vers BV
-%% mfd:dvar_range(X, Min, Max),
-%% (MM0 > Max ->
-%% numbits(Max, NBits),
-%% M0 is MM0 /\ \ ( - 1 << NBits)
-%% ; M0 = MM0 ),
-%% %%
-
-%% get_least_and_greatest_unknown(M1, M0, XLU, XGU, MLU, MGU),
-%% replace_attribute(X, bvdom(M1, M0, MLU, MGU), mbv),
-%% %update_arith_bv_var(X),
-%% (XLU \== MLU ->
-%% %update_congruence_from_bv(X, Meet)
-%% Rest is (MLU - 1) /\ M1,
-%% launch_congr(X, Rest, MLU)
-%% ; true),
-%% update_intervals_from_mbv(X, Meet),
-%% (XGU \== MGU ->
-%% LHS is M0 /\ (\ MGU),
-%% UHS is M1 \/ MGU,
-%% Worthit is (UHS - LHS),
-%% ( Worthit > 1 ->
-
-
-%% mfd:get_intervals(X, Intervals), !,
-%% drill_heavy(Intervals, LHS, UHS, NInter),!,
-%% mfd:set_intervals(X, NInter), !
-%% ; true)
-%% ; true),
-
- %% notify_constrained(X))
- %% )
- %% ; print("IMPOSSIBLE, Filling a var with no BVDOM attr"), nl, nl, fail).
-
-
-
-
-
-
-
-
- %% meet_bvbounds(bvbounds(X1, X0), bvbounds(Y1, Y0), bvbounds(M1, MM0)),
- %% mfd:dvar_range(X, Min, Max),
- %% (MM0 > Max ->
- %% numbits(Max, NBits),
- %% M0 is MM0 /\ \ ( (- 1) << NBits)
- %% ; M0 = MM0 ),
- %% Meet = bvbounds(M1, M0),
- %% (singleton_bvbounds(Meet, M) ->
- %% protected_unify(X = M)
- %% ; valid_bvbounds(Meet),
- %% (bvbounds(X1, X0) \== Meet ->
- %% get_least_and_greatest_unknown(M1, M0, CurrentLU, CurrentGU, MLU, MGU),
- %% replace_attribute(X, bvdom(M1, M0, MLU, MGU), mbv),
- %% (XLU \== MLU ->
- %% Rest is (MLU - 1) /\ M1,
- %% launch_congr(X, Rest, MLU)
- %% ; true),
- %% update_intervals_from_mbv(X, Meet),
- %% (XGU \== MGU ->
- %% LHS is M0 /\ (\ MGU),
- %% UHS is M1 \/ MGU,
- %% Worthit is (UHS - LHS),
- %% ( Worthit > 1 ->
- %% mfd:get_intervals(X, Intervals), !,
- %% drill_heavy(Intervals, LHS, UHS, NInter),!,
- %% mfd:set_intervals(X, NInter), !
- %% ; true)
- %% ; true),
- %% notify_constrained(X)
- %% ; true)
- %% ).
-
-% Old version (11 Aout) Got wrong sat because guard in get-least-and-greatest was
-% down. And an Unknown was NULL.
-%% unify_dom_dom(X, AttrX, AttrY) :-
-%% nonvar(AttrX),
-%% AttrX = bvdom(X1, X0, XLU, XGU),
-%% AttrY = bvdom(Y1, Y0, _, _),
-%% meet_bvbounds(bvbounds(X1, X0), bvbounds(Y1, Y0), Meet),
-%% (singleton_bvbounds(Meet, M) ->
-%% protected_unify(X = M)
-%% ; valid_bvbounds(Meet),
-%% (bvbounds(X1, X0) \== Meet ->
-%% %Meet = bvbounds(M1, M0),
-%% Meet = bvbounds(M1, MM0),
-%% % Essayons le Int vers BV
-%% mfd:dvar_range(X, Min, Max),
-%% (MM0 > Max ->
-%% numbits(Max, NBits),
-%% M0 is MM0 /\ \ ( (- 1) << NBits)
-%% ; M0 = MM0 ),
-%% %%
-%% get_least_and_greatest_unknown(M1, M0, XLU, XGU, MLU, MGU),
-%% replace_attribute(X, bvdom(M1, M0, MLU, MGU), mbv),
-%% %update_arith_bv_var(X),
-%% (XLU \== MLU ->
-%% %update_congruence_from_bv(X, Meet)
-%% Rest is (MLU - 1) /\ M1,
-%% launch_congr(X, Rest, MLU)
-%% ; true),
-%% update_intervals_from_mbv(X, Meet),
-%% (XGU \== MGU ->
-%% LHS is M0 /\ (\ MGU),
-%% UHS is M1 \/ MGU,
-%% Worthit is (UHS - LHS),
-%% ( Worthit > 1 ->
-%% mfd:get_intervals(X, Intervals), !,
-%% drill_heavy(Intervals, LHS, UHS, NInter),!,
-%% mfd:set_intervals(X, NInter), !
-%% ; true)
-%% ; true),
-%% notify_constrained(X)
-%% ; true)
-%% ).
-
-
-
-
-
-%----------------------------------------------------------------
-% Propagation in whole constraints: Utilities (TODO : remove this)
-%----------------------------------------------------------------
-:- export label_bv/2.
-label_bv(bvdom( X1, X0), V) :- %TODO : try to make it better
- valid_bvdom(bvdom( X1, X0)),
- Unsett is (xor(X1,X0)),
- numbits(Unsett, SSize),
- Size is SSize + 1,
- Mask is (-1 << Size),
- Unset is ((\ Mask) /\ Unsett),
- label_aux(Unset,Size,Result),
- V is (X0 /\ X1) \/ Result.
-
-label_aux(Done, Negative, Done) :- Negative < 0,!.
-label_aux(In, Idx, Out) :-
- Idx >= 0,!,
- NIdx is Idx - 1,
- (is_setbit(In, Idx) -> (NIn is clrbit(In, Idx) ; NIn = In)
- ;
- NIn = In),
- label_aux(NIn, NIdx, Out).
-
-:- export label_all/2.
-label_all(X, AllSol) :-
- setof(X, labeling_bv([X]), AllSol).
-
-
-
-:- export leq_constr/4.
-leq_constr(DX, DY,NDX, NDY):-
- get_stops_and_sets(DX, DY, Stop, Con, SetY, ClearX),
- (Stop < 0 -> NDX = DX, NDY = DY %Stop at infinity
- ;
- Con >= 0, % If negative, means infinity of 1, means bad
- Stop >= Con, % Must be able to stop before reaching conflict
- numbits(Stop, SStop),
- ((SStop > 0, true) -> % If it's 0, no need to mask, apply to all
- (M is (-1 << (SStop )),
- Set is M /\ SetY, Clear is M /\ ClearX,
- set_bits_dom(DY, Set, NDY),
- clr_bits_dom(DX, Clear, NDX))
- ; true
- /* (set_bits_dom(DY, SetY, NDY),
- clr_bits_dom(DX, ClearX, NDX)) */
- )).
-:- export add_constr/6.
-add_constr(DX, DY, DZ, NDX, NDY, NDZ) :-
- join_bvdom(DX, DY, E),
- shiftL_norm(E, 1, C),
- iter_add(DX, DY, DZ, C, NDX, NDY, NDZ).
-/*
-iter_add(DX, DY, DZ, C, IDX, IDY, IDZ) :-
- % What the current position carry should be
- xor_prop(DX, DY, C, ZZ),
- xor_prop(DY, DZ, C, XX),
- xor_prop(DZ, DX, C, YY),
- xor_prop(DX, DY, DZ, CC),
- meet_bvdom(DX, XX, NX),
- meet_bvdom(DY, YY, NY),
- meet_bvdom(DZ, ZZ, NZ),
- meet_bvdom(C, CC, IC),
-
- % What the next Carry says about the current position
- shiftR_norm(IC, 1, NextCarry),
- and_dir_prop(NX, NY, C1),
- and_dir_prop(NX, IC, C2),
- and_dir_prop(NY, IC, C3),
- or_dir_prop(C1, C2, C4),
- or_dir_prop(C3,C4, CNC),
- meet_bvdom(CNC, NextCarry),
-*/
-
-/*
-DEPRECATED, should be anyway. Trying the calling of prop_all in add...
-*/
-iter_add(DX, DY, DZ, C, IDX, IDY, IDZ) :-
- xor_prop(DX, DY, C, ZZ),
- xor_prop(DY, DZ, C, XX),
- xor_prop(DZ, DX, C, YY),
- xor_prop(DX, DY, DZ, CC),
- meet_bvdom(DX, XX, NX),
- %(valid_bvdom(NX) -> true; print_doms("X",[DX, XX])),
- meet_bvdom(DY, YY, NY),
- %(valid_bvdom(NY) -> true; print_doms("Y",[DY, YY])),
- meet_bvdom(DZ, ZZ, NZ),
- %(valid_bvdom(NZ) -> true; print_doms("Z",[DZ, ZZ])),
- meet_bvdom(C, CC, CCa),
- %(valid_bvdom(CCa) -> true; print_doms("C",[C, CC])),
- carry_up(NX, NY, CCa, NC),
- (valid_bvdom(NC) -> true; print_doms("NC",[NC, CCa, NX, NY, NZ]) ),
- (equal_bvdom(DX, DY, DZ, C, NX, NY, NZ, NC) ->
- protected_unify(DX = IDX),
- protected_unify(DY = IDY),
- protected_unify(DZ = IDZ)
- ; iter_add(NX, NY, NZ, NC, IDX, IDY, IDZ)).
-carry_up(A,B,C,CC) :-
- and_dir_prop(A,B,E1),
- and_dir_prop(A,C,E2),
- and_dir_prop(B,C,E3),
- or_dir_prop(E1, E2, E4),
- or_dir_prop(E3,E4,E),
- shiftR_norm(C, 1, CM), meet_bvdom(CM, E, CE),
- shiftL_norm(CE, 1, EE),
- %shiftL_norm(E, 1, EE),
- %or_dir_prop(EE, C, CC).
- meet_bvdom(EE, C, CC), valid_bvdom(CC).
-
-
-print_doms(S,L) :- nl, print(S), print("==>"), nl, print_doms(L).
-print_doms([]).
-print_doms([D|L]) :-
- add_attribute(X,D), print(X), nl, print_doms(L).
-
-
-
-
-
-
-
-
-
-
-
-
-
-/*
-[propagate_all].
-1st param: domains to be tested against new domains for termination
-2nd the variables involved (to be able to get their domain at each run
-3rd the constraints to go through and propagate into).
-*/
-
-propagate_all(_, Vars, Constraints) :-
- propagate(Constraints),
- are_we_done(Vars, Constraints).
-
-:- export propagate_all/1.
-propagate_all(Constraints) :-
- propagate(Constraints),
- term_variables(Constraints, Vars),
- labeling_bv(Vars),
- checkit(Constraints)
- %print(Vars)
- %are_we_done(Constraints)
-.
-are_we_done([]).
-are_we_done([C|Constraints]) :-
- term_variables(C, Vars), print(Vars),
- (labeling_bv(Vars) ->
- (call(C) -> are_we_done(Constraints)
- ; writeln("FAILED ON::"), print(C), nl, nl, fail)
- ; writeln("NOT LABELLED 2 => "), print(Vars), fail).
-
-:- export propagate/1.
-propagate([]).
-propagate([X|ConstraintL]):-
- prop_in_eq(X),
- propagate(ConstraintL).
-
-are_we_done(Vars, Constraints) :-
- (labeling_bv(Vars) -> checkit(Constraints)
- ; writeln("NOT LABELLED")).
-
-checkit([]).
-checkit([C|L]) :-
- (call(C), checkit(L)).
-% ; writeln("FAILED ON::"), print(C), nl, nl).
-
-get_domains([],[]).
-get_domains([V|VL], [D|DL]) :-
- get_bvdom(V, D),
- get_domains(VL,DL).
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-%----------------------------------------------------------------
-% Propagation in whole constraints: Using trees (TODO : remove)
-%----------------------------------------------------------------
-
-mk_prop_tree(L << R, Tree, Vars) :-
- -?-> !,
- mk_prop_tree(L, [DL|RestL], VarsL),
- mk_prop_tree(R, [DR|RestR], VarsR),
- (singleton_bvdom(DR, RisCnst) ->
- shiftL_norm(DL, RisCnst, D)
- ; new_bvdom(D)),
- Tree = [D, [DL|RestL], [DR|RestR]],
- append(VarsL, VarsR, Vars).
-
-mk_prop_tree(L >> R, Tree, Vars) :-
- -?-> !,
- mk_prop_tree(L, [DL|RestL], VarsL),
- mk_prop_tree(R, [DR|RestR], VarsR),
- (singleton_bvdom(DR, RisCnst) ->
- shiftR_norm(DL, RisCnst, D)
- ; new_bvdom(D)),
- Tree = [D, [DL|RestL], [DR|RestR]],
- append(VarsL, VarsR, Vars).
-
-mk_prop_tree(L /\ R, Tree, Vars) :-
- -?-> !,
- Tree = [D, [DL|RestL], [DR|RestR]],
- mk_prop_tree(L, [DL|RestL], VarsL),
- mk_prop_tree(R, [DR|RestR], VarsR),
- and_dir_prop(DL, DR, D),
- append(VarsL, VarsR, Vars).
-
-mk_prop_tree(L \/ R, Tree, Vars) :-
- -?-> !,
- Tree = [D, [DL|RestL], [DR|RestR]],
- mk_prop_tree(L, [DL|RestL], VarsL),
- mk_prop_tree(R, [DR|RestR], VarsR),
- or_dir_prop(DL, DR, D),
- append(VarsL, VarsR, Vars).
-
-mk_prop_tree(xor(L, R), Tree, Vars) :-
- -?-> !,
- Tree = [D, [DL|RestL], [DR|RestR]],
- mk_prop_tree(L, [DL|RestL], VarsL),
- mk_prop_tree(R, [DR|RestR], VarsR),
- xor_prop(DL, DR, D),
- append(VarsL, VarsR, Vars).
-
-mk_prop_tree(\ N, Tree, Vars) :-
- -?-> !,
- mk_prop_tree(N,[DN|Rest], Vars),
- negate_bvdom(DN, D),
- Tree = [D, [DN|Rest]].
-
-mk_prop_tree(C, Tree, Vars) :-
- -?-> !,
- (var(C) ->
- get_bvdom(C, DC),
- Tree = [DC],
- Vars = [C]
- ; (integer(C) ->
- Tree = [bvdom( C, C)],
- Vars = []
- ; fail)).
-
-prop_in_eq(Left =:= Right) :-
-!,
- mk_prop_tree(Left, [HL|LT], VarsL),
- mk_prop_tree(Right,[HR|RT], VarsR),
- prop_in_tree(Right, RT, HL),
- prop_in_tree(Left, LT, HR),
- append(VarsL, VarsR, Varss),
- term_variables(Varss, Vars),
- (Vars == [] -> true
- %(not (at_least_two(Vars)) -> true
- ; suspend(prop_in_eq(Left =:= Right), 0, (Vars -> suspend:constrained))).
-
-prop_in_eq(badd(X,Y,Z)) :-
- !,
- (integer(X), integer(Y) -> Zp is X + Y, protected_unify(Z = Zp)
- ;
- (integer(Y), integer(Z) -> Xp is Z - Y, protected_unify(X = Xp)
- ;
- (integer(X), integer(Z) -> Yp is Z - X, protected_unify(Y = Yp);
- get_bvdom(X, DX),
- get_bvdom(Y, DY),
- join_bvdom(DX, DY, DNC),
- shiftL_norm(DNC, 1, DC),
- add_attribute(C, DC),
- add_attribute(NC, DNC),
- bvadd_prop_bis(X,Y,Z,C,NC)))).
-
-bvadd_prop_bis(X,Y,Z,C,NC) :-
- (integer(X), integer(Y) -> Zp is X + Y, protected_unify(Z = Zp)
- ;
- (integer(Y), integer(Z) -> Xp is Z - Y, protected_unify(X = Xp)
- ;
- (integer(X), integer(Z) -> Yp is Z - X, protected_unify(Y = Yp);
- propagate([
- C =:= xor(xor(X,Y),Z),
- % Don't need all these!!
- %X =:= xor(xor(C,Y),Z),
- %Y =:= xor(xor(X,C),Z),
- %Z =:= xor(xor(X,Y),C),
- NC =:= (X /\ Y) \/ ((X /\ C) \/ (Y /\ C)),
- C =:= NC << 1
- ])
- %% term_variables([X,Y,Z],Vars),
- %% (Vars == [] -> true
- %% ; suspend(bvadd_prop_bis(X,Y,Z,C,NC) , 0, (Vars -> suspend:constrained)
- %% ))
-))).
-
-
-/*
-% Trying something else
-prop_in_eq(badd(X,Y,Z)) :-
- %% get_priority(Prio),
- %% set_priority(1),
- !,
- (integer(X), integer(Y) -> Zp is X + Y, protected_unify(Z = Zp)
- ;
- (integer(Y), integer(Z) -> Xp is Z - Y, protected_unify(X = Xp)
- ;
- (integer(X), integer(Z) -> Yp is Z - X, protected_unify(Y = Yp);
- get_bvdom(X, DX),
- get_bvdom(Y, DY),
- get_bvdom(Z, DZ),
- add_constr(DX, DY, DZ, NDX, NDY, NDZ),
- fill_bvdom(X,NDX),
- fill_bvdom(Y,NDY),
- fill_bvdom(Z,NDZ),
- term_variables([X,Y,Z],Vars),
- (not (at_least_two(Vars)) -> true
- ; suspend(prop_in_eq(badd(X,Y,Z)) , 0, (Vars -> suspend:constrained))))))%% ,
- %% set_priority(Prio),
- %% wake_if_other_scheduled(Prio)
-.
-*/
-badd(A,B,R) :- (A + B) =:= R.
-
-/*
-prop_in_tree(Expression, Tree of that expression, Outside)
-Once the tree of direct propagations is made, it is used for indirect
-propagations. The parameter [Outside] is used for this.
-*/
-
-prop_in_tree(C, _ , Outside) :-
- % Leaf
- (var(C);integer(C)), !,
- fill_bvdom(C, Outside).
-
-prop_in_tree(L /\ R, [[HL|LT], [HR|RT]], Outside) :-
- !,
- and_inv_prop(HL, Outside, OHL),
- and_inv_prop(HR, Outside, OHR),
- % We can test if it's empty, and stop
- (new_bvdom(OHL) -> true; prop_in_tree(R, RT, OHL)),
- (new_bvdom(OHR) -> true; prop_in_tree(L, LT, OHR)).
-
-prop_in_tree(L \/ R, [[HL|LT], [HR|RT]], Outside) :-
- !,
- or_inv_prop(HL, Outside, OHL),
- or_inv_prop(HR, Outside, OHR),
- (new_bvdom(OHL) -> true; prop_in_tree(R, RT, OHL)),
- (new_bvdom(OHR) -> true; prop_in_tree(L, LT, OHR)).
-
-prop_in_tree(xor(L, R), [[HL|LT], [HR|RT]], Outside) :-
- !,
- xor_prop(HL, Outside, OHL),
- xor_prop(HR, Outside, OHR),
- (new_bvdom(OHL) -> true; prop_in_tree(R, RT, OHL)),
- (new_bvdom(OHR) -> true; prop_in_tree(L, LT, OHR)).
-
-prop_in_tree(\ N, [[_|NT]], Outside) :-
- !,
- negate_bvdom(Outside, NOutside),
- (new_bvdom(NOutside) -> true
- ; prop_in_tree(N, NT, NOutside)).
-
-prop_in_tree(L << _ , [[_|LT], [HR|_]], Outside) :-
- !,
- (singleton_bvdom(HR, RisCnst) ->
- shiftR_unk(Outside, RisCnst, OHR),
- (new_bvdom(OHR) -> true
- ; prop_in_tree(L, LT, OHR))
- ; true).
-
-prop_in_tree(L >> _ , [[_|LT], [HR|_]], Outside) :-
- !,
- (singleton_bvdom(HR, RisCnst) ->
- shiftL_unk(Outside, RisCnst, OHR),
- (new_bvdom(OHR) -> true
- ; prop_in_tree(L, LT, OHR))
- ; true).
-
-
-
-
-%-----------------------------
-% Utils
-%-----------------------------
-
-:- export bvconcret/2.
-bvconcret(S, L) :-
- varof(X, S),
- label_all(X,L).
diff --git a/Src/COLIBRI/mbv_propa.pl b/Src/COLIBRI/mbv_propa.pl
index 52eaf4e65fe523c430419dc2ede7a7286f14c94d..86ae21bd8856c5bcd35c4a6494960aa534163a00 100644
--- a/Src/COLIBRI/mbv_propa.pl
+++ b/Src/COLIBRI/mbv_propa.pl
@@ -24,99 +24,6 @@ xorify(X, [Y|L],[R|RL]) :-
R is X xor Y,
xorify(X,L, RL).
-:- export orInter/4.
-
-orInter(A,B,C,D) :-
- dobee(or, A, B, C, D).
-xorInter(A,B,C,D) :-
- dobee(xor, A, B, C, D).
-andInter(A,B,C,D) :-
- dobee(and, A, B, C, D).
-dobee(OP, Amin, Amax, Bmin, Bmax) :-
- fromto(Amin,Amax,A),
- fromto(Bmin,Bmax,B),
- (
- OP == or, update_ui_or(A, B, C), !
- ;
- OP == xor, update_ui_xor(A, B, C)
- ),
- interval_range(C, Cmin, Cmax),
- M is max([Amin,Amax,Bmin,Bmax,Cmin, Cmax]),
- numbits(M, Size),
- to_bits(Amin, AminB, Size),
- to_bits(Bmin, BminB, Size),
- to_bits(Cmin, CminB, Size),
- to_bits(Amax, AmaxB, Size),
- to_bits(Bmax, BmaxB, Size),
- to_bits(Cmax, CmaxB, Size),
- printf(output, "[%s,%s]=[%d,%d]\n", [AminB,AmaxB,Amin,Amax]),
- printf(output, "[%s,%s]=[%d,%d]\n", [BminB,BmaxB,Bmin,Bmax]),
- printf(output, "[%s,%s]=[%d,%d]\n", [CminB,CmaxB,Cmin,Cmax]).
-
-/*
-Untru that min is the or of mins:
-orInter(3,6,4,9).
-[00011,00110]=[3,6]
-[00100,01001]=[4,9]
-[00100,01111]=[4,15]
-Mais c'est pas le max non plus
-orInter(3,3,4,9).
-[00011,00011]=[3,3]
-[00100,01001]=[4,9]
-[00111,01011]=[7,11]
-
-
-*/
-
-
-
-/*
-:- export da/2.
-da(X, X):- !.
-da(X, Y) :- X < Y, print(X), print(";"), nl, XX is X + 1, da(XX, Y).
-
-:- export compute1/5.
-compute1(StringDomain, Size, Len, LL, IN) :-
- varof(X, StringDomain),
- label_all(X, LL),
- list_to_intervals(integer, LL, IN),
- sum_intervals_size(IN, 0, Size),
- length(IN, Len).
-
-:- export orlyfy/3.
-orlyfy(A,B,C) :-
- update_ui_or(A, B, C).
-
-:- export comp2/3.
-
-comp2(StringDomain, IIn, IOut) :-
- varof(X, StringDomain),
- get_bvbounds(X,DX),
- tighten_bounds(IIn, DX, IOut).
-
-:- export compute3/3.
-compute3(StringDomain, Bound, NB, LL) :-
- varof(X, StringDomain),
- label_all(X, LL),
- get_bvbounds(X,DX),
- find_lb(Bound, DX, NB).
-
-:- export compute4/4.
-compute4(StringDomain, BoundL, BoundH, NB, LL) :-
- varof(X, StringDomain),
- label_all(X, LL),
- get_bvbounds(X,DX),
- aux_compute4(BoundL, BoundH, DX, NB).
-
-aux_compute4(BoundL, BoundL,DX, NB) :-
- !,
- find_gb(BoundL, DX, NB).
-aux_compute4(BoundL, BoundH, DX, NB) :-
- find_gb(BoundL, DX, NB),
- BoundT is BoundL + 1,
- aux_compute4(BoundT, BoundH, DX, NB).
-*/
-
% ================== Utils ===================
bulk_lazy_doms([],_) :- !.
bulk_lazy_doms([X|L],M) :-
@@ -830,7 +737,7 @@ bvnot_bis(M,X,Z) :-
set_priority(Prio),
wake_if_other_scheduled(Prio).
-:- export update_ui_not/2.
+:- export update_ui_not/3.
update_ui_not(Mask,I, II) :-
update_ui_not0(Mask,I, [], II).
update_ui_not0(Mask,[], IOut, IOut).
@@ -1600,7 +1507,7 @@ reduce_dom_concat(SX,X, SY, Y, Z) :-
mfd:set_intervals(Y,YYInter)
.
-:- export generate_ui/4.
+:- export update_ui/4.
update_ui(XInter,SY, YInter,ZInter) :-
getval(max_prod_intervals,MaxProd),
LX is length(XInter),
diff --git a/Src/COLIBRI/ndelta.pl b/Src/COLIBRI/ndelta.pl
index d5c1375cc55eb74a20d1dec472514110a628b87d..6817c254a2c7790baff5a12b50042aa6d5550155 100755
--- a/Src/COLIBRI/ndelta.pl
+++ b/Src/COLIBRI/ndelta.pl
@@ -1211,9 +1211,11 @@ launch_delta_bis1(X,Y,S,C) :-
(S == '=' ->
C == 0
; % S == +, C doit accepter 0
- C = Min..Max,
- Min =< 0,
- Max >= 0)
+ (C == 0 ->
+ true
+ ; C = Min..Max,
+ Min =< 0,
+ Max >= 0))
; launch_delta_bis2(X,Y,S,C,CheckCycle,LoopOnly,Abort),
((var(CheckCycle);
nonvar(Abort))
diff --git a/Src/COLIBRI/new_parser_builtins.pl b/Src/COLIBRI/new_parser_builtins.pl
index 30db561ddbe9425e055d98909cd96c649ad39f1a..108e64da6b6c01d355704b628a0a51f2e33f67e4 100644
--- a/Src/COLIBRI/new_parser_builtins.pl
+++ b/Src/COLIBRI/new_parser_builtins.pl
@@ -45,7 +45,7 @@ Et ainsi parser et typer:
Dans un hypothètique p_simplex_ocaml_add_builtins([builtin("fp2bv",[],[bv],[m,e],[],[fp(m,e)],bitv(bv))]). . m et e sont implicites et bv est explicite. Donc l'utilisateur peut écrire ((_ fp2bv 5) myfp) : bv vaudra 5 et m et e seront déterminé par le type de myfp.
*/
-:- export addadd_new_parser_builtins/0.
+:- export add_new_parser_builtins/0.
add_new_parser_builtins :-
p_simplex_ocaml_add_builtins([builtin("spy_here",[],[],[],[],[],bool)]),
p_simplex_ocaml_add_builtins([builtin("to_int",[],[],[],[],[real],int)]),
diff --git a/Src/COLIBRI/notify.pl b/Src/COLIBRI/notify.pl
index e49d8f8a78d4cf7829ead8027cad3dc70eb1b658..f3994a99c2871f2f012d63667437c3cc80a80544 100755
--- a/Src/COLIBRI/notify.pl
+++ b/Src/COLIBRI/notify.pl
@@ -16,7 +16,6 @@
wake_if_other_scheduled/0,
wake_if_other_scheduled/1,
check_no_scheduled_priority/0,
- constrained_var/1,
check_constrained_var/2,
check_constrained_vars/2,
wake_if_constrained/1,
@@ -139,13 +138,13 @@ build_schedule_handler_calls([Mod:FH|Handlers],Goal,Var,Susp,ScheduleHandlerCall
%% sur l'evenement "constrained"
check_constrained_vars([],_).
check_constrained_vars([V|LV],Constrained) :-
- check_constrained_var(V,Constrained),
+ check_constrained_var(V,Constrained),
(nonvar(Constrained) ->
- true
- ; check_constrained_vars(LV,Constrained)).
+ true
+ ; check_constrained_vars(LV,Constrained)).
check_constrained_var(Var,Constrained) :-
- (is_suspend_var(Var,_,_,CstrL) ->
+ (is_suspend_var(Var,_,_,CstrL) ->
check_and_clean_constrained_list(CstrL,NCstrL,Constrained,Clean),
(nonvar(Clean) ->
set_constrained_attr(Var,NCstrL)
diff --git a/Src/COLIBRI/realarith.pl b/Src/COLIBRI/realarith.pl
index dd4c850a0e244b42d4d8ea2afc5d1e037a04bc86..97d4e15e28753ed073dcf9934a1b2f3099d5749c 100755
--- a/Src/COLIBRI/realarith.pl
+++ b/Src/COLIBRI/realarith.pl
@@ -7813,10 +7813,10 @@ op_real1(Type,A,B) :-
wake_if_other_scheduled(Prio).
op_real_bis(Type,A,B) :-
- ((A == B,
- Type == real)
- ->
- protected_unify(A = 0.0)
+ (A == B ->
+ % fail en flottants
+ Type == real,
+ protected_unify(A,0.0)
; save_cstr_suspensions((A,B)),
(is_float_int_number(A) ->
launch_float_int_number(B)
@@ -7874,33 +7874,38 @@ op_real_ineq(Type,A,B) :-
; % A et B sont deja reduits
mreal:dvar_range(A,MinA,MaxA),
mreal:dvar_range(B,MinB,MaxB),
- (MinA >= 0.0 ->
- MaxDelta is get_number_of_floats_between(Type,MinB,MaxA) - 1,
- ((MinA > 0.0;
- not_zero(A))
- ->
- MinDelta is get_number_of_floats_between(Type,MaxB,MinA) - 1
- ; MinDelta = 0),
- interval_from_bounds(MinDelta,MaxDelta,Delta),
- launch_delta(B,A,+,Delta)
- ; (MaxA =< 0.0 ->
- MaxDelta is get_number_of_floats_between(Type,MinA,MaxB) - 1,
- ((MaxA < 0.0;
+ (((MinA,MaxA) == (-0.0,0.0);
+ (MinB,MaxB) == (-0.0,0.0))
+ ->
+ % cas pathologique
+ launch_delta(A,B,#,-1..1)
+ ; (MinA >= 0.0 ->
+ MaxDelta is get_number_of_floats_between(Type,MinB,MaxA) - 1,
+ ((MinA > 0.0;
not_zero(A))
->
- MinDelta is get_number_of_floats_between(Type,MaxA,MinB) - 1
+ MinDelta is get_number_of_floats_between(Type,MaxB,MinA) - 1
; MinDelta = 0),
interval_from_bounds(MinDelta,MaxDelta,Delta),
- launch_delta(A,B,+,Delta)
- ; % A et B non signe
- % MaxDelta avance maximum de MinA vers MaxB
- % MinDelta recul maximum de MaxA vers MinB
- MaxDelta is get_number_of_floats_between(Type,MinA,MaxB) - 1,
- MinDelta is -(get_number_of_floats_between(Type,MinB,MaxA) - 1),
- (not_zero(A) ->
- Sign = '#'
- ; Sign = '+'),
- launch_delta(A,B,Sign,MinDelta..MaxDelta)))),
+ launch_delta(B,A,+,Delta)
+ ; (MaxA =< 0.0 ->
+ MaxDelta is get_number_of_floats_between(Type,MinA,MaxB) - 1,
+ ((MaxA < 0.0;
+ not_zero(A))
+ ->
+ MinDelta is get_number_of_floats_between(Type,MaxA,MinB) - 1
+ ; MinDelta = 0),
+ interval_from_bounds(MinDelta,MaxDelta,Delta),
+ launch_delta(A,B,+,Delta)
+ ; % A et B non signe
+ % MaxDelta avance maximum de MinA vers MaxB
+ % MinDelta recul maximum de MaxA vers MinB
+ MaxDelta is get_number_of_floats_between(Type,MinA,MaxB) - 1,
+ MinDelta is -(get_number_of_floats_between(Type,MinB,MaxA) - 1),
+ (not_zero(A) ->
+ Sign = '#'
+ ; Sign = '+'),
+ launch_delta(A,B,Sign,MinDelta..MaxDelta))))),
% -A > T ==> A < -T
% -A >= T ==> A =< -T
% si A >= -T alors A = -T donc -(-T) = T et -T = -T
@@ -13096,7 +13101,6 @@ average_real_ineqs(Type,A,B,C) :-
occurs(Rel,(<,=<,>,>=)))
->
(getval(use_delta,1)@eclipse ->
- call(spy_here)@eclipse,
(occurs(Rel,(=<,<)) ->
launch_real_ineq(=<,Type,X,C),
launch_real_ineq(=<,Type,C,Y)
@@ -18937,7 +18941,7 @@ geq_real_ineq(Type,A,B) :-
; (occurs(ORel,(=<,>)) ->
Stop = 1,
(ORel == =< ->
- protected_unify(A = B)
+ protected_unify(A,B)
; true)
; % On ajuste les bornes pour avoir les "vrais deltas"
% Attention aux zeros
@@ -18972,11 +18976,18 @@ geq_real_ineq(Type,A,B) :-
protected_unify(B = MinB),
mreal:dvar_remove_smaller(A,MinA)
; true)),
+ mreal:dvar_range(A,NMinA,NMaxA),
+ mreal:dvar_range(B,NMinB,NMaxB),
((nonvar(Stop);
nonvar(A);
- nonvar(B))
+ nonvar(B);
+ (NMinA,NMaxA) == (-0.0,0.0),
+ (NMinB,NMaxB) == (-0.0,0.0),
+ DZ = 1) % cas pathologique
->
- true
+ (nonvar(DZ) ->
+ launch_delta(A,B,+,-1..1)
+ ; true)
; (MinA > MaxB ->
MinDelta is get_number_of_floats_between(Type,MaxB,MinA) - 1
; % Les intervalles se recouvrent la plus petite distance
diff --git a/Src/COLIBRI/smt_import.pl b/Src/COLIBRI/smt_import.pl
index 238293d069cb58853c286d89ec3557728052e00f..e6e8caab41c89f4bc52bb7a80c0a728523f97e5f 100644
--- a/Src/COLIBRI/smt_import.pl
+++ b/Src/COLIBRI/smt_import.pl
@@ -15,6 +15,8 @@
:- include([new_parser_builtins]).
parse_smtlib_file(File,Res) :-
+ % passera à 1 si Int rencontré
+ setval(int_used,0)@eclipse,
% defaut pour la simulation des entiers non bornes
getval(def_real_for_int,RI),
setval(real_for_int,RI)@eclipse,
@@ -169,10 +171,12 @@ check_overloaded(colibri_real_isIntegral,colibri_isIntegral) :- !.
check_overloaded(colibri_fp_isIntegral,colibri_isIntegral) :- !.
check_overloaded(colibri_min_int,colibri_min) :- !.
check_overloaded(colibri_min_real,colibri_min) :- !.
-check_overloaded(colibri_min_fp,colibri_min) :- !.
+%check_overloaded(colibri_min_fp,colibri_min) :- !.
+check_overloaded(colibri_min_fp,'fp.min') :- !.
check_overloaded(colibri_max_int,colibri_max) :- !.
check_overloaded(colibri_max_real,colibri_max) :- !.
-check_overloaded(colibri_max_fp,colibri_max) :- !.
+%check_overloaded(colibri_max_fp,colibri_max) :- !.
+check_overloaded(colibri_max_fp,'fp.max') :- !.
check_overloaded(colibri_exp_real,colibri_exp) :- !.
check_overloaded(colibri_exp_fp,colibri_exp) :- !.
check_overloaded(colibri_ln_real,colibri_ln) :- !.
@@ -1150,8 +1154,8 @@ factorize_and_dump_uninterps([(VN,InSorts,OutSort)|Uninterps]) :-
foreach((SIV,SIs),NInSorts),
foreach(InSorted,InSorteds) do
dump_smt_sort(Is,SIs),
- set_var_name(IV,"ColVar"),
- get_var_name(IV,SIV),
+ protected_set_var_name(IV,"ColVar"),
+ protected_get_var_name(IV,SIV),
concat_string(["(",SIV," ",SIs,")"],InSorted)),
join_string(InSorteds," ",InProf0),
concat_string(["(",InProf0,")"],InProf),
@@ -1513,9 +1517,9 @@ add_binding(Var,Type,Val) :-
(hash_contains(HBinding,Var) ->
true
; ((var(Val),
- not get_var_name(Val,_))
+ not protected_get_var_name(Val,_))
->
- set_var_name(Val,"ColVar")
+ protected_set_var_name(Val,"ColVar")
; true),
hash_set(HBinding,Var,(Type,Val))).
@@ -1529,9 +1533,9 @@ add_label(Label,Type,Val) :-
(hash_contains(HBinding,Label) ->
true
; ((var(Val),
- not get_var_name(Val,_))
+ not protected_get_var_name(Val,_))
->
- set_var_name(Val,"ColVar")
+ protected_set_var_name(Val,"ColVar")
; true),
hash_set(HBinding,Label,(Type,Val))),
getval(labels,Labels-End),
@@ -1638,8 +1642,8 @@ find_mult_occ_compound_subterm(Expr,ST,LP) :-
new_let_var(VId) :-
% Pas de collision possible avec les id smt_lib
- set_var_name(V,"ColId"),
- get_var_name(V,SVId),
+ protected_set_var_name(V,"ColId"),
+ protected_get_var_name(V,SVId),
concat_string(["\"",SVId,"\""],Str),
atom_string(VId,Str).
@@ -2411,9 +2415,18 @@ smt_interp0('bv2nat'(BV),RES,Type) :- !,
(getval(real_for_int,1)@eclipse ->
RES = real_from_int(int_from_uintN(SIZE,IBV))
; RES= int_from_uintN(SIZE,IBV)).
-smt_interp0('int2bv'(Size,Int),Res,Type) :- !,
- smt_interp0('nat2bv'(Size,Int),Res,Type).
smt_interp0('nat2bv'(Size,Int),Res,Type) :- !,
+ integer(Size),
+ Size > 0,
+ (getval(real_for_int,1)@eclipse ->
+ IType = real_int
+ ; IType = int),
+ smt_interp(Int,IInt,IType),
+ Type = uint(Size),
+ (IType == real_int ->
+ Res = uintN_from_nat(Size,int_from_real(IInt))
+ ; Res = uintN_from_nat(Size,IInt)).
+smt_interp0('int2bv'(Size,Int),Res,Type) :- !,
integer(Size),
Size > 0,
(getval(real_for_int,1)@eclipse ->
@@ -2848,8 +2861,8 @@ new_quantifier_abstraction(Res) :-
setval(quantifier,1),
% On cree une variable
get_decl_type_from_sort('Bool',NVar,Decl,bool),
- set_var_name(NVar,"ColQuant"),
- get_var_name(NVar,VS),
+ protected_set_var_name(NVar,"ColQuant"),
+ protected_get_var_name(NVar,VS),
atom_string(Id,VS),
add_binding(Id,bool,NVar),
(getval(decl,ODecl-End) ->
@@ -3032,6 +3045,7 @@ get_type_from_sort(poly(Var),ColType,Type) :- !,
; get_type_from_sort(Var,ColType,Type)).
get_type_from_sort('Bool',bool,bool) :- !.
get_type_from_sort('Int',IType,Type) :-
+ setval(int_used,1)@eclipse,
(getval(real_for_int,1)@eclipse ->
% IType = real,
IType = real_int,
@@ -3119,8 +3133,8 @@ check_rnd(Rnd) :-
IRnd = as(VRnd,_),
var(VRnd))
->
- write(output,"(error \"Warning RoundingMode variable "),
- write(output,Rnd),
+ write(error,"(error \"Warning RoundingMode variable "),
+ write(error,Rnd),
writeln(error," is interpreted as RNE\")")
; true),
check_rnd0(IRnd).
@@ -3295,7 +3309,8 @@ get_int_from_bv('_'(BVNum,Size),Num,Size) :- !,
Size > 0)
->
true
- ; unknown_syntax_error).
+ ; writeln(error,"(error \"Unknown syntax error\")"),
+ exit_block(syntax)).
get_int_from_bv(bv(BX,BVS),I,Size) :-
string_length(BVS,Len),
(BX == "x" ->
diff --git a/Src/COLIBRI/solve.pl b/Src/COLIBRI/solve.pl
index 1fdbb2e86358eb8279dc33c1b377b430a9f99e69..71f957f1a0d5a02895f31ab8a46564f02628aaf4 100644
--- a/Src/COLIBRI/solve.pl
+++ b/Src/COLIBRI/solve.pl
@@ -76,7 +76,7 @@
portray(and_seq_reif/4,trans_and_reif/2,[goal]),
portray(or_seq_reif/4,trans_or_reif/2,[goal]).
*/
-/*
+
trans_col(add_int(X,_,Y,_,Z,_),X + Y #= Z).
trans_col(mult_int(X,_,Y,_,Z,_),X * Y #= Z).
trans_col(div_mod_int(A,B,Q,_,R),((A // B) #= Q,(A rem B) #= R)).
@@ -140,7 +140,7 @@ trans_col(geq_real_reif(_,X,Y,Z),(X $>= Y) #= Z).
trans_col(gt_real_reif(_,X,Y,Z),(X $> Y) #= Z).
trans_col(and_seq_reif(X,_,Y,Z),(X and Y) #= Z).
trans_col(or_seq_reif(X,_,Y,Z),(X or Y) #= Z).
-*/
+
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -318,14 +318,6 @@ set_intSize(Int) :-
update_min_max_lazy_int(Low,High).
-bv_vars(Size, Listvars). % TODO
-/*
-For now, Not bothering with the size
-*/
-bv_var(X, S) :- mbv:varof(X,S). % Initialize domain
-bv_label(L) :- labeling_bv(L).
-
-
sort_vars(Type,T) :-
term_variables(T,Vars),
Type = sort(SId),
@@ -390,8 +382,8 @@ int_vars(Type,T) :-
param(Type) do
(check_int_var_type(X,Type) ->
true
- ; set_int_type(Type,X),
- add_typed_var(X,Type),
+ ; add_typed_var(X,Type),
+ set_int_type(Type,X), % peut instancier X
(Type == bool ->
true
; insert_dep_inst(inst_cstr(0,X))))).
@@ -403,8 +395,8 @@ let_int_vars(int,T) ?- !,
true
; % on retarde le typage par defaut des int
% definis dans les let
- %set_int_type(Type,X),
add_typed_var(X,int),
+ %set_int_type(Type,X),
insert_dep_inst(inst_cstr(0,X)))).
let_int_vars(Type,T) :-
int_vars(Type,T).
@@ -461,6 +453,7 @@ add_typed_var(V,Type) :-
exit_block(syntax))
; hash_set(Hash,VA,(V,Type)),
setval(typed_vars,Hash))).
+
get_variable_type(V,Type) :-
var(V),
@@ -476,11 +469,24 @@ get_variable_from_name(Name,Var) :-
hash_get(Hash,AName,(Var,_)).
:- lib(var_name).
+protected_get_var_name(V,Name) :-
+ (var(V) ->
+ get_var_name(V,Name)
+ ; call(spy_here)@eclipse,
+ writeln(error,"Error: variable needed as first argument of get_var_name/2"),
+ exit_block(syntax)).
+protected_set_var_name(V,Name) :-
+ (var(V) ->
+ set_var_name(V,Name)
+ ; call(spy_here)@eclipse,
+ writeln(error,"Error: variable needed as first argument of set_var_name/2"),
+ exit_block(syntax)).
+
get_variable_atom(V,VA) :-
- (get_var_name(V,VS) ->
+ (protected_get_var_name(V,VS) ->
atom_string(VA,VS)
- ; set_var_name(V,"ColVar"),
- get_var_name(V,VS),
+ ; protected_set_var_name(V,"ColVar"),
+ protected_get_var_name(V,VS),
atom_string(VA,VS)).
check_int_var_type(V,Type) :-
@@ -1784,6 +1790,7 @@ unfold_int_expr(intN_from_uint(N,EA),D,Cstr,Type,R) ?-
insert_dep_inst(dep(A,D,[UO])),
insert_dep_inst(dep(R,D,[A,UO])),
make_conj(CA,uintN_to_intN(N,A,R,UO),Cstr)).
+% smtlib int2bv
unfold_int_expr(uintN_from_int(N,EA),D,Cstr,Type,R) ?-
ND is D + 1,
integer(N),
@@ -1797,6 +1804,18 @@ unfold_int_expr(uintN_from_int(N,EA),D,Cstr,Type,R) ?-
Cstr = CA
; insert_dep_inst(dep(R,D,[A])),
make_conj(CA,to_intNu(N,A,R),Cstr)).
+% smtlib nat2bv, partielle
+unfold_int_expr(uintN_from_nat(N,EA),D,Cstr,Type,R) ?-
+ ND is D + 1,
+ integer(N),
+ N > 0,
+ unfold_int_expr(EA,ND,CA,int,A),
+ !,
+ Type = uint(N),
+ unfold_int_expr(as(A,int) #< as(0,int),D,CBool,bool,Bool),
+ insert_dep_inst(dep(R,D,[Bool,A])),
+ make_conj(CA,CBool,CABool),
+ make_conj(CABool,chk_undef_nat_to_intNu(Bool,N,A,R),Cstr).
unfold_int_expr(uintN_from_intN(N,EA),D,Cstr,Type,R) ?-
ND is D + 1,
integer(N),
@@ -4033,87 +4052,6 @@ eval_select(Type,A,I,E,Start,true) :-
array_vars(TI,TE,Start),
protected_unify(A,storec(Start,I,v(u,E,true))).
-/*
-smtlib_select(array(TypeI,TypeE),A,I,E) :-
- (real_type(TypeI,_) ->
- real_vars(real_int,I)
- ; let_int_vars(TypeI,I)),
- (real_type(TypeE,_) ->
- real_vars(TypeE,E)
- ; let_int_vars(TypeE,E)),
- smtlib_select(A,I,E,TypeI,TypeE).
-
-smtlib_select(storec(A,J,TrJ),I,E,TI,TE) ?- !,
- (I == J ->
- TrJ = v(_,VEJ,CstrEJ),
- (TE = array(_,_) ->
- check_eq_array(TE,VEJ,E)
- ; protected_unify(VEJ,E)),
- call(CstrEJ)
- ; (not_unify(I,J) ->
- smtlib_select(A,I,E,TI,TE)
- ; TrJ = v(_,VEJ,_),
- ((TE \= array(_,_),
- not_unify(E,VEJ))
- ->
- diff_reif(TE,_,VEJ,E,1),
- smtlib_select(A,I,E,TI,TE)
- ; remove_not_possible_stores(A,I,E,TE,NA),
- Array = storec(NA,J,TrJ),
- get_array_start(NA,Start),
- ((once (TE \= array(_,_);
- var(E)),
- save_cstr_suspensions(Start),
- get_saved_cstr_suspensions(LS),
- member((S,smtlib_select(AA,II,EE,TI,TE)),LS),
- get_suspension_data(S,goal,smtlib_select(AArray,II,EE,TI,TE)),
- Array == AArray,
- I == II)
- ->
- kill_suspension(S),
- protected_unify(E,EE)
- ; true),
- int_vars(bool,Bool),
- diff_reif(TI,_,I,J,Bool),
- (nonvar(Bool) ->
- smtlib_select(Array,I,E,TI,TE)
- ; get_reif_var_depth_from_labchoice(Depth),
- insert_dep_inst(dep(Bool,Depth,[])),
- insert_dep_inst(dep(I,Depth,[])),
- insert_dep_inst(dep(E,Depth,[])),
- insert_dep_inst(dep(J,Depth,[])),
- insert_dep_inst(dep(Bool,Depth,[I,J,A])),
- insert_dep_inst(dep(I,Depth,[Bool,J,E,A])),
- insert_dep_inst(dep(J,Depth,[Bool,I,E,A])),
- my_suspend(smtlib_select(Array,I,E,TI,TE),
- 0,
- [Start->suspend:constrained,Bool->suspend:inst]))))).
-smtlib_select(A,I,E,TI,TE) :-
- (var(A) ->
- array_vars(TI,TE,Start),
- A = storec(Start,I,v(u,E,true))
- ; A = const_array(TI,TE,Const),
- (TE = array(_,_) ->
- check_eq_array(TE,Const,E)
- ; protected_unify(Const,E))).
-
-remove_not_possible_stores(A,I,E,TE,NA) :-
- ((var(A);
- A = const_array(_,_,_))
- ->
- NA = A
- ; A = storec(SA,J,TrJ),
- (not_unify(I,J) ->
- remove_not_possible_stores(SA,I,E,TE,NA)
- ; TrJ = v(_,VJ,_),
- ((TE \= array(_,_),
- not_unify(VJ,E))
- ->
- diff_reif(TE,_,I,J,1),
- NA = SNA
- ; NA = storec(SNA,J,TrJ)),
- remove_not_possible_stores(SA,I,E,TE,SNA))).
-*/
smtlib_select(array(TypeI,TypeE),A,I,E) :-
(real_type(TypeI,_) ->
@@ -4160,7 +4098,7 @@ smtlib_select_bis(A,I,E,TypeI,TypeE) :-
int_vars(bool,Bool),
diff_reif(TypeI,_,I,J,Bool),
(nonvar(Bool) ->
- smtlib_select(NewA,NStart,Sure,I,E,TypeI,TypeE)
+ smtlib_select(NewA,NStart,I,E,TypeI,TypeE)
; get_reif_var_depth_from_labchoice(Depth),
insert_dep_inst(dep(Bool,Depth,[])),
insert_dep_inst(dep(I,Depth,[])),
@@ -4178,11 +4116,6 @@ check_before_suspend_select(NewA,NStart,I,E,TypeI,TypeE,SuspVars,LSusp) :-
I == II,
NStart == NNStart,
NewA == NNewA)
-/*
- once (TypeE \= array(_,_);
- var(E);
- var(EE)))
-*/
->
((TypeE \= array(_,_);
var(E);
@@ -5490,10 +5423,18 @@ or_seq_reif(A,CB,B,C) :-
*/
get_bool_var_type(V,Type) :-
+ var(V),
getval(typed_vars,Hash),
Hash \== 0,
get_variable_atom(V,VA),
hash_get(Hash,VA,(_,Type)).
+get_bool_var_type(Num,Type) :-
+ number(Num),
+ once (Num == 0;
+ Num == 1),
+ (var(Type) ->
+ Type = bool
+ ; occurs(Type,(int,bool))).
%% ESSAI
@@ -6209,7 +6150,9 @@ real_vars(Type,T) :-
exit_block(syntax))
; insert_dep_inst(inst_cstr(0,X)),
set_lazy_domain(RType,X)),
- add_typed_var(X,RType),
+ (var(X) ->
+ add_typed_var(X,RType)
+ ; true),
(RType == real ->
% on accepte les rbox
ensure_not_NaN(X),
@@ -7405,7 +7348,8 @@ unfold_real_expr(fp_ln(EA),D,Cstr,Type,R) ?-
unfold_real_expr(exp(EA),D,Cstr,RType,R) ?-
ND is D + 1,
unfold_real_expr(EA,ND,CA,RType,A),
- nonvar(RType,Type),
+ nonvar(RType),
+ real_type(RType,Type),
!,
insert_dep_inst(dep(R,D,[A])),
make_conj(CA,exp(Type,A,R),Cstr).
@@ -7456,9 +7400,13 @@ unfold_real_expr(min(EA,EB),D,Cstr,RType,R) ?- !,
unfold_real_expr(EB,ND,CB,RType,B),
nonvar(RType),
real_type(RType,Type),
- insert_dep_inst(dep(R,D,[A,B])),
make_conj(CA,CB,CAB),
- make_conj(CAB,launch_min_real(Type,A,B,R),Cstr).
+ (occurs(Type,(float_simple,float_double)) ->
+ unfold_real_expr(fp_min(as(A,Type),as(B,Type)),D,CFP,Type,R),
+ make_conj(CA,CB,CAB),
+ make_conj(CAB,CFP,Cstr)
+ ; insert_dep_inst(dep(R,D,[A,B])),
+ make_conj(CAB,launch_min_real(Type,A,B,R),Cstr)).
unfold_real_expr(fp_max(EA,EB),D,Cstr,Type,R) ?- !,
ND is D + 1,
@@ -7489,9 +7437,14 @@ unfold_real_expr(max(EA,EB),D,Cstr,RType,R) ?- !,
unfold_real_expr(EB,ND,CB,RType,B),
nonvar(RType),
real_type(RType,Type),
- insert_dep_inst(dep(R,D,[A,B])),
make_conj(CA,CB,CAB),
- make_conj(CAB,launch_max_real(Type,A,B,R),Cstr).
+ (occurs(Type,(float_simple,float_double)) ->
+ unfold_real_expr(fp_max(as(A,Type),as(B,Type)),D,CFP,Type,R),
+ make_conj(CA,CB,CAB),
+ make_conj(CAB,CFP,Cstr)
+ ; insert_dep_inst(dep(R,D,[A,B])),
+ make_conj(CAB,launch_max_real(Type,A,B,R),Cstr)).
+
unfold_real_expr(ite(Cond,Then,Else),D,Cstr,RType,R) ?-
ND is D + 1,
unfold_int_expr(Cond,ND,CC,bool,RCond),
@@ -9747,6 +9700,31 @@ only_one_neq_args_pair([T|TArgs],[A1|Args],[CA1|CArgs],TA,A,CA) :-
%% Les undef
+chk_undef_nat_to_intNu(0,N,A,R) ?- !,
+ to_intNu(N,A,R).
+chk_undef_nat_to_intNu(1,N,A,R) ?- !,
+ int_vars(int,A),
+ int_vars(uint(N),R),
+ undef_nat_to_intNu(N,A,R).
+chk_undef_nat_to_intNu(Bool,N,A,R) :-
+ get_priority(P),
+ set_priority(1),
+ save_cstr_suspensions(A),
+ get_saved_cstr_suspensions(LSusp),
+ ((member((_,chk_undef_nat_to_intNu(BBool,N,AA,RR)),LSusp),
+ AA == A)
+ ->
+ protected_unify(BBool,Bool),
+ protected_unify(RR,R)
+ ; my_suspend(chk_undef_nat_to_intNu(Bool,N,A,R),0,
+ (Bool,A)->suspend:constrained)),
+ set_priority(P),
+ wake_if_other_scheduled(P).
+
+undef_nat_to_intNu(N,A,R) :-
+ uninterp(nat2bv,nat2bv,[int],uint(N),[A],R).
+
+
chk_undef_div_real(Bool,A,B,R) :-
get_priority(P),
set_priority(1),
@@ -11094,7 +11072,7 @@ solve_cstrs_list([UseList|SplitUseList]) :-
/*
term_variables(UseList,Vars),
(foreach(Var,Vars) do
- (get_var_name(Var,_) ->
+ (protected_get_var_name(Var,_) ->
true
; (get_type(Var,Type) ->
add_typed_var(Var,Type)
@@ -11150,7 +11128,7 @@ new_choose_fd_var3(UseList0,CVars,NCVars,Seen,NSeen,Var,Size,NUseList) :-
getval(new_dep,Deps),
term_variables(Deps,DepVars),
(foreach(DV,DepVars) do
- (get_var_name(DV,_) ->
+ (protected_get_var_name(DV,_) ->
true
; (get_type(DV,TDV) ->
add_typed_var(DV,TDV)
@@ -11242,15 +11220,15 @@ get_most_constrained_bool_var(UseList,Var,Nb) :-
BSVars = SVars
; BSVars = BVars),
(BSVars = [(V,NbV)|EBSVars] ->
- (get_var_name(V,_) ->
+ (protected_get_var_name(V,_) ->
true
- ; set_var_name(V,"ColVar")),
+ ; protected_set_var_name(V,"ColVar")),
(foreach((VV,NbVV),EBSVars),
fromto(V,IV,OV,Var),
fromto(NbV,IN,ON,Nb) do
- (get_var_name(VV,_) ->
+ (protected_get_var_name(VV,_) ->
true
- ; set_var_name(VV,"ColVar")),
+ ; protected_set_var_name(VV,"ColVar")),
(NbVV > IN ->
ON = NbVV,
OV = VV
@@ -11314,11 +11292,11 @@ get_most_constrained_bool_var([(V,D,Adj)|UseList],VN,NUseList,Seen,OVar,ONb,Var,
call(spy_here)@eclipse)),
not occurs(E,ISeen))
->
- (get_var_name(E,_) ->
+ (protected_get_var_name(E,_) ->
true
- ; set_var_name(E,"ColVar")),
+ ; protected_set_var_name(E,"ColVar")),
delayed_goals_number(E,NbE),
- ((get_var_name(E,EN),
+ ((protected_get_var_name(E,EN),
EN == VN,
FoundVN = 1;
NbE > IN)
@@ -12009,7 +11987,7 @@ simple_solve_var_type(int,Var,_) :-
(IVar = [_,_|_] ->
(call_priority(simple_resol_int(Var),1);
IVar == [0,1],
- get_var_name(Var,VN),
+ protected_get_var_name(Var,VN),
getval(last_var_fail,LVN)@eclipse,
append(LVN,[VN],NLVN),
setval(last_var_fail,NLVN)@eclipse,
@@ -12025,14 +12003,6 @@ simple_solve_var_type(int,Var,_) :-
; call_priority(simple_resol_bv(Var),1))
))
-/*
- ;
- get_var_name(Var,VN),
- getval(last_var_fail,LVN)@eclipse,
- append(LVN,[VN],NLVN),
- setval(last_var_fail,NLVN)@eclipse,
- fail
-*/
; true).
simple_solve_var_type(real,Var,_) :-
@@ -12071,7 +12041,7 @@ simple_solve_var_float(Type,Var) :-
1).
/*
;
- get_var_name(Var,VN),
+ protected_get_var_name(Var,VN),
getval(last_var_fail,LVN)@eclipse,
append(LVN,[VN],NLVN),
setval(last_var_fail,NLVN)@eclipse,
@@ -12477,18 +12447,8 @@ inst_type(enum(_),V) :-!,
inst_type(rnd,V) :- !,
inst_rnd(V).
inst_type(int,V) :-!,
- ((var(V),
- get_bvbounds(V,_))
- ->
- once simple_resol_bv(V)
- ; true),
inst_int(V).
inst_type(int(_),V) :-
- ((var(V),
- get_bvbounds(V,_))
- ->
- once simple_resol_bv(V)
- ; true),
inst_int(V).
inst_type(real,V) :-
inst_real(V).
diff --git a/Src/COLIBRI/util.pl b/Src/COLIBRI/util.pl
index 041524b266784fad5ff085d231cedfbd9c48eb24..042e6885c5622ecad90a221c58a55632f1e4a2ac 100755
--- a/Src/COLIBRI/util.pl
+++ b/Src/COLIBRI/util.pl
@@ -71,13 +71,14 @@ extract_susp_goals([S|LS],LSG) :-
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% open avec stream nomme
+:- export open_named_stream/3.
open_named_stream(Source,Mode,StreamName) :-
- ((nonvar(StreamName),
- current_stream(StreamName))
- ->
- close(StreamName)
- ; true),
- open(Source,Mode,StreamName).
+ ((nonvar(StreamName),
+ current_stream(StreamName))
+ ->
+ close(StreamName)
+ ; true),
+ open(Source,Mode,StreamName).
%% Pour les utilitaires qui sont
%% utilises dans les modules (mfd,mreal,ndelta)