From e5312e673f8b00e162cf40616ba767d9cb3df702 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Tue, 31 May 2022 10:39:17 +0200
Subject: [PATCH] Import from Bin:a1af7a0 Src:59c2c35f0 farith:a93db57
---
Src/COLIBRI/arith.pl | 15 +-
Src/COLIBRI/col_solve.pl | 617 ++++++++++++++++++++++++++++----------
Src/COLIBRI/colibri.pl | 3 +
Src/COLIBRI/mbv_propa.pl | 54 ++--
Src/COLIBRI/mfd.pl | 7 +-
Src/COLIBRI/mod_arith.pl | 169 ++++++-----
Src/COLIBRI/mreal.pl | 8 +-
Src/COLIBRI/my_suspend.pl | 19 +-
Src/COLIBRI/ndelta.pl | 41 ++-
Src/COLIBRI/notify.pl | 13 +-
Src/COLIBRI/realarith.pl | 416 +++++++++++++------------
Src/COLIBRI/smt_import.pl | 111 +++++--
Src/COLIBRI/solve.pl | 258 ++++++++++++----
Src/COLIBRI/util.pl | 32 +-
14 files changed, 1185 insertions(+), 578 deletions(-)
diff --git a/Src/COLIBRI/arith.pl b/Src/COLIBRI/arith.pl
index 111fd00f5..86097b74a 100755
--- a/Src/COLIBRI/arith.pl
+++ b/Src/COLIBRI/arith.pl
@@ -3507,7 +3507,7 @@ divides_vars(X,Y,Seen) :-
var(B),divides_vars(X,B,[S|Seen])).
check_dont_divide(A,B,Q,BQ,Rem) :-
- getval(refutation_chk,0)@eclipse,
+ fail,getval(refutation_chk,0)@eclipse,
number(B),
not_unify(Rem,0),
AB is abs(B),
@@ -3522,11 +3522,8 @@ check_dont_divide(A,B,Q,BQ,Rem) :-
(block(((for(Cst,0,AB-1),
fromto([],In,Out,PossibleCst),
param(A,X,Rem) do
- (timeout(not not (launch_congr(X,Cst,B),
- wake),
- %1.0Inf,
- 0.01,
- true)
+ (not not (launch_congr(X,Cst,B),
+ wake)
->
Out = [Cst|In]
; Out = In)),
@@ -6125,9 +6122,9 @@ notify_ineq_to_int_cstrs_if_new_rel(OldRel,A,B) :-
(foreach((Susp,Goal),LSusp),
param(A,B) do
functor(Goal,FGoal,_),
- (((occurs(A,Goal);occurs(B,Goal)),
- occurs(FGoal,(add_int,op_int,mult_int,div_mod_int,
- power_int,abs_val_int)))
+ ((occurs(FGoal,(add_int,op_int,mult_int,div_mod_int,
+ power_int,abs_val_int)),
+ (occurs(A,Goal);occurs(B,Goal)))
->
schedule_suspensions(1,s([Susp]))
; true))).
diff --git a/Src/COLIBRI/col_solve.pl b/Src/COLIBRI/col_solve.pl
index a2e8486a6..c10b11cb1 100644
--- a/Src/COLIBRI/col_solve.pl
+++ b/Src/COLIBRI/col_solve.pl
@@ -501,6 +501,7 @@ smt_comp_solve(FILE) :-
exit(Code).
smt_solve(FILE) :-
+ seed(0),
% Désactivation du simplex apres DDSteps
% (5000 par défaut dans colibri.pl)
% setval(simplex_delay_deactivation,DDSteps)@eclipse,
@@ -522,6 +523,7 @@ smt_solve(FILE) :-
exit(Code).
smt_solve_get_stat(FILE) :-
+ seed(0),
% On passe en mode comptage du nombre de steps
setval(step_stats,1)@eclipse,
% Si on a une limite elle est donnée dans la ligne de commande
@@ -548,7 +550,8 @@ smt_solve_bis(Test,FILE,TO,Code) :-
getval(def_real_for_int,RI)@colibri,
not not (smt_solve_bis0(Test,FILE,TO,Code0),
setval(init_code,Code0)),
- getval(init_code,Code0),
+ getval(init_code,Code).
+/*
((nonvar(Test),
Code0 == 0, % unsat
getval(real_for_int,1)@eclipse,
@@ -564,14 +567,16 @@ smt_solve_bis(Test,FILE,TO,Code) :-
; writeln(output,unknown),
Code = 2)
; Code = Code0).
-
+*/
+
smt_solve_bis0(Test,FILE,TO,Code) :-
% seed(0),
- setval(smt_status,unknown)@eclipse,
+ setval(smt_status,unknown_col)@eclipse,
setval(nb_steps,0)@eclipse,
setval(simplex_steps,0)@eclipse,
setval(solve,1),
- setval(time_limit,0),
+ %setval(time_limit,0),
+ reset_solve_timeout,
%setval(smt_status,0),
(nonvar(Test) ->
setval(scrambler,1)
@@ -592,6 +597,22 @@ smt_solve_bis0(Test,FILE,TO,Code) :-
writeln(output,unknown),
Code = 2,
setval(diag_code,(unknown,2))),
+
+ (var(TO) ->
+ NTO = 0
+ ; NTO = TO),
+ statistics(session_time,Start),
+ setval(start_solve,Start),
+ % Essai pour smt_comp : pas de delta/simplex apres DDSteps
+ getval(simplex_delay_deactivation,DDSteps)@eclipse,
+ smt_start_enable_delta_check(DDSteps),
+ ((var(Test),
+ DDSteps == 0)
+ ->
+ smt_disable_delta_check
+ ; smt_enable_delta_check),
+ start_solve_timeout(NTO),
+
(nonvar(Code) ->
true
; block((smt_interp_file(FILE,Goal) ->
@@ -600,34 +621,26 @@ smt_solve_bis0(Test,FILE,TO,Code) :-
TagRead,
((TagRead == unsupported ->
Code = 5
- ; concat_string(["(error \"",FILE,":",TagRead,"\")"],Mess),
- writeln(output,Mess),
- Code = 2),
- writeln(output,unknown),
- setval(diag_code,(unknown,Code))))),
+ ; (TagRead == timeout_col ->
+ (nonvar(Test) ->
+ writeln(output,'UNKNOWN':timeout)
+ ; true),
+ Code = 3,
+ setval(diag_code,(timeout,3))
+ ; (Tag == syntax ->
+ concat_string(["(error \"",FILE,":",TagRead,"\")"],Mess),
+ writeln(output,Mess),
+ Code = 2
+ ; % debug
+ (Test == 1 -> halt;true),
+ writeln(output,unknown),
+ setval(diag_code,(unknown,Code)))))))),
getval(use_delta,UD)@eclipse,
getval(use_simplex,US)@eclipse,
(nonvar(Code) ->
true
; save_goal_before_check_sat(Goal),
- (var(TO) ->
- setval(time_limit,0)
- ; setval(time_limit,TO)),
- statistics(session_time,Start),
- setval(start_solve,Start),
- % Essai pour smt_comp : pas de delta/simplex apres DDSteps
- getval(simplex_delay_deactivation,DDSteps)@eclipse,
- smt_start_enable_delta_check(DDSteps),
- ((var(Test),
- (%TO > 0;
- DDSteps == 0))
- ->
- smt_disable_delta_check
- ; smt_enable_delta_check),
- getval(time_limit,NTO),
- block((timeout(not not call(Goal),
- NTO,
- exit_block(timeout_col))
+ block((not not call(Goal)
->
getval(diag_code,(Diag,Code))
; % echec a la propagation
@@ -643,7 +656,7 @@ smt_solve_bis0(Test,FILE,TO,Code) :-
setval(diag_code,(Diag,Code))),
Tag,
(update_min_max_lazy_int(MinInt,MaxInt),
- (Tag == timeout_col ->
+ (Tag == timeout_col ->
(nonvar(Test) ->
writeln(output,'UNKNOWN':timeout)
; true),
@@ -698,7 +711,7 @@ save_goal_before_check_sat(Goal) :-
goal_before_check_sat(Goal,NGoal0),
get_type_decl(NGoal0,Decl,NGoal),
% call(Decl),
- keep_ground_goals(NGoal,NGoal1,GCG,EGCG),
+ keep_ground_goals(NGoal,NGoal1,_GCG,_EGCG),
sort(NGoal1,NGoal2),
term_variables(NGoal2,LVars),
% my_term_variables(NGoal2,LVars),
@@ -716,7 +729,7 @@ save_goal_before_check_sat(Goal) :-
(get_variable_type(MV,Type) ->
OTV = [(MV,Type,CV)|ITV]
; OTV = ITV)),
- setval(gsat,CNGoal1-TCGVars).
+ setval(gsat,CNGoal2-TCGVars).
:- export my_term_variables/2.
my_term_variables(Term,Vars) :-
@@ -787,6 +800,7 @@ smt_solve_test_bis(FILE,TO,Code) :-
Status = Diag;
Diag \== unknown,
Status0 \== unknown,
+ Status0 \== unknown_col,
Status0 \== 0,
Status0 \== Diag,
Status = Status0)
@@ -815,8 +829,8 @@ smt_test_CI(TO,Size) :-
smt_test(TO,Size,CI) :-
%StrDir = "./colibri_tests/colibri/tests/",
%StrDir = "./colibri_tests/colibri/tests/sat/",
- % 0 (sans real/float->int!)
- StrDir = "./colibri_tests/colibri/tests/unsat/", %0
+ % 0 en 20s (sans real/float->int!)
+ %StrDir = "./colibri_tests/colibri/tests/unsat/", %0
%StrDir = "./colibri_tests/colibri/tests/unknown/",
%StrDir = "./colibri_tests/colibri/tests/timeout/",
@@ -969,7 +983,7 @@ smt_test(TO,Size,CI) :-
%StrDir = "./QF_ABVFP/20170428-Liew-KLEE/aachen_real_gmp_gmp_klee_mul.x86_64/", % 3 (bitwuzla 0)
%StrDir = "QF_ABVFP/20170428-Liew-KLEE/aachen_real_numerical_recipes_qrdcmp.x86_64/", % 0
- %StrDir = "./QF_ABVFP/20170428-Liew-KLEE/", % 104/17933 (177 u, 101 I) (cvc4 55)
+ %StrDir = "./QF_ABVFP/20170428-Liew-KLEE/", % 123/18033 (177 u, 1 I) (cvc4 55)
%StrDir = "./QF_ABVFP/20170501-Heizmann-UltimateAutomizer/", % 0 min_solve (cvc4 0) OK
%----------------------------------------------------------------------
%StrDir = "./QF_ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/",% 0 (cvc4 1|2)!
@@ -980,7 +994,7 @@ smt_test(TO,Size,CI) :-
%StrDir = "./QF_BVFP/20170428-Liew-KLEE/aachen_syn_halve_longdouble-flow.x86_64/",% 4u
- %StrDir = "./QF_BVFP/20170428-Liew-KLEE/", % 16 (cvc4 50)(bitwuzla
+ %StrDir = "./QF_BVFP/20170428-Liew-KLEE/", % 57/17156 (cvc4 50)(bitwuzla
% 15)(89 u)(11 20mn)
%StrDir = "./QF_BVFP/20170501-Heizmann-UltimateAutomizer/", % 0 (bitwuzla 0)
%StrDir = "./QF_BVFP/ramalho/", % 0 TO (bitwuzla 0)
@@ -994,13 +1008,13 @@ smt_test(TO,Size,CI) :-
%----------------------------------------------------------------
%StrDir = "./QF_FPLRA/20170501-Heizmann-UltimateAutomizer/", % 0 (cvc4 0)
%StrDir = "./QF_FPLRA/20190429-UltimateAutomizerSvcomp2019/", % 0 (cvc4 0)
- %StrDir = "./QF_FPLRA/2019-Gudemann/", % 2 (cvc4 7)
+ %StrDir = "./QF_FPLRA/2019-Gudemann/", % 2/13 (cvc4 7)
%StrDir = "./QF_FPLRA/schanda/", % 0 (cvc4 0)
%----------------------------------------------------------------
%StrDir = "./QF_FP/20170501-Heizmann-UltimateAutomizer/", % 0
%StrDir = "./QF_FP/20190429-UltimateAutomizerSvcomp2019/",% 0 (bitwuzla 0)
- %StrDir = "./QF_FP/ramalho/", % 0 (cvc4 19)(bitwuzla 17)
- %StrDir = "./QF_FP/griggio/", % 49 (min_solve, sans lin_solve ni ls_reduce..)(39)
+ %StrDir = "./QF_FP/ramalho/", % 1 (cvc4 19)(bitwuzla 17)
+ StrDir = "./QF_FP/griggio/", % 52/214 (min_solve, sans lin_solve ni ls_reduce..)(39)
%(cvc4 89)(bitwuzla 74) LES DD DEMARRENT TROP VITE ?
%StrDir = "./QF_FP/schanda/spark/", % 6! (min_solve avec X =< (X+Y)/2 =< Y) (ncvc4 8)(bitwuzla 3)
%StrDir = "./QF_FP/wintersteiger/", % tout OK
@@ -1089,7 +1103,7 @@ smt_test(TO,Size,CI) :-
smt_test0(TO,Size,StrDir,CI).
:- lib(timeout).
-:- setval(nbTryCI,2).
+:- setval(nbTryCI,2)@eclipse.
smt_test0(TO,Size,StrDir,CI) :-
setval(bug,[]),
@@ -1150,7 +1164,7 @@ smt_test0(TO,Size,StrDir,CI) :-
USS = "use_simplex,"
; USS = "no_simplex,"),
% Nombre de tentatives en CI
- getval(nbTryCI,NbTryCI),
+ getval(nbTryCI,NbTryCI)@eclipse,
(CI == 0 ->
NbFiles = NbFiles0,
NbTry = 1
@@ -1277,6 +1291,64 @@ set_colibri_tests_unsat_status :-
fail);
true).
*/
+
+:- lib(toplevel).
+interrupt_colibri :-
+ (current_module(toplevel) ->
+ interrupt_colibri_fg
+ ; interrupt_colibri_bg).
+
+interrupt_colibri_fg :-
+ repeat,
+ writeln(user,"\nPlease choose among:"),
+ write(user," a(abort), b(break), c(continue), d(switch debug infos on/off),"
+ " e(exit), m(make) ? "),
+ flush(user),
+ tyi(C),
+ ( C == 0'a -> (writeln(user,abort),
+ exit_block(abort))
+ ; C == 0'e -> (writeln(user,exit),
+ halt)
+ ; C == 0'd -> (getval(gdbg,N),
+ (N == 0 ->
+ NewN = 1,
+ OnOff = on
+ ; NewN = 0,
+ OnOff = off),
+ write(user,"debugging "),
+ writeln(user,OnOff),
+ setval(gdbg,NewN))
+ ; C == 0'b -> toplevel:break
+ ; C == 0'c -> writeln(user,continue)
+ ; C == 0'm -> (writeln(user,make),
+ deactivate_check_pu,
+ make,
+ activate_check_pu)
+ ; fail),!.
+
+
+interrupt_colibri_bg :-
+ repeat,
+ writeln(user,"\nPlease choose among:"),
+ write(user," a(abort), e(exit), d(switch debug on/off), b(break) ? "),
+ flush(user),
+ tyi(C),
+ ( C == 0'a -> (writeln(user,abort),
+ exit_block(abort))
+ ; C == 0'e -> (writeln(user,exit),
+ halt)
+ ; C == 0'd -> (getval(gdbg,N),
+ (N == 0 ->
+ NewN = 1,
+ OnOff = on
+ ; NewN = 0,
+ OnOff = off),
+ write(user,"debugging "),
+ writeln(user,OnOff),
+ setval(gdbg,NewN))
+ ; C == 0'b -> toplevel:break
+ ; fail),!.
+
repeatN :-
repeat,
getval(nb_try,Nb),
@@ -1290,13 +1362,18 @@ smt_unit_test(TO) :-
smt_unit_test_CI(TO) :-
smt_unit_test(TO,1).
-% pour limiter les bv à 256, sinon pbs de TO pas déclenchés !
-:- setval(unit_tests,0)@eclipse.
-
smt_unit_test(TO,CI) :-
- setval(unit_tests,1)@eclipse,
- setval(bug,[]),
- StrDir = "./colibri_tests/colibri/tests/sat/", % 0
+ %StrDir = "./UnitTests/sat/",
+ %StrDir = "./UnitTests/unsat/",
+ %StrDir = "./UnitTests/unsat/QF_ABV/",
+ %StrDir = "./UnitTests/sat/QF_ABV/",
+
+ %StrDir = "./UnitTests/sat/QF_ABV/",
+ %StrDir = "./UnitTests/sat/QF_BV/",
+ %StrDir = "./UnitTests/sat/QF_NIA/",
+
+ %StrDir = "./colibri_tests/colibri/tests/sat/", % 0 (en 15s, 1 en
+ % 2s newton)
%StrDir = "./colibri_tests/colibri/tests/unsat/", % 0
@@ -1307,137 +1384,146 @@ smt_unit_test(TO,CI) :-
%StrDir = "./smtlib_schanda-master/random/fp.mul/",
%StrDir = "./smtlib_schanda-master/nyxbrain/",
%StrDir = "./smtlib_schanda-master/spark_2014/",
+
+%-----------------------------------------------------------------------
+ %StrDir = "./QF_AUFBVFP/20210301-Alive2/",% 1/1
%------------------------------------------------------------------------
- %StrDir = "./QF_ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/",% 0
- %StrDir = "./QF_ABVFPLRA/20170501-Heizmann-UltimateAutomizer/",% 0
+ %StrDir = "./QF_ABVFPLRA/", % 3/74
+ %StrDir = "./QF_ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/",% 0/41
+ %StrDir = "./QF_ABVFPLRA/20170501-Heizmann-UltimateAutomizer/",% 0/33
%------------------------------------------------------------------------
- %StrDir = "./QF_ABVFP/20170428-Liew-KLEE/", % 79 TO (69 sans simplex) (cvc4 76)
- %StrDir = "./QF_ABVFP/20170501-Heizmann-UltimateAutomizer/", % 0 TO
+ %StrDir = "./QF_ABVFP/",
+ %StrDir = "./QF_ABVFP/20170428-Liew-KLEE/", % 232/18033 TO (1 I,
+ % 177 u) (69 sans simplex) (cvc4 76)
+ %StrDir = "./QF_ABVFP/20170501-Heizmann-UltimateAutomizer/", % 0/96 TO
%------------------------------------------------------------------------
%StrDir = "./QF_BVFP/",
- %StrDir = "./QF_BVFP/20170428-Liew-KLEE/", % 33-76 ()
- %StrDir = "./QF_BVFP/20170501-Heizmann-UltimateAutomizer/", % 0 TO
- %StrDir = "./QF_BVFP/ramalho/", % 0 TO
- %StrDir = "./QF_BVFP/schanda/spark/", % 1 TO
+ %StrDir = "./QF_BVFP/20170428-Liew-KLEE/", % 131/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
%------------------------------------------------------------------------
%StrDir = "./QF_UFFP/schanda/spark/",% 0/2 TO
%------------------------------------------------------------------------
- %StrDir = "./QF_FPLRA/20170501-Heizmann-UltimateAutomizer/",% 0/3 TO
- %StrDir = "./QF_FPLRA/20190429-UltimateAutomizerSvcomp2019/",% 0/8 TO
+ %StrDir = "./QF_FPLRA/",
+ %StrDir = "./QF_FPLRA/20170501-Heizmann-UltimateAutomizer/",% 0/4 TO
+ %StrDir = "./QF_FPLRA/20190429-UltimateAutomizerSvcomp2019/",% 0/38 TO
%StrDir = "./QF_FPLRA/schanda/spark/",% 0/2 TO
- %StrDir = "./QF_FPLRA/2019-Gudemann/",% 2/13 (11)
+ %StrDir = "./QF_FPLRA/2019-Gudemann/",% 2/13 (3/13 en 2s)
%------------------------------------------------------------------------
+ %StrDir = "./QF_BVFPLRA/",
%StrDir = "./QF_BVFPLRA/20170501-Heizmann-UltimateAutomizer/",% 0/15 TO
- %StrDir = "./QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/",% 8/
- %152
- %
- % (11 u)
+ %StrDir = "./QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/",% 8/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/ramalho/",% 0/38 T0
- %StrDir = "./QF_FP/griggio/", % 50 TO en 24s (cvc4 90 en 60s)
- %StrDir = "./QF_FP/schanda/spark/",% 7 TO
- %StrDir = "./QF_FP/wintersteiger/", % 0 TO
+ %StrDir = "./QF_FP/ramalho/",% 1/38 T0 (5/38 en 2s)
+ %StrDir = "./QF_FP/griggio/", % 49 TO en 24s (cvc4 90 en 60s) (65/214 en 2s)
+ %StrDir = "./QF_FP/schanda/spark/",% 6/46 TO (7 en 2s)
+ %StrDir = "./QF_FP/wintersteiger/", % 0/39994
+%-----------------------------------------------------------------------
+ %StrDir = "./QF_UFFP/schanda/",% 0/2
%------------------------------------------------------------------------
- %StrDir = "QF_AX/", % 14/551
- %StrDir = "QF_AX/storeinv/",
- %StrDir = "QF_AX/swap/",
- %StrDir = "QF_AX/storecomm/",
- %StrDir = "QF_AX/cvc/",
+ %StrDir = "QF_AX/", % 75/551
+ %StrDir = "QF_AX/storeinv/", % 6/38
+ %StrDir = "QF_AX/swap/", % 14/302
+ %StrDir = "QF_AX/storecomm/", % 46/210
+ %StrDir = "QF_AX/cvc/", % 0/1
%----------------------------------------------------------------------
- %StrDir = "./QF_BV/",
+% %StrDir = "./QF_BV/",
%StrDir = "./QF_BV/20170501-Heizmann-UltimateAutomizer/",% 0/1
-
%StrDir = "./QF_BV/20170531-Hansen-Check/", % 0/3
%StrDir = "./QF_BV/2017-BuchwaldFried/", % 3/4
- %StrDir = "./QF_BV/2018-Goel-hwbench/",
- %StrDir = "./QF_BV/2019-Mann/", %2/2
- %StrDir = "./QF_BV/2019-Wolf-fmbench/", % too big
+ %StrDir = "./QF_BV/2018-Goel-hwbench/", % 5/45 (9 I)
+ %StrDir = "./QF_BV/2019-Mann/", % 1/1 (1 I)
+ %StrDir = "./QF_BV/2019-Wolf-fmbench/", % 14 too big
%StrDir = "./QF_BV/20200415-Yurichev/", % 1/1
- %StrDir = "./QF_BV/bmc-bv-svcomp14/", % 8/24 (8 I)
+
+ %StrDir = "./QF_BV/bmc-bv-svcomp14/", % 18/24 (8 I)
%StrDir = "./QF_BV/calypto/", % 20/23
%StrDir = "./QF_BV/challenge/", % 2/2
%StrDir = "./QF_BV/check2/", % 0/6
%StrDir = "./QF_BV/dwp_formulas/", % 0/332
- %StrDir = "./QF_BV/ecc/", % 0/1 (7 I) NULL comparé a cvc4
- %StrDir = "./QF_BV/float/", % 78/89 (120 I)
+ %StrDir = "./QF_BV/ecc/", % 0/1 (7 I)
+ %StrDir = "./QF_BV/float/", % 80/89 (120 I)
%StrDir = "./QF_BV/galois/", % 4/4
%StrDir = "./QF_BV/gulwani-pldi08/", % 5/6
- %StrDir = "./QF_BV/log-slicing/", % 208 (unsupported ou TO sans limite)
- %StrDir = "./QF_BV/mcm/", % 108/108
+ %StrDir = "./QF_BV/log-slicing/", % 208/208
+ %StrDir = "./QF_BV/mcm/", % 108/108 (75 I)
%StrDir = "./QF_BV/pipe/", % 1/1
%StrDir = "./QF_BV/pspace/", % 23/86
%StrDir = "./QF_BV/rubik/", % 6/6 (1 I)
%StrDir = "./QF_BV/RWS/", % 19/19 (1 I)
-
%StrDir = "./QF_BV/sage/",
- %StrDir = "./QF_BV/sage/app1/", % 31/2676
- %StrDir = "./QF_BV/sage/app2/", % 1/1346
- %StrDir = "./QF_BV/sage/app5/", % 2/1103
- %StrDir = "./QF_BV/sage/app6/", % 0/1345
+ % Il suffit pour couvrir sage
%StrDir = "./QF_BV/sage/app7/", % 11/4813 (3850 I)
- %StrDir = "./QF_BV/sage/app8/", % 15/2756
- %StrDir = "./QF_BV/sage/app9/", % 16/3301
+/*
+ %StrDir = "./QF_BV/sage/app1/", % 42/2676
+ %StrDir = "./QF_BV/sage/app2/", % 1/1346 (71 I)
+ %StrDir = "./QF_BV/sage/app5/", % 2/1103
+ %StrDir = "./QF_BV/sage/app6/", % 0/245
+ %StrDir = "./QF_BV/sage/app8/", % 32/2756
+ %StrDir = "./QF_BV/sage/app9/", % 38/3301
%StrDir = "./QF_BV/sage/app10/", % 0/51
%StrDir = "./QF_BV/sage/app11/", % 611 too big
- %StrDir = "./QF_BV/sage/app12/", % 12/5784
- %StrDir = "./QF_BV/spear/", % 501/807 (888 I)
- %StrDir = "./QF_BV/stp_samples/", % 45/426
+ %StrDir = "./QF_BV/sage/app12/", % 17/5784
+*/
+ %StrDir = "./QF_BV/spear/", % 531/807 (888 I)
+ %StrDir = "./QF_BV/stp_samples/", % 47/426
%StrDir = "./QF_BV/tacas07/", % 3/3 (2 I)
%StrDir = "./QF_BV/uclid/", % 0/4 (410 I)
- %StrDir = "./QF_BV/uclid_contrib_smtcomp09/", 7/7
+ %StrDir = "./QF_BV/uclid_contrib_smtcomp09/", % 7/7
%StrDir = "./QF_BV/uum/", % 8/8
%StrDir = "./QF_BV/VS3/", % 10/10 (1 I)
%StrDir = "./QF_BV/wienand-cav2008/", % 3/15 (3 I)
-
%StrDir = "./QF_BV/asp/", % 35/35 (356 I)
%StrDir = "./QF_BV/bench_ab/", % 0/285
- %StrDir = "./QF_BV/bmc-bv/", % 7/26 (4 I)
- %StrDir = "./QF_BV/bmc-bv-svcomp14/", % 8/24 (8 I)
- %StrDir = "./QF_BV/brummayerbiere/", % 38/52
- %StrDir = "./QF_BV/brummayerbiere2/", % 30/65 (22 u)
+ %StrDir = "./QF_BV/bmc-bv/", % 9/26 (4 I)
+ %StrDir = "./QF_BV/bmc-bv-svcomp14/", % 18/24 (8 I)
+
+ %StrDir = "./QF_BV/brummayerbiere/", % 46/52
+
+ %StrDir = "./QF_BV/brummayerbiere2/", % 44/65
%StrDir = "./QF_BV/brummayerbiere3/", % 73/73 (6 I)
%StrDir = "./QF_BV/brummayerbiere4/", % 0/10
- %StrDir = "./QF_BV/bruttomesso/", % plein de TO
+ %StrDir = "./QF_BV/bruttomesso/", % 893 TO (83 I)
%StrDir = "./QF_BV/crafted/", % 6/21
%-----------------------------------------------------------------------
-
- %StrDir = "QF_ABV/bench_ab/", % 0/117
- %StrDir = "QF_ABV/bmc-arrays/", % 12/20 (19 I)
- %StrDir = "QF_ABV/brummayerbiere/", %TROP DUR
- %StrDir = "QF_ABV/btfnt/", %TROP DUR
- %StrDir = "QF_ABV/calc2/", %TROP DUR
- %StrDir = "QF_ABV/dwp_formulas/", %TRES DUR
- %StrDir = "QF_ABV/ecc/", %TRES DUR
- %StrDir = "QF_ABV/egt/",
-
- %StrDir = "QF_ABV/jager/",
- %StrDir = "QF_ABV/klee-selected-smt2/",
-
+ %StrDir = "QF_ABV/",
+ %StrDir = "QF_ABV/bench_ab/", % 0/117 (2 I)
+ %StrDir = "QF_ABV/bmc-arrays/", % 13/20 (19 I)
+ %StrDir = "QF_ABV/brummayerbiere/", % 236/286 I) (2s, 7 I)
+ %StrDir = "QF_ABV/btfnt/", % 1/1
+ %StrDir = "QF_ABV/calc2/", % 12/18 (18 I)
+ %StrDir = "QF_ABV/dwp_formulas/", % 2399/5730 (35 I)
+ %StrDir = "QF_ABV/ecc/", % 25/41 (11 I)
+ %StrDir = "QF_ABV/egt/", % 1/7687 (32 I)
+ %StrDir = "QF_ABV/jager/", % 2 too big
+ %StrDir = "QF_ABV/klee-selected-smt2/", % 256/350 (245 I)
+%-----------------------------------------------------------------------
%StrDir = "QF_ALIA/", % 63/114 (1 I)
- %StrDir = "QF_ALIA/qlock2/", % 45/52
- %StrDir = "QF_ALIA/cvc/", % 4/5
- %StrDir = "QF_ALIA/UltimateAutomizer/",% 4/8
+ %StrDir = "QF_ALIA/qlock2/", % 52/52
+ %StrDir = "QF_ALIA/cvc/", % 5/5
+ %StrDir = "QF_ALIA/UltimateAutomizer/",% 5/8
%StrDir = "QF_ALIA/UltimateAutomizer2/",% 1/4 (1 I)
%StrDir = "QF_ALIA/piVC/", % 6/15
%StrDir = "QF_ALIA/ios/", % 0/30
+%-----------------------------------------------------------------------
+ %StrDir = "QF_NIA/", !!!! pleins de unknown sur check_sat_vars !!!!
+% %StrDir = "QF_NIA/20170427-VeryMax/", %Que des TO
- %StrDir = "QF_NIA/",
- %StrDir = "QF_NIA/20170427-VeryMax/", %Que des TO
- %StrDir = "QF_NIA/20170427-VeryMax/ITS/", %Que des TO
- %StrDir = "QF_NIA/20170427-VeryMax/CInteger/", %Que des TO
- %StrDir = "bugs_CInteger/", % 4/8
- %StrDir = "QF_NIA/AProVE/", % 1484/2406 (3 I)
- %StrDir = "bugs_NIA/", % 6/6
- %StrDir = "QF_NIA/calypto/", % 6/117
- %StrDir = "QF_NIA/LassoRanker/",% 52/106
+ %StrDir = "QF_NIA/20170427-VeryMax/ITS/", % 14865/15371 (1675 I)
+ %StrDir = "QF_NIA/20170427-VeryMax/CInteger/", % 19105 Que des TO
+ %StrDir = "QF_NIA/AProVE/", % 1477/2406 (3 I)
+ %StrDir = "QF_NIA/calypto/", % 24/117
+ %StrDir = "QF_NIA/LassoRanker/",% 83/106
%StrDir = "QF_NIA/LCTES/",% 2/2
- %StrDir = "QF_NIA/leipzig/", % 126/167
+ %StrDir = "QF_NIA/leipzig/", % 142/167
%StrDir = "QF_NIA/mcm/",% 162/162 (24 I)
%StrDir = "QF_NIA/UltimateAutomizer/",% 0/7
%StrDir = "QF_NIA/UltimateLassoRanker/",% 0/4
-
+%-----------------------------------------------------------------------
+ %StrDir = "QF_LIA/",
%StrDir = "QF_LIA/20180326-Bromberger/more_slacked/CAV_2009_benchmarks/coef-size/smt/size-10/", % 5/6
%StrDir = "QF_LIA/20180326-Bromberger/more_slacked/cut_lemmas/10-vars/",% 4/7
%StrDir = "QF_LIA/20180326-Bromberger/unbd-sage/unbd010v15c/",% 25/25
@@ -1446,17 +1532,86 @@ smt_unit_test(TO,CI) :-
%StrDir = "QF_LIA/arctic-matrix/",% 5/5 (95 I)
%StrDir = "QF_LIA/check/", % 0/5
%StrDir = "QF_LIA/RTCL/", % 0/2
- %StrDir = "QF_LIA/miplib2003/", % too big
- %StrDir = "QF_LIA/rings_preprocessed/", % 288/294
- %StrDir = "QF_LIA/mathsat/", % 51/91
- %StrDir = "QF_LIA/CAV_2009_benchmarks/smt/", % 508/540
- %StrDir = "QF_LIA/rings/", % 278/294
- %StrDir = "QF_LIA/fft/", % 7/9
-
+ %StrDir = "QF_LIA/miplib2003/", % 16 too big
+ %StrDir = "QF_LIA/rings_preprocessed/", % 292/294
+ %StrDir = "QF_LIA/mathsat/", % 58/91 (30 I)
+ %StrDir = "QF_LIA/CAV_2009_benchmarks/smt/", % 518/540
+ %StrDir = "QF_LIA/rings/", % 294/294
+ %StrDir = "QF_LIA/fft/", % 9/9
+%-----------------------------------------------------------------------
%StrDir = "QF_ANIA/",% 0/1 (7 I)
+%-----------------------------------------------------------------------
+ %StrDir = "./QF_LRA/", % 460/573 (61 I)
+ %StrDir = "./QF_LRA/2017-Heizmann-UltimateInvariantSynthesis/",
+ % 29/29 (29 I)
+ %StrDir = "./QF_LRA/DTP-Scheduling/", % 84/86 (5 I)
+ %StrDir = "./QF_LRA/LassoRanker/", % 31/31 (389 I)
+ %StrDir = "./QF_LRA/latendresse/", % 10/10 (8 I)
+ %StrDir = "./QF_LRA/miplib/", % 40/42
+ %StrDir = "./QF_LRA/check/", % 0/2
+ %StrDir = "./QF_LRA/keymaera/", % 0/21
+ %StrDir = "./QF_LRA/meti-tarski/", % 0/31
+ %StrDir = "./QF_LRA/sal/", % 34/107
+ %StrDir = "./QF_LRA/sc/", % 116/144
+ %StrDir = "./QF_LRA/spider_benchmarks/", % 24/42
+ %StrDir = "./QF_LRA/TM/", % 10/10 (15 I)
+ %StrDir = "./QF_LRA/tropical-matrix/", % 6/6 (4 Ignored)
+ %StrDir = "./QF_LRA/uart/", % 73/73
+ %StrDir = "./QF_LRA/tta_startup/", % 48/72
+%-----------------------------------------------------------------
+ StrDir = "./QF_UF/",
+ %StrDir = "./QF_UF/20170829-Rodin/",
+ %StrDir = "./QF_UF/2018-Goel-hwbench/",
+ %StrDir = "./QF_UF/eq_diamond/",
+ %StrDir = "./QF_UF/NEQ/",
+ %StrDir = "./QF_UF/PEQ/",
+ %StrDir = "./QF_UF/QG-classification/",
+ %StrDir = "./QF_UF/SEQ/",
+ %StrDir = "./QF_UF/TypeSafe/",
+%----------------------------------------------------------------
+ %StrDir = "./QF_AUFBV/",
+ %StrDir = "./QF_AUFBV/2019-Gonzalvez/",
+ %StrDir = "./QF_AUFBV/2019-Wolf-fmbench/",
+ %StrDir = "./QF_AUFBV/ecc/",
+%----------------------------------------------------------------
+ %StrDir = "QF_UFIDL/",
+ %StrDir = "./QF_UFIDL/mathsat/EufLaArithmetic/vhard/",
+ %StrDir = "./QF_UFIDL/pete/",
+ %StrDir = "./QF_UFIDL/pete2/",
+ %StrDir = "./QF_UFIDL/pete3/",
+ %StrDir = "./QF_UFIDL/RDS/",
+ %StrDir = "./QF_UFIDL/RTCL/",
+ %StrDir = "./QF_UFIDL/TwoSquares/",
+ %StrDir = "./QF_UFIDL/uclid/",
+ %StrDir = "./QF_UFIDL/uclid2/", % 13/13
+ %StrDir = "./QF_UFIDL/UCLID-pred/",
+%----------------------------------------------------------------
+ %StrDir = "./QF_UFLIA/",
+ %StrDir = "./QF_UFLIA/mathsat/",
+ %StrDir = "./QF_UFLIA/TwoSquares/",
+ %StrDir = "./QF_UFLIA/wisas/", %
+%----------------------------------------------------------------
+ %StrDir = "./QF_UFLRA/",
+ %StrDir = "./QF_UFLRA/cpachecker-bmc-svcomp14/",
+ %StrDir = "./QF_UFLRA/cpachecker-induction-svcomp14/",
+ %StrDir = "./QF_UFLRA/FFT/",
+ %StrDir = "./QF_UFLRA/mathsat/",
+%----------------------------------------------------------------
+ smt_unit_test(StrDir,TO,CI).
+
+smt_unit_test(StrDir0,TO,CI) :-
+ (atom(StrDir0) ->
+ atom_string(StrDir0,StrDir)
+ ; StrDir = StrDir0),
+ toplevel_init(tty),
+ set_interrupt_handler(int,interrupt_colibri/0),
+ setval(bug,[]),
os_file_name(StrDir,OS_Examples),
((StrDir == "./QF_FP/wintersteiger/";
+ StrDir = "./QF_BVFP/";
+ StrDir == "QF_LIA/";
+ StrDir == "QF_UFIDL/";
StrDir == "./QF_BVFP/schanda/spark/")
->
read_directory(OS_Examples,"*/*",SubdirList0,_)
@@ -1470,7 +1625,7 @@ smt_unit_test(TO,CI) :-
fromto(0,ITB,OTB,TooBig),
fromto(0,IMS,OMS,MaxSizeSeen),
param(StrDir,MaxSize) do
- append_strings(StrDir,Dir,SubDir),
+ concat_string([StrDir,Dir],SubDir),
os_file_name(SubDir,OS_SubDir),
read_directory(OS_SubDir, "*.smt2", _, SmtList),
(foreach(F,SmtList),
@@ -1495,13 +1650,15 @@ smt_unit_test(TO,CI) :-
getval(use_delta,UD)@eclipse,
getval(use_simplex,US)@eclipse,
length(SmtFileList,NFs0),
- getval(nbTryCI,NbTryCI),
+ getval(nbTryCI,NbTryCI)@eclipse,
+ %NbTryCI = 4,
(CI == 1 ->
+ Test = 1,
NFs is NFs0 * NbTryCI,
- NbTry = NbTryCI,
- Test = 1
+ NbTry = NbTryCI
; NFs = NFs0,
NbTry = 1),
+
( member(F,SmtFileList),
setval(nb_try,NbTry),
repeatN,
@@ -1513,49 +1670,195 @@ smt_unit_test(TO,CI) :-
setval(use_delta,UD)@eclipse,
setval(use_simplex,US)@eclipse,
- %set_flag(occur_check,on),
-
% On passe en mode comptage du nombre de steps
show_stats,
- not not (seed(0),
- smt_solve_bis(Test,F,TO,Code),
- setval(init_code,Code)),
+ block(not not (seed(0),
+ smt_solve_bis(Test,F,TO,Code),
+ setval(init_code,Code)),
+ Tag,
+ (Tag == timeout_col ->
+ setval(init_code,3)
+ ; exit_block(Tag))),
+
+ getval(logic,Logic),
+
getval(init_code,Code),
incNbCode(Code),
(Code == 2 ->
- getval(bug,Bugs),
- setval(bug,[F|Bugs])
- ; (Code == 3 ->
- incval(nbTO)
- ; true)),
+ ((CI == 1,
+ getval(make_UT,0)@eclipse)
+ ->
+ % on est en mode check avec scrambler
+ writeln(output,bug:F),
+ exit(4)
+ ; true),
+ getval(bug,Bugs),
+ (getval(smt_status,unknown)@eclipse ->
+ setval(bug,[smt_unknown:F|Bugs])
+ ; setval(bug,[F|Bugs]))
+ ; (Code == 3 ->
+ incval(nbTO)
+ ; pathname(F,PF,NF),
+ (Code > 2 ->
+ true
+ ; (Code == 0 ->
+ concat_string(["UnitTests/unsat/",Logic,"/"],TargetDir)
+ ; % Code == 1
+ concat_string(["UnitTests/sat/",Logic,"/"],TargetDir)),
+ (exists(TargetDir) ->
+ true
+ ; append_strings("mkdir ",TargetDir,Mkd),
+ system(Mkd)),
+ concat_string([TargetDir,NF],TargetFile),
+ (exists(TargetFile) ->
+ true
+ ; concat_string(["cp ",F," ",TargetDir],Cp),
+ system(Cp))))),
garbage_collect,
fail
; true),
+ call(spy_here)@eclipse,
+ (getval(make_UT,1)@eclipse ->
+ Slog = output
+ ; % on est en check
+ pathname(StrDir,Path,Base,Suffix),
+ (append_strings(BegF,"/",Base) ->
+ true
+ ; BegF = Base),
+ concat_string([Path,BegF,".log"],Flog),
+ open(Flog,write,Slog)),
+
getval(nbFile,NbFile),
- writeln(output,"Files":NbFile),
+ writeln(Slog,"Files":NbFile),
(TooBig > 0 ->
- write(output,"Ignored Too Big Files (> "),
- write(output,MaxSize),
- writeln(output,"k)":TooBig),
- writeln(output,"MaxSizeSeen":MaxSizeSeen)
+ write(Slog,"Ignored Too Big Files (> "),
+ write(Slog,MaxSize),
+ writeln(Slog,"k)":TooBig),
+ writeln(Slog,"MaxSizeSeen":MaxSizeSeen)
; true),
getval(nb0,Nb0),
- writeln(output,"Unsat":Nb0),
+ (Nb0 > 0 ->
+ writeln(Slog," Unsat":Nb0)
+ ; true),
getval(nb1,Nb1),
- writeln(output,"Sat":Nb1),
+ (Nb1 > 0 ->
+ writeln(Slog," Sat":Nb1)
+ ; true),
getval(nb2,Nb2),
- writeln(output,"Error":Nb2),
+ (Nb2 > 0 ->
+ writeln(Slog," Error":Nb2)
+ ; true),
getval(nb3,Nb3),
- writeln(output,"Timeout":Nb3),
+ (Nb3 > 0 ->
+ writeln(Slog," Timeout":Nb3)
+ ; true),
getval(nb5,Nb5),
- writeln(output,"Unsupported":Nb5),
+ (Nb5 > 0 ->
+ writeln(Slog," Unsupported":Nb5)
+ ; true),
getval(bug,Bugs),
(Bugs == [] ->
true
; nl(output),
- writeln(output,"BUGS:"),
- (foreach(B,Bugs) do
- writeln(output,B))).
+ writeln(Slog," BUGS:"),
+ (foreach(B,Bugs),
+ param(Slog) do
+ writeln(Slog,B))),
+ (getval(make_UT,1)@eclipse ->
+ true
+ ; close(Slog)).
+
+:- setval(make_UT,1)@eclipse.
+
+
+make_unit_tests(TO,Mod) :-
+ (Mod == 1 ->
+ setval(force_model,1)@eclipse
+ ; setval(force_model,0)@eclipse),
+ make_unit_tests(TO).
+make_unit_tests(TO) :-
+ setval(make_UT,1)@eclipse,
+ smt_unit_test(TO).
+
+check_unit_tests(SatUnsat,TO,Mod) :-
+ (Mod == 1 ->
+ setval(force_model,1)@eclipse
+ ; setval(force_model,0)@eclipse),
+ check_unit_tests(SatUnsat,TO).
+
+check_unit_tests(SatUnsat,TO) :-
+ Sat = ["./UnitTests/sat/ALL/",
+ "./UnitTests/sat/QF_ABVFPLRA/",
+ "./UnitTests/sat/QF_AX/",
+ "./UnitTests/sat/QF_BVFPLRA/",
+ "./UnitTests/sat/QF_LIA/",
+ "./UnitTests/sat/QF_UF/",
+ "./UnitTests/sat/QF_UFLRA/",
+ "./UnitTests/sat/QF_ABV/",
+ "./UnitTests/sat/QF_ALIA/",
+ "./UnitTests/sat/QF_BV/",
+ "./UnitTests/sat/QF_FP/",
+ "./UnitTests/sat/QF_LRA/",
+ "./UnitTests/sat/QF_UFIDL/",
+ "./UnitTests/sat/QF_ABVFP/",
+ "./UnitTests/sat/QF_AUFBV/",
+ "./UnitTests/sat/QF_BVFP/",
+ "./UnitTests/sat/QF_FPLRA/",
+ "./UnitTests/sat/QF_NIA/",
+ "./UnitTests/sat/QF_UFLIA/"],
+
+ Unsat = ["./UnitTests/unsat/ALL/",
+ "./UnitTests/unsat/AUFBVFPDTNIRA/",
+ "./UnitTests/unsat/QF_ABV/",
+ "./UnitTests/unsat/QF_ABVFP/",
+ "./UnitTests/unsat/QF_ABVFPLRA/",
+ "./UnitTests/unsat/QF_ALIA/",
+ "./UnitTests/unsat/QF_AUFBV/",
+ "./UnitTests/unsat/QF_AX/",
+ "./UnitTests/unsat/QF_BV/",
+ "./UnitTests/unsat/QF_BVFP/",
+ "./UnitTests/unsat/QF_BVFPLRA/",
+ "./UnitTests/unsat/QF_FP/",
+ "./UnitTests/unsat/QF_FPLRA/",
+ "./UnitTests/unsat/QF_LIA/",
+ "./UnitTests/unsat/QF_LRA/",
+ "./UnitTests/unsat/QF_NIA/",
+ "./UnitTests/unsat/QF_UF/",
+ "./UnitTests/unsat/QF_UFFP/",
+ "./UnitTests/unsat/QF_UFIDL/",
+ "./UnitTests/unsat/QF_UFLIA/",
+ "./UnitTests/unsat/QF_UFLRA/"],
+
+ (SatUnsat == sat ->
+ Dirs = Sat
+ ; (SatUnsat == unsat ->
+ Dirs = Unsat
+ ; Dirs = ["./UnitTests/bug/"])),
+ get_flag(version_as_list,[Ver|_]),
+ ((Ver == 7) ->
+ ECLIPSE = eclipse7,
+ COL = "col_solve.eco"
+ ; ECLIPSE = eclipse,
+ COL = "col_solve.pl"),
+ Scr = 1,
+ (foreach(Dir,Dirs),
+ param(TO,ECLIPSE,Scr) do
+ concat_string([ECLIPSE,
+ " -b col_solve.pl -g 5000M -e \"setval(make_UT,0)@eclipse,smt_unit_test('",
+ Dir,
+ "',",
+ TO,
+ ",",
+ Scr,
+ ")\""
+ ],Com),
+ % writeln(Com),
+ exec(Com,[],Pid),
+ wait(Pid,CodeExt),
+ (CodeExt =:= 4*256 ->
+ halt
+ ; true)).
+
show_stats :-
setval(step_stats,1)@eclipse,
diff --git a/Src/COLIBRI/colibri.pl b/Src/COLIBRI/colibri.pl
index 03e9cbce5..634cdf45f 100755
--- a/Src/COLIBRI/colibri.pl
+++ b/Src/COLIBRI/colibri.pl
@@ -129,6 +129,9 @@ init_colibri :-
%% Variables globalles creees dans le module eclipse
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ % pour les tests de get-model
+ setval(force_model,0)@eclipse,
+
% Si gdbg vaut 1, affichages de debug
setval(gdbg,1)@eclipse, %PMO mise a 1 pour identifier les erreurs eventuelles
% Valeurs de MinInt et MaxInt par defaut
diff --git a/Src/COLIBRI/mbv_propa.pl b/Src/COLIBRI/mbv_propa.pl
index 112127292..b9a1aa753 100644
--- a/Src/COLIBRI/mbv_propa.pl
+++ b/Src/COLIBRI/mbv_propa.pl
@@ -104,7 +104,7 @@ bveq(Sx, X, Sy, Y):-
((var(X),
var(Y))
->
- suspend(bveq(Sx, X, Sy, Y), 0, [X,Y] -> suspend:constrained)
+ my_suspend(bveq(Sx, X, Sy, Y), 0, [X,Y] -> suspend:constrained)
; protected_unify(X,Y) )),
set_priority(Prio),
@@ -213,7 +213,7 @@ bvand_bis(M,X,Y,Z) :-
fill_bvbounds(Z,NDZ),
bvand_inst_free(M,X,Y,Z,Continue1),
(nonvar(Continue1) ->
- suspend(bvand_bis(M,X,Y,Z), 0, (X,Y,Z) -> suspend:constrained)
+ my_suspend(bvand_bis(M,X,Y,Z), 0, (X,Y,Z) -> suspend:constrained)
; true))),
set_priority(Prio),
wake_if_other_scheduled(Prio).
@@ -453,7 +453,7 @@ bvor_bis(M,X,Y,Z) :-
fill_bvbounds(Z,NDZ),
bvor_inst_free(M,X,Y,Z,Continue1),
(nonvar(Continue1) ->
- suspend(bvor_bis(M,X,Y,Z), 0, (X,Y,Z) -> suspend:constrained)
+ my_suspend(bvor_bis(M,X,Y,Z), 0, (X,Y,Z) -> suspend:constrained)
; true))),
set_priority(Prio),
wake_if_other_scheduled(Prio).
@@ -615,11 +615,13 @@ bvxor_bis(M,X,Y,Z) :-
fill_bvbounds(Z,NDZ),
bvxor_inst_free(M,X,Y,Z,Continue1),
(nonvar(Continue1) ->
- suspend(bvxor_bis(M,X,Y,Z), 0, (X,Y,Z) -> suspend:constrained)
+ my_suspend(bvxor_bis(M,X,Y,Z), 0, (X,Y,Z) -> suspend:constrained)
; true))),
set_priority(Prio),
wake_if_other_scheduled(Prio).
+bvxor_inst_free(_M,A,A,C,_Continue) ?- !,
+ protected_unify(C,0).
bvxor_inst_free(M,A,B,C,Continue) :-
Mask is \ ( (- 1) << M),
((integer(A),
@@ -733,7 +735,7 @@ bvnot_bis(M,X,Z) :-
fill_bvbounds(Z,NDZ),
bvnot_inst_free(M,X,Z,Continue1),
(nonvar(Continue1) ->
- suspend(bvnot_bis(M,X,Z), 0, ([X,Z] -> suspend:constrained))
+ my_suspend(bvnot_bis(M,X,Z), 0, ([X,Z] -> suspend:constrained))
; true))),
set_priority(Prio),
wake_if_other_scheduled(Prio).
@@ -784,7 +786,7 @@ bvsl(M,X,Y,Z) :-
Y == YY)
->
protected_unify(Z,ZZ)
- ; suspend(bvsl(M,X,Y,Z), 0, [Y] -> suspend:inst)).
+ ; my_suspend(bvsl(M,X,Y,Z), 0, [Y] -> suspend:inst)).
bvsl(M,X,Y,Z) :-
bulk_lazy_doms([X,Z],M),
@@ -849,7 +851,7 @@ bvsl_bis(M,X,Y,Z) :-
lin_mult_int(Coeff,X,Z)
; true),
(nonground((X,Z)) ->
- suspend(bvsl_bis(M,X,Y,Z), 0, ([X , Z] -> suspend:constrained))
+ my_suspend(bvsl_bis(M,X,Y,Z), 0, ([X , Z] -> suspend:constrained))
; true)
; true)),
set_priority(Prio),
@@ -950,7 +952,7 @@ bvsr(M,X,Y,Z) :-
Y == YY)
->
protected_unify(Z,ZZ)
- ; suspend(bvsr(M,X,Y,Z), 0, [X,Y] -> suspend:constrained)).
+ ; my_suspend(bvsr(M,X,Y,Z), 0, [X,Y] -> suspend:constrained)).
bvsr(M,X,Y,Z) :-
bulk_lazy_doms([X,Z],M),
@@ -1020,7 +1022,7 @@ bvsr_bis(M,X,Y,Z) :-
lin_mult_int(Coeff,Z,X)
; true),
(nonground((X,Z)) ->
- suspend(bvsr_bis(M,X,Y,Z), 0, ([X,Z] -> suspend:constrained))
+ my_suspend(bvsr_bis(M,X,Y,Z), 0, ([X,Z] -> suspend:constrained))
; true)
; true)),
set_priority(Prio),
@@ -1109,7 +1111,7 @@ bvlsr(M, X, Y, Z) :-
bvasr(M,X,Y,Z) :-
var(Y), !,
- suspend(bvasr(M,X,Y,Z), 0, [Y] -> suspend:inst).
+ my_suspend(bvasr(M,X,Y,Z), 0, [Y] -> suspend:inst).
bvasr(M,X,0,Z) ?- !,
protected_unify(X,Z).
@@ -1364,7 +1366,7 @@ bvconcat_v2_bis(SX,X, SY, Y, Z) :-
bvconcat_v2_ter(SX,X, SY, Y, Z),
bvconcat_inst_free(SX, X, SY, Y, Z, Stop),
(var(Stop) ->
- suspend(bvconcat_v2_bis(SX,X,SY,Y,Z),0,(X,Y,Z)->suspend:constrained)
+ my_suspend(bvconcat_v2_bis(SX,X,SY,Y,Z),0,(X,Y,Z)->suspend:constrained)
; true)),
set_priority(Prio),
wake_if_other_scheduled(Prio).
@@ -1718,7 +1720,7 @@ check_eq_args_bvrotateLR(M,X,Z,Work) :-
Ones is 2^M - 1,
mfd:set_intervals(X,[0,Ones]),
Work = 1
- ; suspend(check_eq_args_bvrotateLR(M,X,Z,_),0,(X,Z)->
+ ; my_suspend(check_eq_args_bvrotateLR(M,X,Z,_),0,(X,Z)->
suspend:constrained))).
@@ -1793,7 +1795,7 @@ zero_extend(Sx,Extend,X,Y) :-
% pour obtenir Y
sign_extend(Sx, I, X, Y) :-
var(I), !,
- suspend(sign_extend(Sx, I, X, Y),0,[I] -> inst).
+ my_suspend(sign_extend(Sx, I, X, Y),0,[I] -> inst).
sign_extend(_, 0, X, Y) ?-
!, protected_unify(X,Y).
sign_extend(Sx, I, 0, Y) ?-
@@ -1949,7 +1951,7 @@ Similar for bvgt.
%% fill_bvbounds(Y,NDY),
%% term_variables([X,Y],Vars),
%% (Vars == [] -> true
-%% ; suspend(bvleq(X, Y), 0, (Vars -> suspend:constrained))).
+%% ; my_suspend(bvleq(X, Y), 0, (Vars -> suspend:constrained))).
%% % =================== geq ====================
%% :- export bvgeq/2.
@@ -1981,11 +1983,11 @@ Similar for bvgt.
%% fill_bvbounds(Y,NDY),
%% term_variables([X,Y],Vars),
%% (Vars == [] -> true
-%% ; suspend(bvsleq(X, Y), 0, (Vars -> suspend:constrained))))
+%% ; my_suspend(bvsleq(X, Y), 0, (Vars -> suspend:constrained))))
%% ;
%% term_variables([X,Y],Vars),
%% (Vars == [] -> true
-%% ; suspend(bvsleq(X, Y), 0, (Vars -> suspend:constrained)))
+%% ; my_suspend(bvsleq(X, Y), 0, (Vars -> suspend:constrained)))
%% ).
%% get_sign_bits(M,DX,DY,SX,SY) :-
@@ -2037,7 +2039,7 @@ Similar for bvgt.
%% fill_bvbounds(Z,NDZ),
%% term_variables([X,Y,Z],Vars),
%% (Vars = [_|_] ->
-%% suspend(bvand_bis(M,X,Y,Z), 0, Vars -> suspend:constrained);
+%% my_suspend(bvand_bis(M,X,Y,Z), 0, Vars -> suspend:constrained);
%% true),
%% set_priority(Prio),
%% wake_if_other_scheduled(Prio).
@@ -2078,7 +2080,7 @@ sl_constr(M, DX, Y, DZ, NDX, NDZ) :-
%% term_variables([X,Z],Vars),
%% (Vars == [] ->
%% true
-%% ; suspend(bvsr_bis(M,X,Y,Z), 0, (Vars -> suspend:constrained)))),
+%% ; my_suspend(bvsr_bis(M,X,Y,Z), 0, (Vars -> suspend:constrained)))),
%% set_priority(Prio),
%% wake_if_other_scheduled(Prio).
@@ -2129,7 +2131,7 @@ zero_extend_bis(SizeX,Extend,X,Y) :-
((var(X),
var(Y))
->
- suspend(zero_extend_bis(SizeX,Extend,X,Y),0,[X,Y]->
+ my_suspend(zero_extend_bis(SizeX,Extend,X,Y),0,[X,Y]->
suspend:constrained)
; protected_unify(X,Y)))),
set_priority(Prio),
@@ -2186,7 +2188,7 @@ zero_extend_bis(SizeX,Extend,X,Y) :-
%% ((var(X),
%% var(Y))
%% ->
- %% suspend(zero_extend_bis(SizeX,Extend,X,Y),0,[X,Y]->
+ %% my_suspend(zero_extend_bis(SizeX,Extend,X,Y),0,[X,Y]->
%% suspend:constrained)
%% ; protected_unify(X,Y)))),
%% set_priority(Prio),
@@ -2196,7 +2198,7 @@ zero_extend_bis(SizeX,Extend,X,Y) :-
/*
sign_extend(M, I, X, Y) :-
var(I), !,
- suspend(sign_extend(M, I, X, Y),0,[I] -> inst).
+ my_suspend(sign_extend(M, I, X, Y),0,[I] -> inst).
sign_extend(_, 0, X, Y) ?-
!, protected_unify(X,Y).
sign_extend(Sx, I, X, Y) :-
@@ -2257,7 +2259,7 @@ sign_extend_bis_bis(Sx, Sy, I, X, Y) :-
get_attr_bv(X, bvdom(_, _, _, XGU)),
get_attr_bv(Y, bvdom(Y1, Y0, YLU, _)),
replace_attribute(Y, bvdom(Y1, Y0, YLU, XGU), mbv),
- suspend(sign_extend_bis_bis(Sx, Sy, I, X, Y),0,[X,Y]
+ my_suspend(sign_extend_bis_bis(Sx, Sy, I, X, Y),0,[X,Y]
-> suspend:constrained)
; sign_extend_bis(Sx, Sy, I, X, Y))
)).
@@ -2359,12 +2361,12 @@ adapt_inter([C|XInter], OnesOnLeft, [CC|AXInter]) :-
%% replace_attribute(Y, bvdom(Y1, Y0, YLU, XGU), mbv),
%% ((var(X), var(Y))
%% ->
-%% suspend(sign_extend_bis(Sx, Sy, I, X, Y),0,[X,Y]-> suspend:constrained)
+%% my_suspend(sign_extend_bis(Sx, Sy, I, X, Y),0,[X,Y]-> suspend:constrained)
%% ; sign_extend_bis(Sx, Sy, I, X, Y)))).
/*
sign_extend(M, I, X, Y) :-
var(I), !,
- suspend(sign_extend(M, I, X, Y),0,[I] -> inst).
+ my_suspend(sign_extend(M, I, X, Y),0,[I] -> inst).
sign_extend(_, 0, X, Y) ?-
!, protected_unify(X,Y).
sign_extend(Sx, I, X, Y) :-
@@ -2397,7 +2399,7 @@ sign_extend_bis(M, I, X, Y):-
; term_variables([X,Y],Vars),
(Vars == [] ->
true
- ; suspend(sign_extend_bis(M, I, X, Y) , 0, (Vars -> suspend:constrained)))
+ ; my_suspend(sign_extend_bis(M, I, X, Y) , 0, (Vars -> suspend:constrained)))
)).
@@ -2520,7 +2522,7 @@ bvasr(M, X, Y, Z):-
%% /*ShiftingUI*/sr_interval_ON(X,Y,Z)
%% ; true),
%% ((var(X), var(Z)) ->
-%% suspend(bvsr_bis(M,X,Y,Z), 0, ([X , Z] -> suspend:constrained))
+%% my_suspend(bvsr_bis(M,X,Y,Z), 0, ([X , Z] -> suspend:constrained))
%% ; true)
%% ; true)),
%% set_priority(Prio),
diff --git a/Src/COLIBRI/mfd.pl b/Src/COLIBRI/mfd.pl
index 5603d6030..8af5230c9 100755
--- a/Src/COLIBRI/mfd.pl
+++ b/Src/COLIBRI/mfd.pl
@@ -724,7 +724,12 @@ set_domain_list([V|Vars],Inter,Wake) :-
-set_var_domain(V{mfd:dom(Inter)},Inter,_) ?- !.
+set_var_domain(V{mfd:dom(Inter)},Inter,_) ?- !,
+ ((Inter = [Val],
+ number(Val))
+ ->
+ protected_unify(V,Val)
+ ; true).
set_var_domain(V{mfd:OldDom},Inter,Wake) ?- !,
(compound(OldDom) ->
dom_intersection(OldDom,dom(Inter),dom(NInterval0)),
diff --git a/Src/COLIBRI/mod_arith.pl b/Src/COLIBRI/mod_arith.pl
index bd0fd77d8..1d0717f7b 100755
--- a/Src/COLIBRI/mod_arith.pl
+++ b/Src/COLIBRI/mod_arith.pl
@@ -262,8 +262,18 @@ addNu(N,A,B,C,UO) :-
mfd:set_intervals(UO,[0,1]),
addNsu(u,N,A,B,C,UO).
+/* FAUX
+addNsu(u,N,A,B,0,UO) ?- !,
+ opNsu(u,N,A,B,UO).
+*/
addNsu(SU,N,A,A,C,UO) ?- !,
multNsu(SU,N,2,A,C,UO).
+addNsu(SU,N,0,B,C,UO) ?- !,
+ protected_unify(UO,0),
+ protected_unify(B,C).
+addNsu(SU,N,A,0,C,UO) ?- !,
+ protected_unify(UO,0),
+ protected_unify(A,C).
addNsu(SU,N,A,B,C,UO) :-
intN_min_max(SU,N,Min,Max),
mfd:set_intervals(A,[Min..Max]),
@@ -292,19 +302,19 @@ addNsu(SU,N,A,B,C,UO) :-
% Pas de débordement négatif
(LRes > Max ->
% Débordement positif
- UO = 1
+ protected_unify(UO,1)
; mfd:dvar_remove_smaller(UO,0))
; true),
(HRes =< Max ->
% Pas de débordement positif
(HRes < Min ->
% Débordement négatif
- UO = -1
+ protected_unify(UO,-1)
; mfd:dvar_remove_greater(UO,0))
; true),
(UO == 0 ->
% Pas de débordement
- C = Res
+ protected_unify(C,Res)
; (SU == u ->
% On peut utiliser div_mod (en fait div_rem)
div_mod(Res,Size,UO,C)
@@ -356,14 +366,14 @@ check_addN(SU,N,A,B,ApB,C,UO) :-
% Pas de débordement négatif
(LApB > Max ->
% Débordement positif
- UO = 1
+ protected_unify(UO,1)
; mfd:dvar_remove_smaller(UO,0))
; true),
(HApB =< Max ->
% Pas de débordement positif
(HApB < Min ->
% Débordement négatif
- UO = -1
+ protected_unify(UO,-1)
; mfd:dvar_remove_greater(UO,0))
; true),
% On peut exploiter les deltas pour réduire UO
@@ -880,18 +890,18 @@ reduce_UO_from_delta_B_C(DeltaBC,Min,Max,A,UO) :-
DMax =< Max)
->
%% Min..Max contient DMin..DMax => UO = 0
- UO = 0
+ protected_unify(UO,0)
; (DMin >= Min ->
%% Pas de débordement positif, UO <> 1
(DMin > Max ->
%% Min..Max disjoint de DMin..DMax => UO <> 0
- UO = -1
+ protected_unify(UO,-1)
; mfd:dvar_remove_element(UO,1))
; (DMax =< Max ->
%% Pas de débordement négatif, UO <> -1
(DMax < Min ->
%% Min..Max disjoint de DMin..DMax => UO <> 0
- UO = 1
+ protected_unify(UO,1)
; mfd:dvar_remove_element(UO, -1))
; true))),
(UO == 0 ->
@@ -1125,6 +1135,9 @@ minusNu(N,A,B,C,UO) :-
minus(A,B,AmB),
to_intNu(N,AmB,C).
*/
+minusNu(N,A,0,C,UO) ?- !,
+ protected_unify(UO,0),
+ protected_unify(A,C).
minusNu(N,A,B,C,UO) :-
mfd:set_intervals(UO,[-1,0]),
mfd:set_intervals(OpUO,[0,1]),
@@ -1173,35 +1186,35 @@ opNu(N,A,OpA,UO) :-
opNsu(u,N,A,OpA,UO).
opNsu(SU,N,A,OpA,UO) :-
- %% op(A) = OpA + UO*Size,
- intN_min_max(SU,N,Min,Max),
- mfd:set_intervals(A,[Min..Max]),
- mfd:set_intervals(OpA,[Min..Max]),
- op(A,Res),
- mfd:dvar_range(Res,LRes,HRes),
- (Min =< LRes ->
- %% Pas de débordement négatif
- (LRes > Max ->
- %% Débordement positif
- UO = 1
- ; mfd:dvar_remove_smaller(UO,0))
- ; true),
- (HRes =< Max ->
- %% Pas de débordement positif
- (HRes < Min ->
- %% Débordement négatif
- UO = -1
- ; mfd:dvar_remove_greater(UO,0))
- ; true),
- (UO == 0 ->
- %% Pas de débordement
- OpA = Res
- ; Size is 2^N,
- (OpA == 0 ->
- mult(Size,UO,Res)
- ; mult(Size,UO,UOSize),
- add(OpA,UOSize,Res)),
- check_opN(SU,N,A,Res,OpA,UO)).
+ % op(A) = OpA + UO*Size,
+ intN_min_max(SU,N,Min,Max),
+ mfd:set_intervals(A,[Min..Max]),
+ mfd:set_intervals(OpA,[Min..Max]),
+ op(A,Res),
+ mfd:dvar_range(Res,LRes,HRes),
+ (Min =< LRes ->
+ % Pas de débordement négatif
+ (LRes > Max ->
+ % Débordement positif
+ protected_unify(UO,1)
+ ; mfd:dvar_remove_smaller(UO,0))
+ ; true),
+ (HRes =< Max ->
+ % Pas de débordement positif
+ (HRes < Min ->
+ % Débordement négatif
+ protected_unify(UO,-1)
+ ; mfd:dvar_remove_greater(UO,0))
+ ; true),
+ (UO == 0 ->
+ % Pas de débordement
+ OpA = Res
+ ; Size is 2^N,
+ (OpA == 0 ->
+ mult(Size,UO,Res)
+ ; mult(Size,UO,UOSize),
+ add(OpA,UOSize,Res)),
+ check_opN(SU,N,A,Res,OpA,UO)).
check_opN(SU,N,A,IOpA,OpA,UO) :-
@@ -1222,14 +1235,14 @@ check_opN(SU,N,A,IOpA,OpA,UO) :-
% Pas de débordement négatif
(LIOpA > Max ->
% Débordement positif
- UO = 1
+ protected_unify(UO,1)
; mfd:dvar_remove_smaller(UO,0))
; true),
(HIOpA =< Max ->
% Pas de débordement positif
(HIOpA < Min ->
% Débordement négatif
- UO = -1
+ protected_unify(UO,-1)
; mfd:dvar_remove_greater(UO,0))
; true),
saturate_opNus_inequalities(Min,Max,A,OpA),
@@ -1277,7 +1290,7 @@ apply_opN_UO(Min,Max,A,B,UO,Continue) :-
apply_opN_UO_unsigned(Rel,Sd2,Max,A,B,UO)
; % Cas signé
(occurs(Rel,('#','>','<')) ->
- UO = 0
+ protected_unify(UO,0)
; apply_opN_UO_signed(Rel,Min,Max,A,B),
Continue = 1)).
@@ -1299,15 +1312,15 @@ apply_opN_UO(Min,Max,A,B,1,_) :-
apply_opN_UO_unsigned('?',Sd2,Max,A,B,UO) :- !.
apply_opN_UO_unsigned('=',Sd2,Max,A,B,UO) :-
mfd:set_intervals(A,[0,Sd2]),
- A = B.
+ protected_unify(A = B).
apply_opN_UO_unsigned('#',Sd2,Max,A,B,UO) :- !,
- UO = -1,
+ protected_unify(UO = -1),
mfd:dvar_remove_element(A,0),
mfd:dvar_remove_element(A,Sd2),
mfd:dvar_remove_element(B,0),
mfd:dvar_remove_element(B,Sd2).
apply_opN_UO_unsigned('<',Sd2,Max,A,B,UO) :- !,
- UO = -1,
+ protected_unify(UO = -1),
PSd2 is Sd2 - 1,
NSd2 is Sd2 + 1,
mfd:dvar_remove_element(A,0),
@@ -1320,9 +1333,9 @@ apply_opN_UO_unsigned('=<',Sd2,Max,A,B,UO) :- !,
mfd:get_intervals(B,IB),
(number_in_interval(IB,0) ->
true
- ; UO = -1,
+ ; protected_unify(UO = -1),
mfd:dvar_remove_element(A,0))
- ; UO = -1,
+ ; protected_unify(UO = -1),
mfd:dvar_remove_element(B,0)),
mfd:dvar_remove_greater(A,Sd2),
mfd:dvar_update(B,dom([0,Sd2..Max])).
@@ -1344,7 +1357,7 @@ apply_opN_UO_signed('>',Min,Max,A,B) :-
apply_opN_UO_signed('?',_,_,_,_).
apply_opN_UO_signed('=',Min,Max,A,B) :-
mfd:set_intervals(A,[Min,0]),
- A = B.
+ protected_unify(A = B).
apply_opN_UO_signed('>=',Min,Max,A,B) :-
% A positif U -8, B négatif
mfd:dvar_update(A,dom([Min,0..Max])),
@@ -1587,19 +1600,19 @@ multNsu(SU,N,A,B,C,UO) :-
% Pas de débordement négatif
(LRes > Max ->
% Débordement positif
- UO = 1
+ protected_unify(UO = 1)
; mfd:dvar_remove_smaller(UO,0))
; true),
(HRes =< Max ->
% Pas de débordement positif
(HRes < Min ->
% Débordement négatif
- UO = -1
+ protected_unify(UO = -1)
; mfd:dvar_remove_greater(UO,0))
; true),
(UO == 0 ->
% Pas de débordement
- C = Res
+ protected_unify(C = Res)
; (SU == u ->
% On peut utiliser div_mod (en fait div_rem)
div_mod(Res,Size,K,C)
@@ -1667,14 +1680,14 @@ check_multN(SU,N,A,B,Res,C,K,UO) :-
% Pas de débordement négatif
(LRes > Max ->
% Débordement positif
- UO = 1
+ protected_unify(UO = 1)
; mfd:dvar_remove_smaller(UO,0))
; true),
(HRes =< Max ->
% Pas de débordement positif
(HRes < Min ->
% Débordement négatif
- UO = -1
+ protected_unify(UO = -1)
; mfd:dvar_remove_greater(UO,0))
; true),
check_multNbis(SU,N,A,B,Res,C,K,UO,Continue),
@@ -1727,9 +1740,9 @@ check_multNbis(SU,N,A,B,Res,C,K,UO,Continue) :-
(is_odd(int,B), %% B impair ne divise pas 2^N donc A = 0
Var = A))
->
- UO = 0,
- K = 0,
- Var = 0
+ protected_unify(UO = 0),
+ protected_unify(K = 0),
+ protected_unify(Var = 0)
; (not_unify(A,0) ->
%% Réciproque de B impair
launch_congr(B,0,2),
@@ -1774,9 +1787,9 @@ check_multNbis(SU,N,A,B,Res,A,K,UO,Continue) ?- !,
Val = 0))
->
%% A = 0 ou B = 1 donc pas de débordement
- UO = 0,
- K = 0,
- Var = Val
+ protected_unify(UO = 0),
+ protected_unify(K = 0),
+ protected_unify(Var = Val)
; %% si A <> 0, alors B impair
%% si B <> 1, alors A pair
(not_unify(A,0) ->
@@ -1835,14 +1848,14 @@ check_UO_K(K,K) ?- !.
check_UO_K(K,UO) :-
nonvar(K),!,
(K == 0 ->
- UO = 0
+ protected_unify(UO = 0)
; (K > 0 ->
- UO = 1
- ; UO = -1)).
+ protected_unify(UO = 1)
+ ; protected_unify(UO = -1))).
check_UO_K(K,UO) :-
nonvar(UO),!,
(UO == 0 ->
- K = 0
+ protected_unify(K = 0)
; (UO == 1 ->
mfd:dvar_remove_smaller(K,1)
; mfd:dvar_remove_greater(K,-1))).
@@ -1866,24 +1879,24 @@ check_UO_K(K,UO) :-
%% On a pu réduire K
(K == 0 ->
%% On a fini
- UO = 0
+ protected_unify(UO = 0)
; mfd:dvar_range(K,MinK,MaxK),
(MinK >= 0 ->
%% Pas de débordement négatif
(MinK > 0 ->
- UO = 1
+ protected_unify(UO = 1)
; mfd:dvar_remove_element(UO,-1))
; (MaxK =< 0 ->
%% Pas de débordement positif
(MaxK < 0 ->
- UO = -1
+ protected_unify(UO = -1)
; mfd:dvar_remove_element(UO,1))
; true)),
((MinK >= -1,
MaxK =< 1)
->
%% On peut identifier K et UO
- K = UO
+ protected_unify(K = UO)
; true)).
@@ -2124,13 +2137,13 @@ powerNu(N,A,P,B,UO) :-
powerNsu(SU,N,A,0,B,UO) :- !,
intN_min_max(SU,N,Min,Max),
mfd:set_intervals(A,[Min..Max]),
- B = 1,
- UO = 0.
+ protected_unify(B = 1),
+ protected_unify(UO = 0).
powerNsu(SU,N,A,1,B,UO) :- !,
intN_min_max(SU,N,Min,Max),
mfd:set_intervals(A,[Min..Max]),
- B = A,
- UO = 0.
+ protected_unify(B = A),
+ protected_unify(UO = 0).
powerNsu(SU,N,A,P,B,UO) :-
%% P > 1
intN_min_max(SU,N,Min,Max),
@@ -2164,14 +2177,14 @@ powerNsu(SU,N,A,P,B,UO) :-
%% Pas de débordement négatif
(LPowAP > Max ->
%% Débordement positif
- UO = 1
+ protected_unify(UO = 1)
; mfd:dvar_remove_smaller(UO,0))
; true),
(HPowAP =< Max ->
%% Pas de débordement positif
(HPowAP < Min ->
%% Débordement négatif
- UO = -1
+ protected_unify(UO = -1)
; mfd:dvar_remove_greater(UO,0))
; true),
(UO == 0 ->
@@ -2213,14 +2226,14 @@ powerNsu(SU,N,A,P,B,UO) :-
%% les identités et les factorisations
check_powerN(SU,N,A,P,PowAP,B,K,0) ?- !,
%% L'arithmétique normale travaille
- K = 0,
+ protected_unify(K = 0),
true,
- PowAP = B.
+ protected_unify(PowAP = B).
check_powerN(SU,N,A,P,PowAP,B,0,UO) ?- !,
%% L'arithmétique normale travaille
- UO = 0,
+ protected_unify(UO = 0),
true,
- PowAP = B.
+ protected_unify(PowAP = B).
check_powerN(SU,N,A,P,PowAP,B,K,UO) :-
get_priority(Prio),
set_priority(1),
@@ -2231,14 +2244,14 @@ check_powerN(SU,N,A,P,PowAP,B,K,UO) :-
%% Pas de débordement négatif
(LPowAP > Max ->
%% Débordement positif
- UO = 1
+ protected_unify(UO = 1)
; mfd:dvar_remove_smaller(UO,0))
; true),
(HPowAP =< Max ->
%% Pas de débordement positif
(HPowAP < Min ->
%% Débordement négatif
- UO = -1
+ protected_unify(UO = -1)
; mfd:dvar_remove_greater(UO,0))
; true),
check_powerNbis(SU,N,A,P,B,K,UO,Continue),
@@ -2307,7 +2320,7 @@ factorize_powerNsu(check_powerN(SU,N,X,PX,_,Y,KY,UOY),Susp,SU,N,A,PA,B,KB,UOB,Go
%% On laisse l'autre power travailler
%% les contraintes auxiliaires se factorisent
%% après les unifications
- Goal = (B = Y, true, KB = KY, true, UOB = UOY).
+ Goal = (protected_unify(B = Y), protected_unify(KB = KY), protected_unify(UOB = UOY)).
/*
A VOIR LES UO DU NOUVEAU POWER SONT FAUX
diff --git a/Src/COLIBRI/mreal.pl b/Src/COLIBRI/mreal.pl
index 3ef78a749..1dc687af0 100755
--- a/Src/COLIBRI/mreal.pl
+++ b/Src/COLIBRI/mreal.pl
@@ -755,7 +755,13 @@ set_domain_list([V|Vars],Type,Inter,S,Wake) :-
from colibri.
%% S, la taille de Inter, peut etre non instanciee
-set_var_domain(V{mreal:dom(_,Inter,_)},_Type,Inter,_,_) ?- !.
+set_var_domain(V{mreal:dom(_,Inter,_)},_Type,Inter,_,_) ?- !,
+ ((Inter = [Val],
+ (number(Val);
+ atomic(Val)))
+ ->
+ protected_unify(V,Val)
+ ; true).
set_var_domain(V{mreal:OldDom},Type,Inter,S,Wake) ?- !,
(compound(OldDom) ->
(get_sign(V,OSV) ->
diff --git a/Src/COLIBRI/my_suspend.pl b/Src/COLIBRI/my_suspend.pl
index 9d9bde659..7d57e7747 100755
--- a/Src/COLIBRI/my_suspend.pl
+++ b/Src/COLIBRI/my_suspend.pl
@@ -6,16 +6,25 @@
get_cstr_suspensions/2,
is_suspend_var/4.
+
+
+%% La compilation "inline" ne fait pas bon menage avec les suspensions.
+%% option interdite pour ce fichier.
+:- pragma(noexpand).
+
% Variables globalles pour faire des stats de propagation.
:- setval(step_stats,0)@eclipse.
:- setval(step_limit,0)@eclipse.
:- setval(nb_steps,0)@eclipse.
+:- import check_solve_timeout/0 from ndelta.
+:- export check_steps/0.
check_steps :-
+ check_solve_timeout,
(getval(step_stats,1)@eclipse ->
% Mode ou on compte le nombre de steps
incval(nb_steps)@eclipse,
- smt_check_disabled_delta@eclipse,
+ smt_check_disabled_delta,
getval(step_limit,StepLim)@eclipse,
(StepLim == 0 ->
% Pas de limite
@@ -29,18 +38,11 @@ check_steps :-
exit(6)))
; % Pas de comptage
true).
-
-
-%% La compilation "inline" ne fait pas bon menage avec les suspensions.
-%% option interdite pour ce fichier.
-:- pragma(noexpand).
-
:- export my_suspend/3.
:- tool(my_suspend/3,my_suspend_body/4).
my_suspend_body(G,Prio,Attr,Module) :-
check_steps,
- trigger_lin_solve,
(getval(refutation_chk,1)@eclipse ->
% On ajuste la priorite des contraintes
% suspendues pendant une refutation pour qu'elles
@@ -55,7 +57,6 @@ my_suspend_body(G,Prio,Attr,Module) :-
:- tool(my_suspend/4,my_suspend_body/5).
my_suspend_body(G,Prio,Attr,Susp,Module) :-
check_steps,
- trigger_lin_solve,
(getval(refutation_chk,1)@eclipse ->
% On ajuste la priorite des contraintes
% suspendues pendant une refutation pour qu'elles
diff --git a/Src/COLIBRI/ndelta.pl b/Src/COLIBRI/ndelta.pl
index fa39e1294..3490d1df0 100755
--- a/Src/COLIBRI/ndelta.pl
+++ b/Src/COLIBRI/ndelta.pl
@@ -301,6 +301,35 @@ activate_check_pu :-
deactivate_check_pu :-
setval(ckpu,0).
+
+:- setval(solve_timeout,1.0Inf).
+
+:- export reset_solve_timeout/0.
+reset_solve_timeout :-
+ %writeln(reset_solve_timeout),
+ setval(solve_timeout,1.0Inf).
+
+:- export start_solve_timeout/1.
+start_solve_timeout(TO) :-
+ % on passe en ms
+ statistics(session_time,FT),
+ (TO == 0 ->
+ MaxT = 1.0Inf
+ ; MaxT is integer(ceiling(FT))*1000+(TO*1000)),
+ %writeln(start:MaxT),
+ setval(solve_timeout,MaxT).
+
+:- export check_solve_timeout/0.
+check_solve_timeout :-
+ getval(solve_timeout,MaxT),
+ statistics(session_time,FT),
+ (MaxT < integer(ceiling(FT))*1000 ->
+ % call(spy_here)@eclipse,
+ %writeln(output,timeout_col),
+ exit_block(timeout_col)
+ ; true).
+
+
%----------------------------------------------------------------
% attribute declaration
%----------------------------------------------------------------
@@ -336,8 +365,13 @@ deactivate_check_pu :-
%% sur un graphe conrompu. "pre_unify_delta" permet de traiter
%% le graphe avant que la variable soit instanciee.
%% De plus, on teste l'unifiabilite avant de lancer le traitement du graphe.
-pre_unify_delta(T,T) ?- !.
+
pre_unify_delta(T1,T2) :-
+ check_solve_timeout,
+ pre_unify_delta0(T1,T2).
+
+pre_unify_delta0(T,T) ?- !.
+pre_unify_delta0(T1,T2) :-
check_pu(T1,T2),
(is_delta_var(T1) ->
pre_unify_delta_var(T1,T2)
@@ -1738,8 +1772,8 @@ clean_seen_delta([_X{ndelta:Delta}|Vars]) ?-
clean_seen_delta(Vars).
-
check_previous_deltas(Loop,[(Start,_End)|Vars],Last,Done,InJoin,Join,NewLoop) ?- !,
+ check_solve_timeout,
getval(delta_credit,Credit),
((seen_delta(Start);
Credit == 0)
@@ -1908,7 +1942,8 @@ add_new_previous(Loop,Start,End,S,C,OpC,EndTransPath,NewLoop,_InJoin,Join) :-
% Nbp = 1 et MaxPaths <> []
change_plus_and_adjust_to_equal([(Start,MaxPaths)],TC,Join)
; % Le '+' de Start-End devient un '=' de cout TC-Cp
- NewC is TC-Cp,
+ % NewC is TC-Cp,
+ protected_rat_diff(TC,Cp,NewC),
replace_delta_plus_by_equal(Start,End,NewC))
; % Si S = '+' on peut mettre a jour Start-End (C et OpC)
%% en faisant l'intersection avec Start-Join + Join-End
diff --git a/Src/COLIBRI/notify.pl b/Src/COLIBRI/notify.pl
index 1840361c3..ffc44ecbe 100755
--- a/Src/COLIBRI/notify.pl
+++ b/Src/COLIBRI/notify.pl
@@ -186,16 +186,18 @@ last_scheduled_prio(P,LS) :-
%% wake conditionnel selon l'existence de contraintes "schedulees"
%% avec un niveau de priorite inferieur strictement au niveau courant
wake_if_other_scheduled :-
- get_priority(Prio),
- wake_if_other_scheduled(Prio).
+ get_priority(Prio),
+ wake_if_other_scheduled(Prio).
+:- import check_solve_timeout/0 from ndelta.
%% wake conditionnel selon l'existence de contraintes "schedulees"
%% avec un niveau de priorite inferieur strictement a "Prio"
wake_if_other_scheduled(1) :- !.
wake_if_other_scheduled(Prio) :-
(check_no_scheduled_prio(Prio) ->
- true
- ; wake,
+ check_solve_timeout
+ ; check_solve_timeout,
+ wake,
true).
check_no_scheduled_prio(Prio) :-
@@ -288,6 +290,7 @@ scheduled_suspensions(Prio,SuspsPrio) :-
%% Si X et Y ont des suspensions dans bound/constrained
%% qui partagent une autre variable que Y, elles sont reveillees
+%schedule_bound(SuspX,_):- !.
schedule_bound(SuspX,_):-
var(SuspX),!. %% Pas de suspension sur X
schedule_bound(suspend(_,[],[]),_) :- -?-> !. %% Pas de suspension sur X
@@ -354,6 +357,8 @@ sleeping_suspensions_and_vars1([Susp|LSusp],PairLSusp,AccuV,SV,NLSusp) :-
:- mode get_sleeping_suspension_vars(++,-).
get_sleeping_suspension_vars(S,V) :-
get_suspension_data(S,goal,G),
+ functor(G,FG,_),
+ not occurs(FG,(smtlib_select,eq_array,diff_array1,diff_reif_array)),
term_variables(G,V).
diff --git a/Src/COLIBRI/realarith.pl b/Src/COLIBRI/realarith.pl
index 98979d052..ccbf83397 100644
--- a/Src/COLIBRI/realarith.pl
+++ b/Src/COLIBRI/realarith.pl
@@ -3752,7 +3752,7 @@ add_real_inst(real,0.0,B,C,_) ?- !,
add_real_inst(real,A,0.0,C,_) ?- !,
protected_unify(A,C).
add_real_inst(real,A,B,0.0,_) ?- !,
- op_real(Type,A,B).
+ op_real(real,A,B).
add_real_inst(Type,A,B,C,Continue) :-
(is_fzero(A) ->
%Type <> real
@@ -4587,7 +4587,7 @@ get_rel_between_real_args_from_cstrs(A,B,RelAB) :-
:- mode add_real_rec(++,++,++,++,++,++,++,++,++,++,++,-,-,-).
add_real_rec(real,_,FIA,FIB,FIC,DomA,DomB,DomC,RelAB,RelCB,RelCA,NDomA,NDomB,NDomC) :- !,
- add_real_rec1(FIA,FIB,FIC,DomA,DomB,DomC,RelAB,RelCB,RelCA,NDomA,NDomB,NDomC).
+ add_real_rec1(5,FIA,FIB,FIC,DomA,DomB,DomC,RelAB,RelCB,RelCA,NDomA,NDomB,NDomC).
add_real_rec(Type,RS,FIA,FIB,FIC,DomA0,DomB0,DomC,RelAB,RelCB,RelCA,
NDomA,NDomB,NDomC) :-
% On reduit les domaines de A et B par les proprietes de
@@ -4600,8 +4600,12 @@ add_real_rec(Type,RS,FIA,FIB,FIC,DomA0,DomB0,DomC,RelAB,RelCB,RelCA,
add_float_rec(RS,Type,3,FIA,FIB,FIC,DomA,DomB,DomC,RelAB,RelCB,RelCA,NDomA,NDomB,NDomC).
%% MODE real
-:- mode add_real_rec1(++,++,++,++,++,++,++,++,++,-,-,-).
-add_real_rec1(FIA,FIB,FIC,DomA,DomB,DomC,RelAB,RelCB,RelCA,NDomA,NDomB,NDomC) :-
+:- mode add_real_rec1(++,++,++,++,++,++,++,++,++,++,-,-,-).
+add_real_rec1(0,FIA,FIB,FIC,DomA,DomB,DomC,RelAB,RelCB,RelCA,NDomA,NDomB,NDomC) ?- !,
+ NDomA = DomA,
+ NDomB = DomB,
+ NDomC = DomC.
+add_real_rec1(Credit,FIA,FIB,FIC,DomA,DomB,DomC,RelAB,RelCB,RelCA,NDomA,NDomB,NDomC) :-
mreal:dom_interval(DomA,InterA),
mreal:dom_interval(DomB,InterB),
mreal:dom_interval(DomC,InterC),
@@ -4630,13 +4634,14 @@ add_real_rec1(FIA,FIB,FIC,DomA,DomB,DomC,RelAB,RelCB,RelCA,NDomA,NDomB,NDomC) :-
NDomA = DomA3,
NDomB = DomB3,
NDomC = DomC3
- ; add_real_rec1(FIA,FIB,FIC,DomA3,DomB3,DomC3,RelAB,RelCB,RelCA,NDomA,NDomB,NDomC)).
+ ; NCredit is Credit - 1,
+ add_real_rec1(NCredit,FIA,FIB,FIC,DomA3,DomB3,DomC3,RelAB,RelCB,RelCA,NDomA,NDomB,NDomC)).
%% EqAC
-real_inter_dom_if_eq('=',EqBC,DomA,DomB,DomC,NDom,DomB,NDom) :- !,
+real_inter_dom_if_eq('=',EqBC,DomA,DomB,DomC,NDom,DomB,NDom) ?- !,
mreal:dom_intersection(DomA,DomC,NDom,_).
%% EqBC
-real_inter_dom_if_eq(_,'=',DomA,DomB,DomC,DomA,NDom,NDom) :- !,
+real_inter_dom_if_eq(_,'=',DomA,DomB,DomC,DomA,NDom,NDom) ?- !,
mreal:dom_intersection(DomB,DomC,NDom,_).
real_inter_dom_if_eq(_,_,DomA,DomB,DomC,DomA,DomB,DomC).
@@ -9478,89 +9483,84 @@ inv2_minus_float_max(_,C,B,F,A) :-
%% Mode reel
minus_real_rec(real,A,B,C) :- !,
- getval(real_simp,RS)@eclipse,
- minus_real_rec(3,RS,Type,A,B,C).
+ minus_real_rec(5,Type,A,B,C).
%% Mode double/simple nearest
minus_real_rec(Type,A,B,C) :-
- getval(real_simp,RS)@eclipse,
- minus_float_rec(3,RS,Type,A,B,C).
-
+ getval(real_simp,RS)@eclipse,
+ minus_float_rec(3,RS,Type,A,B,C).
-minus_real_rec(0,1,Type,A,B,C) :- !,
- (getval(gdbg,1)@eclipse ->
- writeln(output,max_iter:minus_real_rec(A,B,C))
- ; true).
-minus_real_rec(Cpt,RS,Type,A,B,C) :-
- mreal:dvar_domain(A,DomA),
- mreal:dvar_domain(B,DomB),
- mreal:dvar_domain(C,DomC),
- (RS == 1 ->
- get_rel_between_real_args(A,B,RelAB),
- get_rel_between_real_args(C,B,RelCB),
- get_rel_between_real_args(A,C,RelAC),
- get_float_int_status(A,FIA),
- get_float_int_status(B,FIB),
- get_float_int_status(C,FIC)
- ; (RelAB,RelCB,RelCA) = (?,?,?),
- (FIA,FIB,FIC) = (0,0,0)),
- %% Projections
- minus_real_rec(FIA,FIB,FIC,DomA,DomB,DomC,RelAB,RelCB,RelAC,NDomA,NDomB,NDomC),
- mreal:dvar_set(A,NDomA),
- mreal:dvar_set(B,NDomB),
- mreal:dvar_set(C,NDomC),
- (RS == 1 ->
- mreal:dvar_domain(A,NewDomA),
- mreal:dvar_domain(B,NewDomB),
- mreal:dvar_domain(C,NewDomC),
- % = necessaire
- ((NDomA,NDomB,NDomC) = (NewDomA,NewDomB,NewDomC) ->
- true
- ; NCpt is Cpt - 1,
- minus_real_rec(NCpt,RS,Type,A,B,C))
- ; true).
-minus_real_rec(FIA,FIB,FIC,DomA,DomB,DomC,RelAB,RelCB,RelAC,NDomA,NDomB,NDomC) :-
- mreal:dom_interval(DomA,InterA),
- mreal:dom_interval(DomB,InterB),
- mreal:dom_interval(DomC,InterC),
- %% On freine des qu'un des produit cartesien est sup a MaxProd
- (check_maxprod_intervals(InterA,InterB,InterC) ->
- %% On ne travaille que sur les bornes
- % A - B -> C
+minus_real_rec(0,Type,A,B,C) :- !,
+ (getval(gdbg,1)@eclipse ->
+ writeln(output,max_iter:minus_real_rec(A,B,C))
+ ; true).
+minus_real_rec(Credit,Type,A,B,C) :-
+ mreal:dvar_domain(A,DomA),
+ mreal:dvar_domain(B,DomB),
+ mreal:dvar_domain(C,DomC),
+ (RS == 1 ->
+ get_rel_between_real_args(A,B,RelAB),
+ get_rel_between_real_args(C,B,RelCB),
+ get_rel_between_real_args(A,C,RelAC),
+ get_float_int_status(A,FIA),
+ get_float_int_status(B,FIB),
+ get_float_int_status(C,FIC)
+ ; (RelAB,RelCB,RelAC) = (?,?,?),
+ (FIA,FIB,FIC) = (0,0,0)),
+ % Projections
+ minus_real_rec(Credit,FIA,FIB,FIC,DomA,DomB,DomC,RelAB,RelCB,RelAC,NDomA,NDomB,NDomC),
+ mreal:dvar_set(A,NDomA),
+ mreal:dvar_set(B,NDomB),
+ mreal:dvar_set(C,NDomC).
+
+minus_real_rec(0,FIA,FIB,FIC,DomA,DomB,DomC,RelAB,RelCB,RelAC,NDomA,
+ NDomB,NDomC) ?- !,
+ NDomA = DomA,
+ NDomB = DomB,
+ NDomC = DomC.
+minus_real_rec(Credit,FIA,FIB,FIC,DomA,DomB,DomC,RelAB,RelCB,RelAC,NDomA,NDomB,NDomC) :-
+ mreal:dom_interval(DomA,InterA),
+ mreal:dom_interval(DomB,InterB),
+ mreal:dom_interval(DomC,InterC),
+ % On freine des qu'un des produit cartesien est sup a MaxProd
+ (check_maxprod_intervals(InterA,InterB,InterC) ->
+ % On ne travaille que sur les bornes
+ % A - B -> C
minus_real_dom_bounds(RelAB,FIC,DomA,DomB,DomC,DomC0),
- real_inter_dom_if_eq(RelAC,RelCB,DomA,DomB,DomC0,DomA1,DomB1,DomC1),
- % C + B -> A
+ real_inter_dom_if_eq(RelAC,RelCB,DomA,DomB,DomC0,DomA1,DomB1,DomC1),
+ % C + B -> A
inv1_minus_real_dom_bounds(RelCB,FIA,DomC1,DomB1,DomA1,DomA10),
- real_inter_dom_if_eq(RelAC,RelAB,DomC1,DomB1,DomA10,DomC2,DomB2,DomA2),
- % A - C -> B
+ real_inter_dom_if_eq(RelAC,RelAB,DomC1,DomB1,DomA10,DomC2,DomB2,DomA2),
+ % A - C -> B
inv2_minus_real_dom_bounds(RelAC,FIB,DomA2,DomC2,DomB2,DomB20)
- ; minus_real_dom(RelAB,FIC,DomA,DomB,DomC,DomC0),
- real_inter_dom_if_eq(RelAC,RelCB,DomA,DomB,DomC0,DomA1,DomB1,DomC1),
- inv1_minus_real_dom(RelCB,FIA,DomC1,DomB1,DomA1,DomA10),
- real_inter_dom_if_eq(RelAC,RelAB,DomC1,DomB1,DomA10,DomC2,DomB2,DomA2),
- inv2_minus_real_dom(RelAC,FIB,DomA2,DomC2,DomB2,DomB20)),
-
- real_inter_dom_if_eq(RelCB,RelAB,DomC2,DomA2,DomB20,DomC3,DomA3,DomB3),
-
- (((DomA3 == DomA,
- DomB3 == DomB,
- DomC3 == DomC0);
- (mreal:dom_size(DomA3,1),
- mreal:dom_size(DomB3,1)))
- ->
- NDomA = DomA3,
- NDomB = DomB3,
- NDomC = DomC3
- ; minus_real_rec(FIA,FIB,FIC,DomA3,DomB3,DomC3,RelAB,RelCB,RelAC,NDomA,NDomB,NDomC)).
+ ; minus_real_dom(RelAB,FIC,DomA,DomB,DomC,DomC0),
+ real_inter_dom_if_eq(RelAC,RelCB,DomA,DomB,DomC0,DomA1,DomB1,DomC1),
+ inv1_minus_real_dom(RelCB,FIA,DomC1,DomB1,DomA1,DomA10),
+ real_inter_dom_if_eq(RelAC,RelAB,DomC1,DomB1,DomA10,DomC2,DomB2,DomA2),
+ inv2_minus_real_dom(RelAC,FIB,DomA2,DomC2,DomB2,DomB20)),
+
+ real_inter_dom_if_eq(RelCB,RelAB,DomC2,DomA2,DomB20,DomC3,DomA3,DomB3),
+
+ (((DomA3 == DomA,
+ DomB3 == DomB,
+ DomC3 == DomC0);
+ (mreal:dom_size(DomA3,1),
+ mreal:dom_size(DomB3,1)))
+ ->
+ NDomA = DomA3,
+ NDomB = DomB3,
+ NDomC = DomC3
+ ; NCredit is Credit - 1,
+ minus_real_rec(NCredit,FIA,FIB,FIC,DomA3,DomB3,DomC3,RelAB,RelCB,RelAC,NDomA,NDomB,NDomC)).
minus_float_rec(0,1,Type,A,B,C) :- !,
- (getval(gdbg,1)@eclipse ->
- writeln(output,max_iter:minus_float_rec(A,B,C))
- ; true).
+ (getval(gdbg,1)@eclipse ->
+ writeln(output,max_iter:minus_float_rec(A,B,C))
+ ; true).
minus_float_rec(Cpt,RS,Type,A,B,C) :-
mreal:dvar_domain(A,DomA0),
mreal:dvar_domain(B,DomB0),
@@ -10885,20 +10885,31 @@ mult_real_2_args_equal(Type,X,Y,Z,Continue) :-
mult_real_2_args_equal(Type,A,B,C,Continue) :-
get_saved_cstr_suspensions(LSusp),
member((Susp,op_real1(Type,X,Y)),LSusp),
- ( A == X,
- (B == Y, Goal = (square_real(Type,A,OpC),op_real(Type,OpC,C)); %% A * -A = C
- C == Y, Goal = mult_real_op_arg_res(Type,A,B,Continue)) %% A * B = -A, ie A * -B = A
- ; A == Y,
- (B == X, Goal = (square_real(Type,A,OpC),op_real(Type,OpC,C)); %% -B * B = C
- C == X, Goal = mult_real_op_arg_res(Type,A,B,Continue)) %% -C * B = C, ie C * -B = C
- ; B == X,
- (A == Y, Goal = (square_real(Type,A,OpC),op_real(Type,OpC,C)); %% -B * B = C
- C == Y, Goal = mult_real_op_arg_res(Type,B,A,Continue)) %% A * B = -B, ie B * -A = B
- ; B == Y,
- (A == X, Goal = (square_real(Type,A,OpC),op_real(Type,OpC,C)); %% A * -A = C
- C == X, Goal = mult_real_op_arg_res(Type,B,A,Continue))),%% A * -C = C, ie C * -A = C
+ (A == X ->
+ (B == Y ->
+ % -A = B et A * -A = C
+ Goal = (square_real(Type,A,OpC),op_real(Type,OpC,C))
+ ; C == Y,
+ % -A = C et A * B = -A
+ Goal = mult_real_op_arg_res(Type,A,B,Continue))
+ ; (A == Y ->
+ (B == X ->
+ % -B = A et -B * B = C
+ Goal = (square_real(Type,B,OpC),op_real(Type,OpC,C))
+ ; C == X,
+ % A = -C et -C * B = C, ie C * B = -C
+ Goal = mult_real_op_arg_res(Type,C,B,Continue))
+ ; (B == X ->
+ % A <> Y
+ C == Y,
+ % -B = C et A * B = -B, ie B * A = -B
+ Goal = mult_real_op_arg_res(Type,B,A,Continue)
+ ; B == Y,
+ C == X,
+ % B = -C et A * -C = C, C * A = -C
+ Goal = mult_real_op_arg_res(Type,C,A,Continue)))),
!,
- call_priority(Goal,2).
+ call(Goal).
mult_real_2_args_equal(_,_,_,_,1).
@@ -10922,9 +10933,9 @@ mult_real_op_arg_res(Type,A,B,Continue) :-
(Type == real ->
% A == 0.0 et/ou B == -1.0
(diff_real_value(A,0.0) ->
- protected_unify(B = -1.0)
+ protected_unify(B,-1.0)
; (diff_real_value(B,-1.0) ->
- protected_unify(A = 0.0)
+ protected_unify(A,0.0)
; Continue = 1))
; % B change le signe de A donc B neg
mreal:dvar_remove_greater(B,-0.0),
@@ -11156,6 +11167,7 @@ mult_real_inst0(Type,A,B,C,Continue) :-
Continue = 1
; Continue = 1)))))).
+%refute_null_mult_real(A,B,Work) :- !.
refute_null_mult_real(A,B,Work) :-
get_priority(P),
set_priority(12),
@@ -11222,44 +11234,45 @@ mult_real_rec(Type,A,B,C) :-
get_float_int_status(A,FIA),%%PMO
get_float_int_status(B,FIB),%%PMO
get_float_int_status(C,FIC),%%PMO
- mult_real_float_rec(Type,FIA,FIB,FIC,RelAB,RelCB,RelCA,A,B,C,DomA,DomB,DomC).
-
-:- mode mult_real_float_rec(++,++,++,++,++,++,++,?,?,?,++,++,++).
-mult_real_float_rec(Type,FIA,FIB,FIC,RelAB,RelCB,RelCA,A,B,C,DomA,DomB,DomC) :-
- mreal:dom_interval(DomA,InterA),
- mreal:dom_interval(DomB,InterB),
- mreal:dom_interval(DomC,InterC),
- %% On freine des qu'un des produit cart�sien est sup a MaxProd
- (check_maxprod_intervals(InterA,InterB,InterC) ->
- %% On ne travaille que sur les bornes
- mult_real_dom_bounds(Type,RelAB,FIA,FIB,FIC,DomA,DomB,DomC,DomC0),
- real_inter_dom_if_eq(RelCA,RelCB,DomA,DomB,DomC0,DomA1,DomB1,DomC1),
- inv_mult_real_dom_bounds(Type,RelCB,FIC,FIB,FIA,DomC1,DomB1,DomA1,DomA10),
-
- real_inter_dom_if_eq(RelCA,RelCB,DomA10,DomB1,DomC1,DomA2,DomB2,DomC2),
- inv_mult_real_dom_bounds(Type,RelCA,FIC,FIA,FIB,DomC2,DomA2,DomB2,DomB20)
- ; mult_real_dom(Type,RelAB,FIA,FIB,FIC,DomA,DomB,DomC,DomC0),
-
- real_inter_dom_if_eq(RelCA,RelCB,DomA,DomB,DomC0,DomA1,DomB1,DomC1),
- inv_mult_real_dom(Type,RelCB,FIC,FIB,FIA,DomC1,DomB1,DomA1,DomA10),
-
- real_inter_dom_if_eq(RelCA,RelCB,DomA10,DomB1,DomC1,DomA2,DomB2,DomC2),
- inv_mult_real_dom(Type,RelCA,FIC,FIA,FIB,DomC2,DomA2,DomB2,DomB20)),
-
- real_inter_dom_if_eq(RelAB,RelCB,DomA2,DomC2,DomB20,DomA3,DomC3,DomB3),
-
- reduce_dom_inv_mult_eq_args(Type,FIA,FIB,RelCA,RelCB,DomA3,DomB3,DomC3,NDomA,NDomB,NDomC),
- (((NDomA = DomA,% = necessaire
- NDomB = DomB,
- NDomC = DomC0);
- (mreal:dom_size(NDomA,1),
- mreal:dom_size(NDomB,1)))
- ->
- %% On a fini : un seul update pour tout le point fixe
- mreal:dvar_set(A,NDomA),
- mreal:dvar_set(B,NDomB),
- mreal:dvar_set(C,NDomC)
- ; mult_real_float_rec(Type,FIA,FIB,FIC,RelAB,RelCB,RelCA,A,B,C,NDomA,NDomB,NDomC)).
+ mult_real_float_rec(5,Type,FIA,FIB,FIC,RelAB,RelCB,RelCA,A,B,C,DomA,DomB,DomC).
+
+:- mode mult_real_float_rec(++,++,++,++,++,++,++,++,?,?,?,++,++,++).
+mult_real_float_rec(0,Type,FIA,FIB,FIC,RelAB,RelCB,RelCA,A,B,C,DomA,
+ DomB,DomC) ?- !,
+ mreal:dvar_set(A,DomA),
+ mreal:dvar_set(B,DomB),
+ mreal:dvar_set(C,DomC).
+mult_real_float_rec(Credit,Type,FIA,FIB,FIC,RelAB,RelCB,RelCA,A,B,C,DomA,DomB,DomC) :-
+ mreal:dom_interval(DomA,InterA),
+ mreal:dom_interval(DomB,InterB),
+ mreal:dom_interval(DomC,InterC),
+ % On freine des qu'un des produit cart�sien est sup a MaxProd
+ (check_maxprod_intervals(InterA,InterB,InterC) ->
+ % On ne travaille que sur les bornes
+ mult_real_dom_bounds(Type,RelAB,FIA,FIB,FIC,DomA,DomB,DomC,DomC0),
+ real_inter_dom_if_eq(RelCA,RelCB,DomA,DomB,DomC0,DomA1,DomB1,DomC1),
+ inv_mult_real_dom_bounds(Type,RelCB,FIC,FIB,FIA,DomC1,DomB1,DomA1,DomA10),
+ real_inter_dom_if_eq(RelCA,RelCB,DomA10,DomB1,DomC1,DomA2,DomB2,DomC2),
+ inv_mult_real_dom_bounds(Type,RelCA,FIC,FIA,FIB,DomC2,DomA2,DomB2,DomB20)
+ ; mult_real_dom(Type,RelAB,FIA,FIB,FIC,DomA,DomB,DomC,DomC0),
+ real_inter_dom_if_eq(RelCA,RelCB,DomA,DomB,DomC0,DomA1,DomB1,DomC1),
+ inv_mult_real_dom(Type,RelCB,FIC,FIB,FIA,DomC1,DomB1,DomA1,DomA10),
+ real_inter_dom_if_eq(RelCA,RelCB,DomA10,DomB1,DomC1,DomA2,DomB2,DomC2),
+ inv_mult_real_dom(Type,RelCA,FIC,FIA,FIB,DomC2,DomA2,DomB2,DomB20)),
+ real_inter_dom_if_eq(RelAB,RelCB,DomA2,DomC2,DomB20,DomA3,DomC3,DomB3),
+ reduce_dom_inv_mult_eq_args(Type,FIA,FIB,RelCA,RelCB,DomA3,DomB3,DomC3,NDomA,NDomB,NDomC),
+ (((NDomA = DomA,% = necessaire
+ NDomB = DomB,
+ NDomC = DomC0);
+ (mreal:dom_size(NDomA,1),
+ mreal:dom_size(NDomB,1)))
+ ->
+ % On a fini : un seul update pour tout le point fixe
+ mreal:dvar_set(A,NDomA),
+ mreal:dvar_set(B,NDomB),
+ mreal:dvar_set(C,NDomC)
+ ; NCredit is Credit - 1,
+ mult_real_float_rec(NCredit,Type,FIA,FIB,FIC,RelAB,RelCB,RelCA,A,B,C,NDomA,NDomB,NDomC)).
%% On ameliore la reduction de A (ou B) quand A = C (ou B = C)
@@ -14668,62 +14681,62 @@ div_real_op_arg1_res(Type,A,B,OpA,Continue) :-
%% Point fixe
div_real_rec(Type,A,B,C) :-
- mreal:dvar_domain(A,DomA),
- mreal:dvar_domain(B,DomB),
- mreal:dvar_domain(C,DomC),
- get_rel_between_real_args(A,B,RelAB),
- get_rel_between_real_args(C,B,RelCB),
- get_rel_between_real_args(A,C,RelAC),
- get_float_int_status(A,FIA),%%PMO
- get_float_int_status(B,FIB),%%PMO
- get_float_int_status(C,FIC),%%PMO
- div_real_float_rec(5,Type,FIA,FIB,FIC,RelAB,RelCB,RelAC,A,B,C,DomA,DomB,DomC).
+ mreal:dvar_domain(A,DomA),
+ mreal:dvar_domain(B,DomB),
+ mreal:dvar_domain(C,DomC),
+ get_rel_between_real_args(A,B,RelAB),
+ get_rel_between_real_args(C,B,RelCB),
+ get_rel_between_real_args(A,C,RelAC),
+ get_float_int_status(A,FIA),%%PMO
+ get_float_int_status(B,FIB),%%PMO
+ get_float_int_status(C,FIC),%%PMO
+ div_real_float_rec(5,Type,FIA,FIB,FIC,RelAB,RelCB,RelAC,A,B,C,DomA,DomB,DomC).
:- mode div_real_float_rec(++,++,++,++,++,++,++,++,?,?,?,++,++,++).
div_real_float_rec(Cpt,Type,FIA,FIB,FIC,RelAB,RelCB,RelAC,A,B,C,DomA,DomB,DomC) :-
- mreal:dom_interval(DomA,InterA),
- mreal:dom_interval(DomB,InterB),
- mreal:dom_interval(DomC,InterC),
- (RelCB == '=' ->
- % On est en simple/double car div_real_2_args_equal a delegue
- % le calcul a square_real en mode real
- % A/B = B, A est "presque" le carre de B (et C)
- % A > 0, B <> 0, A et B <> +/-Inf
- div_float_dom_eqBC(Type,FIA,FIB,DomA,DomB,DomA1,DomB1),
- inv1_div_float_dom_eqBC(Type,FIB,FIA,DomB1,DomA1,DomB20,DomA2),
- DomC2 = DomB20
- ;
- %% On freine des qu un des produit cartesien est sup a MaxProd
- (check_maxprod_intervals(InterA,InterB,InterC) ->
- %% On ne travaille que sur les bornes
- div_real_float_dom_bounds(Type,RelAB,FIA,FIB,FIC,DomA,DomB,DomC,DomC0),
- real_inter_dom_if_eq(RelAC,RelCB,DomA,DomB,DomC0,DomA1,DomB1,DomC1),
-
- inv1_div_real_float_dom_bounds(Type,RelCB,FIC,FIB,FIA,DomC1,DomB1,DomA1,DomA10),
- real_inter_dom_if_eq(RelAC,RelAB,DomC1,DomB1,DomA10,DomC2,DomB2,DomA2),
-
- inv2_div_real_float_dom_bounds(Type,RelAC,FIA,FIC,FIB,DomA2,DomC2,DomB2,DomB20)
- ; div_real_float_dom(Type,RelAB,FIA,FIB,FIC,DomA,DomB,DomC,DomC0),
- real_inter_dom_if_eq(RelAC,RelCB,DomA,DomB,DomC0,DomA1,DomB1,DomC1),
-
- inv1_div_real_float_dom(Type,RelCB,FIC,FIB,FIA,DomC1,DomB1,DomA1,DomA10),
- real_inter_dom_if_eq(RelAC,RelAB,DomC1,DomB1,DomA10,DomC2,DomB2,DomA2),
-
- inv2_div_real_float_dom(Type,RelAC,FIA,FIC,FIB,DomA2,DomC2,DomB2,DomB20))),
-
- real_inter_dom_if_eq(RelAB,RelCB,DomA2,DomC2,DomB20,DomA3,DomC3,DomB3),
- reduce_dom_inv2_div_eq_args(Type,FIA,FIB,RelAC,DomA3,DomB3,DomC3,NDomA,NDomB,NDomC),
- ((Cpt == 0;
+ mreal:dom_interval(DomA,InterA),
+ mreal:dom_interval(DomB,InterB),
+ mreal:dom_interval(DomC,InterC),
+ (RelCB == '=' ->
+ % On est en simple/double car div_real_2_args_equal a delegue
+ % le calcul a square_real en mode real
+ % A/B = B, A est "presque" le carre de B (et C)
+ % A > 0, B <> 0, A et B <> +/-Inf
+ div_float_dom_eqBC(Type,FIA,FIB,DomA,DomB,DomA1,DomB1),
+ inv1_div_float_dom_eqBC(Type,FIB,FIA,DomB1,DomA1,DomB20,DomA2),
+ DomC2 = DomB20
+ ;
+ % On freine des qu un des produit cartesien est sup a MaxProd
+ (check_maxprod_intervals(InterA,InterB,InterC) ->
+ % On ne travaille que sur les bornes
+ div_real_float_dom_bounds(Type,RelAB,FIA,FIB,FIC,DomA,DomB,DomC,DomC0),
+ real_inter_dom_if_eq(RelAC,RelCB,DomA,DomB,DomC0,DomA1,DomB1,DomC1),
+
+ inv1_div_real_float_dom_bounds(Type,RelCB,FIC,FIB,FIA,DomC1,DomB1,DomA1,DomA10),
+ real_inter_dom_if_eq(RelAC,RelAB,DomC1,DomB1,DomA10,DomC2,DomB2,DomA2),
+
+ inv2_div_real_float_dom_bounds(Type,RelAC,FIA,FIC,FIB,DomA2,DomC2,DomB2,DomB20)
+ ; div_real_float_dom(Type,RelAB,FIA,FIB,FIC,DomA,DomB,DomC,DomC0),
+ real_inter_dom_if_eq(RelAC,RelCB,DomA,DomB,DomC0,DomA1,DomB1,DomC1),
+
+ inv1_div_real_float_dom(Type,RelCB,FIC,FIB,FIA,DomC1,DomB1,DomA1,DomA10),
+ real_inter_dom_if_eq(RelAC,RelAB,DomC1,DomB1,DomA10,DomC2,DomB2,DomA2),
+
+ inv2_div_real_float_dom(Type,RelAC,FIA,FIC,FIB,DomA2,DomC2,DomB2,DomB20))),
+
+ real_inter_dom_if_eq(RelAB,RelCB,DomA2,DomC2,DomB20,DomA3,DomC3,DomB3),
+ reduce_dom_inv2_div_eq_args(Type,FIA,FIB,RelAC,DomA3,DomB3,DomC3,NDomA,NDomB,NDomC),
+ ((Cpt == 0;
(NDomA = DomA,% = necessaire pour les cstes (type variable)
- NDomB = DomB,
- NDomC = DomC0);
- (mreal:dom_size(NDomA,1),
- mreal:dom_size(NDomB,1)))
- ->
- mreal:dvar_set(A,NDomA),
- mreal:dvar_set(B,NDomB),
- mreal:dvar_set(C,NDomC)
- ; NCpt is Cpt - 1,
+ NDomB = DomB,
+ NDomC = DomC0);
+ (mreal:dom_size(NDomA,1),
+ mreal:dom_size(NDomB,1)))
+ ->
+ mreal:dvar_set(A,NDomA),
+ mreal:dvar_set(B,NDomB),
+ mreal:dvar_set(C,NDomC)
+ ; NCpt is Cpt - 1,
div_real_float_rec(NCpt,Type,FIA,FIB,FIC,RelAB,RelCB,RelAC,A,B,C,NDomA,NDomB,NDomC)).
@@ -16295,9 +16308,10 @@ power_real_inst(Type,Val1,N,Val,Continue) :-
power_real_rec(Type,Val1,N,Val) :-
mreal:dvar_domain(Val1,Dom1),
mreal:dvar_domain(Val,Dom),
- power_real_rec(Type,Val1,N,Val,Dom1,Dom).
+ power_real_rec(5,Type,Val1,N,Val,Dom1,Dom).
-power_real_rec(Type,Val1,N,Val,Dom1,Dom) :-
+power_real_rec(Credit0,Type,Val1,N,Val,Dom1,Dom) ?- !.
+power_real_rec(Credit,Type,Val1,N,Val,Dom1,Dom) :-
% Val = exp(Val1)
mreal:dom_interval(Dom1,LInter1),
power_real_interval_list(Type,LInter1,N,PowLInter),
@@ -16316,7 +16330,8 @@ power_real_rec(Type,Val1,N,Val,Dom1,Dom) :-
(NewDom1 = Dom1 ->
% On a fini
true
- ; power_real_rec(Type,Val1,N,Val,NewDom1,NewDom)).
+ ; NCredit is Credit - 1,
+ power_real_rec(NCredit,Type,Val1,N,Val,NewDom1,NewDom)).
%% Typage et calcul de la projection directe
@@ -19305,14 +19320,13 @@ geq_real_int_ineq(A,B) :-
(is_real_box_rat(B,MinB) ->
MaxB = MinB
; mreal:dvar_range(B,MinB,MaxB)),
- ((MaxA == 1.0Inf;
- MinB == -1.0Inf)
+ ((abs(MaxA) =:= 1.0Inf;
+ abs(MinB) =:= 1.0Inf)
->
H = 1.0Inf
; H is rational(MaxA) - rational(MinB)),
- ((MaxA \== 1.0Inf,
- MinA \== -1.0Inf,
- MaxB =< MinA)
+ ((abs(MinA) =\= 1.0Inf,
+ abs(MaxB) =\= 1.0Inf)
->
% Forme resolue, pas d'inf ici
L is rational(MinA) - rational(MaxB)
@@ -19632,14 +19646,13 @@ gt_real_int_ineq(A,B) :-
(is_real_box_rat(B,MinB) ->
MaxB = MinB
; mreal:dvar_range(B,MinB,MaxB)),
- ((MaxA == 1.0Inf;
- MinB == -1.0Inf)
+ ((abs(MaxA) =:= 1.0Inf;
+ abs(MinB) =:= 1.0Inf)
->
H = 1.0Inf
; H is rational(MaxA) - rational(MinB)),
- ((MaxA \== 1.0Inf,
- MinA \== -1.0Inf,
- MaxB < MinA)
+ ((abs(MinA) =\= 1.0Inf,
+ abs(MaxB) =\= 1.0Inf)
->
% Forme resolue, pas d'inf ici
L is rational(MinA) - rational(MaxB)
@@ -21794,7 +21807,8 @@ one_prod_is_geq_maxprod(LA,LB,LC,MaxProd) :-
!.
% Essai abstraction inegalites a travers les cast vers double et rounding
-%compare_real_terms(A,B,?) :- !.
+% INHIBE trop cher
+compare_real_terms(A,B,?) :- !.
compare_real_terms(A,B,Rel) :-
((real_term(A,[],NA),
real_term(B,[],NB),
@@ -21810,9 +21824,13 @@ real_term(A,Seen,NA) :-
!,
NA = A.
real_term(A,Seen,NA) :-
+ (var(A) ->
+ not occurs(A,Seen)
+ ; true),
+ !,
suspensions(A,LSusp),
((member(Susp,LSusp),
- not member(Susp,Seen),
+ %not member(Susp,Seen),
get_suspension_data(Susp,goal,Goal),
(Goal = cast_float_to_double_bis(FA,AA),
A == AA,
@@ -21876,9 +21894,11 @@ real_term(A,Seen,NA) :-
NA = NA0
; NA =.. [NRnA,NA0]))))
->
- NSeen = [Susp|Seen],
+ NSeen = [A|Seen],
call(Todo)
; NA = A).
+real_term(A,Seen,NA) :-
+ NA = A.
check_exists_rel_between_real_terms(A,A,Rel) ?- !,
diff --git a/Src/COLIBRI/smt_import.pl b/Src/COLIBRI/smt_import.pl
index 139904d36..a41b9b0af 100644
--- a/Src/COLIBRI/smt_import.pl
+++ b/Src/COLIBRI/smt_import.pl
@@ -15,6 +15,23 @@
:- include([new_parser_builtins]).
+% pour smt_unit_test
+get_logic_from_file(File,Slog) :-
+ (get_logic_from_file0(File,Slog) ->
+ true
+ ; Slog = "ALL").
+
+get_logic_from_file0(File,Slog) :-
+ open(File,read,Stream),
+ read_string(Stream,end_of_file,_,SFile),
+ close(Stream),
+ once substring(SFile, S, Len, "set-logic "),
+ NS is S + Len,
+ once (substring(SFile, NS, L, R),
+ append_strings(Beg,")",R)),
+ split_string(Beg," ","",NR),
+ join_string(NR,"",Slog).
+
parse_smtlib_file(File,Res) :-
% passera à 1 si Int rencontré
setval(int_used,0)@eclipse,
@@ -29,14 +46,23 @@ parse_smtlib_file(File,Res) :-
; true),
(getval(scrambler,1)@eclipse ->
% avec scrambling, uniquement sous Linux
- concat_string(["sh -c \"scrambler -support-non-smtcomp true < ",File," > check.smt2\""],Com),
+ pathname(File,Path,_,_),
+ append_strings(Path,"check.scr",FilteredFile),
+ concat_string(["sh -c \"scrambler -support-non-smtcomp true < ",
+ File," > ",
+ FilteredFile,"\""],Com),
+ %writeln(error,scrambling),
exec(Com,[null,null,null],ComPid),
wait(ComPid,Status),
- Status == 0,
- FilteredFile = 'check.smt2'
+ Status == 0
; FilteredFile = File),
- p_simplex_ocaml_create_parser(FilteredFile,PEnv),
- read_dolmen_terms(PEnv,Res).
+ block((p_simplex_ocaml_create_parser(FilteredFile,PEnv),
+ read_dolmen_terms(PEnv,Res)),
+ Tag,
+ (getval(scrambler,1)@eclipse ->
+ writeln(output,"pb scrambler":File),
+ exit(4)
+ ; exit_block(Tag))).
read_dolmen_terms(PEnv,Terms) :-
p_simplex_ocaml_parser_next(PEnv,DTerm),
@@ -665,6 +691,7 @@ check_sat0 :-
check_sat_vars :-
not not check_sat_vars0.
check_sat_vars0 :-
+ reset_solve_timeout,
setval(diag_code,(wrong_sat,2))@eclipse,
getval(gsat,Goals-GVars)@eclipse,
(foreach((V,Type,CV),GVars) do
@@ -797,7 +824,8 @@ get_model :-
Type == rnd;
Type = sort(_))
->
- inst_type(Type,V)
+ remove_upper_as(V,VV,_),
+ inst_type(Type,VV)
; true))),
dump_smt_model(Vars)
; true),
@@ -964,7 +992,11 @@ dump_type_val('Int',Val0,Val) ?- !,
(float(Val0) ->
% simulation real/int
integer(Val0,Val1)
- ; Val1 = Val0),
+ ; (var(Val0) ->
+ (is_real_box_rat(Val0,Rat) ->
+ numerator(Rat,Val1)
+ ; dump_type_val('Real',Val0,Val1))
+ ; Val1 = Val0)),
(Val1 < 0 ->
Op is -Val1,
concat_string(["(- ",Op,")"],Val)
@@ -1016,14 +1048,40 @@ dump_type_val('RoundingMode',Val0,Val) ?- !,
true
; % rne par defaut
Val = 'RNE').
+dump_type_val('(_ FloatingPoint 8 24)',Val0,Val) ?- !,
+ dump_type_val('_'('FloatingPoint',8,24),Val0,Val).
dump_type_val('_'('FloatingPoint',8,24),Val0,Val) ?- !,
(Val0 == nan ->
- concat_string(["(_ NaN ",8," ",24,")"],Val)
+ SVal = "NaN"
+ ; (Val0 == 1.0Inf ->
+ SVal = "+oo"
+ ; (Val0 == -1.0Inf ->
+ SVal = "-oo"
+ ; (Val0 == 0.0 ->
+ SVal = "+zero"
+ ; (Val0 == -0.0 ->
+ SVal = "-zero"
+ ; true))))),
+ (nonvar(SVal) ->
+ concat_string(["(_ ",SVal," 8 24)"],Val)
; get_raw_uint_from_float(float_simple,Val0,I),
concat_string(["((_ to_fp ",8," ",24,") (_ bv",I," ",32,"))"],Val)).
+dump_type_val('(_ FloatingPoint,11,53)',Val0,Val) ?- !,
+ dump_type_val('_'('FloatingPoint',11,53),Val0,Val).
dump_type_val('_'('FloatingPoint',11,53),Val0,Val) ?- !,
(Val0 == nan ->
- concat_string(["(_ NaN ",11," ",53,")"],Val)
+ SVal = "NaN"
+ ; (Val0 == 1.0Inf ->
+ SVal = "+oo"
+ ; (Val0 == -1.0Inf ->
+ SVal = "-oo"
+ ; (Val0 == 0.0 ->
+ SVal = "+zero"
+ ; (Val0 == -0.0 ->
+ SVal = "-zero"
+ ; true))))),
+ (nonvar(SVal) ->
+ concat_string(["(_ ",SVal," 11 53)"],Val)
; get_raw_uint_from_float(float_double,Val0,I),
concat_string(["((_ to_fp ",11," ",53,") (_ bv",I," ",64,"))"],Val)).
dump_type_val('_'('BitVec',Size),Val0,Val) ?- !,
@@ -1158,7 +1216,8 @@ dump_smt_sort(Sort,NSort) :-
foreach(NArg,NArgs) do
dump_smt_sort(Arg,NArg)),
join_string([F|NArgs]," ",NSort0),
- concat_string(["(",NSort0,")"],NSort)).
+ concat_string(["(",NSort0,")"],SNSort),
+ atom_string(NSort,SNSort)).
factorize_and_dump_uninterps([]).
factorize_and_dump_uninterps([(VN,InSorts,OutSort)|Uninterps]) :-
@@ -1194,6 +1253,7 @@ factorize_and_dump_uninterps([(VN,InSorts,OutSort)|Uninterps]) :-
factorize_and_dump_uninterps(Uninterps).
% Constante
+% DANGER: AJOUTER LES declare-fun POUR CHAQUE CONSTANTE NON-INTERPRETEE !!!!
dump_smt_uninterps([],_,OutSort,Default) :-
((get_type_from_sort(OutSort,Type,_),
Type = sort(_))
@@ -1728,7 +1788,8 @@ new_let_var(VId) :-
smt_interp(Expr,IExpr,Type) :-
(check_seen_expr(Expr,IExpr,Type) ->
true
- ; smt_interp0(Expr,IExpr,Type),
+ ; check_solve_timeout,
+ smt_interp0(Expr,IExpr,Type),
add_seen_expr(Expr,IExpr,Type)).
:- setval(logic,"ALL")@eclipse.
@@ -2450,14 +2511,20 @@ smt_interp0(colibri_pow_int_int(A,B),colibri_pow_int(IA,IB),Type) :- !,
smt_interp(A,IA0,int),
add_as(int,IA0,IA),
smt_interp(B,IB,int)).
-smt_interp0(colibri_max(A,B),max(IA,IB),Type) :- !,
+smt_interp0(colibri_max(A,B),Exp,Type) :- !,
smt_interp(A,IA0,Type),
add_as(Type,IA0,IA),
- smt_interp(B,IB,Type).
-smt_interp0(colibri_min(A,B),min(IA,IB),Type) :- !,
+ smt_interp(B,IB,Type),
+ (occurs(Type,(float_simple,float_double)) ->
+ Exp = fp_max(IA,IB)
+ ; Exp = max(IA,IB)).
+smt_interp0(colibri_min(A,B),Exp,Type) :- !,
smt_interp(A,IA0,Type),
add_as(Type,IA0,IA),
- smt_interp(B,IB,Type).
+ smt_interp(B,IB,Type),
+ (occurs(Type,(float_simple,float_double)) ->
+ Exp = fp_min(IA,IB)
+ ; Exp = min(IA,IB)).
% real/float/double
smt_interp0(colibri_exp(A),Exp,Type) :-
smt_interp(A,IA0,Type0),
@@ -2942,7 +3009,7 @@ new_quantifier_abstraction(Res) :-
setval(quantifier,1),
% On cree une variable
get_decl_type_from_sort('Bool',NVar,Decl,bool),
- protected_set_var_name(NVar,"ColQuant"),
+ set_var_name(NVar,"ColQuant"),
protected_get_var_name(NVar,VS),
atom_string(Id,VS),
add_binding(Id,bool,NVar),
@@ -2955,6 +3022,7 @@ new_quantifier_abstraction(Res) :-
Res = as(NVar,bool).
is_quantifier_abstraction(Var) :-
+ var(Var),
protected_get_var_name(Var,VS),
append_strings("ColQuant",_,VS).
@@ -3062,11 +3130,7 @@ get_decl_type_from_sort('Int',NVar,Decl,Type) :- !,
Decl = real_vars(real_int,NVar)
; Decl = int_vars(int,NVar)).
get_decl_type_from_sort('_'('BitVec',N),NVar,Decl,uint(N)) :- !,
- ((getval(unit_tests,1)@eclipse,
- N > 256) ->
- concat_string([" format (_ BitVec ",N,")"],Mess),
- unsupported_error(Mess)
- ; Decl = int_vars(uint(N),NVar)).
+ Decl = int_vars(uint(N),NVar).
get_decl_type_from_sort('Real',NVar,Decl,real) :- !,
Decl = real_vars(real,NVar).
get_decl_type_from_sort('_'('FloatingPoint',EB,SB),NVar,Decl,Type) :- !,
@@ -3465,7 +3529,10 @@ smt_interp_file(File,NewGoals) :-
OD = ID,
OE = IE,
make_conj(IG,Goal,OG)))))),
- make_conj(Array_elts,Goals,Goals1),
+ (getval(force_model,1)@eclipse ->
+ make_conj(Goals,get_model,Goals0)
+ ; Goals0 = Goals),
+ make_conj(Array_elts,Goals0,Goals1),
make_conj(Array_defs,Goals1,Goals2),
make_conj(Array_vars,Goals2,Goals3),
make_conj(Sort_vars,Goals3,NewGoals),
diff --git a/Src/COLIBRI/solve.pl b/Src/COLIBRI/solve.pl
index 843934ab1..0c1f3f87c 100644
--- a/Src/COLIBRI/solve.pl
+++ b/Src/COLIBRI/solve.pl
@@ -472,7 +472,7 @@ protected_get_var_name(V,Name) :-
(var(V) ->
get_var_name(V,Name)
; call(spy_here)@eclipse,
- writeln(error,"Error: variable needed as first argument of get_var_name/2"),
+ fail,writeln(error,"Error: variable needed as first argument of get_var_name/2"),
exit_block(syntax)).
protected_set_var_name(V,Name) :-
(var(V) ->
@@ -896,15 +896,20 @@ unfold_int_expr(store(EA,EI,EE), _D, Cstr, Type, R) ?-
% pour les real_int
real_vars(real_int,I)
; let_int_vars(TI,I)),
- get_array_start(A,Start),
+% get_array_start(A,Start),
% insert_dep_inst(dep(I,0,[E,Start])),
% insert_dep_inst(dep(E,0,[I,Start]))
insert_dep_inst(dep(I,0,[E])),
insert_dep_inst(dep(E,0,[I]))
; true),
+/*
blocked_unify(R,storec(A,I,v(u,E,CE))),
make_conj(CA,CI,Cstr).
+*/
+ blocked_unify(R,storec(A,I,v(u,E,true))),
+ make_conj(CA,CI,CAI),
+ make_conj(CAI,CE,Cstr).
unfold_int_expr(storec(A,I,E), _D, Cstr, Type, R) ?-
% constructeur interne
!,
@@ -1937,7 +1942,6 @@ unfold_int_expr(EA / EB,D,Cstr,Type,R) ?- !,
unfold_int_expr(EA // EB,D,Cstr,Type,R).
unfold_int_expr(EA // EB,D,Cstr,Type,R) ?-
- call(spy_here)@eclipse,
ND is D + 1,
unfold_int_expr(EA,ND,CA,Type,A),
unfold_int_expr(EB,ND,CB,Type,B),
@@ -1960,7 +1964,6 @@ unfold_int_expr(EA // EB,D,Cstr,Type,R) ?-
make_conj(CAB,Cond,CABCond),
make_conj(CABCond,chk_undef_div_rem(Bool,Type,A,B,R,Rem,UO),Cstr).
unfold_int_expr(EA rem EB,D,Cstr,Type,R) ?-
- call(spy_here)@eclipse,
ND is D + 1,
unfold_int_expr(EA,ND,CA,Type,A),
unfold_int_expr(EB,ND,CB,Type,B),
@@ -2846,7 +2849,13 @@ unfold_int_expr(neg(EA),D,Cstr,Type,R) ?- !,
make_conj(CA,not_int(A,R),Cstr)
; Cstr = CA)).
-unfold_int_expr((EA and EB),D,Cstr,Type,R) ?-
+/*
+unfold_int_expr(((EA1 and EA2) and EB),D,Cstr,Type,R) ?-
+ nonvar(R),
+ !,
+ unfold_int_expr((EA1 and (EA2 and EB)),D,Cstr,Type,R).
+*/
+unfold_int_expr((EA and EB),D,Cstr,Type,R) ?-
Type = bool,
ND is D + 1,
(R == 1 ->
@@ -2904,7 +2913,18 @@ unfold_int_expr((EA and EB),D,Cstr,Type,R) ?-
; make_conj(CA,CB,CAB),
make_conj(CAB,and_reif(A,B,R),Cstr)))))).
-unfold_int_expr((EA or EB),D,Cstr,Type,R) ?-
+
+/*
+unfold_int_expr(((EA1 or EA2) or EB),D,Cstr,Type,R) ?-
+ nonvar(R),
+ !,
+ unfold_int_expr((EA1 or (EA2 or EB)),D,Cstr,Type,R).
+*/
+unfold_int_expr((EA or EB),D,Cstr,Type,R) ?-
+ var(R),
+ !,
+ unfold_int_expr(chk_nan(EA,as(1,bool),EB),D,Cstr,Type,R).
+unfold_int_expr((EA or EB),D,Cstr,Type,R) ?-
Type = bool,
ND is D + 1,
(R == 0 ->
@@ -3389,10 +3409,7 @@ unfold_let(From,[],E,D,Cstrs,Cstr,Type,R) :-
unfold_let(From,[(V,TypeV,EV)|T],E,D,Cstrs,Cstr,Type,R) :-
(var(TypeV) ->
exit_block(syntax)
- ; (real_type(TypeV,_) ->
- real_vars(TypeV,V)
- ; let_int_vars(TypeV,V)),
- (nonvar(V) ->
+ ; (nonvar(V) ->
% Autre occurence de ce let deja traitee
% on peut ignorer EV et reutiliser le resultat
NCstrs = Cstrs
@@ -3401,7 +3418,10 @@ unfold_let(From,[(V,TypeV,EV)|T],E,D,Cstrs,Cstr,Type,R) :-
; (real_type(TypeV,_) ->
unfold_real_expr(EV,D,CV,TypeV,V)
; unfold_int_expr(EV,D,CV,TypeV,V)),
- make_conj(Cstrs,CV,NCstrs)))),
+ make_conj(Cstrs,CV,NCstrs))),
+ (real_type(TypeV,_) ->
+ real_vars(TypeV,V)
+ ; let_int_vars(TypeV,V))),
unfold_let(From,T,E,D,NCstrs,Cstr,Type,R).
get_reif_var_depth_from_labchoice(D) :-
@@ -3803,7 +3823,7 @@ check_alldiffint_card(Bool,Kill,L) :-
check_alldiffint_card(Bool,Kill,NewL)
; (NewL = [_] ->
true
- ; suspend(check_alldiffint_card(Bool,Kill,NewL),0,(Bool,Kill,NewL)->suspend:constrained)))))),
+ ; my_suspend(check_alldiffint_card(Bool,Kill,NewL),0,(Bool,Kill,NewL)->suspend:constrained)))))),
set_priority(Prio),
wake_if_other_scheduled(Prio)).
@@ -4101,11 +4121,11 @@ get_array_start(storec(A,_,_),Start) :-
get_array_start(A,Start).
-/*
+% INHIBE: bugs sur QF_ABV
eval_select(Type,A,I,E,Start,Cstr) :- !,
get_array_start(A,Start),
Cstr = smtlib_select(Type,A,I,E).
-*/
+
% Evaluation partielle de select
eval_select(_Type,const_array(TI,TE,Const),_I,E,Start,Cstr) ?- !,
Start = const_array(TI,TE,Const),
@@ -4197,7 +4217,7 @@ check_before_suspend_select(NewA,NStart,I,E,TypeI,TypeE,SuspVars,LSusp) :-
(TypeE \= array(_,_) ->
protected_unify(E,EE)
; % TypeE = array(_,_)
- call(spy_here)@eclipse,
+ %call(spy_here)@eclipse,
check_eq_array(TypeE,E,EE))
; my_suspend(smtlib_select(NewA,NStart,I,E,TypeI,TypeE),4,SuspVars->suspend:constrained)).
@@ -7357,14 +7377,19 @@ unfold_real_expr(sqrt(EA),D,Cstr,RType,R) ?-
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).
-unfold_real_expr(ln(EA),D,Cstr,RType,R) ?-
+unfold_real_expr(ln(EA),D,Cstr,RType,R) ?- !,
ND is D + 1,
unfold_real_expr(EA,ND,CA,RType,A),
nonvar(RType),
real_type(RType,Type),
!,
- insert_dep_inst(dep(R,D,[A])),
- make_conj(CA,logn(Type,A,R),Cstr).
+ ensure_not_NaN([A,R]),
+ unfold_int_expr(as(A,real) $< as(0.0,Type),D,
+ CNeg,bool,Neg),
+ insert_dep_inst(inst_cstr(D,Neg)),
+ insert_dep_inst(dep(R,D,[Neg,A])),
+ make_conj(CA,CNeg,CACNeg),
+ make_conj(CACNeg,real_ln(Neg,A,R),Cstr).
% seulement rne
unfold_real_expr(fp_ln(EA),D,Cstr,Type,R) ?-
ND is D + 1,
@@ -7377,8 +7402,7 @@ unfold_real_expr(fp_ln(EA),D,Cstr,Type,R) ?-
!,
unfold_int_expr((isNaN(as(A,Type)) or fp_lt(as(A,Type),as(-0.0,Type))),D,
CNaN,bool,NaN),
- get_reif_var_depth_from_labchoice(DD),
- insert_dep_inst(inst_cstr(DD,NaN)),
+ insert_dep_inst(inst_cstr(D,NaN)),
insert_dep_inst(dep(R,D,[A,NaN])),
make_conj(CNaN,CA,CNA),
make_conj(CNA,fp_ln(NaN,Type,A,R),Cstr)).
@@ -7440,7 +7464,6 @@ unfold_real_expr(min(EA,EB),D,Cstr,RType,R) ?- !,
make_conj(CA,CB,CAB),
(occurs(Type,(float_simple,float_double)) ->
unfold_real_expr(fp_min(as(A,Type),as(B,Type)),D,CFP,Type,R),
- make_conj(CA,CB,CAB),
make_conj(CAB,CFP,Cstr)
; insert_dep_inst(dep(R,D,[A,B])),
make_conj(CAB,launch_min_real(Type,A,B,R),Cstr)).
@@ -7477,7 +7500,6 @@ unfold_real_expr(max(EA,EB),D,Cstr,RType,R) ?- !,
make_conj(CA,CB,CAB),
(occurs(Type,(float_simple,float_double)) ->
unfold_real_expr(fp_max(as(A,Type),as(B,Type)),D,CFP,Type,R),
- make_conj(CA,CB,CAB),
make_conj(CAB,CFP,Cstr)
; insert_dep_inst(dep(R,D,[A,B])),
make_conj(CAB,launch_max_real(Type,A,B,R),Cstr)).
@@ -8230,7 +8252,7 @@ fp_sub_inst(Rnd,Type,A,B,R,Continue) :-
((is_fzero(A),
not_zero(B))
->
- op_real(Type,A,B)
+ op_real(Type,B,R)
; ((is_fzero(B),
not_zero(A))
->
@@ -9714,7 +9736,7 @@ uninterp(F,Trigger,TypeArgs,TypeR,Args,R) :-
% factorisation
kill_suspension(Susp),
(TypeR = array(_,_) ->
- call(spy_here)@eclipse,
+ %call(spy_here)@eclipse,
eq_array(TypeR,R,CR)
; protected_unify(R,CR))
; (((TypeR = array(_,TE) ->
@@ -9725,10 +9747,9 @@ uninterp(F,Trigger,TypeArgs,TypeR,Args,R) :-
diff_reif(TA,_Kill,A,CA,1)
; true))
; true)),
- (ground(Args) ->
+ (ground((Args,R)) ->
my_suspend(uninterp(F,Trigger,TypeArgs,TypeR,Args,R),0,trigger(Trigger))
; my_suspend(uninterp(F,Trigger,TypeArgs,TypeR,Args,R),0,[(Args,R)->suspend:constrained,trigger(Trigger)])),
-% ; my_suspend(uninterp(F,Trigger,TypeArgs,TypeR,Args,R),0,(Args,R)->suspend:inst)),
set_priority(P),
wake_if_other_scheduled(P).
@@ -10264,13 +10285,8 @@ cdiv_crem(A,1.0,Q,R) ?- !,
cdiv_crem(A,-1.0,Q,R) ?- !,
protected_unify(R,0.0),
op_real(real,A,Q).
-
-% convergence lente sur cdiv_test_zero_sat.smt2
-% car on manque des congruences ici
-% A ajouter/adapter ?
cdiv_crem(A,B,Q,0.0) ?- !,
mult_real(real,B,Q,A).
-
cdiv_crem(A,A,Q,R) ?- !,
protected_unify(Q,1.0),
protected_unify(R,0.0).
@@ -10311,7 +10327,9 @@ cdiv_crem(A,B,Q,R) :-
(var(Continue) ->
true
; (not_unify(R,0.0) ->
- mreal:dvar_remove_element(A,0.0)
+ % donc A <> 0.0 et B ne divise pas A
+ mreal:dvar_remove_element(A,0.0),
+ refute_real_A_equals_R(A,Q,R)
; true),
(Q == 0.0 ->
protected_unify(A,R)
@@ -10386,12 +10404,40 @@ cdiv_crem(A,B,Q,R) :-
div_mod(IA,IB,IQ,IR),
cast_int_real(real,IQ,Q),
cast_int_real(real,IR,R)
- ; my_suspend(cdiv_crem(A,B,Q,R),
- 5,
+ ; (nonvar(SB) ->
+ Prio = 4
+ ; Prio = 5),
+ my_suspend(cdiv_crem(A,B,Q,R),
+ Prio,
(A,B,Q,R)->suspend:constrained)))),
set_priority(P),
wake_if_other_scheduled(P).
+% pour unsat.issue35.smt
+refute_real_A_equals_R(A,Q,R) :-
+ % A et B de meme signe et <> 0.0
+ set_priority(5),
+ block((not (protected_unify(Q,0.0),
+ protected_unify(A,R),
+ wake)
+ ->
+ set_priority(1),
+ launch_diff_real(real,A,R),
+ mreal:dvar_remove_element(Q,0.0),
+ force_lin_solve_var(A)
+ ; (not (diff_real(real,A,R),
+ mreal:dvar_remove_element(Q,0.0),
+ wake)
+ ->
+ set_priority(1),
+ protected_unify(Q,0.0),
+ protected_unify(A,R),
+ force_lin_solve_var(A)
+ ; set_priority(1))),
+ Tag,
+ (set_priority(1),
+ exit_block(Tag))).
+
cdiv_crem_inst_free(A,B,Q,R,Continue) :-
(A == 0.0 ->
protected_unify(Q,0.0),
@@ -10420,7 +10466,6 @@ cdiv_crem_inst_free(A,B,Q,R,Continue) :-
% car on manque des congruences ici
% A ajouter/adapter ?
(R == 0.0 ->
- call(spy_here)@eclipse,
mult_real(real,B,Q,A)
; (number(A) ->
(number(B) ->
@@ -10479,8 +10524,11 @@ check_exists_cdiv_crem(A,B,Q,R,Suspend) :-
->
(nonvar(ZQ) ->
Suspend = 1,
- protected_unify(Q,0),
- protected_unify(QQ,0)
+ % A = B*Q + R, A = BB*Q + R et B <> BB
+ % donc B*Q = BB*Q avec B et BB <> 0.0
+ % et donc Q = 0.0 et A = R
+ protected_unify(Q,0.0),
+ protected_unify(A,R)
; % Factorisation
protected_unify(A,AA),
protected_unify(B,BB),
@@ -10891,9 +10939,20 @@ fp_power(NaN,Type,A,N,R) :-
(NaN,A,R)->suspend:constrained))).
-fp_ln(1,_Type,_A,R) ?- !,
- protected_unify(R,nan).
+fp_ln(1,Type,A,R) ?-
+ ((A == nan;
+ R == nan)
+ ->
+ !,
+ protected_unify(A,nan),
+ protected_unify(R,nan)
+ ; check_not_NaN(A),
+ !,
+ ensure_not_NaN(R),
+ gt_real(Type,-0.0,A),
+ undef_fp_ln(Type,A,R)).
fp_ln(0,Type,A,R) ?- !,
+ % ni nan ni neg
ensure_not_NaN([A,R]),
set_typed_intervals(A,Type,[-0.0 .. 1.0Inf]),
set_typed_intervals(R,Type,[-1.0Inf .. 1.0Inf]),
@@ -10901,9 +10960,10 @@ fp_ln(0,Type,A,R) ?- !,
fp_ln(NaN,_Type,nan,R) ?- !,
protected_unify(NaN,1),
protected_unify(R,nan).
-fp_ln(NaN,_Type,_A,nan) ?- !,
- % A est NaN ou < -0
- protected_unify(NaN,1).
+fp_ln(NaN,_Type,A,nan) ?- !,
+ % A est NaN
+ protected_unify(NaN,1),
+ protected_unify(A,nan).
fp_ln(NaN,Type,A,R) :-
(check_not_NaN(R) ->
ensure_not_NaN(A),
@@ -10918,6 +10978,36 @@ fp_ln(NaN,Type,A,R) :-
protected_unify(R,RR)
; my_suspend(fp_ln(NaN,Type,A,R),0,
(NaN,A,R)->suspend:constrained))).
+undef_fp_ln(Type,A,R) :-
+ uninterp_trigger(fp_ln,[Type],Type,Trigger),
+ uninterp(fp_ln,Trigger,[Type],Type,[A],R).
+
+
+real_ln(1,A,R) ?- !,
+ ensure_not_NaN([A,R]),
+ gt_real(Type,-0.0,A),
+ undef_real_ln(A,R).
+real_ln(0,A,R) ?- !,
+ % pas neg
+ ensure_not_NaN([A,R]),
+ set_typed_intervals(A,real,[0.0 .. 1.0Inf]),
+ set_typed_intervals(R,real,[-1.0Inf .. 1.0Inf]),
+ logn(real,A,R).
+real_ln(Neg,A,R) :-
+ save_cstr_suspensions((A,R)),
+ get_saved_cstr_suspensions(LSusp),
+ ((member((_,real_ln(NNeg,AA,RR)),LSusp),
+ A == AA)
+ ->
+ protected_unify(Neg,NNeg),
+ protected_unify(R,RR)
+ ; my_suspend(real_ln(Neg,A,R),0,
+ (Neg,A,R)->suspend:constrained)).
+undef_real_ln(A,R) :-
+ uninterp_trigger(real_ln,[real],real,Trigger),
+ uninterp(real_ln,Trigger,[real],real,[A],R).
+
+
fp_exp(1,_Type,_A,R) ?- !,
protected_unify(R,nan).
@@ -11266,7 +11356,8 @@ new_choose_fd_var(UseList0,CVars,NCVars,Var,Size,NUseList) :-
connected_bool_vars(Var,Vars) :-
delayed_goals(Var,DGL),
- term_variables(DGL,CVars),
+ filter_array_goals(DGL,NDGL),
+ term_variables(NDGL,CVars),
(foreach(V,CVars),
fromto([],In,Out,Vars),
param(Var) do
@@ -11491,6 +11582,22 @@ choose_fd_var([Adj|UseList],Var,Size,NUseList) :-
% var_with_min_dom_max_cstr(MinVars,Var,Size).
*/
+%filter_array_goals(L,L) :- !.
+filter_array_goals([],[]).
+filter_array_goals([G|LG],[NG|NLG]) :-
+ functor(G,FG,Ar),
+ (occurs(FG,(smtlib_select,eq_array,diff_array1,diff_reif_array)) ->
+ ( G = diff_reif_array(_,_,_,_,Bool) ->
+ NG = Bool
+ ; G = diff_array1(_,_,_,SureA,SureB) ->
+ NG = (SureA,SureB)
+ ; G = eq_array(_,_,_,_,_,SureA,SureB) ->
+ NG = (SureA,SureB)
+ ; G = smtlib_select(_,_,I,_,_,_),
+ NG = I)
+ ; NG = G),
+ filter_array_goals(LG,NLG).
+
% Nouvelle version plus simple
choose_fd_var([Adj|UseList],Var,Size,NUseList) :-
% Recolte des variables de plus grand cycle
@@ -11498,7 +11605,8 @@ choose_fd_var([Adj|UseList],Var,Size,NUseList) :-
% et apparaissant dans une adjacence singleton ou paire avec resultat connu
% ou bien dans une adjacence ne contenant que des MaxCycleVars
delayed_goals(DG),
- term_variables(DG,Vars0),
+ filter_array_goals(DG,NDG),
+ term_variables(NDG,Vars0),
%filter_not_box_constrained_vars(Vars0,MinVars),
filter_constrained_vars(Vars0,MinVars),
MinVars \== [],
@@ -12019,6 +12127,7 @@ var_with_max_cstr_min_dom1([VV|LV],IV,IS,INb,Var,MinSize) :-
:- mode simple_solve_var(?,++).
simple_solve_var(Var,Size) :-
(var(Var) ->
+ check_solve_timeout,
get_type(Var,Type),
simple_solve_var_type(Type,Var,Size)
; true).
@@ -12117,16 +12226,22 @@ is_mult_div_arg(Var) :-
simple_resol_int(Int) :-
(var(Int) ->
call_priority(
- (protected_unify(Int,0);
- mfd:dvar_remove_element(Int,0),
- (is_mult_div_arg(Int) ->
- (protected_unify(Int,1);
- protected_unify(Int,-1);
- mfd:dvar_remove_element(Int,1),
- mfd:dvar_remove_element(Int,-1),
- simple_resol_int1(Int))
- ; simple_resol_int1(Int))),
- 1)
+ (not_unify(Int,0) ->
+ (is_mult_div_arg(Int) ->
+ (not_unify(Int,1) ->
+ (not_unify(Int,-1) ->
+ simple_resol_int1(Int)
+ ; (protected_unify(Int,-1);
+ mfd:dvar_remove_element(Int,-1),
+ simple_resol_int(Int)))
+ ; (protected_unify(Int,1);
+ mfd:dvar_remove_element(Int,1),
+ simple_resol_int(Int)))
+ ; simple_resol_int1(Int))
+ ; (protected_unify(Int,0);
+ mfd:dvar_remove_element(Int,0),
+ simple_resol_int(Int))),
+ 1)
; true).
simple_resol_int1(Int) :-
@@ -12138,11 +12253,11 @@ simple_resol_int1(Int) :-
% valeur absolue
abs_min_interval(IList,Inter),
( mfd:set_intervals(Int,[Inter])
- ; % On retire Inter du domaine de Int
+ ; % On retire Inter du domaine de Int
once member_begin_end(Inter,IList,NIList,End,End),
mfd:set_intervals(Int,NIList))
%simple_resol_int(Int)
- ; % Un seul intervalle
+ ; % Un seul intervalle
IList = [Inter],
min_max_inter(Inter,Min0,Max0),
( protected_unify(Int,Min0)
@@ -12433,10 +12548,17 @@ get_rand_rat_in_rbox(Var,Value,NV,Rat) :-
Rat is max(min(MinR,Rat1),MaxR)).
occurs_in_comp(Var,Comp) :-
+ mreal:dvar_range(Var,L,H),
+ (L,H) \== (-1.0Inf,1.0Inf),
delayed_goals(Var,Goals),
member(Comp,Goals),
functor(Comp,FComp,_),
- occurs(FComp,(gt_real,diff_real)).
+ occurs(FComp,(gt_real,diff_real)),
+ Comp =.. [_,X,Y],
+ mreal:dvar_range(X,LX,HX),
+ (LX,HX) \== (-1.0Inf,1.0Inf),
+ mreal:dvar_range(Y,LY,HY),
+ (LY,HY) \== (-1.0Inf,1.0Inf).
try_rat_satisfying_comp(gt_real(_,X,Y),Var,Rat) :-
(X == Var ->
@@ -12489,27 +12611,31 @@ try_rat_satisfying_comp(diff_real(_,X,Y),Var,Rat) :-
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
inst_type(bool,V) :-!,
- inst_bool(V).
+ inst_bool(V).
inst_type(enum(_),V) :-!,
- inst_enum(V).
+ inst_enum(V).
inst_type(rnd,V) :- !,
inst_rnd(V).
inst_type(int,V) :-!,
inst_int(V).
inst_type(int(_),V) :-
inst_int(V).
+inst_type(uint(_),V) :-
+ inst_int(V).
inst_type(real,V) :-
- inst_real(V).
+ inst_real(V).
+inst_type(real_int,V) :-
+ inst_real(V).
inst_type(real(_),V) :-
- inst_real(V).
+ inst_real(V).
inst_type(float_double,V) :-
- inst_float_double(V).
+ inst_float_double(V).
inst_type(float_double(_),V) :-
- inst_float_double(V).
+ inst_float_double(V).
inst_type(float_simple,V) :-
- inst_float_simple(V).
+ inst_float_simple(V).
inst_type(float_simple(_),V) :-
- inst_float_simple(V).
+ inst_float_simple(V).
inst_type(array(TI,TE),A) :-
inst_array(TI,TE,A).
inst_type(sort(S),A) :-
@@ -12519,7 +12645,7 @@ inst_type(sort(S),A) :-
random_less(N,Rand),
choose_value_in_interval(LIA,0,Rand,A0),
protected_unify(A,A0).
-inst_array(TI,TE,storec(A,I,(_,E,_))) ?- !,
+inst_array(TI,TE,storec(A,I,v(_,E,_))) ?- !,
inst_type(TI,I),
inst_type(TE,E),
inst_array(TI,TE,A).
diff --git a/Src/COLIBRI/util.pl b/Src/COLIBRI/util.pl
index f7bcce4f1..219bae34c 100755
--- a/Src/COLIBRI/util.pl
+++ b/Src/COLIBRI/util.pl
@@ -260,7 +260,24 @@ protected_unify(X,Y) :-
set_flag(occur_check,OC)
; protected_unify0(X,Y)).
*/
+protected_unify(storec(X,I,v(_,EI,CI)),storec(Y,J,v(_,EJ,CJ))) ?- !,
+ protected_unify(EI,EJ),
+ protected_unify(CI,CJ),
+ protected_unify(X,Y).
+protected_unify(storec(X,I,E),Y) ?- !,
+ (meta(Y) ->
+ not occurs(Y,(X,E))
+ ; true),
+ protected_unify0(Y,storec(X,I,E)).
+protected_unify(Y,storec(X,I,E)) ?- !,
+ (meta(Y) ->
+ not occurs(Y,(X,E))
+ ; true),
+ protected_unify0(Y,storec(X,I,E)).
protected_unify(X,Y) :-
+ protected_unify0(X,Y).
+
+protected_unify0(X,Y) :-
getval(from_pu,PU)@eclipse,
setval(from_pu,1)@eclipse,
block((X = Y ->
@@ -289,16 +306,23 @@ protected_occurs_in_list(X,L) :-
:- export protected_numerator/2.
protected_numerator(Rat,R) :-
+ NRat is Rat,
+ R is numerator(NRat).
+/*
block(R is numerator(Rat),
- _Tag,
- (call(spy_here)@eclipse,
- R is numerator(Rat))).
+ Tag,
+ (R is numerator(Rat))).
+*/
:- export protected_denominator/2.
protected_denominator(Rat,R) :-
+ NRat is Rat,
+ R is denominator(NRat).
+/*
block(R is denominator(Rat),
- _Tag,
+ Tag,
(call(spy_here)@eclipse,
R is denominator(Rat))).
+*/
%%:- mode unify_vars(+).
unify_vars([A|L]) :-
--
GitLab