diff --git a/Src/COLIBRI/realarith.pl b/Src/COLIBRI/realarith.pl
index 50fd3165b24a2c07bfc6fa5e7296dee675e1fd39..3bd2216e898ad8423e03f821cbb922a15abd2973 100755
--- a/Src/COLIBRI/realarith.pl
+++ b/Src/COLIBRI/realarith.pl
@@ -3840,24 +3840,26 @@ set_interval_box(Var,Min,Max) :-
%% avec une autre contrainte produisant une rbox
%% pour les memes arguments
check_rbox_cstrs(3,Goal) :-
- %% Arite 3
- Goal =.. [F,Type,A0,B0,C],
- check_rbox_rat(A0,A),
- check_rbox_rat(B0,B),
+ % Arite 3
+ Goal =.. [F,Type,A0,B0,C],
+ check_rbox_rat(A0,A),
+ (occurs(F,(power_real,inv_power_real)) ->
+ B = B0
+ ; check_rbox_rat(B0,B)),
var(C),
!,
(occurs(F,(add_real1,mult_real1)) ->
- number_sort(0,=<,[A,B],[NA,NB])
- ; (NA,NB) = (A,B)),
+ number_sort(0,=<,[A,B],[NA,NB])
+ ; (NA,NB) = (A,B)),
Key =.. [F,Type,NA,NB],
(check_seen_expr(Key,NC,Type) ->
protected_unify(C,NC)
; add_seen_expr(Key,C,Type)),
make_box_rat(F,A,B,C).
check_rbox_cstrs(2,Goal) :-
- %% Arite 2
- Goal =.. [F,Type,A,B],
- var(B),
+ % Arite 2
+ Goal =.. [F,Type,A,B],
+ var(B),
!,
Key =.. [F,Type,A],
(check_seen_expr(Key,NB,Type) ->
@@ -15063,162 +15065,165 @@ power_real_type(Type,A,N,B) :-
; fp_power(as(A,Type),as(N,int)) $= as(B,Type)).
power_real(Type,A,2,B) ?- !,
- %% square_real est plus efficace car
- %% elle a une projection inverse
+ % square_real est plus efficace car
+ % elle a une projection inverse
ensure_not_NaN((A,B)),
set_lazy_domain(Type,A),
- set_lazy_domain(Type,B),
+ set_lazy_domain(Type,B),
check_no_float_error(Type,(A,B)),
- square_real(Type,A,B).
+ square_real(Type,A,B).
power_real(Type,A,N,B) :-
- integer(N),
- N >= 0,
- N =< 2^53,
- mreal:set_typed_intervals(A,Type,[-1.0Inf..1.0Inf]),
- mreal:set_typed_intervals(B,Type,[-1.0Inf..1.0Inf]),
+ integer(N),
+ N >= 0,
+ N =< 2^53,
+ mreal:set_typed_intervals(A,Type,[-1.0Inf..1.0Inf]),
+ mreal:set_typed_intervals(B,Type,[-1.0Inf..1.0Inf]),
ensure_not_NaN((A,B)),
- (Type == real ->
- true
- ; launch_float_number(A),
- launch_float_number(B)),
- (N == 0 ->
- protected_unify(B = 1.0)
- ; (N == 1 ->
- protected_unify(A = B)
- ; same_float_int_number_status(Type,A,B),
+ (Type == real ->
+ true
+ ; launch_float_number(A),
+ launch_float_number(B)),
+ (N == 0 ->
+ protected_unify(B = 1.0)
+ ; (N == 1 ->
+ protected_unify(A = B)
+ ; same_float_int_number_status(Type,A,B),
power_real_interval(Type,A,N,B),
- (mod(N,2,0) ->
- mreal:set_typed_intervals(B,Type,[0.0..1.0Inf])
- ; true),
- power_real1(Type,A,N,B))).
+ (mod(N,2,0) ->
+ mreal:set_typed_intervals(B,Type,[0.0..1.0Inf])
+ ; true),
+ power_real1(Type,A,N,B))).
power_real1(Type,A,N,B) :-
- get_priority(Prio),
- set_priority(1),
- same_float_int_number_status(Type,A,B),
+ get_priority(Prio),
+ set_priority(1),
+ same_float_int_number_status(Type,A,B),
power_real_bis(Type,A,N,B),
- set_priority(Prio),
- wake_if_other_scheduled(Prio).
+ set_priority(Prio),
+ wake_if_other_scheduled(Prio).
power_real_bis(Type,Val1,N,Val) :-
- save_cstr_suspensions((Val1,Val)),
- power_real_2_args_equal(Type,Val1,N,Val,Continue0),
- (var(Continue0) ->
- true
- ; check_exists_power_real(Type,Val1,N,Val),
- check_delta_power_real_int(Type,Val1,N,Mod2,Val),
+ save_cstr_suspensions((Val1,Val)),
+ power_real_2_args_equal(Type,Val1,N,Val,Continue0),
+ (var(Continue0) ->
+ true
+ ; check_exists_power_real(Type,Val1,N,Val),
+ check_delta_power_real_int(Type,Val1,N,Mod2,Val),
power_real_inst(Type,Val1,N,Val,Continue0),
check_launch_power_int(Type,Val1,N,Val,Continue0,Continue),
- (nonvar(Continue) ->
- power_real_rec(Type,Val1,N,Val),
- % Ajouter des inegalites quand c est possible ici
- % gt_real_ineq(Type,Val,Val1),
- check_before_susp_power_real(Type,Val1,N,Val)
- ; true)).
+ (nonvar(Continue) ->
+ (ground((Val1,N)) ->
+ % Val rationnel ?
+ true
+ ; power_real_rec(Type,Val1,N,Val)),
+ % Ajouter des inegalites quand c est possible ici
+ % gt_real_ineq(Type,Val,Val1),
+ check_before_susp_power_real(Type,Val1,N,Val)
+ ; true)).
check_launch_power_int(Type,A,N,B,Continue,_) :-
var(Continue),
!.
check_launch_power_int(Type,A,N,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),
- power(IA,N,IB),
- cast_real_int(Type,B,IB)
- ; Continue = 1).
+ ->
+ cast_real_int(Type,A,IA),
+ power(IA,N,IB),
+ cast_real_int(Type,B,IB)
+ ; Continue = 1).
check_delta_power_real_int(Type,A,N,Mod2,B) :-
((Type == real,
is_float_int_number(A),
exists_delta_Rel(A,B,Rel,_,_))
->
- (Mod2 == 0 ->
- Rel \== '>',
- (Rel == '>=' ->
- %% Donc A = B et A :: [0,1]
- mreal:set_typed_intervals(A,real,[0.0,1.0]),
- protected_unify(A = B)
- ; (Rel == '=<' ->
- true
- ; %% A <> B
- mreal:set_typed_intervals(A,real,[-1.0Inf .. -1.0,
+ (Mod2 == 0 ->
+ Rel \== '>',
+ (Rel == '>=' ->
+ % Donc A = B et A :: [0,1]
+ mreal:set_typed_intervals(A,real,[0.0,1.0]),
+ protected_unify(A = B)
+ ; (Rel == '=<' ->
+ true
+ ; % A <> B
+ mreal:set_typed_intervals(A,real,[-1.0Inf .. -1.0,
2.0 .. 1.0Inf]),
mreal:set_typed_intervals(B,real,[-1.0Inf .. -1.0,
- 1.0..1.0Inf])))
- ; %% A et B de meme signe
- (Rel == '<' ->
- %% A > 1
- mreal:dvar_remove_smaller(A,2.0),
- float_of_rat(real,rtn,RMinB,MinB),
+ 1.0..1.0Inf])))
+ ; % A et B de meme signe
+ (Rel == '<' ->
+ % A > 1
+ mreal:dvar_remove_smaller(A,2.0),
+ float_of_rat(real,rtn,RMinB,MinB),
RMinB is 2_1^N,
- float_of_rat(real,rtn,RMinB,MinB),
+ float_of_rat(real,rtn,RMinB,MinB),
mreal:dvar_remove_smaller(B,MinB)
- ; (Rel == '=<' ->
- %% A >= -1
- mreal:dvar_remove_smaller(A,-1.0),
- mreal:dvar_remove_smaller(B,-1.0)
- ; (Rel == '>' ->
- %% A < -1
- mreal:dvar_remove_greater(A,-2.0),
- RMaxB is -2_1^N,
+ ; (Rel == '=<' ->
+ % A >= -1
+ mreal:dvar_remove_smaller(A,-1.0),
+ mreal:dvar_remove_smaller(B,-1.0)
+ ; (Rel == '>' ->
+ % A < -1
+ mreal:dvar_remove_greater(A,-2.0),
+ RMaxB is -2_1^N,
float_of_rat(real,rtp,RMaxB,MaxB),
- mreal:dvar_remove_greater(B,MaxB)
- ; (Rel == '>=' ->
- %% A =< 1
- mreal:dvar_remove_greater(A,1.0),
- mreal:dvar_remove_greater(B,1.0)
- ; %% Rel = '#'
- mreal:set_typed_intervals(A,real,[-1.0Inf.. -2.0, 2.0..1.0Inf]),
- mreal:set_typed_intervals(B,real,[-1.0Inf.. -2.0, 2.0..1.0Inf]))))))
- ; true).
+ mreal:dvar_remove_greater(B,MaxB)
+ ; (Rel == '>=' ->
+ % A =< 1
+ mreal:dvar_remove_greater(A,1.0),
+ mreal:dvar_remove_greater(B,1.0)
+ ; % Rel = '#'
+ mreal:set_typed_intervals(A,real,[-1.0Inf.. -2.0, 2.0..1.0Inf]),
+ mreal:set_typed_intervals(B,real,[-1.0Inf.. -2.0, 2.0..1.0Inf]))))))
+ ; true).
%% Val^N = Val
power_real_2_args_equal(Type,Val,N,Val,_) ?- !,
- (Type == real ->
+ (Type == real ->
(mod(N,2,0) ->
Inter = [0.0,1.0]
- ; Inter = [-1.0,0.0,1.0])
+ ; Inter = [-1.0,0.0,1.0])
; (mod(N,2,0) ->
Inter = [0.0,1.0,1.0Inf]
- ; Inter = [-1.0Inf,-1.0,-0.0,0.0,1.0,1.0Inf])),
- mreal:set_typed_intervals(Val,Type,Inter).
+ ; Inter = [-1.0Inf,-1.0,-0.0,0.0,1.0,1.0Inf])),
+ mreal:set_typed_intervals(Val,Type,Inter).
%% Val^N = -Val
power_real_2_args_equal(Type,Val1,N,Val,Continue) :-
- get_saved_cstr_suspensions(LSusp),
- ((member((Susp,op_real1(Type,X,Y)),LSusp),
- (X == Val1, Y == Val;
- X == Val, Y == Val1))
- ->
- % Val1: [-1.0Inf,-1.0,-0.0], Val: [0.0,1.0,1.0Inf], N pair
- mod(N,2,0),
+ get_saved_cstr_suspensions(LSusp),
+ ((member((Susp,op_real1(Type,X,Y)),LSusp),
+ (X == Val1, Y == Val;
+ X == Val, Y == Val1))
+ ->
+ % Val1: [-1.0Inf,-1.0,-0.0], Val: [0.0,1.0,1.0Inf], N pair
+ mod(N,2,0),
(Type == real ->
mreal:set_typed_intervals(Val1,real,[-1.0,0.0]),
mreal:set_typed_intervals(Val,real,[0.0,1.0])
; 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).
+ ; Continue = 1).
check_exists_power_real(Type,A,N,B) :-
- ((var(A),
- get_saved_cstr_suspensions(LSusp),
- member((Susp,power_real1(Type,X,N,Y)),LSusp),
- ( X == A, (U1,U2) = (Y,B)
- ; Type == real, mod(N,2,1), var(Y),Y == B, (U1,U2) = (X,A)))
- ->
- kill_suspension(Susp),
- protected_unify(U1 = U2)
- ; true).
+ ((var(A),
+ get_saved_cstr_suspensions(LSusp),
+ member((Susp,power_real1(Type,X,N,Y)),LSusp),
+ ( X == A, (U1,U2) = (Y,B)
+ ; Type == real, mod(N,2,1), var(Y),Y == B, (U1,U2) = (X,A)))
+ ->
+ kill_suspension(Susp),
+ protected_unify(U1 = U2)
+ ; true).
check_before_susp_power_real(Type,Val1,N,Val) :-
- power_real_inst(Type,Val1,N,Val,Continue),
- (var(Continue) ->
- true
- ; ndelta:disable_delta_check,
+ power_real_inst(Type,Val1,N,Val,Continue),
+ (var(Continue) ->
+ true
+ ; ndelta:disable_delta_check,
check_other_power_ineqs_from_res(Type,N,Val1,Val),
ndelta:allow_delta_check,
@@ -15438,36 +15443,36 @@ power_real_inst(Type,Val1,N,Val,Continue) :-
; Continue = 1)).
power_real_rec(Type,Val1,N,Val) :-
- mreal:dvar_domain(Val1,Dom1),
- mreal:dvar_domain(Val,Dom),
- power_real_rec(Type,Val1,N,Val,Dom1,Dom).
+ mreal:dvar_domain(Val1,Dom1),
+ mreal:dvar_domain(Val,Dom),
+ power_real_rec(Type,Val1,N,Val,Dom1,Dom).
power_real_rec(Type,Val1,N,Val,Dom1,Dom) :-
- %% Val = exp(Val1)
- mreal:dom_interval(Dom1,LInter1),
- power_real_interval_list(Type,LInter1,N,PowLInter),
- mreal:list_to_typed_dom(Type,PowLInter,PowDom),
- mreal:dom_intersection(Dom,PowDom,NDom,_),
- mreal:dvar_set(Val,NDom),
- %% Val1 ~= pow(Val,1/N)
- mreal:dvar_domain(Val,NewDom),
- mreal:dom_interval(NewDom,NLInter),
- inv_power_real_interval_list(Type,NLInter,N,InvPowLInter),
- mreal:list_to_typed_dom(Type,InvPowLInter,InvPowDom),
- mreal:dom_intersection(Dom1,InvPowDom,NDom1,_),
- mreal:dvar_set(Val1,NDom1),
- mreal:dvar_domain(Val1,NewDom1),
- % = necessaire
- (NewDom1 = Dom1 ->
- %% On a fini
- true
- ; power_real_rec(Type,Val1,N,Val,NewDom1,NewDom)).
+ % Val = exp(Val1)
+ mreal:dom_interval(Dom1,LInter1),
+ power_real_interval_list(Type,LInter1,N,PowLInter),
+ mreal:list_to_typed_dom(Type,PowLInter,PowDom),
+ mreal:dom_intersection(Dom,PowDom,NDom,_),
+ mreal:dvar_set(Val,NDom),
+ % Val1 ~= pow(Val,1/N)
+ mreal:dvar_domain(Val,NewDom),
+ mreal:dom_interval(NewDom,NLInter),
+ inv_power_real_interval_list(Type,NLInter,N,InvPowLInter),
+ mreal:list_to_typed_dom(Type,InvPowLInter,InvPowDom),
+ mreal:dom_intersection(Dom1,InvPowDom,NDom1,_),
+ mreal:dvar_set(Val1,NDom1),
+ mreal:dvar_domain(Val1,NewDom1),
+ % = necessaire
+ (NewDom1 = Dom1 ->
+ % On a fini
+ true
+ ; power_real_rec(Type,Val1,N,Val,NewDom1,NewDom)).
%% Typage et calcul de la projection directe
%% Utilise aussi pour l'evaluation
power_real_interval(A,2,B) ?- !,
- square_real_interval(A,B).
+ square_real_interval(A,B).
power_real_interval(A,N,B) :-
getval(float_eval,Type)@eclipse,
integer(N),
@@ -15484,13 +15489,13 @@ power_real_interval_type(Type,A,N,B) :-
; set_lazy_domain(Type,B))).
power_real_interval(_,A,0,B) ?- !,
- protected_unify(B = 1.0).
+ protected_unify(B = 1.0).
power_real_interval(Type,A,1,B) ?- !,
-% set_lazy_domain(Type,A),
- mreal:set_typed_intervals(A,Type,[-1.0Inf..1.0Inf]),
- protected_unify(B = A).
+ % set_lazy_domain(Type,A),
+ mreal:set_typed_intervals(A,Type,[-1.0Inf..1.0Inf]),
+ protected_unify(B = A).
power_real_interval(Type,A,N,B) :-
- N > 1,
+ N > 1,
((Type == real,
check_rbox_rat(A,RatA))
->
@@ -15517,56 +15522,56 @@ power_real_interval(Type,A,N,B) :-
%% Pour simplif_node
power_real_intervals(IV,N,NIV) :-
- getval(float_eval,Type)@eclipse,
- integer(N),
- N >= 0,
- N =< 2^53,
+ getval(float_eval,Type)@eclipse,
+ integer(N),
+ N >= 0,
+ N =< 2^53,
set_lazy_domain(Tyep,NIV),
- power_interval_real(Type,IV,N,NIV).
+ power_interval_real(Type,IV,N,NIV).
power_real_interval_list(Type,[],N,[]).
power_real_interval_list(Type,[I|L],N,[NI|NL]) :-
- power_interval_real(Type,I,N,NI),
- power_real_interval_list(Type,L,N,NL).
+ power_interval_real(Type,I,N,NI),
+ power_real_interval_list(Type,L,N,NL).
power_interval_real(Type,I,N,NI) :-
- (float(I) ->
- power_real_value(Type,I,N,Low,High)
- ; min_max_inter(I,Min,Max),
- ((mod(N,2,0),
- Min < 0.0)
- ->
- (Max >= 0.0 ->
- %% I AUTOUR DE 0
- Low = 0.0,
- norm_zero_op(Type,Min,OpMin),
- NMax is max(OpMin,Max),
- power_real_max(Type,NMax,N,High)
- ; %% I NEGATIF
- norm_zero_op(Type,Max,OpMax),
- power_real_min(Type,OpMax,N,Low),
- norm_zero_op(Type,Min,OpMin),
- power_real_max(Type,OpMin,N,High))
- ; power_real_min(Type,Min,N,Low),
- power_real_max(Type,Max,N,High))),
- interval_from_bounds(Low,High,NI).
+ (float(I) ->
+ power_real_value(Type,I,N,Low,High)
+ ; min_max_inter(I,Min,Max),
+ ((mod(N,2,0),
+ Min < 0.0)
+ ->
+ (Max >= 0.0 ->
+ % I AUTOUR DE 0
+ Low = 0.0,
+ norm_zero_op(Type,Min,OpMin),
+ NMax is max(OpMin,Max),
+ power_real_max(Type,NMax,N,High)
+ ; % I NEGATIF
+ norm_zero_op(Type,Max,OpMax),
+ power_real_min(Type,OpMax,N,Low),
+ norm_zero_op(Type,Min,OpMin),
+ power_real_max(Type,OpMin,N,High))
+ ; power_real_min(Type,Min,N,Low),
+ power_real_max(Type,Max,N,High))),
+ interval_from_bounds(Low,High,NI).
power_real_value(real,Val,N,L,H) :-
- power_real_value(Val,N,L,H).
+ power_real_value(Val,N,L,H).
power_real_value(float_double,Val,N,PVal,PVal) :-
- pow_double(Val,N,PVal0),
- norm_zero(float_double,PVal0,PVal).
+ pow_double(Val,N,PVal0),
+ norm_zero(float_double,PVal0,PVal).
power_real_value(float_simple,Val,N,PVal,PVal) :-
- pow_float(Val,N,PVal0),
- norm_zero(float_simple,PVal0,PVal).
+ pow_float(Val,N,PVal0),
+ norm_zero(float_simple,PVal0,PVal).
%% N >= 1, mode real
power_real_value(Val,1,Val,Val) :- !.
power_real_value(0.0,N,0.0,0.0) :- !.
power_real_value(Val,N,L,H) :-
- pow_real_min_max(Val,N,L,H).
+ pow_real_min_max(Val,N,L,H).
pow_real_min_max(Val,N,L,H) :-
rational(Val,RatVal),
@@ -15622,75 +15627,75 @@ power_real_max(Type,Val,N,H) :-
inv_power_real_interval_list(Type,[],N,[]).
inv_power_real_interval_list(Type,[I|L],N,NL) :-
- inv_power_real_interval(Type,I,N,NL,ENL),
- inv_power_real_interval_list(Type,L,N,ENL).
+ inv_power_real_interval(Type,I,N,NL,ENL),
+ inv_power_real_interval_list(Type,L,N,ENL).
inv_power_real_interval(Type,Min..Max,N,L,EL) :- !,
- (Min >= 0.0 ->
- min_inv_power_real(Type,Min,N,Low),
- max_inv_power_real(Type,Max,N,High),
- (Low > High ->
- L = EL
- ; interval_from_bounds(Low,High,NI),
- (mod(N,2,0) ->
- norm_zero_op(Type,Low,OpLow),
- norm_zero_op(Type,High,OpHigh),
- interval_from_bounds(OpHigh,OpLow,OpNI),
- L = [OpNI,NI|EL]
- ; L = [NI|EL]))
- ; % Min < 0.0
- % N est impair car on a enleve les negatifs
- % pour les N pairs
- OpMin is -Min,
- (Max < 0.0 ->
- OpMax is -Max,
- max_inv_power_real(Type,OpMin,N,OpLow),
- min_inv_power_real(Type,OpMax,N,OpHigh),
- norm_zero_op(Type,OpLow,Low),
- norm_zero_op(Type,OpHigh,High)
- ; % Min =< 0.0 et Max >= 0.0
- max_inv_power_real(Type,OpMin,N,OpLow),
- norm_zero_op(Type,OpLow,Low),
- max_inv_power_real(Type,Max,N,High)),
- (Low > High ->
- L = EL
- ; interval_from_bounds(Low,High,NI),
- L = [NI|EL])).
+ (Min >= 0.0 ->
+ min_inv_power_real(Type,Min,N,Low),
+ max_inv_power_real(Type,Max,N,High),
+ (Low > High ->
+ L = EL
+ ; interval_from_bounds(Low,High,NI),
+ (mod(N,2,0) ->
+ norm_zero_op(Type,Low,OpLow),
+ norm_zero_op(Type,High,OpHigh),
+ interval_from_bounds(OpHigh,OpLow,OpNI),
+ L = [OpNI,NI|EL]
+ ; L = [NI|EL]))
+ ; % Min < 0.0
+ % N est impair car on a enleve les negatifs
+ % pour les N pairs
+ OpMin is -Min,
+ (Max < 0.0 ->
+ OpMax is -Max,
+ max_inv_power_real(Type,OpMin,N,OpLow),
+ min_inv_power_real(Type,OpMax,N,OpHigh),
+ norm_zero_op(Type,OpLow,Low),
+ norm_zero_op(Type,OpHigh,High)
+ ; % Min =< 0.0 et Max >= 0.0
+ max_inv_power_real(Type,OpMin,N,OpLow),
+ norm_zero_op(Type,OpLow,Low),
+ max_inv_power_real(Type,Max,N,High)),
+ (Low > High ->
+ L = EL
+ ; interval_from_bounds(Low,High,NI),
+ L = [NI|EL])).
inv_power_real_interval(Type,Val,N,L,EL) :-
- (Val < 0.0 ->
- % N est impair
- OpVal is -Val,
- min_inv_power_real(Type,OpVal,N,OpHigh),
- max_inv_power_real(Type,OpVal,N,OpLow),
- (OpLow < OpHigh ->
- L = EL
- ; norm_zero_op(Type,OpLow,Low),
- norm_zero_op(Type,OpHigh,High),
- interval_from_bounds(Low,High,NI),
- L = [NI|EL])
- ; min_inv_power_real(Type,Val,N,Low),
- max_inv_power_real(Type,Val,N,High),
- (Low > High ->
- L = EL
- ; interval_from_bounds(Low,High,NI),
- (mod(N,2,0) ->
- (number(NI) ->
- norm_zero_op(Type,NI,OpNI)
- ; norm_zero_op(Type,Low,OpLow),
- norm_zero_op(Type,High,OpHigh),
- interval_from_bounds(OpHigh,OpLow,OpNI)),
- L = [OpNI,NI|EL]
- ; L = [NI|EL]))).
+ (Val < 0.0 ->
+ % N est impair
+ OpVal is -Val,
+ min_inv_power_real(Type,OpVal,N,OpHigh),
+ max_inv_power_real(Type,OpVal,N,OpLow),
+ (OpLow < OpHigh ->
+ L = EL
+ ; norm_zero_op(Type,OpLow,Low),
+ norm_zero_op(Type,OpHigh,High),
+ interval_from_bounds(Low,High,NI),
+ L = [NI|EL])
+ ; min_inv_power_real(Type,Val,N,Low),
+ max_inv_power_real(Type,Val,N,High),
+ (Low > High ->
+ L = EL
+ ; interval_from_bounds(Low,High,NI),
+ (mod(N,2,0) ->
+ (number(NI) ->
+ norm_zero_op(Type,NI,OpNI)
+ ; norm_zero_op(Type,Low,OpLow),
+ norm_zero_op(Type,High,OpHigh),
+ interval_from_bounds(OpHigh,OpLow,OpNI)),
+ L = [OpNI,NI|EL]
+ ; L = [NI|EL]))).
inv_powN_val(float_simple,ValpN,N,InvValpN) :- !,
- InvN is 1/N,
- pow_float(ValpN,InvN,InvValpN).
+ InvN is 1/N,
+ pow_float(ValpN,InvN,InvValpN).
inv_powN_val(Type,ValpN,N,InvValpN) :-
- InvN is 1/N,
- pow_double(ValpN,InvN,InvValpN).
+ InvN is 1/N,
+ pow_double(ValpN,InvN,InvValpN).
%% Pour memoriser le resultat de check_reachable_from_power
%% entre les appels a min_inv_power_real et max_inv_power_real
@@ -15702,190 +15707,190 @@ inv_powN_val(Type,ValpN,N,InvValpN) :-
% invariant Val >= 0
check_reachable_from_pow0(real,Val,N,Unreachable,Low,High,ValpInvN) :- !,
- (getval(reachable_from_pow,(real,Val,N,Unreachable,Low,High,ValpInvN)) ->
- true
- ; inv_powN_val(real,Val,N,ValpInvN0),
- power_real_value(real,ValpInvN0,N,LVal0,HVal0),
- ((LVal0 == Val,
- HVal0 == Val)
- ->
- ValpInvN = ValpInvN0
- ; (LVal0 >= Val ->
- check_down_reachable_from_pow_real(ValpInvN0,Val,N,Unreachable,Low,High,ValpInvN)
- ; % LVal0 < Val, HVal0 =< Val
- check_up_reachable_from_pow_real(ValpInvN0,Val,N,Unreachable,Low,High,ValpInvN))),
- setval(reachable_from_pow,(real,Val,N,Unreachable,Low,High,ValpInvN))).
+ (getval(reachable_from_pow,(real,Val,N,Unreachable,Low,High,ValpInvN)) ->
+ true
+ ; inv_powN_val(real,Val,N,ValpInvN0),
+ power_real_value(real,ValpInvN0,N,LVal0,HVal0),
+ ((LVal0 == Val,
+ HVal0 == Val)
+ ->
+ ValpInvN = ValpInvN0
+ ; (LVal0 >= Val ->
+ check_down_reachable_from_pow_real(ValpInvN0,Val,N,Unreachable,Low,High,ValpInvN)
+ ; % LVal0 < Val, HVal0 =< Val
+ check_up_reachable_from_pow_real(ValpInvN0,Val,N,Unreachable,Low,High,ValpInvN))),
+ setval(reachable_from_pow,(real,Val,N,Unreachable,Low,High,ValpInvN))).
% double ou simple
check_reachable_from_pow0(Type,Val,N,Unreachable,Low,High,ValpInvN) :-
- (getval(reachable_from_pow,(Type,Val,N,Unreachable,Low,High,ValpInvN)) ->
- true
- ; inv_powN_val(Type,Val,N,ValpInvN0),
- power_real_value(Type,ValpInvN0,N,Val0,_),
- (Val0 == Val ->
- ValpInvN = ValpInvN0
- ; (Val0 > Val ->
- check_down_reachable_from_pow(Type,ValpInvN0,Val,N,Unreachable,Low,High,ValpInvN)
- ; % Val0 < Val
- check_up_reachable_from_pow(Type,ValpInvN0,Val,N,Unreachable,Low,High,ValpInvN))),
- setval(reachable_from_pow,(Type,Val,N,Unreachable,Low,High,ValpInvN))).
+ (getval(reachable_from_pow,(Type,Val,N,Unreachable,Low,High,ValpInvN)) ->
+ true
+ ; inv_powN_val(Type,Val,N,ValpInvN0),
+ power_real_value(Type,ValpInvN0,N,Val0,_),
+ (Val0 == Val ->
+ ValpInvN = ValpInvN0
+ ; (Val0 > Val ->
+ check_down_reachable_from_pow(Type,ValpInvN0,Val,N,Unreachable,Low,High,ValpInvN)
+ ; % Val0 < Val
+ check_up_reachable_from_pow(Type,ValpInvN0,Val,N,Unreachable,Low,High,ValpInvN))),
+ setval(reachable_from_pow,(Type,Val,N,Unreachable,Low,High,ValpInvN))).
check_up_reachable_from_pow_real(ValpInvN0,Val,N,Unreachable,Low,High,ValpInvN) :- !,
- % On cherche un End tel que pow(Start,N) =< Val et pow(End,N) > Val
- choose_end_narrow_pow_real(ValpInvN0,4,Val,N,ValpInvN0,Start,End),
- power_real_value(real,End,N,LEndpN,HEndpN),
- ((LEndpN == Val,
- HEndpN == Val)
- ->
- ValpInvN = End
- ; get_number_of_double_floats_between(Start,End,Nb),
- check_up_reachable_from_pow_real(Start,End,Val,N,Nb,Unreachable,Low,High,ValpInvN)).
+ % On cherche un End tel que pow(Start,N) =< Val et pow(End,N) > Val
+ choose_end_narrow_pow_real(ValpInvN0,4,Val,N,ValpInvN0,Start,End),
+ power_real_value(real,End,N,LEndpN,HEndpN),
+ ((LEndpN == Val,
+ HEndpN == Val)
+ ->
+ ValpInvN = End
+ ; get_number_of_double_floats_between(Start,End,Nb),
+ check_up_reachable_from_pow_real(Start,End,Val,N,Nb,Unreachable,Low,High,ValpInvN)).
% Delta > 0, on avance en doublant la distance a chaque fois
choose_end_narrow_pow_real(ValpInvN0,Delta,Val,N,OStart,Start,End) :-
- get_nth_double_float_from(ValpInvN0,Delta,End0),
- power_real_value(real,End0,N,_,HEnd0pN),
- ((End0 < 1.0Inf,
- HEnd0pN =< Val)
- ->
- NDelta is 2*Delta,
- choose_end_narrow_pow_real(ValpInvN0,NDelta,Val,N,End0,Start,End)
- ; Start = OStart,
- End = End0).
+ get_nth_double_float_from(ValpInvN0,Delta,End0),
+ power_real_value(real,End0,N,_,HEnd0pN),
+ ((End0 < 1.0Inf,
+ HEnd0pN =< Val)
+ ->
+ NDelta is 2*Delta,
+ choose_end_narrow_pow_real(ValpInvN0,NDelta,Val,N,End0,Start,End)
+ ; Start = OStart,
+ End = End0).
% invariant: pow(Start,N) =< Val < pow(End,N)
check_up_reachable_from_pow_real(Start,End,Val,N,Nb,Unreachable,Low,High,ValpInvN) :- !,
- (Nb == 2 ->
- Try = End
- ; Rank is (Nb-1) div 2,
- get_nth_float_from(real,Start,Rank,Try)),
- power_real_value(real,Try,N,LTrypN,HTrypN),
- ((LTrypN == Val,
- HTrypN == Val)
- ->
- ValpInvN = Try
- ; (HTrypN =< Val ->
- (Nb == 2 ->
- % Start et End sont trop petits pour atteindre Val
- Unreachable = 1,
- Low = End,
- get_next_float(real,Low,High)
- ; NNb is Nb - Rank,
- check_up_reachable_from_pow_real(Try,End,Val,N,NNb,Unreachable,Low,High,ValpInvN))
- ; % HTrypN > Val
- (Nb == 2 ->
- % Start trop petit et Try trop grand
- Unreachable = 1,
- Low = Start,
- High = Try
- ; NNb is Rank + 1,
- check_up_reachable_from_pow_real(Start,Try,Val,N,NNb,Unreachable,Low,High,ValpInvN)))).
+ (Nb == 2 ->
+ Try = End
+ ; Rank is (Nb-1) div 2,
+ get_nth_float_from(real,Start,Rank,Try)),
+ power_real_value(real,Try,N,LTrypN,HTrypN),
+ ((LTrypN == Val,
+ HTrypN == Val)
+ ->
+ ValpInvN = Try
+ ; (HTrypN =< Val ->
+ (Nb == 2 ->
+ % Start et End sont trop petits pour atteindre Val
+ Unreachable = 1,
+ Low = End,
+ get_next_float(real,Low,High)
+ ; NNb is Nb - Rank,
+ check_up_reachable_from_pow_real(Try,End,Val,N,NNb,Unreachable,Low,High,ValpInvN))
+ ; % HTrypN > Val
+ (Nb == 2 ->
+ % Start trop petit et Try trop grand
+ Unreachable = 1,
+ Low = Start,
+ High = Try
+ ; NNb is Rank + 1,
+ check_up_reachable_from_pow_real(Start,Try,Val,N,NNb,Unreachable,Low,High,ValpInvN)))).
check_down_reachable_from_pow_real(ValpInvN0,Val,N,Unreachable,Low,High,ValpInvN) :- !,
- choose_start_narrow_pow_real(ValpInvN0,-4,Val,N,ValpInvN0,Start,End),
- power_real_value(real,Start,N,LStartpN,HStartpN),
- ((LStartpN == Val,
- HStartpN == Val)
- ->
- ValpInvN = Start
- ; get_number_of_double_floats_between(Start,End,Nb),
- check_up_reachable_from_pow_real(Start,End,Val,N,Nb,Unreachable,Low,High,ValpInvN)).
+ choose_start_narrow_pow_real(ValpInvN0,-4,Val,N,ValpInvN0,Start,End),
+ power_real_value(real,Start,N,LStartpN,HStartpN),
+ ((LStartpN == Val,
+ HStartpN == Val)
+ ->
+ ValpInvN = Start
+ ; get_number_of_double_floats_between(Start,End,Nb),
+ check_up_reachable_from_pow_real(Start,End,Val,N,Nb,Unreachable,Low,High,ValpInvN)).
% Delta < 0, on recule
choose_start_narrow_pow_real(ValpInvN0,Delta,Val,N,OEnd,Start,End) :-
- get_nth_double_float_from(ValpInvN0,Delta,Start0),
- power_real_value(real,Start0,N,LStart0pN,_),
- ((Start0 >= 0.0,
- LStart0pN >= Val)
- ->
- NDelta is 2*Delta,
- choose_start_narrow_pow_real(ValpInvN0,NDelta,Val,N,Start0,Start,End)
- ; Start is max(0.0,Start0),
- End = OEnd).
+ get_nth_double_float_from(ValpInvN0,Delta,Start0),
+ power_real_value(real,Start0,N,LStart0pN,_),
+ ((Start0 >= 0.0,
+ LStart0pN >= Val)
+ ->
+ NDelta is 2*Delta,
+ choose_start_narrow_pow_real(ValpInvN0,NDelta,Val,N,Start0,Start,End)
+ ; Start is max(0.0,Start0),
+ End = OEnd).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% double ou simple
check_up_reachable_from_pow(Type,ValpInvN0,Val,N,Unreachable,Low,High,ValpInvN) :-
- % On cherche un End tel que pow(Start,N) < Val et pow(End,N) >= Val
- choose_end_narrow_pow(Type,ValpInvN0,4,Val,N,ValpInvN0,Start,End),
- power_real_value(Type,End,N,EndpN,_),
- (EndpN == Val ->
- ValpInvN = End
- ; get_number_of_floats_between(Type,Start,End,Nb),
- check_up_reachable_from_pow(Type,Start,End,Val,N,Nb,Unreachable,Low,High,ValpInvN)).
+ % On cherche un End tel que pow(Start,N) < Val et pow(End,N) >= Val
+ choose_end_narrow_pow(Type,ValpInvN0,4,Val,N,ValpInvN0,Start,End),
+ power_real_value(Type,End,N,EndpN,_),
+ (EndpN == Val ->
+ ValpInvN = End
+ ; get_number_of_floats_between(Type,Start,End,Nb),
+ check_up_reachable_from_pow(Type,Start,End,Val,N,Nb,Unreachable,Low,High,ValpInvN)).
% Delta > 0, on avance en doublant la distance a chaque fois
choose_end_narrow_pow(Type,ValpInvN0,Delta,Val,N,OStart,Start,End) :-
- get_nth_float_from(Type,ValpInvN0,Delta,End0),
- power_real_value(Type,End0,N,_,HEnd0pN),
- (HEnd0pN < Val ->
- NDelta is 2*Delta,
- choose_end_narrow_pow(Type,ValpInvN0,NDelta,Val,N,End0,Start,End)
- ; Start = OStart,
- End = End0).
+ get_nth_float_from(Type,ValpInvN0,Delta,End0),
+ power_real_value(Type,End0,N,_,HEnd0pN),
+ (HEnd0pN < Val ->
+ NDelta is 2*Delta,
+ choose_end_narrow_pow(Type,ValpInvN0,NDelta,Val,N,End0,Start,End)
+ ; Start = OStart,
+ End = End0).
% invariant: pow(Start,N) < Val < pow(End,N)
check_up_reachable_from_pow(Type,Start,End,Val,N,Nb,Unreachable,Low,High,ValpInvN) :-
- (Nb == 2 ->
- Try = End
- ; Rank is (Nb-1) div 2,
- get_nth_float_from(Type,Start,Rank,Try)),
- power_real_value(Type,Try,N,TrypN,_),
- (TrypN == Val ->
- ValpInvN = Try
- ; (TrypN < Val ->
- (Nb == 2 ->
- % Start et End sont trop petits pour atteindre Val
- Unreachable = 1,
- Low = End,
- get_next_float(Type,Low,High)
- ; NNb is Nb - Rank,
- check_up_reachable_from_pow(Type,Try,End,Val,N,NNb,Unreachable,Low,High,ValpInvN))
- ; % TrypN > Val
- (Nb == 2 ->
- % Start trop petit et Try trop grand
- Unreachable = 1,
- Low = Start,
- High = Try
- ; NNb is Rank + 1,
- check_up_reachable_from_pow(Type,Start,Try,Val,N,NNb,Unreachable,Low,High,ValpInvN)))).
+ (Nb == 2 ->
+ Try = End
+ ; Rank is (Nb-1) div 2,
+ get_nth_float_from(Type,Start,Rank,Try)),
+ power_real_value(Type,Try,N,TrypN,_),
+ (TrypN == Val ->
+ ValpInvN = Try
+ ; (TrypN < Val ->
+ (Nb == 2 ->
+ % Start et End sont trop petits pour atteindre Val
+ Unreachable = 1,
+ Low = End,
+ get_next_float(Type,Low,High)
+ ; NNb is Nb - Rank,
+ check_up_reachable_from_pow(Type,Try,End,Val,N,NNb,Unreachable,Low,High,ValpInvN))
+ ; % TrypN > Val
+ (Nb == 2 ->
+ % Start trop petit et Try trop grand
+ Unreachable = 1,
+ Low = Start,
+ High = Try
+ ; NNb is Rank + 1,
+ check_up_reachable_from_pow(Type,Start,Try,Val,N,NNb,Unreachable,Low,High,ValpInvN)))).
check_down_reachable_from_pow(Type,ValpInvN0,Val,N,Unreachable,Low,High,ValpInvN) :-
- choose_start_narrow_pow(Type,ValpInvN0,-4,Val,N,ValpInvN0,Start,End),
- power_real_value(Type,Start,N,StartpN,_),
- (StartpN == Val ->
- ValpInvN = Start
- ; get_number_of_floats_between(Type,Start,End,Nb),
- check_up_reachable_from_pow(Type,Start,End,Val,N,Nb,Unreachable,Low,High,ValpInvN)).
+ choose_start_narrow_pow(Type,ValpInvN0,-4,Val,N,ValpInvN0,Start,End),
+ power_real_value(Type,Start,N,StartpN,_),
+ (StartpN == Val ->
+ ValpInvN = Start
+ ; get_number_of_floats_between(Type,Start,End,Nb),
+ check_up_reachable_from_pow(Type,Start,End,Val,N,Nb,Unreachable,Low,High,ValpInvN)).
% Delta < 0, on recule
choose_start_narrow_pow(Type,ValpInvN0,Delta,Val,N,OEnd,Start,End) :-
- get_nth_float_from(Type,ValpInvN0,Delta,Start0),
- power_real_value(Type,Start0,N,LStart0pN,_),
- (LStart0pN > Val ->
- NDelta is 2*Delta,
- choose_start_narrow_pow(Type,ValpInvN0,NDelta,Val,N,Start0,Start,End)
- ; Start = Start0,
- End = OEnd).
+ get_nth_float_from(Type,ValpInvN0,Delta,Start0),
+ power_real_value(Type,Start0,N,LStart0pN,_),
+ (LStart0pN > Val ->
+ NDelta is 2*Delta,
+ choose_start_narrow_pow(Type,ValpInvN0,NDelta,Val,N,Start0,Start,End)
+ ; Start = Start0,
+ End = OEnd).
min_inv_power_real(Type,0.0,N,Min) :- !,
- max_inv_power_real(Type,0.0,N,Max),
- Min is -Max.
+ max_inv_power_real(Type,0.0,N,Max),
+ Min is -Max.
min_inv_power_real(real,Val,N,Min) :- !,
- check_reachable_from_pow0(Type,Val,N,Unreachable,Min0,_,HMin),
- (nonvar(Unreachable) ->
- Min = Min0
- ; %% en real HMin est le seul a atteindre Val (Err == 0)
- Min = HMin).
+ check_reachable_from_pow0(Type,Val,N,Unreachable,Min0,_,HMin),
+ (nonvar(Unreachable) ->
+ Min = Min0
+ ; % en real HMin est le seul a atteindre Val (Err == 0)
+ Min = HMin).
% double ou simple
min_inv_power_real(Type,Val,N,Min) :-
- check_reachable_from_pow0(Type,Val,N,Unreachable,Min0,Max0,HMin),
- (nonvar(Unreachable) ->
- Min = Max0
- ; get_previous_float(Type,Val,PVal),
- inv_powN_val(Type,PVal,N,LMin),
- narrow_min_inv_pow(Type,Val,N,LMin,HMin,Min)).
+ check_reachable_from_pow0(Type,Val,N,Unreachable,Min0,Max0,HMin),
+ (nonvar(Unreachable) ->
+ Min = Max0
+ ; get_previous_float(Type,Val,PVal),
+ inv_powN_val(Type,PVal,N,LMin),
+ narrow_min_inv_pow(Type,Val,N,LMin,HMin,Min)).
@@ -15895,78 +15900,78 @@ min_inv_power_real(Type,Val,N,Min) :-
% pow(Val,1/N) = HMin
% On cherche Min par dichotomie entre LMin et HMin
narrow_min_inv_pow(Type,Val,N,LMin,HMin,Min) :-
- (LMin >= HMin ->
- get_previous_float(Type,HMin,NLMin)
- % A priori pow(NLMin,1/N) < Val
- ; NLMin = LMin),
- get_number_of_floats_between(Type,NLMin,HMin,Num),
- narrow_min_inv_pow(Type,Val,N,NLMin,HMin,Num,Min).
+ (LMin >= HMin ->
+ get_previous_float(Type,HMin,NLMin)
+ % A priori pow(NLMin,1/N) < Val
+ ; NLMin = LMin),
+ get_number_of_floats_between(Type,NLMin,HMin,Num),
+ narrow_min_inv_pow(Type,Val,N,NLMin,HMin,Num,Min).
narrow_min_inv_pow(Type,Val,N,LMin,HMin,Num,Min) :-
- Rank is (Num-1) div 2,
- get_nth_float_from(Type,LMin,Rank,Min0),
- power_real_value(Type,Min0,N,Val0,_),
- (Val0 == Val ->
- (Min0 == LMin ->
- Min = LMin
- ; NNum is Rank + 1,
- narrow_min_inv_pow(Type,Val,N,LMin,Min0,NNum,Min))
- ; % Val0 < Val
- ((Num == 2,
- Rank == 0)
- ->
- Min = HMin
- ; % on ignore Min0,
- get_next_float(Type,Min0,NLMin),
- NNum is -1 + Num - Rank,
- narrow_min_inv_pow(Type,Val,N,NLMin,HMin,NNum,Min))).
+ Rank is (Num-1) div 2,
+ get_nth_float_from(Type,LMin,Rank,Min0),
+ power_real_value(Type,Min0,N,Val0,_),
+ (Val0 == Val ->
+ (Min0 == LMin ->
+ Min = LMin
+ ; NNum is Rank + 1,
+ narrow_min_inv_pow(Type,Val,N,LMin,Min0,NNum,Min))
+ ; % Val0 < Val
+ ((Num == 2,
+ Rank == 0)
+ ->
+ Min = HMin
+ ; % on ignore Min0,
+ get_next_float(Type,Min0,NLMin),
+ NNum is -1 + Num - Rank,
+ narrow_min_inv_pow(Type,Val,N,NLMin,HMin,NNum,Min))).
max_inv_power_real(_,1.0Inf,N,1.0Inf) :- !.
max_inv_power_real(real,Val,N,Max) :- !,
- check_reachable_from_pow0(real,Val,N,Unreachable,_,Max0,LMax),
- (nonvar(Unreachable) ->
- Max = Max0
- ; %% en real LMax est le seul a atteindre Val (Err == 0)
- Max = LMax).
+ check_reachable_from_pow0(real,Val,N,Unreachable,_,Max0,LMax),
+ (nonvar(Unreachable) ->
+ Max = Max0
+ ; % en real LMax est le seul a atteindre Val (Err == 0)
+ Max = LMax).
% double ou simple
max_inv_power_real(Type,Val,N,Max) :-
- check_reachable_from_pow0(Type,Val,N,Unreachable,Min0,Max0,LMax),
- (nonvar(Unreachable) ->
- Max = Min0
- ; get_next_float(Type,Val,NVal),
- inv_powN_val(Type,NVal,N,HMax),
- narrow_max_inv_pow(Type,Val,N,LMax,HMax,Max)).
+ check_reachable_from_pow0(Type,Val,N,Unreachable,Min0,Max0,LMax),
+ (nonvar(Unreachable) ->
+ Max = Min0
+ ; get_next_float(Type,Val,NVal),
+ inv_powN_val(Type,NVal,N,HMax),
+ narrow_max_inv_pow(Type,Val,N,LMax,HMax,Max)).
%% LMax atteint Val
narrow_max_inv_pow(Type,Val,N,LMax,HMax,Max) :-
- (LMax >= HMax ->
- get_next_float(Type,LMax,NHMax)
- % A priori pow(NHMax,N) > Val
- ; NHMax = HMax),
- get_number_of_floats_between(Type,LMax,NHMax,Num),
- narrow_max_inv_pow(Type,Val,N,LMax,NHMax,Num,Max).
+ (LMax >= HMax ->
+ get_next_float(Type,LMax,NHMax)
+ % A priori pow(NHMax,N) > Val
+ ; NHMax = HMax),
+ get_number_of_floats_between(Type,LMax,NHMax,Num),
+ narrow_max_inv_pow(Type,Val,N,LMax,NHMax,Num,Max).
% double ou simple
narrow_max_inv_pow(Type,Val,N,LMax,HMax,Num,Max) :-
- Rank is Num div 2,
- get_nth_float_from(Type,LMax,Rank,Max0),
- power_real_value(Type,Max0,N,Val0,_),
- (Val == Val0 ->
- (Max0 == HMax ->
- Max = Max0
- ; NNum is Num - Rank,
- narrow_max_inv_pow(Type,Val,N,Max0,HMax,NNum,Max))
- ; % Val0 > Val
- ((Num == 2,
- Rank == 1)
- ->
- Max = LMax
- ; % on ignore Max0
- get_previous_float(Type,Max0,NHMax),
- narrow_max_inv_pow(Type,Val,N,LMax,NHMax,Rank,Max))).
+ Rank is Num div 2,
+ get_nth_float_from(Type,LMax,Rank,Max0),
+ power_real_value(Type,Max0,N,Val0,_),
+ (Val == Val0 ->
+ (Max0 == HMax ->
+ Max = Max0
+ ; NNum is Num - Rank,
+ narrow_max_inv_pow(Type,Val,N,Max0,HMax,NNum,Max))
+ ; % Val0 > Val
+ ((Num == 2,
+ Rank == 1)
+ ->
+ Max = LMax
+ ; % on ignore Max0
+ get_previous_float(Type,Max0,NHMax),
+ narrow_max_inv_pow(Type,Val,N,LMax,NHMax,Rank,Max))).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
diff --git a/Src/COLIBRI/simplex_ocaml/Makefile b/Src/COLIBRI/simplex_ocaml/Makefile
index 479e6675481d628d6690b17217fdb9decaf25cca..1df2bd3e37b54863dd174cbaf2652ec1f11fc38c 100644
--- a/Src/COLIBRI/simplex_ocaml/Makefile
+++ b/Src/COLIBRI/simplex_ocaml/Makefile
@@ -23,15 +23,15 @@ windows_32:
docker:
- sudo docker build - -t simplex_ocaml_build < Dockerfile
- sudo docker run -v $(PWD)/../../..:/home/opam/build -w /home/opam/build/Src/COLIBRI/simplex_ocaml/ --env DUNE_BUILD_DIR=_build_docker simplex_ocaml_build opam exec -- make
+ docker build - -t simplex_ocaml_build < Dockerfile
+ docker run -v $(shell pwd)/../../..:/home/opam/build -w /home/opam/build/Src/COLIBRI/simplex_ocaml/ --env DUNE_BUILD_DIR=_build_docker simplex_ocaml_build opam exec -- make
cp _build_docker/default/simplex_ocaml.pl ..
cp _build_docker/default/simplex_ocaml_mod.so ../lib/v5/x86_64_linux/simplex_ocaml.so
cp _build_docker/default/simplex_ocaml_mod_v7.so ../lib/v7/x86_64_linux/simplex_ocaml.so
test_version:
- sudo docker build - -t simplex_ocaml_build < Dockerfile
- sudo docker run -v $(PWD)/../../..:/home/opam/build -w /home/opam/build/Src/COLIBRI/simplex_ocaml/ --env DUNE_BUILD_DIR=_build_docker simplex_ocaml_build opam exec -- make all_version
+ docker build - -t simplex_ocaml_build < Dockerfile
+ docker run -v $(shell pwd)/../../..:/home/opam/build -w /home/opam/build/Src/COLIBRI/simplex_ocaml/ --env DUNE_BUILD_DIR=_build_docker simplex_ocaml_build opam exec -- make all_version
clean:
dune clean
diff --git a/Src/COLIBRI/simplex_ocaml/dolmen/src/loop/typer.ml b/Src/COLIBRI/simplex_ocaml/dolmen/src/loop/typer.ml
index 4f25f387db7d72bc8661c8bbba6b55acef238be8..5662c39df41ea9f80957eb2accba971f7467e2f3 100644
--- a/Src/COLIBRI/simplex_ocaml/dolmen/src/loop/typer.ml
+++ b/Src/COLIBRI/simplex_ocaml/dolmen/src/loop/typer.ml
@@ -163,6 +163,7 @@ module Make(S : State_intf.Typer with type ty_state := ty_state) = struct
| None -> Format.fprintf fmt "<location missing>"
let report_warning (T.Warning (_env, _fragment, warn)) =
+ let aux: type a. a T.warn -> _ = fun warn ->
match warn with
| T.Unused_type_variable v -> Some (fun fmt () ->
Format.fprintf fmt
@@ -190,7 +191,19 @@ module Make(S : State_intf.Typer with type ty_state := ty_state) = struct
)
| Smtlib2_Ints.Restriction msg
+ -> Some (fun fmt () ->
+ Format.fprintf fmt
+ "This is a non-linear expression according to the smtlib spec.%a"
+ pp_hint msg
+ )
+
| Smtlib2_Reals.Restriction msg
+ -> Some (fun fmt () ->
+ Format.fprintf fmt
+ "This is a non-linear expression according to the smtlib spec.%a"
+ pp_hint msg
+ )
+
| Smtlib2_Reals_Ints.Restriction msg
-> Some (fun fmt () ->
Format.fprintf fmt
@@ -212,6 +225,8 @@ module Make(S : State_intf.Typer with type ty_state := ty_state) = struct
Format.fprintf fmt
"Unknown warning, please report upstream, ^^"
)
+ in
+ aux warn
(* Report type errors *)
(* ************************************************************************ *)
@@ -389,8 +404,10 @@ module Make(S : State_intf.Typer with type ty_state := ty_state) = struct
Format.fprintf fmt "Forbidden array sort.%a" pp_hint msg
(* Smtlib Arithmetic errors *)
- | Smtlib2_Ints.Forbidden msg
- | Smtlib2_Reals.Forbidden msg
+ | Smtlib2_Ints.Forbidden msg ->
+ Format.fprintf fmt "Non-linear expressions are forbidden by the logic.%a" pp_hint msg
+ | Smtlib2_Reals.Forbidden msg ->
+ Format.fprintf fmt "Non-linear expressions are forbidden by the logic.%a" pp_hint msg
| Smtlib2_Reals_Ints.Forbidden msg ->
Format.fprintf fmt "Non-linear expressions are forbidden by the logic.%a" pp_hint msg
| Smtlib2_Reals_Ints.Expected_arith_type ty ->
@@ -490,12 +507,18 @@ module Make(S : State_intf.Typer with type ty_state := ty_state) = struct
T._error env fragment (Warning_as_error w)
| Smtlib2_Ints.Restriction _, fragment
+ when conf.strict_typing ->
+ T._error env fragment (Warning_as_error w)
| Smtlib2_Reals.Restriction _, fragment
+ when conf.strict_typing ->
+ T._error env fragment (Warning_as_error w)
| Smtlib2_Reals_Ints.Restriction _, fragment
when conf.strict_typing ->
T._error env fragment (Warning_as_error w)
| Smtlib2_Float.Real_lit, fragment
+ when conf.strict_typing ->
+ T._error env fragment (Warning_as_error w)
| Smtlib2_Float.Bitv_extended_lit, fragment
when conf.strict_typing ->
T._error env fragment (Warning_as_error w)
diff --git a/Src/COLIBRI/simplex_ocaml/dolmen/src/standard/transformer.ml b/Src/COLIBRI/simplex_ocaml/dolmen/src/standard/transformer.ml
index bb1e003d8d64f9d71b2f9fddfbc0b8c62b9efe80..5ca22e28de3f6d18c9593e3e6884843073191ebf 100644
--- a/Src/COLIBRI/simplex_ocaml/dolmen/src/standard/transformer.ml
+++ b/Src/COLIBRI/simplex_ocaml/dolmen/src/standard/transformer.ml
@@ -65,27 +65,27 @@ module Make
let s = state checkpoint in
match token with
| None ->
- Format.dprintf "Syntax error@ with@ missing@ token@ read,@ \
- please@ report upstream,@ ^^"
+ (fun fmt -> Format.fprintf fmt "Syntax error@ with@ missing@ token@ read,@ \
+ please@ report upstream,@ ^^")
| Some tok ->
let tok_descr = Lexer.descr tok in
begin match String.trim (Ty.error s) with
| exception Not_found ->
- Format.dprintf "Missing@ syntax@ error@ message (state %d),@ \
- please@ report@ upstream,@ ^^" s
+ (fun fmt -> Format.fprintf fmt "Missing@ syntax@ error@ message (state %d),@ \
+ please@ report@ upstream,@ ^^" s)
| "<YOUR SYNTAX ERROR MESSAGE HERE>" ->
- Format.dprintf "Syntax error (state %d)@ while reading %a."
- s Tok.print tok_descr
+ (fun fmt -> Format.fprintf fmt "Syntax error (state %d)@ while reading %a."
+ s Tok.print tok_descr)
| msg ->
begin match Misc.split_on_char '\n' msg with
| error_no :: production :: l ->
let expected = String.concat " " l in
- Format.dprintf
- "@[<v>@[<hv>(%s) while parsing %s,@ read %a,@]@ @[<hov>but expected %a.@]@]"
- error_no production Tok.print tok_descr
- Format.pp_print_text expected
+ (fun fmt -> Format.fprintf fmt
+ "@[<v>@[<hv>(%s) while parsing %s,@ read %a,@]@ @[<hov>but expected %a.@]@]"
+ error_no production Tok.print tok_descr
+ Format.pp_print_text expected)
| _ ->
- Format.dprintf "Syntax error (state %d)." s
+ (fun fmt -> Format.fprintf fmt "Syntax error (state %d)." s)
end
end
@@ -129,7 +129,7 @@ module Make
raise (Loc.Lexing_error (pos, err))
| exception Parser.Error ->
let pos = Loc.of_lexbuf lexbuf in
- let msg = Format.dprintf "" in
+ let msg fmt = Format.fprintf fmt "" in
let () = k_exn () in
raise (Loc.Syntax_error (pos, msg))
| exception e ->
@@ -158,7 +158,7 @@ module Make
if not Ty.incremental then begin
(* If incremental mode is not supported, raise an error rather than
do weird things. *)
- let msg = Format.dprintf ": @[<hov>%a@]"
+ let msg fmt = Format.fprintf fmt ": @[<hov>%a@]"
Format.pp_print_text "Input format does not support incremental parsing"
in
raise (Loc.Syntax_error (Loc.of_lexbuf lexbuf, msg))
diff --git a/Src/COLIBRI/simplex_ocaml/dune-workspace b/Src/COLIBRI/simplex_ocaml/dune-workspace
index bd3920b49243a21fcb605acde4ff15471ef16636..f9fec08bd8fa58334397ce0a608777a3439c6176 100644
--- a/Src/COLIBRI/simplex_ocaml/dune-workspace
+++ b/Src/COLIBRI/simplex_ocaml/dune-workspace
@@ -1,4 +1,4 @@
(lang dune 1.0)
(context default)
-;(context (opam (switch 4.07.0) (targets native)))
+;(context (name docker) (opam (switch 4.07) (targets native)))
diff --git a/Src/COLIBRI/simplex_ocaml/parser.ml b/Src/COLIBRI/simplex_ocaml/parser.ml
index c9b0ef3ecea5aeb140c02020a4896ed68e85662d..d4066cac901c4d8e86fcbf6c4c6000c84da7025f 100644
--- a/Src/COLIBRI/simplex_ocaml/parser.ml
+++ b/Src/COLIBRI/simplex_ocaml/parser.ml
@@ -1,6 +1,6 @@
module State = struct
- (* include (Dolmen_loop.State : ((module type of Dolmen_loop.State) with type t := Dolmen_loop.State.t)) *)
- include Dolmen_loop.State
+ include (Dolmen_loop.State : ((module type of Dolmen_loop.State) with type t := Dolmen_loop.State.t))
+ (* include Dolmen_loop.State *)
type error_state = {
warns : string list;
error : [ `No_error | `Error of string ]
@@ -225,7 +225,7 @@ module Colibri_Builtins = struct
let len = List.length args in
let app env ast targs instantiation_explicit =
let l = List.length args in
- if not (Int.equal l len)
+ if not (l = len)
then
Dolmen_loop.Typer.T._error env (Dolmen_loop.Typer.T.Ast ast)
(Dolmen_loop.Typer.T.Bad_op_arity (name, [len], l))