dpllt_benchmarks

benchmark(1, [synthesis]) :-
    print_enter_benchmark(1),
    setup_scheduler,
    preferences:temporary_set_preference(time_out, 2500, OldTimeOut),
    load_constraint_from_file(prob_examples('public_examples/Synthesis_Tests/constraints/scheduler_inv1_contradiction.pl'), Constraint),
    benchmark_constraint(Constraint, FastestSolver, Res, TimeDiff),
    asserta(fastest_solver(FastestSolver, Res, TimeDiff)),
    preferences:reset_temporary_preference(time_out, OldTimeOut).

benchmark(2, [synthesis]) :-
    print_enter_benchmark(2),
    setup_scheduler,
    preferences:temporary_set_preference(time_out, 2500, OldTimeOut),
    load_constraint_from_file(prob_examples('public_examples/Synthesis_Tests/constraints/scheduler_inv2_contradiction.pl'), Constraint),
    benchmark_constraint(Constraint, FastestSolver, Res, TimeDiff),
    asserta(fastest_solver(FastestSolver, Res, TimeDiff)),
    preferences:reset_temporary_preference(time_out, OldTimeOut).

benchmark(3, [synthesis]) :-
    print_enter_benchmark(3),
    setup_scheduler,
    preferences:temporary_set_preference(time_out, 2500, OldTimeOut),
    load_constraint_from_file(prob_examples('public_examples/Synthesis_Tests/constraints/scheduler_inv3_contradiction.pl'), Constraint),
    benchmark_constraint(Constraint, FastestSolver, Res, TimeDiff),
    asserta(fastest_solver(FastestSolver, Res, TimeDiff)),
    preferences:reset_temporary_preference(time_out, OldTimeOut).

benchmark(4, [synthesis]) :-
    print_enter_benchmark(4),
    setup_scheduler,
    preferences:temporary_set_preference(time_out, 2500, OldTimeOut),
    load_constraint_from_file(prob_examples('public_examples/Synthesis_Tests/constraints/scheduler_inv1.pl'), Constraint),
    benchmark_constraint(Constraint, FastestSolver, Res, TimeDiff),
    asserta(fastest_solver(FastestSolver, Res, TimeDiff)),
    preferences:reset_temporary_preference(time_out, OldTimeOut).

benchmark(5, [synthesis]) :-
    % contradiction
    print_enter_benchmark(5),
    setup_scheduler,
    preferences:temporary_set_preference(time_out, 2500, OldTimeOut),
    load_constraint_from_file(prob_examples('public_examples/Synthesis_Tests/constraints/scheduler_inv2_contradiction.pl'), Constraint),
    benchmark_constraint(Constraint, FastestSolver, Res, TimeDiff),
    asserta(fastest_solver(FastestSolver, Res, TimeDiff)),
    preferences:reset_temporary_preference(time_out, OldTimeOut).

benchmark(6, [synthesis]) :-
    print_enter_benchmark(6),
    setup_scheduler,
    preferences:temporary_set_preference(time_out, 2500, OldTimeOut),
    load_constraint_from_file(prob_examples('public_examples/Synthesis_Tests/constraints/scheduler_inv3.pl'), Constraint),
    benchmark_constraint(Constraint, FastestSolver, Res, TimeDiff),
    asserta(fastest_solver(FastestSolver, Res, TimeDiff)),
    preferences:reset_temporary_preference(time_out, OldTimeOut).

benchmark(7, [synthesis]) :-
    print_enter_benchmark(7),
    setup_scheduler,
    preferences:temporary_set_preference(time_out, 2500, OldTimeOut),
    load_constraint_from_file(prob_examples('public_examples/Synthesis_Tests/constraints/scheduler_inv4.pl'), Constraint),
    benchmark_constraint(Constraint, FastestSolver, Res, TimeDiff),
    asserta(fastest_solver(FastestSolver, Res, TimeDiff)),
    preferences:reset_temporary_preference(time_out, OldTimeOut).

