cdclt_solver_benchmarks

add_benchmark_result(Solver, ConstraintPath, Result) :-
    asserta(benchmark_result(Solver,ConstraintPath,Result)).

amount_of_sat_vars(BenchmarkName, FolderPath, Acc, NewAcc) :-
    write('Eval amount of sat variables for '), write(FolderPath), nl,
    directory_exists(FolderPath),
    file_members_of_directory(FolderPath, FilePaths),
    select_machine_file_path(FilePaths, MachineFilePath, TBenchmarkFilePaths),
    findall(FilePath, (member(_-FilePath, TBenchmarkFilePaths), atom_concat(_, '.eval', FilePath)), BenchmarkFilePaths),
    load_b_eventb_or_tla(MachineFilePath),
    amount_of_sat_vars_for_benchmark(BenchmarkFilePaths, AmountOfSatVars),
    append(Acc, AmountOfSatVars, NewAcc),
    eval_amount_of_sat_vars(BenchmarkName, AmountOfSatVars).

amount_of_sat_vars_bmc :-
    amount_of_sat_vars(bmc, 'benchmarks/abz16_m4/', [], Acc1),
    amount_of_sat_vars(bmc, 'benchmarks/abz16_m5/', Acc1, Acc2),
    amount_of_sat_vars(bmc, 'benchmarks/abz16_m6/', Acc2, Acc3),
    amount_of_sat_vars(bmc, 'benchmarks/abz16_m7/', Acc3, Acc4),
    amount_of_sat_vars(bmc, 'benchmarks/r0_geardoor/', Acc4, Acc5),
    amount_of_sat_vars(bmc, 'benchmarks/r1_valve/', Acc5, Acc6),
    amount_of_sat_vars(bmc, 'benchmarks/r2_outputs/', Acc6, Acc7),
    amount_of_sat_vars(bmc, 'benchmarks/r3_sensors/', Acc7, Acc8),
    amount_of_sat_vars(bmc, 'benchmarks/r4_handle/', Acc8, Acc9),
    amount_of_sat_vars(bmc, 'benchmarks/r5_switch/', Acc9, Acc10),
    amount_of_sat_vars(bmc, 'benchmarks/pm_m0_aai/', Acc10, Acc11),
    amount_of_sat_vars(bmc, 'benchmarks/pm_m0_aat/', Acc11, Acc12),
    amount_of_sat_vars(bmc, 'benchmarks/pm_m0_aoo/', Acc12, Acc13),
    amount_of_sat_vars(bmc, 'benchmarks/pm_m0_voo/', Acc13, Acc14),
    amount_of_sat_vars(bmc, 'benchmarks/pm_m0_vvi/', Acc14, Acc15),
    amount_of_sat_vars(bmc, 'benchmarks/pm_m0_vvt/', Acc15, Acc16),
    amount_of_sat_vars(bmc, 'benchmarks/pm_m1_aoor/', Acc16, Acc17),
    amount_of_sat_vars(bmc, 'benchmarks/pm_m1_voor/', Acc17, Acc18),
    amount_of_sat_vars(bmc, 'benchmarks/pm_m2_aai/', Acc18, Acc19),
    amount_of_sat_vars(bmc, 'benchmarks/simple-two-phase/', Acc19, Acc20),
    amount_of_sat_vars(bmc, 'benchmarks/prisoners-4/', Acc20, Acc21),
    amount_of_sat_vars(bmc, 'benchmarks/bakery/', Acc21, Acc22),
    amount_of_sat_vars(bmc, 'benchmarks/paxos-3/', Acc22, Acc23),
    amount_of_sat_vars(bmc, 'benchmarks/lightbot/', Acc23, Acc24),
    amount_of_sat_vars(bmc, 'benchmarks/travel_agency/', Acc24, Acc25),
    amount_of_sat_vars(bmc, 'benchmarks/search_events/', Acc25, Acc26),
    amount_of_sat_vars(bmc, 'benchmarks/large_branching/', Acc26, Acc27),
    amount_of_sat_vars(bmc, 'benchmarks/r6_lights/', Acc27, Acc28),
    mean_of_list(Acc28, TotalMean),
    median_of_list(Acc28, TotalMedian),
    max_member(Max, Acc28),
    open('amount_of_sat_vars_bmc/total.txt', write, Stream),
    tell(Stream),
    format("Total mean: ~w~nTotal median: ~w~nTotal max: ~w~n", [TotalMean,TotalMedian,Max]),
    close(Stream).

