| 1 | :- module(smt_solver_benchmarks, [run_additional_bmc_benchmarks/1, | |
| 2 | run_additional_inductive_inv_benchmarks/1, | |
| 3 | run_additional_deadlock_benchmarks/1, | |
| 4 | run_misc_benchmarks/0, | |
| 5 | run_bmc_benchmarks1/0, | |
| 6 | run_bmc_benchmarks2/0, | |
| 7 | run_bmc_benchmarks3/0, | |
| 8 | run_bmc_benchmarks4/0, | |
| 9 | run_bmc_benchmarks5/0, | |
| 10 | run_bmc_benchmarks6/0, | |
| 11 | run_deadlock_benchmarks1/0, | |
| 12 | run_deadlock_benchmarks2/0, | |
| 13 | run_deadlock_benchmarks3/0, | |
| 14 | run_deadlock_benchmarks4/0, | |
| 15 | run_deadlock_benchmarks5/0, | |
| 16 | run_deadlock_benchmarks6/0, | |
| 17 | run_cbc_benchmarks1/0, | |
| 18 | run_cbc_benchmarks2/0, | |
| 19 | run_cbc_benchmarks3/0, | |
| 20 | run_cbc_benchmarks4/0, | |
| 21 | run_cbc_benchmarks5/0, | |
| 22 | run_cbc_benchmarks6/0, | |
| 23 | run_cbc_benchmarks/2, | |
| 24 | run_bmc_benchmarks/2, | |
| 25 | run_n_queens_benchmarks/0, | |
| 26 | amount_of_sat_vars_in_dir/1, | |
| 27 | amount_of_sat_vars_bmc/0, | |
| 28 | amount_of_sat_vars_inductive_inv/0, | |
| 29 | amount_of_sat_vars_deadlock/0]). | |
| 30 | ||
| 31 | :- use_module(library(csv)). | |
| 32 | :- use_module(library(lists)). | |
| 33 | :- use_module(library(file_systems)). | |
| 34 | ||
| 35 | :- use_module(probsrc(preferences)). | |
| 36 | :- use_module(probsrc(b_compiler), [b_compile/6]). | |
| 37 | :- use_module(probsrc('cdclt_solver/cdclt_solver')). | |
| 38 | :- use_module(probsrc('cdclt_solver/cdclt_settings')). | |
| 39 | :- use_module(probsrc('alloy2b/alloy2b')). | |
| 40 | :- use_module(probsrc(tools)). | |
| 41 | :- use_module(probsrc(solver_interface)). | |
| 42 | :- use_module(probsrc(parsercall)). | |
| 43 | :- use_module(probsrc(bmachine)). | |
| 44 | :- use_module(probsrc(bsyntaxtree)). | |
| 45 | :- use_module(probsrc(error_manager)). | |
| 46 | :- use_module(probsrc(b_ast_cleanup), [clean_up_pred/3]). | |
| 47 | :- use_module(extrasrc(b2setlog), [solve_pred_with_setlog/3]). | |
| 48 | :- use_module(probsrc('well_def/well_def_analyser'), [prove_sequent/1]). | |
| 49 | :- use_module('../test_paths', []). % set up prob_examples(...) alias | |
| 50 | ||
| 51 | :- use_module(smt_solvers_interface(smt_solvers_interface)). | |
| 52 | :- use_module(cdclt_solver('symmetry_check/smt_symmetry_breaking')). | |
| 53 | ||
| 54 | :- use_module(probsrc(module_information), [module_info/2]). | |
| 55 | ||
| 56 | :- module_info(group, cdclt). | |
| 57 | :- module_info(description,'This module provides benchmarks for the integration of Z3 and the different versions of the CDCL(T) based solver.'). | |
| 58 | ||
| 59 | :- dynamic fastest_solver/3, solved_constraints/2, benchmark_result/3, symmetry_breaking_predicates/3. | |
| 60 | :- volatile fastest_solver/3, solved_constraints/2, benchmark_result/3, symmetry_breaking_predicates/3. | |
| 61 | ||
| 62 | inc_solved_counter(Solver) :- | |
| 63 | (retract(solved_constraints(Solver, Old)); Old = 0), | |
| 64 | !, | |
| 65 | New is Old + 1, | |
| 66 | asserta(solved_constraints(Solver, New)). | |
| 67 | ||
| 68 | add_benchmark_result(Solver, ConstraintPath, Result) :- | |
| 69 | asserta(benchmark_result(Solver,ConstraintPath,Result)). | |
| 70 | ||
| 71 | bmc_timeout(120000). | |
| 72 | inductive_inv_timeout(120000). | |
| 73 | deadlock_timeout(120000). | |
| 74 | ||
| 75 | amount_of_sat_vars_in_dir(DirPath) :- | |
| 76 | % get amount of SAT variables for all ConstraintPath in all .csv files in the current top-level directory | |
| 77 | file_members_of_directory(DirPath, Files), | |
| 78 | findall(CsvFile, (member(_-CsvFile, Files), atom_concat(_, '.csv', CsvFile)), CsvFiles), | |
| 79 | amount_of_sat_vars_csv_files(CsvFiles, [], LAmountOfVars), | |
| 80 | length(LAmountOfVars, Len), | |
| 81 | median_of_list(LAmountOfVars, MedianAmountOfSatVars), | |
| 82 | mean_of_list(LAmountOfVars, MeanAmountOfSatVars), | |
| 83 | max_member(MaxAmountOfSatVars, LAmountOfVars), | |
| 84 | format("AmountOfSatVarsList: ~w~nLen: ~w~nMean: ~w~nMedian: ~w~nMax: ~w~n", [LAmountOfVars,Len,MeanAmountOfSatVars,MedianAmountOfSatVars,MaxAmountOfSatVars]). | |
| 85 | ||
| 86 | amount_of_sat_vars_csv_files([], Acc, Acc). | |
| 87 | amount_of_sat_vars_csv_files([CsvFile|T], Acc, LAmountOfVars) :- | |
| 88 | open(CsvFile, read, Stream, [encoding(utf8)]), | |
| 89 | read_records(Stream, Records), | |
| 90 | close(Stream), | |
| 91 | Records = [Header|CsvRecords], | |
| 92 | Header = [string(Codes)|_], | |
| 93 | atom_codes('ConstraintPath', Codes), | |
| 94 | amount_of_sat_vars_csv_records(CsvRecords, Acc, NAcc), !, | |
| 95 | amount_of_sat_vars_csv_files(T, NAcc, LAmountOfVars). | |
| 96 | amount_of_sat_vars_csv_files([CsvFile|T], Acc, LAmountOfVars) :- | |
| 97 | format("CSV file has wrong format: ~w~n", [CsvFile]), | |
| 98 | amount_of_sat_vars_csv_files(T, Acc, LAmountOfVars). | |
| 99 | ||
| 100 | amount_of_sat_vars_csv_records([], Acc, Acc). | |
| 101 | amount_of_sat_vars_csv_records([CsvRecord|T], Acc, Out) :- | |
| 102 | CsvRecord = [string(Codes),string(CodesSolver)|_], | |
| 103 | atom_codes(prob, CodesSolver), % only for one solver, e.g., prob | |
| 104 | atom_codes(ConstraintPath, Codes), | |
| 105 | % patch to get the correct ProB Examples model path from the constraint's path | |
| 106 | %get_machine_path_from_inductive_inv_bench_path(ConstraintPath, MachinePath), | |
| 107 | %get_machine_path_from_deadlock_freedom_bench_path(ConstraintPath, MachinePath), | |
| 108 | get_machine_path_from_bmc_bench_path(ConstraintPath, MachinePath), | |
| 109 | load_b_eventb_or_tla(MachinePath), | |
| 110 | format("Count SAT vars for ~w~n", [ConstraintPath]), | |
| 111 | amount_of_sat_vars_for_benchmark([ConstraintPath], AmountOfSatVars), | |
| 112 | append(AmountOfSatVars, Acc, NAcc), !, | |
| 113 | amount_of_sat_vars_csv_records(T, NAcc, Out). | |
| 114 | amount_of_sat_vars_csv_records([_|T], Acc, Out) :- | |
| 115 | amount_of_sat_vars_csv_records(T, Acc, Out). | |
| 116 | ||
| 117 | atomic_list_concat(Atom,Separator,Res) :- | |
| 118 | atom_chars(Atom,CAtom), | |
| 119 | atomic_list_concat_(CAtom,Separator,List), | |
| 120 | maplist(atom_chars,Res,List). | |
| 121 | ||
| 122 | atomic_list_concat_([],_,[[]]) :- ! . | |
| 123 | atomic_list_concat_([A|As],Sep,[[]|Args]) :- | |
| 124 | A=Sep, | |
| 125 | atomic_list_concat_(As,Sep,Args). | |
| 126 | atomic_list_concat_([A|As],Sep,[[A|Arg]|Args]) :- | |
| 127 | A\=Sep, | |
| 128 | atomic_list_concat_(As,Sep,[Arg|Args]). | |
| 129 | ||
| 130 | join_atom_list([Atom], _, Out) :- | |
| 131 | !, | |
| 132 | Out = Atom. | |
| 133 | join_atom_list([Atom|T], Sep, Out) :- | |
| 134 | atom_codes(Atom, Codes), | |
| 135 | atom_codes(Sep, SepCodes), | |
| 136 | join_atom_list(T, SepCodes, Codes, NAcc), | |
| 137 | atom_codes(Out, NAcc). | |
| 138 | ||
| 139 | join_atom_list([], _, Acc, Acc). | |
| 140 | join_atom_list([Atom|T], SepCodes, Acc, Codes) :- | |
| 141 | atom_codes(Atom, ACodes), | |
| 142 | append([Acc,SepCodes,ACodes], NAcc), | |
| 143 | join_atom_list(T, SepCodes, NAcc, Codes). | |
| 144 | ||
| 145 | get_machine_path_from_bmc_bench_path(ConstraintPath, MachinePath) :- | |
| 146 | atom_concat('/home/joshua/raw_benchmarks/additional_benchmarks_bmc/', Postfix, ConstraintPath), | |
| 147 | atomic_list_concat(Postfix, '_', Split), | |
| 148 | append(PreSplit, [monolithic,bmc|_], Split), | |
| 149 | join_atom_list(PreSplit, '_', PreClean), | |
| 150 | atom_concat('../prob_examples/', PreClean, FullPrefix), | |
| 151 | atom_concat(FullPrefix, '.mch', MchPath), | |
| 152 | atom_concat(FullPrefix, '.eventb', EventBPath), | |
| 153 | atom_concat(FullPrefix, '.tla', TlaPath), | |
| 154 | ( file_exists(MchPath) | |
| 155 | -> MachinePath = MchPath | |
| 156 | ; file_exists(EventBPath) | |
| 157 | -> MachinePath = EventBPath | |
| 158 | ; file_exists(TlaPath), | |
| 159 | MachinePath = TlaPath | |
| 160 | ). | |
| 161 | ||
| 162 | get_machine_path_from_deadlock_freedom_bench_path(ConstraintPath, MachinePath) :- | |
| 163 | atom_concat('/home/joshua/raw_benchmarks/additional_benchmarks_deadlock/', Postfix, ConstraintPath), | |
| 164 | atomic_list_concat(Postfix, '_', Split), | |
| 165 | append(PreSplit, [deadlock,'freedom.eval'|_], Split), | |
| 166 | join_atom_list(PreSplit, '_', PreClean), | |
| 167 | atom_concat('../prob_examples/', PreClean, FullPrefix), | |
| 168 | atom_concat(FullPrefix, '.mch', MchPath), | |
| 169 | atom_concat(FullPrefix, '.eventb', EventBPath), | |
| 170 | atom_concat(FullPrefix, '.tla', TlaPath), | |
| 171 | ( file_exists(MchPath) | |
| 172 | -> MachinePath = MchPath | |
| 173 | ; file_exists(EventBPath) | |
| 174 | -> MachinePath = EventBPath | |
| 175 | ; file_exists(TlaPath), | |
| 176 | MachinePath = TlaPath | |
| 177 | ). | |
| 178 | ||
| 179 | get_machine_path_from_inductive_inv_bench_path(ConstraintPath, MachinePath) :- | |
| 180 | atom_concat('/home/joshua/raw_benchmarks/additional_benchmarks_inductive_inv/', Postfix, ConstraintPath), | |
| 181 | atomic_list_concat(Postfix, '_', Split), | |
| 182 | append(PreSplit, [inductive,inv|_], Split), | |
| 183 | join_atom_list(PreSplit, '_', PreClean), | |
| 184 | atom_concat('../prob_examples/', PreClean, FullPrefix), | |
| 185 | atom_concat(FullPrefix, '.mch', MchPath), | |
| 186 | atom_concat(FullPrefix, '.eventb', EventBPath), | |
| 187 | atom_concat(FullPrefix, '.tla', TlaPath), | |
| 188 | ( file_exists(MchPath) | |
| 189 | -> MachinePath = MchPath | |
| 190 | ; file_exists(EventBPath) | |
| 191 | -> MachinePath = EventBPath | |
| 192 | ; file_exists(TlaPath), | |
| 193 | MachinePath = TlaPath | |
| 194 | ). | |
| 195 | ||
| 196 | amount_of_sat_vars_deadlock :- | |
| 197 | amount_of_sat_vars(deadlock, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/abz16_m4/', [], Acc1), | |
| 198 | amount_of_sat_vars(deadlock, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/abz16_m5/', Acc1, Acc2), | |
| 199 | amount_of_sat_vars(deadlock, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/abz16_m6/', Acc2, Acc3), | |
| 200 | amount_of_sat_vars(deadlock, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/abz16_m7/', Acc3, Acc4), | |
| 201 | amount_of_sat_vars(deadlock, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/r0_geardoor/', Acc4, Acc5), | |
| 202 | amount_of_sat_vars(deadlock, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/r1_valve/', Acc5, Acc6), | |
| 203 | amount_of_sat_vars(deadlock, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/r2_outputs/', Acc6, Acc7), | |
| 204 | amount_of_sat_vars(deadlock, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/r3_sensors/', Acc7, Acc8), | |
| 205 | amount_of_sat_vars(deadlock, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/r4_handle/', Acc8, Acc9), | |
| 206 | amount_of_sat_vars(deadlock, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/r5_switch/', Acc9, Acc10), | |
| 207 | amount_of_sat_vars(deadlock, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/pm_m0_aai/', Acc10, Acc11), | |
| 208 | amount_of_sat_vars(deadlock, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/pm_m0_aat/', Acc11, Acc12), | |
| 209 | amount_of_sat_vars(deadlock, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/pm_m0_aoo/', Acc12, Acc13), | |
| 210 | amount_of_sat_vars(deadlock, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/pm_m0_voo/', Acc13, Acc14), | |
| 211 | amount_of_sat_vars(deadlock, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/pm_m0_vvi/', Acc14, Acc15), | |
| 212 | amount_of_sat_vars(deadlock, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/pm_m0_vvt/', Acc15, Acc16), | |
| 213 | amount_of_sat_vars(deadlock, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/pm_m1_aoor/', Acc16, Acc17), | |
| 214 | amount_of_sat_vars(deadlock, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/pm_m1_voor/', Acc17, Acc18), | |
| 215 | amount_of_sat_vars(deadlock, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/pm_m2_aai/', Acc18, Acc19), | |
| 216 | amount_of_sat_vars(deadlock, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/simple-two-phase/', Acc19, Acc20), | |
| 217 | amount_of_sat_vars(deadlock, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/prisoners-4/', Acc20, Acc21), | |
| 218 | amount_of_sat_vars(deadlock, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/bakery/', Acc21, Acc22), | |
| 219 | amount_of_sat_vars(deadlock, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/paxos-3/', Acc22, Acc23), | |
| 220 | amount_of_sat_vars(deadlock, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/lightbot/', Acc23, Acc24), | |
| 221 | amount_of_sat_vars(deadlock, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/travel_agency/', Acc24, Acc25), | |
| 222 | amount_of_sat_vars(deadlock, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/search_events/', Acc25, Acc26), | |
| 223 | amount_of_sat_vars(deadlock, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/large_branching/', Acc26, Acc27), | |
| 224 | mean_of_list(Acc27, TotalMean), | |
| 225 | median_of_list(Acc27, TotalMedian), | |
| 226 | max_member(Max, Acc27), | |
| 227 | open('amount_of_sat_vars_deadlock/total.txt', write, Stream), | |
| 228 | tell(Stream), | |
| 229 | format("Total mean: ~w~nTotal median: ~w~nTotal max: ~w~n", [TotalMean,TotalMedian,Max]), | |
| 230 | close(Stream). | |
| 231 | ||
| 232 | amount_of_sat_vars_inductive_inv :- | |
| 233 | amount_of_sat_vars(inductive_inv, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/abz16_m4/', [], Acc1), | |
| 234 | amount_of_sat_vars(inductive_inv, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/abz16_m5/', Acc1, Acc2), | |
| 235 | amount_of_sat_vars(inductive_inv, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/abz16_m6/', Acc2, Acc3), | |
| 236 | amount_of_sat_vars(inductive_inv, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/abz16_m7/', Acc3, Acc4), | |
| 237 | amount_of_sat_vars(inductive_inv, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/r0_geardoor/', Acc4, Acc5), | |
| 238 | amount_of_sat_vars(inductive_inv, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/r1_valve/', Acc5, Acc6), | |
| 239 | amount_of_sat_vars(inductive_inv, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/r2_outputs/', Acc6, Acc7), | |
| 240 | amount_of_sat_vars(inductive_inv, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/r3_sensors/', Acc7, Acc8), | |
| 241 | amount_of_sat_vars(inductive_inv, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/r4_handle/', Acc8, Acc9), | |
| 242 | amount_of_sat_vars(inductive_inv, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/r5_switch/', Acc9, Acc10), | |
| 243 | amount_of_sat_vars(inductive_inv, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/pm_m0_aai/', Acc10, Acc11), | |
| 244 | amount_of_sat_vars(inductive_inv, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/pm_m0_aat/', Acc11, Acc12), | |
| 245 | amount_of_sat_vars(inductive_inv, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/pm_m0_aoo/', Acc12, Acc13), | |
| 246 | amount_of_sat_vars(inductive_inv, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/pm_m0_voo/', Acc13, Acc14), | |
| 247 | amount_of_sat_vars(inductive_inv, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/pm_m0_vvi/', Acc14, Acc15), | |
| 248 | amount_of_sat_vars(inductive_inv, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/pm_m0_vvt/', Acc15, Acc16), | |
| 249 | amount_of_sat_vars(inductive_inv, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/pm_m1_aoor/', Acc16, Acc17), | |
| 250 | amount_of_sat_vars(inductive_inv, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/pm_m1_voor/', Acc17, Acc18), | |
| 251 | amount_of_sat_vars(inductive_inv, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/pm_m2_aai/', Acc18, Acc19), | |
| 252 | amount_of_sat_vars(inductive_inv, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/r6_lights/', Acc19, Acc20), | |
| 253 | amount_of_sat_vars(inductive_inv, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/prisoners-4/', Acc20, Acc21), | |
| 254 | amount_of_sat_vars(inductive_inv, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/bakery/', Acc21, Acc22), | |
| 255 | amount_of_sat_vars(inductive_inv, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/paxos-3/', Acc22, Acc23), | |
| 256 | amount_of_sat_vars(inductive_inv, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/lightbot/', Acc23, Acc24), | |
| 257 | amount_of_sat_vars(inductive_inv, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/travel_agency/', Acc24, Acc25), | |
| 258 | amount_of_sat_vars(inductive_inv, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/search_events/', Acc25, Acc26), | |
| 259 | amount_of_sat_vars(inductive_inv, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/large_branching/', Acc26, Acc27), | |
| 260 | mean_of_list(Acc27, TotalMean), | |
| 261 | median_of_list(Acc27, TotalMedian), | |
| 262 | max_member(Max, Acc27), | |
| 263 | open('amount_of_sat_vars_inductive_inv/total.txt', write, Stream), | |
| 264 | tell(Stream), | |
| 265 | format("Total mean: ~w~nTotal median: ~w~nTotal max: ~w~n", [TotalMean,TotalMedian,Max]), | |
| 266 | close(Stream). | |
| 267 | ||
| 268 | amount_of_sat_vars_bmc :- | |
| 269 | amount_of_sat_vars(bmc, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_bmc/abz16_m4/', [], Acc1), | |
| 270 | amount_of_sat_vars(bmc, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_bmc/abz16_m5/', Acc1, Acc2), | |
| 271 | amount_of_sat_vars(bmc, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_bmc/abz16_m6/', Acc2, Acc3), | |
| 272 | amount_of_sat_vars(bmc, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_bmc/abz16_m7/', Acc3, Acc4), | |
| 273 | amount_of_sat_vars(bmc, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_bmc/r0_geardoor/', Acc4, Acc5), | |
| 274 | amount_of_sat_vars(bmc, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_bmc/r1_valve/', Acc5, Acc6), | |
| 275 | amount_of_sat_vars(bmc, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_bmc/r2_outputs/', Acc6, Acc7), | |
| 276 | amount_of_sat_vars(bmc, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_bmc/r3_sensors/', Acc7, Acc8), | |
| 277 | amount_of_sat_vars(bmc, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_bmc/r4_handle/', Acc8, Acc9), | |
| 278 | amount_of_sat_vars(bmc, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_bmc/r5_switch/', Acc9, Acc10), | |
| 279 | amount_of_sat_vars(bmc, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_bmc/pm_m0_aai/', Acc10, Acc11), | |
| 280 | amount_of_sat_vars(bmc, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_bmc/pm_m0_aat/', Acc11, Acc12), | |
| 281 | amount_of_sat_vars(bmc, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_bmc/pm_m0_aoo/', Acc12, Acc13), | |
| 282 | amount_of_sat_vars(bmc, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_bmc/pm_m0_voo/', Acc13, Acc14), | |
| 283 | amount_of_sat_vars(bmc, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_bmc/pm_m0_vvi/', Acc14, Acc15), | |
| 284 | amount_of_sat_vars(bmc, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_bmc/pm_m0_vvt/', Acc15, Acc16), | |
| 285 | amount_of_sat_vars(bmc, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_bmc/pm_m1_aoor/', Acc16, Acc17), | |
| 286 | amount_of_sat_vars(bmc, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_bmc/pm_m1_voor/', Acc17, Acc18), | |
| 287 | amount_of_sat_vars(bmc, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_bmc/pm_m2_aai/', Acc18, Acc19), | |
| 288 | amount_of_sat_vars(bmc, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_bmc/simple-two-phase/', Acc19, Acc20), | |
| 289 | amount_of_sat_vars(bmc, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_bmc/prisoners-4/', Acc20, Acc21), | |
| 290 | amount_of_sat_vars(bmc, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_bmc/bakery/', Acc21, Acc22), | |
| 291 | amount_of_sat_vars(bmc, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_bmc/paxos-3/', Acc22, Acc23), | |
| 292 | amount_of_sat_vars(bmc, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_bmc/lightbot/', Acc23, Acc24), | |
| 293 | amount_of_sat_vars(bmc, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_bmc/travel_agency/', Acc24, Acc25), | |
| 294 | amount_of_sat_vars(bmc, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_bmc/search_events/', Acc25, Acc26), | |
| 295 | amount_of_sat_vars(bmc, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_bmc/large_branching/', Acc26, Acc27), | |
| 296 | amount_of_sat_vars(bmc, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_bmc/r6_lights/', Acc27, Acc28), | |
| 297 | mean_of_list(Acc28, TotalMean), | |
| 298 | median_of_list(Acc28, TotalMedian), | |
| 299 | max_member(Max, Acc28), | |
| 300 | open('amount_of_sat_vars_bmc/total.txt', write, Stream), | |
| 301 | tell(Stream), | |
| 302 | format("Total mean: ~w~nTotal median: ~w~nTotal max: ~w~n", [TotalMean,TotalMedian,Max]), | |
| 303 | close(Stream). | |
| 304 | ||
| 305 | run_deadlock_benchmarks1 :- | |
| 306 | deadlock_timeout(Timeout), | |
| 307 | preferences:set_preference(time_out, Timeout), | |
| 308 | /*run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/abz16_m0/'), | |
| 309 | run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/abz16_m1/'), | |
| 310 | run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/abz16_m2/'), | |
| 311 | run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/abz16_m3/'),*/ | |
| 312 | run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/abz16_m4/'), | |
| 313 | run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/abz16_m5/'), | |
| 314 | run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/abz16_m6/'), | |
| 315 | run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/abz16_m7/'). | |
| 316 | ||
| 317 | run_deadlock_benchmarks2 :- | |
| 318 | deadlock_timeout(Timeout), | |
| 319 | preferences:set_preference(time_out, Timeout), | |
| 320 | run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/r0_geardoor/'), | |
| 321 | run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/r1_valve/'), | |
| 322 | run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/r2_outputs/'), | |
| 323 | run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/r3_sensors/'), | |
| 324 | run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/r4_handle/'), | |
| 325 | run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/r5_switch/'). | |
| 326 | %run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/r6_lights/'), % static contradiction | |
| 327 | ||
| 328 | run_deadlock_benchmarks3 :- | |
| 329 | deadlock_timeout(Timeout), | |
| 330 | preferences:set_preference(time_out, Timeout), | |
| 331 | run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/pm_m0_aai/'), | |
| 332 | run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/pm_m0_aat/'), | |
| 333 | run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/pm_m0_aoo/'), | |
| 334 | run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/pm_m0_voo/'). | |
| 335 | /* | |
| 336 | run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/pm_m2_aat/'), | |
| 337 | run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/pm_m2_vvi/'), | |
| 338 | run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/pm_m2_vvt/'), | |
| 339 | run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/pm_m3_aai/'), | |
| 340 | run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/pm_m3_aat/'), | |
| 341 | run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/pm_m3_vvi/'), | |
| 342 | run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/pm_m3_vvt/'), | |
| 343 | run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/pm_m4_aair/'), | |
| 344 | run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/pm_m4_aatr/'), | |
| 345 | run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/pm_m4_vvir/'), | |
| 346 | run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/pm_m4_vvtr/'),*/ | |
| 347 | ||
| 348 | run_deadlock_benchmarks4 :- | |
| 349 | deadlock_timeout(Timeout), | |
| 350 | preferences:set_preference(time_out, Timeout), | |
| 351 | run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/pm_m0_vvi/'), | |
| 352 | run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/pm_m0_vvt/'), | |
| 353 | run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/pm_m1_aoor/'), | |
| 354 | run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/pm_m1_voor/'), | |
| 355 | run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/pm_m2_aai/'). | |
| 356 | ||
| 357 | run_deadlock_benchmarks5 :- | |
| 358 | deadlock_timeout(Timeout), | |
| 359 | preferences:set_preference(time_out, Timeout), | |
| 360 | run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/simple-two-phase/'), | |
| 361 | run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/prisoners-4/'), | |
| 362 | run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/bakery/'), | |
| 363 | run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/paxos-3/'). | |
| 364 | ||
| 365 | run_deadlock_benchmarks6 :- | |
| 366 | deadlock_timeout(Timeout), | |
| 367 | preferences:set_preference(time_out, Timeout), | |
| 368 | run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/lightbot/'), | |
| 369 | run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/travel_agency/'), | |
| 370 | run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/search_events/'), | |
| 371 | run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_cbc_deadlock/large_branching/'). | |
| 372 | ||
| 373 | run_cbc_benchmarks1 :- | |
| 374 | inductive_inv_timeout(Timeout), | |
| 375 | preferences:set_preference(time_out, Timeout), | |
| 376 | /*run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/abz16_m0/'), | |
| 377 | run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/abz16_m1/'), | |
| 378 | run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/abz16_m2/'), | |
| 379 | run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/abz16_m3/'),*/ | |
| 380 | run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/abz16_m4/'), | |
| 381 | run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/abz16_m5/'), | |
| 382 | run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/abz16_m6/'), | |
| 383 | run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/abz16_m7/'). | |
| 384 | ||
| 385 | run_cbc_benchmarks2 :- | |
| 386 | inductive_inv_timeout(Timeout), | |
| 387 | preferences:set_preference(time_out, Timeout), | |
| 388 | run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/r0_geardoor/'), | |
| 389 | run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/r1_valve/'), | |
| 390 | run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/r2_outputs/'), | |
| 391 | run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/r3_sensors/'), | |
| 392 | run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/r4_handle/'), | |
| 393 | run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/r5_switch/'), | |
| 394 | run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/r6_lights/'). | |
| 395 | ||
| 396 | run_cbc_benchmarks3 :- | |
| 397 | inductive_inv_timeout(Timeout), | |
| 398 | preferences:set_preference(time_out, Timeout), | |
| 399 | run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/pm_m0_aai/'), | |
| 400 | run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/pm_m0_aat/'), | |
| 401 | run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/pm_m0_aoo/'), | |
| 402 | run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/pm_m0_voo/'). | |
| 403 | /*run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/pm_m2_aat/'), | |
| 404 | run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/pm_m2_vvi/'), | |
| 405 | run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/pm_m2_vvt/'), | |
| 406 | run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/pm_m3_aai/'), | |
| 407 | run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/pm_m3_aat/'), | |
| 408 | run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/pm_m3_vvi/'), | |
| 409 | run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/pm_m3_vvt/'), | |
| 410 | run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/pm_m4_aair/'), | |
| 411 | run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/pm_m4_aatr/'), | |
| 412 | run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/pm_m4_vvir/'), | |
| 413 | run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/pm_m4_vvtr/'),*/ | |
| 414 | ||
| 415 | run_cbc_benchmarks4 :- | |
| 416 | inductive_inv_timeout(Timeout), | |
| 417 | preferences:set_preference(time_out, Timeout), | |
| 418 | run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/pm_m0_vvi/'), | |
| 419 | run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/pm_m0_vvt/'), | |
| 420 | run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/pm_m1_aoor/'), | |
| 421 | run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/pm_m1_voor/'), | |
| 422 | run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/pm_m2_aai/'). | |
| 423 | ||
| 424 | run_cbc_benchmarks5 :- | |
| 425 | inductive_inv_timeout(Timeout), | |
| 426 | preferences:set_preference(time_out, Timeout), | |
| 427 | %run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/simple-two-phase/'), % static contradiction | |
| 428 | run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/prisoners-4/'), | |
| 429 | run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/bakery/'), | |
| 430 | run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/paxos-3/'). | |
| 431 | ||
| 432 | run_cbc_benchmarks6 :- | |
| 433 | inductive_inv_timeout(Timeout), | |
| 434 | preferences:set_preference(time_out, Timeout), | |
| 435 | run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/lightbot/'), | |
| 436 | run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/travel_agency/'), | |
| 437 | run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/search_events/'), | |
| 438 | run_cbc_benchmarks(false, '../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/benchmarks_inductive_inv/large_branching/'). | |
| 439 | ||
| 440 | /* | |
| 441 | Transformation from B AST to pretty print: | |
| 442 | preferences:set_preference(translate_force_all_typing_infos, true), preferences:set_preference(translate_print_typing_infos, true), open('/home/joshua/raw_benchmarks/benchmarks_bmc/bakery/Bakery_monolithic_bmc_k_0.txt', read, S1, [encoding(utf8)]), read(S1, C1), close(S1), open('/home/joshua/raw_benchmarks/benchmarks_bmc/bakery/Bakery_monolithic_bmc_k_0.eval', write, S11, [encoding(utf8)]), tell(S11), translate:print_bexpr(C1), close(S11) | |
| 443 | */ | |
| 444 | ||
| 445 | run_bmc_benchmarks1 :- | |
| 446 | bmc_timeout(Timeout), | |
| 447 | preferences:set_preference(time_out, Timeout), | |
| 448 | %run_bmc_benchmarks(false, '/home/joshua/raw_benchmarks/benchmarks_bmc/paxos-5/'), | |
| 449 | %run_bmc_benchmarks(false, '/home/joshua/raw_benchmarks/benchmarks_bmc/abz16_m0/'), | |
| 450 | /*run_bmc_benchmarks(false, '/home/joshua/raw_benchmarks/benchmarks_bmc/abz16_m1/'), | |
| 451 | run_bmc_benchmarks(false, '/home/joshua/raw_benchmarks/benchmarks_bmc/abz16_m2/'), | |
| 452 | run_bmc_benchmarks(false, '/home/joshua/raw_benchmarks/benchmarks_bmc/abz16_m3/'),*/ | |
| 453 | run_bmc_benchmarks(false, '/home/joshua/raw_benchmarks/benchmarks_bmc/abz16_m6/'), | |
| 454 | run_bmc_benchmarks(false, '/home/joshua/raw_benchmarks/benchmarks_bmc/abz16_m7/'). | |
| 455 | ||
| 456 | run_bmc_benchmarks11 :- | |
| 457 | bmc_timeout(Timeout), | |
| 458 | preferences:set_preference(time_out, Timeout), | |
| 459 | run_bmc_benchmarks(false, '/home/joshua/raw_benchmarks/benchmarks_bmc/abz16_m4/'), | |
| 460 | run_bmc_benchmarks(false, '/home/joshua/raw_benchmarks/benchmarks_bmc/abz16_m5/'). | |
| 461 | ||
| 462 | run_bmc_benchmarks2 :- | |
| 463 | bmc_timeout(Timeout), | |
| 464 | preferences:set_preference(time_out, Timeout), | |
| 465 | run_bmc_benchmarks(false, '/home/joshua/raw_benchmarks/benchmarks_bmc/r4_handle/'), | |
| 466 | run_bmc_benchmarks(false, '/home/joshua/raw_benchmarks/benchmarks_bmc/r5_switch/'), | |
| 467 | run_bmc_benchmarks(false, '/home/joshua/raw_benchmarks/benchmarks_bmc/r6_lights/'). | |
| 468 | ||
| 469 | run_bmc_benchmarks22 :- | |
| 470 | bmc_timeout(Timeout), | |
| 471 | preferences:set_preference(time_out, Timeout), | |
| 472 | run_bmc_benchmarks(false, '/home/joshua/raw_benchmarks/benchmarks_bmc/r0_geardoor/'), | |
| 473 | run_bmc_benchmarks(false, '/home/joshua/raw_benchmarks/benchmarks_bmc/r1_valve/'), | |
| 474 | run_bmc_benchmarks(false, '/home/joshua/raw_benchmarks/benchmarks_bmc/r2_outputs/'), | |
| 475 | run_bmc_benchmarks(false, '/home/joshua/raw_benchmarks/benchmarks_bmc/r3_sensors/'). | |
| 476 | ||
| 477 | run_bmc_benchmarks3 :- | |
| 478 | bmc_timeout(Timeout), | |
| 479 | preferences:set_preference(time_out, Timeout), | |
| 480 | run_bmc_benchmarks(false, '/home/joshua/raw_benchmarks/benchmarks_bmc/pm_m0_aai/'), | |
| 481 | run_bmc_benchmarks(false, '/home/joshua/raw_benchmarks/benchmarks_bmc/pm_m0_aat/'). | |
| 482 | ||
| 483 | run_bmc_benchmarks33 :- | |
| 484 | bmc_timeout(Timeout), | |
| 485 | preferences:set_preference(time_out, Timeout), | |
| 486 | run_bmc_benchmarks(false, '/home/joshua/raw_benchmarks/benchmarks_bmc/pm_m0_aoo/'), | |
| 487 | run_bmc_benchmarks(false, '/home/joshua/raw_benchmarks/benchmarks_bmc/pm_m0_voo/'), | |
| 488 | run_bmc_benchmarks(false, '/home/joshua/raw_benchmarks/benchmarks_bmc/pm_m0_vvi/'). | |
| 489 | ||
| 490 | run_bmc_benchmarks4 :- | |
| 491 | bmc_timeout(Timeout), | |
| 492 | preferences:set_preference(time_out, Timeout), | |
| 493 | run_bmc_benchmarks(false, '/home/joshua/raw_benchmarks/benchmarks_bmc/pm_m0_vvt/'), | |
| 494 | run_bmc_benchmarks(false, '/home/joshua/raw_benchmarks/benchmarks_bmc/pm_m1_aoor/'), | |
| 495 | run_bmc_benchmarks(false, '/home/joshua/raw_benchmarks/benchmarks_bmc/pm_m1_voor/'), | |
| 496 | run_bmc_benchmarks(false, '/home/joshua/raw_benchmarks/benchmarks_bmc/pm_m2_aai/'). | |
| 497 | /*run_bmc_benchmarks(false, '/home/joshua/raw_benchmarks/benchmarks_bmc/pm_m2_aat/'), | |
| 498 | run_bmc_benchmarks(false, '/home/joshua/raw_benchmarks/benchmarks_bmc/pm_m2_vvi/'), | |
| 499 | run_bmc_benchmarks(false, '/home/joshua/raw_benchmarks/benchmarks_bmc/pm_m2_vvt/'), | |
| 500 | run_bmc_benchmarks(false, '/home/joshua/raw_benchmarks/benchmarks_bmc/pm_m3_aai/'), | |
| 501 | run_bmc_benchmarks(false, '/home/joshua/raw_benchmarks/benchmarks_bmc/pm_m3_aat/'), | |
| 502 | run_bmc_benchmarks(false, '/home/joshua/raw_benchmarks/benchmarks_bmc/pm_m3_vvi/'), | |
| 503 | run_bmc_benchmarks(false, '/home/joshua/raw_benchmarks/benchmarks_bmc/pm_m3_vvt/'), | |
| 504 | run_bmc_benchmarks(false, '/home/joshua/raw_benchmarks/benchmarks_bmc/pm_m4_aair/'), | |
| 505 | run_bmc_benchmarks(false, '/home/joshua/raw_benchmarks/benchmarks_bmc/pm_m4_aatr/'), | |
| 506 | run_bmc_benchmarks(false, '/home/joshua/raw_benchmarks/benchmarks_bmc/pm_m4_vvir/'), | |
| 507 | run_bmc_benchmarks(false, '/home/joshua/raw_benchmarks/benchmarks_bmc/pm_m4_vvtr/')*/ | |
| 508 | ||
| 509 | run_bmc_benchmarks5 :- | |
| 510 | bmc_timeout(Timeout), | |
| 511 | preferences:set_preference(time_out, Timeout), | |
| 512 | run_bmc_benchmarks(false, '/home/joshua/raw_benchmarks/benchmarks_bmc/simple-two-phase/'), | |
| 513 | run_bmc_benchmarks(false, '/home/joshua/raw_benchmarks/benchmarks_bmc/lightbot/'), | |
| 514 | run_bmc_benchmarks(false, '/home/joshua/raw_benchmarks/benchmarks_bmc/travel_agency/'), | |
| 515 | run_bmc_benchmarks(false, '/home/joshua/raw_benchmarks/benchmarks_bmc/search_events/'). | |
| 516 | ||
| 517 | run_bmc_benchmarks6 :- | |
| 518 | bmc_timeout(Timeout), | |
| 519 | preferences:set_preference(time_out, Timeout), | |
| 520 | run_bmc_benchmarks(false, '/home/joshua/raw_benchmarks/benchmarks_bmc/large_branching/'), | |
| 521 | run_bmc_benchmarks(false, '/home/joshua/raw_benchmarks/benchmarks_bmc/prisoners-4/'), | |
| 522 | run_bmc_benchmarks(false, '/home/joshua/raw_benchmarks/benchmarks_bmc/bakery/'), | |
| 523 | run_bmc_benchmarks(false, '/home/joshua/raw_benchmarks/benchmarks_bmc/paxos-3/'). | |
| 524 | ||
| 525 | run_additional_bmc_benchmarks(UseIdlSolver) :- | |
| 526 | findall(ExamplesPath, additional_benchmark_model(_, ExamplesPath), ExamplesPaths), | |
| 527 | run_additional_bmc_benchmarks(UseIdlSolver, ExamplesPaths). | |
| 528 | ||
| 529 | run_additional_bmc_benchmarks(_, []). | |
| 530 | run_additional_bmc_benchmarks(UseIdlSolver, [ExamplesPath|T]) :- | |
| 531 | run_additional_bmc_benchmark(UseIdlSolver, ExamplesPath), | |
| 532 | run_additional_bmc_benchmarks(UseIdlSolver, T). | |
| 533 | ||
| 534 | run_additional_bmc_benchmark(UseIdlSolver, ExamplesPath) :- | |
| 535 | atom_concat('../cbc_benchmarks/bounded_model_checking/', ExamplesPath, FullExamplesPath), | |
| 536 | atom_concat('../prob_examples/', ExamplesPath, MachinePath), | |
| 537 | load_b_eventb_or_tla(MachinePath), | |
| 538 | get_filename_from_path(MachinePath, FileName), | |
| 539 | atom_concat('../cbc_benchmarks/results/bounded_model_checking/', FileName, TempPath), | |
| 540 | atom_concat(TempPath, '_results.csv', ResultPath), | |
| 541 | \+ file_exists(ResultPath), | |
| 542 | !, % don't run benchmark if result already exists | |
| 543 | ( atom_concat(Prefix, '.eventb', FullExamplesPath) | |
| 544 | ; atom_concat(Prefix, '.mch', FullExamplesPath) | |
| 545 | ; atom_concat(Prefix, '.tla', FullExamplesPath) | |
| 546 | ), | |
| 547 | atom_concat(Prefix, '_monolithic_bmc_k_1.eval', Path1), | |
| 548 | atom_concat(Prefix, '_monolithic_bmc_k_5.eval', Path2), | |
| 549 | atom_concat(Prefix, '_monolithic_bmc_k_10.eval', Path3), | |
| 550 | retractall(cdclt_sat_solver:incremental_mode), | |
| 551 | benchmark_constraints(UseIdlSolver, [Path1,Path2,Path3], [], Data), | |
| 552 | retractall(cdclt_sat_solver:memoize_backjump_clause(_, _, _)), | |
| 553 | eval_benchmark_data_csv('../cbc_benchmarks/results/bounded_model_checking/', FileName, 'Additional BMC benchmarks', Data). | |
| 554 | run_additional_bmc_benchmark(_, _). | |
| 555 | ||
| 556 | run_additional_inductive_inv_benchmarks(UseIdlSolver) :- | |
| 557 | findall(ExamplesPath, additional_benchmark_model(_, ExamplesPath), ExamplesPaths), | |
| 558 | run_additional_inductive_inv_benchmarks(UseIdlSolver, ExamplesPaths). | |
| 559 | ||
| 560 | run_additional_inductive_inv_benchmarks(_, []). | |
| 561 | run_additional_inductive_inv_benchmarks(UseIdlSolver, [ExamplesPath|T]) :- | |
| 562 | run_additional_inductive_inv_benchmark(UseIdlSolver, ExamplesPath), | |
| 563 | run_additional_inductive_inv_benchmarks(UseIdlSolver, T). | |
| 564 | ||
| 565 | run_additional_inductive_inv_benchmark(UseIdlSolver, ExamplesPath) :- | |
| 566 | atom_concat('../cbc_benchmarks/inductive_invariant_checking/', ExamplesPath, FullExamplesPath), | |
| 567 | atom_concat('../prob_examples/', ExamplesPath, MachinePath), | |
| 568 | load_b_eventb_or_tla(MachinePath), | |
| 569 | get_filename_from_path(MachinePath, FileName), | |
| 570 | atom_concat('../cbc_benchmarks/results/inductive_invariant_checking/', FileName, TempPath), | |
| 571 | atom_concat(TempPath, '_results.csv', ResultPath), | |
| 572 | \+ file_exists(ResultPath), | |
| 573 | !, % don't run benchmark if result already exists | |
| 574 | ( atom_concat(Prefix, '.eventb', FullExamplesPath) | |
| 575 | ; atom_concat(Prefix, '.mch', FullExamplesPath) | |
| 576 | ; atom_concat(Prefix, '.tla', FullExamplesPath) | |
| 577 | ), | |
| 578 | findall(BenchPath, (b_is_operation_name(OpName), | |
| 579 | atom_concat(Prefix, '_inductive_inv_', Path1), | |
| 580 | atom_concat(Path1, OpName, Path2), | |
| 581 | atom_concat(Path2, '.eval', BenchPath)), | |
| 582 | BenchPaths), | |
| 583 | retractall(cdclt_sat_solver:incremental_mode), | |
| 584 | benchmark_constraints(UseIdlSolver, BenchPaths, [], Data), | |
| 585 | retractall(cdclt_sat_solver:memoize_backjump_clause(_, _, _)), | |
| 586 | eval_benchmark_data_csv('../cbc_benchmarks/results/inductive_invariant_checking/', FileName, 'Additional CBC benchmarks', Data). | |
| 587 | run_additional_inductive_inv_benchmark(_, _). | |
| 588 | ||
| 589 | get_filename_from_path(MachinePath, FileName) :- | |
| 590 | atomic_list_concat(MachinePath, '/', Split), | |
| 591 | last(Split, FileNameExt), | |
| 592 | atomic_list_concat(FileNameExt, '.', Split2), | |
| 593 | Split2 = [FileName|_]. | |
| 594 | ||
| 595 | run_additional_deadlock_benchmarks(UseIdlSolver) :- | |
| 596 | findall(ExamplesPath, additional_deadlock_benchmark_model(_, ExamplesPath), ExamplesPaths), | |
| 597 | run_additional_deadlock_benchmarks(UseIdlSolver, ExamplesPaths). | |
| 598 | ||
| 599 | run_additional_deadlock_benchmarks(_, []). | |
| 600 | run_additional_deadlock_benchmarks(UseIdlSolver, [ExamplesPath|T]) :- | |
| 601 | run_additional_deadlock_benchmark(UseIdlSolver, ExamplesPath), | |
| 602 | run_additional_deadlock_benchmarks(UseIdlSolver, T). | |
| 603 | ||
| 604 | run_additional_deadlock_benchmark(UseIdlSolver, ExamplesPath) :- | |
| 605 | atom_concat('../cbc_benchmarks/deadlock_checking/', ExamplesPath, FullExamplesPath), | |
| 606 | atom_concat('../prob_examples/', ExamplesPath, MachinePath), | |
| 607 | load_b_eventb_or_tla(MachinePath), | |
| 608 | get_filename_from_path(MachinePath, FileName), | |
| 609 | atom_concat('../cbc_benchmarks/results/deadlock_checking/', FileName, TempPath), | |
| 610 | atom_concat(TempPath, '_results.csv', ResultPath), | |
| 611 | \+ file_exists(ResultPath), | |
| 612 | !, % don't run benchmark if result already exists | |
| 613 | ( atom_concat(Prefix, '.eventb', FullExamplesPath) | |
| 614 | ; atom_concat(Prefix, '.mch', FullExamplesPath) | |
| 615 | ; atom_concat(Prefix, '.tla', FullExamplesPath) | |
| 616 | ), | |
| 617 | atom_concat(Prefix, '_deadlock_freedom.eval', Path1), | |
| 618 | retractall(cdclt_sat_solver:incremental_mode), | |
| 619 | benchmark_constraints(UseIdlSolver, [Path1], [], Data), | |
| 620 | retractall(cdclt_sat_solver:memoize_backjump_clause(_, _, _)), | |
| 621 | eval_benchmark_data_csv('../cbc_benchmarks/results/deadlock_checking/', FileName, 'Additional BMC benchmarks', Data). | |
| 622 | run_additional_deadlock_benchmark(_, _). | |
| 623 | ||
| 624 | select_machine_file_path(FilePaths, MachineFilePath, BenchmarkFilePaths) :- | |
| 625 | select(_-MachineFilePath, FilePaths, BenchmarkFilePaths), | |
| 626 | ( atom_concat(_, '.eventb', MachineFilePath) | |
| 627 | ; atom_concat(_, '.mch', MachineFilePath) | |
| 628 | ; atom_concat(_, '.tla', MachineFilePath) | |
| 629 | ). | |
| 630 | ||
| 631 | load_b_eventb_or_tla(MachineFilePath) :- | |
| 632 | ( is_eventb_machine(MachineFilePath) | |
| 633 | -> b_load_eventb_project(MachineFilePath) | |
| 634 | ; is_tla_file(MachineFilePath) | |
| 635 | -> call_tla2b_parser(MachineFilePath), | |
| 636 | atom_concat(PrefixPath, '.tla', MachineFilePath), | |
| 637 | atom_concat(PrefixPath, '.prob', BMachinePath), | |
| 638 | b_load_machine_probfile(BMachinePath) | |
| 639 | ; b_load_machine_from_file(MachineFilePath) | |
| 640 | ), | |
| 641 | b_machine_precompile. | |
| 642 | ||
| 643 | amount_of_sat_vars(BenchmarkName, FolderPath, Acc, NewAcc) :- | |
| 644 | write('Eval amount of sat variables for '), write(FolderPath), nl, | |
| 645 | directory_exists(FolderPath), | |
| 646 | file_members_of_directory(FolderPath, FilePaths), | |
| 647 | select_machine_file_path(FilePaths, MachineFilePath, TBenchmarkFilePaths), | |
| 648 | findall(FilePath, (member(_-FilePath, TBenchmarkFilePaths), atom_concat(_, '.eval', FilePath)), BenchmarkFilePaths), | |
| 649 | load_b_eventb_or_tla(MachineFilePath), | |
| 650 | amount_of_sat_vars_for_benchmark(BenchmarkFilePaths, AmountOfSatVars), | |
| 651 | append(Acc, AmountOfSatVars, NewAcc), | |
| 652 | eval_amount_of_sat_vars(BenchmarkName, AmountOfSatVars). | |
| 653 | ||
| 654 | mean_of_list([], M) :- | |
| 655 | !, | |
| 656 | M = 0. | |
| 657 | mean_of_list(L, M) :- | |
| 658 | length(L, Len), | |
| 659 | sumlist(L, Sum), | |
| 660 | M is Sum / Len. | |
| 661 | ||
| 662 | median_of_list(L, M) :- | |
| 663 | length(L, Len), | |
| 664 | sort(L, LS), | |
| 665 | ( LS = [E] | |
| 666 | -> M = E | |
| 667 | ; Len21 is floor(Len / 2), | |
| 668 | Len22 is ceiling(Len / 2), | |
| 669 | ( Len21 \== Len22 | |
| 670 | -> nth1(Len22, L, M) | |
| 671 | ; nth1(Len21, L, M1), | |
| 672 | Len211 is Len21 + 1, | |
| 673 | nth1(Len211, L, M2), | |
| 674 | M is (M1+M2)/2 | |
| 675 | ) | |
| 676 | ). | |
| 677 | ||
| 678 | eval_amount_of_sat_vars(BenchmarkName, AmountOfSatVars) :- | |
| 679 | bmachine:b_machine_name(MachineName), | |
| 680 | atom_concat(MachineName, 'amount_of_sat_vars.txt', OutPath1), | |
| 681 | atom_concat('amount_of_sat_vars_', BenchmarkName, OutFolder1), | |
| 682 | atom_concat(OutFolder1, '/', OutFolder), | |
| 683 | atom_concat(OutFolder, OutPath1, OutPath), | |
| 684 | mean_of_list(AmountOfSatVars, MeanAmountOfSatVars), | |
| 685 | median_of_list(AmountOfSatVars, MedianAmountOfSatVars), | |
| 686 | open(OutPath, write, Stream), | |
| 687 | tell(Stream), | |
| 688 | format("AmountOfSatVarsList: ~w~nMean: ~w~nMedian: ~w~n", [AmountOfSatVars, MeanAmountOfSatVars, MedianAmountOfSatVars]), | |
| 689 | close(Stream). | |
| 690 | ||
| 691 | amount_of_sat_vars_for_benchmark([], []). | |
| 692 | amount_of_sat_vars_for_benchmark([BenchmarkFilePath|T], [AmountOfSatVars|TAmountOfSatVars]) :- | |
| 693 | safe_read_string_from_file(BenchmarkFilePath, utf8, Codes), | |
| 694 | parse_formula(Codes, UntypedAst), | |
| 695 | type_check_in_machine_context([UntypedAst], [Constraint]), | |
| 696 | cdclt_solver:get_amount_of_sat_variables(Constraint, AmountOfSatVars), | |
| 697 | amount_of_sat_vars_for_benchmark(T, TAmountOfSatVars). | |
| 698 | ||
| 699 | run_cbc_benchmarks(UseIdlSolver, FolderPath) :- | |
| 700 | directory_exists(FolderPath), | |
| 701 | file_members_of_directory(FolderPath, FilePaths), | |
| 702 | select_machine_file_path(FilePaths, MachineFilePath, TBenchmarkFilePaths), | |
| 703 | findall(FileName-FilePath, (member(FileName-FilePath, TBenchmarkFilePaths), atom_concat(_, '.eval', FilePath)), BenchmarkFilePaths), | |
| 704 | load_b_eventb_or_tla(MachineFilePath), | |
| 705 | run_cbc_benchmarks(UseIdlSolver, FolderPath, BenchmarkFilePaths). | |
| 706 | ||
| 707 | run_cbc_benchmarks(_, _, []). | |
| 708 | run_cbc_benchmarks(UseIdlSolver, FolderPath, [FileName-BenchmarkFilePath|T]) :- | |
| 709 | safe_read_string_from_file(BenchmarkFilePath, utf8, Codes), | |
| 710 | parse_formula(Codes, UntypedAst), | |
| 711 | type_check_in_machine_context([UntypedAst], [Constraint]), | |
| 712 | retractall(cdclt_sat_solver:incremental_mode), | |
| 713 | run_cbc_benchmark(UseIdlSolver, FolderPath, FileName-BenchmarkFilePath, Constraint), | |
| 714 | run_cbc_benchmarks(UseIdlSolver, FolderPath, T). | |
| 715 | ||
| 716 | % only z3 par and no chr or cse for prob; old version from the journal article | |
| 717 | run_cbc_benchmark(UseIdlSolver, FolderPath, FileName-BenchmarkFilePath, Constraint) :- | |
| 718 | inductive_inv_timeout(Timeout), | |
| 719 | preferences:set_preference(time_out, Timeout), | |
| 720 | set_preference(cdclt_use_idl_theory_solver, false), | |
| 721 | set_preference(cdclt_perform_static_analysis, false), | |
| 722 | set_preference(cdclt_perform_symmetry_breaking, true), | |
| 723 | cdclt_solver:init, | |
| 724 | write('Solve with Sym-Raw-SMT..'),nl, | |
| 725 | writeq(BenchmarkFilePath),nl, | |
| 726 | statistics(walltime, [StartCdcltRawSym|_]), | |
| 727 | cdclt_solve_predicate(Constraint, _, ResCdcltRawSym), | |
| 728 | statistics(walltime, [StopCdcltRawSym|_]), | |
| 729 | (cdclt_sat_solver:restarts(RestartsCdcltRawSym); RestartsCdcltRawSym = 0), | |
| 730 | TimeCdcltRawSym is StopCdcltRawSym - StartCdcltRawSym, | |
| 731 | nl,nl,write(ResCdcltRawSym),nl,nl, | |
| 732 | %% | |
| 733 | write('done.'), nl, | |
| 734 | set_preference(cdclt_perform_static_analysis, true), | |
| 735 | cdclt_solver:init, | |
| 736 | write('Solve with Sym-SMT..'),nl, | |
| 737 | writeq(BenchmarkFilePath),nl, | |
| 738 | statistics(walltime, [StartCdclt|_]), | |
| 739 | cdclt_solve_predicate(Constraint, _, ResCdclt), | |
| 740 | statistics(walltime, [StopCdclt|_]), | |
| 741 | (cdclt_sat_solver:restarts(RestartsCdclt); RestartsCdclt = 0), | |
| 742 | TimeCdclt is StopCdclt - StartCdclt, | |
| 743 | nl,nl,write(ResCdclt),nl,nl, | |
| 744 | %% | |
| 745 | write('done.'), nl, | |
| 746 | preferences:set_preference(time_out, Timeout), | |
| 747 | ( UseIdlSolver | |
| 748 | -> set_preference(cdclt_perform_symmetry_breaking,false), | |
| 749 | set_preference(cdclt_use_idl_theory_solver,true), | |
| 750 | cdclt_solver:init, | |
| 751 | write('Solve with IDL-SMT..'),nl, | |
| 752 | writeq(BenchmarkFilePath),nl, | |
| 753 | statistics(walltime, [StartCdcltIdl|_]), | |
| 754 | cdclt_solve_predicate(Constraint, _, ResCdcltIdl), | |
| 755 | statistics(walltime, [StopCdcltIdl|_]), | |
| 756 | (cdclt_sat_solver:restarts(RestartsCdcltIdl); RestartsCdcltIdl = 0), | |
| 757 | TimeCdcltIdl is StopCdcltIdl - StartCdcltIdl, | |
| 758 | set_preference(cdclt_use_idl_theory_solver,false), | |
| 759 | set_preference(cdclt_perform_symmetry_breaking,true) | |
| 760 | ; TimeCdcltIdl = 0, | |
| 761 | RestartsCdcltIdl = 0, | |
| 762 | ResCdcltIdl = none | |
| 763 | ), | |
| 764 | nl,nl,write(ResCdcltIdl),nl,nl, | |
| 765 | write('done.'), nl, | |
| 766 | %% | |
| 767 | preferences:set_preference(time_out, Timeout), | |
| 768 | set_preference(cdclt_perform_symmetry_breaking,false), | |
| 769 | cdclt_solver:init, | |
| 770 | write('Solve with SMT..'),nl, | |
| 771 | writeq(BenchmarkFilePath),nl, | |
| 772 | statistics(walltime, [StartCdcltNoSym|_]), | |
| 773 | cdclt_solve_predicate(Constraint, _, ResCdcltNoSym), | |
| 774 | statistics(walltime, [StopCdcltNoSym|_]), | |
| 775 | (cdclt_sat_solver:restarts(RestartsCdcltNoSym); RestartsCdcltNoSym = 0), | |
| 776 | TimeCdcltNoSym is StopCdcltNoSym - StartCdcltNoSym, | |
| 777 | nl,nl,write(ResCdcltNoSym),nl,nl, | |
| 778 | write('done.'), nl, | |
| 779 | preferences:set_preference(time_out, Timeout), | |
| 780 | %% | |
| 781 | set_preference(cdclt_perform_static_analysis,false), | |
| 782 | set_preference(cdclt_perform_symmetry_breaking,false), | |
| 783 | cdclt_solver:init, | |
| 784 | write('Solve with Raw-SMT..'),nl, | |
| 785 | writeq(BenchmarkFilePath),nl, | |
| 786 | statistics(walltime, [StartCdcltRaw|_]), | |
| 787 | cdclt_solve_predicate(Constraint, _, ResCdcltRaw), | |
| 788 | statistics(walltime, [StopCdcltRaw|_]), | |
| 789 | (cdclt_sat_solver:restarts(RestartsCdcltRaw); RestartsCdcltRaw = 0), | |
| 790 | TimeCdcltRaw is StopCdcltRaw - StartCdcltRaw, | |
| 791 | nl,nl,write(ResCdcltRaw),nl,nl, | |
| 792 | write('done.'), nl, | |
| 793 | preferences:set_preference(time_out, Timeout), | |
| 794 | %% | |
| 795 | write('Solve with Z3..'),nl, | |
| 796 | writeq(BenchmarkFilePath),nl, | |
| 797 | %translate:print_bexpr(Constraint),nl, | |
| 798 | statistics(walltime, [StartZ3|_]), | |
| 799 | smt_solve_predicate(z3,Constraint, _, ResZ3), | |
| 800 | %ResZ3 = no_solution_found(solver_answered_unknown), | |
| 801 | statistics(walltime, [StopZ3|_]), | |
| 802 | TimeZ3 is StopZ3 - StartZ3, | |
| 803 | nl,nl,write(ResZ3),nl,nl, | |
| 804 | preferences:set_preference(time_out, Timeout), | |
| 805 | %% | |
| 806 | write('Solve with ProB..'),nl, | |
| 807 | writeq(BenchmarkFilePath),nl, | |
| 808 | statistics(walltime, [StartProB|_]), | |
| 809 | solve_predicate(Constraint, _, 1, [use_smt_mode/true,use_clpfd_solver/true,clean_up_pred,allow_improving_wd_mode/true], ResProB), | |
| 810 | %ResProB = no_solution_found(solver_answered_unknown), | |
| 811 | statistics(walltime, [StopProB|_]), | |
| 812 | TimeProB is StopProB - StartProB, | |
| 813 | nl,nl,write(ResProB),nl,nl, | |
| 814 | write('done.'), nl, | |
| 815 | !, | |
| 816 | 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). | |
| 817 | ||
| 818 | 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) :- | |
| 819 | atom_concat(FileNameNoExt, '.eval', FileName), | |
| 820 | atom_concat('benchmark_cbc_results_', FileNameNoExt, TResultsPath), | |
| 821 | atom_concat(TResultsPath, '.csv', TTResultsPath), | |
| 822 | atom_concat(FolderPath, TTResultsPath, ResultsPath), | |
| 823 | open(ResultsPath, write, Stream), | |
| 824 | tell(Stream), | |
| 825 | format("ConstraintPath,Solver,Result,Time (ms),Restarts~n", []), | |
| 826 | format("~w,~w,~w,~w,~w~n", [BenchmarkFilePath,prob,ResProB,TimeProB,-1]), | |
| 827 | format("~w,~w,~w,~w,~w~n", [BenchmarkFilePath,z3par,ResZ3,TimeZ3,-1]), | |
| 828 | format("~w,~w,~w,~w,~w~n", [BenchmarkFilePath,sym_smt,ResCdclt,TimeCdclt,RestartsCdclt]), | |
| 829 | format("~w,~w,~w,~w,~w~n", [BenchmarkFilePath,smt,ResCdcltNoSym,TimeCdcltNoSym,RestartsCdcltNoSym]), | |
| 830 | format("~w,~w,~w,~w,~w~n", [BenchmarkFilePath,smt_idl,ResCdcltIdl,TimeCdcltIdl,RestartsCdcltIdl]), | |
| 831 | format("~w,~w,~w,~w,~w~n", [BenchmarkFilePath,raw_smt,ResCdcltRaw,TimeCdcltRaw,RestartsCdcltRaw]), | |
| 832 | format("~w,~w,~w,~w,~w~n", [BenchmarkFilePath,sym_raw_smt,ResCdcltRawSym,TimeCdcltRawSym,RestartsCdcltRawSym]), | |
| 833 | close(Stream), | |
| 834 | !. | |
| 835 | ||
| 836 | int_range(C, B, R) :- | |
| 837 | C == B, | |
| 838 | !, | |
| 839 | R = [C]. | |
| 840 | int_range(C, B, [C|T]) :- | |
| 841 | C1 is C + 1, | |
| 842 | int_range(C1, B, T). | |
| 843 | ||
| 844 | get_file_paths_from_config(ConfigPath, MachineFile, ConstraintPaths, Description, MachineName) :- | |
| 845 | open(ConfigPath, read, Stream), | |
| 846 | read(Stream, Config), | |
| 847 | close(Stream), | |
| 848 | Config = benchmark_config(Description, MachineFile, MachineName, MaxBound), | |
| 849 | int_range(0, MaxBound, KRange), | |
| 850 | findall(ConstraintPath, | |
| 851 | (member(K, KRange), atom_concat(MachineName, '_monolithic_bmc_k_', T1), | |
| 852 | number_codes(K, CK), atom_codes(AK, CK), | |
| 853 | atom_concat(T1, AK, T2), atom_concat(T2, '.eval', ConstraintPath)), | |
| 854 | ConstraintPaths). | |
| 855 | ||
| 856 | is_eventb_machine(MachineFile) :- | |
| 857 | atom_concat(_, '.eventb', MachineFile). | |
| 858 | ||
| 859 | is_tla_file(File) :- | |
| 860 | atom_concat(_, '.tla', File). | |
| 861 | ||
| 862 | start_csv_stream(OutputPath, MachineName, Stream) :- | |
| 863 | atom_concat(OutputPath, MachineName, TempPath), | |
| 864 | atom_concat(TempPath, '_results.csv', EvalFilePath), | |
| 865 | nl,nl,write('csv'),nl, | |
| 866 | write(EvalFilePath),nl,nl, | |
| 867 | open(EvalFilePath, write, Stream), | |
| 868 | write(Stream, 'ConstraintPath,Solver,Result,Time (ms)'), nl(Stream). | |
| 869 | ||
| 870 | start_csv_stream_symmetry(OutputPath, MachineName, Stream) :- | |
| 871 | atom_concat(OutputPath, MachineName, TempPath), | |
| 872 | atom_concat(TempPath, '_sym_preds.csv', EvalFilePath), | |
| 873 | nl,nl,write('csv'),nl, | |
| 874 | write(EvalFilePath),nl,nl, | |
| 875 | open(EvalFilePath, write, Stream), | |
| 876 | write(Stream, 'ConstraintPath,Solver,SBPs'), nl(Stream). | |
| 877 | ||
| 878 | write_to_csv_stream(_, _, []). | |
| 879 | write_to_csv_stream(SolverName, Stream, [(ConstraintPath,Time)|T]) :- | |
| 880 | ( benchmark_result(SolverName, ConstraintPath, Result) | |
| 881 | -> true | |
| 882 | ; Result = not_evaluated | |
| 883 | ), | |
| 884 | prepare_result(Result, PResult), | |
| 885 | format("~w,~w,~w,~w~n", [ConstraintPath,SolverName,PResult,Time]), | |
| 886 | write_to_csv_stream(SolverName, Stream, T). | |
| 887 | ||
| 888 | %write_to_symmetry_csv_stream([]). | |
| 889 | %write_to_symmetry_csv_stream([(ConstraintPath,SolverName,SBPs)|T]) :- | |
| 890 | % format("~w,~w,~w~n", [ConstraintPath,SolverName,SBPs]), | |
| 891 | % write_to_symmetry_csv_stream(T). | |
| 892 | ||
| 893 | prepare_result(solution(_), Out) :- | |
| 894 | !, | |
| 895 | Out = solution. | |
| 896 | prepare_result(no_solution_found(enumeration_warning(_,_,_,_,_)), Out) :- | |
| 897 | !, | |
| 898 | Out = no_solution_found(enumeration_warning). | |
| 899 | prepare_result(Res, Res). | |
| 900 | ||
| 901 | eval_benchmark_data_csv(OutputPath, MachineName, Description, Data) :- | |
| 902 | format("Evaluate benchmarks ~w for detailed CSV~n", [Description]), | |
| 903 | findall((ConstraintPath,TimeZ3Par), member((ConstraintPath,TimeZ3Par,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_), Data), DataZ3Par), | |
| 904 | findall((ConstraintPath,TimeZ3Axm), member((ConstraintPath,_,TimeZ3Axm,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_), Data), DataZ3Axm), | |
| 905 | findall((ConstraintPath,TimeZ3Cns), member((ConstraintPath,_,_,TimeZ3Cns,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_), Data), DataZ3Cns), | |
| 906 | findall((ConstraintPath,TimeZ3Dec), member((ConstraintPath,_,_,_,TimeZ3Dec,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_), Data), DataZ3Dec), | |
| 907 | findall((ConstraintPath,TimeCdclt), member((ConstraintPath,_,_,_,_,TimeCdclt,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_), Data), DataCdclt), | |
| 908 | findall((ConstraintPath,TimeCdcltRaw), member((ConstraintPath,_,_,_,_,_,TimeCdcltRaw,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_), Data), DataCdcltRaw), | |
| 909 | findall((ConstraintPath,TimeCdcltIdl), member((ConstraintPath,_,_,_,_,_,_,TimeCdcltIdl,_,_,_,_,_,_,_,_,_,_,_,_,_,_), Data), DataCdcltIdl), | |
| 910 | findall((ConstraintPath,TimeCdcltNoSym), member((ConstraintPath,_,_,_,_,_,_,_,TimeCdcltNoSym,_,_,_,_,_,_,_,_,_,_,_,_,_), Data), DataCdcltNoSym), | |
| 911 | findall((ConstraintPath,TimeCdcltRawSym), member((ConstraintPath,_,_,_,_,_,_,_,_,TimeCdcltRawSym,_,_,_,_,_,_,_,_,_,_,_,_), Data), DataCdcltRawSym), | |
| 912 | findall((ConstraintPath,TimeProBComp), member((ConstraintPath,_,_,_,_,_,_,_,_,_,TimeProBComp,_,_,_,_,_,_,_,_,_,_), Data), DataProBComp), | |
| 913 | findall((ConstraintPath,TimeProBSym), member((ConstraintPath,_,_,_,_,_,_,_,_,_,_,TimeProBSym,_,_,_,_,_,_,_,_,_,_), Data), DataProBSym), | |
| 914 | findall((ConstraintPath,TimeProB), member((ConstraintPath,_,_,_,_,_,_,_,_,_,_,_,TimeProB,_,_,_,_,_,_,_,_,_), Data), DataProB), | |
| 915 | findall((ConstraintPath,TimeProBChr), member((ConstraintPath,_,_,_,_,_,_,_,_,_,_,_,_,TimeProBChr,_,_,_,_,_,_,_,_), Data), DataProBChr), | |
| 916 | findall((ConstraintPath,TimeProBCse), member((ConstraintPath,_,_,_,_,_,_,_,_,_,_,_,_,_,TimeProBCse,_,_,_,_,_,_,_), Data), DataProBCse), | |
| 917 | findall((ConstraintPath,TimeSetlog), member((ConstraintPath,_,_,_,_,_,_,_,_,_,_,_,_,_,_,TimeSetlog,_,_,_,_,_,_), Data), DataSetlog), | |
| 918 | findall((ConstraintPath,TimeProBProver), member((ConstraintPath,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,TimeProBProver,_,_,_,_,_), Data), DataProBProver), | |
| 919 | start_csv_stream(OutputPath, MachineName, Stream), | |
| 920 | tell(Stream), | |
| 921 | write_to_csv_stream(z3par, MachineName, DataZ3Par), | |
| 922 | write_to_csv_stream(z3axm, MachineName, DataZ3Axm), | |
| 923 | write_to_csv_stream(z3cns, MachineName, DataZ3Cns), | |
| 924 | write_to_csv_stream(z3dec, MachineName, DataZ3Dec), | |
| 925 | write_to_csv_stream(smt, MachineName, DataCdcltNoSym), | |
| 926 | write_to_csv_stream(sym_smt, MachineName, DataCdclt), | |
| 927 | write_to_csv_stream(raw_smt, MachineName, DataCdcltRaw), | |
| 928 | write_to_csv_stream(idl_smt, MachineName, DataCdcltIdl), | |
| 929 | write_to_csv_stream(sym_raw_smt, MachineName, DataCdcltRawSym), | |
| 930 | write_to_csv_stream(prob_comp, MachineName, DataProBComp), | |
| 931 | write_to_csv_stream(prob_sym, MachineName, DataProBSym), | |
| 932 | write_to_csv_stream(prob, MachineName, DataProB), | |
| 933 | write_to_csv_stream(prob_chr, MachineName, DataProBChr), | |
| 934 | write_to_csv_stream(prob_cse, MachineName, DataProBCse), | |
| 935 | write_to_csv_stream(setlog, MachineName, DataSetlog), | |
| 936 | write_to_csv_stream(prob_prover, MachineName, DataProBProver), | |
| 937 | close(Stream). | |
| 938 | /*start_csv_stream_symmetry(OutputPath, MachineName, SymStream), | |
| 939 | findall((ConstraintPath,Solver,SBPs), symmetry_breaking_predicates(ConstraintPath,Solver,SBPs), SBPs), | |
| 940 | tell(SymStream), | |
| 941 | write_to_symmetry_csv_stream(SBPs), | |
| 942 | retractall(symmetry_breaking_predicates(_,_,_)), | |
| 943 | close(SymStream).*/ | |
| 944 | ||
| 945 | /*eval_benchmark_data(MachineName, Description, Data) :- | |
| 946 | format("Evaluate benchmarks ~w~n", [Description]), | |
| 947 | findall(TimeZ3, member((_,TimeZ3,_,_,_,_,_,_,_,_,_,_), Data), TimesZ3), | |
| 948 | findall(TimeCdclt, member((_,_,TimeCdclt,_,_,_,_,_,_,_,_,_), Data), TimesCdclt), | |
| 949 | findall(TimeCdcltRaw, member((_,_,_,TimeCdcltRaw,_,_,_,_,_,_,_,_,_), Data), TimesCdcltRaw), | |
| 950 | findall(TimeCdcltIdl, member((_,_,_,_,TimeCdcltIdl,_,_,_,_,_,_,_,_), Data), TimesCdcltIdl), | |
| 951 | findall(TimeCdcltNoSym, member((_,_,_,_,_,TimeCdcltNoSym,_,_,_,_,_,_,_), Data), TimesCdcltNoSym), | |
| 952 | findall(TimeCdcltRawSym, member((_,_,_,_,_,_,TimeCdcltRawSym,_,_,_,_,_,_), Data), TimesCdcltRawSym), | |
| 953 | findall(TimeProB, member((_,_,_,_,_,_,_,TimeProB,_,_,_,_,_), Data), TimesProB), | |
| 954 | findall(RestartCdclt, member((_,_,_,_,_,_,_,_,RestartCdclt,_,_,_,_), Data), RestartsCdclt), | |
| 955 | findall(RestartCdcltRaw, member((_,_,_,_,_,_,_,_,_,RestartCdcltRaw,_,_), Data), RestartsCdcltRaw), | |
| 956 | findall(RestartCdcltIdl, member((_,_,_,_,_,_,_,_,_,_,RestartCdcltIdl,_,_), Data), RestartsCdcltIdl), | |
| 957 | findall(RestartCdcltNoSym, member((_,_,_,_,_,_,_,_,_,_,_,RestartCdcltNoSym,_), Data), RestartsCdcltNoSym), | |
| 958 | findall(RestartCdcltRawSym, member((_,_,_,_,_,_,_,_,_,_,_,_,RestartCdcltRawSym), Data), RestartsCdcltRawSym), | |
| 959 | sumlist(TimesZ3, TimeZ3), | |
| 960 | sumlist(TimesCdclt, TimeCdclt), | |
| 961 | sumlist(TimesCdcltRaw, TimeCdcltRaw), | |
| 962 | sumlist(TimesCdcltIdl, TimeCdcltIdl), | |
| 963 | sumlist(TimesCdcltNoSym, TimeCdcltNoSym), | |
| 964 | sumlist(TimesCdcltRawSym, TimeCdcltRawSym), | |
| 965 | sumlist(TimesProB, TimeProB), | |
| 966 | sumlist(RestartsCdclt, RestartCdclt), | |
| 967 | sumlist(RestartsCdcltRaw, RestartCdcltRaw), | |
| 968 | sumlist(RestartsCdcltIdl, RestartCdcltIdl), | |
| 969 | sumlist(RestartsCdcltNoSym, RestartCdcltNoSym), | |
| 970 | sumlist(RestartsCdcltRawSym, RestartCdcltRawSym), | |
| 971 | atom_concat('benchmarks_cdclt_journal/', MachineName, Path1), | |
| 972 | atom_concat(Path1, '_results.txt', EvalFilePath), | |
| 973 | nl,nl,write('eval'),nl, | |
| 974 | write(EvalFilePath),nl,nl, | |
| 975 | open(EvalFilePath, write, Stream), | |
| 976 | tell(Stream), | |
| 977 | format("Time Sym-Raw-SMT: ~w~nRestart Sym-Raw-SMT: ~w~nTime Z3: ~w~nTime Sym-SMT: ~w~nRestart Sym-SMT: ~w~nTime Idl-SMT: ~w~nRestart Idl-SMT: ~w~nTime SMT: ~w~nRestart SMT: ~w~nTime Raw-SMT: ~w~nRestart Raw-SMT: ~w~nTime ProB: ~w~n~n", [TimeCdcltRawSym,RestartsCdcltRawSym,TimeZ3,TimeCdclt,RestartCdclt,TimeCdcltIdl,RestartCdcltIdl,TimeCdcltNoSym,RestartCdcltNoSym,TimeCdcltRaw,RestartCdcltRaw,TimeProB]), | |
| 978 | findall(TO, (solved_constraints(A,B), TO = solved_constraints(A,B)), TOs), | |
| 979 | (member(solved_constraints(prob,SolvedProB), TOs); SolvedProB = 0), | |
| 980 | (member(solved_constraints(z3,SolvedZ3), TOs); SolvedZ3 = 0), | |
| 981 | (member(solved_constraints(smt,SolvedSMT), TOs); SolvedSMT = 0), | |
| 982 | (member(solved_constraints(raw_smt,SolvedRawSMT), TOs); SolvedRawSMT = 0), | |
| 983 | (member(solved_constraints(sym_smt,SolvedSymSMT), TOs); SolvedSymSMT = 0), | |
| 984 | (member(solved_constraints(sym_raw_smt,SolvedSymRawSMT), TOs); SolvedSymRawSMT = 0), | |
| 985 | format("~w / ~w & ~w / ~w & ~w / ~w & ~w / ~w & ~w / ~w & ~w / ~w~n", [SolvedProB,TimeProB,SolvedZ3,TimeZ3,SolvedSMT,TimeCdcltNoSym,SolvedRawSMT,TimeCdcltRaw,SolvedSymSMT,TimeCdclt,SolvedSymRawSMT,TimeCdcltRawSym]), | |
| 986 | nl, write(TOs), nl, | |
| 987 | close(Stream).*/ | |
| 988 | ||
| 989 | run_bmc_benchmarks(UseIdlSolver, DirPath) :- | |
| 990 | retractall(solved_constraints(_,_)), | |
| 991 | retractall(benchmark_result(_,_,_)), | |
| 992 | atom_concat(DirPath, 'benchmark_config.pl', ConfigPath), | |
| 993 | get_file_paths_from_config(ConfigPath, MachineFile, ConstraintPaths, Description, MachineName), | |
| 994 | format("Run benchmarks ~w~n", [Description]), | |
| 995 | atom_concat(DirPath, MachineFile, MachinePath), | |
| 996 | load_b_eventb_or_tla(MachinePath), | |
| 997 | maplist(atom_concat(DirPath), ConstraintPaths, FullConstraintPaths), | |
| 998 | retractall(cdclt_sat_solver:incremental_mode), | |
| 999 | benchmark_constraints(UseIdlSolver, FullConstraintPaths, [], Data), | |
| 1000 | retractall(cdclt_sat_solver:memoize_backjump_clause(_, _, _)), | |
| 1001 | %eval_benchmark_data(MachineName, Description, Data), | |
| 1002 | eval_benchmark_data_csv('benchmark_results_smt/', MachineName, Description, Data). | |
| 1003 | ||
| 1004 | benchmark_constraints(_, [], Acc, Acc). | |
| 1005 | benchmark_constraints(UseIdlSolver, [ConstraintPath|T], Acc, Data) :- | |
| 1006 | 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), !, | |
| 1007 | !, | |
| 1008 | 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). | |
| 1009 | benchmark_constraints(UseIdlSolver, [_|T], Acc, Data) :- | |
| 1010 | format("Skipped constraints due to error~n", []), | |
| 1011 | benchmark_constraints(UseIdlSolver, T, Acc, Data). | |
| 1012 | ||
| 1013 | 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) :- | |
| 1014 | bmc_timeout(Timeout), | |
| 1015 | write(ConstraintPath),nl, | |
| 1016 | safe_read_string_from_file(ConstraintPath, utf8, Codes), | |
| 1017 | parse_formula(Codes, UntypedAst), | |
| 1018 | type_check_in_machine_context([UntypedAst], [Constraint]), | |
| 1019 | preferences:set_preference(time_out, 2500), % dummy call for clp(fd) jit | |
| 1020 | solve_predicate(Constraint, _, 1, [use_smt_mode/true,use_clpfd_solver/true,use_chr_solver/false,clean_up_pred,allow_improving_wd_mode/true], _), | |
| 1021 | %translate:print_bexpr(Constraint),nl, | |
| 1022 | preferences:set_preference(time_out, Timeout), | |
| 1023 | write('Solve with Setlog..'),nl, | |
| 1024 | write(ConstraintPath),nl, | |
| 1025 | error_manager:reset_errors, | |
| 1026 | statistics(walltime, [StartSetlog|_]), | |
| 1027 | solve_pred_with_setlog(Constraint, _, ResSetlog), | |
| 1028 | statistics(walltime, [StopSetlog|_]), | |
| 1029 | TimeSetlog is StopSetlog - StartSetlog, | |
| 1030 | ( solved_constraint(ResSetlog) | |
| 1031 | -> inc_solved_counter(setlog) | |
| 1032 | ; true | |
| 1033 | ), | |
| 1034 | add_benchmark_result(setlog, ConstraintPath, ResSetlog), | |
| 1035 | nl,nl,write(ResSetlog),nl,nl, | |
| 1036 | write('done.'), nl, | |
| 1037 | preferences:set_preference(time_out, Timeout), | |
| 1038 | write('Solve with ProB Prover..'),nl, | |
| 1039 | write(ConstraintPath),nl, | |
| 1040 | error_manager:reset_errors, | |
| 1041 | statistics(walltime, [StartProBProver|_]), | |
| 1042 | ( prove_sequent(Constraint) | |
| 1043 | -> ResProBProver = solution([]) | |
| 1044 | ; ResProBProver = contradiction_found | |
| 1045 | ), | |
| 1046 | statistics(walltime, [StopProBProver|_]), | |
| 1047 | ( solved_constraint(ResProBProver) | |
| 1048 | -> inc_solved_counter(prob_prover) | |
| 1049 | ; true | |
| 1050 | ), | |
| 1051 | TimeProBProver is StopProBProver - StartProBProver, | |
| 1052 | add_benchmark_result(prob_prover, ConstraintPath, ResProBProver), | |
| 1053 | nl,nl,write(ResProBProver),nl,nl, | |
| 1054 | write('done.'), nl, | |
| 1055 | preferences:set_preference(time_out, Timeout), | |
| 1056 | set_preference(cdclt_use_idl_theory_solver, false), | |
| 1057 | set_preference(cdclt_perform_static_analysis, false), | |
| 1058 | set_preference(cdclt_perform_symmetry_breaking, true), | |
| 1059 | cdclt_solver:init, | |
| 1060 | write('Solve with Sym-Raw-SMT..'),nl, | |
| 1061 | write(ConstraintPath),nl, | |
| 1062 | error_manager:reset_errors, | |
| 1063 | statistics(walltime, [StartCdcltRawSym|_]), | |
| 1064 | cdclt_solve_predicate(sym_raw_smt, Constraint, _SolvedPred1, ResCdcltRawSym), | |
| 1065 | get_amount_of_found_sbps(SBPsRawSym), | |
| 1066 | asserta(symmetry_breaking_predicates(ConstraintPath,sym_raw_smt,SBPsRawSym)), | |
| 1067 | %ResCdcltRawSym = no_solution_found(solver_answered_unknown), | |
| 1068 | statistics(walltime, [StopCdcltRawSym|_]), | |
| 1069 | (cdclt_sat_solver:restarts(RestartsCdcltRawSym); RestartsCdcltRawSym = 0), | |
| 1070 | format("Restarts: ~w~n", [RestartsCdcltRawSym]), | |
| 1071 | TimeCdcltRawSym is StopCdcltRawSym - StartCdcltRawSym, | |
| 1072 | ( solved_constraint(ResCdcltRawSym) | |
| 1073 | -> inc_solved_counter(sym_raw_smt) | |
| 1074 | ; true | |
| 1075 | ), | |
| 1076 | add_benchmark_result(sym_raw_smt, ConstraintPath, ResCdcltRawSym), | |
| 1077 | !, | |
| 1078 | nl,nl,write(ResCdcltRawSym),nl,nl, | |
| 1079 | write('done.'), nl, | |
| 1080 | preferences:set_preference(time_out, Timeout), | |
| 1081 | set_preference(cdclt_perform_static_analysis, true), | |
| 1082 | cdclt_solver:init, | |
| 1083 | write('Solve with Sym-SMT..'),nl, | |
| 1084 | write(ConstraintPath),nl, | |
| 1085 | error_manager:reset_errors, | |
| 1086 | statistics(walltime, [StartCdclt|_]), | |
| 1087 | cdclt_solve_predicate(sym_smt, Constraint, _SolvedPred2, ResCdclt), | |
| 1088 | get_amount_of_found_sbps(SBPsSym), | |
| 1089 | asserta(symmetry_breaking_predicates(ConstraintPath,sym_smt,SBPsSym)), | |
| 1090 | %ResCdclt = no_solution_found(solver_answered_unknown), | |
| 1091 | statistics(walltime, [StopCdclt|_]), | |
| 1092 | (cdclt_sat_solver:restarts(RestartsCdclt); RestartsCdclt = 0), | |
| 1093 | format("Restarts: ~w~n", [RestartsCdclt]), | |
| 1094 | TimeCdclt is StopCdclt - StartCdclt, | |
| 1095 | ( solved_constraint(ResCdclt) | |
| 1096 | -> inc_solved_counter(sym_smt) | |
| 1097 | ; true | |
| 1098 | ), | |
| 1099 | add_benchmark_result(sym_smt, ConstraintPath, ResCdclt), | |
| 1100 | !, | |
| 1101 | nl,nl,write(ResCdclt),nl,nl, | |
| 1102 | write('done.'), nl, | |
| 1103 | preferences:set_preference(time_out, Timeout), | |
| 1104 | ( UseIdlSolver | |
| 1105 | -> set_preference(cdclt_perform_symmetry_breaking, false), | |
| 1106 | set_preference(cdclt_use_idl_theory_solver, true), | |
| 1107 | cdclt_solver:init, | |
| 1108 | preferences:set_preference(time_out, Timeout), | |
| 1109 | write('Solve with IDL-SMT..'),nl, | |
| 1110 | error_manager:reset_errors, | |
| 1111 | statistics(walltime, [StartCdcltIdl|_]), | |
| 1112 | cdclt_solve_predicate(idl_smt, Constraint, _SolvedPred3, ResCdcltIdl), | |
| 1113 | %ResCdcltIdl = no_solution_found(solver_answered_unknown), | |
| 1114 | statistics(walltime, [StopCdcltIdl|_]), | |
| 1115 | (cdclt_sat_solver:restarts(RestartsCdcltIdl); RestartsCdcltIdl = 0), | |
| 1116 | format("Restarts: ~w~n", [RestartsCdcltIdl]), | |
| 1117 | TimeCdcltIdl is StopCdcltIdl - StartCdcltIdl, | |
| 1118 | ( solved_constraint(ResCdcltIdl) | |
| 1119 | -> inc_solved_counter(idl_smt) | |
| 1120 | ; true | |
| 1121 | ), | |
| 1122 | add_benchmark_result(idl_smt, ConstraintPath, ResCdcltIdl), | |
| 1123 | !, | |
| 1124 | set_preference(cdclt_use_idl_theory_solver, false), | |
| 1125 | set_preference(cdclt_perform_symmetry_breaking, true) | |
| 1126 | ; TimeCdcltIdl = 0, | |
| 1127 | RestartsCdcltIdl = 0, | |
| 1128 | ResCdcltIdl = none | |
| 1129 | ), | |
| 1130 | nl,nl,write(ResCdcltIdl),nl,nl, | |
| 1131 | write('done.'), nl, | |
| 1132 | %% | |
| 1133 | preferences:set_preference(time_out, Timeout), | |
| 1134 | set_preference(cdclt_perform_symmetry_breaking, false), | |
| 1135 | cdclt_solver:init, | |
| 1136 | preferences:set_preference(time_out, Timeout), | |
| 1137 | write('Solve with SMT..'),nl, | |
| 1138 | write(ConstraintPath),nl, | |
| 1139 | error_manager:reset_errors, | |
| 1140 | statistics(walltime, [StartCdcltNoSym|_]), | |
| 1141 | cdclt_solve_predicate(smt, Constraint, _, ResCdcltNoSym), | |
| 1142 | %ResCdcltNoSym = no_solution_found(solver_answered_unknown), | |
| 1143 | statistics(walltime, [StopCdcltNoSym|_]), | |
| 1144 | (cdclt_sat_solver:restarts(RestartsCdcltNoSym); RestartsCdcltNoSym = 0), | |
| 1145 | format("Restarts: ~w~n", [RestartsCdcltNoSym]), | |
| 1146 | TimeCdcltNoSym is StopCdcltNoSym - StartCdcltNoSym, | |
| 1147 | ( solved_constraint(ResCdcltNoSym) | |
| 1148 | -> inc_solved_counter(smt) | |
| 1149 | ; true | |
| 1150 | ), | |
| 1151 | add_benchmark_result(smt, ConstraintPath, ResCdcltNoSym), | |
| 1152 | !, | |
| 1153 | nl,nl,write(ResCdcltNoSym),nl,nl, | |
| 1154 | write('done.'), nl, | |
| 1155 | preferences:set_preference(time_out, Timeout), | |
| 1156 | %% | |
| 1157 | set_preference(cdclt_perform_static_analysis, false), | |
| 1158 | set_preference(cdclt_perform_symmetry_breaking, false), | |
| 1159 | cdclt_solver:init, | |
| 1160 | preferences:set_preference(time_out, Timeout), | |
| 1161 | write('Solve with Raw-SMT..'),nl, | |
| 1162 | write(ConstraintPath),nl, | |
| 1163 | error_manager:reset_errors, | |
| 1164 | statistics(walltime, [StartCdcltRaw|_]), | |
| 1165 | cdclt_solve_predicate(raw_smt, Constraint, _, ResCdcltRaw), | |
| 1166 | %ResCdcltRaw = no_solution_found(solver_answered_unknown), | |
| 1167 | statistics(walltime, [StopCdcltRaw|_]), | |
| 1168 | (cdclt_sat_solver:restarts(RestartsCdcltRaw); RestartsCdcltRaw = 0), | |
| 1169 | format("Restarts: ~w~n", [RestartsCdcltRaw]), | |
| 1170 | TimeCdcltRaw is StopCdcltRaw - StartCdcltRaw, | |
| 1171 | ( solved_constraint(ResCdcltRaw) | |
| 1172 | -> inc_solved_counter(raw_smt) | |
| 1173 | ; true | |
| 1174 | ), | |
| 1175 | add_benchmark_result(raw_smt, ConstraintPath, ResCdcltRaw), | |
| 1176 | !, | |
| 1177 | nl,nl,write(ResCdcltRaw),nl,nl, | |
| 1178 | write('done.'), nl, | |
| 1179 | preferences:set_preference(time_out, Timeout), | |
| 1180 | set_preference(cdclt_perform_static_analysis,true), | |
| 1181 | set_preference(cdclt_perform_symmetry_breaking,true), | |
| 1182 | %% | |
| 1183 | write('Solve with Z3-Par..'),nl, | |
| 1184 | write(ConstraintPath),nl, | |
| 1185 | error_manager:reset_errors, | |
| 1186 | statistics(walltime, [StartZ3Par|_]), | |
| 1187 | smt_solve_predicate(z3,Constraint, _, ResZ3Par), | |
| 1188 | %ResZ3Par = no_solution_found(solver_answered_unknown), | |
| 1189 | statistics(walltime, [StopZ3Par|_]), | |
| 1190 | TimeZ3Par is StopZ3Par - StartZ3Par, | |
| 1191 | ( solved_constraint(ResZ3Par) | |
| 1192 | -> inc_solved_counter(z3par) | |
| 1193 | ; true | |
| 1194 | ), | |
| 1195 | add_benchmark_result(z3par, ConstraintPath, ResZ3Par), | |
| 1196 | !, | |
| 1197 | nl,nl,write(ResZ3Par),nl,nl, | |
| 1198 | preferences:set_preference(time_out, Timeout), | |
| 1199 | write('Solve with Z3-Axm..'),nl, | |
| 1200 | write(ConstraintPath),nl, | |
| 1201 | error_manager:reset_errors, | |
| 1202 | statistics(walltime, [StartZ3Axm|_]), | |
| 1203 | smt_solve_predicate(z3axm,Constraint, _, ResZ3Axm), | |
| 1204 | %ResZ3Axm = no_solution_found(solver_answered_unknown), | |
| 1205 | statistics(walltime, [StopZ3Axm|_]), | |
| 1206 | TimeZ3Axm is StopZ3Axm - StartZ3Axm, | |
| 1207 | ( solved_constraint(ResZ3Axm) | |
| 1208 | -> inc_solved_counter(z3axm) | |
| 1209 | ; true | |
| 1210 | ), | |
| 1211 | add_benchmark_result(z3axm, ConstraintPath, ResZ3Axm), | |
| 1212 | !, | |
| 1213 | nl,nl,write(ResZ3Axm),nl,nl, | |
| 1214 | preferences:set_preference(time_out, Timeout), | |
| 1215 | write('Solve with Z3-Cns..'),nl, | |
| 1216 | write(ConstraintPath),nl, | |
| 1217 | error_manager:reset_errors, | |
| 1218 | statistics(walltime, [StartZ3Cns|_]), | |
| 1219 | smt_solve_predicate(z3cns,Constraint, _, ResZ3Cns), | |
| 1220 | %ResZ3Cns = no_solution_found(solver_answered_unknown), | |
| 1221 | statistics(walltime, [StopZ3Cns|_]), | |
| 1222 | TimeZ3Cns is StopZ3Cns - StartZ3Cns, | |
| 1223 | ( solved_constraint(ResZ3Cns) | |
| 1224 | -> inc_solved_counter(z3cns) | |
| 1225 | ; true | |
| 1226 | ), | |
| 1227 | add_benchmark_result(z3cns, ConstraintPath, ResZ3Cns), | |
| 1228 | !, | |
| 1229 | nl,nl,write(ResZ3Cns),nl,nl, | |
| 1230 | preferences:set_preference(time_out, Timeout), | |
| 1231 | write('Solve with Z3-Dec..'),nl, | |
| 1232 | write(ConstraintPath),nl, | |
| 1233 | error_manager:reset_errors, | |
| 1234 | statistics(walltime, [StartZ3Dec|_]), | |
| 1235 | smt_solve_predicate(z3, [decompose_into_components], Constraint, _, ResZ3Dec), | |
| 1236 | %ResZ3Dec = no_solution_found(solver_answered_unknown), | |
| 1237 | statistics(walltime, [StopZ3Dec|_]), | |
| 1238 | TimeZ3Dec is StopZ3Dec - StartZ3Dec, | |
| 1239 | ( solved_constraint(ResZ3Dec) | |
| 1240 | -> inc_solved_counter(z3dec) | |
| 1241 | ; true | |
| 1242 | ), | |
| 1243 | add_benchmark_result(z3dec, ConstraintPath, ResZ3Dec), | |
| 1244 | !, | |
| 1245 | nl,nl,write(ResZ3Dec),nl,nl, | |
| 1246 | preferences:set_preference(time_out, Timeout), | |
| 1247 | write('Solve with Sym-ProB..'),nl, | |
| 1248 | write(ConstraintPath),nl, | |
| 1249 | error_manager:reset_errors, | |
| 1250 | preferences:set_preference(use_chr_solver, false), | |
| 1251 | preferences:set_preference(use_common_subexpression_elimination, false), | |
| 1252 | preferences:set_preference(use_common_subexpression_also_for_predicates, false), | |
| 1253 | statistics(walltime, [StartProBSym|_]), | |
| 1254 | clean_up_pred(Constraint, [], CConstraint), | |
| 1255 | (add_symmetry_breaking_predicates(CConstraint, SymConstraint), !; SymConstraint = CConstraint), | |
| 1256 | get_amount_of_found_sbps(FoundSBPs), | |
| 1257 | asserta(symmetry_breaking_predicates(ConstraintPath,prob_sym,FoundSBPs)), | |
| 1258 | 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), | |
| 1259 | %ResProBSym = no_solution_found(solver_answered_unknown), | |
| 1260 | statistics(walltime, [StopProBSym|_]), | |
| 1261 | TimeProBSym is StopProBSym - StartProBSym, | |
| 1262 | ( solved_constraint(ResProBSym) | |
| 1263 | -> inc_solved_counter(prob_sym) | |
| 1264 | ; true | |
| 1265 | ), | |
| 1266 | add_benchmark_result(prob_sym, ConstraintPath, ResProBSym), | |
| 1267 | !, | |
| 1268 | nl,nl,write(ResProBSym),nl,nl, | |
| 1269 | preferences:set_preference(time_out, Timeout), | |
| 1270 | write('Solve with ProB..'),nl, | |
| 1271 | write(ConstraintPath),nl, | |
| 1272 | error_manager:reset_errors, | |
| 1273 | preferences:set_preference(use_chr_solver, false), | |
| 1274 | preferences:set_preference(use_common_subexpression_elimination, false), | |
| 1275 | preferences:set_preference(use_common_subexpression_also_for_predicates, false), | |
| 1276 | statistics(walltime, [StartProB|_]), | |
| 1277 | 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), | |
| 1278 | %ResProB = no_solution_found(solver_answered_unknown), | |
| 1279 | statistics(walltime, [StopProB|_]), | |
| 1280 | TimeProB is StopProB - StartProB, | |
| 1281 | ( solved_constraint(ResProB) | |
| 1282 | -> inc_solved_counter(prob) | |
| 1283 | ; true | |
| 1284 | ), | |
| 1285 | add_benchmark_result(prob, ConstraintPath, ResProB), | |
| 1286 | !, | |
| 1287 | nl,nl,write(ResProB),nl,nl, | |
| 1288 | write('Solve with ProB-CHR..'),nl, | |
| 1289 | preferences:set_preference(time_out, Timeout), | |
| 1290 | write(ConstraintPath),nl, | |
| 1291 | error_manager:reset_errors, | |
| 1292 | preferences:set_preference(use_chr_solver, true), | |
| 1293 | preferences:set_preference(use_common_subexpression_elimination, false), | |
| 1294 | preferences:set_preference(use_common_subexpression_also_for_predicates, false), | |
| 1295 | statistics(walltime, [StartProBChr|_]), | |
| 1296 | 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), | |
| 1297 | %ResProBChr = no_solution_found(solver_answered_unknown), | |
| 1298 | statistics(walltime, [StopProBChr|_]), | |
| 1299 | TimeProBChr is StopProBChr - StartProBChr, | |
| 1300 | ( solved_constraint(ResProBChr) | |
| 1301 | -> inc_solved_counter(prob_chr) | |
| 1302 | ; true | |
| 1303 | ), | |
| 1304 | add_benchmark_result(prob_chr, ConstraintPath, ResProBChr), | |
| 1305 | !, | |
| 1306 | nl,nl,write(ResProBChr),nl,nl, | |
| 1307 | write('Solve with ProB-CSE..'),nl, | |
| 1308 | write(ConstraintPath),nl, | |
| 1309 | error_manager:reset_errors, | |
| 1310 | preferences:set_preference(use_chr_solver, false), | |
| 1311 | preferences:set_preference(use_common_subexpression_elimination, true), | |
| 1312 | preferences:set_preference(use_common_subexpression_also_for_predicates, true), | |
| 1313 | statistics(walltime, [StartProBCse|_]), | |
| 1314 | %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), | |
| 1315 | ResProBCse = no_solution_found(solver_answered_unknown), | |
| 1316 | statistics(walltime, [StopProBCse|_]), | |
| 1317 | TimeProBCse is StopProBCse - StartProBCse, | |
| 1318 | ( solved_constraint(ResProBCse) | |
| 1319 | -> inc_solved_counter(prob_cse) | |
| 1320 | ; true | |
| 1321 | ), | |
| 1322 | add_benchmark_result(prob_cse, ConstraintPath, ResProBCse), | |
| 1323 | !, | |
| 1324 | nl,nl,write(ResProBCse),nl,nl, | |
| 1325 | write('Solve with ProB-Comp..'),nl, | |
| 1326 | statistics(walltime, [StartProBComp|_]), | |
| 1327 | find_identifier_uses(Constraint, [], UsedIds), | |
| 1328 | temporary_set_preference(data_validation_mode, true), | |
| 1329 | catch(b_compile(Constraint, UsedIds, [], [], AstCompiled, no_wf_available), | |
| 1330 | enumeration_warning(_,_,_,_,_), % cancel if enumeration warning has occurred | |
| 1331 | AstCompiled = Constraint), | |
| 1332 | clear_wd_errors, % b_compile might throw a wd error | |
| 1333 | reset_temporary_preference(data_validation_mode), | |
| 1334 | %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), | |
| 1335 | ResProBComp = no_solution_found(solver_answered_unknown), | |
| 1336 | statistics(walltime, [StopProBComp|_]), | |
| 1337 | TimeProBComp is StopProBComp - StartProBComp, | |
| 1338 | ( solved_constraint(ResProBComp) | |
| 1339 | -> inc_solved_counter(prob_comp) | |
| 1340 | ; true | |
| 1341 | ), | |
| 1342 | add_benchmark_result(prob_comp, ConstraintPath, ResProBComp), | |
| 1343 | !, | |
| 1344 | nl,nl,write(ResProBComp),nl,nl, | |
| 1345 | write('done.'), nl. | |
| 1346 | /*( validate_results(ResCdclt, ResProB), | |
| 1347 | validate_results(ResCdcltIdl, ResProB), | |
| 1348 | validate_results(ResCdcltNoSym, ResProB) | |
| 1349 | -> true | |
| 1350 | ; add_error(benchmark_constraint, 'Benchmarks results differ'), | |
| 1351 | writeq(ResCdclt), | |
| 1352 | writeq(ResCdcltIdl), | |
| 1353 | writeq(ResCdcltNoSym), | |
| 1354 | writeq(ResProB) | |
| 1355 | ).*/ | |
| 1356 | ||
| 1357 | solved_constraint(solution(_)). | |
| 1358 | solved_constraint(contradiction_found). | |
| 1359 | ||
| 1360 | %validate_results(contradiction_found, contradiction_found). | |
| 1361 | %validate_results(time_out, _). | |
| 1362 | %validate_results(_, time_out). | |
| 1363 | %validate_results(solution(_), solution(_)). | |
| 1364 | ||
| 1365 | %% N-Queens, e.g., to evaluate performance improvement of quantifier instantiation for | |
| 1366 | 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. | |
| 1367 | ||
| 1368 | p(L) :- | |
| 1369 | writeq(L), nl, | |
| 1370 | L = [_AmountOfSatVars,(prob,N,TimeProB,_FResProB),(z3,N,TimeZ3,_FResZ3),(sym_smt,N,TimeCdclt,_FResCdclt)], | |
| 1371 | format("~w & ~w & ~w & ~w & ~n", [N,TimeProB,TimeZ3,TimeCdclt]). | |
| 1372 | ||
| 1373 | print_n_queens_data(Data) :- | |
| 1374 | maplist(p, Data). | |
| 1375 | ||
| 1376 | % for an evaluation of quantifier instantiation | |
| 1377 | run_n_queens_benchmarks :- | |
| 1378 | N = [4,6,8,10,12,14,16,18,20], | |
| 1379 | preferences:set_preference(time_out, 60000), | |
| 1380 | run_n_queens_benchmarks(N, [], Data), | |
| 1381 | print_n_queens_data(Data). | |
| 1382 | ||
| 1383 | run_n_queens_benchmarks([], Data, Data). | |
| 1384 | run_n_queens_benchmarks([N|T], DataAcc, Data) :- | |
| 1385 | run_n_queens_benchmark(N, DataAcc, NewDataAcc), | |
| 1386 | run_n_queens_benchmarks(T, NewDataAcc, Data). | |
| 1387 | ||
| 1388 | run_n_queens_benchmark(N, DataAcc, NewDataAcc) :- | |
| 1389 | n_queens_encoding(N, Constraint), | |
| 1390 | ast_optimizer_for_smt:precompute_values(Constraint, [instantiate_quantifier_limit(10000)], IConstraint), | |
| 1391 | cdclt_solver:get_amount_of_sat_variables(IConstraint, AmountOfSatVars), | |
| 1392 | format("Amount of SAT variables: ~w", [AmountOfSatVars]),nl, | |
| 1393 | format("Solve with ProB for N=~w~n", [N]), | |
| 1394 | statistics(walltime, [StartProB|_]), | |
| 1395 | solve_predicate(IConstraint, _, 1, [use_smt_mode/true,use_clpfd_solver/true,clean_up_pred,allow_improving_wd_mode/true], ResProB), | |
| 1396 | statistics(walltime, [StopProB|_]), | |
| 1397 | ResProB \= contradiction_found, | |
| 1398 | TimeProB is StopProB - StartProB, | |
| 1399 | format("Solve with Z3~n for N=~w", [N]), | |
| 1400 | statistics(walltime, [StartZ3|_]), | |
| 1401 | smt_solve_predicate(z3, Constraint, _, ResZ3), | |
| 1402 | statistics(walltime, [StopZ3|_]), | |
| 1403 | ResZ3 \= contradiction_found, | |
| 1404 | TimeZ3 is StopZ3 - StartZ3, | |
| 1405 | format("Solve with Sym-SMT~n for N=~w", [N]), | |
| 1406 | set_preference(cdclt_perform_static_analysis, true), | |
| 1407 | set_preference(cdclt_perform_symmetry_breaking, true), | |
| 1408 | cdclt_solver:init, | |
| 1409 | statistics(walltime, [StartCdclt|_]), | |
| 1410 | cdclt_solve_predicate(sym_smt, Constraint, _SolvedPred, ResCdclt), | |
| 1411 | statistics(walltime, [StopCdclt|_]), | |
| 1412 | ResCdclt \= contradiction_found, | |
| 1413 | TimeCdclt is StopCdclt - StartCdclt, | |
| 1414 | functor(ResProB, FResProB, _), | |
| 1415 | functor(ResZ3, FResZ3, _), | |
| 1416 | functor(ResCdclt, FResCdclt, _), | |
| 1417 | append(DataAcc, [[AmountOfSatVars,(prob,N,TimeProB,FResProB),(z3,N,TimeZ3,FResZ3),(sym_smt,N,TimeCdclt,FResCdclt)]], NewDataAcc). | |
| 1418 | ||
| 1419 | %% Mixed constraints, e.g., taken from program synthesis or Alloy2B | |
| 1420 | % Run benchmarks from prob_prolog root folder. | |
| 1421 | ||
| 1422 | run_misc_benchmarks :- | |
| 1423 | setup_scheduler, | |
| 1424 | reset_misc_benchmarks, | |
| 1425 | benchmark(_, _), | |
| 1426 | fail. | |
| 1427 | run_misc_benchmarks :- | |
| 1428 | preferences:temporary_set_preference(normalize_ast, true), | |
| 1429 | findall(FastestSolver-SolutionOrNot-TimeDiff, fastest_solver(FastestSolver, SolutionOrNot, TimeDiff), LFastestSolver), | |
| 1430 | length(LFastestSolver, Results), | |
| 1431 | format("~n~n#Results: ~w~n~n", [Results]), | |
| 1432 | print_complete_benchmarks(LFastestSolver), | |
| 1433 | preferences:reset_temporary_preference(normalize_ast). | |
| 1434 | ||
| 1435 | reset_misc_benchmarks :- | |
| 1436 | retractall(fastest_solver(_, _, _)),!. | |
| 1437 | ||
| 1438 | setup_scheduler :- | |
| 1439 | bmachine:b_load_machine_from_file(prob_examples('public_examples/Synthesis_Tests/scheduler.mch')), | |
| 1440 | bmachine:b_machine_precompile,!. | |
| 1441 | ||
| 1442 | load_constraint_from_file(FilePath, Constraint) :- | |
| 1443 | file_exists(FilePath), | |
| 1444 | !, | |
| 1445 | open(FilePath, read, Stream), | |
| 1446 | read_term(Stream, Constraint, []), | |
| 1447 | close(Stream). | |
| 1448 | load_constraint_from_file(FilePath, _) :- | |
| 1449 | format("File does not exist: ~w~n~n", [FilePath]), | |
| 1450 | fail. | |
| 1451 | ||
| 1452 | benchmark_misc_constraint(Constraint, FastestSolver, Res, TimeDiff) :- | |
| 1453 | preferences:set_preference(randomise_enumeration_order, false), | |
| 1454 | format("Solve with ProB..~n", []), | |
| 1455 | statistics(walltime, [ProBStart|_]), | |
| 1456 | %kodkod_annotator:annotate_kodkod_constraints(greedy, Constraint, AConstraint), | |
| 1457 | solve_predicate(Constraint, _, 1, [use_smt_mode/true,use_clpfd_solver/true,clean_up_pred,allow_improving_wd_mode/true], ProBRes), | |
| 1458 | statistics(walltime, [ProBEnd|_]), | |
| 1459 | format("~nProB result: ~w~n", [ProBRes]), | |
| 1460 | ProBTime is ProBEnd - ProBStart, | |
| 1461 | format("ProB finished.~nSolve with CDCL(T)..~n", []), | |
| 1462 | statistics(walltime, [CDCLTStart|_]), | |
| 1463 | cdclt_solve_predicate(Constraint, _, CDCLTRes), | |
| 1464 | statistics(walltime, [CDCLTEnd|_]), | |
| 1465 | format("~nCDCL(T) result: ~w~n", [CDCLTRes]), | |
| 1466 | format("CDCL(T) finished..~n", []), | |
| 1467 | CDCLTTime is CDCLTEnd - CDCLTStart, | |
| 1468 | print_times(ProBTime, CDCLTTime), | |
| 1469 | !, | |
| 1470 | ( ProBRes = solution(_), | |
| 1471 | ( CDCLTRes == contradiction_found | |
| 1472 | ; CDCLTRes == error), | |
| 1473 | format('Error found: ProB found a solution while CDCL(T) did not.', []), | |
| 1474 | trace | |
| 1475 | ; ProBRes = contradiction_found, | |
| 1476 | ( CDCLTRes = solution(_) | |
| 1477 | ; CDCLTRes == error), | |
| 1478 | format('Error found: ProB found a contradiction while CDCL(T) did not.', []), | |
| 1479 | trace | |
| 1480 | ; CDCLTRes == time_out, | |
| 1481 | ProBRes == time_out, | |
| 1482 | Res = time_out, | |
| 1483 | FastestSolver = same, | |
| 1484 | TimeDiff = 0 | |
| 1485 | ; ProBRes == time_out, | |
| 1486 | solution_or_contradiction(CDCLTRes, Res), | |
| 1487 | !, | |
| 1488 | FastestSolver = cdclt, | |
| 1489 | TimeDiff is ProBTime - CDCLTTime | |
| 1490 | ; CDCLTRes == time_out, | |
| 1491 | solution_or_contradiction(ProBRes, Res), | |
| 1492 | !, | |
| 1493 | FastestSolver = prob, | |
| 1494 | TimeDiff is CDCLTTime - ProBTime | |
| 1495 | ; % ProB could not find a result but CDCL(T) | |
| 1496 | ProBRes = no_solution_found(_), | |
| 1497 | solution_or_contradiction(CDCLTRes, Res), | |
| 1498 | !, | |
| 1499 | FastestSolver = cdclt, | |
| 1500 | TimeDiff = 0 | |
| 1501 | ; % CDCL(T) could not find a result but ProB | |
| 1502 | CDCLTRes = no_solution_found(_), | |
| 1503 | solution_or_contradiction(ProBRes, Res), | |
| 1504 | !, | |
| 1505 | FastestSolver = prob, | |
| 1506 | TimeDiff = 0 | |
| 1507 | ; CDCLTTime < ProBTime, | |
| 1508 | FastestSolver = cdclt, | |
| 1509 | solution_or_contradiction(CDCLTRes, Res), | |
| 1510 | TimeDiff is ProBTime - CDCLTTime | |
| 1511 | ; CDCLTTime > ProBTime, | |
| 1512 | FastestSolver = prob, | |
| 1513 | solution_or_contradiction(CDCLTRes, Res), | |
| 1514 | TimeDiff is CDCLTTime - ProBTime | |
| 1515 | ; CDCLTTime == ProBTime, | |
| 1516 | FastestSolver = same, | |
| 1517 | solution_or_contradiction(CDCLTRes, Res), | |
| 1518 | TimeDiff = 0),!. | |
| 1519 | ||
| 1520 | solution_or_contradiction(solution(_), solution). | |
| 1521 | solution_or_contradiction(contradiction_found, contradiction). | |
| 1522 | ||
| 1523 | print_times(ProBTime, CDCLTTime) :- | |
| 1524 | format("ProB: ~w~nCDCL(T) using ProB only: ~w~n", [ProBTime, CDCLTTime]). | |
| 1525 | ||
| 1526 | print_enter_benchmark(Nr) :- | |
| 1527 | format("Run benchmark #~d~n---------------------------------------~n", [Nr]). | |
| 1528 | ||
| 1529 | print_complete_benchmarks(LFastestSolver) :- | |
| 1530 | filter_fastest_solver(cdclt, LFastestSolver, CdcltSol, CdcltNoSol, _, CdcltTimeDiff), | |
| 1531 | filter_fastest_solver(prob, LFastestSolver, ProBSol, ProBNoSol, _, ProBTimeDiff), | |
| 1532 | filter_fastest_solver(same, LFastestSolver, SameSol, SameNoSol, SameTimeout, _), | |
| 1533 | 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]), | |
| 1534 | ( CdcltTimeDiff > ProBTimeDiff | |
| 1535 | -> TotalDiff is CdcltTimeDiff - ProBTimeDiff, | |
| 1536 | format("~nIn total, CDCL(T) is ~d ms faster than ProB.~n", [TotalDiff]) | |
| 1537 | ; TotalDiff is ProBTimeDiff - CdcltTimeDiff, | |
| 1538 | format("~nIn total, ProB is ~d ms faster than CDCL(T).~n", [TotalDiff]) | |
| 1539 | ). | |
| 1540 | ||
| 1541 | filter_fastest_solver(Name, LFastestSolver, SolAmount, ContrAmount, TimeoutsAmount, TimeDiff) :- | |
| 1542 | findall(TimeDiff, member(Name-solution-TimeDiff, LFastestSolver), Solutions), | |
| 1543 | findall(TimeDiff, member(Name-contradiction-TimeDiff, LFastestSolver), Contradictions), | |
| 1544 | findall(TimeDiff, member(Name-time_out-TimeDiff, LFastestSolver), Timeouts), | |
| 1545 | length(Solutions, SolAmount), | |
| 1546 | length(Contradictions, ContrAmount), | |
| 1547 | length(Timeouts, TimeoutsAmount), | |
| 1548 | sumlist(Solutions, TimeDiff1), | |
| 1549 | sumlist(Contradictions, TimeDiff2), | |
| 1550 | TimeDiff is TimeDiff1 + TimeDiff2. | |
| 1551 | ||
| 1552 | benchmark(1, [synthesis]) :- | |
| 1553 | print_enter_benchmark(1), | |
| 1554 | setup_scheduler, | |
| 1555 | preferences:temporary_set_preference(time_out, 2500, OldTimeOut), | |
| 1556 | load_constraint_from_file(prob_examples('public_examples/Synthesis_Tests/constraints/scheduler_inv1_contradiction.pl'), Constraint), | |
| 1557 | benchmark_misc_constraint(Constraint, FastestSolver, Res, TimeDiff), | |
| 1558 | asserta(fastest_solver(FastestSolver, Res, TimeDiff)), | |
| 1559 | preferences:reset_temporary_preference(time_out, OldTimeOut). | |
| 1560 | ||
| 1561 | benchmark(2, [synthesis]) :- | |
| 1562 | print_enter_benchmark(2), | |
| 1563 | setup_scheduler, | |
| 1564 | preferences:temporary_set_preference(time_out, 2500, OldTimeOut), | |
| 1565 | load_constraint_from_file(prob_examples('public_examples/Synthesis_Tests/constraints/scheduler_inv2_contradiction.pl'), Constraint), | |
| 1566 | benchmark_misc_constraint(Constraint, FastestSolver, Res, TimeDiff), | |
| 1567 | asserta(fastest_solver(FastestSolver, Res, TimeDiff)), | |
| 1568 | preferences:reset_temporary_preference(time_out, OldTimeOut). | |
| 1569 | ||
| 1570 | benchmark(3, [synthesis]) :- | |
| 1571 | print_enter_benchmark(3), | |
| 1572 | setup_scheduler, | |
| 1573 | preferences:temporary_set_preference(time_out, 2500, OldTimeOut), | |
| 1574 | load_constraint_from_file(prob_examples('public_examples/Synthesis_Tests/constraints/scheduler_inv3_contradiction.pl'), Constraint), | |
| 1575 | benchmark_misc_constraint(Constraint, FastestSolver, Res, TimeDiff), | |
| 1576 | asserta(fastest_solver(FastestSolver, Res, TimeDiff)), | |
| 1577 | preferences:reset_temporary_preference(time_out, OldTimeOut). | |
| 1578 | ||
| 1579 | benchmark(4, [synthesis]) :- | |
| 1580 | print_enter_benchmark(4), | |
| 1581 | setup_scheduler, | |
| 1582 | preferences:temporary_set_preference(time_out, 2500, OldTimeOut), | |
| 1583 | load_constraint_from_file(prob_examples('public_examples/Synthesis_Tests/constraints/scheduler_inv1.pl'), Constraint), | |
| 1584 | benchmark_misc_constraint(Constraint, FastestSolver, Res, TimeDiff), | |
| 1585 | asserta(fastest_solver(FastestSolver, Res, TimeDiff)), | |
| 1586 | preferences:reset_temporary_preference(time_out, OldTimeOut). | |
| 1587 | ||
| 1588 | benchmark(5, [synthesis]) :- | |
| 1589 | % contradiction | |
| 1590 | print_enter_benchmark(5), | |
| 1591 | setup_scheduler, | |
| 1592 | preferences:temporary_set_preference(time_out, 2500, OldTimeOut), | |
| 1593 | load_constraint_from_file(prob_examples('public_examples/Synthesis_Tests/constraints/scheduler_inv2_contradiction.pl'), Constraint), | |
| 1594 | benchmark_misc_constraint(Constraint, FastestSolver, Res, TimeDiff), | |
| 1595 | asserta(fastest_solver(FastestSolver, Res, TimeDiff)), | |
| 1596 | preferences:reset_temporary_preference(time_out, OldTimeOut). | |
| 1597 | ||
| 1598 | benchmark(6, [synthesis]) :- | |
| 1599 | print_enter_benchmark(6), | |
| 1600 | setup_scheduler, | |
| 1601 | preferences:temporary_set_preference(time_out, 2500, OldTimeOut), | |
| 1602 | load_constraint_from_file(prob_examples('public_examples/Synthesis_Tests/constraints/scheduler_inv3.pl'), Constraint), | |
| 1603 | benchmark_misc_constraint(Constraint, FastestSolver, Res, TimeDiff), | |
| 1604 | asserta(fastest_solver(FastestSolver, Res, TimeDiff)), | |
| 1605 | preferences:reset_temporary_preference(time_out, OldTimeOut). | |
| 1606 | ||
| 1607 | benchmark(7, [synthesis]) :- | |
| 1608 | print_enter_benchmark(7), | |
| 1609 | setup_scheduler, | |
| 1610 | preferences:temporary_set_preference(time_out, 2500, OldTimeOut), | |
| 1611 | load_constraint_from_file(prob_examples('public_examples/Synthesis_Tests/constraints/scheduler_inv4.pl'), Constraint), | |
| 1612 | benchmark_misc_constraint(Constraint, FastestSolver, Res, TimeDiff), | |
| 1613 | asserta(fastest_solver(FastestSolver, Res, TimeDiff)), | |
| 1614 | preferences:reset_temporary_preference(time_out, OldTimeOut). | |
| 1615 | ||
| 1616 | benchmark(8, [synthesis]) :- | |
| 1617 | print_enter_benchmark(8), | |
| 1618 | setup_scheduler, | |
| 1619 | preferences:temporary_set_preference(time_out, 2500, OldTimeOut), | |
| 1620 | load_constraint_from_file(prob_examples('public_examples/Synthesis_Tests/constraints/scheduler_new_process.pl'), Constraint), | |
| 1621 | benchmark_misc_constraint(Constraint, FastestSolver, Res, TimeDiff), | |
| 1622 | asserta(fastest_solver(FastestSolver, Res, TimeDiff)), | |
| 1623 | preferences:reset_temporary_preference(time_out, OldTimeOut). | |
| 1624 | ||
| 1625 | benchmark(9, [synthesis]) :- | |
| 1626 | print_enter_benchmark(9), | |
| 1627 | setup_scheduler, | |
| 1628 | preferences:temporary_set_preference(time_out, 10000, OldTimeOut), | |
| 1629 | load_constraint_from_file(prob_examples('public_examples/Synthesis_Tests/constraints/scheduler_delete_process.pl'), Constraint), | |
| 1630 | benchmark_misc_constraint(Constraint, FastestSolver, Res, TimeDiff), | |
| 1631 | asserta(fastest_solver(FastestSolver, Res, TimeDiff)), | |
| 1632 | preferences:reset_temporary_preference(time_out, OldTimeOut). | |
| 1633 | ||
| 1634 | benchmark(10, [synthesis]) :- | |
| 1635 | print_enter_benchmark(10), | |
| 1636 | setup_scheduler, | |
| 1637 | preferences:temporary_set_preference(time_out, 2500, OldTimeOut), | |
| 1638 | load_constraint_from_file(prob_examples('public_examples/Synthesis_Tests/constraints/scheduler_set_active.pl'), Constraint), | |
| 1639 | benchmark_misc_constraint(Constraint, FastestSolver, Res, TimeDiff), | |
| 1640 | asserta(fastest_solver(FastestSolver, Res, TimeDiff)), | |
| 1641 | preferences:reset_temporary_preference(time_out, OldTimeOut). | |
| 1642 | ||
| 1643 | benchmark(11, [synthesis]) :- | |
| 1644 | % Note: CDCL(T) is much faster than ProB if chr_solver preference is set | |
| 1645 | print_enter_benchmark(11), | |
| 1646 | preferences:temporary_set_preference(time_out, 15000, OldTimeOut), | |
| 1647 | setup_scheduler, | |
| 1648 | load_constraint_from_file(prob_examples('public_examples/Synthesis_Tests/constraints/scheduler_active_to_waiting_precondition.pl'), Constraint), | |
| 1649 | benchmark_misc_constraint(Constraint, FastestSolver, Res, TimeDiff), | |
| 1650 | asserta(fastest_solver(FastestSolver, Res, TimeDiff)), | |
| 1651 | preferences:reset_temporary_preference(time_out, OldTimeOut). | |
| 1652 | ||
| 1653 | ||
| 1654 | benchmark(12, [alloy]) :- | |
| 1655 | print_enter_benchmark(12), | |
| 1656 | alloy2b:load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/alloy_models/toys/grandpa.als.pl')), | |
| 1657 | bmachine:b_machine_precompile, | |
| 1658 | preferences:temporary_set_preference(time_out, 15000, OldTimeOut), | |
| 1659 | load_constraint_from_file(prob_examples('public_examples/Alloy/constraints/alloy_self_grandpas.pl'), Constraint), | |
| 1660 | benchmark_misc_constraint(Constraint, FastestSolver, Res, TimeDiff), | |
| 1661 | asserta(fastest_solver(FastestSolver, Res, TimeDiff)), | |
| 1662 | preferences:reset_temporary_preference(time_out, OldTimeOut). | |
| 1663 | /* | |
| 1664 | benchmark(13, [alloy]) :- | |
| 1665 | print_enter_benchmark(13), | |
| 1666 | alloy2b:load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Puzzles/queens.als.pl')), | |
| 1667 | bmachine:b_machine_precompile, | |
| 1668 | preferences:temporary_set_preference(time_out, 2500, OldTimeOut), | |
| 1669 | load_constraint_from_file(prob_examples('public_examples/Alloy/constraints/alloy_queens1.pl'), Constraint), | |
| 1670 | benchmark_misc_constraint(Constraint, FastestSolver, Res, TimeDiff), | |
| 1671 | asserta(fastest_solver(FastestSolver, Res, TimeDiff)), | |
| 1672 | preferences:reset_temporary_preference(time_out, OldTimeOut). | |
| 1673 | ||
| 1674 | benchmark(14, [alloy]) :- | |
| 1675 | print_enter_benchmark(14), | |
| 1676 | alloy2b:load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Puzzles/queens.als.pl')), | |
| 1677 | bmachine:b_machine_precompile, | |
| 1678 | preferences:temporary_set_preference(time_out, 2500, OldTimeOut), | |
| 1679 | load_constraint_from_file(prob_examples('public_examples/Alloy/constraints/alloy_queens2.pl'), Constraint), | |
| 1680 | benchmark_misc_constraint(Constraint, FastestSolver, Res, TimeDiff), | |
| 1681 | asserta(fastest_solver(FastestSolver, Res, TimeDiff)), | |
| 1682 | preferences:reset_temporary_preference(time_out, OldTimeOut). | |
| 1683 | ||
| 1684 | benchmark(15, [alloy]) :- | |
| 1685 | print_enter_benchmark(15), | |
| 1686 | alloy2b:load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Puzzles/queens.als.pl')), | |
| 1687 | bmachine:b_machine_precompile, | |
| 1688 | preferences:temporary_set_preference(time_out, 2500, OldTimeOut), | |
| 1689 | load_constraint_from_file(prob_examples('public_examples/Alloy/constraints/alloy_queens3.pl'), Constraint), | |
| 1690 | benchmark_misc_constraint(Constraint, FastestSolver, Res, TimeDiff), | |
| 1691 | asserta(fastest_solver(FastestSolver, Res, TimeDiff)), | |
| 1692 | preferences:reset_temporary_preference(time_out, OldTimeOut). | |
| 1693 | */ | |
| 1694 | benchmark(16, [alloy]) :- | |
| 1695 | print_enter_benchmark(16), | |
| 1696 | alloy2b:load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Puzzles/rivercrossing.pl')), | |
| 1697 | bmachine:b_machine_precompile, | |
| 1698 | preferences:temporary_set_preference(time_out, 2500, OldTimeOut), | |
| 1699 | load_constraint_from_file(prob_examples('public_examples/Alloy/constraints/alloy_river_crossing1.pl'), Constraint), | |
| 1700 | benchmark_misc_constraint(Constraint, FastestSolver, Res, TimeDiff), | |
| 1701 | asserta(fastest_solver(FastestSolver, Res, TimeDiff)), | |
| 1702 | preferences:reset_temporary_preference(time_out, OldTimeOut). | |
| 1703 | ||
| 1704 | benchmark(17, [alloy]) :- | |
| 1705 | print_enter_benchmark(17), | |
| 1706 | alloy2b:load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Puzzles/rivercrossing.pl')), | |
| 1707 | bmachine:b_machine_precompile, | |
| 1708 | preferences:temporary_set_preference(time_out, 20000, OldTimeOut), | |
| 1709 | load_constraint_from_file(prob_examples('public_examples/Alloy/constraints/alloy_river_crossing2.pl'), Constraint), | |
| 1710 | benchmark_misc_constraint(Constraint, FastestSolver, Res, TimeDiff), | |
| 1711 | asserta(fastest_solver(FastestSolver, Res, TimeDiff)), | |
| 1712 | preferences:reset_temporary_preference(time_out, OldTimeOut). | |
| 1713 | ||
| 1714 | benchmark(18, [alloy]) :- | |
| 1715 | print_enter_benchmark(18), | |
| 1716 | alloy2b:load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Puzzles/rivercrossing.pl')), | |
| 1717 | bmachine:b_machine_precompile, | |
| 1718 | preferences:temporary_set_preference(time_out, 2500, OldTimeOut), | |
| 1719 | load_constraint_from_file(prob_examples('public_examples/Alloy/constraints/alloy_river_crossing3.pl'), Constraint), | |
| 1720 | benchmark_misc_constraint(Constraint, FastestSolver, Res, TimeDiff), | |
| 1721 | asserta(fastest_solver(FastestSolver, Res, TimeDiff)), | |
| 1722 | preferences:reset_temporary_preference(time_out, OldTimeOut). | |
| 1723 | ||
| 1724 | benchmark(19, [alloy]) :- | |
| 1725 | print_enter_benchmark(19), | |
| 1726 | alloy2b:load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Puzzles/crewalloc.als.pl')), | |
| 1727 | bmachine:b_machine_precompile, | |
| 1728 | preferences:temporary_set_preference(time_out, 10000, OldTimeOut), | |
| 1729 | load_constraint_from_file(prob_examples('public_examples/Alloy/constraints/alloy_crewalloc1.pl'), Constraint), | |
| 1730 | benchmark_misc_constraint(Constraint, FastestSolver, Res, TimeDiff), | |
| 1731 | asserta(fastest_solver(FastestSolver, Res, TimeDiff)), | |
| 1732 | preferences:reset_temporary_preference(time_out, OldTimeOut). | |
| 1733 | ||
| 1734 | benchmark(20, [alloy]) :- | |
| 1735 | print_enter_benchmark(20), | |
| 1736 | alloy2b:load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Puzzles/crewalloc.als.pl')), | |
| 1737 | bmachine:b_machine_precompile, | |
| 1738 | preferences:temporary_set_preference(time_out, 2500, OldTimeOut), | |
| 1739 | load_constraint_from_file(prob_examples('public_examples/Alloy/constraints/alloy_crewalloc2.pl'), Constraint), | |
| 1740 | benchmark_misc_constraint(Constraint, FastestSolver, Res, TimeDiff), | |
| 1741 | asserta(fastest_solver(FastestSolver, Res, TimeDiff)), | |
| 1742 | preferences:reset_temporary_preference(time_out, OldTimeOut). | |
| 1743 | ||
| 1744 | benchmark(21, [misc]) :- | |
| 1745 | print_enter_benchmark(21), | |
| 1746 | preferences:temporary_set_preference(time_out, 2500, OldTimeOut), | |
| 1747 | 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,[]), | |
| 1748 | benchmark_misc_constraint(Constraint, FastestSolver, Res, TimeDiff), | |
| 1749 | asserta(fastest_solver(FastestSolver, Res, TimeDiff)), | |
| 1750 | preferences:reset_temporary_preference(time_out, OldTimeOut). | |
| 1751 | ||
| 1752 | % process gets killed for theory prop, CLP(FD) bug in SICStus? | |
| 1753 | % probcli -repl ../prob_examples/public_examples/B/PragmasUnits/CaseStudies/Abrial_Hybrid/hybrid_nuclear/C_m0.mch -init | |
| 1754 | % :cdclt-free #file ../prob_examples/public_examples/B/SmtSolverTests/raw_benchmarks/additional_benchmarks_bmc/public_examples/B/PragmasUnits/CaseStudies/Abrial_Hybrid/hybrid_nuclear/C_m0_monolithic_bmc_k_10.eval | |
| 1755 | /*smt_benchmarks_path('/home/joshua/smt-comp/lia19/psyco'). | |
| 1756 | ||
| 1757 | run_smt_comp_benchmarks :- | |
| 1758 | retractall(smt_stat(_, _, _, _, _)), | |
| 1759 | smt_benchmarks_path(Root), | |
| 1760 | run_smt_comp_benchmarks(Root), | |
| 1761 | print_smt_comp_results. | |
| 1762 | ||
| 1763 | print_smt_comp_results :- | |
| 1764 | findall(smt_stat(FilePath, CdcltTime, ProBTime, CdcltRes, ProBRes), retract(smt_stat(FilePath, CdcltTime, ProBTime, CdcltRes, ProBRes)), Stats), | |
| 1765 | print_smt_comp_results(Stats). | |
| 1766 | ||
| 1767 | print_smt_comp_results(Stats) :- | |
| 1768 | open('cdclt_benchmarks_smt_comp.txt', write, Stream), | |
| 1769 | write(Stream, 'Filepath,Time CDCL(T),Result CDCL(T),Time ProB,Result ProB\n'), | |
| 1770 | print_smt_comp_results_to_stream(Stream, Stats). | |
| 1771 | ||
| 1772 | print_smt_comp_results_to_stream(Stream, []) :- | |
| 1773 | close(Stream). | |
| 1774 | print_smt_comp_results_to_stream(Stream, [Stat|T]) :- | |
| 1775 | print_stat_to_stream(Stream, Stat), | |
| 1776 | print_smt_comp_results_to_stream(Stream, T). | |
| 1777 | ||
| 1778 | print_stat_to_stream(Stream, smt_stat(FilePath, cdclt_time(CdcltTime), prob_time(ProBTime), cdclt_res(CdcltRes), prob_res(ProBRes))) :- | |
| 1779 | writeq(Stream, FilePath),write(Stream, ','), writeq(Stream, CdcltTime),write(Stream, ','), writeq(Stream, CdcltRes),write(Stream, ','), | |
| 1780 | writeq(Stream, ProBTime),write(Stream, ','), writeq(Stream, ProBRes),write(Stream, '\n'). | |
| 1781 | ||
| 1782 | run_smt_comp_benchmarks(Root) :- | |
| 1783 | get_all_smt2_files(Root, [], Files),!, | |
| 1784 | run_smt_comp_benchmarks_from_files(Files). | |
| 1785 | ||
| 1786 | run_smt_comp_benchmarks_from_files(Files) :- | |
| 1787 | member(_-FilePath, Files), | |
| 1788 | smtlib2_file(FilePath), | |
| 1789 | retract(smtlib2_interpreter:stat(CdcltTime, ProBTime, CdcltRes, ProBRes)), | |
| 1790 | asserta(smt_stat(FilePath, CdcltTime, ProBTime, CdcltRes, ProBRes)), | |
| 1791 | format("SMT-lib file path: ~w", [FilePath]), | |
| 1792 | fail. | |
| 1793 | run_smt_comp_benchmarks_from_files(_). | |
| 1794 | ||
| 1795 | get_all_smt2_files(Path, Acc, Files) :- | |
| 1796 | directory_exists(Path), | |
| 1797 | file_members_of_directory(Path, '*.smt2', Members), | |
| 1798 | directory_members_of_directory(Path, Dirs), | |
| 1799 | append(Acc, Members, NewAcc), | |
| 1800 | map_get_all_smt2_files(Dirs, NewAcc, Files). | |
| 1801 | ||
| 1802 | map_get_all_smt2_files([], Acc, Acc). | |
| 1803 | map_get_all_smt2_files([_-Dir|T], Acc, Files) :- | |
| 1804 | get_all_smt2_files(Dir, Acc, NewAcc), | |
| 1805 | map_get_all_smt2_files(T, NewAcc, Files).*/ | |
| 1806 | ||
| 1807 | ||
| 1808 | ||
| 1809 | % Interesting constraints for ProB-Z3 | |
| 1810 | /* | |
| 1811 | ||
| 1812 | :- use_module(probsrc(bmachine), [b_set_empty_machine/0, b_machine_precompile/0]). | |
| 1813 | :- use_module(probsrc(eval_strings), [eval_codes/6]). | |
| 1814 | :- use_module(library(timeout), [time_out/3]). | |
| 1815 | ||
| 1816 | :- dynamic index/0. | |
| 1817 | :- volatile index/0. | |
| 1818 | ||
| 1819 | timeout(15000). | |
| 1820 | ||
| 1821 | reset_dynamic_state :- | |
| 1822 | retractall(index(_)), | |
| 1823 | asserta(index(1)). | |
| 1824 | ||
| 1825 | %% run_benchmarks(+OutputFilePath). | |
| 1826 | run_benchmarks(OutputFilePath) :- | |
| 1827 | b_set_empty_machine, | |
| 1828 | b_machine_precompile, | |
| 1829 | reset_dynamic_state, | |
| 1830 | open(OutputFilePath, write, OutStream), | |
| 1831 | format(OutStream, "Result ProB, Bindings ProB, Time ProB, Result Z3, Bindings Z3, Time Z3~n", []), | |
| 1832 | findall(B, benchmark(B), Preds), | |
| 1833 | timeout(Timeout), | |
| 1834 | run_benchmarks_loop(Timeout, Preds, OutStream), | |
| 1835 | close(OutStream). | |
| 1836 | ||
| 1837 | %% increase_index(-CurIndex). | |
| 1838 | increase_index(CurIndex) :- | |
| 1839 | retract(index(CurIndex)), | |
| 1840 | NewIndex is CurIndex + 1, | |
| 1841 | asserta(index(NewIndex)). | |
| 1842 | ||
| 1843 | eval_result(Timeout, TRes, TBindings, Res, Bindings) :- | |
| 1844 | Timeout == success, | |
| 1845 | !, | |
| 1846 | ( TRes == contradiction_found | |
| 1847 | -> Res = TRes, | |
| 1848 | Bindings = [] | |
| 1849 | ; Res = TRes, | |
| 1850 | Bindings = TBindings | |
| 1851 | ). | |
| 1852 | eval_result(Timeout, TRes, TBindings, time_out, []). | |
| 1853 | ||
| 1854 | %% run_benchmarks_loop(+Timeout, +Predicates, +OutStream). | |
| 1855 | run_benchmarks_loop(_, [], _). | |
| 1856 | run_benchmarks_loop(Timeout, [Pred|T], OutStream) :- | |
| 1857 | increase_index(CurIndex), | |
| 1858 | format("Solve benchmark ~w~n", [CurIndex]), | |
| 1859 | atom_codes(Pred, ProBCodes), | |
| 1860 | atom_concat(':z3 ', Pred, Z3Eval), | |
| 1861 | atom_codes(Z3Eval, Z3Codes), | |
| 1862 | statistics(walltime, [StartProB|_]), | |
| 1863 | time_out(eval_codes(ProBCodes,exists,TResProB,_,TBindingsProB,_), Timeout, TimeoutProB), | |
| 1864 | eval_result(TimeoutProB, TResProB, TBindingsProB, ResProB, BindingsProB), | |
| 1865 | statistics(walltime, [StopProB|_]), | |
| 1866 | TimeProB is StopProB - StartProB, | |
| 1867 | statistics(walltime, [StartZ3|_]), | |
| 1868 | time_out(eval_codes(Z3Codes,exists,TResZ3,_,TBindingsZ3,_), Timeout, TimeoutZ3), | |
| 1869 | eval_result(TimeoutZ3, TResZ3, TBindingsZ3, ResZ3, BindingsZ3), | |
| 1870 | statistics(walltime, [StopZ3|_]), | |
| 1871 | TimeZ3 is StopZ3 - StartZ3, | |
| 1872 | format(OutStream, "~w,~w,~w,~w,~w,~w~n", [ResProB,BindingsProB,TimeProB,ResZ3,BindingsZ3,TimeZ3]), | |
| 1873 | !, | |
| 1874 | run_benchmarks_loop(Timeout, T, OutStream). | |
| 1875 | ||
| 1876 | benchmark('x:INTEGER & x > 3'). | |
| 1877 | benchmark('x:INTEGER & y:INTEGER & x > y & y > x'). | |
| 1878 | benchmark('x:INTEGER & y:INTEGER & x = 3 & x > y & y = 4'). | |
| 1879 | benchmark('x:INTEGER & y:INTEGER & x = 3 & x > y'). | |
| 1880 | benchmark('x:INTEGER & y:INTEGER & x = 3 & x < y'). | |
| 1881 | benchmark('x:INTEGER & y:INTEGER & w:INTEGER & z:INTEGER & w > x & x > y & y > z & w = 1 & z = 1'). | |
| 1882 | benchmark('x:INTEGER & y:INTEGER & w:INTEGER & z:INTEGER & w > x & x > y & y > z & z > w'). | |
| 1883 | benchmark('x:INTEGER & y:INTEGER & x + 2 > y + 1 & y > x'). | |
| 1884 | benchmark('x:INTEGER & y:INTEGER & x > y & y > x+1'). | |
| 1885 | benchmark('x:INTEGER & y:INTEGER & x > y & gt : {x+1} & y > gt'). | |
| 1886 | benchmark('x:S & y:S & y/:T & S<:NATURAL & T=S'). | |
| 1887 | benchmark('f:1..3 --> NATURAL & g = f<+{2|->3} & g(2) /= 3'). | |
| 1888 | benchmark('{x,y,z} <: 1..200 & x+y+z = 600'). | |
| 1889 | benchmark('x:INTEGER & y:INTEGER & x >= 0 & x <= 100 & y >= 0 & y <= 100 & x * y - 37 * y + 71 * x - 2627 = 0'). | |
| 1890 | benchmark('f:NATURAL +->NATURAL & x:NATURAL & g=f<+{x|->x+1} & not(g:NATURAL+->NATURAL)'). | |
| 1891 | benchmark('f=%x.(x:1..100|x+1) & r = f(2)'). | |
| 1892 | benchmark('f=%x.(x:INTEGER|x*x*x) & f(f(x))=y & y=512 '). | |
| 1893 | benchmark('f = {(1|->2),(2|->3),(3|->4),(4|->5),(5|->6),(6|->7),(7|->8),(8|->9),(9|->10),(10|->11)} & r = (f;f)(2)'). | |
| 1894 | benchmark('f = {(1|->2),(2|->3),(3|->4),(4|->5),(5|->6),(6|->7),(7|->8),(8|->9),(9|->10),(10|->8)} & x = f[x] & x /= {} & x<:dom(f)'). | |
| 1895 | benchmark('10000..40000 = {y}'). | |
| 1896 | benchmark('f : 1..11 -->> 1..20'). | |
| 1897 | benchmark('n: 0..9999 & n1:0..9999 & {n} = r & r={n1} & (n1/=n)'). | |
| 1898 | benchmark('z:11..10002 & z2:10003..520004 & z3: -1000..11 & z4:-22222..-2000 &a: {z2,z} & a:{z3,z4}'). | |
| 1899 | benchmark('2000+x = y & 3000+y : {100000,100001}'). | |
| 1900 | benchmark('x \\/ 2..n = 0..(n+10) & x /\\ 2..n = {} & x <: 0..n+20 & n=1000'). | |
| 1901 | benchmark('f:1..n --> 1..2 & !x.(x:2..n => f(x) /= f(x-1)) & n=250'). | |
| 1902 | benchmark('f:1..10 -->> 1001..1005 & !x.(x:2..10 => f(x)>=f(x-1)) & f(1)+f(2)+f(3)+f(4)=f(5)+f(6)+f(7)+f(8)-5'). | |
| 1903 | benchmark('{X,Y,Z,V,W,A,B,C} = {1,2,3,4,5,6,7,1800} & X>Y & Y>Z & Z>V & V>W & W>A & A>B & B>C'). | |
| 1904 | benchmark('{x} /\\ {y} /= {} & x:1000000..20000000 & y>=0 & y<2000000'). | |
| 1905 | benchmark('x:1..400 & y:1..400 & f: 280..290 --> 290..299 & x|->y :f & y|->x :f'). | |
| 1906 | benchmark('x:0..10001 & y:9999..19999 & {x} /\\ 10000..999999 = {y}'). | |
| 1907 | benchmark('x = y \\/ z & y = z~ & z = %x.(x:1..n|x-1) & n=300'). | |
| 1908 | benchmark('{x} /<<: {111,112} <=> y=3 & x>112 & x:0..1500 & y:0..100'). | |
| 1909 | benchmark('x \\/ y = 1..1000 & x /\\ y = {} & x=1..102'). | |
| 1910 | benchmark('f = %x.(x:1..n|x+1) \\/ {n+1 |-> (n/2)} & x = f[x] & x /= {} & n = 20'). | |
| 1911 | benchmark('a=id(1..1000)'). | |
| 1912 | benchmark('x = %i.(i:1..10|i+i) & x[{4}] = a'). | |
| 1913 | benchmark('x = %i.(i:1..10|i+i) & x[{4}] = {8}'). | |
| 1914 | benchmark('x = %i.(i:1..10|i+i) & x[{4}] = {5}'). | |
| 1915 | benchmark('a=POW(1..10) & b=union(a) & c=inter(a)'). | |
| 1916 | benchmark('f: 1..n --> BOOL & f(1)=TRUE & !x.(x:2..n => f(x) /= f(x-1)) & n=5'). | |
| 1917 | benchmark('f: 1..n --> BOOL & f(1)=TRUE & !x.(x:2..n => f(x) /= f(x-1)) & n=60'). | |
| 1918 | */ |