benchmark(8, [synthesis]) :-
    print_enter_benchmark(8),
    setup_scheduler,
    preferences:temporary_set_preference(time_out, 2500, OldTimeOut),
    load_constraint_from_file(prob_examples('public_examples/Synthesis_Tests/constraints/scheduler_new_process.pl'), Constraint),
    benchmark_constraint(Constraint, FastestSolver, Res, TimeDiff),
    asserta(fastest_solver(FastestSolver, Res, TimeDiff)),
    preferences:reset_temporary_preference(time_out, OldTimeOut).

benchmark(9, [synthesis]) :-
    print_enter_benchmark(9),
    setup_scheduler,
    preferences:temporary_set_preference(time_out, 10000, OldTimeOut),
    load_constraint_from_file(prob_examples('public_examples/Synthesis_Tests/constraints/scheduler_delete_process.pl'), Constraint),
    benchmark_constraint(Constraint, FastestSolver, Res, TimeDiff),
    asserta(fastest_solver(FastestSolver, Res, TimeDiff)),
    preferences:reset_temporary_preference(time_out, OldTimeOut).

benchmark(10, [synthesis]) :-
    print_enter_benchmark(10),
    setup_scheduler,
    preferences:temporary_set_preference(time_out, 2500, OldTimeOut),
    load_constraint_from_file(prob_examples('public_examples/Synthesis_Tests/constraints/scheduler_set_active.pl'), Constraint),
    benchmark_constraint(Constraint, FastestSolver, Res, TimeDiff),
    asserta(fastest_solver(FastestSolver, Res, TimeDiff)),
    preferences:reset_temporary_preference(time_out, OldTimeOut).

benchmark(11, [synthesis]) :-
    % Note: DPLL(T) is much faster than ProB if chr_solver preference is set
    print_enter_benchmark(11),
    preferences:temporary_set_preference(time_out, 15000, OldTimeOut),
    setup_scheduler,
    load_constraint_from_file(prob_examples('public_examples/Synthesis_Tests/constraints/scheduler_active_to_waiting_precondition.pl'), Constraint),
    benchmark_constraint(Constraint, FastestSolver, Res, TimeDiff),
    asserta(fastest_solver(FastestSolver, Res, TimeDiff)),
    preferences:reset_temporary_preference(time_out, OldTimeOut).

benchmark(12, [alloy]) :-
    print_enter_benchmark(12),
    alloy2b:load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/alloy_models/toys/grandpa.als.pl')),
    bmachine:b_machine_precompile,
    preferences:temporary_set_preference(time_out, 15000, OldTimeOut),
    load_constraint_from_file(prob_examples('public_examples/Alloy/constraints/alloy_self_grandpas.pl'), Constraint),
    benchmark_constraint(Constraint, FastestSolver, Res, TimeDiff),
    asserta(fastest_solver(FastestSolver, Res, TimeDiff)),
    preferences:reset_temporary_preference(time_out, OldTimeOut).

benchmark(16, [alloy]) :-
    print_enter_benchmark(16),
    alloy2b:load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Puzzles/rivercrossing.pl')),
    bmachine:b_machine_precompile,
    preferences:temporary_set_preference(time_out, 2500, OldTimeOut),
    load_constraint_from_file(prob_examples('public_examples/Alloy/constraints/alloy_river_crossing1.pl'), Constraint),
    benchmark_constraint(Constraint, FastestSolver, Res, TimeDiff),
    asserta(fastest_solver(FastestSolver, Res, TimeDiff)),
    preferences:reset_temporary_preference(time_out, OldTimeOut).

benchmark(17, [alloy]) :-
    print_enter_benchmark(17),
    alloy2b:load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Puzzles/rivercrossing.pl')),
    bmachine:b_machine_precompile,
    preferences:temporary_set_preference(time_out, 20000, OldTimeOut),
    load_constraint_from_file(prob_examples('public_examples/Alloy/constraints/alloy_river_crossing2.pl'), Constraint),
    benchmark_constraint(Constraint, FastestSolver, Res, TimeDiff),
    asserta(fastest_solver(FastestSolver, Res, TimeDiff)),
    preferences:reset_temporary_preference(time_out, OldTimeOut).

