diff --git a/Src/COLIBRI/check_lin_expr.pl b/Src/COLIBRI/check_lin_expr.pl
index b51c5c62ccb66a97e2833f53b82df2e6f4cea308..6197d3892fa71e6b8ca3fab7eeb9c51a6901250e 100755
--- a/Src/COLIBRI/check_lin_expr.pl
+++ b/Src/COLIBRI/check_lin_expr.pl
@@ -71,7 +71,6 @@ 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),
@@ -117,21 +116,30 @@ 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),
- ((number(A),Val = A,Other = B;
- number(B),Val = B,Other = A)
+ ((is_real_box_rat(A,RA),
+ is_real_box_rat(B,RB))
->
- (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),
+ RA \== RB,
+ Stop = 1
+ ; ((number(A),
+ Val = A,
+ Other = B;
+ number(B),
+ Val = B,
+ Other = A)
+ ->
+ (Type == int ->
+ mfd:dvar_remove_element(Other,Val),
Stop = 1
- ; true))
- ; true).
+ ; % 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)).
%% 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 2cf9d66f177eeb115c28d4ef23e34ab6018cc96e..f9f6e9fd365e2b7f869a30c8a25395cb50ba2dbe 100644
--- a/Src/COLIBRI/col_solve.pl
+++ b/Src/COLIBRI/col_solve.pl
@@ -613,10 +613,11 @@ smt_solve_bis0(Test,FILE,Code) :-
; true),
Code = 3,
setval(diag_code,(timeout,3))
- ; (Tag == syntax ->
+ ; (TagRead == syntax ->
concat_string(["(error \"",FILE,":",TagRead,"\")"],Mess),
writeln(output,Mess),
- Code = 2
+ Code = 2,
+ setval(diag_code,(unknown,2))
; % debug
(Test == 1 -> halt;true),
writeln(output,unknown),
@@ -754,7 +755,10 @@ 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),
- remove_unused_decl_goal(LDecl,NLDecl,NLGoal1,CleanLGoal),
+ (occurs(get_model,LEndNewGoal) ->
+ NLDecl = LDecl,
+ CleanLGoal = NLGoal1
+ ; remove_unused_decl_goal(LDecl,NLDecl,NLGoal1,LEndNewGoal,CleanLGoal)),
keep_ground_goals(CleanLGoal,NLGoal2,_GCG,_EGCG),
% BUG copy_term trop gros
@@ -799,10 +803,11 @@ 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,NLG) ?- !,
+remove_unused_decl_goal([],[],LG,_,LG).
+remove_unused_decl_goal([D|LD],NLD,LG,LEndNewGoal,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,
@@ -816,9 +821,9 @@ remove_unused_decl_goal([D|LD],NLD,LG,NLG) ?- !,
->
% D inutile
% call(spy_here)@eclipse,
- remove_unused_decl_goal(LD,NLD,NewLG,NLG)
+ remove_unused_decl_goal(LD,NLD,NewLG,LEndNewGoal,NLG)
; NLD = [D|ENLD],
- remove_unused_decl_goal(LD,ENLD,LG,NLG)).
+ remove_unused_decl_goal(LD,ENLD,LG,LEndNewGoal,NLG)).
:- export my_term_variables/2.
my_term_variables(Term,Vars) :-
@@ -1944,6 +1949,7 @@ check_unit_tests(SatUnsat,TO,Mod) :-
check_unit_tests(SatUnsat,TO) :-
Sat = [
+ "./UnitTests/sat/BV/",
"./UnitTests/sat/FP/",
"./UnitTests/sat/BVFP/",
"./UnitTests/sat/FPLRA/",
@@ -1979,6 +1985,7 @@ 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/lp_arith.pl b/Src/COLIBRI/lp_arith.pl
index 293df43b3e4aea2d153437da21b98a1bfcf6a21a..b16ee55b1baeb014c945bf6b9956c3bd324229e9 100755
--- a/Src/COLIBRI/lp_arith.pl
+++ b/Src/COLIBRI/lp_arith.pl
@@ -1856,6 +1856,23 @@ 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 61e6c1cf6432dec73fa86a3963b16338cc5d6743..a49fe0db683d29e3fc1a29a74e3dc167b68d443a 100755
--- a/Src/COLIBRI/ndelta.pl
+++ b/Src/COLIBRI/ndelta.pl
@@ -1444,11 +1444,13 @@ 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),
- (NMin0 =:= 0 ->
+ (fail,NMin0 =:= 0 ->
+ % seulement pour int et real_int
NMin = 1
; NMin = NMin0),
NMax0 is protected_rat_min(OMax,Max),
- (NMax0 =:= 0 ->
+ (fail,NMax0 =:= 0 ->
+ % seulement pour int et real_int
NMax = -1
; NMax = NMax0),
% On peut echouer ici
@@ -1463,7 +1465,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 3dae31c41abe98e0933c23863ee25fde19574a38..55c97e8ab8b50438667d9f93d81cd12c76c8d708 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)
- ; safe_minus_rat(B,0.5,A0),
+ ; check_minus_rat(B,0.5,A0),
(A0 == 0.0 ->
(get_sign(B,neg) ->
A = -0.0
@@ -1227,19 +1227,23 @@ ceiling_bis(Type,A,B) :-
true
; (nonvar(A) ->
get_next_float_int(Type,A,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)))),
+ ; (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))))),
(var(Continue) ->
true
; save_cstr_suspensions([A]),
@@ -3264,8 +3268,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),
@@ -3275,8 +3279,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 -> X - C = B
- Goal = minus_real_bis(real,OpX,C,B)
+ % -X + B = C -> C + X = B
+ Goal = add_real_bis(real,OpX,C,B)
; (X == B ->
% A + -X = C -> X + C = A
Goal = add_real_bis(real,OpX,C,A)
@@ -3287,9 +3291,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).
@@ -4636,12 +4640,16 @@ 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;
- is_fzero(B))
+ (((is_fzero(A),
+ ZA = 1,
+ get_type(B,Type);
+ is_fzero(B),
+ get_type(A,Type)),
+ Type \== real)
->
(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 ->
@@ -7085,18 +7093,10 @@ cast_int_real(Rnd,Type,A,B) :-
% initialisation de A si necessaire/possible
(get_type(A,_) ->
dvar_range(int,A,LA,HA),
- ((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)),
+ make_OCamlRat(LA,LRA),
+ float_of_OCamlRat(Type,LRnd,LRA,LB),
+ make_OCamlRat(HA,HRA),
+ float_of_OCamlRat(Type,HRnd,HRA,HB),
set_typed_intervals(B,Type,[LB..HB])
; true),
% pas de projection inverse
@@ -7469,32 +7469,34 @@ 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,
@@ -8398,7 +8400,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).
@@ -13601,37 +13603,36 @@ idiv_mod_real(A,B,Q,R) :- !,
% pour la simulation des entiers non bornes par des reels
get_priority(P),
set_priority(1),
- 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),
+ 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_priority(P),
wake_if_other_scheduled(P).
@@ -13696,6 +13697,30 @@ 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,[]))
@@ -13728,11 +13753,8 @@ check_idiv_mod_real(X,Y,Q,YQ,R) :-
->
launch_diff_real(real,D1,D2)
; true)),
-
- (var(Stop) ->
- my_suspend(check_idiv_mod_real(X,Y,Q,YQ,R),4,(X,Y,Q,YQ,R)->
- suspend:constrained)
- ; true)
+ my_suspend(check_idiv_mod_real(X,Y,Q,YQ,R),4,
+ (X,Y,Q,YQ,R)->suspend:constrained)
; true),
set_priority(P),
wake_if_other_scheduled(P).
@@ -19734,27 +19756,30 @@ diff_real_ineq(_,_,_).
is_removable_real_value_in_var(Type,DiffGt,A,B,PA,NA) ?- !,
number(A),
- (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_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))).
diff_real_number_box(_,A,B,1,Continue) ?- !.
diff_real_number_box(Type,A,B,_,Continue) :-
@@ -20127,7 +20152,11 @@ check_geq_real(Type,A,B,_,Suspend) :-
; geq_real_number_box(Type,A,B,Continue),
(var(Continue) ->
true
- ; Suspend = 1))).
+ ; mreal:mindomain(A,NMinA),
+ mreal:maxdomain(B,NMaxB),
+ (NMinA >= NMaxB ->
+ true
+ ; Suspend = 1)))).
geq_real_number_box(real,A,B,Continue) ?- !,
(is_real_box_rat(A,RA) ->
@@ -20163,7 +20192,9 @@ geq_real_number_box(real,A,B,Continue) ?- !,
->
true
; % on a pu creer une boite
- (get_next_float(real,-1.0Inf) =:= MaxB ->
+ ((var(B),
+ get_next_float(real,-1.0Inf) =:= MaxB)
+ ->
launch_box(B),
geq_real_number_box(real,A,B,Continue)
; Continue = 1))))))
@@ -20205,7 +20236,9 @@ geq_real_number_box(real,A,B,Continue) ?- !,
; mreal:maxdomain(B,MaxB),
(MinA >= MaxB ->
true
- ; (MaxB =:= get_next_float(real,-1.0Inf) ->
+ ; ((var(B),
+ MaxB =:= get_next_float(real,-1.0Inf))
+ ->
launch_box(B),
geq_real_number_box(real,A,B,Continue)
; Continue = 1)))))
@@ -20225,7 +20258,9 @@ geq_real_number_box(real,A,B,Continue) ?- !,
; % peut echouer
mreal:maxdomain(A) >= MinB,
% on peut avoir une boite pour A maintenant
- (MinA =:= get_previous_float(real,1.0Inf) ->
+ ((var(A),
+ MinA =:= get_previous_float(real,1.0Inf))
+ ->
% nouvelle boite, on recommence
launch_box(A),
geq_real_number_box(real,A,B,Continue)
@@ -20236,11 +20271,15 @@ geq_real_number_box(real,A,B,Continue) ?- !,
mreal:dvar_remove_greater(B,MaxA),
mreal:mindomain(B,MinB),
mreal:dvar_remove_smaller(A,MinB),
- (mreal:maxdomain(B) =:= get_next_float(real,-1.0Inf) ->
+ ((var(B),
+ mreal:maxdomain(B) =:= get_next_float(real,-1.0Inf))
+ ->
launch_box(B),
Iter = 1
; true),
- (mreal:mindomain(A) =:= get_previous_float(real,1.0Inf) ->
+ ((var(A),
+ 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 51496686c66e1dd460c1d86e610dac4981a715e4..cc621e38c28b185c1b9a4d9f2e66995bc93a5dfd 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,7 +91,8 @@ parse_smtlib_file(File,Res) :-
wait(ComPid,Status),
Status == 0
; FilteredFile = File),
- block((p_simplex_ocaml_create_parser(FilteredFile,PEnv),
+ ignore_logic(FilteredFile,NFilteredFile),
+ block((p_simplex_ocaml_create_parser(NFilteredFile,PEnv),
read_dolmen_terms(PEnv,Res)),
Tag,
(getval(scrambler,1)@eclipse ->
@@ -99,6 +100,45 @@ 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 ->
@@ -625,10 +665,16 @@ check_sat :-
writeln(output,unknown),
setval(unknown_quantifier_abstraction,1)@eclipse
; setval(unknown_quantifier_abstraction,0)@eclipse,
- check_sat_vars,
- setval(diag_code,(sat,1))@eclipse,
- writeln(output,sat))).
-
+ %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_sat0 :-
% pour les unknowm lies aux
% contraintes residuelles en Real
@@ -1833,7 +1879,14 @@ add_binding(Var,Type,Val) :-
get_binding(Var,Type,Val) :-
getval(binding,HBinding),
hash_contains(HBinding,Var),
- hash_get(HBinding,Var,(Type,Val)).
+ hash_get(HBinding,Var,(Type0,Val)),
+ (var(Type) ->
+ Type = Type0
+ ; (real_type(Type0,T) ->
+ (var(Type) ->
+ Type = T
+ ; real_type(Type,T))
+ ; Type0 = Type)).
add_label(Label,Type,Val) :-
getval(binding,HBinding),
@@ -1871,7 +1924,13 @@ remove_let_var(Var) :-
get_let_var_type(Var,NVar,Type) :-
atomic(Var),
getval(let_vars,HLV),
- hash_get(HLV,Var,(Type,NVar)).
+ hash_get(HLV,Var,(Type0,NVar)),
+ (var(Type) ->
+ Type = Type0
+ ; (Type == Type0 ->
+ true
+ ; real_type(Type,T),
+ real_type(Type,T))).
unsupported_error(Com) :-
concat_string(["(error \"Unsupported:",Com,"\")"],Err),
@@ -1964,8 +2023,9 @@ smt_interp(Expr,IExpr,Type) :-
:- setval(in_assert,0).
% INTERPRETATION
smt_interp0(exit,true,bool) :- !.
-smt_interp0('set-logic'(SLogic),true,bool) :- !,
- setval(logic,SLogic)@eclipse.
+smt_interp0('set-logic'(SLogic),true,bool) :- !.
+ % deja fait dans ignore_logic
+ % setval(logic,SLogic)@eclipse.
smt_interp0('get-info'(Key),true,bool) :-
call(spy_here)@eclipse,
@@ -2042,7 +2102,8 @@ 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))
->
@@ -2053,17 +2114,7 @@ smt_interp0(assert(A0),NewDecl,bool) :- !,
; NEnd = IA),
(integer(Decl) ->
NDecl = as(Decl,bool)
- ; ((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))),
+ ; NDecl = Decl)),
reset_let_vars,
remove_true_decl(NDecl,NewDecl),
setval(decl,OD),
@@ -2375,9 +2426,7 @@ smt_interp0(not(A),NegIA,bool) :- !,
((nonvar(A),
remove_upper_as(A,AA,_),
(AA = let(Pairs,Expr),
- NA = let(Pairs,not(Expr));
- AA = forall(Pairs,Expr),
- NA = exists(Pairs,not(Expr))))
+ NA = let(Pairs,not(Expr))))
->
smt_interp(NA,NegIA,bool)
; ((nonvar(A),
@@ -2405,8 +2454,14 @@ smt_interp0(A => B,IA => IB,bool) :- !,
smt_interp(B,IB,bool).
% comparaisons
smt_interp0(A < B,Comp,bool) :- !,
- smt_interp(A,IA0,Type),
- smt_interp(B,IB,Type),
+ smt_interp(A,IA0,Type0),
+ smt_interp(B,IB,Type1),
+ ((real_type(Type0,Type),
+ real_type(Type1,Type))
+ ->
+ true
+ ; Type0 == Type1,
+ Type = Type0),
get_real_int_type_from_logic(Type),
add_as(Type,IA0,IA),
functor(Type,FType,_),
@@ -2414,8 +2469,14 @@ smt_interp0(A < B,Comp,bool) :- !,
Comp = (as(IA,FType) #< IB)
; Comp = (IA $< IB)).
smt_interp0(A <= B,Comp,bool) :- !,
- smt_interp(A,IA0,Type),
- smt_interp(B,IB,Type),
+ smt_interp(A,IA0,Type0),
+ smt_interp(B,IB,Type1),
+ ((real_type(Type0,Type),
+ real_type(Type1,Type))
+ ->
+ true
+ ; Type0 == Type1,
+ Type = Type0),
get_real_int_type_from_logic(Type),
add_as(Type,IA0,IA),
functor(Type,FType,_),
@@ -3472,13 +3533,23 @@ 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 ->
-% IType = real,
- IType = real_int,
- Type = real_int
+ (var(IType) ->
+ IType = real_int,
+ Type = real_int
+ ; Type = real)
; Type = IType,
IType = int),
!.
-get_type_from_sort('Real',real,real) :- !.
+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('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 759b7a66a6ce6f39ee6855a8aa6a5a232818da61..6236381094f3bc587d489fb57e9f70b9e8fd363b 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),
- (((Type \== real;
+ ((fail,(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)
- ; (((Type \== real;
+ ; ((fail,(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),
- ((Type \== real,
+ (fail,(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)
- ; (((Type \== real;
+ ; ((fail,(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,_),
- (((Type \== real;
+ ((fail,(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)
- ; (((Type \== real;
+ ; ((fail,(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,_),
- (((Type \== real;
+ ((fail,(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)
- ; (((Type \== real;
+ ; ((fail,(Type \== real;
fail,is_float_int_number(A)),
(number(B),C = B;
number(EB),to_real(Type,EB,C)),
@@ -5818,7 +5818,10 @@ isNaN(F,R) :-
protected_unify(R,RR),
(R == 0 ->
ensure_not_NaN(F)
- ; true)
+ ; (R == 1 ->
+ protected_unify(F,nan)
+ ; % on laisse l'autre travailler
+ true))
; my_suspend(isNaN(F,R),0,[trigger(isNaN),(F,R)->suspend:constrained])))),
set_priority(Prio),
wake_if_other_scheduled(Prio).
@@ -6292,7 +6295,8 @@ to_real(Type,X,FX) :-
to_real1(real,X,FX) ?- !,
(getval(check_sat_vars,1)@eclipse ->
FX = X
- ; term_string(X,SX),
+ ; rational(X,RX),
+ term_string(RX,SX),
unfold_real_expr(realString(SX),0,_,real,FX)).
%norm_zero(real,X,FX).
to_real1(_Type,nan,FX) ?- !,
@@ -6596,6 +6600,11 @@ 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))
->
@@ -6603,6 +6612,7 @@ 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) :-
@@ -10135,27 +10145,35 @@ 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) :-
- (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)))).
+ (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),
@@ -10204,9 +10222,32 @@ 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).
+ 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).
/*
geq_real_reif(Type,A,B,Bool) :-
gt_real_reif(Type,B,A,NotBool),
@@ -10253,11 +10294,9 @@ 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)
- ; true),
- check_before_susp_float_from_raw_uintN(Type,Size,Int,Res)),
+ ; check_before_susp_float_from_raw_uintN(Type,Size,Int,Res))),
set_priority(Prio),
wake_if_other_scheduled(Prio).
@@ -10265,10 +10304,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
- ; (check_not_NaN(Res) ->
+ ; ((true;check_not_NaN(Res)) ->
my_suspend(float_from_raw_uintN(Type,Size,Int,Res),
0,(Int,Res)->suspend:constrained),
- (get_sign(Res,_) ->
+ ((true;get_sign(Res,_)) ->
true
; % A VERIFIER SUR UnitTest QF_*BVFP* !!!
chk_nan(not(isZero((as(Res,Type)))),
@@ -10276,10 +10315,14 @@ 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)))
- ; int_vars(bool,Bool),
- my_suspend(float_from_raw_uintN(Type,Size,Int,Res),
- 0,Bool->suspend:inst),
- isNaN(Res,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))).
float_from_raw_uintN_inst(Type,Size,Int,Res,Continue) :-
(integer(Int) ->
@@ -11112,6 +11155,7 @@ 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),
@@ -11124,6 +11168,7 @@ 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).
@@ -11132,22 +11177,53 @@ cdiv_crem(A,B,Q,R) :-
check_cdiv_crem(A,B,Q,BQ,R) :-
get_priority(P),
set_priority(1),
- check_cdiv_crem1(A,B,Q,BQ,R),
+ check_cdiv_crem_inst_free(A,B,Q,BQ,R,Continue),
+ (nonvar(Continue) ->
+ check_cdiv_crem1(A,B,Q,BQ,R)
+ ; true),
set_priority(P),
wake_if_other_scheduled(P).
-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_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,R) :-
+/*
((not not_zero(A),
not not_zero(Q),
(nonvar(A);
@@ -11156,18 +11232,21 @@ 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)),
+ ;
+*/
+ % 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) ->
(foreach((S,G),LS),
foreach(Unif,LUnif),
- param(A,B,Q,BQ,R) do
+ param(A,B,Q,BQ,R,Stop) do
(G = check_cdiv_crem(AA,BB,QQ,BBQQ,RR) ->
(AA == A ->
(BB == B ->
@@ -11179,7 +11258,9 @@ check_cdiv_crem1(A,B,Q,BQ,R) :-
; (RR == R ->
% R = A - BBQQ et R = A - BQ
% donc BBQQ = BQ
- (QQ == Q ->
+ ((QQ == Q,
+ not_zero(Q))
+ ->
% R = A - BBQ et R = A - BQ
% donc BB == B
Stop = 1,
@@ -11209,9 +11290,7 @@ check_cdiv_crem1(A,B,Q,BQ,R) :-
% donc RR = OpA + BQ
% donc RR = -R
Stop = 1,
- Unif = (set_lazy_domain(real,Q,QQ),
- op_real_bis(real,Q,QQ),
- set_lazy_domain(real,RR),
+ Unif = (op_real_bis(real,Q,QQ),
op_real_bis(real,R,RR))
; ((is_op_real(real,B,OpB),
BB == OpB)
@@ -11223,19 +11302,18 @@ 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)),
- (var(Stop) ->
- my_suspend(check_cdiv_crem(A,B,Q,BQ,R),0,
- [trigger(cdcr),(A,B,Q,BQ,R)->suspend:constrained])
- ; true)).
+ 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])).
same_abs(Type,A,X,LSusp,Rel,NLSusp) :-
(Type = real ->
@@ -12771,6 +12849,7 @@ 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).