From cd3ec4b1b740f746364d5a5e7ea19bf01700d89d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Fri, 30 Jun 2023 17:50:19 +0200
Subject: [PATCH] Import from Src:010e79722 farith:a93db57
---
Src/COLIBRI/check_ineq.pl | 2 +-
Src/COLIBRI/check_lin_expr.pl | 2 +-
Src/COLIBRI/col_solve.pl | 18 +-
Src/COLIBRI/colibri.pl | 2 +
Src/COLIBRI/mod.pl | 1 +
Src/COLIBRI/mreal.pl | 9 +-
Src/COLIBRI/ndelta.pl | 11 +-
Src/COLIBRI/new_parser_builtins.pl | 21 +
Src/COLIBRI/rbox.pl | 14 +-
Src/COLIBRI/realarith.pl | 300 +++---
Src/COLIBRI/smt_import.pl | 172 +++-
Src/COLIBRI/solve.pl | 481 ++++++----
Src/COLIBRI/solve_util.pl | 3 +
Src/COLIBRI/trigo.pl | 1351 ++++++++++++++++++++++++++++
14 files changed, 2011 insertions(+), 376 deletions(-)
create mode 100644 Src/COLIBRI/trigo.pl
diff --git a/Src/COLIBRI/check_ineq.pl b/Src/COLIBRI/check_ineq.pl
index ed15c39c5..dfb4d60c5 100644
--- a/Src/COLIBRI/check_ineq.pl
+++ b/Src/COLIBRI/check_ineq.pl
@@ -398,7 +398,7 @@ exists_diff_Rel(A,B) :-
get_suspension_data(S,goal,Goal),
(Goal = diff_real(_,X,Y);
Goal = gt_real(_,X,Y);
- fp_eq_reif(_,X,Y,Z),
+ Goal = fp_eq_reif(_,X,Y,Z),
Z == 0)),
((X,Y) == (A,B); (X,Y) == (B,A))).
diff --git a/Src/COLIBRI/check_lin_expr.pl b/Src/COLIBRI/check_lin_expr.pl
index 54b3d46c1..cab1fe108 100755
--- a/Src/COLIBRI/check_lin_expr.pl
+++ b/Src/COLIBRI/check_lin_expr.pl
@@ -18,7 +18,7 @@ check_exists_lin_expr_giving_diff_args(Type,A,B,Stop) :-
!,
(block(col_timeout(try_check_exists_lin_expr_giving_diff_args(Type,A,B,Stop),
0.5,
- %1.0Inf,
+% 1.0Inf,
true),
Tag,
(exit_block(Tag),
diff --git a/Src/COLIBRI/col_solve.pl b/Src/COLIBRI/col_solve.pl
index aad4ca1ad..c048f9582 100644
--- a/Src/COLIBRI/col_solve.pl
+++ b/Src/COLIBRI/col_solve.pl
@@ -1362,17 +1362,17 @@ smt_unit_test(TO,CI) :-
%-----------------------------------------------------------------------
%StrDir = "./QF_AUFBVFP/20210301-Alive2/",% 1/1
%------------------------------------------------------------------------
- %StrDir = "./QF_ABVFPLRA/", % 0/74
- %StrDir = "./QF_ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/",% 0/41
- %StrDir = "./QF_ABVFPLRA/20170501-Heizmann-UltimateAutomizer/",% 0/33
+ %StrDir = "./QF_ABVFPLRA/", % 1?(0)/74
+ %StrDir = "./QF_ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/",% 1?(0)/41
+ %StrDir = "./QF_ABVFPLRA/20170501-Heizmann-UltimateAutomizer/",% 1??(0)/33
%------------------------------------------------------------------------
%StrDir = "./QF_ABVFP/",
- %StrDir = "./QF_ABVFP/20170428-Liew-KLEE/", % 122/18033 TO (1 I,
+ %StrDir = "./QF_ABVFP/20170428-Liew-KLEE/", % 113/18033 TO (1 I,
% 177 u) (69 sans simplex) (cvc4 76)
- %StrDir = "./QF_ABVFP/20170501-Heizmann-UltimateAutomizer/", % 0/96 TO
+ %StrDir = "./QF_ABVFP/20170501-Heizmann-UltimateAutomizer/", % 1/96 TO
%------------------------------------------------------------------------
%StrDir = "./QF_BVFP/",
- %StrDir = "./QF_BVFP/20170428-Liew-KLEE/", % 38(40)/17156 (89 u)
+ %StrDir = "./QF_BVFP/20170428-Liew-KLEE/", % 40/17156 (89 u)
%StrDir = "./QF_BVFP/20170501-Heizmann-UltimateAutomizer/", % 0/4 TO
%StrDir = "./QF_BVFP/ramalho/", % 0/32 TO
%StrDir = "./QF_BVFP/schanda/spark/", % 1/8 TO
@@ -1385,16 +1385,16 @@ smt_unit_test(TO,CI) :-
%StrDir = "./QF_FPLRA/schanda/spark/",% 0/2 TO
%StrDir = "./QF_FPLRA/2019-Gudemann/",% 2/13 (3/13 en 2s)
%------------------------------------------------------------------------
- StrDir = "./QF_BVFPLRA/",
+ %StrDir = "./QF_BVFPLRA/",
%StrDir = "./QF_BVFPLRA/20170501-Heizmann-UltimateAutomizer/",% 0/15 TO
- %StrDir = "./QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/",% 10/152 (11 u) (12/152 en 2s)
+ %StrDir = "./QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/",% 10(9)/152 (11 u) (12/152 en 2s)
%StrDir = "./QF_BVFPLRA/2019-Gudemann/",% 0/1 TO
%------------------------------------------------------------------------
%StrDir = "./QF_FP/20170501-Heizmann-UltimateAutomizer/", % 0/2 TO
%StrDir = "./QF_FP/20190429-UltimateAutomizerSvcomp2019/", % 0/24
%StrDir = "./QF_FP/20210211-Vector/", % 0/91
%StrDir = "./QF_FP/ramalho/",% 0/38 T0 (5/38 en 2s)
- %StrDir = "./QF_FP/griggio/", % 45 TO en 24s (cvc4 90 en 60s) (65/214 en 2s)
+ StrDir = "./QF_FP/griggio/", % 44 TO en 24s (cvc4 90 en 60s) (65/214 en 2s)
%StrDir = "./QF_FP/schanda/spark/",% 5/46 TO (7 en 2s)
%StrDir = "./QF_FP/wintersteiger/", % 0/39994
%-----------------------------------------------------------------------
diff --git a/Src/COLIBRI/colibri.pl b/Src/COLIBRI/colibri.pl
index 97918421e..141e8a094 100755
--- a/Src/COLIBRI/colibri.pl
+++ b/Src/COLIBRI/colibri.pl
@@ -279,6 +279,8 @@ init_colibri :-
arith,
mod_arith,
realarith,
+ % NEW
+ trigo,
dump_constraints,
smt_import,
simplex_ocaml,
diff --git a/Src/COLIBRI/mod.pl b/Src/COLIBRI/mod.pl
index c8cac0d93..fdb8a9f17 100755
--- a/Src/COLIBRI/mod.pl
+++ b/Src/COLIBRI/mod.pl
@@ -161,6 +161,7 @@ print_mod(_{mod:congr(R,M)}, Attribute) :-
exists_congr(Num,C,Mod) :-
number(Num),
+ abs(Num) =\= 1.0Inf,
once (integer(Num);
is_float_int_number(Num)),
!,
diff --git a/Src/COLIBRI/mreal.pl b/Src/COLIBRI/mreal.pl
index ce147d3bb..b88a9085a 100755
--- a/Src/COLIBRI/mreal.pl
+++ b/Src/COLIBRI/mreal.pl
@@ -780,7 +780,8 @@ set_var_domain(V{mreal:OldDom},Type,Inter,S,Wake) ?- !,
(NInterval == OldInter ->
true
; ((NInterval = [Val],
- float(Val)) ->
+ float(Val))
+ ->
(Type == real ->
abs(Val) =\= 1.0Inf
; true),
@@ -788,7 +789,8 @@ set_var_domain(V{mreal:OldDom},Type,Inter,S,Wake) ?- !,
; arg(3,OldDom,OS),
setarg(2,OldDom,NInterval),
setarg(3,OldDom,NS),
- ((get_sign(V,SV), SV \== OSV; % on devient signe
+ ((Type == real;
+ get_sign(V,SV), SV \== OSV; % on devient signe
is_float_int_number(V);
is_not_float_int_number(V);
check_threshold(NInterval,NS,OldInter,OS))
@@ -973,7 +975,8 @@ dvar_set(Var{mreal:dom(Type,Inter0,S0)},dom(Type,Inter,S)) ?- !,
reduce_float_int(Var,Type,Inter,S,Inter1,S1),
Inter1 \== [],
((Inter1 = [Val],
- float(Val)) ->
+ float(Val))
+ ->
(Type == real ->
abs(Val) =\= 1.0Inf
; true),
diff --git a/Src/COLIBRI/ndelta.pl b/Src/COLIBRI/ndelta.pl
index b9c190bb6..8b792c085 100755
--- a/Src/COLIBRI/ndelta.pl
+++ b/Src/COLIBRI/ndelta.pl
@@ -351,7 +351,7 @@ check_pu(T1,T2) :-
call(getval(from_pu,0))@eclipse)
->
call(spy_here)@eclipse,
- writeln(output,pb_unify_from_pu)
+ writeln(output,pb_unify_from_pu(T1,T2))
; call(setval(from_pu,0))@eclipse)
; true).
@@ -1307,6 +1307,13 @@ launch_delta_bis1(X,Y,S,C) :-
% on ignore les distances nulles (pbs sinon)
%launch_delta_bis2(X,Y,S,0,CheckCycle,LoopOnly,Abort) ?- !.
launch_delta_bis2(X,Y,S0,C,CheckCycle,_LoopOnly,Abort) :-
+ ((C = LC..HC,
+ HC < LC)
+ ->
+ call(spy_here)@eclipse,
+ writeln(output,pb_launch_delta_bis2(X,Y,S0,C)),
+ fail
+ ; true),
once (getval(use_delta,1)@eclipse ->
true
; (once (get_type(X,T);
@@ -1340,7 +1347,7 @@ launch_delta_bis2(X,Y,S0,C,CheckCycle,_LoopOnly,Abort) :-
% On a reduit un arc d'une ou plusieurs boucles
% on doit verifier chaque boucle connexe
CheckCycle = 1
- % LoopOnly = 1
+ % LoopOnly = 1
; true)))
; % On n'avait pas de delta entre X et Y
(same_CC(X,Y) ->
diff --git a/Src/COLIBRI/new_parser_builtins.pl b/Src/COLIBRI/new_parser_builtins.pl
index 7e83f16d8..08d60ceac 100644
--- a/Src/COLIBRI/new_parser_builtins.pl
+++ b/Src/COLIBRI/new_parser_builtins.pl
@@ -86,15 +86,36 @@ add_new_parser_builtins :-
[real,real],real)]),
p_simplex_ocaml_add_builtins([builtin("colibri_min_fp",[],[],[m,e],[],
[fp(m,e),fp(m,e)],fp(m,e))]),
+ p_simplex_ocaml_add_builtins([builtin("colibri_sqrt",[],[],[],[],
+ [real],real)]),
p_simplex_ocaml_add_builtins([builtin("colibri_exp_real",[],[],[],[],
[real],real)]),
+ p_simplex_ocaml_add_builtins([builtin("colibri_exp",[],[],[],[],
+ [real],real)]),
p_simplex_ocaml_add_builtins([builtin("colibri_exp_fp",[],[],[m,e],[],
[fp(m,e)],fp(m,e))]),
p_simplex_ocaml_add_builtins([builtin("colibri_ln_real",[],[],[],[],
[real],real)]),
+ p_simplex_ocaml_add_builtins([builtin("colibri_ln",[],[],[],[],
+ [real],real)]),
p_simplex_ocaml_add_builtins([builtin("colibri_ln_fp",[],[],[m,e],[],
[fp(m,e)],fp(m,e))]),
+ p_simplex_ocaml_add_builtins([builtin("colibri_sin",[],[],[],[],
+ [real],real)]),
+ p_simplex_ocaml_add_builtins([builtin("colibri_cos",[],[],[],[],
+ [real],real)]),
+ p_simplex_ocaml_add_builtins([builtin("colibri_tan",[],[],[],[],
+ [real],real)]),
+ p_simplex_ocaml_add_builtins([builtin("colibri_asin",[],[],[],[],
+ [real],real)]),
+ p_simplex_ocaml_add_builtins([builtin("colibri_acos",[],[],[],[],
+ [real],real)]),
+ p_simplex_ocaml_add_builtins([builtin("colibri_atan",[],[],[],[],
+ [real],real)]),
+ p_simplex_ocaml_add_builtins([builtin("colibri_pi",[],[],[],[],
+ [],real)]),
% pour inities
+ p_simplex_ocaml_add_builtins([builtin("colibri_range",[],[],[],[],[real,real,real],real)]),
p_simplex_ocaml_add_builtins([builtin("colibri_setIntegral",[],[],[],[],
[real],real)]),
% Utilisés pour définition semantique et aussi par AdaCore
diff --git a/Src/COLIBRI/rbox.pl b/Src/COLIBRI/rbox.pl
index 6179ad97f..264ea9c9e 100755
--- a/Src/COLIBRI/rbox.pl
+++ b/Src/COLIBRI/rbox.pl
@@ -254,19 +254,26 @@ print_rbox(Var{rbox:rf(RF,NaN)}, Attribute) :-
%----------------------------------------------------------------
% Les lanceurs/observateurs de status
%----------------------------------------------------------------
+:- import is_mpi_var/4 from colibri.
launch_box(Var) :-
var(Var),
+ !,
get_priority(Prio),
set_priority(1),
((mreal:get_intervals(Var,[L..H]),
- get_next_float(float_double,L,NL),
- NL == H)
+ get_next_float(real,L,NL),
+ NL =:= H) % attention aux zeros
->
% on a bien une boite
- launch_box_prio(Var,_)
+ launch_box_prio(Var,_),
+ (is_mpi_var(Var,PV,_,_) ->
+ protected_unify(Var,PV)
+ ; true)
; true),
set_priority(Prio),
wake_if_other_scheduled(Prio).
+launch_box(_Var).
+
launch_box_rat(Var,Rat) :-
% Attention Var et Rat peuvent etre instancies
get_priority(Prio),
@@ -283,6 +290,7 @@ launch_box_rat(Var,Rat) :-
from colibri.
%% Variable deja attribuee
+:- export launch_box_prio/2.
launch_box_prio(Var{rbox:rf(RF,NaN)},Rat) ?- !,
NaN == 0,
RF \== float,
diff --git a/Src/COLIBRI/realarith.pl b/Src/COLIBRI/realarith.pl
index bb54cd527..a3833f9aa 100644
--- a/Src/COLIBRI/realarith.pl
+++ b/Src/COLIBRI/realarith.pl
@@ -1,7 +1,6 @@
%% Par defaut on utilise les simplifications
:- setval(real_simp,1)@eclipse.
-
%% ARITHMETIQUE RELLE ET FLOTTANTE SELON LA
%% VARIABLE GLOBALLE "float_eval" (real ou float_simple ou float_double )
%% PMO pour l instant seule real et float_double sont implantees mais le materiel
@@ -1751,8 +1750,6 @@ real_from_rat(Rat,R) :-
protected_unify(R,LR)
; Inter = [LR..HR],
real_vars(real,R),
- get_reif_var_depth_from_labchoice(DD),
- insert_dep_inst(inst_cstr(DD,R)),
mreal:set_typed_intervals(R,real,Inter),
add_real_cst(Rat,R),
launch_box_rat(R,Rat))).
@@ -3399,9 +3396,9 @@ is_op_real(Type,A,OpA) :-
get_saved_cstr_suspensions(LS),
member((_,op_real1(Type,X,Y)),LS),
(A == X ->
- OpA == Y
+ protected_unify(OpA,Y)
; A == Y,
- OpA == X).
+ protected_unify(OpA,X)).
check_2box(real,L) ?- !,
@@ -3686,83 +3683,85 @@ forbid_OpInf(Type,V) :-
forbid_Inf(real,V) :- !.
forbid_Inf(Type,V) :-
- (float(V) ->
- V \== 1.0Inf
- ; get_previous_float(Type,1.0Inf,Max),
- mreal:dvar_remove_greater(V,Max)).
+ (float(V) ->
+ V \== 1.0Inf
+ ; get_previous_float(Type,1.0Inf,Max),
+ mreal:dvar_remove_greater(V,Max)).
%%greatest_interval_not_absorbing(_,_,B,0.0) :- !.
greatest_interval_not_absorbing(add,Type,B,Inter) :-
- greatest_interval_not_absorbing(Type,B,Inter).
+ greatest_interval_not_absorbing(Type,B,Inter).
greatest_interval_not_absorbing(minus,Type,B,Inter) :-
- (float(B) ->
- norm_zero_op(real,B,OpB),
- greatest_interval_not_absorbing(Type,OpB,Inter)
- ; mreal:get_intervals(B,IB),
- get_float_int_status(B,FIB),%%PMO
- split_neg_pos_real(Type,FIB,IB,NegB,PosB,_),
- (last(NegB,NB) ->
- min_max_inter(NB,_,OpMinPos),
- MinPos is -OpMinPos
- ; true),
- (PosB = [PB|_] ->
- min_max_inter(PB,OpMaxNeg,_),
- MaxNeg is -OpMaxNeg
- ; true),
- greatest_interval_not_absorbing_interval(Type,MaxNeg,MinPos,Inter)).
+ (float(B) ->
+ norm_zero_op(real,B,OpB),
+ greatest_interval_not_absorbing(Type,OpB,Inter)
+ ; mreal:get_intervals(B,IB),
+ get_float_int_status(B,FIB),%%PMO
+ split_neg_pos_real(Type,FIB,IB,NegB,PosB,_),
+ (last(NegB,NB) ->
+ min_max_inter(NB,_,OpMinPos),
+ MinPos is -OpMinPos
+ ; true),
+ (PosB = [PB|_] ->
+ min_max_inter(PB,OpMaxNeg,_),
+ MaxNeg is -OpMaxNeg
+ ; true),
+ greatest_interval_not_absorbing_interval(Type,MaxNeg,MinPos,Inter)).
greatest_interval_not_absorbing(Type,B,Low..High) :-
- %% B <> 0.0
- float(B),!,
- greatest_interval_not_absorbing_val(Type,B,Low,High).
+ % B <> 0.0
+ float(B),!,
+ greatest_interval_not_absorbing_val(Type,B,Low,High).
greatest_interval_not_absorbing(Type,B,Low..High) :-
- mreal:get_intervals(B,IB),
- get_float_int_status(B,FIB),%%PMO
- split_neg_pos_real(Type,FIB,IB,NegB,PosB,_),
- (last(NegB,NB) ->
- min_max_inter(NB,_,MaxNeg)
- ; true),
- (PosB = [PB|_] ->
- min_max_inter(PB,MinPos,_)
- ; true),
- greatest_interval_not_absorbing_interval(Type,MaxNeg,MinPos,Low..High).
+ mreal:get_intervals(B,IB),
+ get_float_int_status(B,FIB),%%PMO
+ split_neg_pos_real(Type,FIB,IB,NegB,PosB,_),
+ (last(NegB,NB) ->
+ min_max_inter(NB,_,MaxNeg)
+ ; (Type == real ->
+ MaxNeg = 0.0
+ ; MaxNeg = -0.0)),
+ (PosB = [PB|_] ->
+ min_max_inter(PB,MinPos,_)
+ ; MinPos = 0.0),
+ greatest_interval_not_absorbing_interval(Type,MaxNeg,MinPos,Low..High).
greatest_interval_not_absorbing_interval(Type,MaxNeg,MinPos,Low..High) :-
- (nonvar(MaxNeg) ->
- greatest_interval_not_absorbing_val(Type,MaxNeg,L1,H1),
- (nonvar(MinPos)->
- greatest_interval_not_absorbing_val(Type,MinPos,L2,H2),
- Low is max(L1,L2),
- High is min(H1,H2)
- ; Low = L1,
- High = H1)
- ; %% nonvar(MinPos)
- greatest_interval_not_absorbing_val(Type,MinPos,Low,High)).
+ (nonvar(MaxNeg) ->
+ greatest_interval_not_absorbing_val(Type,MaxNeg,L1,H1),
+ (nonvar(MinPos)->
+ greatest_interval_not_absorbing_val(Type,MinPos,L2,H2),
+ Low is max(L1,L2),
+ High is min(H1,H2)
+ ; Low = L1,
+ High = H1)
+ ; % nonvar(MinPos)
+ greatest_interval_not_absorbing_val(Type,MinPos,Low,High)).
%% On calcule le plus grand intervalle dont toute valeur
%% absorbe B
greatest_interval_not_absorbing_val(Type,B,Low,High) :-
- AbsB is abs(B),
- floor_log2(AbsB,FL2),
- (AbsB is 2.0^FL2 ->
- %% On est sur une puissance de 2
- %% SH est le plus petit flottant positif qui absorbe AbsB
- SH is 2.0^(FL2+get_mantissa_size(Type)+1),
- get_previous_float(Type,SH,H),
- get_next_float(Type,SH,OpL),
- L is - OpL
- ; %% Entre 2 puissances de deux, le premier positif est a 2^(54+FL2)
- SH is 2.0^(FL2+get_mantissa_size(Type)+2),
- get_previous_float(Type,SH,H),
- L is -SH),
- (B > 0.0 ->
- Low = L,
- High = H
- ; Low is -H,
- High is -L).
+ AbsB is abs(B),
+ floor_log2(AbsB,FL2),
+ (AbsB is 2.0^FL2 ->
+ % On est sur une puissance de 2
+ % SH est le plus petit flottant positif qui absorbe AbsB
+ SH is 2.0^(FL2+get_mantissa_size(Type)+1),
+ get_previous_float(Type,SH,H),
+ get_next_float(Type,SH,OpL),
+ L is - OpL
+ ; % Entre 2 puissances de deux, le premier positif est a 2^(54+FL2)
+ SH is 2.0^(FL2+get_mantissa_size(Type)+2),
+ get_previous_float(Type,SH,H),
+ L is -SH),
+ (B > 0.0 ->
+ Low = L,
+ High = H
+ ; Low is -H,
+ High is -L).
add_real_zeroes(real,_,_,C) ?- !,
protected_unify(C,0.0).
@@ -3965,7 +3964,12 @@ add_real_inst0(real,A,B,C,Continue) :- !,
; (C == 0.0 ->
Stop = 1,
op_real(real,A,B)
- ; true))),
+ ; ((is_real_box(A),
+ is_real_box(B))
+ ->
+ add_real_interval(real,A,B,C),
+ launch_box(C)
+ ; true)))),
(nonvar(Stop) ->
true
; (nonvar(BoxGoal) ->
@@ -5639,7 +5643,7 @@ minus_real_int_ineqs(A,B,C) :-
op_real_int_ineqs(A,OpA) :-
getval(use_delta,1)@eclipse,
- get_sign(A,SA),
+ get_sign_real(A,SA),
!,
(SA == pos ->
% SOpA = neg
@@ -7570,8 +7574,10 @@ cast_real_int(A,B) :-
cast_real_int_type(Type,A,B).
cast_real_int_type(real,A,B) ?- !,
+ ensure_not_NaN(A),
cast_real_int(real,A,B).
cast_real_int_type(Type,A,B) :-
+ ensure_not_NaN(A),
cast_fp_int(Type,A,B).
cast_fp_int(Type,A,B) :-
@@ -7591,13 +7597,14 @@ cast_fp_int(Type,A,B) :-
cast_fp_int(Cond,Type,A,B).
cast_fp_int(0,Type,A,B) ?- !,
+ ensure_not_NaN(A),
cast_real_int(Type,A,B).
cast_fp_int(1,Type,A,B) ?- !,
uninterp(cast_fp_int,cast_fp_int,[Type],int,[A],B).
cast_fp_int(Cond,Type,A,B) :-
get_priority(Prio),
- set_priority(1),
- ((check_not_NaN(A),
+ set_priority(1),
+ ((check_not_NaN(A),
not_inf([A]))
->
protected_unify(Cond,0),
@@ -7618,6 +7625,7 @@ cast_real_int(Type,A,B) :-
get_priority(Prio),
set_priority(1),
set_lazy_domain(Type,A),
+ ensure_not_NaN(A),
save_cstr_suspensions((A,B)),
(not_inf_bounds(A) ->
% on peut dimensioner B
@@ -8247,12 +8255,22 @@ op_real_inst(real,A,B,Continue) :- !,
%launch_box_rat(A,RatA),
check_op_rat(B,A),
BoxGoal = op_real1(real,B,A)
- ; same_box_float_number_status(A,B,Box),
- Continue = 1)),
+ ; ((is_real_box(A),
+ is_mpi_var(A,PA,OPA,_))
+ ->
+ protected_unify(A,PA),
+ protected_unify(B,OPA)
+ ; ((is_mpi_var(B,PB,OPB,_),
+ is_real_box(B))
+ ->
+ protected_unify(B,PB),
+ protected_unify(A,OPB)
+ ; same_box_float_number_status(A,B,Box),
+ Continue = 1)))),
(var(Continue) ->
- check_rbox_cstrs(2,BoxGoal),
(nonvar(BoxGoal) ->
% parano
+ check_rbox_cstrs(2,BoxGoal),
check_op_rat(A,B)
; true)
; true))).
@@ -8379,7 +8397,6 @@ check_before_susp_op_real(Type,A,B) :-
(MinA >= 0 ->
AA = B, BB = A
; AA = A, BB = B),
-
my_suspend(op_real1(Type,AA,BB),2,(AA,BB)->suspend:constrained)).
@@ -10314,12 +10331,10 @@ diff_real_value(Var,Val) :-
get_sign_real(A,SA) :-
- mreal:mindomain(A,MinA),
- mreal:maxdomain(A,MaxA),
- (MinA >= 0.0 ->
- % donc 0 est pos
+ mreal:dvar_range(A,L,H) ,
+ (L >= 0.0 ->
SA = pos
- ; MaxA =< 0.0,
+ ; H =< 0.0,
SA = neg).
%% On force le signe d'un argument
@@ -10419,12 +10434,13 @@ mult_real_int_ineqs(SA,SB,A,B,C) :-
forbid_zero(real,C)
; true)),
% A revoir et generaliser
+ once (get_sign_real(C,SC);true),
((getval(use_delta,1)@eclipse,
nonvar(SA),
nonvar(SB),
+ nonvar(SC),
var(C))
->
- once (get_sign(C,SC);true),
(var(A) ->
mult_real_int_ineqs0(NZ,SC,SA,A,B,C)
; true),
@@ -10436,10 +10452,13 @@ mult_real_int_ineqs(SA,SB,A,B,C) :-
mult_real_int_ineqs0(NZ,SC,SOther,Other,Fact,C) :-
% Fact * Other = C
minus_real_interval(real,C,Other,Diff),
+ % C - Other = Diff -> C = Diff + Other
mreal:dvar_range(Diff,LD0,HD0),
+ launch_delta(Other,C,+,LD0..HD0).
+/*
(SOther \== SC ->
(SOther == pos ->
- % C neg, Other >= C
+ % C neg, Other pos, Other >= C
HD1 is min(HD0,0.0),
LD1 = LD0
; % Other neg, C pos, Other =< C
@@ -10457,13 +10476,15 @@ mult_real_int_ineqs0(NZ,SC,SOther,Other,Fact,C) :-
; rational(LD1,LD))),
(HD1 == 1.0Inf ->
HD = HD1
- ; ((HD1 == 0.0,
+ ; call(spy_here)@eclipse,
+ ((HD1 == 0.0,
nonvar(NZ),
not_unify(Fact,1.0))
->
HD is -1_1
; rational(HD1,HD))),
launch_delta(Other,C,+,LD..HD).
+*/
op_rel(<,>).
op_rel(>,<).
@@ -11096,14 +11117,6 @@ get_first_normal_div_mult(_,DN) :-
%DN is 2.0^(-1022).
DN = 2.2250738585072014e-308.
-is_op_real(V,OpV) :-
- (number(V) ->
- number(OpV),
- OpV is -V
- ; get_saved_cstr_suspensions(LS),
- member((Susp,op_real1(_,X,Y)),LS),
- ((X,Y) == (V,OpV); (X,Y) == (OpV,V))).
-
%% A * B = -A
mult_real_op_arg_res(Type,A,B,Continue) :-
(Type == real ->
@@ -12734,12 +12747,14 @@ div_real_dom(Rel12,FI1,FI2,FI,Dom1,Dom2,Dom,NewDom) :-
(Z1 == 0.0 ->
mreal:dom_intersection(dom(real,[0.0],1),Dom,NewDom,_)
; (MP1 == 1.0 ->
- mreal:dom_intersection(Dom2,Dom,NDom,_)
- ; % -1
+ %mreal:dom_intersection(Dom2,Dom,NDom,_)
+ mreal:dom_intersection(Dom1,Dom,NDom,_),
+ reduce_float_int_domain(real,FI,NDom,NewDom)
+ ; % MP1 == -1.0
op_real_intervals(Type,Inter1,-1.0Inf,[],Inter),
mreal:list_to_typed_dom(real,Inter,NDom0),
- mreal:dom_intersection(Dom,NDom0,NDom,_)),
- reduce_float_int_domain(real,FI,NDom,NewDom))
+ mreal:dom_intersection(Dom,NDom0,NDom,_),
+ reduce_float_int_domain(real,FI,NDom,NewDom)))
; ((Inter1 = [I1],
Inter2 = [I2])
->
@@ -13877,6 +13892,7 @@ div_real_ineqs(Type,A,B,C) :-
%On peut etre plus precis sur les float_int
div_real_int_ineqs(SA,SB,A,B,C) :-
+ % B <> 0,
(not_zero(C) ->
NZ = 1,
forbid_zero(real,A)
@@ -13885,12 +13901,13 @@ div_real_int_ineqs(SA,SB,A,B,C) :-
forbid_zero(real,C)
; true)),
% A revoir et generaliser
+ once (get_sign_real(C,SC);true),
((getval(use_delta,1)@eclipse,
nonvar(SA),
nonvar(SB),
+ nonvar(SC),
var(C))
->
- once (get_sign(C,SC);true),
(var(A) ->
mult_real_int_ineqs0(NZ,SC,SA,A,B,C),
% en float_int B divise A donc A=C*B
@@ -17162,7 +17179,7 @@ square_real_type(Type,A,B) :-
square_real(Type,A,B) :-
ensure_not_NaN((A,B)),
- (ground(A) ->
+ (nonvar(A) ->
mult_real_inst(Type,A,A,B,_)
; set_lazy_domain(Type,A),
set_lazy_domain(Type,B),
@@ -17810,33 +17827,33 @@ sqrt_real_interval(Type,A,B) :-
sqrt_real1(Type,A,B) :-
- get_priority(Prio),
- set_priority(1),
- sqrt_real_bis(Type,A,B),
- set_priority(Prio),
- wake_if_other_scheduled(Prio).
+ get_priority(Prio),
+ set_priority(1),
+ sqrt_real_bis(Type,A,B),
+ set_priority(Prio),
+ wake_if_other_scheduled(Prio).
sqrt_real_bis(Type,Val1,Val) :-
- (Val1 == Val ->
- (Type == real ->
+ (Val1 == Val ->
+ (Type == real ->
mreal:set_typed_intervals(Val,Type,[0.0,1.0])
; mreal:set_typed_intervals(Val,Type,[-0.0,0.0,1.0,1.0Inf]))
- ; save_cstr_suspensions((Val1,Val)),
- (Type == real ->
- (not_zero(Val1) ->
- forbid_zero(Type,Val)
- ; (not_zero(Val) ->
- forbid_zero(Type,Val1)
- ; true))
- ; %% Inutile en float
- true),
- check_exists_sqrt_real(Type,Val1,Val),
- sqrt_real_inst(Type,Val1,Val,Continue),
- (nonvar(Continue) ->
- sqrt_real_rec(Type,Val1,Val),
- check_before_susp_sqrt_real(Type,Val1,Val)
- ; true)).
+ ; save_cstr_suspensions((Val1,Val)),
+ (Type == real ->
+ (not_zero(Val1) ->
+ forbid_zero(Type,Val)
+ ; (not_zero(Val) ->
+ forbid_zero(Type,Val1)
+ ; true))
+ ; % Inutile en float
+ true),
+ check_exists_sqrt_real(Type,Val1,Val),
+ sqrt_real_inst(Type,Val1,Val,Continue),
+ (nonvar(Continue) ->
+ sqrt_real_rec(Type,Val1,Val),
+ check_before_susp_sqrt_real(Type,Val1,Val)
+ ; true)).
sqrt_real_rec(Type,Val1,Val) :-
@@ -19062,6 +19079,7 @@ refute_diff_real_with_gt_lt(Type,A,B,Stop) :-
var(Stop),
getval(use_delta,1)@eclipse,
getval(refutation_chk,0)@eclipse,
+ get_priority(Prio),
once (mreal:get_intervals(A,[L,H]),
number(L),number(H),
Var = A,Other = B;
@@ -19093,7 +19111,7 @@ refute_diff_real_with_gt_lt(Type,A,B,Stop) :-
; set_priority(1),
protected_unify(Var,H),
launch_diff_real(Type,Var,Other))
- ; set_priority(1),
+ ; set_priority(Prio),
protected_unify(Var,L),
launch_diff_real(Type,Var,Other))
; Continue = 1),
@@ -19111,7 +19129,7 @@ refute_diff_real_with_gt_lt(Type,A,B,Stop) :-
mreal:dvar_range(Var,L,H),
setval(rangeVar,(L,H)))
->
- set_priority(1),
+ set_priority(Prio),
Stop = 1,
lin_gt_real(A,B),
gt_real(Type,A,B),
@@ -19125,7 +19143,7 @@ refute_diff_real_with_gt_lt(Type,A,B,Stop) :-
mreal:dvar_range(Var,L,H),
setval(rangeVar,[ORange,(L,H)]))
->
- set_priority(1),
+ set_priority(Prio),
Stop = 1,
ORange = (L,H),
interval_from_bounds(L,H,Inter),
@@ -19133,7 +19151,7 @@ refute_diff_real_with_gt_lt(Type,A,B,Stop) :-
lin_gt_real(B,A),
gt_real(Type,B,A)
% lin_solve_var inutile ici
- ; set_priority(1),
+ ; set_priority(Prio),
getval(rangeVar,[(L1,H1),(L2,H2)]),
list_to_intervals(Type,[L1..H1,L2..H2],Intervals),
mreal:set_typed_intervals(Var,Type,Intervals),
@@ -19292,7 +19310,8 @@ diff_real_number_box(Type,A,B,_,Continue) :-
A \== B,
(float(A) ->
((float(B);
- is_real_box(B)) ->
+ is_real_box(B))
+ ->
true
; (is_removable_real_value_in_var(Type,diff,A,B,L,H) ->
mreal:set_typed_intervals(B,Type,[-1.0Inf..L,H..1.0Inf])
@@ -19314,10 +19333,17 @@ diff_real_number_box(Type,A,B,_,Continue) :-
->
% marche aussi si variables quand IA <> IB
RatA \== RatB
- ; % Si IA = IB, il y a des solutions reelles mais
- % pas de forme resolue: on garde diff_real
- % en esperant une unification provoquant le fail
- Continue = 1)
+ ; % c'est le moment de regarder si on est sur des *pi*
+ (is_mpi_var(A,PA,OPA,_) ->
+ protected_unify(A,PA),
+ (is_mpi_var(B,PB,OPB,_) ->
+ protected_unify(B,PB),
+ A \== B
+ ; % Si IA = IB, il y a des solutions reelles mais
+ % pas de forme resolue: on garde diff_real
+ % en esperant une unification provoquant le fail
+ Continue = 1)
+ ; Continue = 1))
; CheckIntersection = 1))
; (is_removable_real_value_in_var(Type,diff,B,A,L,H) ->
(float(B) ->
@@ -19735,7 +19761,15 @@ geq_real_number_box(real,A,B,Continue) ?- !,
rational(MinA) > RB)
->
true
- ; Continue = 1)
+ ; (is_mpi_var(A,PA,OPA,_) ->
+ protected_unify(A,PA),
+ (is_mpi_var(B,PB,OPB,_) ->
+ protected_unify(B,PB),
+ (A == B ->
+ true
+ ; Continue = 1)
+ ; Continue = 1)
+ ; Continue = 1))
; % A real_box et B intervalle
% on ne peut enlever que au dessus de MaxA
% et on garde la contrainte (pour le cas = ?)
@@ -20171,8 +20205,14 @@ gt_real_boxA(A,B,Continue) :-
MaxA >= MaxB,
(MinA >= MaxB ->
true
- ; % Les rbox interdisent A = B
- Continue = 1)
+ ; (is_mpi_var(A,PA,OPA,_) ->
+ protected_unify(A,PA),
+ (is_mpi_var(A,PB,OPB,_) ->
+ protected_unify(B,PB),
+ A \== B
+ ; Continue = 1)
+ ; % Les rbox interdisent A = B
+ Continue = 1))
; (is_float_number(B) ->
% MinA < A
mreal:dvar_remove_greater(B,MinA)
diff --git a/Src/COLIBRI/smt_import.pl b/Src/COLIBRI/smt_import.pl
index 425adb586..0ecd85539 100644
--- a/Src/COLIBRI/smt_import.pl
+++ b/Src/COLIBRI/smt_import.pl
@@ -1,4 +1,4 @@
-
+:- pragma(noexpand).
:- set_flag(syntax_option,iso_base_prefix).
:- set_flag(syntax_option,based_bignums).
@@ -200,11 +200,9 @@ check_overloaded(colibri_real_isIntegral,colibri_isIntegral) :- !.
check_overloaded(colibri_fp_isIntegral,colibri_isIntegral) :- !.
check_overloaded(colibri_min_int,colibri_min) :- !.
check_overloaded(colibri_min_real,colibri_min) :- !.
-%check_overloaded(colibri_min_fp,colibri_min) :- !.
check_overloaded(colibri_min_fp,'fp.min') :- !.
check_overloaded(colibri_max_int,colibri_max) :- !.
check_overloaded(colibri_max_real,colibri_max) :- !.
-%check_overloaded(colibri_max_fp,colibri_max) :- !.
check_overloaded(colibri_max_fp,'fp.max') :- !.
check_overloaded(colibri_exp_real,colibri_exp) :- !.
check_overloaded(colibri_exp_fp,colibri_exp) :- !.
@@ -362,7 +360,8 @@ term_from_dolmen_const(nan(E,S),Term) ?- !,
Term = '_'('NaN',E,S).
term_from_dolmen_const(fp(S,E,M),Term) ?- !,
Term = fp(bv("b",S),bv("b",E),bv("b",M)).
-
+term_from_dolmen_const(colibri_builtin(S,_),Term) ?- !,
+ term_string(Term,S).
build_cterm(CId,TId,CTerms,Term) :-
get_col_id(CId,TId,ColId,Chainable),
@@ -607,7 +606,11 @@ check_sat0 :-
((occurs(F,(isNaN,isNormal,isSubnormal,
isInfinite,isFinite,isZero,
isPositive,isNegative,
- uninterp,fp_eq1));
+ uninterp,fp_eq1,
+ sin_cos_value));
+ occurs(F,(sinr,cosr)),
+ arg(1,Goal,SC),
+ is_real_box(SC);
(Goal = chk_nan_reif(_,_,_,CN);
((% not_int
Goal = diff_int(V1,V2);
@@ -689,7 +692,8 @@ check_sat0 :-
; writeln(output,Diag)).
check_sat_vars :-
- not not check_sat_vars0.
+% not not check_sat_vars0.
+ check_sat_vars0.
check_sat_vars0 :-
init_real_cst,
init_seen_expr,
@@ -713,6 +717,14 @@ check_sat_vars0 :-
spy_here,
call(Goal)))),
setval(diag_code,(sat,1))@eclipse,
+
+ delayed_goals(NGoals),
+ term_variables(NGoals,GoalsVars),
+ (foreach(GV,GoalsVars),
+ foreach((GV,0,[]),NGoalsVars) do
+ trigo_no_rat(GV)),
+ once solve_cstrs_list([NGoalsVars]),
+
% pas de residue,sinon wrong_sat
suspensions(LSusp),
(foreach(Susp,LSusp) do
@@ -721,7 +733,11 @@ check_sat_vars0 :-
((occurs(F,(isNaN,isNormal,isSubnormal,
isInfinite,isFinite,isZero,
isPositive,isNegative,
- uninterp,fp_eq1));
+ uninterp,fp_eq1,
+ sin_cos_value));
+ occurs(F,(sinr,cosr)),
+ arg(1,Goal,SC),
+ is_real_box(SC);
(Goal = chk_nan_reif(_,_,_,CN);
((% not_int
Goal = diff_int(V1,V2);
@@ -791,6 +807,11 @@ get_assignment :-
% apres un check-sat
get_model :-
+ (get_model0 ->
+ true
+ ; Warn = "(warning: unknown error in get-model)",
+ writeln(error,Warn)).
+get_model0 :-
(getval(diag_code,(_,1))@eclipse;
getval(unknown_quantifier_abstraction,1)@eclipse),
!,
@@ -833,7 +854,7 @@ get_model :-
; true),
setval(use_delta,UD)@eclipse,
setval(use_simplex,US)@eclipse.
-get_model.
+get_model0.
get_initial_variable_type(V,Type0,Type) :-
(get_variable_type(V,TypeI) ->
@@ -857,6 +878,11 @@ get_initial_type(sort(Sort),Sort) :- !.
% apres un check-sat
get_value(LExpr) :-
+ (get_value0(LExpr) ->
+ true
+ ; Warn = "(warning: unknown error in get-value)",
+ writeln(error,Warn)).
+get_value0(LExpr) :-
(getval(diag_code,(_,1))@eclipse;
getval(unknown_quantifier_abstraction,1)@eclipse),
!,
@@ -925,8 +951,9 @@ get_value(LExpr) :-
as(Expr,Type) $= Res),
((nonvar(Res);
%FType == sort;
- FType == real,
- is_real_box(Res))
+ FType == real)
+ % trop strict pour la tigo !
+ %is_real_box(Res))
->
true
; ((FType == array;
@@ -939,7 +966,7 @@ get_value(LExpr) :-
; true),
setval(use_delta,UD)@eclipse,
setval(use_simplex,US)@eclipse.
-get_value(_).
+get_value0(_).
remove_all_as(Atom,Atom) :-
atomic(Atom),
@@ -1007,24 +1034,35 @@ dump_type_val(real,Val0,Val) ?- !,
dump_type_val('Real',Val0,Val).
dump_type_val('Real',Val0,NVal) ?- !,
(var(Val0) ->
- (known_real_box(Val0,SNum,SDen,Neg) ->
- (SDen == "1" ->
- concat_string([SNum,".0"],Val)
- ; concat_string(["(/ ",SNum,".0 ",SDen,".0)"],Val))
- ; mreal:dvar_range(Val0,L,H),
- rational(L,RL),
- rational(H,RH),
- protected_numerator(RL,NumL),
- protected_denominator(RL,DenL),
- (DenL == 1 ->
- concat_string([NumL,".0"],SL)
- ; concat_string(["(/ ",NumL,".0 ",DenL,".0)"],SL)),
- protected_numerator(RH,NumH),
- protected_denominator(RH,DenH),
- (DenH == 1 ->
- concat_string([NumH,".0"],SH)
- ; concat_string(["(/ ",NumH,".0 ",DenH,".0)"],SH)),
- concat_string(["(range ",SL," ",SH,")"], Val))
+ mreal:dvar_range(Val0,L,H),
+ (is_decimal_string(L) ->
+ number_string(L,SL0)
+ ; true),
+ (is_decimal_string(H) ->
+ number_string(H,SH0)
+ ; true),
+ ((nonvar(SL0),
+ nonvar(SH0))
+ ->
+ SL = SL0,
+ SH = SH0
+ ; (known_real_box(Val0,SNum,SDen,Neg) ->
+ (SDen == "1" ->
+ concat_string([SNum,".0"],Val)
+ ; concat_string(["(/ ",SNum,".0 ",SDen,".0)"],Val))
+ ; rational(L,RL),
+ rational(H,RH),
+ protected_numerator(RL,NumL),
+ protected_denominator(RL,DenL),
+ (DenL == 1 ->
+ concat_string([NumL,".0"],SL)
+ ; concat_string(["(/ ",NumL,".0 ",DenL,".0)"],SL)),
+ protected_numerator(RH,NumH),
+ protected_denominator(RH,DenH),
+ (DenH == 1 ->
+ concat_string([NumH,".0"],SH)
+ ; concat_string(["(/ ",NumH,".0 ",DenH,".0)"],SH)))),
+ concat_string(["(colibri_range ",SL," ",SH,")"], Val)
; rational(Val0,Val1),
(Val1 < 0_1 ->
Neg = 1,
@@ -1099,7 +1137,14 @@ dump_type_val(OType,Val,SVal) :-
atom_string(OType,SOType),
split_string(SOType,"|","",LSOType),
join_string(LSOType,"",SEndVal0),
- concat_string(["(as |@uc_",SEndVal0,"_",Cpt,"| ",SEndVal,")"],SVal).
+ concat_string(["(as |@uc_",SEndVal0,"_",Cpt,"| ",SEndVal,")"],
+ SVal).
+
+is_decimal_string(F) :-
+ float(F),
+ number_string(F,SF),
+ split_string(SF,"e","",L),
+ L = [_].
build_end_val_from_old_type([],[]) :- !.
build_end_val_from_old_type([OType|OTypes],[NType|NTypes]) :- !,
@@ -1532,11 +1577,12 @@ defined_smt_func(F/Ar,IArgs,Type,IExpr) :-
FIArg0 == FIArg),
protected_unify(FIArg,IArg),
OE = OE1,
- ((nonvar(IArgType),
- IArgType = sort(Sort))
- ->
- % Peuplement des valeurs de Sort
- new_sort_val(Sort)
+ (nonvar(IArgType) ->
+ findall(Sort,cgiveInstanceAndPath(sort(_),IArgType,
+ sort(Sort),_),LSs),
+ (foreach(Sort,LSs) do
+ % Peuplement de valeurs de Sort pour les diff
+ new_sort_val(Sort))
; true)),
(FType == Type ->
IExpr = IExpr0
@@ -1557,11 +1603,13 @@ defined_smt_func(F/Ar,IArgs,Type,IExpr) :-
->
NIArg = IArg
; NIArg = as(IArg,IArgType)),
- ((nonvar(IArgType),
- IArgType = sort(Sort))
- ->
- % Peuplement des valeurs de Sort
- new_sort_val(Sort)
+ call(spy_here)@eclipse,
+ (nonvar(IArgType) ->
+ findall(Sort,cgiveInstanceAndPath(sort(_),IArgType,
+ sort(Sort),_),LSs),
+ (foreach(Sort,LSs) do
+ % Peuplement de valeurs de Sort pour les diff
+ new_sort_val(Sort))
; true)),
Term =.. [F|NIArgs],
(Profile == real_int ->
@@ -2177,6 +2225,7 @@ smt_interp0('_'(FCst,EB,SB),as(Val,Type),Type) :- !,
fp_cst(FCst,EB,SB,Val,Type).
smt_interp0(true,as(1,bool),bool) :- !.
smt_interp0(false,as(0,bool),bool) :- !.
+smt_interp0(colibri_pi,as(pi,real),real) :- !.
smt_interp0(Atom,IAtom,Type) :-
atomic(Atom),
!,
@@ -2567,13 +2616,54 @@ smt_interp0(colibri_ln(A),Ln,Type) :-
(Type == real ->
Ln = ln(IA)
; Ln = fp_ln(IA)).
+
+smt_interp0(colibri_range(A,LA,HA),Exp,real) :-
+ smt_interp(A,A0,real),
+ smt_interp(LA,RL,real),
+ smt_interp(HA,RH,real),
+ Exp = as(range(A0,RL,RH),real).
+smt_interp0(colibri_sin(A),Exp,real) :-
+ smt_interp(A,IA0,real),
+ !,
+ add_as(real,IA0,IA),
+ Exp = sin(IA).
+smt_interp0(colibri_cos(A),Exp,real) :-
+ smt_interp(A,IA0,real),
+ !,
+ add_as(real,IA0,IA),
+ Exp = cos(IA).
+smt_interp0(colibri_tan(A),Exp,real) :-
+ smt_interp(A,IA0,real),
+ !,
+ add_as(Type,IA0,IA),
+ Exp = tan(IA).
+smt_interp0(colibri_asin(A),Exp,real) :-
+ smt_interp(A,IA0,real),
+ !,
+ add_as(real,IA0,IA),
+ Exp = asin(IA).
+smt_interp0(colibri_acos(A),Exp,real) :-
+ smt_interp(A,IA0,real),
+ !,
+ add_as(real,IA0,IA),
+ Exp = acos(IA).
+smt_interp0(colibri_atan(A),Exp,real) :-
+ smt_interp(A,IA0,real),
+ !,
+ add_as(Type,IA0,IA),
+ Exp = atan(IA).
+
smt_interp0(colibri_isIntegral(A),Exp,bool) :-
- smt_interp(A,IA0,Type0),
+ smt_interp(A,IA0,Type),
real_type(Type0,Type),
!,
add_as(Type,IA0,IA),
Exp = isIntegral(IA).
% uniquement pour les "real"
+smt_interp0(colibri_sqrt(A),Res,real) :- !,
+ smt_interp(A,IA0,real),
+ add_as(real,IA0,IA),
+ Res = sqrt(IA).
smt_interp0(colibri_setIntegral(A),Exp,real) :-
smt_interp(A,IA0,real),
!,
diff --git a/Src/COLIBRI/solve.pl b/Src/COLIBRI/solve.pl
index 2be984352..f66f3bf6a 100644
--- a/Src/COLIBRI/solve.pl
+++ b/Src/COLIBRI/solve.pl
@@ -4847,22 +4847,32 @@ diff_array(Type,A,const_array(TI,TE,Const)) ?- !,
diff_array(Type,A,B) :-
get_priority(P),
set_priority(1),
- Type = array(TI,TE),
- (getval(check_sat_vars,1)@eclipse ->
- % Il existe un indice commun ou les elements sont non
- % unifiables
- check_diff_array(TE,A,B)
- ; (real_type(TI,_) ->
- real_vars(TI,I)
- ; % ok pour les "sort" aussi
- int_vars(TI,I)),
- (real_type(TE,_) ->
- real_vars(TE,[EA,EB])
- ; % ok pour les "sort/array" aussi
- int_vars(TE,[EA,EB])),
- smtlib_select(Type,A,I,EA),
- smtlib_select(Type,B,I,EB),
- diff_reif(TE,_,EA,EB,1)),
+ attached_suspensions(diff_array,LS),
+ ((member(S,LS),
+ get_suspension_data(S,goal,diff_array(Type,X,Y)),
+ (A == X ->
+ B == Y
+ ; A == Y,
+ B == X))
+ ->
+ true
+ ; Type = array(TI,TE),
+ (getval(check_sat_vars,1)@eclipse ->
+ % Il existe un indice commun ou les elements sont non
+ % unifiables
+ check_diff_array(TE,A,B)
+ ; (real_type(TI,_) ->
+ real_vars(TI,I)
+ ; % ok pour les "sort" aussi
+ int_vars(TI,I)),
+ (real_type(TE,_) ->
+ real_vars(TE,[EA,EB])
+ ; % ok pour les "sort/array" aussi
+ int_vars(TE,[EA,EB])),
+ smtlib_select(Type,A,I,EA),
+ smtlib_select(Type,B,I,EB),
+ diff_reif(TE,_,EA,EB,1),
+ my_suspend(diff_array(Type,A,B),0,trigger(diff_array)))),
/*
% ANCIENNE VERSION MOINS RAPIDE QUE LES "select" !!!
; hash_create(SureA),
@@ -6254,6 +6264,10 @@ unfold_real_expr(X,_D,Cstr,Type,R) :-
exit_block(syntax)),
%insert_dep_inst(inst_cstr(D,X)),
Cstr = true.
+unfold_real_expr(pi,D,Cstr,Type,R) ?- !,
+ Type = real,
+ Cstr = true,
+ R is mpi.
unfold_real_expr(X,_,Cstr,Type,FX) :-
float(X),!,
ensure_not_NaN(FX),
@@ -7017,15 +7031,6 @@ unfold_real_expr(fp_mul(Rnd0,EA,EB),D,Cstr,Type,R) ?-
isZero(as(A,Type)),
as(0,bool)))),
D,Cond,bool,BCond)),
-/*
- unfold_int_expr(chk_nan(isNaN(as(A,Type)) or isNaN(as(B,Type)),
- as(1,bool),
- chk_nan(isInfinite(as(A,Type)),
- isZero(as(B,Type)),
- (isInfinite(as(B,Type)) and
- isZero(as(A,Type))))),
- D,Cond,bool,BCond)),
-*/
!,
(BCond == 0 ->
ensure_not_NaN((A,B,R))
@@ -7438,7 +7443,10 @@ unfold_real_expr(sqrt(EA),D,Cstr,RType,R) ?-
real_type(RType,Type),
!,
insert_dep_inst(dep(R,D,[A])),
- make_conj(CA,(ensure_not_NaN([A,R]),geq_real(Type,A,-0.0),sqrt_real(Type,A,R)),Cstr).
+ (Type == real ->
+ Z = 0.0
+ ; Z = -0.0),
+ make_conj(CA,(ensure_not_NaN([A,R]),geq_real(Type,A,Z),sqrt_real(Type,A,R)),Cstr).
unfold_real_expr(ln(EA),D,Cstr,RType,R) ?- !,
ND is D + 1,
@@ -7494,6 +7502,65 @@ unfold_real_expr(fp_exp(EA),D,Cstr,Type,R) ?-
make_conj(CNaN,CA,CNA),
make_conj(CNA,fp_exp(NaN,Type,A,R),Cstr)).
+unfold_real_expr(range(EA,LA,HA),D,Cstr,Type,A) ?-
+ ND is D + 1,
+ Type = real,
+ unfold_real_expr(EA,ND,CA,real,A),
+ unfold_real_expr(LA,ND,CL,real,L),
+ unfold_real_expr(HA,ND,CH,real,H),
+ !,
+ real_vars(real,A),
+ insert_dep_inst(dep(A,D,[L,H])),
+ unfold_int_expr(((as(A,real) $>= as(L,real)) and
+ (as(A,real) $=< as(H,real))),
+ ND,CBool,bool,1),
+ make_conj(CA,CL,CAL),
+ make_conj(CH,CAL,Cstr0),
+ make_conj(CBool,Cstr0,Cstr).
+
+unfold_real_expr(sin(EA),D,Cstr,RType,R) ?-
+ ND is D + 1,
+ unfold_real_expr(EA,ND,CA,RType,A),
+ Type = real,
+ !,
+ insert_dep_inst(dep(R,D,[A])),
+ make_conj(CA,sin_real(A,R),Cstr).
+unfold_real_expr(cos(EA),D,Cstr,RType,R) ?-
+ ND is D + 1,
+ unfold_real_expr(EA,ND,CA,RType,A),
+ Type = real,
+ !,
+ insert_dep_inst(dep(R,D,[A])),
+ make_conj(CA,cos_real(A,R),Cstr).
+unfold_real_expr(tan(EA),D,Cstr,RType,R) ?-
+ ND is D + 1,
+ unfold_real_expr(EA,ND,CA,RType,A),
+ Type = real,
+ !,
+ insert_dep_inst(dep(R,D,[A])),
+ make_conj(CA,tan_real(A,R),Cstr).
+unfold_real_expr(asin(EA),D,Cstr,RType,R) ?-
+ ND is D + 1,
+ unfold_real_expr(EA,ND,CA,RType,A),
+ Type = real,
+ !,
+ insert_dep_inst(dep(R,D,[A])),
+ make_conj(CA,asin_real(A,R),Cstr).
+unfold_real_expr(acos(EA),D,Cstr,RType,R) ?-
+ ND is D + 1,
+ unfold_real_expr(EA,ND,CA,RType,A),
+ Type = real,
+ !,
+ insert_dep_inst(dep(R,D,[A])),
+ make_conj(CA,acos_real(A,R),Cstr).
+unfold_real_expr(atan(EA),D,Cstr,RType,R) ?-
+ ND is D + 1,
+ unfold_real_expr(EA,ND,CA,RType,A),
+ Type = real,
+ !,
+ insert_dep_inst(dep(R,D,[A])),
+ make_conj(CA,atan_real(A,R),Cstr).
+
unfold_real_expr(fp_min(EA,EB),D,Cstr,Type,R) ?- !,
ND is D + 1,
unfold_real_expr(EA,ND,CA,Type,A),
@@ -7593,6 +7660,40 @@ unfold_real_expr(ite(Cond,Then,Else),D,Cstr,RType,R) ?-
unfold_real_expr(let(T,E),D,Cstr,Type,R) ?- !,
unfold_let(real,T,E,D,true,Cstr,Type,R).
+unfold_real_expr(chk_nan(Cond,Then,Else),D,Cstr,Type,R) ?-
+ ND is D + 1,
+ unfold_int_expr(Cond,ND,CC,bool,RCond),
+ unfold_real_expr(Then,ND,CT,Type,RT),
+ unfold_real_expr(Else,ND,CE,Type,RE),
+ !,
+ int_vars(bool,RCond),
+ real_vars(real,R),
+ insert_dep_inst(dep(R,D,[RCond,RT,RE])),
+ insert_dep_inst(dep(RT,D,[RCond])),
+ insert_dep_inst(dep(RE,D,[RCond])),
+ (not_unify(RT,R) ->
+ blocked_unify(RCond,0),
+ blocked_unify(RE,R),
+ make_conj(CC,CE,Cstr)
+ ; (not_unify(RE,R) ->
+ blocked_unify(RCond,1),
+ blocked_unify(RT,R),
+ make_conj(CC,CT,Cstr)
+ ; ((RT == RE,
+ CT == true,
+ CE == true)
+ ->
+ % on ignore Cond
+ blocked_unify(R,RT),
+ Cstr = true
+ ; (var(RCond) ->
+ make_conj(CC,chk_nan_reif(RCond,(RT,CT),(RE,CE),R),Cstr)
+ ; (RCond == 1 ->
+ Cstr = CT,
+ blocked_unify(R=RT)
+ ; Cstr = CE,
+ blocked_unify(R=RE)))))).
+
unfold_real_expr(uninterp(Term),D,Cstr,Type,R) ?- !,
nonvar(Term),
Term =.. [F|ArgsTypes],
@@ -7612,7 +7713,8 @@ unfold_real_expr(uninterp(Term),D,Cstr,Type,R) ?- !,
; make_conj(IC,(SetType,AC),OC))),
!,
insert_dep_inst(dep(R,D,IArgs)),
- make_conj(ACstrs,(real_vars(Type,R),uninterp_trigger(F,Types,Type,Trigger),uninterp(F,Trigger,Types,Type,IArgs,R)),Cstr).
+ make_conj(ACstrs,(real_vars(Type,R),uninterp_trigger(F,Types,Type,Trigger),
+ uninterp(F,Trigger,Types,Type,IArgs,R)),Cstr).
unfold_real_expr(Expr,_,_,_,_) :-
spy_here,
@@ -9839,6 +9941,7 @@ uninterp(F,Trigger,TypeArgs,TypeR,Args,R) :-
check_diff_array(TE,R,CR)
; not_unify(R,CR)),
only_one_neq_args_pair(TypeArgs,Args,CArgs,TA,A,CA))
+ %%TA \= array(_,_))
->
call_priority(diff_reif(TA,_Kill,A,CA,1),2)
; true))
@@ -10009,6 +10112,7 @@ chk_undef_float_to_real(Bool,TypeF,A,R) :-
; true)),
(nonvar(Bool) ->
(Bool == 0 ->
+ ensure_not_NaN(A),
float_to_real(TypeF,A,R)
; undef_float_to_real(TypeF,A,R))
; save_cstr_suspensions(A),
@@ -10025,30 +10129,13 @@ chk_undef_float_to_real(Bool,TypeF,A,R) :-
undef_float_to_real(Type,A,R) :-
uninterp_trigger(float_to_real,[Type],real,Trigger),
uninterp(float_to_real,Trigger,[Type],real,[A],R).
-/*
-undef_float_to_real(Type,A,R) :-
- get_priority(Prio),
- set_priority(1),
- (ground(A) ->
- (check_seen_expr(undef_float_to_real(Type,A),RR,Type) ->
- protected_unify(R,RR)
- ; add_seen_expr(undef_float_to_real(Type,A),R,Type))
- ; save_cstr_suspensions(A),
- get_saved_cstr_suspensions(LSusp),
- ((member((Susp,undef_float_to_real(Type,AA,RR)),LSusp),
- AA == A)
- ->
- protected_unify(R,RR)
- ; my_suspend(undef_float_to_real(Type,A,R),0,A->suspend:constrained))),
- set_priority(Prio),
- wake_if_other_scheduled(Prio).
-*/
% A est le round(Rnd,EA)
% on peut utiliser cast_real_int
chk_undef_float_to_ubv(Bool,TypeF,Size,A,R) :-
(nonvar(Bool) ->
(Bool == 0 ->
+ ensure_not_NaN(A),
cast_real_int(TypeF,A,SR),
to_intNu(Size,SR,R)
; set_lazy_domain(TypeF,A),
@@ -10068,25 +10155,6 @@ chk_undef_float_to_ubv(Bool,TypeF,Size,A,R) :-
undef_float_to_ubv(Type,Size,A,R) :-
uninterp_trigger(float_to_ubv,[Type],uint(Size),Trigger),
uninterp(float_to_ubv,Trigger,[Type],uint(Size),[A],R).
-/*
-undef_float_to_ubv(Type,Size,A,R) :-
- get_priority(Prio),
- set_priority(1),
- (ground(A) ->
- (check_seen_expr(undef_float_to_ubv(Type,Size,A),RR,Type) ->
- protected_unify(R,RR)
- ; add_seen_expr(undef_float_to_ubv(Type,Size,A),R,Type))
- ; save_cstr_suspensions(A),
- get_saved_cstr_suspensions(LSusp),
- ((member((Susp,undef_float_to_ubv(Type,Size,AA,RR)),LSusp),
- AA == A)
- ->
- protected_unify(R,RR)
- ; my_suspend(undef_float_to_ubv(Type,Size,A,R),0,
- A->suspend:constrained))),
- set_priority(Prio),
- wake_if_other_scheduled(Prio).
-*/
% A est le round(Rnd,EA)
@@ -10095,6 +10163,7 @@ undef_float_to_ubv(Type,Size,A,R) :-
chk_undef_float_to_sbv(Bool,TypeF,Size,A,R) :-
(nonvar(Bool) ->
(Bool == 0 ->
+ ensure_not_NaN(A),
cast_real_int(TypeF,A,SR),
to_intNu(Size,SR,R)
; set_lazy_domain(TypeF,A),
@@ -11592,6 +11661,8 @@ get_range(V,_,V,V).
; (local reference(new_dep))).
solve_cstrs :-
+ % la TRIGO peut désactiver le simplex
+ getval(use_simplex,US)@eclipse,
garbage_collect,
setval(nbFail,0)@eclipse,
setval(ihm_stat,0)@eclipse,
@@ -11602,10 +11673,15 @@ solve_cstrs :-
(DepConstraints \= [] ->
clear_single_inst_cstr(DepConstraints,NDepConstraints),
build_single_use_list(NDepConstraints,NSplitUseList),
- once solve_cstrs_list([NSplitUseList]),
+ (solve_cstrs_list([NSplitUseList]) ->
+ setval(use_simplex,US)@eclipse
+ ; setval(use_simplex,US)@eclipse,
+ fail),
% Si on continue dans la ligne de requete
init_dep_constraints(_NPC)
- ; true).
+ ; true),
+ attached_suspensions(diff_array,LS),
+ (foreach(S,LS) do kill_suspension(S)).
try_noNaN :-
attached_suspensions(isNaN,LS),
@@ -11637,7 +11713,7 @@ solve_cstrs_list([UseList|SplitUseList]) :-
(current_suspension(_) ->
% filtrage 3B: on rogne les bords gauche et droit des feuilles
% dans la limite du threshold (meme pour les entiers)
- narrow_leaves(UseList),
+ %narrow_leaves(UseList),
%reduce_lin_vars_bounds(UseList),
init_last_var_fail,
solve_cstrs2(UseList,[],0),
@@ -11961,8 +12037,8 @@ choose_fd_var([Adj|UseList],Var,Size,NUseList) :-
MinVars \== [],
leaf_vars([Adj|UseList],Leaves,NUseList),
leaf_var_with_max_cstr_min_dom(MinVars,[],Var,Size).
- %var_with_min_dom_max_cstr(MinVars,Var,Size).
-%% leaf_var_with_max_cstr_min_dom(MinVars,Leaves,Var,Size).
+%% var_with_min_dom_max_cstr(MinVars,Var,Size).
+% leaf_var_with_max_cstr_min_dom(MinVars,Leaves,Var,Size).
leaf_vars(UseList,Leaves,NUseList) :-
@@ -12086,6 +12162,7 @@ clean_uselist_var(V,C,Adj,UseList,NC,NAdj,NUseList) :-
filter_not_box_constrained_vars([],[]).
filter_not_box_constrained_vars([V|L],NL) :-
((no_constraint(V);
+ is_sin_cos_value(V);
is_real_box(V))
->
NL = ENL
@@ -12095,6 +12172,7 @@ filter_not_box_constrained_vars([V|L],NL) :-
filter_constrained_vars([],[]).
filter_constrained_vars([V|L],NL) :-
((no_constraint(V);
+ is_sin_cos_value(V);
is_real_box_rat(V,_))
->
NL = ENL
@@ -12224,15 +12302,15 @@ is_two_values_var(V) :-
keep_choosable_vars([],_,[]).
keep_choosable_vars([V|LV],DGVars,NLV) :-
- ((nonvar(V);
+ ((nonvar(V);
is_real_box(V);
get_type(V,T),
T = array(_,_);
not occurs(V,DGVars))
- ->
- NLV = EndNLV
- ; NLV = [V|EndNLV]),
- keep_choosable_vars(LV,DGVars,EndNLV).
+ ->
+ NLV = EndNLV
+ ; NLV = [V|EndNLV]),
+ keep_choosable_vars(LV,DGVars,EndNLV).
add_adj_to_sufficient(Adj,NAdj,Sufficient,EndSufficient) :-
@@ -12415,66 +12493,70 @@ real_int_size(V,Size) :-
sum_intervals_size_congr(ILIV,S,Mod,Size).
var_with_max_cstr_min_dom([V|LV],Var,MinSize) :-
- ((get_type(V,Type),
- Type \= array(_,_))
- ->
- (LV == [] ->
- Var = V,
- dvar_size_check_real(Type,V,MinSize)
- ; dvar_size_check_real(Type,V,Size),
- constraints_number(V,NbV),
- var_with_max_cstr_min_dom1(LV,V,Size,NbV,Var,MinSize))
- ; var_with_max_cstr_min_dom(LV,Var,MinSize)).
+ (is_sin_cos_value(V) ->
+ var_with_max_cstr_min_dom(LV,Var,MinSize)
+ ; ((get_type(V,Type),
+ Type \= array(_,_))
+ ->
+ (LV == [] ->
+ Var = V,
+ dvar_size_check_real(Type,V,MinSize)
+ ; dvar_size_check_real(Type,V,Size),
+ constraints_number(V,NbV),
+ var_with_max_cstr_min_dom1(LV,V,Size,NbV,Var,MinSize))
+ ; var_with_max_cstr_min_dom(LV,Var,MinSize))).
var_with_max_cstr_min_dom1([],V,Size,_NbV,V,Size).
var_with_max_cstr_min_dom1([VV|LV],IV,IS,INb,Var,MinSize) :-
% plus de Array
- get_type(VV,Type),
- ((is_real_box(IV),
- not is_real_box(VV))
- ->
- OV = VV,
- dvar_size_check_real(Type,VV,OS),
- constraints_number(VV,ONb)
- ; ((is_real_box(VV),
- not is_real_box(IV))
+ (is_sin_cos_value(VV) ->
+ var_with_max_cstr_min_dom1(LV,IV,IS,INb,Var,MinSize)
+ ; get_type(VV,Type),
+ ((is_real_box(IV),
+ not is_real_box(VV))
->
- OV = IV,
- OS = IS,
- ONb = INb
- ; dvar_size_check_real(Type,VV,Size),
- ((IS == 2,
- Size > 2)
+ OV = VV,
+ dvar_size_check_real(Type,VV,OS),
+ constraints_number(VV,ONb)
+ ; ((is_real_box(VV),
+ not is_real_box(IV))
->
- % priorite aux booleens
+ OV = IV,
OS = IS,
- ONb = INb,
- OV = IV
- ; constraints_number(VV,NbVar),
- ((IS > 2,
- Size == 2)
+ ONb = INb
+ ; dvar_size_check_real(Type,VV,Size),
+ ((IS == 2,
+ Size > 2)
->
% priorite aux booleens
- ONb = NbVar,
- OS = Size,
- OV = VV
- ; (NbVar > INb ->
- OV = VV,
+ OS = IS,
+ ONb = INb,
+ OV = IV
+ ; constraints_number(VV,NbVar),
+ ((IS > 2,
+ Size == 2)
+ ->
+ % priorite aux booleens
ONb = NbVar,
- OS = Size
- ; (NbVar < INb ->
- OV = IV,
- ONb = INb,
- OS = IS
- ; % NbVar == INb
- (Size < IS ->
- OV = VV,
- ONb = NbVar,
- OS = Size
- ; OV = IV,
+ OS = Size,
+ OV = VV
+ ; (NbVar > INb ->
+ OV = VV,
+ ONb = NbVar,
+ OS = Size
+ ; (NbVar < INb ->
+ OV = IV,
ONb = INb,
- OS = IS))))))),
- var_with_max_cstr_min_dom1(LV,OV,OS,ONb,Var,MinSize).
+ OS = IS
+ ; % NbVar == INb
+ (Size < IS ->
+ OV = VV,
+ ONb = NbVar,
+ OS = Size
+ ; OV = IV,
+ ONb = INb,
+ OS = IS))))))),
+ var_with_max_cstr_min_dom1(LV,OV,OS,ONb,Var,MinSize)).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% VERSIONS ADAPTEES DES PREDICATS DE "Noyau/fd_solve.pl"
@@ -12597,11 +12679,14 @@ simple_resol_int(Int) :-
mfd:dvar_remove_element(Int,1),
simple_resol_int(Int)))
; simple_resol_int1(Int))
- ; (protected_unify(Int,0);
- mfd:dvar_remove_element(Int,0),
+
+ ; Val = 0,
+ (protected_unify(Int,Val);
+ mfd:dvar_remove_element(Int,Val),
simple_resol_int(Int))),
1)
- ; true).
+ ; true).
+
simple_resol_int1(Int) :-
(var(Int) ->
@@ -12755,36 +12840,36 @@ simple_resol_float(Var) :-
( mreal:set_typed_intervals(Var,Type,[Inter])
; (once member_begin_end(Inter,IList,NIList,End,End)),
mreal:set_typed_intervals(Var,Type,NIList))
+
; % Un seul intervalle
% ESSAI BM: on regarde d'abord le min puis le max
% avant de piocher au hasard
IList = [Min0..Max0],
(Var = Min0 ;
+ Var = Max0 ;
get_next_float(Type,Min0,Min1),
- mreal:set_typed_intervals(Var,Type,[Min1..Max0]),
- (Var = Max0 ;
- get_previous_float(Type,Max0,Max1),
- mreal:set_typed_intervals(Var,Type,[Min1..Max1]),
- (nonvar(Var) ->
- true
- ; mreal:dvar_range(Var,Min,Max),
- (is_float_int_number(Var) ->
- % On reutilise le choix de la version entiere
- get_small_random_value_in_real_interval_float_int(Type,Min..Max,Value)
- ; get_small_random_value_in_real_interval(Type,Min..Max,Size,Value)),
- random_less(2,Rand),
- % On essaye Value, puis au dessus/dessous de Value
- ( Var = Value
- ; (Rand == 0 ->
- get_next_zfloat(Type,Value,Next),
- mreal:dvar_remove_smaller(Var,Next)
- ; get_previous_zfloat(Type,Value,Prev),
- mreal:dvar_remove_greater(Var,Prev))
- ; (Rand == 0 ->
- get_previous_zfloat(Type,Value,Prev),
- mreal:dvar_remove_greater(Var,Prev)
- ; get_next_zfloat(Type,Value,Next),
- mreal:dvar_remove_smaller(Var,Next))))))),
+ get_previous_float(Type,Max0,Max1),
+ mreal:set_typed_intervals(Var,Type,[Min1..Max1])),
+ (nonvar(Var) ->
+ true
+ ; mreal:dvar_range(Var,Min,Max),
+ (is_float_int_number(Var) ->
+ % On reutilise le choix de la version entiere
+ get_small_random_value_in_real_interval_float_int(Type,Min..Max,Value)
+ ; get_small_random_value_in_real_interval(Type,Min..Max,Size,Value)),
+ random_less(2,Rand),
+ % On essaye Value, puis au dessus/dessous de Value
+ ( Var = Value
+ ; (Rand == 0 ->
+ get_next_zfloat(Type,Value,Next),
+ mreal:dvar_remove_smaller(Var,Next)
+ ; get_previous_zfloat(Type,Value,Prev),
+ mreal:dvar_remove_greater(Var,Prev))
+ ; (Rand == 0 ->
+ get_previous_zfloat(Type,Value,Prev),
+ mreal:dvar_remove_greater(Var,Prev)
+ ; get_next_zfloat(Type,Value,Next),
+ mreal:dvar_remove_smaller(Var,Next))))),
my_notify_constrained(Var)
; true).
@@ -12812,6 +12897,19 @@ simple_resol_real(Var) :-
simple_resol_real_int(Var).
*/
simple_resol_real(Var) :-
+ is_trigo_no_rat(Var),
+ mpis(_,_,Pi,OpPi,Pid2,OpPid2,Pid4,OpPid4,TPid4,OTPid4),
+ Choices = [OpPi,OpPid2,OTPid4,OpPid2,OpPid4,0.0,Pid4,Pid2,TPid4,Pi],
+ member(Val,Choices),
+ protected_unify(Var,Val).
+simple_resol_real(Var) :-
+ (is_trigo_no_rat(Var) ->
+ mpis(_,_,Pi,OpPi,Pid2,OpPid2,Pid4,OpPid4,TPid4,OTPid4),
+ Choices = [OpPi,OpPid2,OTPid4,OpPid2,OpPid4,0.0,Pid4,Pid2,TPid4,Pi],
+ (foreach(Val,Choices),
+ param(Var) do
+ diff_real(real,Var,Val))
+ ; true),
(var(Var) ->
mreal:get_intervals(Var,IList),
(IList = [_,_|_] ->
@@ -12822,17 +12920,20 @@ simple_resol_real(Var) :-
mreal:set_typed_intervals(Var,real,NIList))
; % Un seul intervalle real
IList = [Min0..Max0],
+ (is_real_box(Var) ->
+ Rbox = 1
+ ; true),
((is_float_number(Var),
- not is_real_box(Var))
+ var(Rbox))
->
% ESSAI BM: on regarde d'abord le min puis le max
% avant de piocher au hasard
- (Var = Min0 ;
+ (protected_unify(Var,Min0) ;
get_next_float(real,Min0,Min1),
(Min1 == 1.0Inf ->
launch_box(Var)
; mreal:set_typed_intervals(Var,real,[Min1..Max0]),
- (Var = Max0 ;
+ (protected_unify(Var,Max0) ;
get_previous_float(real,Max0,Max1),
(Max1 == -1.0Inf ->
launch_box(Var)
@@ -12851,7 +12952,7 @@ simple_resol_real(Var) :-
get_previous_float(real,Value,PV)),
random_less(2,Rand),
% On essaye Value, puis au dessus/dessous de Value
- ( Var = Value
+ ( protected_unify(Var,Value)
; (Rand == 0 ->
set_typed_intervals(Var,real,[NV..1.0Inf])
; set_typed_intervals(Var,real,[-1.0Inf..PV]))
@@ -12860,7 +12961,8 @@ simple_resol_real(Var) :-
; set_typed_intervals(Var,real,[NV..1.0Inf])))))))
; mreal:dvar_range(Var,Min,Max),
mreal:dvar_size(Var,Size),
- (not (Size == 2,
+ (not (nonvar(Rbox);
+ Size == 2,
(Min == -1.0Inf;
Max == 1.0Inf))
->
@@ -12874,7 +12976,7 @@ simple_resol_real(Var) :-
random_less(2,Rand),
% On essaye Value, puis au dessus/dessous de Value
( % echec is +/-Inf
- Var = Value
+ protected_unify(Var,Value)
; (Rand == 0 ->
set_typed_intervals(Var,real,[NV..1.0Inf])
; set_typed_intervals(Var,real,[-1.0Inf..PV]))
@@ -12884,23 +12986,29 @@ simple_resol_real(Var) :-
; % on essaye les boites autour de Value
set_typed_intervals(Var,real,[PV..Value]),
- get_rand_rat_in_rbox(Var,PV,Value,Rat),
- (launch_box_rat(Var,Rat);
+ (not is_trigo_no_rat(Var),
+ get_rand_rat_in_rbox(Var,PV,Value,Rat),
+ launch_box_rat(Var,Rat);
launch_box(Var))
; set_typed_intervals(Var,real,[Value..NV]),
- get_rand_rat_in_rbox(Var,Value,NV,Rat),
- (launch_box_rat(Var,Rat);
+ (not is_trigo_no_rat(Var),
+ get_rand_rat_in_rbox(Var,Value,NV,Rat),
+ launch_box_rat(Var,Rat);
+ % on boucle
launch_box(Var)))
- ; (is_real_box(Var) ->
+ ; (nonvar(Rbox) ->
get_rand_rat_in_rbox(Var,Min,Max,Rat),
(launch_box_rat(Var,Rat);
- launch_box(Var))
+ trigo_no_rat(Var),
+ Ratfailed = 1)
; (Min == -1.0Inf ->
Value = Max
; Value = Min),
- ( Var = Value
+ ( protected_unify(Var,Value)
; launch_box(Var)))))),
- my_notify_constrained(Var)
+ (nonvar(Ratfailed) ->
+ true
+ ; my_notify_constrained(Var))
; true).
simple_resol_real_int(Var) :-
@@ -13115,42 +13223,43 @@ inst_rnd(Enum) :-
protected_unify(Enum,Enum0).
inst_int(Int) :-
- nonvar(Int),
- !.
+ nonvar(Int),
+ !.
inst_int(Int) :-
dvar_intervals(int,Int,IList),
- abs_min_interval(IList,Inter),
- min_max_inter(Inter,L,H),
- Size is 1 + H - L,
- mod:get_congr(Int,C,Mod),
- get_small_random_value_in_interval(Inter,Size,C,Mod,Int0),
+ abs_min_interval(IList,Inter),
+ min_max_inter(Inter,L,H),
+ Size is 1 + H - L,
+ mod:get_congr(Int,C,Mod),
+ get_small_random_value_in_interval(Inter,Size,C,Mod,Int0),
protected_unify(Int,Int0).
inst_real(Real) :-
- nonvar(Real),
- !.
+ (nonvar(Real);
+ is_real_box(Real)),
+ !.
inst_real(Real) :-
- dvar_intervals(real,Real,IList),
- abs_min_interval(IList,Inter),
- get_small_random_value_in_real_interval(real,Inter,_,Real0),
+ dvar_intervals(real,Real,IList),
+ abs_min_interval(IList,Inter),
+ get_small_random_value_in_real_interval(real,Inter,_,Real0),
protected_unify(Real,Real0).
inst_float_double(Real) :-
- nonvar(Real),
- !.
+ nonvar(Real),
+ !.
inst_float_double(Real) :-
- dvar_intervals(float_double,Real,IList),
- abs_min_interval(IList,Inter),
- get_small_random_value_in_real_interval(float_double,Inter,_,Real0),
+ dvar_intervals(float_double,Real,IList),
+ abs_min_interval(IList,Inter),
+ get_small_random_value_in_real_interval(float_double,Inter,_,Real0),
protected_unify(Real,Real0).
inst_float_simple(Real) :-
- nonvar(Real),
- !.
+ nonvar(Real),
+ !.
inst_float_simple(Real) :-
- dvar_intervals(float_simple,Real,IList),
- abs_min_interval(IList,Inter),
- get_small_random_value_in_real_interval(float_simple,Inter,_,Real0),
+ dvar_intervals(float_simple,Real,IList),
+ abs_min_interval(IList,Inter),
+ get_small_random_value_in_real_interval(float_simple,Inter,_,Real0),
protected_unify(Real,Real0).
diff --git a/Src/COLIBRI/solve_util.pl b/Src/COLIBRI/solve_util.pl
index 4d1716db4..6e269a5f5 100755
--- a/Src/COLIBRI/solve_util.pl
+++ b/Src/COLIBRI/solve_util.pl
@@ -529,6 +529,9 @@ get_small_random_value_in_real_interval(Inter,Size,Res) :-
get_small_random_value_in_real_interval(Type,Inter,Size,Res).
%%:- mode get_small_random_value_in_real_interval(++,++,++,?).
+get_small_random_value_in_real_interval(Type,LH..LH,_Size,Res) ?- !,
+ protected_unify(Res,LH).
+
get_small_random_value_in_real_interval(Type,Low..High,_Size,Res) :-
Low =< 0.0,
High >= 0.0,
diff --git a/Src/COLIBRI/trigo.pl b/Src/COLIBRI/trigo.pl
new file mode 100644
index 000000000..769f6b8ec
--- /dev/null
+++ b/Src/COLIBRI/trigo.pl
@@ -0,0 +1,1351 @@
+/*
+BUG sur:
+real_vars(real, (A, T, S, C)), tan_real(A, T), sin_real(A, S),
+ cos_real(A, C), A $: -1e-8 .. 0.0, A = -1e-8, solve_cstrs.
+-> fail
+Le pb vient de cos_real qui impose A = 0.0 ?
+le fact_periodic du cos doit rester pour tuer le sinr correspondant
+sinon le sinr_rec imposera 1 pour cos en forcant pi/2 pour NA
+et donc 0 pour A !
+*/
+
+:- setval(bpis,1).
+:- export use_bpis/0.
+use_bpis :-
+ setval(bpis,1).
+:- export no_bpis/0.
+no_bpis :-
+ setval(bpis,0).
+:- local reference(pis).
+%:- import launch_box_prio/2 from colibr.
+:- export mpis/8.
+mpis(DPi,OpDPi,Pi,OpPi,Pid2,OpPid2,Pid4,OpPid4,TPid4,OTPid4) :-
+ getval(pis,Pis),
+ (Pis == 0 ->
+ (getval(bpis,0)@colibri ->
+ DPi is 2.0*pi,
+ OpDPi is -DPi,
+ Pi is pi,
+ OpPi is -Pi,
+ Pid2 is Pi/2.0,
+ OpPid2 is -Pid2,
+ % pour sin(A)=cos(A)
+ Pid4 is Pi/4.0,
+ OPid4 is -Pid4,
+ % pour sin(-A)=cos(A)
+ TPid4 is 3*(Pi/4),
+ OTPid4 is -TPid4
+ ; % on est trop précis avec des rbox !!!!
+ % 2pi
+ DPi0 is 2.0*pi,
+ get_next_float(real,DPi0,DPi1),
+ set_intervals(real,DPi,[DPi0..DPi1]),
+ launch_box_prio(DPi,_),
+ % -2pi
+ ODPi0 is -DPi0,
+ get_previous_float(real,ODPi0,ODPi1),
+ set_intervals(real,OpDPi,[ODPi1..ODPi0]),
+ launch_box_prio(OpDPi,_),
+ % pi
+ Pi0 is pi,
+ get_next_float(real,Pi0,Pi1),
+ set_intervals(real,Pi,[Pi0..Pi1]),
+ launch_box_prio(Pi,_),
+ % -pi
+ set_lazy_domain(real,OpPi),
+ op_real_interval(real,Pi,OpPi),
+ launch_box_prio(OpPi,_),
+ % pi/2
+ Pi0d2 is Pi0/2.0,
+ Pi1d2 is Pi1/2.0,
+ set_intervals(real,Pid2,[Pi0d2..Pi1d2]),
+ launch_box_prio(Pid2,_),
+ % -pi/2
+ set_lazy_domain(real,OpPid2),
+ op_real_interval(real,Pid2,OpPid2),
+ launch_box_prio(OpPid2,_),
+ % pi/4
+ Pi0d4 is Pi0d2/2.0,
+ Pi1d4 is Pi1d2/2.0,
+ set_intervals(real,Pid4,[Pi0d4..Pi1d4]),
+ launch_box_prio(Pid4,_),
+ % -pi/4
+ set_lazy_domain(real,OpPid4),
+ op_real_interval(real,Pid4,OpPid4),
+ launch_box_prio(OpPid4,_),
+ % 3pi/4
+ set_lazy_domain(real,TPid4),
+ set_intervals(real,TPid4,[2.3561944901923448 .. 2.3561944901923453]),
+ launch_box_prio(TPid4,_),
+ % -3pi/4
+ set_lazy_domain(real,OTPid4),
+ op_real_interval(real,TPid4,OTPid4),
+ launch_box_prio(OTPid4,_)),
+ setval(pis,(DPi,OpDPi,Pi,OpPi,Pid2,OpPid2,Pid4,OpPid4,TPid4,OTPid4))
+ ; Pis = (DPi,OpDPi,Pi,OpPi,Pid2,OpPid2,Pid4,OpPid4,TPid4,OTPid4)).
+
+m2pi(DPi) :-
+ mpis(DPi0,_,_,_,_,_,_,_,_,_),
+ protected_unify(DPi0,DPi).
+mpi(Pi) :-
+ mpis(_,_,Pi0,_,_,_,_,_,_,_),
+ protected_unify(Pi0,Pi).
+moppi(OpPi) :-
+ mpis(_,_,_,OpPi0,_,_,_,_,_,_),
+ protected_unify(OpPi0,OpPi).
+mpid2(Pid2) :-
+ mpis(_,_,_,_,Pid20,_,_,_,_,_),
+ protected_unify(Pid20,Pid2).
+moppid2(OpPid2) :-
+ mpis(_,_,_,_,_,OpPid20,_,_,_,_),
+ protected_unify(OpPid20,OpPid2).
+mpid4(Pid4) :-
+ mpis(_,_,_,_,_,_,Pid40,_,_,_),
+ protected_unify(Pid40,Pid4).
+moppid4(OpPid4) :-
+ mpis(_,_,_,_,_,_,_,OpPid40,_,_),
+ protected_unify(OpPid40,OpPid4).
+mtpid4(TPid4) :-
+ mpis(_,_,_,_,_,_,_,_,TPid40,_),
+ protected_unify(TPid40,TPid4).
+moptpid4(OTPid4) :-
+ mpis(_,_,_,_,_,_,_,_,_,OTPid40),
+ protected_unify(OTPid40,OTPid4).
+
+:- export is_mis_mpi_var/4.
+is_mpi_var(V,PV,OPV,Name) :-
+ is_real_box(V),
+ mpis(DPi,OpDPi,Pi,OpPi,Pid2,OpPid2,Pid4,OpPid4,TPid4,OTPid4),
+ mreal:get_intervals(V,IV),
+ mreal:get_intervals(Pi,Ip),
+ (IV == Ip ->
+ Name = pi,
+ PV = Pi,
+ OPV = OpPi
+ ; mreal:get_intervals(OpPi,Iop),
+ (IV == Iop ->
+ Name = -pi,
+ PV = OpPi,
+ OPV = Pi
+ ; mreal:get_intervals(Pid2,Ipd2),
+ (IV == Ipd2 ->
+ Name = pi/2.0,
+ PV = Pid2,
+ OPV = OpPid2
+ ; mreal:get_intervals(OpPid2,Iopd2),
+ (IV == Iopd2 ->
+ Name = -pi/2.0,
+ PV = OpPid2,
+ OPV = Pid2
+ ; mreal:get_intervals(DPi,Idp),
+ (IV == Idp ->
+ Name = 2.0*pi,
+ PV = DPi,
+ OPV = OpDPi
+ ; mreal:get_intervals(OpDPi,IOdp),
+ (IV == IOdp ->
+ Name = -2.0*pi,
+ PV = OpDPi,
+ OPV = DPi
+ ; mreal:get_intervals(Pid4,Ipd4),
+ (IV == Ipd4 ->
+ Name = pi/4.0,
+ PV = Pid4,
+ OPV = OpPid4
+ ; mreal:get_intervals(OpPid4,Iopd4),
+ (IV == Iopd4 ->
+ Name = -pi/4.0,
+ PV = OpPid4,
+ OPV = Pid4
+ ; mreal:get_intervals(TPid4,Itpid4),
+ (IV == Itpid4 ->
+ Name = 3.0/4.0*pi,
+ PV = TPid4,
+ OPV = OTPid4
+ ; mreal:get_intervals(OTPid4,Iotpid4),
+ Name = -3.0/4.0*pi,
+ IV == Iotpid4,
+ PV = OTPid4,
+ OPV = TPid4))))))))).
+
+% pour interdire d'instancier une variable trigo par un rat
+:- local reference(trigo_no_rat).
+:- export trigo_no_rat/1.
+trigo_no_rat(A) :-
+ var(A),
+ !,
+ getval(trigo_no_rat,L),
+ (L \== 0 ->
+ (occurs(A,L) ->
+ true
+ ; setval(trigo_no_rat,[A|L]))
+ ; setval(trigo_no_rat,[A])).
+trigo_no_rat(A).
+
+:- export is_trigo_no_rat/1.
+is_trigo_no_rat(A) :-
+ var(A),
+ getval(trigo_no_rat,L)@colibri,
+ occurs(A,L).
+
+% sinus real
+sin_real(A,Sin) :-
+ get_priority(P),
+ set_priority(1),
+ no_simplex,
+ (exists_fact_periodic(sin,A,_,Res) ->
+ % on a un autre sin sur A
+ % factorisation
+ protected_unify(Sin,Res)
+ ; real_vars(real,A),
+ set_intervals(real,Sin,[-1.0 .. 1.0]),
+ % invariant
+ % sin(A+k2pi) = sin(A)
+ sin_cos_tan_period(sin,A,NA,K,Sin,Stop),
+ (var(Stop) ->
+ trigo_no_rat(Sin),
+ real_vars_have_same_sign(NA,Sin),
+ sinr0(NA,Sin)
+ ; true)),
+ set_priority(P),
+ wake_if_other_scheduled(P).
+
+real_vars_have_same_sign(0.0,0.0) ?- !.
+real_vars_have_same_sign(A,B) :-
+ (((number(A) ->
+ A =\= 0.0
+ ; true),
+ get_sign_real(A,SAB);
+ (number(B) ->
+ B =\= 0.0
+ ; true),
+ get_sign_real(B,SAB))
+ ->
+ set_sign(real,A,SAB),
+ set_sign(real,B,SAB)
+ ; suspensions(A,LS),
+ ((member(Susp,LS),
+ get_suspension_data(Susp,goal,real_vars_have_same_sign(AA,BB)),
+ (AA == A ->
+ BB == B
+ ; AA == B,
+ BB == A))
+ ->
+ true
+ ; my_suspend(real_vars_have_same_sign(A,B),0,(A,B)->suspend:constrained))).
+
+exists_fact_periodic(SCT,A,CNA,CRes) :-
+ get_cstr_suspensions(A,LS),
+ once (member(Susp,LS),
+ get_suspension_data(Susp,goal,fact_periodic(SCT,CA,CNA,CK,CKP,CRes)),
+ A == CA).
+
+
+sin_cos_tan_period(SCT,A,NA,K,Res,Stop) :-
+ trigo_no_rat(A),
+ trigo_no_rat(NA),
+ trigo_no_rat(KP),
+ trigo_no_rat(Res),
+ (((SCT == sin ->
+ inside_Pid2(A)
+ ; SCT == cos,
+ inside_Pi(A)),
+ attached_suspensions(sin_val,LSusp),
+ member(Susp,LSusp),
+ get_suspension_data(Susp,goal,sin_cos_value(AA,Sin,Cos)),
+ once (Res == Sin;
+ Res == Cos),
+ (SCT == sin ->
+ inside_Pid2(AA)
+ ; SCT == cos,
+ inside_Pi(AA)))
+ ->
+ protected_unify(A,AA),
+ protected_unify(A,NA),
+ protected_unify(K,0.0),
+ Stop = 1
+ ; true),
+ (var(Stop) ->
+ set_lazy_domain(real,NA),
+ real_vars(real_int,K),
+ save_cstr_suspensions((A,NA,Res)),
+ get_saved_cstr_suspensions(LS),
+ (foreach((S,Goal),LS),
+ param(SCT,A,NA,K,Res,Stop) do
+ ((Goal = fact_periodic(CSCT,CA,CNA,CK,CKP,CRes),
+ (A == CA;
+ Res == CRes))
+ ->
+ ((A == CA,
+ occurs(SCT,(sin,cos)),
+ occurs(CSCT,(sin,cos)))
+ ->
+ % on a un autre sin/cos sur A
+ % meme periode, factorisation sur NA et K
+ protected_unify(NA,CNA),
+ protected_unify(K,CK),
+ protected_unify(KP,CKP),
+ (CSCT == SCT ->
+ Stop = 1,
+ protected_unify(Res,CRes)
+ ; true)
+ ; ((SCT == tan,
+ CSCT == SCT,
+ (A == CA;
+ Res == CRes))
+ ->
+ % tan,tan
+ ((A == CA;
+ (inside_Pid2(A),
+ inside_Pid2(CA)))
+ ->
+ Stop = 1,
+ protected_unify(A,CA),
+ protected_unify(K,CK),
+ protected_unify(K,0.0),
+ protected_unify(Res,CRes)
+ ; protected_unify(NA,CNA),
+ protected_unify(Res,CRes))
+ ; true))
+ ; true))
+ ; true),
+ (nonvar(Stop) ->
+ true
+ ; real_vars(real,A),
+ real_vars(real_int,K),
+ set_lazy_domain(real,NA),
+ % periodicité:
+ % sin et cos : sin(A+K*2pi) = sin(A)
+ % tan(A + pi) = tan(pi)
+ % pour forcer le plus grand K ?
+ mpis(DPi,_,Pi,OpPi,Pid2,OpPid2,_,_,_,_),
+ ((mreal:dvar_range(A,LA,HA),
+ (SCT \== tan ->
+ % sin, cos
+ VMin = OpPi,
+ VMax = Pi
+ ; VMin = OpPid2,
+ VMax = Pid2),
+ mreal:dvar_range(VMax,_,Max),
+ mreal:dvar_range(VMin,Min,_),
+ LA >= Min,
+ HA =< Max)
+ ->
+ protected_unify(K,0.0),
+ protected_unify(KP,0.0),
+ protected_unify(A,NA),
+ (SCT == tan ->
+ true
+ ; NStop = 1)
+ ; true),
+ (nonvar(NStop) ->
+ true
+ ; (SCT == tan ->
+ NMax = Pid2,
+ NOpMax = OpPid2,
+ set_lazy_domain(real,Res),
+ Period = Pi
+ ; set_intervals(real,Res,[-1.0 .. 1.0]),
+ NMax = Pi,
+ NOpMax = OpPi,
+ Period = DPi),
+ launch_geq_real(real,NA,NOpMax),
+ launch_geq_real(real,NMax,NA),
+ mult_real(real,K,Period,KP),
+ add_real(real,NA,KP,A),
+ fact_periodic(SCT,A,NA,K,KP,Res))).
+
+
+/*
+fact_periodic(SCT,A,NA,K,KP,Res) :-
+ SCT == sin,
+ once (K == 0.0;
+ KP == 0.0),
+ !,
+ call_priority((protected_unify(A,NA),
+ protected_unify(K,0.0),
+ protected_unify(KP,0.0)),
+ 1).
+*/
+fact_periodic(SCT,A,NA,K,KP,Res) :-
+ get_priority(P),
+ set_priority(1),
+ trigo_no_rat(A),
+ trigo_no_rat(NA),
+ trigo_no_rat(KP),
+ trigo_no_rat(Res),
+ ((SCT == sin,
+ (A \== 0.0,
+ get_sign_real(A,SA);
+ NA \== 0.0,
+ get_sign_real(NA,SA);
+ Res \== 0.0,
+ get_sign_real(Res,SA)))
+ ->
+ set_sign(real,A,SA),
+ set_sign(real,NA,SA),
+ set_sign(real,Res,SA)
+ ; true),
+ ((mreal:dvar_range(A,LA,HA),
+ mpis(_,_,Pi,OpPi,Pid2,OpPid2,_,_,_,_),
+ (SCT \== tan ->
+ % sin, cos
+ VMin = OpPi,
+ VMax = Pi
+ ; VMin = OpPid2,
+ VMax = Pid2),
+ mreal:dvar_range(VMax,_,Max),
+ mreal:dvar_range(VMin,Min,_),
+ LA >= Min,
+ HA =< Max)
+ ->
+ protected_unify(K,0.0)
+ ; true),
+ (K == 0.0 ->
+ protected_unify(A,NA),
+ protected_unify(KP,0.0)
+ ; true),
+ ((SCT == tan; % trace pour atan
+ var(A), % trace pour sin/cos si pas de sin_cos_value
+ not is_real_box(A))
+ ->
+ periodic_not_accurate(SCT,A,Res,Stop),
+ (nonvar(Stop) ->
+ protected_unify(K,0.0),
+ protected_unify(KP,0.0)
+ ; Continue = 1),
+ (nonvar(Continue) ->
+ (exists_fact_periodic(SCT,A,CNA,CRes) ->
+ protected_unify(Res,CRes),
+ protected_unify(NA,CNA)
+ ; my_suspend(fact_periodic(SCT,A,NA,K,KP,Res),0,(A,NA,K,KP,Res)->
+ suspend:constrained))
+ ; true)
+ ; true),
+ set_priority(P),
+ wake_if_other_scheduled(P).
+
+
+periodic_not_accurate(cos,A,Cos,Stop) ?- !,
+ % imprécision de cos
+ mreal:dvar_range(A,L,H),
+ ((L >= -1e-8,
+ H =< 1e-8)
+ ->
+ Stop = 1,
+ get_previous_float(real,1.0,L1),
+ get_next_float(real,1.0,H1),
+ set_intervals(real,Cos,[L1..H1])
+ ; true).
+periodic_not_accurate(_,_,_,_Stop).
+
+sinr0(A,Sin) :-
+ % si A : -p1..0 -> sin(A) = -sin(-A)
+ % si A : 0..pi -> sin(A) = -sin(-A)
+ sinr(A,Sin).
+sinr(0.0,Sin) ?- !,
+ protected_unify(Sin,0.0).
+sinr(A,0.0) ?- !,
+ (A == 0.0 ->
+ true
+ ; mreal:dvar_range(A,LA,HA),
+ mpis(_,_,Pi,OpPi,_,_,_,_,_,_),
+ mreal:get_intervals(Pi,IAp),
+ mreal:get_intervals(OpPi,IAn),
+ append(IAn,IAp,IA),
+ (exists_diff_Rel(A,0.0) ->
+ set_intervals(real,A,IA),
+ %int_vars(bool,Bool),
+ set_intervals(int,Bool,[0,1]),
+ insert_dep_inst(inst_cstr(0,Bool)),
+ isNegative(real,A,Bool),
+ chk_nan_reif(Bool,(OpPi,true),(Pi,true),A)
+ ; set_intervals(real,A,[0.0|IA]),
+ %int_vars(bool,Bool),
+ set_intervals(int,Bool,[0,1]),
+ insert_dep_inst(inst_cstr(0,Bool)),
+ isZero(real,A,Bool),
+ chk_nan_reif(Bool,
+ (0.0,true),
+ (A,
+ (%int_vars(bool,Bool1),
+ set_intervals(int,Bool1,[0,1]),
+ insert_dep_inst(inst_cstr(0,Bool1)),
+ isNegative(real,A,Bool1),
+ chk_nan_reif(Bool1,(OpPi,true),(Pi,true),A))),
+ A))).
+sinr(A,1.0) ?- !,
+ Pid2 is mpid2,
+ %mreal:get_intervals(Pid2,IA),
+ %set_intervals(real,A,IA).
+ protected_unify(A,Pid2).
+sinr(A,-1.0) ?- !,
+ OpPid2 is moppid2,
+ %mreal:get_intervals(OpPid2,IA),
+ %set_intervals(real,A,IA).
+ protected_unify(A,OpPid2).
+sinr(A,Sin) :-
+ (number(A),
+ RA = A;
+ is_real_box_rat(A,RA)),
+ !,
+ sin_cos_val(RA,Sin,_).
+sinr(A,Sin) :-
+ is_real_box(A),
+ mpis(_,_,Pi,OpPi,Pid2,OpPid2,Pid4,_,TPid4,OpTPid4),
+ mreal:get_intervals(A,IA),
+ mreal:get_intervals(Pi,IPi),
+ mreal:get_intervals(OpPi,IOpPi),
+ ((IA == IPi,
+ NA = Pi;
+ IA == IOpPi,
+ NA = OpPi)
+ ->
+ !,
+ protected_unify(A,NA),
+ protected_unify(Sin,0.0)
+ ; mreal:get_intervals(Pid2,IPid2),
+ (IA == IPid2 ->
+ !,
+ protected_unify(A,Pid2),
+ protected_unify(Sin,1.0)
+ ; mreal:get_intervals(OpPid2,IOpPid2),
+ (IA == IOpPid2 ->
+ !,
+ protected_unify(A,OpPid2),
+ protected_unify(Sin,-1.0)
+ ; mreal:get_intervals(Pid4,IPid4),
+ (IA == IPid4 ->
+ !,
+ sin_cos_val(A,Sin,Sin)
+ ; mreal:get_intervals(OpTPid4,IOTPd4),
+ IA == IOTPd4,
+ !,
+ sin_cos_val(A,Sin,Sin))))).
+sinr(A,Sin) :-
+ get_priority(P),
+ set_priority(1),
+ save_cstr_suspensions((A,Sin)),
+ ((get_sign_real(A,SA);
+ get_sign_real(Sin,SA))
+ ->
+ set_sign(real,A,SA),
+ set_sign(real,Sin,SA),
+ (SA == pos ->
+ % 0 .. A .. pi
+ mpi(Pi),
+ geq_real(real,A,0.0),
+ geq_real(real,Pi,A)
+ ; % neg: -pi .. A .. 0
+ moppi(OpPi),
+ geq_real(real,A,OpPi),
+ geq_real(real,0.0,A))
+ ; true),
+ (A == Sin ->
+ set_intervals(real,A,[-2.1498999999999986e-8..2.1498999999999986e-8])
+ ; true),
+ (inside_Pid2(A) ->
+ InPid2 = 1
+ ; true),
+ (nonvar(InPid2) ->
+ attached_suspensions(sin_val,LS),
+ ((member(SV,LS),
+ get_suspension_data(SV,goal,sin_cos_value(AA0,SA0,_)),
+ Sin == SA0,
+ inside_Pid2(AA0))
+ ->
+ protected_unify(A,AA0)
+ ; true)
+ ; true),
+ get_saved_cstr_suspensions(LSusp),
+ (foreach((S,Goal),LSusp),
+ param(A,Sin,InPid2,SeqC) do
+ ((Goal = sinr(AA,SA),
+ (A == AA;
+ nonvar(InPid2),
+ inside_Pid2(AA),
+ Sin == SA))
+ ->
+ % factorisation
+ kill_suspension(S),
+ protected_unify(A,AA),
+ protected_unify(Sin,SA)
+ ; ((Goal = cosr(AA,Cos),
+ Cos == Sin)
+ ->
+ ((A == AA,
+ get_sign_real(A,pos))
+ ->
+ % A pos
+ SeqC = 1,
+ mpid4(Pid4),
+ protected_unify(A,Pid4)
+ ; ((get_sign_real(A,neg),
+ is_op_real(real,A,OpA),
+ AA == OpA)
+ ->
+ % A neg: -3*pi/4
+ SeqC = 1,
+ moptpid4(OpTPid4),
+ protected_unify(A,OpTPid4)
+ ; true))
+ ; true))),
+ (nonvar(SeqC) ->
+ trigo_no_rat(A),
+ protected_unify(Sin,Cos),
+ sin_cos_val(A,Sin,Cos)
+ ; sinr_rec(A,Sin),
+ sin_cos_ineqs(sin,A,Sin),
+ (number(A) ->
+ sin_cos_val(A,Sin,Cos)
+ ; my_suspend(sinr(A,Sin),5,(A,Sin)->suspend:constrained))),
+ set_priority(P),
+ wake_if_other_scheduled(P).
+
+inside_Pid2(Var) :-
+ mpid2(Pid2),
+ mreal:dvar_range(Pid2,_,H),
+ OpH is -H,
+ mreal:dvar_range(Var,LA,HA),
+ OpH =< LA,
+ H >= HA.
+inside_Pi(Var) :-
+ mpi(Pi),
+ mreal:dvar_range(Pi,_,H),
+ OpH is -H,
+ mreal:dvar_range(Var,LA,HA),
+ OpH =< LA,
+ H >= HA.
+
+%sin_cos_ineqs(_,A,B) ?- !.
+
+sin_cos_ineqs(sin,A,A) ?- !. % deja traite
+sin_cos_ineqs(sin,A,Sin) :-
+ % A = Sin sur -2.1498999999999986e-8 .. 2.1498999999999986e-8
+ mreal:dvar_range(A,LA,HA),
+ % sur 0..pid2 -> 0..1, Rel = >=
+ % sur pid2..pi -> 1..0, Rel = >
+ % donc 0+..pi -> Rel = > (= autour de 0)
+
+ % sur -pi..-pid2 -> 0..-1, Rel = <
+ % sur -pid2..0 -> -1..0, Rel = =<
+ % donc -pi..-0 -> Rel = < (= autour de 0)
+
+ (LA >= 0.0 ->
+ (LA > 2.1498999999999986e-8 ->
+ Rel = '>'
+ ; Rel = '>='),
+ launch_real_ineq(Rel,real,A,Sin)
+ ; (HA =< 0.0 ->
+ (HA < -2.1498999999999986e-8 ->
+ Rel = '<'
+ ; Rel = '=<'),
+ launch_real_ineq(Rel,real,A,Sin)
+ ; true)).
+sin_cos_ineqs(cos,A,A) ?- !. % deja traite
+sin_cos_ineqs(cos,A,Cos) :-
+ % on est sur 0..pi
+ % A = Cos sur 0.73908513321516056 .. 0.73908513321516067
+ % sur pi/2..pi, décroissant -> 0..-1 Cos < A, Rel = '>'
+ % sur 0..pi/2 -> 1..0,
+ % Rel = '=<' jusqu'a 0.73908513321516067, '>=' après
+ mreal:dvar_range(A,LA,HA),
+ Pid2 is pi/2.0,
+ (LA >= Pid2 ->
+ launch_real_ineq(>=,real,A,Cos)
+ ; (HA =< Pid2 ->
+ (HA =< 0.73908513321516067 ->
+ launch_real_ineq(>=,real,Cos,A)
+ ; (LA >= 0.73908513321516067 ->
+ launch_real_ineq(>=,real,A,Cos)
+ ; true))
+ ; true)).
+
+sin_cos_val(Val,Sin,Cos) :-
+ get_priority(P),
+ set_priority(1),
+ sin_cos_val0(Val,Sin,Cos),
+ set_priority(P),
+ wake_if_other_scheduled(P).
+
+sin_cos_val0(0.0,Sin,Cos) ?- !,
+ protected_unify(Sin,0.0),
+ protected_unify(Cos,1.0).
+sin_cos_val0(Val,Sin,Cos) :-
+ nonvar(Val),
+ mpis(_,_,Pi,OpPi,Pid2,OpPid2,_,_,_,_),
+ mreal:get_intervals(Pi,Ip),
+ mreal:get_intervals(OpPi,Iop),
+ ((mreal:in_interval(Ip,Val);
+ mreal:in_interval(Iop,Val))
+ ->
+ !,
+ protected_unify(Sin,0.0),
+ protected_unify(Cos,-1.0)
+ ; mreal:get_intervals(Pid2,Ipd2),
+ (mreal:in_interval(Ipd2,Val) ->
+ !,
+ protected_unify(Sin,1.0),
+ protected_unify(Cos,0.0)
+ ; mreal:get_intervals(OpPid2,Iopd2),
+ mreal:in_interval(Iopd2,Val),
+ !,
+ protected_unify(Sin,-1.0),
+ protected_unify(Cos,0.0))).
+sin_cos_val0(A,Sin,Cos) :-
+ attached_suspensions(sin_val,LS),
+ ((member(Susp,LS),
+ get_suspension_data(Susp,goal,sin_cos_value(AA,SA,CA)),
+ A == AA)
+ ->
+ protected_unify(Sin,SA),
+ protected_unify(Cos,CA)
+ ; real_vars(real,(VS,VC)),
+ set_intervals(real,VS,[-1.0 .. 1.0]),
+ set_intervals(real,VC,[-1.0 .. 1.0]),
+ ((is_real_box(A),
+ Sin == Cos)
+ ->
+ sin_cos_pid4(Sin),
+ protected_unify(Sin,VS),
+ protected_unify(VS,VC)
+ ; sin(A,S),
+ get_previous_float(real,S,PS),
+ get_next_float(real,S,NS),
+ set_intervals(real,VS,[PS..NS]),
+ protected_unify(Sin,VS),
+ (A == S ->
+ % A <> 0, imprécision de sin autour de 0
+ launch_box_prio(Sin,_)
+ ; true),
+ cos(A,C),
+ get_previous_float(real,C,PC),
+ get_next_float(real,C,NC),
+ set_intervals(real,VC,[PC..NC]),
+ protected_unify(Cos,VC)),
+ trigo_no_rat(A),
+ trigo_no_rat(VS),
+ trigo_no_rat(VC),
+ sin_cos_value(A,VS,VC)).
+
+sin_cos_pid4(SC) :-
+ % +/-sqrt(2)/2
+ (get_sign_real(SC,neg) ->
+ ISC = [-0.70710678118654757 .. -0.70710678118654746]
+ ; ISC = [0.70710678118654746 .. 0.70710678118654757]),
+ set_intervals(real,SC,ISC),
+ trigo_no_rat(SC),
+ launch_box_prio(SC,_).
+
+sin_cos_value(A,VS,VC) :-
+ mreal:dvar_range(VS,LS,HS),
+ (get_next_float(real,LS,HS) ->
+ launch_box_prio(VS,_)
+ ; true),
+ mreal:dvar_range(VC,LC,HC),
+ (get_next_float(real,LC,HC) ->
+ launch_box_prio(VC,_)
+ ; true),
+ my_suspend(sin_cos_value(A,VS,VC),0,[(A,VS,VC)->suspend:constrained,trigger(sin_val)]).
+
+
+is_sin_cos_value(Var) :-
+ is_real_box(Var),
+ mpis(DPi,OpDPi,Pi,OpPi,Pid2,OpPid2,Pid4,OpPid4,TPid4,OTPid4),
+ mreal:get_intervals(Var,IV),
+ mreal:get_intervals(DPi,Idp),
+ mreal:get_intervals(OpDPi,Iodp),
+ mreal:get_intervals(Pi,Ip),
+ mreal:get_intervals(OpPi,Iop),
+ mreal:get_intervals(Pid2,Ipd2),
+ mreal:get_intervals(OpPid2,Iopd2),
+ mreal:get_intervals(Pid4,Ipd4),
+ mreal:get_intervals(OpPid4,Iopd4),
+ mreal:get_intervals(TPid4,Itpd4),
+ mreal:get_intervals(OTPid4,Iotpd4),
+ (member(IV,[Idp,Iodp,Ip,Iop,Ipd2,Iopd2,Ipd4,Iopd4,Itpd4,Iotpd4]) ->
+ true
+ ; is_trigo_no_rat(Var)).
+
+
+sin_val_min(0.0,Res) ?- !,
+ Res = 0.0.
+sin_val_min(A,Res) :-
+ abs(A,AA),
+ (AA =:= pi ->
+ Res = 0.0
+ ; (A =:= pi/2 ->
+ Res = 1.0
+ ; (A =:= -pi/2 ->
+ Res = -1.0
+ ; sin(A,S),
+ get_previous_float(real,S,Res)))).
+sin_val_max(0.0,Res) ?- !,
+ Res = 0.0.
+sin_val_max(A,Res) :-
+ abs(A,AA),
+ (AA =:= pi ->
+ Res = 0.0
+ ; (A =:= pi/2 ->
+ Res = 1.0
+ ; (A =:= -pi/2 ->
+ Res = -1.0
+ ; sin(A,S),
+ get_next_float(real,S,Res)))).
+
+asin_val_min(A,Min) :-
+ asin(A,S),
+ get_previous_float(real,S,Min).
+asin_val_max(A,Max) :-
+ asin(A,S),
+ get_next_float(real,S,Max).
+
+sinr_rec(A,Sin) :-
+ Pid2 is pi/2.0,
+ OpPid2 is - Pid2,
+ sinr_rec0(A,Pid2,OpPid2,Sin).
+
+sinr_rec0(A,Pid2,OpPid2,Sin) :-
+ mreal:get_intervals(A,As),
+ mreal:get_intervals(Sin,Sins),
+ sin_intervals(As,Pid2,OpPid2,Sins0),
+ (is_real_box(Sin) ->
+ list_to_intervals(real,Sins0,IS0),
+ check_intervals_intersection(IS0,Sins)
+ ; set_intervals(real,Sin,Sins0)),
+ mreal:get_intervals(Sin,NSins),
+
+ asin_intervals0(NSins,As1),
+ (is_real_box(A)->
+ list_to_intervals(real,As1,IAs1),
+ check_intervals_intersection(IAs1,As)
+ ; set_intervals(real,A,As1)),
+ mreal:get_intervals(A,NAs),
+ ((As == NAs,
+ Sins == NSins)
+ ->
+ true
+ ; sinr_rec0(A,Pid2,OpPid2,Sin)).
+
+sin_intervals(LI,NLI) :-
+ Pid2 is mpid2,
+ OpPid2 is - Pid2,
+ sin_intervals(LI,Pid2,OpPid2,NLI).
+
+sin_intervals([],_,_,[]).
+sin_intervals([I|LI],Pid2,OpPid2,NewLI) :-
+ min_max_inter(I,L,H),
+ (L < OpPid2 ->
+ (H =< OpPid2 ->
+ % -pi..-pi/2 on est décroissant
+ sin_val_max(L,NH),
+ sin_val_min(H,NL),
+ NLI = LI,
+ NewLI = [NL..NH|ENewLI]
+ ; (H =< 0.0 ->
+ % -pi..0 -> -pi..-pi/2 U -pi/2..0
+ NLI = [L..OpPid2,OpPid2..H|LI],
+ NewLI = ENewLI
+ ; (H =< pi/2 ->
+ % -pi..pi/2 -> -pi..-pi/2 U -pi/2..pi/2
+ NLI = [L..OpPid2,OpPid2..H|LI],
+ NewLI = ENewLI
+ ; % -pi..pi -> -pi..-pi/2 U -pi/2..pi/2 U pi/2..pi
+ NLI = [L..OpPid2,OpPid2..Pid2, Pid2..H|LI],
+ NewLI = ENewLI)))
+ ; % L >= OpPid2
+ (H =< Pid2 ->
+ % -pi/2..pi/2 on est croissant
+ sin_val_min(L,NL),
+ sin_val_max(H,NH),
+ NLI = LI,
+ NewLI = [NL..NH|ENewLI]
+ ; (L >= Pid2 ->
+ % pi/2..pi on est décroissant
+ sin_val_max(L,NH),
+ sin_val_min(H,NL),
+ NLI = LI,
+ NewLI = [NL..NH|ENewLI]
+ ; % -pi/2..pi -> 0..pi/2 U pi/2..pi
+ NLI = [L..Pid2,Pid2..H|LI],
+ NewLI = ENewLI))),
+ sin_intervals(NLI,Pid2,OpPid2,ENewLI).
+
+asin_intervals0([],[]).
+asin_intervals0([I|LI],NLI) :-
+ Pid2 is pi/2,
+ Pi is pi,
+ min_max_inter(I,L,H),
+ (H =< 0.0 ->
+ % on est dans -1 .. 0 donc asin dans -pi/2 .. 0 U -pi .. -pi/2
+ % [asin(L)..asin(H)] U [-pi-asin(H) .. -pi/2-asin(L)]
+ asin_val_min(L,AL),
+ asin_val_max(H,AH),
+ % AL..AH dans -pi/2 ..0, symétrie autour de -pi/2
+ NAH0 is -Pi - AL,
+ NAL0 is -Pi - AH,
+ get_previous_float(real,NAL0,NAL),
+ get_next_float(real,NAH0,NAH),
+ append([AL..AH,NAL..NAH],ENLI,NLI),
+ asin_intervals0(LI,ENLI)
+ ; (L >= 0.0 ->
+ % [asin(L)..asin(H)] U [pi-asin(H) .. pi-asin(L)]
+ asin_val_min(L,AL),
+ asin_val_max(H,AH),
+ NAH1 is Pi - AL,
+ NAL1 is Pi - AH,
+ get_previous_float(real,NAL1,NAL),
+ get_next_float(real,NAH1,NAH),
+ append([AL..AH,NAL..NAH],ENLI,NLI),
+ asin_intervals0(LI,ENLI)
+ ; asin_intervals0([L..0.0,0.0..H|LI],NLI))).
+
+
+cosr(0.0,Cos) ?- !,
+ protected_unify(Cos,1.0).
+cosr(A,0.0) ?- !,
+ mpis(_,_,_,_,Pid2,OpPid2,_,_,_,_),
+ mreal:get_intervals(Pid2,I1),
+ mreal:get_intervals(OpPid2,I2),
+ append(I2,I1,IA),
+ set_intervals(real,A,IA),
+ %int_vars(bool,Bool),
+ set_intervals(int,Bool,[0,1]),
+ insert_dep_inst(inst_cstr(0,Bool)),
+ isNegative(real,A,Bool),
+ chk_nan_reif(Bool,(OpPid2,true),(Pid2,true),A).
+
+cosr(A,1.0) ?- !,
+ protected_unify(A,0.0).
+cosr(A,-1.0) ?- !,
+ mpis(_,_,Pi,OpPi,_,_,_,_,_,_),
+ mreal:get_intervals(Pi,I1),
+ mreal:get_intervals(OpPi,I2),
+ append(I2,I1,IA),
+ set_intervals(real,A,IA),
+ %int_vars(bool,Bool),
+ set_intervals(int,Bool,[0,1]),
+ insert_dep_inst(inst_cstr(0,Bool)),
+ isNegative(real,A,Bool),
+ chk_nan_reif(Bool,(OpPi,true),(Pi,true),A).
+
+cosr(A,Cos) :-
+ (number(A),
+ RA = A;
+ is_real_box_rat(A,RA)),
+ !,
+ sin_cos_val(RA,_,Cos).
+cosr(A,Cos) :-
+ is_real_box(A),
+ mpis(_,_,Pi,OpPi,Pid2,OpPid2,_,_,_,_),
+ mreal:get_intervals(A,IA),
+ mreal:get_intervals(Pid2,IPid2),
+ mreal:get_intervals(OpPid2,IOpPid2),
+ ((IA == IPid2,
+ NA = Pid2;
+ IA == IOpPid2,
+ NA = OpPid2)
+ ->
+ !,
+ protected_unify(A,NA),
+ protected_unify(Cos,0.0)
+ ; mreal:get_intervals(Pi,IPi),
+ mreal:get_intervals(OpPi,IOpPi),
+ once (IA == IPi,
+ NA = Pi;
+ IA == IOpPi,
+ NA = OpPi),
+ !,
+ protected_unify(A,NA),
+ protected_unify(Cos,-1.0)).
+cosr(A,Cos) :-
+ get_priority(P),
+ set_priority(1),
+ % cos(-A) = cos(A), passage dans 0..pi
+ (get_sign_real(A,SA) ->
+ % si fail on passe aux cas suivants
+ set_priority(P),
+ SA == neg,
+ !,
+ op_real(real,A,OpA),
+ trigo_no_rat(A),
+ trigo_no_rat(OpA),
+ cosr(OpA,Cos)
+ ; !,
+ save_cstr_suspensions(A),
+ get_saved_cstr_suspensions(LSusp),
+ ((member((Susp,cosr(AA,CC)),LSusp),
+ A == AA)
+ ->
+ set_priority(P),
+ protected_unify(Cos,CC)
+ ; %int_vars(bool,Bool),
+ set_intervals(int,Bool,[0,1]),
+ insert_dep_inst(inst_cstr(0,Bool)),
+ % pour forcer le signe, pos en priorite au labeling
+ isNegative(real,A,Bool),
+ (nonvar(Bool) ->
+ set_priority(P),
+ (Bool == 0 ->
+ % pos
+ set_sign(real,A,pos)
+ ; % neg
+ set_sign(real,A,neg)),
+ cosr(A,Cos)
+ ; set_priority(P),
+ my_suspend(cosr(A,Cos),3,(A,Cos,Bool)->suspend:constrained)))).
+cosr(A,Cos) :-
+ get_priority(P),
+ set_priority(1),
+ save_cstr_suspensions((A,Cos)),
+ get_saved_cstr_suspensions(LSusp),
+ % 0 .. A .. pi,
+ % si A =< pi/2 alors Cos >= 0
+ % sinon Cos =< 0
+ mpid2(Pid2),
+ (get_sign_real(Cos,SC) ->
+ % A pos
+ (SC == neg ->
+ % pi/2 .. A .. pi
+ launch_geq_real(real,A,Pid2)
+ ; % pos: 0 .. A .. pi/2
+ launch_geq_real(real,Pid2,A))
+ ; true),
+ (exists_diff_Rel(Cos,0.0) ->
+ launch_diff_real(real,A,Pid2)
+ ; true),
+ (A == Cos ->
+ set_intervals(real,A,[0.73908513321516056 .. 0.73908513321516067])
+ ; true),
+ % si on a un sin_cos_value(AA,SS,Cos) avec A et AA pos
+ % on peut factoriser !!!
+ attached_suspensions(sin_val,LS),
+ ((member(S,LS),
+ get_suspension_data(S,goal,sin_cos_value(AA,SS,CC)),
+ get_sign_real(AA,pos),
+ CC == Cos)
+ ->
+ Stop = 1,
+ protected_unify(A,AA)
+ ; (foreach((S,Goal),LSusp),
+ param(A,Cos,SeqC,Stop) do
+ ((Goal = cosr(AA,CA),
+ (A == AA;
+ var(Cos),
+ % entre 0 et pi c'est bon
+ Cos == CA))
+ ->
+ % factorisation
+ kill_suspension(S),
+ protected_unify(A,AA),
+ protected_unify(Cos,CA)
+ ; ((Goal = sinr(AA,Sin),
+ Cos == Sin)
+ ->
+ (A == AA ->
+ % A pos
+ SeqC = 1,
+ mpid4(Pid4),
+ protected_unify(A,Pid4)
+ ; ((get_sign_real(AA,neg),
+ is_op_real(real,A,OpA),
+ AA == OpA)
+ ->
+ % AA neg donc A: 3*pi/4
+ SeqC = 1,
+ mtpid4(TPid4),
+ protected_unify(A,TPid4)
+ ; true))
+ ; ((Goal = sin_cos_value(AA,SA,CA),
+ SA == CA,
+ (A == AA;
+ is_mpi_var(A,PosA,NegA,_),
+ AA == NegA))
+ ->
+ Stop = 1,
+ protected_unify(Cos,CA)
+ ; true))))),
+ (nonvar(Stop) ->
+ true
+ ; (nonvar(SeqC) ->
+ trigo_no_rat(A),
+ protected_unify(Sin,Cos),
+ sin_cos_val(A,Sin,Cos)
+ ; cosr_rec(A,Cos),
+ sin_cos_ineqs(cos,A,Cos),
+ (number(A) ->
+ sin_cos_val(A,Sin,Cos)
+ ; my_suspend(cosr(A,Cos),5,(A,Cos)->suspend:constrained)))),
+ set_priority(P),
+ wake_if_other_scheduled(P).
+
+cos_val_min(0.0,Res) ?- !,
+ Res = 1.0.
+cos_val_min(A,Res) :-
+ abs(A,AA),
+ (AA =:= pi ->
+ Res = -1.0
+ ; (AA =:= pi/2 ->
+ Res = 0.0
+ ; cos(A,S),
+ get_previous_float(real,S,Res))).
+cos_val_max(0.0,Res) ?- !,
+ Res = 1.0.
+cos_val_max(A,Res) :-
+ abs(A,AA),
+ (AA =:= pi ->
+ Res = -1.0
+ ; (AA =:= pi/2 ->
+ Res = 0.0
+ ; cos(A,S),
+ get_next_float(real,S,Res))).
+
+acos_val_min(A,Min) :-
+ acos(A,S),
+ get_previous_float(real,S,Min).
+acos_val_max(A,Max) :-
+ acos(A,S),
+ get_next_float(real,S,Max).
+
+cosr_rec(A,Cos) :-
+ mreal:get_intervals(A,As),
+ mreal:get_intervals(Cos,Coss),
+
+ cos_intervals(As,Coss0),
+ (is_real_box(Cos) ->
+ list_to_intervals(real,Coss0,IC),
+ check_intervals_intersection(IC,Coss)
+ ; set_intervals(real,Cos,Coss0)),
+ mreal:get_intervals(Cos,NCoss),
+
+ inv_acos_intervals(NCoss,Ac1),
+ (is_real_box(A) ->
+ list_to_intervals(real,Ac1,IA1),
+ check_intervals_intersection(IA1,As)
+ ; set_intervals(real,A,Ac1)),
+ mreal:get_intervals(A,NAs),
+ ((As == NAs,
+ Coss == NCoss)
+ ->
+ true
+ ; cosr_rec(A,Cos)).
+
+% on est dans 0..pi: cos décroissant
+cos_intervals([],[]).
+cos_intervals([I|LI],NLI) :-
+ min_max_inter(I,L,H),
+ cos_val_max(L,NH),
+ cos_val_min(H,NL),
+ NLI = [NL..NH|ENLI],
+ cos_intervals(LI,ENLI).
+
+% on vient de 0..pi et on est dans -1..1
+% décroissant sur 0 .. pi
+inv_acos_intervals([],[]).
+inv_acos_intervals([I|LI],NLI) :-
+ min_max_inter(I,L,H),
+ acos_val_min(H,NL),
+ acos_val_max(L,NH),
+ NLI = [NL..NH|ENLI],
+ inv_acos_intervals(LI,ENLI).
+
+
+cos_real(A,Cos) :-
+ get_priority(P),
+ set_priority(1),
+ no_simplex,
+ (exists_fact_periodic(cos,A,_,Res) ->
+ % on a un autre cos sur A
+ % factorisation
+ protected_unify(Cos,Res)
+ ; real_vars(real,A),
+ set_intervals(real,Cos,[-1.0 .. 1.0]),
+ sin_cos_tan_period(cos,A,NA,_,Cos,Stop),
+ (var(Stop) ->
+ trigo_no_rat(Cos),
+ cosr(NA,Cos)
+ ; true)),
+ set_priority(P),
+ wake_if_other_scheduled(P).
+
+tan_real(A,Tan) :-
+ (exists_fact_periodic(tan,A,_,Res) ->
+ protected_unify(Tan,Res)
+ ; real_vars(real,(A,Tan)),
+ trigo_no_rat(A),
+ trigo_no_rat(Tan),
+
+ cos_real(A,Cos),
+ ((exists_diff_Rel(Cos,0.0),
+ exists_diff_Rel(Tan,0.0))
+ ->
+ launch_diff_real(real,A,0.0)
+ ; true),
+
+ ((number(Tan),
+ exists_diff_Rel(Cos,0.0),
+ occurs(Tan,(-1.0,0.0,1.0)))
+ ->
+ (Tan == -1.0 ->
+ Goal = (op_real(real,Sin,OpSin),protected_unify(OpSin,Cos),sin_real(A,Sin))
+ ; (Tan == 0.0 ->
+ Goal = (protected_unify(Sin,0.0),sin_real(A,Sin))
+ ; % Tan == 1.0
+ Goal = (protected_unify(Sin,Cos),sin_real(A,Sin)))),
+ call(Goal)
+ ; set_intervals(int,Bool,[0,1]),
+ (as(Cos,real) $= as(0.0,real)) #= as(Bool,bool),
+ tan_real(Bool,A,Cos,Tan))).
+
+tan_real(1,A,_,Tan) ?- !,
+ as(Tan,real) $= as(uninterp(tan(as(A,real))),real).
+tan_real(0,A,Cos,Tan) ?- !,
+ get_priority(P),
+ set_priority(1),
+ ((number(Tan),
+ exists_diff_Rel(Cos,0.0),
+ occurs(Tan,(-1.0,0.0,1.0)))
+ ->
+ (Tan == -1.0 ->
+ Goal = (op_real(real,Sin,OpSin),protected_unify(OpSin,Cos),sin_real(A,Sin))
+ ; (Tan == 0.0 ->
+ Goal = (protected_unify(Sin,0.0),sin_real(A,Sin))
+ ; % Tan == 1.0
+ Goal = (protected_unify(Sin,Cos),sin_real(A,Sin)))),
+ call(Goal)
+ ; sin_cos_tan_period(tan,A,NA,K,Tan,Stop),
+ (nonvar(Stop) ->
+ true
+ ; (A == Tan ->
+ protected_unify(NA,0.0)
+ ; sin_real(NA,Sin),
+ cos_real(NA,Cos),
+ div_real(real,Sin,Cos,Tan)))),
+ set_priority(P),
+ wake_if_other_scheduled(P).
+tan_real(Bool,A,Cos,Tan) :-
+ my_suspend(tan_real(Bool,A,Cos,Tan),0,Bool->suspend:inst).
+
+
+% Versions naives de asin/acos/atan
+% pas définies partout danger !!!
+asin_real(Sin,A) :-
+ real_vars(real,(Sin,A)),
+ set_intervals(int,B,[0,1]),
+ insert_dep_inst(inst_cstr(0,B)),
+ ((as(Sin,real) $< as(-1.0,real)) or
+ (as(Sin,real) $> as(1.0,real))) #=
+ not(as(B,bool)),
+ asin_real(B,Sin,A).
+asin_real(0,Sin,A) ?- !,
+ as(Sin,real) $= uninterp(asin(as(A,real))).
+asin_real(1,Sin,A) ?- !,
+ trigo_no_rat(A),
+ trigo_no_rat(Sin),
+ % inversible vers -pi/2..pi/2
+ mpid2(Pid2),
+ mreal:dvar_range(Pid2,_,Max),
+ Min is - Max,
+ set_intervals(real,A,[Min..Max]),
+ asin_intervals(Sin,A),
+ sin_real(A,Sin).
+asin_real(B,Sin,A) :-
+ my_suspend(asin_real(B,Sin,A),0,B->my_suspend:inst).
+
+asin_intervals(Sin,A) :-
+ mreal:get_intervals(Sin,ISs),
+ asin_intervals0(ISs,IAs),
+ set_intervals(real,A,IAs).
+
+
+acos_real(Cos,A) :-
+ real_vars(real,(Cos,A)),
+ set_intervals(int,B,[0,1]),
+ insert_dep_inst(inst_cstr(0,B)),
+ ((as(Cos,real) $< as(-1.0,real)) or
+ (as(Cos,real) $> as(1.0,real))) #=
+ not(as(B,bool)),
+ acos_real(B,Cos,A).
+
+acos_real(0,Cos,A) ?- !,
+ as(Cos,real) $= uninterp(acos(as(A,real))).
+acos_real(1,Cos,A) ?- !,
+ get_priority(P),
+ set_priority(1),
+ trigo_no_rat(A),
+ trigo_no_rat(Cos),
+ % inversible vers 0..pi
+ mpi(Pi),
+ launch_geq_real(real,A,0.0),
+ launch_geq_real(real,Pi,A),
+ acos_intervals(Cos,A),
+ % si on a un cosr/sin_cos_value sur Cos avec
+ % un AA dans 0..pi alors A = AA
+ get_cstr_suspensions(Cos,LS),
+ ((member(S,LS),
+ get_suspension_data(S,goal,G),
+ (G = cosr(_,AA,CC);
+ G = cosr(AA,CC)),
+ Cos == CC,
+ inside_0Pi(AA))
+ ->
+ protected_unify(A,AA)
+ ; attached_suspensions(sin_val,NLS),
+ ((member(NS,NLS),
+ get_suspension_data(NS,goal,sin_cos_value(AA,_,CC)),
+ Cos == CC,
+ inside_0Pi(AA))
+ ->
+ protected_unify(A,AA)
+ ; cos_real(A,Cos))),
+ set_priority(P),
+ wake_if_other_scheduled(P).
+acos_real(B,Cos,A) :-
+ my_suspend(acos_real(B,Cos,A),0,B->my_suspend:inst).
+
+inside_0Pi(V) :-
+ mpi(Pi),
+ mreal:dvar_range(V,L,H),
+ mreal:dvar_range(Pi,_,PM),
+ 0.0 =< L,
+ PM >= H.
+
+acos_intervals(Cos,A) :-
+ mreal:get_intervals(Cos,ICs),
+ inv_acos_intervals(ICs,PIAs),
+ op_real_intervals(real,PIAs,0.0,[],NIAs),
+ append(NIAs,PIAs,IAs),
+ set_intervals(real,A,IAs).
+
+
+atan_real(Tan,A) :-
+ real_vars(real,(Tan,A)),
+ trigo_no_rat(Tan),
+ trigo_no_rat(A),
+ % inversible vers ]-pi/2..pi/2[
+ ((get_sign_real(Tan,S);
+ get_sign_real(A,S))
+ ->
+ set_sign(real,Tan,S),
+ set_sign(real,A,S)
+ ; true),
+ moppid2(OpPid2),
+ mpid2(Pid2),
+ gt_real(real,A,OpPid2),
+ gt_real(real,Pid2,A),
+ atan_intervals(Tan,A),
+ tan_real(A,Tan).
+
+atan_intervals(Tan,A) :-
+ mreal:get_intervals(Tan,ITs),
+ (foreach(IT,ITs),
+ foreach(IA,IAs) do
+ (IT = L..H ->
+ atan(L,L0),
+ atan(H,H0)
+ ; atan(IT,L0),
+ H0 = L0),
+ get_previous_float(real,L0,LA),
+ get_next_float(real,H0,HA),
+ IA = LA..HA),
+ set_intervals(real,A,IAs).
\ No newline at end of file
--
GitLab