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