amount_of_sat_vars_deadlock :-
    amount_of_sat_vars(deadlock, 'benchmarks_cbc_deadlock/abz16_m4/', [], Acc1),
    amount_of_sat_vars(deadlock, 'benchmarks_cbc_deadlock/abz16_m5/', Acc1, Acc2),
    amount_of_sat_vars(deadlock, 'benchmarks_cbc_deadlock/abz16_m6/', Acc2, Acc3),
    amount_of_sat_vars(deadlock, 'benchmarks_cbc_deadlock/abz16_m7/', Acc3, Acc4),
    amount_of_sat_vars(deadlock, 'benchmarks_cbc_deadlock/r0_geardoor/', Acc4, Acc5),
    amount_of_sat_vars(deadlock, 'benchmarks_cbc_deadlock/r1_valve/', Acc5, Acc6),
    amount_of_sat_vars(deadlock, 'benchmarks_cbc_deadlock/r2_outputs/', Acc6, Acc7),
    amount_of_sat_vars(deadlock, 'benchmarks_cbc_deadlock/r3_sensors/', Acc7, Acc8),
    amount_of_sat_vars(deadlock, 'benchmarks_cbc_deadlock/r4_handle/', Acc8, Acc9),
    amount_of_sat_vars(deadlock, 'benchmarks_cbc_deadlock/r5_switch/', Acc9, Acc10),
    amount_of_sat_vars(deadlock, 'benchmarks_cbc_deadlock/pm_m0_aai/', Acc10, Acc11),
    amount_of_sat_vars(deadlock, 'benchmarks_cbc_deadlock/pm_m0_aat/', Acc11, Acc12),
    amount_of_sat_vars(deadlock, 'benchmarks_cbc_deadlock/pm_m0_aoo/', Acc12, Acc13),
    amount_of_sat_vars(deadlock, 'benchmarks_cbc_deadlock/pm_m0_voo/', Acc13, Acc14),
    amount_of_sat_vars(deadlock, 'benchmarks_cbc_deadlock/pm_m0_vvi/', Acc14, Acc15),
    amount_of_sat_vars(deadlock, 'benchmarks_cbc_deadlock/pm_m0_vvt/', Acc15, Acc16),
    amount_of_sat_vars(deadlock, 'benchmarks_cbc_deadlock/pm_m1_aoor/', Acc16, Acc17),
    amount_of_sat_vars(deadlock, 'benchmarks_cbc_deadlock/pm_m1_voor/', Acc17, Acc18),
    amount_of_sat_vars(deadlock, 'benchmarks_cbc_deadlock/pm_m2_aai/', Acc18, Acc19),
    amount_of_sat_vars(deadlock, 'benchmarks_cbc_deadlock/simple-two-phase/', Acc19, Acc20),
    amount_of_sat_vars(deadlock, 'benchmarks_cbc_deadlock/prisoners-4/', Acc20, Acc21),
    amount_of_sat_vars(deadlock, 'benchmarks_cbc_deadlock/bakery/', Acc21, Acc22),
    amount_of_sat_vars(deadlock, 'benchmarks_cbc_deadlock/paxos-3/', Acc22, Acc23),
    amount_of_sat_vars(deadlock, 'benchmarks_cbc_deadlock/lightbot/', Acc23, Acc24),
    amount_of_sat_vars(deadlock, 'benchmarks_cbc_deadlock/travel_agency/', Acc24, Acc25),
    amount_of_sat_vars(deadlock, 'benchmarks_cbc_deadlock/search_events/', Acc25, Acc26),
    amount_of_sat_vars(deadlock, 'benchmarks_cbc_deadlock/large_branching/', Acc26, Acc27),
    mean_of_list(Acc27, TotalMean),
    median_of_list(Acc27, TotalMedian),
    max_member(Max, Acc27),
    open('amount_of_sat_vars_deadlock/total.txt', write, Stream),
    tell(Stream),
    format("Total mean: ~w~nTotal median: ~w~nTotal max: ~w~n", [TotalMean,TotalMedian,Max]),
    close(Stream).

amount_of_sat_vars_for_benchmark([], []).

amount_of_sat_vars_for_benchmark([BenchmarkFilePath|T], [AmountOfSatVars|TAmountOfSatVars]) :-
    open(BenchmarkFilePath, read, Stream),
    read(Stream, Constraint),
    close(Stream),
    cdclt_solver:get_amount_of_sat_variables(Constraint, AmountOfSatVars),
    amount_of_sat_vars_for_benchmark(T, TAmountOfSatVars).

amount_of_sat_vars_inductive_inv :-
    amount_of_sat_vars(inductive_inv, 'benchmarks_inductive_inv/abz16_m4/', [], Acc1),
    amount_of_sat_vars(inductive_inv, 'benchmarks_inductive_inv/abz16_m5/', Acc1, Acc2),
    amount_of_sat_vars(inductive_inv, 'benchmarks_inductive_inv/abz16_m6/', Acc2, Acc3),
    amount_of_sat_vars(inductive_inv, 'benchmarks_inductive_inv/abz16_m7/', Acc3, Acc4),
    amount_of_sat_vars(inductive_inv, 'benchmarks_inductive_inv/r0_geardoor/', Acc4, Acc5),
    amount_of_sat_vars(inductive_inv, 'benchmarks_inductive_inv/r1_valve/', Acc5, Acc6),
    amount_of_sat_vars(inductive_inv, 'benchmarks_inductive_inv/r2_outputs/', Acc6, Acc7),
    amount_of_sat_vars(inductive_inv, 'benchmarks_inductive_inv/r3_sensors/', Acc7, Acc8),
    amount_of_sat_vars(inductive_inv, 'benchmarks_inductive_inv/r4_handle/', Acc8, Acc9),
    amount_of_sat_vars(inductive_inv, 'benchmarks_inductive_inv/r5_switch/', Acc9, Acc10),
    amount_of_sat_vars(inductive_inv, 'benchmarks_inductive_inv/pm_m0_aai/', Acc10, Acc11),
    amount_of_sat_vars(inductive_inv, 'benchmarks_inductive_inv/pm_m0_aat/', Acc11, Acc12),
    amount_of_sat_vars(inductive_inv, 'benchmarks_inductive_inv/pm_m0_aoo/', Acc12, Acc13),
    amount_of_sat_vars(inductive_inv, 'benchmarks_inductive_inv/pm_m0_voo/', Acc13, Acc14),
    amount_of_sat_vars(inductive_inv, 'benchmarks_inductive_inv/pm_m0_vvi/', Acc14, Acc15),
    amount_of_sat_vars(inductive_inv, 'benchmarks_inductive_inv/pm_m0_vvt/', Acc15, Acc16),
    amount_of_sat_vars(inductive_inv, 'benchmarks_inductive_inv/pm_m1_aoor/', Acc16, Acc17),
    amount_of_sat_vars(inductive_inv, 'benchmarks_inductive_inv/pm_m1_voor/', Acc17, Acc18),
    amount_of_sat_vars(inductive_inv, 'benchmarks_inductive_inv/pm_m2_aai/', Acc18, Acc19),
    amount_of_sat_vars(inductive_inv, 'benchmarks_inductive_inv/r6_lights/', Acc19, Acc20),
    amount_of_sat_vars(inductive_inv, 'benchmarks_inductive_inv/prisoners-4/', Acc20, Acc21),
    amount_of_sat_vars(inductive_inv, 'benchmarks_inductive_inv/bakery/', Acc21, Acc22),
    amount_of_sat_vars(inductive_inv, 'benchmarks_inductive_inv/paxos-3/', Acc22, Acc23),
    amount_of_sat_vars(inductive_inv, 'benchmarks_inductive_inv/lightbot/', Acc23, Acc24),
    amount_of_sat_vars(inductive_inv, 'benchmarks_inductive_inv/travel_agency/', Acc24, Acc25),
    amount_of_sat_vars(inductive_inv, 'benchmarks_inductive_inv/search_events/', Acc25, Acc26),
    amount_of_sat_vars(inductive_inv, 'benchmarks_inductive_inv/large_branching/', Acc26, Acc27),
    mean_of_list(Acc27, TotalMean),
    median_of_list(Acc27, TotalMedian),
    max_member(Max, Acc27),
    open('amount_of_sat_vars_inductive_inv/total.txt', write, Stream),
    tell(Stream),
    format("Total mean: ~w~nTotal median: ~w~nTotal max: ~w~n", [TotalMean,TotalMedian,Max]),
    close(Stream).

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_misc_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_misc_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_misc_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_misc_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_misc_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_misc_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_misc_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_misc_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_misc_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_misc_constraint(Constraint, FastestSolver, Res, TimeDiff),
    asserta(fastest_solver(FastestSolver, Res, TimeDiff)),
    preferences:reset_temporary_preference(time_out, OldTimeOut).

