From c0426ded4bf803bd68e8443b5e3272905619c595 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Fri, 18 Jun 2021 15:58:33 +0200
Subject: [PATCH] Import from Bin:a1af7a0 Src:08a70c336 farith:a93db57
---
Src/COLIBRI/realarith.pl | 6 ++++--
Src/COLIBRI/solve.pl | 45 +++++++++++++++++++++++++++++++++-------
2 files changed, 41 insertions(+), 10 deletions(-)
diff --git a/Src/COLIBRI/realarith.pl b/Src/COLIBRI/realarith.pl
index a5fe445e2..360b43325 100755
--- a/Src/COLIBRI/realarith.pl
+++ b/Src/COLIBRI/realarith.pl
@@ -19385,8 +19385,10 @@ gt_real_float_numberA(A,B,Continue) :-
% en plus, on doit interdire A = B
mreal:maxdomain(B,MaxB),
(MaxB < 1.0Inf ->
- Continue = 1,
- mreal:dvar_remove_smaller(A,MaxB)
+ mreal:dvar_remove_smaller(A,MaxB),
+ (number(A) ->
+ gt_real_numberA(A,B,Continue)
+ ; Continue = 1)
; get_previous_float(real,1.0Inf,PInf),
set_interval_box(A,PInf,1.0Inf),
gt_real_boxA(A,B,Continue))
diff --git a/Src/COLIBRI/solve.pl b/Src/COLIBRI/solve.pl
index 87eb6d996..a8d1cefa6 100644
--- a/Src/COLIBRI/solve.pl
+++ b/Src/COLIBRI/solve.pl
@@ -6545,8 +6545,11 @@ unfold_real_expr(real(EA),D,Cstr,Type,R) ?-
% Conversions depuis float
% hors smtlib
-unfold_real_expr(real_from_float(EA),D,Cstr,real,R) :-
+unfold_real_expr(real_from_float(EA),D,Cstr,Real,R) :-
ND is D + 1,
+ (var(Real) ->
+ Real = real
+ ; real_type(Real,real)),
unfold_real_expr(EA,ND,CA,float_simple,A),
!,
insert_dep_inst(dep(R,D,[A])),
@@ -6623,15 +6626,21 @@ unfold_real_expr(float_from_double(Rnd0,EA),D,Cstr,Type,R) ?-
make_conj(CARnd,Cond,CACond),
make_conj(CACond,double_to_float(BCond,Rnd,A,R),Cstr))).
-unfold_real_expr(real_from_double(EA),D,Cstr,real,R) :-
+unfold_real_expr(real_from_double(EA),D,Cstr,Real,R) :-
ND is D + 1,
+ (var(Real) ->
+ Real = real
+ ; real_type(Real,real)),
unfold_real_expr(EA,ND,CA,float_double,A),
!,
insert_dep_inst(dep(R,D,[A])),
make_conj(CA,float_to_real(float_double,A,R),Cstr).
-unfold_real_expr(fp_to_real(EA),D,Cstr,real,R) :-
+unfold_real_expr(fp_to_real(EA),D,Cstr,Real,R) :-
ND is D + 1,
+ (var(Real) ->
+ Real = real
+ ; real_type(Real,real)),
unfold_real_expr(EA,ND,CA,TypeF,A),
% NaN autorise pour Cond
unfold_int_expr(isNaN(as(A,TypeF)) or isInfinite(as(A,TypeF)),D,Cond,bool,Bool),
@@ -11072,19 +11081,24 @@ choose_fd_var([Adj|UseList],Var,Size,NUseList) :-
MinVars \== [],
leaf_vars([Adj|UseList],Leaves,NUseList),
leaf_var_with_max_cstr_min_dom(MinVars,[],Var,Size).
-% leaf_var_with_max_cstr_min_dom(MinVars,Leaves,Var,Size).
+%% leaf_var_with_max_cstr_min_dom(MinVars,Leaves,Var,Size).
leaf_vars(UseList,Leaves,NUseList) :-
(foreach((V,D,A),UseList),
fromto([],IT,OT,NUseList0) do
- term_variables(A,NA),
+ term_variables(A,NA0),
(nonvar(V) ->
- (foreach(VA,NA),
+ (foreach(VA,NA0),
fromto(IT,INA,ONA,NewAdjs) do
ONA = [(VA,0,[])|INA]),
OT = NewAdjs
- ; OT = [(V,0,NA)|IT])),
+ ; ((member_begin_end(VV,NA0,NA,End,End),
+ VV == V)
+ ->
+ true
+ ; NA = NA0),
+ OT = [(V,0,NA)|IT])),
sort(NUseList0,NUseList),
leaf_vars(NUseList,Leaves0),
sort(Leaves0,Leaves).
@@ -11439,6 +11453,20 @@ leaf_var_with_max_cstr_min_dom(L,Leaves,Var,MinSize) :-
Var,MinSize))).
leaf_var_with_max_cstr_min_dom0([V|LV],Leaves,Var0,NbV0,Size0,Leaf0,Var,MinSize) :-
+ (((occurs(V,Leaves) ->
+ Leaf = 1
+ ; true),
+ (nonvar(Leaf0) ->
+ Leaf == 1
+ ; true),
+ constraints_number(V,NbV),
+ NbV >= NbV0,
+ get_type(V,Type),
+ dvar_size(Type,V,Size),
+ (NbV > NbV0 ->
+ true
+ ; Size < Size0))
+/*
constraints_number(V,NbV),
(occurs(V,Leaves) ->
Leaf = 1
@@ -11452,7 +11480,8 @@ leaf_var_with_max_cstr_min_dom0([V|LV],Leaves,Var0,NbV0,Size0,Leaf0,Var,MinSize)
(nonvar(Leaf0) ->
nonvar(Leaf)
; true)))
- ->
+*/
+ ->
Var1 = V,
NbV1 = NbV,
Size1 = Size,
--
GitLab