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