benchmark(11, [synthesis]) :-
    % Note: CDCL(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_misc_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_misc_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_misc_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_misc_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_misc_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_misc_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_misc_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_misc_constraint(Constraint, FastestSolver, Res, TimeDiff),
    asserta(fastest_solver(FastestSolver, Res, TimeDiff)),
    preferences:reset_temporary_preference(time_out, OldTimeOut).

benchmark_constraint(UseIdlSolver, _, ConstraintPath, TimeZ3, TimeCdclt, TimeCdcltRaw, TimeCdcltIdl, TimeCdcltNoSym, TimeCdcltRawSym, TimeProB, RestartsCdclt, RestartsCdcltRaw, RestartsCdcltIdl, RestartsCdcltNoSym, RestartsCdcltRawSym) :-
    bmc_timeout(Timeout),
    open(ConstraintPath, read, Stream),
    read(Stream, Constraint),
    close(Stream),
    write(ConstraintPath),nl,
    %translate:print_bexpr(Constraint),nl,
    preferences:set_preference(time_out, Timeout),
    set_preference(cdclt_use_idl_theory_solver, false),
    set_preference(cdclt_perform_static_analysis, false),
    set_preference(cdclt_perform_symmetry_breaking, true),
    cdclt_solver:init,
    write('Solve with Sym-Raw-SMT..'),nl,
    write(ConstraintPath),nl,
    statistics(walltime, [StartCdcltRawSym|_]),
    cdclt_solve_predicate(sym_raw_smt, Constraint, _SolvedPred1, ResCdcltRawSym),
    %ResCdcltRawSym = no_solution_found(solver_answered_unknown),
    statistics(walltime, [StopCdcltRawSym|_]),
    (cdclt_sat_solver:restarts(RestartsCdcltRawSym); RestartsCdcltRawSym = 0),
    format("Restarts: ~w~n", [RestartsCdcltRawSym]),
    TimeCdcltRawSym is StopCdcltRawSym - StartCdcltRawSym,
    ( solved_constraint(ResCdcltRawSym)
    -> inc_solved_counter(sym_raw_smt),
    add_benchmark_result(sym_raw_smt, ConstraintPath, ResCdcltRawSym)
    ; true
    ),
    nl,nl,write(ResCdcltRawSym),nl,nl,
    write('done.'), nl,
    set_preference(cdclt_perform_static_analysis, true),
    cdclt_solver:init,
    write('Solve with Sym-SMT..'),nl,
    write(ConstraintPath),nl,
    statistics(walltime, [StartCdclt|_]),
    cdclt_solve_predicate(sym_smt, Constraint, _SolvedPred2, ResCdclt),
    %ResCdclt = no_solution_found(solver_answered_unknown),
    statistics(walltime, [StopCdclt|_]),
    (cdclt_sat_solver:restarts(RestartsCdclt); RestartsCdclt = 0),
    format("Restarts: ~w~n", [RestartsCdclt]),
    TimeCdclt is StopCdclt - StartCdclt,
    ( solved_constraint(ResCdclt)
    -> inc_solved_counter(sym_smt),
    add_benchmark_result(sym_smt, ConstraintPath, ResCdclt)
    ; true
    ),
    nl,nl,write(ResCdclt),nl,nl,
    write('done.'), nl,
    preferences:set_preference(time_out, Timeout),
    ( UseIdlSolver
    -> set_preference(cdclt_perform_symmetry_breaking, false),
    set_preference(cdclt_use_idl_theory_solver, true),
    cdclt_solver:init,
    write('Solve with IDL-SMT..'),nl,
    statistics(walltime, [StartCdcltIdl|_]),
    cdclt_solve_predicate(idl_smt, Constraint, _SolvedPred3, ResCdcltIdl),
    statistics(walltime, [StopCdcltIdl|_]),
    (cdclt_sat_solver:restarts(RestartsCdcltIdl); RestartsCdcltIdl = 0),
    format("Restarts: ~w~n", [RestartsCdcltIdl]),
    TimeCdcltIdl is StopCdcltIdl - StartCdcltIdl,
    ( solved_constraint(ResCdcltIdl)
    -> inc_solved_counter(idl_smt),
    add_benchmark_result(idl_smt, ConstraintPath, ResCdcltIdl)
    ; true
    ),
    set_preference(cdclt_use_idl_theory_solver, false),
    set_preference(cdclt_perform_symmetry_breaking, true)
    ; TimeCdcltIdl = 0,
    RestartsCdcltIdl = 0,
    ResCdcltIdl = none
    ),
    nl,nl,write(ResCdcltIdl),nl,nl,
    write('done.'), nl,
   
    preferences:set_preference(time_out, Timeout),
    set_preference(cdclt_perform_symmetry_breaking, false),
    cdclt_solver:init,
    write('Solve with SMT..'),nl,
    write(ConstraintPath),nl,
    statistics(walltime, [StartCdcltNoSym|_]),
    cdclt_solve_predicate(smt, Constraint, _, ResCdcltNoSym),
    %ResCdcltNoSym = no_solution_found(solver_answered_unknown),
    statistics(walltime, [StopCdcltNoSym|_]),
    (cdclt_sat_solver:restarts(RestartsCdcltNoSym); RestartsCdcltNoSym = 0),
    format("Restarts: ~w~n", [RestartsCdcltNoSym]),
    TimeCdcltNoSym is StopCdcltNoSym - StartCdcltNoSym,
    ( solved_constraint(ResCdcltNoSym)
    -> inc_solved_counter(smt),
    add_benchmark_result(smt, ConstraintPath, ResCdcltNoSym)
    ; true
    ),
    nl,nl,write(ResCdcltNoSym),nl,nl,
    write('done.'), nl,
    preferences:set_preference(time_out, Timeout),
   
    set_preference(cdclt_perform_static_analysis, false),
    set_preference(cdclt_perform_symmetry_breaking, false),
    cdclt_solver:init,
    write('Solve with Raw-SMT..'),nl,
    write(ConstraintPath),nl,
    statistics(walltime, [StartCdcltRaw|_]),
    cdclt_solve_predicate(raw_smt, Constraint, _, ResCdcltRaw),
    %ResCdcltRaw = no_solution_found(solver_answered_unknown),
    statistics(walltime, [StopCdcltRaw|_]),
    (cdclt_sat_solver:restarts(RestartsCdcltRaw); RestartsCdcltRaw = 0),
    format("Restarts: ~w~n", [RestartsCdcltRaw]),
    TimeCdcltRaw is StopCdcltRaw - StartCdcltRaw,
    ( solved_constraint(ResCdcltRaw)
    -> inc_solved_counter(raw_smt),
    add_benchmark_result(raw_smt, ConstraintPath, ResCdcltRaw)
    ; true
    ),
    nl,nl,write(ResCdcltRaw),nl,nl,
    write('done.'), nl,
    preferences:set_preference(time_out, Timeout),
    set_preference(cdclt_perform_static_analysis,true),
    set_preference(cdclt_perform_symmetry_breaking,true),
   
    write('Solve with Z3..'),nl,
    write(ConstraintPath),nl,
    statistics(walltime, [StartZ3|_]),
    smt_solve_predicate(z3,Constraint, _, ResZ3),
    %ResZ3 = no_solution_found(solver_answered_unknown),
    statistics(walltime, [StopZ3|_]),
    TimeZ3 is StopZ3 - StartZ3,
    ( solved_constraint(ResZ3)
    -> inc_solved_counter(z3),
    add_benchmark_result(z3, ConstraintPath, ResZ3)
    ; true
    ),
    nl,nl,write(ResZ3),nl,nl,
    preferences:set_preference(time_out, Timeout),
    write('Solve with ProB..'),nl,
    write(ConstraintPath),nl,
    statistics(walltime, [StartProB|_]),
    solve_predicate(Constraint, _, ResProB),
    %ResProB = no_solution_found(solver_answered_unknown),
    statistics(walltime, [StopProB|_]),
    TimeProB is StopProB - StartProB,
    ( solved_constraint(ResProB)
    -> inc_solved_counter(prob),
    add_benchmark_result(prob, ConstraintPath, ResProB)
    ; true
    ),
    nl,nl,write(ResProB),nl,nl,
    write('done.'), nl.

benchmark_constraints(_, _, [], Acc, Acc).

benchmark_constraints(UseIdlSolver, Timeout, [ConstraintPath|T], Acc, Data) :-
    benchmark_constraint(UseIdlSolver, Timeout, ConstraintPath, TimeZ3, TimeCdclt, TimeCdcltRaw, TimeCdcltIdl, TimeCdcltNoSym, TimeCdcltRawSym, TimeProB, RestartsCdclt, RestartsCdcltRaw, RestartsCdcltIdl, RestartsCdcltNoSym, RestartsCdcltRawSym), !,
    benchmark_constraints(UseIdlSolver, Timeout, T, [(ConstraintPath,TimeZ3,TimeCdclt,TimeCdcltRaw,TimeCdcltIdl,TimeCdcltNoSym,TimeCdcltRawSym,TimeProB,RestartsCdclt,RestartsCdcltRaw,RestartsCdcltIdl,RestartsCdcltNoSym,RestartsCdcltRawSym)|Acc], Data).

benchmark_misc_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 CDCL(T)..~n", []),
    statistics(walltime, [CDCLTStart|_]),
    cdclt_solve_predicate(Constraint, _, CDCLTRes),
    statistics(walltime, [CDCLTEnd|_]),
    format("~nCDCL(T) result: ~w~n", [CDCLTRes]),
    format("CDCL(T) finished..~n", []),
    CDCLTTime is CDCLTEnd - CDCLTStart,
    print_times(ProBTime, CDCLTTime),
    !,
    ( ProBRes = solution(_),
    ( CDCLTRes == contradiction_found
    ; CDCLTRes == error),
    format('Error found: ProB found a solution while CDCL(T) did not.', []),
    trace
    ; ProBRes = contradiction_found,
    ( CDCLTRes = solution(_)
    ; CDCLTRes == error),
    format('Error found: ProB found a contradiction while CDCL(T) did not.', []),
    trace
    ; CDCLTRes == time_out,
    ProBRes == time_out,
    Res = time_out,
    FastestSolver = same,
    TimeDiff = 0
    ; ProBRes == time_out,
    solution_or_contradiction(CDCLTRes, Res),
    !,
    FastestSolver = cdclt,
    TimeDiff is ProBTime - CDCLTTime
    ; CDCLTRes == time_out,
    solution_or_contradiction(ProBRes, Res),
    !,
    FastestSolver = prob,
    TimeDiff is CDCLTTime - ProBTime
    ; % ProB could not find a result but CDCL(T)
    ProBRes = no_solution_found(_),
    solution_or_contradiction(CDCLTRes, Res),
    !,
    FastestSolver = cdclt,
    TimeDiff = 0
    ; % CDCL(T) could not find a result but ProB
    CDCLTRes = no_solution_found(_),
    solution_or_contradiction(ProBRes, Res),
    !,
    FastestSolver = prob,
    TimeDiff = 0
    ; CDCLTTime < ProBTime,
    FastestSolver = cdclt,
    solution_or_contradiction(CDCLTRes, Res),
    TimeDiff is ProBTime - CDCLTTime
    ; CDCLTTime > ProBTime,
    FastestSolver = prob,
    solution_or_contradiction(CDCLTRes, Res),
    TimeDiff is CDCLTTime - ProBTime
    ; CDCLTTime == ProBTime,
    FastestSolver = same,
    solution_or_contradiction(CDCLTRes, Res),
    TimeDiff = 0),!.

bmc_timeout(120000).

deadlock_timeout(120000).

eval_amount_of_sat_vars(BenchmarkName, AmountOfSatVars) :-
    bmachine:b_machine_name(MachineName),
    atom_concat(MachineName, 'amount_of_sat_vars.txt', OutPath1),
    atom_concat('amount_of_sat_vars_', BenchmarkName, OutFolder1),
    atom_concat(OutFolder1, '/', OutFolder),
    atom_concat(OutFolder, OutPath1, OutPath),
    mean_of_list(AmountOfSatVars, MeanAmountOfSatVars),
    median_of_list(AmountOfSatVars, MedianAmountOfSatVars),
    open(OutPath, write, Stream),
    tell(Stream),
    format("AmountOfSatVarsList: ~w~nMean: ~w~nMedian: ~w~n", [AmountOfSatVars, MeanAmountOfSatVars, MedianAmountOfSatVars]),
    close(Stream).

eval_benchmark_data(MachineName, Description, Data) :-
    format("Evaluate benchmarks ~w~n", [Description]),
    findall(TimeZ3, member((_,TimeZ3,_,_,_,_,_,_,_,_,_,_), Data), TimesZ3),
    findall(TimeCdclt, member((_,_,TimeCdclt,_,_,_,_,_,_,_,_,_), Data), TimesCdclt),
    findall(TimeCdcltRaw, member((_,_,_,TimeCdcltRaw,_,_,_,_,_,_,_,_,_), Data), TimesCdcltRaw),
    findall(TimeCdcltIdl, member((_,_,_,_,TimeCdcltIdl,_,_,_,_,_,_,_,_), Data), TimesCdcltIdl),
    findall(TimeCdcltNoSym, member((_,_,_,_,_,TimeCdcltNoSym,_,_,_,_,_,_,_), Data), TimesCdcltNoSym),
    findall(TimeCdcltRawSym, member((_,_,_,_,_,_,TimeCdcltRawSym,_,_,_,_,_,_), Data), TimesCdcltRawSym),
    findall(TimeProB, member((_,_,_,_,_,_,_,TimeProB,_,_,_,_,_), Data), TimesProB),
    findall(RestartCdclt, member((_,_,_,_,_,_,_,_,RestartCdclt,_,_,_,_), Data), RestartsCdclt),
    findall(RestartCdcltRaw, member((_,_,_,_,_,_,_,_,_,RestartCdcltRaw,_,_), Data), RestartsCdcltRaw),
    findall(RestartCdcltIdl, member((_,_,_,_,_,_,_,_,_,_,RestartCdcltIdl,_,_), Data), RestartsCdcltIdl),
    findall(RestartCdcltNoSym, member((_,_,_,_,_,_,_,_,_,_,_,RestartCdcltNoSym,_), Data), RestartsCdcltNoSym),
    findall(RestartCdcltRawSym, member((_,_,_,_,_,_,_,_,_,_,_,_,RestartCdcltRawSym), Data), RestartsCdcltRawSym),
    sumlist(TimesZ3, TimeZ3),
    sumlist(TimesCdclt, TimeCdclt),
    sumlist(TimesCdcltRaw, TimeCdcltRaw),
    sumlist(TimesCdcltIdl, TimeCdcltIdl),
    sumlist(TimesCdcltNoSym, TimeCdcltNoSym),
    sumlist(TimesCdcltRawSym, TimeCdcltRawSym),
    sumlist(TimesProB, TimeProB),
    sumlist(RestartsCdclt, RestartCdclt),
    sumlist(RestartsCdcltRaw, RestartCdcltRaw),
    sumlist(RestartsCdcltIdl, RestartCdcltIdl),
    sumlist(RestartsCdcltNoSym, RestartCdcltNoSym),
    sumlist(RestartsCdcltRawSym, RestartCdcltRawSym),
    atom_concat('benchmarks_cdclt_journal/', MachineName, Path1),
    atom_concat(Path1, '_results.txt', EvalFilePath),
    nl,nl,write('eval'),nl,
    write(EvalFilePath),nl,nl,
    open(EvalFilePath, write, Stream),
    tell(Stream),
    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]),
    findall(TO, (solved_constraints(A,B), TO = solved_constraints(A,B)), TOs),
    (member(solved_constraints(prob,SolvedProB), TOs); SolvedProB = 0),
    (member(solved_constraints(z3,SolvedZ3), TOs); SolvedZ3 = 0),
    (member(solved_constraints(smt,SolvedSMT), TOs); SolvedSMT = 0),
    (member(solved_constraints(raw_smt,SolvedRawSMT), TOs); SolvedRawSMT = 0),
    (member(solved_constraints(sym_smt,SolvedSymSMT), TOs); SolvedSymSMT = 0),
    (member(solved_constraints(sym_raw_smt,SolvedSymRawSMT), TOs); SolvedSymRawSMT = 0),
    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]),
    nl, write(TOs), nl,
    close(Stream).

