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::mkRealOrIntegerFromStrHelper for 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/cardinality_constraint.h"
45 #include "expr/dtype.h"
46 #include "expr/dtype_cons.h"
47 #include "expr/dtype_selector.h"
48 #include "expr/emptybag.h"
49 #include "expr/emptyset.h"
50 #include "expr/kind.h"
51 #include "expr/metakind.h"
52 #include "expr/node.h"
53 #include "expr/node_algorithm.h"
54 #include "expr/node_builder.h"
55 #include "expr/node_manager.h"
56 #include "expr/node_manager_attributes.h"
57 #include "expr/sequence.h"
58 #include "expr/type_node.h"
59 #include "expr/uninterpreted_constant.h"
60 #include "options/base_options.h"
61 #include "options/main_options.h"
62 #include "options/option_exception.h"
63 #include "options/options.h"
64 #include "options/options_public.h"
65 #include "options/smt_options.h"
66 #include "proof/unsat_core.h"
68 #include "smt/model.h"
69 #include "smt/smt_mode.h"
70 #include "smt/solver_engine.h"
71 #include "theory/datatypes/tuple_project_op.h"
72 #include "theory/logic_info.h"
73 #include "theory/theory_model.h"
74 #include "util/abstract_value.h"
75 #include "util/bitvector.h"
76 #include "util/divisible.h"
77 #include "util/floatingpoint.h"
78 #include "util/iand.h"
79 #include "util/random.h"
80 #include "util/regexp.h"
81 #include "util/result.h"
82 #include "util/roundingmode.h"
83 #include "util/statistics_registry.h"
84 #include "util/statistics_stats.h"
85 #include "util/statistics_value.h"
86 #include "util/string.h"
87 #include "util/utility.h"
92 /* -------------------------------------------------------------------------- */
94 /* -------------------------------------------------------------------------- */
98 HistogramStat
<TypeConstant
> d_consts
;
99 HistogramStat
<TypeConstant
> d_vars
;
100 HistogramStat
<Kind
> d_terms
;
103 /* -------------------------------------------------------------------------- */
105 /* -------------------------------------------------------------------------- */
107 /* Mapping from external (API) kind to internal kind. */
108 const static std::unordered_map
<Kind
, cvc5::Kind
> s_kinds
{
109 {INTERNAL_KIND
, cvc5::Kind::UNDEFINED_KIND
},
110 {UNDEFINED_KIND
, cvc5::Kind::UNDEFINED_KIND
},
111 {NULL_EXPR
, cvc5::Kind::NULL_EXPR
},
112 /* Builtin ------------------------------------------------------------- */
113 {UNINTERPRETED_CONSTANT
, cvc5::Kind::UNINTERPRETED_CONSTANT
},
114 {ABSTRACT_VALUE
, cvc5::Kind::ABSTRACT_VALUE
},
115 {EQUAL
, cvc5::Kind::EQUAL
},
116 {DISTINCT
, cvc5::Kind::DISTINCT
},
117 {CONSTANT
, cvc5::Kind::VARIABLE
},
118 {VARIABLE
, cvc5::Kind::BOUND_VARIABLE
},
119 {SEXPR
, cvc5::Kind::SEXPR
},
120 {LAMBDA
, cvc5::Kind::LAMBDA
},
121 {WITNESS
, cvc5::Kind::WITNESS
},
122 /* Boolean ------------------------------------------------------------- */
123 {CONST_BOOLEAN
, cvc5::Kind::CONST_BOOLEAN
},
124 {NOT
, cvc5::Kind::NOT
},
125 {AND
, cvc5::Kind::AND
},
126 {IMPLIES
, cvc5::Kind::IMPLIES
},
127 {OR
, cvc5::Kind::OR
},
128 {XOR
, cvc5::Kind::XOR
},
129 {ITE
, cvc5::Kind::ITE
},
130 /* UF ------------------------------------------------------------------ */
131 {APPLY_UF
, cvc5::Kind::APPLY_UF
},
132 {CARDINALITY_CONSTRAINT
, cvc5::Kind::CARDINALITY_CONSTRAINT
},
133 {HO_APPLY
, cvc5::Kind::HO_APPLY
},
134 /* Arithmetic ---------------------------------------------------------- */
135 {PLUS
, cvc5::Kind::PLUS
},
136 {MULT
, cvc5::Kind::MULT
},
137 {IAND
, cvc5::Kind::IAND
},
138 {POW2
, cvc5::Kind::POW2
},
139 {MINUS
, cvc5::Kind::MINUS
},
140 {UMINUS
, cvc5::Kind::UMINUS
},
141 {DIVISION
, cvc5::Kind::DIVISION
},
142 {INTS_DIVISION
, cvc5::Kind::INTS_DIVISION
},
143 {INTS_MODULUS
, cvc5::Kind::INTS_MODULUS
},
144 {ABS
, cvc5::Kind::ABS
},
145 {DIVISIBLE
, cvc5::Kind::DIVISIBLE
},
146 {POW
, cvc5::Kind::POW
},
147 {EXPONENTIAL
, cvc5::Kind::EXPONENTIAL
},
148 {SINE
, cvc5::Kind::SINE
},
149 {COSINE
, cvc5::Kind::COSINE
},
150 {TANGENT
, cvc5::Kind::TANGENT
},
151 {COSECANT
, cvc5::Kind::COSECANT
},
152 {SECANT
, cvc5::Kind::SECANT
},
153 {COTANGENT
, cvc5::Kind::COTANGENT
},
154 {ARCSINE
, cvc5::Kind::ARCSINE
},
155 {ARCCOSINE
, cvc5::Kind::ARCCOSINE
},
156 {ARCTANGENT
, cvc5::Kind::ARCTANGENT
},
157 {ARCCOSECANT
, cvc5::Kind::ARCCOSECANT
},
158 {ARCSECANT
, cvc5::Kind::ARCSECANT
},
159 {ARCCOTANGENT
, cvc5::Kind::ARCCOTANGENT
},
160 {SQRT
, cvc5::Kind::SQRT
},
161 {CONST_RATIONAL
, cvc5::Kind::CONST_RATIONAL
},
162 {LT
, cvc5::Kind::LT
},
163 {LEQ
, cvc5::Kind::LEQ
},
164 {GT
, cvc5::Kind::GT
},
165 {GEQ
, cvc5::Kind::GEQ
},
166 {IS_INTEGER
, cvc5::Kind::IS_INTEGER
},
167 {TO_INTEGER
, cvc5::Kind::TO_INTEGER
},
168 {TO_REAL
, cvc5::Kind::TO_REAL
},
169 {PI
, cvc5::Kind::PI
},
170 /* BV ------------------------------------------------------------------ */
171 {CONST_BITVECTOR
, cvc5::Kind::CONST_BITVECTOR
},
172 {BITVECTOR_CONCAT
, cvc5::Kind::BITVECTOR_CONCAT
},
173 {BITVECTOR_AND
, cvc5::Kind::BITVECTOR_AND
},
174 {BITVECTOR_OR
, cvc5::Kind::BITVECTOR_OR
},
175 {BITVECTOR_XOR
, cvc5::Kind::BITVECTOR_XOR
},
176 {BITVECTOR_NOT
, cvc5::Kind::BITVECTOR_NOT
},
177 {BITVECTOR_NAND
, cvc5::Kind::BITVECTOR_NAND
},
178 {BITVECTOR_NOR
, cvc5::Kind::BITVECTOR_NOR
},
179 {BITVECTOR_XNOR
, cvc5::Kind::BITVECTOR_XNOR
},
180 {BITVECTOR_COMP
, cvc5::Kind::BITVECTOR_COMP
},
181 {BITVECTOR_MULT
, cvc5::Kind::BITVECTOR_MULT
},
182 {BITVECTOR_ADD
, cvc5::Kind::BITVECTOR_ADD
},
183 {BITVECTOR_SUB
, cvc5::Kind::BITVECTOR_SUB
},
184 {BITVECTOR_NEG
, cvc5::Kind::BITVECTOR_NEG
},
185 {BITVECTOR_UDIV
, cvc5::Kind::BITVECTOR_UDIV
},
186 {BITVECTOR_UREM
, cvc5::Kind::BITVECTOR_UREM
},
187 {BITVECTOR_SDIV
, cvc5::Kind::BITVECTOR_SDIV
},
188 {BITVECTOR_SREM
, cvc5::Kind::BITVECTOR_SREM
},
189 {BITVECTOR_SMOD
, cvc5::Kind::BITVECTOR_SMOD
},
190 {BITVECTOR_SHL
, cvc5::Kind::BITVECTOR_SHL
},
191 {BITVECTOR_LSHR
, cvc5::Kind::BITVECTOR_LSHR
},
192 {BITVECTOR_ASHR
, cvc5::Kind::BITVECTOR_ASHR
},
193 {BITVECTOR_ULT
, cvc5::Kind::BITVECTOR_ULT
},
194 {BITVECTOR_ULE
, cvc5::Kind::BITVECTOR_ULE
},
195 {BITVECTOR_UGT
, cvc5::Kind::BITVECTOR_UGT
},
196 {BITVECTOR_UGE
, cvc5::Kind::BITVECTOR_UGE
},
197 {BITVECTOR_SLT
, cvc5::Kind::BITVECTOR_SLT
},
198 {BITVECTOR_SLE
, cvc5::Kind::BITVECTOR_SLE
},
199 {BITVECTOR_SGT
, cvc5::Kind::BITVECTOR_SGT
},
200 {BITVECTOR_SGE
, cvc5::Kind::BITVECTOR_SGE
},
201 {BITVECTOR_ULTBV
, cvc5::Kind::BITVECTOR_ULTBV
},
202 {BITVECTOR_SLTBV
, cvc5::Kind::BITVECTOR_SLTBV
},
203 {BITVECTOR_ITE
, cvc5::Kind::BITVECTOR_ITE
},
204 {BITVECTOR_REDOR
, cvc5::Kind::BITVECTOR_REDOR
},
205 {BITVECTOR_REDAND
, cvc5::Kind::BITVECTOR_REDAND
},
206 {BITVECTOR_EXTRACT
, cvc5::Kind::BITVECTOR_EXTRACT
},
207 {BITVECTOR_REPEAT
, cvc5::Kind::BITVECTOR_REPEAT
},
208 {BITVECTOR_ZERO_EXTEND
, cvc5::Kind::BITVECTOR_ZERO_EXTEND
},
209 {BITVECTOR_SIGN_EXTEND
, cvc5::Kind::BITVECTOR_SIGN_EXTEND
},
210 {BITVECTOR_ROTATE_LEFT
, cvc5::Kind::BITVECTOR_ROTATE_LEFT
},
211 {BITVECTOR_ROTATE_RIGHT
, cvc5::Kind::BITVECTOR_ROTATE_RIGHT
},
212 {INT_TO_BITVECTOR
, cvc5::Kind::INT_TO_BITVECTOR
},
213 {BITVECTOR_TO_NAT
, cvc5::Kind::BITVECTOR_TO_NAT
},
214 /* FP ------------------------------------------------------------------ */
215 {CONST_FLOATINGPOINT
, cvc5::Kind::CONST_FLOATINGPOINT
},
216 {CONST_ROUNDINGMODE
, cvc5::Kind::CONST_ROUNDINGMODE
},
217 {FLOATINGPOINT_FP
, cvc5::Kind::FLOATINGPOINT_FP
},
218 {FLOATINGPOINT_EQ
, cvc5::Kind::FLOATINGPOINT_EQ
},
219 {FLOATINGPOINT_ABS
, cvc5::Kind::FLOATINGPOINT_ABS
},
220 {FLOATINGPOINT_NEG
, cvc5::Kind::FLOATINGPOINT_NEG
},
221 {FLOATINGPOINT_ADD
, cvc5::Kind::FLOATINGPOINT_ADD
},
222 {FLOATINGPOINT_SUB
, cvc5::Kind::FLOATINGPOINT_SUB
},
223 {FLOATINGPOINT_MULT
, cvc5::Kind::FLOATINGPOINT_MULT
},
224 {FLOATINGPOINT_DIV
, cvc5::Kind::FLOATINGPOINT_DIV
},
225 {FLOATINGPOINT_FMA
, cvc5::Kind::FLOATINGPOINT_FMA
},
226 {FLOATINGPOINT_SQRT
, cvc5::Kind::FLOATINGPOINT_SQRT
},
227 {FLOATINGPOINT_REM
, cvc5::Kind::FLOATINGPOINT_REM
},
228 {FLOATINGPOINT_RTI
, cvc5::Kind::FLOATINGPOINT_RTI
},
229 {FLOATINGPOINT_MIN
, cvc5::Kind::FLOATINGPOINT_MIN
},
230 {FLOATINGPOINT_MAX
, cvc5::Kind::FLOATINGPOINT_MAX
},
231 {FLOATINGPOINT_LEQ
, cvc5::Kind::FLOATINGPOINT_LEQ
},
232 {FLOATINGPOINT_LT
, cvc5::Kind::FLOATINGPOINT_LT
},
233 {FLOATINGPOINT_GEQ
, cvc5::Kind::FLOATINGPOINT_GEQ
},
234 {FLOATINGPOINT_GT
, cvc5::Kind::FLOATINGPOINT_GT
},
235 {FLOATINGPOINT_ISN
, cvc5::Kind::FLOATINGPOINT_ISN
},
236 {FLOATINGPOINT_ISSN
, cvc5::Kind::FLOATINGPOINT_ISSN
},
237 {FLOATINGPOINT_ISZ
, cvc5::Kind::FLOATINGPOINT_ISZ
},
238 {FLOATINGPOINT_ISINF
, cvc5::Kind::FLOATINGPOINT_ISINF
},
239 {FLOATINGPOINT_ISNAN
, cvc5::Kind::FLOATINGPOINT_ISNAN
},
240 {FLOATINGPOINT_ISNEG
, cvc5::Kind::FLOATINGPOINT_ISNEG
},
241 {FLOATINGPOINT_ISPOS
, cvc5::Kind::FLOATINGPOINT_ISPOS
},
242 {FLOATINGPOINT_TO_FP_FLOATINGPOINT
,
243 cvc5::Kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT
},
244 {FLOATINGPOINT_TO_FP_IEEE_BITVECTOR
,
245 cvc5::Kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR
},
246 {FLOATINGPOINT_TO_FP_REAL
, cvc5::Kind::FLOATINGPOINT_TO_FP_REAL
},
247 {FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR
,
248 cvc5::Kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR
},
249 {FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR
,
250 cvc5::Kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR
},
251 {FLOATINGPOINT_TO_FP_GENERIC
, cvc5::Kind::FLOATINGPOINT_TO_FP_GENERIC
},
252 {FLOATINGPOINT_TO_UBV
, cvc5::Kind::FLOATINGPOINT_TO_UBV
},
253 {FLOATINGPOINT_TO_SBV
, cvc5::Kind::FLOATINGPOINT_TO_SBV
},
254 {FLOATINGPOINT_TO_REAL
, cvc5::Kind::FLOATINGPOINT_TO_REAL
},
255 /* Arrays -------------------------------------------------------------- */
256 {SELECT
, cvc5::Kind::SELECT
},
257 {STORE
, cvc5::Kind::STORE
},
258 {CONST_ARRAY
, cvc5::Kind::STORE_ALL
},
259 {EQ_RANGE
, cvc5::Kind::EQ_RANGE
},
260 /* Datatypes ----------------------------------------------------------- */
261 {APPLY_SELECTOR
, cvc5::Kind::APPLY_SELECTOR
},
262 {APPLY_CONSTRUCTOR
, cvc5::Kind::APPLY_CONSTRUCTOR
},
263 {APPLY_TESTER
, cvc5::Kind::APPLY_TESTER
},
264 {APPLY_UPDATER
, cvc5::Kind::APPLY_UPDATER
},
265 {DT_SIZE
, cvc5::Kind::DT_SIZE
},
266 {MATCH
, cvc5::Kind::MATCH
},
267 {MATCH_CASE
, cvc5::Kind::MATCH_CASE
},
268 {MATCH_BIND_CASE
, cvc5::Kind::MATCH_BIND_CASE
},
269 {TUPLE_PROJECT
, cvc5::Kind::TUPLE_PROJECT
},
270 /* Separation Logic ---------------------------------------------------- */
271 {SEP_NIL
, cvc5::Kind::SEP_NIL
},
272 {SEP_EMP
, cvc5::Kind::SEP_EMP
},
273 {SEP_PTO
, cvc5::Kind::SEP_PTO
},
274 {SEP_STAR
, cvc5::Kind::SEP_STAR
},
275 {SEP_WAND
, cvc5::Kind::SEP_WAND
},
276 /* Sets ---------------------------------------------------------------- */
277 {SET_EMPTY
, cvc5::Kind::SET_EMPTY
},
278 {SET_UNION
, cvc5::Kind::SET_UNION
},
279 {SET_INTER
, cvc5::Kind::SET_INTER
},
280 {SET_MINUS
, cvc5::Kind::SET_MINUS
},
281 {SET_SUBSET
, cvc5::Kind::SET_SUBSET
},
282 {SET_MEMBER
, cvc5::Kind::SET_MEMBER
},
283 {SET_SINGLETON
, cvc5::Kind::SET_SINGLETON
},
284 {SET_INSERT
, cvc5::Kind::SET_INSERT
},
285 {SET_CARD
, cvc5::Kind::SET_CARD
},
286 {SET_COMPLEMENT
, cvc5::Kind::SET_COMPLEMENT
},
287 {SET_UNIVERSE
, cvc5::Kind::SET_UNIVERSE
},
288 {SET_COMPREHENSION
, cvc5::Kind::SET_COMPREHENSION
},
289 {SET_CHOOSE
, cvc5::Kind::SET_CHOOSE
},
290 {SET_IS_SINGLETON
, cvc5::Kind::SET_IS_SINGLETON
},
291 {SET_MAP
, cvc5::Kind::SET_MAP
},
292 /* Relations ----------------------------------------------------------- */
293 {RELATION_JOIN
, cvc5::Kind::RELATION_JOIN
},
294 {RELATION_PRODUCT
, cvc5::Kind::RELATION_PRODUCT
},
295 {RELATION_TRANSPOSE
, cvc5::Kind::RELATION_TRANSPOSE
},
296 {RELATION_TCLOSURE
, cvc5::Kind::RELATION_TCLOSURE
},
297 {RELATION_JOIN_IMAGE
, cvc5::Kind::RELATION_JOIN_IMAGE
},
298 {RELATION_IDEN
, cvc5::Kind::RELATION_IDEN
},
299 /* Bags ---------------------------------------------------------------- */
300 {BAG_UNION_MAX
, cvc5::Kind::BAG_UNION_MAX
},
301 {BAG_UNION_DISJOINT
, cvc5::Kind::BAG_UNION_DISJOINT
},
302 {BAG_INTER_MIN
, cvc5::Kind::BAG_INTER_MIN
},
303 {BAG_DIFFERENCE_SUBTRACT
, cvc5::Kind::BAG_DIFFERENCE_SUBTRACT
},
304 {BAG_DIFFERENCE_REMOVE
, cvc5::Kind::BAG_DIFFERENCE_REMOVE
},
305 {BAG_SUBBAG
, cvc5::Kind::BAG_SUBBAG
},
306 {BAG_COUNT
, cvc5::Kind::BAG_COUNT
},
307 {BAG_DUPLICATE_REMOVAL
, cvc5::Kind::BAG_DUPLICATE_REMOVAL
},
308 {BAG_MAKE
, cvc5::Kind::BAG_MAKE
},
309 {BAG_EMPTY
, cvc5::Kind::BAG_EMPTY
},
310 {BAG_CARD
, cvc5::Kind::BAG_CARD
},
311 {BAG_CHOOSE
, cvc5::Kind::BAG_CHOOSE
},
312 {BAG_IS_SINGLETON
, cvc5::Kind::BAG_IS_SINGLETON
},
313 {BAG_FROM_SET
, cvc5::Kind::BAG_FROM_SET
},
314 {BAG_TO_SET
, cvc5::Kind::BAG_TO_SET
},
315 {BAG_MAP
, cvc5::Kind::BAG_MAP
},
316 {BAG_FOLD
, cvc5::Kind::BAG_FOLD
},
317 /* Strings ------------------------------------------------------------- */
318 {STRING_CONCAT
, cvc5::Kind::STRING_CONCAT
},
319 {STRING_IN_REGEXP
, cvc5::Kind::STRING_IN_REGEXP
},
320 {STRING_LENGTH
, cvc5::Kind::STRING_LENGTH
},
321 {STRING_SUBSTR
, cvc5::Kind::STRING_SUBSTR
},
322 {STRING_UPDATE
, cvc5::Kind::STRING_UPDATE
},
323 {STRING_CHARAT
, cvc5::Kind::STRING_CHARAT
},
324 {STRING_CONTAINS
, cvc5::Kind::STRING_CONTAINS
},
325 {STRING_INDEXOF
, cvc5::Kind::STRING_INDEXOF
},
326 {STRING_INDEXOF_RE
, cvc5::Kind::STRING_INDEXOF_RE
},
327 {STRING_REPLACE
, cvc5::Kind::STRING_REPLACE
},
328 {STRING_REPLACE_ALL
, cvc5::Kind::STRING_REPLACE_ALL
},
329 {STRING_REPLACE_RE
, cvc5::Kind::STRING_REPLACE_RE
},
330 {STRING_REPLACE_RE_ALL
, cvc5::Kind::STRING_REPLACE_RE_ALL
},
331 {STRING_TOLOWER
, cvc5::Kind::STRING_TOLOWER
},
332 {STRING_TOUPPER
, cvc5::Kind::STRING_TOUPPER
},
333 {STRING_REV
, cvc5::Kind::STRING_REV
},
334 {STRING_FROM_CODE
, cvc5::Kind::STRING_FROM_CODE
},
335 {STRING_TO_CODE
, cvc5::Kind::STRING_TO_CODE
},
336 {STRING_LT
, cvc5::Kind::STRING_LT
},
337 {STRING_LEQ
, cvc5::Kind::STRING_LEQ
},
338 {STRING_PREFIX
, cvc5::Kind::STRING_PREFIX
},
339 {STRING_SUFFIX
, cvc5::Kind::STRING_SUFFIX
},
340 {STRING_IS_DIGIT
, cvc5::Kind::STRING_IS_DIGIT
},
341 {STRING_FROM_INT
, cvc5::Kind::STRING_ITOS
},
342 {STRING_TO_INT
, cvc5::Kind::STRING_STOI
},
343 {CONST_STRING
, cvc5::Kind::CONST_STRING
},
344 {STRING_TO_REGEXP
, cvc5::Kind::STRING_TO_REGEXP
},
345 {REGEXP_CONCAT
, cvc5::Kind::REGEXP_CONCAT
},
346 {REGEXP_UNION
, cvc5::Kind::REGEXP_UNION
},
347 {REGEXP_INTER
, cvc5::Kind::REGEXP_INTER
},
348 {REGEXP_DIFF
, cvc5::Kind::REGEXP_DIFF
},
349 {REGEXP_STAR
, cvc5::Kind::REGEXP_STAR
},
350 {REGEXP_PLUS
, cvc5::Kind::REGEXP_PLUS
},
351 {REGEXP_OPT
, cvc5::Kind::REGEXP_OPT
},
352 {REGEXP_RANGE
, cvc5::Kind::REGEXP_RANGE
},
353 {REGEXP_REPEAT
, cvc5::Kind::REGEXP_REPEAT
},
354 {REGEXP_LOOP
, cvc5::Kind::REGEXP_LOOP
},
355 {REGEXP_NONE
, cvc5::Kind::REGEXP_NONE
},
356 {REGEXP_ALLCHAR
, cvc5::Kind::REGEXP_ALLCHAR
},
357 {REGEXP_COMPLEMENT
, cvc5::Kind::REGEXP_COMPLEMENT
},
358 // maps to the same kind as the string versions
359 {SEQ_CONCAT
, cvc5::Kind::STRING_CONCAT
},
360 {SEQ_LENGTH
, cvc5::Kind::STRING_LENGTH
},
361 {SEQ_EXTRACT
, cvc5::Kind::STRING_SUBSTR
},
362 {SEQ_UPDATE
, cvc5::Kind::STRING_UPDATE
},
363 {SEQ_AT
, cvc5::Kind::STRING_CHARAT
},
364 {SEQ_CONTAINS
, cvc5::Kind::STRING_CONTAINS
},
365 {SEQ_INDEXOF
, cvc5::Kind::STRING_INDEXOF
},
366 {SEQ_REPLACE
, cvc5::Kind::STRING_REPLACE
},
367 {SEQ_REPLACE_ALL
, cvc5::Kind::STRING_REPLACE_ALL
},
368 {SEQ_REV
, cvc5::Kind::STRING_REV
},
369 {SEQ_PREFIX
, cvc5::Kind::STRING_PREFIX
},
370 {SEQ_SUFFIX
, cvc5::Kind::STRING_SUFFIX
},
371 {CONST_SEQUENCE
, cvc5::Kind::CONST_SEQUENCE
},
372 {SEQ_UNIT
, cvc5::Kind::SEQ_UNIT
},
373 {SEQ_NTH
, cvc5::Kind::SEQ_NTH
},
374 /* Quantifiers --------------------------------------------------------- */
375 {FORALL
, cvc5::Kind::FORALL
},
376 {EXISTS
, cvc5::Kind::EXISTS
},
377 {VARIABLE_LIST
, cvc5::Kind::BOUND_VAR_LIST
},
378 {INST_PATTERN
, cvc5::Kind::INST_PATTERN
},
379 {INST_NO_PATTERN
, cvc5::Kind::INST_NO_PATTERN
},
380 {INST_POOL
, cvc5::Kind::INST_POOL
},
381 {INST_ADD_TO_POOL
, cvc5::Kind::INST_ADD_TO_POOL
},
382 {SKOLEM_ADD_TO_POOL
, cvc5::Kind::SKOLEM_ADD_TO_POOL
},
383 {INST_ATTRIBUTE
, cvc5::Kind::INST_ATTRIBUTE
},
384 {INST_PATTERN_LIST
, cvc5::Kind::INST_PATTERN_LIST
},
385 {LAST_KIND
, cvc5::Kind::LAST_KIND
},
388 /* Mapping from internal kind to external (API) kind. */
389 const static std::unordered_map
<cvc5::Kind
, Kind
, cvc5::kind::KindHashFunction
>
391 {cvc5::Kind::UNDEFINED_KIND
, UNDEFINED_KIND
},
392 {cvc5::Kind::NULL_EXPR
, NULL_EXPR
},
393 /* Builtin --------------------------------------------------------- */
394 {cvc5::Kind::UNINTERPRETED_CONSTANT
, UNINTERPRETED_CONSTANT
},
395 {cvc5::Kind::ABSTRACT_VALUE
, ABSTRACT_VALUE
},
396 {cvc5::Kind::EQUAL
, EQUAL
},
397 {cvc5::Kind::DISTINCT
, DISTINCT
},
398 {cvc5::Kind::VARIABLE
, CONSTANT
},
399 {cvc5::Kind::BOUND_VARIABLE
, VARIABLE
},
400 {cvc5::Kind::SEXPR
, SEXPR
},
401 {cvc5::Kind::LAMBDA
, LAMBDA
},
402 {cvc5::Kind::WITNESS
, WITNESS
},
403 /* Boolean --------------------------------------------------------- */
404 {cvc5::Kind::CONST_BOOLEAN
, CONST_BOOLEAN
},
405 {cvc5::Kind::NOT
, NOT
},
406 {cvc5::Kind::AND
, AND
},
407 {cvc5::Kind::IMPLIES
, IMPLIES
},
408 {cvc5::Kind::OR
, OR
},
409 {cvc5::Kind::XOR
, XOR
},
410 {cvc5::Kind::ITE
, ITE
},
411 /* UF -------------------------------------------------------------- */
412 {cvc5::Kind::APPLY_UF
, APPLY_UF
},
413 {cvc5::Kind::CARDINALITY_CONSTRAINT
, CARDINALITY_CONSTRAINT
},
414 {cvc5::Kind::HO_APPLY
, HO_APPLY
},
415 /* Arithmetic ------------------------------------------------------ */
416 {cvc5::Kind::PLUS
, PLUS
},
417 {cvc5::Kind::MULT
, MULT
},
418 {cvc5::Kind::IAND
, IAND
},
419 {cvc5::Kind::POW2
, POW2
},
420 {cvc5::Kind::MINUS
, MINUS
},
421 {cvc5::Kind::UMINUS
, UMINUS
},
422 {cvc5::Kind::DIVISION
, DIVISION
},
423 {cvc5::Kind::DIVISION_TOTAL
, INTERNAL_KIND
},
424 {cvc5::Kind::INTS_DIVISION
, INTS_DIVISION
},
425 {cvc5::Kind::INTS_DIVISION_TOTAL
, INTERNAL_KIND
},
426 {cvc5::Kind::INTS_MODULUS
, INTS_MODULUS
},
427 {cvc5::Kind::INTS_MODULUS_TOTAL
, INTERNAL_KIND
},
428 {cvc5::Kind::ABS
, ABS
},
429 {cvc5::Kind::DIVISIBLE
, DIVISIBLE
},
430 {cvc5::Kind::POW
, POW
},
431 {cvc5::Kind::EXPONENTIAL
, EXPONENTIAL
},
432 {cvc5::Kind::SINE
, SINE
},
433 {cvc5::Kind::COSINE
, COSINE
},
434 {cvc5::Kind::TANGENT
, TANGENT
},
435 {cvc5::Kind::COSECANT
, COSECANT
},
436 {cvc5::Kind::SECANT
, SECANT
},
437 {cvc5::Kind::COTANGENT
, COTANGENT
},
438 {cvc5::Kind::ARCSINE
, ARCSINE
},
439 {cvc5::Kind::ARCCOSINE
, ARCCOSINE
},
440 {cvc5::Kind::ARCTANGENT
, ARCTANGENT
},
441 {cvc5::Kind::ARCCOSECANT
, ARCCOSECANT
},
442 {cvc5::Kind::ARCSECANT
, ARCSECANT
},
443 {cvc5::Kind::ARCCOTANGENT
, ARCCOTANGENT
},
444 {cvc5::Kind::SQRT
, SQRT
},
445 {cvc5::Kind::DIVISIBLE_OP
, DIVISIBLE
},
446 {cvc5::Kind::CONST_RATIONAL
, CONST_RATIONAL
},
447 {cvc5::Kind::LT
, LT
},
448 {cvc5::Kind::LEQ
, LEQ
},
449 {cvc5::Kind::GT
, GT
},
450 {cvc5::Kind::GEQ
, GEQ
},
451 {cvc5::Kind::IS_INTEGER
, IS_INTEGER
},
452 {cvc5::Kind::TO_INTEGER
, TO_INTEGER
},
453 {cvc5::Kind::TO_REAL
, TO_REAL
},
454 {cvc5::Kind::PI
, PI
},
455 {cvc5::Kind::IAND_OP
, IAND
},
456 /* BV -------------------------------------------------------------- */
457 {cvc5::Kind::CONST_BITVECTOR
, CONST_BITVECTOR
},
458 {cvc5::Kind::BITVECTOR_CONCAT
, BITVECTOR_CONCAT
},
459 {cvc5::Kind::BITVECTOR_AND
, BITVECTOR_AND
},
460 {cvc5::Kind::BITVECTOR_OR
, BITVECTOR_OR
},
461 {cvc5::Kind::BITVECTOR_XOR
, BITVECTOR_XOR
},
462 {cvc5::Kind::BITVECTOR_NOT
, BITVECTOR_NOT
},
463 {cvc5::Kind::BITVECTOR_NAND
, BITVECTOR_NAND
},
464 {cvc5::Kind::BITVECTOR_NOR
, BITVECTOR_NOR
},
465 {cvc5::Kind::BITVECTOR_XNOR
, BITVECTOR_XNOR
},
466 {cvc5::Kind::BITVECTOR_COMP
, BITVECTOR_COMP
},
467 {cvc5::Kind::BITVECTOR_MULT
, BITVECTOR_MULT
},
468 {cvc5::Kind::BITVECTOR_ADD
, BITVECTOR_ADD
},
469 {cvc5::Kind::BITVECTOR_SUB
, BITVECTOR_SUB
},
470 {cvc5::Kind::BITVECTOR_NEG
, BITVECTOR_NEG
},
471 {cvc5::Kind::BITVECTOR_UDIV
, BITVECTOR_UDIV
},
472 {cvc5::Kind::BITVECTOR_UREM
, BITVECTOR_UREM
},
473 {cvc5::Kind::BITVECTOR_SDIV
, BITVECTOR_SDIV
},
474 {cvc5::Kind::BITVECTOR_SREM
, BITVECTOR_SREM
},
475 {cvc5::Kind::BITVECTOR_SMOD
, BITVECTOR_SMOD
},
476 {cvc5::Kind::BITVECTOR_SHL
, BITVECTOR_SHL
},
477 {cvc5::Kind::BITVECTOR_LSHR
, BITVECTOR_LSHR
},
478 {cvc5::Kind::BITVECTOR_ASHR
, BITVECTOR_ASHR
},
479 {cvc5::Kind::BITVECTOR_ULT
, BITVECTOR_ULT
},
480 {cvc5::Kind::BITVECTOR_ULE
, BITVECTOR_ULE
},
481 {cvc5::Kind::BITVECTOR_UGT
, BITVECTOR_UGT
},
482 {cvc5::Kind::BITVECTOR_UGE
, BITVECTOR_UGE
},
483 {cvc5::Kind::BITVECTOR_SLT
, BITVECTOR_SLT
},
484 {cvc5::Kind::BITVECTOR_SLE
, BITVECTOR_SLE
},
485 {cvc5::Kind::BITVECTOR_SGT
, BITVECTOR_SGT
},
486 {cvc5::Kind::BITVECTOR_SGE
, BITVECTOR_SGE
},
487 {cvc5::Kind::BITVECTOR_ULTBV
, BITVECTOR_ULTBV
},
488 {cvc5::Kind::BITVECTOR_SLTBV
, BITVECTOR_SLTBV
},
489 {cvc5::Kind::BITVECTOR_ITE
, BITVECTOR_ITE
},
490 {cvc5::Kind::BITVECTOR_REDOR
, BITVECTOR_REDOR
},
491 {cvc5::Kind::BITVECTOR_REDAND
, BITVECTOR_REDAND
},
492 {cvc5::Kind::BITVECTOR_EXTRACT_OP
, BITVECTOR_EXTRACT
},
493 {cvc5::Kind::BITVECTOR_REPEAT_OP
, BITVECTOR_REPEAT
},
494 {cvc5::Kind::BITVECTOR_ZERO_EXTEND_OP
, BITVECTOR_ZERO_EXTEND
},
495 {cvc5::Kind::BITVECTOR_SIGN_EXTEND_OP
, BITVECTOR_SIGN_EXTEND
},
496 {cvc5::Kind::BITVECTOR_ROTATE_LEFT_OP
, BITVECTOR_ROTATE_LEFT
},
497 {cvc5::Kind::BITVECTOR_ROTATE_RIGHT_OP
, BITVECTOR_ROTATE_RIGHT
},
498 {cvc5::Kind::BITVECTOR_EXTRACT
, BITVECTOR_EXTRACT
},
499 {cvc5::Kind::BITVECTOR_REPEAT
, BITVECTOR_REPEAT
},
500 {cvc5::Kind::BITVECTOR_ZERO_EXTEND
, BITVECTOR_ZERO_EXTEND
},
501 {cvc5::Kind::BITVECTOR_SIGN_EXTEND
, BITVECTOR_SIGN_EXTEND
},
502 {cvc5::Kind::BITVECTOR_ROTATE_LEFT
, BITVECTOR_ROTATE_LEFT
},
503 {cvc5::Kind::BITVECTOR_ROTATE_RIGHT
, BITVECTOR_ROTATE_RIGHT
},
504 {cvc5::Kind::INT_TO_BITVECTOR_OP
, INT_TO_BITVECTOR
},
505 {cvc5::Kind::INT_TO_BITVECTOR
, INT_TO_BITVECTOR
},
506 {cvc5::Kind::BITVECTOR_TO_NAT
, BITVECTOR_TO_NAT
},
507 /* FP -------------------------------------------------------------- */
508 {cvc5::Kind::CONST_FLOATINGPOINT
, CONST_FLOATINGPOINT
},
509 {cvc5::Kind::CONST_ROUNDINGMODE
, CONST_ROUNDINGMODE
},
510 {cvc5::Kind::FLOATINGPOINT_FP
, FLOATINGPOINT_FP
},
511 {cvc5::Kind::FLOATINGPOINT_EQ
, FLOATINGPOINT_EQ
},
512 {cvc5::Kind::FLOATINGPOINT_ABS
, FLOATINGPOINT_ABS
},
513 {cvc5::Kind::FLOATINGPOINT_NEG
, FLOATINGPOINT_NEG
},
514 {cvc5::Kind::FLOATINGPOINT_ADD
, FLOATINGPOINT_ADD
},
515 {cvc5::Kind::FLOATINGPOINT_SUB
, FLOATINGPOINT_SUB
},
516 {cvc5::Kind::FLOATINGPOINT_MULT
, FLOATINGPOINT_MULT
},
517 {cvc5::Kind::FLOATINGPOINT_DIV
, FLOATINGPOINT_DIV
},
518 {cvc5::Kind::FLOATINGPOINT_FMA
, FLOATINGPOINT_FMA
},
519 {cvc5::Kind::FLOATINGPOINT_SQRT
, FLOATINGPOINT_SQRT
},
520 {cvc5::Kind::FLOATINGPOINT_REM
, FLOATINGPOINT_REM
},
521 {cvc5::Kind::FLOATINGPOINT_RTI
, FLOATINGPOINT_RTI
},
522 {cvc5::Kind::FLOATINGPOINT_MIN
, FLOATINGPOINT_MIN
},
523 {cvc5::Kind::FLOATINGPOINT_MAX
, FLOATINGPOINT_MAX
},
524 {cvc5::Kind::FLOATINGPOINT_LEQ
, FLOATINGPOINT_LEQ
},
525 {cvc5::Kind::FLOATINGPOINT_LT
, FLOATINGPOINT_LT
},
526 {cvc5::Kind::FLOATINGPOINT_GEQ
, FLOATINGPOINT_GEQ
},
527 {cvc5::Kind::FLOATINGPOINT_GT
, FLOATINGPOINT_GT
},
528 {cvc5::Kind::FLOATINGPOINT_ISN
, FLOATINGPOINT_ISN
},
529 {cvc5::Kind::FLOATINGPOINT_ISSN
, FLOATINGPOINT_ISSN
},
530 {cvc5::Kind::FLOATINGPOINT_ISZ
, FLOATINGPOINT_ISZ
},
531 {cvc5::Kind::FLOATINGPOINT_ISINF
, FLOATINGPOINT_ISINF
},
532 {cvc5::Kind::FLOATINGPOINT_ISNAN
, FLOATINGPOINT_ISNAN
},
533 {cvc5::Kind::FLOATINGPOINT_ISNEG
, FLOATINGPOINT_ISNEG
},
534 {cvc5::Kind::FLOATINGPOINT_ISPOS
, FLOATINGPOINT_ISPOS
},
535 {cvc5::Kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP
,
536 FLOATINGPOINT_TO_FP_IEEE_BITVECTOR
},
537 {cvc5::Kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR
,
538 FLOATINGPOINT_TO_FP_IEEE_BITVECTOR
},
539 {cvc5::Kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP
,
540 FLOATINGPOINT_TO_FP_FLOATINGPOINT
},
541 {cvc5::Kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT
,
542 FLOATINGPOINT_TO_FP_FLOATINGPOINT
},
543 {cvc5::Kind::FLOATINGPOINT_TO_FP_REAL_OP
, FLOATINGPOINT_TO_FP_REAL
},
544 {cvc5::Kind::FLOATINGPOINT_TO_FP_REAL
, FLOATINGPOINT_TO_FP_REAL
},
545 {cvc5::Kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP
,
546 FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR
},
547 {cvc5::Kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR
,
548 FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR
},
549 {cvc5::Kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP
,
550 FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR
},
551 {cvc5::Kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR
,
552 FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR
},
553 {cvc5::Kind::FLOATINGPOINT_TO_FP_GENERIC_OP
,
554 FLOATINGPOINT_TO_FP_GENERIC
},
555 {cvc5::Kind::FLOATINGPOINT_TO_FP_GENERIC
, FLOATINGPOINT_TO_FP_GENERIC
},
556 {cvc5::Kind::FLOATINGPOINT_TO_UBV_OP
, FLOATINGPOINT_TO_UBV
},
557 {cvc5::Kind::FLOATINGPOINT_TO_UBV
, FLOATINGPOINT_TO_UBV
},
558 {cvc5::Kind::FLOATINGPOINT_TO_UBV_TOTAL_OP
, INTERNAL_KIND
},
559 {cvc5::Kind::FLOATINGPOINT_TO_UBV_TOTAL
, INTERNAL_KIND
},
560 {cvc5::Kind::FLOATINGPOINT_TO_SBV_OP
, FLOATINGPOINT_TO_SBV
},
561 {cvc5::Kind::FLOATINGPOINT_TO_SBV
, FLOATINGPOINT_TO_SBV
},
562 {cvc5::Kind::FLOATINGPOINT_TO_SBV_TOTAL_OP
, INTERNAL_KIND
},
563 {cvc5::Kind::FLOATINGPOINT_TO_SBV_TOTAL
, INTERNAL_KIND
},
564 {cvc5::Kind::FLOATINGPOINT_TO_REAL
, FLOATINGPOINT_TO_REAL
},
565 {cvc5::Kind::FLOATINGPOINT_TO_REAL_TOTAL
, INTERNAL_KIND
},
566 /* Arrays ---------------------------------------------------------- */
567 {cvc5::Kind::SELECT
, SELECT
},
568 {cvc5::Kind::STORE
, STORE
},
569 {cvc5::Kind::STORE_ALL
, CONST_ARRAY
},
570 /* Datatypes ------------------------------------------------------- */
571 {cvc5::Kind::APPLY_SELECTOR
, APPLY_SELECTOR
},
572 {cvc5::Kind::APPLY_CONSTRUCTOR
, APPLY_CONSTRUCTOR
},
573 {cvc5::Kind::APPLY_SELECTOR_TOTAL
, INTERNAL_KIND
},
574 {cvc5::Kind::APPLY_TESTER
, APPLY_TESTER
},
575 {cvc5::Kind::APPLY_UPDATER
, APPLY_UPDATER
},
576 {cvc5::Kind::DT_SIZE
, DT_SIZE
},
577 {cvc5::Kind::MATCH
, MATCH
},
578 {cvc5::Kind::MATCH_CASE
, MATCH_CASE
},
579 {cvc5::Kind::MATCH_BIND_CASE
, MATCH_BIND_CASE
},
580 {cvc5::Kind::TUPLE_PROJECT
, TUPLE_PROJECT
},
581 {cvc5::Kind::TUPLE_PROJECT_OP
, TUPLE_PROJECT
},
582 /* Separation Logic ------------------------------------------------ */
583 {cvc5::Kind::SEP_NIL
, SEP_NIL
},
584 {cvc5::Kind::SEP_EMP
, SEP_EMP
},
585 {cvc5::Kind::SEP_PTO
, SEP_PTO
},
586 {cvc5::Kind::SEP_STAR
, SEP_STAR
},
587 {cvc5::Kind::SEP_WAND
, SEP_WAND
},
588 /* Sets ------------------------------------------------------------ */
589 {cvc5::Kind::SET_EMPTY
, SET_EMPTY
},
590 {cvc5::Kind::SET_UNION
, SET_UNION
},
591 {cvc5::Kind::SET_INTER
, SET_INTER
},
592 {cvc5::Kind::SET_MINUS
, SET_MINUS
},
593 {cvc5::Kind::SET_SUBSET
, SET_SUBSET
},
594 {cvc5::Kind::SET_MEMBER
, SET_MEMBER
},
595 {cvc5::Kind::SET_SINGLETON
, SET_SINGLETON
},
596 {cvc5::Kind::SET_INSERT
, SET_INSERT
},
597 {cvc5::Kind::SET_CARD
, SET_CARD
},
598 {cvc5::Kind::SET_COMPLEMENT
, SET_COMPLEMENT
},
599 {cvc5::Kind::SET_UNIVERSE
, SET_UNIVERSE
},
600 {cvc5::Kind::SET_COMPREHENSION
, SET_COMPREHENSION
},
601 {cvc5::Kind::SET_CHOOSE
, SET_CHOOSE
},
602 {cvc5::Kind::SET_IS_SINGLETON
, SET_IS_SINGLETON
},
603 {cvc5::Kind::SET_MAP
, SET_MAP
},
604 /* Relations ------------------------------------------------------- */
605 {cvc5::Kind::RELATION_JOIN
, RELATION_JOIN
},
606 {cvc5::Kind::RELATION_PRODUCT
, RELATION_PRODUCT
},
607 {cvc5::Kind::RELATION_TRANSPOSE
, RELATION_TRANSPOSE
},
608 {cvc5::Kind::RELATION_TCLOSURE
, RELATION_TCLOSURE
},
609 {cvc5::Kind::RELATION_JOIN_IMAGE
, RELATION_JOIN_IMAGE
},
610 {cvc5::Kind::RELATION_IDEN
, RELATION_IDEN
},
611 /* Bags ------------------------------------------------------------ */
612 {cvc5::Kind::BAG_UNION_MAX
, BAG_UNION_MAX
},
613 {cvc5::Kind::BAG_UNION_DISJOINT
, BAG_UNION_DISJOINT
},
614 {cvc5::Kind::BAG_INTER_MIN
, BAG_INTER_MIN
},
615 {cvc5::Kind::BAG_DIFFERENCE_SUBTRACT
, BAG_DIFFERENCE_SUBTRACT
},
616 {cvc5::Kind::BAG_DIFFERENCE_REMOVE
, BAG_DIFFERENCE_REMOVE
},
617 {cvc5::Kind::BAG_SUBBAG
, BAG_SUBBAG
},
618 {cvc5::Kind::BAG_COUNT
, BAG_COUNT
},
619 {cvc5::Kind::BAG_DUPLICATE_REMOVAL
, BAG_DUPLICATE_REMOVAL
},
620 {cvc5::Kind::BAG_MAKE
, BAG_MAKE
},
621 {cvc5::Kind::BAG_EMPTY
, BAG_EMPTY
},
622 {cvc5::Kind::BAG_CARD
, BAG_CARD
},
623 {cvc5::Kind::BAG_CHOOSE
, BAG_CHOOSE
},
624 {cvc5::Kind::BAG_IS_SINGLETON
, BAG_IS_SINGLETON
},
625 {cvc5::Kind::BAG_FROM_SET
, BAG_FROM_SET
},
626 {cvc5::Kind::BAG_TO_SET
, BAG_TO_SET
},
627 {cvc5::Kind::BAG_MAP
, BAG_MAP
},
628 {cvc5::Kind::BAG_FOLD
, BAG_FOLD
},
629 /* Strings --------------------------------------------------------- */
630 {cvc5::Kind::STRING_CONCAT
, STRING_CONCAT
},
631 {cvc5::Kind::STRING_IN_REGEXP
, STRING_IN_REGEXP
},
632 {cvc5::Kind::STRING_LENGTH
, STRING_LENGTH
},
633 {cvc5::Kind::STRING_SUBSTR
, STRING_SUBSTR
},
634 {cvc5::Kind::STRING_UPDATE
, STRING_UPDATE
},
635 {cvc5::Kind::STRING_CHARAT
, STRING_CHARAT
},
636 {cvc5::Kind::STRING_CONTAINS
, STRING_CONTAINS
},
637 {cvc5::Kind::STRING_INDEXOF
, STRING_INDEXOF
},
638 {cvc5::Kind::STRING_INDEXOF_RE
, STRING_INDEXOF_RE
},
639 {cvc5::Kind::STRING_REPLACE
, STRING_REPLACE
},
640 {cvc5::Kind::STRING_REPLACE_ALL
, STRING_REPLACE_ALL
},
641 {cvc5::Kind::STRING_REPLACE_RE
, STRING_REPLACE_RE
},
642 {cvc5::Kind::STRING_REPLACE_RE_ALL
, STRING_REPLACE_RE_ALL
},
643 {cvc5::Kind::STRING_TOLOWER
, STRING_TOLOWER
},
644 {cvc5::Kind::STRING_TOUPPER
, STRING_TOUPPER
},
645 {cvc5::Kind::STRING_REV
, STRING_REV
},
646 {cvc5::Kind::STRING_FROM_CODE
, STRING_FROM_CODE
},
647 {cvc5::Kind::STRING_TO_CODE
, STRING_TO_CODE
},
648 {cvc5::Kind::STRING_LT
, STRING_LT
},
649 {cvc5::Kind::STRING_LEQ
, STRING_LEQ
},
650 {cvc5::Kind::STRING_PREFIX
, STRING_PREFIX
},
651 {cvc5::Kind::STRING_SUFFIX
, STRING_SUFFIX
},
652 {cvc5::Kind::STRING_IS_DIGIT
, STRING_IS_DIGIT
},
653 {cvc5::Kind::STRING_ITOS
, STRING_FROM_INT
},
654 {cvc5::Kind::STRING_STOI
, STRING_TO_INT
},
655 {cvc5::Kind::CONST_STRING
, CONST_STRING
},
656 {cvc5::Kind::STRING_TO_REGEXP
, STRING_TO_REGEXP
},
657 {cvc5::Kind::REGEXP_CONCAT
, REGEXP_CONCAT
},
658 {cvc5::Kind::REGEXP_UNION
, REGEXP_UNION
},
659 {cvc5::Kind::REGEXP_INTER
, REGEXP_INTER
},
660 {cvc5::Kind::REGEXP_DIFF
, REGEXP_DIFF
},
661 {cvc5::Kind::REGEXP_STAR
, REGEXP_STAR
},
662 {cvc5::Kind::REGEXP_PLUS
, REGEXP_PLUS
},
663 {cvc5::Kind::REGEXP_OPT
, REGEXP_OPT
},
664 {cvc5::Kind::REGEXP_RANGE
, REGEXP_RANGE
},
665 {cvc5::Kind::REGEXP_REPEAT
, REGEXP_REPEAT
},
666 {cvc5::Kind::REGEXP_REPEAT_OP
, REGEXP_REPEAT
},
667 {cvc5::Kind::REGEXP_LOOP
, REGEXP_LOOP
},
668 {cvc5::Kind::REGEXP_LOOP_OP
, REGEXP_LOOP
},
669 {cvc5::Kind::REGEXP_NONE
, REGEXP_NONE
},
670 {cvc5::Kind::REGEXP_ALLCHAR
, REGEXP_ALLCHAR
},
671 {cvc5::Kind::REGEXP_COMPLEMENT
, REGEXP_COMPLEMENT
},
672 {cvc5::Kind::CONST_SEQUENCE
, CONST_SEQUENCE
},
673 {cvc5::Kind::SEQ_UNIT
, SEQ_UNIT
},
674 {cvc5::Kind::SEQ_NTH
, SEQ_NTH
},
675 /* Quantifiers ----------------------------------------------------- */
676 {cvc5::Kind::FORALL
, FORALL
},
677 {cvc5::Kind::EXISTS
, EXISTS
},
678 {cvc5::Kind::BOUND_VAR_LIST
, VARIABLE_LIST
},
679 {cvc5::Kind::INST_PATTERN
, INST_PATTERN
},
680 {cvc5::Kind::INST_NO_PATTERN
, INST_NO_PATTERN
},
681 {cvc5::Kind::INST_POOL
, INST_POOL
},
682 {cvc5::Kind::INST_ADD_TO_POOL
, INST_ADD_TO_POOL
},
683 {cvc5::Kind::SKOLEM_ADD_TO_POOL
, SKOLEM_ADD_TO_POOL
},
684 {cvc5::Kind::INST_ATTRIBUTE
, INST_ATTRIBUTE
},
685 {cvc5::Kind::INST_PATTERN_LIST
, INST_PATTERN_LIST
},
686 /* ----------------------------------------------------------------- */
687 {cvc5::Kind::LAST_KIND
, LAST_KIND
},
690 /* Set of kinds for indexed operators */
691 const static std::unordered_set
<Kind
> s_indexed_kinds(
695 BITVECTOR_ZERO_EXTEND
,
696 BITVECTOR_SIGN_EXTEND
,
697 BITVECTOR_ROTATE_LEFT
,
698 BITVECTOR_ROTATE_RIGHT
,
700 FLOATINGPOINT_TO_UBV
,
701 FLOATINGPOINT_TO_SBV
,
703 FLOATINGPOINT_TO_FP_IEEE_BITVECTOR
,
704 FLOATINGPOINT_TO_FP_FLOATINGPOINT
,
705 FLOATINGPOINT_TO_FP_REAL
,
706 FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR
,
707 FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR
,
708 FLOATINGPOINT_TO_FP_GENERIC
});
712 /** Convert a cvc5::Kind (internal) to a cvc5::api::Kind (external). */
713 cvc5::api::Kind
intToExtKind(cvc5::Kind k
)
715 auto it
= api::s_kinds_internal
.find(k
);
716 if (it
== api::s_kinds_internal
.end())
718 return api::INTERNAL_KIND
;
723 /** Convert a cvc5::api::Kind (external) to a cvc5::Kind (internal). */
724 cvc5::Kind
extToIntKind(cvc5::api::Kind k
)
726 auto it
= api::s_kinds
.find(k
);
727 if (it
== api::s_kinds
.end())
729 return cvc5::Kind::UNDEFINED_KIND
;
734 /** Return true if given kind is a defined external kind. */
735 bool isDefinedKind(Kind k
) { return k
> UNDEFINED_KIND
&& k
< LAST_KIND
; }
738 * Return true if the internal kind is one where the API term structure
739 * differs from internal structure. This happens for APPLY_* kinds.
740 * The API takes a "higher-order" perspective and treats functions as well
741 * as datatype constructors/selectors/testers as terms
742 * but interally they are not
744 bool isApplyKind(cvc5::Kind k
)
746 return (k
== cvc5::Kind::APPLY_UF
|| k
== cvc5::Kind::APPLY_CONSTRUCTOR
747 || k
== cvc5::Kind::APPLY_SELECTOR
|| k
== cvc5::Kind::APPLY_TESTER
748 || k
== cvc5::Kind::APPLY_UPDATER
);
751 #ifdef CVC5_ASSERTIONS
752 /** Return true if given kind is a defined internal kind. */
753 bool isDefinedIntKind(cvc5::Kind k
)
755 return k
!= cvc5::Kind::UNDEFINED_KIND
&& k
!= cvc5::Kind::LAST_KIND
;
759 /** Return the minimum arity of given kind. */
760 uint32_t minArity(Kind k
)
762 Assert(isDefinedKind(k
));
763 Assert(isDefinedIntKind(extToIntKind(k
)));
764 uint32_t min
= cvc5::kind::metakind::getMinArityForKind(extToIntKind(k
));
766 // At the API level, we treat functions/constructors/selectors/testers as
767 // normal terms instead of making them part of the operator
768 if (isApplyKind(extToIntKind(k
)))
775 /** Return the maximum arity of given kind. */
776 uint32_t maxArity(Kind k
)
778 Assert(isDefinedKind(k
));
779 Assert(isDefinedIntKind(extToIntKind(k
)));
780 uint32_t max
= cvc5::kind::metakind::getMaxArityForKind(extToIntKind(k
));
782 // At the API level, we treat functions/constructors/selectors/testers as
783 // normal terms instead of making them part of the operator
784 if (isApplyKind(extToIntKind(k
))
785 && max
!= std::numeric_limits
<uint32_t>::max()) // be careful not to
795 std::string
kindToString(Kind k
)
797 return k
== INTERNAL_KIND
? "INTERNAL_KIND"
798 : cvc5::kind::kindToString(extToIntKind(k
));
801 const char* toString(Kind k
)
803 return k
== INTERNAL_KIND
? "INTERNAL_KIND"
804 : cvc5::kind::toString(extToIntKind(k
));
807 std::ostream
& operator<<(std::ostream
& out
, Kind k
)
811 case INTERNAL_KIND
: out
<< "INTERNAL_KIND"; break;
812 default: out
<< extToIntKind(k
);
817 /* -------------------------------------------------------------------------- */
818 /* API guard helpers */
819 /* -------------------------------------------------------------------------- */
823 class CVC5ApiExceptionStream
826 CVC5ApiExceptionStream() {}
827 /* Note: This needs to be explicitly set to 'noexcept(false)' since it is
828 * a destructor that throws an exception and in C++11 all destructors
829 * default to noexcept(true) (else this triggers a call to std::terminate). */
830 ~CVC5ApiExceptionStream() noexcept(false)
832 if (std::uncaught_exceptions() == 0)
834 throw CVC5ApiException(d_stream
.str());
838 std::ostream
& ostream() { return d_stream
; }
841 std::stringstream d_stream
;
844 class CVC5ApiRecoverableExceptionStream
847 CVC5ApiRecoverableExceptionStream() {}
848 /* Note: This needs to be explicitly set to 'noexcept(false)' since it is
849 * a destructor that throws an exception and in C++11 all destructors
850 * default to noexcept(true) (else this triggers a call to std::terminate). */
851 ~CVC5ApiRecoverableExceptionStream() noexcept(false)
853 if (std::uncaught_exceptions() == 0)
855 throw CVC5ApiRecoverableException(d_stream
.str());
859 std::ostream
& ostream() { return d_stream
; }
862 std::stringstream d_stream
;
865 class CVC5ApiUnsupportedExceptionStream
868 CVC5ApiUnsupportedExceptionStream() {}
869 /* Note: This needs to be explicitly set to 'noexcept(false)' since it is
870 * a destructor that throws an exception and in C++11 all destructors
871 * default to noexcept(true) (else this triggers a call to std::terminate). */
872 ~CVC5ApiUnsupportedExceptionStream() noexcept(false)
874 if (std::uncaught_exceptions() == 0)
876 throw CVC5ApiUnsupportedException(d_stream
.str());
880 std::ostream
& ostream() { return d_stream
; }
883 std::stringstream d_stream
;
886 #define CVC5_API_TRY_CATCH_BEGIN \
889 #define CVC5_API_TRY_CATCH_END \
891 catch (const OptionException& e) \
893 throw CVC5ApiOptionException(e.getMessage()); \
895 catch (const cvc5::RecoverableModalException& e) \
897 throw CVC5ApiRecoverableException(e.getMessage()); \
899 catch (const cvc5::Exception& e) { throw CVC5ApiException(e.getMessage()); } \
900 catch (const std::invalid_argument& e) { throw CVC5ApiException(e.what()); }
904 /* -------------------------------------------------------------------------- */
906 /* -------------------------------------------------------------------------- */
908 Result::Result(const cvc5::Result
& r
) : d_result(new cvc5::Result(r
)) {}
910 Result::Result() : d_result(new cvc5::Result()) {}
912 bool Result::isNull() const
914 return d_result
->getType() == cvc5::Result::TYPE_NONE
;
917 bool Result::isSat(void) const
919 return d_result
->getType() == cvc5::Result::TYPE_SAT
920 && d_result
->isSat() == cvc5::Result::SAT
;
923 bool Result::isUnsat(void) const
925 return d_result
->getType() == cvc5::Result::TYPE_SAT
926 && d_result
->isSat() == cvc5::Result::UNSAT
;
929 bool Result::isSatUnknown(void) const
931 return d_result
->getType() == cvc5::Result::TYPE_SAT
932 && d_result
->isSat() == cvc5::Result::SAT_UNKNOWN
;
935 bool Result::isEntailed(void) const
937 return d_result
->getType() == cvc5::Result::TYPE_ENTAILMENT
938 && d_result
->isEntailed() == cvc5::Result::ENTAILED
;
941 bool Result::isNotEntailed(void) const
943 return d_result
->getType() == cvc5::Result::TYPE_ENTAILMENT
944 && d_result
->isEntailed() == cvc5::Result::NOT_ENTAILED
;
947 bool Result::isEntailmentUnknown(void) const
949 return d_result
->getType() == cvc5::Result::TYPE_ENTAILMENT
950 && d_result
->isEntailed() == cvc5::Result::ENTAILMENT_UNKNOWN
;
953 bool Result::operator==(const Result
& r
) const
955 return *d_result
== *r
.d_result
;
958 bool Result::operator!=(const Result
& r
) const
960 return *d_result
!= *r
.d_result
;
963 Result::UnknownExplanation
Result::getUnknownExplanation(void) const
965 cvc5::Result::UnknownExplanation expl
= d_result
->whyUnknown();
968 case cvc5::Result::REQUIRES_FULL_CHECK
: return REQUIRES_FULL_CHECK
;
969 case cvc5::Result::INCOMPLETE
: return INCOMPLETE
;
970 case cvc5::Result::TIMEOUT
: return TIMEOUT
;
971 case cvc5::Result::RESOURCEOUT
: return RESOURCEOUT
;
972 case cvc5::Result::MEMOUT
: return MEMOUT
;
973 case cvc5::Result::INTERRUPTED
: return INTERRUPTED
;
974 case cvc5::Result::NO_STATUS
: return NO_STATUS
;
975 case cvc5::Result::UNSUPPORTED
: return UNSUPPORTED
;
976 case cvc5::Result::OTHER
: return OTHER
;
977 default: return UNKNOWN_REASON
;
979 return UNKNOWN_REASON
;
982 std::string
Result::toString(void) const { return d_result
->toString(); }
984 std::ostream
& operator<<(std::ostream
& out
, const Result
& r
)
990 std::ostream
& operator<<(std::ostream
& out
, enum Result::UnknownExplanation e
)
994 case Result::REQUIRES_FULL_CHECK
: out
<< "REQUIRES_FULL_CHECK"; break;
995 case Result::INCOMPLETE
: out
<< "INCOMPLETE"; break;
996 case Result::TIMEOUT
: out
<< "TIMEOUT"; break;
997 case Result::RESOURCEOUT
: out
<< "RESOURCEOUT"; break;
998 case Result::MEMOUT
: out
<< "MEMOUT"; break;
999 case Result::INTERRUPTED
: out
<< "INTERRUPTED"; break;
1000 case Result::NO_STATUS
: out
<< "NO_STATUS"; break;
1001 case Result::UNSUPPORTED
: out
<< "UNSUPPORTED"; break;
1002 case Result::OTHER
: out
<< "OTHER"; break;
1003 case Result::UNKNOWN_REASON
: out
<< "UNKNOWN_REASON"; break;
1004 default: Unhandled() << e
;
1009 /* -------------------------------------------------------------------------- */
1011 /* -------------------------------------------------------------------------- */
1013 Sort::Sort(const Solver
* slv
, const cvc5::TypeNode
& t
)
1014 : d_solver(slv
), d_type(new cvc5::TypeNode(t
))
1018 Sort::Sort() : d_solver(nullptr), d_type(new cvc5::TypeNode()) {}
1022 if (d_solver
!= nullptr)
1028 std::set
<TypeNode
> Sort::sortSetToTypeNodes(const std::set
<Sort
>& sorts
)
1030 std::set
<TypeNode
> types
;
1031 for (const Sort
& s
: sorts
)
1033 types
.insert(s
.getTypeNode());
1038 std::vector
<TypeNode
> Sort::sortVectorToTypeNodes(
1039 const std::vector
<Sort
>& sorts
)
1041 std::vector
<TypeNode
> typeNodes
;
1042 for (const Sort
& sort
: sorts
)
1044 typeNodes
.push_back(sort
.getTypeNode());
1049 std::vector
<Sort
> Sort::typeNodeVectorToSorts(
1050 const Solver
* slv
, const std::vector
<TypeNode
>& types
)
1052 std::vector
<Sort
> sorts
;
1053 for (size_t i
= 0, tsize
= types
.size(); i
< tsize
; i
++)
1055 sorts
.push_back(Sort(slv
, types
[i
]));
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::operator>(const Sort
& s
) const
1089 CVC5_API_TRY_CATCH_BEGIN
;
1090 //////// all checks before this line
1091 return *d_type
> *s
.d_type
;
1093 CVC5_API_TRY_CATCH_END
;
1096 bool Sort::operator<=(const Sort
& s
) const
1098 CVC5_API_TRY_CATCH_BEGIN
;
1099 //////// all checks before this line
1100 return *d_type
<= *s
.d_type
;
1102 CVC5_API_TRY_CATCH_END
;
1105 bool Sort::operator>=(const Sort
& s
) const
1107 CVC5_API_TRY_CATCH_BEGIN
;
1108 //////// all checks before this line
1109 return *d_type
>= *s
.d_type
;
1111 CVC5_API_TRY_CATCH_END
;
1114 bool Sort::hasSymbol() const
1116 CVC5_API_TRY_CATCH_BEGIN
;
1117 CVC5_API_CHECK_NOT_NULL
;
1118 //////// all checks before this line
1119 return d_type
->hasAttribute(expr::VarNameAttr());
1121 CVC5_API_TRY_CATCH_END
;
1124 std::string
Sort::getSymbol() const
1126 CVC5_API_TRY_CATCH_BEGIN
;
1127 CVC5_API_CHECK_NOT_NULL
;
1128 CVC5_API_CHECK(d_type
->hasAttribute(expr::VarNameAttr()))
1129 << "Invalid call to '" << __PRETTY_FUNCTION__
1130 << "', expected the sort to have a symbol.";
1131 //////// all checks before this line
1132 return d_type
->getAttribute(expr::VarNameAttr());
1134 CVC5_API_TRY_CATCH_END
;
1137 bool Sort::isNull() const
1139 CVC5_API_TRY_CATCH_BEGIN
;
1140 //////// all checks before this line
1141 return isNullHelper();
1143 CVC5_API_TRY_CATCH_END
;
1146 bool Sort::isBoolean() const
1148 CVC5_API_TRY_CATCH_BEGIN
;
1149 //////// all checks before this line
1150 return d_type
->isBoolean();
1152 CVC5_API_TRY_CATCH_END
;
1155 bool Sort::isInteger() const
1157 CVC5_API_TRY_CATCH_BEGIN
;
1158 //////// all checks before this line
1159 return d_type
->isInteger();
1161 CVC5_API_TRY_CATCH_END
;
1164 bool Sort::isReal() const
1166 CVC5_API_TRY_CATCH_BEGIN
;
1167 //////// all checks before this line
1168 // notice that we do not expose internal subtyping to the user
1169 return d_type
->isReal() && !d_type
->isInteger();
1171 CVC5_API_TRY_CATCH_END
;
1174 bool Sort::isString() const
1176 CVC5_API_TRY_CATCH_BEGIN
;
1177 //////// all checks before this line
1178 return d_type
->isString();
1180 CVC5_API_TRY_CATCH_END
;
1183 bool Sort::isRegExp() const
1185 CVC5_API_TRY_CATCH_BEGIN
;
1186 //////// all checks before this line
1187 return d_type
->isRegExp();
1189 CVC5_API_TRY_CATCH_END
;
1192 bool Sort::isRoundingMode() const
1194 CVC5_API_TRY_CATCH_BEGIN
;
1195 //////// all checks before this line
1196 return d_type
->isRoundingMode();
1198 CVC5_API_TRY_CATCH_END
;
1201 bool Sort::isBitVector() const
1203 CVC5_API_TRY_CATCH_BEGIN
;
1204 //////// all checks before this line
1205 return d_type
->isBitVector();
1207 CVC5_API_TRY_CATCH_END
;
1210 bool Sort::isFloatingPoint() const
1212 CVC5_API_TRY_CATCH_BEGIN
;
1213 //////// all checks before this line
1214 return d_type
->isFloatingPoint();
1216 CVC5_API_TRY_CATCH_END
;
1219 bool Sort::isDatatype() const
1221 CVC5_API_TRY_CATCH_BEGIN
;
1222 //////// all checks before this line
1223 return d_type
->isDatatype();
1225 CVC5_API_TRY_CATCH_END
;
1228 bool Sort::isParametricDatatype() const
1230 CVC5_API_TRY_CATCH_BEGIN
;
1231 //////// all checks before this line
1232 if (!d_type
->isDatatype()) return false;
1233 return d_type
->isParametricDatatype();
1235 CVC5_API_TRY_CATCH_END
;
1238 bool Sort::isConstructor() const
1240 CVC5_API_TRY_CATCH_BEGIN
;
1241 //////// all checks before this line
1242 return d_type
->isConstructor();
1244 CVC5_API_TRY_CATCH_END
;
1247 bool Sort::isSelector() const
1249 CVC5_API_TRY_CATCH_BEGIN
;
1250 //////// all checks before this line
1251 return d_type
->isSelector();
1253 CVC5_API_TRY_CATCH_END
;
1256 bool Sort::isTester() const
1258 CVC5_API_TRY_CATCH_BEGIN
;
1259 //////// all checks before this line
1260 return d_type
->isTester();
1262 CVC5_API_TRY_CATCH_END
;
1265 bool Sort::isUpdater() const
1267 CVC5_API_TRY_CATCH_BEGIN
;
1268 //////// all checks before this line
1269 return d_type
->isUpdater();
1271 CVC5_API_TRY_CATCH_END
;
1274 bool Sort::isFunction() const
1276 CVC5_API_TRY_CATCH_BEGIN
;
1277 //////// all checks before this line
1278 return d_type
->isFunction();
1280 CVC5_API_TRY_CATCH_END
;
1283 bool Sort::isPredicate() const
1285 CVC5_API_TRY_CATCH_BEGIN
;
1286 //////// all checks before this line
1287 return d_type
->isPredicate();
1289 CVC5_API_TRY_CATCH_END
;
1292 bool Sort::isTuple() const
1294 CVC5_API_TRY_CATCH_BEGIN
;
1295 //////// all checks before this line
1296 return d_type
->isTuple();
1298 CVC5_API_TRY_CATCH_END
;
1301 bool Sort::isRecord() const
1303 CVC5_API_TRY_CATCH_BEGIN
;
1304 //////// all checks before this line
1305 return d_type
->isRecord();
1307 CVC5_API_TRY_CATCH_END
;
1310 bool Sort::isArray() const
1312 CVC5_API_TRY_CATCH_BEGIN
;
1313 //////// all checks before this line
1314 return d_type
->isArray();
1316 CVC5_API_TRY_CATCH_END
;
1319 bool Sort::isSet() const
1321 CVC5_API_TRY_CATCH_BEGIN
;
1322 //////// all checks before this line
1323 return d_type
->isSet();
1325 CVC5_API_TRY_CATCH_END
;
1328 bool Sort::isBag() const
1330 CVC5_API_TRY_CATCH_BEGIN
;
1331 //////// all checks before this line
1332 return d_type
->isBag();
1334 CVC5_API_TRY_CATCH_END
;
1337 bool Sort::isSequence() const
1339 CVC5_API_TRY_CATCH_BEGIN
;
1340 //////// all checks before this line
1341 return d_type
->isSequence();
1343 CVC5_API_TRY_CATCH_END
;
1346 bool Sort::isUninterpretedSort() const
1348 CVC5_API_TRY_CATCH_BEGIN
;
1349 //////// all checks before this line
1350 return d_type
->isSort();
1352 CVC5_API_TRY_CATCH_END
;
1355 bool Sort::isSortConstructor() const
1357 CVC5_API_TRY_CATCH_BEGIN
;
1358 //////// all checks before this line
1359 return d_type
->isSortConstructor();
1361 CVC5_API_TRY_CATCH_END
;
1364 bool Sort::isFirstClass() const
1366 CVC5_API_TRY_CATCH_BEGIN
;
1367 //////// all checks before this line
1368 return d_type
->isFirstClass();
1370 CVC5_API_TRY_CATCH_END
;
1373 bool Sort::isFunctionLike() const
1375 CVC5_API_TRY_CATCH_BEGIN
;
1376 //////// all checks before this line
1377 return d_type
->isFunctionLike();
1379 CVC5_API_TRY_CATCH_END
;
1382 bool Sort::isSubsortOf(const Sort
& s
) const
1384 CVC5_API_TRY_CATCH_BEGIN
;
1385 CVC5_API_ARG_CHECK_SOLVER("sort", s
);
1386 //////// all checks before this line
1387 return d_type
->isSubtypeOf(*s
.d_type
);
1389 CVC5_API_TRY_CATCH_END
;
1392 bool Sort::isComparableTo(const Sort
& s
) const
1394 CVC5_API_TRY_CATCH_BEGIN
;
1395 CVC5_API_ARG_CHECK_SOLVER("sort", s
);
1396 //////// all checks before this line
1397 return d_type
->isComparableTo(*s
.d_type
);
1399 CVC5_API_TRY_CATCH_END
;
1402 Datatype
Sort::getDatatype() const
1404 CVC5_API_TRY_CATCH_BEGIN
;
1405 CVC5_API_CHECK_NOT_NULL
;
1406 CVC5_API_CHECK(isDatatype()) << "Expected datatype sort.";
1407 //////// all checks before this line
1408 return Datatype(d_solver
, d_type
->getDType());
1410 CVC5_API_TRY_CATCH_END
;
1413 Sort
Sort::instantiate(const std::vector
<Sort
>& params
) const
1415 CVC5_API_TRY_CATCH_BEGIN
;
1416 CVC5_API_CHECK_NOT_NULL
;
1417 CVC5_API_CHECK_SORTS(params
);
1418 CVC5_API_CHECK(isParametricDatatype() || isSortConstructor())
1419 << "Expected parametric datatype or sort constructor sort.";
1420 //////// all checks before this line
1421 std::vector
<cvc5::TypeNode
> tparams
= sortVectorToTypeNodes(params
);
1422 if (d_type
->isDatatype())
1424 return Sort(d_solver
, d_type
->instantiateParametricDatatype(tparams
));
1426 Assert(d_type
->isSortConstructor());
1427 return Sort(d_solver
, d_solver
->getNodeManager()->mkSort(*d_type
, tparams
));
1429 CVC5_API_TRY_CATCH_END
;
1432 Sort
Sort::substitute(const Sort
& sort
, const Sort
& replacement
) const
1434 CVC5_API_TRY_CATCH_BEGIN
;
1435 CVC5_API_CHECK_NOT_NULL
;
1436 CVC5_API_CHECK_SORT(sort
);
1437 CVC5_API_CHECK_SORT(replacement
);
1438 //////// all checks before this line
1441 d_type
->substitute(sort
.getTypeNode(), replacement
.getTypeNode()));
1443 CVC5_API_TRY_CATCH_END
;
1446 Sort
Sort::substitute(const std::vector
<Sort
>& sorts
,
1447 const std::vector
<Sort
>& replacements
) const
1449 CVC5_API_TRY_CATCH_BEGIN
;
1450 CVC5_API_CHECK_NOT_NULL
;
1451 CVC5_API_CHECK_SORTS(sorts
);
1452 CVC5_API_CHECK_SORTS(replacements
);
1453 //////// all checks before this line
1455 std::vector
<cvc5::TypeNode
> tSorts
= sortVectorToTypeNodes(sorts
),
1457 sortVectorToTypeNodes(replacements
);
1458 return Sort(d_solver
,
1459 d_type
->substitute(tSorts
.begin(),
1461 tReplacements
.begin(),
1462 tReplacements
.end()));
1464 CVC5_API_TRY_CATCH_END
;
1467 std::string
Sort::toString() const
1469 CVC5_API_TRY_CATCH_BEGIN
;
1470 //////// all checks before this line
1471 return d_type
->toString();
1473 CVC5_API_TRY_CATCH_END
;
1476 const cvc5::TypeNode
& Sort::getTypeNode(void) const { return *d_type
; }
1478 /* Constructor sort ------------------------------------------------------- */
1480 size_t Sort::getConstructorArity() const
1482 CVC5_API_TRY_CATCH_BEGIN
;
1483 CVC5_API_CHECK_NOT_NULL
;
1484 CVC5_API_CHECK(isConstructor()) << "Not a constructor sort: " << (*this);
1485 //////// all checks before this line
1486 return d_type
->getNumChildren() - 1;
1488 CVC5_API_TRY_CATCH_END
;
1491 std::vector
<Sort
> Sort::getConstructorDomainSorts() const
1493 CVC5_API_TRY_CATCH_BEGIN
;
1494 CVC5_API_CHECK_NOT_NULL
;
1495 CVC5_API_CHECK(isConstructor()) << "Not a constructor sort: " << (*this);
1496 //////// all checks before this line
1497 return typeNodeVectorToSorts(d_solver
, d_type
->getArgTypes());
1499 CVC5_API_TRY_CATCH_END
;
1502 Sort
Sort::getConstructorCodomainSort() const
1504 CVC5_API_TRY_CATCH_BEGIN
;
1505 CVC5_API_CHECK_NOT_NULL
;
1506 CVC5_API_CHECK(isConstructor()) << "Not a constructor sort: " << (*this);
1507 //////// all checks before this line
1508 return Sort(d_solver
, d_type
->getConstructorRangeType());
1510 CVC5_API_TRY_CATCH_END
;
1513 /* Selector sort ------------------------------------------------------- */
1515 Sort
Sort::getSelectorDomainSort() const
1517 CVC5_API_TRY_CATCH_BEGIN
;
1518 CVC5_API_CHECK_NOT_NULL
;
1519 CVC5_API_CHECK(isSelector()) << "Not a selector sort: " << (*this);
1520 //////// all checks before this line
1521 return Sort(d_solver
, d_type
->getSelectorDomainType());
1523 CVC5_API_TRY_CATCH_END
;
1526 Sort
Sort::getSelectorCodomainSort() const
1528 CVC5_API_TRY_CATCH_BEGIN
;
1529 CVC5_API_CHECK_NOT_NULL
;
1530 CVC5_API_CHECK(isSelector()) << "Not a selector sort: " << (*this);
1531 //////// all checks before this line
1532 return Sort(d_solver
, d_type
->getSelectorRangeType());
1534 CVC5_API_TRY_CATCH_END
;
1537 /* Tester sort ------------------------------------------------------- */
1539 Sort
Sort::getTesterDomainSort() const
1541 CVC5_API_TRY_CATCH_BEGIN
;
1542 CVC5_API_CHECK_NOT_NULL
;
1543 CVC5_API_CHECK(isTester()) << "Not a tester sort: " << (*this);
1544 //////// all checks before this line
1545 return Sort(d_solver
, d_type
->getTesterDomainType());
1547 CVC5_API_TRY_CATCH_END
;
1550 Sort
Sort::getTesterCodomainSort() const
1552 CVC5_API_TRY_CATCH_BEGIN
;
1553 CVC5_API_CHECK_NOT_NULL
;
1554 CVC5_API_CHECK(isTester()) << "Not a tester sort: " << (*this);
1555 //////// all checks before this line
1556 return d_solver
->getBooleanSort();
1558 CVC5_API_TRY_CATCH_END
;
1561 /* Function sort ------------------------------------------------------- */
1563 size_t Sort::getFunctionArity() const
1565 CVC5_API_TRY_CATCH_BEGIN
;
1566 CVC5_API_CHECK_NOT_NULL
;
1567 CVC5_API_CHECK(isFunction()) << "Not a function sort: " << (*this);
1568 //////// all checks before this line
1569 return d_type
->getNumChildren() - 1;
1571 CVC5_API_TRY_CATCH_END
;
1574 std::vector
<Sort
> Sort::getFunctionDomainSorts() const
1576 CVC5_API_TRY_CATCH_BEGIN
;
1577 CVC5_API_CHECK_NOT_NULL
;
1578 CVC5_API_CHECK(isFunction()) << "Not a function sort: " << (*this);
1579 //////// all checks before this line
1580 return typeNodeVectorToSorts(d_solver
, d_type
->getArgTypes());
1582 CVC5_API_TRY_CATCH_END
;
1585 Sort
Sort::getFunctionCodomainSort() const
1587 CVC5_API_TRY_CATCH_BEGIN
;
1588 CVC5_API_CHECK_NOT_NULL
;
1589 CVC5_API_CHECK(isFunction()) << "Not a function sort" << (*this);
1590 //////// all checks before this line
1591 return Sort(d_solver
, d_type
->getRangeType());
1593 CVC5_API_TRY_CATCH_END
;
1596 /* Array sort ---------------------------------------------------------- */
1598 Sort
Sort::getArrayIndexSort() const
1600 CVC5_API_TRY_CATCH_BEGIN
;
1601 CVC5_API_CHECK_NOT_NULL
;
1602 CVC5_API_CHECK(isArray()) << "Not an array sort.";
1603 //////// all checks before this line
1604 return Sort(d_solver
, d_type
->getArrayIndexType());
1606 CVC5_API_TRY_CATCH_END
;
1609 Sort
Sort::getArrayElementSort() const
1611 CVC5_API_TRY_CATCH_BEGIN
;
1612 CVC5_API_CHECK_NOT_NULL
;
1613 CVC5_API_CHECK(isArray()) << "Not an array sort.";
1614 //////// all checks before this line
1615 return Sort(d_solver
, d_type
->getArrayConstituentType());
1617 CVC5_API_TRY_CATCH_END
;
1620 /* Set sort ------------------------------------------------------------ */
1622 Sort
Sort::getSetElementSort() const
1624 CVC5_API_TRY_CATCH_BEGIN
;
1625 CVC5_API_CHECK_NOT_NULL
;
1626 CVC5_API_CHECK(isSet()) << "Not a set sort.";
1627 //////// all checks before this line
1628 return Sort(d_solver
, d_type
->getSetElementType());
1630 CVC5_API_TRY_CATCH_END
;
1633 /* Bag sort ------------------------------------------------------------ */
1635 Sort
Sort::getBagElementSort() const
1637 CVC5_API_TRY_CATCH_BEGIN
;
1638 CVC5_API_CHECK_NOT_NULL
;
1639 CVC5_API_CHECK(isBag()) << "Not a bag sort.";
1640 //////// all checks before this line
1641 return Sort(d_solver
, d_type
->getBagElementType());
1643 CVC5_API_TRY_CATCH_END
;
1646 /* Sequence sort ------------------------------------------------------- */
1648 Sort
Sort::getSequenceElementSort() const
1650 CVC5_API_TRY_CATCH_BEGIN
;
1651 CVC5_API_CHECK_NOT_NULL
;
1652 CVC5_API_CHECK(isSequence()) << "Not a sequence sort.";
1653 //////// all checks before this line
1654 return Sort(d_solver
, d_type
->getSequenceElementType());
1656 CVC5_API_TRY_CATCH_END
;
1659 /* Uninterpreted sort -------------------------------------------------- */
1661 std::string
Sort::getUninterpretedSortName() const
1663 CVC5_API_TRY_CATCH_BEGIN
;
1664 CVC5_API_CHECK_NOT_NULL
;
1665 CVC5_API_CHECK(isUninterpretedSort()) << "Not an uninterpreted sort.";
1666 //////// all checks before this line
1667 return d_type
->getName();
1669 CVC5_API_TRY_CATCH_END
;
1672 bool Sort::isUninterpretedSortParameterized() const
1674 CVC5_API_TRY_CATCH_BEGIN
;
1675 CVC5_API_CHECK_NOT_NULL
;
1676 CVC5_API_CHECK(isUninterpretedSort()) << "Not an uninterpreted sort.";
1677 //////// all checks before this line
1679 /* This method is not implemented in the NodeManager, since whether a
1680 * uninterpreted sort is parameterized is irrelevant for solving. */
1681 return d_type
->getNumChildren() > 0;
1683 CVC5_API_TRY_CATCH_END
;
1686 std::vector
<Sort
> Sort::getUninterpretedSortParamSorts() const
1688 CVC5_API_TRY_CATCH_BEGIN
;
1689 CVC5_API_CHECK_NOT_NULL
;
1690 CVC5_API_CHECK(isUninterpretedSort()) << "Not an uninterpreted sort.";
1691 //////// all checks before this line
1693 /* This method is not implemented in the NodeManager, since whether a
1694 * uninterpreted sort is parameterized is irrelevant for solving. */
1695 std::vector
<TypeNode
> params
;
1696 for (size_t i
= 0, nchildren
= d_type
->getNumChildren(); i
< nchildren
; i
++)
1698 params
.push_back((*d_type
)[i
]);
1700 return typeNodeVectorToSorts(d_solver
, params
);
1702 CVC5_API_TRY_CATCH_END
;
1705 /* Sort constructor sort ----------------------------------------------- */
1707 std::string
Sort::getSortConstructorName() const
1709 CVC5_API_TRY_CATCH_BEGIN
;
1710 CVC5_API_CHECK_NOT_NULL
;
1711 CVC5_API_CHECK(isSortConstructor()) << "Not a sort constructor sort.";
1712 //////// all checks before this line
1713 return d_type
->getName();
1715 CVC5_API_TRY_CATCH_END
;
1718 size_t Sort::getSortConstructorArity() const
1720 CVC5_API_TRY_CATCH_BEGIN
;
1721 CVC5_API_CHECK_NOT_NULL
;
1722 CVC5_API_CHECK(isSortConstructor()) << "Not a sort constructor sort.";
1723 //////// all checks before this line
1724 return d_type
->getSortConstructorArity();
1726 CVC5_API_TRY_CATCH_END
;
1729 /* Bit-vector sort ----------------------------------------------------- */
1731 uint32_t Sort::getBitVectorSize() const
1733 CVC5_API_TRY_CATCH_BEGIN
;
1734 CVC5_API_CHECK_NOT_NULL
;
1735 CVC5_API_CHECK(isBitVector()) << "Not a bit-vector sort.";
1736 //////// all checks before this line
1737 return d_type
->getBitVectorSize();
1739 CVC5_API_TRY_CATCH_END
;
1742 /* Floating-point sort ------------------------------------------------- */
1744 uint32_t Sort::getFloatingPointExponentSize() const
1746 CVC5_API_TRY_CATCH_BEGIN
;
1747 CVC5_API_CHECK_NOT_NULL
;
1748 CVC5_API_CHECK(isFloatingPoint()) << "Not a floating-point sort.";
1749 //////// all checks before this line
1750 return d_type
->getFloatingPointExponentSize();
1752 CVC5_API_TRY_CATCH_END
;
1755 uint32_t Sort::getFloatingPointSignificandSize() const
1757 CVC5_API_TRY_CATCH_BEGIN
;
1758 CVC5_API_CHECK_NOT_NULL
;
1759 CVC5_API_CHECK(isFloatingPoint()) << "Not a floating-point sort.";
1760 //////// all checks before this line
1761 return d_type
->getFloatingPointSignificandSize();
1763 CVC5_API_TRY_CATCH_END
;
1766 /* Datatype sort ------------------------------------------------------- */
1768 std::vector
<Sort
> Sort::getDatatypeParamSorts() const
1770 CVC5_API_TRY_CATCH_BEGIN
;
1771 CVC5_API_CHECK_NOT_NULL
;
1772 CVC5_API_CHECK(isParametricDatatype()) << "Not a parametric datatype sort.";
1773 //////// all checks before this line
1774 return typeNodeVectorToSorts(d_solver
, d_type
->getParamTypes());
1776 CVC5_API_TRY_CATCH_END
;
1779 size_t Sort::getDatatypeArity() const
1781 CVC5_API_TRY_CATCH_BEGIN
;
1782 CVC5_API_CHECK_NOT_NULL
;
1783 CVC5_API_CHECK(isDatatype()) << "Not a datatype sort.";
1784 //////// all checks before this line
1785 return d_type
->isParametricDatatype() ? d_type
->getNumChildren() - 1 : 0;
1787 CVC5_API_TRY_CATCH_END
;
1790 /* Tuple sort ---------------------------------------------------------- */
1792 size_t Sort::getTupleLength() const
1794 CVC5_API_TRY_CATCH_BEGIN
;
1795 CVC5_API_CHECK_NOT_NULL
;
1796 CVC5_API_CHECK(isTuple()) << "Not a tuple sort.";
1797 //////// all checks before this line
1798 return d_type
->getTupleLength();
1800 CVC5_API_TRY_CATCH_END
;
1803 std::vector
<Sort
> Sort::getTupleSorts() const
1805 CVC5_API_TRY_CATCH_BEGIN
;
1806 CVC5_API_CHECK_NOT_NULL
;
1807 CVC5_API_CHECK(isTuple()) << "Not a tuple sort.";
1808 //////// all checks before this line
1809 return typeNodeVectorToSorts(d_solver
, d_type
->getTupleTypes());
1811 CVC5_API_TRY_CATCH_END
;
1814 /* --------------------------------------------------------------------- */
1816 std::ostream
& operator<<(std::ostream
& out
, const Sort
& s
)
1818 out
<< s
.toString();
1823 /* -------------------------------------------------------------------------- */
1825 /* Split out to avoid nested API calls (problematic with API tracing). */
1826 /* .......................................................................... */
1828 bool Sort::isNullHelper() const { return d_type
->isNull(); }
1830 /* -------------------------------------------------------------------------- */
1832 /* -------------------------------------------------------------------------- */
1834 Op::Op() : d_solver(nullptr), d_kind(NULL_EXPR
), d_node(new cvc5::Node()) {}
1836 Op::Op(const Solver
* slv
, const Kind k
)
1837 : d_solver(slv
), d_kind(k
), d_node(new cvc5::Node())
1841 Op::Op(const Solver
* slv
, const Kind k
, const cvc5::Node
& n
)
1842 : d_solver(slv
), d_kind(k
), d_node(new cvc5::Node(n
))
1848 if (d_solver
!= nullptr)
1850 // Ensure that the correct node manager is in scope when the type node is
1856 /* Public methods */
1857 bool Op::operator==(const Op
& t
) const
1859 CVC5_API_TRY_CATCH_BEGIN
;
1860 //////// all checks before this line
1861 if (d_node
->isNull() && t
.d_node
->isNull())
1863 return (d_kind
== t
.d_kind
);
1865 else if (d_node
->isNull() || t
.d_node
->isNull())
1869 return (d_kind
== t
.d_kind
) && (*d_node
== *t
.d_node
);
1871 CVC5_API_TRY_CATCH_END
;
1874 bool Op::operator!=(const Op
& t
) const
1876 CVC5_API_TRY_CATCH_BEGIN
;
1877 //////// all checks before this line
1878 return !(*this == t
);
1880 CVC5_API_TRY_CATCH_END
;
1883 Kind
Op::getKind() const
1885 CVC5_API_CHECK(d_kind
!= NULL_EXPR
) << "Expecting a non-null Kind";
1886 //////// all checks before this line
1890 bool Op::isNull() const
1892 CVC5_API_TRY_CATCH_BEGIN
;
1893 //////// all checks before this line
1894 return isNullHelper();
1896 CVC5_API_TRY_CATCH_END
;
1899 bool Op::isIndexed() const
1901 CVC5_API_TRY_CATCH_BEGIN
;
1902 //////// all checks before this line
1903 return isIndexedHelper();
1905 CVC5_API_TRY_CATCH_END
;
1908 size_t Op::getNumIndices() const
1910 CVC5_API_TRY_CATCH_BEGIN
;
1911 CVC5_API_CHECK_NOT_NULL
;
1912 //////// all checks before this line
1913 return getNumIndicesHelper();
1915 CVC5_API_TRY_CATCH_END
;
1918 size_t Op::getNumIndicesHelper() const
1920 if (!isIndexedHelper())
1925 Kind k
= intToExtKind(d_node
->getKind());
1929 case DIVISIBLE
: size
= 1; break;
1930 case BITVECTOR_REPEAT
: size
= 1; break;
1931 case BITVECTOR_ZERO_EXTEND
: size
= 1; break;
1932 case BITVECTOR_SIGN_EXTEND
: size
= 1; break;
1933 case BITVECTOR_ROTATE_LEFT
: size
= 1; break;
1934 case BITVECTOR_ROTATE_RIGHT
: size
= 1; break;
1935 case INT_TO_BITVECTOR
: size
= 1; break;
1936 case IAND
: size
= 1; break;
1937 case FLOATINGPOINT_TO_UBV
: size
= 1; break;
1938 case FLOATINGPOINT_TO_SBV
: size
= 1; break;
1939 case REGEXP_REPEAT
: size
= 1; break;
1940 case BITVECTOR_EXTRACT
: size
= 2; break;
1941 case FLOATINGPOINT_TO_FP_IEEE_BITVECTOR
: size
= 2; break;
1942 case FLOATINGPOINT_TO_FP_FLOATINGPOINT
: size
= 2; break;
1943 case FLOATINGPOINT_TO_FP_REAL
: size
= 2; break;
1944 case FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR
: size
= 2; break;
1945 case FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR
: size
= 2; break;
1946 case FLOATINGPOINT_TO_FP_GENERIC
: size
= 2; break;
1947 case REGEXP_LOOP
: size
= 2; break;
1949 size
= d_node
->getConst
<TupleProjectOp
>().getIndices().size();
1951 default: CVC5_API_CHECK(false) << "Unhandled kind " << kindToString(k
);
1956 Term
Op::operator[](size_t index
) const
1958 return getIndexHelper(index
);
1961 Term
Op::getIndexHelper(size_t index
) const
1963 CVC5_API_TRY_CATCH_BEGIN
;
1964 CVC5_API_CHECK_NOT_NULL
;
1965 CVC5_API_CHECK(!d_node
->isNull())
1966 << "Expecting a non-null internal expression. This Op is not indexed.";
1967 CVC5_API_CHECK(index
< getNumIndicesHelper()) << "index out of bound";
1968 Kind k
= intToExtKind(d_node
->getKind());
1974 t
= d_solver
->mkRationalValHelper(
1975 Rational(d_node
->getConst
<Divisible
>().k
));
1978 case BITVECTOR_REPEAT
:
1980 t
= d_solver
->mkRationalValHelper(
1981 d_node
->getConst
<BitVectorRepeat
>().d_repeatAmount
);
1984 case BITVECTOR_ZERO_EXTEND
:
1986 t
= d_solver
->mkRationalValHelper(
1987 d_node
->getConst
<BitVectorZeroExtend
>().d_zeroExtendAmount
);
1990 case BITVECTOR_SIGN_EXTEND
:
1992 t
= d_solver
->mkRationalValHelper(
1993 d_node
->getConst
<BitVectorSignExtend
>().d_signExtendAmount
);
1996 case BITVECTOR_ROTATE_LEFT
:
1998 t
= d_solver
->mkRationalValHelper(
1999 d_node
->getConst
<BitVectorRotateLeft
>().d_rotateLeftAmount
);
2002 case BITVECTOR_ROTATE_RIGHT
:
2004 t
= d_solver
->mkRationalValHelper(
2005 d_node
->getConst
<BitVectorRotateRight
>().d_rotateRightAmount
);
2008 case INT_TO_BITVECTOR
:
2010 t
= d_solver
->mkRationalValHelper(
2011 d_node
->getConst
<IntToBitVector
>().d_size
);
2016 t
= d_solver
->mkRationalValHelper(d_node
->getConst
<IntAnd
>().d_size
);
2019 case FLOATINGPOINT_TO_UBV
:
2021 t
= d_solver
->mkRationalValHelper(
2022 d_node
->getConst
<FloatingPointToUBV
>().d_bv_size
.d_size
);
2025 case FLOATINGPOINT_TO_SBV
:
2027 t
= d_solver
->mkRationalValHelper(
2028 d_node
->getConst
<FloatingPointToSBV
>().d_bv_size
.d_size
);
2033 t
= d_solver
->mkRationalValHelper(
2034 d_node
->getConst
<RegExpRepeat
>().d_repeatAmount
);
2037 case BITVECTOR_EXTRACT
:
2039 cvc5::BitVectorExtract ext
= d_node
->getConst
<BitVectorExtract
>();
2040 t
= index
== 0 ? d_solver
->mkRationalValHelper(ext
.d_high
)
2041 : d_solver
->mkRationalValHelper(ext
.d_low
);
2044 case FLOATINGPOINT_TO_FP_IEEE_BITVECTOR
:
2046 cvc5::FloatingPointToFPIEEEBitVector ext
=
2047 d_node
->getConst
<FloatingPointToFPIEEEBitVector
>();
2050 ? d_solver
->mkRationalValHelper(ext
.getSize().exponentWidth())
2051 : d_solver
->mkRationalValHelper(ext
.getSize().significandWidth());
2054 case FLOATINGPOINT_TO_FP_FLOATINGPOINT
:
2056 cvc5::FloatingPointToFPFloatingPoint ext
=
2057 d_node
->getConst
<FloatingPointToFPFloatingPoint
>();
2059 ? d_solver
->mkRationalValHelper(ext
.getSize().exponentWidth())
2060 : d_solver
->mkRationalValHelper(ext
.getSize().significandWidth());
2063 case FLOATINGPOINT_TO_FP_REAL
:
2065 cvc5::FloatingPointToFPReal ext
=
2066 d_node
->getConst
<FloatingPointToFPReal
>();
2069 ? d_solver
->mkRationalValHelper(ext
.getSize().exponentWidth())
2070 : d_solver
->mkRationalValHelper(ext
.getSize().significandWidth());
2073 case FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR
:
2075 cvc5::FloatingPointToFPSignedBitVector ext
=
2076 d_node
->getConst
<FloatingPointToFPSignedBitVector
>();
2078 ? d_solver
->mkRationalValHelper(ext
.getSize().exponentWidth())
2079 : d_solver
->mkRationalValHelper(ext
.getSize().significandWidth());
2082 case FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR
:
2084 cvc5::FloatingPointToFPUnsignedBitVector ext
=
2085 d_node
->getConst
<FloatingPointToFPUnsignedBitVector
>();
2087 ? d_solver
->mkRationalValHelper(ext
.getSize().exponentWidth())
2088 : d_solver
->mkRationalValHelper(ext
.getSize().significandWidth());
2091 case FLOATINGPOINT_TO_FP_GENERIC
:
2093 cvc5::FloatingPointToFPGeneric ext
=
2094 d_node
->getConst
<FloatingPointToFPGeneric
>();
2096 ? d_solver
->mkRationalValHelper(ext
.getSize().exponentWidth())
2097 : d_solver
->mkRationalValHelper(ext
.getSize().significandWidth());
2102 cvc5::RegExpLoop ext
= d_node
->getConst
<RegExpLoop
>();
2103 t
= index
== 0 ? d_solver
->mkRationalValHelper(ext
.d_loopMinOcc
)
2104 : d_solver
->mkRationalValHelper(ext
.d_loopMaxOcc
);
2111 const std::vector
<uint32_t>& projectionIndices
=
2112 d_node
->getConst
<TupleProjectOp
>().getIndices();
2113 t
= d_solver
->mkRationalValHelper(projectionIndices
[index
]);
2118 CVC5_API_CHECK(false) << "Unhandled kind " << kindToString(k
);
2123 //////// all checks before this line
2126 CVC5_API_TRY_CATCH_END
;
2130 std::string
Op::getIndices() const
2132 CVC5_API_TRY_CATCH_BEGIN
;
2133 CVC5_API_CHECK_NOT_NULL
;
2134 CVC5_API_CHECK(!d_node
->isNull())
2135 << "Expecting a non-null internal expression. This Op is not indexed.";
2136 Kind k
= intToExtKind(d_node
->getKind());
2137 CVC5_API_CHECK(k
== DIVISIBLE
) << "Can't get string index from"
2138 << " kind " << kindToString(k
);
2139 //////// all checks before this line
2140 return d_node
->getConst
<Divisible
>().k
.toString();
2142 CVC5_API_TRY_CATCH_END
;
2146 uint32_t Op::getIndices() const
2148 CVC5_API_TRY_CATCH_BEGIN
;
2149 CVC5_API_CHECK_NOT_NULL
;
2150 CVC5_API_CHECK(!d_node
->isNull())
2151 << "Expecting a non-null internal expression. This Op is not indexed.";
2152 //////// all checks before this line
2155 Kind k
= intToExtKind(d_node
->getKind());
2158 case BITVECTOR_REPEAT
:
2159 i
= d_node
->getConst
<BitVectorRepeat
>().d_repeatAmount
;
2161 case BITVECTOR_ZERO_EXTEND
:
2162 i
= d_node
->getConst
<BitVectorZeroExtend
>().d_zeroExtendAmount
;
2164 case BITVECTOR_SIGN_EXTEND
:
2165 i
= d_node
->getConst
<BitVectorSignExtend
>().d_signExtendAmount
;
2167 case BITVECTOR_ROTATE_LEFT
:
2168 i
= d_node
->getConst
<BitVectorRotateLeft
>().d_rotateLeftAmount
;
2170 case BITVECTOR_ROTATE_RIGHT
:
2171 i
= d_node
->getConst
<BitVectorRotateRight
>().d_rotateRightAmount
;
2173 case INT_TO_BITVECTOR
: i
= d_node
->getConst
<IntToBitVector
>().d_size
; break;
2174 case IAND
: i
= d_node
->getConst
<IntAnd
>().d_size
; break;
2175 case FLOATINGPOINT_TO_UBV
:
2176 i
= d_node
->getConst
<FloatingPointToUBV
>().d_bv_size
.d_size
;
2178 case FLOATINGPOINT_TO_SBV
:
2179 i
= d_node
->getConst
<FloatingPointToSBV
>().d_bv_size
.d_size
;
2182 i
= d_node
->getConst
<RegExpRepeat
>().d_repeatAmount
;
2185 CVC5_API_CHECK(false) << "Can't get uint32_t index from"
2186 << " kind " << kindToString(k
);
2190 CVC5_API_TRY_CATCH_END
;
2194 std::pair
<uint32_t, uint32_t> Op::getIndices() const
2196 CVC5_API_TRY_CATCH_BEGIN
;
2197 CVC5_API_CHECK_NOT_NULL
;
2198 CVC5_API_CHECK(!d_node
->isNull())
2199 << "Expecting a non-null internal expression. This Op is not indexed.";
2200 //////// all checks before this line
2202 std::pair
<uint32_t, uint32_t> indices
;
2203 Kind k
= intToExtKind(d_node
->getKind());
2205 // using if/else instead of case statement because want local variables
2206 if (k
== BITVECTOR_EXTRACT
)
2208 cvc5::BitVectorExtract ext
= d_node
->getConst
<BitVectorExtract
>();
2209 indices
= std::make_pair(ext
.d_high
, ext
.d_low
);
2211 else if (k
== FLOATINGPOINT_TO_FP_IEEE_BITVECTOR
)
2213 cvc5::FloatingPointToFPIEEEBitVector ext
=
2214 d_node
->getConst
<FloatingPointToFPIEEEBitVector
>();
2215 indices
= std::make_pair(ext
.getSize().exponentWidth(),
2216 ext
.getSize().significandWidth());
2218 else if (k
== FLOATINGPOINT_TO_FP_FLOATINGPOINT
)
2220 cvc5::FloatingPointToFPFloatingPoint ext
=
2221 d_node
->getConst
<FloatingPointToFPFloatingPoint
>();
2222 indices
= std::make_pair(ext
.getSize().exponentWidth(),
2223 ext
.getSize().significandWidth());
2225 else if (k
== FLOATINGPOINT_TO_FP_REAL
)
2227 cvc5::FloatingPointToFPReal ext
= d_node
->getConst
<FloatingPointToFPReal
>();
2228 indices
= std::make_pair(ext
.getSize().exponentWidth(),
2229 ext
.getSize().significandWidth());
2231 else if (k
== FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR
)
2233 cvc5::FloatingPointToFPSignedBitVector ext
=
2234 d_node
->getConst
<FloatingPointToFPSignedBitVector
>();
2235 indices
= std::make_pair(ext
.getSize().exponentWidth(),
2236 ext
.getSize().significandWidth());
2238 else if (k
== FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR
)
2240 cvc5::FloatingPointToFPUnsignedBitVector ext
=
2241 d_node
->getConst
<FloatingPointToFPUnsignedBitVector
>();
2242 indices
= std::make_pair(ext
.getSize().exponentWidth(),
2243 ext
.getSize().significandWidth());
2245 else if (k
== FLOATINGPOINT_TO_FP_GENERIC
)
2247 cvc5::FloatingPointToFPGeneric ext
=
2248 d_node
->getConst
<FloatingPointToFPGeneric
>();
2249 indices
= std::make_pair(ext
.getSize().exponentWidth(),
2250 ext
.getSize().significandWidth());
2252 else if (k
== REGEXP_LOOP
)
2254 cvc5::RegExpLoop ext
= d_node
->getConst
<RegExpLoop
>();
2255 indices
= std::make_pair(ext
.d_loopMinOcc
, ext
.d_loopMaxOcc
);
2259 CVC5_API_CHECK(false) << "Can't get pair<uint32_t, uint32_t> indices from"
2260 << " kind " << kindToString(k
);
2264 CVC5_API_TRY_CATCH_END
;
2268 std::vector
<api::Term
> Op::getIndices() const
2270 CVC5_API_TRY_CATCH_BEGIN
;
2271 CVC5_API_CHECK_NOT_NULL
;
2272 CVC5_API_CHECK(!d_node
->isNull())
2273 << "Expecting a non-null internal expression. This Op is not indexed.";
2274 size_t size
= getNumIndicesHelper();
2275 std::vector
<Term
> terms(getNumIndices());
2276 for (size_t i
= 0; i
< size
; i
++)
2278 terms
[i
] = getIndexHelper(i
);
2280 //////// all checks before this line
2283 CVC5_API_TRY_CATCH_END
;
2286 std::string
Op::toString() const
2288 CVC5_API_TRY_CATCH_BEGIN
;
2289 //////// all checks before this line
2290 if (d_node
->isNull())
2292 return kindToString(d_kind
);
2296 CVC5_API_CHECK(!d_node
->isNull())
2297 << "Expecting a non-null internal expression";
2298 if (d_solver
!= nullptr)
2300 return d_node
->toString();
2302 return d_node
->toString();
2305 CVC5_API_TRY_CATCH_END
;
2308 std::ostream
& operator<<(std::ostream
& out
, const Op
& t
)
2310 out
<< t
.toString();
2315 /* -------------------------------------------------------------------------- */
2317 /* Split out to avoid nested API calls (problematic with API tracing). */
2318 /* .......................................................................... */
2320 bool Op::isNullHelper() const
2322 return (d_node
->isNull() && (d_kind
== NULL_EXPR
));
2325 bool Op::isIndexedHelper() const { return !d_node
->isNull(); }
2327 /* -------------------------------------------------------------------------- */
2329 /* -------------------------------------------------------------------------- */
2331 Term::Term() : d_solver(nullptr), d_node(new cvc5::Node()) {}
2333 Term::Term(const Solver
* slv
, const cvc5::Node
& n
) : d_solver(slv
)
2335 d_node
.reset(new cvc5::Node(n
));
2340 if (d_solver
!= nullptr)
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 bool Term::operator>(const Term
& t
) const
2375 CVC5_API_TRY_CATCH_BEGIN
;
2376 //////// all checks before this line
2377 return *d_node
> *t
.d_node
;
2379 CVC5_API_TRY_CATCH_END
;
2382 bool Term::operator<=(const Term
& t
) const
2384 CVC5_API_TRY_CATCH_BEGIN
;
2385 //////// all checks before this line
2386 return *d_node
<= *t
.d_node
;
2388 CVC5_API_TRY_CATCH_END
;
2391 bool Term::operator>=(const Term
& t
) const
2393 CVC5_API_TRY_CATCH_BEGIN
;
2394 //////// all checks before this line
2395 return *d_node
>= *t
.d_node
;
2397 CVC5_API_TRY_CATCH_END
;
2400 size_t Term::getNumChildren() const
2402 CVC5_API_TRY_CATCH_BEGIN
;
2403 CVC5_API_CHECK_NOT_NULL
;
2404 //////// all checks before this line
2406 // special case for apply kinds
2407 if (isApplyKind(d_node
->getKind()))
2409 return d_node
->getNumChildren() + 1;
2415 return d_node
->getNumChildren();
2417 CVC5_API_TRY_CATCH_END
;
2420 Term
Term::operator[](size_t index
) const
2422 CVC5_API_TRY_CATCH_BEGIN
;
2423 CVC5_API_CHECK_NOT_NULL
;
2424 CVC5_API_CHECK(index
< getNumChildren()) << "index out of bound";
2425 CVC5_API_CHECK(!isApplyKind(d_node
->getKind()) || d_node
->hasOperator())
2426 << "Expected apply kind to have operator when accessing child of Term";
2427 //////// all checks before this line
2429 // special cases for apply kinds
2430 if (isApplyKind(d_node
->getKind()))
2434 // return the operator
2435 return Term(d_solver
, d_node
->getOperator());
2442 // otherwise we are looking up child at (index-1)
2443 return Term(d_solver
, (*d_node
)[index
]);
2445 CVC5_API_TRY_CATCH_END
;
2448 uint64_t Term::getId() const
2450 CVC5_API_TRY_CATCH_BEGIN
;
2451 CVC5_API_CHECK_NOT_NULL
;
2452 //////// all checks before this line
2453 return d_node
->getId();
2455 CVC5_API_TRY_CATCH_END
;
2458 Kind
Term::getKind() const
2460 CVC5_API_TRY_CATCH_BEGIN
;
2461 CVC5_API_CHECK_NOT_NULL
;
2462 //////// all checks before this line
2463 return getKindHelper();
2465 CVC5_API_TRY_CATCH_END
;
2468 Sort
Term::getSort() const
2470 CVC5_API_TRY_CATCH_BEGIN
;
2471 CVC5_API_CHECK_NOT_NULL
;
2472 //////// all checks before this line
2473 return Sort(d_solver
, d_node
->getType());
2475 CVC5_API_TRY_CATCH_END
;
2478 Term
Term::substitute(const Term
& term
, const Term
& replacement
) const
2480 CVC5_API_TRY_CATCH_BEGIN
;
2481 CVC5_API_CHECK_NOT_NULL
;
2482 CVC5_API_CHECK_TERM(term
);
2483 CVC5_API_CHECK_TERM(replacement
);
2484 CVC5_API_CHECK(term
.getSort().isComparableTo(replacement
.getSort()))
2485 << "Expecting terms of comparable sort in substitute";
2486 //////// all checks before this line
2489 d_node
->substitute(TNode(*term
.d_node
), TNode(*replacement
.d_node
)));
2491 CVC5_API_TRY_CATCH_END
;
2494 Term
Term::substitute(const std::vector
<Term
>& terms
,
2495 const std::vector
<Term
>& replacements
) const
2497 CVC5_API_TRY_CATCH_BEGIN
;
2498 CVC5_API_CHECK_NOT_NULL
;
2499 CVC5_API_CHECK(terms
.size() == replacements
.size())
2500 << "Expecting vectors of the same arity in substitute";
2501 CVC5_API_TERM_CHECK_TERMS_WITH_TERMS_COMPARABLE_TO(terms
, replacements
);
2502 //////// all checks before this line
2503 std::vector
<Node
> nodes
= Term::termVectorToNodes(terms
);
2504 std::vector
<Node
> nodeReplacements
= Term::termVectorToNodes(replacements
);
2505 return Term(d_solver
,
2506 d_node
->substitute(nodes
.begin(),
2508 nodeReplacements
.begin(),
2509 nodeReplacements
.end()));
2511 CVC5_API_TRY_CATCH_END
;
2514 bool Term::hasOp() const
2516 CVC5_API_TRY_CATCH_BEGIN
;
2517 CVC5_API_CHECK_NOT_NULL
;
2518 //////// all checks before this line
2519 return d_node
->hasOperator();
2521 CVC5_API_TRY_CATCH_END
;
2524 Op
Term::getOp() const
2526 CVC5_API_TRY_CATCH_BEGIN
;
2527 CVC5_API_CHECK_NOT_NULL
;
2528 CVC5_API_CHECK(d_node
->hasOperator())
2529 << "Expecting Term to have an Op when calling getOp()";
2530 //////// all checks before this line
2532 // special cases for parameterized operators that are not indexed operators
2533 // the API level differs from the internal structure
2534 // indexed operators are stored in Ops
2535 // whereas functions and datatype operators are terms, and the Op
2536 // is one of the APPLY_* kinds
2537 if (isApplyKind(d_node
->getKind()))
2539 return Op(d_solver
, intToExtKind(d_node
->getKind()));
2541 else if (d_node
->getMetaKind() == kind::metakind::PARAMETERIZED
)
2543 // it's an indexed operator
2544 // so we should return the indexed op
2545 cvc5::Node op
= d_node
->getOperator();
2546 return Op(d_solver
, intToExtKind(d_node
->getKind()), op
);
2548 // Notice this is the only case where getKindHelper is used, since the
2549 // cases above do not have special cases for intToExtKind.
2550 return Op(d_solver
, getKindHelper());
2552 CVC5_API_TRY_CATCH_END
;
2555 bool Term::hasSymbol() const
2557 CVC5_API_TRY_CATCH_BEGIN
;
2558 CVC5_API_CHECK_NOT_NULL
;
2559 //////// all checks before this line
2560 return d_node
->hasAttribute(expr::VarNameAttr());
2562 CVC5_API_TRY_CATCH_END
;
2565 std::string
Term::getSymbol() const
2567 CVC5_API_TRY_CATCH_BEGIN
;
2568 CVC5_API_CHECK_NOT_NULL
;
2569 CVC5_API_CHECK(d_node
->hasAttribute(expr::VarNameAttr()))
2570 << "Invalid call to '" << __PRETTY_FUNCTION__
2571 << "', expected the term to have a symbol.";
2572 //////// all checks before this line
2573 return d_node
->getAttribute(expr::VarNameAttr());
2575 CVC5_API_TRY_CATCH_END
;
2578 bool Term::isNull() const
2580 CVC5_API_TRY_CATCH_BEGIN
;
2581 //////// all checks before this line
2582 return isNullHelper();
2584 CVC5_API_TRY_CATCH_END
;
2587 Term
Term::notTerm() const
2589 CVC5_API_TRY_CATCH_BEGIN
;
2590 CVC5_API_CHECK_NOT_NULL
;
2591 //////// all checks before this line
2592 Node res
= d_node
->notNode();
2593 (void)res
.getType(true); /* kick off type checking */
2594 return Term(d_solver
, res
);
2596 CVC5_API_TRY_CATCH_END
;
2599 Term
Term::andTerm(const Term
& t
) const
2601 CVC5_API_TRY_CATCH_BEGIN
;
2602 CVC5_API_CHECK_NOT_NULL
;
2603 CVC5_API_CHECK_TERM(t
);
2604 //////// all checks before this line
2605 Node res
= d_node
->andNode(*t
.d_node
);
2606 (void)res
.getType(true); /* kick off type checking */
2607 return Term(d_solver
, res
);
2609 CVC5_API_TRY_CATCH_END
;
2612 Term
Term::orTerm(const Term
& t
) const
2614 CVC5_API_TRY_CATCH_BEGIN
;
2615 CVC5_API_CHECK_NOT_NULL
;
2616 CVC5_API_CHECK_TERM(t
);
2617 //////// all checks before this line
2618 Node res
= d_node
->orNode(*t
.d_node
);
2619 (void)res
.getType(true); /* kick off type checking */
2620 return Term(d_solver
, res
);
2622 CVC5_API_TRY_CATCH_END
;
2625 Term
Term::xorTerm(const Term
& t
) const
2627 CVC5_API_TRY_CATCH_BEGIN
;
2628 CVC5_API_CHECK_NOT_NULL
;
2629 CVC5_API_CHECK_TERM(t
);
2630 //////// all checks before this line
2631 Node res
= d_node
->xorNode(*t
.d_node
);
2632 (void)res
.getType(true); /* kick off type checking */
2633 return Term(d_solver
, res
);
2635 CVC5_API_TRY_CATCH_END
;
2638 Term
Term::eqTerm(const Term
& t
) const
2640 CVC5_API_TRY_CATCH_BEGIN
;
2641 CVC5_API_CHECK_NOT_NULL
;
2642 CVC5_API_CHECK_TERM(t
);
2643 //////// all checks before this line
2644 Node res
= d_node
->eqNode(*t
.d_node
);
2645 (void)res
.getType(true); /* kick off type checking */
2646 return Term(d_solver
, res
);
2648 CVC5_API_TRY_CATCH_END
;
2651 Term
Term::impTerm(const Term
& t
) const
2653 CVC5_API_TRY_CATCH_BEGIN
;
2654 CVC5_API_CHECK_NOT_NULL
;
2655 CVC5_API_CHECK_TERM(t
);
2656 //////// all checks before this line
2657 Node res
= d_node
->impNode(*t
.d_node
);
2658 (void)res
.getType(true); /* kick off type checking */
2659 return Term(d_solver
, res
);
2661 CVC5_API_TRY_CATCH_END
;
2664 Term
Term::iteTerm(const Term
& then_t
, const Term
& else_t
) const
2666 CVC5_API_TRY_CATCH_BEGIN
;
2667 CVC5_API_CHECK_NOT_NULL
;
2668 CVC5_API_CHECK_TERM(then_t
);
2669 CVC5_API_CHECK_TERM(else_t
);
2670 //////// all checks before this line
2671 Node res
= d_node
->iteNode(*then_t
.d_node
, *else_t
.d_node
);
2672 (void)res
.getType(true); /* kick off type checking */
2673 return Term(d_solver
, res
);
2675 CVC5_API_TRY_CATCH_END
;
2678 std::string
Term::toString() const
2680 CVC5_API_TRY_CATCH_BEGIN
;
2681 //////// all checks before this line
2682 if (d_solver
!= nullptr)
2684 return d_node
->toString();
2686 return d_node
->toString();
2688 CVC5_API_TRY_CATCH_END
;
2691 Term::const_iterator::const_iterator()
2692 : d_solver(nullptr), d_origNode(nullptr), d_pos(0)
2696 Term::const_iterator::const_iterator(const Solver
* slv
,
2697 const std::shared_ptr
<cvc5::Node
>& n
,
2699 : d_solver(slv
), d_origNode(n
), d_pos(p
)
2703 Term::const_iterator::const_iterator(const const_iterator
& it
)
2704 : d_solver(nullptr), d_origNode(nullptr)
2706 if (it
.d_origNode
!= nullptr)
2708 d_solver
= it
.d_solver
;
2709 d_origNode
= it
.d_origNode
;
2714 Term::const_iterator
& Term::const_iterator::operator=(const const_iterator
& it
)
2716 d_solver
= it
.d_solver
;
2717 d_origNode
= it
.d_origNode
;
2722 bool Term::const_iterator::operator==(const const_iterator
& it
) const
2724 if (d_origNode
== nullptr || it
.d_origNode
== nullptr)
2728 return (d_solver
== it
.d_solver
&& *d_origNode
== *it
.d_origNode
)
2729 && (d_pos
== it
.d_pos
);
2732 bool Term::const_iterator::operator!=(const const_iterator
& it
) const
2734 return !(*this == it
);
2737 Term::const_iterator
& Term::const_iterator::operator++()
2739 Assert(d_origNode
!= nullptr);
2744 Term::const_iterator
Term::const_iterator::operator++(int)
2746 Assert(d_origNode
!= nullptr);
2747 const_iterator it
= *this;
2752 Term
Term::const_iterator::operator*() const
2754 Assert(d_origNode
!= nullptr);
2755 // this term has an extra child (mismatch between API and internal structure)
2756 // the extra child will be the first child
2757 bool extra_child
= isApplyKind(d_origNode
->getKind());
2759 if (!d_pos
&& extra_child
)
2761 return Term(d_solver
, d_origNode
->getOperator());
2765 uint32_t idx
= d_pos
;
2772 return Term(d_solver
, (*d_origNode
)[idx
]);
2776 Term::const_iterator
Term::begin() const
2778 return Term::const_iterator(d_solver
, d_node
, 0);
2781 Term::const_iterator
Term::end() const
2783 int endpos
= d_node
->getNumChildren();
2784 // special cases for APPLY_*
2785 // the API differs from the internal structure
2786 // the API takes a "higher-order" perspective and the applied
2787 // function or datatype constructor/selector/tester is a Term
2788 // which means it needs to be one of the children, even though
2789 // internally it is not
2790 if (isApplyKind(d_node
->getKind()))
2792 // one more child if this is a UF application (count the UF as a child)
2795 return Term::const_iterator(d_solver
, d_node
, endpos
);
2798 const cvc5::Node
& Term::getNode(void) const { return *d_node
; }
2801 const Rational
& getRational(const cvc5::Node
& node
)
2803 switch (node
.getKind())
2805 case cvc5::Kind::CAST_TO_REAL
: return node
[0].getConst
<Rational
>();
2806 case cvc5::Kind::CONST_RATIONAL
: return node
.getConst
<Rational
>();
2808 CVC5_API_CHECK(false) << "Node is not a rational.";
2809 return node
.getConst
<Rational
>();
2812 Integer
getInteger(const cvc5::Node
& node
)
2814 return node
.getConst
<Rational
>().getNumerator();
2816 template <typename T
>
2817 bool checkIntegerBounds(const Integer
& i
)
2819 return i
>= std::numeric_limits
<T
>::min()
2820 && i
<= std::numeric_limits
<T
>::max();
2822 bool checkReal32Bounds(const Rational
& r
)
2824 return checkIntegerBounds
<std::int32_t>(r
.getNumerator())
2825 && checkIntegerBounds
<std::uint32_t>(r
.getDenominator());
2827 bool checkReal64Bounds(const Rational
& r
)
2829 return checkIntegerBounds
<std::int64_t>(r
.getNumerator())
2830 && checkIntegerBounds
<std::uint64_t>(r
.getDenominator());
2833 bool isReal(const Node
& node
)
2835 return node
.getKind() == cvc5::Kind::CONST_RATIONAL
2836 || node
.getKind() == cvc5::Kind::CAST_TO_REAL
;
2838 bool isReal32(const Node
& node
)
2840 return isReal(node
) && checkReal32Bounds(getRational(node
));
2842 bool isReal64(const Node
& node
)
2844 return isReal(node
) && checkReal64Bounds(getRational(node
));
2847 bool isInteger(const Node
& node
)
2849 return node
.getKind() == cvc5::Kind::CONST_RATIONAL
2850 && node
.getConst
<Rational
>().isIntegral();
2852 bool isInt32(const Node
& node
)
2854 return isInteger(node
) && checkIntegerBounds
<std::int32_t>(getInteger(node
));
2856 bool isUInt32(const Node
& node
)
2858 return isInteger(node
) && checkIntegerBounds
<std::uint32_t>(getInteger(node
));
2860 bool isInt64(const Node
& node
)
2862 return isInteger(node
) && checkIntegerBounds
<std::int64_t>(getInteger(node
));
2864 bool isUInt64(const Node
& node
)
2866 return isInteger(node
) && checkIntegerBounds
<std::uint64_t>(getInteger(node
));
2868 } // namespace detail
2870 int32_t Term::getRealOrIntegerValueSign() const
2872 CVC5_API_TRY_CATCH_BEGIN
;
2873 CVC5_API_CHECK_NOT_NULL
;
2874 //////// all checks before this line
2875 const Rational
& r
= detail::getRational(*d_node
);
2876 return static_cast<int32_t>(r
.sgn());
2878 CVC5_API_TRY_CATCH_END
;
2881 bool Term::isInt32Value() const
2883 CVC5_API_TRY_CATCH_BEGIN
;
2884 CVC5_API_CHECK_NOT_NULL
;
2885 //////// all checks before this line
2886 return detail::isInt32(*d_node
);
2888 CVC5_API_TRY_CATCH_END
;
2891 std::int32_t Term::getInt32Value() const
2893 CVC5_API_TRY_CATCH_BEGIN
;
2894 CVC5_API_CHECK_NOT_NULL
;
2895 CVC5_API_ARG_CHECK_EXPECTED(detail::isInt32(*d_node
), *d_node
)
2896 << "Term to be a 32-bit integer value when calling getInt32Value()";
2897 //////// all checks before this line
2898 return detail::getInteger(*d_node
).getSignedInt();
2900 CVC5_API_TRY_CATCH_END
;
2903 bool Term::isUInt32Value() const
2905 CVC5_API_TRY_CATCH_BEGIN
;
2906 CVC5_API_CHECK_NOT_NULL
;
2907 //////// all checks before this line
2908 return detail::isUInt32(*d_node
);
2910 CVC5_API_TRY_CATCH_END
;
2912 std::uint32_t Term::getUInt32Value() const
2914 CVC5_API_TRY_CATCH_BEGIN
;
2915 CVC5_API_CHECK_NOT_NULL
;
2916 CVC5_API_ARG_CHECK_EXPECTED(detail::isUInt32(*d_node
), *d_node
)
2917 << "Term to be a unsigned 32-bit integer value when calling "
2919 //////// all checks before this line
2920 return detail::getInteger(*d_node
).getUnsignedInt();
2922 CVC5_API_TRY_CATCH_END
;
2925 bool Term::isInt64Value() const
2927 CVC5_API_TRY_CATCH_BEGIN
;
2928 CVC5_API_CHECK_NOT_NULL
;
2929 //////// all checks before this line
2930 return detail::isInt64(*d_node
);
2932 CVC5_API_TRY_CATCH_END
;
2934 std::int64_t Term::getInt64Value() const
2936 CVC5_API_TRY_CATCH_BEGIN
;
2937 CVC5_API_CHECK_NOT_NULL
;
2938 CVC5_API_ARG_CHECK_EXPECTED(detail::isInt64(*d_node
), *d_node
)
2939 << "Term to be a 64-bit integer value when calling getInt64Value()";
2940 //////// all checks before this line
2941 return detail::getInteger(*d_node
).getSigned64();
2943 CVC5_API_TRY_CATCH_END
;
2946 bool Term::isUInt64Value() const
2948 CVC5_API_TRY_CATCH_BEGIN
;
2949 CVC5_API_CHECK_NOT_NULL
;
2950 //////// all checks before this line
2951 return detail::isUInt64(*d_node
);
2953 CVC5_API_TRY_CATCH_END
;
2956 std::uint64_t Term::getUInt64Value() const
2958 CVC5_API_TRY_CATCH_BEGIN
;
2959 CVC5_API_CHECK_NOT_NULL
;
2960 CVC5_API_ARG_CHECK_EXPECTED(detail::isUInt64(*d_node
), *d_node
)
2961 << "Term to be a unsigned 64-bit integer value when calling "
2963 //////// all checks before this line
2964 return detail::getInteger(*d_node
).getUnsigned64();
2966 CVC5_API_TRY_CATCH_END
;
2969 bool Term::isIntegerValue() const
2971 CVC5_API_TRY_CATCH_BEGIN
;
2972 CVC5_API_CHECK_NOT_NULL
;
2973 //////// all checks before this line
2974 return detail::isInteger(*d_node
);
2976 CVC5_API_TRY_CATCH_END
;
2978 std::string
Term::getIntegerValue() const
2980 CVC5_API_TRY_CATCH_BEGIN
;
2981 CVC5_API_CHECK_NOT_NULL
;
2982 CVC5_API_ARG_CHECK_EXPECTED(detail::isInteger(*d_node
), *d_node
)
2983 << "Term to be an integer value when calling getIntegerValue()";
2984 //////// all checks before this line
2985 return detail::getInteger(*d_node
).toString();
2987 CVC5_API_TRY_CATCH_END
;
2990 bool Term::isStringValue() const
2992 CVC5_API_TRY_CATCH_BEGIN
;
2993 CVC5_API_CHECK_NOT_NULL
;
2994 //////// all checks before this line
2995 return d_node
->getKind() == cvc5::Kind::CONST_STRING
;
2997 CVC5_API_TRY_CATCH_END
;
3000 std::wstring
Term::getStringValue() const
3002 CVC5_API_TRY_CATCH_BEGIN
;
3003 CVC5_API_CHECK_NOT_NULL
;
3004 CVC5_API_ARG_CHECK_EXPECTED(d_node
->getKind() == cvc5::Kind::CONST_STRING
,
3006 << "Term to be a string value when calling getStringValue()";
3007 //////// all checks before this line
3008 return d_node
->getConst
<cvc5::String
>().toWString();
3010 CVC5_API_TRY_CATCH_END
;
3013 std::vector
<Node
> Term::termVectorToNodes(const std::vector
<Term
>& terms
)
3015 std::vector
<Node
> res
;
3016 for (const Term
& t
: terms
)
3018 res
.push_back(t
.getNode());
3023 bool Term::isReal32Value() const
3025 CVC5_API_TRY_CATCH_BEGIN
;
3026 CVC5_API_CHECK_NOT_NULL
;
3027 //////// all checks before this line
3028 return detail::isReal32(*d_node
);
3030 CVC5_API_TRY_CATCH_END
;
3032 std::pair
<std::int32_t, std::uint32_t> Term::getReal32Value() const
3034 CVC5_API_TRY_CATCH_BEGIN
;
3035 CVC5_API_CHECK_NOT_NULL
;
3036 CVC5_API_ARG_CHECK_EXPECTED(detail::isReal32(*d_node
), *d_node
)
3037 << "Term to be a 32-bit rational value when calling getReal32Value()";
3038 //////// all checks before this line
3039 const Rational
& r
= detail::getRational(*d_node
);
3040 return std::make_pair(r
.getNumerator().getSignedInt(),
3041 r
.getDenominator().getUnsignedInt());
3043 CVC5_API_TRY_CATCH_END
;
3045 bool Term::isReal64Value() const
3047 CVC5_API_TRY_CATCH_BEGIN
;
3048 CVC5_API_CHECK_NOT_NULL
;
3049 //////// all checks before this line
3050 return detail::isReal64(*d_node
);
3052 CVC5_API_TRY_CATCH_END
;
3054 std::pair
<std::int64_t, std::uint64_t> Term::getReal64Value() const
3056 CVC5_API_TRY_CATCH_BEGIN
;
3057 CVC5_API_CHECK_NOT_NULL
;
3058 CVC5_API_ARG_CHECK_EXPECTED(detail::isReal64(*d_node
), *d_node
)
3059 << "Term to be a 64-bit rational value when calling getReal64Value()";
3060 //////// all checks before this line
3061 const Rational
& r
= detail::getRational(*d_node
);
3062 return std::make_pair(r
.getNumerator().getSigned64(),
3063 r
.getDenominator().getUnsigned64());
3065 CVC5_API_TRY_CATCH_END
;
3067 bool Term::isRealValue() const
3069 CVC5_API_TRY_CATCH_BEGIN
;
3070 CVC5_API_CHECK_NOT_NULL
;
3071 //////// all checks before this line
3072 return detail::isReal(*d_node
);
3074 CVC5_API_TRY_CATCH_END
;
3076 std::string
Term::getRealValue() const
3078 CVC5_API_TRY_CATCH_BEGIN
;
3079 CVC5_API_CHECK_NOT_NULL
;
3080 CVC5_API_ARG_CHECK_EXPECTED(detail::isReal(*d_node
), *d_node
)
3081 << "Term to be a rational value when calling getRealValue()";
3082 //////// all checks before this line
3083 const Rational
& rat
= detail::getRational(*d_node
);
3084 std::string res
= rat
.toString();
3085 if (rat
.isIntegral())
3091 CVC5_API_TRY_CATCH_END
;
3094 bool Term::isConstArray() const
3096 CVC5_API_TRY_CATCH_BEGIN
;
3097 CVC5_API_CHECK_NOT_NULL
;
3098 //////// all checks before this line
3099 return d_node
->getKind() == cvc5::Kind::STORE_ALL
;
3101 CVC5_API_TRY_CATCH_END
;
3103 Term
Term::getConstArrayBase() const
3105 CVC5_API_TRY_CATCH_BEGIN
;
3106 CVC5_API_CHECK_NOT_NULL
;
3107 CVC5_API_ARG_CHECK_EXPECTED(d_node
->getKind() == cvc5::Kind::STORE_ALL
,
3109 << "Term to be a constant array when calling getConstArrayBase()";
3110 //////// all checks before this line
3111 const auto& ar
= d_node
->getConst
<ArrayStoreAll
>();
3112 return Term(d_solver
, ar
.getValue());
3114 CVC5_API_TRY_CATCH_END
;
3117 bool Term::isBooleanValue() const
3119 CVC5_API_TRY_CATCH_BEGIN
;
3120 CVC5_API_CHECK_NOT_NULL
;
3121 //////// all checks before this line
3122 return d_node
->getKind() == cvc5::Kind::CONST_BOOLEAN
;
3124 CVC5_API_TRY_CATCH_END
;
3126 bool Term::getBooleanValue() const
3128 CVC5_API_TRY_CATCH_BEGIN
;
3129 CVC5_API_CHECK_NOT_NULL
;
3130 CVC5_API_ARG_CHECK_EXPECTED(d_node
->getKind() == cvc5::Kind::CONST_BOOLEAN
,
3132 << "Term to be a Boolean value when calling getBooleanValue()";
3133 //////// all checks before this line
3134 return d_node
->getConst
<bool>();
3136 CVC5_API_TRY_CATCH_END
;
3139 bool Term::isBitVectorValue() const
3141 CVC5_API_TRY_CATCH_BEGIN
;
3142 CVC5_API_CHECK_NOT_NULL
;
3143 //////// all checks before this line
3144 return d_node
->getKind() == cvc5::Kind::CONST_BITVECTOR
;
3146 CVC5_API_TRY_CATCH_END
;
3148 std::string
Term::getBitVectorValue(std::uint32_t base
) const
3150 CVC5_API_TRY_CATCH_BEGIN
;
3151 CVC5_API_CHECK_NOT_NULL
;
3152 CVC5_API_ARG_CHECK_EXPECTED(d_node
->getKind() == cvc5::Kind::CONST_BITVECTOR
,
3154 << "Term to be a bit-vector value when calling getBitVectorValue()";
3155 //////// all checks before this line
3156 return d_node
->getConst
<BitVector
>().toString(base
);
3158 CVC5_API_TRY_CATCH_END
;
3161 bool Term::isAbstractValue() const
3163 CVC5_API_TRY_CATCH_BEGIN
;
3164 CVC5_API_CHECK_NOT_NULL
;
3165 //////// all checks before this line
3166 return d_node
->getKind() == cvc5::Kind::ABSTRACT_VALUE
;
3168 CVC5_API_TRY_CATCH_END
;
3170 std::string
Term::getAbstractValue() const
3172 CVC5_API_TRY_CATCH_BEGIN
;
3173 CVC5_API_CHECK_NOT_NULL
;
3174 CVC5_API_ARG_CHECK_EXPECTED(d_node
->getKind() == cvc5::Kind::ABSTRACT_VALUE
,
3176 << "Term to be an abstract value when calling "
3177 "getAbstractValue()";
3178 //////// all checks before this line
3179 return d_node
->getConst
<AbstractValue
>().getIndex().toString();
3181 CVC5_API_TRY_CATCH_END
;
3184 bool Term::isTupleValue() const
3186 CVC5_API_TRY_CATCH_BEGIN
;
3187 CVC5_API_CHECK_NOT_NULL
;
3188 //////// all checks before this line
3189 return d_node
->getKind() == cvc5::Kind::APPLY_CONSTRUCTOR
&& d_node
->isConst()
3190 && d_node
->getType().getDType().isTuple();
3192 CVC5_API_TRY_CATCH_END
;
3194 std::vector
<Term
> Term::getTupleValue() const
3196 CVC5_API_TRY_CATCH_BEGIN
;
3197 CVC5_API_CHECK_NOT_NULL
;
3198 CVC5_API_ARG_CHECK_EXPECTED(d_node
->getKind() == cvc5::Kind::APPLY_CONSTRUCTOR
3199 && d_node
->isConst()
3200 && d_node
->getType().getDType().isTuple(),
3202 << "Term to be a tuple value when calling getTupleValue()";
3203 //////// all checks before this line
3204 std::vector
<Term
> res
;
3205 for (size_t i
= 0, n
= d_node
->getNumChildren(); i
< n
; ++i
)
3207 res
.emplace_back(Term(d_solver
, (*d_node
)[i
]));
3211 CVC5_API_TRY_CATCH_END
;
3214 bool Term::isFloatingPointPosZero() const
3216 CVC5_API_TRY_CATCH_BEGIN
;
3217 CVC5_API_CHECK_NOT_NULL
;
3218 //////// all checks before this line
3219 if (d_node
->getKind() == cvc5::Kind::CONST_FLOATINGPOINT
)
3221 const auto& fp
= d_node
->getConst
<FloatingPoint
>();
3222 return fp
.isZero() && fp
.isPositive();
3226 CVC5_API_TRY_CATCH_END
;
3228 bool Term::isFloatingPointNegZero() const
3230 CVC5_API_TRY_CATCH_BEGIN
;
3231 CVC5_API_CHECK_NOT_NULL
;
3232 //////// all checks before this line
3233 if (d_node
->getKind() == cvc5::Kind::CONST_FLOATINGPOINT
)
3235 const auto& fp
= d_node
->getConst
<FloatingPoint
>();
3236 return fp
.isZero() && fp
.isNegative();
3240 CVC5_API_TRY_CATCH_END
;
3242 bool Term::isFloatingPointPosInf() const
3244 CVC5_API_TRY_CATCH_BEGIN
;
3245 CVC5_API_CHECK_NOT_NULL
;
3246 //////// all checks before this line
3247 if (d_node
->getKind() == cvc5::Kind::CONST_FLOATINGPOINT
)
3249 const auto& fp
= d_node
->getConst
<FloatingPoint
>();
3250 return fp
.isInfinite() && fp
.isPositive();
3254 CVC5_API_TRY_CATCH_END
;
3256 bool Term::isFloatingPointNegInf() const
3258 CVC5_API_TRY_CATCH_BEGIN
;
3259 CVC5_API_CHECK_NOT_NULL
;
3260 //////// all checks before this line
3261 if (d_node
->getKind() == cvc5::Kind::CONST_FLOATINGPOINT
)
3263 const auto& fp
= d_node
->getConst
<FloatingPoint
>();
3264 return fp
.isInfinite() && fp
.isNegative();
3268 CVC5_API_TRY_CATCH_END
;
3270 bool Term::isFloatingPointNaN() const
3272 CVC5_API_TRY_CATCH_BEGIN
;
3273 CVC5_API_CHECK_NOT_NULL
;
3274 //////// all checks before this line
3275 return d_node
->getKind() == cvc5::Kind::CONST_FLOATINGPOINT
3276 && d_node
->getConst
<FloatingPoint
>().isNaN();
3278 CVC5_API_TRY_CATCH_END
;
3280 bool Term::isFloatingPointValue() const
3282 CVC5_API_TRY_CATCH_BEGIN
;
3283 CVC5_API_CHECK_NOT_NULL
;
3284 //////// all checks before this line
3285 return d_node
->getKind() == cvc5::Kind::CONST_FLOATINGPOINT
;
3287 CVC5_API_TRY_CATCH_END
;
3289 std::tuple
<std::uint32_t, std::uint32_t, Term
> Term::getFloatingPointValue()
3292 CVC5_API_TRY_CATCH_BEGIN
;
3293 CVC5_API_CHECK_NOT_NULL
;
3294 CVC5_API_ARG_CHECK_EXPECTED(
3295 d_node
->getKind() == cvc5::Kind::CONST_FLOATINGPOINT
, *d_node
)
3296 << "Term to be a floating-point value when calling "
3297 "getFloatingPointValue()";
3298 //////// all checks before this line
3299 const auto& fp
= d_node
->getConst
<FloatingPoint
>();
3300 return std::make_tuple(fp
.getSize().exponentWidth(),
3301 fp
.getSize().significandWidth(),
3302 d_solver
->mkValHelper
<BitVector
>(fp
.pack()));
3304 CVC5_API_TRY_CATCH_END
;
3307 bool Term::isSetValue() const
3309 CVC5_API_TRY_CATCH_BEGIN
;
3310 CVC5_API_CHECK_NOT_NULL
;
3311 //////// all checks before this line
3312 return d_node
->getType().isSet() && d_node
->isConst();
3314 CVC5_API_TRY_CATCH_END
;
3317 void Term::collectSet(std::set
<Term
>& set
,
3318 const cvc5::Node
& node
,
3321 // We asserted that node has a set type, and node.isConst()
3322 // Thus, node only contains of SET_EMPTY, SET_UNION and SET_SINGLETON.
3323 switch (node
.getKind())
3325 case cvc5::Kind::SET_EMPTY
: break;
3326 case cvc5::Kind::SET_SINGLETON
: set
.emplace(Term(slv
, node
[0])); break;
3327 case cvc5::Kind::SET_UNION
:
3329 for (const auto& sub
: node
)
3331 collectSet(set
, sub
, slv
);
3336 CVC5_API_ARG_CHECK_EXPECTED(false, node
)
3337 << "Term to be a set value when calling getSetValue()";
3342 std::set
<Term
> Term::getSetValue() const
3344 CVC5_API_TRY_CATCH_BEGIN
;
3345 CVC5_API_CHECK_NOT_NULL
;
3346 CVC5_API_ARG_CHECK_EXPECTED(d_node
->getType().isSet() && d_node
->isConst(),
3348 << "Term to be a set value when calling getSetValue()";
3349 //////// all checks before this line
3351 Term::collectSet(res
, *d_node
, d_solver
);
3354 CVC5_API_TRY_CATCH_END
;
3357 bool Term::isSequenceValue() const
3359 CVC5_API_TRY_CATCH_BEGIN
;
3360 CVC5_API_CHECK_NOT_NULL
;
3361 //////// all checks before this line
3362 return d_node
->getKind() == cvc5::Kind::CONST_SEQUENCE
;
3364 CVC5_API_TRY_CATCH_END
;
3366 std::vector
<Term
> Term::getSequenceValue() const
3368 CVC5_API_TRY_CATCH_BEGIN
;
3369 CVC5_API_CHECK_NOT_NULL
;
3370 CVC5_API_ARG_CHECK_EXPECTED(d_node
->getKind() == cvc5::Kind::CONST_SEQUENCE
,
3372 << "Term to be a sequence value when calling getSequenceValue()";
3373 //////// all checks before this line
3374 std::vector
<Term
> res
;
3375 const Sequence
& seq
= d_node
->getConst
<Sequence
>();
3376 for (const auto& node
: seq
.getVec())
3378 res
.emplace_back(Term(d_solver
, node
));
3382 CVC5_API_TRY_CATCH_END
;
3385 bool Term::isUninterpretedValue() const
3387 CVC5_API_TRY_CATCH_BEGIN
;
3388 CVC5_API_CHECK_NOT_NULL
;
3389 //////// all checks before this line
3390 return d_node
->getKind() == cvc5::Kind::UNINTERPRETED_CONSTANT
;
3392 CVC5_API_TRY_CATCH_END
;
3394 std::pair
<Sort
, std::int32_t> Term::getUninterpretedValue() const
3396 CVC5_API_TRY_CATCH_BEGIN
;
3397 CVC5_API_CHECK_NOT_NULL
;
3398 CVC5_API_ARG_CHECK_EXPECTED(
3399 d_node
->getKind() == cvc5::Kind::UNINTERPRETED_CONSTANT
, *d_node
)
3400 << "Term to be an uninterpreted value when calling "
3401 "getUninterpretedValue()";
3402 //////// all checks before this line
3403 const auto& uc
= d_node
->getConst
<UninterpretedConstant
>();
3404 return std::make_pair(Sort(d_solver
, uc
.getType()),
3405 uc
.getIndex().toUnsignedInt());
3407 CVC5_API_TRY_CATCH_END
;
3410 std::ostream
& operator<<(std::ostream
& out
, const Term
& t
)
3412 out
<< t
.toString();
3416 std::ostream
& operator<<(std::ostream
& out
, const std::vector
<Term
>& vector
)
3418 container_to_stream(out
, vector
);
3422 std::ostream
& operator<<(std::ostream
& out
, const std::set
<Term
>& set
)
3424 container_to_stream(out
, set
);
3428 std::ostream
& operator<<(std::ostream
& out
,
3429 const std::unordered_set
<Term
>& unordered_set
)
3431 container_to_stream(out
, unordered_set
);
3435 template <typename V
>
3436 std::ostream
& operator<<(std::ostream
& out
, const std::map
<Term
, V
>& map
)
3438 container_to_stream(out
, map
);
3442 template <typename V
>
3443 std::ostream
& operator<<(std::ostream
& out
,
3444 const std::unordered_map
<Term
, V
>& unordered_map
)
3446 container_to_stream(out
, unordered_map
);
3451 /* -------------------------------------------------------------------------- */
3453 /* Split out to avoid nested API calls (problematic with API tracing). */
3454 /* .......................................................................... */
3456 bool Term::isNullHelper() const
3458 /* Split out to avoid nested API calls (problematic with API tracing). */
3459 return d_node
->isNull();
3462 Kind
Term::getKindHelper() const
3464 /* Sequence kinds do not exist internally, so we must convert their internal
3465 * (string) versions back to sequence. All operators where this is
3466 * necessary are such that their first child is of sequence type, which
3468 if (d_node
->getNumChildren() > 0 && (*d_node
)[0].getType().isSequence())
3470 switch (d_node
->getKind())
3472 case cvc5::Kind::STRING_CONCAT
: return SEQ_CONCAT
;
3473 case cvc5::Kind::STRING_LENGTH
: return SEQ_LENGTH
;
3474 case cvc5::Kind::STRING_SUBSTR
: return SEQ_EXTRACT
;
3475 case cvc5::Kind::STRING_UPDATE
: return SEQ_UPDATE
;
3476 case cvc5::Kind::STRING_CHARAT
: return SEQ_AT
;
3477 case cvc5::Kind::STRING_CONTAINS
: return SEQ_CONTAINS
;
3478 case cvc5::Kind::STRING_INDEXOF
: return SEQ_INDEXOF
;
3479 case cvc5::Kind::STRING_REPLACE
: return SEQ_REPLACE
;
3480 case cvc5::Kind::STRING_REPLACE_ALL
: return SEQ_REPLACE_ALL
;
3481 case cvc5::Kind::STRING_REV
: return SEQ_REV
;
3482 case cvc5::Kind::STRING_PREFIX
: return SEQ_PREFIX
;
3483 case cvc5::Kind::STRING_SUFFIX
: return SEQ_SUFFIX
;
3485 // fall through to conversion below
3489 // Notice that kinds like APPLY_TYPE_ASCRIPTION will be converted to
3493 return CONST_RATIONAL
;
3495 return intToExtKind(d_node
->getKind());
3498 bool Term::isCastedReal() const
3500 if (d_node
->getKind() == kind::CAST_TO_REAL
)
3502 return (*d_node
)[0].isConst() && (*d_node
)[0].getType().isInteger();
3507 /* -------------------------------------------------------------------------- */
3509 /* -------------------------------------------------------------------------- */
3511 /* DatatypeConstructorDecl -------------------------------------------------- */
3513 DatatypeConstructorDecl::DatatypeConstructorDecl()
3514 : d_solver(nullptr), d_ctor(nullptr)
3518 DatatypeConstructorDecl::DatatypeConstructorDecl(const Solver
* slv
,
3519 const std::string
& name
)
3520 : d_solver(slv
), d_ctor(new cvc5::DTypeConstructor(name
))
3523 DatatypeConstructorDecl::~DatatypeConstructorDecl()
3525 if (d_ctor
!= nullptr)
3531 void DatatypeConstructorDecl::addSelector(const std::string
& name
,
3534 CVC5_API_TRY_CATCH_BEGIN
;
3535 CVC5_API_CHECK_NOT_NULL
;
3536 CVC5_API_CHECK_SORT(sort
);
3537 CVC5_API_ARG_CHECK_EXPECTED(!sort
.isNull(), sort
)
3538 << "non-null codomain sort for selector";
3539 //////// all checks before this line
3540 d_ctor
->addArg(name
, *sort
.d_type
);
3542 CVC5_API_TRY_CATCH_END
;
3545 void DatatypeConstructorDecl::addSelectorSelf(const std::string
& name
)
3547 CVC5_API_TRY_CATCH_BEGIN
;
3548 CVC5_API_CHECK_NOT_NULL
;
3549 //////// all checks before this line
3550 d_ctor
->addArgSelf(name
);
3552 CVC5_API_TRY_CATCH_END
;
3555 bool DatatypeConstructorDecl::isNull() const
3557 CVC5_API_TRY_CATCH_BEGIN
;
3558 //////// all checks before this line
3559 return isNullHelper();
3561 CVC5_API_TRY_CATCH_END
;
3564 std::string
DatatypeConstructorDecl::toString() const
3566 CVC5_API_TRY_CATCH_BEGIN
;
3567 //////// all checks before this line
3568 std::stringstream ss
;
3572 CVC5_API_TRY_CATCH_END
;
3575 std::ostream
& operator<<(std::ostream
& out
,
3576 const DatatypeConstructorDecl
& ctordecl
)
3578 out
<< ctordecl
.toString();
3582 std::ostream
& operator<<(std::ostream
& out
,
3583 const std::vector
<DatatypeConstructorDecl
>& vector
)
3585 container_to_stream(out
, vector
);
3589 bool DatatypeConstructorDecl::isNullHelper() const { return d_ctor
== nullptr; }
3591 bool DatatypeConstructorDecl::isResolved() const
3593 return d_ctor
== nullptr || d_ctor
->isResolved();
3596 /* DatatypeDecl ------------------------------------------------------------- */
3598 DatatypeDecl::DatatypeDecl() : d_solver(nullptr), d_dtype(nullptr) {}
3600 DatatypeDecl::DatatypeDecl(const Solver
* slv
,
3601 const std::string
& name
,
3603 : d_solver(slv
), d_dtype(new cvc5::DType(name
, isCoDatatype
))
3607 DatatypeDecl::DatatypeDecl(const Solver
* slv
,
3608 const std::string
& name
,
3612 d_dtype(new cvc5::DType(
3613 name
, std::vector
<TypeNode
>{*param
.d_type
}, isCoDatatype
))
3617 DatatypeDecl::DatatypeDecl(const Solver
* slv
,
3618 const std::string
& name
,
3619 const std::vector
<Sort
>& params
,
3623 std::vector
<TypeNode
> tparams
= Sort::sortVectorToTypeNodes(params
);
3624 d_dtype
= std::shared_ptr
<cvc5::DType
>(
3625 new cvc5::DType(name
, tparams
, isCoDatatype
));
3628 bool DatatypeDecl::isNullHelper() const { return !d_dtype
; }
3630 DatatypeDecl::~DatatypeDecl()
3632 if (d_dtype
!= nullptr)
3638 void DatatypeDecl::addConstructor(const DatatypeConstructorDecl
& ctor
)
3640 CVC5_API_TRY_CATCH_BEGIN
;
3641 CVC5_API_CHECK_NOT_NULL
;
3642 CVC5_API_ARG_CHECK_NOT_NULL(ctor
);
3643 CVC5_API_ARG_CHECK_SOLVER("datatype constructor declaration", ctor
);
3644 //////// all checks before this line
3645 d_dtype
->addConstructor(ctor
.d_ctor
);
3647 CVC5_API_TRY_CATCH_END
;
3650 size_t DatatypeDecl::getNumConstructors() const
3652 CVC5_API_TRY_CATCH_BEGIN
;
3653 CVC5_API_CHECK_NOT_NULL
;
3654 //////// all checks before this line
3655 return d_dtype
->getNumConstructors();
3657 CVC5_API_TRY_CATCH_END
;
3660 bool DatatypeDecl::isParametric() const
3662 CVC5_API_TRY_CATCH_BEGIN
;
3663 CVC5_API_CHECK_NOT_NULL
;
3664 //////// all checks before this line
3665 return d_dtype
->isParametric();
3667 CVC5_API_TRY_CATCH_END
;
3670 std::string
DatatypeDecl::toString() const
3672 CVC5_API_TRY_CATCH_BEGIN
;
3673 CVC5_API_CHECK_NOT_NULL
;
3674 //////// all checks before this line
3675 std::stringstream ss
;
3679 CVC5_API_TRY_CATCH_END
;
3682 std::string
DatatypeDecl::getName() const
3684 CVC5_API_TRY_CATCH_BEGIN
;
3685 CVC5_API_CHECK_NOT_NULL
;
3686 //////// all checks before this line
3687 return d_dtype
->getName();
3689 CVC5_API_TRY_CATCH_END
;
3692 bool DatatypeDecl::isNull() const
3694 CVC5_API_TRY_CATCH_BEGIN
;
3695 //////// all checks before this line
3696 return isNullHelper();
3698 CVC5_API_TRY_CATCH_END
;
3701 std::ostream
& operator<<(std::ostream
& out
, const DatatypeDecl
& dtdecl
)
3703 out
<< dtdecl
.toString();
3707 cvc5::DType
& DatatypeDecl::getDatatype(void) const { return *d_dtype
; }
3709 /* DatatypeSelector --------------------------------------------------------- */
3711 DatatypeSelector::DatatypeSelector() : d_solver(nullptr), d_stor(nullptr) {}
3713 DatatypeSelector::DatatypeSelector(const Solver
* slv
,
3714 const cvc5::DTypeSelector
& stor
)
3715 : d_solver(slv
), d_stor(new cvc5::DTypeSelector(stor
))
3717 CVC5_API_CHECK(d_stor
->isResolved()) << "Expected resolved datatype selector";
3720 DatatypeSelector::~DatatypeSelector()
3722 if (d_stor
!= nullptr)
3728 std::string
DatatypeSelector::getName() const
3730 CVC5_API_TRY_CATCH_BEGIN
;
3731 CVC5_API_CHECK_NOT_NULL
;
3732 //////// all checks before this line
3733 return d_stor
->getName();
3735 CVC5_API_TRY_CATCH_END
;
3738 Term
DatatypeSelector::getSelectorTerm() const
3740 CVC5_API_TRY_CATCH_BEGIN
;
3741 CVC5_API_CHECK_NOT_NULL
;
3742 //////// all checks before this line
3743 return Term(d_solver
, d_stor
->getSelector());
3745 CVC5_API_TRY_CATCH_END
;
3747 Term
DatatypeSelector::getUpdaterTerm() const
3749 CVC5_API_TRY_CATCH_BEGIN
;
3750 CVC5_API_CHECK_NOT_NULL
;
3751 //////// all checks before this line
3752 return Term(d_solver
, d_stor
->getUpdater());
3754 CVC5_API_TRY_CATCH_END
;
3757 Sort
DatatypeSelector::getCodomainSort() const
3759 CVC5_API_TRY_CATCH_BEGIN
;
3760 CVC5_API_CHECK_NOT_NULL
;
3761 //////// all checks before this line
3762 return Sort(d_solver
, d_stor
->getRangeType());
3764 CVC5_API_TRY_CATCH_END
;
3767 bool DatatypeSelector::isNull() const
3769 CVC5_API_TRY_CATCH_BEGIN
;
3770 //////// all checks before this line
3771 return isNullHelper();
3773 CVC5_API_TRY_CATCH_END
;
3776 std::string
DatatypeSelector::toString() const
3778 CVC5_API_TRY_CATCH_BEGIN
;
3779 //////// all checks before this line
3780 std::stringstream ss
;
3784 CVC5_API_TRY_CATCH_END
;
3787 std::ostream
& operator<<(std::ostream
& out
, const DatatypeSelector
& stor
)
3789 out
<< stor
.toString();
3793 bool DatatypeSelector::isNullHelper() const { return d_stor
== nullptr; }
3795 /* DatatypeConstructor ------------------------------------------------------ */
3797 DatatypeConstructor::DatatypeConstructor() : d_solver(nullptr), d_ctor(nullptr)
3801 DatatypeConstructor::DatatypeConstructor(const Solver
* slv
,
3802 const cvc5::DTypeConstructor
& ctor
)
3803 : d_solver(slv
), d_ctor(new cvc5::DTypeConstructor(ctor
))
3805 CVC5_API_CHECK(d_ctor
->isResolved())
3806 << "Expected resolved datatype constructor";
3809 DatatypeConstructor::~DatatypeConstructor()
3811 if (d_ctor
!= nullptr)
3817 std::string
DatatypeConstructor::getName() const
3819 CVC5_API_TRY_CATCH_BEGIN
;
3820 CVC5_API_CHECK_NOT_NULL
;
3821 //////// all checks before this line
3822 return d_ctor
->getName();
3824 CVC5_API_TRY_CATCH_END
;
3827 Term
DatatypeConstructor::getConstructorTerm() const
3829 CVC5_API_TRY_CATCH_BEGIN
;
3830 CVC5_API_CHECK_NOT_NULL
;
3831 //////// all checks before this line
3832 return Term(d_solver
, d_ctor
->getConstructor());
3834 CVC5_API_TRY_CATCH_END
;
3837 Term
DatatypeConstructor::getInstantiatedConstructorTerm(
3838 const Sort
& retSort
) const
3840 CVC5_API_TRY_CATCH_BEGIN
;
3841 CVC5_API_CHECK_NOT_NULL
;
3842 CVC5_API_CHECK(d_ctor
->isResolved())
3843 << "Expected resolved datatype constructor";
3844 CVC5_API_CHECK(retSort
.isDatatype())
3845 << "Cannot get specialized constructor type for non-datatype type "
3847 //////// all checks before this line
3848 Node ret
= d_ctor
->getInstantiatedConstructor(*retSort
.d_type
);
3849 (void)ret
.getType(true); /* kick off type checking */
3850 // apply type ascription to the operator
3851 Term sctor
= api::Term(d_solver
, ret
);
3854 CVC5_API_TRY_CATCH_END
;
3857 Term
DatatypeConstructor::getTesterTerm() const
3859 CVC5_API_TRY_CATCH_BEGIN
;
3860 CVC5_API_CHECK_NOT_NULL
;
3861 //////// all checks before this line
3862 return Term(d_solver
, d_ctor
->getTester());
3864 CVC5_API_TRY_CATCH_END
;
3867 size_t DatatypeConstructor::getNumSelectors() const
3869 CVC5_API_TRY_CATCH_BEGIN
;
3870 CVC5_API_CHECK_NOT_NULL
;
3871 //////// all checks before this line
3872 return d_ctor
->getNumArgs();
3874 CVC5_API_TRY_CATCH_END
;
3877 DatatypeSelector
DatatypeConstructor::operator[](size_t index
) const
3879 CVC5_API_TRY_CATCH_BEGIN
;
3880 CVC5_API_CHECK_NOT_NULL
;
3881 //////// all checks before this line
3882 return DatatypeSelector(d_solver
, (*d_ctor
)[index
]);
3884 CVC5_API_TRY_CATCH_END
;
3887 DatatypeSelector
DatatypeConstructor::operator[](const std::string
& name
) const
3889 CVC5_API_TRY_CATCH_BEGIN
;
3890 CVC5_API_CHECK_NOT_NULL
;
3891 //////// all checks before this line
3892 return getSelectorForName(name
);
3894 CVC5_API_TRY_CATCH_END
;
3897 DatatypeSelector
DatatypeConstructor::getSelector(const std::string
& name
) const
3899 CVC5_API_TRY_CATCH_BEGIN
;
3900 CVC5_API_CHECK_NOT_NULL
;
3901 //////// all checks before this line
3902 return getSelectorForName(name
);
3904 CVC5_API_TRY_CATCH_END
;
3907 Term
DatatypeConstructor::getSelectorTerm(const std::string
& name
) const
3909 CVC5_API_TRY_CATCH_BEGIN
;
3910 CVC5_API_CHECK_NOT_NULL
;
3911 //////// all checks before this line
3912 return getSelector(name
).getSelectorTerm();
3914 CVC5_API_TRY_CATCH_END
;
3917 DatatypeConstructor::const_iterator
DatatypeConstructor::begin() const
3919 return DatatypeConstructor::const_iterator(d_solver
, *d_ctor
, true);
3922 DatatypeConstructor::const_iterator
DatatypeConstructor::end() const
3924 return DatatypeConstructor::const_iterator(d_solver
, *d_ctor
, false);
3927 DatatypeConstructor::const_iterator::const_iterator(
3928 const Solver
* slv
, const cvc5::DTypeConstructor
& ctor
, bool begin
)
3931 d_int_stors
= &ctor
.getArgs();
3933 const std::vector
<std::shared_ptr
<cvc5::DTypeSelector
>>& sels
=
3935 for (const std::shared_ptr
<cvc5::DTypeSelector
>& s
: sels
)
3937 /* Can not use emplace_back here since constructor is private. */
3938 d_stors
.push_back(DatatypeSelector(d_solver
, *s
.get()));
3940 d_idx
= begin
? 0 : sels
.size();
3943 DatatypeConstructor::const_iterator::const_iterator()
3944 : d_solver(nullptr), d_int_stors(nullptr), d_idx(0)
3948 DatatypeConstructor::const_iterator
&
3949 DatatypeConstructor::const_iterator::operator=(
3950 const DatatypeConstructor::const_iterator
& it
)
3952 d_solver
= it
.d_solver
;
3953 d_int_stors
= it
.d_int_stors
;
3954 d_stors
= it
.d_stors
;
3959 const DatatypeSelector
& DatatypeConstructor::const_iterator::operator*() const
3961 return d_stors
[d_idx
];
3964 const DatatypeSelector
* DatatypeConstructor::const_iterator::operator->() const
3966 return &d_stors
[d_idx
];
3969 DatatypeConstructor::const_iterator
&
3970 DatatypeConstructor::const_iterator::operator++()
3976 DatatypeConstructor::const_iterator
3977 DatatypeConstructor::const_iterator::operator++(int)
3979 DatatypeConstructor::const_iterator
it(*this);
3984 bool DatatypeConstructor::const_iterator::operator==(
3985 const DatatypeConstructor::const_iterator
& other
) const
3987 return d_int_stors
== other
.d_int_stors
&& d_idx
== other
.d_idx
;
3990 bool DatatypeConstructor::const_iterator::operator!=(
3991 const DatatypeConstructor::const_iterator
& other
) const
3993 return d_int_stors
!= other
.d_int_stors
|| d_idx
!= other
.d_idx
;
3996 bool DatatypeConstructor::isNull() const
3998 CVC5_API_TRY_CATCH_BEGIN
;
3999 //////// all checks before this line
4000 return isNullHelper();
4002 CVC5_API_TRY_CATCH_END
;
4005 std::string
DatatypeConstructor::toString() const
4007 CVC5_API_TRY_CATCH_BEGIN
;
4008 //////// all checks before this line
4009 std::stringstream ss
;
4013 CVC5_API_TRY_CATCH_END
;
4016 bool DatatypeConstructor::isNullHelper() const { return d_ctor
== nullptr; }
4018 DatatypeSelector
DatatypeConstructor::getSelectorForName(
4019 const std::string
& name
) const
4021 bool foundSel
= false;
4023 for (size_t i
= 0, nsels
= getNumSelectors(); i
< nsels
; i
++)
4025 if ((*d_ctor
)[i
].getName() == name
)
4034 std::stringstream snames
;
4036 for (size_t i
= 0, ncons
= getNumSelectors(); i
< ncons
; i
++)
4038 snames
<< (*d_ctor
)[i
].getName() << " ";
4041 CVC5_API_CHECK(foundSel
) << "No selector " << name
<< " for constructor "
4042 << getName() << " exists among " << snames
.str();
4044 return DatatypeSelector(d_solver
, (*d_ctor
)[index
]);
4047 std::ostream
& operator<<(std::ostream
& out
, const DatatypeConstructor
& ctor
)
4049 out
<< ctor
.toString();
4053 /* Datatype ----------------------------------------------------------------- */
4055 Datatype::Datatype(const Solver
* slv
, const cvc5::DType
& dtype
)
4056 : d_solver(slv
), d_dtype(new cvc5::DType(dtype
))
4058 CVC5_API_CHECK(d_dtype
->isResolved()) << "Expected resolved datatype";
4061 Datatype::Datatype() : d_solver(nullptr), d_dtype(nullptr) {}
4063 Datatype::~Datatype()
4065 if (d_dtype
!= nullptr)
4071 DatatypeConstructor
Datatype::operator[](size_t idx
) const
4073 CVC5_API_TRY_CATCH_BEGIN
;
4074 CVC5_API_CHECK_NOT_NULL
;
4075 CVC5_API_CHECK(idx
< getNumConstructors()) << "Index out of bounds.";
4076 //////// all checks before this line
4077 return DatatypeConstructor(d_solver
, (*d_dtype
)[idx
]);
4079 CVC5_API_TRY_CATCH_END
;
4082 DatatypeConstructor
Datatype::operator[](const std::string
& name
) const
4084 CVC5_API_TRY_CATCH_BEGIN
;
4085 CVC5_API_CHECK_NOT_NULL
;
4086 //////// all checks before this line
4087 return getConstructorForName(name
);
4089 CVC5_API_TRY_CATCH_END
;
4092 DatatypeConstructor
Datatype::getConstructor(const std::string
& name
) const
4094 CVC5_API_TRY_CATCH_BEGIN
;
4095 CVC5_API_CHECK_NOT_NULL
;
4096 //////// all checks before this line
4097 return getConstructorForName(name
);
4099 CVC5_API_TRY_CATCH_END
;
4102 Term
Datatype::getConstructorTerm(const std::string
& name
) const
4104 CVC5_API_TRY_CATCH_BEGIN
;
4105 CVC5_API_CHECK_NOT_NULL
;
4106 //////// all checks before this line
4107 return getConstructorForName(name
).getConstructorTerm();
4109 CVC5_API_TRY_CATCH_END
;
4112 DatatypeSelector
Datatype::getSelector(const std::string
& name
) const
4114 CVC5_API_TRY_CATCH_BEGIN
;
4115 CVC5_API_CHECK_NOT_NULL
;
4116 //////// all checks before this line
4117 return getSelectorForName(name
);
4119 CVC5_API_TRY_CATCH_END
;
4122 std::string
Datatype::getName() const
4124 CVC5_API_TRY_CATCH_BEGIN
;
4125 CVC5_API_CHECK_NOT_NULL
;
4126 //////// all checks before this line
4127 return d_dtype
->getName();
4129 CVC5_API_TRY_CATCH_END
;
4132 size_t Datatype::getNumConstructors() const
4134 CVC5_API_TRY_CATCH_BEGIN
;
4135 CVC5_API_CHECK_NOT_NULL
;
4136 //////// all checks before this line
4137 return d_dtype
->getNumConstructors();
4139 CVC5_API_TRY_CATCH_END
;
4142 std::vector
<Sort
> Datatype::getParameters() const
4144 CVC5_API_TRY_CATCH_BEGIN
;
4145 CVC5_API_CHECK_NOT_NULL
;
4146 CVC5_API_CHECK(isParametric()) << "Expected parametric datatype";
4147 //////// all checks before this line
4148 std::vector
<cvc5::TypeNode
> params
= d_dtype
->getParameters();
4149 return Sort::typeNodeVectorToSorts(d_solver
, params
);
4151 CVC5_API_TRY_CATCH_END
;
4154 bool Datatype::isParametric() const
4156 CVC5_API_TRY_CATCH_BEGIN
;
4157 CVC5_API_CHECK_NOT_NULL
;
4158 //////// all checks before this line
4159 return d_dtype
->isParametric();
4161 CVC5_API_TRY_CATCH_END
;
4164 bool Datatype::isCodatatype() const
4166 CVC5_API_TRY_CATCH_BEGIN
;
4167 CVC5_API_CHECK_NOT_NULL
;
4168 //////// all checks before this line
4169 return d_dtype
->isCodatatype();
4171 CVC5_API_TRY_CATCH_END
;
4174 bool Datatype::isTuple() const
4176 CVC5_API_TRY_CATCH_BEGIN
;
4177 CVC5_API_CHECK_NOT_NULL
;
4178 //////// all checks before this line
4179 return d_dtype
->isTuple();
4181 CVC5_API_TRY_CATCH_END
;
4184 bool Datatype::isRecord() const
4186 CVC5_API_TRY_CATCH_BEGIN
;
4187 CVC5_API_CHECK_NOT_NULL
;
4188 //////// all checks before this line
4189 return d_dtype
->isRecord();
4191 CVC5_API_TRY_CATCH_END
;
4194 bool Datatype::isFinite() const
4196 CVC5_API_TRY_CATCH_BEGIN
;
4197 CVC5_API_CHECK_NOT_NULL
;
4198 //////// all checks before this line
4199 // we assume that finite model finding is disabled by passing false as the
4201 return isCardinalityClassFinite(d_dtype
->getCardinalityClass(), false);
4203 CVC5_API_TRY_CATCH_END
;
4206 bool Datatype::isWellFounded() const
4208 CVC5_API_TRY_CATCH_BEGIN
;
4209 CVC5_API_CHECK_NOT_NULL
;
4210 //////// all checks before this line
4211 return d_dtype
->isWellFounded();
4213 CVC5_API_TRY_CATCH_END
;
4215 bool Datatype::hasNestedRecursion() const
4217 CVC5_API_TRY_CATCH_BEGIN
;
4218 CVC5_API_CHECK_NOT_NULL
;
4219 //////// all checks before this line
4220 return d_dtype
->hasNestedRecursion();
4222 CVC5_API_TRY_CATCH_END
;
4225 bool Datatype::isNull() const
4227 CVC5_API_TRY_CATCH_BEGIN
;
4228 //////// all checks before this line
4229 return isNullHelper();
4231 CVC5_API_TRY_CATCH_END
;
4234 std::string
Datatype::toString() const
4236 CVC5_API_TRY_CATCH_BEGIN
;
4237 CVC5_API_CHECK_NOT_NULL
;
4238 //////// all checks before this line
4239 return d_dtype
->getName();
4241 CVC5_API_TRY_CATCH_END
;
4244 Datatype::const_iterator
Datatype::begin() const
4246 return Datatype::const_iterator(d_solver
, *d_dtype
, true);
4249 Datatype::const_iterator
Datatype::end() const
4251 return Datatype::const_iterator(d_solver
, *d_dtype
, false);
4254 DatatypeConstructor
Datatype::getConstructorForName(
4255 const std::string
& name
) const
4257 bool foundCons
= false;
4259 for (size_t i
= 0, ncons
= getNumConstructors(); i
< ncons
; i
++)
4261 if ((*d_dtype
)[i
].getName() == name
)
4270 std::stringstream snames
;
4272 for (size_t i
= 0, ncons
= getNumConstructors(); i
< ncons
; i
++)
4274 snames
<< (*d_dtype
)[i
].getName() << " ";
4277 CVC5_API_CHECK(foundCons
) << "No constructor " << name
<< " for datatype "
4278 << getName() << " exists, among " << snames
.str();
4280 return DatatypeConstructor(d_solver
, (*d_dtype
)[index
]);
4283 DatatypeSelector
Datatype::getSelectorForName(const std::string
& name
) const
4285 bool foundSel
= false;
4288 for (size_t i
= 0, ncons
= getNumConstructors(); i
< ncons
; i
++)
4290 int si
= (*d_dtype
)[i
].getSelectorIndexForName(name
);
4293 sindex
= static_cast<size_t>(si
);
4301 CVC5_API_CHECK(foundSel
)
4302 << "No select " << name
<< " for datatype " << getName() << " exists";
4304 return DatatypeSelector(d_solver
, (*d_dtype
)[index
][sindex
]);
4307 Datatype::const_iterator::const_iterator(const Solver
* slv
,
4308 const cvc5::DType
& dtype
,
4310 : d_solver(slv
), d_int_ctors(&dtype
.getConstructors())
4312 const std::vector
<std::shared_ptr
<DTypeConstructor
>>& cons
=
4313 dtype
.getConstructors();
4314 for (const std::shared_ptr
<DTypeConstructor
>& c
: cons
)
4316 /* Can not use emplace_back here since constructor is private. */
4317 d_ctors
.push_back(DatatypeConstructor(d_solver
, *c
.get()));
4319 d_idx
= begin
? 0 : cons
.size();
4322 Datatype::const_iterator::const_iterator()
4323 : d_solver(nullptr), d_int_ctors(nullptr), d_idx(0)
4327 Datatype::const_iterator
& Datatype::const_iterator::operator=(
4328 const Datatype::const_iterator
& it
)
4330 d_solver
= it
.d_solver
;
4331 d_int_ctors
= it
.d_int_ctors
;
4332 d_ctors
= it
.d_ctors
;
4337 const DatatypeConstructor
& Datatype::const_iterator::operator*() const
4339 return d_ctors
[d_idx
];
4342 const DatatypeConstructor
* Datatype::const_iterator::operator->() const
4344 return &d_ctors
[d_idx
];
4347 Datatype::const_iterator
& Datatype::const_iterator::operator++()
4353 Datatype::const_iterator
Datatype::const_iterator::operator++(int)
4355 Datatype::const_iterator
it(*this);
4360 bool Datatype::const_iterator::operator==(
4361 const Datatype::const_iterator
& other
) const
4363 return d_int_ctors
== other
.d_int_ctors
&& d_idx
== other
.d_idx
;
4366 bool Datatype::const_iterator::operator!=(
4367 const Datatype::const_iterator
& other
) const
4369 return d_int_ctors
!= other
.d_int_ctors
|| d_idx
!= other
.d_idx
;
4372 bool Datatype::isNullHelper() const { return d_dtype
== nullptr; }
4374 /* -------------------------------------------------------------------------- */
4376 /* -------------------------------------------------------------------------- */
4379 : d_solver(nullptr),
4389 Grammar::Grammar(const Solver
* slv
,
4390 const std::vector
<Term
>& sygusVars
,
4391 const std::vector
<Term
>& ntSymbols
)
4393 d_sygusVars(sygusVars
),
4394 d_ntSyms(ntSymbols
),
4395 d_ntsToTerms(ntSymbols
.size()),
4400 for (Term ntsymbol
: d_ntSyms
)
4402 d_ntsToTerms
.emplace(ntsymbol
, std::vector
<Term
>());
4406 void Grammar::addRule(const Term
& ntSymbol
, const Term
& rule
)
4408 CVC5_API_TRY_CATCH_BEGIN
;
4409 CVC5_API_CHECK(!d_isResolved
) << "Grammar cannot be modified after passing "
4410 "it as an argument to synthFun/synthInv";
4411 CVC5_API_CHECK_TERM(ntSymbol
);
4412 CVC5_API_CHECK_TERM(rule
);
4413 CVC5_API_ARG_CHECK_EXPECTED(
4414 d_ntsToTerms
.find(ntSymbol
) != d_ntsToTerms
.cend(), ntSymbol
)
4415 << "ntSymbol to be one of the non-terminal symbols given in the "
4417 CVC5_API_CHECK(ntSymbol
.d_node
->getType() == rule
.d_node
->getType())
4418 << "Expected ntSymbol and rule to have the same sort";
4419 CVC5_API_ARG_CHECK_EXPECTED(!containsFreeVariables(rule
), rule
)
4420 << "a term whose free variables are limited to synthFun/synthInv "
4421 "parameters and non-terminal symbols of the grammar";
4422 //////// all checks before this line
4423 d_ntsToTerms
[ntSymbol
].push_back(rule
);
4425 CVC5_API_TRY_CATCH_END
;
4428 void Grammar::addRules(const Term
& ntSymbol
, const std::vector
<Term
>& rules
)
4430 CVC5_API_TRY_CATCH_BEGIN
;
4431 CVC5_API_CHECK(!d_isResolved
) << "Grammar cannot be modified after passing "
4432 "it as an argument to synthFun/synthInv";
4433 CVC5_API_CHECK_TERM(ntSymbol
);
4434 CVC5_API_CHECK_TERMS_WITH_SORT(rules
, ntSymbol
.getSort());
4435 CVC5_API_ARG_CHECK_EXPECTED(
4436 d_ntsToTerms
.find(ntSymbol
) != d_ntsToTerms
.cend(), ntSymbol
)
4437 << "ntSymbol to be one of the non-terminal symbols given in the "
4439 for (size_t i
= 0, n
= rules
.size(); i
< n
; ++i
)
4441 CVC5_API_ARG_AT_INDEX_CHECK_EXPECTED(
4442 !containsFreeVariables(rules
[i
]), rules
[i
], rules
, i
)
4443 << "a term whose free variables are limited to synthFun/synthInv "
4444 "parameters and non-terminal symbols of the grammar";
4446 //////// all checks before this line
4447 d_ntsToTerms
[ntSymbol
].insert(
4448 d_ntsToTerms
[ntSymbol
].cend(), rules
.cbegin(), rules
.cend());
4450 CVC5_API_TRY_CATCH_END
;
4453 void Grammar::addAnyConstant(const Term
& ntSymbol
)
4455 CVC5_API_TRY_CATCH_BEGIN
;
4456 CVC5_API_CHECK(!d_isResolved
) << "Grammar cannot be modified after passing "
4457 "it as an argument to synthFun/synthInv";
4458 CVC5_API_CHECK_TERM(ntSymbol
);
4459 CVC5_API_ARG_CHECK_EXPECTED(
4460 d_ntsToTerms
.find(ntSymbol
) != d_ntsToTerms
.cend(), ntSymbol
)
4461 << "ntSymbol to be one of the non-terminal symbols given in the "
4463 //////// all checks before this line
4464 d_allowConst
.insert(ntSymbol
);
4466 CVC5_API_TRY_CATCH_END
;
4469 void Grammar::addAnyVariable(const Term
& ntSymbol
)
4471 CVC5_API_TRY_CATCH_BEGIN
;
4472 CVC5_API_CHECK(!d_isResolved
) << "Grammar cannot be modified after passing "
4473 "it as an argument to synthFun/synthInv";
4474 CVC5_API_CHECK_TERM(ntSymbol
);
4475 CVC5_API_ARG_CHECK_EXPECTED(
4476 d_ntsToTerms
.find(ntSymbol
) != d_ntsToTerms
.cend(), ntSymbol
)
4477 << "ntSymbol to be one of the non-terminal symbols given in the "
4479 //////// all checks before this line
4480 d_allowVars
.insert(ntSymbol
);
4482 CVC5_API_TRY_CATCH_END
;
4486 * This function concatenates the outputs of calling f on each element between
4487 * first and last, seperated by sep.
4488 * @param first the beginning of the range
4489 * @param last the end of the range
4490 * @param f the function to call on each element in the range, its output must
4491 * be overloaded for operator<<
4492 * @param sep the string to add between successive calls to f
4494 template <typename Iterator
, typename Function
>
4495 std::string
join(Iterator first
, Iterator last
, Function f
, std::string sep
)
4497 std::stringstream ss
;
4515 std::string
Grammar::toString() const
4517 CVC5_API_TRY_CATCH_BEGIN
;
4518 //////// all checks before this line
4519 std::stringstream ss
;
4520 ss
<< " (" // pre-declaration
4525 std::stringstream s
;
4526 s
<< '(' << t
<< ' ' << t
.getSort() << ')';
4530 << ")\n (" // grouped rule listing
4534 [this](const Term
& t
) {
4535 bool allowConst
= d_allowConst
.find(t
) != d_allowConst
.cend(),
4536 allowVars
= d_allowVars
.find(t
) != d_allowVars
.cend();
4537 const std::vector
<Term
>& rules
= d_ntsToTerms
.at(t
);
4538 std::stringstream s
;
4539 s
<< '(' << t
<< ' ' << t
.getSort() << " ("
4540 << (allowConst
? "(Constant " + t
.getSort().toString() + ")"
4542 << (allowConst
&& allowVars
? " " : "")
4543 << (allowVars
? "(Var " + t
.getSort().toString() + ")" : "")
4544 << ((allowConst
|| allowVars
) && !rules
.empty() ? " " : "")
4548 [](const Term
& rule
) { return rule
.toString(); },
4558 CVC5_API_TRY_CATCH_END
;
4561 Sort
Grammar::resolve()
4563 CVC5_API_TRY_CATCH_BEGIN
;
4564 //////// all checks before this line
4566 d_isResolved
= true;
4570 if (!d_sygusVars
.empty())
4574 d_solver
->getNodeManager()->mkNode(
4575 cvc5::kind::BOUND_VAR_LIST
, Term::termVectorToNodes(d_sygusVars
)));
4578 std::unordered_map
<Term
, Sort
> ntsToUnres(d_ntSyms
.size());
4580 for (Term ntsymbol
: d_ntSyms
)
4582 // make the unresolved type, used for referencing the final version of
4583 // the ntsymbol's datatype
4584 ntsToUnres
[ntsymbol
] =
4585 Sort(d_solver
, d_solver
->getNodeManager()->mkSort(ntsymbol
.toString()));
4588 std::vector
<cvc5::DType
> datatypes
;
4589 std::set
<TypeNode
> unresTypes
;
4591 datatypes
.reserve(d_ntSyms
.size());
4593 for (const Term
& ntSym
: d_ntSyms
)
4595 // make the datatype, which encodes terms generated by this non-terminal
4596 DatatypeDecl
dtDecl(d_solver
, ntSym
.toString());
4598 for (const Term
& consTerm
: d_ntsToTerms
[ntSym
])
4600 addSygusConstructorTerm(dtDecl
, consTerm
, ntsToUnres
);
4603 if (d_allowVars
.find(ntSym
) != d_allowVars
.cend())
4605 addSygusConstructorVariables(dtDecl
,
4606 Sort(d_solver
, ntSym
.d_node
->getType()));
4609 bool aci
= d_allowConst
.find(ntSym
) != d_allowConst
.end();
4610 TypeNode btt
= ntSym
.d_node
->getType();
4611 dtDecl
.d_dtype
->setSygus(btt
, *bvl
.d_node
, aci
, false);
4613 // We can be in a case where the only rule specified was (Variable T)
4614 // and there are no variables of type T, in which case this is a bogus
4615 // grammar. This results in the error below.
4616 CVC5_API_CHECK(dtDecl
.d_dtype
->getNumConstructors() != 0)
4617 << "Grouped rule listing for " << *dtDecl
.d_dtype
4618 << " produced an empty rule list";
4620 datatypes
.push_back(*dtDecl
.d_dtype
);
4621 unresTypes
.insert(*ntsToUnres
[ntSym
].d_type
);
4624 std::vector
<TypeNode
> datatypeTypes
=
4625 d_solver
->getNodeManager()->mkMutualDatatypeTypes(
4626 datatypes
, unresTypes
, NodeManager::DATATYPE_FLAG_PLACEHOLDER
);
4628 // return is the first datatype
4629 return Sort(d_solver
, datatypeTypes
[0]);
4631 CVC5_API_TRY_CATCH_END
;
4634 void Grammar::addSygusConstructorTerm(
4637 const std::unordered_map
<Term
, Sort
>& ntsToUnres
) const
4639 CVC5_API_TRY_CATCH_BEGIN
;
4640 CVC5_API_CHECK_DTDECL(dt
);
4641 CVC5_API_CHECK_TERM(term
);
4642 CVC5_API_CHECK_TERMS_MAP(ntsToUnres
);
4643 //////// all checks before this line
4645 // At this point, we should know that dt is well founded, and that its
4646 // builtin sygus operators are well-typed.
4647 // Now, purify each occurrence of a non-terminal symbol in term, replace by
4648 // free variables. These become arguments to constructors. Notice we must do
4649 // a tree traversal in this function, since unique paths to the same term
4650 // should be treated as distinct terms.
4651 // Notice that let expressions are forbidden in the input syntax of term, so
4652 // this does not lead to exponential behavior with respect to input size.
4653 std::vector
<Term
> args
;
4654 std::vector
<Sort
> cargs
;
4655 Term op
= purifySygusGTerm(term
, args
, cargs
, ntsToUnres
);
4656 std::stringstream ssCName
;
4657 ssCName
<< op
.getKind();
4662 d_solver
->getNodeManager()->mkNode(cvc5::kind::BOUND_VAR_LIST
,
4663 Term::termVectorToNodes(args
)));
4664 // its operator is a lambda
4666 d_solver
->getNodeManager()->mkNode(
4667 cvc5::kind::LAMBDA
, *lbvl
.d_node
, *op
.d_node
));
4669 std::vector
<TypeNode
> cargst
= Sort::sortVectorToTypeNodes(cargs
);
4670 dt
.d_dtype
->addSygusConstructor(*op
.d_node
, ssCName
.str(), cargst
);
4672 CVC5_API_TRY_CATCH_END
;
4675 Term
Grammar::purifySygusGTerm(
4677 std::vector
<Term
>& args
,
4678 std::vector
<Sort
>& cargs
,
4679 const std::unordered_map
<Term
, Sort
>& ntsToUnres
) const
4681 CVC5_API_TRY_CATCH_BEGIN
;
4682 CVC5_API_CHECK_TERM(term
);
4683 CVC5_API_CHECK_TERMS(args
);
4684 CVC5_API_CHECK_SORTS(cargs
);
4685 CVC5_API_CHECK_TERMS_MAP(ntsToUnres
);
4686 //////// all checks before this line
4688 std::unordered_map
<Term
, Sort
>::const_iterator itn
= ntsToUnres
.find(term
);
4689 if (itn
!= ntsToUnres
.cend())
4693 d_solver
->getNodeManager()->mkBoundVar(term
.d_node
->getType()));
4694 args
.push_back(ret
);
4695 cargs
.push_back(itn
->second
);
4698 std::vector
<Term
> pchildren
;
4699 bool childChanged
= false;
4700 for (unsigned i
= 0, nchild
= term
.d_node
->getNumChildren(); i
< nchild
; i
++)
4702 Term ptermc
= purifySygusGTerm(
4703 Term(d_solver
, (*term
.d_node
)[i
]), args
, cargs
, ntsToUnres
);
4704 pchildren
.push_back(ptermc
);
4705 childChanged
= childChanged
|| *ptermc
.d_node
!= (*term
.d_node
)[i
];
4714 if (term
.d_node
->getMetaKind() == kind::metakind::PARAMETERIZED
)
4716 // it's an indexed operator so we should provide the op
4717 NodeBuilder
nb(term
.d_node
->getKind());
4718 nb
<< term
.d_node
->getOperator();
4719 nb
.append(Term::termVectorToNodes(pchildren
));
4720 nret
= nb
.constructNode();
4724 nret
= d_solver
->getNodeManager()->mkNode(
4725 term
.d_node
->getKind(), Term::termVectorToNodes(pchildren
));
4728 return Term(d_solver
, nret
);
4730 CVC5_API_TRY_CATCH_END
;
4733 void Grammar::addSygusConstructorVariables(DatatypeDecl
& dt
,
4734 const Sort
& sort
) const
4736 CVC5_API_TRY_CATCH_BEGIN
;
4737 CVC5_API_CHECK_DTDECL(dt
);
4738 CVC5_API_CHECK_SORT(sort
);
4739 //////// all checks before this line
4741 // each variable of appropriate type becomes a sygus constructor in dt.
4742 for (unsigned i
= 0, size
= d_sygusVars
.size(); i
< size
; i
++)
4744 Term v
= d_sygusVars
[i
];
4745 if (v
.d_node
->getType() == *sort
.d_type
)
4747 std::stringstream ss
;
4749 std::vector
<TypeNode
> cargs
;
4750 dt
.d_dtype
->addSygusConstructor(*v
.d_node
, ss
.str(), cargs
);
4754 CVC5_API_TRY_CATCH_END
;
4757 bool Grammar::containsFreeVariables(const Term
& rule
) const
4759 // we allow the argument list and non-terminal symbols to be in scope
4760 std::unordered_set
<TNode
> scope
;
4762 for (const Term
& sygusVar
: d_sygusVars
)
4764 scope
.emplace(*sygusVar
.d_node
);
4767 for (const Term
& ntsymbol
: d_ntSyms
)
4769 scope
.emplace(*ntsymbol
.d_node
);
4772 return expr::hasFreeVariablesScope(*rule
.d_node
, scope
);
4775 std::ostream
& operator<<(std::ostream
& out
, const Grammar
& grammar
)
4777 return out
<< grammar
.toString();
4780 /* -------------------------------------------------------------------------- */
4781 /* Rounding Mode for Floating Points */
4782 /* -------------------------------------------------------------------------- */
4784 const static std::unordered_map
<RoundingMode
, cvc5::RoundingMode
> s_rmodes
{
4785 {ROUND_NEAREST_TIES_TO_EVEN
,
4786 cvc5::RoundingMode::ROUND_NEAREST_TIES_TO_EVEN
},
4787 {ROUND_TOWARD_POSITIVE
, cvc5::RoundingMode::ROUND_TOWARD_POSITIVE
},
4788 {ROUND_TOWARD_NEGATIVE
, cvc5::RoundingMode::ROUND_TOWARD_NEGATIVE
},
4789 {ROUND_TOWARD_ZERO
, cvc5::RoundingMode::ROUND_TOWARD_ZERO
},
4790 {ROUND_NEAREST_TIES_TO_AWAY
,
4791 cvc5::RoundingMode::ROUND_NEAREST_TIES_TO_AWAY
},
4794 const static std::unordered_map
<cvc5::RoundingMode
,
4796 cvc5::RoundingModeHashFunction
>
4798 {cvc5::RoundingMode::ROUND_NEAREST_TIES_TO_EVEN
,
4799 ROUND_NEAREST_TIES_TO_EVEN
},
4800 {cvc5::RoundingMode::ROUND_TOWARD_POSITIVE
, ROUND_TOWARD_POSITIVE
},
4801 {cvc5::RoundingMode::ROUND_TOWARD_POSITIVE
, ROUND_TOWARD_NEGATIVE
},
4802 {cvc5::RoundingMode::ROUND_TOWARD_ZERO
, ROUND_TOWARD_ZERO
},
4803 {cvc5::RoundingMode::ROUND_NEAREST_TIES_TO_AWAY
,
4804 ROUND_NEAREST_TIES_TO_AWAY
},
4807 /* -------------------------------------------------------------------------- */
4809 /* -------------------------------------------------------------------------- */
4811 DriverOptions::DriverOptions(const Solver
& solver
) : d_solver(solver
) {}
4813 std::istream
& DriverOptions::in() const
4815 return *d_solver
.d_slv
->getOptions().base
.in
;
4817 std::ostream
& DriverOptions::err() const
4819 return *d_solver
.d_slv
->getOptions().base
.err
;
4821 std::ostream
& DriverOptions::out() const
4823 return *d_solver
.d_slv
->getOptions().base
.out
;
4826 /* -------------------------------------------------------------------------- */
4828 /* -------------------------------------------------------------------------- */
4830 struct Stat::StatData
4832 cvc5::StatExportData data
;
4833 template <typename T
>
4834 StatData(T
&& t
) : data(std::forward
<T
>(t
))
4837 StatData() : data() {}
4841 Stat::Stat(const Stat
& s
)
4842 : d_expert(s
.d_expert
),
4843 d_default(s
.d_default
),
4844 d_data(std::make_unique
<StatData
>(s
.d_data
->data
))
4847 Stat
& Stat::operator=(const Stat
& s
)
4849 d_expert
= s
.d_expert
;
4850 d_data
= std::make_unique
<StatData
>(s
.d_data
->data
);
4854 bool Stat::isExpert() const { return d_expert
; }
4855 bool Stat::isDefault() const { return d_default
; }
4857 bool Stat::isInt() const
4859 return std::holds_alternative
<int64_t>(d_data
->data
);
4861 int64_t Stat::getInt() const
4863 CVC5_API_TRY_CATCH_BEGIN
;
4864 CVC5_API_RECOVERABLE_CHECK(isInt()) << "Expected Stat of type int64_t.";
4865 return std::get
<int64_t>(d_data
->data
);
4866 CVC5_API_TRY_CATCH_END
;
4868 bool Stat::isDouble() const
4870 return std::holds_alternative
<double>(d_data
->data
);
4872 double Stat::getDouble() const
4874 CVC5_API_TRY_CATCH_BEGIN
;
4875 CVC5_API_RECOVERABLE_CHECK(isDouble()) << "Expected Stat of type double.";
4876 return std::get
<double>(d_data
->data
);
4877 CVC5_API_TRY_CATCH_END
;
4879 bool Stat::isString() const
4881 return std::holds_alternative
<std::string
>(d_data
->data
);
4883 const std::string
& Stat::getString() const
4885 CVC5_API_TRY_CATCH_BEGIN
;
4886 CVC5_API_RECOVERABLE_CHECK(isString())
4887 << "Expected Stat of type std::string.";
4888 return std::get
<std::string
>(d_data
->data
);
4889 CVC5_API_TRY_CATCH_END
;
4891 bool Stat::isHistogram() const
4893 return std::holds_alternative
<HistogramData
>(d_data
->data
);
4895 const Stat::HistogramData
& Stat::getHistogram() const
4897 CVC5_API_TRY_CATCH_BEGIN
;
4898 CVC5_API_RECOVERABLE_CHECK(isHistogram())
4899 << "Expected Stat of type histogram.";
4900 return std::get
<HistogramData
>(d_data
->data
);
4901 CVC5_API_TRY_CATCH_END
;
4904 Stat::Stat(bool expert
, bool defaulted
, StatData
&& sd
)
4906 d_default(defaulted
),
4907 d_data(std::make_unique
<StatData
>(std::move(sd
)))
4911 std::ostream
& operator<<(std::ostream
& os
, const Stat
& sv
)
4913 return cvc5::detail::print(os
, sv
.d_data
->data
);
4916 Statistics::BaseType::const_reference
Statistics::iterator::operator*() const
4918 return d_it
.operator*();
4920 Statistics::BaseType::const_pointer
Statistics::iterator::operator->() const
4922 return d_it
.operator->();
4924 Statistics::iterator
& Statistics::iterator::operator++()
4929 } while (!isVisible());
4932 Statistics::iterator
Statistics::iterator::operator++(int)
4934 iterator tmp
= *this;
4938 } while (!isVisible());
4941 Statistics::iterator
& Statistics::iterator::operator--()
4946 } while (!isVisible());
4949 Statistics::iterator
Statistics::iterator::operator--(int)
4951 iterator tmp
= *this;
4955 } while (!isVisible());
4958 bool Statistics::iterator::operator==(const Statistics::iterator
& rhs
) const
4960 return d_it
== rhs
.d_it
;
4962 bool Statistics::iterator::operator!=(const Statistics::iterator
& rhs
) const
4964 return d_it
!= rhs
.d_it
;
4966 Statistics::iterator::iterator(Statistics::BaseType::const_iterator it
,
4967 const Statistics::BaseType
& base
,
4970 : d_it(it
), d_base(&base
), d_showExpert(expert
), d_showDefault(defaulted
)
4972 while (!isVisible())
4977 bool Statistics::iterator::isVisible() const
4979 if (d_it
== d_base
->end()) return true;
4980 if (!d_showExpert
&& d_it
->second
.isExpert()) return false;
4981 if (!d_showDefault
&& d_it
->second
.isDefault()) return false;
4985 const Stat
& Statistics::get(const std::string
& name
)
4987 CVC5_API_TRY_CATCH_BEGIN
;
4988 auto it
= d_stats
.find(name
);
4989 CVC5_API_RECOVERABLE_CHECK(it
!= d_stats
.end())
4990 << "No stat with name \"" << name
<< "\" exists.";
4992 CVC5_API_TRY_CATCH_END
;
4995 Statistics::iterator
Statistics::begin(bool expert
, bool defaulted
) const
4997 return iterator(d_stats
.begin(), d_stats
, expert
, defaulted
);
4999 Statistics::iterator
Statistics::end() const
5001 return iterator(d_stats
.end(), d_stats
, false, false);
5004 Statistics::Statistics(const StatisticsRegistry
& reg
)
5006 for (const auto& svp
: reg
)
5008 d_stats
.emplace(svp
.first
,
5009 Stat(svp
.second
->d_expert
,
5010 svp
.second
->isDefault(),
5011 svp
.second
->getViewer()));
5015 std::ostream
& operator<<(std::ostream
& out
, const Statistics
& stats
)
5017 for (const auto& stat
: stats
)
5019 out
<< stat
.first
<< " = " << stat
.second
<< std::endl
;
5024 /* -------------------------------------------------------------------------- */
5026 /* -------------------------------------------------------------------------- */
5028 Solver::Solver(std::unique_ptr
<Options
>&& original
)
5030 d_nodeMgr
= NodeManager::currentNM();
5032 d_originalOptions
= std::move(original
);
5033 d_slv
.reset(new SolverEngine(d_nodeMgr
, d_originalOptions
.get()));
5034 d_slv
->setSolver(this);
5035 d_rng
.reset(new Random(d_slv
->getOptions().driver
.seed
));
5039 Solver::Solver() : Solver(std::make_unique
<Options
>()) {}
5041 Solver::~Solver() {}
5043 /* Helpers and private functions */
5044 /* -------------------------------------------------------------------------- */
5046 NodeManager
* Solver::getNodeManager(void) const { return d_nodeMgr
; }
5048 void Solver::increment_term_stats(Kind kind
) const
5050 if constexpr (Configuration::isStatisticsBuild())
5052 d_stats
->d_terms
<< kind
;
5056 void Solver::increment_vars_consts_stats(const Sort
& sort
, bool is_var
) const
5058 if constexpr (Configuration::isStatisticsBuild())
5060 const TypeNode tn
= sort
.getTypeNode();
5061 TypeConstant tc
= tn
.getKind() == cvc5::kind::TYPE_CONSTANT
5062 ? tn
.getConst
<TypeConstant
>()
5066 d_stats
->d_vars
<< tc
;
5070 d_stats
->d_consts
<< tc
;
5075 /* Split out to avoid nested API calls (problematic with API tracing). */
5076 /* .......................................................................... */
5078 template <typename T
>
5079 Term
Solver::mkValHelper(const T
& t
) const
5081 //////// all checks before this line
5082 Node res
= getNodeManager()->mkConst(t
);
5083 (void)res
.getType(true); /* kick off type checking */
5084 return Term(this, res
);
5087 Term
Solver::mkRationalValHelper(const Rational
& r
, bool isInt
) const
5089 //////// all checks before this line
5090 NodeManager
* nm
= getNodeManager();
5091 Node res
= isInt
? nm
->mkConstInt(r
) : nm
->mkConstReal(r
);
5092 (void)res
.getType(true); /* kick off type checking */
5093 api::Term t
= Term(this, res
);
5094 // NOTE: this block will be eliminated when arithmetic subtyping is eliminated
5097 t
= ensureRealSort(t
);
5102 Term
Solver::mkRealOrIntegerFromStrHelper(const std::string
& s
,
5105 //////// all checks before this line
5108 cvc5::Rational r
= s
.find('/') != std::string::npos
5110 : cvc5::Rational::fromDecimal(s
);
5111 return mkRationalValHelper(r
, isInt
);
5113 catch (const std::invalid_argument
& e
)
5115 /* Catch to throw with a more meaningful error message. To be caught in
5116 * enclosing CVC5_API_TRY_CATCH_* block to throw CVC5ApiException. */
5117 std::stringstream message
;
5118 message
<< "Cannot construct Real or Int from string argument '" << s
<< "'"
5120 throw std::invalid_argument(message
.str());
5124 Term
Solver::mkBVFromIntHelper(uint32_t size
, uint64_t val
) const
5126 CVC5_API_ARG_CHECK_EXPECTED(size
> 0, size
) << "a bit-width > 0";
5127 //////// all checks before this line
5128 return mkValHelper
<cvc5::BitVector
>(cvc5::BitVector(size
, val
));
5131 Term
Solver::mkBVFromStrHelper(uint32_t size
,
5132 const std::string
& s
,
5133 uint32_t base
) const
5135 CVC5_API_ARG_CHECK_EXPECTED(size
> 0, size
) << "a bit-width > 0";
5136 CVC5_API_ARG_CHECK_EXPECTED(!s
.empty(), s
) << "a non-empty string";
5137 CVC5_API_ARG_CHECK_EXPECTED(base
== 2 || base
== 10 || base
== 16, base
)
5138 << "base 2, 10, or 16";
5139 //////// all checks before this line
5141 Integer
val(s
, base
);
5143 if (val
.strictlyNegative())
5145 CVC5_API_CHECK(val
>= -Integer(2).pow(size
- 1))
5146 << "Overflow in bitvector construction (specified bitvector size "
5147 << size
<< " too small to hold value " << s
<< ")";
5151 CVC5_API_CHECK(val
.modByPow2(size
) == val
)
5152 << "Overflow in bitvector construction (specified bitvector size "
5153 << size
<< " too small to hold value " << s
<< ")";
5155 return mkValHelper
<cvc5::BitVector
>(cvc5::BitVector(size
, val
));
5158 Term
Solver::getValueHelper(const Term
& term
) const
5160 // Note: Term is checked in the caller to avoid double checks
5161 bool wasShadow
= false;
5162 bool freeOrShadowedVar
=
5163 expr::hasFreeOrShadowedVar(term
.getNode(), wasShadow
);
5164 CVC5_API_RECOVERABLE_CHECK(!freeOrShadowedVar
)
5165 << "Cannot get value of term containing "
5166 << (wasShadow
? "shadowed" : "free") << " variables";
5167 //////// all checks before this line
5168 Node value
= d_slv
->getValue(*term
.d_node
);
5169 Term res
= Term(this, value
);
5170 // May need to wrap in real cast so that user know this is a real.
5171 TypeNode tn
= (*term
.d_node
).getType();
5172 if (!tn
.isInteger() && value
.getType().isInteger())
5174 return ensureRealSort(res
);
5179 Sort
Solver::mkTupleSortHelper(const std::vector
<Sort
>& sorts
) const
5181 // Note: Sorts are checked in the caller to avoid double checks
5182 //////// all checks before this line
5183 std::vector
<TypeNode
> typeNodes
= Sort::sortVectorToTypeNodes(sorts
);
5184 return Sort(this, getNodeManager()->mkTupleType(typeNodes
));
5187 Term
Solver::mkTermFromKind(Kind kind
) const
5189 CVC5_API_KIND_CHECK_EXPECTED(kind
== PI
|| kind
== REGEXP_NONE
5190 || kind
== REGEXP_ALLCHAR
|| kind
== SEP_EMP
,
5192 << "PI, REGEXP_NONE, REGEXP_ALLCHAR or SEP_EMP";
5193 //////// all checks before this line
5195 cvc5::Kind k
= extToIntKind(kind
);
5196 if (kind
== REGEXP_NONE
|| kind
== REGEXP_ALLCHAR
)
5198 Assert(isDefinedIntKind(k
));
5199 res
= d_nodeMgr
->mkNode(k
, std::vector
<Node
>());
5201 else if (kind
== SEP_EMP
)
5203 res
= d_nodeMgr
->mkNullaryOperator(d_nodeMgr
->booleanType(), k
);
5208 res
= d_nodeMgr
->mkNullaryOperator(d_nodeMgr
->realType(), k
);
5210 (void)res
.getType(true); /* kick off type checking */
5211 increment_term_stats(kind
);
5212 return Term(this, res
);
5215 Term
Solver::mkTermHelper(Kind kind
, const std::vector
<Term
>& children
) const
5217 // Note: Kind and children are checked in the caller to avoid double checks
5218 //////// all checks before this line
5219 if (children
.size() == 0)
5221 return mkTermFromKind(kind
);
5223 std::vector
<Node
> echildren
= Term::termVectorToNodes(children
);
5224 cvc5::Kind k
= extToIntKind(kind
);
5226 if (echildren
.size() > 2)
5228 if (kind
== INTS_DIVISION
|| kind
== XOR
|| kind
== MINUS
5229 || kind
== DIVISION
|| kind
== HO_APPLY
|| kind
== REGEXP_DIFF
)
5231 // left-associative, but cvc5 internally only supports 2 args
5232 res
= d_nodeMgr
->mkLeftAssociative(k
, echildren
);
5234 else if (kind
== IMPLIES
)
5236 // right-associative, but cvc5 internally only supports 2 args
5237 res
= d_nodeMgr
->mkRightAssociative(k
, echildren
);
5239 else if (kind
== EQUAL
|| kind
== LT
|| kind
== GT
|| kind
== LEQ
5242 // "chainable", but cvc5 internally only supports 2 args
5243 res
= d_nodeMgr
->mkChain(k
, echildren
);
5245 else if (kind::isAssociative(k
))
5247 // mkAssociative has special treatment for associative operators with lots
5249 res
= d_nodeMgr
->mkAssociative(k
, echildren
);
5253 // default case, must check kind
5254 checkMkTerm(kind
, children
.size());
5255 res
= d_nodeMgr
->mkNode(k
, echildren
);
5258 else if (kind::isAssociative(k
))
5260 // associative case, same as above
5261 res
= d_nodeMgr
->mkAssociative(k
, echildren
);
5265 // default case, same as above
5266 checkMkTerm(kind
, children
.size());
5267 if (kind
== api::SET_SINGLETON
)
5269 // the type of the term is the same as the type of the internal node
5270 // see Term::getSort()
5271 TypeNode type
= children
[0].d_node
->getType();
5272 // Internally NodeManager::mkSingleton needs a type argument
5273 // to construct a singleton, since there is no difference between
5274 // integers and reals (both are Rationals).
5275 // At the API, mkReal and mkInteger are different and therefore the
5276 // element type can be used safely here.
5277 res
= getNodeManager()->mkSingleton(type
, *children
[0].d_node
);
5279 else if (kind
== api::BAG_MAKE
)
5281 // the type of the term is the same as the type of the internal node
5282 // see Term::getSort()
5283 TypeNode type
= children
[0].d_node
->getType();
5284 // Internally NodeManager::mkBag needs a type argument
5285 // to construct a bag, since there is no difference between
5286 // integers and reals (both are Rationals).
5287 // At the API, mkReal and mkInteger are different and therefore the
5288 // element type can be used safely here.
5289 res
= getNodeManager()->mkBag(
5290 type
, *children
[0].d_node
, *children
[1].d_node
);
5294 res
= d_nodeMgr
->mkNode(k
, echildren
);
5298 (void)res
.getType(true); /* kick off type checking */
5299 increment_term_stats(kind
);
5300 return Term(this, res
);
5303 Term
Solver::mkTermHelper(const Op
& op
, const std::vector
<Term
>& children
) const
5305 if (!op
.isIndexedHelper())
5307 return mkTermHelper(op
.d_kind
, children
);
5310 // Note: Op and children are checked in the caller to avoid double checks
5311 checkMkTerm(op
.d_kind
, children
.size());
5312 //////// all checks before this line
5314 const cvc5::Kind int_kind
= extToIntKind(op
.d_kind
);
5315 std::vector
<Node
> echildren
= Term::termVectorToNodes(children
);
5317 NodeBuilder
nb(int_kind
);
5319 nb
.append(echildren
);
5320 Node res
= nb
.constructNode();
5322 (void)res
.getType(true); /* kick off type checking */
5323 return Term(this, res
);
5326 std::vector
<Sort
> Solver::mkDatatypeSortsInternal(
5327 const std::vector
<DatatypeDecl
>& dtypedecls
,
5328 const std::set
<Sort
>& unresolvedSorts
) const
5330 // Note: dtypedecls and unresolvedSorts are checked in the caller to avoid
5332 //////// all checks before this line
5334 std::vector
<cvc5::DType
> datatypes
;
5335 for (size_t i
= 0, ndts
= dtypedecls
.size(); i
< ndts
; ++i
)
5337 datatypes
.push_back(dtypedecls
[i
].getDatatype());
5340 std::set
<TypeNode
> utypes
= Sort::sortSetToTypeNodes(unresolvedSorts
);
5341 std::vector
<cvc5::TypeNode
> dtypes
=
5342 getNodeManager()->mkMutualDatatypeTypes(datatypes
, utypes
);
5343 std::vector
<Sort
> retTypes
= Sort::typeNodeVectorToSorts(this, dtypes
);
5347 Term
Solver::synthFunHelper(const std::string
& symbol
,
5348 const std::vector
<Term
>& boundVars
,
5351 Grammar
* grammar
) const
5353 // Note: boundVars, sort and grammar are checked in the caller to avoid
5355 std::vector
<TypeNode
> varTypes
;
5356 for (const auto& bv
: boundVars
)
5360 CVC5_API_CHECK(grammar
->d_ntSyms
[0].d_node
->getType() == *sort
.d_type
)
5361 << "Invalid Start symbol for grammar, Expected Start's sort to be "
5362 << *sort
.d_type
<< " but found "
5363 << grammar
->d_ntSyms
[0].d_node
->getType();
5365 varTypes
.push_back(bv
.d_node
->getType());
5367 //////// all checks before this line
5369 TypeNode funType
= varTypes
.empty() ? *sort
.d_type
5370 : getNodeManager()->mkFunctionType(
5371 varTypes
, *sort
.d_type
);
5373 Node fun
= getNodeManager()->mkBoundVar(symbol
, funType
);
5374 (void)fun
.getType(true); /* kick off type checking */
5376 std::vector
<Node
> bvns
= Term::termVectorToNodes(boundVars
);
5378 d_slv
->declareSynthFun(
5380 grammar
== nullptr ? funType
: *grammar
->resolve().d_type
,
5384 return Term(this, fun
);
5387 Term
Solver::ensureTermSort(const Term
& term
, const Sort
& sort
) const
5389 // Note: Term and sort are checked in the caller to avoid double checks
5390 CVC5_API_CHECK(term
.getSort() == sort
5391 || (term
.getSort().isInteger() && sort
.isReal()))
5392 << "Expected conversion from Int to Real";
5393 //////// all checks before this line
5395 Sort t
= term
.getSort();
5396 if (term
.getSort() == sort
)
5401 // Integers are reals, too
5402 Assert(t
.d_type
->isReal());
5406 // Must cast to Real to ensure correct type is passed to parametric type
5407 // constructors. We do this cast using division with 1. This has the
5408 // advantage wrt using TO_REAL since (constant) division is always included
5411 d_nodeMgr
->mkNode(extToIntKind(DIVISION
),
5413 d_nodeMgr
->mkConst(kind::CONST_RATIONAL
,
5414 cvc5::Rational(1))));
5416 Assert(res
.getSort() == sort
);
5420 Term
Solver::ensureRealSort(const Term
& t
) const
5422 Assert(this == t
.d_solver
);
5423 CVC5_API_ARG_CHECK_EXPECTED(
5424 t
.getSort() == getIntegerSort() || t
.getSort() == getRealSort(),
5425 " an integer or real term");
5426 // Note: Term is checked in the caller to avoid double checks
5427 //////// all checks before this line
5428 if (t
.getSort() == getIntegerSort())
5430 Node n
= getNodeManager()->mkNode(kind::CAST_TO_REAL
, *t
.d_node
);
5431 return Term(this, n
);
5436 bool Solver::isValidInteger(const std::string
& s
) const
5438 //////// all checks before this line
5439 if (s
.length() == 0)
5441 // string should not be empty
5446 if (s
[index
] == '-')
5448 if (s
.length() == 1)
5450 // negative integers should contain at least one digit
5456 if (s
[index
] == '0' && s
.length() > (index
+ 1))
5458 // From SMT-Lib 2.6: A <numeral> is the digit 0 or a non-empty sequence of
5459 // digits not starting with 0. So integers like 001, 000 are not allowed
5463 // all remaining characters should be decimal digits
5464 for (; index
< s
.length(); ++index
)
5466 if (!std::isdigit(s
[index
]))
5475 void Solver::resetStatistics()
5477 if constexpr (Configuration::isStatisticsBuild())
5479 d_stats
.reset(new APIStatistics
{
5480 d_slv
->getStatisticsRegistry().registerHistogram
<TypeConstant
>(
5482 d_slv
->getStatisticsRegistry().registerHistogram
<TypeConstant
>(
5484 d_slv
->getStatisticsRegistry().registerHistogram
<Kind
>("api::TERM"),
5489 void Solver::printStatisticsSafe(int fd
) const
5491 d_slv
->printStatisticsSafe(fd
);
5494 /* Helpers for mkTerm checks. */
5495 /* .......................................................................... */
5497 void Solver::checkMkTerm(Kind kind
, uint32_t nchildren
) const
5499 CVC5_API_KIND_CHECK(kind
);
5500 Assert(isDefinedIntKind(extToIntKind(kind
)));
5501 const cvc5::kind::MetaKind mk
= kind::metaKindOf(extToIntKind(kind
));
5502 CVC5_API_KIND_CHECK_EXPECTED(
5503 mk
== kind::metakind::PARAMETERIZED
|| mk
== kind::metakind::OPERATOR
,
5505 << "Only operator-style terms are created with mkTerm(), "
5506 "to create variables, constants and values see mkVar(), mkConst() "
5507 "and the respective theory-specific functions to create values, "
5508 "e.g., mkBitVector().";
5509 CVC5_API_KIND_CHECK_EXPECTED(
5510 nchildren
>= minArity(kind
) && nchildren
<= maxArity(kind
), kind
)
5511 << "Terms with kind " << kindToString(kind
) << " must have at least "
5512 << minArity(kind
) << " children and at most " << maxArity(kind
)
5513 << " children (the one under construction has " << nchildren
<< ")";
5516 /* Sorts Handling */
5517 /* -------------------------------------------------------------------------- */
5519 Sort
Solver::getNullSort(void) const
5521 CVC5_API_TRY_CATCH_BEGIN
;
5522 //////// all checks before this line
5523 return Sort(this, TypeNode());
5525 CVC5_API_TRY_CATCH_END
;
5528 Sort
Solver::getBooleanSort(void) const
5530 CVC5_API_TRY_CATCH_BEGIN
;
5531 //////// all checks before this line
5532 return Sort(this, getNodeManager()->booleanType());
5534 CVC5_API_TRY_CATCH_END
;
5537 Sort
Solver::getIntegerSort(void) const
5539 CVC5_API_TRY_CATCH_BEGIN
;
5540 //////// all checks before this line
5541 return Sort(this, getNodeManager()->integerType());
5543 CVC5_API_TRY_CATCH_END
;
5546 Sort
Solver::getRealSort(void) const
5548 CVC5_API_TRY_CATCH_BEGIN
;
5549 //////// all checks before this line
5550 return Sort(this, getNodeManager()->realType());
5552 CVC5_API_TRY_CATCH_END
;
5555 Sort
Solver::getRegExpSort(void) const
5557 CVC5_API_TRY_CATCH_BEGIN
;
5558 //////// all checks before this line
5559 return Sort(this, getNodeManager()->regExpType());
5561 CVC5_API_TRY_CATCH_END
;
5564 Sort
Solver::getStringSort(void) const
5566 CVC5_API_TRY_CATCH_BEGIN
;
5567 //////// all checks before this line
5568 return Sort(this, getNodeManager()->stringType());
5570 CVC5_API_TRY_CATCH_END
;
5573 Sort
Solver::getRoundingModeSort(void) const
5575 CVC5_API_TRY_CATCH_BEGIN
;
5576 //////// all checks before this line
5577 return Sort(this, getNodeManager()->roundingModeType());
5579 CVC5_API_TRY_CATCH_END
;
5582 /* Create sorts ------------------------------------------------------- */
5584 Sort
Solver::mkArraySort(const Sort
& indexSort
, const Sort
& elemSort
) const
5586 CVC5_API_TRY_CATCH_BEGIN
;
5587 CVC5_API_SOLVER_CHECK_SORT(indexSort
);
5588 CVC5_API_SOLVER_CHECK_SORT(elemSort
);
5589 //////// all checks before this line
5591 this, getNodeManager()->mkArrayType(*indexSort
.d_type
, *elemSort
.d_type
));
5593 CVC5_API_TRY_CATCH_END
;
5596 Sort
Solver::mkBitVectorSort(uint32_t size
) const
5598 CVC5_API_TRY_CATCH_BEGIN
;
5599 CVC5_API_ARG_CHECK_EXPECTED(size
> 0, size
) << "size > 0";
5600 //////// all checks before this line
5601 return Sort(this, getNodeManager()->mkBitVectorType(size
));
5603 CVC5_API_TRY_CATCH_END
;
5606 Sort
Solver::mkFloatingPointSort(uint32_t exp
, uint32_t sig
) const
5608 CVC5_API_TRY_CATCH_BEGIN
;
5609 CVC5_API_ARG_CHECK_EXPECTED(exp
> 0, exp
) << "exponent size > 0";
5610 CVC5_API_ARG_CHECK_EXPECTED(sig
> 0, sig
) << "significand size > 0";
5611 //////// all checks before this line
5612 return Sort(this, getNodeManager()->mkFloatingPointType(exp
, sig
));
5614 CVC5_API_TRY_CATCH_END
;
5617 Sort
Solver::mkDatatypeSort(const DatatypeDecl
& dtypedecl
) const
5619 CVC5_API_TRY_CATCH_BEGIN
;
5620 CVC5_API_SOLVER_CHECK_DTDECL(dtypedecl
);
5621 //////// all checks before this line
5622 return Sort(this, getNodeManager()->mkDatatypeType(*dtypedecl
.d_dtype
));
5624 CVC5_API_TRY_CATCH_END
;
5627 std::vector
<Sort
> Solver::mkDatatypeSorts(
5628 const std::vector
<DatatypeDecl
>& dtypedecls
) const
5630 CVC5_API_SOLVER_CHECK_DTDECLS(dtypedecls
);
5631 CVC5_API_TRY_CATCH_BEGIN
;
5632 //////// all checks before this line
5633 return mkDatatypeSortsInternal(dtypedecls
, {});
5635 CVC5_API_TRY_CATCH_END
;
5638 std::vector
<Sort
> Solver::mkDatatypeSorts(
5639 const std::vector
<DatatypeDecl
>& dtypedecls
,
5640 const std::set
<Sort
>& unresolvedSorts
) const
5642 CVC5_API_TRY_CATCH_BEGIN
;
5643 CVC5_API_SOLVER_CHECK_DTDECLS(dtypedecls
);
5644 CVC5_API_SOLVER_CHECK_SORTS(unresolvedSorts
);
5645 //////// all checks before this line
5646 return mkDatatypeSortsInternal(dtypedecls
, unresolvedSorts
);
5648 CVC5_API_TRY_CATCH_END
;
5651 Sort
Solver::mkFunctionSort(const Sort
& domain
, const Sort
& codomain
) const
5653 CVC5_API_TRY_CATCH_BEGIN
;
5654 CVC5_API_SOLVER_CHECK_DOMAIN_SORT(domain
);
5655 CVC5_API_SOLVER_CHECK_CODOMAIN_SORT(codomain
);
5656 //////// all checks before this line
5658 this, getNodeManager()->mkFunctionType(*domain
.d_type
, *codomain
.d_type
));
5660 CVC5_API_TRY_CATCH_END
;
5663 Sort
Solver::mkFunctionSort(const std::vector
<Sort
>& sorts
,
5664 const Sort
& codomain
) const
5666 CVC5_API_TRY_CATCH_BEGIN
;
5667 CVC5_API_ARG_SIZE_CHECK_EXPECTED(sorts
.size() >= 1, sorts
)
5668 << "at least one parameter sort for function sort";
5669 CVC5_API_SOLVER_CHECK_DOMAIN_SORTS(sorts
);
5670 CVC5_API_SOLVER_CHECK_CODOMAIN_SORT(codomain
);
5671 //////// all checks before this line
5672 std::vector
<TypeNode
> argTypes
= Sort::sortVectorToTypeNodes(sorts
);
5674 getNodeManager()->mkFunctionType(argTypes
, *codomain
.d_type
));
5676 CVC5_API_TRY_CATCH_END
;
5679 Sort
Solver::mkParamSort(const std::string
& symbol
) const
5681 CVC5_API_TRY_CATCH_BEGIN
;
5682 //////// all checks before this line
5685 getNodeManager()->mkSort(symbol
, NodeManager::SORT_FLAG_PLACEHOLDER
));
5687 CVC5_API_TRY_CATCH_END
;
5690 Sort
Solver::mkPredicateSort(const std::vector
<Sort
>& sorts
) const
5692 CVC5_API_TRY_CATCH_BEGIN
;
5693 CVC5_API_ARG_SIZE_CHECK_EXPECTED(sorts
.size() >= 1, sorts
)
5694 << "at least one parameter sort for predicate sort";
5695 CVC5_API_SOLVER_CHECK_DOMAIN_SORTS(sorts
);
5696 //////// all checks before this line
5699 getNodeManager()->mkPredicateType(Sort::sortVectorToTypeNodes(sorts
)));
5701 CVC5_API_TRY_CATCH_END
;
5704 Sort
Solver::mkRecordSort(
5705 const std::vector
<std::pair
<std::string
, Sort
>>& fields
) const
5707 CVC5_API_TRY_CATCH_BEGIN
;
5708 std::vector
<std::pair
<std::string
, TypeNode
>> f
;
5709 for (size_t i
= 0, size
= fields
.size(); i
< size
; ++i
)
5711 const auto& p
= fields
[i
];
5712 CVC5_API_ARG_AT_INDEX_CHECK_EXPECTED(!p
.second
.isNull(), "sort", fields
, i
)
5714 CVC5_API_ARG_AT_INDEX_CHECK_EXPECTED(
5715 this == p
.second
.d_solver
, "sort", fields
, i
)
5716 << "sort associated with this solver object";
5717 f
.emplace_back(p
.first
, *p
.second
.d_type
);
5719 //////// all checks before this line
5720 return Sort(this, getNodeManager()->mkRecordType(f
));
5722 CVC5_API_TRY_CATCH_END
;
5725 Sort
Solver::mkSetSort(const Sort
& elemSort
) const
5727 CVC5_API_TRY_CATCH_BEGIN
;
5728 CVC5_API_SOLVER_CHECK_SORT(elemSort
);
5729 //////// all checks before this line
5730 return Sort(this, getNodeManager()->mkSetType(*elemSort
.d_type
));
5732 CVC5_API_TRY_CATCH_END
;
5735 Sort
Solver::mkBagSort(const Sort
& elemSort
) const
5737 CVC5_API_TRY_CATCH_BEGIN
;
5738 CVC5_API_SOLVER_CHECK_SORT(elemSort
);
5739 //////// all checks before this line
5740 return Sort(this, getNodeManager()->mkBagType(*elemSort
.d_type
));
5742 CVC5_API_TRY_CATCH_END
;
5745 Sort
Solver::mkSequenceSort(const Sort
& elemSort
) const
5747 CVC5_API_TRY_CATCH_BEGIN
;
5748 CVC5_API_SOLVER_CHECK_SORT(elemSort
);
5749 //////// all checks before this line
5750 return Sort(this, getNodeManager()->mkSequenceType(*elemSort
.d_type
));
5752 CVC5_API_TRY_CATCH_END
;
5755 Sort
Solver::mkUninterpretedSort(const std::string
& symbol
) const
5757 CVC5_API_TRY_CATCH_BEGIN
;
5758 //////// all checks before this line
5759 return Sort(this, getNodeManager()->mkSort(symbol
));
5761 CVC5_API_TRY_CATCH_END
;
5764 Sort
Solver::mkUnresolvedSort(const std::string
& symbol
, size_t arity
) const
5766 CVC5_API_TRY_CATCH_BEGIN
;
5767 //////// all checks before this line
5770 return Sort(this, getNodeManager()->mkSortConstructor(symbol
, arity
));
5772 return Sort(this, getNodeManager()->mkSort(symbol
));
5774 CVC5_API_TRY_CATCH_END
;
5777 Sort
Solver::mkSortConstructorSort(const std::string
& symbol
,
5780 CVC5_API_TRY_CATCH_BEGIN
;
5781 CVC5_API_ARG_CHECK_EXPECTED(arity
> 0, arity
) << "an arity > 0";
5782 //////// all checks before this line
5783 return Sort(this, getNodeManager()->mkSortConstructor(symbol
, arity
));
5785 CVC5_API_TRY_CATCH_END
;
5788 Sort
Solver::mkTupleSort(const std::vector
<Sort
>& sorts
) const
5790 CVC5_API_TRY_CATCH_BEGIN
;
5791 CVC5_API_SOLVER_CHECK_SORTS_NOT_FUNCTION_LIKE(sorts
);
5792 //////// all checks before this line
5793 return mkTupleSortHelper(sorts
);
5795 CVC5_API_TRY_CATCH_END
;
5799 /* -------------------------------------------------------------------------- */
5801 Term
Solver::mkTrue(void) const
5803 CVC5_API_TRY_CATCH_BEGIN
;
5804 //////// all checks before this line
5805 return Term(this, d_nodeMgr
->mkConst
<bool>(true));
5807 CVC5_API_TRY_CATCH_END
;
5810 Term
Solver::mkFalse(void) const
5812 CVC5_API_TRY_CATCH_BEGIN
;
5813 //////// all checks before this line
5814 return Term(this, d_nodeMgr
->mkConst
<bool>(false));
5816 CVC5_API_TRY_CATCH_END
;
5819 Term
Solver::mkBoolean(bool val
) const
5821 CVC5_API_TRY_CATCH_BEGIN
;
5822 //////// all checks before this line
5823 return Term(this, d_nodeMgr
->mkConst
<bool>(val
));
5825 CVC5_API_TRY_CATCH_END
;
5828 Term
Solver::mkPi() const
5830 CVC5_API_TRY_CATCH_BEGIN
;
5831 //////// all checks before this line
5833 d_nodeMgr
->mkNullaryOperator(d_nodeMgr
->realType(), cvc5::kind::PI
);
5834 (void)res
.getType(true); /* kick off type checking */
5835 return Term(this, res
);
5837 CVC5_API_TRY_CATCH_END
;
5840 Term
Solver::mkInteger(const std::string
& s
) const
5842 CVC5_API_TRY_CATCH_BEGIN
;
5843 CVC5_API_ARG_CHECK_EXPECTED(isValidInteger(s
), s
) << " an integer ";
5844 Term integer
= mkRealOrIntegerFromStrHelper(s
);
5845 CVC5_API_ARG_CHECK_EXPECTED(integer
.getSort() == getIntegerSort(), s
)
5846 << " a string representing an integer";
5847 //////// all checks before this line
5850 CVC5_API_TRY_CATCH_END
;
5853 Term
Solver::mkInteger(int64_t val
) const
5855 CVC5_API_TRY_CATCH_BEGIN
;
5856 //////// all checks before this line
5857 Term integer
= mkRationalValHelper(cvc5::Rational(val
));
5858 Assert(integer
.getSort() == getIntegerSort());
5861 CVC5_API_TRY_CATCH_END
;
5864 Term
Solver::mkReal(const std::string
& s
) const
5866 CVC5_API_TRY_CATCH_BEGIN
;
5867 /* CLN and GMP handle this case differently, CLN interprets it as 0, GMP
5868 * throws an std::invalid_argument exception. For consistency, we treat it
5870 CVC5_API_ARG_CHECK_EXPECTED(s
!= ".", s
)
5871 << "a string representing a real or rational value.";
5872 //////// all checks before this line
5873 return mkRealOrIntegerFromStrHelper(s
, false);
5875 CVC5_API_TRY_CATCH_END
;
5878 Term
Solver::mkReal(int64_t val
) const
5880 CVC5_API_TRY_CATCH_BEGIN
;
5881 //////// all checks before this line
5882 return mkRationalValHelper(cvc5::Rational(val
), false);
5884 CVC5_API_TRY_CATCH_END
;
5887 Term
Solver::mkReal(int64_t num
, int64_t den
) const
5889 CVC5_API_TRY_CATCH_BEGIN
;
5890 //////// all checks before this line
5891 return mkRationalValHelper(cvc5::Rational(num
, den
), false);
5893 CVC5_API_TRY_CATCH_END
;
5896 Term
Solver::mkRegexpAll() const
5898 CVC5_API_TRY_CATCH_BEGIN
;
5899 //////// all checks before this line
5900 Node res
= d_nodeMgr
->mkNode(
5901 cvc5::kind::REGEXP_STAR
,
5902 d_nodeMgr
->mkNode(cvc5::kind::REGEXP_ALLCHAR
, std::vector
<cvc5::Node
>()));
5903 (void)res
.getType(true); /* kick off type checking */
5904 return Term(this, res
);
5906 CVC5_API_TRY_CATCH_END
;
5909 Term
Solver::mkRegexpNone() const
5911 CVC5_API_TRY_CATCH_BEGIN
;
5912 //////// all checks before this line
5914 d_nodeMgr
->mkNode(cvc5::kind::REGEXP_NONE
, std::vector
<cvc5::Node
>());
5915 (void)res
.getType(true); /* kick off type checking */
5916 return Term(this, res
);
5918 CVC5_API_TRY_CATCH_END
;
5921 Term
Solver::mkRegexpAllchar() const
5923 CVC5_API_TRY_CATCH_BEGIN
;
5924 //////// all checks before this line
5926 d_nodeMgr
->mkNode(cvc5::kind::REGEXP_ALLCHAR
, std::vector
<cvc5::Node
>());
5927 (void)res
.getType(true); /* kick off type checking */
5928 return Term(this, res
);
5930 CVC5_API_TRY_CATCH_END
;
5933 Term
Solver::mkEmptySet(const Sort
& sort
) const
5935 CVC5_API_TRY_CATCH_BEGIN
;
5936 CVC5_API_ARG_CHECK_EXPECTED(sort
.isNull() || sort
.isSet(), sort
)
5937 << "null sort or set sort";
5938 CVC5_API_ARG_CHECK_EXPECTED(sort
.isNull() || this == sort
.d_solver
, sort
)
5939 << "set sort associated with this solver object";
5940 //////// all checks before this line
5941 return mkValHelper
<cvc5::EmptySet
>(cvc5::EmptySet(*sort
.d_type
));
5943 CVC5_API_TRY_CATCH_END
;
5946 Term
Solver::mkEmptyBag(const Sort
& sort
) const
5948 CVC5_API_TRY_CATCH_BEGIN
;
5949 CVC5_API_ARG_CHECK_EXPECTED(sort
.isNull() || sort
.isBag(), sort
)
5950 << "null sort or bag sort";
5951 CVC5_API_ARG_CHECK_EXPECTED(sort
.isNull() || this == sort
.d_solver
, sort
)
5952 << "bag sort associated with this solver object";
5953 //////// all checks before this line
5954 return mkValHelper
<cvc5::EmptyBag
>(cvc5::EmptyBag(*sort
.d_type
));
5956 CVC5_API_TRY_CATCH_END
;
5959 Term
Solver::mkSepEmp() const
5961 CVC5_API_TRY_CATCH_BEGIN
;
5962 //////// all checks before this line
5963 Node res
= getNodeManager()->mkNullaryOperator(d_nodeMgr
->booleanType(),
5964 cvc5::Kind::SEP_EMP
);
5965 (void)res
.getType(true); /* kick off type checking */
5966 return Term(this, res
);
5968 CVC5_API_TRY_CATCH_END
;
5971 Term
Solver::mkSepNil(const Sort
& sort
) const
5973 CVC5_API_TRY_CATCH_BEGIN
;
5974 CVC5_API_SOLVER_CHECK_SORT(sort
);
5975 //////// all checks before this line
5977 getNodeManager()->mkNullaryOperator(*sort
.d_type
, cvc5::kind::SEP_NIL
);
5978 (void)res
.getType(true); /* kick off type checking */
5979 return Term(this, res
);
5981 CVC5_API_TRY_CATCH_END
;
5984 Term
Solver::mkString(const std::string
& s
, bool useEscSequences
) const
5986 CVC5_API_TRY_CATCH_BEGIN
;
5987 //////// all checks before this line
5988 return mkValHelper
<cvc5::String
>(cvc5::String(s
, useEscSequences
));
5990 CVC5_API_TRY_CATCH_END
;
5993 Term
Solver::mkString(const std::wstring
& s
) const
5995 CVC5_API_TRY_CATCH_BEGIN
;
5996 //////// all checks before this line
5997 return mkValHelper
<cvc5::String
>(cvc5::String(s
));
5999 CVC5_API_TRY_CATCH_END
;
6002 Term
Solver::mkEmptySequence(const Sort
& sort
) const
6004 CVC5_API_TRY_CATCH_BEGIN
;
6005 CVC5_API_SOLVER_CHECK_SORT(sort
);
6006 //////// all checks before this line
6007 std::vector
<Node
> seq
;
6008 Node res
= d_nodeMgr
->mkConst(Sequence(*sort
.d_type
, seq
));
6009 return Term(this, res
);
6011 CVC5_API_TRY_CATCH_END
;
6014 Term
Solver::mkUniverseSet(const Sort
& sort
) const
6016 CVC5_API_TRY_CATCH_BEGIN
;
6017 CVC5_API_SOLVER_CHECK_SORT(sort
);
6018 //////// all checks before this line
6020 Node res
= getNodeManager()->mkNullaryOperator(*sort
.d_type
,
6021 cvc5::kind::SET_UNIVERSE
);
6022 // TODO(#2771): Reenable?
6023 // (void)res->getType(true); /* kick off type checking */
6024 return Term(this, res
);
6026 CVC5_API_TRY_CATCH_END
;
6029 Term
Solver::mkBitVector(uint32_t size
, uint64_t val
) const
6031 CVC5_API_TRY_CATCH_BEGIN
;
6032 //////// all checks before this line
6033 return mkBVFromIntHelper(size
, val
);
6035 CVC5_API_TRY_CATCH_END
;
6038 Term
Solver::mkBitVector(uint32_t size
,
6039 const std::string
& s
,
6040 uint32_t base
) const
6042 CVC5_API_TRY_CATCH_BEGIN
;
6043 //////// all checks before this line
6044 return mkBVFromStrHelper(size
, s
, base
);
6046 CVC5_API_TRY_CATCH_END
;
6049 Term
Solver::mkConstArray(const Sort
& sort
, const Term
& val
) const
6051 CVC5_API_TRY_CATCH_BEGIN
;
6052 CVC5_API_SOLVER_CHECK_SORT(sort
);
6053 CVC5_API_SOLVER_CHECK_TERM(val
);
6054 CVC5_API_ARG_CHECK_EXPECTED(sort
.isArray(), sort
) << "an array sort";
6055 CVC5_API_CHECK(val
.getSort().isSubsortOf(sort
.getArrayElementSort()))
6056 << "Value does not match element sort";
6057 //////// all checks before this line
6059 // handle the special case of (CAST_TO_REAL n) where n is an integer
6060 Node n
= *val
.d_node
;
6061 if (val
.isCastedReal())
6063 // this is safe because the constant array stores its type
6067 mkValHelper
<cvc5::ArrayStoreAll
>(cvc5::ArrayStoreAll(*sort
.d_type
, n
));
6070 CVC5_API_TRY_CATCH_END
;
6073 Term
Solver::mkPosInf(uint32_t exp
, uint32_t sig
) const
6075 CVC5_API_TRY_CATCH_BEGIN
;
6076 //////// all checks before this line
6077 return mkValHelper
<cvc5::FloatingPoint
>(
6078 FloatingPoint::makeInf(FloatingPointSize(exp
, sig
), false));
6080 CVC5_API_TRY_CATCH_END
;
6083 Term
Solver::mkNegInf(uint32_t exp
, uint32_t sig
) const
6085 CVC5_API_TRY_CATCH_BEGIN
;
6086 //////// all checks before this line
6087 return mkValHelper
<cvc5::FloatingPoint
>(
6088 FloatingPoint::makeInf(FloatingPointSize(exp
, sig
), true));
6090 CVC5_API_TRY_CATCH_END
;
6093 Term
Solver::mkNaN(uint32_t exp
, uint32_t sig
) const
6095 CVC5_API_TRY_CATCH_BEGIN
;
6096 //////// all checks before this line
6097 return mkValHelper
<cvc5::FloatingPoint
>(
6098 FloatingPoint::makeNaN(FloatingPointSize(exp
, sig
)));
6100 CVC5_API_TRY_CATCH_END
;
6103 Term
Solver::mkPosZero(uint32_t exp
, uint32_t sig
) const
6105 CVC5_API_TRY_CATCH_BEGIN
;
6106 //////// all checks before this line
6107 return mkValHelper
<cvc5::FloatingPoint
>(
6108 FloatingPoint::makeZero(FloatingPointSize(exp
, sig
), false));
6110 CVC5_API_TRY_CATCH_END
;
6113 Term
Solver::mkNegZero(uint32_t exp
, uint32_t sig
) const
6115 CVC5_API_TRY_CATCH_BEGIN
;
6116 //////// all checks before this line
6117 return mkValHelper
<cvc5::FloatingPoint
>(
6118 FloatingPoint::makeZero(FloatingPointSize(exp
, sig
), true));
6120 CVC5_API_TRY_CATCH_END
;
6123 Term
Solver::mkRoundingMode(RoundingMode rm
) const
6125 CVC5_API_TRY_CATCH_BEGIN
;
6126 //////// all checks before this line
6127 return mkValHelper
<cvc5::RoundingMode
>(s_rmodes
.at(rm
));
6129 CVC5_API_TRY_CATCH_END
;
6132 Term
Solver::mkUninterpretedConst(const Sort
& sort
, int32_t index
) const
6134 CVC5_API_TRY_CATCH_BEGIN
;
6135 CVC5_API_SOLVER_CHECK_SORT(sort
);
6136 //////// all checks before this line
6137 return mkValHelper
<cvc5::UninterpretedConstant
>(
6138 cvc5::UninterpretedConstant(*sort
.d_type
, index
));
6140 CVC5_API_TRY_CATCH_END
;
6143 Term
Solver::mkAbstractValue(const std::string
& index
) const
6145 CVC5_API_TRY_CATCH_BEGIN
;
6146 CVC5_API_ARG_CHECK_EXPECTED(!index
.empty(), index
) << "a non-empty string";
6148 cvc5::Integer
idx(index
, 10);
6149 CVC5_API_ARG_CHECK_EXPECTED(idx
> 0, index
)
6150 << "a string representing an integer > 0";
6151 //////// all checks before this line
6152 return Term(this, getNodeManager()->mkConst(cvc5::AbstractValue(idx
)));
6153 // do not call getType(), for abstract values, type can not be computed
6154 // until it is substituted away
6156 CVC5_API_TRY_CATCH_END
;
6159 Term
Solver::mkAbstractValue(uint64_t index
) const
6161 CVC5_API_TRY_CATCH_BEGIN
;
6162 CVC5_API_ARG_CHECK_EXPECTED(index
> 0, index
) << "an integer > 0";
6163 //////// all checks before this line
6165 getNodeManager()->mkConst(cvc5::AbstractValue(Integer(index
))));
6166 // do not call getType(), for abstract values, type can not be computed
6167 // until it is substituted away
6169 CVC5_API_TRY_CATCH_END
;
6172 Term
Solver::mkFloatingPoint(uint32_t exp
, uint32_t sig
, Term val
) const
6174 CVC5_API_TRY_CATCH_BEGIN
;
6175 CVC5_API_SOLVER_CHECK_TERM(val
);
6176 CVC5_API_ARG_CHECK_EXPECTED(exp
> 0, exp
) << "a value > 0";
6177 CVC5_API_ARG_CHECK_EXPECTED(sig
> 0, sig
) << "a value > 0";
6178 uint32_t bw
= exp
+ sig
;
6179 CVC5_API_ARG_CHECK_EXPECTED(bw
== val
.d_node
->getType().getBitVectorSize(),
6181 << "a bit-vector constant with bit-width '" << bw
<< "'";
6182 CVC5_API_ARG_CHECK_EXPECTED(
6183 val
.d_node
->getType().isBitVector() && val
.d_node
->isConst(), val
)
6184 << "bit-vector constant";
6185 //////// all checks before this line
6186 return mkValHelper
<cvc5::FloatingPoint
>(
6187 cvc5::FloatingPoint(exp
, sig
, val
.d_node
->getConst
<BitVector
>()));
6189 CVC5_API_TRY_CATCH_END
;
6192 Term
Solver::mkCardinalityConstraint(const Sort
& sort
, uint32_t upperBound
) const
6194 CVC5_API_TRY_CATCH_BEGIN
;
6195 CVC5_API_SOLVER_CHECK_SORT(sort
);
6196 CVC5_API_ARG_CHECK_EXPECTED(sort
.isUninterpretedSort(), sort
)
6197 << "an uninterpreted sort";
6198 CVC5_API_ARG_CHECK_EXPECTED(upperBound
> 0, upperBound
) << "a value > 0";
6199 //////// all checks before this line
6201 d_nodeMgr
->mkConst(cvc5::CardinalityConstraint(*sort
.d_type
, upperBound
));
6202 Node cc
= d_nodeMgr
->mkNode(cvc5::Kind::CARDINALITY_CONSTRAINT
, cco
);
6203 return Term(this, cc
);
6205 CVC5_API_TRY_CATCH_END
;
6208 /* Create constants */
6209 /* -------------------------------------------------------------------------- */
6211 Term
Solver::mkConst(const Sort
& sort
, const std::string
& symbol
) const
6213 CVC5_API_TRY_CATCH_BEGIN
;
6214 CVC5_API_SOLVER_CHECK_SORT(sort
);
6215 //////// all checks before this line
6216 Node res
= d_nodeMgr
->mkVar(symbol
, *sort
.d_type
);
6217 (void)res
.getType(true); /* kick off type checking */
6218 increment_vars_consts_stats(sort
, false);
6219 return Term(this, res
);
6221 CVC5_API_TRY_CATCH_END
;
6224 Term
Solver::mkConst(const Sort
& sort
) const
6226 CVC5_API_TRY_CATCH_BEGIN
;
6227 CVC5_API_SOLVER_CHECK_SORT(sort
);
6228 //////// all checks before this line
6229 Node res
= d_nodeMgr
->mkVar(*sort
.d_type
);
6230 (void)res
.getType(true); /* kick off type checking */
6231 increment_vars_consts_stats(sort
, false);
6232 return Term(this, res
);
6234 CVC5_API_TRY_CATCH_END
;
6237 /* Create variables */
6238 /* -------------------------------------------------------------------------- */
6240 Term
Solver::mkVar(const Sort
& sort
, const std::string
& symbol
) const
6242 CVC5_API_TRY_CATCH_BEGIN
;
6243 CVC5_API_SOLVER_CHECK_SORT(sort
);
6244 //////// all checks before this line
6245 Node res
= symbol
.empty() ? d_nodeMgr
->mkBoundVar(*sort
.d_type
)
6246 : d_nodeMgr
->mkBoundVar(symbol
, *sort
.d_type
);
6247 (void)res
.getType(true); /* kick off type checking */
6248 increment_vars_consts_stats(sort
, true);
6249 return Term(this, res
);
6251 CVC5_API_TRY_CATCH_END
;
6254 /* Create datatype constructor declarations */
6255 /* -------------------------------------------------------------------------- */
6257 DatatypeConstructorDecl
Solver::mkDatatypeConstructorDecl(
6258 const std::string
& name
)
6260 CVC5_API_TRY_CATCH_BEGIN
;
6261 //////// all checks before this line
6262 return DatatypeConstructorDecl(this, name
);
6264 CVC5_API_TRY_CATCH_END
;
6267 /* Create datatype declarations */
6268 /* -------------------------------------------------------------------------- */
6270 DatatypeDecl
Solver::mkDatatypeDecl(const std::string
& name
, bool isCoDatatype
)
6272 CVC5_API_TRY_CATCH_BEGIN
;
6273 //////// all checks before this line
6274 return DatatypeDecl(this, name
, isCoDatatype
);
6276 CVC5_API_TRY_CATCH_END
;
6279 DatatypeDecl
Solver::mkDatatypeDecl(const std::string
& name
,
6283 CVC5_API_TRY_CATCH_BEGIN
;
6284 CVC5_API_SOLVER_CHECK_SORT(param
);
6285 //////// all checks before this line
6286 return DatatypeDecl(this, name
, param
, isCoDatatype
);
6288 CVC5_API_TRY_CATCH_END
;
6291 DatatypeDecl
Solver::mkDatatypeDecl(const std::string
& name
,
6292 const std::vector
<Sort
>& params
,
6295 CVC5_API_TRY_CATCH_BEGIN
;
6296 CVC5_API_SOLVER_CHECK_SORTS(params
);
6297 //////// all checks before this line
6298 return DatatypeDecl(this, name
, params
, isCoDatatype
);
6300 CVC5_API_TRY_CATCH_END
;
6304 /* -------------------------------------------------------------------------- */
6306 Term
Solver::mkTerm(Kind kind
) const
6308 CVC5_API_TRY_CATCH_BEGIN
;
6309 CVC5_API_KIND_CHECK(kind
);
6310 //////// all checks before this line
6311 return mkTermFromKind(kind
);
6313 CVC5_API_TRY_CATCH_END
;
6316 Term
Solver::mkTerm(Kind kind
, const Term
& child
) const
6318 CVC5_API_TRY_CATCH_BEGIN
;
6319 CVC5_API_KIND_CHECK(kind
);
6320 CVC5_API_SOLVER_CHECK_TERM(child
);
6321 //////// all checks before this line
6322 return mkTermHelper(kind
, std::vector
<Term
>{child
});
6324 CVC5_API_TRY_CATCH_END
;
6327 Term
Solver::mkTerm(Kind kind
, const Term
& child1
, const Term
& child2
) const
6329 CVC5_API_TRY_CATCH_BEGIN
;
6330 CVC5_API_KIND_CHECK(kind
);
6331 CVC5_API_SOLVER_CHECK_TERM(child1
);
6332 CVC5_API_SOLVER_CHECK_TERM(child2
);
6333 //////// all checks before this line
6334 return mkTermHelper(kind
, std::vector
<Term
>{child1
, child2
});
6336 CVC5_API_TRY_CATCH_END
;
6339 Term
Solver::mkTerm(Kind kind
,
6342 const Term
& child3
) const
6344 CVC5_API_TRY_CATCH_BEGIN
;
6345 CVC5_API_KIND_CHECK(kind
);
6346 CVC5_API_SOLVER_CHECK_TERM(child1
);
6347 CVC5_API_SOLVER_CHECK_TERM(child2
);
6348 CVC5_API_SOLVER_CHECK_TERM(child3
);
6349 //////// all checks before this line
6350 // need to use internal term call to check e.g. associative construction
6351 return mkTermHelper(kind
, std::vector
<Term
>{child1
, child2
, child3
});
6353 CVC5_API_TRY_CATCH_END
;
6356 Term
Solver::mkTerm(Kind kind
, const std::vector
<Term
>& children
) const
6358 CVC5_API_TRY_CATCH_BEGIN
;
6359 CVC5_API_KIND_CHECK(kind
);
6360 CVC5_API_SOLVER_CHECK_TERMS(children
);
6361 //////// all checks before this line
6362 return mkTermHelper(kind
, children
);
6364 CVC5_API_TRY_CATCH_END
;
6367 Term
Solver::mkTerm(const Op
& op
) const
6369 CVC5_API_TRY_CATCH_BEGIN
;
6370 CVC5_API_SOLVER_CHECK_OP(op
);
6371 if (!op
.isIndexedHelper())
6373 return mkTermFromKind(op
.d_kind
);
6375 checkMkTerm(op
.d_kind
, 0);
6376 //////// all checks before this line
6377 const cvc5::Kind int_kind
= extToIntKind(op
.d_kind
);
6378 Term res
= Term(this, getNodeManager()->mkNode(int_kind
, *op
.d_node
));
6380 (void)res
.d_node
->getType(true); /* kick off type checking */
6383 CVC5_API_TRY_CATCH_END
;
6386 Term
Solver::mkTerm(const Op
& op
, const Term
& child
) const
6388 CVC5_API_TRY_CATCH_BEGIN
;
6389 CVC5_API_SOLVER_CHECK_OP(op
);
6390 CVC5_API_SOLVER_CHECK_TERM(child
);
6391 //////// all checks before this line
6392 return mkTermHelper(op
, std::vector
<Term
>{child
});
6394 CVC5_API_TRY_CATCH_END
;
6397 Term
Solver::mkTerm(const Op
& op
, const Term
& child1
, const Term
& child2
) const
6399 CVC5_API_TRY_CATCH_BEGIN
;
6400 CVC5_API_SOLVER_CHECK_OP(op
);
6401 CVC5_API_SOLVER_CHECK_TERM(child1
);
6402 CVC5_API_SOLVER_CHECK_TERM(child2
);
6403 //////// all checks before this line
6404 return mkTermHelper(op
, std::vector
<Term
>{child1
, child2
});
6406 CVC5_API_TRY_CATCH_END
;
6409 Term
Solver::mkTerm(const Op
& op
,
6412 const Term
& child3
) const
6414 CVC5_API_TRY_CATCH_BEGIN
;
6415 CVC5_API_SOLVER_CHECK_OP(op
);
6416 CVC5_API_SOLVER_CHECK_TERM(child1
);
6417 CVC5_API_SOLVER_CHECK_TERM(child2
);
6418 CVC5_API_SOLVER_CHECK_TERM(child3
);
6419 //////// all checks before this line
6420 return mkTermHelper(op
, std::vector
<Term
>{child1
, child2
, child3
});
6422 CVC5_API_TRY_CATCH_END
;
6425 Term
Solver::mkTerm(const Op
& op
, const std::vector
<Term
>& children
) const
6427 CVC5_API_TRY_CATCH_BEGIN
;
6428 CVC5_API_SOLVER_CHECK_OP(op
);
6429 CVC5_API_SOLVER_CHECK_TERMS(children
);
6430 //////// all checks before this line
6431 return mkTermHelper(op
, children
);
6433 CVC5_API_TRY_CATCH_END
;
6436 Term
Solver::mkTuple(const std::vector
<Sort
>& sorts
,
6437 const std::vector
<Term
>& terms
) const
6439 CVC5_API_TRY_CATCH_BEGIN
;
6440 CVC5_API_CHECK(sorts
.size() == terms
.size())
6441 << "Expected the same number of sorts and elements";
6442 CVC5_API_SOLVER_CHECK_SORTS(sorts
);
6443 CVC5_API_SOLVER_CHECK_TERMS(terms
);
6444 //////// all checks before this line
6445 std::vector
<cvc5::Node
> args
;
6446 for (size_t i
= 0, size
= sorts
.size(); i
< size
; i
++)
6448 args
.push_back(*(ensureTermSort(terms
[i
], sorts
[i
])).d_node
);
6451 Sort s
= mkTupleSortHelper(sorts
);
6452 Datatype dt
= s
.getDatatype();
6453 NodeBuilder
nb(extToIntKind(APPLY_CONSTRUCTOR
));
6454 nb
<< *dt
[0].getConstructorTerm().d_node
;
6456 Node res
= nb
.constructNode();
6457 (void)res
.getType(true); /* kick off type checking */
6458 return Term(this, res
);
6460 CVC5_API_TRY_CATCH_END
;
6463 /* Create operators */
6464 /* -------------------------------------------------------------------------- */
6466 Op
Solver::mkOp(Kind kind
) const
6468 CVC5_API_TRY_CATCH_BEGIN
;
6469 CVC5_API_KIND_CHECK(kind
);
6470 CVC5_API_CHECK(s_indexed_kinds
.find(kind
) == s_indexed_kinds
.end())
6471 << "Expected a kind for a non-indexed operator.";
6472 //////// all checks before this line
6473 return Op(this, kind
);
6475 CVC5_API_TRY_CATCH_END
6478 Op
Solver::mkOp(Kind kind
, const std::string
& arg
) const
6480 CVC5_API_TRY_CATCH_BEGIN
;
6481 CVC5_API_KIND_CHECK(kind
);
6482 CVC5_API_KIND_CHECK_EXPECTED((kind
== DIVISIBLE
), kind
) << "DIVISIBLE";
6483 //////// all checks before this line
6485 /* CLN and GMP handle this case differently, CLN interprets it as 0, GMP
6486 * throws an std::invalid_argument exception. For consistency, we treat it
6488 CVC5_API_ARG_CHECK_EXPECTED(arg
!= ".", arg
)
6489 << "a string representing an integer, real or rational value.";
6492 *mkValHelper
<cvc5::Divisible
>(cvc5::Divisible(cvc5::Integer(arg
)))
6496 CVC5_API_TRY_CATCH_END
;
6499 Op
Solver::mkOp(Kind kind
, uint32_t arg
) const
6501 CVC5_API_TRY_CATCH_BEGIN
;
6502 CVC5_API_KIND_CHECK(kind
);
6503 //////// all checks before this line
6510 *mkValHelper
<cvc5::Divisible
>(cvc5::Divisible(arg
)).d_node
);
6512 case BITVECTOR_REPEAT
:
6515 *mkValHelper
<cvc5::BitVectorRepeat
>(cvc5::BitVectorRepeat(arg
))
6518 case BITVECTOR_ZERO_EXTEND
:
6521 *mkValHelper
<cvc5::BitVectorZeroExtend
>(
6522 cvc5::BitVectorZeroExtend(arg
))
6525 case BITVECTOR_SIGN_EXTEND
:
6528 *mkValHelper
<cvc5::BitVectorSignExtend
>(
6529 cvc5::BitVectorSignExtend(arg
))
6532 case BITVECTOR_ROTATE_LEFT
:
6535 *mkValHelper
<cvc5::BitVectorRotateLeft
>(
6536 cvc5::BitVectorRotateLeft(arg
))
6539 case BITVECTOR_ROTATE_RIGHT
:
6542 *mkValHelper
<cvc5::BitVectorRotateRight
>(
6543 cvc5::BitVectorRotateRight(arg
))
6546 case INT_TO_BITVECTOR
:
6550 *mkValHelper
<cvc5::IntToBitVector
>(cvc5::IntToBitVector(arg
)).d_node
);
6554 Op(this, kind
, *mkValHelper
<cvc5::IntAnd
>(cvc5::IntAnd(arg
)).d_node
);
6556 case FLOATINGPOINT_TO_UBV
:
6560 *mkValHelper
<cvc5::FloatingPointToUBV
>(cvc5::FloatingPointToUBV(arg
))
6563 case FLOATINGPOINT_TO_SBV
:
6567 *mkValHelper
<cvc5::FloatingPointToSBV
>(cvc5::FloatingPointToSBV(arg
))
6574 *mkValHelper
<cvc5::RegExpRepeat
>(cvc5::RegExpRepeat(arg
)).d_node
);
6577 CVC5_API_KIND_CHECK_EXPECTED(false, kind
)
6578 << "operator kind with uint32_t argument";
6580 Assert(!res
.isNull());
6583 CVC5_API_TRY_CATCH_END
;
6586 Op
Solver::mkOp(Kind kind
, uint32_t arg1
, uint32_t arg2
) const
6588 CVC5_API_TRY_CATCH_BEGIN
;
6589 CVC5_API_KIND_CHECK(kind
);
6590 //////// all checks before this line
6595 case BITVECTOR_EXTRACT
:
6598 *mkValHelper
<cvc5::BitVectorExtract
>(
6599 cvc5::BitVectorExtract(arg1
, arg2
))
6602 case FLOATINGPOINT_TO_FP_IEEE_BITVECTOR
:
6605 *mkValHelper
<cvc5::FloatingPointToFPIEEEBitVector
>(
6606 cvc5::FloatingPointToFPIEEEBitVector(arg1
, arg2
))
6609 case FLOATINGPOINT_TO_FP_FLOATINGPOINT
:
6612 *mkValHelper
<cvc5::FloatingPointToFPFloatingPoint
>(
6613 cvc5::FloatingPointToFPFloatingPoint(arg1
, arg2
))
6616 case FLOATINGPOINT_TO_FP_REAL
:
6619 *mkValHelper
<cvc5::FloatingPointToFPReal
>(
6620 cvc5::FloatingPointToFPReal(arg1
, arg2
))
6623 case FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR
:
6626 *mkValHelper
<cvc5::FloatingPointToFPSignedBitVector
>(
6627 cvc5::FloatingPointToFPSignedBitVector(arg1
, arg2
))
6630 case FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR
:
6633 *mkValHelper
<cvc5::FloatingPointToFPUnsignedBitVector
>(
6634 cvc5::FloatingPointToFPUnsignedBitVector(arg1
, arg2
))
6637 case FLOATINGPOINT_TO_FP_GENERIC
:
6640 *mkValHelper
<cvc5::FloatingPointToFPGeneric
>(
6641 cvc5::FloatingPointToFPGeneric(arg1
, arg2
))
6648 *mkValHelper
<cvc5::RegExpLoop
>(cvc5::RegExpLoop(arg1
, arg2
)).d_node
);
6651 CVC5_API_KIND_CHECK_EXPECTED(false, kind
)
6652 << "operator kind with two uint32_t arguments";
6654 Assert(!res
.isNull());
6657 CVC5_API_TRY_CATCH_END
;
6660 Op
Solver::mkOp(Kind kind
, const std::vector
<uint32_t>& args
) const
6662 CVC5_API_TRY_CATCH_BEGIN
;
6663 CVC5_API_KIND_CHECK(kind
);
6664 //////// all checks before this line
6673 *mkValHelper
<cvc5::TupleProjectOp
>(cvc5::TupleProjectOp(args
))
6679 std::string message
= "operator kind with " + std::to_string(args
.size())
6680 + " uint32_t arguments";
6681 CVC5_API_KIND_CHECK_EXPECTED(false, kind
) << message
;
6684 Assert(!res
.isNull());
6687 CVC5_API_TRY_CATCH_END
;
6690 /* Non-SMT-LIB commands */
6691 /* -------------------------------------------------------------------------- */
6693 Term
Solver::simplify(const Term
& term
)
6695 CVC5_API_TRY_CATCH_BEGIN
;
6696 CVC5_API_SOLVER_CHECK_TERM(term
);
6697 //////// all checks before this line
6698 return Term(this, d_slv
->simplify(*term
.d_node
));
6700 CVC5_API_TRY_CATCH_END
;
6703 Result
Solver::checkEntailed(const Term
& term
) const
6705 CVC5_API_TRY_CATCH_BEGIN
;
6706 CVC5_API_CHECK(!d_slv
->isQueryMade()
6707 || d_slv
->getOptions().base
.incrementalSolving
)
6708 << "Cannot make multiple queries unless incremental solving is enabled "
6709 "(try --incremental)";
6710 CVC5_API_SOLVER_CHECK_TERM(term
);
6711 //////// all checks before this line
6712 return d_slv
->checkEntailed(*term
.d_node
);
6714 CVC5_API_TRY_CATCH_END
;
6717 Result
Solver::checkEntailed(const std::vector
<Term
>& terms
) const
6719 CVC5_API_TRY_CATCH_BEGIN
;
6720 CVC5_API_CHECK(!d_slv
->isQueryMade()
6721 || d_slv
->getOptions().base
.incrementalSolving
)
6722 << "Cannot make multiple queries unless incremental solving is enabled "
6723 "(try --incremental)";
6724 CVC5_API_SOLVER_CHECK_TERMS(terms
);
6725 //////// all checks before this line
6726 return d_slv
->checkEntailed(Term::termVectorToNodes(terms
));
6728 CVC5_API_TRY_CATCH_END
;
6731 /* SMT-LIB commands */
6732 /* -------------------------------------------------------------------------- */
6734 void Solver::assertFormula(const Term
& term
) const
6736 CVC5_API_TRY_CATCH_BEGIN
;
6737 CVC5_API_SOLVER_CHECK_TERM(term
);
6738 CVC5_API_SOLVER_CHECK_TERM_WITH_SORT(term
, getBooleanSort());
6739 //////// all checks before this line
6740 d_slv
->assertFormula(*term
.d_node
);
6742 CVC5_API_TRY_CATCH_END
;
6745 Result
Solver::checkSat(void) const
6747 CVC5_API_TRY_CATCH_BEGIN
;
6748 CVC5_API_CHECK(!d_slv
->isQueryMade()
6749 || d_slv
->getOptions().base
.incrementalSolving
)
6750 << "Cannot make multiple queries unless incremental solving is enabled "
6751 "(try --incremental)";
6752 //////// all checks before this line
6753 return d_slv
->checkSat();
6755 CVC5_API_TRY_CATCH_END
;
6758 Result
Solver::checkSatAssuming(const Term
& assumption
) const
6760 CVC5_API_TRY_CATCH_BEGIN
;
6761 CVC5_API_CHECK(!d_slv
->isQueryMade()
6762 || d_slv
->getOptions().base
.incrementalSolving
)
6763 << "Cannot make multiple queries unless incremental solving is enabled "
6764 "(try --incremental)";
6765 CVC5_API_SOLVER_CHECK_TERM_WITH_SORT(assumption
, getBooleanSort());
6766 //////// all checks before this line
6767 return d_slv
->checkSat(*assumption
.d_node
);
6769 CVC5_API_TRY_CATCH_END
;
6772 Result
Solver::checkSatAssuming(const std::vector
<Term
>& assumptions
) const
6774 CVC5_API_TRY_CATCH_BEGIN
;
6775 CVC5_API_CHECK(!d_slv
->isQueryMade() || assumptions
.size() == 0
6776 || d_slv
->getOptions().base
.incrementalSolving
)
6777 << "Cannot make multiple queries unless incremental solving is enabled "
6778 "(try --incremental)";
6779 CVC5_API_SOLVER_CHECK_TERMS_WITH_SORT(assumptions
, getBooleanSort());
6780 //////// all checks before this line
6781 for (const Term
& term
: assumptions
)
6783 CVC5_API_SOLVER_CHECK_TERM(term
);
6785 std::vector
<Node
> eassumptions
= Term::termVectorToNodes(assumptions
);
6786 return d_slv
->checkSat(eassumptions
);
6788 CVC5_API_TRY_CATCH_END
;
6791 Sort
Solver::declareDatatype(
6792 const std::string
& symbol
,
6793 const std::vector
<DatatypeConstructorDecl
>& ctors
) const
6795 CVC5_API_TRY_CATCH_BEGIN
;
6796 CVC5_API_ARG_CHECK_EXPECTED(ctors
.size() > 0, ctors
)
6797 << "a datatype declaration with at least one constructor";
6798 CVC5_API_SOLVER_CHECK_DTCTORDECLS(ctors
);
6799 for (size_t i
= 0, size
= ctors
.size(); i
< size
; i
++)
6801 CVC5_API_CHECK(!ctors
[i
].isResolved())
6802 << "cannot use a constructor for multiple datatypes";
6804 //////// all checks before this line
6805 DatatypeDecl
dtdecl(this, symbol
);
6806 for (size_t i
= 0, size
= ctors
.size(); i
< size
; i
++)
6808 dtdecl
.addConstructor(ctors
[i
]);
6810 return Sort(this, getNodeManager()->mkDatatypeType(*dtdecl
.d_dtype
));
6812 CVC5_API_TRY_CATCH_END
;
6815 Term
Solver::declareFun(const std::string
& symbol
,
6816 const std::vector
<Sort
>& sorts
,
6817 const Sort
& sort
) const
6819 CVC5_API_TRY_CATCH_BEGIN
;
6820 CVC5_API_SOLVER_CHECK_DOMAIN_SORTS(sorts
);
6821 CVC5_API_SOLVER_CHECK_CODOMAIN_SORT(sort
);
6822 //////// all checks before this line
6824 TypeNode type
= *sort
.d_type
;
6827 std::vector
<TypeNode
> types
= Sort::sortVectorToTypeNodes(sorts
);
6828 type
= getNodeManager()->mkFunctionType(types
, type
);
6830 return Term(this, d_nodeMgr
->mkVar(symbol
, type
));
6832 CVC5_API_TRY_CATCH_END
;
6835 Sort
Solver::declareSort(const std::string
& symbol
, uint32_t arity
) const
6837 CVC5_API_TRY_CATCH_BEGIN
;
6838 //////// all checks before this line
6841 return Sort(this, getNodeManager()->mkSort(symbol
));
6843 return Sort(this, getNodeManager()->mkSortConstructor(symbol
, arity
));
6845 CVC5_API_TRY_CATCH_END
;
6848 Term
Solver::defineFun(const std::string
& symbol
,
6849 const std::vector
<Term
>& bound_vars
,
6854 CVC5_API_TRY_CATCH_BEGIN
;
6855 CVC5_API_SOLVER_CHECK_CODOMAIN_SORT(sort
);
6856 CVC5_API_SOLVER_CHECK_TERM(term
);
6857 CVC5_API_CHECK(term
.getSort().isSubsortOf(sort
))
6858 << "Invalid sort of function body '" << term
<< "', expected '" << sort
6861 std::vector
<Sort
> domain_sorts
;
6862 for (const auto& bv
: bound_vars
)
6864 domain_sorts
.push_back(bv
.getSort());
6867 domain_sorts
.empty()
6870 getNodeManager()->mkFunctionType(
6871 Sort::sortVectorToTypeNodes(domain_sorts
), *sort
.d_type
));
6872 Term fun
= mkConst(fun_sort
, symbol
);
6874 CVC5_API_SOLVER_CHECK_BOUND_VARS_DEF_FUN(fun
, bound_vars
, domain_sorts
);
6875 //////// all checks before this line
6877 d_slv
->defineFunction(
6878 *fun
.d_node
, Term::termVectorToNodes(bound_vars
), *term
.d_node
, global
);
6881 CVC5_API_TRY_CATCH_END
;
6884 Term
Solver::defineFunRec(const std::string
& symbol
,
6885 const std::vector
<Term
>& bound_vars
,
6890 CVC5_API_TRY_CATCH_BEGIN
;
6892 CVC5_API_CHECK(d_slv
->getUserLogicInfo().isQuantified())
6893 << "recursive function definitions require a logic with quantifiers";
6894 CVC5_API_CHECK(d_slv
->getUserLogicInfo().isTheoryEnabled(theory::THEORY_UF
))
6895 << "recursive function definitions require a logic with uninterpreted "
6898 CVC5_API_SOLVER_CHECK_TERM(term
);
6899 CVC5_API_SOLVER_CHECK_CODOMAIN_SORT(sort
);
6900 CVC5_API_CHECK(sort
== term
.getSort())
6901 << "Invalid sort of function body '" << term
<< "', expected '" << sort
6904 std::vector
<Sort
> domain_sorts
;
6905 for (const auto& bv
: bound_vars
)
6907 domain_sorts
.push_back(bv
.getSort());
6910 domain_sorts
.empty()
6913 getNodeManager()->mkFunctionType(
6914 Sort::sortVectorToTypeNodes(domain_sorts
), *sort
.d_type
));
6915 Term fun
= mkConst(fun_sort
, symbol
);
6917 CVC5_API_SOLVER_CHECK_BOUND_VARS_DEF_FUN(fun
, bound_vars
, domain_sorts
);
6918 //////// all checks before this line
6920 d_slv
->defineFunctionRec(
6921 *fun
.d_node
, Term::termVectorToNodes(bound_vars
), *term
.d_node
, global
);
6925 CVC5_API_TRY_CATCH_END
;
6928 Term
Solver::defineFunRec(const Term
& fun
,
6929 const std::vector
<Term
>& bound_vars
,
6933 CVC5_API_TRY_CATCH_BEGIN
;
6935 CVC5_API_CHECK(d_slv
->getUserLogicInfo().isQuantified())
6936 << "recursive function definitions require a logic with quantifiers";
6937 CVC5_API_CHECK(d_slv
->getUserLogicInfo().isTheoryEnabled(theory::THEORY_UF
))
6938 << "recursive function definitions require a logic with uninterpreted "
6941 CVC5_API_SOLVER_CHECK_TERM(fun
);
6942 CVC5_API_SOLVER_CHECK_TERM(term
);
6943 if (fun
.getSort().isFunction())
6945 std::vector
<Sort
> domain_sorts
= fun
.getSort().getFunctionDomainSorts();
6946 CVC5_API_SOLVER_CHECK_BOUND_VARS_DEF_FUN(fun
, bound_vars
, domain_sorts
);
6947 Sort codomain
= fun
.getSort().getFunctionCodomainSort();
6948 CVC5_API_CHECK(codomain
== term
.getSort())
6949 << "Invalid sort of function body '" << term
<< "', expected '"
6954 CVC5_API_SOLVER_CHECK_BOUND_VARS(bound_vars
);
6955 CVC5_API_ARG_CHECK_EXPECTED(bound_vars
.size() == 0, fun
)
6956 << "function or nullary symbol";
6958 //////// all checks before this line
6960 std::vector
<Node
> ebound_vars
= Term::termVectorToNodes(bound_vars
);
6961 d_slv
->defineFunctionRec(*fun
.d_node
, ebound_vars
, *term
.d_node
, global
);
6964 CVC5_API_TRY_CATCH_END
;
6967 void Solver::defineFunsRec(const std::vector
<Term
>& funs
,
6968 const std::vector
<std::vector
<Term
>>& bound_vars
,
6969 const std::vector
<Term
>& terms
,
6972 CVC5_API_TRY_CATCH_BEGIN
;
6974 CVC5_API_CHECK(d_slv
->getUserLogicInfo().isQuantified())
6975 << "recursive function definitions require a logic with quantifiers";
6976 CVC5_API_CHECK(d_slv
->getUserLogicInfo().isTheoryEnabled(theory::THEORY_UF
))
6977 << "recursive function definitions require a logic with uninterpreted "
6979 CVC5_API_SOLVER_CHECK_TERMS(funs
);
6980 CVC5_API_SOLVER_CHECK_TERMS(terms
);
6982 size_t funs_size
= funs
.size();
6983 CVC5_API_ARG_SIZE_CHECK_EXPECTED(funs_size
== bound_vars
.size(), bound_vars
)
6984 << "'" << funs_size
<< "'";
6985 CVC5_API_ARG_SIZE_CHECK_EXPECTED(funs_size
== terms
.size(), terms
)
6986 << "'" << funs_size
<< "'";
6988 for (size_t j
= 0; j
< funs_size
; ++j
)
6990 const Term
& fun
= funs
[j
];
6991 const std::vector
<Term
>& bvars
= bound_vars
[j
];
6992 const Term
& term
= terms
[j
];
6994 CVC5_API_ARG_AT_INDEX_CHECK_EXPECTED(
6995 this == fun
.d_solver
, "function", funs
, j
)
6996 << "function associated with this solver object";
6997 CVC5_API_ARG_AT_INDEX_CHECK_EXPECTED(
6998 this == term
.d_solver
, "term", terms
, j
)
6999 << "term associated with this solver object";
7001 if (fun
.getSort().isFunction())
7003 std::vector
<Sort
> domain_sorts
= fun
.getSort().getFunctionDomainSorts();
7004 CVC5_API_SOLVER_CHECK_BOUND_VARS_DEF_FUN(fun
, bvars
, domain_sorts
);
7005 Sort codomain
= fun
.getSort().getFunctionCodomainSort();
7006 CVC5_API_ARG_AT_INDEX_CHECK_EXPECTED(
7007 codomain
== term
.getSort(), "sort of function body", terms
, j
)
7008 << "'" << codomain
<< "'";
7012 CVC5_API_SOLVER_CHECK_BOUND_VARS(bvars
);
7013 CVC5_API_ARG_CHECK_EXPECTED(bvars
.size() == 0, fun
)
7014 << "function or nullary symbol";
7017 //////// all checks before this line
7018 std::vector
<Node
> efuns
= Term::termVectorToNodes(funs
);
7019 std::vector
<std::vector
<Node
>> ebound_vars
;
7020 for (const auto& v
: bound_vars
)
7022 ebound_vars
.push_back(Term::termVectorToNodes(v
));
7024 std::vector
<Node
> nodes
= Term::termVectorToNodes(terms
);
7025 d_slv
->defineFunctionsRec(efuns
, ebound_vars
, nodes
, global
);
7027 CVC5_API_TRY_CATCH_END
;
7030 void Solver::echo(std::ostream
& out
, const std::string
& str
) const
7035 std::vector
<Term
> Solver::getAssertions(void) const
7037 CVC5_API_TRY_CATCH_BEGIN
;
7038 //////// all checks before this line
7039 std::vector
<Node
> assertions
= d_slv
->getAssertions();
7041 * return std::vector<Term>(assertions.begin(), assertions.end());
7042 * here since constructor is private */
7043 std::vector
<Term
> res
;
7044 for (const Node
& e
: assertions
)
7046 res
.push_back(Term(this, e
));
7050 CVC5_API_TRY_CATCH_END
;
7053 std::string
Solver::getInfo(const std::string
& flag
) const
7055 CVC5_API_TRY_CATCH_BEGIN
;
7056 CVC5_API_UNSUPPORTED_CHECK(d_slv
->isValidGetInfoFlag(flag
))
7057 << "Unrecognized flag: " << flag
<< ".";
7058 //////// all checks before this line
7059 return d_slv
->getInfo(flag
);
7061 CVC5_API_TRY_CATCH_END
;
7064 std::string
Solver::getOption(const std::string
& option
) const
7068 return d_slv
->getOption(option
);
7070 catch (OptionException
& e
)
7072 throw CVC5ApiUnsupportedException(e
.getMessage());
7076 // Supports a visitor from a list of lambdas
7077 // Taken from https://en.cppreference.com/w/cpp/utility/variant/visit
7078 template<class... Ts
> struct overloaded
: Ts
... { using Ts::operator()...; };
7079 template<class... Ts
> overloaded(Ts
...) -> overloaded
<Ts
...>;
7081 bool OptionInfo::boolValue() const
7083 CVC5_API_TRY_CATCH_BEGIN
;
7084 CVC5_API_RECOVERABLE_CHECK(std::holds_alternative
<ValueInfo
<bool>>(valueInfo
))
7085 << name
<< " is not a bool option";
7086 //////// all checks before this line
7087 return std::get
<ValueInfo
<bool>>(valueInfo
).currentValue
;
7089 CVC5_API_TRY_CATCH_END
;
7091 std::string
OptionInfo::stringValue() const
7093 CVC5_API_TRY_CATCH_BEGIN
;
7094 CVC5_API_RECOVERABLE_CHECK(
7095 std::holds_alternative
<ValueInfo
<std::string
>>(valueInfo
))
7096 << name
<< " is not a string option";
7097 //////// all checks before this line
7098 return std::get
<ValueInfo
<std::string
>>(valueInfo
).currentValue
;
7100 CVC5_API_TRY_CATCH_END
;
7102 int64_t OptionInfo::intValue() const
7104 CVC5_API_TRY_CATCH_BEGIN
;
7105 CVC5_API_RECOVERABLE_CHECK(
7106 std::holds_alternative
<NumberInfo
<int64_t>>(valueInfo
))
7107 << name
<< " is not an int option";
7108 //////// all checks before this line
7109 return std::get
<NumberInfo
<int64_t>>(valueInfo
).currentValue
;
7111 CVC5_API_TRY_CATCH_END
;
7113 uint64_t OptionInfo::uintValue() const
7115 CVC5_API_TRY_CATCH_BEGIN
;
7116 CVC5_API_RECOVERABLE_CHECK(
7117 std::holds_alternative
<NumberInfo
<uint64_t>>(valueInfo
))
7118 << name
<< " is not a uint option";
7119 //////// all checks before this line
7120 return std::get
<NumberInfo
<uint64_t>>(valueInfo
).currentValue
;
7122 CVC5_API_TRY_CATCH_END
;
7124 double OptionInfo::doubleValue() const
7126 CVC5_API_TRY_CATCH_BEGIN
;
7127 CVC5_API_RECOVERABLE_CHECK(
7128 std::holds_alternative
<NumberInfo
<double>>(valueInfo
))
7129 << name
<< " is not a double option";
7130 //////// all checks before this line
7131 return std::get
<NumberInfo
<double>>(valueInfo
).currentValue
;
7133 CVC5_API_TRY_CATCH_END
;
7136 std::ostream
& operator<<(std::ostream
& os
, const OptionInfo
& oi
)
7138 os
<< "OptionInfo{ " << oi
.name
;
7141 os
<< " | set by user";
7143 if (!oi
.aliases
.empty())
7145 container_to_stream(os
, oi
.aliases
, ", ", "", ", ");
7147 auto printNum
= [&os
](const std::string
& type
, const auto& vi
) {
7148 os
<< " | " << type
<< " | " << vi
.currentValue
<< " | default "
7150 if (vi
.minimum
|| vi
.maximum
)
7155 os
<< " " << *vi
.minimum
<< " <=";
7160 os
<< " <= " << *vi
.maximum
;
7164 std::visit(overloaded
{
7165 [&os
](const OptionInfo::VoidInfo
& vi
) { os
<< " | void"; },
7166 [&os
](const OptionInfo::ValueInfo
<bool>& vi
) {
7167 os
<< " | bool | " << vi
.currentValue
<< " | default "
7170 [&os
](const OptionInfo::ValueInfo
<std::string
>& vi
) {
7171 os
<< " | string | " << vi
.currentValue
<< " | default "
7174 [&printNum
](const OptionInfo::NumberInfo
<int64_t>& vi
) {
7175 printNum("int64_t", vi
);
7177 [&printNum
](const OptionInfo::NumberInfo
<uint64_t>& vi
) {
7178 printNum("uint64_t", vi
);
7180 [&printNum
](const OptionInfo::NumberInfo
<double>& vi
) {
7181 printNum("double", vi
);
7183 [&os
](const OptionInfo::ModeInfo
& vi
) {
7184 os
<< " | mode | " << vi
.currentValue
<< " | default "
7185 << vi
.defaultValue
<< " | modes: ";
7186 container_to_stream(os
, vi
.modes
, "", "", ", ");
7194 std::vector
<std::string
> Solver::getOptionNames() const
7196 CVC5_API_TRY_CATCH_BEGIN
;
7197 //////// all checks before this line
7198 return options::getNames();
7200 CVC5_API_TRY_CATCH_END
;
7203 OptionInfo
Solver::getOptionInfo(const std::string
& option
) const
7205 CVC5_API_TRY_CATCH_BEGIN
;
7206 //////// all checks before this line
7207 auto info
= options::getInfo(d_slv
->getOptions(), option
);
7208 CVC5_API_CHECK(info
.name
!= "")
7209 << "Querying invalid or unknown option " << option
;
7212 [&info
](const options::OptionInfo::VoidInfo
& vi
) {
7213 return OptionInfo
{info
.name
,
7216 OptionInfo::VoidInfo
{}};
7218 [&info
](const options::OptionInfo::ValueInfo
<bool>& vi
) {
7223 OptionInfo::ValueInfo
<bool>{vi
.defaultValue
, vi
.currentValue
}};
7225 [&info
](const options::OptionInfo::ValueInfo
<std::string
>& vi
) {
7226 return OptionInfo
{info
.name
,
7229 OptionInfo::ValueInfo
<std::string
>{
7230 vi
.defaultValue
, vi
.currentValue
}};
7232 [&info
](const options::OptionInfo::NumberInfo
<int64_t>& vi
) {
7237 OptionInfo::NumberInfo
<int64_t>{
7238 vi
.defaultValue
, vi
.currentValue
, vi
.minimum
, vi
.maximum
}};
7240 [&info
](const options::OptionInfo::NumberInfo
<uint64_t>& vi
) {
7245 OptionInfo::NumberInfo
<uint64_t>{
7246 vi
.defaultValue
, vi
.currentValue
, vi
.minimum
, vi
.maximum
}};
7248 [&info
](const options::OptionInfo::NumberInfo
<double>& vi
) {
7253 OptionInfo::NumberInfo
<double>{
7254 vi
.defaultValue
, vi
.currentValue
, vi
.minimum
, vi
.maximum
}};
7256 [&info
](const options::OptionInfo::ModeInfo
& vi
) {
7257 return OptionInfo
{info
.name
,
7260 OptionInfo::ModeInfo
{
7261 vi
.defaultValue
, vi
.currentValue
, vi
.modes
}};
7266 CVC5_API_TRY_CATCH_END
;
7269 DriverOptions
Solver::getDriverOptions() const { return DriverOptions(*this); }
7271 std::vector
<Term
> Solver::getUnsatAssumptions(void) const
7273 CVC5_API_TRY_CATCH_BEGIN
;
7274 CVC5_API_CHECK(d_slv
->getOptions().base
.incrementalSolving
)
7275 << "Cannot get unsat assumptions unless incremental solving is enabled "
7276 "(try --incremental)";
7277 CVC5_API_CHECK(d_slv
->getOptions().smt
.unsatAssumptions
)
7278 << "Cannot get unsat assumptions unless explicitly enabled "
7279 "(try --produce-unsat-assumptions)";
7280 CVC5_API_CHECK(d_slv
->getSmtMode() == SmtMode::UNSAT
)
7281 << "Cannot get unsat assumptions unless in unsat mode.";
7282 //////// all checks before this line
7284 std::vector
<Node
> uassumptions
= d_slv
->getUnsatAssumptions();
7286 * return std::vector<Term>(uassumptions.begin(), uassumptions.end());
7287 * here since constructor is private */
7288 std::vector
<Term
> res
;
7289 for (const Node
& n
: uassumptions
)
7291 res
.push_back(Term(this, n
));
7295 CVC5_API_TRY_CATCH_END
;
7298 std::vector
<Term
> Solver::getUnsatCore(void) const
7300 CVC5_API_TRY_CATCH_BEGIN
;
7301 CVC5_API_CHECK(d_slv
->getOptions().smt
.unsatCores
)
7302 << "Cannot get unsat core unless explicitly enabled "
7303 "(try --produce-unsat-cores)";
7304 CVC5_API_RECOVERABLE_CHECK(d_slv
->getSmtMode() == SmtMode::UNSAT
)
7305 << "Cannot get unsat core unless in unsat mode.";
7306 //////// all checks before this line
7307 UnsatCore core
= d_slv
->getUnsatCore();
7309 * return std::vector<Term>(core.begin(), core.end());
7310 * here since constructor is private */
7311 std::vector
<Term
> res
;
7312 for (const Node
& e
: core
)
7314 res
.push_back(Term(this, e
));
7318 CVC5_API_TRY_CATCH_END
;
7321 std::map
<Term
, Term
> Solver::getDifficulty() const
7323 CVC5_API_TRY_CATCH_BEGIN
;
7324 CVC5_API_RECOVERABLE_CHECK(d_slv
->getSmtMode() == SmtMode::UNSAT
7325 || d_slv
->getSmtMode() == SmtMode::SAT
7326 || d_slv
->getSmtMode() == SmtMode::SAT_UNKNOWN
)
7327 << "Cannot get difficulty unless after a UNSAT, SAT or UNKNOWN response.";
7328 //////// all checks before this line
7329 std::map
<Term
, Term
> res
;
7330 std::map
<Node
, Node
> dmap
;
7331 d_slv
->getDifficultyMap(dmap
);
7332 for (const std::pair
<const Node
, Node
>& d
: dmap
)
7334 res
[Term(this, d
.first
)] = Term(this, d
.second
);
7338 CVC5_API_TRY_CATCH_END
;
7341 std::string
Solver::getProof(void) const
7343 CVC5_API_TRY_CATCH_BEGIN
;
7344 CVC5_API_CHECK(d_slv
->getOptions().smt
.produceProofs
)
7345 << "Cannot get proof unless proofs are enabled (try --produce-proofs)";
7346 CVC5_API_RECOVERABLE_CHECK(d_slv
->getSmtMode() == SmtMode::UNSAT
)
7347 << "Cannot get proof unless in unsat mode.";
7348 return d_slv
->getProof();
7349 CVC5_API_TRY_CATCH_END
;
7352 Term
Solver::getValue(const Term
& term
) const
7354 CVC5_API_TRY_CATCH_BEGIN
;
7355 CVC5_API_RECOVERABLE_CHECK(d_slv
->getOptions().smt
.produceModels
)
7356 << "Cannot get value unless model generation is enabled "
7357 "(try --produce-models)";
7358 CVC5_API_RECOVERABLE_CHECK(d_slv
->isSmtModeSat())
7359 << "Cannot get value unless after a SAT or UNKNOWN response.";
7360 CVC5_API_SOLVER_CHECK_TERM(term
);
7361 CVC5_API_RECOVERABLE_CHECK(term
.getSort().isFirstClass())
7362 << "Cannot get value of a term that is not first class.";
7363 CVC5_API_RECOVERABLE_CHECK(!term
.getSort().isDatatype()
7364 || term
.getSort().getDatatype().isWellFounded())
7365 << "Cannot get value of a term of non-well-founded datatype sort.";
7366 //////// all checks before this line
7367 return getValueHelper(term
);
7369 CVC5_API_TRY_CATCH_END
;
7372 std::vector
<Term
> Solver::getValue(const std::vector
<Term
>& terms
) const
7374 CVC5_API_TRY_CATCH_BEGIN
;
7375 CVC5_API_RECOVERABLE_CHECK(d_slv
->getOptions().smt
.produceModels
)
7376 << "Cannot get value unless model generation is enabled "
7377 "(try --produce-models)";
7378 CVC5_API_RECOVERABLE_CHECK(d_slv
->isSmtModeSat())
7379 << "Cannot get value unless after a SAT or UNKNOWN response.";
7380 for (const Term
& t
: terms
)
7382 CVC5_API_RECOVERABLE_CHECK(t
.getSort().isFirstClass())
7383 << "Cannot get value of a term that is not first class.";
7384 CVC5_API_RECOVERABLE_CHECK(!t
.getSort().isDatatype()
7385 || t
.getSort().getDatatype().isWellFounded())
7386 << "Cannot get value of a term of non-well-founded datatype sort.";
7388 CVC5_API_SOLVER_CHECK_TERMS(terms
);
7389 //////// all checks before this line
7391 std::vector
<Term
> res
;
7392 for (size_t i
= 0, n
= terms
.size(); i
< n
; ++i
)
7394 /* Can not use emplace_back here since constructor is private. */
7395 res
.push_back(getValueHelper(terms
[i
]));
7399 CVC5_API_TRY_CATCH_END
;
7402 std::vector
<Term
> Solver::getModelDomainElements(const Sort
& s
) const
7404 CVC5_API_TRY_CATCH_BEGIN
;
7405 CVC5_API_RECOVERABLE_CHECK(d_slv
->getOptions().smt
.produceModels
)
7406 << "Cannot get domain elements unless model generation is enabled "
7407 "(try --produce-models)";
7408 CVC5_API_RECOVERABLE_CHECK(d_slv
->isSmtModeSat())
7409 << "Cannot get domain elements unless after a SAT or UNKNOWN response.";
7410 CVC5_API_SOLVER_CHECK_SORT(s
);
7411 CVC5_API_RECOVERABLE_CHECK(s
.isUninterpretedSort())
7412 << "Expecting an uninterpreted sort as argument to "
7413 "getModelDomainElements.";
7414 //////// all checks before this line
7415 std::vector
<Term
> res
;
7416 std::vector
<Node
> elements
= d_slv
->getModelDomainElements(s
.getTypeNode());
7417 for (const Node
& n
: elements
)
7419 res
.push_back(Term(this, n
));
7423 CVC5_API_TRY_CATCH_END
;
7426 bool Solver::isModelCoreSymbol(const Term
& v
) const
7428 CVC5_API_TRY_CATCH_BEGIN
;
7429 CVC5_API_RECOVERABLE_CHECK(d_slv
->getOptions().smt
.produceModels
)
7430 << "Cannot check if model core symbol unless model generation is enabled "
7431 "(try --produce-models)";
7432 CVC5_API_RECOVERABLE_CHECK(d_slv
->isSmtModeSat())
7433 << "Cannot check if model core symbol unless after a SAT or UNKNOWN "
7435 CVC5_API_SOLVER_CHECK_TERM(v
);
7436 CVC5_API_RECOVERABLE_CHECK(v
.getKind() == CONSTANT
)
7437 << "Expecting a free constant as argument to isModelCoreSymbol.";
7438 //////// all checks before this line
7439 return d_slv
->isModelCoreSymbol(v
.getNode());
7441 CVC5_API_TRY_CATCH_END
;
7444 std::string
Solver::getModel(const std::vector
<Sort
>& sorts
,
7445 const std::vector
<Term
>& vars
) const
7447 CVC5_API_TRY_CATCH_BEGIN
;
7448 CVC5_API_RECOVERABLE_CHECK(d_slv
->getOptions().smt
.produceModels
)
7449 << "Cannot get model unless model generation is enabled "
7450 "(try --produce-models)";
7451 CVC5_API_RECOVERABLE_CHECK(d_slv
->isSmtModeSat())
7452 << "Cannot get model unless after a SAT or UNKNOWN response.";
7453 CVC5_API_SOLVER_CHECK_SORTS(sorts
);
7454 for (const Sort
& s
: sorts
)
7456 CVC5_API_RECOVERABLE_CHECK(s
.isUninterpretedSort())
7457 << "Expecting an uninterpreted sort as argument to "
7460 CVC5_API_SOLVER_CHECK_TERMS(vars
);
7461 for (const Term
& v
: vars
)
7463 CVC5_API_RECOVERABLE_CHECK(v
.getKind() == CONSTANT
)
7464 << "Expecting a free constant as argument to getModel.";
7466 //////// all checks before this line
7467 return d_slv
->getModel(Sort::sortVectorToTypeNodes(sorts
),
7468 Term::termVectorToNodes(vars
));
7470 CVC5_API_TRY_CATCH_END
;
7473 Term
Solver::getQuantifierElimination(const Term
& q
) const
7475 CVC5_API_TRY_CATCH_BEGIN
;
7476 CVC5_API_SOLVER_CHECK_TERM(q
);
7477 //////// all checks before this line
7478 return Term(this, d_slv
->getQuantifierElimination(q
.getNode(), true, true));
7480 CVC5_API_TRY_CATCH_END
;
7483 Term
Solver::getQuantifierEliminationDisjunct(const Term
& q
) const
7485 CVC5_API_TRY_CATCH_BEGIN
;
7486 CVC5_API_SOLVER_CHECK_TERM(q
);
7487 //////// all checks before this line
7488 return Term(this, d_slv
->getQuantifierElimination(q
.getNode(), false, true));
7490 CVC5_API_TRY_CATCH_END
;
7493 void Solver::declareSepHeap(const Sort
& locSort
, const Sort
& dataSort
) const
7495 CVC5_API_TRY_CATCH_BEGIN
;
7496 CVC5_API_SOLVER_CHECK_SORT(locSort
);
7497 CVC5_API_SOLVER_CHECK_SORT(dataSort
);
7498 CVC5_API_CHECK(d_slv
->getLogicInfo().isTheoryEnabled(theory::THEORY_SEP
))
7499 << "Cannot obtain separation logic expressions if not using the "
7500 "separation logic theory.";
7501 //////// all checks before this line
7502 d_slv
->declareSepHeap(locSort
.getTypeNode(), dataSort
.getTypeNode());
7504 CVC5_API_TRY_CATCH_END
;
7507 Term
Solver::getValueSepHeap() const
7509 CVC5_API_TRY_CATCH_BEGIN
;
7510 CVC5_API_CHECK(d_slv
->getLogicInfo().isTheoryEnabled(theory::THEORY_SEP
))
7511 << "Cannot obtain separation logic expressions if not using the "
7512 "separation logic theory.";
7513 CVC5_API_CHECK(d_slv
->getOptions().smt
.produceModels
)
7514 << "Cannot get separation heap term unless model generation is enabled "
7515 "(try --produce-models)";
7516 CVC5_API_RECOVERABLE_CHECK(d_slv
->isSmtModeSat())
7517 << "Can only get separtion heap term after SAT or UNKNOWN response.";
7518 //////// all checks before this line
7519 return Term(this, d_slv
->getSepHeapExpr());
7521 CVC5_API_TRY_CATCH_END
;
7524 Term
Solver::getValueSepNil() const
7526 CVC5_API_TRY_CATCH_BEGIN
;
7527 CVC5_API_CHECK(d_slv
->getLogicInfo().isTheoryEnabled(theory::THEORY_SEP
))
7528 << "Cannot obtain separation logic expressions if not using the "
7529 "separation logic theory.";
7530 CVC5_API_CHECK(d_slv
->getOptions().smt
.produceModels
)
7531 << "Cannot get separation nil term unless model generation is enabled "
7532 "(try --produce-models)";
7533 CVC5_API_RECOVERABLE_CHECK(d_slv
->isSmtModeSat())
7534 << "Can only get separtion nil term after SAT or UNKNOWN response.";
7535 //////// all checks before this line
7536 return Term(this, d_slv
->getSepNilExpr());
7538 CVC5_API_TRY_CATCH_END
;
7541 Term
Solver::declarePool(const std::string
& symbol
,
7543 const std::vector
<Term
>& initValue
) const
7545 CVC5_API_TRY_CATCH_BEGIN
;
7546 CVC5_API_SOLVER_CHECK_SORT(sort
);
7547 CVC5_API_SOLVER_CHECK_TERMS(initValue
);
7548 //////// all checks before this line
7549 TypeNode setType
= getNodeManager()->mkSetType(*sort
.d_type
);
7550 Node pool
= getNodeManager()->mkBoundVar(symbol
, setType
);
7551 std::vector
<Node
> initv
= Term::termVectorToNodes(initValue
);
7552 d_slv
->declarePool(pool
, initv
);
7553 return Term(this, pool
);
7555 CVC5_API_TRY_CATCH_END
;
7558 void Solver::pop(uint32_t nscopes
) const
7560 CVC5_API_TRY_CATCH_BEGIN
;
7561 CVC5_API_CHECK(d_slv
->getOptions().base
.incrementalSolving
)
7562 << "Cannot pop when not solving incrementally (use --incremental)";
7563 CVC5_API_CHECK(nscopes
<= d_slv
->getNumUserLevels())
7564 << "Cannot pop beyond first pushed context";
7565 //////// all checks before this line
7566 for (uint32_t n
= 0; n
< nscopes
; ++n
)
7571 CVC5_API_TRY_CATCH_END
;
7574 bool Solver::getInterpolant(const Term
& conj
, Term
& output
) const
7576 CVC5_API_TRY_CATCH_BEGIN
;
7577 CVC5_API_SOLVER_CHECK_TERM(conj
);
7578 CVC5_API_CHECK(d_slv
->getOptions().smt
.produceInterpols
7579 != options::ProduceInterpols::NONE
)
7580 << "Cannot get interpolant unless interpolants are enabled (try "
7581 "--produce-interpols=mode)";
7582 //////// all checks before this line
7585 bool success
= d_slv
->getInterpolant(*conj
.d_node
, nullType
, result
);
7588 output
= Term(this, result
);
7592 CVC5_API_TRY_CATCH_END
;
7595 bool Solver::getInterpolant(const Term
& conj
,
7599 CVC5_API_TRY_CATCH_BEGIN
;
7600 CVC5_API_SOLVER_CHECK_TERM(conj
);
7601 CVC5_API_CHECK(d_slv
->getOptions().smt
.produceInterpols
7602 != options::ProduceInterpols::NONE
)
7603 << "Cannot get interpolant unless interpolants are enabled (try "
7604 "--produce-interpols=mode)";
7605 //////// all checks before this line
7608 d_slv
->getInterpolant(*conj
.d_node
, *grammar
.resolve().d_type
, result
);
7611 output
= Term(this, result
);
7615 CVC5_API_TRY_CATCH_END
;
7618 bool Solver::getInterpolantNext(Term
& output
) const
7620 CVC5_API_TRY_CATCH_BEGIN
;
7621 CVC5_API_CHECK(d_slv
->getOptions().smt
.produceInterpols
7622 != options::ProduceInterpols::NONE
)
7623 << "Cannot get interpolant unless interpolants are enabled (try "
7624 "--produce-interpols=mode)";
7625 CVC5_API_CHECK(d_slv
->getOptions().base
.incrementalSolving
)
7626 << "Cannot get next interpolant when not solving incrementally (try "
7628 //////// all checks before this line
7630 bool success
= d_slv
->getInterpolantNext(result
);
7633 output
= Term(this, result
);
7637 CVC5_API_TRY_CATCH_END
;
7640 bool Solver::getAbduct(const Term
& conj
, Term
& output
) const
7642 CVC5_API_TRY_CATCH_BEGIN
;
7643 CVC5_API_SOLVER_CHECK_TERM(conj
);
7644 CVC5_API_CHECK(d_slv
->getOptions().smt
.produceAbducts
)
7645 << "Cannot get abduct unless abducts are enabled (try --produce-abducts)";
7646 //////// all checks before this line
7649 bool success
= d_slv
->getAbduct(*conj
.d_node
, nullType
, result
);
7652 output
= Term(this, result
);
7656 CVC5_API_TRY_CATCH_END
;
7659 bool Solver::getAbduct(const Term
& conj
, Grammar
& grammar
, Term
& output
) const
7661 CVC5_API_TRY_CATCH_BEGIN
;
7662 CVC5_API_SOLVER_CHECK_TERM(conj
);
7663 CVC5_API_CHECK(d_slv
->getOptions().smt
.produceAbducts
)
7664 << "Cannot get abduct unless abducts are enabled (try --produce-abducts)";
7665 //////// all checks before this line
7668 d_slv
->getAbduct(*conj
.d_node
, *grammar
.resolve().d_type
, result
);
7671 output
= Term(this, result
);
7675 CVC5_API_TRY_CATCH_END
;
7678 bool Solver::getAbductNext(Term
& output
) const
7680 CVC5_API_TRY_CATCH_BEGIN
;
7681 CVC5_API_CHECK(d_slv
->getOptions().smt
.produceAbducts
)
7682 << "Cannot get next abduct unless abducts are enabled (try "
7683 "--produce-abducts)";
7684 CVC5_API_CHECK(d_slv
->getOptions().base
.incrementalSolving
)
7685 << "Cannot get next abduct when not solving incrementally (try "
7687 //////// all checks before this line
7689 bool success
= d_slv
->getAbductNext(result
);
7692 output
= Term(this, result
);
7696 CVC5_API_TRY_CATCH_END
;
7699 void Solver::blockModel() const
7701 CVC5_API_TRY_CATCH_BEGIN
;
7702 CVC5_API_CHECK(d_slv
->getOptions().smt
.produceModels
)
7703 << "Cannot get value unless model generation is enabled "
7704 "(try --produce-models)";
7705 CVC5_API_RECOVERABLE_CHECK(d_slv
->isSmtModeSat())
7706 << "Can only block model after SAT or UNKNOWN response.";
7707 //////// all checks before this line
7708 d_slv
->blockModel();
7710 CVC5_API_TRY_CATCH_END
;
7713 void Solver::blockModelValues(const std::vector
<Term
>& terms
) const
7715 CVC5_API_TRY_CATCH_BEGIN
;
7716 CVC5_API_CHECK(d_slv
->getOptions().smt
.produceModels
)
7717 << "Cannot get value unless model generation is enabled "
7718 "(try --produce-models)";
7719 CVC5_API_RECOVERABLE_CHECK(d_slv
->isSmtModeSat())
7720 << "Can only block model values after SAT or UNKNOWN response.";
7721 CVC5_API_ARG_SIZE_CHECK_EXPECTED(!terms
.empty(), terms
)
7722 << "a non-empty set of terms";
7723 CVC5_API_SOLVER_CHECK_TERMS(terms
);
7724 //////// all checks before this line
7725 d_slv
->blockModelValues(Term::termVectorToNodes(terms
));
7727 CVC5_API_TRY_CATCH_END
;
7730 void Solver::printInstantiations(std::ostream
& out
) const
7732 CVC5_API_TRY_CATCH_BEGIN
;
7733 //////// all checks before this line
7734 d_slv
->printInstantiations(out
);
7736 CVC5_API_TRY_CATCH_END
;
7739 void Solver::push(uint32_t nscopes
) const
7741 CVC5_API_TRY_CATCH_BEGIN
;
7742 CVC5_API_CHECK(d_slv
->getOptions().base
.incrementalSolving
)
7743 << "Cannot push when not solving incrementally (use --incremental)";
7744 //////// all checks before this line
7745 for (uint32_t n
= 0; n
< nscopes
; ++n
)
7750 CVC5_API_TRY_CATCH_END
;
7753 void Solver::resetAssertions(void) const
7755 CVC5_API_TRY_CATCH_BEGIN
;
7756 //////// all checks before this line
7757 d_slv
->resetAssertions();
7759 CVC5_API_TRY_CATCH_END
;
7762 void Solver::setInfo(const std::string
& keyword
, const std::string
& value
) const
7764 CVC5_API_TRY_CATCH_BEGIN
;
7765 CVC5_API_UNSUPPORTED_CHECK(
7766 keyword
== "source" || keyword
== "category" || keyword
== "difficulty"
7767 || keyword
== "filename" || keyword
== "license" || keyword
== "name"
7768 || keyword
== "notes" || keyword
== "smt-lib-version"
7769 || keyword
== "status")
7770 << "Unrecognized keyword: " << keyword
7771 << ", expected 'source', 'category', 'difficulty', "
7772 "'filename', 'license', 'name', "
7773 "'notes', 'smt-lib-version' or 'status'";
7774 CVC5_API_RECOVERABLE_ARG_CHECK_EXPECTED(
7775 keyword
!= "smt-lib-version" || value
== "2" || value
== "2.0"
7776 || value
== "2.5" || value
== "2.6",
7778 << "'2.0', '2.5', '2.6'";
7779 CVC5_API_ARG_CHECK_EXPECTED(keyword
!= "status" || value
== "sat"
7780 || value
== "unsat" || value
== "unknown",
7782 << "'sat', 'unsat' or 'unknown'";
7783 //////// all checks before this line
7784 d_slv
->setInfo(keyword
, value
);
7786 CVC5_API_TRY_CATCH_END
;
7789 void Solver::setLogic(const std::string
& logic
) const
7791 CVC5_API_TRY_CATCH_BEGIN
;
7792 CVC5_API_CHECK(!d_slv
->isFullyInited())
7793 << "Invalid call to 'setLogic', solver is already fully initialized";
7794 cvc5::LogicInfo
logic_info(logic
);
7795 //////// all checks before this line
7796 d_slv
->setLogic(logic_info
);
7798 CVC5_API_TRY_CATCH_END
;
7801 void Solver::setOption(const std::string
& option
,
7802 const std::string
& value
) const
7804 CVC5_API_TRY_CATCH_BEGIN
;
7805 std::vector
<std::string
> options
= options::getNames();
7806 CVC5_API_UNSUPPORTED_CHECK(
7807 option
.find("command-verbosity") != std::string::npos
7808 || std::find(options
.cbegin(), options
.cend(), option
) != options
.cend())
7809 << "Unrecognized option: " << option
<< '.';
7810 static constexpr auto mutableOpts
= {"diagnostic-output-channel",
7812 "regular-output-channel",
7813 "reproducible-resource-limit",
7815 if (std::find(mutableOpts
.begin(), mutableOpts
.end(), option
)
7816 == mutableOpts
.end())
7818 CVC5_API_CHECK(!d_slv
->isFullyInited())
7819 << "Invalid call to 'setOption' for option '" << option
7820 << "', solver is already fully initialized";
7822 //////// all checks before this line
7823 d_slv
->setOption(option
, value
);
7825 CVC5_API_TRY_CATCH_END
;
7828 Term
Solver::mkSygusVar(const Sort
& sort
, const std::string
& symbol
) const
7830 CVC5_API_TRY_CATCH_BEGIN
;
7831 CVC5_API_SOLVER_CHECK_SORT(sort
);
7832 //////// all checks before this line
7833 Node res
= getNodeManager()->mkBoundVar(symbol
, *sort
.d_type
);
7834 (void)res
.getType(true); /* kick off type checking */
7836 d_slv
->declareSygusVar(res
);
7838 return Term(this, res
);
7840 CVC5_API_TRY_CATCH_END
;
7843 Grammar
Solver::mkSygusGrammar(const std::vector
<Term
>& boundVars
,
7844 const std::vector
<Term
>& ntSymbols
) const
7846 CVC5_API_TRY_CATCH_BEGIN
;
7847 CVC5_API_ARG_SIZE_CHECK_EXPECTED(!ntSymbols
.empty(), ntSymbols
)
7848 << "a non-empty vector";
7849 CVC5_API_SOLVER_CHECK_BOUND_VARS(boundVars
);
7850 CVC5_API_SOLVER_CHECK_BOUND_VARS(ntSymbols
);
7851 //////// all checks before this line
7852 return Grammar(this, boundVars
, ntSymbols
);
7854 CVC5_API_TRY_CATCH_END
;
7857 Term
Solver::synthFun(const std::string
& symbol
,
7858 const std::vector
<Term
>& boundVars
,
7859 const Sort
& sort
) const
7861 CVC5_API_TRY_CATCH_BEGIN
;
7862 CVC5_API_SOLVER_CHECK_BOUND_VARS(boundVars
);
7863 CVC5_API_SOLVER_CHECK_SORT(sort
);
7864 //////// all checks before this line
7865 return synthFunHelper(symbol
, boundVars
, sort
);
7867 CVC5_API_TRY_CATCH_END
;
7870 Term
Solver::synthFun(const std::string
& symbol
,
7871 const std::vector
<Term
>& boundVars
,
7873 Grammar
& grammar
) const
7875 CVC5_API_TRY_CATCH_BEGIN
;
7876 CVC5_API_SOLVER_CHECK_BOUND_VARS(boundVars
);
7877 CVC5_API_SOLVER_CHECK_SORT(sort
);
7878 //////// all checks before this line
7879 return synthFunHelper(symbol
, boundVars
, sort
, false, &grammar
);
7881 CVC5_API_TRY_CATCH_END
;
7884 Term
Solver::synthInv(const std::string
& symbol
,
7885 const std::vector
<Term
>& boundVars
) const
7887 CVC5_API_TRY_CATCH_BEGIN
;
7888 CVC5_API_SOLVER_CHECK_BOUND_VARS(boundVars
);
7889 //////// all checks before this line
7890 return synthFunHelper(
7891 symbol
, boundVars
, Sort(this, getNodeManager()->booleanType()), true);
7893 CVC5_API_TRY_CATCH_END
;
7896 Term
Solver::synthInv(const std::string
& symbol
,
7897 const std::vector
<Term
>& boundVars
,
7898 Grammar
& grammar
) const
7900 CVC5_API_TRY_CATCH_BEGIN
;
7901 CVC5_API_SOLVER_CHECK_BOUND_VARS(boundVars
);
7902 //////// all checks before this line
7903 return synthFunHelper(symbol
,
7905 Sort(this, getNodeManager()->booleanType()),
7909 CVC5_API_TRY_CATCH_END
;
7912 void Solver::addSygusConstraint(const Term
& term
) const
7914 CVC5_API_TRY_CATCH_BEGIN
;
7915 CVC5_API_SOLVER_CHECK_TERM(term
);
7916 CVC5_API_ARG_CHECK_EXPECTED(
7917 term
.d_node
->getType() == getNodeManager()->booleanType(), term
)
7919 //////// all checks before this line
7920 d_slv
->assertSygusConstraint(*term
.d_node
, false);
7922 CVC5_API_TRY_CATCH_END
;
7925 void Solver::addSygusAssume(const Term
& term
) const
7927 CVC5_API_TRY_CATCH_BEGIN
;
7928 CVC5_API_SOLVER_CHECK_TERM(term
);
7929 CVC5_API_ARG_CHECK_EXPECTED(
7930 term
.d_node
->getType() == getNodeManager()->booleanType(), term
)
7932 //////// all checks before this line
7933 d_slv
->assertSygusConstraint(*term
.d_node
, true);
7935 CVC5_API_TRY_CATCH_END
;
7938 void Solver::addSygusInvConstraint(Term inv
,
7943 CVC5_API_TRY_CATCH_BEGIN
;
7944 CVC5_API_SOLVER_CHECK_TERM(inv
);
7945 CVC5_API_SOLVER_CHECK_TERM(pre
);
7946 CVC5_API_SOLVER_CHECK_TERM(trans
);
7947 CVC5_API_SOLVER_CHECK_TERM(post
);
7949 CVC5_API_ARG_CHECK_EXPECTED(inv
.d_node
->getType().isFunction(), inv
)
7952 TypeNode invType
= inv
.d_node
->getType();
7954 CVC5_API_ARG_CHECK_EXPECTED(invType
.getRangeType().isBoolean(), inv
)
7957 CVC5_API_CHECK(pre
.d_node
->getType() == invType
)
7958 << "Expected inv and pre to have the same sort";
7960 CVC5_API_CHECK(post
.d_node
->getType() == invType
)
7961 << "Expected inv and post to have the same sort";
7962 //////// all checks before this line
7964 const std::vector
<TypeNode
>& invArgTypes
= invType
.getArgTypes();
7966 std::vector
<TypeNode
> expectedTypes
;
7967 expectedTypes
.reserve(2 * invArgTypes
.size() + 1);
7969 for (size_t i
= 0, n
= invArgTypes
.size(); i
< 2 * n
; i
+= 2)
7971 expectedTypes
.push_back(invArgTypes
[i
% n
]);
7972 expectedTypes
.push_back(invArgTypes
[(i
+ 1) % n
]);
7975 expectedTypes
.push_back(invType
.getRangeType());
7976 TypeNode expectedTransType
= getNodeManager()->mkFunctionType(expectedTypes
);
7978 CVC5_API_CHECK(trans
.d_node
->getType() == expectedTransType
)
7979 << "Expected trans's sort to be " << invType
;
7981 d_slv
->assertSygusInvConstraint(
7982 *inv
.d_node
, *pre
.d_node
, *trans
.d_node
, *post
.d_node
);
7984 CVC5_API_TRY_CATCH_END
;
7987 Result
Solver::checkSynth() const
7989 CVC5_API_TRY_CATCH_BEGIN
;
7990 //////// all checks before this line
7991 return d_slv
->checkSynth();
7993 CVC5_API_TRY_CATCH_END
;
7996 Result
Solver::checkSynthNext() const
7998 CVC5_API_TRY_CATCH_BEGIN
;
7999 CVC5_API_CHECK(d_slv
->getOptions().base
.incrementalSolving
)
8000 << "Cannot checkSynthNext when not solving incrementally (use "
8002 //////// all checks before this line
8003 return d_slv
->checkSynth(true);
8005 CVC5_API_TRY_CATCH_END
;
8008 Term
Solver::getSynthSolution(Term term
) const
8010 CVC5_API_TRY_CATCH_BEGIN
;
8011 CVC5_API_SOLVER_CHECK_TERM(term
);
8013 std::map
<cvc5::Node
, cvc5::Node
> map
;
8014 CVC5_API_CHECK(d_slv
->getSynthSolutions(map
))
8015 << "The solver is not in a state immediately preceded by a "
8016 "successful call to checkSynth";
8018 std::map
<cvc5::Node
, cvc5::Node
>::const_iterator it
= map
.find(*term
.d_node
);
8020 CVC5_API_CHECK(it
!= map
.cend()) << "Synth solution not found for given term";
8021 //////// all checks before this line
8022 return Term(this, it
->second
);
8024 CVC5_API_TRY_CATCH_END
;
8027 std::vector
<Term
> Solver::getSynthSolutions(
8028 const std::vector
<Term
>& terms
) const
8030 CVC5_API_TRY_CATCH_BEGIN
;
8031 CVC5_API_ARG_SIZE_CHECK_EXPECTED(!terms
.empty(), terms
) << "non-empty vector";
8032 CVC5_API_SOLVER_CHECK_TERMS(terms
);
8034 std::map
<cvc5::Node
, cvc5::Node
> map
;
8035 CVC5_API_CHECK(d_slv
->getSynthSolutions(map
))
8036 << "The solver is not in a state immediately preceded by a "
8037 "successful call to checkSynth";
8038 //////// all checks before this line
8040 std::vector
<Term
> synthSolution
;
8041 synthSolution
.reserve(terms
.size());
8043 for (size_t i
= 0, n
= terms
.size(); i
< n
; ++i
)
8045 std::map
<cvc5::Node
, cvc5::Node
>::const_iterator it
=
8046 map
.find(*terms
[i
].d_node
);
8048 CVC5_API_CHECK(it
!= map
.cend())
8049 << "Synth solution not found for term at index " << i
;
8051 synthSolution
.push_back(Term(this, it
->second
));
8054 return synthSolution
;
8056 CVC5_API_TRY_CATCH_END
;
8059 Statistics
Solver::getStatistics() const
8061 return Statistics(d_slv
->getStatisticsRegistry());
8064 bool Solver::isOutputOn(const std::string
& tag
) const
8066 // `isOutputOn(tag)` may raise an `OptionException`, which we do not want to
8067 // forward as such. We thus do not use the standard exception handling macros
8068 // here but roll our own.
8071 return d_slv
->getEnv().isOutputOn(tag
);
8073 catch (const cvc5::Exception
& e
)
8075 throw CVC5ApiException("Invalid output tag " + tag
);
8079 std::ostream
& Solver::getOutput(const std::string
& tag
) const
8081 // `output(tag)` may raise an `OptionException`, which we do not want to
8082 // forward as such. We thus do not use the standard exception handling macros
8083 // here but roll our own.
8086 return d_slv
->getEnv().output(tag
);
8088 catch (const cvc5::Exception
& e
)
8090 throw CVC5ApiException("Invalid output tag " + tag
);
8100 size_t hash
<cvc5::api::Kind
>::operator()(cvc5::api::Kind k
) const
8102 return static_cast<size_t>(k
);
8105 size_t hash
<cvc5::api::Op
>::operator()(const cvc5::api::Op
& t
) const
8107 if (t
.isIndexedHelper())
8109 return std::hash
<cvc5::Node
>()(*t
.d_node
);
8113 return std::hash
<cvc5::api::Kind
>()(t
.d_kind
);
8117 size_t std::hash
<cvc5::api::RoundingMode
>::operator()(
8118 cvc5::api::RoundingMode rm
) const
8120 return static_cast<size_t>(rm
);
8123 size_t std::hash
<cvc5::api::Sort
>::operator()(const cvc5::api::Sort
& s
) const
8125 return std::hash
<cvc5::TypeNode
>()(*s
.d_type
);
8128 size_t std::hash
<cvc5::api::Term
>::operator()(const cvc5::api::Term
& t
) const
8130 return std::hash
<cvc5::Node
>()(*t
.d_node
);