1 % (c) 2015-2026 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,
7 cvc4_interface_call/1]).
8
9 :- use_module('../../src/module_information.pl').
10 :- use_module(probsrc(tools_strings), [ajoin/2]).
11 :- module_info(group,smt_solvers).
12 :- module_info(description,'This is the interface between ProB and the cvc5 SMT solver (formerly CVC4, hence the name of the module and of the solver cvc4 in ProB)').
13
14 /*
15 :- use_module(probsrc(bsyntaxtree), [map_over_typed_bexpr/2,
16 find_typed_identifier_uses/3,
17 get_texpr_type/2,
18 get_texpr_id/2]).
19 */
20 foreign_resource('cvc4interface', [init,
21 reset,
22 mk_var,
23 mk_bounded_var,
24 mk_int_const,
25 mk_string_const,
26 mk_bool_const,
27 mk_empty_set,
28 mk_record_const,
29 mk_record_field,
30 mk_set,
31 mk_sort,
32 mk_sort_with_cardinality,
33 pop_frame, push_frame,
34 mk_op,
35 mk_op_arglist,
36 mk_op_couple_prj,
37 mk_op_closure,
38 smt_solve_query,
39 get_model_string,
40 get_model_value,
41 mk_quantifier,
42 conjoin_negated_state,
43 add_interpreter_constraint,
44 mk_couple,
45 get_version]).
46
47 % will be called by solver_interface:
48 :- public mk_var/4, mk_bounded_var/4, mk_empty_set/3, mk_int_const/3, mk_bool_const/2, mk_string_const/3.
49 :- public mk_set/3, mk_sort/2, mk_sort_with_cardinality/5, mk_record_const/4, mk_record_field/4.
50 :- public mk_op/5, mk_quantifier/5, mk_op_arglist/4, mk_op_couple_prj/5, mk_op_closure/7.
51 :- public smt_solve_query/3, get_model_string/2, get_model_value/2, conjoin_negated_state/4.
52 :- public pop_frame/0, push_frame/0, add_interpreter_constraint/4, mk_couple/5, get_version/1.
53
54 %%
55 % Just one translation (axiomatic) for cvc5 for now.
56 % The wrappers drop the translation type passed by smt_solvers_interface.
57 % Operators that are not supported are filtered by smt_solvers_interface:unsupported_expr/4,
58 % see also cvc4_interface_call/1.
59 mk_var(_TranslationType, A2, A3, A4) :-
60 mk_var(A2, A3, A4).
61
62 mk_bounded_var(_TranslationType, A2, A3, A4) :-
63 mk_bounded_var(A2, A3, A4).
64
65 mk_empty_set(_TranslationType, A2, A3) :-
66 mk_empty_set(A2, A3).
67
68 mk_int_const(_TranslationType, A2, A3) :-
69 mk_int_const(A2, A3).
70
71 mk_string_const(_TranslationType, A2, A3) :-
72 mk_string_const(A2, A3).
73
74 mk_set(_TranslationType, A2, A3) :-
75 mk_set(A2, A3).
76
77 mk_sort(_TranslationType, A2) :-
78 mk_sort(A2).
79
80 mk_sort_with_cardinality(_TranslationType, SetName, Cardinality, ElementNames, ElementExprs) :-
81 mk_sort_with_cardinality(SetName, Cardinality, ElementNames, ElementExprs).
82
83 mk_record_const(_TranslationType, A2, A3, A4) :-
84 mk_record_const(A2, A3, A4).
85
86 mk_record_field(_TranslationType, A2, A3, A4) :-
87 mk_record_field(A2, A3, A4).
88
89 mk_op(_TranslationType, A2, A3, A4, A5) :-
90 mk_op(A2, A3, A4, A5).
91
92 conjoin_negated_state(_TranslationType, A2, A3, A4) :-
93 conjoin_negated_state(A2, A3, A4).
94
95 mk_couple(_TranslationType, A2, A3, A4, A5) :-
96 mk_couple(A2, A3, A4, A5).
97
98 mk_quantifier(_TranslationType, A2, A3, A4, A5) :-
99 mk_quantifier(A2, A3, A4, A5).
100
101 mk_op_arglist(_TranslationType, A2, A3, A4) :-
102 mk_op_arglist(A2, A3, A4).
103
104 mk_op_couple_prj(_TranslationType, FirstOrSecond, A3, CoupleType, A5) :-
105 mk_op_couple_prj(FirstOrSecond, A3, CoupleType, A5).
106
107 mk_op_closure(_TranslationType, IsReflexive, A3, Type, CoupleType, ExistsVarType, A7) :-
108 mk_op_closure(IsReflexive, A3, Type, CoupleType, ExistsVarType, A7).
109 %%
110
111 % function declarations
112 foreign(init, c, init).
113 foreign(reset, c, reset).
114 foreign(mk_var, c, mk_var(+term, +string, [-integer])). % creates a variable; first argument is the type,
115 % second argument is the identifier
116 foreign(mk_bounded_var, c, mk_bounded_var(+term, +string, [-integer])).
117 foreign(mk_empty_set, c, mk_empty_set(+term, [-integer])).
118 foreign(mk_int_const, c, mk_int_const(+integer, [-integer])). % creates an int constant
119 foreign(mk_bool_const, c, mk_bool_const(+string, [-integer])). % creates a bool constant
120 foreign(mk_string_const, c, mk_string_const(+string, [-integer])).
121 foreign(mk_set, c, mk_set(+term, [-integer])).
122 foreign(mk_sort, c, mk_sort(+atom)). % deferred set
123 foreign(mk_sort_with_cardinality, c, mk_sort_with_cardinality(+atom,+integer,+term,[-term])). % enumerated set, returns the elements
124 foreign(mk_record_const, c, mk_record_const(+term, +term, [-integer])).
125 foreign(mk_record_field, c, mk_record_field(+integer, +integer, [-integer])). % the field number starts at 0
126 foreign(mk_op, c, mk_op(+string, +integer, +integer, [-integer])).
127 foreign(mk_quantifier, c, mk_quantifier(+string, +term, +integer, [-integer])).
128 foreign(mk_op_arglist, c, mk_op_arglist(+string, +term, [-integer])).
129 foreign(mk_op_couple_prj, c, mk_op_couple_prj(+atom, +integer, +term, [-integer])).
130 foreign(mk_op_closure, c, mk_op_closure(+integer, +integer, +term, +term, +term, [-integer])).
131 foreign(smt_solve_query, c, smt_solve_query(+integer,+integer,[-atom])).
132 foreign(get_model_string, c, get_model_string(+integer, [-atom])). % SMT-LIB syntax, for debugging
133 foreign(get_model_value, c, get_model_value(+integer, [-term])). % see model_translation:translate_cvc5_value/3
134 foreign(conjoin_negated_state, c, conjoin_negated_state(+term,+integer,[-integer])).
135 foreign(pop_frame, c, pop_frame).
136 foreign(push_frame, c, push_frame).
137 foreign(add_interpreter_constraint, c, add_interpreter_constraint(+integer,+atom,+integer,[-term])).
138 foreign(mk_couple, c, mk_couple(+term,+integer,+integer,[-integer])).
139 foreign(get_version, c, get_version([-atom])).
140
141
142 %:- load_foreign_resource(cvc4interface).
143 :- dynamic is_initialised/0.
144
145 init_cvc4interface :- is_initialised,!.
146 init_cvc4interface :-
147 catch(load_foreign_resource(library(cvc4interface)),E,(format(user_error,'*** LOADING cvc5 interface failed~n*** Be sure to have libcvc5.dylib/so on your dynamic library path (LD_LIBRARY_PATH or DYLD_LIBRARY_PATH).~n*** ~w~n',[E]),fail)),
148 init,
149 assertz(is_initialised).
150
151 reset_cvc4interface :- is_initialised, !,
152 reset.
153 reset_cvc4interface :- init_cvc4interface.
154
155 :- meta_predicate cvc4_interface_call(+).
156 % Operators that are only implemented for Z3 (e.g., mk_op_interval) should be filtered by smt_solvers_interface;
157 % if one is called nevertheless, this is reported as a logic_exception (as for other unsupported input),
158 % so that the solver answers unknown.
159 cvc4_interface_call(Call) :-
160 catch(call(Call), error(existence_error(procedure, cvc4interface:PI), _),
161 (ajoin(['operator not supported by cvc5 interface: ',PI], Msg),
162 throw(logic_exception(Msg)))).