From bcddf43b70148693f2c46be34d8413c33e151b78 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Fri, 8 Oct 2021 13:34:00 +0200
Subject: [PATCH 1/3] Regression test for #46
---
tests/sat/issue_46.smt2 | 8 ++++++++
1 file changed, 8 insertions(+)
create mode 100644 tests/sat/issue_46.smt2
diff --git a/tests/sat/issue_46.smt2 b/tests/sat/issue_46.smt2
new file mode 100644
index 000000000..9c53d2369
--- /dev/null
+++ b/tests/sat/issue_46.smt2
@@ -0,0 +1,8 @@
+(set-logic ALL)
+(set-info :smt-lib-version 2.6)
+(declare-const modes_on Bool)
+(declare-const unit_delay_memory Bool)
+(assert
+(not
+(= (ite (= unit_delay_memory true) true (ite (= modes_on true) false true)) true)))
+(check-sat)
--
GitLab
From 68cc1e86c7d547203a3a899c39edfd5981025dac Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Fri, 8 Oct 2021 13:34:24 +0200
Subject: [PATCH 2/3] Import from Bin:a1af7a0 Src:c7a5f59b0 farith:a93db57
---
Src/COLIBRI/col_solve.pl | 151 ++++--
Src/COLIBRI/colibri.pl | 4 +-
Src/COLIBRI/mbv.pl | 743 +----------------------------
Src/COLIBRI/mbv_propa.pl | 97 +---
Src/COLIBRI/ndelta.pl | 8 +-
Src/COLIBRI/new_parser_builtins.pl | 2 +-
Src/COLIBRI/notify.pl | 9 +-
Src/COLIBRI/realarith.pl | 73 +--
Src/COLIBRI/smt_import.pl | 49 +-
Src/COLIBRI/solve.pl | 236 ++++-----
Src/COLIBRI/util.pl | 13 +-
11 files changed, 310 insertions(+), 1075 deletions(-)
diff --git a/Src/COLIBRI/col_solve.pl b/Src/COLIBRI/col_solve.pl
index edb8d1ab3..838ef4b26 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 4bd9c1424..f54b06899 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 2f3a7d90c..32a70dfdf 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 52eaf4e65..86ae21bd8 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 d5c1375cc..6817c254a 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 30db561dd..108e64da6 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 e49d8f8a7..f3994a99c 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 dd4c850a0..97d4e15e2 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 238293d06..e6e8caab4 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 1fdbb2e86..71f957f1a 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 041524b26..042e6885c 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)
--
GitLab
From 9794c2ab8437a1aced183a4cd85ee5c4cd05c2c3 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Sun, 10 Oct 2021 18:32:35 +0200
Subject: [PATCH 3/3] Import from Bin:a1af7a0 Src:f66bd1f8c farith:a93db57
---
Src/COLIBRI/arith.pl | 1604 ++++++++++++++++++-------------------
Src/COLIBRI/check_ineq.pl | 283 +++----
Src/COLIBRI/col_solve.pl | 7 +-
3 files changed, 945 insertions(+), 949 deletions(-)
diff --git a/Src/COLIBRI/arith.pl b/Src/COLIBRI/arith.pl
index 001fd1373..fbd9e800d 100755
--- a/Src/COLIBRI/arith.pl
+++ b/Src/COLIBRI/arith.pl
@@ -872,147 +872,147 @@ add_free_rec(Cpt,A,TA,B,TB,C,TC) :-
%% C = C{(mod) : '0[2]', mfd : [4 .. 24]}
%% et on a delta(A, B, =, -2)
add_interval(Val1,Val2,Val) :-
- integer(Val1),
- integer(Val2),!,
- Val0 is Val1 + Val2,
+ integer(Val1),
+ integer(Val2),!,
+ Val0 is Val1 + Val2,
protected_unify(Val,Val0).
add_interval(Val1,Val2,Val) :-
- (get_type(Val,_) ->
- true
- ; % Val non initialise
- mfd:dvar_range(Val1,Low1,High1),
- mfd:dvar_range(Val2,Low2,High2),
- add_intervals(Low1..High1,Low2..High2,Low,High),
- mfd:quiet_set_intervals(Val,[Low..High])),
- (integer(Val) ->
- true
- ; %% on peut mettre a jour Val1 et Val2 selon le delta (Val1,Val2)
- update_args_from_delta(Rel12,Delta,Val1,Val2),
- %% on met a jour Val1 et Val2 selon les deltas (Val2,Val) et (Val1,Val)
- update_var_from_delta(Val1,Val2,Val),
- update_var_from_delta(Val2,Val1,Val),
- mfd:get_intervals(Val1,Inter1),
- mfd:get_intervals(Val2,Inter2),
- mfd:get_intervals(Val,Inter),
- ((Rel12 == ?,
- (Inter1 == Inter, number_in_interval(Inter2,0);
- Inter2 == Inter, number_in_interval(Inter1,0)))
- ->
- %% Le 0 de Val1 ou Val2 copiera Val2 ou Val1
- %% Inutile de continuer
- true
- ; ((Inter1 = [I1],
- Inter2 = [I2])
- ->
- %% 90% des cas, les bornes sont ajustees pour #
- %% sinon elles sont compatibles
- binop_intervals_Rel(Rel12,add,I1,I2,NMin,NMax),
- %% add_intervals(I1,I2,NMin,NMax),
- LInter = [NMin..NMax]
- ; getval(max_prod_intervals,MaxProd),
- L1 is length(Inter1),
- L2 is length(Inter2),
- (L1*L2 > MaxProd ->
- %% On ne travaille que sur les bornes
- %% en gardant le trou autour de zero si il existe
- mfd:dvar_range(Val1,Min1,Max1),
- mfd:dvar_range(Val2,Min2,Max2),
- keep_zero_hole(Inter1,Min1,Max1,NInter1),
- keep_zero_hole(Inter2,Min2,Max2,NInter2)
- ; NInter1 = Inter1,
- NInter2 = Inter2),
- mfd:dvar_range(Val,Min,Max),
- add_interval_list(Rel12,Delta,NInter1,NInter2,Min,Max,NewInter1,NewInter2,LInter,NDelta),
- (Rel12 \== ? ->
- list_to_intervals(integer,NewInter1,NLInter1),
- mfd:quiet_set_intervals(Val1,NLInter1),
- list_to_intervals(integer,NewInter2,NLInter2),
- mfd:quiet_set_intervals(Val2,NLInter2),
- %% Mise a jour du delta si different
- launch_delta(Val1,Val2,'+',NDelta)
- ; true)),
- list_to_intervals(integer,LInter,InterAdd),
- mfd:quiet_set_intervals(Val,InterAdd))),
- congr_add_directe(Val1,Val2,Val).
+ (get_type(Val,_) ->
+ true
+ ; % Val non initialise
+ mfd:dvar_range(Val1,Low1,High1),
+ mfd:dvar_range(Val2,Low2,High2),
+ add_intervals(Low1..High1,Low2..High2,Low,High),
+ mfd:quiet_set_intervals(Val,[Low..High])),
+ (integer(Val) ->
+ true
+ ; % on peut mettre a jour Val1 et Val2 selon le delta (Val1,Val2)
+ update_args_from_delta(Rel12,Delta,Val1,Val2),
+ % on met a jour Val1 et Val2 selon les deltas (Val2,Val) et (Val1,Val)
+ update_var_from_delta(Val1,Val2,Val),
+ update_var_from_delta(Val2,Val1,Val),
+ mfd:get_intervals(Val1,Inter1),
+ mfd:get_intervals(Val2,Inter2),
+ mfd:get_intervals(Val,Inter),
+ ((Rel12 == ?,
+ (Inter1 == Inter, number_in_interval(Inter2,0);
+ Inter2 == Inter, number_in_interval(Inter1,0)))
+ ->
+ % Le 0 de Val1 ou Val2 copiera Val2 ou Val1
+ % Inutile de continuer
+ true
+ ; ((Inter1 = [I1],
+ Inter2 = [I2])
+ ->
+ % 90% des cas, les bornes sont ajustees pour #
+ % sinon elles sont compatibles
+ binop_intervals_Rel(Rel12,add,I1,I2,NMin,NMax),
+ % add_intervals(I1,I2,NMin,NMax),
+ LInter = [NMin..NMax]
+ ; getval(max_prod_intervals,MaxProd),
+ L1 is length(Inter1),
+ L2 is length(Inter2),
+ (L1*L2 > MaxProd ->
+ % On ne travaille que sur les bornes
+ % en gardant le trou autour de zero si il existe
+ mfd:dvar_range(Val1,Min1,Max1),
+ mfd:dvar_range(Val2,Min2,Max2),
+ keep_zero_hole(Inter1,Min1,Max1,NInter1),
+ keep_zero_hole(Inter2,Min2,Max2,NInter2)
+ ; NInter1 = Inter1,
+ NInter2 = Inter2),
+ mfd:dvar_range(Val,Min,Max),
+ add_interval_list(Rel12,Delta,NInter1,NInter2,Min,Max,NewInter1,NewInter2,LInter,NDelta),
+ (Rel12 \== ? ->
+ list_to_intervals(integer,NewInter1,NLInter1),
+ mfd:quiet_set_intervals(Val1,NLInter1),
+ list_to_intervals(integer,NewInter2,NLInter2),
+ mfd:quiet_set_intervals(Val2,NLInter2),
+ % Mise a jour du delta si different
+ launch_delta(Val1,Val2,'+',NDelta)
+ ; true)),
+ list_to_intervals(integer,LInter,InterAdd),
+ mfd:quiet_set_intervals(Val,InterAdd))),
+ congr_add_directe(Val1,Val2,Val).
add_interval_list(?,?,LI1,LI2,MinInt,MaxInt,LI1,LI2,LI,?) :- !,
- add_interval_list(LI1,LI2,MinInt,MaxInt,LI).
+ add_interval_list(LI1,LI2,MinInt,MaxInt,LI).
add_interval_list(Rel12,Delta,LI1,LI2,MinInt,MaxInt,NewLI1,NewLI2,LI,NL..NH) :-
- min_max_inter(Delta,L,H),
- binop_interval_list_delta(add,Rel12,L..H,LI1,LI2,NewLI1,NewLI2,LI,H..L,NL..NH).
+ min_max_inter(Delta,L,H),
+ binop_interval_list_delta(add,Rel12,L..H,LI1,LI2,NewLI1,NewLI2,LI,H..L,NL..NH).
%% On peut abandonner des qu'on calcule un intervalle
%% contenant MinInt..MaxInt
add_interval_list(LI1,LI2,MinInt,MaxInt,LI) :-
- block(
- add_interval_list1(LI1,LI2,MinInt,MaxInt,LI),
- included_interval,
- (interval_from_bounds(MinInt,MaxInt,Inter),
- LI = [Inter])).
+ block(
+ add_interval_list1(LI1,LI2,MinInt,MaxInt,LI),
+ included_interval,
+ (interval_from_bounds(MinInt,MaxInt,Inter),
+ LI = [Inter])).
:- mode(add_interval_list1(++,++,++,++,-)).
add_interval_list1([],_,_,_,[]).
add_interval_list1([I1|LI1],LI2,MinInt,MaxInt,LI) :-
- min_max_inter(I1,Min1,Max1),
- add_interval_list_bis(Min1,Max1,LI2,MinInt,MaxInt,NotFirst,TooBig,LI,ELI),
- ((var(NotFirst),
- nonvar(TooBig))
- ->
- %% On a echoue sur le premier de LI2 avec
- %% un intervalle trop grand.
- %% Inutile de continuer sur LI1 car add est croissante
- %% (les intervalles sont aussi classes par ordre croissant)
- ELI = []
- ; add_interval_list1(LI1,LI2,MinInt,MaxInt,ELI)).
+ min_max_inter(I1,Min1,Max1),
+ add_interval_list_bis(Min1,Max1,LI2,MinInt,MaxInt,NotFirst,TooBig,LI,ELI),
+ ((var(NotFirst),
+ nonvar(TooBig))
+ ->
+ % On a echoue sur le premier de LI2 avec
+ % un intervalle trop grand.
+ % Inutile de continuer sur LI1 car add est croissante
+ % (les intervalles sont aussi classes par ordre croissant)
+ ELI = []
+ ; add_interval_list1(LI1,LI2,MinInt,MaxInt,ELI)).
:- mode(add_interval_list_bis(++,++,++,++,++,?,?,?,?)).
add_interval_list_bis(_,_,[],_,_,_,_,LI,LI).
add_interval_list_bis(Min1,Max1,[I2|LI2],MinInt,MaxInt,NotFirst,TooBig,LI,ELI) :-
- min_max_inter(I2,Min2,Max2),
- Max is Max1 + Max2,
- (Max < MinInt ->
- %% Trop petit: on continue dans LI2
- %% Donc on n'abandonne pas sur le premier
- NotFirst = 1,
- add_interval_list_bis(Min1,Max1,LI2,MinInt,MaxInt,NotFirst,TooBig,LI,ELI)
- ; Min is Min1 + Min2,
- (Min > MaxInt ->
- %% Trop grand: pas la peine de continuer dans LI2
- %% On continue dans LI1
- TooBig = 1,
- LI = ELI
- ; %% On continue dans LI2
- %% Donc on n'abandonne pas sur le premier
- check_included(MinInt,MaxInt,Min,Max),
- NotFirst = 1,
- interval_from_bounds(Min,Max,Inter),
- LI = [Inter|NLI],
- add_interval_list_bis(Min1,Max1,LI2,MinInt,MaxInt,NotFirst,TooBig,NLI,ELI))).
+ min_max_inter(I2,Min2,Max2),
+ Max is Max1 + Max2,
+ (Max < MinInt ->
+ % Trop petit: on continue dans LI2
+ % Donc on n'abandonne pas sur le premier
+ NotFirst = 1,
+ add_interval_list_bis(Min1,Max1,LI2,MinInt,MaxInt,NotFirst,TooBig,LI,ELI)
+ ; Min is Min1 + Min2,
+ (Min > MaxInt ->
+ % Trop grand: pas la peine de continuer dans LI2
+ % On continue dans LI1
+ TooBig = 1,
+ LI = ELI
+ ; % On continue dans LI2
+ % Donc on n'abandonne pas sur le premier
+ check_included(MinInt,MaxInt,Min,Max),
+ NotFirst = 1,
+ interval_from_bounds(Min,Max,Inter),
+ LI = [Inter|NLI],
+ add_interval_list_bis(Min1,Max1,LI2,MinInt,MaxInt,NotFirst,TooBig,NLI,ELI))).
:- mode check_included(++,++,++,++).
check_included(MinInt,MaxInt,Min,Max) :-
- ((Min =< MinInt,
- Max >= MaxInt)
- ->
- %% Inutile de continuer, on peut abandonner
- exit_block(included_interval)
- ; true).
+ ((Min =< MinInt,
+ Max >= MaxInt)
+ ->
+ % Inutile de continuer, on peut abandonner
+ exit_block(included_interval)
+ ; true).
:- mode(add_intervals(++,++,-,-)).
add_intervals(ValInter1,ValInter2,B1,B2) :-
- min_max_inter(ValInter1,Min1,Max1),
- min_max_inter(ValInter2,Min2,Max2),
- B1 is Min2 + Min1,
- B2 is Max2 + Max1.
+ min_max_inter(ValInter1,Min1,Max1),
+ min_max_inter(ValInter2,Min2,Max2),
+ B1 is Min2 + Min1,
+ B2 is Max2 + Max1.
@@ -1020,127 +1020,127 @@ add_intervals(ValInter1,ValInter2,B1,B2) :-
%% Puis intersection du domaine calcule (MinusDom, non initialise)
%% avec celui de la variable resultat (Val)
minus_interval(Val1,Val2,Val) :-
- integer(Val1),
- integer(Val2),!,
- Val0 is Val1 - Val2,
+ integer(Val1),
+ integer(Val2),!,
+ Val0 is Val1 - Val2,
protected_unify(Val,Val0).
minus_interval(Val1,Val2,Val) :-
- (get_type(Val,_) ->
- true
- ; % Val non initialise
- mfd:dvar_range(Val1,Low1,High1),
- mfd:dvar_range(Val2,Low2,High2),
- minus_intervals(Low1..High1,Low2..High2,Low,High),
- mfd:quiet_set_intervals(Val,[Low..High])),
- (integer(Val) ->
- true
- ; %% on peut mettre a jour Val1 et Val2 selon le delta(Val1,Val2)
- update_args_from_delta(Rel12,Delta,Val1,Val2),
- %% on a Val1 - Val2 = Val, ie Val + Val2 = Val1
- %% on peut mettre a jour Val2 selon le delta(Val,Val1)
- update_var_from_delta(Val2,Val,Val1),
- mfd:get_intervals(Val1,Inter1),
- mfd:get_intervals(Val2,Inter2),
- mfd:get_intervals(Val,Inter),
- ((Rel12 == ?,
- Inter1 == Inter,
- number_in_interval(Inter2,0))
- ->
- %% Le 0 de Val2 copie Val1
- %% Inutile de continuer
- true
- ; ((Inter1 = [I1],
- Inter2 = [I2])
- ->
- binop_intervals_Rel(Rel12,minus,I1,I2,NMin,NMax),
- %% minus_intervals(I1,I2,NMin,NMax),
- LInter = [NMin..NMax]
- ; L1 is length(Inter1),
- L2 is length(Inter2),
- getval(max_prod_intervals,MaxProd),
- (L1*L2 > MaxProd ->
- %% On ne travaille que sur les bornes
- %% en gardant le trou autour de zero si il existe
- mfd:dvar_range(Val1,Min1,Max1),
- mfd:dvar_range(Val2,Min2,Max2),
- keep_zero_hole(Inter1,Min1,Max1,NInter1),
- keep_zero_hole(Inter2,Min2,Max2,NInter2)
- ; NInter1 = Inter1,
- NInter2 = Inter2),
- mfd:dvar_range(Val,Min,Max),
- minus_interval_list(Rel12,Delta,NInter1,NInter2,Min,Max,NewInter1,NewInter2,LInter,NDelta),
- (Rel12 \== ? ->
- list_to_intervals(integer,NewInter1,NLInter1),
- mfd:quiet_set_intervals(Val1,NLInter1),
- list_to_intervals(integer,NewInter2,NLInter2),
- mfd:quiet_set_intervals(Val2,NLInter2),
- launch_delta(Val1,Val2,'+',NDelta)
- ; true)),
- list_to_intervals(integer,LInter,InterMinus),
- mfd:quiet_set_intervals(Val,InterMinus))),
- congr_add_inverse(Val1,Val2,Val).
+ (get_type(Val,_) ->
+ true
+ ; % Val non initialise
+ mfd:dvar_range(Val1,Low1,High1),
+ mfd:dvar_range(Val2,Low2,High2),
+ minus_intervals(Low1..High1,Low2..High2,Low,High),
+ mfd:quiet_set_intervals(Val,[Low..High])),
+ (integer(Val) ->
+ true
+ ; % on peut mettre a jour Val1 et Val2 selon le delta(Val1,Val2)
+ update_args_from_delta(Rel12,Delta,Val1,Val2),
+ % on a Val1 - Val2 = Val, ie Val + Val2 = Val1
+ % on peut mettre a jour Val2 selon le delta(Val,Val1)
+ update_var_from_delta(Val2,Val,Val1),
+ mfd:get_intervals(Val1,Inter1),
+ mfd:get_intervals(Val2,Inter2),
+ mfd:get_intervals(Val,Inter),
+ ((Rel12 == ?,
+ Inter1 == Inter,
+ number_in_interval(Inter2,0))
+ ->
+ % Le 0 de Val2 copie Val1
+ % Inutile de continuer
+ true
+ ; ((Inter1 = [I1],
+ Inter2 = [I2])
+ ->
+ binop_intervals_Rel(Rel12,minus,I1,I2,NMin,NMax),
+ % minus_intervals(I1,I2,NMin,NMax),
+ LInter = [NMin..NMax]
+ ; L1 is length(Inter1),
+ L2 is length(Inter2),
+ getval(max_prod_intervals,MaxProd),
+ (L1*L2 > MaxProd ->
+ % On ne travaille que sur les bornes
+ % en gardant le trou autour de zero si il existe
+ mfd:dvar_range(Val1,Min1,Max1),
+ mfd:dvar_range(Val2,Min2,Max2),
+ keep_zero_hole(Inter1,Min1,Max1,NInter1),
+ keep_zero_hole(Inter2,Min2,Max2,NInter2)
+ ; NInter1 = Inter1,
+ NInter2 = Inter2),
+ mfd:dvar_range(Val,Min,Max),
+ minus_interval_list(Rel12,Delta,NInter1,NInter2,Min,Max,NewInter1,NewInter2,LInter,NDelta),
+ (Rel12 \== ? ->
+ list_to_intervals(integer,NewInter1,NLInter1),
+ mfd:quiet_set_intervals(Val1,NLInter1),
+ list_to_intervals(integer,NewInter2,NLInter2),
+ mfd:quiet_set_intervals(Val2,NLInter2),
+ launch_delta(Val1,Val2,'+',NDelta)
+ ; true)),
+ list_to_intervals(integer,LInter,InterMinus),
+ mfd:quiet_set_intervals(Val,InterMinus))),
+ congr_add_inverse(Val1,Val2,Val).
:- mode(minus_intervals(++,++,-,-)).
minus_intervals(ValInter1,ValInter2,B1,B2) :-
- ((integer(ValInter1),
- integer(ValInter2))
- ->
- B1 is ValInter1 - ValInter2,
- B2 = B1
- ; min_max_inter(ValInter1,Min1,Max1),
- min_max_inter(ValInter2,Min2,Max2),
- B1 is Min1 - Max2,
- B2 is Max1 - Min2).
+ ((integer(ValInter1),
+ integer(ValInter2))
+ ->
+ B1 is ValInter1 - ValInter2,
+ B2 = B1
+ ; min_max_inter(ValInter1,Min1,Max1),
+ min_max_inter(ValInter2,Min2,Max2),
+ B1 is Min1 - Max2,
+ B2 is Max1 - Min2).
minus_interval_list(?,?,LI1,LI2,MinInt,MaxInt,LI1,LI2,LI,?) :- !,
- minus_interval_list(LI1,LI2,MinInt,MaxInt,LI).
+ minus_interval_list(LI1,LI2,MinInt,MaxInt,LI).
minus_interval_list(Rel12,Delta,LI1,LI2,MinInt,MaxInt,NewLI1,NewLI2,LI,NL..NH) :-
- min_max_inter(Delta,L,H),
- binop_interval_list_delta(minus,Rel12,Delta,LI1,LI2,NewLI1,NewLI2,LI,H..L,NL..NH).
+ min_max_inter(Delta,L,H),
+ binop_interval_list_delta(minus,Rel12,Delta,LI1,LI2,NewLI1,NewLI2,LI,H..L,NL..NH).
%% On peut abandonner des qu'on calcule un intervalle
%% contenant MinInt .. MaxInt
minus_interval_list(LI1,LI2,MinInt,MaxInt,LI) :-
- block(
- minus_interval_list1(LI1,LI2,MinInt,MaxInt,LI),
- included_interval,
- (interval_from_bounds(MinInt,MaxInt,Inter),
- LI = [Inter])).
+ block(
+ minus_interval_list1(LI1,LI2,MinInt,MaxInt,LI),
+ included_interval,
+ (interval_from_bounds(MinInt,MaxInt,Inter),
+ LI = [Inter])).
:- mode(minus_interval_list1(++,++,++,++,-)).
minus_interval_list1([],_,_,_,[]).
minus_interval_list1([I1|LI1],LI2,MinInt,MaxInt,LI) :-
- min_max_inter(I1,Min1,Max1),
- minus_interval_list_bis(Min1,Max1,LI2,MinInt,MaxInt,_,LastTooBig,LI,ELI),
- (nonvar(LastTooBig) ->
- %% On a echoue sur le dernier de LI2 avec
- %% un intervalle trop grand.
- %% Inutile de continuer sur LI1 car les intervalles sont
- %% classes par ordre croissant, donc on restera au dessus de MaxInt
- %% pour les autres intervalles de LI1
- ELI = []
- ; minus_interval_list1(LI1,LI2,MinInt,MaxInt,ELI)).
+ min_max_inter(I1,Min1,Max1),
+ minus_interval_list_bis(Min1,Max1,LI2,MinInt,MaxInt,_,LastTooBig,LI,ELI),
+ (nonvar(LastTooBig) ->
+ % On a echoue sur le dernier de LI2 avec
+ % un intervalle trop grand.
+ % Inutile de continuer sur LI1 car les intervalles sont
+ % classes par ordre croissant, donc on restera au dessus de MaxInt
+ % pour les autres intervalles de LI1
+ ELI = []
+ ; minus_interval_list1(LI1,LI2,MinInt,MaxInt,ELI)).
:- mode(minus_interval_list_bis(++,++,++,++,++,?,?,?,?)).
minus_interval_list_bis(_,_,[],_,_,LastTooBig,LastTooBig,LI,LI).
minus_interval_list_bis(Min1,Max1,[I2|LI2],MinInt,MaxInt,_,LastTooBig,LI,ELI) :-
- min_max_inter(I2,Min2,Max2),
- Min is Min1 - Max2,
- (Min > MaxInt ->
- %% Trop grand: on continue dans LI2
- %% Si on est sur le dernier de LI2 on pourra
- %% abandonner le parcours de LI1
- TooBig = 1,
- minus_interval_list_bis(Min1,Max1,LI2,MinInt,MaxInt,TooBig,LastTooBig,LI,ELI)
- ; Max is Max1 - Min2,
- (Max < MinInt ->
- %% Trop petit: pas la peine de continuer dans LI2
- ELI = LI
- ; check_included(MinInt,MaxInt,Min,Max),
- interval_from_bounds(Min,Max,I),
- LI = [I|NLI],
- minus_interval_list_bis(Min1,Max1,LI2,MinInt,MaxInt,_,LastTooBig,NLI,ELI))).
+ min_max_inter(I2,Min2,Max2),
+ Min is Min1 - Max2,
+ (Min > MaxInt ->
+ % Trop grand: on continue dans LI2
+ % Si on est sur le dernier de LI2 on pourra
+ % abandonner le parcours de LI1
+ TooBig = 1,
+ minus_interval_list_bis(Min1,Max1,LI2,MinInt,MaxInt,TooBig,LastTooBig,LI,ELI)
+ ; Max is Max1 - Min2,
+ (Max < MinInt ->
+ % Trop petit: pas la peine de continuer dans LI2
+ ELI = LI
+ ; check_included(MinInt,MaxInt,Min,Max),
+ interval_from_bounds(Min,Max,I),
+ LI = [I|NLI],
+ minus_interval_list_bis(Min1,Max1,LI2,MinInt,MaxInt,_,LastTooBig,NLI,ELI))).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -2553,204 +2553,204 @@ check_zero_and_div_interval_mult(Val1,Val2,Val) :-
%% Puis intersection du domaine calcule
%% avec celui de la variable resultat (Val)
div_interval(DivMult,Val1,Val2,Val) :-
- (integer(Val) ->
- true
- ; update_args_from_delta(Rel12,Delta,Val1,Val2),
- mfd:get_intervals(Val1,Inter1),
- mfd:get_intervals(Val2,Inter2),
+ (integer(Val) ->
+ true
+ ; update_args_from_delta(Rel12,Delta,Val1,Val2),
+ mfd:get_intervals(Val1,Inter1),
+ mfd:get_intervals(Val2,Inter2),
mfd:get_intervals(Val,Inter),
- ((Inter1 == Inter,
- number_in_interval(Inter2,1))
- ->
- %% Le 1 de Inter2 copie Inter1 dans Inter
- %% Inutile de continuer
- true
- ; interval_range(Inter,Min,Max),
- ((Inter1 = [I1],
- Inter2 = [I2])
- ->
- (Min >= 0 ->
- %% Seules les variantes positives nous interessent
- split_neg_pos(Inter1,Neg1,Pos1,Zero_in_arg),
- split_neg_pos(Inter2,Neg2,Pos2,_),
- ((Neg1 == [];
- Neg2 == [])
- ->
- EndLInter = []
- ; Neg1 = [INeg1],Neg2 = [INeg2],
- binop_intervals_Rel(Rel12,DivMult,INeg1,INeg2,LN,HN),
- EndLInter = [LN..HN]),
- ((Pos1 == [];
- Pos2 == [])
- ->
- NEndLInter = EndLInter
- ; Pos1 = [IPos1],Pos2 = [IPos2],
- binop_intervals_Rel(Rel12,DivMult,IPos1,IPos2,LP,HP),
- NEndLInter = [LP..HP|EndLInter]),
- (nonvar(Zero_in_arg) ->
- LInter = [0|NEndLInter]
- ; LInter = NEndLInter)
- ; (Max =< 0 ->
- %% Seules les variantes negatives nous interessent
- split_neg_pos(Inter1,Neg1,Pos1,Zero_in_arg),
- split_neg_pos(Inter2,Neg2,Pos2,_),
- ((Neg1 == [];
- Pos2 == [])
- ->
- EndLInter = []
- ; Neg1 = [INeg1],Pos2 = [IPos2],
- binop_intervals_Rel(Rel12,DivMult,INeg1,IPos2,LN,HN),
- EndLInter = [LN..HN]),
- ((Pos1 == [];
- Neg2 == [])
- ->
- NEndLInter = EndLInter
- ; Pos1 = [IPos1],Neg2 = [INeg2],
- binop_intervals_Rel(Rel12,DivMult,IPos1,INeg2,LP,HP),
- NEndLInter = [LP..HP|EndLInter]),
- (nonvar(Zero_in_arg) ->
- LInter = [0|NEndLInter]
- ; LInter = NEndLInter)
- ; binop_intervals_Rel(Rel12,DivMult,I1,I2,L,H),
- %% div_intervals(DivMult,I1,I2,NInter),
- LInter = [L..H]))
- ; L1 is length(Inter1),
- L2 is length(Inter2),
- getval(max_prod_intervals,MaxProd),
- (L1*L2 > MaxProd ->
- %% On ne travaille que sur les bornes
- %% en gardant le trou eventuel autour de 0
- mfd:dvar_range(Val1,Min1,Max1),
- mfd:dvar_range(Val2,Min2,Max2),
- keep_zero_hole(Inter1,Min1,Max1,NInter1),
- keep_zero_hole(Inter2,Min2,Max2,NInter2)
- ; NInter1 = Inter1,
- NInter2 = Inter2),
- (Rel12 \== '?' ->
- %% On peut se limiter aux associations d'intervalles compatibles
- %% avec le delta, reduire ces intervalles selon le delta
- %% et synthetiser un delta a partir de ces intervalles
- (Min >= 0 ->
- %% Seules les variantes positives nous interessent
- %% Exemple: [A,B,C] #: -1000 .. 1000, gt(C, 0), lt(A, B), div_mod(A, B, C,_).
- %% -->
- %%
- split_neg_pos(NInter1,Neg1,Pos1,Zero_in_arg),
- split_neg_pos(NInter2,Neg2,Pos2,_),
- binop_interval_list_delta(DivMult,Rel12,Delta,Neg1,Neg2,NNeg1,NNeg2,LInterP1,Delta1),
- binop_interval_list_delta(DivMult,Rel12,Delta,Pos1,Pos2,NPos1,NPos2,LInterP2,Delta2),
- min_max_inter(Delta1,LD1,HD1),min_max_inter(Delta2,LD2,HD2),
- min(LD1,LD2,Low),max(HD1,HD2,High),
- NDelta = Low..High,
- append(NNeg2,NPos2,NNInter2),
- (var(Zero_in_arg) ->
- append(NNeg1,NPos1,NNInter1),
- append(LInterP1,LInterP2,LInter)
- ; append(NNeg1,[0|NPos1],NNInter1),
- append(LInterP1,[0|LInterP2],LInter))
- ; (Max =< 0 ->
- %% Seules les variantes negatives nous interessent
- %% Exemple: [A,B,C] #: -1000 .. 1000, lt(C, 0), lt(A, B), div_mod(A, B, C,_).
- %% -->
- %%
- split_neg_pos(NInter1,Neg1,Pos1,Zero_in_arg),
- split_neg_pos(NInter2,Neg2,Pos2,_),
- binop_interval_list_delta(DivMult,Rel12,Delta,Neg1,Pos2,NNeg1,NPos2,LInterN1,Delta1),
- binop_interval_list_delta(DivMult,Rel12,Delta,Pos1,Neg2,NPos1,NNeg2,LInterN2,Delta2),
- min_max_inter(Delta1,LD1,HD1),min_max_inter(Delta2,LD2,HD2),
- min(LD1,LD2,Low),max(HD1,HD2,High),
- NDelta = Low..High,
- append(NNeg2,NPos2,NNInter2),
- (var(Zero_in_arg) ->
- append(NNeg1,NPos1,NNInter1),
- append(LInterN1,LInterN2,LInter)
- ; append(NNeg1,[0|NPos1],NNInter1),
- append(LInterN1,[0|LInterN2],LInter))
- ; binop_interval_list_delta(DivMult,Rel12,Delta,NInter1,NInter2,NNInter1,NNInter2,LInter,NDelta))),
- list_to_intervals(integer,NNInter1,NewInter1),
- mfd:quiet_set_intervals(Val1,NewInter1),
- list_to_intervals(integer,NNInter2,NewInter2),
- mfd:quiet_set_intervals(Val2,NewInter2),
- launch_delta(Val1,Val2,'+',NDelta)
- ; (Min >= 0 ->
- % Seules les variantes positives nous interessent
- split_neg_pos(NInter1,NegL1,PosL1,Zero_in_arg),
- split_neg_pos(NInter2,NegL2,PosL2,_),
- div_interval_list_nn(DivMult,NegL1,NegL2,Min,Max,LInterP1),
- div_interval_list_pp(DivMult,PosL1,PosL2,Min,Max,LInterP2),
- (nonvar(Zero_in_arg) ->
- append([0|LInterP1],LInterP2,LInter)
- ; append(LInterP1,LInterP2,LInter))
- ; (Max =< 0 ->
- %% Seules les variantes negatives nous interessent
- split_neg_pos(NInter1,NegL1,PosL1,Zero_in_arg),
- split_neg_pos(NInter2,NegL2,PosL2,_),
- div_interval_list_np(DivMult,NegL1,PosL2,Min,Max,LInterN1),
- div_interval_list_pn(DivMult,PosL1,NegL2,Min,Max,LInterN2),
- (nonvar(Zero_in_arg) ->
- append([0|LInterN1],LInterN2,LInter)
- ; append(LInterN1,LInterN2,LInter))
- ; %% On calcule tout
- div_interval_list(DivMult,NInter1,NInter2,LInter))))),
- mfd:list_to_dom(LInter,dom(InterDiv)),
- mfd:quiet_set_intervals(Val,InterDiv))).
+ ((Inter1 == Inter,
+ number_in_interval(Inter2,1))
+ ->
+ % Le 1 de Inter2 copie Inter1 dans Inter
+ % Inutile de continuer
+ true
+ ; interval_range(Inter,Min,Max),
+ ((Inter1 = [I1],
+ Inter2 = [I2])
+ ->
+ (Min >= 0 ->
+ % Seules les variantes positives nous interessent
+ split_neg_pos(Inter1,Neg1,Pos1,Zero_in_arg),
+ split_neg_pos(Inter2,Neg2,Pos2,_),
+ ((Neg1 == [];
+ Neg2 == [])
+ ->
+ EndLInter = []
+ ; Neg1 = [INeg1],Neg2 = [INeg2],
+ binop_intervals_Rel(Rel12,DivMult,INeg1,INeg2,LN,HN),
+ EndLInter = [LN..HN]),
+ ((Pos1 == [];
+ Pos2 == [])
+ ->
+ NEndLInter = EndLInter
+ ; Pos1 = [IPos1],Pos2 = [IPos2],
+ binop_intervals_Rel(Rel12,DivMult,IPos1,IPos2,LP,HP),
+ NEndLInter = [LP..HP|EndLInter]),
+ (nonvar(Zero_in_arg) ->
+ LInter = [0|NEndLInter]
+ ; LInter = NEndLInter)
+ ; (Max =< 0 ->
+ % Seules les variantes negatives nous interessent
+ split_neg_pos(Inter1,Neg1,Pos1,Zero_in_arg),
+ split_neg_pos(Inter2,Neg2,Pos2,_),
+ ((Neg1 == [];
+ Pos2 == [])
+ ->
+ EndLInter = []
+ ; Neg1 = [INeg1],Pos2 = [IPos2],
+ binop_intervals_Rel(Rel12,DivMult,INeg1,IPos2,LN,HN),
+ EndLInter = [LN..HN]),
+ ((Pos1 == [];
+ Neg2 == [])
+ ->
+ NEndLInter = EndLInter
+ ; Pos1 = [IPos1],Neg2 = [INeg2],
+ binop_intervals_Rel(Rel12,DivMult,IPos1,INeg2,LP,HP),
+ NEndLInter = [LP..HP|EndLInter]),
+ (nonvar(Zero_in_arg) ->
+ LInter = [0|NEndLInter]
+ ; LInter = NEndLInter)
+ ; binop_intervals_Rel(Rel12,DivMult,I1,I2,L,H),
+ % div_intervals(DivMult,I1,I2,NInter),
+ LInter = [L..H]))
+ ; L1 is length(Inter1),
+ L2 is length(Inter2),
+ getval(max_prod_intervals,MaxProd),
+ (L1*L2 > MaxProd ->
+ % On ne travaille que sur les bornes
+ % en gardant le trou eventuel autour de 0
+ mfd:dvar_range(Val1,Min1,Max1),
+ mfd:dvar_range(Val2,Min2,Max2),
+ keep_zero_hole(Inter1,Min1,Max1,NInter1),
+ keep_zero_hole(Inter2,Min2,Max2,NInter2)
+ ; NInter1 = Inter1,
+ NInter2 = Inter2),
+ (Rel12 \== '?' ->
+ % On peut se limiter aux associations d'intervalles compatibles
+ % avec le delta, reduire ces intervalles selon le delta
+ % et synthetiser un delta a partir de ces intervalles
+ (Min >= 0 ->
+ % Seules les variantes positives nous interessent
+ % Exemple: [A,B,C] #: -1000 .. 1000, gt(C, 0), lt(A, B), div_mod(A, B, C,_).
+ % -->
+ %
+ split_neg_pos(NInter1,Neg1,Pos1,Zero_in_arg),
+ split_neg_pos(NInter2,Neg2,Pos2,_),
+ binop_interval_list_delta(DivMult,Rel12,Delta,Neg1,Neg2,NNeg1,NNeg2,LInterP1,Delta1),
+ binop_interval_list_delta(DivMult,Rel12,Delta,Pos1,Pos2,NPos1,NPos2,LInterP2,Delta2),
+ min_max_inter(Delta1,LD1,HD1),min_max_inter(Delta2,LD2,HD2),
+ min(LD1,LD2,Low),max(HD1,HD2,High),
+ NDelta = Low..High,
+ append(NNeg2,NPos2,NNInter2),
+ (var(Zero_in_arg) ->
+ append(NNeg1,NPos1,NNInter1),
+ append(LInterP1,LInterP2,LInter)
+ ; append(NNeg1,[0|NPos1],NNInter1),
+ append(LInterP1,[0|LInterP2],LInter))
+ ; (Max =< 0 ->
+ % Seules les variantes negatives nous interessent
+ % Exemple: [A,B,C] #: -1000 .. 1000, lt(C, 0), lt(A, B), div_mod(A, B, C,_).
+ % -->
+ %
+ split_neg_pos(NInter1,Neg1,Pos1,Zero_in_arg),
+ split_neg_pos(NInter2,Neg2,Pos2,_),
+ binop_interval_list_delta(DivMult,Rel12,Delta,Neg1,Pos2,NNeg1,NPos2,LInterN1,Delta1),
+ binop_interval_list_delta(DivMult,Rel12,Delta,Pos1,Neg2,NPos1,NNeg2,LInterN2,Delta2),
+ min_max_inter(Delta1,LD1,HD1),min_max_inter(Delta2,LD2,HD2),
+ min(LD1,LD2,Low),max(HD1,HD2,High),
+ NDelta = Low..High,
+ append(NNeg2,NPos2,NNInter2),
+ (var(Zero_in_arg) ->
+ append(NNeg1,NPos1,NNInter1),
+ append(LInterN1,LInterN2,LInter)
+ ; append(NNeg1,[0|NPos1],NNInter1),
+ append(LInterN1,[0|LInterN2],LInter))
+ ; binop_interval_list_delta(DivMult,Rel12,Delta,NInter1,NInter2,NNInter1,NNInter2,LInter,NDelta))),
+ list_to_intervals(integer,NNInter1,NewInter1),
+ mfd:quiet_set_intervals(Val1,NewInter1),
+ list_to_intervals(integer,NNInter2,NewInter2),
+ mfd:quiet_set_intervals(Val2,NewInter2),
+ launch_delta(Val1,Val2,'+',NDelta)
+ ; (Min >= 0 ->
+ % Seules les variantes positives nous interessent
+ split_neg_pos(NInter1,NegL1,PosL1,Zero_in_arg),
+ split_neg_pos(NInter2,NegL2,PosL2,_),
+ div_interval_list_nn(DivMult,NegL1,NegL2,Min,Max,LInterP1),
+ div_interval_list_pp(DivMult,PosL1,PosL2,Min,Max,LInterP2),
+ (nonvar(Zero_in_arg) ->
+ append([0|LInterP1],LInterP2,LInter)
+ ; append(LInterP1,LInterP2,LInter))
+ ; (Max =< 0 ->
+ % Seules les variantes negatives nous interessent
+ split_neg_pos(NInter1,NegL1,PosL1,Zero_in_arg),
+ split_neg_pos(NInter2,NegL2,PosL2,_),
+ div_interval_list_np(DivMult,NegL1,PosL2,Min,Max,LInterN1),
+ div_interval_list_pn(DivMult,PosL1,NegL2,Min,Max,LInterN2),
+ (nonvar(Zero_in_arg) ->
+ append([0|LInterN1],LInterN2,LInter)
+ ; append(LInterN1,LInterN2,LInter))
+ ; % On calcule tout
+ div_interval_list(DivMult,NInter1,NInter2,LInter))))),
+ mfd:list_to_dom(LInter,dom(InterDiv)),
+ mfd:quiet_set_intervals(Val,InterDiv))).
:- mode(div_intervals(++,++,++,-)).
div_intervals(div_mult,ValInter1,ValInter2,Inter) :-
- div_intervals_mult(ValInter1,ValInter2,Inter).
+ div_intervals_mult(ValInter1,ValInter2,Inter).
div_intervals(div,ValInter1,ValInter2,Inter) :-
- div_intervals_div(ValInter1,ValInter2,Inter).
+ div_intervals_div(ValInter1,ValInter2,Inter).
%% Division entiere normale
:- mode(div_intervals_div(++,++,-)).
div_intervals_div(ValInter1,ValInter2,Inter) :-
- %% 0 est interdit dans ValInter2
- (integer(ValInter1) ->
- (ValInter1 == 0 ->
- Inter = 0
- ; (integer(ValInter2) ->
- Inter is ValInter1 // ValInter2
- ; ValInter2 = Min2..Max2,
- B1 is ValInter1 // Min2,
- B2 is ValInter1 // Max2,
- sort_bounds(B1,B2,Inter)))
- ; ValInter1 = Min1..Max1,
- (integer(ValInter2) ->
- B1 is Min1 // ValInter2,
- B2 is Max1 // ValInter2,
- sort_bounds(B1,B2,Inter)
- ; ValInter2 = Min2..Max2,
- (Min1 >= 0 ->
- (Min2 >= 1 ->
- %% Inter >= 0
- B1 is Min1 // Max2,
- B2 is Max1 // Min2
- ; %% Max2 =< -1,
- %% Inter =< 0
- B1 is Max1 // Max2,
- B2 is Min1 // Min2)
- ; (Max1 =< 0 ->
- (Min2 >= 1 ->
- %% Inter =< 0
- B1 is Min1 // Min2,
- B2 is Max1 // Max2
- ; %% Max2 =< -1,
- %% Inter >= 0
- B1 is Max1 // Min2,
- B2 is Min1 // Max2)
- ; %% Min1..0..Max1
- (Min2 >= 1 ->
- B1 is Min1 // Min2,
- B2 is Max1 // Min2
- ; %% Max2 =< -1,
- B1 is Max1 // Max2,
- B2 is Min1 // Max2))),
- sort_bounds(B1,B2,Inter))).
+ % 0 est interdit dans ValInter2
+ (integer(ValInter1) ->
+ (ValInter1 == 0 ->
+ Inter = 0
+ ; (integer(ValInter2) ->
+ Inter is ValInter1 // ValInter2
+ ; ValInter2 = Min2..Max2,
+ B1 is ValInter1 // Min2,
+ B2 is ValInter1 // Max2,
+ sort_bounds(B1,B2,Inter)))
+ ; ValInter1 = Min1..Max1,
+ (integer(ValInter2) ->
+ B1 is Min1 // ValInter2,
+ B2 is Max1 // ValInter2,
+ sort_bounds(B1,B2,Inter)
+ ; ValInter2 = Min2..Max2,
+ (Min1 >= 0 ->
+ (Min2 >= 1 ->
+ % Inter >= 0
+ B1 is Min1 // Max2,
+ B2 is Max1 // Min2
+ ; % Max2 =< -1,
+ % Inter =< 0
+ B1 is Max1 // Max2,
+ B2 is Min1 // Min2)
+ ; (Max1 =< 0 ->
+ (Min2 >= 1 ->
+ % Inter =< 0
+ B1 is Min1 // Min2,
+ B2 is Max1 // Max2
+ ; % Max2 =< -1,
+ % Inter >= 0
+ B1 is Max1 // Min2,
+ B2 is Min1 // Max2)
+ ; % Min1..0..Max1
+ (Min2 >= 1 ->
+ B1 is Min1 // Min2,
+ B2 is Max1 // Min2
+ ; % Max2 =< -1,
+ B1 is Max1 // Max2,
+ B2 is Min1 // Max2))),
+ sort_bounds(B1,B2,Inter))).
sort_bounds(B1,B2,Inter) :-
- (B2 < B1 ->
- interval_from_bounds(B2,B1,Inter)
- ; interval_from_bounds(B1,B2,Inter)).
+ (B2 < B1 ->
+ interval_from_bounds(B2,B1,Inter)
+ ; interval_from_bounds(B1,B2,Inter)).
%% Inversion d'une multiplication entiere.
@@ -2758,150 +2758,150 @@ sort_bounds(B1,B2,Inter) :-
%% (les autres projections font ce travail la)
:- mode(div_intervals_mult(++,++,-)).
div_intervals_mult(ValInter1,ValInter2,Inter) :-
- %% 0 est interdit dans ValInter2
- %% donc ValInter2 est signe
- (integer(ValInter1) ->
- (ValInter1 == 0 ->
- Inter = 0
- ; (integer(ValInter2) ->
- Inter is ValInter1 // ValInter2,
- %% Ca doit tomber juste
- ValInter1 is Inter * ValInter2
- ; ValInter2 = Min2..Max2,
- div_intervals_mult2(ValInter1,ValInter1,Min2,Max2,Inter)))
- ; ValInter1 = Min1..Max1,
- (integer(ValInter2) ->
- div_intervals_mult2(Min1,Max1,ValInter2,ValInter2,Inter)
- ; ValInter2 = Min2..Max2,
- div_intervals_mult2(Min1,Max1,Min2,Max2,Inter))).
+ % 0 est interdit dans ValInter2
+ % donc ValInter2 est signe
+ (integer(ValInter1) ->
+ (ValInter1 == 0 ->
+ Inter = 0
+ ; (integer(ValInter2) ->
+ Inter is ValInter1 // ValInter2,
+ % Ca doit tomber juste
+ ValInter1 is Inter * ValInter2
+ ; ValInter2 = Min2..Max2,
+ div_intervals_mult2(ValInter1,ValInter1,Min2,Max2,Inter)))
+ ; ValInter1 = Min1..Max1,
+ (integer(ValInter2) ->
+ div_intervals_mult2(Min1,Max1,ValInter2,ValInter2,Inter)
+ ; ValInter2 = Min2..Max2,
+ div_intervals_mult2(Min1,Max1,Min2,Max2,Inter))).
div_intervals_mult2(Min1,Max1,Min2,Max2,Inter) :-
- (Min1 >= 0 ->
- (Min2 >= 1 ->
- %% pos // pos -> pos
- div_intervals_mult2(ppp,Min1,Max1,Min2,Max2,Min,Max)
- ; %% Max2 =< -1,
- %% pos // neg -> neg
- div_intervals_mult2(pnn,Min1,Max1,Min2,Max2,Min,Max))
- ; (Max1 =< 0 ->
- (Min2 >= 1 ->
- %% neg // pos -> neq
- div_intervals_mult2(npn,Min1,Max1,Min2,Max2,Min,Max)
- ; %% Max2 =< -1,
- %% neg // neg -> pos
- div_intervals_mult2(nnp,Min1,Max1,Min2,Max2,Min,Max))
- ; %% Min1..0..Max1
- (Min2 >= 1 ->
- %% ?? // pos -> ??
- Min is Min1 // Min2,
- Max is Max1 // Min2
- ; %% Max2 =< -1,
- %% ?? // neg -> op(??)
- Min is Max1 // Max2,
- Max is Min1 // Max2))),
- Min =< Max,
- interval_from_bounds(Min,Max,Inter).
+ (Min1 >= 0 ->
+ (Min2 >= 1 ->
+ % pos // pos -> pos
+ div_intervals_mult2(ppp,Min1,Max1,Min2,Max2,Min,Max)
+ ; % Max2 =< -1,
+ % pos // neg -> neg
+ div_intervals_mult2(pnn,Min1,Max1,Min2,Max2,Min,Max))
+ ; (Max1 =< 0 ->
+ (Min2 >= 1 ->
+ % neg // pos -> neq
+ div_intervals_mult2(npn,Min1,Max1,Min2,Max2,Min,Max)
+ ; % Max2 =< -1,
+ % neg // neg -> pos
+ div_intervals_mult2(nnp,Min1,Max1,Min2,Max2,Min,Max))
+ ; % Min1..0..Max1
+ (Min2 >= 1 ->
+ % ?? // pos -> ??
+ Min is Min1 // Min2,
+ Max is Max1 // Min2
+ ; % Max2 =< -1,
+ % ?? // neg -> op(??)
+ Min is Max1 // Max2,
+ Max is Min1 // Max2))),
+ Min =< Max,
+ interval_from_bounds(Min,Max,Inter).
div_intervals_mult2(ppp,Min1,Max1,Min2,Max2,Min,Max) :-
- %% Min = Min1 / Max2
- %% Max = Max1 / Min2
- min_div_intervals_mult_ppp(Min1,Max2,Min),
- max_div_intervals_mult_ppp(Max1,Min2,Max).
+ % Min = Min1 / Max2
+ % Max = Max1 / Min2
+ min_div_intervals_mult_ppp(Min1,Max2,Min),
+ max_div_intervals_mult_ppp(Max1,Min2,Max).
div_intervals_mult2(pnn,Min1,Max1,Min2,Max2,Min,Max) :-
- %% Min = Max1 / Max2
- %% Max = Min1 / Min2
- min_div_intervals_mult_pnn(Max1,Max2,Min),
- max_div_intervals_mult_pnn(Min1,Min2,Max).
+ % Min = Max1 / Max2
+ % Max = Min1 / Min2
+ min_div_intervals_mult_pnn(Max1,Max2,Min),
+ max_div_intervals_mult_pnn(Min1,Min2,Max).
div_intervals_mult2(npn,Min1,Max1,Min2,Max2,Min,Max) :-
- %% Min = Min1 / Min2
- %% Max = Max1 / Max2
- min_div_intervals_mult_npn(Min1,Min2,Min),
- max_div_intervals_mult_npn(Max1,Max2,Max).
+ % Min = Min1 / Min2
+ % Max = Max1 / Max2
+ min_div_intervals_mult_npn(Min1,Min2,Min),
+ max_div_intervals_mult_npn(Max1,Max2,Max).
div_intervals_mult2(nnp,Min1,Max1,Min2,Max2,Min,Max) :-
- %% Min = Max1 / Min2
- %% Max = Min1 / Max2
- min_div_intervals_mult_nnp(Max1,Min2,Min),
- max_div_intervals_mult_nnp(Min1,Max2,Max).
+ % Min = Max1 / Min2
+ % Max = Min1 / Max2
+ min_div_intervals_mult_nnp(Max1,Min2,Min),
+ max_div_intervals_mult_nnp(Min1,Max2,Max).
min_div_intervals_mult_ppp(Min1,Max2,Min) :-
- Min0 is Min1 // Max2,
- %% Si pMin*pMax2 < pMin1,
- %% On ne peut pas augmenter Max2 ou diminuer Min1
- %% donc on peut augmenter Min
- (Min0*Max2 < Min1 ->
- Min is Min0 + 1
- ; Min = Min0).
+ Min0 is Min1 // Max2,
+ % Si pMin*pMax2 < pMin1,
+ % On ne peut pas augmenter Max2 ou diminuer Min1
+ % donc on peut augmenter Min
+ (Min0*Max2 < Min1 ->
+ Min is Min0 + 1
+ ; Min = Min0).
max_div_intervals_mult_ppp(Max1,Min2,Max) :-
- Max0 is Max1 // Min2,
- %% Si pMax*pMin2 > pMax1
- %% On ne peut pas diminuer Min2 ou augmenter Max1
- %% donc on peut diminuer Max
- (Max0*Min2 > Max1 ->
- Max is Max0 - 1
- ; Max = Max0).
+ Max0 is Max1 // Min2,
+ % Si pMax*pMin2 > pMax1
+ % On ne peut pas diminuer Min2 ou augmenter Max1
+ % donc on peut diminuer Max
+ (Max0*Min2 > Max1 ->
+ Max is Max0 - 1
+ ; Max = Max0).
%% p.n.n -> p.op(n).op(n)
min_div_intervals_mult_pnn(Max1,Max2,Min) :-
- OpMax2 is - Max2,
- max_div_intervals_mult_ppp(Max1,OpMax2,OpMin),
- Min is - OpMin.
+ OpMax2 is - Max2,
+ max_div_intervals_mult_ppp(Max1,OpMax2,OpMin),
+ Min is - OpMin.
max_div_intervals_mult_pnn(Min1,Min2,Max) :-
- OpMin2 is - Min2,
- min_div_intervals_mult_ppp(Min1,OpMin2,OpMax),
- Max is - OpMax.
+ OpMin2 is - Min2,
+ min_div_intervals_mult_ppp(Min1,OpMin2,OpMax),
+ Max is - OpMax.
%% n.p.n -> op(n).p.op(n)
min_div_intervals_mult_npn(Min1,Min2,Min) :-
- OpMin1 is - Min1,
- max_div_intervals_mult_ppp(OpMin1,Min2,OpMin),
- Min is - OpMin.
+ OpMin1 is - Min1,
+ max_div_intervals_mult_ppp(OpMin1,Min2,OpMin),
+ Min is - OpMin.
max_div_intervals_mult_npn(Max1,Max2,Max) :-
- OpMax1 is - Max1,
- min_div_intervals_mult_ppp(OpMax1,Max2,OpMax),
- Max is - OpMax.
+ OpMax1 is - Max1,
+ min_div_intervals_mult_ppp(OpMax1,Max2,OpMax),
+ Max is - OpMax.
%% n.n.n -> op(n).op(n).p
min_div_intervals_mult_nnp(Max1,Min2,Min) :-
- OpMax1 is - Max1,
- OpMin2 is - Min2,
- min_div_intervals_mult_ppp(OpMax1,OpMin2,Min).
+ OpMax1 is - Max1,
+ OpMin2 is - Min2,
+ min_div_intervals_mult_ppp(OpMax1,OpMin2,Min).
max_div_intervals_mult_nnp(Min1,Max2,Max) :-
- OpMin1 is - Min1,
- OpMax2 is - Max2,
- max_div_intervals_mult_ppp(OpMin1,OpMax2,Max).
+ OpMin1 is - Min1,
+ OpMax2 is - Max2,
+ max_div_intervals_mult_ppp(OpMin1,OpMax2,Max).
%% Decroissante vers +0, mais de plus en plus pour L1 (intervalles croissants)
:- mode(div_interval_list_pp(++,++,++,++,++,-)).
div_interval_list_pp(DivMult,LI1,LI2,MinInt,MaxInt,LI) :-
- block(
- div_interval_list_pp1(DivMult,LI1,LI2,MinInt,MaxInt,LI),
- included_interval,
- (interval_from_bounds(MinInt,MaxInt,Inter),
- LI = [Inter])
- ).
+ block(
+ div_interval_list_pp1(DivMult,LI1,LI2,MinInt,MaxInt,LI),
+ included_interval,
+ (interval_from_bounds(MinInt,MaxInt,Inter),
+ LI = [Inter])
+ ).
:- mode(div_interval_list_pp1(++,++,++,++,++,-)).
div_interval_list_pp1(div,LI1,LI2,MinInt,MaxInt,LI) :-
- div_interval_list_pp1_div(LI1,LI2,MinInt,MaxInt,LI).
+ div_interval_list_pp1_div(LI1,LI2,MinInt,MaxInt,LI).
div_interval_list_pp1(div_mult,LI1,LI2,MinInt,MaxInt,LI) :-
- div_interval_list_pp1_mult(LI1,LI2,MinInt,MaxInt,LI).
+ div_interval_list_pp1_mult(LI1,LI2,MinInt,MaxInt,LI).
:- mode(div_interval_list_pp1_div(++,++,++,++,-)).
div_interval_list_pp1_div([],_,_,_,[]).
div_interval_list_pp1_div([I1|LI1],LI2,MinInt,MaxInt,LI) :-
- min_max_inter(I1,Min1,Max1),
- div_interval_list_bis_pp_div(Min1,Max1,LI2,MinInt,MaxInt,_,LastTooBig,LI,ELI),
- (nonvar(LastTooBig) ->
- %% On a echoue sur le dernier de LI2 avec
- %% un intervalle trop grand.
- %% Inutile de continuer sur LI1 car les intervalles sont
- %% classes par ordre croissant, donc on restera au dessus de MaxInt
- %% pour les autres intervalles de LI1
- ELI = []
- ; div_interval_list_pp1_div(LI1,LI2,MinInt,MaxInt,ELI)).
+ min_max_inter(I1,Min1,Max1),
+ div_interval_list_bis_pp_div(Min1,Max1,LI2,MinInt,MaxInt,_,LastTooBig,LI,ELI),
+ (nonvar(LastTooBig) ->
+ % On a echoue sur le dernier de LI2 avec
+ % un intervalle trop grand.
+ % Inutile de continuer sur LI1 car les intervalles sont
+ % classes par ordre croissant, donc on restera au dessus de MaxInt
+ % pour les autres intervalles de LI1
+ ELI = []
+ ; div_interval_list_pp1_div(LI1,LI2,MinInt,MaxInt,ELI)).
:- mode(div_interval_list_bis_pp_div(++,++,++,++,++,?,?,?,?)).
@@ -3277,26 +3277,22 @@ div_interval_list_bis(DivMult,ValInter1,LInter2) :-
%% Par consequent R est du signe de A
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
div_mod(A, B, Q, R) :-
- get_priority(Prio),
- set_priority(1),
- div_mod0(A, B, Q, BQ, R),
- div_mod_int_bis(A, B, Q, BQ, R),
- lin_div_mod_int(A,B,Q,BQ,R),
- set_priority(Prio),
- wake_if_other_scheduled(Prio).
+ get_priority(Prio),
+ set_priority(1),
+ div_mod0(A, B, Q, BQ, R),
+ div_mod_int_bis(A, B, Q, BQ, R),
+ lin_div_mod_int(A,B,Q,BQ,R),
+ set_priority(Prio),
+ wake_if_other_scheduled(Prio).
-/*
-no_lin_div_mod(A, B, Q, R) :- !,
- div_mod(A, B, Q, R).
-*/
no_lin_div_mod(A, B, Q, R) :-
- get_priority(Prio),
- set_priority(1),
- div_mod0(A, B, Q, BQ, R),
- div_mod_int_bis(A, B, Q, BQ, R),
- set_priority(Prio),
- wake_if_other_scheduled(Prio).
+ get_priority(Prio),
+ set_priority(1),
+ div_mod0(A, B, Q, BQ, R),
+ div_mod_int_bis(A, B, Q, BQ, R),
+ set_priority(Prio),
+ wake_if_other_scheduled(Prio).
div_mod0(A, B, Q, BQ, R) :-
set_lazy_domain(int,A),
@@ -4028,75 +4024,76 @@ check_absA_lt_absB(A,B) :-
%% - Q > 0 alors A et B de meme signe
%% - Q < 0 alors A et B de signe oppose
%% - A > 0 et B > 0 et Q > 0 alors R >= 0 et BQ =< A
+%clean_div_mod_args(A, B, Q, BQ, R) :- !.
clean_div_mod_args(A, B, Q, BQ, R) :-
- %% Dans le cas B == Q on a A >= 0 (car Q est du signe de AB)
- %% et pas vraiment plus ? (il peut y avoir un reste)
- (B == Q ->
- mfd:dvar_remove_smaller(A,0)
- ; true),
- %% A <> R <=> Q <> 0
- (not_unify(A,R) ->
- %% On n'attend pas les projections pour propager Q <> 0
- mfd:dvar_remove_element(Q,0)
- ; (not_unify(Q,0) ->
- %% idem, A = BQ + R cree le delta '#'
- %% car BQ <> 0
- saturate_diff_int_inequalities(A,R,_)
- ; true)),
- %% R est borne par A et du meme signe
- (integer(A) ->
- (A >= 0 ->
- %% Le cas A = 0 est traite par div_mod_inst
- mfd:(R :: 0..A)
- ; mfd:(R :: A..0))
- ; mfd:dvar_range(A,MinA,MaxA),
- (integer(R) ->
- (R > 0 ->
- (MinA >= R ->
- true
- ; % R =< MaxA,
- mfd:dvar_remove_smaller(A,R))
- ; %% R < 0, le cas R = 0 est traite par div_mod_inst
- (MaxA =< R ->
- true
- ; % R >= MinA,
- mfd:dvar_remove_greater(A,R)))
- ; (MinA >= 0 ->
- mfd:(R :: 0..MaxA),
- %% A >= 0 donc A >= R
- launch_delta_leq(R,A)
- ; (MaxA =< 0 ->
- mfd:(R :: MinA..0),
- %% A =< 0 donc R >= A
- launch_delta_leq(A,R)
- ; Max is max(abs(MinA),abs(MaxA)),
- OpMax is -Max,
- mfd:(R :: OpMax..Max),
- %% si le signe de R est connu
- %% on donne le meme a A
- mfd:mindomain(R,MinR),
- (MinR >= 0 ->
- mfd:dvar_remove_smaller(A,0),
- %% A >= 0 donc A >= R
- launch_delta_leq(R,A)
- ; mfd:maxdomain(R,MaxR),
- (MaxR =< 0 ->
- mfd:dvar_remove_greater(A,0),
- %% A =< 0 donc R >= A
- launch_delta_leq(A,R)
- ; ((exists_delta_Rel(A,R,RelAR,_,_),
- RelAR \== '#')
- ->
- (occurs(RelAR,('<','=<')) ->
- %% R et A =< 0
- mfd:dvar_remove_greater(A,0),
- mfd:dvar_remove_greater(R,0)
- ; %% occurs(RelAR,('>','>=')) ->
- %% R et A >= 0
- mfd:dvar_remove_smaller(A,0),
- mfd:dvar_remove_smaller(R,0))
- ; true))))))),
- %% A > 0 et B > 0 et Q > 0 alors BQ =< A
+ % Dans le cas B == Q on a A >= 0 (car Q est du signe de AB)
+ % et pas vraiment plus ? (il peut y avoir un reste)
+ (B == Q ->
+ mfd:dvar_remove_smaller(A,0)
+ ; true),
+ % A <> R <=> Q <> 0
+ (not_unify(A,R) ->
+ % On n'attend pas les projections pour propager Q <> 0
+ mfd:dvar_remove_element(Q,0)
+ ; (not_unify(Q,0) ->
+ % idem, A = BQ + R cree le delta '#'
+ % car BQ <> 0
+ saturate_diff_int_inequalities(A,R,_)
+ ; true)),
+ % R est borne par A et du meme signe
+ (integer(A) ->
+ (A >= 0 ->
+ % Le cas A = 0 est traite par div_mod_inst
+ mfd:(R :: 0..A)
+ ; mfd:(R :: A..0))
+ ; mfd:dvar_range(A,MinA,MaxA),
+ (integer(R) ->
+ (R > 0 ->
+ (MinA >= R ->
+ true
+ ; % R =< MaxA,
+ mfd:dvar_remove_smaller(A,R))
+ ; % R < 0, le cas R = 0 est traite par div_mod_inst
+ (MaxA =< R ->
+ true
+ ; % R >= MinA,
+ mfd:dvar_remove_greater(A,R)))
+ ; (MinA >= 0 ->
+ mfd:(R :: 0..MaxA),
+ % A >= 0 donc A >= R
+ launch_delta_leq(R,A)
+ ; (MaxA =< 0 ->
+ mfd:(R :: MinA..0),
+ % A =< 0 donc R >= A
+ launch_delta_leq(A,R)
+ ; Max is max(abs(MinA),abs(MaxA)),
+ OpMax is -Max,
+ mfd:(R :: OpMax..Max),
+ % si le signe de R est connu
+ % on donne le meme a A
+ mfd:mindomain(R,MinR),
+ (MinR >= 0 ->
+ mfd:dvar_remove_smaller(A,0),
+ % A >= 0 donc A >= R
+ launch_delta_leq(R,A)
+ ; mfd:maxdomain(R,MaxR),
+ (MaxR =< 0 ->
+ mfd:dvar_remove_greater(A,0),
+ % A =< 0 donc R >= A
+ launch_delta_leq(A,R)
+ ; ((exists_delta_Rel(A,R,RelAR,_,_),
+ RelAR \== '#')
+ ->
+ (occurs(RelAR,('<','=<')) ->
+ % R et A =< 0
+ mfd:dvar_remove_greater(A,0),
+ mfd:dvar_remove_greater(R,0)
+ ; % occurs(RelAR,('>','>=')) ->
+ % R et A >= 0
+ mfd:dvar_remove_smaller(A,0),
+ mfd:dvar_remove_smaller(R,0))
+ ; true))))))),
+ % A > 0 et B > 0 et Q > 0 alors BQ =< A
((mfd:mindomain(A) > 0,
mfd:mindomain(B) > 0,
mfd:mindomain(Q) > 0)
@@ -4105,119 +4102,119 @@ clean_div_mod_args(A, B, Q, BQ, R) :-
launch_delta_leq(BQ,A),
lin_geq_int(A,BQ)
; true),
- %% |B| > |R|
- ensure_absA_lt_absB(R,B),
- adjust_sign_from_Q(Q,A,B,R).
+ % |B| > |R|
+ ensure_absA_lt_absB(R,B),
+ adjust_sign_from_Q(Q,A,B,R).
%% Si Q est < ou > a 0
%% on a des infos sur le signe de A, B et R
adjust_sign_from_Q(Q,A,B,R) :-
- mfd:mindomain(Q,MinQ),
- (MinQ > 0 ->
- %% Q positif donc A,R et B sont du meme signe
- mfd:mindomain(A,MinA),
- (MinA >= 0 ->
- %% A positif
- mfd:dvar_remove_smaller(B,0),
- launch_delta_leq(R,A)
- ; mfd:maxdomain(A,MaxA),
- (MaxA =< 0 ->
- %% A negatif
- mfd:dvar_remove_greater(B,0),
- launch_delta_leq(A,R)
- ; mfd:mindomain(B,MinB),
- (MinB >= 0 ->
- %% Q et B positifs donc A et R positifs
- mfd:dvar_remove_smaller(A,0),
- mfd:dvar_remove_smaller(R,0),
- launch_delta_leq(R,A)
- ; mfd:maxdomain(B,MaxB),
- (MaxB =< 0 ->
- %% Q positif et B negatif donc A et R negatifs
- mfd:dvar_remove_greater(A,0),
- mfd:dvar_remove_greater(R,0),
- launch_delta_leq(A,R)
- ; ((exists_delta_Rel(A,B,Rel,_,_),
- Rel \== '#')
- ->
- %% A < B et A positif => Q=0 -> fail
- %% donc A,R et B negatifs
- %% Pour A =< B et A positif => Q=1
- %% donc si Q > 1 alors A,R et B negatifs
- ((Rel == '<';
- Rel == '=<',
- MinQ > 1)
- ->
- mfd:dvar_remove_greater(A,0),
- mfd:dvar_remove_greater(R,0),
- mfd:dvar_remove_greater(B,0)
- ; %% A > B et A negatif => Q=0 -> fail
- %% donc A,R et B positifs
- %% Pour A >= B et A negatif => Q=1
- %% donc si Q > 1 alors A,R et B positifs
- ((Rel == '>';
- Rel == '>=',
- MinQ > 1)
- ->
- mfd:dvar_remove_smaller(A,0),
- mfd:dvar_remove_smaller(R,0),
- mfd:dvar_remove_smaller(B,0)
- ; true))
- ; true)))))
- ; mfd:maxdomain(Q,MaxQ),
- (MaxQ < 0 ->
- %% Q negatif donc A,R et B sont de signe opposes
- mfd:mindomain(A,MinA),
- (MinA >= 0 ->
- %% A positif
- mfd:dvar_remove_greater(B,0),
- launch_delta_leq(B,A),
- launch_delta_leq(R,A)
- ; mfd:maxdomain(A,MaxA),
- (MaxA =< 0 ->
- %% A negatif
- mfd:dvar_remove_smaller(B,0),
- launch_delta_leq(A,B),
- launch_delta_leq(A,R)
- ; mfd:mindomain(B,MinB),
- (MinB >= 0 ->
- %% B positif
- mfd:dvar_remove_greater(A,0),
- launch_delta_leq(A,B),
- mfd:dvar_remove_greater(R,0),
- launch_delta_leq(A,R)
- ; mfd:maxdomain(B,MaxB),
- (MaxB =< 0 ->
- %% B negatif
- mfd:dvar_remove_smaller(A,0),
- launch_delta_leq(B,A),
- mfd:dvar_remove_smaller(R,0),
- launch_delta_leq(R,A)
- ; (((exists_delta_Rel(A,B,Rel,_,_);
- exists_delta_Rel(R,B,Rel,_,_)),
- Rel \== '#')
- ->
- %% A|R et B sont ordonnes donc
- %% on peut deduire leur signe et celui de R
- (occurs(Rel,('=<','<')) ->
- %% A et R negatifs, B positifs
- mfd:dvar_remove_greater(A,0),
- mfd:dvar_remove_greater(R,0),
- mfd:dvar_remove_smaller(B,0)
- ; %% occurs(Rel,('>=','>'))
- %% A et R positifs, B negatif
- mfd:dvar_remove_smaller(A,0),
- mfd:dvar_remove_smaller(R,0),
- mfd:dvar_remove_greater(B,0))
- ; true)))))
- ; true)).
+ mfd:mindomain(Q,MinQ),
+ (MinQ > 0 ->
+ % Q positif donc A,R et B sont du meme signe
+ mfd:mindomain(A,MinA),
+ (MinA >= 0 ->
+ % A positif
+ mfd:dvar_remove_smaller(B,0),
+ launch_delta_leq(R,A)
+ ; mfd:maxdomain(A,MaxA),
+ (MaxA =< 0 ->
+ % A negatif
+ mfd:dvar_remove_greater(B,0),
+ launch_delta_leq(A,R)
+ ; mfd:mindomain(B,MinB),
+ (MinB >= 0 ->
+ % Q et B positifs donc A et R positifs
+ mfd:dvar_remove_smaller(A,0),
+ mfd:dvar_remove_smaller(R,0),
+ launch_delta_leq(R,A)
+ ; mfd:maxdomain(B,MaxB),
+ (MaxB =< 0 ->
+ % Q positif et B negatif donc A et R negatifs
+ mfd:dvar_remove_greater(A,0),
+ mfd:dvar_remove_greater(R,0),
+ launch_delta_leq(A,R)
+ ; ((exists_delta_Rel(A,B,Rel,_,_),
+ Rel \== '#')
+ ->
+ % A < B et A positif => Q=0 -> fail
+ % donc A,R et B negatifs
+ % Pour A =< B et A positif => Q=1
+ % donc si Q > 1 alors A,R et B negatifs
+ ((Rel == '<';
+ Rel == '=<',
+ MinQ > 1)
+ ->
+ mfd:dvar_remove_greater(A,0),
+ mfd:dvar_remove_greater(R,0),
+ mfd:dvar_remove_greater(B,0)
+ ; % A > B et A negatif => Q=0 -> fail
+ % donc A,R et B positifs
+ % Pour A >= B et A negatif => Q=1
+ % donc si Q > 1 alors A,R et B positifs
+ ((Rel == '>';
+ Rel == '>=',
+ MinQ > 1)
+ ->
+ mfd:dvar_remove_smaller(A,0),
+ mfd:dvar_remove_smaller(R,0),
+ mfd:dvar_remove_smaller(B,0)
+ ; true))
+ ; true)))))
+ ; mfd:maxdomain(Q,MaxQ),
+ (MaxQ < 0 ->
+ % Q negatif donc A,R et B sont de signe opposes
+ mfd:mindomain(A,MinA),
+ (MinA >= 0 ->
+ % A positif
+ mfd:dvar_remove_greater(B,0),
+ launch_delta_leq(B,A),
+ launch_delta_leq(R,A)
+ ; mfd:maxdomain(A,MaxA),
+ (MaxA =< 0 ->
+ % A negatif
+ mfd:dvar_remove_smaller(B,0),
+ launch_delta_leq(A,B),
+ launch_delta_leq(A,R)
+ ; mfd:mindomain(B,MinB),
+ (MinB >= 0 ->
+ % B positif
+ mfd:dvar_remove_greater(A,0),
+ launch_delta_leq(A,B),
+ mfd:dvar_remove_greater(R,0),
+ launch_delta_leq(A,R)
+ ; mfd:maxdomain(B,MaxB),
+ (MaxB =< 0 ->
+ % B negatif
+ mfd:dvar_remove_smaller(A,0),
+ launch_delta_leq(B,A),
+ mfd:dvar_remove_smaller(R,0),
+ launch_delta_leq(R,A)
+ ; (((exists_delta_Rel(A,B,Rel,_,_);
+ exists_delta_Rel(R,B,Rel,_,_)),
+ Rel \== '#')
+ ->
+ % A|R et B sont ordonnes donc
+ % on peut deduire leur signe et celui de R
+ (occurs(Rel,('=<','<')) ->
+ % A et R negatifs, B positifs
+ mfd:dvar_remove_greater(A,0),
+ mfd:dvar_remove_greater(R,0),
+ mfd:dvar_remove_smaller(B,0)
+ ; % occurs(Rel,('>=','>'))
+ % A et R positifs, B negatif
+ mfd:dvar_remove_smaller(A,0),
+ mfd:dvar_remove_smaller(R,0),
+ mfd:dvar_remove_greater(B,0))
+ ; true)))))
+ ; true)).
div_mod_rec(A, B, Q, BQ, R) :-
- mfd:get_intervals(A,SA),
- mfd:get_intervals(B,SB),
- mfd:get_intervals(Q,SQ),
- mfd:get_intervals(R,SR),
- div_mod_rec(5,A, SA, B, SB, Q, SQ, BQ, R, SR).
+ mfd:get_intervals(A,SA),
+ mfd:get_intervals(B,SB),
+ mfd:get_intervals(Q,SQ),
+ mfd:get_intervals(R,SR),
+ div_mod_rec(5,A, SA, B, SB, Q, SQ, BQ, R, SR).
%% - |B| > |R|
@@ -4229,123 +4226,120 @@ div_mod_rec(A, B, Q, BQ, R) :-
%% - si Q < 0 BQ est du signe oppose de B donc du signe de A et R
%% - si Q = 0, BQ=0
div_mod_rec(Credit, A, SA, B, SB, Q, SQ, BQ, R, SR) :-
- %% Propagation des arguments vers les resultats
- %% Q = A div B
- div_interval(div,A,B,Q),
-
- %% BQ = B*Q
- check_zero_and_mult_interval(B,Q,BQ),
-
- %% R = A - B*Q
- %% BQ est du signe de A et R
- same_sign_minus_interval(A,BQ,R),
-%% minus_interval(A,BQ,R),
-
- %% Propagation des resultats vers les arguments
- %% A = B*Q + R
- %% BQ est du signe de A et R
- same_sign_add_interval(BQ,R,A),
-%% add_interval(BQ,R,A),
-
- %% B*Q = A - R
- %% A et R sont du meme signe
- same_sign_minus_interval(A,R,BQ),
-%% minus_interval(A,R,BQ),
-
- %% Q = (B*Q) div B
- div_interval(div,BQ,B,Q),
- %% Plus precis que congr_div_directe
- congr_mult_inverse(BQ,B,Q),
-
- %% Attention au zero de Q
- %% B = (B*Q) div Q
- check_zero_and_div_interval(BQ,Q,B),
- %% Plus precis que congr_div_directe
- congr_mult_inverse(BQ,Q,B),
-
- congr_div_directe(A,B,Q),
- congr_mod_directe(A,B,R),
-
- saturate_add_inequalities(A,BQ,R),
- saturate_mult_inequalities(BQ,Q,B),
- mfd:get_intervals(A,NSA),
- mfd:get_intervals(B,NSB),
- mfd:get_intervals(Q,NSQ),
- mfd:get_intervals(R,NSR),
-
- ((Credit == 0;
+ % Propagation des arguments vers les resultats
+ % Q = A div B
+ div_interval(div,A,B,Q),
+
+ % BQ = B*Q
+ check_zero_and_mult_interval(B,Q,BQ),
+
+ % R = A - B*Q
+ % BQ est du signe de A et R
+ same_sign_minus_interval(A,BQ,R),
+
+ % Propagation des resultats vers les arguments
+ % A = B*Q + R
+ % BQ est du signe de A et R
+ same_sign_add_interval(BQ,R,A),
+
+ % B*Q = A - R
+ % A et R sont du meme signe
+ same_sign_minus_interval(A,R,BQ),
+
+ % Q = (B*Q) div B
+ div_interval(div,BQ,B,Q),
+ % Plus precis que congr_div_directe
+ congr_mult_inverse(BQ,B,Q),
+
+ % Attention au zero de Q
+ % B = (B*Q) div Q
+ check_zero_and_div_interval(BQ,Q,B),
+ % Plus precis que congr_div_directe
+ congr_mult_inverse(BQ,Q,B),
+
+ congr_div_directe(A,B,Q),
+ congr_mod_directe(A,B,R),
+
+ saturate_add_inequalities(A,BQ,R),
+ saturate_mult_inequalities(BQ,Q,B),
+ mfd:get_intervals(A,NSA),
+ mfd:get_intervals(B,NSB),
+ mfd:get_intervals(Q,NSQ),
+ mfd:get_intervals(R,NSR),
+
+ ((Credit == 0;
SA == NSA,
- SB == NSB,
- SQ == NSQ,
- SR == NSR)
- ->
- true
- ; NCredit is Credit - 1,
+ SB == NSB,
+ SQ == NSQ,
+ SR == NSR)
+ ->
+ true
+ ; NCredit is Credit - 1,
div_mod_rec(NCredit, A, NSA, B, NSB, Q, NSQ, BQ, R, NSR)).
same_sign_add_interval(Val1,Val2,Val) :-
- (integer(Val) ->
- true
- ; mfd:get_intervals(Val1,Inter1),
- mfd:get_intervals(Val2,Inter2),
- mfd:get_intervals(Val,Inter),
- ((Inter1 == Inter, number_in_interval(Inter2,0);
- Inter2 == Inter, number_in_interval(Inter1,0))
- ->
- %% Le 0 de Val1 ou Val2 copiera Val2 ou Val1
- %% Inutile de continuer
- true
- ; mfd:dvar_range(Val,Min,Max),
- split_neg_pos(Inter1,Neg1,Pos1,Z1),
- split_neg_pos(Inter2,Neg2,Pos2,Z2),
- (nonvar(Z1) ->
- append(Neg1,[0],NNeg1),
- NPos1 = [0|Pos1]
- ; NNeg1 = Neg1,
- NPos1 = Pos1),
- add_interval_list(NNeg1,Neg2,Min,Max,Neg),
- add_interval_list(NPos1,Pos2,Min,Max,Pos),
- (nonvar(Z2) ->
- %% Le zero de Val2 copie le domaine de Val1
- append(Neg,Pos,EBagNInter),
- append(Inter1,EBagNInter,BagNInter)
- ; append(Neg,Pos,BagNInter)),
- list_to_intervals(integer,BagNInter,NInter),
- mfd:quiet_set_intervals(Val,NInter))),
- congr_add_directe(Val1,Val2,Val).
+ (integer(Val) ->
+ true
+ ; mfd:get_intervals(Val1,Inter1),
+ mfd:get_intervals(Val2,Inter2),
+ mfd:get_intervals(Val,Inter),
+ ((Inter1 == Inter, number_in_interval(Inter2,0);
+ Inter2 == Inter, number_in_interval(Inter1,0))
+ ->
+ % Le 0 de Val1 ou Val2 copiera Val2 ou Val1
+ % Inutile de continuer
+ true
+ ; mfd:dvar_range(Val,Min,Max),
+ split_neg_pos(Inter1,Neg1,Pos1,Z1),
+ split_neg_pos(Inter2,Neg2,Pos2,Z2),
+ (nonvar(Z1) ->
+ append(Neg1,[0],NNeg1),
+ NPos1 = [0|Pos1]
+ ; NNeg1 = Neg1,
+ NPos1 = Pos1),
+ add_interval_list(NNeg1,Neg2,Min,Max,Neg),
+ add_interval_list(NPos1,Pos2,Min,Max,Pos),
+ (nonvar(Z2) ->
+ % Le zero de Val2 copie le domaine de Val1
+ append(Neg,Pos,EBagNInter),
+ append(Inter1,EBagNInter,BagNInter)
+ ; append(Neg,Pos,BagNInter)),
+ list_to_intervals(integer,BagNInter,NInter),
+ mfd:quiet_set_intervals(Val,NInter))),
+ congr_add_directe(Val1,Val2,Val).
same_sign_minus_interval(Val1,Val2,Val) :-
- (integer(Val) ->
- true
- ; mfd:get_intervals(Val1,Inter1),
- mfd:get_intervals(Val2,Inter2),
- mfd:get_intervals(Val,Inter),
- ((Inter1 == Inter,
- number_in_interval(Inter2,0))
- ->
- %% Le 0 de Val2 copiera Val1
- %% Inutile de continuer
- true
- ; mfd:dvar_range(Val,Min,Max),
- split_neg_pos(Inter1,Neg1,Pos1,Z1),
- split_neg_pos(Inter2,Neg2,Pos2,Z2),
- (nonvar(Z1) ->
- append(Neg1,[0],NNeg1),
- NPos1 = [0|Pos1]
- ; NNeg1 = Neg1,
- NPos1 = Pos1),
- minus_interval_list(NNeg1,Neg2,Min,Max,Neg),
- minus_interval_list(NPos1,Pos2,Min,Max,Pos),
- (nonvar(Z2) ->
- %% Le zero de Val2 copie le domaine de Val1
- append(Neg,Pos,EBagNInter),
- append(Inter1,EBagNInter,BagNInter)
- ; append(Neg,Pos,BagNInter)),
- list_to_intervals(integer,BagNInter,NInter),
- mfd:quiet_set_intervals(Val,NInter))),
- congr_add_inverse(Val1,Val2,Val).
+ (integer(Val) ->
+ true
+ ; mfd:get_intervals(Val1,Inter1),
+ mfd:get_intervals(Val2,Inter2),
+ mfd:get_intervals(Val,Inter),
+ ((Inter1 == Inter,
+ number_in_interval(Inter2,0))
+ ->
+ % Le 0 de Val2 copiera Val1
+ % Inutile de continuer
+ true
+ ; mfd:dvar_range(Val,Min,Max),
+ split_neg_pos(Inter1,Neg1,Pos1,Z1),
+ split_neg_pos(Inter2,Neg2,Pos2,Z2),
+ (nonvar(Z1) ->
+ append(Neg1,[0],NNeg1),
+ NPos1 = [0|Pos1]
+ ; NNeg1 = Neg1,
+ NPos1 = Pos1),
+ minus_interval_list(NNeg1,Neg2,Min,Max,Neg),
+ minus_interval_list(NPos1,Pos2,Min,Max,Pos),
+ (nonvar(Z2) ->
+ % Le zero de Val2 copie le domaine de Val1
+ append(Neg,Pos,EBagNInter),
+ append(Inter1,EBagNInter,BagNInter)
+ ; append(Neg,Pos,BagNInter)),
+ list_to_intervals(integer,BagNInter,NInter),
+ mfd:quiet_set_intervals(Val,NInter))),
+ congr_add_inverse(Val1,Val2,Val).
@@ -5995,7 +5989,7 @@ launch_delta_leq_lt(+,Inter,A,B) :-
; true).
:- export update_delta_cost_with_congr/6.
-%%update_delta_cost_with_congr(X,Y,S,C,S,C) :- !.
+%update_delta_cost_with_congr(X,Y,S,C,S,C) :- !.
update_delta_cost_with_congr(X,Y,S,C,NS,NC) :-
((exists_congr(X,CX,MX),
exists_congr(Y,CY,MY),
diff --git a/Src/COLIBRI/check_ineq.pl b/Src/COLIBRI/check_ineq.pl
index 280ae45a4..3e0b03112 100644
--- a/Src/COLIBRI/check_ineq.pl
+++ b/Src/COLIBRI/check_ineq.pl
@@ -13,25 +13,25 @@ saturate_add_inequalities(A,B,C):-
getval(use_delta,1)@eclipse,
!,
ndelta:disable_delta_check,
- (nonvar(A) ->
- ((var(B),
- var(C))
- ->
- launch_delta_add_res_inst(A,B,C)
- ; true)
- ; (var(B) ->
- (var(C) ->
- launch_delta_add(A,B,C),
- %% Les update_var sont indispensables ici pour NETON !
- update_var_from_delta(B,C,A),
- update_var_from_delta(C,B,A)
- ; %% A = B + cste
- launch_delta_equal(A,B,C))
- ; (var(C) ->
- %% A = C + cste
- launch_delta_equal(A,C,B)
- ; %% Normalement inutile !
- true))),
+ (nonvar(A) ->
+ ((var(B),
+ var(C))
+ ->
+ launch_delta_add_res_inst(A,B,C)
+ ; true)
+ ; (var(B) ->
+ (var(C) ->
+ launch_delta_add(A,B,C),
+ % Les update_var sont indispensables ici pour NETON !
+ update_var_from_delta(B,C,A),
+ update_var_from_delta(C,B,A)
+ ; % A = B + cste
+ launch_delta_equal(A,B,C))
+ ; (var(C) ->
+ % A = C + cste
+ launch_delta_equal(A,C,B)
+ ; % Normalement inutile !
+ true))),
ndelta:allow_delta_check.
saturate_add_inequalities(A,B,C).
@@ -172,23 +172,23 @@ launch_delta_equal(A,B,Cste) :-
%update_var_from_delta(B,A,C) :- !.
update_var_from_delta(B,A,C) :-
- %% C = A + B
- (ndelta:get_deltas(A,C,RelAC,DistAC) ->
- update_var_from_delta_rel(RelAC,DistAC,B,A,C)
- ; true),!.
+ % C = A + B
+ (ndelta:get_deltas(A,C,RelAC,DistAC) ->
+ update_var_from_delta_rel(RelAC,DistAC,B,A,C)
+ ; true),!.
update_var_from_delta(B,A,C) :-
- ndelta:fail_delta.
+ ndelta:fail_delta.
update_var_from_delta_rel('#',L..H,B,A,C) :-
- interval_from_bounds(L,-1,Neg),
- interval_from_bounds(1,H,Pos),
- % pas de notify_constrained
- mfd:quiet_set_intervals(B,[Neg,Pos]).
+ interval_from_bounds(L,-1,Neg),
+ interval_from_bounds(1,H,Pos),
+ % pas de notify_constrained
+ mfd:quiet_set_intervals(B,[Neg,Pos]).
update_var_from_delta_rel('=',DistAC,B,_,_) :-
- protected_unify(B = DistAC).
+ protected_unify(B = DistAC).
update_var_from_delta_rel('+',DistAC,B,A,C) :-
- % pas de notify_constrained
- mfd:quiet_set_intervals(B,[DistAC]).
+ % pas de notify_constrained
+ mfd:quiet_set_intervals(B,[DistAC]).
%% Mise a jour du range de A et B de maniere
%% compatible avec leur delta
@@ -197,10 +197,11 @@ update_var_from_delta_rel('+',DistAC,B,A,C) :-
%% des intervalles compatibles de A et B pour ajuster les bornes
%% (on pourrait alors provoquer des convergences lentes)
-%update_args_from_delta(?,?,A,B) :- !.
-
+% FAUX !!!
+% PROVOQUE DES BUGS DANS div_mod_rec
+update_args_from_delta(?,?,A,B) :- !.
update_args_from_delta(Rel,Delta,A,B) :-
- update_args_from_delta0(Rel0,Delta0,A,B),
+ update_args_from_delta0(Rel0,Delta0,A,B),
((nonvar(Rel),
nonvar(Delta))
->
@@ -212,141 +213,141 @@ update_args_from_delta(Rel,Delta,A,B) :-
% on exploite pas ce delta dans les compositions d intervalles
Rel = ?,
Delta = ?
- ; Rel = Rel0,
+ ; Rel = Rel0,
Delta = Delta0)).
update_args_from_delta0(Rel,Delta,A,A) ?- !,
- Rel = '=',
- Delta = 0.
+ Rel = '=',
+ Delta = 0.
update_args_from_delta0(Rel,Delta,A,B) :-
- (exists_delta_Rel(A,B,Rel0,S,C) ->
- update_args_from_delta(Rel0,S,C,A,B,Rel,Delta)
- ; Rel = ?,
- Delta = ?),
- !.
+ (exists_delta_Rel(A,B,Rel0,S,C) ->
+ update_args_from_delta(Rel0,S,C,A,B,Rel,Delta)
+ ; Rel = ?,
+ Delta = ?),
+ !.
update_args_from_delta0(Rel,Delta,A,B) :-
- ndelta:fail_delta.
+ ndelta:fail_delta.
update_args_from_delta(Rel0,S,C,A,B,Rel,Delta) :-
- update_delta_cost_with_congr(A,B,S,C,NS,NC),
- ((S,C) == (NS,NC) ->
- Rel = Rel0,
- Delta = C,
- update_A_B_from_delta(Rel0,C,A,B)
- ; %% On peut devoir unifier A et B
- (NC == 0 ->
- protected_unify(A = B),
- Rel = '=',
- Delta = 0
- ; %% on met a jour le delta sans provoquer
- %% une analyse
- ndelta:update_deltas_between(A,B,NS,NC),
- exists_delta_Rel(A,B,Rel,_,Delta),
- update_A_B_from_delta(Rel,Delta,A,B))).
+ update_delta_cost_with_congr(A,B,S,C,NS,NC),
+ ((S,C) == (NS,NC) ->
+ Rel = Rel0,
+ Delta = C,
+ update_A_B_from_delta(Rel0,C,A,B)
+ ; % On peut devoir unifier A et B
+ (NC == 0 ->
+ protected_unify(A = B),
+ Rel = '=',
+ Delta = 0
+ ; % on met a jour le delta sans provoquer
+ % une analyse
+ ndelta:update_deltas_between(A,B,NS,NC),
+ exists_delta_Rel(A,B,Rel,_,Delta),
+ update_A_B_from_delta(Rel,Delta,A,B))).
update_A_B_from_delta(Rel,Delta,A,B) :-
- update_A_B_from_delta0(Rel,Delta,A,B).
+ update_A_B_from_delta0(Rel,Delta,A,B).
update_A_B_from_delta0(?,?,A,B) :- !.
update_A_B_from_delta0(_,0,A,B) :- !,
- protected_unify(A = B).
+ protected_unify(A = B).
update_A_B_from_delta0(Rel,Delta,A,B) :-
- A \== B,
- mfd:dvar_range(A,MinA,MaxA),
- mfd:dvar_range(B,MinB,MaxB),
- update_A_B_from_delta(Rel,Delta,MinA,MaxA,MinB,MaxB,NMinA,NMaxA,NMinB,NMaxB),
- ((NMinA,NMaxA) == (MinA,MaxA) ->
- true
- ; interval_from_bounds(NMinA,NMaxA,IA),
- % pas de notify_constrained
- mfd:quiet_set_intervals(A,[IA])),
- ((NMinB,NMaxB) == (MinB,MaxB) ->
- true
- ; interval_from_bounds(NMinB,NMaxB,IB),
- % pas de notify_constrained
- mfd:quiet_set_intervals(B,[IB])).
+ A \== B,
+ mfd:dvar_range(A,MinA,MaxA),
+ mfd:dvar_range(B,MinB,MaxB),
+ update_A_B_from_delta(Rel,Delta,MinA,MaxA,MinB,MaxB,NMinA,NMaxA,NMinB,NMaxB),
+ ((NMinA,NMaxA) == (MinA,MaxA) ->
+ true
+ ; interval_from_bounds(NMinA,NMaxA,IA),
+ % pas de notify_constrained
+ mfd:quiet_set_intervals(A,[IA])),
+ ((NMinB,NMaxB) == (MinB,MaxB) ->
+ true
+ ; interval_from_bounds(NMinB,NMaxB,IB),
+ % pas de notify_constrained
+ mfd:quiet_set_intervals(B,[IB])).
update_A_B_from_delta('#',Delta,MinA,MaxA,MinB,MaxB,NMinA,NMaxA,NMinB,NMaxB) :- !,
- update_A_B_from_delta_diff(Delta,MinA,MaxA,MinB,MaxB,NMinA,NMaxA,NMinB,NMaxB).
+ update_A_B_from_delta_diff(Delta,MinA,MaxA,MinB,MaxB,NMinA,NMaxA,NMinB,NMaxB).
update_A_B_from_delta(_,Delta,MinA,MaxA,MinB,MaxB,NMinA,NMaxA,NMinB,NMaxB) :-
- update_A_B_from_delta(Delta,MinA,MaxA,MinB,MaxB,NMinA,NMaxA,NMinB,NMaxB),
- NMinA =< NMaxA,
- NMinB =< NMaxB.
+ update_A_B_from_delta(Delta,MinA,MaxA,MinB,MaxB,NMinA,NMaxA,NMinB,NMaxB),
+ NMinA =< NMaxA,
+ NMinB =< NMaxB.
% Reduction possible si A ou B est instancie
update_A_B_from_delta_diff(Delta,MinA,MaxA,MinB,MaxB,NMinA,NMaxA,NMinB,NMaxB) :-
- update_A_B_from_delta(Delta,MinA,MaxA,MinB,MaxB,MinA0,MaxA0,MinB0,MaxB0),
- (MinA0 == MaxA0 ->
- (MinB0 == MaxB0 ->
- MinA0 \== MinB0,
- NMinA = MinA0,
- NMaxA = MaxA0,
- NMinB = MinB0,
- NMaxB = MaxB0
- ; %% MinA0 interdit pour MinB0 et MaxB0
- NMinA = MinA0,
- NMaxA = MaxA0,
- (MinA0 == MinB0 ->
- NMaxB = MaxB0,
- NMinB is MinB0 + 1
- ; (MinA0 == MaxB0 ->
- NMinB = MinB0,
- NMaxB is MaxB0 - 1
- ; NMinB = MinB0,
- NMaxB = MaxB0)))
- ; (MinB0 == MaxB0 ->
- %% MinB0 interdit pour MinA0 et MaxA0
- NMinB = MinB0,
- NMaxB = MaxB0,
- (MinB0 == MinA0 ->
- NMaxA = MaxA0,
- NMinA is MinA0 + 1
- ; (MinB0 == MaxA0 ->
- NMinA = MinA0,
- NMaxA is MaxA0 - 1
- ; NMinA = MinA0,
- NMaxA = MaxA0))
- ; NMinA = MinA0,
- NMaxA = MaxA0,
- NMinB = MinB0,
- NMaxB = MaxB0)),
- NMinA =< NMaxA,
- NMinB =< NMaxB.
+ update_A_B_from_delta(Delta,MinA,MaxA,MinB,MaxB,MinA0,MaxA0,MinB0,MaxB0),
+ (MinA0 == MaxA0 ->
+ (MinB0 == MaxB0 ->
+ MinA0 \== MinB0,
+ NMinA = MinA0,
+ NMaxA = MaxA0,
+ NMinB = MinB0,
+ NMaxB = MaxB0
+ ; % MinA0 interdit pour MinB0 et MaxB0
+ NMinA = MinA0,
+ NMaxA = MaxA0,
+ (MinA0 == MinB0 ->
+ NMaxB = MaxB0,
+ NMinB is MinB0 + 1
+ ; (MinA0 == MaxB0 ->
+ NMinB = MinB0,
+ NMaxB is MaxB0 - 1
+ ; NMinB = MinB0,
+ NMaxB = MaxB0)))
+ ; (MinB0 == MaxB0 ->
+ % MinB0 interdit pour MinA0 et MaxA0
+ NMinB = MinB0,
+ NMaxB = MaxB0,
+ (MinB0 == MinA0 ->
+ NMaxA = MaxA0,
+ NMinA is MinA0 + 1
+ ; (MinB0 == MaxA0 ->
+ NMinA = MinA0,
+ NMaxA is MaxA0 - 1
+ ; NMinA = MinA0,
+ NMaxA = MaxA0))
+ ; NMinA = MinA0,
+ NMaxA = MaxA0,
+ NMinB = MinB0,
+ NMaxB = MaxB0)),
+ NMinA =< NMaxA,
+ NMinB =< NMaxB.
update_A_B_from_delta(0,MinA,MaxA,MinB,MaxB,MinA,MaxA,MinB,MaxB) :- !.
update_A_B_from_delta(Delta,A,A,MinB,MaxB,NMinA,NMaxA,NMinB,NMaxB) ?- !,
- NMinA = A,
- NMaxA = A,
- min_max_inter(Delta,L,H),
- (MinB == MaxB ->
- A + L =< MinB,
- MinB =< A + H,
- NMinB = MinB,
- NMaxB = MinB
- ; NMinB is max(MinB,A + L),
- NMaxB is min(MaxB,A + H)).
+ NMinA = A,
+ NMaxA = A,
+ min_max_inter(Delta,L,H),
+ (MinB == MaxB ->
+ A + L =< MinB,
+ MinB =< A + H,
+ NMinB = MinB,
+ NMaxB = MinB
+ ; NMinB is max(MinB,A + L),
+ NMaxB is min(MaxB,A + H)).
update_A_B_from_delta(Delta,MinA,MaxA,B,B,NMinA,NMaxA,NMinB,NMaxB) ?- !,
- NMinB = B,
- NMaxB = B,
- min_max_inter(Delta,L,H),
- %% MinA < MaxA
- NMinA is max(MinA,B - H),
- NMaxA is min(MaxA,B - L).
+ NMinB = B,
+ NMaxB = B,
+ min_max_inter(Delta,L,H),
+ % MinA < MaxA
+ NMinA is max(MinA,B - H),
+ NMaxA is min(MaxA,B - L).
update_A_B_from_delta(Delta,MinA,MaxA,MinB,MaxB,NMinA,NMaxA,NMinB,NMaxB) :-
- %% MinA..MaxA + L..H = MinB..MaxB sans toucher L..H
- add_intervals(MinA..MaxA,Delta,MinB0,MaxB0),
- NMinB is max(MinB,MinB0),
- NMaxB is min(MaxB,MaxB0),
- ((NMinB,NMaxB) == (MinB0,MaxB0) ->
- NMinA = MinA,
- NMaxA = MaxA
- ; minus_intervals(NMinB..NMaxB,Delta,MinA0,MaxA0),
- NMinA is max(MinA,MinA0),
- NMaxA is min(MaxA,MaxA0)).
+ % MinA..MaxA + L..H = MinB..MaxB sans toucher L..H
+ add_intervals(MinA..MaxA,Delta,MinB0,MaxB0),
+ NMinB is max(MinB,MinB0),
+ NMaxB is min(MaxB,MaxB0),
+ ((NMinB,NMaxB) == (MinB0,MaxB0) ->
+ NMinA = MinA,
+ NMaxA = MaxA
+ ; minus_intervals(NMinB..NMaxB,Delta,MinA0,MaxA0),
+ NMinA is max(MinA,MinA0),
+ NMaxA is min(MaxA,MaxA0)).
diff --git a/Src/COLIBRI/col_solve.pl b/Src/COLIBRI/col_solve.pl
index 838ef4b26..09c49b9a6 100644
--- a/Src/COLIBRI/col_solve.pl
+++ b/Src/COLIBRI/col_solve.pl
@@ -872,7 +872,8 @@ smt_test(TO,Size,CI) :-
%StrDir = "./QF_BV/crafted/",
%-----------------------------------------------------------------------
- %StrDir = "./QF_AUFBVFP/20210301-Alive2/",% 1 (durdur)
+ %StrDir = "./QF_AUFBVFP/20210301-Alive2/",% 0
+ % devenu sat après correction d'un mauvais appel a smtlib_select !!!!
%-----------------------------------------------------------------------
%StrDir = "QF_ABVFP/20170428-Liew-KLEE/imperial_svcomp_float-benchs_svcomp_mea8000.x86_64/", %0
%StrDir = "QF_ABVFP/20170428-Liew-KLEE/imperial_synthetic_non_terminating_klee_bug.x86_64/", % 0
@@ -880,7 +881,7 @@ smt_test(TO,Size,CI) :-
%StrDir = "./QF_ABVFP/20170428-Liew-KLEE/aachen_real_gmp_gmp_klee_mul.x86_64/", % 3 (bitwuzla 0)
%StrDir = "QF_ABVFP/20170428-Liew-KLEE/aachen_real_numerical_recipes_qrdcmp.x86_64/",
- %StrDir = "./QF_ABVFP/20170428-Liew-KLEE/", % 106 (177 unsupported) (cvc4 55)
+ %StrDir = "./QF_ABVFP/20170428-Liew-KLEE/", % 109 (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)!
@@ -891,7 +892,7 @@ smt_test(TO,Size,CI) :-
%StrDir = "./QF_BVFP/20170428-Liew-KLEE/aachen_syn_halve_longdouble-flow.x86_64/",% 4u
- %StrDir = "./QF_BVFP/20170428-Liew-KLEE/", % 21 (cvc4 50)(bitwuzla
+ %StrDir = "./QF_BVFP/20170428-Liew-KLEE/", % 16 (cvc4 50)(bitwuzla
% 15)(89 u)(11 20mn)
%StrDir = "./QF_BVFP/20170501-Heizmann-UltimateAutomizer/", % 0 (bitwuzla 0)
%StrDir = "./QF_BVFP/ramalho/", % 0 TO (bitwuzla 0)
--
GitLab