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 :- module(z3interface, [init_z3interface/0,
6 reset_z3interface/0, % TODO: make more lightweight once cvc 1.5 is out
7 z3interface_init_error/1,
8 pretty_print_smt/0, % pretty print Z3's internal status and constraints
9 pretty_print_smt_for_id/2, % pretty print store + constraint pointed to by ID (previously created by z3_interface_call(s))
10 z3_interface_call/1]).
11
12 :- use_module(probsrc(module_information)).
13 :- module_info(group, smt_solvers).
14 :- module_info(description, 'This is the interface between ProB and the Z3 SMT solver').
15
16
17 foreign_resource(z3interface, [init,
18 pretty_print_smt, pretty_print_smt_for_id,
19 mk_var,
20 mk_bounded_var,
21 mk_string_const,
22 mk_int_const,
23 mk_real_const,
24 mk_bool_const,
25 mk_empty_set,
26 mk_full_set,
27 mk_record_const,
28 mk_record_field,
29 mk_set,
30 mk_sort,
31 mk_sort_with_cardinality,
32 pop_frame, push_frame,
33 mk_op,
34 mk_op_arglist,
35 mk_op_reverse,
36 mk_op_domain,
37 mk_op_range,
38 mk_op_image,
39 mk_op_cartesian,
40 mk_op_identity,
41 mk_op_interval,
42 mk_op_pow_subset,
43 mk_op_pow1_subset,
44 mk_op_composition,
45 mk_op_direct_product,
46 mk_op_parallel_product,
47 mk_op_iteration,
48 mk_op_closure,
49 mk_op_dom_res,
50 mk_op_couple_prj,
51 mk_op_dom_sub,
52 mk_op_ran_res,
53 mk_op_ran_sub,
54 mk_op_general_union,
55 mk_op_general_intersection,
56 mk_op_lambda,
57 mk_op_comprehension_set_multi,
58 mk_op_comprehension_set_singleton,
59 mk_op_floor,
60 mk_op_ceiling,
61 smt_solve_query,
62 reset,
63 get_model_string,
64 get_full_model_string,
65 mk_quantifier,
66 conjoin_negated_state,
67 add_interpreter_constraint,
68 mk_couple,
69 get_header_version,
70 get_full_version]).
71 % will be called by solver_interface:
72 :- public mk_var/4, mk_bounded_var/4, mk_empty_set/3, mk_int_const/3, mk_real_const/3, mk_bool_const/2, mk_string_const/3.
73 :- public mk_set/3, mk_sort/2, mk_sort_with_cardinality/5, mk_record_const/4, mk_record_field/4.
74 :- public mk_op/5, mk_quantifier/5, mk_op_arglist/4, get_model_string/2, conjoin_negated_state/4.
75 :- public pop_frame/0, push_frame/0, add_interpreter_constraint/4, mk_couple/5, mk_op_image/7, mk_op_reverse/4, mk_op_domain/6, mk_op_range/6.
76 :- public mk_op_comprehension_set_multi/5, mk_op_comprehension_set_singleton/4, mk_op_general_union/5, mk_op_general_intersection/6.
77 :- public mk_op_interval/4, mk_op_pow_subset/4, mk_op_pow1_subset/5, mk_op_identity/5, mk_op_couple_prj/5, mk_op_composition/8, mk_op_direct_product/8, mk_op_parallel_product/9.
78 :- public mk_op_dom_res/5, mk_op_dom_sub/5, mk_op_ran_res/5, mk_op_ran_sub/5, mk_op_lambda/6, mk_op_iteration/7, mk_op_closure/7, mk_op_cartesian/5, mk_op_floor/5, mk_op_ceiling/5.
79
80 :- public mk_full_set/3, get_full_model_string/1, reset/0, smt_solve_query/6, get_header_version/1, get_full_version/1. % Z3 only
81
82 % function declarations
83 foreign(init, c, init).
84 foreign(pretty_print_smt, c, pretty_print_smt).
85 foreign(pretty_print_smt_for_id, c, pretty_print_smt_for_id(+atom, +integer)).
86 foreign(mk_var, c, mk_var(+atom, +term, +string, [-integer])). % creates a variable; second argument is an atom of the type,
87 % third argument is the identifier
88 foreign(mk_bounded_var, c, mk_bounded_var(+atom, +term, +string, [-integer])).
89 foreign(mk_empty_set, c, mk_empty_set(+atom, +term, [-integer])).
90 foreign(mk_full_set, c, mk_full_set(+atom, +term, [-integer])).
91 foreign(mk_int_const, c, mk_int_const(+atom, +integer, [-integer])). % creates an int constant
92 foreign(mk_real_const, c, mk_real_const(+atom, +string, [-integer])). % creates a real constant
93 foreign(mk_bool_const, c, mk_bool_const(+string, [-integer])). % creates a bool constant
94 foreign(mk_string_const, c, mk_string_const(+atom, +string, [-integer])).
95 foreign(mk_set, c, mk_set(+atom, +term, [-integer])).
96 foreign(mk_sort, c, mk_sort(+atom, +atom)).
97 foreign(mk_sort_with_cardinality, c, mk_sort_with_cardinality(+atom, +atom, +integer, +term, [-term])).
98 foreign(mk_record_const, c, mk_record_const(+atom, +term, +term, [-integer])).
99 foreign(mk_record_field, c, mk_record_field(+atom, +integer, +integer, [-integer])).
100 foreign(mk_op, c, mk_op(+atom, +string, +integer, +integer, [-integer])).
101 foreign(mk_quantifier, c, mk_quantifier(+atom, +string, +term, +integer, [-integer])).
102 foreign(mk_op_arglist, c, mk_op_arglist(+atom, +string, +term, [-integer])).
103 foreign(mk_op_identity, c, mk_op_identity(+atom, +integer, +term, +term, [-integer])).
104 foreign(mk_op_interval, c, mk_op_interval(+atom, +integer, +integer, [-integer])).
105 foreign(mk_op_pow_subset, c, mk_op_pow_subset(+atom, +integer, +term, [-integer])).
106 foreign(mk_op_pow1_subset, c, mk_op_pow1_subset(+atom, +integer, +term, +term, [-integer])).
107 foreign(mk_op_composition, c, mk_op_composition(+atom, +integer, +integer, +term, +term, +term, +term, [-integer])).
108 foreign(mk_op_direct_product, c, mk_op_direct_product(+atom, +integer, +integer, +term, +term, +term, +term, [-integer])).
109 foreign(mk_op_parallel_product, c, mk_op_parallel_product(+atom, +integer, +integer, +term, +term, +term, +term, +term, [-integer])).
110 foreign(mk_op_iteration, c, mk_op_iteration(+atom, +integer, +integer, +term, +term, +term, [-integer])).
111 foreign(mk_op_closure, c, mk_op_closure(+atom, +integer, +integer, +term, +term, +term, [-integer])).
112 foreign(mk_op_cartesian, c, mk_op_cartesian(+atom, +integer, +integer, +term, [-integer])).
113 foreign(mk_op_dom_res, c, mk_op_dom_res(+atom, +integer, +integer, +term, [-integer])).
114 foreign(mk_op_dom_sub, c, mk_op_dom_sub(+atom, +integer, +integer, +term, [-integer])).
115 foreign(mk_op_ran_res, c, mk_op_ran_res(+atom, +integer, +integer, +term, [-integer])).
116 foreign(mk_op_ran_sub, c, mk_op_ran_sub(+atom, +integer, +integer, +term, [-integer])).
117 foreign(mk_op_reverse, c, mk_op_reverse(+atom, +integer, +term, [-integer])).
118 foreign(mk_op_domain, c, mk_op_domain(+atom, +integer, +term, +term, +term, [-integer])).
119 foreign(mk_op_range, c, mk_op_range(+atom, +integer, +term, +term, +term, [-integer])).
120 foreign(mk_op_image, c, mk_op_image(+atom, +integer, +integer, +term, +term, +term, [-integer])).
121 foreign(mk_op_general_union, c, mk_op_general_union(+atom, +integer, +term, +term, [-integer])).
122 foreign(mk_op_general_intersection, c, mk_op_general_intersection(+atom, +atom, +integer, +term, +term, [-integer])).
123 foreign(mk_op_lambda, c, mk_op_lambda(+atom, +integer, +integer, +integer, +term, [-integer])).
124 foreign(mk_op_comprehension_set_singleton, c, mk_op_comprehension_set_singleton(+atom, +integer, +integer, [-integer])).
125 foreign(mk_op_comprehension_set_multi, c, mk_op_comprehension_set_multi(+atom, +term, +term, +integer, [-integer])).
126 foreign(mk_op_couple_prj, c, mk_op_couple_prj(+atom, +atom, +integer, +term, [-integer])).
127 foreign(mk_op_floor, c, mk_op_floor(+atom, +integer, +atom, +integer, [-integer])).
128 foreign(mk_op_ceiling, c, mk_op_ceiling(+atom, +integer, +atom, +integer, [-integer])).
129 foreign(smt_solve_query, c, smt_solve_query(+term, +integer, +integer, +integer, +integer, [-term])).
130 foreign(get_model_string, c, get_model_string(+integer, [-atom])).
131 foreign(get_full_model_string, c, get_full_model_string([-atom])).
132 foreign(conjoin_negated_state, c, conjoin_negated_state(+atom, +term, +integer, [-integer])).
133 foreign(pop_frame, c, pop_frame).
134 foreign(push_frame, c, push_frame).
135 foreign(reset, c, reset).
136 foreign(add_interpreter_constraint, c, add_interpreter_constraint(+integer, +atom, +integer, [-term])).
137 foreign(mk_couple, c, mk_couple(+atom, +term, +integer, +integer, [-integer])).
138 foreign(get_header_version, c, get_header_version([-atom])).
139 foreign(get_full_version, c, get_full_version([-atom])).
140
141 :- dynamic is_initialised/0, z3_init_exception/1.
142
143 z3interface_init_error(E) :- z3_init_exception(Exc),!, Exc=E.
144 z3interface_init_error(unknown) :- \+ is_initialised.
145
146 :- use_module(probsrc(pathes_lib), [check_lib_component_available/1]).
147 init_z3interface :- is_initialised,!.
148 init_z3interface :-
149 catch(load_foreign_resource(library(z3interface)),E,
150 (format(user_error,'*** LOADING Z3 library failed~n',[]),
151 format(user_error,'Try installing Z3 with probcli -install z3~n',[]),
152 assert(z3_init_exception(E)), % asserted and then added as error by solver_dispatcher
153 check_lib_component_available(z3),
154 fail)
155 ),
156 init,
157 assertz(is_initialised).
158
159 reset_z3interface :- is_initialised, !,
160 reset.
161 reset_z3interface :- init_z3interface.
162
163 :- meta_predicate z3_interface_call(+).
164 z3_interface_call(Call) :-
165 call(z3interface:Call).