dpllt_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),
    dpllt_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_constraint(UseIdlSolver, _, ConstraintPath, TimeZ3, TimeDpllt, TimeDplltRaw, TimeDplltIdl, TimeDplltNoSym, TimeDplltRawSym, TimeProB, RestartsDpllt, RestartsDplltRaw, RestartsDplltIdl, RestartsDplltNoSym, RestartsDplltRawSym) :-
    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(dpllt_use_idl_theory_solver, false),
    set_preference(dpllt_perform_static_analysis, false),
    set_preference(dpllt_perform_symmetry_breaking, true),
    dpllt_solver:init,
    write('Solve with Sym-Raw-SMT..'),nl,
    write(ConstraintPath),nl,
    statistics(walltime, [StartDplltRawSym|_]),
    dpllt_solve_predicate(sym_raw_smt, Constraint, _SolvedPred1, ResDplltRawSym),
    %ResDplltRawSym = no_solution_found(solver_answered_unknown),
    statistics(walltime, [StopDplltRawSym|_]),
    (dpllt_sat_solver:restarts(RestartsDplltRawSym); RestartsDplltRawSym = 0),
    format("Restarts: ~w~n", [RestartsDplltRawSym]),
    TimeDplltRawSym is StopDplltRawSym - StartDplltRawSym,
    ( solved_constraint(ResDplltRawSym)
    -> inc_solved_counter(sym_raw_smt),
    add_benchmark_result(sym_raw_smt, ConstraintPath, ResDplltRawSym)
    ; true
    ),
    nl,nl,write(ResDplltRawSym),nl,nl,
    write('done.'), nl,
    set_preference(dpllt_perform_static_analysis, true),
    dpllt_solver:init,
    write('Solve with Sym-SMT..'),nl,
    write(ConstraintPath),nl,
    statistics(walltime, [StartDpllt|_]),
    dpllt_solve_predicate(sym_smt, Constraint, _SolvedPred2, ResDpllt),
    %ResDpllt = no_solution_found(solver_answered_unknown),
    statistics(walltime, [StopDpllt|_]),
    (dpllt_sat_solver:restarts(RestartsDpllt); RestartsDpllt = 0),
    format("Restarts: ~w~n", [RestartsDpllt]),
    TimeDpllt is StopDpllt - StartDpllt,
    ( solved_constraint(ResDpllt)
    -> inc_solved_counter(sym_smt),
    add_benchmark_result(sym_smt, ConstraintPath, ResDpllt)
    ; true
    ),
    nl,nl,write(ResDpllt),nl,nl,
    write('done.'), nl,
    preferences:set_preference(time_out, Timeout),
    ( UseIdlSolver
    -> set_preference(dpllt_perform_symmetry_breaking, false),
    set_preference(dpllt_use_idl_theory_solver, true),
    dpllt_solver:init,
    write('Solve with IDL-SMT..'),nl,
    statistics(walltime, [StartDplltIdl|_]),
    dpllt_solve_predicate(idl_smt, Constraint, _SolvedPred3, ResDplltIdl),
    statistics(walltime, [StopDplltIdl|_]),
    (dpllt_sat_solver:restarts(RestartsDplltIdl); RestartsDplltIdl = 0),
    format("Restarts: ~w~n", [RestartsDplltIdl]),
    TimeDplltIdl is StopDplltIdl - StartDplltIdl,
    ( solved_constraint(ResDplltIdl)
    -> inc_solved_counter(idl_smt),
    add_benchmark_result(idl_smt, ConstraintPath, ResDplltIdl)
    ; true
    ),
    set_preference(dpllt_use_idl_theory_solver, false),
    set_preference(dpllt_perform_symmetry_breaking, true)
    ; TimeDplltIdl = 0,
    RestartsDplltIdl = 0,
    ResDplltIdl = none
    ),
    nl,nl,write(ResDplltIdl),nl,nl,
    write('done.'), nl,
   
    preferences:set_preference(time_out, Timeout),
    set_preference(dpllt_perform_symmetry_breaking, false),
    dpllt_solver:init,
    write('Solve with SMT..'),nl,
    write(ConstraintPath),nl,
    statistics(walltime, [StartDplltNoSym|_]),
    dpllt_solve_predicate(smt, Constraint, _, ResDplltNoSym),
    %ResDplltNoSym = no_solution_found(solver_answered_unknown),
    statistics(walltime, [StopDplltNoSym|_]),
    (dpllt_sat_solver:restarts(RestartsDplltNoSym); RestartsDplltNoSym = 0),
    format("Restarts: ~w~n", [RestartsDplltNoSym]),
    TimeDplltNoSym is StopDplltNoSym - StartDplltNoSym,
    ( solved_constraint(ResDplltNoSym)
    -> inc_solved_counter(smt),
    add_benchmark_result(smt, ConstraintPath, ResDplltNoSym)
    ; true
    ),
    nl,nl,write(ResDplltNoSym),nl,nl,
    write('done.'), nl,
    preferences:set_preference(time_out, Timeout),
   
    set_preference(dpllt_perform_static_analysis, false),
    set_preference(dpllt_perform_symmetry_breaking, false),
    dpllt_solver:init,
    write('Solve with Raw-SMT..'),nl,
    write(ConstraintPath),nl,
    statistics(walltime, [StartDplltRaw|_]),
    dpllt_solve_predicate(raw_smt, Constraint, _, ResDplltRaw),
    %ResDplltRaw = no_solution_found(solver_answered_unknown),
    statistics(walltime, [StopDplltRaw|_]),
    (dpllt_sat_solver:restarts(RestartsDplltRaw); RestartsDplltRaw = 0),
    format("Restarts: ~w~n", [RestartsDplltRaw]),
    TimeDplltRaw is StopDplltRaw - StartDplltRaw,
    ( solved_constraint(ResDplltRaw)
    -> inc_solved_counter(raw_smt),
    add_benchmark_result(raw_smt, ConstraintPath, ResDplltRaw)
    ; true
    ),
    nl,nl,write(ResDplltRaw),nl,nl,
    write('done.'), nl,
    preferences:set_preference(time_out, Timeout),
    set_preference(dpllt_perform_static_analysis,true),
    set_preference(dpllt_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, TimeDpllt, TimeDplltRaw, TimeDplltIdl, TimeDplltNoSym, TimeDplltRawSym, TimeProB, RestartsDpllt, RestartsDplltRaw, RestartsDplltIdl, RestartsDplltNoSym, RestartsDplltRawSym), !,
    benchmark_constraints(UseIdlSolver, Timeout, T, [(ConstraintPath,TimeZ3,TimeDpllt,TimeDplltRaw,TimeDplltIdl,TimeDplltNoSym,TimeDplltRawSym,TimeProB,RestartsDpllt,RestartsDplltRaw,RestartsDplltIdl,RestartsDplltNoSym,RestartsDplltRawSym)|Acc], Data).

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(TimeDpllt, member((_,_,TimeDpllt,_,_,_,_,_,_,_,_,_), Data), TimesDpllt),
    findall(TimeDplltRaw, member((_,_,_,TimeDplltRaw,_,_,_,_,_,_,_,_,_), Data), TimesDplltRaw),
    findall(TimeDplltIdl, member((_,_,_,_,TimeDplltIdl,_,_,_,_,_,_,_,_), Data), TimesDplltIdl),
    findall(TimeDplltNoSym, member((_,_,_,_,_,TimeDplltNoSym,_,_,_,_,_,_,_), Data), TimesDplltNoSym),
    findall(TimeDplltRawSym, member((_,_,_,_,_,_,TimeDplltRawSym,_,_,_,_,_,_), Data), TimesDplltRawSym),
    findall(TimeProB, member((_,_,_,_,_,_,_,TimeProB,_,_,_,_,_), Data), TimesProB),
    findall(RestartDpllt, member((_,_,_,_,_,_,_,_,RestartDpllt,_,_,_,_), Data), RestartsDpllt),
    findall(RestartDplltRaw, member((_,_,_,_,_,_,_,_,_,RestartDplltRaw,_,_), Data), RestartsDplltRaw),
    findall(RestartDplltIdl, member((_,_,_,_,_,_,_,_,_,_,RestartDplltIdl,_,_), Data), RestartsDplltIdl),
    findall(RestartDplltNoSym, member((_,_,_,_,_,_,_,_,_,_,_,RestartDplltNoSym,_), Data), RestartsDplltNoSym),
    findall(RestartDplltRawSym, member((_,_,_,_,_,_,_,_,_,_,_,_,RestartDplltRawSym), Data), RestartsDplltRawSym),
    sumlist(TimesZ3, TimeZ3),
    sumlist(TimesDpllt, TimeDpllt),
    sumlist(TimesDplltRaw, TimeDplltRaw),
    sumlist(TimesDplltIdl, TimeDplltIdl),
    sumlist(TimesDplltNoSym, TimeDplltNoSym),
    sumlist(TimesDplltRawSym, TimeDplltRawSym),
    sumlist(TimesProB, TimeProB),
    sumlist(RestartsDpllt, RestartDpllt),
    sumlist(RestartsDplltRaw, RestartDplltRaw),
    sumlist(RestartsDplltIdl, RestartDplltIdl),
    sumlist(RestartsDplltNoSym, RestartDplltNoSym),
    sumlist(RestartsDplltRawSym, RestartDplltRawSym),
    atom_concat('benchmarks_dpllt_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", [TimeDplltRawSym,RestartsDplltRawSym,TimeZ3,TimeDpllt,RestartDpllt,TimeDplltIdl,RestartDplltIdl,TimeDplltNoSym,RestartDplltNoSym,TimeDplltRaw,RestartDplltRaw,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,TimeDplltNoSym,SolvedRawSMT,TimeDplltRaw,SolvedSymSMT,TimeDpllt,SolvedSymRawSMT,TimeDplltRawSym]),
    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,TimeDpllt), member((ConstraintPath,_,TimeDpllt,_,_,_,_,_,_,_,_,_), Data), DataDpllt),
    findall((ConstraintPath,TimeDplltRaw), member((ConstraintPath,_,_,TimeDplltRaw,_,_,_,_,_,_,_,_,_), Data), DataDplltRaw),
    %findall((ConstraintPath,TimeDplltIdl), member((ConstraintPath,_,_,_,TimeDplltIdl,_,_,_,_,_,_,_,_), Data), DataDplltIdl),
    findall((ConstraintPath,TimeDplltNoSym), member((ConstraintPath,_,_,_,_,TimeDplltNoSym,_,_,_,_,_,_,_), Data), DataDplltNoSym),
    findall((ConstraintPath,TimeDplltRawSym), member((ConstraintPath,_,_,_,_,_,TimeDplltRawSym,_,_,_,_,_,_), Data), DataDplltRawSym),
    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, DataDplltNoSym),
    write_to_csv(sym_smt, MachineName, DataDpllt),
    write_to_csv(raw_smt, MachineName, DataDplltRaw),
    write_to_csv(sym_raw_smt, MachineName, DataDplltRawSym).

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) :-
    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("DPLLT-Res: ~w~nDPLLT-Time: ~w~nDPLLT-Restarts: ~w~n", [ResDpllt,TimeDpllt,RestartsDpllt]),
    format("DPLLT-No-Sym-Res: ~w~nDPLLT-No-Sym-Time: ~w~nDPLLT-No-Sym-Restarts: ~w~n", [ResDplltNoSym,TimeDplltNoSym,RestartsDplltNoSym]),
    format("DPLLT-Idl-Res: ~w~nDPLLT-Idl-Time: ~w~nDPLLT-Idl-Restarts: ~w~n", [ResDplltIdl,TimeDplltIdl,RestartsDplltIdl]),
    format("DPLLT-Raw-Res: ~w~nDPLLT-Raw-Time: ~w~nDPLLT-Raw-Restarts: ~w~n", [ResDplltRaw,TimeDplltRaw,RestartsDplltRaw]),
    format("DPLLT-Sym-Raw-Res: ~w~nDPLLT-Sym-Raw-Time: ~w~nDPLLT-Sym-Raw-Restarts: ~w~n", [ResDplltRawSym,TimeDplltRawSym,RestartsDplltRawSym]),
    format("Z3-Res: ~w~nZ3-Time: ~w~n", [ResZ3,TimeZ3]),
    format("ProB-Res: ~w~nProB-Time: ~w~n", [ResProB,TimeProB]),
    close(Stream),
    !.

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.

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,TimeDpllt,_FResDpllt)],
    format("~w & ~w & ~w & ~w & ~n", [N,TimeProB,TimeZ3,TimeDpllt]).

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

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(dpllt_sat_solver:incremental_mode),
    benchmark_constraints(UseIdlSolver, Timeout, FullConstraintPaths, [], Data),
    retractall(dpllt_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(dpllt_use_idl_theory_solver, false),
    set_preference(dpllt_perform_static_analysis, false),
    set_preference(dpllt_perform_symmetry_breaking, true),
    dpllt_solver:init,
    write('Solve with Sym-Raw-SMT..'),nl,
    writeq(BenchmarkFilePath),nl,
    statistics(walltime, [StartDplltRawSym|_]),
    dpllt_solve_predicate(Constraint, _, ResDplltRawSym),
    statistics(walltime, [StopDplltRawSym|_]),
    (dpllt_sat_solver:restarts(RestartsDplltRawSym); RestartsDplltRawSym = 0),
    TimeDplltRawSym is StopDplltRawSym - StartDplltRawSym,
    nl,nl,write(ResDplltRawSym),nl,nl,
   
    write('done.'), nl,
    set_preference(dpllt_perform_static_analysis, true),
    dpllt_solver:init,
    write('Solve with Sym-SMT..'),nl,
    writeq(BenchmarkFilePath),nl,
    statistics(walltime, [StartDpllt|_]),
    dpllt_solve_predicate(Constraint, _, ResDpllt),
    statistics(walltime, [StopDpllt|_]),
    (dpllt_sat_solver:restarts(RestartsDpllt); RestartsDpllt = 0),
    TimeDpllt is StopDpllt - StartDpllt,
    nl,nl,write(ResDpllt),nl,nl,
   
    write('done.'), nl,
    preferences:set_preference(time_out, Timeout),
    ( UseIdlSolver
    -> set_preference(dpllt_perform_symmetry_breaking,false),
    set_preference(dpllt_use_idl_theory_solver,true),
    dpllt_solver:init,
    write('Solve with IDL-SMT..'),nl,
    writeq(BenchmarkFilePath),nl,
    statistics(walltime, [StartDplltIdl|_]),
    dpllt_solve_predicate(Constraint, _, ResDplltIdl),
    statistics(walltime, [StopDplltIdl|_]),
    (dpllt_sat_solver:restarts(RestartsDplltIdl); RestartsDplltIdl = 0),
    TimeDplltIdl is StopDplltIdl - StartDplltIdl,
    set_preference(dpllt_use_idl_theory_solver,false),
    set_preference(dpllt_perform_symmetry_breaking,true)
    ; TimeDplltIdl = 0,
    RestartsDplltIdl = 0,
    ResDplltIdl = none
    ),
    nl,nl,write(ResDplltIdl),nl,nl,
    write('done.'), nl,
   
    preferences:set_preference(time_out, Timeout),
    set_preference(dpllt_perform_symmetry_breaking,false),
    dpllt_solver:init,
    write('Solve with SMT..'),nl,
    writeq(BenchmarkFilePath),nl,
    statistics(walltime, [StartDplltNoSym|_]),
    dpllt_solve_predicate(Constraint, _, ResDplltNoSym),
    statistics(walltime, [StopDplltNoSym|_]),
    (dpllt_sat_solver:restarts(RestartsDplltNoSym); RestartsDplltNoSym = 0),
    TimeDplltNoSym is StopDplltNoSym - StartDplltNoSym,
    nl,nl,write(ResDplltNoSym),nl,nl,
    write('done.'), nl,
    preferences:set_preference(time_out, Timeout),
   
    set_preference(dpllt_perform_static_analysis,false),
    set_preference(dpllt_perform_symmetry_breaking,false),
    dpllt_solver:init,
    write('Solve with Raw-SMT..'),nl,
    writeq(BenchmarkFilePath),nl,
    statistics(walltime, [StartDplltRaw|_]),
    dpllt_solve_predicate(Constraint, _, ResDplltRaw),
    statistics(walltime, [StopDplltRaw|_]),
    (dpllt_sat_solver:restarts(RestartsDplltRaw); RestartsDplltRaw = 0),
    TimeDplltRaw is StopDplltRaw - StartDplltRaw,
    nl,nl,write(ResDplltRaw),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, ResDplltRawSym, TimeDplltRawSym, RestartsDplltRawSym, ResDpllt, TimeDpllt, RestartsDpllt, ResDplltNoSym, TimeDplltNoSym, RestartsDplltNoSym, ResDplltIdl, TimeDplltIdl, RestartsDplltIdl, ResDplltRaw, TimeDplltRaw, RestartsDplltRaw, ResZ3, TimeZ3, ResProB, TimeProB).