eval_benchmark_data_csv(MachineName, Description, Data) :-
    format("Evaluate benchmarks ~w for detailed CSV~n", [Description]),
    findall((ConstraintPath,TimeZ3), member((ConstraintPath,TimeZ3,_,_,_,_,_,_,_,_,_,_), Data), DataZ3),
    findall((ConstraintPath,TimeCdclt), member((ConstraintPath,_,TimeCdclt,_,_,_,_,_,_,_,_,_), Data), DataCdclt),
    findall((ConstraintPath,TimeCdcltRaw), member((ConstraintPath,_,_,TimeCdcltRaw,_,_,_,_,_,_,_,_,_), Data), DataCdcltRaw),
    %findall((ConstraintPath,TimeCdcltIdl), member((ConstraintPath,_,_,_,TimeCdcltIdl,_,_,_,_,_,_,_,_), Data), DataCdcltIdl),
    findall((ConstraintPath,TimeCdcltNoSym), member((ConstraintPath,_,_,_,_,TimeCdcltNoSym,_,_,_,_,_,_,_), Data), DataCdcltNoSym),
    findall((ConstraintPath,TimeCdcltRawSym), member((ConstraintPath,_,_,_,_,_,TimeCdcltRawSym,_,_,_,_,_,_), Data), DataCdcltRawSym),
    findall((ConstraintPath,TimeProB), member((ConstraintPath,_,_,_,_,_,_,TimeProB,_,_,_,_,_), Data), DataProB),
    write_to_csv(z3, MachineName, DataZ3),
    write_to_csv(prob, MachineName, DataProB),
    write_to_csv(smt, MachineName, DataCdcltNoSym),
    write_to_csv(sym_smt, MachineName, DataCdclt),
    write_to_csv(raw_smt, MachineName, DataCdcltRaw),
    write_to_csv(sym_raw_smt, MachineName, DataCdcltRawSym).

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) :-
    atom_concat(FileNameNoExt, '.eval', FileName),
    atom_concat('benchmark_results_', FileNameNoExt, TResultsPath),
    atom_concat(TResultsPath, '.txt', TTResultsPath),
    atom_concat(FolderPath, TTResultsPath, ResultsPath),
    open(ResultsPath, write, Stream),
    tell(Stream),
    writeq(BenchmarkFilePath),nl,nl,
    format("CDCLT-Res: ~w~nCDCLT-Time: ~w~nCDCLT-Restarts: ~w~n", [ResCdclt,TimeCdclt,RestartsCdclt]),
    format("CDCLT-No-Sym-Res: ~w~nCDCLT-No-Sym-Time: ~w~nCDCLT-No-Sym-Restarts: ~w~n", [ResCdcltNoSym,TimeCdcltNoSym,RestartsCdcltNoSym]),
    format("CDCLT-Idl-Res: ~w~nCDCLT-Idl-Time: ~w~nCDCLT-Idl-Restarts: ~w~n", [ResCdcltIdl,TimeCdcltIdl,RestartsCdcltIdl]),
    format("CDCLT-Raw-Res: ~w~nCDCLT-Raw-Time: ~w~nCDCLT-Raw-Restarts: ~w~n", [ResCdcltRaw,TimeCdcltRaw,RestartsCdcltRaw]),
    format("CDCLT-Sym-Raw-Res: ~w~nCDCLT-Sym-Raw-Time: ~w~nCDCLT-Sym-Raw-Restarts: ~w~n", [ResCdcltRawSym,TimeCdcltRawSym,RestartsCdcltRawSym]),
    format("Z3-Res: ~w~nZ3-Time: ~w~n", [ResZ3,TimeZ3]),
    format("ProB-Res: ~w~nProB-Time: ~w~n", [ResProB,TimeProB]),
    close(Stream),
    !.

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_file_paths_from_config(ConfigPath, MachineFile, ConstraintPaths, Description, MachineName) :-
    open(ConfigPath, read, Stream),
    read(Stream, Config),
    close(Stream),
    Config = benchmark_config(Description, MachineFile, MachineName, MaxBound),
    int_range(0, MaxBound, KRange),
    findall(ConstraintPath,
    (member(K, KRange), atom_concat(MachineName, '_monolithic_bmc_k_', T1),
    number_codes(K, CK), atom_codes(AK, CK),
    atom_concat(T1, AK, T2), atom_concat(T2, '.eval', ConstraintPath)),
    ConstraintPaths).

