1		:- module(cvc4interface, [init_cvc4interface/0,
2		reset_cvc4interface/0, % TODO: make more lightweight once cvc 1.5 is out
3		cvc4_interface_call/1]).
4
5		:- use_module('../../src/module_information.pl').
6		:- module_info(group,experimental).
7		:- module_info(description,'This is the interface between ProB and the CVC4 SMT solver').
8
9		/*
10		:- use_module(probsrc(bsyntaxtree), [map_over_typed_bexpr/2,
11		find_typed_identifier_uses/3,
12		get_texpr_type/2,
13		get_texpr_id/2]).
14		*/
15		foreign_resource('cvc4interface', [init,
16		reset,
17		mk_var,
18		mk_bounded_var,
19		mk_int_const,
20		mk_string_const,
21		mk_bool_const,
22		mk_empty_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		setup_enumerated_set,
30		mk_op,
31		mk_op_arglist,
32		query,
33		get_string,
34		mk_quantifier,
35		conjoin_negated_state,
36		add_interpreter_constraint,
37		mk_couple]).
38
39		% will be called by solver_interface:
40		:- public mk_var/3, mk_bounded_var/3, mk_empty_set/2, mk_int_const/2, mk_bool_const/2, mk_string_const/2.
41		:- public mk_set/2, mk_sort/1, mk_sort_with_cardinality/2, mk_record_const/3, mk_record_field/4.
42		:- public setup_enumerated_set/1, mk_op/4, mk_quantifier/4, mk_op_arglist/3, query/3, get_string/2, conjoin_negated_state/3.
43		:- public pop_frame/0, push_frame/0, add_interpreter_constraint/4, mk_couple/4.
44
45		% function declarations
46		foreign(init, c, init).
47		foreign(reset, c, reset).
48		foreign(mk_var, c, mk_var(+term, +string, [-integer])). % creates a variable; first argument is an atom of the type,
49		% second argument is the identifier
50		foreign(mk_bounded_var, c, mk_bounded_var(+term, +string, [-integer])).
51		foreign(mk_empty_set, c, mk_empty_set(+term, [-integer])).
52		foreign(mk_int_const, c, mk_int_const(+integer, [-integer])). % creates an int constant
53		foreign(mk_bool_const, c, mk_bool_const(+string, [-integer])). % creates a bool constant
54		foreign(mk_string_const, c, mk_string_const(+atom, [-integer])).
55		foreign(mk_set, c, mk_set(+term, [-integer])).
56		foreign(mk_sort, c, mk_sort(+atom)).
57		foreign(mk_sort_with_cardinality, c, mk_sort_with_cardinality(+atom,+integer)).
58		foreign(mk_record_const, c, mk_record_const(+term, +term, [-integer])).
59		foreign(mk_record_field, c, mk_record_field(+integer, +integer, +atom, [-integer])).
60		foreign(setup_enumerated_set, c, setup_enumerated_set(+term)).
61		foreign(mk_op, c, mk_op(+string, +integer, +integer, [-integer])).
62		foreign(mk_quantifier, c, mk_quantifier(+string, +term, +integer, [-integer])).
63		foreign(mk_op_arglist, c, mk_op_arglist(+string, +term, [-integer])).
64		foreign(query, c, query(+integer,+integer,[-atom])).
65		foreign(get_string, c, get_string(+integer, [-atom])).
66		foreign(conjoin_negated_state, c, conjoin_negated_state(+term,+integer,[-integer])).
67		foreign(pop_frame, c, pop_frame).
68		foreign(push_frame, c, push_frame).
69		foreign(add_interpreter_constraint, c, add_interpreter_constraint(+integer,+atom,+integer,[-term])).
70		foreign(mk_couple, c, mk_couple(+term,+integer,+integer,[-integer])).
71
72
73		%:- load_foreign_resource(cvc4interface).
74		:- dynamic is_initialised/0.
75
76		init_cvc4interface :- is_initialised,!.
77		init_cvc4interface :-
78		catch(load_foreign_resource(library(cvc4interface)),_,fail),
79		init,
80		assert(is_initialised).
81
82		reset_cvc4interface :- is_initialised, !,
83		reset.
84		reset_cvc4interface :- init_cvc4interface.
85
86		:- meta_predicate cvc4_interface_call(+).
87		cvc4_interface_call(Call) :-
88		call(Call).