1 /********************* */
2 /*! \file cvc4cpp.cpp
3 ** \verbatim
4 ** Top contributors (to current version):
5 ** Aina Niemetz, Andres Noetzli
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
8 ** in the top-level source directory) and their institutional affiliations.
9 ** All rights reserved. See the file COPYING in the top-level source
10 ** directory for licensing information.\endverbatim
11 **
12 ** \brief The CVC4 C++ API.
13 **
14 ** The CVC4 C++ API.
15 **/
16
17 #include "api/cvc4cpp.h"
18
19 #include "base/configuration.h"
20 #include "base/cvc4_assert.h"
21 #include "base/cvc4_check.h"
22 #include "expr/expr.h"
23 #include "expr/expr_manager.h"
24 #include "expr/kind.h"
25 #include "expr/metakind.h"
26 #include "expr/node_manager.h"
27 #include "expr/type.h"
28 #include "options/main_options.h"
29 #include "options/options.h"
30 #include "smt/model.h"
31 #include "smt/smt_engine.h"
32 #include "theory/logic_info.h"
33 #include "util/random.h"
34 #include "util/result.h"
35 #include "util/utility.h"
36
37 #include <cstring>
38 #include <sstream>
39
40 namespace CVC4 {
41 namespace api {
42
43 /* -------------------------------------------------------------------------- */
44 /* Kind */
45 /* -------------------------------------------------------------------------- */
46
47 /* Mapping from external (API) kind to internal kind. */
48 const static std::unordered_map<Kind, CVC4::Kind, KindHashFunction> s_kinds{
49 {INTERNAL_KIND, CVC4::Kind::UNDEFINED_KIND},
50 {UNDEFINED_KIND, CVC4::Kind::UNDEFINED_KIND},
51 {NULL_EXPR, CVC4::Kind::NULL_EXPR},
52 /* Builtin ------------------------------------------------------------- */
53 {UNINTERPRETED_CONSTANT, CVC4::Kind::UNINTERPRETED_CONSTANT},
54 {ABSTRACT_VALUE, CVC4::Kind::ABSTRACT_VALUE},
55 {FUNCTION, CVC4::Kind::FUNCTION},
56 {APPLY, CVC4::Kind::APPLY},
57 {EQUAL, CVC4::Kind::EQUAL},
58 {DISTINCT, CVC4::Kind::DISTINCT},
59 {VARIABLE, CVC4::Kind::VARIABLE},
60 {BOUND_VARIABLE, CVC4::Kind::BOUND_VARIABLE},
61 {LAMBDA, CVC4::Kind::LAMBDA},
62 {CHOICE, CVC4::Kind::CHOICE},
63 {CHAIN, CVC4::Kind::CHAIN},
64 {CHAIN_OP, CVC4::Kind::CHAIN_OP},
65 /* Boolean ------------------------------------------------------------- */
66 {CONST_BOOLEAN, CVC4::Kind::CONST_BOOLEAN},
67 {NOT, CVC4::Kind::NOT},
68 {AND, CVC4::Kind::AND},
69 {IMPLIES, CVC4::Kind::IMPLIES},
70 {OR, CVC4::Kind::OR},
71 {XOR, CVC4::Kind::XOR},
72 {ITE, CVC4::Kind::ITE},
73 /* UF ------------------------------------------------------------------ */
74 {APPLY_UF, CVC4::Kind::APPLY_UF},
75 {CARDINALITY_CONSTRAINT, CVC4::Kind::CARDINALITY_CONSTRAINT},
76 {HO_APPLY, CVC4::Kind::HO_APPLY},
77 /* Arithmetic ---------------------------------------------------------- */
78 {PLUS, CVC4::Kind::PLUS},
79 {MULT, CVC4::Kind::MULT},
80 {MINUS, CVC4::Kind::MINUS},
81 {UMINUS, CVC4::Kind::UMINUS},
82 {DIVISION, CVC4::Kind::DIVISION},
83 {DIVISION_TOTAL, CVC4::Kind::DIVISION_TOTAL},
84 {INTS_DIVISION, CVC4::Kind::INTS_DIVISION},
85 {INTS_DIVISION_TOTAL, CVC4::Kind::INTS_DIVISION_TOTAL},
86 {INTS_MODULUS, CVC4::Kind::INTS_MODULUS},
87 {INTS_MODULUS_TOTAL, CVC4::Kind::INTS_MODULUS_TOTAL},
88 {ABS, CVC4::Kind::ABS},
89 {DIVISIBLE, CVC4::Kind::DIVISIBLE},
90 {POW, CVC4::Kind::POW},
91 {EXPONENTIAL, CVC4::Kind::EXPONENTIAL},
92 {SINE, CVC4::Kind::SINE},
93 {COSINE, CVC4::Kind::COSINE},
94 {TANGENT, CVC4::Kind::TANGENT},
95 {COSECANT, CVC4::Kind::COSECANT},
96 {SECANT, CVC4::Kind::SECANT},
97 {COTANGENT, CVC4::Kind::COTANGENT},
98 {ARCSINE, CVC4::Kind::ARCSINE},
99 {ARCCOSINE, CVC4::Kind::ARCCOSINE},
100 {ARCTANGENT, CVC4::Kind::ARCTANGENT},
101 {ARCCOSECANT, CVC4::Kind::ARCCOSECANT},
102 {ARCSECANT, CVC4::Kind::ARCSECANT},
103 {ARCCOTANGENT, CVC4::Kind::ARCCOTANGENT},
104 {SQRT, CVC4::Kind::SQRT},
105 {DIVISIBLE_OP, CVC4::Kind::DIVISIBLE_OP},
106 {CONST_RATIONAL, CVC4::Kind::CONST_RATIONAL},
107 {LT, CVC4::Kind::LT},
108 {LEQ, CVC4::Kind::LEQ},
109 {GT, CVC4::Kind::GT},
110 {GEQ, CVC4::Kind::GEQ},
111 {IS_INTEGER, CVC4::Kind::IS_INTEGER},
112 {TO_INTEGER, CVC4::Kind::TO_INTEGER},
113 {TO_REAL, CVC4::Kind::TO_REAL},
114 {PI, CVC4::Kind::PI},
115 /* BV ------------------------------------------------------------------ */
116 {CONST_BITVECTOR, CVC4::Kind::CONST_BITVECTOR},
117 {BITVECTOR_CONCAT, CVC4::Kind::BITVECTOR_CONCAT},
118 {BITVECTOR_AND, CVC4::Kind::BITVECTOR_AND},
119 {BITVECTOR_OR, CVC4::Kind::BITVECTOR_OR},
120 {BITVECTOR_XOR, CVC4::Kind::BITVECTOR_XOR},
121 {BITVECTOR_NOT, CVC4::Kind::BITVECTOR_NOT},
122 {BITVECTOR_NAND, CVC4::Kind::BITVECTOR_NAND},
123 {BITVECTOR_NOR, CVC4::Kind::BITVECTOR_NOR},
124 {BITVECTOR_XNOR, CVC4::Kind::BITVECTOR_XNOR},
125 {BITVECTOR_COMP, CVC4::Kind::BITVECTOR_COMP},
126 {BITVECTOR_MULT, CVC4::Kind::BITVECTOR_MULT},
127 {BITVECTOR_PLUS, CVC4::Kind::BITVECTOR_PLUS},
128 {BITVECTOR_SUB, CVC4::Kind::BITVECTOR_SUB},
129 {BITVECTOR_NEG, CVC4::Kind::BITVECTOR_NEG},
130 {BITVECTOR_UDIV, CVC4::Kind::BITVECTOR_UDIV},
131 {BITVECTOR_UREM, CVC4::Kind::BITVECTOR_UREM},
132 {BITVECTOR_SDIV, CVC4::Kind::BITVECTOR_SDIV},
133 {BITVECTOR_SREM, CVC4::Kind::BITVECTOR_SREM},
134 {BITVECTOR_SMOD, CVC4::Kind::BITVECTOR_SMOD},
135 {BITVECTOR_UDIV_TOTAL, CVC4::Kind::BITVECTOR_UDIV_TOTAL},
136 {BITVECTOR_UREM_TOTAL, CVC4::Kind::BITVECTOR_UREM_TOTAL},
137 {BITVECTOR_SHL, CVC4::Kind::BITVECTOR_SHL},
138 {BITVECTOR_LSHR, CVC4::Kind::BITVECTOR_LSHR},
139 {BITVECTOR_ASHR, CVC4::Kind::BITVECTOR_ASHR},
140 {BITVECTOR_ULT, CVC4::Kind::BITVECTOR_ULT},
141 {BITVECTOR_ULE, CVC4::Kind::BITVECTOR_ULE},
142 {BITVECTOR_UGT, CVC4::Kind::BITVECTOR_UGT},
143 {BITVECTOR_UGE, CVC4::Kind::BITVECTOR_UGE},
144 {BITVECTOR_SLT, CVC4::Kind::BITVECTOR_SLT},
145 {BITVECTOR_SLE, CVC4::Kind::BITVECTOR_SLE},
146 {BITVECTOR_SGT, CVC4::Kind::BITVECTOR_SGT},
147 {BITVECTOR_SGE, CVC4::Kind::BITVECTOR_SGE},
148 {BITVECTOR_ULTBV, CVC4::Kind::BITVECTOR_ULTBV},
149 {BITVECTOR_SLTBV, CVC4::Kind::BITVECTOR_SLTBV},
150 {BITVECTOR_ITE, CVC4::Kind::BITVECTOR_ITE},
151 {BITVECTOR_REDOR, CVC4::Kind::BITVECTOR_REDOR},
152 {BITVECTOR_REDAND, CVC4::Kind::BITVECTOR_REDAND},
153 {BITVECTOR_EXTRACT_OP, CVC4::Kind::BITVECTOR_EXTRACT_OP},
154 {BITVECTOR_REPEAT_OP, CVC4::Kind::BITVECTOR_REPEAT_OP},
155 {BITVECTOR_ZERO_EXTEND_OP, CVC4::Kind::BITVECTOR_ZERO_EXTEND_OP},
156 {BITVECTOR_SIGN_EXTEND_OP, CVC4::Kind::BITVECTOR_SIGN_EXTEND_OP},
157 {BITVECTOR_ROTATE_LEFT_OP, CVC4::Kind::BITVECTOR_ROTATE_LEFT_OP},
158 {BITVECTOR_ROTATE_RIGHT_OP, CVC4::Kind::BITVECTOR_ROTATE_RIGHT_OP},
159 {BITVECTOR_EXTRACT, CVC4::Kind::BITVECTOR_EXTRACT},
160 {BITVECTOR_REPEAT, CVC4::Kind::BITVECTOR_REPEAT},
161 {BITVECTOR_ZERO_EXTEND, CVC4::Kind::BITVECTOR_ZERO_EXTEND},
162 {BITVECTOR_SIGN_EXTEND, CVC4::Kind::BITVECTOR_SIGN_EXTEND},
163 {BITVECTOR_ROTATE_LEFT, CVC4::Kind::BITVECTOR_ROTATE_LEFT},
164 {BITVECTOR_ROTATE_RIGHT, CVC4::Kind::BITVECTOR_ROTATE_RIGHT},
165 {INT_TO_BITVECTOR_OP, CVC4::Kind::INT_TO_BITVECTOR_OP},
166 {INT_TO_BITVECTOR, CVC4::Kind::INT_TO_BITVECTOR},
167 {BITVECTOR_TO_NAT, CVC4::Kind::BITVECTOR_TO_NAT},
168 /* FP ------------------------------------------------------------------ */
169 {CONST_FLOATINGPOINT, CVC4::Kind::CONST_FLOATINGPOINT},
170 {CONST_ROUNDINGMODE, CVC4::Kind::CONST_ROUNDINGMODE},
171 {FLOATINGPOINT_FP, CVC4::Kind::FLOATINGPOINT_FP},
172 {FLOATINGPOINT_EQ, CVC4::Kind::FLOATINGPOINT_EQ},
173 {FLOATINGPOINT_ABS, CVC4::Kind::FLOATINGPOINT_ABS},
174 {FLOATINGPOINT_NEG, CVC4::Kind::FLOATINGPOINT_NEG},
175 {FLOATINGPOINT_PLUS, CVC4::Kind::FLOATINGPOINT_PLUS},
176 {FLOATINGPOINT_SUB, CVC4::Kind::FLOATINGPOINT_SUB},
177 {FLOATINGPOINT_MULT, CVC4::Kind::FLOATINGPOINT_MULT},
178 {FLOATINGPOINT_DIV, CVC4::Kind::FLOATINGPOINT_DIV},
179 {FLOATINGPOINT_FMA, CVC4::Kind::FLOATINGPOINT_FMA},
180 {FLOATINGPOINT_SQRT, CVC4::Kind::FLOATINGPOINT_SQRT},
181 {FLOATINGPOINT_REM, CVC4::Kind::FLOATINGPOINT_REM},
182 {FLOATINGPOINT_RTI, CVC4::Kind::FLOATINGPOINT_RTI},
183 {FLOATINGPOINT_MIN, CVC4::Kind::FLOATINGPOINT_MIN},
184 {FLOATINGPOINT_MAX, CVC4::Kind::FLOATINGPOINT_MAX},
185 {FLOATINGPOINT_LEQ, CVC4::Kind::FLOATINGPOINT_LEQ},
186 {FLOATINGPOINT_LT, CVC4::Kind::FLOATINGPOINT_LT},
187 {FLOATINGPOINT_GEQ, CVC4::Kind::FLOATINGPOINT_GEQ},
188 {FLOATINGPOINT_GT, CVC4::Kind::FLOATINGPOINT_GT},
189 {FLOATINGPOINT_ISN, CVC4::Kind::FLOATINGPOINT_ISN},
190 {FLOATINGPOINT_ISSN, CVC4::Kind::FLOATINGPOINT_ISSN},
191 {FLOATINGPOINT_ISZ, CVC4::Kind::FLOATINGPOINT_ISZ},
192 {FLOATINGPOINT_ISINF, CVC4::Kind::FLOATINGPOINT_ISINF},
193 {FLOATINGPOINT_ISNAN, CVC4::Kind::FLOATINGPOINT_ISNAN},
194 {FLOATINGPOINT_ISNEG, CVC4::Kind::FLOATINGPOINT_ISNEG},
195 {FLOATINGPOINT_ISPOS, CVC4::Kind::FLOATINGPOINT_ISPOS},
196 {FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP,
197 CVC4::Kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP},
198 {FLOATINGPOINT_TO_FP_IEEE_BITVECTOR,
199 CVC4::Kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR},
200 {FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP,
201 CVC4::Kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP},
202 {FLOATINGPOINT_TO_FP_FLOATINGPOINT,
203 CVC4::Kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT},
204 {FLOATINGPOINT_TO_FP_REAL_OP, CVC4::Kind::FLOATINGPOINT_TO_FP_REAL_OP},
205 {FLOATINGPOINT_TO_FP_REAL, CVC4::Kind::FLOATINGPOINT_TO_FP_REAL},
206 {FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP,
207 CVC4::Kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP},
208 {FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR,
209 CVC4::Kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR},
210 {FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP,
211 CVC4::Kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP},
212 {FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR,
213 CVC4::Kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR},
214 {FLOATINGPOINT_TO_FP_GENERIC_OP,
215 CVC4::Kind::FLOATINGPOINT_TO_FP_GENERIC_OP},
216 {FLOATINGPOINT_TO_FP_GENERIC, CVC4::Kind::FLOATINGPOINT_TO_FP_GENERIC},
217 {FLOATINGPOINT_TO_UBV_OP, CVC4::Kind::FLOATINGPOINT_TO_UBV_OP},
218 {FLOATINGPOINT_TO_UBV, CVC4::Kind::FLOATINGPOINT_TO_UBV},
219 {FLOATINGPOINT_TO_UBV_TOTAL_OP, CVC4::Kind::FLOATINGPOINT_TO_UBV_TOTAL_OP},
220 {FLOATINGPOINT_TO_UBV_TOTAL, CVC4::Kind::FLOATINGPOINT_TO_UBV_TOTAL},
221 {FLOATINGPOINT_TO_SBV_OP, CVC4::Kind::FLOATINGPOINT_TO_SBV_OP},
222 {FLOATINGPOINT_TO_SBV, CVC4::Kind::FLOATINGPOINT_TO_SBV},
223 {FLOATINGPOINT_TO_SBV_TOTAL_OP, CVC4::Kind::FLOATINGPOINT_TO_SBV_TOTAL_OP},
224 {FLOATINGPOINT_TO_SBV_TOTAL, CVC4::Kind::FLOATINGPOINT_TO_SBV_TOTAL},
225 {FLOATINGPOINT_TO_REAL, CVC4::Kind::FLOATINGPOINT_TO_REAL},
226 {FLOATINGPOINT_TO_REAL_TOTAL, CVC4::Kind::FLOATINGPOINT_TO_REAL_TOTAL},
227 /* Arrays -------------------------------------------------------------- */
228 {SELECT, CVC4::Kind::SELECT},
229 {STORE, CVC4::Kind::STORE},
230 {STORE_ALL, CVC4::Kind::STORE_ALL},
231 /* Datatypes ----------------------------------------------------------- */
232 {APPLY_SELECTOR, CVC4::Kind::APPLY_SELECTOR},
233 {APPLY_CONSTRUCTOR, CVC4::Kind::APPLY_CONSTRUCTOR},
234 {APPLY_SELECTOR_TOTAL, CVC4::Kind::APPLY_SELECTOR_TOTAL},
235 {APPLY_TESTER, CVC4::Kind::APPLY_TESTER},
236 {TUPLE_UPDATE_OP, CVC4::Kind::TUPLE_UPDATE_OP},
237 {TUPLE_UPDATE, CVC4::Kind::TUPLE_UPDATE},
238 {RECORD_UPDATE_OP, CVC4::Kind::RECORD_UPDATE_OP},
239 {RECORD_UPDATE, CVC4::Kind::RECORD_UPDATE},
240 /* Separation Logic ---------------------------------------------------- */
241 {SEP_NIL, CVC4::Kind::SEP_NIL},
242 {SEP_EMP, CVC4::Kind::SEP_EMP},
243 {SEP_PTO, CVC4::Kind::SEP_PTO},
244 {SEP_STAR, CVC4::Kind::SEP_STAR},
245 {SEP_WAND, CVC4::Kind::SEP_WAND},
246 /* Sets ---------------------------------------------------------------- */
247 {EMPTYSET, CVC4::Kind::EMPTYSET},
248 {UNION, CVC4::Kind::UNION},
249 {INTERSECTION, CVC4::Kind::INTERSECTION},
250 {SETMINUS, CVC4::Kind::SETMINUS},
251 {SUBSET, CVC4::Kind::SUBSET},
252 {MEMBER, CVC4::Kind::MEMBER},
253 {SINGLETON, CVC4::Kind::SINGLETON},
254 {INSERT, CVC4::Kind::INSERT},
255 {CARD, CVC4::Kind::CARD},
256 {COMPLEMENT, CVC4::Kind::COMPLEMENT},
257 {UNIVERSE_SET, CVC4::Kind::UNIVERSE_SET},
258 {JOIN, CVC4::Kind::JOIN},
259 {PRODUCT, CVC4::Kind::PRODUCT},
260 {TRANSPOSE, CVC4::Kind::TRANSPOSE},
261 {TCLOSURE, CVC4::Kind::TCLOSURE},
262 {JOIN_IMAGE, CVC4::Kind::JOIN_IMAGE},
263 {IDEN, CVC4::Kind::IDEN},
264 /* Strings ------------------------------------------------------------- */
265 {STRING_CONCAT, CVC4::Kind::STRING_CONCAT},
266 {STRING_IN_REGEXP, CVC4::Kind::STRING_IN_REGEXP},
267 {STRING_LENGTH, CVC4::Kind::STRING_LENGTH},
268 {STRING_SUBSTR, CVC4::Kind::STRING_SUBSTR},
269 {STRING_CHARAT, CVC4::Kind::STRING_CHARAT},
270 {STRING_STRCTN, CVC4::Kind::STRING_STRCTN},
271 {STRING_STRIDOF, CVC4::Kind::STRING_STRIDOF},
272 {STRING_STRREPL, CVC4::Kind::STRING_STRREPL},
273 {STRING_PREFIX, CVC4::Kind::STRING_PREFIX},
274 {STRING_SUFFIX, CVC4::Kind::STRING_SUFFIX},
275 {STRING_ITOS, CVC4::Kind::STRING_ITOS},
276 {STRING_STOI, CVC4::Kind::STRING_STOI},
277 {CONST_STRING, CVC4::Kind::CONST_STRING},
278 {STRING_TO_REGEXP, CVC4::Kind::STRING_TO_REGEXP},
279 {REGEXP_CONCAT, CVC4::Kind::REGEXP_CONCAT},
280 {REGEXP_UNION, CVC4::Kind::REGEXP_UNION},
281 {REGEXP_INTER, CVC4::Kind::REGEXP_INTER},
282 {REGEXP_STAR, CVC4::Kind::REGEXP_STAR},
283 {REGEXP_PLUS, CVC4::Kind::REGEXP_PLUS},
284 {REGEXP_OPT, CVC4::Kind::REGEXP_OPT},
285 {REGEXP_RANGE, CVC4::Kind::REGEXP_RANGE},
286 {REGEXP_LOOP, CVC4::Kind::REGEXP_LOOP},
287 {REGEXP_EMPTY, CVC4::Kind::REGEXP_EMPTY},
288 {REGEXP_SIGMA, CVC4::Kind::REGEXP_SIGMA},
289 /* Quantifiers --------------------------------------------------------- */
290 {FORALL, CVC4::Kind::FORALL},
291 {EXISTS, CVC4::Kind::EXISTS},
292 {LAST_KIND, CVC4::Kind::LAST_KIND},
293 };
294
295 /* Mapping from internal kind to external (API) kind. */
296 const static std::unordered_map<CVC4::Kind, Kind, CVC4::kind::KindHashFunction>
297 s_kinds_internal{
298 {CVC4::Kind::UNDEFINED_KIND, UNDEFINED_KIND},
299 {CVC4::Kind::NULL_EXPR, NULL_EXPR},
300 /* Builtin --------------------------------------------------------- */
301 {CVC4::Kind::UNINTERPRETED_CONSTANT, UNINTERPRETED_CONSTANT},
302 {CVC4::Kind::ABSTRACT_VALUE, ABSTRACT_VALUE},
303 {CVC4::Kind::FUNCTION, FUNCTION},
304 {CVC4::Kind::APPLY, APPLY},
305 {CVC4::Kind::EQUAL, EQUAL},
306 {CVC4::Kind::DISTINCT, DISTINCT},
307 {CVC4::Kind::VARIABLE, VARIABLE},
308 {CVC4::Kind::BOUND_VARIABLE, BOUND_VARIABLE},
309 {CVC4::Kind::LAMBDA, LAMBDA},
310 {CVC4::Kind::CHOICE, CHOICE},
311 {CVC4::Kind::CHAIN, CHAIN},
312 {CVC4::Kind::CHAIN_OP, CHAIN_OP},
313 /* Boolean --------------------------------------------------------- */
314 {CVC4::Kind::CONST_BOOLEAN, CONST_BOOLEAN},
315 {CVC4::Kind::NOT, NOT},
316 {CVC4::Kind::AND, AND},
317 {CVC4::Kind::IMPLIES, IMPLIES},
318 {CVC4::Kind::OR, OR},
319 {CVC4::Kind::XOR, XOR},
320 {CVC4::Kind::ITE, ITE},
321 /* UF -------------------------------------------------------------- */
322 {CVC4::Kind::APPLY_UF, APPLY_UF},
323 {CVC4::Kind::CARDINALITY_CONSTRAINT, CARDINALITY_CONSTRAINT},
324 {CVC4::Kind::HO_APPLY, HO_APPLY},
325 /* Arithmetic ------------------------------------------------------ */
326 {CVC4::Kind::PLUS, PLUS},
327 {CVC4::Kind::MULT, MULT},
328 {CVC4::Kind::MINUS, MINUS},
329 {CVC4::Kind::UMINUS, UMINUS},
330 {CVC4::Kind::DIVISION, DIVISION},
331 {CVC4::Kind::DIVISION_TOTAL, DIVISION_TOTAL},
332 {CVC4::Kind::INTS_DIVISION, INTS_DIVISION},
333 {CVC4::Kind::INTS_DIVISION_TOTAL, INTS_DIVISION_TOTAL},
334 {CVC4::Kind::INTS_MODULUS, INTS_MODULUS},
335 {CVC4::Kind::INTS_MODULUS_TOTAL, INTS_MODULUS_TOTAL},
336 {CVC4::Kind::ABS, ABS},
337 {CVC4::Kind::DIVISIBLE, DIVISIBLE},
338 {CVC4::Kind::POW, POW},
339 {CVC4::Kind::EXPONENTIAL, EXPONENTIAL},
340 {CVC4::Kind::SINE, SINE},
341 {CVC4::Kind::COSINE, COSINE},
342 {CVC4::Kind::TANGENT, TANGENT},
343 {CVC4::Kind::COSECANT, COSECANT},
344 {CVC4::Kind::SECANT, SECANT},
345 {CVC4::Kind::COTANGENT, COTANGENT},
346 {CVC4::Kind::ARCSINE, ARCSINE},
347 {CVC4::Kind::ARCCOSINE, ARCCOSINE},
348 {CVC4::Kind::ARCTANGENT, ARCTANGENT},
349 {CVC4::Kind::ARCCOSECANT, ARCCOSECANT},
350 {CVC4::Kind::ARCSECANT, ARCSECANT},
351 {CVC4::Kind::ARCCOTANGENT, ARCCOTANGENT},
352 {CVC4::Kind::SQRT, SQRT},
353 {CVC4::Kind::DIVISIBLE_OP, DIVISIBLE_OP},
354 {CVC4::Kind::CONST_RATIONAL, CONST_RATIONAL},
355 {CVC4::Kind::LT, LT},
356 {CVC4::Kind::LEQ, LEQ},
357 {CVC4::Kind::GT, GT},
358 {CVC4::Kind::GEQ, GEQ},
359 {CVC4::Kind::IS_INTEGER, IS_INTEGER},
360 {CVC4::Kind::TO_INTEGER, TO_INTEGER},
361 {CVC4::Kind::TO_REAL, TO_REAL},
362 {CVC4::Kind::PI, PI},
363 /* BV -------------------------------------------------------------- */
364 {CVC4::Kind::CONST_BITVECTOR, CONST_BITVECTOR},
365 {CVC4::Kind::BITVECTOR_CONCAT, BITVECTOR_CONCAT},
366 {CVC4::Kind::BITVECTOR_AND, BITVECTOR_AND},
367 {CVC4::Kind::BITVECTOR_OR, BITVECTOR_OR},
368 {CVC4::Kind::BITVECTOR_XOR, BITVECTOR_XOR},
369 {CVC4::Kind::BITVECTOR_NOT, BITVECTOR_NOT},
370 {CVC4::Kind::BITVECTOR_NAND, BITVECTOR_NAND},
371 {CVC4::Kind::BITVECTOR_NOR, BITVECTOR_NOR},
372 {CVC4::Kind::BITVECTOR_XNOR, BITVECTOR_XNOR},
373 {CVC4::Kind::BITVECTOR_COMP, BITVECTOR_COMP},
374 {CVC4::Kind::BITVECTOR_MULT, BITVECTOR_MULT},
375 {CVC4::Kind::BITVECTOR_PLUS, BITVECTOR_PLUS},
376 {CVC4::Kind::BITVECTOR_SUB, BITVECTOR_SUB},
377 {CVC4::Kind::BITVECTOR_NEG, BITVECTOR_NEG},
378 {CVC4::Kind::BITVECTOR_UDIV, BITVECTOR_UDIV},
379 {CVC4::Kind::BITVECTOR_UREM, BITVECTOR_UREM},
380 {CVC4::Kind::BITVECTOR_SDIV, BITVECTOR_SDIV},
381 {CVC4::Kind::BITVECTOR_SREM, BITVECTOR_SREM},
382 {CVC4::Kind::BITVECTOR_SMOD, BITVECTOR_SMOD},
383 {CVC4::Kind::BITVECTOR_UDIV_TOTAL, BITVECTOR_UDIV_TOTAL},
384 {CVC4::Kind::BITVECTOR_UREM_TOTAL, BITVECTOR_UREM_TOTAL},
385 {CVC4::Kind::BITVECTOR_SHL, BITVECTOR_SHL},
386 {CVC4::Kind::BITVECTOR_LSHR, BITVECTOR_LSHR},
387 {CVC4::Kind::BITVECTOR_ASHR, BITVECTOR_ASHR},
388 {CVC4::Kind::BITVECTOR_ULT, BITVECTOR_ULT},
389 {CVC4::Kind::BITVECTOR_ULE, BITVECTOR_ULE},
390 {CVC4::Kind::BITVECTOR_UGT, BITVECTOR_UGT},
391 {CVC4::Kind::BITVECTOR_UGE, BITVECTOR_UGE},
392 {CVC4::Kind::BITVECTOR_SLT, BITVECTOR_SLT},
393 {CVC4::Kind::BITVECTOR_SLE, BITVECTOR_SLE},
394 {CVC4::Kind::BITVECTOR_SGT, BITVECTOR_SGT},
395 {CVC4::Kind::BITVECTOR_SGE, BITVECTOR_SGE},
396 {CVC4::Kind::BITVECTOR_ULTBV, BITVECTOR_ULTBV},
397 {CVC4::Kind::BITVECTOR_SLTBV, BITVECTOR_SLTBV},
398 {CVC4::Kind::BITVECTOR_ITE, BITVECTOR_ITE},
399 {CVC4::Kind::BITVECTOR_REDOR, BITVECTOR_REDOR},
400 {CVC4::Kind::BITVECTOR_REDAND, BITVECTOR_REDAND},
401 {CVC4::Kind::BITVECTOR_EXTRACT_OP, BITVECTOR_EXTRACT_OP},
402 {CVC4::Kind::BITVECTOR_REPEAT_OP, BITVECTOR_REPEAT_OP},
403 {CVC4::Kind::BITVECTOR_ZERO_EXTEND_OP, BITVECTOR_ZERO_EXTEND_OP},
404 {CVC4::Kind::BITVECTOR_SIGN_EXTEND_OP, BITVECTOR_SIGN_EXTEND_OP},
405 {CVC4::Kind::BITVECTOR_ROTATE_LEFT_OP, BITVECTOR_ROTATE_LEFT_OP},
406 {CVC4::Kind::BITVECTOR_ROTATE_RIGHT_OP, BITVECTOR_ROTATE_RIGHT_OP},
407 {CVC4::Kind::BITVECTOR_EXTRACT, BITVECTOR_EXTRACT},
408 {CVC4::Kind::BITVECTOR_REPEAT, BITVECTOR_REPEAT},
409 {CVC4::Kind::BITVECTOR_ZERO_EXTEND, BITVECTOR_ZERO_EXTEND},
410 {CVC4::Kind::BITVECTOR_SIGN_EXTEND, BITVECTOR_SIGN_EXTEND},
411 {CVC4::Kind::BITVECTOR_ROTATE_LEFT, BITVECTOR_ROTATE_LEFT},
412 {CVC4::Kind::BITVECTOR_ROTATE_RIGHT, BITVECTOR_ROTATE_RIGHT},
413 {CVC4::Kind::INT_TO_BITVECTOR_OP, INT_TO_BITVECTOR_OP},
414 {CVC4::Kind::INT_TO_BITVECTOR, INT_TO_BITVECTOR},
415 {CVC4::Kind::BITVECTOR_TO_NAT, BITVECTOR_TO_NAT},
416 /* FP -------------------------------------------------------------- */
417 {CVC4::Kind::CONST_FLOATINGPOINT, CONST_FLOATINGPOINT},
418 {CVC4::Kind::CONST_ROUNDINGMODE, CONST_ROUNDINGMODE},
419 {CVC4::Kind::FLOATINGPOINT_FP, FLOATINGPOINT_FP},
420 {CVC4::Kind::FLOATINGPOINT_EQ, FLOATINGPOINT_EQ},
421 {CVC4::Kind::FLOATINGPOINT_ABS, FLOATINGPOINT_ABS},
422 {CVC4::Kind::FLOATINGPOINT_NEG, FLOATINGPOINT_NEG},
423 {CVC4::Kind::FLOATINGPOINT_PLUS, FLOATINGPOINT_PLUS},
424 {CVC4::Kind::FLOATINGPOINT_SUB, FLOATINGPOINT_SUB},
425 {CVC4::Kind::FLOATINGPOINT_MULT, FLOATINGPOINT_MULT},
426 {CVC4::Kind::FLOATINGPOINT_DIV, FLOATINGPOINT_DIV},
427 {CVC4::Kind::FLOATINGPOINT_FMA, FLOATINGPOINT_FMA},
428 {CVC4::Kind::FLOATINGPOINT_SQRT, FLOATINGPOINT_SQRT},
429 {CVC4::Kind::FLOATINGPOINT_REM, FLOATINGPOINT_REM},
430 {CVC4::Kind::FLOATINGPOINT_RTI, FLOATINGPOINT_RTI},
431 {CVC4::Kind::FLOATINGPOINT_MIN, FLOATINGPOINT_MIN},
432 {CVC4::Kind::FLOATINGPOINT_MAX, FLOATINGPOINT_MAX},
433 {CVC4::Kind::FLOATINGPOINT_LEQ, FLOATINGPOINT_LEQ},
434 {CVC4::Kind::FLOATINGPOINT_LT, FLOATINGPOINT_LT},
435 {CVC4::Kind::FLOATINGPOINT_GEQ, FLOATINGPOINT_GEQ},
436 {CVC4::Kind::FLOATINGPOINT_GT, FLOATINGPOINT_GT},
437 {CVC4::Kind::FLOATINGPOINT_ISN, FLOATINGPOINT_ISN},
438 {CVC4::Kind::FLOATINGPOINT_ISSN, FLOATINGPOINT_ISSN},
439 {CVC4::Kind::FLOATINGPOINT_ISZ, FLOATINGPOINT_ISZ},
440 {CVC4::Kind::FLOATINGPOINT_ISINF, FLOATINGPOINT_ISINF},
441 {CVC4::Kind::FLOATINGPOINT_ISNAN, FLOATINGPOINT_ISNAN},
442 {CVC4::Kind::FLOATINGPOINT_ISNEG, FLOATINGPOINT_ISNEG},
443 {CVC4::Kind::FLOATINGPOINT_ISPOS, FLOATINGPOINT_ISPOS},
444 {CVC4::Kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP,
445 FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP},
446 {CVC4::Kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR,
447 FLOATINGPOINT_TO_FP_IEEE_BITVECTOR},
448 {CVC4::Kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP,
449 FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP},
450 {CVC4::Kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT,
451 FLOATINGPOINT_TO_FP_FLOATINGPOINT},
452 {CVC4::Kind::FLOATINGPOINT_TO_FP_REAL_OP, FLOATINGPOINT_TO_FP_REAL_OP},
453 {CVC4::Kind::FLOATINGPOINT_TO_FP_REAL, FLOATINGPOINT_TO_FP_REAL},
454 {CVC4::Kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP,
455 FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP},
456 {CVC4::Kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR,
457 FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR},
458 {CVC4::Kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP,
459 FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP},
460 {CVC4::Kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR,
461 FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR},
462 {CVC4::Kind::FLOATINGPOINT_TO_FP_GENERIC_OP,
463 FLOATINGPOINT_TO_FP_GENERIC_OP},
464 {CVC4::Kind::FLOATINGPOINT_TO_FP_GENERIC, FLOATINGPOINT_TO_FP_GENERIC},
465 {CVC4::Kind::FLOATINGPOINT_TO_UBV_OP, FLOATINGPOINT_TO_UBV_OP},
466 {CVC4::Kind::FLOATINGPOINT_TO_UBV, FLOATINGPOINT_TO_UBV},
467 {CVC4::Kind::FLOATINGPOINT_TO_UBV_TOTAL_OP,
468 FLOATINGPOINT_TO_UBV_TOTAL_OP},
469 {CVC4::Kind::FLOATINGPOINT_TO_UBV_TOTAL, FLOATINGPOINT_TO_UBV_TOTAL},
470 {CVC4::Kind::FLOATINGPOINT_TO_SBV_OP, FLOATINGPOINT_TO_SBV_OP},
471 {CVC4::Kind::FLOATINGPOINT_TO_SBV, FLOATINGPOINT_TO_SBV},
472 {CVC4::Kind::FLOATINGPOINT_TO_SBV_TOTAL_OP,
473 FLOATINGPOINT_TO_SBV_TOTAL_OP},
474 {CVC4::Kind::FLOATINGPOINT_TO_SBV_TOTAL, FLOATINGPOINT_TO_SBV_TOTAL},
475 {CVC4::Kind::FLOATINGPOINT_TO_REAL, FLOATINGPOINT_TO_REAL},
476 {CVC4::Kind::FLOATINGPOINT_TO_REAL_TOTAL, FLOATINGPOINT_TO_REAL_TOTAL},
477 /* Arrays ---------------------------------------------------------- */
478 {CVC4::Kind::SELECT, SELECT},
479 {CVC4::Kind::STORE, STORE},
480 {CVC4::Kind::STORE_ALL, STORE_ALL},
481 /* Datatypes ------------------------------------------------------- */
482 {CVC4::Kind::APPLY_SELECTOR, APPLY_SELECTOR},
483 {CVC4::Kind::APPLY_CONSTRUCTOR, APPLY_CONSTRUCTOR},
484 {CVC4::Kind::APPLY_SELECTOR_TOTAL, APPLY_SELECTOR_TOTAL},
485 {CVC4::Kind::APPLY_TESTER, APPLY_TESTER},
486 {CVC4::Kind::TUPLE_UPDATE_OP, TUPLE_UPDATE_OP},
487 {CVC4::Kind::TUPLE_UPDATE, TUPLE_UPDATE},
488 {CVC4::Kind::RECORD_UPDATE_OP, RECORD_UPDATE_OP},
489 {CVC4::Kind::RECORD_UPDATE, RECORD_UPDATE},
490 /* Separation Logic ------------------------------------------------ */
491 {CVC4::Kind::SEP_NIL, SEP_NIL},
492 {CVC4::Kind::SEP_EMP, SEP_EMP},
493 {CVC4::Kind::SEP_PTO, SEP_PTO},
494 {CVC4::Kind::SEP_STAR, SEP_STAR},
495 {CVC4::Kind::SEP_WAND, SEP_WAND},
496 /* Sets ------------------------------------------------------------ */
497 {CVC4::Kind::EMPTYSET, EMPTYSET},
498 {CVC4::Kind::UNION, UNION},
499 {CVC4::Kind::INTERSECTION, INTERSECTION},
500 {CVC4::Kind::SETMINUS, SETMINUS},
501 {CVC4::Kind::SUBSET, SUBSET},
502 {CVC4::Kind::MEMBER, MEMBER},
503 {CVC4::Kind::SINGLETON, SINGLETON},
504 {CVC4::Kind::INSERT, INSERT},
505 {CVC4::Kind::CARD, CARD},
506 {CVC4::Kind::COMPLEMENT, COMPLEMENT},
507 {CVC4::Kind::UNIVERSE_SET, UNIVERSE_SET},
508 {CVC4::Kind::JOIN, JOIN},
509 {CVC4::Kind::PRODUCT, PRODUCT},
510 {CVC4::Kind::TRANSPOSE, TRANSPOSE},
511 {CVC4::Kind::TCLOSURE, TCLOSURE},
512 {CVC4::Kind::JOIN_IMAGE, JOIN_IMAGE},
513 {CVC4::Kind::IDEN, IDEN},
514 /* Strings --------------------------------------------------------- */
515 {CVC4::Kind::STRING_CONCAT, STRING_CONCAT},
516 {CVC4::Kind::STRING_IN_REGEXP, STRING_IN_REGEXP},
517 {CVC4::Kind::STRING_LENGTH, STRING_LENGTH},
518 {CVC4::Kind::STRING_SUBSTR, STRING_SUBSTR},
519 {CVC4::Kind::STRING_CHARAT, STRING_CHARAT},
520 {CVC4::Kind::STRING_STRCTN, STRING_STRCTN},
521 {CVC4::Kind::STRING_STRIDOF, STRING_STRIDOF},
522 {CVC4::Kind::STRING_STRREPL, STRING_STRREPL},
523 {CVC4::Kind::STRING_PREFIX, STRING_PREFIX},
524 {CVC4::Kind::STRING_SUFFIX, STRING_SUFFIX},
525 {CVC4::Kind::STRING_ITOS, STRING_ITOS},
526 {CVC4::Kind::STRING_STOI, STRING_STOI},
527 {CVC4::Kind::CONST_STRING, CONST_STRING},
528 {CVC4::Kind::STRING_TO_REGEXP, STRING_TO_REGEXP},
529 {CVC4::Kind::REGEXP_CONCAT, REGEXP_CONCAT},
530 {CVC4::Kind::REGEXP_UNION, REGEXP_UNION},
531 {CVC4::Kind::REGEXP_INTER, REGEXP_INTER},
532 {CVC4::Kind::REGEXP_STAR, REGEXP_STAR},
533 {CVC4::Kind::REGEXP_PLUS, REGEXP_PLUS},
534 {CVC4::Kind::REGEXP_OPT, REGEXP_OPT},
535 {CVC4::Kind::REGEXP_RANGE, REGEXP_RANGE},
536 {CVC4::Kind::REGEXP_LOOP, REGEXP_LOOP},
537 {CVC4::Kind::REGEXP_EMPTY, REGEXP_EMPTY},
538 {CVC4::Kind::REGEXP_SIGMA, REGEXP_SIGMA},
539 /* Quantifiers ----------------------------------------------------- */
540 {CVC4::Kind::FORALL, FORALL},
541 {CVC4::Kind::EXISTS, EXISTS},
542 /* ----------------------------------------------------------------- */
543 {CVC4::Kind::LAST_KIND, LAST_KIND},
544 };
545
546 namespace {
547
isDefinedKind(Kind k)548 bool isDefinedKind(Kind k) { return k > UNDEFINED_KIND && k < LAST_KIND; }
549
550 #ifdef CVC4_ASSERTIONS
isDefinedIntKind(CVC4::Kind k)551 bool isDefinedIntKind(CVC4::Kind k)
552 {
553 return k != CVC4::Kind::UNDEFINED_KIND && k != CVC4::Kind::LAST_KIND;
554 }
555 #endif
556
intToExtKind(CVC4::Kind k)557 Kind intToExtKind(CVC4::Kind k)
558 {
559 auto it = s_kinds_internal.find(k);
560 if (it == s_kinds_internal.end())
561 {
562 return INTERNAL_KIND;
563 }
564 return it->second;
565 }
566
extToIntKind(Kind k)567 CVC4::Kind extToIntKind(Kind k)
568 {
569 auto it = s_kinds.find(k);
570 if (it == s_kinds.end())
571 {
572 return CVC4::Kind::UNDEFINED_KIND;
573 }
574 return it->second;
575 }
576
minArity(Kind k)577 uint32_t minArity(Kind k)
578 {
579 Assert(isDefinedKind(k));
580 Assert(isDefinedIntKind(extToIntKind(k)));
581 return CVC4::ExprManager::minArity(extToIntKind(k));
582 }
583
maxArity(Kind k)584 uint32_t maxArity(Kind k)
585 {
586 Assert(isDefinedKind(k));
587 Assert(isDefinedIntKind(extToIntKind(k)));
588 return CVC4::ExprManager::maxArity(extToIntKind(k));
589 }
590 } // namespace
591
kindToString(Kind k)592 std::string kindToString(Kind k)
593 {
594 return k == INTERNAL_KIND ? "INTERNAL_KIND"
595 : CVC4::kind::kindToString(extToIntKind(k));
596 }
597
operator <<(std::ostream & out,Kind k)598 std::ostream& operator<<(std::ostream& out, Kind k)
599 {
600 switch (k)
601 {
602 case INTERNAL_KIND: out << "INTERNAL_KIND"; break;
603 default: out << extToIntKind(k);
604 }
605 return out;
606 }
607
operator ()(Kind k) const608 size_t KindHashFunction::operator()(Kind k) const { return k; }
609
610 /* -------------------------------------------------------------------------- */
611 /* API guard helpers */
612 /* -------------------------------------------------------------------------- */
613
614 namespace {
615
616 class CVC4ApiExceptionStream
617 {
618 public:
CVC4ApiExceptionStream()619 CVC4ApiExceptionStream() {}
620 /* Note: This needs to be explicitly set to 'noexcept(false)' since it is
621 * a destructor that throws an exception and in C++11 all destructors
622 * default to noexcept(true) (else this triggers a call to std::terminate). */
~CVC4ApiExceptionStream()623 ~CVC4ApiExceptionStream() noexcept(false)
624 {
625 if (!std::uncaught_exception())
626 {
627 throw CVC4ApiException(d_stream.str());
628 }
629 }
630
ostream()631 std::ostream& ostream() { return d_stream; }
632
633 private:
634 std::stringstream d_stream;
635 };
636
637 #define CVC4_API_CHECK(cond) \
638 CVC4_PREDICT_FALSE(cond) \
639 ? (void)0 : OstreamVoider() & CVC4ApiExceptionStream().ostream()
640
641 #define CVC4_API_CHECK_NOT_NULL \
642 CVC4_API_CHECK(!isNull()) << "Invalid call to '" << __PRETTY_FUNCTION__ \
643 << "', expected non-null object";
644
645 #define CVC4_API_ARG_CHECK_NOT_NULL(arg) \
646 CVC4_API_CHECK(arg != nullptr) \
647 << "Invalid null argument for '" << #arg << "'";
648
649 #define CVC4_API_KIND_CHECK(kind) \
650 CVC4_API_CHECK(isDefinedKind(kind)) \
651 << "Invalid kind '" << kindToString(kind) << "'";
652
653 #define CVC4_API_KIND_CHECK_EXPECTED(cond, kind) \
654 CVC4_PREDICT_FALSE(cond) \
655 ? (void)0 \
656 : OstreamVoider() \
657 & CVC4ApiExceptionStream().ostream() \
658 << "Invalid kind '" << kindToString(kind) << "', expected "
659
660 #define CVC4_API_ARG_CHECK_EXPECTED(cond, arg) \
661 CVC4_PREDICT_FALSE(cond) \
662 ? (void)0 \
663 : OstreamVoider() \
664 & CVC4ApiExceptionStream().ostream() \
665 << "Invalid argument '" << arg << "' for '" << #arg \
666 << "', expected "
667
668 #define CVC4_API_ARG_SIZE_CHECK_EXPECTED(cond, arg) \
669 CVC4_PREDICT_FALSE(cond) \
670 ? (void)0 \
671 : OstreamVoider() \
672 & CVC4ApiExceptionStream().ostream() \
673 << "Invalid size of argument '" << #arg << "', expected "
674
675 #define CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(cond, what, arg, idx) \
676 CVC4_PREDICT_FALSE(cond) \
677 ? (void)0 \
678 : OstreamVoider() \
679 & CVC4ApiExceptionStream().ostream() \
680 << "Invalid " << what << " '" << arg << "' at index" << idx \
681 << ", expected "
682 } // namespace
683
684 /* -------------------------------------------------------------------------- */
685 /* Result */
686 /* -------------------------------------------------------------------------- */
687
Result(const CVC4::Result & r)688 Result::Result(const CVC4::Result& r) : d_result(new CVC4::Result(r)) {}
689
isSat(void) const690 bool Result::isSat(void) const
691 {
692 return d_result->getType() == CVC4::Result::TYPE_SAT
693 && d_result->isSat() == CVC4::Result::SAT;
694 }
695
isUnsat(void) const696 bool Result::isUnsat(void) const
697 {
698 return d_result->getType() == CVC4::Result::TYPE_SAT
699 && d_result->isSat() == CVC4::Result::UNSAT;
700 }
701
isSatUnknown(void) const702 bool Result::isSatUnknown(void) const
703 {
704 return d_result->getType() == CVC4::Result::TYPE_SAT
705 && d_result->isSat() == CVC4::Result::SAT_UNKNOWN;
706 }
707
isValid(void) const708 bool Result::isValid(void) const
709 {
710 return d_result->getType() == CVC4::Result::TYPE_VALIDITY
711 && d_result->isValid() == CVC4::Result::VALID;
712 }
713
isInvalid(void) const714 bool Result::isInvalid(void) const
715 {
716 return d_result->getType() == CVC4::Result::TYPE_VALIDITY
717 && d_result->isValid() == CVC4::Result::INVALID;
718 }
719
isValidUnknown(void) const720 bool Result::isValidUnknown(void) const
721 {
722 return d_result->getType() == CVC4::Result::TYPE_VALIDITY
723 && d_result->isValid() == CVC4::Result::VALIDITY_UNKNOWN;
724 }
725
operator ==(const Result & r) const726 bool Result::operator==(const Result& r) const
727 {
728 return *d_result == *r.d_result;
729 }
730
operator !=(const Result & r) const731 bool Result::operator!=(const Result& r) const
732 {
733 return *d_result != *r.d_result;
734 }
735
getUnknownExplanation(void) const736 std::string Result::getUnknownExplanation(void) const
737 {
738 std::stringstream ss;
739 ss << d_result->whyUnknown();
740 return ss.str();
741 }
742
toString(void) const743 std::string Result::toString(void) const { return d_result->toString(); }
744
745 // !!! This is only temporarily available until the parser is fully migrated
746 // to the new API. !!!
getResult(void) const747 CVC4::Result Result::getResult(void) const { return *d_result; }
748
operator <<(std::ostream & out,const Result & r)749 std::ostream& operator<<(std::ostream& out, const Result& r)
750 {
751 out << r.toString();
752 return out;
753 }
754
755 /* -------------------------------------------------------------------------- */
756 /* Sort */
757 /* -------------------------------------------------------------------------- */
758
Sort(const CVC4::Type & t)759 Sort::Sort(const CVC4::Type& t) : d_type(new CVC4::Type(t)) {}
760
Sort()761 Sort::Sort() : d_type(new CVC4::Type()) {}
762
~Sort()763 Sort::~Sort() {}
764
operator ==(const Sort & s) const765 bool Sort::operator==(const Sort& s) const { return *d_type == *s.d_type; }
766
operator !=(const Sort & s) const767 bool Sort::operator!=(const Sort& s) const { return *d_type != *s.d_type; }
768
isNull() const769 bool Sort::isNull() const { return d_type->isNull(); }
770
isBoolean() const771 bool Sort::isBoolean() const { return d_type->isBoolean(); }
772
isInteger() const773 bool Sort::isInteger() const { return d_type->isInteger(); }
774
isReal() const775 bool Sort::isReal() const { return d_type->isReal(); }
776
isString() const777 bool Sort::isString() const { return d_type->isString(); }
778
isRegExp() const779 bool Sort::isRegExp() const { return d_type->isRegExp(); }
780
isRoundingMode() const781 bool Sort::isRoundingMode() const { return d_type->isRoundingMode(); }
782
isBitVector() const783 bool Sort::isBitVector() const { return d_type->isBitVector(); }
784
isFloatingPoint() const785 bool Sort::isFloatingPoint() const { return d_type->isFloatingPoint(); }
786
isDatatype() const787 bool Sort::isDatatype() const { return d_type->isDatatype(); }
788
isParametricDatatype() const789 bool Sort::isParametricDatatype() const
790 {
791 if (!d_type->isDatatype()) return false;
792 DatatypeType* type = static_cast<DatatypeType*>(d_type.get());
793 return type->isParametric();
794 }
795
isFunction() const796 bool Sort::isFunction() const { return d_type->isFunction(); }
797
isPredicate() const798 bool Sort::isPredicate() const { return d_type->isPredicate(); }
799
isTuple() const800 bool Sort::isTuple() const { return d_type->isTuple(); }
801
isRecord() const802 bool Sort::isRecord() const { return d_type->isRecord(); }
803
isArray() const804 bool Sort::isArray() const { return d_type->isArray(); }
805
isSet() const806 bool Sort::isSet() const { return d_type->isSet(); }
807
isUninterpretedSort() const808 bool Sort::isUninterpretedSort() const { return d_type->isSort(); }
809
isSortConstructor() const810 bool Sort::isSortConstructor() const { return d_type->isSortConstructor(); }
811
isFirstClass() const812 bool Sort::isFirstClass() const { return d_type->isFirstClass(); }
813
isFunctionLike() const814 bool Sort::isFunctionLike() const { return d_type->isFunctionLike(); }
815
getDatatype() const816 Datatype Sort::getDatatype() const
817 {
818 CVC4_API_CHECK(isDatatype()) << "Expected datatype sort.";
819 DatatypeType* type = static_cast<DatatypeType*>(d_type.get());
820 return type->getDatatype();
821 }
822
instantiate(const std::vector<Sort> & params) const823 Sort Sort::instantiate(const std::vector<Sort>& params) const
824 {
825 CVC4_API_CHECK(isParametricDatatype() || isSortConstructor())
826 << "Expected parametric datatype or sort constructor sort.";
827 std::vector<Type> tparams;
828 for (const Sort& s : params)
829 {
830 tparams.push_back(*s.d_type.get());
831 }
832 if (d_type->isDatatype())
833 {
834 DatatypeType* type = static_cast<DatatypeType*>(d_type.get());
835 return type->instantiate(tparams);
836 }
837 Assert(d_type->isSortConstructor());
838 return static_cast<SortConstructorType*>(d_type.get())->instantiate(tparams);
839 }
840
toString() const841 std::string Sort::toString() const { return d_type->toString(); }
842
843 // !!! This is only temporarily available until the parser is fully migrated
844 // to the new API. !!!
getType(void) const845 CVC4::Type Sort::getType(void) const { return *d_type; }
846
847 /* Function sort ------------------------------------------------------- */
848
getFunctionArity() const849 size_t Sort::getFunctionArity() const
850 {
851 CVC4_API_CHECK(isFunction()) << "Not a function sort.";
852 return static_cast<FunctionType*>(d_type.get())->getArity();
853 }
854
getFunctionDomainSorts() const855 std::vector<Sort> Sort::getFunctionDomainSorts() const
856 {
857 CVC4_API_CHECK(isFunction()) << "Not a function sort.";
858 std::vector<CVC4::Type> types =
859 static_cast<FunctionType*>(d_type.get())->getArgTypes();
860 return typeVectorToSorts(types);
861 }
862
getFunctionCodomainSort() const863 Sort Sort::getFunctionCodomainSort() const
864 {
865 CVC4_API_CHECK(isFunction()) << "Not a function sort.";
866 return static_cast<FunctionType*>(d_type.get())->getRangeType();
867 }
868
869 /* Array sort ---------------------------------------------------------- */
870
getArrayIndexSort() const871 Sort Sort::getArrayIndexSort() const
872 {
873 CVC4_API_CHECK(isArray()) << "Not an array sort.";
874 return static_cast<ArrayType*>(d_type.get())->getIndexType();
875 }
876
getArrayElementSort() const877 Sort Sort::getArrayElementSort() const
878 {
879 CVC4_API_CHECK(isArray()) << "Not an array sort.";
880 return static_cast<ArrayType*>(d_type.get())->getConstituentType();
881 }
882
883 /* Set sort ------------------------------------------------------------ */
884
getSetElementSort() const885 Sort Sort::getSetElementSort() const
886 {
887 CVC4_API_CHECK(isSet()) << "Not a set sort.";
888 return static_cast<SetType*>(d_type.get())->getElementType();
889 }
890
891 /* Uninterpreted sort -------------------------------------------------- */
892
getUninterpretedSortName() const893 std::string Sort::getUninterpretedSortName() const
894 {
895 CVC4_API_CHECK(isUninterpretedSort()) << "Not an uninterpreted sort.";
896 return static_cast<SortType*>(d_type.get())->getName();
897 }
898
isUninterpretedSortParameterized() const899 bool Sort::isUninterpretedSortParameterized() const
900 {
901 CVC4_API_CHECK(isUninterpretedSort()) << "Not an uninterpreted sort.";
902 return static_cast<SortType*>(d_type.get())->isParameterized();
903 }
904
getUninterpretedSortParamSorts() const905 std::vector<Sort> Sort::getUninterpretedSortParamSorts() const
906 {
907 CVC4_API_CHECK(isUninterpretedSort()) << "Not an uninterpreted sort.";
908 std::vector<CVC4::Type> types =
909 static_cast<SortType*>(d_type.get())->getParamTypes();
910 return typeVectorToSorts(types);
911 }
912
913 /* Sort constructor sort ----------------------------------------------- */
914
getSortConstructorName() const915 std::string Sort::getSortConstructorName() const
916 {
917 CVC4_API_CHECK(isSortConstructor()) << "Not a sort constructor sort.";
918 return static_cast<SortConstructorType*>(d_type.get())->getName();
919 }
920
getSortConstructorArity() const921 size_t Sort::getSortConstructorArity() const
922 {
923 CVC4_API_CHECK(isSortConstructor()) << "Not a sort constructor sort.";
924 return static_cast<SortConstructorType*>(d_type.get())->getArity();
925 }
926
927 /* Bit-vector sort ----------------------------------------------------- */
928
getBVSize() const929 uint32_t Sort::getBVSize() const
930 {
931 CVC4_API_CHECK(isBitVector()) << "Not a bit-vector sort.";
932 return static_cast<BitVectorType*>(d_type.get())->getSize();
933 }
934
935 /* Floating-point sort ------------------------------------------------- */
936
getFPExponentSize() const937 uint32_t Sort::getFPExponentSize() const
938 {
939 CVC4_API_CHECK(isFloatingPoint()) << "Not a floating-point sort.";
940 return static_cast<FloatingPointType*>(d_type.get())->getExponentSize();
941 }
942
getFPSignificandSize() const943 uint32_t Sort::getFPSignificandSize() const
944 {
945 CVC4_API_CHECK(isFloatingPoint()) << "Not a floating-point sort.";
946 return static_cast<FloatingPointType*>(d_type.get())->getSignificandSize();
947 }
948
949 /* Datatype sort ------------------------------------------------------- */
950
getDatatypeParamSorts() const951 std::vector<Sort> Sort::getDatatypeParamSorts() const
952 {
953 CVC4_API_CHECK(isParametricDatatype()) << "Not a parametric datatype sort.";
954 std::vector<CVC4::Type> types =
955 static_cast<DatatypeType*>(d_type.get())->getParamTypes();
956 return typeVectorToSorts(types);
957 }
958
getDatatypeArity() const959 size_t Sort::getDatatypeArity() const
960 {
961 CVC4_API_CHECK(isDatatype()) << "Not a datatype sort.";
962 return static_cast<DatatypeType*>(d_type.get())->getArity();
963 }
964
965 /* Tuple sort ---------------------------------------------------------- */
966
getTupleLength() const967 size_t Sort::getTupleLength() const
968 {
969 CVC4_API_CHECK(isTuple()) << "Not a tuple sort.";
970 return static_cast<DatatypeType*>(d_type.get())->getTupleLength();
971 }
972
getTupleSorts() const973 std::vector<Sort> Sort::getTupleSorts() const
974 {
975 CVC4_API_CHECK(isTuple()) << "Not a tuple sort.";
976 std::vector<CVC4::Type> types =
977 static_cast<DatatypeType*>(d_type.get())->getTupleTypes();
978 return typeVectorToSorts(types);
979 }
980
981 /* --------------------------------------------------------------------- */
982
typeVectorToSorts(const std::vector<CVC4::Type> & types) const983 std::vector<Sort> Sort::typeVectorToSorts(
984 const std::vector<CVC4::Type>& types) const
985 {
986 std::vector<Sort> res;
987 for (const CVC4::Type& t : types)
988 {
989 res.push_back(Sort(t));
990 }
991 return res;
992 }
993
994 /* --------------------------------------------------------------------- */
995
operator <<(std::ostream & out,const Sort & s)996 std::ostream& operator<<(std::ostream& out, const Sort& s)
997 {
998 out << s.toString();
999 return out;
1000 }
1001
operator ()(const Sort & s) const1002 size_t SortHashFunction::operator()(const Sort& s) const
1003 {
1004 return TypeHashFunction()(*s.d_type);
1005 }
1006
1007 /* -------------------------------------------------------------------------- */
1008 /* Term */
1009 /* -------------------------------------------------------------------------- */
1010
Term()1011 Term::Term() : d_expr(new CVC4::Expr()) {}
1012
Term(const CVC4::Expr & e)1013 Term::Term(const CVC4::Expr& e) : d_expr(new CVC4::Expr(e)) {}
1014
~Term()1015 Term::~Term() {}
1016
operator ==(const Term & t) const1017 bool Term::operator==(const Term& t) const { return *d_expr == *t.d_expr; }
1018
operator !=(const Term & t) const1019 bool Term::operator!=(const Term& t) const { return *d_expr != *t.d_expr; }
1020
getKind() const1021 Kind Term::getKind() const
1022 {
1023 CVC4_API_CHECK_NOT_NULL;
1024 return intToExtKind(d_expr->getKind());
1025 }
1026
getSort() const1027 Sort Term::getSort() const
1028 {
1029 CVC4_API_CHECK_NOT_NULL;
1030 return Sort(d_expr->getType());
1031 }
1032
isNull() const1033 bool Term::isNull() const { return d_expr->isNull(); }
1034
notTerm() const1035 Term Term::notTerm() const
1036 {
1037 try
1038 {
1039 Term res = d_expr->notExpr();
1040 (void)res.d_expr->getType(true); /* kick off type checking */
1041 return res;
1042 }
1043 catch (const CVC4::TypeCheckingException& e)
1044 {
1045 throw CVC4ApiException(e.getMessage());
1046 }
1047 }
1048
andTerm(const Term & t) const1049 Term Term::andTerm(const Term& t) const
1050 {
1051 try
1052 {
1053 Term res = d_expr->andExpr(*t.d_expr);
1054 (void)res.d_expr->getType(true); /* kick off type checking */
1055 return res;
1056 }
1057 catch (const CVC4::TypeCheckingException& e)
1058 {
1059 throw CVC4ApiException(e.getMessage());
1060 }
1061 }
1062
orTerm(const Term & t) const1063 Term Term::orTerm(const Term& t) const
1064 {
1065 try
1066 {
1067 Term res = d_expr->orExpr(*t.d_expr);
1068 (void)res.d_expr->getType(true); /* kick off type checking */
1069 return res;
1070 }
1071 catch (const CVC4::TypeCheckingException& e)
1072 {
1073 throw CVC4ApiException(e.getMessage());
1074 }
1075 }
1076
xorTerm(const Term & t) const1077 Term Term::xorTerm(const Term& t) const
1078 {
1079 try
1080 {
1081 Term res = d_expr->xorExpr(*t.d_expr);
1082 (void)res.d_expr->getType(true); /* kick off type checking */
1083 return res;
1084 }
1085 catch (const CVC4::TypeCheckingException& e)
1086 {
1087 throw CVC4ApiException(e.getMessage());
1088 }
1089 }
1090
eqTerm(const Term & t) const1091 Term Term::eqTerm(const Term& t) const
1092 {
1093 try
1094 {
1095 Term res = d_expr->eqExpr(*t.d_expr);
1096 (void)res.d_expr->getType(true); /* kick off type checking */
1097 return res;
1098 }
1099 catch (const CVC4::TypeCheckingException& e)
1100 {
1101 throw CVC4ApiException(e.getMessage());
1102 }
1103 }
1104
impTerm(const Term & t) const1105 Term Term::impTerm(const Term& t) const
1106 {
1107 try
1108 {
1109 Term res = d_expr->impExpr(*t.d_expr);
1110 (void)res.d_expr->getType(true); /* kick off type checking */
1111 return res;
1112 }
1113 catch (const CVC4::TypeCheckingException& e)
1114 {
1115 throw CVC4ApiException(e.getMessage());
1116 }
1117 }
1118
iteTerm(const Term & then_t,const Term & else_t) const1119 Term Term::iteTerm(const Term& then_t, const Term& else_t) const
1120 {
1121 try
1122 {
1123 Term res = d_expr->iteExpr(*then_t.d_expr, *else_t.d_expr);
1124 (void)res.d_expr->getType(true); /* kick off type checking */
1125 return res;
1126 }
1127 catch (const CVC4::TypeCheckingException& e)
1128 {
1129 throw CVC4ApiException(e.getMessage());
1130 }
1131 }
1132
toString() const1133 std::string Term::toString() const { return d_expr->toString(); }
1134
const_iterator()1135 Term::const_iterator::const_iterator() : d_iterator(nullptr) {}
1136
const_iterator(void * it)1137 Term::const_iterator::const_iterator(void* it) : d_iterator(it) {}
1138
const_iterator(const const_iterator & it)1139 Term::const_iterator::const_iterator(const const_iterator& it)
1140 : d_iterator(nullptr)
1141 {
1142 if (it.d_iterator != nullptr)
1143 {
1144 d_iterator = new CVC4::Expr::const_iterator(
1145 *static_cast<CVC4::Expr::const_iterator*>(it.d_iterator));
1146 }
1147 }
1148
operator =(const const_iterator & it)1149 Term::const_iterator& Term::const_iterator::operator=(const const_iterator& it)
1150 {
1151 delete static_cast<CVC4::Expr::const_iterator*>(d_iterator);
1152 d_iterator = new CVC4::Expr::const_iterator(
1153 *static_cast<CVC4::Expr::const_iterator*>(it.d_iterator));
1154 return *this;
1155 }
1156
~const_iterator()1157 Term::const_iterator::~const_iterator()
1158 {
1159 delete static_cast<CVC4::Expr::const_iterator*>(d_iterator);
1160 }
1161
operator ==(const const_iterator & it) const1162 bool Term::const_iterator::operator==(const const_iterator& it) const
1163 {
1164 if (d_iterator == nullptr || it.d_iterator == nullptr)
1165 {
1166 return false;
1167 }
1168 return *static_cast<CVC4::Expr::const_iterator*>(d_iterator)
1169 == *static_cast<CVC4::Expr::const_iterator*>(it.d_iterator);
1170 }
1171
operator !=(const const_iterator & it) const1172 bool Term::const_iterator::operator!=(const const_iterator& it) const
1173 {
1174 return !(*this == it);
1175 }
1176
operator ++()1177 Term::const_iterator& Term::const_iterator::operator++()
1178 {
1179 Assert(d_iterator != nullptr);
1180 ++*static_cast<CVC4::Expr::const_iterator*>(d_iterator);
1181 return *this;
1182 }
1183
operator ++(int)1184 Term::const_iterator Term::const_iterator::operator++(int)
1185 {
1186 Assert(d_iterator != nullptr);
1187 const_iterator it = *this;
1188 ++*static_cast<CVC4::Expr::const_iterator*>(d_iterator);
1189 return it;
1190 }
1191
operator *() const1192 Term Term::const_iterator::operator*() const
1193 {
1194 Assert(d_iterator != nullptr);
1195 return Term(**static_cast<CVC4::Expr::const_iterator*>(d_iterator));
1196 }
1197
begin() const1198 Term::const_iterator Term::begin() const
1199 {
1200 return Term::const_iterator(new CVC4::Expr::const_iterator(d_expr->begin()));
1201 }
1202
end() const1203 Term::const_iterator Term::end() const
1204 {
1205 return Term::const_iterator(new CVC4::Expr::const_iterator(d_expr->end()));
1206 }
1207
1208 // !!! This is only temporarily available until the parser is fully migrated
1209 // to the new API. !!!
getExpr(void) const1210 CVC4::Expr Term::getExpr(void) const { return *d_expr; }
1211
operator <<(std::ostream & out,const Term & t)1212 std::ostream& operator<<(std::ostream& out, const Term& t)
1213 {
1214 out << t.toString();
1215 return out;
1216 }
1217
operator <<(std::ostream & out,const std::vector<Term> & vector)1218 std::ostream& operator<<(std::ostream& out, const std::vector<Term>& vector)
1219 {
1220 container_to_stream(out, vector);
1221 return out;
1222 }
1223
operator <<(std::ostream & out,const std::set<Term> & set)1224 std::ostream& operator<<(std::ostream& out, const std::set<Term>& set)
1225 {
1226 container_to_stream(out, set);
1227 return out;
1228 }
1229
operator <<(std::ostream & out,const std::unordered_set<Term,TermHashFunction> & unordered_set)1230 std::ostream& operator<<(
1231 std::ostream& out,
1232 const std::unordered_set<Term, TermHashFunction>& unordered_set)
1233 {
1234 container_to_stream(out, unordered_set);
1235 return out;
1236 }
1237
1238 template <typename V>
operator <<(std::ostream & out,const std::map<Term,V> & map)1239 std::ostream& operator<<(std::ostream& out, const std::map<Term, V>& map)
1240 {
1241 container_to_stream(out, map);
1242 return out;
1243 }
1244
1245 template <typename V>
operator <<(std::ostream & out,const std::unordered_map<Term,V,TermHashFunction> & unordered_map)1246 std::ostream& operator<<(
1247 std::ostream& out,
1248 const std::unordered_map<Term, V, TermHashFunction>& unordered_map)
1249 {
1250 container_to_stream(out, unordered_map);
1251 return out;
1252 }
1253
operator ()(const Term & t) const1254 size_t TermHashFunction::operator()(const Term& t) const
1255 {
1256 return ExprHashFunction()(*t.d_expr);
1257 }
1258
1259 /* -------------------------------------------------------------------------- */
1260 /* OpTerm */
1261 /* -------------------------------------------------------------------------- */
1262
OpTerm()1263 OpTerm::OpTerm() : d_expr(new CVC4::Expr()) {}
1264
OpTerm(const CVC4::Expr & e)1265 OpTerm::OpTerm(const CVC4::Expr& e) : d_expr(new CVC4::Expr(e)) {}
1266
~OpTerm()1267 OpTerm::~OpTerm() {}
1268
operator ==(const OpTerm & t) const1269 bool OpTerm::operator==(const OpTerm& t) const { return *d_expr == *t.d_expr; }
1270
operator !=(const OpTerm & t) const1271 bool OpTerm::operator!=(const OpTerm& t) const { return *d_expr != *t.d_expr; }
1272
getKind() const1273 Kind OpTerm::getKind() const
1274 {
1275 CVC4_API_CHECK_NOT_NULL;
1276 return intToExtKind(d_expr->getKind());
1277 }
1278
getSort() const1279 Sort OpTerm::getSort() const
1280 {
1281 CVC4_API_CHECK_NOT_NULL;
1282 return Sort(d_expr->getType());
1283 }
1284
isNull() const1285 bool OpTerm::isNull() const { return d_expr->isNull(); }
1286
toString() const1287 std::string OpTerm::toString() const { return d_expr->toString(); }
1288
1289 // !!! This is only temporarily available until the parser is fully migrated
1290 // to the new API. !!!
getExpr(void) const1291 CVC4::Expr OpTerm::getExpr(void) const { return *d_expr; }
1292
operator <<(std::ostream & out,const OpTerm & t)1293 std::ostream& operator<<(std::ostream& out, const OpTerm& t)
1294 {
1295 out << t.toString();
1296 return out;
1297 }
1298
operator ()(const OpTerm & t) const1299 size_t OpTermHashFunction::operator()(const OpTerm& t) const
1300 {
1301 return ExprHashFunction()(*t.d_expr);
1302 }
1303
1304 /* -------------------------------------------------------------------------- */
1305 /* Datatypes */
1306 /* -------------------------------------------------------------------------- */
1307
1308 /* DatatypeSelectorDecl ----------------------------------------------------- */
1309
DatatypeSelectorDecl(const std::string & name,Sort sort)1310 DatatypeSelectorDecl::DatatypeSelectorDecl(const std::string& name, Sort sort)
1311 : d_name(name), d_sort(sort)
1312 {
1313 }
1314
DatatypeSelectorDecl(const std::string & name,DatatypeDeclSelfSort sort)1315 DatatypeSelectorDecl::DatatypeSelectorDecl(const std::string& name,
1316 DatatypeDeclSelfSort sort)
1317 : d_name(name), d_sort(Sort(CVC4::Type()))
1318 {
1319 }
1320
toString() const1321 std::string DatatypeSelectorDecl::toString() const
1322 {
1323 std::stringstream ss;
1324 ss << d_name << ": " << d_sort;
1325 return ss.str();
1326 }
1327
operator <<(std::ostream & out,const DatatypeDecl & dtdecl)1328 std::ostream& operator<<(std::ostream& out, const DatatypeDecl& dtdecl)
1329 {
1330 out << dtdecl.toString();
1331 return out;
1332 }
1333
1334 /* DatatypeConstructorDecl -------------------------------------------------- */
1335
DatatypeConstructorDecl(const std::string & name)1336 DatatypeConstructorDecl::DatatypeConstructorDecl(const std::string& name)
1337 : d_ctor(new CVC4::DatatypeConstructor(name))
1338 {
1339 }
1340
addSelector(const DatatypeSelectorDecl & stor)1341 void DatatypeConstructorDecl::addSelector(const DatatypeSelectorDecl& stor)
1342 {
1343 CVC4::Type t = *stor.d_sort.d_type;
1344 if (t.isNull())
1345 {
1346 d_ctor->addArg(stor.d_name, DatatypeSelfType());
1347 }
1348 else
1349 {
1350 d_ctor->addArg(stor.d_name, t);
1351 }
1352 }
1353
toString() const1354 std::string DatatypeConstructorDecl::toString() const
1355 {
1356 std::stringstream ss;
1357 ss << *d_ctor;
1358 return ss.str();
1359 }
1360
1361 // !!! This is only temporarily available until the parser is fully migrated
1362 // to the new API. !!!
getDatatypeConstructor(void) const1363 CVC4::DatatypeConstructor DatatypeConstructorDecl::getDatatypeConstructor(
1364 void) const
1365 {
1366 return *d_ctor;
1367 }
1368
operator <<(std::ostream & out,const DatatypeConstructorDecl & ctordecl)1369 std::ostream& operator<<(std::ostream& out,
1370 const DatatypeConstructorDecl& ctordecl)
1371 {
1372 out << ctordecl.toString();
1373 return out;
1374 }
1375
operator <<(std::ostream & out,const std::vector<DatatypeConstructorDecl> & vector)1376 std::ostream& operator<<(std::ostream& out,
1377 const std::vector<DatatypeConstructorDecl>& vector)
1378 {
1379 container_to_stream(out, vector);
1380 return out;
1381 }
1382
1383 /* DatatypeDecl ------------------------------------------------------------- */
1384
DatatypeDecl(const std::string & name,bool isCoDatatype)1385 DatatypeDecl::DatatypeDecl(const std::string& name, bool isCoDatatype)
1386 : d_dtype(new CVC4::Datatype(name, isCoDatatype))
1387 {
1388 }
1389
DatatypeDecl(const std::string & name,Sort param,bool isCoDatatype)1390 DatatypeDecl::DatatypeDecl(const std::string& name,
1391 Sort param,
1392 bool isCoDatatype)
1393 : d_dtype(new CVC4::Datatype(
1394 name, std::vector<Type>{*param.d_type}, isCoDatatype))
1395 {
1396 }
1397
DatatypeDecl(const std::string & name,const std::vector<Sort> & params,bool isCoDatatype)1398 DatatypeDecl::DatatypeDecl(const std::string& name,
1399 const std::vector<Sort>& params,
1400 bool isCoDatatype)
1401 {
1402 std::vector<Type> tparams;
1403 for (const Sort& s : params)
1404 {
1405 tparams.push_back(*s.d_type);
1406 }
1407 d_dtype = std::shared_ptr<CVC4::Datatype>(
1408 new CVC4::Datatype(name, tparams, isCoDatatype));
1409 }
1410
~DatatypeDecl()1411 DatatypeDecl::~DatatypeDecl() {}
1412
addConstructor(const DatatypeConstructorDecl & ctor)1413 void DatatypeDecl::addConstructor(const DatatypeConstructorDecl& ctor)
1414 {
1415 d_dtype->addConstructor(*ctor.d_ctor);
1416 }
1417
getNumConstructors() const1418 size_t DatatypeDecl::getNumConstructors() const
1419 {
1420 return d_dtype->getNumConstructors();
1421 }
1422
isParametric() const1423 bool DatatypeDecl::isParametric() const { return d_dtype->isParametric(); }
1424
toString() const1425 std::string DatatypeDecl::toString() const
1426 {
1427 std::stringstream ss;
1428 ss << *d_dtype;
1429 return ss.str();
1430 }
1431
1432 // !!! This is only temporarily available until the parser is fully migrated
1433 // to the new API. !!!
getDatatype(void) const1434 CVC4::Datatype DatatypeDecl::getDatatype(void) const { return *d_dtype; }
1435
operator <<(std::ostream & out,const DatatypeSelectorDecl & stordecl)1436 std::ostream& operator<<(std::ostream& out,
1437 const DatatypeSelectorDecl& stordecl)
1438 {
1439 out << stordecl.toString();
1440 return out;
1441 }
1442
1443 /* DatatypeSelector --------------------------------------------------------- */
1444
DatatypeSelector()1445 DatatypeSelector::DatatypeSelector() { d_stor = nullptr; }
1446
DatatypeSelector(const CVC4::DatatypeConstructorArg & stor)1447 DatatypeSelector::DatatypeSelector(const CVC4::DatatypeConstructorArg& stor)
1448 : d_stor(new CVC4::DatatypeConstructorArg(stor))
1449 {
1450 }
1451
~DatatypeSelector()1452 DatatypeSelector::~DatatypeSelector() {}
1453
isResolved() const1454 bool DatatypeSelector::isResolved() const { return d_stor->isResolved(); }
1455
getSelectorTerm() const1456 OpTerm DatatypeSelector::getSelectorTerm() const
1457 {
1458 CVC4_API_CHECK(isResolved()) << "Expected resolved datatype selector.";
1459 return d_stor->getSelector();
1460 }
1461
toString() const1462 std::string DatatypeSelector::toString() const
1463 {
1464 std::stringstream ss;
1465 ss << *d_stor;
1466 return ss.str();
1467 }
1468
1469 // !!! This is only temporarily available until the parser is fully migrated
1470 // to the new API. !!!
getDatatypeConstructorArg(void) const1471 CVC4::DatatypeConstructorArg DatatypeSelector::getDatatypeConstructorArg(
1472 void) const
1473 {
1474 return *d_stor;
1475 }
1476
operator <<(std::ostream & out,const DatatypeSelector & stor)1477 std::ostream& operator<<(std::ostream& out, const DatatypeSelector& stor)
1478 {
1479 out << stor.toString();
1480 return out;
1481 }
1482
1483 /* DatatypeConstructor ------------------------------------------------------ */
1484
DatatypeConstructor()1485 DatatypeConstructor::DatatypeConstructor() { d_ctor = nullptr; }
1486
DatatypeConstructor(const CVC4::DatatypeConstructor & ctor)1487 DatatypeConstructor::DatatypeConstructor(const CVC4::DatatypeConstructor& ctor)
1488 : d_ctor(new CVC4::DatatypeConstructor(ctor))
1489 {
1490 }
1491
~DatatypeConstructor()1492 DatatypeConstructor::~DatatypeConstructor() {}
1493
isResolved() const1494 bool DatatypeConstructor::isResolved() const { return d_ctor->isResolved(); }
1495
getConstructorTerm() const1496 OpTerm DatatypeConstructor::getConstructorTerm() const
1497 {
1498 CVC4_API_CHECK(isResolved()) << "Expected resolved datatype constructor.";
1499 return OpTerm(d_ctor->getConstructor());
1500 }
1501
operator [](const std::string & name) const1502 DatatypeSelector DatatypeConstructor::operator[](const std::string& name) const
1503 {
1504 // CHECK: selector with name exists?
1505 // CHECK: is resolved?
1506 return (*d_ctor)[name];
1507 }
1508
getSelector(const std::string & name) const1509 DatatypeSelector DatatypeConstructor::getSelector(const std::string& name) const
1510 {
1511 // CHECK: cons with name exists?
1512 // CHECK: is resolved?
1513 return (*d_ctor)[name];
1514 }
1515
getSelectorTerm(const std::string & name) const1516 OpTerm DatatypeConstructor::getSelectorTerm(const std::string& name) const
1517 {
1518 // CHECK: cons with name exists?
1519 // CHECK: is resolved?
1520 return d_ctor->getSelector(name);
1521 }
1522
begin() const1523 DatatypeConstructor::const_iterator DatatypeConstructor::begin() const
1524 {
1525 return DatatypeConstructor::const_iterator(*d_ctor, true);
1526 }
1527
end() const1528 DatatypeConstructor::const_iterator DatatypeConstructor::end() const
1529 {
1530 return DatatypeConstructor::const_iterator(*d_ctor, false);
1531 }
1532
const_iterator(const CVC4::DatatypeConstructor & ctor,bool begin)1533 DatatypeConstructor::const_iterator::const_iterator(
1534 const CVC4::DatatypeConstructor& ctor, bool begin)
1535 {
1536 d_int_stors = ctor.getArgs();
1537 const std::vector<CVC4::DatatypeConstructorArg>* sels =
1538 static_cast<const std::vector<CVC4::DatatypeConstructorArg>*>(
1539 d_int_stors);
1540 for (const auto& s : *sels)
1541 {
1542 /* Can not use emplace_back here since constructor is private. */
1543 d_stors.push_back(DatatypeSelector(s));
1544 }
1545 d_idx = begin ? 0 : sels->size();
1546 }
1547
1548 DatatypeConstructor::const_iterator& DatatypeConstructor::const_iterator::
operator =(const DatatypeConstructor::const_iterator & it)1549 operator=(const DatatypeConstructor::const_iterator& it)
1550 {
1551 d_int_stors = it.d_int_stors;
1552 d_stors = it.d_stors;
1553 d_idx = it.d_idx;
1554 return *this;
1555 }
1556
operator *() const1557 const DatatypeSelector& DatatypeConstructor::const_iterator::operator*() const
1558 {
1559 return d_stors[d_idx];
1560 }
1561
operator ->() const1562 const DatatypeSelector* DatatypeConstructor::const_iterator::operator->() const
1563 {
1564 return &d_stors[d_idx];
1565 }
1566
1567 DatatypeConstructor::const_iterator& DatatypeConstructor::const_iterator::
operator ++()1568 operator++()
1569 {
1570 ++d_idx;
1571 return *this;
1572 }
1573
1574 DatatypeConstructor::const_iterator DatatypeConstructor::const_iterator::
operator ++(int)1575 operator++(int)
1576 {
1577 DatatypeConstructor::const_iterator it(*this);
1578 ++d_idx;
1579 return it;
1580 }
1581
operator ==(const DatatypeConstructor::const_iterator & other) const1582 bool DatatypeConstructor::const_iterator::operator==(
1583 const DatatypeConstructor::const_iterator& other) const
1584 {
1585 return d_int_stors == other.d_int_stors && d_idx == other.d_idx;
1586 }
1587
operator !=(const DatatypeConstructor::const_iterator & other) const1588 bool DatatypeConstructor::const_iterator::operator!=(
1589 const DatatypeConstructor::const_iterator& other) const
1590 {
1591 return d_int_stors != other.d_int_stors || d_idx != other.d_idx;
1592 }
1593
toString() const1594 std::string DatatypeConstructor::toString() const
1595 {
1596 std::stringstream ss;
1597 ss << *d_ctor;
1598 return ss.str();
1599 }
1600
1601 // !!! This is only temporarily available until the parser is fully migrated
1602 // to the new API. !!!
getDatatypeConstructor(void) const1603 CVC4::DatatypeConstructor DatatypeConstructor::getDatatypeConstructor(
1604 void) const
1605 {
1606 return *d_ctor;
1607 }
1608
operator <<(std::ostream & out,const DatatypeConstructor & ctor)1609 std::ostream& operator<<(std::ostream& out, const DatatypeConstructor& ctor)
1610 {
1611 out << ctor.toString();
1612 return out;
1613 }
1614
1615 /* Datatype ----------------------------------------------------------------- */
1616
Datatype(const CVC4::Datatype & dtype)1617 Datatype::Datatype(const CVC4::Datatype& dtype)
1618 : d_dtype(new CVC4::Datatype(dtype))
1619 {
1620 }
1621
~Datatype()1622 Datatype::~Datatype() {}
1623
operator [](size_t idx) const1624 DatatypeConstructor Datatype::operator[](size_t idx) const
1625 {
1626 // CHECK (maybe): is resolved?
1627 CVC4_API_CHECK(idx < getNumConstructors()) << "Index out of bounds.";
1628 return (*d_dtype)[idx];
1629 }
1630
operator [](const std::string & name) const1631 DatatypeConstructor Datatype::operator[](const std::string& name) const
1632 {
1633 // CHECK: cons with name exists?
1634 // CHECK: is resolved?
1635 return (*d_dtype)[name];
1636 }
1637
getConstructor(const std::string & name) const1638 DatatypeConstructor Datatype::getConstructor(const std::string& name) const
1639 {
1640 // CHECK: cons with name exists?
1641 // CHECK: is resolved?
1642 return (*d_dtype)[name];
1643 }
1644
getConstructorTerm(const std::string & name) const1645 OpTerm Datatype::getConstructorTerm(const std::string& name) const
1646 {
1647 // CHECK: cons with name exists?
1648 // CHECK: is resolved?
1649 return d_dtype->getConstructor(name);
1650 }
1651
getNumConstructors() const1652 size_t Datatype::getNumConstructors() const
1653 {
1654 return d_dtype->getNumConstructors();
1655 }
1656
isParametric() const1657 bool Datatype::isParametric() const { return d_dtype->isParametric(); }
1658
begin() const1659 Datatype::const_iterator Datatype::begin() const
1660 {
1661 return Datatype::const_iterator(*d_dtype, true);
1662 }
1663
end() const1664 Datatype::const_iterator Datatype::end() const
1665 {
1666 return Datatype::const_iterator(*d_dtype, false);
1667 }
1668
1669 // !!! This is only temporarily available until the parser is fully migrated
1670 // to the new API. !!!
getDatatype(void) const1671 CVC4::Datatype Datatype::getDatatype(void) const { return *d_dtype; }
1672
const_iterator(const CVC4::Datatype & dtype,bool begin)1673 Datatype::const_iterator::const_iterator(const CVC4::Datatype& dtype,
1674 bool begin)
1675 {
1676 d_int_ctors = dtype.getConstructors();
1677 const std::vector<CVC4::DatatypeConstructor>* cons =
1678 static_cast<const std::vector<CVC4::DatatypeConstructor>*>(d_int_ctors);
1679 for (const auto& c : *cons)
1680 {
1681 /* Can not use emplace_back here since constructor is private. */
1682 d_ctors.push_back(DatatypeConstructor(c));
1683 }
1684 d_idx = begin ? 0 : cons->size();
1685 }
1686
operator =(const Datatype::const_iterator & it)1687 Datatype::const_iterator& Datatype::const_iterator::operator=(
1688 const Datatype::const_iterator& it)
1689 {
1690 d_int_ctors = it.d_int_ctors;
1691 d_ctors = it.d_ctors;
1692 d_idx = it.d_idx;
1693 return *this;
1694 }
1695
operator *() const1696 const DatatypeConstructor& Datatype::const_iterator::operator*() const
1697 {
1698 return d_ctors[d_idx];
1699 }
1700
operator ->() const1701 const DatatypeConstructor* Datatype::const_iterator::operator->() const
1702 {
1703 return &d_ctors[d_idx];
1704 }
1705
operator ++()1706 Datatype::const_iterator& Datatype::const_iterator::operator++()
1707 {
1708 ++d_idx;
1709 return *this;
1710 }
1711
operator ++(int)1712 Datatype::const_iterator Datatype::const_iterator::operator++(int)
1713 {
1714 Datatype::const_iterator it(*this);
1715 ++d_idx;
1716 return it;
1717 }
1718
operator ==(const Datatype::const_iterator & other) const1719 bool Datatype::const_iterator::operator==(
1720 const Datatype::const_iterator& other) const
1721 {
1722 return d_int_ctors == other.d_int_ctors && d_idx == other.d_idx;
1723 }
1724
operator !=(const Datatype::const_iterator & other) const1725 bool Datatype::const_iterator::operator!=(
1726 const Datatype::const_iterator& other) const
1727 {
1728 return d_int_ctors != other.d_int_ctors || d_idx != other.d_idx;
1729 }
1730
1731 /* -------------------------------------------------------------------------- */
1732 /* Rounding Mode for Floating Points */
1733 /* -------------------------------------------------------------------------- */
1734
1735 const static std::
1736 unordered_map<RoundingMode, CVC4::RoundingMode, RoundingModeHashFunction>
1737 s_rmodes{
1738 {ROUND_NEAREST_TIES_TO_EVEN,
1739 CVC4::RoundingMode::roundNearestTiesToEven},
1740 {ROUND_TOWARD_POSITIVE, CVC4::RoundingMode::roundTowardPositive},
1741 {ROUND_TOWARD_NEGATIVE, CVC4::RoundingMode::roundTowardNegative},
1742 {ROUND_TOWARD_ZERO, CVC4::RoundingMode::roundTowardZero},
1743 {ROUND_NEAREST_TIES_TO_AWAY,
1744 CVC4::RoundingMode::roundNearestTiesToAway},
1745 };
1746
1747 const static std::unordered_map<CVC4::RoundingMode,
1748 RoundingMode,
1749 CVC4::RoundingModeHashFunction>
1750 s_rmodes_internal{
1751 {CVC4::RoundingMode::roundNearestTiesToEven,
1752 ROUND_NEAREST_TIES_TO_EVEN},
1753 {CVC4::RoundingMode::roundTowardPositive, ROUND_TOWARD_POSITIVE},
1754 {CVC4::RoundingMode::roundTowardNegative, ROUND_TOWARD_NEGATIVE},
1755 {CVC4::RoundingMode::roundTowardZero, ROUND_TOWARD_ZERO},
1756 {CVC4::RoundingMode::roundNearestTiesToAway,
1757 ROUND_NEAREST_TIES_TO_AWAY},
1758 };
1759
operator ()(const RoundingMode & rm) const1760 size_t RoundingModeHashFunction::operator()(const RoundingMode& rm) const
1761 {
1762 return size_t(rm);
1763 }
1764
1765 /* -------------------------------------------------------------------------- */
1766 /* Solver */
1767 /* -------------------------------------------------------------------------- */
1768
Solver(Options * opts)1769 Solver::Solver(Options* opts)
1770 {
1771 Options* o = opts == nullptr ? new Options() : opts;
1772 d_exprMgr.reset(new ExprManager(*o));
1773 d_smtEngine.reset(new SmtEngine(d_exprMgr.get()));
1774 d_rng.reset(new Random((*o)[options::seed]));
1775 if (opts == nullptr) delete o;
1776 }
1777
~Solver()1778 Solver::~Solver() {}
1779
1780 /* Sorts Handling */
1781 /* -------------------------------------------------------------------------- */
1782
getNullSort(void) const1783 Sort Solver::getNullSort(void) const { return Type(); }
1784
getBooleanSort(void) const1785 Sort Solver::getBooleanSort(void) const { return d_exprMgr->booleanType(); }
1786
getIntegerSort(void) const1787 Sort Solver::getIntegerSort(void) const { return d_exprMgr->integerType(); }
1788
getRealSort(void) const1789 Sort Solver::getRealSort(void) const { return d_exprMgr->realType(); }
1790
getRegExpSort(void) const1791 Sort Solver::getRegExpSort(void) const { return d_exprMgr->regExpType(); }
1792
getStringSort(void) const1793 Sort Solver::getStringSort(void) const { return d_exprMgr->stringType(); }
1794
getRoundingmodeSort(void) const1795 Sort Solver::getRoundingmodeSort(void) const
1796 {
1797 return d_exprMgr->roundingModeType();
1798 }
1799
1800 /* Create sorts ------------------------------------------------------- */
1801
mkArraySort(Sort indexSort,Sort elemSort) const1802 Sort Solver::mkArraySort(Sort indexSort, Sort elemSort) const
1803 {
1804 CVC4_API_ARG_CHECK_EXPECTED(!indexSort.isNull(), indexSort)
1805 << "non-null index sort";
1806 CVC4_API_ARG_CHECK_EXPECTED(!elemSort.isNull(), elemSort)
1807 << "non-null element sort";
1808 return d_exprMgr->mkArrayType(*indexSort.d_type, *elemSort.d_type);
1809 }
1810
mkBitVectorSort(uint32_t size) const1811 Sort Solver::mkBitVectorSort(uint32_t size) const
1812 {
1813 CVC4_API_ARG_CHECK_EXPECTED(size > 0, size) << "size > 0";
1814 return d_exprMgr->mkBitVectorType(size);
1815 }
1816
mkFloatingPointSort(uint32_t exp,uint32_t sig) const1817 Sort Solver::mkFloatingPointSort(uint32_t exp, uint32_t sig) const
1818 {
1819 CVC4_API_ARG_CHECK_EXPECTED(exp > 0, exp) << "exponent size > 0";
1820 CVC4_API_ARG_CHECK_EXPECTED(sig > 0, sig) << "significand size > 0";
1821 return d_exprMgr->mkFloatingPointType(exp, sig);
1822 }
1823
mkDatatypeSort(DatatypeDecl dtypedecl) const1824 Sort Solver::mkDatatypeSort(DatatypeDecl dtypedecl) const
1825 {
1826 CVC4_API_ARG_CHECK_EXPECTED(dtypedecl.getNumConstructors() > 0, dtypedecl)
1827 << "a datatype declaration with at least one constructor";
1828 return d_exprMgr->mkDatatypeType(*dtypedecl.d_dtype);
1829 }
1830
mkFunctionSort(Sort domain,Sort codomain) const1831 Sort Solver::mkFunctionSort(Sort domain, Sort codomain) const
1832 {
1833 CVC4_API_ARG_CHECK_EXPECTED(!codomain.isNull(), codomain)
1834 << "non-null codomain sort";
1835 CVC4_API_ARG_CHECK_EXPECTED(domain.isFirstClass(), domain)
1836 << "first-class sort as domain sort for function sort";
1837 CVC4_API_ARG_CHECK_EXPECTED(codomain.isFirstClass(), codomain)
1838 << "first-class sort as codomain sort for function sort";
1839 Assert(!codomain.isFunction()); /* A function sort is not first-class. */
1840 return d_exprMgr->mkFunctionType(*domain.d_type, *codomain.d_type);
1841 }
1842
mkFunctionSort(const std::vector<Sort> & sorts,Sort codomain) const1843 Sort Solver::mkFunctionSort(const std::vector<Sort>& sorts, Sort codomain) const
1844 {
1845 CVC4_API_ARG_SIZE_CHECK_EXPECTED(sorts.size() >= 1, sorts)
1846 << "at least one parameter sort for function sort";
1847 for (size_t i = 0, size = sorts.size(); i < size; ++i)
1848 {
1849 CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
1850 !sorts[i].isNull(), "parameter sort", sorts[i], i)
1851 << "non-null sort";
1852 CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
1853 sorts[i].isFirstClass(), "parameter sort", sorts[i], i)
1854 << "first-class sort as parameter sort for function sort";
1855 }
1856 CVC4_API_ARG_CHECK_EXPECTED(!codomain.isNull(), codomain)
1857 << "non-null codomain sort";
1858 CVC4_API_ARG_CHECK_EXPECTED(codomain.isFirstClass(), codomain)
1859 << "first-class sort as codomain sort for function sort";
1860 Assert(!codomain.isFunction()); /* A function sort is not first-class. */
1861 std::vector<Type> argTypes = sortVectorToTypes(sorts);
1862 return d_exprMgr->mkFunctionType(argTypes, *codomain.d_type);
1863 }
1864
mkParamSort(const std::string & symbol) const1865 Sort Solver::mkParamSort(const std::string& symbol) const
1866 {
1867 return d_exprMgr->mkSort(symbol, ExprManager::SORT_FLAG_PLACEHOLDER);
1868 }
1869
mkPredicateSort(const std::vector<Sort> & sorts) const1870 Sort Solver::mkPredicateSort(const std::vector<Sort>& sorts) const
1871 {
1872 CVC4_API_ARG_SIZE_CHECK_EXPECTED(sorts.size() >= 1, sorts)
1873 << "at least one parameter sort for predicate sort";
1874 for (size_t i = 0, size = sorts.size(); i < size; ++i)
1875 {
1876 CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
1877 !sorts[i].isNull(), "parameter sort", sorts[i], i)
1878 << "non-null sort";
1879 CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
1880 sorts[i].isFirstClass(), "parameter sort", sorts[i], i)
1881 << "first-class sort as parameter sort for predicate sort";
1882 }
1883 std::vector<Type> types = sortVectorToTypes(sorts);
1884 return d_exprMgr->mkPredicateType(types);
1885 }
1886
mkRecordSort(const std::vector<std::pair<std::string,Sort>> & fields) const1887 Sort Solver::mkRecordSort(
1888 const std::vector<std::pair<std::string, Sort>>& fields) const
1889 {
1890 std::vector<std::pair<std::string, Type>> f;
1891 size_t i = 0;
1892 for (const auto& p : fields)
1893 {
1894 CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
1895 !p.second.isNull(), "parameter sort", p.second, i)
1896 << "non-null sort";
1897 i += 1;
1898 f.emplace_back(p.first, *p.second.d_type);
1899 }
1900 return d_exprMgr->mkRecordType(Record(f));
1901 }
1902
mkSetSort(Sort elemSort) const1903 Sort Solver::mkSetSort(Sort elemSort) const
1904 {
1905 CVC4_API_ARG_CHECK_EXPECTED(!elemSort.isNull(), elemSort)
1906 << "non-null element sort";
1907 return d_exprMgr->mkSetType(*elemSort.d_type);
1908 }
1909
mkUninterpretedSort(const std::string & symbol) const1910 Sort Solver::mkUninterpretedSort(const std::string& symbol) const
1911 {
1912 return d_exprMgr->mkSort(symbol);
1913 }
1914
mkSortConstructorSort(const std::string & symbol,size_t arity) const1915 Sort Solver::mkSortConstructorSort(const std::string& symbol,
1916 size_t arity) const
1917 {
1918 CVC4_API_ARG_CHECK_EXPECTED(arity > 0, arity) << "an arity > 0";
1919 return d_exprMgr->mkSortConstructor(symbol, arity);
1920 }
1921
mkTupleSort(const std::vector<Sort> & sorts) const1922 Sort Solver::mkTupleSort(const std::vector<Sort>& sorts) const
1923 {
1924 for (size_t i = 0, size = sorts.size(); i < size; ++i)
1925 {
1926 CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
1927 !sorts[i].isNull(), "parameter sort", sorts[i], i)
1928 << "non-null sort";
1929 CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
1930 !sorts[i].isFunctionLike(), "parameter sort", sorts[i], i)
1931 << "non-function-like sort as parameter sort for tuple sort";
1932 }
1933 std::vector<Type> types = sortVectorToTypes(sorts);
1934 return d_exprMgr->mkTupleType(types);
1935 }
1936
sortVectorToTypes(const std::vector<Sort> & sorts) const1937 std::vector<Type> Solver::sortVectorToTypes(
1938 const std::vector<Sort>& sorts) const
1939 {
1940 std::vector<Type> res;
1941 for (const Sort& s : sorts)
1942 {
1943 res.push_back(*s.d_type);
1944 }
1945 return res;
1946 }
1947
1948 /* Create consts */
1949 /* -------------------------------------------------------------------------- */
1950
mkTrue(void) const1951 Term Solver::mkTrue(void) const { return d_exprMgr->mkConst<bool>(true); }
1952
mkFalse(void) const1953 Term Solver::mkFalse(void) const { return d_exprMgr->mkConst<bool>(false); }
1954
mkBoolean(bool val) const1955 Term Solver::mkBoolean(bool val) const { return d_exprMgr->mkConst<bool>(val); }
1956
mkPi() const1957 Term Solver::mkPi() const
1958 {
1959 try
1960 {
1961 Term res =
1962 d_exprMgr->mkNullaryOperator(d_exprMgr->realType(), CVC4::kind::PI);
1963 (void)res.d_expr->getType(true); /* kick off type checking */
1964 return res;
1965 }
1966 catch (const CVC4::TypeCheckingException& e)
1967 {
1968 throw CVC4ApiException(e.getMessage());
1969 }
1970 }
1971
1972 template <typename T>
mkConstHelper(T t) const1973 Term Solver::mkConstHelper(T t) const
1974 {
1975 try
1976 {
1977 Term res = d_exprMgr->mkConst(t);
1978 (void)res.d_expr->getType(true); /* kick off type checking */
1979 return res;
1980 }
1981 catch (const CVC4::TypeCheckingException& e)
1982 {
1983 throw CVC4ApiException(e.getMessage());
1984 }
1985 }
1986
1987 /* Split out to avoid nested API calls (problematic with API tracing). */
mkRealFromStrHelper(std::string s) const1988 Term Solver::mkRealFromStrHelper(std::string s) const
1989 {
1990 /* CLN and GMP handle this case differently, CLN interprets it as 0, GMP
1991 * throws an std::invalid_argument exception. For consistency, we treat it
1992 * as invalid. */
1993 CVC4_API_ARG_CHECK_EXPECTED(s != ".", s)
1994 << "a string representing an integer, real or rational value.";
1995 try
1996 {
1997 CVC4::Rational r = s.find('/') != std::string::npos
1998 ? CVC4::Rational(s)
1999 : CVC4::Rational::fromDecimal(s);
2000 return mkConstHelper<CVC4::Rational>(r);
2001 }
2002 catch (const std::invalid_argument& e)
2003 {
2004 throw CVC4ApiException(e.what());
2005 }
2006 }
2007
mkReal(const char * s) const2008 Term Solver::mkReal(const char* s) const
2009 {
2010 CVC4_API_ARG_CHECK_NOT_NULL(s);
2011 return mkRealFromStrHelper(std::string(s));
2012 }
2013
mkReal(const std::string & s) const2014 Term Solver::mkReal(const std::string& s) const
2015 {
2016 return mkRealFromStrHelper(s);
2017 }
2018
mkReal(int32_t val) const2019 Term Solver::mkReal(int32_t val) const
2020 {
2021 try
2022 {
2023 return mkConstHelper<CVC4::Rational>(CVC4::Rational(val));
2024 }
2025 catch (const std::invalid_argument& e)
2026 {
2027 throw CVC4ApiException(e.what());
2028 }
2029 }
2030
mkReal(int64_t val) const2031 Term Solver::mkReal(int64_t val) const
2032 {
2033 try
2034 {
2035 return mkConstHelper<CVC4::Rational>(CVC4::Rational(val));
2036 }
2037 catch (const std::invalid_argument& e)
2038 {
2039 throw CVC4ApiException(e.what());
2040 }
2041 }
2042
mkReal(uint32_t val) const2043 Term Solver::mkReal(uint32_t val) const
2044 {
2045 try
2046 {
2047 return mkConstHelper<CVC4::Rational>(CVC4::Rational(val));
2048 }
2049 catch (const std::invalid_argument& e)
2050 {
2051 throw CVC4ApiException(e.what());
2052 }
2053 }
2054
mkReal(uint64_t val) const2055 Term Solver::mkReal(uint64_t val) const
2056 {
2057 try
2058 {
2059 return mkConstHelper<CVC4::Rational>(CVC4::Rational(val));
2060 }
2061 catch (const std::invalid_argument& e)
2062 {
2063 throw CVC4ApiException(e.what());
2064 }
2065 }
2066
mkReal(int32_t num,int32_t den) const2067 Term Solver::mkReal(int32_t num, int32_t den) const
2068 {
2069 try
2070 {
2071 return mkConstHelper<CVC4::Rational>(CVC4::Rational(num, den));
2072 }
2073 catch (const std::invalid_argument& e)
2074 {
2075 throw CVC4ApiException(e.what());
2076 }
2077 }
2078
mkReal(int64_t num,int64_t den) const2079 Term Solver::mkReal(int64_t num, int64_t den) const
2080 {
2081 try
2082 {
2083 return mkConstHelper<CVC4::Rational>(CVC4::Rational(num, den));
2084 }
2085 catch (const std::invalid_argument& e)
2086 {
2087 throw CVC4ApiException(e.what());
2088 }
2089 }
2090
mkReal(uint32_t num,uint32_t den) const2091 Term Solver::mkReal(uint32_t num, uint32_t den) const
2092 {
2093 try
2094 {
2095 return mkConstHelper<CVC4::Rational>(CVC4::Rational(num, den));
2096 }
2097 catch (const std::invalid_argument& e)
2098 {
2099 throw CVC4ApiException(e.what());
2100 }
2101 }
2102
mkReal(uint64_t num,uint64_t den) const2103 Term Solver::mkReal(uint64_t num, uint64_t den) const
2104 {
2105 try
2106 {
2107 return mkConstHelper<CVC4::Rational>(CVC4::Rational(num, den));
2108 }
2109 catch (const std::invalid_argument& e)
2110 {
2111 throw CVC4ApiException(e.what());
2112 }
2113 }
2114
mkRegexpEmpty() const2115 Term Solver::mkRegexpEmpty() const
2116 {
2117 try
2118 {
2119 Term res =
2120 d_exprMgr->mkExpr(CVC4::kind::REGEXP_EMPTY, std::vector<CVC4::Expr>());
2121 (void)res.d_expr->getType(true); /* kick off type checking */
2122 return res;
2123 }
2124 catch (const CVC4::TypeCheckingException& e)
2125 {
2126 throw CVC4ApiException(e.getMessage());
2127 }
2128 }
2129
mkRegexpSigma() const2130 Term Solver::mkRegexpSigma() const
2131 {
2132 try
2133 {
2134 Term res =
2135 d_exprMgr->mkExpr(CVC4::kind::REGEXP_SIGMA, std::vector<CVC4::Expr>());
2136 (void)res.d_expr->getType(true); /* kick off type checking */
2137 return res;
2138 }
2139 catch (const CVC4::TypeCheckingException& e)
2140 {
2141 throw CVC4ApiException(e.getMessage());
2142 }
2143 }
2144
mkEmptySet(Sort s) const2145 Term Solver::mkEmptySet(Sort s) const
2146 {
2147 CVC4_API_ARG_CHECK_EXPECTED(s.isNull() || s.isSet(), s)
2148 << "null sort or set sort";
2149 return mkConstHelper<CVC4::EmptySet>(CVC4::EmptySet(*s.d_type));
2150 }
2151
mkSepNil(Sort sort) const2152 Term Solver::mkSepNil(Sort sort) const
2153 {
2154 try
2155 {
2156 CVC4_API_ARG_CHECK_EXPECTED(!sort.isNull(), sort) << "non-null sort";
2157 Term res = d_exprMgr->mkNullaryOperator(*sort.d_type, CVC4::kind::SEP_NIL);
2158 (void)res.d_expr->getType(true); /* kick off type checking */
2159 return res;
2160 }
2161 catch (const CVC4::TypeCheckingException& e)
2162 {
2163 throw CVC4ApiException(e.getMessage());
2164 }
2165 }
2166
mkString(const char * s,bool useEscSequences) const2167 Term Solver::mkString(const char* s, bool useEscSequences) const
2168 {
2169 return mkConstHelper<CVC4::String>(CVC4::String(s, useEscSequences));
2170 }
2171
mkString(const std::string & s,bool useEscSequences) const2172 Term Solver::mkString(const std::string& s, bool useEscSequences) const
2173 {
2174 return mkConstHelper<CVC4::String>(CVC4::String(s, useEscSequences));
2175 }
2176
mkString(const unsigned char c) const2177 Term Solver::mkString(const unsigned char c) const
2178 {
2179 return mkConstHelper<CVC4::String>(CVC4::String(std::string(1, c)));
2180 }
2181
mkString(const std::vector<unsigned> & s) const2182 Term Solver::mkString(const std::vector<unsigned>& s) const
2183 {
2184 return mkConstHelper<CVC4::String>(CVC4::String(s));
2185 }
2186
mkUniverseSet(Sort sort) const2187 Term Solver::mkUniverseSet(Sort sort) const
2188 {
2189 try
2190 {
2191 CVC4_API_ARG_CHECK_EXPECTED(!sort.isNull(), sort) << "non-null sort";
2192 Term res =
2193 d_exprMgr->mkNullaryOperator(*sort.d_type, CVC4::kind::UNIVERSE_SET);
2194 // TODO(#2771): Reenable?
2195 // (void)res.d_expr->getType(true); /* kick off type checking */
2196 return res;
2197 }
2198 catch (const CVC4::TypeCheckingException& e)
2199 {
2200 throw CVC4ApiException(e.getMessage());
2201 }
2202 }
2203
2204 /* Split out to avoid nested API calls (problematic with API tracing). */
mkBVFromIntHelper(uint32_t size,uint64_t val) const2205 Term Solver::mkBVFromIntHelper(uint32_t size, uint64_t val) const
2206 {
2207 CVC4_API_ARG_CHECK_EXPECTED(size > 0, size) << "a bit-width > 0";
2208 try
2209 {
2210 return mkConstHelper<CVC4::BitVector>(CVC4::BitVector(size, val));
2211 }
2212 catch (const std::invalid_argument& e)
2213 {
2214 throw CVC4ApiException(e.what());
2215 }
2216 }
2217
mkBitVector(uint32_t size,uint64_t val) const2218 Term Solver::mkBitVector(uint32_t size, uint64_t val) const
2219 {
2220 return mkBVFromIntHelper(size, val);
2221 }
2222
2223 /* Split out to avoid nested API calls (problematic with API tracing). */
mkBVFromStrHelper(std::string s,uint32_t base) const2224 Term Solver::mkBVFromStrHelper(std::string s, uint32_t base) const
2225 {
2226 CVC4_API_ARG_CHECK_EXPECTED(!s.empty(), s) << "a non-empty string";
2227 CVC4_API_ARG_CHECK_EXPECTED(base == 2 || base == 10 || base == 16, s)
2228 << "base 2, 10, or 16";
2229 try
2230 {
2231 return mkConstHelper<CVC4::BitVector>(CVC4::BitVector(s, base));
2232 }
2233 catch (const std::invalid_argument& e)
2234 {
2235 throw CVC4ApiException(e.what());
2236 }
2237 }
2238
mkBVFromStrHelper(uint32_t size,std::string s,uint32_t base) const2239 Term Solver::mkBVFromStrHelper(uint32_t size,
2240 std::string s,
2241 uint32_t base) const
2242 {
2243 CVC4_API_ARG_CHECK_EXPECTED(!s.empty(), s) << "a non-empty string";
2244 CVC4_API_ARG_CHECK_EXPECTED(base == 2 || base == 10 || base == 16, s)
2245 << "base 2, 10, or 16";
2246 try
2247 {
2248 Integer val(s, base);
2249 CVC4_API_CHECK(val.modByPow2(size) == val)
2250 << "Overflow in bitvector construction (specified bitvector size "
2251 << size << " too small to hold value " << s << ")";
2252 return mkConstHelper<CVC4::BitVector>(CVC4::BitVector(size, val));
2253 }
2254 catch (const std::invalid_argument& e)
2255 {
2256 throw CVC4ApiException(e.what());
2257 }
2258 }
2259
mkBitVector(const char * s,uint32_t base) const2260 Term Solver::mkBitVector(const char* s, uint32_t base) const
2261 {
2262 CVC4_API_ARG_CHECK_NOT_NULL(s);
2263 return mkBVFromStrHelper(std::string(s), base);
2264 }
2265
mkBitVector(const std::string & s,uint32_t base) const2266 Term Solver::mkBitVector(const std::string& s, uint32_t base) const
2267 {
2268 return mkBVFromStrHelper(s, base);
2269 }
2270
mkBitVector(uint32_t size,const char * s,uint32_t base) const2271 Term Solver::mkBitVector(uint32_t size, const char* s, uint32_t base) const
2272 {
2273 CVC4_API_ARG_CHECK_NOT_NULL(s);
2274 return mkBVFromStrHelper(size, s, base);
2275 }
2276
mkBitVector(uint32_t size,std::string & s,uint32_t base) const2277 Term Solver::mkBitVector(uint32_t size, std::string& s, uint32_t base) const
2278 {
2279 return mkBVFromStrHelper(size, s, base);
2280 }
2281
mkPosInf(uint32_t exp,uint32_t sig) const2282 Term Solver::mkPosInf(uint32_t exp, uint32_t sig) const
2283 {
2284 CVC4_API_CHECK(Configuration::isBuiltWithSymFPU())
2285 << "Expected CVC4 to be compiled with SymFPU support";
2286 return mkConstHelper<CVC4::FloatingPoint>(
2287 FloatingPoint::makeInf(FloatingPointSize(exp, sig), false));
2288 }
2289
mkNegInf(uint32_t exp,uint32_t sig) const2290 Term Solver::mkNegInf(uint32_t exp, uint32_t sig) const
2291 {
2292 CVC4_API_CHECK(Configuration::isBuiltWithSymFPU())
2293 << "Expected CVC4 to be compiled with SymFPU support";
2294 return mkConstHelper<CVC4::FloatingPoint>(
2295 FloatingPoint::makeInf(FloatingPointSize(exp, sig), true));
2296 }
2297
mkNaN(uint32_t exp,uint32_t sig) const2298 Term Solver::mkNaN(uint32_t exp, uint32_t sig) const
2299 {
2300 CVC4_API_CHECK(Configuration::isBuiltWithSymFPU())
2301 << "Expected CVC4 to be compiled with SymFPU support";
2302 return mkConstHelper<CVC4::FloatingPoint>(
2303 FloatingPoint::makeNaN(FloatingPointSize(exp, sig)));
2304 }
2305
mkPosZero(uint32_t exp,uint32_t sig) const2306 Term Solver::mkPosZero(uint32_t exp, uint32_t sig) const
2307 {
2308 CVC4_API_CHECK(Configuration::isBuiltWithSymFPU())
2309 << "Expected CVC4 to be compiled with SymFPU support";
2310 return mkConstHelper<CVC4::FloatingPoint>(
2311 FloatingPoint::makeZero(FloatingPointSize(exp, sig), false));
2312 }
2313
mkNegZero(uint32_t exp,uint32_t sig) const2314 Term Solver::mkNegZero(uint32_t exp, uint32_t sig) const
2315 {
2316 CVC4_API_CHECK(Configuration::isBuiltWithSymFPU())
2317 << "Expected CVC4 to be compiled with SymFPU support";
2318 return mkConstHelper<CVC4::FloatingPoint>(
2319 FloatingPoint::makeZero(FloatingPointSize(exp, sig), true));
2320 }
2321
mkRoundingMode(RoundingMode rm) const2322 Term Solver::mkRoundingMode(RoundingMode rm) const
2323 {
2324 return mkConstHelper<CVC4::RoundingMode>(s_rmodes.at(rm));
2325 }
2326
mkUninterpretedConst(Sort sort,int32_t index) const2327 Term Solver::mkUninterpretedConst(Sort sort, int32_t index) const
2328 {
2329 CVC4_API_ARG_CHECK_EXPECTED(!sort.isNull(), sort) << "non-null sort";
2330 return mkConstHelper<CVC4::UninterpretedConstant>(
2331 CVC4::UninterpretedConstant(*sort.d_type, index));
2332 }
2333
mkAbstractValue(const std::string & index) const2334 Term Solver::mkAbstractValue(const std::string& index) const
2335 {
2336 CVC4_API_ARG_CHECK_EXPECTED(!index.empty(), index) << "a non-empty string";
2337 try
2338 {
2339 CVC4::Integer idx(index, 10);
2340 CVC4_API_ARG_CHECK_EXPECTED(idx > 0, index)
2341 << "a string representing an integer > 0";
2342 return d_exprMgr->mkConst(CVC4::AbstractValue(idx));
2343 // do not call getType(), for abstract values, type can not be computed
2344 // until it is substituted away
2345 }
2346 catch (const std::invalid_argument& e)
2347 {
2348 throw CVC4ApiException(e.what());
2349 }
2350 catch (const CVC4::TypeCheckingException& e)
2351 {
2352 throw CVC4ApiException(e.getMessage());
2353 }
2354 }
2355
mkAbstractValue(uint64_t index) const2356 Term Solver::mkAbstractValue(uint64_t index) const
2357 {
2358 try
2359 {
2360 CVC4_API_ARG_CHECK_EXPECTED(index > 0, index) << "an integer > 0";
2361 return d_exprMgr->mkConst(CVC4::AbstractValue(Integer(index)));
2362 // do not call getType(), for abstract values, type can not be computed
2363 // until it is substituted away
2364 }
2365 catch (const std::invalid_argument& e)
2366 {
2367 throw CVC4ApiException(e.what());
2368 }
2369 catch (const CVC4::TypeCheckingException& e)
2370 {
2371 throw CVC4ApiException(e.getMessage());
2372 }
2373 }
2374
mkFloatingPoint(uint32_t exp,uint32_t sig,Term val) const2375 Term Solver::mkFloatingPoint(uint32_t exp, uint32_t sig, Term val) const
2376 {
2377 CVC4_API_CHECK(Configuration::isBuiltWithSymFPU())
2378 << "Expected CVC4 to be compiled with SymFPU support";
2379 CVC4_API_ARG_CHECK_EXPECTED(exp > 0, exp) << "a value > 0";
2380 CVC4_API_ARG_CHECK_EXPECTED(sig > 0, sig) << "a value > 0";
2381 uint32_t bw = exp + sig;
2382 CVC4_API_ARG_CHECK_EXPECTED(bw == val.getSort().getBVSize(), val)
2383 << "a bit-vector constant with bit-width '" << bw << "'";
2384 CVC4_API_ARG_CHECK_EXPECTED(!val.isNull(), val) << "non-null term";
2385 CVC4_API_ARG_CHECK_EXPECTED(
2386 val.getSort().isBitVector() && val.d_expr->isConst(), val)
2387 << "bit-vector constant";
2388 return mkConstHelper<CVC4::FloatingPoint>(
2389 CVC4::FloatingPoint(exp, sig, val.d_expr->getConst<BitVector>()));
2390 }
2391
2392 /* Create variables */
2393 /* -------------------------------------------------------------------------- */
2394
mkVar(Sort sort,const std::string & symbol) const2395 Term Solver::mkVar(Sort sort, const std::string& symbol) const
2396 {
2397 try
2398 {
2399 CVC4_API_ARG_CHECK_EXPECTED(!sort.isNull(), sort) << "non-null sort";
2400 Term res = symbol.empty() ? d_exprMgr->mkVar(*sort.d_type)
2401 : d_exprMgr->mkVar(symbol, *sort.d_type);
2402 (void)res.d_expr->getType(true); /* kick off type checking */
2403 return res;
2404 }
2405 catch (const CVC4::TypeCheckingException& e)
2406 {
2407 throw CVC4ApiException(e.getMessage());
2408 }
2409 }
2410
mkBoundVar(Sort sort,const std::string & symbol) const2411 Term Solver::mkBoundVar(Sort sort, const std::string& symbol) const
2412 {
2413 try
2414 {
2415 CVC4_API_ARG_CHECK_EXPECTED(!sort.isNull(), sort) << "non-null sort";
2416 Term res = symbol.empty() ? d_exprMgr->mkBoundVar(*sort.d_type)
2417 : d_exprMgr->mkBoundVar(symbol, *sort.d_type);
2418 (void)res.d_expr->getType(true); /* kick off type checking */
2419 return res;
2420 }
2421 catch (const CVC4::TypeCheckingException& e)
2422 {
2423 throw CVC4ApiException(e.getMessage());
2424 }
2425 }
2426
2427 /* Create terms */
2428 /* -------------------------------------------------------------------------- */
2429
checkMkTerm(Kind kind,uint32_t nchildren) const2430 void Solver::checkMkTerm(Kind kind, uint32_t nchildren) const
2431 {
2432 CVC4_API_KIND_CHECK(kind);
2433 Assert(isDefinedIntKind(extToIntKind(kind)));
2434 const CVC4::kind::MetaKind mk = kind::metaKindOf(extToIntKind(kind));
2435 CVC4_API_KIND_CHECK_EXPECTED(
2436 mk == kind::metakind::PARAMETERIZED || mk == kind::metakind::OPERATOR,
2437 kind)
2438 << "Only operator-style terms are created with mkTerm(), "
2439 "to create variables and constants see mkVar(), mkBoundVar(), "
2440 "and mkConst().";
2441 CVC4_API_KIND_CHECK_EXPECTED(
2442 nchildren >= minArity(kind) && nchildren <= maxArity(kind), kind)
2443 << "Terms with kind " << kindToString(kind) << " must have at least "
2444 << minArity(kind) << " children and at most " << maxArity(kind)
2445 << " children (the one under construction has " << nchildren << ")";
2446 }
2447
checkMkOpTerm(Kind kind,OpTerm opTerm,uint32_t nchildren) const2448 void Solver::checkMkOpTerm(Kind kind, OpTerm opTerm, uint32_t nchildren) const
2449 {
2450 Assert(isDefinedIntKind(extToIntKind(kind)));
2451 const CVC4::Kind int_kind = extToIntKind(kind);
2452 const CVC4::Kind int_op_kind = opTerm.d_expr->getKind();
2453 const CVC4::Kind int_op_to_kind =
2454 NodeManager::operatorToKind(opTerm.d_expr->getNode());
2455 CVC4_API_ARG_CHECK_EXPECTED(
2456 int_kind == int_op_to_kind
2457 || (kind == APPLY_CONSTRUCTOR
2458 && int_op_to_kind == CVC4::Kind::UNDEFINED_KIND)
2459 || (kind == APPLY_SELECTOR
2460 && int_op_to_kind == CVC4::Kind::UNDEFINED_KIND)
2461 || (kind == APPLY_UF && int_op_to_kind == CVC4::Kind::UNDEFINED_KIND),
2462 kind)
2463 << "kind that matches kind associated with given operator term";
2464 CVC4_API_ARG_CHECK_EXPECTED(
2465 int_op_kind == CVC4::kind::BUILTIN
2466 || CVC4::kind::metaKindOf(int_kind) == kind::metakind::PARAMETERIZED,
2467 opTerm)
2468 << "This term constructor is for parameterized kinds only";
2469 uint32_t min_arity = ExprManager::minArity(int_kind);
2470 uint32_t max_arity = ExprManager::maxArity(int_kind);
2471 CVC4_API_KIND_CHECK_EXPECTED(nchildren >= min_arity && nchildren <= max_arity,
2472 kind)
2473 << "Terms with kind " << kindToString(kind) << " must have at least "
2474 << min_arity << " children and at most " << max_arity
2475 << " children (the one under construction has " << nchildren << ")";
2476 }
2477
mkTerm(Kind kind) const2478 Term Solver::mkTerm(Kind kind) const
2479 {
2480 try
2481 {
2482 CVC4_API_KIND_CHECK_EXPECTED(
2483 kind == PI || kind == REGEXP_EMPTY || kind == REGEXP_SIGMA, kind)
2484 << "PI or REGEXP_EMPTY or REGEXP_SIGMA";
2485 Term res;
2486 if (kind == REGEXP_EMPTY || kind == REGEXP_SIGMA)
2487 {
2488 CVC4::Kind k = extToIntKind(kind);
2489 Assert(isDefinedIntKind(k));
2490 res = d_exprMgr->mkExpr(k, std::vector<Expr>());
2491 }
2492 else
2493 {
2494 Assert(kind == PI);
2495 res = d_exprMgr->mkNullaryOperator(d_exprMgr->realType(), CVC4::kind::PI);
2496 }
2497 (void)res.d_expr->getType(true); /* kick off type checking */
2498 return res;
2499 }
2500 catch (const CVC4::TypeCheckingException& e)
2501 {
2502 throw CVC4ApiException(e.getMessage());
2503 }
2504 }
2505
mkTerm(Kind kind,Term child) const2506 Term Solver::mkTerm(Kind kind, Term child) const
2507 {
2508 try
2509 {
2510 CVC4_API_ARG_CHECK_EXPECTED(!child.isNull(), child) << "non-null term";
2511 checkMkTerm(kind, 1);
2512 Term res = d_exprMgr->mkExpr(extToIntKind(kind), *child.d_expr);
2513 (void)res.d_expr->getType(true); /* kick off type checking */
2514 return res;
2515 }
2516 catch (const CVC4::TypeCheckingException& e)
2517 {
2518 throw CVC4ApiException(e.getMessage());
2519 }
2520 }
2521
mkTerm(Kind kind,Term child1,Term child2) const2522 Term Solver::mkTerm(Kind kind, Term child1, Term child2) const
2523 {
2524 try
2525 {
2526 CVC4_API_ARG_CHECK_EXPECTED(!child1.isNull(), child1) << "non-null term";
2527 CVC4_API_ARG_CHECK_EXPECTED(!child2.isNull(), child2) << "non-null term";
2528 checkMkTerm(kind, 2);
2529 Term res =
2530 d_exprMgr->mkExpr(extToIntKind(kind), *child1.d_expr, *child2.d_expr);
2531 (void)res.d_expr->getType(true); /* kick off type checking */
2532 return res;
2533 }
2534 catch (const CVC4::TypeCheckingException& e)
2535 {
2536 throw CVC4ApiException(e.getMessage());
2537 }
2538 }
2539
mkTerm(Kind kind,Term child1,Term child2,Term child3) const2540 Term Solver::mkTerm(Kind kind, Term child1, Term child2, Term child3) const
2541 {
2542 try
2543 {
2544 CVC4_API_ARG_CHECK_EXPECTED(!child1.isNull(), child1) << "non-null term";
2545 CVC4_API_ARG_CHECK_EXPECTED(!child2.isNull(), child2) << "non-null term";
2546 CVC4_API_ARG_CHECK_EXPECTED(!child3.isNull(), child3) << "non-null term";
2547 checkMkTerm(kind, 3);
2548 std::vector<Expr> echildren{*child1.d_expr, *child2.d_expr, *child3.d_expr};
2549 CVC4::Kind k = extToIntKind(kind);
2550 Assert(isDefinedIntKind(k));
2551 Term res = kind::isAssociative(k) ? d_exprMgr->mkAssociative(k, echildren)
2552 : d_exprMgr->mkExpr(k, echildren);
2553 (void)res.d_expr->getType(true); /* kick off type checking */
2554 return res;
2555 }
2556 catch (const CVC4::TypeCheckingException& e)
2557 {
2558 throw CVC4ApiException(e.getMessage());
2559 }
2560 }
2561
mkTerm(Kind kind,const std::vector<Term> & children) const2562 Term Solver::mkTerm(Kind kind, const std::vector<Term>& children) const
2563 {
2564 try
2565 {
2566 for (size_t i = 0, size = children.size(); i < size; ++i)
2567 {
2568 CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
2569 !children[i].isNull(), "parameter term", children[i], i)
2570 << "non-null term";
2571 }
2572 checkMkTerm(kind, children.size());
2573 std::vector<Expr> echildren = termVectorToExprs(children);
2574 CVC4::Kind k = extToIntKind(kind);
2575 Assert(isDefinedIntKind(k));
2576 Term res = kind::isAssociative(k) ? d_exprMgr->mkAssociative(k, echildren)
2577 : d_exprMgr->mkExpr(k, echildren);
2578 (void)res.d_expr->getType(true); /* kick off type checking */
2579 return res;
2580 }
2581 catch (const CVC4::TypeCheckingException& e)
2582 {
2583 throw CVC4ApiException(e.getMessage());
2584 }
2585 }
2586
mkTerm(Kind kind,OpTerm opTerm) const2587 Term Solver::mkTerm(Kind kind, OpTerm opTerm) const
2588 {
2589 try
2590 {
2591 checkMkOpTerm(kind, opTerm, 0);
2592 const CVC4::Kind int_kind = extToIntKind(kind);
2593 Term res = d_exprMgr->mkExpr(int_kind, *opTerm.d_expr);
2594 (void)res.d_expr->getType(true); /* kick off type checking */
2595 return res;
2596 }
2597 catch (const CVC4::TypeCheckingException& e)
2598 {
2599 throw CVC4ApiException(e.getMessage());
2600 }
2601 }
2602
mkTerm(Kind kind,OpTerm opTerm,Term child) const2603 Term Solver::mkTerm(Kind kind, OpTerm opTerm, Term child) const
2604 {
2605 try
2606 {
2607 CVC4_API_ARG_CHECK_EXPECTED(!child.isNull(), child) << "non-null term";
2608 checkMkOpTerm(kind, opTerm, 1);
2609 const CVC4::Kind int_kind = extToIntKind(kind);
2610 Term res = d_exprMgr->mkExpr(int_kind, *opTerm.d_expr, *child.d_expr);
2611 (void)res.d_expr->getType(true); /* kick off type checking */
2612 return res;
2613 }
2614 catch (const CVC4::TypeCheckingException& e)
2615 {
2616 throw CVC4ApiException(e.getMessage());
2617 }
2618 }
2619
mkTerm(Kind kind,OpTerm opTerm,Term child1,Term child2) const2620 Term Solver::mkTerm(Kind kind, OpTerm opTerm, Term child1, Term child2) const
2621 {
2622 try
2623 {
2624 CVC4_API_ARG_CHECK_EXPECTED(!child1.isNull(), child1) << "non-null term";
2625 CVC4_API_ARG_CHECK_EXPECTED(!child2.isNull(), child2) << "non-null term";
2626 checkMkOpTerm(kind, opTerm, 2);
2627 const CVC4::Kind int_kind = extToIntKind(kind);
2628 Term res = d_exprMgr->mkExpr(
2629 int_kind, *opTerm.d_expr, *child1.d_expr, *child2.d_expr);
2630 (void)res.d_expr->getType(true); /* kick off type checking */
2631 return res;
2632 }
2633 catch (const CVC4::TypeCheckingException& e)
2634 {
2635 throw CVC4ApiException(e.getMessage());
2636 }
2637 }
2638
mkTerm(Kind kind,OpTerm opTerm,Term child1,Term child2,Term child3) const2639 Term Solver::mkTerm(
2640 Kind kind, OpTerm opTerm, Term child1, Term child2, Term child3) const
2641 {
2642 try
2643 {
2644 CVC4_API_ARG_CHECK_EXPECTED(!child1.isNull(), child1) << "non-null term";
2645 CVC4_API_ARG_CHECK_EXPECTED(!child2.isNull(), child2) << "non-null term";
2646 CVC4_API_ARG_CHECK_EXPECTED(!child3.isNull(), child3) << "non-null term";
2647 checkMkOpTerm(kind, opTerm, 3);
2648 const CVC4::Kind int_kind = extToIntKind(kind);
2649 Term res = d_exprMgr->mkExpr(int_kind,
2650 *opTerm.d_expr,
2651 *child1.d_expr,
2652 *child2.d_expr,
2653 *child3.d_expr);
2654 (void)res.d_expr->getType(true); /* kick off type checking */
2655 return res;
2656 }
2657 catch (const CVC4::TypeCheckingException& e)
2658 {
2659 throw CVC4ApiException(e.getMessage());
2660 }
2661 }
2662
mkTerm(Kind kind,OpTerm opTerm,const std::vector<Term> & children) const2663 Term Solver::mkTerm(Kind kind,
2664 OpTerm opTerm,
2665 const std::vector<Term>& children) const
2666 {
2667 try
2668 {
2669 for (size_t i = 0, size = children.size(); i < size; ++i)
2670 {
2671 CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
2672 !children[i].isNull(), "parameter term", children[i], i)
2673 << "non-null term";
2674 }
2675 checkMkOpTerm(kind, opTerm, children.size());
2676 const CVC4::Kind int_kind = extToIntKind(kind);
2677 std::vector<Expr> echildren = termVectorToExprs(children);
2678 Term res = d_exprMgr->mkExpr(int_kind, *opTerm.d_expr, echildren);
2679 (void)res.d_expr->getType(true); /* kick off type checking */
2680 return res;
2681 }
2682 catch (const CVC4::TypeCheckingException& e)
2683 {
2684 throw CVC4ApiException(e.getMessage());
2685 }
2686 }
2687
mkTuple(const std::vector<Sort> & sorts,const std::vector<Term> & terms) const2688 Term Solver::mkTuple(const std::vector<Sort>& sorts,
2689 const std::vector<Term>& terms) const
2690 {
2691 CVC4_API_CHECK(sorts.size() == terms.size())
2692 << "Expected the same number of sorts and elements";
2693 try
2694 {
2695 std::vector<CVC4::Expr> args;
2696 for (size_t i = 0, size = sorts.size(); i < size; i++)
2697 {
2698 args.push_back(*(ensureTermSort(terms[i], sorts[i])).d_expr);
2699 }
2700
2701 Sort s = mkTupleSort(sorts);
2702 Datatype dt = s.getDatatype();
2703 Term res = d_exprMgr->mkExpr(extToIntKind(APPLY_CONSTRUCTOR),
2704 *dt[0].getConstructorTerm().d_expr,
2705 args);
2706 (void)res.d_expr->getType(true); /* kick off type checking */
2707 return res;
2708 }
2709 catch (const CVC4::TypeCheckingException& e)
2710 {
2711 throw CVC4ApiException(e.getMessage());
2712 }
2713 }
2714
termVectorToExprs(const std::vector<Term> & terms) const2715 std::vector<Expr> Solver::termVectorToExprs(
2716 const std::vector<Term>& terms) const
2717 {
2718 std::vector<Expr> res;
2719 for (const Term& t : terms)
2720 {
2721 res.push_back(*t.d_expr);
2722 }
2723 return res;
2724 }
2725
2726 /* Create operator terms */
2727 /* -------------------------------------------------------------------------- */
2728
mkOpTerm(Kind kind,Kind k)2729 OpTerm Solver::mkOpTerm(Kind kind, Kind k)
2730 {
2731 CVC4_API_KIND_CHECK_EXPECTED(kind == CHAIN_OP, kind) << "CHAIN_OP";
2732 return *mkConstHelper<CVC4::Chain>(CVC4::Chain(extToIntKind(k))).d_expr.get();
2733 }
2734
mkOpTerm(Kind kind,const std::string & arg)2735 OpTerm Solver::mkOpTerm(Kind kind, const std::string& arg)
2736 {
2737 CVC4_API_KIND_CHECK_EXPECTED(kind == RECORD_UPDATE_OP, kind)
2738 << "RECORD_UPDATE_OP";
2739 return *mkConstHelper<CVC4::RecordUpdate>(CVC4::RecordUpdate(arg))
2740 .d_expr.get();
2741 }
2742
mkOpTerm(Kind kind,uint32_t arg)2743 OpTerm Solver::mkOpTerm(Kind kind, uint32_t arg)
2744 {
2745 CVC4_API_KIND_CHECK(kind);
2746 OpTerm res;
2747 switch (kind)
2748 {
2749 case DIVISIBLE_OP:
2750 res = *mkConstHelper<CVC4::Divisible>(CVC4::Divisible(arg)).d_expr.get();
2751 break;
2752 case BITVECTOR_REPEAT_OP:
2753 res = *mkConstHelper<CVC4::BitVectorRepeat>(CVC4::BitVectorRepeat(arg))
2754 .d_expr.get();
2755 break;
2756 case BITVECTOR_ZERO_EXTEND_OP:
2757 res = *mkConstHelper<CVC4::BitVectorZeroExtend>(
2758 CVC4::BitVectorZeroExtend(arg))
2759 .d_expr.get();
2760 break;
2761 case BITVECTOR_SIGN_EXTEND_OP:
2762 res = *mkConstHelper<CVC4::BitVectorSignExtend>(
2763 CVC4::BitVectorSignExtend(arg))
2764 .d_expr.get();
2765 break;
2766 case BITVECTOR_ROTATE_LEFT_OP:
2767 res = *mkConstHelper<CVC4::BitVectorRotateLeft>(
2768 CVC4::BitVectorRotateLeft(arg))
2769 .d_expr.get();
2770 break;
2771 case BITVECTOR_ROTATE_RIGHT_OP:
2772 res = *mkConstHelper<CVC4::BitVectorRotateRight>(
2773 CVC4::BitVectorRotateRight(arg))
2774 .d_expr.get();
2775 break;
2776 case INT_TO_BITVECTOR_OP:
2777 res = *mkConstHelper<CVC4::IntToBitVector>(CVC4::IntToBitVector(arg))
2778 .d_expr.get();
2779 break;
2780 case FLOATINGPOINT_TO_UBV_OP:
2781 res = *mkConstHelper<CVC4::FloatingPointToUBV>(
2782 CVC4::FloatingPointToUBV(arg))
2783 .d_expr.get();
2784 break;
2785 case FLOATINGPOINT_TO_UBV_TOTAL_OP:
2786 res = *mkConstHelper<CVC4::FloatingPointToUBVTotal>(
2787 CVC4::FloatingPointToUBVTotal(arg))
2788 .d_expr.get();
2789 break;
2790 case FLOATINGPOINT_TO_SBV_OP:
2791 res = *mkConstHelper<CVC4::FloatingPointToSBV>(
2792 CVC4::FloatingPointToSBV(arg))
2793 .d_expr.get();
2794 break;
2795 case FLOATINGPOINT_TO_SBV_TOTAL_OP:
2796 res = *mkConstHelper<CVC4::FloatingPointToSBVTotal>(
2797 CVC4::FloatingPointToSBVTotal(arg))
2798 .d_expr.get();
2799 break;
2800 case TUPLE_UPDATE_OP:
2801 res = *mkConstHelper<CVC4::TupleUpdate>(CVC4::TupleUpdate(arg))
2802 .d_expr.get();
2803 break;
2804 default:
2805 CVC4_API_KIND_CHECK_EXPECTED(false, kind)
2806 << "operator kind with uint32_t argument";
2807 }
2808 Assert(!res.isNull());
2809 return res;
2810 }
2811
mkOpTerm(Kind kind,uint32_t arg1,uint32_t arg2)2812 OpTerm Solver::mkOpTerm(Kind kind, uint32_t arg1, uint32_t arg2)
2813 {
2814 CVC4_API_KIND_CHECK(kind);
2815 OpTerm res;
2816 switch (kind)
2817 {
2818 case BITVECTOR_EXTRACT_OP:
2819 res = *mkConstHelper<CVC4::BitVectorExtract>(
2820 CVC4::BitVectorExtract(arg1, arg2))
2821 .d_expr.get();
2822 break;
2823 case FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP:
2824 res = *mkConstHelper<CVC4::FloatingPointToFPIEEEBitVector>(
2825 CVC4::FloatingPointToFPIEEEBitVector(arg1, arg2))
2826 .d_expr.get();
2827 break;
2828 case FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP:
2829 res = *mkConstHelper<CVC4::FloatingPointToFPFloatingPoint>(
2830 CVC4::FloatingPointToFPFloatingPoint(arg1, arg2))
2831 .d_expr.get();
2832 break;
2833 case FLOATINGPOINT_TO_FP_REAL_OP:
2834 res = *mkConstHelper<CVC4::FloatingPointToFPReal>(
2835 CVC4::FloatingPointToFPReal(arg1, arg2))
2836 .d_expr.get();
2837 break;
2838 case FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP:
2839 res = *mkConstHelper<CVC4::FloatingPointToFPSignedBitVector>(
2840 CVC4::FloatingPointToFPSignedBitVector(arg1, arg2))
2841 .d_expr.get();
2842 break;
2843 case FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP:
2844 res = *mkConstHelper<CVC4::FloatingPointToFPUnsignedBitVector>(
2845 CVC4::FloatingPointToFPUnsignedBitVector(arg1, arg2))
2846 .d_expr.get();
2847 break;
2848 case FLOATINGPOINT_TO_FP_GENERIC_OP:
2849 res = *mkConstHelper<CVC4::FloatingPointToFPGeneric>(
2850 CVC4::FloatingPointToFPGeneric(arg1, arg2))
2851 .d_expr.get();
2852 break;
2853 default:
2854 CVC4_API_KIND_CHECK_EXPECTED(false, kind)
2855 << "operator kind with two uint32_t arguments";
2856 }
2857 Assert(!res.isNull());
2858 return res;
2859 }
2860
2861 /* Non-SMT-LIB commands */
2862 /* -------------------------------------------------------------------------- */
2863
simplify(const Term & t)2864 Term Solver::simplify(const Term& t)
2865 {
2866 return d_smtEngine->simplify(*t.d_expr);
2867 }
2868
checkValid(void) const2869 Result Solver::checkValid(void) const
2870 {
2871 // CHECK:
2872 // if d_queryMade -> incremental enabled
2873 CVC4::Result r = d_smtEngine->query();
2874 return Result(r);
2875 }
2876
checkValidAssuming(Term assumption) const2877 Result Solver::checkValidAssuming(Term assumption) const
2878 {
2879 // CHECK:
2880 // if assumptions.size() > 0: incremental enabled?
2881 CVC4::Result r = d_smtEngine->query(*assumption.d_expr);
2882 return Result(r);
2883 }
2884
checkValidAssuming(const std::vector<Term> & assumptions) const2885 Result Solver::checkValidAssuming(const std::vector<Term>& assumptions) const
2886 {
2887 // CHECK:
2888 // if assumptions.size() > 0: incremental enabled?
2889 std::vector<Expr> eassumptions = termVectorToExprs(assumptions);
2890 CVC4::Result r = d_smtEngine->query(eassumptions);
2891 return Result(r);
2892 }
2893
2894 /* SMT-LIB commands */
2895 /* -------------------------------------------------------------------------- */
2896
2897 /**
2898 * ( assert <term> )
2899 */
assertFormula(Term term) const2900 void Solver::assertFormula(Term term) const
2901 {
2902 // CHECK:
2903 // NodeManager::fromExprManager(d_exprMgr)
2904 // == NodeManager::fromExprManager(expr.getExprManager())
2905 d_smtEngine->assertFormula(*term.d_expr);
2906 }
2907
2908 /**
2909 * ( check-sat )
2910 */
checkSat(void) const2911 Result Solver::checkSat(void) const
2912 {
2913 // CHECK:
2914 // if d_queryMade -> incremental enabled
2915 CVC4::Result r = d_smtEngine->checkSat();
2916 return Result(r);
2917 }
2918
2919 /**
2920 * ( check-sat-assuming ( <prop_literal> ) )
2921 */
checkSatAssuming(Term assumption) const2922 Result Solver::checkSatAssuming(Term assumption) const
2923 {
2924 // CHECK:
2925 // if assumptions.size() > 0: incremental enabled?
2926 CVC4::Result r = d_smtEngine->checkSat(*assumption.d_expr);
2927 return Result(r);
2928 }
2929
2930 /**
2931 * ( check-sat-assuming ( <prop_literal>* ) )
2932 */
checkSatAssuming(const std::vector<Term> & assumptions) const2933 Result Solver::checkSatAssuming(const std::vector<Term>& assumptions) const
2934 {
2935 // CHECK:
2936 // if assumptions.size() > 0: incremental enabled?
2937 std::vector<Expr> eassumptions = termVectorToExprs(assumptions);
2938 CVC4::Result r = d_smtEngine->checkSat(eassumptions);
2939 return Result(r);
2940 }
2941
2942 /**
2943 * ( declare-const <symbol> <sort> )
2944 */
declareConst(const std::string & symbol,Sort sort) const2945 Term Solver::declareConst(const std::string& symbol, Sort sort) const
2946 {
2947 try
2948 {
2949 CVC4_API_ARG_CHECK_EXPECTED(!sort.isNull(), sort) << "non-null sort";
2950 Term res = d_exprMgr->mkVar(symbol, *sort.d_type);
2951 (void)res.d_expr->getType(true); /* kick off type checking */
2952 return res;
2953 }
2954 catch (const CVC4::TypeCheckingException& e)
2955 {
2956 throw CVC4ApiException(e.getMessage());
2957 }
2958 }
2959
2960 /**
2961 * ( declare-datatype <symbol> <datatype_decl> )
2962 */
declareDatatype(const std::string & symbol,const std::vector<DatatypeConstructorDecl> & ctors) const2963 Sort Solver::declareDatatype(
2964 const std::string& symbol,
2965 const std::vector<DatatypeConstructorDecl>& ctors) const
2966 {
2967 CVC4_API_ARG_CHECK_EXPECTED(ctors.size() > 0, ctors)
2968 << "a datatype declaration with at least one constructor";
2969 DatatypeDecl dtdecl(symbol);
2970 for (const DatatypeConstructorDecl& ctor : ctors)
2971 {
2972 dtdecl.addConstructor(ctor);
2973 }
2974 return d_exprMgr->mkDatatypeType(*dtdecl.d_dtype);
2975 }
2976
2977 /**
2978 * ( declare-fun <symbol> ( <sort>* ) <sort> )
2979 */
declareFun(const std::string & symbol,const std::vector<Sort> & sorts,Sort sort) const2980 Term Solver::declareFun(const std::string& symbol,
2981 const std::vector<Sort>& sorts,
2982 Sort sort) const
2983 {
2984 for (size_t i = 0, size = sorts.size(); i < size; ++i)
2985 {
2986 CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
2987 sorts[i].isFirstClass(), "parameter sort", sorts[i], i)
2988 << "first-class sort as parameter sort for function sort";
2989 }
2990 CVC4_API_ARG_CHECK_EXPECTED(sort.isFirstClass(), sort)
2991 << "first-class sort as function codomain sort";
2992 Assert(!sort.isFunction()); /* A function sort is not first-class. */
2993 Type type = *sort.d_type;
2994 if (!sorts.empty())
2995 {
2996 std::vector<Type> types = sortVectorToTypes(sorts);
2997 type = d_exprMgr->mkFunctionType(types, type);
2998 }
2999 return d_exprMgr->mkVar(symbol, type);
3000 }
3001
3002 /**
3003 * ( declare-sort <symbol> <numeral> )
3004 */
declareSort(const std::string & symbol,uint32_t arity) const3005 Sort Solver::declareSort(const std::string& symbol, uint32_t arity) const
3006 {
3007 if (arity == 0) return d_exprMgr->mkSort(symbol);
3008 return d_exprMgr->mkSortConstructor(symbol, arity);
3009 }
3010
3011 /**
3012 * ( define-fun <function_def> )
3013 */
defineFun(const std::string & symbol,const std::vector<Term> & bound_vars,Sort sort,Term term) const3014 Term Solver::defineFun(const std::string& symbol,
3015 const std::vector<Term>& bound_vars,
3016 Sort sort,
3017 Term term) const
3018 {
3019 // CHECK:
3020 // for bv in bound_vars:
3021 // NodeManager::fromExprManager(d_exprMgr)
3022 // == NodeManager::fromExprManager(bv.getExprManager())
3023 // NodeManager::fromExprManager(d_exprMgr)
3024 // == NodeManager::fromExprManager(expr.getExprManager())
3025 // CHECK: not recursive
3026 CVC4_API_ARG_CHECK_EXPECTED(sort.isFirstClass(), sort)
3027 << "first-class sort as codomain sort for function sort";
3028 // CHECK:
3029 // for v in bound_vars: is bound var
3030 std::vector<Type> domain_types;
3031 for (size_t i = 0, size = bound_vars.size(); i < size; ++i)
3032 {
3033 CVC4::Type t = bound_vars[i].d_expr->getType();
3034 CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
3035 t.isFirstClass(), "sort of parameter", bound_vars[i], i)
3036 << "first-class sort of parameter of defined function";
3037 domain_types.push_back(t);
3038 }
3039 CVC4_API_CHECK(sort == term.getSort())
3040 << "Invalid sort of function body '" << term << "', expected '" << sort
3041 << "'";
3042 Type type = *sort.d_type;
3043 if (!domain_types.empty())
3044 {
3045 type = d_exprMgr->mkFunctionType(domain_types, type);
3046 }
3047 Expr fun = d_exprMgr->mkVar(symbol, type);
3048 std::vector<Expr> ebound_vars = termVectorToExprs(bound_vars);
3049 d_smtEngine->defineFunction(fun, ebound_vars, *term.d_expr);
3050 return fun;
3051 }
3052
defineFun(Term fun,const std::vector<Term> & bound_vars,Term term) const3053 Term Solver::defineFun(Term fun,
3054 const std::vector<Term>& bound_vars,
3055 Term term) const
3056 {
3057 // CHECK:
3058 // NodeManager::fromExprManager(d_exprMgr)
3059 // == NodeManager::fromExprManager(bv.getExprManager())
3060 // NodeManager::fromExprManager(d_exprMgr)
3061 // == NodeManager::fromExprManager(expr.getExprManager())
3062 CVC4_API_ARG_CHECK_EXPECTED(fun.getSort().isFunction(), fun) << "function";
3063 std::vector<Sort> domain_sorts = fun.getSort().getFunctionDomainSorts();
3064 size_t size = bound_vars.size();
3065 CVC4_API_ARG_SIZE_CHECK_EXPECTED(size == domain_sorts.size(), bound_vars)
3066 << "'" << domain_sorts.size() << "'";
3067 for (size_t i = 0; i < size; ++i)
3068 {
3069 CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
3070 domain_sorts[i] == bound_vars[i].getSort(),
3071 "sort of parameter",
3072 bound_vars[i],
3073 i)
3074 << "'" << domain_sorts[i] << "'";
3075 }
3076 Sort codomain = fun.getSort().getFunctionCodomainSort();
3077 CVC4_API_CHECK(codomain == term.getSort())
3078 << "Invalid sort of function body '" << term << "', expected '"
3079 << codomain << "'";
3080
3081 // CHECK: not recursive
3082 // CHECK:
3083 // for v in bound_vars: is bound var
3084 std::vector<Expr> ebound_vars = termVectorToExprs(bound_vars);
3085 d_smtEngine->defineFunction(*fun.d_expr, ebound_vars, *term.d_expr);
3086 return fun;
3087 }
3088
3089 /**
3090 * ( define-fun-rec <function_def> )
3091 */
defineFunRec(const std::string & symbol,const std::vector<Term> & bound_vars,Sort sort,Term term) const3092 Term Solver::defineFunRec(const std::string& symbol,
3093 const std::vector<Term>& bound_vars,
3094 Sort sort,
3095 Term term) const
3096 {
3097 // CHECK:
3098 // for bv in bound_vars:
3099 // NodeManager::fromExprManager(d_exprMgr)
3100 // == NodeManager::fromExprManager(bv.getExprManager())
3101 // NodeManager::fromExprManager(d_exprMgr)
3102 // == NodeManager::fromExprManager(expr.getExprManager())
3103 CVC4_API_ARG_CHECK_EXPECTED(sort.isFirstClass(), sort)
3104 << "first-class sort as function codomain sort";
3105 Assert(!sort.isFunction()); /* A function sort is not first-class. */
3106 // CHECK:
3107 // for v in bound_vars: is bound var
3108 std::vector<Type> domain_types;
3109 for (size_t i = 0, size = bound_vars.size(); i < size; ++i)
3110 {
3111 CVC4::Type t = bound_vars[i].d_expr->getType();
3112 CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
3113 t.isFirstClass(), "sort of parameter", bound_vars[i], i)
3114 << "first-class sort of parameter of defined function";
3115 domain_types.push_back(t);
3116 }
3117 CVC4_API_CHECK(sort == term.getSort())
3118 << "Invalid sort of function body '" << term << "', expected '" << sort
3119 << "'";
3120 Type type = *sort.d_type;
3121 if (!domain_types.empty())
3122 {
3123 type = d_exprMgr->mkFunctionType(domain_types, type);
3124 }
3125 Expr fun = d_exprMgr->mkVar(symbol, type);
3126 std::vector<Expr> ebound_vars = termVectorToExprs(bound_vars);
3127 d_smtEngine->defineFunctionRec(fun, ebound_vars, *term.d_expr);
3128 return fun;
3129 }
3130
defineFunRec(Term fun,const std::vector<Term> & bound_vars,Term term) const3131 Term Solver::defineFunRec(Term fun,
3132 const std::vector<Term>& bound_vars,
3133 Term term) const
3134 {
3135 // CHECK:
3136 // for bv in bound_vars:
3137 // NodeManager::fromExprManager(d_exprMgr)
3138 // == NodeManager::fromExprManager(bv.getExprManager())
3139 // NodeManager::fromExprManager(d_exprMgr)
3140 // == NodeManager::fromExprManager(expr.getExprManager())
3141 CVC4_API_ARG_CHECK_EXPECTED(fun.getSort().isFunction(), fun) << "function";
3142 std::vector<Sort> domain_sorts = fun.getSort().getFunctionDomainSorts();
3143 size_t size = bound_vars.size();
3144 CVC4_API_ARG_SIZE_CHECK_EXPECTED(size == domain_sorts.size(), bound_vars)
3145 << "'" << domain_sorts.size() << "'";
3146 for (size_t i = 0; i < size; ++i)
3147 {
3148 CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
3149 domain_sorts[i] == bound_vars[i].getSort(),
3150 "sort of parameter",
3151 bound_vars[i],
3152 i)
3153 << "'" << domain_sorts[i] << "'";
3154 }
3155 Sort codomain = fun.getSort().getFunctionCodomainSort();
3156 CVC4_API_CHECK(codomain == term.getSort())
3157 << "Invalid sort of function body '" << term << "', expected '"
3158 << codomain << "'";
3159 // CHECK:
3160 // for v in bound_vars: is bound var
3161 std::vector<Expr> ebound_vars = termVectorToExprs(bound_vars);
3162 d_smtEngine->defineFunctionRec(*fun.d_expr, ebound_vars, *term.d_expr);
3163 return fun;
3164 }
3165
3166 /**
3167 * ( define-funs-rec ( <function_decl>^{n+1} ) ( <term>^{n+1} ) )
3168 */
defineFunsRec(const std::vector<Term> & funs,const std::vector<std::vector<Term>> & bound_vars,const std::vector<Term> & terms) const3169 void Solver::defineFunsRec(const std::vector<Term>& funs,
3170 const std::vector<std::vector<Term>>& bound_vars,
3171 const std::vector<Term>& terms) const
3172 {
3173 // CHECK:
3174 // for f in funs:
3175 // NodeManager::fromExprManager(d_exprMgr)
3176 // == NodeManager::fromExprManager(f.getExprManager())
3177 // for bv in bound_vars:
3178 // NodeManager::fromExprManager(d_exprMgr)
3179 // == NodeManager::fromExprManager(bv.getExprManager())
3180 // NodeManager::fromExprManager(d_exprMgr)
3181 // == NodeManager::fromExprManager(expr.getExprManager())
3182 size_t funs_size = funs.size();
3183 CVC4_API_ARG_SIZE_CHECK_EXPECTED(funs_size == bound_vars.size(), bound_vars)
3184 << "'" << funs_size << "'";
3185 for (size_t j = 0; j < funs_size; ++j)
3186 {
3187 const Term& fun = funs[j];
3188 const std::vector<Term>& bvars = bound_vars[j];
3189 const Term& term = terms[j];
3190
3191 CVC4_API_ARG_CHECK_EXPECTED(fun.getSort().isFunction(), fun) << "function";
3192 std::vector<Sort> domain_sorts = fun.getSort().getFunctionDomainSorts();
3193 size_t size = bvars.size();
3194 CVC4_API_ARG_SIZE_CHECK_EXPECTED(size == domain_sorts.size(), bvars)
3195 << "'" << domain_sorts.size() << "'";
3196 for (size_t i = 0; i < size; ++i)
3197 {
3198 CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
3199 domain_sorts[i] == bvars[i].getSort(),
3200 "sort of parameter",
3201 bvars[i],
3202 i)
3203 << "'" << domain_sorts[i] << "' in parameter bound_vars[" << j << "]";
3204 }
3205 Sort codomain = fun.getSort().getFunctionCodomainSort();
3206 CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
3207 codomain == term.getSort(), "sort of function body", term, j)
3208 << "'" << codomain << "'";
3209 }
3210 // CHECK:
3211 // for bv in bound_vars (for v in bv): is bound var
3212 std::vector<Expr> efuns = termVectorToExprs(funs);
3213 std::vector<std::vector<Expr>> ebound_vars;
3214 for (const auto& v : bound_vars)
3215 {
3216 ebound_vars.push_back(termVectorToExprs(v));
3217 }
3218 std::vector<Expr> exprs = termVectorToExprs(terms);
3219 d_smtEngine->defineFunctionsRec(efuns, ebound_vars, exprs);
3220 }
3221
3222 /**
3223 * ( echo <std::string> )
3224 */
echo(std::ostream & out,const std::string & str) const3225 void Solver::echo(std::ostream& out, const std::string& str) const
3226 {
3227 out << str;
3228 }
3229
3230 /**
3231 * ( get-assertions )
3232 */
getAssertions(void) const3233 std::vector<Term> Solver::getAssertions(void) const
3234 {
3235 std::vector<Expr> assertions = d_smtEngine->getAssertions();
3236 /* Can not use
3237 * return std::vector<Term>(assertions.begin(), assertions.end());
3238 * here since constructor is private */
3239 std::vector<Term> res;
3240 for (const Expr& e : assertions)
3241 {
3242 res.push_back(Term(e));
3243 }
3244 return res;
3245 }
3246
3247 /**
3248 * ( get-assignment )
3249 */
getAssignment(void) const3250 std::vector<std::pair<Term, Term>> Solver::getAssignment(void) const
3251 {
3252 // CHECK: produce-models set
3253 // CHECK: result sat
3254 std::vector<std::pair<Expr, Expr>> assignment = d_smtEngine->getAssignment();
3255 std::vector<std::pair<Term, Term>> res;
3256 for (const auto& p : assignment)
3257 {
3258 res.emplace_back(Term(p.first), Term(p.second));
3259 }
3260 return res;
3261 }
3262
3263 /**
3264 * ( get-info <info_flag> )
3265 */
getInfo(const std::string & flag) const3266 std::string Solver::getInfo(const std::string& flag) const
3267 {
3268 // CHECK: flag valid?
3269 return d_smtEngine->getInfo(flag).toString();
3270 }
3271
3272 /**
3273 * ( get-option <keyword> )
3274 */
getOption(const std::string & option) const3275 std::string Solver::getOption(const std::string& option) const
3276 {
3277 // CHECK: option exists?
3278 SExpr res = d_smtEngine->getOption(option);
3279 return res.toString();
3280 }
3281
3282 /**
3283 * ( get-unsat-assumptions )
3284 */
getUnsatAssumptions(void) const3285 std::vector<Term> Solver::getUnsatAssumptions(void) const
3286 {
3287 // CHECK: incremental?
3288 // CHECK: option produce-unsat-assumptions set?
3289 // CHECK: last check sat/valid result is unsat/invalid
3290 std::vector<Expr> uassumptions = d_smtEngine->getUnsatAssumptions();
3291 /* Can not use
3292 * return std::vector<Term>(uassumptions.begin(), uassumptions.end());
3293 * here since constructor is private */
3294 std::vector<Term> res;
3295 for (const Expr& e : uassumptions)
3296 {
3297 res.push_back(Term(e));
3298 }
3299 return res;
3300 }
3301
3302 /**
3303 * ( get-unsat-core )
3304 */
getUnsatCore(void) const3305 std::vector<Term> Solver::getUnsatCore(void) const
3306 {
3307 // CHECK: result unsat?
3308 UnsatCore core = d_smtEngine->getUnsatCore();
3309 /* Can not use
3310 * return std::vector<Term>(core.begin(), core.end());
3311 * here since constructor is private */
3312 std::vector<Term> res;
3313 for (const Expr& e : core)
3314 {
3315 res.push_back(Term(e));
3316 }
3317 return res;
3318 }
3319
3320 /**
3321 * ( get-value ( <term> ) )
3322 */
getValue(Term term) const3323 Term Solver::getValue(Term term) const
3324 {
3325 // CHECK:
3326 // NodeManager::fromExprManager(d_exprMgr)
3327 // == NodeManager::fromExprManager(expr.getExprManager())
3328 return d_smtEngine->getValue(*term.d_expr);
3329 }
3330
3331 /**
3332 * ( get-value ( <term>+ ) )
3333 */
getValue(const std::vector<Term> & terms) const3334 std::vector<Term> Solver::getValue(const std::vector<Term>& terms) const
3335 {
3336 // CHECK:
3337 // for e in exprs:
3338 // NodeManager::fromExprManager(d_exprMgr)
3339 // == NodeManager::fromExprManager(e.getExprManager())
3340 std::vector<Term> res;
3341 for (const Term& t : terms)
3342 {
3343 /* Can not use emplace_back here since constructor is private. */
3344 res.push_back(Term(d_smtEngine->getValue(*t.d_expr)));
3345 }
3346 return res;
3347 }
3348
3349 /**
3350 * ( pop <numeral> )
3351 */
pop(uint32_t nscopes) const3352 void Solver::pop(uint32_t nscopes) const
3353 {
3354 // CHECK: incremental enabled?
3355 // CHECK: nscopes <= d_smtEngine->d_userLevels.size()
3356 for (uint32_t n = 0; n < nscopes; ++n)
3357 {
3358 d_smtEngine->pop();
3359 }
3360 }
3361
printModel(std::ostream & out) const3362 void Solver::printModel(std::ostream& out) const
3363 {
3364 // CHECK: produce-models?
3365 out << *d_smtEngine->getModel();
3366 }
3367
3368 /**
3369 * ( push <numeral> )
3370 */
push(uint32_t nscopes) const3371 void Solver::push(uint32_t nscopes) const
3372 {
3373 // CHECK: incremental enabled?
3374 for (uint32_t n = 0; n < nscopes; ++n)
3375 {
3376 d_smtEngine->push();
3377 }
3378 }
3379
3380 /**
3381 * ( reset )
3382 */
reset(void) const3383 void Solver::reset(void) const { d_smtEngine->reset(); }
3384
3385 /**
3386 * ( reset-assertions )
3387 */
resetAssertions(void) const3388 void Solver::resetAssertions(void) const { d_smtEngine->resetAssertions(); }
3389
3390 // TODO: issue #2781
setLogicHelper(const std::string & logic) const3391 void Solver::setLogicHelper(const std::string& logic) const
3392 {
3393 CVC4_API_CHECK(!d_smtEngine->isFullyInited())
3394 << "Invalid call to 'setLogic', solver is already fully initialized";
3395 try
3396 {
3397 CVC4::LogicInfo logic_info(logic);
3398 d_smtEngine->setLogic(logic_info);
3399 }
3400 catch (CVC4::IllegalArgumentException& e)
3401 {
3402 throw CVC4ApiException(e.getMessage());
3403 }
3404 }
3405
3406 /**
3407 * ( set-info <attribute> )
3408 */
setInfo(const std::string & keyword,const std::string & value) const3409 void Solver::setInfo(const std::string& keyword, const std::string& value) const
3410 {
3411 bool is_cvc4_keyword = false;
3412
3413 /* Check for CVC4-specific info keys (prefixed with "cvc4-" or "cvc4_") */
3414 if (keyword.length() > 5)
3415 {
3416 std::string prefix = keyword.substr(0, 5);
3417 if (prefix == "cvc4-" || prefix == "cvc4_")
3418 {
3419 is_cvc4_keyword = true;
3420 std::string cvc4key = keyword.substr(5);
3421 CVC4_API_ARG_CHECK_EXPECTED(cvc4key == "logic", keyword)
3422 << "keyword 'cvc4-logic'";
3423 setLogicHelper(value);
3424 }
3425 }
3426 if (!is_cvc4_keyword)
3427 {
3428 CVC4_API_ARG_CHECK_EXPECTED(
3429 keyword == "source" || keyword == "category" || keyword == "difficulty"
3430 || keyword == "filename" || keyword == "license"
3431 || keyword == "name" || keyword == "notes"
3432 || keyword == "smt-lib-version" || keyword == "status",
3433 keyword)
3434 << "'source', 'category', 'difficulty', 'filename', 'license', 'name', "
3435 "'notes', 'smt-lib-version' or 'status'";
3436 CVC4_API_ARG_CHECK_EXPECTED(keyword != "smt-lib-version" || value == "2"
3437 || value == "2.0" || value == "2.5"
3438 || value == "2.6" || value == "2.6.1",
3439 value)
3440 << "'2.0', '2.5', '2.6' or '2.6.1'";
3441 CVC4_API_ARG_CHECK_EXPECTED(keyword != "status" || value == "sat"
3442 || value == "unsat" || value == "unknown",
3443 value)
3444 << "'sat', 'unsat' or 'unknown'";
3445 }
3446
3447 d_smtEngine->setInfo(keyword, value);
3448 }
3449
3450 /**
3451 * ( set-logic <symbol> )
3452 */
setLogic(const std::string & logic) const3453 void Solver::setLogic(const std::string& logic) const { setLogicHelper(logic); }
3454
3455 /**
3456 * ( set-option <option> )
3457 */
setOption(const std::string & option,const std::string & value) const3458 void Solver::setOption(const std::string& option,
3459 const std::string& value) const
3460 {
3461 CVC4_API_CHECK(!d_smtEngine->isFullyInited())
3462 << "Invalid call to 'setOption', solver is already fully initialized";
3463 try
3464 {
3465 d_smtEngine->setOption(option, value);
3466 }
3467 catch (CVC4::OptionException& e)
3468 {
3469 throw CVC4ApiException(e.getMessage());
3470 }
3471 }
3472
ensureTermSort(const Term & term,const Sort & sort) const3473 Term Solver::ensureTermSort(const Term& term, const Sort& sort) const
3474 {
3475 CVC4_API_CHECK(term.getSort() == sort
3476 || (term.getSort().isInteger() && sort.isReal()))
3477 << "Expected conversion from Int to Real";
3478
3479 Sort t = term.getSort();
3480 if (term.getSort() == sort)
3481 {
3482 return term;
3483 }
3484
3485 // Integers are reals, too
3486 Assert(t.isReal());
3487 Term res = term;
3488 if (t.isInteger())
3489 {
3490 // Must cast to Real to ensure correct type is passed to parametric type
3491 // constructors. We do this cast using division with 1. This has the
3492 // advantage wrt using TO_REAL since (constant) division is always included
3493 // in the theory.
3494 res = Term(d_exprMgr->mkExpr(extToIntKind(DIVISION),
3495 *res.d_expr,
3496 d_exprMgr->mkConst(CVC4::Rational(1))));
3497 }
3498 Assert(res.getSort() == sort);
3499 return res;
3500 }
3501
3502 /**
3503 * !!! This is only temporarily available until the parser is fully migrated to
3504 * the new API. !!!
3505 */
getExprManager(void) const3506 ExprManager* Solver::getExprManager(void) const { return d_exprMgr.get(); }
3507
3508 /**
3509 * !!! This is only temporarily available until the parser is fully migrated to
3510 * the new API. !!!
3511 */
getSmtEngine(void) const3512 SmtEngine* Solver::getSmtEngine(void) const { return d_smtEngine.get(); }
3513
3514 } // namespace api
3515 } // namespace CVC4
3516