inc_solved_counter(Solver) :-
    (retract(solved_constraints(Solver, Old)); Old = 0),
    !,
    New is Old + 1,
    asserta(solved_constraints(Solver, New)).

inductive_inv_timeout(120000).

int_range(C, B, R) :-
    C == B,
    !,
    R = [C].

int_range(C, B, [C|T]) :-
    C1 is C + 1,
    int_range(C1, B, T).

is_eventb_machine(MachineFile) :-
    atom_concat(_, '.eventb', MachineFile).

is_tla_file(File) :-
    atom_concat(_, '.tla', File).

load_b_eventb_or_tla(MachineFilePath) :-
    ( is_eventb_machine(MachineFilePath)
    -> b_load_eventb_project(MachineFilePath)
    ; is_tla_file(MachineFilePath)
    -> call_tla2b_parser(MachineFilePath),
    atom_concat(PrefixPath, '.tla', MachineFilePath),
    atom_concat(PrefixPath, '.prob', BMachinePath),
    b_load_machine_probfile(BMachinePath)
    ; b_load_machine_from_file(MachineFilePath)
    ),
    b_machine_precompile.

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.

mean_of_list([], M) :-
    !,
    M = 0.

mean_of_list(L, M) :-
    length(L, Len),
    sumlist(L, Sum),
    M is Sum / Len.

