diff --git a/Src/COLIBRI/col_solve.pl b/Src/COLIBRI/col_solve.pl
index db253f132511cdd6bb2f5655aff490fe9702de74..c8c93c123945495b23309c2314647e12451e76cf 100644
--- a/Src/COLIBRI/col_solve.pl
+++ b/Src/COLIBRI/col_solve.pl
@@ -800,12 +800,10 @@ smt_test(TO,Size) :-
%StrDir = "./QF_FPLRA/schanda/", % 0 TO (cvc4 0)
%----------------------------------------------------------------
%StrDir = "./QF_FP/20170501-Heizmann-UltimateAutomizer/", % 0
-% A VOIR
%StrDir = "./QF_FP/20190429-UltimateAutomizerSvcomp2019/",% 0 (bitwuzla 0)
- %StrDir = "./QF_FP/ramalho/", % 4 (4 min_solve)(cvc4 19)(bitwuzla 17)
- %StrDir = "./QF_FP/griggio/", % 43 TO (42/41 min_solve)(cast float-double, delta 0) (cvc4 89)(bitwuzla 74)
- %StrDir = "./QF_FP/schanda/spark/", % 5 TO (5 min_solve) (avec (X+Y)/2 = X/2+Y/2
- % quand c'est correcte, pas de inf/0 pour le resultat) (ncvc4 8)(bitwuzla 3)
+ %StrDir = "./QF_FP/ramalho/", % 4 (min_solve)(cvc4 19)(bitwuzla 17)
+ StrDir = "./QF_FP/griggio/", % 43 (min_solve, cast float-double, delta 0) (cvc4 89)(bitwuzla 74)
+ %StrDir = "./QF_FP/schanda/spark/", % 7 (min_solve avec X =< (X+Y)/2 =< Y) (ncvc4 8)(bitwuzla 3)
%StrDir = "./QF_FP/wintersteiger/", % tout OK
%-----------------------------------------------------------------
@@ -823,12 +821,12 @@ smt_test(TO,Size) :-
%StrDir = "./QF_ABV/bmc-arrays/",
%-----------------------------------------------------------------
%StrDir = "QF_AX/",
- %StrDir = "QF_AX/storeinv/",
- %StrDir = "QF_AX/swap/",
- %StrDir = "QF_AX/storecomm/",
- %StrDir = "QF_AX/cvc/",
+ %StrDir = "QF_AX/storeinv/", % 3
+ %StrDir = "QF_AX/swap/", % 8
+ %StrDir = "QF_AX/storecomm/", % 0
+ %StrDir = "QF_AX/cvc/", % 0
- StrDir = "QF_ALIA/qlock2/", % Des TO et core dump
+ %StrDir = "QF_ALIA/qlock2/", % Des TO et core dump
%StrDir = "QF_ALIA/cvc/", % TOUT OK
%StrDir = "QF_ALIA/UltimateAutomizer2/",% des TO
%StrDir = "QF_ALIA/piVC/", % TOUT OK
@@ -1035,12 +1033,13 @@ 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/",
%StrDir = "QF_AX/storeinv/",
%StrDir = "QF_AX/swap/",
%StrDir = "QF_AX/storecomm/",
+ %StrDir = "QF_AX/cvc/",
%----------------------------------------------------------------------
%StrDir = "./QF_BV/",
%StrDir = "./QF_BV/20170501-Heizmann-UltimateAutomizer/",
diff --git a/Src/COLIBRI/realarith.pl b/Src/COLIBRI/realarith.pl
index d49b4481fdf8e1d2444b558a9298a2841ef249a1..29cc334d0c0195e60f4ac45c94516f76896a7122 100755
--- a/Src/COLIBRI/realarith.pl
+++ b/Src/COLIBRI/realarith.pl
@@ -12792,6 +12792,7 @@ div_real_bis(Type,A,B,C) :-
true
; div_real_rec(Type,A,B,C),
div_real_ineqs(Type,A,B,C),
+ average_real_ineqs(Type,A,B,C),
div_real_inst(Type,A,B,C,Continue3),
check_div_mult_exact(Type,A,B,C,Continue3,Continue4),
(var(Continue4) ->
@@ -12800,8 +12801,7 @@ div_real_bis(Type,A,B,C) :-
set_prio_inst([A,B,C],4,5,Prio),
NewGoal = div_real1(Type,A,B,C),
- my_suspend(NewGoal,Prio,(A,B,C)->suspend:constrained),
- saturate_div_real_two(Type,A,B,C)))).
+ my_suspend(NewGoal,Prio,(A,B,C)->suspend:constrained)))).
check_div_mult_exact(Type,A,B,C,Continue,NContinue) :-
var(Continue),
@@ -12828,52 +12828,31 @@ check_div_mult_exact(Type,A,B,C,_,Continue) :-
% permet de capturer certains calculs de moyenne
% Ex A =< (A+B)/2 =< B et A < B
% pour les average_(1,2,3) de schanda
-%saturate_div_real_two(Type,A,B,C) :- !.
+% average_real_ineqs(Type,A,B,C) :- !.
% Bizarre !!
-saturate_div_real_two(Type,A,B,C) :-
+average_real_ineqs(Type,A,B,C) :-
((B == 2.0,
- not_inf_bounds(A),
- not_zero(C),
get_saved_cstr_suspensions(LSusp),
member((S,add_real1(Type,X,Y,AA)),LSusp),
- % (X+Y)/2 = C
- % dans ce cas (X+Y)/2 = X/2 + Y/2
+ AA == A,
var(X),
- var(Y))
+ var(Y),
+ get_rel_between_real_args(X,Y,Rel),
+ occurs(Rel,(<,=<,>,>=)))
->
- % on sature en creant X/2 + Y/2 = C
- get_cstr_suspensions(X,LSX),
- ((member(SX,LSX),
- get_suspension_data(SX,goal,div_real1(Type,XX,X2,Xd2)),
- X2 == 2.0,
- XX == X)
- ->
- Goals1 = []
- ; Goals1 = [div_real(Type,X,2.0,Xd2)]),
- get_cstr_suspensions(Y,LSY),
- ((member(SY,LSY),
- get_suspension_data(SY,goal,div_real1(Type,YY,Y2,Yd2)),
- Y2 == 2.0,
- YY == Y)
- ->
- Goals2 = Goals1
- ; append(Goals1,[div_real(Type,Y,2.0,Yd2)],Goals2)),
- (Goals2 == [] ->
- ((member((_,add_real1(Type,Ud2,Vd2,CC)),LSusp),
- CC == C,
- (Ud2 == Xd2 ->
- Vd2 == Yd2
- ; Ud2 == Yd2,
- Vd2 == Xd2))
- ->
- Goals = []
- ; Goals = [add_real(Type,Xd2,Yd2,C)])
- ; append(Goals2,[add_real(Type,Xd2,Yd2,C)],Goals)),
- (foreach(G,Goals) do
- call_priority(G,2))
+ (getval(use_delta,1)@eclipse ->
+ (occurs(Rel,(=<,<)) ->
+ launch_real_ineq(=<,Type,X,C),
+ launch_real_ineq(=<,Type,C,Y)
+ ; launch_real_ineq(=<,Type,Y,C),
+ launch_real_ineq(=<,Type,C,X))
+ ; (occurs(Rel,(=<,<)) ->
+ launch_geq_real(Type,Y,C),
+ launch_geq_real(Type,C,X)
+ ; launch_geq_real(Type,X,C),
+ launch_geq_real(Type,C,Y)))
; true).
-
%% PMO si les 3 args sont des float_int entre -2^53 et 2^53 on peut
%% deleguer le calcul de mult_real aux entiers
check_launch_div_int(Type,A,B,C,Continue,_) :-