z3interface

foreign(init, c, init).

foreign(pretty_print_smt, c, pretty_print_smt).

foreign(pretty_print_smt_for_id, c, pretty_print_smt_for_id(+atom, +integer)).

foreign(mk_var, c, mk_var(+atom, +term, +string, [-integer])). % creates a variable; second argument is an atom of the type,

foreign(mk_bounded_var, c, mk_bounded_var(+atom, +term, +string, [-integer])).

foreign(mk_empty_set, c, mk_empty_set(+atom, +term, [-integer])).

foreign(mk_full_set, c, mk_full_set(+atom, +term, [-integer])).

foreign(mk_int_const, c, mk_int_const(+atom, +integer, [-integer])). % creates an int constant

foreign(mk_real_const, c, mk_real_const(+atom, +string, [-integer])). % creates a real constant

foreign(mk_bool_const, c, mk_bool_const(+string, [-integer])). % creates a bool constant

foreign(mk_string_const, c, mk_string_const(+atom, +string, [-integer])).

foreign(mk_set, c, mk_set(+atom, +term, [-integer])).

foreign(mk_sort, c, mk_sort(+atom, +atom)).

foreign(mk_sort_with_cardinality, c, mk_sort_with_cardinality(+atom, +atom, +integer, +term, [-term])).

foreign(mk_record_const, c, mk_record_const(+atom, +term, +term, [-integer])).

foreign(mk_record_field, c, mk_record_field(+atom, +integer, +integer, [-integer])).

foreign(mk_op, c, mk_op(+atom, +string, +integer, +integer, [-integer])).

foreign(mk_quantifier, c, mk_quantifier(+atom, +string, +term, +integer, [-integer])).

foreign(mk_op_arglist, c, mk_op_arglist(+atom, +string, +term, [-integer])).

foreign(mk_op_identity, c, mk_op_identity(+atom, +integer, +term, +term, [-integer])).

foreign(mk_op_interval, c, mk_op_interval(+atom, +integer, +integer, [-integer])).

foreign(mk_op_pow_subset, c, mk_op_pow_subset(+atom, +integer, +term, [-integer])).

foreign(mk_op_pow1_subset, c, mk_op_pow1_subset(+atom, +integer, +term, +term, [-integer])).

foreign(mk_op_composition, c, mk_op_composition(+atom, +integer, +integer, +term, +term, +term, +term, [-integer])).

foreign(mk_op_direct_product, c, mk_op_direct_product(+atom, +integer, +integer, +term, +term, +term, +term, [-integer])).

foreign(mk_op_parallel_product, c, mk_op_parallel_product(+atom, +integer, +integer, +term, +term, +term, +term, +term, [-integer])).

foreign(mk_op_iteration, c, mk_op_iteration(+atom, +integer, +integer, +term, +term, +term, [-integer])).

foreign(mk_op_closure, c, mk_op_closure(+atom, +integer, +integer, +term, +term, +term, [-integer])).

foreign(mk_op_cartesian, c, mk_op_cartesian(+atom, +integer, +integer, +term, [-integer])).

foreign(mk_op_dom_res, c, mk_op_dom_res(+atom, +integer, +integer, +term, [-integer])).

foreign(mk_op_dom_sub, c, mk_op_dom_sub(+atom, +integer, +integer, +term, [-integer])).

foreign(mk_op_ran_res, c, mk_op_ran_res(+atom, +integer, +integer, +term, [-integer])).

foreign(mk_op_ran_sub, c, mk_op_ran_sub(+atom, +integer, +integer, +term, [-integer])).

foreign(mk_op_reverse, c, mk_op_reverse(+atom, +integer, +term, [-integer])).

foreign(mk_op_domain, c, mk_op_domain(+atom, +integer, +term, +term, +term, [-integer])).

foreign(mk_op_range, c, mk_op_range(+atom, +integer, +term, +term, +term, [-integer])).

foreign(mk_op_image, c, mk_op_image(+atom, +integer, +integer, +term, +term, +term, [-integer])).