median_of_list(L, M) :-
    length(L, Len),
    sort(L, LS),
    ( LS = [E]
    -> M = E
    ; Len21 is floor(Len / 2),
    Len22 is ceiling(Len / 2),
    ( Len21 \== Len22
    -> nth1(Len22, L, M)
    ; nth1(Len21, L, M1),
    Len211 is Len21 + 1,
    nth1(Len211, L, M2),
    M is (M1+M2)/2
)
).

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.

p(L) :-
    writeq(L), nl,
    L = [_AmountOfSatVars,(prob,N,TimeProB,_FResProB),(z3,N,TimeZ3,_FResZ3),(sym_smt,N,TimeCdclt,_FResCdclt)],
    format("~w & ~w & ~w & ~w & ~n", [N,TimeProB,TimeZ3,TimeCdclt]).

print_complete_benchmarks(LFastestSolver) :-
    filter_fastest_solver(cdclt, LFastestSolver, CdcltSol, CdcltNoSol, _, CdcltTimeDiff),
    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:~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]),
    ( CdcltTimeDiff > ProBTimeDiff
    -> TotalDiff is CdcltTimeDiff - ProBTimeDiff,
    format("~nIn total, CDCL(T) is ~d ms faster than ProB.~n", [TotalDiff])
    ; TotalDiff is ProBTimeDiff - CdcltTimeDiff,
    format("~nIn total, ProB is ~d ms faster than CDCL(T).~n", [TotalDiff])
).

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

