From 35c28b66b9cb092830d95ae4ad97832d689e91a8 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Tue, 3 Aug 2021 16:25:45 +0200
Subject: [PATCH] Import from Bin:a1af7a0 Src:7c0e42a8f farith:a93db57
---
Src/COLIBRI/col_solve.pl | 18 +++--
Src/COLIBRI/lp_arith.pl | 4 +-
Src/COLIBRI/realarith.pl | 142 ++++++++++++++++++++------------------
Src/COLIBRI/smt_import.pl | 55 +++++++++++++--
Src/COLIBRI/solve.pl | 105 +++++++++++++++++-----------
5 files changed, 202 insertions(+), 122 deletions(-)
diff --git a/Src/COLIBRI/col_solve.pl b/Src/COLIBRI/col_solve.pl
index 8ddf7328a..724013edc 100644
--- a/Src/COLIBRI/col_solve.pl
+++ b/Src/COLIBRI/col_solve.pl
@@ -520,6 +520,10 @@ smt_comp_solve(FILE) :-
exit(Code).
smt_solve(FILE) :-
+ % Pas de désactivation du simples apres DDSteps
+ DDSteps = 0,
+ setval(simplex_delay_deactivation,DDSteps)@eclipse,
+ % Pas de comptage de steps
setval(step_stats,0)@eclipse,
setval(step_limit,0)@eclipse,
setval(nb_steps,0)@eclipse,
@@ -542,7 +546,7 @@ smt_solve_bis(Test,FILE,TO,Code) :-
setval(simplex_steps,0)@eclipse,
setval(solve,1),
setval(time_limit,0),
- setval(smt_status,0),
+ %setval(smt_status,0),
(nonvar(Test) ->
setval(scrambler,1)
; setval(scrambler,0)),
@@ -736,7 +740,7 @@ smt_test(TO,Size) :-
%StrDir = "./colibri-master-tests/tests/",
%StrDir = "./colibri-master-tests/tests/sat/", %0 (sans real/float-> int!)
%StrDir = "./colibri-master-tests/tests/unsat/", %0
- StrDir = "./colibri-master-tests/tests/unknown/",
+ %StrDir = "./colibri-master-tests/tests/unknown/",
%StrDir = "./smt/",
%StrDir = "./AdaCore/",
@@ -841,7 +845,7 @@ smt_test(TO,Size) :-
%StrDir = "./QF_ABVFP/20170428-Liew-KLEE/aachen_real_gmp_gmp_klee_mul.x86_64/", % 3 (bitwuzla 0)
%StrDir = "QF_ABVFP/20170428-Liew-KLEE/aachen_real_numerical_recipes_qrdcmp.x86_64/",
- %StrDir = "./QF_ABVFP/20170428-Liew-KLEE/", % 106 (177 unsupported) (cvc4 55)
+ %StrDir = "./QF_ABVFP/20170428-Liew-KLEE/", % 105 (177 unsupported) (cvc4 55)
%StrDir = "./QF_ABVFP/20170501-Heizmann-UltimateAutomizer/", % 0 min_solve (cvc4 0) OK
%----------------------------------------------------------------------
%StrDir = "./QF_ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/",% 0 (cvc4 1|2)!
@@ -851,7 +855,7 @@ smt_test(TO,Size) :-
%StrDir = "./QF_BVFP/20170428-Liew-KLEE/imperial_synthetic_sqrt_klee.x86_64/", % 3 (bitwuzla 3)
%StrDir = "./QF_BVFP/20170428-Liew-KLEE/aachen_syn_halve_longdouble-flow.x86_64/",% 4u
- %StrDir = "./QF_BVFP/20170428-Liew-KLEE/", % 17 (cvc4 50)(bitwuzla
+ %StrDir = "./QF_BVFP/20170428-Liew-KLEE/", % 16 (cvc4 50)(bitwuzla
% 15)(89 u)(11 20mn)
%StrDir = "./QF_BVFP/20170501-Heizmann-UltimateAutomizer/", % 0 (bitwuzla 0)
%StrDir = "./QF_BVFP/ramalho/", % 0 TO (bitwuzla 0)
@@ -870,8 +874,8 @@ smt_test(TO,Size) :-
%----------------------------------------------------------------
%StrDir = "./QF_FP/20170501-Heizmann-UltimateAutomizer/", % 0
%StrDir = "./QF_FP/20190429-UltimateAutomizerSvcomp2019/",% 0 (bitwuzla 0)
- %StrDir = "./QF_FP/ramalho/", % 0! (cvc4 19)(bitwuzla 17)
- %StrDir = "./QF_FP/griggio/", % 50 (min_solve, sans lin_solve ni ls_reduce..)(39)
+ %StrDir = "./QF_FP/ramalho/", % 0 (cvc4 19)(bitwuzla 17)
+ StrDir = "./QF_FP/griggio/", % 50 (min_solve, sans lin_solve ni ls_reduce..)(39)
%(cvc4 89)(bitwuzla 74) LES DD DEMARRENT TROP VITE ?
%StrDir = "./QF_FP/schanda/spark/", % 6 (min_solve avec X =< (X+Y)/2 =< Y) (ncvc4 8)(bitwuzla 3)
%StrDir = "./QF_FP/wintersteiger/", % tout OK
@@ -893,7 +897,7 @@ smt_test(TO,Size) :-
%-----------------------------------------------------------------
%StrDir = "QF_AX/",
%StrDir = "QF_AX/storeinv/", % 4
- %StrDir = "QF_AX/swap/", % 8
+ %StrDir = "QF_AX/swap/", % 8 -> 15
%StrDir = "QF_AX/storecomm/", % 0
%StrDir = "QF_AX/cvc/", % 0
diff --git a/Src/COLIBRI/lp_arith.pl b/Src/COLIBRI/lp_arith.pl
index e1c8c78bb..cad874d21 100755
--- a/Src/COLIBRI/lp_arith.pl
+++ b/Src/COLIBRI/lp_arith.pl
@@ -475,7 +475,7 @@ lin_solve1(Status) :-
% quand meme si il n'y a plus de contraintes
((current_suspension(Susp),
get_suspension_data(Susp,goal,Goal),
- not (Goal = uninterp(_,_,_);
+ not (Goal = uninterp(_,_,_,_,_,_);
Goal = fp_eq1(_,_,_);
Goal = op_real1(_,_,_);
Goal = real_to_float_bis(Type,A,_),
@@ -699,7 +699,7 @@ try_lin_solution0(LVars,LSol,Status) :-
set_priority(Prio),
((current_suspension(Susp),
get_suspension_data(Susp,goal,Goal),
- not (Goal = uninterp(_,_,_);
+ not (Goal = uninterp(_,_,_,_,_,_);
(Goal = fp_eq1(Type,Z,_);
Goal = op_real1(Type,Z,_)),
Type \== real,
diff --git a/Src/COLIBRI/realarith.pl b/Src/COLIBRI/realarith.pl
index 8f743bfdd..177ca70b3 100755
--- a/Src/COLIBRI/realarith.pl
+++ b/Src/COLIBRI/realarith.pl
@@ -7331,7 +7331,7 @@ cast_fp_int(Type,A,B) :-
cast_fp_int(0,Type,A,B) ?- !,
cast_real_int(Type,A,B).
cast_fp_int(1,Type,A,B) ?- !,
- uninterp(cast_fp_int,cast_fp_int,[Type,A],B).
+ uninterp(cast_fp_int,cast_fp_int,[Type],int,[A],B).
cast_fp_int(Cond,Type,A,B) :-
get_priority(Prio),
set_priority(1),
@@ -12827,76 +12827,84 @@ div_real_float_intervals1(Type,ValInter1,ValInter2,L,EndL) :-
idiv_mod_real(A,B,Q,R) :-
% version integrale de mod_real
% pour la simulation des entiers non bornes par des reels
- 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]),
- diff_real(real,B,0.0),
+ get_priority(P),
+ set_priority(1),
+ save_cstr_suspensions((A,B)),
+ get_saved_cstr_suspensions(LSusp),
+ ((member((_,check_diff_real(BB,AA,QQ,RR)),LSusp),
+ BB == B,
+ AA == A)
+ ->
+ protected_unify(Q,QQ),
+ protected_unify(R,RR)
+ ; 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]),
+ diff_real(real,B,0.0),
- as(R,real) $>= 0.0,
- % R est borné par B en valeur absolue
- abs(as(R,real)) $< abs(as(B,real)),
-/*
- % R est du signe de B
- ite(as(B,real) $>= 0.0,
as(R,real) $>= 0.0,
- as(R,real) $< 0),
- % Q est du signe de A * B
- ite(as(A,real) $>= 0.0,
- ite(as(B,real) $> 0.0,
- as(Q,real) $>= 0.0,
- as(Q,real) $=< 0.0),
- ite(as(B,real) $< 0.0,
- as(Q,real) $>= 0.0,
- as(Q,real) $=< 0.0)),
-*/
-/*
- div_real(real,A,B,Q0),
- ite(as(B,real) $>= 0.0,
- floor(as(Q0,real)) $= as(Q,real),
- ceiling(as(Q0,real)) $= as(Q,real)),
- %truncate(real,Q0,Q),
-*/ % R = A-BQ
- mult_real(real,B,Q,BQ),
- minus_real(real,A,BQ,R),
- % on teste la divisibilite pour forcer R Ã 0 ou <> 0
- check_divides_real(B,A,R).
+ % R est borné par B en valeur absolue
+ as(R,real) $< abs(as(B,real)),
+ % R = A-BQ, mais de lien direct sur A et B ?
+ mult_real(real,B,Q,BQ),
+ minus_real(real,A,BQ,R),
+ % on teste la divisibilite pour forcer R Ã 0 ou <> 0
+ % et on garde une trace de idiv_mod_real
+ check_divides_real(B,A,Q,R)),
+ set_priority(P),
+ wake_if_other_scheduled(P).
-%check_divides_real(Y,X,R) :- !.
-check_divides_real(X,X,R) ?- !,
+%check_divides_real(Y,X,Q,R) :- !.
+check_divides_real(X,X,Q,R) ?- !,
+ protected_unify(Q,1.0),
protected_unify(R,0.0).
-check_divides_real(Y,X,R) :-
- nonvar(R),
- !.
-check_divides_real(Y,X,R) :-
- not_unify(R,0.0),
- !.
-check_divides_real(Y,X,R) :-
- %is_float_int_number(Y),
- %is_float_int_number(X),
- %not_unify(Y,0.0),
- (((nonvar(Y),
- integer(Y,IY);
- is_real_box_rat(Y,RY),
- integer(RY,IY)),
- (nonvar(X),
- integer(X,IX);
- is_real_box_rat(X,RX),
- integer(RX,IX)))
+check_divides_real(Y,X,Q,R) :-
+ get_priority(P),
+ set_priority(1),
+ save_cstr_suspensions((X,Y)),
+ ((nonvar(Y),
+ nonvar(X))
->
- (IX mod IY =:= 0 ->
- protected_unify(R,0.0)
- ; launch_diff_real(real,R,0.0))
- ; (divides_real_vars(Y,X,[]) ->
+ rational(X,RX),
+ rational(Y,RY),
+ (RY > 0 ->
+ Q is float(floor(RX/RY))
+ ; Q is float(ceiling(RX/RY))),
+ R is float(RX - (RY*rational(Q)))
+ ; % X et/ou Y variable
+ ((var(R),
+ divides_real_vars(Y,X,[]))
+ ->
protected_unify(R,0.0)
- ; my_suspend(check_divides_real(Y,X,R),0,(Y,X,R)->suspend:constrained))).
+ ; true)),
+ ((var(X);
+ var(Y))
+ ->
+ get_saved_cstr_suspensions(LSusp),
+ ((member((_,check_divides_real(YY,XX,QQ,RR)),LSusp),
+ once (YY == Y,
+ OO = XX,
+ O = X;
+ XX == X,
+ OO = YY,
+ O = Y),
+ (exists_diff_Rel(QQ,Q);
+ exists_diff_Rel(RR,R)))
+ ->
+ launch_diff_real(real,OO,O)
+ ; true),
+ my_suspend(check_divides_real(Y,X,Q,R),0,(Y,X)->suspend:constrained)
+ ; true),
+ set_priority(P),
+ wake_if_other_scheduled(P).
divides_real_vars(X,X,_) ?- !.
divides_real_vars(Y,X,Seen) :-
@@ -17680,7 +17688,7 @@ min_real_bis(Type,A,B,C) :-
B == -0.0)
->
concat_atom([fp_min,Type],F),
- uninterp(F,F,[A,B],C)
+ uninterp(F,F,[Type,Type],Type,[A,B],C)
; set_prio_inst([A,B,C],3,4,Prio),
my_suspend(min_real(Type,A,B,C),Prio,(A,B,C)->suspend:constrained))
; true).
@@ -17947,7 +17955,7 @@ max_real_bis(Type,A,B,C) :-
B == -0.0)
->
concat_atom([fp_max,Type],F),
- uninterp(F,F,[A,B],C)
+ uninterp(F,F,[Type,Type],Type,[A,B],C)
; my_suspend(max_real(Type,A,B,C),Prio,(A,B,C) -> suspend:constrained))
; true).
diff --git a/Src/COLIBRI/smt_import.pl b/Src/COLIBRI/smt_import.pl
index cdc395df8..1cbae6d6d 100644
--- a/Src/COLIBRI/smt_import.pl
+++ b/Src/COLIBRI/smt_import.pl
@@ -566,7 +566,7 @@ check_sat0 :-
suspensions(LSusp),
(foreach(Susp,LSusp) do
get_suspension_data(Susp,goal,Goal),
- (Goal = uninterp(_,_,_,_) ->
+ (Goal = uninterp(_,_,_,_,_,_) ->
% on garde les uninterp pour check_sat_vars
true
; kill_suspension(Susp)),
@@ -1143,7 +1143,7 @@ factorize_and_dump_uninterps([(VN,InSorts,OutSort)|Uninterps]) :-
(LSusp \== [] ->
findall((Ins,Out),
(member(Susp,LSusp),
- get_suspension_data(Susp,goal,uninterp(VN,Trigger,Ins,Out)),
+ get_suspension_data(Susp,goal,uninterp(VN,Trigger,_,_,Ins,Out)),
kill_suspension(Susp)),
Profiles),
(foreach(Is,InSorts),
@@ -1597,7 +1597,51 @@ match_isObvious_tests(['fp.isNormal'(Arg),
Res) ?- !,
Res = Arg.
+% Trop lent !!!
+%try_factorize_in_let(Expr,Expr) :- !.
+try_factorize_in_let(Expr,NExpr) :-
+ (cgiveInstancePath(let(_,_),Expr,_) ->
+ % a priori déjà fait
+ NExpr = Expr
+ ; try_factorize_in_let1(Expr,NExpr)).
+
+try_factorize_in_let1(Expr,NExpr) :-
+ (find_mult_occ_compound_subterm(Expr,ST,LP) ->
+ %call(spy_here)@eclipse,
+ new_let_var(VId),
+ (ST = as(_,Type) ->
+ TVId = as(VId,Type)
+ ; TVId = VId),
+ (foreach(P,LP),
+ fromto(Expr,IE,OE,Expr1),
+ param(TVId) do
+ creplace_at_path_in_term(P,IE,TVId,OE)),
+ NExpr = let([(VId,ST)],NExpr1),
+ try_factorize_in_let1(Expr1,NExpr1)
+ ; NExpr = Expr).
+
+find_mult_occ_compound_subterm(Expr,ST,LP) :-
+ my_subterm(Expr,ST),
+ compound(ST),
+ (ST = as(SST,_) ->
+ compound(SST)
+ ; SST = ST),
+ functor(SST,FST,_),
+ FST \== 'Array',
+ FST \== '.',
+ (FST == '_' ->
+ arg(1,SST,T),
+ not member(T,['BitVec','FloatingPoint'])
+ ; true),
+ findall(P,cgiveInstancePath(ST,Expr,P),LP),
+ LP = [_,_|_].
+new_let_var(VId) :-
+ % Pas de collision possible avec les id smt_lib
+ set_var_name(V,"ColId"),
+ get_var_name(V,SVId),
+ concat_string(["\"",SVId,"\""],Str),
+ atom_string(VId,Str).
smt_interp(Expr,IExpr,Type) :-
(check_seen_expr(Expr,IExpr,Type) ->
@@ -1810,8 +1854,10 @@ smt_interp0('define-fun'(F,TypedVars,Sort,Expr),Decl,bool) :- !,
; (match_isObvious(Expr,Arg) ->
smt_interp(Arg,IArg,VType),
IExpr = isFinite(IArg) and neg(isSubnormal(IArg))
- ; smt_interp(Expr,IExpr,Type)))
- ; smt_interp(Expr,IExpr,Type)),
+ ; try_factorize_in_let(Expr,NExpr),
+ smt_interp(NExpr,IExpr,Type)))
+ ; try_factorize_in_let(Expr,NExpr),
+ smt_interp(Expr,IExpr,Type)),
setval(seen_expr,OSE),
reset_let_vars,
Decl = true,
@@ -1823,7 +1869,6 @@ smt_interp0('define-fun'(F,TypedVars,Sort,Expr),Decl,bool) :- !,
add_binding(F,Type,Res)
; define_smt_func(F,TypedArgs,Type,IExpr))).
-
smt_interp0('define-const'(F,Sort,Expr),Decl,bool) :- !,
reset_let_vars,
smt_interp0('declare-var'(F,Sort),Decl0,bool),
diff --git a/Src/COLIBRI/solve.pl b/Src/COLIBRI/solve.pl
index e57447fa5..55efe8da6 100644
--- a/Src/COLIBRI/solve.pl
+++ b/Src/COLIBRI/solve.pl
@@ -3321,7 +3321,7 @@ unfold_int_expr(uninterp(Term),D,Cstr,Type,R) ?- !,
!,
%int_vars(Type,R),
insert_dep_inst(dep(R,D,IArgs)),
- make_conj(ACstrs,(int_vars(Type,R),uninterp_trigger(F,Types,Type,Trigger),uninterp(F,Trigger,IArgs,R)),Cstr).
+ make_conj(ACstrs,(int_vars(Type,R),uninterp_trigger(F,Types,Type,Trigger),uninterp(F,Trigger,Types,Type,IArgs,R)),Cstr).
unfold_int_expr(Val,D,Cstr,Type,R) :-
atomic(Val),
@@ -4803,12 +4803,12 @@ diff_array(Type,A,const_array(TI,TE,Const)) ?- !,
diff_array(Type,A,B) :-
get_priority(P),
set_priority(1),
+ Type = array(TI,TE),
(getval(check_sat_vars,1)@eclipse ->
% Il existe un indice commun ou les elements sont non
% unifiables
- check_diff_array(A,B)
- ; Type = array(TI,TE),
- (real_type(TI,_) ->
+ check_diff_array(TE,A,B)
+ ; (real_type(TI,_) ->
real_vars(TI,I)
; % ok pour les "sort" aussi
int_vars(TI,I)),
@@ -5129,9 +5129,9 @@ remove_common_stores0(storec(A,IA,v(_,EA,CEA)),SureA,SureB,NA) :-
-check_diff_array(const_array(_,_,CA),const_array(_,_,CB)) ?- !,
+check_diff_array(_,const_array(_,_,CA),const_array(_,_,CB)) ?- !,
not_unify(CA,CB).
-check_diff_array(const_array(_,_,Const),A) ?- !,
+check_diff_array(TE,const_array(_,_,Const),A) ?- !,
hash_create(HA),
clean_array(A,NA,(HA,[]),SureA),
SureA = (_,LA),
@@ -5139,10 +5139,12 @@ check_diff_array(const_array(_,_,Const),A) ?- !,
once ((member(I,GIAs);
member((I,_),LA)),
get_sure_index(SureA,I,EA),
- not_unify(EA,Const)).
-check_diff_array(A,const_array(_,_,Const)) ?- !,
- check_diff_array(const_array(_,_,Const),A).
-check_diff_array(A,B) :-
+ (TE = array(_,TEE) ->
+ check_diff_array(TEE,EA,Const)
+ ; not_unify(EA,Const))).
+check_diff_array(TE,A,const_array(_,_,Const)) ?- !,
+ check_diff_array(TE,const_array(_,_,Const),A).
+check_diff_array(TE,A,B) :-
hash_create(HA),
hash_create(HB),
clean_array(A,NA,(HA,[]),SureA),
@@ -5153,7 +5155,9 @@ check_diff_array(A,B) :-
member((I,_),LA)),
get_sure_index(SureA,I,EA),
get_sure_index(SureB,I,EB),
- not_unify(EA,EB)).
+ (TE = array(_,TEE) ->
+ check_diff_array(TEE,EA,EB)
+ ; not_unify(EA,EB))).
@@ -6924,7 +6928,7 @@ unfold_real_expr(EA * EB,D,Cstr,Type,R) ?-
(real_type(Type,real) ->
make_conj(CAB,mult_real(real,A,B,R),Cstr)
; make_conj(CAB,(ensure_not_NaN((A,B,R)),mult_real(Type,A,B,R)),Cstr)).
-unfold_real_expr(fp_mul(EA,EB),D,Cstr,Type,R) ?-
+unfold_real_expr(fp_mul(EA,EB),D,Cstr,Type,R) ?- !,
unfold_real_expr(fp_mul(rne,EA,EB),D,Cstr,Type,R).
unfold_real_expr(fp_mul(Rnd0,EA,EB),D,Cstr,Type,R) ?-
ND is D + 1,
@@ -7526,7 +7530,7 @@ unfold_real_expr(uninterp(Term),D,Cstr,Type,R) ?- !,
make_conj(IC,(SetType,AC),OC)),
!,
insert_dep_inst(dep(R,D,IArgs)),
- make_conj(ACstrs,(real_vars(Type,R),uninterp_trigger(F,Types,Type,Trigger),uninterp(F,Trigger,IArgs,R)),Cstr).
+ make_conj(ACstrs,(real_vars(Type,R),uninterp_trigger(F,Types,Type,Trigger),uninterp(F,Trigger,Types,Type,IArgs,R)),Cstr).
unfold_real_expr(Expr,_,_,_,_) :-
spy_here,
@@ -9689,7 +9693,7 @@ uninterp_trigger(F,Types0,Type0,Trigger) :-
concat_string([SFTerm,":",SType],STrigger)),
atom_string(Trigger,STrigger).
-uninterp(F,Trigger,Args,R) :-
+uninterp(F,Trigger,TypeArgs,TypeR,Args,R) :-
get_priority(P),
set_priority(1),
save_cstr_suspensions((Args,R)),
@@ -9698,39 +9702,41 @@ uninterp(F,Trigger,Args,R) :-
attached_suspensions(Trigger,LSusp1),
append(LSusp0,LSusp1,LSusp),
(foreach(PairOrSusp,LSusp),
- param(F,Args,R,TypeR) do
+ param(F,Args,R,TypeArgs,TypeR) do
(PairOrSusp = (Susp,Goal) ->
true
; Susp = PairOrSusp,
(get_suspension_data(Susp,goal,Goal) ->
true
; Goal = dead)),
- (Goal = uninterp(F,Trigger,CArgs,CR) ->
+ (Goal = uninterp(F,Trigger,TypeArgs,TypeR,CArgs,CR) ->
(Args == CArgs ->
% factorisation
kill_suspension(Susp),
- protected_unify(R,CR)
- ; ((not_unify(R,CR),
- only_one_neq_args_pair(Args,CArgs,A,CA))
+ (TypeR = array(_,_) ->
+ call(spy_here)@eclipse,
+ eq_array(TypeR,R,CR)
+ ; protected_unify(R,CR))
+ ; (((TypeR = array(_,TE) ->
+ check_diff_array(TE,R,CR)
+ ; not_unify(R,CR)),
+ only_one_neq_args_pair(TypeArgs,Args,CArgs,TA,A,CA))
->
- (term_variables((A,CA),[V|_]) ->
- (get_type(V,T) ->
- diff_reif(T,Kill,A,CA,1)
- ; launch_delta(A,CA,#,-1..1))
- ; % A <> CA
- true)
+ diff_reif(TA,Kill,A,CA,1)
; true))
; true)),
(ground(Args) ->
- my_suspend(uninterp(F,Trigger,Args,R),0,trigger(Trigger))
- ; my_suspend(uninterp(F,Trigger,Args,R),0,(Args,R)->suspend:constrained)),
+ my_suspend(uninterp(F,Trigger,TypeArgs,TypeR,Args,R),0,trigger(Trigger))
+ ; my_suspend(uninterp(F,Trigger,TypeArgs,TypeR,Args,R),0,(Args,R)->suspend:constrained)),
set_priority(P),
wake_if_other_scheduled(P).
-only_one_neq_args_pair([A1|Args],[CA1|CArgs],A,CA) :-
+only_one_neq_args_pair([T|TArgs],[A1|Args],[CA1|CArgs],TA,A,CA) :-
(A1 == CA1 ->
- only_one_neq_args_pair(Args,CArgs,A,CA)
- ; Args == CArgs,
+ only_one_neq_args_pair(TArgs,Args,CArgs,TA,A,CA)
+ ; % T \= array(_,_), % meme dans ce cas
+ Args == CArgs,
+ TA = T,
A = A1,
CA = CA1).
@@ -9761,7 +9767,7 @@ chk_undef_div_real(Bool,A,B,R) :-
wake_if_other_scheduled(P).
undef_div_real(A,R) :-
- uninterp(div_real,div_real,[A],R).
+ uninterp(div_real,div_real,[real],real,[A],R).
chk_undef_idiv_real(Bool,Type,A,B,R) :-
get_priority(P),
@@ -9797,7 +9803,7 @@ undef_idiv_real(Type,A,R) :-
launch_float_int_number(A),
launch_float_int_number(R),
uninterp_trigger(idiv_real,[Type],Type,Trigger),
- uninterp(idiv_real,Trigger,[A],R).
+ uninterp(idiv_real,Trigger,[Type],Type,[A],R).
chk_undef_imod_real(Bool,Type,A,B,R) :-
get_priority(P),
@@ -9833,8 +9839,8 @@ undef_imod_real(Type,A,R) :-
real_vars(real,(A,R)),
launch_float_int_number(A),
launch_float_int_number(R),
- uninterp_trigger(imod_real,[Type],type,Trigger),
- uninterp(imod_real,Type,[A],R).
+ uninterp_trigger(imod_real,[Type],Type,Trigger),
+ uninterp(imod_real,Type,[Type],Type,[A],R).
chk_undef_float_to_real(Bool,TypeF,A,R) :-
set_lazy_domain(real,R),
@@ -9862,7 +9868,7 @@ chk_undef_float_to_real(Bool,TypeF,A,R) :-
undef_float_to_real(Type,A,R) :-
uninterp_trigger(float_to_real,[Type],real,Trigger),
- uninterp(float_to_real,Trigger,[Type,A],R).
+ uninterp(float_to_real,Trigger,[Type],real,[A],R).
/*
undef_float_to_real(Type,A,R) :-
get_priority(Prio),
@@ -9905,7 +9911,7 @@ chk_undef_float_to_ubv(Bool,TypeF,Size,A,R) :-
(Bool,A)->suspend:constrained))).
undef_float_to_ubv(Type,Size,A,R) :-
uninterp_trigger(float_to_ubv,[Type],uint(Size),Trigger),
- uninterp(float_to_ubv,Trigger,[A],R).
+ uninterp(float_to_ubv,Trigger,[Type],uint(Size),[A],R).
/*
undef_float_to_ubv(Type,Size,A,R) :-
get_priority(Prio),
@@ -9952,7 +9958,7 @@ chk_undef_float_to_sbv(Bool,TypeF,Size,A,R) :-
undef_float_to_sbv(Type,Size,A,R) :-
uninterp_trigger(float_to_sbv,[Type],uint(Size),Trigger),
- uninterp(float_to_sbv,Trigger,[A],R).
+ uninterp(float_to_sbv,Trigger,[Type],uint(Size),[A],R).
/*
undef_float_to_sbv(Type,Size,A,R) :-
get_priority(Prio),
@@ -10012,7 +10018,7 @@ chk_undef_ediv_mod(Bool,Type,A,B,Q,R) :-
undef_ediv_mod(int,A,Q,R) :- !,
uninterp_trigger(smt_ediv_mod_int,[int],int,Trigger),
- uninterp(smt_ediv_mod_int,Trigger,[A],(Q,R)).
+ uninterp(smt_ediv_mod_int,Trigger,[int],int,[A],(Q,R)).
undef_ediv_mod(Type,A,Q,R) :-
arg(1,Type,N),
All1 is 2^N-1,
@@ -10178,7 +10184,7 @@ chk_undef_div_rem(Bool,Type,A,B,Q,R,UO) :-
(Bool,A,B)->suspend:constrained))).
undef_div_rem(int,A,Q,R,UO) :- !,
uninterp_trigger(div_rem_int,[int],int,Trigger),
- uninterp(div_rem_int,Trigger,[A],(Q,R)).
+ uninterp(div_rem_int,Trigger,[int],int,[A],(Q,R)).
undef_div_rem(Type,A,Q,R,UO) :-
% uint(N)
% Q = 0
@@ -10225,7 +10231,7 @@ chk_undef_cdiv_crem(Bool,A,B,Q,R) :-
undef_cdiv_crem(A,Q,R) :-
uninterp_trigger(cdiv_crem,[real],real,Trigger),
- uninterp(cdiv_crem,Trigger,[A],(Q,R)).
+ uninterp(cdiv_crem,Trigger,[real],real,[A],(Q,R)).
cdiv_crem(A,B,Q,R) :-
@@ -11140,7 +11146,14 @@ get_most_constrained_bool_var([(V,D,Adj)|UseList],VN,NUseList,Seen,OVar,ONb,Var,
get_type(E,Type),
(Type == int ->
mfd:get_intervals(E,[0,1])
- ; Type == rnd),
+ ; (Type == rnd ->
+ true
+ ; % A ANALYSER/GENERALISER AUX AUTRES TYPES
+ % Bon sur ramalho +1
+ % Mauvais sur griggio -2
+ real_type(Type,_),
+ mreal:dvar_size(E,2),
+ call(spy_here)@eclipse)),
not occurs(E,ISeen))
->
(get_var_name(E,_) ->
@@ -12500,3 +12513,13 @@ smt_check_disabled_delta :-
; true)
; true).
+
+% pour énumérer les sous termes de T
+my_subterm(T,ST) :-
+ my_subterm_list([T],ST).
+my_subterm_list([T|L],ST) :-
+ (ST = T;
+ compound(T),
+ T =.. [_|LT],
+ (my_subterm_list(LT,ST);
+ my_subterm_list(L,ST))).
\ No newline at end of file
--
GitLab