benchmark(18, [alloy]) :-
    print_enter_benchmark(18),
    alloy2b:load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Puzzles/rivercrossing.pl')),
    bmachine:b_machine_precompile,
    preferences:temporary_set_preference(time_out, 2500, OldTimeOut),
    load_constraint_from_file(prob_examples('public_examples/Alloy/constraints/alloy_river_crossing3.pl'), Constraint),
    benchmark_constraint(Constraint, FastestSolver, Res, TimeDiff),
    asserta(fastest_solver(FastestSolver, Res, TimeDiff)),
    preferences:reset_temporary_preference(time_out, OldTimeOut).

benchmark(19, [alloy]) :-
    print_enter_benchmark(19),
    alloy2b:load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Puzzles/crewalloc.als.pl')),
    bmachine:b_machine_precompile,
    preferences:temporary_set_preference(time_out, 10000, OldTimeOut),
    load_constraint_from_file(prob_examples('public_examples/Alloy/constraints/alloy_crewalloc1.pl'), Constraint),
    benchmark_constraint(Constraint, FastestSolver, Res, TimeDiff),
    asserta(fastest_solver(FastestSolver, Res, TimeDiff)),
    preferences:reset_temporary_preference(time_out, OldTimeOut).

benchmark(20, [alloy]) :-
    print_enter_benchmark(20),
    alloy2b:load_alloy_ast_prolog_file(prob_examples('public_examples/Alloy/Puzzles/crewalloc.als.pl')),
    bmachine:b_machine_precompile,
    preferences:temporary_set_preference(time_out, 2500, OldTimeOut),
    load_constraint_from_file(prob_examples('public_examples/Alloy/constraints/alloy_crewalloc2.pl'), Constraint),
    benchmark_constraint(Constraint, FastestSolver, Res, TimeDiff),
    asserta(fastest_solver(FastestSolver, Res, TimeDiff)),
    preferences:reset_temporary_preference(time_out, OldTimeOut).

benchmark(21, [misc]) :-
    print_enter_benchmark(21),
    preferences:temporary_set_preference(time_out, 2500, OldTimeOut),
    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,[]),
    benchmark_constraint(Constraint, FastestSolver, Res, TimeDiff),
    asserta(fastest_solver(FastestSolver, Res, TimeDiff)),
    preferences:reset_temporary_preference(time_out, OldTimeOut).

