alloy2b_benchmarks

benchmark_alloy_command(CmdName, AlloyFilePath) :-
    call_alloy2pl_parser(AlloyFilePath, PrologFile),
    statistics(walltime, [LoadStart|_]),
    load_alloy_ast_prolog_file(PrologFile),
    statistics(walltime, [LoadEnd|_]),
    LoadTime is LoadEnd - LoadStart,
    solver_timeout_ms(Timeout),
    temporary_set_preference(time_out, Timeout), !,
    format('Running Alloy benchmarks for ~w with timeout ~w~n',[CmdName,Timeout]),
    benchmark_command_initialized(CmdName, BenchResults), !,
    write_benchmark_results_to_file([(loading_and_translation,LoadTime)|BenchResults], AlloyFilePath, CmdName),
    reset_temporary_preference(time_out), halt.

benchmark_command_initialized(CmdName, BenchResults) :-
    verify_command_multi(z3, CmdName, 3, CmdIsValidProBZ3, ProBZ3Times, ProBZ3Results),
    verify_command_multi(prob, CmdName, 3, CmdIsValidProB, ProBTimes, ProBResults),
    verify_command_multi(probkodkod, CmdName, 3, CmdIsValidProBKodkod, ProBKodkodTimes, ProBKodkodResults),
    set_preference(cdclt_use_idl_theory_solver, false),
    set_preference(cdclt_perform_static_analysis, true),
    set_preference(cdclt_perform_symmetry_breaking, false),
    verify_command_multi(probsmt, CmdName, 3, CmdIsValidProBSmt, ProBSmtTimes, ProBSmtResults),
    set_preference(cdclt_perform_static_analysis, false),
    verify_command_multi(probsmt, CmdName, 3, CmdIsValidProBRawSmt, ProBRawSmtTimes, ProBRawSmtResults),
    set_preference(cdclt_perform_symmetry_breaking, true),
    verify_command_multi(probsmt, CmdName, 3, CmdIsValidProBSymRawSmt, ProBSymRawSmtTimes, ProBSymRawSmtResults),
    set_preference(cdclt_perform_static_analysis, true),
    verify_command_multi(probsmt, CmdName, 3, CmdIsValidProBSymSmt, ProBSymSmtTimes, ProBSymSmtResults),
    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)].

pretty_res(solution(_), PRes) :-
    !,
    PRes = solution.

pretty_res(Res, Res).

solver_timeout_ms(300000).

verify_command_multi(_, _, 0, _, [], []).

verify_command_multi(Solver, CmdName, C, CmdIsValid, [Time|NT], [PRes|NR]) :-
    C \== 0,
    statistics(walltime, [Start|_]),
    verify_alloy_command(CmdName, Solver, TCmdIsValid, _, Res),
    pretty_res(Res, PRes),
    statistics(walltime, [End|_]),
    TTime is End - Start,
    CmdIsValid = TCmdIsValid,
    solver_timeout_ms(Timeout),
    ( TTime >= Timeout
    -> Time = TTime,
    NT = [], % stop multi execution if timeout exceeded
    NR = []
    ; Time = TTime,
    C1 is C - 1,
    verify_command_multi(Solver, CmdName, C1, CmdIsValid, NT, NR)
).

write_benchmark_results_to_file(BenchResults, AlloyFilePath, CmdName) :-
    atom_concat('_benchmarked_', CmdName, TFilename),
    atom_concat(TFilename, '.txt', FileName),
    atom_concat(AlloyFilePath, FileName, FilePath),
    open(FilePath, write, Stream),
    writeq(Stream, BenchResults),
    close(Stream).