diff --git a/Src/COLIBRI/check_lin_expr.pl b/Src/COLIBRI/check_lin_expr.pl
index 6197d3892fa71e6b8ca3fab7eeb9c51a6901250e..b51c5c62ccb66a97e2833f53b82df2e6f4cea308 100755
--- a/Src/COLIBRI/check_lin_expr.pl
+++ b/Src/COLIBRI/check_lin_expr.pl
@@ -71,6 +71,7 @@ try_check_exists_lin_expr_giving_diff_args(Type,A,B,Stop) :-
init_vardef,
+ %((var(A),var(B)) -> call(spy_here)@eclipse ; true),
setval(get_args_from_other,0),
((number(A),
@@ -116,30 +117,21 @@ try_check_exists_lin_expr_giving_diff_args(Type,A,B,Stop) :-
% qui peuvent etre utilises pour reduire A et B
(reduce_var_from_rat_interval(Type,A,R1) -> true;call(spy_here)@eclipse),
(reduce_var_from_rat_interval(Type,B,R2) -> true;call(spy_here)@eclipse),
- ((is_real_box_rat(A,RA),
- is_real_box_rat(B,RB))
+ ((number(A),Val = A,Other = B;
+ number(B),Val = B,Other = A)
->
- RA \== RB,
- Stop = 1
- ; ((number(A),
- Val = A,
- Other = B;
- number(B),
- Val = B,
- Other = A)
- ->
- (Type == int ->
- mfd:dvar_remove_element(Other,Val),
+ (Type == int ->
+ mfd:dvar_remove_element(Other,Val),
+ Stop = 1
+ ; % real
+ ((not_inf_bounds(Other), % prudence pour p(Inf) ou s(-Inf)
+ is_float_number(Other),
+ not is_real_box(Other))
+ ->
+ mreal:dvar_remove_element(Other,Val),
Stop = 1
- ; % real
- ((not_inf_bounds(Other), % prudence pour p(Inf) ou s(-Inf)
- is_float_number(Other),
- not is_real_box(Other))
- ->
- mreal:dvar_remove_element(Other,Val),
- Stop = 1
- ; true))
- ; true)).
+ ; true))
+ ; true).
%% Repérer (x+y)^2 et (x-y)^2 exhiber des carrés forcant le signe
protected_find_square_ids(L,R) :-
diff --git a/Src/COLIBRI/col_solve.pl b/Src/COLIBRI/col_solve.pl
index f9f6e9fd365e2b7f869a30c8a25395cb50ba2dbe..2cf9d66f177eeb115c28d4ef23e34ab6018cc96e 100644
--- a/Src/COLIBRI/col_solve.pl
+++ b/Src/COLIBRI/col_solve.pl
@@ -613,11 +613,10 @@ smt_solve_bis0(Test,FILE,Code) :-
; true),
Code = 3,
setval(diag_code,(timeout,3))
- ; (TagRead == syntax ->
+ ; (Tag == syntax ->
concat_string(["(error \"",FILE,":",TagRead,"\")"],Mess),
writeln(output,Mess),
- Code = 2,
- setval(diag_code,(unknown,2))
+ Code = 2
; % debug
(Test == 1 -> halt;true),
writeln(output,unknown),
@@ -755,10 +754,7 @@ clean_and_save_goal_before_check_sat(Goal,NewGoal) :-
conj_to_list(Goal,LGoal),
goals_before_check_sat(LGoal,NLGoal0,LEndNewGoal),
get_type_decl_list(NLGoal0,LDecl,NLGoal1),
- (occurs(get_model,LEndNewGoal) ->
- NLDecl = LDecl,
- CleanLGoal = NLGoal1
- ; remove_unused_decl_goal(LDecl,NLDecl,NLGoal1,LEndNewGoal,CleanLGoal)),
+ remove_unused_decl_goal(LDecl,NLDecl,NLGoal1,CleanLGoal),
keep_ground_goals(CleanLGoal,NLGoal2,_GCG,_EGCG),
% BUG copy_term trop gros
@@ -803,11 +799,10 @@ list_to_conj([A,B|L],(A,CBL)) :- !,
list_to_conj([A],A) :- !.
list_to_conj([],true).
-remove_unused_decl_goal([],[],LG,_,LG).
-remove_unused_decl_goal([D|LD],NLD,LG,LEndNewGoal,NLG) ?- !,
+remove_unused_decl_goal([],[],LG,LG).
+remove_unused_decl_goal([D|LD],NLD,LG,NLG) ?- !,
((is_decl(D),
term_variables(D,[V]),
- not occurs(V,LEndNewGoal),
member_begin_end(G,LG,NewLG,ELG,ELG),
once member(G,[A $= B,
A #= B,
@@ -821,9 +816,9 @@ remove_unused_decl_goal([D|LD],NLD,LG,LEndNewGoal,NLG) ?- !,
->
% D inutile
% call(spy_here)@eclipse,
- remove_unused_decl_goal(LD,NLD,NewLG,LEndNewGoal,NLG)
+ remove_unused_decl_goal(LD,NLD,NewLG,NLG)
; NLD = [D|ENLD],
- remove_unused_decl_goal(LD,ENLD,LG,LEndNewGoal,NLG)).
+ remove_unused_decl_goal(LD,ENLD,LG,NLG)).
:- export my_term_variables/2.
my_term_variables(Term,Vars) :-
@@ -1949,7 +1944,6 @@ check_unit_tests(SatUnsat,TO,Mod) :-
check_unit_tests(SatUnsat,TO) :-
Sat = [
- "./UnitTests/sat/BV/",
"./UnitTests/sat/FP/",
"./UnitTests/sat/BVFP/",
"./UnitTests/sat/FPLRA/",
@@ -1985,7 +1979,6 @@ check_unit_tests(SatUnsat,TO) :-
Unsat =
[
"./UnitTests/unsat/FP/",
- "./UnitTests/unsat/BV/",
"./UnitTests/unsat/BVFPLRA/",
"./UnitTests/unsat/ALL/",
"./UnitTests/unsat/FP/",
diff --git a/Src/COLIBRI/lin.pl b/Src/COLIBRI/lin.pl
index 88ce686a8b01d55fc858755edd7aee5bda16a707..0bbffdf2f99dbdc0d6dd526e7f962402db4e2ade 100644
--- a/Src/COLIBRI/lin.pl
+++ b/Src/COLIBRI/lin.pl
@@ -60,8 +60,7 @@ unify_lin_lin(Y, (_,CCX,LX,HX,InfosX), (IdY,CCY,LY,HY,InfosY)) ?-
CCX = CCY,
((LX,HX,InfosX) == (LY,HY,InfosY) ->
true
- ; append(InfosX,InfosY,Infos),
- sort(0,<,Infos,NInfos),
+ ; merge(0, <, InfosX, InfosY, NInfos),
% garder les pires bornes pour Y
NLY is min(LX,LY),
NHY is max(HX,HY),
@@ -93,7 +92,7 @@ set_lin_var_bounds(V{(Id,CC,_,_,Infos)},L,H) ?-
:- export add_lin_cstr/2.
add_lin_cstr(V{(Id,CC,L,H,Infos)},Cstr) ?- !,
- sort(0,<,[Cstr|Infos],NInfos),
+ merge(0,<,[Cstr],Infos,NInfos),
replace_attribute(V,(Id,CC,L,H,NInfos),lin).
add_lin_cstr(_,_).
diff --git a/Src/COLIBRI/lp_arith.pl b/Src/COLIBRI/lp_arith.pl
index b16ee55b1baeb014c945bf6b9956c3bd324229e9..1ddd447a9d48b117745dc4fdbfe0c47abf803a93 100755
--- a/Src/COLIBRI/lp_arith.pl
+++ b/Src/COLIBRI/lp_arith.pl
@@ -1447,7 +1447,8 @@ lin_abs_int(A,B) :-
add_lin_cstr(B,abs_int(A,B)),
remind_lin_cstr(abs_int(A,B))).
lin_abs_int(A,B).
-
+
+%%%% CJ: never used ??
%lin_abs_real(A,B) :- !.
lin_abs_real(A,B) :-
getval(use_delta,1)@eclipse,
@@ -1856,23 +1857,6 @@ insert_lin_cstr(square_int(X,XX)) ?- !,
make_poly([(LXpHX,X),(-1,XX),(OpHX,LX)],P3,Int3),
assert_poly_geq_val(P3,Int3).
-/*
-si A non signe les propagateurs garantissent:
-MaxB = min(op(MinA0),MaxA0)
-MinB = 0
-MinA = max(op(MaxB0),MinA0)
-MaxA = min(MaxB0,MaxA)
- (Ap >= 0),
- (An >= 0),
- (Ap =< MaxB),
- (An =< MaxB),
- (Ap - An =:= A)
- (Ap + An =:= B)
- (Ap =< MaxB * Bool),
- (NegBool + Bool = 1),
- (An =< MaxB * NegBool)
- NegBool * Bool = 0
-*/
insert_lin_cstr(abs_int(A,B)) ?- !,
mfd:dvar_range(A,MinA,MaxA),
(MaxA =< 0 ->
diff --git a/Src/COLIBRI/ndelta.pl b/Src/COLIBRI/ndelta.pl
index a49fe0db683d29e3fc1a29a74e3dc167b68d443a..61e6c1cf6432dec73fa86a3963b16338cc5d6743 100755
--- a/Src/COLIBRI/ndelta.pl
+++ b/Src/COLIBRI/ndelta.pl
@@ -1444,13 +1444,11 @@ deltas_inter_diff(OMin..OMax,=,C,=,C,1) :- !,
C \== 0.
deltas_inter_diff(OMin..OMax,_PlusDiff,Min..Max,NS,NC,Check) :-
NMin0 is protected_rat_max(OMin,Min),
- (fail,NMin0 =:= 0 ->
- % seulement pour int et real_int
+ (NMin0 =:= 0 ->
NMin = 1
; NMin = NMin0),
NMax0 is protected_rat_min(OMax,Max),
- (fail,NMax0 =:= 0 ->
- % seulement pour int et real_int
+ (NMax0 =:= 0 ->
NMax = -1
; NMax = NMax0),
% On peut echouer ici
@@ -1465,7 +1463,7 @@ deltas_inter_diff(OMin..OMax,_PlusDiff,Min..Max,NS,NC,Check) :-
NS = '=',
NC = NMin
; NC = NMin..NMax,
- ((NMin > 0;
+ ((NMin > 0;
NMax < 0)
->
NS = '+'
diff --git a/Src/COLIBRI/realarith.pl b/Src/COLIBRI/realarith.pl
index 55c97e8ab8b50438667d9f93d81cd12c76c8d708..3dae31c41abe98e0933c23863ee25fde19574a38 100644
--- a/Src/COLIBRI/realarith.pl
+++ b/Src/COLIBRI/realarith.pl
@@ -761,7 +761,7 @@ min_inv_round_rna_val(Type,B,A) :-
(B == -0.0 ->
get_next_float(Type,-0.5,A)
; A = 0.0)
- ; check_minus_rat(B,0.5,A0),
+ ; safe_minus_rat(B,0.5,A0),
(A0 == 0.0 ->
(get_sign(B,neg) ->
A = -0.0
@@ -1227,23 +1227,19 @@ ceiling_bis(Type,A,B) :-
true
; (nonvar(A) ->
get_next_float_int(Type,A,B)
- ; (is_real_box_rat(A,RA) ->
- ceiling(RA,CRA),
- numerator(CRA,IC),
- cast_int_real(Type,IC,B)
- ; (nonvar(B) ->
- (abs(B) =:= 1.0Inf ->
- % real impossible
- Type \== real,
- protected_unify(A,B)
- ; get_previous_float_int(Type,B,LA0),
- (Type == real ->
- mreal:set_typed_intervals(A,Type,[LA0..B]),
- Continue = 1
- % A peut devenir un float_int
- ; get_next_float(Type,LA0,LA),
- mreal:set_typed_intervals(A,Type,[LA..B])))
- ; Continue = 1))))),
+ ; (nonvar(B) ->
+ (abs(B) =:= 1.0Inf ->
+ % real impossible
+ Type \== real,
+ protected_unify(A,B)
+ ; get_previous_float_int(Type,B,LA0),
+ (Type == real ->
+ mreal:set_typed_intervals(A,Type,[LA0..B]),
+ Continue = 1
+ % A peut devenir un float_int
+ ; get_next_float(Type,LA0,LA),
+ mreal:set_typed_intervals(A,Type,[LA..B])))
+ ; Continue = 1)))),
(var(Continue) ->
true
; save_cstr_suspensions([A]),
@@ -3268,8 +3264,8 @@ add_real1(Type,A,B,C) :-
set_priority(Prio),
wake_if_other_scheduled(Prio).
-%check_real_add_opp(_,A,B,C,1) :- !.
-check_real_add_opp(real,A,B,C,Continue) ?-
+check_real_add_opp(_,A,B,C,1) :- !.
+check_real_add_opp(real,A,B,C,Continue) :-
nonvar(C),
C \== 0.0,
var(A),
@@ -3279,8 +3275,8 @@ check_real_add_opp(real,A,B,C,Continue) ?-
get_saved_cstr_suspensions(LS),
((member((_,op_real1(real,X,OpX)),LS),
(X == A ->
- % -X + B = C -> C + X = B
- Goal = add_real_bis(real,OpX,C,B)
+ % -X + B = C -> X - C = B
+ Goal = minus_real_bis(real,OpX,C,B)
; (X == B ->
% A + -X = C -> X + C = A
Goal = add_real_bis(real,OpX,C,A)
@@ -3291,9 +3287,9 @@ check_real_add_opp(real,A,B,C,Continue) ?-
% A + OpX = C -> A = X + C
Goal = add_real_bis(real,X,C,A)))))
->
- call(spy_here)@eclipse,
- call_priority(Goal,2)
- %Continue = 1
+ %call(spy_here)@eclipse,
+ call_priority(Goal,2),
+ Continue = 1
; Continue = 1).
check_real_add_opp(_,A,B,C,1).
@@ -4640,16 +4636,12 @@ is_fzero_interval([I]) ?-
get_rel_between_real_args(A,A,RelAB) ?- !,
RelAB = '='.
get_rel_between_real_args(A,B,RelAB) :-
- (((is_fzero(A),
- ZA = 1,
- get_type(B,Type);
- is_fzero(B),
- get_type(A,Type)),
- Type \== real)
+ ((is_fzero(A),ZA = 1;
+ is_fzero(B))
->
(nonvar(ZA) ->
(is_fzero(B) ->
- % on ne peut pas dire = ici
+ % on ne peut pas dire = ici
RelAB = ?
; mreal:dvar_range(B,MinB,MaxB),
(MinB >= 0.0 ->
@@ -7093,10 +7085,18 @@ cast_int_real(Rnd,Type,A,B) :-
% initialisation de A si necessaire/possible
(get_type(A,_) ->
dvar_range(int,A,LA,HA),
- make_OCamlRat(LA,LRA),
- float_of_OCamlRat(Type,LRnd,LRA,LB),
- make_OCamlRat(HA,HRA),
- float_of_OCamlRat(Type,HRnd,HRA,HB),
+ ((LRnd == rtn,
+ LA == 0)
+ ->
+ LB = -0.0
+ ; make_OCamlRat(LA,LRA),
+ float_of_OCamlRat(Type,LRnd,LRA,LB)),
+ ((LRnd == rtn,
+ HA == 0)
+ ->
+ HB = -0.0
+ ; make_OCamlRat(HA,HRA),
+ float_of_OCamlRat(Type,HRnd,HRA,HB)),
set_typed_intervals(B,Type,[LB..HB])
; true),
% pas de projection inverse
@@ -7469,34 +7469,32 @@ cast_int_real_intervals(Type,[I|L],[CI|CL]) :-
%% Pour simplif_node
int_to_real_interval(I,CI) :-
- getval(float_eval,Type)@eclipse,
- int_to_real_interval(Type,I,CI).
+ getval(float_eval,Type)@eclipse,
+ int_to_real_interval(Type,I,CI).
int_to_real_interval(real,I,CI) :- !,
- int_to_real_interval0(I,CI).
+ int_to_real_interval0(I,CI).
int_to_real_interval(Type,I,CI) :-
- int_to_float_interval(Type,I,CI).
+ int_to_float_interval(Type,I,CI).
int_to_real_interval0(Min..Max,CI) ?- !,
- int_to_float_min(real,Min,CMin),
- int_to_float_max(real,Max,CMax),
- interval_from_bounds(CMin,CMax,CI).
+ int_to_float_min(real,Min,CMin),
+ int_to_float_max(real,Max,CMax),
+ interval_from_bounds(CMin,CMax,CI).
int_to_real_interval0(I,CI) :-
- int_to_float_min_max(real,I,CMin,CMax),
- interval_from_bounds(CMin,CMax,CI).
+ int_to_float_min_max(real,I,CMin,CMax),
+ interval_from_bounds(CMin,CMax,CI).
int_to_float_interval(Type,Min..Max,CI) ?- !,
- int_to_float(Type,Min,CMin),
- int_to_float(Type,Max,CMax),
- interval_from_bounds(CMin,CMax,CI).
+ int_to_float(Type,Min,CMin),
+ int_to_float(Type,Max,CMax),
+ interval_from_bounds(CMin,CMax,CI).
int_to_float_interval(Type,I,F) :-
- int_to_float(Type,I,F).
+ int_to_float(Type,I,F).
-inv_cast_int_real_interval(Type,1.0Inf,A) ?- !.
-inv_cast_int_real_interval(Type,-1.0Inf,A) ?- !.
inv_cast_int_real_interval(Type,B,A) :-
- mfd:dvar_range(A,MinA,MaxA),
+ mfd:dvar_range(A,MinA,MaxA),
mreal:dvar_range(B,MinB,MaxB),
(MinB == -1.0Inf ->
Stop = 1,
@@ -8400,7 +8398,7 @@ check_op_mult_div_real(real,A,OpA) ?- !,
% -(X op Y) = OpA
% ou -round/truncate(X) = OpA
% on essaye de saturer
- %call(spy_here)@eclipse,
+ call(spy_here)@eclipse,
(foreach(NGs,LNGs) do
call_priority(NGs,2))
; true).
@@ -13603,36 +13601,37 @@ idiv_mod_real(A,B,Q,R) :- !,
% pour la simulation des entiers non bornes par des reels
get_priority(P),
set_priority(1),
- save_cstr_suspensions((A,B)),
- get_saved_cstr_suspensions(LS),
- ((member((_,check_idiv_mod_real(AA,BB,QQ,BQ,RR)),LS),
- A == AA,B == BB)
- ->
- protected_unify(Q,QQ),
- protected_unify(R,RR)
- ; set_lazy_domain(real,BQ),
- launch_float_int_number(BQ),
- ensure_not_NaN([A,B,Q,BQ,R]),
- % 0.0 <= R <= abs(B)-1.0
- launch_geq_real(real,R,0.0),
- abs_val_real(real,B,AbsB),
- launch_gt_real(real,AbsB,R),
- % A = BQ + R
- mult_real(real,B,Q,BQ),
- add_real(real,BQ,R,A),
- % cas à gérer explicitement pour forcer
- % les signes de A et B
- chk_nan(as(A,real) $= as(0.0,real),
- (as(Q,real) $= as(0.0,real)) and
- (as(R,real) $= as(0.0,real)),
- chk_nan(as(A,real) $> as(0.0,real),
- chk_nan(as(B,real) $> as(0.0,real),
- as(Q,real) $>= as(0.0,real),
- as(Q,real) $=< as(0.0,real)),
- chk_nan(as(B,real) $> as(0.0,real),
- as(Q,real) $=< as(0.0,real),
- as(Q,real) $>= as(0.0,real)))),
- check_idiv_mod_real(A,B,Q,BQ,R)),
+ set_lazy_domain(real,A),
+ set_lazy_domain(real,B),
+ set_lazy_domain(real,Q),
+ set_lazy_domain(real,BQ),
+ set_lazy_domain(real,R),
+ launch_float_int_number(A),
+ launch_float_int_number(B),
+ launch_float_int_number(Q),
+ launch_float_int_number(BQ),
+ launch_float_int_number(R),
+ ensure_not_NaN([A,B,Q,BQ,R]),
+ % 0.0 <= R <= abs(B)-1.0
+ launch_geq_real(real,R,0.0),
+ abs_val_real(real,B,AbsB),
+ launch_gt_real(real,AbsB,R),
+ % A = BQ + R
+ mult_real(real,B,Q,BQ),
+ add_real(real,BQ,R,A),
+ % cas à gérer explicitement pour forcer
+ % les signes de A et B
+ chk_nan(as(A,real) $= as(0.0,real),
+ (as(Q,real) $= as(0.0,real)) and
+ (as(R,real) $= as(0.0,real)),
+ chk_nan(as(A,real) $> as(0.0,real),
+ chk_nan(as(B,real) $> as(0.0,real),
+ as(Q,real) $>= as(0.0,real),
+ as(Q,real) $=< as(0.0,real)),
+ chk_nan(as(B,real) $> as(0.0,real),
+ as(Q,real) $=< as(0.0,real),
+ as(Q,real) $>= as(0.0,real)))),
+ check_idiv_mod_real(A,B,Q,BQ,R),
set_priority(P),
wake_if_other_scheduled(P).
@@ -13697,30 +13696,6 @@ check_idiv_mod_real(X,Y,Q,YQ,R) :-
protected_unify(R,RR)
; call_priority(Goal,2))
; true),
- % issue 63, A ETOFFER ?
- % X > 0, X = -OpX, Q = -OpQ ,R = -OpR
- % => idiv_mod_real(OpX,Y,OpQ,OpR)
- % saturation: OpX = Y*OpQ + OpR
- ((member_begin_end((_,op_real1(real,A,B)),LSusp,BLS,ELS,ELS),
- (A == X ->
- OpX = B
- ; B == X,
- OpX = A),
- member_begin_end((_,op_real1(real,C,D)),BLS,BLS1,ELS1,ELS1),
- (C == Q ->
- OpQ = D
- ; D == Q,
- OpQ = C),
- member_begin_end((_,op_real1(real,E,F)),BLS1,BLS2,ELS2,ELS2),
- (E == R ->
- OpR = F
- ; F == R,
- OpR = E))
- ->
- Goal = (mult_real(real,Y,OpQ,YOpQ),
- add_real(real,YOpQ,OpR,OpX)),
- call_priority(Goal,2)
- ; true),
% X et/ou Y variable
((var(Stop),
divides_real_vars(Y,X,[]))
@@ -13753,8 +13728,11 @@ check_idiv_mod_real(X,Y,Q,YQ,R) :-
->
launch_diff_real(real,D1,D2)
; true)),
- my_suspend(check_idiv_mod_real(X,Y,Q,YQ,R),4,
- (X,Y,Q,YQ,R)->suspend:constrained)
+
+ (var(Stop) ->
+ my_suspend(check_idiv_mod_real(X,Y,Q,YQ,R),4,(X,Y,Q,YQ,R)->
+ suspend:constrained)
+ ; true)
; true),
set_priority(P),
wake_if_other_scheduled(P).
@@ -19756,30 +19734,27 @@ diff_real_ineq(_,_,_).
is_removable_real_value_in_var(Type,DiffGt,A,B,PA,NA) ?- !,
number(A),
- (is_float_int_number(B) ->
- get_previous_float_int(Type,A,PA),
- get_next_float_int(Type,A,NA)
- ; (is_float_number(B) ->
- get_previous_float(Type,A,PA0),
- get_next_float(Type,A,NA0),
- ((DiffGt == diff,
- Type \== real,
- abs(A) =:= 0.0)
- ->
- (A == 0.0 ->
- PA = -0.0,
- NA = NA0
- ; % A = -0
- PA = PA0,
- NA = 0.0)
- ; PA = PA0,
- NA = NA0)
- ; Type = real,
- is_float_int_number(B),
- get_previous_float_int(real,A,PA),
- is_inside_mantissa(real,PA),
- get_next_float_int(real,A,NA),
- is_inside_mantissa(real,NA))).
+ (is_float_number(B) ->
+ get_previous_float(Type,A,PA0),
+ get_next_float(Type,A,NA0),
+ ((DiffGt == diff,
+ Type \== real,
+ abs(A) =:= 0.0)
+ ->
+ (A == 0.0 ->
+ PA = -0.0,
+ NA = NA0
+ ; % A = -0
+ PA = PA0,
+ NA = 0.0)
+ ; PA = PA0,
+ NA = NA0)
+ ; Type = real,
+ is_float_int_number(B),
+ get_previous_float_int(real,A,PA),
+ is_inside_mantissa(real,PA),
+ get_next_float_int(real,A,NA),
+ is_inside_mantissa(real,NA)).
diff_real_number_box(_,A,B,1,Continue) ?- !.
diff_real_number_box(Type,A,B,_,Continue) :-
@@ -20152,11 +20127,7 @@ check_geq_real(Type,A,B,_,Suspend) :-
; geq_real_number_box(Type,A,B,Continue),
(var(Continue) ->
true
- ; mreal:mindomain(A,NMinA),
- mreal:maxdomain(B,NMaxB),
- (NMinA >= NMaxB ->
- true
- ; Suspend = 1)))).
+ ; Suspend = 1))).
geq_real_number_box(real,A,B,Continue) ?- !,
(is_real_box_rat(A,RA) ->
@@ -20192,9 +20163,7 @@ geq_real_number_box(real,A,B,Continue) ?- !,
->
true
; % on a pu creer une boite
- ((var(B),
- get_next_float(real,-1.0Inf) =:= MaxB)
- ->
+ (get_next_float(real,-1.0Inf) =:= MaxB ->
launch_box(B),
geq_real_number_box(real,A,B,Continue)
; Continue = 1))))))
@@ -20236,9 +20205,7 @@ geq_real_number_box(real,A,B,Continue) ?- !,
; mreal:maxdomain(B,MaxB),
(MinA >= MaxB ->
true
- ; ((var(B),
- MaxB =:= get_next_float(real,-1.0Inf))
- ->
+ ; (MaxB =:= get_next_float(real,-1.0Inf) ->
launch_box(B),
geq_real_number_box(real,A,B,Continue)
; Continue = 1)))))
@@ -20258,9 +20225,7 @@ geq_real_number_box(real,A,B,Continue) ?- !,
; % peut echouer
mreal:maxdomain(A) >= MinB,
% on peut avoir une boite pour A maintenant
- ((var(A),
- MinA =:= get_previous_float(real,1.0Inf))
- ->
+ (MinA =:= get_previous_float(real,1.0Inf) ->
% nouvelle boite, on recommence
launch_box(A),
geq_real_number_box(real,A,B,Continue)
@@ -20271,15 +20236,11 @@ geq_real_number_box(real,A,B,Continue) ?- !,
mreal:dvar_remove_greater(B,MaxA),
mreal:mindomain(B,MinB),
mreal:dvar_remove_smaller(A,MinB),
- ((var(B),
- mreal:maxdomain(B) =:= get_next_float(real,-1.0Inf))
- ->
+ (mreal:maxdomain(B) =:= get_next_float(real,-1.0Inf) ->
launch_box(B),
Iter = 1
; true),
- ((var(A),
- mreal:mindomain(A) =:= get_previous_float(real,1.0Inf))
- ->
+ (mreal:mindomain(A) =:= get_previous_float(real,1.0Inf) ->
launch_box(A),
Iter = 1
; true),
diff --git a/Src/COLIBRI/smt_import.pl b/Src/COLIBRI/smt_import.pl
index cc621e38c28b185c1b9a4d9f2e66995bc93a5dfd..51496686c66e1dd460c1d86e610dac4981a715e4 100644
--- a/Src/COLIBRI/smt_import.pl
+++ b/Src/COLIBRI/smt_import.pl
@@ -23,7 +23,7 @@ quant_abs(Expr) :-
(occurs(Expr,(0,1)) ->
Var = Expr
; exit_block(syntax))
- ; %Var = 1,
+ ; Var = 1,
call(as(Var,bool) #= as(Expr,bool)))),
getval(quant_abs,TL),
(TL == 0 ->
@@ -91,8 +91,7 @@ parse_smtlib_file(File,Res) :-
wait(ComPid,Status),
Status == 0
; FilteredFile = File),
- ignore_logic(FilteredFile,NFilteredFile),
- block((p_simplex_ocaml_create_parser(NFilteredFile,PEnv),
+ block((p_simplex_ocaml_create_parser(FilteredFile,PEnv),
read_dolmen_terms(PEnv,Res)),
Tag,
(getval(scrambler,1)@eclipse ->
@@ -100,45 +99,6 @@ parse_smtlib_file(File,Res) :-
exit(4)
; exit_block(Tag))).
-ignore_logic(File,NFile) :-
- open(File,update,Stream),
- find_logic(Stream,Logic,NewFstr),
- close(Stream),
- setval(logic,Logic)@eclipse,
- (var(NewFstr) ->
- NFile = File
- ; NFile = "/tmp/col_temp.smt2",
- open(NFile,write,S),
- write(S,NewFstr),
- close(S)).
-find_logic(Stream,Logic,NewFStr) :-
- (at_eof(Stream) ->
- Logic = ALL
- ; at(Stream,Pos),
- read_string(Stream, end_of_line, Length, String),
- ((substring(String,Before,After,"(set-logic "),
- PBefore is Before-1,
- not substring(String,1,PBefore,";"))
- ->
- (String == "(set-logic ALL)" ->
- Logic = "ALL"
- ; Start is Before+11,
- End is Length-Start,
- substring(String,Start,End,EStr),
- split_string(EStr,")","",LEstr),
- (LEstr = [Logic] ->
- true
- ; LEstr = [_,Logic|_]),
- at(Stream,PosE),
- read_string(Stream,end_of_file,_,EFStr),
- % on remplace pas un commentaire
- concat_string(["(set-logic ALL)\n;",String,"\n",EFStr],EndStr),
- seek(Stream,0),
- read_string(Stream,end_of_file,_,FStr),
- substring(FStr,1,Pos,BFStr),
- concat_string([BFStr,EndStr],NewFStr))
- ; find_logic(Stream,Logic,NewFStr))).
-
read_dolmen_terms(PEnv,Terms) :-
p_simplex_ocaml_parser_next(PEnv,DTerm),
(DTerm == end ->
@@ -665,16 +625,10 @@ check_sat :-
writeln(output,unknown),
setval(unknown_quantifier_abstraction,1)@eclipse
; setval(unknown_quantifier_abstraction,0)@eclipse,
- %setval(check_sat_vars,1)@eclipse,
- check_sat0)).
-/* (check_sat_vars ->
- setval(check_sat_vars,0)@eclipse,
- setval(diag_code,(sat,1))@eclipse,
- writeln(output,sat)
- ; setval(diag_code,(unknown,2))@eclipse,
- writeln(output,unknown),
- setval(check_sat_vars,0)@eclipse))).
-*/
+ check_sat_vars,
+ setval(diag_code,(sat,1))@eclipse,
+ writeln(output,sat))).
+
check_sat0 :-
% pour les unknowm lies aux
% contraintes residuelles en Real
@@ -1879,14 +1833,7 @@ add_binding(Var,Type,Val) :-
get_binding(Var,Type,Val) :-
getval(binding,HBinding),
hash_contains(HBinding,Var),
- hash_get(HBinding,Var,(Type0,Val)),
- (var(Type) ->
- Type = Type0
- ; (real_type(Type0,T) ->
- (var(Type) ->
- Type = T
- ; real_type(Type,T))
- ; Type0 = Type)).
+ hash_get(HBinding,Var,(Type,Val)).
add_label(Label,Type,Val) :-
getval(binding,HBinding),
@@ -1924,13 +1871,7 @@ remove_let_var(Var) :-
get_let_var_type(Var,NVar,Type) :-
atomic(Var),
getval(let_vars,HLV),
- hash_get(HLV,Var,(Type0,NVar)),
- (var(Type) ->
- Type = Type0
- ; (Type == Type0 ->
- true
- ; real_type(Type,T),
- real_type(Type,T))).
+ hash_get(HLV,Var,(Type,NVar)).
unsupported_error(Com) :-
concat_string(["(error \"Unsupported:",Com,"\")"],Err),
@@ -2023,9 +1964,8 @@ smt_interp(Expr,IExpr,Type) :-
:- setval(in_assert,0).
% INTERPRETATION
smt_interp0(exit,true,bool) :- !.
-smt_interp0('set-logic'(SLogic),true,bool) :- !.
- % deja fait dans ignore_logic
- % setval(logic,SLogic)@eclipse.
+smt_interp0('set-logic'(SLogic),true,bool) :- !,
+ setval(logic,SLogic)@eclipse.
smt_interp0('get-info'(Key),true,bool) :-
call(spy_here)@eclipse,
@@ -2102,8 +2042,7 @@ smt_interp0(assert(A0),NewDecl,bool) :- !,
; IA = IA0))
; IA = IA0),
getval(decl,Decl-NEnd),
- ((var(IA),
- VIA = IA;
+ ((var(IA),VIA = IA;
remove_upper_as(IA,VIA,_),
var(VIA))
->
@@ -2114,7 +2053,17 @@ smt_interp0(assert(A0),NewDecl,bool) :- !,
; NEnd = IA),
(integer(Decl) ->
NDecl = as(Decl,bool)
- ; NDecl = Decl)),
+ ; ((Decl =.. [FD,X,Y],
+ occurs(FD,('#=','$=')),
+ remove_upper_as(X,X1,_),
+ remove_upper_as(Y,Y1,_),
+ (var(X1);atomic(X1)),
+ (var(Y1);atomic(Y1)))
+ ->
+ (protected_unify(X1,Y1) ->
+ NDecl = as(1,bool)
+ ; NDecl = as(0,bool))
+ ; NDecl = Decl))),
reset_let_vars,
remove_true_decl(NDecl,NewDecl),
setval(decl,OD),
@@ -2426,7 +2375,9 @@ smt_interp0(not(A),NegIA,bool) :- !,
((nonvar(A),
remove_upper_as(A,AA,_),
(AA = let(Pairs,Expr),
- NA = let(Pairs,not(Expr))))
+ NA = let(Pairs,not(Expr));
+ AA = forall(Pairs,Expr),
+ NA = exists(Pairs,not(Expr))))
->
smt_interp(NA,NegIA,bool)
; ((nonvar(A),
@@ -2454,14 +2405,8 @@ smt_interp0(A => B,IA => IB,bool) :- !,
smt_interp(B,IB,bool).
% comparaisons
smt_interp0(A < B,Comp,bool) :- !,
- smt_interp(A,IA0,Type0),
- smt_interp(B,IB,Type1),
- ((real_type(Type0,Type),
- real_type(Type1,Type))
- ->
- true
- ; Type0 == Type1,
- Type = Type0),
+ smt_interp(A,IA0,Type),
+ smt_interp(B,IB,Type),
get_real_int_type_from_logic(Type),
add_as(Type,IA0,IA),
functor(Type,FType,_),
@@ -2469,14 +2414,8 @@ smt_interp0(A < B,Comp,bool) :- !,
Comp = (as(IA,FType) #< IB)
; Comp = (IA $< IB)).
smt_interp0(A <= B,Comp,bool) :- !,
- smt_interp(A,IA0,Type0),
- smt_interp(B,IB,Type1),
- ((real_type(Type0,Type),
- real_type(Type1,Type))
- ->
- true
- ; Type0 == Type1,
- Type = Type0),
+ smt_interp(A,IA0,Type),
+ smt_interp(B,IB,Type),
get_real_int_type_from_logic(Type),
add_as(Type,IA0,IA),
functor(Type,FType,_),
@@ -3533,23 +3472,13 @@ get_type_from_sort('Bool',bool,bool) :- !.
get_type_from_sort('Int',IType,Type) :-
setval(int_used,1)@eclipse,
(getval(real_for_int,1)@eclipse ->
- (var(IType) ->
- IType = real_int,
- Type = real_int
- ; Type = real)
+% IType = real,
+ IType = real_int,
+ Type = real_int
; Type = IType,
IType = int),
!.
-get_type_from_sort('Real',IType,Type) ?- !,
- (var(IType) ->
- (var(Type) ->
- IType = real,
- Type = IType
- ; Type = IType)
- ; (var(Type) ->
- Type = IType
- ; occurs(IType,(real,real_int)),
- occurs(Type,(real,real_int)))).
+get_type_from_sort('Real',real,real) :- !.
get_type_from_sort('RoundingMode',rnd,rnd) :- !.
get_type_from_sort('_'('BitVec',N),uint(N),uint(N)) :- !.
get_type_from_sort('Float32',float_simple,float) :- !.
diff --git a/Src/COLIBRI/solve.pl b/Src/COLIBRI/solve.pl
index 6236381094f3bc587d489fb57e9f70b9e8fd363b..759b7a66a6ce6f39ee6855a8aa6a5a232818da61 100644
--- a/Src/COLIBRI/solve.pl
+++ b/Src/COLIBRI/solve.pl
@@ -2488,7 +2488,7 @@ unfold_int_expr(EA $= EB,D,Cstr,Type0,R) ?-
insert_dep_inst(dep(A,D,[R])),
insert_dep_inst(dep(B,D,[R])),
make_conj(CA,CB,CAB),
- ((fail,(Type \== real;
+ (((Type \== real;
fail,is_float_int_number(B)),
(number(A),
C = A;
@@ -2497,7 +2497,7 @@ unfold_int_expr(EA $= EB,D,Cstr,Type0,R) ?-
var(B))
->
Goal = in_intervals_reif(Type,B,[C],R)
- ; ((fail,(Type \== real;
+ ; (((Type \== real;
fail,is_float_int_number(A)),
(number(B),
C = B;
@@ -2574,7 +2574,7 @@ unfold_int_expr(EA $\= EB,D,Cstr,Type0,R) ?- !,
insert_dep_inst(dep(A,D,[R])),
insert_dep_inst(dep(B,D,[R])),
make_conj(CA,CB,CAB),
- (fail,(Type \== real,
+ ((Type \== real,
(number(A),C = A;
number(EA),to_real(Type,EA,C)),
var(B))
@@ -2588,7 +2588,7 @@ unfold_int_expr(EA $\= EB,D,Cstr,Type0,R) ?- !,
Inter = [NA..1.0Inf]
; Inter = [-1.0Inf..PA,NA..1.0Inf])),
Goal = in_intervals_reif(Type,B,Inter,R)
- ; ((fail,(Type \== real;
+ ; (((Type \== real;
fail,is_float_int_number(A)),
(number(B),
C = B;
@@ -2642,7 +2642,7 @@ unfold_int_expr(EA $< EB,D,Cstr,Type0,R) ?-
insert_dep_inst(dep(A,D,[R])),
insert_dep_inst(dep(B,D,[R])),
min_max_lazy(Type,Min,Max,_),
- ((fail,(Type \== real;
+ (((Type \== real;
fail,is_float_int_number(B),
FI = 1),
(number(A),C = A;
@@ -2655,7 +2655,7 @@ unfold_int_expr(EA $< EB,D,Cstr,Type0,R) ?-
; NA = C),
Inter = [NA..Max],
Goal = in_intervals_reif(Type,B,Inter,R)
- ; ((fail,(Type \== real;
+ ; (((Type \== real;
fail,is_float_int_number(A),
FI = 1),
(number(B),C = B;
@@ -2745,7 +2745,7 @@ unfold_int_expr(EA $=< EB,D,Cstr,Type0,R) ?-
insert_dep_inst(dep(A,D,[R])),
insert_dep_inst(dep(B,D,[R])),
min_max_lazy(Type,Min,Max,_),
- ((fail,(Type \== real;
+ (((Type \== real;
fail,is_float_int_number(B)),
(number(A),C = A;
number(EA),to_real(Type,EA,C)),
@@ -2759,7 +2759,7 @@ unfold_int_expr(EA $=< EB,D,Cstr,Type0,R) ?-
; NC = C),
Inter = [NC..Max],
Goal = in_intervals_reif(Type,B,Inter,R)
- ; ((fail,(Type \== real;
+ ; (((Type \== real;
fail,is_float_int_number(A)),
(number(B),C = B;
number(EB),to_real(Type,EB,C)),
@@ -5818,10 +5818,7 @@ isNaN(F,R) :-
protected_unify(R,RR),
(R == 0 ->
ensure_not_NaN(F)
- ; (R == 1 ->
- protected_unify(F,nan)
- ; % on laisse l'autre travailler
- true))
+ ; true)
; my_suspend(isNaN(F,R),0,[trigger(isNaN),(F,R)->suspend:constrained])))),
set_priority(Prio),
wake_if_other_scheduled(Prio).
@@ -6295,8 +6292,7 @@ to_real(Type,X,FX) :-
to_real1(real,X,FX) ?- !,
(getval(check_sat_vars,1)@eclipse ->
FX = X
- ; rational(X,RX),
- term_string(RX,SX),
+ ; term_string(X,SX),
unfold_real_expr(realString(SX),0,_,real,FX)).
%norm_zero(real,X,FX).
to_real1(_Type,nan,FX) ?- !,
@@ -6600,11 +6596,6 @@ unfold_real_expr(float_from_raw_uintN(EA),D,Cstr,Type,R) :-
; Size == 64,
Type = float_double),
!,
- unfold_int_expr(isNaN(as(R,Type)),D,CN,bool,Bool),
- insert_dep_inst(dep(R,D,[A,Bool])),
- make_conj(CA,CN,CAN),
- make_conj(CAN,float_from_raw_uintN(Type,A,R),Cstr).
-/*
((number(A);
number(R))
->
@@ -6612,7 +6603,6 @@ unfold_real_expr(float_from_raw_uintN(EA),D,Cstr,Type,R) :-
blocked_call(float_from_raw_uintN(Type,A,R))
; insert_dep_inst(dep(R,D,[A])),
make_conj(CA,float_from_raw_uintN(Type,A,R),Cstr)).
-*/
unfold_real_expr(float_from_int(EA),D,Cstr,float_simple,R) :- !,
unfold_real_expr(float_from_int(rne,EA),D,Cstr,float_simple,R).
unfold_real_expr(float_from_int(Rnd0,EA),D,Cstr,float_simple,R) :-
@@ -10145,35 +10135,27 @@ check_exists_fp_geq_reif(Cond,Type,A,B,Bool,Continue) :-
; Continue = 1).
-gt_real_reif(Type,A,A,Bool) ?-
- check_not_NaN(A),
- !,
- protected_unify(Bool,0).
-gt_real_reif(Type,A,B,Bool) ?-
- Type \== real,
- is_fzero(A),
- is_fzero(B),
- !,
- protected_unify(Bool,0).
gt_real_reif(Type,A,B,Bool) :-
- (nonvar(Bool) ->
- (Bool == 1 ->
- launch_gt_real(Type,A,B)
- ; % Bool = 0
- launch_geq_real(Type,B,A))
- ; ((getval(check_sat_vars,1)@eclipse,
- Type == real,
- once (number(A),
- rational(A,RA);
- is_real_box_rat(A,RA)),
- once (number(B),
- rational(B,RB);
- is_real_box_rat(B,RB)))
- ->
- (RA > RB ->
- protected_unify(Bool,1)
- ; protected_unify(Bool,0))
- ; gt_real_reif_bis(Type,A,B,Bool))).
+ (A == B ->
+ protected_unify(Bool,0)
+ ; (nonvar(Bool) ->
+ (Bool == 1 ->
+ launch_gt_real(Type,A,B)
+ ; % Bool = 0
+ launch_geq_real(Type,B,A))
+ ; ((getval(check_sat_vars,1)@eclipse,
+ Type == real,
+ once (number(A),
+ rational(A,RA);
+ is_real_box_rat(A,RA)),
+ once (number(B),
+ rational(B,RB);
+ is_real_box_rat(B,RB)))
+ ->
+ (RA > RB ->
+ protected_unify(Bool,1)
+ ; protected_unify(Bool,0))
+ ; gt_real_reif_bis(Type,A,B,Bool)))).
gt_real_reif_bis(Type,A,B,Bool) :-
get_priority(Prio),
@@ -10222,32 +10204,9 @@ check_exists_gt_real_reif(Type,A,B,Bool,Continue) :-
; Continue = 1).
-geq_real_reif(Type,A,A,Bool) ?-
- check_not_NaN(A),
- !,
- protected_unify(Bool,1).
-geq_real_reif(Type,A,B,Bool) ?-
- Type \== real,
- is_fzero(A),
- is_fzero(B),
- !,
- protected_unify(Bool,1).
geq_real_reif(Type,A,B,Bool) :-
- get_priority(Prio),
- set_priority(1),
not_int(Bool,NotBool),
- gt_real_reif(Type,B,A,NotBool),
- (nonvar(Bool) ->
- (Bool == 1 ->
- protected_unify(NotBool,0)
- ; protected_unify(NotBool,1))
- ; (nonvar(NotBool) ->
- (NotBool == 1 ->
- protected_unify(Bool,0)
- ; protected_unify(Bool,1))
- ; true)),
- set_priority(Prio),
- wake_if_other_scheduled(Prio).
+ gt_real_reif(Type,B,A,NotBool).
/*
geq_real_reif(Type,A,B,Bool) :-
gt_real_reif(Type,B,A,NotBool),
@@ -10294,9 +10253,11 @@ float_from_raw_uintN(Type,Size,Int,Res) :-
Res == R,
check_not_NaN(Res)))
->
+ kill_suspension(S),
protected_unify(Int,IInt),
protected_unify(R,Res)
- ; check_before_susp_float_from_raw_uintN(Type,Size,Int,Res))),
+ ; true),
+ check_before_susp_float_from_raw_uintN(Type,Size,Int,Res)),
set_priority(Prio),
wake_if_other_scheduled(Prio).
@@ -10304,10 +10265,10 @@ check_before_susp_float_from_raw_uintN(Type,Size,Int,Res) :-
float_from_raw_uintN_inst(Type,Size,Int,Res,Continue),
(var(Continue) ->
true
- ; ((true;check_not_NaN(Res)) ->
+ ; (check_not_NaN(Res) ->
my_suspend(float_from_raw_uintN(Type,Size,Int,Res),
0,(Int,Res)->suspend:constrained),
- ((true;get_sign(Res,_)) ->
+ (get_sign(Res,_) ->
true
; % A VERIFIER SUR UnitTest QF_*BVFP* !!!
chk_nan(not(isZero((as(Res,Type)))),
@@ -10315,14 +10276,10 @@ check_before_susp_float_from_raw_uintN(Type,Size,Int,Res) :-
as(0.0,Type) $>= as(Res,Type),
as(Res,Type) $>= as(0.0,Type)),
as(1,bool)))
- ; get_saved_cstr_suspensions(LS),
- ((member((_,isNaN(R,B)),LS),
- R == Res)
- ->
- protected_unify(B,Bool)
- ; int_vars(bool,Bool),
- isNaN(Res,Bool)),
- my_suspend(float_from_raw_uintN(Type,Size,Int,Res),0,Bool->suspend:inst))).
+ ; int_vars(bool,Bool),
+ my_suspend(float_from_raw_uintN(Type,Size,Int,Res),
+ 0,Bool->suspend:inst),
+ isNaN(Res,Bool))).
float_from_raw_uintN_inst(Type,Size,Int,Res,Continue) :-
(integer(Int) ->
@@ -11155,7 +11112,6 @@ cdiv_crem(A,B,Q,R) :-
mult_real(real,B,Q,BQ),
% A = BQ + R
add_real(real,BQ,R,A),
-/*
% cas à gérer explicitement pour forcer
% les signes de A et B
chk_nan(as(A,real) $= as(0.0,real),
@@ -11168,7 +11124,6 @@ cdiv_crem(A,B,Q,R) :-
chk_nan(as(B,real) $> as(0.0,real),
as(Q,real) $=< as(0.0,real),
as(Q,real) $>= as(0.0,real)))),
-*/
check_cdiv_crem(A,B,Q,BQ,R),
set_priority(P),
wake_if_other_scheduled(P).
@@ -11177,53 +11132,22 @@ cdiv_crem(A,B,Q,R) :-
check_cdiv_crem(A,B,Q,BQ,R) :-
get_priority(P),
set_priority(1),
- check_cdiv_crem_inst_free(A,B,Q,BQ,R,Continue),
- (nonvar(Continue) ->
- check_cdiv_crem1(A,B,Q,BQ,R)
- ; true),
+ check_cdiv_crem1(A,B,Q,BQ,R),
set_priority(P),
wake_if_other_scheduled(P).
-check_cdiv_crem_inst_free(A,B,Q,BQ,R,Continue) ?- !,
- (A == 0.0 ->
- protected_unify(Q,0.0),
- protected_unify(R,0.0);
- (B == 1 ->
- protected_unify(Q,A),
- protected_unify(R,0.0);
- (B == -1 ->
- protected_unify(R,0.0),
- op_real(real,A,Q);
- (R == 0 ->
- mult_real(real,B,Q,A);
- (A == B ->
- protected_unify(Q,1.0),
- protected_unify(R,0.0);
- (A == R ->
- protected_unify(BQ,0.0),
- protected_unify(Q,0.0);
- ((Q == 0.0;
- BQ == 0.0)
- ->
- protected_unify(Q,0.0),
- protected_unify(BQ,0.0),
- protected_unify(A,R);
- ((is_inst_box(B),
- once (is_inst_box(A);
- is_inst_box(Q)))
- ->
- div_real(real,A,B,RQ),
- truncate(real,RQ,Q),
- mult_real(real,B,Q,BQ),
- add_real(real,BQ,R,A);
- Continue = 1)))))))).
-
-is_inst_box(A) :-
- once (nonvar(A);
- is_real_box_rat(A,_)).
-
+check_cdiv_crem1(A,B,Q,BQ,A) ?- !,
+ protected_unify(BQ,0.0),
+ protected_unify(Q,0.0).
+check_cdiv_crem1(A,B,Q,BQ,R) :-
+ nonvar(A),
+ nonvar(B),
+ !,
+ div_real(real,A,B,RQ),
+ truncate(real,RQ,Q),
+ mult_real(real,B,Q,BQ),
+ add_real(real,BQ,R,A).
check_cdiv_crem1(A,B,Q,BQ,R) :-
-/*
((not not_zero(A),
not not_zero(Q),
(nonvar(A);
@@ -11232,21 +11156,18 @@ check_cdiv_crem1(A,B,Q,BQ,R) :-
is_real_box_rat(B,_)))
->
true
- ;
-*/
- % A FAIRE: anti_congr,gestion des opposés ...
- save_cstr_suspensions((A,B,Q,BQ,R)),
- get_saved_cstr_suspensions(LS1),
- attached_suspensions(cdcr,LST),
- (foreach(S,LST),
- fromto(LS1,ILS,OLS,LS) do
- (get_suspension_data(S,goal,GS) ->
- OLS = [(S,GS)|ILS]
- ; OLS = ILS)),
- (member((_,check_cdiv_crem(_,_,_,_,_)),LS) ->
+ ; % A FAIRE: anti_congr,gestion des opposés ...
+ save_cstr_suspensions((A,B,Q,BQ,R)),
+ get_saved_cstr_suspensions(LS1),
+ attached_suspensions(cdcr,LST),
+ (foreach(S,LST),
+ fromto(LS1,ILS,OLS,LS) do
+ (get_suspension_data(S,goal,GS) ->
+ OLS = [(S,GS)|ILS]
+ ; OLS = ILS)),
(foreach((S,G),LS),
foreach(Unif,LUnif),
- param(A,B,Q,BQ,R,Stop) do
+ param(A,B,Q,BQ,R) do
(G = check_cdiv_crem(AA,BB,QQ,BBQQ,RR) ->
(AA == A ->
(BB == B ->
@@ -11258,9 +11179,7 @@ check_cdiv_crem1(A,B,Q,BQ,R) :-
; (RR == R ->
% R = A - BBQQ et R = A - BQ
% donc BBQQ = BQ
- ((QQ == Q,
- not_zero(Q))
- ->
+ (QQ == Q ->
% R = A - BBQ et R = A - BQ
% donc BB == B
Stop = 1,
@@ -11290,7 +11209,9 @@ check_cdiv_crem1(A,B,Q,BQ,R) :-
% donc RR = OpA + BQ
% donc RR = -R
Stop = 1,
- Unif = (op_real_bis(real,Q,QQ),
+ Unif = (set_lazy_domain(real,Q,QQ),
+ op_real_bis(real,Q,QQ),
+ set_lazy_domain(real,RR),
op_real_bis(real,R,RR))
; ((is_op_real(real,B,OpB),
BB == OpB)
@@ -11302,18 +11223,19 @@ check_cdiv_crem1(A,B,Q,BQ,R) :-
% donc RR = -R
Stop = 1,
Unif = (protected_unify(Q,QQ),
+ set_lazy_domain(real,BBQQ),
op_real_bis(real,BQ,BBQQ),
+ set_lazy_domain(real,RR),
op_real_bis(real,R,RR))
; Unif = true))
; Unif = true))
; Unif = true)),
(foreach(U,LUnif) do
- call_priority(U,2))
- ; true),
- (nonvar(Stop) ->
- true
- ; my_suspend(check_cdiv_crem(A,B,Q,BQ,R),0,
- [trigger(cdcr),(A,B,Q,BQ,R)->suspend:constrained])).
+ call_priority(U,2)),
+ (var(Stop) ->
+ my_suspend(check_cdiv_crem(A,B,Q,BQ,R),0,
+ [trigger(cdcr),(A,B,Q,BQ,R)->suspend:constrained])
+ ; true)).
same_abs(Type,A,X,LSusp,Rel,NLSusp) :-
(Type = real ->
@@ -12849,7 +12771,6 @@ dvar_size_check_real(real,V,Size) ?- !,
real_int_size(V,Size)
; dvar_size(float_double,V,Size))
; Size = 1.0Inf).
-
dvar_size_check_real(Type,V,Size) :-
dvar_size(Type,V,Size).