From 5fd696afdd49b90e0d0ed1c27688c7ab9c0346de Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Wed, 1 Jun 2022 21:21:07 +0200
Subject: [PATCH] Import from Bin:a1af7a0 Src:9fd72416b farith:a93db57
---
Src/COLIBRI/col_solve.pl | 26 +++++++++++++++++++-------
Src/COLIBRI/smt_import.pl | 12 +++---------
Src/COLIBRI/solve.pl | 12 +++++++-----
3 files changed, 29 insertions(+), 21 deletions(-)
diff --git a/Src/COLIBRI/col_solve.pl b/Src/COLIBRI/col_solve.pl
index c10b11cb1..1676ba9db 100644
--- a/Src/COLIBRI/col_solve.pl
+++ b/Src/COLIBRI/col_solve.pl
@@ -830,7 +830,7 @@ smt_test(TO,Size,CI) :-
%StrDir = "./colibri_tests/colibri/tests/",
%StrDir = "./colibri_tests/colibri/tests/sat/",
% 0 en 20s (sans real/float->int!)
- %StrDir = "./colibri_tests/colibri/tests/unsat/", %0
+ StrDir = "./colibri_tests/colibri/tests/unsat/", %0
%StrDir = "./colibri_tests/colibri/tests/unknown/",
%StrDir = "./colibri_tests/colibri/tests/timeout/",
@@ -1014,7 +1014,7 @@ smt_test(TO,Size,CI) :-
%StrDir = "./QF_FP/20170501-Heizmann-UltimateAutomizer/", % 0
%StrDir = "./QF_FP/20190429-UltimateAutomizerSvcomp2019/",% 0 (bitwuzla 0)
%StrDir = "./QF_FP/ramalho/", % 1 (cvc4 19)(bitwuzla 17)
- StrDir = "./QF_FP/griggio/", % 52/214 (min_solve, sans lin_solve ni ls_reduce..)(39)
+ %StrDir = "./QF_FP/griggio/", % 52/214 (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
@@ -1684,6 +1684,7 @@ smt_unit_test(StrDir0,TO,CI) :-
getval(init_code,Code),
incNbCode(Code),
+ getval(smt_status,Status)@eclipse,
(Code == 2 ->
((CI == 1,
getval(make_UT,0)@eclipse)
@@ -1693,13 +1694,24 @@ smt_unit_test(StrDir0,TO,CI) :-
exit(4)
; true),
getval(bug,Bugs),
- (getval(smt_status,unknown)@eclipse ->
+ (Status == unknown ->
setval(bug,[smt_unknown:F|Bugs])
; setval(bug,[F|Bugs]))
- ; (Code == 3 ->
- incval(nbTO)
- ; pathname(F,PF,NF),
- (Code > 2 ->
+ ; pathname(F,PF,NF),
+ (Code == 3 ->
+ incval(nbTO),
+ ((CI == 1,
+ getval(make_UT,0)@eclipse)
+ ->
+ true
+ ; % on supprime le TO de UnitTests
+ concat_string(["UnitTests/",Status,"/",Logic,"/",NF],
+ TargetFile),
+ (exists(TargetFile) ->
+ concat_string(["rm ",TargetFile],Rm),
+ system(Rm)
+ ; true))
+ ; (Code > 2 ->
true
; (Code == 0 ->
concat_string(["UnitTests/unsat/",Logic,"/"],TargetDir)
diff --git a/Src/COLIBRI/smt_import.pl b/Src/COLIBRI/smt_import.pl
index a41b9b0af..4dad14dc0 100644
--- a/Src/COLIBRI/smt_import.pl
+++ b/Src/COLIBRI/smt_import.pl
@@ -1005,7 +1005,7 @@ dump_type_val(real,Val0,Val) ?- !,
dump_type_val('Real',Val0,Val).
dump_type_val('Real',Val0,NVal) ?- !,
(var(Val0) ->
- (known_real_box(Val0,SNum,SDenN,Neg) ->
+ (known_real_box(Val0,SNum,SDen,Neg) ->
(SDen == "1" ->
concat_string([SNum,".0"],Val)
; concat_string(["(/ ",SNum,".0 ",SDen,".0)"],Val))
@@ -1094,7 +1094,8 @@ dump_type_val(OType,Val,SVal) :-
term_string(TVal,STVal),
TVal =.. [':',Type,Cpt],
build_end_val_from_old_type(OType,SEndVal),
- concat_string(["|val",Cpt,":",SEndVal,"|"],SVal).
+% concat_string(["|val",Cpt,":",SEndVal,"|"],SVal).
+ concat_string(["(as @uc_",SEndVal,"_",Cpt," ",SEndVal,")"],SVal).
build_end_val_from_old_type([],[]) :- !.
build_end_val_from_old_type([OType|OTypes],[NType|NTypes]) :- !,
@@ -1184,13 +1185,6 @@ dump_smt_model(Vars) :-
getval(sorts,HSorts),
getval(declared_funs,DFs-[]),
writeln(output,"(model"),
- (HSorts == 0 ->
- true
- ; hash_list(HSorts,Ks,Vs),
- (foreach(Sort,Ks),
- foreach((Ar,SortVals),Vs) do
- concat_string([" (declare-sort ",Sort," ",Ar,")"],Ds),
- writeln(output,Ds))),
(foreach((VN,InSorts,OutSort),DFs),
fromto([],IU,OU,Uninterps),
fromto(Vars,InVars,OutVars,NVars) do
diff --git a/Src/COLIBRI/solve.pl b/Src/COLIBRI/solve.pl
index 0c1f3f87c..f884918f7 100644
--- a/Src/COLIBRI/solve.pl
+++ b/Src/COLIBRI/solve.pl
@@ -12554,11 +12554,13 @@ occurs_in_comp(Var,Comp) :-
member(Comp,Goals),
functor(Comp,FComp,_),
occurs(FComp,(gt_real,diff_real)),
- Comp =.. [_,X,Y],
- mreal:dvar_range(X,LX,HX),
- (LX,HX) \== (-1.0Inf,1.0Inf),
- mreal:dvar_range(Y,LY,HY),
- (LY,HY) \== (-1.0Inf,1.0Inf).
+ Comp =.. [_,_,X,Y],
+ (Y == Var ->
+ mreal:dvar_range(X,LX,HX),
+ (LX,HX) \== (-1.0Inf,1.0Inf)
+ ; % X == Var
+ mreal:dvar_range(Y,LY,HY),
+ (LY,HY) \== (-1.0Inf,1.0Inf)).
try_rat_satisfying_comp(gt_real(_,X,Y),Var,Rat) :-
(X == Var ->
--
GitLab