benchmark_constraint(Constraint, FastestSolver, Res, TimeDiff) :-
    preferences:set_preference(randomise_enumeration_order, false),
    format("Solve with ProB..~n", []),
    statistics(walltime, [ProBStart|_]),
    %kodkod_annotator:annotate_kodkod_constraints(greedy, Constraint, AConstraint),
    solve_predicate(Constraint,_,ProBRes), % from solver_interface
    statistics(walltime, [ProBEnd|_]),
    format("~nProB result: ~w~n", [ProBRes]),
    ProBTime is ProBEnd - ProBStart,
    format("ProB finished.~nSolve with DPLL(T)..~n", []),
    statistics(walltime, [DPLLTStart|_]),
    dpllt_solve_predicate(Constraint, _, DPLLTRes),
    statistics(walltime, [DPLLTEnd|_]),
    format("~nDPLL(T) result: ~w~n", [DPLLTRes]),
    format("DPLL(T) finished..~n", []),
    DPLLTTime is DPLLTEnd - DPLLTStart,
    print_times(ProBTime, DPLLTTime),
    !,
    ( ProBRes = solution(_),
    ( DPLLTRes == contradiction_found
    ; DPLLTRes == error),
    format('Error found: ProB found a solution while DPLL(T) did not.', []),
    trace
    ; ProBRes = contradiction_found,
    ( DPLLTRes = solution(_)
    ; DPLLTRes == error),
    format('Error found: ProB found a contradiction while DPLL(T) did not.', []),
    trace
    ; DPLLTRes == time_out,
    ProBRes == time_out,
    Res = time_out,
    FastestSolver = same,
    TimeDiff = 0
    ; ProBRes == time_out,
    solution_or_contradiction(DPLLTRes, Res),
    !,
    FastestSolver = dpllt,
    TimeDiff is ProBTime - DPLLTTime
    ; DPLLTRes == time_out,
    solution_or_contradiction(ProBRes, Res),
    !,
    FastestSolver = prob,
    TimeDiff is DPLLTTime - ProBTime
    ; % ProB could not find a result but DPLL(T)
    ProBRes = no_solution_found(_),
    solution_or_contradiction(DPLLTRes, Res),
    !,
    FastestSolver = dpllt,
    TimeDiff = 0
    ; % DPLL(T) could not find a result but ProB
    DPLLTRes = no_solution_found(_),
    solution_or_contradiction(ProBRes, Res),
    !,
    FastestSolver = prob,
    TimeDiff = 0
    ; DPLLTTime < ProBTime,
    FastestSolver = dpllt,
    solution_or_contradiction(DPLLTRes, Res),
    TimeDiff is ProBTime - DPLLTTime
    ; DPLLTTime > ProBTime,
    FastestSolver = prob,
    solution_or_contradiction(DPLLTRes, Res),
    TimeDiff is DPLLTTime - ProBTime
    ; DPLLTTime == ProBTime,
    FastestSolver = same,
    solution_or_contradiction(DPLLTRes, Res),
    TimeDiff = 0),!.

filter_fastest_solver(Name, LFastestSolver, SolAmount, ContrAmount, TimeoutsAmount, TimeDiff) :-
    findall(TimeDiff, member(Name-solution-TimeDiff, LFastestSolver), Solutions),
    findall(TimeDiff, member(Name-contradiction-TimeDiff, LFastestSolver), Contradictions),
    findall(TimeDiff, member(Name-time_out-TimeDiff, LFastestSolver), Timeouts),
    length(Solutions, SolAmount),
    length(Contradictions, ContrAmount),
    length(Timeouts, TimeoutsAmount),
    sumlist(Solutions, TimeDiff1),
    sumlist(Contradictions, TimeDiff2),
    TimeDiff is TimeDiff1 + TimeDiff2.

get_all_smt2_files(Path, Acc, Files) :-
    directory_exists(Path),
    file_members_of_directory(Path, '*.smt2', Members),
    directory_members_of_directory(Path, Dirs),
    append(Acc, Members, NewAcc),
    map_get_all_smt2_files(Dirs, NewAcc, Files).

load_constraint_from_file(FilePath, Constraint) :-
    file_exists(FilePath),
    !,
    open(FilePath, read, Stream),
    read_term(Stream, Constraint, []),
    close(Stream).

load_constraint_from_file(FilePath, _) :-
    format("File does not exist: ~w~n~n", [FilePath]),
    fail.

map_get_all_smt2_files([], Acc, Acc).

map_get_all_smt2_files([_-Dir|T], Acc, Files) :-
    get_all_smt2_files(Dir, Acc, NewAcc),
    map_get_all_smt2_files(T, NewAcc, Files).

print_complete_benchmarks(LFastestSolver) :-
    filter_fastest_solver(dpllt, LFastestSolver, DplltSol, DplltNoSol, _, DplltTimeDiff),
    filter_fastest_solver(prob, LFastestSolver, ProBSol, ProBNoSol, _, ProBTimeDiff),
    filter_fastest_solver(same, LFastestSolver, SameSol, SameNoSol, SameTimeout, _),
    format("~n~nResults for all benchmarks:~n~nFastest Solver:~nDPLL(T): ~d (solution), ~d (contradiction)~nProB: ~d (solution), ~d (contradiction)~nEqual runtime: ~d (solution), ~d (contradiction), ~d (timeout)~n", [DplltSol,DplltNoSol,ProBSol,ProBNoSol,SameSol,SameNoSol,SameTimeout]),
    ( DplltTimeDiff > ProBTimeDiff
    -> TotalDiff is DplltTimeDiff - ProBTimeDiff,
    format("~nIn total, DPLL(T) is ~d ms faster than ProB.~n", [TotalDiff])
    ; TotalDiff is ProBTimeDiff - DplltTimeDiff,
    format("~nIn total, ProB is ~d ms faster than DPLL(T).~n", [TotalDiff])
).