run_cbc_benchmarks(UseIdlSolver, FolderPath) :-
    directory_exists(FolderPath),
    file_members_of_directory(FolderPath, FilePaths),
    select_machine_file_path(FilePaths, MachineFilePath, TBenchmarkFilePaths),
    findall(FileName-FilePath, (member(FileName-FilePath, TBenchmarkFilePaths), atom_concat(_, '.eval', FilePath)), BenchmarkFilePaths),
    load_b_eventb_or_tla(MachineFilePath),
    run_cbc_benchmarks(UseIdlSolver, FolderPath, BenchmarkFilePaths).

run_cbc_benchmarks(_, _, []).

run_cbc_benchmarks(UseIdlSolver, FolderPath, [FileName-BenchmarkFilePath|T]) :-
    open(BenchmarkFilePath, read, Stream),
    read(Stream, Constraint),
    close(Stream),
    retractall(dpllt_sat_solver:incremental_mode),
    run_cbc_benchmark(UseIdlSolver, FolderPath, FileName-BenchmarkFilePath, Constraint),
    run_cbc_benchmarks(UseIdlSolver, FolderPath, T).

run_cbc_benchmarks1 :-
    inductive_inv_timeout(Timeout),
    preferences:set_preference(time_out, Timeout),
    /*run_cbc_benchmarks(false, 'benchmarks_inductive_inv/abz16_m0/'),
    run_cbc_benchmarks(false, 'benchmarks_inductive_inv/abz16_m1/'),
    run_cbc_benchmarks(false, 'benchmarks_inductive_inv/abz16_m2/'),
    run_cbc_benchmarks(false, 'benchmarks_inductive_inv/abz16_m3/'),*/
    run_cbc_benchmarks(false, 'benchmarks_inductive_inv/abz16_m4/'),
    run_cbc_benchmarks(false, 'benchmarks_inductive_inv/abz16_m5/'),
    run_cbc_benchmarks(false, 'benchmarks_inductive_inv/abz16_m6/'),
    run_cbc_benchmarks(false, 'benchmarks_inductive_inv/abz16_m7/').

