From 52229fdedf69caf1eb7a601efa5394029a17ee61 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Fri, 23 Apr 2021 08:20:06 +0200
Subject: [PATCH] Import from Bin:a1af7a0 Src:66b5297cc farith:a93db57
---
Src/COLIBRI/arith.pl | 417 +++++++++++++++++++--------------------
Src/COLIBRI/col_solve.pl | 8 +-
Src/COLIBRI/notify.pl | 13 +-
Src/COLIBRI/rbox.pl | 2 +-
Src/COLIBRI/realarith.pl | 247 +++++++++++++++++------
Src/COLIBRI/solve.pl | 17 +-
6 files changed, 422 insertions(+), 282 deletions(-)
diff --git a/Src/COLIBRI/arith.pl b/Src/COLIBRI/arith.pl
index f7d02ebbf..728931bb2 100755
--- a/Src/COLIBRI/arith.pl
+++ b/Src/COLIBRI/arith.pl
@@ -1383,13 +1383,13 @@ no_lin_mult(A,B,C) :-
mult_int(A,_,A,_,C,_) ?- !,
- power(A,2,C).
+ power(A,2,C).
mult_int(A,TA,B,TB,C,TC) :-
- get_priority(Prio),
- set_priority(1),
- mult_bis(A,TA,B,TB,C,TC),
- set_priority(Prio),
- wake_if_other_scheduled(Prio).
+ get_priority(Prio),
+ set_priority(1),
+ mult_bis(A,TA,B,TB,C,TC),
+ set_priority(Prio),
+ wake_if_other_scheduled(Prio).
% on cherche (-X) * (-Y) = C --> X * Y = C
check_mult_opp(A,B,C,Continue) :-
@@ -1404,136 +1404,136 @@ check_mult_opp(A,B,C,Continue) :-
; Continue = 1).
mult_bis(A,TA,B,TB,C,TC) :-
- mfd:get_intervals(A,IA),
- mfd:get_intervals(B,IB),
- mfd:get_intervals(C,IC),
- save_cstr_suspensions((A,B,C)),
- %% Point fixe sur les projections de congruence
- %% on peut aller jusqu'a instancier A,B ou C
- fp_congr_mult(A,B,C),
- mult_inst(A,B,C,Continue),
- (var(Continue) ->
- true
- ; mult_free(A,B,C,Continue1),
- check_exists_power_int_with_mult_args(A,B,C,Continue1,Continue2),
- (var(Continue2) ->
- true
- ; %% Factorisation avec un mult_int
- clear_Goal(mult_int,A,B,C),
- %% On regarde si on a un div_mod_int(C,A,...)
- %% ou div_mod_int(C,B,...)
- check_fusion_div_mod_int(mult_int,A,B,C),
- check_zero_mult_int(A,B,C),
+ mfd:get_intervals(A,IA),
+ mfd:get_intervals(B,IB),
+ mfd:get_intervals(C,IC),
+ save_cstr_suspensions((A,B,C)),
+ % Point fixe sur les projections de congruence
+ % on peut aller jusqu'a instancier A,B ou C
+ fp_congr_mult(A,B,C),
+ mult_inst(A,B,C,Continue),
+ (var(Continue) ->
+ true
+ ; mult_free(A,B,C,Continue1),
+ check_exists_power_int_with_mult_args(A,B,C,Continue1,Continue2),
+ (var(Continue2) ->
+ true
+ ; % Factorisation avec un mult_int
+ clear_Goal(mult_int,A,B,C),
+ % On regarde si on a un div_mod_int(C,A,...)
+ % ou div_mod_int(C,B,...)
+ check_fusion_div_mod_int(mult_int,A,B,C),
+ check_zero_mult_int(A,B,C),
check_assoc_dist(mult_int,A,B,C),
- %% On a peut etre reduit A,B,C avant
- mfd:get_intervals(A,NIA),
- mfd:get_intervals(B,NIB),
- mfd:get_intervals(C,NIC),
- check_reduced(IA,NIA,TA),
- check_reduced(IB,NIB,TB),
- check_reduced(IC,NIC,TC),
- ((var(TA),var(TB),var(TC)) ->
- %% Probleme avec arith_sched sans doute
- TA = 1,
- TB = 1,
- TC = 1
- ; true),
- %% Calcul des projections
- mult_free_proj(A,TA,B,TB,C,TC),
- int_check_notify_constrained(A,IA),
- int_check_notify_constrained(B,IB),
- int_check_notify_constrained(C,IC),
- check_before_susp_mult(A,B,C))).
+ % On a peut etre reduit A,B,C avant
+ mfd:get_intervals(A,NIA),
+ mfd:get_intervals(B,NIB),
+ mfd:get_intervals(C,NIC),
+ check_reduced(IA,NIA,TA),
+ check_reduced(IB,NIB,TB),
+ check_reduced(IC,NIC,TC),
+ ((var(TA),var(TB),var(TC)) ->
+ % Probleme avec arith_sched sans doute
+ TA = 1,
+ TB = 1,
+ TC = 1
+ ; true),
+ % Calcul des projections
+ mult_free_proj(A,TA,B,TB,C,TC),
+ int_check_notify_constrained(A,IA),
+ int_check_notify_constrained(B,IB),
+ int_check_notify_constrained(C,IC),
+ check_before_susp_mult(A,B,C))).
check_exists_power_int_with_mult_args(X,Y,Z,1,Continue) ?- !,
- ((get_saved_cstr_suspensions(LS),
- member((Susp,power_int(A,_,N,B,_)),LS),
- B == Z, %% A^N = Z
- (A == X, V = Y; %% A*Y = Z
- A == Y, V = X)) %% A*X = Z
- ->
- PN is N - 1,
- (not_unify(A,0) ->
- %% le mult_int va devenir un power_int
- power(A,PN,V)
- ; Continue = 1,
- %% le mult_int reste mais on reduit selon le power_int
- copy_term(A,CA),
- mfd:dvar_remove_element(CA,0),
- copy_term(V,CV),
- Mod2 is PN mod 2,
- power_int_ter(CA,1,PN,Mod2,CV,1),
- mfd:get_intervals(CA,ICA),
- mfd:(A:: [0|ICA]))
- ; Continue = 1).
+ ((get_saved_cstr_suspensions(LS),
+ member((Susp,power_int(A,_,N,B,_)),LS),
+ B == Z, %% A^N = Z
+ (A == X, V = Y; %% A*Y = Z
+ A == Y, V = X)) %% A*X = Z
+ ->
+ PN is N - 1,
+ (not_unify(A,0) ->
+ % le mult_int va devenir un power_int
+ power(A,PN,V)
+ ; Continue = 1,
+ % le mult_int reste mais on reduit selon le power_int
+ copy_term(A,CA),
+ mfd:dvar_remove_element(CA,0),
+ copy_term(V,CV),
+ Mod2 is PN mod 2,
+ power_int_ter(CA,1,PN,Mod2,CV,1),
+ mfd:get_intervals(CA,ICA),
+ mfd:(A:: [0|ICA]))
+ ; Continue = 1).
check_exists_power_int_with_mult_args(_,_,_,_,_).
%% Peut on enlever 0 de A,B,C ?
check_zero_mult_int(A,B,C) :-
- (not_unify(C,0) ->
- %% on peut enlever 0 dans A et B
- mfd:dvar_remove_element(A,0),
- mfd:dvar_remove_element(B,0)
- ; ((not_unify(A,0),
- not_unify(B,0))
- ->
- %% on peut enlever 0 dans C
- mfd:dvar_remove_element(C,0)
- ; true)).
+ (not_unify(C,0) ->
+ % on peut enlever 0 dans A et B
+ mfd:dvar_remove_element(A,0),
+ mfd:dvar_remove_element(B,0)
+ ; ((not_unify(A,0),
+ not_unify(B,0))
+ ->
+ % on peut enlever 0 dans C
+ mfd:dvar_remove_element(C,0)
+ ; true)).
%% Exploitation d'instanciations
mult_inst(A,B,C,Continue) :-
- (integer(A) ->
- (integer(B) ->
- C0 is A * B,
+ (integer(A) ->
+ (integer(B) ->
+ C0 is A * B,
protected_unify(C,C0)
- ; (A == 0 ->
- protected_unify(C = 0)
- ; (A == 1 ->
- protected_unify(C = B)
- ; (integer(C) ->
- B0 is C // A,
+ ; (A == 0 ->
+ protected_unify(C = 0)
+ ; (A == 1 ->
+ protected_unify(C = B)
+ ; (integer(C) ->
+ B0 is C // A,
protected_unify(B,B0),
- C is A * B
- ; (A == -1 ->
- no_lin_op(B,C)
- ; Continue = 1)))))
- ; (integer(B) ->
- (B == 0 ->
- protected_unify(C = 0)
- ; (B == 1 ->
- protected_unify(C = A)
- ; (integer(C) ->
- A0 is C // B,
+ C is A * B
+ ; (A == -1 ->
+ no_lin_op(B,C)
+ ; Continue = 1)))))
+ ; (integer(B) ->
+ (B == 0 ->
+ protected_unify(C = 0)
+ ; (B == 1 ->
+ protected_unify(C = A)
+ ; (integer(C) ->
+ A0 is C // B,
protected_unify(A,A0),
- C is A * B
- ; (B == -1 ->
- no_lin_op(A,C)
- ; Continue = 1))))
- ; (integer(C) ->
- (C == 0 ->
- (not_unify(A,0) ->
- protected_unify(B = 0)
- ; (not_unify(B,0) ->
- protected_unify(A = 0)
- ; Continue = 1))
- ; (C == 1 ->
- mfd:quiet_set_intervals(A,[-1,1]),
- A = B
- ; (C == -1 ->
- mfd:quiet_set_intervals(A,[-1,1]),
- no_lin_op(A,B)
- ; %% On pourrait ameliorer en remarquant
- %% que A et B divisent C !!
- OpC is -C,
- (C > 0 ->
- InterAB = [OpC .. -1, 1 .. C]
- ; InterAB = [C .. -1, 1 .. OpC]),
- mfd:([A,B] :: InterAB),
- Continue = 1)))
- ; Continue = 1))).
+ C is A * B
+ ; (B == -1 ->
+ no_lin_op(A,C)
+ ; Continue = 1))))
+ ; (integer(C) ->
+ (C == 0 ->
+ (not_unify(A,0) ->
+ protected_unify(B = 0)
+ ; (not_unify(B,0) ->
+ protected_unify(A = 0)
+ ; Continue = 1))
+ ; (C == 1 ->
+ mfd:quiet_set_intervals(A,[-1,1]),
+ A = B
+ ; (C == -1 ->
+ mfd:quiet_set_intervals(A,[-1,1]),
+ no_lin_op(A,B)
+ ; % On pourrait ameliorer en remarquant
+ % que A et B divisent C !!
+ OpC is -C,
+ (C > 0 ->
+ InterAB = [OpC .. -1, 1 .. C]
+ ; InterAB = [C .. -1, 1 .. OpC]),
+ mfd:([A,B] :: InterAB),
+ Continue = 1)))
+ ; Continue = 1))).
%% Exploitation d'identites entre arguments
mult_free(A,B,C,NContinue) :-
@@ -1542,7 +1542,7 @@ mult_free(A,B,C,NContinue) :-
protected_unify(B = 1)
; (not_unify(B,1) ->
protected_unify(A = 0)
- ; Continue = 1))
+ ; Continue = 1))
; (B == C ->
(not_unify(B,0) ->
protected_unify(A = 1)
@@ -1634,13 +1634,12 @@ mult_free_rec(Cpt,A,TA,B,TB,C,TC) :-
check_before_susp_mult(A,B,C) :-
- check_mult_int_ineqs(A,B,C),
+ check_mult_int_ineqs(A,B,C),
mult_inst(A,B,C,Continue),
- (var(Continue) ->
- true
- ; set_prio_inst([A,B,C],4,5,Prio),
- %%set_prio_inst([A,B,C],3,4,Prio),
-
+ (var(Continue) ->
+ true
+ ; set_prio_inst([A,B,C],4,5,Prio),
+ %set_prio_inst([A,B,C],3,4,Prio),
my_suspend(mult_int(A,_,B,_,C,_), Prio, (A,B,C) -> suspend:constrained)).
check_mult_int_ineqs(A,B,C) :-
@@ -2019,89 +2018,89 @@ check_zero_and_mult_interval(Val1,Val2,Val) :- !,
congr_mult_directe(Val1,Val2,Val).
*/
check_zero_and_mult_interval(Val1,Val2,Val) :-
- (get_type(Val,_) ->
- true
- ; % Val non initialise
- mfd:dvar_range(Val1,Low1,High1),
- mfd:dvar_range(Val2,Low2,High2),
- mult_intervals(Low1..High1,Low2..High2,Low,High),
- mfd:quiet_set_intervals(Val,[Low..High])),
- %% On fait le menage (on l'a peut etre enleve au tour precedent)
- (not_unify(Val,0) ->
- mfd:dvar_remove_element(Val1,0),
- mfd:dvar_remove_element(Val2,0),
- mult_interval(Val1,Val2,Val)
- ; (not_unify(Val1,0) ->
- (not_unify(Val2,0) ->
- mult_interval(Val1,Val2,Val)
- ; %% On met 0 de cote pour le resultat
- %% et on calcule sur une copie de Val2 privee de 0
- ((mfd:copy_domain(Val1,CVal1),
- get_congr(Val1,C1,M1),
- launch_congr(CVal1,C1,M1),
- mfd:copy_domain(Val2,CVal2),
- get_congr(Val2,C2,M2),
- launch_congr(CVal2,C2,M2),
- mfd:dvar_remove_element(CVal2,0),
- mfd:copy_domain(Val,CVal),
- get_congr(Val,C,M),
- launch_congr(CVal,C,M),
- mfd:dvar_remove_element(CVal,0),
- copy_delta(Val1,Val2,CVal1,CVal2),
- mult_interval(CVal1,CVal2,CVal))
- ->
- %% mult_interval a pu modifier CVal1 et CVal2
- %% On ne peut recopier tel quel le delta(CVal1,CVal2)
- mfd:dvar_domain(CVal1,DomCVal1),
- mfd:dvar_set(Val1,DomCVal1),
- mfd:dvar_domain(CVal2,DomCVal2),
- mfd:dom_union(dom([0]),DomCVal2,NDomVal2),
- mfd:dvar_set(Val2,NDomVal2),
- mfd:dvar_domain(CVal,DomCVal),
- mfd:dom_union(dom([0]),DomCVal,NDomVal),
- mfd:dvar_set(Val,NDomVal)
- ; %% On a echoue en elevant 0 de Val2
- %% donc solution uniquement pour Val2 = 0
- protected_unify(Val2 = 0),
- protected_unify(Val = 0)))
- ; (not_unify(Val2,0) ->
- %% On met 0 de cote pour le resultat
- %% et on calcule sur une copie de Val1 privee de 0
- ((mfd:copy_domain(Val1,CVal1),
- get_congr(Val1,C1,M1),
- launch_congr(CVal1,C1,M1),
- mfd:dvar_remove_element(CVal1,0),
- mfd:copy_domain(Val2,CVal2),
- get_congr(Val2,C2,M2),
- launch_congr(CVal2,C2,M2),
- mfd:copy_domain(Val,CVal),
- get_congr(Val,C,M),
- launch_congr(CVal,C,M),
- mfd:dvar_remove_element(CVal,0),
- copy_delta(Val1,Val2,CVal1,CVal2),
- mult_interval(CVal1,CVal2,CVal))
- ->
- %% mult_interval a pu modifier CVal1 et CVal2
- %% On ne peut recopier tel quel le delta(CVal1,CVal2)
- mfd:dvar_domain(CVal1,DomCVal1),
- mfd:dom_union(dom([0]),DomCVal1,NDomVal1),
- mfd:dvar_set(Val1,NDomVal1),
- mfd:dvar_domain(CVal2,DomCVal2),
- mfd:dvar_set(Val2,DomCVal2),
- mfd:dvar_domain(CVal,DomCVal),
- mfd:dom_union(dom([0]),DomCVal,NDomVal),
- mfd:dvar_set(Val,NDomVal)
- ; %% On a echoue en elevant 0 de Val1
- %% donc solution uniquement pour Val1 = 0
- protected_unify(Val1 = 0),
- protected_unify(Val = 0))
- ; mult_interval(Val1,Val2,Val)))),
- congr_mult_directe(Val1,Val2,Val).
+ (get_type(Val,_) ->
+ true
+ ; % Val non initialise
+ mfd:dvar_range(Val1,Low1,High1),
+ mfd:dvar_range(Val2,Low2,High2),
+ mult_intervals(Low1..High1,Low2..High2,Low,High),
+ mfd:quiet_set_intervals(Val,[Low..High])),
+ % On fait le menage (on l'a peut etre enleve au tour precedent)
+ (not_unify(Val,0) ->
+ mfd:dvar_remove_element(Val1,0),
+ mfd:dvar_remove_element(Val2,0),
+ mult_interval(Val1,Val2,Val)
+ ; (not_unify(Val1,0) ->
+ (not_unify(Val2,0) ->
+ mult_interval(Val1,Val2,Val)
+ ; % On met 0 de cote pour le resultat
+ % et on calcule sur une copie de Val2 privee de 0
+ ((mfd:copy_domain(Val1,CVal1),
+ get_congr(Val1,C1,M1),
+ launch_congr(CVal1,C1,M1),
+ mfd:copy_domain(Val2,CVal2),
+ get_congr(Val2,C2,M2),
+ launch_congr(CVal2,C2,M2),
+ mfd:dvar_remove_element(CVal2,0),
+ mfd:copy_domain(Val,CVal),
+ get_congr(Val,C,M),
+ launch_congr(CVal,C,M),
+ mfd:dvar_remove_element(CVal,0),
+ copy_delta(Val1,Val2,CVal1,CVal2),
+ mult_interval(CVal1,CVal2,CVal))
+ ->
+ % mult_interval a pu modifier CVal1 et CVal2
+ % On ne peut recopier tel quel le delta(CVal1,CVal2)
+ mfd:dvar_domain(CVal1,DomCVal1),
+ mfd:dvar_set(Val1,DomCVal1),
+ mfd:dvar_domain(CVal2,DomCVal2),
+ mfd:dom_union(dom([0]),DomCVal2,NDomVal2),
+ mfd:dvar_set(Val2,NDomVal2),
+ mfd:dvar_domain(CVal,DomCVal),
+ mfd:dom_union(dom([0]),DomCVal,NDomVal),
+ mfd:dvar_set(Val,NDomVal)
+ ; % On a echoue en elevant 0 de Val2
+ % donc solution uniquement pour Val2 = 0
+ protected_unify(Val2 = 0),
+ protected_unify(Val = 0)))
+ ; (not_unify(Val2,0) ->
+ % On met 0 de cote pour le resultat
+ % et on calcule sur une copie de Val1 privee de 0
+ ((mfd:copy_domain(Val1,CVal1),
+ get_congr(Val1,C1,M1),
+ launch_congr(CVal1,C1,M1),
+ mfd:dvar_remove_element(CVal1,0),
+ mfd:copy_domain(Val2,CVal2),
+ get_congr(Val2,C2,M2),
+ launch_congr(CVal2,C2,M2),
+ mfd:copy_domain(Val,CVal),
+ get_congr(Val,C,M),
+ launch_congr(CVal,C,M),
+ mfd:dvar_remove_element(CVal,0),
+ copy_delta(Val1,Val2,CVal1,CVal2),
+ mult_interval(CVal1,CVal2,CVal))
+ ->
+ % mult_interval a pu modifier CVal1 et CVal2
+ % On ne peut recopier tel quel le delta(CVal1,CVal2)
+ mfd:dvar_domain(CVal1,DomCVal1),
+ mfd:dom_union(dom([0]),DomCVal1,NDomVal1),
+ mfd:dvar_set(Val1,NDomVal1),
+ mfd:dvar_domain(CVal2,DomCVal2),
+ mfd:dvar_set(Val2,DomCVal2),
+ mfd:dvar_domain(CVal,DomCVal),
+ mfd:dom_union(dom([0]),DomCVal,NDomVal),
+ mfd:dvar_set(Val,NDomVal)
+ ; % On a echoue en elevant 0 de Val1
+ % donc solution uniquement pour Val1 = 0
+ protected_unify(Val1 = 0),
+ protected_unify(Val = 0))
+ ; mult_interval(Val1,Val2,Val)))),
+ congr_mult_directe(Val1,Val2,Val).
copy_delta(A,B,CA,CB) :-
- (get_deltas(A,B,S,C) ->
- launch_delta(CA,CB,S,C)
- ; true).
+ (get_deltas(A,B,S,C) ->
+ launch_delta(CA,CB,S,C)
+ ; true).
%% Multiplication intervalle par intervalle de Val1 par Val2
%% Puis intersection du domaine calcule
diff --git a/Src/COLIBRI/col_solve.pl b/Src/COLIBRI/col_solve.pl
index b5484eb96..857883376 100644
--- a/Src/COLIBRI/col_solve.pl
+++ b/Src/COLIBRI/col_solve.pl
@@ -807,19 +807,19 @@ smt_test(TO,Size) :-
%StrDir = "./QF_FP/ramalho/", % 4 (min_solve)(cvc4 19)(bitwuzla 17)
%StrDir = "./QF_FP/griggio/", % 42 (min_solve, delta 0 pour cast
% float->double) 51 sans simplex !! (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/schanda/spark/", % 6 (min_solve avec X =< (X+Y)/2 =< Y) (ncvc4 8)(bitwuzla 3)
%StrDir = "./QF_FP/wintersteiger/", % tout OK
%-----------------------------------------------------------------
- StrDir = "./QF_UF/", %
+ %StrDir = "./QF_UF/", % 426 (pour 1061)
%----------------------------------------------------------------
%StrDir = "./QF_AUFBV/", %
%----------------------------------------------------------------
- %StrDir = "./QF_UFIDL/", %
+ %StrDir = "./QF_UFIDL/", % 290 (pour 329)
%----------------------------------------------------------------
%StrDir = "./QF_UFLIA/", % 104 (pour 129)
%----------------------------------------------------------------
- %StrDir = "./QF_UFLRA/", % 142 (pour 384)
+ %StrDir = "./QF_UFLRA/", % 141 (pour 384)
%----------------------------------------------------------------
%StrDir = "./QF_ABV/bench_ab/",
%StrDir = "./QF_ABV/bmc-arrays/",
diff --git a/Src/COLIBRI/notify.pl b/Src/COLIBRI/notify.pl
index 143f14842..e49d8f8a7 100755
--- a/Src/COLIBRI/notify.pl
+++ b/Src/COLIBRI/notify.pl
@@ -194,16 +194,15 @@ wake_if_other_scheduled :-
%% avec un niveau de priorite inferieur strictement a "Prio"
wake_if_other_scheduled(1) :- !.
wake_if_other_scheduled(Prio) :-
- WPrio is max(1,Prio - 1),
- last_scheduled(ScheduledSusps),
- (check_no_scheduled(Prio,ScheduledSusps) ->
+ (check_no_scheduled_prio(Prio) ->
true
- ; wake_scheduled,
+ ; wake,
true).
-:- export wake_scheduled/0.
-wake_scheduled :-
- wake.
+check_no_scheduled_prio(Prio) :-
+ last_scheduled(ScheduledSusps),
+ check_no_scheduled(Prio,ScheduledSusps).
+
/*
; (getval(use_delta,0)@eclipse ->
diff --git a/Src/COLIBRI/rbox.pl b/Src/COLIBRI/rbox.pl
index edea1d076..7a616ce74 100755
--- a/Src/COLIBRI/rbox.pl
+++ b/Src/COLIBRI/rbox.pl
@@ -381,7 +381,7 @@ is_float_number(Var) :-
float(Var),
!.
is_float_number(V{rbox:rf(RF,_)}) ?-
- atomic(RF),
+ nonvar(RF),
get_type(V,Type),
once (RF == float;
RF == float_int;
diff --git a/Src/COLIBRI/realarith.pl b/Src/COLIBRI/realarith.pl
index fe7469f53..704af1937 100755
--- a/Src/COLIBRI/realarith.pl
+++ b/Src/COLIBRI/realarith.pl
@@ -2263,7 +2263,17 @@ cast_double_to_float_bis(Rnd,A,B) :-
HB1 = HA0
; HB1 = HB0),
set_typed_intervals(B,float_simple,[LB1..HB1]),
- % pas de projection inverse pour l'instant
+ % Si on a deux float_int qui tiennent dans la mantisse simple
+ % on peut intersecter les intervalles des deux !!
+ ((is_float_int_number(A), % donc B aussi
+ is_inside_mantissa(float_simple,A))
+ ->
+ mreal:get_intervals(B,IB),
+ mreal:set_typed_intervals(A,float_simple,IB),
+ mreal:get_intervals(A,IA),
+ mreal:set_typed_intervals(B,float_simple,IA)
+ ; % Pas de projection inverse pour l'instant
+ true),
(ground((A,B)) ->
(var(Rnd) ->
% on peut reduire Rnd
@@ -2297,6 +2307,8 @@ cast_double_to_float_bis(Rnd,A,B) :-
launch_delta_double_to_float(_,D,F) :- !.
/*
+% Le flottant n'a que des zeros en poid faible de la mantisse double
+% quand le flottant cible est "normal"
launch_delta_double_to_float(rne,D,F) ?-
var(A),
var(B),
@@ -2348,6 +2360,16 @@ cast_double_to_float_bis(A,B) :-
get_dvar_fintervals(B,IB1),
inv_cast_double_to_float_intervals(IB1,NIA),
mreal:set_typed_intervals(A,float_double,NIA),
+ % Si on a deux float_int qui tiennent dans la mantisse simple
+ % on peut intersecter les intervalles des deux !!
+ ((is_float_int_number(A), % donc B aussi
+ is_inside_mantissa(float_simple,A))
+ ->
+ mreal:get_intervals(B,NewIB),
+ mreal:set_typed_intervals(A,float_simple,NewIB),
+ mreal:get_intervals(A,NewIA),
+ mreal:set_typed_intervals(B,float_simple,NewIA)
+ ; true),
check_before_susp_cast_double_to_float_bis(A,B))),
check_simple_float_bounds(B),
set_priority(Prio),
@@ -2458,7 +2480,6 @@ check_before_susp_cast_double_to_float_bis(A,B) :-
inv_cast_double_to_float_interval(B,IA),
mreal:set_typed_intervals(A,float_double,[IA])
; cast_double_to_float_ineqs(A,B),
-
my_suspend(cast_double_to_float_bis(A,B),3,(A,B)->suspend:constrained))).
cast_double_to_float_ineqs(A,B) :-
@@ -9958,45 +9979,65 @@ mult_real_ineqs(Type,A,B,C) :-
bin_op_real_ineq(Type,mult_real1,A,B,C).
% seulement dans le cas ou les arguments sont signés
-% et un est instancié
+%mult_real_int_ineqs(SA,SB,A,B,C) :- !.
mult_real_int_ineqs(SA,SB,A,B,C) :-
- nonvar(SA),
- nonvar(SB),
- var(C),
- (nonvar(A) ->
- var(B),
- Cst = A,
- Other = B
- ; nonvar(B),
- Cst = B,
- Other = A),
- !,
- rational(Cst,RCst),
- (is_real_box_rat(Other,RL) ->
- RH = RL
- ; mreal:dvar_range(Other,RL,RH)),
- % A REVOIRE
- (RL == -1.0Inf ->
- % donc RH <> 1.0Inf, S = neg
- (RCst > 0 ->
- L = RL,
- H is RCst * rational(RH)
- ; H = 1.0Inf,
- L is RCst * rational(RL))
- ; (RH == 1.0Inf ->
- % S = pos
- (RCst > 0 ->
- L is RCst * rational(RL),
- H = 1.0Inf
- ; L = -1.0Inf,
- H is RCst * rational(RL))
- ; B1 is RCst * rational(RL),
- B2 is RCst * rational(RH),
- sort([B1,B2],[L,H]))),
- launch_delta(Other,C,+,L..H).
-mult_real_int_ineqs(SA,SB,A,B,C).
+ (not_zero(C) ->
+ NZ = 1,
+ forbid_zero(real,A),
+ forbid_zero(real,B)
+ ; ((not_zero(A),
+ not_zero(B))
+ ->
+ NZ = 1,
+ forbid_zero(real,C)
+ ; true)),
+ % A revoir et generaliser
+ ((getval(use_delta,1)@eclipse,
+ nonvar(SA),
+ nonvar(SB),
+ var(C))
+ ->
+ once (get_sign(C,SC);true),
+ (var(A) ->
+ mult_real_int_ineqs0(NZ,SC,SA,A,B,C)
+ ; true),
+ (var(B) ->
+ mult_real_int_ineqs0(NZ,SC,SB,B,A,C)
+ ; true)
+ ; true).
+
+mult_real_int_ineqs0(NZ,SC,SOther,Other,Fact,C) :-
+ % Fact * Other = C
+ minus_real_interval(real,C,Other,Diff),
+ mreal:dvar_range(Diff,LD0,HD0),
+ (SOther \== SC ->
+ (SOther == pos ->
+ % C neg, Other >= C
+ HD1 is min(HD0,0.0),
+ LD1 = LD0
+ ; % Other neg, C pos, Other =< C
+ HD1 = HD0,
+ LD1 is min(LD0,0.0))
+ ; LD1 = LD0,
+ HD1 = HD0),
+ (LD1 == -1.0Inf ->
+ LD = LD1
+ ; ((LD1 == 0.0,
+ nonvar(NZ),
+ not_unify(Fact,1.0))
+ ->
+ LD = 1_1
+ ; rational(LD1,LD))),
+ (HD1 == 1.0Inf ->
+ HD = HD1
+ ; ((HD1 == 0.0,
+ nonvar(NZ),
+ not_unify(Fact,1.0))
+ ->
+ HD is -1_1
+ ; rational(HD1,HD))),
+ launch_delta(Other,C,+,LD..HD).
-
op_rel(<,>).
op_rel(>,<).
op_rel(=<,>=).
@@ -12919,9 +12960,10 @@ check_div_mult_exact(Type,A,B,C,_,Continue) :-
% average_real_ineqs(Type,A,B,C) :- !.
% Bizarre !!
average_real_ineqs(Type,A,B,C) :-
- ((B == 2.0,
- get_saved_cstr_suspensions(LSusp),
- member((S,add_real1(Type,X,Y,AA)),LSusp),
+ B == 2.0,
+ !,
+ get_saved_cstr_suspensions(LSusp),
+ ((member((S,add_real1(Type,X,Y,AA)),LSusp),
AA == A,
var(X),
var(Y),
@@ -12929,6 +12971,7 @@ 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)
@@ -12939,7 +12982,76 @@ average_real_ineqs(Type,A,B,C) :-
launch_geq_real(Type,C,X)
; launch_geq_real(Type,X,C),
launch_geq_real(Type,C,Y)))
- ; true).
+ ; ((once (member((_,cast_float_to_double_bis(FA,DA)),LSusp),
+ DA == A),% double(FA)/2 = C
+ get_cstr_suspensions(FA,LSFA),
+ once (member(SA,LSFA),
+ get_suspension_data(SA,goal,div_real1(float_simple,FFA,D,FAd2)),
+ D == 2.0,
+ FFA == FA),
+ get_cstr_suspensions(FAd2,LSFAd2),
+ member(SFAd2,LSFAd2),
+ get_suspension_data(SFAd2,goal,
+ cast_float_to_double_bis(FFAd2,DAd2)),
+ FFAd2 == FAd2) % double(FA/2) = DAd2
+ ->
+ % double(FA)/2 = double(FA/2)
+ protected_unify(C,DAd2)
+ ; ((once (member_begin_end((_,cast_float_to_double_bis(CC,DC)),LSusp,NLSusp,End,End),
+ CC == C, % double(A/2) = DC
+ member((_,cast_float_to_double_bis(AA,DA)),NLSusp),
+ AA == A),% double(A) = DA
+ get_cstr_suspensions(DA,LSDA),
+ member(SDA,LSDA),
+ get_suspension_data(SA,goal,div_real1(float_double,DDA,D,DAd2)),
+ D == 2.0,
+ DDA == DA) % double(A)/2 = DAd2
+ ->
+ % double(A/2) = double(A)/2
+ protected_unify(DC,DAd2)
+ ; % normal(C),A/2 = C, float(double(A)/2) ?
+ ((Type == float_simple,
+ not not (isNormal(Type,C,BN),
+ BN == 1),
+ once (member((_,cast_float_to_double_bis(AA,DA)),LSusp),
+ AA == A),
+ % double(A) = DA
+ get_cstr_suspensions(DA,LSDA),
+ once (member(SDA,LSDA),
+ get_suspension_data(SDA,goal,div_real1(_,DDA,D,
+ DAd2)),
+ D == 2.0,
+ DDA == DA),
+ % double(A)/2 == DAd2
+ get_cstr_suspensions(DAd2,LSDAd2),
+ member(SDAd2,LSDAd2),
+ get_suspension_data(SDAd2,goal,
+ cast_double_to_float_bis(DDAd2,
+ FDAd2)),
+ DDAd2 == DAd2)% floar(double(A)/2) = FDAD2
+ ->
+ protected_unify(C,FDAd2)
+ ; % float(double(A))/2 = A/2 ?
+ ((once (member_begin_end((_,cast_float_to_double_bis(FA,AA)),
+ LSusp,NLSusp,End,End),
+ AA == A, % double(FA) = A
+ % float(double(FA)/2) ?
+ member((_,cast_double_to_float_bis(CC,FC)),
+ NLSusp),
+ CC == C),
+ % FA/2 = FAd2 ?
+ get_cstr_suspensions(FA,LSFA),
+ member(SFA,LSFA),
+ get_suspension_data(SFA,goal,div_real1(_,FFA,D,FAd2)),
+ D = 2.0,
+ FFA == FA,
+ not not (isNormal(float_simple,FAd2,BN),
+ BN == 1))
+ ->
+ call(spy_here)@eclipse,
+ protected_unify(FC,FAd2)
+ ; true))))).
+average_real_ineqs(Type,A,B,C).
%% 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
@@ -13095,19 +13207,36 @@ div_real_ineqs(Type,A,B,C) :-
%div_real_ineqs(Type,A,B,C).
div_real_ineqs(Type,A,B,C) :-
bin_op_real_ineq(Type,div_real1,A,B,C).
-
+
+%On peut etre plus precis sur les float_int
div_real_int_ineqs(SA,SB,A,B,C) :-
- var(A),
- var(C),
- nonvar(SA),
- (nonvar(B),
- not_inf_bounds(B),
- rational(B,RB);
- is_real_box_rat(B,RB)),
- !,
- InvB is 1_1/RB,
- mult_real_int_ineqs(SA,SB,A,InvB,C).
-div_real_int_ineqs(_,_,_,_,_).
+ (not_zero(C) ->
+ NZ = 1,
+ forbid_zero(real,A)
+ ; (not_zero(A) ->
+ NZ = 1,
+ forbid_zero(real,C)
+ ; true)),
+ % A revoir et generaliser
+ ((getval(use_delta,1)@eclipse,
+ nonvar(SA),
+ nonvar(SB),
+ var(C))
+ ->
+ once (get_sign(C,SC);true),
+ (var(A) ->
+ mult_real_int_ineqs0(NZ,SC,SA,A,B,C),
+ % en float_int B divise A donc A=C*B
+ ((var(B),
+ is_float_int_number(A),
+ is_float_int_number(B),
+ is_float_int_number(C))
+ ->
+ mult_real_int_ineqs0(NZ,SA,SB,B,C,A)
+ ; true)
+ ; true)
+ ; true).
+
exists_mult_with_abs_op_B(SB,B) :-
get_saved_cstr_suspensions(LSusp),
@@ -13890,8 +14019,12 @@ div_real_inst0(Type,A,B,C,Continue) :-
; Continue0 = 1)))
; (float(B) ->
(float(C) ->
- inv1_div_real_float_min_max(Type,C,B,A1,A2,Continue),
- mreal:set_typed_intervals(A,Type,[A1..A2])
+ inv1_div_real_float_min_max(Type,C,B,A1,A2,Continue0),
+ mreal:set_typed_intervals(A,Type,[A1..A2]),
+ % Essai BM
+ (var(A) ->
+ Continue = 1
+ ; true)
; % A et C variables
((Type \== real,
dvar_size(Type,C,2))
diff --git a/Src/COLIBRI/solve.pl b/Src/COLIBRI/solve.pl
index 60153db4d..1d6bbbb9e 100644
--- a/Src/COLIBRI/solve.pl
+++ b/Src/COLIBRI/solve.pl
@@ -11046,12 +11046,24 @@ remove_seen_vars([V|Seen],L,NL) :-
; remove_seen_vars(Seen,L,NL)).
+/*
choose_fd_var([Adj|UseList],Var,Size,NUseList) :-
% Recolte des variables de plus grand cycle
% ne dependant d'aucune autre (MaxCycleVars)
% et apparaissant dans une adjacence singleton ou paire avec resultat connu
% ou bien dans une adjacence ne contenant que des MaxCycleVars
+ min_vars([Adj|UseList],MinVars,NUseList),
+ MinVars \== [],
+ var_with_max_cstr_min_dom(MinVars,Var,Size).
+% var_with_min_dom_max_cstr(MinVars,Var,Size).
+*/
+% Nouvelle version plus simple
+choose_fd_var([Adj|UseList],Var,Size,NUseList) :-
+ % Recolte des variables de plus grand cycle
+ % ne dependant d'aucune autre (MaxCycleVars)
+ % et apparaissant dans une adjacence singleton ou paire avec resultat connu
+ % ou bien dans une adjacence ne contenant que des MaxCycleVars
delayed_goals(DG),
term_variables(DG,Vars0),
filter_constrained_vars(Vars0,MinVars0),
@@ -11060,15 +11072,12 @@ choose_fd_var([Adj|UseList],Var,Size,NUseList) :-
(is_real_box_rat(V,_) ->
OV = IV
; OV = [V|IV])),
-% min_vars([Adj|UseList],MinVars,NUseList),
-
MinVars \== [],
-%% var_with_min_dom_max_cstr(MinVars,Var,Size).
-% var_with_max_cstr_min_dom(MinVars,Var,Size).
leaf_vars([Adj|UseList],Leaves,NUseList),
leaf_var_with_max_cstr_min_dom(MinVars,[],Var,Size).
% leaf_var_with_max_cstr_min_dom(MinVars,Leaves,Var,Size).
+
leaf_vars(UseList,Leaves,NUseList) :-
(foreach((V,D,A),UseList),
fromto([],IT,OT,NUseList0) do
--
GitLab