diff --git a/Src/COLIBRI/arith.pl b/Src/COLIBRI/arith.pl
index 1fee14576f1e01806eff4f0cc199c8bedc59078c..ba424247751dc60dbd478cb18470417e149fb310 100755
--- a/Src/COLIBRI/arith.pl
+++ b/Src/COLIBRI/arith.pl
@@ -1394,6 +1394,7 @@ mult_int(A,TA,B,TB,C,TC) :-
wake_if_other_scheduled(Prio).
% on cherche (-X) * (-Y) = C --> X * Y = C
+%check_mult_opp(A,B,C,1) :- !.
check_mult_opp(A,B,C,Continue) :-
save_cstr_suspensions((A,B)),
get_saved_cstr_suspensions(LS),
diff --git a/Src/COLIBRI/col_solve.pl b/Src/COLIBRI/col_solve.pl
index 8e6127866001222253ab733633e2832ff1dc0806..c0ceace71eb2bcf210c31a7010e37f771b0212cb 100644
--- a/Src/COLIBRI/col_solve.pl
+++ b/Src/COLIBRI/col_solve.pl
@@ -798,7 +798,7 @@ smt_test_CI(TO,Size) :-
smt_test(TO,Size,CI) :-
%StrDir = "./colibri_tests/colibri/tests/",
- %StrDir = "./colibri_tests/colibri/tests/sat/",
+ StrDir = "./colibri_tests/colibri/tests/sat/",
% 0 (sans real/float->int!) 1 TO sur newton à 15s mais pas a 24s
%StrDir = "./colibri_tests/colibri/tests/unsat/", %0
@@ -1031,7 +1031,7 @@ smt_test(TO,Size,CI) :-
%StrDir = "QF_NIA/",
%StrDir = "QF_NIA/20170427-VeryMax/", %Que des TO
%StrDir = "QF_NIA/AProVE/", % 1475/2406 (3 I) 5 unknown
- StrDir = "bugs_NIA/", % 6/6 unknown !!!
+ %StrDir = "bugs_NIA/", % 6/6 unknown !!!
%StrDir = "QF_NIA/calypto/", % 6/117
%StrDir = "QF_NIA/LassoRanker/",% 52/106
%StrDir = "QF_NIA/LCTES/",% 2/2
diff --git a/Src/COLIBRI/realarith.pl b/Src/COLIBRI/realarith.pl
index 4c689732fed9ad1da41382ede88c9c0ea7c0e8aa..6c0d1175f0ae2a1b52583c611141dcbece3985f3 100644
--- a/Src/COLIBRI/realarith.pl
+++ b/Src/COLIBRI/realarith.pl
@@ -4053,7 +4053,9 @@ rat_of_decimal_string(Str0,Rat) :-
split_string(Str1,"E","",[Str,SExp]))
->
string_list(SExp,LSExp),
- (LSExp = [0'-|LSExp1] ->
+ ((LSExp = [0'-|LSExp1];
+ LSExp = [0'+|LSExp1])
+ ->
true
; LSExp1 = LSExp),
(foreach(C,LSExp1) do
@@ -4061,7 +4063,7 @@ rat_of_decimal_string(Str0,Rat) :-
C =< 0'9),
number_string(Exp,SExp),
abs(Exp,AExp),
- build_power_10(AExp,P10Exp),
+ P10Exp is 10^AExp,
(Exp < 0 ->
RExp is 1_1/P10Exp
; RExp is rational(P10Exp))
@@ -4091,12 +4093,6 @@ rat_of_number(N,R) :-
rat_of_decimal_string(SN,R))
; rational(N,R)).
-build_power_10(0,1) :- !.
-build_power_10(N,P10) :-
- PN is N - 1,
- build_power_10(PN,PP10),
- P10 is 10*PP10.
-
get_interval_from_rat(Rat,Inter) :-
float_of_rat(real,rtn,Rat,L),
float_of_rat(real,rtp,Rat,H),
@@ -19221,12 +19217,17 @@ geq_real_number_box(real,A,B,Continue) ?- !,
; (is_real_box(B) ->
% On ne peut rien enlever
get_dvar_fintervals(B,[MinB..MaxB]),
- ((MaxB =\= 1.0Inf,
- RA > rational(MaxB))
+ (MinB > -1.0Inf ->
+ RA >= rational(MinB)
+ ; % -1.0Inf interdit
+ true),
+ ((MaxB < 1.0Inf,
+ RA >= rational(MaxB))
->
% donc RA > B, on a fini
true
- ; % RA < MaxB et on doit continuer
+ ; % RA < MaxB ou MaxB = 1.0Inf
+ % donc on doit continuer
Continue = 1)
; (number(B) ->
RA >= rational(B)
@@ -19252,7 +19253,8 @@ geq_real_number_box(real,A,B,Continue) ?- !,
(number(B) ->
% rbox interdit A = B donc A > B
launch_gt_real(real,A,B)
- ; (is_real_box(B) ->
+ ; % BM: peux mieux faire si is_real_box_rat(B,RB)
+ (is_real_box(B) ->
% On ne peut rien enlever dans A et B
% Succes certain quand MinA >= MaxB
% Sinon, echec certain quand MaxA <= MinB
@@ -19614,13 +19616,13 @@ gt_real_numberA(A,B,Continue) :-
; mreal:dvar_remove_greater(B,A),
(number(B) ->
A > B
- ; (mreal:maxdomain(B) =:= get_next_float(real,-1.0Inf) ->
+ ; (mreal:maxdomain(B) =:= get_next_float(Type,-1.0Inf) ->
launch_box(B),
gt_real_numberA(A,B,Continue)
; mreal:get_intervals(B,InterB),
(append(NInterB,[A],InterB) ->
% A isole dans B, on le retire
- mreal:set_typed_intervals(B,real,NInterB)
+ mreal:set_typed_intervals(B,Type,NInterB)
; Continue = 1)))))).
gt_real_boxA(A,B,Continue) :-
@@ -19630,15 +19632,26 @@ gt_real_boxA(A,B,Continue) :-
(check_rbox_rat(B,RatB) ->
RatA > RatB
; (is_real_box(B) ->
- % pas de reduction possible
- MinA >= MinB,
- MaxA >= MaxB,
(MinA >= MaxB ->
- % les rbox interdisent A = B
+ % c'est fini
true
- ; Continue = 1)
+ ; MaxA >= MaxB,
+ % pas de reduction possible
+ % les rbox interdisent A = B
+ (MinB == -1.0Inf ->
+ RMinB = MinB
+ ; RMinB is rational(MinB)),
+ RatA >= RMinB,
+ (MaxB == 1.0Inf ->
+ RMaxB = MaxB
+ ; RMaxB is rational(MaxB)),
+ (RatA >= RMaxB ->
+ true
+ ; % MinB < RatA < MaxB
+ % On peut avoir plus tard un RatB < RatA
+ Continue = 1))
; (is_float_number(B) ->
- % donc box impossible
+ % donc box impossible sauf ibox
% MinA < A, on doit interdire A = B
Continue = 1,
mreal:dvar_remove_greater(B,MinA)
@@ -19650,38 +19663,47 @@ gt_real_boxA(A,B,Continue) :-
RatA > rational(B)
; mreal:maxdomain(B,Max),
((not_inf_bounds(Max),
- RatA > Max)
+ RatA > rational(Max))
->
true
; (Max =:= get_next_float(real,-1.0Inf) ->
launch_box(B),
gt_real_boxA(A,B,Continue)
; Continue = 1)))))
- ; (is_real_box(B) ->
+ ; % A est une box
+ (is_real_box_rat(B,RatB) ->
% pas de reduction possible
- % Seul le cas MinA >= B est autorise (A > MinA)
- MinA >= MinB,
- MaxA >= MaxB,
- (MinA >= MaxB ->
+ % Les rbox interdisent A = B
+ ((not_inf_bounds(MinA),
+ rational(MinA) >= RatB)
+ ->
true
- ; % Les rbox interdisent A = B
- Continue = 1)
- ; (is_float_number(B) ->
- % MinA < A
- mreal:dvar_remove_greater(B,MinA)
- ; % B intervalle normal
- % On peut enlever dans A seulement
- % comme pour un geq_real
- mreal:dvar_remove_greater(B,MaxA)),
- (number(B) ->
- MaxA > B
- ; mreal:maxdomain(B,Max),
- (MinA > MaxB ->
+ ; Continue = 1)
+ ; (is_real_box(B) ->
+ % pas de reduction possible
+ % Seul le cas MinA >= B est autorise (A > MinA)
+ MinA >= MinB,
+ MaxA >= MaxB,
+ (MinA >= MaxB ->
true
- ; (mreal:maxdomain(B) =:= get_next_float(real,-1.0Inf) ->
- launch_box(B),
- gt_real_boxA(A,B,Continue)
- ; Continue = 1))))).
+ ; % Les rbox interdisent A = B
+ Continue = 1)
+ ; (is_float_number(B) ->
+ % MinA < A
+ mreal:dvar_remove_greater(B,MinA)
+ ; % B intervalle normal
+ % On peut enlever dans A seulement
+ % comme pour un geq_real
+ mreal:dvar_remove_greater(B,MaxA)),
+ (number(B) ->
+ MaxA > B
+ ; mreal:maxdomain(B,Max),
+ (MinA > MaxB ->
+ true
+ ; (mreal:maxdomain(B) =:= get_next_float(real,-1.0Inf) ->
+ launch_box(B),
+ gt_real_boxA(A,B,Continue)
+ ; Continue = 1)))))).
gt_real_float_numberA(A,B,Continue) :-
(number(B) ->
diff --git a/Src/COLIBRI/solve.pl b/Src/COLIBRI/solve.pl
index 4fd129a2833e02424cc3e012f702bb93fa866383..c2fd3283131e32aa5192aab6949419442aadb422 100644
--- a/Src/COLIBRI/solve.pl
+++ b/Src/COLIBRI/solve.pl
@@ -3962,29 +3962,53 @@ diff_real_chk_nan(Type,A,B) :-
ensure_not_NaN(B)
; (B == nan ->
ensure_not_NaN(A)
- ; ((check_not_NaN(A),
- check_not_NaN(B))
+ ; ((number(A) ->
+ check_not_NaN(B),
+ Val = A,
+ Var = B
+ ; number(B),
+ check_not_NaN(A),
+ Val = B,
+ Var = A)
->
- launch_diff_real(Type,A,B)
- ; save_cstr_suspensions((A,B)),
- get_saved_cstr_suspensions(LSusp),
- ((member((_,diff_real_chk_nan(Type,AA,BB)),LSusp),
- (AA == A ->
- BB == B
- ; AA == B,
- BB == A))
+ mreal:dvar_remove_element(Var,Val)
+ ; ((check_not_NaN(A),
+ check_not_NaN(B),
+ (not_zero(A);
+ not_zero(B)))
->
- true
- ; my_suspend(diff_real_chk_nan(Type,A,B),0,
- (A,B)->suspend:constrained),
- % on est bloque par un NaN ?
- (check_not_NaN(A) ->
- VNaN = B
- ; VNaN = A),
- int_vars(bool,Bool),
- set_lazy_domain(Type,VNaN),
- isNaN(VNaN,Bool),
- insert_dep_inst(dep(Bool,0,[])))))),
+ launch_diff_real(Type,A,B)
+ ; save_cstr_suspensions((A,B)),
+ get_saved_cstr_suspensions(LSusp),
+ ((member((Susp,diff_real_chk_nan(Type,AA,BB)),LSusp),
+ get_suspension_data(Susp,state,State),
+ State \= 2,
+ (AA == A ->
+ BB == B
+ ; AA == B,
+ BB == A))
+ ->
+ true
+ ; % on est bloque par un NaN ou zero ?
+ (check_not_NaN(A) ->
+ (check_not_NaN(B) ->
+ % A et B peuvent valoir zero 0
+ true
+ ; ChkNan = 1,
+ VNaN = B)
+ ; ChkNan = 1,
+ VNaN = A),
+ (nonvar(ChkNan) ->
+ int_vars(bool,Bool),
+ set_lazy_domain(Type,VNaN),
+ isNaN(VNaN,Bool),
+ insert_dep_inst(dep(Bool,0,[]))
+ ; true),
+ (var(Bool) ->
+ my_suspend(diff_real_chk_nan(Type,A,B),0,
+ (A,B,Bool)->suspend:
+ constrained)
+ ; diff_real_chk_nan(Type,A,B))))))),
set_priority(P),
wake_if_other_scheduled(P).