| 1 | :- module(z3interface, [init_z3interface/0, | |
| 2 | reset_z3interface/0, % TODO: make more lightweight once cvc 1.5 is out | |
| 3 | pretty_print_smt1/0, % pretty print Z3's internal status and constraints | |
| 4 | pretty_print_smt2/0, % pretty print Z3's internal status and constraints | |
| 5 | pretty_print_smt2_for_id/1, % pretty print store + constraint pointed to by ID (previously created by z3_interface_call(s)) | |
| 6 | z3_interface_call/1]). | |
| 7 | ||
| 8 | :- use_module('../../src/module_information.pl'). | |
| 9 | :- module_info(group,experimental). | |
| 10 | :- module_info(description,'This is the interface between ProB and the Z3 SMT solver'). | |
| 11 | ||
| 12 | /* | |
| 13 | :- use_module(probsrc(bsyntaxtree), [map_over_typed_bexpr/2, | |
| 14 | find_typed_identifier_uses/3, | |
| 15 | get_texpr_type/2, | |
| 16 | get_texpr_id/2]). | |
| 17 | */ | |
| 18 | foreign_resource('z3interface', [init, | |
| 19 | pretty_print_smt1, pretty_print_smt2, pretty_print_smt2_for_id, | |
| 20 | mk_var, | |
| 21 | mk_bounded_var, | |
| 22 | mk_int_const, | |
| 23 | mk_bool_const, | |
| 24 | mk_empty_set, | |
| 25 | mk_full_set, | |
| 26 | mk_record_const, | |
| 27 | mk_record_field, | |
| 28 | mk_set, | |
| 29 | mk_sort, | |
| 30 | mk_sort_with_cardinality, | |
| 31 | pop_frame, push_frame, | |
| 32 | setup_enumerated_set, | |
| 33 | mk_op, | |
| 34 | mk_op_arglist, | |
| 35 | query, | |
| 36 | reset, | |
| 37 | get_string, | |
| 38 | get_full_model_string, | |
| 39 | mk_quantifier, | |
| 40 | conjoin_negated_state, | |
| 41 | add_interpreter_constraint, | |
| 42 | mk_couple]). | |
| 43 | % will be called by solver_interface: | |
| 44 | :- public mk_var/3, mk_bounded_var/3, mk_empty_set/2, mk_int_const/2, mk_bool_const/2. %, mk_string_const/2. | |
| 45 | :- public mk_set/2, mk_sort/1, mk_sort_with_cardinality/2, mk_record_const/3, mk_record_field/4. | |
| 46 | :- public setup_enumerated_set/1, mk_op/4, mk_quantifier/4, mk_op_arglist/3, query/3, get_string/2, conjoin_negated_state/3. | |
| 47 | :- public pop_frame/0, push_frame/0, add_interpreter_constraint/4, mk_couple/4. | |
| 48 | ||
| 49 | :- public mk_full_set/2, get_full_model_string/1, reset/0. % Z3 only | |
| 50 | ||
| 51 | % function declarations | |
| 52 | foreign(init, c, init). | |
| 53 | foreign(pretty_print_smt1, c, pretty_print_smt1). | |
| 54 | foreign(pretty_print_smt2, c, pretty_print_smt2). | |
| 55 | foreign(pretty_print_smt2_for_id, c, pretty_print_smt2_for_id(+integer)). | |
| 56 | foreign(mk_var, c, mk_var(+term, +string, [-integer])). % creates a variable; first argument is an atom of the type, | |
| 57 | % second argument is the identifier | |
| 58 | foreign(mk_bounded_var, c, mk_bounded_var(+term, +string, [-integer])). | |
| 59 | foreign(mk_empty_set, c, mk_empty_set(+term, [-integer])). | |
| 60 | foreign(mk_full_set, c, mk_full_set(+term, [-integer])). | |
| 61 | foreign(mk_int_const, c, mk_int_const(+integer, [-integer])). % creates an int constant | |
| 62 | foreign(mk_bool_const, c, mk_bool_const(+string, [-integer])). % creates a bool constant | |
| 63 | foreign(mk_set, c, mk_set(+term, [-integer])). | |
| 64 | foreign(mk_sort, c, mk_sort(+atom)). | |
| 65 | foreign(mk_sort_with_cardinality, c, mk_sort_with_cardinality(+atom,+integer)). | |
| 66 | foreign(mk_record_const, c, mk_record_const(+term, +term, [-integer])). | |
| 67 | foreign(mk_record_field, c, mk_record_field(+integer, +integer, +atom, [-integer])). | |
| 68 | foreign(setup_enumerated_set, c, setup_enumerated_set(+term)). | |
| 69 | foreign(mk_op, c, mk_op(+string, +integer, +integer, [-integer])). | |
| 70 | foreign(mk_quantifier, c, mk_quantifier(+string, +term, +integer, [-integer])). | |
| 71 | foreign(mk_op_arglist, c, mk_op_arglist(+string, +term, [-integer])). | |
| 72 | foreign(query, c, query(+integer,+integer,[-atom])). | |
| 73 | foreign(get_string, c, get_string(+integer, [-atom])). | |
| 74 | foreign(get_full_model_string, c, get_full_model_string([-atom])). | |
| 75 | foreign(conjoin_negated_state, c, conjoin_negated_state(+term,+integer,[-integer])). | |
| 76 | foreign(pop_frame, c, pop_frame). | |
| 77 | foreign(push_frame, c, push_frame). | |
| 78 | foreign(reset, c, reset). | |
| 79 | foreign(add_interpreter_constraint, c, add_interpreter_constraint(+integer,+atom,+integer,[-term])). | |
| 80 | foreign(mk_couple, c, mk_couple(+term,+integer,+integer,[-integer])). | |
| 81 | ||
| 82 | ||
| 83 | :- dynamic is_initialised/0. | |
| 84 | ||
| 85 | init_z3interface :- is_initialised,!. | |
| 86 | init_z3interface :- | |
| 87 | catch(load_foreign_resource(library(z3interface)),E,(format(user_error,'*** LOADING Z3 library failed~n*** ~w~n',[E]),fail)), | |
| 88 | init, | |
| 89 | assert(is_initialised). | |
| 90 | ||
| 91 | reset_z3interface :- is_initialised, !, | |
| 92 | reset. | |
| 93 | reset_z3interface :- init_z3interface. | |
| 94 | ||
| 95 | :- meta_predicate z3_interface_call(+). | |
| 96 | z3_interface_call(Call) :- | |
| 97 | call(z3interface:Call). |