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]). |