run_cbc_benchmarks2 :-
    inductive_inv_timeout(Timeout),
    preferences:set_preference(time_out, Timeout),
    run_cbc_benchmarks(false, 'benchmarks_inductive_inv/r0_geardoor/'),
    run_cbc_benchmarks(false, 'benchmarks_inductive_inv/r1_valve/'),
    run_cbc_benchmarks(false, 'benchmarks_inductive_inv/r2_outputs/'),
    run_cbc_benchmarks(false, 'benchmarks_inductive_inv/r3_sensors/'),
    run_cbc_benchmarks(false, 'benchmarks_inductive_inv/r4_handle/'),
    run_cbc_benchmarks(false, 'benchmarks_inductive_inv/r5_switch/'),
    run_cbc_benchmarks(false, 'benchmarks_inductive_inv/r6_lights/').

run_cbc_benchmarks3 :-
    inductive_inv_timeout(Timeout),
    preferences:set_preference(time_out, Timeout),
    run_cbc_benchmarks(false, 'benchmarks_inductive_inv/pm_m0_aai/'),
    run_cbc_benchmarks(false, 'benchmarks_inductive_inv/pm_m0_aat/'),
    run_cbc_benchmarks(false, 'benchmarks_inductive_inv/pm_m0_aoo/'),
    run_cbc_benchmarks(false, 'benchmarks_inductive_inv/pm_m0_voo/').

