solver_dispatcher

init_interface(cvc4) :-
    init_cvc4interface.

init_interface(z3) :-
    init_z3interface,!.

init_interface(z3) :-
    (z3interface_init_error(E)
    -> add_error(z3,'Loading Z3 extension failed:',E)
    ; add_error(z3,'Z3 initialisation failed:','') % should not happen
    ),
    add_message(z3,'Be sure that libz3.dylib/so/dll is on your dynamic library path',''),
    % Z3_HOME is not used (anymore), Z3_HOME_FOR_PROB is used when compiling
    % (environ('Z3_HOME',Path) -> add_message(z3,'Currently Z3_HOME is set to: ',Path)
    % ; add_message(z3,'Currently Z3_HOME is not set.','') ),
    fail.

pretty_print_smt(z3) :- !,pretty_print_smt.

pretty_print_smt(Solver) :- format('Pretty print not available for ~w~n',[Solver]).

pretty_print_smt(TranslationType, z3, ExprID) :- !, pretty_print_smt_for_id(TranslationType, ExprID).

pretty_print_smt(_, Solver, _) :- format('Pretty print not available for ~w~n', [Solver]).

reset_interface(cvc4) :-
    reset_cvc4interface.

reset_interface(z3) :-
    reset_z3interface.

smt_solver_header_version(z3,Version) :- !,
    init_interface(z3),
    z3_interface_call(get_header_version(Version)).

smt_solver_header_version(_,'?').

smt_solver_interface_call(z3,Call) :-
    %debug_format_flush(9,'z3: calling ~w~n',[Call]),
    z3_interface_call(Call),
    debug_format_flush(9,'z3: called ~w~n',[Call]).

smt_solver_interface_call(cvc4,Call) :-
    %debug_format_flush(9,'cvc4: calling ~w~n',[Call]),
    cvc4_interface_call(Call),
    debug_format_flush(9,'cvc4: called ~w~n',[Call]).

smt_solver_version(z3,Version) :- !,
    init_interface(z3),
    z3_interface_call(get_full_version(Version)).

smt_solver_version(_,'?').