print_enter_benchmark(Nr) :-
    format("Run benchmark #~d~n---------------------------------------~n", [Nr]).

print_smt_comp_results :-
    findall(smt_stat(FilePath, DplltTime, ProBTime, DplltRes, ProBRes), retract(smt_stat(FilePath, DplltTime, ProBTime, DplltRes, ProBRes)), Stats),
    print_smt_comp_results(Stats).

print_smt_comp_results(Stats) :-
    open('dpllt_benchmarks_smt_comp.txt', write, Stream),
    write(Stream, 'Filepath,Time DPLL(T),Result DPLL(T),Time ProB,Result ProB\n'),
    print_smt_comp_results_to_stream(Stream, Stats).

print_smt_comp_results_to_stream(Stream, []) :-
    close(Stream).

print_smt_comp_results_to_stream(Stream, [Stat|T]) :-
    print_stat_to_stream(Stream, Stat),
    print_smt_comp_results_to_stream(Stream, T).

print_stat_to_stream(Stream, smt_stat(FilePath, dpllt_time(DplltTime), prob_time(ProBTime), dpllt_res(DplltRes), prob_res(ProBRes))) :-
    writeq(Stream, FilePath),write(Stream, ','), writeq(Stream, DplltTime),write(Stream, ','), writeq(Stream, DplltRes),write(Stream, ','),
    writeq(Stream, ProBTime),write(Stream, ','), writeq(Stream, ProBRes),write(Stream, '\n').

print_times(ProBTime, DPLLTTime) :-
    format("ProB: ~w~nDPLL(T) using ProB only: ~w~n", [ProBTime, DPLLTTime]).

reset_benchmarks :-
    retractall(fastest_solver(_, _, _)),!.

run_benchmarks :-
    prob_cli:cli_set_empty_machine,
    reset_benchmarks,
    benchmark(_, _),
    fail.

run_benchmarks :-
    preferences:temporary_set_preference(normalize_ast, true),
    findall(FastestSolver-SolutionOrNot-TimeDiff, fastest_solver(FastestSolver, SolutionOrNot, TimeDiff), LFastestSolver),
    length(LFastestSolver, Results),
    format("~n~n#Results: ~w~n~n", [Results]),
    print_complete_benchmarks(LFastestSolver),
    preferences:reset_temporary_preference(normalize_ast).

run_smt_comp_benchmarks :-
    retractall(smt_stat(_, _, _, _, _)),
    smt_benchmarks_path(Root),
    run_smt_comp_benchmarks(Root),
    print_smt_comp_results.

run_smt_comp_benchmarks(Root) :-
    get_all_smt2_files(Root, [], Files),!,
    run_smt_comp_benchmarks_from_files(Files).

run_smt_comp_benchmarks_from_files(Files) :-
    member(_-FilePath, Files),
    smtlib2_file(FilePath),
    retract(smtlib2_interpreter:stat(DplltTime, ProBTime, DplltRes, ProBRes)),
    asserta(smt_stat(FilePath, DplltTime, ProBTime, DplltRes, ProBRes)),
    format("SMT-lib file path: ~w", [FilePath]),
    fail.

run_smt_comp_benchmarks_from_files(_).

setup_scheduler :-
    bmachine:b_load_machine_from_file(prob_examples('public_examples/Synthesis_Tests/scheduler.mch')),
    bmachine:b_machine_precompile,!.

smt_benchmarks_path('/home/joshua/smt-comp/lia19/psyco').

solution_or_contradiction(solution(_), solution).

solution_or_contradiction(contradiction_found, contradiction).