foreign(mk_op_general_union, c, mk_op_general_union(+atom, +integer, +term, +term, [-integer])).

foreign(mk_op_general_intersection, c, mk_op_general_intersection(+atom, +atom, +integer, +term, +term, [-integer])).

foreign(mk_op_lambda, c, mk_op_lambda(+atom, +integer, +integer, +integer, +term, [-integer])).

foreign(mk_op_comprehension_set_singleton, c, mk_op_comprehension_set_singleton(+atom, +integer, +integer, [-integer])).

foreign(mk_op_comprehension_set_multi, c, mk_op_comprehension_set_multi(+atom, +term, +term, +integer, [-integer])).

foreign(mk_op_couple_prj, c, mk_op_couple_prj(+atom, +atom, +integer, +term, [-integer])).

foreign(mk_op_floor, c, mk_op_floor(+atom, +integer, +atom, +integer, [-integer])).

foreign(mk_op_ceiling, c, mk_op_ceiling(+atom, +integer, +atom, +integer, [-integer])).

foreign(smt_solve_query, c, smt_solve_query(+term, +integer, +integer, +integer, +integer, [-term])).

foreign(get_model_string, c, get_model_string(+integer, [-atom])).

foreign(get_full_model_string, c, get_full_model_string([-atom])).

foreign(conjoin_negated_state, c, conjoin_negated_state(+atom, +term, +integer, [-integer])).

foreign(pop_frame, c, pop_frame).

foreign(push_frame, c, push_frame).

foreign(reset, c, reset).

foreign(add_interpreter_constraint, c, add_interpreter_constraint(+integer, +atom, +integer, [-term])).

foreign(mk_couple, c, mk_couple(+atom, +term, +integer, +integer, [-integer])).

foreign(get_header_version, c, get_header_version([-atom])).

foreign(get_full_version, c, get_full_version([-atom])).

foreign_resource(z3interface, [init,
    pretty_print_smt, pretty_print_smt_for_id,
    mk_var,
    mk_bounded_var,
    mk_string_const,
    mk_int_const,
    mk_real_const,
    mk_bool_const,
    mk_empty_set,
    mk_full_set,
    mk_record_const,
    mk_record_field,
    mk_set,
    mk_sort,
    mk_sort_with_cardinality,
    pop_frame, push_frame,
    mk_op,
    mk_op_arglist,
    mk_op_reverse,
    mk_op_domain,
    mk_op_range,
    mk_op_image,
    mk_op_cartesian,
    mk_op_identity,
    mk_op_interval,
    mk_op_pow_subset,
    mk_op_pow1_subset,
    mk_op_composition,
    mk_op_direct_product,
    mk_op_parallel_product,
    mk_op_iteration,
    mk_op_closure,
    mk_op_dom_res,
    mk_op_couple_prj,
    mk_op_dom_sub,
    mk_op_ran_res,
    mk_op_ran_sub,
    mk_op_general_union,
    mk_op_general_intersection,
    mk_op_lambda,
    mk_op_comprehension_set_multi,
    mk_op_comprehension_set_singleton,
    mk_op_floor,
    mk_op_ceiling,
    smt_solve_query,
    reset,
    get_model_string,
    get_full_model_string,
    mk_quantifier,
    conjoin_negated_state,
    add_interpreter_constraint,
    mk_couple,
    get_header_version,
    get_full_version]).

init_z3interface :- is_initialised,!.

init_z3interface :-
    catch(load_foreign_resource(library(z3interface)),E,
    (format(user_error,'*** LOADING Z3 library failed~n',[]),
    assert(z3_init_exception(E)), % asserted and then added as error by solver_dispatcher
    fail)
    ),
    init,
    assertz(is_initialised).

reset_z3interface :- is_initialised, !,
    reset.

reset_z3interface :- init_z3interface.

z3_interface_call(Call) :-
    call(z3interface:Call).

z3interface_init_error(E) :- z3_init_exception(Exc),!, Exc=E.

z3interface_init_error(unknown) :- \+ is_initialised.