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). |