run_cbc_benchmarks4 :-
    inductive_inv_timeout(Timeout),
    preferences:set_preference(time_out, Timeout),
    run_cbc_benchmarks(false, 'benchmarks_inductive_inv/pm_m0_vvi/'),
    run_cbc_benchmarks(false, 'benchmarks_inductive_inv/pm_m0_vvt/'),
    run_cbc_benchmarks(false, 'benchmarks_inductive_inv/pm_m1_aoor/'),
    run_cbc_benchmarks(false, 'benchmarks_inductive_inv/pm_m1_voor/'),
    run_cbc_benchmarks(false, 'benchmarks_inductive_inv/pm_m2_aai/').

run_cbc_benchmarks5 :-
    inductive_inv_timeout(Timeout),
    preferences:set_preference(time_out, Timeout),
    %run_cbc_benchmarks(false, 'benchmarks_inductive_inv/simple-two-phase/'), % static contradiction
    run_cbc_benchmarks(false, 'benchmarks_inductive_inv/prisoners-4/'),
    run_cbc_benchmarks(false, 'benchmarks_inductive_inv/bakery/'),
    run_cbc_benchmarks(false, 'benchmarks_inductive_inv/paxos-3/').

run_cbc_benchmarks6 :-
    inductive_inv_timeout(Timeout),
    preferences:set_preference(time_out, Timeout),
    run_cbc_benchmarks(false, 'benchmarks_inductive_inv/lightbot/'),
    run_cbc_benchmarks(false, 'benchmarks_inductive_inv/travel_agency/'),
    run_cbc_benchmarks(false, 'benchmarks_inductive_inv/search_events/'),
    run_cbc_benchmarks(false, 'benchmarks_inductive_inv/large_branching/').

