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).*/ |