1		:- module(solver_dispatcher, [init_interface/1,reset_interface/1,smt_solver_interface_call/2,
2		pretty_print_smt/1, pretty_print_smt/2]).
3
4		:- use_module(probsrc(module_information),[module_info/2]).
5		:- module_info(group,smt_solvers).
6		:- module_info(description,'This module provides an interface to SMT-solvers like CVC4 or Z3.').
7
8		:- use_module(extension('cvc4interface/cvc4interface')).
9		:- use_module(extension('z3interface/z3interface')).
10
11		:- use_module(probsrc(debug), [debug_format_flush/3]).
12
13		init_interface(cvc4) :-
14		init_cvc4interface.
15		init_interface(z3) :-
16		init_z3interface.
17		reset_interface(cvc4) :-
18		reset_cvc4interface.
19		reset_interface(z3) :-
20		reset_z3interface.
21
22		:- meta_predicate smt_solver_interface_call(+,+).
23		smt_solver_interface_call(z3,Call) :-
24		%debug_format(9,'z3: calling ~w~n',[Call]),
25		z3_interface_call(Call),
26		debug_format_flush(9,'z3: called ~w~n',[Call]).
27		smt_solver_interface_call(cvc4,Call) :-
28		debug_format_flush(9,'cvc4: calling ~w~n',[Call]),
29		cvc4_interface_call(Call).
30
31		pretty_print_smt(z3) :- !,pretty_print_smt2.
32		pretty_print_smt(Solver) :- format('Pretty print not available for ~w~n',[Solver]).
33
34		pretty_print_smt(z3,ExprID) :- !,pretty_print_smt2_for_id(ExprID).
35		pretty_print_smt(Solver,_) :- format('Pretty print not available for ~w~n',[Solver]).