1		:- module(dpllt_solver_benchmarks, [run_bmc_benchmarks1/0,
2		run_bmc_benchmarks2/0,
3		run_bmc_benchmarks3/0,
4		run_bmc_benchmarks4/0,
5		run_bmc_benchmarks5/0,
6		run_bmc_benchmarks6/0,
7		run_deadlock_benchmarks1/0,
8		run_deadlock_benchmarks2/0,
9		run_deadlock_benchmarks3/0,
10		run_deadlock_benchmarks4/0,
11		run_deadlock_benchmarks5/0,
12		run_deadlock_benchmarks6/0,
13		run_cbc_benchmarks1/0,
14		run_cbc_benchmarks2/0,
15		run_cbc_benchmarks3/0,
16		run_cbc_benchmarks4/0,
17		run_cbc_benchmarks5/0,
18		run_cbc_benchmarks6/0,
19		run_cbc_benchmarks/2,
20		run_bmc_benchmarks/2,
21		run_n_queens_benchmarks/0]).
22
23		:- meta_predicate(run_cbc_benchmark(0, ?, ?, ?)).
24		:- meta_predicate(benchmark_constraint(0, ?, ?, ?, ?, ?, ?, ?, ?, ?, ?, ?, ?, ?, ?)).
25
26		:- use_module(library(lists), [maplist/2,maplist/3,sumlist/2,select/3,nth1/3,max_member/2]).
27		:- use_module(library(file_systems)).
28
29		:- use_module(probsrc(preferences), [get_preference/2,set_preference/2]).
30		:- use_module(probsrc('dpllt_solver/dpllt_solver')).
31		:- use_module(probsrc('dpllt_solver/dpllt_settings')).
32		:- use_module(probsrc(solver_interface), [solve_predicate/3]).
33		:- use_module(probsrc(parsercall), [call_tla2b_parser/1]).
34		:- use_module(probsrc(bmachine), [b_machine_precompile/0,b_load_machine_from_file/1,b_load_eventb_project/1,b_load_machine_probfile/1]).
35
36		:- use_module(smt_solvers_interface(smt_solvers_interface), [smt_solve_predicate/4]).
37
38		:- dynamic solved_constraints/2, benchmark_result/3.
39		:- volatile solved_constraints/2, benchmark_result/3.
40
41		inc_solved_counter(Solver) :-
42		(retract(solved_constraints(Solver, Old)); Old = 0),
43		!,
44		New is Old + 1,
45		asserta(solved_constraints(Solver, New)).
46
47		add_benchmark_result(Solver, ConstraintPath, Result) :-
48		asserta(benchmark_result(Solver,ConstraintPath,Result)).
49
50		bmc_timeout(120000).
51		inductive_inv_timeout(120000).
52		deadlock_timeout(120000).
53
54		:- public amount_of_sat_vars_deadlock/0.
55
56		amount_of_sat_vars_deadlock :-
57		amount_of_sat_vars(deadlock, 'benchmarks_cbc_deadlock/abz16_m4/', [], Acc1),
58		amount_of_sat_vars(deadlock, 'benchmarks_cbc_deadlock/abz16_m5/', Acc1, Acc2),
59		amount_of_sat_vars(deadlock, 'benchmarks_cbc_deadlock/abz16_m6/', Acc2, Acc3),
60		amount_of_sat_vars(deadlock, 'benchmarks_cbc_deadlock/abz16_m7/', Acc3, Acc4),
61		amount_of_sat_vars(deadlock, 'benchmarks_cbc_deadlock/r0_geardoor/', Acc4, Acc5),
62		amount_of_sat_vars(deadlock, 'benchmarks_cbc_deadlock/r1_valve/', Acc5, Acc6),
63		amount_of_sat_vars(deadlock, 'benchmarks_cbc_deadlock/r2_outputs/', Acc6, Acc7),
64		amount_of_sat_vars(deadlock, 'benchmarks_cbc_deadlock/r3_sensors/', Acc7, Acc8),
65		amount_of_sat_vars(deadlock, 'benchmarks_cbc_deadlock/r4_handle/', Acc8, Acc9),
66		amount_of_sat_vars(deadlock, 'benchmarks_cbc_deadlock/r5_switch/', Acc9, Acc10),
67		amount_of_sat_vars(deadlock, 'benchmarks_cbc_deadlock/pm_m0_aai/', Acc10, Acc11),
68		amount_of_sat_vars(deadlock, 'benchmarks_cbc_deadlock/pm_m0_aat/', Acc11, Acc12),
69		amount_of_sat_vars(deadlock, 'benchmarks_cbc_deadlock/pm_m0_aoo/', Acc12, Acc13),
70		amount_of_sat_vars(deadlock, 'benchmarks_cbc_deadlock/pm_m0_voo/', Acc13, Acc14),
71		amount_of_sat_vars(deadlock, 'benchmarks_cbc_deadlock/pm_m0_vvi/', Acc14, Acc15),
72		amount_of_sat_vars(deadlock, 'benchmarks_cbc_deadlock/pm_m0_vvt/', Acc15, Acc16),
73		amount_of_sat_vars(deadlock, 'benchmarks_cbc_deadlock/pm_m1_aoor/', Acc16, Acc17),
74		amount_of_sat_vars(deadlock, 'benchmarks_cbc_deadlock/pm_m1_voor/', Acc17, Acc18),
75		amount_of_sat_vars(deadlock, 'benchmarks_cbc_deadlock/pm_m2_aai/', Acc18, Acc19),
76		amount_of_sat_vars(deadlock, 'benchmarks_cbc_deadlock/simple-two-phase/', Acc19, Acc20),
77		amount_of_sat_vars(deadlock, 'benchmarks_cbc_deadlock/prisoners-4/', Acc20, Acc21),
78		amount_of_sat_vars(deadlock, 'benchmarks_cbc_deadlock/bakery/', Acc21, Acc22),
79		amount_of_sat_vars(deadlock, 'benchmarks_cbc_deadlock/paxos-3/', Acc22, Acc23),
80		amount_of_sat_vars(deadlock, 'benchmarks_cbc_deadlock/lightbot/', Acc23, Acc24),
81		amount_of_sat_vars(deadlock, 'benchmarks_cbc_deadlock/travel_agency/', Acc24, Acc25),
82		amount_of_sat_vars(deadlock, 'benchmarks_cbc_deadlock/search_events/', Acc25, Acc26),
83		amount_of_sat_vars(deadlock, 'benchmarks_cbc_deadlock/large_branching/', Acc26, Acc27),
84		mean_of_list(Acc27, TotalMean),
85		median_of_list(Acc27, TotalMedian),
86		max_member(Max, Acc27),
87		open('amount_of_sat_vars_deadlock/total.txt', write, Stream),
88		tell(Stream),
89		format("Total mean: ~w~nTotal median: ~w~nTotal max: ~w~n", [TotalMean,TotalMedian,Max]),
90		close(Stream).
91
92		amount_of_sat_vars_inductive_inv :-
93		amount_of_sat_vars(inductive_inv, 'benchmarks_inductive_inv/abz16_m4/', [], Acc1),
94		amount_of_sat_vars(inductive_inv, 'benchmarks_inductive_inv/abz16_m5/', Acc1, Acc2),
95		amount_of_sat_vars(inductive_inv, 'benchmarks_inductive_inv/abz16_m6/', Acc2, Acc3),
96		amount_of_sat_vars(inductive_inv, 'benchmarks_inductive_inv/abz16_m7/', Acc3, Acc4),
97		amount_of_sat_vars(inductive_inv, 'benchmarks_inductive_inv/r0_geardoor/', Acc4, Acc5),
98		amount_of_sat_vars(inductive_inv, 'benchmarks_inductive_inv/r1_valve/', Acc5, Acc6),
99		amount_of_sat_vars(inductive_inv, 'benchmarks_inductive_inv/r2_outputs/', Acc6, Acc7),
100		amount_of_sat_vars(inductive_inv, 'benchmarks_inductive_inv/r3_sensors/', Acc7, Acc8),
101		amount_of_sat_vars(inductive_inv, 'benchmarks_inductive_inv/r4_handle/', Acc8, Acc9),
102		amount_of_sat_vars(inductive_inv, 'benchmarks_inductive_inv/r5_switch/', Acc9, Acc10),
103		amount_of_sat_vars(inductive_inv, 'benchmarks_inductive_inv/pm_m0_aai/', Acc10, Acc11),
104		amount_of_sat_vars(inductive_inv, 'benchmarks_inductive_inv/pm_m0_aat/', Acc11, Acc12),
105		amount_of_sat_vars(inductive_inv, 'benchmarks_inductive_inv/pm_m0_aoo/', Acc12, Acc13),
106		amount_of_sat_vars(inductive_inv, 'benchmarks_inductive_inv/pm_m0_voo/', Acc13, Acc14),
107		amount_of_sat_vars(inductive_inv, 'benchmarks_inductive_inv/pm_m0_vvi/', Acc14, Acc15),
108		amount_of_sat_vars(inductive_inv, 'benchmarks_inductive_inv/pm_m0_vvt/', Acc15, Acc16),
109		amount_of_sat_vars(inductive_inv, 'benchmarks_inductive_inv/pm_m1_aoor/', Acc16, Acc17),
110		amount_of_sat_vars(inductive_inv, 'benchmarks_inductive_inv/pm_m1_voor/', Acc17, Acc18),
111		amount_of_sat_vars(inductive_inv, 'benchmarks_inductive_inv/pm_m2_aai/', Acc18, Acc19),
112		amount_of_sat_vars(inductive_inv, 'benchmarks_inductive_inv/r6_lights/', Acc19, Acc20),
113		amount_of_sat_vars(inductive_inv, 'benchmarks_inductive_inv/prisoners-4/', Acc20, Acc21),
114		amount_of_sat_vars(inductive_inv, 'benchmarks_inductive_inv/bakery/', Acc21, Acc22),
115		amount_of_sat_vars(inductive_inv, 'benchmarks_inductive_inv/paxos-3/', Acc22, Acc23),
116		amount_of_sat_vars(inductive_inv, 'benchmarks_inductive_inv/lightbot/', Acc23, Acc24),
117		amount_of_sat_vars(inductive_inv, 'benchmarks_inductive_inv/travel_agency/', Acc24, Acc25),
118		amount_of_sat_vars(inductive_inv, 'benchmarks_inductive_inv/search_events/', Acc25, Acc26),
119		amount_of_sat_vars(inductive_inv, 'benchmarks_inductive_inv/large_branching/', Acc26, Acc27),
120		mean_of_list(Acc27, TotalMean),
121		median_of_list(Acc27, TotalMedian),
122		max_member(Max, Acc27),
123		open('amount_of_sat_vars_inductive_inv/total.txt', write, Stream),
124		tell(Stream),
125		format("Total mean: ~w~nTotal median: ~w~nTotal max: ~w~n", [TotalMean,TotalMedian,Max]),
126		close(Stream).
127
128		amount_of_sat_vars_bmc :-
129		amount_of_sat_vars(bmc, 'benchmarks/abz16_m4/', [], Acc1),
130		amount_of_sat_vars(bmc, 'benchmarks/abz16_m5/', Acc1, Acc2),
131		amount_of_sat_vars(bmc, 'benchmarks/abz16_m6/', Acc2, Acc3),
132		amount_of_sat_vars(bmc, 'benchmarks/abz16_m7/', Acc3, Acc4),
133		amount_of_sat_vars(bmc, 'benchmarks/r0_geardoor/', Acc4, Acc5),
134		amount_of_sat_vars(bmc, 'benchmarks/r1_valve/', Acc5, Acc6),
135		amount_of_sat_vars(bmc, 'benchmarks/r2_outputs/', Acc6, Acc7),
136		amount_of_sat_vars(bmc, 'benchmarks/r3_sensors/', Acc7, Acc8),
137		amount_of_sat_vars(bmc, 'benchmarks/r4_handle/', Acc8, Acc9),
138		amount_of_sat_vars(bmc, 'benchmarks/r5_switch/', Acc9, Acc10),
139		amount_of_sat_vars(bmc, 'benchmarks/pm_m0_aai/', Acc10, Acc11),
140		amount_of_sat_vars(bmc, 'benchmarks/pm_m0_aat/', Acc11, Acc12),
141		amount_of_sat_vars(bmc, 'benchmarks/pm_m0_aoo/', Acc12, Acc13),
142		amount_of_sat_vars(bmc, 'benchmarks/pm_m0_voo/', Acc13, Acc14),
143		amount_of_sat_vars(bmc, 'benchmarks/pm_m0_vvi/', Acc14, Acc15),
144		amount_of_sat_vars(bmc, 'benchmarks/pm_m0_vvt/', Acc15, Acc16),
145		amount_of_sat_vars(bmc, 'benchmarks/pm_m1_aoor/', Acc16, Acc17),
146		amount_of_sat_vars(bmc, 'benchmarks/pm_m1_voor/', Acc17, Acc18),
147		amount_of_sat_vars(bmc, 'benchmarks/pm_m2_aai/', Acc18, Acc19),
148		amount_of_sat_vars(bmc, 'benchmarks/simple-two-phase/', Acc19, Acc20),
149		amount_of_sat_vars(bmc, 'benchmarks/prisoners-4/', Acc20, Acc21),
150		amount_of_sat_vars(bmc, 'benchmarks/bakery/', Acc21, Acc22),
151		amount_of_sat_vars(bmc, 'benchmarks/paxos-3/', Acc22, Acc23),
152		amount_of_sat_vars(bmc, 'benchmarks/lightbot/', Acc23, Acc24),
153		amount_of_sat_vars(bmc, 'benchmarks/travel_agency/', Acc24, Acc25),
154		amount_of_sat_vars(bmc, 'benchmarks/search_events/', Acc25, Acc26),
155		amount_of_sat_vars(bmc, 'benchmarks/large_branching/', Acc26, Acc27),
156		amount_of_sat_vars(bmc, 'benchmarks/r6_lights/', Acc27, Acc28),
157		mean_of_list(Acc28, TotalMean),
158		median_of_list(Acc28, TotalMedian),
159		max_member(Max, Acc28),
160		open('amount_of_sat_vars_bmc/total.txt', write, Stream),
161		tell(Stream),
162		format("Total mean: ~w~nTotal median: ~w~nTotal max: ~w~n", [TotalMean,TotalMedian,Max]),
163		close(Stream).
164
165		run_deadlock_benchmarks1 :-
166		deadlock_timeout(Timeout),
167		preferences:set_preference(time_out, Timeout),
168		/*run_cbc_benchmarks(false, 'benchmarks_cbc_deadlock/abz16_m0/'),
169		run_cbc_benchmarks(false, 'benchmarks_cbc_deadlock/abz16_m1/'),
170		run_cbc_benchmarks(false, 'benchmarks_cbc_deadlock/abz16_m2/'),
171		run_cbc_benchmarks(false, 'benchmarks_cbc_deadlock/abz16_m3/'),*/
172		run_cbc_benchmarks(false, 'benchmarks_cbc_deadlock/abz16_m4/'),
173		run_cbc_benchmarks(false, 'benchmarks_cbc_deadlock/abz16_m5/'),
174		run_cbc_benchmarks(false, 'benchmarks_cbc_deadlock/abz16_m6/'),
175		run_cbc_benchmarks(false, 'benchmarks_cbc_deadlock/abz16_m7/').
176
177		run_deadlock_benchmarks2 :-
178		deadlock_timeout(Timeout),
179		preferences:set_preference(time_out, Timeout),
180		run_cbc_benchmarks(false, 'benchmarks_cbc_deadlock/r0_geardoor/'),
181		run_cbc_benchmarks(false, 'benchmarks_cbc_deadlock/r1_valve/'),
182		run_cbc_benchmarks(false, 'benchmarks_cbc_deadlock/r2_outputs/'),
183		run_cbc_benchmarks(false, 'benchmarks_cbc_deadlock/r3_sensors/'),
184		run_cbc_benchmarks(false, 'benchmarks_cbc_deadlock/r4_handle/'),
185		run_cbc_benchmarks(false, 'benchmarks_cbc_deadlock/r5_switch/').
186		%run_cbc_benchmarks(false, 'benchmarks_cbc_deadlock/r6_lights/'), % static contradiction
187
188		run_deadlock_benchmarks3 :-
189		deadlock_timeout(Timeout),
190		preferences:set_preference(time_out, Timeout),
191		run_cbc_benchmarks(false, 'benchmarks_cbc_deadlock/pm_m0_aai/'),
192		run_cbc_benchmarks(false, 'benchmarks_cbc_deadlock/pm_m0_aat/'),
193		run_cbc_benchmarks(false, 'benchmarks_cbc_deadlock/pm_m0_aoo/'),
194		run_cbc_benchmarks(false, 'benchmarks_cbc_deadlock/pm_m0_voo/').
195		/*
196		run_cbc_benchmarks(false, 'benchmarks_cbc_deadlock/pm_m2_aat/'),
197		run_cbc_benchmarks(false, 'benchmarks_cbc_deadlock/pm_m2_vvi/'),
198		run_cbc_benchmarks(false, 'benchmarks_cbc_deadlock/pm_m2_vvt/'),
199		run_cbc_benchmarks(false, 'benchmarks_cbc_deadlock/pm_m3_aai/'),
200		run_cbc_benchmarks(false, 'benchmarks_cbc_deadlock/pm_m3_aat/'),
201		run_cbc_benchmarks(false, 'benchmarks_cbc_deadlock/pm_m3_vvi/'),
202		run_cbc_benchmarks(false, 'benchmarks_cbc_deadlock/pm_m3_vvt/'),
203		run_cbc_benchmarks(false, 'benchmarks_cbc_deadlock/pm_m4_aair/'),
204		run_cbc_benchmarks(false, 'benchmarks_cbc_deadlock/pm_m4_aatr/'),
205		run_cbc_benchmarks(false, 'benchmarks_cbc_deadlock/pm_m4_vvir/'),
206		run_cbc_benchmarks(false, 'benchmarks_cbc_deadlock/pm_m4_vvtr/'),*/
207
208		run_deadlock_benchmarks4 :-
209		deadlock_timeout(Timeout),
210		preferences:set_preference(time_out, Timeout),
211		run_cbc_benchmarks(false, 'benchmarks_cbc_deadlock/pm_m0_vvi/'),
212		run_cbc_benchmarks(false, 'benchmarks_cbc_deadlock/pm_m0_vvt/'),
213		run_cbc_benchmarks(false, 'benchmarks_cbc_deadlock/pm_m1_aoor/'),
214		run_cbc_benchmarks(false, 'benchmarks_cbc_deadlock/pm_m1_voor/'),
215		run_cbc_benchmarks(false, 'benchmarks_cbc_deadlock/pm_m2_aai/').
216
217		run_deadlock_benchmarks5 :-
218		deadlock_timeout(Timeout),
219		preferences:set_preference(time_out, Timeout),
220		run_cbc_benchmarks(false, 'benchmarks_cbc_deadlock/simple-two-phase/'),
221		run_cbc_benchmarks(false, 'benchmarks_cbc_deadlock/prisoners-4/'),
222		run_cbc_benchmarks(false, 'benchmarks_cbc_deadlock/bakery/'),
223		run_cbc_benchmarks(false, 'benchmarks_cbc_deadlock/paxos-3/').
224
225		run_deadlock_benchmarks6 :-
226		deadlock_timeout(Timeout),
227		preferences:set_preference(time_out, Timeout),
228		run_cbc_benchmarks(false, 'benchmarks_cbc_deadlock/lightbot/'),
229		run_cbc_benchmarks(false, 'benchmarks_cbc_deadlock/travel_agency/'),
230		run_cbc_benchmarks(false, 'benchmarks_cbc_deadlock/search_events/'),
231		run_cbc_benchmarks(false, 'benchmarks_cbc_deadlock/large_branching/').
232
233		run_cbc_benchmarks1 :-
234		inductive_inv_timeout(Timeout),
235		preferences:set_preference(time_out, Timeout),
236		/*run_cbc_benchmarks(false, 'benchmarks_inductive_inv/abz16_m0/'),
237		run_cbc_benchmarks(false, 'benchmarks_inductive_inv/abz16_m1/'),
238		run_cbc_benchmarks(false, 'benchmarks_inductive_inv/abz16_m2/'),
239		run_cbc_benchmarks(false, 'benchmarks_inductive_inv/abz16_m3/'),*/
240		run_cbc_benchmarks(false, 'benchmarks_inductive_inv/abz16_m4/'),
241		run_cbc_benchmarks(false, 'benchmarks_inductive_inv/abz16_m5/'),
242		run_cbc_benchmarks(false, 'benchmarks_inductive_inv/abz16_m6/'),
243		run_cbc_benchmarks(false, 'benchmarks_inductive_inv/abz16_m7/').
244
245		run_cbc_benchmarks2 :-
246		inductive_inv_timeout(Timeout),
247		preferences:set_preference(time_out, Timeout),
248		run_cbc_benchmarks(false, 'benchmarks_inductive_inv/r0_geardoor/'),
249		run_cbc_benchmarks(false, 'benchmarks_inductive_inv/r1_valve/'),
250		run_cbc_benchmarks(false, 'benchmarks_inductive_inv/r2_outputs/'),
251		run_cbc_benchmarks(false, 'benchmarks_inductive_inv/r3_sensors/'),
252		run_cbc_benchmarks(false, 'benchmarks_inductive_inv/r4_handle/'),
253		run_cbc_benchmarks(false, 'benchmarks_inductive_inv/r5_switch/'),
254		run_cbc_benchmarks(false, 'benchmarks_inductive_inv/r6_lights/').
255
256		run_cbc_benchmarks3 :-
257		inductive_inv_timeout(Timeout),
258		preferences:set_preference(time_out, Timeout),
259		run_cbc_benchmarks(false, 'benchmarks_inductive_inv/pm_m0_aai/'),
260		run_cbc_benchmarks(false, 'benchmarks_inductive_inv/pm_m0_aat/'),
261		run_cbc_benchmarks(false, 'benchmarks_inductive_inv/pm_m0_aoo/'),
262		run_cbc_benchmarks(false, 'benchmarks_inductive_inv/pm_m0_voo/').
263		/*run_cbc_benchmarks(false, 'benchmarks_inductive_inv/pm_m2_aat/'),
264		run_cbc_benchmarks(false, 'benchmarks_inductive_inv/pm_m2_vvi/'),
265		run_cbc_benchmarks(false, 'benchmarks_inductive_inv/pm_m2_vvt/'),
266		run_cbc_benchmarks(false, 'benchmarks_inductive_inv/pm_m3_aai/'),
267		run_cbc_benchmarks(false, 'benchmarks_inductive_inv/pm_m3_aat/'),
268		run_cbc_benchmarks(false, 'benchmarks_inductive_inv/pm_m3_vvi/'),
269		run_cbc_benchmarks(false, 'benchmarks_inductive_inv/pm_m3_vvt/'),
270		run_cbc_benchmarks(false, 'benchmarks_inductive_inv/pm_m4_aair/'),
271		run_cbc_benchmarks(false, 'benchmarks_inductive_inv/pm_m4_aatr/'),
272		run_cbc_benchmarks(false, 'benchmarks_inductive_inv/pm_m4_vvir/'),
273		run_cbc_benchmarks(false, 'benchmarks_inductive_inv/pm_m4_vvtr/'),*/
274
275		run_cbc_benchmarks4 :-
276		inductive_inv_timeout(Timeout),
277		preferences:set_preference(time_out, Timeout),
278		run_cbc_benchmarks(false, 'benchmarks_inductive_inv/pm_m0_vvi/'),
279		run_cbc_benchmarks(false, 'benchmarks_inductive_inv/pm_m0_vvt/'),
280		run_cbc_benchmarks(false, 'benchmarks_inductive_inv/pm_m1_aoor/'),
281		run_cbc_benchmarks(false, 'benchmarks_inductive_inv/pm_m1_voor/'),
282		run_cbc_benchmarks(false, 'benchmarks_inductive_inv/pm_m2_aai/').
283
284		run_cbc_benchmarks5 :-
285		inductive_inv_timeout(Timeout),
286		preferences:set_preference(time_out, Timeout),
287		%run_cbc_benchmarks(false, 'benchmarks_inductive_inv/simple-two-phase/'), % static contradiction
288		run_cbc_benchmarks(false, 'benchmarks_inductive_inv/prisoners-4/'),
289		run_cbc_benchmarks(false, 'benchmarks_inductive_inv/bakery/'),
290		run_cbc_benchmarks(false, 'benchmarks_inductive_inv/paxos-3/').
291
292		run_cbc_benchmarks6 :-
293		inductive_inv_timeout(Timeout),
294		preferences:set_preference(time_out, Timeout),
295		run_cbc_benchmarks(false, 'benchmarks_inductive_inv/lightbot/'),
296		run_cbc_benchmarks(false, 'benchmarks_inductive_inv/travel_agency/'),
297		run_cbc_benchmarks(false, 'benchmarks_inductive_inv/search_events/'),
298		run_cbc_benchmarks(false, 'benchmarks_inductive_inv/large_branching/').
299
300
301		run_bmc_benchmarks1 :-
302		bmc_timeout(Timeout),
303		preferences:set_preference(time_out, Timeout),
304		%run_bmc_benchmarks(false, 'benchmarks/paxos-5/'),
305		%run_bmc_benchmarks(false, 'benchmarks/abz16_m0/'),
306		/*run_bmc_benchmarks(false, 'benchmarks/abz16_m1/'),
307		run_bmc_benchmarks(false, 'benchmarks/abz16_m2/'),
308		run_bmc_benchmarks(false, 'benchmarks/abz16_m3/'),*/
309		run_bmc_benchmarks(false, 'benchmarks/abz16_m6/'),
310		run_bmc_benchmarks(false, 'benchmarks/abz16_m7/'),
311		run_bmc_benchmarks(false, 'benchmarks/abz16_m4/'),
312		run_bmc_benchmarks(false, 'benchmarks/abz16_m5/').
313
314		run_bmc_benchmarks2 :-
315		bmc_timeout(Timeout),
316		preferences:set_preference(time_out, Timeout),
317		run_bmc_benchmarks(false, 'benchmarks/r4_handle/'),
318		run_bmc_benchmarks(false, 'benchmarks/r5_switch/'),
319		run_bmc_benchmarks(false, 'benchmarks/r6_lights/'),
320		run_bmc_benchmarks(false, 'benchmarks/r0_geardoor/'),
321		run_bmc_benchmarks(false, 'benchmarks/r1_valve/'),
322		run_bmc_benchmarks(false, 'benchmarks/r2_outputs/'),
323		run_bmc_benchmarks(false, 'benchmarks/r3_sensors/').
324
325		run_bmc_benchmarks3 :-
326		bmc_timeout(Timeout),
327		preferences:set_preference(time_out, Timeout),
328		run_bmc_benchmarks(false, 'benchmarks/pm_m0_aai/'),
329		run_bmc_benchmarks(false, 'benchmarks/pm_m0_aat/'),
330		run_bmc_benchmarks(false, 'benchmarks/pm_m0_aoo/'),
331		run_bmc_benchmarks(false, 'benchmarks/pm_m0_voo/'),
332		run_bmc_benchmarks(false, 'benchmarks/pm_m0_vvi/').
333
334		run_bmc_benchmarks4 :-
335		bmc_timeout(Timeout),
336		preferences:set_preference(time_out, Timeout),
337		run_bmc_benchmarks(false, 'benchmarks/pm_m0_vvt/'),
338		run_bmc_benchmarks(false, 'benchmarks/pm_m1_aoor/'),
339		run_bmc_benchmarks(false, 'benchmarks/pm_m1_voor/'),
340		run_bmc_benchmarks(false, 'benchmarks/pm_m2_aai/').
341		/*run_bmc_benchmarks(false, 'benchmarks/pm_m2_aat/'),
342		run_bmc_benchmarks(false, 'benchmarks/pm_m2_vvi/'),
343		run_bmc_benchmarks(false, 'benchmarks/pm_m2_vvt/'),
344		run_bmc_benchmarks(false, 'benchmarks/pm_m3_aai/'),
345		run_bmc_benchmarks(false, 'benchmarks/pm_m3_aat/'),
346		run_bmc_benchmarks(false, 'benchmarks/pm_m3_vvi/'),
347		run_bmc_benchmarks(false, 'benchmarks/pm_m3_vvt/'),
348		run_bmc_benchmarks(false, 'benchmarks/pm_m4_aair/'),
349		run_bmc_benchmarks(false, 'benchmarks/pm_m4_aatr/'),
350		run_bmc_benchmarks(false, 'benchmarks/pm_m4_vvir/'),
351		run_bmc_benchmarks(false, 'benchmarks/pm_m4_vvtr/')*/
352
353		run_bmc_benchmarks5 :-
354		bmc_timeout(Timeout),
355		preferences:set_preference(time_out, Timeout),
356		run_bmc_benchmarks(false, 'benchmarks/simple-two-phase/'),
357		run_bmc_benchmarks(false, 'benchmarks/lightbot/'),
358		run_bmc_benchmarks(false, 'benchmarks/travel_agency/'),
359		run_bmc_benchmarks(false, 'benchmarks/search_events/').
360
361		run_bmc_benchmarks6 :-
362		bmc_timeout(Timeout),
363		preferences:set_preference(time_out, Timeout),
364		run_bmc_benchmarks(false, 'benchmarks/large_branching/'),
365		run_bmc_benchmarks(false, 'benchmarks/prisoners-4/'),
366		run_bmc_benchmarks(false, 'benchmarks/bakery/'),
367		run_bmc_benchmarks(false, 'benchmarks/paxos-3/').
368
369		select_machine_file_path(FilePaths, MachineFilePath, BenchmarkFilePaths) :-
370		select(_-MachineFilePath, FilePaths, BenchmarkFilePaths),
371		( atom_concat(_, '.eventb', MachineFilePath)
372		; atom_concat(_, '.mch', MachineFilePath)
373		; atom_concat(_, '.tla', MachineFilePath)
374		).
375
376		load_b_eventb_or_tla(MachineFilePath) :-
377		( is_eventb_machine(MachineFilePath)
378		-> b_load_eventb_project(MachineFilePath)
379		; is_tla_file(MachineFilePath)
380		-> call_tla2b_parser(MachineFilePath),
381		atom_concat(PrefixPath, '.tla', MachineFilePath),
382		atom_concat(PrefixPath, '.prob', BMachinePath),
383		b_load_machine_probfile(BMachinePath)
384		; b_load_machine_from_file(MachineFilePath)
385		),
386		b_machine_precompile.
387
388		amount_of_sat_vars(BenchmarkName, FolderPath, Acc, NewAcc) :-
389		write('Eval amount of sat variables for '), write(FolderPath), nl,
390		directory_exists(FolderPath),
391		file_members_of_directory(FolderPath, FilePaths),
392		select_machine_file_path(FilePaths, MachineFilePath, TBenchmarkFilePaths),
393		findall(FilePath, (member(_-FilePath, TBenchmarkFilePaths), atom_concat(_, '.eval', FilePath)), BenchmarkFilePaths),
394		load_b_eventb_or_tla(MachineFilePath),
395		amount_of_sat_vars_for_benchmark(BenchmarkFilePaths, AmountOfSatVars),
396		append(Acc, AmountOfSatVars, NewAcc),
397		eval_amount_of_sat_vars(BenchmarkName, AmountOfSatVars).
398
399		mean_of_list([], M) :-
400		!,
401		M = 0.
402		mean_of_list(L, M) :-
403		length(L, Len),
404		sumlist(L, Sum),
405		M is Sum / Len.
406
407		median_of_list(L, M) :-
408		length(L, Len),
409		sort(L, LS),
410		( LS = [E]
411		-> M = E
412		; Len21 is floor(Len / 2),
413		Len22 is ceiling(Len / 2),
414		( Len21 \== Len22
415		-> nth1(Len22, L, M)
416		; nth1(Len21, L, M1),
417		Len211 is Len21 + 1,
418		nth1(Len211, L, M2),
419		M is (M1+M2)/2
420		)
421		).
422
423		eval_amount_of_sat_vars(BenchmarkName, AmountOfSatVars) :-
424		bmachine:b_machine_name(MachineName),
425		atom_concat(MachineName, 'amount_of_sat_vars.txt', OutPath1),
426		atom_concat('amount_of_sat_vars_', BenchmarkName, OutFolder1),
427		atom_concat(OutFolder1, '/', OutFolder),
428		atom_concat(OutFolder, OutPath1, OutPath),
429		mean_of_list(AmountOfSatVars, MeanAmountOfSatVars),
430		median_of_list(AmountOfSatVars, MedianAmountOfSatVars),
431		open(OutPath, write, Stream),
432		tell(Stream),
433		format("AmountOfSatVarsList: ~w~nMean: ~w~nMedian: ~w~n", [AmountOfSatVars, MeanAmountOfSatVars, MedianAmountOfSatVars]),
434		close(Stream).
435
436		amount_of_sat_vars_for_benchmark([], []).
437		amount_of_sat_vars_for_benchmark([BenchmarkFilePath|T], [AmountOfSatVars|TAmountOfSatVars]) :-
438		open(BenchmarkFilePath, read, Stream),
439		read(Stream, Constraint),
440		close(Stream),
441		dpllt_solver:get_amount_of_sat_variables(Constraint, AmountOfSatVars),
442		amount_of_sat_vars_for_benchmark(T, TAmountOfSatVars).
443
444		run_cbc_benchmarks(UseIdlSolver, FolderPath) :-
445		directory_exists(FolderPath),
446		file_members_of_directory(FolderPath, FilePaths),
447		select_machine_file_path(FilePaths, MachineFilePath, TBenchmarkFilePaths),
448		findall(FileName-FilePath, (member(FileName-FilePath, TBenchmarkFilePaths), atom_concat(_, '.eval', FilePath)), BenchmarkFilePaths),
449		load_b_eventb_or_tla(MachineFilePath),
450		run_cbc_benchmarks(UseIdlSolver, FolderPath, BenchmarkFilePaths).
451
452		run_cbc_benchmarks(_, _, []).
453		run_cbc_benchmarks(UseIdlSolver, FolderPath, [FileName-BenchmarkFilePath|T]) :-
454		open(BenchmarkFilePath, read, Stream),
455		read(Stream, Constraint),
456		close(Stream),
457		retractall(dpllt_sat_solver:incremental_mode),
458		run_cbc_benchmark(UseIdlSolver, FolderPath, FileName-BenchmarkFilePath, Constraint),
459		run_cbc_benchmarks(UseIdlSolver, FolderPath, T).
460
461		run_cbc_benchmark(UseIdlSolver, FolderPath, FileName-BenchmarkFilePath, Constraint) :-
462		inductive_inv_timeout(Timeout),
463		preferences:set_preference(time_out, Timeout),
464		set_preference(dpllt_use_idl_theory_solver, false),
465		set_preference(dpllt_perform_static_analysis, false),
466		set_preference(dpllt_perform_symmetry_breaking, true),
467		dpllt_solver:init,
468		write('Solve with Sym-Raw-SMT..'),nl,
469		writeq(BenchmarkFilePath),nl,
470		statistics(walltime, [StartDplltRawSym|_]),
471		dpllt_solve_predicate(Constraint, _, ResDplltRawSym),
472		statistics(walltime, [StopDplltRawSym|_]),
473		(dpllt_sat_solver:restarts(RestartsDplltRawSym); RestartsDplltRawSym = 0),
474		TimeDplltRawSym is StopDplltRawSym - StartDplltRawSym,
475		nl,nl,write(ResDplltRawSym),nl,nl,
476		%%
477		write('done.'), nl,
478		set_preference(dpllt_perform_static_analysis, true),
479		dpllt_solver:init,
480		write('Solve with Sym-SMT..'),nl,
481		writeq(BenchmarkFilePath),nl,
482		statistics(walltime, [StartDpllt|_]),
483		dpllt_solve_predicate(Constraint, _, ResDpllt),
484		statistics(walltime, [StopDpllt|_]),
485		(dpllt_sat_solver:restarts(RestartsDpllt); RestartsDpllt = 0),
486		TimeDpllt is StopDpllt - StartDpllt,
487		nl,nl,write(ResDpllt),nl,nl,
488		%%
489		write('done.'), nl,
490		preferences:set_preference(time_out, Timeout),
491		( UseIdlSolver
492		-> set_preference(dpllt_perform_symmetry_breaking,false),
493		set_preference(dpllt_use_idl_theory_solver,true),
494		dpllt_solver:init,
495		write('Solve with IDL-SMT..'),nl,
496		writeq(BenchmarkFilePath),nl,
497		statistics(walltime, [StartDplltIdl|_]),
498		dpllt_solve_predicate(Constraint, _, ResDplltIdl),
499		statistics(walltime, [StopDplltIdl|_]),
500		(dpllt_sat_solver:restarts(RestartsDplltIdl); RestartsDplltIdl = 0),
501		TimeDplltIdl is StopDplltIdl - StartDplltIdl,
502		set_preference(dpllt_use_idl_theory_solver,false),
503		set_preference(dpllt_perform_symmetry_breaking,true)
504		; TimeDplltIdl = 0,
505		RestartsDplltIdl = 0,
506		ResDplltIdl = none
507		),
508		nl,nl,write(ResDplltIdl),nl,nl,
509		write('done.'), nl,
510		%%
511		preferences:set_preference(time_out, Timeout),
512		set_preference(dpllt_perform_symmetry_breaking,false),
513		dpllt_solver:init,
514		write('Solve with SMT..'),nl,
515		writeq(BenchmarkFilePath),nl,
516		statistics(walltime, [StartDplltNoSym|_]),
517		dpllt_solve_predicate(Constraint, _, ResDplltNoSym),
518		statistics(walltime, [StopDplltNoSym|_]),
519		(dpllt_sat_solver:restarts(RestartsDplltNoSym); RestartsDplltNoSym = 0),
520		TimeDplltNoSym is StopDplltNoSym - StartDplltNoSym,
521		nl,nl,write(ResDplltNoSym),nl,nl,
522		write('done.'), nl,
523		preferences:set_preference(time_out, Timeout),
524		%%
525		set_preference(dpllt_perform_static_analysis,false),
526		set_preference(dpllt_perform_symmetry_breaking,false),
527		dpllt_solver:init,
528		write('Solve with Raw-SMT..'),nl,
529		writeq(BenchmarkFilePath),nl,
530		statistics(walltime, [StartDplltRaw|_]),
531		dpllt_solve_predicate(Constraint, _, ResDplltRaw),
532		statistics(walltime, [StopDplltRaw|_]),
533		(dpllt_sat_solver:restarts(RestartsDplltRaw); RestartsDplltRaw = 0),
534		TimeDplltRaw is StopDplltRaw - StartDplltRaw,
535		nl,nl,write(ResDplltRaw),nl,nl,
536		write('done.'), nl,
537		preferences:set_preference(time_out, Timeout),
538		%%
539		write('Solve with Z3..'),nl,
540		writeq(BenchmarkFilePath),nl,
541		%translate:print_bexpr(Constraint),nl,
542		statistics(walltime, [StartZ3|_]),
543		smt_solve_predicate(z3,Constraint, _, ResZ3),
544		%ResZ3 = no_solution_found(solver_answered_unknown),
545		statistics(walltime, [StopZ3|_]),
546		TimeZ3 is StopZ3 - StartZ3,
547		nl,nl,write(ResZ3),nl,nl,
548		preferences:set_preference(time_out, Timeout),
549		%%
550		write('Solve with ProB..'),nl,
551		writeq(BenchmarkFilePath),nl,
552		statistics(walltime, [StartProB|_]),
553		solve_predicate(Constraint, _, ResProB),
554		%ResProB = no_solution_found(solver_answered_unknown),
555		statistics(walltime, [StopProB|_]),
556		TimeProB is StopProB - StartProB,
557		nl,nl,write(ResProB),nl,nl,
558		write('done.'), nl,
559		!,
560		eval_cbc_benchmark_data(FolderPath, FileName-BenchmarkFilePath, ResDplltRawSym, TimeDplltRawSym, RestartsDplltRawSym, ResDpllt, TimeDpllt, RestartsDpllt, ResDplltNoSym, TimeDplltNoSym, RestartsDplltNoSym, ResDplltIdl, TimeDplltIdl, RestartsDplltIdl, ResDplltRaw, TimeDplltRaw, RestartsDplltRaw, ResZ3, TimeZ3, ResProB, TimeProB).
561
562		eval_cbc_benchmark_data(FolderPath, FileName-BenchmarkFilePath, ResDplltRawSym, TimeDplltRawSym, RestartsDplltRawSym, ResDpllt, TimeDpllt, RestartsDpllt, ResDplltNoSym, TimeDplltNoSym, RestartsDplltNoSym, ResDplltIdl, TimeDplltIdl, RestartsDplltIdl, ResDplltRaw, TimeDplltRaw, RestartsDplltRaw, ResZ3, TimeZ3, ResProB, TimeProB) :-
563		atom_concat(FileNameNoExt, '.eval', FileName),
564		atom_concat('benchmark_results_', FileNameNoExt, TResultsPath),
565		atom_concat(TResultsPath, '.txt', TTResultsPath),
566		atom_concat(FolderPath, TTResultsPath, ResultsPath),
567		open(ResultsPath, write, Stream),
568		tell(Stream),
569		writeq(BenchmarkFilePath),nl,nl,
570		format("DPLLT-Res: ~w~nDPLLT-Time: ~w~nDPLLT-Restarts: ~w~n", [ResDpllt,TimeDpllt,RestartsDpllt]),
571		format("DPLLT-No-Sym-Res: ~w~nDPLLT-No-Sym-Time: ~w~nDPLLT-No-Sym-Restarts: ~w~n", [ResDplltNoSym,TimeDplltNoSym,RestartsDplltNoSym]),
572		format("DPLLT-Idl-Res: ~w~nDPLLT-Idl-Time: ~w~nDPLLT-Idl-Restarts: ~w~n", [ResDplltIdl,TimeDplltIdl,RestartsDplltIdl]),
573		format("DPLLT-Raw-Res: ~w~nDPLLT-Raw-Time: ~w~nDPLLT-Raw-Restarts: ~w~n", [ResDplltRaw,TimeDplltRaw,RestartsDplltRaw]),
574		format("DPLLT-Sym-Raw-Res: ~w~nDPLLT-Sym-Raw-Time: ~w~nDPLLT-Sym-Raw-Restarts: ~w~n", [ResDplltRawSym,TimeDplltRawSym,RestartsDplltRawSym]),
575		format("Z3-Res: ~w~nZ3-Time: ~w~n", [ResZ3,TimeZ3]),
576		format("ProB-Res: ~w~nProB-Time: ~w~n", [ResProB,TimeProB]),
577		close(Stream),
578		!.
579
580		int_range(C, B, R) :-
581		C == B,
582		!,
583		R = [C].
584		int_range(C, B, [C|T]) :-
585		C1 is C + 1,
586		int_range(C1, B, T).
587
588		get_file_paths_from_config(ConfigPath, MachineFile, ConstraintPaths, Description, MachineName) :-
589		open(ConfigPath, read, Stream),
590		read(Stream, Config),
591		close(Stream),
592		Config = benchmark_config(Description, MachineFile, MachineName, MaxBound),
593		int_range(0, MaxBound, KRange),
594		findall(ConstraintPath,
595		(member(K, KRange), atom_concat(MachineName, '_monolithic_bmc_k_', T1),
596		number_codes(K, CK), atom_codes(AK, CK),
597		atom_concat(T1, AK, T2), atom_concat(T2, '.eval', ConstraintPath)),
598		ConstraintPaths).
599
600		is_eventb_machine(MachineFile) :-
601		atom_concat(_, '.eventb', MachineFile).
602
603		is_tla_file(File) :-
604		atom_concat(_, '.tla', File).
605
606		write_to_csv(SolverName, MachineName, Data) :-
607		atom_concat('benchmarks_dpllt_journal/', MachineName, Path1),
608		atom_concat(Path1, '_results_', Path2),
609		atom_concat(Path2, SolverName, Path3),
610		atom_concat(Path3, '.csv', EvalFilePath),
611		nl,nl,write('csv'),nl,
612		write(EvalFilePath),nl,nl,
613		open(EvalFilePath, write, Stream),
614		tell(Stream),
615		format("ConstraintPath,Result,Time (ms)~n", []),
616		write_to_csv_stream(SolverName, Stream, Data),
617		close(Stream).
618
619		write_to_csv_stream(_, _, []).
620		write_to_csv_stream(SolverName, Stream, [(ConstraintPath,Time)|T]) :-
621		( benchmark_result(SolverName, ConstraintPath, Result)
622		-> true
623		; Result = no_solution_found
624		),
625		format("~w,~w,~w~n", [ConstraintPath,Result,Time]),
626		write_to_csv_stream(SolverName, Stream, T).
627
628		eval_benchmark_data_csv(MachineName, Description, Data) :-
629		format("Evaluate benchmarks ~w for detailed CSV~n", [Description]),
630		findall((ConstraintPath,TimeZ3), member((ConstraintPath,TimeZ3,_,_,_,_,_,_,_,_,_,_), Data), DataZ3),
631		findall((ConstraintPath,TimeDpllt), member((ConstraintPath,_,TimeDpllt,_,_,_,_,_,_,_,_,_), Data), DataDpllt),
632		findall((ConstraintPath,TimeDplltRaw), member((ConstraintPath,_,_,TimeDplltRaw,_,_,_,_,_,_,_,_,_), Data), DataDplltRaw),
633		%findall((ConstraintPath,TimeDplltIdl), member((ConstraintPath,_,_,_,TimeDplltIdl,_,_,_,_,_,_,_,_), Data), DataDplltIdl),
634		findall((ConstraintPath,TimeDplltNoSym), member((ConstraintPath,_,_,_,_,TimeDplltNoSym,_,_,_,_,_,_,_), Data), DataDplltNoSym),
635		findall((ConstraintPath,TimeDplltRawSym), member((ConstraintPath,_,_,_,_,_,TimeDplltRawSym,_,_,_,_,_,_), Data), DataDplltRawSym),
636		findall((ConstraintPath,TimeProB), member((ConstraintPath,_,_,_,_,_,_,TimeProB,_,_,_,_,_), Data), DataProB),
637		write_to_csv(z3, MachineName, DataZ3),
638		write_to_csv(prob, MachineName, DataProB),
639		write_to_csv(smt, MachineName, DataDplltNoSym),
640		write_to_csv(sym_smt, MachineName, DataDpllt),
641		write_to_csv(raw_smt, MachineName, DataDplltRaw),
642		write_to_csv(sym_raw_smt, MachineName, DataDplltRawSym).
643
644		eval_benchmark_data(MachineName, Description, Data) :-
645		format("Evaluate benchmarks ~w~n", [Description]),
646		findall(TimeZ3, member((_,TimeZ3,_,_,_,_,_,_,_,_,_,_), Data), TimesZ3),
647		findall(TimeDpllt, member((_,_,TimeDpllt,_,_,_,_,_,_,_,_,_), Data), TimesDpllt),
648		findall(TimeDplltRaw, member((_,_,_,TimeDplltRaw,_,_,_,_,_,_,_,_,_), Data), TimesDplltRaw),
649		findall(TimeDplltIdl, member((_,_,_,_,TimeDplltIdl,_,_,_,_,_,_,_,_), Data), TimesDplltIdl),
650		findall(TimeDplltNoSym, member((_,_,_,_,_,TimeDplltNoSym,_,_,_,_,_,_,_), Data), TimesDplltNoSym),
651		findall(TimeDplltRawSym, member((_,_,_,_,_,_,TimeDplltRawSym,_,_,_,_,_,_), Data), TimesDplltRawSym),
652		findall(TimeProB, member((_,_,_,_,_,_,_,TimeProB,_,_,_,_,_), Data), TimesProB),
653		findall(RestartDpllt, member((_,_,_,_,_,_,_,_,RestartDpllt,_,_,_,_), Data), RestartsDpllt),
654		findall(RestartDplltRaw, member((_,_,_,_,_,_,_,_,_,RestartDplltRaw,_,_), Data), RestartsDplltRaw),
655		findall(RestartDplltIdl, member((_,_,_,_,_,_,_,_,_,_,RestartDplltIdl,_,_), Data), RestartsDplltIdl),
656		findall(RestartDplltNoSym, member((_,_,_,_,_,_,_,_,_,_,_,RestartDplltNoSym,_), Data), RestartsDplltNoSym),
657		findall(RestartDplltRawSym, member((_,_,_,_,_,_,_,_,_,_,_,_,RestartDplltRawSym), Data), RestartsDplltRawSym),
658		sumlist(TimesZ3, TimeZ3),
659		sumlist(TimesDpllt, TimeDpllt),
660		sumlist(TimesDplltRaw, TimeDplltRaw),
661		sumlist(TimesDplltIdl, TimeDplltIdl),
662		sumlist(TimesDplltNoSym, TimeDplltNoSym),
663		sumlist(TimesDplltRawSym, TimeDplltRawSym),
664		sumlist(TimesProB, TimeProB),
665		sumlist(RestartsDpllt, RestartDpllt),
666		sumlist(RestartsDplltRaw, RestartDplltRaw),
667		sumlist(RestartsDplltIdl, RestartDplltIdl),
668		sumlist(RestartsDplltNoSym, RestartDplltNoSym),
669		sumlist(RestartsDplltRawSym, RestartDplltRawSym),
670		atom_concat('benchmarks_dpllt_journal/', MachineName, Path1),
671		atom_concat(Path1, '_results.txt', EvalFilePath),
672		nl,nl,write('eval'),nl,
673		write(EvalFilePath),nl,nl,
674		open(EvalFilePath, write, Stream),
675		tell(Stream),
676		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", [TimeDplltRawSym,RestartsDplltRawSym,TimeZ3,TimeDpllt,RestartDpllt,TimeDplltIdl,RestartDplltIdl,TimeDplltNoSym,RestartDplltNoSym,TimeDplltRaw,RestartDplltRaw,TimeProB]),
677		findall(TO, (solved_constraints(A,B), TO = solved_constraints(A,B)), TOs),
678		(member(solved_constraints(prob,SolvedProB), TOs); SolvedProB = 0),
679		(member(solved_constraints(z3,SolvedZ3), TOs); SolvedZ3 = 0),
680		(member(solved_constraints(smt,SolvedSMT), TOs); SolvedSMT = 0),
681		(member(solved_constraints(raw_smt,SolvedRawSMT), TOs); SolvedRawSMT = 0),
682		(member(solved_constraints(sym_smt,SolvedSymSMT), TOs); SolvedSymSMT = 0),
683		(member(solved_constraints(sym_raw_smt,SolvedSymRawSMT), TOs); SolvedSymRawSMT = 0),
684		format("~w / ~w & ~w / ~w & ~w / ~w & ~w / ~w & ~w / ~w & ~w / ~w~n", [SolvedProB,TimeProB,SolvedZ3,TimeZ3,SolvedSMT,TimeDplltNoSym,SolvedRawSMT,TimeDplltRaw,SolvedSymSMT,TimeDpllt,SolvedSymRawSMT,TimeDplltRawSym]),
685		nl, write(TOs), nl,
686		close(Stream).
687
688		run_bmc_benchmarks(UseIdlSolver, DirPath) :-
689		retractall(solved_constraints(_,_)),
690		retractall(benchmark_result(_,_,_)),
691		atom_concat(DirPath, 'benchmark_config.pl', ConfigPath),
692		get_file_paths_from_config(ConfigPath, MachineFile, ConstraintPaths, Description, MachineName),
693		format("Run benchmarks ~w~n", [Description]),
694		atom_concat(DirPath, MachineFile, MachinePath),
695		load_b_eventb_or_tla(MachinePath),
696		maplist(atom_concat(DirPath), ConstraintPaths, FullConstraintPaths),
697		get_preference(time_out, Timeout),
698		retractall(dpllt_sat_solver:incremental_mode),
699		benchmark_constraints(UseIdlSolver, Timeout, FullConstraintPaths, [], Data),
700		retractall(dpllt_sat_solver:memoize_backjump_clause(_, _, _)),
701		eval_benchmark_data(MachineName, Description, Data),
702		eval_benchmark_data_csv(MachineName, Description, Data).
703
704		benchmark_constraints(_, _, [], Acc, Acc).
705		benchmark_constraints(UseIdlSolver, Timeout, [ConstraintPath|T], Acc, Data) :-
706		benchmark_constraint(UseIdlSolver, Timeout, ConstraintPath, TimeZ3, TimeDpllt, TimeDplltRaw, TimeDplltIdl, TimeDplltNoSym, TimeDplltRawSym, TimeProB, RestartsDpllt, RestartsDplltRaw, RestartsDplltIdl, RestartsDplltNoSym, RestartsDplltRawSym), !,
707		benchmark_constraints(UseIdlSolver, Timeout, T, [(ConstraintPath,TimeZ3,TimeDpllt,TimeDplltRaw,TimeDplltIdl,TimeDplltNoSym,TimeDplltRawSym,TimeProB,RestartsDpllt,RestartsDplltRaw,RestartsDplltIdl,RestartsDplltNoSym,RestartsDplltRawSym)|Acc], Data).
708
709		benchmark_constraint(UseIdlSolver, _, ConstraintPath, TimeZ3, TimeDpllt, TimeDplltRaw, TimeDplltIdl, TimeDplltNoSym, TimeDplltRawSym, TimeProB, RestartsDpllt, RestartsDplltRaw, RestartsDplltIdl, RestartsDplltNoSym, RestartsDplltRawSym) :-
710		bmc_timeout(Timeout),
711		open(ConstraintPath, read, Stream),
712		read(Stream, Constraint),
713		close(Stream),
714		write(ConstraintPath),nl,
715		%translate:print_bexpr(Constraint),nl,
716		preferences:set_preference(time_out, Timeout),
717		set_preference(dpllt_use_idl_theory_solver, false),
718		set_preference(dpllt_perform_static_analysis, false),
719		set_preference(dpllt_perform_symmetry_breaking, true),
720		dpllt_solver:init,
721		write('Solve with Sym-Raw-SMT..'),nl,
722		write(ConstraintPath),nl,
723		statistics(walltime, [StartDplltRawSym|_]),
724		dpllt_solve_predicate(sym_raw_smt, Constraint, _SolvedPred1, ResDplltRawSym),
725		%ResDplltRawSym = no_solution_found(solver_answered_unknown),
726		statistics(walltime, [StopDplltRawSym|_]),
727		(dpllt_sat_solver:restarts(RestartsDplltRawSym); RestartsDplltRawSym = 0),
728		format("Restarts: ~w~n", [RestartsDplltRawSym]),
729		TimeDplltRawSym is StopDplltRawSym - StartDplltRawSym,
730		( solved_constraint(ResDplltRawSym)
731		-> inc_solved_counter(sym_raw_smt),
732		add_benchmark_result(sym_raw_smt, ConstraintPath, ResDplltRawSym)
733		; true
734		),
735		nl,nl,write(ResDplltRawSym),nl,nl,
736		write('done.'), nl,
737		set_preference(dpllt_perform_static_analysis, true),
738		dpllt_solver:init,
739		write('Solve with Sym-SMT..'),nl,
740		write(ConstraintPath),nl,
741		statistics(walltime, [StartDpllt|_]),
742		dpllt_solve_predicate(sym_smt, Constraint, _SolvedPred2, ResDpllt),
743		%ResDpllt = no_solution_found(solver_answered_unknown),
744		statistics(walltime, [StopDpllt|_]),
745		(dpllt_sat_solver:restarts(RestartsDpllt); RestartsDpllt = 0),
746		format("Restarts: ~w~n", [RestartsDpllt]),
747		TimeDpllt is StopDpllt - StartDpllt,
748		( solved_constraint(ResDpllt)
749		-> inc_solved_counter(sym_smt),
750		add_benchmark_result(sym_smt, ConstraintPath, ResDpllt)
751		; true
752		),
753		nl,nl,write(ResDpllt),nl,nl,
754		write('done.'), nl,
755		preferences:set_preference(time_out, Timeout),
756		( UseIdlSolver
757		-> set_preference(dpllt_perform_symmetry_breaking, false),
758		set_preference(dpllt_use_idl_theory_solver, true),
759		dpllt_solver:init,
760		write('Solve with IDL-SMT..'),nl,
761		statistics(walltime, [StartDplltIdl|_]),
762		dpllt_solve_predicate(idl_smt, Constraint, _SolvedPred3, ResDplltIdl),
763		statistics(walltime, [StopDplltIdl|_]),
764		(dpllt_sat_solver:restarts(RestartsDplltIdl); RestartsDplltIdl = 0),
765		format("Restarts: ~w~n", [RestartsDplltIdl]),
766		TimeDplltIdl is StopDplltIdl - StartDplltIdl,
767		( solved_constraint(ResDplltIdl)
768		-> inc_solved_counter(idl_smt),
769		add_benchmark_result(idl_smt, ConstraintPath, ResDplltIdl)
770		; true
771		),
772		set_preference(dpllt_use_idl_theory_solver, false),
773		set_preference(dpllt_perform_symmetry_breaking, true)
774		; TimeDplltIdl = 0,
775		RestartsDplltIdl = 0,
776		ResDplltIdl = none
777		),
778		nl,nl,write(ResDplltIdl),nl,nl,
779		write('done.'), nl,
780		%%
781		preferences:set_preference(time_out, Timeout),
782		set_preference(dpllt_perform_symmetry_breaking, false),
783		dpllt_solver:init,
784		write('Solve with SMT..'),nl,
785		write(ConstraintPath),nl,
786		statistics(walltime, [StartDplltNoSym|_]),
787		dpllt_solve_predicate(smt, Constraint, _, ResDplltNoSym),
788		%ResDplltNoSym = no_solution_found(solver_answered_unknown),
789		statistics(walltime, [StopDplltNoSym|_]),
790		(dpllt_sat_solver:restarts(RestartsDplltNoSym); RestartsDplltNoSym = 0),
791		format("Restarts: ~w~n", [RestartsDplltNoSym]),
792		TimeDplltNoSym is StopDplltNoSym - StartDplltNoSym,
793		( solved_constraint(ResDplltNoSym)
794		-> inc_solved_counter(smt),
795		add_benchmark_result(smt, ConstraintPath, ResDplltNoSym)
796		; true
797		),
798		nl,nl,write(ResDplltNoSym),nl,nl,
799		write('done.'), nl,
800		preferences:set_preference(time_out, Timeout),
801		%%
802		set_preference(dpllt_perform_static_analysis, false),
803		set_preference(dpllt_perform_symmetry_breaking, false),
804		dpllt_solver:init,
805		write('Solve with Raw-SMT..'),nl,
806		write(ConstraintPath),nl,
807		statistics(walltime, [StartDplltRaw|_]),
808		dpllt_solve_predicate(raw_smt, Constraint, _, ResDplltRaw),
809		%ResDplltRaw = no_solution_found(solver_answered_unknown),
810		statistics(walltime, [StopDplltRaw|_]),
811		(dpllt_sat_solver:restarts(RestartsDplltRaw); RestartsDplltRaw = 0),
812		format("Restarts: ~w~n", [RestartsDplltRaw]),
813		TimeDplltRaw is StopDplltRaw - StartDplltRaw,
814		( solved_constraint(ResDplltRaw)
815		-> inc_solved_counter(raw_smt),
816		add_benchmark_result(raw_smt, ConstraintPath, ResDplltRaw)
817		; true
818		),
819		nl,nl,write(ResDplltRaw),nl,nl,
820		write('done.'), nl,
821		preferences:set_preference(time_out, Timeout),
822		set_preference(dpllt_perform_static_analysis,true),
823		set_preference(dpllt_perform_symmetry_breaking,true),
824		%%
825		write('Solve with Z3..'),nl,
826		write(ConstraintPath),nl,
827		statistics(walltime, [StartZ3|_]),
828		smt_solve_predicate(z3,Constraint, _, ResZ3),
829		%ResZ3 = no_solution_found(solver_answered_unknown),
830		statistics(walltime, [StopZ3|_]),
831		TimeZ3 is StopZ3 - StartZ3,
832		( solved_constraint(ResZ3)
833		-> inc_solved_counter(z3),
834		add_benchmark_result(z3, ConstraintPath, ResZ3)
835		; true
836		),
837		nl,nl,write(ResZ3),nl,nl,
838		preferences:set_preference(time_out, Timeout),
839		write('Solve with ProB..'),nl,
840		write(ConstraintPath),nl,
841		statistics(walltime, [StartProB|_]),
842		solve_predicate(Constraint, _, ResProB),
843		%ResProB = no_solution_found(solver_answered_unknown),
844		statistics(walltime, [StopProB|_]),
845		TimeProB is StopProB - StartProB,
846		( solved_constraint(ResProB)
847		-> inc_solved_counter(prob),
848		add_benchmark_result(prob, ConstraintPath, ResProB)
849		; true
850		),
851		nl,nl,write(ResProB),nl,nl,
852		write('done.'), nl.
853		/*( validate_results(ResDpllt, ResProB),
854		validate_results(ResDplltIdl, ResProB),
855		validate_results(ResDplltNoSym, ResProB)
856		-> true
857		; add_error(benchmark_constraint, 'Benchmarks results differ'),
858		writeq(ResDpllt),
859		writeq(ResDplltIdl),
860		writeq(ResDplltNoSym),
861		writeq(ResProB)
862		).*/
863
864		solved_constraint(solution(_)).
865		solved_constraint(contradiction_found).
866
867		validate_results(contradiction_found, contradiction_found).
868		%validate_results(time_out, _).
869		%validate_results(_, time_out).
870		validate_results(solution(_), solution(_)).
871
872		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.
873
874		p(L) :-
875		writeq(L), nl,
876		L = [_AmountOfSatVars,(prob,N,TimeProB,_FResProB),(z3,N,TimeZ3,_FResZ3),(sym_smt,N,TimeDpllt,_FResDpllt)],
877		format("~w & ~w & ~w & ~w & ~n", [N,TimeProB,TimeZ3,TimeDpllt]).
878
879		print_n_queens_data(Data) :-
880		maplist(p, Data).
881
882		% for an evaluation of quantifier instantiation
883		run_n_queens_benchmarks :-
884		N = [4,6,8,10,12,14,16,18,20],
885		preferences:set_preference(time_out, 60000),
886		run_n_queens_benchmarks(N, [], Data),
887		print_n_queens_data(Data).
888
889		run_n_queens_benchmarks([], Data, Data).
890		run_n_queens_benchmarks([N|T], DataAcc, Data) :-
891		run_n_queens_benchmark(N, DataAcc, NewDataAcc),
892		run_n_queens_benchmarks(T, NewDataAcc, Data).
893
894		run_n_queens_benchmark(N, DataAcc, NewDataAcc) :-
895		n_queens_encoding(N, Constraint),
896		ast_optimizer_for_smt:precompute_values(Constraint, [instantiate_quantifier_limit(10000)], IConstraint),
897		dpllt_solver:get_amount_of_sat_variables(IConstraint, AmountOfSatVars),
898		format("Amount of SAT variables: ~w", [AmountOfSatVars]),nl,
899		format("Solve with ProB for N=~w~n", [N]),
900		statistics(walltime, [StartProB|_]),
901		solve_predicate(IConstraint, _, ResProB),
902		statistics(walltime, [StopProB|_]),
903		ResProB \= contradiction_found,
904		TimeProB is StopProB - StartProB,
905		format("Solve with Z3~n for N=~w", [N]),
906		statistics(walltime, [StartZ3|_]),
907		smt_solve_predicate(z3, Constraint, _, ResZ3),
908		statistics(walltime, [StopZ3|_]),
909		ResZ3 \= contradiction_found,
910		TimeZ3 is StopZ3 - StartZ3,
911		format("Solve with Sym-SMT~n for N=~w", [N]),
912		set_preference(dpllt_perform_static_analysis, true),
913		set_preference(dpllt_perform_symmetry_breaking, true),
914		dpllt_solver:init,
915		statistics(walltime, [StartDpllt|_]),
916		dpllt_solve_predicate(sym_smt, Constraint, _SolvedPred, ResDpllt),
917		statistics(walltime, [StopDpllt|_]),
918		ResDpllt \= contradiction_found,
919		TimeDpllt is StopDpllt - StartDpllt,
920		functor(ResProB, FResProB, _),
921		functor(ResZ3, FResZ3, _),
922		functor(ResDpllt, FResDpllt, _),
923		append(DataAcc, [[AmountOfSatVars,(prob,N,TimeProB,FResProB),(z3,N,TimeZ3,FResZ3),(sym_smt,N,TimeDpllt,FResDpllt)]], NewDataAcc).