run_deadlock_benchmarks1 :-
    deadlock_timeout(Timeout),
    preferences:set_preference(time_out, Timeout),
    /*run_cbc_benchmarks(false, 'benchmarks_cbc_deadlock/abz16_m0/'),
    run_cbc_benchmarks(false, 'benchmarks_cbc_deadlock/abz16_m1/'),
    run_cbc_benchmarks(false, 'benchmarks_cbc_deadlock/abz16_m2/'),
    run_cbc_benchmarks(false, 'benchmarks_cbc_deadlock/abz16_m3/'),*/
    run_cbc_benchmarks(false, 'benchmarks_cbc_deadlock/abz16_m4/'),
    run_cbc_benchmarks(false, 'benchmarks_cbc_deadlock/abz16_m5/'),
    run_cbc_benchmarks(false, 'benchmarks_cbc_deadlock/abz16_m6/'),
    run_cbc_benchmarks(false, 'benchmarks_cbc_deadlock/abz16_m7/').

run_deadlock_benchmarks2 :-
    deadlock_timeout(Timeout),
    preferences:set_preference(time_out, Timeout),
    run_cbc_benchmarks(false, 'benchmarks_cbc_deadlock/r0_geardoor/'),
    run_cbc_benchmarks(false, 'benchmarks_cbc_deadlock/r1_valve/'),
    run_cbc_benchmarks(false, 'benchmarks_cbc_deadlock/r2_outputs/'),
    run_cbc_benchmarks(false, 'benchmarks_cbc_deadlock/r3_sensors/'),
    run_cbc_benchmarks(false, 'benchmarks_cbc_deadlock/r4_handle/'),
    run_cbc_benchmarks(false, 'benchmarks_cbc_deadlock/r5_switch/').

