From 798ef63598702de5363d32b49b0609c76b5ca65a Mon Sep 17 00:00:00 2001
From: Bruno Marre <bruno.marre@cea.fr>
Date: Wed, 23 Mar 2022 23:05:16 +0100
Subject: [PATCH 1/2] ajout issue54 corrigee
---
tests/sat/issue54.smt2 | 24 ++++++++++++++++++++++++
1 file changed, 24 insertions(+)
create mode 100644 tests/sat/issue54.smt2
diff --git a/tests/sat/issue54.smt2 b/tests/sat/issue54.smt2
new file mode 100644
index 000000000..5fcad14c3
--- /dev/null
+++ b/tests/sat/issue54.smt2
@@ -0,0 +1,24 @@
+(set-logic ALL)
+(set-info :smt-lib-version 2.6)
+(set-info :status sat)
+
+(define-fun uint_in_range ((i Int)) Bool
+ (and (<= 0 i) (<= i 18446744073709551615)))
+
+(declare-sort t 0)
+
+(declare-fun first (t) (_ BitVec 64))
+(declare-fun last (t) (_ BitVec 64))
+
+(define-fun t2_length ((a1 t)) Int
+ (ite (bvule (first a1) (last a1))
+ (+ (- (bv2nat (last a1)) (bv2nat (first a1))) 1)
+ 0))
+
+(declare-const c t)
+
+(assert (and (= (first c) #x0000000000000000) (= (last c) #xFFFFFFFFFFFFFFFF)))
+
+(assert (not (uint_in_range (t2_length c))))
+
+(check-sat)
--
GitLab
From 810134feedda6687086fb6b9b9740c7d806acc24 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Wed, 6 Apr 2022 12:06:53 +0200
Subject: [PATCH 2/2] Import from Bin:a1af7a0 Src:18e322698 farith:a93db57
---
Src/COLIBRI/arith.pl | 12 +-
Src/COLIBRI/arith_sched.pl | 70 +++---
Src/COLIBRI/check_lin_expr.pl | 42 ++--
Src/COLIBRI/col_solve.pl | 20 +-
Src/COLIBRI/lp_arith.pl | 232 ++++++++++++--------
Src/COLIBRI/realarith.pl | 392 ++++++++++++++++++++++------------
Src/COLIBRI/smt_import.pl | 50 +++--
Src/COLIBRI/solve.pl | 110 ++++------
Src/COLIBRI/util.pl | 163 +++++++-------
9 files changed, 649 insertions(+), 442 deletions(-)
diff --git a/Src/COLIBRI/arith.pl b/Src/COLIBRI/arith.pl
index be17f34c6..111fd00f5 100755
--- a/Src/COLIBRI/arith.pl
+++ b/Src/COLIBRI/arith.pl
@@ -284,11 +284,11 @@ check_reduced(_,_,1).
check_before_susp_add(A,B,C) :-
% On a peut etre une forme resolue
+ check_add_int_ineqs(A,B,C),
add_inst_free(A,B,C,Continue),
(var(Continue) ->
true
- ; check_add_int_ineqs(A,B,C),
- (ground((A,B,C)) ->
+ ; (ground((A,B,C)) ->
add_inst_free(A,B,C,_)
; set_prio_inst([A,B,C],4,5,Prio),
my_suspend(add_int(A,_,B,_,C,_), Prio, (A,B,C) -> suspend:constrained))).
@@ -1637,11 +1637,11 @@ mult_free_rec(Cpt,A,TA,B,TB,C,TC) :-
check_before_susp_mult(A,B,C) :-
+ check_mult_int_ineqs(A,B,C),
mult_inst(A,B,C,Continue),
(var(Continue) ->
true
- ; check_mult_int_ineqs(A,B,C),
- (ground((A,B,C)) ->
+ ; (ground((A,B,C)) ->
mult_inst(A,B,C,_)
; set_prio_inst([A,B,C],4,5,Prio),
%set_prio_inst([A,B,C],3,4,Prio),
@@ -4347,11 +4347,11 @@ same_sign_minus_interval(Val1,Val2,Val) :-
check_before_susp_div_mod(A,B,Q,BQ,R) :-
% on verifie si on a deja fini
+ check_div_int_ineqs(A,B,Q,BQ,R),
div_mod_inst(A,B,Q,BQ,R,Continue),
(var(Continue) ->
true
- ; check_div_int_ineqs(A,B,Q,BQ,R),
- ((get_bvbounds(A,_),
+ ; ((get_bvbounds(A,_),
% donc A pos
nonvar(B),
B >= 0)
diff --git a/Src/COLIBRI/arith_sched.pl b/Src/COLIBRI/arith_sched.pl
index 62fd483f8..b672c382d 100755
--- a/Src/COLIBRI/arith_sched.pl
+++ b/Src/COLIBRI/arith_sched.pl
@@ -149,7 +149,7 @@ set_touched_arg_from_goal(abs_val_int(A,B),_Var,S) :- !,
set_touched_arg_from_goal(geq(A,B),_Var,S) :- !,
(A == B ->
- kill_suspension(S)
+ change_prio_if_not_RC(S,2)
; ((nonvar(A);
nonvar(B))
->
@@ -163,32 +163,32 @@ set_touched_arg_from_goal(geq(A,B),_Var,S) :- !,
; true))).
set_touched_arg_from_goal(gt(A,B),_Var,S) :- !,
- % pour echouer plus vite
- A \== B,
- ((nonvar(A);
- nonvar(B))
- ->
+ (A == B ->
change_prio_if_not_RC(S,2)
- ; mfd:dvar_range(A,MinA,MaxA),
- mfd:dvar_range(B,MinB,MaxB),
- ((MinA =< MinB;
- MaxA =< MaxB)
+ ; ((nonvar(A);
+ nonvar(B))
->
- change_prio_if_not_RC(S,3)
- ; true)).
+ change_prio_if_not_RC(S,2)
+ ; mfd:dvar_range(A,MinA,MaxA),
+ mfd:dvar_range(B,MinB,MaxB),
+ ((MinA =< MinB;
+ MaxA =< MaxB)
+ ->
+ change_prio_if_not_RC(S,3)
+ ; true))).
set_touched_arg_from_goal(diff_int(A,B),_Var,S) :- !,
- % pour echouer plus vite
- A \== B,
- ((nonvar(A);
- nonvar(B))
- ->
+ (A == B ->
change_prio_if_not_RC(S,2)
- ; true).
+ ; ((nonvar(A);
+ nonvar(B))
+ ->
+ change_prio_if_not_RC(S,2)
+ ; true)).
set_touched_arg_from_goal(geq_real(_,A,B),_Var,S) :- !,
(A == B ->
- kill_suspension(S)
+ change_prio_if_not_RC(S,2)
; ((is_fzero(A);
is_fzero(B);
nonvar(A);
@@ -198,26 +198,26 @@ set_touched_arg_from_goal(geq_real(_,A,B),_Var,S) :- !,
; true)).
set_touched_arg_from_goal(gt_real(_,A,B),_Var,S) :- !,
- % pour echouer plus vite
- A \== B,
- ((is_fzero(A);
- is_fzero(B);
- nonvar(A);
- nonvar(B))
- ->
+ (A == B ->
change_prio_if_not_RC(S,2)
- ; true).
+ ; ((is_fzero(A);
+ is_fzero(B);
+ nonvar(A);
+ nonvar(B))
+ ->
+ change_prio_if_not_RC(S,2)
+ ; true)).
set_touched_arg_from_goal(diff_real(_,A,B),_Var,S) :- !,
- % pour echouer plus vite
- A \== B,
- ((is_fzero(A);
- is_fzero(B);
- nonvar(A);
- nonvar(B))
- ->
+ (A == B ->
change_prio_if_not_RC(S,2)
- ; true).
+ ; ((is_fzero(A);
+ is_fzero(B);
+ nonvar(A);
+ nonvar(B))
+ ->
+ change_prio_if_not_RC(S,2)
+ ; true)).
set_touched_arg_from_goal(_,_,_).
diff --git a/Src/COLIBRI/check_lin_expr.pl b/Src/COLIBRI/check_lin_expr.pl
index e2983a56d..6497dd8ba 100755
--- a/Src/COLIBRI/check_lin_expr.pl
+++ b/Src/COLIBRI/check_lin_expr.pl
@@ -105,7 +105,8 @@ try_check_exists_lin_expr_giving_diff_args(Type,A,B,Stop) :-
Stop = 1
; % real
((not_inf_bounds(Other), % prudence pour p(Inf) ou s(-Inf)
- is_float_number(Other))
+ is_float_number(Other),
+ not is_real_box(Other))
->
mreal:dvar_remove_element(Other,Val),
Stop = 1
@@ -208,7 +209,8 @@ eval_factor(Type,0_1*V,R) ?- !,
eval_factor(Type,N*V,R) :-
number(V),
!,
- R is rational(N)*rational(V).
+ %R is rational(N)*rational(V).
+ safe_mult_rat(N,V,R).
eval_factor(Type,N*V,R) :-
mult_rat_intervals(Type,N,V,R).
@@ -261,7 +263,8 @@ protected_rat_mult(A,B,C) :-
rational(A),
rational(B),
!,
- C is A*B.
+ %C is A*B.
+ safe_mult_rat(A,B,C).
protected_rat_mult(A,B,C) ?- !,
(abs(A) =:= 1.0Inf ->
(B > 0_1 ->
@@ -300,7 +303,8 @@ protected_rat_add(A,B,C) :-
rational(A),
rational(B),
!,
- C is A+B.
+ %C is A+B.
+ safe_add_rat(A,B,C).
protected_rat_add(A,B,C) :-
(abs(A) =:= 1.0Inf ->
C = A
@@ -334,7 +338,8 @@ insert_largs_in_lsum(Type,Coeff,[Args|LArgs],From,MaxDepth,Seen,C,NLSeen) :-
% les descendants d'une seule somme
insert_args_in_lsum(_,_,[],_,_,L,L).
insert_args_in_lsum(Type,Coeff,[CoeffV*V|Args],From,MaxDepth,LSeen,NLSeen) :-
- NC is Coeff*CoeffV,
+ %NC is Coeff*CoeffV,
+ safe_mult_rat(Coeff,CoeffV,NC),
get_lsum_giving(Type,NC*V,From,MaxDepth,LSeen,NLseen0),
insert_args_in_lsum(Type,Coeff,Args,From,MaxDepth,NLseen0,NLSeen).
@@ -342,11 +347,13 @@ insert_args_in_lsum(Type,Coeff,[CoeffV*V|Args],From,MaxDepth,LSeen,NLSeen) :-
get_lsum_giving(Type,NV*V,From,MaxDepth,LSeen,NLSeen) :-
(number(V) ->
% on modifie tous les C de LSeen
- NVxV is NV*rational(V),
+ %NVxV is NV*rational(V),
+ safe_mult_rat(NV,V,NVxV),
(foreach((Seen,C),LSeen),
foreach((Seen,NC),NLSeen),
param(NVxV) do
- NC is C + NVxV)
+ %NC is C + NVxV
+ safe_add_rat(C,NVxV,NC))
; get_lsum1_giving(Type,NV*V,From,MaxDepth,LSeen,NLSeen)).
get_lsum1_giving(Type,NV*V,From,MaxDepth,[],[]).
@@ -355,7 +362,8 @@ get_lsum1_giving(Type,NV*V,From,MaxDepth,[(Seen,C)|ELSeen],NLSeen) :-
member_begin_end(ONV*VV,Seen,NSeen,End,EndNSeen),
V == VV)
->
- NNV is ONV + NV,
+ %NNV is ONV + NV,
+ safe_add_rat(ONV,NV,NNV),
(NNV == 0_1 ->
% plus de V
End = EndNSeen
@@ -468,7 +476,8 @@ get_args_from_add_mult_giving(Type,LC,V,LArgs,ELArgs,NLC) :-
((Z == V,
number(Y),
rational(Y,RY),
- InvY is 1_1/RY,
+ %InvY is 1_1/RY,
+ safe_div_rat(1_1,RY,InvY),
Args = [InvY*X])
->
OLC = ILC,
@@ -502,14 +511,16 @@ get_args_from_other_add_op_mult(Type,LC,V,LArgs) :-
number(Y),
not_zero(Y),
rational(Y,RY),
- InvY is 1_1/RY,
+ %InvY is 1_1/RY,
+ safe_div_rat(1_1,RY,InvY),
OLArgs = [[InvY*Z]|ILArgs];
V == Y,
% Y = Z * 1/X
number(X),
not_zero(X),
rational(X,RX),
- InvX is 1_1/RX,
+ %InvX is 1_1/RX,
+ safe_div_rat(1_1,RX,InvX),
OLArgs = [[InvX*Z]|ILArgs]))
->
true
@@ -534,14 +545,16 @@ get_args_from_other_add_op_mult(Type,LC,V,LArgs) :-
not_zero(Y),
% X = Z * 1/Y
rational(Y,RY),
- InvY is 1_1/RY,
+ %InvY is 1_1/RY,
+ safe_div_rat(1_1,RY,InvY),
Args = [InvY*Z];
V == Y,
number(X),
not_zero(X),
% Y = Z * 1/X
rational(X,RX),
- InvX is 1_1/RX,
+ %InvX is 1_1/RX,
+ safe_div_rat(1_1,RX,InvX),
Args = [InvX*Z]))
->
OLArgs = [Args|ILArgs]
@@ -559,7 +572,8 @@ get_args_from_other_add_op_mult(Type,LC,V,LArgs) :-
V == Y,
% Y = X/Z
rational(Z,RZ),
- InvZ is 1_1/RZ,
+ %InvZ is 1_1/RZ,
+ safe_div_rat(1_1,RZ,InvZ),
Args = [InvZ*X]))
->
OLArgs = [Args|ILArgs]
diff --git a/Src/COLIBRI/col_solve.pl b/Src/COLIBRI/col_solve.pl
index c0ceace71..adbbfba84 100644
--- a/Src/COLIBRI/col_solve.pl
+++ b/Src/COLIBRI/col_solve.pl
@@ -617,7 +617,7 @@ smt_solve_bis0(Test,FILE,TO,Code) :-
getval(simplex_delay_deactivation,DDSteps)@eclipse,
smt_start_enable_delta_check(DDSteps),
((var(Test),
- (TO > 0;
+ (%TO > 0;
DDSteps == 0))
->
smt_disable_delta_check
@@ -798,9 +798,8 @@ smt_test_CI(TO,Size) :-
smt_test(TO,Size,CI) :-
%StrDir = "./colibri_tests/colibri/tests/",
- StrDir = "./colibri_tests/colibri/tests/sat/",
+ %StrDir = "./colibri_tests/colibri/tests/sat/",
% 0 (sans real/float->int!) 1 TO sur newton à 15s mais pas a 24s
-
%StrDir = "./colibri_tests/colibri/tests/unsat/", %0
%StrDir = "./colibri_tests/colibri/tests/unknown/",
%StrDir = "./colibri_tests/colibri/tests/timeout/",
@@ -938,7 +937,7 @@ smt_test(TO,Size,CI) :-
%-----------------------------------------------------------------------
%StrDir = "./QF_AUFBVFP/20210301-Alive2/",% 1
%-----------------------------------------------------------------------
- %StrDir = "QF_ABVFP/20170428-Liew-KLEE/imperial_svcomp_float-benchs_svcomp_mea8000.x86_64/", %0
+ StrDir = "QF_ABVFP/20170428-Liew-KLEE/imperial_svcomp_float-benchs_svcomp_mea8000.x86_64/", %0
%StrDir = "QF_ABVFP/20170428-Liew-KLEE/imperial_synthetic_non_terminating_klee_bug.x86_64/", % 0
%StrDir = "./QF_ABVFP/20170428-Liew-KLEE/aachen_real_gmp_gmp_klee_mul.x86_64/", % 3 (bitwuzla 0)
@@ -1030,8 +1029,11 @@ smt_test(TO,Size,CI) :-
%StrDir = "QF_NIA/",
%StrDir = "QF_NIA/20170427-VeryMax/", %Que des TO
- %StrDir = "QF_NIA/AProVE/", % 1475/2406 (3 I) 5 unknown
- %StrDir = "bugs_NIA/", % 6/6 unknown !!!
+ %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/LCTES/",% 2/2
@@ -1427,6 +1429,12 @@ smt_unit_test(TO,CI) :-
setval(cpt_solve,0)@colibri,
setval(use_delta,UD)@eclipse,
setval(use_simplex,US)@eclipse,
+ % On passe en mode comptage du nombre de steps
+ setval(step_stats,1)@eclipse,
+ setval(step_limit,0)@eclipse,
+ setval(nb_steps,0)@eclipse,
+ setval(simplex_steps,0)@eclipse,
+ setval(show_steps,1)@eclipse,
not not (seed(0),
smt_solve_bis(Test,F,TO,Code),
setval(init_code,Code)),
diff --git a/Src/COLIBRI/lp_arith.pl b/Src/COLIBRI/lp_arith.pl
index 55e6a38fa..0155b37ab 100755
--- a/Src/COLIBRI/lp_arith.pl
+++ b/Src/COLIBRI/lp_arith.pl
@@ -153,7 +153,8 @@ make_poly([(C,V)|L],P0,Rat0,P,Rat) :-
P1 = P0,
Rat1 = Rat0
; (number(V) ->
- Rat1 is Rat0 + rational(C)*rational(V),
+ %Rat1 is Rat0 + rational(C)*rational(V),
+ Rat1 is safe_add_rat(Rat0,safe_mult_rat(rational(C),rational(V))),
P1 = P0
; Rat1 = Rat0,
make_monome_arg(C,MC),
@@ -1096,9 +1097,11 @@ lin_add_int(A,B,C) :-
!,
((get_lin_cstrs(V,Cstrs),
member(add_int(X,Y,Z),Cstrs),
- match_inv_com_binop(A,B,C,X,Y,Z,U1,U2))
+ match_com_binop(A,B,C,X,Y,Z,U1,U2))
->
- protected_unify(U1 = U2)
+ % pas ici
+ % protected_unify(U1,U2)
+ true
; ls_setup,
ls_define(A),
ls_define(B),
@@ -1112,24 +1115,27 @@ lin_add_int(A,B,C) :-
add_lin_cstr(VV,add_int(A,B,C)))).
lin_add_int(A,B,C).
-match_inv_com_binop(A,B,C,A,Y,Z,U1,U2) ?- !,
- (B == Y ->
- (U1,U2) = (C,Z)
- ; C == Z,
- (U1,U2) = (B,Y)).
-match_inv_com_binop(A,B,C,X,A,Z,U1,U2) ?- !,
- (B == X ->
- (U1,U2) = (C,Z)
- ; C == Z,
- (U1,U2) = (B,X)).
-match_inv_com_binop(A,B,C,B,Y,Z,U1,U2) ?- !,
- % A <> Y
- C == Z,
- (U1,U2) = (A,Y).
-match_inv_com_binop(A,B,C,X,B,Z,U1,U2) ?-
- % A <> X
- C == Z,
- (U1,U2) = (A,X).
+match_inv_com_binop(A,B,C,X,Y,Z,U1,U2) :-
+ (A == X ->
+ (B == Y ->
+ % com
+ (U1,U2) = (C,Z)
+ ; % inv
+ C == Z,
+ (U1,U2) = (B,Y))
+ ; (A == Y ->
+ (B == X ->
+ % com
+ (U1,U2) = (C,Z)
+ ; % inv
+ C == Z,
+ (U1,U2) = (B,X))
+ ; % inv
+ C == Z,
+ (B == X ->
+ (U1,U2) = (A,Y)
+ ; B == Y,
+ (U1,U2) = (A,X)))).
match_com_binop(A,B,C,A,Y,Z,U1,U2) ?- !,
B == Y,
@@ -1150,11 +1156,11 @@ lin_add_real(Type,A,B,C) :-
!,
((get_lin_cstrs(V,Cstrs),
member(add_real(Type,X,Y,Z),Cstrs),
- (Type == real ->
- match_inv_com_binop(A,B,C,X,Y,Z,U1,U2)
- ; match_com_binop(A,B,C,X,Y,Z,U1,U2)))
+ match_com_binop(A,B,C,X,Y,Z,U1,U2))
->
- protected_unify(U1 = U2)
+ % pas ici
+ % protected_unify(U1,U2)
+ true
; ls_setup,
ls_define(A),
ls_define(B),
@@ -1180,12 +1186,11 @@ lin_minus_real(Type,A,B,C) :-
member(minus_real(Type,X,Y,Z),Cstrs),
((X,Y) == (A,B),
U1 = C,
- U2 = Z;
- Type == real,
- (X == A, C == Z, U1 = B, U2 = Y;
- Y == B, C == Z, U1 = A, U2 = X)))
+ U2 = Z))
->
- protected_unify(U1 = U2)
+ % pas ici
+ % protected_unify(U1,U2),
+ true
; ls_setup,
ls_define(A),
ls_define(B),
@@ -1216,7 +1221,9 @@ lin_op_int(A,B) :-
(B == X,(U1,U2) = (A,Y);
B == Y,(U1,U2) = (A,X))))
->
- protected_unify(U1 = U2)
+ % pas ici
+ % protected_unify(U1,U2)
+ true
; ls_setup,
ls_define(A),
ls_define(B),
@@ -1239,11 +1246,11 @@ lin_mult_int(A,B,C) :-
(Vars = [V,_|_] ->
((get_lin_cstrs(V,Cstrs),
member(mult_int(X,Y,Z),Cstrs),
- (not_unify(C,0) ->
- match_inv_com_binop(A,B,C,X,Y,Z,U1,U2)
- ; match_com_binop(A,B,C,X,Y,Z,U1,U2)))
+ match_com_binop(A,B,C,X,Y,Z,U1,U2))
->
- protected_unify(U1 = U2)
+ % pas ici
+ % protected_unify(U1,U2)
+ true
; ls_setup,
ls_define(A),
ls_define(B),
@@ -1270,13 +1277,11 @@ lin_mult_real(Type,A,B,C) :-
(Vars = [V,_|_] ->
((get_lin_cstrs(V,Cstrs),
member(mult_real(Type,X,Y,Z),Cstrs),
- ((Type == real,
- not_unify(C,0.0))
- ->
- match_inv_com_binop(A,B,C,X,Y,Z,U1,U2)
- ; match_com_binop(A,B,C,X,Y,Z,U1,U2)))
+ match_com_binop(A,B,C,X,Y,Z,U1,U2))
->
- protected_unify(U1 = U2)
+ % pas ici
+ % protected_unify(U1,U2)
+ true
; ls_setup,
ls_define(A),
ls_define(B),
@@ -1309,7 +1314,9 @@ lin_div_real(Type,A,B,C) :-
A == X,
B == Y)
->
- protected_unify(C = Z)
+ % pas ici
+ % protected_unify(C,Z)
+ true
; ls_setup,
ls_define(A),
ls_define(B),
@@ -1338,7 +1345,9 @@ lin_sqrt(A,B) :-
member(sqrt(AA,BB),Cstrs),
A == AA)
->
- protected_unify(B = BB)
+ % pas ici
+ % protected_unify(B,BB)
+ true
; ls_setup,
ls_define(A),
ls_define(B),
@@ -1383,7 +1392,9 @@ lin_abs_int(A,B) :-
member(abs_int(AA,BB),Cstrs),
A == AA)
->
- protected_unify(B = BB)
+ % pas ici
+ % protected_unify(B,BB)
+ true
; ls_setup,
ls_define(A),
ls_define(B),
@@ -1404,7 +1415,9 @@ lin_abs_real(A,B) :-
member(abs_real(AA,BB),Cstrs),
A == AA)
->
- protected_unify(B = BB)
+ % pas ici
+ % protected_unify(B,BB)
+ true
; ls_setup,
ls_define(A),
ls_define(B),
@@ -1564,8 +1577,10 @@ lin_min_max_real(A,B,Min,Max) :-
((A,B) == (X,Y);
(B,A) == (X,Y)))
->
- protected_unify(Min,CMin),
- protected_unify(Max,CMax)
+ % pas ici
+ % protected_unify(Min,CMin),
+ % protected_unify(Max,CMax)
+ true
; ls_setup,
ls_define(A),
ls_define(B),
@@ -1589,7 +1604,9 @@ lin_cast_float_to_double(F,D) ?-
member(cast_float_to_double(FF,DD),Cstrs),
F == FF)
->
- protected_unify(D = DD)
+ % pas ici
+ % protected_unify(D,DD)
+ true
; ls_setup,
ls_define(F),
ls_define(D),
@@ -1612,7 +1629,9 @@ lin_cast_int_real(Type,I,R) ?-
member(cast_int_real(Type,II,RR),Cstrs),
I == II)
->
- protected_unify(R = RR)
+ % pas ici
+ % protected_unify(R,RR)
+ true
; ls_setup,
ls_define(I),
ls_define(R),
@@ -1776,14 +1795,14 @@ insert_lin_cstr(square_int(X,XX)) ?- !,
rational(LX,RLX),
rational(HX,RHX),
% XX + LX*LX - 2*LX*X >= 0
- Op2LX is -2*RLX,
+ Op2LX is safe_mult_rat(-2_1,RLX),
make_poly([(1,XX),(LX,LX),(Op2LX,X)],P1,Int1),
assert_poly_geq_val(P1,Int1),
% XX + HX*HX - 2*HX*X >= 0
- Op2HX is -2*RHX,
+ Op2HX is safe_mult_rat(-2_1,RHX),
make_poly([(1,XX),(HX,HX),(Op2HX,X)],P2,Int2),
assert_poly_geq_val(P2,Int2),
- LXpHX is RLX+RHX,
+ LXpHX is safe_add_rat(RLX,RHX),
OpHX is -RHX,
% (LX+HX)*X - XX - HX*LX >= 0
make_poly([(LXpHX,X),(-1,XX),(OpHX,LX)],P3,Int3),
@@ -1907,8 +1926,10 @@ insert_lin_cstr(min_max_real(A,B,Min,Max)) ?- !,
->
protected_unify(ApB,A)
; new_ocaml_var(ApB),
- LS is rational(LA)+rational(LB),
- HS is rational(HA)+rational(HB),
+ %LS is rational(LA)+rational(LB),
+ LS is safe_add_rat(rational(LA),rational(LB)),
+ %HS is rational(HA)+rational(HB),
+ HS is safe_add_rat(rational(HA),rational(HB)),
set_lin_var_bounds(ApB,LS,HS),
set_lin_var_range(real,ApB,LS,HS))),
((var(A);
@@ -1928,20 +1949,25 @@ insert_lin_cstr(min_max_real(A,B,Min,Max)) ?- !,
->
insert_lin_cstr(add_int(Min,Max,ApB))
; % ApB deja calcule, Min et Max deja reduits
- S is rational(Min) + rational(Max),
+ %S is rational(Min) + rational(Max),
+ S is safe_add_rat(rational(Min),rational(Max)),
set_lin_var_bounds(ApB,S,S),
set_lin_var_range(real,ApB,S,S)))),
new_ocaml_var(DMin),
- LDMin is 2_1 * rational(LMin),
- HDMin is 2_1 * rational(HMin),
+ %LDMin is 2_1 * rational(LMin),
+ LDMin is safe_mult_rat(2_1,rational(LMin)),
+ %HDMin is 2_1 * rational(HMin),
+ HDMin is safe_mult_rat(2_1,rational(HMin)),
set_lin_var_bounds(DMin,LDMin,HDMin),
set_lin_var_range(real,DMin,LDMin,HDMin),
(var(Min) ->
insert_lin_cstr(mult_int(2,Min,DMin))
; true),
new_ocaml_var(DMax),
- LDMax is 2_1 * rational(LMax),
- HDMax is 2_1 * rational(HMax),
+ %LDMax is 2_1 * rational(LMax),
+ LDMax is safe_mult_rat(2_1,rational(LMax)),
+ %HDMax is 2_1 * rational(HMax),
+ HDMax is safe_mult_rat(2_1,rational(HMax)),
set_lin_var_bounds(DMax,LDMax,HDMax),
set_lin_var_range(real,DMax,LDMax,HDMax),
(var(Max) ->
@@ -1970,8 +1996,10 @@ insert_lin_cstr(add_real(Type,X,Y,XY)) ?- !,
insert_lin_cstr(add_int(X,Y,XY))
; dvar_range(Type,X,LIX,HIX),
dvar_range(Type,Y,LIY,HIY),
- Min is rational(LIX) + rational(LIY),
- Max is rational(HIX) + rational(HIY),
+ %Min is rational(LIX) + rational(LIY),
+ Min is safe_add_rat(rational(LIX),rational(LIY)),
+ %Max is rational(HIX) + rational(HIY),
+ Max is safe_add_rat(rational(HIX),rational(HIY)),
new_ocaml_var(RXY),
set_lin_var_bounds(RXY,Min,Max),
set_lin_var_range(Type,RXY,Min,Max),
@@ -1989,14 +2017,16 @@ insert_lin_cstr(minus_real(Type,X,Y,XY)) ?- !,
XY =:= 0.0)
->
add_lin_vars_eq(X,Y)
- %protected_unify(X,Y)
+ % protected_unify(X,Y)
; (Type == real ->
% idem entiers
insert_lin_cstr(add_int(XY,Y,X))
; dvar_range(Type,X,LIX,HIX),
dvar_range(Type,Y,LIY,HIY),
- Min is rational(LIX) - rational(HIY),
- Max is rational(HIX) - rational(LIY),
+ %Min is rational(LIX) - rational(HIY),
+ Min is safe_minus_rat(rational(LIX),rational(HIY)),
+ %Max is rational(HIX) - rational(LIY),
+ Max is safe_minus_rat(rational(HIX),rational(LIY)),
new_ocaml_var(RXY),
set_lin_var_bounds(RXY,Min,Max),
set_lin_var_range(Type,RXY,Min,Max),
@@ -2034,8 +2064,10 @@ insert_lin_cstr(mult_real(Type,X,Y,XY)) ?- !,
insert_lin_cstr(mult_int(Cst,V,XY))
; dvar_range(Type,V,MinV,MaxV),
RCst is rational(Cst),
- B1 is RCst*rational(MinV),
- B2 is RCst*rational(MaxV),
+ %B1 is RCst*rational(MinV),
+ B1 is safe_mult_rat(RCst,rational(MinV)),
+ %B2 is RCst*rational(MaxV),
+ B2 is safe_mult_rat(RCst,rational(MaxV)),
sort(0,=<,[B1,B2],[Min,Max]),
new_ocaml_var(RXY),
set_lin_var_bounds(RXY,Min,Max),
@@ -2050,10 +2082,14 @@ insert_lin_cstr(mult_real(Type,X,Y,XY)) ?- !,
; true)
; dvar_range(Type,X,MinX,MaxX),
dvar_range(Type,Y,MinY,MaxY),
- B1 is rational(MinX)*rational(MinY),
- B2 is rational(MinX)*rational(MaxY),
- B3 is rational(MaxX)*rational(MinY),
- B4 is rational(MaxX)*rational(MaxY),
+ %B1 is rational(MinX)*rational(MinY),
+ B1 is safe_mult_rat(rational(MinX),rational(MinY)),
+ %B2 is rational(MinX)*rational(MaxY),
+ B2 is safe_mult_rat(rational(MinX),rational(MaxY)),
+ %B3 is rational(MaxX)*rational(MinY),
+ B3 is safe_mult_rat(rational(MaxX),rational(MinY)),
+ %B4 is rational(MaxX)*rational(MaxY),
+ B4 is safe_mult_rat(rational(MaxX),rational(MaxY)),
sort(0,=<,[B1,B2,B3,B4],[Min,_,_,Max]),
new_ocaml_var(RXY),
set_lin_var_bounds(RXY,Min,Max),
@@ -2077,8 +2113,12 @@ insert_lin_cstr(square_real(X,XX)) ?- !,
HX >= 0)
->
LRXX = 0
- ; LRXX is rational(min(abs(LX),abs(HX)))^2),
- HRXX is rational(max(abs(LX),abs(HX)))^2,
+ ; %LRXX is rational(min(abs(LX),abs(HX)))^2,
+ RMin is rational(min(abs(LX),abs(HX))),
+ LRXX is safe_mult_rat(RMin,RMin)),
+ %HRXX is rational(max(abs(LX),abs(HX)))^2,
+ RMax is rational(max(abs(LX),abs(HX))),
+ HRXX is safe_mult_rat(RMax,RMax),
set_lin_var_bounds(RXX,LRXX,HRXX),
set_lin_var_range(Type,RXX,LRXX,HRXX),
% idem entiers
@@ -2101,15 +2141,18 @@ insert_lin_cstr(sqrt(XX,X)) ?- !,
ls_define(RX)),
dvar_range(Type,RX,LRX,HRX),
% (XX + LRX*LRX - 2.0*LRX*RX >= 0.0)
- Op2LRX is -2*rational(LRX),
+ %Op2LRX is -2*rational(LRX),
+ Op2LRX is safe_mult_rat(-2_1,rational(LRX)),
make_poly([(1,XX),(LRX,LRX),(Op2LRX,RX)],P1,Val1),
assert_poly_geq_val(P1,Val1),
% (XX + HRX*HRX - 2.0*HRX*RX >= 0.0)
- Op2HRX is -2*rational(HRX),
+ %Op2HRX is -2*rational(HRX),
+ Op2HRX is safe_mult_rat(-2_1,rational(HRX)),
make_poly([(1,XX),(HRX,HRX),(Op2HRX,RX)],P2,Val2),
assert_poly_geq_val(P2,Val2),
% ((LRX+HRX)*RX - XX - HRX*LRX >= 0.0)
- Sum is rational(LRX)+rational(HRX),
+ %Sum is rational(LRX)+rational(HRX),
+ Sum is safe_add_rat(rational(LRX),rational(HRX)),
OpHRX is -HRX,
make_poly([(Sum,RX),(-1,XX),(OpHRX,LRX)],P3,Val3),
assert_poly_geq_val(P3,Val3),
@@ -2137,8 +2180,10 @@ insert_lin_cstr(div_real(Type,X,Y,XdY)) ?- !,
new_ocaml_var(RXdY),
dvar_range(Type,X,LX,HX),
RY is rational(Y),
- B1 is rational(LX)/RY,
- B2 is rational(HX)/RY,
+ %B1 is rational(LX)/RY,
+ B1 is safe_div_rat(rational(LX),RY),
+ %B2 is rational(HX)/RY,
+ B2 is safe_div_rat(rational(HX),RY),
sort(0,=<,[B1,B2],[LRXdY,HRXdY]),
set_lin_var_bounds(RXdY,LRXdY,HRXdY),
set_lin_var_range(Type,RXdY,LRXdY,HRXdY),
@@ -2155,8 +2200,10 @@ insert_lin_cstr(div_real(Type,X,Y,XdY)) ?- !,
new_ocaml_var(RXdY),
dvar_range(Type,Y,LY,HY),
RX is rational(X),
- B1 is RX/rational(LY),
- B2 is RX/rational(HY),
+ %B1 is RX/rational(LY),
+ B1 is safe_div_rat(RX,rational(LY)),
+ %B2 is RX/rational(HY),
+ B2 is safe_div_rat(RX,rational(HY)),
sort(0,=<,[B1,B2],[LRXdY,HRXdY]),
set_lin_var_bounds(RXdY,LRXdY,HRXdY),
set_lin_var_range(Type,RXdY,LRXdY,HRXdY),
@@ -2172,10 +2219,14 @@ insert_lin_cstr(div_real(Type,X,Y,XdY)) ?- !,
RXdY = XdY,
dvar_range(Type,RXdY,LR,HR)
; set_lazy_domain(real,RXdY),
- B1 is rational(LX)/rational(LY),
- B2 is rational(LX)/rational(HY),
- B3 is rational(HX)/rational(LY),
- B4 is rational(HX)/rational(HY),
+ %B1 is rational(LX)/rational(LY),
+ B1 is safe_div_rat(rational(LX),rational(LY)),
+ %B2 is rational(LX)/rational(HY),
+ B2 is safe_div_rat(rational(LX),rational(HY)),
+ %B3 is rational(HX)/rational(LY),
+ B3 is safe_div_rat(rational(HX),rational(LY)),
+ %B4 is rational(HX)/rational(HY),
+ B4 is safe_div_rat(rational(HX),rational(HY)),
sort(0,=<,[B1,B2,B3,B4],[LR,_,_,HR]),
new_ocaml_var(RXdY),
set_lin_var_bounds(RXdY,LR,HR),
@@ -2274,7 +2325,8 @@ get_mid_rounded_to_Inf(Type,MPInf,Mid) :-
(Type == float_double ->
RInf is rational(2^1024)
; RInf is rational(2^128)),
- AbsRMid is RPInf + (RInf - RPInf)/2_1,
+ %AbsRMid is RPInf + (RInf - RPInf)/2_1,
+ AbsRMid is safe_add_rat(RPInf,safe_div_rat(safe_minus_rat(RInf,RPInf),2_1)),
new_ocaml_var(Mid),
get_lin_var_id(Mid,IMid),
(MPInf > 0.0 ->
@@ -2299,18 +2351,22 @@ lin_real_approx(Type,X,RX) :-
% ARX == RX
% RX * (1 - (2^(-P)/(1- 2^(-P)))) - MinF/2 =< X
% X =< RX * (1 + (2^(-P)/(1- 2^(-P)))) + MinF/2
- Coeff1 is 1_1 - Coeff,
+ %Coeff1 is 1_1 - Coeff,
+ Coeff1 is safe_minus_rat(1_1,Coeff),
make_poly([(Coeff1,RX),(-1,MinFd2),(-1,X)],P1,Val1),
- Coeff2 is 1_1 + Coeff,
+ %Coeff2 is 1_1 + Coeff,
+ Coeff2 is safe_add_rat(1_1,Coeff),
make_poly([(Coeff2,RX),(1,MinFd2),(-1,X)],P2,Val2)
; % L < 0
(H =< 0 ->
% ARX == -RX
% RX * (1 + (2^(-P)/(1- 2^(-P)))) - MinF/2 =< X
% X =< RX * (1 - (2^(-P)/(1- 2^(-P)))) + MinF/2
- Coeff1 is 1_1 + Coeff,
+ %Coeff1 is 1_1 + Coeff,
+ Coeff1 is safe_add_rat(1_1,Coeff),
make_poly([(Coeff1,RX),(-1,MinFd2),(-1,X)],P1,Val1),
- Coeff2 is 1_1 - Coeff,
+ %Coeff2 is 1_1 - Coeff,
+ Coeff2 is safe_minus_rat(1_1,Coeff),
make_poly([(Coeff2,RX),(1,MinFd2),(-1,X)],P2,Val2)
; abs(L,AL),
abs(H,AH),
diff --git a/Src/COLIBRI/realarith.pl b/Src/COLIBRI/realarith.pl
index 6c0d1175f..a0310370c 100644
--- a/Src/COLIBRI/realarith.pl
+++ b/Src/COLIBRI/realarith.pl
@@ -3337,12 +3337,15 @@ clear_Goals_add_real(Type,A,B,C) :-
(AA == A ->
BB == B
; AA == B,
- BB == A);
+ BB == A),
+ Kill == 1;
G = minus_real1(Type,AA,BB,CC),
AA == A,
- is_op_real(Type,BB,B)))
+ is_op_real(Type,B,BB)))
->
- kill_suspension(S),
+ (nonvar(Kill) ->
+ kill_suspension(S)
+ ; true),
protected_unify(C,CC)
; true).
clear_Goals_add_real0(real,A,B,C) ?- !,
@@ -3351,18 +3354,18 @@ clear_Goals_add_real0(real,A,B,C) ?- !,
clear_Goals_add_real0(_,A,B,C) :-
clear_Goal(add_real1,A,B,C).
-is_op_real(_,A,OpA) :-
- number(A),
- number(OpA),
+is_op_real(_,B,OpB) :-
+ number(B),
+ number(OpB),
!,
- OpA is -A.
-is_op_real(Type,A,OpA) :-
+ OpB is -B.
+is_op_real(Type,B,OpB) :-
get_saved_cstr_suspensions(LS),
member((_,op_real1(Type,X,Y)),LS),
- (A == X ->
- OpA == Y
- ; A == Y,
- OpA == X).
+ (B == X ->
+ OpB == Y
+ ; B == Y,
+ OpB == X).
check_2box(real,L) ?- !,
@@ -3512,10 +3515,11 @@ check_launch_add_int(Type,A,B,C,_,Continue) :-
is_float_int_number(A),
is_float_int_number(B),
is_float_int_number(C),
+/*
not_inf_bounds(A),
not_inf_bounds(B),
not_inf_bounds(C),
-
+*/
is_inside_mantissa(Type,A),
is_inside_mantissa(Type,B),
is_inside_mantissa(Type,C))
@@ -3870,12 +3874,14 @@ add_real_inst0(real,A,B,C,Continue) :- !,
Stop = 1,
protected_unify(B,C)
; (check_rbox_rat(B,RatB) ->
- RatC is RatA + RatB,
- launch_box_rat(C,RatC),
+ %RatC is RatA + RatB,
+ %launch_box_rat(C,RatC),
+ check_add_rat(RatA,RatB,C),
BoxGoal = add_real1(real,A,B,C)
; (check_rbox_rat(C,RatC) ->
- RatB is RatC - RatA,
- launch_box_rat(B,RatB),
+ %RatB is RatC - RatA,
+ %launch_box_rat(B,RatB),
+ check_minus_rat(RatC,RatA,B),
BoxGoal = minus_real1(real,C,A,B)
; true)))
; (check_rbox_rat(B,RatB) ->
@@ -3883,8 +3889,9 @@ add_real_inst0(real,A,B,C,Continue) :- !,
Stop = 1,
protected_unify(A,C)
; (check_rbox_rat(C,RatC) ->
- RatA is RatC - RatB,
- launch_box_rat(A,RatA),
+ %RatA is RatC - RatB,
+ %launch_box_rat(A,RatA),
+ check_minus_rat(RatC,RatB,A),
BoxGoal = minus_real1(real,C,B,A)
; true))
; (C == 0.0 ->
@@ -3895,7 +3902,9 @@ add_real_inst0(real,A,B,C,Continue) :- !,
true
; (nonvar(BoxGoal) ->
% memorisation/factorisation du calcul de boites
- check_rbox_cstrs(3,BoxGoal)
+ check_rbox_cstrs(3,BoxGoal),
+ % parano
+ check_add_rat(A,B,C)
; Continue = 1)).
% Mode double/simple nearest
@@ -3968,6 +3977,98 @@ add_real_inst0(Type,A,B,C,Continue) :-
reduce_add_args_from_Inf_res(Type,A,B,C)
; true)))))).
+check_add_rat(A,B,C) :-
+ safe_add_rat(A,B,RatC),
+ (check_rbox_rat(C,ORatC) ->
+ ORatC == RatC
+ ; launch_box_rat(C,RatC)).
+safe_add_rat(A0,B0,RatC) :-
+ (var(A0) ->
+ A = A0
+ ; A is A0),
+ (var(B0) ->
+ B = B0
+ ; B is B0),
+ check_rbox_rat(A,RatA),
+ check_rbox_rat(B,RatB),
+ make_OCamlRat(RatA,RA),
+ make_OCamlRat(RatB,RB),
+ add_rat(RA,RB,RC),
+ simplex_ocaml_rat_num(RC,SCNum),
+ simplex_ocaml_rat_den(RC,SCDen),
+ concat_string([SCNum,"_",SCDen],SRatC),
+ number_string(RatC,SRatC).
+
+check_minus_rat(A,B,C) :-
+ safe_minus_rat(A,B,RatC),
+ (check_rbox_rat(C,ORatC) ->
+ ORatC == RatC
+ ; launch_box_rat(C,RatC)).
+safe_minus_rat(A0,B0,RatC) :-
+ (var(A0) ->
+ A = A0
+ ; A is A0),
+ (var(B0) ->
+ B = B0
+ ; B is B0),
+ check_rbox_rat(A,RatA),
+ check_rbox_rat(B,RatB),
+ OpRatB is -RatB,
+ make_OCamlRat(RatA,RA),
+ make_OCamlRat(OpRatB,OpRB),
+ add_rat(RA,OpRB,RC),
+ simplex_ocaml_rat_num(RC,SCNum),
+ simplex_ocaml_rat_den(RC,SCDen),
+ concat_string([SCNum,"_",SCDen],SRatC),
+ number_string(RatC,SRatC).
+
+check_op_rat(A,OpA) :-
+ check_minus_rat(0.0,A,OpA).
+
+check_mult_rat(A,B,C) :-
+ safe_mult_rat(A,B,RatC),
+ (check_rbox_rat(C,ORatC) ->
+ ORatC == RatC
+ ; launch_box_rat(C,RatC)).
+safe_mult_rat(A0,B0,RatC) :-
+ (var(A0) ->
+ A = A0
+ ; A is A0),
+ (var(B0) ->
+ B = B0
+ ; B is B0),
+ check_rbox_rat(A,RatA),
+ check_rbox_rat(B,RatB),
+ make_OCamlRat(RatA,RA),
+ make_OCamlRat(RatB,RB),
+ mult_rat(RA,RB,RC),
+ simplex_ocaml_rat_num(RC,SCNum),
+ simplex_ocaml_rat_den(RC,SCDen),
+ concat_string([SCNum,"_",SCDen],SRatC),
+ number_string(RatC,SRatC).
+
+check_div_rat(A,B,C) :-
+ safe_div_rat(A,B,RatC),
+ (check_rbox_rat(C,ORatC) ->
+ ORatC == RatC
+ ; launch_box_rat(C,RatC)).
+safe_div_rat(A0,B0,RatC) :-
+ (var(A0) ->
+ A = A0
+ ; A is A0),
+ (var(B0) ->
+ B = B0
+ ; B is B0),
+ check_rbox_rat(A,RatA),
+ check_rbox_rat(B,RatB),
+ make_OCamlRat(RatA,RA),
+ make_OCamlRat(RatB,RB),
+ div_rat(RA,RB,RC),
+ simplex_ocaml_rat_num(RC,SCNum),
+ simplex_ocaml_rat_den(RC,SCDen),
+ concat_string([SCNum,"_",SCDen],SRatC),
+ number_string(RatC,SRatC).
+
set_interval_box(Var,Min,Max) :-
interval_from_bounds(Min,Max,Inter),
(float(Inter) ->
@@ -4038,11 +4139,13 @@ make_box_rat(square_real1,A,C) ?- !,
make_box_rat(_,_,_).
check_rbox_rat(A,Rat) :-
- (float(A) ->
- abs(A,AbsA),
- AbsA =\= 1.0Inf,
- Rat is rational(A)
- ; is_real_box_rat(A,Rat)).
+ (rational(A) ->
+ Rat = A
+ ; (number(A) ->
+ abs(A,AbsA),
+ AbsA =\= 1.0Inf,
+ Rat is rational(A)
+ ; is_real_box_rat(A,Rat))).
rat_of_decimal_string(Str0,Rat) :-
(append_strings("-",Str1,Str0) ->
@@ -6941,7 +7044,7 @@ check_exists_cast_int_real(Type,A,B) :-
% B = real(A) et B = real(C) ==> A = C
% int(real(X)) = X:
% B = real(A) et C = int(B) ==> C = int(real(A)) et C = A
- ((var(B),
+ ((fail,var(B),
once (Type == real;
safe_integer_to_real(Type,A)),% un entier representable
get_saved_cstr_suspensions(LSusp1),
@@ -7711,57 +7814,57 @@ inv_real_to_int(Type,FI,I,R) :-
%% MODIF BM
%% la bijection n'est vraie qu'en "real" ou sous 2^53(double)/2^24(simple)
check_exists_cast_real_int(Type,A,B,Kill) :-
- %% B = int(A)
- var(A),
- get_saved_cstr_suspensions(LSusp),
- LSusp = [_|_],
- !,
- %% F(X) = Y et F(X) = Z ==> Y = Z:
- %% C = int(A) ==> B = C
- %% En real ou dans -2^53+1..2^53-1, real/int est bijectif
- %% PMO NB : a partir de 2^53 on peut absorber 1 comme 2^53+1 qui sera
- %% "remplace" par 2^53 donc a partir de 2^53 on perd la bijection
- %% int(real(X)) = X:
- %% A = real(C) ==> B = int(real(C)) et B = C
- ((Type == real;
- mreal:dvar_range(A,MinA,MaxA),
- min_max_integral_bounds(Type,MinRep,MaxRep),
- MinA > MinRep,
- MaxA < MaxRep)
- ->
- Bij = 1
- ; true),
- ((member((Susp,G),LSusp),
- (% F(X) = Y et F(X) = Z ==> Y = Z
- G = cast_real_int1(Type,V1,V2),
- A == V1, V = V2, AB = B;
- (nonvar(Bij),
- (G = cast_int_real1(Type,V1,V2),
- A == V2, V = V1, AB = B, Kill = 1; %% A = real(V1) donc V1 = B
- (G = cast_real_int(Type,V1,V2);
- G = cast_real_int1(Type,V1,V2)),
- B == V2, %% B = int(V1),integral(V1),integral(A)
- is_float_int_number(A),%% donc V1 = A
- is_float_int_number(V1),
- V = V1, AB = A))))
- ->
- %% Le cast_int_real1 est plus contraignant,
- %% on le laisse travailler
- (var(Kill) ->
- kill_suspension(Susp)
- ; true),
- protected_unify(AB = V)
- ; true).
+ % B = int(A)
+ var(A),
+ get_saved_cstr_suspensions(LSusp),
+ LSusp = [_|_],
+ !,
+ % F(X) = Y et F(X) = Z ==> Y = Z:
+ % C = int(A) ==> B = C
+ % En real ou dans -2^53+1..2^53-1, real/int est bijectif
+ % PMO NB : a partir de 2^53 on peut absorber 1 comme 2^53+1 qui sera
+ % "remplace" par 2^53 donc a partir de 2^53 on perd la bijection
+ % int(real(X)) = X:
+ % A = real(C) ==> B = int(real(C)) et B = C
+ ((Type == real;
+ mreal:dvar_range(A,MinA,MaxA),
+ min_max_integral_bounds(Type,MinRep,MaxRep),
+ MinA > MinRep,
+ MaxA < MaxRep)
+ ->
+ Bij = 1
+ ; true),
+ ((member((Susp,G),LSusp),
+ (% F(X) = Y et F(X) = Z ==> Y = Z
+ G = cast_real_int1(Type,V1,V2),
+ A == V1, V = V2, AB = B;
+ (fail,nonvar(Bij),
+ (G = cast_int_real1(Type,V1,V2),
+ A == V2, V = V1, AB = B, Kill = 1; %A = real(V1) donc V1 = B
+ (G = cast_real_int(Type,V1,V2);
+ G = cast_real_int1(Type,V1,V2)),
+ B == V2, % B = int(V1),integral(V1),integral(A)
+ is_float_int_number(A),% donc V1 = A
+ is_float_int_number(V1),
+ V = V1, AB = A))))
+ ->
+ % Le cast_int_real1 est plus contraignant,
+ % on le laisse travailler
+ (var(Kill) ->
+ kill_suspension(Susp)
+ ; true),
+ protected_unify(AB = V)
+ ; true).
check_exists_cast_real_int(_,A,B,Kill).
%% Utilise en evaluation
cast_real_int_interval(A,B) :-
- getval(float_eval,Type)@eclipse,
- cast_real_int_interval_type(Type,A,B).
+ getval(float_eval,Type)@eclipse,
+ cast_real_int_interval_type(Type,A,B).
cast_real_int_interval_type(real,A,B) ?- !,
- cast_real_int_interval(real,A,B).
+ cast_real_int_interval(real,A,B).
cast_real_int_interval_type(Type,A,B) :-
((check_not_NaN(A),
not_inf_bounds(A))
@@ -8031,17 +8134,23 @@ op_real_inst(real,A,B,Continue) :- !,
; A0 is - B),
protected_unify(A,A0)
; (check_rbox_rat(A,RatA) ->
- RatB is -RatA,
- launch_box_rat(B,RatB),
+ %RatB is -RatA,
+ %launch_box_rat(B,RatB),
+ check_op_rat(A,B),
BoxGoal = op_real1(real,A,B)
; (check_rbox_rat(B,RatB) ->
- RatA is -RatB,
- launch_box_rat(A,RatA),
+ %RatA is -RatB,
+ %launch_box_rat(A,RatA),
+ check_op_rat(B,A),
BoxGoal = op_real1(real,B,A)
; same_box_float_number_status(A,B,Box),
Continue = 1)),
(var(Continue) ->
- check_rbox_cstrs(2,BoxGoal)
+ check_rbox_cstrs(2,BoxGoal),
+ (nonvar(BoxGoal) ->
+ % parano
+ check_op_rat(A,B)
+ ; true)
; true))).
op_real_inst(_,A,B,Continue) :-
(number(A) ->
@@ -8081,12 +8190,22 @@ same_box_float_number_status(A,B,Box) :-
check_exists_op_real(Type,A,B) :-
((get_saved_cstr_suspensions(LSusp),
member((Susp,op_real1(Type,V1,V2)),LSusp),
- ((AorB=A,U1=B); (AorB=B,U1=A)),
- ((AorB == V1, U2 = V2)
- ;(AorB == V2, U2 = V1)))
+ (A == V1 ->
+ U1 = B,
+ U2 = V2
+ ; (A == V2 ->
+ U1 = B,
+ U2 = V1
+ ; (B == V2 ->
+ U1 = A,
+ U2 = V1
+ ; B == V1,
+ U1 = A,
+ U2 = V2))))
->
+ % bug incomprehensible sur NIA/aprove
kill_suspension(Susp),
- protected_unify(U1 = U2)
+ protected_unify(U1,U2)
; true).
@@ -8168,22 +8287,16 @@ check_launch_op_int(Type,A,B,Continue,_) :-
var(Continue),
!.
check_launch_op_int(Type,A,B,_,Continue) :-
- ((Type == real,
+ ((fail,Type == real,
term_variables((A,B),[_,_]),
is_float_int_number(A),
is_float_int_number(B),
+/*
not_inf_bounds(A),
not_inf_bounds(B),
-
+*/
is_inside_mantissa(Type,A),
is_inside_mantissa(Type,B))
-/*
- mreal:dvar_range(A,MinA,MaxA),
- get_mantissa_size(Type,MSize),
- MaxRep is 2.0^(MSize+1),
- MinA >= -MaxRep,%% -2^53 en double
- MaxA =< MaxRep)
-*/
->
cast_real_int(Type,A,IA),
op(IA,IB),
@@ -8206,14 +8319,6 @@ minus_real_type(Type,A,B,C) :-
minus_real(Type,A,B,C)
; fp_sub(rne,as(A,Type),as(B,Type)) $= as(C,Type)).
-/*
-minus_real(Type,A,B,C) :-
- Type \== real,
- !,
- op_real(Type,B,OpB),
- fp_eq(Type,OpB,OpBB),
- add_real(Type,A,OpBB,C).
-*/
minus_real(Type,A,B,C) :-
((Type == real,
var(A),
@@ -8457,10 +8562,11 @@ check_launch_minus_int(Type,A,B,C,_,Continue) :-
is_float_int_number(A),
is_float_int_number(B),
is_float_int_number(C),
+/*
not_inf_bounds(A),
not_inf_bounds(B),
not_inf_bounds(C),
-
+*/
is_inside_mantissa(Type,A),
is_inside_mantissa(Type,B),
is_inside_mantissa(Type,C))
@@ -9092,15 +9198,17 @@ minus_real_inst0(real,A,B,C,Continue) :- !,
; (C == 0.0 ->
protected_unify(A,B),
Stop = 1
- ; RatC is RatA - RatB,
- launch_box_rat(C,RatC),
+ ; %RatC is RatA - RatB,
+ %launch_box_rat(C,RatC),
+ check_minus_rat(RatA,RatB,C),
BoxGoal = minus_real1(real,A,B,C)))
; (check_rbox_rat(C,RatC) ->
(C == 0.0 ->
protected_unify(A,B),
Stop = 1
- ; RatB is RatA - RatC,
- launch_box_rat(B,RatB),
+ ; %RatB is RatA - RatC,
+ %launch_box_rat(B,RatB),
+ check_minus_rat(RatA,RatC,B),
BoxGoal = minus_real1(real,A,C,B))
; true)))
; (C == 0.0 ->
@@ -9112,15 +9220,18 @@ minus_real_inst0(real,A,B,C,Continue) :- !,
Stop = 1
; (check_rbox_rat(C,RatC) ->
% C <> 0
- RatA is RatC + RatB,
- launch_box_rat(A,RatA),
+ %RatA is RatC + RatB,
+ %launch_box_rat(A,RatA),
+ check_add_rat(RatC,RatB,A),
BoxGoal = add_real1(real,C,B,A)
; true))
; true))),
(nonvar(Stop) ->
true
; (nonvar(BoxGoal) ->
- check_rbox_cstrs(3,BoxGoal)
+ check_rbox_cstrs(3,BoxGoal),
+ % parano
+ check_minus_rat(A,B,C)
; Continue = 1)).
%% Mode simple double
@@ -9958,10 +10069,11 @@ check_launch_mult_int(Type,A,B,C,_,Continue) :-
is_float_int_number(A),
is_float_int_number(B),
is_float_int_number(C),
+/*
not_inf_bounds(A),
not_inf_bounds(B),
not_inf_bounds(C),
-
+*/
is_inside_mantissa(Type,A),
is_inside_mantissa(Type,B),
is_inside_mantissa(Type,C))
@@ -10416,11 +10528,7 @@ launch_mult_div_real_ineqs(Type,Exact,Susp,AA,BB,SBB,X,Z,C) :-
(var(Exact) ->
weak_rel(Rel1,NRel)
; NRel = Rel1),
- launch_real_ineq(NRel,Type,AA,Z),
- (NRel == = ->
- % donc AllExact et inversible, Susp inutile
- true %kill_suspension(Susp)
- ; true)
+ launch_real_ineq(NRel,Type,AA,Z)
; true),
get_rel_between_real_args(AA,Z,RelAZ),
((RelAZ \== ?,
@@ -11079,26 +11187,31 @@ mult_float_nearest(_,A,B,C) :-
mult_real_two_floats(A,B,C,Continue) :-
(check_rbox_rat(A,RatA) ->
(check_rbox_rat(B,RatB) ->
- RatC is RatA * RatB,
- launch_box_rat(C,RatC),
+ %RatC is RatA * RatB,
+ %launch_box_rat(C,RatC),
+ check_mult_rat(RatA,RatB,C),
BoxGoal = mult_real1(real,A,B,C)
; (check_rbox_rat(C,RatC) ->
% A <> 0.0
- RatB is RatC/RatA,
- launch_box_rat(B,RatB),
+ %RatB is RatC/RatA,
+ %launch_box_rat(B,RatB),
+ check_div_rat(RatC,RatA,B),
BoxGoal = div_real1(real,C,A,B)
; true))
; ((check_rbox_rat(B,RatB),
check_rbox_rat(C,RatC))
->
% B <> 0.0
- RatA is RatC/RatB,
- launch_box_rat(A,RatA),
+ %RatA is RatC/RatB,
+ %launch_box_rat(A,RatA),
+ check_div_rat(RatC,RatB,A),
BoxGoal = div_real1(real,C,B,A)
; true)),
(var(BoxGoal) ->
Continue = 1
- ; check_rbox_cstrs(3,BoxGoal)).
+ ; check_rbox_cstrs(3,BoxGoal),
+ % parano
+ check_mult_rat(A,B,C)).
%% Point fixe
mult_real_rec(Type,A,B,C) :-
@@ -13346,8 +13459,8 @@ clear_Goals_div_real(Type,A,B,C) :-
BB == B,
not_zero(C),
not_inf_bounds(C),
- U1 == AA,
- U2 == A)))
+ U1 = AA,
+ U2 = A)))
->
kill_suspension(S),
@@ -14190,25 +14303,30 @@ div_real_inst0(real,A,B,C,Continue) :- !,
true
; (check_rbox_rat(A,RatA) ->
(check_rbox_rat(B,RatB) ->
- RatC is RatA/RatB,
- launch_box_rat(C,RatC),
+ %RatC is RatA/RatB,
+ %launch_box_rat(C,RatC),
+ check_div_rat(RatA,RatB,C),
BoxGoal = div_real1(real,A,B,C)
; (check_rbox_rat(C,RatC) ->
% A / B = C -> A = B * C -> B = A / C
- RatB is RatA / RatC,
- launch_box_rat(B,RatB),
+ %RatB is RatA / RatC,
+ %launch_box_rat(B,RatB),
+ check_div_rat(RatA,RatC,B),
BoxGoal = div_real1(real,A,C,B)
; true))
; ((check_rbox_rat(B,RatB),
check_rbox_rat(C,RatC))
->
- RatA is RatB * RatC,
- launch_box_rat(A,RatA),
+ %RatA is RatB * RatC,
+ %launch_box_rat(A,RatA),
+ check_mult_rat(RatB,RatC,A),
BoxGoal = mult_real1(real,B,C,A)
; true)),
(var(BoxGoal) ->
Continue = 1
- ; check_rbox_cstrs(3,BoxGoal))).
+ ; check_rbox_cstrs(3,BoxGoal),
+ % parano
+ check_div_rat(A,B,C))).
div_real_inst0(Type,A,B,C,Continue) :-
% float/double
(B == 1.0 ->
@@ -17521,7 +17639,7 @@ check_exists_sqrt_real(real,A,B) ?- !,
U2 = Y,
Call = kill_suspension(Susp)
; A == Y,
- Call = (kill_suspension(Susp),abs_val_real(real,X,B)))))
+ Call = (my_suspension(Susp),abs_val_real(real,X,B)))))
->
protected_unify(U1,U2),
call(Call)
@@ -19980,12 +20098,15 @@ analyze_gt_real_ineq(Type,A,B,gt_real(Type,X,Y),S,Stop) ?-
; Stop = 1).
analyze_gt_real_ineq(Type,A,B,gt_real_reif(Type,X,Y,Bool),S,_Stop) ?-
kill_suspension(S),
- (A == X ->
- % B == Y,
- protected_unify(Bool,1)
- ; % A == Y,
- % B == X,
- protected_unify(Bool,0)).
+ ((A == X ->
+ B == Y,
+ VBool = 1
+ ; A == Y,
+ B == X,
+ VBool = 0)
+ ->
+ protected_unify(Bool,VBool)
+ ; true).
analyze_gt_real_ineq(Type,A,B,geq_real(Type,X,Y),S,Stop) ?-
A == X,
B == Y,
@@ -20004,8 +20125,9 @@ analyze_geq_real_ineq(Type,A,B,gt_real(Type,X,Y),S,Stop) ?-
check_gt_real(Type,A,B)
; true).
analyze_geq_real_ineq(Type,A,B,gt_real_reif(Type,X,Y,Bool),S,Stop) ?-
- (A == X ->
- % B == Y
+ ((A == X,
+ B == Y)
+ ->
(Bool == 0 ->
Stop = 1,
kill_suspension(S),
diff --git a/Src/COLIBRI/smt_import.pl b/Src/COLIBRI/smt_import.pl
index 4aa3320d4..1cbeef534 100644
--- a/Src/COLIBRI/smt_import.pl
+++ b/Src/COLIBRI/smt_import.pl
@@ -728,7 +728,7 @@ get_assignment :-
no_simplex,
((once (getval(diag_code,(_,1))@eclipse;
getval(unknown_quantifier_abstraction,1)@eclipse),
- getval(binding,HNV)@eclipse,
+ getval(binding,HNV),
HNV \== 0)
->
hash_list(HNV,Ks,Vs),
@@ -738,7 +738,8 @@ get_assignment :-
((Type \= sort(_),
Type \= array(_,_),
(var(V),VV = V;
- remove_upper_as(V,VV,_),var(VV)))
+ remove_upper_as(V,VV,_),var(VV)),
+ not is_real_box(VV))
->
functor(Type,FType,_),
(occurs(FType,(bool,int,uint)) ->
@@ -948,15 +949,29 @@ dump_type_val('Bool',Val0,Val) ?- !,
(Val0 == 1 ->
Val = "true"
; Val = "false").
+dump_type_val(int,Val0,Val) ?- !,
+ dump_type_val('Int',Val0,Val).
+dump_type_val(real_int,Val0,Val) ?- !,
+ (var(Val0) ->
+ (is_real_box_rat(Val0,Rat) ->
+ numerator(Rat,Val1),
+ dump_type_val('Int',Val1,Val)
+ ; dump_type_val('Real',Val0,Val))
+ ; dump_type_val('Int',Val0,Val)).
dump_type_val('Int',Val0,Val) ?- !,
(float(Val0) ->
% simulation real/int
- integer(Val0,Val1),
- number_string(Val1,Val)
- ; number_string(Val0,Val)).
-dump_type_val('Real',Val0,Val) ?- !,
+ integer(Val0,Val1)
+ ; Val1 = Val0),
+ (Val1 < 0 ->
+ Op is -Val1,
+ concat_string(["(- ",Op,")"],Val)
+ ; number_string(Val1,Val)).
+dump_type_val(real,Val0,Val) ?- !,
+ dump_type_val('Real',Val0,Val).
+dump_type_val('Real',Val0,NVal) ?- !,
(var(Val0) ->
- (known_real_box(Val0,SNum,SDen) ->
+ (known_real_box(Val0,SNum,SDenN,Neg) ->
(SDen == "1" ->
concat_string([SNum,".0"],Val)
; concat_string(["(/ ",SNum,".0 ",SDen,".0)"],Val))
@@ -975,11 +990,18 @@ dump_type_val('Real',Val0,Val) ?- !,
; concat_string(["(/ ",NumH,".0 ",DenH,".0)"],SH)),
concat_string(["(range ",SL," ",SH,")"], Val))
; rational(Val0,Val1),
- protected_numerator(Val1,Num),
- protected_denominator(Val1,Den),
+ (Val1 < 0_1 ->
+ Neg = 1,
+ Val2 is -Val1
+ ; Val2 = Val1),
+ protected_numerator(Val2,Num),
+ protected_denominator(Val2,Den),
(Den == 1 ->
concat_string([Num,".0"],Val)
- ; concat_string(["(/ ",Num,".0 ",Den,".0)"],Val))).
+ ; concat_string(["(/ ",Num,".0 ",Den,".0)"],Val))),
+ (nonvar(Neg) ->
+ concat_string(["(- ",Val,")"],NVal)
+ ; NVal = Val).
dump_type_val('RoundingMode',Val0,Val) ?- !,
((nonvar(Val0),
member((Val0,Val),
@@ -1222,8 +1244,12 @@ dump_smt_uninterps([(Ins,Out)|Profiles],InSorts,OutSort,SUninterp) :-
; concat_string(["(ite ",SAE," ",SOut," ",NSUninterp,")"],SUninterp))).
-known_real_box(Box,SNum,SDen) :-
- is_real_box_rat(Box,Rat),
+known_real_box(Box,SNum,SDen,Neg) :-
+ is_real_box_rat(Box,Rat0),
+ (Rat0 < 0_1 ->
+ Neg = 1,
+ Rat is -Rat0
+ ; Rat = Rat0),
term_string(Rat,SRat),
split_string(SRat,"_","",[SNum,SDen]).
diff --git a/Src/COLIBRI/solve.pl b/Src/COLIBRI/solve.pl
index c2fd32831..e13311ab2 100644
--- a/Src/COLIBRI/solve.pl
+++ b/Src/COLIBRI/solve.pl
@@ -219,7 +219,9 @@ array_def(Var,Def) :-
get_variable_type(V,Type),
unfold_int_expr_block(Def,0,C,Type,V),
call(C)
- ; '#='(Var,Def)).
+ ; (getval(check_sat_vars,1)@eclipse ->
+ true
+ ; '#='(Var,Def))).
array_elt_def(E,A,I) :-
unfold_int_expr(A,0,_true,array(_TI,TE),IA),
(real_type(TE,_) ->
@@ -2212,7 +2214,10 @@ unfold_int_expr(alldiff(Type,L),D,Cstr,Bool,R) :-
ND is D + 1,
Bool = bool,
!,
- (real_type(Type,IType) ->
+ ((nonvar(Type),
+ real_type(Type,IType))
+ ->
+ % ????
Real = 1
; true),
((IType == real,
@@ -2226,10 +2231,14 @@ unfold_int_expr(alldiff(Type,L),D,Cstr,Bool,R) :-
; (foreach(E,L),
foreach(RE,NL),
fromto(true,I,O,CL),
- param(Type,Real,ND,R) do
+ param(Type,IType,Real,ND,R) do
(var(Real) ->
unfold_int_expr(E,ND,CE,Type,RE)
- ; unfold_real_expr(E,ND,CE,Type,RE)),
+ ; % pas de NaN ici
+ (IType == real ->
+ ensure_not_NaN(RE) %????
+ ; true),
+ unfold_real_expr(E,ND,CE,Type,RE)),
insert_dep_inst(dep(RE,ND,[R])),
make_conj(I,CE,O)),
int_vars(bool,R),
@@ -2447,6 +2456,9 @@ unfold_int_expr(EA $= EB,D,Cstr,Type0,R) ?-
nonvar(RType),
real_type(RType,Type),
!,
+ (Type == real ->
+ ensure_not_NaN((A,B))
+ ; true),
int_vars(bool,R),
insert_dep_inst(dep(R,D,[A,B])),
(var(R) ->
@@ -2548,6 +2560,9 @@ unfold_int_expr(EA $\= EB,D,Cstr,Type0,R) ?- !,
nonvar(RType),
real_type(RType,Type),
!,
+ (Type == real ->
+ ensure_not_NaN((A,B))
+ ; true),
int_vars(bool,R),
insert_dep_inst(dep(R,D,[A,B])),
(var(R) ->
@@ -2594,14 +2609,14 @@ unfold_int_expr(EA $\= EB,D,Cstr,Type0,R) ?- !,
unfold_int_expr(EA $< EB,D,Cstr,Type0,R) ?-
Type0 = bool,
ND is D + 1,
- (R == 1 ->
- ensure_not_NaN((A,B))
- ; true),
unfold_real_expr(EA,ND,CA,RType,A),
unfold_real_expr(EB,ND,CB,RType,B),
nonvar(RType),
real_type(RType,Type),
!,
+ (Type == real ->
+ ensure_not_NaN((A,B))
+ ; true),
make_conj(CA,CB,CAB),
int_vars(bool,R),
insert_dep_inst(dep(R,D,[A,B])),
@@ -2629,11 +2644,11 @@ unfold_int_expr(EA $< EB,D,Cstr,Type0,R) ?-
Inter = [Min..PB],
Goal = in_intervals_reif(Type,A,Inter,R)
; Goal = gt_real_reif(Type,B,A,R))),
- make_conj(CAB,(ensure_not_NaN((A,B)),Goal),Cstr)
+ make_conj(CAB,Goal,Cstr)
; (R == 1 ->
- make_conj(CAB,(ensure_not_NaN((A,B)),launch_gt_real(Type,B,A)),Cstr)
+ make_conj(CAB,launch_gt_real(Type,B,A),Cstr)
; % R == 0
- make_conj(CAB,(ensure_not_NaN((A,B)),launch_geq_real(Type,A,B)),Cstr))).
+ make_conj(CAB,launch_geq_real(Type,A,B),Cstr))).
unfold_int_expr(fp_lt(EA,EB),D,Cstr,Type0,R) ?-
ND is D + 1,
Type0 = bool,
@@ -2681,14 +2696,14 @@ unfold_int_expr(fp_lt(EA,EB),D,Cstr,Type0,R) ?-
unfold_int_expr(EA $=< EB,D,Cstr,Type0,R) ?-
Type0 = bool,
ND is D + 1,
- (R == 1 ->
- ensure_not_NaN((A,B))
- ; true),
unfold_real_expr(EA,ND,CA,RType,A),
unfold_real_expr(EB,ND,CB,RType,B),
nonvar(RType),
real_type(RType,Type),
!,
+ (Type == real ->
+ ensure_not_NaN((A,B))
+ ; true),
make_conj(CA,CB,CAB),
int_vars(bool,R),
insert_dep_inst(dep(R,D,[A,B])),
@@ -2723,11 +2738,11 @@ unfold_int_expr(EA $=< EB,D,Cstr,Type0,R) ?-
Inter = [Min..NC],
Goal = in_intervals_reif(Type,A,Inter,R)
; Goal = geq_real_reif(Type,B,A,R))),
- make_conj(CAB,(ensure_not_NaN((A,B)),Goal),Cstr)
+ make_conj(CAB,Goal,Cstr)
; (R == 1 ->
- make_conj(CAB,(ensure_not_NaN((A,B)),launch_geq_real(Type,B,A)),Cstr)
+ make_conj(CAB,launch_geq_real(Type,B,A),Cstr)
; % R == 0
- make_conj(CAB,(ensure_not_NaN((A,B)),launch_gt_real(Type,A,B)),Cstr))).
+ make_conj(CAB,launch_gt_real(Type,A,B),Cstr))).
unfold_int_expr(fp_leq(EA,EB),D,Cstr,Type0,R) ?-
ND is D + 1,
Type0 = bool,
@@ -6687,6 +6702,7 @@ unfold_real_expr(EA + EB,D,Cstr,Type,R) ?-
make_conj(CA,PC,CAB)))
->
%call(spy_here)@eclipse,
+ % X + -Op = R, pattern frequent dans QF_NIA
make_conj(CAB,minus_real(real,X,Op,R),Cstr),
insert_dep_inst(dep(R,D,[X,Op]))
; insert_dep_inst(dep(R,D,[A,B])),
@@ -6757,33 +6773,11 @@ unfold_real_expr(EA - EB,D,Cstr,Type,R) ?-
unfold_real_expr(EA,ND,CA,Type,A),
unfold_real_expr(EB,ND,CB,Type,B),
!,
- ((fail,nonvar(Type),
- real_type(Type,real),
- ((CA = (PC,op_real(_,Op,_));
- CA = op_real(_,Op,_),
- PC = true),
- X = B,
- make_conj(PC,CB,CAB),
- % -Op - X -> -(X + Op)
- Goal = (add_real(real,X,Op,XpOp),op_real(real,XpOp,R)),
- insert_dep_inst(XpOp,D,[X,Op]),
- insert_dep_inst(R,D,[XpOp]);
- (CB = (PC,op_real(_,Op,_));
- CB = op_real(_,Op,_),
- PC = true),
- X = A,
- make_conj(CA,PC,CAB),
- % X - (-Op) -> X + Op
- Goal = add_real(real,X,Op,R),
- insert_dep_inst(R,D,[X,Op])))
- ->
- %call(spy_here)@eclipse,
- make_conj(CAB,Goal,Cstr)
- ; insert_dep_inst(dep(R,D,[A,B])),
- make_conj(CA,CB,CAB),
- (real_type(Type,real) ->
- make_conj(CAB,minus_real(real,A,B,R),Cstr)
- ; make_conj(CAB,(ensure_not_NaN((A,B,R)),minus_real(Type,A,B,R)),Cstr)))).
+ insert_dep_inst(dep(R,D,[A,B])),
+ make_conj(CA,CB,CAB),
+ (real_type(Type,real) ->
+ make_conj(CAB,minus_real(real,A,B,R),Cstr)
+ ; make_conj(CAB,(ensure_not_NaN((A,B,R)),minus_real(Type,A,B,R)),Cstr))).
unfold_real_expr(fp_sub(EA,EB),D,Cstr,Type,R) ?-
!,
unfold_real_expr(fp_sub(rne,EA,EB),D,Cstr,Type,R).
@@ -6849,20 +6843,14 @@ unfold_real_expr(EA * EB,D,Cstr,Type,R) ?-
make_conj(CA,CB,CAB),
((nonvar(Type),
real_type(Type,real),
- (occurs(A,(-1.0,0.0,1.0)),
+ (A == -1.0,
Cst = A, X = B;
- occurs(B,(-1.0,0.0,1.0)),
+ B == -1.0,
Cst = B, X = A))
->
%call(spy_here)@eclipse,
- (Cst == 0.0 ->
- Cstr = CAB,
- blocked_unify(R,0.0)
- ; (Cst == 1.0 ->
- Cstr = CAB,
- blocked_unify(R,X)
- ; % -1
- make_conj(CAB,op_real(real,X,R),Cstr)))
+ % X * -1 = R, pattern frequent dans QF_NIA
+ make_conj(CAB,op_real(real,X,R),Cstr)
; insert_dep_inst(dep(R,D,[A,B])),
(real_type(Type,real) ->
make_conj(CAB,mult_real(real,A,B,R),Cstr)
@@ -7283,6 +7271,7 @@ unfold_real_expr(fp_sqrt(EA),D,Cstr,Type,R) ?-
!,
unfold_real_expr(fp_sqrt(rne,EA),D,Cstr,Type,R).
unfold_real_expr(fp_sqrt(Rnd0,EA),D,Cstr,Type,R) ?-
+ call(spy_here)@eclipse,
ND is D + 1,
unfold_int_expr(Rnd0,ND,CRnd,rnd,Rnd),
rnd_vars(Rnd),
@@ -9658,21 +9647,6 @@ uninterp_trigger(F,Types0,Type0,Trigger) :-
uninterp(F,Trigger,TypeArgs,TypeR,Args,R) :-
get_priority(P),
set_priority(1),
-/*
- %save_cstr_suspensions((Args,R)),
- %get_saved_cstr_suspensions(LSusp0),
- % on a peut etre un uninterp clos contradictoire
- attached_suspensions(Trigger,LSusp1),
- append(LSusp0,LSusp1,LSusp),
- (foreach(PairOrSusp,LSusp),
- param(F,Trigger,Args,R,TypeArgs,TypeR) do
- (PairOrSusp = (Susp,Goal) ->
- true
- ; Susp = PairOrSusp,
- (get_suspension_data(Susp,goal,Goal) ->
- true
- ; Goal = dead)),
-*/
attached_suspensions(Trigger,LSusp),
(foreach(Susp,LSusp),
param(F,Trigger,Args,R,TypeArgs,TypeR) do
diff --git a/Src/COLIBRI/util.pl b/Src/COLIBRI/util.pl
index 133241fdb..01f6d3558 100755
--- a/Src/COLIBRI/util.pl
+++ b/Src/COLIBRI/util.pl
@@ -492,6 +492,11 @@ unify_pairs([V1,V2|L]) :-
protected_unify(V1,V2),
unify_pairs(L).
+% por le debug
+my_kill_suspension(_) :- !.
+my_kill_suspension(S) :-
+ kill_suspension(S).
+
collect_UVars_in_matching_Goal_suspensions([],_,_,_,_,[],[]).
collect_UVars_in_matching_Goal_suspensions([(Susp,Goal)|LSusp],Name,Val1,Val2,Val,UVars,NLSusp) :-
((make_matching_goal(Name,Goal,V1,V2,V3,Kind),
@@ -500,12 +505,12 @@ collect_UVars_in_matching_Goal_suspensions([(Susp,Goal)|LSusp],Name,Val1,Val2,Va
% On essaye le match de minus(Val1,Val2,Val3)
match_minus(Name,Val1,Val2,Val,V1,V2,V3,U1,U2);
match_op_from_add(Name,Val1,Val2,Val,V1,V2,V3,U1,U2,MatchOp)))
- ->
+ ->
kill_suspension(Susp),
(var(MatchOp) ->
UVars = [U1,U2|UVars1]
; UVars = UVars1,
- % On lancera un op_int/real apres
+ % On sature un op_int/real apres
get_priority(P),
NP is min(12,P+1),
(Name == add_int ->
@@ -514,7 +519,7 @@ collect_UVars_in_matching_Goal_suspensions([(Susp,Goal)|LSusp],Name,Val1,Val2,Va
((var(U1),
get_type(U1,Type);
var(U2),
- get_type(U1,Type))
+ get_type(U2,Type))
->
call_priority(op_real(Type,U1,U2),NP)
; call_priority(op_real(U1,U2),NP)))),
@@ -572,20 +577,20 @@ not_null(_,V) :-
%% ou un minus(Val2,Val1,Val) <=> add(Val1,Val,Val2)
%% alors Val1 = 0 et Val = Val2
match_minus(add_int,Val1,Val2,Val,V1,V2,V3,U1,U2) :-
- (Val == V1 ->
- ((Val2,Val1) == (V2,V3) ->
- U1 = Val2,
- U2 = 0
- ; (Val1,Val2) == (V2,V3),
- U1 = Val1,
- U2 = 0)
- ; Val == V2,
- ((Val2,Val1) == (V1,V3) ->
- U1 = Val2,
- U2 = 0
- ; (Val1,Val2) == (V1,V3),
- U1 = Val1,
- U2 = 0)).
+ (Val == V1 ->
+ ((Val2,Val1) == (V2,V3) ->
+ U1 = Val2,
+ U2 = 0
+ ; (Val1,Val2) == (V2,V3),
+ U1 = Val1,
+ U2 = 0)
+ ; Val == V2,
+ ((Val2,Val1) == (V1,V3) ->
+ U1 = Val2,
+ U2 = 0
+ ; (Val1,Val2) == (V1,V3),
+ U1 = Val1,
+ U2 = 0)).
%% add(N,Val2,Val),add(OpN,Val,V3) --> V3=Val2
%% add(N,Val2,Val),add(OpN,V2,Val2) --> Val=V2
@@ -597,30 +602,30 @@ match_minus(add_int,Val1,Val2,Val,V1,V2,V3,U1,U2) :-
%% add(Val1,N,Val),add(Val,OpN,V3) --> V3=Val1
%% add(Val1,N,Val),add(V1,OpN,Val1) --> Val=V1
match_add_with_op_number(add_int,Val1,Val2,Val,V1,V2,V3,U1,U2) :-
- (integer(Val1) ->
- Op is -Val1,
- (Op == V1 ->
- (Val == V2 ->
- (U1,U2) = (V3,Val2)
- ; Val2 == V3,
- (U1,U2) = (Val,V2))
- ; Op == V2,
- (Val == V1 ->
- (U1,U2) = (V3,Val2)
- ; Val2 == V3,
- (U1,U2) = (Val,V1)))
- ; integer(Val2),
- Op is -Val2,
- (Op == V1 ->
- (Val == V2 ->
- (U1,U2) = (V3,Val1)
- ; Val1 == V3,
- (U1,U2) = (Val,V2))
- ; Op == V2,
- (Val == V1 ->
- (U1,U2) = (V3,Val1)
- ; Val1 == V3,
- (U1,U2) = (Val,V1)))).
+ (integer(Val1) ->
+ Op is -Val1,
+ (Op == V1 ->
+ (Val == V2 ->
+ (U1,U2) = (V3,Val2)
+ ; Val2 == V3,
+ (U1,U2) = (Val,V2))
+ ; Op == V2,
+ (Val == V1 ->
+ (U1,U2) = (V3,Val2)
+ ; Val2 == V3,
+ (U1,U2) = (Val,V1)))
+ ; integer(Val2),
+ Op is -Val2,
+ (Op == V1 ->
+ (Val == V2 ->
+ (U1,U2) = (V3,Val1)
+ ; Val1 == V3,
+ (U1,U2) = (Val,V2))
+ ; Op == V2,
+ (Val == V1 ->
+ (U1,U2) = (V3,Val1)
+ ; Val1 == V3,
+ (U1,U2) = (Val,V1)))).
%% si add(A,B,C),add(C,D,A) --> op(B,D)
@@ -628,44 +633,46 @@ match_add_with_op_number(add_int,Val1,Val2,Val,V1,V2,V3,U1,U2) :-
%% si add(B,A,C),add(C,D,A) --> op(B,D)
%% si add(B,A,C),add(D,C,A) --> op(B,D)
match_op_from_add(add_int,Val1,Val2,Val,V1,V2,V3,Arg,OpArg,1) :-
- (Val1 == V3 ->
- (Val == V1 ->
- %% si add(A,B,C) et add(C,D,A) --> op(B,D)
- Arg = Val2,
- OpArg = V2
- ; Val == V2,
- %% si add(A,B,C) et add(D,C,A) --> op(B,D)
- Arg = Val2,
- OpArg = V1)
- ; Val2 == V3,
- (Val == V1 ->
- %% si add(B,A,C) et add(C,D,A) --> op(B,D)
- Arg = Val1,
- OpArg = V2
- ; Val == V2,
- %% si add(B,A,C) et add(D,C,A) --> op(B,D)
- Arg = Val1,
- OpArg = V1)).
+ (Val1 == V3 ->
+ (Val == V1 ->
+ % si add(A,B,C) et add(C,D,A) --> op(B,D)
+ Arg = Val2,
+ OpArg = V2
+ ; Val == V2,
+ % si add(A,B,C) et add(D,C,A) --> op(B,D)
+ Arg = Val2,
+ OpArg = V1)
+ ; Val2 == V3,
+ (Val == V1 ->
+ % si add(B,A,C) et add(C,D,A) --> op(B,D)
+ Arg = Val1,
+ OpArg = V2
+ ; Val == V2,
+ % si add(B,A,C) et add(D,C,A) --> op(B,D)
+ Arg = Val1,
+ OpArg = V1)).
+
match_op_from_add(add_real1,Val1,Val2,Val,V1,V2,V3,Arg,OpArg,1) :-
- get_type_from_real_vars((Val1,Val2,Val),real),
- (Val1 == V3 ->
- (Val == V1 ->
- %% si add(A,B,C) et add(C,D,A) --> op(B,D)
- Arg = Val2,
- OpArg = V2
- ; Val == V2,
- %% si add(A,B,C) et add(D,C,A) --> op(B,D)
- Arg = Val2,
- OpArg = V1)
- ; Val2 == V3,
- (Val == V1 ->
- %% si add(B,A,C) et add(C,D,A) --> op(B,D)
- Arg = Val1,
- OpArg = V2
- ; Val == V2,
- %% si add(B,A,C) et add(D,C,A) --> op(B,D)
- Arg = Val1,
- OpArg = V1)).
+ get_type_from_real_vars((Val1,Val2,Val),real),
+ (Val1 == V3 ->
+ (Val == V1 ->
+ % si add(A,B,C) et add(C,D,A) --> op(B,D)
+ Arg = Val2,
+ OpArg = V2
+ ; Val == V2,
+ % si add(A,B,C) et add(D,C,A) --> op(B,D)
+ Arg = Val2,
+ OpArg = V1)
+ ; Val2 == V3,
+ (Val == V1 ->
+ % si add(B,A,C) et add(C,D,A) --> op(B,D)
+ Arg = Val1,
+ OpArg = V2
+ ; Val == V2,
+ % si add(B,A,C) et add(D,C,A) --> op(B,D)
+ Arg = Val1,
+ OpArg = V1)).
+
%% Commutatif et inversible
match_bin_op(all,A,B,C,V1,V2,V3,U1,U2) :-
--
GitLab