print_n_queens_data(Data) :-
    maplist(p, Data).

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

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

run_bmc_benchmarks(UseIdlSolver, DirPath) :-
    retractall(solved_constraints(_,_)),
    retractall(benchmark_result(_,_,_)),
    atom_concat(DirPath, 'benchmark_config.pl', ConfigPath),
    get_file_paths_from_config(ConfigPath, MachineFile, ConstraintPaths, Description, MachineName),
    format("Run benchmarks ~w~n", [Description]),
    atom_concat(DirPath, MachineFile, MachinePath),
    load_b_eventb_or_tla(MachinePath),
    maplist(atom_concat(DirPath), ConstraintPaths, FullConstraintPaths),
    get_preference(time_out, Timeout),
    retractall(cdclt_sat_solver:incremental_mode),
    benchmark_constraints(UseIdlSolver, Timeout, FullConstraintPaths, [], Data),
    retractall(cdclt_sat_solver:memoize_backjump_clause(_, _, _)),
    eval_benchmark_data(MachineName, Description, Data),
    eval_benchmark_data_csv(MachineName, Description, Data).

run_bmc_benchmarks1 :-
    bmc_timeout(Timeout),
    preferences:set_preference(time_out, Timeout),
    %run_bmc_benchmarks(false, 'benchmarks/paxos-5/'),
    %run_bmc_benchmarks(false, 'benchmarks/abz16_m0/'),
    /*run_bmc_benchmarks(false, 'benchmarks/abz16_m1/'),
    run_bmc_benchmarks(false, 'benchmarks/abz16_m2/'),
    run_bmc_benchmarks(false, 'benchmarks/abz16_m3/'),*/
    run_bmc_benchmarks(false, 'benchmarks/abz16_m6/'),
    run_bmc_benchmarks(false, 'benchmarks/abz16_m7/'),
    run_bmc_benchmarks(false, 'benchmarks/abz16_m4/'),
    run_bmc_benchmarks(false, 'benchmarks/abz16_m5/').

run_bmc_benchmarks2 :-
    bmc_timeout(Timeout),
    preferences:set_preference(time_out, Timeout),
    run_bmc_benchmarks(false, 'benchmarks/r4_handle/'),
    run_bmc_benchmarks(false, 'benchmarks/r5_switch/'),
    run_bmc_benchmarks(false, 'benchmarks/r6_lights/'),
    run_bmc_benchmarks(false, 'benchmarks/r0_geardoor/'),
    run_bmc_benchmarks(false, 'benchmarks/r1_valve/'),
    run_bmc_benchmarks(false, 'benchmarks/r2_outputs/'),
    run_bmc_benchmarks(false, 'benchmarks/r3_sensors/').

run_bmc_benchmarks3 :-
    bmc_timeout(Timeout),
    preferences:set_preference(time_out, Timeout),
    run_bmc_benchmarks(false, 'benchmarks/pm_m0_aai/'),
    run_bmc_benchmarks(false, 'benchmarks/pm_m0_aat/'),
    run_bmc_benchmarks(false, 'benchmarks/pm_m0_aoo/'),
    run_bmc_benchmarks(false, 'benchmarks/pm_m0_voo/'),
    run_bmc_benchmarks(false, 'benchmarks/pm_m0_vvi/').

run_bmc_benchmarks4 :-
    bmc_timeout(Timeout),
    preferences:set_preference(time_out, Timeout),
    run_bmc_benchmarks(false, 'benchmarks/pm_m0_vvt/'),
    run_bmc_benchmarks(false, 'benchmarks/pm_m1_aoor/'),
    run_bmc_benchmarks(false, 'benchmarks/pm_m1_voor/'),
    run_bmc_benchmarks(false, 'benchmarks/pm_m2_aai/').

run_bmc_benchmarks5 :-
    bmc_timeout(Timeout),
    preferences:set_preference(time_out, Timeout),
    run_bmc_benchmarks(false, 'benchmarks/simple-two-phase/'),
    run_bmc_benchmarks(false, 'benchmarks/lightbot/'),
    run_bmc_benchmarks(false, 'benchmarks/travel_agency/'),
    run_bmc_benchmarks(false, 'benchmarks/search_events/').

