From 1ad1ddd8852c7a99be9ffcf36d347e5d7505000e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Mon, 12 Apr 2021 11:37:49 +0200
Subject: [PATCH] Import from Bin:a1af7a0 Src:e3c0f494d farith:a93db57
---
Src/COLIBRI/arith_sched.pl | 221 ++++++++++----------
Src/COLIBRI/col_solve.pl | 107 +++-------
Src/COLIBRI/lp_arith.pl | 34 ++--
Src/COLIBRI/ndelta.pl | 6 +-
Src/COLIBRI/rbox.pl | 6 +-
Src/COLIBRI/realarith.pl | 406 +++++++++++++++++++++----------------
Src/COLIBRI/smt_import.pl | 12 ++
Src/COLIBRI/solve.pl | 158 ++++++++++++---
8 files changed, 536 insertions(+), 414 deletions(-)
diff --git a/Src/COLIBRI/arith_sched.pl b/Src/COLIBRI/arith_sched.pl
index b633fb6b7..e59c4f8dd 100755
--- a/Src/COLIBRI/arith_sched.pl
+++ b/Src/COLIBRI/arith_sched.pl
@@ -13,112 +13,105 @@
%:- pragma(expand).
%:- pragma(nodebug).
+:- import is_fzero/1 from colibri.
notify_arith(_).
:- mode set_touched_arg_from_goal(+,-,+).
set_touched_arg_from_goal(add_int(A,TA,B,TB,C,TC),Var,S) :- !,
- instantiate_flag([(A,TA),(B,TB),(C,TC)],Var,0,NInst0),
- ((A == 0;
- B == 0;
- C == 0;
- A == B;
- A == C;
- B == C)
- ->
- NInst is NInst0 + 2
- ; NInst = NInst0),
- change_prio_if_inst_arg(NInst,2,S,2,4).
+ instantiate_flag([(A,TA),(B,TB),(C,TC)],Var,0,NInst0),
+ ((A == 0;
+ B == 0;
+ C == 0;
+ A == B;
+ A == C;
+ B == C)
+ ->
+ NInst is NInst0 + 2
+ ; NInst = NInst0),
+ change_prio_if_inst_arg(NInst,2,S,2,4).
set_touched_arg_from_goal(add_real1(_,A,B,C),Var,S) :- !,
- term_variables((A,B,C),L),
- NInst0 is 3 - length(L),
- ((A == 0.0;
- B == 0.0;
- C == 0.0;
- A == B;
- A == C;
- B == C)
- ->
- LP = 2,
- NInst is NInst0 + 2
- ; LP = 3,
- NInst = NInst0),
- change_prio_if_inst_arg(NInst,2,S,LP,4).
+ term_variables((A,B,C),L),
+ NInst0 is 3 - length(L),
+ ((is_fzero(A);
+ is_fzero(B);
+ is_fzero(C);
+ A == B;
+ A == C;
+ B == C)
+ ->
+ LP = 2,
+ NInst is NInst0 + 2
+ ; LP = 3,
+ NInst = NInst0),
+ change_prio_if_inst_arg(NInst,2,S,LP,4).
set_touched_arg_from_goal(minus_real1(_,A,B,C),Var,S) :- !,
- term_variables((A,B,C),L),
- NInst0 is 3 - length(L),
- ((A == 0.0;
- B == 0.0;
- C == 0.0;
- A == B;
- A == C;
- B == C)
- ->
- LP = 2,
- NInst is NInst0 + 2
- ; LP = 3,
- NInst = NInst0),
- change_prio_if_inst_arg(NInst,2,S,LP,4).
+ set_touched_arg_from_goal(add_real1(_,A,B,C),Var,S).
set_touched_arg_from_goal(mult_int(A,TA,B,TB,C,TC),Var,S) :- !,
- instantiate_flag([(A,TA),(B,TB),(C,TC)],Var,0,NInst0),
- ((nonvar(A),member(A,[-1,0,1]);
- nonvar(B),member(B,[-1,0,1]);
- A == B;
- A == C;
- B == C)
- ->
- NInst is NInst0 + 2
- ; NInst = NInst0),
- change_prio_if_inst_arg(NInst,2,S,2,4).
+ instantiate_flag([(A,TA),(B,TB),(C,TC)],Var,0,NInst0),
+ ((nonvar(A),member(A,[-1,0,1]);
+ nonvar(B),member(B,[-1,0,1]);
+ A == B;
+ A == C;
+ B == C)
+ ->
+ NInst is NInst0 + 2
+ ; NInst = NInst0),
+ change_prio_if_inst_arg(NInst,2,S,2,4).
set_touched_arg_from_goal(mult_real1(_,A,B,C),Var,S) :- !,
- term_variables((A,B,C),L),
- NInst0 is 3 - length(L),
- ((nonvar(A),member(A,[-1.0,0.0,1.0]);
- nonvar(B),member(B,[-1.0,0.0,1.0]);
- A == B;
- A == C;
- B == C)
- ->
- LP = 2,
- NInst is NInst0 + 2
- ; LP = 3,
- NInst = NInst0),
- change_prio_if_inst_arg(NInst,2,S,LP,4).
+ term_variables((A,B,C),L),
+ NInst0 is 3 - length(L),
+ ((is_fzero(A);
+ is_fzero(B);
+ is_fzero(C);
+ nonvar(A),member(A,[-1.0,1.0]);
+ nonvar(B),member(B,[-1.0,1.0]);
+ A == B;
+ A == C;
+ B == C)
+ ->
+ LP = 2,
+ NInst is NInst0 + 2
+ ; LP = 3,
+ NInst = NInst0),
+ change_prio_if_inst_arg(NInst,2,S,LP,4).
set_touched_arg_from_goal(div_mod_int(A,B,C,_BC,R),Var,S) :- !,
- term_variables((A,B,C,R),L),
- NInst0 is 4 - length(L),
- ((A == 0;
- nonvar(B),member(B,[-1,1]);
- R == 0;
- A == B;
- A == C;
- B == C)
- ->
- LP = 2,
- NInst is NInst0 + 2
- ; LP = 3,
- NInst = NInst0),
- change_prio_if_inst_arg(NInst,2,S,LP,4).
+ term_variables((A,B,C,R),L),
+ NInst0 is 4 - length(L),
+ ((A == 0;
+ nonvar(B),member(B,[-1,1]);
+ R == 0;
+ A == B;
+ A == C;
+ B == C)
+ ->
+ LP = 2,
+ NInst is NInst0 + 2
+ ; LP = 3,
+ NInst = NInst0),
+ change_prio_if_inst_arg(NInst,2,S,LP,4).
set_touched_arg_from_goal(div_real1(_,A,B,C),Var,S) :- !,
- term_variables((A,B,C),L),
- NInst0 is 3 - length(L),
- ((A == 0.0;
- nonvar(B),member(B,[-1.0,1.0]);
- A == B;
- A == C;
- B == C)
- ->
- LP = 2,
- NInst is NInst0 + 2
- ; LP = 3,
- NInst = NInst0),
- change_prio_if_inst_arg(NInst,2,S,LP,4).
+ term_variables((A,B,C),L),
+ NInst0 is 3 - length(L),
+ ((is_fzero(A);
+ is_fzero(B);
+ is_fzero(C);
+ nonvar(B),member(B,[-1.0,1.0]);
+ A == B;
+ A == C;
+ B == C)
+ ->
+ LP = 2,
+ NInst is NInst0 + 2
+ ; LP = 3,
+ NInst = NInst0),
+ change_prio_if_inst_arg(NInst,2,S,LP,4).
set_touched_arg_from_goal(power_int(A,TA,_,B,TB),Var,S) :- !,
instantiate_flag([(A,TA),(B,TB)],Var,0,NInst),
@@ -194,31 +187,37 @@ set_touched_arg_from_goal(diff_int(A,B),Var,S) :- !,
; true).
set_touched_arg_from_goal(geq_real(_,A,B),Var,S) :- !,
- (A == B ->
- kill_suspension(S)
- ; ((nonvar(A);
- nonvar(B))
- ->
- change_prio_if_not_RC(S,2)
- ; true)).
+ (A == B ->
+ kill_suspension(S)
+ ; ((is_fzero(A);
+ is_fzero(B);
+ nonvar(A);
+ nonvar(B))
+ ->
+ change_prio_if_not_RC(S,2)
+ ; true)).
set_touched_arg_from_goal(gt_real(_,A,B),Var,S) :- !,
- %% pour echouer plus vite
- A \== B,
- ((nonvar(A);
- nonvar(B))
- ->
- change_prio_if_not_RC(S,2)
- ; true).
+ % pour echouer plus vite
+ A \== B,
+ ((is_fzero(A);
+ is_fzero(B);
+ nonvar(A);
+ nonvar(B))
+ ->
+ change_prio_if_not_RC(S,2)
+ ; true).
set_touched_arg_from_goal(diff_real(_,A,B),Var,S) :- !,
- %% pour echouer plus vite
- A \== B,
- ((nonvar(A);
- nonvar(B))
- ->
- change_prio_if_not_RC(S,2)
- ; true).
+ % pour echouer plus vite
+ A \== B,
+ ((is_fzero(A);
+ is_fzero(B);
+ nonvar(A);
+ nonvar(B))
+ ->
+ change_prio_if_not_RC(S,2)
+ ; true).
set_touched_arg_from_goal(_,_,_).
@@ -265,7 +264,7 @@ change_prio_if_inst_arg(NInst,Min,S,HighPrio,LowPrio) :-
:- export change_prio_scheduled_susp/4.
% INHIBE (plus lent !)
-change_prio_scheduled_susp(S,Goal,Mod,Prio) :- !.
+%change_prio_scheduled_susp(S,Goal,Mod,Prio) :- !.
change_prio_scheduled_susp(S,Goal,Mod,Prio) :-
kill_suspension(S),
term_variables(Goal,GoalVars0),
diff --git a/Src/COLIBRI/col_solve.pl b/Src/COLIBRI/col_solve.pl
index 90b58bdb2..db253f132 100644
--- a/Src/COLIBRI/col_solve.pl
+++ b/Src/COLIBRI/col_solve.pl
@@ -478,7 +478,7 @@ smt_solve(Test,FILE,TO,Code) :-
smt_solve_bis(Test,FILE,TO,Code).
-%:- setval(simplex_delay_deactivation,5).
+%:- setval(simplex_delay_deactivation,2).
:- setval(simplex_delay_deactivation,2).
smt_solve_bis(Test,FILE,TO,Code) :-
@@ -727,26 +727,6 @@ smt_test(TO,Size) :-
%StrDir = "./totest/",
%StrDir = "./AdaCore/",
%------------------------------------------------------------------------
- %StrDir = "./QF_ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/",% 6 (2) !
- %StrDir = "./QF_ABVFPLRA/20170501-Heizmann-UltimateAutomizer/",% 0 (0)
-%--------------------------------------------------------------------------
- %StrDir = "./QF_ABVFP/20170428-Liew-KLEE/imperial_synthetic_memcpy_and_use_as_bitvector_klee.x86_64/", % 0 TO (cvc4 0)
- %StrDir = "./QF_ABVFP/20170428-Liew-KLEE/imperial_synthetic_sorted_search_klee_no_bug_float.x86_64/", % 0 TO (cvc4 1)
- %StrDir = "./QF_ABVFP/20170428-Liew-KLEE/imperial_synthetic_sorted_search_klee_bug_float.x86_64/", % 0 TO (cvc4 1)
- %StrDir = "./QF_ABVFP/20170428-Liew-KLEE/imperial_svcomp_float-benchs_svcomp_sin_interpolated_bigrange_tight.x86_64/", % 1 TO (cvc4 1)
- %StrDir = "./QF_ABVFP/20170428-Liew-KLEE/aachen_real_libmatheval_sym_x.x86_64/", % 0 TO (cvc4 0)
- %StrDir = "./QF_ABVFP/20170428-Liew-KLEE/aachen_real_gmp_gmp_klee_mul.x86_64/", % 1 TO (cvc4 17)
- %StrDir = "./QF_ABVFP/20170428-Liew-KLEE/aachen_real_wxpro_tostr.x86_64/", % 2 TO (cvc4 1)
- %StrDir = "./QF_ABVFP/20170428-Liew-KLEE/aachen_real_sorting_full_sym_doubles.x86_64/", % 9 TO! (cvc4 1)
- %StrDir = "./QF_ABVFP/20170428-Liew-KLEE/imperial_synthetic_count_klee_bug.x86_64/", % 9 TO! (cvc4 0)
- %StrDir = "./QF_ABVFP/20170428-Liew-KLEE/imperial_synthetic_count_klee.x86_64/", % 47 TO/87! (cvc4 0)
- %StrDir = "./QF_ABVFP/20170428-Liew-KLEE/imperial_synthetic_count_klee_bug.x86_64/", % 9 TO! (cvc4 0)
- %StrDir = "./QF_ABVFP/20170428-Liew-KLEE/imperial_gsl_benchmarks_histogram2d_klee_bug.x86_64/", %OK
-
- %StrDir = "./QF_ABVFP/20170428-Liew-KLEE/", % 80 TO! (177 unsupported) (cvc4 95)
- %StrDir = "./QF_ABVFP/20170501-Heizmann-UltimateAutomizer/", % 0 (cvc4 2 TO)
-
-%----------------------------------------------------------------------
%StrDir = "./QF_BV/",
%StrDir = "./QF_BV/20170501-Heizmann-UltimateAutomizer/",
@@ -797,39 +777,38 @@ smt_test(TO,Size) :-
%StrDir = "./QF_BV/brummayerbiere4/",
%StrDir = "./QF_BV/bruttomesso/", % plein de TO
%StrDir = "./QF_BV/crafted/",
+
%-----------------------------------------------------------------------
- %StrDir = "./QF_BVFP/",
- %StrDir = "./QF_BVFP/20170428-Liew-KLEE/imperial_svcomp_float-benchs_svcomp_mea8000.x86_64/",
- %StrDir = "./QF_BVFP/20170428-Liew-KLEE/imperial_synthetic_interval_klee_bug_symbolic_increment.x86_64/", % tout OK
- %StrDir = "./QF_BVFP/20170428-Liew-KLEE/imperial_synthetic_count_klee_bug.x86_64/", % 9 TO/9 (0 si > 60s, cvc4 0)
- %StrDir = "./QF_BVFP/20170428-Liew-KLEE/imperial_synthetic_count_klee.x86_64/", % 45 TO/87 (0 si > 60s, cvc4 0)
- %StrDir = "./QF_BVFP/20170428-Liew-KLEE/imperial_synthetic_fadd_to_exact_zero_klee_float.x86_64/", % 0 TO (cvc4 0)
- %StrDir = "./QF_BVFP/20170428-Liew-KLEE/imperial_synthetic_fsub_to_exact_zero_klee_float.x86_64/", % 0 TO
- %StrDir = "./QF_BVFP/20170428-Liew-KLEE/imperial_gsl_benchmarks_statistics_full_sym_klee.x86_64/", % 2 TO/11 (cvc4 2)
- %StrDir = "./QF_BVFP/20170428-Liew-KLEE/aachen_real_wxpro_tostr.x86_64/", % 2 TO (cvc4 1)
- %StrDir = "./QF_BVFP/20170428-Liew-KLEE/imperial_synthetic_interval_klee_no_bug.x86_64/", % 0 TO (cv4 5)
- %StrDir = "./QF_BVFP/20170428-Liew-KLEE/imperial_synthetic_non_terminating_klee_bug.x86_64/", % tout OK
- %StrDir = "./QF_BVFP/20170428-Liew-KLEE/imperial_synthetic_sqrt_klee.x86_64/", % 5 TO en 24s,3 en 60s (cvc4 aussi,2 en 60s)
- %StrDir = "./QF_BVFP/20170428-Liew-KLEE/imperial_gsl_benchmarks_vectors_klee_bug.x86_64/", % tout OK
-
- %StrDir = "./QF_BVFP/20170428-Liew-KLEE/imperial_svcomp_float-benchs_svcomp_rlim_invariant.x86_64/", % tout OK
- %StrDir = "./QF_BVFP/20170428-Liew-KLEE/", % 30 TO (cvc4 50)
- %StrDir = "./QF_BVFP/20170501-Heizmann-UltimateAutomizer/", % tout OK
- %StrDir = "./QF_BVFP/ramalho/", % tout OK
- %StrDir = "./QF_BVFP/schanda/spark/", % 1 TO (quake)
- %StrDir = "./QF_BVFP/20190429-UltimateAutomizerSvcomp2019/", % tout OK
+ %StrDir = "./QF_ABVFP/20170428-Liew-KLEE/", % 138 TO!(117 min_solve) (177 unsupported) (cvc4 55)
+ %StrDir = "./QF_ABVFP/20170501-Heizmann-UltimateAutomizer/", % 1(0 min_solve) (cvc4 0)
+%----------------------------------------------------------------------
+ %StrDir = "./QF_ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/",% 6 (1)!(4 min_solve)
+ %StrDir = "./QF_ABVFPLRA/20170501-Heizmann-UltimateAutomizer/",% 0 (0)
+%--------------------------------------------------------------------------
+ %StrDir = "./QF_BVFP/20170428-Liew-KLEE/", % 15 TO (18/19 min_solve)(cvc4 50) (bitwuzla 15)
+ %StrDir = "./QF_BVFP/20170501-Heizmann-UltimateAutomizer/", % 0 TO (bitwuzla 0)
+ %StrDir = "./QF_BVFP/ramalho/", % 0 TO (bitwuzla 0)
+ %StrDir = "./QF_BVFP/schanda/spark/", % 1 TO (quake) (bitwuzla 1)
%----------------------------------------------------------------
- %StrDir = "./QF_BVFPLRA/20170501-Heizmann-UltimateAutomizer/", % tout OK
- %StrDir = "./QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/", % 14 TO (cvc4 22)
- %StrDir = "./QF_BVFPLRA/2019-Gudemann/", % tout OK
+ %StrDir = "./QF_BVFPLRA/20170501-Heizmann-UltimateAutomizer/", % 0 (cvc4 0) (0 min_solve)
+ %StrDir = "./QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/", % 10 TO(8) + 11 unsupported (cvc4 17 + 11u sinon 0u avec --fp-exp?))
+ %StrDir = "./QF_BVFPLRA/2019-Gudemann/", % 0 TO (cvc4 1)
%----------------------------------------------------------------
- %StrDir = "./QF_FPLRA/20170501-Heizmann-UltimateAutomizer/", % tout OK
- %StrDir = "./QF_FPLRA/20190429-UltimateAutomizerSvcomp2019/", % tout OK
- %StrDir = "./QF_FPLRA/2019-Gudemann/", % 2 TO (cvc4 11)
- %StrDir = "./QF_FPLRA/schanda/", % tout OK
-%----------------------------------------------------------------
- %StrDir = "./QF_UFFP/schanda/spark/", % tout OK
+ %StrDir = "./QF_FPLRA/20170501-Heizmann-UltimateAutomizer/", % 0 TO (cvc4 0)
+ %StrDir = "./QF_FPLRA/20190429-UltimateAutomizerSvcomp2019/", % 0 TO (cvc4 0)
+ %StrDir = "./QF_FPLRA/2019-Gudemann/", % 1 TO (cvc4 7)
+ %StrDir = "./QF_FPLRA/schanda/", % 0 TO (cvc4 0)
%----------------------------------------------------------------
+ %StrDir = "./QF_FP/20170501-Heizmann-UltimateAutomizer/", % 0
+% A VOIR
+ %StrDir = "./QF_FP/20190429-UltimateAutomizerSvcomp2019/",% 0 (bitwuzla 0)
+ %StrDir = "./QF_FP/ramalho/", % 4 (4 min_solve)(cvc4 19)(bitwuzla 17)
+ %StrDir = "./QF_FP/griggio/", % 43 TO (42/41 min_solve)(cast float-double, delta 0) (cvc4 89)(bitwuzla 74)
+ %StrDir = "./QF_FP/schanda/spark/", % 5 TO (5 min_solve) (avec (X+Y)/2 = X/2+Y/2
+ % quand c'est correcte, pas de inf/0 pour le resultat) (ncvc4 8)(bitwuzla 3)
+ %StrDir = "./QF_FP/wintersteiger/", % tout OK
+
+%-----------------------------------------------------------------
%StrDir = "./QF_UF/", %
%----------------------------------------------------------------
%StrDir = "./QF_AUFBV/", %
@@ -838,31 +817,8 @@ smt_test(TO,Size) :-
%----------------------------------------------------------------
%StrDir = "./QF_UFLIA/", %
%----------------------------------------------------------------
- %StrDir = "./QF_UFLRA/", %
+ %StrDir = "./QF_UFLRA/", % 247 TO
%----------------------------------------------------------------
- %StrDir = "./QF_FP/20170501-Heizmann-UltimateAutomizer/", %tout OK
- %StrDir = "./QF_FP/20190429-UltimateAutomizerSvcomp2019/",% 1 TO (bitwuzla 0)
- %StrDir = "./QF_FP/ramalho/", % 4 TO (bitwuzla 17)
- %StrDir = "./QF_FP/griggio/", % 54 TO (43 cast) (bitwuzla 74)
- StrDir = "./QF_FP/schanda/spark/", % 7 (6 avec dist cast 0 pour
- % double->float, mais faux !) TO (bitwuzla 3)
- %StrDir = "./QF_FP/wintersteiger/", % tout OK
- %StrDir = "./QF_FP/wintersteiger/abs/",
- %StrDir = "./QF_FP/wintersteiger/add/",
- %StrDir = "./QF_FP/wintersteiger/sub/",
- %StrDir = "./QF_FP/wintersteiger/mul/",
- %StrDir = "./QF_FP/wintersteiger/div/",
- %StrDir = "./QF_FP/wintersteiger/rem/",
- %StrDir = "./QF_FP/wintersteiger/fma/",
- %StrDir = "./QF_FP/wintersteiger/sqrt/",
- %StrDir = "./QF_FP/wintersteiger/toIntegral/",
- %StrDir = "./QF_FP/wintersteiger/eq/",
- %StrDir = "./QF_FP/wintersteiger/gt/",
- %StrDir = "./QF_FP/wintersteiger/lt/",
- %StrDir = "./QF_FP/wintersteiger/max/",
- %StrDir = "./QF_FP/wintersteiger/min/",
-
-%-----------------------------------------------------------------
%StrDir = "./QF_ABV/bench_ab/",
%StrDir = "./QF_ABV/bmc-arrays/",
%-----------------------------------------------------------------
@@ -872,7 +828,7 @@ smt_test(TO,Size) :-
%StrDir = "QF_AX/storecomm/",
%StrDir = "QF_AX/cvc/",
- %StrDir = "QF_ALIA/qlock2/", % Des TO et core dump
+ StrDir = "QF_ALIA/qlock2/", % Des TO et core dump
%StrDir = "QF_ALIA/cvc/", % TOUT OK
%StrDir = "QF_ALIA/UltimateAutomizer2/",% des TO
%StrDir = "QF_ALIA/piVC/", % TOUT OK
@@ -973,6 +929,7 @@ smt_test0(TO,Size,StrDir) :-
; concat_string(["timeout --signal=KILL --kill-after=0.1 ",TO,"s ",ECLIPSE," -b ",COL," -g ",SizeM," -e \"seed(0),use_delta,setval(def_real_for_int,1)@colibri,setval(step_limit,0),setval(no_dolmen_warning,1)@eclipse,smt_solve_get_stat(\'",F,"\')\""],Com)),
%; concat_string(["timeout --signal=KILL --kill-after=0.1 ",TO,"s cvc4 ",F],Com)),
+%; concat_string(["timeout --signal=KILL --kill-after=0.1 ",TO,"s ncvc4 --fp-exp ",F],Com)),
%; concat_string(["timeout --signal=KILL --kill-after=0.1 ",TO,"s z3 ",F],Com)),
%; concat_string(["timeout --signal=KILL --kill-after=0.1 ",TO,"s bitwuzla ",F],Com)),
exec(Com,[],Pid),
diff --git a/Src/COLIBRI/lp_arith.pl b/Src/COLIBRI/lp_arith.pl
index d19befa61..e7c250757 100755
--- a/Src/COLIBRI/lp_arith.pl
+++ b/Src/COLIBRI/lp_arith.pl
@@ -372,9 +372,9 @@ new_lin_env.
% inhibe car pbs sur les 0 et Inf a regler
%lin_solve(not_solved) :- !.
lin_solve(Status) :-
- getval(use_delta,1)@eclipse,
- getval(use_simplex,1)@eclipse,
- getval(lin_env,Env),
+ getval(use_delta,1)@eclipse,
+ getval(use_simplex,1)@eclipse,
+ getval(lin_env,Env),
Env \== 0,!,
(current_suspension(_) ->
lin_solve0(Status)
@@ -389,24 +389,28 @@ lin_solve0(Status) :-
block((not not (lin_solve1(Status),
setval(status,Status))
*/
+ getval(use_delta,UD)@eclipse,
block((lin_solve1(Status) ->
% getval(status,Status),
+ setval(use_delta,UD)@eclipse,
set_priority(Prio)
- ; set_priority(Prio),
+ ; setval(use_delta,UD)@eclipse,
+ set_priority(Prio),
fail),
Tag,
- ((Tag == abort;
- Tag == retry;
- Tag == timeout_col;
- Tag == timeout_ball_thrown)
+ (setval(use_delta,UD)@eclipse,
+ ((Tag == abort;
+ Tag == retry;
+ Tag == timeout_col;
+ Tag == timeout_ball_thrown)
->
- set_priority(Prio),
- exit_block(Tag)
- ; (getval(gdbg,1)@eclipse ->
- writeln(output,exit_full_lin_solve(Tag))
- ; true),
- set_priority(Prio),
- Status = not_solved)).
+ set_priority(Prio),
+ exit_block(Tag)
+ ; (getval(gdbg,1)@eclipse ->
+ writeln(output,exit_full_lin_solve(Tag))
+ ; true),
+ set_priority(Prio),
+ Status = not_solved))).
lin_solve1(Status) :-
getval(lin_cstrs,LCstrs0),
diff --git a/Src/COLIBRI/ndelta.pl b/Src/COLIBRI/ndelta.pl
index 883b9772d..bbe8ce330 100755
--- a/Src/COLIBRI/ndelta.pl
+++ b/Src/COLIBRI/ndelta.pl
@@ -1136,7 +1136,11 @@ insert_EqPaths([(V1,TC1)|EqPaths],V,TC,NEqPaths) :-
NEqPaths = [(V,TC),(V1,TC1)|EqPaths]
; (TC == TC1 ->
NEqPaths = [(V1,TC1)|EqPaths],
- (V1 \== V ->
+ ((V1 \== V,
+ get_type(V1,T1),
+ get_type(V,T),
+ T1 == T2)
+ ->
unify_later(V,V1)
; true)
; % TC < TC1
diff --git a/Src/COLIBRI/rbox.pl b/Src/COLIBRI/rbox.pl
index c7a70a4fe..20872c635 100755
--- a/Src/COLIBRI/rbox.pl
+++ b/Src/COLIBRI/rbox.pl
@@ -501,9 +501,9 @@ is_not_float_int_number(Var) :-
!,
Var =\= truncate(Var).
is_not_float_int_number(_{rbox:rf(RF,_)}) ?-
- once (RF == not_float_int;
- nonvar(RF),
- RF = nibox-_).
+ once (nonvar(RF),
+ (RF == not_float_int;
+ RF = nibox-_)).
:- export ensure_not_NaN/1.
ensure_not_NaN(T) :-
diff --git a/Src/COLIBRI/realarith.pl b/Src/COLIBRI/realarith.pl
index 4c01e477e..d49b4481f 100755
--- a/Src/COLIBRI/realarith.pl
+++ b/Src/COLIBRI/realarith.pl
@@ -142,7 +142,7 @@ truncate_bis(Type,A,B) :-
; Continue = 1))))))),
(var(Continue) ->
(nonvar(Goal) ->
- call_priority(Goal,2)
+ call(Goal)
; true)
; truncate_intervals(Type,A,B,NotIntegral),
check_exists_truncate_before_susp(Type,NotIntegral,A,B)),
@@ -479,18 +479,24 @@ refute_ineq_round(Goal,Type,A,B,NotIntegral,Stop) :-
Stop = 1,
% A = B et A integral
protected_unify(A,B)
- ; disable_timeout,
+ ;
+ disable_timeout,
+ getval(refutation_chk,RC)@eclipse,
(timeout(block(refute_ineq_round0(Goal,Type,A,B,NotIntegral,NewGoal,
Stop),
Tag,
(Tag == timeout_col ->
true
- ; exit_block(Tag))),
+ ; setval(refutation_chk,RC)@eclipse,
+ exit_block(Tag))),
0.001,
+% 1.0Inf,
true)
->
+ setval(refutation_chk,RC)@eclipse,
enable_check_global_timeout
- ; enable_check_global_timeout,
+ ; setval(refutation_chk,RC)@eclipse,
+ enable_check_global_timeout,
fail),
(nonvar(NewGoal) ->
call(NewGoal)
@@ -1428,7 +1434,17 @@ real_to_float_bis(Type,Rnd,A,B) :-
A == AA)
->
protected_unify(B,BB)
- ; my_suspend(real_to_float_bis(Type,Rnd,A,B),2,Rnd->suspend:inst)).
+ ; (number(A) ->
+ float_of_rat(Type,rtn,A,LB),
+ float_of_rat(Type,rtp,A,HB),
+ set_typed_intervals(B,Type,[LB..HB]),
+ (number(B) ->
+ true
+ ; Continue = 1)
+ ; Continue = 1),
+ (var(Continue) ->
+ true
+ ; my_suspend(real_to_float_bis(Type,Rnd,A,B),2,Rnd->suspend:inst))).
real_to_float_bis(Type,Rnd,A,B) :-
get_priority(Prio),
set_priority(1),
@@ -2179,9 +2195,6 @@ cast_double_to_float(Rnd,A,B) :-
launch_float_number(A),
launch_float_number(B),
ensure_not_NaN([A,B]),
- % Essai BM ?? (surement faux car deux doubles <> peuvent etre = en float)
- % A calculer selon rnd !!!
- %launch_delta(A,B,=,0),
(Rnd == rne ->
cast_double_to_float_bis(A,B)
; cast_double_to_float_bis(Rnd,A,B)).
@@ -2268,7 +2281,9 @@ cast_double_to_float_bis(Rnd,A,B) :-
; Continue = 1),
(var(Continue) ->
true
- ; get_saved_cstr_suspensions(LSusp),
+ ; % Essai BM ??
+ launch_delta_double_to_float(rne,A,B),
+ get_saved_cstr_suspensions(LSusp),
((member((_,cast_double_to_float_bis(RRnd,X,Y)),LSusp),
RRnd == Rnd,
A == X)
@@ -2280,6 +2295,20 @@ cast_double_to_float_bis(Rnd,A,B) :-
set_priority(Prio),
wake_if_other_scheduled(Prio).
+launch_delta_double_to_float(_,D,F) :- !.
+/*
+launch_delta_double_to_float(rne,D,F) ?-
+ var(A),
+ var(B),
+ getval(use_delta,1)@eclipse,
+ !,
+ % double(float(D)) peut etre <> D
+ % alors que float(double(F)) = F
+ % D peut etre arrondi sur un F hors de D (ex: Inf ou 0)
+ % Si F tient dans D le delta contient 0
+launch_delta_double_to_float(_,_,_).
+*/
+
cast_double_to_float_interval(Rnd,LA1,HA1,LB0,HB0) :-
(var(Rnd) ->
LRnd = rtn,
@@ -3421,8 +3450,8 @@ check_launch_add_int(Type,A,B,C,_,Continue) :-
->
cast_real_int(Type,A,IA),
cast_real_int(Type,B,IB),
- cast_real_int(Type,C,IC),
- add(IA,IB,IC)
+ add(IA,IB,IC),
+ cast_int_real(Type,IC,C)
; Continue = 1).
exists_feq(Type,A,A) ?- !.
@@ -6523,11 +6552,6 @@ cast_int_real(Type,A,B0) :-
Continue = 1
; true)),
(nonvar(Continue) ->
- ((Type \== real;
- is_float_number(B))
- ->
- launch_float_int_number(B)
- ; true),
cast_int_real1(Type,A,B),
lin_cast_int_real(Type,A,B)
;
@@ -6536,32 +6560,32 @@ cast_int_real(Type,A,B0) :-
wake_if_other_scheduled(Prio).
cast_int_real1(Type,A,B) :-
- get_priority(Prio),
- set_priority(1),
- cast_int_real_bis(Type,A,B),
- set_priority(Prio),
- wake_if_other_scheduled(Prio).
+ get_priority(Prio),
+ set_priority(1),
+ cast_int_real_bis(Type,A,B),
+ set_priority(Prio),
+ wake_if_other_scheduled(Prio).
cast_int_real_bis(Type,A,B) :-
- save_cstr_suspensions((A,B)),
- ((is_float_number(B); % unification avec une entree
- safe_integer_to_real(Type,A)) % A est un entier representable en flottants
- ->
- launch_float_int_number(B)
- ; true),
- check_exists_cast_int_real(Type,A,B),
- cast_int_real_inst(Type,A,B,Continue),
- (var(Continue) ->
- true
- ; cast_int_real_interval(Type,A,B),
- mfd:dvar_domain(A,DomA),
- inv_cast_int_real_interval(Type,B,A),
- mfd:dvar_domain(A,NDomA),
- % = necessaire
- (NDomA = DomA ->
- true
- ; cast_int_real_interval(Type,A,B)),
- check_before_susp_cast_int_real(Type,A,B)).
+ save_cstr_suspensions((A,B)),
+ cast_int_real_interval(Type,A,B),
+ ((is_float_number(B); % unification avec une entree
+ safe_integer_to_real(Type,A)) % A est un entier representable en flottants
+ ->
+ launch_float_int_number(B)
+ ; true),
+ check_exists_cast_int_real(Type,A,B),
+ cast_int_real_inst(Type,A,B,Continue),
+ (var(Continue) ->
+ true
+ ; mfd:dvar_domain(A,DomA),
+ inv_cast_int_real_interval(Type,B,A),
+ mfd:dvar_domain(A,NDomA),
+ % = necessaire
+ (NDomA = DomA ->
+ true
+ ; cast_int_real_interval(Type,A,B)),
+ check_before_susp_cast_int_real(Type,A,B)).
safe_integer_to_real(Type,V) :-
mfd:dvar_range(V,LV,HV),
@@ -6592,18 +6616,17 @@ check_before_susp_cast_int_real(Type,A,B) :-
set_intervals(int,A,InterA),
cast_int_real_interval(Type,A,B)
; true),
- ((is_float_number(B);
+ ((is_float_number(B);
safe_integer_to_real(Type,A))
->
- launch_float_int_number(B)
- ; true),
- cast_int_real_inst(Type,A,B,Continue),
- (var(Continue) ->
- true
- ; cast_int_real_ineqs(Type,A,B),
+ launch_float_int_number(B)
+ ; true),
+ cast_int_real_inst(Type,A,B,Continue),
+ (var(Continue) ->
+ true
+ ; cast_int_real_ineqs(Type,A,B),
%Prio = 3,
Prio = 4,
-
my_suspend(cast_int_real1(Type,A,B),Prio,(A,B)->suspend:constrained)).
cast_int_real_ineqs(Type,I,RI) :-
@@ -6611,20 +6634,24 @@ cast_int_real_ineqs(Type,I,RI) :-
var(I),
var(RI),
!,
- get_delta_before_after(RI,BR,AR),
- term_variables((BR,AR),Vars),
- (Vars == [] ->
- SeenSusps = []
- ; (foreach(V,Vars),
- fromto([],ISeen,OSeen,SeenSups),
- param(Type,I,RI) do
- get_cstr_suspensions(V,LSusp),
- get_rel_between_real_args(RI,V,RelRIV),
- cast_int_real_ineqs1(LSusp,ISeen,OSeen,Type,I,RI,V,RelRIV))),
- get_delta_before_after(I,BI,AI),
- term_variables((BI,AI),VarsI),
- cast_int_real_ineqs0(VarsI,Vars,SeenSups,Type,I,RI).
-
+ ((Type == real;
+ is_float_int_number(RI),
+ is_inside_mantissa(Type,RI))
+ ->
+ launch_delta(I,RI,=,0)
+ ; get_delta_before_after(RI,BR,AR),
+ term_variables((BR,AR),Vars),
+ (Vars == [] ->
+ SeenSusps = []
+ ; (foreach(V,Vars),
+ fromto([],ISeen,OSeen,SeenSups),
+ param(Type,I,RI) do
+ get_cstr_suspensions(V,LSusp),
+ get_rel_between_real_args(RI,V,RelRIV),
+ cast_int_real_ineqs1(LSusp,ISeen,OSeen,Type,I,RI,V,RelRIV))),
+ get_delta_before_after(I,BI,AI),
+ term_variables((BI,AI),VarsI),
+ cast_int_real_ineqs0(VarsI,Vars,SeenSups,Type,I,RI)).
cast_int_real_ineqs(Type,I,R).
cast_int_real_ineqs0([],Vars,Seen,Type,I,RI).
@@ -6780,46 +6807,50 @@ check_exists_cast_int_real(Type,A,B) :-
%% Mode reel
cast_int_real_inst(real,A,B,Continue) :- !,
- (number(A) ->
- %% Les grands entiers tels que |I| > 2^53
- %% ne sont pas tous representables par des doubles
- int_to_float_min_max(real,A,MinB,MaxB),
- (MinB == MaxB ->
- protected_unify(B = MinB)
- ; rational(A,RA),
+ (number(A) ->
+ % Les grands entiers tels que |I| > 2^53
+ % ne sont pas tous representables par des doubles
+ int_to_float_min_max(real,A,MinB,MaxB),
+ (MinB == MaxB ->
+ protected_unify(B = MinB)
+ ; rational(A,RA),
launch_box_rat(B,RA),
- mreal:set_typed_intervals(B,real,[MinB..MaxB]))
- ; (number(B) ->
- inv_int_to_real(real,B,A)
- ; Continue = 1)).
+ mreal:set_typed_intervals(B,real,[MinB..MaxB]))
+ ; (number(B) ->
+ inv_int_to_real(real,B,A)
+ ; (is_real_box_rat(B,RB) ->
+ denominator(RB,1),
+ numerator(RB,A0),
+ protected_unify(A,A0)
+ ; Continue = 1))).
%% Mode double/simple nearest
cast_int_real_inst(Type,A,B,Continue) :-
- (number(A) ->
- int_to_float(Type,A,B)
- ; (number(B) ->
- inv_int_to_real(Type,B,A)
- ; Continue = 1)).
+ (number(A) ->
+ int_to_float(Type,A,B)
+ ; (number(B) ->
+ inv_int_to_real(Type,B,A)
+ ; Continue = 1)).
inv_int_to_real(real,B,A) ?- !,
- % B <> +/-Inf et un seul entier donne exactement B
- B > -1.0Inf,
- B < 1.0Inf,
- fix(B,A0),
+ % B <> +/-Inf et un seul entier donne exactement B
+ B > -1.0Inf,
+ B < 1.0Inf,
+ fix(B,A0),
protected_unify(A,A0),
- float(A,B).
+ float(A,B).
inv_int_to_real(Type,B,A) :-
- mfd:dvar_range(A,MinA,MaxA),
- ((B > -1.0Inf,
- B < 1.0Inf)
- ->
- % B integral
- fix(B,FB),
- B is int_to_float(Type,FB)
- ; true),
- min_max_integral_bounds(Type,MinRep,MaxRep),
- inv_int_interval_to_real_value(Type,B,MinRep,MaxRep,MinA,MaxA,Inter),
- mfd:set_intervals(A,[Inter]),
+ mfd:dvar_range(A,MinA,MaxA),
+ ((B > -1.0Inf,
+ B < 1.0Inf)
+ ->
+ % B integral
+ fix(B,FB),
+ B is int_to_float(Type,FB)
+ ; true),
+ min_max_integral_bounds(Type,MinRep,MaxRep),
+ inv_int_interval_to_real_value(Type,B,MinRep,MaxRep,MinA,MaxA,Inter),
+ mfd:set_intervals(A,[Inter]),
(number(A) ->
int_to_float(Type,A,B)
; true).
@@ -7172,7 +7203,7 @@ reduce_float_int_domain(Type,1,Dom,NDom) :-
%% Echec si le domaine de A ne contient pas truncate(A)
%% Les infinis sont bien sur exclus
cast_real_int(A,B) :-
- getval(float_eval,Type)@eclipse,
+ getval(float_eval,Type)@eclipse,
cast_real_int_type(Type,A,B).
cast_real_int_type(real,A,B) ?- !,
@@ -7181,7 +7212,7 @@ cast_real_int_type(Type,A,B) :-
cast_fp_int(Type,A,B).
cast_fp_int(Type,A,B) :-
- set_lazy_domain(Type,A),
+ set_lazy_domain(Type,A),
set_lazy_domain(int,B),
int_vars(bool,Cond),
(getval(no_float_error,1)@eclipse ->
@@ -7225,28 +7256,20 @@ cast_real_int(Type,A,B) :-
set_priority(1),
set_lazy_domain(Type,A),
save_cstr_suspensions((A,B)),
- % on peut dimensioner B
- (var(B) ->
- get_previous_float(Type,1.0Inf,MaxBF),
- MaxB is integer(MaxBF),
- MinB is -MaxB,
- set_intervals(int,B,[MinB..MaxB])
- ; true),
- check_exists_cast_real_int(Type,A,B,Kill),
- (var(Kill) ->
- ((not_inf([A]);
- number(B))
- ->
- % initialisation pour B
- (var(B) ->
- cast_real_int_interval(Type,A,B)
- ; true),
- (Type == real ->
+ (not_inf_bounds(A) ->
+ % on peut dimensioner B
+ cast_real_int_interval(Type,A,B)
+ ; (var(B) ->
+ (get_type(B,_) ->
true
- ; launch_float_number(A)),
+ ; Suspend = 1)
+ ; true)),
+ check_exists_cast_real_int(Type,A,B,Kill),
+ (nonvar(Kill) ->
+ true
+ ; (var(Suspend) ->
cast_real_int1(Type,A,B)
- ; my_suspend(cast_real_int(Type,A,B),0,(A,B)->suspend:constrained))
- ; true),
+ ; my_suspend(cast_real_int(Type,A,B),0,(A,B)->suspend:constrained))),
set_priority(Prio),
wake_if_other_scheduled(Prio).
@@ -7301,7 +7324,7 @@ check_before_susp_cast_real_int(Type,A,B) :-
cast_real_int_inst(Type,FIA,A,B,Continue),
(var(Continue) ->
true
- ; (is_float_number(A) ->
+ ; (is_float_number(A) ->
Prio = 3
; Prio = 4),
my_suspend(cast_real_int1(Type,A,B),Prio,(A,B)->suspend:constrained)).
@@ -7314,23 +7337,28 @@ cast_real_int_ineqs(Type,RI,I) :-
var(I),
var(RI),
!,
- get_delta_before_after(RI,BR,AR),
- term_variables((BR,AR),Vars),
- (foreach(V,Vars),
- fromto([],ISeen,OSeen,SeenSups),
- param(Type,I,RI) do
- get_cstr_suspensions(V,LSusp),
- get_rel_between_real_args(RI,V,RelRIV),
- cast_real_int_ineqs1(LSusp,ISeen,OSeen,Type,RI,I,V,RelRIV)),
- get_delta_before_after(I,BI,AI),
- term_variables((BI,AI),VarsI),
- (foreach(NV,VarsI),
- fromto(SeenSups,ISeen,OSeen,_),
- param(Type,I,RI,SeenSups,Vars) do
- (occurs(NV,Vars) ->
- OSeen = ISeen
- ; get_cstr_suspensions(NV,LSusp),
- cast_real_int_ineqs2(LSusp,ISeen,OSeen,Type,RI,I,NV))).
+ (((Type == real;
+ is_inside_mantissa(Type,RI)),
+ is_float_int_number(RI))
+ ->
+ launch_delta(RI,I,=,0)
+ ; get_delta_before_after(RI,BR,AR),
+ term_variables((BR,AR),Vars),
+ (foreach(V,Vars),
+ fromto([],ISeen,OSeen,SeenSups),
+ param(Type,I,RI) do
+ get_cstr_suspensions(V,LSusp),
+ get_rel_between_real_args(RI,V,RelRIV),
+ cast_real_int_ineqs1(LSusp,ISeen,OSeen,Type,RI,I,V,RelRIV)),
+ get_delta_before_after(I,BI,AI),
+ term_variables((BI,AI),VarsI),
+ (foreach(NV,VarsI),
+ fromto(SeenSups,ISeen,OSeen,_),
+ param(Type,I,RI,SeenSups,Vars) do
+ (occurs(NV,Vars) ->
+ OSeen = ISeen
+ ; get_cstr_suspensions(NV,LSusp),
+ cast_real_int_ineqs2(LSusp,ISeen,OSeen,Type,RI,I,NV)))).
cast_real_int_ineqs(Type,I,R).
cast_real_int_ineqs1([],_,[],Type,RI,I,V,RelRIV).
@@ -8120,14 +8148,11 @@ minus_real_bis(1,Type,A,B,C) :-
clean_inf_args_from_res(Type,C,[A,B]),
propagate_float_int_bin_op(Type,A,B,C),
minus_real_inst(Type,A,B,C,Continue),
- % PMO si les 3 args sont des float_int entre -2^53 et 2^53 on peut
- % deleguer le calcul aux entiers
- check_launch_minus_int(Type,A,B,C,Continue,Continue1),
- (var(Continue1) ->
+ (var(Continue) ->
true
; clear_Goals_minus_real(Type,A,B,C),
- minus_real_2_args_equal(Type,A,B,C,Continue2),
- (var(Continue2) ->
+ minus_real_2_args_equal(Type,A,B,C,Continue1),
+ (var(Continue1) ->
true
; reduce_Res_from_matching_Goals(minus_real1,Type,A,B,C),
check_RelABC_minus_real(Type,A,B,C),
@@ -8135,13 +8160,15 @@ minus_real_bis(1,Type,A,B,C) :-
% Les deltas sont calcules apres point fixe
% (sinon ils sont faux !!)
minus_real_ineqs(Type,A,B,C),
- minus_real_inst(Type,A,B,C,Continue3),
+ minus_real_inst(Type,A,B,C,Continue2),
+ % PMO si les 3 args sont des float_int entre -2^53 et 2^53 on peut
+ % deleguer le calcul aux entiers
+ check_launch_minus_int(Type,A,B,C,Continue2,Continue3),
(var(Continue3) ->
true
; check_2box(Type,[A,B,C]),
set_prio_inst([A,B,C],4,5,Prio),
NewGoal = minus_real1(Type,A,B,C),
-
my_suspend(NewGoal, Prio, (A,B,C)-> suspend:constrained)))).
%% Pas de simplifications
@@ -8235,8 +8262,8 @@ check_launch_minus_int(Type,A,B,C,_,Continue) :-
->
cast_real_int(Type,A,IA),
cast_real_int(Type,B,IB),
- cast_real_int(Type,C,IC),
- add(IB,IC,IA)
+ add(IB,IC,IA),
+ cast_int_real(Type,IC,C)
; Continue = 1).
%% Identites communes real/float
@@ -9728,8 +9755,8 @@ check_launch_mult_int(Type,A,B,C,_,Continue) :-
->
cast_real_int(Type,A,IA),
cast_real_int(Type,B,IB),
- cast_real_int(Type,C,IC),
- mult(IA,IB,IC)
+ mult(IA,IB,IC),
+ cast_int_real(Type,IC,C)
; Continue = 1).
@@ -9905,6 +9932,7 @@ mult_real_int_ineqs(SA,SB,A,B,C) :-
(is_real_box_rat(Other,RL) ->
RH = RL
; mreal:dvar_range(Other,RL,RH)),
+ % A REVOIRE
(RL == -1.0Inf ->
% donc RH <> 1.0Inf, S = neg
(RCst > 0 ->
@@ -12750,13 +12778,13 @@ check_real_div_opp(Type,A,B,C,Continue) :-
div_real_bis(Type,A,B,C) :-
save_cstr_suspensions((A,B,C)),
+ clear_Goals_div_real(Type,A,B,C),
mult_real_sign(Type,A,B,C),
check_zero_inf_div_real(Type,A,B,C),
div_real_inst(Type,A,B,C,Continue0),
(var(Continue0) ->
true
- ; clear_Goals_div_real(Type,A,B,C),
- div_real_2_args_equal(Type,A,B,C,Continue),
+ ; div_real_2_args_equal(Type,A,B,C,Continue),
% PMO si les 3 args sont des float_int entre -2^53 et 2^53 on peut
% deleguer le calcul aux entiers
check_launch_div_int(Type,A,B,C,Continue,Continue1),
@@ -12803,42 +12831,49 @@ check_div_mult_exact(Type,A,B,C,_,Continue) :-
%saturate_div_real_two(Type,A,B,C) :- !.
% Bizarre !!
saturate_div_real_two(Type,A,B,C) :-
- get_saved_cstr_suspensions(LSusp),
((B == 2.0,
+ not_inf_bounds(A),
+ not_zero(C),
+ get_saved_cstr_suspensions(LSusp),
member((S,add_real1(Type,X,Y,AA)),LSusp),
+ % (X+Y)/2 = C
+ % dans ce cas (X+Y)/2 = X/2 + Y/2
var(X),
- var(Y),
- A == A,
- get_rel_between_real_args(X,Y,RelXY),
- RelXY \== ?,
- (get_rel_between_real_args(X,C,RelC);
- get_rel_between_real_args(Y,C,RelC)),
- RelC \== ?)
+ var(Y))
->
- % (X+Y)/B = C
- % on sature en creant B*X et B*Y
- ((get_cstr_suspensions(X,LSX),
- member(SX,LSX),
- get_suspension_data(SX,goal,mult_real1(Type,U,V,W)),
- (B == U ->
- V == X
- ; B == V,
- U == X))
+ % on sature en creant X/2 + Y/2 = C
+ get_cstr_suspensions(X,LSX),
+ ((member(SX,LSX),
+ get_suspension_data(SX,goal,div_real1(Type,XX,X2,Xd2)),
+ X2 == 2.0,
+ XX == X)
->
- true
- ; call_priority(mult_real(Type,B,X,BX),2)),
- ((get_cstr_suspensions(Y,LSY),
- member(SY,LSY),
- get_suspension_data(SY,goal,mult_real1(Type,U1,V1,W1)),
- (B == U1 ->
- V1 == Y
- ; B == V1,
- U1 == Y))
+ Goals1 = []
+ ; Goals1 = [div_real(Type,X,2.0,Xd2)]),
+ get_cstr_suspensions(Y,LSY),
+ ((member(SY,LSY),
+ get_suspension_data(SY,goal,div_real1(Type,YY,Y2,Yd2)),
+ Y2 == 2.0,
+ YY == Y)
->
- true
- ; call_priority(mult_real(Type,B,Y,BY),2))
+ Goals2 = Goals1
+ ; append(Goals1,[div_real(Type,Y,2.0,Yd2)],Goals2)),
+ (Goals2 == [] ->
+ ((member((_,add_real1(Type,Ud2,Vd2,CC)),LSusp),
+ CC == C,
+ (Ud2 == Xd2 ->
+ Vd2 == Yd2
+ ; Ud2 == Yd2,
+ Vd2 == Xd2))
+ ->
+ Goals = []
+ ; Goals = [add_real(Type,Xd2,Yd2,C)])
+ ; append(Goals2,[add_real(Type,Xd2,Yd2,C)],Goals)),
+ (foreach(G,Goals) do
+ call_priority(G,2))
; true).
+
%% PMO si les 3 args sont des float_int entre -2^53 et 2^53 on peut
%% deleguer le calcul de mult_real aux entiers
check_launch_div_int(Type,A,B,C,Continue,_) :-
@@ -12856,8 +12891,8 @@ check_launch_div_int(Type,A,B,C,_,Continue) :-
->
cast_real_int(Type,A,IA),
cast_real_int(Type,B,IB),
- cast_real_int(Type,C,IC),
- mult(IB,IC,IA)%% BM: reste nul donc on a une multiplication
+ mult(IB,IC,IA),%% BM: reste nul donc on a une multiplication
+ cast_int_real(Type,IC,C)
; Continue = 1).
@@ -12883,12 +12918,22 @@ check_zero_inf_div_real(Type,A,B,C) :-
clear_Goals_div_real(Type,A,B,C) :-
- clear_Goals_div_real0(Type,A,B,C),
get_saved_cstr_suspensions(LSusp),
+ clear_Goals_div_real0(Type,A,B,C),
((member((S,div_real1(Type,AA,BB,CC)),LSusp),
- AA == A, BB == B)
+ ((AA == A,
+ BB == B);
+ (CC == C,
+ B == 2.0,
+ BB == B,
+ not_zero(C),
+ not_inf_bounds(C),
+ U1 == AA,
+ U2 == A)))
+
->
kill_suspension(S),
+ protected_unify(U1,U2),
protected_unify(C,CC)
; true).
@@ -12989,6 +13034,7 @@ div_real_int_ineqs(SA,SB,A,B,C) :-
var(C),
nonvar(SA),
(nonvar(B),
+ not_inf_bounds(B),
rational(B,RB);
is_real_box_rat(B,RB)),
!,
diff --git a/Src/COLIBRI/smt_import.pl b/Src/COLIBRI/smt_import.pl
index 6c9a00020..52493ca58 100644
--- a/Src/COLIBRI/smt_import.pl
+++ b/Src/COLIBRI/smt_import.pl
@@ -970,6 +970,18 @@ dump_type_val('Real',Val0,Val) ?- !,
(Den == 1 ->
concat_string([Num,".0"],Val)
; concat_string(["(/ ",Num,".0 ",Den,".0)"],Val))).
+dump_type_val('RoundingMode',Val0,Val) ?- !,
+ ((nonvar(Val0),
+ member((Val0,Val),
+ [(rne,'RNE'),
+ (rna,'RNA'),
+ (rtn,'RTN'),
+ (rtp,'RTP'),
+ (rtz,'RTZ')]))
+ ->
+ true
+ ; % rne par defaut
+ Val = 'RNE').
dump_type_val('_'('FloatingPoint',8,24),Val0,Val) ?- !,
(Val0 == nan ->
concat_string(["(_ NaN ",8," ",24,")"],Val)
diff --git a/Src/COLIBRI/solve.pl b/Src/COLIBRI/solve.pl
index 4d5611c17..ad8dd1457 100644
--- a/Src/COLIBRI/solve.pl
+++ b/Src/COLIBRI/solve.pl
@@ -8117,6 +8117,8 @@ fp_sub_rnd(Rnd,Type,A,B,R) :-
->
protected_unify(R,RR)
; my_suspend(fp_sub_rnd(Rnd,Type,A,B,R),2,Rnd->suspend:constrained)).
+fp_sub_rnd(rne,Type,A,B,R) ?- !,
+ minus_real(Type,A,B,R).
fp_sub_rnd(Rnd,Type,A,B,R) :-
get_priority(Prio),
set_priority(1),
@@ -8351,6 +8353,9 @@ fp_mul_rnd(Rnd,Type,A,B,R) :-
(not_inf_bounds(R) ->
forbid_infinities(Type,[A,B])
; true),
+ (not_zero(R) ->
+ mult_real_sign(Type,A,B,R)
+ ; true),
fp_mul_inst(Rnd,Type,A,B,R,Continue),
(var(Continue) ->
true
@@ -8370,7 +8375,9 @@ fp_mul_rnd(Rnd,Type,A,B,R) :-
set_typed_intervals(R,Type,[LR..HR])
; true),
(ground((A,B,R)) ->
- true
+ % check
+ fp_mul_val(Rnd,Type,A,B,R0),
+ R0 == R
; my_suspend(fp_mul_rnd(Rnd,Type,A,B,R),0,(A,B,R)->
suspend:constrained)))),
set_priority(Prio),
@@ -8651,6 +8658,9 @@ fp_div_rnd(Rnd,Type,A,B,R) :-
forbid_zero(Type,A),
forbid_infinities(Type,[B])
; true)),
+ (not_zero(R) ->
+ mult_real_sign(Type,A,B,R)
+ ; true),
((number(A),
number(B);
not_zero(A),
@@ -8664,7 +8674,9 @@ fp_div_rnd(Rnd,Type,A,B,R) :-
set_typed_intervals(R,Type,[LR..HR])
; true),
(ground((A,B,R)) ->
- true
+ % check
+ fp_div_val(Rnd,Type,A,B,R0),
+ R0 == R
; my_suspend(fp_div_rnd(Rnd,Type,A,B,R),0,(A,B,R)->
suspend:constrained))),
set_priority(Prio),
@@ -11049,14 +11061,44 @@ choose_fd_var([Adj|UseList],Var,Size,NUseList) :-
% ne dependant d'aucune autre (MaxCycleVars)
% et apparaissant dans une adjacence singleton ou paire avec resultat connu
% ou bien dans une adjacence ne contenant que des MaxCycleVars
- min_vars([Adj|UseList],MinVars,NUseList),
- MinVars \== [],
- % Dans les selectionnables on en choisit une
- % de plus petit domaine et reveillant le maximum de contraintes
-% var_with_min_dom_max_cstr(MinVars,Var,Size).
- var_with_max_cstr_min_dom(MinVars,Var,Size).
+ delayed_goals(DG),
+ term_variables(DG,Vars0),
+ filter_constrained_vars(Vars0,MinVars),
+
+% min_vars([Adj|UseList],MinVars,NUseList),
+ MinVars \== [],
+%% var_with_min_dom_max_cstr(MinVars,Var,Size).
+% var_with_max_cstr_min_dom(MinVars,Var,Size).
+ leaf_vars([Adj|UseList],Leaves,NUseList),
+ leaf_var_with_max_cstr_min_dom(MinVars,[],Var,Size).
+% leaf_var_with_max_cstr_min_dom(MinVars,Leaves,Var,Size).
+
+leaf_vars(UseList,Leaves,NUseList) :-
+ (foreach((V,D,A),UseList),
+ fromto([],IT,OT,NUseList0) do
+ term_variables(A,NA),
+ (nonvar(V) ->
+ (foreach(VA,NA),
+ fromto(IT,INA,ONA,NewAdjs) do
+ ONA = [(VA,0,[])|INA]),
+ OT = NewAdjs
+ ; OT = [(V,0,NA)|IT])),
+ sort(NUseList0,NUseList),
+ leaf_vars(NUseList,Leaves0),
+ sort(Leaves0,Leaves).
+
+leaf_vars([],[]).
+leaf_vars([Adj|UseList],Leaves) :-
+ ((Adj = (V,_,Vars),
+ var(V),
+ not no_constraint(V),
+ filter_constrained_vars(Vars,[]))
+ ->
+ Leaves = [V|ELeaves]
+ ; ELeaves = Leaves),
+ leaf_vars(UseList,ELeaves).
%% Idem deleteffc mais plus precis, utilise "constraints_number"
%% et prend en compte les numeros de cycle
@@ -11373,6 +11415,58 @@ var_with_min_dom_max_cstr([V1|LV],V,Size,MinSize,Cstr,Var) :-
var_with_min_dom_max_cstr(LV,V,Size,MinSize,Cstr,Var)).
+leaf_var_with_max_cstr_min_dom(L,Leaves,Var,MinSize) :-
+ (foreach(V,L),
+ fromto([],IL,OL,NL) do
+ ((get_type(V,Type),
+ Type \= array(_,_))
+ ->
+ OL = [V|IL]
+ ; OL = IL)),
+ (Leaves == [] ->
+ var_with_max_cstr_min_dom(NL,Var,MinSize)
+ ; NL = [NV|ENL],
+ get_type(NV,Type),
+ dvar_size(Type,NV,Size0),
+ (ENL == [] ->
+ Var = NV,
+ MinSize = Size0
+ ; (occurs(NV,Leaves) ->
+ Leaf = 1
+ ; true),
+ constraints_number(NV,NbV0),
+ leaf_var_with_max_cstr_min_dom0(ENL,Leaves,NV,NbV0,Size0,Leaf,
+ Var,MinSize))).
+
+leaf_var_with_max_cstr_min_dom0([V|LV],Leaves,Var0,NbV0,Size0,Leaf0,Var,MinSize) :-
+ constraints_number(V,NbV),
+ (occurs(V,Leaves) ->
+ Leaf = 1
+ ; true),
+ ((NbV >= NbV0,
+ get_type(V,Type),
+ dvar_size(Type,V,Size),
+ (NbV > NbV0 ->
+ true
+ ; Size =< Size0,
+ (nonvar(Leaf0) ->
+ nonvar(Leaf)
+ ; true)))
+ ->
+ Var1 = V,
+ NbV1 = NbV,
+ Size1 = Size,
+ Leaf1 = Leaf
+ ; Var1 = Var0,
+ NbV1 = NbV0,
+ Size1 = Size0,
+ Leaf1 = Leaf0),
+ (LV == [] ->
+ Var = Var1,
+ MinSize = Size1
+ ; leaf_var_with_max_cstr_min_dom0(LV,Leaves,Var1,NbV1,Size1,Leaf1,Var,MinSize)).
+
+
var_with_max_cstr_min_dom([V|LV],Var,MinSize) :-
((get_type(V,Type),
Type \= array(_,_))
@@ -11380,7 +11474,7 @@ var_with_max_cstr_min_dom([V|LV],Var,MinSize) :-
(LV == [] ->
Var = V,
dvar_size(Type,V,MinSize)
- ; dvar_size(Type,V,Size),
+ ; dvar_size(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)).
@@ -11427,22 +11521,22 @@ var_with_max_cstr_min_dom1([VV|LV],IV,IS,INb,Var,MinSize) :-
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
:- mode simple_solve_var(?,++).
simple_solve_var(Var,Size) :-
- (var(Var) ->
- get_type(Var,Type),
- simple_solve_var_type(Type,Var,Size)
- ; true).
+ (var(Var) ->
+ get_type(Var,Type),
+ simple_solve_var_type(Type,Var,Size)
+ ; true).
:- mode simple_solve_var_type(++,?,++).
simple_solve_var_type(bool,Var,_) :-
- random_less(2,Rand),
- (Rand == 1 ->
- V1 = t,
- V2 = f
- ; V1 = f,
- V2 = t),
- ( Var = V1
- ; Var = V2).
+ random_less(2,Rand),
+ (Rand == 1 ->
+ V1 = t,
+ V2 = f
+ ; V1 = f,
+ V2 = t),
+ ( Var = V1
+ ; Var = V2).
simple_solve_var_type(int,Var,_) :-
(get_bvbounds(Var,_) ->
@@ -11490,7 +11584,11 @@ simple_solve_var_type(float_simple,Var,_) :-
simple_solve_var_float(float_simple,Var).
simple_solve_var_type(rnd,Var,_) :-
call_priority( (mfd:get_intervals(Var,LInter),
- member(Var,LInter)),
+ % pour les sat on va plus vite en rne !
+ (member_begin_end(rne,LInter,NLInter,End,End) ->
+ (Var = rne;
+ member(Var,NLInter))
+ ; member(Var,LInter))),
1).
simple_solve_var_type(sort(_),Var,_) :-
call_priority( (mfd:get_intervals(Var,LInter),
@@ -11499,17 +11597,18 @@ simple_solve_var_type(sort(_),Var,_) :-
simple_solve_var_float(Type,Var) :-
call_priority(
- (Type \== real,
- Var = -0.0;
+ (Var = -0.0;
Var = 0.0;
- forbid_zero(Type,Var),
- (is_mult_div_real_arg(Type,Var) ->
+ (fail,is_mult_div_real_arg(Type,Var) ->
+ % mauvais pour spark/asso_mult (sat)
(Var = 1.0;
Var = -1.0;
+ forbid_zero(Type,Var),
mreal:dvar_remove_element(Var,1.0),
mreal:dvar_remove_element(Var,-1.0),
simple_resol_float(Var))
- ; simple_resol_float(Var))),
+ ; forbid_zero(Type,Var),
+ simple_resol_float(Var))),
1).
/*
;
@@ -11524,9 +11623,10 @@ is_mult_div_real_arg(Type,Var) :-
suspensions(Var,LSusp),
member(Susp,LSusp),
get_suspension_data(Susp,goal,Goal),
- (Goal = mult_real1(Type,X,Y,_) ->
+ (member(Goal,[mult_real1(Type,X,Y,_),fp_mul_rnd(_,Type,X,Y,_)])
+ ->
(Var == X; Var == Y)
- ; Goal = div_real1(Type,_,Y,_),
+ ; member(Goal,[div_real1(Type,X,Y,_),fp_div_rnd(_,Type,X,Y,_)]),
Var == Y).
is_mult_div_arg(Var) :-
--
GitLab