-
François Bobot authoredFrançois Bobot authored
col_solve.pl 52.20 KiB
:- pragma(nowarnings).
%% Rend le compilateur silencieux
:- set_event_handler(139,true/0).
%% Warning "deprecated"
:- set_event_handler(75,true/0).
%% Warning "declared but not defined"
:- set_event_handler(76,true/0).
%% Warning "used but not declared"
:- set_event_handler(77,true/0).
%% Warning "referring to non-exported predicate"
:- set_event_handler(84,true/0).
%% Warning "already reexported"
:- set_event_handler(90,true/0).
%:- set_flag(variable_names,off).
:- lib(lists).
:- lib(timeout).
:- include(colibri).
%% On doit refaire les set_handler apres le chargement de colibri
%% Rend le compilateur silencieux
:- set_event_handler(139,true/0).
%% Warning "deprecated"
:- set_event_handler(75,true/0).
%% Warning "declared but not defined"
:- set_event_handler(76,true/0).
%% Warning "used but not declared"
:- set_event_handler(77,true/0).
%% Warning "referring to non-exported predicate"
:- set_event_handler(84,true/0).
%% Warning "already reexported"
:- set_event_handler(90,true/0).
:- module(eclipse).
:- import(colibri).
?- start_colibri.
?- setval(float_eval,float_double).
% mode nodebug.
?- setval(gdbg,0).
?- setval(threshold,1e-3).
/*
?- % Pour reduire la frequence des gc
% et gagner du temps
get_flag(max_global_trail,MGT),
% la valeur par defaut est max_global_trail/32
GCInter is fix(MGT/2),
set_flag(gc_interval,GCInter),
set_flag(gc_interval_dict,10000000).
*/
:- local reference(constraints).
:- local reference(from_pu).
:- no_3B.
:- setval(solve,1).
:- setval(time_limit,0).
no_solve :-
setval(solve,0).
set_timeout(T) :-
((integer(T),
T >= 0) ->
setval(time_limit,T)
; writeln(output,"Expecting timeout integer value > 0."),
exit_block(syntax)).
get_version(Num) :-
system("svn info --show-item revision > revision"),
open(revision,read,Stream),
read_string(Stream,"\n\r",_,Str),
close(Stream),
system("rm revision"),
split_string(Str,":"," ",[_,Num]).
set_version :-
get_version(Num),
assert(colibri_version(Num)).
show_version :-
colibri_version(Num),
writeln(output,Num).
interactive_solve :-
% set_flag(variable_names,on),
repeat,
garbage_collect,
write(output,[colibri]:""),
block(read(input,Goal),
Tag,
(writeln(error,exit(Tag)),
fail)),
((Goal == halt;
Goal == end_of_file)
->
!
; no_3B,
use_delta,
set_threshold(1e-3),
term_variables(Goal,Vars),
(foreach(Var,Vars),
foreach((SVar,Var),Bindings) do
open(string(""),write,Stream),
write(Stream,Var),
get_stream_info(Stream,name,SVar),
close(Stream)),
(cgiveInstancePath(solve_cstrs,Goal,Path) ->
creplace_at_path_in_term(Path,Goal,(type_bindings(Test,
Bindings,
NBindings),
solve_cstrs)),
Solve = 1,
NGoal = Goal
; NGoal = (Goal,type_bindings(Test,Bindings,NBindings))),
block((call(NGoal) ->
(nonvar(Solve) ->
nl(output),
writeln(output,'SAT'),
nl(output),
dump_binding(Test,NBindings)
; (current_suspension(_) ->
true
; nl(output),
writeln(output,'SAT'),
SAT = 1),
(nonvar(SAT) ->
nl(output),
dump_binding(Test,NBindings)
; get_goals(LSusp,LinSusps,Goals),
term_variables(Bindings,ProtectedVars),
fold_goals(Goals,Goals,ProtectedVars,NewGoals), term_variables(NewGoals,GVars0),
(foreach(GVar0,GVars0),
fromto([],I,O,GVars),
param(NBindings) do
(occurs(GVar0,NBindings) ->
O = I
; O = [GVar0|I])),
(foreach(GVar,GVars),
foreach((GSVar,GVar),GBindings) do
open(string(""),write,Stream),
write_term(Stream,GVar,
[attributes(none)]),
get_stream_info(Stream,name,GSVar),
close(Stream)),
type_bindings(Test,GBindings,NGBindings),
nl(output),
dump_binding(Test,NBindings),
dump_binding(Test,NGBindings),
nl(output),
writeln(output,'CONSTRAINTS:'),
(foreach(TGoal,NewGoals) do
write_term(output,TGoal,
[as(goal),depth(full),
attributes(none)]),
nl(output))))
; nl(output),
writeln(output,'UNSAT')),
Tag,
writeln(error,exit(Tag))),
fail).
get_goals([],_,[]).
get_goals([Susp|LSusp],LinSusps,Goals) :-
(member(Susp,LinSusps) ->
Goals = EGoals
; get_suspension_data(Susp,goal,Goal),
(trans_col(Goal,TGoal) ->
(TGoal = "" ->
Goals = EGoals
; Goals = [TGoal|EGoals])
; Goals = [Goal|EGoals])),
get_goals(LSusp,LinSusps,EGoals).
fold_goals(Goals,OGoals,ProtectedVars,NewGoals) :-
fold_goals0(Goals,OGoals,ProtectedVars,NGoals),
sort(NGoals,SGoals),
trivial_goal_elim(SGoals,NewGoals).
fold_goals0([],Gs,_,Gs).
fold_goals0([Goal|Goals],OGoals,ProtectedVars,NewGoals) :-
fold_goal(Goal,OGoals,ProtectedVars,NGoals),
fold_goals0(Goals,NGoals,ProtectedVars,NewGoals).
fold_goal(Goal,OGoals,ProtectedVars,NGoals) :-
((compound(Goal),
Goal =.. [F,E,V],
occurs(F,(#=,$=)))
->
((var(V),
not occurs(V,E),
not occurs(V,ProtectedVars))
->
findall(Path,cgiveVarInstancePath(V,OGoals,[],Path),Paths),
(foreach(Path,Paths),
param(OGoals,E) do
creplace_at_path_in_term(Path,OGoals,E)),
NGoals = OGoals
; ((Goal = (A + B #= V),
(Var = A, Other = B; Var = B, Other = A),
var(Var), not occurs(Var,ProtectedVars))
->
once (member_begin_end(CGoal,OGoals,NGoals,End,End),
Goal == CGoal),
findall(Path,cgiveVarInstancePath(Var,NGoals,[],Path),
Paths),
NE = (V-Other),
(foreach(Path,Paths),
param(NGoals,NE) do
creplace_at_path_in_term(Path,NGoals,NE))
; NGoals = OGoals))
; NGoals = OGoals).
trivial_goal_elim([],[]).
trivial_goal_elim([Goal|Goals],NewGoals) :-
((compound(Goal),
Goal =.. [F,E1,E2],
E1 == E2)
->
(occurs(F,(#=,#>=,$=,$>=)) ->
NewGoals = ENewGoals
; (occurs(F,(#\=,#<,#>,($\=,$<,$>))) ->
nl(output),
writeln(output,'UNSAT'),
fail
; NewGoals = [Goal|ENewGoals]))
; NewGoals = [Goal|ENewGoals]),
trivial_goal_elim(Goals,ENewGoals).
solve(FILE) :-
solve(_,FILE,0,Code),
exit(Code).
solve(Test,FILE,TO,Code) :-
setval(solve,1),
set_flag(variable_names,on),
no_3B,
use_delta,
%no_simplex,
%use_simplex par defaut
%no_approx,
%use_approx par_defaut
set_threshold(1e-3),
set_timeout_handler,
set_timeout(TO),
((exists(FILE),
get_file_info(FILE, readable, on))
->
true
; concat_string(["Cannot read input file ",FILE],Mess),
writeln(error,Mess),
Code = 2),
(nonvar(Code) ->
true
; open(FILE,read,S),
block((read(S,Goal) ->
true
; exit_block(syntax)),
TagRead,
(writeln(error,'ERROR'(FILE):TagRead),
Code = 2)),
close(S)),
(nonvar(Code) ->
true
; term_variables(Goal,Vars),
(foreach(Var,Vars), foreach((SVar,Var),Bindings) do
open(string(""),write,Stream),
write(Stream,Var),
get_stream_info(Stream,name,SVar),
close(Stream)),
(occurs(solve_cstrs,Goal) ->
% on le retire du but
findall(Path,cgiveInstancePath(solve_cstrs,Goal,Path),Paths),
(foreach(Path,Paths),
param(Goal) do
creplace_at_path_in_term(Path,Goal,true))
; true),
(occurs(no_solve,Goal) ->
% no_solve prioritaire a solve_cstrs
setval(solve,0)
; setval(solve,1)),
block((getval(solve,0) ->
% les or, and ... ne sont pas transformes
% en ",", ";" ...
(call(Goal) ->
(current_suspension(_) ->
writeln(output,'UNKNOWN':no_solve),
Code = 3
; Code = 1,
writeln(output,'SAT'),
SAT = 1),
(nonvar(Test) ->
true
; (nonvar(SAT) ->
dump_binding(Test,NBindings)
; get_goals(LSusp,LinSusps,Goals),
term_variables(Bindings,ProtectedVars),
fold_goals(Goals,Goals,ProtectedVars,NewGoals),
term_variables(NewGoals,GVars0),
(foreach(GVar0,GVars0),
fromto([],I,O,GVars),
param(NBindings) do
(occurs(GVar0,NBindings) ->
O = I
; O = [GVar0|I])),
(foreach(GVar,GVars),
foreach((GSVar,GVar),GBindings) do
open(string(""),write,Stream),
write_term(Stream,GVar,
[attributes(none)]),
get_stream_info(Stream,name,GSVar),
close(Stream)),
type_bindings(Test,GBindings,NGBindings),
dump_binding(Test,NBindings),
dump_binding(Test,NGBindings),
nl(output),
writeln(output,'CONSTRAINTS:'),
(foreach(TGoal,NewGoals) do
write_term(output,TGoal,
[as(goal),depth(full),
attributes(none)]),
nl(output))))
; writeln(output,'UNSAT'),
Code = 0)
; getval(time_limit,Timeout),
alarm(Timeout),
((call(Goal),
type_bindings(Test,Bindings,NBindings),
solve_cstrs)
->
alarm(0),
writeln(output,'SAT'),
(nonvar(Test) ->
true
; nl(output), dump_binding(Test,NBindings)),
Code = 1
; alarm(0),
writeln(output,'UNSAT'),
Code = 0)),
Tag,
(Tag == timeout_col ->
writeln(output,'UNKNOWN':timeout),
Code = 3
; writeln(error,'ERROR'(FILE):Tag),
Code = 2))).
type_bindings(1,_,_) ?- !.
type_bindings(Test,Bindings,NBindings) :-
(foreach((SVar,Var),Bindings),
foreach((SVar,Type,Var),NBindings) do
get_type(Var,Type)).
dump_binding(1,_) ?- !.
dump_binding(Test,Bindings) :-
set_flag(print_depth,1000),
(foreach((SVar,Type,Val0),Bindings) do
(var(Val0) ->
(Type == int ->
mfd:get_intervals(Val0,Val)
; mreal:get_intervals(Val0,LI),
(Type == float_simple ->
(foreach(I,LI),
foreach(NI,Val) do
(I = L..H ->
simple_float_to_string(L,SL),
simple_float_to_string(H,SH),
NI = SL..SH
; simple_float_to_string(I,NI)))
; ((Type == real,
check_rbox_rat(Val0,Rat))
->
term_string(Rat,SRat),
term_string(realString(SRat),Val)
; term_string(LI,Val))))
; (Type == float_simple ->
simple_float_to_string(Val0,Val)
; Val = Val0)),
writeln(output,SVar = Val)).
test_colibri :-
setval(bug,[]),
os_file_name("./Examples",OS_Examples),
read_directory(OS_Examples,"*",SubdirList,_),
(foreach(Dir,SubdirList),
fromto([],IS,OS,SatFileList),
fromto([],IU,OU,UnsatFileList),
fromto([],IUk,OUk,UnknownFileList) do
append_strings("./Examples/",Dir,SubDir),
os_file_name(SubDir,OS_SubDir),
read_directory(OS_SubDir, "*_unsat", _, UnsatList0),
(foreach(U,UnsatList0),
foreach(SU,UnsatList),
param(Dir) do
concat_string(["./Examples/",Dir,"/",U],SU0),
os_file_name(SU0,SU)),
read_directory(SubDir, "*_sat", _, SatList0),
(foreach(S,SatList0),
foreach(SS,SatList),
param(Dir) do
concat_string(["./Examples/",Dir,"/",S],SS0),
os_file_name(SS0,SS)),
read_directory(SubDir, "*_unknown", _, UnknownList0),
(foreach(Uk,UnknownList0), foreach(SUk,UnknownList),
param(Dir) do
concat_string(["./Examples/",Dir,"/",Uk],SUk0),
os_file_name(SUk0,SUk)),
append(SatList,IS,OS),
append(UnsatList,IU,OU),
append(UnknownList,IUk,OUk)),
( member((List,Code0),[(SatFileList,1),(UnsatFileList,0),
(UnknownFileList,3)]),
member(F,List),
writeln(output,F),
%seed(0),
solve(1,F,6,Code),
(Code \== Code0 ->
writeln(output,ko:Code),
getval(bug,Bugs),
setval(bug,[F:Code|Bugs])
; writeln(output,ok)),
fail
; true),
getval(bug,Bugs),
(Bugs == [] ->
true
; nl(output),
writeln(output,"BUGS:"),
(foreach(B,Bugs) do
writeln(output,B))),
getval(cpt_solve,NbS)@colibri,
writeln(output,"NbSimplex":NbS).
smt_solve_get_stat(FILE) :-
% On passe en mode comptage du nombre de steps
setval(step_stats,1)@eclipse,
% Si on a une limite elle est donnée dans la ligne de commande
(current_array(step_limit,_) ->
true
; setval(step_limit,0)@eclipse),
setval(nb_steps,0)@eclipse,
setval(simplex_steps,0)@eclipse,
smt_solve(_,FILE,0,Code),
(getval(show_steps,1)@eclipse ->
getval(nb_steps,Steps)@eclipse,
writeln(output,"Steps":Steps)
; true),
exit(Code).
smt_solve_with_step_limit(FILE) :-
% On passe en mode comptage du nombre de steps
setval(step_stats,1)@eclipse,
setval(show_steps,1)@eclipse,
% Si on a une limite elle est donnée dans la ligne de commande
(current_array(step_limit,_) ->
true
; setval(step_limit,0)@eclipse),
setval(nb_steps,0)@eclipse,
setval(simplex_steps,0)@eclipse,
smt_solve(_,FILE,0,Code),
exit(Code).
smt_solve_count_steps(FILE,TO) :-
setval(show_steps,1)@eclipse,
getval(use_delta,UD)@eclipse,
getval(use_simplex,US)@eclipse,
% On passe en mode comptage du nombre de steps
setval(step_stats,1)@eclipse,
% Si on a une limite elle est donnée dans la ligne de commande
(current_array(step_limit,_) ->
true
; setval(step_limit,0)@eclipse), setval(nb_steps,0)@eclipse,
setval(simplex_steps,0)@eclipse,
block((smt_solve(_,FILE,TO,Code) ->
true
; setval(use_delta,UD)@eclipse,
setval(use_simplex,US)@eclipse,
fail),
Tag,
(writeln(output,exit(Tag)),
setval(use_delta,UD)@eclipse,
setval(use_simplex,US)@eclipse,
exit_block(Tag))),
setval(use_delta,UD)@eclipse,
setval(use_simplex,US)@eclipse.
smt_comp_solve(FILE) :-
% pas de message sur error pour la smtcomp
get_stream(null,Snull),
set_stream(error,Snull),
% on compte les steps pour desactiver deltas/simplex
setval(step_stats,1)@eclipse,
setval(step_limit,0)@eclipse,
setval(nb_steps,0)@eclipse,
setval(simplex_steps,0)@eclipse,
% on desactive les warning de dolmen
setval(no_dolmen_warning,1)@eclipse,
smt_solve(_,FILE,0,Code),
exit(Code).
smt_solve(FILE) :-
setval(step_stats,0)@eclipse,
setval(step_limit,0)@eclipse,
setval(nb_steps,0)@eclipse,
setval(simplex_steps,0)@eclipse,
% on active les warning de dolmen
setval(no_dolmen_warning,0)@eclipse,
smt_solve(_,FILE,0,Code),
exit(Code).
smt_solve(Test,FILE,TO,Code) :-
no_3B,
set_threshold(1e-3),
smt_solve_bis(Test,FILE,TO,Code).
smt_solve_bis(Test,FILE,TO,Code) :-
% seed(0),
setval(smt_status,unknown)@eclipse,
setval(nb_steps,0)@eclipse,
setval(simplex_steps,0)@eclipse,
setval(solve,1),
setval(time_limit,0),
%setval(smt_status,0),
(nonvar(Test) ->
setval(scrambler,1)
; setval(scrambler,0)),
setval(diag_code,0),
min_max_lazy(int,MinInt,MaxInt,_),
setval(refutation_chk,0)@eclipse,
setval(logic,"ALL")@eclipse,
% les deltas sont utiles pour les tableaux
% positionné par smt_interp0, lu dans solve.pl
setval(keep_deltas_if_arrays,0)@eclipse,
((exists(FILE),
get_file_info(FILE, readable, on))
->
true
; concat_string(["(error \"Cannot read input file ",FILE,"\")"],Mess), writeln(output,Mess),
writeln(output,unknown),
Code = 2,
setval(diag_code,(unknown,2))),
(nonvar(Code) ->
true
; block((smt_interp_file(FILE,Goal) ->
true
; exit_block(syntax)),
TagRead,
((TagRead == unsupported ->
Code = 5
; concat_string(["(error \"",FILE,":",TagRead,"\")"],Mess),
writeln(output,Mess),
Code = 2),
writeln(output,unknown),
setval(diag_code,(unknown,Code))))),
getval(use_delta,UD)@eclipse,
getval(use_simplex,US)@eclipse,
(nonvar(Code) ->
true
; save_goal_before_check_sat(Goal),
setval(time_limit,TO),
statistics(session_time,Start),
setval(start_solve,Start),
% Essai pour smt_comp : pas de delta/simplex apres DDSteps
getval(simplex_delay_deactivation,DDSteps)@eclipse,
smt_start_enable_delta_check(DDSteps),
((var(Test),
(TO > 0;
DDSteps == 0))
->
smt_disable_delta_check
; smt_enable_delta_check),
block((timeout(not not call(Goal),
TO,
exit_block(timeout_col))
->
getval(diag_code,(Diag,Code))
; % echec a la propagation
(Status == sat ->
Code = 2,
Diag = unknown,
writeln(output,unknown),
writeln(error,"wrong unsat")
; Code = 0,
Diag = unsat,
writeln(output,unsat)),
setval(diag_code,(Diag,Code))),
Tag,
(update_min_max_lazy_int(MinInt,MaxInt),
(Tag == timeout_col ->
(nonvar(Test) ->
writeln(output,'UNKNOWN':timeout)
; true),
Code = 3,
setval(diag_code,(timeout,3))
; (concat_string(["(error \"",FILE,":",Tag,"\")"],Mess),
writeln(error,Mess),
writeln(output,unknown),
Code = 2,
setval(diag_code,(unknown,2))))))),
% Menage
clear_dep_constraints,
setval(use_delta,UD)@eclipse,
setval(use_simplex,US)@eclipse,
update_min_max_lazy_int(MinInt,MaxInt).
:- local reference(gsat).goal_before_check_sat((Beg,G),Goal) ?- !,
(occurs(check_sat,G) ->
(G == check_sat ->
Goal = Beg
; Goal = (Beg,EGoal),
goal_before_check_sat(G,EGoal))
; goal_before_check_sat(Beg,Goal)).
goal_before_check_sat(_,true).
get_type_decl((Beg,End),Decl,Goal) ?- !,
get_type_decl(Beg,BDecl,BGoal),
get_type_decl(End,EDecl,EGoal),
make_conj(BDecl,EDecl,Decl),
append(BGoal,EGoal,Goal).
get_type_decl(D,Decl,Goal) ?-
(is_decl(D) ->
Decl = D,
Goal = []
; Decl = true,
Goal = [D]).
is_decl(int_vars(_,_)) ?- !.
is_decl(bool_vars(_,_)) ?- !.
is_decl(sort_vars(_,_)) ?- !.
is_decl(real_vars(_,_)) ?- !.
is_decl(rnd_vars(_)) ?- !.
is_decl(array_vars(_,_,_)) ?- !.
% pour check_sat_vars
save_goal_before_check_sat(Goal) :-
goal_before_check_sat(Goal,NGoal0),
get_type_decl(NGoal0,Decl,NGoal),
% Les variables de Decl sont attribuees
% par leur type
call(Decl),
% Les CGVars ne contiennent que des variables
% attribuees (donc celles de Decl normalement ?)
copy_term(NGoal,CG,CGVars),
(foreach([V|CV],CGVars),
foreach((V,Type,CV),TCGVars) do
get_variable_type(V,Type)),
setval(gsat,CG-TCGVars).
initNbCodes :-
setval(nbFile,0),
setval(nb0,0),
setval(nb1,0),
setval(nb2,0),
setval(nb3,0),
setval(nb4,0),
setval(nb5,0),
setval(nb6,0).
incNbCode(0) :-
incval(nb0).
incNbCode(1) :-
incval(nb1).
incNbCode(2) :-
incval(nb2).
incNbCode(3) :-
incval(nb3).
incNbCode(4) :-
incval(nb4).
incNbCode(5) :-
incval(nb5).
incNbCode(6) :-
incval(nb6).
smt_solve_test(FILE,TO) :-
seed(0), smt_solve_test_bis(FILE,TO,Code),
exit(Code).
smt_solve_test_bis(FILE,TO,Code) :-
set_threshold(1e-3),
setval(cpt_solve,0)@colibri,
smt_solve_bis(1,FILE,TO,ICode),
getval(diag_code,(Diag,Code0)),
(ICode == 3 ->
% timeout
Code = 3
; getval(smt_status,Status0),
((Diag == wrong_sat,
Status = Diag;
Diag \== unknown,
Status0 \== unknown,
Status0 \== 0,
Status0 \== Diag,
Status = Status0)
->
Code = 2,
writeln(output,FILE:ko:Status)
; Code = Code0,
writeln(output,FILE:ok))),
(getval(use_simplex,1) ->
getval(cpt_solve,NbS)@colibri,
writeln(output,"NbSimplex":NbS)
; true).
% pour tester l'installation colibri
smt_test :-
StrDir = "./Examples/QF_FP/schanda/spark/",
smt_test0(5,1000,StrDir).
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 = "./smt/",
%StrDir = "./AdaCore/",
%StrDir = "./AdaCore/smt/",
%StrDir = "./QF_LRA/2017-Heizmann-UltimateInvariantSynthesis/",
%StrDir = "./QF_LRA/DTP-Scheduling/",
%StrDir = "./QF_LRA/LassoRanker/",
%StrDir = "./QF_LRA/latendresse/",
%StrDir = "./QF_LRA/miplib/",
%StrDir = "./QF_LRA/check/", %OK
%StrDir = "./QF_LRA/keymaera/", %OK
%StrDir = "./QF_LRA/meti-tarski/", %OK
%StrDir = "./QF_LRA/sal/",
%StrDir = "./QF_LRA/sc/",
%StrDir = "./QF_LRA/spider_benchmarks/",
%StrDir = "./QF_LRA/TM/",
%StrDir = "./QF_LRA/tropical-matrix/",
%StrDir = "./QF_LRA/uart/",
%StrDir = "./QF_LRA/tta_startup/",
%StrDir = "./smtlib_schanda-master/crafted/",
%StrDir = "./smtlib_schanda-master/crafted/QF_FP/",
%StrDir = "./smtlib_schanda-master/crafted/QF_FPBV/",
%StrDir = "./smtlib_schanda-master/crafted/QF_FPLRA/",
%StrDir = "./smtlib_schanda-master/griggio/",
%StrDir = "./smtlib_schanda-master/nyxbrain/",
%StrDir = "./smtlib_schanda-master/nyxbrain/executable-tests/",
%StrDir = "./smtlib_schanda-master/nyxbrain/crafted-edge-cases/",
%StrDir = "./smtlib_schanda-master/random/fp.from.real/",
%StrDir = "./smtlib_schanda-master/random/",
%StrDir = "./smtlib_schanda-master/random/fp.from.real/",
%StrDir = "./smtlib_schanda-master/random/fp.fma/",
%StrDir = "./smtlib_schanda-master/random/fp.to.ubv/",
%StrDir = "./smtlib_schanda-master/random/fp.add/",
%StrDir = "./smtlib_schanda-master/random/fp.eq/",
%StrDir = "./smtlib_schanda-master/random/fp.gt/",
%StrDir = "./smtlib_schanda-master/random/fp.geq/",
%StrDir = "./smtlib_schanda-master/random/fp.leq/",
%StrDir = "./smtlib_schanda-master/random/fp.lt/",
%StrDir = "./smtlib_schanda-master/random/fp.from.ubv/",
%StrDir = "./smtlib_schanda-master/random/fp.from.sbv/",
% declare-datatypes ????
%StrDir = "./smtlib_schanda-master/spark_2014/",
%StrDir = "./smtlib_schanda-master/wintersteiger/",
%StrDir = "./Examples/QF_FP/schanda/spark/",
%StrDir = "./totest/",
%StrDir = "./AdaCore/",
%------------------------------------------------------------------------
%StrDir = "./QF_BV/",
%StrDir = "./QF_BV/20170501-Heizmann-UltimateAutomizer/",% 0
%StrDir = "./QF_BV/20170531-Hansen-Check/", % 0
%StrDir = "./QF_BV/2017-BuchwaldFried/",% 3/4
%StrDir = "./QF_BV/2018-Goel-hwbench/",% 11/11
%StrDir = "./QF_BV/2019-Mann/",% 2/2
%StrDir = "./QF_BV/2019-Wolf-fmbench/",% 14/14
%StrDir = "./QF_BV/20200415-Yurichev/",% 1/1
%StrDir = "./QF_BV/bmc-bv-svcomp14/",% 14/32
%StrDir = "./QF_BV/calypto/",% 20/23
%StrDir = "./QF_BV/challenge/",% 1/2
%StrDir = "./QF_BV/check2/",% 0/6
%StrDir = "./QF_BV/dwp_formulas/",% 0/332
%StrDir = "./QF_BV/ecc/", % 7/8
%StrDir = "./QF_BV/float/",% 182/209
%StrDir = "./QF_BV/galois/", % 2 BUGS / 4 fich (unknown)
%StrDir = "./QF_BV/gulwani-pldi08/",
%StrDir = "./QF_BV/log-slicing/",
%StrDir = "./QF_BV/mcm/",
%StrDir = "./QF_BV/pipe/",
%StrDir = "./QF_BV/pspace/",
%StrDir = "./QF_BV/rubik/",
%StrDir = "./QF_BV/RWS/",
%StrDir = "./QF_BV/sage/",
%StrDir = "./QF_BV/spear/",
%StrDir = "./QF_BV/stp_samples/",
%StrDir = "./QF_BV/tacas07/",
%StrDir = "./QF_BV/uclid/",
%StrDir = "./QF_BV/uclid_contrib_smtcomp09/",
%StrDir = "./QF_BV/uum/",
%StrDir = "./QF_BV/VS3/",
%StrDir = "./QF_BV/wienand-cav2008/",
%StrDir = "./QF_BV/asp/",
%StrDir = "./QF_BV/bench_ab/",%OK
%StrDir = "./QF_BV/bmc-bv/",
%StrDir = "./QF_BV/bmc-bv-svcomp14/",
%StrDir = "./QF_BV/brummayerbiere/",
%StrDir = "./QF_BV/brummayerbiere2/",
%StrDir = "./QF_BV/brummayerbiere3/",
%StrDir = "./QF_BV/brummayerbiere4/",
%StrDir = "./QF_BV/bruttomesso/", % plein de TO
%StrDir = "./QF_BV/crafted/",
%-----------------------------------------------------------------------
%StrDir = "./QF_AUFBVFP/20210301-Alive2/",% 1 (durdur)
%-----------------------------------------------------------------------
%StrDir = "QF_ABVFP/20170428-Liew-KLEE/imperial_svcomp_float-benchs_svcomp_mea8000.x86_64/", %0
%StrDir = "QF_ABVFP/20170428-Liew-KLEE/imperial_synthetic_non_terminating_klee_bug.x86_64/", % 0
%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/20170501-Heizmann-UltimateAutomizer/", % 0 min_solve (cvc4 0) OK
%----------------------------------------------------------------------
%StrDir = "./QF_ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/",% 0 (cvc4 1|2)!
%StrDir = "./QF_ABVFPLRA/20170501-Heizmann-UltimateAutomizer/",% 0 (0)
%--------------------------------------------------------------------------
%StrDir = "./QF_BVFP/20170428-Liew-KLEE/aachen_real_numerical_recipes_qrdcmp.x86_64/",
%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
% 15)(89 u)(11 20mn)
%StrDir = "./QF_BVFP/20170501-Heizmann-UltimateAutomizer/", % 0 (bitwuzla 0)
%StrDir = "./QF_BVFP/ramalho/", % 0 TO (bitwuzla 0)
%StrDir = "./QF_BVFP/schanda/spark/", % 1 sans -> int (quake)
% (bitwuzla 1) (le passage en int casse les deltas)
%----------------------------------------------------------------
%StrDir = "./QF_BVFPLRA/20170501-Heizmann-UltimateAutomizer/", % 0 (cvc4 0)
%StrDir = "./QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/", % 9 + 11u (cvc4 17 + 11u sinon 0u avec --fp-exp?))
%StrDir = "./QF_BVFPLRA/2019-Gudemann/", % 0 (cvc4 1)
%----------------------------------------------------------------
%StrDir = "./QF_FPLRA/20170501-Heizmann-UltimateAutomizer/", % 0 (cvc4 0)
%StrDir = "./QF_FPLRA/20190429-UltimateAutomizerSvcomp2019/", % 0 (cvc4 0)
%StrDir = "./QF_FPLRA/2019-Gudemann/", % 2 (cvc4 7)
%StrDir = "./QF_FPLRA/schanda/", % 0 (cvc4 0)
%----------------------------------------------------------------
%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)
%(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
%-----------------------------------------------------------------------
%StrDir = "./QF_UFFP/schanda/",% 0
%-----------------------------------------------------------------
%StrDir = "./QF_UF/", % 426 (pour 1061)
%----------------------------------------------------------------
%StrDir = "./QF_AUFBV/", %
%----------------------------------------------------------------
%StrDir = "./QF_UFIDL/", % 290 (pour 329)
%----------------------------------------------------------------
%StrDir = "./QF_UFLIA/", % 104 (pour 129)
%----------------------------------------------------------------
%StrDir = "./QF_UFLRA/", % 141 (pour 384)
%----------------------------------------------------------------
%StrDir = "./QF_ABV/bench_ab/",%1
%StrDir = "./QF_ABV/bmc-arrays/",%10(9 core)
%-----------------------------------------------------------------
%StrDir = "QF_AX/",
%StrDir = "QF_AX/storeinv/", % 4
%StrDir = "QF_AX/swap/", % 8 -> 15
%StrDir = "QF_AX/storecomm/", % 0
%StrDir = "QF_AX/cvc/", % 0
%StrDir = "QF_ALIA/qlock2/", % Des TO et core dump
%StrDir = "QF_ALIA/cvc/", % 3
%StrDir = "QF_ALIA/UltimateAutomizer2/",% des TO
%StrDir = "QF_ALIA/piVC/", % 11
%StrDir = "QF_ALIA/ios/", % 26
%StrDir = "QF_NIA/20170427-VeryMax/", Que des TO
%StrDir = "QF_NIA/AProVE/",
%StrDir = "QF_NIA/calypto/", %OK
%StrDir = "QF_NIA/LassoRanker/",%OK mieux en real_int qu'en int !!
%StrDir = "QF_NIA/LCTES/",%TO %StrDir = "QF_NIA/leipzig/",
%StrDir = "QF_NIA/mcm/",%TO
%StrDir = "QF_NIA/UltimateAutomizer/",%OK
%StrDir = "QF_NIA/UltimateLassoRanker/",%TO
%StrDir = "QF_LIA/20180326-Bromberger/",
%StrDir = "QF_LIA/cut_lemmas/", %TO
%StrDir = "QF_LIA/wisa/", %TO
%StrDir = "QF_LIA/arctic-matrix/", %TO
%StrDir = "QF_LIA/check/", %OK + TO
%StrDir = "QF_LIA/RTCL/", %OK
%StrDir = "QF_LIA/miplib2003/", %TO
%StrDir = "QF_LIA/rings_preprocessed/", %TO
%StrDir = "QF_LIA/mathsat/", %TO
%StrDir = "QF_LIA/CAV_2009_benchmarks/smt/", %TO
%StrDir = "QF_LIA/rings/", %TO
%StrDir = "QF_LIA/fft/", %TO
%StrDir = "QF_ANIA/",% Unsupported ou TO
%StrDir = "QF_ABV/bmc-arrays/",
%StrDir = "QF_AFPBV/dwp_formulas/", %TRES DUR
smt_test0(TO,Size,StrDir).
:- lib(timeout).
read_file_list(SmtFileList) :-
(at_eof(tataS) ->
close(tataS),
SmtFileList = []
; SmtFileList = [F| NSmtFileList],
read_string(tataS,end_of_line,_,F),
read_file_list(NSmtFileList)).
smt_test0(TO,Size,StrDir) :-
setval(bug,[]),
setval(cpt_solve,0)@colibri,
os_file_name(StrDir,OS_Examples),
(StrDir == "./QF_FP/wintersteiger/" ->
read_directory(OS_Examples,"*/*",SubdirList0,_)
; read_directory(OS_Examples,"*",SubdirList0,_)),
(SubdirList0 == [] ->
SubdirList = ["."]
; SubdirList = SubdirList0),
(foreach(Dir,SubdirList),
fromto([],IS,OS,SmtFileList),
param(StrDir) do
append_strings(StrDir,Dir,SubDir),
os_file_name(SubDir,OS_SubDir),
read_directory(OS_SubDir, "*.smt2", _, SmtList),
(foreach(F,SmtList),
fromto(IS,I,O,OS),
param(SubDir) do
concat_string([SubDir,"/",F],PF),
os_file_name(PF,OS_PF),
O = [OS_PF|I])),
initNbCodes,
get_flag(version_as_list,[Ver|_]),
((Ver == 7) ->
ECLIPSE = eclipse7,
COL = "col_solve.eco"
; ECLIPSE = eclipse,
COL = "col_solve.pl"),
get_flag(hostarch,ARCH),
((ARCH == "i386_nt";
ARCH == "x86_64_nt")
->
Windows = 1 ; true),
/*
open(tata,read,tataS),
read_file_list(SmtFileList),
*/
length(SmtFileList,NbFiles),
setval(nbTO,0),
( member(F,SmtFileList),
incval(nbFile),
getval(nbFile,NumF),
getval(nbTO,NbTO),
writeln(output,F:NumF/NbFiles-'TO':NbTO),
concat_atom([Size,'M'],SizeM),
(nonvar(Windows) ->
get_flag(installation_directory,EDIR),
os_file_name(OF,F),
concat_string(["cmd.exe /D /C smt_test_file ",OF," ",TO],Com)
; concat_string(["timeout --signal=KILL --kill-after=0.1 ",TO,"s ",ECLIPSE," -b ",COL," -g ",SizeM," -e \"seed(0),use_delta,use_simplex,setval(def_real_for_int,1)@colibri,setval(step_limit,0),setval(no_dolmen_warning,1)@eclipse,setval(show_steps,1),smt_solve_get_stat(\'",F,"\')\""],Com)),
% ; concat_string(["timeout --signal=KILL --kill-after=0.1 ",TO,"s ",ECLIPSE," -b ",COL," -g ",SizeM," -e \"seed(0),smt_comp_solve(\'",F,"\')\""],Com)),
%; concat_string(["timeout --signal=KILL --kill-after=0.1 ",TO,"s cvc4 ",F],Com)),
%; concat_string(["timeout --signal=KILL --kill-after=0.1 ",TO,"s ncvc4 --fp-exp ",F],Com)),
%; concat_string(["timeout --signal=KILL --kill-after=0.1 ",TO,"s z3 ",F],Com)),
%; concat_string(["timeout --signal=KILL --kill-after=0.1 ",TO,"s bitwuzla ",F],Com)),
exec(Com,[],Pid),
wait(Pid,CodeExt),
writeln(code:CodeExt),
(CodeExt == 0 ->
% unsat
Code = 0
; ((CodeExt == 256;
CodeExt == 1)
->
% sat 1*256
Code = 1
; ((CodeExt == 9;
CodeExt == 3)
->
% timeout
Code = 3,
incval(nbTO)
; (CodeExt == 11 ->
% core dump
Code = 4
; (CodeExt == 512 ->
% erreur ou wrong_sat/wrong_unsat ou bug 2*256
Code = 2
; (CodeExt == 1536 ->
% Step limit reached: 6*256
Code = 6
; % unsupported 5*256=1280
Code = 5)))))),
incNbCode(Code),
(Code == 2 ->
%halt,
getval(bug,Bugs),
setval(bug,[F|Bugs])
; true),
fail
; true),
getval(nbFile,NbFile),
writeln(output,"Files":NbFile),
getval(nb0,Nb0),
writeln(output,"Unsat":Nb0),
getval(nb1,Nb1),
writeln(output,"Sat":Nb1),
getval(nb2,Nb2),
writeln(output,"Error":Nb2),
getval(nb6,Nb6),
writeln(output,"Step limit":Nb6), getval(nb3,Nb3),
writeln(output,"Timeout":Nb3),
getval(nb4,Nb4),
writeln(output,"Core dump":Nb4),
getval(nb5,Nb5),
writeln(output,"Unsupported":Nb5),
getval(bug,Bugs),
(Bugs == [] ->
true
; nl(output),
writeln(output,"BUGS:"),
(foreach(B,Bugs) do
writeln(output,B))).
smt_unit_test(TO) :-
setval(bug,[]),
%StrDir = "./QF_BVFP/20170428-Liew-KLEE/imperial_svcomp_float-benchs_svcomp_mea8000.x86_64/",
%StrDir = "./smtlib_schanda-master/random/", % tout OK ou unsupported
%StrDir = "./smtlib_schanda-master/random/fp.from.real/",
%StrDir = "./smtlib_schanda-master/random/fp.fma/",
%StrDir = "./smtlib_schanda-master/random/fp.div/",
%StrDir = "./smtlib_schanda-master/random/fp.mul/",
%StrDir = "./smtlib_schanda-master/nyxbrain/",
%StrDir = "./smtlib_schanda-master/spark_2014/",
%------------------------------------------------------------------------
%StrDir = "./QF_ABVFPLRA/20190429-UltimateAutomizerSvcomp2019/",% 2-3 (4)
%StrDir = "./QF_ABVFPLRA/20170501-Heizmann-UltimateAutomizer/",% 0-1 (0)
%------------------------------------------------------------------------
%StrDir = "./QF_ABVFP/20170428-Liew-KLEE/", % 79 TO (69 sans simplex) (cvc4 76)
%StrDir = "./QF_ABVFP/20170428-Liew-KLEE/aachen_real_gmp_gmp_klee_mul.x86_64/",
%StrDir = "./QF_ABVFP/20170501-Heizmann-UltimateAutomizer/", % 0 TO
%StrDir = "./QF_ABVFP/20170428-Liew-KLEE/imperial_synthetic_count_klee_bug.x86_64/", % 6 TO/9! (cvc4 0)
%StrDir = "./QF_ABVFP/20170428-Liew-KLEE/imperial_synthetic_count_klee.x86_64/", % 3/87! (0)
%StrDir = "./QF_ABVFP/20170428-Liew-KLEE/aachen_real_sorting_full_sym_floats.x86_64/", % 2
%StrDir = "./QF_ABVFP/20170428-Liew-KLEE/aachen_real_sorting_doubles.x86_64/", % 10/58
%------------------------------------------------------------------------
%StrDir = "./QF_BVFP/",
%StrDir = "./QF_BVFP/20170428-Liew-KLEE/", % 33-76 ()
%StrDir = "./QF_BVFP/20170501-Heizmann-UltimateAutomizer/", % 0 TO
%StrDir = "./QF_BVFP/20190429-UltimateAutomizerSvcomp2019/",% 1
%StrDir = "./QF_BVFP/ramalho/", % 0 TO
%StrDir = "./QF_BVFP/schanda/spark/", % 1 TO
%------------------------------------------------------------------------
%StrDir = "./QF_UFFP/schanda/spark/",% 0 TO
%------------------------------------------------------------------------
%StrDir = "./QF_FPLRA/20170501-Heizmann-UltimateAutomizer/",% 0 TO
%StrDir = "./QF_FPLRA/20190429-UltimateAutomizerSvcomp2019/",% 0 TO
%StrDir = "./QF_FPLRA/schanda/spark/",% 1-0 TO
%StrDir = "./QF_FPLRA/2019-Gudemann/",% 2 (11)
%------------------------------------------------------------------------
%StrDir = "./QF_BVFPLRA/20170501-Heizmann-UltimateAutomizer/",% 0 TO
%StrDir = "./QF_BVFPLRA/20190429-UltimateAutomizerSvcomp2019/",% 15-11 (22)
%StrDir = "./QF_BVFPLRA/2019-Gudemann/",% 0 TO
%------------------------------------------------------------------------
%StrDir = "./QF_FP/20170501-Heizmann-UltimateAutomizer/", % 0 TO
%StrDir = "./QF_FP/ramalho/",% 6-2 T0
%StrDir = "./QF_FP/griggio/", % 59 TO en 24s, 51 en 60s (cvc4 90 en 60s)
%StrDir = "./QF_FP/schanda/spark/",% 7 TO
StrDir = "./QF_FP/wintersteiger/", % 0 TO
%------------------------------------------------------------------------
%StrDir = "QF_AX/",
%StrDir = "QF_AX/storeinv/",
%StrDir = "QF_AX/swap/",
%StrDir = "QF_AX/storecomm/",
%StrDir = "QF_AX/cvc/",
%----------------------------------------------------------------------
%StrDir = "./QF_BV/",
%StrDir = "./QF_BV/20170501-Heizmann-UltimateAutomizer/",
%StrDir = "./QF_BV/20170531-Hansen-Check/", %OK
%StrDir = "./QF_BV/2017-BuchwaldFried/",
%StrDir = "./QF_BV/2018-Goel-hwbench/",
%StrDir = "./QF_BV/2019-Mann/",
%StrDir = "./QF_BV/2019-Wolf-fmbench/",
%StrDir = "./QF_BV/20200415-Yurichev/",
%StrDir = "./QF_BV/bmc-bv-svcomp14/",
%StrDir = "./QF_BV/calypto/",
%StrDir = "./QF_BV/challenge/",
%StrDir = "./QF_BV/check2/",
%StrDir = "./QF_BV/dwp_formulas/",
%StrDir = "./QF_BV/ecc/", % NULL comparé a cvc4
%StrDir = "./QF_BV/float/",
%StrDir = "./QF_BV/galois/", % 2 BUGS / 4 fich (unknown)
%StrDir = "./QF_BV/gulwani-pldi08/",
%StrDir = "./QF_BV/log-slicing/",
%StrDir = "./QF_BV/mcm/",
%StrDir = "./QF_BV/pipe/",
%StrDir = "./QF_BV/pspace/",
%StrDir = "./QF_BV/rubik/",
%StrDir = "./QF_BV/RWS/",
%StrDir = "./QF_BV/sage/",
%StrDir = "./QF_BV/sage2/",
%StrDir = "./QF_BV/spear/",
%StrDir = "./QF_BV/stp/",
%StrDir = "./QF_BV/stp_samples/",
%StrDir = "./QF_BV/tacas07/",
%StrDir = "./QF_BV/uclid/",
%StrDir = "./QF_BV/uclid_contrib_smtcomp09/",
%StrDir = "./QF_BV/uum/",
%StrDir = "./QF_BV/VS3/",
%StrDir = "./QF_BV/wienand-cav2008/",
%StrDir = "./QF_BV/asp/",
%StrDir = "./QF_BV/bench_ab/",%OK
%StrDir = "./QF_BV/bmc-bv/",
%StrDir = "./QF_BV/bmc-bv-svcomp14/",
%StrDir = "./QF_BV/brummayerbiere/",
%StrDir = "./QF_BV/brummayerbiere2/",
%StrDir = "./QF_BV/brummayerbiere3/",
%StrDir = "./QF_BV/brummayerbiere4/",
%StrDir = "./QF_BV/bruttomesso/", % plein de TO
%StrDir = "./QF_BV/crafted/",
%-----------------------------------------------------------------------
%StrDir = "QF_ABV/bench_ab/",
%StrDir = "QF_ABV/bmc-arrays/",
%StrDir = "QF_ABV/brummayerbiere/", %TROP DUR
%StrDir = "QF_ABV/btfnt/", %TROP DUR
%StrDir = "QF_ABV/calc2/", %TROP DUR
%StrDir = "QF_ABV/dwp_formulas/", %TRES DUR
%StrDir = "QF_ABV/ecc/", %TRES DUR
%StrDir = "QF_ABV/egt/",
%StrDir = "QF_ABV/jager/",
%StrDir = "QF_ABV/klee-selected-smt2/",
os_file_name(StrDir,OS_Examples),
((StrDir == "./QF_FP/wintersteiger/";
StrDir == "./QF_BVFP/schanda/spark/")
->
read_directory(OS_Examples,"*/*",SubdirList0,_)
; read_directory(OS_Examples,"*",SubdirList0,_)),
(SubdirList0 == [] ->
SubdirList = ["."]
; SubdirList = SubdirList0),
(foreach(Dir,SubdirList),
fromto([],IS,OS,SmtFileList),
param(StrDir) do
append_strings(StrDir,Dir,SubDir),
os_file_name(SubDir,OS_SubDir), read_directory(OS_SubDir, "*.smt2", _, SmtList),
(foreach(F,SmtList),
fromto(IS,I,O,OS),
param(SubDir) do
concat_string([SubDir,"/",F],PF),
os_file_name(PF,OS_PF),
O = [OS_PF|I])),
initNbCodes,
setval(nbFile,0),
setval(nbTO,0),
setval(no_dolmen_warning,1)@eclipse,
getval(use_delta,UD)@eclipse,
getval(use_simplex,US)@eclipse,
length(SmtFileList,NFs),
( member(F,SmtFileList),
incval(nbFile),
getval(nbFile,NbF),
getval(nbTO,NbTO),
writeln(output,F:NbF/NFs-'TO':NbTO),
garbage_collect,
setval(cpt_solve,0)@colibri,
setval(use_delta,UD)@eclipse,
setval(use_simplex,US)@eclipse,
smt_solve_bis(1,F,TO,Code),
incNbCode(Code),
(Code == 2 ->
getval(bug,Bugs),
setval(bug,[F|Bugs])
; (Code == 3 ->
incval(nbTO)
; true)),
fail
; true),
getval(nbFile,NbFile),
writeln(output,"Files":NbFile),
getval(nb0,Nb0),
writeln(output,"Unsat":Nb0),
getval(nb1,Nb1),
writeln(output,"Sat":Nb1),
getval(nb2,Nb2),
writeln(output,"Error":Nb2),
getval(nb3,Nb3),
writeln(output,"Timeout":Nb3),
getval(nb5,Nb5),
writeln(output,"Unsupported":Nb5),
getval(bug,Bugs),
(Bugs == [] ->
true
; nl(output),
writeln(output,"BUGS:"),
(foreach(B,Bugs) do
writeln(output,B))).
smt_unit_test1 :-
setval(bug,[]),
setval(cpt_solve,0)@colibri,
StrDir = "./QF_BVFP/20170428-Liew-KLEE/",
os_file_name(StrDir,OS_Examples),
(StrDir == "./QF_FP/wintersteiger/" ->
read_directory(OS_Examples,"*/*",SubdirList0,_)
; read_directory(OS_Examples,"*",SubdirList0,_)),
(SubdirList0 == [] ->
SubdirList = ["."]
; SubdirList = SubdirList0),
(foreach(Dir,SubdirList),
fromto([],IS,OS,SmtFileList),
param(StrDir) do
append_strings(StrDir,Dir,SubDir),
os_file_name(SubDir,OS_SubDir),
read_directory(OS_SubDir, "*.smt2", _, SmtList), (foreach(F,SmtList),
fromto(IS,I,O,OS),
param(SubDir) do
concat_string([SubDir,"/",F],PF),
os_file_name(PF,OS_PF),
O = [OS_PF|I])),
initNbCodes,
( member(F,SmtFileList),
incval(nbFile),
writeln(output,F),
smt_solve_test_bis(F,1,Code),
incNbCode(Code),
(Code == 2 ->
getval(bug,Bugs),
setval(bug,[F|Bugs])
; true),
fail
; true),
getval(nbFile,NbFile),
writeln(output,"Files":NbFile),
getval(nb0,Nb0),
writeln(output,"Unsat":Nb0),
getval(nb1,Nb1),
writeln(output,"Sat":Nb1),
getval(nb2,Nb2),
writeln(output,"Error":Nb2),
getval(nb6,Nb6),
writeln(output,"Step limit":Nb6),
getval(nb3,Nb3),
writeln(output,"Timeout":Nb3),
getval(nb5,Nb5),
writeln(output,"Unsupported":Nb5),
getval(bug,Bugs),
(Bugs == [] ->
true
; nl(output),
writeln(output,"BUGS:"),
(foreach(B,Bugs) do
writeln(output,B))).
make_scripts :-
(get_flag(hostarch,"x86_64_nt") ->
make_scripts_windows
; make_scripts_unix).
make_scripts_windows :-
(exists('colibri.bat') ->
delete('colibri.bat')
; true),
(exists('test_colibri.bat') ->
delete('test_colibri.bat')
; true),
get_flag(cwd,COLDIR0),
os_file_name(COLDIR0,COLDIR),
writeln(output,"Making script colibri.bat"),
open('colibri.bat',write,colibri),
writeln(colibri,"@echo off"),
write(colibri,"set COLDIR="),
writeln(colibri,COLDIR),
writeln(colibri,"set PATH=%PATH%;%COLDIR%\\lib\\v7\\x86_64_nt"),
writeln(colibri,"set ECLIPSEDIR=%COLDIR%\\ECLiPSe"),
writeln(colibri,"set GOAL=\"solve('%1')\""),
writeln(colibri,"if \"%1\" == \"\" (set GOAL=\"solve('colibri.in')\")"),
% writeln(colibri,"@echo on"),
writeln(colibri,"\"%ECLIPSEDIR%\\lib\\x86_64_nt\\eclipse.exe\" -b"
" \"%COLDIR%\\compile_flag\" -b"
" \"%COLDIR%\\col_solve\" -g 2000M -e %GOAL%"),
close(colibri),
writeln(output,"Making script test_colibri.bat"), open('test_colibri.bat',write,test_colibri),
writeln(test_colibri,"@echo off"),
write(test_colibri,"set COLDIR="),
writeln(test_colibri,COLDIR),
writeln(test_colibri,"set PATH=%PATH%;%COLDIR%\\lib\\v7\\x86_64_nt"),
writeln(test_colibri,"set ECLIPSEDIR=%COLDIR%\\ECLiPSe"),
% writeln(test_colibri,"@echo on"),
writeln(test_colibri,"\"%ECLIPSEDIR%\\lib\\x86_64_nt\\eclipse.exe\" -b"
" \"%COLDIR%\\compile_flag\" -b"
" \"%COLDIR%\\col_solve\" -g 2000M -e test_colibri"),
close(test_colibri),
writeln(output,"Making script smt_colibri.bat"),
open('smt_colibri.bat',write,smt_colibri),
writeln(smt_colibri,"@echo off"),
write(smt_colibri,"set COLDIR="),
writeln(smt_colibri,COLDIR),
writeln(smt_colibri,"set PATH=%PATH%;%COLDIR%\\lib\\v7\\x86_64_nt"),
writeln(smt_colibri,"set ECLIPSEDIR=%COLDIR%\\ECLiPSe"),
writeln(smt_colibri,"set GOAL=\"smt_solve('%1')\""),
writeln(smt_colibri,"if \"%1\" == \"\" (set GOAL=\"smt_solve('smt_colibri.in')\")"),
% writeln(smt_colibri,"@echo on"),
writeln(smt_colibri,"\"%ECLIPSEDIR%\\lib\\x86_64_nt\\eclipse.exe\" -b"
" \"%COLDIR%\\compile_flag\" -b"
" \"%COLDIR%\\col_solve\" -g 2000M -e %GOAL%"),
close(smt_colibri),
writeln(output,"Making script smt_test_colibri.bat"),
open('smt_test_colibri.bat',write,smt_test_colibri),
writeln(smt_test_colibri,"@echo off"),
write(smt_test_colibri,"set COLDIR="),
writeln(smt_test_colibri,COLDIR),
writeln(smt_test_colibri,"set PATH=%PATH%;%COLDIR%\\lib\\v7\\x86_64_nt"),
writeln(smt_test_colibri,"set ECLIPSEDIR=%COLDIR%\\ECLiPSe"),
% writeln(smt_test_colibri,"@echo on"),
writeln(smt_test_colibri,"\"%ECLIPSEDIR%\\lib\\x86_64_nt\\eclipse.exe\" -b"
" \"%COLDIR%\\compile_flag\" -b"
" \"%COLDIR%\\col_solve\" -g 2000M -e smt_test"),
close(smt_test_colibri),
writeln(output,"Making script smt_test_file.bat"),
open('smt_test_file.bat',write,smt_test_file),
writeln(smt_test_file,"@echo off"),
write(smt_test_file,"set COLDIR="),
writeln(smt_test_file,COLDIR),
writeln(smt_test_file,"set PATH=%PATH%;%COLDIR%\\lib\\v7\\x86_64_nt"),
writeln(smt_test_file,"set ECLIPSEDIR=%COLDIR%\\ECLiPSe"),
% writeln(smt_test_file,"@echo on"),
writeln(smt_test_file,"\"%ECLIPSEDIR%\\lib\\x86_64_nt\\eclipse.exe\" -b"
" \"%COLDIR%\\compile_flag\" -b"
" \"%COLDIR%\\col_solve\" -g 2000M -e \"no_simplex,smt_solve_test('%1',%2)\""),
close(smt_test_file).
make_scripts_unix :-
(exists('colibri.sh') ->
delete('colibri.sh')
; true),
(exists('test_colibri.sh') ->
delete('test_colibri.sh')
; true),
(exists('smt_colibri.sh') ->
delete('smt_colibri.sh')
; true),
(exists('smt_test_colibri.sh') ->
delete('smt_test_colibri.sh')
; true),
get_flag(cwd,COLDIR),
get_flag(hostarch,ARCH),
get_flag(installation_directory,ECLIPSEDIR),
writeln(output,"Making script colibri.sh"),
open('colibri.sh',write,colibri), concat_string(["#!/bin/sh
FILE=$1
GOAL=\"solve('colibri.in')\"
if [ \"$FILE\" != \"\" ]
then
GOAL=\"solve('$FILE')\"
fi
COLDIR=",COLDIR,"
# Repertoire ECLiPSe Prolog
ECLIPSEDIR=",ECLIPSEDIR,"
ARCH=x86_64_linux
LD_LIBRARY_PATH=${ECLIPSEDIR}/lib/${ARCH}:$LD_LIBRARY_PATH
export ECLIPSEDIR ARCH LD_LIBRARY_PATH
# Chargement/demarrage de test_colibri
exec ${ECLIPSEDIR}/lib/${ARCH}/eclipse.exe -b ${COLDIR}/compile_flag -b ${COLDIR}/col_solve -g 2000M -e ${GOAL}"],COLIBRI),
writeln(colibri,COLIBRI),
close(colibri),
exec('chmod a+rx ./colibri.sh',[]),
writeln(output,"Making script smt_colibri.sh"),
open('smt_colibri.sh',write,smt_colibri),
concat_string(["#!/bin/sh
FILE=$1
GOAL=\"solve('smt_colibri.in')\"
if [ \"$FILE\" != \"\" ]
then
GOAL=\"smt_solve('$FILE')\"
fi
COLDIR=`/bin/pwd`
# Repertoire ECLiPSe Prolog
ECLIPSEDIR=${COLDIR}/ECLiPSe
ARCH=x86_64_linux
LD_LIBRARY_PATH=${ECLIPSEDIR}/lib/${ARCH}:$LD_LIBRARY_PATH
export ECLIPSEDIR ARCH LD_LIBRARY_PATH
# Chargement/demarrage de test_colibri
exec ${ECLIPSEDIR}/lib/${ARCH}/eclipse.exe -b ${COLDIR}/compile_flag -b ${COLDIR}/col_solve -g 2000M -e ${GOAL}"],SMTCOLIBRI),
writeln(smt_colibri,SMTCOLIBRI),
close(smt_colibri),
exec('chmod a+rx ./smt_colibri.sh',[]),
writeln(output,"Making script test_colibri.sh"),
open('test_colibri.sh',write,test_colibri),
concat_string(["#!/bin/sh
COLDIR=`/bin/pwd`
# Repertoire ECLiPSe Prolog
ECLIPSEDIR=",ECLIPSEDIR,"
ARCH=x86_64_linux
LD_LIBRARY_PATH=${ECLIPSEDIR}/lib/${ARCH}:$LD_LIBRARY_PATH
export ECLIPSEDIR ARCH LD_LIBRARY_PATH
# Chargement/demarrage de test_colibri
exec ${ECLIPSEDIR}/lib/${ARCH}/eclipse.exe -b ${COLDIR}/compile_flag -b ${COLDIR}/col_solve -g 2000M -e test_colibri"],TestCOLIBRI),
writeln(test_colibri,TestCOLIBRI),
close(test_colibri),
exec('chmod a+rx ./test_colibri.sh',[]),
writeln(output,"Making script smt_test_colibri.sh"),
open('smt_test_colibri.sh',write,smt_test_colibri),
concat_string(["#!/bin/sh
COLDIR=",COLDIR,"
# Repertoire ECLiPSe Prolog
ECLIPSEDIR=",ECLIPSEDIR,"
ARCH=x86_64_linux
LD_LIBRARY_PATH=${ECLIPSEDIR}/lib/${ARCH}:$LD_LIBRARY_PATH
export ECLIPSEDIR ARCH LD_LIBRARY_PATH
# Chargement/demarrage de test_colibri
exec ${ECLIPSEDIR}/lib/${ARCH}/eclipse.exe -b ${COLDIR}/compile_flag -b ${COLDIR}/col_solve -g 2000M -e smt_test"],SMTTestCOLIBRI),
writeln(smt_test_colibri,SMTTestCOLIBRI),
close(smt_test_colibri),
exec('chmod a+rx ./smt_test_colibri.sh',[]).