run_deadlock_benchmarks3 :-
    deadlock_timeout(Timeout),
    preferences:set_preference(time_out, Timeout),
    run_cbc_benchmarks(false, 'benchmarks_cbc_deadlock/pm_m0_aai/'),
    run_cbc_benchmarks(false, 'benchmarks_cbc_deadlock/pm_m0_aat/'),
    run_cbc_benchmarks(false, 'benchmarks_cbc_deadlock/pm_m0_aoo/'),
    run_cbc_benchmarks(false, 'benchmarks_cbc_deadlock/pm_m0_voo/').

run_deadlock_benchmarks4 :-
    deadlock_timeout(Timeout),
    preferences:set_preference(time_out, Timeout),
    run_cbc_benchmarks(false, 'benchmarks_cbc_deadlock/pm_m0_vvi/'),
    run_cbc_benchmarks(false, 'benchmarks_cbc_deadlock/pm_m0_vvt/'),
    run_cbc_benchmarks(false, 'benchmarks_cbc_deadlock/pm_m1_aoor/'),
    run_cbc_benchmarks(false, 'benchmarks_cbc_deadlock/pm_m1_voor/'),
    run_cbc_benchmarks(false, 'benchmarks_cbc_deadlock/pm_m2_aai/').

run_deadlock_benchmarks5 :-
    deadlock_timeout(Timeout),
    preferences:set_preference(time_out, Timeout),
    run_cbc_benchmarks(false, 'benchmarks_cbc_deadlock/simple-two-phase/'),
    run_cbc_benchmarks(false, 'benchmarks_cbc_deadlock/prisoners-4/'),
    run_cbc_benchmarks(false, 'benchmarks_cbc_deadlock/bakery/'),
    run_cbc_benchmarks(false, 'benchmarks_cbc_deadlock/paxos-3/').

