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 "options/base_options.h"
60 #include "options/main_options.h"
61 #include "options/option_exception.h"
62 #include "options/options.h"
63 #include "options/options_public.h"
64 #include "options/smt_options.h"
65 #include "proof/unsat_core.h"
67 #include "smt/model.h"
68 #include "smt/smt_mode.h"
69 #include "smt/solver_engine.h"
70 #include "theory/datatypes/tuple_project_op.h"
71 #include "theory/logic_info.h"
72 #include "theory/theory_model.h"
73 #include "util/bitvector.h"
74 #include "util/divisible.h"
75 #include "util/floatingpoint.h"
76 #include "util/iand.h"
77 #include "util/random.h"
78 #include "util/regexp.h"
79 #include "util/result.h"
80 #include "util/roundingmode.h"
81 #include "util/statistics_registry.h"
82 #include "util/statistics_stats.h"
83 #include "util/statistics_value.h"
84 #include "util/string.h"
85 #include "util/uninterpreted_sort_value.h"
86 #include "util/utility.h"
91 /* -------------------------------------------------------------------------- */
93 /* -------------------------------------------------------------------------- */
97 HistogramStat
<TypeConstant
> d_consts
;
98 HistogramStat
<TypeConstant
> d_vars
;
99 HistogramStat
<Kind
> d_terms
;
102 /* -------------------------------------------------------------------------- */
104 /* -------------------------------------------------------------------------- */
106 /* Mapping from external (API) kind to internal kind. */
107 const static std::unordered_map
<Kind
, cvc5::Kind
> s_kinds
{
108 {INTERNAL_KIND
, cvc5::Kind::UNDEFINED_KIND
},
109 {UNDEFINED_KIND
, cvc5::Kind::UNDEFINED_KIND
},
110 {NULL_EXPR
, cvc5::Kind::NULL_EXPR
},
111 /* Builtin ------------------------------------------------------------- */
112 {UNINTERPRETED_SORT_VALUE
, cvc5::Kind::UNINTERPRETED_SORT_VALUE
},
113 {EQUAL
, cvc5::Kind::EQUAL
},
114 {DISTINCT
, cvc5::Kind::DISTINCT
},
115 {CONSTANT
, cvc5::Kind::VARIABLE
},
116 {VARIABLE
, cvc5::Kind::BOUND_VARIABLE
},
117 {SEXPR
, cvc5::Kind::SEXPR
},
118 {LAMBDA
, cvc5::Kind::LAMBDA
},
119 {WITNESS
, cvc5::Kind::WITNESS
},
120 /* Boolean ------------------------------------------------------------- */
121 {CONST_BOOLEAN
, cvc5::Kind::CONST_BOOLEAN
},
122 {NOT
, cvc5::Kind::NOT
},
123 {AND
, cvc5::Kind::AND
},
124 {IMPLIES
, cvc5::Kind::IMPLIES
},
125 {OR
, cvc5::Kind::OR
},
126 {XOR
, cvc5::Kind::XOR
},
127 {ITE
, cvc5::Kind::ITE
},
128 /* UF ------------------------------------------------------------------ */
129 {APPLY_UF
, cvc5::Kind::APPLY_UF
},
130 {CARDINALITY_CONSTRAINT
, cvc5::Kind::CARDINALITY_CONSTRAINT
},
131 {HO_APPLY
, cvc5::Kind::HO_APPLY
},
132 /* Arithmetic ---------------------------------------------------------- */
133 {PLUS
, cvc5::Kind::PLUS
},
134 {MULT
, cvc5::Kind::MULT
},
135 {IAND
, cvc5::Kind::IAND
},
136 {POW2
, cvc5::Kind::POW2
},
137 {MINUS
, cvc5::Kind::MINUS
},
138 {UMINUS
, cvc5::Kind::UMINUS
},
139 {DIVISION
, cvc5::Kind::DIVISION
},
140 {INTS_DIVISION
, cvc5::Kind::INTS_DIVISION
},
141 {INTS_MODULUS
, cvc5::Kind::INTS_MODULUS
},
142 {ABS
, cvc5::Kind::ABS
},
143 {DIVISIBLE
, cvc5::Kind::DIVISIBLE
},
144 {POW
, cvc5::Kind::POW
},
145 {EXPONENTIAL
, cvc5::Kind::EXPONENTIAL
},
146 {SINE
, cvc5::Kind::SINE
},
147 {COSINE
, cvc5::Kind::COSINE
},
148 {TANGENT
, cvc5::Kind::TANGENT
},
149 {COSECANT
, cvc5::Kind::COSECANT
},
150 {SECANT
, cvc5::Kind::SECANT
},
151 {COTANGENT
, cvc5::Kind::COTANGENT
},
152 {ARCSINE
, cvc5::Kind::ARCSINE
},
153 {ARCCOSINE
, cvc5::Kind::ARCCOSINE
},
154 {ARCTANGENT
, cvc5::Kind::ARCTANGENT
},
155 {ARCCOSECANT
, cvc5::Kind::ARCCOSECANT
},
156 {ARCSECANT
, cvc5::Kind::ARCSECANT
},
157 {ARCCOTANGENT
, cvc5::Kind::ARCCOTANGENT
},
158 {SQRT
, cvc5::Kind::SQRT
},
159 {CONST_RATIONAL
, cvc5::Kind::CONST_RATIONAL
},
160 {LT
, cvc5::Kind::LT
},
161 {LEQ
, cvc5::Kind::LEQ
},
162 {GT
, cvc5::Kind::GT
},
163 {GEQ
, cvc5::Kind::GEQ
},
164 {IS_INTEGER
, cvc5::Kind::IS_INTEGER
},
165 {TO_INTEGER
, cvc5::Kind::TO_INTEGER
},
166 {TO_REAL
, cvc5::Kind::TO_REAL
},
167 {PI
, cvc5::Kind::PI
},
168 /* BV ------------------------------------------------------------------ */
169 {CONST_BITVECTOR
, cvc5::Kind::CONST_BITVECTOR
},
170 {BITVECTOR_CONCAT
, cvc5::Kind::BITVECTOR_CONCAT
},
171 {BITVECTOR_AND
, cvc5::Kind::BITVECTOR_AND
},
172 {BITVECTOR_OR
, cvc5::Kind::BITVECTOR_OR
},
173 {BITVECTOR_XOR
, cvc5::Kind::BITVECTOR_XOR
},
174 {BITVECTOR_NOT
, cvc5::Kind::BITVECTOR_NOT
},
175 {BITVECTOR_NAND
, cvc5::Kind::BITVECTOR_NAND
},
176 {BITVECTOR_NOR
, cvc5::Kind::BITVECTOR_NOR
},
177 {BITVECTOR_XNOR
, cvc5::Kind::BITVECTOR_XNOR
},
178 {BITVECTOR_COMP
, cvc5::Kind::BITVECTOR_COMP
},
179 {BITVECTOR_MULT
, cvc5::Kind::BITVECTOR_MULT
},
180 {BITVECTOR_ADD
, cvc5::Kind::BITVECTOR_ADD
},
181 {BITVECTOR_SUB
, cvc5::Kind::BITVECTOR_SUB
},
182 {BITVECTOR_NEG
, cvc5::Kind::BITVECTOR_NEG
},
183 {BITVECTOR_UDIV
, cvc5::Kind::BITVECTOR_UDIV
},
184 {BITVECTOR_UREM
, cvc5::Kind::BITVECTOR_UREM
},
185 {BITVECTOR_SDIV
, cvc5::Kind::BITVECTOR_SDIV
},
186 {BITVECTOR_SREM
, cvc5::Kind::BITVECTOR_SREM
},
187 {BITVECTOR_SMOD
, cvc5::Kind::BITVECTOR_SMOD
},
188 {BITVECTOR_SHL
, cvc5::Kind::BITVECTOR_SHL
},
189 {BITVECTOR_LSHR
, cvc5::Kind::BITVECTOR_LSHR
},
190 {BITVECTOR_ASHR
, cvc5::Kind::BITVECTOR_ASHR
},
191 {BITVECTOR_ULT
, cvc5::Kind::BITVECTOR_ULT
},
192 {BITVECTOR_ULE
, cvc5::Kind::BITVECTOR_ULE
},
193 {BITVECTOR_UGT
, cvc5::Kind::BITVECTOR_UGT
},
194 {BITVECTOR_UGE
, cvc5::Kind::BITVECTOR_UGE
},
195 {BITVECTOR_SLT
, cvc5::Kind::BITVECTOR_SLT
},
196 {BITVECTOR_SLE
, cvc5::Kind::BITVECTOR_SLE
},
197 {BITVECTOR_SGT
, cvc5::Kind::BITVECTOR_SGT
},
198 {BITVECTOR_SGE
, cvc5::Kind::BITVECTOR_SGE
},
199 {BITVECTOR_ULTBV
, cvc5::Kind::BITVECTOR_ULTBV
},
200 {BITVECTOR_SLTBV
, cvc5::Kind::BITVECTOR_SLTBV
},
201 {BITVECTOR_ITE
, cvc5::Kind::BITVECTOR_ITE
},
202 {BITVECTOR_REDOR
, cvc5::Kind::BITVECTOR_REDOR
},
203 {BITVECTOR_REDAND
, cvc5::Kind::BITVECTOR_REDAND
},
204 {BITVECTOR_EXTRACT
, cvc5::Kind::BITVECTOR_EXTRACT
},
205 {BITVECTOR_REPEAT
, cvc5::Kind::BITVECTOR_REPEAT
},
206 {BITVECTOR_ZERO_EXTEND
, cvc5::Kind::BITVECTOR_ZERO_EXTEND
},
207 {BITVECTOR_SIGN_EXTEND
, cvc5::Kind::BITVECTOR_SIGN_EXTEND
},
208 {BITVECTOR_ROTATE_LEFT
, cvc5::Kind::BITVECTOR_ROTATE_LEFT
},
209 {BITVECTOR_ROTATE_RIGHT
, cvc5::Kind::BITVECTOR_ROTATE_RIGHT
},
210 {INT_TO_BITVECTOR
, cvc5::Kind::INT_TO_BITVECTOR
},
211 {BITVECTOR_TO_NAT
, cvc5::Kind::BITVECTOR_TO_NAT
},
212 /* FP ------------------------------------------------------------------ */
213 {CONST_FLOATINGPOINT
, cvc5::Kind::CONST_FLOATINGPOINT
},
214 {CONST_ROUNDINGMODE
, cvc5::Kind::CONST_ROUNDINGMODE
},
215 {FLOATINGPOINT_FP
, cvc5::Kind::FLOATINGPOINT_FP
},
216 {FLOATINGPOINT_EQ
, cvc5::Kind::FLOATINGPOINT_EQ
},
217 {FLOATINGPOINT_ABS
, cvc5::Kind::FLOATINGPOINT_ABS
},
218 {FLOATINGPOINT_NEG
, cvc5::Kind::FLOATINGPOINT_NEG
},
219 {FLOATINGPOINT_ADD
, cvc5::Kind::FLOATINGPOINT_ADD
},
220 {FLOATINGPOINT_SUB
, cvc5::Kind::FLOATINGPOINT_SUB
},
221 {FLOATINGPOINT_MULT
, cvc5::Kind::FLOATINGPOINT_MULT
},
222 {FLOATINGPOINT_DIV
, cvc5::Kind::FLOATINGPOINT_DIV
},
223 {FLOATINGPOINT_FMA
, cvc5::Kind::FLOATINGPOINT_FMA
},
224 {FLOATINGPOINT_SQRT
, cvc5::Kind::FLOATINGPOINT_SQRT
},
225 {FLOATINGPOINT_REM
, cvc5::Kind::FLOATINGPOINT_REM
},
226 {FLOATINGPOINT_RTI
, cvc5::Kind::FLOATINGPOINT_RTI
},
227 {FLOATINGPOINT_MIN
, cvc5::Kind::FLOATINGPOINT_MIN
},
228 {FLOATINGPOINT_MAX
, cvc5::Kind::FLOATINGPOINT_MAX
},
229 {FLOATINGPOINT_LEQ
, cvc5::Kind::FLOATINGPOINT_LEQ
},
230 {FLOATINGPOINT_LT
, cvc5::Kind::FLOATINGPOINT_LT
},
231 {FLOATINGPOINT_GEQ
, cvc5::Kind::FLOATINGPOINT_GEQ
},
232 {FLOATINGPOINT_GT
, cvc5::Kind::FLOATINGPOINT_GT
},
233 {FLOATINGPOINT_ISN
, cvc5::Kind::FLOATINGPOINT_ISN
},
234 {FLOATINGPOINT_ISSN
, cvc5::Kind::FLOATINGPOINT_ISSN
},
235 {FLOATINGPOINT_ISZ
, cvc5::Kind::FLOATINGPOINT_ISZ
},
236 {FLOATINGPOINT_ISINF
, cvc5::Kind::FLOATINGPOINT_ISINF
},
237 {FLOATINGPOINT_ISNAN
, cvc5::Kind::FLOATINGPOINT_ISNAN
},
238 {FLOATINGPOINT_ISNEG
, cvc5::Kind::FLOATINGPOINT_ISNEG
},
239 {FLOATINGPOINT_ISPOS
, cvc5::Kind::FLOATINGPOINT_ISPOS
},
240 {FLOATINGPOINT_TO_FP_FLOATINGPOINT
,
241 cvc5::Kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT
},
242 {FLOATINGPOINT_TO_FP_IEEE_BITVECTOR
,
243 cvc5::Kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR
},
244 {FLOATINGPOINT_TO_FP_REAL
, cvc5::Kind::FLOATINGPOINT_TO_FP_REAL
},
245 {FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR
,
246 cvc5::Kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR
},
247 {FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR
,
248 cvc5::Kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR
},
249 {FLOATINGPOINT_TO_FP_GENERIC
, cvc5::Kind::FLOATINGPOINT_TO_FP_GENERIC
},
250 {FLOATINGPOINT_TO_UBV
, cvc5::Kind::FLOATINGPOINT_TO_UBV
},
251 {FLOATINGPOINT_TO_SBV
, cvc5::Kind::FLOATINGPOINT_TO_SBV
},
252 {FLOATINGPOINT_TO_REAL
, cvc5::Kind::FLOATINGPOINT_TO_REAL
},
253 /* Arrays -------------------------------------------------------------- */
254 {SELECT
, cvc5::Kind::SELECT
},
255 {STORE
, cvc5::Kind::STORE
},
256 {CONST_ARRAY
, cvc5::Kind::STORE_ALL
},
257 {EQ_RANGE
, cvc5::Kind::EQ_RANGE
},
258 /* Datatypes ----------------------------------------------------------- */
259 {APPLY_SELECTOR
, cvc5::Kind::APPLY_SELECTOR
},
260 {APPLY_CONSTRUCTOR
, cvc5::Kind::APPLY_CONSTRUCTOR
},
261 {APPLY_TESTER
, cvc5::Kind::APPLY_TESTER
},
262 {APPLY_UPDATER
, cvc5::Kind::APPLY_UPDATER
},
263 {DT_SIZE
, cvc5::Kind::DT_SIZE
},
264 {MATCH
, cvc5::Kind::MATCH
},
265 {MATCH_CASE
, cvc5::Kind::MATCH_CASE
},
266 {MATCH_BIND_CASE
, cvc5::Kind::MATCH_BIND_CASE
},
267 {TUPLE_PROJECT
, cvc5::Kind::TUPLE_PROJECT
},
268 /* Separation Logic ---------------------------------------------------- */
269 {SEP_NIL
, cvc5::Kind::SEP_NIL
},
270 {SEP_EMP
, cvc5::Kind::SEP_EMP
},
271 {SEP_PTO
, cvc5::Kind::SEP_PTO
},
272 {SEP_STAR
, cvc5::Kind::SEP_STAR
},
273 {SEP_WAND
, cvc5::Kind::SEP_WAND
},
274 /* Sets ---------------------------------------------------------------- */
275 {SET_EMPTY
, cvc5::Kind::SET_EMPTY
},
276 {SET_UNION
, cvc5::Kind::SET_UNION
},
277 {SET_INTER
, cvc5::Kind::SET_INTER
},
278 {SET_MINUS
, cvc5::Kind::SET_MINUS
},
279 {SET_SUBSET
, cvc5::Kind::SET_SUBSET
},
280 {SET_MEMBER
, cvc5::Kind::SET_MEMBER
},
281 {SET_SINGLETON
, cvc5::Kind::SET_SINGLETON
},
282 {SET_INSERT
, cvc5::Kind::SET_INSERT
},
283 {SET_CARD
, cvc5::Kind::SET_CARD
},
284 {SET_COMPLEMENT
, cvc5::Kind::SET_COMPLEMENT
},
285 {SET_UNIVERSE
, cvc5::Kind::SET_UNIVERSE
},
286 {SET_COMPREHENSION
, cvc5::Kind::SET_COMPREHENSION
},
287 {SET_CHOOSE
, cvc5::Kind::SET_CHOOSE
},
288 {SET_IS_SINGLETON
, cvc5::Kind::SET_IS_SINGLETON
},
289 {SET_MAP
, cvc5::Kind::SET_MAP
},
290 /* Relations ----------------------------------------------------------- */
291 {RELATION_JOIN
, cvc5::Kind::RELATION_JOIN
},
292 {RELATION_PRODUCT
, cvc5::Kind::RELATION_PRODUCT
},
293 {RELATION_TRANSPOSE
, cvc5::Kind::RELATION_TRANSPOSE
},
294 {RELATION_TCLOSURE
, cvc5::Kind::RELATION_TCLOSURE
},
295 {RELATION_JOIN_IMAGE
, cvc5::Kind::RELATION_JOIN_IMAGE
},
296 {RELATION_IDEN
, cvc5::Kind::RELATION_IDEN
},
297 /* Bags ---------------------------------------------------------------- */
298 {BAG_UNION_MAX
, cvc5::Kind::BAG_UNION_MAX
},
299 {BAG_UNION_DISJOINT
, cvc5::Kind::BAG_UNION_DISJOINT
},
300 {BAG_INTER_MIN
, cvc5::Kind::BAG_INTER_MIN
},
301 {BAG_DIFFERENCE_SUBTRACT
, cvc5::Kind::BAG_DIFFERENCE_SUBTRACT
},
302 {BAG_DIFFERENCE_REMOVE
, cvc5::Kind::BAG_DIFFERENCE_REMOVE
},
303 {BAG_SUBBAG
, cvc5::Kind::BAG_SUBBAG
},
304 {BAG_COUNT
, cvc5::Kind::BAG_COUNT
},
305 {BAG_MEMBER
, cvc5::Kind::BAG_MEMBER
},
306 {BAG_DUPLICATE_REMOVAL
, cvc5::Kind::BAG_DUPLICATE_REMOVAL
},
307 {BAG_MAKE
, cvc5::Kind::BAG_MAKE
},
308 {BAG_EMPTY
, cvc5::Kind::BAG_EMPTY
},
309 {BAG_CARD
, cvc5::Kind::BAG_CARD
},
310 {BAG_CHOOSE
, cvc5::Kind::BAG_CHOOSE
},
311 {BAG_IS_SINGLETON
, cvc5::Kind::BAG_IS_SINGLETON
},
312 {BAG_FROM_SET
, cvc5::Kind::BAG_FROM_SET
},
313 {BAG_TO_SET
, cvc5::Kind::BAG_TO_SET
},
314 {BAG_MAP
, cvc5::Kind::BAG_MAP
},
315 {BAG_FILTER
, cvc5::Kind::BAG_FILTER
},
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_SORT_VALUE
, UNINTERPRETED_SORT_VALUE
},
395 {cvc5::Kind::EQUAL
, EQUAL
},
396 {cvc5::Kind::DISTINCT
, DISTINCT
},
397 {cvc5::Kind::VARIABLE
, CONSTANT
},
398 {cvc5::Kind::BOUND_VARIABLE
, VARIABLE
},
399 {cvc5::Kind::SEXPR
, SEXPR
},
400 {cvc5::Kind::LAMBDA
, LAMBDA
},
401 {cvc5::Kind::WITNESS
, WITNESS
},
402 /* Boolean --------------------------------------------------------- */
403 {cvc5::Kind::CONST_BOOLEAN
, CONST_BOOLEAN
},
404 {cvc5::Kind::NOT
, NOT
},
405 {cvc5::Kind::AND
, AND
},
406 {cvc5::Kind::IMPLIES
, IMPLIES
},
407 {cvc5::Kind::OR
, OR
},
408 {cvc5::Kind::XOR
, XOR
},
409 {cvc5::Kind::ITE
, ITE
},
410 /* UF -------------------------------------------------------------- */
411 {cvc5::Kind::APPLY_UF
, APPLY_UF
},
412 {cvc5::Kind::CARDINALITY_CONSTRAINT
, CARDINALITY_CONSTRAINT
},
413 {cvc5::Kind::HO_APPLY
, HO_APPLY
},
414 /* Arithmetic ------------------------------------------------------ */
415 {cvc5::Kind::PLUS
, PLUS
},
416 {cvc5::Kind::MULT
, MULT
},
417 {cvc5::Kind::IAND
, IAND
},
418 {cvc5::Kind::POW2
, POW2
},
419 {cvc5::Kind::MINUS
, MINUS
},
420 {cvc5::Kind::UMINUS
, UMINUS
},
421 {cvc5::Kind::DIVISION
, DIVISION
},
422 {cvc5::Kind::DIVISION_TOTAL
, INTERNAL_KIND
},
423 {cvc5::Kind::INTS_DIVISION
, INTS_DIVISION
},
424 {cvc5::Kind::INTS_DIVISION_TOTAL
, INTERNAL_KIND
},
425 {cvc5::Kind::INTS_MODULUS
, INTS_MODULUS
},
426 {cvc5::Kind::INTS_MODULUS_TOTAL
, INTERNAL_KIND
},
427 {cvc5::Kind::ABS
, ABS
},
428 {cvc5::Kind::DIVISIBLE
, DIVISIBLE
},
429 {cvc5::Kind::POW
, POW
},
430 {cvc5::Kind::EXPONENTIAL
, EXPONENTIAL
},
431 {cvc5::Kind::SINE
, SINE
},
432 {cvc5::Kind::COSINE
, COSINE
},
433 {cvc5::Kind::TANGENT
, TANGENT
},
434 {cvc5::Kind::COSECANT
, COSECANT
},
435 {cvc5::Kind::SECANT
, SECANT
},
436 {cvc5::Kind::COTANGENT
, COTANGENT
},
437 {cvc5::Kind::ARCSINE
, ARCSINE
},
438 {cvc5::Kind::ARCCOSINE
, ARCCOSINE
},
439 {cvc5::Kind::ARCTANGENT
, ARCTANGENT
},
440 {cvc5::Kind::ARCCOSECANT
, ARCCOSECANT
},
441 {cvc5::Kind::ARCSECANT
, ARCSECANT
},
442 {cvc5::Kind::ARCCOTANGENT
, ARCCOTANGENT
},
443 {cvc5::Kind::SQRT
, SQRT
},
444 {cvc5::Kind::DIVISIBLE_OP
, DIVISIBLE
},
445 {cvc5::Kind::CONST_RATIONAL
, CONST_RATIONAL
},
446 {cvc5::Kind::LT
, LT
},
447 {cvc5::Kind::LEQ
, LEQ
},
448 {cvc5::Kind::GT
, GT
},
449 {cvc5::Kind::GEQ
, GEQ
},
450 {cvc5::Kind::IS_INTEGER
, IS_INTEGER
},
451 {cvc5::Kind::TO_INTEGER
, TO_INTEGER
},
452 {cvc5::Kind::TO_REAL
, TO_REAL
},
453 {cvc5::Kind::PI
, PI
},
454 {cvc5::Kind::IAND_OP
, IAND
},
455 /* BV -------------------------------------------------------------- */
456 {cvc5::Kind::CONST_BITVECTOR
, CONST_BITVECTOR
},
457 {cvc5::Kind::BITVECTOR_CONCAT
, BITVECTOR_CONCAT
},
458 {cvc5::Kind::BITVECTOR_AND
, BITVECTOR_AND
},
459 {cvc5::Kind::BITVECTOR_OR
, BITVECTOR_OR
},
460 {cvc5::Kind::BITVECTOR_XOR
, BITVECTOR_XOR
},
461 {cvc5::Kind::BITVECTOR_NOT
, BITVECTOR_NOT
},
462 {cvc5::Kind::BITVECTOR_NAND
, BITVECTOR_NAND
},
463 {cvc5::Kind::BITVECTOR_NOR
, BITVECTOR_NOR
},
464 {cvc5::Kind::BITVECTOR_XNOR
, BITVECTOR_XNOR
},
465 {cvc5::Kind::BITVECTOR_COMP
, BITVECTOR_COMP
},
466 {cvc5::Kind::BITVECTOR_MULT
, BITVECTOR_MULT
},
467 {cvc5::Kind::BITVECTOR_ADD
, BITVECTOR_ADD
},
468 {cvc5::Kind::BITVECTOR_SUB
, BITVECTOR_SUB
},
469 {cvc5::Kind::BITVECTOR_NEG
, BITVECTOR_NEG
},
470 {cvc5::Kind::BITVECTOR_UDIV
, BITVECTOR_UDIV
},
471 {cvc5::Kind::BITVECTOR_UREM
, BITVECTOR_UREM
},
472 {cvc5::Kind::BITVECTOR_SDIV
, BITVECTOR_SDIV
},
473 {cvc5::Kind::BITVECTOR_SREM
, BITVECTOR_SREM
},
474 {cvc5::Kind::BITVECTOR_SMOD
, BITVECTOR_SMOD
},
475 {cvc5::Kind::BITVECTOR_SHL
, BITVECTOR_SHL
},
476 {cvc5::Kind::BITVECTOR_LSHR
, BITVECTOR_LSHR
},
477 {cvc5::Kind::BITVECTOR_ASHR
, BITVECTOR_ASHR
},
478 {cvc5::Kind::BITVECTOR_ULT
, BITVECTOR_ULT
},
479 {cvc5::Kind::BITVECTOR_ULE
, BITVECTOR_ULE
},
480 {cvc5::Kind::BITVECTOR_UGT
, BITVECTOR_UGT
},
481 {cvc5::Kind::BITVECTOR_UGE
, BITVECTOR_UGE
},
482 {cvc5::Kind::BITVECTOR_SLT
, BITVECTOR_SLT
},
483 {cvc5::Kind::BITVECTOR_SLE
, BITVECTOR_SLE
},
484 {cvc5::Kind::BITVECTOR_SGT
, BITVECTOR_SGT
},
485 {cvc5::Kind::BITVECTOR_SGE
, BITVECTOR_SGE
},
486 {cvc5::Kind::BITVECTOR_ULTBV
, BITVECTOR_ULTBV
},
487 {cvc5::Kind::BITVECTOR_SLTBV
, BITVECTOR_SLTBV
},
488 {cvc5::Kind::BITVECTOR_ITE
, BITVECTOR_ITE
},
489 {cvc5::Kind::BITVECTOR_REDOR
, BITVECTOR_REDOR
},
490 {cvc5::Kind::BITVECTOR_REDAND
, BITVECTOR_REDAND
},
491 {cvc5::Kind::BITVECTOR_EXTRACT_OP
, BITVECTOR_EXTRACT
},
492 {cvc5::Kind::BITVECTOR_REPEAT_OP
, BITVECTOR_REPEAT
},
493 {cvc5::Kind::BITVECTOR_ZERO_EXTEND_OP
, BITVECTOR_ZERO_EXTEND
},
494 {cvc5::Kind::BITVECTOR_SIGN_EXTEND_OP
, BITVECTOR_SIGN_EXTEND
},
495 {cvc5::Kind::BITVECTOR_ROTATE_LEFT_OP
, BITVECTOR_ROTATE_LEFT
},
496 {cvc5::Kind::BITVECTOR_ROTATE_RIGHT_OP
, BITVECTOR_ROTATE_RIGHT
},
497 {cvc5::Kind::BITVECTOR_EXTRACT
, BITVECTOR_EXTRACT
},
498 {cvc5::Kind::BITVECTOR_REPEAT
, BITVECTOR_REPEAT
},
499 {cvc5::Kind::BITVECTOR_ZERO_EXTEND
, BITVECTOR_ZERO_EXTEND
},
500 {cvc5::Kind::BITVECTOR_SIGN_EXTEND
, BITVECTOR_SIGN_EXTEND
},
501 {cvc5::Kind::BITVECTOR_ROTATE_LEFT
, BITVECTOR_ROTATE_LEFT
},
502 {cvc5::Kind::BITVECTOR_ROTATE_RIGHT
, BITVECTOR_ROTATE_RIGHT
},
503 {cvc5::Kind::INT_TO_BITVECTOR_OP
, INT_TO_BITVECTOR
},
504 {cvc5::Kind::INT_TO_BITVECTOR
, INT_TO_BITVECTOR
},
505 {cvc5::Kind::BITVECTOR_TO_NAT
, BITVECTOR_TO_NAT
},
506 /* FP -------------------------------------------------------------- */
507 {cvc5::Kind::CONST_FLOATINGPOINT
, CONST_FLOATINGPOINT
},
508 {cvc5::Kind::CONST_ROUNDINGMODE
, CONST_ROUNDINGMODE
},
509 {cvc5::Kind::FLOATINGPOINT_FP
, FLOATINGPOINT_FP
},
510 {cvc5::Kind::FLOATINGPOINT_EQ
, FLOATINGPOINT_EQ
},
511 {cvc5::Kind::FLOATINGPOINT_ABS
, FLOATINGPOINT_ABS
},
512 {cvc5::Kind::FLOATINGPOINT_NEG
, FLOATINGPOINT_NEG
},
513 {cvc5::Kind::FLOATINGPOINT_ADD
, FLOATINGPOINT_ADD
},
514 {cvc5::Kind::FLOATINGPOINT_SUB
, FLOATINGPOINT_SUB
},
515 {cvc5::Kind::FLOATINGPOINT_MULT
, FLOATINGPOINT_MULT
},
516 {cvc5::Kind::FLOATINGPOINT_DIV
, FLOATINGPOINT_DIV
},
517 {cvc5::Kind::FLOATINGPOINT_FMA
, FLOATINGPOINT_FMA
},
518 {cvc5::Kind::FLOATINGPOINT_SQRT
, FLOATINGPOINT_SQRT
},
519 {cvc5::Kind::FLOATINGPOINT_REM
, FLOATINGPOINT_REM
},
520 {cvc5::Kind::FLOATINGPOINT_RTI
, FLOATINGPOINT_RTI
},
521 {cvc5::Kind::FLOATINGPOINT_MIN
, FLOATINGPOINT_MIN
},
522 {cvc5::Kind::FLOATINGPOINT_MAX
, FLOATINGPOINT_MAX
},
523 {cvc5::Kind::FLOATINGPOINT_LEQ
, FLOATINGPOINT_LEQ
},
524 {cvc5::Kind::FLOATINGPOINT_LT
, FLOATINGPOINT_LT
},
525 {cvc5::Kind::FLOATINGPOINT_GEQ
, FLOATINGPOINT_GEQ
},
526 {cvc5::Kind::FLOATINGPOINT_GT
, FLOATINGPOINT_GT
},
527 {cvc5::Kind::FLOATINGPOINT_ISN
, FLOATINGPOINT_ISN
},
528 {cvc5::Kind::FLOATINGPOINT_ISSN
, FLOATINGPOINT_ISSN
},
529 {cvc5::Kind::FLOATINGPOINT_ISZ
, FLOATINGPOINT_ISZ
},
530 {cvc5::Kind::FLOATINGPOINT_ISINF
, FLOATINGPOINT_ISINF
},
531 {cvc5::Kind::FLOATINGPOINT_ISNAN
, FLOATINGPOINT_ISNAN
},
532 {cvc5::Kind::FLOATINGPOINT_ISNEG
, FLOATINGPOINT_ISNEG
},
533 {cvc5::Kind::FLOATINGPOINT_ISPOS
, FLOATINGPOINT_ISPOS
},
534 {cvc5::Kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP
,
535 FLOATINGPOINT_TO_FP_IEEE_BITVECTOR
},
536 {cvc5::Kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR
,
537 FLOATINGPOINT_TO_FP_IEEE_BITVECTOR
},
538 {cvc5::Kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP
,
539 FLOATINGPOINT_TO_FP_FLOATINGPOINT
},
540 {cvc5::Kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT
,
541 FLOATINGPOINT_TO_FP_FLOATINGPOINT
},
542 {cvc5::Kind::FLOATINGPOINT_TO_FP_REAL_OP
, FLOATINGPOINT_TO_FP_REAL
},
543 {cvc5::Kind::FLOATINGPOINT_TO_FP_REAL
, FLOATINGPOINT_TO_FP_REAL
},
544 {cvc5::Kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP
,
545 FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR
},
546 {cvc5::Kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR
,
547 FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR
},
548 {cvc5::Kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP
,
549 FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR
},
550 {cvc5::Kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR
,
551 FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR
},
552 {cvc5::Kind::FLOATINGPOINT_TO_FP_GENERIC_OP
,
553 FLOATINGPOINT_TO_FP_GENERIC
},
554 {cvc5::Kind::FLOATINGPOINT_TO_FP_GENERIC
, FLOATINGPOINT_TO_FP_GENERIC
},
555 {cvc5::Kind::FLOATINGPOINT_TO_UBV_OP
, FLOATINGPOINT_TO_UBV
},
556 {cvc5::Kind::FLOATINGPOINT_TO_UBV
, FLOATINGPOINT_TO_UBV
},
557 {cvc5::Kind::FLOATINGPOINT_TO_UBV_TOTAL_OP
, INTERNAL_KIND
},
558 {cvc5::Kind::FLOATINGPOINT_TO_UBV_TOTAL
, INTERNAL_KIND
},
559 {cvc5::Kind::FLOATINGPOINT_TO_SBV_OP
, FLOATINGPOINT_TO_SBV
},
560 {cvc5::Kind::FLOATINGPOINT_TO_SBV
, FLOATINGPOINT_TO_SBV
},
561 {cvc5::Kind::FLOATINGPOINT_TO_SBV_TOTAL_OP
, INTERNAL_KIND
},
562 {cvc5::Kind::FLOATINGPOINT_TO_SBV_TOTAL
, INTERNAL_KIND
},
563 {cvc5::Kind::FLOATINGPOINT_TO_REAL
, FLOATINGPOINT_TO_REAL
},
564 {cvc5::Kind::FLOATINGPOINT_TO_REAL_TOTAL
, INTERNAL_KIND
},
565 /* Arrays ---------------------------------------------------------- */
566 {cvc5::Kind::SELECT
, SELECT
},
567 {cvc5::Kind::STORE
, STORE
},
568 {cvc5::Kind::STORE_ALL
, CONST_ARRAY
},
569 /* Datatypes ------------------------------------------------------- */
570 {cvc5::Kind::APPLY_SELECTOR
, APPLY_SELECTOR
},
571 {cvc5::Kind::APPLY_CONSTRUCTOR
, APPLY_CONSTRUCTOR
},
572 {cvc5::Kind::APPLY_SELECTOR_TOTAL
, INTERNAL_KIND
},
573 {cvc5::Kind::APPLY_TESTER
, APPLY_TESTER
},
574 {cvc5::Kind::APPLY_UPDATER
, APPLY_UPDATER
},
575 {cvc5::Kind::DT_SIZE
, DT_SIZE
},
576 {cvc5::Kind::MATCH
, MATCH
},
577 {cvc5::Kind::MATCH_CASE
, MATCH_CASE
},
578 {cvc5::Kind::MATCH_BIND_CASE
, MATCH_BIND_CASE
},
579 {cvc5::Kind::TUPLE_PROJECT
, TUPLE_PROJECT
},
580 {cvc5::Kind::TUPLE_PROJECT_OP
, TUPLE_PROJECT
},
581 /* Separation Logic ------------------------------------------------ */
582 {cvc5::Kind::SEP_NIL
, SEP_NIL
},
583 {cvc5::Kind::SEP_EMP
, SEP_EMP
},
584 {cvc5::Kind::SEP_PTO
, SEP_PTO
},
585 {cvc5::Kind::SEP_STAR
, SEP_STAR
},
586 {cvc5::Kind::SEP_WAND
, SEP_WAND
},
587 /* Sets ------------------------------------------------------------ */
588 {cvc5::Kind::SET_EMPTY
, SET_EMPTY
},
589 {cvc5::Kind::SET_UNION
, SET_UNION
},
590 {cvc5::Kind::SET_INTER
, SET_INTER
},
591 {cvc5::Kind::SET_MINUS
, SET_MINUS
},
592 {cvc5::Kind::SET_SUBSET
, SET_SUBSET
},
593 {cvc5::Kind::SET_MEMBER
, SET_MEMBER
},
594 {cvc5::Kind::SET_SINGLETON
, SET_SINGLETON
},
595 {cvc5::Kind::SET_INSERT
, SET_INSERT
},
596 {cvc5::Kind::SET_CARD
, SET_CARD
},
597 {cvc5::Kind::SET_COMPLEMENT
, SET_COMPLEMENT
},
598 {cvc5::Kind::SET_UNIVERSE
, SET_UNIVERSE
},
599 {cvc5::Kind::SET_COMPREHENSION
, SET_COMPREHENSION
},
600 {cvc5::Kind::SET_CHOOSE
, SET_CHOOSE
},
601 {cvc5::Kind::SET_IS_SINGLETON
, SET_IS_SINGLETON
},
602 {cvc5::Kind::SET_MAP
, SET_MAP
},
603 /* Relations ------------------------------------------------------- */
604 {cvc5::Kind::RELATION_JOIN
, RELATION_JOIN
},
605 {cvc5::Kind::RELATION_PRODUCT
, RELATION_PRODUCT
},
606 {cvc5::Kind::RELATION_TRANSPOSE
, RELATION_TRANSPOSE
},
607 {cvc5::Kind::RELATION_TCLOSURE
, RELATION_TCLOSURE
},
608 {cvc5::Kind::RELATION_JOIN_IMAGE
, RELATION_JOIN_IMAGE
},
609 {cvc5::Kind::RELATION_IDEN
, RELATION_IDEN
},
610 /* Bags ------------------------------------------------------------ */
611 {cvc5::Kind::BAG_UNION_MAX
, BAG_UNION_MAX
},
612 {cvc5::Kind::BAG_UNION_DISJOINT
, BAG_UNION_DISJOINT
},
613 {cvc5::Kind::BAG_INTER_MIN
, BAG_INTER_MIN
},
614 {cvc5::Kind::BAG_DIFFERENCE_SUBTRACT
, BAG_DIFFERENCE_SUBTRACT
},
615 {cvc5::Kind::BAG_DIFFERENCE_REMOVE
, BAG_DIFFERENCE_REMOVE
},
616 {cvc5::Kind::BAG_SUBBAG
, BAG_SUBBAG
},
617 {cvc5::Kind::BAG_COUNT
, BAG_COUNT
},
618 {cvc5::Kind::BAG_MEMBER
, BAG_MEMBER
},
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_FILTER
, BAG_FILTER
},
629 {cvc5::Kind::BAG_FOLD
, BAG_FOLD
},
630 /* Strings --------------------------------------------------------- */
631 {cvc5::Kind::STRING_CONCAT
, STRING_CONCAT
},
632 {cvc5::Kind::STRING_IN_REGEXP
, STRING_IN_REGEXP
},
633 {cvc5::Kind::STRING_LENGTH
, STRING_LENGTH
},
634 {cvc5::Kind::STRING_SUBSTR
, STRING_SUBSTR
},
635 {cvc5::Kind::STRING_UPDATE
, STRING_UPDATE
},
636 {cvc5::Kind::STRING_CHARAT
, STRING_CHARAT
},
637 {cvc5::Kind::STRING_CONTAINS
, STRING_CONTAINS
},
638 {cvc5::Kind::STRING_INDEXOF
, STRING_INDEXOF
},
639 {cvc5::Kind::STRING_INDEXOF_RE
, STRING_INDEXOF_RE
},
640 {cvc5::Kind::STRING_REPLACE
, STRING_REPLACE
},
641 {cvc5::Kind::STRING_REPLACE_ALL
, STRING_REPLACE_ALL
},
642 {cvc5::Kind::STRING_REPLACE_RE
, STRING_REPLACE_RE
},
643 {cvc5::Kind::STRING_REPLACE_RE_ALL
, STRING_REPLACE_RE_ALL
},
644 {cvc5::Kind::STRING_TOLOWER
, STRING_TOLOWER
},
645 {cvc5::Kind::STRING_TOUPPER
, STRING_TOUPPER
},
646 {cvc5::Kind::STRING_REV
, STRING_REV
},
647 {cvc5::Kind::STRING_FROM_CODE
, STRING_FROM_CODE
},
648 {cvc5::Kind::STRING_TO_CODE
, STRING_TO_CODE
},
649 {cvc5::Kind::STRING_LT
, STRING_LT
},
650 {cvc5::Kind::STRING_LEQ
, STRING_LEQ
},
651 {cvc5::Kind::STRING_PREFIX
, STRING_PREFIX
},
652 {cvc5::Kind::STRING_SUFFIX
, STRING_SUFFIX
},
653 {cvc5::Kind::STRING_IS_DIGIT
, STRING_IS_DIGIT
},
654 {cvc5::Kind::STRING_ITOS
, STRING_FROM_INT
},
655 {cvc5::Kind::STRING_STOI
, STRING_TO_INT
},
656 {cvc5::Kind::CONST_STRING
, CONST_STRING
},
657 {cvc5::Kind::STRING_TO_REGEXP
, STRING_TO_REGEXP
},
658 {cvc5::Kind::REGEXP_CONCAT
, REGEXP_CONCAT
},
659 {cvc5::Kind::REGEXP_UNION
, REGEXP_UNION
},
660 {cvc5::Kind::REGEXP_INTER
, REGEXP_INTER
},
661 {cvc5::Kind::REGEXP_DIFF
, REGEXP_DIFF
},
662 {cvc5::Kind::REGEXP_STAR
, REGEXP_STAR
},
663 {cvc5::Kind::REGEXP_PLUS
, REGEXP_PLUS
},
664 {cvc5::Kind::REGEXP_OPT
, REGEXP_OPT
},
665 {cvc5::Kind::REGEXP_RANGE
, REGEXP_RANGE
},
666 {cvc5::Kind::REGEXP_REPEAT
, REGEXP_REPEAT
},
667 {cvc5::Kind::REGEXP_REPEAT_OP
, REGEXP_REPEAT
},
668 {cvc5::Kind::REGEXP_LOOP
, REGEXP_LOOP
},
669 {cvc5::Kind::REGEXP_LOOP_OP
, REGEXP_LOOP
},
670 {cvc5::Kind::REGEXP_NONE
, REGEXP_NONE
},
671 {cvc5::Kind::REGEXP_ALLCHAR
, REGEXP_ALLCHAR
},
672 {cvc5::Kind::REGEXP_COMPLEMENT
, REGEXP_COMPLEMENT
},
673 {cvc5::Kind::CONST_SEQUENCE
, CONST_SEQUENCE
},
674 {cvc5::Kind::SEQ_UNIT
, SEQ_UNIT
},
675 {cvc5::Kind::SEQ_NTH
, SEQ_NTH
},
676 /* Quantifiers ----------------------------------------------------- */
677 {cvc5::Kind::FORALL
, FORALL
},
678 {cvc5::Kind::EXISTS
, EXISTS
},
679 {cvc5::Kind::BOUND_VAR_LIST
, VARIABLE_LIST
},
680 {cvc5::Kind::INST_PATTERN
, INST_PATTERN
},
681 {cvc5::Kind::INST_NO_PATTERN
, INST_NO_PATTERN
},
682 {cvc5::Kind::INST_POOL
, INST_POOL
},
683 {cvc5::Kind::INST_ADD_TO_POOL
, INST_ADD_TO_POOL
},
684 {cvc5::Kind::SKOLEM_ADD_TO_POOL
, SKOLEM_ADD_TO_POOL
},
685 {cvc5::Kind::INST_ATTRIBUTE
, INST_ATTRIBUTE
},
686 {cvc5::Kind::INST_PATTERN_LIST
, INST_PATTERN_LIST
},
687 /* ----------------------------------------------------------------- */
688 {cvc5::Kind::LAST_KIND
, LAST_KIND
},
691 /* Set of kinds for indexed operators */
692 const static std::unordered_set
<Kind
> s_indexed_kinds(
696 BITVECTOR_ZERO_EXTEND
,
697 BITVECTOR_SIGN_EXTEND
,
698 BITVECTOR_ROTATE_LEFT
,
699 BITVECTOR_ROTATE_RIGHT
,
701 FLOATINGPOINT_TO_UBV
,
702 FLOATINGPOINT_TO_SBV
,
704 FLOATINGPOINT_TO_FP_IEEE_BITVECTOR
,
705 FLOATINGPOINT_TO_FP_FLOATINGPOINT
,
706 FLOATINGPOINT_TO_FP_REAL
,
707 FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR
,
708 FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR
,
709 FLOATINGPOINT_TO_FP_GENERIC
});
713 /** Convert a cvc5::Kind (internal) to a cvc5::api::Kind (external). */
714 cvc5::api::Kind
intToExtKind(cvc5::Kind k
)
716 auto it
= api::s_kinds_internal
.find(k
);
717 if (it
== api::s_kinds_internal
.end())
719 return api::INTERNAL_KIND
;
724 /** Convert a cvc5::api::Kind (external) to a cvc5::Kind (internal). */
725 cvc5::Kind
extToIntKind(cvc5::api::Kind k
)
727 auto it
= api::s_kinds
.find(k
);
728 if (it
== api::s_kinds
.end())
730 return cvc5::Kind::UNDEFINED_KIND
;
735 /** Return true if given kind is a defined external kind. */
736 bool isDefinedKind(Kind k
) { return k
> UNDEFINED_KIND
&& k
< LAST_KIND
; }
739 * Return true if the internal kind is one where the API term structure
740 * differs from internal structure. This happens for APPLY_* kinds.
741 * The API takes a "higher-order" perspective and treats functions as well
742 * as datatype constructors/selectors/testers as terms
743 * but interally they are not
745 bool isApplyKind(cvc5::Kind k
)
747 return (k
== cvc5::Kind::APPLY_UF
|| k
== cvc5::Kind::APPLY_CONSTRUCTOR
748 || k
== cvc5::Kind::APPLY_SELECTOR
|| k
== cvc5::Kind::APPLY_TESTER
749 || k
== cvc5::Kind::APPLY_UPDATER
);
752 #ifdef CVC5_ASSERTIONS
753 /** Return true if given kind is a defined internal kind. */
754 bool isDefinedIntKind(cvc5::Kind k
)
756 return k
!= cvc5::Kind::UNDEFINED_KIND
&& k
!= cvc5::Kind::LAST_KIND
;
760 /** Return the minimum arity of given kind. */
761 uint32_t minArity(Kind k
)
763 Assert(isDefinedKind(k
));
764 Assert(isDefinedIntKind(extToIntKind(k
)));
765 uint32_t min
= cvc5::kind::metakind::getMinArityForKind(extToIntKind(k
));
767 // At the API level, we treat functions/constructors/selectors/testers as
768 // normal terms instead of making them part of the operator
769 if (isApplyKind(extToIntKind(k
)))
776 /** Return the maximum arity of given kind. */
777 uint32_t maxArity(Kind k
)
779 Assert(isDefinedKind(k
));
780 Assert(isDefinedIntKind(extToIntKind(k
)));
781 uint32_t max
= cvc5::kind::metakind::getMaxArityForKind(extToIntKind(k
));
783 // At the API level, we treat functions/constructors/selectors/testers as
784 // normal terms instead of making them part of the operator
785 if (isApplyKind(extToIntKind(k
))
786 && max
!= std::numeric_limits
<uint32_t>::max()) // be careful not to
796 std::string
kindToString(Kind k
)
798 return k
== INTERNAL_KIND
? "INTERNAL_KIND"
799 : cvc5::kind::kindToString(extToIntKind(k
));
802 const char* toString(Kind k
)
804 return k
== INTERNAL_KIND
? "INTERNAL_KIND"
805 : cvc5::kind::toString(extToIntKind(k
));
808 std::ostream
& operator<<(std::ostream
& out
, Kind k
)
812 case INTERNAL_KIND
: out
<< "INTERNAL_KIND"; break;
813 default: out
<< extToIntKind(k
);
818 /* -------------------------------------------------------------------------- */
819 /* API guard helpers */
820 /* -------------------------------------------------------------------------- */
824 class CVC5ApiExceptionStream
827 CVC5ApiExceptionStream() {}
828 /* Note: This needs to be explicitly set to 'noexcept(false)' since it is
829 * a destructor that throws an exception and in C++11 all destructors
830 * default to noexcept(true) (else this triggers a call to std::terminate). */
831 ~CVC5ApiExceptionStream() noexcept(false)
833 if (std::uncaught_exceptions() == 0)
835 throw CVC5ApiException(d_stream
.str());
839 std::ostream
& ostream() { return d_stream
; }
842 std::stringstream d_stream
;
845 class CVC5ApiRecoverableExceptionStream
848 CVC5ApiRecoverableExceptionStream() {}
849 /* Note: This needs to be explicitly set to 'noexcept(false)' since it is
850 * a destructor that throws an exception and in C++11 all destructors
851 * default to noexcept(true) (else this triggers a call to std::terminate). */
852 ~CVC5ApiRecoverableExceptionStream() noexcept(false)
854 if (std::uncaught_exceptions() == 0)
856 throw CVC5ApiRecoverableException(d_stream
.str());
860 std::ostream
& ostream() { return d_stream
; }
863 std::stringstream d_stream
;
866 class CVC5ApiUnsupportedExceptionStream
869 CVC5ApiUnsupportedExceptionStream() {}
870 /* Note: This needs to be explicitly set to 'noexcept(false)' since it is
871 * a destructor that throws an exception and in C++11 all destructors
872 * default to noexcept(true) (else this triggers a call to std::terminate). */
873 ~CVC5ApiUnsupportedExceptionStream() noexcept(false)
875 if (std::uncaught_exceptions() == 0)
877 throw CVC5ApiUnsupportedException(d_stream
.str());
881 std::ostream
& ostream() { return d_stream
; }
884 std::stringstream d_stream
;
887 #define CVC5_API_TRY_CATCH_BEGIN \
890 #define CVC5_API_TRY_CATCH_END \
892 catch (const OptionException& e) \
894 throw CVC5ApiOptionException(e.getMessage()); \
896 catch (const cvc5::RecoverableModalException& e) \
898 throw CVC5ApiRecoverableException(e.getMessage()); \
900 catch (const cvc5::Exception& e) { throw CVC5ApiException(e.getMessage()); } \
901 catch (const std::invalid_argument& e) { throw CVC5ApiException(e.what()); }
905 /* -------------------------------------------------------------------------- */
907 /* -------------------------------------------------------------------------- */
909 Result::Result(const cvc5::Result
& r
) : d_result(new cvc5::Result(r
)) {}
911 Result::Result() : d_result(new cvc5::Result()) {}
913 bool Result::isNull() const
915 return d_result
->getType() == cvc5::Result::TYPE_NONE
;
918 bool Result::isSat(void) const
920 return d_result
->getType() == cvc5::Result::TYPE_SAT
921 && d_result
->isSat() == cvc5::Result::SAT
;
924 bool Result::isUnsat(void) const
926 return d_result
->getType() == cvc5::Result::TYPE_SAT
927 && d_result
->isSat() == cvc5::Result::UNSAT
;
930 bool Result::isSatUnknown(void) const
932 return d_result
->getType() == cvc5::Result::TYPE_SAT
933 && d_result
->isSat() == cvc5::Result::SAT_UNKNOWN
;
936 bool Result::isEntailed(void) const
938 return d_result
->getType() == cvc5::Result::TYPE_ENTAILMENT
939 && d_result
->isEntailed() == cvc5::Result::ENTAILED
;
942 bool Result::isNotEntailed(void) const
944 return d_result
->getType() == cvc5::Result::TYPE_ENTAILMENT
945 && d_result
->isEntailed() == cvc5::Result::NOT_ENTAILED
;
948 bool Result::isEntailmentUnknown(void) const
950 return d_result
->getType() == cvc5::Result::TYPE_ENTAILMENT
951 && d_result
->isEntailed() == cvc5::Result::ENTAILMENT_UNKNOWN
;
954 bool Result::operator==(const Result
& r
) const
956 return *d_result
== *r
.d_result
;
959 bool Result::operator!=(const Result
& r
) const
961 return *d_result
!= *r
.d_result
;
964 Result::UnknownExplanation
Result::getUnknownExplanation(void) const
966 cvc5::Result::UnknownExplanation expl
= d_result
->whyUnknown();
969 case cvc5::Result::REQUIRES_FULL_CHECK
: return REQUIRES_FULL_CHECK
;
970 case cvc5::Result::INCOMPLETE
: return INCOMPLETE
;
971 case cvc5::Result::TIMEOUT
: return TIMEOUT
;
972 case cvc5::Result::RESOURCEOUT
: return RESOURCEOUT
;
973 case cvc5::Result::MEMOUT
: return MEMOUT
;
974 case cvc5::Result::INTERRUPTED
: return INTERRUPTED
;
975 case cvc5::Result::NO_STATUS
: return NO_STATUS
;
976 case cvc5::Result::UNSUPPORTED
: return UNSUPPORTED
;
977 case cvc5::Result::OTHER
: return OTHER
;
978 default: return UNKNOWN_REASON
;
980 return UNKNOWN_REASON
;
983 std::string
Result::toString(void) const { return d_result
->toString(); }
985 std::ostream
& operator<<(std::ostream
& out
, const Result
& r
)
991 std::ostream
& operator<<(std::ostream
& out
, enum Result::UnknownExplanation e
)
995 case Result::REQUIRES_FULL_CHECK
: out
<< "REQUIRES_FULL_CHECK"; break;
996 case Result::INCOMPLETE
: out
<< "INCOMPLETE"; break;
997 case Result::TIMEOUT
: out
<< "TIMEOUT"; break;
998 case Result::RESOURCEOUT
: out
<< "RESOURCEOUT"; break;
999 case Result::MEMOUT
: out
<< "MEMOUT"; break;
1000 case Result::INTERRUPTED
: out
<< "INTERRUPTED"; break;
1001 case Result::NO_STATUS
: out
<< "NO_STATUS"; break;
1002 case Result::UNSUPPORTED
: out
<< "UNSUPPORTED"; break;
1003 case Result::OTHER
: out
<< "OTHER"; break;
1004 case Result::UNKNOWN_REASON
: out
<< "UNKNOWN_REASON"; break;
1005 default: Unhandled() << e
;
1010 /* -------------------------------------------------------------------------- */
1012 /* -------------------------------------------------------------------------- */
1014 Sort::Sort(const Solver
* slv
, const cvc5::TypeNode
& t
)
1015 : d_solver(slv
), d_type(new cvc5::TypeNode(t
))
1019 Sort::Sort() : d_solver(nullptr), d_type(new cvc5::TypeNode()) {}
1023 if (d_solver
!= nullptr)
1029 std::set
<TypeNode
> Sort::sortSetToTypeNodes(const std::set
<Sort
>& sorts
)
1031 std::set
<TypeNode
> types
;
1032 for (const Sort
& s
: sorts
)
1034 types
.insert(s
.getTypeNode());
1039 std::vector
<TypeNode
> Sort::sortVectorToTypeNodes(
1040 const std::vector
<Sort
>& sorts
)
1042 std::vector
<TypeNode
> typeNodes
;
1043 for (const Sort
& sort
: sorts
)
1045 typeNodes
.push_back(sort
.getTypeNode());
1050 std::vector
<Sort
> Sort::typeNodeVectorToSorts(
1051 const Solver
* slv
, const std::vector
<TypeNode
>& types
)
1053 std::vector
<Sort
> sorts
;
1054 for (size_t i
= 0, tsize
= types
.size(); i
< tsize
; i
++)
1056 sorts
.push_back(Sort(slv
, types
[i
]));
1061 bool Sort::operator==(const Sort
& s
) const
1063 CVC5_API_TRY_CATCH_BEGIN
;
1064 //////// all checks before this line
1065 return *d_type
== *s
.d_type
;
1067 CVC5_API_TRY_CATCH_END
;
1070 bool Sort::operator!=(const Sort
& s
) const
1072 CVC5_API_TRY_CATCH_BEGIN
;
1073 //////// all checks before this line
1074 return *d_type
!= *s
.d_type
;
1076 CVC5_API_TRY_CATCH_END
;
1079 bool Sort::operator<(const Sort
& s
) const
1081 CVC5_API_TRY_CATCH_BEGIN
;
1082 //////// all checks before this line
1083 return *d_type
< *s
.d_type
;
1085 CVC5_API_TRY_CATCH_END
;
1088 bool Sort::operator>(const Sort
& s
) const
1090 CVC5_API_TRY_CATCH_BEGIN
;
1091 //////// all checks before this line
1092 return *d_type
> *s
.d_type
;
1094 CVC5_API_TRY_CATCH_END
;
1097 bool Sort::operator<=(const Sort
& s
) const
1099 CVC5_API_TRY_CATCH_BEGIN
;
1100 //////// all checks before this line
1101 return *d_type
<= *s
.d_type
;
1103 CVC5_API_TRY_CATCH_END
;
1106 bool Sort::operator>=(const Sort
& s
) const
1108 CVC5_API_TRY_CATCH_BEGIN
;
1109 //////// all checks before this line
1110 return *d_type
>= *s
.d_type
;
1112 CVC5_API_TRY_CATCH_END
;
1115 bool Sort::hasSymbol() const
1117 CVC5_API_TRY_CATCH_BEGIN
;
1118 CVC5_API_CHECK_NOT_NULL
;
1119 //////// all checks before this line
1120 return d_type
->hasAttribute(expr::VarNameAttr());
1122 CVC5_API_TRY_CATCH_END
;
1125 std::string
Sort::getSymbol() const
1127 CVC5_API_TRY_CATCH_BEGIN
;
1128 CVC5_API_CHECK_NOT_NULL
;
1129 CVC5_API_CHECK(d_type
->hasAttribute(expr::VarNameAttr()))
1130 << "Invalid call to '" << __PRETTY_FUNCTION__
1131 << "', expected the sort to have a symbol.";
1132 //////// all checks before this line
1133 return d_type
->getAttribute(expr::VarNameAttr());
1135 CVC5_API_TRY_CATCH_END
;
1138 bool Sort::isNull() const
1140 CVC5_API_TRY_CATCH_BEGIN
;
1141 //////// all checks before this line
1142 return isNullHelper();
1144 CVC5_API_TRY_CATCH_END
;
1147 bool Sort::isBoolean() const
1149 CVC5_API_TRY_CATCH_BEGIN
;
1150 //////// all checks before this line
1151 return d_type
->isBoolean();
1153 CVC5_API_TRY_CATCH_END
;
1156 bool Sort::isInteger() const
1158 CVC5_API_TRY_CATCH_BEGIN
;
1159 //////// all checks before this line
1160 return d_type
->isInteger();
1162 CVC5_API_TRY_CATCH_END
;
1165 bool Sort::isReal() const
1167 CVC5_API_TRY_CATCH_BEGIN
;
1168 //////// all checks before this line
1169 // notice that we do not expose internal subtyping to the user
1170 return d_type
->isReal() && !d_type
->isInteger();
1172 CVC5_API_TRY_CATCH_END
;
1175 bool Sort::isString() const
1177 CVC5_API_TRY_CATCH_BEGIN
;
1178 //////// all checks before this line
1179 return d_type
->isString();
1181 CVC5_API_TRY_CATCH_END
;
1184 bool Sort::isRegExp() const
1186 CVC5_API_TRY_CATCH_BEGIN
;
1187 //////// all checks before this line
1188 return d_type
->isRegExp();
1190 CVC5_API_TRY_CATCH_END
;
1193 bool Sort::isRoundingMode() const
1195 CVC5_API_TRY_CATCH_BEGIN
;
1196 //////// all checks before this line
1197 return d_type
->isRoundingMode();
1199 CVC5_API_TRY_CATCH_END
;
1202 bool Sort::isBitVector() const
1204 CVC5_API_TRY_CATCH_BEGIN
;
1205 //////// all checks before this line
1206 return d_type
->isBitVector();
1208 CVC5_API_TRY_CATCH_END
;
1211 bool Sort::isFloatingPoint() const
1213 CVC5_API_TRY_CATCH_BEGIN
;
1214 //////// all checks before this line
1215 return d_type
->isFloatingPoint();
1217 CVC5_API_TRY_CATCH_END
;
1220 bool Sort::isDatatype() const
1222 CVC5_API_TRY_CATCH_BEGIN
;
1223 //////// all checks before this line
1224 return d_type
->isDatatype();
1226 CVC5_API_TRY_CATCH_END
;
1229 bool Sort::isParametricDatatype() const
1231 CVC5_API_TRY_CATCH_BEGIN
;
1232 //////// all checks before this line
1233 if (!d_type
->isDatatype()) return false;
1234 return d_type
->isParametricDatatype();
1236 CVC5_API_TRY_CATCH_END
;
1239 bool Sort::isConstructor() const
1241 CVC5_API_TRY_CATCH_BEGIN
;
1242 //////// all checks before this line
1243 return d_type
->isConstructor();
1245 CVC5_API_TRY_CATCH_END
;
1248 bool Sort::isSelector() const
1250 CVC5_API_TRY_CATCH_BEGIN
;
1251 //////// all checks before this line
1252 return d_type
->isSelector();
1254 CVC5_API_TRY_CATCH_END
;
1257 bool Sort::isTester() const
1259 CVC5_API_TRY_CATCH_BEGIN
;
1260 //////// all checks before this line
1261 return d_type
->isTester();
1263 CVC5_API_TRY_CATCH_END
;
1266 bool Sort::isUpdater() const
1268 CVC5_API_TRY_CATCH_BEGIN
;
1269 //////// all checks before this line
1270 return d_type
->isUpdater();
1272 CVC5_API_TRY_CATCH_END
;
1275 bool Sort::isFunction() const
1277 CVC5_API_TRY_CATCH_BEGIN
;
1278 //////// all checks before this line
1279 return d_type
->isFunction();
1281 CVC5_API_TRY_CATCH_END
;
1284 bool Sort::isPredicate() const
1286 CVC5_API_TRY_CATCH_BEGIN
;
1287 //////// all checks before this line
1288 return d_type
->isPredicate();
1290 CVC5_API_TRY_CATCH_END
;
1293 bool Sort::isTuple() const
1295 CVC5_API_TRY_CATCH_BEGIN
;
1296 //////// all checks before this line
1297 return d_type
->isTuple();
1299 CVC5_API_TRY_CATCH_END
;
1302 bool Sort::isRecord() const
1304 CVC5_API_TRY_CATCH_BEGIN
;
1305 //////// all checks before this line
1306 return d_type
->isRecord();
1308 CVC5_API_TRY_CATCH_END
;
1311 bool Sort::isArray() const
1313 CVC5_API_TRY_CATCH_BEGIN
;
1314 //////// all checks before this line
1315 return d_type
->isArray();
1317 CVC5_API_TRY_CATCH_END
;
1320 bool Sort::isSet() const
1322 CVC5_API_TRY_CATCH_BEGIN
;
1323 //////// all checks before this line
1324 return d_type
->isSet();
1326 CVC5_API_TRY_CATCH_END
;
1329 bool Sort::isBag() const
1331 CVC5_API_TRY_CATCH_BEGIN
;
1332 //////// all checks before this line
1333 return d_type
->isBag();
1335 CVC5_API_TRY_CATCH_END
;
1338 bool Sort::isSequence() const
1340 CVC5_API_TRY_CATCH_BEGIN
;
1341 //////// all checks before this line
1342 return d_type
->isSequence();
1344 CVC5_API_TRY_CATCH_END
;
1347 bool Sort::isUninterpretedSort() const
1349 CVC5_API_TRY_CATCH_BEGIN
;
1350 //////// all checks before this line
1351 return d_type
->isSort();
1353 CVC5_API_TRY_CATCH_END
;
1356 bool Sort::isSortConstructor() const
1358 CVC5_API_TRY_CATCH_BEGIN
;
1359 //////// all checks before this line
1360 return d_type
->isSortConstructor();
1362 CVC5_API_TRY_CATCH_END
;
1365 bool Sort::isFirstClass() const
1367 CVC5_API_TRY_CATCH_BEGIN
;
1368 //////// all checks before this line
1369 return d_type
->isFirstClass();
1371 CVC5_API_TRY_CATCH_END
;
1374 bool Sort::isFunctionLike() const
1376 CVC5_API_TRY_CATCH_BEGIN
;
1377 //////// all checks before this line
1378 return d_type
->isFunctionLike();
1380 CVC5_API_TRY_CATCH_END
;
1383 bool Sort::isSubsortOf(const Sort
& s
) const
1385 CVC5_API_TRY_CATCH_BEGIN
;
1386 CVC5_API_ARG_CHECK_SOLVER("sort", s
);
1387 //////// all checks before this line
1388 return d_type
->isSubtypeOf(*s
.d_type
);
1390 CVC5_API_TRY_CATCH_END
;
1393 Datatype
Sort::getDatatype() const
1395 CVC5_API_TRY_CATCH_BEGIN
;
1396 CVC5_API_CHECK_NOT_NULL
;
1397 CVC5_API_CHECK(isDatatype()) << "Expected datatype sort.";
1398 //////// all checks before this line
1399 return Datatype(d_solver
, d_type
->getDType());
1401 CVC5_API_TRY_CATCH_END
;
1404 Sort
Sort::instantiate(const std::vector
<Sort
>& params
) const
1406 CVC5_API_TRY_CATCH_BEGIN
;
1407 CVC5_API_CHECK_NOT_NULL
;
1408 CVC5_API_CHECK_SORTS(params
);
1409 CVC5_API_CHECK(isParametricDatatype() || isSortConstructor())
1410 << "Expected parametric datatype or sort constructor sort.";
1411 CVC5_API_CHECK(isSortConstructor()
1412 || d_type
->getNumChildren() == params
.size() + 1)
1413 << "Arity mismatch for instantiated parametric datatype";
1414 //////// all checks before this line
1415 std::vector
<cvc5::TypeNode
> tparams
= sortVectorToTypeNodes(params
);
1416 if (d_type
->isDatatype())
1418 return Sort(d_solver
, d_type
->instantiateParametricDatatype(tparams
));
1420 Assert(d_type
->isSortConstructor());
1421 return Sort(d_solver
, d_solver
->getNodeManager()->mkSort(*d_type
, tparams
));
1423 CVC5_API_TRY_CATCH_END
;
1426 Sort
Sort::substitute(const Sort
& sort
, const Sort
& replacement
) const
1428 CVC5_API_TRY_CATCH_BEGIN
;
1429 CVC5_API_CHECK_NOT_NULL
;
1430 CVC5_API_CHECK_SORT(sort
);
1431 CVC5_API_CHECK_SORT(replacement
);
1432 //////// all checks before this line
1435 d_type
->substitute(sort
.getTypeNode(), replacement
.getTypeNode()));
1437 CVC5_API_TRY_CATCH_END
;
1440 Sort
Sort::substitute(const std::vector
<Sort
>& sorts
,
1441 const std::vector
<Sort
>& replacements
) const
1443 CVC5_API_TRY_CATCH_BEGIN
;
1444 CVC5_API_CHECK_NOT_NULL
;
1445 CVC5_API_CHECK_SORTS(sorts
);
1446 CVC5_API_CHECK_SORTS(replacements
);
1447 //////// all checks before this line
1449 std::vector
<cvc5::TypeNode
> tSorts
= sortVectorToTypeNodes(sorts
),
1451 sortVectorToTypeNodes(replacements
);
1452 return Sort(d_solver
,
1453 d_type
->substitute(tSorts
.begin(),
1455 tReplacements
.begin(),
1456 tReplacements
.end()));
1458 CVC5_API_TRY_CATCH_END
;
1461 std::string
Sort::toString() const
1463 CVC5_API_TRY_CATCH_BEGIN
;
1464 //////// all checks before this line
1465 return d_type
->toString();
1467 CVC5_API_TRY_CATCH_END
;
1470 const cvc5::TypeNode
& Sort::getTypeNode(void) const { return *d_type
; }
1472 /* Constructor sort ------------------------------------------------------- */
1474 size_t Sort::getConstructorArity() const
1476 CVC5_API_TRY_CATCH_BEGIN
;
1477 CVC5_API_CHECK_NOT_NULL
;
1478 CVC5_API_CHECK(isConstructor()) << "Not a constructor sort: " << (*this);
1479 //////// all checks before this line
1480 return d_type
->getNumChildren() - 1;
1482 CVC5_API_TRY_CATCH_END
;
1485 std::vector
<Sort
> Sort::getConstructorDomainSorts() const
1487 CVC5_API_TRY_CATCH_BEGIN
;
1488 CVC5_API_CHECK_NOT_NULL
;
1489 CVC5_API_CHECK(isConstructor()) << "Not a constructor sort: " << (*this);
1490 //////// all checks before this line
1491 return typeNodeVectorToSorts(d_solver
, d_type
->getArgTypes());
1493 CVC5_API_TRY_CATCH_END
;
1496 Sort
Sort::getConstructorCodomainSort() const
1498 CVC5_API_TRY_CATCH_BEGIN
;
1499 CVC5_API_CHECK_NOT_NULL
;
1500 CVC5_API_CHECK(isConstructor()) << "Not a constructor sort: " << (*this);
1501 //////// all checks before this line
1502 return Sort(d_solver
, d_type
->getConstructorRangeType());
1504 CVC5_API_TRY_CATCH_END
;
1507 /* Selector sort ------------------------------------------------------- */
1509 Sort
Sort::getSelectorDomainSort() const
1511 CVC5_API_TRY_CATCH_BEGIN
;
1512 CVC5_API_CHECK_NOT_NULL
;
1513 CVC5_API_CHECK(isSelector()) << "Not a selector sort: " << (*this);
1514 //////// all checks before this line
1515 return Sort(d_solver
, d_type
->getSelectorDomainType());
1517 CVC5_API_TRY_CATCH_END
;
1520 Sort
Sort::getSelectorCodomainSort() const
1522 CVC5_API_TRY_CATCH_BEGIN
;
1523 CVC5_API_CHECK_NOT_NULL
;
1524 CVC5_API_CHECK(isSelector()) << "Not a selector sort: " << (*this);
1525 //////// all checks before this line
1526 return Sort(d_solver
, d_type
->getSelectorRangeType());
1528 CVC5_API_TRY_CATCH_END
;
1531 /* Tester sort ------------------------------------------------------- */
1533 Sort
Sort::getTesterDomainSort() const
1535 CVC5_API_TRY_CATCH_BEGIN
;
1536 CVC5_API_CHECK_NOT_NULL
;
1537 CVC5_API_CHECK(isTester()) << "Not a tester sort: " << (*this);
1538 //////// all checks before this line
1539 return Sort(d_solver
, d_type
->getTesterDomainType());
1541 CVC5_API_TRY_CATCH_END
;
1544 Sort
Sort::getTesterCodomainSort() const
1546 CVC5_API_TRY_CATCH_BEGIN
;
1547 CVC5_API_CHECK_NOT_NULL
;
1548 CVC5_API_CHECK(isTester()) << "Not a tester sort: " << (*this);
1549 //////// all checks before this line
1550 return d_solver
->getBooleanSort();
1552 CVC5_API_TRY_CATCH_END
;
1555 /* Function sort ------------------------------------------------------- */
1557 size_t Sort::getFunctionArity() const
1559 CVC5_API_TRY_CATCH_BEGIN
;
1560 CVC5_API_CHECK_NOT_NULL
;
1561 CVC5_API_CHECK(isFunction()) << "Not a function sort: " << (*this);
1562 //////// all checks before this line
1563 return d_type
->getNumChildren() - 1;
1565 CVC5_API_TRY_CATCH_END
;
1568 std::vector
<Sort
> Sort::getFunctionDomainSorts() const
1570 CVC5_API_TRY_CATCH_BEGIN
;
1571 CVC5_API_CHECK_NOT_NULL
;
1572 CVC5_API_CHECK(isFunction()) << "Not a function sort: " << (*this);
1573 //////// all checks before this line
1574 return typeNodeVectorToSorts(d_solver
, d_type
->getArgTypes());
1576 CVC5_API_TRY_CATCH_END
;
1579 Sort
Sort::getFunctionCodomainSort() const
1581 CVC5_API_TRY_CATCH_BEGIN
;
1582 CVC5_API_CHECK_NOT_NULL
;
1583 CVC5_API_CHECK(isFunction()) << "Not a function sort" << (*this);
1584 //////// all checks before this line
1585 return Sort(d_solver
, d_type
->getRangeType());
1587 CVC5_API_TRY_CATCH_END
;
1590 /* Array sort ---------------------------------------------------------- */
1592 Sort
Sort::getArrayIndexSort() const
1594 CVC5_API_TRY_CATCH_BEGIN
;
1595 CVC5_API_CHECK_NOT_NULL
;
1596 CVC5_API_CHECK(isArray()) << "Not an array sort.";
1597 //////// all checks before this line
1598 return Sort(d_solver
, d_type
->getArrayIndexType());
1600 CVC5_API_TRY_CATCH_END
;
1603 Sort
Sort::getArrayElementSort() const
1605 CVC5_API_TRY_CATCH_BEGIN
;
1606 CVC5_API_CHECK_NOT_NULL
;
1607 CVC5_API_CHECK(isArray()) << "Not an array sort.";
1608 //////// all checks before this line
1609 return Sort(d_solver
, d_type
->getArrayConstituentType());
1611 CVC5_API_TRY_CATCH_END
;
1614 /* Set sort ------------------------------------------------------------ */
1616 Sort
Sort::getSetElementSort() const
1618 CVC5_API_TRY_CATCH_BEGIN
;
1619 CVC5_API_CHECK_NOT_NULL
;
1620 CVC5_API_CHECK(isSet()) << "Not a set sort.";
1621 //////// all checks before this line
1622 return Sort(d_solver
, d_type
->getSetElementType());
1624 CVC5_API_TRY_CATCH_END
;
1627 /* Bag sort ------------------------------------------------------------ */
1629 Sort
Sort::getBagElementSort() const
1631 CVC5_API_TRY_CATCH_BEGIN
;
1632 CVC5_API_CHECK_NOT_NULL
;
1633 CVC5_API_CHECK(isBag()) << "Not a bag sort.";
1634 //////// all checks before this line
1635 return Sort(d_solver
, d_type
->getBagElementType());
1637 CVC5_API_TRY_CATCH_END
;
1640 /* Sequence sort ------------------------------------------------------- */
1642 Sort
Sort::getSequenceElementSort() const
1644 CVC5_API_TRY_CATCH_BEGIN
;
1645 CVC5_API_CHECK_NOT_NULL
;
1646 CVC5_API_CHECK(isSequence()) << "Not a sequence sort.";
1647 //////// all checks before this line
1648 return Sort(d_solver
, d_type
->getSequenceElementType());
1650 CVC5_API_TRY_CATCH_END
;
1653 /* Uninterpreted sort -------------------------------------------------- */
1655 std::string
Sort::getUninterpretedSortName() const
1657 CVC5_API_TRY_CATCH_BEGIN
;
1658 CVC5_API_CHECK_NOT_NULL
;
1659 CVC5_API_CHECK(isUninterpretedSort()) << "Not an uninterpreted sort.";
1660 //////// all checks before this line
1661 return d_type
->getName();
1663 CVC5_API_TRY_CATCH_END
;
1666 bool Sort::isUninterpretedSortParameterized() const
1668 CVC5_API_TRY_CATCH_BEGIN
;
1669 CVC5_API_CHECK_NOT_NULL
;
1670 CVC5_API_CHECK(isUninterpretedSort()) << "Not an uninterpreted sort.";
1671 //////// all checks before this line
1673 /* This method is not implemented in the NodeManager, since whether a
1674 * uninterpreted sort is parameterized is irrelevant for solving. */
1675 return d_type
->getNumChildren() > 0;
1677 CVC5_API_TRY_CATCH_END
;
1680 std::vector
<Sort
> Sort::getUninterpretedSortParamSorts() const
1682 CVC5_API_TRY_CATCH_BEGIN
;
1683 CVC5_API_CHECK_NOT_NULL
;
1684 CVC5_API_CHECK(isUninterpretedSort()) << "Not an uninterpreted sort.";
1685 //////// all checks before this line
1687 /* This method is not implemented in the NodeManager, since whether a
1688 * uninterpreted sort is parameterized is irrelevant for solving. */
1689 std::vector
<TypeNode
> params
;
1690 for (size_t i
= 0, nchildren
= d_type
->getNumChildren(); i
< nchildren
; i
++)
1692 params
.push_back((*d_type
)[i
]);
1694 return typeNodeVectorToSorts(d_solver
, params
);
1696 CVC5_API_TRY_CATCH_END
;
1699 /* Sort constructor sort ----------------------------------------------- */
1701 std::string
Sort::getSortConstructorName() const
1703 CVC5_API_TRY_CATCH_BEGIN
;
1704 CVC5_API_CHECK_NOT_NULL
;
1705 CVC5_API_CHECK(isSortConstructor()) << "Not a sort constructor sort.";
1706 //////// all checks before this line
1707 return d_type
->getName();
1709 CVC5_API_TRY_CATCH_END
;
1712 size_t Sort::getSortConstructorArity() const
1714 CVC5_API_TRY_CATCH_BEGIN
;
1715 CVC5_API_CHECK_NOT_NULL
;
1716 CVC5_API_CHECK(isSortConstructor()) << "Not a sort constructor sort.";
1717 //////// all checks before this line
1718 return d_type
->getSortConstructorArity();
1720 CVC5_API_TRY_CATCH_END
;
1723 /* Bit-vector sort ----------------------------------------------------- */
1725 uint32_t Sort::getBitVectorSize() const
1727 CVC5_API_TRY_CATCH_BEGIN
;
1728 CVC5_API_CHECK_NOT_NULL
;
1729 CVC5_API_CHECK(isBitVector()) << "Not a bit-vector sort.";
1730 //////// all checks before this line
1731 return d_type
->getBitVectorSize();
1733 CVC5_API_TRY_CATCH_END
;
1736 /* Floating-point sort ------------------------------------------------- */
1738 uint32_t Sort::getFloatingPointExponentSize() const
1740 CVC5_API_TRY_CATCH_BEGIN
;
1741 CVC5_API_CHECK_NOT_NULL
;
1742 CVC5_API_CHECK(isFloatingPoint()) << "Not a floating-point sort.";
1743 //////// all checks before this line
1744 return d_type
->getFloatingPointExponentSize();
1746 CVC5_API_TRY_CATCH_END
;
1749 uint32_t Sort::getFloatingPointSignificandSize() const
1751 CVC5_API_TRY_CATCH_BEGIN
;
1752 CVC5_API_CHECK_NOT_NULL
;
1753 CVC5_API_CHECK(isFloatingPoint()) << "Not a floating-point sort.";
1754 //////// all checks before this line
1755 return d_type
->getFloatingPointSignificandSize();
1757 CVC5_API_TRY_CATCH_END
;
1760 /* Datatype sort ------------------------------------------------------- */
1762 std::vector
<Sort
> Sort::getDatatypeParamSorts() const
1764 CVC5_API_TRY_CATCH_BEGIN
;
1765 CVC5_API_CHECK_NOT_NULL
;
1766 CVC5_API_CHECK(isParametricDatatype()) << "Not a parametric datatype sort.";
1767 //////// all checks before this line
1768 return typeNodeVectorToSorts(d_solver
, d_type
->getParamTypes());
1770 CVC5_API_TRY_CATCH_END
;
1773 size_t Sort::getDatatypeArity() const
1775 CVC5_API_TRY_CATCH_BEGIN
;
1776 CVC5_API_CHECK_NOT_NULL
;
1777 CVC5_API_CHECK(isDatatype()) << "Not a datatype sort.";
1778 //////// all checks before this line
1779 return d_type
->isParametricDatatype() ? d_type
->getNumChildren() - 1 : 0;
1781 CVC5_API_TRY_CATCH_END
;
1784 /* Tuple sort ---------------------------------------------------------- */
1786 size_t Sort::getTupleLength() const
1788 CVC5_API_TRY_CATCH_BEGIN
;
1789 CVC5_API_CHECK_NOT_NULL
;
1790 CVC5_API_CHECK(isTuple()) << "Not a tuple sort.";
1791 //////// all checks before this line
1792 return d_type
->getTupleLength();
1794 CVC5_API_TRY_CATCH_END
;
1797 std::vector
<Sort
> Sort::getTupleSorts() const
1799 CVC5_API_TRY_CATCH_BEGIN
;
1800 CVC5_API_CHECK_NOT_NULL
;
1801 CVC5_API_CHECK(isTuple()) << "Not a tuple sort.";
1802 //////// all checks before this line
1803 return typeNodeVectorToSorts(d_solver
, d_type
->getTupleTypes());
1805 CVC5_API_TRY_CATCH_END
;
1808 /* --------------------------------------------------------------------- */
1810 std::ostream
& operator<<(std::ostream
& out
, const Sort
& s
)
1812 out
<< s
.toString();
1817 /* -------------------------------------------------------------------------- */
1819 /* Split out to avoid nested API calls (problematic with API tracing). */
1820 /* .......................................................................... */
1822 bool Sort::isNullHelper() const { return d_type
->isNull(); }
1824 /* -------------------------------------------------------------------------- */
1826 /* -------------------------------------------------------------------------- */
1828 Op::Op() : d_solver(nullptr), d_kind(NULL_EXPR
), d_node(new cvc5::Node()) {}
1830 Op::Op(const Solver
* slv
, const Kind k
)
1831 : d_solver(slv
), d_kind(k
), d_node(new cvc5::Node())
1835 Op::Op(const Solver
* slv
, const Kind k
, const cvc5::Node
& n
)
1836 : d_solver(slv
), d_kind(k
), d_node(new cvc5::Node(n
))
1842 if (d_solver
!= nullptr)
1844 // Ensure that the correct node manager is in scope when the type node is
1850 /* Public methods */
1851 bool Op::operator==(const Op
& t
) const
1853 CVC5_API_TRY_CATCH_BEGIN
;
1854 //////// all checks before this line
1855 if (d_node
->isNull() && t
.d_node
->isNull())
1857 return (d_kind
== t
.d_kind
);
1859 else if (d_node
->isNull() || t
.d_node
->isNull())
1863 return (d_kind
== t
.d_kind
) && (*d_node
== *t
.d_node
);
1865 CVC5_API_TRY_CATCH_END
;
1868 bool Op::operator!=(const Op
& t
) const
1870 CVC5_API_TRY_CATCH_BEGIN
;
1871 //////// all checks before this line
1872 return !(*this == t
);
1874 CVC5_API_TRY_CATCH_END
;
1877 Kind
Op::getKind() const
1879 CVC5_API_CHECK(d_kind
!= NULL_EXPR
) << "Expecting a non-null Kind";
1880 //////// all checks before this line
1884 bool Op::isNull() const
1886 CVC5_API_TRY_CATCH_BEGIN
;
1887 //////// all checks before this line
1888 return isNullHelper();
1890 CVC5_API_TRY_CATCH_END
;
1893 bool Op::isIndexed() const
1895 CVC5_API_TRY_CATCH_BEGIN
;
1896 //////// all checks before this line
1897 return isIndexedHelper();
1899 CVC5_API_TRY_CATCH_END
;
1902 size_t Op::getNumIndices() const
1904 CVC5_API_TRY_CATCH_BEGIN
;
1905 CVC5_API_CHECK_NOT_NULL
;
1906 //////// all checks before this line
1907 return getNumIndicesHelper();
1909 CVC5_API_TRY_CATCH_END
;
1912 size_t Op::getNumIndicesHelper() const
1914 if (!isIndexedHelper())
1919 Kind k
= intToExtKind(d_node
->getKind());
1923 case DIVISIBLE
: size
= 1; break;
1924 case BITVECTOR_REPEAT
: size
= 1; break;
1925 case BITVECTOR_ZERO_EXTEND
: size
= 1; break;
1926 case BITVECTOR_SIGN_EXTEND
: size
= 1; break;
1927 case BITVECTOR_ROTATE_LEFT
: size
= 1; break;
1928 case BITVECTOR_ROTATE_RIGHT
: size
= 1; break;
1929 case INT_TO_BITVECTOR
: size
= 1; break;
1930 case IAND
: size
= 1; break;
1931 case FLOATINGPOINT_TO_UBV
: size
= 1; break;
1932 case FLOATINGPOINT_TO_SBV
: size
= 1; break;
1933 case REGEXP_REPEAT
: size
= 1; break;
1934 case BITVECTOR_EXTRACT
: size
= 2; break;
1935 case FLOATINGPOINT_TO_FP_IEEE_BITVECTOR
: size
= 2; break;
1936 case FLOATINGPOINT_TO_FP_FLOATINGPOINT
: size
= 2; break;
1937 case FLOATINGPOINT_TO_FP_REAL
: size
= 2; break;
1938 case FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR
: size
= 2; break;
1939 case FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR
: size
= 2; break;
1940 case FLOATINGPOINT_TO_FP_GENERIC
: size
= 2; break;
1941 case REGEXP_LOOP
: size
= 2; break;
1943 size
= d_node
->getConst
<TupleProjectOp
>().getIndices().size();
1945 default: CVC5_API_CHECK(false) << "Unhandled kind " << kindToString(k
);
1950 Term
Op::operator[](size_t index
) const
1952 return getIndexHelper(index
);
1955 Term
Op::getIndexHelper(size_t index
) const
1957 CVC5_API_TRY_CATCH_BEGIN
;
1958 CVC5_API_CHECK_NOT_NULL
;
1959 CVC5_API_CHECK(!d_node
->isNull())
1960 << "Expecting a non-null internal expression. This Op is not indexed.";
1961 CVC5_API_CHECK(index
< getNumIndicesHelper()) << "index out of bound";
1962 Kind k
= intToExtKind(d_node
->getKind());
1968 t
= d_solver
->mkRationalValHelper(
1969 Rational(d_node
->getConst
<Divisible
>().k
));
1972 case BITVECTOR_REPEAT
:
1974 t
= d_solver
->mkRationalValHelper(
1975 d_node
->getConst
<BitVectorRepeat
>().d_repeatAmount
);
1978 case BITVECTOR_ZERO_EXTEND
:
1980 t
= d_solver
->mkRationalValHelper(
1981 d_node
->getConst
<BitVectorZeroExtend
>().d_zeroExtendAmount
);
1984 case BITVECTOR_SIGN_EXTEND
:
1986 t
= d_solver
->mkRationalValHelper(
1987 d_node
->getConst
<BitVectorSignExtend
>().d_signExtendAmount
);
1990 case BITVECTOR_ROTATE_LEFT
:
1992 t
= d_solver
->mkRationalValHelper(
1993 d_node
->getConst
<BitVectorRotateLeft
>().d_rotateLeftAmount
);
1996 case BITVECTOR_ROTATE_RIGHT
:
1998 t
= d_solver
->mkRationalValHelper(
1999 d_node
->getConst
<BitVectorRotateRight
>().d_rotateRightAmount
);
2002 case INT_TO_BITVECTOR
:
2004 t
= d_solver
->mkRationalValHelper(
2005 d_node
->getConst
<IntToBitVector
>().d_size
);
2010 t
= d_solver
->mkRationalValHelper(d_node
->getConst
<IntAnd
>().d_size
);
2013 case FLOATINGPOINT_TO_UBV
:
2015 t
= d_solver
->mkRationalValHelper(
2016 d_node
->getConst
<FloatingPointToUBV
>().d_bv_size
.d_size
);
2019 case FLOATINGPOINT_TO_SBV
:
2021 t
= d_solver
->mkRationalValHelper(
2022 d_node
->getConst
<FloatingPointToSBV
>().d_bv_size
.d_size
);
2027 t
= d_solver
->mkRationalValHelper(
2028 d_node
->getConst
<RegExpRepeat
>().d_repeatAmount
);
2031 case BITVECTOR_EXTRACT
:
2033 cvc5::BitVectorExtract ext
= d_node
->getConst
<BitVectorExtract
>();
2034 t
= index
== 0 ? d_solver
->mkRationalValHelper(ext
.d_high
)
2035 : d_solver
->mkRationalValHelper(ext
.d_low
);
2038 case FLOATINGPOINT_TO_FP_IEEE_BITVECTOR
:
2040 cvc5::FloatingPointToFPIEEEBitVector ext
=
2041 d_node
->getConst
<FloatingPointToFPIEEEBitVector
>();
2044 ? d_solver
->mkRationalValHelper(ext
.getSize().exponentWidth())
2045 : d_solver
->mkRationalValHelper(ext
.getSize().significandWidth());
2048 case FLOATINGPOINT_TO_FP_FLOATINGPOINT
:
2050 cvc5::FloatingPointToFPFloatingPoint ext
=
2051 d_node
->getConst
<FloatingPointToFPFloatingPoint
>();
2053 ? d_solver
->mkRationalValHelper(ext
.getSize().exponentWidth())
2054 : d_solver
->mkRationalValHelper(ext
.getSize().significandWidth());
2057 case FLOATINGPOINT_TO_FP_REAL
:
2059 cvc5::FloatingPointToFPReal ext
=
2060 d_node
->getConst
<FloatingPointToFPReal
>();
2063 ? d_solver
->mkRationalValHelper(ext
.getSize().exponentWidth())
2064 : d_solver
->mkRationalValHelper(ext
.getSize().significandWidth());
2067 case FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR
:
2069 cvc5::FloatingPointToFPSignedBitVector ext
=
2070 d_node
->getConst
<FloatingPointToFPSignedBitVector
>();
2072 ? d_solver
->mkRationalValHelper(ext
.getSize().exponentWidth())
2073 : d_solver
->mkRationalValHelper(ext
.getSize().significandWidth());
2076 case FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR
:
2078 cvc5::FloatingPointToFPUnsignedBitVector ext
=
2079 d_node
->getConst
<FloatingPointToFPUnsignedBitVector
>();
2081 ? d_solver
->mkRationalValHelper(ext
.getSize().exponentWidth())
2082 : d_solver
->mkRationalValHelper(ext
.getSize().significandWidth());
2085 case FLOATINGPOINT_TO_FP_GENERIC
:
2087 cvc5::FloatingPointToFPGeneric ext
=
2088 d_node
->getConst
<FloatingPointToFPGeneric
>();
2090 ? d_solver
->mkRationalValHelper(ext
.getSize().exponentWidth())
2091 : d_solver
->mkRationalValHelper(ext
.getSize().significandWidth());
2096 cvc5::RegExpLoop ext
= d_node
->getConst
<RegExpLoop
>();
2097 t
= index
== 0 ? d_solver
->mkRationalValHelper(ext
.d_loopMinOcc
)
2098 : d_solver
->mkRationalValHelper(ext
.d_loopMaxOcc
);
2105 const std::vector
<uint32_t>& projectionIndices
=
2106 d_node
->getConst
<TupleProjectOp
>().getIndices();
2107 t
= d_solver
->mkRationalValHelper(projectionIndices
[index
]);
2112 CVC5_API_CHECK(false) << "Unhandled kind " << kindToString(k
);
2117 //////// all checks before this line
2120 CVC5_API_TRY_CATCH_END
;
2124 std::string
Op::getIndices() const
2126 CVC5_API_TRY_CATCH_BEGIN
;
2127 CVC5_API_CHECK_NOT_NULL
;
2128 CVC5_API_CHECK(!d_node
->isNull())
2129 << "Expecting a non-null internal expression. This Op is not indexed.";
2130 Kind k
= intToExtKind(d_node
->getKind());
2131 CVC5_API_CHECK(k
== DIVISIBLE
) << "Can't get string index from"
2132 << " kind " << kindToString(k
);
2133 //////// all checks before this line
2134 return d_node
->getConst
<Divisible
>().k
.toString();
2136 CVC5_API_TRY_CATCH_END
;
2140 uint32_t Op::getIndices() const
2142 CVC5_API_TRY_CATCH_BEGIN
;
2143 CVC5_API_CHECK_NOT_NULL
;
2144 CVC5_API_CHECK(!d_node
->isNull())
2145 << "Expecting a non-null internal expression. This Op is not indexed.";
2146 //////// all checks before this line
2149 Kind k
= intToExtKind(d_node
->getKind());
2152 case BITVECTOR_REPEAT
:
2153 i
= d_node
->getConst
<BitVectorRepeat
>().d_repeatAmount
;
2155 case BITVECTOR_ZERO_EXTEND
:
2156 i
= d_node
->getConst
<BitVectorZeroExtend
>().d_zeroExtendAmount
;
2158 case BITVECTOR_SIGN_EXTEND
:
2159 i
= d_node
->getConst
<BitVectorSignExtend
>().d_signExtendAmount
;
2161 case BITVECTOR_ROTATE_LEFT
:
2162 i
= d_node
->getConst
<BitVectorRotateLeft
>().d_rotateLeftAmount
;
2164 case BITVECTOR_ROTATE_RIGHT
:
2165 i
= d_node
->getConst
<BitVectorRotateRight
>().d_rotateRightAmount
;
2167 case INT_TO_BITVECTOR
: i
= d_node
->getConst
<IntToBitVector
>().d_size
; break;
2168 case IAND
: i
= d_node
->getConst
<IntAnd
>().d_size
; break;
2169 case FLOATINGPOINT_TO_UBV
:
2170 i
= d_node
->getConst
<FloatingPointToUBV
>().d_bv_size
.d_size
;
2172 case FLOATINGPOINT_TO_SBV
:
2173 i
= d_node
->getConst
<FloatingPointToSBV
>().d_bv_size
.d_size
;
2176 i
= d_node
->getConst
<RegExpRepeat
>().d_repeatAmount
;
2179 CVC5_API_CHECK(false) << "Can't get uint32_t index from"
2180 << " kind " << kindToString(k
);
2184 CVC5_API_TRY_CATCH_END
;
2188 std::pair
<uint32_t, uint32_t> Op::getIndices() const
2190 CVC5_API_TRY_CATCH_BEGIN
;
2191 CVC5_API_CHECK_NOT_NULL
;
2192 CVC5_API_CHECK(!d_node
->isNull())
2193 << "Expecting a non-null internal expression. This Op is not indexed.";
2194 //////// all checks before this line
2196 std::pair
<uint32_t, uint32_t> indices
;
2197 Kind k
= intToExtKind(d_node
->getKind());
2199 // using if/else instead of case statement because want local variables
2200 if (k
== BITVECTOR_EXTRACT
)
2202 cvc5::BitVectorExtract ext
= d_node
->getConst
<BitVectorExtract
>();
2203 indices
= std::make_pair(ext
.d_high
, ext
.d_low
);
2205 else if (k
== FLOATINGPOINT_TO_FP_IEEE_BITVECTOR
)
2207 cvc5::FloatingPointToFPIEEEBitVector ext
=
2208 d_node
->getConst
<FloatingPointToFPIEEEBitVector
>();
2209 indices
= std::make_pair(ext
.getSize().exponentWidth(),
2210 ext
.getSize().significandWidth());
2212 else if (k
== FLOATINGPOINT_TO_FP_FLOATINGPOINT
)
2214 cvc5::FloatingPointToFPFloatingPoint ext
=
2215 d_node
->getConst
<FloatingPointToFPFloatingPoint
>();
2216 indices
= std::make_pair(ext
.getSize().exponentWidth(),
2217 ext
.getSize().significandWidth());
2219 else if (k
== FLOATINGPOINT_TO_FP_REAL
)
2221 cvc5::FloatingPointToFPReal ext
= d_node
->getConst
<FloatingPointToFPReal
>();
2222 indices
= std::make_pair(ext
.getSize().exponentWidth(),
2223 ext
.getSize().significandWidth());
2225 else if (k
== FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR
)
2227 cvc5::FloatingPointToFPSignedBitVector ext
=
2228 d_node
->getConst
<FloatingPointToFPSignedBitVector
>();
2229 indices
= std::make_pair(ext
.getSize().exponentWidth(),
2230 ext
.getSize().significandWidth());
2232 else if (k
== FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR
)
2234 cvc5::FloatingPointToFPUnsignedBitVector ext
=
2235 d_node
->getConst
<FloatingPointToFPUnsignedBitVector
>();
2236 indices
= std::make_pair(ext
.getSize().exponentWidth(),
2237 ext
.getSize().significandWidth());
2239 else if (k
== FLOATINGPOINT_TO_FP_GENERIC
)
2241 cvc5::FloatingPointToFPGeneric ext
=
2242 d_node
->getConst
<FloatingPointToFPGeneric
>();
2243 indices
= std::make_pair(ext
.getSize().exponentWidth(),
2244 ext
.getSize().significandWidth());
2246 else if (k
== REGEXP_LOOP
)
2248 cvc5::RegExpLoop ext
= d_node
->getConst
<RegExpLoop
>();
2249 indices
= std::make_pair(ext
.d_loopMinOcc
, ext
.d_loopMaxOcc
);
2253 CVC5_API_CHECK(false) << "Can't get pair<uint32_t, uint32_t> indices from"
2254 << " kind " << kindToString(k
);
2258 CVC5_API_TRY_CATCH_END
;
2262 std::vector
<api::Term
> Op::getIndices() const
2264 CVC5_API_TRY_CATCH_BEGIN
;
2265 CVC5_API_CHECK_NOT_NULL
;
2266 CVC5_API_CHECK(!d_node
->isNull())
2267 << "Expecting a non-null internal expression. This Op is not indexed.";
2268 size_t size
= getNumIndicesHelper();
2269 std::vector
<Term
> terms(getNumIndices());
2270 for (size_t i
= 0; i
< size
; i
++)
2272 terms
[i
] = getIndexHelper(i
);
2274 //////// all checks before this line
2277 CVC5_API_TRY_CATCH_END
;
2280 std::string
Op::toString() const
2282 CVC5_API_TRY_CATCH_BEGIN
;
2283 //////// all checks before this line
2284 if (d_node
->isNull())
2286 return kindToString(d_kind
);
2290 CVC5_API_CHECK(!d_node
->isNull())
2291 << "Expecting a non-null internal expression";
2292 if (d_solver
!= nullptr)
2294 return d_node
->toString();
2296 return d_node
->toString();
2299 CVC5_API_TRY_CATCH_END
;
2302 std::ostream
& operator<<(std::ostream
& out
, const Op
& t
)
2304 out
<< t
.toString();
2309 /* -------------------------------------------------------------------------- */
2311 /* Split out to avoid nested API calls (problematic with API tracing). */
2312 /* .......................................................................... */
2314 bool Op::isNullHelper() const
2316 return (d_node
->isNull() && (d_kind
== NULL_EXPR
));
2319 bool Op::isIndexedHelper() const { return !d_node
->isNull(); }
2321 /* -------------------------------------------------------------------------- */
2323 /* -------------------------------------------------------------------------- */
2325 Term::Term() : d_solver(nullptr), d_node(new cvc5::Node()) {}
2327 Term::Term(const Solver
* slv
, const cvc5::Node
& n
) : d_solver(slv
)
2329 d_node
.reset(new cvc5::Node(n
));
2334 if (d_solver
!= nullptr)
2340 bool Term::operator==(const Term
& t
) const
2342 CVC5_API_TRY_CATCH_BEGIN
;
2343 //////// all checks before this line
2344 return *d_node
== *t
.d_node
;
2346 CVC5_API_TRY_CATCH_END
;
2349 bool Term::operator!=(const Term
& t
) const
2351 CVC5_API_TRY_CATCH_BEGIN
;
2352 //////// all checks before this line
2353 return *d_node
!= *t
.d_node
;
2355 CVC5_API_TRY_CATCH_END
;
2358 bool Term::operator<(const Term
& t
) const
2360 CVC5_API_TRY_CATCH_BEGIN
;
2361 //////// all checks before this line
2362 return *d_node
< *t
.d_node
;
2364 CVC5_API_TRY_CATCH_END
;
2367 bool Term::operator>(const Term
& t
) const
2369 CVC5_API_TRY_CATCH_BEGIN
;
2370 //////// all checks before this line
2371 return *d_node
> *t
.d_node
;
2373 CVC5_API_TRY_CATCH_END
;
2376 bool Term::operator<=(const Term
& t
) const
2378 CVC5_API_TRY_CATCH_BEGIN
;
2379 //////// all checks before this line
2380 return *d_node
<= *t
.d_node
;
2382 CVC5_API_TRY_CATCH_END
;
2385 bool Term::operator>=(const Term
& t
) const
2387 CVC5_API_TRY_CATCH_BEGIN
;
2388 //////// all checks before this line
2389 return *d_node
>= *t
.d_node
;
2391 CVC5_API_TRY_CATCH_END
;
2394 size_t Term::getNumChildren() const
2396 CVC5_API_TRY_CATCH_BEGIN
;
2397 CVC5_API_CHECK_NOT_NULL
;
2398 //////// all checks before this line
2400 // special case for apply kinds
2401 if (isApplyKind(d_node
->getKind()))
2403 return d_node
->getNumChildren() + 1;
2409 return d_node
->getNumChildren();
2411 CVC5_API_TRY_CATCH_END
;
2414 Term
Term::operator[](size_t index
) const
2416 CVC5_API_TRY_CATCH_BEGIN
;
2417 CVC5_API_CHECK_NOT_NULL
;
2418 CVC5_API_CHECK(index
< getNumChildren()) << "index out of bound";
2419 CVC5_API_CHECK(!isApplyKind(d_node
->getKind()) || d_node
->hasOperator())
2420 << "Expected apply kind to have operator when accessing child of Term";
2421 //////// all checks before this line
2423 // special cases for apply kinds
2424 if (isApplyKind(d_node
->getKind()))
2428 // return the operator
2429 return Term(d_solver
, d_node
->getOperator());
2436 // otherwise we are looking up child at (index-1)
2437 return Term(d_solver
, (*d_node
)[index
]);
2439 CVC5_API_TRY_CATCH_END
;
2442 uint64_t Term::getId() const
2444 CVC5_API_TRY_CATCH_BEGIN
;
2445 CVC5_API_CHECK_NOT_NULL
;
2446 //////// all checks before this line
2447 return d_node
->getId();
2449 CVC5_API_TRY_CATCH_END
;
2452 Kind
Term::getKind() const
2454 CVC5_API_TRY_CATCH_BEGIN
;
2455 CVC5_API_CHECK_NOT_NULL
;
2456 //////// all checks before this line
2457 return getKindHelper();
2459 CVC5_API_TRY_CATCH_END
;
2462 Sort
Term::getSort() const
2464 CVC5_API_TRY_CATCH_BEGIN
;
2465 CVC5_API_CHECK_NOT_NULL
;
2466 //////// all checks before this line
2467 return Sort(d_solver
, d_node
->getType());
2469 CVC5_API_TRY_CATCH_END
;
2472 Term
Term::substitute(const Term
& term
, const Term
& replacement
) const
2474 CVC5_API_TRY_CATCH_BEGIN
;
2475 CVC5_API_CHECK_NOT_NULL
;
2476 CVC5_API_CHECK_TERM(term
);
2477 CVC5_API_CHECK_TERM(replacement
);
2478 CVC5_API_CHECK(term
.getSort() == replacement
.getSort())
2479 << "Expecting terms of the same sort in substitute";
2480 //////// all checks before this line
2483 d_node
->substitute(TNode(*term
.d_node
), TNode(*replacement
.d_node
)));
2485 CVC5_API_TRY_CATCH_END
;
2488 Term
Term::substitute(const std::vector
<Term
>& terms
,
2489 const std::vector
<Term
>& replacements
) const
2491 CVC5_API_TRY_CATCH_BEGIN
;
2492 CVC5_API_CHECK_NOT_NULL
;
2493 CVC5_API_CHECK(terms
.size() == replacements
.size())
2494 << "Expecting vectors of the same arity in substitute";
2495 CVC5_API_TERM_CHECK_TERMS_WITH_TERMS_SORT_EQUAL_TO(terms
, replacements
);
2496 //////// all checks before this line
2497 std::vector
<Node
> nodes
= Term::termVectorToNodes(terms
);
2498 std::vector
<Node
> nodeReplacements
= Term::termVectorToNodes(replacements
);
2499 return Term(d_solver
,
2500 d_node
->substitute(nodes
.begin(),
2502 nodeReplacements
.begin(),
2503 nodeReplacements
.end()));
2505 CVC5_API_TRY_CATCH_END
;
2508 bool Term::hasOp() const
2510 CVC5_API_TRY_CATCH_BEGIN
;
2511 CVC5_API_CHECK_NOT_NULL
;
2512 //////// all checks before this line
2513 return d_node
->hasOperator();
2515 CVC5_API_TRY_CATCH_END
;
2518 Op
Term::getOp() const
2520 CVC5_API_TRY_CATCH_BEGIN
;
2521 CVC5_API_CHECK_NOT_NULL
;
2522 CVC5_API_CHECK(d_node
->hasOperator())
2523 << "Expecting Term to have an Op when calling getOp()";
2524 //////// all checks before this line
2526 // special cases for parameterized operators that are not indexed operators
2527 // the API level differs from the internal structure
2528 // indexed operators are stored in Ops
2529 // whereas functions and datatype operators are terms, and the Op
2530 // is one of the APPLY_* kinds
2531 if (isApplyKind(d_node
->getKind()))
2533 return Op(d_solver
, intToExtKind(d_node
->getKind()));
2535 else if (d_node
->getMetaKind() == kind::metakind::PARAMETERIZED
)
2537 // it's an indexed operator
2538 // so we should return the indexed op
2539 cvc5::Node op
= d_node
->getOperator();
2540 return Op(d_solver
, intToExtKind(d_node
->getKind()), op
);
2542 // Notice this is the only case where getKindHelper is used, since the
2543 // cases above do not have special cases for intToExtKind.
2544 return Op(d_solver
, getKindHelper());
2546 CVC5_API_TRY_CATCH_END
;
2549 bool Term::hasSymbol() const
2551 CVC5_API_TRY_CATCH_BEGIN
;
2552 CVC5_API_CHECK_NOT_NULL
;
2553 //////// all checks before this line
2554 return d_node
->hasAttribute(expr::VarNameAttr());
2556 CVC5_API_TRY_CATCH_END
;
2559 std::string
Term::getSymbol() const
2561 CVC5_API_TRY_CATCH_BEGIN
;
2562 CVC5_API_CHECK_NOT_NULL
;
2563 CVC5_API_CHECK(d_node
->hasAttribute(expr::VarNameAttr()))
2564 << "Invalid call to '" << __PRETTY_FUNCTION__
2565 << "', expected the term to have a symbol.";
2566 //////// all checks before this line
2567 return d_node
->getAttribute(expr::VarNameAttr());
2569 CVC5_API_TRY_CATCH_END
;
2572 bool Term::isNull() const
2574 CVC5_API_TRY_CATCH_BEGIN
;
2575 //////// all checks before this line
2576 return isNullHelper();
2578 CVC5_API_TRY_CATCH_END
;
2581 Term
Term::notTerm() const
2583 CVC5_API_TRY_CATCH_BEGIN
;
2584 CVC5_API_CHECK_NOT_NULL
;
2585 //////// all checks before this line
2586 Node res
= d_node
->notNode();
2587 (void)res
.getType(true); /* kick off type checking */
2588 return Term(d_solver
, res
);
2590 CVC5_API_TRY_CATCH_END
;
2593 Term
Term::andTerm(const Term
& t
) const
2595 CVC5_API_TRY_CATCH_BEGIN
;
2596 CVC5_API_CHECK_NOT_NULL
;
2597 CVC5_API_CHECK_TERM(t
);
2598 //////// all checks before this line
2599 Node res
= d_node
->andNode(*t
.d_node
);
2600 (void)res
.getType(true); /* kick off type checking */
2601 return Term(d_solver
, res
);
2603 CVC5_API_TRY_CATCH_END
;
2606 Term
Term::orTerm(const Term
& t
) const
2608 CVC5_API_TRY_CATCH_BEGIN
;
2609 CVC5_API_CHECK_NOT_NULL
;
2610 CVC5_API_CHECK_TERM(t
);
2611 //////// all checks before this line
2612 Node res
= d_node
->orNode(*t
.d_node
);
2613 (void)res
.getType(true); /* kick off type checking */
2614 return Term(d_solver
, res
);
2616 CVC5_API_TRY_CATCH_END
;
2619 Term
Term::xorTerm(const Term
& t
) const
2621 CVC5_API_TRY_CATCH_BEGIN
;
2622 CVC5_API_CHECK_NOT_NULL
;
2623 CVC5_API_CHECK_TERM(t
);
2624 //////// all checks before this line
2625 Node res
= d_node
->xorNode(*t
.d_node
);
2626 (void)res
.getType(true); /* kick off type checking */
2627 return Term(d_solver
, res
);
2629 CVC5_API_TRY_CATCH_END
;
2632 Term
Term::eqTerm(const Term
& t
) const
2634 CVC5_API_TRY_CATCH_BEGIN
;
2635 CVC5_API_CHECK_NOT_NULL
;
2636 CVC5_API_CHECK_TERM(t
);
2637 //////// all checks before this line
2638 Node res
= d_node
->eqNode(*t
.d_node
);
2639 (void)res
.getType(true); /* kick off type checking */
2640 return Term(d_solver
, res
);
2642 CVC5_API_TRY_CATCH_END
;
2645 Term
Term::impTerm(const Term
& t
) const
2647 CVC5_API_TRY_CATCH_BEGIN
;
2648 CVC5_API_CHECK_NOT_NULL
;
2649 CVC5_API_CHECK_TERM(t
);
2650 //////// all checks before this line
2651 Node res
= d_node
->impNode(*t
.d_node
);
2652 (void)res
.getType(true); /* kick off type checking */
2653 return Term(d_solver
, res
);
2655 CVC5_API_TRY_CATCH_END
;
2658 Term
Term::iteTerm(const Term
& then_t
, const Term
& else_t
) const
2660 CVC5_API_TRY_CATCH_BEGIN
;
2661 CVC5_API_CHECK_NOT_NULL
;
2662 CVC5_API_CHECK_TERM(then_t
);
2663 CVC5_API_CHECK_TERM(else_t
);
2664 //////// all checks before this line
2665 Node res
= d_node
->iteNode(*then_t
.d_node
, *else_t
.d_node
);
2666 (void)res
.getType(true); /* kick off type checking */
2667 return Term(d_solver
, res
);
2669 CVC5_API_TRY_CATCH_END
;
2672 std::string
Term::toString() const
2674 CVC5_API_TRY_CATCH_BEGIN
;
2675 //////// all checks before this line
2676 return d_node
->toString();
2678 CVC5_API_TRY_CATCH_END
;
2681 Term::const_iterator::const_iterator()
2682 : d_solver(nullptr), d_origNode(nullptr), d_pos(0)
2686 Term::const_iterator::const_iterator(const Solver
* slv
,
2687 const std::shared_ptr
<cvc5::Node
>& n
,
2689 : d_solver(slv
), d_origNode(n
), d_pos(p
)
2693 Term::const_iterator::const_iterator(const const_iterator
& it
)
2694 : d_solver(nullptr), d_origNode(nullptr)
2696 if (it
.d_origNode
!= nullptr)
2698 d_solver
= it
.d_solver
;
2699 d_origNode
= it
.d_origNode
;
2704 Term::const_iterator
& Term::const_iterator::operator=(const const_iterator
& it
)
2706 d_solver
= it
.d_solver
;
2707 d_origNode
= it
.d_origNode
;
2712 bool Term::const_iterator::operator==(const const_iterator
& it
) const
2714 if (d_origNode
== nullptr || it
.d_origNode
== nullptr)
2718 return (d_solver
== it
.d_solver
&& *d_origNode
== *it
.d_origNode
)
2719 && (d_pos
== it
.d_pos
);
2722 bool Term::const_iterator::operator!=(const const_iterator
& it
) const
2724 return !(*this == it
);
2727 Term::const_iterator
& Term::const_iterator::operator++()
2729 Assert(d_origNode
!= nullptr);
2734 Term::const_iterator
Term::const_iterator::operator++(int)
2736 Assert(d_origNode
!= nullptr);
2737 const_iterator it
= *this;
2742 Term
Term::const_iterator::operator*() const
2744 Assert(d_origNode
!= nullptr);
2745 // this term has an extra child (mismatch between API and internal structure)
2746 // the extra child will be the first child
2747 bool extra_child
= isApplyKind(d_origNode
->getKind());
2749 if (!d_pos
&& extra_child
)
2751 return Term(d_solver
, d_origNode
->getOperator());
2755 uint32_t idx
= d_pos
;
2762 return Term(d_solver
, (*d_origNode
)[idx
]);
2766 Term::const_iterator
Term::begin() const
2768 return Term::const_iterator(d_solver
, d_node
, 0);
2771 Term::const_iterator
Term::end() const
2773 int endpos
= d_node
->getNumChildren();
2774 // special cases for APPLY_*
2775 // the API differs from the internal structure
2776 // the API takes a "higher-order" perspective and the applied
2777 // function or datatype constructor/selector/tester is a Term
2778 // which means it needs to be one of the children, even though
2779 // internally it is not
2780 if (isApplyKind(d_node
->getKind()))
2782 // one more child if this is a UF application (count the UF as a child)
2785 return Term::const_iterator(d_solver
, d_node
, endpos
);
2788 const cvc5::Node
& Term::getNode(void) const { return *d_node
; }
2791 const Rational
& getRational(const cvc5::Node
& node
)
2793 switch (node
.getKind())
2795 case cvc5::Kind::CAST_TO_REAL
: return node
[0].getConst
<Rational
>();
2796 case cvc5::Kind::CONST_RATIONAL
: return node
.getConst
<Rational
>();
2798 CVC5_API_CHECK(false) << "Node is not a rational.";
2799 return node
.getConst
<Rational
>();
2802 Integer
getInteger(const cvc5::Node
& node
)
2804 return node
.getConst
<Rational
>().getNumerator();
2806 template <typename T
>
2807 bool checkIntegerBounds(const Integer
& i
)
2809 return i
>= std::numeric_limits
<T
>::min()
2810 && i
<= std::numeric_limits
<T
>::max();
2812 bool checkReal32Bounds(const Rational
& r
)
2814 return checkIntegerBounds
<std::int32_t>(r
.getNumerator())
2815 && checkIntegerBounds
<std::uint32_t>(r
.getDenominator());
2817 bool checkReal64Bounds(const Rational
& r
)
2819 return checkIntegerBounds
<std::int64_t>(r
.getNumerator())
2820 && checkIntegerBounds
<std::uint64_t>(r
.getDenominator());
2823 bool isReal(const Node
& node
)
2825 return node
.getKind() == cvc5::Kind::CONST_RATIONAL
2826 || node
.getKind() == cvc5::Kind::CAST_TO_REAL
;
2828 bool isReal32(const Node
& node
)
2830 return isReal(node
) && checkReal32Bounds(getRational(node
));
2832 bool isReal64(const Node
& node
)
2834 return isReal(node
) && checkReal64Bounds(getRational(node
));
2837 bool isInteger(const Node
& node
)
2839 return node
.getKind() == cvc5::Kind::CONST_RATIONAL
2840 && node
.getConst
<Rational
>().isIntegral();
2842 bool isInt32(const Node
& node
)
2844 return isInteger(node
) && checkIntegerBounds
<std::int32_t>(getInteger(node
));
2846 bool isUInt32(const Node
& node
)
2848 return isInteger(node
) && checkIntegerBounds
<std::uint32_t>(getInteger(node
));
2850 bool isInt64(const Node
& node
)
2852 return isInteger(node
) && checkIntegerBounds
<std::int64_t>(getInteger(node
));
2854 bool isUInt64(const Node
& node
)
2856 return isInteger(node
) && checkIntegerBounds
<std::uint64_t>(getInteger(node
));
2858 } // namespace detail
2860 int32_t Term::getRealOrIntegerValueSign() const
2862 CVC5_API_TRY_CATCH_BEGIN
;
2863 CVC5_API_CHECK_NOT_NULL
;
2864 //////// all checks before this line
2865 const Rational
& r
= detail::getRational(*d_node
);
2866 return static_cast<int32_t>(r
.sgn());
2868 CVC5_API_TRY_CATCH_END
;
2871 bool Term::isInt32Value() const
2873 CVC5_API_TRY_CATCH_BEGIN
;
2874 CVC5_API_CHECK_NOT_NULL
;
2875 //////// all checks before this line
2876 return detail::isInt32(*d_node
);
2878 CVC5_API_TRY_CATCH_END
;
2881 std::int32_t Term::getInt32Value() const
2883 CVC5_API_TRY_CATCH_BEGIN
;
2884 CVC5_API_CHECK_NOT_NULL
;
2885 CVC5_API_ARG_CHECK_EXPECTED(detail::isInt32(*d_node
), *d_node
)
2886 << "Term to be a 32-bit integer value when calling getInt32Value()";
2887 //////// all checks before this line
2888 return detail::getInteger(*d_node
).getSignedInt();
2890 CVC5_API_TRY_CATCH_END
;
2893 bool Term::isUInt32Value() const
2895 CVC5_API_TRY_CATCH_BEGIN
;
2896 CVC5_API_CHECK_NOT_NULL
;
2897 //////// all checks before this line
2898 return detail::isUInt32(*d_node
);
2900 CVC5_API_TRY_CATCH_END
;
2902 std::uint32_t Term::getUInt32Value() const
2904 CVC5_API_TRY_CATCH_BEGIN
;
2905 CVC5_API_CHECK_NOT_NULL
;
2906 CVC5_API_ARG_CHECK_EXPECTED(detail::isUInt32(*d_node
), *d_node
)
2907 << "Term to be a unsigned 32-bit integer value when calling "
2909 //////// all checks before this line
2910 return detail::getInteger(*d_node
).getUnsignedInt();
2912 CVC5_API_TRY_CATCH_END
;
2915 bool Term::isInt64Value() const
2917 CVC5_API_TRY_CATCH_BEGIN
;
2918 CVC5_API_CHECK_NOT_NULL
;
2919 //////// all checks before this line
2920 return detail::isInt64(*d_node
);
2922 CVC5_API_TRY_CATCH_END
;
2924 std::int64_t Term::getInt64Value() const
2926 CVC5_API_TRY_CATCH_BEGIN
;
2927 CVC5_API_CHECK_NOT_NULL
;
2928 CVC5_API_ARG_CHECK_EXPECTED(detail::isInt64(*d_node
), *d_node
)
2929 << "Term to be a 64-bit integer value when calling getInt64Value()";
2930 //////// all checks before this line
2931 return detail::getInteger(*d_node
).getSigned64();
2933 CVC5_API_TRY_CATCH_END
;
2936 bool Term::isUInt64Value() const
2938 CVC5_API_TRY_CATCH_BEGIN
;
2939 CVC5_API_CHECK_NOT_NULL
;
2940 //////// all checks before this line
2941 return detail::isUInt64(*d_node
);
2943 CVC5_API_TRY_CATCH_END
;
2946 std::uint64_t Term::getUInt64Value() const
2948 CVC5_API_TRY_CATCH_BEGIN
;
2949 CVC5_API_CHECK_NOT_NULL
;
2950 CVC5_API_ARG_CHECK_EXPECTED(detail::isUInt64(*d_node
), *d_node
)
2951 << "Term to be a unsigned 64-bit integer value when calling "
2953 //////// all checks before this line
2954 return detail::getInteger(*d_node
).getUnsigned64();
2956 CVC5_API_TRY_CATCH_END
;
2959 bool Term::isIntegerValue() const
2961 CVC5_API_TRY_CATCH_BEGIN
;
2962 CVC5_API_CHECK_NOT_NULL
;
2963 //////// all checks before this line
2964 return detail::isInteger(*d_node
);
2966 CVC5_API_TRY_CATCH_END
;
2968 std::string
Term::getIntegerValue() const
2970 CVC5_API_TRY_CATCH_BEGIN
;
2971 CVC5_API_CHECK_NOT_NULL
;
2972 CVC5_API_ARG_CHECK_EXPECTED(detail::isInteger(*d_node
), *d_node
)
2973 << "Term to be an integer value when calling getIntegerValue()";
2974 //////// all checks before this line
2975 return detail::getInteger(*d_node
).toString();
2977 CVC5_API_TRY_CATCH_END
;
2980 bool Term::isStringValue() const
2982 CVC5_API_TRY_CATCH_BEGIN
;
2983 CVC5_API_CHECK_NOT_NULL
;
2984 //////// all checks before this line
2985 return d_node
->getKind() == cvc5::Kind::CONST_STRING
;
2987 CVC5_API_TRY_CATCH_END
;
2990 std::wstring
Term::getStringValue() const
2992 CVC5_API_TRY_CATCH_BEGIN
;
2993 CVC5_API_CHECK_NOT_NULL
;
2994 CVC5_API_ARG_CHECK_EXPECTED(d_node
->getKind() == cvc5::Kind::CONST_STRING
,
2996 << "Term to be a string value when calling getStringValue()";
2997 //////// all checks before this line
2998 return d_node
->getConst
<cvc5::String
>().toWString();
3000 CVC5_API_TRY_CATCH_END
;
3003 std::vector
<Node
> Term::termVectorToNodes(const std::vector
<Term
>& terms
)
3005 std::vector
<Node
> res
;
3006 for (const Term
& t
: terms
)
3008 res
.push_back(t
.getNode());
3013 bool Term::isReal32Value() const
3015 CVC5_API_TRY_CATCH_BEGIN
;
3016 CVC5_API_CHECK_NOT_NULL
;
3017 //////// all checks before this line
3018 return detail::isReal32(*d_node
);
3020 CVC5_API_TRY_CATCH_END
;
3022 std::pair
<std::int32_t, std::uint32_t> Term::getReal32Value() const
3024 CVC5_API_TRY_CATCH_BEGIN
;
3025 CVC5_API_CHECK_NOT_NULL
;
3026 CVC5_API_ARG_CHECK_EXPECTED(detail::isReal32(*d_node
), *d_node
)
3027 << "Term to be a 32-bit rational value when calling getReal32Value()";
3028 //////// all checks before this line
3029 const Rational
& r
= detail::getRational(*d_node
);
3030 return std::make_pair(r
.getNumerator().getSignedInt(),
3031 r
.getDenominator().getUnsignedInt());
3033 CVC5_API_TRY_CATCH_END
;
3035 bool Term::isReal64Value() const
3037 CVC5_API_TRY_CATCH_BEGIN
;
3038 CVC5_API_CHECK_NOT_NULL
;
3039 //////// all checks before this line
3040 return detail::isReal64(*d_node
);
3042 CVC5_API_TRY_CATCH_END
;
3044 std::pair
<std::int64_t, std::uint64_t> Term::getReal64Value() const
3046 CVC5_API_TRY_CATCH_BEGIN
;
3047 CVC5_API_CHECK_NOT_NULL
;
3048 CVC5_API_ARG_CHECK_EXPECTED(detail::isReal64(*d_node
), *d_node
)
3049 << "Term to be a 64-bit rational value when calling getReal64Value()";
3050 //////// all checks before this line
3051 const Rational
& r
= detail::getRational(*d_node
);
3052 return std::make_pair(r
.getNumerator().getSigned64(),
3053 r
.getDenominator().getUnsigned64());
3055 CVC5_API_TRY_CATCH_END
;
3057 bool Term::isRealValue() const
3059 CVC5_API_TRY_CATCH_BEGIN
;
3060 CVC5_API_CHECK_NOT_NULL
;
3061 //////// all checks before this line
3062 return detail::isReal(*d_node
);
3064 CVC5_API_TRY_CATCH_END
;
3066 std::string
Term::getRealValue() const
3068 CVC5_API_TRY_CATCH_BEGIN
;
3069 CVC5_API_CHECK_NOT_NULL
;
3070 CVC5_API_ARG_CHECK_EXPECTED(detail::isReal(*d_node
), *d_node
)
3071 << "Term to be a rational value when calling getRealValue()";
3072 //////// all checks before this line
3073 const Rational
& rat
= detail::getRational(*d_node
);
3074 std::string res
= rat
.toString();
3075 if (rat
.isIntegral())
3081 CVC5_API_TRY_CATCH_END
;
3084 bool Term::isConstArray() const
3086 CVC5_API_TRY_CATCH_BEGIN
;
3087 CVC5_API_CHECK_NOT_NULL
;
3088 //////// all checks before this line
3089 return d_node
->getKind() == cvc5::Kind::STORE_ALL
;
3091 CVC5_API_TRY_CATCH_END
;
3093 Term
Term::getConstArrayBase() const
3095 CVC5_API_TRY_CATCH_BEGIN
;
3096 CVC5_API_CHECK_NOT_NULL
;
3097 CVC5_API_ARG_CHECK_EXPECTED(d_node
->getKind() == cvc5::Kind::STORE_ALL
,
3099 << "Term to be a constant array when calling getConstArrayBase()";
3100 //////// all checks before this line
3101 const auto& ar
= d_node
->getConst
<ArrayStoreAll
>();
3102 return Term(d_solver
, ar
.getValue());
3104 CVC5_API_TRY_CATCH_END
;
3107 bool Term::isBooleanValue() const
3109 CVC5_API_TRY_CATCH_BEGIN
;
3110 CVC5_API_CHECK_NOT_NULL
;
3111 //////// all checks before this line
3112 return d_node
->getKind() == cvc5::Kind::CONST_BOOLEAN
;
3114 CVC5_API_TRY_CATCH_END
;
3116 bool Term::getBooleanValue() const
3118 CVC5_API_TRY_CATCH_BEGIN
;
3119 CVC5_API_CHECK_NOT_NULL
;
3120 CVC5_API_ARG_CHECK_EXPECTED(d_node
->getKind() == cvc5::Kind::CONST_BOOLEAN
,
3122 << "Term to be a Boolean value when calling getBooleanValue()";
3123 //////// all checks before this line
3124 return d_node
->getConst
<bool>();
3126 CVC5_API_TRY_CATCH_END
;
3129 bool Term::isBitVectorValue() const
3131 CVC5_API_TRY_CATCH_BEGIN
;
3132 CVC5_API_CHECK_NOT_NULL
;
3133 //////// all checks before this line
3134 return d_node
->getKind() == cvc5::Kind::CONST_BITVECTOR
;
3136 CVC5_API_TRY_CATCH_END
;
3138 std::string
Term::getBitVectorValue(std::uint32_t base
) const
3140 CVC5_API_TRY_CATCH_BEGIN
;
3141 CVC5_API_CHECK_NOT_NULL
;
3142 CVC5_API_ARG_CHECK_EXPECTED(d_node
->getKind() == cvc5::Kind::CONST_BITVECTOR
,
3144 << "Term to be a bit-vector value when calling getBitVectorValue()";
3145 //////// all checks before this line
3146 return d_node
->getConst
<BitVector
>().toString(base
);
3148 CVC5_API_TRY_CATCH_END
;
3151 bool Term::isUninterpretedSortValue() const
3153 CVC5_API_TRY_CATCH_BEGIN
;
3154 CVC5_API_CHECK_NOT_NULL
;
3155 //////// all checks before this line
3156 return d_node
->getKind() == cvc5::Kind::UNINTERPRETED_SORT_VALUE
;
3158 CVC5_API_TRY_CATCH_END
;
3160 std::string
Term::getUninterpretedSortValue() const
3162 CVC5_API_TRY_CATCH_BEGIN
;
3163 CVC5_API_CHECK_NOT_NULL
;
3164 CVC5_API_ARG_CHECK_EXPECTED(
3165 d_node
->getKind() == cvc5::Kind::UNINTERPRETED_SORT_VALUE
, *d_node
)
3166 << "Term to be an abstract value when calling "
3167 "getUninterpretedSortValue()";
3168 //////// all checks before this line
3169 std::stringstream ss
;
3170 ss
<< d_node
->getConst
<UninterpretedSortValue
>();
3173 CVC5_API_TRY_CATCH_END
;
3176 bool Term::isTupleValue() const
3178 CVC5_API_TRY_CATCH_BEGIN
;
3179 CVC5_API_CHECK_NOT_NULL
;
3180 //////// all checks before this line
3181 return d_node
->getKind() == cvc5::Kind::APPLY_CONSTRUCTOR
&& d_node
->isConst()
3182 && d_node
->getType().getDType().isTuple();
3184 CVC5_API_TRY_CATCH_END
;
3186 std::vector
<Term
> Term::getTupleValue() const
3188 CVC5_API_TRY_CATCH_BEGIN
;
3189 CVC5_API_CHECK_NOT_NULL
;
3190 CVC5_API_ARG_CHECK_EXPECTED(d_node
->getKind() == cvc5::Kind::APPLY_CONSTRUCTOR
3191 && d_node
->isConst()
3192 && d_node
->getType().getDType().isTuple(),
3194 << "Term to be a tuple value when calling getTupleValue()";
3195 //////// all checks before this line
3196 std::vector
<Term
> res
;
3197 for (size_t i
= 0, n
= d_node
->getNumChildren(); i
< n
; ++i
)
3199 res
.emplace_back(Term(d_solver
, (*d_node
)[i
]));
3203 CVC5_API_TRY_CATCH_END
;
3206 bool Term::isFloatingPointPosZero() const
3208 CVC5_API_TRY_CATCH_BEGIN
;
3209 CVC5_API_CHECK_NOT_NULL
;
3210 //////// all checks before this line
3211 if (d_node
->getKind() == cvc5::Kind::CONST_FLOATINGPOINT
)
3213 const auto& fp
= d_node
->getConst
<FloatingPoint
>();
3214 return fp
.isZero() && fp
.isPositive();
3218 CVC5_API_TRY_CATCH_END
;
3220 bool Term::isFloatingPointNegZero() const
3222 CVC5_API_TRY_CATCH_BEGIN
;
3223 CVC5_API_CHECK_NOT_NULL
;
3224 //////// all checks before this line
3225 if (d_node
->getKind() == cvc5::Kind::CONST_FLOATINGPOINT
)
3227 const auto& fp
= d_node
->getConst
<FloatingPoint
>();
3228 return fp
.isZero() && fp
.isNegative();
3232 CVC5_API_TRY_CATCH_END
;
3234 bool Term::isFloatingPointPosInf() const
3236 CVC5_API_TRY_CATCH_BEGIN
;
3237 CVC5_API_CHECK_NOT_NULL
;
3238 //////// all checks before this line
3239 if (d_node
->getKind() == cvc5::Kind::CONST_FLOATINGPOINT
)
3241 const auto& fp
= d_node
->getConst
<FloatingPoint
>();
3242 return fp
.isInfinite() && fp
.isPositive();
3246 CVC5_API_TRY_CATCH_END
;
3248 bool Term::isFloatingPointNegInf() const
3250 CVC5_API_TRY_CATCH_BEGIN
;
3251 CVC5_API_CHECK_NOT_NULL
;
3252 //////// all checks before this line
3253 if (d_node
->getKind() == cvc5::Kind::CONST_FLOATINGPOINT
)
3255 const auto& fp
= d_node
->getConst
<FloatingPoint
>();
3256 return fp
.isInfinite() && fp
.isNegative();
3260 CVC5_API_TRY_CATCH_END
;
3262 bool Term::isFloatingPointNaN() const
3264 CVC5_API_TRY_CATCH_BEGIN
;
3265 CVC5_API_CHECK_NOT_NULL
;
3266 //////// all checks before this line
3267 return d_node
->getKind() == cvc5::Kind::CONST_FLOATINGPOINT
3268 && d_node
->getConst
<FloatingPoint
>().isNaN();
3270 CVC5_API_TRY_CATCH_END
;
3272 bool Term::isFloatingPointValue() const
3274 CVC5_API_TRY_CATCH_BEGIN
;
3275 CVC5_API_CHECK_NOT_NULL
;
3276 //////// all checks before this line
3277 return d_node
->getKind() == cvc5::Kind::CONST_FLOATINGPOINT
;
3279 CVC5_API_TRY_CATCH_END
;
3281 std::tuple
<std::uint32_t, std::uint32_t, Term
> Term::getFloatingPointValue()
3284 CVC5_API_TRY_CATCH_BEGIN
;
3285 CVC5_API_CHECK_NOT_NULL
;
3286 CVC5_API_ARG_CHECK_EXPECTED(
3287 d_node
->getKind() == cvc5::Kind::CONST_FLOATINGPOINT
, *d_node
)
3288 << "Term to be a floating-point value when calling "
3289 "getFloatingPointValue()";
3290 //////// all checks before this line
3291 const auto& fp
= d_node
->getConst
<FloatingPoint
>();
3292 return std::make_tuple(fp
.getSize().exponentWidth(),
3293 fp
.getSize().significandWidth(),
3294 d_solver
->mkValHelper
<BitVector
>(fp
.pack()));
3296 CVC5_API_TRY_CATCH_END
;
3299 bool Term::isSetValue() const
3301 CVC5_API_TRY_CATCH_BEGIN
;
3302 CVC5_API_CHECK_NOT_NULL
;
3303 //////// all checks before this line
3304 return d_node
->getType().isSet() && d_node
->isConst();
3306 CVC5_API_TRY_CATCH_END
;
3309 void Term::collectSet(std::set
<Term
>& set
,
3310 const cvc5::Node
& node
,
3313 // We asserted that node has a set type, and node.isConst()
3314 // Thus, node only contains of SET_EMPTY, SET_UNION and SET_SINGLETON.
3315 switch (node
.getKind())
3317 case cvc5::Kind::SET_EMPTY
: break;
3318 case cvc5::Kind::SET_SINGLETON
: set
.emplace(Term(slv
, node
[0])); break;
3319 case cvc5::Kind::SET_UNION
:
3321 for (const auto& sub
: node
)
3323 collectSet(set
, sub
, slv
);
3328 CVC5_API_ARG_CHECK_EXPECTED(false, node
)
3329 << "Term to be a set value when calling getSetValue()";
3334 std::set
<Term
> Term::getSetValue() const
3336 CVC5_API_TRY_CATCH_BEGIN
;
3337 CVC5_API_CHECK_NOT_NULL
;
3338 CVC5_API_ARG_CHECK_EXPECTED(d_node
->getType().isSet() && d_node
->isConst(),
3340 << "Term to be a set value when calling getSetValue()";
3341 //////// all checks before this line
3343 Term::collectSet(res
, *d_node
, d_solver
);
3346 CVC5_API_TRY_CATCH_END
;
3349 bool Term::isSequenceValue() const
3351 CVC5_API_TRY_CATCH_BEGIN
;
3352 CVC5_API_CHECK_NOT_NULL
;
3353 //////// all checks before this line
3354 return d_node
->getKind() == cvc5::Kind::CONST_SEQUENCE
;
3356 CVC5_API_TRY_CATCH_END
;
3358 std::vector
<Term
> Term::getSequenceValue() const
3360 CVC5_API_TRY_CATCH_BEGIN
;
3361 CVC5_API_CHECK_NOT_NULL
;
3362 CVC5_API_ARG_CHECK_EXPECTED(d_node
->getKind() == cvc5::Kind::CONST_SEQUENCE
,
3364 << "Term to be a sequence value when calling getSequenceValue()";
3365 //////// all checks before this line
3366 std::vector
<Term
> res
;
3367 const Sequence
& seq
= d_node
->getConst
<Sequence
>();
3368 for (const auto& node
: seq
.getVec())
3370 res
.emplace_back(Term(d_solver
, node
));
3374 CVC5_API_TRY_CATCH_END
;
3377 std::ostream
& operator<<(std::ostream
& out
, const Term
& t
)
3379 out
<< t
.toString();
3383 std::ostream
& operator<<(std::ostream
& out
, const std::vector
<Term
>& vector
)
3385 container_to_stream(out
, vector
);
3389 std::ostream
& operator<<(std::ostream
& out
, const std::set
<Term
>& set
)
3391 container_to_stream(out
, set
);
3395 std::ostream
& operator<<(std::ostream
& out
,
3396 const std::unordered_set
<Term
>& unordered_set
)
3398 container_to_stream(out
, unordered_set
);
3402 template <typename V
>
3403 std::ostream
& operator<<(std::ostream
& out
, const std::map
<Term
, V
>& map
)
3405 container_to_stream(out
, map
);
3409 template <typename V
>
3410 std::ostream
& operator<<(std::ostream
& out
,
3411 const std::unordered_map
<Term
, V
>& unordered_map
)
3413 container_to_stream(out
, unordered_map
);
3418 /* -------------------------------------------------------------------------- */
3420 /* Split out to avoid nested API calls (problematic with API tracing). */
3421 /* .......................................................................... */
3423 bool Term::isNullHelper() const
3425 /* Split out to avoid nested API calls (problematic with API tracing). */
3426 return d_node
->isNull();
3429 Kind
Term::getKindHelper() const
3431 /* Sequence kinds do not exist internally, so we must convert their internal
3432 * (string) versions back to sequence. All operators where this is
3433 * necessary are such that their first child is of sequence type, which
3435 if (d_node
->getNumChildren() > 0 && (*d_node
)[0].getType().isSequence())
3437 switch (d_node
->getKind())
3439 case cvc5::Kind::STRING_CONCAT
: return SEQ_CONCAT
;
3440 case cvc5::Kind::STRING_LENGTH
: return SEQ_LENGTH
;
3441 case cvc5::Kind::STRING_SUBSTR
: return SEQ_EXTRACT
;
3442 case cvc5::Kind::STRING_UPDATE
: return SEQ_UPDATE
;
3443 case cvc5::Kind::STRING_CHARAT
: return SEQ_AT
;
3444 case cvc5::Kind::STRING_CONTAINS
: return SEQ_CONTAINS
;
3445 case cvc5::Kind::STRING_INDEXOF
: return SEQ_INDEXOF
;
3446 case cvc5::Kind::STRING_REPLACE
: return SEQ_REPLACE
;
3447 case cvc5::Kind::STRING_REPLACE_ALL
: return SEQ_REPLACE_ALL
;
3448 case cvc5::Kind::STRING_REV
: return SEQ_REV
;
3449 case cvc5::Kind::STRING_PREFIX
: return SEQ_PREFIX
;
3450 case cvc5::Kind::STRING_SUFFIX
: return SEQ_SUFFIX
;
3452 // fall through to conversion below
3456 // Notice that kinds like APPLY_TYPE_ASCRIPTION will be converted to
3460 return CONST_RATIONAL
;
3462 return intToExtKind(d_node
->getKind());
3465 bool Term::isCastedReal() const
3467 if (d_node
->getKind() == kind::CAST_TO_REAL
)
3469 return (*d_node
)[0].isConst() && (*d_node
)[0].getType().isInteger();
3474 /* -------------------------------------------------------------------------- */
3476 /* -------------------------------------------------------------------------- */
3478 /* DatatypeConstructorDecl -------------------------------------------------- */
3480 DatatypeConstructorDecl::DatatypeConstructorDecl()
3481 : d_solver(nullptr), d_ctor(nullptr)
3485 DatatypeConstructorDecl::DatatypeConstructorDecl(const Solver
* slv
,
3486 const std::string
& name
)
3487 : d_solver(slv
), d_ctor(new cvc5::DTypeConstructor(name
))
3490 DatatypeConstructorDecl::~DatatypeConstructorDecl()
3492 if (d_ctor
!= nullptr)
3498 void DatatypeConstructorDecl::addSelector(const std::string
& name
,
3501 CVC5_API_TRY_CATCH_BEGIN
;
3502 CVC5_API_CHECK_NOT_NULL
;
3503 CVC5_API_CHECK_SORT(sort
);
3504 CVC5_API_ARG_CHECK_EXPECTED(!sort
.isNull(), sort
)
3505 << "non-null codomain sort for selector";
3506 //////// all checks before this line
3507 d_ctor
->addArg(name
, *sort
.d_type
);
3509 CVC5_API_TRY_CATCH_END
;
3512 void DatatypeConstructorDecl::addSelectorSelf(const std::string
& name
)
3514 CVC5_API_TRY_CATCH_BEGIN
;
3515 CVC5_API_CHECK_NOT_NULL
;
3516 //////// all checks before this line
3517 d_ctor
->addArgSelf(name
);
3519 CVC5_API_TRY_CATCH_END
;
3522 bool DatatypeConstructorDecl::isNull() const
3524 CVC5_API_TRY_CATCH_BEGIN
;
3525 //////// all checks before this line
3526 return isNullHelper();
3528 CVC5_API_TRY_CATCH_END
;
3531 std::string
DatatypeConstructorDecl::toString() const
3533 CVC5_API_TRY_CATCH_BEGIN
;
3534 //////// all checks before this line
3535 std::stringstream ss
;
3539 CVC5_API_TRY_CATCH_END
;
3542 std::ostream
& operator<<(std::ostream
& out
,
3543 const DatatypeConstructorDecl
& ctordecl
)
3545 out
<< ctordecl
.toString();
3549 std::ostream
& operator<<(std::ostream
& out
,
3550 const std::vector
<DatatypeConstructorDecl
>& vector
)
3552 container_to_stream(out
, vector
);
3556 bool DatatypeConstructorDecl::isNullHelper() const { return d_ctor
== nullptr; }
3558 bool DatatypeConstructorDecl::isResolved() const
3560 return d_ctor
== nullptr || d_ctor
->isResolved();
3563 /* DatatypeDecl ------------------------------------------------------------- */
3565 DatatypeDecl::DatatypeDecl() : d_solver(nullptr), d_dtype(nullptr) {}
3567 DatatypeDecl::DatatypeDecl(const Solver
* slv
,
3568 const std::string
& name
,
3570 : d_solver(slv
), d_dtype(new cvc5::DType(name
, isCoDatatype
))
3574 DatatypeDecl::DatatypeDecl(const Solver
* slv
,
3575 const std::string
& name
,
3579 d_dtype(new cvc5::DType(
3580 name
, std::vector
<TypeNode
>{*param
.d_type
}, isCoDatatype
))
3584 DatatypeDecl::DatatypeDecl(const Solver
* slv
,
3585 const std::string
& name
,
3586 const std::vector
<Sort
>& params
,
3590 std::vector
<TypeNode
> tparams
= Sort::sortVectorToTypeNodes(params
);
3591 d_dtype
= std::shared_ptr
<cvc5::DType
>(
3592 new cvc5::DType(name
, tparams
, isCoDatatype
));
3595 bool DatatypeDecl::isNullHelper() const { return !d_dtype
; }
3597 DatatypeDecl::~DatatypeDecl()
3599 if (d_dtype
!= nullptr)
3605 void DatatypeDecl::addConstructor(const DatatypeConstructorDecl
& ctor
)
3607 CVC5_API_TRY_CATCH_BEGIN
;
3608 CVC5_API_CHECK_NOT_NULL
;
3609 CVC5_API_ARG_CHECK_NOT_NULL(ctor
);
3610 CVC5_API_ARG_CHECK_SOLVER("datatype constructor declaration", ctor
);
3611 //////// all checks before this line
3612 d_dtype
->addConstructor(ctor
.d_ctor
);
3614 CVC5_API_TRY_CATCH_END
;
3617 size_t DatatypeDecl::getNumConstructors() const
3619 CVC5_API_TRY_CATCH_BEGIN
;
3620 CVC5_API_CHECK_NOT_NULL
;
3621 //////// all checks before this line
3622 return d_dtype
->getNumConstructors();
3624 CVC5_API_TRY_CATCH_END
;
3627 bool DatatypeDecl::isParametric() const
3629 CVC5_API_TRY_CATCH_BEGIN
;
3630 CVC5_API_CHECK_NOT_NULL
;
3631 //////// all checks before this line
3632 return d_dtype
->isParametric();
3634 CVC5_API_TRY_CATCH_END
;
3637 std::string
DatatypeDecl::toString() const
3639 CVC5_API_TRY_CATCH_BEGIN
;
3640 CVC5_API_CHECK_NOT_NULL
;
3641 //////// all checks before this line
3642 std::stringstream ss
;
3646 CVC5_API_TRY_CATCH_END
;
3649 std::string
DatatypeDecl::getName() const
3651 CVC5_API_TRY_CATCH_BEGIN
;
3652 CVC5_API_CHECK_NOT_NULL
;
3653 //////// all checks before this line
3654 return d_dtype
->getName();
3656 CVC5_API_TRY_CATCH_END
;
3659 bool DatatypeDecl::isNull() const
3661 CVC5_API_TRY_CATCH_BEGIN
;
3662 //////// all checks before this line
3663 return isNullHelper();
3665 CVC5_API_TRY_CATCH_END
;
3668 std::ostream
& operator<<(std::ostream
& out
, const DatatypeDecl
& dtdecl
)
3670 out
<< dtdecl
.toString();
3674 cvc5::DType
& DatatypeDecl::getDatatype(void) const { return *d_dtype
; }
3676 /* DatatypeSelector --------------------------------------------------------- */
3678 DatatypeSelector::DatatypeSelector() : d_solver(nullptr), d_stor(nullptr) {}
3680 DatatypeSelector::DatatypeSelector(const Solver
* slv
,
3681 const cvc5::DTypeSelector
& stor
)
3682 : d_solver(slv
), d_stor(new cvc5::DTypeSelector(stor
))
3684 CVC5_API_CHECK(d_stor
->isResolved()) << "Expected resolved datatype selector";
3687 DatatypeSelector::~DatatypeSelector()
3689 if (d_stor
!= nullptr)
3695 std::string
DatatypeSelector::getName() const
3697 CVC5_API_TRY_CATCH_BEGIN
;
3698 CVC5_API_CHECK_NOT_NULL
;
3699 //////// all checks before this line
3700 return d_stor
->getName();
3702 CVC5_API_TRY_CATCH_END
;
3705 Term
DatatypeSelector::getSelectorTerm() const
3707 CVC5_API_TRY_CATCH_BEGIN
;
3708 CVC5_API_CHECK_NOT_NULL
;
3709 //////// all checks before this line
3710 return Term(d_solver
, d_stor
->getSelector());
3712 CVC5_API_TRY_CATCH_END
;
3714 Term
DatatypeSelector::getUpdaterTerm() const
3716 CVC5_API_TRY_CATCH_BEGIN
;
3717 CVC5_API_CHECK_NOT_NULL
;
3718 //////// all checks before this line
3719 return Term(d_solver
, d_stor
->getUpdater());
3721 CVC5_API_TRY_CATCH_END
;
3724 Sort
DatatypeSelector::getCodomainSort() const
3726 CVC5_API_TRY_CATCH_BEGIN
;
3727 CVC5_API_CHECK_NOT_NULL
;
3728 //////// all checks before this line
3729 return Sort(d_solver
, d_stor
->getRangeType());
3731 CVC5_API_TRY_CATCH_END
;
3734 bool DatatypeSelector::isNull() const
3736 CVC5_API_TRY_CATCH_BEGIN
;
3737 //////// all checks before this line
3738 return isNullHelper();
3740 CVC5_API_TRY_CATCH_END
;
3743 std::string
DatatypeSelector::toString() const
3745 CVC5_API_TRY_CATCH_BEGIN
;
3746 //////// all checks before this line
3747 std::stringstream ss
;
3751 CVC5_API_TRY_CATCH_END
;
3754 std::ostream
& operator<<(std::ostream
& out
, const DatatypeSelector
& stor
)
3756 out
<< stor
.toString();
3760 bool DatatypeSelector::isNullHelper() const { return d_stor
== nullptr; }
3762 /* DatatypeConstructor ------------------------------------------------------ */
3764 DatatypeConstructor::DatatypeConstructor() : d_solver(nullptr), d_ctor(nullptr)
3768 DatatypeConstructor::DatatypeConstructor(const Solver
* slv
,
3769 const cvc5::DTypeConstructor
& ctor
)
3770 : d_solver(slv
), d_ctor(new cvc5::DTypeConstructor(ctor
))
3772 CVC5_API_CHECK(d_ctor
->isResolved())
3773 << "Expected resolved datatype constructor";
3776 DatatypeConstructor::~DatatypeConstructor()
3778 if (d_ctor
!= nullptr)
3784 std::string
DatatypeConstructor::getName() const
3786 CVC5_API_TRY_CATCH_BEGIN
;
3787 CVC5_API_CHECK_NOT_NULL
;
3788 //////// all checks before this line
3789 return d_ctor
->getName();
3791 CVC5_API_TRY_CATCH_END
;
3794 Term
DatatypeConstructor::getConstructorTerm() const
3796 CVC5_API_TRY_CATCH_BEGIN
;
3797 CVC5_API_CHECK_NOT_NULL
;
3798 //////// all checks before this line
3799 return Term(d_solver
, d_ctor
->getConstructor());
3801 CVC5_API_TRY_CATCH_END
;
3804 Term
DatatypeConstructor::getInstantiatedConstructorTerm(
3805 const Sort
& retSort
) const
3807 CVC5_API_TRY_CATCH_BEGIN
;
3808 CVC5_API_CHECK_NOT_NULL
;
3809 CVC5_API_CHECK(d_ctor
->isResolved())
3810 << "Expected resolved datatype constructor";
3811 CVC5_API_CHECK(retSort
.isDatatype())
3812 << "Cannot get specialized constructor type for non-datatype type "
3814 //////// all checks before this line
3815 Node ret
= d_ctor
->getInstantiatedConstructor(*retSort
.d_type
);
3816 (void)ret
.getType(true); /* kick off type checking */
3817 // apply type ascription to the operator
3818 Term sctor
= api::Term(d_solver
, ret
);
3821 CVC5_API_TRY_CATCH_END
;
3824 Term
DatatypeConstructor::getTesterTerm() const
3826 CVC5_API_TRY_CATCH_BEGIN
;
3827 CVC5_API_CHECK_NOT_NULL
;
3828 //////// all checks before this line
3829 return Term(d_solver
, d_ctor
->getTester());
3831 CVC5_API_TRY_CATCH_END
;
3834 size_t DatatypeConstructor::getNumSelectors() const
3836 CVC5_API_TRY_CATCH_BEGIN
;
3837 CVC5_API_CHECK_NOT_NULL
;
3838 //////// all checks before this line
3839 return d_ctor
->getNumArgs();
3841 CVC5_API_TRY_CATCH_END
;
3844 DatatypeSelector
DatatypeConstructor::operator[](size_t index
) const
3846 CVC5_API_TRY_CATCH_BEGIN
;
3847 CVC5_API_CHECK_NOT_NULL
;
3848 //////// all checks before this line
3849 return DatatypeSelector(d_solver
, (*d_ctor
)[index
]);
3851 CVC5_API_TRY_CATCH_END
;
3854 DatatypeSelector
DatatypeConstructor::operator[](const std::string
& name
) const
3856 CVC5_API_TRY_CATCH_BEGIN
;
3857 CVC5_API_CHECK_NOT_NULL
;
3858 //////// all checks before this line
3859 return getSelectorForName(name
);
3861 CVC5_API_TRY_CATCH_END
;
3864 DatatypeSelector
DatatypeConstructor::getSelector(const std::string
& name
) const
3866 CVC5_API_TRY_CATCH_BEGIN
;
3867 CVC5_API_CHECK_NOT_NULL
;
3868 //////// all checks before this line
3869 return getSelectorForName(name
);
3871 CVC5_API_TRY_CATCH_END
;
3874 Term
DatatypeConstructor::getSelectorTerm(const std::string
& name
) const
3876 CVC5_API_TRY_CATCH_BEGIN
;
3877 CVC5_API_CHECK_NOT_NULL
;
3878 //////// all checks before this line
3879 return getSelector(name
).getSelectorTerm();
3881 CVC5_API_TRY_CATCH_END
;
3884 DatatypeConstructor::const_iterator
DatatypeConstructor::begin() const
3886 return DatatypeConstructor::const_iterator(d_solver
, *d_ctor
, true);
3889 DatatypeConstructor::const_iterator
DatatypeConstructor::end() const
3891 return DatatypeConstructor::const_iterator(d_solver
, *d_ctor
, false);
3894 DatatypeConstructor::const_iterator::const_iterator(
3895 const Solver
* slv
, const cvc5::DTypeConstructor
& ctor
, bool begin
)
3898 d_int_stors
= &ctor
.getArgs();
3900 const std::vector
<std::shared_ptr
<cvc5::DTypeSelector
>>& sels
=
3902 for (const std::shared_ptr
<cvc5::DTypeSelector
>& s
: sels
)
3904 /* Can not use emplace_back here since constructor is private. */
3905 d_stors
.push_back(DatatypeSelector(d_solver
, *s
.get()));
3907 d_idx
= begin
? 0 : sels
.size();
3910 DatatypeConstructor::const_iterator::const_iterator()
3911 : d_solver(nullptr), d_int_stors(nullptr), d_idx(0)
3915 DatatypeConstructor::const_iterator
&
3916 DatatypeConstructor::const_iterator::operator=(
3917 const DatatypeConstructor::const_iterator
& it
)
3919 d_solver
= it
.d_solver
;
3920 d_int_stors
= it
.d_int_stors
;
3921 d_stors
= it
.d_stors
;
3926 const DatatypeSelector
& DatatypeConstructor::const_iterator::operator*() const
3928 return d_stors
[d_idx
];
3931 const DatatypeSelector
* DatatypeConstructor::const_iterator::operator->() const
3933 return &d_stors
[d_idx
];
3936 DatatypeConstructor::const_iterator
&
3937 DatatypeConstructor::const_iterator::operator++()
3943 DatatypeConstructor::const_iterator
3944 DatatypeConstructor::const_iterator::operator++(int)
3946 DatatypeConstructor::const_iterator
it(*this);
3951 bool DatatypeConstructor::const_iterator::operator==(
3952 const DatatypeConstructor::const_iterator
& other
) const
3954 return d_int_stors
== other
.d_int_stors
&& d_idx
== other
.d_idx
;
3957 bool DatatypeConstructor::const_iterator::operator!=(
3958 const DatatypeConstructor::const_iterator
& other
) const
3960 return d_int_stors
!= other
.d_int_stors
|| d_idx
!= other
.d_idx
;
3963 bool DatatypeConstructor::isNull() const
3965 CVC5_API_TRY_CATCH_BEGIN
;
3966 //////// all checks before this line
3967 return isNullHelper();
3969 CVC5_API_TRY_CATCH_END
;
3972 std::string
DatatypeConstructor::toString() const
3974 CVC5_API_TRY_CATCH_BEGIN
;
3975 //////// all checks before this line
3976 std::stringstream ss
;
3980 CVC5_API_TRY_CATCH_END
;
3983 bool DatatypeConstructor::isNullHelper() const { return d_ctor
== nullptr; }
3985 DatatypeSelector
DatatypeConstructor::getSelectorForName(
3986 const std::string
& name
) const
3988 bool foundSel
= false;
3990 for (size_t i
= 0, nsels
= getNumSelectors(); i
< nsels
; i
++)
3992 if ((*d_ctor
)[i
].getName() == name
)
4001 std::stringstream snames
;
4003 for (size_t i
= 0, ncons
= getNumSelectors(); i
< ncons
; i
++)
4005 snames
<< (*d_ctor
)[i
].getName() << " ";
4008 CVC5_API_CHECK(foundSel
) << "No selector " << name
<< " for constructor "
4009 << getName() << " exists among " << snames
.str();
4011 return DatatypeSelector(d_solver
, (*d_ctor
)[index
]);
4014 std::ostream
& operator<<(std::ostream
& out
, const DatatypeConstructor
& ctor
)
4016 out
<< ctor
.toString();
4020 /* Datatype ----------------------------------------------------------------- */
4022 Datatype::Datatype(const Solver
* slv
, const cvc5::DType
& dtype
)
4023 : d_solver(slv
), d_dtype(new cvc5::DType(dtype
))
4025 CVC5_API_CHECK(d_dtype
->isResolved()) << "Expected resolved datatype";
4028 Datatype::Datatype() : d_solver(nullptr), d_dtype(nullptr) {}
4030 Datatype::~Datatype()
4032 if (d_dtype
!= nullptr)
4038 DatatypeConstructor
Datatype::operator[](size_t idx
) const
4040 CVC5_API_TRY_CATCH_BEGIN
;
4041 CVC5_API_CHECK_NOT_NULL
;
4042 CVC5_API_CHECK(idx
< getNumConstructors()) << "Index out of bounds.";
4043 //////// all checks before this line
4044 return DatatypeConstructor(d_solver
, (*d_dtype
)[idx
]);
4046 CVC5_API_TRY_CATCH_END
;
4049 DatatypeConstructor
Datatype::operator[](const std::string
& name
) const
4051 CVC5_API_TRY_CATCH_BEGIN
;
4052 CVC5_API_CHECK_NOT_NULL
;
4053 //////// all checks before this line
4054 return getConstructorForName(name
);
4056 CVC5_API_TRY_CATCH_END
;
4059 DatatypeConstructor
Datatype::getConstructor(const std::string
& name
) const
4061 CVC5_API_TRY_CATCH_BEGIN
;
4062 CVC5_API_CHECK_NOT_NULL
;
4063 //////// all checks before this line
4064 return getConstructorForName(name
);
4066 CVC5_API_TRY_CATCH_END
;
4069 Term
Datatype::getConstructorTerm(const std::string
& name
) const
4071 CVC5_API_TRY_CATCH_BEGIN
;
4072 CVC5_API_CHECK_NOT_NULL
;
4073 //////// all checks before this line
4074 return getConstructorForName(name
).getConstructorTerm();
4076 CVC5_API_TRY_CATCH_END
;
4079 DatatypeSelector
Datatype::getSelector(const std::string
& name
) const
4081 CVC5_API_TRY_CATCH_BEGIN
;
4082 CVC5_API_CHECK_NOT_NULL
;
4083 //////// all checks before this line
4084 return getSelectorForName(name
);
4086 CVC5_API_TRY_CATCH_END
;
4089 std::string
Datatype::getName() const
4091 CVC5_API_TRY_CATCH_BEGIN
;
4092 CVC5_API_CHECK_NOT_NULL
;
4093 //////// all checks before this line
4094 return d_dtype
->getName();
4096 CVC5_API_TRY_CATCH_END
;
4099 size_t Datatype::getNumConstructors() const
4101 CVC5_API_TRY_CATCH_BEGIN
;
4102 CVC5_API_CHECK_NOT_NULL
;
4103 //////// all checks before this line
4104 return d_dtype
->getNumConstructors();
4106 CVC5_API_TRY_CATCH_END
;
4109 std::vector
<Sort
> Datatype::getParameters() const
4111 CVC5_API_TRY_CATCH_BEGIN
;
4112 CVC5_API_CHECK_NOT_NULL
;
4113 CVC5_API_CHECK(isParametric()) << "Expected parametric datatype";
4114 //////// all checks before this line
4115 std::vector
<cvc5::TypeNode
> params
= d_dtype
->getParameters();
4116 return Sort::typeNodeVectorToSorts(d_solver
, params
);
4118 CVC5_API_TRY_CATCH_END
;
4121 bool Datatype::isParametric() const
4123 CVC5_API_TRY_CATCH_BEGIN
;
4124 CVC5_API_CHECK_NOT_NULL
;
4125 //////// all checks before this line
4126 return d_dtype
->isParametric();
4128 CVC5_API_TRY_CATCH_END
;
4131 bool Datatype::isCodatatype() const
4133 CVC5_API_TRY_CATCH_BEGIN
;
4134 CVC5_API_CHECK_NOT_NULL
;
4135 //////// all checks before this line
4136 return d_dtype
->isCodatatype();
4138 CVC5_API_TRY_CATCH_END
;
4141 bool Datatype::isTuple() const
4143 CVC5_API_TRY_CATCH_BEGIN
;
4144 CVC5_API_CHECK_NOT_NULL
;
4145 //////// all checks before this line
4146 return d_dtype
->isTuple();
4148 CVC5_API_TRY_CATCH_END
;
4151 bool Datatype::isRecord() const
4153 CVC5_API_TRY_CATCH_BEGIN
;
4154 CVC5_API_CHECK_NOT_NULL
;
4155 //////// all checks before this line
4156 return d_dtype
->isRecord();
4158 CVC5_API_TRY_CATCH_END
;
4161 bool Datatype::isFinite() const
4163 CVC5_API_TRY_CATCH_BEGIN
;
4164 CVC5_API_CHECK_NOT_NULL
;
4165 CVC5_API_CHECK(!d_dtype
->isParametric())
4166 << "Invalid call to 'isFinite()', expected non-parametric Datatype";
4167 //////// all checks before this line
4168 // we assume that finite model finding is disabled by passing false as the
4170 return isCardinalityClassFinite(d_dtype
->getCardinalityClass(), false);
4172 CVC5_API_TRY_CATCH_END
;
4175 bool Datatype::isWellFounded() const
4177 CVC5_API_TRY_CATCH_BEGIN
;
4178 CVC5_API_CHECK_NOT_NULL
;
4179 //////// all checks before this line
4180 return d_dtype
->isWellFounded();
4182 CVC5_API_TRY_CATCH_END
;
4185 bool Datatype::isNull() const
4187 CVC5_API_TRY_CATCH_BEGIN
;
4188 //////// all checks before this line
4189 return isNullHelper();
4191 CVC5_API_TRY_CATCH_END
;
4194 std::string
Datatype::toString() const
4196 CVC5_API_TRY_CATCH_BEGIN
;
4197 CVC5_API_CHECK_NOT_NULL
;
4198 //////// all checks before this line
4199 return d_dtype
->getName();
4201 CVC5_API_TRY_CATCH_END
;
4204 Datatype::const_iterator
Datatype::begin() const
4206 return Datatype::const_iterator(d_solver
, *d_dtype
, true);
4209 Datatype::const_iterator
Datatype::end() const
4211 return Datatype::const_iterator(d_solver
, *d_dtype
, false);
4214 DatatypeConstructor
Datatype::getConstructorForName(
4215 const std::string
& name
) const
4217 bool foundCons
= false;
4219 for (size_t i
= 0, ncons
= getNumConstructors(); i
< ncons
; i
++)
4221 if ((*d_dtype
)[i
].getName() == name
)
4230 std::stringstream snames
;
4232 for (size_t i
= 0, ncons
= getNumConstructors(); i
< ncons
; i
++)
4234 snames
<< (*d_dtype
)[i
].getName() << " ";
4237 CVC5_API_CHECK(foundCons
) << "No constructor " << name
<< " for datatype "
4238 << getName() << " exists, among " << snames
.str();
4240 return DatatypeConstructor(d_solver
, (*d_dtype
)[index
]);
4243 DatatypeSelector
Datatype::getSelectorForName(const std::string
& name
) const
4245 bool foundSel
= false;
4248 for (size_t i
= 0, ncons
= getNumConstructors(); i
< ncons
; i
++)
4250 int si
= (*d_dtype
)[i
].getSelectorIndexForName(name
);
4253 sindex
= static_cast<size_t>(si
);
4261 CVC5_API_CHECK(foundSel
)
4262 << "No select " << name
<< " for datatype " << getName() << " exists";
4264 return DatatypeSelector(d_solver
, (*d_dtype
)[index
][sindex
]);
4267 Datatype::const_iterator::const_iterator(const Solver
* slv
,
4268 const cvc5::DType
& dtype
,
4270 : d_solver(slv
), d_int_ctors(&dtype
.getConstructors())
4272 const std::vector
<std::shared_ptr
<DTypeConstructor
>>& cons
=
4273 dtype
.getConstructors();
4274 for (const std::shared_ptr
<DTypeConstructor
>& c
: cons
)
4276 /* Can not use emplace_back here since constructor is private. */
4277 d_ctors
.push_back(DatatypeConstructor(d_solver
, *c
.get()));
4279 d_idx
= begin
? 0 : cons
.size();
4282 Datatype::const_iterator::const_iterator()
4283 : d_solver(nullptr), d_int_ctors(nullptr), d_idx(0)
4287 Datatype::const_iterator
& Datatype::const_iterator::operator=(
4288 const Datatype::const_iterator
& it
)
4290 d_solver
= it
.d_solver
;
4291 d_int_ctors
= it
.d_int_ctors
;
4292 d_ctors
= it
.d_ctors
;
4297 const DatatypeConstructor
& Datatype::const_iterator::operator*() const
4299 return d_ctors
[d_idx
];
4302 const DatatypeConstructor
* Datatype::const_iterator::operator->() const
4304 return &d_ctors
[d_idx
];
4307 Datatype::const_iterator
& Datatype::const_iterator::operator++()
4313 Datatype::const_iterator
Datatype::const_iterator::operator++(int)
4315 Datatype::const_iterator
it(*this);
4320 bool Datatype::const_iterator::operator==(
4321 const Datatype::const_iterator
& other
) const
4323 return d_int_ctors
== other
.d_int_ctors
&& d_idx
== other
.d_idx
;
4326 bool Datatype::const_iterator::operator!=(
4327 const Datatype::const_iterator
& other
) const
4329 return d_int_ctors
!= other
.d_int_ctors
|| d_idx
!= other
.d_idx
;
4332 bool Datatype::isNullHelper() const { return d_dtype
== nullptr; }
4334 /* -------------------------------------------------------------------------- */
4336 /* -------------------------------------------------------------------------- */
4339 : d_solver(nullptr),
4349 Grammar::Grammar(const Solver
* slv
,
4350 const std::vector
<Term
>& sygusVars
,
4351 const std::vector
<Term
>& ntSymbols
)
4353 d_sygusVars(sygusVars
),
4354 d_ntSyms(ntSymbols
),
4355 d_ntsToTerms(ntSymbols
.size()),
4360 for (Term ntsymbol
: d_ntSyms
)
4362 d_ntsToTerms
.emplace(ntsymbol
, std::vector
<Term
>());
4366 void Grammar::addRule(const Term
& ntSymbol
, const Term
& rule
)
4368 CVC5_API_TRY_CATCH_BEGIN
;
4369 CVC5_API_CHECK(!d_isResolved
) << "Grammar cannot be modified after passing "
4370 "it as an argument to synthFun/synthInv";
4371 CVC5_API_CHECK_TERM(ntSymbol
);
4372 CVC5_API_CHECK_TERM(rule
);
4373 CVC5_API_ARG_CHECK_EXPECTED(
4374 d_ntsToTerms
.find(ntSymbol
) != d_ntsToTerms
.cend(), ntSymbol
)
4375 << "ntSymbol to be one of the non-terminal symbols given in the "
4377 CVC5_API_CHECK(ntSymbol
.d_node
->getType() == rule
.d_node
->getType())
4378 << "Expected ntSymbol and rule to have the same sort";
4379 CVC5_API_ARG_CHECK_EXPECTED(!containsFreeVariables(rule
), rule
)
4380 << "a term whose free variables are limited to synthFun/synthInv "
4381 "parameters and non-terminal symbols of the grammar";
4382 //////// all checks before this line
4383 d_ntsToTerms
[ntSymbol
].push_back(rule
);
4385 CVC5_API_TRY_CATCH_END
;
4388 void Grammar::addRules(const Term
& ntSymbol
, const std::vector
<Term
>& rules
)
4390 CVC5_API_TRY_CATCH_BEGIN
;
4391 CVC5_API_CHECK(!d_isResolved
) << "Grammar cannot be modified after passing "
4392 "it as an argument to synthFun/synthInv";
4393 CVC5_API_CHECK_TERM(ntSymbol
);
4394 CVC5_API_CHECK_TERMS_WITH_SORT(rules
, ntSymbol
.getSort());
4395 CVC5_API_ARG_CHECK_EXPECTED(
4396 d_ntsToTerms
.find(ntSymbol
) != d_ntsToTerms
.cend(), ntSymbol
)
4397 << "ntSymbol to be one of the non-terminal symbols given in the "
4399 for (size_t i
= 0, n
= rules
.size(); i
< n
; ++i
)
4401 CVC5_API_ARG_AT_INDEX_CHECK_EXPECTED(
4402 !containsFreeVariables(rules
[i
]), rules
[i
], rules
, i
)
4403 << "a term whose free variables are limited to synthFun/synthInv "
4404 "parameters and non-terminal symbols of the grammar";
4406 //////// all checks before this line
4407 d_ntsToTerms
[ntSymbol
].insert(
4408 d_ntsToTerms
[ntSymbol
].cend(), rules
.cbegin(), rules
.cend());
4410 CVC5_API_TRY_CATCH_END
;
4413 void Grammar::addAnyConstant(const Term
& ntSymbol
)
4415 CVC5_API_TRY_CATCH_BEGIN
;
4416 CVC5_API_CHECK(!d_isResolved
) << "Grammar cannot be modified after passing "
4417 "it as an argument to synthFun/synthInv";
4418 CVC5_API_CHECK_TERM(ntSymbol
);
4419 CVC5_API_ARG_CHECK_EXPECTED(
4420 d_ntsToTerms
.find(ntSymbol
) != d_ntsToTerms
.cend(), ntSymbol
)
4421 << "ntSymbol to be one of the non-terminal symbols given in the "
4423 //////// all checks before this line
4424 d_allowConst
.insert(ntSymbol
);
4426 CVC5_API_TRY_CATCH_END
;
4429 void Grammar::addAnyVariable(const Term
& ntSymbol
)
4431 CVC5_API_TRY_CATCH_BEGIN
;
4432 CVC5_API_CHECK(!d_isResolved
) << "Grammar cannot be modified after passing "
4433 "it as an argument to synthFun/synthInv";
4434 CVC5_API_CHECK_TERM(ntSymbol
);
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 //////// all checks before this line
4440 d_allowVars
.insert(ntSymbol
);
4442 CVC5_API_TRY_CATCH_END
;
4446 * This function concatenates the outputs of calling f on each element between
4447 * first and last, seperated by sep.
4448 * @param first the beginning of the range
4449 * @param last the end of the range
4450 * @param f the function to call on each element in the range, its output must
4451 * be overloaded for operator<<
4452 * @param sep the string to add between successive calls to f
4454 template <typename Iterator
, typename Function
>
4455 std::string
join(Iterator first
, Iterator last
, Function f
, std::string sep
)
4457 std::stringstream ss
;
4475 std::string
Grammar::toString() const
4477 CVC5_API_TRY_CATCH_BEGIN
;
4478 //////// all checks before this line
4479 std::stringstream ss
;
4480 ss
<< " (" // pre-declaration
4485 std::stringstream s
;
4486 s
<< '(' << t
<< ' ' << t
.getSort() << ')';
4490 << ")\n (" // grouped rule listing
4494 [this](const Term
& t
) {
4495 bool allowConst
= d_allowConst
.find(t
) != d_allowConst
.cend(),
4496 allowVars
= d_allowVars
.find(t
) != d_allowVars
.cend();
4497 const std::vector
<Term
>& rules
= d_ntsToTerms
.at(t
);
4498 std::stringstream s
;
4499 s
<< '(' << t
<< ' ' << t
.getSort() << " ("
4500 << (allowConst
? "(Constant " + t
.getSort().toString() + ")"
4502 << (allowConst
&& allowVars
? " " : "")
4503 << (allowVars
? "(Var " + t
.getSort().toString() + ")" : "")
4504 << ((allowConst
|| allowVars
) && !rules
.empty() ? " " : "")
4508 [](const Term
& rule
) { return rule
.toString(); },
4518 CVC5_API_TRY_CATCH_END
;
4521 Sort
Grammar::resolve()
4523 CVC5_API_TRY_CATCH_BEGIN
;
4524 //////// all checks before this line
4526 d_isResolved
= true;
4530 if (!d_sygusVars
.empty())
4534 d_solver
->getNodeManager()->mkNode(
4535 cvc5::kind::BOUND_VAR_LIST
, Term::termVectorToNodes(d_sygusVars
)));
4538 std::unordered_map
<Term
, Sort
> ntsToUnres(d_ntSyms
.size());
4540 for (Term ntsymbol
: d_ntSyms
)
4542 // make the unresolved type, used for referencing the final version of
4543 // the ntsymbol's datatype
4544 ntsToUnres
[ntsymbol
] =
4545 Sort(d_solver
, d_solver
->getNodeManager()->mkSort(ntsymbol
.toString()));
4548 std::vector
<cvc5::DType
> datatypes
;
4549 std::set
<TypeNode
> unresTypes
;
4551 datatypes
.reserve(d_ntSyms
.size());
4553 for (const Term
& ntSym
: d_ntSyms
)
4555 // make the datatype, which encodes terms generated by this non-terminal
4556 DatatypeDecl
dtDecl(d_solver
, ntSym
.toString());
4558 for (const Term
& consTerm
: d_ntsToTerms
[ntSym
])
4560 addSygusConstructorTerm(dtDecl
, consTerm
, ntsToUnres
);
4563 if (d_allowVars
.find(ntSym
) != d_allowVars
.cend())
4565 addSygusConstructorVariables(dtDecl
,
4566 Sort(d_solver
, ntSym
.d_node
->getType()));
4569 bool aci
= d_allowConst
.find(ntSym
) != d_allowConst
.end();
4570 TypeNode btt
= ntSym
.d_node
->getType();
4571 dtDecl
.d_dtype
->setSygus(btt
, *bvl
.d_node
, aci
, false);
4573 // We can be in a case where the only rule specified was (Variable T)
4574 // and there are no variables of type T, in which case this is a bogus
4575 // grammar. This results in the error below.
4576 CVC5_API_CHECK(dtDecl
.d_dtype
->getNumConstructors() != 0)
4577 << "Grouped rule listing for " << *dtDecl
.d_dtype
4578 << " produced an empty rule list";
4580 datatypes
.push_back(*dtDecl
.d_dtype
);
4581 unresTypes
.insert(*ntsToUnres
[ntSym
].d_type
);
4584 std::vector
<TypeNode
> datatypeTypes
=
4585 d_solver
->getNodeManager()->mkMutualDatatypeTypes(
4586 datatypes
, unresTypes
, NodeManager::DATATYPE_FLAG_PLACEHOLDER
);
4588 // return is the first datatype
4589 return Sort(d_solver
, datatypeTypes
[0]);
4591 CVC5_API_TRY_CATCH_END
;
4594 void Grammar::addSygusConstructorTerm(
4597 const std::unordered_map
<Term
, Sort
>& ntsToUnres
) const
4599 CVC5_API_TRY_CATCH_BEGIN
;
4600 CVC5_API_CHECK_DTDECL(dt
);
4601 CVC5_API_CHECK_TERM(term
);
4602 CVC5_API_CHECK_TERMS_MAP(ntsToUnres
);
4603 //////// all checks before this line
4605 // At this point, we should know that dt is well founded, and that its
4606 // builtin sygus operators are well-typed.
4607 // Now, purify each occurrence of a non-terminal symbol in term, replace by
4608 // free variables. These become arguments to constructors. Notice we must do
4609 // a tree traversal in this function, since unique paths to the same term
4610 // should be treated as distinct terms.
4611 // Notice that let expressions are forbidden in the input syntax of term, so
4612 // this does not lead to exponential behavior with respect to input size.
4613 std::vector
<Term
> args
;
4614 std::vector
<Sort
> cargs
;
4615 Term op
= purifySygusGTerm(term
, args
, cargs
, ntsToUnres
);
4616 std::stringstream ssCName
;
4617 ssCName
<< op
.getKind();
4622 d_solver
->getNodeManager()->mkNode(cvc5::kind::BOUND_VAR_LIST
,
4623 Term::termVectorToNodes(args
)));
4624 // its operator is a lambda
4626 d_solver
->getNodeManager()->mkNode(
4627 cvc5::kind::LAMBDA
, *lbvl
.d_node
, *op
.d_node
));
4629 std::vector
<TypeNode
> cargst
= Sort::sortVectorToTypeNodes(cargs
);
4630 dt
.d_dtype
->addSygusConstructor(*op
.d_node
, ssCName
.str(), cargst
);
4632 CVC5_API_TRY_CATCH_END
;
4635 Term
Grammar::purifySygusGTerm(
4637 std::vector
<Term
>& args
,
4638 std::vector
<Sort
>& cargs
,
4639 const std::unordered_map
<Term
, Sort
>& ntsToUnres
) const
4641 CVC5_API_TRY_CATCH_BEGIN
;
4642 CVC5_API_CHECK_TERM(term
);
4643 CVC5_API_CHECK_TERMS(args
);
4644 CVC5_API_CHECK_SORTS(cargs
);
4645 CVC5_API_CHECK_TERMS_MAP(ntsToUnres
);
4646 //////// all checks before this line
4648 std::unordered_map
<Term
, Sort
>::const_iterator itn
= ntsToUnres
.find(term
);
4649 if (itn
!= ntsToUnres
.cend())
4653 d_solver
->getNodeManager()->mkBoundVar(term
.d_node
->getType()));
4654 args
.push_back(ret
);
4655 cargs
.push_back(itn
->second
);
4658 std::vector
<Term
> pchildren
;
4659 bool childChanged
= false;
4660 for (unsigned i
= 0, nchild
= term
.d_node
->getNumChildren(); i
< nchild
; i
++)
4662 Term ptermc
= purifySygusGTerm(
4663 Term(d_solver
, (*term
.d_node
)[i
]), args
, cargs
, ntsToUnres
);
4664 pchildren
.push_back(ptermc
);
4665 childChanged
= childChanged
|| *ptermc
.d_node
!= (*term
.d_node
)[i
];
4674 if (term
.d_node
->getMetaKind() == kind::metakind::PARAMETERIZED
)
4676 // it's an indexed operator so we should provide the op
4677 NodeBuilder
nb(term
.d_node
->getKind());
4678 nb
<< term
.d_node
->getOperator();
4679 nb
.append(Term::termVectorToNodes(pchildren
));
4680 nret
= nb
.constructNode();
4684 nret
= d_solver
->getNodeManager()->mkNode(
4685 term
.d_node
->getKind(), Term::termVectorToNodes(pchildren
));
4688 return Term(d_solver
, nret
);
4690 CVC5_API_TRY_CATCH_END
;
4693 void Grammar::addSygusConstructorVariables(DatatypeDecl
& dt
,
4694 const Sort
& sort
) const
4696 CVC5_API_TRY_CATCH_BEGIN
;
4697 CVC5_API_CHECK_DTDECL(dt
);
4698 CVC5_API_CHECK_SORT(sort
);
4699 //////// all checks before this line
4701 // each variable of appropriate type becomes a sygus constructor in dt.
4702 for (unsigned i
= 0, size
= d_sygusVars
.size(); i
< size
; i
++)
4704 Term v
= d_sygusVars
[i
];
4705 if (v
.d_node
->getType() == *sort
.d_type
)
4707 std::stringstream ss
;
4709 std::vector
<TypeNode
> cargs
;
4710 dt
.d_dtype
->addSygusConstructor(*v
.d_node
, ss
.str(), cargs
);
4714 CVC5_API_TRY_CATCH_END
;
4717 bool Grammar::containsFreeVariables(const Term
& rule
) const
4719 // we allow the argument list and non-terminal symbols to be in scope
4720 std::unordered_set
<TNode
> scope
;
4722 for (const Term
& sygusVar
: d_sygusVars
)
4724 scope
.emplace(*sygusVar
.d_node
);
4727 for (const Term
& ntsymbol
: d_ntSyms
)
4729 scope
.emplace(*ntsymbol
.d_node
);
4732 return expr::hasFreeVariablesScope(*rule
.d_node
, scope
);
4735 std::ostream
& operator<<(std::ostream
& out
, const Grammar
& grammar
)
4737 return out
<< grammar
.toString();
4740 /* -------------------------------------------------------------------------- */
4741 /* Rounding Mode for Floating Points */
4742 /* -------------------------------------------------------------------------- */
4744 const static std::unordered_map
<RoundingMode
, cvc5::RoundingMode
> s_rmodes
{
4745 {ROUND_NEAREST_TIES_TO_EVEN
,
4746 cvc5::RoundingMode::ROUND_NEAREST_TIES_TO_EVEN
},
4747 {ROUND_TOWARD_POSITIVE
, cvc5::RoundingMode::ROUND_TOWARD_POSITIVE
},
4748 {ROUND_TOWARD_NEGATIVE
, cvc5::RoundingMode::ROUND_TOWARD_NEGATIVE
},
4749 {ROUND_TOWARD_ZERO
, cvc5::RoundingMode::ROUND_TOWARD_ZERO
},
4750 {ROUND_NEAREST_TIES_TO_AWAY
,
4751 cvc5::RoundingMode::ROUND_NEAREST_TIES_TO_AWAY
},
4754 const static std::unordered_map
<cvc5::RoundingMode
,
4756 cvc5::RoundingModeHashFunction
>
4758 {cvc5::RoundingMode::ROUND_NEAREST_TIES_TO_EVEN
,
4759 ROUND_NEAREST_TIES_TO_EVEN
},
4760 {cvc5::RoundingMode::ROUND_TOWARD_POSITIVE
, ROUND_TOWARD_POSITIVE
},
4761 {cvc5::RoundingMode::ROUND_TOWARD_POSITIVE
, ROUND_TOWARD_NEGATIVE
},
4762 {cvc5::RoundingMode::ROUND_TOWARD_ZERO
, ROUND_TOWARD_ZERO
},
4763 {cvc5::RoundingMode::ROUND_NEAREST_TIES_TO_AWAY
,
4764 ROUND_NEAREST_TIES_TO_AWAY
},
4767 /* -------------------------------------------------------------------------- */
4769 /* -------------------------------------------------------------------------- */
4771 DriverOptions::DriverOptions(const Solver
& solver
) : d_solver(solver
) {}
4773 std::istream
& DriverOptions::in() const
4775 return *d_solver
.d_slv
->getOptions().base
.in
;
4777 std::ostream
& DriverOptions::err() const
4779 return *d_solver
.d_slv
->getOptions().base
.err
;
4781 std::ostream
& DriverOptions::out() const
4783 return *d_solver
.d_slv
->getOptions().base
.out
;
4786 /* -------------------------------------------------------------------------- */
4788 /* -------------------------------------------------------------------------- */
4790 struct Stat::StatData
4792 cvc5::StatExportData data
;
4793 template <typename T
>
4794 StatData(T
&& t
) : data(std::forward
<T
>(t
))
4797 StatData() : data() {}
4801 Stat::Stat(const Stat
& s
)
4802 : d_expert(s
.d_expert
),
4803 d_default(s
.d_default
),
4804 d_data(std::make_unique
<StatData
>(s
.d_data
->data
))
4807 Stat
& Stat::operator=(const Stat
& s
)
4809 d_expert
= s
.d_expert
;
4810 d_data
= std::make_unique
<StatData
>(s
.d_data
->data
);
4814 bool Stat::isExpert() const { return d_expert
; }
4815 bool Stat::isDefault() const { return d_default
; }
4817 bool Stat::isInt() const
4819 return std::holds_alternative
<int64_t>(d_data
->data
);
4821 int64_t Stat::getInt() const
4823 CVC5_API_TRY_CATCH_BEGIN
;
4824 CVC5_API_RECOVERABLE_CHECK(isInt()) << "Expected Stat of type int64_t.";
4825 return std::get
<int64_t>(d_data
->data
);
4826 CVC5_API_TRY_CATCH_END
;
4828 bool Stat::isDouble() const
4830 return std::holds_alternative
<double>(d_data
->data
);
4832 double Stat::getDouble() const
4834 CVC5_API_TRY_CATCH_BEGIN
;
4835 CVC5_API_RECOVERABLE_CHECK(isDouble()) << "Expected Stat of type double.";
4836 return std::get
<double>(d_data
->data
);
4837 CVC5_API_TRY_CATCH_END
;
4839 bool Stat::isString() const
4841 return std::holds_alternative
<std::string
>(d_data
->data
);
4843 const std::string
& Stat::getString() const
4845 CVC5_API_TRY_CATCH_BEGIN
;
4846 CVC5_API_RECOVERABLE_CHECK(isString())
4847 << "Expected Stat of type std::string.";
4848 return std::get
<std::string
>(d_data
->data
);
4849 CVC5_API_TRY_CATCH_END
;
4851 bool Stat::isHistogram() const
4853 return std::holds_alternative
<HistogramData
>(d_data
->data
);
4855 const Stat::HistogramData
& Stat::getHistogram() const
4857 CVC5_API_TRY_CATCH_BEGIN
;
4858 CVC5_API_RECOVERABLE_CHECK(isHistogram())
4859 << "Expected Stat of type histogram.";
4860 return std::get
<HistogramData
>(d_data
->data
);
4861 CVC5_API_TRY_CATCH_END
;
4864 Stat::Stat(bool expert
, bool defaulted
, StatData
&& sd
)
4866 d_default(defaulted
),
4867 d_data(std::make_unique
<StatData
>(std::move(sd
)))
4871 std::ostream
& operator<<(std::ostream
& os
, const Stat
& sv
)
4873 return cvc5::detail::print(os
, sv
.d_data
->data
);
4876 Statistics::BaseType::const_reference
Statistics::iterator::operator*() const
4878 return d_it
.operator*();
4880 Statistics::BaseType::const_pointer
Statistics::iterator::operator->() const
4882 return d_it
.operator->();
4884 Statistics::iterator
& Statistics::iterator::operator++()
4889 } while (!isVisible());
4892 Statistics::iterator
Statistics::iterator::operator++(int)
4894 iterator tmp
= *this;
4898 } while (!isVisible());
4901 Statistics::iterator
& Statistics::iterator::operator--()
4906 } while (!isVisible());
4909 Statistics::iterator
Statistics::iterator::operator--(int)
4911 iterator tmp
= *this;
4915 } while (!isVisible());
4918 bool Statistics::iterator::operator==(const Statistics::iterator
& rhs
) const
4920 return d_it
== rhs
.d_it
;
4922 bool Statistics::iterator::operator!=(const Statistics::iterator
& rhs
) const
4924 return d_it
!= rhs
.d_it
;
4926 Statistics::iterator::iterator(Statistics::BaseType::const_iterator it
,
4927 const Statistics::BaseType
& base
,
4930 : d_it(it
), d_base(&base
), d_showExpert(expert
), d_showDefault(defaulted
)
4932 while (!isVisible())
4937 bool Statistics::iterator::isVisible() const
4939 if (d_it
== d_base
->end()) return true;
4940 if (!d_showExpert
&& d_it
->second
.isExpert()) return false;
4941 if (!d_showDefault
&& d_it
->second
.isDefault()) return false;
4945 const Stat
& Statistics::get(const std::string
& name
)
4947 CVC5_API_TRY_CATCH_BEGIN
;
4948 auto it
= d_stats
.find(name
);
4949 CVC5_API_RECOVERABLE_CHECK(it
!= d_stats
.end())
4950 << "No stat with name \"" << name
<< "\" exists.";
4952 CVC5_API_TRY_CATCH_END
;
4955 Statistics::iterator
Statistics::begin(bool expert
, bool defaulted
) const
4957 return iterator(d_stats
.begin(), d_stats
, expert
, defaulted
);
4959 Statistics::iterator
Statistics::end() const
4961 return iterator(d_stats
.end(), d_stats
, false, false);
4964 Statistics::Statistics(const StatisticsRegistry
& reg
)
4966 for (const auto& svp
: reg
)
4968 d_stats
.emplace(svp
.first
,
4969 Stat(svp
.second
->d_expert
,
4970 svp
.second
->isDefault(),
4971 svp
.second
->getViewer()));
4975 std::ostream
& operator<<(std::ostream
& out
, const Statistics
& stats
)
4977 for (const auto& stat
: stats
)
4979 out
<< stat
.first
<< " = " << stat
.second
<< std::endl
;
4984 /* -------------------------------------------------------------------------- */
4986 /* -------------------------------------------------------------------------- */
4988 Solver::Solver(std::unique_ptr
<Options
>&& original
)
4990 d_nodeMgr
= NodeManager::currentNM();
4992 d_originalOptions
= std::move(original
);
4993 d_slv
.reset(new SolverEngine(d_nodeMgr
, d_originalOptions
.get()));
4994 d_slv
->setSolver(this);
4995 d_rng
.reset(new Random(d_slv
->getOptions().driver
.seed
));
4999 Solver::Solver() : Solver(std::make_unique
<Options
>()) {}
5001 Solver::~Solver() {}
5003 /* Helpers and private functions */
5004 /* -------------------------------------------------------------------------- */
5006 NodeManager
* Solver::getNodeManager(void) const { return d_nodeMgr
; }
5008 void Solver::increment_term_stats(Kind kind
) const
5010 if constexpr (configuration::isStatisticsBuild())
5012 d_stats
->d_terms
<< kind
;
5016 void Solver::increment_vars_consts_stats(const Sort
& sort
, bool is_var
) const
5018 if constexpr (configuration::isStatisticsBuild())
5020 const TypeNode tn
= sort
.getTypeNode();
5021 TypeConstant tc
= tn
.getKind() == cvc5::kind::TYPE_CONSTANT
5022 ? tn
.getConst
<TypeConstant
>()
5026 d_stats
->d_vars
<< tc
;
5030 d_stats
->d_consts
<< tc
;
5035 /* Split out to avoid nested API calls (problematic with API tracing). */
5036 /* .......................................................................... */
5038 template <typename T
>
5039 Term
Solver::mkValHelper(const T
& t
) const
5041 //////// all checks before this line
5042 Node res
= getNodeManager()->mkConst(t
);
5043 (void)res
.getType(true); /* kick off type checking */
5044 return Term(this, res
);
5047 Term
Solver::mkRationalValHelper(const Rational
& r
, bool isInt
) const
5049 //////// all checks before this line
5050 NodeManager
* nm
= getNodeManager();
5051 Node res
= isInt
? nm
->mkConstInt(r
) : nm
->mkConstReal(r
);
5052 (void)res
.getType(true); /* kick off type checking */
5053 api::Term t
= Term(this, res
);
5054 // NOTE: this block will be eliminated when arithmetic subtyping is eliminated
5057 t
= ensureRealSort(t
);
5062 Term
Solver::mkRealOrIntegerFromStrHelper(const std::string
& s
,
5065 //////// all checks before this line
5068 cvc5::Rational r
= s
.find('/') != std::string::npos
5070 : cvc5::Rational::fromDecimal(s
);
5071 return mkRationalValHelper(r
, isInt
);
5073 catch (const std::invalid_argument
& e
)
5075 /* Catch to throw with a more meaningful error message. To be caught in
5076 * enclosing CVC5_API_TRY_CATCH_* block to throw CVC5ApiException. */
5077 std::stringstream message
;
5078 message
<< "Cannot construct Real or Int from string argument '" << s
<< "'"
5080 throw std::invalid_argument(message
.str());
5084 Term
Solver::mkBVFromIntHelper(uint32_t size
, uint64_t val
) const
5086 CVC5_API_ARG_CHECK_EXPECTED(size
> 0, size
) << "a bit-width > 0";
5087 //////// all checks before this line
5088 return mkValHelper
<cvc5::BitVector
>(cvc5::BitVector(size
, val
));
5091 Term
Solver::mkBVFromStrHelper(uint32_t size
,
5092 const std::string
& s
,
5093 uint32_t base
) const
5095 CVC5_API_ARG_CHECK_EXPECTED(size
> 0, size
) << "a bit-width > 0";
5096 CVC5_API_ARG_CHECK_EXPECTED(!s
.empty(), s
) << "a non-empty string";
5097 CVC5_API_ARG_CHECK_EXPECTED(base
== 2 || base
== 10 || base
== 16, base
)
5098 << "base 2, 10, or 16";
5099 //////// all checks before this line
5101 Integer
val(s
, base
);
5103 if (val
.strictlyNegative())
5105 CVC5_API_CHECK(val
>= -Integer(2).pow(size
- 1))
5106 << "Overflow in bitvector construction (specified bitvector size "
5107 << size
<< " too small to hold value " << s
<< ")";
5111 CVC5_API_CHECK(val
.modByPow2(size
) == val
)
5112 << "Overflow in bitvector construction (specified bitvector size "
5113 << size
<< " too small to hold value " << s
<< ")";
5115 return mkValHelper
<cvc5::BitVector
>(cvc5::BitVector(size
, val
));
5118 Term
Solver::getValueHelper(const Term
& term
) const
5120 // Note: Term is checked in the caller to avoid double checks
5121 bool wasShadow
= false;
5122 bool freeOrShadowedVar
=
5123 expr::hasFreeOrShadowedVar(term
.getNode(), wasShadow
);
5124 CVC5_API_RECOVERABLE_CHECK(!freeOrShadowedVar
)
5125 << "Cannot get value of term containing "
5126 << (wasShadow
? "shadowed" : "free") << " variables";
5127 //////// all checks before this line
5128 Node value
= d_slv
->getValue(*term
.d_node
);
5129 Term res
= Term(this, value
);
5130 // May need to wrap in real cast so that user know this is a real.
5131 TypeNode tn
= (*term
.d_node
).getType();
5132 if (!tn
.isInteger() && value
.getType().isInteger())
5134 return ensureRealSort(res
);
5139 Sort
Solver::mkTupleSortHelper(const std::vector
<Sort
>& sorts
) const
5141 // Note: Sorts are checked in the caller to avoid double checks
5142 //////// all checks before this line
5143 std::vector
<TypeNode
> typeNodes
= Sort::sortVectorToTypeNodes(sorts
);
5144 return Sort(this, getNodeManager()->mkTupleType(typeNodes
));
5147 Term
Solver::mkTermFromKind(Kind kind
) const
5149 CVC5_API_KIND_CHECK_EXPECTED(kind
== PI
|| kind
== REGEXP_NONE
5150 || kind
== REGEXP_ALLCHAR
|| kind
== SEP_EMP
,
5152 << "PI, REGEXP_NONE, REGEXP_ALLCHAR or SEP_EMP";
5153 //////// all checks before this line
5155 cvc5::Kind k
= extToIntKind(kind
);
5156 if (kind
== REGEXP_NONE
|| kind
== REGEXP_ALLCHAR
)
5158 Assert(isDefinedIntKind(k
));
5159 res
= d_nodeMgr
->mkNode(k
, std::vector
<Node
>());
5161 else if (kind
== SEP_EMP
)
5163 res
= d_nodeMgr
->mkNullaryOperator(d_nodeMgr
->booleanType(), k
);
5168 res
= d_nodeMgr
->mkNullaryOperator(d_nodeMgr
->realType(), k
);
5170 (void)res
.getType(true); /* kick off type checking */
5171 increment_term_stats(kind
);
5172 return Term(this, res
);
5175 Term
Solver::mkTermHelper(Kind kind
, const std::vector
<Term
>& children
) const
5177 // Note: Kind and children are checked in the caller to avoid double checks
5178 //////// all checks before this line
5179 if (children
.size() == 0)
5181 return mkTermFromKind(kind
);
5183 std::vector
<Node
> echildren
= Term::termVectorToNodes(children
);
5184 cvc5::Kind k
= extToIntKind(kind
);
5186 if (echildren
.size() > 2)
5188 if (kind
== INTS_DIVISION
|| kind
== XOR
|| kind
== MINUS
5189 || kind
== DIVISION
|| kind
== HO_APPLY
|| kind
== REGEXP_DIFF
)
5191 // left-associative, but cvc5 internally only supports 2 args
5192 res
= d_nodeMgr
->mkLeftAssociative(k
, echildren
);
5194 else if (kind
== IMPLIES
)
5196 // right-associative, but cvc5 internally only supports 2 args
5197 res
= d_nodeMgr
->mkRightAssociative(k
, echildren
);
5199 else if (kind
== EQUAL
|| kind
== LT
|| kind
== GT
|| kind
== LEQ
5202 // "chainable", but cvc5 internally only supports 2 args
5203 res
= d_nodeMgr
->mkChain(k
, echildren
);
5205 else if (kind::isAssociative(k
))
5207 // mkAssociative has special treatment for associative operators with lots
5209 res
= d_nodeMgr
->mkAssociative(k
, echildren
);
5213 // default case, must check kind
5214 checkMkTerm(kind
, children
.size());
5215 res
= d_nodeMgr
->mkNode(k
, echildren
);
5218 else if (kind::isAssociative(k
))
5220 // associative case, same as above
5221 checkMkTerm(kind
, children
.size());
5222 res
= d_nodeMgr
->mkAssociative(k
, echildren
);
5226 // default case, same as above
5227 checkMkTerm(kind
, children
.size());
5228 if (kind
== api::SET_SINGLETON
)
5230 // the type of the term is the same as the type of the internal node
5231 // see Term::getSort()
5232 TypeNode type
= children
[0].d_node
->getType();
5233 // Internally NodeManager::mkSingleton needs a type argument
5234 // to construct a singleton, since there is no difference between
5235 // integers and reals (both are Rationals).
5236 // At the API, mkReal and mkInteger are different and therefore the
5237 // element type can be used safely here.
5238 res
= getNodeManager()->mkSingleton(type
, *children
[0].d_node
);
5240 else if (kind
== api::BAG_MAKE
)
5242 // the type of the term is the same as the type of the internal node
5243 // see Term::getSort()
5244 TypeNode type
= children
[0].d_node
->getType();
5245 // Internally NodeManager::mkBag needs a type argument
5246 // to construct a bag, since there is no difference between
5247 // integers and reals (both are Rationals).
5248 // At the API, mkReal and mkInteger are different and therefore the
5249 // element type can be used safely here.
5250 res
= getNodeManager()->mkBag(
5251 type
, *children
[0].d_node
, *children
[1].d_node
);
5255 res
= d_nodeMgr
->mkNode(k
, echildren
);
5259 (void)res
.getType(true); /* kick off type checking */
5260 increment_term_stats(kind
);
5261 return Term(this, res
);
5264 Term
Solver::mkTermHelper(const Op
& op
, const std::vector
<Term
>& children
) const
5266 if (!op
.isIndexedHelper())
5268 return mkTermHelper(op
.d_kind
, children
);
5271 // Note: Op and children are checked in the caller to avoid double checks
5272 checkMkTerm(op
.d_kind
, children
.size());
5273 //////// all checks before this line
5275 const cvc5::Kind int_kind
= extToIntKind(op
.d_kind
);
5276 std::vector
<Node
> echildren
= Term::termVectorToNodes(children
);
5278 NodeBuilder
nb(int_kind
);
5280 nb
.append(echildren
);
5281 Node res
= nb
.constructNode();
5283 (void)res
.getType(true); /* kick off type checking */
5284 return Term(this, res
);
5287 std::vector
<Sort
> Solver::mkDatatypeSortsInternal(
5288 const std::vector
<DatatypeDecl
>& dtypedecls
,
5289 const std::set
<Sort
>& unresolvedSorts
) const
5291 // Note: dtypedecls and unresolvedSorts are checked in the caller to avoid
5293 //////// all checks before this line
5295 std::vector
<cvc5::DType
> datatypes
;
5296 for (size_t i
= 0, ndts
= dtypedecls
.size(); i
< ndts
; ++i
)
5298 datatypes
.push_back(dtypedecls
[i
].getDatatype());
5301 std::set
<TypeNode
> utypes
= Sort::sortSetToTypeNodes(unresolvedSorts
);
5302 std::vector
<cvc5::TypeNode
> dtypes
=
5303 getNodeManager()->mkMutualDatatypeTypes(datatypes
, utypes
);
5304 std::vector
<Sort
> retTypes
= Sort::typeNodeVectorToSorts(this, dtypes
);
5308 Term
Solver::synthFunHelper(const std::string
& symbol
,
5309 const std::vector
<Term
>& boundVars
,
5312 Grammar
* grammar
) const
5314 // Note: boundVars, sort and grammar are checked in the caller to avoid
5316 std::vector
<TypeNode
> varTypes
;
5317 for (const auto& bv
: boundVars
)
5321 CVC5_API_CHECK(grammar
->d_ntSyms
[0].d_node
->getType() == *sort
.d_type
)
5322 << "Invalid Start symbol for grammar, Expected Start's sort to be "
5323 << *sort
.d_type
<< " but found "
5324 << grammar
->d_ntSyms
[0].d_node
->getType();
5326 varTypes
.push_back(bv
.d_node
->getType());
5328 //////// all checks before this line
5330 TypeNode funType
= varTypes
.empty() ? *sort
.d_type
5331 : getNodeManager()->mkFunctionType(
5332 varTypes
, *sort
.d_type
);
5334 Node fun
= getNodeManager()->mkBoundVar(symbol
, funType
);
5335 (void)fun
.getType(true); /* kick off type checking */
5337 std::vector
<Node
> bvns
= Term::termVectorToNodes(boundVars
);
5339 d_slv
->declareSynthFun(
5341 grammar
== nullptr ? funType
: *grammar
->resolve().d_type
,
5345 return Term(this, fun
);
5348 Term
Solver::ensureTermSort(const Term
& term
, const Sort
& sort
) const
5350 // Note: Term and sort are checked in the caller to avoid double checks
5351 CVC5_API_CHECK(term
.getSort() == sort
5352 || (term
.getSort().isInteger() && sort
.isReal()))
5353 << "Expected conversion from Int to Real";
5354 //////// all checks before this line
5356 Sort t
= term
.getSort();
5357 if (term
.getSort() == sort
)
5362 // Integers are reals, too
5363 Assert(t
.d_type
->isReal());
5367 // Must cast to Real to ensure correct type is passed to parametric type
5368 // constructors. We do this cast using division with 1. This has the
5369 // advantage wrt using TO_REAL since (constant) division is always included
5372 d_nodeMgr
->mkNode(extToIntKind(DIVISION
),
5374 d_nodeMgr
->mkConst(kind::CONST_RATIONAL
,
5375 cvc5::Rational(1))));
5377 Assert(res
.getSort() == sort
);
5381 Term
Solver::ensureRealSort(const Term
& t
) const
5383 Assert(this == t
.d_solver
);
5384 CVC5_API_ARG_CHECK_EXPECTED(
5385 t
.getSort() == getIntegerSort() || t
.getSort() == getRealSort(),
5386 " an integer or real term");
5387 // Note: Term is checked in the caller to avoid double checks
5388 //////// all checks before this line
5389 if (t
.getSort() == getIntegerSort())
5391 Node n
= getNodeManager()->mkNode(kind::CAST_TO_REAL
, *t
.d_node
);
5392 return Term(this, n
);
5397 bool Solver::isValidInteger(const std::string
& s
) const
5399 //////// all checks before this line
5400 if (s
.length() == 0)
5402 // string should not be empty
5407 if (s
[index
] == '-')
5409 if (s
.length() == 1)
5411 // negative integers should contain at least one digit
5417 if (s
[index
] == '0' && s
.length() > (index
+ 1))
5419 // From SMT-Lib 2.6: A <numeral> is the digit 0 or a non-empty sequence of
5420 // digits not starting with 0. So integers like 001, 000 are not allowed
5424 // all remaining characters should be decimal digits
5425 for (; index
< s
.length(); ++index
)
5427 if (!std::isdigit(s
[index
]))
5436 void Solver::resetStatistics()
5438 if constexpr (configuration::isStatisticsBuild())
5440 d_stats
.reset(new APIStatistics
{
5441 d_slv
->getStatisticsRegistry().registerHistogram
<TypeConstant
>(
5443 d_slv
->getStatisticsRegistry().registerHistogram
<TypeConstant
>(
5445 d_slv
->getStatisticsRegistry().registerHistogram
<Kind
>("api::TERM"),
5450 void Solver::printStatisticsSafe(int fd
) const
5452 d_slv
->printStatisticsSafe(fd
);
5455 /* Helpers for mkTerm checks. */
5456 /* .......................................................................... */
5458 void Solver::checkMkTerm(Kind kind
, uint32_t nchildren
) const
5460 CVC5_API_KIND_CHECK(kind
);
5461 Assert(isDefinedIntKind(extToIntKind(kind
)));
5462 const cvc5::kind::MetaKind mk
= kind::metaKindOf(extToIntKind(kind
));
5463 CVC5_API_KIND_CHECK_EXPECTED(
5464 mk
== kind::metakind::PARAMETERIZED
|| mk
== kind::metakind::OPERATOR
,
5466 << "Only operator-style terms are created with mkTerm(), "
5467 "to create variables, constants and values see mkVar(), mkConst() "
5468 "and the respective theory-specific functions to create values, "
5469 "e.g., mkBitVector().";
5470 CVC5_API_KIND_CHECK_EXPECTED(
5471 nchildren
>= minArity(kind
) && nchildren
<= maxArity(kind
), kind
)
5472 << "Terms with kind " << kindToString(kind
) << " must have at least "
5473 << minArity(kind
) << " children and at most " << maxArity(kind
)
5474 << " children (the one under construction has " << nchildren
<< ")";
5477 /* Sorts Handling */
5478 /* -------------------------------------------------------------------------- */
5480 Sort
Solver::getNullSort(void) const
5482 CVC5_API_TRY_CATCH_BEGIN
;
5483 //////// all checks before this line
5484 return Sort(this, TypeNode());
5486 CVC5_API_TRY_CATCH_END
;
5489 Sort
Solver::getBooleanSort(void) const
5491 CVC5_API_TRY_CATCH_BEGIN
;
5492 //////// all checks before this line
5493 return Sort(this, getNodeManager()->booleanType());
5495 CVC5_API_TRY_CATCH_END
;
5498 Sort
Solver::getIntegerSort(void) const
5500 CVC5_API_TRY_CATCH_BEGIN
;
5501 //////// all checks before this line
5502 return Sort(this, getNodeManager()->integerType());
5504 CVC5_API_TRY_CATCH_END
;
5507 Sort
Solver::getRealSort(void) const
5509 CVC5_API_TRY_CATCH_BEGIN
;
5510 //////// all checks before this line
5511 return Sort(this, getNodeManager()->realType());
5513 CVC5_API_TRY_CATCH_END
;
5516 Sort
Solver::getRegExpSort(void) const
5518 CVC5_API_TRY_CATCH_BEGIN
;
5519 //////// all checks before this line
5520 return Sort(this, getNodeManager()->regExpType());
5522 CVC5_API_TRY_CATCH_END
;
5525 Sort
Solver::getStringSort(void) const
5527 CVC5_API_TRY_CATCH_BEGIN
;
5528 //////// all checks before this line
5529 return Sort(this, getNodeManager()->stringType());
5531 CVC5_API_TRY_CATCH_END
;
5534 Sort
Solver::getRoundingModeSort(void) const
5536 CVC5_API_TRY_CATCH_BEGIN
;
5537 //////// all checks before this line
5538 return Sort(this, getNodeManager()->roundingModeType());
5540 CVC5_API_TRY_CATCH_END
;
5543 /* Create sorts ------------------------------------------------------- */
5545 Sort
Solver::mkArraySort(const Sort
& indexSort
, const Sort
& elemSort
) const
5547 CVC5_API_TRY_CATCH_BEGIN
;
5548 CVC5_API_SOLVER_CHECK_SORT(indexSort
);
5549 CVC5_API_SOLVER_CHECK_SORT(elemSort
);
5550 //////// all checks before this line
5552 this, getNodeManager()->mkArrayType(*indexSort
.d_type
, *elemSort
.d_type
));
5554 CVC5_API_TRY_CATCH_END
;
5557 Sort
Solver::mkBitVectorSort(uint32_t size
) const
5559 CVC5_API_TRY_CATCH_BEGIN
;
5560 CVC5_API_ARG_CHECK_EXPECTED(size
> 0, size
) << "size > 0";
5561 //////// all checks before this line
5562 return Sort(this, getNodeManager()->mkBitVectorType(size
));
5564 CVC5_API_TRY_CATCH_END
;
5567 Sort
Solver::mkFloatingPointSort(uint32_t exp
, uint32_t sig
) const
5569 CVC5_API_TRY_CATCH_BEGIN
;
5570 CVC5_API_ARG_CHECK_EXPECTED(exp
> 0, exp
) << "exponent size > 0";
5571 CVC5_API_ARG_CHECK_EXPECTED(sig
> 0, sig
) << "significand size > 0";
5572 //////// all checks before this line
5573 return Sort(this, getNodeManager()->mkFloatingPointType(exp
, sig
));
5575 CVC5_API_TRY_CATCH_END
;
5578 Sort
Solver::mkDatatypeSort(const DatatypeDecl
& dtypedecl
) const
5580 CVC5_API_TRY_CATCH_BEGIN
;
5581 CVC5_API_SOLVER_CHECK_DTDECL(dtypedecl
);
5582 //////// all checks before this line
5583 return Sort(this, getNodeManager()->mkDatatypeType(*dtypedecl
.d_dtype
));
5585 CVC5_API_TRY_CATCH_END
;
5588 std::vector
<Sort
> Solver::mkDatatypeSorts(
5589 const std::vector
<DatatypeDecl
>& dtypedecls
) const
5591 CVC5_API_SOLVER_CHECK_DTDECLS(dtypedecls
);
5592 CVC5_API_TRY_CATCH_BEGIN
;
5593 //////// all checks before this line
5594 return mkDatatypeSortsInternal(dtypedecls
, {});
5596 CVC5_API_TRY_CATCH_END
;
5599 std::vector
<Sort
> Solver::mkDatatypeSorts(
5600 const std::vector
<DatatypeDecl
>& dtypedecls
,
5601 const std::set
<Sort
>& unresolvedSorts
) const
5603 CVC5_API_TRY_CATCH_BEGIN
;
5604 CVC5_API_SOLVER_CHECK_DTDECLS(dtypedecls
);
5605 CVC5_API_SOLVER_CHECK_SORTS(unresolvedSorts
);
5606 //////// all checks before this line
5607 return mkDatatypeSortsInternal(dtypedecls
, unresolvedSorts
);
5609 CVC5_API_TRY_CATCH_END
;
5612 Sort
Solver::mkFunctionSort(const Sort
& domain
, const Sort
& codomain
) const
5614 CVC5_API_TRY_CATCH_BEGIN
;
5615 CVC5_API_SOLVER_CHECK_DOMAIN_SORT(domain
);
5616 CVC5_API_SOLVER_CHECK_CODOMAIN_SORT(codomain
);
5617 //////// all checks before this line
5619 this, getNodeManager()->mkFunctionType(*domain
.d_type
, *codomain
.d_type
));
5621 CVC5_API_TRY_CATCH_END
;
5624 Sort
Solver::mkFunctionSort(const std::vector
<Sort
>& sorts
,
5625 const Sort
& codomain
) const
5627 CVC5_API_TRY_CATCH_BEGIN
;
5628 CVC5_API_ARG_SIZE_CHECK_EXPECTED(sorts
.size() >= 1, sorts
)
5629 << "at least one parameter sort for function sort";
5630 CVC5_API_SOLVER_CHECK_DOMAIN_SORTS(sorts
);
5631 CVC5_API_SOLVER_CHECK_CODOMAIN_SORT(codomain
);
5632 //////// all checks before this line
5633 std::vector
<TypeNode
> argTypes
= Sort::sortVectorToTypeNodes(sorts
);
5635 getNodeManager()->mkFunctionType(argTypes
, *codomain
.d_type
));
5637 CVC5_API_TRY_CATCH_END
;
5640 Sort
Solver::mkParamSort(const std::string
& symbol
) const
5642 CVC5_API_TRY_CATCH_BEGIN
;
5643 //////// all checks before this line
5646 getNodeManager()->mkSort(symbol
, NodeManager::SORT_FLAG_PLACEHOLDER
));
5648 CVC5_API_TRY_CATCH_END
;
5651 Sort
Solver::mkPredicateSort(const std::vector
<Sort
>& sorts
) const
5653 CVC5_API_TRY_CATCH_BEGIN
;
5654 CVC5_API_ARG_SIZE_CHECK_EXPECTED(sorts
.size() >= 1, sorts
)
5655 << "at least one parameter sort for predicate sort";
5656 CVC5_API_SOLVER_CHECK_DOMAIN_SORTS(sorts
);
5657 //////// all checks before this line
5660 getNodeManager()->mkPredicateType(Sort::sortVectorToTypeNodes(sorts
)));
5662 CVC5_API_TRY_CATCH_END
;
5665 Sort
Solver::mkRecordSort(
5666 const std::vector
<std::pair
<std::string
, Sort
>>& fields
) const
5668 CVC5_API_TRY_CATCH_BEGIN
;
5669 std::vector
<std::pair
<std::string
, TypeNode
>> f
;
5670 for (size_t i
= 0, size
= fields
.size(); i
< size
; ++i
)
5672 const auto& p
= fields
[i
];
5673 CVC5_API_ARG_AT_INDEX_CHECK_EXPECTED(!p
.second
.isNull(), "sort", fields
, i
)
5675 CVC5_API_ARG_AT_INDEX_CHECK_EXPECTED(
5676 this == p
.second
.d_solver
, "sort", fields
, i
)
5677 << "sort associated with this solver object";
5678 f
.emplace_back(p
.first
, *p
.second
.d_type
);
5680 //////// all checks before this line
5681 return Sort(this, getNodeManager()->mkRecordType(f
));
5683 CVC5_API_TRY_CATCH_END
;
5686 Sort
Solver::mkSetSort(const Sort
& elemSort
) const
5688 CVC5_API_TRY_CATCH_BEGIN
;
5689 CVC5_API_SOLVER_CHECK_SORT(elemSort
);
5690 //////// all checks before this line
5691 return Sort(this, getNodeManager()->mkSetType(*elemSort
.d_type
));
5693 CVC5_API_TRY_CATCH_END
;
5696 Sort
Solver::mkBagSort(const Sort
& elemSort
) const
5698 CVC5_API_TRY_CATCH_BEGIN
;
5699 CVC5_API_SOLVER_CHECK_SORT(elemSort
);
5700 //////// all checks before this line
5701 return Sort(this, getNodeManager()->mkBagType(*elemSort
.d_type
));
5703 CVC5_API_TRY_CATCH_END
;
5706 Sort
Solver::mkSequenceSort(const Sort
& elemSort
) const
5708 CVC5_API_TRY_CATCH_BEGIN
;
5709 CVC5_API_SOLVER_CHECK_SORT(elemSort
);
5710 //////// all checks before this line
5711 return Sort(this, getNodeManager()->mkSequenceType(*elemSort
.d_type
));
5713 CVC5_API_TRY_CATCH_END
;
5716 Sort
Solver::mkUninterpretedSort(const std::string
& symbol
) const
5718 CVC5_API_TRY_CATCH_BEGIN
;
5719 //////// all checks before this line
5720 return Sort(this, getNodeManager()->mkSort(symbol
));
5722 CVC5_API_TRY_CATCH_END
;
5725 Sort
Solver::mkUnresolvedSort(const std::string
& symbol
, size_t arity
) const
5727 CVC5_API_TRY_CATCH_BEGIN
;
5728 //////// all checks before this line
5731 return Sort(this, getNodeManager()->mkSortConstructor(symbol
, arity
));
5733 return Sort(this, getNodeManager()->mkSort(symbol
));
5735 CVC5_API_TRY_CATCH_END
;
5738 Sort
Solver::mkSortConstructorSort(const std::string
& symbol
,
5741 CVC5_API_TRY_CATCH_BEGIN
;
5742 CVC5_API_ARG_CHECK_EXPECTED(arity
> 0, arity
) << "an arity > 0";
5743 //////// all checks before this line
5744 return Sort(this, getNodeManager()->mkSortConstructor(symbol
, arity
));
5746 CVC5_API_TRY_CATCH_END
;
5749 Sort
Solver::mkTupleSort(const std::vector
<Sort
>& sorts
) const
5751 CVC5_API_TRY_CATCH_BEGIN
;
5752 CVC5_API_SOLVER_CHECK_SORTS_NOT_FUNCTION_LIKE(sorts
);
5753 //////// all checks before this line
5754 return mkTupleSortHelper(sorts
);
5756 CVC5_API_TRY_CATCH_END
;
5760 /* -------------------------------------------------------------------------- */
5762 Term
Solver::mkTrue(void) const
5764 CVC5_API_TRY_CATCH_BEGIN
;
5765 //////// all checks before this line
5766 return Term(this, d_nodeMgr
->mkConst
<bool>(true));
5768 CVC5_API_TRY_CATCH_END
;
5771 Term
Solver::mkFalse(void) const
5773 CVC5_API_TRY_CATCH_BEGIN
;
5774 //////// all checks before this line
5775 return Term(this, d_nodeMgr
->mkConst
<bool>(false));
5777 CVC5_API_TRY_CATCH_END
;
5780 Term
Solver::mkBoolean(bool val
) const
5782 CVC5_API_TRY_CATCH_BEGIN
;
5783 //////// all checks before this line
5784 return Term(this, d_nodeMgr
->mkConst
<bool>(val
));
5786 CVC5_API_TRY_CATCH_END
;
5789 Term
Solver::mkPi() const
5791 CVC5_API_TRY_CATCH_BEGIN
;
5792 //////// all checks before this line
5794 d_nodeMgr
->mkNullaryOperator(d_nodeMgr
->realType(), cvc5::kind::PI
);
5795 (void)res
.getType(true); /* kick off type checking */
5796 return Term(this, res
);
5798 CVC5_API_TRY_CATCH_END
;
5801 Term
Solver::mkInteger(const std::string
& s
) const
5803 CVC5_API_TRY_CATCH_BEGIN
;
5804 CVC5_API_ARG_CHECK_EXPECTED(isValidInteger(s
), s
) << " an integer ";
5805 Term integer
= mkRealOrIntegerFromStrHelper(s
);
5806 CVC5_API_ARG_CHECK_EXPECTED(integer
.getSort() == getIntegerSort(), s
)
5807 << " a string representing an integer";
5808 //////// all checks before this line
5811 CVC5_API_TRY_CATCH_END
;
5814 Term
Solver::mkInteger(int64_t val
) const
5816 CVC5_API_TRY_CATCH_BEGIN
;
5817 //////// all checks before this line
5818 Term integer
= mkRationalValHelper(cvc5::Rational(val
));
5819 Assert(integer
.getSort() == getIntegerSort());
5822 CVC5_API_TRY_CATCH_END
;
5825 Term
Solver::mkReal(const std::string
& s
) const
5827 CVC5_API_TRY_CATCH_BEGIN
;
5828 /* CLN and GMP handle this case differently, CLN interprets it as 0, GMP
5829 * throws an std::invalid_argument exception. For consistency, we treat it
5831 CVC5_API_ARG_CHECK_EXPECTED(s
!= ".", s
)
5832 << "a string representing a real or rational value.";
5833 //////// all checks before this line
5834 return mkRealOrIntegerFromStrHelper(s
, false);
5836 CVC5_API_TRY_CATCH_END
;
5839 Term
Solver::mkReal(int64_t val
) const
5841 CVC5_API_TRY_CATCH_BEGIN
;
5842 //////// all checks before this line
5843 return mkRationalValHelper(cvc5::Rational(val
), false);
5845 CVC5_API_TRY_CATCH_END
;
5848 Term
Solver::mkReal(int64_t num
, int64_t den
) const
5850 CVC5_API_TRY_CATCH_BEGIN
;
5851 //////// all checks before this line
5852 return mkRationalValHelper(cvc5::Rational(num
, den
), false);
5854 CVC5_API_TRY_CATCH_END
;
5857 Term
Solver::mkRegexpAll() const
5859 CVC5_API_TRY_CATCH_BEGIN
;
5860 //////// all checks before this line
5861 Node res
= d_nodeMgr
->mkNode(
5862 cvc5::kind::REGEXP_STAR
,
5863 d_nodeMgr
->mkNode(cvc5::kind::REGEXP_ALLCHAR
, std::vector
<cvc5::Node
>()));
5864 (void)res
.getType(true); /* kick off type checking */
5865 return Term(this, res
);
5867 CVC5_API_TRY_CATCH_END
;
5870 Term
Solver::mkRegexpNone() const
5872 CVC5_API_TRY_CATCH_BEGIN
;
5873 //////// all checks before this line
5875 d_nodeMgr
->mkNode(cvc5::kind::REGEXP_NONE
, std::vector
<cvc5::Node
>());
5876 (void)res
.getType(true); /* kick off type checking */
5877 return Term(this, res
);
5879 CVC5_API_TRY_CATCH_END
;
5882 Term
Solver::mkRegexpAllchar() const
5884 CVC5_API_TRY_CATCH_BEGIN
;
5885 //////// all checks before this line
5887 d_nodeMgr
->mkNode(cvc5::kind::REGEXP_ALLCHAR
, std::vector
<cvc5::Node
>());
5888 (void)res
.getType(true); /* kick off type checking */
5889 return Term(this, res
);
5891 CVC5_API_TRY_CATCH_END
;
5894 Term
Solver::mkEmptySet(const Sort
& sort
) const
5896 CVC5_API_TRY_CATCH_BEGIN
;
5897 CVC5_API_ARG_CHECK_EXPECTED(sort
.isNull() || sort
.isSet(), sort
)
5898 << "null sort or set sort";
5899 CVC5_API_ARG_CHECK_EXPECTED(sort
.isNull() || this == sort
.d_solver
, sort
)
5900 << "set sort associated with this solver object";
5901 //////// all checks before this line
5902 return mkValHelper
<cvc5::EmptySet
>(cvc5::EmptySet(*sort
.d_type
));
5904 CVC5_API_TRY_CATCH_END
;
5907 Term
Solver::mkEmptyBag(const Sort
& sort
) const
5909 CVC5_API_TRY_CATCH_BEGIN
;
5910 CVC5_API_ARG_CHECK_EXPECTED(sort
.isNull() || sort
.isBag(), sort
)
5911 << "null sort or bag sort";
5912 CVC5_API_ARG_CHECK_EXPECTED(sort
.isNull() || this == sort
.d_solver
, sort
)
5913 << "bag sort associated with this solver object";
5914 //////// all checks before this line
5915 return mkValHelper
<cvc5::EmptyBag
>(cvc5::EmptyBag(*sort
.d_type
));
5917 CVC5_API_TRY_CATCH_END
;
5920 Term
Solver::mkSepEmp() const
5922 CVC5_API_TRY_CATCH_BEGIN
;
5923 //////// all checks before this line
5924 Node res
= getNodeManager()->mkNullaryOperator(d_nodeMgr
->booleanType(),
5925 cvc5::Kind::SEP_EMP
);
5926 (void)res
.getType(true); /* kick off type checking */
5927 return Term(this, res
);
5929 CVC5_API_TRY_CATCH_END
;
5932 Term
Solver::mkSepNil(const Sort
& sort
) const
5934 CVC5_API_TRY_CATCH_BEGIN
;
5935 CVC5_API_SOLVER_CHECK_SORT(sort
);
5936 //////// all checks before this line
5938 getNodeManager()->mkNullaryOperator(*sort
.d_type
, cvc5::kind::SEP_NIL
);
5939 (void)res
.getType(true); /* kick off type checking */
5940 return Term(this, res
);
5942 CVC5_API_TRY_CATCH_END
;
5945 Term
Solver::mkString(const std::string
& s
, bool useEscSequences
) const
5947 CVC5_API_TRY_CATCH_BEGIN
;
5948 //////// all checks before this line
5949 return mkValHelper
<cvc5::String
>(cvc5::String(s
, useEscSequences
));
5951 CVC5_API_TRY_CATCH_END
;
5954 Term
Solver::mkString(const std::wstring
& s
) const
5956 CVC5_API_TRY_CATCH_BEGIN
;
5957 //////// all checks before this line
5958 return mkValHelper
<cvc5::String
>(cvc5::String(s
));
5960 CVC5_API_TRY_CATCH_END
;
5963 Term
Solver::mkEmptySequence(const Sort
& sort
) const
5965 CVC5_API_TRY_CATCH_BEGIN
;
5966 CVC5_API_SOLVER_CHECK_SORT(sort
);
5967 //////// all checks before this line
5968 std::vector
<Node
> seq
;
5969 Node res
= d_nodeMgr
->mkConst(Sequence(*sort
.d_type
, seq
));
5970 return Term(this, res
);
5972 CVC5_API_TRY_CATCH_END
;
5975 Term
Solver::mkUniverseSet(const Sort
& sort
) const
5977 CVC5_API_TRY_CATCH_BEGIN
;
5978 CVC5_API_SOLVER_CHECK_SORT(sort
);
5979 //////// all checks before this line
5981 Node res
= getNodeManager()->mkNullaryOperator(*sort
.d_type
,
5982 cvc5::kind::SET_UNIVERSE
);
5983 // TODO(#2771): Reenable?
5984 // (void)res->getType(true); /* kick off type checking */
5985 return Term(this, res
);
5987 CVC5_API_TRY_CATCH_END
;
5990 Term
Solver::mkBitVector(uint32_t size
, uint64_t val
) const
5992 CVC5_API_TRY_CATCH_BEGIN
;
5993 //////// all checks before this line
5994 return mkBVFromIntHelper(size
, val
);
5996 CVC5_API_TRY_CATCH_END
;
5999 Term
Solver::mkBitVector(uint32_t size
,
6000 const std::string
& s
,
6001 uint32_t base
) const
6003 CVC5_API_TRY_CATCH_BEGIN
;
6004 //////// all checks before this line
6005 return mkBVFromStrHelper(size
, s
, base
);
6007 CVC5_API_TRY_CATCH_END
;
6010 Term
Solver::mkConstArray(const Sort
& sort
, const Term
& val
) const
6012 CVC5_API_TRY_CATCH_BEGIN
;
6013 CVC5_API_SOLVER_CHECK_SORT(sort
);
6014 CVC5_API_SOLVER_CHECK_TERM(val
);
6015 CVC5_API_ARG_CHECK_EXPECTED(sort
.isArray(), sort
) << "an array sort";
6016 CVC5_API_CHECK(val
.getSort().isSubsortOf(sort
.getArrayElementSort()))
6017 << "Value does not match element sort";
6018 //////// all checks before this line
6020 // handle the special case of (CAST_TO_REAL n) where n is an integer
6021 Node n
= *val
.d_node
;
6022 if (val
.isCastedReal())
6024 // this is safe because the constant array stores its type
6028 mkValHelper
<cvc5::ArrayStoreAll
>(cvc5::ArrayStoreAll(*sort
.d_type
, n
));
6031 CVC5_API_TRY_CATCH_END
;
6034 Term
Solver::mkFloatingPointPosInf(uint32_t exp
, uint32_t sig
) const
6036 CVC5_API_TRY_CATCH_BEGIN
;
6037 //////// all checks before this line
6038 return mkValHelper
<cvc5::FloatingPoint
>(
6039 FloatingPoint::makeInf(FloatingPointSize(exp
, sig
), false));
6041 CVC5_API_TRY_CATCH_END
;
6044 Term
Solver::mkFloatingPointNegInf(uint32_t exp
, uint32_t sig
) const
6046 CVC5_API_TRY_CATCH_BEGIN
;
6047 //////// all checks before this line
6048 return mkValHelper
<cvc5::FloatingPoint
>(
6049 FloatingPoint::makeInf(FloatingPointSize(exp
, sig
), true));
6051 CVC5_API_TRY_CATCH_END
;
6054 Term
Solver::mkFloatingPointNaN(uint32_t exp
, uint32_t sig
) const
6056 CVC5_API_TRY_CATCH_BEGIN
;
6057 //////// all checks before this line
6058 return mkValHelper
<cvc5::FloatingPoint
>(
6059 FloatingPoint::makeNaN(FloatingPointSize(exp
, sig
)));
6061 CVC5_API_TRY_CATCH_END
;
6064 Term
Solver::mkFloatingPointPosZero(uint32_t exp
, uint32_t sig
) const
6066 CVC5_API_TRY_CATCH_BEGIN
;
6067 //////// all checks before this line
6068 return mkValHelper
<cvc5::FloatingPoint
>(
6069 FloatingPoint::makeZero(FloatingPointSize(exp
, sig
), false));
6071 CVC5_API_TRY_CATCH_END
;
6074 Term
Solver::mkFloatingPointNegZero(uint32_t exp
, uint32_t sig
) const
6076 CVC5_API_TRY_CATCH_BEGIN
;
6077 //////// all checks before this line
6078 return mkValHelper
<cvc5::FloatingPoint
>(
6079 FloatingPoint::makeZero(FloatingPointSize(exp
, sig
), true));
6081 CVC5_API_TRY_CATCH_END
;
6084 Term
Solver::mkRoundingMode(RoundingMode rm
) const
6086 CVC5_API_TRY_CATCH_BEGIN
;
6087 //////// all checks before this line
6088 return mkValHelper
<cvc5::RoundingMode
>(s_rmodes
.at(rm
));
6090 CVC5_API_TRY_CATCH_END
;
6093 Term
Solver::mkFloatingPoint(uint32_t exp
, uint32_t sig
, Term val
) const
6095 CVC5_API_TRY_CATCH_BEGIN
;
6096 CVC5_API_SOLVER_CHECK_TERM(val
);
6097 CVC5_API_ARG_CHECK_EXPECTED(exp
> 0, exp
) << "a value > 0";
6098 CVC5_API_ARG_CHECK_EXPECTED(sig
> 0, sig
) << "a value > 0";
6099 uint32_t bw
= exp
+ sig
;
6100 CVC5_API_ARG_CHECK_EXPECTED(bw
== val
.d_node
->getType().getBitVectorSize(),
6102 << "a bit-vector constant with bit-width '" << bw
<< "'";
6103 CVC5_API_ARG_CHECK_EXPECTED(
6104 val
.d_node
->getType().isBitVector() && val
.d_node
->isConst(), val
)
6105 << "bit-vector constant";
6106 //////// all checks before this line
6107 return mkValHelper
<cvc5::FloatingPoint
>(
6108 cvc5::FloatingPoint(exp
, sig
, val
.d_node
->getConst
<BitVector
>()));
6110 CVC5_API_TRY_CATCH_END
;
6113 Term
Solver::mkCardinalityConstraint(const Sort
& sort
, uint32_t upperBound
) const
6115 CVC5_API_TRY_CATCH_BEGIN
;
6116 CVC5_API_SOLVER_CHECK_SORT(sort
);
6117 CVC5_API_ARG_CHECK_EXPECTED(sort
.isUninterpretedSort(), sort
)
6118 << "an uninterpreted sort";
6119 CVC5_API_ARG_CHECK_EXPECTED(upperBound
> 0, upperBound
) << "a value > 0";
6120 //////// all checks before this line
6122 d_nodeMgr
->mkConst(cvc5::CardinalityConstraint(*sort
.d_type
, upperBound
));
6123 Node cc
= d_nodeMgr
->mkNode(cvc5::Kind::CARDINALITY_CONSTRAINT
, cco
);
6124 return Term(this, cc
);
6126 CVC5_API_TRY_CATCH_END
;
6129 /* Create constants */
6130 /* -------------------------------------------------------------------------- */
6132 Term
Solver::mkConst(const Sort
& sort
, const std::string
& symbol
) const
6134 CVC5_API_TRY_CATCH_BEGIN
;
6135 CVC5_API_SOLVER_CHECK_SORT(sort
);
6136 //////// all checks before this line
6137 Node res
= d_nodeMgr
->mkVar(symbol
, *sort
.d_type
);
6138 (void)res
.getType(true); /* kick off type checking */
6139 increment_vars_consts_stats(sort
, false);
6140 return Term(this, res
);
6142 CVC5_API_TRY_CATCH_END
;
6145 Term
Solver::mkConst(const Sort
& sort
) const
6147 CVC5_API_TRY_CATCH_BEGIN
;
6148 CVC5_API_SOLVER_CHECK_SORT(sort
);
6149 //////// all checks before this line
6150 Node res
= d_nodeMgr
->mkVar(*sort
.d_type
);
6151 (void)res
.getType(true); /* kick off type checking */
6152 increment_vars_consts_stats(sort
, false);
6153 return Term(this, res
);
6155 CVC5_API_TRY_CATCH_END
;
6158 /* Create variables */
6159 /* -------------------------------------------------------------------------- */
6161 Term
Solver::mkVar(const Sort
& sort
, const std::string
& symbol
) const
6163 CVC5_API_TRY_CATCH_BEGIN
;
6164 CVC5_API_SOLVER_CHECK_SORT(sort
);
6165 //////// all checks before this line
6166 Node res
= symbol
.empty() ? d_nodeMgr
->mkBoundVar(*sort
.d_type
)
6167 : d_nodeMgr
->mkBoundVar(symbol
, *sort
.d_type
);
6168 (void)res
.getType(true); /* kick off type checking */
6169 increment_vars_consts_stats(sort
, true);
6170 return Term(this, res
);
6172 CVC5_API_TRY_CATCH_END
;
6175 /* Create datatype constructor declarations */
6176 /* -------------------------------------------------------------------------- */
6178 DatatypeConstructorDecl
Solver::mkDatatypeConstructorDecl(
6179 const std::string
& name
)
6181 CVC5_API_TRY_CATCH_BEGIN
;
6182 //////// all checks before this line
6183 return DatatypeConstructorDecl(this, name
);
6185 CVC5_API_TRY_CATCH_END
;
6188 /* Create datatype declarations */
6189 /* -------------------------------------------------------------------------- */
6191 DatatypeDecl
Solver::mkDatatypeDecl(const std::string
& name
, bool isCoDatatype
)
6193 CVC5_API_TRY_CATCH_BEGIN
;
6194 //////// all checks before this line
6195 return DatatypeDecl(this, name
, isCoDatatype
);
6197 CVC5_API_TRY_CATCH_END
;
6200 DatatypeDecl
Solver::mkDatatypeDecl(const std::string
& name
,
6204 CVC5_API_TRY_CATCH_BEGIN
;
6205 CVC5_API_SOLVER_CHECK_SORT(param
);
6206 //////// all checks before this line
6207 return DatatypeDecl(this, name
, param
, isCoDatatype
);
6209 CVC5_API_TRY_CATCH_END
;
6212 DatatypeDecl
Solver::mkDatatypeDecl(const std::string
& name
,
6213 const std::vector
<Sort
>& params
,
6216 CVC5_API_TRY_CATCH_BEGIN
;
6217 CVC5_API_SOLVER_CHECK_SORTS(params
);
6218 //////// all checks before this line
6219 return DatatypeDecl(this, name
, params
, isCoDatatype
);
6221 CVC5_API_TRY_CATCH_END
;
6225 /* -------------------------------------------------------------------------- */
6227 Term
Solver::mkTerm(Kind kind
) const
6229 CVC5_API_TRY_CATCH_BEGIN
;
6230 CVC5_API_KIND_CHECK(kind
);
6231 //////// all checks before this line
6232 return mkTermFromKind(kind
);
6234 CVC5_API_TRY_CATCH_END
;
6237 Term
Solver::mkTerm(Kind kind
, const Term
& child
) const
6239 CVC5_API_TRY_CATCH_BEGIN
;
6240 CVC5_API_KIND_CHECK(kind
);
6241 CVC5_API_SOLVER_CHECK_TERM(child
);
6242 //////// all checks before this line
6243 return mkTermHelper(kind
, std::vector
<Term
>{child
});
6245 CVC5_API_TRY_CATCH_END
;
6248 Term
Solver::mkTerm(Kind kind
, const Term
& child1
, const Term
& child2
) const
6250 CVC5_API_TRY_CATCH_BEGIN
;
6251 CVC5_API_KIND_CHECK(kind
);
6252 CVC5_API_SOLVER_CHECK_TERM(child1
);
6253 CVC5_API_SOLVER_CHECK_TERM(child2
);
6254 //////// all checks before this line
6255 return mkTermHelper(kind
, std::vector
<Term
>{child1
, child2
});
6257 CVC5_API_TRY_CATCH_END
;
6260 Term
Solver::mkTerm(Kind kind
,
6263 const Term
& child3
) const
6265 CVC5_API_TRY_CATCH_BEGIN
;
6266 CVC5_API_KIND_CHECK(kind
);
6267 CVC5_API_SOLVER_CHECK_TERM(child1
);
6268 CVC5_API_SOLVER_CHECK_TERM(child2
);
6269 CVC5_API_SOLVER_CHECK_TERM(child3
);
6270 //////// all checks before this line
6271 // need to use internal term call to check e.g. associative construction
6272 return mkTermHelper(kind
, std::vector
<Term
>{child1
, child2
, child3
});
6274 CVC5_API_TRY_CATCH_END
;
6277 Term
Solver::mkTerm(Kind kind
, const std::vector
<Term
>& children
) const
6279 CVC5_API_TRY_CATCH_BEGIN
;
6280 CVC5_API_KIND_CHECK(kind
);
6281 CVC5_API_SOLVER_CHECK_TERMS(children
);
6282 //////// all checks before this line
6283 return mkTermHelper(kind
, children
);
6285 CVC5_API_TRY_CATCH_END
;
6288 Term
Solver::mkTerm(const Op
& op
) const
6290 CVC5_API_TRY_CATCH_BEGIN
;
6291 CVC5_API_SOLVER_CHECK_OP(op
);
6292 if (!op
.isIndexedHelper())
6294 return mkTermFromKind(op
.d_kind
);
6296 checkMkTerm(op
.d_kind
, 0);
6297 //////// all checks before this line
6298 const cvc5::Kind int_kind
= extToIntKind(op
.d_kind
);
6299 Term res
= Term(this, getNodeManager()->mkNode(int_kind
, *op
.d_node
));
6301 (void)res
.d_node
->getType(true); /* kick off type checking */
6304 CVC5_API_TRY_CATCH_END
;
6307 Term
Solver::mkTerm(const Op
& op
, const Term
& child
) const
6309 CVC5_API_TRY_CATCH_BEGIN
;
6310 CVC5_API_SOLVER_CHECK_OP(op
);
6311 CVC5_API_SOLVER_CHECK_TERM(child
);
6312 //////// all checks before this line
6313 return mkTermHelper(op
, std::vector
<Term
>{child
});
6315 CVC5_API_TRY_CATCH_END
;
6318 Term
Solver::mkTerm(const Op
& op
, const Term
& child1
, const Term
& child2
) const
6320 CVC5_API_TRY_CATCH_BEGIN
;
6321 CVC5_API_SOLVER_CHECK_OP(op
);
6322 CVC5_API_SOLVER_CHECK_TERM(child1
);
6323 CVC5_API_SOLVER_CHECK_TERM(child2
);
6324 //////// all checks before this line
6325 return mkTermHelper(op
, std::vector
<Term
>{child1
, child2
});
6327 CVC5_API_TRY_CATCH_END
;
6330 Term
Solver::mkTerm(const Op
& op
,
6333 const Term
& child3
) const
6335 CVC5_API_TRY_CATCH_BEGIN
;
6336 CVC5_API_SOLVER_CHECK_OP(op
);
6337 CVC5_API_SOLVER_CHECK_TERM(child1
);
6338 CVC5_API_SOLVER_CHECK_TERM(child2
);
6339 CVC5_API_SOLVER_CHECK_TERM(child3
);
6340 //////// all checks before this line
6341 return mkTermHelper(op
, std::vector
<Term
>{child1
, child2
, child3
});
6343 CVC5_API_TRY_CATCH_END
;
6346 Term
Solver::mkTerm(const Op
& op
, const std::vector
<Term
>& children
) const
6348 CVC5_API_TRY_CATCH_BEGIN
;
6349 CVC5_API_SOLVER_CHECK_OP(op
);
6350 CVC5_API_SOLVER_CHECK_TERMS(children
);
6351 //////// all checks before this line
6352 return mkTermHelper(op
, children
);
6354 CVC5_API_TRY_CATCH_END
;
6357 Term
Solver::mkTuple(const std::vector
<Sort
>& sorts
,
6358 const std::vector
<Term
>& terms
) const
6360 CVC5_API_TRY_CATCH_BEGIN
;
6361 CVC5_API_CHECK(sorts
.size() == terms
.size())
6362 << "Expected the same number of sorts and elements";
6363 CVC5_API_SOLVER_CHECK_SORTS(sorts
);
6364 CVC5_API_SOLVER_CHECK_TERMS(terms
);
6365 //////// all checks before this line
6366 std::vector
<cvc5::Node
> args
;
6367 for (size_t i
= 0, size
= sorts
.size(); i
< size
; i
++)
6369 args
.push_back(*(ensureTermSort(terms
[i
], sorts
[i
])).d_node
);
6372 Sort s
= mkTupleSortHelper(sorts
);
6373 Datatype dt
= s
.getDatatype();
6374 NodeBuilder
nb(extToIntKind(APPLY_CONSTRUCTOR
));
6375 nb
<< *dt
[0].getConstructorTerm().d_node
;
6377 Node res
= nb
.constructNode();
6378 (void)res
.getType(true); /* kick off type checking */
6379 return Term(this, res
);
6381 CVC5_API_TRY_CATCH_END
;
6384 /* Create operators */
6385 /* -------------------------------------------------------------------------- */
6387 Op
Solver::mkOp(Kind kind
) const
6389 CVC5_API_TRY_CATCH_BEGIN
;
6390 CVC5_API_KIND_CHECK(kind
);
6391 CVC5_API_CHECK(s_indexed_kinds
.find(kind
) == s_indexed_kinds
.end())
6392 << "Expected a kind for a non-indexed operator.";
6393 //////// all checks before this line
6394 return Op(this, kind
);
6396 CVC5_API_TRY_CATCH_END
6399 Op
Solver::mkOp(Kind kind
, const std::string
& arg
) const
6401 CVC5_API_TRY_CATCH_BEGIN
;
6402 CVC5_API_KIND_CHECK(kind
);
6403 CVC5_API_KIND_CHECK_EXPECTED((kind
== DIVISIBLE
), kind
) << "DIVISIBLE";
6404 //////// all checks before this line
6406 /* CLN and GMP handle this case differently, CLN interprets it as 0, GMP
6407 * throws an std::invalid_argument exception. For consistency, we treat it
6409 CVC5_API_ARG_CHECK_EXPECTED(arg
!= ".", arg
)
6410 << "a string representing an integer, real or rational value.";
6413 *mkValHelper
<cvc5::Divisible
>(cvc5::Divisible(cvc5::Integer(arg
)))
6417 CVC5_API_TRY_CATCH_END
;
6420 Op
Solver::mkOp(Kind kind
, uint32_t arg
) const
6422 CVC5_API_TRY_CATCH_BEGIN
;
6423 CVC5_API_KIND_CHECK(kind
);
6424 //////// all checks before this line
6431 *mkValHelper
<cvc5::Divisible
>(cvc5::Divisible(arg
)).d_node
);
6433 case BITVECTOR_REPEAT
:
6436 *mkValHelper
<cvc5::BitVectorRepeat
>(cvc5::BitVectorRepeat(arg
))
6439 case BITVECTOR_ZERO_EXTEND
:
6442 *mkValHelper
<cvc5::BitVectorZeroExtend
>(
6443 cvc5::BitVectorZeroExtend(arg
))
6446 case BITVECTOR_SIGN_EXTEND
:
6449 *mkValHelper
<cvc5::BitVectorSignExtend
>(
6450 cvc5::BitVectorSignExtend(arg
))
6453 case BITVECTOR_ROTATE_LEFT
:
6456 *mkValHelper
<cvc5::BitVectorRotateLeft
>(
6457 cvc5::BitVectorRotateLeft(arg
))
6460 case BITVECTOR_ROTATE_RIGHT
:
6463 *mkValHelper
<cvc5::BitVectorRotateRight
>(
6464 cvc5::BitVectorRotateRight(arg
))
6467 case INT_TO_BITVECTOR
:
6471 *mkValHelper
<cvc5::IntToBitVector
>(cvc5::IntToBitVector(arg
)).d_node
);
6475 Op(this, kind
, *mkValHelper
<cvc5::IntAnd
>(cvc5::IntAnd(arg
)).d_node
);
6477 case FLOATINGPOINT_TO_UBV
:
6481 *mkValHelper
<cvc5::FloatingPointToUBV
>(cvc5::FloatingPointToUBV(arg
))
6484 case FLOATINGPOINT_TO_SBV
:
6488 *mkValHelper
<cvc5::FloatingPointToSBV
>(cvc5::FloatingPointToSBV(arg
))
6495 *mkValHelper
<cvc5::RegExpRepeat
>(cvc5::RegExpRepeat(arg
)).d_node
);
6498 CVC5_API_KIND_CHECK_EXPECTED(false, kind
)
6499 << "operator kind with uint32_t argument";
6501 Assert(!res
.isNull());
6504 CVC5_API_TRY_CATCH_END
;
6507 Op
Solver::mkOp(Kind kind
, uint32_t arg1
, uint32_t arg2
) const
6509 CVC5_API_TRY_CATCH_BEGIN
;
6510 CVC5_API_KIND_CHECK(kind
);
6511 //////// all checks before this line
6516 case BITVECTOR_EXTRACT
:
6519 *mkValHelper
<cvc5::BitVectorExtract
>(
6520 cvc5::BitVectorExtract(arg1
, arg2
))
6523 case FLOATINGPOINT_TO_FP_IEEE_BITVECTOR
:
6526 *mkValHelper
<cvc5::FloatingPointToFPIEEEBitVector
>(
6527 cvc5::FloatingPointToFPIEEEBitVector(arg1
, arg2
))
6530 case FLOATINGPOINT_TO_FP_FLOATINGPOINT
:
6533 *mkValHelper
<cvc5::FloatingPointToFPFloatingPoint
>(
6534 cvc5::FloatingPointToFPFloatingPoint(arg1
, arg2
))
6537 case FLOATINGPOINT_TO_FP_REAL
:
6540 *mkValHelper
<cvc5::FloatingPointToFPReal
>(
6541 cvc5::FloatingPointToFPReal(arg1
, arg2
))
6544 case FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR
:
6547 *mkValHelper
<cvc5::FloatingPointToFPSignedBitVector
>(
6548 cvc5::FloatingPointToFPSignedBitVector(arg1
, arg2
))
6551 case FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR
:
6554 *mkValHelper
<cvc5::FloatingPointToFPUnsignedBitVector
>(
6555 cvc5::FloatingPointToFPUnsignedBitVector(arg1
, arg2
))
6558 case FLOATINGPOINT_TO_FP_GENERIC
:
6561 *mkValHelper
<cvc5::FloatingPointToFPGeneric
>(
6562 cvc5::FloatingPointToFPGeneric(arg1
, arg2
))
6569 *mkValHelper
<cvc5::RegExpLoop
>(cvc5::RegExpLoop(arg1
, arg2
)).d_node
);
6572 CVC5_API_KIND_CHECK_EXPECTED(false, kind
)
6573 << "operator kind with two uint32_t arguments";
6575 Assert(!res
.isNull());
6578 CVC5_API_TRY_CATCH_END
;
6581 Op
Solver::mkOp(Kind kind
, const std::vector
<uint32_t>& args
) const
6583 CVC5_API_TRY_CATCH_BEGIN
;
6584 CVC5_API_KIND_CHECK(kind
);
6585 //////// all checks before this line
6594 *mkValHelper
<cvc5::TupleProjectOp
>(cvc5::TupleProjectOp(args
))
6600 std::string message
= "operator kind with " + std::to_string(args
.size())
6601 + " uint32_t arguments";
6602 CVC5_API_KIND_CHECK_EXPECTED(false, kind
) << message
;
6605 Assert(!res
.isNull());
6608 CVC5_API_TRY_CATCH_END
;
6611 /* Non-SMT-LIB commands */
6612 /* -------------------------------------------------------------------------- */
6614 Term
Solver::simplify(const Term
& term
)
6616 CVC5_API_TRY_CATCH_BEGIN
;
6617 CVC5_API_SOLVER_CHECK_TERM(term
);
6618 //////// all checks before this line
6619 return Term(this, d_slv
->simplify(*term
.d_node
));
6621 CVC5_API_TRY_CATCH_END
;
6624 Result
Solver::checkEntailed(const Term
& term
) const
6626 CVC5_API_TRY_CATCH_BEGIN
;
6627 CVC5_API_CHECK(!d_slv
->isQueryMade()
6628 || d_slv
->getOptions().base
.incrementalSolving
)
6629 << "Cannot make multiple queries unless incremental solving is enabled "
6630 "(try --incremental)";
6631 CVC5_API_SOLVER_CHECK_TERM(term
);
6632 //////// all checks before this line
6633 return d_slv
->checkEntailed(*term
.d_node
);
6635 CVC5_API_TRY_CATCH_END
;
6638 Result
Solver::checkEntailed(const std::vector
<Term
>& terms
) const
6640 CVC5_API_TRY_CATCH_BEGIN
;
6641 CVC5_API_CHECK(!d_slv
->isQueryMade()
6642 || d_slv
->getOptions().base
.incrementalSolving
)
6643 << "Cannot make multiple queries unless incremental solving is enabled "
6644 "(try --incremental)";
6645 CVC5_API_SOLVER_CHECK_TERMS(terms
);
6646 //////// all checks before this line
6647 return d_slv
->checkEntailed(Term::termVectorToNodes(terms
));
6649 CVC5_API_TRY_CATCH_END
;
6652 /* SMT-LIB commands */
6653 /* -------------------------------------------------------------------------- */
6655 void Solver::assertFormula(const Term
& term
) const
6657 CVC5_API_TRY_CATCH_BEGIN
;
6658 CVC5_API_SOLVER_CHECK_TERM(term
);
6659 CVC5_API_SOLVER_CHECK_TERM_WITH_SORT(term
, getBooleanSort());
6660 //////// all checks before this line
6661 d_slv
->assertFormula(*term
.d_node
);
6663 CVC5_API_TRY_CATCH_END
;
6666 Result
Solver::checkSat(void) const
6668 CVC5_API_TRY_CATCH_BEGIN
;
6669 CVC5_API_CHECK(!d_slv
->isQueryMade()
6670 || d_slv
->getOptions().base
.incrementalSolving
)
6671 << "Cannot make multiple queries unless incremental solving is enabled "
6672 "(try --incremental)";
6673 //////// all checks before this line
6674 return d_slv
->checkSat();
6676 CVC5_API_TRY_CATCH_END
;
6679 Result
Solver::checkSatAssuming(const Term
& assumption
) const
6681 CVC5_API_TRY_CATCH_BEGIN
;
6682 CVC5_API_CHECK(!d_slv
->isQueryMade()
6683 || d_slv
->getOptions().base
.incrementalSolving
)
6684 << "Cannot make multiple queries unless incremental solving is enabled "
6685 "(try --incremental)";
6686 CVC5_API_SOLVER_CHECK_TERM_WITH_SORT(assumption
, getBooleanSort());
6687 //////// all checks before this line
6688 return d_slv
->checkSat(*assumption
.d_node
);
6690 CVC5_API_TRY_CATCH_END
;
6693 Result
Solver::checkSatAssuming(const std::vector
<Term
>& assumptions
) const
6695 CVC5_API_TRY_CATCH_BEGIN
;
6696 CVC5_API_CHECK(!d_slv
->isQueryMade() || assumptions
.size() == 0
6697 || d_slv
->getOptions().base
.incrementalSolving
)
6698 << "Cannot make multiple queries unless incremental solving is enabled "
6699 "(try --incremental)";
6700 CVC5_API_SOLVER_CHECK_TERMS_WITH_SORT(assumptions
, getBooleanSort());
6701 //////// all checks before this line
6702 for (const Term
& term
: assumptions
)
6704 CVC5_API_SOLVER_CHECK_TERM(term
);
6706 std::vector
<Node
> eassumptions
= Term::termVectorToNodes(assumptions
);
6707 return d_slv
->checkSat(eassumptions
);
6709 CVC5_API_TRY_CATCH_END
;
6712 Sort
Solver::declareDatatype(
6713 const std::string
& symbol
,
6714 const std::vector
<DatatypeConstructorDecl
>& ctors
) const
6716 CVC5_API_TRY_CATCH_BEGIN
;
6717 CVC5_API_ARG_CHECK_EXPECTED(ctors
.size() > 0, ctors
)
6718 << "a datatype declaration with at least one constructor";
6719 CVC5_API_SOLVER_CHECK_DTCTORDECLS(ctors
);
6720 for (size_t i
= 0, size
= ctors
.size(); i
< size
; i
++)
6722 CVC5_API_CHECK(!ctors
[i
].isResolved())
6723 << "cannot use a constructor for multiple datatypes";
6725 //////// all checks before this line
6726 DatatypeDecl
dtdecl(this, symbol
);
6727 for (size_t i
= 0, size
= ctors
.size(); i
< size
; i
++)
6729 dtdecl
.addConstructor(ctors
[i
]);
6731 return Sort(this, getNodeManager()->mkDatatypeType(*dtdecl
.d_dtype
));
6733 CVC5_API_TRY_CATCH_END
;
6736 Term
Solver::declareFun(const std::string
& symbol
,
6737 const std::vector
<Sort
>& sorts
,
6738 const Sort
& sort
) const
6740 CVC5_API_TRY_CATCH_BEGIN
;
6741 CVC5_API_SOLVER_CHECK_DOMAIN_SORTS(sorts
);
6742 CVC5_API_SOLVER_CHECK_CODOMAIN_SORT(sort
);
6743 //////// all checks before this line
6745 TypeNode type
= *sort
.d_type
;
6748 std::vector
<TypeNode
> types
= Sort::sortVectorToTypeNodes(sorts
);
6749 type
= getNodeManager()->mkFunctionType(types
, type
);
6751 return Term(this, d_nodeMgr
->mkVar(symbol
, type
));
6753 CVC5_API_TRY_CATCH_END
;
6756 Sort
Solver::declareSort(const std::string
& symbol
, uint32_t arity
) const
6758 CVC5_API_TRY_CATCH_BEGIN
;
6759 //////// all checks before this line
6762 return Sort(this, getNodeManager()->mkSort(symbol
));
6764 return Sort(this, getNodeManager()->mkSortConstructor(symbol
, arity
));
6766 CVC5_API_TRY_CATCH_END
;
6769 Term
Solver::defineFun(const std::string
& symbol
,
6770 const std::vector
<Term
>& bound_vars
,
6775 CVC5_API_TRY_CATCH_BEGIN
;
6776 CVC5_API_SOLVER_CHECK_CODOMAIN_SORT(sort
);
6777 CVC5_API_SOLVER_CHECK_TERM(term
);
6778 CVC5_API_CHECK(term
.getSort().isSubsortOf(sort
))
6779 << "Invalid sort of function body '" << term
<< "', expected '" << sort
6782 std::vector
<Sort
> domain_sorts
;
6783 for (const auto& bv
: bound_vars
)
6785 domain_sorts
.push_back(bv
.getSort());
6788 domain_sorts
.empty()
6791 getNodeManager()->mkFunctionType(
6792 Sort::sortVectorToTypeNodes(domain_sorts
), *sort
.d_type
));
6793 Term fun
= mkConst(fun_sort
, symbol
);
6795 CVC5_API_SOLVER_CHECK_BOUND_VARS_DEF_FUN(fun
, bound_vars
, domain_sorts
);
6796 //////// all checks before this line
6798 d_slv
->defineFunction(
6799 *fun
.d_node
, Term::termVectorToNodes(bound_vars
), *term
.d_node
, global
);
6802 CVC5_API_TRY_CATCH_END
;
6805 Term
Solver::defineFunRec(const std::string
& symbol
,
6806 const std::vector
<Term
>& bound_vars
,
6811 CVC5_API_TRY_CATCH_BEGIN
;
6813 CVC5_API_CHECK(d_slv
->getUserLogicInfo().isQuantified())
6814 << "recursive function definitions require a logic with quantifiers";
6815 CVC5_API_CHECK(d_slv
->getUserLogicInfo().isTheoryEnabled(theory::THEORY_UF
))
6816 << "recursive function definitions require a logic with uninterpreted "
6819 CVC5_API_SOLVER_CHECK_TERM(term
);
6820 CVC5_API_SOLVER_CHECK_CODOMAIN_SORT(sort
);
6821 CVC5_API_CHECK(sort
== term
.getSort())
6822 << "Invalid sort of function body '" << term
<< "', expected '" << sort
6825 std::vector
<Sort
> domain_sorts
;
6826 for (const auto& bv
: bound_vars
)
6828 domain_sorts
.push_back(bv
.getSort());
6831 domain_sorts
.empty()
6834 getNodeManager()->mkFunctionType(
6835 Sort::sortVectorToTypeNodes(domain_sorts
), *sort
.d_type
));
6836 Term fun
= mkConst(fun_sort
, symbol
);
6838 CVC5_API_SOLVER_CHECK_BOUND_VARS_DEF_FUN(fun
, bound_vars
, domain_sorts
);
6839 //////// all checks before this line
6841 d_slv
->defineFunctionRec(
6842 *fun
.d_node
, Term::termVectorToNodes(bound_vars
), *term
.d_node
, global
);
6846 CVC5_API_TRY_CATCH_END
;
6849 Term
Solver::defineFunRec(const Term
& fun
,
6850 const std::vector
<Term
>& bound_vars
,
6854 CVC5_API_TRY_CATCH_BEGIN
;
6856 CVC5_API_CHECK(d_slv
->getUserLogicInfo().isQuantified())
6857 << "recursive function definitions require a logic with quantifiers";
6858 CVC5_API_CHECK(d_slv
->getUserLogicInfo().isTheoryEnabled(theory::THEORY_UF
))
6859 << "recursive function definitions require a logic with uninterpreted "
6862 CVC5_API_SOLVER_CHECK_TERM(fun
);
6863 CVC5_API_SOLVER_CHECK_TERM(term
);
6864 if (fun
.getSort().isFunction())
6866 std::vector
<Sort
> domain_sorts
= fun
.getSort().getFunctionDomainSorts();
6867 CVC5_API_SOLVER_CHECK_BOUND_VARS_DEF_FUN(fun
, bound_vars
, domain_sorts
);
6868 Sort codomain
= fun
.getSort().getFunctionCodomainSort();
6869 CVC5_API_CHECK(codomain
== term
.getSort())
6870 << "Invalid sort of function body '" << term
<< "', expected '"
6875 CVC5_API_SOLVER_CHECK_BOUND_VARS(bound_vars
);
6876 CVC5_API_ARG_CHECK_EXPECTED(bound_vars
.size() == 0, fun
)
6877 << "function or nullary symbol";
6879 //////// all checks before this line
6881 std::vector
<Node
> ebound_vars
= Term::termVectorToNodes(bound_vars
);
6882 d_slv
->defineFunctionRec(*fun
.d_node
, ebound_vars
, *term
.d_node
, global
);
6885 CVC5_API_TRY_CATCH_END
;
6888 void Solver::defineFunsRec(const std::vector
<Term
>& funs
,
6889 const std::vector
<std::vector
<Term
>>& bound_vars
,
6890 const std::vector
<Term
>& terms
,
6893 CVC5_API_TRY_CATCH_BEGIN
;
6895 CVC5_API_CHECK(d_slv
->getUserLogicInfo().isQuantified())
6896 << "recursive function definitions require a logic with quantifiers";
6897 CVC5_API_CHECK(d_slv
->getUserLogicInfo().isTheoryEnabled(theory::THEORY_UF
))
6898 << "recursive function definitions require a logic with uninterpreted "
6900 CVC5_API_SOLVER_CHECK_TERMS(funs
);
6901 CVC5_API_SOLVER_CHECK_TERMS(terms
);
6903 size_t funs_size
= funs
.size();
6904 CVC5_API_ARG_SIZE_CHECK_EXPECTED(funs_size
== bound_vars
.size(), bound_vars
)
6905 << "'" << funs_size
<< "'";
6906 CVC5_API_ARG_SIZE_CHECK_EXPECTED(funs_size
== terms
.size(), terms
)
6907 << "'" << funs_size
<< "'";
6909 for (size_t j
= 0; j
< funs_size
; ++j
)
6911 const Term
& fun
= funs
[j
];
6912 const std::vector
<Term
>& bvars
= bound_vars
[j
];
6913 const Term
& term
= terms
[j
];
6915 CVC5_API_ARG_AT_INDEX_CHECK_EXPECTED(
6916 this == fun
.d_solver
, "function", funs
, j
)
6917 << "function associated with this solver object";
6918 CVC5_API_ARG_AT_INDEX_CHECK_EXPECTED(
6919 this == term
.d_solver
, "term", terms
, j
)
6920 << "term associated with this solver object";
6922 if (fun
.getSort().isFunction())
6924 std::vector
<Sort
> domain_sorts
= fun
.getSort().getFunctionDomainSorts();
6925 CVC5_API_SOLVER_CHECK_BOUND_VARS_DEF_FUN(fun
, bvars
, domain_sorts
);
6926 Sort codomain
= fun
.getSort().getFunctionCodomainSort();
6927 CVC5_API_ARG_AT_INDEX_CHECK_EXPECTED(
6928 codomain
== term
.getSort(), "sort of function body", terms
, j
)
6929 << "'" << codomain
<< "'";
6933 CVC5_API_SOLVER_CHECK_BOUND_VARS(bvars
);
6934 CVC5_API_ARG_CHECK_EXPECTED(bvars
.size() == 0, fun
)
6935 << "function or nullary symbol";
6938 //////// all checks before this line
6939 std::vector
<Node
> efuns
= Term::termVectorToNodes(funs
);
6940 std::vector
<std::vector
<Node
>> ebound_vars
;
6941 for (const auto& v
: bound_vars
)
6943 ebound_vars
.push_back(Term::termVectorToNodes(v
));
6945 std::vector
<Node
> nodes
= Term::termVectorToNodes(terms
);
6946 d_slv
->defineFunctionsRec(efuns
, ebound_vars
, nodes
, global
);
6948 CVC5_API_TRY_CATCH_END
;
6951 void Solver::echo(std::ostream
& out
, const std::string
& str
) const
6956 std::vector
<Term
> Solver::getAssertions(void) const
6958 CVC5_API_TRY_CATCH_BEGIN
;
6959 //////// all checks before this line
6960 std::vector
<Node
> assertions
= d_slv
->getAssertions();
6962 * return std::vector<Term>(assertions.begin(), assertions.end());
6963 * here since constructor is private */
6964 std::vector
<Term
> res
;
6965 for (const Node
& e
: assertions
)
6967 res
.push_back(Term(this, e
));
6971 CVC5_API_TRY_CATCH_END
;
6974 std::string
Solver::getInfo(const std::string
& flag
) const
6976 CVC5_API_TRY_CATCH_BEGIN
;
6977 CVC5_API_UNSUPPORTED_CHECK(d_slv
->isValidGetInfoFlag(flag
))
6978 << "Unrecognized flag: " << flag
<< ".";
6979 //////// all checks before this line
6980 return d_slv
->getInfo(flag
);
6982 CVC5_API_TRY_CATCH_END
;
6985 std::string
Solver::getOption(const std::string
& option
) const
6989 return d_slv
->getOption(option
);
6991 catch (OptionException
& e
)
6993 throw CVC5ApiUnsupportedException(e
.getMessage());
6997 // Supports a visitor from a list of lambdas
6998 // Taken from https://en.cppreference.com/w/cpp/utility/variant/visit
6999 template<class... Ts
> struct overloaded
: Ts
... { using Ts::operator()...; };
7000 template<class... Ts
> overloaded(Ts
...) -> overloaded
<Ts
...>;
7002 bool OptionInfo::boolValue() const
7004 CVC5_API_TRY_CATCH_BEGIN
;
7005 CVC5_API_RECOVERABLE_CHECK(std::holds_alternative
<ValueInfo
<bool>>(valueInfo
))
7006 << name
<< " is not a bool option";
7007 //////// all checks before this line
7008 return std::get
<ValueInfo
<bool>>(valueInfo
).currentValue
;
7010 CVC5_API_TRY_CATCH_END
;
7012 std::string
OptionInfo::stringValue() const
7014 CVC5_API_TRY_CATCH_BEGIN
;
7015 CVC5_API_RECOVERABLE_CHECK(
7016 std::holds_alternative
<ValueInfo
<std::string
>>(valueInfo
))
7017 << name
<< " is not a string option";
7018 //////// all checks before this line
7019 return std::get
<ValueInfo
<std::string
>>(valueInfo
).currentValue
;
7021 CVC5_API_TRY_CATCH_END
;
7023 int64_t OptionInfo::intValue() const
7025 CVC5_API_TRY_CATCH_BEGIN
;
7026 CVC5_API_RECOVERABLE_CHECK(
7027 std::holds_alternative
<NumberInfo
<int64_t>>(valueInfo
))
7028 << name
<< " is not an int option";
7029 //////// all checks before this line
7030 return std::get
<NumberInfo
<int64_t>>(valueInfo
).currentValue
;
7032 CVC5_API_TRY_CATCH_END
;
7034 uint64_t OptionInfo::uintValue() const
7036 CVC5_API_TRY_CATCH_BEGIN
;
7037 CVC5_API_RECOVERABLE_CHECK(
7038 std::holds_alternative
<NumberInfo
<uint64_t>>(valueInfo
))
7039 << name
<< " is not a uint option";
7040 //////// all checks before this line
7041 return std::get
<NumberInfo
<uint64_t>>(valueInfo
).currentValue
;
7043 CVC5_API_TRY_CATCH_END
;
7045 double OptionInfo::doubleValue() const
7047 CVC5_API_TRY_CATCH_BEGIN
;
7048 CVC5_API_RECOVERABLE_CHECK(
7049 std::holds_alternative
<NumberInfo
<double>>(valueInfo
))
7050 << name
<< " is not a double option";
7051 //////// all checks before this line
7052 return std::get
<NumberInfo
<double>>(valueInfo
).currentValue
;
7054 CVC5_API_TRY_CATCH_END
;
7057 std::ostream
& operator<<(std::ostream
& os
, const OptionInfo
& oi
)
7059 os
<< "OptionInfo{ " << oi
.name
;
7062 os
<< " | set by user";
7064 if (!oi
.aliases
.empty())
7066 container_to_stream(os
, oi
.aliases
, ", ", "", ", ");
7068 auto printNum
= [&os
](const std::string
& type
, const auto& vi
) {
7069 os
<< " | " << type
<< " | " << vi
.currentValue
<< " | default "
7071 if (vi
.minimum
|| vi
.maximum
)
7076 os
<< " " << *vi
.minimum
<< " <=";
7081 os
<< " <= " << *vi
.maximum
;
7085 std::visit(overloaded
{
7086 [&os
](const OptionInfo::VoidInfo
& vi
) { os
<< " | void"; },
7087 [&os
](const OptionInfo::ValueInfo
<bool>& vi
) {
7088 os
<< " | bool | " << vi
.currentValue
<< " | default "
7091 [&os
](const OptionInfo::ValueInfo
<std::string
>& vi
) {
7092 os
<< " | string | " << vi
.currentValue
<< " | default "
7095 [&printNum
](const OptionInfo::NumberInfo
<int64_t>& vi
) {
7096 printNum("int64_t", vi
);
7098 [&printNum
](const OptionInfo::NumberInfo
<uint64_t>& vi
) {
7099 printNum("uint64_t", vi
);
7101 [&printNum
](const OptionInfo::NumberInfo
<double>& vi
) {
7102 printNum("double", vi
);
7104 [&os
](const OptionInfo::ModeInfo
& vi
) {
7105 os
<< " | mode | " << vi
.currentValue
<< " | default "
7106 << vi
.defaultValue
<< " | modes: ";
7107 container_to_stream(os
, vi
.modes
, "", "", ", ");
7115 std::vector
<std::string
> Solver::getOptionNames() const
7117 CVC5_API_TRY_CATCH_BEGIN
;
7118 //////// all checks before this line
7119 return options::getNames();
7121 CVC5_API_TRY_CATCH_END
;
7124 OptionInfo
Solver::getOptionInfo(const std::string
& option
) const
7126 CVC5_API_TRY_CATCH_BEGIN
;
7127 //////// all checks before this line
7128 auto info
= options::getInfo(d_slv
->getOptions(), option
);
7129 CVC5_API_CHECK(info
.name
!= "")
7130 << "Querying invalid or unknown option " << option
;
7133 [&info
](const options::OptionInfo::VoidInfo
& vi
) {
7134 return OptionInfo
{info
.name
,
7137 OptionInfo::VoidInfo
{}};
7139 [&info
](const options::OptionInfo::ValueInfo
<bool>& vi
) {
7144 OptionInfo::ValueInfo
<bool>{vi
.defaultValue
, vi
.currentValue
}};
7146 [&info
](const options::OptionInfo::ValueInfo
<std::string
>& vi
) {
7147 return OptionInfo
{info
.name
,
7150 OptionInfo::ValueInfo
<std::string
>{
7151 vi
.defaultValue
, vi
.currentValue
}};
7153 [&info
](const options::OptionInfo::NumberInfo
<int64_t>& vi
) {
7158 OptionInfo::NumberInfo
<int64_t>{
7159 vi
.defaultValue
, vi
.currentValue
, vi
.minimum
, vi
.maximum
}};
7161 [&info
](const options::OptionInfo::NumberInfo
<uint64_t>& vi
) {
7166 OptionInfo::NumberInfo
<uint64_t>{
7167 vi
.defaultValue
, vi
.currentValue
, vi
.minimum
, vi
.maximum
}};
7169 [&info
](const options::OptionInfo::NumberInfo
<double>& vi
) {
7174 OptionInfo::NumberInfo
<double>{
7175 vi
.defaultValue
, vi
.currentValue
, vi
.minimum
, vi
.maximum
}};
7177 [&info
](const options::OptionInfo::ModeInfo
& vi
) {
7178 return OptionInfo
{info
.name
,
7181 OptionInfo::ModeInfo
{
7182 vi
.defaultValue
, vi
.currentValue
, vi
.modes
}};
7187 CVC5_API_TRY_CATCH_END
;
7190 DriverOptions
Solver::getDriverOptions() const { return DriverOptions(*this); }
7192 std::vector
<Term
> Solver::getUnsatAssumptions(void) const
7194 CVC5_API_TRY_CATCH_BEGIN
;
7195 CVC5_API_CHECK(d_slv
->getOptions().base
.incrementalSolving
)
7196 << "Cannot get unsat assumptions unless incremental solving is enabled "
7197 "(try --incremental)";
7198 CVC5_API_CHECK(d_slv
->getOptions().smt
.unsatAssumptions
)
7199 << "Cannot get unsat assumptions unless explicitly enabled "
7200 "(try --produce-unsat-assumptions)";
7201 CVC5_API_CHECK(d_slv
->getSmtMode() == SmtMode::UNSAT
)
7202 << "Cannot get unsat assumptions unless in unsat mode.";
7203 //////// all checks before this line
7205 std::vector
<Node
> uassumptions
= d_slv
->getUnsatAssumptions();
7207 * return std::vector<Term>(uassumptions.begin(), uassumptions.end());
7208 * here since constructor is private */
7209 std::vector
<Term
> res
;
7210 for (const Node
& n
: uassumptions
)
7212 res
.push_back(Term(this, n
));
7216 CVC5_API_TRY_CATCH_END
;
7219 std::vector
<Term
> Solver::getUnsatCore(void) const
7221 CVC5_API_TRY_CATCH_BEGIN
;
7222 CVC5_API_CHECK(d_slv
->getOptions().smt
.unsatCores
)
7223 << "Cannot get unsat core unless explicitly enabled "
7224 "(try --produce-unsat-cores)";
7225 CVC5_API_RECOVERABLE_CHECK(d_slv
->getSmtMode() == SmtMode::UNSAT
)
7226 << "Cannot get unsat core unless in unsat mode.";
7227 //////// all checks before this line
7228 UnsatCore core
= d_slv
->getUnsatCore();
7230 * return std::vector<Term>(core.begin(), core.end());
7231 * here since constructor is private */
7232 std::vector
<Term
> res
;
7233 for (const Node
& e
: core
)
7235 res
.push_back(Term(this, e
));
7239 CVC5_API_TRY_CATCH_END
;
7242 std::map
<Term
, Term
> Solver::getDifficulty() const
7244 CVC5_API_TRY_CATCH_BEGIN
;
7245 CVC5_API_RECOVERABLE_CHECK(d_slv
->getSmtMode() == SmtMode::UNSAT
7246 || d_slv
->getSmtMode() == SmtMode::SAT
7247 || d_slv
->getSmtMode() == SmtMode::SAT_UNKNOWN
)
7248 << "Cannot get difficulty unless after a UNSAT, SAT or UNKNOWN response.";
7249 //////// all checks before this line
7250 std::map
<Term
, Term
> res
;
7251 std::map
<Node
, Node
> dmap
;
7252 d_slv
->getDifficultyMap(dmap
);
7253 for (const std::pair
<const Node
, Node
>& d
: dmap
)
7255 res
[Term(this, d
.first
)] = Term(this, d
.second
);
7259 CVC5_API_TRY_CATCH_END
;
7262 std::string
Solver::getProof(void) const
7264 CVC5_API_TRY_CATCH_BEGIN
;
7265 CVC5_API_CHECK(d_slv
->getOptions().smt
.produceProofs
)
7266 << "Cannot get proof unless proofs are enabled (try --produce-proofs)";
7267 CVC5_API_RECOVERABLE_CHECK(d_slv
->getSmtMode() == SmtMode::UNSAT
)
7268 << "Cannot get proof unless in unsat mode.";
7269 return d_slv
->getProof();
7270 CVC5_API_TRY_CATCH_END
;
7273 Term
Solver::getValue(const Term
& term
) const
7275 CVC5_API_TRY_CATCH_BEGIN
;
7276 CVC5_API_RECOVERABLE_CHECK(d_slv
->getOptions().smt
.produceModels
)
7277 << "Cannot get value unless model generation is enabled "
7278 "(try --produce-models)";
7279 CVC5_API_RECOVERABLE_CHECK(d_slv
->isSmtModeSat())
7280 << "Cannot get value unless after a SAT or UNKNOWN response.";
7281 CVC5_API_SOLVER_CHECK_TERM(term
);
7282 CVC5_API_RECOVERABLE_CHECK(term
.getSort().isFirstClass())
7283 << "Cannot get value of a term that is not first class.";
7284 CVC5_API_RECOVERABLE_CHECK(!term
.getSort().isDatatype()
7285 || term
.getSort().getDatatype().isWellFounded())
7286 << "Cannot get value of a term of non-well-founded datatype sort.";
7287 //////// all checks before this line
7288 return getValueHelper(term
);
7290 CVC5_API_TRY_CATCH_END
;
7293 std::vector
<Term
> Solver::getValue(const std::vector
<Term
>& terms
) const
7295 CVC5_API_TRY_CATCH_BEGIN
;
7296 CVC5_API_RECOVERABLE_CHECK(d_slv
->getOptions().smt
.produceModels
)
7297 << "Cannot get value unless model generation is enabled "
7298 "(try --produce-models)";
7299 CVC5_API_RECOVERABLE_CHECK(d_slv
->isSmtModeSat())
7300 << "Cannot get value unless after a SAT or UNKNOWN response.";
7301 for (const Term
& t
: terms
)
7303 CVC5_API_RECOVERABLE_CHECK(t
.getSort().isFirstClass())
7304 << "Cannot get value of a term that is not first class.";
7305 CVC5_API_RECOVERABLE_CHECK(!t
.getSort().isDatatype()
7306 || t
.getSort().getDatatype().isWellFounded())
7307 << "Cannot get value of a term of non-well-founded datatype sort.";
7309 CVC5_API_SOLVER_CHECK_TERMS(terms
);
7310 //////// all checks before this line
7312 std::vector
<Term
> res
;
7313 for (size_t i
= 0, n
= terms
.size(); i
< n
; ++i
)
7315 /* Can not use emplace_back here since constructor is private. */
7316 res
.push_back(getValueHelper(terms
[i
]));
7320 CVC5_API_TRY_CATCH_END
;
7323 std::vector
<Term
> Solver::getModelDomainElements(const Sort
& s
) const
7325 CVC5_API_TRY_CATCH_BEGIN
;
7326 CVC5_API_RECOVERABLE_CHECK(d_slv
->getOptions().smt
.produceModels
)
7327 << "Cannot get domain elements unless model generation is enabled "
7328 "(try --produce-models)";
7329 CVC5_API_RECOVERABLE_CHECK(d_slv
->isSmtModeSat())
7330 << "Cannot get domain elements unless after a SAT or UNKNOWN response.";
7331 CVC5_API_SOLVER_CHECK_SORT(s
);
7332 CVC5_API_RECOVERABLE_CHECK(s
.isUninterpretedSort())
7333 << "Expecting an uninterpreted sort as argument to "
7334 "getModelDomainElements.";
7335 //////// all checks before this line
7336 std::vector
<Term
> res
;
7337 std::vector
<Node
> elements
= d_slv
->getModelDomainElements(s
.getTypeNode());
7338 for (const Node
& n
: elements
)
7340 res
.push_back(Term(this, n
));
7344 CVC5_API_TRY_CATCH_END
;
7347 bool Solver::isModelCoreSymbol(const Term
& v
) const
7349 CVC5_API_TRY_CATCH_BEGIN
;
7350 CVC5_API_RECOVERABLE_CHECK(d_slv
->getOptions().smt
.produceModels
)
7351 << "Cannot check if model core symbol unless model generation is enabled "
7352 "(try --produce-models)";
7353 CVC5_API_RECOVERABLE_CHECK(d_slv
->isSmtModeSat())
7354 << "Cannot check if model core symbol unless after a SAT or UNKNOWN "
7356 CVC5_API_SOLVER_CHECK_TERM(v
);
7357 CVC5_API_RECOVERABLE_CHECK(v
.getKind() == CONSTANT
)
7358 << "Expecting a free constant as argument to isModelCoreSymbol.";
7359 //////// all checks before this line
7360 return d_slv
->isModelCoreSymbol(v
.getNode());
7362 CVC5_API_TRY_CATCH_END
;
7365 std::string
Solver::getModel(const std::vector
<Sort
>& sorts
,
7366 const std::vector
<Term
>& vars
) const
7368 CVC5_API_TRY_CATCH_BEGIN
;
7369 CVC5_API_RECOVERABLE_CHECK(d_slv
->getOptions().smt
.produceModels
)
7370 << "Cannot get model unless model generation is enabled "
7371 "(try --produce-models)";
7372 CVC5_API_RECOVERABLE_CHECK(d_slv
->isSmtModeSat())
7373 << "Cannot get model unless after a SAT or UNKNOWN response.";
7374 CVC5_API_SOLVER_CHECK_SORTS(sorts
);
7375 for (const Sort
& s
: sorts
)
7377 CVC5_API_RECOVERABLE_CHECK(s
.isUninterpretedSort())
7378 << "Expecting an uninterpreted sort as argument to "
7381 CVC5_API_SOLVER_CHECK_TERMS(vars
);
7382 for (const Term
& v
: vars
)
7384 CVC5_API_RECOVERABLE_CHECK(v
.getKind() == CONSTANT
)
7385 << "Expecting a free constant as argument to getModel.";
7387 //////// all checks before this line
7388 return d_slv
->getModel(Sort::sortVectorToTypeNodes(sorts
),
7389 Term::termVectorToNodes(vars
));
7391 CVC5_API_TRY_CATCH_END
;
7394 Term
Solver::getQuantifierElimination(const Term
& q
) const
7396 CVC5_API_TRY_CATCH_BEGIN
;
7397 CVC5_API_SOLVER_CHECK_TERM(q
);
7398 //////// all checks before this line
7399 return Term(this, d_slv
->getQuantifierElimination(q
.getNode(), true));
7401 CVC5_API_TRY_CATCH_END
;
7404 Term
Solver::getQuantifierEliminationDisjunct(const Term
& q
) const
7406 CVC5_API_TRY_CATCH_BEGIN
;
7407 CVC5_API_SOLVER_CHECK_TERM(q
);
7408 //////// all checks before this line
7409 return Term(this, d_slv
->getQuantifierElimination(q
.getNode(), false));
7411 CVC5_API_TRY_CATCH_END
;
7414 void Solver::declareSepHeap(const Sort
& locSort
, const Sort
& dataSort
) const
7416 CVC5_API_TRY_CATCH_BEGIN
;
7417 CVC5_API_SOLVER_CHECK_SORT(locSort
);
7418 CVC5_API_SOLVER_CHECK_SORT(dataSort
);
7419 CVC5_API_CHECK(d_slv
->getLogicInfo().isTheoryEnabled(theory::THEORY_SEP
))
7420 << "Cannot obtain separation logic expressions if not using the "
7421 "separation logic theory.";
7422 //////// all checks before this line
7423 d_slv
->declareSepHeap(locSort
.getTypeNode(), dataSort
.getTypeNode());
7425 CVC5_API_TRY_CATCH_END
;
7428 Term
Solver::getValueSepHeap() const
7430 CVC5_API_TRY_CATCH_BEGIN
;
7431 CVC5_API_CHECK(d_slv
->getLogicInfo().isTheoryEnabled(theory::THEORY_SEP
))
7432 << "Cannot obtain separation logic expressions if not using the "
7433 "separation logic theory.";
7434 CVC5_API_CHECK(d_slv
->getOptions().smt
.produceModels
)
7435 << "Cannot get separation heap term unless model generation is enabled "
7436 "(try --produce-models)";
7437 CVC5_API_RECOVERABLE_CHECK(d_slv
->isSmtModeSat())
7438 << "Can only get separtion heap term after SAT or UNKNOWN response.";
7439 //////// all checks before this line
7440 return Term(this, d_slv
->getSepHeapExpr());
7442 CVC5_API_TRY_CATCH_END
;
7445 Term
Solver::getValueSepNil() const
7447 CVC5_API_TRY_CATCH_BEGIN
;
7448 CVC5_API_CHECK(d_slv
->getLogicInfo().isTheoryEnabled(theory::THEORY_SEP
))
7449 << "Cannot obtain separation logic expressions if not using the "
7450 "separation logic theory.";
7451 CVC5_API_CHECK(d_slv
->getOptions().smt
.produceModels
)
7452 << "Cannot get separation nil term unless model generation is enabled "
7453 "(try --produce-models)";
7454 CVC5_API_RECOVERABLE_CHECK(d_slv
->isSmtModeSat())
7455 << "Can only get separtion nil term after SAT or UNKNOWN response.";
7456 //////// all checks before this line
7457 return Term(this, d_slv
->getSepNilExpr());
7459 CVC5_API_TRY_CATCH_END
;
7462 Term
Solver::declarePool(const std::string
& symbol
,
7464 const std::vector
<Term
>& initValue
) const
7466 CVC5_API_TRY_CATCH_BEGIN
;
7467 CVC5_API_SOLVER_CHECK_SORT(sort
);
7468 CVC5_API_SOLVER_CHECK_TERMS(initValue
);
7469 //////// all checks before this line
7470 TypeNode setType
= getNodeManager()->mkSetType(*sort
.d_type
);
7471 Node pool
= getNodeManager()->mkBoundVar(symbol
, setType
);
7472 std::vector
<Node
> initv
= Term::termVectorToNodes(initValue
);
7473 d_slv
->declarePool(pool
, initv
);
7474 return Term(this, pool
);
7476 CVC5_API_TRY_CATCH_END
;
7479 void Solver::pop(uint32_t nscopes
) const
7481 CVC5_API_TRY_CATCH_BEGIN
;
7482 CVC5_API_CHECK(d_slv
->getOptions().base
.incrementalSolving
)
7483 << "Cannot pop when not solving incrementally (use --incremental)";
7484 CVC5_API_CHECK(nscopes
<= d_slv
->getNumUserLevels())
7485 << "Cannot pop beyond first pushed context";
7486 //////// all checks before this line
7487 for (uint32_t n
= 0; n
< nscopes
; ++n
)
7492 CVC5_API_TRY_CATCH_END
;
7495 bool Solver::getInterpolant(const Term
& conj
, Term
& output
) const
7497 CVC5_API_TRY_CATCH_BEGIN
;
7498 CVC5_API_SOLVER_CHECK_TERM(conj
);
7499 CVC5_API_CHECK(d_slv
->getOptions().smt
.produceInterpols
7500 != options::ProduceInterpols::NONE
)
7501 << "Cannot get interpolant unless interpolants are enabled (try "
7502 "--produce-interpols=mode)";
7503 //////// all checks before this line
7506 bool success
= d_slv
->getInterpolant(*conj
.d_node
, nullType
, result
);
7509 output
= Term(this, result
);
7513 CVC5_API_TRY_CATCH_END
;
7516 bool Solver::getInterpolant(const Term
& conj
,
7520 CVC5_API_TRY_CATCH_BEGIN
;
7521 CVC5_API_SOLVER_CHECK_TERM(conj
);
7522 CVC5_API_CHECK(d_slv
->getOptions().smt
.produceInterpols
7523 != options::ProduceInterpols::NONE
)
7524 << "Cannot get interpolant unless interpolants are enabled (try "
7525 "--produce-interpols=mode)";
7526 //////// all checks before this line
7529 d_slv
->getInterpolant(*conj
.d_node
, *grammar
.resolve().d_type
, result
);
7532 output
= Term(this, result
);
7536 CVC5_API_TRY_CATCH_END
;
7539 bool Solver::getInterpolantNext(Term
& output
) const
7541 CVC5_API_TRY_CATCH_BEGIN
;
7542 CVC5_API_CHECK(d_slv
->getOptions().smt
.produceInterpols
7543 != options::ProduceInterpols::NONE
)
7544 << "Cannot get interpolant unless interpolants are enabled (try "
7545 "--produce-interpols=mode)";
7546 CVC5_API_CHECK(d_slv
->getOptions().base
.incrementalSolving
)
7547 << "Cannot get next interpolant when not solving incrementally (try "
7549 //////// all checks before this line
7551 bool success
= d_slv
->getInterpolantNext(result
);
7554 output
= Term(this, result
);
7558 CVC5_API_TRY_CATCH_END
;
7561 bool Solver::getAbduct(const Term
& conj
, Term
& output
) const
7563 CVC5_API_TRY_CATCH_BEGIN
;
7564 CVC5_API_SOLVER_CHECK_TERM(conj
);
7565 CVC5_API_CHECK(d_slv
->getOptions().smt
.produceAbducts
)
7566 << "Cannot get abduct unless abducts are enabled (try --produce-abducts)";
7567 //////// all checks before this line
7570 bool success
= d_slv
->getAbduct(*conj
.d_node
, nullType
, result
);
7573 output
= Term(this, result
);
7577 CVC5_API_TRY_CATCH_END
;
7580 bool Solver::getAbduct(const Term
& conj
, Grammar
& grammar
, Term
& output
) const
7582 CVC5_API_TRY_CATCH_BEGIN
;
7583 CVC5_API_SOLVER_CHECK_TERM(conj
);
7584 CVC5_API_CHECK(d_slv
->getOptions().smt
.produceAbducts
)
7585 << "Cannot get abduct unless abducts are enabled (try --produce-abducts)";
7586 //////// all checks before this line
7589 d_slv
->getAbduct(*conj
.d_node
, *grammar
.resolve().d_type
, result
);
7592 output
= Term(this, result
);
7596 CVC5_API_TRY_CATCH_END
;
7599 bool Solver::getAbductNext(Term
& output
) const
7601 CVC5_API_TRY_CATCH_BEGIN
;
7602 CVC5_API_CHECK(d_slv
->getOptions().smt
.produceAbducts
)
7603 << "Cannot get next abduct unless abducts are enabled (try "
7604 "--produce-abducts)";
7605 CVC5_API_CHECK(d_slv
->getOptions().base
.incrementalSolving
)
7606 << "Cannot get next abduct when not solving incrementally (try "
7608 //////// all checks before this line
7610 bool success
= d_slv
->getAbductNext(result
);
7613 output
= Term(this, result
);
7617 CVC5_API_TRY_CATCH_END
;
7620 void Solver::blockModel() const
7622 CVC5_API_TRY_CATCH_BEGIN
;
7623 CVC5_API_CHECK(d_slv
->getOptions().smt
.produceModels
)
7624 << "Cannot get value unless model generation is enabled "
7625 "(try --produce-models)";
7626 CVC5_API_RECOVERABLE_CHECK(d_slv
->isSmtModeSat())
7627 << "Can only block model after SAT or UNKNOWN response.";
7628 //////// all checks before this line
7629 d_slv
->blockModel();
7631 CVC5_API_TRY_CATCH_END
;
7634 void Solver::blockModelValues(const std::vector
<Term
>& terms
) const
7636 CVC5_API_TRY_CATCH_BEGIN
;
7637 CVC5_API_CHECK(d_slv
->getOptions().smt
.produceModels
)
7638 << "Cannot get value unless model generation is enabled "
7639 "(try --produce-models)";
7640 CVC5_API_RECOVERABLE_CHECK(d_slv
->isSmtModeSat())
7641 << "Can only block model values after SAT or UNKNOWN response.";
7642 CVC5_API_ARG_SIZE_CHECK_EXPECTED(!terms
.empty(), terms
)
7643 << "a non-empty set of terms";
7644 CVC5_API_SOLVER_CHECK_TERMS(terms
);
7645 //////// all checks before this line
7646 d_slv
->blockModelValues(Term::termVectorToNodes(terms
));
7648 CVC5_API_TRY_CATCH_END
;
7651 void Solver::printInstantiations(std::ostream
& out
) const
7653 CVC5_API_TRY_CATCH_BEGIN
;
7654 //////// all checks before this line
7655 d_slv
->printInstantiations(out
);
7657 CVC5_API_TRY_CATCH_END
;
7660 void Solver::push(uint32_t nscopes
) const
7662 CVC5_API_TRY_CATCH_BEGIN
;
7663 CVC5_API_CHECK(d_slv
->getOptions().base
.incrementalSolving
)
7664 << "Cannot push when not solving incrementally (use --incremental)";
7665 //////// all checks before this line
7666 for (uint32_t n
= 0; n
< nscopes
; ++n
)
7671 CVC5_API_TRY_CATCH_END
;
7674 void Solver::resetAssertions(void) const
7676 CVC5_API_TRY_CATCH_BEGIN
;
7677 //////// all checks before this line
7678 d_slv
->resetAssertions();
7680 CVC5_API_TRY_CATCH_END
;
7683 void Solver::setInfo(const std::string
& keyword
, const std::string
& value
) const
7685 CVC5_API_TRY_CATCH_BEGIN
;
7686 CVC5_API_UNSUPPORTED_CHECK(
7687 keyword
== "source" || keyword
== "category" || keyword
== "difficulty"
7688 || keyword
== "filename" || keyword
== "license" || keyword
== "name"
7689 || keyword
== "notes" || keyword
== "smt-lib-version"
7690 || keyword
== "status")
7691 << "Unrecognized keyword: " << keyword
7692 << ", expected 'source', 'category', 'difficulty', "
7693 "'filename', 'license', 'name', "
7694 "'notes', 'smt-lib-version' or 'status'";
7695 CVC5_API_RECOVERABLE_ARG_CHECK_EXPECTED(
7696 keyword
!= "smt-lib-version" || value
== "2" || value
== "2.0"
7697 || value
== "2.5" || value
== "2.6",
7699 << "'2.0', '2.5', '2.6'";
7700 CVC5_API_ARG_CHECK_EXPECTED(keyword
!= "status" || value
== "sat"
7701 || value
== "unsat" || value
== "unknown",
7703 << "'sat', 'unsat' or 'unknown'";
7704 //////// all checks before this line
7705 d_slv
->setInfo(keyword
, value
);
7707 CVC5_API_TRY_CATCH_END
;
7710 void Solver::setLogic(const std::string
& logic
) const
7712 CVC5_API_TRY_CATCH_BEGIN
;
7713 CVC5_API_CHECK(!d_slv
->isFullyInited())
7714 << "Invalid call to 'setLogic', solver is already fully initialized";
7715 cvc5::LogicInfo
logic_info(logic
);
7716 //////// all checks before this line
7717 d_slv
->setLogic(logic_info
);
7719 CVC5_API_TRY_CATCH_END
;
7722 void Solver::setOption(const std::string
& option
,
7723 const std::string
& value
) const
7725 CVC5_API_TRY_CATCH_BEGIN
;
7726 std::vector
<std::string
> options
= options::getNames();
7727 CVC5_API_UNSUPPORTED_CHECK(
7728 option
.find("command-verbosity") != std::string::npos
7729 || std::find(options
.cbegin(), options
.cend(), option
) != options
.cend())
7730 << "Unrecognized option: " << option
<< '.';
7731 static constexpr auto mutableOpts
= {"diagnostic-output-channel",
7733 "regular-output-channel",
7734 "reproducible-resource-limit",
7736 if (std::find(mutableOpts
.begin(), mutableOpts
.end(), option
)
7737 == mutableOpts
.end())
7739 CVC5_API_CHECK(!d_slv
->isFullyInited())
7740 << "Invalid call to 'setOption' for option '" << option
7741 << "', solver is already fully initialized";
7743 //////// all checks before this line
7744 d_slv
->setOption(option
, value
);
7746 CVC5_API_TRY_CATCH_END
;
7749 Term
Solver::mkSygusVar(const Sort
& sort
, const std::string
& symbol
) const
7751 CVC5_API_TRY_CATCH_BEGIN
;
7752 CVC5_API_SOLVER_CHECK_SORT(sort
);
7753 //////// all checks before this line
7754 Node res
= getNodeManager()->mkBoundVar(symbol
, *sort
.d_type
);
7755 (void)res
.getType(true); /* kick off type checking */
7757 d_slv
->declareSygusVar(res
);
7759 return Term(this, res
);
7761 CVC5_API_TRY_CATCH_END
;
7764 Grammar
Solver::mkSygusGrammar(const std::vector
<Term
>& boundVars
,
7765 const std::vector
<Term
>& ntSymbols
) const
7767 CVC5_API_TRY_CATCH_BEGIN
;
7768 CVC5_API_ARG_SIZE_CHECK_EXPECTED(!ntSymbols
.empty(), ntSymbols
)
7769 << "a non-empty vector";
7770 CVC5_API_SOLVER_CHECK_BOUND_VARS(boundVars
);
7771 CVC5_API_SOLVER_CHECK_BOUND_VARS(ntSymbols
);
7772 //////// all checks before this line
7773 return Grammar(this, boundVars
, ntSymbols
);
7775 CVC5_API_TRY_CATCH_END
;
7778 Term
Solver::synthFun(const std::string
& symbol
,
7779 const std::vector
<Term
>& boundVars
,
7780 const Sort
& sort
) const
7782 CVC5_API_TRY_CATCH_BEGIN
;
7783 CVC5_API_SOLVER_CHECK_BOUND_VARS(boundVars
);
7784 CVC5_API_SOLVER_CHECK_SORT(sort
);
7785 //////// all checks before this line
7786 return synthFunHelper(symbol
, boundVars
, sort
);
7788 CVC5_API_TRY_CATCH_END
;
7791 Term
Solver::synthFun(const std::string
& symbol
,
7792 const std::vector
<Term
>& boundVars
,
7794 Grammar
& grammar
) const
7796 CVC5_API_TRY_CATCH_BEGIN
;
7797 CVC5_API_SOLVER_CHECK_BOUND_VARS(boundVars
);
7798 CVC5_API_SOLVER_CHECK_SORT(sort
);
7799 //////// all checks before this line
7800 return synthFunHelper(symbol
, boundVars
, sort
, false, &grammar
);
7802 CVC5_API_TRY_CATCH_END
;
7805 Term
Solver::synthInv(const std::string
& symbol
,
7806 const std::vector
<Term
>& boundVars
) const
7808 CVC5_API_TRY_CATCH_BEGIN
;
7809 CVC5_API_SOLVER_CHECK_BOUND_VARS(boundVars
);
7810 //////// all checks before this line
7811 return synthFunHelper(
7812 symbol
, boundVars
, Sort(this, getNodeManager()->booleanType()), true);
7814 CVC5_API_TRY_CATCH_END
;
7817 Term
Solver::synthInv(const std::string
& symbol
,
7818 const std::vector
<Term
>& boundVars
,
7819 Grammar
& grammar
) const
7821 CVC5_API_TRY_CATCH_BEGIN
;
7822 CVC5_API_SOLVER_CHECK_BOUND_VARS(boundVars
);
7823 //////// all checks before this line
7824 return synthFunHelper(symbol
,
7826 Sort(this, getNodeManager()->booleanType()),
7830 CVC5_API_TRY_CATCH_END
;
7833 void Solver::addSygusConstraint(const Term
& term
) const
7835 CVC5_API_TRY_CATCH_BEGIN
;
7836 CVC5_API_SOLVER_CHECK_TERM(term
);
7837 CVC5_API_ARG_CHECK_EXPECTED(
7838 term
.d_node
->getType() == getNodeManager()->booleanType(), term
)
7840 //////// all checks before this line
7841 d_slv
->assertSygusConstraint(*term
.d_node
, false);
7843 CVC5_API_TRY_CATCH_END
;
7846 void Solver::addSygusAssume(const Term
& term
) const
7848 CVC5_API_TRY_CATCH_BEGIN
;
7849 CVC5_API_SOLVER_CHECK_TERM(term
);
7850 CVC5_API_ARG_CHECK_EXPECTED(
7851 term
.d_node
->getType() == getNodeManager()->booleanType(), term
)
7853 //////// all checks before this line
7854 d_slv
->assertSygusConstraint(*term
.d_node
, true);
7856 CVC5_API_TRY_CATCH_END
;
7859 void Solver::addSygusInvConstraint(Term inv
,
7864 CVC5_API_TRY_CATCH_BEGIN
;
7865 CVC5_API_SOLVER_CHECK_TERM(inv
);
7866 CVC5_API_SOLVER_CHECK_TERM(pre
);
7867 CVC5_API_SOLVER_CHECK_TERM(trans
);
7868 CVC5_API_SOLVER_CHECK_TERM(post
);
7870 CVC5_API_ARG_CHECK_EXPECTED(inv
.d_node
->getType().isFunction(), inv
)
7873 TypeNode invType
= inv
.d_node
->getType();
7875 CVC5_API_ARG_CHECK_EXPECTED(invType
.getRangeType().isBoolean(), inv
)
7878 CVC5_API_CHECK(pre
.d_node
->getType() == invType
)
7879 << "Expected inv and pre to have the same sort";
7881 CVC5_API_CHECK(post
.d_node
->getType() == invType
)
7882 << "Expected inv and post to have the same sort";
7883 //////// all checks before this line
7885 const std::vector
<TypeNode
>& invArgTypes
= invType
.getArgTypes();
7887 std::vector
<TypeNode
> expectedTypes
;
7888 expectedTypes
.reserve(2 * invArgTypes
.size() + 1);
7890 for (size_t i
= 0, n
= invArgTypes
.size(); i
< 2 * n
; i
+= 2)
7892 expectedTypes
.push_back(invArgTypes
[i
% n
]);
7893 expectedTypes
.push_back(invArgTypes
[(i
+ 1) % n
]);
7896 expectedTypes
.push_back(invType
.getRangeType());
7897 TypeNode expectedTransType
= getNodeManager()->mkFunctionType(expectedTypes
);
7899 CVC5_API_CHECK(trans
.d_node
->getType() == expectedTransType
)
7900 << "Expected trans's sort to be " << invType
;
7902 d_slv
->assertSygusInvConstraint(
7903 *inv
.d_node
, *pre
.d_node
, *trans
.d_node
, *post
.d_node
);
7905 CVC5_API_TRY_CATCH_END
;
7908 Result
Solver::checkSynth() const
7910 CVC5_API_TRY_CATCH_BEGIN
;
7911 //////// all checks before this line
7912 return d_slv
->checkSynth();
7914 CVC5_API_TRY_CATCH_END
;
7917 Result
Solver::checkSynthNext() const
7919 CVC5_API_TRY_CATCH_BEGIN
;
7920 CVC5_API_CHECK(d_slv
->getOptions().base
.incrementalSolving
)
7921 << "Cannot checkSynthNext when not solving incrementally (use "
7923 //////// all checks before this line
7924 return d_slv
->checkSynth(true);
7926 CVC5_API_TRY_CATCH_END
;
7929 Term
Solver::getSynthSolution(Term term
) const
7931 CVC5_API_TRY_CATCH_BEGIN
;
7932 CVC5_API_SOLVER_CHECK_TERM(term
);
7934 std::map
<cvc5::Node
, cvc5::Node
> map
;
7935 CVC5_API_CHECK(d_slv
->getSynthSolutions(map
))
7936 << "The solver is not in a state immediately preceded by a "
7937 "successful call to checkSynth";
7939 std::map
<cvc5::Node
, cvc5::Node
>::const_iterator it
= map
.find(*term
.d_node
);
7941 CVC5_API_CHECK(it
!= map
.cend()) << "Synth solution not found for given term";
7942 //////// all checks before this line
7943 return Term(this, it
->second
);
7945 CVC5_API_TRY_CATCH_END
;
7948 std::vector
<Term
> Solver::getSynthSolutions(
7949 const std::vector
<Term
>& terms
) const
7951 CVC5_API_TRY_CATCH_BEGIN
;
7952 CVC5_API_ARG_SIZE_CHECK_EXPECTED(!terms
.empty(), terms
) << "non-empty vector";
7953 CVC5_API_SOLVER_CHECK_TERMS(terms
);
7955 std::map
<cvc5::Node
, cvc5::Node
> map
;
7956 CVC5_API_CHECK(d_slv
->getSynthSolutions(map
))
7957 << "The solver is not in a state immediately preceded by a "
7958 "successful call to checkSynth";
7959 //////// all checks before this line
7961 std::vector
<Term
> synthSolution
;
7962 synthSolution
.reserve(terms
.size());
7964 for (size_t i
= 0, n
= terms
.size(); i
< n
; ++i
)
7966 std::map
<cvc5::Node
, cvc5::Node
>::const_iterator it
=
7967 map
.find(*terms
[i
].d_node
);
7969 CVC5_API_CHECK(it
!= map
.cend())
7970 << "Synth solution not found for term at index " << i
;
7972 synthSolution
.push_back(Term(this, it
->second
));
7975 return synthSolution
;
7977 CVC5_API_TRY_CATCH_END
;
7980 Statistics
Solver::getStatistics() const
7982 return Statistics(d_slv
->getStatisticsRegistry());
7985 bool Solver::isOutputOn(const std::string
& tag
) const
7987 // `isOutputOn(tag)` may raise an `OptionException`, which we do not want to
7988 // forward as such. We thus do not use the standard exception handling macros
7989 // here but roll our own.
7992 return d_slv
->getEnv().isOutputOn(tag
);
7994 catch (const cvc5::Exception
& e
)
7996 throw CVC5ApiException("Invalid output tag " + tag
);
8000 std::ostream
& Solver::getOutput(const std::string
& tag
) const
8002 // `output(tag)` may raise an `OptionException`, which we do not want to
8003 // forward as such. We thus do not use the standard exception handling macros
8004 // here but roll our own.
8007 return d_slv
->getEnv().output(tag
);
8009 catch (const cvc5::Exception
& e
)
8011 throw CVC5ApiException("Invalid output tag " + tag
);
8021 size_t hash
<cvc5::api::Kind
>::operator()(cvc5::api::Kind k
) const
8023 return static_cast<size_t>(k
);
8026 size_t hash
<cvc5::api::Op
>::operator()(const cvc5::api::Op
& t
) const
8028 if (t
.isIndexedHelper())
8030 return std::hash
<cvc5::Node
>()(*t
.d_node
);
8034 return std::hash
<cvc5::api::Kind
>()(t
.d_kind
);
8038 size_t std::hash
<cvc5::api::RoundingMode
>::operator()(
8039 cvc5::api::RoundingMode rm
) const
8041 return static_cast<size_t>(rm
);
8044 size_t std::hash
<cvc5::api::Sort
>::operator()(const cvc5::api::Sort
& s
) const
8046 return std::hash
<cvc5::TypeNode
>()(*s
.d_type
);
8049 size_t std::hash
<cvc5::api::Term
>::operator()(const cvc5::api::Term
& t
) const
8051 return std::hash
<cvc5::Node
>()(*t
.d_node
);