1 /******************************************************************************
2 * Top contributors (to current version):
3 * Aina Niemetz, Andrew Reynolds, Andres Noetzli
5 * This file is part of the cvc5 project.
7 * Copyright (c) 2009-2021 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.
11 * ****************************************************************************
15 * A brief note on how to guard API functions:
17 * In general, we think of API guards as a fence -- they are supposed to make
18 * sure that no invalid arguments get passed into internal realms of cvc5.
19 * Thus we always want to catch such cases on the API level (and can then
20 * assert internally that no invalid argument is passed in).
22 * The only special case is when we use 3rd party back-ends we have no control
23 * over, and which throw (invalid_argument) exceptions anyways. In this case,
24 * we do not replicate argument checks but delegate them to the back-end,
25 * catch thrown exceptions, and raise a CVC5ApiException.
27 * Our Integer implementation, e.g., is such a special case since we support
28 * two different back end implementations (GMP, CLN). Be aware that they do
29 * not fully agree on what is (in)valid input, which requires extra checks for
30 * consistent behavior (see Solver::mkRealFromStrHelper for an example).
33 #include "api/cpp/cvc5.h"
38 #include "api/cpp/cvc5_checks.h"
39 #include "base/check.h"
40 #include "base/configuration.h"
41 #include "base/modal_exception.h"
42 #include "expr/array_store_all.h"
43 #include "expr/ascription_type.h"
44 #include "expr/dtype.h"
45 #include "expr/dtype_cons.h"
46 #include "expr/dtype_selector.h"
47 #include "expr/emptybag.h"
48 #include "expr/emptyset.h"
49 #include "expr/kind.h"
50 #include "expr/metakind.h"
51 #include "expr/node.h"
52 #include "expr/node_algorithm.h"
53 #include "expr/node_builder.h"
54 #include "expr/node_manager.h"
55 #include "expr/sequence.h"
56 #include "expr/type_node.h"
57 #include "expr/uninterpreted_constant.h"
58 #include "options/base_options.h"
59 #include "options/main_options.h"
60 #include "options/option_exception.h"
61 #include "options/options.h"
62 #include "options/options_public.h"
63 #include "options/smt_options.h"
64 #include "proof/unsat_core.h"
65 #include "smt/model.h"
66 #include "smt/smt_engine.h"
67 #include "smt/smt_mode.h"
68 #include "theory/datatypes/tuple_project_op.h"
69 #include "theory/logic_info.h"
70 #include "theory/theory_model.h"
71 #include "util/abstract_value.h"
72 #include "util/bitvector.h"
73 #include "util/divisible.h"
74 #include "util/floatingpoint.h"
75 #include "util/iand.h"
76 #include "util/random.h"
77 #include "util/regexp.h"
78 #include "util/result.h"
79 #include "util/roundingmode.h"
80 #include "util/statistics_registry.h"
81 #include "util/statistics_stats.h"
82 #include "util/statistics_value.h"
83 #include "util/string.h"
84 #include "util/utility.h"
89 /* -------------------------------------------------------------------------- */
91 /* -------------------------------------------------------------------------- */
95 HistogramStat
<TypeConstant
> d_consts
;
96 HistogramStat
<TypeConstant
> d_vars
;
97 HistogramStat
<Kind
> d_terms
;
100 /* -------------------------------------------------------------------------- */
102 /* -------------------------------------------------------------------------- */
104 /* Mapping from external (API) kind to internal kind. */
105 const static std::unordered_map
<Kind
, cvc5::Kind
> s_kinds
{
106 {INTERNAL_KIND
, cvc5::Kind::UNDEFINED_KIND
},
107 {UNDEFINED_KIND
, cvc5::Kind::UNDEFINED_KIND
},
108 {NULL_EXPR
, cvc5::Kind::NULL_EXPR
},
109 /* Builtin ------------------------------------------------------------- */
110 {UNINTERPRETED_CONSTANT
, cvc5::Kind::UNINTERPRETED_CONSTANT
},
111 {ABSTRACT_VALUE
, cvc5::Kind::ABSTRACT_VALUE
},
112 {EQUAL
, cvc5::Kind::EQUAL
},
113 {DISTINCT
, cvc5::Kind::DISTINCT
},
114 {CONSTANT
, cvc5::Kind::VARIABLE
},
115 {VARIABLE
, cvc5::Kind::BOUND_VARIABLE
},
116 {SEXPR
, cvc5::Kind::SEXPR
},
117 {LAMBDA
, cvc5::Kind::LAMBDA
},
118 {WITNESS
, cvc5::Kind::WITNESS
},
119 /* Boolean ------------------------------------------------------------- */
120 {CONST_BOOLEAN
, cvc5::Kind::CONST_BOOLEAN
},
121 {NOT
, cvc5::Kind::NOT
},
122 {AND
, cvc5::Kind::AND
},
123 {IMPLIES
, cvc5::Kind::IMPLIES
},
124 {OR
, cvc5::Kind::OR
},
125 {XOR
, cvc5::Kind::XOR
},
126 {ITE
, cvc5::Kind::ITE
},
127 {MATCH
, cvc5::Kind::MATCH
},
128 {MATCH_CASE
, cvc5::Kind::MATCH_CASE
},
129 {MATCH_BIND_CASE
, cvc5::Kind::MATCH_BIND_CASE
},
130 /* UF ------------------------------------------------------------------ */
131 {APPLY_UF
, cvc5::Kind::APPLY_UF
},
132 {CARDINALITY_CONSTRAINT
, cvc5::Kind::CARDINALITY_CONSTRAINT
},
133 {CARDINALITY_VALUE
, cvc5::Kind::CARDINALITY_VALUE
},
134 {HO_APPLY
, cvc5::Kind::HO_APPLY
},
135 /* Arithmetic ---------------------------------------------------------- */
136 {PLUS
, cvc5::Kind::PLUS
},
137 {MULT
, cvc5::Kind::MULT
},
138 {IAND
, cvc5::Kind::IAND
},
139 {POW2
, cvc5::Kind::POW2
},
140 {MINUS
, cvc5::Kind::MINUS
},
141 {UMINUS
, cvc5::Kind::UMINUS
},
142 {DIVISION
, cvc5::Kind::DIVISION
},
143 {INTS_DIVISION
, cvc5::Kind::INTS_DIVISION
},
144 {INTS_MODULUS
, cvc5::Kind::INTS_MODULUS
},
145 {ABS
, cvc5::Kind::ABS
},
146 {DIVISIBLE
, cvc5::Kind::DIVISIBLE
},
147 {POW
, cvc5::Kind::POW
},
148 {EXPONENTIAL
, cvc5::Kind::EXPONENTIAL
},
149 {SINE
, cvc5::Kind::SINE
},
150 {COSINE
, cvc5::Kind::COSINE
},
151 {TANGENT
, cvc5::Kind::TANGENT
},
152 {COSECANT
, cvc5::Kind::COSECANT
},
153 {SECANT
, cvc5::Kind::SECANT
},
154 {COTANGENT
, cvc5::Kind::COTANGENT
},
155 {ARCSINE
, cvc5::Kind::ARCSINE
},
156 {ARCCOSINE
, cvc5::Kind::ARCCOSINE
},
157 {ARCTANGENT
, cvc5::Kind::ARCTANGENT
},
158 {ARCCOSECANT
, cvc5::Kind::ARCCOSECANT
},
159 {ARCSECANT
, cvc5::Kind::ARCSECANT
},
160 {ARCCOTANGENT
, cvc5::Kind::ARCCOTANGENT
},
161 {SQRT
, cvc5::Kind::SQRT
},
162 {CONST_RATIONAL
, cvc5::Kind::CONST_RATIONAL
},
163 {LT
, cvc5::Kind::LT
},
164 {LEQ
, cvc5::Kind::LEQ
},
165 {GT
, cvc5::Kind::GT
},
166 {GEQ
, cvc5::Kind::GEQ
},
167 {IS_INTEGER
, cvc5::Kind::IS_INTEGER
},
168 {TO_INTEGER
, cvc5::Kind::TO_INTEGER
},
169 {TO_REAL
, cvc5::Kind::TO_REAL
},
170 {PI
, cvc5::Kind::PI
},
171 /* BV ------------------------------------------------------------------ */
172 {CONST_BITVECTOR
, cvc5::Kind::CONST_BITVECTOR
},
173 {BITVECTOR_CONCAT
, cvc5::Kind::BITVECTOR_CONCAT
},
174 {BITVECTOR_AND
, cvc5::Kind::BITVECTOR_AND
},
175 {BITVECTOR_OR
, cvc5::Kind::BITVECTOR_OR
},
176 {BITVECTOR_XOR
, cvc5::Kind::BITVECTOR_XOR
},
177 {BITVECTOR_NOT
, cvc5::Kind::BITVECTOR_NOT
},
178 {BITVECTOR_NAND
, cvc5::Kind::BITVECTOR_NAND
},
179 {BITVECTOR_NOR
, cvc5::Kind::BITVECTOR_NOR
},
180 {BITVECTOR_XNOR
, cvc5::Kind::BITVECTOR_XNOR
},
181 {BITVECTOR_COMP
, cvc5::Kind::BITVECTOR_COMP
},
182 {BITVECTOR_MULT
, cvc5::Kind::BITVECTOR_MULT
},
183 {BITVECTOR_ADD
, cvc5::Kind::BITVECTOR_ADD
},
184 {BITVECTOR_SUB
, cvc5::Kind::BITVECTOR_SUB
},
185 {BITVECTOR_NEG
, cvc5::Kind::BITVECTOR_NEG
},
186 {BITVECTOR_UDIV
, cvc5::Kind::BITVECTOR_UDIV
},
187 {BITVECTOR_UREM
, cvc5::Kind::BITVECTOR_UREM
},
188 {BITVECTOR_SDIV
, cvc5::Kind::BITVECTOR_SDIV
},
189 {BITVECTOR_SREM
, cvc5::Kind::BITVECTOR_SREM
},
190 {BITVECTOR_SMOD
, cvc5::Kind::BITVECTOR_SMOD
},
191 {BITVECTOR_SHL
, cvc5::Kind::BITVECTOR_SHL
},
192 {BITVECTOR_LSHR
, cvc5::Kind::BITVECTOR_LSHR
},
193 {BITVECTOR_ASHR
, cvc5::Kind::BITVECTOR_ASHR
},
194 {BITVECTOR_ULT
, cvc5::Kind::BITVECTOR_ULT
},
195 {BITVECTOR_ULE
, cvc5::Kind::BITVECTOR_ULE
},
196 {BITVECTOR_UGT
, cvc5::Kind::BITVECTOR_UGT
},
197 {BITVECTOR_UGE
, cvc5::Kind::BITVECTOR_UGE
},
198 {BITVECTOR_SLT
, cvc5::Kind::BITVECTOR_SLT
},
199 {BITVECTOR_SLE
, cvc5::Kind::BITVECTOR_SLE
},
200 {BITVECTOR_SGT
, cvc5::Kind::BITVECTOR_SGT
},
201 {BITVECTOR_SGE
, cvc5::Kind::BITVECTOR_SGE
},
202 {BITVECTOR_ULTBV
, cvc5::Kind::BITVECTOR_ULTBV
},
203 {BITVECTOR_SLTBV
, cvc5::Kind::BITVECTOR_SLTBV
},
204 {BITVECTOR_ITE
, cvc5::Kind::BITVECTOR_ITE
},
205 {BITVECTOR_REDOR
, cvc5::Kind::BITVECTOR_REDOR
},
206 {BITVECTOR_REDAND
, cvc5::Kind::BITVECTOR_REDAND
},
207 {BITVECTOR_EXTRACT
, cvc5::Kind::BITVECTOR_EXTRACT
},
208 {BITVECTOR_REPEAT
, cvc5::Kind::BITVECTOR_REPEAT
},
209 {BITVECTOR_ZERO_EXTEND
, cvc5::Kind::BITVECTOR_ZERO_EXTEND
},
210 {BITVECTOR_SIGN_EXTEND
, cvc5::Kind::BITVECTOR_SIGN_EXTEND
},
211 {BITVECTOR_ROTATE_LEFT
, cvc5::Kind::BITVECTOR_ROTATE_LEFT
},
212 {BITVECTOR_ROTATE_RIGHT
, cvc5::Kind::BITVECTOR_ROTATE_RIGHT
},
213 {INT_TO_BITVECTOR
, cvc5::Kind::INT_TO_BITVECTOR
},
214 {BITVECTOR_TO_NAT
, cvc5::Kind::BITVECTOR_TO_NAT
},
215 /* FP ------------------------------------------------------------------ */
216 {CONST_FLOATINGPOINT
, cvc5::Kind::CONST_FLOATINGPOINT
},
217 {CONST_ROUNDINGMODE
, cvc5::Kind::CONST_ROUNDINGMODE
},
218 {FLOATINGPOINT_FP
, cvc5::Kind::FLOATINGPOINT_FP
},
219 {FLOATINGPOINT_EQ
, cvc5::Kind::FLOATINGPOINT_EQ
},
220 {FLOATINGPOINT_ABS
, cvc5::Kind::FLOATINGPOINT_ABS
},
221 {FLOATINGPOINT_NEG
, cvc5::Kind::FLOATINGPOINT_NEG
},
222 {FLOATINGPOINT_ADD
, cvc5::Kind::FLOATINGPOINT_ADD
},
223 {FLOATINGPOINT_SUB
, cvc5::Kind::FLOATINGPOINT_SUB
},
224 {FLOATINGPOINT_MULT
, cvc5::Kind::FLOATINGPOINT_MULT
},
225 {FLOATINGPOINT_DIV
, cvc5::Kind::FLOATINGPOINT_DIV
},
226 {FLOATINGPOINT_FMA
, cvc5::Kind::FLOATINGPOINT_FMA
},
227 {FLOATINGPOINT_SQRT
, cvc5::Kind::FLOATINGPOINT_SQRT
},
228 {FLOATINGPOINT_REM
, cvc5::Kind::FLOATINGPOINT_REM
},
229 {FLOATINGPOINT_RTI
, cvc5::Kind::FLOATINGPOINT_RTI
},
230 {FLOATINGPOINT_MIN
, cvc5::Kind::FLOATINGPOINT_MIN
},
231 {FLOATINGPOINT_MAX
, cvc5::Kind::FLOATINGPOINT_MAX
},
232 {FLOATINGPOINT_LEQ
, cvc5::Kind::FLOATINGPOINT_LEQ
},
233 {FLOATINGPOINT_LT
, cvc5::Kind::FLOATINGPOINT_LT
},
234 {FLOATINGPOINT_GEQ
, cvc5::Kind::FLOATINGPOINT_GEQ
},
235 {FLOATINGPOINT_GT
, cvc5::Kind::FLOATINGPOINT_GT
},
236 {FLOATINGPOINT_ISN
, cvc5::Kind::FLOATINGPOINT_ISN
},
237 {FLOATINGPOINT_ISSN
, cvc5::Kind::FLOATINGPOINT_ISSN
},
238 {FLOATINGPOINT_ISZ
, cvc5::Kind::FLOATINGPOINT_ISZ
},
239 {FLOATINGPOINT_ISINF
, cvc5::Kind::FLOATINGPOINT_ISINF
},
240 {FLOATINGPOINT_ISNAN
, cvc5::Kind::FLOATINGPOINT_ISNAN
},
241 {FLOATINGPOINT_ISNEG
, cvc5::Kind::FLOATINGPOINT_ISNEG
},
242 {FLOATINGPOINT_ISPOS
, cvc5::Kind::FLOATINGPOINT_ISPOS
},
243 {FLOATINGPOINT_TO_FP_FLOATINGPOINT
,
244 cvc5::Kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT
},
245 {FLOATINGPOINT_TO_FP_IEEE_BITVECTOR
,
246 cvc5::Kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR
},
247 {FLOATINGPOINT_TO_FP_REAL
, cvc5::Kind::FLOATINGPOINT_TO_FP_REAL
},
248 {FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR
,
249 cvc5::Kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR
},
250 {FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR
,
251 cvc5::Kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR
},
252 {FLOATINGPOINT_TO_FP_GENERIC
, cvc5::Kind::FLOATINGPOINT_TO_FP_GENERIC
},
253 {FLOATINGPOINT_TO_UBV
, cvc5::Kind::FLOATINGPOINT_TO_UBV
},
254 {FLOATINGPOINT_TO_SBV
, cvc5::Kind::FLOATINGPOINT_TO_SBV
},
255 {FLOATINGPOINT_TO_REAL
, cvc5::Kind::FLOATINGPOINT_TO_REAL
},
256 /* Arrays -------------------------------------------------------------- */
257 {SELECT
, cvc5::Kind::SELECT
},
258 {STORE
, cvc5::Kind::STORE
},
259 {CONST_ARRAY
, cvc5::Kind::STORE_ALL
},
260 {EQ_RANGE
, cvc5::Kind::EQ_RANGE
},
261 /* Datatypes ----------------------------------------------------------- */
262 {APPLY_SELECTOR
, cvc5::Kind::APPLY_SELECTOR
},
263 {APPLY_CONSTRUCTOR
, cvc5::Kind::APPLY_CONSTRUCTOR
},
264 {APPLY_TESTER
, cvc5::Kind::APPLY_TESTER
},
265 {APPLY_UPDATER
, cvc5::Kind::APPLY_UPDATER
},
266 {DT_SIZE
, cvc5::Kind::DT_SIZE
},
267 {TUPLE_PROJECT
, cvc5::Kind::TUPLE_PROJECT
},
268 /* Separation Logic ---------------------------------------------------- */
269 {SEP_NIL
, cvc5::Kind::SEP_NIL
},
270 {SEP_EMP
, cvc5::Kind::SEP_EMP
},
271 {SEP_PTO
, cvc5::Kind::SEP_PTO
},
272 {SEP_STAR
, cvc5::Kind::SEP_STAR
},
273 {SEP_WAND
, cvc5::Kind::SEP_WAND
},
274 /* Sets ---------------------------------------------------------------- */
275 {EMPTYSET
, cvc5::Kind::EMPTYSET
},
276 {UNION
, cvc5::Kind::UNION
},
277 {INTERSECTION
, cvc5::Kind::INTERSECTION
},
278 {SETMINUS
, cvc5::Kind::SETMINUS
},
279 {SUBSET
, cvc5::Kind::SUBSET
},
280 {MEMBER
, cvc5::Kind::MEMBER
},
281 {SINGLETON
, cvc5::Kind::SINGLETON
},
282 {INSERT
, cvc5::Kind::INSERT
},
283 {CARD
, cvc5::Kind::CARD
},
284 {COMPLEMENT
, cvc5::Kind::COMPLEMENT
},
285 {UNIVERSE_SET
, cvc5::Kind::UNIVERSE_SET
},
286 {JOIN
, cvc5::Kind::JOIN
},
287 {PRODUCT
, cvc5::Kind::PRODUCT
},
288 {TRANSPOSE
, cvc5::Kind::TRANSPOSE
},
289 {TCLOSURE
, cvc5::Kind::TCLOSURE
},
290 {JOIN_IMAGE
, cvc5::Kind::JOIN_IMAGE
},
291 {IDEN
, cvc5::Kind::IDEN
},
292 {COMPREHENSION
, cvc5::Kind::COMPREHENSION
},
293 {CHOOSE
, cvc5::Kind::CHOOSE
},
294 {IS_SINGLETON
, cvc5::Kind::IS_SINGLETON
},
295 /* Bags ---------------------------------------------------------------- */
296 {UNION_MAX
, cvc5::Kind::UNION_MAX
},
297 {UNION_DISJOINT
, cvc5::Kind::UNION_DISJOINT
},
298 {INTERSECTION_MIN
, cvc5::Kind::INTERSECTION_MIN
},
299 {DIFFERENCE_SUBTRACT
, cvc5::Kind::DIFFERENCE_SUBTRACT
},
300 {DIFFERENCE_REMOVE
, cvc5::Kind::DIFFERENCE_REMOVE
},
301 {SUBBAG
, cvc5::Kind::SUBBAG
},
302 {BAG_COUNT
, cvc5::Kind::BAG_COUNT
},
303 {DUPLICATE_REMOVAL
, cvc5::Kind::DUPLICATE_REMOVAL
},
304 {MK_BAG
, cvc5::Kind::MK_BAG
},
305 {EMPTYBAG
, cvc5::Kind::EMPTYBAG
},
306 {BAG_CARD
, cvc5::Kind::BAG_CARD
},
307 {BAG_CHOOSE
, cvc5::Kind::BAG_CHOOSE
},
308 {BAG_IS_SINGLETON
, cvc5::Kind::BAG_IS_SINGLETON
},
309 {BAG_FROM_SET
, cvc5::Kind::BAG_FROM_SET
},
310 {BAG_TO_SET
, cvc5::Kind::BAG_TO_SET
},
311 /* Strings ------------------------------------------------------------- */
312 {STRING_CONCAT
, cvc5::Kind::STRING_CONCAT
},
313 {STRING_IN_REGEXP
, cvc5::Kind::STRING_IN_REGEXP
},
314 {STRING_LENGTH
, cvc5::Kind::STRING_LENGTH
},
315 {STRING_SUBSTR
, cvc5::Kind::STRING_SUBSTR
},
316 {STRING_UPDATE
, cvc5::Kind::STRING_UPDATE
},
317 {STRING_CHARAT
, cvc5::Kind::STRING_CHARAT
},
318 {STRING_CONTAINS
, cvc5::Kind::STRING_CONTAINS
},
319 {STRING_INDEXOF
, cvc5::Kind::STRING_INDEXOF
},
320 {STRING_INDEXOF_RE
, cvc5::Kind::STRING_INDEXOF_RE
},
321 {STRING_REPLACE
, cvc5::Kind::STRING_REPLACE
},
322 {STRING_REPLACE_ALL
, cvc5::Kind::STRING_REPLACE_ALL
},
323 {STRING_REPLACE_RE
, cvc5::Kind::STRING_REPLACE_RE
},
324 {STRING_REPLACE_RE_ALL
, cvc5::Kind::STRING_REPLACE_RE_ALL
},
325 {STRING_TOLOWER
, cvc5::Kind::STRING_TOLOWER
},
326 {STRING_TOUPPER
, cvc5::Kind::STRING_TOUPPER
},
327 {STRING_REV
, cvc5::Kind::STRING_REV
},
328 {STRING_FROM_CODE
, cvc5::Kind::STRING_FROM_CODE
},
329 {STRING_TO_CODE
, cvc5::Kind::STRING_TO_CODE
},
330 {STRING_LT
, cvc5::Kind::STRING_LT
},
331 {STRING_LEQ
, cvc5::Kind::STRING_LEQ
},
332 {STRING_PREFIX
, cvc5::Kind::STRING_PREFIX
},
333 {STRING_SUFFIX
, cvc5::Kind::STRING_SUFFIX
},
334 {STRING_IS_DIGIT
, cvc5::Kind::STRING_IS_DIGIT
},
335 {STRING_FROM_INT
, cvc5::Kind::STRING_ITOS
},
336 {STRING_TO_INT
, cvc5::Kind::STRING_STOI
},
337 {CONST_STRING
, cvc5::Kind::CONST_STRING
},
338 {STRING_TO_REGEXP
, cvc5::Kind::STRING_TO_REGEXP
},
339 {REGEXP_CONCAT
, cvc5::Kind::REGEXP_CONCAT
},
340 {REGEXP_UNION
, cvc5::Kind::REGEXP_UNION
},
341 {REGEXP_INTER
, cvc5::Kind::REGEXP_INTER
},
342 {REGEXP_DIFF
, cvc5::Kind::REGEXP_DIFF
},
343 {REGEXP_STAR
, cvc5::Kind::REGEXP_STAR
},
344 {REGEXP_PLUS
, cvc5::Kind::REGEXP_PLUS
},
345 {REGEXP_OPT
, cvc5::Kind::REGEXP_OPT
},
346 {REGEXP_RANGE
, cvc5::Kind::REGEXP_RANGE
},
347 {REGEXP_REPEAT
, cvc5::Kind::REGEXP_REPEAT
},
348 {REGEXP_LOOP
, cvc5::Kind::REGEXP_LOOP
},
349 {REGEXP_EMPTY
, cvc5::Kind::REGEXP_EMPTY
},
350 {REGEXP_SIGMA
, cvc5::Kind::REGEXP_SIGMA
},
351 {REGEXP_COMPLEMENT
, cvc5::Kind::REGEXP_COMPLEMENT
},
352 // maps to the same kind as the string versions
353 {SEQ_CONCAT
, cvc5::Kind::STRING_CONCAT
},
354 {SEQ_LENGTH
, cvc5::Kind::STRING_LENGTH
},
355 {SEQ_EXTRACT
, cvc5::Kind::STRING_SUBSTR
},
356 {SEQ_UPDATE
, cvc5::Kind::STRING_UPDATE
},
357 {SEQ_AT
, cvc5::Kind::STRING_CHARAT
},
358 {SEQ_CONTAINS
, cvc5::Kind::STRING_CONTAINS
},
359 {SEQ_INDEXOF
, cvc5::Kind::STRING_INDEXOF
},
360 {SEQ_REPLACE
, cvc5::Kind::STRING_REPLACE
},
361 {SEQ_REPLACE_ALL
, cvc5::Kind::STRING_REPLACE_ALL
},
362 {SEQ_REV
, cvc5::Kind::STRING_REV
},
363 {SEQ_PREFIX
, cvc5::Kind::STRING_PREFIX
},
364 {SEQ_SUFFIX
, cvc5::Kind::STRING_SUFFIX
},
365 {CONST_SEQUENCE
, cvc5::Kind::CONST_SEQUENCE
},
366 {SEQ_UNIT
, cvc5::Kind::SEQ_UNIT
},
367 {SEQ_NTH
, cvc5::Kind::SEQ_NTH
},
368 /* Quantifiers --------------------------------------------------------- */
369 {FORALL
, cvc5::Kind::FORALL
},
370 {EXISTS
, cvc5::Kind::EXISTS
},
371 {BOUND_VAR_LIST
, cvc5::Kind::BOUND_VAR_LIST
},
372 {INST_PATTERN
, cvc5::Kind::INST_PATTERN
},
373 {INST_NO_PATTERN
, cvc5::Kind::INST_NO_PATTERN
},
374 {INST_POOL
, cvc5::Kind::INST_POOL
},
375 {INST_ADD_TO_POOL
, cvc5::Kind::INST_ADD_TO_POOL
},
376 {SKOLEM_ADD_TO_POOL
, cvc5::Kind::SKOLEM_ADD_TO_POOL
},
377 {INST_ATTRIBUTE
, cvc5::Kind::INST_ATTRIBUTE
},
378 {INST_PATTERN_LIST
, cvc5::Kind::INST_PATTERN_LIST
},
379 {LAST_KIND
, cvc5::Kind::LAST_KIND
},
382 /* Mapping from internal kind to external (API) kind. */
383 const static std::unordered_map
<cvc5::Kind
, Kind
, cvc5::kind::KindHashFunction
>
385 {cvc5::Kind::UNDEFINED_KIND
, UNDEFINED_KIND
},
386 {cvc5::Kind::NULL_EXPR
, NULL_EXPR
},
387 /* Builtin --------------------------------------------------------- */
388 {cvc5::Kind::UNINTERPRETED_CONSTANT
, UNINTERPRETED_CONSTANT
},
389 {cvc5::Kind::ABSTRACT_VALUE
, ABSTRACT_VALUE
},
390 {cvc5::Kind::EQUAL
, EQUAL
},
391 {cvc5::Kind::DISTINCT
, DISTINCT
},
392 {cvc5::Kind::VARIABLE
, CONSTANT
},
393 {cvc5::Kind::BOUND_VARIABLE
, VARIABLE
},
394 {cvc5::Kind::SEXPR
, SEXPR
},
395 {cvc5::Kind::LAMBDA
, LAMBDA
},
396 {cvc5::Kind::WITNESS
, WITNESS
},
397 /* Boolean --------------------------------------------------------- */
398 {cvc5::Kind::CONST_BOOLEAN
, CONST_BOOLEAN
},
399 {cvc5::Kind::NOT
, NOT
},
400 {cvc5::Kind::AND
, AND
},
401 {cvc5::Kind::IMPLIES
, IMPLIES
},
402 {cvc5::Kind::OR
, OR
},
403 {cvc5::Kind::XOR
, XOR
},
404 {cvc5::Kind::ITE
, ITE
},
405 {cvc5::Kind::MATCH
, MATCH
},
406 {cvc5::Kind::MATCH_CASE
, MATCH_CASE
},
407 {cvc5::Kind::MATCH_BIND_CASE
, MATCH_BIND_CASE
},
408 /* UF -------------------------------------------------------------- */
409 {cvc5::Kind::APPLY_UF
, APPLY_UF
},
410 {cvc5::Kind::CARDINALITY_CONSTRAINT
, CARDINALITY_CONSTRAINT
},
411 {cvc5::Kind::CARDINALITY_VALUE
, CARDINALITY_VALUE
},
412 {cvc5::Kind::HO_APPLY
, HO_APPLY
},
413 /* Arithmetic ------------------------------------------------------ */
414 {cvc5::Kind::PLUS
, PLUS
},
415 {cvc5::Kind::MULT
, MULT
},
416 {cvc5::Kind::IAND
, IAND
},
417 {cvc5::Kind::POW2
, POW2
},
418 {cvc5::Kind::MINUS
, MINUS
},
419 {cvc5::Kind::UMINUS
, UMINUS
},
420 {cvc5::Kind::DIVISION
, DIVISION
},
421 {cvc5::Kind::DIVISION_TOTAL
, INTERNAL_KIND
},
422 {cvc5::Kind::INTS_DIVISION
, INTS_DIVISION
},
423 {cvc5::Kind::INTS_DIVISION_TOTAL
, INTERNAL_KIND
},
424 {cvc5::Kind::INTS_MODULUS
, INTS_MODULUS
},
425 {cvc5::Kind::INTS_MODULUS_TOTAL
, INTERNAL_KIND
},
426 {cvc5::Kind::ABS
, ABS
},
427 {cvc5::Kind::DIVISIBLE
, DIVISIBLE
},
428 {cvc5::Kind::POW
, POW
},
429 {cvc5::Kind::EXPONENTIAL
, EXPONENTIAL
},
430 {cvc5::Kind::SINE
, SINE
},
431 {cvc5::Kind::COSINE
, COSINE
},
432 {cvc5::Kind::TANGENT
, TANGENT
},
433 {cvc5::Kind::COSECANT
, COSECANT
},
434 {cvc5::Kind::SECANT
, SECANT
},
435 {cvc5::Kind::COTANGENT
, COTANGENT
},
436 {cvc5::Kind::ARCSINE
, ARCSINE
},
437 {cvc5::Kind::ARCCOSINE
, ARCCOSINE
},
438 {cvc5::Kind::ARCTANGENT
, ARCTANGENT
},
439 {cvc5::Kind::ARCCOSECANT
, ARCCOSECANT
},
440 {cvc5::Kind::ARCSECANT
, ARCSECANT
},
441 {cvc5::Kind::ARCCOTANGENT
, ARCCOTANGENT
},
442 {cvc5::Kind::SQRT
, SQRT
},
443 {cvc5::Kind::DIVISIBLE_OP
, DIVISIBLE
},
444 {cvc5::Kind::CONST_RATIONAL
, CONST_RATIONAL
},
445 {cvc5::Kind::LT
, LT
},
446 {cvc5::Kind::LEQ
, LEQ
},
447 {cvc5::Kind::GT
, GT
},
448 {cvc5::Kind::GEQ
, GEQ
},
449 {cvc5::Kind::IS_INTEGER
, IS_INTEGER
},
450 {cvc5::Kind::TO_INTEGER
, TO_INTEGER
},
451 {cvc5::Kind::TO_REAL
, TO_REAL
},
452 {cvc5::Kind::PI
, PI
},
453 {cvc5::Kind::IAND_OP
, IAND
},
454 /* BV -------------------------------------------------------------- */
455 {cvc5::Kind::CONST_BITVECTOR
, CONST_BITVECTOR
},
456 {cvc5::Kind::BITVECTOR_CONCAT
, BITVECTOR_CONCAT
},
457 {cvc5::Kind::BITVECTOR_AND
, BITVECTOR_AND
},
458 {cvc5::Kind::BITVECTOR_OR
, BITVECTOR_OR
},
459 {cvc5::Kind::BITVECTOR_XOR
, BITVECTOR_XOR
},
460 {cvc5::Kind::BITVECTOR_NOT
, BITVECTOR_NOT
},
461 {cvc5::Kind::BITVECTOR_NAND
, BITVECTOR_NAND
},
462 {cvc5::Kind::BITVECTOR_NOR
, BITVECTOR_NOR
},
463 {cvc5::Kind::BITVECTOR_XNOR
, BITVECTOR_XNOR
},
464 {cvc5::Kind::BITVECTOR_COMP
, BITVECTOR_COMP
},
465 {cvc5::Kind::BITVECTOR_MULT
, BITVECTOR_MULT
},
466 {cvc5::Kind::BITVECTOR_ADD
, BITVECTOR_ADD
},
467 {cvc5::Kind::BITVECTOR_SUB
, BITVECTOR_SUB
},
468 {cvc5::Kind::BITVECTOR_NEG
, BITVECTOR_NEG
},
469 {cvc5::Kind::BITVECTOR_UDIV
, BITVECTOR_UDIV
},
470 {cvc5::Kind::BITVECTOR_UREM
, BITVECTOR_UREM
},
471 {cvc5::Kind::BITVECTOR_SDIV
, BITVECTOR_SDIV
},
472 {cvc5::Kind::BITVECTOR_SREM
, BITVECTOR_SREM
},
473 {cvc5::Kind::BITVECTOR_SMOD
, BITVECTOR_SMOD
},
474 {cvc5::Kind::BITVECTOR_SHL
, BITVECTOR_SHL
},
475 {cvc5::Kind::BITVECTOR_LSHR
, BITVECTOR_LSHR
},
476 {cvc5::Kind::BITVECTOR_ASHR
, BITVECTOR_ASHR
},
477 {cvc5::Kind::BITVECTOR_ULT
, BITVECTOR_ULT
},
478 {cvc5::Kind::BITVECTOR_ULE
, BITVECTOR_ULE
},
479 {cvc5::Kind::BITVECTOR_UGT
, BITVECTOR_UGT
},
480 {cvc5::Kind::BITVECTOR_UGE
, BITVECTOR_UGE
},
481 {cvc5::Kind::BITVECTOR_SLT
, BITVECTOR_SLT
},
482 {cvc5::Kind::BITVECTOR_SLE
, BITVECTOR_SLE
},
483 {cvc5::Kind::BITVECTOR_SGT
, BITVECTOR_SGT
},
484 {cvc5::Kind::BITVECTOR_SGE
, BITVECTOR_SGE
},
485 {cvc5::Kind::BITVECTOR_ULTBV
, BITVECTOR_ULTBV
},
486 {cvc5::Kind::BITVECTOR_SLTBV
, BITVECTOR_SLTBV
},
487 {cvc5::Kind::BITVECTOR_ITE
, BITVECTOR_ITE
},
488 {cvc5::Kind::BITVECTOR_REDOR
, BITVECTOR_REDOR
},
489 {cvc5::Kind::BITVECTOR_REDAND
, BITVECTOR_REDAND
},
490 {cvc5::Kind::BITVECTOR_EXTRACT_OP
, BITVECTOR_EXTRACT
},
491 {cvc5::Kind::BITVECTOR_REPEAT_OP
, BITVECTOR_REPEAT
},
492 {cvc5::Kind::BITVECTOR_ZERO_EXTEND_OP
, BITVECTOR_ZERO_EXTEND
},
493 {cvc5::Kind::BITVECTOR_SIGN_EXTEND_OP
, BITVECTOR_SIGN_EXTEND
},
494 {cvc5::Kind::BITVECTOR_ROTATE_LEFT_OP
, BITVECTOR_ROTATE_LEFT
},
495 {cvc5::Kind::BITVECTOR_ROTATE_RIGHT_OP
, BITVECTOR_ROTATE_RIGHT
},
496 {cvc5::Kind::BITVECTOR_EXTRACT
, BITVECTOR_EXTRACT
},
497 {cvc5::Kind::BITVECTOR_REPEAT
, BITVECTOR_REPEAT
},
498 {cvc5::Kind::BITVECTOR_ZERO_EXTEND
, BITVECTOR_ZERO_EXTEND
},
499 {cvc5::Kind::BITVECTOR_SIGN_EXTEND
, BITVECTOR_SIGN_EXTEND
},
500 {cvc5::Kind::BITVECTOR_ROTATE_LEFT
, BITVECTOR_ROTATE_LEFT
},
501 {cvc5::Kind::BITVECTOR_ROTATE_RIGHT
, BITVECTOR_ROTATE_RIGHT
},
502 {cvc5::Kind::INT_TO_BITVECTOR_OP
, INT_TO_BITVECTOR
},
503 {cvc5::Kind::INT_TO_BITVECTOR
, INT_TO_BITVECTOR
},
504 {cvc5::Kind::BITVECTOR_TO_NAT
, BITVECTOR_TO_NAT
},
505 /* FP -------------------------------------------------------------- */
506 {cvc5::Kind::CONST_FLOATINGPOINT
, CONST_FLOATINGPOINT
},
507 {cvc5::Kind::CONST_ROUNDINGMODE
, CONST_ROUNDINGMODE
},
508 {cvc5::Kind::FLOATINGPOINT_FP
, FLOATINGPOINT_FP
},
509 {cvc5::Kind::FLOATINGPOINT_EQ
, FLOATINGPOINT_EQ
},
510 {cvc5::Kind::FLOATINGPOINT_ABS
, FLOATINGPOINT_ABS
},
511 {cvc5::Kind::FLOATINGPOINT_NEG
, FLOATINGPOINT_NEG
},
512 {cvc5::Kind::FLOATINGPOINT_ADD
, FLOATINGPOINT_ADD
},
513 {cvc5::Kind::FLOATINGPOINT_SUB
, FLOATINGPOINT_SUB
},
514 {cvc5::Kind::FLOATINGPOINT_MULT
, FLOATINGPOINT_MULT
},
515 {cvc5::Kind::FLOATINGPOINT_DIV
, FLOATINGPOINT_DIV
},
516 {cvc5::Kind::FLOATINGPOINT_FMA
, FLOATINGPOINT_FMA
},
517 {cvc5::Kind::FLOATINGPOINT_SQRT
, FLOATINGPOINT_SQRT
},
518 {cvc5::Kind::FLOATINGPOINT_REM
, FLOATINGPOINT_REM
},
519 {cvc5::Kind::FLOATINGPOINT_RTI
, FLOATINGPOINT_RTI
},
520 {cvc5::Kind::FLOATINGPOINT_MIN
, FLOATINGPOINT_MIN
},
521 {cvc5::Kind::FLOATINGPOINT_MAX
, FLOATINGPOINT_MAX
},
522 {cvc5::Kind::FLOATINGPOINT_LEQ
, FLOATINGPOINT_LEQ
},
523 {cvc5::Kind::FLOATINGPOINT_LT
, FLOATINGPOINT_LT
},
524 {cvc5::Kind::FLOATINGPOINT_GEQ
, FLOATINGPOINT_GEQ
},
525 {cvc5::Kind::FLOATINGPOINT_GT
, FLOATINGPOINT_GT
},
526 {cvc5::Kind::FLOATINGPOINT_ISN
, FLOATINGPOINT_ISN
},
527 {cvc5::Kind::FLOATINGPOINT_ISSN
, FLOATINGPOINT_ISSN
},
528 {cvc5::Kind::FLOATINGPOINT_ISZ
, FLOATINGPOINT_ISZ
},
529 {cvc5::Kind::FLOATINGPOINT_ISINF
, FLOATINGPOINT_ISINF
},
530 {cvc5::Kind::FLOATINGPOINT_ISNAN
, FLOATINGPOINT_ISNAN
},
531 {cvc5::Kind::FLOATINGPOINT_ISNEG
, FLOATINGPOINT_ISNEG
},
532 {cvc5::Kind::FLOATINGPOINT_ISPOS
, FLOATINGPOINT_ISPOS
},
533 {cvc5::Kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP
,
534 FLOATINGPOINT_TO_FP_IEEE_BITVECTOR
},
535 {cvc5::Kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR
,
536 FLOATINGPOINT_TO_FP_IEEE_BITVECTOR
},
537 {cvc5::Kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP
,
538 FLOATINGPOINT_TO_FP_FLOATINGPOINT
},
539 {cvc5::Kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT
,
540 FLOATINGPOINT_TO_FP_FLOATINGPOINT
},
541 {cvc5::Kind::FLOATINGPOINT_TO_FP_REAL_OP
, FLOATINGPOINT_TO_FP_REAL
},
542 {cvc5::Kind::FLOATINGPOINT_TO_FP_REAL
, FLOATINGPOINT_TO_FP_REAL
},
543 {cvc5::Kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP
,
544 FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR
},
545 {cvc5::Kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR
,
546 FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR
},
547 {cvc5::Kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP
,
548 FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR
},
549 {cvc5::Kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR
,
550 FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR
},
551 {cvc5::Kind::FLOATINGPOINT_TO_FP_GENERIC_OP
,
552 FLOATINGPOINT_TO_FP_GENERIC
},
553 {cvc5::Kind::FLOATINGPOINT_TO_FP_GENERIC
, FLOATINGPOINT_TO_FP_GENERIC
},
554 {cvc5::Kind::FLOATINGPOINT_TO_UBV_OP
, FLOATINGPOINT_TO_UBV
},
555 {cvc5::Kind::FLOATINGPOINT_TO_UBV
, FLOATINGPOINT_TO_UBV
},
556 {cvc5::Kind::FLOATINGPOINT_TO_UBV_TOTAL_OP
, INTERNAL_KIND
},
557 {cvc5::Kind::FLOATINGPOINT_TO_UBV_TOTAL
, INTERNAL_KIND
},
558 {cvc5::Kind::FLOATINGPOINT_TO_SBV_OP
, FLOATINGPOINT_TO_SBV
},
559 {cvc5::Kind::FLOATINGPOINT_TO_SBV
, FLOATINGPOINT_TO_SBV
},
560 {cvc5::Kind::FLOATINGPOINT_TO_SBV_TOTAL_OP
, INTERNAL_KIND
},
561 {cvc5::Kind::FLOATINGPOINT_TO_SBV_TOTAL
, INTERNAL_KIND
},
562 {cvc5::Kind::FLOATINGPOINT_TO_REAL
, FLOATINGPOINT_TO_REAL
},
563 {cvc5::Kind::FLOATINGPOINT_TO_REAL_TOTAL
, INTERNAL_KIND
},
564 /* Arrays ---------------------------------------------------------- */
565 {cvc5::Kind::SELECT
, SELECT
},
566 {cvc5::Kind::STORE
, STORE
},
567 {cvc5::Kind::STORE_ALL
, CONST_ARRAY
},
568 /* Datatypes ------------------------------------------------------- */
569 {cvc5::Kind::APPLY_SELECTOR
, APPLY_SELECTOR
},
570 {cvc5::Kind::APPLY_CONSTRUCTOR
, APPLY_CONSTRUCTOR
},
571 {cvc5::Kind::APPLY_SELECTOR_TOTAL
, INTERNAL_KIND
},
572 {cvc5::Kind::APPLY_TESTER
, APPLY_TESTER
},
573 {cvc5::Kind::APPLY_UPDATER
, APPLY_UPDATER
},
574 {cvc5::Kind::DT_SIZE
, DT_SIZE
},
575 {cvc5::Kind::TUPLE_PROJECT
, TUPLE_PROJECT
},
576 {cvc5::Kind::TUPLE_PROJECT_OP
, TUPLE_PROJECT
},
577 /* Separation Logic ------------------------------------------------ */
578 {cvc5::Kind::SEP_NIL
, SEP_NIL
},
579 {cvc5::Kind::SEP_EMP
, SEP_EMP
},
580 {cvc5::Kind::SEP_PTO
, SEP_PTO
},
581 {cvc5::Kind::SEP_STAR
, SEP_STAR
},
582 {cvc5::Kind::SEP_WAND
, SEP_WAND
},
583 /* Sets ------------------------------------------------------------ */
584 {cvc5::Kind::EMPTYSET
, EMPTYSET
},
585 {cvc5::Kind::UNION
, UNION
},
586 {cvc5::Kind::INTERSECTION
, INTERSECTION
},
587 {cvc5::Kind::SETMINUS
, SETMINUS
},
588 {cvc5::Kind::SUBSET
, SUBSET
},
589 {cvc5::Kind::MEMBER
, MEMBER
},
590 {cvc5::Kind::SINGLETON
, SINGLETON
},
591 {cvc5::Kind::INSERT
, INSERT
},
592 {cvc5::Kind::CARD
, CARD
},
593 {cvc5::Kind::COMPLEMENT
, COMPLEMENT
},
594 {cvc5::Kind::UNIVERSE_SET
, UNIVERSE_SET
},
595 {cvc5::Kind::JOIN
, JOIN
},
596 {cvc5::Kind::PRODUCT
, PRODUCT
},
597 {cvc5::Kind::TRANSPOSE
, TRANSPOSE
},
598 {cvc5::Kind::TCLOSURE
, TCLOSURE
},
599 {cvc5::Kind::JOIN_IMAGE
, JOIN_IMAGE
},
600 {cvc5::Kind::IDEN
, IDEN
},
601 {cvc5::Kind::COMPREHENSION
, COMPREHENSION
},
602 {cvc5::Kind::CHOOSE
, CHOOSE
},
603 {cvc5::Kind::IS_SINGLETON
, IS_SINGLETON
},
604 /* Bags ------------------------------------------------------------ */
605 {cvc5::Kind::UNION_MAX
, UNION_MAX
},
606 {cvc5::Kind::UNION_DISJOINT
, UNION_DISJOINT
},
607 {cvc5::Kind::INTERSECTION_MIN
, INTERSECTION_MIN
},
608 {cvc5::Kind::DIFFERENCE_SUBTRACT
, DIFFERENCE_SUBTRACT
},
609 {cvc5::Kind::DIFFERENCE_REMOVE
, DIFFERENCE_REMOVE
},
610 {cvc5::Kind::SUBBAG
, SUBBAG
},
611 {cvc5::Kind::BAG_COUNT
, BAG_COUNT
},
612 {cvc5::Kind::DUPLICATE_REMOVAL
, DUPLICATE_REMOVAL
},
613 {cvc5::Kind::MK_BAG
, MK_BAG
},
614 {cvc5::Kind::EMPTYBAG
, EMPTYBAG
},
615 {cvc5::Kind::BAG_CARD
, BAG_CARD
},
616 {cvc5::Kind::BAG_CHOOSE
, BAG_CHOOSE
},
617 {cvc5::Kind::BAG_IS_SINGLETON
, BAG_IS_SINGLETON
},
618 {cvc5::Kind::BAG_FROM_SET
, BAG_FROM_SET
},
619 {cvc5::Kind::BAG_TO_SET
, BAG_TO_SET
},
620 /* Strings --------------------------------------------------------- */
621 {cvc5::Kind::STRING_CONCAT
, STRING_CONCAT
},
622 {cvc5::Kind::STRING_IN_REGEXP
, STRING_IN_REGEXP
},
623 {cvc5::Kind::STRING_LENGTH
, STRING_LENGTH
},
624 {cvc5::Kind::STRING_SUBSTR
, STRING_SUBSTR
},
625 {cvc5::Kind::STRING_UPDATE
, STRING_UPDATE
},
626 {cvc5::Kind::STRING_CHARAT
, STRING_CHARAT
},
627 {cvc5::Kind::STRING_CONTAINS
, STRING_CONTAINS
},
628 {cvc5::Kind::STRING_INDEXOF
, STRING_INDEXOF
},
629 {cvc5::Kind::STRING_INDEXOF_RE
, STRING_INDEXOF_RE
},
630 {cvc5::Kind::STRING_REPLACE
, STRING_REPLACE
},
631 {cvc5::Kind::STRING_REPLACE_ALL
, STRING_REPLACE_ALL
},
632 {cvc5::Kind::STRING_REPLACE_RE
, STRING_REPLACE_RE
},
633 {cvc5::Kind::STRING_REPLACE_RE_ALL
, STRING_REPLACE_RE_ALL
},
634 {cvc5::Kind::STRING_TOLOWER
, STRING_TOLOWER
},
635 {cvc5::Kind::STRING_TOUPPER
, STRING_TOUPPER
},
636 {cvc5::Kind::STRING_REV
, STRING_REV
},
637 {cvc5::Kind::STRING_FROM_CODE
, STRING_FROM_CODE
},
638 {cvc5::Kind::STRING_TO_CODE
, STRING_TO_CODE
},
639 {cvc5::Kind::STRING_LT
, STRING_LT
},
640 {cvc5::Kind::STRING_LEQ
, STRING_LEQ
},
641 {cvc5::Kind::STRING_PREFIX
, STRING_PREFIX
},
642 {cvc5::Kind::STRING_SUFFIX
, STRING_SUFFIX
},
643 {cvc5::Kind::STRING_IS_DIGIT
, STRING_IS_DIGIT
},
644 {cvc5::Kind::STRING_ITOS
, STRING_FROM_INT
},
645 {cvc5::Kind::STRING_STOI
, STRING_TO_INT
},
646 {cvc5::Kind::CONST_STRING
, CONST_STRING
},
647 {cvc5::Kind::STRING_TO_REGEXP
, STRING_TO_REGEXP
},
648 {cvc5::Kind::REGEXP_CONCAT
, REGEXP_CONCAT
},
649 {cvc5::Kind::REGEXP_UNION
, REGEXP_UNION
},
650 {cvc5::Kind::REGEXP_INTER
, REGEXP_INTER
},
651 {cvc5::Kind::REGEXP_DIFF
, REGEXP_DIFF
},
652 {cvc5::Kind::REGEXP_STAR
, REGEXP_STAR
},
653 {cvc5::Kind::REGEXP_PLUS
, REGEXP_PLUS
},
654 {cvc5::Kind::REGEXP_OPT
, REGEXP_OPT
},
655 {cvc5::Kind::REGEXP_RANGE
, REGEXP_RANGE
},
656 {cvc5::Kind::REGEXP_REPEAT
, REGEXP_REPEAT
},
657 {cvc5::Kind::REGEXP_REPEAT_OP
, REGEXP_REPEAT
},
658 {cvc5::Kind::REGEXP_LOOP
, REGEXP_LOOP
},
659 {cvc5::Kind::REGEXP_LOOP_OP
, REGEXP_LOOP
},
660 {cvc5::Kind::REGEXP_EMPTY
, REGEXP_EMPTY
},
661 {cvc5::Kind::REGEXP_SIGMA
, REGEXP_SIGMA
},
662 {cvc5::Kind::REGEXP_COMPLEMENT
, REGEXP_COMPLEMENT
},
663 {cvc5::Kind::CONST_SEQUENCE
, CONST_SEQUENCE
},
664 {cvc5::Kind::SEQ_UNIT
, SEQ_UNIT
},
665 {cvc5::Kind::SEQ_NTH
, SEQ_NTH
},
666 /* Quantifiers ----------------------------------------------------- */
667 {cvc5::Kind::FORALL
, FORALL
},
668 {cvc5::Kind::EXISTS
, EXISTS
},
669 {cvc5::Kind::BOUND_VAR_LIST
, BOUND_VAR_LIST
},
670 {cvc5::Kind::INST_PATTERN
, INST_PATTERN
},
671 {cvc5::Kind::INST_NO_PATTERN
, INST_NO_PATTERN
},
672 {cvc5::Kind::INST_POOL
, INST_POOL
},
673 {cvc5::Kind::INST_ADD_TO_POOL
, INST_ADD_TO_POOL
},
674 {cvc5::Kind::SKOLEM_ADD_TO_POOL
, SKOLEM_ADD_TO_POOL
},
675 {cvc5::Kind::INST_ATTRIBUTE
, INST_ATTRIBUTE
},
676 {cvc5::Kind::INST_PATTERN_LIST
, INST_PATTERN_LIST
},
677 /* ----------------------------------------------------------------- */
678 {cvc5::Kind::LAST_KIND
, LAST_KIND
},
681 /* Set of kinds for indexed operators */
682 const static std::unordered_set
<Kind
> s_indexed_kinds(
686 BITVECTOR_ZERO_EXTEND
,
687 BITVECTOR_SIGN_EXTEND
,
688 BITVECTOR_ROTATE_LEFT
,
689 BITVECTOR_ROTATE_RIGHT
,
691 FLOATINGPOINT_TO_UBV
,
692 FLOATINGPOINT_TO_SBV
,
694 FLOATINGPOINT_TO_FP_IEEE_BITVECTOR
,
695 FLOATINGPOINT_TO_FP_FLOATINGPOINT
,
696 FLOATINGPOINT_TO_FP_REAL
,
697 FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR
,
698 FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR
,
699 FLOATINGPOINT_TO_FP_GENERIC
});
703 /** Convert a cvc5::Kind (internal) to a cvc5::api::Kind (external). */
704 cvc5::api::Kind
intToExtKind(cvc5::Kind k
)
706 auto it
= api::s_kinds_internal
.find(k
);
707 if (it
== api::s_kinds_internal
.end())
709 return api::INTERNAL_KIND
;
714 /** Convert a cvc5::api::Kind (external) to a cvc5::Kind (internal). */
715 cvc5::Kind
extToIntKind(cvc5::api::Kind k
)
717 auto it
= api::s_kinds
.find(k
);
718 if (it
== api::s_kinds
.end())
720 return cvc5::Kind::UNDEFINED_KIND
;
725 /** Return true if given kind is a defined external kind. */
726 bool isDefinedKind(Kind k
) { return k
> UNDEFINED_KIND
&& k
< LAST_KIND
; }
729 * Return true if the internal kind is one where the API term structure
730 * differs from internal structure. This happens for APPLY_* kinds.
731 * The API takes a "higher-order" perspective and treats functions as well
732 * as datatype constructors/selectors/testers as terms
733 * but interally they are not
735 bool isApplyKind(cvc5::Kind k
)
737 return (k
== cvc5::Kind::APPLY_UF
|| k
== cvc5::Kind::APPLY_CONSTRUCTOR
738 || k
== cvc5::Kind::APPLY_SELECTOR
|| k
== cvc5::Kind::APPLY_TESTER
739 || k
== cvc5::Kind::APPLY_UPDATER
);
742 #ifdef CVC5_ASSERTIONS
743 /** Return true if given kind is a defined internal kind. */
744 bool isDefinedIntKind(cvc5::Kind k
)
746 return k
!= cvc5::Kind::UNDEFINED_KIND
&& k
!= cvc5::Kind::LAST_KIND
;
750 /** Return the minimum arity of given kind. */
751 uint32_t minArity(Kind k
)
753 Assert(isDefinedKind(k
));
754 Assert(isDefinedIntKind(extToIntKind(k
)));
755 uint32_t min
= cvc5::kind::metakind::getMinArityForKind(extToIntKind(k
));
757 // At the API level, we treat functions/constructors/selectors/testers as
758 // normal terms instead of making them part of the operator
759 if (isApplyKind(extToIntKind(k
)))
766 /** Return the maximum arity of given kind. */
767 uint32_t maxArity(Kind k
)
769 Assert(isDefinedKind(k
));
770 Assert(isDefinedIntKind(extToIntKind(k
)));
771 uint32_t max
= cvc5::kind::metakind::getMaxArityForKind(extToIntKind(k
));
773 // At the API level, we treat functions/constructors/selectors/testers as
774 // normal terms instead of making them part of the operator
775 if (isApplyKind(extToIntKind(k
))
776 && max
!= std::numeric_limits
<uint32_t>::max()) // be careful not to
786 std::string
kindToString(Kind k
)
788 return k
== INTERNAL_KIND
? "INTERNAL_KIND"
789 : cvc5::kind::kindToString(extToIntKind(k
));
792 const char* toString(Kind k
)
794 return k
== INTERNAL_KIND
? "INTERNAL_KIND"
795 : cvc5::kind::toString(extToIntKind(k
));
798 std::ostream
& operator<<(std::ostream
& out
, Kind k
)
802 case INTERNAL_KIND
: out
<< "INTERNAL_KIND"; break;
803 default: out
<< extToIntKind(k
);
808 /* -------------------------------------------------------------------------- */
809 /* API guard helpers */
810 /* -------------------------------------------------------------------------- */
814 class CVC5ApiExceptionStream
817 CVC5ApiExceptionStream() {}
818 /* Note: This needs to be explicitly set to 'noexcept(false)' since it is
819 * a destructor that throws an exception and in C++11 all destructors
820 * default to noexcept(true) (else this triggers a call to std::terminate). */
821 ~CVC5ApiExceptionStream() noexcept(false)
823 if (std::uncaught_exceptions() == 0)
825 throw CVC5ApiException(d_stream
.str());
829 std::ostream
& ostream() { return d_stream
; }
832 std::stringstream d_stream
;
835 class CVC5ApiRecoverableExceptionStream
838 CVC5ApiRecoverableExceptionStream() {}
839 /* Note: This needs to be explicitly set to 'noexcept(false)' since it is
840 * a destructor that throws an exception and in C++11 all destructors
841 * default to noexcept(true) (else this triggers a call to std::terminate). */
842 ~CVC5ApiRecoverableExceptionStream() noexcept(false)
844 if (std::uncaught_exceptions() == 0)
846 throw CVC5ApiRecoverableException(d_stream
.str());
850 std::ostream
& ostream() { return d_stream
; }
853 std::stringstream d_stream
;
856 #define CVC5_API_TRY_CATCH_BEGIN \
859 #define CVC5_API_TRY_CATCH_END \
861 catch (const OptionException& e) \
863 throw CVC5ApiOptionException(e.getMessage()); \
865 catch (const cvc5::RecoverableModalException& e) \
867 throw CVC5ApiRecoverableException(e.getMessage()); \
869 catch (const cvc5::Exception& e) { throw CVC5ApiException(e.getMessage()); } \
870 catch (const std::invalid_argument& e) { throw CVC5ApiException(e.what()); }
874 /* -------------------------------------------------------------------------- */
876 /* -------------------------------------------------------------------------- */
878 Result::Result(const cvc5::Result
& r
) : d_result(new cvc5::Result(r
)) {}
880 Result::Result() : d_result(new cvc5::Result()) {}
882 bool Result::isNull() const
884 return d_result
->getType() == cvc5::Result::TYPE_NONE
;
887 bool Result::isSat(void) const
889 return d_result
->getType() == cvc5::Result::TYPE_SAT
890 && d_result
->isSat() == cvc5::Result::SAT
;
893 bool Result::isUnsat(void) const
895 return d_result
->getType() == cvc5::Result::TYPE_SAT
896 && d_result
->isSat() == cvc5::Result::UNSAT
;
899 bool Result::isSatUnknown(void) const
901 return d_result
->getType() == cvc5::Result::TYPE_SAT
902 && d_result
->isSat() == cvc5::Result::SAT_UNKNOWN
;
905 bool Result::isEntailed(void) const
907 return d_result
->getType() == cvc5::Result::TYPE_ENTAILMENT
908 && d_result
->isEntailed() == cvc5::Result::ENTAILED
;
911 bool Result::isNotEntailed(void) const
913 return d_result
->getType() == cvc5::Result::TYPE_ENTAILMENT
914 && d_result
->isEntailed() == cvc5::Result::NOT_ENTAILED
;
917 bool Result::isEntailmentUnknown(void) const
919 return d_result
->getType() == cvc5::Result::TYPE_ENTAILMENT
920 && d_result
->isEntailed() == cvc5::Result::ENTAILMENT_UNKNOWN
;
923 bool Result::operator==(const Result
& r
) const
925 return *d_result
== *r
.d_result
;
928 bool Result::operator!=(const Result
& r
) const
930 return *d_result
!= *r
.d_result
;
933 Result::UnknownExplanation
Result::getUnknownExplanation(void) const
935 cvc5::Result::UnknownExplanation expl
= d_result
->whyUnknown();
938 case cvc5::Result::REQUIRES_FULL_CHECK
: return REQUIRES_FULL_CHECK
;
939 case cvc5::Result::INCOMPLETE
: return INCOMPLETE
;
940 case cvc5::Result::TIMEOUT
: return TIMEOUT
;
941 case cvc5::Result::RESOURCEOUT
: return RESOURCEOUT
;
942 case cvc5::Result::MEMOUT
: return MEMOUT
;
943 case cvc5::Result::INTERRUPTED
: return INTERRUPTED
;
944 case cvc5::Result::NO_STATUS
: return NO_STATUS
;
945 case cvc5::Result::UNSUPPORTED
: return UNSUPPORTED
;
946 case cvc5::Result::OTHER
: return OTHER
;
947 default: return UNKNOWN_REASON
;
949 return UNKNOWN_REASON
;
952 std::string
Result::toString(void) const { return d_result
->toString(); }
954 std::ostream
& operator<<(std::ostream
& out
, const Result
& r
)
960 std::ostream
& operator<<(std::ostream
& out
, enum Result::UnknownExplanation e
)
964 case Result::REQUIRES_FULL_CHECK
: out
<< "REQUIRES_FULL_CHECK"; break;
965 case Result::INCOMPLETE
: out
<< "INCOMPLETE"; break;
966 case Result::TIMEOUT
: out
<< "TIMEOUT"; break;
967 case Result::RESOURCEOUT
: out
<< "RESOURCEOUT"; break;
968 case Result::MEMOUT
: out
<< "MEMOUT"; break;
969 case Result::INTERRUPTED
: out
<< "INTERRUPTED"; break;
970 case Result::NO_STATUS
: out
<< "NO_STATUS"; break;
971 case Result::UNSUPPORTED
: out
<< "UNSUPPORTED"; break;
972 case Result::OTHER
: out
<< "OTHER"; break;
973 case Result::UNKNOWN_REASON
: out
<< "UNKNOWN_REASON"; break;
974 default: Unhandled() << e
;
979 /* -------------------------------------------------------------------------- */
981 /* -------------------------------------------------------------------------- */
983 Sort::Sort(const Solver
* slv
, const cvc5::TypeNode
& t
)
984 : d_solver(slv
), d_type(new cvc5::TypeNode(t
))
988 Sort::Sort() : d_solver(nullptr), d_type(new cvc5::TypeNode()) {}
992 if (d_solver
!= nullptr)
994 // Ensure that the correct node manager is in scope when the node is
996 NodeManagerScope
scope(d_solver
->getNodeManager());
1001 std::set
<TypeNode
> Sort::sortSetToTypeNodes(const std::set
<Sort
>& sorts
)
1003 std::set
<TypeNode
> types
;
1004 for (const Sort
& s
: sorts
)
1006 types
.insert(s
.getTypeNode());
1011 std::vector
<TypeNode
> Sort::sortVectorToTypeNodes(
1012 const std::vector
<Sort
>& sorts
)
1014 std::vector
<TypeNode
> typeNodes
;
1015 for (const Sort
& sort
: sorts
)
1017 typeNodes
.push_back(sort
.getTypeNode());
1022 std::vector
<Sort
> Sort::typeNodeVectorToSorts(
1023 const Solver
* slv
, const std::vector
<TypeNode
>& types
)
1025 std::vector
<Sort
> sorts
;
1026 for (size_t i
= 0, tsize
= types
.size(); i
< tsize
; i
++)
1028 sorts
.push_back(Sort(slv
, types
[i
]));
1033 bool Sort::operator==(const Sort
& s
) const
1035 CVC5_API_TRY_CATCH_BEGIN
;
1036 //////// all checks before this line
1037 return *d_type
== *s
.d_type
;
1039 CVC5_API_TRY_CATCH_END
;
1042 bool Sort::operator!=(const Sort
& s
) const
1044 CVC5_API_TRY_CATCH_BEGIN
;
1045 //////// all checks before this line
1046 return *d_type
!= *s
.d_type
;
1048 CVC5_API_TRY_CATCH_END
;
1051 bool Sort::operator<(const Sort
& s
) const
1053 CVC5_API_TRY_CATCH_BEGIN
;
1054 //////// all checks before this line
1055 return *d_type
< *s
.d_type
;
1057 CVC5_API_TRY_CATCH_END
;
1060 bool Sort::operator>(const Sort
& s
) const
1062 CVC5_API_TRY_CATCH_BEGIN
;
1063 //////// all checks before this line
1064 return *d_type
> *s
.d_type
;
1066 CVC5_API_TRY_CATCH_END
;
1069 bool Sort::operator<=(const Sort
& s
) const
1071 CVC5_API_TRY_CATCH_BEGIN
;
1072 //////// all checks before this line
1073 return *d_type
<= *s
.d_type
;
1075 CVC5_API_TRY_CATCH_END
;
1078 bool Sort::operator>=(const Sort
& s
) const
1080 CVC5_API_TRY_CATCH_BEGIN
;
1081 //////// all checks before this line
1082 return *d_type
>= *s
.d_type
;
1084 CVC5_API_TRY_CATCH_END
;
1087 bool Sort::isNull() const
1089 CVC5_API_TRY_CATCH_BEGIN
;
1090 //////// all checks before this line
1091 return isNullHelper();
1093 CVC5_API_TRY_CATCH_END
;
1096 bool Sort::isBoolean() const
1098 CVC5_API_TRY_CATCH_BEGIN
;
1099 //////// all checks before this line
1100 return d_type
->isBoolean();
1102 CVC5_API_TRY_CATCH_END
;
1105 bool Sort::isInteger() const
1107 CVC5_API_TRY_CATCH_BEGIN
;
1108 //////// all checks before this line
1109 return d_type
->isInteger();
1111 CVC5_API_TRY_CATCH_END
;
1114 bool Sort::isReal() const
1116 CVC5_API_TRY_CATCH_BEGIN
;
1117 //////// all checks before this line
1118 // notice that we do not expose internal subtyping to the user
1119 return d_type
->isReal() && !d_type
->isInteger();
1121 CVC5_API_TRY_CATCH_END
;
1124 bool Sort::isString() const
1126 CVC5_API_TRY_CATCH_BEGIN
;
1127 //////// all checks before this line
1128 return d_type
->isString();
1130 CVC5_API_TRY_CATCH_END
;
1133 bool Sort::isRegExp() const
1135 CVC5_API_TRY_CATCH_BEGIN
;
1136 //////// all checks before this line
1137 return d_type
->isRegExp();
1139 CVC5_API_TRY_CATCH_END
;
1142 bool Sort::isRoundingMode() const
1144 CVC5_API_TRY_CATCH_BEGIN
;
1145 //////// all checks before this line
1146 return d_type
->isRoundingMode();
1148 CVC5_API_TRY_CATCH_END
;
1151 bool Sort::isBitVector() const
1153 CVC5_API_TRY_CATCH_BEGIN
;
1154 //////// all checks before this line
1155 return d_type
->isBitVector();
1157 CVC5_API_TRY_CATCH_END
;
1160 bool Sort::isFloatingPoint() const
1162 CVC5_API_TRY_CATCH_BEGIN
;
1163 //////// all checks before this line
1164 return d_type
->isFloatingPoint();
1166 CVC5_API_TRY_CATCH_END
;
1169 bool Sort::isDatatype() const
1171 CVC5_API_TRY_CATCH_BEGIN
;
1172 //////// all checks before this line
1173 return d_type
->isDatatype();
1175 CVC5_API_TRY_CATCH_END
;
1178 bool Sort::isParametricDatatype() const
1180 CVC5_API_TRY_CATCH_BEGIN
;
1181 //////// all checks before this line
1182 if (!d_type
->isDatatype()) return false;
1183 return d_type
->isParametricDatatype();
1185 CVC5_API_TRY_CATCH_END
;
1188 bool Sort::isConstructor() const
1190 CVC5_API_TRY_CATCH_BEGIN
;
1191 //////// all checks before this line
1192 return d_type
->isConstructor();
1194 CVC5_API_TRY_CATCH_END
;
1197 bool Sort::isSelector() const
1199 CVC5_API_TRY_CATCH_BEGIN
;
1200 //////// all checks before this line
1201 return d_type
->isSelector();
1203 CVC5_API_TRY_CATCH_END
;
1206 bool Sort::isTester() const
1208 CVC5_API_TRY_CATCH_BEGIN
;
1209 //////// all checks before this line
1210 return d_type
->isTester();
1212 CVC5_API_TRY_CATCH_END
;
1215 bool Sort::isUpdater() const
1217 CVC5_API_TRY_CATCH_BEGIN
;
1218 //////// all checks before this line
1219 return d_type
->isUpdater();
1221 CVC5_API_TRY_CATCH_END
;
1224 bool Sort::isFunction() const
1226 CVC5_API_TRY_CATCH_BEGIN
;
1227 //////// all checks before this line
1228 return d_type
->isFunction();
1230 CVC5_API_TRY_CATCH_END
;
1233 bool Sort::isPredicate() const
1235 CVC5_API_TRY_CATCH_BEGIN
;
1236 //////// all checks before this line
1237 return d_type
->isPredicate();
1239 CVC5_API_TRY_CATCH_END
;
1242 bool Sort::isTuple() const
1244 CVC5_API_TRY_CATCH_BEGIN
;
1245 //////// all checks before this line
1246 return d_type
->isTuple();
1248 CVC5_API_TRY_CATCH_END
;
1251 bool Sort::isRecord() const
1253 CVC5_API_TRY_CATCH_BEGIN
;
1254 //////// all checks before this line
1255 return d_type
->isRecord();
1257 CVC5_API_TRY_CATCH_END
;
1260 bool Sort::isArray() const
1262 CVC5_API_TRY_CATCH_BEGIN
;
1263 //////// all checks before this line
1264 return d_type
->isArray();
1266 CVC5_API_TRY_CATCH_END
;
1269 bool Sort::isSet() const
1271 CVC5_API_TRY_CATCH_BEGIN
;
1272 //////// all checks before this line
1273 return d_type
->isSet();
1275 CVC5_API_TRY_CATCH_END
;
1278 bool Sort::isBag() const
1280 CVC5_API_TRY_CATCH_BEGIN
;
1281 //////// all checks before this line
1282 return d_type
->isBag();
1284 CVC5_API_TRY_CATCH_END
;
1287 bool Sort::isSequence() const
1289 CVC5_API_TRY_CATCH_BEGIN
;
1290 //////// all checks before this line
1291 return d_type
->isSequence();
1293 CVC5_API_TRY_CATCH_END
;
1296 bool Sort::isUninterpretedSort() const
1298 CVC5_API_TRY_CATCH_BEGIN
;
1299 //////// all checks before this line
1300 return d_type
->isSort();
1302 CVC5_API_TRY_CATCH_END
;
1305 bool Sort::isSortConstructor() const
1307 CVC5_API_TRY_CATCH_BEGIN
;
1308 //////// all checks before this line
1309 return d_type
->isSortConstructor();
1311 CVC5_API_TRY_CATCH_END
;
1314 bool Sort::isFirstClass() const
1316 CVC5_API_TRY_CATCH_BEGIN
;
1317 //////// all checks before this line
1318 return d_type
->isFirstClass();
1320 CVC5_API_TRY_CATCH_END
;
1323 bool Sort::isFunctionLike() const
1325 CVC5_API_TRY_CATCH_BEGIN
;
1326 //////// all checks before this line
1327 return d_type
->isFunctionLike();
1329 CVC5_API_TRY_CATCH_END
;
1332 bool Sort::isSubsortOf(const Sort
& s
) const
1334 CVC5_API_TRY_CATCH_BEGIN
;
1335 CVC5_API_ARG_CHECK_SOLVER("sort", s
);
1336 //////// all checks before this line
1337 return d_type
->isSubtypeOf(*s
.d_type
);
1339 CVC5_API_TRY_CATCH_END
;
1342 bool Sort::isComparableTo(const Sort
& s
) const
1344 CVC5_API_TRY_CATCH_BEGIN
;
1345 CVC5_API_ARG_CHECK_SOLVER("sort", s
);
1346 //////// all checks before this line
1347 return d_type
->isComparableTo(*s
.d_type
);
1349 CVC5_API_TRY_CATCH_END
;
1352 Datatype
Sort::getDatatype() const
1354 NodeManagerScope
scope(d_solver
->getNodeManager());
1355 CVC5_API_TRY_CATCH_BEGIN
;
1356 CVC5_API_CHECK_NOT_NULL
;
1357 CVC5_API_CHECK(isDatatype()) << "Expected datatype sort.";
1358 //////// all checks before this line
1359 return Datatype(d_solver
, d_type
->getDType());
1361 CVC5_API_TRY_CATCH_END
;
1364 Sort
Sort::instantiate(const std::vector
<Sort
>& params
) const
1366 NodeManagerScope
scope(d_solver
->getNodeManager());
1367 CVC5_API_TRY_CATCH_BEGIN
;
1368 CVC5_API_CHECK_NOT_NULL
;
1369 CVC5_API_CHECK_SORTS(params
);
1370 CVC5_API_CHECK(isParametricDatatype() || isSortConstructor())
1371 << "Expected parametric datatype or sort constructor sort.";
1372 //////// all checks before this line
1373 std::vector
<cvc5::TypeNode
> tparams
= sortVectorToTypeNodes(params
);
1374 if (d_type
->isDatatype())
1376 return Sort(d_solver
, d_type
->instantiateParametricDatatype(tparams
));
1378 Assert(d_type
->isSortConstructor());
1379 return Sort(d_solver
, d_solver
->getNodeManager()->mkSort(*d_type
, tparams
));
1381 CVC5_API_TRY_CATCH_END
;
1384 Sort
Sort::substitute(const Sort
& sort
, const Sort
& replacement
) const
1386 NodeManagerScope
scope(d_solver
->getNodeManager());
1387 CVC5_API_TRY_CATCH_BEGIN
;
1388 CVC5_API_CHECK_NOT_NULL
;
1389 CVC5_API_CHECK_SORT(sort
);
1390 CVC5_API_CHECK_SORT(replacement
);
1391 //////// all checks before this line
1394 d_type
->substitute(sort
.getTypeNode(), replacement
.getTypeNode()));
1396 CVC5_API_TRY_CATCH_END
;
1399 Sort
Sort::substitute(const std::vector
<Sort
>& sorts
,
1400 const std::vector
<Sort
>& replacements
) const
1402 NodeManagerScope
scope(d_solver
->getNodeManager());
1403 CVC5_API_TRY_CATCH_BEGIN
;
1404 CVC5_API_CHECK_NOT_NULL
;
1405 CVC5_API_CHECK_SORTS(sorts
);
1406 CVC5_API_CHECK_SORTS(replacements
);
1407 //////// all checks before this line
1409 std::vector
<cvc5::TypeNode
> tSorts
= sortVectorToTypeNodes(sorts
),
1411 sortVectorToTypeNodes(replacements
);
1412 return Sort(d_solver
,
1413 d_type
->substitute(tSorts
.begin(),
1415 tReplacements
.begin(),
1416 tReplacements
.end()));
1418 CVC5_API_TRY_CATCH_END
;
1421 std::string
Sort::toString() const
1423 CVC5_API_TRY_CATCH_BEGIN
;
1424 //////// all checks before this line
1425 if (d_solver
!= nullptr)
1427 NodeManagerScope
scope(d_solver
->getNodeManager());
1428 return d_type
->toString();
1430 return d_type
->toString();
1432 CVC5_API_TRY_CATCH_END
;
1435 const cvc5::TypeNode
& Sort::getTypeNode(void) const { return *d_type
; }
1437 /* Constructor sort ------------------------------------------------------- */
1439 size_t Sort::getConstructorArity() const
1441 CVC5_API_TRY_CATCH_BEGIN
;
1442 CVC5_API_CHECK_NOT_NULL
;
1443 CVC5_API_CHECK(isConstructor()) << "Not a constructor sort: " << (*this);
1444 //////// all checks before this line
1445 return d_type
->getNumChildren() - 1;
1447 CVC5_API_TRY_CATCH_END
;
1450 std::vector
<Sort
> Sort::getConstructorDomainSorts() const
1452 CVC5_API_TRY_CATCH_BEGIN
;
1453 CVC5_API_CHECK_NOT_NULL
;
1454 CVC5_API_CHECK(isConstructor()) << "Not a constructor sort: " << (*this);
1455 //////// all checks before this line
1456 return typeNodeVectorToSorts(d_solver
, d_type
->getArgTypes());
1458 CVC5_API_TRY_CATCH_END
;
1461 Sort
Sort::getConstructorCodomainSort() const
1463 CVC5_API_TRY_CATCH_BEGIN
;
1464 CVC5_API_CHECK_NOT_NULL
;
1465 CVC5_API_CHECK(isConstructor()) << "Not a constructor sort: " << (*this);
1466 //////// all checks before this line
1467 return Sort(d_solver
, d_type
->getConstructorRangeType());
1469 CVC5_API_TRY_CATCH_END
;
1472 /* Selector sort ------------------------------------------------------- */
1474 Sort
Sort::getSelectorDomainSort() const
1476 CVC5_API_TRY_CATCH_BEGIN
;
1477 CVC5_API_CHECK_NOT_NULL
;
1478 CVC5_API_CHECK(isSelector()) << "Not a selector sort: " << (*this);
1479 //////// all checks before this line
1480 return Sort(d_solver
, d_type
->getSelectorDomainType());
1482 CVC5_API_TRY_CATCH_END
;
1485 Sort
Sort::getSelectorCodomainSort() const
1487 CVC5_API_TRY_CATCH_BEGIN
;
1488 CVC5_API_CHECK_NOT_NULL
;
1489 CVC5_API_CHECK(isSelector()) << "Not a selector sort: " << (*this);
1490 //////// all checks before this line
1491 return Sort(d_solver
, d_type
->getSelectorRangeType());
1493 CVC5_API_TRY_CATCH_END
;
1496 /* Tester sort ------------------------------------------------------- */
1498 Sort
Sort::getTesterDomainSort() const
1500 CVC5_API_TRY_CATCH_BEGIN
;
1501 CVC5_API_CHECK_NOT_NULL
;
1502 CVC5_API_CHECK(isTester()) << "Not a tester sort: " << (*this);
1503 //////// all checks before this line
1504 return Sort(d_solver
, d_type
->getTesterDomainType());
1506 CVC5_API_TRY_CATCH_END
;
1509 Sort
Sort::getTesterCodomainSort() const
1511 CVC5_API_TRY_CATCH_BEGIN
;
1512 CVC5_API_CHECK_NOT_NULL
;
1513 CVC5_API_CHECK(isTester()) << "Not a tester sort: " << (*this);
1514 //////// all checks before this line
1515 return d_solver
->getBooleanSort();
1517 CVC5_API_TRY_CATCH_END
;
1520 /* Function sort ------------------------------------------------------- */
1522 size_t Sort::getFunctionArity() const
1524 CVC5_API_TRY_CATCH_BEGIN
;
1525 CVC5_API_CHECK_NOT_NULL
;
1526 CVC5_API_CHECK(isFunction()) << "Not a function sort: " << (*this);
1527 //////// all checks before this line
1528 return d_type
->getNumChildren() - 1;
1530 CVC5_API_TRY_CATCH_END
;
1533 std::vector
<Sort
> Sort::getFunctionDomainSorts() const
1535 CVC5_API_TRY_CATCH_BEGIN
;
1536 CVC5_API_CHECK_NOT_NULL
;
1537 CVC5_API_CHECK(isFunction()) << "Not a function sort: " << (*this);
1538 //////// all checks before this line
1539 return typeNodeVectorToSorts(d_solver
, d_type
->getArgTypes());
1541 CVC5_API_TRY_CATCH_END
;
1544 Sort
Sort::getFunctionCodomainSort() const
1546 CVC5_API_TRY_CATCH_BEGIN
;
1547 CVC5_API_CHECK_NOT_NULL
;
1548 CVC5_API_CHECK(isFunction()) << "Not a function sort" << (*this);
1549 //////// all checks before this line
1550 return Sort(d_solver
, d_type
->getRangeType());
1552 CVC5_API_TRY_CATCH_END
;
1555 /* Array sort ---------------------------------------------------------- */
1557 Sort
Sort::getArrayIndexSort() const
1559 CVC5_API_TRY_CATCH_BEGIN
;
1560 CVC5_API_CHECK_NOT_NULL
;
1561 CVC5_API_CHECK(isArray()) << "Not an array sort.";
1562 //////// all checks before this line
1563 return Sort(d_solver
, d_type
->getArrayIndexType());
1565 CVC5_API_TRY_CATCH_END
;
1568 Sort
Sort::getArrayElementSort() const
1570 CVC5_API_TRY_CATCH_BEGIN
;
1571 CVC5_API_CHECK_NOT_NULL
;
1572 CVC5_API_CHECK(isArray()) << "Not an array sort.";
1573 //////// all checks before this line
1574 return Sort(d_solver
, d_type
->getArrayConstituentType());
1576 CVC5_API_TRY_CATCH_END
;
1579 /* Set sort ------------------------------------------------------------ */
1581 Sort
Sort::getSetElementSort() const
1583 CVC5_API_TRY_CATCH_BEGIN
;
1584 CVC5_API_CHECK_NOT_NULL
;
1585 CVC5_API_CHECK(isSet()) << "Not a set sort.";
1586 //////// all checks before this line
1587 return Sort(d_solver
, d_type
->getSetElementType());
1589 CVC5_API_TRY_CATCH_END
;
1592 /* Bag sort ------------------------------------------------------------ */
1594 Sort
Sort::getBagElementSort() const
1596 CVC5_API_TRY_CATCH_BEGIN
;
1597 CVC5_API_CHECK_NOT_NULL
;
1598 CVC5_API_CHECK(isBag()) << "Not a bag sort.";
1599 //////// all checks before this line
1600 return Sort(d_solver
, d_type
->getBagElementType());
1602 CVC5_API_TRY_CATCH_END
;
1605 /* Sequence sort ------------------------------------------------------- */
1607 Sort
Sort::getSequenceElementSort() const
1609 CVC5_API_TRY_CATCH_BEGIN
;
1610 CVC5_API_CHECK_NOT_NULL
;
1611 CVC5_API_CHECK(isSequence()) << "Not a sequence sort.";
1612 //////// all checks before this line
1613 return Sort(d_solver
, d_type
->getSequenceElementType());
1615 CVC5_API_TRY_CATCH_END
;
1618 /* Uninterpreted sort -------------------------------------------------- */
1620 std::string
Sort::getUninterpretedSortName() const
1622 CVC5_API_TRY_CATCH_BEGIN
;
1623 CVC5_API_CHECK_NOT_NULL
;
1624 CVC5_API_CHECK(isUninterpretedSort()) << "Not an uninterpreted sort.";
1625 //////// all checks before this line
1626 return d_type
->getName();
1628 CVC5_API_TRY_CATCH_END
;
1631 bool Sort::isUninterpretedSortParameterized() const
1633 CVC5_API_TRY_CATCH_BEGIN
;
1634 CVC5_API_CHECK_NOT_NULL
;
1635 CVC5_API_CHECK(isUninterpretedSort()) << "Not an uninterpreted sort.";
1636 //////// all checks before this line
1638 /* This method is not implemented in the NodeManager, since whether a
1639 * uninterpreted sort is parameterized is irrelevant for solving. */
1640 return d_type
->getNumChildren() > 0;
1642 CVC5_API_TRY_CATCH_END
;
1645 std::vector
<Sort
> Sort::getUninterpretedSortParamSorts() const
1647 CVC5_API_TRY_CATCH_BEGIN
;
1648 CVC5_API_CHECK_NOT_NULL
;
1649 CVC5_API_CHECK(isUninterpretedSort()) << "Not an uninterpreted sort.";
1650 //////// all checks before this line
1652 /* This method is not implemented in the NodeManager, since whether a
1653 * uninterpreted sort is parameterized is irrelevant for solving. */
1654 std::vector
<TypeNode
> params
;
1655 for (size_t i
= 0, nchildren
= d_type
->getNumChildren(); i
< nchildren
; i
++)
1657 params
.push_back((*d_type
)[i
]);
1659 return typeNodeVectorToSorts(d_solver
, params
);
1661 CVC5_API_TRY_CATCH_END
;
1664 /* Sort constructor sort ----------------------------------------------- */
1666 std::string
Sort::getSortConstructorName() const
1668 CVC5_API_TRY_CATCH_BEGIN
;
1669 CVC5_API_CHECK_NOT_NULL
;
1670 CVC5_API_CHECK(isSortConstructor()) << "Not a sort constructor sort.";
1671 //////// all checks before this line
1672 return d_type
->getName();
1674 CVC5_API_TRY_CATCH_END
;
1677 size_t Sort::getSortConstructorArity() const
1679 CVC5_API_TRY_CATCH_BEGIN
;
1680 CVC5_API_CHECK_NOT_NULL
;
1681 CVC5_API_CHECK(isSortConstructor()) << "Not a sort constructor sort.";
1682 //////// all checks before this line
1683 return d_type
->getSortConstructorArity();
1685 CVC5_API_TRY_CATCH_END
;
1688 /* Bit-vector sort ----------------------------------------------------- */
1690 uint32_t Sort::getBVSize() const
1692 CVC5_API_TRY_CATCH_BEGIN
;
1693 CVC5_API_CHECK_NOT_NULL
;
1694 CVC5_API_CHECK(isBitVector()) << "Not a bit-vector sort.";
1695 //////// all checks before this line
1696 return d_type
->getBitVectorSize();
1698 CVC5_API_TRY_CATCH_END
;
1701 /* Floating-point sort ------------------------------------------------- */
1703 uint32_t Sort::getFPExponentSize() const
1705 CVC5_API_TRY_CATCH_BEGIN
;
1706 CVC5_API_CHECK_NOT_NULL
;
1707 CVC5_API_CHECK(isFloatingPoint()) << "Not a floating-point sort.";
1708 //////// all checks before this line
1709 return d_type
->getFloatingPointExponentSize();
1711 CVC5_API_TRY_CATCH_END
;
1714 uint32_t Sort::getFPSignificandSize() const
1716 CVC5_API_TRY_CATCH_BEGIN
;
1717 CVC5_API_CHECK_NOT_NULL
;
1718 CVC5_API_CHECK(isFloatingPoint()) << "Not a floating-point sort.";
1719 //////// all checks before this line
1720 return d_type
->getFloatingPointSignificandSize();
1722 CVC5_API_TRY_CATCH_END
;
1725 /* Datatype sort ------------------------------------------------------- */
1727 std::vector
<Sort
> Sort::getDatatypeParamSorts() const
1729 CVC5_API_TRY_CATCH_BEGIN
;
1730 CVC5_API_CHECK_NOT_NULL
;
1731 CVC5_API_CHECK(isParametricDatatype()) << "Not a parametric datatype sort.";
1732 //////// all checks before this line
1733 return typeNodeVectorToSorts(d_solver
, d_type
->getParamTypes());
1735 CVC5_API_TRY_CATCH_END
;
1738 size_t Sort::getDatatypeArity() const
1740 CVC5_API_TRY_CATCH_BEGIN
;
1741 CVC5_API_CHECK_NOT_NULL
;
1742 CVC5_API_CHECK(isDatatype()) << "Not a datatype sort.";
1743 //////// all checks before this line
1744 return d_type
->getNumChildren() - 1;
1746 CVC5_API_TRY_CATCH_END
;
1749 /* Tuple sort ---------------------------------------------------------- */
1751 size_t Sort::getTupleLength() const
1753 CVC5_API_TRY_CATCH_BEGIN
;
1754 CVC5_API_CHECK_NOT_NULL
;
1755 CVC5_API_CHECK(isTuple()) << "Not a tuple sort.";
1756 //////// all checks before this line
1757 return d_type
->getTupleLength();
1759 CVC5_API_TRY_CATCH_END
;
1762 std::vector
<Sort
> Sort::getTupleSorts() const
1764 CVC5_API_TRY_CATCH_BEGIN
;
1765 CVC5_API_CHECK_NOT_NULL
;
1766 CVC5_API_CHECK(isTuple()) << "Not a tuple sort.";
1767 //////// all checks before this line
1768 return typeNodeVectorToSorts(d_solver
, d_type
->getTupleTypes());
1770 CVC5_API_TRY_CATCH_END
;
1773 /* --------------------------------------------------------------------- */
1775 std::ostream
& operator<<(std::ostream
& out
, const Sort
& s
)
1777 out
<< s
.toString();
1782 /* -------------------------------------------------------------------------- */
1784 /* Split out to avoid nested API calls (problematic with API tracing). */
1785 /* .......................................................................... */
1787 bool Sort::isNullHelper() const { return d_type
->isNull(); }
1789 /* -------------------------------------------------------------------------- */
1791 /* -------------------------------------------------------------------------- */
1793 Op::Op() : d_solver(nullptr), d_kind(NULL_EXPR
), d_node(new cvc5::Node()) {}
1795 Op::Op(const Solver
* slv
, const Kind k
)
1796 : d_solver(slv
), d_kind(k
), d_node(new cvc5::Node())
1800 Op::Op(const Solver
* slv
, const Kind k
, const cvc5::Node
& n
)
1801 : d_solver(slv
), d_kind(k
), d_node(new cvc5::Node(n
))
1807 if (d_solver
!= nullptr)
1809 // Ensure that the correct node manager is in scope when the type node is
1811 NodeManagerScope
scope(d_solver
->getNodeManager());
1816 /* Public methods */
1817 bool Op::operator==(const Op
& t
) const
1819 CVC5_API_TRY_CATCH_BEGIN
;
1820 //////// all checks before this line
1821 if (d_node
->isNull() && t
.d_node
->isNull())
1823 return (d_kind
== t
.d_kind
);
1825 else if (d_node
->isNull() || t
.d_node
->isNull())
1829 return (d_kind
== t
.d_kind
) && (*d_node
== *t
.d_node
);
1831 CVC5_API_TRY_CATCH_END
;
1834 bool Op::operator!=(const Op
& t
) const
1836 CVC5_API_TRY_CATCH_BEGIN
;
1837 //////// all checks before this line
1838 return !(*this == t
);
1840 CVC5_API_TRY_CATCH_END
;
1843 Kind
Op::getKind() const
1845 CVC5_API_CHECK(d_kind
!= NULL_EXPR
) << "Expecting a non-null Kind";
1846 //////// all checks before this line
1850 bool Op::isNull() const
1852 CVC5_API_TRY_CATCH_BEGIN
;
1853 //////// all checks before this line
1854 return isNullHelper();
1856 CVC5_API_TRY_CATCH_END
;
1859 bool Op::isIndexed() const
1861 CVC5_API_TRY_CATCH_BEGIN
;
1862 //////// all checks before this line
1863 return isIndexedHelper();
1865 CVC5_API_TRY_CATCH_END
;
1868 size_t Op::getNumIndices() const
1870 CVC5_API_TRY_CATCH_BEGIN
;
1871 CVC5_API_CHECK_NOT_NULL
;
1872 //////// all checks before this line
1873 return getNumIndicesHelper();
1875 CVC5_API_TRY_CATCH_END
;
1878 size_t Op::getNumIndicesHelper() const
1880 if (!isIndexedHelper())
1885 Kind k
= intToExtKind(d_node
->getKind());
1889 case DIVISIBLE
: size
= 1; break;
1890 case BITVECTOR_REPEAT
: size
= 1; break;
1891 case BITVECTOR_ZERO_EXTEND
: size
= 1; break;
1892 case BITVECTOR_SIGN_EXTEND
: size
= 1; break;
1893 case BITVECTOR_ROTATE_LEFT
: size
= 1; break;
1894 case BITVECTOR_ROTATE_RIGHT
: size
= 1; break;
1895 case INT_TO_BITVECTOR
: size
= 1; break;
1896 case IAND
: size
= 1; break;
1897 case FLOATINGPOINT_TO_UBV
: size
= 1; break;
1898 case FLOATINGPOINT_TO_SBV
: size
= 1; break;
1899 case REGEXP_REPEAT
: size
= 1; break;
1900 case BITVECTOR_EXTRACT
: size
= 2; break;
1901 case FLOATINGPOINT_TO_FP_IEEE_BITVECTOR
: size
= 2; break;
1902 case FLOATINGPOINT_TO_FP_FLOATINGPOINT
: size
= 2; break;
1903 case FLOATINGPOINT_TO_FP_REAL
: size
= 2; break;
1904 case FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR
: size
= 2; break;
1905 case FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR
: size
= 2; break;
1906 case FLOATINGPOINT_TO_FP_GENERIC
: size
= 2; break;
1907 case REGEXP_LOOP
: size
= 2; break;
1909 size
= d_node
->getConst
<TupleProjectOp
>().getIndices().size();
1911 default: CVC5_API_CHECK(false) << "Unhandled kind " << kindToString(k
);
1916 Term
Op::operator[](size_t index
) const
1918 return getIndexHelper(index
);
1921 Term
Op::getIndexHelper(size_t index
) const
1923 CVC5_API_TRY_CATCH_BEGIN
;
1924 CVC5_API_CHECK_NOT_NULL
;
1925 CVC5_API_CHECK(!d_node
->isNull())
1926 << "Expecting a non-null internal expression. This Op is not indexed.";
1927 CVC5_API_CHECK(index
< getNumIndicesHelper()) << "index out of bound";
1928 Kind k
= intToExtKind(d_node
->getKind());
1934 t
= d_solver
->mkValHelper
<Rational
>(
1935 Rational(d_node
->getConst
<Divisible
>().k
));
1938 case BITVECTOR_REPEAT
:
1940 t
= d_solver
->mkValHelper
<cvc5::Rational
>(
1941 d_node
->getConst
<BitVectorRepeat
>().d_repeatAmount
);
1944 case BITVECTOR_ZERO_EXTEND
:
1946 t
= d_solver
->mkValHelper
<cvc5::Rational
>(
1947 d_node
->getConst
<BitVectorZeroExtend
>().d_zeroExtendAmount
);
1950 case BITVECTOR_SIGN_EXTEND
:
1952 t
= d_solver
->mkValHelper
<cvc5::Rational
>(
1953 d_node
->getConst
<BitVectorSignExtend
>().d_signExtendAmount
);
1956 case BITVECTOR_ROTATE_LEFT
:
1958 t
= d_solver
->mkValHelper
<cvc5::Rational
>(
1959 d_node
->getConst
<BitVectorRotateLeft
>().d_rotateLeftAmount
);
1962 case BITVECTOR_ROTATE_RIGHT
:
1964 t
= d_solver
->mkValHelper
<cvc5::Rational
>(
1965 d_node
->getConst
<BitVectorRotateRight
>().d_rotateRightAmount
);
1968 case INT_TO_BITVECTOR
:
1970 t
= d_solver
->mkValHelper
<cvc5::Rational
>(
1971 d_node
->getConst
<IntToBitVector
>().d_size
);
1976 t
= d_solver
->mkValHelper
<cvc5::Rational
>(
1977 d_node
->getConst
<IntAnd
>().d_size
);
1980 case FLOATINGPOINT_TO_UBV
:
1982 t
= d_solver
->mkValHelper
<cvc5::Rational
>(
1983 d_node
->getConst
<FloatingPointToUBV
>().d_bv_size
.d_size
);
1986 case FLOATINGPOINT_TO_SBV
:
1988 t
= d_solver
->mkValHelper
<cvc5::Rational
>(
1989 d_node
->getConst
<FloatingPointToSBV
>().d_bv_size
.d_size
);
1994 t
= d_solver
->mkValHelper
<cvc5::Rational
>(
1995 d_node
->getConst
<RegExpRepeat
>().d_repeatAmount
);
1998 case BITVECTOR_EXTRACT
:
2000 cvc5::BitVectorExtract ext
= d_node
->getConst
<BitVectorExtract
>();
2001 t
= index
== 0 ? d_solver
->mkValHelper
<cvc5::Rational
>(ext
.d_high
)
2002 : d_solver
->mkValHelper
<cvc5::Rational
>(ext
.d_low
);
2005 case FLOATINGPOINT_TO_FP_IEEE_BITVECTOR
:
2007 cvc5::FloatingPointToFPIEEEBitVector ext
=
2008 d_node
->getConst
<FloatingPointToFPIEEEBitVector
>();
2010 t
= index
== 0 ? d_solver
->mkValHelper
<cvc5::Rational
>(
2011 ext
.getSize().exponentWidth())
2012 : d_solver
->mkValHelper
<cvc5::Rational
>(
2013 ext
.getSize().significandWidth());
2016 case FLOATINGPOINT_TO_FP_FLOATINGPOINT
:
2018 cvc5::FloatingPointToFPFloatingPoint ext
=
2019 d_node
->getConst
<FloatingPointToFPFloatingPoint
>();
2020 t
= index
== 0 ? d_solver
->mkValHelper
<cvc5::Rational
>(
2021 ext
.getSize().exponentWidth())
2022 : d_solver
->mkValHelper
<cvc5::Rational
>(
2023 ext
.getSize().significandWidth());
2026 case FLOATINGPOINT_TO_FP_REAL
:
2028 cvc5::FloatingPointToFPReal ext
=
2029 d_node
->getConst
<FloatingPointToFPReal
>();
2031 t
= index
== 0 ? d_solver
->mkValHelper
<cvc5::Rational
>(
2032 ext
.getSize().exponentWidth())
2033 : d_solver
->mkValHelper
<cvc5::Rational
>(
2034 ext
.getSize().significandWidth());
2037 case FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR
:
2039 cvc5::FloatingPointToFPSignedBitVector ext
=
2040 d_node
->getConst
<FloatingPointToFPSignedBitVector
>();
2041 t
= index
== 0 ? d_solver
->mkValHelper
<cvc5::Rational
>(
2042 ext
.getSize().exponentWidth())
2043 : d_solver
->mkValHelper
<cvc5::Rational
>(
2044 ext
.getSize().significandWidth());
2047 case FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR
:
2049 cvc5::FloatingPointToFPUnsignedBitVector ext
=
2050 d_node
->getConst
<FloatingPointToFPUnsignedBitVector
>();
2051 t
= index
== 0 ? d_solver
->mkValHelper
<cvc5::Rational
>(
2052 ext
.getSize().exponentWidth())
2053 : d_solver
->mkValHelper
<cvc5::Rational
>(
2054 ext
.getSize().significandWidth());
2057 case FLOATINGPOINT_TO_FP_GENERIC
:
2059 cvc5::FloatingPointToFPGeneric ext
=
2060 d_node
->getConst
<FloatingPointToFPGeneric
>();
2061 t
= index
== 0 ? d_solver
->mkValHelper
<cvc5::Rational
>(
2062 ext
.getSize().exponentWidth())
2063 : d_solver
->mkValHelper
<cvc5::Rational
>(
2064 ext
.getSize().significandWidth());
2069 cvc5::RegExpLoop ext
= d_node
->getConst
<RegExpLoop
>();
2070 t
= index
== 0 ? d_solver
->mkValHelper
<cvc5::Rational
>(ext
.d_loopMinOcc
)
2071 : d_solver
->mkValHelper
<cvc5::Rational
>(ext
.d_loopMaxOcc
);
2078 const std::vector
<uint32_t>& projectionIndices
=
2079 d_node
->getConst
<TupleProjectOp
>().getIndices();
2080 t
= d_solver
->mkValHelper
<cvc5::Rational
>(projectionIndices
[index
]);
2085 CVC5_API_CHECK(false) << "Unhandled kind " << kindToString(k
);
2090 //////// all checks before this line
2093 CVC5_API_TRY_CATCH_END
;
2097 std::string
Op::getIndices() const
2099 CVC5_API_TRY_CATCH_BEGIN
;
2100 CVC5_API_CHECK_NOT_NULL
;
2101 CVC5_API_CHECK(!d_node
->isNull())
2102 << "Expecting a non-null internal expression. This Op is not indexed.";
2103 Kind k
= intToExtKind(d_node
->getKind());
2104 CVC5_API_CHECK(k
== DIVISIBLE
) << "Can't get string index from"
2105 << " kind " << kindToString(k
);
2106 //////// all checks before this line
2107 return d_node
->getConst
<Divisible
>().k
.toString();
2109 CVC5_API_TRY_CATCH_END
;
2113 uint32_t Op::getIndices() const
2115 CVC5_API_TRY_CATCH_BEGIN
;
2116 CVC5_API_CHECK_NOT_NULL
;
2117 CVC5_API_CHECK(!d_node
->isNull())
2118 << "Expecting a non-null internal expression. This Op is not indexed.";
2119 //////// all checks before this line
2122 Kind k
= intToExtKind(d_node
->getKind());
2125 case BITVECTOR_REPEAT
:
2126 i
= d_node
->getConst
<BitVectorRepeat
>().d_repeatAmount
;
2128 case BITVECTOR_ZERO_EXTEND
:
2129 i
= d_node
->getConst
<BitVectorZeroExtend
>().d_zeroExtendAmount
;
2131 case BITVECTOR_SIGN_EXTEND
:
2132 i
= d_node
->getConst
<BitVectorSignExtend
>().d_signExtendAmount
;
2134 case BITVECTOR_ROTATE_LEFT
:
2135 i
= d_node
->getConst
<BitVectorRotateLeft
>().d_rotateLeftAmount
;
2137 case BITVECTOR_ROTATE_RIGHT
:
2138 i
= d_node
->getConst
<BitVectorRotateRight
>().d_rotateRightAmount
;
2140 case INT_TO_BITVECTOR
: i
= d_node
->getConst
<IntToBitVector
>().d_size
; break;
2141 case IAND
: i
= d_node
->getConst
<IntAnd
>().d_size
; break;
2142 case FLOATINGPOINT_TO_UBV
:
2143 i
= d_node
->getConst
<FloatingPointToUBV
>().d_bv_size
.d_size
;
2145 case FLOATINGPOINT_TO_SBV
:
2146 i
= d_node
->getConst
<FloatingPointToSBV
>().d_bv_size
.d_size
;
2149 i
= d_node
->getConst
<RegExpRepeat
>().d_repeatAmount
;
2152 CVC5_API_CHECK(false) << "Can't get uint32_t index from"
2153 << " kind " << kindToString(k
);
2157 CVC5_API_TRY_CATCH_END
;
2161 std::pair
<uint32_t, uint32_t> Op::getIndices() const
2163 CVC5_API_TRY_CATCH_BEGIN
;
2164 CVC5_API_CHECK_NOT_NULL
;
2165 CVC5_API_CHECK(!d_node
->isNull())
2166 << "Expecting a non-null internal expression. This Op is not indexed.";
2167 //////// all checks before this line
2169 std::pair
<uint32_t, uint32_t> indices
;
2170 Kind k
= intToExtKind(d_node
->getKind());
2172 // using if/else instead of case statement because want local variables
2173 if (k
== BITVECTOR_EXTRACT
)
2175 cvc5::BitVectorExtract ext
= d_node
->getConst
<BitVectorExtract
>();
2176 indices
= std::make_pair(ext
.d_high
, ext
.d_low
);
2178 else if (k
== FLOATINGPOINT_TO_FP_IEEE_BITVECTOR
)
2180 cvc5::FloatingPointToFPIEEEBitVector ext
=
2181 d_node
->getConst
<FloatingPointToFPIEEEBitVector
>();
2182 indices
= std::make_pair(ext
.getSize().exponentWidth(),
2183 ext
.getSize().significandWidth());
2185 else if (k
== FLOATINGPOINT_TO_FP_FLOATINGPOINT
)
2187 cvc5::FloatingPointToFPFloatingPoint ext
=
2188 d_node
->getConst
<FloatingPointToFPFloatingPoint
>();
2189 indices
= std::make_pair(ext
.getSize().exponentWidth(),
2190 ext
.getSize().significandWidth());
2192 else if (k
== FLOATINGPOINT_TO_FP_REAL
)
2194 cvc5::FloatingPointToFPReal ext
= d_node
->getConst
<FloatingPointToFPReal
>();
2195 indices
= std::make_pair(ext
.getSize().exponentWidth(),
2196 ext
.getSize().significandWidth());
2198 else if (k
== FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR
)
2200 cvc5::FloatingPointToFPSignedBitVector ext
=
2201 d_node
->getConst
<FloatingPointToFPSignedBitVector
>();
2202 indices
= std::make_pair(ext
.getSize().exponentWidth(),
2203 ext
.getSize().significandWidth());
2205 else if (k
== FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR
)
2207 cvc5::FloatingPointToFPUnsignedBitVector ext
=
2208 d_node
->getConst
<FloatingPointToFPUnsignedBitVector
>();
2209 indices
= std::make_pair(ext
.getSize().exponentWidth(),
2210 ext
.getSize().significandWidth());
2212 else if (k
== FLOATINGPOINT_TO_FP_GENERIC
)
2214 cvc5::FloatingPointToFPGeneric ext
=
2215 d_node
->getConst
<FloatingPointToFPGeneric
>();
2216 indices
= std::make_pair(ext
.getSize().exponentWidth(),
2217 ext
.getSize().significandWidth());
2219 else if (k
== REGEXP_LOOP
)
2221 cvc5::RegExpLoop ext
= d_node
->getConst
<RegExpLoop
>();
2222 indices
= std::make_pair(ext
.d_loopMinOcc
, ext
.d_loopMaxOcc
);
2226 CVC5_API_CHECK(false) << "Can't get pair<uint32_t, uint32_t> indices from"
2227 << " kind " << kindToString(k
);
2231 CVC5_API_TRY_CATCH_END
;
2235 std::vector
<api::Term
> Op::getIndices() const
2237 CVC5_API_TRY_CATCH_BEGIN
;
2238 CVC5_API_CHECK_NOT_NULL
;
2239 CVC5_API_CHECK(!d_node
->isNull())
2240 << "Expecting a non-null internal expression. This Op is not indexed.";
2241 size_t size
= getNumIndicesHelper();
2242 std::vector
<Term
> terms(getNumIndices());
2243 for (size_t i
= 0; i
< size
; i
++)
2245 terms
[i
] = getIndexHelper(i
);
2247 //////// all checks before this line
2250 CVC5_API_TRY_CATCH_END
;
2253 std::string
Op::toString() const
2255 CVC5_API_TRY_CATCH_BEGIN
;
2256 //////// all checks before this line
2257 if (d_node
->isNull())
2259 return kindToString(d_kind
);
2263 CVC5_API_CHECK(!d_node
->isNull())
2264 << "Expecting a non-null internal expression";
2265 if (d_solver
!= nullptr)
2267 NodeManagerScope
scope(d_solver
->getNodeManager());
2268 return d_node
->toString();
2270 return d_node
->toString();
2273 CVC5_API_TRY_CATCH_END
;
2276 std::ostream
& operator<<(std::ostream
& out
, const Op
& t
)
2278 out
<< t
.toString();
2283 /* -------------------------------------------------------------------------- */
2285 /* Split out to avoid nested API calls (problematic with API tracing). */
2286 /* .......................................................................... */
2288 bool Op::isNullHelper() const
2290 return (d_node
->isNull() && (d_kind
== NULL_EXPR
));
2293 bool Op::isIndexedHelper() const { return !d_node
->isNull(); }
2295 /* -------------------------------------------------------------------------- */
2297 /* -------------------------------------------------------------------------- */
2299 Term::Term() : d_solver(nullptr), d_node(new cvc5::Node()) {}
2301 Term::Term(const Solver
* slv
, const cvc5::Node
& n
) : d_solver(slv
)
2303 // Ensure that we create the node in the correct node manager.
2304 NodeManagerScope
scope(d_solver
->getNodeManager());
2305 d_node
.reset(new cvc5::Node(n
));
2310 if (d_solver
!= nullptr)
2312 // Ensure that the correct node manager is in scope when the node is
2314 NodeManagerScope
scope(d_solver
->getNodeManager());
2319 bool Term::operator==(const Term
& t
) const
2321 CVC5_API_TRY_CATCH_BEGIN
;
2322 //////// all checks before this line
2323 return *d_node
== *t
.d_node
;
2325 CVC5_API_TRY_CATCH_END
;
2328 bool Term::operator!=(const Term
& t
) const
2330 CVC5_API_TRY_CATCH_BEGIN
;
2331 //////// all checks before this line
2332 return *d_node
!= *t
.d_node
;
2334 CVC5_API_TRY_CATCH_END
;
2337 bool Term::operator<(const Term
& t
) const
2339 CVC5_API_TRY_CATCH_BEGIN
;
2340 //////// all checks before this line
2341 return *d_node
< *t
.d_node
;
2343 CVC5_API_TRY_CATCH_END
;
2346 bool Term::operator>(const Term
& t
) const
2348 CVC5_API_TRY_CATCH_BEGIN
;
2349 //////// all checks before this line
2350 return *d_node
> *t
.d_node
;
2352 CVC5_API_TRY_CATCH_END
;
2355 bool Term::operator<=(const Term
& t
) const
2357 CVC5_API_TRY_CATCH_BEGIN
;
2358 //////// all checks before this line
2359 return *d_node
<= *t
.d_node
;
2361 CVC5_API_TRY_CATCH_END
;
2364 bool Term::operator>=(const Term
& t
) const
2366 CVC5_API_TRY_CATCH_BEGIN
;
2367 //////// all checks before this line
2368 return *d_node
>= *t
.d_node
;
2370 CVC5_API_TRY_CATCH_END
;
2373 size_t Term::getNumChildren() const
2375 CVC5_API_TRY_CATCH_BEGIN
;
2376 CVC5_API_CHECK_NOT_NULL
;
2377 //////// all checks before this line
2379 // special case for apply kinds
2380 if (isApplyKind(d_node
->getKind()))
2382 return d_node
->getNumChildren() + 1;
2388 return d_node
->getNumChildren();
2390 CVC5_API_TRY_CATCH_END
;
2393 Term
Term::operator[](size_t index
) const
2395 CVC5_API_TRY_CATCH_BEGIN
;
2396 CVC5_API_CHECK_NOT_NULL
;
2397 CVC5_API_CHECK(index
< getNumChildren()) << "index out of bound";
2398 CVC5_API_CHECK(!isApplyKind(d_node
->getKind()) || d_node
->hasOperator())
2399 << "Expected apply kind to have operator when accessing child of Term";
2400 //////// all checks before this line
2402 // special cases for apply kinds
2403 if (isApplyKind(d_node
->getKind()))
2407 // return the operator
2408 return Term(d_solver
, d_node
->getOperator());
2415 // otherwise we are looking up child at (index-1)
2416 return Term(d_solver
, (*d_node
)[index
]);
2418 CVC5_API_TRY_CATCH_END
;
2421 uint64_t Term::getId() const
2423 CVC5_API_TRY_CATCH_BEGIN
;
2424 CVC5_API_CHECK_NOT_NULL
;
2425 //////// all checks before this line
2426 return d_node
->getId();
2428 CVC5_API_TRY_CATCH_END
;
2431 Kind
Term::getKind() const
2433 CVC5_API_TRY_CATCH_BEGIN
;
2434 CVC5_API_CHECK_NOT_NULL
;
2435 //////// all checks before this line
2436 return getKindHelper();
2438 CVC5_API_TRY_CATCH_END
;
2441 Sort
Term::getSort() const
2443 CVC5_API_TRY_CATCH_BEGIN
;
2444 CVC5_API_CHECK_NOT_NULL
;
2445 NodeManagerScope
scope(d_solver
->getNodeManager());
2446 //////// all checks before this line
2447 return Sort(d_solver
, d_node
->getType());
2449 CVC5_API_TRY_CATCH_END
;
2452 Term
Term::substitute(const Term
& term
, const Term
& replacement
) const
2454 CVC5_API_TRY_CATCH_BEGIN
;
2455 CVC5_API_CHECK_NOT_NULL
;
2456 CVC5_API_CHECK_TERM(term
);
2457 CVC5_API_CHECK_TERM(replacement
);
2458 CVC5_API_CHECK(term
.getSort().isComparableTo(replacement
.getSort()))
2459 << "Expecting terms of comparable sort in substitute";
2460 //////// all checks before this line
2463 d_node
->substitute(TNode(*term
.d_node
), TNode(*replacement
.d_node
)));
2465 CVC5_API_TRY_CATCH_END
;
2468 Term
Term::substitute(const std::vector
<Term
>& terms
,
2469 const std::vector
<Term
>& replacements
) const
2471 CVC5_API_TRY_CATCH_BEGIN
;
2472 CVC5_API_CHECK_NOT_NULL
;
2473 CVC5_API_CHECK(terms
.size() == replacements
.size())
2474 << "Expecting vectors of the same arity in substitute";
2475 CVC5_API_TERM_CHECK_TERMS_WITH_TERMS_COMPARABLE_TO(terms
, replacements
);
2476 //////// all checks before this line
2477 std::vector
<Node
> nodes
= Term::termVectorToNodes(terms
);
2478 std::vector
<Node
> nodeReplacements
= Term::termVectorToNodes(replacements
);
2479 return Term(d_solver
,
2480 d_node
->substitute(nodes
.begin(),
2482 nodeReplacements
.begin(),
2483 nodeReplacements
.end()));
2485 CVC5_API_TRY_CATCH_END
;
2488 bool Term::hasOp() const
2490 CVC5_API_TRY_CATCH_BEGIN
;
2491 CVC5_API_CHECK_NOT_NULL
;
2492 //////// all checks before this line
2493 return d_node
->hasOperator();
2495 CVC5_API_TRY_CATCH_END
;
2498 Op
Term::getOp() const
2500 CVC5_API_TRY_CATCH_BEGIN
;
2501 CVC5_API_CHECK_NOT_NULL
;
2502 CVC5_API_CHECK(d_node
->hasOperator())
2503 << "Expecting Term to have an Op when calling getOp()";
2504 //////// all checks before this line
2506 // special cases for parameterized operators that are not indexed operators
2507 // the API level differs from the internal structure
2508 // indexed operators are stored in Ops
2509 // whereas functions and datatype operators are terms, and the Op
2510 // is one of the APPLY_* kinds
2511 if (isApplyKind(d_node
->getKind()))
2513 return Op(d_solver
, intToExtKind(d_node
->getKind()));
2515 else if (d_node
->getMetaKind() == kind::metakind::PARAMETERIZED
)
2517 // it's an indexed operator
2518 // so we should return the indexed op
2519 cvc5::Node op
= d_node
->getOperator();
2520 return Op(d_solver
, intToExtKind(d_node
->getKind()), op
);
2522 // Notice this is the only case where getKindHelper is used, since the
2523 // cases above do not have special cases for intToExtKind.
2524 return Op(d_solver
, getKindHelper());
2526 CVC5_API_TRY_CATCH_END
;
2529 bool Term::isNull() const
2531 CVC5_API_TRY_CATCH_BEGIN
;
2532 //////// all checks before this line
2533 return isNullHelper();
2535 CVC5_API_TRY_CATCH_END
;
2538 Term
Term::notTerm() const
2540 CVC5_API_TRY_CATCH_BEGIN
;
2541 CVC5_API_CHECK_NOT_NULL
;
2542 //////// all checks before this line
2543 Node res
= d_node
->notNode();
2544 (void)res
.getType(true); /* kick off type checking */
2545 return Term(d_solver
, res
);
2547 CVC5_API_TRY_CATCH_END
;
2550 Term
Term::andTerm(const Term
& t
) const
2552 CVC5_API_TRY_CATCH_BEGIN
;
2553 CVC5_API_CHECK_NOT_NULL
;
2554 CVC5_API_CHECK_TERM(t
);
2555 //////// all checks before this line
2556 Node res
= d_node
->andNode(*t
.d_node
);
2557 (void)res
.getType(true); /* kick off type checking */
2558 return Term(d_solver
, res
);
2560 CVC5_API_TRY_CATCH_END
;
2563 Term
Term::orTerm(const Term
& t
) const
2565 CVC5_API_TRY_CATCH_BEGIN
;
2566 CVC5_API_CHECK_NOT_NULL
;
2567 CVC5_API_CHECK_TERM(t
);
2568 //////// all checks before this line
2569 Node res
= d_node
->orNode(*t
.d_node
);
2570 (void)res
.getType(true); /* kick off type checking */
2571 return Term(d_solver
, res
);
2573 CVC5_API_TRY_CATCH_END
;
2576 Term
Term::xorTerm(const Term
& t
) const
2578 CVC5_API_TRY_CATCH_BEGIN
;
2579 CVC5_API_CHECK_NOT_NULL
;
2580 CVC5_API_CHECK_TERM(t
);
2581 //////// all checks before this line
2582 Node res
= d_node
->xorNode(*t
.d_node
);
2583 (void)res
.getType(true); /* kick off type checking */
2584 return Term(d_solver
, res
);
2586 CVC5_API_TRY_CATCH_END
;
2589 Term
Term::eqTerm(const Term
& t
) const
2591 CVC5_API_TRY_CATCH_BEGIN
;
2592 CVC5_API_CHECK_NOT_NULL
;
2593 CVC5_API_CHECK_TERM(t
);
2594 //////// all checks before this line
2595 Node res
= d_node
->eqNode(*t
.d_node
);
2596 (void)res
.getType(true); /* kick off type checking */
2597 return Term(d_solver
, res
);
2599 CVC5_API_TRY_CATCH_END
;
2602 Term
Term::impTerm(const Term
& t
) const
2604 CVC5_API_TRY_CATCH_BEGIN
;
2605 CVC5_API_CHECK_NOT_NULL
;
2606 CVC5_API_CHECK_TERM(t
);
2607 //////// all checks before this line
2608 Node res
= d_node
->impNode(*t
.d_node
);
2609 (void)res
.getType(true); /* kick off type checking */
2610 return Term(d_solver
, res
);
2612 CVC5_API_TRY_CATCH_END
;
2615 Term
Term::iteTerm(const Term
& then_t
, const Term
& else_t
) const
2617 CVC5_API_TRY_CATCH_BEGIN
;
2618 CVC5_API_CHECK_NOT_NULL
;
2619 CVC5_API_CHECK_TERM(then_t
);
2620 CVC5_API_CHECK_TERM(else_t
);
2621 //////// all checks before this line
2622 Node res
= d_node
->iteNode(*then_t
.d_node
, *else_t
.d_node
);
2623 (void)res
.getType(true); /* kick off type checking */
2624 return Term(d_solver
, res
);
2626 CVC5_API_TRY_CATCH_END
;
2629 std::string
Term::toString() const
2631 CVC5_API_TRY_CATCH_BEGIN
;
2632 //////// all checks before this line
2633 if (d_solver
!= nullptr)
2635 NodeManagerScope
scope(d_solver
->getNodeManager());
2636 return d_node
->toString();
2638 return d_node
->toString();
2640 CVC5_API_TRY_CATCH_END
;
2643 Term::const_iterator::const_iterator()
2644 : d_solver(nullptr), d_origNode(nullptr), d_pos(0)
2648 Term::const_iterator::const_iterator(const Solver
* slv
,
2649 const std::shared_ptr
<cvc5::Node
>& n
,
2651 : d_solver(slv
), d_origNode(n
), d_pos(p
)
2655 Term::const_iterator::const_iterator(const const_iterator
& it
)
2656 : d_solver(nullptr), d_origNode(nullptr)
2658 if (it
.d_origNode
!= nullptr)
2660 d_solver
= it
.d_solver
;
2661 d_origNode
= it
.d_origNode
;
2666 Term::const_iterator
& Term::const_iterator::operator=(const const_iterator
& it
)
2668 d_solver
= it
.d_solver
;
2669 d_origNode
= it
.d_origNode
;
2674 bool Term::const_iterator::operator==(const const_iterator
& it
) const
2676 if (d_origNode
== nullptr || it
.d_origNode
== nullptr)
2680 return (d_solver
== it
.d_solver
&& *d_origNode
== *it
.d_origNode
)
2681 && (d_pos
== it
.d_pos
);
2684 bool Term::const_iterator::operator!=(const const_iterator
& it
) const
2686 return !(*this == it
);
2689 Term::const_iterator
& Term::const_iterator::operator++()
2691 Assert(d_origNode
!= nullptr);
2696 Term::const_iterator
Term::const_iterator::operator++(int)
2698 Assert(d_origNode
!= nullptr);
2699 const_iterator it
= *this;
2704 Term
Term::const_iterator::operator*() const
2706 Assert(d_origNode
!= nullptr);
2707 // this term has an extra child (mismatch between API and internal structure)
2708 // the extra child will be the first child
2709 bool extra_child
= isApplyKind(d_origNode
->getKind());
2711 if (!d_pos
&& extra_child
)
2713 return Term(d_solver
, d_origNode
->getOperator());
2717 uint32_t idx
= d_pos
;
2724 return Term(d_solver
, (*d_origNode
)[idx
]);
2728 Term::const_iterator
Term::begin() const
2730 return Term::const_iterator(d_solver
, d_node
, 0);
2733 Term::const_iterator
Term::end() const
2735 int endpos
= d_node
->getNumChildren();
2736 // special cases for APPLY_*
2737 // the API differs from the internal structure
2738 // the API takes a "higher-order" perspective and the applied
2739 // function or datatype constructor/selector/tester is a Term
2740 // which means it needs to be one of the children, even though
2741 // internally it is not
2742 if (isApplyKind(d_node
->getKind()))
2744 // one more child if this is a UF application (count the UF as a child)
2747 return Term::const_iterator(d_solver
, d_node
, endpos
);
2750 const cvc5::Node
& Term::getNode(void) const { return *d_node
; }
2753 const Rational
& getRational(const cvc5::Node
& node
)
2755 switch (node
.getKind())
2757 case cvc5::Kind::CAST_TO_REAL
: return node
[0].getConst
<Rational
>();
2758 case cvc5::Kind::CONST_RATIONAL
: return node
.getConst
<Rational
>();
2760 CVC5_API_CHECK(false) << "Node is not a rational.";
2761 return node
.getConst
<Rational
>();
2764 Integer
getInteger(const cvc5::Node
& node
)
2766 return node
.getConst
<Rational
>().getNumerator();
2768 template <typename T
>
2769 bool checkIntegerBounds(const Integer
& i
)
2771 return i
>= std::numeric_limits
<T
>::min()
2772 && i
<= std::numeric_limits
<T
>::max();
2774 bool checkReal32Bounds(const Rational
& r
)
2776 return checkIntegerBounds
<std::int32_t>(r
.getNumerator())
2777 && checkIntegerBounds
<std::uint32_t>(r
.getDenominator());
2779 bool checkReal64Bounds(const Rational
& r
)
2781 return checkIntegerBounds
<std::int64_t>(r
.getNumerator())
2782 && checkIntegerBounds
<std::uint64_t>(r
.getDenominator());
2785 bool isReal(const Node
& node
)
2787 return node
.getKind() == cvc5::Kind::CONST_RATIONAL
2788 || node
.getKind() == cvc5::Kind::CAST_TO_REAL
;
2790 bool isReal32(const Node
& node
)
2792 return isReal(node
) && checkReal32Bounds(getRational(node
));
2794 bool isReal64(const Node
& node
)
2796 return isReal(node
) && checkReal64Bounds(getRational(node
));
2799 bool isInteger(const Node
& node
)
2801 return node
.getKind() == cvc5::Kind::CONST_RATIONAL
2802 && node
.getConst
<Rational
>().isIntegral();
2804 bool isInt32(const Node
& node
)
2806 return isInteger(node
) && checkIntegerBounds
<std::int32_t>(getInteger(node
));
2808 bool isUInt32(const Node
& node
)
2810 return isInteger(node
) && checkIntegerBounds
<std::uint32_t>(getInteger(node
));
2812 bool isInt64(const Node
& node
)
2814 return isInteger(node
) && checkIntegerBounds
<std::int64_t>(getInteger(node
));
2816 bool isUInt64(const Node
& node
)
2818 return isInteger(node
) && checkIntegerBounds
<std::uint64_t>(getInteger(node
));
2820 } // namespace detail
2822 bool Term::isInt32Value() const
2824 CVC5_API_TRY_CATCH_BEGIN
;
2825 CVC5_API_CHECK_NOT_NULL
;
2826 //////// all checks before this line
2827 return detail::isInt32(*d_node
);
2829 CVC5_API_TRY_CATCH_END
;
2832 std::int32_t Term::getInt32Value() const
2834 CVC5_API_TRY_CATCH_BEGIN
;
2835 CVC5_API_CHECK_NOT_NULL
;
2836 CVC5_API_ARG_CHECK_EXPECTED(detail::isInt32(*d_node
), *d_node
)
2837 << "Term to be a 32-bit integer value when calling getInt32Value()";
2838 //////// all checks before this line
2839 return detail::getInteger(*d_node
).getSignedInt();
2841 CVC5_API_TRY_CATCH_END
;
2844 bool Term::isUInt32Value() const
2846 CVC5_API_TRY_CATCH_BEGIN
;
2847 CVC5_API_CHECK_NOT_NULL
;
2848 //////// all checks before this line
2849 return detail::isUInt32(*d_node
);
2851 CVC5_API_TRY_CATCH_END
;
2853 std::uint32_t Term::getUInt32Value() const
2855 CVC5_API_TRY_CATCH_BEGIN
;
2856 CVC5_API_CHECK_NOT_NULL
;
2857 CVC5_API_ARG_CHECK_EXPECTED(detail::isUInt32(*d_node
), *d_node
)
2858 << "Term to be a unsigned 32-bit integer value when calling "
2860 //////// all checks before this line
2861 return detail::getInteger(*d_node
).getUnsignedInt();
2863 CVC5_API_TRY_CATCH_END
;
2866 bool Term::isInt64Value() const
2868 CVC5_API_TRY_CATCH_BEGIN
;
2869 CVC5_API_CHECK_NOT_NULL
;
2870 //////// all checks before this line
2871 return detail::isInt64(*d_node
);
2873 CVC5_API_TRY_CATCH_END
;
2875 std::int64_t Term::getInt64Value() const
2877 CVC5_API_TRY_CATCH_BEGIN
;
2878 CVC5_API_CHECK_NOT_NULL
;
2879 CVC5_API_ARG_CHECK_EXPECTED(detail::isInt64(*d_node
), *d_node
)
2880 << "Term to be a 64-bit integer value when calling getInt64Value()";
2881 //////// all checks before this line
2882 return detail::getInteger(*d_node
).getLong();
2884 CVC5_API_TRY_CATCH_END
;
2887 bool Term::isUInt64Value() const
2889 CVC5_API_TRY_CATCH_BEGIN
;
2890 CVC5_API_CHECK_NOT_NULL
;
2891 //////// all checks before this line
2892 return detail::isUInt64(*d_node
);
2894 CVC5_API_TRY_CATCH_END
;
2897 std::uint64_t Term::getUInt64Value() const
2899 CVC5_API_TRY_CATCH_BEGIN
;
2900 CVC5_API_CHECK_NOT_NULL
;
2901 CVC5_API_ARG_CHECK_EXPECTED(detail::isUInt64(*d_node
), *d_node
)
2902 << "Term to be a unsigned 64-bit integer value when calling "
2904 //////// all checks before this line
2905 return detail::getInteger(*d_node
).getUnsignedLong();
2907 CVC5_API_TRY_CATCH_END
;
2910 bool Term::isIntegerValue() const
2912 CVC5_API_TRY_CATCH_BEGIN
;
2913 CVC5_API_CHECK_NOT_NULL
;
2914 //////// all checks before this line
2915 return detail::isInteger(*d_node
);
2917 CVC5_API_TRY_CATCH_END
;
2919 std::string
Term::getIntegerValue() const
2921 CVC5_API_TRY_CATCH_BEGIN
;
2922 CVC5_API_CHECK_NOT_NULL
;
2923 CVC5_API_ARG_CHECK_EXPECTED(detail::isInteger(*d_node
), *d_node
)
2924 << "Term to be an integer value when calling getIntegerValue()";
2925 //////// all checks before this line
2926 return detail::getInteger(*d_node
).toString();
2928 CVC5_API_TRY_CATCH_END
;
2931 bool Term::isStringValue() const
2933 CVC5_API_TRY_CATCH_BEGIN
;
2934 CVC5_API_CHECK_NOT_NULL
;
2935 //////// all checks before this line
2936 return d_node
->getKind() == cvc5::Kind::CONST_STRING
;
2938 CVC5_API_TRY_CATCH_END
;
2941 std::wstring
Term::getStringValue() const
2943 CVC5_API_TRY_CATCH_BEGIN
;
2944 CVC5_API_CHECK_NOT_NULL
;
2945 CVC5_API_ARG_CHECK_EXPECTED(d_node
->getKind() == cvc5::Kind::CONST_STRING
,
2947 << "Term to be a string value when calling getStringValue()";
2948 //////// all checks before this line
2949 return d_node
->getConst
<cvc5::String
>().toWString();
2951 CVC5_API_TRY_CATCH_END
;
2954 std::vector
<Node
> Term::termVectorToNodes(const std::vector
<Term
>& terms
)
2956 std::vector
<Node
> res
;
2957 for (const Term
& t
: terms
)
2959 res
.push_back(t
.getNode());
2964 bool Term::isReal32Value() const
2966 CVC5_API_TRY_CATCH_BEGIN
;
2967 CVC5_API_CHECK_NOT_NULL
;
2968 //////// all checks before this line
2969 return detail::isReal32(*d_node
);
2971 CVC5_API_TRY_CATCH_END
;
2973 std::pair
<std::int32_t, std::uint32_t> Term::getReal32Value() const
2975 CVC5_API_TRY_CATCH_BEGIN
;
2976 CVC5_API_CHECK_NOT_NULL
;
2977 CVC5_API_ARG_CHECK_EXPECTED(detail::isReal32(*d_node
), *d_node
)
2978 << "Term to be a 32-bit rational value when calling getReal32Value()";
2979 //////// all checks before this line
2980 const Rational
& r
= detail::getRational(*d_node
);
2981 return std::make_pair(r
.getNumerator().getSignedInt(),
2982 r
.getDenominator().getUnsignedInt());
2984 CVC5_API_TRY_CATCH_END
;
2986 bool Term::isReal64Value() const
2988 CVC5_API_TRY_CATCH_BEGIN
;
2989 CVC5_API_CHECK_NOT_NULL
;
2990 //////// all checks before this line
2991 return detail::isReal64(*d_node
);
2993 CVC5_API_TRY_CATCH_END
;
2995 std::pair
<std::int64_t, std::uint64_t> Term::getReal64Value() const
2997 CVC5_API_TRY_CATCH_BEGIN
;
2998 CVC5_API_CHECK_NOT_NULL
;
2999 CVC5_API_ARG_CHECK_EXPECTED(detail::isReal64(*d_node
), *d_node
)
3000 << "Term to be a 64-bit rational value when calling getReal64Value()";
3001 //////// all checks before this line
3002 const Rational
& r
= detail::getRational(*d_node
);
3003 return std::make_pair(r
.getNumerator().getLong(),
3004 r
.getDenominator().getUnsignedLong());
3006 CVC5_API_TRY_CATCH_END
;
3008 bool Term::isRealValue() const
3010 CVC5_API_TRY_CATCH_BEGIN
;
3011 CVC5_API_CHECK_NOT_NULL
;
3012 //////// all checks before this line
3013 return detail::isReal(*d_node
);
3015 CVC5_API_TRY_CATCH_END
;
3017 std::string
Term::getRealValue() const
3019 CVC5_API_TRY_CATCH_BEGIN
;
3020 CVC5_API_CHECK_NOT_NULL
;
3021 CVC5_API_ARG_CHECK_EXPECTED(detail::isReal(*d_node
), *d_node
)
3022 << "Term to be a rational value when calling getRealValue()";
3023 //////// all checks before this line
3024 const Rational
& rat
= detail::getRational(*d_node
);
3025 std::string res
= rat
.toString();
3026 if (rat
.isIntegral())
3032 CVC5_API_TRY_CATCH_END
;
3035 bool Term::isConstArray() const
3037 CVC5_API_TRY_CATCH_BEGIN
;
3038 CVC5_API_CHECK_NOT_NULL
;
3039 //////// all checks before this line
3040 return d_node
->getKind() == cvc5::Kind::STORE_ALL
;
3042 CVC5_API_TRY_CATCH_END
;
3044 Term
Term::getConstArrayBase() const
3046 CVC5_API_TRY_CATCH_BEGIN
;
3047 CVC5_API_CHECK_NOT_NULL
;
3048 CVC5_API_ARG_CHECK_EXPECTED(d_node
->getKind() == cvc5::Kind::STORE_ALL
,
3050 << "Term to be a constant array when calling getConstArrayBase()";
3051 //////// all checks before this line
3052 const auto& ar
= d_node
->getConst
<ArrayStoreAll
>();
3053 return Term(d_solver
, ar
.getValue());
3055 CVC5_API_TRY_CATCH_END
;
3058 bool Term::isBooleanValue() const
3060 CVC5_API_TRY_CATCH_BEGIN
;
3061 CVC5_API_CHECK_NOT_NULL
;
3062 //////// all checks before this line
3063 return d_node
->getKind() == cvc5::Kind::CONST_BOOLEAN
;
3065 CVC5_API_TRY_CATCH_END
;
3067 bool Term::getBooleanValue() const
3069 CVC5_API_TRY_CATCH_BEGIN
;
3070 CVC5_API_CHECK_NOT_NULL
;
3071 CVC5_API_ARG_CHECK_EXPECTED(d_node
->getKind() == cvc5::Kind::CONST_BOOLEAN
,
3073 << "Term to be a Boolean value when calling getBooleanValue()";
3074 //////// all checks before this line
3075 return d_node
->getConst
<bool>();
3077 CVC5_API_TRY_CATCH_END
;
3080 bool Term::isBitVectorValue() const
3082 CVC5_API_TRY_CATCH_BEGIN
;
3083 CVC5_API_CHECK_NOT_NULL
;
3084 //////// all checks before this line
3085 return d_node
->getKind() == cvc5::Kind::CONST_BITVECTOR
;
3087 CVC5_API_TRY_CATCH_END
;
3089 std::string
Term::getBitVectorValue(std::uint32_t base
) const
3091 CVC5_API_TRY_CATCH_BEGIN
;
3092 CVC5_API_CHECK_NOT_NULL
;
3093 CVC5_API_ARG_CHECK_EXPECTED(d_node
->getKind() == cvc5::Kind::CONST_BITVECTOR
,
3095 << "Term to be a bit-vector value when calling getBitVectorValue()";
3096 //////// all checks before this line
3097 return d_node
->getConst
<BitVector
>().toString(base
);
3099 CVC5_API_TRY_CATCH_END
;
3102 bool Term::isAbstractValue() const
3104 CVC5_API_TRY_CATCH_BEGIN
;
3105 CVC5_API_CHECK_NOT_NULL
;
3106 //////// all checks before this line
3107 return d_node
->getKind() == cvc5::Kind::ABSTRACT_VALUE
;
3109 CVC5_API_TRY_CATCH_END
;
3111 std::string
Term::getAbstractValue() const
3113 CVC5_API_TRY_CATCH_BEGIN
;
3114 CVC5_API_CHECK_NOT_NULL
;
3115 CVC5_API_ARG_CHECK_EXPECTED(d_node
->getKind() == cvc5::Kind::ABSTRACT_VALUE
,
3117 << "Term to be an abstract value when calling "
3118 "getAbstractValue()";
3119 //////// all checks before this line
3120 return d_node
->getConst
<AbstractValue
>().getIndex().toString();
3122 CVC5_API_TRY_CATCH_END
;
3125 bool Term::isTupleValue() const
3127 CVC5_API_TRY_CATCH_BEGIN
;
3128 CVC5_API_CHECK_NOT_NULL
;
3129 //////// all checks before this line
3130 return d_node
->getKind() == cvc5::Kind::APPLY_CONSTRUCTOR
&& d_node
->isConst()
3131 && d_node
->getType().getDType().isTuple();
3133 CVC5_API_TRY_CATCH_END
;
3135 std::vector
<Term
> Term::getTupleValue() const
3137 CVC5_API_TRY_CATCH_BEGIN
;
3138 CVC5_API_CHECK_NOT_NULL
;
3139 CVC5_API_ARG_CHECK_EXPECTED(d_node
->getKind() == cvc5::Kind::APPLY_CONSTRUCTOR
3140 && d_node
->isConst()
3141 && d_node
->getType().getDType().isTuple(),
3143 << "Term to be a tuple value when calling getTupleValue()";
3144 //////// all checks before this line
3145 std::vector
<Term
> res
;
3146 for (size_t i
= 0, n
= d_node
->getNumChildren(); i
< n
; ++i
)
3148 res
.emplace_back(Term(d_solver
, (*d_node
)[i
]));
3152 CVC5_API_TRY_CATCH_END
;
3155 bool Term::isFloatingPointPosZero() const
3157 CVC5_API_TRY_CATCH_BEGIN
;
3158 CVC5_API_CHECK_NOT_NULL
;
3159 //////// all checks before this line
3160 if (d_node
->getKind() == cvc5::Kind::CONST_FLOATINGPOINT
)
3162 const auto& fp
= d_node
->getConst
<FloatingPoint
>();
3163 return fp
.isZero() && fp
.isPositive();
3167 CVC5_API_TRY_CATCH_END
;
3169 bool Term::isFloatingPointNegZero() const
3171 CVC5_API_TRY_CATCH_BEGIN
;
3172 CVC5_API_CHECK_NOT_NULL
;
3173 //////// all checks before this line
3174 if (d_node
->getKind() == cvc5::Kind::CONST_FLOATINGPOINT
)
3176 const auto& fp
= d_node
->getConst
<FloatingPoint
>();
3177 return fp
.isZero() && fp
.isNegative();
3181 CVC5_API_TRY_CATCH_END
;
3183 bool Term::isFloatingPointPosInf() const
3185 CVC5_API_TRY_CATCH_BEGIN
;
3186 CVC5_API_CHECK_NOT_NULL
;
3187 //////// all checks before this line
3188 if (d_node
->getKind() == cvc5::Kind::CONST_FLOATINGPOINT
)
3190 const auto& fp
= d_node
->getConst
<FloatingPoint
>();
3191 return fp
.isInfinite() && fp
.isPositive();
3195 CVC5_API_TRY_CATCH_END
;
3197 bool Term::isFloatingPointNegInf() const
3199 CVC5_API_TRY_CATCH_BEGIN
;
3200 CVC5_API_CHECK_NOT_NULL
;
3201 //////// all checks before this line
3202 if (d_node
->getKind() == cvc5::Kind::CONST_FLOATINGPOINT
)
3204 const auto& fp
= d_node
->getConst
<FloatingPoint
>();
3205 return fp
.isInfinite() && fp
.isNegative();
3209 CVC5_API_TRY_CATCH_END
;
3211 bool Term::isFloatingPointNaN() const
3213 CVC5_API_TRY_CATCH_BEGIN
;
3214 CVC5_API_CHECK_NOT_NULL
;
3215 //////// all checks before this line
3216 return d_node
->getKind() == cvc5::Kind::CONST_FLOATINGPOINT
3217 && d_node
->getConst
<FloatingPoint
>().isNaN();
3219 CVC5_API_TRY_CATCH_END
;
3221 bool Term::isFloatingPointValue() const
3223 CVC5_API_TRY_CATCH_BEGIN
;
3224 CVC5_API_CHECK_NOT_NULL
;
3225 //////// all checks before this line
3226 return d_node
->getKind() == cvc5::Kind::CONST_FLOATINGPOINT
;
3228 CVC5_API_TRY_CATCH_END
;
3230 std::tuple
<std::uint32_t, std::uint32_t, Term
> Term::getFloatingPointValue()
3233 CVC5_API_TRY_CATCH_BEGIN
;
3234 CVC5_API_CHECK_NOT_NULL
;
3235 CVC5_API_ARG_CHECK_EXPECTED(
3236 d_node
->getKind() == cvc5::Kind::CONST_FLOATINGPOINT
, *d_node
)
3237 << "Term to be a floating-point value when calling "
3238 "getFloatingPointValue()";
3239 //////// all checks before this line
3240 const auto& fp
= d_node
->getConst
<FloatingPoint
>();
3241 return std::make_tuple(fp
.getSize().exponentWidth(),
3242 fp
.getSize().significandWidth(),
3243 d_solver
->mkValHelper
<BitVector
>(fp
.pack()));
3245 CVC5_API_TRY_CATCH_END
;
3248 bool Term::isSetValue() const
3250 CVC5_API_TRY_CATCH_BEGIN
;
3251 CVC5_API_CHECK_NOT_NULL
;
3252 //////// all checks before this line
3253 return d_node
->getType().isSet() && d_node
->isConst();
3255 CVC5_API_TRY_CATCH_END
;
3258 void Term::collectSet(std::set
<Term
>& set
,
3259 const cvc5::Node
& node
,
3262 // We asserted that node has a set type, and node.isConst()
3263 // Thus, node only contains of EMPTYSET, UNION and SINGLETON.
3264 switch (node
.getKind())
3266 case cvc5::Kind::EMPTYSET
: break;
3267 case cvc5::Kind::SINGLETON
: set
.emplace(Term(slv
, node
[0])); break;
3268 case cvc5::Kind::UNION
:
3270 for (const auto& sub
: node
)
3272 collectSet(set
, sub
, slv
);
3277 CVC5_API_ARG_CHECK_EXPECTED(false, node
)
3278 << "Term to be a set value when calling getSetValue()";
3283 std::set
<Term
> Term::getSetValue() const
3285 CVC5_API_TRY_CATCH_BEGIN
;
3286 CVC5_API_CHECK_NOT_NULL
;
3287 CVC5_API_ARG_CHECK_EXPECTED(d_node
->getType().isSet() && d_node
->isConst(),
3289 << "Term to be a set value when calling getSetValue()";
3290 //////// all checks before this line
3292 Term::collectSet(res
, *d_node
, d_solver
);
3295 CVC5_API_TRY_CATCH_END
;
3298 bool Term::isSequenceValue() const
3300 CVC5_API_TRY_CATCH_BEGIN
;
3301 CVC5_API_CHECK_NOT_NULL
;
3302 //////// all checks before this line
3303 return d_node
->getKind() == cvc5::Kind::CONST_SEQUENCE
;
3305 CVC5_API_TRY_CATCH_END
;
3307 std::vector
<Term
> Term::getSequenceValue() const
3309 CVC5_API_TRY_CATCH_BEGIN
;
3310 CVC5_API_CHECK_NOT_NULL
;
3311 CVC5_API_ARG_CHECK_EXPECTED(d_node
->getKind() == cvc5::Kind::CONST_SEQUENCE
,
3313 << "Term to be a sequence value when calling getSequenceValue()";
3314 //////// all checks before this line
3315 std::vector
<Term
> res
;
3316 const Sequence
& seq
= d_node
->getConst
<Sequence
>();
3317 for (const auto& node
: seq
.getVec())
3319 res
.emplace_back(Term(d_solver
, node
));
3323 CVC5_API_TRY_CATCH_END
;
3326 bool Term::isUninterpretedValue() const
3328 CVC5_API_TRY_CATCH_BEGIN
;
3329 CVC5_API_CHECK_NOT_NULL
;
3330 //////// all checks before this line
3331 return d_node
->getKind() == cvc5::Kind::UNINTERPRETED_CONSTANT
;
3333 CVC5_API_TRY_CATCH_END
;
3335 std::pair
<Sort
, std::int32_t> Term::getUninterpretedValue() const
3337 CVC5_API_TRY_CATCH_BEGIN
;
3338 CVC5_API_CHECK_NOT_NULL
;
3339 CVC5_API_ARG_CHECK_EXPECTED(
3340 d_node
->getKind() == cvc5::Kind::UNINTERPRETED_CONSTANT
, *d_node
)
3341 << "Term to be an uninterpreted value when calling "
3342 "getUninterpretedValue()";
3343 //////// all checks before this line
3344 const auto& uc
= d_node
->getConst
<UninterpretedConstant
>();
3345 return std::make_pair(Sort(d_solver
, uc
.getType()),
3346 uc
.getIndex().toUnsignedInt());
3348 CVC5_API_TRY_CATCH_END
;
3351 std::ostream
& operator<<(std::ostream
& out
, const Term
& t
)
3353 out
<< t
.toString();
3357 std::ostream
& operator<<(std::ostream
& out
, const std::vector
<Term
>& vector
)
3359 container_to_stream(out
, vector
);
3363 std::ostream
& operator<<(std::ostream
& out
, const std::set
<Term
>& set
)
3365 container_to_stream(out
, set
);
3369 std::ostream
& operator<<(std::ostream
& out
,
3370 const std::unordered_set
<Term
>& unordered_set
)
3372 container_to_stream(out
, unordered_set
);
3376 template <typename V
>
3377 std::ostream
& operator<<(std::ostream
& out
, const std::map
<Term
, V
>& map
)
3379 container_to_stream(out
, map
);
3383 template <typename V
>
3384 std::ostream
& operator<<(std::ostream
& out
,
3385 const std::unordered_map
<Term
, V
>& unordered_map
)
3387 container_to_stream(out
, unordered_map
);
3392 /* -------------------------------------------------------------------------- */
3394 /* Split out to avoid nested API calls (problematic with API tracing). */
3395 /* .......................................................................... */
3397 bool Term::isNullHelper() const
3399 /* Split out to avoid nested API calls (problematic with API tracing). */
3400 return d_node
->isNull();
3403 Kind
Term::getKindHelper() const
3405 /* Sequence kinds do not exist internally, so we must convert their internal
3406 * (string) versions back to sequence. All operators where this is
3407 * necessary are such that their first child is of sequence type, which
3409 if (d_node
->getNumChildren() > 0 && (*d_node
)[0].getType().isSequence())
3411 switch (d_node
->getKind())
3413 case cvc5::Kind::STRING_CONCAT
: return SEQ_CONCAT
;
3414 case cvc5::Kind::STRING_LENGTH
: return SEQ_LENGTH
;
3415 case cvc5::Kind::STRING_SUBSTR
: return SEQ_EXTRACT
;
3416 case cvc5::Kind::STRING_UPDATE
: return SEQ_UPDATE
;
3417 case cvc5::Kind::STRING_CHARAT
: return SEQ_AT
;
3418 case cvc5::Kind::STRING_CONTAINS
: return SEQ_CONTAINS
;
3419 case cvc5::Kind::STRING_INDEXOF
: return SEQ_INDEXOF
;
3420 case cvc5::Kind::STRING_REPLACE
: return SEQ_REPLACE
;
3421 case cvc5::Kind::STRING_REPLACE_ALL
: return SEQ_REPLACE_ALL
;
3422 case cvc5::Kind::STRING_REV
: return SEQ_REV
;
3423 case cvc5::Kind::STRING_PREFIX
: return SEQ_PREFIX
;
3424 case cvc5::Kind::STRING_SUFFIX
: return SEQ_SUFFIX
;
3426 // fall through to conversion below
3430 // Notice that kinds like APPLY_TYPE_ASCRIPTION will be converted to
3434 return CONST_RATIONAL
;
3436 return intToExtKind(d_node
->getKind());
3439 bool Term::isCastedReal() const
3441 if (d_node
->getKind() == kind::CAST_TO_REAL
)
3443 return (*d_node
)[0].isConst() && (*d_node
)[0].getType().isInteger();
3448 /* -------------------------------------------------------------------------- */
3450 /* -------------------------------------------------------------------------- */
3452 /* DatatypeConstructorDecl -------------------------------------------------- */
3454 DatatypeConstructorDecl::DatatypeConstructorDecl()
3455 : d_solver(nullptr), d_ctor(nullptr)
3459 DatatypeConstructorDecl::DatatypeConstructorDecl(const Solver
* slv
,
3460 const std::string
& name
)
3461 : d_solver(slv
), d_ctor(new cvc5::DTypeConstructor(name
))
3464 DatatypeConstructorDecl::~DatatypeConstructorDecl()
3466 if (d_ctor
!= nullptr)
3468 // ensure proper node manager is in scope
3469 NodeManagerScope
scope(d_solver
->getNodeManager());
3474 void DatatypeConstructorDecl::addSelector(const std::string
& name
,
3477 NodeManagerScope
scope(d_solver
->getNodeManager());
3478 CVC5_API_TRY_CATCH_BEGIN
;
3479 CVC5_API_CHECK_NOT_NULL
;
3480 CVC5_API_CHECK_SORT(sort
);
3481 CVC5_API_ARG_CHECK_EXPECTED(!sort
.isNull(), sort
)
3482 << "non-null range sort for selector";
3483 //////// all checks before this line
3484 d_ctor
->addArg(name
, *sort
.d_type
);
3486 CVC5_API_TRY_CATCH_END
;
3489 void DatatypeConstructorDecl::addSelectorSelf(const std::string
& name
)
3491 NodeManagerScope
scope(d_solver
->getNodeManager());
3492 CVC5_API_TRY_CATCH_BEGIN
;
3493 CVC5_API_CHECK_NOT_NULL
;
3494 //////// all checks before this line
3495 d_ctor
->addArgSelf(name
);
3497 CVC5_API_TRY_CATCH_END
;
3500 bool DatatypeConstructorDecl::isNull() const
3502 CVC5_API_TRY_CATCH_BEGIN
;
3503 //////// all checks before this line
3504 return isNullHelper();
3506 CVC5_API_TRY_CATCH_END
;
3509 std::string
DatatypeConstructorDecl::toString() const
3511 CVC5_API_TRY_CATCH_BEGIN
;
3512 //////// all checks before this line
3513 std::stringstream ss
;
3517 CVC5_API_TRY_CATCH_END
;
3520 std::ostream
& operator<<(std::ostream
& out
,
3521 const DatatypeConstructorDecl
& ctordecl
)
3523 out
<< ctordecl
.toString();
3527 std::ostream
& operator<<(std::ostream
& out
,
3528 const std::vector
<DatatypeConstructorDecl
>& vector
)
3530 container_to_stream(out
, vector
);
3534 bool DatatypeConstructorDecl::isNullHelper() const { return d_ctor
== nullptr; }
3536 /* DatatypeDecl ------------------------------------------------------------- */
3538 DatatypeDecl::DatatypeDecl() : d_solver(nullptr), d_dtype(nullptr) {}
3540 DatatypeDecl::DatatypeDecl(const Solver
* slv
,
3541 const std::string
& name
,
3543 : d_solver(slv
), d_dtype(new cvc5::DType(name
, isCoDatatype
))
3547 DatatypeDecl::DatatypeDecl(const Solver
* slv
,
3548 const std::string
& name
,
3552 d_dtype(new cvc5::DType(
3553 name
, std::vector
<TypeNode
>{*param
.d_type
}, isCoDatatype
))
3557 DatatypeDecl::DatatypeDecl(const Solver
* slv
,
3558 const std::string
& name
,
3559 const std::vector
<Sort
>& params
,
3563 std::vector
<TypeNode
> tparams
= Sort::sortVectorToTypeNodes(params
);
3564 d_dtype
= std::shared_ptr
<cvc5::DType
>(
3565 new cvc5::DType(name
, tparams
, isCoDatatype
));
3568 bool DatatypeDecl::isNullHelper() const { return !d_dtype
; }
3570 DatatypeDecl::~DatatypeDecl()
3572 if (d_dtype
!= nullptr)
3574 // ensure proper node manager is in scope
3575 NodeManagerScope
scope(d_solver
->getNodeManager());
3580 void DatatypeDecl::addConstructor(const DatatypeConstructorDecl
& ctor
)
3582 NodeManagerScope
scope(d_solver
->getNodeManager());
3583 CVC5_API_TRY_CATCH_BEGIN
;
3584 CVC5_API_CHECK_NOT_NULL
;
3585 CVC5_API_ARG_CHECK_NOT_NULL(ctor
);
3586 CVC5_API_ARG_CHECK_SOLVER("datatype constructor declaration", ctor
);
3587 //////// all checks before this line
3588 d_dtype
->addConstructor(ctor
.d_ctor
);
3590 CVC5_API_TRY_CATCH_END
;
3593 size_t DatatypeDecl::getNumConstructors() const
3595 CVC5_API_TRY_CATCH_BEGIN
;
3596 CVC5_API_CHECK_NOT_NULL
;
3597 //////// all checks before this line
3598 return d_dtype
->getNumConstructors();
3600 CVC5_API_TRY_CATCH_END
;
3603 bool DatatypeDecl::isParametric() const
3605 CVC5_API_TRY_CATCH_BEGIN
;
3606 CVC5_API_CHECK_NOT_NULL
;
3607 //////// all checks before this line
3608 return d_dtype
->isParametric();
3610 CVC5_API_TRY_CATCH_END
;
3613 std::string
DatatypeDecl::toString() const
3615 CVC5_API_TRY_CATCH_BEGIN
;
3616 CVC5_API_CHECK_NOT_NULL
;
3617 //////// all checks before this line
3618 std::stringstream ss
;
3622 CVC5_API_TRY_CATCH_END
;
3625 std::string
DatatypeDecl::getName() const
3627 CVC5_API_TRY_CATCH_BEGIN
;
3628 CVC5_API_CHECK_NOT_NULL
;
3629 //////// all checks before this line
3630 return d_dtype
->getName();
3632 CVC5_API_TRY_CATCH_END
;
3635 bool DatatypeDecl::isNull() const
3637 CVC5_API_TRY_CATCH_BEGIN
;
3638 //////// all checks before this line
3639 return isNullHelper();
3641 CVC5_API_TRY_CATCH_END
;
3644 std::ostream
& operator<<(std::ostream
& out
, const DatatypeDecl
& dtdecl
)
3646 out
<< dtdecl
.toString();
3650 cvc5::DType
& DatatypeDecl::getDatatype(void) const { return *d_dtype
; }
3652 /* DatatypeSelector --------------------------------------------------------- */
3654 DatatypeSelector::DatatypeSelector() : d_solver(nullptr), d_stor(nullptr) {}
3656 DatatypeSelector::DatatypeSelector(const Solver
* slv
,
3657 const cvc5::DTypeSelector
& stor
)
3658 : d_solver(slv
), d_stor(new cvc5::DTypeSelector(stor
))
3660 CVC5_API_CHECK(d_stor
->isResolved()) << "Expected resolved datatype selector";
3663 DatatypeSelector::~DatatypeSelector()
3665 if (d_stor
!= nullptr)
3667 // ensure proper node manager is in scope
3668 NodeManagerScope
scope(d_solver
->getNodeManager());
3673 std::string
DatatypeSelector::getName() const
3675 CVC5_API_TRY_CATCH_BEGIN
;
3676 CVC5_API_CHECK_NOT_NULL
;
3677 //////// all checks before this line
3678 return d_stor
->getName();
3680 CVC5_API_TRY_CATCH_END
;
3683 Term
DatatypeSelector::getSelectorTerm() const
3685 CVC5_API_TRY_CATCH_BEGIN
;
3686 CVC5_API_CHECK_NOT_NULL
;
3687 //////// all checks before this line
3688 return Term(d_solver
, d_stor
->getSelector());
3690 CVC5_API_TRY_CATCH_END
;
3692 Term
DatatypeSelector::getUpdaterTerm() const
3694 CVC5_API_TRY_CATCH_BEGIN
;
3695 CVC5_API_CHECK_NOT_NULL
;
3696 //////// all checks before this line
3697 return Term(d_solver
, d_stor
->getUpdater());
3699 CVC5_API_TRY_CATCH_END
;
3702 Sort
DatatypeSelector::getRangeSort() const
3704 CVC5_API_TRY_CATCH_BEGIN
;
3705 CVC5_API_CHECK_NOT_NULL
;
3706 //////// all checks before this line
3707 return Sort(d_solver
, d_stor
->getRangeType());
3709 CVC5_API_TRY_CATCH_END
;
3712 bool DatatypeSelector::isNull() const
3714 CVC5_API_TRY_CATCH_BEGIN
;
3715 //////// all checks before this line
3716 return isNullHelper();
3718 CVC5_API_TRY_CATCH_END
;
3721 std::string
DatatypeSelector::toString() const
3723 CVC5_API_TRY_CATCH_BEGIN
;
3724 //////// all checks before this line
3725 std::stringstream ss
;
3729 CVC5_API_TRY_CATCH_END
;
3732 std::ostream
& operator<<(std::ostream
& out
, const DatatypeSelector
& stor
)
3734 out
<< stor
.toString();
3738 bool DatatypeSelector::isNullHelper() const { return d_stor
== nullptr; }
3740 /* DatatypeConstructor ------------------------------------------------------ */
3742 DatatypeConstructor::DatatypeConstructor() : d_solver(nullptr), d_ctor(nullptr)
3746 DatatypeConstructor::DatatypeConstructor(const Solver
* slv
,
3747 const cvc5::DTypeConstructor
& ctor
)
3748 : d_solver(slv
), d_ctor(new cvc5::DTypeConstructor(ctor
))
3750 CVC5_API_CHECK(d_ctor
->isResolved())
3751 << "Expected resolved datatype constructor";
3754 DatatypeConstructor::~DatatypeConstructor()
3756 if (d_ctor
!= nullptr)
3758 // ensure proper node manager is in scope
3759 NodeManagerScope
scope(d_solver
->getNodeManager());
3764 std::string
DatatypeConstructor::getName() const
3766 CVC5_API_TRY_CATCH_BEGIN
;
3767 CVC5_API_CHECK_NOT_NULL
;
3768 //////// all checks before this line
3769 return d_ctor
->getName();
3771 CVC5_API_TRY_CATCH_END
;
3774 Term
DatatypeConstructor::getConstructorTerm() const
3776 CVC5_API_TRY_CATCH_BEGIN
;
3777 CVC5_API_CHECK_NOT_NULL
;
3778 //////// all checks before this line
3779 return Term(d_solver
, d_ctor
->getConstructor());
3781 CVC5_API_TRY_CATCH_END
;
3784 Term
DatatypeConstructor::getSpecializedConstructorTerm(
3785 const Sort
& retSort
) const
3787 NodeManagerScope
scope(d_solver
->getNodeManager());
3788 CVC5_API_TRY_CATCH_BEGIN
;
3789 CVC5_API_CHECK_NOT_NULL
;
3790 CVC5_API_CHECK(d_ctor
->isResolved())
3791 << "Expected resolved datatype constructor";
3792 CVC5_API_CHECK(retSort
.isDatatype())
3793 << "Cannot get specialized constructor type for non-datatype type "
3795 //////// all checks before this line
3797 NodeManager
* nm
= d_solver
->getNodeManager();
3799 nm
->mkNode(kind::APPLY_TYPE_ASCRIPTION
,
3800 nm
->mkConst(AscriptionType(
3801 d_ctor
->getSpecializedConstructorType(*retSort
.d_type
))),
3802 d_ctor
->getConstructor());
3803 (void)ret
.getType(true); /* kick off type checking */
3804 // apply type ascription to the operator
3805 Term sctor
= api::Term(d_solver
, ret
);
3808 CVC5_API_TRY_CATCH_END
;
3811 Term
DatatypeConstructor::getTesterTerm() const
3813 CVC5_API_TRY_CATCH_BEGIN
;
3814 CVC5_API_CHECK_NOT_NULL
;
3815 //////// all checks before this line
3816 return Term(d_solver
, d_ctor
->getTester());
3818 CVC5_API_TRY_CATCH_END
;
3821 size_t DatatypeConstructor::getNumSelectors() const
3823 CVC5_API_TRY_CATCH_BEGIN
;
3824 CVC5_API_CHECK_NOT_NULL
;
3825 //////// all checks before this line
3826 return d_ctor
->getNumArgs();
3828 CVC5_API_TRY_CATCH_END
;
3831 DatatypeSelector
DatatypeConstructor::operator[](size_t index
) const
3833 CVC5_API_TRY_CATCH_BEGIN
;
3834 CVC5_API_CHECK_NOT_NULL
;
3835 //////// all checks before this line
3836 return DatatypeSelector(d_solver
, (*d_ctor
)[index
]);
3838 CVC5_API_TRY_CATCH_END
;
3841 DatatypeSelector
DatatypeConstructor::operator[](const std::string
& name
) const
3843 CVC5_API_TRY_CATCH_BEGIN
;
3844 CVC5_API_CHECK_NOT_NULL
;
3845 //////// all checks before this line
3846 return getSelectorForName(name
);
3848 CVC5_API_TRY_CATCH_END
;
3851 DatatypeSelector
DatatypeConstructor::getSelector(const std::string
& name
) const
3853 CVC5_API_TRY_CATCH_BEGIN
;
3854 CVC5_API_CHECK_NOT_NULL
;
3855 //////// all checks before this line
3856 return getSelectorForName(name
);
3858 CVC5_API_TRY_CATCH_END
;
3861 Term
DatatypeConstructor::getSelectorTerm(const std::string
& name
) const
3863 CVC5_API_TRY_CATCH_BEGIN
;
3864 CVC5_API_CHECK_NOT_NULL
;
3865 //////// all checks before this line
3866 return getSelector(name
).getSelectorTerm();
3868 CVC5_API_TRY_CATCH_END
;
3871 DatatypeConstructor::const_iterator
DatatypeConstructor::begin() const
3873 return DatatypeConstructor::const_iterator(d_solver
, *d_ctor
, true);
3876 DatatypeConstructor::const_iterator
DatatypeConstructor::end() const
3878 return DatatypeConstructor::const_iterator(d_solver
, *d_ctor
, false);
3881 DatatypeConstructor::const_iterator::const_iterator(
3882 const Solver
* slv
, const cvc5::DTypeConstructor
& ctor
, bool begin
)
3885 d_int_stors
= &ctor
.getArgs();
3887 const std::vector
<std::shared_ptr
<cvc5::DTypeSelector
>>& sels
=
3889 for (const std::shared_ptr
<cvc5::DTypeSelector
>& s
: sels
)
3891 /* Can not use emplace_back here since constructor is private. */
3892 d_stors
.push_back(DatatypeSelector(d_solver
, *s
.get()));
3894 d_idx
= begin
? 0 : sels
.size();
3897 DatatypeConstructor::const_iterator::const_iterator()
3898 : d_solver(nullptr), d_int_stors(nullptr), d_idx(0)
3902 DatatypeConstructor::const_iterator
&
3903 DatatypeConstructor::const_iterator::operator=(
3904 const DatatypeConstructor::const_iterator
& it
)
3906 d_solver
= it
.d_solver
;
3907 d_int_stors
= it
.d_int_stors
;
3908 d_stors
= it
.d_stors
;
3913 const DatatypeSelector
& DatatypeConstructor::const_iterator::operator*() const
3915 return d_stors
[d_idx
];
3918 const DatatypeSelector
* DatatypeConstructor::const_iterator::operator->() const
3920 return &d_stors
[d_idx
];
3923 DatatypeConstructor::const_iterator
&
3924 DatatypeConstructor::const_iterator::operator++()
3930 DatatypeConstructor::const_iterator
3931 DatatypeConstructor::const_iterator::operator++(int)
3933 DatatypeConstructor::const_iterator
it(*this);
3938 bool DatatypeConstructor::const_iterator::operator==(
3939 const DatatypeConstructor::const_iterator
& other
) const
3941 return d_int_stors
== other
.d_int_stors
&& d_idx
== other
.d_idx
;
3944 bool DatatypeConstructor::const_iterator::operator!=(
3945 const DatatypeConstructor::const_iterator
& other
) const
3947 return d_int_stors
!= other
.d_int_stors
|| d_idx
!= other
.d_idx
;
3950 bool DatatypeConstructor::isNull() const
3952 CVC5_API_TRY_CATCH_BEGIN
;
3953 //////// all checks before this line
3954 return isNullHelper();
3956 CVC5_API_TRY_CATCH_END
;
3959 std::string
DatatypeConstructor::toString() const
3961 CVC5_API_TRY_CATCH_BEGIN
;
3962 //////// all checks before this line
3963 std::stringstream ss
;
3967 CVC5_API_TRY_CATCH_END
;
3970 bool DatatypeConstructor::isNullHelper() const { return d_ctor
== nullptr; }
3972 DatatypeSelector
DatatypeConstructor::getSelectorForName(
3973 const std::string
& name
) const
3975 bool foundSel
= false;
3977 for (size_t i
= 0, nsels
= getNumSelectors(); i
< nsels
; i
++)
3979 if ((*d_ctor
)[i
].getName() == name
)
3988 std::stringstream snames
;
3990 for (size_t i
= 0, ncons
= getNumSelectors(); i
< ncons
; i
++)
3992 snames
<< (*d_ctor
)[i
].getName() << " ";
3995 CVC5_API_CHECK(foundSel
) << "No selector " << name
<< " for constructor "
3996 << getName() << " exists among " << snames
.str();
3998 return DatatypeSelector(d_solver
, (*d_ctor
)[index
]);
4001 std::ostream
& operator<<(std::ostream
& out
, const DatatypeConstructor
& ctor
)
4003 out
<< ctor
.toString();
4007 /* Datatype ----------------------------------------------------------------- */
4009 Datatype::Datatype(const Solver
* slv
, const cvc5::DType
& dtype
)
4010 : d_solver(slv
), d_dtype(new cvc5::DType(dtype
))
4012 CVC5_API_CHECK(d_dtype
->isResolved()) << "Expected resolved datatype";
4015 Datatype::Datatype() : d_solver(nullptr), d_dtype(nullptr) {}
4017 Datatype::~Datatype()
4019 if (d_dtype
!= nullptr)
4021 // ensure proper node manager is in scope
4022 NodeManagerScope
scope(d_solver
->getNodeManager());
4027 DatatypeConstructor
Datatype::operator[](size_t idx
) const
4029 CVC5_API_TRY_CATCH_BEGIN
;
4030 CVC5_API_CHECK_NOT_NULL
;
4031 CVC5_API_CHECK(idx
< getNumConstructors()) << "Index out of bounds.";
4032 //////// all checks before this line
4033 return DatatypeConstructor(d_solver
, (*d_dtype
)[idx
]);
4035 CVC5_API_TRY_CATCH_END
;
4038 DatatypeConstructor
Datatype::operator[](const std::string
& name
) const
4040 CVC5_API_TRY_CATCH_BEGIN
;
4041 CVC5_API_CHECK_NOT_NULL
;
4042 //////// all checks before this line
4043 return getConstructorForName(name
);
4045 CVC5_API_TRY_CATCH_END
;
4048 DatatypeConstructor
Datatype::getConstructor(const std::string
& name
) const
4050 CVC5_API_TRY_CATCH_BEGIN
;
4051 CVC5_API_CHECK_NOT_NULL
;
4052 //////// all checks before this line
4053 return getConstructorForName(name
);
4055 CVC5_API_TRY_CATCH_END
;
4058 Term
Datatype::getConstructorTerm(const std::string
& name
) const
4060 CVC5_API_TRY_CATCH_BEGIN
;
4061 CVC5_API_CHECK_NOT_NULL
;
4062 //////// all checks before this line
4063 return getConstructorForName(name
).getConstructorTerm();
4065 CVC5_API_TRY_CATCH_END
;
4068 DatatypeSelector
Datatype::getSelector(const std::string
& name
) const
4070 CVC5_API_TRY_CATCH_BEGIN
;
4071 CVC5_API_CHECK_NOT_NULL
;
4072 //////// all checks before this line
4073 return getSelectorForName(name
);
4075 CVC5_API_TRY_CATCH_END
;
4078 std::string
Datatype::getName() const
4080 CVC5_API_TRY_CATCH_BEGIN
;
4081 CVC5_API_CHECK_NOT_NULL
;
4082 //////// all checks before this line
4083 return d_dtype
->getName();
4085 CVC5_API_TRY_CATCH_END
;
4088 size_t Datatype::getNumConstructors() const
4090 CVC5_API_TRY_CATCH_BEGIN
;
4091 CVC5_API_CHECK_NOT_NULL
;
4092 //////// all checks before this line
4093 return d_dtype
->getNumConstructors();
4095 CVC5_API_TRY_CATCH_END
;
4098 bool Datatype::isParametric() const
4100 CVC5_API_TRY_CATCH_BEGIN
;
4101 CVC5_API_CHECK_NOT_NULL
;
4102 //////// all checks before this line
4103 return d_dtype
->isParametric();
4105 CVC5_API_TRY_CATCH_END
;
4108 bool Datatype::isCodatatype() const
4110 CVC5_API_TRY_CATCH_BEGIN
;
4111 CVC5_API_CHECK_NOT_NULL
;
4112 //////// all checks before this line
4113 return d_dtype
->isCodatatype();
4115 CVC5_API_TRY_CATCH_END
;
4118 bool Datatype::isTuple() const
4120 CVC5_API_TRY_CATCH_BEGIN
;
4121 CVC5_API_CHECK_NOT_NULL
;
4122 //////// all checks before this line
4123 return d_dtype
->isTuple();
4125 CVC5_API_TRY_CATCH_END
;
4128 bool Datatype::isRecord() const
4130 CVC5_API_TRY_CATCH_BEGIN
;
4131 CVC5_API_CHECK_NOT_NULL
;
4132 //////// all checks before this line
4133 return d_dtype
->isRecord();
4135 CVC5_API_TRY_CATCH_END
;
4138 bool Datatype::isFinite() const
4140 CVC5_API_TRY_CATCH_BEGIN
;
4141 CVC5_API_CHECK_NOT_NULL
;
4142 //////// all checks before this line
4143 // we assume that finite model finding is disabled by passing false as the
4145 return isCardinalityClassFinite(d_dtype
->getCardinalityClass(), false);
4147 CVC5_API_TRY_CATCH_END
;
4150 bool Datatype::isWellFounded() const
4152 CVC5_API_TRY_CATCH_BEGIN
;
4153 CVC5_API_CHECK_NOT_NULL
;
4154 //////// all checks before this line
4155 return d_dtype
->isWellFounded();
4157 CVC5_API_TRY_CATCH_END
;
4159 bool Datatype::hasNestedRecursion() const
4161 CVC5_API_TRY_CATCH_BEGIN
;
4162 CVC5_API_CHECK_NOT_NULL
;
4163 //////// all checks before this line
4164 return d_dtype
->hasNestedRecursion();
4166 CVC5_API_TRY_CATCH_END
;
4169 bool Datatype::isNull() const
4171 CVC5_API_TRY_CATCH_BEGIN
;
4172 CVC5_API_CHECK_NOT_NULL
;
4173 //////// all checks before this line
4174 return isNullHelper();
4176 CVC5_API_TRY_CATCH_END
;
4179 std::string
Datatype::toString() const
4181 CVC5_API_TRY_CATCH_BEGIN
;
4182 CVC5_API_CHECK_NOT_NULL
;
4183 //////// all checks before this line
4184 return d_dtype
->getName();
4186 CVC5_API_TRY_CATCH_END
;
4189 Datatype::const_iterator
Datatype::begin() const
4191 return Datatype::const_iterator(d_solver
, *d_dtype
, true);
4194 Datatype::const_iterator
Datatype::end() const
4196 return Datatype::const_iterator(d_solver
, *d_dtype
, false);
4199 DatatypeConstructor
Datatype::getConstructorForName(
4200 const std::string
& name
) const
4202 bool foundCons
= false;
4204 for (size_t i
= 0, ncons
= getNumConstructors(); i
< ncons
; i
++)
4206 if ((*d_dtype
)[i
].getName() == name
)
4215 std::stringstream snames
;
4217 for (size_t i
= 0, ncons
= getNumConstructors(); i
< ncons
; i
++)
4219 snames
<< (*d_dtype
)[i
].getName() << " ";
4222 CVC5_API_CHECK(foundCons
) << "No constructor " << name
<< " for datatype "
4223 << getName() << " exists, among " << snames
.str();
4225 return DatatypeConstructor(d_solver
, (*d_dtype
)[index
]);
4228 DatatypeSelector
Datatype::getSelectorForName(const std::string
& name
) const
4230 bool foundSel
= false;
4233 for (size_t i
= 0, ncons
= getNumConstructors(); i
< ncons
; i
++)
4235 int si
= (*d_dtype
)[i
].getSelectorIndexForName(name
);
4238 sindex
= static_cast<size_t>(si
);
4246 CVC5_API_CHECK(foundSel
)
4247 << "No select " << name
<< " for datatype " << getName() << " exists";
4249 return DatatypeSelector(d_solver
, (*d_dtype
)[index
][sindex
]);
4252 Datatype::const_iterator::const_iterator(const Solver
* slv
,
4253 const cvc5::DType
& dtype
,
4255 : d_solver(slv
), d_int_ctors(&dtype
.getConstructors())
4257 const std::vector
<std::shared_ptr
<DTypeConstructor
>>& cons
=
4258 dtype
.getConstructors();
4259 for (const std::shared_ptr
<DTypeConstructor
>& c
: cons
)
4261 /* Can not use emplace_back here since constructor is private. */
4262 d_ctors
.push_back(DatatypeConstructor(d_solver
, *c
.get()));
4264 d_idx
= begin
? 0 : cons
.size();
4267 Datatype::const_iterator::const_iterator()
4268 : d_solver(nullptr), d_int_ctors(nullptr), d_idx(0)
4272 Datatype::const_iterator
& Datatype::const_iterator::operator=(
4273 const Datatype::const_iterator
& it
)
4275 d_solver
= it
.d_solver
;
4276 d_int_ctors
= it
.d_int_ctors
;
4277 d_ctors
= it
.d_ctors
;
4282 const DatatypeConstructor
& Datatype::const_iterator::operator*() const
4284 return d_ctors
[d_idx
];
4287 const DatatypeConstructor
* Datatype::const_iterator::operator->() const
4289 return &d_ctors
[d_idx
];
4292 Datatype::const_iterator
& Datatype::const_iterator::operator++()
4298 Datatype::const_iterator
Datatype::const_iterator::operator++(int)
4300 Datatype::const_iterator
it(*this);
4305 bool Datatype::const_iterator::operator==(
4306 const Datatype::const_iterator
& other
) const
4308 return d_int_ctors
== other
.d_int_ctors
&& d_idx
== other
.d_idx
;
4311 bool Datatype::const_iterator::operator!=(
4312 const Datatype::const_iterator
& other
) const
4314 return d_int_ctors
!= other
.d_int_ctors
|| d_idx
!= other
.d_idx
;
4317 bool Datatype::isNullHelper() const { return d_dtype
== nullptr; }
4319 /* -------------------------------------------------------------------------- */
4321 /* -------------------------------------------------------------------------- */
4324 : d_solver(nullptr),
4334 Grammar::Grammar(const Solver
* slv
,
4335 const std::vector
<Term
>& sygusVars
,
4336 const std::vector
<Term
>& ntSymbols
)
4338 d_sygusVars(sygusVars
),
4339 d_ntSyms(ntSymbols
),
4340 d_ntsToTerms(ntSymbols
.size()),
4345 for (Term ntsymbol
: d_ntSyms
)
4347 d_ntsToTerms
.emplace(ntsymbol
, std::vector
<Term
>());
4351 void Grammar::addRule(const Term
& ntSymbol
, const Term
& rule
)
4353 CVC5_API_TRY_CATCH_BEGIN
;
4354 CVC5_API_CHECK(!d_isResolved
) << "Grammar cannot be modified after passing "
4355 "it as an argument to synthFun/synthInv";
4356 CVC5_API_CHECK_TERM(ntSymbol
);
4357 CVC5_API_CHECK_TERM(rule
);
4358 CVC5_API_ARG_CHECK_EXPECTED(
4359 d_ntsToTerms
.find(ntSymbol
) != d_ntsToTerms
.cend(), ntSymbol
)
4360 << "ntSymbol to be one of the non-terminal symbols given in the "
4362 CVC5_API_CHECK(ntSymbol
.d_node
->getType() == rule
.d_node
->getType())
4363 << "Expected ntSymbol and rule to have the same sort";
4364 CVC5_API_ARG_CHECK_EXPECTED(!containsFreeVariables(rule
), rule
)
4365 << "a term whose free variables are limited to synthFun/synthInv "
4366 "parameters and non-terminal symbols of the grammar";
4367 //////// all checks before this line
4368 d_ntsToTerms
[ntSymbol
].push_back(rule
);
4370 CVC5_API_TRY_CATCH_END
;
4373 void Grammar::addRules(const Term
& ntSymbol
, const std::vector
<Term
>& rules
)
4375 CVC5_API_TRY_CATCH_BEGIN
;
4376 CVC5_API_CHECK(!d_isResolved
) << "Grammar cannot be modified after passing "
4377 "it as an argument to synthFun/synthInv";
4378 CVC5_API_CHECK_TERM(ntSymbol
);
4379 CVC5_API_CHECK_TERMS_WITH_SORT(rules
, ntSymbol
.getSort());
4380 CVC5_API_ARG_CHECK_EXPECTED(
4381 d_ntsToTerms
.find(ntSymbol
) != d_ntsToTerms
.cend(), ntSymbol
)
4382 << "ntSymbol to be one of the non-terminal symbols given in the "
4384 for (size_t i
= 0, n
= rules
.size(); i
< n
; ++i
)
4386 CVC5_API_ARG_AT_INDEX_CHECK_EXPECTED(
4387 !containsFreeVariables(rules
[i
]), rules
[i
], rules
, i
)
4388 << "a term whose free variables are limited to synthFun/synthInv "
4389 "parameters and non-terminal symbols of the grammar";
4391 //////// all checks before this line
4392 d_ntsToTerms
[ntSymbol
].insert(
4393 d_ntsToTerms
[ntSymbol
].cend(), rules
.cbegin(), rules
.cend());
4395 CVC5_API_TRY_CATCH_END
;
4398 void Grammar::addAnyConstant(const Term
& ntSymbol
)
4400 CVC5_API_TRY_CATCH_BEGIN
;
4401 CVC5_API_CHECK(!d_isResolved
) << "Grammar cannot be modified after passing "
4402 "it as an argument to synthFun/synthInv";
4403 CVC5_API_CHECK_TERM(ntSymbol
);
4404 CVC5_API_ARG_CHECK_EXPECTED(
4405 d_ntsToTerms
.find(ntSymbol
) != d_ntsToTerms
.cend(), ntSymbol
)
4406 << "ntSymbol to be one of the non-terminal symbols given in the "
4408 //////// all checks before this line
4409 d_allowConst
.insert(ntSymbol
);
4411 CVC5_API_TRY_CATCH_END
;
4414 void Grammar::addAnyVariable(const Term
& ntSymbol
)
4416 CVC5_API_TRY_CATCH_BEGIN
;
4417 CVC5_API_CHECK(!d_isResolved
) << "Grammar cannot be modified after passing "
4418 "it as an argument to synthFun/synthInv";
4419 CVC5_API_CHECK_TERM(ntSymbol
);
4420 CVC5_API_ARG_CHECK_EXPECTED(
4421 d_ntsToTerms
.find(ntSymbol
) != d_ntsToTerms
.cend(), ntSymbol
)
4422 << "ntSymbol to be one of the non-terminal symbols given in the "
4424 //////// all checks before this line
4425 d_allowVars
.insert(ntSymbol
);
4427 CVC5_API_TRY_CATCH_END
;
4431 * This function concatenates the outputs of calling f on each element between
4432 * first and last, seperated by sep.
4433 * @param first the beginning of the range
4434 * @param last the end of the range
4435 * @param f the function to call on each element in the range, its output must
4436 * be overloaded for operator<<
4437 * @param sep the string to add between successive calls to f
4439 template <typename Iterator
, typename Function
>
4440 std::string
join(Iterator first
, Iterator last
, Function f
, std::string sep
)
4442 std::stringstream ss
;
4460 std::string
Grammar::toString() const
4462 CVC5_API_TRY_CATCH_BEGIN
;
4463 //////// all checks before this line
4464 std::stringstream ss
;
4465 ss
<< " (" // pre-declaration
4470 std::stringstream s
;
4471 s
<< '(' << t
<< ' ' << t
.getSort() << ')';
4475 << ")\n (" // grouped rule listing
4479 [this](const Term
& t
) {
4480 bool allowConst
= d_allowConst
.find(t
) != d_allowConst
.cend(),
4481 allowVars
= d_allowVars
.find(t
) != d_allowVars
.cend();
4482 const std::vector
<Term
>& rules
= d_ntsToTerms
.at(t
);
4483 std::stringstream s
;
4484 s
<< '(' << t
<< ' ' << t
.getSort() << " ("
4485 << (allowConst
? "(Constant " + t
.getSort().toString() + ")"
4487 << (allowConst
&& allowVars
? " " : "")
4488 << (allowVars
? "(Var " + t
.getSort().toString() + ")" : "")
4489 << ((allowConst
|| allowVars
) && !rules
.empty() ? " " : "")
4493 [](const Term
& rule
) { return rule
.toString(); },
4503 CVC5_API_TRY_CATCH_END
;
4506 Sort
Grammar::resolve()
4508 CVC5_API_TRY_CATCH_BEGIN
;
4509 //////// all checks before this line
4511 d_isResolved
= true;
4515 if (!d_sygusVars
.empty())
4519 d_solver
->getNodeManager()->mkNode(
4520 cvc5::kind::BOUND_VAR_LIST
, Term::termVectorToNodes(d_sygusVars
)));
4523 std::unordered_map
<Term
, Sort
> ntsToUnres(d_ntSyms
.size());
4525 for (Term ntsymbol
: d_ntSyms
)
4527 // make the unresolved type, used for referencing the final version of
4528 // the ntsymbol's datatype
4529 ntsToUnres
[ntsymbol
] =
4530 Sort(d_solver
, d_solver
->getNodeManager()->mkSort(ntsymbol
.toString()));
4533 std::vector
<cvc5::DType
> datatypes
;
4534 std::set
<TypeNode
> unresTypes
;
4536 datatypes
.reserve(d_ntSyms
.size());
4538 for (const Term
& ntSym
: d_ntSyms
)
4540 // make the datatype, which encodes terms generated by this non-terminal
4541 DatatypeDecl
dtDecl(d_solver
, ntSym
.toString());
4543 for (const Term
& consTerm
: d_ntsToTerms
[ntSym
])
4545 addSygusConstructorTerm(dtDecl
, consTerm
, ntsToUnres
);
4548 if (d_allowVars
.find(ntSym
) != d_allowVars
.cend())
4550 addSygusConstructorVariables(dtDecl
,
4551 Sort(d_solver
, ntSym
.d_node
->getType()));
4554 bool aci
= d_allowConst
.find(ntSym
) != d_allowConst
.end();
4555 TypeNode btt
= ntSym
.d_node
->getType();
4556 dtDecl
.d_dtype
->setSygus(btt
, *bvl
.d_node
, aci
, false);
4558 // We can be in a case where the only rule specified was (Variable T)
4559 // and there are no variables of type T, in which case this is a bogus
4560 // grammar. This results in the error below.
4561 CVC5_API_CHECK(dtDecl
.d_dtype
->getNumConstructors() != 0)
4562 << "Grouped rule listing for " << *dtDecl
.d_dtype
4563 << " produced an empty rule list";
4565 datatypes
.push_back(*dtDecl
.d_dtype
);
4566 unresTypes
.insert(*ntsToUnres
[ntSym
].d_type
);
4569 std::vector
<TypeNode
> datatypeTypes
=
4570 d_solver
->getNodeManager()->mkMutualDatatypeTypes(
4571 datatypes
, unresTypes
, NodeManager::DATATYPE_FLAG_PLACEHOLDER
);
4573 // return is the first datatype
4574 return Sort(d_solver
, datatypeTypes
[0]);
4576 CVC5_API_TRY_CATCH_END
;
4579 void Grammar::addSygusConstructorTerm(
4582 const std::unordered_map
<Term
, Sort
>& ntsToUnres
) const
4584 CVC5_API_TRY_CATCH_BEGIN
;
4585 CVC5_API_CHECK_DTDECL(dt
);
4586 CVC5_API_CHECK_TERM(term
);
4587 CVC5_API_CHECK_TERMS_MAP(ntsToUnres
);
4588 //////// all checks before this line
4590 // At this point, we should know that dt is well founded, and that its
4591 // builtin sygus operators are well-typed.
4592 // Now, purify each occurrence of a non-terminal symbol in term, replace by
4593 // free variables. These become arguments to constructors. Notice we must do
4594 // a tree traversal in this function, since unique paths to the same term
4595 // should be treated as distinct terms.
4596 // Notice that let expressions are forbidden in the input syntax of term, so
4597 // this does not lead to exponential behavior with respect to input size.
4598 std::vector
<Term
> args
;
4599 std::vector
<Sort
> cargs
;
4600 Term op
= purifySygusGTerm(term
, args
, cargs
, ntsToUnres
);
4601 std::stringstream ssCName
;
4602 ssCName
<< op
.getKind();
4607 d_solver
->getNodeManager()->mkNode(cvc5::kind::BOUND_VAR_LIST
,
4608 Term::termVectorToNodes(args
)));
4609 // its operator is a lambda
4611 d_solver
->getNodeManager()->mkNode(
4612 cvc5::kind::LAMBDA
, *lbvl
.d_node
, *op
.d_node
));
4614 std::vector
<TypeNode
> cargst
= Sort::sortVectorToTypeNodes(cargs
);
4615 dt
.d_dtype
->addSygusConstructor(*op
.d_node
, ssCName
.str(), cargst
);
4617 CVC5_API_TRY_CATCH_END
;
4620 Term
Grammar::purifySygusGTerm(
4622 std::vector
<Term
>& args
,
4623 std::vector
<Sort
>& cargs
,
4624 const std::unordered_map
<Term
, Sort
>& ntsToUnres
) const
4626 CVC5_API_TRY_CATCH_BEGIN
;
4627 CVC5_API_CHECK_TERM(term
);
4628 CVC5_API_CHECK_TERMS(args
);
4629 CVC5_API_CHECK_SORTS(cargs
);
4630 CVC5_API_CHECK_TERMS_MAP(ntsToUnres
);
4631 //////// all checks before this line
4633 std::unordered_map
<Term
, Sort
>::const_iterator itn
= ntsToUnres
.find(term
);
4634 if (itn
!= ntsToUnres
.cend())
4638 d_solver
->getNodeManager()->mkBoundVar(term
.d_node
->getType()));
4639 args
.push_back(ret
);
4640 cargs
.push_back(itn
->second
);
4643 std::vector
<Term
> pchildren
;
4644 bool childChanged
= false;
4645 for (unsigned i
= 0, nchild
= term
.d_node
->getNumChildren(); i
< nchild
; i
++)
4647 Term ptermc
= purifySygusGTerm(
4648 Term(d_solver
, (*term
.d_node
)[i
]), args
, cargs
, ntsToUnres
);
4649 pchildren
.push_back(ptermc
);
4650 childChanged
= childChanged
|| *ptermc
.d_node
!= (*term
.d_node
)[i
];
4659 if (term
.d_node
->getMetaKind() == kind::metakind::PARAMETERIZED
)
4661 // it's an indexed operator so we should provide the op
4662 NodeBuilder
nb(term
.d_node
->getKind());
4663 nb
<< term
.d_node
->getOperator();
4664 nb
.append(Term::termVectorToNodes(pchildren
));
4665 nret
= nb
.constructNode();
4669 nret
= d_solver
->getNodeManager()->mkNode(
4670 term
.d_node
->getKind(), Term::termVectorToNodes(pchildren
));
4673 return Term(d_solver
, nret
);
4675 CVC5_API_TRY_CATCH_END
;
4678 void Grammar::addSygusConstructorVariables(DatatypeDecl
& dt
,
4679 const Sort
& sort
) const
4681 CVC5_API_TRY_CATCH_BEGIN
;
4682 CVC5_API_CHECK_DTDECL(dt
);
4683 CVC5_API_CHECK_SORT(sort
);
4684 //////// all checks before this line
4686 // each variable of appropriate type becomes a sygus constructor in dt.
4687 for (unsigned i
= 0, size
= d_sygusVars
.size(); i
< size
; i
++)
4689 Term v
= d_sygusVars
[i
];
4690 if (v
.d_node
->getType() == *sort
.d_type
)
4692 std::stringstream ss
;
4694 std::vector
<TypeNode
> cargs
;
4695 dt
.d_dtype
->addSygusConstructor(*v
.d_node
, ss
.str(), cargs
);
4699 CVC5_API_TRY_CATCH_END
;
4702 bool Grammar::containsFreeVariables(const Term
& rule
) const
4704 std::unordered_set
<TNode
> scope
;
4706 for (const Term
& sygusVar
: d_sygusVars
)
4708 scope
.emplace(*sygusVar
.d_node
);
4711 for (const Term
& ntsymbol
: d_ntSyms
)
4713 scope
.emplace(*ntsymbol
.d_node
);
4716 std::unordered_set
<Node
> fvs
;
4717 return expr::getFreeVariablesScope(*rule
.d_node
, fvs
, scope
, false);
4720 std::ostream
& operator<<(std::ostream
& out
, const Grammar
& grammar
)
4722 return out
<< grammar
.toString();
4725 /* -------------------------------------------------------------------------- */
4726 /* Rounding Mode for Floating Points */
4727 /* -------------------------------------------------------------------------- */
4729 const static std::unordered_map
<RoundingMode
, cvc5::RoundingMode
> s_rmodes
{
4730 {ROUND_NEAREST_TIES_TO_EVEN
,
4731 cvc5::RoundingMode::ROUND_NEAREST_TIES_TO_EVEN
},
4732 {ROUND_TOWARD_POSITIVE
, cvc5::RoundingMode::ROUND_TOWARD_POSITIVE
},
4733 {ROUND_TOWARD_NEGATIVE
, cvc5::RoundingMode::ROUND_TOWARD_NEGATIVE
},
4734 {ROUND_TOWARD_ZERO
, cvc5::RoundingMode::ROUND_TOWARD_ZERO
},
4735 {ROUND_NEAREST_TIES_TO_AWAY
,
4736 cvc5::RoundingMode::ROUND_NEAREST_TIES_TO_AWAY
},
4739 const static std::unordered_map
<cvc5::RoundingMode
,
4741 cvc5::RoundingModeHashFunction
>
4743 {cvc5::RoundingMode::ROUND_NEAREST_TIES_TO_EVEN
,
4744 ROUND_NEAREST_TIES_TO_EVEN
},
4745 {cvc5::RoundingMode::ROUND_TOWARD_POSITIVE
, ROUND_TOWARD_POSITIVE
},
4746 {cvc5::RoundingMode::ROUND_TOWARD_POSITIVE
, ROUND_TOWARD_NEGATIVE
},
4747 {cvc5::RoundingMode::ROUND_TOWARD_ZERO
, ROUND_TOWARD_ZERO
},
4748 {cvc5::RoundingMode::ROUND_NEAREST_TIES_TO_AWAY
,
4749 ROUND_NEAREST_TIES_TO_AWAY
},
4752 /* -------------------------------------------------------------------------- */
4754 /* -------------------------------------------------------------------------- */
4756 struct Stat::StatData
4758 cvc5::StatExportData data
;
4759 template <typename T
>
4760 StatData(T
&& t
) : data(std::forward
<T
>(t
))
4763 StatData() : data() {}
4767 Stat::Stat(const Stat
& s
)
4768 : d_expert(s
.d_expert
),
4769 d_default(s
.d_default
),
4770 d_data(std::make_unique
<StatData
>(s
.d_data
->data
))
4773 Stat
& Stat::operator=(const Stat
& s
)
4775 d_expert
= s
.d_expert
;
4776 d_data
= std::make_unique
<StatData
>(s
.d_data
->data
);
4780 bool Stat::isExpert() const { return d_expert
; }
4781 bool Stat::isDefault() const { return d_default
; }
4783 bool Stat::isInt() const
4785 return std::holds_alternative
<int64_t>(d_data
->data
);
4787 int64_t Stat::getInt() const
4789 CVC5_API_TRY_CATCH_BEGIN
;
4790 CVC5_API_RECOVERABLE_CHECK(isInt()) << "Expected Stat of type int64_t.";
4791 return std::get
<int64_t>(d_data
->data
);
4792 CVC5_API_TRY_CATCH_END
;
4794 bool Stat::isDouble() const
4796 return std::holds_alternative
<double>(d_data
->data
);
4798 double Stat::getDouble() const
4800 CVC5_API_TRY_CATCH_BEGIN
;
4801 CVC5_API_RECOVERABLE_CHECK(isDouble()) << "Expected Stat of type double.";
4802 return std::get
<double>(d_data
->data
);
4803 CVC5_API_TRY_CATCH_END
;
4805 bool Stat::isString() const
4807 return std::holds_alternative
<std::string
>(d_data
->data
);
4809 const std::string
& Stat::getString() const
4811 CVC5_API_TRY_CATCH_BEGIN
;
4812 CVC5_API_RECOVERABLE_CHECK(isString())
4813 << "Expected Stat of type std::string.";
4814 return std::get
<std::string
>(d_data
->data
);
4815 CVC5_API_TRY_CATCH_END
;
4817 bool Stat::isHistogram() const
4819 return std::holds_alternative
<HistogramData
>(d_data
->data
);
4821 const Stat::HistogramData
& Stat::getHistogram() const
4823 CVC5_API_TRY_CATCH_BEGIN
;
4824 CVC5_API_RECOVERABLE_CHECK(isHistogram())
4825 << "Expected Stat of type histogram.";
4826 return std::get
<HistogramData
>(d_data
->data
);
4827 CVC5_API_TRY_CATCH_END
;
4830 Stat::Stat(bool expert
, bool defaulted
, StatData
&& sd
)
4832 d_default(defaulted
),
4833 d_data(std::make_unique
<StatData
>(std::move(sd
)))
4837 std::ostream
& operator<<(std::ostream
& os
, const Stat
& sv
)
4839 return cvc5::detail::print(os
, sv
.d_data
->data
);
4842 Statistics::BaseType::const_reference
Statistics::iterator::operator*() const
4844 return d_it
.operator*();
4846 Statistics::BaseType::const_pointer
Statistics::iterator::operator->() const
4848 return d_it
.operator->();
4850 Statistics::iterator
& Statistics::iterator::operator++()
4855 } while (!isVisible());
4858 Statistics::iterator
Statistics::iterator::operator++(int)
4860 iterator tmp
= *this;
4864 } while (!isVisible());
4867 Statistics::iterator
& Statistics::iterator::operator--()
4872 } while (!isVisible());
4875 Statistics::iterator
Statistics::iterator::operator--(int)
4877 iterator tmp
= *this;
4881 } while (!isVisible());
4884 bool Statistics::iterator::operator==(const Statistics::iterator
& rhs
) const
4886 return d_it
== rhs
.d_it
;
4888 bool Statistics::iterator::operator!=(const Statistics::iterator
& rhs
) const
4890 return d_it
!= rhs
.d_it
;
4892 Statistics::iterator::iterator(Statistics::BaseType::const_iterator it
,
4893 const Statistics::BaseType
& base
,
4896 : d_it(it
), d_base(&base
), d_showExpert(expert
), d_showDefault(defaulted
)
4898 while (!isVisible())
4903 bool Statistics::iterator::isVisible() const
4905 if (d_it
== d_base
->end()) return true;
4906 if (!d_showExpert
&& d_it
->second
.isExpert()) return false;
4907 if (!d_showDefault
&& d_it
->second
.isDefault()) return false;
4911 const Stat
& Statistics::get(const std::string
& name
)
4913 CVC5_API_TRY_CATCH_BEGIN
;
4914 auto it
= d_stats
.find(name
);
4915 CVC5_API_RECOVERABLE_CHECK(it
!= d_stats
.end())
4916 << "No stat with name \"" << name
<< "\" exists.";
4918 CVC5_API_TRY_CATCH_END
;
4921 Statistics::iterator
Statistics::begin(bool expert
, bool defaulted
) const
4923 return iterator(d_stats
.begin(), d_stats
, expert
, defaulted
);
4925 Statistics::iterator
Statistics::end() const
4927 return iterator(d_stats
.end(), d_stats
, false, false);
4930 Statistics::Statistics(const StatisticsRegistry
& reg
)
4932 for (const auto& svp
: reg
)
4934 d_stats
.emplace(svp
.first
,
4935 Stat(svp
.second
->d_expert
,
4936 svp
.second
->isDefault(),
4937 svp
.second
->getViewer()));
4941 std::ostream
& operator<<(std::ostream
& out
, const Statistics
& stats
)
4943 for (const auto& stat
: stats
)
4945 out
<< stat
.first
<< " = " << stat
.second
<< std::endl
;
4950 /* -------------------------------------------------------------------------- */
4952 /* -------------------------------------------------------------------------- */
4954 Solver::Solver(std::unique_ptr
<Options
>&& original
)
4956 d_nodeMgr
.reset(new NodeManager());
4957 d_originalOptions
= std::move(original
);
4958 d_smtEngine
.reset(new SmtEngine(d_nodeMgr
.get(), d_originalOptions
.get()));
4959 d_smtEngine
->setSolver(this);
4960 d_rng
.reset(new Random(d_smtEngine
->getOptions().driver
.seed
));
4964 Solver::Solver() : Solver(std::make_unique
<Options
>()) {}
4966 Solver::~Solver() {}
4968 /* Helpers and private functions */
4969 /* -------------------------------------------------------------------------- */
4971 NodeManager
* Solver::getNodeManager(void) const { return d_nodeMgr
.get(); }
4973 void Solver::increment_term_stats(Kind kind
) const
4975 if constexpr (Configuration::isStatisticsBuild())
4977 d_stats
->d_terms
<< kind
;
4981 void Solver::increment_vars_consts_stats(const Sort
& sort
, bool is_var
) const
4983 if constexpr (Configuration::isStatisticsBuild())
4985 const TypeNode tn
= sort
.getTypeNode();
4986 TypeConstant tc
= tn
.getKind() == cvc5::kind::TYPE_CONSTANT
4987 ? tn
.getConst
<TypeConstant
>()
4991 d_stats
->d_vars
<< tc
;
4995 d_stats
->d_consts
<< tc
;
5000 /* Split out to avoid nested API calls (problematic with API tracing). */
5001 /* .......................................................................... */
5003 template <typename T
>
5004 Term
Solver::mkValHelper(T t
) const
5006 //////// all checks before this line
5007 Node res
= getNodeManager()->mkConst(t
);
5008 (void)res
.getType(true); /* kick off type checking */
5009 return Term(this, res
);
5012 Term
Solver::mkRealFromStrHelper(const std::string
& s
) const
5014 //////// all checks before this line
5017 cvc5::Rational r
= s
.find('/') != std::string::npos
5019 : cvc5::Rational::fromDecimal(s
);
5020 return mkValHelper
<cvc5::Rational
>(r
);
5022 catch (const std::invalid_argument
& e
)
5024 /* Catch to throw with a more meaningful error message. To be caught in
5025 * enclosing CVC5_API_TRY_CATCH_* block to throw CVC5ApiException. */
5026 std::stringstream message
;
5027 message
<< "Cannot construct Real or Int from string argument '" << s
<< "'"
5029 throw std::invalid_argument(message
.str());
5033 Term
Solver::mkBVFromIntHelper(uint32_t size
, uint64_t val
) const
5035 CVC5_API_ARG_CHECK_EXPECTED(size
> 0, size
) << "a bit-width > 0";
5036 //////// all checks before this line
5037 return mkValHelper
<cvc5::BitVector
>(cvc5::BitVector(size
, val
));
5040 Term
Solver::mkBVFromStrHelper(uint32_t size
,
5041 const std::string
& s
,
5042 uint32_t base
) const
5044 CVC5_API_ARG_CHECK_EXPECTED(!s
.empty(), s
) << "a non-empty string";
5045 CVC5_API_ARG_CHECK_EXPECTED(base
== 2 || base
== 10 || base
== 16, base
)
5046 << "base 2, 10, or 16";
5047 //////// all checks before this line
5049 Integer
val(s
, base
);
5051 if (val
.strictlyNegative())
5053 CVC5_API_CHECK(val
>= -Integer("2", 10).pow(size
- 1))
5054 << "Overflow in bitvector construction (specified bitvector size "
5055 << size
<< " too small to hold value " << s
<< ")";
5059 CVC5_API_CHECK(val
.modByPow2(size
) == val
)
5060 << "Overflow in bitvector construction (specified bitvector size "
5061 << size
<< " too small to hold value " << s
<< ")";
5063 return mkValHelper
<cvc5::BitVector
>(cvc5::BitVector(size
, val
));
5066 Term
Solver::getValueHelper(const Term
& term
) const
5068 // Note: Term is checked in the caller to avoid double checks
5069 //////// all checks before this line
5070 Node value
= d_smtEngine
->getValue(*term
.d_node
);
5071 Term res
= Term(this, value
);
5072 // May need to wrap in real cast so that user know this is a real.
5073 TypeNode tn
= (*term
.d_node
).getType();
5074 if (!tn
.isInteger() && value
.getType().isInteger())
5076 return ensureRealSort(res
);
5081 Sort
Solver::mkTupleSortHelper(const std::vector
<Sort
>& sorts
) const
5083 // Note: Sorts are checked in the caller to avoid double checks
5084 //////// all checks before this line
5085 std::vector
<TypeNode
> typeNodes
= Sort::sortVectorToTypeNodes(sorts
);
5086 return Sort(this, getNodeManager()->mkTupleType(typeNodes
));
5089 Term
Solver::mkTermFromKind(Kind kind
) const
5091 CVC5_API_KIND_CHECK_EXPECTED(
5092 kind
== PI
|| kind
== REGEXP_EMPTY
|| kind
== REGEXP_SIGMA
, kind
)
5093 << "PI or REGEXP_EMPTY or REGEXP_SIGMA";
5094 //////// all checks before this line
5096 if (kind
== REGEXP_EMPTY
|| kind
== REGEXP_SIGMA
)
5098 cvc5::Kind k
= extToIntKind(kind
);
5099 Assert(isDefinedIntKind(k
));
5100 res
= d_nodeMgr
->mkNode(k
, std::vector
<Node
>());
5105 res
= d_nodeMgr
->mkNullaryOperator(d_nodeMgr
->realType(), cvc5::kind::PI
);
5107 (void)res
.getType(true); /* kick off type checking */
5108 increment_term_stats(kind
);
5109 return Term(this, res
);
5112 Term
Solver::mkTermHelper(Kind kind
, const std::vector
<Term
>& children
) const
5114 // Note: Kind and children are checked in the caller to avoid double checks
5115 //////// all checks before this line
5117 std::vector
<Node
> echildren
= Term::termVectorToNodes(children
);
5118 cvc5::Kind k
= extToIntKind(kind
);
5120 if (echildren
.size() > 2)
5122 if (kind
== INTS_DIVISION
|| kind
== XOR
|| kind
== MINUS
5123 || kind
== DIVISION
|| kind
== HO_APPLY
|| kind
== REGEXP_DIFF
)
5125 // left-associative, but cvc5 internally only supports 2 args
5126 res
= d_nodeMgr
->mkLeftAssociative(k
, echildren
);
5128 else if (kind
== IMPLIES
)
5130 // right-associative, but cvc5 internally only supports 2 args
5131 res
= d_nodeMgr
->mkRightAssociative(k
, echildren
);
5133 else if (kind
== EQUAL
|| kind
== LT
|| kind
== GT
|| kind
== LEQ
5136 // "chainable", but cvc5 internally only supports 2 args
5137 res
= d_nodeMgr
->mkChain(k
, echildren
);
5139 else if (kind::isAssociative(k
))
5141 // mkAssociative has special treatment for associative operators with lots
5143 res
= d_nodeMgr
->mkAssociative(k
, echildren
);
5147 // default case, must check kind
5148 checkMkTerm(kind
, children
.size());
5149 res
= d_nodeMgr
->mkNode(k
, echildren
);
5152 else if (kind::isAssociative(k
))
5154 // associative case, same as above
5155 res
= d_nodeMgr
->mkAssociative(k
, echildren
);
5159 // default case, same as above
5160 checkMkTerm(kind
, children
.size());
5161 if (kind
== api::SINGLETON
)
5163 // the type of the term is the same as the type of the internal node
5164 // see Term::getSort()
5165 TypeNode type
= children
[0].d_node
->getType();
5166 // Internally NodeManager::mkSingleton needs a type argument
5167 // to construct a singleton, since there is no difference between
5168 // integers and reals (both are Rationals).
5169 // At the API, mkReal and mkInteger are different and therefore the
5170 // element type can be used safely here.
5171 res
= getNodeManager()->mkSingleton(type
, *children
[0].d_node
);
5173 else if (kind
== api::MK_BAG
)
5175 // the type of the term is the same as the type of the internal node
5176 // see Term::getSort()
5177 TypeNode type
= children
[0].d_node
->getType();
5178 // Internally NodeManager::mkBag needs a type argument
5179 // to construct a bag, since there is no difference between
5180 // integers and reals (both are Rationals).
5181 // At the API, mkReal and mkInteger are different and therefore the
5182 // element type can be used safely here.
5183 res
= getNodeManager()->mkBag(
5184 type
, *children
[0].d_node
, *children
[1].d_node
);
5188 res
= d_nodeMgr
->mkNode(k
, echildren
);
5192 (void)res
.getType(true); /* kick off type checking */
5193 increment_term_stats(kind
);
5194 return Term(this, res
);
5197 Term
Solver::mkTermHelper(const Op
& op
, const std::vector
<Term
>& children
) const
5199 // Note: Op and children are checked in the caller to avoid double checks
5200 checkMkTerm(op
.d_kind
, children
.size());
5201 //////// all checks before this line
5203 if (!op
.isIndexedHelper())
5205 return mkTermHelper(op
.d_kind
, children
);
5208 const cvc5::Kind int_kind
= extToIntKind(op
.d_kind
);
5209 std::vector
<Node
> echildren
= Term::termVectorToNodes(children
);
5211 NodeBuilder
nb(int_kind
);
5213 nb
.append(echildren
);
5214 Node res
= nb
.constructNode();
5216 (void)res
.getType(true); /* kick off type checking */
5217 return Term(this, res
);
5220 std::vector
<Sort
> Solver::mkDatatypeSortsInternal(
5221 const std::vector
<DatatypeDecl
>& dtypedecls
,
5222 const std::set
<Sort
>& unresolvedSorts
) const
5224 // Note: dtypedecls and unresolvedSorts are checked in the caller to avoid
5226 //////// all checks before this line
5228 std::vector
<cvc5::DType
> datatypes
;
5229 for (size_t i
= 0, ndts
= dtypedecls
.size(); i
< ndts
; ++i
)
5231 datatypes
.push_back(dtypedecls
[i
].getDatatype());
5234 std::set
<TypeNode
> utypes
= Sort::sortSetToTypeNodes(unresolvedSorts
);
5235 std::vector
<cvc5::TypeNode
> dtypes
=
5236 getNodeManager()->mkMutualDatatypeTypes(datatypes
, utypes
);
5237 std::vector
<Sort
> retTypes
= Sort::typeNodeVectorToSorts(this, dtypes
);
5241 Term
Solver::synthFunHelper(const std::string
& symbol
,
5242 const std::vector
<Term
>& boundVars
,
5245 Grammar
* grammar
) const
5247 // Note: boundVars, sort and grammar are checked in the caller to avoid
5249 std::vector
<TypeNode
> varTypes
;
5250 for (const auto& bv
: boundVars
)
5254 CVC5_API_CHECK(grammar
->d_ntSyms
[0].d_node
->getType() == *sort
.d_type
)
5255 << "Invalid Start symbol for grammar, Expected Start's sort to be "
5256 << *sort
.d_type
<< " but found "
5257 << grammar
->d_ntSyms
[0].d_node
->getType();
5259 varTypes
.push_back(bv
.d_node
->getType());
5261 //////// all checks before this line
5263 TypeNode funType
= varTypes
.empty() ? *sort
.d_type
5264 : getNodeManager()->mkFunctionType(
5265 varTypes
, *sort
.d_type
);
5267 Node fun
= getNodeManager()->mkBoundVar(symbol
, funType
);
5268 (void)fun
.getType(true); /* kick off type checking */
5270 std::vector
<Node
> bvns
= Term::termVectorToNodes(boundVars
);
5272 d_smtEngine
->declareSynthFun(
5274 grammar
== nullptr ? funType
: *grammar
->resolve().d_type
,
5278 return Term(this, fun
);
5281 Term
Solver::ensureTermSort(const Term
& term
, const Sort
& sort
) const
5283 // Note: Term and sort are checked in the caller to avoid double checks
5284 CVC5_API_CHECK(term
.getSort() == sort
5285 || (term
.getSort().isInteger() && sort
.isReal()))
5286 << "Expected conversion from Int to Real";
5287 //////// all checks before this line
5289 Sort t
= term
.getSort();
5290 if (term
.getSort() == sort
)
5295 // Integers are reals, too
5296 Assert(t
.d_type
->isReal());
5300 // Must cast to Real to ensure correct type is passed to parametric type
5301 // constructors. We do this cast using division with 1. This has the
5302 // advantage wrt using TO_REAL since (constant) division is always included
5305 d_nodeMgr
->mkNode(extToIntKind(DIVISION
),
5307 d_nodeMgr
->mkConst(cvc5::Rational(1))));
5309 Assert(res
.getSort() == sort
);
5313 Term
Solver::ensureRealSort(const Term
& t
) const
5315 Assert(this == t
.d_solver
);
5316 CVC5_API_ARG_CHECK_EXPECTED(
5317 t
.getSort() == getIntegerSort() || t
.getSort() == getRealSort(),
5318 " an integer or real term");
5319 // Note: Term is checked in the caller to avoid double checks
5320 //////// all checks before this line
5321 if (t
.getSort() == getIntegerSort())
5323 Node n
= getNodeManager()->mkNode(kind::CAST_TO_REAL
, *t
.d_node
);
5324 return Term(this, n
);
5329 bool Solver::isValidInteger(const std::string
& s
) const
5331 //////// all checks before this line
5332 if (s
.length() == 0)
5334 // string should not be empty
5339 if (s
[index
] == '-')
5341 if (s
.length() == 1)
5343 // negative integers should contain at least one digit
5349 if (s
[index
] == '0' && s
.length() > (index
+ 1))
5351 // From SMT-Lib 2.6: A <numeral> is the digit 0 or a non-empty sequence of
5352 // digits not starting with 0. So integers like 001, 000 are not allowed
5356 // all remaining characters should be decimal digits
5357 for (; index
< s
.length(); ++index
)
5359 if (!std::isdigit(s
[index
]))
5368 void Solver::resetStatistics()
5370 if constexpr (Configuration::isStatisticsBuild())
5372 d_stats
.reset(new APIStatistics
{
5373 d_smtEngine
->getStatisticsRegistry().registerHistogram
<TypeConstant
>(
5375 d_smtEngine
->getStatisticsRegistry().registerHistogram
<TypeConstant
>(
5377 d_smtEngine
->getStatisticsRegistry().registerHistogram
<Kind
>(
5383 void Solver::printStatisticsSafe(int fd
) const
5385 d_smtEngine
->printStatisticsSafe(fd
);
5388 /* Helpers for mkTerm checks. */
5389 /* .......................................................................... */
5391 void Solver::checkMkTerm(Kind kind
, uint32_t nchildren
) const
5393 CVC5_API_KIND_CHECK(kind
);
5394 Assert(isDefinedIntKind(extToIntKind(kind
)));
5395 const cvc5::kind::MetaKind mk
= kind::metaKindOf(extToIntKind(kind
));
5396 CVC5_API_KIND_CHECK_EXPECTED(
5397 mk
== kind::metakind::PARAMETERIZED
|| mk
== kind::metakind::OPERATOR
,
5399 << "Only operator-style terms are created with mkTerm(), "
5400 "to create variables, constants and values see mkVar(), mkConst() "
5401 "and the respective theory-specific functions to create values, "
5402 "e.g., mkBitVector().";
5403 CVC5_API_KIND_CHECK_EXPECTED(
5404 nchildren
>= minArity(kind
) && nchildren
<= maxArity(kind
), kind
)
5405 << "Terms with kind " << kindToString(kind
) << " must have at least "
5406 << minArity(kind
) << " children and at most " << maxArity(kind
)
5407 << " children (the one under construction has " << nchildren
<< ")";
5410 /* Sorts Handling */
5411 /* -------------------------------------------------------------------------- */
5413 Sort
Solver::getNullSort(void) const
5415 NodeManagerScope
scope(getNodeManager());
5416 CVC5_API_TRY_CATCH_BEGIN
;
5417 //////// all checks before this line
5418 return Sort(this, TypeNode());
5420 CVC5_API_TRY_CATCH_END
;
5423 Sort
Solver::getBooleanSort(void) const
5425 NodeManagerScope
scope(getNodeManager());
5426 CVC5_API_TRY_CATCH_BEGIN
;
5427 //////// all checks before this line
5428 return Sort(this, getNodeManager()->booleanType());
5430 CVC5_API_TRY_CATCH_END
;
5433 Sort
Solver::getIntegerSort(void) const
5435 NodeManagerScope
scope(getNodeManager());
5436 CVC5_API_TRY_CATCH_BEGIN
;
5437 //////// all checks before this line
5438 return Sort(this, getNodeManager()->integerType());
5440 CVC5_API_TRY_CATCH_END
;
5443 Sort
Solver::getRealSort(void) const
5445 NodeManagerScope
scope(getNodeManager());
5446 CVC5_API_TRY_CATCH_BEGIN
;
5447 //////// all checks before this line
5448 return Sort(this, getNodeManager()->realType());
5450 CVC5_API_TRY_CATCH_END
;
5453 Sort
Solver::getRegExpSort(void) const
5455 NodeManagerScope
scope(getNodeManager());
5456 CVC5_API_TRY_CATCH_BEGIN
;
5457 //////// all checks before this line
5458 return Sort(this, getNodeManager()->regExpType());
5460 CVC5_API_TRY_CATCH_END
;
5463 Sort
Solver::getStringSort(void) const
5465 NodeManagerScope
scope(getNodeManager());
5466 CVC5_API_TRY_CATCH_BEGIN
;
5467 //////// all checks before this line
5468 return Sort(this, getNodeManager()->stringType());
5470 CVC5_API_TRY_CATCH_END
;
5473 Sort
Solver::getRoundingModeSort(void) const
5475 NodeManagerScope
scope(getNodeManager());
5476 CVC5_API_TRY_CATCH_BEGIN
;
5477 //////// all checks before this line
5478 return Sort(this, getNodeManager()->roundingModeType());
5480 CVC5_API_TRY_CATCH_END
;
5483 /* Create sorts ------------------------------------------------------- */
5485 Sort
Solver::mkArraySort(const Sort
& indexSort
, const Sort
& elemSort
) const
5487 NodeManagerScope
scope(getNodeManager());
5488 CVC5_API_TRY_CATCH_BEGIN
;
5489 CVC5_API_SOLVER_CHECK_SORT(indexSort
);
5490 CVC5_API_SOLVER_CHECK_SORT(elemSort
);
5491 //////// all checks before this line
5493 this, getNodeManager()->mkArrayType(*indexSort
.d_type
, *elemSort
.d_type
));
5495 CVC5_API_TRY_CATCH_END
;
5498 Sort
Solver::mkBitVectorSort(uint32_t size
) const
5500 NodeManagerScope
scope(getNodeManager());
5501 CVC5_API_TRY_CATCH_BEGIN
;
5502 CVC5_API_ARG_CHECK_EXPECTED(size
> 0, size
) << "size > 0";
5503 //////// all checks before this line
5504 return Sort(this, getNodeManager()->mkBitVectorType(size
));
5506 CVC5_API_TRY_CATCH_END
;
5509 Sort
Solver::mkFloatingPointSort(uint32_t exp
, uint32_t sig
) const
5511 NodeManagerScope
scope(getNodeManager());
5512 CVC5_API_TRY_CATCH_BEGIN
;
5513 CVC5_API_ARG_CHECK_EXPECTED(exp
> 0, exp
) << "exponent size > 0";
5514 CVC5_API_ARG_CHECK_EXPECTED(sig
> 0, sig
) << "significand size > 0";
5515 //////// all checks before this line
5516 return Sort(this, getNodeManager()->mkFloatingPointType(exp
, sig
));
5518 CVC5_API_TRY_CATCH_END
;
5521 Sort
Solver::mkDatatypeSort(const DatatypeDecl
& dtypedecl
) const
5523 NodeManagerScope
scope(getNodeManager());
5524 CVC5_API_TRY_CATCH_BEGIN
;
5525 CVC5_API_SOLVER_CHECK_DTDECL(dtypedecl
);
5526 //////// all checks before this line
5527 return Sort(this, getNodeManager()->mkDatatypeType(*dtypedecl
.d_dtype
));
5529 CVC5_API_TRY_CATCH_END
;
5532 std::vector
<Sort
> Solver::mkDatatypeSorts(
5533 const std::vector
<DatatypeDecl
>& dtypedecls
) const
5535 NodeManagerScope
scope(getNodeManager());
5536 CVC5_API_SOLVER_CHECK_DTDECLS(dtypedecls
);
5537 CVC5_API_TRY_CATCH_BEGIN
;
5538 //////// all checks before this line
5539 return mkDatatypeSortsInternal(dtypedecls
, {});
5541 CVC5_API_TRY_CATCH_END
;
5544 std::vector
<Sort
> Solver::mkDatatypeSorts(
5545 const std::vector
<DatatypeDecl
>& dtypedecls
,
5546 const std::set
<Sort
>& unresolvedSorts
) const
5548 NodeManagerScope
scope(getNodeManager());
5549 CVC5_API_TRY_CATCH_BEGIN
;
5550 CVC5_API_SOLVER_CHECK_DTDECLS(dtypedecls
);
5551 CVC5_API_SOLVER_CHECK_SORTS(unresolvedSorts
);
5552 //////// all checks before this line
5553 return mkDatatypeSortsInternal(dtypedecls
, unresolvedSorts
);
5555 CVC5_API_TRY_CATCH_END
;
5558 Sort
Solver::mkFunctionSort(const Sort
& domain
, const Sort
& codomain
) const
5560 NodeManagerScope
scope(getNodeManager());
5561 CVC5_API_TRY_CATCH_BEGIN
;
5562 CVC5_API_SOLVER_CHECK_DOMAIN_SORT(domain
);
5563 CVC5_API_SOLVER_CHECK_CODOMAIN_SORT(codomain
);
5564 //////// all checks before this line
5566 this, getNodeManager()->mkFunctionType(*domain
.d_type
, *codomain
.d_type
));
5568 CVC5_API_TRY_CATCH_END
;
5571 Sort
Solver::mkFunctionSort(const std::vector
<Sort
>& sorts
,
5572 const Sort
& codomain
) const
5574 NodeManagerScope
scope(getNodeManager());
5575 CVC5_API_TRY_CATCH_BEGIN
;
5576 CVC5_API_ARG_SIZE_CHECK_EXPECTED(sorts
.size() >= 1, sorts
)
5577 << "at least one parameter sort for function sort";
5578 CVC5_API_SOLVER_CHECK_DOMAIN_SORTS(sorts
);
5579 CVC5_API_SOLVER_CHECK_CODOMAIN_SORT(codomain
);
5580 //////// all checks before this line
5581 std::vector
<TypeNode
> argTypes
= Sort::sortVectorToTypeNodes(sorts
);
5583 getNodeManager()->mkFunctionType(argTypes
, *codomain
.d_type
));
5585 CVC5_API_TRY_CATCH_END
;
5588 Sort
Solver::mkParamSort(const std::string
& symbol
) const
5590 NodeManagerScope
scope(getNodeManager());
5591 CVC5_API_TRY_CATCH_BEGIN
;
5592 //////// all checks before this line
5595 getNodeManager()->mkSort(symbol
, NodeManager::SORT_FLAG_PLACEHOLDER
));
5597 CVC5_API_TRY_CATCH_END
;
5600 Sort
Solver::mkPredicateSort(const std::vector
<Sort
>& sorts
) const
5602 NodeManagerScope
scope(getNodeManager());
5603 CVC5_API_TRY_CATCH_BEGIN
;
5604 CVC5_API_ARG_SIZE_CHECK_EXPECTED(sorts
.size() >= 1, sorts
)
5605 << "at least one parameter sort for predicate sort";
5606 CVC5_API_SOLVER_CHECK_DOMAIN_SORTS(sorts
);
5607 //////// all checks before this line
5610 getNodeManager()->mkPredicateType(Sort::sortVectorToTypeNodes(sorts
)));
5612 CVC5_API_TRY_CATCH_END
;
5615 Sort
Solver::mkRecordSort(
5616 const std::vector
<std::pair
<std::string
, Sort
>>& fields
) const
5618 NodeManagerScope
scope(getNodeManager());
5619 CVC5_API_TRY_CATCH_BEGIN
;
5620 std::vector
<std::pair
<std::string
, TypeNode
>> f
;
5621 for (size_t i
= 0, size
= fields
.size(); i
< size
; ++i
)
5623 const auto& p
= fields
[i
];
5624 CVC5_API_ARG_AT_INDEX_CHECK_EXPECTED(!p
.second
.isNull(), "sort", fields
, i
)
5626 CVC5_API_ARG_AT_INDEX_CHECK_EXPECTED(
5627 this == p
.second
.d_solver
, "sort", fields
, i
)
5628 << "sort associated with this solver object";
5629 f
.emplace_back(p
.first
, *p
.second
.d_type
);
5631 //////// all checks before this line
5632 return Sort(this, getNodeManager()->mkRecordType(f
));
5634 CVC5_API_TRY_CATCH_END
;
5637 Sort
Solver::mkSetSort(const Sort
& elemSort
) const
5639 NodeManagerScope
scope(getNodeManager());
5640 CVC5_API_TRY_CATCH_BEGIN
;
5641 CVC5_API_SOLVER_CHECK_SORT(elemSort
);
5642 //////// all checks before this line
5643 return Sort(this, getNodeManager()->mkSetType(*elemSort
.d_type
));
5645 CVC5_API_TRY_CATCH_END
;
5648 Sort
Solver::mkBagSort(const Sort
& elemSort
) const
5650 NodeManagerScope
scope(getNodeManager());
5651 CVC5_API_TRY_CATCH_BEGIN
;
5652 CVC5_API_SOLVER_CHECK_SORT(elemSort
);
5653 //////// all checks before this line
5654 return Sort(this, getNodeManager()->mkBagType(*elemSort
.d_type
));
5656 CVC5_API_TRY_CATCH_END
;
5659 Sort
Solver::mkSequenceSort(const Sort
& elemSort
) const
5661 NodeManagerScope
scope(getNodeManager());
5662 CVC5_API_TRY_CATCH_BEGIN
;
5663 CVC5_API_SOLVER_CHECK_SORT(elemSort
);
5664 //////// all checks before this line
5665 return Sort(this, getNodeManager()->mkSequenceType(*elemSort
.d_type
));
5667 CVC5_API_TRY_CATCH_END
;
5670 Sort
Solver::mkUninterpretedSort(const std::string
& symbol
) const
5672 NodeManagerScope
scope(getNodeManager());
5673 CVC5_API_TRY_CATCH_BEGIN
;
5674 //////// all checks before this line
5675 return Sort(this, getNodeManager()->mkSort(symbol
));
5677 CVC5_API_TRY_CATCH_END
;
5680 Sort
Solver::mkSortConstructorSort(const std::string
& symbol
,
5683 NodeManagerScope
scope(getNodeManager());
5684 CVC5_API_TRY_CATCH_BEGIN
;
5685 CVC5_API_ARG_CHECK_EXPECTED(arity
> 0, arity
) << "an arity > 0";
5686 //////// all checks before this line
5687 return Sort(this, getNodeManager()->mkSortConstructor(symbol
, arity
));
5689 CVC5_API_TRY_CATCH_END
;
5692 Sort
Solver::mkTupleSort(const std::vector
<Sort
>& sorts
) const
5694 NodeManagerScope
scope(getNodeManager());
5695 CVC5_API_TRY_CATCH_BEGIN
;
5696 CVC5_API_SOLVER_CHECK_SORTS_NOT_FUNCTION_LIKE(sorts
);
5697 //////// all checks before this line
5698 return mkTupleSortHelper(sorts
);
5700 CVC5_API_TRY_CATCH_END
;
5704 /* -------------------------------------------------------------------------- */
5706 Term
Solver::mkTrue(void) const
5708 NodeManagerScope
scope(getNodeManager());
5709 CVC5_API_TRY_CATCH_BEGIN
;
5710 //////// all checks before this line
5711 return Term(this, d_nodeMgr
->mkConst
<bool>(true));
5713 CVC5_API_TRY_CATCH_END
;
5716 Term
Solver::mkFalse(void) const
5718 NodeManagerScope
scope(getNodeManager());
5719 CVC5_API_TRY_CATCH_BEGIN
;
5720 //////// all checks before this line
5721 return Term(this, d_nodeMgr
->mkConst
<bool>(false));
5723 CVC5_API_TRY_CATCH_END
;
5726 Term
Solver::mkBoolean(bool val
) const
5728 NodeManagerScope
scope(getNodeManager());
5729 CVC5_API_TRY_CATCH_BEGIN
;
5730 //////// all checks before this line
5731 return Term(this, d_nodeMgr
->mkConst
<bool>(val
));
5733 CVC5_API_TRY_CATCH_END
;
5736 Term
Solver::mkPi() const
5738 NodeManagerScope
scope(getNodeManager());
5739 CVC5_API_TRY_CATCH_BEGIN
;
5740 //////// all checks before this line
5742 d_nodeMgr
->mkNullaryOperator(d_nodeMgr
->realType(), cvc5::kind::PI
);
5743 (void)res
.getType(true); /* kick off type checking */
5744 return Term(this, res
);
5746 CVC5_API_TRY_CATCH_END
;
5749 Term
Solver::mkInteger(const std::string
& s
) const
5751 NodeManagerScope
scope(getNodeManager());
5752 CVC5_API_TRY_CATCH_BEGIN
;
5753 CVC5_API_ARG_CHECK_EXPECTED(isValidInteger(s
), s
) << " an integer ";
5754 Term integer
= mkRealFromStrHelper(s
);
5755 CVC5_API_ARG_CHECK_EXPECTED(integer
.getSort() == getIntegerSort(), s
)
5756 << " a string representing an integer";
5757 //////// all checks before this line
5760 CVC5_API_TRY_CATCH_END
;
5763 Term
Solver::mkInteger(int64_t val
) const
5765 NodeManagerScope
scope(getNodeManager());
5766 CVC5_API_TRY_CATCH_BEGIN
;
5767 //////// all checks before this line
5768 Term integer
= mkValHelper
<cvc5::Rational
>(cvc5::Rational(val
));
5769 Assert(integer
.getSort() == getIntegerSort());
5772 CVC5_API_TRY_CATCH_END
;
5775 Term
Solver::mkReal(const std::string
& s
) const
5777 NodeManagerScope
scope(getNodeManager());
5778 CVC5_API_TRY_CATCH_BEGIN
;
5779 /* CLN and GMP handle this case differently, CLN interprets it as 0, GMP
5780 * throws an std::invalid_argument exception. For consistency, we treat it
5782 CVC5_API_ARG_CHECK_EXPECTED(s
!= ".", s
)
5783 << "a string representing a real or rational value.";
5784 //////// all checks before this line
5785 Term rational
= mkRealFromStrHelper(s
);
5786 return ensureRealSort(rational
);
5788 CVC5_API_TRY_CATCH_END
;
5791 Term
Solver::mkReal(int64_t val
) const
5793 NodeManagerScope
scope(getNodeManager());
5794 CVC5_API_TRY_CATCH_BEGIN
;
5795 //////// all checks before this line
5796 Term rational
= mkValHelper
<cvc5::Rational
>(cvc5::Rational(val
));
5797 return ensureRealSort(rational
);
5799 CVC5_API_TRY_CATCH_END
;
5802 Term
Solver::mkReal(int64_t num
, int64_t den
) const
5804 NodeManagerScope
scope(getNodeManager());
5805 CVC5_API_TRY_CATCH_BEGIN
;
5806 //////// all checks before this line
5807 Term rational
= mkValHelper
<cvc5::Rational
>(cvc5::Rational(num
, den
));
5808 return ensureRealSort(rational
);
5810 CVC5_API_TRY_CATCH_END
;
5813 Term
Solver::mkRegexpEmpty() const
5815 NodeManagerScope
scope(getNodeManager());
5816 CVC5_API_TRY_CATCH_BEGIN
;
5817 //////// all checks before this line
5819 d_nodeMgr
->mkNode(cvc5::kind::REGEXP_EMPTY
, std::vector
<cvc5::Node
>());
5820 (void)res
.getType(true); /* kick off type checking */
5821 return Term(this, res
);
5823 CVC5_API_TRY_CATCH_END
;
5826 Term
Solver::mkRegexpSigma() const
5828 NodeManagerScope
scope(getNodeManager());
5829 CVC5_API_TRY_CATCH_BEGIN
;
5830 //////// all checks before this line
5832 d_nodeMgr
->mkNode(cvc5::kind::REGEXP_SIGMA
, std::vector
<cvc5::Node
>());
5833 (void)res
.getType(true); /* kick off type checking */
5834 return Term(this, res
);
5836 CVC5_API_TRY_CATCH_END
;
5839 Term
Solver::mkEmptySet(const Sort
& sort
) const
5841 NodeManagerScope
scope(getNodeManager());
5842 CVC5_API_TRY_CATCH_BEGIN
;
5843 CVC5_API_ARG_CHECK_EXPECTED(sort
.isNull() || sort
.isSet(), sort
)
5844 << "null sort or set sort";
5845 CVC5_API_ARG_CHECK_EXPECTED(sort
.isNull() || this == sort
.d_solver
, sort
)
5846 << "set sort associated with this solver object";
5847 //////// all checks before this line
5848 return mkValHelper
<cvc5::EmptySet
>(cvc5::EmptySet(*sort
.d_type
));
5850 CVC5_API_TRY_CATCH_END
;
5853 Term
Solver::mkEmptyBag(const Sort
& sort
) const
5855 NodeManagerScope
scope(getNodeManager());
5856 CVC5_API_TRY_CATCH_BEGIN
;
5857 CVC5_API_ARG_CHECK_EXPECTED(sort
.isNull() || sort
.isBag(), sort
)
5858 << "null sort or bag sort";
5859 CVC5_API_ARG_CHECK_EXPECTED(sort
.isNull() || this == sort
.d_solver
, sort
)
5860 << "bag sort associated with this solver object";
5861 //////// all checks before this line
5862 return mkValHelper
<cvc5::EmptyBag
>(cvc5::EmptyBag(*sort
.d_type
));
5864 CVC5_API_TRY_CATCH_END
;
5867 Term
Solver::mkSepNil(const Sort
& sort
) const
5869 NodeManagerScope
scope(getNodeManager());
5870 CVC5_API_TRY_CATCH_BEGIN
;
5871 CVC5_API_SOLVER_CHECK_SORT(sort
);
5872 //////// all checks before this line
5874 getNodeManager()->mkNullaryOperator(*sort
.d_type
, cvc5::kind::SEP_NIL
);
5875 (void)res
.getType(true); /* kick off type checking */
5876 return Term(this, res
);
5878 CVC5_API_TRY_CATCH_END
;
5881 Term
Solver::mkString(const std::string
& s
, bool useEscSequences
) const
5883 NodeManagerScope
scope(getNodeManager());
5884 CVC5_API_TRY_CATCH_BEGIN
;
5885 //////// all checks before this line
5886 return mkValHelper
<cvc5::String
>(cvc5::String(s
, useEscSequences
));
5888 CVC5_API_TRY_CATCH_END
;
5891 Term
Solver::mkString(const std::wstring
& s
) const
5893 NodeManagerScope
scope(getNodeManager());
5894 CVC5_API_TRY_CATCH_BEGIN
;
5895 //////// all checks before this line
5896 return mkValHelper
<cvc5::String
>(cvc5::String(s
));
5898 CVC5_API_TRY_CATCH_END
;
5901 Term
Solver::mkEmptySequence(const Sort
& sort
) const
5903 NodeManagerScope
scope(getNodeManager());
5904 CVC5_API_TRY_CATCH_BEGIN
;
5905 CVC5_API_SOLVER_CHECK_SORT(sort
);
5906 //////// all checks before this line
5907 std::vector
<Node
> seq
;
5908 Node res
= d_nodeMgr
->mkConst(Sequence(*sort
.d_type
, seq
));
5909 return Term(this, res
);
5911 CVC5_API_TRY_CATCH_END
;
5914 Term
Solver::mkUniverseSet(const Sort
& sort
) const
5916 NodeManagerScope
scope(getNodeManager());
5917 CVC5_API_TRY_CATCH_BEGIN
;
5918 CVC5_API_SOLVER_CHECK_SORT(sort
);
5919 //////// all checks before this line
5921 Node res
= getNodeManager()->mkNullaryOperator(*sort
.d_type
,
5922 cvc5::kind::UNIVERSE_SET
);
5923 // TODO(#2771): Reenable?
5924 // (void)res->getType(true); /* kick off type checking */
5925 return Term(this, res
);
5927 CVC5_API_TRY_CATCH_END
;
5930 Term
Solver::mkBitVector(uint32_t size
, uint64_t val
) const
5932 NodeManagerScope
scope(getNodeManager());
5933 CVC5_API_TRY_CATCH_BEGIN
;
5934 //////// all checks before this line
5935 return mkBVFromIntHelper(size
, val
);
5937 CVC5_API_TRY_CATCH_END
;
5940 Term
Solver::mkBitVector(uint32_t size
,
5941 const std::string
& s
,
5942 uint32_t base
) const
5944 NodeManagerScope
scope(getNodeManager());
5945 CVC5_API_TRY_CATCH_BEGIN
;
5946 //////// all checks before this line
5947 return mkBVFromStrHelper(size
, s
, base
);
5949 CVC5_API_TRY_CATCH_END
;
5952 Term
Solver::mkConstArray(const Sort
& sort
, const Term
& val
) const
5954 NodeManagerScope
scope(getNodeManager());
5955 CVC5_API_TRY_CATCH_BEGIN
;
5956 CVC5_API_SOLVER_CHECK_SORT(sort
);
5957 CVC5_API_SOLVER_CHECK_TERM(val
);
5958 CVC5_API_ARG_CHECK_EXPECTED(sort
.isArray(), sort
) << "an array sort";
5959 CVC5_API_CHECK(val
.getSort().isSubsortOf(sort
.getArrayElementSort()))
5960 << "Value does not match element sort";
5961 //////// all checks before this line
5963 // handle the special case of (CAST_TO_REAL n) where n is an integer
5964 Node n
= *val
.d_node
;
5965 if (val
.isCastedReal())
5967 // this is safe because the constant array stores its type
5971 mkValHelper
<cvc5::ArrayStoreAll
>(cvc5::ArrayStoreAll(*sort
.d_type
, n
));
5974 CVC5_API_TRY_CATCH_END
;
5977 Term
Solver::mkPosInf(uint32_t exp
, uint32_t sig
) const
5979 NodeManagerScope
scope(getNodeManager());
5980 CVC5_API_TRY_CATCH_BEGIN
;
5981 //////// all checks before this line
5982 return mkValHelper
<cvc5::FloatingPoint
>(
5983 FloatingPoint::makeInf(FloatingPointSize(exp
, sig
), false));
5985 CVC5_API_TRY_CATCH_END
;
5988 Term
Solver::mkNegInf(uint32_t exp
, uint32_t sig
) const
5990 NodeManagerScope
scope(getNodeManager());
5991 CVC5_API_TRY_CATCH_BEGIN
;
5992 //////// all checks before this line
5993 return mkValHelper
<cvc5::FloatingPoint
>(
5994 FloatingPoint::makeInf(FloatingPointSize(exp
, sig
), true));
5996 CVC5_API_TRY_CATCH_END
;
5999 Term
Solver::mkNaN(uint32_t exp
, uint32_t sig
) const
6001 NodeManagerScope
scope(getNodeManager());
6002 CVC5_API_TRY_CATCH_BEGIN
;
6003 //////// all checks before this line
6004 return mkValHelper
<cvc5::FloatingPoint
>(
6005 FloatingPoint::makeNaN(FloatingPointSize(exp
, sig
)));
6007 CVC5_API_TRY_CATCH_END
;
6010 Term
Solver::mkPosZero(uint32_t exp
, uint32_t sig
) const
6012 NodeManagerScope
scope(getNodeManager());
6013 CVC5_API_TRY_CATCH_BEGIN
;
6014 //////// all checks before this line
6015 return mkValHelper
<cvc5::FloatingPoint
>(
6016 FloatingPoint::makeZero(FloatingPointSize(exp
, sig
), false));
6018 CVC5_API_TRY_CATCH_END
;
6021 Term
Solver::mkNegZero(uint32_t exp
, uint32_t sig
) const
6023 NodeManagerScope
scope(getNodeManager());
6024 CVC5_API_TRY_CATCH_BEGIN
;
6025 //////// all checks before this line
6026 return mkValHelper
<cvc5::FloatingPoint
>(
6027 FloatingPoint::makeZero(FloatingPointSize(exp
, sig
), true));
6029 CVC5_API_TRY_CATCH_END
;
6032 Term
Solver::mkRoundingMode(RoundingMode rm
) const
6034 NodeManagerScope
scope(getNodeManager());
6035 CVC5_API_TRY_CATCH_BEGIN
;
6036 //////// all checks before this line
6037 return mkValHelper
<cvc5::RoundingMode
>(s_rmodes
.at(rm
));
6039 CVC5_API_TRY_CATCH_END
;
6042 Term
Solver::mkUninterpretedConst(const Sort
& sort
, int32_t index
) const
6044 NodeManagerScope
scope(getNodeManager());
6045 CVC5_API_TRY_CATCH_BEGIN
;
6046 CVC5_API_SOLVER_CHECK_SORT(sort
);
6047 //////// all checks before this line
6048 return mkValHelper
<cvc5::UninterpretedConstant
>(
6049 cvc5::UninterpretedConstant(*sort
.d_type
, index
));
6051 CVC5_API_TRY_CATCH_END
;
6054 Term
Solver::mkAbstractValue(const std::string
& index
) const
6056 NodeManagerScope
scope(getNodeManager());
6057 CVC5_API_TRY_CATCH_BEGIN
;
6058 CVC5_API_ARG_CHECK_EXPECTED(!index
.empty(), index
) << "a non-empty string";
6060 cvc5::Integer
idx(index
, 10);
6061 CVC5_API_ARG_CHECK_EXPECTED(idx
> 0, index
)
6062 << "a string representing an integer > 0";
6063 //////// all checks before this line
6064 return Term(this, getNodeManager()->mkConst(cvc5::AbstractValue(idx
)));
6065 // do not call getType(), for abstract values, type can not be computed
6066 // until it is substituted away
6068 CVC5_API_TRY_CATCH_END
;
6071 Term
Solver::mkAbstractValue(uint64_t index
) const
6073 NodeManagerScope
scope(getNodeManager());
6074 CVC5_API_TRY_CATCH_BEGIN
;
6075 CVC5_API_ARG_CHECK_EXPECTED(index
> 0, index
) << "an integer > 0";
6076 //////// all checks before this line
6078 getNodeManager()->mkConst(cvc5::AbstractValue(Integer(index
))));
6079 // do not call getType(), for abstract values, type can not be computed
6080 // until it is substituted away
6082 CVC5_API_TRY_CATCH_END
;
6085 Term
Solver::mkFloatingPoint(uint32_t exp
, uint32_t sig
, Term val
) const
6087 NodeManagerScope
scope(getNodeManager());
6088 CVC5_API_TRY_CATCH_BEGIN
;
6089 CVC5_API_SOLVER_CHECK_TERM(val
);
6090 CVC5_API_ARG_CHECK_EXPECTED(exp
> 0, exp
) << "a value > 0";
6091 CVC5_API_ARG_CHECK_EXPECTED(sig
> 0, sig
) << "a value > 0";
6092 uint32_t bw
= exp
+ sig
;
6093 CVC5_API_ARG_CHECK_EXPECTED(bw
== val
.getSort().getBVSize(), val
)
6094 << "a bit-vector constant with bit-width '" << bw
<< "'";
6095 CVC5_API_ARG_CHECK_EXPECTED(
6096 val
.getSort().isBitVector() && val
.d_node
->isConst(), val
)
6097 << "bit-vector constant";
6098 //////// all checks before this line
6099 return mkValHelper
<cvc5::FloatingPoint
>(
6100 cvc5::FloatingPoint(exp
, sig
, val
.d_node
->getConst
<BitVector
>()));
6102 CVC5_API_TRY_CATCH_END
;
6105 /* Create constants */
6106 /* -------------------------------------------------------------------------- */
6108 Term
Solver::mkConst(const Sort
& sort
, const std::string
& symbol
) const
6110 NodeManagerScope
scope(getNodeManager());
6111 CVC5_API_TRY_CATCH_BEGIN
;
6112 CVC5_API_SOLVER_CHECK_SORT(sort
);
6113 //////// all checks before this line
6114 Node res
= d_nodeMgr
->mkVar(symbol
, *sort
.d_type
);
6115 (void)res
.getType(true); /* kick off type checking */
6116 increment_vars_consts_stats(sort
, false);
6117 return Term(this, res
);
6119 CVC5_API_TRY_CATCH_END
;
6122 Term
Solver::mkConst(const Sort
& sort
) const
6124 NodeManagerScope
scope(getNodeManager());
6125 CVC5_API_TRY_CATCH_BEGIN
;
6126 CVC5_API_SOLVER_CHECK_SORT(sort
);
6127 //////// all checks before this line
6128 Node res
= d_nodeMgr
->mkVar(*sort
.d_type
);
6129 (void)res
.getType(true); /* kick off type checking */
6130 increment_vars_consts_stats(sort
, false);
6131 return Term(this, res
);
6133 CVC5_API_TRY_CATCH_END
;
6136 /* Create variables */
6137 /* -------------------------------------------------------------------------- */
6139 Term
Solver::mkVar(const Sort
& sort
, const std::string
& symbol
) const
6141 NodeManagerScope
scope(getNodeManager());
6142 CVC5_API_TRY_CATCH_BEGIN
;
6143 CVC5_API_SOLVER_CHECK_SORT(sort
);
6144 //////// all checks before this line
6145 Node res
= symbol
.empty() ? d_nodeMgr
->mkBoundVar(*sort
.d_type
)
6146 : d_nodeMgr
->mkBoundVar(symbol
, *sort
.d_type
);
6147 (void)res
.getType(true); /* kick off type checking */
6148 increment_vars_consts_stats(sort
, true);
6149 return Term(this, res
);
6151 CVC5_API_TRY_CATCH_END
;
6154 /* Create datatype constructor declarations */
6155 /* -------------------------------------------------------------------------- */
6157 DatatypeConstructorDecl
Solver::mkDatatypeConstructorDecl(
6158 const std::string
& name
)
6160 NodeManagerScope
scope(getNodeManager());
6161 CVC5_API_TRY_CATCH_BEGIN
;
6162 //////// all checks before this line
6163 return DatatypeConstructorDecl(this, name
);
6165 CVC5_API_TRY_CATCH_END
;
6168 /* Create datatype declarations */
6169 /* -------------------------------------------------------------------------- */
6171 DatatypeDecl
Solver::mkDatatypeDecl(const std::string
& name
, bool isCoDatatype
)
6173 NodeManagerScope
scope(getNodeManager());
6174 CVC5_API_TRY_CATCH_BEGIN
;
6175 //////// all checks before this line
6176 return DatatypeDecl(this, name
, isCoDatatype
);
6178 CVC5_API_TRY_CATCH_END
;
6181 DatatypeDecl
Solver::mkDatatypeDecl(const std::string
& name
,
6185 NodeManagerScope
scope(getNodeManager());
6186 CVC5_API_TRY_CATCH_BEGIN
;
6187 CVC5_API_SOLVER_CHECK_SORT(param
);
6188 //////// all checks before this line
6189 return DatatypeDecl(this, name
, param
, isCoDatatype
);
6191 CVC5_API_TRY_CATCH_END
;
6194 DatatypeDecl
Solver::mkDatatypeDecl(const std::string
& name
,
6195 const std::vector
<Sort
>& params
,
6198 NodeManagerScope
scope(getNodeManager());
6199 CVC5_API_TRY_CATCH_BEGIN
;
6200 CVC5_API_SOLVER_CHECK_SORTS(params
);
6201 //////// all checks before this line
6202 return DatatypeDecl(this, name
, params
, isCoDatatype
);
6204 CVC5_API_TRY_CATCH_END
;
6208 /* -------------------------------------------------------------------------- */
6210 Term
Solver::mkTerm(Kind kind
) const
6212 NodeManagerScope
scope(getNodeManager());
6213 CVC5_API_TRY_CATCH_BEGIN
;
6214 CVC5_API_KIND_CHECK(kind
);
6215 //////// all checks before this line
6216 return mkTermFromKind(kind
);
6218 CVC5_API_TRY_CATCH_END
;
6221 Term
Solver::mkTerm(Kind kind
, const Term
& child
) const
6223 NodeManagerScope
scope(getNodeManager());
6224 CVC5_API_TRY_CATCH_BEGIN
;
6225 CVC5_API_KIND_CHECK(kind
);
6226 CVC5_API_SOLVER_CHECK_TERM(child
);
6227 //////// all checks before this line
6228 return mkTermHelper(kind
, std::vector
<Term
>{child
});
6230 CVC5_API_TRY_CATCH_END
;
6233 Term
Solver::mkTerm(Kind kind
, const Term
& child1
, const Term
& child2
) const
6235 NodeManagerScope
scope(getNodeManager());
6236 CVC5_API_TRY_CATCH_BEGIN
;
6237 CVC5_API_KIND_CHECK(kind
);
6238 CVC5_API_SOLVER_CHECK_TERM(child1
);
6239 CVC5_API_SOLVER_CHECK_TERM(child2
);
6240 //////// all checks before this line
6241 return mkTermHelper(kind
, std::vector
<Term
>{child1
, child2
});
6243 CVC5_API_TRY_CATCH_END
;
6246 Term
Solver::mkTerm(Kind kind
,
6249 const Term
& child3
) const
6251 NodeManagerScope
scope(getNodeManager());
6252 CVC5_API_TRY_CATCH_BEGIN
;
6253 CVC5_API_KIND_CHECK(kind
);
6254 CVC5_API_SOLVER_CHECK_TERM(child1
);
6255 CVC5_API_SOLVER_CHECK_TERM(child2
);
6256 CVC5_API_SOLVER_CHECK_TERM(child3
);
6257 //////// all checks before this line
6258 // need to use internal term call to check e.g. associative construction
6259 return mkTermHelper(kind
, std::vector
<Term
>{child1
, child2
, child3
});
6261 CVC5_API_TRY_CATCH_END
;
6264 Term
Solver::mkTerm(Kind kind
, const std::vector
<Term
>& children
) const
6266 NodeManagerScope
scope(getNodeManager());
6267 CVC5_API_TRY_CATCH_BEGIN
;
6268 CVC5_API_KIND_CHECK(kind
);
6269 CVC5_API_SOLVER_CHECK_TERMS(children
);
6270 //////// all checks before this line
6271 return mkTermHelper(kind
, children
);
6273 CVC5_API_TRY_CATCH_END
;
6276 Term
Solver::mkTerm(const Op
& op
) const
6278 NodeManagerScope
scope(getNodeManager());
6279 CVC5_API_TRY_CATCH_BEGIN
;
6280 CVC5_API_SOLVER_CHECK_OP(op
);
6281 checkMkTerm(op
.d_kind
, 0);
6282 //////// all checks before this line
6284 if (!op
.isIndexedHelper())
6286 return mkTermFromKind(op
.d_kind
);
6289 const cvc5::Kind int_kind
= extToIntKind(op
.d_kind
);
6290 Term res
= Term(this, getNodeManager()->mkNode(int_kind
, *op
.d_node
));
6292 (void)res
.d_node
->getType(true); /* kick off type checking */
6295 CVC5_API_TRY_CATCH_END
;
6298 Term
Solver::mkTerm(const Op
& op
, const Term
& child
) const
6300 NodeManagerScope
scope(getNodeManager());
6301 CVC5_API_TRY_CATCH_BEGIN
;
6302 CVC5_API_SOLVER_CHECK_OP(op
);
6303 CVC5_API_SOLVER_CHECK_TERM(child
);
6304 //////// all checks before this line
6305 return mkTermHelper(op
, std::vector
<Term
>{child
});
6307 CVC5_API_TRY_CATCH_END
;
6310 Term
Solver::mkTerm(const Op
& op
, const Term
& child1
, const Term
& child2
) const
6312 NodeManagerScope
scope(getNodeManager());
6313 CVC5_API_TRY_CATCH_BEGIN
;
6314 CVC5_API_SOLVER_CHECK_OP(op
);
6315 CVC5_API_SOLVER_CHECK_TERM(child1
);
6316 CVC5_API_SOLVER_CHECK_TERM(child2
);
6317 //////// all checks before this line
6318 return mkTermHelper(op
, std::vector
<Term
>{child1
, child2
});
6320 CVC5_API_TRY_CATCH_END
;
6323 Term
Solver::mkTerm(const Op
& op
,
6326 const Term
& child3
) const
6328 NodeManagerScope
scope(getNodeManager());
6329 CVC5_API_TRY_CATCH_BEGIN
;
6330 CVC5_API_SOLVER_CHECK_OP(op
);
6331 CVC5_API_SOLVER_CHECK_TERM(child1
);
6332 CVC5_API_SOLVER_CHECK_TERM(child2
);
6333 CVC5_API_SOLVER_CHECK_TERM(child3
);
6334 //////// all checks before this line
6335 return mkTermHelper(op
, std::vector
<Term
>{child1
, child2
, child3
});
6337 CVC5_API_TRY_CATCH_END
;
6340 Term
Solver::mkTerm(const Op
& op
, const std::vector
<Term
>& children
) const
6342 NodeManagerScope
scope(getNodeManager());
6343 CVC5_API_TRY_CATCH_BEGIN
;
6344 CVC5_API_SOLVER_CHECK_OP(op
);
6345 CVC5_API_SOLVER_CHECK_TERMS(children
);
6346 //////// all checks before this line
6347 return mkTermHelper(op
, children
);
6349 CVC5_API_TRY_CATCH_END
;
6352 Term
Solver::mkTuple(const std::vector
<Sort
>& sorts
,
6353 const std::vector
<Term
>& terms
) const
6355 NodeManagerScope
scope(getNodeManager());
6356 CVC5_API_TRY_CATCH_BEGIN
;
6357 CVC5_API_CHECK(sorts
.size() == terms
.size())
6358 << "Expected the same number of sorts and elements";
6359 CVC5_API_SOLVER_CHECK_SORTS(sorts
);
6360 CVC5_API_SOLVER_CHECK_TERMS(terms
);
6361 //////// all checks before this line
6362 std::vector
<cvc5::Node
> args
;
6363 for (size_t i
= 0, size
= sorts
.size(); i
< size
; i
++)
6365 args
.push_back(*(ensureTermSort(terms
[i
], sorts
[i
])).d_node
);
6368 Sort s
= mkTupleSortHelper(sorts
);
6369 Datatype dt
= s
.getDatatype();
6370 NodeBuilder
nb(extToIntKind(APPLY_CONSTRUCTOR
));
6371 nb
<< *dt
[0].getConstructorTerm().d_node
;
6373 Node res
= nb
.constructNode();
6374 (void)res
.getType(true); /* kick off type checking */
6375 return Term(this, res
);
6377 CVC5_API_TRY_CATCH_END
;
6380 /* Create operators */
6381 /* -------------------------------------------------------------------------- */
6383 Op
Solver::mkOp(Kind kind
) const
6385 CVC5_API_TRY_CATCH_BEGIN
;
6386 CVC5_API_KIND_CHECK(kind
);
6387 CVC5_API_CHECK(s_indexed_kinds
.find(kind
) == s_indexed_kinds
.end())
6388 << "Expected a kind for a non-indexed operator.";
6389 //////// all checks before this line
6390 return Op(this, kind
);
6392 CVC5_API_TRY_CATCH_END
6395 Op
Solver::mkOp(Kind kind
, const std::string
& arg
) const
6397 CVC5_API_TRY_CATCH_BEGIN
;
6398 CVC5_API_KIND_CHECK(kind
);
6399 CVC5_API_KIND_CHECK_EXPECTED((kind
== DIVISIBLE
), kind
) << "DIVISIBLE";
6400 //////// all checks before this line
6402 /* CLN and GMP handle this case differently, CLN interprets it as 0, GMP
6403 * throws an std::invalid_argument exception. For consistency, we treat it
6405 CVC5_API_ARG_CHECK_EXPECTED(arg
!= ".", arg
)
6406 << "a string representing an integer, real or rational value.";
6409 *mkValHelper
<cvc5::Divisible
>(cvc5::Divisible(cvc5::Integer(arg
)))
6413 CVC5_API_TRY_CATCH_END
;
6416 Op
Solver::mkOp(Kind kind
, uint32_t arg
) const
6418 CVC5_API_TRY_CATCH_BEGIN
;
6419 CVC5_API_KIND_CHECK(kind
);
6420 //////// all checks before this line
6427 *mkValHelper
<cvc5::Divisible
>(cvc5::Divisible(arg
)).d_node
);
6429 case BITVECTOR_REPEAT
:
6432 *mkValHelper
<cvc5::BitVectorRepeat
>(cvc5::BitVectorRepeat(arg
))
6435 case BITVECTOR_ZERO_EXTEND
:
6438 *mkValHelper
<cvc5::BitVectorZeroExtend
>(
6439 cvc5::BitVectorZeroExtend(arg
))
6442 case BITVECTOR_SIGN_EXTEND
:
6445 *mkValHelper
<cvc5::BitVectorSignExtend
>(
6446 cvc5::BitVectorSignExtend(arg
))
6449 case BITVECTOR_ROTATE_LEFT
:
6452 *mkValHelper
<cvc5::BitVectorRotateLeft
>(
6453 cvc5::BitVectorRotateLeft(arg
))
6456 case BITVECTOR_ROTATE_RIGHT
:
6459 *mkValHelper
<cvc5::BitVectorRotateRight
>(
6460 cvc5::BitVectorRotateRight(arg
))
6463 case INT_TO_BITVECTOR
:
6467 *mkValHelper
<cvc5::IntToBitVector
>(cvc5::IntToBitVector(arg
)).d_node
);
6471 Op(this, kind
, *mkValHelper
<cvc5::IntAnd
>(cvc5::IntAnd(arg
)).d_node
);
6473 case FLOATINGPOINT_TO_UBV
:
6477 *mkValHelper
<cvc5::FloatingPointToUBV
>(cvc5::FloatingPointToUBV(arg
))
6480 case FLOATINGPOINT_TO_SBV
:
6484 *mkValHelper
<cvc5::FloatingPointToSBV
>(cvc5::FloatingPointToSBV(arg
))
6491 *mkValHelper
<cvc5::RegExpRepeat
>(cvc5::RegExpRepeat(arg
)).d_node
);
6494 CVC5_API_KIND_CHECK_EXPECTED(false, kind
)
6495 << "operator kind with uint32_t argument";
6497 Assert(!res
.isNull());
6500 CVC5_API_TRY_CATCH_END
;
6503 Op
Solver::mkOp(Kind kind
, uint32_t arg1
, uint32_t arg2
) const
6505 CVC5_API_TRY_CATCH_BEGIN
;
6506 CVC5_API_KIND_CHECK(kind
);
6507 //////// all checks before this line
6512 case BITVECTOR_EXTRACT
:
6515 *mkValHelper
<cvc5::BitVectorExtract
>(
6516 cvc5::BitVectorExtract(arg1
, arg2
))
6519 case FLOATINGPOINT_TO_FP_IEEE_BITVECTOR
:
6522 *mkValHelper
<cvc5::FloatingPointToFPIEEEBitVector
>(
6523 cvc5::FloatingPointToFPIEEEBitVector(arg1
, arg2
))
6526 case FLOATINGPOINT_TO_FP_FLOATINGPOINT
:
6529 *mkValHelper
<cvc5::FloatingPointToFPFloatingPoint
>(
6530 cvc5::FloatingPointToFPFloatingPoint(arg1
, arg2
))
6533 case FLOATINGPOINT_TO_FP_REAL
:
6536 *mkValHelper
<cvc5::FloatingPointToFPReal
>(
6537 cvc5::FloatingPointToFPReal(arg1
, arg2
))
6540 case FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR
:
6543 *mkValHelper
<cvc5::FloatingPointToFPSignedBitVector
>(
6544 cvc5::FloatingPointToFPSignedBitVector(arg1
, arg2
))
6547 case FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR
:
6550 *mkValHelper
<cvc5::FloatingPointToFPUnsignedBitVector
>(
6551 cvc5::FloatingPointToFPUnsignedBitVector(arg1
, arg2
))
6554 case FLOATINGPOINT_TO_FP_GENERIC
:
6557 *mkValHelper
<cvc5::FloatingPointToFPGeneric
>(
6558 cvc5::FloatingPointToFPGeneric(arg1
, arg2
))
6565 *mkValHelper
<cvc5::RegExpLoop
>(cvc5::RegExpLoop(arg1
, arg2
)).d_node
);
6568 CVC5_API_KIND_CHECK_EXPECTED(false, kind
)
6569 << "operator kind with two uint32_t arguments";
6571 Assert(!res
.isNull());
6574 CVC5_API_TRY_CATCH_END
;
6577 Op
Solver::mkOp(Kind kind
, const std::vector
<uint32_t>& args
) const
6579 CVC5_API_TRY_CATCH_BEGIN
;
6580 CVC5_API_KIND_CHECK(kind
);
6581 //////// all checks before this line
6590 *mkValHelper
<cvc5::TupleProjectOp
>(cvc5::TupleProjectOp(args
))
6596 std::string message
= "operator kind with " + std::to_string(args
.size())
6597 + " uint32_t arguments";
6598 CVC5_API_KIND_CHECK_EXPECTED(false, kind
) << message
;
6601 Assert(!res
.isNull());
6604 CVC5_API_TRY_CATCH_END
;
6607 /* Non-SMT-LIB commands */
6608 /* -------------------------------------------------------------------------- */
6610 Term
Solver::simplify(const Term
& term
)
6612 NodeManagerScope
scope(getNodeManager());
6613 CVC5_API_TRY_CATCH_BEGIN
;
6614 CVC5_API_SOLVER_CHECK_TERM(term
);
6615 //////// all checks before this line
6616 return Term(this, d_smtEngine
->simplify(*term
.d_node
));
6618 CVC5_API_TRY_CATCH_END
;
6621 Result
Solver::checkEntailed(const Term
& term
) const
6623 NodeManagerScope
scope(getNodeManager());
6624 CVC5_API_TRY_CATCH_BEGIN
;
6625 CVC5_API_CHECK(!d_smtEngine
->isQueryMade()
6626 || d_smtEngine
->getOptions().base
.incrementalSolving
)
6627 << "Cannot make multiple queries unless incremental solving is enabled "
6628 "(try --incremental)";
6629 CVC5_API_SOLVER_CHECK_TERM(term
);
6630 //////// all checks before this line
6631 return d_smtEngine
->checkEntailed(*term
.d_node
);
6633 CVC5_API_TRY_CATCH_END
;
6636 Result
Solver::checkEntailed(const std::vector
<Term
>& terms
) const
6638 CVC5_API_TRY_CATCH_BEGIN
;
6639 NodeManagerScope
scope(getNodeManager());
6640 CVC5_API_CHECK(!d_smtEngine
->isQueryMade()
6641 || d_smtEngine
->getOptions().base
.incrementalSolving
)
6642 << "Cannot make multiple queries unless incremental solving is enabled "
6643 "(try --incremental)";
6644 CVC5_API_SOLVER_CHECK_TERMS(terms
);
6645 //////// all checks before this line
6646 return d_smtEngine
->checkEntailed(Term::termVectorToNodes(terms
));
6648 CVC5_API_TRY_CATCH_END
;
6651 /* SMT-LIB commands */
6652 /* -------------------------------------------------------------------------- */
6654 void Solver::assertFormula(const Term
& term
) const
6656 CVC5_API_TRY_CATCH_BEGIN
;
6657 CVC5_API_SOLVER_CHECK_TERM(term
);
6658 CVC5_API_SOLVER_CHECK_TERM_WITH_SORT(term
, getBooleanSort());
6659 //////// all checks before this line
6660 d_smtEngine
->assertFormula(*term
.d_node
);
6662 CVC5_API_TRY_CATCH_END
;
6665 Result
Solver::checkSat(void) const
6667 CVC5_API_TRY_CATCH_BEGIN
;
6668 NodeManagerScope
scope(getNodeManager());
6669 CVC5_API_CHECK(!d_smtEngine
->isQueryMade()
6670 || d_smtEngine
->getOptions().base
.incrementalSolving
)
6671 << "Cannot make multiple queries unless incremental solving is enabled "
6672 "(try --incremental)";
6673 //////// all checks before this line
6674 return d_smtEngine
->checkSat();
6676 CVC5_API_TRY_CATCH_END
;
6679 Result
Solver::checkSatAssuming(const Term
& assumption
) const
6681 CVC5_API_TRY_CATCH_BEGIN
;
6682 NodeManagerScope
scope(getNodeManager());
6683 CVC5_API_CHECK(!d_smtEngine
->isQueryMade()
6684 || d_smtEngine
->getOptions().base
.incrementalSolving
)
6685 << "Cannot make multiple queries unless incremental solving is enabled "
6686 "(try --incremental)";
6687 CVC5_API_SOLVER_CHECK_TERM_WITH_SORT(assumption
, getBooleanSort());
6688 //////// all checks before this line
6689 return d_smtEngine
->checkSat(*assumption
.d_node
);
6691 CVC5_API_TRY_CATCH_END
;
6694 Result
Solver::checkSatAssuming(const std::vector
<Term
>& assumptions
) const
6696 CVC5_API_TRY_CATCH_BEGIN
;
6697 NodeManagerScope
scope(getNodeManager());
6698 CVC5_API_CHECK(!d_smtEngine
->isQueryMade() || assumptions
.size() == 0
6699 || d_smtEngine
->getOptions().base
.incrementalSolving
)
6700 << "Cannot make multiple queries unless incremental solving is enabled "
6701 "(try --incremental)";
6702 CVC5_API_SOLVER_CHECK_TERMS_WITH_SORT(assumptions
, getBooleanSort());
6703 //////// all checks before this line
6704 for (const Term
& term
: assumptions
)
6706 CVC5_API_SOLVER_CHECK_TERM(term
);
6708 std::vector
<Node
> eassumptions
= Term::termVectorToNodes(assumptions
);
6709 return d_smtEngine
->checkSat(eassumptions
);
6711 CVC5_API_TRY_CATCH_END
;
6714 Sort
Solver::declareDatatype(
6715 const std::string
& symbol
,
6716 const std::vector
<DatatypeConstructorDecl
>& ctors
) const
6718 CVC5_API_TRY_CATCH_BEGIN
;
6719 CVC5_API_ARG_CHECK_EXPECTED(ctors
.size() > 0, ctors
)
6720 << "a datatype declaration with at least one constructor";
6721 CVC5_API_SOLVER_CHECK_DTCTORDECLS(ctors
);
6722 //////// all checks before this line
6723 DatatypeDecl
dtdecl(this, symbol
);
6724 for (size_t i
= 0, size
= ctors
.size(); i
< size
; i
++)
6726 dtdecl
.addConstructor(ctors
[i
]);
6728 return Sort(this, getNodeManager()->mkDatatypeType(*dtdecl
.d_dtype
));
6730 CVC5_API_TRY_CATCH_END
;
6733 Term
Solver::declareFun(const std::string
& symbol
,
6734 const std::vector
<Sort
>& sorts
,
6735 const Sort
& sort
) const
6737 CVC5_API_TRY_CATCH_BEGIN
;
6738 CVC5_API_SOLVER_CHECK_DOMAIN_SORTS(sorts
);
6739 CVC5_API_SOLVER_CHECK_CODOMAIN_SORT(sort
);
6740 //////// all checks before this line
6742 TypeNode type
= *sort
.d_type
;
6745 std::vector
<TypeNode
> types
= Sort::sortVectorToTypeNodes(sorts
);
6746 type
= getNodeManager()->mkFunctionType(types
, type
);
6748 return Term(this, d_nodeMgr
->mkVar(symbol
, type
));
6750 CVC5_API_TRY_CATCH_END
;
6753 Sort
Solver::declareSort(const std::string
& symbol
, uint32_t arity
) const
6755 CVC5_API_TRY_CATCH_BEGIN
;
6756 //////// all checks before this line
6759 return Sort(this, getNodeManager()->mkSort(symbol
));
6761 return Sort(this, getNodeManager()->mkSortConstructor(symbol
, arity
));
6763 CVC5_API_TRY_CATCH_END
;
6766 Term
Solver::defineFun(const std::string
& symbol
,
6767 const std::vector
<Term
>& bound_vars
,
6772 CVC5_API_TRY_CATCH_BEGIN
;
6773 CVC5_API_SOLVER_CHECK_CODOMAIN_SORT(sort
);
6774 CVC5_API_SOLVER_CHECK_TERM(term
);
6775 CVC5_API_CHECK(sort
== term
.getSort())
6776 << "Invalid sort of function body '" << term
<< "', expected '" << sort
6779 std::vector
<Sort
> domain_sorts
;
6780 for (const auto& bv
: bound_vars
)
6782 domain_sorts
.push_back(bv
.getSort());
6785 domain_sorts
.empty()
6788 getNodeManager()->mkFunctionType(
6789 Sort::sortVectorToTypeNodes(domain_sorts
), *sort
.d_type
));
6790 Term fun
= mkConst(fun_sort
, symbol
);
6792 CVC5_API_SOLVER_CHECK_BOUND_VARS_DEF_FUN(fun
, bound_vars
, domain_sorts
);
6793 //////// all checks before this line
6795 d_smtEngine
->defineFunction(
6796 *fun
.d_node
, Term::termVectorToNodes(bound_vars
), *term
.d_node
, global
);
6799 CVC5_API_TRY_CATCH_END
;
6802 Term
Solver::defineFun(const Term
& fun
,
6803 const std::vector
<Term
>& bound_vars
,
6807 CVC5_API_TRY_CATCH_BEGIN
;
6808 CVC5_API_SOLVER_CHECK_TERM(fun
);
6809 CVC5_API_SOLVER_CHECK_TERM(term
);
6810 if (fun
.getSort().isFunction())
6812 std::vector
<Sort
> domain_sorts
= fun
.getSort().getFunctionDomainSorts();
6813 CVC5_API_SOLVER_CHECK_BOUND_VARS_DEF_FUN(fun
, bound_vars
, domain_sorts
);
6814 Sort codomain
= fun
.getSort().getFunctionCodomainSort();
6815 CVC5_API_CHECK(codomain
== term
.getSort())
6816 << "Invalid sort of function body '" << term
<< "', expected '"
6821 CVC5_API_SOLVER_CHECK_BOUND_VARS(bound_vars
);
6822 CVC5_API_ARG_CHECK_EXPECTED(bound_vars
.size() == 0, fun
)
6823 << "function or nullary symbol";
6825 //////// all checks before this line
6826 std::vector
<Node
> ebound_vars
= Term::termVectorToNodes(bound_vars
);
6827 d_smtEngine
->defineFunction(*fun
.d_node
, ebound_vars
, *term
.d_node
, global
);
6830 CVC5_API_TRY_CATCH_END
;
6833 Term
Solver::defineFunRec(const std::string
& symbol
,
6834 const std::vector
<Term
>& bound_vars
,
6839 NodeManagerScope
scope(getNodeManager());
6840 CVC5_API_TRY_CATCH_BEGIN
;
6842 CVC5_API_CHECK(d_smtEngine
->getUserLogicInfo().isQuantified())
6843 << "recursive function definitions require a logic with quantifiers";
6845 d_smtEngine
->getUserLogicInfo().isTheoryEnabled(theory::THEORY_UF
))
6846 << "recursive function definitions require a logic with uninterpreted "
6849 CVC5_API_SOLVER_CHECK_TERM(term
);
6850 CVC5_API_SOLVER_CHECK_CODOMAIN_SORT(sort
);
6851 CVC5_API_CHECK(sort
== term
.getSort())
6852 << "Invalid sort of function body '" << term
<< "', expected '" << sort
6855 std::vector
<Sort
> domain_sorts
;
6856 for (const auto& bv
: bound_vars
)
6858 domain_sorts
.push_back(bv
.getSort());
6861 domain_sorts
.empty()
6864 getNodeManager()->mkFunctionType(
6865 Sort::sortVectorToTypeNodes(domain_sorts
), *sort
.d_type
));
6866 Term fun
= mkConst(fun_sort
, symbol
);
6868 CVC5_API_SOLVER_CHECK_BOUND_VARS_DEF_FUN(fun
, bound_vars
, domain_sorts
);
6869 //////// all checks before this line
6871 d_smtEngine
->defineFunctionRec(
6872 *fun
.d_node
, Term::termVectorToNodes(bound_vars
), *term
.d_node
, global
);
6876 CVC5_API_TRY_CATCH_END
;
6879 Term
Solver::defineFunRec(const Term
& fun
,
6880 const std::vector
<Term
>& bound_vars
,
6884 NodeManagerScope
scope(getNodeManager());
6885 CVC5_API_TRY_CATCH_BEGIN
;
6887 CVC5_API_CHECK(d_smtEngine
->getUserLogicInfo().isQuantified())
6888 << "recursive function definitions require a logic with quantifiers";
6890 d_smtEngine
->getUserLogicInfo().isTheoryEnabled(theory::THEORY_UF
))
6891 << "recursive function definitions require a logic with uninterpreted "
6894 CVC5_API_SOLVER_CHECK_TERM(fun
);
6895 CVC5_API_SOLVER_CHECK_TERM(term
);
6896 if (fun
.getSort().isFunction())
6898 std::vector
<Sort
> domain_sorts
= fun
.getSort().getFunctionDomainSorts();
6899 CVC5_API_SOLVER_CHECK_BOUND_VARS_DEF_FUN(fun
, bound_vars
, domain_sorts
);
6900 Sort codomain
= fun
.getSort().getFunctionCodomainSort();
6901 CVC5_API_CHECK(codomain
== term
.getSort())
6902 << "Invalid sort of function body '" << term
<< "', expected '"
6907 CVC5_API_SOLVER_CHECK_BOUND_VARS(bound_vars
);
6908 CVC5_API_ARG_CHECK_EXPECTED(bound_vars
.size() == 0, fun
)
6909 << "function or nullary symbol";
6911 //////// all checks before this line
6913 std::vector
<Node
> ebound_vars
= Term::termVectorToNodes(bound_vars
);
6914 d_smtEngine
->defineFunctionRec(
6915 *fun
.d_node
, ebound_vars
, *term
.d_node
, global
);
6918 CVC5_API_TRY_CATCH_END
;
6921 void Solver::defineFunsRec(const std::vector
<Term
>& funs
,
6922 const std::vector
<std::vector
<Term
>>& bound_vars
,
6923 const std::vector
<Term
>& terms
,
6926 NodeManagerScope
scope(getNodeManager());
6927 CVC5_API_TRY_CATCH_BEGIN
;
6929 CVC5_API_CHECK(d_smtEngine
->getUserLogicInfo().isQuantified())
6930 << "recursive function definitions require a logic with quantifiers";
6932 d_smtEngine
->getUserLogicInfo().isTheoryEnabled(theory::THEORY_UF
))
6933 << "recursive function definitions require a logic with uninterpreted "
6935 CVC5_API_SOLVER_CHECK_TERMS(funs
);
6936 CVC5_API_SOLVER_CHECK_TERMS(terms
);
6938 size_t funs_size
= funs
.size();
6939 CVC5_API_ARG_SIZE_CHECK_EXPECTED(funs_size
== bound_vars
.size(), bound_vars
)
6940 << "'" << funs_size
<< "'";
6941 CVC5_API_ARG_SIZE_CHECK_EXPECTED(funs_size
== terms
.size(), terms
)
6942 << "'" << funs_size
<< "'";
6944 for (size_t j
= 0; j
< funs_size
; ++j
)
6946 const Term
& fun
= funs
[j
];
6947 const std::vector
<Term
>& bvars
= bound_vars
[j
];
6948 const Term
& term
= terms
[j
];
6950 CVC5_API_ARG_AT_INDEX_CHECK_EXPECTED(
6951 this == fun
.d_solver
, "function", funs
, j
)
6952 << "function associated with this solver object";
6953 CVC5_API_ARG_AT_INDEX_CHECK_EXPECTED(
6954 this == term
.d_solver
, "term", terms
, j
)
6955 << "term associated with this solver object";
6957 if (fun
.getSort().isFunction())
6959 std::vector
<Sort
> domain_sorts
= fun
.getSort().getFunctionDomainSorts();
6960 CVC5_API_SOLVER_CHECK_BOUND_VARS_DEF_FUN(fun
, bvars
, domain_sorts
);
6961 Sort codomain
= fun
.getSort().getFunctionCodomainSort();
6962 CVC5_API_ARG_AT_INDEX_CHECK_EXPECTED(
6963 codomain
== term
.getSort(), "sort of function body", terms
, j
)
6964 << "'" << codomain
<< "'";
6968 CVC5_API_SOLVER_CHECK_BOUND_VARS(bvars
);
6969 CVC5_API_ARG_CHECK_EXPECTED(bvars
.size() == 0, fun
)
6970 << "function or nullary symbol";
6973 //////// all checks before this line
6974 std::vector
<Node
> efuns
= Term::termVectorToNodes(funs
);
6975 std::vector
<std::vector
<Node
>> ebound_vars
;
6976 for (const auto& v
: bound_vars
)
6978 ebound_vars
.push_back(Term::termVectorToNodes(v
));
6980 std::vector
<Node
> nodes
= Term::termVectorToNodes(terms
);
6981 d_smtEngine
->defineFunctionsRec(efuns
, ebound_vars
, nodes
, global
);
6983 CVC5_API_TRY_CATCH_END
;
6986 void Solver::echo(std::ostream
& out
, const std::string
& str
) const
6991 std::vector
<Term
> Solver::getAssertions(void) const
6993 CVC5_API_TRY_CATCH_BEGIN
;
6994 //////// all checks before this line
6995 std::vector
<Node
> assertions
= d_smtEngine
->getAssertions();
6997 * return std::vector<Term>(assertions.begin(), assertions.end());
6998 * here since constructor is private */
6999 std::vector
<Term
> res
;
7000 for (const Node
& e
: assertions
)
7002 res
.push_back(Term(this, e
));
7006 CVC5_API_TRY_CATCH_END
;
7009 std::string
Solver::getInfo(const std::string
& flag
) const
7011 CVC5_API_TRY_CATCH_BEGIN
;
7012 CVC5_API_RECOVERABLE_CHECK(d_smtEngine
->isValidGetInfoFlag(flag
))
7013 << "Unrecognized flag for getInfo.";
7014 //////// all checks before this line
7015 return d_smtEngine
->getInfo(flag
);
7017 CVC5_API_TRY_CATCH_END
;
7020 std::string
Solver::getOption(const std::string
& option
) const
7022 CVC5_API_TRY_CATCH_BEGIN
;
7023 //////// all checks before this line
7024 return d_smtEngine
->getOption(option
);
7026 CVC5_API_TRY_CATCH_END
;
7029 std::vector
<std::string
> Solver::getOptionNames() const
7031 CVC5_API_TRY_CATCH_BEGIN
;
7032 //////// all checks before this line
7033 return options::getNames();
7035 CVC5_API_TRY_CATCH_END
;
7038 std::vector
<Term
> Solver::getUnsatAssumptions(void) const
7040 CVC5_API_TRY_CATCH_BEGIN
;
7041 NodeManagerScope
scope(getNodeManager());
7042 CVC5_API_CHECK(d_smtEngine
->getOptions().base
.incrementalSolving
)
7043 << "Cannot get unsat assumptions unless incremental solving is enabled "
7044 "(try --incremental)";
7045 CVC5_API_CHECK(d_smtEngine
->getOptions().smt
.unsatAssumptions
)
7046 << "Cannot get unsat assumptions unless explicitly enabled "
7047 "(try --produce-unsat-assumptions)";
7048 CVC5_API_CHECK(d_smtEngine
->getSmtMode() == SmtMode::UNSAT
)
7049 << "Cannot get unsat assumptions unless in unsat mode.";
7050 //////// all checks before this line
7052 std::vector
<Node
> uassumptions
= d_smtEngine
->getUnsatAssumptions();
7054 * return std::vector<Term>(uassumptions.begin(), uassumptions.end());
7055 * here since constructor is private */
7056 std::vector
<Term
> res
;
7057 for (const Node
& n
: uassumptions
)
7059 res
.push_back(Term(this, n
));
7063 CVC5_API_TRY_CATCH_END
;
7066 std::vector
<Term
> Solver::getUnsatCore(void) const
7068 CVC5_API_TRY_CATCH_BEGIN
;
7069 NodeManagerScope
scope(getNodeManager());
7070 CVC5_API_CHECK(d_smtEngine
->getOptions().smt
.unsatCores
)
7071 << "Cannot get unsat core unless explicitly enabled "
7072 "(try --produce-unsat-cores)";
7073 CVC5_API_RECOVERABLE_CHECK(d_smtEngine
->getSmtMode() == SmtMode::UNSAT
)
7074 << "Cannot get unsat core unless in unsat mode.";
7075 //////// all checks before this line
7076 UnsatCore core
= d_smtEngine
->getUnsatCore();
7078 * return std::vector<Term>(core.begin(), core.end());
7079 * here since constructor is private */
7080 std::vector
<Term
> res
;
7081 for (const Node
& e
: core
)
7083 res
.push_back(Term(this, e
));
7087 CVC5_API_TRY_CATCH_END
;
7090 std::string
Solver::getProof(void) const
7092 CVC5_API_TRY_CATCH_BEGIN
;
7093 NodeManagerScope
scope(getNodeManager());
7094 CVC5_API_CHECK(d_smtEngine
->getOptions().smt
.produceProofs
)
7095 << "Cannot get proof explicitly enabled (try --prooduce-proofs)";
7096 CVC5_API_RECOVERABLE_CHECK(d_smtEngine
->getSmtMode() == SmtMode::UNSAT
)
7097 << "Cannot get proof unless in unsat mode.";
7098 return d_smtEngine
->getProof();
7099 CVC5_API_TRY_CATCH_END
;
7102 Term
Solver::getValue(const Term
& term
) const
7104 CVC5_API_TRY_CATCH_BEGIN
;
7105 CVC5_API_SOLVER_CHECK_TERM(term
);
7106 //////// all checks before this line
7107 return getValueHelper(term
);
7109 CVC5_API_TRY_CATCH_END
;
7112 std::vector
<Term
> Solver::getValue(const std::vector
<Term
>& terms
) const
7114 CVC5_API_TRY_CATCH_BEGIN
;
7115 NodeManagerScope
scope(getNodeManager());
7116 CVC5_API_RECOVERABLE_CHECK(d_smtEngine
->getOptions().smt
.produceModels
)
7117 << "Cannot get value unless model generation is enabled "
7118 "(try --produce-models)";
7119 CVC5_API_RECOVERABLE_CHECK(d_smtEngine
->isSmtModeSat())
7120 << "Cannot get value unless after a SAT or unknown response.";
7121 CVC5_API_SOLVER_CHECK_TERMS(terms
);
7122 //////// all checks before this line
7124 std::vector
<Term
> res
;
7125 for (size_t i
= 0, n
= terms
.size(); i
< n
; ++i
)
7127 /* Can not use emplace_back here since constructor is private. */
7128 res
.push_back(getValueHelper(terms
[i
]));
7132 CVC5_API_TRY_CATCH_END
;
7135 Term
Solver::getQuantifierElimination(const Term
& q
) const
7137 NodeManagerScope
scope(getNodeManager());
7138 CVC5_API_TRY_CATCH_BEGIN
;
7139 CVC5_API_SOLVER_CHECK_TERM(q
);
7140 //////// all checks before this line
7142 d_smtEngine
->getQuantifierElimination(q
.getNode(), true, true));
7144 CVC5_API_TRY_CATCH_END
;
7147 Term
Solver::getQuantifierEliminationDisjunct(const Term
& q
) const
7149 NodeManagerScope
scope(getNodeManager());
7150 CVC5_API_TRY_CATCH_BEGIN
;
7151 CVC5_API_SOLVER_CHECK_TERM(q
);
7152 //////// all checks before this line
7154 d_smtEngine
->getQuantifierElimination(q
.getNode(), false, true));
7156 CVC5_API_TRY_CATCH_END
;
7159 void Solver::declareSeparationHeap(const Sort
& locSort
,
7160 const Sort
& dataSort
) const
7162 CVC5_API_TRY_CATCH_BEGIN
;
7163 CVC5_API_SOLVER_CHECK_SORT(locSort
);
7164 CVC5_API_SOLVER_CHECK_SORT(dataSort
);
7166 d_smtEngine
->getLogicInfo().isTheoryEnabled(theory::THEORY_SEP
))
7167 << "Cannot obtain separation logic expressions if not using the "
7168 "separation logic theory.";
7169 //////// all checks before this line
7170 d_smtEngine
->declareSepHeap(locSort
.getTypeNode(), dataSort
.getTypeNode());
7172 CVC5_API_TRY_CATCH_END
;
7175 Term
Solver::getSeparationHeap() const
7177 NodeManagerScope
scope(getNodeManager());
7178 CVC5_API_TRY_CATCH_BEGIN
;
7180 d_smtEngine
->getLogicInfo().isTheoryEnabled(theory::THEORY_SEP
))
7181 << "Cannot obtain separation logic expressions if not using the "
7182 "separation logic theory.";
7183 CVC5_API_CHECK(d_smtEngine
->getOptions().smt
.produceModels
)
7184 << "Cannot get separation heap term unless model generation is enabled "
7185 "(try --produce-models)";
7186 CVC5_API_RECOVERABLE_CHECK(d_smtEngine
->isSmtModeSat())
7187 << "Can only get separtion heap term after sat or unknown response.";
7188 //////// all checks before this line
7189 return Term(this, d_smtEngine
->getSepHeapExpr());
7191 CVC5_API_TRY_CATCH_END
;
7194 Term
Solver::getSeparationNilTerm() const
7196 NodeManagerScope
scope(getNodeManager());
7197 CVC5_API_TRY_CATCH_BEGIN
;
7199 d_smtEngine
->getLogicInfo().isTheoryEnabled(theory::THEORY_SEP
))
7200 << "Cannot obtain separation logic expressions if not using the "
7201 "separation logic theory.";
7202 CVC5_API_CHECK(d_smtEngine
->getOptions().smt
.produceModels
)
7203 << "Cannot get separation nil term unless model generation is enabled "
7204 "(try --produce-models)";
7205 CVC5_API_RECOVERABLE_CHECK(d_smtEngine
->isSmtModeSat())
7206 << "Can only get separtion nil term after sat or unknown response.";
7207 //////// all checks before this line
7208 return Term(this, d_smtEngine
->getSepNilExpr());
7210 CVC5_API_TRY_CATCH_END
;
7213 Term
Solver::declarePool(const std::string
& symbol
,
7215 const std::vector
<Term
>& initValue
) const
7217 NodeManagerScope
scope(getNodeManager());
7218 CVC5_API_TRY_CATCH_BEGIN
;
7219 CVC5_API_SOLVER_CHECK_SORT(sort
);
7220 CVC5_API_SOLVER_CHECK_TERMS(initValue
);
7221 //////// all checks before this line
7222 TypeNode setType
= getNodeManager()->mkSetType(*sort
.d_type
);
7223 Node pool
= getNodeManager()->mkBoundVar(symbol
, setType
);
7224 std::vector
<Node
> initv
= Term::termVectorToNodes(initValue
);
7225 d_smtEngine
->declarePool(pool
, initv
);
7226 return Term(this, pool
);
7228 CVC5_API_TRY_CATCH_END
;
7231 void Solver::pop(uint32_t nscopes
) const
7233 NodeManagerScope
scope(getNodeManager());
7234 CVC5_API_TRY_CATCH_BEGIN
;
7235 CVC5_API_CHECK(d_smtEngine
->getOptions().base
.incrementalSolving
)
7236 << "Cannot pop when not solving incrementally (use --incremental)";
7237 CVC5_API_CHECK(nscopes
<= d_smtEngine
->getNumUserLevels())
7238 << "Cannot pop beyond first pushed context";
7239 //////// all checks before this line
7240 for (uint32_t n
= 0; n
< nscopes
; ++n
)
7245 CVC5_API_TRY_CATCH_END
;
7248 bool Solver::getInterpolant(const Term
& conj
, Term
& output
) const
7250 NodeManagerScope
scope(getNodeManager());
7251 CVC5_API_TRY_CATCH_BEGIN
;
7252 CVC5_API_SOLVER_CHECK_TERM(conj
);
7253 //////// all checks before this line
7255 bool success
= d_smtEngine
->getInterpol(*conj
.d_node
, result
);
7258 output
= Term(this, result
);
7262 CVC5_API_TRY_CATCH_END
;
7265 bool Solver::getInterpolant(const Term
& conj
,
7269 NodeManagerScope
scope(getNodeManager());
7270 CVC5_API_TRY_CATCH_BEGIN
;
7271 CVC5_API_SOLVER_CHECK_TERM(conj
);
7272 //////// all checks before this line
7275 d_smtEngine
->getInterpol(*conj
.d_node
, *grammar
.resolve().d_type
, result
);
7278 output
= Term(this, result
);
7282 CVC5_API_TRY_CATCH_END
;
7285 bool Solver::getAbduct(const Term
& conj
, Term
& output
) const
7287 NodeManagerScope
scope(getNodeManager());
7288 CVC5_API_TRY_CATCH_BEGIN
;
7289 CVC5_API_SOLVER_CHECK_TERM(conj
);
7290 //////// all checks before this line
7292 bool success
= d_smtEngine
->getAbduct(*conj
.d_node
, result
);
7295 output
= Term(this, result
);
7299 CVC5_API_TRY_CATCH_END
;
7302 bool Solver::getAbduct(const Term
& conj
, Grammar
& grammar
, Term
& output
) const
7304 NodeManagerScope
scope(getNodeManager());
7305 CVC5_API_TRY_CATCH_BEGIN
;
7306 CVC5_API_SOLVER_CHECK_TERM(conj
);
7307 //////// all checks before this line
7310 d_smtEngine
->getAbduct(*conj
.d_node
, *grammar
.resolve().d_type
, result
);
7313 output
= Term(this, result
);
7317 CVC5_API_TRY_CATCH_END
;
7320 void Solver::blockModel() const
7322 NodeManagerScope
scope(getNodeManager());
7323 CVC5_API_TRY_CATCH_BEGIN
;
7324 CVC5_API_CHECK(d_smtEngine
->getOptions().smt
.produceModels
)
7325 << "Cannot get value unless model generation is enabled "
7326 "(try --produce-models)";
7327 CVC5_API_RECOVERABLE_CHECK(d_smtEngine
->isSmtModeSat())
7328 << "Can only block model after sat or unknown response.";
7329 //////// all checks before this line
7330 d_smtEngine
->blockModel();
7332 CVC5_API_TRY_CATCH_END
;
7335 void Solver::blockModelValues(const std::vector
<Term
>& terms
) const
7337 NodeManagerScope
scope(getNodeManager());
7338 CVC5_API_TRY_CATCH_BEGIN
;
7339 CVC5_API_CHECK(d_smtEngine
->getOptions().smt
.produceModels
)
7340 << "Cannot get value unless model generation is enabled "
7341 "(try --produce-models)";
7342 CVC5_API_RECOVERABLE_CHECK(d_smtEngine
->isSmtModeSat())
7343 << "Can only block model values after sat or unknown response.";
7344 CVC5_API_ARG_SIZE_CHECK_EXPECTED(!terms
.empty(), terms
)
7345 << "a non-empty set of terms";
7346 CVC5_API_SOLVER_CHECK_TERMS(terms
);
7347 //////// all checks before this line
7348 d_smtEngine
->blockModelValues(Term::termVectorToNodes(terms
));
7350 CVC5_API_TRY_CATCH_END
;
7353 void Solver::printInstantiations(std::ostream
& out
) const
7355 NodeManagerScope
scope(getNodeManager());
7356 CVC5_API_TRY_CATCH_BEGIN
;
7357 //////// all checks before this line
7358 d_smtEngine
->printInstantiations(out
);
7360 CVC5_API_TRY_CATCH_END
;
7363 void Solver::push(uint32_t nscopes
) const
7365 NodeManagerScope
scope(getNodeManager());
7366 CVC5_API_TRY_CATCH_BEGIN
;
7367 CVC5_API_CHECK(d_smtEngine
->getOptions().base
.incrementalSolving
)
7368 << "Cannot push when not solving incrementally (use --incremental)";
7369 //////// all checks before this line
7370 for (uint32_t n
= 0; n
< nscopes
; ++n
)
7372 d_smtEngine
->push();
7375 CVC5_API_TRY_CATCH_END
;
7378 void Solver::resetAssertions(void) const
7380 CVC5_API_TRY_CATCH_BEGIN
;
7381 //////// all checks before this line
7382 d_smtEngine
->resetAssertions();
7384 CVC5_API_TRY_CATCH_END
;
7387 void Solver::setInfo(const std::string
& keyword
, const std::string
& value
) const
7389 CVC5_API_TRY_CATCH_BEGIN
;
7390 CVC5_API_RECOVERABLE_ARG_CHECK_EXPECTED(
7391 keyword
== "source" || keyword
== "category" || keyword
== "difficulty"
7392 || keyword
== "filename" || keyword
== "license" || keyword
== "name"
7393 || keyword
== "notes" || keyword
== "smt-lib-version"
7394 || keyword
== "status",
7396 << "'source', 'category', 'difficulty', 'filename', 'license', 'name', "
7397 "'notes', 'smt-lib-version' or 'status'";
7398 CVC5_API_RECOVERABLE_ARG_CHECK_EXPECTED(
7399 keyword
!= "smt-lib-version" || value
== "2" || value
== "2.0"
7400 || value
== "2.5" || value
== "2.6",
7402 << "'2.0', '2.5', '2.6'";
7403 CVC5_API_ARG_CHECK_EXPECTED(keyword
!= "status" || value
== "sat"
7404 || value
== "unsat" || value
== "unknown",
7406 << "'sat', 'unsat' or 'unknown'";
7407 //////// all checks before this line
7408 d_smtEngine
->setInfo(keyword
, value
);
7410 CVC5_API_TRY_CATCH_END
;
7413 void Solver::setLogic(const std::string
& logic
) const
7415 CVC5_API_TRY_CATCH_BEGIN
;
7416 CVC5_API_CHECK(!d_smtEngine
->isFullyInited())
7417 << "Invalid call to 'setLogic', solver is already fully initialized";
7418 cvc5::LogicInfo
logic_info(logic
);
7419 //////// all checks before this line
7420 d_smtEngine
->setLogic(logic_info
);
7422 CVC5_API_TRY_CATCH_END
;
7425 void Solver::setOption(const std::string
& option
,
7426 const std::string
& value
) const
7428 CVC5_API_TRY_CATCH_BEGIN
;
7429 static constexpr auto mutableOpts
= {"diagnostic-output-channel",
7431 "regular-output-channel",
7432 "reproducible-resource-limit",
7434 if (std::find(mutableOpts
.begin(), mutableOpts
.end(), option
)
7435 == mutableOpts
.end())
7437 CVC5_API_CHECK(!d_smtEngine
->isFullyInited())
7438 << "Invalid call to 'setOption' for option '" << option
7439 << "', solver is already fully initialized";
7441 //////// all checks before this line
7442 d_smtEngine
->setOption(option
, value
);
7444 CVC5_API_TRY_CATCH_END
;
7447 Term
Solver::mkSygusVar(const Sort
& sort
, const std::string
& symbol
) const
7449 CVC5_API_TRY_CATCH_BEGIN
;
7450 CVC5_API_SOLVER_CHECK_SORT(sort
);
7451 //////// all checks before this line
7452 Node res
= getNodeManager()->mkBoundVar(symbol
, *sort
.d_type
);
7453 (void)res
.getType(true); /* kick off type checking */
7455 d_smtEngine
->declareSygusVar(res
);
7457 return Term(this, res
);
7459 CVC5_API_TRY_CATCH_END
;
7462 Grammar
Solver::mkSygusGrammar(const std::vector
<Term
>& boundVars
,
7463 const std::vector
<Term
>& ntSymbols
) const
7465 CVC5_API_TRY_CATCH_BEGIN
;
7466 CVC5_API_ARG_SIZE_CHECK_EXPECTED(!ntSymbols
.empty(), ntSymbols
)
7467 << "a non-empty vector";
7468 CVC5_API_SOLVER_CHECK_BOUND_VARS(boundVars
);
7469 CVC5_API_SOLVER_CHECK_BOUND_VARS(ntSymbols
);
7470 //////// all checks before this line
7471 return Grammar(this, boundVars
, ntSymbols
);
7473 CVC5_API_TRY_CATCH_END
;
7476 Term
Solver::synthFun(const std::string
& symbol
,
7477 const std::vector
<Term
>& boundVars
,
7478 const Sort
& sort
) const
7480 CVC5_API_TRY_CATCH_BEGIN
;
7481 CVC5_API_SOLVER_CHECK_BOUND_VARS(boundVars
);
7482 CVC5_API_SOLVER_CHECK_SORT(sort
);
7483 //////// all checks before this line
7484 return synthFunHelper(symbol
, boundVars
, sort
);
7486 CVC5_API_TRY_CATCH_END
;
7489 Term
Solver::synthFun(const std::string
& symbol
,
7490 const std::vector
<Term
>& boundVars
,
7492 Grammar
& grammar
) const
7494 CVC5_API_TRY_CATCH_BEGIN
;
7495 CVC5_API_SOLVER_CHECK_BOUND_VARS(boundVars
);
7496 CVC5_API_SOLVER_CHECK_SORT(sort
);
7497 //////// all checks before this line
7498 return synthFunHelper(symbol
, boundVars
, sort
, false, &grammar
);
7500 CVC5_API_TRY_CATCH_END
;
7503 Term
Solver::synthInv(const std::string
& symbol
,
7504 const std::vector
<Term
>& boundVars
) const
7506 CVC5_API_TRY_CATCH_BEGIN
;
7507 CVC5_API_SOLVER_CHECK_BOUND_VARS(boundVars
);
7508 //////// all checks before this line
7509 return synthFunHelper(
7510 symbol
, boundVars
, Sort(this, getNodeManager()->booleanType()), true);
7512 CVC5_API_TRY_CATCH_END
;
7515 Term
Solver::synthInv(const std::string
& symbol
,
7516 const std::vector
<Term
>& boundVars
,
7517 Grammar
& grammar
) const
7519 CVC5_API_TRY_CATCH_BEGIN
;
7520 CVC5_API_SOLVER_CHECK_BOUND_VARS(boundVars
);
7521 //////// all checks before this line
7522 return synthFunHelper(symbol
,
7524 Sort(this, getNodeManager()->booleanType()),
7528 CVC5_API_TRY_CATCH_END
;
7531 void Solver::addSygusConstraint(const Term
& term
) const
7533 NodeManagerScope
scope(getNodeManager());
7534 CVC5_API_TRY_CATCH_BEGIN
;
7535 CVC5_API_SOLVER_CHECK_TERM(term
);
7536 CVC5_API_ARG_CHECK_EXPECTED(
7537 term
.d_node
->getType() == getNodeManager()->booleanType(), term
)
7539 //////// all checks before this line
7540 d_smtEngine
->assertSygusConstraint(*term
.d_node
);
7542 CVC5_API_TRY_CATCH_END
;
7545 void Solver::addSygusInvConstraint(Term inv
,
7550 CVC5_API_TRY_CATCH_BEGIN
;
7551 CVC5_API_SOLVER_CHECK_TERM(inv
);
7552 CVC5_API_SOLVER_CHECK_TERM(pre
);
7553 CVC5_API_SOLVER_CHECK_TERM(trans
);
7554 CVC5_API_SOLVER_CHECK_TERM(post
);
7556 CVC5_API_ARG_CHECK_EXPECTED(inv
.d_node
->getType().isFunction(), inv
)
7559 TypeNode invType
= inv
.d_node
->getType();
7561 CVC5_API_ARG_CHECK_EXPECTED(invType
.getRangeType().isBoolean(), inv
)
7564 CVC5_API_CHECK(pre
.d_node
->getType() == invType
)
7565 << "Expected inv and pre to have the same sort";
7567 CVC5_API_CHECK(post
.d_node
->getType() == invType
)
7568 << "Expected inv and post to have the same sort";
7569 //////// all checks before this line
7571 const std::vector
<TypeNode
>& invArgTypes
= invType
.getArgTypes();
7573 std::vector
<TypeNode
> expectedTypes
;
7574 expectedTypes
.reserve(2 * invArgTypes
.size() + 1);
7576 for (size_t i
= 0, n
= invArgTypes
.size(); i
< 2 * n
; i
+= 2)
7578 expectedTypes
.push_back(invArgTypes
[i
% n
]);
7579 expectedTypes
.push_back(invArgTypes
[(i
+ 1) % n
]);
7582 expectedTypes
.push_back(invType
.getRangeType());
7583 TypeNode expectedTransType
= getNodeManager()->mkFunctionType(expectedTypes
);
7585 CVC5_API_CHECK(trans
.d_node
->getType() == expectedTransType
)
7586 << "Expected trans's sort to be " << invType
;
7588 d_smtEngine
->assertSygusInvConstraint(
7589 *inv
.d_node
, *pre
.d_node
, *trans
.d_node
, *post
.d_node
);
7591 CVC5_API_TRY_CATCH_END
;
7594 Result
Solver::checkSynth() const
7596 CVC5_API_TRY_CATCH_BEGIN
;
7597 //////// all checks before this line
7598 return d_smtEngine
->checkSynth();
7600 CVC5_API_TRY_CATCH_END
;
7603 Term
Solver::getSynthSolution(Term term
) const
7605 CVC5_API_TRY_CATCH_BEGIN
;
7606 CVC5_API_SOLVER_CHECK_TERM(term
);
7608 std::map
<cvc5::Node
, cvc5::Node
> map
;
7609 CVC5_API_CHECK(d_smtEngine
->getSynthSolutions(map
))
7610 << "The solver is not in a state immediately preceded by a "
7611 "successful call to checkSynth";
7613 std::map
<cvc5::Node
, cvc5::Node
>::const_iterator it
= map
.find(*term
.d_node
);
7615 CVC5_API_CHECK(it
!= map
.cend()) << "Synth solution not found for given term";
7616 //////// all checks before this line
7617 return Term(this, it
->second
);
7619 CVC5_API_TRY_CATCH_END
;
7622 std::vector
<Term
> Solver::getSynthSolutions(
7623 const std::vector
<Term
>& terms
) const
7625 CVC5_API_TRY_CATCH_BEGIN
;
7626 CVC5_API_ARG_SIZE_CHECK_EXPECTED(!terms
.empty(), terms
) << "non-empty vector";
7627 CVC5_API_SOLVER_CHECK_TERMS(terms
);
7629 std::map
<cvc5::Node
, cvc5::Node
> map
;
7630 CVC5_API_CHECK(d_smtEngine
->getSynthSolutions(map
))
7631 << "The solver is not in a state immediately preceded by a "
7632 "successful call to checkSynth";
7633 //////// all checks before this line
7635 std::vector
<Term
> synthSolution
;
7636 synthSolution
.reserve(terms
.size());
7638 for (size_t i
= 0, n
= terms
.size(); i
< n
; ++i
)
7640 std::map
<cvc5::Node
, cvc5::Node
>::const_iterator it
=
7641 map
.find(*terms
[i
].d_node
);
7643 CVC5_API_CHECK(it
!= map
.cend())
7644 << "Synth solution not found for term at index " << i
;
7646 synthSolution
.push_back(Term(this, it
->second
));
7649 return synthSolution
;
7651 CVC5_API_TRY_CATCH_END
;
7655 * !!! This is only temporarily available until the parser is fully migrated to
7658 SmtEngine
* Solver::getSmtEngine(void) const { return d_smtEngine
.get(); }
7661 * !!! This is only temporarily available until the parser is fully migrated to
7664 Options
& Solver::getOptions(void) { return d_smtEngine
->getOptions(); }
7666 Statistics
Solver::getStatistics() const
7668 return Statistics(d_smtEngine
->getStatisticsRegistry());
7677 size_t hash
<cvc5::api::Kind
>::operator()(cvc5::api::Kind k
) const
7679 return static_cast<size_t>(k
);
7682 size_t hash
<cvc5::api::Op
>::operator()(const cvc5::api::Op
& t
) const
7684 if (t
.isIndexedHelper())
7686 return std::hash
<cvc5::Node
>()(*t
.d_node
);
7690 return std::hash
<cvc5::api::Kind
>()(t
.d_kind
);
7694 size_t std::hash
<cvc5::api::RoundingMode
>::operator()(
7695 cvc5::api::RoundingMode rm
) const
7697 return static_cast<size_t>(rm
);
7700 size_t std::hash
<cvc5::api::Sort
>::operator()(const cvc5::api::Sort
& s
) const
7702 return std::hash
<cvc5::TypeNode
>()(*s
.d_type
);
7705 size_t std::hash
<cvc5::api::Term
>::operator()(const cvc5::api::Term
& t
) const
7707 return std::hash
<cvc5::Node
>()(*t
.d_node
);