add_benchmark_result(Solver, ConstraintPath, Result) :-
asserta(benchmark_result(Solver,ConstraintPath,Result)).
Calls:
Name: asserta/1 |
Called:
Name: benchmark_constraint/23 |
Module: smt_solver_benchmarks |
amount_of_sat_vars(BenchmarkName, FolderPath, Acc, NewAcc) :-
write('Eval amount of sat variables for '), write(FolderPath), nl,
directory_exists(FolderPath),
file_members_of_directory(FolderPath, FilePaths),
select_machine_file_path(FilePaths, MachineFilePath, TBenchmarkFilePaths),
findall(FilePath, (member(_-FilePath, TBenchmarkFilePaths), atom_concat(_, '.eval', FilePath)), BenchmarkFilePaths),
load_b_eventb_or_tla(MachineFilePath),
amount_of_sat_vars_for_benchmark(BenchmarkFilePaths, AmountOfSatVars),
append(Acc, AmountOfSatVars, NewAcc),
eval_amount_of_sat_vars(BenchmarkName, AmountOfSatVars).
Calls:
| Module: smt_solver_benchmarks | |
Name: append/3 |
|
| Module: smt_solver_benchmarks | |
Name: load_b_eventb_or_tla/1 |
Module: smt_solver_benchmarks |
Name: findall/3 |
|
| Module: smt_solver_benchmarks | |
Name: file_members_of_directory/2 |
Module: foo_error |
Name: directory_exists/1 |
Module: foo_error |
Name: nl |
|
Name: write/1 |
Called:
| Module: smt_solver_benchmarks | |
| Module: smt_solver_benchmarks | |
Name: amount_of_sat_vars_bmc/0 |
Module: smt_solver_benchmarks |
amount_of_sat_vars_bmc :-
amount_of_sat_vars(bmc, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_bmc/abz16_m4/', [], Acc1),
amount_of_sat_vars(bmc, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_bmc/abz16_m5/', Acc1, Acc2),
amount_of_sat_vars(bmc, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_bmc/abz16_m6/', Acc2, Acc3),
amount_of_sat_vars(bmc, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_bmc/abz16_m7/', Acc3, Acc4),
amount_of_sat_vars(bmc, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_bmc/r0_geardoor/', Acc4, Acc5),
amount_of_sat_vars(bmc, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_bmc/r1_valve/', Acc5, Acc6),
amount_of_sat_vars(bmc, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_bmc/r2_outputs/', Acc6, Acc7),
amount_of_sat_vars(bmc, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_bmc/r3_sensors/', Acc7, Acc8),
amount_of_sat_vars(bmc, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_bmc/r4_handle/', Acc8, Acc9),
amount_of_sat_vars(bmc, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_bmc/r5_switch/', Acc9, Acc10),
amount_of_sat_vars(bmc, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_bmc/pm_m0_aai/', Acc10, Acc11),
amount_of_sat_vars(bmc, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_bmc/pm_m0_aat/', Acc11, Acc12),
amount_of_sat_vars(bmc, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_bmc/pm_m0_aoo/', Acc12, Acc13),
amount_of_sat_vars(bmc, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_bmc/pm_m0_voo/', Acc13, Acc14),
amount_of_sat_vars(bmc, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_bmc/pm_m0_vvi/', Acc14, Acc15),
amount_of_sat_vars(bmc, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_bmc/pm_m0_vvt/', Acc15, Acc16),
amount_of_sat_vars(bmc, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_bmc/pm_m1_aoor/', Acc16, Acc17),
amount_of_sat_vars(bmc, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_bmc/pm_m1_voor/', Acc17, Acc18),
amount_of_sat_vars(bmc, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_bmc/pm_m2_aai/', Acc18, Acc19),
amount_of_sat_vars(bmc, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_bmc/simple-two-phase/', Acc19, Acc20),
amount_of_sat_vars(bmc, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_bmc/prisoners-4/', Acc20, Acc21),
amount_of_sat_vars(bmc, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_bmc/bakery/', Acc21, Acc22),
amount_of_sat_vars(bmc, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_bmc/paxos-3/', Acc22, Acc23),
amount_of_sat_vars(bmc, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_bmc/lightbot/', Acc23, Acc24),
amount_of_sat_vars(bmc, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_bmc/travel_agency/', Acc24, Acc25),
amount_of_sat_vars(bmc, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_bmc/search_events/', Acc25, Acc26),
amount_of_sat_vars(bmc, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_bmc/large_branching/', Acc26, Acc27),
amount_of_sat_vars(bmc, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_bmc/r6_lights/', Acc27, Acc28),
mean_of_list(Acc28, TotalMean),
median_of_list(Acc28, TotalMedian),
max_member(Max, Acc28),
open('amount_of_sat_vars_bmc/total.txt', write, Stream),
tell(Stream),
format("Total mean: ~w~nTotal median: ~w~nTotal max: ~w~n", [TotalMean,TotalMedian,Max]),
close(Stream).
Calls:
Name: close/1 |
|
Name: format/2 |
|
Name: tell/1 |
|
Name: open/3 |
|
Name: max_member/2 |
Module: foo_error |
Name: median_of_list/2 |
Module: smt_solver_benchmarks |
Name: mean_of_list/2 |
Module: smt_solver_benchmarks |
Name: amount_of_sat_vars/4 |
Module: smt_solver_benchmarks |
amount_of_sat_vars_csv_files([], Acc, Acc).
amount_of_sat_vars_csv_files([CsvFile|T], Acc, LAmountOfVars) :-
open(CsvFile, read, Stream, [encoding(utf8)]),
read_records(Stream, Records),
close(Stream),
Records = [Header|CsvRecords],
Header = [string(Codes)|_],
atom_codes('ConstraintPath', Codes),
amount_of_sat_vars_csv_records(CsvRecords, Acc, NAcc), !,
amount_of_sat_vars_csv_files(T, NAcc, LAmountOfVars).
amount_of_sat_vars_csv_files([CsvFile|T], Acc, LAmountOfVars) :-
format("CSV file has wrong format: ~w~n", [CsvFile]),
amount_of_sat_vars_csv_files(T, Acc, LAmountOfVars).
Calls:
Name: RECURSIVE_CALL/3 |
Module: smt_solver_benchmarks |
Name: format/2 |
|
Name: ! |
|
| Module: smt_solver_benchmarks | |
Name: atom_codes/2 |
|
Name: =/2 |
|
Name: close/1 |
|
Name: read_records/2 |
Module: foo_error |
Name: open/4 |
Called:
| Module: smt_solver_benchmarks |
amount_of_sat_vars_csv_records([], Acc, Acc).
amount_of_sat_vars_csv_records([CsvRecord|T], Acc, Out) :-
CsvRecord = [string(Codes),string(CodesSolver)|_],
atom_codes(prob, CodesSolver), % only for one solver, e.g., prob
atom_codes(ConstraintPath, Codes),
% patch to get the correct ProB Examples model path from the constraint's path
%get_machine_path_from_inductive_inv_bench_path(ConstraintPath, MachinePath),
%get_machine_path_from_deadlock_freedom_bench_path(ConstraintPath, MachinePath),
get_machine_path_from_bmc_bench_path(ConstraintPath, MachinePath),
load_b_eventb_or_tla(MachinePath),
format("Count SAT vars for ~w~n", [ConstraintPath]),
amount_of_sat_vars_for_benchmark([ConstraintPath], AmountOfSatVars),
append(AmountOfSatVars, Acc, NAcc), !,
amount_of_sat_vars_csv_records(T, NAcc, Out).
amount_of_sat_vars_csv_records([_|T], Acc, Out) :-
amount_of_sat_vars_csv_records(T, Acc, Out).
Calls:
Name: RECURSIVE_CALL/3 |
Module: smt_solver_benchmarks |
Name: ! |
|
Name: append/3 |
|
| Module: smt_solver_benchmarks | |
Name: format/2 |
|
Name: load_b_eventb_or_tla/1 |
Module: smt_solver_benchmarks |
| Module: smt_solver_benchmarks | |
Name: atom_codes/2 |
|
Name: =/2 |
Called:
| Module: smt_solver_benchmarks |
amount_of_sat_vars_deadlock :-
amount_of_sat_vars(deadlock, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/abz16_m4/', [], Acc1),
amount_of_sat_vars(deadlock, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/abz16_m5/', Acc1, Acc2),
amount_of_sat_vars(deadlock, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/abz16_m6/', Acc2, Acc3),
amount_of_sat_vars(deadlock, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/abz16_m7/', Acc3, Acc4),
amount_of_sat_vars(deadlock, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/r0_geardoor/', Acc4, Acc5),
amount_of_sat_vars(deadlock, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/r1_valve/', Acc5, Acc6),
amount_of_sat_vars(deadlock, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/r2_outputs/', Acc6, Acc7),
amount_of_sat_vars(deadlock, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/r3_sensors/', Acc7, Acc8),
amount_of_sat_vars(deadlock, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/r4_handle/', Acc8, Acc9),
amount_of_sat_vars(deadlock, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/r5_switch/', Acc9, Acc10),
amount_of_sat_vars(deadlock, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/pm_m0_aai/', Acc10, Acc11),
amount_of_sat_vars(deadlock, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/pm_m0_aat/', Acc11, Acc12),
amount_of_sat_vars(deadlock, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/pm_m0_aoo/', Acc12, Acc13),
amount_of_sat_vars(deadlock, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/pm_m0_voo/', Acc13, Acc14),
amount_of_sat_vars(deadlock, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/pm_m0_vvi/', Acc14, Acc15),
amount_of_sat_vars(deadlock, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/pm_m0_vvt/', Acc15, Acc16),
amount_of_sat_vars(deadlock, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/pm_m1_aoor/', Acc16, Acc17),
amount_of_sat_vars(deadlock, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/pm_m1_voor/', Acc17, Acc18),
amount_of_sat_vars(deadlock, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/pm_m2_aai/', Acc18, Acc19),
amount_of_sat_vars(deadlock, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/simple-two-phase/', Acc19, Acc20),
amount_of_sat_vars(deadlock, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/prisoners-4/', Acc20, Acc21),
amount_of_sat_vars(deadlock, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/bakery/', Acc21, Acc22),
amount_of_sat_vars(deadlock, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/paxos-3/', Acc22, Acc23),
amount_of_sat_vars(deadlock, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/lightbot/', Acc23, Acc24),
amount_of_sat_vars(deadlock, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/travel_agency/', Acc24, Acc25),
amount_of_sat_vars(deadlock, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/search_events/', Acc25, Acc26),
amount_of_sat_vars(deadlock, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/large_branching/', Acc26, Acc27),
mean_of_list(Acc27, TotalMean),
median_of_list(Acc27, TotalMedian),
max_member(Max, Acc27),
open('amount_of_sat_vars_deadlock/total.txt', write, Stream),
tell(Stream),
format("Total mean: ~w~nTotal median: ~w~nTotal max: ~w~n", [TotalMean,TotalMedian,Max]),
close(Stream).
Calls:
Name: close/1 |
|
Name: format/2 |
|
Name: tell/1 |
|
Name: open/3 |
|
Name: max_member/2 |
Module: foo_error |
Name: median_of_list/2 |
Module: smt_solver_benchmarks |
Name: mean_of_list/2 |
Module: smt_solver_benchmarks |
Name: amount_of_sat_vars/4 |
Module: smt_solver_benchmarks |
amount_of_sat_vars_for_benchmark([], []).
amount_of_sat_vars_for_benchmark([BenchmarkFilePath|T], [AmountOfSatVars|TAmountOfSatVars]) :-
safe_read_string_from_file(BenchmarkFilePath, utf8, Codes),
parse_formula(Codes, UntypedAst),
type_check_in_machine_context([UntypedAst], [Constraint]),
cdclt_solver:get_amount_of_sat_variables(Constraint, AmountOfSatVars),
amount_of_sat_vars_for_benchmark(T, TAmountOfSatVars).
Calls:
Name: RECURSIVE_CALL/2 |
Module: smt_solver_benchmarks |
| Module: cdclt_solver | |
Name: type_check_in_machine_context/2 |
Module: foo_error |
Name: parse_formula/2 |
Module: foo_error |
Name: safe_read_string_from_file/3 |
Module: foo_error |
Called:
Name: amount_of_sat_vars/4 |
Module: smt_solver_benchmarks |
| Module: smt_solver_benchmarks |
amount_of_sat_vars_in_dir(DirPath) :-
% get amount of SAT variables for all ConstraintPath in all .csv files in the current top-level directory
file_members_of_directory(DirPath, Files),
findall(CsvFile, (member(_-CsvFile, Files), atom_concat(_, '.csv', CsvFile)), CsvFiles),
amount_of_sat_vars_csv_files(CsvFiles, [], LAmountOfVars),
length(LAmountOfVars, Len),
median_of_list(LAmountOfVars, MedianAmountOfSatVars),
mean_of_list(LAmountOfVars, MeanAmountOfSatVars),
max_member(MaxAmountOfSatVars, LAmountOfVars),
format("AmountOfSatVarsList: ~w~nLen: ~w~nMean: ~w~nMedian: ~w~nMax: ~w~n", [LAmountOfVars,Len,MeanAmountOfSatVars,MedianAmountOfSatVars,MaxAmountOfSatVars]).
Calls:
Name: format/2 |
|
Name: max_member/2 |
Module: foo_error |
Name: mean_of_list/2 |
Module: smt_solver_benchmarks |
Name: median_of_list/2 |
Module: smt_solver_benchmarks |
Name: length/2 |
|
| Module: smt_solver_benchmarks | |
Name: findall/3 |
|
Name: file_members_of_directory/2 |
Module: foo_error |
amount_of_sat_vars_inductive_inv :-
amount_of_sat_vars(inductive_inv, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/abz16_m4/', [], Acc1),
amount_of_sat_vars(inductive_inv, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/abz16_m5/', Acc1, Acc2),
amount_of_sat_vars(inductive_inv, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/abz16_m6/', Acc2, Acc3),
amount_of_sat_vars(inductive_inv, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/abz16_m7/', Acc3, Acc4),
amount_of_sat_vars(inductive_inv, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/r0_geardoor/', Acc4, Acc5),
amount_of_sat_vars(inductive_inv, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/r1_valve/', Acc5, Acc6),
amount_of_sat_vars(inductive_inv, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/r2_outputs/', Acc6, Acc7),
amount_of_sat_vars(inductive_inv, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/r3_sensors/', Acc7, Acc8),
amount_of_sat_vars(inductive_inv, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/r4_handle/', Acc8, Acc9),
amount_of_sat_vars(inductive_inv, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/r5_switch/', Acc9, Acc10),
amount_of_sat_vars(inductive_inv, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/pm_m0_aai/', Acc10, Acc11),
amount_of_sat_vars(inductive_inv, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/pm_m0_aat/', Acc11, Acc12),
amount_of_sat_vars(inductive_inv, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/pm_m0_aoo/', Acc12, Acc13),
amount_of_sat_vars(inductive_inv, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/pm_m0_voo/', Acc13, Acc14),
amount_of_sat_vars(inductive_inv, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/pm_m0_vvi/', Acc14, Acc15),
amount_of_sat_vars(inductive_inv, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/pm_m0_vvt/', Acc15, Acc16),
amount_of_sat_vars(inductive_inv, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/pm_m1_aoor/', Acc16, Acc17),
amount_of_sat_vars(inductive_inv, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/pm_m1_voor/', Acc17, Acc18),
amount_of_sat_vars(inductive_inv, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/pm_m2_aai/', Acc18, Acc19),
amount_of_sat_vars(inductive_inv, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/r6_lights/', Acc19, Acc20),
amount_of_sat_vars(inductive_inv, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/prisoners-4/', Acc20, Acc21),
amount_of_sat_vars(inductive_inv, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/bakery/', Acc21, Acc22),
amount_of_sat_vars(inductive_inv, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/paxos-3/', Acc22, Acc23),
amount_of_sat_vars(inductive_inv, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/lightbot/', Acc23, Acc24),
amount_of_sat_vars(inductive_inv, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/travel_agency/', Acc24, Acc25),
amount_of_sat_vars(inductive_inv, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/search_events/', Acc25, Acc26),
amount_of_sat_vars(inductive_inv, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/large_branching/', Acc26, Acc27),
mean_of_list(Acc27, TotalMean),
median_of_list(Acc27, TotalMedian),
max_member(Max, Acc27),
open('amount_of_sat_vars_inductive_inv/total.txt', write, Stream),
tell(Stream),
format("Total mean: ~w~nTotal median: ~w~nTotal max: ~w~n", [TotalMean,TotalMedian,Max]),
close(Stream).
Calls:
Name: close/1 |
|
Name: format/2 |
|
Name: tell/1 |
|
Name: open/3 |
|
Name: max_member/2 |
Module: foo_error |
Name: median_of_list/2 |
Module: smt_solver_benchmarks |
Name: mean_of_list/2 |
Module: smt_solver_benchmarks |
Name: amount_of_sat_vars/4 |
Module: smt_solver_benchmarks |
atomic_list_concat(Atom,Separator,Res) :-
atom_chars(Atom,CAtom),
atomic_list_concat_(CAtom,Separator,List),
maplist(atom_chars,Res,List).
Calls:
Name: maplist/3 |
Module: foo_error |
Name: atomic_list_concat_/3 |
Module: smt_solver_benchmarks |
Name: atom_chars/2 |
Called:
| Module: smt_solver_benchmarks | |
| Module: smt_solver_benchmarks | |
| Module: smt_solver_benchmarks | |
Name: get_filename_from_path/2 |
Module: smt_solver_benchmarks |
atomic_list_concat_([],_,[[]]) :- ! .
atomic_list_concat_([A|As],Sep,[[]|Args]) :-
A=Sep,
atomic_list_concat_(As,Sep,Args).
atomic_list_concat_([A|As],Sep,[[A|Arg]|Args]) :-
A\=Sep,
atomic_list_concat_(As,Sep,[Arg|Args]).
Calls:
Name: RECURSIVE_CALL/3 |
Module: smt_solver_benchmarks |
Name: \=/2 |
|
Name: =/2 |
|
Name: ! |
Called:
Name: atomic_list_concat/3 |
Module: smt_solver_benchmarks |
benchmark(1, [synthesis]) :-
print_enter_benchmark(1),
setup_scheduler,
preferences:temporary_set_preference(time_out, 2500, OldTimeOut),
load_constraint_from_file(prob_examples('public_examples/Synthesis_Tests/constraints/scheduler_inv1_contradiction.pl'), Constraint),
benchmark_misc_constraint(Constraint, FastestSolver, Res, TimeDiff),
asserta(fastest_solver(FastestSolver, Res, TimeDiff)),
preferences:reset_temporary_preference(time_out, OldTimeOut).
benchmark(2, [synthesis]) :-
print_enter_benchmark(2),
setup_scheduler,
preferences:temporary_set_preference(time_out, 2500, OldTimeOut),
load_constraint_from_file(prob_examples('public_examples/Synthesis_Tests/constraints/scheduler_inv2_contradiction.pl'), Constraint),
benchmark_misc_constraint(Constraint, FastestSolver, Res, TimeDiff),
asserta(fastest_solver(FastestSolver, Res, TimeDiff)),
preferences:reset_temporary_preference(time_out, OldTimeOut).
benchmark(3, [synthesis]) :-
print_enter_benchmark(3),
setup_scheduler,
preferences:temporary_set_preference(time_out, 2500, OldTimeOut),
load_constraint_from_file(prob_examples('public_examples/Synthesis_Tests/constraints/scheduler_inv3_contradiction.pl'), Constraint),
benchmark_misc_constraint(Constraint, FastestSolver, Res, TimeDiff),
asserta(fastest_solver(FastestSolver, Res, TimeDiff)),
preferences:reset_temporary_preference(time_out, OldTimeOut).
benchmark(4, [synthesis]) :-
print_enter_benchmark(4),
setup_scheduler,
preferences:temporary_set_preference(time_out, 2500, OldTimeOut),
load_constraint_from_file(prob_examples('public_examples/Synthesis_Tests/constraints/scheduler_inv1.pl'), Constraint),
benchmark_misc_constraint(Constraint, FastestSolver, Res, TimeDiff),
asserta(fastest_solver(FastestSolver, Res, TimeDiff)),
preferences:reset_temporary_preference(time_out, OldTimeOut).
benchmark(5, [synthesis]) :-
% contradiction
print_enter_benchmark(5),
setup_scheduler,
preferences:temporary_set_preference(time_out, 2500, OldTimeOut),
load_constraint_from_file(prob_examples('public_examples/Synthesis_Tests/constraints/scheduler_inv2_contradiction.pl'), Constraint),
benchmark_misc_constraint(Constraint, FastestSolver, Res, TimeDiff),
asserta(fastest_solver(FastestSolver, Res, TimeDiff)),
preferences:reset_temporary_preference(time_out, OldTimeOut).
benchmark(6, [synthesis]) :-
print_enter_benchmark(6),
setup_scheduler,
preferences:temporary_set_preference(time_out, 2500, OldTimeOut),
load_constraint_from_file(prob_examples('public_examples/Synthesis_Tests/constraints/scheduler_inv3.pl'), Constraint),
benchmark_misc_constraint(Constraint, FastestSolver, Res, TimeDiff),
asserta(fastest_solver(FastestSolver, Res, TimeDiff)),
preferences:reset_temporary_preference(time_out, OldTimeOut).
benchmark(7, [synthesis]) :-
print_enter_benchmark(7),
setup_scheduler,
preferences:temporary_set_preference(time_out, 2500, OldTimeOut),
load_constraint_from_file(prob_examples('public_examples/Synthesis_Tests/constraints/scheduler_inv4.pl'), Constraint),
benchmark_misc_constraint(Constraint, FastestSolver, Res, TimeDiff),
asserta(fastest_solver(FastestSolver, Res, TimeDiff)),
preferences:reset_temporary_preference(time_out, OldTimeOut).
benchmark(8, [synthesis]) :-
print_enter_benchmark(8),
setup_scheduler,
preferences:temporary_set_preference(time_out, 2500, OldTimeOut),
load_constraint_from_file(prob_examples('public_examples/Synthesis_Tests/constraints/scheduler_new_process.pl'), Constraint),
benchmark_misc_constraint(Constraint, FastestSolver, Res, TimeDiff),
asserta(fastest_solver(FastestSolver, Res, TimeDiff)),
preferences:reset_temporary_preference(time_out, OldTimeOut).
benchmark(9, [synthesis]) :-
print_enter_benchmark(9),
setup_scheduler,
preferences:temporary_set_preference(time_out, 10000, OldTimeOut),
load_constraint_from_file(prob_examples('public_examples/Synthesis_Tests/constraints/scheduler_delete_process.pl'), Constraint),
benchmark_misc_constraint(Constraint, FastestSolver, Res, TimeDiff),
asserta(fastest_solver(FastestSolver, Res, TimeDiff)),
preferences:reset_temporary_preference(time_out, OldTimeOut).
benchmark(10, [synthesis]) :-
print_enter_benchmark(10),
setup_scheduler,
preferences:temporary_set_preference(time_out, 2500, OldTimeOut),
load_constraint_from_file(prob_examples('public_examples/Synthesis_Tests/constraints/scheduler_set_active.pl'), Constraint),
benchmark_misc_constraint(Constraint, FastestSolver, Res, TimeDiff),
asserta(fastest_solver(FastestSolver, Res, TimeDiff)),
preferences:reset_temporary_preference(time_out, OldTimeOut).
benchmark(11, [synthesis]) :-
% Note: CDCL(T) is much faster than ProB if chr_solver preference is set
print_enter_benchmark(11),
preferences:temporary_set_preference(time_out, 15000, OldTimeOut),
setup_scheduler,
load_constraint_from_file(prob_examples('public_examples/Synthesis_Tests/constraints/scheduler_active_to_waiting_precondition.pl'), Constraint),
benchmark_misc_constraint(Constraint, FastestSolver, Res, TimeDiff),
asserta(fastest_solver(FastestSolver, Res, TimeDiff)),
preferences:reset_temporary_preference(time_out, OldTimeOut).
benchmark(12, [alloy]) :-
print_enter_benchmark(12),
alloy2b:load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/alloy_models/toys/grandpa.als.pl')),
bmachine:b_machine_precompile,
preferences:temporary_set_preference(time_out, 15000, OldTimeOut),
load_constraint_from_file(prob_examples('public_examples/Alloy/constraints/alloy_self_grandpas.pl'), Constraint),
benchmark_misc_constraint(Constraint, FastestSolver, Res, TimeDiff),
asserta(fastest_solver(FastestSolver, Res, TimeDiff)),
preferences:reset_temporary_preference(time_out, OldTimeOut).
benchmark(16, [alloy]) :-
print_enter_benchmark(16),
alloy2b:load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Puzzles/rivercrossing.pl')),
bmachine:b_machine_precompile,
preferences:temporary_set_preference(time_out, 2500, OldTimeOut),
load_constraint_from_file(prob_examples('public_examples/Alloy/constraints/alloy_river_crossing1.pl'), Constraint),
benchmark_misc_constraint(Constraint, FastestSolver, Res, TimeDiff),
asserta(fastest_solver(FastestSolver, Res, TimeDiff)),
preferences:reset_temporary_preference(time_out, OldTimeOut).
benchmark(17, [alloy]) :-
print_enter_benchmark(17),
alloy2b:load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Puzzles/rivercrossing.pl')),
bmachine:b_machine_precompile,
preferences:temporary_set_preference(time_out, 20000, OldTimeOut),
load_constraint_from_file(prob_examples('public_examples/Alloy/constraints/alloy_river_crossing2.pl'), Constraint),
benchmark_misc_constraint(Constraint, FastestSolver, Res, TimeDiff),
asserta(fastest_solver(FastestSolver, Res, TimeDiff)),
preferences:reset_temporary_preference(time_out, OldTimeOut).
benchmark(18, [alloy]) :-
print_enter_benchmark(18),
alloy2b:load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Puzzles/rivercrossing.pl')),
bmachine:b_machine_precompile,
preferences:temporary_set_preference(time_out, 2500, OldTimeOut),
load_constraint_from_file(prob_examples('public_examples/Alloy/constraints/alloy_river_crossing3.pl'), Constraint),
benchmark_misc_constraint(Constraint, FastestSolver, Res, TimeDiff),
asserta(fastest_solver(FastestSolver, Res, TimeDiff)),
preferences:reset_temporary_preference(time_out, OldTimeOut).
benchmark(19, [alloy]) :-
print_enter_benchmark(19),
alloy2b:load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Puzzles/crewalloc.als.pl')),
bmachine:b_machine_precompile,
preferences:temporary_set_preference(time_out, 10000, OldTimeOut),
load_constraint_from_file(prob_examples('public_examples/Alloy/constraints/alloy_crewalloc1.pl'), Constraint),
benchmark_misc_constraint(Constraint, FastestSolver, Res, TimeDiff),
asserta(fastest_solver(FastestSolver, Res, TimeDiff)),
preferences:reset_temporary_preference(time_out, OldTimeOut).
benchmark(20, [alloy]) :-
print_enter_benchmark(20),
alloy2b:load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Puzzles/crewalloc.als.pl')),
bmachine:b_machine_precompile,
preferences:temporary_set_preference(time_out, 2500, OldTimeOut),
load_constraint_from_file(prob_examples('public_examples/Alloy/constraints/alloy_crewalloc2.pl'), Constraint),
benchmark_misc_constraint(Constraint, FastestSolver, Res, TimeDiff),
asserta(fastest_solver(FastestSolver, Res, TimeDiff)),
preferences:reset_temporary_preference(time_out, OldTimeOut).
benchmark(21, [misc]) :-
print_enter_benchmark(21),
preferences:temporary_set_preference(time_out, 2500, OldTimeOut),
Constraint = b(conjunct(b(disjunct(b(disjunct(b(equal(b(identifier(x),integer,[]),b(integer(2),integer,[])),pred,[]),b(equal(b(identifier(y),integer,[]),b(integer(3),integer,[])),pred,[])),pred,[]),b(equal(b(identifier(z),integer,[]),b(integer(4),integer,[])),pred,[])),pred,[]),b(conjunct(b(disjunct(b(not_equal(b(identifier(y),integer,[]),b(integer(3),integer,[])),pred,[]),b(not_equal(b(identifier(x),integer,[]),b(integer(2),integer,[])),pred,[])),pred,[]),b(conjunct(b(disjunct(b(equal(b(identifier(y),integer,[]),b(integer(3),integer,[])),pred,[]),b(not_equal(b(identifier(z),integer,[]),b(integer(4),integer,[])),pred,[])),pred,[]),b(disjunct(b(not_equal(b(identifier(x),integer,[]),b(integer(2),integer,[])),pred,[]),b(equal(b(identifier(z),integer,[]),b(integer(4),integer,[])),pred,[])),pred,[])),pred,[])),pred,[])),pred,[]),
benchmark_misc_constraint(Constraint, FastestSolver, Res, TimeDiff),
asserta(fastest_solver(FastestSolver, Res, TimeDiff)),
preferences:reset_temporary_preference(time_out, OldTimeOut).
Calls:
| Module: preferences | |
Name: asserta/1 |
|
| Module: smt_solver_benchmarks | |
Name: =/2 |
|
| Module: preferences | |
Name: print_enter_benchmark/1 |
Module: smt_solver_benchmarks |
| Module: smt_solver_benchmarks | |
Name: b_machine_precompile/0 |
Module: bmachine |
| Module: alloy2b | |
Name: setup_scheduler/0 |
Module: smt_solver_benchmarks |
Called:
Name: run_misc_benchmarks/0 |
Module: smt_solver_benchmarks |
benchmark_constraint(UseIdlSolver, ConstraintPath, TimeZ3Par, TimeZ3Axm, TimeZ3Cns, TimeZ3Dec, TimeCdclt, TimeCdcltRaw, TimeCdcltIdl, TimeCdcltNoSym, TimeCdcltRawSym, TimeProBComp, TimeProBSym, TimeProB, TimeProBChr, TimeProBCse, TimeSetlog, TimeProBProver, RestartsCdclt, RestartsCdcltRaw, RestartsCdcltIdl, RestartsCdcltNoSym, RestartsCdcltRawSym) :-
bmc_timeout(Timeout),
write(ConstraintPath),nl,
safe_read_string_from_file(ConstraintPath, utf8, Codes),
parse_formula(Codes, UntypedAst),
type_check_in_machine_context([UntypedAst], [Constraint]),
preferences:set_preference(time_out, 2500), % dummy call for clp(fd) jit
solve_predicate(Constraint, _, 1, [use_smt_mode/true,use_clpfd_solver/true,use_chr_solver/false,clean_up_pred,allow_improving_wd_mode/true], _),
%translate:print_bexpr(Constraint),nl,
preferences:set_preference(time_out, Timeout),
write('Solve with Setlog..'),nl,
write(ConstraintPath),nl,
error_manager:reset_errors,
statistics(walltime, [StartSetlog|_]),
solve_pred_with_setlog(Constraint, _, ResSetlog),
statistics(walltime, [StopSetlog|_]),
TimeSetlog is StopSetlog - StartSetlog,
( solved_constraint(ResSetlog)
-> inc_solved_counter(setlog)
; true
),
add_benchmark_result(setlog, ConstraintPath, ResSetlog),
nl,nl,write(ResSetlog),nl,nl,
write('done.'), nl,
preferences:set_preference(time_out, Timeout),
write('Solve with ProB Prover..'),nl,
write(ConstraintPath),nl,
error_manager:reset_errors,
statistics(walltime, [StartProBProver|_]),
( prove_sequent(Constraint)
-> ResProBProver = solution([])
; ResProBProver = contradiction_found
),
statistics(walltime, [StopProBProver|_]),
( solved_constraint(ResProBProver)
-> inc_solved_counter(prob_prover)
; true
),
TimeProBProver is StopProBProver - StartProBProver,
add_benchmark_result(prob_prover, ConstraintPath, ResProBProver),
nl,nl,write(ResProBProver),nl,nl,
write('done.'), nl,
preferences:set_preference(time_out, Timeout),
set_preference(cdclt_use_idl_theory_solver, false),
set_preference(cdclt_perform_static_analysis, false),
set_preference(cdclt_perform_symmetry_breaking, true),
cdclt_solver:init,
write('Solve with Sym-Raw-SMT..'),nl,
write(ConstraintPath),nl,
error_manager:reset_errors,
statistics(walltime, [StartCdcltRawSym|_]),
cdclt_solve_predicate(sym_raw_smt, Constraint, _SolvedPred1, ResCdcltRawSym),
get_amount_of_found_sbps(SBPsRawSym),
asserta(symmetry_breaking_predicates(ConstraintPath,sym_raw_smt,SBPsRawSym)),
%ResCdcltRawSym = no_solution_found(solver_answered_unknown),
statistics(walltime, [StopCdcltRawSym|_]),
(cdclt_sat_solver:restarts(RestartsCdcltRawSym); RestartsCdcltRawSym = 0),
format("Restarts: ~w~n", [RestartsCdcltRawSym]),
TimeCdcltRawSym is StopCdcltRawSym - StartCdcltRawSym,
( solved_constraint(ResCdcltRawSym)
-> inc_solved_counter(sym_raw_smt)
; true
),
add_benchmark_result(sym_raw_smt, ConstraintPath, ResCdcltRawSym),
!,
nl,nl,write(ResCdcltRawSym),nl,nl,
write('done.'), nl,
preferences:set_preference(time_out, Timeout),
set_preference(cdclt_perform_static_analysis, true),
cdclt_solver:init,
write('Solve with Sym-SMT..'),nl,
write(ConstraintPath),nl,
error_manager:reset_errors,
statistics(walltime, [StartCdclt|_]),
cdclt_solve_predicate(sym_smt, Constraint, _SolvedPred2, ResCdclt),
get_amount_of_found_sbps(SBPsSym),
asserta(symmetry_breaking_predicates(ConstraintPath,sym_smt,SBPsSym)),
%ResCdclt = no_solution_found(solver_answered_unknown),
statistics(walltime, [StopCdclt|_]),
(cdclt_sat_solver:restarts(RestartsCdclt); RestartsCdclt = 0),
format("Restarts: ~w~n", [RestartsCdclt]),
TimeCdclt is StopCdclt - StartCdclt,
( solved_constraint(ResCdclt)
-> inc_solved_counter(sym_smt)
; true
),
add_benchmark_result(sym_smt, ConstraintPath, ResCdclt),
!,
nl,nl,write(ResCdclt),nl,nl,
write('done.'), nl,
preferences:set_preference(time_out, Timeout),
( UseIdlSolver
-> set_preference(cdclt_perform_symmetry_breaking, false),
set_preference(cdclt_use_idl_theory_solver, true),
cdclt_solver:init,
preferences:set_preference(time_out, Timeout),
write('Solve with IDL-SMT..'),nl,
error_manager:reset_errors,
statistics(walltime, [StartCdcltIdl|_]),
cdclt_solve_predicate(idl_smt, Constraint, _SolvedPred3, ResCdcltIdl),
%ResCdcltIdl = no_solution_found(solver_answered_unknown),
statistics(walltime, [StopCdcltIdl|_]),
(cdclt_sat_solver:restarts(RestartsCdcltIdl); RestartsCdcltIdl = 0),
format("Restarts: ~w~n", [RestartsCdcltIdl]),
TimeCdcltIdl is StopCdcltIdl - StartCdcltIdl,
( solved_constraint(ResCdcltIdl)
-> inc_solved_counter(idl_smt)
; true
),
add_benchmark_result(idl_smt, ConstraintPath, ResCdcltIdl),
!,
set_preference(cdclt_use_idl_theory_solver, false),
set_preference(cdclt_perform_symmetry_breaking, true)
; TimeCdcltIdl = 0,
RestartsCdcltIdl = 0,
ResCdcltIdl = none
),
nl,nl,write(ResCdcltIdl),nl,nl,
write('done.'), nl,
preferences:set_preference(time_out, Timeout),
set_preference(cdclt_perform_symmetry_breaking, false),
cdclt_solver:init,
preferences:set_preference(time_out, Timeout),
write('Solve with SMT..'),nl,
write(ConstraintPath),nl,
error_manager:reset_errors,
statistics(walltime, [StartCdcltNoSym|_]),
cdclt_solve_predicate(smt, Constraint, _, ResCdcltNoSym),
%ResCdcltNoSym = no_solution_found(solver_answered_unknown),
statistics(walltime, [StopCdcltNoSym|_]),
(cdclt_sat_solver:restarts(RestartsCdcltNoSym); RestartsCdcltNoSym = 0),
format("Restarts: ~w~n", [RestartsCdcltNoSym]),
TimeCdcltNoSym is StopCdcltNoSym - StartCdcltNoSym,
( solved_constraint(ResCdcltNoSym)
-> inc_solved_counter(smt)
; true
),
add_benchmark_result(smt, ConstraintPath, ResCdcltNoSym),
!,
nl,nl,write(ResCdcltNoSym),nl,nl,
write('done.'), nl,
preferences:set_preference(time_out, Timeout),
set_preference(cdclt_perform_static_analysis, false),
set_preference(cdclt_perform_symmetry_breaking, false),
cdclt_solver:init,
preferences:set_preference(time_out, Timeout),
write('Solve with Raw-SMT..'),nl,
write(ConstraintPath),nl,
error_manager:reset_errors,
statistics(walltime, [StartCdcltRaw|_]),
cdclt_solve_predicate(raw_smt, Constraint, _, ResCdcltRaw),
%ResCdcltRaw = no_solution_found(solver_answered_unknown),
statistics(walltime, [StopCdcltRaw|_]),
(cdclt_sat_solver:restarts(RestartsCdcltRaw); RestartsCdcltRaw = 0),
format("Restarts: ~w~n", [RestartsCdcltRaw]),
TimeCdcltRaw is StopCdcltRaw - StartCdcltRaw,
( solved_constraint(ResCdcltRaw)
-> inc_solved_counter(raw_smt)
; true
),
add_benchmark_result(raw_smt, ConstraintPath, ResCdcltRaw),
!,
nl,nl,write(ResCdcltRaw),nl,nl,
write('done.'), nl,
preferences:set_preference(time_out, Timeout),
set_preference(cdclt_perform_static_analysis,true),
set_preference(cdclt_perform_symmetry_breaking,true),
write('Solve with Z3-Par..'),nl,
write(ConstraintPath),nl,
error_manager:reset_errors,
statistics(walltime, [StartZ3Par|_]),
smt_solve_predicate(z3,Constraint, _, ResZ3Par),
%ResZ3Par = no_solution_found(solver_answered_unknown),
statistics(walltime, [StopZ3Par|_]),
TimeZ3Par is StopZ3Par - StartZ3Par,
( solved_constraint(ResZ3Par)
-> inc_solved_counter(z3par)
; true
),
add_benchmark_result(z3par, ConstraintPath, ResZ3Par),
!,
nl,nl,write(ResZ3Par),nl,nl,
preferences:set_preference(time_out, Timeout),
write('Solve with Z3-Axm..'),nl,
write(ConstraintPath),nl,
error_manager:reset_errors,
statistics(walltime, [StartZ3Axm|_]),
smt_solve_predicate(z3axm,Constraint, _, ResZ3Axm),
%ResZ3Axm = no_solution_found(solver_answered_unknown),
statistics(walltime, [StopZ3Axm|_]),
TimeZ3Axm is StopZ3Axm - StartZ3Axm,
( solved_constraint(ResZ3Axm)
-> inc_solved_counter(z3axm)
; true
),
add_benchmark_result(z3axm, ConstraintPath, ResZ3Axm),
!,
nl,nl,write(ResZ3Axm),nl,nl,
preferences:set_preference(time_out, Timeout),
write('Solve with Z3-Cns..'),nl,
write(ConstraintPath),nl,
error_manager:reset_errors,
statistics(walltime, [StartZ3Cns|_]),
smt_solve_predicate(z3cns,Constraint, _, ResZ3Cns),
%ResZ3Cns = no_solution_found(solver_answered_unknown),
statistics(walltime, [StopZ3Cns|_]),
TimeZ3Cns is StopZ3Cns - StartZ3Cns,
( solved_constraint(ResZ3Cns)
-> inc_solved_counter(z3cns)
; true
),
add_benchmark_result(z3cns, ConstraintPath, ResZ3Cns),
!,
nl,nl,write(ResZ3Cns),nl,nl,
preferences:set_preference(time_out, Timeout),
write('Solve with Z3-Dec..'),nl,
write(ConstraintPath),nl,
error_manager:reset_errors,
statistics(walltime, [StartZ3Dec|_]),
smt_solve_predicate(z3, [decompose_into_components], Constraint, _, ResZ3Dec),
%ResZ3Dec = no_solution_found(solver_answered_unknown),
statistics(walltime, [StopZ3Dec|_]),
TimeZ3Dec is StopZ3Dec - StartZ3Dec,
( solved_constraint(ResZ3Dec)
-> inc_solved_counter(z3dec)
; true
),
add_benchmark_result(z3dec, ConstraintPath, ResZ3Dec),
!,
nl,nl,write(ResZ3Dec),nl,nl,
preferences:set_preference(time_out, Timeout),
write('Solve with Sym-ProB..'),nl,
write(ConstraintPath),nl,
error_manager:reset_errors,
preferences:set_preference(use_chr_solver, false),
preferences:set_preference(use_common_subexpression_elimination, false),
preferences:set_preference(use_common_subexpression_also_for_predicates, false),
statistics(walltime, [StartProBSym|_]),
clean_up_pred(Constraint, [], CConstraint),
(add_symmetry_breaking_predicates(CConstraint, SymConstraint), !; SymConstraint = CConstraint),
get_amount_of_found_sbps(FoundSBPs),
asserta(symmetry_breaking_predicates(ConstraintPath,prob_sym,FoundSBPs)),
solve_predicate(SymConstraint, _, 1, [use_smt_mode/true,use_clpfd_solver/true,clean_up_pred,use_chr_solver/false,allow_improving_wd_mode/true], ResProBSym),
%ResProBSym = no_solution_found(solver_answered_unknown),
statistics(walltime, [StopProBSym|_]),
TimeProBSym is StopProBSym - StartProBSym,
( solved_constraint(ResProBSym)
-> inc_solved_counter(prob_sym)
; true
),
add_benchmark_result(prob_sym, ConstraintPath, ResProBSym),
!,
nl,nl,write(ResProBSym),nl,nl,
preferences:set_preference(time_out, Timeout),
write('Solve with ProB..'),nl,
write(ConstraintPath),nl,
error_manager:reset_errors,
preferences:set_preference(use_chr_solver, false),
preferences:set_preference(use_common_subexpression_elimination, false),
preferences:set_preference(use_common_subexpression_also_for_predicates, false),
statistics(walltime, [StartProB|_]),
solve_predicate(Constraint, _, 1, [use_smt_mode/true,use_clpfd_solver/true,use_chr_solver/false,clean_up_pred,allow_improving_wd_mode/true], ResProB),
%ResProB = no_solution_found(solver_answered_unknown),
statistics(walltime, [StopProB|_]),
TimeProB is StopProB - StartProB,
( solved_constraint(ResProB)
-> inc_solved_counter(prob)
; true
),
add_benchmark_result(prob, ConstraintPath, ResProB),
!,
nl,nl,write(ResProB),nl,nl,
write('Solve with ProB-CHR..'),nl,
preferences:set_preference(time_out, Timeout),
write(ConstraintPath),nl,
error_manager:reset_errors,
preferences:set_preference(use_chr_solver, true),
preferences:set_preference(use_common_subexpression_elimination, false),
preferences:set_preference(use_common_subexpression_also_for_predicates, false),
statistics(walltime, [StartProBChr|_]),
solve_predicate(Constraint, _, 1, [use_smt_mode/true,use_clpfd_solver/true,use_chr_solver/true,clean_up_pred,allow_improving_wd_mode/true], ResProBChr),
%ResProBChr = no_solution_found(solver_answered_unknown),
statistics(walltime, [StopProBChr|_]),
TimeProBChr is StopProBChr - StartProBChr,
( solved_constraint(ResProBChr)
-> inc_solved_counter(prob_chr)
; true
),
add_benchmark_result(prob_chr, ConstraintPath, ResProBChr),
!,
nl,nl,write(ResProBChr),nl,nl,
write('Solve with ProB-CSE..'),nl,
write(ConstraintPath),nl,
error_manager:reset_errors,
preferences:set_preference(use_chr_solver, false),
preferences:set_preference(use_common_subexpression_elimination, true),
preferences:set_preference(use_common_subexpression_also_for_predicates, true),
statistics(walltime, [StartProBCse|_]),
%solve_predicate(Constraint, _, 1, [use_smt_mode/true,use_clpfd_solver/true,use_chr_solver/false,clean_up_pred,allow_improving_wd_mode/true], ResProBCse),
ResProBCse = no_solution_found(solver_answered_unknown),
statistics(walltime, [StopProBCse|_]),
TimeProBCse is StopProBCse - StartProBCse,
( solved_constraint(ResProBCse)
-> inc_solved_counter(prob_cse)
; true
),
add_benchmark_result(prob_cse, ConstraintPath, ResProBCse),
!,
nl,nl,write(ResProBCse),nl,nl,
write('Solve with ProB-Comp..'),nl,
statistics(walltime, [StartProBComp|_]),
find_identifier_uses(Constraint, [], UsedIds),
temporary_set_preference(data_validation_mode, true),
catch(b_compile(Constraint, UsedIds, [], [], AstCompiled, no_wf_available),
enumeration_warning(_,_,_,_,_), % cancel if enumeration warning has occurred
AstCompiled = Constraint),
clear_wd_errors, % b_compile might throw a wd error
reset_temporary_preference(data_validation_mode),
%solve_predicate(AstCompiled, _, 1, [use_smt_mode/true,use_clpfd_solver/true,use_chr_solver/false,clean_up_pred,allow_improving_wd_mode/true], ResProBComp),
ResProBComp = no_solution_found(solver_answered_unknown),
statistics(walltime, [StopProBComp|_]),
TimeProBComp is StopProBComp - StartProBComp,
( solved_constraint(ResProBComp)
-> inc_solved_counter(prob_comp)
; true
),
add_benchmark_result(prob_comp, ConstraintPath, ResProBComp),
!,
nl,nl,write(ResProBComp),nl,nl,
write('done.'), nl.
Calls:
Name: nl |
|
Name: write/1 |
|
Name: ! |
|
Name: add_benchmark_result/3 |
Module: smt_solver_benchmarks |
Name: true |
|
Name: inc_solved_counter/1 |
Module: smt_solver_benchmarks |
Name: solved_constraint/1 |
Module: smt_solver_benchmarks |
Name: ->/3 |
|
Name: is/2 |
|
Name: statistics/2 |
|
Name: =/2 |
|
Name: reset_temporary_preference/1 |
Module: foo_error |
Name: clear_wd_errors |
Module: foo_error |
Name: catch/3 |
|
Name: temporary_set_preference/2 |
Module: foo_error |
Name: find_identifier_uses/3 |
Module: foo_error |
Name: set_preference/2 |
Module: preferences |
Name: reset_errors/0 |
Module: error_manager |
Name: solve_predicate/5 |
Module: foo_error |
Name: asserta/1 |
|
Name: get_amount_of_found_sbps/1 |
Module: foo_error |
Name: add_symmetry_breaking_predicates/2 |
Module: foo_error |
Name: clean_up_pred/3 |
Module: b_ast_cleanup |
Name: smt_solve_predicate/5 |
Module: foo_error |
Name: smt_solve_predicate/4 |
Module: foo_error |
Name: set_preference/2 |
Module: foo_error |
Name: format/2 |
|
Name: restarts/1 |
Module: cdclt_sat_solver |
Name: cdclt_solve_predicate/4 |
Module: foo_error |
Name: init/0 |
Module: cdclt_solver |
Name: call/1 |
|
Name: prove_sequent/1 |
Module: well_def/well_def_analyser |
Name: solve_pred_with_setlog/3 |
Module: foo_error |
Name: type_check_in_machine_context/2 |
Module: foo_error |
Name: parse_formula/2 |
Module: foo_error |
Name: safe_read_string_from_file/3 |
Module: foo_error |
Name: bmc_timeout/1 |
Module: smt_solver_benchmarks |
Called:
Name: benchmark_constraints/4 |
Module: smt_solver_benchmarks |
benchmark_constraints(_, [], Acc, Acc).
benchmark_constraints(UseIdlSolver, [ConstraintPath|T], Acc, Data) :-
benchmark_constraint(UseIdlSolver, ConstraintPath, TimeZ3Par, TimeZ3Axm, TimeZ3Cns, TimeZ3Dec, TimeCdclt, TimeCdcltRaw, TimeCdcltIdl, TimeCdcltNoSym, TimeCdcltRawSym, TimeProBComp, TimeProBSym, TimeProB, TimeProBChr, TimeProBCse, TimeSetlog, TimeProBProver, RestartsCdclt, RestartsCdcltRaw, RestartsCdcltIdl, RestartsCdcltNoSym, RestartsCdcltRawSym), !,
!,
benchmark_constraints(UseIdlSolver, T, [(ConstraintPath,TimeZ3Par,TimeZ3Axm,TimeZ3Cns,TimeZ3Dec,TimeCdclt,TimeCdcltRaw,TimeCdcltIdl,TimeCdcltNoSym,TimeCdcltRawSym,TimeProBComp,TimeProBSym,TimeProB,TimeProBChr,TimeProBCse,TimeSetlog,TimeProBProver,RestartsCdclt,RestartsCdcltRaw,RestartsCdcltIdl,RestartsCdcltNoSym,RestartsCdcltRawSym)|Acc], Data).
benchmark_constraints(UseIdlSolver, [_|T], Acc, Data) :-
format("Skipped constraints due to error~n", []),
benchmark_constraints(UseIdlSolver, T, Acc, Data).
Calls:
Name: RECURSIVE_CALL/4 |
Module: smt_solver_benchmarks |
Name: format/2 |
|
Name: ! |
|
Name: benchmark_constraint/23 |
Module: smt_solver_benchmarks |
Called:
| Module: smt_solver_benchmarks | |
| Module: smt_solver_benchmarks | |
| Module: smt_solver_benchmarks | |
Name: run_bmc_benchmarks/2 |
Module: smt_solver_benchmarks |
benchmark_misc_constraint(Constraint, FastestSolver, Res, TimeDiff) :-
preferences:set_preference(randomise_enumeration_order, false),
format("Solve with ProB..~n", []),
statistics(walltime, [ProBStart|_]),
%kodkod_annotator:annotate_kodkod_constraints(greedy, Constraint, AConstraint),
solve_predicate(Constraint, _, 1, [use_smt_mode/true,use_clpfd_solver/true,clean_up_pred,allow_improving_wd_mode/true], ProBRes),
statistics(walltime, [ProBEnd|_]),
format("~nProB result: ~w~n", [ProBRes]),
ProBTime is ProBEnd - ProBStart,
format("ProB finished.~nSolve with CDCL(T)..~n", []),
statistics(walltime, [CDCLTStart|_]),
cdclt_solve_predicate(Constraint, _, CDCLTRes),
statistics(walltime, [CDCLTEnd|_]),
format("~nCDCL(T) result: ~w~n", [CDCLTRes]),
format("CDCL(T) finished..~n", []),
CDCLTTime is CDCLTEnd - CDCLTStart,
print_times(ProBTime, CDCLTTime),
!,
( ProBRes = solution(_),
( CDCLTRes == contradiction_found
; CDCLTRes == error),
format('Error found: ProB found a solution while CDCL(T) did not.', []),
trace
; ProBRes = contradiction_found,
( CDCLTRes = solution(_)
; CDCLTRes == error),
format('Error found: ProB found a contradiction while CDCL(T) did not.', []),
trace
; CDCLTRes == time_out,
ProBRes == time_out,
Res = time_out,
FastestSolver = same,
TimeDiff = 0
; ProBRes == time_out,
solution_or_contradiction(CDCLTRes, Res),
!,
FastestSolver = cdclt,
TimeDiff is ProBTime - CDCLTTime
; CDCLTRes == time_out,
solution_or_contradiction(ProBRes, Res),
!,
FastestSolver = prob,
TimeDiff is CDCLTTime - ProBTime
; % ProB could not find a result but CDCL(T)
ProBRes = no_solution_found(_),
solution_or_contradiction(CDCLTRes, Res),
!,
FastestSolver = cdclt,
TimeDiff = 0
; % CDCL(T) could not find a result but ProB
CDCLTRes = no_solution_found(_),
solution_or_contradiction(ProBRes, Res),
!,
FastestSolver = prob,
TimeDiff = 0
; CDCLTTime < ProBTime,
FastestSolver = cdclt,
solution_or_contradiction(CDCLTRes, Res),
TimeDiff is ProBTime - CDCLTTime
; CDCLTTime > ProBTime,
FastestSolver = prob,
solution_or_contradiction(CDCLTRes, Res),
TimeDiff is CDCLTTime - ProBTime
; CDCLTTime == ProBTime,
FastestSolver = same,
solution_or_contradiction(CDCLTRes, Res),
TimeDiff = 0),!.
Calls:
Name: ! |
|
Name: =/2 |
|
| Module: smt_solver_benchmarks | |
Name: ==/2 |
|
Name: is/2 |
|
Name: >/2 |
|
Name: </2 |
|
Name: trace |
|
Name: format/2 |
|
Name: print_times/2 |
Module: smt_solver_benchmarks |
Name: statistics/2 |
|
Name: cdclt_solve_predicate/3 |
Module: foo_error |
Name: solve_predicate/5 |
Module: foo_error |
Name: set_preference/2 |
Module: preferences |
Called:
Name: benchmark/2 |
Module: smt_solver_benchmarks |
bmc_timeout(120000).
Called:
Name: benchmark_constraint/23 |
Module: smt_solver_benchmarks |
Name: run_bmc_benchmarks1/0 |
Module: smt_solver_benchmarks |
Name: run_bmc_benchmarks6/0 |
Module: smt_solver_benchmarks |
Name: run_bmc_benchmarks3/0 |
Module: smt_solver_benchmarks |
Name: run_bmc_benchmarks4/0 |
Module: smt_solver_benchmarks |
Name: run_bmc_benchmarks22/0 |
Module: smt_solver_benchmarks |
Name: run_bmc_benchmarks5/0 |
Module: smt_solver_benchmarks |
Name: run_bmc_benchmarks11/0 |
Module: smt_solver_benchmarks |
Name: run_bmc_benchmarks2/0 |
Module: smt_solver_benchmarks |
Name: run_bmc_benchmarks33/0 |
Module: smt_solver_benchmarks |
deadlock_timeout(120000).
Called:
| Module: smt_solver_benchmarks | |
| Module: smt_solver_benchmarks | |
| Module: smt_solver_benchmarks | |
| Module: smt_solver_benchmarks | |
| Module: smt_solver_benchmarks | |
| Module: smt_solver_benchmarks |
eval_amount_of_sat_vars(BenchmarkName, AmountOfSatVars) :-
bmachine:b_machine_name(MachineName),
atom_concat(MachineName, 'amount_of_sat_vars.txt', OutPath1),
atom_concat('amount_of_sat_vars_', BenchmarkName, OutFolder1),
atom_concat(OutFolder1, '/', OutFolder),
atom_concat(OutFolder, OutPath1, OutPath),
mean_of_list(AmountOfSatVars, MeanAmountOfSatVars),
median_of_list(AmountOfSatVars, MedianAmountOfSatVars),
open(OutPath, write, Stream),
tell(Stream),
format("AmountOfSatVarsList: ~w~nMean: ~w~nMedian: ~w~n", [AmountOfSatVars, MeanAmountOfSatVars, MedianAmountOfSatVars]),
close(Stream).
Calls:
Name: close/1 |
|
Name: format/2 |
|
Name: tell/1 |
|
Name: open/3 |
|
Name: median_of_list/2 |
Module: smt_solver_benchmarks |
Name: mean_of_list/2 |
Module: smt_solver_benchmarks |
Name: atom_concat/3 |
|
Name: b_machine_name/1 |
Module: bmachine |
Called:
Name: amount_of_sat_vars/4 |
Module: smt_solver_benchmarks |
eval_benchmark_data_csv(OutputPath, MachineName, Description, Data) :-
format("Evaluate benchmarks ~w for detailed CSV~n", [Description]),
findall((ConstraintPath,TimeZ3Par), member((ConstraintPath,TimeZ3Par,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_), Data), DataZ3Par),
findall((ConstraintPath,TimeZ3Axm), member((ConstraintPath,_,TimeZ3Axm,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_), Data), DataZ3Axm),
findall((ConstraintPath,TimeZ3Cns), member((ConstraintPath,_,_,TimeZ3Cns,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_), Data), DataZ3Cns),
findall((ConstraintPath,TimeZ3Dec), member((ConstraintPath,_,_,_,TimeZ3Dec,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_), Data), DataZ3Dec),
findall((ConstraintPath,TimeCdclt), member((ConstraintPath,_,_,_,_,TimeCdclt,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_), Data), DataCdclt),
findall((ConstraintPath,TimeCdcltRaw), member((ConstraintPath,_,_,_,_,_,TimeCdcltRaw,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_), Data), DataCdcltRaw),
findall((ConstraintPath,TimeCdcltIdl), member((ConstraintPath,_,_,_,_,_,_,TimeCdcltIdl,_,_,_,_,_,_,_,_,_,_,_,_,_,_), Data), DataCdcltIdl),
findall((ConstraintPath,TimeCdcltNoSym), member((ConstraintPath,_,_,_,_,_,_,_,TimeCdcltNoSym,_,_,_,_,_,_,_,_,_,_,_,_,_), Data), DataCdcltNoSym),
findall((ConstraintPath,TimeCdcltRawSym), member((ConstraintPath,_,_,_,_,_,_,_,_,TimeCdcltRawSym,_,_,_,_,_,_,_,_,_,_,_,_), Data), DataCdcltRawSym),
findall((ConstraintPath,TimeProBComp), member((ConstraintPath,_,_,_,_,_,_,_,_,_,TimeProBComp,_,_,_,_,_,_,_,_,_,_), Data), DataProBComp),
findall((ConstraintPath,TimeProBSym), member((ConstraintPath,_,_,_,_,_,_,_,_,_,_,TimeProBSym,_,_,_,_,_,_,_,_,_,_), Data), DataProBSym),
findall((ConstraintPath,TimeProB), member((ConstraintPath,_,_,_,_,_,_,_,_,_,_,_,TimeProB,_,_,_,_,_,_,_,_,_), Data), DataProB),
findall((ConstraintPath,TimeProBChr), member((ConstraintPath,_,_,_,_,_,_,_,_,_,_,_,_,TimeProBChr,_,_,_,_,_,_,_,_), Data), DataProBChr),
findall((ConstraintPath,TimeProBCse), member((ConstraintPath,_,_,_,_,_,_,_,_,_,_,_,_,_,TimeProBCse,_,_,_,_,_,_,_), Data), DataProBCse),
findall((ConstraintPath,TimeSetlog), member((ConstraintPath,_,_,_,_,_,_,_,_,_,_,_,_,_,_,TimeSetlog,_,_,_,_,_,_), Data), DataSetlog),
findall((ConstraintPath,TimeProBProver), member((ConstraintPath,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,TimeProBProver,_,_,_,_,_), Data), DataProBProver),
start_csv_stream(OutputPath, MachineName, Stream),
tell(Stream),
write_to_csv_stream(z3par, MachineName, DataZ3Par),
write_to_csv_stream(z3axm, MachineName, DataZ3Axm),
write_to_csv_stream(z3cns, MachineName, DataZ3Cns),
write_to_csv_stream(z3dec, MachineName, DataZ3Dec),
write_to_csv_stream(smt, MachineName, DataCdcltNoSym),
write_to_csv_stream(sym_smt, MachineName, DataCdclt),
write_to_csv_stream(raw_smt, MachineName, DataCdcltRaw),
write_to_csv_stream(idl_smt, MachineName, DataCdcltIdl),
write_to_csv_stream(sym_raw_smt, MachineName, DataCdcltRawSym),
write_to_csv_stream(prob_comp, MachineName, DataProBComp),
write_to_csv_stream(prob_sym, MachineName, DataProBSym),
write_to_csv_stream(prob, MachineName, DataProB),
write_to_csv_stream(prob_chr, MachineName, DataProBChr),
write_to_csv_stream(prob_cse, MachineName, DataProBCse),
write_to_csv_stream(setlog, MachineName, DataSetlog),
write_to_csv_stream(prob_prover, MachineName, DataProBProver),
close(Stream).
Calls:
Name: close/1 |
|
Name: write_to_csv_stream/3 |
Module: smt_solver_benchmarks |
Name: tell/1 |
|
Name: start_csv_stream/3 |
Module: smt_solver_benchmarks |
Name: findall/3 |
|
Name: format/2 |
Called:
| Module: smt_solver_benchmarks | |
Name: run_bmc_benchmarks/2 |
Module: smt_solver_benchmarks |
| Module: smt_solver_benchmarks | |
| Module: smt_solver_benchmarks |
eval_cbc_benchmark_data(FolderPath, FileName-BenchmarkFilePath, ResCdcltRawSym, TimeCdcltRawSym, RestartsCdcltRawSym, ResCdclt, TimeCdclt, RestartsCdclt, ResCdcltNoSym, TimeCdcltNoSym, RestartsCdcltNoSym, ResCdcltIdl, TimeCdcltIdl, RestartsCdcltIdl, ResCdcltRaw, TimeCdcltRaw, RestartsCdcltRaw, ResZ3, TimeZ3, ResProB, TimeProB) :-
atom_concat(FileNameNoExt, '.eval', FileName),
atom_concat('benchmark_cbc_results_', FileNameNoExt, TResultsPath),
atom_concat(TResultsPath, '.csv', TTResultsPath),
atom_concat(FolderPath, TTResultsPath, ResultsPath),
open(ResultsPath, write, Stream),
tell(Stream),
format("ConstraintPath,Solver,Result,Time (ms),Restarts~n", []),
format("~w,~w,~w,~w,~w~n", [BenchmarkFilePath,prob,ResProB,TimeProB,-1]),
format("~w,~w,~w,~w,~w~n", [BenchmarkFilePath,z3par,ResZ3,TimeZ3,-1]),
format("~w,~w,~w,~w,~w~n", [BenchmarkFilePath,sym_smt,ResCdclt,TimeCdclt,RestartsCdclt]),
format("~w,~w,~w,~w,~w~n", [BenchmarkFilePath,smt,ResCdcltNoSym,TimeCdcltNoSym,RestartsCdcltNoSym]),
format("~w,~w,~w,~w,~w~n", [BenchmarkFilePath,smt_idl,ResCdcltIdl,TimeCdcltIdl,RestartsCdcltIdl]),
format("~w,~w,~w,~w,~w~n", [BenchmarkFilePath,raw_smt,ResCdcltRaw,TimeCdcltRaw,RestartsCdcltRaw]),
format("~w,~w,~w,~w,~w~n", [BenchmarkFilePath,sym_raw_smt,ResCdcltRawSym,TimeCdcltRawSym,RestartsCdcltRawSym]),
close(Stream),
!.
Calls:
Name: ! |
|
Name: close/1 |
|
Name: format/2 |
|
Name: tell/1 |
|
Name: open/3 |
|
Name: atom_concat/3 |
Called:
Name: run_cbc_benchmark/4 |
Module: smt_solver_benchmarks |
filter_fastest_solver(Name, LFastestSolver, SolAmount, ContrAmount, TimeoutsAmount, TimeDiff) :-
findall(TimeDiff, member(Name-solution-TimeDiff, LFastestSolver), Solutions),
findall(TimeDiff, member(Name-contradiction-TimeDiff, LFastestSolver), Contradictions),
findall(TimeDiff, member(Name-time_out-TimeDiff, LFastestSolver), Timeouts),
length(Solutions, SolAmount),
length(Contradictions, ContrAmount),
length(Timeouts, TimeoutsAmount),
sumlist(Solutions, TimeDiff1),
sumlist(Contradictions, TimeDiff2),
TimeDiff is TimeDiff1 + TimeDiff2.
Calls:
Name: is/2 |
|
Name: sumlist/2 |
Module: foo_error |
Name: length/2 |
|
Name: findall/3 |
Called:
| Module: smt_solver_benchmarks |
get_file_paths_from_config(ConfigPath, MachineFile, ConstraintPaths, Description, MachineName) :-
open(ConfigPath, read, Stream),
read(Stream, Config),
close(Stream),
Config = benchmark_config(Description, MachineFile, MachineName, MaxBound),
int_range(0, MaxBound, KRange),
findall(ConstraintPath,
(member(K, KRange), atom_concat(MachineName, '_monolithic_bmc_k_', T1),
number_codes(K, CK), atom_codes(AK, CK),
atom_concat(T1, AK, T2), atom_concat(T2, '.eval', ConstraintPath)),
ConstraintPaths).
Calls:
Name: findall/3 |
|
Name: int_range/3 |
Module: smt_solver_benchmarks |
Name: =/2 |
|
Name: close/1 |
|
Name: read/2 |
|
Name: open/3 |
Called:
Name: run_bmc_benchmarks/2 |
Module: smt_solver_benchmarks |
get_filename_from_path(MachinePath, FileName) :-
atomic_list_concat(MachinePath, '/', Split),
last(Split, FileNameExt),
atomic_list_concat(FileNameExt, '.', Split2),
Split2 = [FileName|_].
Calls:
Name: =/2 |
|
Name: atomic_list_concat/3 |
Module: smt_solver_benchmarks |
Name: last/2 |
Module: foo_error |
Called:
| Module: smt_solver_benchmarks | |
| Module: smt_solver_benchmarks | |
| Module: smt_solver_benchmarks |
get_machine_path_from_bmc_bench_path(ConstraintPath, MachinePath) :-
atom_concat('/home/joshua/raw_benchmarks/additional_benchmarks_bmc/', Postfix, ConstraintPath),
atomic_list_concat(Postfix, '_', Split),
append(PreSplit, [monolithic,bmc|_], Split),
join_atom_list(PreSplit, '_', PreClean),
atom_concat('../prob_examples/', PreClean, FullPrefix),
atom_concat(FullPrefix, '.mch', MchPath),
atom_concat(FullPrefix, '.eventb', EventBPath),
atom_concat(FullPrefix, '.tla', TlaPath),
( file_exists(MchPath)
-> MachinePath = MchPath
; file_exists(EventBPath)
-> MachinePath = EventBPath
; file_exists(TlaPath),
MachinePath = TlaPath
).
Calls:
Name: =/2 |
|
Name: file_exists/1 |
Module: foo_error |
Name: ->/3 |
|
Name: atom_concat/3 |
|
Name: join_atom_list/3 |
Module: smt_solver_benchmarks |
Name: append/3 |
|
Name: atomic_list_concat/3 |
Module: smt_solver_benchmarks |
Called:
| Module: smt_solver_benchmarks |
get_machine_path_from_deadlock_freedom_bench_path(ConstraintPath, MachinePath) :-
atom_concat('/home/joshua/raw_benchmarks/additional_benchmarks_deadlock/', Postfix, ConstraintPath),
atomic_list_concat(Postfix, '_', Split),
append(PreSplit, [deadlock,'freedom.eval'|_], Split),
join_atom_list(PreSplit, '_', PreClean),
atom_concat('../prob_examples/', PreClean, FullPrefix),
atom_concat(FullPrefix, '.mch', MchPath),
atom_concat(FullPrefix, '.eventb', EventBPath),
atom_concat(FullPrefix, '.tla', TlaPath),
( file_exists(MchPath)
-> MachinePath = MchPath
; file_exists(EventBPath)
-> MachinePath = EventBPath
; file_exists(TlaPath),
MachinePath = TlaPath
).
Calls:
Name: =/2 |
|
Name: file_exists/1 |
Module: foo_error |
Name: ->/3 |
|
Name: atom_concat/3 |
|
Name: join_atom_list/3 |
Module: smt_solver_benchmarks |
Name: append/3 |
|
Name: atomic_list_concat/3 |
Module: smt_solver_benchmarks |
get_machine_path_from_inductive_inv_bench_path(ConstraintPath, MachinePath) :-
atom_concat('/home/joshua/raw_benchmarks/additional_benchmarks_inductive_inv/', Postfix, ConstraintPath),
atomic_list_concat(Postfix, '_', Split),
append(PreSplit, [inductive,inv|_], Split),
join_atom_list(PreSplit, '_', PreClean),
atom_concat('../prob_examples/', PreClean, FullPrefix),
atom_concat(FullPrefix, '.mch', MchPath),
atom_concat(FullPrefix, '.eventb', EventBPath),
atom_concat(FullPrefix, '.tla', TlaPath),
( file_exists(MchPath)
-> MachinePath = MchPath
; file_exists(EventBPath)
-> MachinePath = EventBPath
; file_exists(TlaPath),
MachinePath = TlaPath
).
Calls:
Name: =/2 |
|
Name: file_exists/1 |
Module: foo_error |
Name: ->/3 |
|
Name: atom_concat/3 |
|
Name: join_atom_list/3 |
Module: smt_solver_benchmarks |
Name: append/3 |
|
Name: atomic_list_concat/3 |
Module: smt_solver_benchmarks |
inc_solved_counter(Solver) :-
(retract(solved_constraints(Solver, Old)); Old = 0),
!,
New is Old + 1,
asserta(solved_constraints(Solver, New)).
Calls:
Name: asserta/1 |
|
Name: is/2 |
|
Name: ! |
|
Name: =/2 |
|
Name: solved_constraints/2 |
dynamic predicate |
Name: retract/1 |
Called:
Name: benchmark_constraint/23 |
Module: smt_solver_benchmarks |
inductive_inv_timeout(120000).
Called:
Name: run_cbc_benchmark/4 |
Module: smt_solver_benchmarks |
Name: run_cbc_benchmarks4/0 |
Module: smt_solver_benchmarks |
Name: run_cbc_benchmarks1/0 |
Module: smt_solver_benchmarks |
Name: run_cbc_benchmarks3/0 |
Module: smt_solver_benchmarks |
Name: run_cbc_benchmarks2/0 |
Module: smt_solver_benchmarks |
Name: run_cbc_benchmarks5/0 |
Module: smt_solver_benchmarks |
Name: run_cbc_benchmarks6/0 |
Module: smt_solver_benchmarks |
int_range(C, B, R) :-
C == B,
!,
R = [C].
int_range(C, B, [C|T]) :-
C1 is C + 1,
int_range(C1, B, T).
Calls:
Name: RECURSIVE_CALL/3 |
Module: smt_solver_benchmarks |
Name: is/2 |
|
Name: =/2 |
|
Name: ! |
|
Name: ==/2 |
Called:
| Module: smt_solver_benchmarks |
is_eventb_machine(MachineFile) :-
atom_concat(_, '.eventb', MachineFile).
Calls:
Name: atom_concat/3 |
Called:
Name: load_b_eventb_or_tla/1 |
Module: smt_solver_benchmarks |
is_tla_file(File) :-
atom_concat(_, '.tla', File).
Calls:
Name: atom_concat/3 |
Called:
Name: load_b_eventb_or_tla/1 |
Module: smt_solver_benchmarks |
join_atom_list([Atom], _, Out) :-
!,
Out = Atom.
join_atom_list([Atom|T], Sep, Out) :-
atom_codes(Atom, Codes),
atom_codes(Sep, SepCodes),
join_atom_list(T, SepCodes, Codes, NAcc),
atom_codes(Out, NAcc).
Calls:
Name: atom_codes/2 |
|
Name: join_atom_list/4 |
Module: smt_solver_benchmarks |
Name: =/2 |
|
Name: ! |
Called:
| Module: smt_solver_benchmarks | |
| Module: smt_solver_benchmarks | |
| Module: smt_solver_benchmarks |
join_atom_list([], _, Acc, Acc).
join_atom_list([Atom|T], SepCodes, Acc, Codes) :-
atom_codes(Atom, ACodes),
append([Acc,SepCodes,ACodes], NAcc),
join_atom_list(T, SepCodes, NAcc, Codes).
Calls:
Name: RECURSIVE_CALL/4 |
Module: smt_solver_benchmarks |
Name: append/2 |
Module: foo_error |
Name: atom_codes/2 |
Called:
| Module: smt_solver_benchmarks | |
| Module: smt_solver_benchmarks | |
| Module: smt_solver_benchmarks |
load_b_eventb_or_tla(MachineFilePath) :-
( is_eventb_machine(MachineFilePath)
-> b_load_eventb_project(MachineFilePath)
; is_tla_file(MachineFilePath)
-> call_tla2b_parser(MachineFilePath),
atom_concat(PrefixPath, '.tla', MachineFilePath),
atom_concat(PrefixPath, '.prob', BMachinePath),
b_load_machine_probfile(BMachinePath)
; b_load_machine_from_file(MachineFilePath)
),
b_machine_precompile.
Calls:
Name: b_machine_precompile |
Module: foo_error |
Name: b_load_machine_from_file/1 |
Module: foo_error |
Name: b_load_machine_probfile/1 |
Module: foo_error |
Name: atom_concat/3 |
|
Name: call_tla2b_parser/1 |
Module: foo_error |
Name: is_tla_file/1 |
Module: smt_solver_benchmarks |
Name: ->/3 |
|
Name: b_load_eventb_project/1 |
Module: foo_error |
Name: is_eventb_machine/1 |
Module: smt_solver_benchmarks |
Called:
Name: run_bmc_benchmarks/2 |
Module: smt_solver_benchmarks |
| Module: smt_solver_benchmarks | |
| Module: smt_solver_benchmarks | |
Name: amount_of_sat_vars/4 |
Module: smt_solver_benchmarks |
| Module: smt_solver_benchmarks | |
| Module: smt_solver_benchmarks | |
Name: run_cbc_benchmarks/2 |
Module: smt_solver_benchmarks |
load_constraint_from_file(FilePath, Constraint) :-
file_exists(FilePath),
!,
open(FilePath, read, Stream),
read_term(Stream, Constraint, []),
close(Stream).
load_constraint_from_file(FilePath, _) :-
format("File does not exist: ~w~n~n", [FilePath]),
fail.
Calls:
Name: fail |
|
Name: format/2 |
|
Name: close/1 |
|
Name: read_term/3 |
|
Name: open/3 |
|
Name: ! |
|
Name: file_exists/1 |
Module: foo_error |
Called:
Name: benchmark/2 |
Module: smt_solver_benchmarks |
mean_of_list([], M) :-
!,
M = 0.
mean_of_list(L, M) :-
length(L, Len),
sumlist(L, Sum),
M is Sum / Len.
Calls:
Name: is/2 |
|
Name: sumlist/2 |
Module: foo_error |
Name: length/2 |
|
Name: =/2 |
|
Name: ! |
Called:
| Module: smt_solver_benchmarks | |
| Module: smt_solver_benchmarks | |
Name: amount_of_sat_vars_bmc/0 |
Module: smt_solver_benchmarks |
| Module: smt_solver_benchmarks | |
| Module: smt_solver_benchmarks |
median_of_list(L, M) :-
length(L, Len),
sort(L, LS),
( LS = [E]
-> M = E
; Len21 is floor(Len / 2),
Len22 is ceiling(Len / 2),
( Len21 \== Len22
-> nth1(Len22, L, M)
; nth1(Len21, L, M1),
Len211 is Len21 + 1,
nth1(Len211, L, M2),
M is (M1+M2)/2
)
).
Calls:
Name: is/2 |
|
Name: nth1/3 |
Module: foo_error |
Name: \==/2 |
|
Name: ->/3 |
|
Name: =/2 |
|
Name: sort/2 |
|
Name: length/2 |
Called:
| Module: smt_solver_benchmarks | |
| Module: smt_solver_benchmarks | |
| Module: smt_solver_benchmarks | |
| Module: smt_solver_benchmarks | |
Name: amount_of_sat_vars_bmc/0 |
Module: smt_solver_benchmarks |
Description:
N-Queens, e.g., to evaluate performance improvement of quantifier instantiation for
n_queens_encoding(N, b(conjunct(b(conjunct(b(equal(b(identifier(n),integer,[nodeid(p4(-1,1,1,2))]),b(integer(N),integer,[nodeid(p4(-1,1,5,7))])),pred,[nodeid(p4(-1,1,1,7))]),b(member(b(identifier(queens),set(couple(integer,integer)),[nodeid(p4(-1,1,10,16))]),b(total_injection(b(interval(b(integer(1),integer,[nodeid(p4(-1,1,19,20))]),b(identifier(n),integer,[nodeid(p4(-1,1,22,23))])),set(integer),[nodeid(p4(-1,1,19,23))]),b(interval(b(integer(1),integer,[nodeid(p4(-1,1,28,29))]),b(identifier(n),integer,[nodeid(p4(-1,1,31,32))])),set(integer),[nodeid(p4(-1,1,28,32))])),set(set(couple(integer,integer))),[nodeid(p4(-1,1,19,32))])),pred,[nodeid(p4(-1,1,10,32))])),pred,[]),b(forall([b(identifier(q1),integer,[nodeid(p4(-1,1,37,39)),introduced_by(forall)])],b(member(b(identifier(q1),integer,[nodeid(p4(-1,1,42,44)),introduced_by(forall)]),b(interval(b(integer(1),integer,[nodeid(p4(-1,1,45,46))]),b(identifier(n),integer,[nodeid(p4(-1,1,48,49))])),set(integer),[nodeid(p4(-1,1,45,49))])),pred,[nodeid(p4(-1,1,42,49))]),b(forall([b(identifier(q2),integer,[nodeid(p4(-1,1,55,57)),introduced_by(forall)])],b(conjunct(b(member(b(identifier(q2),integer,[nodeid(p4(-1,1,61,63)),introduced_by(forall)]),b(interval(b(integer(2),integer,[nodeid(p4(-1,1,64,65))]),b(identifier(n),integer,[nodeid(p4(-1,1,67,68))])),set(integer),[nodeid(p4(-1,1,64,68))])),pred,[nodeid(p4(-1,1,61,68))]),b(greater(b(identifier(q2),integer,[nodeid(p4(-1,1,71,73)),introduced_by(forall)]),b(identifier(q1),integer,[nodeid(p4(-1,1,74,76)),introduced_by(forall)])),pred,[nodeid(p4(-1,1,71,76))])),pred,[nodeid(p4(-1,1,61,76)),nodeid(p4(-1,1,61,76))]),b(conjunct(b(not_equal(b(add(b(function(b(identifier(queens),set(couple(integer,integer)),[nodeid(p4(-1,1,80,86))]),b(identifier(q1),integer,[nodeid(p4(-1,1,87,89)),introduced_by(forall)])),integer,[contains_wd_condition,nodeid(p4(-1,1,80,90))]),b(minus(b(identifier(q2),integer,[nodeid(p4(-1,1,92,94)),introduced_by(forall)]),b(identifier(q1),integer,[nodeid(p4(-1,1,95,97)),introduced_by(forall)])),integer,[nodeid(p4(-1,1,92,97))])),integer,[contains_wd_condition,nodeid(p4(-1,1,80,97))]),b(function(b(identifier(queens),set(couple(integer,integer)),[nodeid(p4(-1,1,102,108))]),b(identifier(q2),integer,[nodeid(p4(-1,1,109,111)),introduced_by(forall)])),integer,[contains_wd_condition,nodeid(p4(-1,1,102,112))])),pred,[contains_wd_condition,nodeid(p4(-1,1,80,112))]),b(not_equal(b(add(b(function(b(identifier(queens),set(couple(integer,integer)),[nodeid(p4(-1,1,115,121))]),b(identifier(q1),integer,[nodeid(p4(-1,1,122,124)),introduced_by(forall)])),integer,[contains_wd_condition,nodeid(p4(-1,1,115,125))]),b(minus(b(identifier(q1),integer,[nodeid(p4(-1,1,127,129)),introduced_by(forall)]),b(identifier(q2),integer,[nodeid(p4(-1,1,130,132)),introduced_by(forall)])),integer,[nodeid(p4(-1,1,127,132))])),integer,[contains_wd_condition,nodeid(p4(-1,1,115,132))]),b(function(b(identifier(queens),set(couple(integer,integer)),[nodeid(p4(-1,1,137,143))]),b(identifier(q2),integer,[nodeid(p4(-1,1,144,146)),introduced_by(forall)])),integer,[contains_wd_condition,nodeid(p4(-1,1,137,147))])),pred,[contains_wd_condition,nodeid(p4(-1,1,115,147))])),pred,[contains_wd_condition,nodeid(p4(-1,1,80,147)),nodeid(p4(-1,1,80,147))])),pred,[removed_typing,used_ids([n,q1,queens]),contains_wd_condition,nodeid(p4(-1,1,53,148))])),pred,[removed_typing,used_ids([n,queens]),contains_wd_condition,nodeid(p4(-1,1,35,149))])),pred,[contains_wd_condition,removed_typing])) :- integer(N), N > 0.
Calls:
Name: >/2 |
|
Name: integer/1 |
Called:
Name: run_n_queens_benchmark/3 |
Module: smt_solver_benchmarks |
p(L) :-
writeq(L), nl,
L = [_AmountOfSatVars,(prob,N,TimeProB,_FResProB),(z3,N,TimeZ3,_FResZ3),(sym_smt,N,TimeCdclt,_FResCdclt)],
format("~w & ~w & ~w & ~w & ~n", [N,TimeProB,TimeZ3,TimeCdclt]).
Calls:
Name: format/2 |
|
Name: =/2 |
|
Name: nl |
|
Name: writeq/1 |
prepare_result(solution(_), Out) :-
!,
Out = solution.
prepare_result(no_solution_found(enumeration_warning(_,_,_,_,_)), Out) :-
!,
Out = no_solution_found(enumeration_warning).
prepare_result(Res, Res).
Calls:
Name: =/2 |
|
Name: ! |
Called:
Name: write_to_csv_stream/3 |
Module: smt_solver_benchmarks |
print_complete_benchmarks(LFastestSolver) :-
filter_fastest_solver(cdclt, LFastestSolver, CdcltSol, CdcltNoSol, _, CdcltTimeDiff),
filter_fastest_solver(prob, LFastestSolver, ProBSol, ProBNoSol, _, ProBTimeDiff),
filter_fastest_solver(same, LFastestSolver, SameSol, SameNoSol, SameTimeout, _),
format("~n~nResults for all benchmarks:~n~nFastest Solver:~nCDCL(T): ~d (solution), ~d (contradiction)~nProB: ~d (solution), ~d (contradiction)~nEqual runtime: ~d (solution), ~d (contradiction), ~d (timeout)~n", [CdcltSol,CdcltNoSol,ProBSol,ProBNoSol,SameSol,SameNoSol,SameTimeout]),
( CdcltTimeDiff > ProBTimeDiff
-> TotalDiff is CdcltTimeDiff - ProBTimeDiff,
format("~nIn total, CDCL(T) is ~d ms faster than ProB.~n", [TotalDiff])
; TotalDiff is ProBTimeDiff - CdcltTimeDiff,
format("~nIn total, ProB is ~d ms faster than CDCL(T).~n", [TotalDiff])
).
Calls:
Name: format/2 |
|
Name: is/2 |
|
Name: >/2 |
|
Name: ->/3 |
|
Name: filter_fastest_solver/6 |
Module: smt_solver_benchmarks |
Called:
Name: run_misc_benchmarks/0 |
Module: smt_solver_benchmarks |
print_enter_benchmark(Nr) :-
format("Run benchmark #~d~n---------------------------------------~n", [Nr]).
Calls:
Name: format/2 |
Called:
Name: benchmark/2 |
Module: smt_solver_benchmarks |
print_n_queens_data(Data) :-
maplist(p, Data).
Calls:
Name: maplist/2 |
Module: foo_error |
Called:
| Module: smt_solver_benchmarks |
print_times(ProBTime, CDCLTTime) :-
format("ProB: ~w~nCDCL(T) using ProB only: ~w~n", [ProBTime, CDCLTTime]).
Calls:
Name: format/2 |
Called:
| Module: smt_solver_benchmarks |
reset_misc_benchmarks :-
retractall(fastest_solver(_, _, _)),!.
Calls:
Name: ! |
|
Name: retractall/1 |
Called:
Name: run_misc_benchmarks/0 |
Module: smt_solver_benchmarks |
run_additional_bmc_benchmark(UseIdlSolver, ExamplesPath) :-
atom_concat('../cbc_benchmarks/bounded_model_checking/', ExamplesPath, FullExamplesPath),
atom_concat('../prob_examples/', ExamplesPath, MachinePath),
load_b_eventb_or_tla(MachinePath),
get_filename_from_path(MachinePath, FileName),
atom_concat('../cbc_benchmarks/results/bounded_model_checking/', FileName, TempPath),
atom_concat(TempPath, '_results.csv', ResultPath),
\+ file_exists(ResultPath),
!, % don't run benchmark if result already exists
( atom_concat(Prefix, '.eventb', FullExamplesPath)
; atom_concat(Prefix, '.mch', FullExamplesPath)
; atom_concat(Prefix, '.tla', FullExamplesPath)
),
atom_concat(Prefix, '_monolithic_bmc_k_1.eval', Path1),
atom_concat(Prefix, '_monolithic_bmc_k_5.eval', Path2),
atom_concat(Prefix, '_monolithic_bmc_k_10.eval', Path3),
retractall(cdclt_sat_solver:incremental_mode),
benchmark_constraints(UseIdlSolver, [Path1,Path2,Path3], [], Data),
retractall(cdclt_sat_solver:memoize_backjump_clause(_, _, _)),
eval_benchmark_data_csv('../cbc_benchmarks/results/bounded_model_checking/', FileName, 'Additional BMC benchmarks', Data).
run_additional_bmc_benchmark(_, _).
Calls:
| Module: smt_solver_benchmarks | |
Name: retractall/1 |
|
Name: benchmark_constraints/4 |
Module: smt_solver_benchmarks |
Name: atom_concat/3 |
|
Name: ! |
|
Name: file_exists/1 |
Module: foo_error |
Name: not/1 |
|
Name: get_filename_from_path/2 |
Module: smt_solver_benchmarks |
Name: load_b_eventb_or_tla/1 |
Module: smt_solver_benchmarks |
Called:
| Module: smt_solver_benchmarks |
run_additional_bmc_benchmarks(UseIdlSolver) :-
findall(ExamplesPath, additional_benchmark_model(_, ExamplesPath), ExamplesPaths),
run_additional_bmc_benchmarks(UseIdlSolver, ExamplesPaths).
Calls:
| Module: smt_solver_benchmarks | |
Name: findall/3 |
Called:
| Module: smt_solver_benchmarks | |
Name: run_benchmark/3 |
Module: prob_cli |
run_additional_bmc_benchmarks(_, []).
run_additional_bmc_benchmarks(UseIdlSolver, [ExamplesPath|T]) :-
run_additional_bmc_benchmark(UseIdlSolver, ExamplesPath),
run_additional_bmc_benchmarks(UseIdlSolver, T).
Calls:
Name: RECURSIVE_CALL/2 |
Module: smt_solver_benchmarks |
| Module: smt_solver_benchmarks |
Called:
| Module: smt_solver_benchmarks | |
Name: run_benchmark/3 |
Module: prob_cli |
run_additional_deadlock_benchmark(UseIdlSolver, ExamplesPath) :-
atom_concat('../cbc_benchmarks/deadlock_checking/', ExamplesPath, FullExamplesPath),
atom_concat('../prob_examples/', ExamplesPath, MachinePath),
load_b_eventb_or_tla(MachinePath),
get_filename_from_path(MachinePath, FileName),
atom_concat('../cbc_benchmarks/results/deadlock_checking/', FileName, TempPath),
atom_concat(TempPath, '_results.csv', ResultPath),
\+ file_exists(ResultPath),
!, % don't run benchmark if result already exists
( atom_concat(Prefix, '.eventb', FullExamplesPath)
; atom_concat(Prefix, '.mch', FullExamplesPath)
; atom_concat(Prefix, '.tla', FullExamplesPath)
),
atom_concat(Prefix, '_deadlock_freedom.eval', Path1),
retractall(cdclt_sat_solver:incremental_mode),
benchmark_constraints(UseIdlSolver, [Path1], [], Data),
retractall(cdclt_sat_solver:memoize_backjump_clause(_, _, _)),
eval_benchmark_data_csv('../cbc_benchmarks/results/deadlock_checking/', FileName, 'Additional BMC benchmarks', Data).
run_additional_deadlock_benchmark(_, _).
Calls:
| Module: smt_solver_benchmarks | |
Name: retractall/1 |
|
Name: benchmark_constraints/4 |
Module: smt_solver_benchmarks |
Name: atom_concat/3 |
|
Name: ! |
|
Name: file_exists/1 |
Module: foo_error |
Name: not/1 |
|
Name: get_filename_from_path/2 |
Module: smt_solver_benchmarks |
Name: load_b_eventb_or_tla/1 |
Module: smt_solver_benchmarks |
Called:
| Module: smt_solver_benchmarks |
run_additional_deadlock_benchmarks(UseIdlSolver) :-
findall(ExamplesPath, additional_deadlock_benchmark_model(_, ExamplesPath), ExamplesPaths),
run_additional_deadlock_benchmarks(UseIdlSolver, ExamplesPaths).
Calls:
| Module: smt_solver_benchmarks | |
Name: findall/3 |
Called:
Name: run_benchmark/3 |
Module: prob_cli |
| Module: smt_solver_benchmarks |
run_additional_deadlock_benchmarks(_, []).
run_additional_deadlock_benchmarks(UseIdlSolver, [ExamplesPath|T]) :-
run_additional_deadlock_benchmark(UseIdlSolver, ExamplesPath),
run_additional_deadlock_benchmarks(UseIdlSolver, T).
Calls:
Name: RECURSIVE_CALL/2 |
Module: smt_solver_benchmarks |
| Module: smt_solver_benchmarks |
Called:
Name: run_benchmark/3 |
Module: prob_cli |
| Module: smt_solver_benchmarks |
run_additional_inductive_inv_benchmark(UseIdlSolver, ExamplesPath) :-
atom_concat('../cbc_benchmarks/inductive_invariant_checking/', ExamplesPath, FullExamplesPath),
atom_concat('../prob_examples/', ExamplesPath, MachinePath),
load_b_eventb_or_tla(MachinePath),
get_filename_from_path(MachinePath, FileName),
atom_concat('../cbc_benchmarks/results/inductive_invariant_checking/', FileName, TempPath),
atom_concat(TempPath, '_results.csv', ResultPath),
\+ file_exists(ResultPath),
!, % don't run benchmark if result already exists
( atom_concat(Prefix, '.eventb', FullExamplesPath)
; atom_concat(Prefix, '.mch', FullExamplesPath)
; atom_concat(Prefix, '.tla', FullExamplesPath)
),
findall(BenchPath, (b_is_operation_name(OpName),
atom_concat(Prefix, '_inductive_inv_', Path1),
atom_concat(Path1, OpName, Path2),
atom_concat(Path2, '.eval', BenchPath)),
BenchPaths),
retractall(cdclt_sat_solver:incremental_mode),
benchmark_constraints(UseIdlSolver, BenchPaths, [], Data),
retractall(cdclt_sat_solver:memoize_backjump_clause(_, _, _)),
eval_benchmark_data_csv('../cbc_benchmarks/results/inductive_invariant_checking/', FileName, 'Additional CBC benchmarks', Data).
run_additional_inductive_inv_benchmark(_, _).
Calls:
| Module: smt_solver_benchmarks | |
Name: retractall/1 |
|
Name: benchmark_constraints/4 |
Module: smt_solver_benchmarks |
Name: findall/3 |
|
Name: atom_concat/3 |
|
Name: ! |
|
Name: file_exists/1 |
Module: foo_error |
Name: not/1 |
|
Name: get_filename_from_path/2 |
Module: smt_solver_benchmarks |
Name: load_b_eventb_or_tla/1 |
Module: smt_solver_benchmarks |
Called:
| Module: smt_solver_benchmarks |
run_additional_inductive_inv_benchmarks(UseIdlSolver) :-
findall(ExamplesPath, additional_benchmark_model(_, ExamplesPath), ExamplesPaths),
run_additional_inductive_inv_benchmarks(UseIdlSolver, ExamplesPaths).
Calls:
| Module: smt_solver_benchmarks | |
Name: findall/3 |
Called:
Name: run_benchmark/3 |
Module: prob_cli |
| Module: smt_solver_benchmarks |
run_additional_inductive_inv_benchmarks(_, []).
run_additional_inductive_inv_benchmarks(UseIdlSolver, [ExamplesPath|T]) :-
run_additional_inductive_inv_benchmark(UseIdlSolver, ExamplesPath),
run_additional_inductive_inv_benchmarks(UseIdlSolver, T).
Calls:
Name: RECURSIVE_CALL/2 |
Module: smt_solver_benchmarks |
| Module: smt_solver_benchmarks |
Called:
Name: run_benchmark/3 |
Module: prob_cli |
| Module: smt_solver_benchmarks |
run_bmc_benchmarks(UseIdlSolver, DirPath) :-
retractall(solved_constraints(_,_)),
retractall(benchmark_result(_,_,_)),
atom_concat(DirPath, 'benchmark_config.pl', ConfigPath),
get_file_paths_from_config(ConfigPath, MachineFile, ConstraintPaths, Description, MachineName),
format("Run benchmarks ~w~n", [Description]),
atom_concat(DirPath, MachineFile, MachinePath),
load_b_eventb_or_tla(MachinePath),
maplist(atom_concat(DirPath), ConstraintPaths, FullConstraintPaths),
retractall(cdclt_sat_solver:incremental_mode),
benchmark_constraints(UseIdlSolver, FullConstraintPaths, [], Data),
retractall(cdclt_sat_solver:memoize_backjump_clause(_, _, _)),
%eval_benchmark_data(MachineName, Description, Data),
eval_benchmark_data_csv('benchmark_results_smt/', MachineName, Description, Data).
Calls:
| Module: smt_solver_benchmarks | |
Name: retractall/1 |
|
Name: benchmark_constraints/4 |
Module: smt_solver_benchmarks |
Name: maplist/3 |
Module: foo_error |
Name: load_b_eventb_or_tla/1 |
Module: smt_solver_benchmarks |
Name: atom_concat/3 |
|
Name: format/2 |
|
| Module: smt_solver_benchmarks |
Called:
Name: run_bmc_benchmarks5/0 |
Module: smt_solver_benchmarks |
Name: run_bmc_benchmarks3/0 |
Module: smt_solver_benchmarks |
Name: run_bmc_benchmarks1/0 |
Module: smt_solver_benchmarks |
Name: run_bmc_benchmarks33/0 |
Module: smt_solver_benchmarks |
Name: run_bmc_benchmarks22/0 |
Module: smt_solver_benchmarks |
Name: run_bmc_benchmarks6/0 |
Module: smt_solver_benchmarks |
Name: run_bmc_benchmarks11/0 |
Module: smt_solver_benchmarks |
Name: run_bmc_benchmarks4/0 |
Module: smt_solver_benchmarks |
Name: run_bmc_benchmarks2/0 |
Module: smt_solver_benchmarks |
run_bmc_benchmarks1 :-
bmc_timeout(Timeout),
preferences:set_preference(time_out, Timeout),
%run_bmc_benchmarks(false, '/home/joshua/raw_benchmarks/benchmarks_bmc/paxos-5/'),
%run_bmc_benchmarks(false, '/home/joshua/raw_benchmarks/benchmarks_bmc/abz16_m0/'),
/*run_bmc_benchmarks(false, '/home/joshua/raw_benchmarks/benchmarks_bmc/abz16_m1/'),
run_bmc_benchmarks(false, '/home/joshua/raw_benchmarks/benchmarks_bmc/abz16_m2/'),
run_bmc_benchmarks(false, '/home/joshua/raw_benchmarks/benchmarks_bmc/abz16_m3/'),*/
run_bmc_benchmarks(false, '/home/joshua/raw_benchmarks/benchmarks_bmc/abz16_m6/'),
run_bmc_benchmarks(false, '/home/joshua/raw_benchmarks/benchmarks_bmc/abz16_m7/').
Calls:
Name: run_bmc_benchmarks/2 |
Module: smt_solver_benchmarks |
Name: set_preference/2 |
Module: preferences |
Name: bmc_timeout/1 |
Module: smt_solver_benchmarks |
run_bmc_benchmarks11 :-
bmc_timeout(Timeout),
preferences:set_preference(time_out, Timeout),
run_bmc_benchmarks(false, '/home/joshua/raw_benchmarks/benchmarks_bmc/abz16_m4/'),
run_bmc_benchmarks(false, '/home/joshua/raw_benchmarks/benchmarks_bmc/abz16_m5/').
Calls:
Name: run_bmc_benchmarks/2 |
Module: smt_solver_benchmarks |
Name: set_preference/2 |
Module: preferences |
Name: bmc_timeout/1 |
Module: smt_solver_benchmarks |
run_bmc_benchmarks2 :-
bmc_timeout(Timeout),
preferences:set_preference(time_out, Timeout),
run_bmc_benchmarks(false, '/home/joshua/raw_benchmarks/benchmarks_bmc/r4_handle/'),
run_bmc_benchmarks(false, '/home/joshua/raw_benchmarks/benchmarks_bmc/r5_switch/'),
run_bmc_benchmarks(false, '/home/joshua/raw_benchmarks/benchmarks_bmc/r6_lights/').
Calls:
Name: run_bmc_benchmarks/2 |
Module: smt_solver_benchmarks |
Name: set_preference/2 |
Module: preferences |
Name: bmc_timeout/1 |
Module: smt_solver_benchmarks |
run_bmc_benchmarks22 :-
bmc_timeout(Timeout),
preferences:set_preference(time_out, Timeout),
run_bmc_benchmarks(false, '/home/joshua/raw_benchmarks/benchmarks_bmc/r0_geardoor/'),
run_bmc_benchmarks(false, '/home/joshua/raw_benchmarks/benchmarks_bmc/r1_valve/'),
run_bmc_benchmarks(false, '/home/joshua/raw_benchmarks/benchmarks_bmc/r2_outputs/'),
run_bmc_benchmarks(false, '/home/joshua/raw_benchmarks/benchmarks_bmc/r3_sensors/').
Calls:
Name: run_bmc_benchmarks/2 |
Module: smt_solver_benchmarks |
Name: set_preference/2 |
Module: preferences |
Name: bmc_timeout/1 |
Module: smt_solver_benchmarks |
run_bmc_benchmarks3 :-
bmc_timeout(Timeout),
preferences:set_preference(time_out, Timeout),
run_bmc_benchmarks(false, '/home/joshua/raw_benchmarks/benchmarks_bmc/pm_m0_aai/'),
run_bmc_benchmarks(false, '/home/joshua/raw_benchmarks/benchmarks_bmc/pm_m0_aat/').
Calls:
Name: run_bmc_benchmarks/2 |
Module: smt_solver_benchmarks |
Name: set_preference/2 |
Module: preferences |
Name: bmc_timeout/1 |
Module: smt_solver_benchmarks |
run_bmc_benchmarks33 :-
bmc_timeout(Timeout),
preferences:set_preference(time_out, Timeout),
run_bmc_benchmarks(false, '/home/joshua/raw_benchmarks/benchmarks_bmc/pm_m0_aoo/'),
run_bmc_benchmarks(false, '/home/joshua/raw_benchmarks/benchmarks_bmc/pm_m0_voo/'),
run_bmc_benchmarks(false, '/home/joshua/raw_benchmarks/benchmarks_bmc/pm_m0_vvi/').
Calls:
Name: run_bmc_benchmarks/2 |
Module: smt_solver_benchmarks |
Name: set_preference/2 |
Module: preferences |
Name: bmc_timeout/1 |
Module: smt_solver_benchmarks |
run_bmc_benchmarks4 :-
bmc_timeout(Timeout),
preferences:set_preference(time_out, Timeout),
run_bmc_benchmarks(false, '/home/joshua/raw_benchmarks/benchmarks_bmc/pm_m0_vvt/'),
run_bmc_benchmarks(false, '/home/joshua/raw_benchmarks/benchmarks_bmc/pm_m1_aoor/'),
run_bmc_benchmarks(false, '/home/joshua/raw_benchmarks/benchmarks_bmc/pm_m1_voor/'),
run_bmc_benchmarks(false, '/home/joshua/raw_benchmarks/benchmarks_bmc/pm_m2_aai/').
Calls:
Name: run_bmc_benchmarks/2 |
Module: smt_solver_benchmarks |
Name: set_preference/2 |
Module: preferences |
Name: bmc_timeout/1 |
Module: smt_solver_benchmarks |
run_bmc_benchmarks5 :-
bmc_timeout(Timeout),
preferences:set_preference(time_out, Timeout),
run_bmc_benchmarks(false, '/home/joshua/raw_benchmarks/benchmarks_bmc/simple-two-phase/'),
run_bmc_benchmarks(false, '/home/joshua/raw_benchmarks/benchmarks_bmc/lightbot/'),
run_bmc_benchmarks(false, '/home/joshua/raw_benchmarks/benchmarks_bmc/travel_agency/'),
run_bmc_benchmarks(false, '/home/joshua/raw_benchmarks/benchmarks_bmc/search_events/').
Calls:
Name: run_bmc_benchmarks/2 |
Module: smt_solver_benchmarks |
Name: set_preference/2 |
Module: preferences |
Name: bmc_timeout/1 |
Module: smt_solver_benchmarks |
run_bmc_benchmarks6 :-
bmc_timeout(Timeout),
preferences:set_preference(time_out, Timeout),
run_bmc_benchmarks(false, '/home/joshua/raw_benchmarks/benchmarks_bmc/large_branching/'),
run_bmc_benchmarks(false, '/home/joshua/raw_benchmarks/benchmarks_bmc/prisoners-4/'),
run_bmc_benchmarks(false, '/home/joshua/raw_benchmarks/benchmarks_bmc/bakery/'),
run_bmc_benchmarks(false, '/home/joshua/raw_benchmarks/benchmarks_bmc/paxos-3/').
Calls:
Name: run_bmc_benchmarks/2 |
Module: smt_solver_benchmarks |
Name: set_preference/2 |
Module: preferences |
Name: bmc_timeout/1 |
Module: smt_solver_benchmarks |
run_cbc_benchmark(UseIdlSolver, FolderPath, FileName-BenchmarkFilePath, Constraint) :-
inductive_inv_timeout(Timeout),
preferences:set_preference(time_out, Timeout),
set_preference(cdclt_use_idl_theory_solver, false),
set_preference(cdclt_perform_static_analysis, false),
set_preference(cdclt_perform_symmetry_breaking, true),
cdclt_solver:init,
write('Solve with Sym-Raw-SMT..'),nl,
writeq(BenchmarkFilePath),nl,
statistics(walltime, [StartCdcltRawSym|_]),
cdclt_solve_predicate(Constraint, _, ResCdcltRawSym),
statistics(walltime, [StopCdcltRawSym|_]),
(cdclt_sat_solver:restarts(RestartsCdcltRawSym); RestartsCdcltRawSym = 0),
TimeCdcltRawSym is StopCdcltRawSym - StartCdcltRawSym,
nl,nl,write(ResCdcltRawSym),nl,nl,
write('done.'), nl,
set_preference(cdclt_perform_static_analysis, true),
cdclt_solver:init,
write('Solve with Sym-SMT..'),nl,
writeq(BenchmarkFilePath),nl,
statistics(walltime, [StartCdclt|_]),
cdclt_solve_predicate(Constraint, _, ResCdclt),
statistics(walltime, [StopCdclt|_]),
(cdclt_sat_solver:restarts(RestartsCdclt); RestartsCdclt = 0),
TimeCdclt is StopCdclt - StartCdclt,
nl,nl,write(ResCdclt),nl,nl,
write('done.'), nl,
preferences:set_preference(time_out, Timeout),
( UseIdlSolver
-> set_preference(cdclt_perform_symmetry_breaking,false),
set_preference(cdclt_use_idl_theory_solver,true),
cdclt_solver:init,
write('Solve with IDL-SMT..'),nl,
writeq(BenchmarkFilePath),nl,
statistics(walltime, [StartCdcltIdl|_]),
cdclt_solve_predicate(Constraint, _, ResCdcltIdl),
statistics(walltime, [StopCdcltIdl|_]),
(cdclt_sat_solver:restarts(RestartsCdcltIdl); RestartsCdcltIdl = 0),
TimeCdcltIdl is StopCdcltIdl - StartCdcltIdl,
set_preference(cdclt_use_idl_theory_solver,false),
set_preference(cdclt_perform_symmetry_breaking,true)
; TimeCdcltIdl = 0,
RestartsCdcltIdl = 0,
ResCdcltIdl = none
),
nl,nl,write(ResCdcltIdl),nl,nl,
write('done.'), nl,
preferences:set_preference(time_out, Timeout),
set_preference(cdclt_perform_symmetry_breaking,false),
cdclt_solver:init,
write('Solve with SMT..'),nl,
writeq(BenchmarkFilePath),nl,
statistics(walltime, [StartCdcltNoSym|_]),
cdclt_solve_predicate(Constraint, _, ResCdcltNoSym),
statistics(walltime, [StopCdcltNoSym|_]),
(cdclt_sat_solver:restarts(RestartsCdcltNoSym); RestartsCdcltNoSym = 0),
TimeCdcltNoSym is StopCdcltNoSym - StartCdcltNoSym,
nl,nl,write(ResCdcltNoSym),nl,nl,
write('done.'), nl,
preferences:set_preference(time_out, Timeout),
set_preference(cdclt_perform_static_analysis,false),
set_preference(cdclt_perform_symmetry_breaking,false),
cdclt_solver:init,
write('Solve with Raw-SMT..'),nl,
writeq(BenchmarkFilePath),nl,
statistics(walltime, [StartCdcltRaw|_]),
cdclt_solve_predicate(Constraint, _, ResCdcltRaw),
statistics(walltime, [StopCdcltRaw|_]),
(cdclt_sat_solver:restarts(RestartsCdcltRaw); RestartsCdcltRaw = 0),
TimeCdcltRaw is StopCdcltRaw - StartCdcltRaw,
nl,nl,write(ResCdcltRaw),nl,nl,
write('done.'), nl,
preferences:set_preference(time_out, Timeout),
write('Solve with Z3..'),nl,
writeq(BenchmarkFilePath),nl,
%translate:print_bexpr(Constraint),nl,
statistics(walltime, [StartZ3|_]),
smt_solve_predicate(z3,Constraint, _, ResZ3),
%ResZ3 = no_solution_found(solver_answered_unknown),
statistics(walltime, [StopZ3|_]),
TimeZ3 is StopZ3 - StartZ3,
nl,nl,write(ResZ3),nl,nl,
preferences:set_preference(time_out, Timeout),
write('Solve with ProB..'),nl,
writeq(BenchmarkFilePath),nl,
statistics(walltime, [StartProB|_]),
solve_predicate(Constraint, _, 1, [use_smt_mode/true,use_clpfd_solver/true,clean_up_pred,allow_improving_wd_mode/true], ResProB),
%ResProB = no_solution_found(solver_answered_unknown),
statistics(walltime, [StopProB|_]),
TimeProB is StopProB - StartProB,
nl,nl,write(ResProB),nl,nl,
write('done.'), nl,
!,
eval_cbc_benchmark_data(FolderPath, FileName-BenchmarkFilePath, ResCdcltRawSym, TimeCdcltRawSym, RestartsCdcltRawSym, ResCdclt, TimeCdclt, RestartsCdclt, ResCdcltNoSym, TimeCdcltNoSym, RestartsCdcltNoSym, ResCdcltIdl, TimeCdcltIdl, RestartsCdcltIdl, ResCdcltRaw, TimeCdcltRaw, RestartsCdcltRaw, ResZ3, TimeZ3, ResProB, TimeProB).
Calls:
| Module: smt_solver_benchmarks | |
Name: ! |
|
Name: nl |
|
Name: write/1 |
|
Name: is/2 |
|
Name: statistics/2 |
|
Name: solve_predicate/5 |
Module: foo_error |
Name: writeq/1 |
|
Name: set_preference/2 |
Module: preferences |
Name: smt_solve_predicate/4 |
Module: foo_error |
Name: =/2 |
|
Name: restarts/1 |
Module: cdclt_sat_solver |
Name: cdclt_solve_predicate/3 |
Module: foo_error |
Name: init/0 |
Module: cdclt_solver |
Name: set_preference/2 |
Module: foo_error |
Name: call/1 |
|
Name: ->/3 |
|
Name: inductive_inv_timeout/1 |
Module: smt_solver_benchmarks |
Called:
Name: run_cbc_benchmarks/3 |
Module: smt_solver_benchmarks |
run_cbc_benchmarks(UseIdlSolver, FolderPath) :-
directory_exists(FolderPath),
file_members_of_directory(FolderPath, FilePaths),
select_machine_file_path(FilePaths, MachineFilePath, TBenchmarkFilePaths),
findall(FileName-FilePath, (member(FileName-FilePath, TBenchmarkFilePaths), atom_concat(_, '.eval', FilePath)), BenchmarkFilePaths),
load_b_eventb_or_tla(MachineFilePath),
run_cbc_benchmarks(UseIdlSolver, FolderPath, BenchmarkFilePaths).
Calls:
Name: run_cbc_benchmarks/3 |
Module: smt_solver_benchmarks |
Name: load_b_eventb_or_tla/1 |
Module: smt_solver_benchmarks |
Name: findall/3 |
|
| Module: smt_solver_benchmarks | |
Name: file_members_of_directory/2 |
Module: foo_error |
Name: directory_exists/1 |
Module: foo_error |
Called:
Name: run_cbc_benchmarks/2 |
Module: smt_solver_benchmarks |
run_cbc_benchmarks(_, _, []).
run_cbc_benchmarks(UseIdlSolver, FolderPath, [FileName-BenchmarkFilePath|T]) :-
safe_read_string_from_file(BenchmarkFilePath, utf8, Codes),
parse_formula(Codes, UntypedAst),
type_check_in_machine_context([UntypedAst], [Constraint]),
retractall(cdclt_sat_solver:incremental_mode),
run_cbc_benchmark(UseIdlSolver, FolderPath, FileName-BenchmarkFilePath, Constraint),
run_cbc_benchmarks(UseIdlSolver, FolderPath, T).
Calls:
Name: RECURSIVE_CALL/3 |
Module: smt_solver_benchmarks |
Name: run_cbc_benchmark/4 |
Module: smt_solver_benchmarks |
Name: retractall/1 |
|
Name: type_check_in_machine_context/2 |
Module: foo_error |
Name: parse_formula/2 |
Module: foo_error |
Name: safe_read_string_from_file/3 |
Module: foo_error |
Called:
Name: run_cbc_benchmarks/2 |
Module: smt_solver_benchmarks |
run_cbc_benchmarks1 :-
inductive_inv_timeout(Timeout),
preferences:set_preference(time_out, Timeout),
/*run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/abz16_m0/'),
run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/abz16_m1/'),
run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/abz16_m2/'),
run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/abz16_m3/'),*/
run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/abz16_m4/'),
run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/abz16_m5/'),
run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/abz16_m6/'),
run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/abz16_m7/').
Calls:
Name: run_cbc_benchmarks/2 |
Module: smt_solver_benchmarks |
Name: set_preference/2 |
Module: preferences |
Name: inductive_inv_timeout/1 |
Module: smt_solver_benchmarks |
run_cbc_benchmarks2 :-
inductive_inv_timeout(Timeout),
preferences:set_preference(time_out, Timeout),
run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/r0_geardoor/'),
run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/r1_valve/'),
run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/r2_outputs/'),
run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/r3_sensors/'),
run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/r4_handle/'),
run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/r5_switch/'),
run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/r6_lights/').
Calls:
Name: run_cbc_benchmarks/2 |
Module: smt_solver_benchmarks |
Name: set_preference/2 |
Module: preferences |
Name: inductive_inv_timeout/1 |
Module: smt_solver_benchmarks |
run_cbc_benchmarks3 :-
inductive_inv_timeout(Timeout),
preferences:set_preference(time_out, Timeout),
run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/pm_m0_aai/'),
run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/pm_m0_aat/'),
run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/pm_m0_aoo/'),
run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/pm_m0_voo/').
Calls:
Name: run_cbc_benchmarks/2 |
Module: smt_solver_benchmarks |
Name: set_preference/2 |
Module: preferences |
Name: inductive_inv_timeout/1 |
Module: smt_solver_benchmarks |
run_cbc_benchmarks4 :-
inductive_inv_timeout(Timeout),
preferences:set_preference(time_out, Timeout),
run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/pm_m0_vvi/'),
run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/pm_m0_vvt/'),
run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/pm_m1_aoor/'),
run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/pm_m1_voor/'),
run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/pm_m2_aai/').
Calls:
Name: run_cbc_benchmarks/2 |
Module: smt_solver_benchmarks |
Name: set_preference/2 |
Module: preferences |
Name: inductive_inv_timeout/1 |
Module: smt_solver_benchmarks |
run_cbc_benchmarks5 :-
inductive_inv_timeout(Timeout),
preferences:set_preference(time_out, Timeout),
%run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/simple-two-phase/'), % static contradiction
run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/prisoners-4/'),
run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/bakery/'),
run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/paxos-3/').
Calls:
Name: run_cbc_benchmarks/2 |
Module: smt_solver_benchmarks |
Name: set_preference/2 |
Module: preferences |
Name: inductive_inv_timeout/1 |
Module: smt_solver_benchmarks |
run_cbc_benchmarks6 :-
inductive_inv_timeout(Timeout),
preferences:set_preference(time_out, Timeout),
run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/lightbot/'),
run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/travel_agency/'),
run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/search_events/'),
run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/large_branching/').
Calls:
Name: run_cbc_benchmarks/2 |
Module: smt_solver_benchmarks |
Name: set_preference/2 |
Module: preferences |
Name: inductive_inv_timeout/1 |
Module: smt_solver_benchmarks |
run_deadlock_benchmarks1 :-
deadlock_timeout(Timeout),
preferences:set_preference(time_out, Timeout),
/*run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/abz16_m0/'),
run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/abz16_m1/'),
run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/abz16_m2/'),
run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/abz16_m3/'),*/
run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/abz16_m4/'),
run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/abz16_m5/'),
run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/abz16_m6/'),
run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/abz16_m7/').
Calls:
Name: run_cbc_benchmarks/2 |
Module: smt_solver_benchmarks |
Name: set_preference/2 |
Module: preferences |
Name: deadlock_timeout/1 |
Module: smt_solver_benchmarks |
run_deadlock_benchmarks2 :-
deadlock_timeout(Timeout),
preferences:set_preference(time_out, Timeout),
run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/r0_geardoor/'),
run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/r1_valve/'),
run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/r2_outputs/'),
run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/r3_sensors/'),
run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/r4_handle/'),
run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/r5_switch/').
Calls:
Name: run_cbc_benchmarks/2 |
Module: smt_solver_benchmarks |
Name: set_preference/2 |
Module: preferences |
Name: deadlock_timeout/1 |
Module: smt_solver_benchmarks |
run_deadlock_benchmarks3 :-
deadlock_timeout(Timeout),
preferences:set_preference(time_out, Timeout),
run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/pm_m0_aai/'),
run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/pm_m0_aat/'),
run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/pm_m0_aoo/'),
run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/pm_m0_voo/').
Calls:
Name: run_cbc_benchmarks/2 |
Module: smt_solver_benchmarks |
Name: set_preference/2 |
Module: preferences |
Name: deadlock_timeout/1 |
Module: smt_solver_benchmarks |
run_deadlock_benchmarks4 :-
deadlock_timeout(Timeout),
preferences:set_preference(time_out, Timeout),
run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/pm_m0_vvi/'),
run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/pm_m0_vvt/'),
run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/pm_m1_aoor/'),
run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/pm_m1_voor/'),
run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/pm_m2_aai/').
Calls:
Name: run_cbc_benchmarks/2 |
Module: smt_solver_benchmarks |
Name: set_preference/2 |
Module: preferences |
Name: deadlock_timeout/1 |
Module: smt_solver_benchmarks |
run_deadlock_benchmarks5 :-
deadlock_timeout(Timeout),
preferences:set_preference(time_out, Timeout),
run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/simple-two-phase/'),
run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/prisoners-4/'),
run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/bakery/'),
run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/paxos-3/').
Calls:
Name: run_cbc_benchmarks/2 |
Module: smt_solver_benchmarks |
Name: set_preference/2 |
Module: preferences |
Name: deadlock_timeout/1 |
Module: smt_solver_benchmarks |
run_deadlock_benchmarks6 :-
deadlock_timeout(Timeout),
preferences:set_preference(time_out, Timeout),
run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/lightbot/'),
run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/travel_agency/'),
run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/search_events/'),
run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/large_branching/').
Calls:
Name: run_cbc_benchmarks/2 |
Module: smt_solver_benchmarks |
Name: set_preference/2 |
Module: preferences |
Name: deadlock_timeout/1 |
Module: smt_solver_benchmarks |
Description:
Mixed constraints, e.g., taken from program synthesis or Alloy2B
run_misc_benchmarks :-
setup_scheduler,
reset_misc_benchmarks,
benchmark(_, _),
fail.
run_misc_benchmarks :-
preferences:temporary_set_preference(normalize_ast, true),
findall(FastestSolver-SolutionOrNot-TimeDiff, fastest_solver(FastestSolver, SolutionOrNot, TimeDiff), LFastestSolver),
length(LFastestSolver, Results),
format("~n~n#Results: ~w~n~n", [Results]),
print_complete_benchmarks(LFastestSolver),
preferences:reset_temporary_preference(normalize_ast).
Calls:
| Module: preferences | |
| Module: smt_solver_benchmarks | |
Name: format/2 |
|
Name: length/2 |
|
Name: findall/3 |
|
| Module: preferences | |
Name: fail |
|
Name: benchmark/2 |
Module: smt_solver_benchmarks |
Name: reset_misc_benchmarks/0 |
Module: smt_solver_benchmarks |
Name: setup_scheduler/0 |
Module: smt_solver_benchmarks |
run_n_queens_benchmark(N, DataAcc, NewDataAcc) :-
n_queens_encoding(N, Constraint),
ast_optimizer_for_smt:precompute_values(Constraint, [instantiate_quantifier_limit(10000)], IConstraint),
cdclt_solver:get_amount_of_sat_variables(IConstraint, AmountOfSatVars),
format("Amount of SAT variables: ~w", [AmountOfSatVars]),nl,
format("Solve with ProB for N=~w~n", [N]),
statistics(walltime, [StartProB|_]),
solve_predicate(IConstraint, _, 1, [use_smt_mode/true,use_clpfd_solver/true,clean_up_pred,allow_improving_wd_mode/true], ResProB),
statistics(walltime, [StopProB|_]),
ResProB \= contradiction_found,
TimeProB is StopProB - StartProB,
format("Solve with Z3~n for N=~w", [N]),
statistics(walltime, [StartZ3|_]),
smt_solve_predicate(z3, Constraint, _, ResZ3),
statistics(walltime, [StopZ3|_]),
ResZ3 \= contradiction_found,
TimeZ3 is StopZ3 - StartZ3,
format("Solve with Sym-SMT~n for N=~w", [N]),
set_preference(cdclt_perform_static_analysis, true),
set_preference(cdclt_perform_symmetry_breaking, true),
cdclt_solver:init,
statistics(walltime, [StartCdclt|_]),
cdclt_solve_predicate(sym_smt, Constraint, _SolvedPred, ResCdclt),
statistics(walltime, [StopCdclt|_]),
ResCdclt \= contradiction_found,
TimeCdclt is StopCdclt - StartCdclt,
functor(ResProB, FResProB, _),
functor(ResZ3, FResZ3, _),
functor(ResCdclt, FResCdclt, _),
append(DataAcc, [[AmountOfSatVars,(prob,N,TimeProB,FResProB),(z3,N,TimeZ3,FResZ3),(sym_smt,N,TimeCdclt,FResCdclt)]], NewDataAcc).
Calls:
Name: append/3 |
|
Name: functor/3 |
|
Name: is/2 |
|
Name: \=/2 |
|
Name: statistics/2 |
|
Name: cdclt_solve_predicate/4 |
Module: foo_error |
Name: init/0 |
Module: cdclt_solver |
Name: set_preference/2 |
Module: foo_error |
Name: format/2 |
|
Name: smt_solve_predicate/4 |
Module: foo_error |
Name: solve_predicate/5 |
Module: foo_error |
Name: nl |
|
| Module: cdclt_solver | |
Name: precompute_values/3 |
Module: ast_optimizer_for_smt |
Name: n_queens_encoding/2 |
Module: smt_solver_benchmarks |
Called:
| Module: smt_solver_benchmarks |
run_n_queens_benchmarks :-
N = [4,6,8,10,12,14,16,18,20],
preferences:set_preference(time_out, 60000),
run_n_queens_benchmarks(N, [], Data),
print_n_queens_data(Data).
Calls:
Name: print_n_queens_data/1 |
Module: smt_solver_benchmarks |
| Module: smt_solver_benchmarks | |
Name: set_preference/2 |
Module: preferences |
Name: =/2 |
Called:
| Module: smt_solver_benchmarks |
run_n_queens_benchmarks([], Data, Data).
run_n_queens_benchmarks([N|T], DataAcc, Data) :-
run_n_queens_benchmark(N, DataAcc, NewDataAcc),
run_n_queens_benchmarks(T, NewDataAcc, Data).
Calls:
Name: RECURSIVE_CALL/3 |
Module: smt_solver_benchmarks |
Name: run_n_queens_benchmark/3 |
Module: smt_solver_benchmarks |
Called:
| Module: smt_solver_benchmarks |
select_machine_file_path(FilePaths, MachineFilePath, BenchmarkFilePaths) :-
select(_-MachineFilePath, FilePaths, BenchmarkFilePaths),
( atom_concat(_, '.eventb', MachineFilePath)
; atom_concat(_, '.mch', MachineFilePath)
; atom_concat(_, '.tla', MachineFilePath)
).
Calls:
Name: atom_concat/3 |
|
Name: select/3 |
Module: foo_error |
Called:
Name: run_cbc_benchmarks/2 |
Module: smt_solver_benchmarks |
Name: amount_of_sat_vars/4 |
Module: smt_solver_benchmarks |
setup_scheduler :-
bmachine:b_load_machine_from_file(prob_examples('public_examples/Synthesis_Tests/scheduler.mch')),
bmachine:b_machine_precompile,!.
Calls:
Name: ! |
|
Name: b_machine_precompile/0 |
Module: bmachine |
| Module: bmachine |
Called:
Name: run_misc_benchmarks/0 |
Module: smt_solver_benchmarks |
Name: benchmark/2 |
Module: smt_solver_benchmarks |
solution_or_contradiction(solution(_), solution).
solution_or_contradiction(contradiction_found, contradiction).
Called:
| Module: smt_solver_benchmarks |
solved_constraint(solution(_)).
solved_constraint(contradiction_found).
Called:
Name: benchmark_constraint/23 |
Module: smt_solver_benchmarks |
start_csv_stream(OutputPath, MachineName, Stream) :-
atom_concat(OutputPath, MachineName, TempPath),
atom_concat(TempPath, '_results.csv', EvalFilePath),
nl,nl,write('csv'),nl,
write(EvalFilePath),nl,nl,
open(EvalFilePath, write, Stream),
write(Stream, 'ConstraintPath,Solver,Result,Time (ms)'), nl(Stream).
Calls:
Name: nl/1 |
|
Name: write/2 |
|
Name: open/3 |
|
Name: nl |
|
Name: write/1 |
|
Name: atom_concat/3 |
Called:
| Module: smt_solver_benchmarks |
start_csv_stream_symmetry(OutputPath, MachineName, Stream) :-
atom_concat(OutputPath, MachineName, TempPath),
atom_concat(TempPath, '_sym_preds.csv', EvalFilePath),
nl,nl,write('csv'),nl,
write(EvalFilePath),nl,nl,
open(EvalFilePath, write, Stream),
write(Stream, 'ConstraintPath,Solver,SBPs'), nl(Stream).
Calls:
Name: nl/1 |
|
Name: write/2 |
|
Name: open/3 |
|
Name: nl |
|
Name: write/1 |
|
Name: atom_concat/3 |
write_to_csv_stream(_, _, []).
write_to_csv_stream(SolverName, Stream, [(ConstraintPath,Time)|T]) :-
( benchmark_result(SolverName, ConstraintPath, Result)
-> true
; Result = not_evaluated
),
prepare_result(Result, PResult),
format("~w,~w,~w,~w~n", [ConstraintPath,SolverName,PResult,Time]),
write_to_csv_stream(SolverName, Stream, T).
Calls:
Name: RECURSIVE_CALL/3 |
Module: smt_solver_benchmarks |
Name: format/2 |
|
Name: prepare_result/2 |
Module: smt_solver_benchmarks |
Name: =/2 |
|
Name: true |
|
Name: benchmark_result/3 |
dynamic predicate |
Name: ->/3 |
Called:
| Module: smt_solver_benchmarks |