1		:- module(solver_dispatcher, [init_interface/1,reset_interface/1,smt_solver_interface_call/2,
2		pretty_print_smt/1, pretty_print_smt/3,
3		smt_solver_version/2, smt_solver_header_version/2]).
4
5		:- use_module(extension('cvc4interface/cvc4interface')).
6		:- use_module(extension('z3interface/z3interface')).
7
8		%:- use_module(library(system), [environ/2]).
9		:- use_module(probsrc(debug), [debug_format_flush/3]).
10		:- use_module(probsrc(error_manager), [add_error/3, add_message/3]).
11
12		:- use_module(probsrc(module_information),[module_info/2]).
13		:- module_info(group,smt_solvers).
14		:- module_info(description,'This module provides an interface to SMT-solvers like CVC4 or Z3.').
15
16		init_interface(cvc4) :-
17		init_cvc4interface.
18		init_interface(z3) :-
19		init_z3interface,!.
20		init_interface(z3) :-
21		(z3interface_init_error(E)
22		-> add_error(z3,'Loading Z3 extension failed:',E)
23		; add_error(z3,'Z3 initialisation failed:','') % should not happen
24		),
25		add_message(z3,'Be sure that libz3.dylib/so/dll is on your dynamic library path',''),
26		% Z3_HOME is not used (anymore), Z3_HOME_FOR_PROB is used when compiling
27		% (environ('Z3_HOME',Path) -> add_message(z3,'Currently Z3_HOME is set to: ',Path)
28		% ; add_message(z3,'Currently Z3_HOME is not set.','') ),
29		fail.
30		reset_interface(cvc4) :-
31		reset_cvc4interface.
32		reset_interface(z3) :-
33		reset_z3interface.
34
35
36		:- meta_predicate smt_solver_interface_call(+,+).
37		smt_solver_interface_call(z3,Call) :-
38		%debug_format_flush(9,'z3: calling ~w~n',[Call]),
39		z3_interface_call(Call),
40		debug_format_flush(9,'z3: called ~w~n',[Call]).
41		smt_solver_interface_call(cvc4,Call) :-
42		%debug_format_flush(9,'cvc4: calling ~w~n',[Call]),
43		cvc4_interface_call(Call),
44		debug_format_flush(9,'cvc4: called ~w~n',[Call]).
45
46		pretty_print_smt(z3) :- !,pretty_print_smt.
47		pretty_print_smt(Solver) :- format('Pretty print not available for ~w~n',[Solver]).
48
49		pretty_print_smt(TranslationType, z3, ExprID) :- !, pretty_print_smt_for_id(TranslationType, ExprID).
50		pretty_print_smt(_, Solver, _) :- format('Pretty print not available for ~w~n', [Solver]).
51
52
53		smt_solver_version(z3,Version) :- !,
54		init_interface(z3),
55		z3_interface_call(get_full_version(Version)).
56		smt_solver_version(_,'?').
57
58		% version of the header files with which the ProB extension was linked with
59		% if this is too old or too new compared to the used solver we may have problems !
60		smt_solver_header_version(z3,Version) :- !,
61		init_interface(z3),
62		z3_interface_call(get_header_version(Version)).
63		smt_solver_header_version(_,'?').