| 1 | :- module(cdclt_solver_benchmarks, [run_misc_benchmarks/0, | |
| 2 | run_bmc_benchmarks1/0, | |
| 3 | run_bmc_benchmarks2/0, | |
| 4 | run_bmc_benchmarks3/0, | |
| 5 | run_bmc_benchmarks4/0, | |
| 6 | run_bmc_benchmarks5/0, | |
| 7 | run_bmc_benchmarks6/0, | |
| 8 | run_deadlock_benchmarks1/0, | |
| 9 | run_deadlock_benchmarks2/0, | |
| 10 | run_deadlock_benchmarks3/0, | |
| 11 | run_deadlock_benchmarks4/0, | |
| 12 | run_deadlock_benchmarks5/0, | |
| 13 | run_deadlock_benchmarks6/0, | |
| 14 | run_cbc_benchmarks1/0, | |
| 15 | run_cbc_benchmarks2/0, | |
| 16 | run_cbc_benchmarks3/0, | |
| 17 | run_cbc_benchmarks4/0, | |
| 18 | run_cbc_benchmarks5/0, | |
| 19 | run_cbc_benchmarks6/0, | |
| 20 | run_cbc_benchmarks/2, | |
| 21 | run_bmc_benchmarks/2, | |
| 22 | run_n_queens_benchmarks/0, | |
| 23 | amount_of_sat_vars_bmc/0, | |
| 24 | amount_of_sat_vars_inductive_inv/0, | |
| 25 | amount_of_sat_vars_deadlock/0]). | |
| 26 | ||
| 27 | :- meta_predicate(run_cbc_benchmark(0, ?, ?, ?)). | |
| 28 | :- meta_predicate(benchmark_constraint(0, ?, ?, ?, ?, ?, ?, ?, ?, ?, ?, ?, ?, ?, ?)). | |
| 29 | ||
| 30 | :- use_module(library(lists)). | |
| 31 | :- use_module(library(file_systems)). | |
| 32 | ||
| 33 | :- use_module(probsrc(preferences), [get_preference/2,set_preference/2]). | |
| 34 | :- use_module(probsrc('cdclt_solver/cdclt_solver')). | |
| 35 | :- use_module(probsrc('cdclt_solver/cdclt_settings')). | |
| 36 | :- use_module(probsrc('alloy2b/alloy2b')). | |
| 37 | :- use_module('../test_paths', []). % set up prob_examples(...) alias | |
| 38 | :- use_module(probsrc(solver_interface), [solve_predicate/3]). | |
| 39 | :- use_module(probsrc(parsercall), [call_tla2b_parser/1]). | |
| 40 | :- use_module(probsrc(bmachine), [b_machine_precompile/0,b_load_machine_from_file/1,b_load_eventb_project/1,b_load_machine_probfile/1]). | |
| 41 | ||
| 42 | :- use_module(smt_solvers_interface(smt_solvers_interface), [smt_solve_predicate/4]). | |
| 43 | ||
| 44 | :- use_module(probsrc(module_information), [module_info/2]). | |
| 45 | ||
| 46 | :- module_info(group, cdclt). | |
| 47 | :- module_info(description,'This module provides benchmarks for the CDCL(T) based solver.'). | |
| 48 | ||
| 49 | :- dynamic fastest_solver/3, solved_constraints/2, benchmark_result/3. | |
| 50 | :- volatile fastest_solver/3, solved_constraints/2, benchmark_result/3. | |
| 51 | ||
| 52 | inc_solved_counter(Solver) :- | |
| 53 | (retract(solved_constraints(Solver, Old)); Old = 0), | |
| 54 | !, | |
| 55 | New is Old + 1, | |
| 56 | asserta(solved_constraints(Solver, New)). | |
| 57 | ||
| 58 | add_benchmark_result(Solver, ConstraintPath, Result) :- | |
| 59 | asserta(benchmark_result(Solver,ConstraintPath,Result)). | |
| 60 | ||
| 61 | bmc_timeout(120000). | |
| 62 | inductive_inv_timeout(120000). | |
| 63 | deadlock_timeout(120000). | |
| 64 | ||
| 65 | amount_of_sat_vars_deadlock :- | |
| 66 | amount_of_sat_vars(deadlock, 'benchmarks_cbc_deadlock/abz16_m4/', [], Acc1), | |
| 67 | amount_of_sat_vars(deadlock, 'benchmarks_cbc_deadlock/abz16_m5/', Acc1, Acc2), | |
| 68 | amount_of_sat_vars(deadlock, 'benchmarks_cbc_deadlock/abz16_m6/', Acc2, Acc3), | |
| 69 | amount_of_sat_vars(deadlock, 'benchmarks_cbc_deadlock/abz16_m7/', Acc3, Acc4), | |
| 70 | amount_of_sat_vars(deadlock, 'benchmarks_cbc_deadlock/r0_geardoor/', Acc4, Acc5), | |
| 71 | amount_of_sat_vars(deadlock, 'benchmarks_cbc_deadlock/r1_valve/', Acc5, Acc6), | |
| 72 | amount_of_sat_vars(deadlock, 'benchmarks_cbc_deadlock/r2_outputs/', Acc6, Acc7), | |
| 73 | amount_of_sat_vars(deadlock, 'benchmarks_cbc_deadlock/r3_sensors/', Acc7, Acc8), | |
| 74 | amount_of_sat_vars(deadlock, 'benchmarks_cbc_deadlock/r4_handle/', Acc8, Acc9), | |
| 75 | amount_of_sat_vars(deadlock, 'benchmarks_cbc_deadlock/r5_switch/', Acc9, Acc10), | |
| 76 | amount_of_sat_vars(deadlock, 'benchmarks_cbc_deadlock/pm_m0_aai/', Acc10, Acc11), | |
| 77 | amount_of_sat_vars(deadlock, 'benchmarks_cbc_deadlock/pm_m0_aat/', Acc11, Acc12), | |
| 78 | amount_of_sat_vars(deadlock, 'benchmarks_cbc_deadlock/pm_m0_aoo/', Acc12, Acc13), | |
| 79 | amount_of_sat_vars(deadlock, 'benchmarks_cbc_deadlock/pm_m0_voo/', Acc13, Acc14), | |
| 80 | amount_of_sat_vars(deadlock, 'benchmarks_cbc_deadlock/pm_m0_vvi/', Acc14, Acc15), | |
| 81 | amount_of_sat_vars(deadlock, 'benchmarks_cbc_deadlock/pm_m0_vvt/', Acc15, Acc16), | |
| 82 | amount_of_sat_vars(deadlock, 'benchmarks_cbc_deadlock/pm_m1_aoor/', Acc16, Acc17), | |
| 83 | amount_of_sat_vars(deadlock, 'benchmarks_cbc_deadlock/pm_m1_voor/', Acc17, Acc18), | |
| 84 | amount_of_sat_vars(deadlock, 'benchmarks_cbc_deadlock/pm_m2_aai/', Acc18, Acc19), | |
| 85 | amount_of_sat_vars(deadlock, 'benchmarks_cbc_deadlock/simple-two-phase/', Acc19, Acc20), | |
| 86 | amount_of_sat_vars(deadlock, 'benchmarks_cbc_deadlock/prisoners-4/', Acc20, Acc21), | |
| 87 | amount_of_sat_vars(deadlock, 'benchmarks_cbc_deadlock/bakery/', Acc21, Acc22), | |
| 88 | amount_of_sat_vars(deadlock, 'benchmarks_cbc_deadlock/paxos-3/', Acc22, Acc23), | |
| 89 | amount_of_sat_vars(deadlock, 'benchmarks_cbc_deadlock/lightbot/', Acc23, Acc24), | |
| 90 | amount_of_sat_vars(deadlock, 'benchmarks_cbc_deadlock/travel_agency/', Acc24, Acc25), | |
| 91 | amount_of_sat_vars(deadlock, 'benchmarks_cbc_deadlock/search_events/', Acc25, Acc26), | |
| 92 | amount_of_sat_vars(deadlock, 'benchmarks_cbc_deadlock/large_branching/', Acc26, Acc27), | |
| 93 | mean_of_list(Acc27, TotalMean), | |
| 94 | median_of_list(Acc27, TotalMedian), | |
| 95 | max_member(Max, Acc27), | |
| 96 | open('amount_of_sat_vars_deadlock/total.txt', write, Stream), | |
| 97 | tell(Stream), | |
| 98 | format("Total mean: ~w~nTotal median: ~w~nTotal max: ~w~n", [TotalMean,TotalMedian,Max]), | |
| 99 | close(Stream). | |
| 100 | ||
| 101 | amount_of_sat_vars_inductive_inv :- | |
| 102 | amount_of_sat_vars(inductive_inv, 'benchmarks_inductive_inv/abz16_m4/', [], Acc1), | |
| 103 | amount_of_sat_vars(inductive_inv, 'benchmarks_inductive_inv/abz16_m5/', Acc1, Acc2), | |
| 104 | amount_of_sat_vars(inductive_inv, 'benchmarks_inductive_inv/abz16_m6/', Acc2, Acc3), | |
| 105 | amount_of_sat_vars(inductive_inv, 'benchmarks_inductive_inv/abz16_m7/', Acc3, Acc4), | |
| 106 | amount_of_sat_vars(inductive_inv, 'benchmarks_inductive_inv/r0_geardoor/', Acc4, Acc5), | |
| 107 | amount_of_sat_vars(inductive_inv, 'benchmarks_inductive_inv/r1_valve/', Acc5, Acc6), | |
| 108 | amount_of_sat_vars(inductive_inv, 'benchmarks_inductive_inv/r2_outputs/', Acc6, Acc7), | |
| 109 | amount_of_sat_vars(inductive_inv, 'benchmarks_inductive_inv/r3_sensors/', Acc7, Acc8), | |
| 110 | amount_of_sat_vars(inductive_inv, 'benchmarks_inductive_inv/r4_handle/', Acc8, Acc9), | |
| 111 | amount_of_sat_vars(inductive_inv, 'benchmarks_inductive_inv/r5_switch/', Acc9, Acc10), | |
| 112 | amount_of_sat_vars(inductive_inv, 'benchmarks_inductive_inv/pm_m0_aai/', Acc10, Acc11), | |
| 113 | amount_of_sat_vars(inductive_inv, 'benchmarks_inductive_inv/pm_m0_aat/', Acc11, Acc12), | |
| 114 | amount_of_sat_vars(inductive_inv, 'benchmarks_inductive_inv/pm_m0_aoo/', Acc12, Acc13), | |
| 115 | amount_of_sat_vars(inductive_inv, 'benchmarks_inductive_inv/pm_m0_voo/', Acc13, Acc14), | |
| 116 | amount_of_sat_vars(inductive_inv, 'benchmarks_inductive_inv/pm_m0_vvi/', Acc14, Acc15), | |
| 117 | amount_of_sat_vars(inductive_inv, 'benchmarks_inductive_inv/pm_m0_vvt/', Acc15, Acc16), | |
| 118 | amount_of_sat_vars(inductive_inv, 'benchmarks_inductive_inv/pm_m1_aoor/', Acc16, Acc17), | |
| 119 | amount_of_sat_vars(inductive_inv, 'benchmarks_inductive_inv/pm_m1_voor/', Acc17, Acc18), | |
| 120 | amount_of_sat_vars(inductive_inv, 'benchmarks_inductive_inv/pm_m2_aai/', Acc18, Acc19), | |
| 121 | amount_of_sat_vars(inductive_inv, 'benchmarks_inductive_inv/r6_lights/', Acc19, Acc20), | |
| 122 | amount_of_sat_vars(inductive_inv, 'benchmarks_inductive_inv/prisoners-4/', Acc20, Acc21), | |
| 123 | amount_of_sat_vars(inductive_inv, 'benchmarks_inductive_inv/bakery/', Acc21, Acc22), | |
| 124 | amount_of_sat_vars(inductive_inv, 'benchmarks_inductive_inv/paxos-3/', Acc22, Acc23), | |
| 125 | amount_of_sat_vars(inductive_inv, 'benchmarks_inductive_inv/lightbot/', Acc23, Acc24), | |
| 126 | amount_of_sat_vars(inductive_inv, 'benchmarks_inductive_inv/travel_agency/', Acc24, Acc25), | |
| 127 | amount_of_sat_vars(inductive_inv, 'benchmarks_inductive_inv/search_events/', Acc25, Acc26), | |
| 128 | amount_of_sat_vars(inductive_inv, 'benchmarks_inductive_inv/large_branching/', Acc26, Acc27), | |
| 129 | mean_of_list(Acc27, TotalMean), | |
| 130 | median_of_list(Acc27, TotalMedian), | |
| 131 | max_member(Max, Acc27), | |
| 132 | open('amount_of_sat_vars_inductive_inv/total.txt', write, Stream), | |
| 133 | tell(Stream), | |
| 134 | format("Total mean: ~w~nTotal median: ~w~nTotal max: ~w~n", [TotalMean,TotalMedian,Max]), | |
| 135 | close(Stream). | |
| 136 | ||
| 137 | amount_of_sat_vars_bmc :- | |
| 138 | amount_of_sat_vars(bmc, 'benchmarks/abz16_m4/', [], Acc1), | |
| 139 | amount_of_sat_vars(bmc, 'benchmarks/abz16_m5/', Acc1, Acc2), | |
| 140 | amount_of_sat_vars(bmc, 'benchmarks/abz16_m6/', Acc2, Acc3), | |
| 141 | amount_of_sat_vars(bmc, 'benchmarks/abz16_m7/', Acc3, Acc4), | |
| 142 | amount_of_sat_vars(bmc, 'benchmarks/r0_geardoor/', Acc4, Acc5), | |
| 143 | amount_of_sat_vars(bmc, 'benchmarks/r1_valve/', Acc5, Acc6), | |
| 144 | amount_of_sat_vars(bmc, 'benchmarks/r2_outputs/', Acc6, Acc7), | |
| 145 | amount_of_sat_vars(bmc, 'benchmarks/r3_sensors/', Acc7, Acc8), | |
| 146 | amount_of_sat_vars(bmc, 'benchmarks/r4_handle/', Acc8, Acc9), | |
| 147 | amount_of_sat_vars(bmc, 'benchmarks/r5_switch/', Acc9, Acc10), | |
| 148 | amount_of_sat_vars(bmc, 'benchmarks/pm_m0_aai/', Acc10, Acc11), | |
| 149 | amount_of_sat_vars(bmc, 'benchmarks/pm_m0_aat/', Acc11, Acc12), | |
| 150 | amount_of_sat_vars(bmc, 'benchmarks/pm_m0_aoo/', Acc12, Acc13), | |
| 151 | amount_of_sat_vars(bmc, 'benchmarks/pm_m0_voo/', Acc13, Acc14), | |
| 152 | amount_of_sat_vars(bmc, 'benchmarks/pm_m0_vvi/', Acc14, Acc15), | |
| 153 | amount_of_sat_vars(bmc, 'benchmarks/pm_m0_vvt/', Acc15, Acc16), | |
| 154 | amount_of_sat_vars(bmc, 'benchmarks/pm_m1_aoor/', Acc16, Acc17), | |
| 155 | amount_of_sat_vars(bmc, 'benchmarks/pm_m1_voor/', Acc17, Acc18), | |
| 156 | amount_of_sat_vars(bmc, 'benchmarks/pm_m2_aai/', Acc18, Acc19), | |
| 157 | amount_of_sat_vars(bmc, 'benchmarks/simple-two-phase/', Acc19, Acc20), | |
| 158 | amount_of_sat_vars(bmc, 'benchmarks/prisoners-4/', Acc20, Acc21), | |
| 159 | amount_of_sat_vars(bmc, 'benchmarks/bakery/', Acc21, Acc22), | |
| 160 | amount_of_sat_vars(bmc, 'benchmarks/paxos-3/', Acc22, Acc23), | |
| 161 | amount_of_sat_vars(bmc, 'benchmarks/lightbot/', Acc23, Acc24), | |
| 162 | amount_of_sat_vars(bmc, 'benchmarks/travel_agency/', Acc24, Acc25), | |
| 163 | amount_of_sat_vars(bmc, 'benchmarks/search_events/', Acc25, Acc26), | |
| 164 | amount_of_sat_vars(bmc, 'benchmarks/large_branching/', Acc26, Acc27), | |
| 165 | amount_of_sat_vars(bmc, 'benchmarks/r6_lights/', Acc27, Acc28), | |
| 166 | mean_of_list(Acc28, TotalMean), | |
| 167 | median_of_list(Acc28, TotalMedian), | |
| 168 | max_member(Max, Acc28), | |
| 169 | open('amount_of_sat_vars_bmc/total.txt', write, Stream), | |
| 170 | tell(Stream), | |
| 171 | format("Total mean: ~w~nTotal median: ~w~nTotal max: ~w~n", [TotalMean,TotalMedian,Max]), | |
| 172 | close(Stream). | |
| 173 | ||
| 174 | run_deadlock_benchmarks1 :- | |
| 175 | deadlock_timeout(Timeout), | |
| 176 | preferences:set_preference(time_out, Timeout), | |
| 177 | /*run_cbc_benchmarks(false, 'benchmarks_cbc_deadlock/abz16_m0/'), | |
| 178 | run_cbc_benchmarks(false, 'benchmarks_cbc_deadlock/abz16_m1/'), | |
| 179 | run_cbc_benchmarks(false, 'benchmarks_cbc_deadlock/abz16_m2/'), | |
| 180 | run_cbc_benchmarks(false, 'benchmarks_cbc_deadlock/abz16_m3/'),*/ | |
| 181 | run_cbc_benchmarks(false, 'benchmarks_cbc_deadlock/abz16_m4/'), | |
| 182 | run_cbc_benchmarks(false, 'benchmarks_cbc_deadlock/abz16_m5/'), | |
| 183 | run_cbc_benchmarks(false, 'benchmarks_cbc_deadlock/abz16_m6/'), | |
| 184 | run_cbc_benchmarks(false, 'benchmarks_cbc_deadlock/abz16_m7/'). | |
| 185 | ||
| 186 | run_deadlock_benchmarks2 :- | |
| 187 | deadlock_timeout(Timeout), | |
| 188 | preferences:set_preference(time_out, Timeout), | |
| 189 | run_cbc_benchmarks(false, 'benchmarks_cbc_deadlock/r0_geardoor/'), | |
| 190 | run_cbc_benchmarks(false, 'benchmarks_cbc_deadlock/r1_valve/'), | |
| 191 | run_cbc_benchmarks(false, 'benchmarks_cbc_deadlock/r2_outputs/'), | |
| 192 | run_cbc_benchmarks(false, 'benchmarks_cbc_deadlock/r3_sensors/'), | |
| 193 | run_cbc_benchmarks(false, 'benchmarks_cbc_deadlock/r4_handle/'), | |
| 194 | run_cbc_benchmarks(false, 'benchmarks_cbc_deadlock/r5_switch/'). | |
| 195 | %run_cbc_benchmarks(false, 'benchmarks_cbc_deadlock/r6_lights/'), % static contradiction | |
| 196 | ||
| 197 | run_deadlock_benchmarks3 :- | |
| 198 | deadlock_timeout(Timeout), | |
| 199 | preferences:set_preference(time_out, Timeout), | |
| 200 | run_cbc_benchmarks(false, 'benchmarks_cbc_deadlock/pm_m0_aai/'), | |
| 201 | run_cbc_benchmarks(false, 'benchmarks_cbc_deadlock/pm_m0_aat/'), | |
| 202 | run_cbc_benchmarks(false, 'benchmarks_cbc_deadlock/pm_m0_aoo/'), | |
| 203 | run_cbc_benchmarks(false, 'benchmarks_cbc_deadlock/pm_m0_voo/'). | |
| 204 | /* | |
| 205 | run_cbc_benchmarks(false, 'benchmarks_cbc_deadlock/pm_m2_aat/'), | |
| 206 | run_cbc_benchmarks(false, 'benchmarks_cbc_deadlock/pm_m2_vvi/'), | |
| 207 | run_cbc_benchmarks(false, 'benchmarks_cbc_deadlock/pm_m2_vvt/'), | |
| 208 | run_cbc_benchmarks(false, 'benchmarks_cbc_deadlock/pm_m3_aai/'), | |
| 209 | run_cbc_benchmarks(false, 'benchmarks_cbc_deadlock/pm_m3_aat/'), | |
| 210 | run_cbc_benchmarks(false, 'benchmarks_cbc_deadlock/pm_m3_vvi/'), | |
| 211 | run_cbc_benchmarks(false, 'benchmarks_cbc_deadlock/pm_m3_vvt/'), | |
| 212 | run_cbc_benchmarks(false, 'benchmarks_cbc_deadlock/pm_m4_aair/'), | |
| 213 | run_cbc_benchmarks(false, 'benchmarks_cbc_deadlock/pm_m4_aatr/'), | |
| 214 | run_cbc_benchmarks(false, 'benchmarks_cbc_deadlock/pm_m4_vvir/'), | |
| 215 | run_cbc_benchmarks(false, 'benchmarks_cbc_deadlock/pm_m4_vvtr/'),*/ | |
| 216 | ||
| 217 | run_deadlock_benchmarks4 :- | |
| 218 | deadlock_timeout(Timeout), | |
| 219 | preferences:set_preference(time_out, Timeout), | |
| 220 | run_cbc_benchmarks(false, 'benchmarks_cbc_deadlock/pm_m0_vvi/'), | |
| 221 | run_cbc_benchmarks(false, 'benchmarks_cbc_deadlock/pm_m0_vvt/'), | |
| 222 | run_cbc_benchmarks(false, 'benchmarks_cbc_deadlock/pm_m1_aoor/'), | |
| 223 | run_cbc_benchmarks(false, 'benchmarks_cbc_deadlock/pm_m1_voor/'), | |
| 224 | run_cbc_benchmarks(false, 'benchmarks_cbc_deadlock/pm_m2_aai/'). | |
| 225 | ||
| 226 | run_deadlock_benchmarks5 :- | |
| 227 | deadlock_timeout(Timeout), | |
| 228 | preferences:set_preference(time_out, Timeout), | |
| 229 | run_cbc_benchmarks(false, 'benchmarks_cbc_deadlock/simple-two-phase/'), | |
| 230 | run_cbc_benchmarks(false, 'benchmarks_cbc_deadlock/prisoners-4/'), | |
| 231 | run_cbc_benchmarks(false, 'benchmarks_cbc_deadlock/bakery/'), | |
| 232 | run_cbc_benchmarks(false, 'benchmarks_cbc_deadlock/paxos-3/'). | |
| 233 | ||
| 234 | run_deadlock_benchmarks6 :- | |
| 235 | deadlock_timeout(Timeout), | |
| 236 | preferences:set_preference(time_out, Timeout), | |
| 237 | run_cbc_benchmarks(false, 'benchmarks_cbc_deadlock/lightbot/'), | |
| 238 | run_cbc_benchmarks(false, 'benchmarks_cbc_deadlock/travel_agency/'), | |
| 239 | run_cbc_benchmarks(false, 'benchmarks_cbc_deadlock/search_events/'), | |
| 240 | run_cbc_benchmarks(false, 'benchmarks_cbc_deadlock/large_branching/'). | |
| 241 | ||
| 242 | run_cbc_benchmarks1 :- | |
| 243 | inductive_inv_timeout(Timeout), | |
| 244 | preferences:set_preference(time_out, Timeout), | |
| 245 | /*run_cbc_benchmarks(false, 'benchmarks_inductive_inv/abz16_m0/'), | |
| 246 | run_cbc_benchmarks(false, 'benchmarks_inductive_inv/abz16_m1/'), | |
| 247 | run_cbc_benchmarks(false, 'benchmarks_inductive_inv/abz16_m2/'), | |
| 248 | run_cbc_benchmarks(false, 'benchmarks_inductive_inv/abz16_m3/'),*/ | |
| 249 | run_cbc_benchmarks(false, 'benchmarks_inductive_inv/abz16_m4/'), | |
| 250 | run_cbc_benchmarks(false, 'benchmarks_inductive_inv/abz16_m5/'), | |
| 251 | run_cbc_benchmarks(false, 'benchmarks_inductive_inv/abz16_m6/'), | |
| 252 | run_cbc_benchmarks(false, 'benchmarks_inductive_inv/abz16_m7/'). | |
| 253 | ||
| 254 | run_cbc_benchmarks2 :- | |
| 255 | inductive_inv_timeout(Timeout), | |
| 256 | preferences:set_preference(time_out, Timeout), | |
| 257 | run_cbc_benchmarks(false, 'benchmarks_inductive_inv/r0_geardoor/'), | |
| 258 | run_cbc_benchmarks(false, 'benchmarks_inductive_inv/r1_valve/'), | |
| 259 | run_cbc_benchmarks(false, 'benchmarks_inductive_inv/r2_outputs/'), | |
| 260 | run_cbc_benchmarks(false, 'benchmarks_inductive_inv/r3_sensors/'), | |
| 261 | run_cbc_benchmarks(false, 'benchmarks_inductive_inv/r4_handle/'), | |
| 262 | run_cbc_benchmarks(false, 'benchmarks_inductive_inv/r5_switch/'), | |
| 263 | run_cbc_benchmarks(false, 'benchmarks_inductive_inv/r6_lights/'). | |
| 264 | ||
| 265 | run_cbc_benchmarks3 :- | |
| 266 | inductive_inv_timeout(Timeout), | |
| 267 | preferences:set_preference(time_out, Timeout), | |
| 268 | run_cbc_benchmarks(false, 'benchmarks_inductive_inv/pm_m0_aai/'), | |
| 269 | run_cbc_benchmarks(false, 'benchmarks_inductive_inv/pm_m0_aat/'), | |
| 270 | run_cbc_benchmarks(false, 'benchmarks_inductive_inv/pm_m0_aoo/'), | |
| 271 | run_cbc_benchmarks(false, 'benchmarks_inductive_inv/pm_m0_voo/'). | |
| 272 | /*run_cbc_benchmarks(false, 'benchmarks_inductive_inv/pm_m2_aat/'), | |
| 273 | run_cbc_benchmarks(false, 'benchmarks_inductive_inv/pm_m2_vvi/'), | |
| 274 | run_cbc_benchmarks(false, 'benchmarks_inductive_inv/pm_m2_vvt/'), | |
| 275 | run_cbc_benchmarks(false, 'benchmarks_inductive_inv/pm_m3_aai/'), | |
| 276 | run_cbc_benchmarks(false, 'benchmarks_inductive_inv/pm_m3_aat/'), | |
| 277 | run_cbc_benchmarks(false, 'benchmarks_inductive_inv/pm_m3_vvi/'), | |
| 278 | run_cbc_benchmarks(false, 'benchmarks_inductive_inv/pm_m3_vvt/'), | |
| 279 | run_cbc_benchmarks(false, 'benchmarks_inductive_inv/pm_m4_aair/'), | |
| 280 | run_cbc_benchmarks(false, 'benchmarks_inductive_inv/pm_m4_aatr/'), | |
| 281 | run_cbc_benchmarks(false, 'benchmarks_inductive_inv/pm_m4_vvir/'), | |
| 282 | run_cbc_benchmarks(false, 'benchmarks_inductive_inv/pm_m4_vvtr/'),*/ | |
| 283 | ||
| 284 | run_cbc_benchmarks4 :- | |
| 285 | inductive_inv_timeout(Timeout), | |
| 286 | preferences:set_preference(time_out, Timeout), | |
| 287 | run_cbc_benchmarks(false, 'benchmarks_inductive_inv/pm_m0_vvi/'), | |
| 288 | run_cbc_benchmarks(false, 'benchmarks_inductive_inv/pm_m0_vvt/'), | |
| 289 | run_cbc_benchmarks(false, 'benchmarks_inductive_inv/pm_m1_aoor/'), | |
| 290 | run_cbc_benchmarks(false, 'benchmarks_inductive_inv/pm_m1_voor/'), | |
| 291 | run_cbc_benchmarks(false, 'benchmarks_inductive_inv/pm_m2_aai/'). | |
| 292 | ||
| 293 | run_cbc_benchmarks5 :- | |
| 294 | inductive_inv_timeout(Timeout), | |
| 295 | preferences:set_preference(time_out, Timeout), | |
| 296 | %run_cbc_benchmarks(false, 'benchmarks_inductive_inv/simple-two-phase/'), % static contradiction | |
| 297 | run_cbc_benchmarks(false, 'benchmarks_inductive_inv/prisoners-4/'), | |
| 298 | run_cbc_benchmarks(false, 'benchmarks_inductive_inv/bakery/'), | |
| 299 | run_cbc_benchmarks(false, 'benchmarks_inductive_inv/paxos-3/'). | |
| 300 | ||
| 301 | run_cbc_benchmarks6 :- | |
| 302 | inductive_inv_timeout(Timeout), | |
| 303 | preferences:set_preference(time_out, Timeout), | |
| 304 | run_cbc_benchmarks(false, 'benchmarks_inductive_inv/lightbot/'), | |
| 305 | run_cbc_benchmarks(false, 'benchmarks_inductive_inv/travel_agency/'), | |
| 306 | run_cbc_benchmarks(false, 'benchmarks_inductive_inv/search_events/'), | |
| 307 | run_cbc_benchmarks(false, 'benchmarks_inductive_inv/large_branching/'). | |
| 308 | ||
| 309 | ||
| 310 | run_bmc_benchmarks1 :- | |
| 311 | bmc_timeout(Timeout), | |
| 312 | preferences:set_preference(time_out, Timeout), | |
| 313 | %run_bmc_benchmarks(false, 'benchmarks/paxos-5/'), | |
| 314 | %run_bmc_benchmarks(false, 'benchmarks/abz16_m0/'), | |
| 315 | /*run_bmc_benchmarks(false, 'benchmarks/abz16_m1/'), | |
| 316 | run_bmc_benchmarks(false, 'benchmarks/abz16_m2/'), | |
| 317 | run_bmc_benchmarks(false, 'benchmarks/abz16_m3/'),*/ | |
| 318 | run_bmc_benchmarks(false, 'benchmarks/abz16_m6/'), | |
| 319 | run_bmc_benchmarks(false, 'benchmarks/abz16_m7/'), | |
| 320 | run_bmc_benchmarks(false, 'benchmarks/abz16_m4/'), | |
| 321 | run_bmc_benchmarks(false, 'benchmarks/abz16_m5/'). | |
| 322 | ||
| 323 | run_bmc_benchmarks2 :- | |
| 324 | bmc_timeout(Timeout), | |
| 325 | preferences:set_preference(time_out, Timeout), | |
| 326 | run_bmc_benchmarks(false, 'benchmarks/r4_handle/'), | |
| 327 | run_bmc_benchmarks(false, 'benchmarks/r5_switch/'), | |
| 328 | run_bmc_benchmarks(false, 'benchmarks/r6_lights/'), | |
| 329 | run_bmc_benchmarks(false, 'benchmarks/r0_geardoor/'), | |
| 330 | run_bmc_benchmarks(false, 'benchmarks/r1_valve/'), | |
| 331 | run_bmc_benchmarks(false, 'benchmarks/r2_outputs/'), | |
| 332 | run_bmc_benchmarks(false, 'benchmarks/r3_sensors/'). | |
| 333 | ||
| 334 | run_bmc_benchmarks3 :- | |
| 335 | bmc_timeout(Timeout), | |
| 336 | preferences:set_preference(time_out, Timeout), | |
| 337 | run_bmc_benchmarks(false, 'benchmarks/pm_m0_aai/'), | |
| 338 | run_bmc_benchmarks(false, 'benchmarks/pm_m0_aat/'), | |
| 339 | run_bmc_benchmarks(false, 'benchmarks/pm_m0_aoo/'), | |
| 340 | run_bmc_benchmarks(false, 'benchmarks/pm_m0_voo/'), | |
| 341 | run_bmc_benchmarks(false, 'benchmarks/pm_m0_vvi/'). | |
| 342 | ||
| 343 | run_bmc_benchmarks4 :- | |
| 344 | bmc_timeout(Timeout), | |
| 345 | preferences:set_preference(time_out, Timeout), | |
| 346 | run_bmc_benchmarks(false, 'benchmarks/pm_m0_vvt/'), | |
| 347 | run_bmc_benchmarks(false, 'benchmarks/pm_m1_aoor/'), | |
| 348 | run_bmc_benchmarks(false, 'benchmarks/pm_m1_voor/'), | |
| 349 | run_bmc_benchmarks(false, 'benchmarks/pm_m2_aai/'). | |
| 350 | /*run_bmc_benchmarks(false, 'benchmarks/pm_m2_aat/'), | |
| 351 | run_bmc_benchmarks(false, 'benchmarks/pm_m2_vvi/'), | |
| 352 | run_bmc_benchmarks(false, 'benchmarks/pm_m2_vvt/'), | |
| 353 | run_bmc_benchmarks(false, 'benchmarks/pm_m3_aai/'), | |
| 354 | run_bmc_benchmarks(false, 'benchmarks/pm_m3_aat/'), | |
| 355 | run_bmc_benchmarks(false, 'benchmarks/pm_m3_vvi/'), | |
| 356 | run_bmc_benchmarks(false, 'benchmarks/pm_m3_vvt/'), | |
| 357 | run_bmc_benchmarks(false, 'benchmarks/pm_m4_aair/'), | |
| 358 | run_bmc_benchmarks(false, 'benchmarks/pm_m4_aatr/'), | |
| 359 | run_bmc_benchmarks(false, 'benchmarks/pm_m4_vvir/'), | |
| 360 | run_bmc_benchmarks(false, 'benchmarks/pm_m4_vvtr/')*/ | |
| 361 | ||
| 362 | run_bmc_benchmarks5 :- | |
| 363 | bmc_timeout(Timeout), | |
| 364 | preferences:set_preference(time_out, Timeout), | |
| 365 | run_bmc_benchmarks(false, 'benchmarks/simple-two-phase/'), | |
| 366 | run_bmc_benchmarks(false, 'benchmarks/lightbot/'), | |
| 367 | run_bmc_benchmarks(false, 'benchmarks/travel_agency/'), | |
| 368 | run_bmc_benchmarks(false, 'benchmarks/search_events/'). | |
| 369 | ||
| 370 | run_bmc_benchmarks6 :- | |
| 371 | bmc_timeout(Timeout), | |
| 372 | preferences:set_preference(time_out, Timeout), | |
| 373 | run_bmc_benchmarks(false, 'benchmarks/large_branching/'), | |
| 374 | run_bmc_benchmarks(false, 'benchmarks/prisoners-4/'), | |
| 375 | run_bmc_benchmarks(false, 'benchmarks/bakery/'), | |
| 376 | run_bmc_benchmarks(false, 'benchmarks/paxos-3/'). | |
| 377 | ||
| 378 | select_machine_file_path(FilePaths, MachineFilePath, BenchmarkFilePaths) :- | |
| 379 | select(_-MachineFilePath, FilePaths, BenchmarkFilePaths), | |
| 380 | ( atom_concat(_, '.eventb', MachineFilePath) | |
| 381 | ; atom_concat(_, '.mch', MachineFilePath) | |
| 382 | ; atom_concat(_, '.tla', MachineFilePath) | |
| 383 | ). | |
| 384 | ||
| 385 | load_b_eventb_or_tla(MachineFilePath) :- | |
| 386 | ( is_eventb_machine(MachineFilePath) | |
| 387 | -> b_load_eventb_project(MachineFilePath) | |
| 388 | ; is_tla_file(MachineFilePath) | |
| 389 | -> call_tla2b_parser(MachineFilePath), | |
| 390 | atom_concat(PrefixPath, '.tla', MachineFilePath), | |
| 391 | atom_concat(PrefixPath, '.prob', BMachinePath), | |
| 392 | b_load_machine_probfile(BMachinePath) | |
| 393 | ; b_load_machine_from_file(MachineFilePath) | |
| 394 | ), | |
| 395 | b_machine_precompile. | |
| 396 | ||
| 397 | amount_of_sat_vars(BenchmarkName, FolderPath, Acc, NewAcc) :- | |
| 398 | write('Eval amount of sat variables for '), write(FolderPath), nl, | |
| 399 | directory_exists(FolderPath), | |
| 400 | file_members_of_directory(FolderPath, FilePaths), | |
| 401 | select_machine_file_path(FilePaths, MachineFilePath, TBenchmarkFilePaths), | |
| 402 | findall(FilePath, (member(_-FilePath, TBenchmarkFilePaths), atom_concat(_, '.eval', FilePath)), BenchmarkFilePaths), | |
| 403 | load_b_eventb_or_tla(MachineFilePath), | |
| 404 | amount_of_sat_vars_for_benchmark(BenchmarkFilePaths, AmountOfSatVars), | |
| 405 | append(Acc, AmountOfSatVars, NewAcc), | |
| 406 | eval_amount_of_sat_vars(BenchmarkName, AmountOfSatVars). | |
| 407 | ||
| 408 | mean_of_list([], M) :- | |
| 409 | !, | |
| 410 | M = 0. | |
| 411 | mean_of_list(L, M) :- | |
| 412 | length(L, Len), | |
| 413 | sumlist(L, Sum), | |
| 414 | M is Sum / Len. | |
| 415 | ||
| 416 | median_of_list(L, M) :- | |
| 417 | length(L, Len), | |
| 418 | sort(L, LS), | |
| 419 | ( LS = [E] | |
| 420 | -> M = E | |
| 421 | ; Len21 is floor(Len / 2), | |
| 422 | Len22 is ceiling(Len / 2), | |
| 423 | ( Len21 \== Len22 | |
| 424 | -> nth1(Len22, L, M) | |
| 425 | ; nth1(Len21, L, M1), | |
| 426 | Len211 is Len21 + 1, | |
| 427 | nth1(Len211, L, M2), | |
| 428 | M is (M1+M2)/2 | |
| 429 | ) | |
| 430 | ). | |
| 431 | ||
| 432 | eval_amount_of_sat_vars(BenchmarkName, AmountOfSatVars) :- | |
| 433 | bmachine:b_machine_name(MachineName), | |
| 434 | atom_concat(MachineName, 'amount_of_sat_vars.txt', OutPath1), | |
| 435 | atom_concat('amount_of_sat_vars_', BenchmarkName, OutFolder1), | |
| 436 | atom_concat(OutFolder1, '/', OutFolder), | |
| 437 | atom_concat(OutFolder, OutPath1, OutPath), | |
| 438 | mean_of_list(AmountOfSatVars, MeanAmountOfSatVars), | |
| 439 | median_of_list(AmountOfSatVars, MedianAmountOfSatVars), | |
| 440 | open(OutPath, write, Stream), | |
| 441 | tell(Stream), | |
| 442 | format("AmountOfSatVarsList: ~w~nMean: ~w~nMedian: ~w~n", [AmountOfSatVars, MeanAmountOfSatVars, MedianAmountOfSatVars]), | |
| 443 | close(Stream). | |
| 444 | ||
| 445 | amount_of_sat_vars_for_benchmark([], []). | |
| 446 | amount_of_sat_vars_for_benchmark([BenchmarkFilePath|T], [AmountOfSatVars|TAmountOfSatVars]) :- | |
| 447 | open(BenchmarkFilePath, read, Stream), | |
| 448 | read(Stream, Constraint), | |
| 449 | close(Stream), | |
| 450 | cdclt_solver:get_amount_of_sat_variables(Constraint, AmountOfSatVars), | |
| 451 | amount_of_sat_vars_for_benchmark(T, TAmountOfSatVars). | |
| 452 | ||
| 453 | run_cbc_benchmarks(UseIdlSolver, FolderPath) :- | |
| 454 | directory_exists(FolderPath), | |
| 455 | file_members_of_directory(FolderPath, FilePaths), | |
| 456 | select_machine_file_path(FilePaths, MachineFilePath, TBenchmarkFilePaths), | |
| 457 | findall(FileName-FilePath, (member(FileName-FilePath, TBenchmarkFilePaths), atom_concat(_, '.eval', FilePath)), BenchmarkFilePaths), | |
| 458 | load_b_eventb_or_tla(MachineFilePath), | |
| 459 | run_cbc_benchmarks(UseIdlSolver, FolderPath, BenchmarkFilePaths). | |
| 460 | ||
| 461 | run_cbc_benchmarks(_, _, []). | |
| 462 | run_cbc_benchmarks(UseIdlSolver, FolderPath, [FileName-BenchmarkFilePath|T]) :- | |
| 463 | open(BenchmarkFilePath, read, Stream), | |
| 464 | read(Stream, Constraint), | |
| 465 | close(Stream), | |
| 466 | retractall(cdclt_sat_solver:incremental_mode), | |
| 467 | run_cbc_benchmark(UseIdlSolver, FolderPath, FileName-BenchmarkFilePath, Constraint), | |
| 468 | run_cbc_benchmarks(UseIdlSolver, FolderPath, T). | |
| 469 | ||
| 470 | run_cbc_benchmark(UseIdlSolver, FolderPath, FileName-BenchmarkFilePath, Constraint) :- | |
| 471 | inductive_inv_timeout(Timeout), | |
| 472 | preferences:set_preference(time_out, Timeout), | |
| 473 | set_preference(cdclt_use_idl_theory_solver, false), | |
| 474 | set_preference(cdclt_perform_static_analysis, false), | |
| 475 | set_preference(cdclt_perform_symmetry_breaking, true), | |
| 476 | cdclt_solver:init, | |
| 477 | write('Solve with Sym-Raw-SMT..'),nl, | |
| 478 | writeq(BenchmarkFilePath),nl, | |
| 479 | statistics(walltime, [StartCdcltRawSym|_]), | |
| 480 | cdclt_solve_predicate(Constraint, _, ResCdcltRawSym), | |
| 481 | statistics(walltime, [StopCdcltRawSym|_]), | |
| 482 | (cdclt_sat_solver:restarts(RestartsCdcltRawSym); RestartsCdcltRawSym = 0), | |
| 483 | TimeCdcltRawSym is StopCdcltRawSym - StartCdcltRawSym, | |
| 484 | nl,nl,write(ResCdcltRawSym),nl,nl, | |
| 485 | %% | |
| 486 | write('done.'), nl, | |
| 487 | set_preference(cdclt_perform_static_analysis, true), | |
| 488 | cdclt_solver:init, | |
| 489 | write('Solve with Sym-SMT..'),nl, | |
| 490 | writeq(BenchmarkFilePath),nl, | |
| 491 | statistics(walltime, [StartCdclt|_]), | |
| 492 | cdclt_solve_predicate(Constraint, _, ResCdclt), | |
| 493 | statistics(walltime, [StopCdclt|_]), | |
| 494 | (cdclt_sat_solver:restarts(RestartsCdclt); RestartsCdclt = 0), | |
| 495 | TimeCdclt is StopCdclt - StartCdclt, | |
| 496 | nl,nl,write(ResCdclt),nl,nl, | |
| 497 | %% | |
| 498 | write('done.'), nl, | |
| 499 | preferences:set_preference(time_out, Timeout), | |
| 500 | ( UseIdlSolver | |
| 501 | -> set_preference(cdclt_perform_symmetry_breaking,false), | |
| 502 | set_preference(cdclt_use_idl_theory_solver,true), | |
| 503 | cdclt_solver:init, | |
| 504 | write('Solve with IDL-SMT..'),nl, | |
| 505 | writeq(BenchmarkFilePath),nl, | |
| 506 | statistics(walltime, [StartCdcltIdl|_]), | |
| 507 | cdclt_solve_predicate(Constraint, _, ResCdcltIdl), | |
| 508 | statistics(walltime, [StopCdcltIdl|_]), | |
| 509 | (cdclt_sat_solver:restarts(RestartsCdcltIdl); RestartsCdcltIdl = 0), | |
| 510 | TimeCdcltIdl is StopCdcltIdl - StartCdcltIdl, | |
| 511 | set_preference(cdclt_use_idl_theory_solver,false), | |
| 512 | set_preference(cdclt_perform_symmetry_breaking,true) | |
| 513 | ; TimeCdcltIdl = 0, | |
| 514 | RestartsCdcltIdl = 0, | |
| 515 | ResCdcltIdl = none | |
| 516 | ), | |
| 517 | nl,nl,write(ResCdcltIdl),nl,nl, | |
| 518 | write('done.'), nl, | |
| 519 | %% | |
| 520 | preferences:set_preference(time_out, Timeout), | |
| 521 | set_preference(cdclt_perform_symmetry_breaking,false), | |
| 522 | cdclt_solver:init, | |
| 523 | write('Solve with SMT..'),nl, | |
| 524 | writeq(BenchmarkFilePath),nl, | |
| 525 | statistics(walltime, [StartCdcltNoSym|_]), | |
| 526 | cdclt_solve_predicate(Constraint, _, ResCdcltNoSym), | |
| 527 | statistics(walltime, [StopCdcltNoSym|_]), | |
| 528 | (cdclt_sat_solver:restarts(RestartsCdcltNoSym); RestartsCdcltNoSym = 0), | |
| 529 | TimeCdcltNoSym is StopCdcltNoSym - StartCdcltNoSym, | |
| 530 | nl,nl,write(ResCdcltNoSym),nl,nl, | |
| 531 | write('done.'), nl, | |
| 532 | preferences:set_preference(time_out, Timeout), | |
| 533 | %% | |
| 534 | set_preference(cdclt_perform_static_analysis,false), | |
| 535 | set_preference(cdclt_perform_symmetry_breaking,false), | |
| 536 | cdclt_solver:init, | |
| 537 | write('Solve with Raw-SMT..'),nl, | |
| 538 | writeq(BenchmarkFilePath),nl, | |
| 539 | statistics(walltime, [StartCdcltRaw|_]), | |
| 540 | cdclt_solve_predicate(Constraint, _, ResCdcltRaw), | |
| 541 | statistics(walltime, [StopCdcltRaw|_]), | |
| 542 | (cdclt_sat_solver:restarts(RestartsCdcltRaw); RestartsCdcltRaw = 0), | |
| 543 | TimeCdcltRaw is StopCdcltRaw - StartCdcltRaw, | |
| 544 | nl,nl,write(ResCdcltRaw),nl,nl, | |
| 545 | write('done.'), nl, | |
| 546 | preferences:set_preference(time_out, Timeout), | |
| 547 | %% | |
| 548 | write('Solve with Z3..'),nl, | |
| 549 | writeq(BenchmarkFilePath),nl, | |
| 550 | %translate:print_bexpr(Constraint),nl, | |
| 551 | statistics(walltime, [StartZ3|_]), | |
| 552 | smt_solve_predicate(z3,Constraint, _, ResZ3), | |
| 553 | %ResZ3 = no_solution_found(solver_answered_unknown), | |
| 554 | statistics(walltime, [StopZ3|_]), | |
| 555 | TimeZ3 is StopZ3 - StartZ3, | |
| 556 | nl,nl,write(ResZ3),nl,nl, | |
| 557 | preferences:set_preference(time_out, Timeout), | |
| 558 | %% | |
| 559 | write('Solve with ProB..'),nl, | |
| 560 | writeq(BenchmarkFilePath),nl, | |
| 561 | statistics(walltime, [StartProB|_]), | |
| 562 | solve_predicate(Constraint, _, ResProB), | |
| 563 | %ResProB = no_solution_found(solver_answered_unknown), | |
| 564 | statistics(walltime, [StopProB|_]), | |
| 565 | TimeProB is StopProB - StartProB, | |
| 566 | nl,nl,write(ResProB),nl,nl, | |
| 567 | write('done.'), nl, | |
| 568 | !, | |
| 569 | 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). | |
| 570 | ||
| 571 | 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) :- | |
| 572 | atom_concat(FileNameNoExt, '.eval', FileName), | |
| 573 | atom_concat('benchmark_results_', FileNameNoExt, TResultsPath), | |
| 574 | atom_concat(TResultsPath, '.txt', TTResultsPath), | |
| 575 | atom_concat(FolderPath, TTResultsPath, ResultsPath), | |
| 576 | open(ResultsPath, write, Stream), | |
| 577 | tell(Stream), | |
| 578 | writeq(BenchmarkFilePath),nl,nl, | |
| 579 | format("CDCLT-Res: ~w~nCDCLT-Time: ~w~nCDCLT-Restarts: ~w~n", [ResCdclt,TimeCdclt,RestartsCdclt]), | |
| 580 | format("CDCLT-No-Sym-Res: ~w~nCDCLT-No-Sym-Time: ~w~nCDCLT-No-Sym-Restarts: ~w~n", [ResCdcltNoSym,TimeCdcltNoSym,RestartsCdcltNoSym]), | |
| 581 | format("CDCLT-Idl-Res: ~w~nCDCLT-Idl-Time: ~w~nCDCLT-Idl-Restarts: ~w~n", [ResCdcltIdl,TimeCdcltIdl,RestartsCdcltIdl]), | |
| 582 | format("CDCLT-Raw-Res: ~w~nCDCLT-Raw-Time: ~w~nCDCLT-Raw-Restarts: ~w~n", [ResCdcltRaw,TimeCdcltRaw,RestartsCdcltRaw]), | |
| 583 | format("CDCLT-Sym-Raw-Res: ~w~nCDCLT-Sym-Raw-Time: ~w~nCDCLT-Sym-Raw-Restarts: ~w~n", [ResCdcltRawSym,TimeCdcltRawSym,RestartsCdcltRawSym]), | |
| 584 | format("Z3-Res: ~w~nZ3-Time: ~w~n", [ResZ3,TimeZ3]), | |
| 585 | format("ProB-Res: ~w~nProB-Time: ~w~n", [ResProB,TimeProB]), | |
| 586 | close(Stream), | |
| 587 | !. | |
| 588 | ||
| 589 | int_range(C, B, R) :- | |
| 590 | C == B, | |
| 591 | !, | |
| 592 | R = [C]. | |
| 593 | int_range(C, B, [C|T]) :- | |
| 594 | C1 is C + 1, | |
| 595 | int_range(C1, B, T). | |
| 596 | ||
| 597 | get_file_paths_from_config(ConfigPath, MachineFile, ConstraintPaths, Description, MachineName) :- | |
| 598 | open(ConfigPath, read, Stream), | |
| 599 | read(Stream, Config), | |
| 600 | close(Stream), | |
| 601 | Config = benchmark_config(Description, MachineFile, MachineName, MaxBound), | |
| 602 | int_range(0, MaxBound, KRange), | |
| 603 | findall(ConstraintPath, | |
| 604 | (member(K, KRange), atom_concat(MachineName, '_monolithic_bmc_k_', T1), | |
| 605 | number_codes(K, CK), atom_codes(AK, CK), | |
| 606 | atom_concat(T1, AK, T2), atom_concat(T2, '.eval', ConstraintPath)), | |
| 607 | ConstraintPaths). | |
| 608 | ||
| 609 | is_eventb_machine(MachineFile) :- | |
| 610 | atom_concat(_, '.eventb', MachineFile). | |
| 611 | ||
| 612 | is_tla_file(File) :- | |
| 613 | atom_concat(_, '.tla', File). | |
| 614 | ||
| 615 | write_to_csv(SolverName, MachineName, Data) :- | |
| 616 | atom_concat('benchmarks_cdclt_journal/', MachineName, Path1), | |
| 617 | atom_concat(Path1, '_results_', Path2), | |
| 618 | atom_concat(Path2, SolverName, Path3), | |
| 619 | atom_concat(Path3, '.csv', EvalFilePath), | |
| 620 | nl,nl,write('csv'),nl, | |
| 621 | write(EvalFilePath),nl,nl, | |
| 622 | open(EvalFilePath, write, Stream), | |
| 623 | tell(Stream), | |
| 624 | format("ConstraintPath,Result,Time (ms)~n", []), | |
| 625 | write_to_csv_stream(SolverName, Stream, Data), | |
| 626 | close(Stream). | |
| 627 | ||
| 628 | write_to_csv_stream(_, _, []). | |
| 629 | write_to_csv_stream(SolverName, Stream, [(ConstraintPath,Time)|T]) :- | |
| 630 | ( benchmark_result(SolverName, ConstraintPath, Result) | |
| 631 | -> true | |
| 632 | ; Result = no_solution_found | |
| 633 | ), | |
| 634 | format("~w,~w,~w~n", [ConstraintPath,Result,Time]), | |
| 635 | write_to_csv_stream(SolverName, Stream, T). | |
| 636 | ||
| 637 | eval_benchmark_data_csv(MachineName, Description, Data) :- | |
| 638 | format("Evaluate benchmarks ~w for detailed CSV~n", [Description]), | |
| 639 | findall((ConstraintPath,TimeZ3), member((ConstraintPath,TimeZ3,_,_,_,_,_,_,_,_,_,_), Data), DataZ3), | |
| 640 | findall((ConstraintPath,TimeCdclt), member((ConstraintPath,_,TimeCdclt,_,_,_,_,_,_,_,_,_), Data), DataCdclt), | |
| 641 | findall((ConstraintPath,TimeCdcltRaw), member((ConstraintPath,_,_,TimeCdcltRaw,_,_,_,_,_,_,_,_,_), Data), DataCdcltRaw), | |
| 642 | %findall((ConstraintPath,TimeCdcltIdl), member((ConstraintPath,_,_,_,TimeCdcltIdl,_,_,_,_,_,_,_,_), Data), DataCdcltIdl), | |
| 643 | findall((ConstraintPath,TimeCdcltNoSym), member((ConstraintPath,_,_,_,_,TimeCdcltNoSym,_,_,_,_,_,_,_), Data), DataCdcltNoSym), | |
| 644 | findall((ConstraintPath,TimeCdcltRawSym), member((ConstraintPath,_,_,_,_,_,TimeCdcltRawSym,_,_,_,_,_,_), Data), DataCdcltRawSym), | |
| 645 | findall((ConstraintPath,TimeProB), member((ConstraintPath,_,_,_,_,_,_,TimeProB,_,_,_,_,_), Data), DataProB), | |
| 646 | write_to_csv(z3, MachineName, DataZ3), | |
| 647 | write_to_csv(prob, MachineName, DataProB), | |
| 648 | write_to_csv(smt, MachineName, DataCdcltNoSym), | |
| 649 | write_to_csv(sym_smt, MachineName, DataCdclt), | |
| 650 | write_to_csv(raw_smt, MachineName, DataCdcltRaw), | |
| 651 | write_to_csv(sym_raw_smt, MachineName, DataCdcltRawSym). | |
| 652 | ||
| 653 | eval_benchmark_data(MachineName, Description, Data) :- | |
| 654 | format("Evaluate benchmarks ~w~n", [Description]), | |
| 655 | findall(TimeZ3, member((_,TimeZ3,_,_,_,_,_,_,_,_,_,_), Data), TimesZ3), | |
| 656 | findall(TimeCdclt, member((_,_,TimeCdclt,_,_,_,_,_,_,_,_,_), Data), TimesCdclt), | |
| 657 | findall(TimeCdcltRaw, member((_,_,_,TimeCdcltRaw,_,_,_,_,_,_,_,_,_), Data), TimesCdcltRaw), | |
| 658 | findall(TimeCdcltIdl, member((_,_,_,_,TimeCdcltIdl,_,_,_,_,_,_,_,_), Data), TimesCdcltIdl), | |
| 659 | findall(TimeCdcltNoSym, member((_,_,_,_,_,TimeCdcltNoSym,_,_,_,_,_,_,_), Data), TimesCdcltNoSym), | |
| 660 | findall(TimeCdcltRawSym, member((_,_,_,_,_,_,TimeCdcltRawSym,_,_,_,_,_,_), Data), TimesCdcltRawSym), | |
| 661 | findall(TimeProB, member((_,_,_,_,_,_,_,TimeProB,_,_,_,_,_), Data), TimesProB), | |
| 662 | findall(RestartCdclt, member((_,_,_,_,_,_,_,_,RestartCdclt,_,_,_,_), Data), RestartsCdclt), | |
| 663 | findall(RestartCdcltRaw, member((_,_,_,_,_,_,_,_,_,RestartCdcltRaw,_,_), Data), RestartsCdcltRaw), | |
| 664 | findall(RestartCdcltIdl, member((_,_,_,_,_,_,_,_,_,_,RestartCdcltIdl,_,_), Data), RestartsCdcltIdl), | |
| 665 | findall(RestartCdcltNoSym, member((_,_,_,_,_,_,_,_,_,_,_,RestartCdcltNoSym,_), Data), RestartsCdcltNoSym), | |
| 666 | findall(RestartCdcltRawSym, member((_,_,_,_,_,_,_,_,_,_,_,_,RestartCdcltRawSym), Data), RestartsCdcltRawSym), | |
| 667 | sumlist(TimesZ3, TimeZ3), | |
| 668 | sumlist(TimesCdclt, TimeCdclt), | |
| 669 | sumlist(TimesCdcltRaw, TimeCdcltRaw), | |
| 670 | sumlist(TimesCdcltIdl, TimeCdcltIdl), | |
| 671 | sumlist(TimesCdcltNoSym, TimeCdcltNoSym), | |
| 672 | sumlist(TimesCdcltRawSym, TimeCdcltRawSym), | |
| 673 | sumlist(TimesProB, TimeProB), | |
| 674 | sumlist(RestartsCdclt, RestartCdclt), | |
| 675 | sumlist(RestartsCdcltRaw, RestartCdcltRaw), | |
| 676 | sumlist(RestartsCdcltIdl, RestartCdcltIdl), | |
| 677 | sumlist(RestartsCdcltNoSym, RestartCdcltNoSym), | |
| 678 | sumlist(RestartsCdcltRawSym, RestartCdcltRawSym), | |
| 679 | atom_concat('benchmarks_cdclt_journal/', MachineName, Path1), | |
| 680 | atom_concat(Path1, '_results.txt', EvalFilePath), | |
| 681 | nl,nl,write('eval'),nl, | |
| 682 | write(EvalFilePath),nl,nl, | |
| 683 | open(EvalFilePath, write, Stream), | |
| 684 | tell(Stream), | |
| 685 | 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]), | |
| 686 | findall(TO, (solved_constraints(A,B), TO = solved_constraints(A,B)), TOs), | |
| 687 | (member(solved_constraints(prob,SolvedProB), TOs); SolvedProB = 0), | |
| 688 | (member(solved_constraints(z3,SolvedZ3), TOs); SolvedZ3 = 0), | |
| 689 | (member(solved_constraints(smt,SolvedSMT), TOs); SolvedSMT = 0), | |
| 690 | (member(solved_constraints(raw_smt,SolvedRawSMT), TOs); SolvedRawSMT = 0), | |
| 691 | (member(solved_constraints(sym_smt,SolvedSymSMT), TOs); SolvedSymSMT = 0), | |
| 692 | (member(solved_constraints(sym_raw_smt,SolvedSymRawSMT), TOs); SolvedSymRawSMT = 0), | |
| 693 | 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]), | |
| 694 | nl, write(TOs), nl, | |
| 695 | close(Stream). | |
| 696 | ||
| 697 | run_bmc_benchmarks(UseIdlSolver, DirPath) :- | |
| 698 | retractall(solved_constraints(_,_)), | |
| 699 | retractall(benchmark_result(_,_,_)), | |
| 700 | atom_concat(DirPath, 'benchmark_config.pl', ConfigPath), | |
| 701 | get_file_paths_from_config(ConfigPath, MachineFile, ConstraintPaths, Description, MachineName), | |
| 702 | format("Run benchmarks ~w~n", [Description]), | |
| 703 | atom_concat(DirPath, MachineFile, MachinePath), | |
| 704 | load_b_eventb_or_tla(MachinePath), | |
| 705 | maplist(atom_concat(DirPath), ConstraintPaths, FullConstraintPaths), | |
| 706 | get_preference(time_out, Timeout), | |
| 707 | retractall(cdclt_sat_solver:incremental_mode), | |
| 708 | benchmark_constraints(UseIdlSolver, Timeout, FullConstraintPaths, [], Data), | |
| 709 | retractall(cdclt_sat_solver:memoize_backjump_clause(_, _, _)), | |
| 710 | eval_benchmark_data(MachineName, Description, Data), | |
| 711 | eval_benchmark_data_csv(MachineName, Description, Data). | |
| 712 | ||
| 713 | benchmark_constraints(_, _, [], Acc, Acc). | |
| 714 | benchmark_constraints(UseIdlSolver, Timeout, [ConstraintPath|T], Acc, Data) :- | |
| 715 | benchmark_constraint(UseIdlSolver, Timeout, ConstraintPath, TimeZ3, TimeCdclt, TimeCdcltRaw, TimeCdcltIdl, TimeCdcltNoSym, TimeCdcltRawSym, TimeProB, RestartsCdclt, RestartsCdcltRaw, RestartsCdcltIdl, RestartsCdcltNoSym, RestartsCdcltRawSym), !, | |
| 716 | benchmark_constraints(UseIdlSolver, Timeout, T, [(ConstraintPath,TimeZ3,TimeCdclt,TimeCdcltRaw,TimeCdcltIdl,TimeCdcltNoSym,TimeCdcltRawSym,TimeProB,RestartsCdclt,RestartsCdcltRaw,RestartsCdcltIdl,RestartsCdcltNoSym,RestartsCdcltRawSym)|Acc], Data). | |
| 717 | ||
| 718 | benchmark_constraint(UseIdlSolver, _, ConstraintPath, TimeZ3, TimeCdclt, TimeCdcltRaw, TimeCdcltIdl, TimeCdcltNoSym, TimeCdcltRawSym, TimeProB, RestartsCdclt, RestartsCdcltRaw, RestartsCdcltIdl, RestartsCdcltNoSym, RestartsCdcltRawSym) :- | |
| 719 | bmc_timeout(Timeout), | |
| 720 | open(ConstraintPath, read, Stream), | |
| 721 | read(Stream, Constraint), | |
| 722 | close(Stream), | |
| 723 | write(ConstraintPath),nl, | |
| 724 | %translate:print_bexpr(Constraint),nl, | |
| 725 | preferences:set_preference(time_out, Timeout), | |
| 726 | set_preference(cdclt_use_idl_theory_solver, false), | |
| 727 | set_preference(cdclt_perform_static_analysis, false), | |
| 728 | set_preference(cdclt_perform_symmetry_breaking, true), | |
| 729 | cdclt_solver:init, | |
| 730 | write('Solve with Sym-Raw-SMT..'),nl, | |
| 731 | write(ConstraintPath),nl, | |
| 732 | statistics(walltime, [StartCdcltRawSym|_]), | |
| 733 | cdclt_solve_predicate(sym_raw_smt, Constraint, _SolvedPred1, ResCdcltRawSym), | |
| 734 | %ResCdcltRawSym = no_solution_found(solver_answered_unknown), | |
| 735 | statistics(walltime, [StopCdcltRawSym|_]), | |
| 736 | (cdclt_sat_solver:restarts(RestartsCdcltRawSym); RestartsCdcltRawSym = 0), | |
| 737 | format("Restarts: ~w~n", [RestartsCdcltRawSym]), | |
| 738 | TimeCdcltRawSym is StopCdcltRawSym - StartCdcltRawSym, | |
| 739 | ( solved_constraint(ResCdcltRawSym) | |
| 740 | -> inc_solved_counter(sym_raw_smt), | |
| 741 | add_benchmark_result(sym_raw_smt, ConstraintPath, ResCdcltRawSym) | |
| 742 | ; true | |
| 743 | ), | |
| 744 | nl,nl,write(ResCdcltRawSym),nl,nl, | |
| 745 | write('done.'), nl, | |
| 746 | set_preference(cdclt_perform_static_analysis, true), | |
| 747 | cdclt_solver:init, | |
| 748 | write('Solve with Sym-SMT..'),nl, | |
| 749 | write(ConstraintPath),nl, | |
| 750 | statistics(walltime, [StartCdclt|_]), | |
| 751 | cdclt_solve_predicate(sym_smt, Constraint, _SolvedPred2, ResCdclt), | |
| 752 | %ResCdclt = no_solution_found(solver_answered_unknown), | |
| 753 | statistics(walltime, [StopCdclt|_]), | |
| 754 | (cdclt_sat_solver:restarts(RestartsCdclt); RestartsCdclt = 0), | |
| 755 | format("Restarts: ~w~n", [RestartsCdclt]), | |
| 756 | TimeCdclt is StopCdclt - StartCdclt, | |
| 757 | ( solved_constraint(ResCdclt) | |
| 758 | -> inc_solved_counter(sym_smt), | |
| 759 | add_benchmark_result(sym_smt, ConstraintPath, ResCdclt) | |
| 760 | ; true | |
| 761 | ), | |
| 762 | nl,nl,write(ResCdclt),nl,nl, | |
| 763 | write('done.'), nl, | |
| 764 | preferences:set_preference(time_out, Timeout), | |
| 765 | ( UseIdlSolver | |
| 766 | -> set_preference(cdclt_perform_symmetry_breaking, false), | |
| 767 | set_preference(cdclt_use_idl_theory_solver, true), | |
| 768 | cdclt_solver:init, | |
| 769 | write('Solve with IDL-SMT..'),nl, | |
| 770 | statistics(walltime, [StartCdcltIdl|_]), | |
| 771 | cdclt_solve_predicate(idl_smt, Constraint, _SolvedPred3, ResCdcltIdl), | |
| 772 | statistics(walltime, [StopCdcltIdl|_]), | |
| 773 | (cdclt_sat_solver:restarts(RestartsCdcltIdl); RestartsCdcltIdl = 0), | |
| 774 | format("Restarts: ~w~n", [RestartsCdcltIdl]), | |
| 775 | TimeCdcltIdl is StopCdcltIdl - StartCdcltIdl, | |
| 776 | ( solved_constraint(ResCdcltIdl) | |
| 777 | -> inc_solved_counter(idl_smt), | |
| 778 | add_benchmark_result(idl_smt, ConstraintPath, ResCdcltIdl) | |
| 779 | ; true | |
| 780 | ), | |
| 781 | set_preference(cdclt_use_idl_theory_solver, false), | |
| 782 | set_preference(cdclt_perform_symmetry_breaking, true) | |
| 783 | ; TimeCdcltIdl = 0, | |
| 784 | RestartsCdcltIdl = 0, | |
| 785 | ResCdcltIdl = none | |
| 786 | ), | |
| 787 | nl,nl,write(ResCdcltIdl),nl,nl, | |
| 788 | write('done.'), nl, | |
| 789 | %% | |
| 790 | preferences:set_preference(time_out, Timeout), | |
| 791 | set_preference(cdclt_perform_symmetry_breaking, false), | |
| 792 | cdclt_solver:init, | |
| 793 | write('Solve with SMT..'),nl, | |
| 794 | write(ConstraintPath),nl, | |
| 795 | statistics(walltime, [StartCdcltNoSym|_]), | |
| 796 | cdclt_solve_predicate(smt, Constraint, _, ResCdcltNoSym), | |
| 797 | %ResCdcltNoSym = no_solution_found(solver_answered_unknown), | |
| 798 | statistics(walltime, [StopCdcltNoSym|_]), | |
| 799 | (cdclt_sat_solver:restarts(RestartsCdcltNoSym); RestartsCdcltNoSym = 0), | |
| 800 | format("Restarts: ~w~n", [RestartsCdcltNoSym]), | |
| 801 | TimeCdcltNoSym is StopCdcltNoSym - StartCdcltNoSym, | |
| 802 | ( solved_constraint(ResCdcltNoSym) | |
| 803 | -> inc_solved_counter(smt), | |
| 804 | add_benchmark_result(smt, ConstraintPath, ResCdcltNoSym) | |
| 805 | ; true | |
| 806 | ), | |
| 807 | nl,nl,write(ResCdcltNoSym),nl,nl, | |
| 808 | write('done.'), nl, | |
| 809 | preferences:set_preference(time_out, Timeout), | |
| 810 | %% | |
| 811 | set_preference(cdclt_perform_static_analysis, false), | |
| 812 | set_preference(cdclt_perform_symmetry_breaking, false), | |
| 813 | cdclt_solver:init, | |
| 814 | write('Solve with Raw-SMT..'),nl, | |
| 815 | write(ConstraintPath),nl, | |
| 816 | statistics(walltime, [StartCdcltRaw|_]), | |
| 817 | cdclt_solve_predicate(raw_smt, Constraint, _, ResCdcltRaw), | |
| 818 | %ResCdcltRaw = no_solution_found(solver_answered_unknown), | |
| 819 | statistics(walltime, [StopCdcltRaw|_]), | |
| 820 | (cdclt_sat_solver:restarts(RestartsCdcltRaw); RestartsCdcltRaw = 0), | |
| 821 | format("Restarts: ~w~n", [RestartsCdcltRaw]), | |
| 822 | TimeCdcltRaw is StopCdcltRaw - StartCdcltRaw, | |
| 823 | ( solved_constraint(ResCdcltRaw) | |
| 824 | -> inc_solved_counter(raw_smt), | |
| 825 | add_benchmark_result(raw_smt, ConstraintPath, ResCdcltRaw) | |
| 826 | ; true | |
| 827 | ), | |
| 828 | nl,nl,write(ResCdcltRaw),nl,nl, | |
| 829 | write('done.'), nl, | |
| 830 | preferences:set_preference(time_out, Timeout), | |
| 831 | set_preference(cdclt_perform_static_analysis,true), | |
| 832 | set_preference(cdclt_perform_symmetry_breaking,true), | |
| 833 | %% | |
| 834 | write('Solve with Z3..'),nl, | |
| 835 | write(ConstraintPath),nl, | |
| 836 | statistics(walltime, [StartZ3|_]), | |
| 837 | smt_solve_predicate(z3,Constraint, _, ResZ3), | |
| 838 | %ResZ3 = no_solution_found(solver_answered_unknown), | |
| 839 | statistics(walltime, [StopZ3|_]), | |
| 840 | TimeZ3 is StopZ3 - StartZ3, | |
| 841 | ( solved_constraint(ResZ3) | |
| 842 | -> inc_solved_counter(z3), | |
| 843 | add_benchmark_result(z3, ConstraintPath, ResZ3) | |
| 844 | ; true | |
| 845 | ), | |
| 846 | nl,nl,write(ResZ3),nl,nl, | |
| 847 | preferences:set_preference(time_out, Timeout), | |
| 848 | write('Solve with ProB..'),nl, | |
| 849 | write(ConstraintPath),nl, | |
| 850 | statistics(walltime, [StartProB|_]), | |
| 851 | solve_predicate(Constraint, _, ResProB), | |
| 852 | %ResProB = no_solution_found(solver_answered_unknown), | |
| 853 | statistics(walltime, [StopProB|_]), | |
| 854 | TimeProB is StopProB - StartProB, | |
| 855 | ( solved_constraint(ResProB) | |
| 856 | -> inc_solved_counter(prob), | |
| 857 | add_benchmark_result(prob, ConstraintPath, ResProB) | |
| 858 | ; true | |
| 859 | ), | |
| 860 | nl,nl,write(ResProB),nl,nl, | |
| 861 | write('done.'), nl. | |
| 862 | /*( validate_results(ResCdclt, ResProB), | |
| 863 | validate_results(ResCdcltIdl, ResProB), | |
| 864 | validate_results(ResCdcltNoSym, ResProB) | |
| 865 | -> true | |
| 866 | ; add_error(benchmark_constraint, 'Benchmarks results differ'), | |
| 867 | writeq(ResCdclt), | |
| 868 | writeq(ResCdcltIdl), | |
| 869 | writeq(ResCdcltNoSym), | |
| 870 | writeq(ResProB) | |
| 871 | ).*/ | |
| 872 | ||
| 873 | solved_constraint(solution(_)). | |
| 874 | solved_constraint(contradiction_found). | |
| 875 | ||
| 876 | %validate_results(contradiction_found, contradiction_found). | |
| 877 | %validate_results(time_out, _). | |
| 878 | %validate_results(_, time_out). | |
| 879 | %validate_results(solution(_), solution(_)). | |
| 880 | ||
| 881 | %% N-Queens, e.g., to evaluate performance improvement of quantifier instantiation for | |
| 882 | 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. | |
| 883 | ||
| 884 | p(L) :- | |
| 885 | writeq(L), nl, | |
| 886 | L = [_AmountOfSatVars,(prob,N,TimeProB,_FResProB),(z3,N,TimeZ3,_FResZ3),(sym_smt,N,TimeCdclt,_FResCdclt)], | |
| 887 | format("~w & ~w & ~w & ~w & ~n", [N,TimeProB,TimeZ3,TimeCdclt]). | |
| 888 | ||
| 889 | print_n_queens_data(Data) :- | |
| 890 | maplist(p, Data). | |
| 891 | ||
| 892 | % for an evaluation of quantifier instantiation | |
| 893 | run_n_queens_benchmarks :- | |
| 894 | N = [4,6,8,10,12,14,16,18,20], | |
| 895 | preferences:set_preference(time_out, 60000), | |
| 896 | run_n_queens_benchmarks(N, [], Data), | |
| 897 | print_n_queens_data(Data). | |
| 898 | ||
| 899 | run_n_queens_benchmarks([], Data, Data). | |
| 900 | run_n_queens_benchmarks([N|T], DataAcc, Data) :- | |
| 901 | run_n_queens_benchmark(N, DataAcc, NewDataAcc), | |
| 902 | run_n_queens_benchmarks(T, NewDataAcc, Data). | |
| 903 | ||
| 904 | run_n_queens_benchmark(N, DataAcc, NewDataAcc) :- | |
| 905 | n_queens_encoding(N, Constraint), | |
| 906 | ast_optimizer_for_smt:precompute_values(Constraint, [instantiate_quantifier_limit(10000)], IConstraint), | |
| 907 | cdclt_solver:get_amount_of_sat_variables(IConstraint, AmountOfSatVars), | |
| 908 | format("Amount of SAT variables: ~w", [AmountOfSatVars]),nl, | |
| 909 | format("Solve with ProB for N=~w~n", [N]), | |
| 910 | statistics(walltime, [StartProB|_]), | |
| 911 | solve_predicate(IConstraint, _, ResProB), | |
| 912 | statistics(walltime, [StopProB|_]), | |
| 913 | ResProB \= contradiction_found, | |
| 914 | TimeProB is StopProB - StartProB, | |
| 915 | format("Solve with Z3~n for N=~w", [N]), | |
| 916 | statistics(walltime, [StartZ3|_]), | |
| 917 | smt_solve_predicate(z3, Constraint, _, ResZ3), | |
| 918 | statistics(walltime, [StopZ3|_]), | |
| 919 | ResZ3 \= contradiction_found, | |
| 920 | TimeZ3 is StopZ3 - StartZ3, | |
| 921 | format("Solve with Sym-SMT~n for N=~w", [N]), | |
| 922 | set_preference(cdclt_perform_static_analysis, true), | |
| 923 | set_preference(cdclt_perform_symmetry_breaking, true), | |
| 924 | cdclt_solver:init, | |
| 925 | statistics(walltime, [StartCdclt|_]), | |
| 926 | cdclt_solve_predicate(sym_smt, Constraint, _SolvedPred, ResCdclt), | |
| 927 | statistics(walltime, [StopCdclt|_]), | |
| 928 | ResCdclt \= contradiction_found, | |
| 929 | TimeCdclt is StopCdclt - StartCdclt, | |
| 930 | functor(ResProB, FResProB, _), | |
| 931 | functor(ResZ3, FResZ3, _), | |
| 932 | functor(ResCdclt, FResCdclt, _), | |
| 933 | append(DataAcc, [[AmountOfSatVars,(prob,N,TimeProB,FResProB),(z3,N,TimeZ3,FResZ3),(sym_smt,N,TimeCdclt,FResCdclt)]], NewDataAcc). | |
| 934 | ||
| 935 | %% Mixed constraints, e.g., taken from program synthesis or Alloy2B | |
| 936 | % Run benchmarks from prob_prolog root folder. | |
| 937 | ||
| 938 | run_misc_benchmarks :- | |
| 939 | setup_scheduler, | |
| 940 | reset_misc_benchmarks, | |
| 941 | benchmark(_, _), | |
| 942 | fail. | |
| 943 | run_misc_benchmarks :- | |
| 944 | preferences:temporary_set_preference(normalize_ast, true), | |
| 945 | findall(FastestSolver-SolutionOrNot-TimeDiff, fastest_solver(FastestSolver, SolutionOrNot, TimeDiff), LFastestSolver), | |
| 946 | length(LFastestSolver, Results), | |
| 947 | format("~n~n#Results: ~w~n~n", [Results]), | |
| 948 | print_complete_benchmarks(LFastestSolver), | |
| 949 | preferences:reset_temporary_preference(normalize_ast). | |
| 950 | ||
| 951 | reset_misc_benchmarks :- | |
| 952 | retractall(fastest_solver(_, _, _)),!. | |
| 953 | ||
| 954 | setup_scheduler :- | |
| 955 | bmachine:b_load_machine_from_file(prob_examples('public_examples/Synthesis_Tests/scheduler.mch')), | |
| 956 | bmachine:b_machine_precompile,!. | |
| 957 | ||
| 958 | load_constraint_from_file(FilePath, Constraint) :- | |
| 959 | file_exists(FilePath), | |
| 960 | !, | |
| 961 | open(FilePath, read, Stream), | |
| 962 | read_term(Stream, Constraint, []), | |
| 963 | close(Stream). | |
| 964 | load_constraint_from_file(FilePath, _) :- | |
| 965 | format("File does not exist: ~w~n~n", [FilePath]), | |
| 966 | fail. | |
| 967 | ||
| 968 | benchmark_misc_constraint(Constraint, FastestSolver, Res, TimeDiff) :- | |
| 969 | preferences:set_preference(randomise_enumeration_order, false), | |
| 970 | format("Solve with ProB..~n", []), | |
| 971 | statistics(walltime, [ProBStart|_]), | |
| 972 | %kodkod_annotator:annotate_kodkod_constraints(greedy, Constraint, AConstraint), | |
| 973 | solve_predicate(Constraint,_,ProBRes), % from solver_interface | |
| 974 | statistics(walltime, [ProBEnd|_]), | |
| 975 | format("~nProB result: ~w~n", [ProBRes]), | |
| 976 | ProBTime is ProBEnd - ProBStart, | |
| 977 | format("ProB finished.~nSolve with CDCL(T)..~n", []), | |
| 978 | statistics(walltime, [CDCLTStart|_]), | |
| 979 | cdclt_solve_predicate(Constraint, _, CDCLTRes), | |
| 980 | statistics(walltime, [CDCLTEnd|_]), | |
| 981 | format("~nCDCL(T) result: ~w~n", [CDCLTRes]), | |
| 982 | format("CDCL(T) finished..~n", []), | |
| 983 | CDCLTTime is CDCLTEnd - CDCLTStart, | |
| 984 | print_times(ProBTime, CDCLTTime), | |
| 985 | !, | |
| 986 | ( ProBRes = solution(_), | |
| 987 | ( CDCLTRes == contradiction_found | |
| 988 | ; CDCLTRes == error), | |
| 989 | format('Error found: ProB found a solution while CDCL(T) did not.', []), | |
| 990 | trace | |
| 991 | ; ProBRes = contradiction_found, | |
| 992 | ( CDCLTRes = solution(_) | |
| 993 | ; CDCLTRes == error), | |
| 994 | format('Error found: ProB found a contradiction while CDCL(T) did not.', []), | |
| 995 | trace | |
| 996 | ; CDCLTRes == time_out, | |
| 997 | ProBRes == time_out, | |
| 998 | Res = time_out, | |
| 999 | FastestSolver = same, | |
| 1000 | TimeDiff = 0 | |
| 1001 | ; ProBRes == time_out, | |
| 1002 | solution_or_contradiction(CDCLTRes, Res), | |
| 1003 | !, | |
| 1004 | FastestSolver = cdclt, | |
| 1005 | TimeDiff is ProBTime - CDCLTTime | |
| 1006 | ; CDCLTRes == time_out, | |
| 1007 | solution_or_contradiction(ProBRes, Res), | |
| 1008 | !, | |
| 1009 | FastestSolver = prob, | |
| 1010 | TimeDiff is CDCLTTime - ProBTime | |
| 1011 | ; % ProB could not find a result but CDCL(T) | |
| 1012 | ProBRes = no_solution_found(_), | |
| 1013 | solution_or_contradiction(CDCLTRes, Res), | |
| 1014 | !, | |
| 1015 | FastestSolver = cdclt, | |
| 1016 | TimeDiff = 0 | |
| 1017 | ; % CDCL(T) could not find a result but ProB | |
| 1018 | CDCLTRes = no_solution_found(_), | |
| 1019 | solution_or_contradiction(ProBRes, Res), | |
| 1020 | !, | |
| 1021 | FastestSolver = prob, | |
| 1022 | TimeDiff = 0 | |
| 1023 | ; CDCLTTime < ProBTime, | |
| 1024 | FastestSolver = cdclt, | |
| 1025 | solution_or_contradiction(CDCLTRes, Res), | |
| 1026 | TimeDiff is ProBTime - CDCLTTime | |
| 1027 | ; CDCLTTime > ProBTime, | |
| 1028 | FastestSolver = prob, | |
| 1029 | solution_or_contradiction(CDCLTRes, Res), | |
| 1030 | TimeDiff is CDCLTTime - ProBTime | |
| 1031 | ; CDCLTTime == ProBTime, | |
| 1032 | FastestSolver = same, | |
| 1033 | solution_or_contradiction(CDCLTRes, Res), | |
| 1034 | TimeDiff = 0),!. | |
| 1035 | ||
| 1036 | solution_or_contradiction(solution(_), solution). | |
| 1037 | solution_or_contradiction(contradiction_found, contradiction). | |
| 1038 | ||
| 1039 | print_times(ProBTime, CDCLTTime) :- | |
| 1040 | format("ProB: ~w~nCDCL(T) using ProB only: ~w~n", [ProBTime, CDCLTTime]). | |
| 1041 | ||
| 1042 | print_enter_benchmark(Nr) :- | |
| 1043 | format("Run benchmark #~d~n---------------------------------------~n", [Nr]). | |
| 1044 | ||
| 1045 | print_complete_benchmarks(LFastestSolver) :- | |
| 1046 | filter_fastest_solver(cdclt, LFastestSolver, CdcltSol, CdcltNoSol, _, CdcltTimeDiff), | |
| 1047 | filter_fastest_solver(prob, LFastestSolver, ProBSol, ProBNoSol, _, ProBTimeDiff), | |
| 1048 | filter_fastest_solver(same, LFastestSolver, SameSol, SameNoSol, SameTimeout, _), | |
| 1049 | 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]), | |
| 1050 | ( CdcltTimeDiff > ProBTimeDiff | |
| 1051 | -> TotalDiff is CdcltTimeDiff - ProBTimeDiff, | |
| 1052 | format("~nIn total, CDCL(T) is ~d ms faster than ProB.~n", [TotalDiff]) | |
| 1053 | ; TotalDiff is ProBTimeDiff - CdcltTimeDiff, | |
| 1054 | format("~nIn total, ProB is ~d ms faster than CDCL(T).~n", [TotalDiff]) | |
| 1055 | ). | |
| 1056 | ||
| 1057 | filter_fastest_solver(Name, LFastestSolver, SolAmount, ContrAmount, TimeoutsAmount, TimeDiff) :- | |
| 1058 | findall(TimeDiff, member(Name-solution-TimeDiff, LFastestSolver), Solutions), | |
| 1059 | findall(TimeDiff, member(Name-contradiction-TimeDiff, LFastestSolver), Contradictions), | |
| 1060 | findall(TimeDiff, member(Name-time_out-TimeDiff, LFastestSolver), Timeouts), | |
| 1061 | length(Solutions, SolAmount), | |
| 1062 | length(Contradictions, ContrAmount), | |
| 1063 | length(Timeouts, TimeoutsAmount), | |
| 1064 | sumlist(Solutions, TimeDiff1), | |
| 1065 | sumlist(Contradictions, TimeDiff2), | |
| 1066 | TimeDiff is TimeDiff1 + TimeDiff2. | |
| 1067 | ||
| 1068 | benchmark(1, [synthesis]) :- | |
| 1069 | print_enter_benchmark(1), | |
| 1070 | setup_scheduler, | |
| 1071 | preferences:temporary_set_preference(time_out, 2500, OldTimeOut), | |
| 1072 | load_constraint_from_file(prob_examples('public_examples/Synthesis_Tests/constraints/scheduler_inv1_contradiction.pl'), Constraint), | |
| 1073 | benchmark_misc_constraint(Constraint, FastestSolver, Res, TimeDiff), | |
| 1074 | asserta(fastest_solver(FastestSolver, Res, TimeDiff)), | |
| 1075 | preferences:reset_temporary_preference(time_out, OldTimeOut). | |
| 1076 | ||
| 1077 | benchmark(2, [synthesis]) :- | |
| 1078 | print_enter_benchmark(2), | |
| 1079 | setup_scheduler, | |
| 1080 | preferences:temporary_set_preference(time_out, 2500, OldTimeOut), | |
| 1081 | load_constraint_from_file(prob_examples('public_examples/Synthesis_Tests/constraints/scheduler_inv2_contradiction.pl'), Constraint), | |
| 1082 | benchmark_misc_constraint(Constraint, FastestSolver, Res, TimeDiff), | |
| 1083 | asserta(fastest_solver(FastestSolver, Res, TimeDiff)), | |
| 1084 | preferences:reset_temporary_preference(time_out, OldTimeOut). | |
| 1085 | ||
| 1086 | benchmark(3, [synthesis]) :- | |
| 1087 | print_enter_benchmark(3), | |
| 1088 | setup_scheduler, | |
| 1089 | preferences:temporary_set_preference(time_out, 2500, OldTimeOut), | |
| 1090 | load_constraint_from_file(prob_examples('public_examples/Synthesis_Tests/constraints/scheduler_inv3_contradiction.pl'), Constraint), | |
| 1091 | benchmark_misc_constraint(Constraint, FastestSolver, Res, TimeDiff), | |
| 1092 | asserta(fastest_solver(FastestSolver, Res, TimeDiff)), | |
| 1093 | preferences:reset_temporary_preference(time_out, OldTimeOut). | |
| 1094 | ||
| 1095 | benchmark(4, [synthesis]) :- | |
| 1096 | print_enter_benchmark(4), | |
| 1097 | setup_scheduler, | |
| 1098 | preferences:temporary_set_preference(time_out, 2500, OldTimeOut), | |
| 1099 | load_constraint_from_file(prob_examples('public_examples/Synthesis_Tests/constraints/scheduler_inv1.pl'), Constraint), | |
| 1100 | benchmark_misc_constraint(Constraint, FastestSolver, Res, TimeDiff), | |
| 1101 | asserta(fastest_solver(FastestSolver, Res, TimeDiff)), | |
| 1102 | preferences:reset_temporary_preference(time_out, OldTimeOut). | |
| 1103 | ||
| 1104 | benchmark(5, [synthesis]) :- | |
| 1105 | % contradiction | |
| 1106 | print_enter_benchmark(5), | |
| 1107 | setup_scheduler, | |
| 1108 | preferences:temporary_set_preference(time_out, 2500, OldTimeOut), | |
| 1109 | load_constraint_from_file(prob_examples('public_examples/Synthesis_Tests/constraints/scheduler_inv2_contradiction.pl'), Constraint), | |
| 1110 | benchmark_misc_constraint(Constraint, FastestSolver, Res, TimeDiff), | |
| 1111 | asserta(fastest_solver(FastestSolver, Res, TimeDiff)), | |
| 1112 | preferences:reset_temporary_preference(time_out, OldTimeOut). | |
| 1113 | ||
| 1114 | benchmark(6, [synthesis]) :- | |
| 1115 | print_enter_benchmark(6), | |
| 1116 | setup_scheduler, | |
| 1117 | preferences:temporary_set_preference(time_out, 2500, OldTimeOut), | |
| 1118 | load_constraint_from_file(prob_examples('public_examples/Synthesis_Tests/constraints/scheduler_inv3.pl'), Constraint), | |
| 1119 | benchmark_misc_constraint(Constraint, FastestSolver, Res, TimeDiff), | |
| 1120 | asserta(fastest_solver(FastestSolver, Res, TimeDiff)), | |
| 1121 | preferences:reset_temporary_preference(time_out, OldTimeOut). | |
| 1122 | ||
| 1123 | benchmark(7, [synthesis]) :- | |
| 1124 | print_enter_benchmark(7), | |
| 1125 | setup_scheduler, | |
| 1126 | preferences:temporary_set_preference(time_out, 2500, OldTimeOut), | |
| 1127 | load_constraint_from_file(prob_examples('public_examples/Synthesis_Tests/constraints/scheduler_inv4.pl'), Constraint), | |
| 1128 | benchmark_misc_constraint(Constraint, FastestSolver, Res, TimeDiff), | |
| 1129 | asserta(fastest_solver(FastestSolver, Res, TimeDiff)), | |
| 1130 | preferences:reset_temporary_preference(time_out, OldTimeOut). | |
| 1131 | ||
| 1132 | benchmark(8, [synthesis]) :- | |
| 1133 | print_enter_benchmark(8), | |
| 1134 | setup_scheduler, | |
| 1135 | preferences:temporary_set_preference(time_out, 2500, OldTimeOut), | |
| 1136 | load_constraint_from_file(prob_examples('public_examples/Synthesis_Tests/constraints/scheduler_new_process.pl'), Constraint), | |
| 1137 | benchmark_misc_constraint(Constraint, FastestSolver, Res, TimeDiff), | |
| 1138 | asserta(fastest_solver(FastestSolver, Res, TimeDiff)), | |
| 1139 | preferences:reset_temporary_preference(time_out, OldTimeOut). | |
| 1140 | ||
| 1141 | benchmark(9, [synthesis]) :- | |
| 1142 | print_enter_benchmark(9), | |
| 1143 | setup_scheduler, | |
| 1144 | preferences:temporary_set_preference(time_out, 10000, OldTimeOut), | |
| 1145 | load_constraint_from_file(prob_examples('public_examples/Synthesis_Tests/constraints/scheduler_delete_process.pl'), Constraint), | |
| 1146 | benchmark_misc_constraint(Constraint, FastestSolver, Res, TimeDiff), | |
| 1147 | asserta(fastest_solver(FastestSolver, Res, TimeDiff)), | |
| 1148 | preferences:reset_temporary_preference(time_out, OldTimeOut). | |
| 1149 | ||
| 1150 | benchmark(10, [synthesis]) :- | |
| 1151 | print_enter_benchmark(10), | |
| 1152 | setup_scheduler, | |
| 1153 | preferences:temporary_set_preference(time_out, 2500, OldTimeOut), | |
| 1154 | load_constraint_from_file(prob_examples('public_examples/Synthesis_Tests/constraints/scheduler_set_active.pl'), Constraint), | |
| 1155 | benchmark_misc_constraint(Constraint, FastestSolver, Res, TimeDiff), | |
| 1156 | asserta(fastest_solver(FastestSolver, Res, TimeDiff)), | |
| 1157 | preferences:reset_temporary_preference(time_out, OldTimeOut). | |
| 1158 | ||
| 1159 | benchmark(11, [synthesis]) :- | |
| 1160 | % Note: CDCL(T) is much faster than ProB if chr_solver preference is set | |
| 1161 | print_enter_benchmark(11), | |
| 1162 | preferences:temporary_set_preference(time_out, 15000, OldTimeOut), | |
| 1163 | setup_scheduler, | |
| 1164 | load_constraint_from_file(prob_examples('public_examples/Synthesis_Tests/constraints/scheduler_active_to_waiting_precondition.pl'), Constraint), | |
| 1165 | benchmark_misc_constraint(Constraint, FastestSolver, Res, TimeDiff), | |
| 1166 | asserta(fastest_solver(FastestSolver, Res, TimeDiff)), | |
| 1167 | preferences:reset_temporary_preference(time_out, OldTimeOut). | |
| 1168 | ||
| 1169 | ||
| 1170 | benchmark(12, [alloy]) :- | |
| 1171 | print_enter_benchmark(12), | |
| 1172 | alloy2b:load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/alloy_models/toys/grandpa.als.pl')), | |
| 1173 | bmachine:b_machine_precompile, | |
| 1174 | preferences:temporary_set_preference(time_out, 15000, OldTimeOut), | |
| 1175 | load_constraint_from_file(prob_examples('public_examples/Alloy/constraints/alloy_self_grandpas.pl'), Constraint), | |
| 1176 | benchmark_misc_constraint(Constraint, FastestSolver, Res, TimeDiff), | |
| 1177 | asserta(fastest_solver(FastestSolver, Res, TimeDiff)), | |
| 1178 | preferences:reset_temporary_preference(time_out, OldTimeOut). | |
| 1179 | /* | |
| 1180 | benchmark(13, [alloy]) :- | |
| 1181 | print_enter_benchmark(13), | |
| 1182 | alloy2b:load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Puzzles/queens.als.pl')), | |
| 1183 | bmachine:b_machine_precompile, | |
| 1184 | preferences:temporary_set_preference(time_out, 2500, OldTimeOut), | |
| 1185 | load_constraint_from_file(prob_examples('public_examples/Alloy/constraints/alloy_queens1.pl'), Constraint), | |
| 1186 | benchmark_misc_constraint(Constraint, FastestSolver, Res, TimeDiff), | |
| 1187 | asserta(fastest_solver(FastestSolver, Res, TimeDiff)), | |
| 1188 | preferences:reset_temporary_preference(time_out, OldTimeOut). | |
| 1189 | ||
| 1190 | benchmark(14, [alloy]) :- | |
| 1191 | print_enter_benchmark(14), | |
| 1192 | alloy2b:load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Puzzles/queens.als.pl')), | |
| 1193 | bmachine:b_machine_precompile, | |
| 1194 | preferences:temporary_set_preference(time_out, 2500, OldTimeOut), | |
| 1195 | load_constraint_from_file(prob_examples('public_examples/Alloy/constraints/alloy_queens2.pl'), Constraint), | |
| 1196 | benchmark_misc_constraint(Constraint, FastestSolver, Res, TimeDiff), | |
| 1197 | asserta(fastest_solver(FastestSolver, Res, TimeDiff)), | |
| 1198 | preferences:reset_temporary_preference(time_out, OldTimeOut). | |
| 1199 | ||
| 1200 | benchmark(15, [alloy]) :- | |
| 1201 | print_enter_benchmark(15), | |
| 1202 | alloy2b:load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Puzzles/queens.als.pl')), | |
| 1203 | bmachine:b_machine_precompile, | |
| 1204 | preferences:temporary_set_preference(time_out, 2500, OldTimeOut), | |
| 1205 | load_constraint_from_file(prob_examples('public_examples/Alloy/constraints/alloy_queens3.pl'), Constraint), | |
| 1206 | benchmark_misc_constraint(Constraint, FastestSolver, Res, TimeDiff), | |
| 1207 | asserta(fastest_solver(FastestSolver, Res, TimeDiff)), | |
| 1208 | preferences:reset_temporary_preference(time_out, OldTimeOut). | |
| 1209 | */ | |
| 1210 | benchmark(16, [alloy]) :- | |
| 1211 | print_enter_benchmark(16), | |
| 1212 | alloy2b:load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Puzzles/rivercrossing.pl')), | |
| 1213 | bmachine:b_machine_precompile, | |
| 1214 | preferences:temporary_set_preference(time_out, 2500, OldTimeOut), | |
| 1215 | load_constraint_from_file(prob_examples('public_examples/Alloy/constraints/alloy_river_crossing1.pl'), Constraint), | |
| 1216 | benchmark_misc_constraint(Constraint, FastestSolver, Res, TimeDiff), | |
| 1217 | asserta(fastest_solver(FastestSolver, Res, TimeDiff)), | |
| 1218 | preferences:reset_temporary_preference(time_out, OldTimeOut). | |
| 1219 | ||
| 1220 | benchmark(17, [alloy]) :- | |
| 1221 | print_enter_benchmark(17), | |
| 1222 | alloy2b:load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Puzzles/rivercrossing.pl')), | |
| 1223 | bmachine:b_machine_precompile, | |
| 1224 | preferences:temporary_set_preference(time_out, 20000, OldTimeOut), | |
| 1225 | load_constraint_from_file(prob_examples('public_examples/Alloy/constraints/alloy_river_crossing2.pl'), Constraint), | |
| 1226 | benchmark_misc_constraint(Constraint, FastestSolver, Res, TimeDiff), | |
| 1227 | asserta(fastest_solver(FastestSolver, Res, TimeDiff)), | |
| 1228 | preferences:reset_temporary_preference(time_out, OldTimeOut). | |
| 1229 | ||
| 1230 | benchmark(18, [alloy]) :- | |
| 1231 | print_enter_benchmark(18), | |
| 1232 | alloy2b:load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Puzzles/rivercrossing.pl')), | |
| 1233 | bmachine:b_machine_precompile, | |
| 1234 | preferences:temporary_set_preference(time_out, 2500, OldTimeOut), | |
| 1235 | load_constraint_from_file(prob_examples('public_examples/Alloy/constraints/alloy_river_crossing3.pl'), Constraint), | |
| 1236 | benchmark_misc_constraint(Constraint, FastestSolver, Res, TimeDiff), | |
| 1237 | asserta(fastest_solver(FastestSolver, Res, TimeDiff)), | |
| 1238 | preferences:reset_temporary_preference(time_out, OldTimeOut). | |
| 1239 | ||
| 1240 | benchmark(19, [alloy]) :- | |
| 1241 | print_enter_benchmark(19), | |
| 1242 | alloy2b:load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Puzzles/crewalloc.als.pl')), | |
| 1243 | bmachine:b_machine_precompile, | |
| 1244 | preferences:temporary_set_preference(time_out, 10000, OldTimeOut), | |
| 1245 | load_constraint_from_file(prob_examples('public_examples/Alloy/constraints/alloy_crewalloc1.pl'), Constraint), | |
| 1246 | benchmark_misc_constraint(Constraint, FastestSolver, Res, TimeDiff), | |
| 1247 | asserta(fastest_solver(FastestSolver, Res, TimeDiff)), | |
| 1248 | preferences:reset_temporary_preference(time_out, OldTimeOut). | |
| 1249 | ||
| 1250 | benchmark(20, [alloy]) :- | |
| 1251 | print_enter_benchmark(20), | |
| 1252 | alloy2b:load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Puzzles/crewalloc.als.pl')), | |
| 1253 | bmachine:b_machine_precompile, | |
| 1254 | preferences:temporary_set_preference(time_out, 2500, OldTimeOut), | |
| 1255 | load_constraint_from_file(prob_examples('public_examples/Alloy/constraints/alloy_crewalloc2.pl'), Constraint), | |
| 1256 | benchmark_misc_constraint(Constraint, FastestSolver, Res, TimeDiff), | |
| 1257 | asserta(fastest_solver(FastestSolver, Res, TimeDiff)), | |
| 1258 | preferences:reset_temporary_preference(time_out, OldTimeOut). | |
| 1259 | ||
| 1260 | benchmark(21, [misc]) :- | |
| 1261 | print_enter_benchmark(21), | |
| 1262 | preferences:temporary_set_preference(time_out, 2500, OldTimeOut), | |
| 1263 | 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,[]), | |
| 1264 | benchmark_misc_constraint(Constraint, FastestSolver, Res, TimeDiff), | |
| 1265 | asserta(fastest_solver(FastestSolver, Res, TimeDiff)), | |
| 1266 | preferences:reset_temporary_preference(time_out, OldTimeOut). | |
| 1267 | ||
| 1268 | /*smt_benchmarks_path('/home/joshua/smt-comp/lia19/psyco'). | |
| 1269 | ||
| 1270 | run_smt_comp_benchmarks :- | |
| 1271 | retractall(smt_stat(_, _, _, _, _)), | |
| 1272 | smt_benchmarks_path(Root), | |
| 1273 | run_smt_comp_benchmarks(Root), | |
| 1274 | print_smt_comp_results. | |
| 1275 | ||
| 1276 | print_smt_comp_results :- | |
| 1277 | findall(smt_stat(FilePath, CdcltTime, ProBTime, CdcltRes, ProBRes), retract(smt_stat(FilePath, CdcltTime, ProBTime, CdcltRes, ProBRes)), Stats), | |
| 1278 | print_smt_comp_results(Stats). | |
| 1279 | ||
| 1280 | print_smt_comp_results(Stats) :- | |
| 1281 | open('cdclt_benchmarks_smt_comp.txt', write, Stream), | |
| 1282 | write(Stream, 'Filepath,Time CDCL(T),Result CDCL(T),Time ProB,Result ProB\n'), | |
| 1283 | print_smt_comp_results_to_stream(Stream, Stats). | |
| 1284 | ||
| 1285 | print_smt_comp_results_to_stream(Stream, []) :- | |
| 1286 | close(Stream). | |
| 1287 | print_smt_comp_results_to_stream(Stream, [Stat|T]) :- | |
| 1288 | print_stat_to_stream(Stream, Stat), | |
| 1289 | print_smt_comp_results_to_stream(Stream, T). | |
| 1290 | ||
| 1291 | print_stat_to_stream(Stream, smt_stat(FilePath, cdclt_time(CdcltTime), prob_time(ProBTime), cdclt_res(CdcltRes), prob_res(ProBRes))) :- | |
| 1292 | writeq(Stream, FilePath),write(Stream, ','), writeq(Stream, CdcltTime),write(Stream, ','), writeq(Stream, CdcltRes),write(Stream, ','), | |
| 1293 | writeq(Stream, ProBTime),write(Stream, ','), writeq(Stream, ProBRes),write(Stream, '\n'). | |
| 1294 | ||
| 1295 | run_smt_comp_benchmarks(Root) :- | |
| 1296 | get_all_smt2_files(Root, [], Files),!, | |
| 1297 | run_smt_comp_benchmarks_from_files(Files). | |
| 1298 | ||
| 1299 | run_smt_comp_benchmarks_from_files(Files) :- | |
| 1300 | member(_-FilePath, Files), | |
| 1301 | smtlib2_file(FilePath), | |
| 1302 | retract(smtlib2_interpreter:stat(CdcltTime, ProBTime, CdcltRes, ProBRes)), | |
| 1303 | asserta(smt_stat(FilePath, CdcltTime, ProBTime, CdcltRes, ProBRes)), | |
| 1304 | format("SMT-lib file path: ~w", [FilePath]), | |
| 1305 | fail. | |
| 1306 | run_smt_comp_benchmarks_from_files(_). | |
| 1307 | ||
| 1308 | get_all_smt2_files(Path, Acc, Files) :- | |
| 1309 | directory_exists(Path), | |
| 1310 | file_members_of_directory(Path, '*.smt2', Members), | |
| 1311 | directory_members_of_directory(Path, Dirs), | |
| 1312 | append(Acc, Members, NewAcc), | |
| 1313 | map_get_all_smt2_files(Dirs, NewAcc, Files). | |
| 1314 | ||
| 1315 | map_get_all_smt2_files([], Acc, Acc). | |
| 1316 | map_get_all_smt2_files([_-Dir|T], Acc, Files) :- | |
| 1317 | get_all_smt2_files(Dir, Acc, NewAcc), | |
| 1318 | map_get_all_smt2_files(T, NewAcc, Files).*/ |