run_bmc_benchmarks6 :-
    bmc_timeout(Timeout),
    preferences:set_preference(time_out, Timeout),
    run_bmc_benchmarks(false, 'benchmarks/large_branching/'),
    run_bmc_benchmarks(false, 'benchmarks/prisoners-4/'),
    run_bmc_benchmarks(false, 'benchmarks/bakery/'),
    run_bmc_benchmarks(false, 'benchmarks/paxos-3/').

run_cbc_benchmark(UseIdlSolver, FolderPath, FileName-BenchmarkFilePath, Constraint) :-
    inductive_inv_timeout(Timeout),
    preferences:set_preference(time_out, Timeout),
    set_preference(cdclt_use_idl_theory_solver, false),
    set_preference(cdclt_perform_static_analysis, false),
    set_preference(cdclt_perform_symmetry_breaking, true),
    cdclt_solver:init,
    write('Solve with Sym-Raw-SMT..'),nl,
    writeq(BenchmarkFilePath),nl,
    statistics(walltime, [StartCdcltRawSym|_]),
    cdclt_solve_predicate(Constraint, _, ResCdcltRawSym),
    statistics(walltime, [StopCdcltRawSym|_]),
    (cdclt_sat_solver:restarts(RestartsCdcltRawSym); RestartsCdcltRawSym = 0),
    TimeCdcltRawSym is StopCdcltRawSym - StartCdcltRawSym,
    nl,nl,write(ResCdcltRawSym),nl,nl,
   
    write('done.'), nl,
    set_preference(cdclt_perform_static_analysis, true),
    cdclt_solver:init,
    write('Solve with Sym-SMT..'),nl,
    writeq(BenchmarkFilePath),nl,
    statistics(walltime, [StartCdclt|_]),
    cdclt_solve_predicate(Constraint, _, ResCdclt),
    statistics(walltime, [StopCdclt|_]),
    (cdclt_sat_solver:restarts(RestartsCdclt); RestartsCdclt = 0),
    TimeCdclt is StopCdclt - StartCdclt,
    nl,nl,write(ResCdclt),nl,nl,
   
    write('done.'), nl,
    preferences:set_preference(time_out, Timeout),
    ( UseIdlSolver
    -> set_preference(cdclt_perform_symmetry_breaking,false),
    set_preference(cdclt_use_idl_theory_solver,true),
    cdclt_solver:init,
    write('Solve with IDL-SMT..'),nl,
    writeq(BenchmarkFilePath),nl,
    statistics(walltime, [StartCdcltIdl|_]),
    cdclt_solve_predicate(Constraint, _, ResCdcltIdl),
    statistics(walltime, [StopCdcltIdl|_]),
    (cdclt_sat_solver:restarts(RestartsCdcltIdl); RestartsCdcltIdl = 0),
    TimeCdcltIdl is StopCdcltIdl - StartCdcltIdl,
    set_preference(cdclt_use_idl_theory_solver,false),
    set_preference(cdclt_perform_symmetry_breaking,true)
    ; TimeCdcltIdl = 0,
    RestartsCdcltIdl = 0,
    ResCdcltIdl = none
    ),
    nl,nl,write(ResCdcltIdl),nl,nl,
    write('done.'), nl,
   
    preferences:set_preference(time_out, Timeout),
    set_preference(cdclt_perform_symmetry_breaking,false),
    cdclt_solver:init,
    write('Solve with SMT..'),nl,
    writeq(BenchmarkFilePath),nl,
    statistics(walltime, [StartCdcltNoSym|_]),
    cdclt_solve_predicate(Constraint, _, ResCdcltNoSym),
    statistics(walltime, [StopCdcltNoSym|_]),
    (cdclt_sat_solver:restarts(RestartsCdcltNoSym); RestartsCdcltNoSym = 0),
    TimeCdcltNoSym is StopCdcltNoSym - StartCdcltNoSym,
    nl,nl,write(ResCdcltNoSym),nl,nl,
    write('done.'), nl,
    preferences:set_preference(time_out, Timeout),
   
    set_preference(cdclt_perform_static_analysis,false),
    set_preference(cdclt_perform_symmetry_breaking,false),
    cdclt_solver:init,
    write('Solve with Raw-SMT..'),nl,
    writeq(BenchmarkFilePath),nl,
    statistics(walltime, [StartCdcltRaw|_]),
    cdclt_solve_predicate(Constraint, _, ResCdcltRaw),
    statistics(walltime, [StopCdcltRaw|_]),
    (cdclt_sat_solver:restarts(RestartsCdcltRaw); RestartsCdcltRaw = 0),
    TimeCdcltRaw is StopCdcltRaw - StartCdcltRaw,
    nl,nl,write(ResCdcltRaw),nl,nl,
    write('done.'), nl,
    preferences:set_preference(time_out, Timeout),
   
    write('Solve with Z3..'),nl,
    writeq(BenchmarkFilePath),nl,
    %translate:print_bexpr(Constraint),nl,
    statistics(walltime, [StartZ3|_]),
    smt_solve_predicate(z3,Constraint, _, ResZ3),
    %ResZ3 = no_solution_found(solver_answered_unknown),
    statistics(walltime, [StopZ3|_]),
    TimeZ3 is StopZ3 - StartZ3,
    nl,nl,write(ResZ3),nl,nl,
    preferences:set_preference(time_out, Timeout),
   
    write('Solve with ProB..'),nl,
    writeq(BenchmarkFilePath),nl,
    statistics(walltime, [StartProB|_]),
    solve_predicate(Constraint, _, ResProB),
    %ResProB = no_solution_found(solver_answered_unknown),
    statistics(walltime, [StopProB|_]),
    TimeProB is StopProB - StartProB,
    nl,nl,write(ResProB),nl,nl,
    write('done.'), nl,
    !,
    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).