1		:- module(alloy2b_benchmarks, [benchmark_alloy_command/2]).
2
3		:- use_module(probsrc(debug)).
4		:- use_module(probsrc(parsercall)).
5		:- use_module(probsrc(preferences)).
6		:- use_module(probsrc('alloy2b/alloy2b')).
7		:- use_module(cbcsrc(cbc_path_solver), [verify_alloy_command/5]).
8
9		% For instance: probcli -bench_alloy_cmd run0 ../einsteins_enum.als
10
11		solver_timeout_ms(300000).
12
13		%% benchmark_alloy_command(+CmdName, +AlloyFilePath).
14		benchmark_alloy_command(CmdName, AlloyFilePath) :-
15		call_alloy2pl_parser(AlloyFilePath, PrologFile),
16		statistics(walltime, [LoadStart|_]),
17		load_alloy_ast_prolog_file(PrologFile),
18		statistics(walltime, [LoadEnd|_]),
19		LoadTime is LoadEnd - LoadStart,
20		solver_timeout_ms(Timeout),
21		temporary_set_preference(time_out, Timeout), !,
22		format('Running Alloy benchmarks for ~w with timeout ~w~n',[CmdName,Timeout]),
23		benchmark_command_initialized(CmdName, BenchResults), !,
24		write_benchmark_results_to_file([(loading_and_translation,LoadTime)|BenchResults], AlloyFilePath, CmdName),
25		reset_temporary_preference(time_out), halt.
26
27		write_benchmark_results_to_file(BenchResults, AlloyFilePath, CmdName) :-
28		atom_concat('_benchmarked_', CmdName, TFilename),
29		atom_concat(TFilename, '.txt', FileName),
30		atom_concat(AlloyFilePath, FileName, FilePath),
31		open(FilePath, write, Stream),
32		writeq(Stream, BenchResults),
33		close(Stream).
34
35		verify_command_multi(_, _, 0, _, [], []).
36		verify_command_multi(Solver, CmdName, C, CmdIsValid, [Time|NT], [PRes|NR]) :-
37		C \== 0,
38		statistics(walltime, [Start|_]),
39		verify_alloy_command(CmdName, Solver, TCmdIsValid, _, Res),
40		pretty_res(Res, PRes),
41		statistics(walltime, [End|_]),
42		TTime is End - Start,
43		CmdIsValid = TCmdIsValid,
44		solver_timeout_ms(Timeout),
45		( TTime >= Timeout
46		-> Time = TTime,
47		NT = [], % stop multi execution if timeout exceeded
48		NR = []
49		; Time = TTime,
50		C1 is C - 1,
51		verify_command_multi(Solver, CmdName, C1, CmdIsValid, NT, NR)
52		).
53
54		pretty_res(solution(_), PRes) :-
55		!,
56		PRes = solution.
57		pretty_res(Res, Res).
58
59		%% benchmark_command_initialized(+CmdName, -BenchResults).
60		benchmark_command_initialized(CmdName, BenchResults) :-
61		verify_command_multi(z3, CmdName, 3, CmdIsValidProBZ3, ProBZ3Times, ProBZ3Results),
62		verify_command_multi(prob, CmdName, 3, CmdIsValidProB, ProBTimes, ProBResults),
63		verify_command_multi(probkodkod, CmdName, 3, CmdIsValidProBKodkod, ProBKodkodTimes, ProBKodkodResults),
64		set_preference(cdclt_use_idl_theory_solver, false),
65		set_preference(cdclt_perform_static_analysis, true),
66		set_preference(cdclt_perform_symmetry_breaking, false),
67		verify_command_multi(probsmt, CmdName, 3, CmdIsValidProBSmt, ProBSmtTimes, ProBSmtResults),
68		set_preference(cdclt_perform_static_analysis, false),
69		verify_command_multi(probsmt, CmdName, 3, CmdIsValidProBRawSmt, ProBRawSmtTimes, ProBRawSmtResults),
70		set_preference(cdclt_perform_symmetry_breaking, true),
71		verify_command_multi(probsmt, CmdName, 3, CmdIsValidProBSymRawSmt, ProBSymRawSmtTimes, ProBSymRawSmtResults),
72		set_preference(cdclt_perform_static_analysis, true),
73		verify_command_multi(probsmt, CmdName, 3, CmdIsValidProBSymSmt, ProBSymSmtTimes, ProBSymSmtResults),
74		BenchResults = [(prob,CmdName,CmdIsValidProB,ProBTimes,ProBResults),(probkodkod,CmdName,CmdIsValidProBKodkod,ProBKodkodTimes,ProBKodkodResults),(probsmt,CmdName,CmdIsValidProBSmt,ProBSmtTimes,ProBSmtResults),(probrawsmt,CmdName,CmdIsValidProBRawSmt,ProBRawSmtTimes,ProBRawSmtResults),(probsymrawsmt,CmdName,CmdIsValidProBSymRawSmt,ProBSymRawSmtTimes,ProBSymRawSmtResults),(probsymsmt,CmdName,CmdIsValidProBSymSmt,ProBSymSmtTimes,ProBSymSmtResults),(probz3,CmdName,CmdIsValidProBZ3,ProBZ3Times,ProBZ3Results)].