solvercalls

average_times(Times, SampSize, Averaged) :-
    sum_times(Times, Summed),
    norm_times(Summed, SampSize, Averaged).

contradiction(Res1, Res2) :-
    Res1 =.. [U1|_],
    Res2 =.. [U2|_],
    member(U1, [solution, contradiction_found]),
    member(U2, [solution, contradiction_found]),
    U1 \== U2.

find_contradictions([], []).

find_contradictions(Results, Contradictions) :-
    find_contradictions_([], _, Results, Contradictions).

find_contradictions_([], _, [], []).

find_contradictions_([], _, [N|Rs], Cs) :-
    find_contradictions_(Rs, N, Rs, Cs).

find_contradictions_([S2-O2-V2|Ss], S-O-V, Rs, [(S-O-V, S2-O2-V2) | Cs]) :-
    contradiction(V2, V), !,
    find_contradictions_(Ss, S-O-V, Rs, Cs).

find_contradictions_([_|Ss], S-O-V, Rs, Cs) :-
    find_contradictions_(Ss, S-O-V, Rs, Cs).

norm_times([], _, []) :- !.

norm_times([S-O-T | Ts], N, [S-O-Norm | Norms]) :- !,
    Norm is T/N,
    norm_times(Ts, N, Norms).

par2([], [], []).

par2([Solver-Opts-T|Ts], [Solver-Opts-R|Rs], [Solver-Opts-P2|P2s]) :-
    (R=..[ResType|_], memberchk(ResType, [solution, contradiction_found])
    -> P2 is T
    ; P2 is T + 2500), % TODO: Don't have this hardcoded.
    par2(Ts, Rs, P2s).

performance_margin(TargetTimings, ReferenceTimings, TargetMinTime, ReferenceMaxTime) :-
    findall(TargetTime, member(_-_-TargetTime, TargetTimings), RawTargetTimings),
    findall(ReferenceTime, member(_-_-ReferenceTime, ReferenceTimings), RawReferenceTimings),
    min(RawTargetTimings, TargetMinTime),
    max(RawReferenceTimings, ReferenceMaxTime).

run_iteration(Ast, TargetSolvers, ReferenceSolvers, TargetMinTime, ReferenceMaxTime, AllTimings, AllResults) :-
    run_iteration_(Ast, TargetSolvers, ReferenceSolvers, TargetTimings, TargetResults, ReferenceTimings, ReferenceResults),
    performance_margin(TargetTimings, ReferenceTimings, TargetMinTime, ReferenceMaxTime),
    append(TargetTimings, ReferenceTimings, AllTimings),
    append(TargetResults, ReferenceResults, AllResults).

run_iteration(N, Ast, TargetSolvers, ReferenceSolvers, TargetMinTime, ReferenceMaxTime, AvgTimes, AllResults) :-
    run_n_iterations(N, Ast, TargetSolvers, ReferenceSolvers, TarTimes, [TarResults | _], RefTimes, [RefResults | _]),
    average_times(TarTimes, N, AvgTarTimes),
    average_times(RefTimes, N, AvgRefTimes),
    par2(AvgTarTimes, TarResults, TarPar2),
    par2(AvgRefTimes, RefResults, RefPar2),
    append(TarPar2, RefPar2, AvgTimes),
    append(TarResults, RefResults, AllResults),
    performance_margin(TarPar2, RefPar2, TargetMinTime, ReferenceMaxTime).

run_iteration_(Ast, TargetSolvers, ReferenceSolvers, TargetTimes, TargetResults, ReferenceTimes, ReferenceResults) :-
    solve_timed_with_multiple_solvers(TargetSolvers, Ast, TargetTimes, TargetResults),
    solve_timed_with_multiple_solvers(ReferenceSolvers, Ast, ReferenceTimes, ReferenceResults).

run_n_iterations(0, _, _, _, [], [], [], []) :- !.

run_n_iterations(N, Ast, TargetSolvers, ReferenceSolvers, [TarT|TarTimes], [TarR|TarRes], [RefT|RefTimes], [RefR|RefRes]) :-
    N > 0,
    run_iteration_(Ast, TargetSolvers, ReferenceSolvers, TarT, TarR, RefT, RefR),
    NN is N-1,
    run_n_iterations(NN, Ast, TargetSolvers, ReferenceSolvers, TarTimes, TarRes, RefTimes, RefRes).

smt_solver(z3).

smt_solver(z3cns).

smt_solver(z3axm).

smt_solver(cvc4).

solve_timed(prob, Options, Ast, Result, Time) :-
    timed_solve_predicate(Ast, Options, Result, Time). % clean_up_pred is one useful option

solve_timed(probcomp, Options, Ast, Result, Time) :-
    find_identifier_uses(Ast, [], UsedIds),
    temporary_set_preference(data_validation_mode, true),
    b_compile(Ast, UsedIds, [], [], AstCompiled, no_wf_available),
    reset_temporary_preference(data_validation_mode),
    timed_solve_predicate(AstCompiled, Options, Result, Time).

solve_timed(kodkod, Options, Ast, Result, Time) :-
    timed_solve_predicate(Ast, ['KODKOD' | Options], Result, Time).

solve_timed(smt_supported_interpreter, Options, Ast, Result, Time) :-
    timed_solve_predicate(Ast, ['SMT_SUPPORTED_INTERPRETER' | Options], Result, Time).

solve_timed(cdclt, _, Ast, Result, Time) :-
    statistics(walltime, [Start, _]),
    cdclt_solve_predicate(Ast, _, Result),
    statistics(walltime, [Stop,_]),
    Time is Stop - Start.

solve_timed(SmtSolver, _, Ast, Result, Time) :-
    smt_solver(SmtSolver),
    statistics(walltime, [Start, _]),
    smt_solve_predicate(SmtSolver, Ast, _, Result),
    statistics(walltime, [Stop,_]),
    Time is Stop - Start.

solve_timed_with_multiple_solvers([], _, [], []).

solve_timed_with_multiple_solvers([SolverName-Options | Solvers], Ast,
    [SolverName-Options-Time | Timings],
    [SolverName-Options-Res | Results]) :-
    solve_timed(SolverName, Options, Ast, Res, Time),
    solve_timed_with_multiple_solvers(Solvers, Ast, Timings, Results).

sum_time_samples([], [], []) :- !.

sum_time_samples([S-O-T1 | T1s], [S-O-T2 | T2s], [S-O-Sum | Sums]) :-
    Sum is T1 + T2,
    sum_time_samples(T1s, T2s, Sums).

sum_times([T|Ts], Summed) :- !,
    sum_times(Ts, T, Summed).

sum_times([], T, T).

sum_times([T | Ts], Sum, Result) :-
    sum_time_samples(T, Sum, NewSum),
    sum_times(Ts, NewSum, Result).

timed_solve_predicate(Predicate, Options, Result, Time) :-
    statistics(walltime, [Start, _]),
    solve_predicate(Predicate, _, 1, Options, Result),
    statistics(walltime, [Stop,_]),
    Time is Stop - Start.