run_deadlock_benchmarks6 :-
    deadlock_timeout(Timeout),
    preferences:set_preference(time_out, Timeout),
    run_cbc_benchmarks(false, 'benchmarks_cbc_deadlock/lightbot/'),
    run_cbc_benchmarks(false, 'benchmarks_cbc_deadlock/travel_agency/'),
    run_cbc_benchmarks(false, 'benchmarks_cbc_deadlock/search_events/'),
    run_cbc_benchmarks(false, 'benchmarks_cbc_deadlock/large_branching/').

run_n_queens_benchmark(N, DataAcc, NewDataAcc) :-
    n_queens_encoding(N, Constraint),
    ast_optimizer_for_smt:precompute_values(Constraint, [instantiate_quantifier_limit(10000)], IConstraint),
    dpllt_solver:get_amount_of_sat_variables(IConstraint, AmountOfSatVars),
    format("Amount of SAT variables: ~w", [AmountOfSatVars]),nl,
    format("Solve with ProB for N=~w~n", [N]),
    statistics(walltime, [StartProB|_]),
    solve_predicate(IConstraint, _, ResProB),
    statistics(walltime, [StopProB|_]),
    ResProB \= contradiction_found,
    TimeProB is StopProB - StartProB,
    format("Solve with Z3~n for N=~w", [N]),
    statistics(walltime, [StartZ3|_]),
    smt_solve_predicate(z3, Constraint, _, ResZ3),
    statistics(walltime, [StopZ3|_]),
    ResZ3 \= contradiction_found,
    TimeZ3 is StopZ3 - StartZ3,
    format("Solve with Sym-SMT~n for N=~w", [N]),
    set_preference(dpllt_perform_static_analysis, true),
    set_preference(dpllt_perform_symmetry_breaking, true),
    dpllt_solver:init,
    statistics(walltime, [StartDpllt|_]),
    dpllt_solve_predicate(sym_smt, Constraint, _SolvedPred, ResDpllt),
    statistics(walltime, [StopDpllt|_]),
    ResDpllt \= contradiction_found,
    TimeDpllt is StopDpllt - StartDpllt,
    functor(ResProB, FResProB, _),
    functor(ResZ3, FResZ3, _),
    functor(ResDpllt, FResDpllt, _),
    append(DataAcc, [[AmountOfSatVars,(prob,N,TimeProB,FResProB),(z3,N,TimeZ3,FResZ3),(sym_smt,N,TimeDpllt,FResDpllt)]], NewDataAcc).