diff --git a/Src/COLIBRI/arith.pl b/Src/COLIBRI/arith.pl
index 38780ee6de286021499d8e3bf0fd0ce4de9eaafd..aa24e3316c53e7fcb072466133dfc415ae739c3d 100755
--- a/Src/COLIBRI/arith.pl
+++ b/Src/COLIBRI/arith.pl
@@ -4558,128 +4558,135 @@ power_int_body(A,TA,N,Mod2,B,TB,Continue) :-
%% plus vite !
check_delta_power(A,N,Mod2,B,TA,TB) :-
(exists_delta_Rel(A,B,Rel,_,_) ->
- mfd:dvar_domain(A,DomA),
- mfd:dvar_domain(B,DomB),
- (Mod2 == 0 ->
- Rel \== '>',
- (Rel == '>=' ->
- %% Donc A = B et A :: [0,1]
- mfd:quiet_set_intervals(A,[0,1]),
- protected_unify(A = B)
- ; (Rel == '=<' ->
- true
- ; %% A <> B
- mfd:dom_difference(DomA,dom([0,1]),NDomA),
- mfd:dvar_set(A,NDomA),
- mfd:dvar_remove_element(B,0)))
- ; %% A et B de meme signe
- (Rel == '<' ->
- %% A > 1
- mfd:dvar_remove_smaller(A,2),
- MinB is pow_int(2,N),
- mfd:dvar_remove_smaller(B,MinB)
- ; (Rel == '=<' ->
- %% A >= -1
- mfd:dvar_remove_smaller(A,-1),
- mfd:dvar_remove_smaller(B,-1)
- ; (Rel == '>' ->
- %% A < -1
- mfd:dvar_remove_greater(A,-2),
- MaxB is pow_int(-2,N),
- mfd:dvar_remove_greater(B,MaxB)
- ; (Rel == '>=' ->
- %% A =< 1
- mfd:dvar_remove_greater(A,1),
- mfd:dvar_remove_greater(B,1)
- ; %% Rel = '#'
- mfd:dom_difference(DomA,dom([-1..1]),NDomA),
- mfd:dom_difference(DomB,dom([-1..1]),NDomB),
- mfd:dvar_set(A,NDomA),
- mfd:dvar_set(B,NDomB)))))),
- mfd:dvar_domain(A,NewDomA),
- mfd:dvar_domain(B,NewDomB),
- (NewDomA == DomA ->
- true
- ; TA = 1),
- (NewDomB == DomB ->
- true
- ; TB = 1)
- ; true).
+ mfd:dvar_domain(A,DomA),
+ mfd:dvar_domain(B,DomB),
+ (Mod2 == 0 ->
+ Rel \== '>',
+ (Rel == '>=' ->
+ % Donc A = B et A :: [0,1]
+ mfd:quiet_set_intervals(A,[0,1]),
+ protected_unify(A = B)
+ ; (Rel == '=<' ->
+ true
+ ; % A <> B
+ mfd:dom_difference(DomA,dom([0,1]),NDomA),
+ mfd:dvar_set(A,NDomA),
+ mfd:dvar_remove_element(B,0)))
+ ; % A et B de meme signe
+ (Rel == '<' ->
+ % A > 1
+ mfd:dvar_remove_smaller(A,2),
+ MinB is pow_int(2,N),
+ mfd:dvar_remove_smaller(B,MinB)
+ ; (Rel == '=<' ->
+ % A >= -1
+ mfd:dvar_remove_smaller(A,-1),
+ mfd:dvar_remove_smaller(B,-1)
+ ; (Rel == '>' ->
+ % A < -1
+ mfd:dvar_remove_greater(A,-2),
+ MaxB is pow_int(-2,N),
+ mfd:dvar_remove_greater(B,MaxB)
+ ; (Rel == '>=' ->
+ % A =< 1
+ mfd:dvar_remove_greater(A,1),
+ mfd:dvar_remove_greater(B,1)
+ ; % Rel = '#'
+ mfd:dom_difference(DomA,dom([-1..1]),NDomA),
+ mfd:dom_difference(DomB,dom([-1..1]),NDomB),
+ mfd:dvar_set(A,NDomA),
+ mfd:dvar_set(B,NDomB)))))),
+ mfd:dvar_domain(A,NewDomA),
+ mfd:dvar_domain(B,NewDomB),
+ (NewDomA == DomA ->
+ true
+ ; TA = 1),
+ (NewDomB == DomB ->
+ true
+ ; TB = 1)
+ ; true).
launch_delta_power(A,Mod2,B) :-
var(A),
- var(B),
+ var(B), % donc N > 0
+ A \== B, % donc N > 1
!,
mfd:dvar_range(A,LA,HA),
mfd:dvar_range(B,LB,HB),
(Mod2 == 0 ->
- (LA < 0 ->
- (abs(LA) =< abs(HA) ->
- % LA -> LB, HA -> HB
- MinD is LB - LA,
- MaxD is HB - HA
- ; MinD is HB - HA,
- MaxD is LB - LA)
- ; MinD is LB - LA,
- MaxD is HB - HA)
+ (HA =< 0 ->
+ % A neg, B pos: HA -> LB, LA -> HB
+ D1 is LB - HA,
+ D2 is HB - LA
+ ; (LA < 0 ->
+ % A non signé
+ (not_unify(A,0) ->
+ D1 = 1
+ ; D1 = 0),
+ % HA > 0,
+ D2 is max(HB-LA,HB-HA)
+ ; % A pos, B pos: LA -> LB, HA -> HB
+ D1 is LB - LA,
+ D2 is HB - HA))
; % meme signe pour A et B
- % LA -> LB, HA -> HB
- MinD is LB - LA,
- MaxD is HB - HA),
+ % si A et B neg: on recule LA -> LB, HA -> HB
+ % si A et B pos: on avance LA -> LB, HA -> HB
+ % si A et B non signés: on recule sur LA -> LB,
+ % on avance sur HA -> HB
+ D1 is LB - LA,
+ D2 is HB - HA),
+ sort(0,=<,[D1,D2],[MinD,MaxD]),
launch_delta(A,B,+,MinD..MaxD).
launch_delta_power(A,Mod2,B).
power_inst(A,N,Mod2,B,Continue) :-
- (integer(A) ->
- B0 is pow_int(A,N),
+ (integer(A) ->
+ B0 is pow_int(A,N),
protected_unify(B,B0)
- ; (integer(B) ->
- abs(B,AbsB),
- int_nroot(AbsB,N,Root),
- (B >= 0 ->
- (Mod2 == 0 ->
- %% A neg ou pos
- OpRoot is -Root,
- mfd:(A::[OpRoot, Root])
- ; %% A et B du meme signe
- A = Root)
- ; %% A et B negatifs
- Mod2 == 1,
- A0 is -Root,
+ ; (integer(B) ->
+ abs(B,AbsB),
+ int_nroot(AbsB,N,Root),
+ (B >= 0 ->
+ (Mod2 == 0 ->
+ % A neg ou pos
+ OpRoot is -Root,
+ mfd:(A::[OpRoot, Root])
+ ; % A et B du meme signe
+ A = Root)
+ ; % A et B negatifs
+ Mod2 == 1,
+ A0 is -Root,
protected_unify(A,A0))
- ; (A == B ->
- mfd:(B :: [-1,0,1])
- ; mfd:dvar_range(A,MinA,MaxA),
- ((MinA >= -1,
- MaxA =< 1)
- ->
- %% A : -1..1
- (Mod2 == 1 ->
- protected_unify(A = B)
- ; abs_val_int_bis(A,B))
- ; Continue = 1)))).
-
-
-
+ ; (A == B ->
+ mfd:(B :: [-1,0,1])
+ ; mfd:dvar_range(A,MinA,MaxA),
+ ((MinA >= -1,
+ MaxA =< 1)
+ ->
+ % A : -1..1
+ (Mod2 == 1 ->
+ protected_unify(A = B)
+ ; abs_val_int_bis(A,B))
+ ; Continue = 1)))).
power_int_rec(A,TA,N,Mod2,B,TB,Continue) :-
- power_int_ter(A,TA,N,Mod2,B,TB),
- mfd:get_intervals(A,IA),
- mfd:get_intervals(B,IB),
- saturate_power_inequalities(A,B,N,Mod2),
- power_inst(A,N,Mod2,B,Continue1),
- (var(Continue1) ->
- true
- ; mfd:get_intervals(A,NIA),
- mfd:get_intervals(B,NIB),
- check_reduced(IA,NIA,NTA),
- check_reduced(IB,NIB,NTB),
- ((var(NTA),
- var(NTB))
- ->
- Continue = 1
- ; power_int_rec(A,NTA,N,Mod2,B,NTB,Continue))).
+ power_int_ter(A,TA,N,Mod2,B,TB),
+ mfd:get_intervals(A,IA),
+ mfd:get_intervals(B,IB),
+ saturate_power_inequalities(A,B,N,Mod2),
+ power_inst(A,N,Mod2,B,Continue1),
+ (var(Continue1) ->
+ true
+ ; mfd:get_intervals(A,NIA),
+ mfd:get_intervals(B,NIB),
+ check_reduced(IA,NIA,NTA),
+ check_reduced(IB,NIB,NTB),
+ ((var(NTA),
+ var(NTB))
+ ->
+ Continue = 1
+ ; power_int_rec(A,NTA,N,Mod2,B,NTB,Continue))).
power_int_ter(A,TA,N,Mod2,B,TB) :-
(nonvar(A);
diff --git a/Src/COLIBRI/col_solve.pl b/Src/COLIBRI/col_solve.pl
index 1d4b80cfd0734aaea6a9547caac89fba589052a2..26e243b8a276b5f31fec1ad4d0a84ede72f3fda3 100644
--- a/Src/COLIBRI/col_solve.pl
+++ b/Src/COLIBRI/col_solve.pl
@@ -735,7 +735,7 @@ smt_test :-
smt_test(TO,Size) :-
%StrDir = "./colibri-master-tests/tests/",
%StrDir = "./colibri-master-tests/tests/sat/", %0 (sans real/float-> int!)
- %StrDir = "./colibri-master-tests/tests/unsat/", %0
+ StrDir = "./colibri-master-tests/tests/unsat/", %0
%StrDir = "./colibri-master-tests/tests/unknown/",
%StrDir = "./smt/",
@@ -841,7 +841,7 @@ smt_test(TO,Size) :-
%StrDir = "./QF_ABVFP/20170428-Liew-KLEE/aachen_real_gmp_gmp_klee_mul.x86_64/", % 3 (bitwuzla 0)
%StrDir = "QF_ABVFP/20170428-Liew-KLEE/aachen_real_numerical_recipes_qrdcmp.x86_64/",
- %StrDir = "./QF_ABVFP/20170428-Liew-KLEE/", % 100 (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)!
@@ -851,7 +851,7 @@ smt_test(TO,Size) :-
%StrDir = "./QF_BVFP/20170428-Liew-KLEE/imperial_synthetic_sqrt_klee.x86_64/", % 3 (bitwuzla 3)
%StrDir = "./QF_BVFP/20170428-Liew-KLEE/aachen_syn_halve_longdouble-flow.x86_64/",% 4u
- %StrDir = "./QF_BVFP/20170428-Liew-KLEE/", % 16 (cvc4 50)(bitwuzla
+ %StrDir = "./QF_BVFP/20170428-Liew-KLEE/", % 17 (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)
@@ -871,7 +871,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/", % 50 (min_solve, sans lin_solve ni ls_reduce..)(39)
+ %StrDir = "./QF_FP/griggio/", % 50 (min_solve, sans lin_solve ni ls_reduce..)(39)
%(cvc4 89)(bitwuzla 74) LES DD DEMARRENT TROP VITE ?
%StrDir = "./QF_FP/schanda/spark/", % 6 (min_solve avec X =< (X+Y)/2 =< Y) (ncvc4 8)(bitwuzla 3)
%StrDir = "./QF_FP/wintersteiger/", % tout OK
diff --git a/Src/COLIBRI/realarith.pl b/Src/COLIBRI/realarith.pl
index 76217f8eecfe2361174db0226e7a9aa66f6cc1c7..7017dd67d8b8b15f7394b84562d9e2889547cabe 100755
--- a/Src/COLIBRI/realarith.pl
+++ b/Src/COLIBRI/realarith.pl
@@ -4471,8 +4471,10 @@ real_inter_dom_if_eq(_,_,DomA,DomB,DomC,DomA,DomB,DomC).
-% BUG
-reduce_dom_add_args_from_res(_,Type,FIA,FIB,FIC,RelCA,RelCB,DomA,DomB,DomC,DomA,DomB) :- !.
+reduce_dom_add_args_from_res(_,Type,FIA,FIB,FIC,RelCA,RelCB,DomA,DomB,DomC,DomA,DomB) :-
+ % BUG
+ mreal:dom_interval(DomC,[-0.0 .. 0.0]),
+ !.
reduce_dom_add_args_from_res(0,Type,FIA,FIB,FIC,RelCA,RelCB,DomA,DomB,DomC,DomA,DomB) :- !.
reduce_dom_add_args_from_res(1,Type,FIA,FIB,FIC,RelCA,RelCB,DomA0,DomB0,DomC,DomA,DomB) :-
mreal:dom_interval(DomA0,IA0),
@@ -9383,8 +9385,10 @@ minus_float_rec(Cpt,RS,Type,A,B,C) :-
minus_float_rec(NCpt,RS,Type,A,B,C))
; true).
-% BUG
-reduce_dom_minus_args_from_res(_,_,FIA,FIB,FIC,RelAC,DomA,DomB,DomC,DomA,DomB) :- !.
+reduce_dom_minus_args_from_res(_,_,FIA,FIB,FIC,RelAC,DomA,DomB,DomC,DomA,DomB) :-
+ % BUG
+ mreal:dom_interval(DomC,[-0.0 .. 0.0]),
+ !.
reduce_dom_minus_args_from_res(0,_,FIA,FIB,FIC,RelAC,DomA,DomB,DomC,DomA,DomB) :- !.
reduce_dom_minus_args_from_res(1,Type,FIA,FIB,FIC,RelAC,DomA0,DomB0,DomC,DomA,DomB) :-
mreal:dom_interval(DomA0,IA0),
@@ -15578,8 +15582,8 @@ max_inv2_div_float_nearest0(_,A,C,B) :-
%% ESSAI VARIANTE SIMPLISTE DE power_real AVEC N ENTIER INSTANCIE >= 0
power_real(A,N,B) :-
- getval(float_eval,Type)@eclipse,
- power_real_type(Type,A,N,B).
+ getval(float_eval,Type)@eclipse,
+ power_real_type(Type,A,N,B).
power_real_type(real,A,N,B) ?- !,
power_real(real,A,N,B).