1 % (c) 2015-2022 Lehrstuhl fuer Softwaretechnik und Programmiersprachen,
2 % Heinrich Heine Universitaet Duesseldorf
3 % This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html)
4
5 :- module(cvc4interface, [init_cvc4interface/0,
6 reset_cvc4interface/0, % TODO: make more lightweight once cvc 1.5 is out
7 cvc4_interface_call/1]).
8
9 :- use_module('../../src/module_information.pl').
10 :- module_info(group,smt_solvers).
11 :- module_info(description,'This is the interface between ProB and the CVC4 SMT solver').
12
13 /*
14 :- use_module(probsrc(bsyntaxtree), [map_over_typed_bexpr/2,
15 find_typed_identifier_uses/3,
16 get_texpr_type/2,
17 get_texpr_id/2]).
18 */
19 foreign_resource('cvc4interface', [init,
20 reset,
21 mk_var,
22 mk_bounded_var,
23 mk_int_const,
24 mk_string_const,
25 mk_bool_const,
26 mk_empty_set,
27 mk_record_const,
28 mk_record_field,
29 mk_set,
30 mk_sort,
31 mk_sort_with_cardinality,
32 pop_frame, push_frame,
33 setup_enumerated_set,
34 mk_op,
35 mk_op_arglist,
36 smt_solve_query,
37 get_model_string,
38 mk_quantifier,
39 conjoin_negated_state,
40 add_interpreter_constraint,
41 mk_couple]).
42
43 % will be called by solver_interface:
44 :- public mk_var/4, mk_bounded_var/4, mk_empty_set/3, mk_int_const/3, mk_bool_const/2, mk_string_const/2.
45 :- public mk_set/3, mk_sort/2, mk_sort_with_cardinality/3, mk_record_const/4, mk_record_field/5.
46 :- public setup_enumerated_set/1, mk_op/5, mk_quantifier/5, mk_op_arglist/4, smt_solve_query/3, get_model_string/2, conjoin_negated_state/4.
47 :- public pop_frame/0, push_frame/0, add_interpreter_constraint/4, mk_couple/5.
48
49 %%
50 % Just one translation for CVC4 for now.
51 % Remove these wrappers and branch on the translation type in the CVC4 C++ interface
52 % to provide alternative translations as is done for Z3.
53 mk_var(_TranslationType, A2, A3, A4) :-
54 mk_var(A2, A3, A4).
55
56 mk_bounded_var(_TranslationType, A2, A3, A4) :-
57 mk_bounded_var(A2, A3, A4).
58
59 mk_empty_set(_TranslationType, A2, A3) :-
60 mk_empty_set(A2, A3).
61
62 mk_int_const(_TranslationType, A2, A3) :-
63 mk_int_const(A2, A3).
64
65 mk_set(_TranslationType, A2, A3) :-
66 mk_set(A2, A3).
67
68 mk_sort(_TranslationType, A2) :-
69 mk_sort(A2).
70
71 mk_sort_with_cardinality(_TranslationType, A2, A3) :-
72 mk_sort_with_cardinality(A2, A3).
73
74 mk_record_const(_TranslationType, A2, A3, A4) :-
75 mk_record_const(A2, A3, A4).
76
77 mk_record_field(_TranslationType, A2, A3, A4, A5) :-
78 mk_record_field(A2, A3, A4, A5).
79
80 mk_op(_TranslationType, A2, A3, A4, A5) :-
81 mk_op(A2, A3, A4, A5).
82
83 conjoin_negated_state(_TranslationType, A2, A3, A4) :-
84 conjoin_negated_state(A2, A3, A4).
85
86 mk_couple(_TranslationType, A2, A3, A4, A5) :-
87 mk_couple(A2, A3, A4, A5).
88
89 mk_quantifier(_TranslationType, A2, A3, A4, A5) :-
90 mk_quantifier(A2, A3, A4, A5).
91
92 mk_op_arglist(_TranslationType, A2, A3, A4) :-
93 mk_op_arglist(A2, A3, A4).
94 %%
95
96 % function declarations
97 foreign(init, c, init).
98 foreign(reset, c, reset).
99 foreign(mk_var, c, mk_var(+term, +string, [-integer])). % creates a variable; first argument is an atom of the type,
100 % second argument is the identifier
101 foreign(mk_bounded_var, c, mk_bounded_var(+term, +string, [-integer])).
102 foreign(mk_empty_set, c, mk_empty_set(+term, [-integer])).
103 foreign(mk_int_const, c, mk_int_const(+integer, [-integer])). % creates an int constant
104 foreign(mk_bool_const, c, mk_bool_const(+string, [-integer])). % creates a bool constant
105 foreign(mk_string_const, c, mk_string_const(+atom, [-integer])).
106 foreign(mk_set, c, mk_set(+term, [-integer])).
107 foreign(mk_sort, c, mk_sort(+atom)).
108 foreign(mk_sort_with_cardinality, c, mk_sort_with_cardinality(+atom,+integer)).
109 foreign(mk_record_const, c, mk_record_const(+term, +term, [-integer])).
110 foreign(mk_record_field, c, mk_record_field(+integer, +integer, +atom, [-integer])).
111 foreign(setup_enumerated_set, c, setup_enumerated_set(+term)).
112 foreign(mk_op, c, mk_op(+string, +integer, +integer, [-integer])).
113 foreign(mk_quantifier, c, mk_quantifier(+string, +term, +integer, [-integer])).
114 foreign(mk_op_arglist, c, mk_op_arglist(+string, +term, [-integer])).
115 foreign(smt_solve_query, c, smt_solve_query(+integer,+integer,[-atom])).
116 foreign(get_model_string, c, get_model_string(+integer, [-atom])).
117 foreign(conjoin_negated_state, c, conjoin_negated_state(+term,+integer,[-integer])).
118 foreign(pop_frame, c, pop_frame).
119 foreign(push_frame, c, push_frame).
120 foreign(add_interpreter_constraint, c, add_interpreter_constraint(+integer,+atom,+integer,[-term])).
121 foreign(mk_couple, c, mk_couple(+term,+integer,+integer,[-integer])).
122
123
124 %:- load_foreign_resource(cvc4interface).
125 :- dynamic is_initialised/0.
126
127 init_cvc4interface :- is_initialised,!.
128 init_cvc4interface :-
129 catch(load_foreign_resource(library(cvc4interface)),E,(format(user_error,'*** LOADING CVC4 library failed~n*** Be sure to have libcvc4.dylib/so/dll on your dynamic library path (LD_LIBRARY_PATH or DYLD_LIBRARY_PATH).~n*** ~w~n',[E]),fail)),
130 init,
131 assertz(is_initialised).
132
133 reset_cvc4interface :- is_initialised, !,
134 reset.
135 reset_cvc4interface :- init_cvc4interface.
136
137 :- meta_predicate cvc4_interface_call(+).
138 cvc4_interface_call(Call) :-
139 call(Call).