diff --git a/Src/COLIBRI/arith.pl b/Src/COLIBRI/arith.pl
index 09d36a45a6ba879d6218e0061905d82cd384e3c5..f7d02ebbf3da94716b3584126c8956f7c331fa3b 100755
--- a/Src/COLIBRI/arith.pl
+++ b/Src/COLIBRI/arith.pl
@@ -5811,74 +5811,72 @@ launch_delta_leq(A,B) :-
launch_delta_leq(_,_).
build_delta_leq(A,B,S,Inter) :-
- mfd:dvar_range(A,MinA,MaxA),
- mfd:dvar_range(B,MinB,MaxB),
- DiffMax is MaxB - MinA,
- (MaxA < MinB ->
- %% Forme resolue
- DiffMin is MinB - MaxA
- ; (not_unify(A,B) ->
- DiffMin = 1
- ; DiffMin = 0)),
- update_delta_cost_with_congr(A,B,+,DiffMin..DiffMax,S,Inter).
-
-
- launch_delta_leq_lt(=,Cost,A,B) :-
- %% On a reduit le delta a une distance exacte
- %% on lance le correspondant
- add(A,Cost,B).
- launch_delta_leq_lt(+,Inter,A,B) :-
- ndelta:launch_delta(A,B,+,Inter),
- ((exists_delta_Rel(A,B,Rel,S,Delta),
- Delta \== Inter)
- ->
- update_args_from_delta(Rel,S,Delta,A,B,_,_)
- ; true).
+ mfd:dvar_range(A,MinA,MaxA),
+ mfd:dvar_range(B,MinB,MaxB),
+ DiffMax is MaxB - MinA,
+ (MaxA < MinB ->
+ % Forme resolue
+ DiffMin is MinB - MaxA
+ ; (not_unify(A,B) ->
+ DiffMin = 1
+ ; DiffMin = 0)),
+ update_delta_cost_with_congr(A,B,+,DiffMin..DiffMax,S,Inter).
+
+
+launch_delta_leq_lt(=,Cost,A,B) :-
+ % On a reduit le delta a une distance exacte
+ % on lance le correspondant
+ add(A,Cost,B).
+launch_delta_leq_lt(+,Inter,A,B) :-
+ ndelta:launch_delta(A,B,+,Inter),
+ ((exists_delta_Rel(A,B,Rel,S,Delta),
+ Delta \== Inter)
+ ->
+ update_args_from_delta(Rel,S,Delta,A,B,_,_)
+ ; true).
-:- export
- update_delta_cost_with_congr/6.
+:- 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,NS,NC) :-
- ((exists_congr(X,CX,MX),
- exists_congr(Y,CY,MY),
- MDV is gcd(MX,MY),
- MDV > 1)
- ->
- %% La congruence de Y-X donne une congruence du delta
- CDV is (CY-CX) mod MDV,
- update_delta_with_congr(CDV,MDV,S,C,NS,NC)
- ; NS = S,
- NC = C).
+ ((exists_congr(X,CX,MX),
+ exists_congr(Y,CY,MY),
+ MDV is gcd(MX,MY),
+ MDV > 1)
+ ->
+ % La congruence de Y-X donne une congruence du delta
+ CDV is (CY-CX) mod MDV,
+ update_delta_with_congr(CDV,MDV,S,C,NS,NC)
+ ; NS = S,
+ NC = C).
-:- export
- update_delta_with_congr/6.
+:- export update_delta_with_congr/6.
update_delta_with_congr(0,1,S,C,S,C) :- !.
update_delta_with_congr(R,Mod,=,Cost,=,Cost) :- !,
- %% On verifie seulement
- (R mod Mod) =:= (Cost mod Mod).
+ % On verifie seulement
+ (R mod Mod) =:= (Cost mod Mod).
update_delta_with_congr(R,Mod,S0,Min..Max,NS,NC) :-
- %% S0 = '+'|'#'
- (S0 == '#' ->
- ((Min > 0;
- Max < 0)
- ->
- Inter0 = [Min..Max]
- ; list_to_intervals(integer,[Min.. -1,1..Max],Inter0))
- ; Inter0 = [Min..Max]),
- reduce_congr_bounds_interval_list(Inter0,R,Mod,Inter),
- Inter \== [],
- interval_range(Inter,L,H),
- (L == H ->
- NS = '=',
- NC = L
- ; ((S0 == '#',
- L < 0,
- H > 0)
- ->
- NS = '#'
- ; NS = +),
- NC = L..H).
+ % S0 = '+'|'#'
+ (S0 == '#' ->
+ ((Min > 0;
+ Max < 0)
+ ->
+ Inter0 = [Min..Max]
+ ; list_to_intervals(integer,[Min.. -1,1..Max],Inter0))
+ ; Inter0 = [Min..Max]),
+ reduce_congr_bounds_interval_list(Inter0,R,Mod,Inter),
+ Inter \== [],
+ interval_range(Inter,L,H),
+ (L == H ->
+ NS = '=',
+ NC = L
+ ; ((S0 == '#',
+ L < 0,
+ H > 0)
+ ->
+ NS = '#'
+ ; NS = +),
+ NC = L..H).
@@ -5981,43 +5979,43 @@ notify_ineq_to_int_cstrs_if_new_rel(OldRel,A,B).
launch_delta_lt(A,A) ?- !,
- fail.
+ fail.
launch_delta_lt(A,B) :-
- %% A < B avec MinA < MinB at MaxA < MaxB
- %% donc il existe Min..Max
- %% tel que A + Min..Max = B
- %% avec Min >= max(1,MinB-MaxA)
- %% et Max =< MaxB-MinA
- var(A),
- var(B),!,
- build_delta_lt(A,B,S,Inter),
- (Inter == 0 ->
- fail
- ; launch_delta_leq_lt(S,Inter,A,B)).
+ % A < B avec MinA < MinB at MaxA < MaxB
+ % donc il existe Min..Max
+ % tel que A + Min..Max = B
+ % avec Min >= max(1,MinB-MaxA)
+ % et Max =< MaxB-MinA
+ var(A),
+ var(B),!,
+ build_delta_lt(A,B,S,Inter),
+ (Inter == 0 ->
+ fail
+ ; launch_delta_leq_lt(S,Inter,A,B)).
launch_delta_lt(_,_).
build_delta_lt(A,B,S,Inter) :-
- mfd:dvar_range(A,MinA,MaxA),
- mfd:dvar_range(B,MinB,MaxB),
- DiffMax is MaxB - MinA,
- (MaxA < MinB ->
- %% Forme resolue
- DiffMin is MinB - MaxB
- ; DiffMin = 1),
- update_delta_cost_with_congr(A,B,+,DiffMin..DiffMax,S,Inter).
+ mfd:dvar_range(A,MinA,MaxA),
+ mfd:dvar_range(B,MinB,MaxB),
+ DiffMax is MaxB - MinA,
+ (MaxA < MinB ->
+ % Forme resolue
+ DiffMin is MinB - MaxB
+ ; DiffMin = 1),
+ update_delta_cost_with_congr(A,B,+,DiffMin..DiffMax,S,Inter).
launch_lt(A,B) :-
- launch_gt(B,A).
+ launch_gt(B,A).
launch_leq(A,B) :-
- launch_geq(B,A).
+ launch_geq(B,A).
%% Pour faciliter l'utilisation directe des contraintes
lt(A,B) :-
- gt(B,A).
+ gt(B,A).
leq(A,B) :-
- geq(B,A).
+ geq(B,A).
/************************************************************************
diff --git a/Src/COLIBRI/check_ineq.pl b/Src/COLIBRI/check_ineq.pl
index cbdc2a66f2e0b20ed6245f9a9a737aeab5aabd0f..280ae45a4fb2b7cfdeb97658678fb987acd36882 100644
--- a/Src/COLIBRI/check_ineq.pl
+++ b/Src/COLIBRI/check_ineq.pl
@@ -1186,54 +1186,54 @@ saturate_diff_int_inequalities(A,B,1).
launch_delta_diff_int(A,B) :-
getval(use_delta,1)@eclipse,
!,
- %% On cherche MinY..MaxY tel que
- %% A + Y = B
- mfd:dvar_range(A,MinA,MaxA),
- mfd:dvar_range(B,MinB,MaxB),
- %% MinY..MaxY = MinB-MaxA..MaxB-MinA
- MinY is MinB-MaxA,
- MaxY is MaxB-MinA,
- (MinY == 0 ->
- S = '+',
- LowY = 1,
- HighY = MaxY
- ; LowY = MinY,
- (MaxY == 0 ->
- S = '+',
- HighY = -1
- ; S = '#',
- HighY = MaxY)),
- ndelta:launch_delta(A,B,S,LowY..HighY),
- ((exists_delta_Rel(A,B,Rel,NS,Delta),
- Delta \== LowY..HighY)
- ->
- update_args_from_delta(Rel,Delta,A,B)
- ; true).
+ % On cherche MinY..MaxY tel que
+ % A + Y = B
+ mfd:dvar_range(A,MinA,MaxA),
+ mfd:dvar_range(B,MinB,MaxB),
+ % MinY..MaxY = MinB-MaxA..MaxB-MinA
+ MinY is MinB-MaxA,
+ MaxY is MaxB-MinA,
+ (MinY == 0 ->
+ S = '+',
+ LowY = 1,
+ HighY = MaxY
+ ; LowY = MinY,
+ (MaxY == 0 ->
+ S = '+',
+ HighY = -1
+ ; S = '#',
+ HighY = MaxY)),
+ ndelta:launch_delta(A,B,S,LowY..HighY),
+ ((exists_delta_Rel(A,B,Rel,NS,Delta),
+ Delta \== LowY..HighY)
+ ->
+ update_args_from_delta(Rel,Delta,A,B)
+ ; true).
launch_delta_diff_int(A,B).
check_delta_diff_int_two_value_domain(A,B) :-
- two_value_domain(A,DA),
- two_value_domain(B,DA),!,
- ((ndelta:get_delta_before_after(A,BA,AA),
- (DeltasA = BA; DeltasA = AA),
- member((X,'#',_),DeltasA),
- X \== B,
- two_value_domain(X,DA))
- ->
- protected_unify(X = B)
- ; ((ndelta:get_delta_before_after(B,BB,AB),
- (DeltasB = BB; DeltasB = AB),
- member((X,'#',_),DeltasB),
- X \== A,
- two_value_domain(X,DA))
- ->
- protected_unify(X = A)
- ; true)),
- (ndelta:get_deltas(A,B,_,_) ->
- true
- ; %% Les autres contraintes du domaine a deux valeurs
- %% peuvent exploiter le nouveau '#'
- my_notify_constrained(A)).
+ two_value_domain(A,DA),
+ two_value_domain(B,DA),!,
+ ((ndelta:get_delta_before_after(A,BA,AA),
+ (DeltasA = BA; DeltasA = AA),
+ member((X,'#',_),DeltasA),
+ X \== B,
+ two_value_domain(X,DA))
+ ->
+ protected_unify(X = B)
+ ; ((ndelta:get_delta_before_after(B,BB,AB),
+ (DeltasB = BB; DeltasB = AB),
+ member((X,'#',_),DeltasB),
+ X \== A,
+ two_value_domain(X,DA))
+ ->
+ protected_unify(X = A)
+ ; true)),
+ (ndelta:get_deltas(A,B,_,_) ->
+ true
+ ; % Les autres contraintes du domaine a deux valeurs
+ % peuvent exploiter le nouveau '#'
+ my_notify_constrained(A)).
check_delta_diff_int_two_value_domain(_,_).
diff --git a/Src/COLIBRI/check_lin_expr.pl b/Src/COLIBRI/check_lin_expr.pl
index dba134e183f6c2be39805e0eb332fc28656aeb1c..748134c505430bbfcaaac9f80605347e7394cec3 100755
--- a/Src/COLIBRI/check_lin_expr.pl
+++ b/Src/COLIBRI/check_lin_expr.pl
@@ -50,66 +50,96 @@ try_check_exists_lin_expr_giving_diff_args(Type,A,B,Stop) :-
% On limite la profondeur des termes explores
getval(depth_lin_expr,MaxDepth)@eclipse,
% On construit "une" expression lineaire calculant A
- % L1 est une somme de Ni*Xi
- % C1 est un rationnel
+ % L1 est une liste de sommes de Ni*Xi
+ % C1 est une liste de rationnels
init_vardef,
(number(A) ->
- L1 = [],
- rational(A,C1)
- ; (var(B) ->
- Keep = [B]
- ; Keep = []),
- get_sum_giving(Type,1_1*A,MaxDepth,Keep,[],0_1,L10,C1),
- remove_null_fact(L10,L1)),
- ((Type == int,
- get_congr_from_lin_expr(L1,C1,Rest1,Mod1))
- ->
- launch_congr(A,Rest1,Mod1)
+ Res1 = [([],RA)],
+ rational(A,RA)
+ ; get_lsum_giving(Type,1_1*A,[],MaxDepth,[([],0_1)],Res1)),
+ (Type == int ->
+ (foreach((S1,CS1),Res1),
+ param(A) do
+ (get_congr_from_lin_expr(S1,CS1,Rest1,Mod1) ->
+ launch_congr(A,Rest1,Mod1)
+ ; true))
; true),
- term_variables(L1,NKeep),
- (number(B) ->
- L2 = [],
- rational(B,C2)
- ; get_sum_giving(Type,1_1*B,MaxDepth,NKeep,[],0_1,L20,C2),
- remove_null_fact(L20,L2)),
- ((Type == int,
- get_congr_from_lin_expr(L2,C2,Rest2,Mod2))
- ->
- launch_congr(B,Rest2,Mod2)
+ (number(B) ->
+ Res2 = [([],RB)],
+ rational(B,RB)
+ ; get_lsum_giving(Type,1_1*B,[],MaxDepth,[([],0_1)],Res2)),
+ (Type == int ->
+ (foreach((S2,CS2),Res22),
+ param(B) do
+ (get_congr_from_lin_expr(S2,CS2,Rest2,Mod2) ->
+ launch_congr(B,Rest2,Mod2)
+ ; true))
; true),
- remove_common_vars(L1,L2,NL1,NL2,Work),
+ %remove_common_vars(L1,L2,NL1,NL2,Work),
% on peut echouer ici
- (NL1,C1) \== (NL2,C2),
+ (length(Res1) > length(Res2) ->
+ L1 = Res2,
+ L2 = Res1
+ ; L1 = Res1,
+ L2 = Res2),
+ not (member((NS1,NC),L1),
+ member((NS2,NC),L2),
+ same_lin_sum(NS1,NS2)),
% on peut reduire A et B ?
- eval_lin_expr(Type,L1,C1,R1),
- eval_lin_expr(Type,L2,C2,R2),
+ (foreach((NS1,NC1),Res1),
+ fromto(-1.0Inf .. 1.0Inf,IR1,OR1,R1),
+ param(Type) do
+ eval_lin_expr(Type,NS1,NC1,R),
+ eval_intersect(R,IR1,OR1)),
+ (foreach((NS2,NC2),Res2),
+ fromto(-1.0Inf .. 1.0Inf,IR2,OR2,R2),
+ param(Type) do
+ eval_lin_expr(Type,NS2,NC2,R),
+ eval_intersect(R,IR2,OR2)),
% R1 et R2 sont des nombres ou des intervalles
% qui peuvent etre utilises pour reduire A et B
reduce_var_from_rat_interval(Type,A,R1),
reduce_var_from_rat_interval(Type,B,R2),
- getval(use_delta,UD)@eclipse,
- no_delta,
- (not_unify(A,B) ->
- setval(use_delta,UD)@eclipse,
- % la forme simplifiee des expressions lineaires
- % est résolue, les contraintes correspondantes
- % gerent les reductions sur A et B, et le diff
- % est impliqué par le store
- Stop = 1
- ; setval(use_delta,UD)@eclipse,
- ((number(A),Val = A,Other = B;
- number(B),Val = B,Other = A)
- ->
- (Type == int ->
- mfd:dvar_remove_element(Other,Val),
+ ((number(A),Val = A,Other = B;
+ number(B),Val = B,Other = A)
+ ->
+ (Type == int ->
+ mfd:dvar_remove_element(Other,Val),
+ Stop = 1
+ ; % real
+ (is_float_number(Other) ->
+ mreal:dvar_remove_element(Other,Val),
Stop = 1
- ; % real
- (is_float_number(Other) ->
- mreal:dvar_remove_element(Other,Val),
- Stop = 1
- ; true))
- ; true)).
+ ; true))
+ ; true).
+same_lin_sum(L,L) ?- !.
+same_lin_sum([C*S1|L1],L2) :-
+ member_begin_end(C*S2,L2,NL2,End,End),
+ S1 == S2,
+ !,
+ same_lin_sum(L1,NL2).
+
+eval_intersect(I,I,R) ?- !,
+ R = I.
+eval_intersect(I1,I2,R) :-
+ min_max_inter(I1,L1,H1),
+ min_max_inter(I2,L2,H2),
+ (L1 == -1.0Inf ->
+ L = L2
+ ; (L2 == -1.0Inf ->
+ L = L1
+ ; L is max(L1,L2))),
+ (H1 == 1.0Inf ->
+ H = H2
+ ; (H2 == 1.0Inf ->
+ H = H1
+ ; H is min(H1,H2))),
+ % On peut échouer ici
+ L =< H,
+ (L == H ->
+ R = L
+ ; R = L..H).
%reduce_var_from_rat_interval(real,A,R) :- !.
reduce_var_from_rat_interval(Type,A,R) :-
@@ -141,34 +171,35 @@ reduce_var_from_rat_interval(Type,A,R) :-
; float_of_rat(real,rtp,RH,H)),
set_typed_intervals(A,real,[L..H]))).
+
eval_lin_expr(Type,[],C,C).
eval_lin_expr(Type,[F|L],C,R) :-
- eval_sigma(Type,[F|L],V),
- (C == 0_1 ->
- R = V
- ; add_rat_intervals(Type,C,V,R)).
+ eval_sigma(Type,[F|L],V),
+ (C == 0_1 ->
+ R = V
+ ; add_rat_intervals(Type,C,V,R)).
eval_sigma(Type,[VN1,VN2|LV],R) :- !,
- eval_factor(Type,VN1,R1),
- eval_sigma(Type,[VN2|LV],R2),
- add_rat_intervals(Type,R1,R2,R).
+ eval_factor(Type,VN1,R1),
+ eval_sigma(Type,[VN2|LV],R2),
+ add_rat_intervals(Type,R1,R2,R).
eval_sigma(Type,[VN],R) :-
- eval_factor(Type,VN,R).
+ eval_factor(Type,VN,R).
eval_factor(Type,0_1*V,R) ?- !,
- R = 0_1.
+ R = 0_1.
eval_factor(Type,N*V,R) :-
number(V),
!,
R is rational(N)*rational(V).
eval_factor(Type,N*V,R) :-
- mult_rat_intervals(Type,N,V,R).
+ mult_rat_intervals(Type,N,V,R).
mult_rat_intervals(Type,A,B,RIAB) :-
to_rat_range(Type,A,LA,HA),
to_rat_range(Type,B,LB,HB),
mult_rat_ranges(LA,HA,LB,HB,RIAB).
-
+
to_rat_range(Type,A,RLA,RHA) :-
(rational(A) ->
RLA = A,
@@ -216,11 +247,11 @@ protected_rat_mult(A,B,C) :-
C is A*B.
protected_rat_mult(A,B,C) ?- !,
(abs(A) =:= 1.0Inf ->
- (B > 0 ->
+ (B > 0_1 ->
C = A
; C is -A)
; % abs(B) =:= 1.0Inf
- (A > 0 ->
+ (A > 0_1 ->
C = B
; C is -B)).
@@ -263,83 +294,116 @@ protected_rat_add(A,B,C) :-
:- export get_congr_from_lin_expr/4.
get_congr_from_lin_expr(Sum,C,R,Mod) :-
- denominator(C,1),
+ denominator(C,1),
numerator(C,IC),
- congr_sum(Sum,IC,0,R,Mod).
+ congr_sum(Sum,IC,0,R,Mod).
congr_sum([],C,M,C,M).
congr_sum([Coeff*Var|Sum],C0,M0,NC,NM) :-
- denominator(Coeff,1),
+ denominator(Coeff,1),
get_congr(Var,CV,MV),
numerator(Coeff,ICoeff),
- congr_mult(CV,MV,0,ICoeff,C1,M1),
- congr_add(C1,M1,C0,M0,C,M),
- congr_sum(Sum,C,M,NC,NM).
+ congr_mult(CV,MV,0,ICoeff,C1,M1),
+ congr_add(C1,M1,C0,M0,C,M),
+ congr_sum(Sum,C,M,NC,NM).
-
-insert_args_in_sum(_,_,[],_,_,Sum,C,Sum,C).
-insert_args_in_sum(Type,Coeff,[CoeffV*V|Args],MaxDepth,Keep,SeenV,SeenC,Sum,C) :-
- NC is Coeff*CoeffV,
- get_sum_giving(Type,NC*V,MaxDepth,Keep,SeenV,SeenC,NSeenV,NSeenC),
- insert_args_in_sum(Type,Coeff,Args,MaxDepth,Keep,NSeenV,NSeenC,Sum,C).
-
-%% Keep contient les variables a conserver
-%% (en traitant A dans add(B,C,A) on garde B et C si on les rencontre)
-get_sum_giving(Type,NV*V,MaxDepth,Keep,SeenV,SeenC,Sum,C) :-
+% toutes les sommes
+insert_largs_in_lsum(Type,Coeff,[],From,MaxDepth,Seen,C,[]).
+insert_largs_in_lsum(Type,Coeff,[Args|LArgs],From,MaxDepth,Seen,C,NLSeen) :-
+ insert_args_in_lsum(Type,Coeff,Args,From,MaxDepth,[(Seen,C)],BNLSeen),
+ append(BNLSeen,ENLSeen,NLSeen),
+ insert_largs_in_lsum(Type,Coeff,LArgs,From,MaxDepth,Seen,C,ENLSeen).
+
+% les descendants d'une seule somme
+insert_args_in_lsum(_,_,[],_,_,L,L).
+insert_args_in_lsum(Type,Coeff,[CoeffV*V|Args],From,MaxDepth,LSeen,NLSeen) :-
+ NC is Coeff*CoeffV,
+ get_lsum_giving(Type,NC*V,From,MaxDepth,LSeen,NLseen0),
+ insert_args_in_lsum(Type,Coeff,Args,From,MaxDepth,NLseen0,NLSeen).
+
+
+get_lsum_giving(Type,NV*V,From,MaxDepth,LSeen,NLSeen) :-
(number(V) ->
- C is SeenC + NV*rational(V),
- Sum = SeenV
- ; ((occurs(V,SeenV),
- member_begin_end(ONV*VV,SeenV,Sum,End,EndSum),
- V == VV)
- ->
- C = SeenC,
- NNV is ONV + NV,
- End = [NNV*V|EndSum]
- ; ((MaxDepth =< 0;
- occurs(V,Keep))
- ->
- C = SeenC,
- Sum = [NV*V|SeenV]
- ; % On peut explorer les add/mult de V
- (get_args_from_add_mult_giving(Type,V,Args) ->
- NMaxDepth is MaxDepth - 1,
- insert_args_in_sum(Type,NV,Args,NMaxDepth,Keep,SeenV,SeenC,Sum,C)
- ; C = SeenC,
- Sum = [NV*V|SeenV])))).
+ % on modifie tous les C de LSeen
+ NVxV is NV*rational(V),
+ (foreach((Seen,C),LSeen),
+ foreach((Seen,NC),NLSeen),
+ param(NVxV) do
+ NC is C + NVxV)
+ ; get_lsum1_giving(Type,NV*V,From,MaxDepth,LSeen,NLSeen)).
+
+get_lsum1_giving(Type,NV*V,From,MaxDepth,[],[]).
+get_lsum1_giving(Type,NV*V,From,MaxDepth,[(Seen,C)|ELSeen],NLSeen) :-
+ ((occurs(V,Seen),
+ member_begin_end(ONV*VV,Seen,NSeen,End,EndNSeen),
+ V == VV)
+ ->
+ NNV is ONV + NV,
+ (NNV == 0_1 ->
+ % plus de V
+ End = EndNSeen
+ ; End = [NNV*V|EndNSeen]),
+ NLSeen = [(NSeen,C)|ENLSeen],
+ get_lsum1_giving(Type,NV*V,From,MaxDepth,ELSeen,ENLSeen)
+ ; (MaxDepth =< 0 ->
+ NSeen = [NV*V|Seen],
+ NLSeen = [(NSeen,C)|ENLSeen],
+ get_lsum1_giving(Type,NV*V,From,MaxDepth,ELSeen,ENLSeen)
+ ; % On peut explorer les add/mult de V
+ (get_args_from_add_mult_giving(Type,V,From,LArgs) ->
+ NMaxDepth is MaxDepth - 1,
+ insert_largs_in_lsum(Type,NV,LArgs,[V|From],NMaxDepth,
+ Seen,C,NLSeen1),
+ append(NLSeen1,ENLSeen,NLSeen),
+ get_lsum1_giving(Type,NV*V,From,MaxDepth,ELSeen,ENLSeen)
+ ; NLSeen = [([NV*V|Seen],C)|ENLSeen],
+ get_lsum1_giving(Type,NV*V,From,MaxDepth,ELSeen,ENLSeen)))).
get_linear_constraints(V,L) :-
(get_lin_cstrs(V,L) ->
true
; L = []).
-get_args_from_add_mult_giving(Type,V,Args) :-
- (get_vardef(V,Args) ->
+get_args_from_add_mult_giving(Type,V,From,NLArgs) :-
+ (get_vardef(V,LArgs) ->
true
; get_linear_constraints(V,LC),
% On cherche en priorite les add/mult/op donnant V
- get_args_from_add_mult_giving(Type,LC,V,Args,NLC),
- (nonvar(Args) ->
- true
- ; NLC \== [],
- % On cherche en inversant les add/op/mult
- get_args_from_other_add_op_mult(Type,NLC,V,Args)),
- set_vardef(V,Args)).
-
-get_args_from_add_mult_giving(Type,[],V,Args,[]).
-get_args_from_add_mult_giving(Type,[Goal|LC],V,Args,NLC) :-
- functor(Goal,F,_),
- (occurs(F,(add_int,mult_int,op,add_real,minus_real,mult_real,div_real)) ->
- (Type == int ->
- ((Goal = add_int(X,Y,Z);
- Goal = op(X,Z))
- ->
- (Z == V ->
- (F == add_int ->
- Args = [1_1*X,1_1*Y]
- ; Args = [-1_1*X])
- ; NLC = [Goal|ENLC],
- get_args_from_add_mult_giving(Type,LC,V,Args,ENLC))
+ get_args_from_add_mult_giving(Type,LC,V,LArgs,ELArgs,NLC),
+ % On cherche en inversant les add/op/mult
+ get_args_from_other_add_op_mult(Type,NLC,V,ELArgs),
+ LArgs \== [],
+ set_vardef(V,LArgs)),
+ (foreach(Expr,LArgs),
+ fromto([],IL,OL,NLArgs),
+ param(From) do
+ term_variables(Expr,Vars),
+ ((member(V,Vars),
+ occurs(V,From))
+ ->
+ OL = IL
+ ; OL = [Expr|IL])),
+ NLArgs \== [].
+
+get_args_from_add_mult_giving(Type,LC,V,LArgs,ELArgs,NLC) :-
+ (foreach(Goal,LC),
+ fromto(ELArgs,ILArgs,OLArgs,LArgs),
+ fromto([],ILC,OLC,NLC),
+ param(Type,V) do
+ functor(Goal,F,_),
+ (occurs(F,(add_int,mult_int,op,add_real,minus_real,mult_real,div_real))
+ ->
+ (Type == int ->
+ ((Goal = add_int(X,Y,Z);
+ Goal = op(X,Z))
+ ->
+ (Z == V ->
+ OLC = ILC,
+ (F == add_int ->
+ OLArgs = [[1_1*X,1_1*Y]|ILArgs]
+ ; OLArgs = [[-1_1*X]|ILArgs])
+ ; OLC = [Goal|ILC],
+ OLArgs = ILArgs)
; (Goal = mult_int(X,Y,Z) ->
((Z == V,
(number(X),
@@ -349,112 +413,137 @@ get_args_from_add_mult_giving(Type,[Goal|LC],V,Args,NLC) :-
rational(Y,RY),
Args = [RY*X]))
->
- true
- ; get_args_from_add_mult_giving(Type,LC,V,Args,NLC))
- ; get_args_from_add_mult_giving(Type,LC,V,Args,NLC)))
- ; % Type == real
- ((Goal = add_real(_,X,Y,Z);
- Goal = minus_real(_,X,Y,Z);
- Goal = op(X,Z))
- ->
- (Z == V ->
- (F == add_real ->
- Args = [1_1*X,1_1*Y]
- ; (F == minus_real ->
- Args = [1_1*X,-1_1*Y]
- ; Args = [-1_1*X]))
- ; NLC = [Goal|ENLC],
- get_args_from_add_mult_giving(Type,LC,V,Args,ENLC))
- ; (Goal = mult_real(_,X,Y,Z) ->
- ((Z == V,
- (number(X),
- rational(X,RX),
- Args = [RX*Y],Arg = Y;
- number(Y),
- rational(Y,RY),
- Args = [RY*X],Arg = X))
- ->
- true
- ; get_args_from_add_mult_giving(Type,LC,V,Args,NLC))
- ; % DANGER ICI !!!!
- (fail,Goal = div_real(_,X,Y,Z) ->
+ OLC = ILC,
+ OLArgs = [Args|ILArgs]
+ ; OLC = [Goal|ILC],
+ OLArgs = ILArgs)
+ ; OLC = [Goal|ILC],
+ OLArgs = ILArgs))
+ ; % Type == real
+ ((Goal = add_real(_,X,Y,Z);
+ Goal = minus_real(_,X,Y,Z);
+ Goal = op(X,Z))
+ ->
+ (Z == V ->
+ OLC = ILC,
+ OLArgs = [Args|ILArgs],
+ (F == add_real ->
+ Args = [1_1*X,1_1*Y]
+ ; (F == minus_real ->
+ Args = [1_1*X,-1_1*Y]
+ ; Args = [-1_1*X]))
+ ; OLC = [Goal|ILC],
+ OLArgs = ILArgs)
+ ; (Goal = mult_real(_,X,Y,Z) ->
((Z == V,
- number(Y),
- InvY is 1_1/rational(Y),
- Args = [InvY*X])
+ (number(X),
+ rational(X,RX),
+ Args = [RX*Y],Arg = Y;
+ number(Y),
+ rational(Y,RY),
+ Args = [RY*X],Arg = X))
->
- true
- ; get_args_from_add_mult_giving(Type,LC,V,Args,NLC))
- ; get_args_from_add_mult_giving(Type,LC,V,Args,NLC)))))
- ; get_args_from_add_mult_giving(Type,LC,V,Args,NLC)).
+ OLC = ILC,
+ OLArgs = [Args|ILArgs]
+ ; OLC = [Goal|ILC],
+ OLArgs = ILArgs)
+ ; % DANGER ICI !!!!
+ (Goal = div_real(_,X,Y,Z) ->
+ ((Z == V,
+ number(Y),
+ rational(Y,RY),
+ InvY is 1_1/RY,
+ Args = [InvY*X])
+ ->
+ OLC = ILC,
+ OLArgs = [Args|ILArgs]
+ ; OLC = [Goal|ILC],
+ OLArgs = ILArgs)
+ ; OLC = [Goal|ILC],
+ OLArgs = ILArgs))))
+ ; OLC = ILC,
+ OLArgs = ILArgs)).
% On inverse les add/minus/opp/mult/div_real
-get_args_from_other_add_op_mult(Type,LC,V,Args) :-
- member(Goal,LC),
- functor(Goal,F,_),
- occurs(F,(add_int,mult_int,op,add_real,minus_real,mult_real,div_real)),
- (Goal = op(X,Z) ->
- X == V,
- Args = [-1_1*Z]
- ; (Type == int ->
- (Goal = add_int(X,Y,Z) ->
- (X == V ->
- Args = [1_1*Z,-1_1*Y]
- ; Y == V,
- Args = [1_1*Z,-1_1*X])
- ; Goal = mult_int(X,Y,Z),
- not_unify(Z,0),
- % donc X et Y <> 0
- once (V == X,
- % X = Z * 1/Y
- number(Y),
- InvY = 1_1/rational(Y),
- Args = [InvY*Z];
- V == Y,
- % Y = Z * 1/X
- number(X),
- InvX is 1_1/rational(X),
- Args = [InvX*Z]))
- ; % real
- (Goal = add_real(_,X,Y,Z) ->
- (X == V ->
- Args = [1_1*Z,-1_1*Y]
- ; Y == V,
- Args = [1_1*Z,-1_1*X])
- ; (Goal = minus_real(_,X,Y,Z) ->
+get_args_from_other_add_op_mult(Type,LC,V,LArgs) :-
+ (foreach(Goal,LC),
+ fromto([],ILArgs,OLArgs,LArgs),
+ param(Type,V) do
+ (Goal = op(X,Z) ->
+ X == V,
+ OLArgs = [[-1_1*Z]|ILArgs]
+ ; (Type == int ->
+ (Goal = add_int(X,Y,Z) ->
(X == V ->
- Args = [1_1*Z,1_1*Y]
+ OLArgs = [[1_1*Z,-1_1*Y]|ILArgs]
; Y == V,
- Args = [-1_1*Z,1_1*X])
- ; (Goal = mult_real(_,X,Y,Z) ->
- not_unify(Z,0),
- % donc X et Y <> 0
- % et on peut inverser sur X ou Y
- once (V == X,
- number(Y),
- % X = Z * 1/Y
- InvY = 1_1/rational(Y),
- Args = [InvY*Z];
- V == Y,
- number(X),
- % Y = Z * 1/X
- InvX is 1_1/rational(X),
- Args = [InvX*Z])
- ; Goal = div_real(_,X,Y,Z),
- % Y <> 0 en real
- not_zero(Z),
- % donc X et Y <> 0
- % et on peut inverser sur X ou Y
- number(Z),
- once (V == X,
- % X = Z * Y
- rational(Z,RZ),
- Args = [RZ*Y];
- V == Y,
- % Y = X/Z
- InvZ is 1_1/rational(Z),
- Args = [InvZ*X])))))),
- !.
+ OLArgs = [[1_1*Z,-1_1*X]|ILArgs])
+ ; ((Goal = mult_int(X,Y,Z),
+ not_unify(Z,0),
+ % donc X et Y <> 0
+ (V == X,
+ % X = Z * 1/Y
+ number(Y),
+ rational(Y,RY),
+ InvY = 1_1/RY,
+ OLArgs = [[InvY*Z]|ILArgs];
+ V == Y,
+ % Y = Z * 1/X
+ number(X),
+ rational(X,RX),
+ InvX is 1_1/RX,
+ OLArgs = [[InvX*Z]|ILArgs]))
+ ->
+ true
+ ; OLArgs = ILArgs))
+ ; % real
+ (Goal = add_real(_,X,Y,Z) ->
+ (X == V ->
+ OLArgs = [[1_1*Z,-1_1*Y]|ILArgs]
+ ; Y == V,
+ OLArgs = [[1_1*Z,-1_1*X]|ILArgs])
+ ; (Goal = minus_real(_,X,Y,Z) ->
+ (X == V ->
+ OLArgs = [[1_1*Z,1_1*Y]|ILArgs]
+ ; Y == V,
+ OLArgs = [[-1_1*Z,1_1*X]|ILArgs])
+ ; (Goal = mult_real(_,X,Y,Z) ->
+ ((not_zero(Z),
+ % donc X et Y <> 0
+ % et on peut inverser sur X ou Y
+ (V == X,
+ number(Y),
+ % X = Z * 1/Y
+ rational(Y,RY),
+ InvY = 1_1/RY,
+ Args = [InvY*Z];
+ V == Y,
+ number(X),
+ % Y = Z * 1/X
+ rational(X,RX),
+ InvX is 1_1/RX,
+ Args = [InvX*Z]))
+ ->
+ OLArgs = [Args|ILArgs]
+ ; OLArgs = ILArgs)
+ ; ((Goal = div_real(_,X,Y,Z),
+ % Y <> 0 en real
+ not_zero(Z),
+ % donc X et Y <> 0
+ % et on peut inverser sur X ou Y
+ number(Z),
+ (V == X,
+ % X = Z * Y
+ rational(Z,RZ),
+ Args = [RZ*Y];
+ V == Y,
+ % Y = X/Z
+ rational(Z,RZ),
+ InvZ is 1_1/RZ,
+ Args = [InvZ*X]))
+ ->
+ OLArgs = [Args|ILArgs]
+ ; OLArgs = ILArgs))))))).
diff --git a/Src/COLIBRI/col_solve.pl b/Src/COLIBRI/col_solve.pl
index 98612749465613e585424c5df31b7becb547e61e..90b58bdb29255f98946f945cb823997e4339b239 100644
--- a/Src/COLIBRI/col_solve.pl
+++ b/Src/COLIBRI/col_solve.pl
@@ -838,12 +838,14 @@ smt_test(TO,Size) :-
%----------------------------------------------------------------
%StrDir = "./QF_UFLIA/", %
%----------------------------------------------------------------
- StrDir = "./QF_UFLRA/", %
+ %StrDir = "./QF_UFLRA/", %
%----------------------------------------------------------------
%StrDir = "./QF_FP/20170501-Heizmann-UltimateAutomizer/", %tout OK
- %StrDir = "./QF_FP/ramalho/", % 6-1 TO (cvc4 20)
- %StrDir = "./QF_FP/griggio/", % 58 TO (cvc4 114)
- %StrDir = "./QF_FP/schanda/spark/", % 7 TO (cvc4 9)
+ %StrDir = "./QF_FP/20190429-UltimateAutomizerSvcomp2019/",% 1 TO (bitwuzla 0)
+ %StrDir = "./QF_FP/ramalho/", % 4 TO (bitwuzla 17)
+ %StrDir = "./QF_FP/griggio/", % 54 TO (43 cast) (bitwuzla 74)
+ StrDir = "./QF_FP/schanda/spark/", % 7 (6 avec dist cast 0 pour
+ % double->float, mais faux !) TO (bitwuzla 3)
%StrDir = "./QF_FP/wintersteiger/", % tout OK
%StrDir = "./QF_FP/wintersteiger/abs/",
%StrDir = "./QF_FP/wintersteiger/add/",
@@ -872,7 +874,7 @@ smt_test(TO,Size) :-
%StrDir = "QF_ALIA/qlock2/", % Des TO et core dump
%StrDir = "QF_ALIA/cvc/", % TOUT OK
- %StrDir = "QF_ALIA/UltimateAutomizer2/",% KO tableaux de tableaux
+ %StrDir = "QF_ALIA/UltimateAutomizer2/",% des TO
%StrDir = "QF_ALIA/piVC/", % TOUT OK
%StrDir = "QF_ALIA/ios/", % TOUT OK
@@ -971,6 +973,8 @@ smt_test0(TO,Size,StrDir) :-
; concat_string(["timeout --signal=KILL --kill-after=0.1 ",TO,"s ",ECLIPSE," -b ",COL," -g ",SizeM," -e \"seed(0),use_delta,setval(def_real_for_int,1)@colibri,setval(step_limit,0),setval(no_dolmen_warning,1)@eclipse,smt_solve_get_stat(\'",F,"\')\""],Com)),
%; concat_string(["timeout --signal=KILL --kill-after=0.1 ",TO,"s cvc4 ",F],Com)),
+%; concat_string(["timeout --signal=KILL --kill-after=0.1 ",TO,"s z3 ",F],Com)),
+%; concat_string(["timeout --signal=KILL --kill-after=0.1 ",TO,"s bitwuzla ",F],Com)),
exec(Com,[],Pid),
wait(Pid,CodeExt),
writeln(code:CodeExt),
diff --git a/Src/COLIBRI/ndelta.pl b/Src/COLIBRI/ndelta.pl
index 46a098f4d05c7d4ffb4c1447900089dfa94cee39..883b9772dcd48cd4423dde5945e5dcbd484e7cdd 100755
--- a/Src/COLIBRI/ndelta.pl
+++ b/Src/COLIBRI/ndelta.pl
@@ -221,9 +221,9 @@ add(X, Y, Z), lt(C, Z), add(Y,T,D), add(X, D, C), show_deltas_vars.
:- import
- setarg/3,
- set_priority/1
- from sepia_kernel.
+ setarg/3,
+ set_priority/1
+ from sepia_kernel.
:- import
@@ -246,9 +246,9 @@ add(X, Y, Z), lt(C, Z), add(Y,T,D), add(X, D, C), show_deltas_vars.
:- import
- wake_if_other_scheduled/1,
- check_constrained_var/2
- from notify.
+ wake_if_other_scheduled/1,
+ check_constrained_var/2
+ from notify.
use_delta :-
@@ -373,42 +373,42 @@ pre_unify_delta_var_nonvar(Var{ndelta:delta(Before,After,Loop,CC)},Val) ?-
% unify_delta(+Term, Attribute,Susp of var with Attr)
unify_delta(_, Attr) :-
/*** ANY + VAR ***/
- %% Variable non attribuee
- var(Attr).
+ % Variable non attribuee
+ var(Attr).
unify_delta(Term, Attr) :-
compound(Attr),
- %% Variable attribuee
- unify_term_delta(Term, Attr).
+ % Variable attribuee
+ unify_term_delta(Term, Attr).
:- mode unify_term_delta(?, +).
unify_term_delta(Atom, delta(Before,After,Loop,CC)) :-
nonvar(Atom),
/*** NONVAR + META ***/
- %% Instanciation de la variable
+ % Instanciation de la variable
!,
- atomic(Atom),
- %% On nettoie les Before After
- get_priority(Prio),
- set_priority(1),
- join_before_after(Before,After,Atom,Loop,CC),
- set_priority(Prio).
+ atomic(Atom),
+ % On nettoie les Before After
+ get_priority(Prio),
+ set_priority(1),
+ join_before_after(Before,After,Atom,Loop,CC),
+ set_priority(Prio).
unify_term_delta(Y{AttrY}, AttrX) ?-
unify_delta_delta(Y, AttrX, AttrY).
unify_delta_delta(_, AttrX, AttrY) :-
var(AttrY),
/*** VAR + META ***/
- %% Liaison a une variable non attribuee
+ % Liaison a une variable non attribuee
AttrX = AttrY.
unify_delta_delta(Y, AttrX, AttrY) :-
nonvar(AttrY),
- %% Deux variables attribuees dans delta
- %% On doit nettoyer les deltas
- get_priority(Prio),
- set_priority(1),
- merge_before_after(Y,AttrY,AttrX),
- set_priority(Prio).
+ % Deux variables attribuees dans delta
+ % On doit nettoyer les deltas
+ get_priority(Prio),
+ set_priority(1),
+ merge_before_after(Y,AttrY,AttrX),
+ set_priority(Prio).
%----------------------------------------------------------------
% test_unify
@@ -420,9 +420,9 @@ test_unify_delta(_, Attr) :-
var(Attr). % Ignore if no attribute for this extension
test_unify_delta(Term, Attr) :-
compound(Attr),
- (getval(use_delta,1)@eclipse ->
- test_unify_term_delta(Term, Attr)
- ; true).
+ (getval(use_delta,1)@eclipse ->
+ test_unify_term_delta(Term, Attr)
+ ; true).
% We wake every time a variable is touched.
%%:- mode test_unify_term_delta(?, +).
@@ -435,7 +435,7 @@ test_unify_term_delta(Y{ndelta:AttrY}, AttrX) :-
test_unify_delta_delta(_, _, AttrY) :-
var(AttrY).
test_unify_delta_delta(Y, delta(BeforeX,AfterX,Loop,CC), DeltasY) ?-
- /*** META + META ***/
+ /*** META + META ***/
% Test partiel, si on a un delta entre X et Y
% il doit accepter 0 pour Cost
((match_delta_var(BeforeX,Y,Rel,Cost);
@@ -447,86 +447,86 @@ test_unify_delta_delta(Y, delta(BeforeX,AfterX,Loop,CC), DeltasY) ?-
Cost = L..H,
L =< 0,
H >= 0)
- ; true).
+ ; true).
%----------------------------------------------------------------
% print
%----------------------------------------------------------------
print_delta(_{ndelta:delta(Before,After,Loop,CC)}, Attribute) ?-
- (Before,After) \== ([],[]),
- open_named_stream(string(""),write,str),
- printf(str,"%w",(Before,After,Loop,CC)),
- get_stream_info(str,name,Attribute),
- close(str).
+ (Before,After) \== ([],[]),
+ open_named_stream(string(""),write,str),
+ printf(str,"%w",(Before,After,Loop,CC)),
+ get_stream_info(str,name,Attribute),
+ close(str).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
deltas_number(X{ndelta:delta(B,A,_Loop,_CC)},Nb) ?- !,
- Nb is length(B) + length(A).
+ Nb is length(B) + length(A).
deltas_number(_,0).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
is_delta_var(X{ndelta:delta(B,A,_Loop,_CC)}) ?-
- (B,A) \== ([],[]).
+ (B,A) \== ([],[]).
is_signed_delta_var(X{ndelta:delta(B,A,_Loop,_CC)}) ?-
- (member((_,S,C),B);
- member((_,S,C),A)),
- S \== '#',
- (S == '=';
- min_max_inter(C,L,H),
- (L >= 0;
- H =< 0)),
- !.
+ (member((_,S,C),B);
+ member((_,S,C),A)),
+ S \== '#',
+ (S == '=';
+ min_max_inter(C,L,H),
+ (L >= 0;
+ H =< 0)),
+ !.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% On recupere les deux deltas entre X et Y
%% et C est de la forme B1..B2 pour S = '+'|'#'
%% (B1 peut etre plus grand que B2)
get_deltas(X{ndelta:delta(BX,AfterX,(ILX,_),CC1)},Y{ndelta:delta(BY,AfterY,(ILY,_),CC2)},NS,NC) ?-
- getval(use_delta,1)@eclipse,
- (match_delta_var(AfterX,Y,S,C) ->
- true
- ; match_delta_var(AfterY,X,S,OpC),
- (S == '=' ->
- C is -OpC
- ; OpC = OpH..OpL,
- L is -OpL,
- H is -OpH,
- C = L..H)),
- NS = S,
- NC = C,
- (CC1 \== CC2 ->
- (getval(gdbg,1)@eclipse ->
- writeln(output,'Pb_get_deltasCC'(X,Y,(BX,AfterX),(BY,AfterY)))
- ; true),
- %% On essaye de reparer le graphe
- CC1 = CC2
+ getval(use_delta,1)@eclipse,
+ (match_delta_var(AfterX,Y,S,C) ->
+ true
+ ; match_delta_var(AfterY,X,S,OpC),
+ (S == '=' ->
+ C is -OpC
+ ; OpC = OpH..OpL,
+ L is -OpL,
+ H is -OpH,
+ C = L..H)),
+ NS = S,
+ NC = C,
+ (CC1 \== CC2 ->
+ (getval(gdbg,1)@eclipse ->
+ writeln(output,'Pb_get_deltasCC'(X,Y,(BX,AfterX),(BY,AfterY)))
+ ; true),
+ % On essaye de reparer le graphe
+ CC1 = CC2
/*
- get_priority(Prio),
+ get_priority(Prio),
set_priority(1),
check_delta_join(X,Y,_),
set_priority(Prio)
*/
- ; true).
+ ; true).
match_delta_var([(Var,R,C)|Deltas],Var,Rel,Cost) ?- !,
- Rel = R,
- Cost = C.
+ Rel = R,
+ Cost = C.
match_delta_var([_|Deltas],Var,Rel,Cost) :-
- match_delta_var(Deltas,Var,Rel,Cost).
+ match_delta_var(Deltas,Var,Rel,Cost).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% X contient un delta a partir de X
exists_delta_start(X{ndelta:delta(_,[_|_AfterX],_Loop,_CC)}) ?-
- true.
+ true.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% X contient un delta aboutisant a X
exists_delta_end(X{ndelta:delta([_|_BeforeX],_,_,_CC)}) ?-
- true.
+ true.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% La variable a ete instanciee
@@ -537,144 +537,144 @@ exists_delta_end(X{ndelta:delta([_|_BeforeX],_,_,_CC)}) ?-
join_before_after(Before,After,VarVal,Loop,CC) :-
- (getval(use_delta,1)@eclipse ->
- (join_before_after1(Before,After,VarVal,Loop,CC) ->
- true
- ; getval(gdbg,1)@eclipse,
- writeln(output,fail_join_before_after),
- fail)
- ; (var(VarVal) ->
- replace_attribute(VarVal,_,ndelta)
- ; true)).
+ (getval(use_delta,1)@eclipse ->
+ (join_before_after1(Before,After,VarVal,Loop,CC) ->
+ true
+ ; getval(gdbg,1)@eclipse,
+ writeln(output,fail_join_before_after),
+ fail)
+ ; (var(VarVal) ->
+ replace_attribute(VarVal,_,ndelta)
+ ; true)).
join_before_after2(Before,After,Val,Loop,CC) :-
- %% Si Before et After contiennent en tout
- %% un seul delta, Val est un bout de chaine
- %% et il suffit d'enlever son delta
- %% Sinon Val est entre au moins deux autres
- %% sommets et on doit preserver leur connexite
- %% en remplacant Val par une nouvelle variable
- (Before == [] ->
- (After = [(V,_,_)] ->
- BA = 1
- ; true)
- ; ((After == [],
- Before = [(V,_,_)])
- ->
- BA = 2
- ; true)),
- (var(Val) ->
- replace_attribute(Val,_,ndelta)
- ; true),
- (nonvar(BA) ->
- %% Il suffit d'enlever le delta instancie dans V
- clean_inst_delta_BA(BA,V,Val)
- ; %% On remplace Val par NewVar
- replace_Val_by_NewVar(2,Before,Val,NewVar),
- replace_Val_by_NewVar(1,After,Val,NewVar),
- add_attribute(NewVar,delta(Before,After,Loop,CC),ndelta)).
+ % Si Before et After contiennent en tout
+ % un seul delta, Val est un bout de chaine
+ % et il suffit d'enlever son delta
+ % Sinon Val est entre au moins deux autres
+ % sommets et on doit preserver leur connexite
+ % en remplacant Val par une nouvelle variable
+ (Before == [] ->
+ (After = [(V,_,_)] ->
+ BA = 1
+ ; true)
+ ; ((After == [],
+ Before = [(V,_,_)])
+ ->
+ BA = 2
+ ; true)),
+ (var(Val) ->
+ replace_attribute(Val,_,ndelta)
+ ; true),
+ (nonvar(BA) ->
+ % Il suffit d'enlever le delta instancie dans V
+ clean_inst_delta_BA(BA,V,Val)
+ ; % On remplace Val par NewVar
+ replace_Val_by_NewVar(2,Before,Val,NewVar),
+ replace_Val_by_NewVar(1,After,Val,NewVar),
+ add_attribute(NewVar,delta(Before,After,Loop,CC),ndelta)).
clean_inst_delta_BA(BA,Var{ndelta:Deltas},Val) ?-
- compound(Deltas),!,
- arg(BA,Deltas,LD),
- once (member_begin_end((V,_,_),LD,NLD,E,E),
- V == Val),
- (NLD == [] ->
- Other is 3-BA,
- arg(Other,Deltas,OLD),
- (OLD == [] ->
- replace_attribute(Var,_,ndelta)
- ; setarg(BA,Deltas,NLD))
- ; setarg(BA,Deltas,NLD)).
+ compound(Deltas),!,
+ arg(BA,Deltas,LD),
+ once (member_begin_end((V,_,_),LD,NLD,E,E),
+ V == Val),
+ (NLD == [] ->
+ Other is 3-BA,
+ arg(Other,Deltas,OLD),
+ (OLD == [] ->
+ replace_attribute(Var,_,ndelta)
+ ; setarg(BA,Deltas,NLD))
+ ; setarg(BA,Deltas,NLD)).
clean_inst_delta_BA(_,_,_) :-
- getval(gdbg,1)@eclipse,
- writeln(output,"Pb_clean_inst_delta_BA"),
- fail.
+ getval(gdbg,1)@eclipse,
+ writeln(output,"Pb_clean_inst_delta_BA"),
+ fail.
replace_Val_by_NewVar(_,[],_,_).
replace_Val_by_NewVar(BA,[(Var,_,_)|L],Val,NewVar) :-
- replace_Val_by_NewVar_in_Var(BA,Var,Val,NewVar),
- replace_Val_by_NewVar(BA,L,Val,NewVar).
+ replace_Val_by_NewVar_in_Var(BA,Var,Val,NewVar),
+ replace_Val_by_NewVar(BA,L,Val,NewVar).
replace_Val_by_NewVar_in_Var(BA,Var{ndelta:Deltas},Val,NewVar) ?-
- compound(Deltas),!,
- arg(BA,Deltas,LD),
- once (member_begin_end((V,S,C),LD,NLD,ENLD,End),
- V == Val),
- ENLD = [(NewVar,S,C)|End],
- setarg(BA,Deltas,NLD).
+ compound(Deltas),!,
+ arg(BA,Deltas,LD),
+ once (member_begin_end((V,S,C),LD,NLD,ENLD,End),
+ V == Val),
+ ENLD = [(NewVar,S,C)|End],
+ setarg(BA,Deltas,NLD).
%%replace_Val_by_NewVar_in_Var(_,_,_,_).
join_before_after1(Before,After,VarVal,(Loop,_),CC) :-
- %% VarVal va etre instanciee
- %% Si on instancie au milieu d'une chaine
- %% sans modifier CC de parts et d'autres
- %% (et Loop)
- %% on risque plus tard de provoquer
- %% des check_delta_cycle inutiles !!!
- %% On nettoie les after avec VarVal des variables de Before
- clean_inst_deltas_in_Vars(2,Before,VarVal,[],BVars),
- %% On nettoie les before avec VarVal des variables de After
- clean_inst_deltas_in_Vars(1,After,VarVal,[],AVars),
- (var(VarVal) ->
- %% On vient de pre_unify
- replace_attribute(VarVal,_,ndelta)
- ; true),
- %% BVars contient les variables restantes de Before
- %% AVars contient les variables restantes de After
- append(BVars,AVars,Vars),
- (Vars = [_,_|_] ->
- change_CC(Vars,[])
- ; true).
+ % VarVal va etre instanciee
+ % Si on instancie au milieu d'une chaine
+ % sans modifier CC de parts et d'autres
+ % (et Loop)
+ % on risque plus tard de provoquer
+ % des check_delta_cycle inutiles !!!
+ % On nettoie les after avec VarVal des variables de Before
+ clean_inst_deltas_in_Vars(2,Before,VarVal,[],BVars),
+ % On nettoie les before avec VarVal des variables de After
+ clean_inst_deltas_in_Vars(1,After,VarVal,[],AVars),
+ (var(VarVal) ->
+ % On vient de pre_unify
+ replace_attribute(VarVal,_,ndelta)
+ ; true),
+ % BVars contient les variables restantes de Before
+ % AVars contient les variables restantes de After
+ append(BVars,AVars,Vars),
+ (Vars = [_,_|_] ->
+ change_CC(Vars,[])
+ ; true).
clean_inst_deltas_in_Vars(_,[],_,Vars,Vars).
clean_inst_deltas_in_Vars(BA,[(V,_,_)|L],VarVal,Vars,NVars) :-
- clean_inst_deltas_in_Var(BA,V,VarVal,Vars,Vars1),
- clean_inst_deltas_in_Vars(BA,L,VarVal,Vars1,NVars).
+ clean_inst_deltas_in_Var(BA,V,VarVal,Vars,Vars1),
+ clean_inst_deltas_in_Vars(BA,L,VarVal,Vars1,NVars).
clean_inst_deltas_in_Var(BA,V{ndelta:Deltas},VarVal,Vars,NVars) ?-
- !,
- (var(Deltas) ->
- (getval(gdbg,1)@eclipse ->
- writeln(output,"Pb_clean_inst_deltas_in_Var")
- ; true),
- %% On vient de faire un join_before_after sur V
- %% sans avoir encore instancie V
- NVars = Vars
- ; %% compound(Deltas)
- arg(BA,Deltas,LD),
- remove_inst_deltas(LD,VarVal,NLD),
- ((NLD == [],
- Other is 3-BA,
- arg(Other,Deltas,OLD),
- OLD == [])
- ->
- NVars = Vars,
- %% On supprime V
- replace_attribute(V,_,ndelta)
- ; (V == VarVal ->
- NVars = Vars
- ; NVars = [V|Vars]),
- setarg(BA,Deltas,NLD))).
+ !,
+ (var(Deltas) ->
+ (getval(gdbg,1)@eclipse ->
+ writeln(output,"Pb_clean_inst_deltas_in_Var")
+ ; true),
+ % On vient de faire un join_before_after sur V
+ % sans avoir encore instancie V
+ NVars = Vars
+ ; % compound(Deltas)
+ arg(BA,Deltas,LD),
+ remove_inst_deltas(LD,VarVal,NLD),
+ ((NLD == [],
+ Other is 3-BA,
+ arg(Other,Deltas,OLD),
+ OLD == [])
+ ->
+ NVars = Vars,
+ % On supprime V
+ replace_attribute(V,_,ndelta)
+ ; (V == VarVal ->
+ NVars = Vars
+ ; NVars = [V|Vars]),
+ setarg(BA,Deltas,NLD))).
%% On a un probleme ??
clean_inst_deltas_in_Var(_,_,_,Vars,Vars).
- remove_inst_deltas([(V,S,C)|L],VarVal,NL) :-
- (VarVal == V ->
- NL = L
- ; NL = [(V,S,C)|NL1],
- remove_inst_deltas(L,VarVal,NL1)).
- remove_inst_deltas([],_,[]) :-
- %% On a un probleme
- getval(gdbg,1)@eclipse,
- writeln(output,"Pb_remove_inst_deltas"),
- fail.
+remove_inst_deltas([(V,S,C)|L],VarVal,NL) :-
+ (VarVal == V ->
+ NL = L
+ ; NL = [(V,S,C)|NL1],
+ remove_inst_deltas(L,VarVal,NL1)).
+remove_inst_deltas([],_,[]) :-
+ % On a un probleme
+ getval(gdbg,1)@eclipse,
+ writeln(output,"Pb_remove_inst_deltas"),
+ fail.
%% Changement du CC, parcours en profondeur
@@ -683,51 +683,51 @@ clean_inst_deltas_in_Var(_,_,_,Vars,Vars).
%% Traitement des before/after
change_CC([],_).
change_CC([V|Vars],Seen) :-
- (occurs(V,Seen) ->
- %% Deja vu
- Seen1 = Seen
- ; %% Nouveau et meme CC pour tous les sommets connexes
- change_CC_var(V,CC,[],Seen,Seen1)),
- change_CC(Vars,Seen1).
+ (occurs(V,Seen) ->
+ % Deja vu
+ Seen1 = Seen
+ ; % Nouveau et meme CC pour tous les sommets connexes
+ change_CC_var(V,CC,[],Seen,Seen1)),
+ change_CC(Vars,Seen1).
%% Traitement des variables atteignables
%% par les before/after
change_CC_var(V{ndelta:Delta},CC,Ancestors,Seen,NSeen) ?-
- compound(Delta),
- !,
- %% Plus de loop
- setarg(3,Delta,(_,_)),
- %% Changement de CC
- setarg(4,Delta,CC),
- arg(1,Delta,Before),
- arg(2,Delta,After),
- change_CCV(Before,CC,[V|Ancestors],[V|Seen],Seen1),
- change_CCV(After,CC,[V|Ancestors],Seen1,NSeen).
+ compound(Delta),
+ !,
+ % Plus de loop
+ setarg(3,Delta,(_,_)),
+ % Changement de CC
+ setarg(4,Delta,CC),
+ arg(1,Delta,Before),
+ arg(2,Delta,After),
+ change_CCV(Before,CC,[V|Ancestors],[V|Seen],Seen1),
+ change_CCV(After,CC,[V|Ancestors],Seen1,NSeen).
%% La variable a pu etre instanciee (example V1[1,2]=V2[2,3] -> instanciation a 2)
change_CC_var(V,_,_,Seen,Seen) :-
- (getval(gdbg,1)@eclipse ->
- writeln(output,'Pb_change_CC_var'(V))
- ; true).
+ (getval(gdbg,1)@eclipse ->
+ writeln(output,'Pb_change_CC_var'(V))
+ ; true).
change_CCV([],_,_,Seen,Seen).
change_CCV([(V,_,_)|Vars],CC,Ancestors,Seen,NSeen) :-
- (occurs(V,Seen) ->
- %% Deja vu
- Seen1 = Seen,
- (occurs(V,Ancestors) ->
- set_loop_in_ancestors(Ancestors,V)
- ; true)
- ; change_CC_var(V,CC,Ancestors,Seen,Seen1)),
- change_CCV(Vars,CC,Ancestors,Seen1,NSeen).
+ (occurs(V,Seen) ->
+ % Deja vu
+ Seen1 = Seen,
+ (occurs(V,Ancestors) ->
+ set_loop_in_ancestors(Ancestors,V)
+ ; true)
+ ; change_CC_var(V,CC,Ancestors,Seen,Seen1)),
+ change_CCV(Vars,CC,Ancestors,Seen1,NSeen).
set_loop_in_ancestors(L,V) :-
- member_begin_end(VV,L,Beg,PEnd,End),
- VV == V,!,
- PEnd = [],
- (Beg = [_,_|_] ->
- %% au moins trois variables avec V
- set_loop_id([V|Beg])
- ; true).
+ member_begin_end(VV,L,Beg,PEnd,End),
+ VV == V,!,
+ PEnd = [],
+ (Beg = [_,_|_] ->
+ % au moins trois variables avec V
+ set_loop_id([V|Beg])
+ ; true).
@@ -737,78 +737,78 @@ set_loop_in_ancestors(L,V) :-
:- mode merge_before_after(?,+,+).
merge_before_after(Var,DeltasVar,NDeltas) :-
- (getval(use_delta,1)@eclipse ->
- getval(nbDelta,NbDelta)@eclipse,
- (merge_before_after1(Var,DeltasVar,NDeltas) ->
- true
- ; NewNbDelta is NbDelta + 1,
- setval(nbDelta,NewNbDelta)@eclipse,
- fail)
- ; replace_attribute(Var,_,ndelta)).
+ (getval(use_delta,1)@eclipse ->
+ getval(nbDelta,NbDelta)@eclipse,
+ (merge_before_after1(Var,DeltasVar,NDeltas) ->
+ true
+ ; NewNbDelta is NbDelta + 1,
+ setval(nbDelta,NewNbDelta)@eclipse,
+ fail)
+ ; replace_attribute(Var,_,ndelta)).
merge_before_after1(Var,DeltasVar,NDeltas) :-
DeltasVar = delta(Before,After,Loop1,CC1),
NDeltas = delta(NBefore,NAfter,Loop2,CC2),
- Loop1 = Loop2,
- (CC1 == CC2 ->
- %% Les deux sommets etaient connexes.
- %% On verifie et on enleve les (Var,S,C)
- %% dans les Before et les After de Var (unification des deux bouts d'un delta)
- %% Les S,C qui disparaissent sont ceux entre Var et Var et donc sont
- %% non signes ou nul (sinon fail)
- clear_deltas_var(Before,Var,NewBefore),
- clear_deltas_var(After,Var,NewAfter),
- clear_deltas_var(NBefore,Var,NBefore1),
- clear_deltas_var(NAfter,Var,NAfter1),
- setarg(1,DeltasVar,NewBefore),
- setarg(2,DeltasVar,NewAfter),
- %% On recupere et on supprime dans les sommets adjacents
- %% les deltas nettoyes de NDeltas.
- build_deltas_from_before_after(NBefore1,NAfter1,Var,NewDeltas),
- %% On re-introduit les deltas de NewDeltas
- %% sans faire de check_delta_join mais peut etre
- %% des check_equal_paths qui pourraient provoquer
- %% a leur tour des unifications
- (NewDeltas == [] ->
- ((NewBefore,NewAfter) == ([],[]) ->
- replace_attribute(Var,_,ndelta)
- ; true)
- ; restore_deltas(NewDeltas,Start,End,Check,1,LoopOnly),
- (nonvar(Check) ->
- check_delta_join(Start,End,LoopOnly)
- ; true))
- ; %% Les deux sommets n'etaient pas connexes
- %% donc pas de nouveau cycle,
- %% on peut fusionner les deltas et unifier les CC
- CC1 = CC2,
- append(Before,NBefore,NewBefore),
- append(After,NAfter,NewAfter),
- setarg(1,DeltasVar,NewBefore),
- setarg(2,DeltasVar,NewAfter),
- %% Si chaque sommet avait un delta '='
- %% on peut faire un check_equal_paths
- ((occurs('=',(Before,After)),
- occurs('=',(NBefore,NAfter)))
- ->
- check_equal_paths(Var)
- ; true)).
+ Loop1 = Loop2,
+ (CC1 == CC2 ->
+ % Les deux sommets etaient connexes.
+ % On verifie et on enleve les (Var,S,C)
+ % dans les Before et les After de Var (unification des deux bouts d'un delta)
+ % Les S,C qui disparaissent sont ceux entre Var et Var et donc sont
+ % non signes ou nul (sinon fail)
+ clear_deltas_var(Before,Var,NewBefore),
+ clear_deltas_var(After,Var,NewAfter),
+ clear_deltas_var(NBefore,Var,NBefore1),
+ clear_deltas_var(NAfter,Var,NAfter1),
+ setarg(1,DeltasVar,NewBefore),
+ setarg(2,DeltasVar,NewAfter),
+ % On recupere et on supprime dans les sommets adjacents
+ % les deltas nettoyes de NDeltas.
+ build_deltas_from_before_after(NBefore1,NAfter1,Var,NewDeltas),
+ % On re-introduit les deltas de NewDeltas
+ % sans faire de check_delta_join mais peut etre
+ % des check_equal_paths qui pourraient provoquer
+ % a leur tour des unifications
+ (NewDeltas == [] ->
+ ((NewBefore,NewAfter) == ([],[]) ->
+ replace_attribute(Var,_,ndelta)
+ ; true)
+ ; restore_deltas(NewDeltas,Start,End,Check,1,LoopOnly),
+ (nonvar(Check) ->
+ check_delta_join(Start,End,LoopOnly)
+ ; true))
+ ; % Les deux sommets n'etaient pas connexes
+ % donc pas de nouveau cycle,
+ % on peut fusionner les deltas et unifier les CC
+ CC1 = CC2,
+ append(Before,NBefore,NewBefore),
+ append(After,NAfter,NewAfter),
+ setarg(1,DeltasVar,NewBefore),
+ setarg(2,DeltasVar,NewAfter),
+ % Si chaque sommet avait un delta '='
+ % on peut faire un check_equal_paths
+ ((occurs('=',(Before,After)),
+ occurs('=',(NBefore,NAfter)))
+ ->
+ check_equal_paths(Var)
+ ; true)).
%% On enleve les deltas Var -S,C-> Var
%% On echoue pour # ou =|+ avec C > 0
:- mode clear_deltas_var(+,?,-).
clear_deltas_var([],_,[]).
clear_deltas_var([(X,S,C)|DL1],Var,DL) :-
- (X == Var ->
- %% On peut echouer
- %% Pas de '#' ni de '=' (car C <> 0)
- S == '+',
- %% C doit accepter 0
- C = L..H,
- L =< 0,H >= 0,
- %% On ignore ce delta
- clear_deltas_var(DL1,Var,DL)
- ; DL = [(X,S,C)|EndDL],
- clear_deltas_var(DL1,Var,EndDL)).
+ (X == Var ->
+ % On peut echouer
+ % Pas de '#' ni de '=' (car C <> 0)
+ S == '+',
+ % C doit accepter 0
+ C = L..H,
+ L =< 0,H >= 0,
+ % On ignore ce delta
+ clear_deltas_var(DL1,Var,DL)
+ ; DL = [(X,S,C)|EndDL],
+ clear_deltas_var(DL1,Var,EndDL)).
@@ -817,27 +817,27 @@ clear_deltas_var([(X,S,C)|DL1],Var,DL) :-
%% On ne conserve que les nouveaux deltas ou ceux
%% qui reduisent un delta existant
build_deltas_from_before_after([],After,Var,NewDeltas) :-
- build_deltas_from_after(After,Var,NewDeltas).
+ build_deltas_from_after(After,Var,NewDeltas).
build_deltas_from_before_after([(X,S,C)|Before],After,Var,NewDeltas) :-
- remove_delta_in_after(X,Var,S,C),
- check_with_old_deltas(X,Var,S,C,NewDeltas,EndNewDeltas),
- build_deltas_from_before_after(Before,After,Var,EndNewDeltas).
+ remove_delta_in_after(X,Var,S,C),
+ check_with_old_deltas(X,Var,S,C,NewDeltas,EndNewDeltas),
+ build_deltas_from_before_after(Before,After,Var,EndNewDeltas).
check_with_old_deltas(X,Y,S,C,NewDeltas,End) :-
- (get_deltas(X,Y,OS,OC) ->
- %% On peut echouer ici
- deltas_inter(OS,OC,S,C,NS,NC,Check),
- (var(Check) ->
- %% Delta inutile
- NewDeltas = End
- ; NewDeltas = [(X,Y,NS,NC)|End])
- ; NewDeltas = [(X,Y,S,C)|End]).
+ (get_deltas(X,Y,OS,OC) ->
+ % On peut echouer ici
+ deltas_inter(OS,OC,S,C,NS,NC,Check),
+ (var(Check) ->
+ % Delta inutile
+ NewDeltas = End
+ ; NewDeltas = [(X,Y,NS,NC)|End])
+ ; NewDeltas = [(X,Y,S,C)|End]).
build_deltas_from_after([],_,[]).
build_deltas_from_after([(X,S,C)|After],Var,NewDeltas) :-
- remove_delta_in_before(X,Var,S,C),
- check_with_old_deltas(Var,X,S,C,NewDeltas,EndNewDeltas),
- build_deltas_from_after(After,Var,EndNewDeltas).
+ remove_delta_in_before(X,Var,S,C),
+ check_with_old_deltas(Var,X,S,C,NewDeltas,EndNewDeltas),
+ build_deltas_from_after(After,Var,EndNewDeltas).
%% On enleve (Var,S,C) des after de X
remove_delta_in_after(X{ndelta:DX},Var,S,C) ?-
@@ -863,17 +863,17 @@ remove_delta_in_before(X{ndelta:DX},Var,S,C) ?-
restore_deltas([(X,Y,S,C)|Deltas],Start,End,Check,OLoop,Loop) :-
- launch_delta_bis2(X,Y,S,C,Check,LoopOnly,_Unify),
- ((var(OLoop);
- var(LoopOnly))
- ->
- true
- ; NLoop = 1),
- (Deltas == [] ->
- Start = X,
- End = Y,
- Loop = NLoop
- ; restore_deltas(Deltas,Start,End,Check,NLoop,Loop)).
+ launch_delta_bis2(X,Y,S,C,Check,LoopOnly,_Unify),
+ ((var(OLoop);
+ var(LoopOnly))
+ ->
+ true
+ ; NLoop = 1),
+ (Deltas == [] ->
+ Start = X,
+ End = Y,
+ Loop = NLoop
+ ; restore_deltas(Deltas,Start,End,Check,NLoop,Loop)).
@@ -906,7 +906,11 @@ add_new_delta_bis(X,Y,'+',Min..Max,CC) :-
add_delta_before(Y,X,'+',Min..Max,CC),
check_exists_regular_delta(X,Y,'+',Min..Max)).
add_new_delta_bis(A,B,'=',C,CC) :-
- (C == 0 ->
+ ((C =:= 0,
+ get_type(A,TA),
+ get_type(B,TB),
+ TA == TB) % Essai BM
+ ->
unify_later(A,B)
; add_delta_after(A,B,'=',C,CC),
add_delta_before(B,A,'=',C,CC),
@@ -914,13 +918,18 @@ add_new_delta_bis(A,B,'=',C,CC) :-
check_equal_paths(B)).
add_new_delta_bis(X,Y,'#',L0..H0,CC) :-
- (L0 == 0 ->
- L = 1,
+ ((rational(L0);
+ rational(H0))
+ ->
+ L = L0,
H = H0
- ; L = L0,
- (H0 == 0 ->
- H = -1
- ; H = H0)),
+ ; (L0 =:= 0 ->
+ L = 1,
+ H = H0
+ ; L = L0,
+ (H0 =:= 0 ->
+ H = -1
+ ; H = H0))),
((L > 0;
H < 0)
->
@@ -954,12 +963,17 @@ add_delta_before(Y,X,S,C,CC) :-
:- export unify_later/2.
unify_later(V,V) ?- !.
unify_later(V1,V2) :-
- getval(nbDelta,NbDelta)@eclipse,
- (test_unify_later(V1,V2) ->
- call_priority(unify_later1(V1,V2),2)
- ; NewNbDelta is NbDelta + 1,
- setval(nbDelta,NewNbDelta)@eclipse,
- fail).
+ ((get_type(V1,T1),
+ get_type(V2,T2),
+ T1 == T2) % Essai BM
+ ->
+ getval(nbDelta,NbDelta)@eclipse,
+ (test_unify_later(V1,V2) ->
+ call_priority(unify_later1(V1,V2),2)
+ ; NewNbDelta is NbDelta + 1,
+ setval(nbDelta,NewNbDelta)@eclipse,
+ fail)
+ ; true).
test_unify_later(V1,V2) :-
@@ -1006,115 +1020,115 @@ enable_check_equal_paths:-
check_equal_paths(End) :-
getval(check_equal_paths,1),!,
(check_alived_suspension(delta_join) ->
- %% On a un parcours en cours
- %% On peut avoir une version redondante du parcours en attente
- attached_suspensions(delta_cycle,LS1),
- ((member(S1,LS1),
- get_suspension_data(S1,goal,check_equal_paths_bis(CEnd)),
- CEnd == End)
- ->
- %% On ignore ce parcours
- true
- ; %% On attend la fin du parcours en cours
- %% qui activera le trigger delta_cycle
- suspend(check_equal_paths_bis(End),1,[End->suspend:inst,trigger(delta_join),trigger(delta_cycle)]))
- ; check_equal_paths1(End)).
+ % On a un parcours en cours
+ % On peut avoir une version redondante du parcours en attente
+ attached_suspensions(delta_cycle,LS1),
+ ((member(S1,LS1),
+ get_suspension_data(S1,goal,check_equal_paths_bis(CEnd)),
+ CEnd == End)
+ ->
+ % On ignore ce parcours
+ true
+ ; % On attend la fin du parcours en cours
+ % qui activera le trigger delta_cycle
+ suspend(check_equal_paths_bis(End),1,[End->suspend:inst,trigger(delta_join),trigger(delta_cycle)]))
+ ; check_equal_paths1(End)).
check_equal_paths(_).
%% Variante reveillee
check_equal_paths_bis(End) :-
- var(End),
- !,
- (check_alived_suspension(delta_join) ->
- %% On a un parcours en cours
- %% On peut avoir une version redondante du parcours en attente
- attached_suspensions(delta_cycle,LS1),
- ((member(S1,LS1),
- get_suspension_data(S1,goal,check_equal_paths_bis(CEnd)),
- CEnd == End)
- ->
- %% On ignore ce parcours
- (getval(gdbg,1)@eclipse ->
- writeln(output,ignore_check_equal_paths(End))
- ; true)
- ; %% On attend la fin du parcours en cours
- %% qui activera le trigger delta_cycle
- suspend(check_equal_paths_bis(End),1,[End->suspend:inst,trigger(delta_join),trigger(delta_cycle)]))
- ; getval(nbDelta,NbDelta)@eclipse,
- (check_equal_paths1(End) ->
- true
- ; NewNbDelta is NbDelta + 1,
- setval(nbDelta,NewNbDelta)@eclipse,
- fail)).
+ var(End),
+ !,
+ (check_alived_suspension(delta_join) ->
+ % On a un parcours en cours
+ % On peut avoir une version redondante du parcours en attente
+ attached_suspensions(delta_cycle,LS1),
+ ((member(S1,LS1),
+ get_suspension_data(S1,goal,check_equal_paths_bis(CEnd)),
+ CEnd == End)
+ ->
+ % On ignore ce parcours
+ (getval(gdbg,1)@eclipse ->
+ writeln(output,ignore_check_equal_paths(End))
+ ; true)
+ ; % On attend la fin du parcours en cours
+ % qui activera le trigger delta_cycle
+ suspend(check_equal_paths_bis(End),1,[End->suspend:inst,trigger(delta_join),trigger(delta_cycle)]))
+ ; getval(nbDelta,NbDelta)@eclipse,
+ (check_equal_paths1(End) ->
+ true
+ ; NewNbDelta is NbDelta + 1,
+ setval(nbDelta,NewNbDelta)@eclipse,
+ fail)).
check_equal_paths_bis(_).
%%check_equal_paths1(End) :- !.
check_equal_paths1(End) :-
- get_delta_before_after(End,Before0,After0),
- filter_delta_equal(Before0,[],Before),
- filter_delta_equal(After0,[],After),
- ((Before = [_|_];
- After = [_|_])
- ->
- %% On retarde les eventuels check_equal_paths declenches pandant
- %% ce parcours
- suspend(delta_equal([(End,0)]),1,trigger(delta_join)),
- %% On limite le parcours a un cercle de diametre "Credit" autour de "End"
- Credit = 10,
- keep_and_merge_equal_paths(End,Credit,Before,before,0,[End],Seen,[(End,0)],EqPaths),
- keep_and_merge_equal_paths(End,Credit,After,after,0,Seen,_,EqPaths,_),
- get_priority(P),
- set_priority(2),
- trigger(delta_join),
- trigger(delta_cycle),
- set_priority(P)
- ; true).
-
- filter_delta_equal([],_,[]).
- filter_delta_equal([(V,S,C)|Deltas],Seen,NDeltas) :-
- ((nonvar(V),
- getval(gdbg,1)@eclipse)
- ->
- writeln(output,"Warning filter_delta_equal")
- ; true),
- ((S \== '=';
- nonvar(V); %% on a un sommmet instancie ! on l'ignore en esperant qu'il sera nettoye
- occurs(V,Seen))
- ->
- NDeltas = ENDeltas
- ; NDeltas = [(V,C)|ENDeltas]),
- filter_delta_equal(Deltas,Seen,ENDeltas).
-
-
- keep_and_merge_equal_paths(_,_,[],_,_,Seen,Seen,EqPaths,EqPaths).
- keep_and_merge_equal_paths(End,N,[(V,C)|Deltas],BA,TC,Seen,NSeen,EqPaths,NEqPaths) :-
- sum_BA(BA,TC,C,NTC),
- insert_EqPaths(EqPaths,V,NTC,EqPaths0),
- ((NTC \== 0, %% cas gere par unify_later
- get_deltas(V,End,_,OC),
- OC \== NTC)
- ->
- %% Le delta transitif existe, on le met a jour
- %% sans provoquer un nouveau check_equal_path
- update_deltas_between(V,End,'=',NTC)
- ; true),
- (N > 1 ->
- get_delta_before_after(V,Before0,After0),
- filter_delta_equal(Before0,Seen,Before),
- filter_delta_equal(After0,Seen,After),
- NN is N - 1,
- keep_and_merge_equal_paths(End,NN,Before,before,NTC,[V|Seen],Seen1,EqPaths0,EqPaths1),
- keep_and_merge_equal_paths(End,NN,After,after,NTC,Seen1,Seen2,EqPaths1,EqPaths2)
- ; Seen2 = Seen,
- EqPaths2 = EqPaths),
- keep_and_merge_equal_paths(End,N,Deltas,BA,TC,Seen2,NSeen,EqPaths2,NEqPaths).
-
- sum_BA(before,TC,C,NTC) :-
- NTC is TC + C.
- sum_BA(after,TC,C,NTC) :-
- NTC is TC - C.
+ get_delta_before_after(End,Before0,After0),
+ filter_delta_equal(Before0,[],Before),
+ filter_delta_equal(After0,[],After),
+ ((Before = [_|_];
+ After = [_|_])
+ ->
+ % On retarde les eventuels check_equal_paths declenches pandant
+ % ce parcours
+ suspend(delta_equal([(End,0)]),1,trigger(delta_join)),
+ % On limite le parcours a un cercle de diametre "Credit" autour de "End"
+ Credit = 10,
+ keep_and_merge_equal_paths(End,Credit,Before,before,0,[End],Seen,[(End,0)],EqPaths),
+ keep_and_merge_equal_paths(End,Credit,After,after,0,Seen,_,EqPaths,_),
+ get_priority(P),
+ set_priority(2),
+ trigger(delta_join),
+ trigger(delta_cycle),
+ set_priority(P)
+ ; true).
+
+filter_delta_equal([],_,[]).
+filter_delta_equal([(V,S,C)|Deltas],Seen,NDeltas) :-
+ ((nonvar(V),
+ getval(gdbg,1)@eclipse)
+ ->
+ writeln(output,"Warning filter_delta_equal")
+ ; true),
+ ((S \== '=';
+ nonvar(V); %% on a un sommmet instancie ! on l'ignore en esperant qu'il sera nettoye
+ occurs(V,Seen))
+ ->
+ NDeltas = ENDeltas
+ ; NDeltas = [(V,C)|ENDeltas]),
+ filter_delta_equal(Deltas,Seen,ENDeltas).
+
+
+keep_and_merge_equal_paths(_,_,[],_,_,Seen,Seen,EqPaths,EqPaths).
+keep_and_merge_equal_paths(End,N,[(V,C)|Deltas],BA,TC,Seen,NSeen,EqPaths,NEqPaths) :-
+ sum_BA(BA,TC,C,NTC),
+ insert_EqPaths(EqPaths,V,NTC,EqPaths0),
+ ((NTC \== 0, %% cas gere par unify_later
+ get_deltas(V,End,_,OC),
+ OC \== NTC)
+ ->
+ % Le delta transitif existe, on le met a jour
+ % sans provoquer un nouveau check_equal_path
+ update_deltas_between(V,End,'=',NTC)
+ ; true),
+ (N > 1 ->
+ get_delta_before_after(V,Before0,After0),
+ filter_delta_equal(Before0,Seen,Before),
+ filter_delta_equal(After0,Seen,After),
+ NN is N - 1,
+ keep_and_merge_equal_paths(End,NN,Before,before,NTC,[V|Seen],Seen1,EqPaths0,EqPaths1),
+ keep_and_merge_equal_paths(End,NN,After,after,NTC,Seen1,Seen2,EqPaths1,EqPaths2)
+ ; Seen2 = Seen,
+ EqPaths2 = EqPaths),
+ keep_and_merge_equal_paths(End,N,Deltas,BA,TC,Seen2,NSeen,EqPaths2,NEqPaths).
+
+sum_BA(before,TC,C,NTC) :-
+ NTC is TC + C.
+sum_BA(after,TC,C,NTC) :-
+ NTC is TC - C.
insert_EqPaths([],V,TC,[(V,TC)]).
insert_EqPaths([(V1,TC1)|EqPaths],V,TC,NEqPaths) :-
@@ -1135,28 +1149,28 @@ insert_EqPaths([(V1,TC1)|EqPaths],V,TC,NEqPaths) :-
%% arithmetiques classiques)
%:- mode launch_delta(?,?,++,++).
launch_delta(X,Y,S,C) :-
- ((var(X),var(Y))
- ->
- %% On prend une priorite de 1 si necessaire
- %% pour ne pas etre interrompu
- get_priority(Prio),
- set_priority(1),
- launch_delta_bis(X,Y,S,C),
- set_priority(Prio),
- wake_if_other_scheduled(Prio)
- ; true).
+ ((var(X),var(Y))
+ ->
+ % On prend une priorite de 1 si necessaire
+ % pour ne pas etre interrompu
+ get_priority(Prio),
+ set_priority(1),
+ launch_delta_bis(X,Y,S,C),
+ set_priority(Prio),
+ wake_if_other_scheduled(Prio)
+ ; true).
:- mode launch_delta_bis(?,?,++,++).
launch_delta_bis(X,Y,S,C) :-
- (launch_delta_bis1(X,Y,S,C) ->
- true
- ; fail_delta).
+ (launch_delta_bis1(X,Y,S,C) ->
+ true
+ ; fail_delta).
:- export fail_delta/0.
fail_delta :-
- incval(nbDelta)@eclipse,
- fail.
-
+ incval(nbDelta)@eclipse,
+ fail.
+
:- mode launch_delta_bis1(?,?,++,++).
launch_delta_bis1(X,Y,S,C) :-
% var(X),var(Y)
@@ -1182,7 +1196,7 @@ launch_delta_bis1(X,Y,S,C) :-
:- export launch_delta_bis2/7.
:- mode launch_delta_bis2(?,?,++,++,?,?,?).
% on ignore les distances nulles (pbs sinon)
-launch_delta_bis2(X,Y,S,0,CheckCycle,LoopOnly,Abort) ?- !.
+%launch_delta_bis2(X,Y,S,0,CheckCycle,LoopOnly,Abort) ?- !.
launch_delta_bis2(X,Y,S0,C,CheckCycle,LoopOnly,Abort) :-
getval(use_delta,1)@eclipse,
!,
@@ -1196,7 +1210,11 @@ launch_delta_bis2(X,Y,S0,C,CheckCycle,LoopOnly,Abort) :-
(NS == OS ->
true
; update_deltas(X,Y,NS,NC))
- ; ((NS,NC) == (=,0) ->
+ ; (((NS,NC) == (=,0),
+ get_type(X,TX),
+ get_type(Y,TY),
+ TX == TY)
+ ->
% On doit unifier X et Y
Abort = 1,
unify_later(X,Y)
@@ -1234,134 +1252,156 @@ launch_delta_bis2(_,_,_,_,_,_,_).
:- export check_inside_delta_loop/2.
check_inside_delta_loop(Loop,_) :-
- var(Loop),!.
+ var(Loop),!.
check_inside_delta_loop(_,Var{ndelta:delta(_,_,(IL,_),_CC)}) ?-
- nonvar(IL).
+ nonvar(IL).
get_loop_ids(V{ndelta:delta(_,_,Loop,_)},LoopIds) ?-
- LoopIds = Loop.
+ LoopIds = Loop.
same_CC(X{ndelta:delta(_,_,_,CC)},Y{ndelta:delta(_,_,_,CC)}) ?-
- getval(use_delta,1)@eclipse.
+ getval(use_delta,1)@eclipse.
get_CC(X{ndelta:delta(_,_,_,CC)},XCC) ?- !,
XCC = CC.
get_CC(_,_).
-
+% pour eviter les changements de type sur min/max
+protected_rat_max(A,B,Max) :-
+ (A >= B ->
+ Max = A
+ ; Max = B).
+protected_rat_min(A,B,Min) :-
+ (A =< B ->
+ Min = A
+ ; Min = B).
+
+protected_rat_sum(1.0Inf,_,1.0Inf) :- !.
+protected_rat_sum(-1.0Inf,_,-1.0Inf) :- !.
+protected_rat_sum(_,1.0Inf,1.0Inf) :- !.
+protected_rat_sum(_,-1.0Inf,-1.0Inf) :- !.
+protected_rat_sum(A,B,C) :-
+ C is A + B.
+
+protected_rat_diff(1.0Inf,_,1.0Inf) :- !.
+protected_rat_diff(-1.0Inf,_,-1.0Inf) :- !.
+protected_rat_diff(_,1.0Inf,-1.0Inf) :- !.
+protected_rat_diff(_,-1.0Inf,1.0Inf) :- !.
+protected_rat_diff(A,B,C) :-
+ C is A - B.
:- export deltas_inter/7.
%% Intersection de deltas
%% Check = 1 quand on modifie OS ou OC
deltas_inter(S,C,S,C,NS,NC,_) ?- !,
- NS = S,
- NC = C.
+ NS = S,
+ NC = C.
deltas_inter(#,OC,S,C,NS,NC,Check) :-
- deltas_inter_diff(OC,S,C,NS,NC,Check).
+ deltas_inter_diff(OC,S,C,NS,NC,Check).
deltas_inter(+,OC,S,C,NS,NC,Check) :-
- deltas_inter_plus(OC,S,C,NS,NC,Check).
+ deltas_inter_plus(OC,S,C,NS,NC,Check).
deltas_inter(=,OC,S,C,NS,NC,_Check) :-
- deltas_inter_eg(OC,S,C,NS,NC).
+ deltas_inter_eg(OC,S,C,NS,NC).
deltas_inter_diff(OMin..OMax,=,C,=,C,1) :- !,
- C >= OMin,
- C =< OMax,
- C \== 0.
+ C >= OMin,
+ C =< OMax,
+ C \== 0.
deltas_inter_diff(OMin..OMax,_PlusDiff,Min..Max,NS,NC,Check) :-
- NMin0 is max(OMin,Min),
- (NMin0 == 0 ->
- NMin = 1
- ; NMin = NMin0),
- NMax0 is min(OMax,Max),
- (NMax0 == 0 ->
- NMax = -1
- ; NMax = NMax0),
- %% On peut echouer ici
- NMin =< NMax,
- ((NMin == OMin,
- NMax == OMax)
- ->
- NS = '#',
- NC = NMin..NMax
- ; Check = 1,
- (NMin == NMax ->
- NS = '=',
- NC = NMin
- ; NC = NMin..NMax,
- ((NMin > 0;
- NMax < 0)
- ->
- NS = '+'
- ; %% On n'est pas signe, on garde le '#'
- NS = '#'))).
+ NMin0 is protected_rat_max(OMin,Min),
+ (NMin0 =:= 0 ->
+ NMin = 1
+ ; NMin = NMin0),
+ NMax0 is protected_rat_min(OMax,Max),
+ (NMax0 =:= 0 ->
+ NMax = -1
+ ; NMax = NMax0),
+ % On peut echouer ici
+ NMin =< NMax,
+ ((NMin =:= OMin,
+ NMax =:= OMax)
+ ->
+ NS = '#',
+ NC = OMin..OMax
+ ; Check = 1,
+ (NMin =:= NMax ->
+ NS = '=',
+ NC = NMin
+ ; NC = NMin..NMax,
+ ((NMin > 0;
+ NMax < 0)
+ ->
+ NS = '+'
+ ; % On n'est pas signe, on garde le '#'
+ NS = '#'))).
deltas_inter_plus(Min..Max,=,C,=,C,1) :- !,
- Min =< C,
- C =< Max.
+ Min =< C,
+ C =< Max.
deltas_inter_plus(OMin..OMax,#,Min..Max,NS,NC,Check) :-
- NMin0 is max(OMin,Min),
- (NMin0 == 0 ->
- NMin = 1
- ; NMin = NMin0),
- NMax0 is min(OMax,Max),
- (NMax0 == 0 ->
- NMax = -1
- ; NMax = NMax0),
- %% On peut echouer ici
- NMin =< NMax,
- (NMin == NMax ->
- Check = 1,
- NS = '=',
- NC = NMin
- ; NC = NMin..NMax,
- ((NMin > 0;
- NMax < 0)
- ->
- NS = +,
- ((NMin == OMin,
- NMax == OMax)
- ->
- true
- ; Check = 1)
- ; %% Delta non signe on garde le #
- NS = '#',
- ((NMin == OMin,
- NMax == OMax)
- ->
- true
- ; Check = 1))).
+ NMin0 is protected_rat_max(OMin,Min),
+ (NMin0 =:= 0 ->
+ NMin = 1
+ ; NMin = NMin0),
+ NMax0 is protected_rat_min(OMax,Max),
+ (NMax0 =:= 0 ->
+ NMax = -1
+ ; NMax = NMax0),
+ % On peut echouer ici
+ NMin =< NMax,
+ (NMin =:= NMax ->
+ Check = 1,
+ NS = '=',
+ NC = NMin
+ ; NC = NMin..NMax,
+ ((NMin > 0;
+ NMax < 0)
+ ->
+ NS = +,
+ ((NMin =:= OMin,
+ NMax =:= OMax)
+ ->
+ true
+ ; Check = 1)
+ ; % Delta non signe on garde le #
+ NS = '#',
+ ((NMin =:= OMin,
+ NMax =:= OMax)
+ ->
+ true
+ ; Check = 1))).
deltas_inter_plus(OMin..OMax,+,Min..Max,NS,NC,Check) :-
- NMin is max(Min,OMin),
- NMax is min(Max,OMax),
- %% On peut echouer ici
- NMin =< NMax,
- (NMin == NMax ->
- Check = 1,
- NS = '=',
- NC = NMin
- ; NS = +,
- NC = NMin..NMax,
- ((NMin == OMin,
- NMax == OMax)
- ->
- true
- ; Check = 1)).
+ NMin is protected_rat_max(Min,OMin),
+ NMax is protected_rat_min(Max,OMax),
+ % On peut echouer ici
+ NMin =< NMax,
+ (NMin =:= NMax ->
+ Check = 1,
+ NS = '=',
+ NC = NMin
+ ; NS = +,
+ NC = NMin..NMax,
+ ((NMin =:= OMin,
+ NMax =:= OMax)
+ ->
+ true
+ ; Check = 1)).
deltas_inter_eg(C,#,Min..Max,=,C) :-
- Min =< C,
- C =< Max,
- C \== 0.
+ Min =< C,
+ C =< Max,
+ C \== 0.
deltas_inter_eg(C,+,Min..Max,=,C) :-
- Min =< C,
- C =< Max.
+ Min =< C,
+ C =< Max.
deltas_inter_eg(C,=,OC,=,OC) :-
- C == OC.
+ C == OC.
@@ -1371,9 +1411,13 @@ update_deltas(X,Y,S0,C0) :-
% qu'elles puissent exploiter le nouveau delta
(exists_delta_Rel(X,Y,ORel,OS,OC) ->
true
- ; true),
+ ; true),
update_delta_cost_with_congr(X,Y,S0,C0,S,C),
- (C == 0 ->
+ ((C == 0,
+ get_type(X,TX),
+ get_type(Y,TY),
+ TX == TY)
+ ->
unify_later(X,Y)
; % X et Y ont des deltas
update_deltas_between(X,Y,S,C),
@@ -1394,56 +1438,56 @@ update_deltas(X,Y,S0,C0) :-
- common_suspensions([],_,[]) :- !.
- common_suspensions(_,[],[]) :- !.
- common_suspensions([Susp|LS1],LS2,ComSusps) :-
- (member_begin_end(Susp,LS2,NLS2,End,End) ->
- ComSusps = [Susp|EComSusps],
- common_suspensions(LS1,NLS2,EComSusps)
- ; common_suspensions(LS1,LS2,ComSusps)).
+common_suspensions([],_,[]) :- !.
+common_suspensions(_,[],[]) :- !.
+common_suspensions([Susp|LS1],LS2,ComSusps) :-
+ (member_begin_end(Susp,LS2,NLS2,End,End) ->
+ ComSusps = [Susp|EComSusps],
+ common_suspensions(LS1,NLS2,EComSusps)
+ ; common_suspensions(LS1,LS2,ComSusps)).
:- export update_deltas_between/4.
update_deltas_between(X,Y,NS,NC) :-
- get_delta_before_after(X,BX,AX),
- get_delta_before_after(Y,BY,AY),
- ((member_begin_end((YY,S,C),BX,NBX,E1,E1),
- YY == Y)
- ->
- member_begin_end((XX,S,C),AY,NAY,E2,E2),
- XX == X,!,
- NAX = AX,
- NBY = BY
- ; member_begin_end((YY,S,C),AX,NAX,E1,E1),
- YY == Y,!,
- member_begin_end((XX,S,C),BY,NBY,E2,E2),
- XX == X,!,
- NBX = BX,
- NAY = AY),
- set_before_after(X,NBX,[(Y,NS,NC)|NAX]),
- set_before_after(Y,[(X,NS,NC)|NBY],NAY),
- check_exists_regular_delta(X,Y,NS,NC).
+ get_delta_before_after(X,BX,AX),
+ get_delta_before_after(Y,BY,AY),
+ ((member_begin_end((YY,S,C),BX,NBX,E1,E1),
+ YY == Y)
+ ->
+ member_begin_end((XX,S,C),AY,NAY,E2,E2),
+ XX == X,!,
+ NAX = AX,
+ NBY = BY
+ ; member_begin_end((YY,S,C),AX,NAX,E1,E1),
+ YY == Y,!,
+ member_begin_end((XX,S,C),BY,NBY,E2,E2),
+ XX == X,!,
+ NBX = BX,
+ NAY = AY),
+ set_before_after(X,NBX,[(Y,NS,NC)|NAX]),
+ set_before_after(Y,[(X,NS,NC)|NBY],NAY),
+ check_exists_regular_delta(X,Y,NS,NC).
set_before_after(V{ndelta:Delta},Before,After) ?-
- compound(Delta),
- setarg(1,Delta,Before),
- setarg(2,Delta,After).
+ compound(Delta),
+ setarg(1,Delta,Before),
+ setarg(2,Delta,After).
%% On inhibe check_exists_regular_delta
check_exists_regular_delta(X,Y,S,C) :- !.
check_exists_regular_delta(X,Y,S,C) :-
- get_delta_before_after(X,_,AfterX),
- get_delta_before_after(Y,BeforeY,_),
- ((member((YY,S,C),AfterX),
- YY == Y,
- member((XX,S,C),BeforeY),
- XX == X,
- same_CC(X,Y))
- ->
- true
- ; writeln(output,'Pb check_exists_regular_delta'(X,Y,S,C)),
- exit_block(abort)).
+ get_delta_before_after(X,_,AfterX),
+ get_delta_before_after(Y,BeforeY,_),
+ ((member((YY,S,C),AfterX),
+ YY == Y,
+ member((XX,S,C),BeforeY),
+ XX == X,
+ same_CC(X,Y))
+ ->
+ true
+ ; writeln(output,'Pb check_exists_regular_delta'(X,Y,S,C)),
+ exit_block(abort)).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -1453,12 +1497,12 @@ check_exists_regular_delta(X,Y,S,C) :-
:- export check_delta_cycle/3.
%%check_delta_cycle(X,Y,LoopOnly) :- !.
check_delta_cycle(X,Y,LoopOnly) :-
- %% Pas de check a partir d'un # !!
- ((get_deltas(X,Y,S,Cost),
- connected_to_other_vars(X,Y))
- ->
-
- check_delta_join(X,Y,LoopOnly)
+ % Pas de check a partir d'un # !!
+ ((get_deltas(X,Y,S,Cost),
+ connected_to_other_vars(X,Y))
+ ->
+
+ check_delta_join(X,Y,LoopOnly)
/*
((nonvar(LoopOnly);
@@ -1470,18 +1514,18 @@ check_delta_cycle(X,Y,LoopOnly) :-
; true),
check_delta_join(X,Y,Loop)
*/
- ; %% Pas de cycle passant par Y
- true).
+ ; % Pas de cycle passant par Y
+ true).
connected_to_other_vars(X,Y) :-
- get_delta_before_after(X,BX,AX),
- (DX = BX; DX = AX),
- member((V1,_,_),DX),
- V1 \== Y,!,
- get_delta_before_after(Y,BY,AY),
- (DY = BY; DY = AY),
- member((V2,_,_),DY),
- V2 \== X.
+ get_delta_before_after(X,BX,AX),
+ (DX = BX; DX = AX),
+ member((V1,_,_),DX),
+ V1 \== Y,!,
+ get_delta_before_after(Y,BY,AY),
+ (DY = BY; DY = AY),
+ member((V2,_,_),DY),
+ V2 \== X.
%% On verifie si on peut avoir des chemins
@@ -1576,9 +1620,9 @@ check_delta_join0(X,Y,Loop) :-
:- mode delta_previous(?,?,-,-,-).
delta_previous(End,Loop,Previous,Vars,Last) :-
get_delta_before_after(End,Before,After),
- %% On inverse les deltas de After
- keep_delta_After(After,End,Loop,Previous,EP,Vars,EV),
- keep_delta_Previous(Before,End,Loop,EP,EV,Last).
+ % On inverse les deltas de After
+ keep_delta_After(After,End,Loop,Previous,EP,Vars,EV),
+ keep_delta_Previous(Before,End,Loop,EP,EV,Last).
/*
@@ -1586,60 +1630,60 @@ si e -- L..H --> s est dans After(e) on a implicitement
un arc s -- -H..-L --> e dans Previous(e)
*/
- keep_delta_After([],_,_,EP,EP,Last,Last).
- keep_delta_After([(X,S,C)|After],Y,Loop,Previous,EP,Vars,Last) :-
- (not_seen_inside_delta_loop(Loop,X) ->
- min_max_inter(C,OpCost,MCost),
- %% -C = -H .. -L -> Cost = -H et OpCost = L
- Cost is - MCost,
- Previous = [(X,S,Cost,OpCost)|NPrevious],
- Vars = [(X,Y)|NVars],
- keep_delta_After(After,Y,Loop,NPrevious,EP,NVars,Last)
- ; keep_delta_After(After,Y,Loop,Previous,EP,Vars,Last)).
-
- keep_delta_Previous([],_,_,[],Last,Last).
- keep_delta_Previous([(X,S,C)|Before],Y,Loop,Previous,Vars,Last) :-
- (not_seen_inside_delta_loop(Loop,X) ->
- min_max_inter(C,Cost,MOpCost),
- OpCost is - MOpCost,
- Previous = [(X,S,Cost,OpCost)|NPrevious],
- Vars = [(X,Y)|NVars],
- keep_delta_Previous(Before,Y,Loop,NPrevious,NVars,Last)
- ; keep_delta_Previous(Before,Y,Loop,Previous,Vars,Last)).
+keep_delta_After([],_,_,EP,EP,Last,Last).
+keep_delta_After([(X,S,C)|After],Y,Loop,Previous,EP,Vars,Last) :-
+ (not_seen_inside_delta_loop(Loop,X) ->
+ min_max_inter(C,OpCost,MCost),
+ % -C = -H .. -L -> Cost = -H et OpCost = L
+ Cost is - MCost,
+ Previous = [(X,S,Cost,OpCost)|NPrevious],
+ Vars = [(X,Y)|NVars],
+ keep_delta_After(After,Y,Loop,NPrevious,EP,NVars,Last)
+ ; keep_delta_After(After,Y,Loop,Previous,EP,Vars,Last)).
+
+keep_delta_Previous([],_,_,[],Last,Last).
+keep_delta_Previous([(X,S,C)|Before],Y,Loop,Previous,Vars,Last) :-
+ (not_seen_inside_delta_loop(Loop,X) ->
+ min_max_inter(C,Cost,MOpCost),
+ OpCost is - MOpCost,
+ Previous = [(X,S,Cost,OpCost)|NPrevious],
+ Vars = [(X,Y)|NVars],
+ keep_delta_Previous(Before,Y,Loop,NPrevious,NVars,Last)
+ ; keep_delta_Previous(Before,Y,Loop,Previous,Vars,Last)).
get_delta_before_after(V{ndelta:delta(B,A,_,_CC)},Before,After) ?-
- getval(use_delta,1)@eclipse,!,
- Before = B,
- After = A.
+ getval(use_delta,1)@eclipse,!,
+ Before = B,
+ After = A.
get_delta_before_after(_,[],[]).
seen_delta(X) :-
- get_loop_ids(X,(_,S)),
- nonvar(S).
+ get_loop_ids(X,(_,S)),
+ nonvar(S).
set_seen_delta(X) :-
- get_loop_ids(X,(_,S)),
- S = 1.
+ get_loop_ids(X,(_,S)),
+ S = 1.
not_seen_inside_delta_loop(Loop,X{ndelta:Delta}) ?-
- compound(Delta),!,
- arg(3,Delta,(L,S)),
- var(S),
- (var(Loop) ->
- true
- ; nonvar(L)).
+ compound(Delta),!,
+ arg(3,Delta,(L,S)),
+ var(S),
+ (var(Loop) ->
+ true
+ ; nonvar(L)).
not_seen_inside_delta_loop(Loop,X) :-
call(spy_here)@eclipse,
getval(gdbg,1)@eclipse,
- writeln(output,'Pb not_seen_inside_delta_loop'(Loop,X)),
- fail.
+ writeln(output,'Pb not_seen_inside_delta_loop'(Loop,X)),
+ fail.
clean_seen_delta([]).
clean_seen_delta([X{ndelta:Delta}|Vars]) ?-
- arg(3,Delta,(L,_)),
- setarg(3,Delta,(L,_)),
- clean_seen_delta(Vars).
+ arg(3,Delta,(L,_)),
+ setarg(3,Delta,(L,_)),
+ clean_seen_delta(Vars).
@@ -1667,7 +1711,7 @@ check_previous_deltas(Loop,[(Start,End)|Vars],Last,Done,InJoin,Join,NewLoop) ?-
decval(delta_credit),
check_previous_deltas(Loop,Vars,NewLast,[Start|Done],InJoin,Join,NewLoop)).
check_previous_deltas(_,_,_,Done,_,_,_) :-
- clean_seen_delta(Done).
+ clean_seen_delta(Done).
%% Chaque delta de Previous est confronte aux transivites deja vues dans
@@ -1749,153 +1793,163 @@ spy_delta.
add_new_previous(Loop,Start,End,S,C,OpC,EndTransPath,NewLoop,InJoin,Join) :-
- %% On regarde les transitivites Start -> End -> Join
- %% en recollant un arc transitif End -> Join derriere le nouvel arc Start -> End
- EndTransPath = trans_path{
- sort:Sp,cost:Cp,opcost:OpCp,nbplus:Nbp,
- eqp:EqPaths,maxp:MaxPaths,otherp:OtherPaths},
- %% Arc transitif (Start,Join,NTSp,NTCp,NTOpCp)
- NTCp is C + Cp,
- NTOpCp is OpC + OpCp,
- sum_sign(S,Sp,NTSp),
- (S == '=' ->
- NTNb = Nbp
- ; NTNb is Nbp + 1),
- %% On regarde si on ferme un cycle
- (find_delta_join(Start,TransPath,SuspStart) ->
- NewLoop = 1,
- %% (Start,Join,OTS,OTC,OTOpC) existe deja
- %% DONC ON A UN CYLE PASSANT PAR Start ET Join
- TransPath = trans_path{
- sort:TS,cost:TC,opcost:TOpC,nbplus:TNb,
- eqp:TEqPaths,maxp:TMaxPaths,otherp:TOtherPaths},
- Sum1 is NTCp + TOpC,
- Sum2 is NTOpCp + TC,
- %% Verification invariant dans un sens
- Sum1 =< 0,
- %% Verification invariant dans l'autre sens
- Sum2 =< 0,
-
-%% LES LOOP NE SERVENT A RIEN
-%% ON LES REUTILISE POUR ALLER PLUS VITE DANS LES occurs ?
- %% Chaque variable du cycle a le meme identificateur de boucle
-
-
- notify_vars_from_disjoint_paths_pairs(Loop,
- EqPaths,MaxPaths,OtherPaths,
- TEqPaths,TMaxPaths,TOtherPaths,Join),
-
- %% Si une des sommes est nulle alors on peut transformer tous les
- %% '+' en = dans MaxPaths et TMaxPaths (les couts ne peuvent plus augmenter)
- (Sum1 == 0 ->
- %% Start->End + End->Join = Join->Start
- change_plus_to_equal_in_delta(Start,End),
- change_plus_to_equal_in_paths(MaxPaths,Join),
- change_op_plus_to_equal_in_paths(TMaxPaths,Join)
- ; (Sum2 == 0 ->
- %% Join->End + End->Start = Start->Join
- change_plus_to_equal_in_delta(End,Start),
- change_op_plus_to_equal_in_paths(MaxPaths,Join),
- change_plus_to_equal_in_paths(TMaxPaths,Join)
- ; %% Si un des chemins est un = et que l'autre ne contient qu'un
- %% seul + alors on peut transformer ce + en = en ajustant son cout
- update_equal_paths(NTSp,Join,TNb,Start,NTCp,TMaxPaths,UpdateEqPaths),
- ((NTSp == '+',
- TS == '=',
- NTNb == 1)
- ->
- (S == '=' ->
- %% Nbp = 1 et MaxPaths <> []
- change_plus_and_adjust_to_equal([(Start,MaxPaths)],TC,Join)
- ; %% Le '+' de Start-End devient un '=' de cout TC-Cp
- NewC is TC-Cp,
- replace_delta_plus_by_equal(Start,End,NewC))
- ; %% Si S = '+' on peut mettre a jour Start-End (C et OpC)
- %% en faisant l'intersection avec Start-Join + Join-End
- sum_sign(Sp,TS,Sp1),
- Cp1 is TC + OpCp,
- OpCp1 is TOpC + Cp,
- try_replace_by_equal_or_update_delta(
- Start,End,S,C,OpC,Sp1,Cp1,OpCp1,NS,NC,NOpC),
- %% Si l'arc transitif Start->Join est un delta
- %% on peut le mettre a jour avec Start-End + End-Join
- (get_deltas(Start,Join,_,_) ->
- sum_sign(NS,Sp,NTS),
- NTC is NC + Cp,
- NTOpC is NOpC + OpCp,
- try_replace_by_equal_or_update_delta(
- Start,Join,TS,TC,TOpC,NTS,NTC,NTOpC,
- NNTS,NNTC,NNTOpC)
- ; NNTS = TS,
- NNTC = TC,
- NNTOpC = TOpC),
- %% Si l'arc transitif End->Join est un delta
- %% on peut le mettre a jour avec End-Start + Start-Join
- (get_deltas(End,Join,_,_) ->
- sum_sign(NS,NNTS,NSp),
- NCp is NOpC + NNTC,
- NOpCp is NC + NNTOpC,
- try_replace_by_equal_or_update_delta(
- End,Join,Sp,Cp,OpCp,NSp,NCp,NOpCp,_,RC,ROpC)
- ; true)))),
- %% Start-*-Join ne va plus servir autrement que dans le role de End-*-Join
- %% dans un prochain add_new_previous, seuls les MaxPaths et EqPaths
- %% pourront etre exploites pour reduire des deltas
- %% Les OtherPaths ne sont plus utiles
- setarg(otherp of trans_path,TransPath,[]),
- NewTC is max(TC,NTCp),
- NewTOpC is max(TOpC,NTOpCp),
- (NewTOpC is -NewTC ->
- NewTS = '='
- ; NewTS = '+'),
- NewTNb is min(TNb,NTNb),
- ((TC,TOpC) == (NTCp,NTOpCp) ->
- NewTNb is min(TNb,NTNb),
- %% On fusionne les T*Paths avex les NT*Paths
- extend_paths(Start,EqPaths,NTEqPaths),
- merge_path_trees(NTEqPaths,TEqPaths,NewTEqPaths),
- extend_paths(Start,MaxPaths,NTMaxPaths),
- merge_path_trees(NTMaxPaths,TMaxPaths,NewTMaxPaths),
- setarg(nbplus of trans_path,TransPath,NewTNb),
- setarg(eqp of trans_path,TransPath,NewTEqPaths),
- setarg(maxp of trans_path,TransPath,NewTMaxPaths)
- ; ((TC,TOpC) == (NewTC,NewTOpC) ->
- %% On garde les anciens T*Paths
- true
- ; ((NTCp,NTOpCp) == (NewTC,NewTOpC) ->
- %% On garde les NT*Paths
- (NTSp == '=' ->
- extend_paths(Start,EqPaths,NewTEqPaths),
- NMaxPaths = MaxPaths
- ; NewTEqPaths = [],
- %% On doit fusionner EqPaths et MaxPaths
- merge_path_trees(MaxPaths,EqPaths,NMaxPaths)),
- extend_paths(Start,NMaxPaths,NewTMaxPaths)
- ; %% Aucun ne correspond aux nouveaux couts
- NewTEqPaths = [],
- NewTMaxPaths = []),
- setarg(sort of trans_path,TransPath,NewTS),
- setarg(cost of trans_path,TransPath,NewTC),
- setarg(opcost of trans_path,TransPath,NewTOpC),
- setarg(nbplus of trans_path,TransPath,NewTNb),
- setarg(eqp of trans_path,TransPath,NewTEqPaths),
- setarg(maxp of trans_path,TransPath,NewTMaxPaths)))
- ; %% Cas general on n'est pas dans un cycle
- %% On etend avec Start les chemins transitifs partant de End
- (NTSp == '=' ->
- extend_paths(Start,EqPaths,NewTEqPaths),
- NMaxPaths = MaxPaths
- ; NewTEqPaths = [],
- %% On doit fusionner EqPaths et MaxPaths
- merge_path_trees(MaxPaths,EqPaths,NMaxPaths)),
- extend_paths(Start,NMaxPaths,NewTMaxPaths),
- extend_paths(Start,OtherPaths,NewTOtherPaths),
- NewTransPath = trans_path{
- sort:NTSp,cost:NTCp,opcost:NTOpCp,nbplus:NTNb,
- eqp:NewTEqPaths,maxp:NewTMaxPaths,otherp:NewTOtherPaths},
- %% Si NTSp = '=' ajout de (Start,NTCp) dans equal_paths
- update_equal_paths(NTSp,Join,2,Start,NTCp,_,_),
- suspend(delta_join(NewTransPath),1,[Start->suspend:inst,trigger(delta_join)])).
+ % On regarde les transitivites Start -> End -> Join
+ % en recollant un arc transitif End -> Join derriere le nouvel arc Start -> End
+ EndTransPath = trans_path{
+ sort:Sp,cost:Cp,opcost:OpCp,nbplus:Nbp,
+ eqp:EqPaths,maxp:MaxPaths,otherp:OtherPaths},
+ % Arc transitif (Start,Join,NTSp,NTCp,NTOpCp)
+ protected_rat_sum(C,Cp,NTCp),
+ protected_rat_sum(OpC,OpCp,NTOpCp),
+ %NTCp is C + Cp,
+ %NTOpCp is OpC + OpCp,
+ sum_sign(S,Sp,NTSp),
+ (S == '=' ->
+ NTNb = Nbp
+ ; NTNb is Nbp + 1),
+ % On regarde si on ferme un cycle
+ (find_delta_join(Start,TransPath,SuspStart) ->
+ NewLoop = 1,
+ % (Start,Join,OTS,OTC,OTOpC) existe deja
+ % DONC ON A UN CYLE PASSANT PAR Start ET Join
+ TransPath = trans_path{
+ sort:TS,cost:TC,opcost:TOpC,nbplus:TNb,
+ eqp:TEqPaths,maxp:TMaxPaths,otherp:TOtherPaths},
+ protected_rat_sum(NTCp,TOpC,Sum1),
+ protected_rat_sum(NTOpCp,TC,Sum2),
+ %Sum1 is NTCp + TOpC,
+ %Sum2 is NTOpCp + TC,
+ % Verification invariant dans un sens
+ Sum1 =< 0,
+ % Verification invariant dans l'autre sens
+ Sum2 =< 0,
+
+ % LES LOOP NE SERVENT A RIEN
+ % ON LES REUTILISE POUR ALLER PLUS VITE DANS LES occurs ?
+ % Chaque variable du cycle a le meme identificateur de boucle
+
+
+ notify_vars_from_disjoint_paths_pairs(Loop,
+ EqPaths,MaxPaths,OtherPaths,
+ TEqPaths,TMaxPaths,TOtherPaths,Join),
+
+ % Si une des sommes est nulle alors on peut transformer tous les
+ % '+' en = dans MaxPaths et TMaxPaths (les couts ne peuvent plus augmenter)
+ (Sum1 =:= 0 ->
+ % Start->End + End->Join = Join->Start
+ change_plus_to_equal_in_delta(Start,End),
+ change_plus_to_equal_in_paths(MaxPaths,Join),
+ change_op_plus_to_equal_in_paths(TMaxPaths,Join)
+ ; (Sum2 =:= 0 ->
+ % Join->End + End->Start = Start->Join
+ change_plus_to_equal_in_delta(End,Start),
+ change_op_plus_to_equal_in_paths(MaxPaths,Join),
+ change_plus_to_equal_in_paths(TMaxPaths,Join)
+ ; % Si un des chemins est un = et que l'autre ne contient qu'un
+ % seul + alors on peut transformer ce + en = en ajustant son cout
+ update_equal_paths(NTSp,Join,TNb,Start,NTCp,TMaxPaths,UpdateEqPaths),
+ ((NTSp == '+',
+ TS == '=',
+ NTNb == 1)
+ ->
+ (S == '=' ->
+ % Nbp = 1 et MaxPaths <> []
+ change_plus_and_adjust_to_equal([(Start,MaxPaths)],TC,Join)
+ ; % Le '+' de Start-End devient un '=' de cout TC-Cp
+ NewC is TC-Cp,
+ replace_delta_plus_by_equal(Start,End,NewC))
+ ; % Si S = '+' on peut mettre a jour Start-End (C et OpC)
+ %% en faisant l'intersection avec Start-Join + Join-End
+ sum_sign(Sp,TS,Sp1),
+ protected_rat_sum(TC,OpCp,Cp1),
+ protected_rat_sum(TOpC,Cp,OpCp1),
+ %Cp1 is TC + OpCp,
+ %OpCp1 is TOpC + Cp,
+ try_replace_by_equal_or_update_delta(
+ Start,End,S,C,OpC,Sp1,Cp1,OpCp1,NS,NC,NOpC),
+ % Si l'arc transitif Start->Join est un delta
+ % on peut le mettre a jour avec Start-End + End-Join
+ (get_deltas(Start,Join,_,_) ->
+ sum_sign(NS,Sp,NTS),
+ protected_rat_sum(NC,Cp,NTC),
+ protected_rat_sum(NOpC,OpCp,NTOpC),
+ %NTC is NC + Cp,
+ %NTOpC is NOpC + OpCp,
+ try_replace_by_equal_or_update_delta(
+ Start,Join,TS,TC,TOpC,NTS,NTC,NTOpC,
+ NNTS,NNTC,NNTOpC)
+ ; NNTS = TS,
+ NNTC = TC,
+ NNTOpC = TOpC),
+ % Si l'arc transitif End->Join est un delta
+ % on peut le mettre a jour avec End-Start + Start-Join
+ (get_deltas(End,Join,_,_) ->
+ sum_sign(NS,NNTS,NSp),
+ protected_rat_sum(NOpC,NNTC,NCp),
+ protected_rat_sum(NC,NNTOpC,NOpCp),
+ %NCp is NOpC + NNTC,
+ %NOpCp is NC + NNTOpC,
+ try_replace_by_equal_or_update_delta(
+ End,Join,Sp,Cp,OpCp,NSp,NCp,NOpCp,_,RC,ROpC)
+ ; true)))),
+ % Start-*-Join ne va plus servir autrement que dans le role de End-*-Join
+ % dans un prochain add_new_previous, seuls les MaxPaths et EqPaths
+ % pourront etre exploites pour reduire des deltas
+ % Les OtherPaths ne sont plus utiles
+ setarg(otherp of trans_path,TransPath,[]),
+ NewTC is protected_rat_max(TC,NTCp),
+ NewTOpC is protected_rat_max(TOpC,NTOpCp),
+ (NewTOpC =:= -NewTC ->
+ NewTS = '='
+ ; NewTS = '+'),
+ NewTNb is protected_rat_min(TNb,NTNb),
+ ((TC,TOpC) == (NTCp,NTOpCp) ->
+ NewTNb is protected_rat_min(TNb,NTNb),
+ % On fusionne les T*Paths avex les NT*Paths
+ extend_paths(Start,EqPaths,NTEqPaths),
+ merge_path_trees(NTEqPaths,TEqPaths,NewTEqPaths),
+ extend_paths(Start,MaxPaths,NTMaxPaths),
+ merge_path_trees(NTMaxPaths,TMaxPaths,NewTMaxPaths),
+ setarg(nbplus of trans_path,TransPath,NewTNb),
+ setarg(eqp of trans_path,TransPath,NewTEqPaths),
+ setarg(maxp of trans_path,TransPath,NewTMaxPaths)
+ ; ((TC,TOpC) == (NewTC,NewTOpC) ->
+ % On garde les anciens T*Paths
+ true
+ ; ((NTCp,NTOpCp) == (NewTC,NewTOpC) ->
+ % On garde les NT*Paths
+ (NTSp == '=' ->
+ extend_paths(Start,EqPaths,NewTEqPaths),
+ NMaxPaths = MaxPaths
+ ; NewTEqPaths = [],
+ % On doit fusionner EqPaths et MaxPaths
+ merge_path_trees(MaxPaths,EqPaths,NMaxPaths)),
+ extend_paths(Start,NMaxPaths,NewTMaxPaths)
+ ; % Aucun ne correspond aux nouveaux couts
+ NewTEqPaths = [],
+ NewTMaxPaths = []),
+ setarg(sort of trans_path,TransPath,NewTS),
+ setarg(cost of trans_path,TransPath,NewTC),
+ setarg(opcost of trans_path,TransPath,NewTOpC),
+ setarg(nbplus of trans_path,TransPath,NewTNb),
+ setarg(eqp of trans_path,TransPath,NewTEqPaths),
+ setarg(maxp of trans_path,TransPath,NewTMaxPaths)))
+ ; % Cas general on n'est pas dans un cycle
+ % On etend avec Start les chemins transitifs partant de End
+ (NTSp == '=' ->
+ extend_paths(Start,EqPaths,NewTEqPaths),
+ NMaxPaths = MaxPaths
+ ; NewTEqPaths = [],
+ % On doit fusionner EqPaths et MaxPaths
+ merge_path_trees(MaxPaths,EqPaths,NMaxPaths)),
+ extend_paths(Start,NMaxPaths,NewTMaxPaths),
+ extend_paths(Start,OtherPaths,NewTOtherPaths),
+ NewTransPath = trans_path{
+ sort:NTSp,cost:NTCp,opcost:NTOpCp,nbplus:NTNb,
+ eqp:NewTEqPaths,maxp:NewTMaxPaths,otherp:NewTOtherPaths},
+ % Si NTSp = '=' ajout de (Start,NTCp) dans equal_paths
+ update_equal_paths(NTSp,Join,2,Start,NTCp,_,_),
+ suspend(delta_join(NewTransPath),1,[Start->suspend:inst,trigger(delta_join)])).
extend_paths(Start,[],[]) :- !.
@@ -1905,7 +1959,11 @@ extend_paths(Start,Paths,[(Start,Paths)]).
update_equal_paths('=',Join,NbPlus,Start,Cp,Paths,1) :- !,
get_equal_paths(Join,InfoEqPaths,SuspJoin),
- (member((Var,Cp),InfoEqPaths) ->
+ ((get_type(Start,T1),
+ member((Var,Cp),InfoEqPaths),
+ get_type(Var,T2),
+ T1 == T2) % Essai BM
+ ->
% Var et Start sont a egalle distance de Join
unify_later(Var,Start)
; set_equal_paths(Join,[(Start,Cp)|InfoEqPaths],SuspJoin),
@@ -1930,50 +1988,52 @@ sum_sign('#',_,+).
merge_path_trees([],Trees,Trees) :- !.
merge_path_trees(Trees,[],Trees) :- !.
merge_path_trees([(Root,SubTrees)|Trees],Trees1,Res) :-
- ((member_begin_end((R,S),Trees1,NTrees1,End,End),
- Root == R)
- ->
- Res = [(Root,NSubTrees)|OtherTrees],
- merge_path_trees(SubTrees,S,NSubTrees),
- merge_path_trees(Trees,NTrees1,OtherTrees)
- ; Res = [(Root,SubTrees)|OtherTrees],
- merge_path_trees(Trees,Trees1,OtherTrees)).
+ ((member_begin_end((R,S),Trees1,NTrees1,End,End),
+ Root == R)
+ ->
+ Res = [(Root,NSubTrees)|OtherTrees],
+ merge_path_trees(SubTrees,S,NSubTrees),
+ merge_path_trees(Trees,NTrees1,OtherTrees)
+ ; Res = [(Root,SubTrees)|OtherTrees],
+ merge_path_trees(Trees,Trees1,OtherTrees)).
%%try_replace_by_equal_or_update_delta(Start,End,S,C,OpC,Sp1,Cp1,OpCp1,S,C,OpC) :- !.
try_replace_by_equal_or_update_delta(Start,End,S,C,OpC,Sp1,Cp1,OpCp1,NewS,NewC,NewOpC) :-
- get_deltas(Start,End,OldS,OldCost),
- min_max_inter(OldCost,OldC,MOldOpC),
- OldOpC is -MOldOpC,
- NC is max(max(C,OldC),Cp1),
- NOpC is max(max(OpC,OldOpC),OpCp1),
- ((OldC,OldOpC) == (NC,NOpC)
- ->
- NewS = OldS,
- NewC = OldC,
- NewOpC = OldOpC
- ; (OldS == '#' ->
- (NC == 0 ->
- NewC = 1
- ; NewC = NC),
- (NOpC == 0 ->
- NewOpC = 1 %% ie -(-1)
- ; NewOpC = NOpC)
- ; NewC = NC,
- NewOpC = NOpC),
- MNewOpC is -NewOpC,
- %% On peut echouer
- NewC =< MNewOpC,
- (NewC == MNewOpC ->
- NewS = '=',
- replace_delta_plus_by_equal(Start,End,NewC)
- ; ((OldS == '#',
- NewC < 0,
- MNewOpC > 0)
- ->
- NewS = '#'
- ; NewS = '+'),
- update_deltas(Start,End,NewS,NewC..MNewOpC))).
+ get_deltas(Start,End,OldS,OldCost),
+ min_max_inter(OldCost,OldC,MOldOpC),
+ OldOpC is -MOldOpC,
+ protected_rat_max(C,OldC,Cp0),
+ protected_rat_max(Cp0,Cp1,NC),
+ protected_rat_max(OpC,OldOpC,OpCp0),
+ protected_rat_max(OpCp0,OpCp1,NOpC),
+ ((OldC,OldOpC) == (NC,NOpC)
+ ->
+ NewS = OldS,
+ NewC = OldC,
+ NewOpC = OldOpC
+ ; (OldS == '#' ->
+ (NC =:= 0 ->
+ NewC = 1
+ ; NewC = NC),
+ (NOpC =:= 0 ->
+ NewOpC = 1 %% ie -(-1)
+ ; NewOpC = NOpC)
+ ; NewC = NC,
+ NewOpC = NOpC),
+ MNewOpC is -NewOpC,
+ % On peut echouer
+ NewC =< MNewOpC,
+ (NewC == MNewOpC ->
+ NewS = '=',
+ replace_delta_plus_by_equal(Start,End,NewC)
+ ; ((OldS == '#',
+ NewC < 0,
+ MNewOpC > 0)
+ ->
+ NewS = '#'
+ ; NewS = '+'),
+ update_deltas(Start,End,NewS,NewC..MNewOpC))).
%% On a au moins deux chemins transitifs entre Start et Join
%% On conserve les "vrais cycles" passant par Start
@@ -1986,19 +2046,19 @@ notify_vars_from_disjoint_paths_pairs(EPaths1,MPaths1,OPaths1,EPaths2,MPaths2,OP
%% Si on est confine dans des boucles, tout le monde est deja notifie.
notify_vars_from_disjoint_paths_pairs(Loop,EPaths1,MPaths1,OPaths1,EPaths2,MPaths2,OPaths2,Join) :-
- nonvar(Loop),!.
+ nonvar(Loop),!.
notify_vars_from_disjoint_paths_pairs(_,EPaths1,MPaths1,OPaths1,EPaths2,MPaths2,OPaths2,Join) :-
- term_variables((EPaths1,MPaths1,OPaths1,EPaths2,MPaths2,OPaths2,Join),Vars),
- set_loop_id(Vars).
+ term_variables((EPaths1,MPaths1,OPaths1,EPaths2,MPaths2,OPaths2,Join),Vars),
+ set_loop_id(Vars).
set_loop_id([]).
set_loop_id([V{ndelta:Deltas}|LV]) ?-
- (compound(Deltas) ->
- arg(3,Deltas,(1,_))
- ; getval(gdbg,1)@eclipse,
- writeln(output,"Pb_set_loop_id"),
- fail),
- set_loop_id(LV).
+ (compound(Deltas) ->
+ arg(3,Deltas,(1,_))
+ ; getval(gdbg,1)@eclipse,
+ writeln(output,"Pb_set_loop_id"),
+ fail),
+ set_loop_id(LV).
/*
notify_vars_from_disjoint_paths_pairs(_,EPaths1,MPaths1,OPaths1,EPaths2,MPaths2,OPaths2,Join) :-
@@ -2082,17 +2142,21 @@ change_op_plus_to_equal_in_sub_trees(X,[(Y,SY)|Subtrees],Join) :-
change_plus_to_equal_in_delta(X,Y) :-
- ((get_deltas(X,Y,PlusDiff,Cost),
- Cost = C.._)
- ->
- (PlusDiff == '#' ->
- C \== 0
- ; true),
- replace_delta_plus_by_equal(X,Y,C)
- ; true).
+ ((get_deltas(X,Y,PlusDiff,Cost),
+ Cost = C.._)
+ ->
+ (PlusDiff == '#' ->
+ C =\= 0
+ ; true),
+ replace_delta_plus_by_equal(X,Y,C)
+ ; true).
replace_delta_plus_by_equal(A,B,C) :-
- (C == 0 ->
+ ((C == 0,
+ get_type(A,TA),
+ get_type(B,TB),
+ TA == TB) % Essai BM
+ ->
unify_later(A,B)
; ((two_value_domain(A,[0,1]),
two_value_domain(B,[0,1]))
@@ -2110,41 +2174,43 @@ replace_delta_plus_by_equal(A,B,C) :-
change_plus_and_adjust_to_equal([],_,_).
change_plus_and_adjust_to_equal([(X,Subtrees)],Cost,Join) :-
- (Subtrees == [] ->
- try_replace_delta_plus_by_equal(X,Join,Cost)
- ; change_plus_and_adjust_to_equal_in_subtrees(X,Subtrees,Cost,Join)).
+ (Subtrees == [] ->
+ try_replace_delta_plus_by_equal(X,Join,Cost)
+ ; change_plus_and_adjust_to_equal_in_subtrees(X,Subtrees,Cost,Join)).
change_plus_and_adjust_to_equal_in_subtrees(_,[],_,_).
change_plus_and_adjust_to_equal_in_subtrees(X,[(Y,Subtrees)|Trees],Cost,Join) :-
- (get_deltas(X,Y,S,C) -> true;exit_block(abort_change_plus_and_adjust_to_equal_in_subtrees)),
- (S == '=' ->
- NewCost is Cost - C,
- change_plus_and_adjust_to_equal([(Y,Subtrees)],NewCost,Join)
- ; get_all_paths_starting_with_End(Y,trans_path{sort:Sp,cost:Cp,nbplus:Nbp}),
- (Nbp == 0 ->
- %% On n'a plus de '+' dans (Y,Subtrees)
- NC is Cost - Cp,
- try_replace_delta_plus_by_equal(X,Y,NC)
- ; %% Au moins un '+' dans (Y,Subtrees), rien a faire
- true)),
- change_plus_and_adjust_to_equal_in_subtrees(X,Trees,Cost,Join).
+ (get_deltas(X,Y,S,C) -> true;exit_block(abort_change_plus_and_adjust_to_equal_in_subtrees)),
+ (S == '=' ->
+ protected_rat_diff(Cost,C,NewCost),
+ %NewCost is Cost - C,
+ change_plus_and_adjust_to_equal([(Y,Subtrees)],NewCost,Join)
+ ; get_all_paths_starting_with_End(Y,trans_path{sort:Sp,cost:Cp,nbplus:Nbp}),
+ (Nbp == 0 ->
+ % On n'a plus de '+' dans (Y,Subtrees)
+ protected_rat_diff(Cost,Cp,NC),
+ %NC is Cost - Cp,
+ try_replace_delta_plus_by_equal(X,Y,NC)
+ ; % Au moins un '+' dans (Y,Subtrees), rien a faire
+ true)),
+ change_plus_and_adjust_to_equal_in_subtrees(X,Trees,Cost,Join).
try_replace_delta_plus_by_equal(A,B,C) :-
- (get_deltas(A,B,OS,OC) ->
- true
- ; update_deltas(A,B,'=',C)),
+ (get_deltas(A,B,OS,OC) ->
+ true
+ ; update_deltas(A,B,'=',C)),
%% Patch BM
%% exit_block(abort_try_replace_delta_plus_by_equal)),
- (OS == '=' ->
- C == OC
- ; (OS == '#' ->
- C \== 0
- ; true),
- OC = L..H,
- L =< C,
- H >= C,
- replace_delta_plus_by_equal(A,B,C)).
+ (OS == '=' ->
+ C == OC
+ ; (OS == '#' ->
+ C \== 0
+ ; true),
+ OC = L..H,
+ L =< C,
+ H >= C,
+ replace_delta_plus_by_equal(A,B,C)).
@@ -2153,12 +2219,12 @@ try_replace_delta_plus_by_equal(A,B,C) :-
%% en relation par "Rel"
:- mode exists_delta_Rel(?,?,-,-,-).
exists_delta_Rel(X{ndelta:delta(BeforeX,AfterX,_,CCX)},Y{ndelta:DeltasY},Rel,S,C) ?-
- get_deltas(X,Y,S,C),
- get_rel_from_SC(S,C,Rel).
+ get_deltas(X,Y,S,C),
+ get_rel_from_SC(S,C,Rel).
get_rel_from_SC('#',_,'#') :- !.
get_rel_from_SC('=',C,Rel) :- !,
- (C == 0 ->
+ (C =:= 0 ->
% possible pour les fp_eq
Rel = '='
; (C > 0 ->
@@ -2183,139 +2249,145 @@ get_rel_from_SC('+',L..H,Rel) :-
%% On retourne la relation et les couts.
%delta_path(K,A,B,Rel,Cost,OpCost,_Seen) :- !,fail.
delta_path(K,A,B,Rel,Cost,OpCost,_Seen) :-
- getval(use_delta,1)@eclipse,
- find_deltas_leading_to(K,0,0,B,Deltas,EndDeltas,[B],A,_Found,NFound,StopEqual),
- (nonvar(StopEq) ->
- NFound = (Cost,OpCost),
- Rel = '='
- ; Deltas = [_|_],
- delta_path_from_edges(A,Deltas,EndDeltas,NFound,NewFound),
- nonvar(NewFound),
- NewFound = (Cost,OpCost),
- (Cost is -OpCost ->
- Rel = '='
- ; Rel = '+')).
+ getval(use_delta,1)@eclipse,
+ find_deltas_leading_to(K,0,0,B,Deltas,EndDeltas,[B],A,_Found,NFound,StopEqual),
+ (nonvar(StopEq) ->
+ NFound = (Cost,OpCost),
+ Rel = '='
+ ; Deltas = [_|_],
+ delta_path_from_edges(A,Deltas,EndDeltas,NFound,NewFound),
+ nonvar(NewFound),
+ NewFound = (Cost,OpCost),
+ (Cost =:= -OpCost ->
+ Rel = '='
+ ; Rel = '+')).
find_deltas_leading_to(K0,TC,TOpC,End,Deltas,EndDeltas,Seen,Start,Found,NewFound,StopEqual) :-
- (K0 == 0 ->
- Deltas = EndDeltas,
- NewFound = Found
- ; (K0 == 1 ->
- %% Inutile de chercher autre chose que Start
- %% car on a epuise les credits pour regarder
- %% les autres deltas
- Deltas = EndDeltas,
- (get_deltas(Start,End,S,C) ->
- (S == '=' ->
- L = C,
- H = C
- ; %% S == '+'|'#'
- C = L..H),
- Cost is TC + L,
- OpCost is TOpC - H,
- (var(Found) ->
- (Cost is -OpCost ->
- StopEqual = 1
- ; true),
- NewFound = (Cost,OpCost)
- ; Found = (OldCost,OldOpCost),
- NewCost is max(Cost,OldCost),
- NewOpCost is max(OpCost,OldOpCost),
- NewFound = (NewCost,NewOpCost),
- (NewCost is -NewOpCost ->
- StopEqual = 1
- ; true))
- ; NewFound = Found)
- ; K is K0 - 1,
- get_delta_before_after(End,Before,After),
- keep_unseen_sources(after,K,TC,TOpC,After,Seen,Deltas,BegEndDeltas,Start,Found,Found1,StopEqual),
- (var(StopEqual) ->
- keep_unseen_sources(before,K,TC,TOpC,Before,Seen,BegEndDeltas,EndDeltas,Start,Found1,NewFound,StopEqual)
- ; true))).
+ (K0 == 0 ->
+ Deltas = EndDeltas,
+ NewFound = Found
+ ; (K0 == 1 ->
+ % Inutile de chercher autre chose que Start
+ % car on a epuise les credits pour regarder
+ % les autres deltas
+ Deltas = EndDeltas,
+ (get_deltas(Start,End,S,C) ->
+ (S == '=' ->
+ L = C,
+ H = C
+ ; % S == '+'|'#'
+ C = L..H),
+ protected_rat_sum(TC,L,Cost),
+ protected_rat_diff(TOpC,H,OpCost),
+ %Cost is TC + L,
+ %OpCost is TOpC - H,
+ (var(Found) ->
+ (Cost =:= -OpCost ->
+ StopEqual = 1
+ ; true),
+ NewFound = (Cost,OpCost)
+ ; Found = (OldCost,OldOpCost),
+ NewCost is protected_rat_max(Cost,OldCost),
+ NewOpCost is protected_rat_max(OpCost,OldOpCost),
+ NewFound = (NewCost,NewOpCost),
+ (NewCost =:= -NewOpCost ->
+ StopEqual = 1
+ ; true))
+ ; NewFound = Found)
+ ; K is K0 - 1,
+ get_delta_before_after(End,Before,After),
+ keep_unseen_sources(after,K,TC,TOpC,After,Seen,Deltas,BegEndDeltas,Start,Found,Found1,StopEqual),
+ (var(StopEqual) ->
+ keep_unseen_sources(before,K,TC,TOpC,Before,Seen,BegEndDeltas,EndDeltas,Start,Found1,NewFound,StopEqual)
+ ; true))).
- keep_unseen_sources(_,_,_,_,[],_,EndDeltas,EndDeltas,_,Found,Found,_).
- keep_unseen_sources(BA,K,TC,TOpC,[(X,S,C)|BeforeAfter],Seen,Deltas,EndDeltas,Start,Found,NewFound,StopEqual) :-
- ((nonvar(X),
- getval(gdbg,1)@eclipse)
- ->
- writeln(output,"Warning keep_unseen_sources")
- ; true),
- ((nonvar(X);
- occurs(X,Seen))
- ->
- NDeltas = Deltas,
- NFound = Found
- ; (S == '=' ->
- L = C,
- H = C
- ; C = L..H),
- compute_trans_cost(BA,TC,TOpC,L,H,NTC,NTOpC),
- (X == Start ->
- (var(Found) ->
- NFound = (NTC,NTOpC),
- (NTC is -NTOpC ->
- StopEqual = 1
- ; true)
- ; Found = (OldTC,OldTOpC),
- NewTC is max(NTC,OldTC),
- NewTOpC is max(NTOpC,OldTOpC),
- NFound = (NewTC,NewTOpC),
- (NewTC is -NewTOpC ->
- StopEqual = 1
- ; true)),
- NDeltas = Deltas
- ; NFound = Found,
- Deltas = [(K,X,NTC,NTOpC,Seen)|NDeltas])),
- (var(StopEqual) ->
- keep_unseen_sources(BA,K,TC,TOpC,BeforeAfter,Seen,NDeltas,EndDeltas,Start,NFound,NewFound,StopEqual)
- ; NewFound = Found).
-
- compute_trans_cost(after,TC,TOpC,L,H,NTC,NTOpC) :- !,
- NTC is TC - H,
- NTOpC is TOpC + L.
- compute_trans_cost(before,TC,TOpC,L,H,NTC,NTOpC) :-
- NTC is TC + L,
- NTOpC is TOpC - H.
-
-
- delta_path_from_edges(Source,[(K,X,TC,TOpC,Seen)|Edges],EndEdges,Found,NewFound) ?- !,
- find_deltas_leading_to(K,TC,TOpC,X,EndEdges,NEndEdges,[X|Seen],Source,Found,Found1,StopEqual),
- (nonvar(StopEqual) ->
- NewFound = Found1
- ; delta_path_from_edges(Source,Edges,NEndEdges,Found1,NewFound)).
+keep_unseen_sources(_,_,_,_,[],_,EndDeltas,EndDeltas,_,Found,Found,_).
+keep_unseen_sources(BA,K,TC,TOpC,[(X,S,C)|BeforeAfter],Seen,Deltas,EndDeltas,Start,Found,NewFound,StopEqual) :-
+ ((nonvar(X),
+ getval(gdbg,1)@eclipse)
+ ->
+ writeln(output,"Warning keep_unseen_sources")
+ ; true),
+ ((nonvar(X);
+ occurs(X,Seen))
+ ->
+ NDeltas = Deltas,
+ NFound = Found
+ ; (S == '=' ->
+ L = C,
+ H = C
+ ; C = L..H),
+ compute_trans_cost(BA,TC,TOpC,L,H,NTC,NTOpC),
+ (X == Start ->
+ (var(Found) ->
+ NFound = (NTC,NTOpC),
+ (NTC =:= -NTOpC ->
+ StopEqual = 1
+ ; true)
+ ; Found = (OldTC,OldTOpC),
+ NewTC is protected_rat_max(NTC,OldTC),
+ NewTOpC is protected_rat_max(NTOpC,OldTOpC),
+ NFound = (NewTC,NewTOpC),
+ (NewTC =:= -NewTOpC ->
+ StopEqual = 1
+ ; true)),
+ NDeltas = Deltas
+ ; NFound = Found,
+ Deltas = [(K,X,NTC,NTOpC,Seen)|NDeltas])),
+ (var(StopEqual) ->
+ keep_unseen_sources(BA,K,TC,TOpC,BeforeAfter,Seen,NDeltas,EndDeltas,Start,NFound,NewFound,StopEqual)
+ ; NewFound = Found).
+
+compute_trans_cost(after,TC,TOpC,L,H,NTC,NTOpC) :- !,
+ protected_rat_diff(TC,H,NTC),
+ protected_rat_sum(TOpC,L,NTOpC).
+ %NTC is TC - H,
+ %NTOpC is TOpC + L.
+compute_trans_cost(before,TC,TOpC,L,H,NTC,NTOpC) :-
+ protected_rat_sum(TC,L,NTC),
+ protected_rat_diff(TOpC,H,NTOpC).
+ %NTC is TC + L,
+ %NTOpC is TOpC - H.
+
+
+delta_path_from_edges(Source,[(K,X,TC,TOpC,Seen)|Edges],EndEdges,Found,NewFound) ?- !,
+ find_deltas_leading_to(K,TC,TOpC,X,EndEdges,NEndEdges,[X|Seen],Source,Found,Found1,StopEqual),
+ (nonvar(StopEqual) ->
+ NewFound = Found1
+ ; delta_path_from_edges(Source,Edges,NEndEdges,Found1,NewFound)).
delta_path_from_edges(Source,_,_,Found,Found).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Pour voir les deltas d'une liste de variables
show_deltas_vars :-
- delayed_goals(DG),
- term_variables(DG,LV),
- show_deltas_vars(LV,_).
+ delayed_goals(DG),
+ term_variables(DG,LV),
+ show_deltas_vars(LV,_).
show_deltas_vars([],_) :- !.
show_deltas_vars(LV,LoopOnly) :-
- get_deltas_vars(LV,LoopOnly,Deltas),
- (Deltas = [(X,_,_,_)|_] ->
+ get_deltas_vars(LV,LoopOnly,Deltas),
+ (Deltas = [(X,_,_,_)|_] ->
PSFile = "/tmp/delta.ps",
DotFile = "/tmp/delta.dot",
concat_string(["dot -Tps ",DotFile," -o ",PSFile],Command1),
concat_string(["evince ",PSFile],Command2),
- write(output,"Deltas : ["),
+ write(output,"Deltas : ["),
print_deltas_vars(Deltas),
- open_named_stream(DotFile, write, dotStream),
- writeln(dotStream,"digraph delta \n{ size=\"7.5,10\""),
- term_variables(Deltas,DeltasVars),
+ open_named_stream(DotFile, write, dotStream),
+ writeln(dotStream,"digraph delta \n{ size=\"7.5,10\""),
+ term_variables(Deltas,DeltasVars),
get_cast_links(DeltasVars,Deltas,Casts),
pp_delta_dot(Casts,dotStream),
- close(dotStream),
- block(
- (exec(Command1,[null,null,null]),
- exec_group(Command2,[null,null,null],_)),
- _,
- true)
- ; true).
+ close(dotStream),
+ block(
+ (exec(Command1,[null,null,null]),
+ exec_group(Command2,[null,null,null],_)),
+ _,
+ true)
+ ; true).
get_cast_links(L,Deltas,Casts) :-
get_cast_links0(L,Deltas,Casts0),
@@ -2324,7 +2396,8 @@ get_cast_links(L,Deltas,Casts) :-
get_cast_links0([],Casts,Casts).
get_cast_links0([V|L],Deltas,Casts) :-
get_type(V,Type),
- (occurs(Type,(real,float_simple,float_double)) ->
+ functor(Type,FType,_),
+ (occurs(FType,(real,float_simple,float_double)) ->
suspensions(V,LSusp),
(foreach(Susp,LSusp),
fromto(End,I,O,Casts),
@@ -2362,91 +2435,113 @@ short_type_name(float_simple,float).
short_type_name(float_double,double).
pp_delta_dot([],Stream):-
- writeln(Stream,"}").
-pp_delta_dot([(X,Y,S,C)|Deltas],Stream) :-
- write(Stream,"\""),
- printf(Stream,"%w",X),
- ((get_loop_ids(X,(LoopX,_)),
- nonvar(LoopX))
- ->
- write(Stream,"_o")
-%% write_loop_ids(Stream,LoopIdsX)
- ; true),
- write(Stream,"\""),
- write(Stream," -> "),
- write(Stream,"\""),
- printf(Stream,"%w",Y),
- ((get_loop_ids(Y,(LoopY,_)),
- nonvar(LoopY))
- ->
- write(Stream,"_o")
-%% write_loop_ids(Stream,LoopIdsY)
- ; true),
- write(Stream,"\""),
- (not occurs(S,(+,#)) ->
- concat_string([" [label= \"",S,C,"\"];"],Label)
- ; C = L..H,
- (S == '#' ->
- concat_string([" [label= \"",S,L,"..",H,"\"];"],Label)
- ; concat_string([" [label= \"",L,"..",H,"\"];"],Label))),
- writeln(Stream,Label),
- pp_delta_dot(Deltas,Stream).
+ writeln(Stream,"}").
+pp_delta_dot([(X0,Y0,S,C0)|Deltas],Stream) :-
+ (C0 = L0..H0 ->
+ int_from_integral_rat(L0,L1),
+ int_from_integral_rat(H0,H1),
+ C1 = L1..H1
+ ; int_from_integral_rat(C0,C1)),
+ ((S == +,
+ C1 = L1..H1,
+ H1 =< 0)
+ ->
+ OpH0 is - H1,
+ OpL0 is - L1,
+ (X,Y,C) = (Y0,X0,OpH0..OpL0)
+ ; (X,Y,C) = (X0,Y0,C1)),
+ write(Stream,"\""),
+ printf(Stream,"%w",X),
+ ((get_loop_ids(X,(LoopX,_)),
+ nonvar(LoopX))
+ ->
+ write(Stream,"_o")
+ ; true),
+ write(Stream,"\""),
+ write(Stream," -> "),
+ write(Stream,"\""),
+ printf(Stream,"%w",Y),
+ ((get_loop_ids(Y,(LoopY,_)),
+ nonvar(LoopY))
+ ->
+ write(Stream,"_o")
+ ; true),
+ write(Stream,"\""),
+ (not occurs(S,(+,#)) ->
+ concat_string([" [label= \"",S,C,"\"];"],Label)
+ ; C = L..H,
+ (S == '#' ->
+ concat_string([" [label= \"",S,L,"..",H,"\"];"],Label)
+ ; concat_string([" [label= \"",L,"..",H,"\"];"],Label))),
+ writeln(Stream,Label),
+ pp_delta_dot(Deltas,Stream).
+
+int_from_integral_rat(A,B) :-
+ ((rational(A),
+ denominator(A,1))
+ ->
+ numerator(A,B)
+ ; B = A).
write_loop_ids(Stream,[I1,I2|LI]) :- !,
- write(Stream,I1),
- write(Stream,","),
- write_loop_ids(Stream,[I2|LI]).
+ write(Stream,I1),
+ write(Stream,","),
+ write_loop_ids(Stream,[I2|LI]).
write_loop_ids(Stream,[I]) :-
- write(Stream,I).
+ write(Stream,I).
print_deltas_vars([]) :-
- writeln(output,"]").
+ writeln(output,"]").
print_deltas_vars([(X,Y,S,C)|Deltas]) :-
- nl(output),
- write(output," delta("),
- printf(output,"%w",X),
- write(output,","),
- printf(output,"%w",Y),
- write(output,","),
- write(output,S),
- write(output,","),
-%% write_canonical(output,C),
- write(output,C),
- write(output,")"),
- (Deltas = [] ->
- writeln(output,"]")
- ; write(output,","),
- print_deltas_vars(Deltas)).
+ nl(output),
+ write(output," delta("),
+ printf(output,"%w",X),
+ write(output,","),
+ printf(output,"%w",Y),
+ write(output,","),
+ write(output,S),
+ write(output,","),
+ (C = L..H ->
+ int_from_integral_rat(L,NL),
+ int_from_integral_rat(H,NH),
+ NC = NL..NH
+ ; int_from_integral_rat(C,NC)),
+ write(output,NC),
+ write(output,")"),
+ (Deltas = [] ->
+ writeln(output,"]")
+ ; write(output,","),
+ print_deltas_vars(Deltas)).
get_deltas_vars(LV,LoopOnly,Deltas) :-
- term_variables(LV,NLV),
- get_deltas_vars(NLV,LoopOnly,[],[],Deltas).
+ term_variables(LV,NLV),
+ get_deltas_vars(NLV,LoopOnly,[],[],Deltas).
get_deltas_vars([],_,_,L,L).
get_deltas_vars([V|LV],LoopOnly,Seen,L,NL) :-
- ((nonvar(V),
- getval(gdbg,1)@eclipse)
- ->
- writeln(output,"Warning get_deltas_vars")
- ; true),
- ((nonvar(V);
- occurs(V,Seen);
- nonvar(LoopOnly),
- get_loop_ids(V,(Loop,_)),
- var(Loop))
+ ((nonvar(V),
+ getval(gdbg,1)@eclipse)
+ ->
+ writeln(output,"Warning get_deltas_vars")
+ ; true),
+ ((nonvar(V);
+ occurs(V,Seen);
+ nonvar(LoopOnly),
+ get_loop_ids(V,(Loop,_)),
+ var(Loop))
%% not get_loop_ids(V,[_|_]))
- ->
- L1 = L,
- NLV = LV,
- NSeen = Seen
- ; get_delta_before_after(V,Before,After),
- collect_deltas_before(Before,LoopOnly,V,L,L0),
- collect_deltas_after(After,LoopOnly,V,L0,L1),
- term_variables((Before,After),LV1),
- append(LV1,LV,LV2),
- term_variables(LV2,NLV),
- NSeen = [V|Seen]),
- get_deltas_vars(NLV,LoopOnly,NSeen,L1,NL).
+ ->
+ L1 = L,
+ NLV = LV,
+ NSeen = Seen
+ ; get_delta_before_after(V,Before,After),
+ collect_deltas_before(Before,LoopOnly,V,L,L0),
+ collect_deltas_after(After,LoopOnly,V,L0,L1),
+ term_variables((Before,After),LV1),
+ append(LV1,LV,LV2),
+ term_variables(LV2,NLV),
+ NSeen = [V|Seen]),
+ get_deltas_vars(NLV,LoopOnly,NSeen,L1,NL).
:- mode collect_deltas_before(+,?,?,+,-).
diff --git a/Src/COLIBRI/realarith.pl b/Src/COLIBRI/realarith.pl
index d76035391cf8e87a341e8989badf849203d13aac..4c01e477eaa81c9a228ff9188a63cec2e7a39e2b 100755
--- a/Src/COLIBRI/realarith.pl
+++ b/Src/COLIBRI/realarith.pl
@@ -2036,6 +2036,8 @@ cast_float_to_double(_Rnd,A,B) :-
set_lazy_domain(float_double,B),
launch_float_number(A),
launch_float_number(B),
+ % Essai BM
+ launch_delta(A,B,=,0),
cast_float_to_double_bis(A,B),
lin_cast_float_to_double(A,B).
@@ -2177,6 +2179,9 @@ cast_double_to_float(Rnd,A,B) :-
launch_float_number(A),
launch_float_number(B),
ensure_not_NaN([A,B]),
+ % Essai BM ?? (surement faux car deux doubles <> peuvent etre = en float)
+ % A calculer selon rnd !!!
+ %launch_delta(A,B,=,0),
(Rnd == rne ->
cast_double_to_float_bis(A,B)
; cast_double_to_float_bis(Rnd,A,B)).
@@ -3403,22 +3408,22 @@ get_float_int_status(V,FIV) :-
%% PMO si les 3 args sont des float_int entre -2^53 et 2^53 on peut
%% deleguer le calcul de add_real aux entiers
check_launch_add_int(_,A,B,C,Continue,_) :-
- var(Continue),
- !.
+ var(Continue),
+ !.
check_launch_add_int(Type,A,B,C,_,Continue) :-
- ((term_variables((A,B,C),[_,_|_]),
- is_float_int_number(A),
- is_float_int_number(B),
- is_float_int_number(C),
- is_inside_mantissa(Type,A),
- is_inside_mantissa(Type,B),
- is_inside_mantissa(Type,C))
- ->
- cast_real_int(Type,A,IA),
- cast_real_int(Type,B,IB),
- cast_real_int(Type,C,IC),
- add(IA,IB,IC)
- ; Continue = 1).
+ ((term_variables((A,B,C),[_,_|_]),
+ is_float_int_number(A),
+ is_float_int_number(B),
+ is_float_int_number(C),
+ is_inside_mantissa(Type,A),
+ is_inside_mantissa(Type,B),
+ is_inside_mantissa(Type,C))
+ ->
+ cast_real_int(Type,A,IA),
+ cast_real_int(Type,B,IB),
+ cast_real_int(Type,C,IC),
+ add(IA,IB,IC)
+ ; Continue = 1).
exists_feq(Type,A,A) ?- !.
exists_feq(Type,A,B) :-
@@ -3930,23 +3935,6 @@ check_rbox_rat(A,Rat) :-
AbsA =\= 1.0Inf,
Rat is rational(A)
; is_real_box_rat(A,Rat)).
-/*
-ANCIENNE VERSION OU ON RELIT LA STRING
-POUR CREER UN RATIONNEL
-MAIS EN MODE REEL ON GARDE DES RATIONNELS
-DANS GATEL (SMTLIB ??)
-check_rbox_rat(A,Rat) :-
- (float(A) ->
- abs(A,AbsA),
- AbsA =\= 1.0Inf,
- term_string(AbsA,Str),
- (rat_of_decimal_string(Str,RAbsA) ->
- (A >= 0.0 ->
- Rat = RAbsA
- ; Rat is - RAbsA)
- ; Rat is rational(A))
- ; is_real_box_rat(A,Rat)).
-*/
rat_of_decimal_string(Str0,Rat) :-
(append_strings("-",Str1,Str0) ->
@@ -4230,41 +4218,41 @@ absorbed_range_from_max_neg(Type,MaxN,LN,HN):-
add_real_rec(Type,A,B,C) :-
- getval(real_simp,RS)@eclipse,
- add_real_rec_bis(10,RS,Type,A,B,C).
+ getval(real_simp,RS)@eclipse,
+ add_real_rec_bis(10,RS,Type,A,B,C).
add_real_rec_bis(0,1,Type,A,B,C) :- !,
- (getval(gdbg,1)@eclipse ->
- writeln(output,max_iter:add_real_rec_bis(A,B,C))
- ; true).
+ (getval(gdbg,1)@eclipse ->
+ writeln(output,max_iter:add_real_rec_bis(A,B,C))
+ ; true).
add_real_rec_bis(Cpt,RS,Type,A,B,C) :-
- mreal:dvar_domain(A,DomA),
- mreal:dvar_domain(B,DomB),
- mreal:dvar_domain(C,DomC),
- (RS == 1 ->
- get_rel_between_real_args(A,B,RelAB),
- get_rel_between_real_args(C,B,RelCB),
- get_rel_between_real_args(C,A,RelCA),
- get_float_int_status(A,FIA),
- get_float_int_status(B,FIB),
- get_float_int_status(C,FIC)
- ; (RelAB,RelCB,RelCA) = (?,?,?),
- (FIA,FIB,FIC) = (0,0,0)),
- %% Projections
- add_real_rec(Type,RS,FIA,FIB,FIC,DomA,DomB,DomC,RelAB,RelCB,RelCA,NDomA,NDomB,NDomC),
- mreal:dvar_set(A,NDomA),
- mreal:dvar_set(B,NDomB),
- mreal:dvar_set(C,NDomC),
- (RS == 1 ->
- mreal:dvar_domain(A,NewDomA),
- mreal:dvar_domain(B,NewDomB),
- mreal:dvar_domain(C,NewDomC),
- % = necessaire
- ((NDomA,NDomB,NDomC) = (NewDomA,NewDomB,NewDomC) ->
- true
- ; NCpt is Cpt - 1,
- add_real_rec_bis(NCpt,RS,Type,A,B,C))
- ; true).
+ mreal:dvar_domain(A,DomA),
+ mreal:dvar_domain(B,DomB),
+ mreal:dvar_domain(C,DomC),
+ (RS == 1 ->
+ get_rel_between_real_args(A,B,RelAB),
+ get_rel_between_real_args(C,B,RelCB),
+ get_rel_between_real_args(C,A,RelCA),
+ get_float_int_status(A,FIA),
+ get_float_int_status(B,FIB),
+ get_float_int_status(C,FIC)
+ ; (RelAB,RelCB,RelCA) = (?,?,?),
+ (FIA,FIB,FIC) = (0,0,0)),
+ % Projections
+ add_real_rec(Type,RS,FIA,FIB,FIC,DomA,DomB,DomC,RelAB,RelCB,RelCA,NDomA,NDomB,NDomC),
+ mreal:dvar_set(A,NDomA),
+ mreal:dvar_set(B,NDomB),
+ mreal:dvar_set(C,NDomC),
+ (RS == 1 ->
+ mreal:dvar_domain(A,NewDomA),
+ mreal:dvar_domain(B,NewDomB),
+ mreal:dvar_domain(C,NewDomC),
+ % = necessaire
+ ((NDomA,NDomB,NDomC) = (NewDomA,NewDomB,NewDomC) ->
+ true
+ ; NCpt is Cpt - 1,
+ add_real_rec_bis(NCpt,RS,Type,A,B,C))
+ ; true).
is_fzero(Z) :-
(float(Z) ->
@@ -4363,56 +4351,57 @@ get_rel_between_real_args_from_cstrs(A,B,'?').
:- mode add_real_rec(++,++,++,++,++,++,++,++,++,++,++,-,-,-).
add_real_rec(real,_,FIA,FIB,FIC,DomA,DomB,DomC,RelAB,RelCB,RelCA,NDomA,NDomB,NDomC) :- !,
- add_real_rec1(FIA,FIB,FIC,DomA,DomB,DomC,RelAB,RelCB,RelCA,NDomA,NDomB,NDomC).
-add_real_rec(Type,RS,FIA,FIB,FIC,DomA0,DomB0,DomC,RelAB,RelCB,RelCA,NDomA,NDomB,NDomC) :-
- %% On reduit les domaines de A et B par les proprietes de
- %% NON CANCELATION (C <> 0) et NON ABSORBTION (A ou B <> C)
- reduce_dom_add_args_from_res(RS,Type,FIA,FIB,FIC,RelCA,RelCB,DomA0,DomB0,DomC,DomA,DomB),
- %% Si C instancie et non nul on peut avoir une convergence tr�s lente
- %% (ex: add_real(A,B,2.1))
- %% On utilise donc un compteur pour limiter les iterations de
- %% add_float_rec
- add_float_rec(RS,Type,3,FIA,FIB,FIC,DomA,DomB,DomC,RelAB,RelCB,RelCA,NDomA,NDomB,NDomC).
+ add_real_rec1(FIA,FIB,FIC,DomA,DomB,DomC,RelAB,RelCB,RelCA,NDomA,NDomB,NDomC).
+add_real_rec(Type,RS,FIA,FIB,FIC,DomA0,DomB0,DomC,RelAB,RelCB,RelCA,
+ NDomA,NDomB,NDomC) :-
+ % On reduit les domaines de A et B par les proprietes de
+ % NON CANCELATION (C <> 0) et NON ABSORBTION (A ou B <> C)
+ reduce_dom_add_args_from_res(RS,Type,FIA,FIB,FIC,RelCA,RelCB,DomA0,DomB0,DomC,DomA,DomB),
+ % Si C instancie et non nul on peut avoir une convergence tr�s lente
+ % (ex: add_real(A,B,2.1))
+ % On utilise donc un compteur pour limiter les iterations de
+ % add_float_rec
+ add_float_rec(RS,Type,3,FIA,FIB,FIC,DomA,DomB,DomC,RelAB,RelCB,RelCA,NDomA,NDomB,NDomC).
%% MODE real
:- mode add_real_rec1(++,++,++,++,++,++,++,++,++,-,-,-).
add_real_rec1(FIA,FIB,FIC,DomA,DomB,DomC,RelAB,RelCB,RelCA,NDomA,NDomB,NDomC) :-
- mreal:dom_interval(DomA,InterA),
- mreal:dom_interval(DomB,InterB),
- mreal:dom_interval(DomC,InterC),
- %% On freine des qu'un des produit cart�sien est sup a MaxProd
- (check_maxprod_intervals(InterA,InterB,InterC) ->
- %% On ne travaille que sur les bornes
- add_real_dom_bounds(RelAB,FIC,DomA,DomB,DomC,DomC0),
- real_inter_dom_if_eq(RelCA,RelCB,DomA,DomB,DomC0,DomA1,DomB1,DomC1),
- inv_add_real_dom_bounds(RelCB,FIA,DomC1,DomB1,DomA1,DomA10),
- real_inter_dom_if_eq(RelCA,RelAB,DomC1,DomB1,DomA10,DomC2,DomB2,DomA2),
- inv_add_real_dom_bounds(RelCA,FIB,DomC2,DomA2,DomB2,DomB20)
- ; add_real_dom(RelAB,FIC,DomA,DomB,DomC,DomC0),
- real_inter_dom_if_eq(RelCA,RelCB,DomA,DomB,DomC0,DomA1,DomB1,DomC1),
- inv_add_real_dom(RelCB,FIA,DomC1,DomB1,DomA1,DomA10),
- real_inter_dom_if_eq(RelCA,RelAB,DomC1,DomB1,DomA10,DomC2,DomB2,DomA2),
- inv_add_real_dom(RelCA,FIB,DomC2,DomA2,DomB2,DomB20)),
-
- real_inter_dom_if_eq(RelCB,RelAB,DomC2,DomA2,DomB20,DomC3,DomA3,DomB3),
-
- (((DomA3 == DomA,
- DomB3 == DomB,
- DomC3 == DomC0);
- (mreal:dom_size(DomA3,1),
- mreal:dom_size(DomB3,1)))
- ->
- NDomA = DomA3,
- NDomB = DomB3,
- NDomC = DomC3
- ; add_real_rec1(FIA,FIB,FIC,DomA3,DomB3,DomC3,RelAB,RelCB,RelCA,NDomA,NDomB,NDomC)).
+ mreal:dom_interval(DomA,InterA),
+ mreal:dom_interval(DomB,InterB),
+ mreal:dom_interval(DomC,InterC),
+ % On freine des qu'un des produit cartésien est sup a MaxProd
+ (check_maxprod_intervals(InterA,InterB,InterC) ->
+ % On ne travaille que sur les bornes
+ add_real_dom_bounds(RelAB,FIC,DomA,DomB,DomC,DomC0),
+ real_inter_dom_if_eq(RelCA,RelCB,DomA,DomB,DomC0,DomA1,DomB1,DomC1),
+ inv_add_real_dom_bounds(RelCB,FIA,DomC1,DomB1,DomA1,DomA10),
+ real_inter_dom_if_eq(RelCA,RelAB,DomC1,DomB1,DomA10,DomC2,DomB2,DomA2),
+ inv_add_real_dom_bounds(RelCA,FIB,DomC2,DomA2,DomB2,DomB20)
+ ; add_real_dom(RelAB,FIC,DomA,DomB,DomC,DomC0),
+ real_inter_dom_if_eq(RelCA,RelCB,DomA,DomB,DomC0,DomA1,DomB1,DomC1),
+ inv_add_real_dom(RelCB,FIA,DomC1,DomB1,DomA1,DomA10),
+ real_inter_dom_if_eq(RelCA,RelAB,DomC1,DomB1,DomA10,DomC2,DomB2,DomA2),
+ inv_add_real_dom(RelCA,FIB,DomC2,DomA2,DomB2,DomB20)),
+
+ real_inter_dom_if_eq(RelCB,RelAB,DomC2,DomA2,DomB20,DomC3,DomA3,DomB3),
+
+ (((DomA3 == DomA,
+ DomB3 == DomB,
+ DomC3 == DomC0);
+ (mreal:dom_size(DomA3,1),
+ mreal:dom_size(DomB3,1)))
+ ->
+ NDomA = DomA3,
+ NDomB = DomB3,
+ NDomC = DomC3
+ ; add_real_rec1(FIA,FIB,FIC,DomA3,DomB3,DomC3,RelAB,RelCB,RelCA,NDomA,NDomB,NDomC)).
%% EqAC
real_inter_dom_if_eq('=',EqBC,DomA,DomB,DomC,NDom,DomB,NDom) :- !,
- mreal:dom_intersection(DomA,DomC,NDom,_).
+ mreal:dom_intersection(DomA,DomC,NDom,_).
%% EqBC
real_inter_dom_if_eq(_,'=',DomA,DomB,DomC,DomA,NDom,NDom) :- !,
- mreal:dom_intersection(DomB,DomC,NDom,_).
+ mreal:dom_intersection(DomB,DomC,NDom,_).
real_inter_dom_if_eq(_,_,DomA,DomB,DomC,DomA,DomB,DomC).
@@ -5103,120 +5092,120 @@ inv_add_float_interval_list_rel(Type,Rel12,Min1,Max1,Min2,Max2,LInter2,Min,Max,L
add_real_dom_bounds(_,_,_,_,Dom,NewDom) :-
- mreal:dom_size(Dom,1),
- !,
- NewDom = Dom.
+ mreal:dom_size(Dom,1),
+ !,
+ NewDom = Dom.
add_real_dom_bounds(_,FI,Dom1,Dom2,Dom,NewDom) :-
- mreal:dom_range(Dom1,Min1,Max1),
- mreal:dom_range(Dom2,Min2,Max2),
- interval_from_bounds(Min1,Max1,I1),
- interval_from_bounds(Min2,Max2,I2),
- add_real_float_intervals(real,I1,I2,B1,B2),
- build_new_dom_from_bounds(real,FI,B1,B2,Dom,NewDom).
+ mreal:dom_range(Dom1,Min1,Max1),
+ mreal:dom_range(Dom2,Min2,Max2),
+ interval_from_bounds(Min1,Max1,I1),
+ interval_from_bounds(Min2,Max2,I2),
+ add_real_float_intervals(real,I1,I2,B1,B2),
+ build_new_dom_from_bounds(real,FI,B1,B2,Dom,NewDom).
inv_add_real_dom_bounds(Rel12,FI,Dom1,Dom2,Dom,NewDom) :-
- mreal:dom_interval(Dom1,L1),
- mreal:dom_interval(Dom2,L2),
- ((occurs(-1.0Inf,(L1,L2));
- occurs(1.0Inf,(L1,L2)))
- ->
- NewDom = Dom
- ; minus_real_dom_bounds(Rel12,FI,Dom1,Dom2,Dom,NewDom)).
+ mreal:dom_interval(Dom1,L1),
+ mreal:dom_interval(Dom2,L2),
+ (fail,(occurs(-1.0Inf,(L1,L2));
+ occurs(1.0Inf,(L1,L2)))
+ ->
+ NewDom = Dom
+ ; minus_real_dom_bounds(Rel12,FI,Dom1,Dom2,Dom,NewDom)).
minus_real_dom_bounds(_,_,_,_,Dom,NewDom) :-
- mreal:dom_size(Dom,1),
- !,
- NewDom = Dom.
+ mreal:dom_size(Dom,1),
+ !,
+ NewDom = Dom.
minus_real_dom_bounds(Rel12,FI,Dom1,Dom2,Dom,NewDom) :-
- mreal:dom_range(Dom1,Min1,Max1),
- mreal:dom_range(Dom2,Min2,Max2),
- interval_from_bounds(Min1,Max1,I1),
- interval_from_bounds(Min2,Max2,I2),
- minus_real_float_intervals(real,I1,I2,B10,B20),
- adjust_minus_rf_bounds_from_Rel(Rel12,B10,B20,B1,B2),
- build_new_dom_from_bounds(real,FI,B1,B2,Dom,NewDom).
+ mreal:dom_range(Dom1,Min1,Max1),
+ mreal:dom_range(Dom2,Min2,Max2),
+ interval_from_bounds(Min1,Max1,I1),
+ interval_from_bounds(Min2,Max2,I2),
+ minus_real_float_intervals(real,I1,I2,B10,B20),
+ adjust_minus_rf_bounds_from_Rel(Rel12,B10,B20,B1,B2),
+ build_new_dom_from_bounds(real,FI,B1,B2,Dom,NewDom).
inv1_minus_real_dom_bounds(Rel12,FI,Dom1,Dom2,Dom,NewDom) :-
- mreal:dom_interval(Dom1,L1),
- mreal:dom_interval(Dom2,L2),
- ((occurs(-1.0Inf,(L1,L2));
- occurs(1.0Inf,(L1,L2)))
- ->
- NewDom = Dom
- ; add_real_dom_bounds(Rel12,FI,Dom1,Dom2,Dom,NewDom)).
+ mreal:dom_interval(Dom1,L1),
+ mreal:dom_interval(Dom2,L2),
+ (fail,(occurs(-1.0Inf,(L1,L2));
+ occurs(1.0Inf,(L1,L2)))
+ ->
+ NewDom = Dom
+ ; add_real_dom_bounds(Rel12,FI,Dom1,Dom2,Dom,NewDom)).
inv2_minus_real_dom_bounds(Rel12,FI,Dom1,Dom2,Dom,NewDom) :-
- mreal:dom_interval(Dom1,L1),
- mreal:dom_interval(Dom2,L2),
- ((occurs(-1.0Inf,(L1,L2));
- occurs(1.0Inf,(L1,L2)))
- ->
- NewDom = Dom
- ; minus_real_dom_bounds(Rel12,FI,Dom1,Dom2,Dom,NewDom)).
+ mreal:dom_interval(Dom1,L1),
+ mreal:dom_interval(Dom2,L2),
+ (fail,(occurs(-1.0Inf,(L1,L2));
+ occurs(1.0Inf,(L1,L2)))
+ ->
+ NewDom = Dom
+ ; minus_real_dom_bounds(Rel12,FI,Dom1,Dom2,Dom,NewDom)).
add_real_dom(_,_,_,_,Dom,NewDom) :-
- mreal:dom_size(Dom,1),
- !,
- NewDom = Dom.
+ mreal:dom_size(Dom,1),
+ !,
+ NewDom = Dom.
add_real_dom(Rel12,FI,Dom1,Dom2,Dom,NewDom) :-
- mreal:dom_interval(Dom1,L1),
- mreal:dom_interval(Dom2,L2),
- ((L1 = [_],
- L2 = [_])
- ->
- add_real_dom_bounds(_,FI,Dom1,Dom2,Dom,NewDom)
- ; mreal:dom_range(Dom,Min,Max),
- add_rf_interval_list(Rel12,real,L1,L2,Min,Max,LInter),
- mreal:list_to_typed_dom(real,LInter,NDom),
- mreal:dom_intersection(NDom,Dom,NewDom0,_),
- reduce_float_int_domain(real,FI,NewDom0,NewDom)).
-
+ mreal:dom_interval(Dom1,L1),
+ mreal:dom_interval(Dom2,L2),
+ ((L1 = [_],
+ L2 = [_])
+ ->
+ add_real_dom_bounds(_,FI,Dom1,Dom2,Dom,NewDom)
+ ; mreal:dom_range(Dom,Min,Max),
+ add_rf_interval_list(Rel12,real,L1,L2,Min,Max,LInter),
+ mreal:list_to_typed_dom(real,LInter,NDom),
+ mreal:dom_intersection(NDom,Dom,NewDom0,_),
+ reduce_float_int_domain(real,FI,NewDom0,NewDom)).
+
inv_add_real_dom(Rel12,FI,Dom1,Dom2,Dom,NewDom) :-
- mreal:dom_interval(Dom1,L1),
- mreal:dom_interval(Dom2,L2),
- ((occurs(-1.0Inf,(L1,L2));
- occurs(1.0Inf,(L1,L2)))
- ->
- NewDom = Dom
- ; minus_real_dom(Rel12,FI,Dom1,Dom2,Dom,NewDom)).
+ mreal:dom_interval(Dom1,L1),
+ mreal:dom_interval(Dom2,L2),
+ (fail,(occurs(-1.0Inf,(L1,L2));
+ occurs(1.0Inf,(L1,L2)))
+ ->
+ NewDom = Dom
+ ; minus_real_dom(Rel12,FI,Dom1,Dom2,Dom,NewDom)).
minus_real_dom(_,_,_,_,Dom,NewDom) :-
- mreal:dom_size(Dom,1),
- !,
- NewDom = Dom.
+ mreal:dom_size(Dom,1),
+ !,
+ NewDom = Dom.
minus_real_dom(Rel12,FI,Dom1,Dom2,Dom,NewDom) :-
- mreal:dom_interval(Dom1,L1),
- mreal:dom_interval(Dom2,L2),
- ((L1 = [_],
- L2 = [_])
- ->
- minus_real_dom_bounds(Rel12,FI,Dom1,Dom2,Dom,NewDom)
- ; mreal:dom_range(Dom,Min,Max),
- minus_rf_interval_list(Rel12,real,L1,L2,Min,Max,LInter),
- mreal:list_to_typed_dom(real,LInter,NDom),
- mreal:dom_intersection(NDom,Dom,NewDom0,_),
- reduce_float_int_domain(real,FI,NewDom0,NewDom)).
+ mreal:dom_interval(Dom1,L1),
+ mreal:dom_interval(Dom2,L2),
+ ((L1 = [_],
+ L2 = [_])
+ ->
+ minus_real_dom_bounds(Rel12,FI,Dom1,Dom2,Dom,NewDom)
+ ; mreal:dom_range(Dom,Min,Max),
+ minus_rf_interval_list(Rel12,real,L1,L2,Min,Max,LInter),
+ mreal:list_to_typed_dom(real,LInter,NDom),
+ mreal:dom_intersection(NDom,Dom,NewDom0,_),
+ reduce_float_int_domain(real,FI,NewDom0,NewDom)).
inv1_minus_real_dom(Rel12,FI,Dom1,Dom2,Dom,NewDom) :-
- mreal:dom_interval(Dom1,L1),
- mreal:dom_interval(Dom2,L2),
- ((occurs(-1.0Inf,(L1,L2));
- occurs(1.0Inf,(L1,L2)))
- ->
- NewDom = Dom
- ; add_real_dom(Rel12,FI,Dom1,Dom2,Dom,NewDom)).
+ mreal:dom_interval(Dom1,L1),
+ mreal:dom_interval(Dom2,L2),
+ (fail,(occurs(-1.0Inf,(L1,L2));
+ occurs(1.0Inf,(L1,L2)))
+ ->
+ NewDom = Dom
+ ; add_real_dom(Rel12,FI,Dom1,Dom2,Dom,NewDom)).
inv2_minus_real_dom(Rel12,FI,Dom1,Dom2,Dom,NewDom) :-
- mreal:dom_interval(Dom1,L1),
- mreal:dom_interval(Dom2,L2),
- ((occurs(-1.0Inf,(L1,L2));
- occurs(1.0Inf,(L1,L2)))
- ->
- NewDom = Dom
- ; minus_real_dom(Rel12,FI,Dom1,Dom2,Dom,NewDom)).
+ mreal:dom_interval(Dom1,L1),
+ mreal:dom_interval(Dom2,L2),
+ (fail,(occurs(-1.0Inf,(L1,L2));
+ occurs(1.0Inf,(L1,L2)))
+ ->
+ NewDom = Dom
+ ; minus_real_dom(Rel12,FI,Dom1,Dom2,Dom,NewDom)).
@@ -5226,11 +5215,21 @@ inv2_minus_real_dom(Rel12,FI,Dom1,Dom2,Dom,NewDom) :-
add_real_ineqs(Type,A,B,C) :-
getval(use_delta,1)@eclipse,
!,
+ ndelta:disable_delta_check,
(var(C) ->
- ndelta:disable_delta_check,
- add_real_ineq(Type,A,B,C),
- add_real_ineq(Type,B,A,C)
- ; true),
+ (Type == real ->
+ add_real_int_ineqs(A,B,C)
+ ; add_real_ineq(Type,A,B,C),
+ add_real_ineq(Type,B,A,C))
+ ; % en real, Si A ou B est un op_real
+ % A + op(OpB) = Cst -> A = Cst + OpB
+ (Type == real ->
+ (get_op_real(A,OpA) ->
+ add_real_int_ineqs(C,OpA,B)
+ ; (get_op_real(B,OpB) ->
+ add_real_int_ineqs(C,OpB,A)
+ ; true))
+ ; true)),
((Type == real;
is_exact(Type,add,A,B))
->
@@ -5245,9 +5244,142 @@ add_real_ineqs(Type,A,B,C) :-
->
add_real_2_args_equal(Type,A,B,C,_Continue)
; true),
- ndelta:allow_delta_check.
-add_real_ineqs(Type,A,B,C).
-
+ ndelta:allow_delta_check,
+ ((Type == real,
+ not_zero(C))
+ ->
+ check_exists_lin_expr_giving_diff_args(real,C,0.0,_Stop)
+ ; true),
+ bin_op_real_ineq(Type,add_real1,A,B,C).
+%add_real_ineqs(Type,A,B,C).
+add_real_ineqs(Type,A,B,C) :-
+ ((Type == real,
+ not_zero(C))
+ ->
+ check_exists_lin_expr_giving_diff_args(real,C,0.0,_Stop)
+ ; true),
+ bin_op_real_ineq(Type,add_real1,A,B,C).
+
+% pour les real et real_int
+add_real_int_ineqs(A,B,C) :-
+ var(C),
+ !,
+ launch_delta_add_real_int(A,B,C),
+ launch_delta_add_real_int(B,A,C).
+add_real_int_ineqs(_,_,_).
+
+launch_delta_add_real_int(A,B,C) :-
+ var(B),
+ !,
+ (is_real_box_rat(A,RA) ->
+ launch_delta(B,C,=,RA)
+ ; mreal:dvar_range(A,LA,HA),
+ (LA == -1.0Inf ->
+ (HA == 1.0Inf ->
+ true
+ ; rational(HA,H),
+ L = LA)
+ ; (HA == 1.0Inf ->
+ rational(LA,L),
+ H = HA
+ ; rational(LA,L),
+ rational(HA,H))),
+ (nonvar(L) ->
+ launch_delta(B,C,+,L..H)
+ ; true)).
+launch_delta_add_real_int(A,B,C).
+
+minus_real_int_ineqs(A,B,C) :-
+ % A = B + C,
+ add_real_int_ineqs(B,C,A).
+
+op_real_int_ineqs(A,OpA) :-
+ % 0 - A = OpA
+ minus_real_int_ineqs(0.0,A,OpA).
+
+
+
+get_op_real(A,OpA) :-
+ get_saved_cstr_suspensions(LS),
+ member((_,op_real1(_,X,Y)),LS),
+ (A == X ->
+ OpA = Y
+ ; A == Y,
+ OpA = X).
+
+bin_op_real_ineq(Type,Op,A,B,C) :-
+ % Si on a un carré et que les résultats sont en relation
+ % alors les arguments non identiques ont la même relation
+ % pour les Op commutatifs ou les arg1 pour les Op non commutatifs
+ % Les arg2 sur les Op non commutatifs sont en relation opposée
+ Type == real,
+ occurs(Op,(add_real1,mult_real1,minus_real1,div_real1)),
+ !,
+ (occurs(Op,(minus_real1,div_real1)) ->
+ Only_arg1 = 1
+ ; true),
+ get_saved_cstr_suspensions(LSusp),
+ SGoal =.. [Op,Type,X,Y,Z],
+ ((member((_,SGoal),LSusp),
+ (A == X ->
+ OpRel = 1,
+ O1 = B,
+ O2 = Y
+ ; (B == Y ->
+ O1 = A,
+ O2 = X
+ ; nonvar(Only_arg1),
+ (A == Y ->
+ O1 = B,
+ O2 = X
+ ; B == X,
+ O1 = A,
+ O2 = Y))),
+ get_rel_between_real_args(C,Z,Rel0),
+ Rel0 \== '?',
+ ((var(Only_arg1);
+ var(OpRel);
+ occurs(Rel0,(=,#)))
+ ->
+ Rel = Rel0
+ ; op_rel(Rel0,Rel)))
+ ->
+ (Rel == '=' ->
+ Goal = protected_unify(O1,O2)
+ ; get_rel_between_real_args(O1,O2,Rel12),
+ (Rel == '<' ->
+ not occurs(Rel12,('=','>')),
+ (Rel == Rel12 ->
+ true
+ ; Goal = launch_gt_real(Type,O2,O1))
+ ; (Rel == '=<' ->
+ not occurs(Rel12,('>')),
+ (Rel == Rel12 ->
+ true
+ ; Goal = launch_geq_real(Type,O2,O1))
+ ; (Rel == '>' ->
+ not occurs(Rel12,('=','<')),
+ (Rel == Rel12 ->
+ true
+ ; Goal = launch_gt_real(Type,O1,O2))
+ ; (Rel == '>=' ->
+ not occurs(Rel12,('<')),
+ (Rel == Rel12 ->
+ true
+ ; Goal = launch_geq_real(Type,O1,O2))
+ ; % Rel = #
+ (Rel == Rel12 ->
+ true
+ ; Goal = launch_diff_real(Type,O1,O2))))))),
+ (var(Goal) ->
+ true
+ ; call(Goal)),
+ % on restaure
+ setval(saved_suspensions,(1,LSusp))
+ ; true).
+bin_op_real_ineq(Type,Op,A,B,C).
+
+
real_ineqs_with_other_add_minus_int(Type,A,B,C,Exact) :-
((is_float_int_number(A),
is_inside_mantissa(Type,A);
@@ -5341,7 +5473,8 @@ real_ineqs_with_other_add_minus_int(Type,A,B,C,Exact) :-
; true))
; true).
-% Test si une somme/soustraction est exacte
+% Test si un add/minus/mult/div est exact
+is_exact(real,_,_,_) :- !.
is_exact(Type,add,A,B) :-
mreal:dvar_range(A,L1,H1),
mreal:dvar_range(B,L2,H2),
@@ -5669,24 +5802,24 @@ forbid_zero0(Type,Var) :-
build_delta_add_real(Type,A,B,C,MinDelta,MaxDelta) :-
- mreal:dvar_range(A,MinA,MaxA),
- mreal:dvar_range(B,MinB,MaxB),
- (MinA >= 0.0 ->
- %% B =< C, on AVANCE de MinA depuis B
- %% MinDelta pour MinA et absorbtion maximale de B
- get_MinDelta_forward(Type,MinA,MinB,MaxB,MinDelta),
- %% MaxDelta pour MaxA et absorbtion minimale de B
- get_MaxDelta_forward(Type,MaxA,MinB,MaxB,MaxDelta)
- ; (MaxA =< 0.0 ->
- %% B >= C, on RECULE, MinDelta et MaxDelta negatif
- %% MinDelta pour MinA et absorbtion minimale de B
- get_MinDelta_backward(Type,MinA,MinB,MaxB,MinDelta),
- %% MaxDelta pour MaxA et absorbtion maximale de B
- get_MaxDelta_backward(Type,MaxA,MinB,MaxB,MaxDelta)
- ; %% On RECULE de la distance max pour MinA
- get_MinDelta_backward(Type,MinA,MinB,MaxB,MinDelta),
- %% On AVANCE de la distance max pour MaxA
- get_MaxDelta_forward(Type,MaxA,MinB,MaxB,MaxDelta))).
+ mreal:dvar_range(A,MinA,MaxA),
+ mreal:dvar_range(B,MinB,MaxB),
+ (MinA >= 0.0 ->
+ % B =< C, on AVANCE de MinA depuis B
+ % MinDelta pour MinA et absorbtion maximale de B
+ get_MinDelta_forward(Type,MinA,MinB,MaxB,MinDelta),
+ % MaxDelta pour MaxA et absorbtion minimale de B
+ get_MaxDelta_forward(Type,MaxA,MinB,MaxB,MaxDelta)
+ ; (MaxA =< 0.0 ->
+ % B >= C, on RECULE, MinDelta et MaxDelta negatif
+ % MinDelta pour MinA et absorbtion minimale de B
+ get_MinDelta_backward(Type,MinA,MinB,MaxB,MinDelta),
+ % MaxDelta pour MaxA et absorbtion maximale de B
+ get_MaxDelta_backward(Type,MaxA,MinB,MaxB,MaxDelta)
+ ; % On RECULE de la distance max pour MinA
+ get_MinDelta_backward(Type,MinA,MinB,MaxB,MinDelta),
+ % On AVANCE de la distance max pour MaxA
+ get_MaxDelta_forward(Type,MaxA,MinB,MaxB,MaxDelta))).
%% DEPLACEMENTS POSITIFS: MinA >= 0.0
@@ -7605,36 +7738,38 @@ op_real_ineq(Type,A,B) :-
var(B),
getval(use_delta,1)@eclipse,
!,
- % 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;
+ (Type == real ->
+ op_real_int_ineqs(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,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
@@ -7646,7 +7781,7 @@ op_real_ineq(Type,A,B) :-
param(A,B,Type) do
((T \== A,
get_rel_between_real_args(B,T,RelOpAT),
- occurs(Rel,('<','=<','>','>=')),
+ occurs(RelOpAT,('<','=<','>','>=','#')),
get_cstr_suspensions(T,LSusp),
member(Susp,LSusp),
get_suspension_data(Susp,goal,op_real1(Type,TT,OpTT)),
@@ -7670,11 +7805,15 @@ op_real_ineq(Type,A,B) :-
(ORel == '<' ->
true
; gt_real_ineq(Type,A,OpT))
- ; % RelOpAT = =<
- ORel \== '>',
- (ORel == '=<' ->
- true
- ; geq_real_ineq(Type,A,OpT)))))
+ ; (RelOpAT == '=<' ->
+ ORel \== '>',
+ (ORel == '=<' ->
+ true
+ ; geq_real_ineq(Type,A,OpT))
+ ; % RelOpAT = #
+ (occurs(ORel,('#','<','>')) ->
+ true
+ ; diff_real_ineq(Type,A,OpT))))))
; true)).
op_real_ineq(_,_,_).
@@ -7865,37 +8004,43 @@ minus_real(Type,A,B,C) :-
add_real(Type,A,OpBB,C).
*/
minus_real(Type,A,B,C) :-
- get_priority(Prio),
- set_priority(1),
- ensure_not_NaN((A,B,C)),
- set_lazy_domain(Type,A),
- set_lazy_domain(Type,B),
- set_lazy_domain(Type,C),
- check_no_float_error(Type,(A,B,C)),
- (Type == real ->
- true
- ; launch_float_number(A),
- launch_float_number(B),
- launch_float_number(C)),
- (ground((A,B)) ->
- minus_real_inst(Type,A,B,C,_)
- ; same_float_int_number_status(Type,A,B,C),
- % Calcul de la premiere projection
- minus_real_interval(Type,A,B,C),
- minus_real1(Type,A,B,C),
- lin_minus_real(Type,A,B,C)),
- set_priority(Prio),
- wake_if_other_scheduled(Prio).
-
-%% Typage et premiere projection
-%% utilise aussi en evaluation
-minus_real_interval(Val1,Val2,Val) :-
- getval(float_eval,Type)@eclipse,
- set_lazy_domain(Type,Val),
- minus_real_interval_type(Type,Val1,Val2,Val).
-
-minus_real_interval_type(real,Val1,Val2,Val) ?- !,
- set_lazy_domain(real,Val),
+ ((Type == real,
+ var(A),
+ var(B),
+ number(C))
+ ->
+ add_real(real,B,C,A)
+ ; get_priority(Prio),
+ set_priority(1),
+ ensure_not_NaN((A,B,C)),
+ set_lazy_domain(Type,A),
+ set_lazy_domain(Type,B),
+ set_lazy_domain(Type,C),
+ check_no_float_error(Type,(A,B,C)),
+ (Type == real ->
+ true
+ ; launch_float_number(A),
+ launch_float_number(B),
+ launch_float_number(C)),
+ (ground((A,B)) ->
+ minus_real_inst(Type,A,B,C,_)
+ ; same_float_int_number_status(Type,A,B,C),
+ % Calcul de la premiere projection
+ minus_real_interval(Type,A,B,C),
+ minus_real1(Type,A,B,C),
+ lin_minus_real(Type,A,B,C)),
+ set_priority(Prio),
+ wake_if_other_scheduled(Prio)).
+
+%% Typage et premiere projection
+%% utilise aussi en evaluation
+minus_real_interval(Val1,Val2,Val) :-
+ getval(float_eval,Type)@eclipse,
+ set_lazy_domain(Type,Val),
+ minus_real_interval_type(Type,Val1,Val2,Val).
+
+minus_real_interval_type(real,Val1,Val2,Val) ?- !,
+ set_lazy_domain(real,Val),
minus_real_interval(real,Val1,Val2,Val).
minus_real_interval_type(Type,Val1,Val2,Val) :-
set_lazy_domain(Type,Val),
@@ -8077,22 +8222,22 @@ check_RelAC_minus_real(_,_,_).
%% PMO si les 3 args sont des float_int entre -2^53 et 2^53 on peut
%% deleguer le calcul de minus_real aux entiers
check_launch_minus_int(Type,A,B,C,Continue,_) :-
- var(Continue),
- !.
+ var(Continue),
+ !.
check_launch_minus_int(Type,A,B,C,_,Continue) :-
- ((term_variables((A,B,C),[_,_|_]),
- is_float_int_number(A),
- is_float_int_number(B),
- is_float_int_number(C),
- is_inside_mantissa(Type,A),
- is_inside_mantissa(Type,B),
- is_inside_mantissa(Type,C))
- ->
- cast_real_int(Type,A,IA),
- cast_real_int(Type,B,IB),
- cast_real_int(Type,C,IC),
- add(IB,IC,IA)
- ; Continue = 1).
+ ((term_variables((A,B,C),[_,_|_]),
+ is_float_int_number(A),
+ is_float_int_number(B),
+ is_float_int_number(C),
+ is_inside_mantissa(Type,A),
+ is_inside_mantissa(Type,B),
+ is_inside_mantissa(Type,C))
+ ->
+ cast_real_int(Type,A,IA),
+ cast_real_int(Type,B,IB),
+ cast_real_int(Type,C,IC),
+ add(IB,IC,IA)
+ ; Continue = 1).
%% Identites communes real/float
minus_real_2_args_equal(Type,A,A,C,_) ?- !,
@@ -8186,6 +8331,9 @@ minus_real_ineqs(Type,A,B,C) :-
getval(use_delta,1)@eclipse,
!,
ndelta:disable_delta_check,
+ (Type == real ->
+ minus_real_int_ineqs(A,B,C)
+ ; true),
((var(C),
Type \== real) % peut creer des forbid_zero residus sur OpB
->
@@ -8213,8 +8361,21 @@ minus_real_ineqs(Type,A,B,C) :-
; geq_real_ineq(Type,A,B))
; true)),
minus_minus_add_real_ineqs(Type,A,B,C),
- ndelta:allow_delta_check.
-minus_real_ineqs(Type,A,B,C).
+ ndelta:allow_delta_check,
+ ((Type == real,
+ not_zero(C))
+ ->
+ check_exists_lin_expr_giving_diff_args(real,C,0.0,_Stop)
+ ; true),
+ bin_op_real_ineq(Type,minus_real1,A,B,C).
+%minus_real_ineqs(Type,A,B,C).
+minus_real_ineqs(Type,A,B,C) :-
+ ((Type == real,
+ not_zero(C))
+ ->
+ check_exists_lin_expr_giving_diff_args(real,C,0.0,_Stop)
+ ; true),
+ bin_op_real_ineq(Type,minus_real1,A,B,C).
minus_minus_add_real_ineqs(Type,A,B,C) :-
% On regarde les minus/add ayant une variable commune
@@ -9554,22 +9715,22 @@ mult_real_bis(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
check_launch_mult_int(_,A,B,C,Continue,_) :-
- var(Continue),
- !.
+ var(Continue),
+ !.
check_launch_mult_int(Type,A,B,C,_,Continue) :-
- ((term_variables((A,B,C),[_,_|_]),
- is_float_int_number(A),
- is_float_int_number(B),
- is_float_int_number(C),
- is_inside_mantissa(Type,A),
- is_inside_mantissa(Type,B),
- is_inside_mantissa(Type,C))
- ->
- cast_real_int(Type,A,IA),
- cast_real_int(Type,B,IB),
- cast_real_int(Type,C,IC),
- mult(IA,IB,IC)
- ; Continue = 1).
+ ((term_variables((A,B,C),[_,_|_]),
+ is_float_int_number(A),
+ is_float_int_number(B),
+ is_float_int_number(C),
+ is_inside_mantissa(Type,A),
+ is_inside_mantissa(Type,B),
+ is_inside_mantissa(Type,C))
+ ->
+ cast_real_int(Type,A,IA),
+ cast_real_int(Type,B,IB),
+ cast_real_int(Type,C,IC),
+ mult(IA,IB,IC)
+ ; Continue = 1).
@@ -9633,10 +9794,44 @@ diff_real_value(Var,Val) :-
; true))).
-
+get_sign_real(A,SA) :-
+ mreal:mindomain(A,MinA),
+ mreal:maxdomain(A,MaxA),
+ (MinA >= 0.0 ->
+ % donc 0 est pos
+ SA = pos
+ ; MaxA =< 0.0,
+ SA = neg).
+
%% On force le signe d'un argument
%% quand on connait le signe des deux autres
%% A * B = C
+mult_real_sign(real,A,B,C) :- !,
+ ((A == 0.0;
+ B == 0.0)
+ ->
+ protected_unify(C,0.0)
+ ; (C == 0.0 ->
+ (not_zero(A) ->
+ protected_unify(B,0.0)
+ ; (not_zero(B) ->
+ protected_unify(A,0.0)
+ ; Continue = 1))
+ ; Continue = 1)),
+ (var(Continue) ->
+ true
+ ; (get_sign_real(A,SA) ->
+ (get_sign_real(B,SB) ->
+ prod_sign(SA,SB,SC),
+ set_sign(real,C,SC)
+ ; (get_sign_real(C,SC) ->
+ prod_sign(SA,SC,SB),
+ set_sign(real,B,SB)
+ ; true))
+ ; (get_sign_real(C,SC) ->
+ prod_sign(SB,SC,SA),
+ set_sign(real,A,SA)
+ ; true))).
mult_real_sign(Type,A,B,C) :-
(get_sign(A,SA) ->
(get_sign(B,SB) ->
@@ -9668,16 +9863,69 @@ mult_real_ineqs(Type,A,B,C) :-
(get_sign(B,SB),!;true),
!,
ndelta:disable_delta_check,
- ((nonvar(SA),
- nonvar(SB))
+ (Type == real ->
+ mult_real_int_ineqs(SA,SB,A,B,C)
+ ; ((nonvar(SA),
+ nonvar(SB))
+ ->
+ prod_real_ineqs_type(Type,A,SA,B,SB,C)
+ ; true)),
+ prod_real_ineqs_from_res(Type,A,SA,B,SB,C),
+ ndelta:allow_delta_check,
+ ((fail,Type == real,
+ not_zero(C))
->
- prod_real_ineqs_type(Type,A,SA,B,SB,C)
+ check_exists_lin_expr_giving_diff_args(real,C,0.0,_Stop)
; true),
- prod_real_ineqs_from_res(Type,A,SA,B,SB,C),
- ndelta:allow_delta_check.
-mult_real_ineqs(Type,A,B,C).
+ bin_op_real_ineq(Type,mult_real1,A,B,C).
+%mult_real_ineqs(Type,A,B,C).
+mult_real_ineqs(Type,A,B,C) :-
+ ((fail,Type == real,
+ not_zero(C))
+ ->
+ check_exists_lin_expr_giving_diff_args(real,C,0.0,_Stop)
+ ; true),
+ 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) :-
+ 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)),
+ (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).
+
op_rel(<,>).
op_rel(>,<).
op_rel(=<,>=).
@@ -9881,11 +10129,7 @@ launch_mult_mult_real_ineqs(Type,Exact,Susp,D,SD,NZD,AA,BB,C,Z) :-
->
NRel = Rel
; op_rel(Rel,NRel)),
- launch_real_ineq(NRel,Type,AA,BB),
- (NRel == = ->
- % donc Susp inutile
- true %kill_suspension(Susp)
- ; true)
+ launch_real_ineq(NRel,Type,AA,BB)
; true),
get_rel_between_real_args(AA,BB,RelAB),
((RelAB \== NRel,
@@ -9901,11 +10145,7 @@ launch_mult_mult_real_ineqs(Type,Exact,Susp,D,SD,NZD,AA,BB,C,Z) :-
weak_rel(RelAB1,NRelAB)
; NRelAB = RelAB1))
->
- launch_real_ineq(NRelAB,Type,C,Z),
- (NRelAB == = ->
- % donc Susp inutile
- true %kill_suspension(Susp)
- ; true)
+ launch_real_ineq(NRelAB,Type,C,Z)
; true).
launch_mult_div_real_ineqs(Type,Exact,Susp,AA,BB,SBB,X,Z,C) :-
@@ -9946,11 +10186,7 @@ launch_mult_div_real_ineqs(Type,Exact,Susp,AA,BB,SBB,X,Z,C) :-
(var(Exact1) ->
weak_rel(RelAZ1,NRelAZ)
; NRelAZ = RelAZ1),
- launch_real_ineq(NRelAZ,Type,C,X),
- (NRelAZ == = ->
- % donc AllExact et inversible, Susp inutile
- true %kill_suspension(Susp)
- ; true)
+ launch_real_ineq(NRelAZ,Type,C,X)
; true).
@@ -10011,29 +10247,38 @@ launch_delta_mult_real_pos_pos(Type,A,B,C) :-
LD is min([LD1,HD1]),
HD is max([LD1,HD1]),
launch_delta(B,C,+,LD..HD))
- ; (LA >= 1.0 ->
- ((LA == 1.0;
- LB == LC; % 0
- HB == HC) % inf
- ->
- RelBC = '=<'
- ; RelBC = <)
- ; % LA < 1.0
- (HA =< 1.0 ->
- ((HA == 1.0;
- LB == LC;
- HB == HC)
+ ; ((Type == real,
+ is_float_int_number(A),
+ is_float_int_number(B))
+ ->
+ (LA >= 1.0 ->
+ (LA == 1.0 ->
+ RelBC = '=<'
+ ; RelBC = <)
+ ; (HA =< 1.0 ->
+ (HA == 1.0 ->
+ RelBC = '>='
+ ; RelBC = >)
+ ; true))
+ ; (LA >= 1.0 ->
+ ((LA == 1.0;
+ LB == LC; % 0
+ HB == HC) % inf
->
- RelBC = '>='
- ; RelBC = >)
- ; true)),
+ RelBC = '=<'
+ ; RelBC = <)
+ ; % LA < 1.0
+ (HA =< 1.0 ->
+ ((HA == 1.0;
+ LB == LC;
+ HB == HC)
+ ->
+ RelBC = '>='
+ ; RelBC = >)
+ ; true))),
(var(RelBC) ->
true
; launch_real_ineq(RelBC,Type,B,C))).
-/*
- ; launch_delta_mult_real_pos_pos0(Type,LA,HA,LB,HB,LC,HC,LdBC,HdBC),
- launch_delta(B,C,+,LdBC..HdBC)).
-*/
launch_delta_mult_real_pos_pos(Type,A,B,C).
launch_delta_mult_real_pos_pos0(Type,LA,HA,LB,HB,LC,HC,LdBC,HdBC) :-
@@ -10140,20 +10385,6 @@ launch_delta_mult_real_pos_neg(Type,A,B,C) :-
(nonvar(RelBC) ->
launch_real_ineq(RelBC,Type,B,C)
; true).
-/*
- mreal:dvar_range(B,LB,HB),
- mreal:dvar_range(C,LC,HC),
- mreal:dvar_range(A,LA,HA),
- norm_zero_op(Type,LB,OpLB),
- norm_zero_op(Type,HB,OpHB),
- norm_zero_op(Type,LC,OpLC),
- norm_zero_op(Type,HC,OpHC),
- launch_delta_mult_real_pos_pos0(Type,LA,HA,OpHB,OpLB,OpHC,OpLC,
- OpHdBC,OpLdBC),
- norm_zero_op(Type,OpLdBC,LdBC),
- norm_zero_op(Type,OpHdBC,HdBC),
- launch_delta(B,C,+,LdBC..HdBC).
-*/
launch_delta_mult_real_pos_neg(Type,A,B,C).
@@ -10207,7 +10438,7 @@ get_distance_between(Type,A,B,D) :-
%% Identites communes real/float
mult_real_2_args_equal(Type,A,A,C,Continue) ?- !,
- square_real1(Type,A,C).
+ square_real1(Type,A,C).
%% Identites du mode reel
mult_real_2_args_equal(real,X,Y,Z,Continue) :-
(X == Z ->
@@ -10228,95 +10459,95 @@ mult_real_2_args_equal(real,X,Y,Z,Continue) :-
%% Identites du mode double/simple nearest
mult_real_2_args_equal(Type,X,Y,Z,Continue) :-
- Type \== real,
+ Type \== real,
(X == Z, var(X),X=A,Y=B; %% X * Y = X
- Y == Z, var(Y),X=B,Y=A),%% X * Y = Y
- !,
- % A * B = A
- (not_zero(A) ->
+ Y == Z, var(Y),X=B,Y=A),%% X * Y = Y
+ !,
+ % A * B = A
+ (not_zero(A) ->
% A <> 0.0 donc B > 0.0
get_float_epsilon(Type,Eps),
mreal:dvar_remove_smaller(B,Eps)
- ; true),
+ ; true),
(not_inf_bounds(A) ->
- mreal:dvar_range(A,MinA,MaxA),
- get_first_normal_div_mult(Type,DN),
- ((B == 1.0;
- MinA > DN;
- MaxA < -DN)
- ->
- % Si A hors de [-2^-1022 .. 2^-1022] alors A <> 0.0 donc B = 1.0
- protected_unify(B = 1.0)
- ; % A s'intersecte avec [-2^-1022 .. 2^-1022]
- mreal:get_intervals(B,IB),
- interval_range(IB,MinB,MaxB),
- ((MinB >= 1.5;
- MaxB =< 0.5)
- ->
- % Si B hors de ]0.5 .. 1.5[ alors B <> 1.0 donc A = 0.0
- protected_unify(A = 0.0)
- ; % A intersecte avec [-2^-1022 .. 2^-1022] et B avec ]0.5 .. 1.5[
- (not_zero(A) ->
- % A <> 0.0 donc B > 0.0 et dans ]0.5 .. 1.5[
- get_next_float(Type,0.5,NMinB),
- get_previous_float(Type,1.5,NMaxB),
- mreal:set_typed_intervals(B,Type,[NMinB..NMaxB]),
- (not_unify(B,1.0) ->
- Bdiff1 = 1,
- % B <> 1.0 et dans ]0.5 .. 1.5[
- % Si A est integral et B <> 0.0|1.0 alors fail (A=0.0)
- % Si B est integral et B <> 1.0 alors fail (B :: ]0.5 .. 1.5[)
- get_float_int_status(A,0),
- get_float_int_status(B,0),
- % Si B <> 0.0 et B <> 1.0 alors A :: -2^-1022 .. 2^-1022
- OpDN is -DN,
- mreal:set_typed_intervals(A,Type,[OpDN..DN])
- ; true)
- ; (number_in_interval(IB,1.0) ->
- true
- ; % Si A ou B est integral et B <> 1.0 alors A = 0.0
- ((get_float_int_status(A,1);
+ mreal:dvar_range(A,MinA,MaxA),
+ get_first_normal_div_mult(Type,DN),
+ ((B == 1.0;
+ MinA > DN;
+ MaxA < -DN)
+ ->
+ % Si A hors de [-2^-1022 .. 2^-1022] alors A <> 0.0 donc B = 1.0
+ protected_unify(B = 1.0)
+ ; % A s'intersecte avec [-2^-1022 .. 2^-1022]
+ mreal:get_intervals(B,IB),
+ interval_range(IB,MinB,MaxB),
+ ((MinB >= 1.5;
+ MaxB =< 0.5)
+ ->
+ % Si B hors de ]0.5 .. 1.5[ alors B <> 1.0 donc A = 0.0
+ protected_unify(A = 0.0)
+ ; % A intersecte avec [-2^-1022 .. 2^-1022] et B avec ]0.5 .. 1.5[
+ (not_zero(A) ->
+ % A <> 0.0 donc B > 0.0 et dans ]0.5 .. 1.5[
+ get_next_float(Type,0.5,NMinB),
+ get_previous_float(Type,1.5,NMaxB),
+ mreal:set_typed_intervals(B,Type,[NMinB..NMaxB]),
+ (not_unify(B,1.0) ->
+ Bdiff1 = 1,
+ % B <> 1.0 et dans ]0.5 .. 1.5[
+ % Si A est integral et B <> 0.0|1.0 alors fail (A=0.0)
+ % Si B est integral et B <> 1.0 alors fail (B :: ]0.5 .. 1.5[)
+ get_float_int_status(A,0),
+ get_float_int_status(B,0),
+ % Si B <> 0.0 et B <> 1.0 alors A :: -2^-1022 .. 2^-1022
+ OpDN is -DN,
+ mreal:set_typed_intervals(A,Type,[OpDN..DN])
+ ; true)
+ ; (number_in_interval(IB,1.0) ->
+ true
+ ; % Si A ou B est integral et B <> 1.0 alors A = 0.0
+ ((get_float_int_status(A,1);
get_float_int_status(B,1))
- ->
- mreal:set_typed_intervals(A,Type,[-0.0 .. 0.0])
- ; Bdiff1 = 1,
- OpDN is -DN,
- mreal:set_typed_intervals(A,Type,[OpDN..DN])))),
- (is_fzero(A) ->
- (float(A) ->
+ ->
+ mreal:set_typed_intervals(A,Type,[-0.0 .. 0.0])
+ ; Bdiff1 = 1,
+ OpDN is -DN,
+ mreal:set_typed_intervals(A,Type,[OpDN..DN])))),
+ (is_fzero(A) ->
+ (float(A) ->
true
; Continue = 1)
- ; (nonvar(Bdiff1) ->
- % Ici pas de float_int possible pour A et B
- mreal:dvar_domain(A,DomA),
- mreal:dvar_domain(B,DomB),
- reduce_dom_inv_mult_eq_args(Type,0,0,=,?,DomA,DomB,DomA,NDomA,_,_),
- mreal:dvar_set(A,NDomA),
- (number(B) ->
- %% On est en forme resolue
- true
- ; Continue = 1)
- ; Continue = 1))))
- ; Continue = 1).
+ ; (nonvar(Bdiff1) ->
+ % Ici pas de float_int possible pour A et B
+ mreal:dvar_domain(A,DomA),
+ mreal:dvar_domain(B,DomB),
+ reduce_dom_inv_mult_eq_args(Type,0,0,=,?,DomA,DomB,DomA,NDomA,_,_),
+ mreal:dvar_set(A,NDomA),
+ (number(B) ->
+ % On est en forme resolue
+ true
+ ; Continue = 1)
+ ; Continue = 1))))
+ ; Continue = 1).
%% Simplifications communes avec un "op_real"
mult_real_2_args_equal(Type,A,B,C,Continue) :-
- get_saved_cstr_suspensions(LSusp),
- member((Susp,op_real1(Type,X,Y)),LSusp),
- ( A == X,
- (B == Y, Goal = (square_real(Type,A,OpC),op_real(Type,OpC,C)); %% A * -A = C
- C == Y, Goal = mult_real_op_arg_res(Type,A,B,C,Continue)) %% A * B = -A, ie A * -B = A
- ; A == Y,
- (B == X, Goal = (square_real(Type,A,OpC),op_real(Type,OpC,C)); %% -B * B = C
- C == X, Goal = mult_real_op_arg_res(Type,A,B,C,Continue)) %% -C * B = C, ie C * -B = C
- ; B == X,
- (A == Y, Goal = (square_real(Type,A,OpC),op_real(Type,OpC,C)); %% -B * B = C
- C == Y, Goal = mult_real_op_arg_res(Type,B,A,C,Continue)) %% A * B = -B, ie B * -A = B
- ; B == Y,
- (A == X, Goal = (square_real(Type,A,OpC),op_real(Type,OpC,C)); %% A * -A = C
- C == X, Goal = mult_real_op_arg_res(Type,B,A,C,Continue))),%% A * -C = C, ie C * -A = C
- !,
- call_priority(Goal,2).
+ get_saved_cstr_suspensions(LSusp),
+ member((Susp,op_real1(Type,X,Y)),LSusp),
+ ( A == X,
+ (B == Y, Goal = (square_real(Type,A,OpC),op_real(Type,OpC,C)); %% A * -A = C
+ C == Y, Goal = mult_real_op_arg_res(Type,A,B,Continue)) %% A * B = -A, ie A * -B = A
+ ; A == Y,
+ (B == X, Goal = (square_real(Type,A,OpC),op_real(Type,OpC,C)); %% -B * B = C
+ C == X, Goal = mult_real_op_arg_res(Type,A,B,Continue)) %% -C * B = C, ie C * -B = C
+ ; B == X,
+ (A == Y, Goal = (square_real(Type,A,OpC),op_real(Type,OpC,C)); %% -B * B = C
+ C == Y, Goal = mult_real_op_arg_res(Type,B,A,Continue)) %% A * B = -B, ie B * -A = B
+ ; B == Y,
+ (A == X, Goal = (square_real(Type,A,OpC),op_real(Type,OpC,C)); %% A * -A = C
+ C == X, Goal = mult_real_op_arg_res(Type,B,A,Continue))),%% A * -C = C, ie C * -A = C
+ !,
+ call_priority(Goal,2).
mult_real_2_args_equal(_,_,_,_,1).
@@ -10336,7 +10567,7 @@ is_op_real(V,OpV) :-
((X,Y) == (V,OpV); (X,Y) == (OpV,V))).
%% A * B = -A
-mult_real_op_arg_res(Type,A,B,OpA,Continue) :-
+mult_real_op_arg_res(Type,A,B,Continue) :-
(Type == real ->
% A == 0.0 et/ou B == -1.0
(diff_real_value(A,0.0) ->
@@ -10347,50 +10578,6 @@ mult_real_op_arg_res(Type,A,B,OpA,Continue) :-
; % B change le signe de A donc B neg
mreal:dvar_remove_greater(B,-0.0),
Continue = 1).
-/*
-mult_real_op_arg_res(Type,A,B,OpA,Continue) :-
- ((Type == real;
- not_inf_bounds(A))
- ->
- (Type == real ->
- % A == 0.0 et/ou B == -1.0
- (diff_real_value(A,0.0) ->
- protected_unify(B = -1.0)
- ; (diff_real_value(B,-1.0) ->
- protected_unify(A = 0.0)
- ; Continue = 1))
- ; % A*B = OpA <==> A*OpB = A
- mreal:dvar_range(B,MinB,MaxB),
- ((MinB >= -0.5;
- MaxB =< -1.5)
- ->
- % Si B en dehors de ]-1.5 .. -0.5[ alors A == 0.0
- mreal:set_typed_intervals(A,Type,[-0.0..0.0]),
- (float(A) ->
- true
- ; Continue = 1)
- ; mreal:dvar_range(A,MinA,MaxA),
- get_first_normal_div_mult(Type,DN),
- ((MinA > DN;
- MaxA < -DN)
- ->
- % Si A en dehors de [-2^(-1022)..2^(-1022)] alors B == -1.0
- protected_unify(B = -1.0)
- ; ((not_zero(A);
- number(B);
- not_zero(B),
- not_unify(B,1.0))
- ->
- op_real(Type,B,OpB),
- mult_real(Type,A,OpB,A)
- ; % On pourrait propager un op_real(B,OpB) inutile
- Continue = 1))))
- ; (not_zero(A) ->
- % A <> 0.0 donc -B >= 0.0
- mreal:dvar_remove_greater(B,0.0)
- ; true),
- Continue = 1).
-*/
mult_real_inst(real,A,B,C,Continue) :- !,
@@ -10911,8 +11098,8 @@ inv_mult_real_dom(real,RelAB,FIA,FIB,FIC,DomA,DomB,DomC,NDomC) :- !,
mreal:dom_interval(DomB,InterB),
mreal:dom_interval(DomC,InterC),
((InterC = [F],float(F);
- occurs(-1.0Inf,(InterA,InterB));
- occurs(1.0Inf,(InterA,InterB)))
+ fail,occurs(-1.0Inf,(InterA,InterB));
+ fail,occurs(1.0Inf,(InterA,InterB)))
->
NDomC = DomC
; ((not (InterB = [B],
@@ -12612,12 +12799,16 @@ 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) :- !.
+% Bizarre !!
saturate_div_real_two(Type,A,B,C) :-
get_saved_cstr_suspensions(LSusp),
((B == 2.0,
member((S,add_real1(Type,X,Y,AA)),LSusp),
- AA == A,
+ var(X),
+ var(Y),
+ A == A,
get_rel_between_real_args(X,Y,RelXY),
RelXY \== ?,
(get_rel_between_real_args(X,C,RelC);
@@ -12715,83 +12906,95 @@ div_real_ineqs(Type,A,B,C) :-
mreal:dvar_range(C,MinC,MaxC),
(get_sign(A,SA),!;true),
(get_sign(B,SB),!;true),
- ((nonvar(SA),
- nonvar(SB))
- ->
- ((float(B),
- is_exact(Type,div,A,B),
- get_sign(C,SC))
- ->
- prod_real_ineqs_type(Type,C,SC,B,SB,A)
-/*
- InvB is 1.0/B,
- prod_real_ineqs_type(Type,A,SA,InvB,SB,C)
-*/
- ; div_real_ineqs_type(Type,A,SA,B,SB,C)),
- ((var(A),
- var(B))
+ (Type == real ->
+ div_real_int_ineqs(SA,SB,A,B,C)
+ ; ((nonvar(SA),
+ nonvar(SB))
->
- (MinC >= 1.0 ->
- % A et B de meme signe
- (MinC == 1.0 ->
- (SA == pos ->
- geq_real_ineq(Type,A,B)
- ; geq_real_ineq(Type,B,A))
- ; (SA == pos ->
- gt_real_ineq(Type,A,B)
- ; gt_real_ineq(Type,B,A)))
- ; ((MinC >= 0.0,
- MaxC =< 1.0)
- ->
- (MaxC == 1.0 ->
+ ((float(B),
+ is_exact(Type,div,A,B),
+ get_sign(C,SC))
+ ->
+ prod_real_ineqs_type(Type,C,SC,B,SB,A)
+ ; div_real_ineqs_type(Type,A,SA,B,SB,C)),
+ ((var(A),
+ var(B))
+ ->
+ (MinC >= 1.0 ->
+ % A et B de meme signe
+ (MinC == 1.0 ->
(SA == pos ->
- geq_real_ineq(Type,B,A)
- ; geq_real_ineq(Type,A,B))
+ geq_real_ineq(Type,A,B)
+ ; geq_real_ineq(Type,B,A))
; (SA == pos ->
- gt_real_ineq(Type,B,A)
- ; gt_real_ineq(Type,A,B)))
- ; (MaxC < -1.0 ->
- % on peut avoir une inegalite stricte
- % en introduisant un oppose
- (SB == pos ->
- % A < -B donc -A > B
- op_real(Type,A,OpA),
- gt_real_ineq(Type,OpA,B)
- ; % SB == neg et SA == pos
- % A > -B
- op_real(Type,B,OpB),
- gt_real_ineq(Type,A,OpB))
- ; true)))
- ; true)
- ; true),
- ((get_sign(C,SC),
- var(A),var(B),
- (SA,SB) \== (pos,pos),
- exists_mult_with_abs_op_B(SB,B))
- ->
- % si un cas de monotonie passe par une ingelité inversee
- % par exemple on a A/B Rel X mais le store contient B * OpX
- % ou bien OpB * OpX
- get_saved_cstr_suspensions(LSusp),
- abs_val_real(Type,A,AA),
- abs_val_real(Type,B,AB),
- setval(saved_suspensions,(1,LSusp)),
- get_cstr_suspensions(AA,LSuspV),
- ((member(SV,LSuspV),
- get_suspension_data(SV,goal,div_real1(Type,NA,NB,_)),
- AA == NA,
- AB == NB)
+ gt_real_ineq(Type,A,B)
+ ; gt_real_ineq(Type,B,A)))
+ ; ((MinC >= 0.0,
+ MaxC =< 1.0)
+ ->
+ (MaxC == 1.0 ->
+ (SA == pos ->
+ geq_real_ineq(Type,B,A)
+ ; geq_real_ineq(Type,A,B))
+ ; (SA == pos ->
+ gt_real_ineq(Type,B,A)
+ ; gt_real_ineq(Type,A,B)))
+ ; (MaxC < -1.0 ->
+ % on peut avoir une inegalite stricte
+ % en introduisant un oppose
+ (SB == pos ->
+ % A < -B donc -A > B
+ op_real(Type,A,OpA),
+ gt_real_ineq(Type,OpA,B)
+ ; % SB == neg et SA == pos
+ % A > -B
+ op_real(Type,B,OpB),
+ gt_real_ineq(Type,A,OpB))
+ ; true)))
+ ; true)
+ ; true),
+ ((get_sign(C,SC),
+ var(A),var(B),
+ (SA,SB) \== (pos,pos),
+ exists_mult_with_abs_op_B(SB,B))
->
- true
- ; call_priority(
- (abs_val_real(Type,C,AC),
- div_real(Type,AA,AB,AC)),
- 2))
- ; true),
- div_real_ineqs_from_cstrs(Type,A,SA,B,SB,C,MinC,MaxC),
- ndelta:allow_delta_check.
-div_real_ineqs(Type,A,B,C).
+ % si un cas de monotonie passe par une ingelité inversee
+ % par exemple on a A/B Rel X mais le store contient B * OpX
+ % ou bien OpB * OpX
+ get_saved_cstr_suspensions(LSusp),
+ abs_val_real(Type,A,AA),
+ abs_val_real(Type,B,AB),
+ setval(saved_suspensions,(1,LSusp)),
+ get_cstr_suspensions(AA,LSuspV),
+ ((member(SV,LSuspV),
+ get_suspension_data(SV,goal,div_real1(Type,NA,NB,_)),
+ AA == NA,
+ AB == NB)
+ ->
+ true
+ ; call_priority(
+ (abs_val_real(Type,C,AC),
+ div_real(Type,AA,AB,AC)),
+ 2))
+ ; true),
+ div_real_ineqs_from_cstrs(Type,A,SA,B,SB,C,MinC,MaxC)),
+ ndelta:allow_delta_check,
+ bin_op_real_ineq(Type,div_real1,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).
+div_real_int_ineqs(SA,SB,A,B,C) :-
+ var(A),
+ var(C),
+ nonvar(SA),
+ (nonvar(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(_,_,_,_,_).
exists_mult_with_abs_op_B(SB,B) :-
get_saved_cstr_suspensions(LSusp),
@@ -16008,8 +16211,8 @@ narrow_max_inv_pow(Type,Val,N,LMax,HMax,Num,Max) :-
%% B = A^2
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
square_real(A,B) :-
- getval(float_eval,Type)@eclipse,
- square_real_type(Type,A,B).
+ getval(float_eval,Type)@eclipse,
+ square_real_type(Type,A,B).
square_real_type(real,A,B) ?-
square_real(real,A,B).
@@ -16019,7 +16222,7 @@ square_real_type(Type,A,B) :-
; fp_power(as(A,Type),as(2,int)) $= as(B,Type)).
square_real(Type,A,B) :-
- ensure_not_NaN((A,B)),
+ ensure_not_NaN((A,B)),
(ground(A) ->
mult_real_inst(Type,A,A,B,_)
; set_lazy_domain(Type,A),
@@ -16031,9 +16234,9 @@ square_real(Type,A,B) :-
%% Premier projection et typage, utilise aussi en evaluation
square_real_interval(A,B) :-
- getval(float_eval,Type)@eclipse,
+ getval(float_eval,Type)@eclipse,
set_lazy_domain(Type,B),
- square_real_interval_type(Type,A,B).
+ square_real_interval_type(Type,A,B).
square_real_interval_type(real,A,B) ?- !,
square_real_interval(real,A,B).
@@ -16060,11 +16263,11 @@ square_real_interval(Type,A,B) :-
mreal:set_typed_intervals(B,Type,BInter)).
square_real1(Type,A,B) :-
- get_priority(Prio),
- set_priority(1),
- square_real_bis(Type,A,B),
- set_priority(Prio),
- wake_if_other_scheduled(Prio).
+ get_priority(Prio),
+ set_priority(1),
+ square_real_bis(Type,A,B),
+ set_priority(Prio),
+ wake_if_other_scheduled(Prio).
square_real_bis(Type,Val1,Val) :-
@@ -16095,17 +16298,17 @@ square_real_bis(Type,Val1,Val) :-
%% Val^2 = Val
square_real_2_args_equal(Type,Val,Val,_) ?- !,
- mreal:set_typed_intervals(Val,Type,[0.0,1.0,1.0Inf]).
+ mreal:set_typed_intervals(Val,Type,[0.0,1.0,1.0Inf]).
%% Val^2 = -Val
square_real_2_args_equal(Type,Val1,Val,Continue) :-
- get_saved_cstr_suspensions(LSusp),
- ((member((Susp,op_real1(Type,X,Y)),LSusp),
- (X == Val1, Y == Val;
- X == Val, Y == Val1))
- ->
- mreal:set_typed_intervals(Val1,Type,[-1.0Inf,-1.0,0.0]),
- mreal:set_typed_intervals(Val,Type,[0.0,1.0,1.0Inf])
- ; Continue = 1).
+ get_saved_cstr_suspensions(LSusp),
+ ((member((Susp,op_real1(Type,X,Y)),LSusp),
+ (X == Val1, Y == Val;
+ X == Val, Y == Val1))
+ ->
+ mreal:set_typed_intervals(Val1,Type,[-1.0Inf,-1.0,0.0]),
+ mreal:set_typed_intervals(Val,Type,[0.0,1.0,1.0Inf])
+ ; Continue = 1).
%% PMO propagation du statut float_int pour l'operation unaire square
@@ -16119,64 +16322,64 @@ square_real_2_args_equal(Type,Val1,Val,Continue) :-
%% arguments (propagate_float_int_square(Type,B,A)) car la propagation est
%% alors inversee
propagate_float_int_square(Type,A,B) :-
- ((is_float_int_number(A),
- (Type \== real;
- is_inside_mantissa(Type,B)))
- ->
- launch_float_int_number(B)
- ; ((is_float_int_number(B),
- mreal:mindomain(B,MinB),
- get_mantissa_size(Type,MSize),
- MinRepSquare is 2.0^(2*MSize),%% 2.0^104 en double
- MinB >= MinRepSquare)
- ->
- launch_float_int_number(A)
- ; true)).
+ ((is_float_int_number(A),
+ (Type \== real;
+ is_inside_mantissa(Type,B)))
+ ->
+ launch_float_int_number(B)
+ ; ((is_float_int_number(B),
+ mreal:mindomain(B,MinB),
+ get_mantissa_size(Type,MSize),
+ MinRepSquare is 2.0^(2*MSize),%% 2.0^104 en double
+ MinB >= MinRepSquare)
+ ->
+ launch_float_int_number(A)
+ ; true)).
%% PMO si les 2 args sont des float_int entre -2^53 et 2^53 on peut
%% deleguer le calcul de square_real aux entiers
check_launch_square_int(_,A,B,Continue,_) :-
- var(Continue),
- !.
+ var(Continue),
+ !.
check_launch_square_int(Type,A,B,_,Continue) :-
- ((term_variables((A,B),[_,_]),
- is_float_int_number(A),
- is_float_int_number(B),
- is_inside_mantissa(Type,A),
+ ((term_variables((A,B),[_,_]),
+ is_float_int_number(A),
+ is_float_int_number(B),
+ is_inside_mantissa(Type,A),
is_inside_mantissa(Type,B))
- ->
- cast_real_int(Type,A,IA),
- square(IA,IB),
- cast_real_int(Type,B,IB)
- ; Continue = 1).
+ ->
+ cast_real_int(Type,A,IA),
+ square(IA,IB),
+ cast_real_int(Type,B,IB)
+ ; Continue = 1).
square_real_rec(Type,Val1,Val) :-
- mreal:dvar_domain(Val1,Dom1),
- mreal:dvar_domain(Val,Dom),
- square_real_rec(Type,Val1,Val,Dom1,Dom).
+ mreal:dvar_domain(Val1,Dom1),
+ mreal:dvar_domain(Val,Dom),
+ square_real_rec(Type,Val1,Val,Dom1,Dom).
square_real_rec(Type,Val1,Val,Dom1,Dom) :-
- %% Val = Val1^2
- mreal:dom_interval(Dom1,LInter1),
- sqr_interval_list_real(Type,LInter1,SqrLInter1),
- mreal:list_to_typed_dom(Type,SqrLInter1,SqrDom1),
- mreal:dom_intersection(Dom,SqrDom1,NDom,_),
- mreal:dvar_set(Val,NDom),
- %% PMO dvar_set reduit l'intervalle NLInter0 si float_int
- %% Val1 = sqrt(Val)
- mreal:dvar_domain(Val,NewDom),%% PMO nouveau domaine de Val
- mreal:dom_interval(NewDom,NLInter),
- inv_sqr_interval_list_real(Type,NLInter,SqrtLInter),
- mreal:list_to_typed_dom(Type,SqrtLInter,SqrtDom),
- mreal:dom_intersection(Dom1,SqrtDom,NDom1,_),
- mreal:dvar_set(Val1,NDom1),
- mreal:dvar_domain(Val1,NewDom1),
- % = necessaire
- (NewDom1 = Dom1 ->
- %% On a fini
- true
- ; square_real_rec(Type,Val1,Val,NewDom1,NewDom)).
+ % Val = Val1^2
+ mreal:dom_interval(Dom1,LInter1),
+ sqr_interval_list_real(Type,LInter1,SqrLInter1),
+ mreal:list_to_typed_dom(Type,SqrLInter1,SqrDom1),
+ mreal:dom_intersection(Dom,SqrDom1,NDom,_),
+ mreal:dvar_set(Val,NDom),
+ % PMO dvar_set reduit l'intervalle NLInter0 si float_int
+ % Val1 = sqrt(Val)
+ mreal:dvar_domain(Val,NewDom),%% PMO nouveau domaine de Val
+ mreal:dom_interval(NewDom,NLInter),
+ inv_sqr_interval_list_real(Type,NLInter,SqrtLInter),
+ mreal:list_to_typed_dom(Type,SqrtLInter,SqrtDom),
+ mreal:dom_intersection(Dom1,SqrtDom,NDom1,_),
+ mreal:dvar_set(Val1,NDom1),
+ mreal:dvar_domain(Val1,NewDom1),
+ % = necessaire
+ (NewDom1 = Dom1 ->
+ % On a fini
+ true
+ ; square_real_rec(Type,Val1,Val,NewDom1,NewDom)).
narrow_min_sqrt_real(Res,Min) :-
min_sqrt_real(Res,Min0),
@@ -16214,36 +16417,36 @@ square_real_inst(real,Val1,Val,Continue) :- !,
Rat is Rat1*Rat1,
launch_box_rat(Val,Rat),
check_rbox_cstrs(2,square_real1(real,Val1,Val))
- ; (number(Val) ->
- narrow_min_sqrt_real(Val,Min),
- narrow_max_sqrt_real(Val,Max),
- (Min == Max ->
- norm_zero_op(real,Min,OpMin),
- mreal:set_typed_intervals(Val1,real,[OpMin,Min])
- ; mreal:mindomain(Val1,Min1),
- op_real_intervals(Type,[Min..Max],Min1,[Min..Max],LInter),
- mreal:set_typed_intervals(Val1,real,LInter),
- (float(Val1) ->
- true
- ; (get_sign(Val1,Sign) ->
- % Val1 est signe et non reductible
- launch_box(Val1),
+ ; (number(Val) ->
+ narrow_min_sqrt_real(Val,Min),
+ narrow_max_sqrt_real(Val,Max),
+ (Min == Max ->
+ norm_zero_op(real,Min,OpMin),
+ mreal:set_typed_intervals(Val1,real,[OpMin,Min])
+ ; mreal:mindomain(Val1,Min1),
+ op_real_intervals(Type,[Min..Max],Min1,[Min..Max],LInter),
+ mreal:set_typed_intervals(Val1,real,LInter),
+ (float(Val1) ->
+ true
+ ; (get_sign(Val1,Sign) ->
+ % Val1 est signe et non reductible
+ launch_box(Val1),
check_rbox_cstrs(2,inv_square_real1(Sign,Val,Val1))
- ; Continue = 1)))
- ; (is_real_box(Val1) ->
- get_dvar_fintervals(Val1,[I1]),
- mult_real_float_intervals(real,I1,I1,LInter,[]),
- mreal:set_typed_intervals(Val,real,LInter),
- (float(Val) ->
- %% Val1 est signe et non reductible
+ ; Continue = 1)))
+ ; (is_real_box(Val1) ->
+ get_dvar_fintervals(Val1,[I1]),
+ mult_real_float_intervals(real,I1,I1,LInter,[]),
+ mreal:set_typed_intervals(Val,real,LInter),
+ (float(Val) ->
+ % Val1 est signe et non reductible
get_sign(Val1,Sign),
check_rbox_cstrs(2,inv_square_real1(Sign,Val,Val1))
- ; Continue = 1,
+ ; Continue = 1,
(is_reduced_real(Val) ->
- %% Val1 et Val non reductibles
- launch_box(Val)
- ; true))
- ; Continue = 1))).
+ % Val1 et Val non reductibles
+ launch_box(Val)
+ ; true))
+ ; Continue = 1))).
%% Mode double
square_real_inst(Type,Val1,Val,Continue) :-
(number(Val1) ->
@@ -16294,11 +16497,11 @@ check_exists_square_real(real,A,A2) ?- !,
call(Call)
; true).
check_exists_square_real(Type,A,B) :-
- ((var(A),
+ ((var(A),
min_normalized(Type,MinNorm),
mreal:dvar_range(B,MinB,_),
- get_saved_cstr_suspensions(LSusp),
- member((Susp,Goal),LSusp),
+ get_saved_cstr_suspensions(LSusp),
+ member((Susp,Goal),LSusp),
(Goal = square_real1(Type,X,Y),
X == A;
Goal = sqrt_real1(Type,X,SqrtX),
@@ -16308,8 +16511,8 @@ check_exists_square_real(Type,A,B) :-
; get_rel_between_real_args(SqrtX,A,Rel),
occurs(Rel,(<,>,#)),
PropX2 = 2)))
- ->
- (var(PropX2) ->
+ ->
+ (var(PropX2) ->
kill_suspension(Susp),
protected_unify(B = Y)
; % sqrt(A^2) = abs(A) si A^2 normalise
@@ -16319,7 +16522,7 @@ check_exists_square_real(Type,A,B) :-
; % contraposee
get_previous_float(Type,MinNorm,PMinNorm),
mreal:dvar_remove_greater(B,PMinNorm)))
- ; true).
+ ; true).
check_before_susp_square_real(Type,Val1,Val) :-
@@ -16329,7 +16532,6 @@ check_before_susp_square_real(Type,Val1,Val) :-
; get_rel_between_real_args(Val1,Val,ORel),
square_real_ineqs(Type,Val1,Val),
notify_ineq_to_real_cstrs_if_new_rel(ORel,Val1,Val),
-
my_suspend(square_real1(Type,Val1,Val),4,(Val1,Val)->suspend:constrained)).
@@ -16389,192 +16591,193 @@ square_real_ineqs(Type,X,X2) :-
%% Mode reel
square_real_ineqs1(real,A,B) :- !,
- %% B positif
- mreal:dvar_range(A,MinA,MaxA),
- (MinA >= 0.0 ->
- %% A positif
- (MaxA =< 1.0 ->
- %% decroissant entre 0.0 et 1.0
- ((MaxA < 1.0,
- not_zero(A))
- ->
- %% d�croissance stricte
- gt_real_ineq(real,A,B)
- ; geq_real_ineq(real,A,B))
- ; (MinA >= 1.0 ->
- %% croissant au dessus de 1.0
- (MinA > 1.0 ->
- %% croissance stricte
- gt_real_ineq(real,B,A)
- ; geq_real_ineq(real,B,A))
- ; true))
- ; (MaxA =< 0.0 ->
- %% A negatif, croissance
- (not_zero(A) ->
- %% croissance stricte
- gt_real_ineq(real,B,A)
- ; geq_real_ineq(real,B,A))
- ; %% A autour de zero
- mreal:mindomain(B,MinB),
- (MinB >= 1.0 ->
- %% B au dessus de 1.0, croissance
- (MinB > 1.0 ->
- %% croissance stricte
- gt_real_ineq(real,B,A)
- ; geq_real_ineq(real,B,A))
- ; true))).
+ % B positif
+ mreal:dvar_range(A,MinA,MaxA),
+ (MinA >= 0.0 ->
+ % A positif
+ (MaxA =< 1.0 ->
+ % decroissant entre 0.0 et 1.0
+ ((MaxA < 1.0,
+ not_zero(A))
+ ->
+ % d�croissance stricte
+ gt_real_ineq(real,A,B)
+ ; geq_real_ineq(real,A,B))
+ ; (MinA >= 1.0 ->
+ % croissant au dessus de 1.0
+ (MinA > 1.0 ->
+ % croissance stricte
+ gt_real_ineq(real,B,A)
+ ; geq_real_ineq(real,B,A))
+ ; true))
+ ; (MaxA =< 0.0 ->
+ % A negatif, croissance
+ (not_zero(A) ->
+ % croissance stricte
+ gt_real_ineq(real,B,A)
+ ; geq_real_ineq(real,B,A))
+ ; % A autour de zero
+ mreal:mindomain(B,MinB),
+ (MinB >= 1.0 ->
+ % B au dessus de 1.0, croissance
+ (MinB > 1.0 ->
+ % croissance stricte
+ gt_real_ineq(real,B,A)
+ ; geq_real_ineq(real,B,A))
+ ; true))).
%% Mode double/simple
square_real_ineqs1(Type,Val1,Val) :-
- mreal:dvar_range(Val1,Min1,Max1),
- (Max1 =< 0.0 ->
- %% Val1 neg et Val pos
- geq_real_ineq(Type,Val,Val1)
- ; (Min1 >= 1.0 ->
- %% square croissant sur 1.0 +oo
- geq_real_ineq(Type,Val,Val1)
- ; ((Min1 >= 0.0,
- Max1 < 1.0)
- ->
- %% square decroissant entre 0.0 et 1.0
- geq_real_ineq(Type,Val1,Val)
- ; mreal:mindomain(Val,Min),
- (Min >= 1.0 ->
- %% Val1 ne contient pas 0.0 .. 1.0-eps
- geq_real_ineq(Type,Val,Val1)
- ; true)))).
+ mreal:dvar_range(Val1,Min1,Max1),
+ (Max1 =< 0.0 ->
+ % Val1 neg et Val pos
+ geq_real_ineq(Type,Val,Val1)
+ ; (Min1 >= 1.0 ->
+ % square croissant sur 1.0 +oo
+ geq_real_ineq(Type,Val,Val1)
+ ; ((Min1 >= 0.0,
+ Max1 < 1.0)
+ ->
+ % square decroissant entre 0.0 et 1.0
+ geq_real_ineq(Type,Val1,Val)
+ ; mreal:mindomain(Val,Min),
+ (Min >= 1.0 ->
+ % Val1 ne contient pas 0.0 .. 1.0-eps
+ geq_real_ineq(Type,Val,Val1)
+ ; true)))).
inv_sqr_interval_list_real(real,LInter,Res) :- !,
- sqrt_interval_list_real(LInter,Res).
+ sqrt_interval_list_real(LInter,Res).
inv_sqr_interval_list_real(Type,LInter,Res) :-
- inv_sqr_interval_list_float(Type,LInter,Res).
+ inv_sqr_interval_list_float(Type,LInter,Res).
%% mode real
sqrt_interval_list_real([],[]).
sqrt_interval_list_real([Inter|LInter],Res) :-
- sqrt_interval_real(Inter,L,H),
- interval_from_bounds(L,H,IP),
- (L =< H ->
- (number(IP) ->
- norm_zero_op(real,IP,IN)
- ; norm_zero_op(real,L,OpL),
- norm_zero_op(real,H,OpH),
- interval_from_bounds(OpH,OpL,IN)),
- Res = [IN,IP|NRes]
- ; Res = NRes),
- sqrt_interval_list_real(LInter,NRes).
-
- sqrt_interval_real(Inter,L,H) :-
- min_max_inter(Inter,Min,Max),
-%% getval(floating_biblio,F)@eclipse,
- F = 1,
- sqrt_double_float(Min,1,F,_,L),
- sqrt_double_float(Max,2,F,_,H).
-
- min_sqrt_real(V,SV) :-
-%% getval(floating_biblio,F)@eclipse,
- F = 1,
- sqrt_double_float(V,1,F,_Err,SV).
- max_sqrt_real(V,SV) :-
-%% getval(floating_biblio,F)@eclipse,
- F = 1,
- sqrt_double_float(V,2,F,_Err,SV).
+ sqrt_interval_real(Inter,L,H),
+ interval_from_bounds(L,H,IP),
+ (L =< H ->
+ (number(IP) ->
+ norm_zero_op(real,IP,IN)
+ ; norm_zero_op(real,L,OpL),
+ norm_zero_op(real,H,OpH),
+ interval_from_bounds(OpH,OpL,IN)),
+ Res = [IN,IP|NRes]
+ ; Res = NRes),
+ sqrt_interval_list_real(LInter,NRes).
+
+sqrt_interval_real(Inter,L,H) :-
+ min_max_inter(Inter,Min,Max),
+ % getval(floating_biblio,F)@eclipse,
+ F = 1,
+ sqrt_double_float(Min,1,F,_,L),
+ sqrt_double_float(Max,2,F,_,H).
+
+min_sqrt_real(V,SV) :-
+ % getval(floating_biblio,F)@eclipse,
+ F = 1,
+ sqrt_double_float(V,1,F,_Err,SV).
+
+max_sqrt_real(V,SV) :-
+ % getval(floating_biblio,F)@eclipse,
+ F = 1,
+ sqrt_double_float(V,2,F,_Err,SV).
%% mode float
inv_sqr_interval_list_float(_,[],[]).
inv_sqr_interval_list_float(Type,[Inter|LInter],Res) :-
- min_max_inter(Inter,Min,Max),
- min_inv_sqr_float_nearest(Type,Min,L),
- max_inv_sqr_float_nearest(Type,Max,H),
- (L =< H ->
- interval_from_bounds(L,H,IP),
- (number(IP) ->
- norm_zero_op(Type,IP,IN)
- ; norm_zero_op(Type,L,OpL),
- norm_zero_op(Type,H,OpH),
- interval_from_bounds(OpH,OpL,IN)),
- Res = [IN,IP|NRes]
- ; Res = NRes),
- inv_sqr_interval_list_float(Type,LInter,NRes).
+ min_max_inter(Inter,Min,Max),
+ min_inv_sqr_float_nearest(Type,Min,L),
+ max_inv_sqr_float_nearest(Type,Max,H),
+ (L =< H ->
+ interval_from_bounds(L,H,IP),
+ (number(IP) ->
+ norm_zero_op(Type,IP,IN)
+ ; norm_zero_op(Type,L,OpL),
+ norm_zero_op(Type,H,OpH),
+ interval_from_bounds(OpH,OpL,IN)),
+ Res = [IN,IP|NRes]
+ ; Res = NRes),
+ inv_sqr_interval_list_float(Type,LInter,NRes).
min_inv_sqr_float_nearest(float_simple,V,SV) :- !,
- inv_square_simple_float_min(V,F,SV),
- (F == 2 ->
- writeln(output,"Error":inv_square_simple_float_min(V,F,SV)),
- exit_block(abort)
- ; true).
+ inv_square_simple_float_min(V,F,SV),
+ (F == 2 ->
+ writeln(output,"Error":inv_square_simple_float_min(V,F,SV)),
+ exit_block(abort)
+ ; true).
min_inv_sqr_float_nearest(_,V,SV) :-
- inv_square_double_float_min(V,F,SV),
- (F == 2 ->
- writeln(output,"Error":inv_square_double_float_min(V,F,SV)),
- exit_block(abort)
- ; true).
+ inv_square_double_float_min(V,F,SV),
+ (F == 2 ->
+ writeln(output,"Error":inv_square_double_float_min(V,F,SV)),
+ exit_block(abort)
+ ; true).
max_inv_sqr_float_nearest(float_simple,V,SV) :- !,
- inv_square_simple_float_max(V,F,SV),
- (F == 2 ->
- writeln(output,"Error":inv_square_simple_float_max(V,F,SV)),
- exit_block(abort)
- ; true).
+ inv_square_simple_float_max(V,F,SV),
+ (F == 2 ->
+ writeln(output,"Error":inv_square_simple_float_max(V,F,SV)),
+ exit_block(abort)
+ ; true).
max_inv_sqr_float_nearest(_,V,SV) :-
- inv_square_double_float_max(V,F,SV),
- (F == 2 ->
- writeln(output,"Error":inv_square_double_float_max(V,F,SV)),
- exit_block(abort)
- ; true).
+ inv_square_double_float_max(V,F,SV),
+ (F == 2 ->
+ writeln(output,"Error":inv_square_double_float_max(V,F,SV)),
+ exit_block(abort)
+ ; true).
:- mode(sqr_interval_list_real(++,++,-)).
sqr_interval_list_real(_,[],[]).
sqr_interval_list_real(Type,[IV|LIV],[NIV|NLIV]) :-
- sqr_interval_real(Type,IV,NIV),
- sqr_interval_list_real(Type,LIV,NLIV).
+ sqr_interval_real(Type,IV,NIV),
+ sqr_interval_list_real(Type,LIV,NLIV).
%% Mode reel
sqr_interval_real(real,IV,NIV) :- !,
- min_max_inter(IV,Min,Max),
- (Min > 0.0 ->
- fois_min(Min,Min,L),
- fois_max(Max,Max,H)
- ; (Max < 0.0 ->
- fois_min(Max,Max,L),
- fois_max(Min,Min,H)
- ; % 0.0 est dans Min..Max
- P is max(abs(Min),Max),
- fois_max(P,P,H),
- L = 0.0)),
- interval_from_bounds(L,H,NIV).
+ min_max_inter(IV,Min,Max),
+ (Min > 0.0 ->
+ fois_min(Min,Min,L),
+ fois_max(Max,Max,H)
+ ; (Max < 0.0 ->
+ fois_min(Max,Max,L),
+ fois_max(Min,Min,H)
+ ; % 0.0 est dans Min..Max
+ P is max(abs(Min),Max),
+ fois_max(P,P,H),
+ L = 0.0)),
+ interval_from_bounds(L,H,NIV).
%% Mode double/simple
sqr_interval_real(Type,IV,NIV) :-
- (number(IV) ->
- square_float_nearest(Type,IV,NIV)
- ; min_max_inter(IV,Min,Max),
- (Min > 0.0 ->
- square_float_nearest_min_max(Type,Min,Max,B1,B2),
- interval_from_bounds(B1,B2,NIV)
- ; (Max < 0.0 ->
- square_float_nearest_min_max(Type,Min,Max,B1,B2),
- interval_from_bounds(B2,B1,NIV)
- ; % 0.0 est dans Min..Max
- N is max(abs(Min),Max),
- square_float_nearest(Type,N,N2),
- interval_from_bounds(0.0,N2,NIV)))).
+ (number(IV) ->
+ square_float_nearest(Type,IV,NIV)
+ ; min_max_inter(IV,Min,Max),
+ (Min > 0.0 ->
+ square_float_nearest_min_max(Type,Min,Max,B1,B2),
+ interval_from_bounds(B1,B2,NIV)
+ ; (Max < 0.0 ->
+ square_float_nearest_min_max(Type,Min,Max,B1,B2),
+ interval_from_bounds(B2,B1,NIV)
+ ; % 0.0 est dans Min..Max
+ N is max(abs(Min),Max),
+ square_float_nearest(Type,N,N2),
+ interval_from_bounds(0.0,N2,NIV)))).
square_float_nearest(float_simple,V,SV) :- !,
- getval(floating_biblio,F)@eclipse,
- square_simple_float(V,0,F,_Err,SV).
+ getval(floating_biblio,F)@eclipse,
+ square_simple_float(V,0,F,_Err,SV).
square_float_nearest(_,V,SV) :-
- getval(floating_biblio,F)@eclipse,
- square_double_float(V,0,F,_Err,SV).
-
+ getval(floating_biblio,F)@eclipse,
+ square_double_float(V,0,F,_Err,SV).
+
square_float_nearest_min_max(float_simple,Min,Max,B1,B2) :- !,
- getval(floating_biblio,F)@eclipse,
- square_simple_float(Min,0,F,_Err,B1),
- square_simple_float(Max,0,F,_Err,B2).
+ getval(floating_biblio,F)@eclipse,
+ square_simple_float(Min,0,F,_Err,B1),
+ square_simple_float(Max,0,F,_Err,B2).
square_float_nearest_min_max(_,Min,Max,B1,B2) :-
- getval(floating_biblio,F)@eclipse,
- square_double_float(Min,0,F,_Err,B1),
- square_double_float(Max,0,F,_Err,B2).
+ getval(floating_biblio,F)@eclipse,
+ square_double_float(Min,0,F,_Err,B1),
+ square_double_float(Max,0,F,_Err,B2).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% B = sqrt(A)
@@ -16849,7 +17052,7 @@ check_before_susp_sqrt_real(Type,Val1,Val) :-
true
; get_rel_between_real_args(Val1,Val,Rel),
sqrt_real_ineqs(Type,Val1,Val),
- notify_ineq_to_real_cstrs_if_new_rel(Rel,Val1,Val),
+ notify_ineq_to_real_cstrs_if_new_rel(Rel,Val1,Val),
my_suspend(sqrt_real1(Type,Val1,Val),4,(Val1,Val)->suspend:constrained)).
@@ -17770,17 +17973,11 @@ launch_diff_real(Type,A,B) :-
ensure_not_NaN((A,B)),
set_lazy_domain(Type,A),
set_lazy_domain(Type,B),
- (Type == real ->
- get_cstr_suspensions(A,LA),
- get_cstr_suspensions(B,LB),
- diff_real(Type,A,B),
- schedule_suspensions(1,s(LA)),
- schedule_suspensions(1,s(LB))
- ; diff_real(Type,A,B)),
+ diff_real(Type,A,B),
lin_diff_real(A,B),
set_priority(Prio),
wake_if_other_scheduled(Prio).
-
+
diff_real(Type,A,A) ?- !,
fail.
diff_real(Type,A,B) :-
@@ -18006,13 +18203,52 @@ diff_real_ineq(Type,A,B) :-
(getval(use_delta,1)@eclipse ->
get_rel_between_real_args(A,B,RAB),
(occurs(RAB,('?','#')) ->
- mreal:dvar_range(A,MinA,MaxA),
- mreal:dvar_range(B,MinB,MaxB),
- sort(0,<,[MinB,MaxA],[L1,H1]),
- MinDelta is - (get_number_of_floats_between(Type,L1,H1) - 1),
- sort(0,<,[MinA,MaxB],[L2,H2]),
- MaxDelta is get_number_of_floats_between(Type,L2,H2) - 1,
- launch_delta(A,B,'#',MinDelta..MaxDelta)
+ (Type == real ->
+ (is_real_box_rat(A,MinA) ->
+ MaxA = MinA
+ ; mreal:dvar_range(A,MinA,MaxA)),
+ (is_real_box_rat(B,MinB) ->
+ MaxB = MinB
+ ; mreal:dvar_range(B,MinB,MaxB)),
+ % On cherche MinY..MaxY tel que
+ % A + Y = B
+ % MinY..MaxY = MinB-MaxA..MaxB-MinA
+ ((MinB == -1.0Inf;
+ MaxA == 1.0Inf)
+ ->
+ MinY = -1.0Inf
+ ; MinY is rational(MinB)-rational(MaxA)),
+ ((MinA == -1.0Inf;
+ MaxB == 1.0Inf)
+ ->
+ MaxY = 1.0Inf
+ ; MaxY is rational(MaxB)-rational(MinA)),
+ (MinY == 0_1 ->
+ S = '+',
+ ((is_float_int_number(A),
+ is_float_int_number(B))
+ ->
+ LowY = 1_1
+ ; LowY = 0_1),
+ HighY = MaxY
+ ; LowY = MinY,
+ (MaxY == 0_1 ->
+ S = '+',
+ ((is_float_int_number(A),
+ is_float_int_number(B))
+ ->
+ HighY = -1_1
+ ; HighY = 0_1)
+ ; S = '#',
+ HighY = MaxY)),
+ launch_delta(A,B,S,LowY..HighY)
+ ; mreal:dvar_range(A,MinA,MaxA),
+ mreal:dvar_range(B,MinB,MaxB),
+ sort(0,<,[MinB,MaxA],[L1,H1]),
+ MinDelta is - (get_number_of_floats_between(Type,L1,H1) - 1),
+ sort(0,<,[MinA,MaxB],[L2,H2]),
+ MaxDelta is get_number_of_floats_between(Type,L2,H2) - 1,
+ launch_delta(A,B,'#',MinDelta..MaxDelta))
; (RAB == '=<' ->
NRAB = '<'
; (RAB == '>=' ->
@@ -18195,16 +18431,12 @@ launch_geq_real(Type,A,B) :-
set_lazy_domain(Type,A),
set_lazy_domain(Type,B),
check_no_float_error(Type,(A,B)),
- get_cstr_suspensions(A,LA),
- get_cstr_suspensions(B,LB),
(Type \== real ->
launch_float_number(A),
launch_float_number(B)
; true),
geq_real(Type,A,B),
lin_geq_real(A,B),
- schedule_suspensions(1,s(LA)),
- schedule_suspensions(1,s(LB)),
set_priority(Prio),
wake_if_other_scheduled(Prio).
@@ -18255,16 +18487,21 @@ check_geq_real(Type,A,B) :-
; Continue = 1)),
(var(Continue) ->
true
- ; save_cstr_suspensions((A,B)),
- analyze_other_real_ineq(Type,geq_real,A,B,Stop),
- check_geq_real(Type,A,B,Stop,Continue1),
- check_launch_geq(Type,A,B,Continue1,Suspend),
- geq_real_ineq(Type,A,B),
- notify_ineq_to_real_cstrs_if_new_rel(Rel,A,B),
- (var(Suspend) ->
- true
- ; set_prio_inst([A,B],3,4,Prio),
- my_suspend(geq_real(Type,A,B), Prio, (A,B)->suspend:constrained))).
+ ; ((Type == real,
+ not check_exists_lin_expr_giving_diff_args(Type,A,B,_Stop))
+ ->
+ % si le diff échoue alors =
+ protected_unify(A,B)
+ ; save_cstr_suspensions((A,B)),
+ analyze_other_real_ineq(Type,geq_real,A,B,Stop),
+ check_geq_real(Type,A,B,Stop,Continue1),
+ check_launch_geq(Type,A,B,Continue1,Suspend),
+ geq_real_ineq(Type,A,B),
+ notify_ineq_to_real_cstrs_if_new_rel(Rel,A,B),
+ (var(Suspend) ->
+ true
+ ; set_prio_inst([A,B],3,4,Prio),
+ my_suspend(geq_real(Type,A,B), Prio, (A,B)->suspend:constrained)))).
check_launch_geq(_,A,B,Continue,_) :-
var(Continue),
@@ -18294,65 +18531,92 @@ check_launch_geq(Type,A,B,_,Continue) :-
geq_real_ineq(Type,A,A) ?- !.
geq_real_ineq(Type,A,B) :-
- var(A),
- var(B),
- !,
- (getval(use_delta,1)@eclipse ->
+ ((getval(use_delta,1)@eclipse,
+ var(A),
+ var(B))
+ ->
once (exists_delta_Rel(A,B,ORel,_,_);true),
ORel \== <,
- (occurs(ORel,(=<,>)) ->
- Stop = 1,
- (ORel == =< ->
- protected_unify(A = B)
- ; true)
- ; % On ajuste les bornes pour avoir les "vrais deltas"
- % Attention aux zeros
- mreal:dvar_range(A,MinA0,MaxA),
- mreal:dvar_range(B,MinB,MaxB0),
- (MinA0 < MinB ->
- % Attention aux zeros
- ((MinB == 0.0,
- MaxA == -0.0)
- ->
- MinA = -0.0
- ; MinA = MinB)
- ; MinA = MinA0),
- (MaxA < MaxB0 ->
- % Attention aux zeros
- ((MaxA == -0.0,
- MinB == 0.0)
- ->
- MaxB == 0.0
- ; MaxB = MaxA)
- ; MaxB = MaxB0),
- % Invariants a maintenir
- MinA =< MaxA,
- MinB =< MaxB,
- (MinA == MaxA ->
- Stop = 1,
- protected_unify(A = MinA),
- mreal:dvar_remove_greater(B,MaxB)
- ; true),
- (MinB == MaxB ->
+ (Type == real ->
+ geq_real_int_ineq(A,B)
+ ; (occurs(ORel,(=<,>)) ->
Stop = 1,
- protected_unify(B = MinB),
- mreal:dvar_remove_smaller(A,MinA)
- ; true)),
- ((nonvar(Stop);
- nonvar(A);
- nonvar(B))
- ->
- true
- ; (MinA > MaxB ->
- MinDelta is get_number_of_floats_between(Type,MaxB,MinA) - 1
- ; % Les intervalles se recouvrent la plus petite distance
- % vaut 0
- MinDelta = 0),
- % La plus grande distance est entre MaxA et MinB
- MaxDelta is get_number_of_floats_between(Type,MinB,MaxA) - 1,
- launch_delta(B,A,+,MinDelta..MaxDelta))
+ (ORel == =< ->
+ protected_unify(A = B)
+ ; true)
+ ; % On ajuste les bornes pour avoir les "vrais deltas"
+ % Attention aux zeros
+ mreal:dvar_range(A,MinA0,MaxA),
+ mreal:dvar_range(B,MinB,MaxB0),
+ (MinA0 < MinB ->
+ % Attention aux zeros
+ ((MinB == 0.0,
+ MaxA == -0.0)
+ ->
+ MinA = -0.0
+ ; MinA = MinB)
+ ; MinA = MinA0),
+ (MaxA < MaxB0 ->
+ % Attention aux zeros
+ ((MaxA == -0.0,
+ MinB == 0.0)
+ ->
+ MaxB == 0.0
+ ; MaxB = MaxA)
+ ; MaxB = MaxB0),
+ % Invariants a maintenir
+ MinA =< MaxA,
+ MinB =< MaxB,
+ (MinA == MaxA ->
+ Stop = 1,
+ protected_unify(A = MinA),
+ mreal:dvar_remove_greater(B,MaxB)
+ ; true),
+ (MinB == MaxB ->
+ Stop = 1,
+ protected_unify(B = MinB),
+ mreal:dvar_remove_smaller(A,MinA)
+ ; true)),
+ ((nonvar(Stop);
+ nonvar(A);
+ nonvar(B))
+ ->
+ true
+ ; (MinA > MaxB ->
+ MinDelta is get_number_of_floats_between(Type,MaxB,MinA) - 1
+ ; % Les intervalles se recouvrent la plus petite distance
+ % vaut 0
+ MinDelta = 0),
+ % La plus grande distance est entre MaxA et MinB
+ MaxDelta is get_number_of_floats_between(Type,MinB,MaxA) - 1,
+ launch_delta(B,A,+,MinDelta..MaxDelta)))
; true).
-geq_real_ineq(_,_,_).
+
+geq_real_int_ineq(A,B) :-
+ % A et B sont déjà réduits
+ var(A),
+ var(B),!,
+ (is_real_box_rat(A,MinA) ->
+ MaxA = MinA
+ ; mreal:dvar_range(A,MinA,MaxA)),
+ (is_real_box_rat(B,MinB) ->
+ MaxB = MinB
+ ; mreal:dvar_range(B,MinB,MaxB)),
+ ((MaxA == 1.0Inf;
+ MinB == -1.0Inf)
+ ->
+ H = 1.0Inf
+ ; H is rational(MaxA) - rational(MinB)),
+ ((MaxA \== 1.0Inf,
+ MinA \== -1.0Inf,
+ MaxB =< MinA)
+ ->
+ % Forme resolue, pas d'inf ici
+ L is rational(MinA) - rational(MaxB)
+ ; L = 0_1),
+ launch_delta(B,A,+,L..H).
+geq_real_int_ineq(A,B).
+
check_geq_real(_,_,_,1,_) ?- !.
check_geq_real(Type,A,B,_,Suspend) :-
@@ -18508,22 +18772,20 @@ gt_real(A,B) :-
launch_gt_real(Type,A,B).
launch_gt_real(Type,A,B) :-
+ get_rel_between_real_args(A,B,RelAB),
+ not occurs(RelAB,('=','<','=<')),
get_priority(Prio),
set_priority(1),
ensure_not_NaN((A,B)),
set_lazy_domain(Type,A),
set_lazy_domain(Type,B),
check_no_float_error(Type,(A,B)),
- get_cstr_suspensions(A,LA),
- get_cstr_suspensions(B,LB),
(Type \== real ->
launch_float_number(A),
launch_float_number(B)
; true),
gt_real(Type,A,B),
lin_gt_real(A,B),
- schedule_suspensions(1,s(LA)),
- schedule_suspensions(1,s(LB)),
set_priority(Prio),
wake_if_other_scheduled(Prio).
@@ -18542,6 +18804,10 @@ check_gt_real(Type,A,B) :-
get_rel_between_real_args(A,B,RelAB),
not occurs(RelAB,('=','<','=<')),
analyze_other_real_ineq(Type,gt_real,A,B,Stop),
+ (Type == real ->
+ % si le diff échoue alors le gt aussi
+ check_exists_lin_expr_giving_diff_args(Type,A,B,_)
+ ; true),
check_gt_real(Type,A,B,Stop,Continue),
check_launch_gt(Type,A,B,Continue,Suspend),
gt_real_ineq(Type,A,B),
@@ -18553,7 +18819,6 @@ check_gt_real(Type,A,B) :-
->
true
; set_prio_inst([A,B],3,4,Prio),
-
my_suspend(gt_real(Type,A,B), Prio, (A,B)->suspend:constrained)).
check_launch_gt(_,A,B,Continue,_) :-
@@ -18590,60 +18855,74 @@ is_cast_or_float_int(A) :-
gt_real_ineq(Type,A,A) ?- !,
fail.
gt_real_ineq(Type,A,B) :-
- (getval(use_delta,1)@eclipse ->
+ ((getval(use_delta,1)@eclipse,
+ var(A),
+ var(B))
+ ->
once (exists_delta_Rel(A,B,ORel,_,_);true),
not occurs(ORel,(<,=<)),
- mreal:dvar_range(A,MinA0,MaxA),
- mreal:dvar_range(B,MinB,MaxB0),
- % On ajuste les bornes pour avoir les "vrais deltas"
(Type == real ->
- MinA is max(MinA0,MinB),
- MaxB is min(MaxA,MaxB0)
- ; MinA is max(MinA0,get_next_float(Type,MinB)),
- MaxB is min(get_previous_float(Type,MaxA),MaxB0)),
- % Invariants a maintenir
- MinA =< MaxA,
- MinB =< MaxB,
- (MinA == MaxA ->
- Stop = 1,
- protected_unify(A = MinA),
- mreal:dvar_remove_greater(B,A)
- ; true),
- (MinB == MaxB ->
- Stop = 1,
- protected_unify(B = MinB),
- mreal:dvar_remove_smaller(A,B)
- ; true),
- ((nonvar(Stop);
- nonvar(A);
- nonvar(B))
- ->
- true
- ; (MinA > MaxB ->
- MinDelta is get_number_of_floats_between(Type,MaxB,MinA) - 1
- ; % Les intervalles se recouvrent
- ((is_float_int_number(A),
- is_float_int_number(B))
- ->
- % on doit considerer la plus petite distance entre
- % des entiers de A et B
- get_next_float_int(Type,MinA,NextMinA),
- get_previous_float_int(Type,MaxB,PrevMaxB),
- get_number_of_floats_between(Type,MinA,NextMinA,DMA),
- get_number_of_floats_between(Type,PrevMaxB,MaxB,DMB),
- MinDelta is max(1,min(DMA,DMB) - 1)
- ; % la plus petite distance
- % vaut 1 en float et 0 en real
- ((is_float_number(A),
- is_float_number(B))
- ->
- MinDelta = 1
- ; MinDelta = 0))),
- % La plus grande distance est entre MaxA et MinB
- MaxDelta is get_number_of_floats_between(Type,MinB,MaxA) - 1,
- launch_delta(B,A,+,MinDelta..MaxDelta))
+ gt_real_int_ineq(A,B)
+ ; mreal:dvar_range(A,MinA0,MaxA),
+ mreal:dvar_range(B,MinB,MaxB0),
+ MinA is max(MinA0,get_next_float(Type,MinB)),
+ MaxB is min(get_previous_float(Type,MaxA),MaxB0),
+ % Invariants a maintenir
+ MinA =< MaxA,
+ MinB =< MaxB,
+ (MinA == MaxA ->
+ Stop = 1,
+ protected_unify(A = MinA),
+ mreal:dvar_remove_greater(B,A)
+ ; true),
+ (MinB == MaxB ->
+ Stop = 1,
+ protected_unify(B = MinB),
+ mreal:dvar_remove_smaller(A,B)
+ ; true),
+ ((nonvar(Stop);
+ nonvar(A);
+ nonvar(B))
+ ->
+ true
+ ; (MinA > MaxB ->
+ MinDelta is get_number_of_floats_between(Type,MaxB,MinA) - 1
+ ; % Les intervalles se recouvrent
+ MinDelta = 1),
+ % La plus grande distance est entre MaxA et MinB
+ MaxDelta is get_number_of_floats_between(Type,MinB,MaxA) - 1,
+ launch_delta(B,A,+,MinDelta..MaxDelta)))
; true).
+gt_real_int_ineq(A,B) :-
+ % A et B sont déjà réduits
+ var(A),
+ var(B),!,
+ (is_real_box_rat(A,MinA) ->
+ MaxA = MinA
+ ; mreal:dvar_range(A,MinA,MaxA)),
+ (is_real_box_rat(B,MinB) ->
+ MaxB = MinB
+ ; mreal:dvar_range(B,MinB,MaxB)),
+ ((MaxA == 1.0Inf;
+ MinB == -1.0Inf)
+ ->
+ H = 1.0Inf
+ ; H is rational(MaxA) - rational(MinB)),
+ ((MaxA \== 1.0Inf,
+ MinA \== -1.0Inf,
+ MaxB < MinA)
+ ->
+ % Forme resolue, pas d'inf ici
+ L is rational(MinA) - rational(MaxB)
+ ; ((is_float_int_number(A),
+ is_float_int_number(B))
+ ->
+ L = 1_1
+ ; L = 0_1)),
+ launch_delta(B,A,+,L..H).
+gt_real_int_ineq(A,B).
+
check_gt_real(_,_,_,1,_) ?- !.
check_gt_real(Type,A,B,_,Suspend) :-
@@ -18663,18 +18942,42 @@ check_gt_real(Type,A,B,_,Suspend) :-
; Suspend = 1)).
gt_real_number_box(Type,A,B,Continue) :-
+ % réductions pour un geq
+ mreal:dvar_range(A,MinA0,MaxA0),
+ mreal:dvar_range(B,MinB0,MaxB0),
+ % MinA >= MinB
+ NMinA is max(MinA0,MinB0),
+ mreal:dvar_remove_smaller(A,NMinA),
+ % MaxA >= MaxB
+ NMaxB is min(MaxA0,MaxB0),
+ mreal:dvar_remove_greater(B,NMaxB),
+ mreal:dvar_range(A,MinA,MaxA),
+ mreal:dvar_range(B,MinB,MaxB),
((Type \== real;
is_float_number(A),
is_float_number(B),
- is_inside_mantissa(real,A), % freins inutiles ??
- is_inside_mantissa(real,B))
+ (is_inside_mantissa(real,MaxA) ->
+ Up = 1
+ ; true),
+ (is_inside_mantissa(real,MinB) ->
+ Down = 1
+ ; true),
+ (nonvar(Up);nonvar(Down)))
->
- mreal:dvar_range(A,MinA,MaxA),
- mreal:dvar_range(B,MinB,MaxB),
- get_next_float(Type,MinB,LA),
- mreal:dvar_remove_smaller(A,LA),
- get_previous_float(Type,MaxA,HB),
- mreal:dvar_remove_greater(B,HB),
+ ((Type == real ->
+ nonvar(Down)
+ ; true)
+ ->
+ get_next_float(Type,MinB,LA),
+ mreal:dvar_remove_smaller(A,LA)
+ ; true),
+ ((Type == real ->
+ nonvar(Up)
+ ; true)
+ ->
+ get_previous_float(Type,MaxA,HB),
+ mreal:dvar_remove_greater(B,HB)
+ ; true),
(mreal:mindomain(A) > mreal:maxdomain(B) ->
true
; Continue = 1)
diff --git a/Src/COLIBRI/smt_import.pl b/Src/COLIBRI/smt_import.pl
index 1dbb8ce441847ad28e7c0bfa6cd7e9c05893167a..6c9a00020d452afa51ec1cc8b9173e4475ee422d 100644
--- a/Src/COLIBRI/smt_import.pl
+++ b/Src/COLIBRI/smt_import.pl
@@ -91,7 +91,9 @@ dolmen_to_colibri_term(set_info(app(symbol(SFlagInfo),
dolmen_to_colibri_term(set_option(app(symbol(SFlagOption),
[symbol(SOption)])),Term) ?- !,
atom_string(FlagOption,SFlagOption),
- atom_string(Option,SOption),
+ (SFlagOption == ":colibri_intSize" ->
+ term_string(Option,SOption)
+ ; atom_string(Option,SOption)),
Term = 'set-option'(FlagOption,Option).
dolmen_to_colibri_term(decl([term_decl(id(Id,_,_),fun(Poly,InSorts,
OutSort))]),Term) ?-
diff --git a/Src/COLIBRI/solve.pl b/Src/COLIBRI/solve.pl
index de4de89301c5716979cabfe1a1443d27515ef02c..4d5611c17d7bc34f66c54eb9aac1b9e3c5196e99 100644
--- a/Src/COLIBRI/solve.pl
+++ b/Src/COLIBRI/solve.pl
@@ -3924,6 +3924,9 @@ diff_reif(Type,Kill,A,B,Bool) :- !,
diff_real_chk_nan(Type,A,A) ?- !,
fail.
+diff_real_chk_nan(real_int,A,B) :- !,
+ real_vars(real_int,[A,B]),
+ launch_diff_real(real,A,B).
diff_real_chk_nan(real,A,B) :- !,
launch_diff_real(real,A,B).
diff_real_chk_nan(Type,A,B) :-
@@ -11808,33 +11811,13 @@ simple_resol_real(Var) :-
; % on essaye les boites autour de Value
set_typed_intervals(Var,real,[PV..Value]),
(not_inf_bounds(Var) ->
- RatRand is rational(frandom),
- RV is rational(Value),
- RP is rational(PV),
- Eps is rational(4.9e-324)/2_1,
- MinR is (RP + (abs(RP)*Eps)),
- MaxR is (RV - (abs(RV)*Eps)),
- Rat0 is RP + (RV-RP)*RatRand,
- (is_float_int_number(Var) ->
- Rat1 is truncate(Rat0)
- ; Rat1 = Rat0),
- Rat is min(max(MinR,Rat1),MaxR),
+ get_rand_rat_in_rbox(Var,PV,Value,Rat),
(launch_box_rat(Var,Rat);
launch_box(Var))
; launch_box(Var))
; set_typed_intervals(Var,real,[Value..NV]),
(not_inf_bounds(Var) ->
- RatRand is rational(frandom),
- RV is rational(Value),
- RN is rational(NV),
- Eps is rational(4.9e-324)/2_1,
- MinR is (RV + (abs(RV)*Eps)),
- MaxR is (RN - (abs(RN)*Eps)),
- Rat0 is RV + (RN-RV)*RatRand,
- (is_float_int_number(Var) ->
- Rat1 is truncate(Rat0)
- ; Rat1 = Rat0),
- Rat is max(min(MinR,Rat1),MaxR),
+ get_rand_rat_in_rbox(Var,Value,NV,Rat),
(launch_box_rat(Var,Rat);
launch_box(Var))
; launch_box(Var)))
@@ -11846,6 +11829,20 @@ simple_resol_real(Var) :-
my_notify_constrained(Var)
; true).
+% ESSAI : instanciation pas un rat random dans une rbox finie
+get_rand_rat_in_rbox(Var,Value,NV,Rat) :-
+ RatRand is rational(frandom),
+ RV is rational(Value),
+ RN is rational(NV),
+ Eps is rational(4.9e-324)/2_1,
+ MinR is (RV + (abs(RV)*Eps)),
+ MaxR is (RN - (abs(RN)*Eps)),
+ Rat0 is RV + (RN-RV)*RatRand,
+ (is_float_int_number(Var) ->
+ Rat1 is truncate(Rat0)
+ ; Rat1 = Rat0),
+ Rat is max(min(MinR,Rat1),MaxR).
+
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Instanciations random
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
diff --git a/tests/sat/bug25.smt2 b/tests/sat/bug25.smt2
new file mode 100644
index 0000000000000000000000000000000000000000..cdba76b4f5be00d3677575a59a6637a58f8ee1c1
--- /dev/null
+++ b/tests/sat/bug25.smt2
@@ -0,0 +1,64 @@
+;; produced by colibri.drv ;;
+(set-logic ALL)
+(set-info :smt-lib-version 2.6)
+;;; generated by SMT-LIB2 driver
+;;; SMT-LIB2 driver: bit-vectors, common part
+;;; SMT-LIB2: integer arithmetic
+
+
+(declare-sort value 0)
+
+(declare-fun valueqtint (value) Int)
+
+(define-fun to_rep ((x value)) Int (valueqtint x))
+
+
+(declare-const a (Array Int (Array Int value)))
+
+(declare-const i Int)
+(declare-const j Int)
+
+(declare-const x value)
+(declare-const y value)
+
+(assert
+ (not
+ (= (to_rep
+ (select
+ (select
+ (store
+ (store a i
+ (store
+ (select a i)
+ j x))
+ i
+ (store
+ (select
+ (store a i
+ (store
+ (select a i)
+ j x))
+ i)
+ j y))
+ i)
+ j))
+ (to_rep
+ (select
+ (select
+ (store
+ (store a i
+ (store
+ (select a i)
+ j x))
+ i
+ (store
+ (select
+ (store a i
+ (store
+ (select a i)
+ j x))
+ i)
+ j y))
+ j)
+ i)))))
+(check-sat)