1 /******************************************************************************
2 * Top contributors (to current version):
3 * Aina Niemetz, Andrew Reynolds, Andres Noetzli
5 * This file is part of the cvc5 project.
7 * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
8 * in the top-level source directory and their institutional affiliations.
9 * All rights reserved. See the file COPYING in the top-level source
10 * directory for licensing information.
11 * ****************************************************************************
15 * A brief note on how to guard API functions:
17 * In general, we think of API guards as a fence -- they are supposed to make
18 * sure that no invalid arguments get passed into internal realms of cvc5.
19 * Thus we always want to catch such cases on the API level (and can then
20 * assert internally that no invalid argument is passed in).
22 * The only special case is when we use 3rd party back-ends we have no control
23 * over, and which throw (invalid_argument) exceptions anyways. In this case,
24 * we do not replicate argument checks but delegate them to the back-end,
25 * catch thrown exceptions, and raise a CVC5ApiException.
27 * Our Integer implementation, e.g., is such a special case since we support
28 * two different back end implementations (GMP, CLN). Be aware that they do
29 * not fully agree on what is (in)valid input, which requires extra checks for
30 * consistent behavior (see Solver::mkRealOrIntegerFromStrHelper for example).
33 #include "api/cpp/cvc5.h"
38 #include "api/cpp/cvc5_checks.h"
39 #include "base/check.h"
40 #include "base/configuration.h"
41 #include "base/modal_exception.h"
42 #include "expr/array_store_all.h"
43 #include "expr/ascription_type.h"
44 #include "expr/cardinality_constraint.h"
45 #include "expr/dtype.h"
46 #include "expr/dtype_cons.h"
47 #include "expr/dtype_selector.h"
48 #include "expr/emptybag.h"
49 #include "expr/emptyset.h"
50 #include "expr/kind.h"
51 #include "expr/metakind.h"
52 #include "expr/node.h"
53 #include "expr/node_algorithm.h"
54 #include "expr/node_builder.h"
55 #include "expr/node_manager.h"
56 #include "expr/node_manager_attributes.h"
57 #include "expr/sequence.h"
58 #include "expr/type_node.h"
59 #include "expr/uninterpreted_constant.h"
60 #include "options/base_options.h"
61 #include "options/main_options.h"
62 #include "options/option_exception.h"
63 #include "options/options.h"
64 #include "options/options_public.h"
65 #include "options/smt_options.h"
66 #include "proof/unsat_core.h"
68 #include "smt/model.h"
69 #include "smt/smt_mode.h"
70 #include "smt/solver_engine.h"
71 #include "theory/datatypes/tuple_project_op.h"
72 #include "theory/logic_info.h"
73 #include "theory/theory_model.h"
74 #include "util/abstract_value.h"
75 #include "util/bitvector.h"
76 #include "util/divisible.h"
77 #include "util/floatingpoint.h"
78 #include "util/iand.h"
79 #include "util/random.h"
80 #include "util/regexp.h"
81 #include "util/result.h"
82 #include "util/roundingmode.h"
83 #include "util/statistics_registry.h"
84 #include "util/statistics_stats.h"
85 #include "util/statistics_value.h"
86 #include "util/string.h"
87 #include "util/utility.h"
92 /* -------------------------------------------------------------------------- */
94 /* -------------------------------------------------------------------------- */
98 HistogramStat
<TypeConstant
> d_consts
;
99 HistogramStat
<TypeConstant
> d_vars
;
100 HistogramStat
<Kind
> d_terms
;
103 /* -------------------------------------------------------------------------- */
105 /* -------------------------------------------------------------------------- */
107 /* Mapping from external (API) kind to internal kind. */
108 const static std::unordered_map
<Kind
, cvc5::Kind
> s_kinds
{
109 {INTERNAL_KIND
, cvc5::Kind::UNDEFINED_KIND
},
110 {UNDEFINED_KIND
, cvc5::Kind::UNDEFINED_KIND
},
111 {NULL_EXPR
, cvc5::Kind::NULL_EXPR
},
112 /* Builtin ------------------------------------------------------------- */
113 {UNINTERPRETED_CONSTANT
, cvc5::Kind::UNINTERPRETED_CONSTANT
},
114 {ABSTRACT_VALUE
, cvc5::Kind::ABSTRACT_VALUE
},
115 {EQUAL
, cvc5::Kind::EQUAL
},
116 {DISTINCT
, cvc5::Kind::DISTINCT
},
117 {CONSTANT
, cvc5::Kind::VARIABLE
},
118 {VARIABLE
, cvc5::Kind::BOUND_VARIABLE
},
119 {SEXPR
, cvc5::Kind::SEXPR
},
120 {LAMBDA
, cvc5::Kind::LAMBDA
},
121 {WITNESS
, cvc5::Kind::WITNESS
},
122 /* Boolean ------------------------------------------------------------- */
123 {CONST_BOOLEAN
, cvc5::Kind::CONST_BOOLEAN
},
124 {NOT
, cvc5::Kind::NOT
},
125 {AND
, cvc5::Kind::AND
},
126 {IMPLIES
, cvc5::Kind::IMPLIES
},
127 {OR
, cvc5::Kind::OR
},
128 {XOR
, cvc5::Kind::XOR
},
129 {ITE
, cvc5::Kind::ITE
},
130 /* UF ------------------------------------------------------------------ */
131 {APPLY_UF
, cvc5::Kind::APPLY_UF
},
132 {CARDINALITY_CONSTRAINT
, cvc5::Kind::CARDINALITY_CONSTRAINT
},
133 {HO_APPLY
, cvc5::Kind::HO_APPLY
},
134 /* Arithmetic ---------------------------------------------------------- */
135 {PLUS
, cvc5::Kind::PLUS
},
136 {MULT
, cvc5::Kind::MULT
},
137 {IAND
, cvc5::Kind::IAND
},
138 {POW2
, cvc5::Kind::POW2
},
139 {MINUS
, cvc5::Kind::MINUS
},
140 {UMINUS
, cvc5::Kind::UMINUS
},
141 {DIVISION
, cvc5::Kind::DIVISION
},
142 {INTS_DIVISION
, cvc5::Kind::INTS_DIVISION
},
143 {INTS_MODULUS
, cvc5::Kind::INTS_MODULUS
},
144 {ABS
, cvc5::Kind::ABS
},
145 {DIVISIBLE
, cvc5::Kind::DIVISIBLE
},
146 {POW
, cvc5::Kind::POW
},
147 {EXPONENTIAL
, cvc5::Kind::EXPONENTIAL
},
148 {SINE
, cvc5::Kind::SINE
},
149 {COSINE
, cvc5::Kind::COSINE
},
150 {TANGENT
, cvc5::Kind::TANGENT
},
151 {COSECANT
, cvc5::Kind::COSECANT
},
152 {SECANT
, cvc5::Kind::SECANT
},
153 {COTANGENT
, cvc5::Kind::COTANGENT
},
154 {ARCSINE
, cvc5::Kind::ARCSINE
},
155 {ARCCOSINE
, cvc5::Kind::ARCCOSINE
},
156 {ARCTANGENT
, cvc5::Kind::ARCTANGENT
},
157 {ARCCOSECANT
, cvc5::Kind::ARCCOSECANT
},
158 {ARCSECANT
, cvc5::Kind::ARCSECANT
},
159 {ARCCOTANGENT
, cvc5::Kind::ARCCOTANGENT
},
160 {SQRT
, cvc5::Kind::SQRT
},
161 {CONST_RATIONAL
, cvc5::Kind::CONST_RATIONAL
},
162 {LT
, cvc5::Kind::LT
},
163 {LEQ
, cvc5::Kind::LEQ
},
164 {GT
, cvc5::Kind::GT
},
165 {GEQ
, cvc5::Kind::GEQ
},
166 {IS_INTEGER
, cvc5::Kind::IS_INTEGER
},
167 {TO_INTEGER
, cvc5::Kind::TO_INTEGER
},
168 {TO_REAL
, cvc5::Kind::TO_REAL
},
169 {PI
, cvc5::Kind::PI
},
170 /* BV ------------------------------------------------------------------ */
171 {CONST_BITVECTOR
, cvc5::Kind::CONST_BITVECTOR
},
172 {BITVECTOR_CONCAT
, cvc5::Kind::BITVECTOR_CONCAT
},
173 {BITVECTOR_AND
, cvc5::Kind::BITVECTOR_AND
},
174 {BITVECTOR_OR
, cvc5::Kind::BITVECTOR_OR
},
175 {BITVECTOR_XOR
, cvc5::Kind::BITVECTOR_XOR
},
176 {BITVECTOR_NOT
, cvc5::Kind::BITVECTOR_NOT
},
177 {BITVECTOR_NAND
, cvc5::Kind::BITVECTOR_NAND
},
178 {BITVECTOR_NOR
, cvc5::Kind::BITVECTOR_NOR
},
179 {BITVECTOR_XNOR
, cvc5::Kind::BITVECTOR_XNOR
},
180 {BITVECTOR_COMP
, cvc5::Kind::BITVECTOR_COMP
},
181 {BITVECTOR_MULT
, cvc5::Kind::BITVECTOR_MULT
},
182 {BITVECTOR_ADD
, cvc5::Kind::BITVECTOR_ADD
},
183 {BITVECTOR_SUB
, cvc5::Kind::BITVECTOR_SUB
},
184 {BITVECTOR_NEG
, cvc5::Kind::BITVECTOR_NEG
},
185 {BITVECTOR_UDIV
, cvc5::Kind::BITVECTOR_UDIV
},
186 {BITVECTOR_UREM
, cvc5::Kind::BITVECTOR_UREM
},
187 {BITVECTOR_SDIV
, cvc5::Kind::BITVECTOR_SDIV
},
188 {BITVECTOR_SREM
, cvc5::Kind::BITVECTOR_SREM
},
189 {BITVECTOR_SMOD
, cvc5::Kind::BITVECTOR_SMOD
},
190 {BITVECTOR_SHL
, cvc5::Kind::BITVECTOR_SHL
},
191 {BITVECTOR_LSHR
, cvc5::Kind::BITVECTOR_LSHR
},
192 {BITVECTOR_ASHR
, cvc5::Kind::BITVECTOR_ASHR
},
193 {BITVECTOR_ULT
, cvc5::Kind::BITVECTOR_ULT
},
194 {BITVECTOR_ULE
, cvc5::Kind::BITVECTOR_ULE
},
195 {BITVECTOR_UGT
, cvc5::Kind::BITVECTOR_UGT
},
196 {BITVECTOR_UGE
, cvc5::Kind::BITVECTOR_UGE
},
197 {BITVECTOR_SLT
, cvc5::Kind::BITVECTOR_SLT
},
198 {BITVECTOR_SLE
, cvc5::Kind::BITVECTOR_SLE
},
199 {BITVECTOR_SGT
, cvc5::Kind::BITVECTOR_SGT
},
200 {BITVECTOR_SGE
, cvc5::Kind::BITVECTOR_SGE
},
201 {BITVECTOR_ULTBV
, cvc5::Kind::BITVECTOR_ULTBV
},
202 {BITVECTOR_SLTBV
, cvc5::Kind::BITVECTOR_SLTBV
},
203 {BITVECTOR_ITE
, cvc5::Kind::BITVECTOR_ITE
},
204 {BITVECTOR_REDOR
, cvc5::Kind::BITVECTOR_REDOR
},
205 {BITVECTOR_REDAND
, cvc5::Kind::BITVECTOR_REDAND
},
206 {BITVECTOR_EXTRACT
, cvc5::Kind::BITVECTOR_EXTRACT
},
207 {BITVECTOR_REPEAT
, cvc5::Kind::BITVECTOR_REPEAT
},
208 {BITVECTOR_ZERO_EXTEND
, cvc5::Kind::BITVECTOR_ZERO_EXTEND
},
209 {BITVECTOR_SIGN_EXTEND
, cvc5::Kind::BITVECTOR_SIGN_EXTEND
},
210 {BITVECTOR_ROTATE_LEFT
, cvc5::Kind::BITVECTOR_ROTATE_LEFT
},
211 {BITVECTOR_ROTATE_RIGHT
, cvc5::Kind::BITVECTOR_ROTATE_RIGHT
},
212 {INT_TO_BITVECTOR
, cvc5::Kind::INT_TO_BITVECTOR
},
213 {BITVECTOR_TO_NAT
, cvc5::Kind::BITVECTOR_TO_NAT
},
214 /* FP ------------------------------------------------------------------ */
215 {CONST_FLOATINGPOINT
, cvc5::Kind::CONST_FLOATINGPOINT
},
216 {CONST_ROUNDINGMODE
, cvc5::Kind::CONST_ROUNDINGMODE
},
217 {FLOATINGPOINT_FP
, cvc5::Kind::FLOATINGPOINT_FP
},
218 {FLOATINGPOINT_EQ
, cvc5::Kind::FLOATINGPOINT_EQ
},
219 {FLOATINGPOINT_ABS
, cvc5::Kind::FLOATINGPOINT_ABS
},
220 {FLOATINGPOINT_NEG
, cvc5::Kind::FLOATINGPOINT_NEG
},
221 {FLOATINGPOINT_ADD
, cvc5::Kind::FLOATINGPOINT_ADD
},
222 {FLOATINGPOINT_SUB
, cvc5::Kind::FLOATINGPOINT_SUB
},
223 {FLOATINGPOINT_MULT
, cvc5::Kind::FLOATINGPOINT_MULT
},
224 {FLOATINGPOINT_DIV
, cvc5::Kind::FLOATINGPOINT_DIV
},
225 {FLOATINGPOINT_FMA
, cvc5::Kind::FLOATINGPOINT_FMA
},
226 {FLOATINGPOINT_SQRT
, cvc5::Kind::FLOATINGPOINT_SQRT
},
227 {FLOATINGPOINT_REM
, cvc5::Kind::FLOATINGPOINT_REM
},
228 {FLOATINGPOINT_RTI
, cvc5::Kind::FLOATINGPOINT_RTI
},
229 {FLOATINGPOINT_MIN
, cvc5::Kind::FLOATINGPOINT_MIN
},
230 {FLOATINGPOINT_MAX
, cvc5::Kind::FLOATINGPOINT_MAX
},
231 {FLOATINGPOINT_LEQ
, cvc5::Kind::FLOATINGPOINT_LEQ
},
232 {FLOATINGPOINT_LT
, cvc5::Kind::FLOATINGPOINT_LT
},
233 {FLOATINGPOINT_GEQ
, cvc5::Kind::FLOATINGPOINT_GEQ
},
234 {FLOATINGPOINT_GT
, cvc5::Kind::FLOATINGPOINT_GT
},
235 {FLOATINGPOINT_ISN
, cvc5::Kind::FLOATINGPOINT_ISN
},
236 {FLOATINGPOINT_ISSN
, cvc5::Kind::FLOATINGPOINT_ISSN
},
237 {FLOATINGPOINT_ISZ
, cvc5::Kind::FLOATINGPOINT_ISZ
},
238 {FLOATINGPOINT_ISINF
, cvc5::Kind::FLOATINGPOINT_ISINF
},
239 {FLOATINGPOINT_ISNAN
, cvc5::Kind::FLOATINGPOINT_ISNAN
},
240 {FLOATINGPOINT_ISNEG
, cvc5::Kind::FLOATINGPOINT_ISNEG
},
241 {FLOATINGPOINT_ISPOS
, cvc5::Kind::FLOATINGPOINT_ISPOS
},
242 {FLOATINGPOINT_TO_FP_FLOATINGPOINT
,
243 cvc5::Kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT
},
244 {FLOATINGPOINT_TO_FP_IEEE_BITVECTOR
,
245 cvc5::Kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR
},
246 {FLOATINGPOINT_TO_FP_REAL
, cvc5::Kind::FLOATINGPOINT_TO_FP_REAL
},
247 {FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR
,
248 cvc5::Kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR
},
249 {FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR
,
250 cvc5::Kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR
},
251 {FLOATINGPOINT_TO_FP_GENERIC
, cvc5::Kind::FLOATINGPOINT_TO_FP_GENERIC
},
252 {FLOATINGPOINT_TO_UBV
, cvc5::Kind::FLOATINGPOINT_TO_UBV
},
253 {FLOATINGPOINT_TO_SBV
, cvc5::Kind::FLOATINGPOINT_TO_SBV
},
254 {FLOATINGPOINT_TO_REAL
, cvc5::Kind::FLOATINGPOINT_TO_REAL
},
255 /* Arrays -------------------------------------------------------------- */
256 {SELECT
, cvc5::Kind::SELECT
},
257 {STORE
, cvc5::Kind::STORE
},
258 {CONST_ARRAY
, cvc5::Kind::STORE_ALL
},
259 {EQ_RANGE
, cvc5::Kind::EQ_RANGE
},
260 /* Datatypes ----------------------------------------------------------- */
261 {APPLY_SELECTOR
, cvc5::Kind::APPLY_SELECTOR
},
262 {APPLY_CONSTRUCTOR
, cvc5::Kind::APPLY_CONSTRUCTOR
},
263 {APPLY_TESTER
, cvc5::Kind::APPLY_TESTER
},
264 {APPLY_UPDATER
, cvc5::Kind::APPLY_UPDATER
},
265 {DT_SIZE
, cvc5::Kind::DT_SIZE
},
266 {MATCH
, cvc5::Kind::MATCH
},
267 {MATCH_CASE
, cvc5::Kind::MATCH_CASE
},
268 {MATCH_BIND_CASE
, cvc5::Kind::MATCH_BIND_CASE
},
269 {TUPLE_PROJECT
, cvc5::Kind::TUPLE_PROJECT
},
270 /* Separation Logic ---------------------------------------------------- */
271 {SEP_NIL
, cvc5::Kind::SEP_NIL
},
272 {SEP_EMP
, cvc5::Kind::SEP_EMP
},
273 {SEP_PTO
, cvc5::Kind::SEP_PTO
},
274 {SEP_STAR
, cvc5::Kind::SEP_STAR
},
275 {SEP_WAND
, cvc5::Kind::SEP_WAND
},
276 /* Sets ---------------------------------------------------------------- */
277 {SET_EMPTY
, cvc5::Kind::SET_EMPTY
},
278 {SET_UNION
, cvc5::Kind::SET_UNION
},
279 {SET_INTER
, cvc5::Kind::SET_INTER
},
280 {SET_MINUS
, cvc5::Kind::SET_MINUS
},
281 {SET_SUBSET
, cvc5::Kind::SET_SUBSET
},
282 {SET_MEMBER
, cvc5::Kind::SET_MEMBER
},
283 {SET_SINGLETON
, cvc5::Kind::SET_SINGLETON
},
284 {SET_INSERT
, cvc5::Kind::SET_INSERT
},
285 {SET_CARD
, cvc5::Kind::SET_CARD
},
286 {SET_COMPLEMENT
, cvc5::Kind::SET_COMPLEMENT
},
287 {SET_UNIVERSE
, cvc5::Kind::SET_UNIVERSE
},
288 {SET_COMPREHENSION
, cvc5::Kind::SET_COMPREHENSION
},
289 {SET_CHOOSE
, cvc5::Kind::SET_CHOOSE
},
290 {SET_IS_SINGLETON
, cvc5::Kind::SET_IS_SINGLETON
},
291 {SET_MAP
, cvc5::Kind::SET_MAP
},
292 /* Relations ----------------------------------------------------------- */
293 {RELATION_JOIN
, cvc5::Kind::RELATION_JOIN
},
294 {RELATION_PRODUCT
, cvc5::Kind::RELATION_PRODUCT
},
295 {RELATION_TRANSPOSE
, cvc5::Kind::RELATION_TRANSPOSE
},
296 {RELATION_TCLOSURE
, cvc5::Kind::RELATION_TCLOSURE
},
297 {RELATION_JOIN_IMAGE
, cvc5::Kind::RELATION_JOIN_IMAGE
},
298 {RELATION_IDEN
, cvc5::Kind::RELATION_IDEN
},
299 /* Bags ---------------------------------------------------------------- */
300 {BAG_UNION_MAX
, cvc5::Kind::BAG_UNION_MAX
},
301 {BAG_UNION_DISJOINT
, cvc5::Kind::BAG_UNION_DISJOINT
},
302 {BAG_INTER_MIN
, cvc5::Kind::BAG_INTER_MIN
},
303 {BAG_DIFFERENCE_SUBTRACT
, cvc5::Kind::BAG_DIFFERENCE_SUBTRACT
},
304 {BAG_DIFFERENCE_REMOVE
, cvc5::Kind::BAG_DIFFERENCE_REMOVE
},
305 {BAG_SUBBAG
, cvc5::Kind::BAG_SUBBAG
},
306 {BAG_COUNT
, cvc5::Kind::BAG_COUNT
},
307 {BAG_MEMBER
, cvc5::Kind::BAG_MEMBER
},
308 {BAG_DUPLICATE_REMOVAL
, cvc5::Kind::BAG_DUPLICATE_REMOVAL
},
309 {BAG_MAKE
, cvc5::Kind::BAG_MAKE
},
310 {BAG_EMPTY
, cvc5::Kind::BAG_EMPTY
},
311 {BAG_CARD
, cvc5::Kind::BAG_CARD
},
312 {BAG_CHOOSE
, cvc5::Kind::BAG_CHOOSE
},
313 {BAG_IS_SINGLETON
, cvc5::Kind::BAG_IS_SINGLETON
},
314 {BAG_FROM_SET
, cvc5::Kind::BAG_FROM_SET
},
315 {BAG_TO_SET
, cvc5::Kind::BAG_TO_SET
},
316 {BAG_MAP
, cvc5::Kind::BAG_MAP
},
317 {BAG_FOLD
, cvc5::Kind::BAG_FOLD
},
318 /* Strings ------------------------------------------------------------- */
319 {STRING_CONCAT
, cvc5::Kind::STRING_CONCAT
},
320 {STRING_IN_REGEXP
, cvc5::Kind::STRING_IN_REGEXP
},
321 {STRING_LENGTH
, cvc5::Kind::STRING_LENGTH
},
322 {STRING_SUBSTR
, cvc5::Kind::STRING_SUBSTR
},
323 {STRING_UPDATE
, cvc5::Kind::STRING_UPDATE
},
324 {STRING_CHARAT
, cvc5::Kind::STRING_CHARAT
},
325 {STRING_CONTAINS
, cvc5::Kind::STRING_CONTAINS
},
326 {STRING_INDEXOF
, cvc5::Kind::STRING_INDEXOF
},
327 {STRING_INDEXOF_RE
, cvc5::Kind::STRING_INDEXOF_RE
},
328 {STRING_REPLACE
, cvc5::Kind::STRING_REPLACE
},
329 {STRING_REPLACE_ALL
, cvc5::Kind::STRING_REPLACE_ALL
},
330 {STRING_REPLACE_RE
, cvc5::Kind::STRING_REPLACE_RE
},
331 {STRING_REPLACE_RE_ALL
, cvc5::Kind::STRING_REPLACE_RE_ALL
},
332 {STRING_TOLOWER
, cvc5::Kind::STRING_TOLOWER
},
333 {STRING_TOUPPER
, cvc5::Kind::STRING_TOUPPER
},
334 {STRING_REV
, cvc5::Kind::STRING_REV
},
335 {STRING_FROM_CODE
, cvc5::Kind::STRING_FROM_CODE
},
336 {STRING_TO_CODE
, cvc5::Kind::STRING_TO_CODE
},
337 {STRING_LT
, cvc5::Kind::STRING_LT
},
338 {STRING_LEQ
, cvc5::Kind::STRING_LEQ
},
339 {STRING_PREFIX
, cvc5::Kind::STRING_PREFIX
},
340 {STRING_SUFFIX
, cvc5::Kind::STRING_SUFFIX
},
341 {STRING_IS_DIGIT
, cvc5::Kind::STRING_IS_DIGIT
},
342 {STRING_FROM_INT
, cvc5::Kind::STRING_ITOS
},
343 {STRING_TO_INT
, cvc5::Kind::STRING_STOI
},
344 {CONST_STRING
, cvc5::Kind::CONST_STRING
},
345 {STRING_TO_REGEXP
, cvc5::Kind::STRING_TO_REGEXP
},
346 {REGEXP_CONCAT
, cvc5::Kind::REGEXP_CONCAT
},
347 {REGEXP_UNION
, cvc5::Kind::REGEXP_UNION
},
348 {REGEXP_INTER
, cvc5::Kind::REGEXP_INTER
},
349 {REGEXP_DIFF
, cvc5::Kind::REGEXP_DIFF
},
350 {REGEXP_STAR
, cvc5::Kind::REGEXP_STAR
},
351 {REGEXP_PLUS
, cvc5::Kind::REGEXP_PLUS
},
352 {REGEXP_OPT
, cvc5::Kind::REGEXP_OPT
},
353 {REGEXP_RANGE
, cvc5::Kind::REGEXP_RANGE
},
354 {REGEXP_REPEAT
, cvc5::Kind::REGEXP_REPEAT
},
355 {REGEXP_LOOP
, cvc5::Kind::REGEXP_LOOP
},
356 {REGEXP_NONE
, cvc5::Kind::REGEXP_NONE
},
357 {REGEXP_ALLCHAR
, cvc5::Kind::REGEXP_ALLCHAR
},
358 {REGEXP_COMPLEMENT
, cvc5::Kind::REGEXP_COMPLEMENT
},
359 // maps to the same kind as the string versions
360 {SEQ_CONCAT
, cvc5::Kind::STRING_CONCAT
},
361 {SEQ_LENGTH
, cvc5::Kind::STRING_LENGTH
},
362 {SEQ_EXTRACT
, cvc5::Kind::STRING_SUBSTR
},
363 {SEQ_UPDATE
, cvc5::Kind::STRING_UPDATE
},
364 {SEQ_AT
, cvc5::Kind::STRING_CHARAT
},
365 {SEQ_CONTAINS
, cvc5::Kind::STRING_CONTAINS
},
366 {SEQ_INDEXOF
, cvc5::Kind::STRING_INDEXOF
},
367 {SEQ_REPLACE
, cvc5::Kind::STRING_REPLACE
},
368 {SEQ_REPLACE_ALL
, cvc5::Kind::STRING_REPLACE_ALL
},
369 {SEQ_REV
, cvc5::Kind::STRING_REV
},
370 {SEQ_PREFIX
, cvc5::Kind::STRING_PREFIX
},
371 {SEQ_SUFFIX
, cvc5::Kind::STRING_SUFFIX
},
372 {CONST_SEQUENCE
, cvc5::Kind::CONST_SEQUENCE
},
373 {SEQ_UNIT
, cvc5::Kind::SEQ_UNIT
},
374 {SEQ_NTH
, cvc5::Kind::SEQ_NTH
},
375 /* Quantifiers --------------------------------------------------------- */
376 {FORALL
, cvc5::Kind::FORALL
},
377 {EXISTS
, cvc5::Kind::EXISTS
},
378 {VARIABLE_LIST
, cvc5::Kind::BOUND_VAR_LIST
},
379 {INST_PATTERN
, cvc5::Kind::INST_PATTERN
},
380 {INST_NO_PATTERN
, cvc5::Kind::INST_NO_PATTERN
},
381 {INST_POOL
, cvc5::Kind::INST_POOL
},
382 {INST_ADD_TO_POOL
, cvc5::Kind::INST_ADD_TO_POOL
},
383 {SKOLEM_ADD_TO_POOL
, cvc5::Kind::SKOLEM_ADD_TO_POOL
},
384 {INST_ATTRIBUTE
, cvc5::Kind::INST_ATTRIBUTE
},
385 {INST_PATTERN_LIST
, cvc5::Kind::INST_PATTERN_LIST
},
386 {LAST_KIND
, cvc5::Kind::LAST_KIND
},
389 /* Mapping from internal kind to external (API) kind. */
390 const static std::unordered_map
<cvc5::Kind
, Kind
, cvc5::kind::KindHashFunction
>
392 {cvc5::Kind::UNDEFINED_KIND
, UNDEFINED_KIND
},
393 {cvc5::Kind::NULL_EXPR
, NULL_EXPR
},
394 /* Builtin --------------------------------------------------------- */
395 {cvc5::Kind::UNINTERPRETED_CONSTANT
, UNINTERPRETED_CONSTANT
},
396 {cvc5::Kind::ABSTRACT_VALUE
, ABSTRACT_VALUE
},
397 {cvc5::Kind::EQUAL
, EQUAL
},
398 {cvc5::Kind::DISTINCT
, DISTINCT
},
399 {cvc5::Kind::VARIABLE
, CONSTANT
},
400 {cvc5::Kind::BOUND_VARIABLE
, VARIABLE
},
401 {cvc5::Kind::SEXPR
, SEXPR
},
402 {cvc5::Kind::LAMBDA
, LAMBDA
},
403 {cvc5::Kind::WITNESS
, WITNESS
},
404 /* Boolean --------------------------------------------------------- */
405 {cvc5::Kind::CONST_BOOLEAN
, CONST_BOOLEAN
},
406 {cvc5::Kind::NOT
, NOT
},
407 {cvc5::Kind::AND
, AND
},
408 {cvc5::Kind::IMPLIES
, IMPLIES
},
409 {cvc5::Kind::OR
, OR
},
410 {cvc5::Kind::XOR
, XOR
},
411 {cvc5::Kind::ITE
, ITE
},
412 /* UF -------------------------------------------------------------- */
413 {cvc5::Kind::APPLY_UF
, APPLY_UF
},
414 {cvc5::Kind::CARDINALITY_CONSTRAINT
, CARDINALITY_CONSTRAINT
},
415 {cvc5::Kind::HO_APPLY
, HO_APPLY
},
416 /* Arithmetic ------------------------------------------------------ */
417 {cvc5::Kind::PLUS
, PLUS
},
418 {cvc5::Kind::MULT
, MULT
},
419 {cvc5::Kind::IAND
, IAND
},
420 {cvc5::Kind::POW2
, POW2
},
421 {cvc5::Kind::MINUS
, MINUS
},
422 {cvc5::Kind::UMINUS
, UMINUS
},
423 {cvc5::Kind::DIVISION
, DIVISION
},
424 {cvc5::Kind::DIVISION_TOTAL
, INTERNAL_KIND
},
425 {cvc5::Kind::INTS_DIVISION
, INTS_DIVISION
},
426 {cvc5::Kind::INTS_DIVISION_TOTAL
, INTERNAL_KIND
},
427 {cvc5::Kind::INTS_MODULUS
, INTS_MODULUS
},
428 {cvc5::Kind::INTS_MODULUS_TOTAL
, INTERNAL_KIND
},
429 {cvc5::Kind::ABS
, ABS
},
430 {cvc5::Kind::DIVISIBLE
, DIVISIBLE
},
431 {cvc5::Kind::POW
, POW
},
432 {cvc5::Kind::EXPONENTIAL
, EXPONENTIAL
},
433 {cvc5::Kind::SINE
, SINE
},
434 {cvc5::Kind::COSINE
, COSINE
},
435 {cvc5::Kind::TANGENT
, TANGENT
},
436 {cvc5::Kind::COSECANT
, COSECANT
},
437 {cvc5::Kind::SECANT
, SECANT
},
438 {cvc5::Kind::COTANGENT
, COTANGENT
},
439 {cvc5::Kind::ARCSINE
, ARCSINE
},
440 {cvc5::Kind::ARCCOSINE
, ARCCOSINE
},
441 {cvc5::Kind::ARCTANGENT
, ARCTANGENT
},
442 {cvc5::Kind::ARCCOSECANT
, ARCCOSECANT
},
443 {cvc5::Kind::ARCSECANT
, ARCSECANT
},
444 {cvc5::Kind::ARCCOTANGENT
, ARCCOTANGENT
},
445 {cvc5::Kind::SQRT
, SQRT
},
446 {cvc5::Kind::DIVISIBLE_OP
, DIVISIBLE
},
447 {cvc5::Kind::CONST_RATIONAL
, CONST_RATIONAL
},
448 {cvc5::Kind::LT
, LT
},
449 {cvc5::Kind::LEQ
, LEQ
},
450 {cvc5::Kind::GT
, GT
},
451 {cvc5::Kind::GEQ
, GEQ
},
452 {cvc5::Kind::IS_INTEGER
, IS_INTEGER
},
453 {cvc5::Kind::TO_INTEGER
, TO_INTEGER
},
454 {cvc5::Kind::TO_REAL
, TO_REAL
},
455 {cvc5::Kind::PI
, PI
},
456 {cvc5::Kind::IAND_OP
, IAND
},
457 /* BV -------------------------------------------------------------- */
458 {cvc5::Kind::CONST_BITVECTOR
, CONST_BITVECTOR
},
459 {cvc5::Kind::BITVECTOR_CONCAT
, BITVECTOR_CONCAT
},
460 {cvc5::Kind::BITVECTOR_AND
, BITVECTOR_AND
},
461 {cvc5::Kind::BITVECTOR_OR
, BITVECTOR_OR
},
462 {cvc5::Kind::BITVECTOR_XOR
, BITVECTOR_XOR
},
463 {cvc5::Kind::BITVECTOR_NOT
, BITVECTOR_NOT
},
464 {cvc5::Kind::BITVECTOR_NAND
, BITVECTOR_NAND
},
465 {cvc5::Kind::BITVECTOR_NOR
, BITVECTOR_NOR
},
466 {cvc5::Kind::BITVECTOR_XNOR
, BITVECTOR_XNOR
},
467 {cvc5::Kind::BITVECTOR_COMP
, BITVECTOR_COMP
},
468 {cvc5::Kind::BITVECTOR_MULT
, BITVECTOR_MULT
},
469 {cvc5::Kind::BITVECTOR_ADD
, BITVECTOR_ADD
},
470 {cvc5::Kind::BITVECTOR_SUB
, BITVECTOR_SUB
},
471 {cvc5::Kind::BITVECTOR_NEG
, BITVECTOR_NEG
},
472 {cvc5::Kind::BITVECTOR_UDIV
, BITVECTOR_UDIV
},
473 {cvc5::Kind::BITVECTOR_UREM
, BITVECTOR_UREM
},
474 {cvc5::Kind::BITVECTOR_SDIV
, BITVECTOR_SDIV
},
475 {cvc5::Kind::BITVECTOR_SREM
, BITVECTOR_SREM
},
476 {cvc5::Kind::BITVECTOR_SMOD
, BITVECTOR_SMOD
},
477 {cvc5::Kind::BITVECTOR_SHL
, BITVECTOR_SHL
},
478 {cvc5::Kind::BITVECTOR_LSHR
, BITVECTOR_LSHR
},
479 {cvc5::Kind::BITVECTOR_ASHR
, BITVECTOR_ASHR
},
480 {cvc5::Kind::BITVECTOR_ULT
, BITVECTOR_ULT
},
481 {cvc5::Kind::BITVECTOR_ULE
, BITVECTOR_ULE
},
482 {cvc5::Kind::BITVECTOR_UGT
, BITVECTOR_UGT
},
483 {cvc5::Kind::BITVECTOR_UGE
, BITVECTOR_UGE
},
484 {cvc5::Kind::BITVECTOR_SLT
, BITVECTOR_SLT
},
485 {cvc5::Kind::BITVECTOR_SLE
, BITVECTOR_SLE
},
486 {cvc5::Kind::BITVECTOR_SGT
, BITVECTOR_SGT
},
487 {cvc5::Kind::BITVECTOR_SGE
, BITVECTOR_SGE
},
488 {cvc5::Kind::BITVECTOR_ULTBV
, BITVECTOR_ULTBV
},
489 {cvc5::Kind::BITVECTOR_SLTBV
, BITVECTOR_SLTBV
},
490 {cvc5::Kind::BITVECTOR_ITE
, BITVECTOR_ITE
},
491 {cvc5::Kind::BITVECTOR_REDOR
, BITVECTOR_REDOR
},
492 {cvc5::Kind::BITVECTOR_REDAND
, BITVECTOR_REDAND
},
493 {cvc5::Kind::BITVECTOR_EXTRACT_OP
, BITVECTOR_EXTRACT
},
494 {cvc5::Kind::BITVECTOR_REPEAT_OP
, BITVECTOR_REPEAT
},
495 {cvc5::Kind::BITVECTOR_ZERO_EXTEND_OP
, BITVECTOR_ZERO_EXTEND
},
496 {cvc5::Kind::BITVECTOR_SIGN_EXTEND_OP
, BITVECTOR_SIGN_EXTEND
},
497 {cvc5::Kind::BITVECTOR_ROTATE_LEFT_OP
, BITVECTOR_ROTATE_LEFT
},
498 {cvc5::Kind::BITVECTOR_ROTATE_RIGHT_OP
, BITVECTOR_ROTATE_RIGHT
},
499 {cvc5::Kind::BITVECTOR_EXTRACT
, BITVECTOR_EXTRACT
},
500 {cvc5::Kind::BITVECTOR_REPEAT
, BITVECTOR_REPEAT
},
501 {cvc5::Kind::BITVECTOR_ZERO_EXTEND
, BITVECTOR_ZERO_EXTEND
},
502 {cvc5::Kind::BITVECTOR_SIGN_EXTEND
, BITVECTOR_SIGN_EXTEND
},
503 {cvc5::Kind::BITVECTOR_ROTATE_LEFT
, BITVECTOR_ROTATE_LEFT
},
504 {cvc5::Kind::BITVECTOR_ROTATE_RIGHT
, BITVECTOR_ROTATE_RIGHT
},
505 {cvc5::Kind::INT_TO_BITVECTOR_OP
, INT_TO_BITVECTOR
},
506 {cvc5::Kind::INT_TO_BITVECTOR
, INT_TO_BITVECTOR
},
507 {cvc5::Kind::BITVECTOR_TO_NAT
, BITVECTOR_TO_NAT
},
508 /* FP -------------------------------------------------------------- */
509 {cvc5::Kind::CONST_FLOATINGPOINT
, CONST_FLOATINGPOINT
},
510 {cvc5::Kind::CONST_ROUNDINGMODE
, CONST_ROUNDINGMODE
},
511 {cvc5::Kind::FLOATINGPOINT_FP
, FLOATINGPOINT_FP
},
512 {cvc5::Kind::FLOATINGPOINT_EQ
, FLOATINGPOINT_EQ
},
513 {cvc5::Kind::FLOATINGPOINT_ABS
, FLOATINGPOINT_ABS
},
514 {cvc5::Kind::FLOATINGPOINT_NEG
, FLOATINGPOINT_NEG
},
515 {cvc5::Kind::FLOATINGPOINT_ADD
, FLOATINGPOINT_ADD
},
516 {cvc5::Kind::FLOATINGPOINT_SUB
, FLOATINGPOINT_SUB
},
517 {cvc5::Kind::FLOATINGPOINT_MULT
, FLOATINGPOINT_MULT
},
518 {cvc5::Kind::FLOATINGPOINT_DIV
, FLOATINGPOINT_DIV
},
519 {cvc5::Kind::FLOATINGPOINT_FMA
, FLOATINGPOINT_FMA
},
520 {cvc5::Kind::FLOATINGPOINT_SQRT
, FLOATINGPOINT_SQRT
},
521 {cvc5::Kind::FLOATINGPOINT_REM
, FLOATINGPOINT_REM
},
522 {cvc5::Kind::FLOATINGPOINT_RTI
, FLOATINGPOINT_RTI
},
523 {cvc5::Kind::FLOATINGPOINT_MIN
, FLOATINGPOINT_MIN
},
524 {cvc5::Kind::FLOATINGPOINT_MAX
, FLOATINGPOINT_MAX
},
525 {cvc5::Kind::FLOATINGPOINT_LEQ
, FLOATINGPOINT_LEQ
},
526 {cvc5::Kind::FLOATINGPOINT_LT
, FLOATINGPOINT_LT
},
527 {cvc5::Kind::FLOATINGPOINT_GEQ
, FLOATINGPOINT_GEQ
},
528 {cvc5::Kind::FLOATINGPOINT_GT
, FLOATINGPOINT_GT
},
529 {cvc5::Kind::FLOATINGPOINT_ISN
, FLOATINGPOINT_ISN
},
530 {cvc5::Kind::FLOATINGPOINT_ISSN
, FLOATINGPOINT_ISSN
},
531 {cvc5::Kind::FLOATINGPOINT_ISZ
, FLOATINGPOINT_ISZ
},
532 {cvc5::Kind::FLOATINGPOINT_ISINF
, FLOATINGPOINT_ISINF
},
533 {cvc5::Kind::FLOATINGPOINT_ISNAN
, FLOATINGPOINT_ISNAN
},
534 {cvc5::Kind::FLOATINGPOINT_ISNEG
, FLOATINGPOINT_ISNEG
},
535 {cvc5::Kind::FLOATINGPOINT_ISPOS
, FLOATINGPOINT_ISPOS
},
536 {cvc5::Kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP
,
537 FLOATINGPOINT_TO_FP_IEEE_BITVECTOR
},
538 {cvc5::Kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR
,
539 FLOATINGPOINT_TO_FP_IEEE_BITVECTOR
},
540 {cvc5::Kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP
,
541 FLOATINGPOINT_TO_FP_FLOATINGPOINT
},
542 {cvc5::Kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT
,
543 FLOATINGPOINT_TO_FP_FLOATINGPOINT
},
544 {cvc5::Kind::FLOATINGPOINT_TO_FP_REAL_OP
, FLOATINGPOINT_TO_FP_REAL
},
545 {cvc5::Kind::FLOATINGPOINT_TO_FP_REAL
, FLOATINGPOINT_TO_FP_REAL
},
546 {cvc5::Kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP
,
547 FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR
},
548 {cvc5::Kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR
,
549 FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR
},
550 {cvc5::Kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP
,
551 FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR
},
552 {cvc5::Kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR
,
553 FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR
},
554 {cvc5::Kind::FLOATINGPOINT_TO_FP_GENERIC_OP
,
555 FLOATINGPOINT_TO_FP_GENERIC
},
556 {cvc5::Kind::FLOATINGPOINT_TO_FP_GENERIC
, FLOATINGPOINT_TO_FP_GENERIC
},
557 {cvc5::Kind::FLOATINGPOINT_TO_UBV_OP
, FLOATINGPOINT_TO_UBV
},
558 {cvc5::Kind::FLOATINGPOINT_TO_UBV
, FLOATINGPOINT_TO_UBV
},
559 {cvc5::Kind::FLOATINGPOINT_TO_UBV_TOTAL_OP
, INTERNAL_KIND
},
560 {cvc5::Kind::FLOATINGPOINT_TO_UBV_TOTAL
, INTERNAL_KIND
},
561 {cvc5::Kind::FLOATINGPOINT_TO_SBV_OP
, FLOATINGPOINT_TO_SBV
},
562 {cvc5::Kind::FLOATINGPOINT_TO_SBV
, FLOATINGPOINT_TO_SBV
},
563 {cvc5::Kind::FLOATINGPOINT_TO_SBV_TOTAL_OP
, INTERNAL_KIND
},
564 {cvc5::Kind::FLOATINGPOINT_TO_SBV_TOTAL
, INTERNAL_KIND
},
565 {cvc5::Kind::FLOATINGPOINT_TO_REAL
, FLOATINGPOINT_TO_REAL
},
566 {cvc5::Kind::FLOATINGPOINT_TO_REAL_TOTAL
, INTERNAL_KIND
},
567 /* Arrays ---------------------------------------------------------- */
568 {cvc5::Kind::SELECT
, SELECT
},
569 {cvc5::Kind::STORE
, STORE
},
570 {cvc5::Kind::STORE_ALL
, CONST_ARRAY
},
571 /* Datatypes ------------------------------------------------------- */
572 {cvc5::Kind::APPLY_SELECTOR
, APPLY_SELECTOR
},
573 {cvc5::Kind::APPLY_CONSTRUCTOR
, APPLY_CONSTRUCTOR
},
574 {cvc5::Kind::APPLY_SELECTOR_TOTAL
, INTERNAL_KIND
},
575 {cvc5::Kind::APPLY_TESTER
, APPLY_TESTER
},
576 {cvc5::Kind::APPLY_UPDATER
, APPLY_UPDATER
},
577 {cvc5::Kind::DT_SIZE
, DT_SIZE
},
578 {cvc5::Kind::MATCH
, MATCH
},
579 {cvc5::Kind::MATCH_CASE
, MATCH_CASE
},
580 {cvc5::Kind::MATCH_BIND_CASE
, MATCH_BIND_CASE
},
581 {cvc5::Kind::TUPLE_PROJECT
, TUPLE_PROJECT
},
582 {cvc5::Kind::TUPLE_PROJECT_OP
, TUPLE_PROJECT
},
583 /* Separation Logic ------------------------------------------------ */
584 {cvc5::Kind::SEP_NIL
, SEP_NIL
},
585 {cvc5::Kind::SEP_EMP
, SEP_EMP
},
586 {cvc5::Kind::SEP_PTO
, SEP_PTO
},
587 {cvc5::Kind::SEP_STAR
, SEP_STAR
},
588 {cvc5::Kind::SEP_WAND
, SEP_WAND
},
589 /* Sets ------------------------------------------------------------ */
590 {cvc5::Kind::SET_EMPTY
, SET_EMPTY
},
591 {cvc5::Kind::SET_UNION
, SET_UNION
},
592 {cvc5::Kind::SET_INTER
, SET_INTER
},
593 {cvc5::Kind::SET_MINUS
, SET_MINUS
},
594 {cvc5::Kind::SET_SUBSET
, SET_SUBSET
},
595 {cvc5::Kind::SET_MEMBER
, SET_MEMBER
},
596 {cvc5::Kind::SET_SINGLETON
, SET_SINGLETON
},
597 {cvc5::Kind::SET_INSERT
, SET_INSERT
},
598 {cvc5::Kind::SET_CARD
, SET_CARD
},
599 {cvc5::Kind::SET_COMPLEMENT
, SET_COMPLEMENT
},
600 {cvc5::Kind::SET_UNIVERSE
, SET_UNIVERSE
},
601 {cvc5::Kind::SET_COMPREHENSION
, SET_COMPREHENSION
},
602 {cvc5::Kind::SET_CHOOSE
, SET_CHOOSE
},
603 {cvc5::Kind::SET_IS_SINGLETON
, SET_IS_SINGLETON
},
604 {cvc5::Kind::SET_MAP
, SET_MAP
},
605 /* Relations ------------------------------------------------------- */
606 {cvc5::Kind::RELATION_JOIN
, RELATION_JOIN
},
607 {cvc5::Kind::RELATION_PRODUCT
, RELATION_PRODUCT
},
608 {cvc5::Kind::RELATION_TRANSPOSE
, RELATION_TRANSPOSE
},
609 {cvc5::Kind::RELATION_TCLOSURE
, RELATION_TCLOSURE
},
610 {cvc5::Kind::RELATION_JOIN_IMAGE
, RELATION_JOIN_IMAGE
},
611 {cvc5::Kind::RELATION_IDEN
, RELATION_IDEN
},
612 /* Bags ------------------------------------------------------------ */
613 {cvc5::Kind::BAG_UNION_MAX
, BAG_UNION_MAX
},
614 {cvc5::Kind::BAG_UNION_DISJOINT
, BAG_UNION_DISJOINT
},
615 {cvc5::Kind::BAG_INTER_MIN
, BAG_INTER_MIN
},
616 {cvc5::Kind::BAG_DIFFERENCE_SUBTRACT
, BAG_DIFFERENCE_SUBTRACT
},
617 {cvc5::Kind::BAG_DIFFERENCE_REMOVE
, BAG_DIFFERENCE_REMOVE
},
618 {cvc5::Kind::BAG_SUBBAG
, BAG_SUBBAG
},
619 {cvc5::Kind::BAG_COUNT
, BAG_COUNT
},
620 {cvc5::Kind::BAG_MEMBER
, BAG_MEMBER
},
621 {cvc5::Kind::BAG_DUPLICATE_REMOVAL
, BAG_DUPLICATE_REMOVAL
},
622 {cvc5::Kind::BAG_MAKE
, BAG_MAKE
},
623 {cvc5::Kind::BAG_EMPTY
, BAG_EMPTY
},
624 {cvc5::Kind::BAG_CARD
, BAG_CARD
},
625 {cvc5::Kind::BAG_CHOOSE
, BAG_CHOOSE
},
626 {cvc5::Kind::BAG_IS_SINGLETON
, BAG_IS_SINGLETON
},
627 {cvc5::Kind::BAG_FROM_SET
, BAG_FROM_SET
},
628 {cvc5::Kind::BAG_TO_SET
, BAG_TO_SET
},
629 {cvc5::Kind::BAG_MAP
, BAG_MAP
},
630 {cvc5::Kind::BAG_FOLD
, BAG_FOLD
},
631 /* Strings --------------------------------------------------------- */
632 {cvc5::Kind::STRING_CONCAT
, STRING_CONCAT
},
633 {cvc5::Kind::STRING_IN_REGEXP
, STRING_IN_REGEXP
},
634 {cvc5::Kind::STRING_LENGTH
, STRING_LENGTH
},
635 {cvc5::Kind::STRING_SUBSTR
, STRING_SUBSTR
},
636 {cvc5::Kind::STRING_UPDATE
, STRING_UPDATE
},
637 {cvc5::Kind::STRING_CHARAT
, STRING_CHARAT
},
638 {cvc5::Kind::STRING_CONTAINS
, STRING_CONTAINS
},
639 {cvc5::Kind::STRING_INDEXOF
, STRING_INDEXOF
},
640 {cvc5::Kind::STRING_INDEXOF_RE
, STRING_INDEXOF_RE
},
641 {cvc5::Kind::STRING_REPLACE
, STRING_REPLACE
},
642 {cvc5::Kind::STRING_REPLACE_ALL
, STRING_REPLACE_ALL
},
643 {cvc5::Kind::STRING_REPLACE_RE
, STRING_REPLACE_RE
},
644 {cvc5::Kind::STRING_REPLACE_RE_ALL
, STRING_REPLACE_RE_ALL
},
645 {cvc5::Kind::STRING_TOLOWER
, STRING_TOLOWER
},
646 {cvc5::Kind::STRING_TOUPPER
, STRING_TOUPPER
},
647 {cvc5::Kind::STRING_REV
, STRING_REV
},
648 {cvc5::Kind::STRING_FROM_CODE
, STRING_FROM_CODE
},
649 {cvc5::Kind::STRING_TO_CODE
, STRING_TO_CODE
},
650 {cvc5::Kind::STRING_LT
, STRING_LT
},
651 {cvc5::Kind::STRING_LEQ
, STRING_LEQ
},
652 {cvc5::Kind::STRING_PREFIX
, STRING_PREFIX
},
653 {cvc5::Kind::STRING_SUFFIX
, STRING_SUFFIX
},
654 {cvc5::Kind::STRING_IS_DIGIT
, STRING_IS_DIGIT
},
655 {cvc5::Kind::STRING_ITOS
, STRING_FROM_INT
},
656 {cvc5::Kind::STRING_STOI
, STRING_TO_INT
},
657 {cvc5::Kind::CONST_STRING
, CONST_STRING
},
658 {cvc5::Kind::STRING_TO_REGEXP
, STRING_TO_REGEXP
},
659 {cvc5::Kind::REGEXP_CONCAT
, REGEXP_CONCAT
},
660 {cvc5::Kind::REGEXP_UNION
, REGEXP_UNION
},
661 {cvc5::Kind::REGEXP_INTER
, REGEXP_INTER
},
662 {cvc5::Kind::REGEXP_DIFF
, REGEXP_DIFF
},
663 {cvc5::Kind::REGEXP_STAR
, REGEXP_STAR
},
664 {cvc5::Kind::REGEXP_PLUS
, REGEXP_PLUS
},
665 {cvc5::Kind::REGEXP_OPT
, REGEXP_OPT
},
666 {cvc5::Kind::REGEXP_RANGE
, REGEXP_RANGE
},
667 {cvc5::Kind::REGEXP_REPEAT
, REGEXP_REPEAT
},
668 {cvc5::Kind::REGEXP_REPEAT_OP
, REGEXP_REPEAT
},
669 {cvc5::Kind::REGEXP_LOOP
, REGEXP_LOOP
},
670 {cvc5::Kind::REGEXP_LOOP_OP
, REGEXP_LOOP
},
671 {cvc5::Kind::REGEXP_NONE
, REGEXP_NONE
},
672 {cvc5::Kind::REGEXP_ALLCHAR
, REGEXP_ALLCHAR
},
673 {cvc5::Kind::REGEXP_COMPLEMENT
, REGEXP_COMPLEMENT
},
674 {cvc5::Kind::CONST_SEQUENCE
, CONST_SEQUENCE
},
675 {cvc5::Kind::SEQ_UNIT
, SEQ_UNIT
},
676 {cvc5::Kind::SEQ_NTH
, SEQ_NTH
},
677 /* Quantifiers ----------------------------------------------------- */
678 {cvc5::Kind::FORALL
, FORALL
},
679 {cvc5::Kind::EXISTS
, EXISTS
},
680 {cvc5::Kind::BOUND_VAR_LIST
, VARIABLE_LIST
},
681 {cvc5::Kind::INST_PATTERN
, INST_PATTERN
},
682 {cvc5::Kind::INST_NO_PATTERN
, INST_NO_PATTERN
},
683 {cvc5::Kind::INST_POOL
, INST_POOL
},
684 {cvc5::Kind::INST_ADD_TO_POOL
, INST_ADD_TO_POOL
},
685 {cvc5::Kind::SKOLEM_ADD_TO_POOL
, SKOLEM_ADD_TO_POOL
},
686 {cvc5::Kind::INST_ATTRIBUTE
, INST_ATTRIBUTE
},
687 {cvc5::Kind::INST_PATTERN_LIST
, INST_PATTERN_LIST
},
688 /* ----------------------------------------------------------------- */
689 {cvc5::Kind::LAST_KIND
, LAST_KIND
},
692 /* Set of kinds for indexed operators */
693 const static std::unordered_set
<Kind
> s_indexed_kinds(
697 BITVECTOR_ZERO_EXTEND
,
698 BITVECTOR_SIGN_EXTEND
,
699 BITVECTOR_ROTATE_LEFT
,
700 BITVECTOR_ROTATE_RIGHT
,
702 FLOATINGPOINT_TO_UBV
,
703 FLOATINGPOINT_TO_SBV
,
705 FLOATINGPOINT_TO_FP_IEEE_BITVECTOR
,
706 FLOATINGPOINT_TO_FP_FLOATINGPOINT
,
707 FLOATINGPOINT_TO_FP_REAL
,
708 FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR
,
709 FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR
,
710 FLOATINGPOINT_TO_FP_GENERIC
});
714 /** Convert a cvc5::Kind (internal) to a cvc5::api::Kind (external). */
715 cvc5::api::Kind
intToExtKind(cvc5::Kind k
)
717 auto it
= api::s_kinds_internal
.find(k
);
718 if (it
== api::s_kinds_internal
.end())
720 return api::INTERNAL_KIND
;
725 /** Convert a cvc5::api::Kind (external) to a cvc5::Kind (internal). */
726 cvc5::Kind
extToIntKind(cvc5::api::Kind k
)
728 auto it
= api::s_kinds
.find(k
);
729 if (it
== api::s_kinds
.end())
731 return cvc5::Kind::UNDEFINED_KIND
;
736 /** Return true if given kind is a defined external kind. */
737 bool isDefinedKind(Kind k
) { return k
> UNDEFINED_KIND
&& k
< LAST_KIND
; }
740 * Return true if the internal kind is one where the API term structure
741 * differs from internal structure. This happens for APPLY_* kinds.
742 * The API takes a "higher-order" perspective and treats functions as well
743 * as datatype constructors/selectors/testers as terms
744 * but interally they are not
746 bool isApplyKind(cvc5::Kind k
)
748 return (k
== cvc5::Kind::APPLY_UF
|| k
== cvc5::Kind::APPLY_CONSTRUCTOR
749 || k
== cvc5::Kind::APPLY_SELECTOR
|| k
== cvc5::Kind::APPLY_TESTER
750 || k
== cvc5::Kind::APPLY_UPDATER
);
753 #ifdef CVC5_ASSERTIONS
754 /** Return true if given kind is a defined internal kind. */
755 bool isDefinedIntKind(cvc5::Kind k
)
757 return k
!= cvc5::Kind::UNDEFINED_KIND
&& k
!= cvc5::Kind::LAST_KIND
;
761 /** Return the minimum arity of given kind. */
762 uint32_t minArity(Kind k
)
764 Assert(isDefinedKind(k
));
765 Assert(isDefinedIntKind(extToIntKind(k
)));
766 uint32_t min
= cvc5::kind::metakind::getMinArityForKind(extToIntKind(k
));
768 // At the API level, we treat functions/constructors/selectors/testers as
769 // normal terms instead of making them part of the operator
770 if (isApplyKind(extToIntKind(k
)))
777 /** Return the maximum arity of given kind. */
778 uint32_t maxArity(Kind k
)
780 Assert(isDefinedKind(k
));
781 Assert(isDefinedIntKind(extToIntKind(k
)));
782 uint32_t max
= cvc5::kind::metakind::getMaxArityForKind(extToIntKind(k
));
784 // At the API level, we treat functions/constructors/selectors/testers as
785 // normal terms instead of making them part of the operator
786 if (isApplyKind(extToIntKind(k
))
787 && max
!= std::numeric_limits
<uint32_t>::max()) // be careful not to
797 std::string
kindToString(Kind k
)
799 return k
== INTERNAL_KIND
? "INTERNAL_KIND"
800 : cvc5::kind::kindToString(extToIntKind(k
));
803 const char* toString(Kind k
)
805 return k
== INTERNAL_KIND
? "INTERNAL_KIND"
806 : cvc5::kind::toString(extToIntKind(k
));
809 std::ostream
& operator<<(std::ostream
& out
, Kind k
)
813 case INTERNAL_KIND
: out
<< "INTERNAL_KIND"; break;
814 default: out
<< extToIntKind(k
);
819 /* -------------------------------------------------------------------------- */
820 /* API guard helpers */
821 /* -------------------------------------------------------------------------- */
825 class CVC5ApiExceptionStream
828 CVC5ApiExceptionStream() {}
829 /* Note: This needs to be explicitly set to 'noexcept(false)' since it is
830 * a destructor that throws an exception and in C++11 all destructors
831 * default to noexcept(true) (else this triggers a call to std::terminate). */
832 ~CVC5ApiExceptionStream() noexcept(false)
834 if (std::uncaught_exceptions() == 0)
836 throw CVC5ApiException(d_stream
.str());
840 std::ostream
& ostream() { return d_stream
; }
843 std::stringstream d_stream
;
846 class CVC5ApiRecoverableExceptionStream
849 CVC5ApiRecoverableExceptionStream() {}
850 /* Note: This needs to be explicitly set to 'noexcept(false)' since it is
851 * a destructor that throws an exception and in C++11 all destructors
852 * default to noexcept(true) (else this triggers a call to std::terminate). */
853 ~CVC5ApiRecoverableExceptionStream() noexcept(false)
855 if (std::uncaught_exceptions() == 0)
857 throw CVC5ApiRecoverableException(d_stream
.str());
861 std::ostream
& ostream() { return d_stream
; }
864 std::stringstream d_stream
;
867 class CVC5ApiUnsupportedExceptionStream
870 CVC5ApiUnsupportedExceptionStream() {}
871 /* Note: This needs to be explicitly set to 'noexcept(false)' since it is
872 * a destructor that throws an exception and in C++11 all destructors
873 * default to noexcept(true) (else this triggers a call to std::terminate). */
874 ~CVC5ApiUnsupportedExceptionStream() noexcept(false)
876 if (std::uncaught_exceptions() == 0)
878 throw CVC5ApiUnsupportedException(d_stream
.str());
882 std::ostream
& ostream() { return d_stream
; }
885 std::stringstream d_stream
;
888 #define CVC5_API_TRY_CATCH_BEGIN \
891 #define CVC5_API_TRY_CATCH_END \
893 catch (const OptionException& e) \
895 throw CVC5ApiOptionException(e.getMessage()); \
897 catch (const cvc5::RecoverableModalException& e) \
899 throw CVC5ApiRecoverableException(e.getMessage()); \
901 catch (const cvc5::Exception& e) { throw CVC5ApiException(e.getMessage()); } \
902 catch (const std::invalid_argument& e) { throw CVC5ApiException(e.what()); }
906 /* -------------------------------------------------------------------------- */
908 /* -------------------------------------------------------------------------- */
910 Result::Result(const cvc5::Result
& r
) : d_result(new cvc5::Result(r
)) {}
912 Result::Result() : d_result(new cvc5::Result()) {}
914 bool Result::isNull() const
916 return d_result
->getType() == cvc5::Result::TYPE_NONE
;
919 bool Result::isSat(void) const
921 return d_result
->getType() == cvc5::Result::TYPE_SAT
922 && d_result
->isSat() == cvc5::Result::SAT
;
925 bool Result::isUnsat(void) const
927 return d_result
->getType() == cvc5::Result::TYPE_SAT
928 && d_result
->isSat() == cvc5::Result::UNSAT
;
931 bool Result::isSatUnknown(void) const
933 return d_result
->getType() == cvc5::Result::TYPE_SAT
934 && d_result
->isSat() == cvc5::Result::SAT_UNKNOWN
;
937 bool Result::isEntailed(void) const
939 return d_result
->getType() == cvc5::Result::TYPE_ENTAILMENT
940 && d_result
->isEntailed() == cvc5::Result::ENTAILED
;
943 bool Result::isNotEntailed(void) const
945 return d_result
->getType() == cvc5::Result::TYPE_ENTAILMENT
946 && d_result
->isEntailed() == cvc5::Result::NOT_ENTAILED
;
949 bool Result::isEntailmentUnknown(void) const
951 return d_result
->getType() == cvc5::Result::TYPE_ENTAILMENT
952 && d_result
->isEntailed() == cvc5::Result::ENTAILMENT_UNKNOWN
;
955 bool Result::operator==(const Result
& r
) const
957 return *d_result
== *r
.d_result
;
960 bool Result::operator!=(const Result
& r
) const
962 return *d_result
!= *r
.d_result
;
965 Result::UnknownExplanation
Result::getUnknownExplanation(void) const
967 cvc5::Result::UnknownExplanation expl
= d_result
->whyUnknown();
970 case cvc5::Result::REQUIRES_FULL_CHECK
: return REQUIRES_FULL_CHECK
;
971 case cvc5::Result::INCOMPLETE
: return INCOMPLETE
;
972 case cvc5::Result::TIMEOUT
: return TIMEOUT
;
973 case cvc5::Result::RESOURCEOUT
: return RESOURCEOUT
;
974 case cvc5::Result::MEMOUT
: return MEMOUT
;
975 case cvc5::Result::INTERRUPTED
: return INTERRUPTED
;
976 case cvc5::Result::NO_STATUS
: return NO_STATUS
;
977 case cvc5::Result::UNSUPPORTED
: return UNSUPPORTED
;
978 case cvc5::Result::OTHER
: return OTHER
;
979 default: return UNKNOWN_REASON
;
981 return UNKNOWN_REASON
;
984 std::string
Result::toString(void) const { return d_result
->toString(); }
986 std::ostream
& operator<<(std::ostream
& out
, const Result
& r
)
992 std::ostream
& operator<<(std::ostream
& out
, enum Result::UnknownExplanation e
)
996 case Result::REQUIRES_FULL_CHECK
: out
<< "REQUIRES_FULL_CHECK"; break;
997 case Result::INCOMPLETE
: out
<< "INCOMPLETE"; break;
998 case Result::TIMEOUT
: out
<< "TIMEOUT"; break;
999 case Result::RESOURCEOUT
: out
<< "RESOURCEOUT"; break;
1000 case Result::MEMOUT
: out
<< "MEMOUT"; break;
1001 case Result::INTERRUPTED
: out
<< "INTERRUPTED"; break;
1002 case Result::NO_STATUS
: out
<< "NO_STATUS"; break;
1003 case Result::UNSUPPORTED
: out
<< "UNSUPPORTED"; break;
1004 case Result::OTHER
: out
<< "OTHER"; break;
1005 case Result::UNKNOWN_REASON
: out
<< "UNKNOWN_REASON"; break;
1006 default: Unhandled() << e
;
1011 /* -------------------------------------------------------------------------- */
1013 /* -------------------------------------------------------------------------- */
1015 Sort::Sort(const Solver
* slv
, const cvc5::TypeNode
& t
)
1016 : d_solver(slv
), d_type(new cvc5::TypeNode(t
))
1020 Sort::Sort() : d_solver(nullptr), d_type(new cvc5::TypeNode()) {}
1024 if (d_solver
!= nullptr)
1030 std::set
<TypeNode
> Sort::sortSetToTypeNodes(const std::set
<Sort
>& sorts
)
1032 std::set
<TypeNode
> types
;
1033 for (const Sort
& s
: sorts
)
1035 types
.insert(s
.getTypeNode());
1040 std::vector
<TypeNode
> Sort::sortVectorToTypeNodes(
1041 const std::vector
<Sort
>& sorts
)
1043 std::vector
<TypeNode
> typeNodes
;
1044 for (const Sort
& sort
: sorts
)
1046 typeNodes
.push_back(sort
.getTypeNode());
1051 std::vector
<Sort
> Sort::typeNodeVectorToSorts(
1052 const Solver
* slv
, const std::vector
<TypeNode
>& types
)
1054 std::vector
<Sort
> sorts
;
1055 for (size_t i
= 0, tsize
= types
.size(); i
< tsize
; i
++)
1057 sorts
.push_back(Sort(slv
, types
[i
]));
1062 bool Sort::operator==(const Sort
& s
) const
1064 CVC5_API_TRY_CATCH_BEGIN
;
1065 //////// all checks before this line
1066 return *d_type
== *s
.d_type
;
1068 CVC5_API_TRY_CATCH_END
;
1071 bool Sort::operator!=(const Sort
& s
) const
1073 CVC5_API_TRY_CATCH_BEGIN
;
1074 //////// all checks before this line
1075 return *d_type
!= *s
.d_type
;
1077 CVC5_API_TRY_CATCH_END
;
1080 bool Sort::operator<(const Sort
& s
) const
1082 CVC5_API_TRY_CATCH_BEGIN
;
1083 //////// all checks before this line
1084 return *d_type
< *s
.d_type
;
1086 CVC5_API_TRY_CATCH_END
;
1089 bool Sort::operator>(const Sort
& s
) const
1091 CVC5_API_TRY_CATCH_BEGIN
;
1092 //////// all checks before this line
1093 return *d_type
> *s
.d_type
;
1095 CVC5_API_TRY_CATCH_END
;
1098 bool Sort::operator<=(const Sort
& s
) const
1100 CVC5_API_TRY_CATCH_BEGIN
;
1101 //////// all checks before this line
1102 return *d_type
<= *s
.d_type
;
1104 CVC5_API_TRY_CATCH_END
;
1107 bool Sort::operator>=(const Sort
& s
) const
1109 CVC5_API_TRY_CATCH_BEGIN
;
1110 //////// all checks before this line
1111 return *d_type
>= *s
.d_type
;
1113 CVC5_API_TRY_CATCH_END
;
1116 bool Sort::hasSymbol() const
1118 CVC5_API_TRY_CATCH_BEGIN
;
1119 CVC5_API_CHECK_NOT_NULL
;
1120 //////// all checks before this line
1121 return d_type
->hasAttribute(expr::VarNameAttr());
1123 CVC5_API_TRY_CATCH_END
;
1126 std::string
Sort::getSymbol() const
1128 CVC5_API_TRY_CATCH_BEGIN
;
1129 CVC5_API_CHECK_NOT_NULL
;
1130 CVC5_API_CHECK(d_type
->hasAttribute(expr::VarNameAttr()))
1131 << "Invalid call to '" << __PRETTY_FUNCTION__
1132 << "', expected the sort to have a symbol.";
1133 //////// all checks before this line
1134 return d_type
->getAttribute(expr::VarNameAttr());
1136 CVC5_API_TRY_CATCH_END
;
1139 bool Sort::isNull() const
1141 CVC5_API_TRY_CATCH_BEGIN
;
1142 //////// all checks before this line
1143 return isNullHelper();
1145 CVC5_API_TRY_CATCH_END
;
1148 bool Sort::isBoolean() const
1150 CVC5_API_TRY_CATCH_BEGIN
;
1151 //////// all checks before this line
1152 return d_type
->isBoolean();
1154 CVC5_API_TRY_CATCH_END
;
1157 bool Sort::isInteger() const
1159 CVC5_API_TRY_CATCH_BEGIN
;
1160 //////// all checks before this line
1161 return d_type
->isInteger();
1163 CVC5_API_TRY_CATCH_END
;
1166 bool Sort::isReal() const
1168 CVC5_API_TRY_CATCH_BEGIN
;
1169 //////// all checks before this line
1170 // notice that we do not expose internal subtyping to the user
1171 return d_type
->isReal() && !d_type
->isInteger();
1173 CVC5_API_TRY_CATCH_END
;
1176 bool Sort::isString() const
1178 CVC5_API_TRY_CATCH_BEGIN
;
1179 //////// all checks before this line
1180 return d_type
->isString();
1182 CVC5_API_TRY_CATCH_END
;
1185 bool Sort::isRegExp() const
1187 CVC5_API_TRY_CATCH_BEGIN
;
1188 //////// all checks before this line
1189 return d_type
->isRegExp();
1191 CVC5_API_TRY_CATCH_END
;
1194 bool Sort::isRoundingMode() const
1196 CVC5_API_TRY_CATCH_BEGIN
;
1197 //////// all checks before this line
1198 return d_type
->isRoundingMode();
1200 CVC5_API_TRY_CATCH_END
;
1203 bool Sort::isBitVector() const
1205 CVC5_API_TRY_CATCH_BEGIN
;
1206 //////// all checks before this line
1207 return d_type
->isBitVector();
1209 CVC5_API_TRY_CATCH_END
;
1212 bool Sort::isFloatingPoint() const
1214 CVC5_API_TRY_CATCH_BEGIN
;
1215 //////// all checks before this line
1216 return d_type
->isFloatingPoint();
1218 CVC5_API_TRY_CATCH_END
;
1221 bool Sort::isDatatype() const
1223 CVC5_API_TRY_CATCH_BEGIN
;
1224 //////// all checks before this line
1225 return d_type
->isDatatype();
1227 CVC5_API_TRY_CATCH_END
;
1230 bool Sort::isParametricDatatype() const
1232 CVC5_API_TRY_CATCH_BEGIN
;
1233 //////// all checks before this line
1234 if (!d_type
->isDatatype()) return false;
1235 return d_type
->isParametricDatatype();
1237 CVC5_API_TRY_CATCH_END
;
1240 bool Sort::isConstructor() const
1242 CVC5_API_TRY_CATCH_BEGIN
;
1243 //////// all checks before this line
1244 return d_type
->isConstructor();
1246 CVC5_API_TRY_CATCH_END
;
1249 bool Sort::isSelector() const
1251 CVC5_API_TRY_CATCH_BEGIN
;
1252 //////// all checks before this line
1253 return d_type
->isSelector();
1255 CVC5_API_TRY_CATCH_END
;
1258 bool Sort::isTester() const
1260 CVC5_API_TRY_CATCH_BEGIN
;
1261 //////// all checks before this line
1262 return d_type
->isTester();
1264 CVC5_API_TRY_CATCH_END
;
1267 bool Sort::isUpdater() const
1269 CVC5_API_TRY_CATCH_BEGIN
;
1270 //////// all checks before this line
1271 return d_type
->isUpdater();
1273 CVC5_API_TRY_CATCH_END
;
1276 bool Sort::isFunction() const
1278 CVC5_API_TRY_CATCH_BEGIN
;
1279 //////// all checks before this line
1280 return d_type
->isFunction();
1282 CVC5_API_TRY_CATCH_END
;
1285 bool Sort::isPredicate() const
1287 CVC5_API_TRY_CATCH_BEGIN
;
1288 //////// all checks before this line
1289 return d_type
->isPredicate();
1291 CVC5_API_TRY_CATCH_END
;
1294 bool Sort::isTuple() const
1296 CVC5_API_TRY_CATCH_BEGIN
;
1297 //////// all checks before this line
1298 return d_type
->isTuple();
1300 CVC5_API_TRY_CATCH_END
;
1303 bool Sort::isRecord() const
1305 CVC5_API_TRY_CATCH_BEGIN
;
1306 //////// all checks before this line
1307 return d_type
->isRecord();
1309 CVC5_API_TRY_CATCH_END
;
1312 bool Sort::isArray() const
1314 CVC5_API_TRY_CATCH_BEGIN
;
1315 //////// all checks before this line
1316 return d_type
->isArray();
1318 CVC5_API_TRY_CATCH_END
;
1321 bool Sort::isSet() const
1323 CVC5_API_TRY_CATCH_BEGIN
;
1324 //////// all checks before this line
1325 return d_type
->isSet();
1327 CVC5_API_TRY_CATCH_END
;
1330 bool Sort::isBag() const
1332 CVC5_API_TRY_CATCH_BEGIN
;
1333 //////// all checks before this line
1334 return d_type
->isBag();
1336 CVC5_API_TRY_CATCH_END
;
1339 bool Sort::isSequence() const
1341 CVC5_API_TRY_CATCH_BEGIN
;
1342 //////// all checks before this line
1343 return d_type
->isSequence();
1345 CVC5_API_TRY_CATCH_END
;
1348 bool Sort::isUninterpretedSort() const
1350 CVC5_API_TRY_CATCH_BEGIN
;
1351 //////// all checks before this line
1352 return d_type
->isSort();
1354 CVC5_API_TRY_CATCH_END
;
1357 bool Sort::isSortConstructor() const
1359 CVC5_API_TRY_CATCH_BEGIN
;
1360 //////// all checks before this line
1361 return d_type
->isSortConstructor();
1363 CVC5_API_TRY_CATCH_END
;
1366 bool Sort::isFirstClass() const
1368 CVC5_API_TRY_CATCH_BEGIN
;
1369 //////// all checks before this line
1370 return d_type
->isFirstClass();
1372 CVC5_API_TRY_CATCH_END
;
1375 bool Sort::isFunctionLike() const
1377 CVC5_API_TRY_CATCH_BEGIN
;
1378 //////// all checks before this line
1379 return d_type
->isFunctionLike();
1381 CVC5_API_TRY_CATCH_END
;
1384 bool Sort::isSubsortOf(const Sort
& s
) const
1386 CVC5_API_TRY_CATCH_BEGIN
;
1387 CVC5_API_ARG_CHECK_SOLVER("sort", s
);
1388 //////// all checks before this line
1389 return d_type
->isSubtypeOf(*s
.d_type
);
1391 CVC5_API_TRY_CATCH_END
;
1394 bool Sort::isComparableTo(const Sort
& s
) const
1396 CVC5_API_TRY_CATCH_BEGIN
;
1397 CVC5_API_ARG_CHECK_SOLVER("sort", s
);
1398 //////// all checks before this line
1399 return d_type
->isComparableTo(*s
.d_type
);
1401 CVC5_API_TRY_CATCH_END
;
1404 Datatype
Sort::getDatatype() const
1406 CVC5_API_TRY_CATCH_BEGIN
;
1407 CVC5_API_CHECK_NOT_NULL
;
1408 CVC5_API_CHECK(isDatatype()) << "Expected datatype sort.";
1409 //////// all checks before this line
1410 return Datatype(d_solver
, d_type
->getDType());
1412 CVC5_API_TRY_CATCH_END
;
1415 Sort
Sort::instantiate(const std::vector
<Sort
>& params
) const
1417 CVC5_API_TRY_CATCH_BEGIN
;
1418 CVC5_API_CHECK_NOT_NULL
;
1419 CVC5_API_CHECK_SORTS(params
);
1420 CVC5_API_CHECK(isParametricDatatype() || isSortConstructor())
1421 << "Expected parametric datatype or sort constructor sort.";
1422 //////// all checks before this line
1423 std::vector
<cvc5::TypeNode
> tparams
= sortVectorToTypeNodes(params
);
1424 if (d_type
->isDatatype())
1426 return Sort(d_solver
, d_type
->instantiateParametricDatatype(tparams
));
1428 Assert(d_type
->isSortConstructor());
1429 return Sort(d_solver
, d_solver
->getNodeManager()->mkSort(*d_type
, tparams
));
1431 CVC5_API_TRY_CATCH_END
;
1434 Sort
Sort::substitute(const Sort
& sort
, const Sort
& replacement
) const
1436 CVC5_API_TRY_CATCH_BEGIN
;
1437 CVC5_API_CHECK_NOT_NULL
;
1438 CVC5_API_CHECK_SORT(sort
);
1439 CVC5_API_CHECK_SORT(replacement
);
1440 //////// all checks before this line
1443 d_type
->substitute(sort
.getTypeNode(), replacement
.getTypeNode()));
1445 CVC5_API_TRY_CATCH_END
;
1448 Sort
Sort::substitute(const std::vector
<Sort
>& sorts
,
1449 const std::vector
<Sort
>& replacements
) const
1451 CVC5_API_TRY_CATCH_BEGIN
;
1452 CVC5_API_CHECK_NOT_NULL
;
1453 CVC5_API_CHECK_SORTS(sorts
);
1454 CVC5_API_CHECK_SORTS(replacements
);
1455 //////// all checks before this line
1457 std::vector
<cvc5::TypeNode
> tSorts
= sortVectorToTypeNodes(sorts
),
1459 sortVectorToTypeNodes(replacements
);
1460 return Sort(d_solver
,
1461 d_type
->substitute(tSorts
.begin(),
1463 tReplacements
.begin(),
1464 tReplacements
.end()));
1466 CVC5_API_TRY_CATCH_END
;
1469 std::string
Sort::toString() const
1471 CVC5_API_TRY_CATCH_BEGIN
;
1472 //////// all checks before this line
1473 return d_type
->toString();
1475 CVC5_API_TRY_CATCH_END
;
1478 const cvc5::TypeNode
& Sort::getTypeNode(void) const { return *d_type
; }
1480 /* Constructor sort ------------------------------------------------------- */
1482 size_t Sort::getConstructorArity() const
1484 CVC5_API_TRY_CATCH_BEGIN
;
1485 CVC5_API_CHECK_NOT_NULL
;
1486 CVC5_API_CHECK(isConstructor()) << "Not a constructor sort: " << (*this);
1487 //////// all checks before this line
1488 return d_type
->getNumChildren() - 1;
1490 CVC5_API_TRY_CATCH_END
;
1493 std::vector
<Sort
> Sort::getConstructorDomainSorts() const
1495 CVC5_API_TRY_CATCH_BEGIN
;
1496 CVC5_API_CHECK_NOT_NULL
;
1497 CVC5_API_CHECK(isConstructor()) << "Not a constructor sort: " << (*this);
1498 //////// all checks before this line
1499 return typeNodeVectorToSorts(d_solver
, d_type
->getArgTypes());
1501 CVC5_API_TRY_CATCH_END
;
1504 Sort
Sort::getConstructorCodomainSort() const
1506 CVC5_API_TRY_CATCH_BEGIN
;
1507 CVC5_API_CHECK_NOT_NULL
;
1508 CVC5_API_CHECK(isConstructor()) << "Not a constructor sort: " << (*this);
1509 //////// all checks before this line
1510 return Sort(d_solver
, d_type
->getConstructorRangeType());
1512 CVC5_API_TRY_CATCH_END
;
1515 /* Selector sort ------------------------------------------------------- */
1517 Sort
Sort::getSelectorDomainSort() const
1519 CVC5_API_TRY_CATCH_BEGIN
;
1520 CVC5_API_CHECK_NOT_NULL
;
1521 CVC5_API_CHECK(isSelector()) << "Not a selector sort: " << (*this);
1522 //////// all checks before this line
1523 return Sort(d_solver
, d_type
->getSelectorDomainType());
1525 CVC5_API_TRY_CATCH_END
;
1528 Sort
Sort::getSelectorCodomainSort() const
1530 CVC5_API_TRY_CATCH_BEGIN
;
1531 CVC5_API_CHECK_NOT_NULL
;
1532 CVC5_API_CHECK(isSelector()) << "Not a selector sort: " << (*this);
1533 //////// all checks before this line
1534 return Sort(d_solver
, d_type
->getSelectorRangeType());
1536 CVC5_API_TRY_CATCH_END
;
1539 /* Tester sort ------------------------------------------------------- */
1541 Sort
Sort::getTesterDomainSort() const
1543 CVC5_API_TRY_CATCH_BEGIN
;
1544 CVC5_API_CHECK_NOT_NULL
;
1545 CVC5_API_CHECK(isTester()) << "Not a tester sort: " << (*this);
1546 //////// all checks before this line
1547 return Sort(d_solver
, d_type
->getTesterDomainType());
1549 CVC5_API_TRY_CATCH_END
;
1552 Sort
Sort::getTesterCodomainSort() const
1554 CVC5_API_TRY_CATCH_BEGIN
;
1555 CVC5_API_CHECK_NOT_NULL
;
1556 CVC5_API_CHECK(isTester()) << "Not a tester sort: " << (*this);
1557 //////// all checks before this line
1558 return d_solver
->getBooleanSort();
1560 CVC5_API_TRY_CATCH_END
;
1563 /* Function sort ------------------------------------------------------- */
1565 size_t Sort::getFunctionArity() const
1567 CVC5_API_TRY_CATCH_BEGIN
;
1568 CVC5_API_CHECK_NOT_NULL
;
1569 CVC5_API_CHECK(isFunction()) << "Not a function sort: " << (*this);
1570 //////// all checks before this line
1571 return d_type
->getNumChildren() - 1;
1573 CVC5_API_TRY_CATCH_END
;
1576 std::vector
<Sort
> Sort::getFunctionDomainSorts() const
1578 CVC5_API_TRY_CATCH_BEGIN
;
1579 CVC5_API_CHECK_NOT_NULL
;
1580 CVC5_API_CHECK(isFunction()) << "Not a function sort: " << (*this);
1581 //////// all checks before this line
1582 return typeNodeVectorToSorts(d_solver
, d_type
->getArgTypes());
1584 CVC5_API_TRY_CATCH_END
;
1587 Sort
Sort::getFunctionCodomainSort() const
1589 CVC5_API_TRY_CATCH_BEGIN
;
1590 CVC5_API_CHECK_NOT_NULL
;
1591 CVC5_API_CHECK(isFunction()) << "Not a function sort" << (*this);
1592 //////// all checks before this line
1593 return Sort(d_solver
, d_type
->getRangeType());
1595 CVC5_API_TRY_CATCH_END
;
1598 /* Array sort ---------------------------------------------------------- */
1600 Sort
Sort::getArrayIndexSort() const
1602 CVC5_API_TRY_CATCH_BEGIN
;
1603 CVC5_API_CHECK_NOT_NULL
;
1604 CVC5_API_CHECK(isArray()) << "Not an array sort.";
1605 //////// all checks before this line
1606 return Sort(d_solver
, d_type
->getArrayIndexType());
1608 CVC5_API_TRY_CATCH_END
;
1611 Sort
Sort::getArrayElementSort() const
1613 CVC5_API_TRY_CATCH_BEGIN
;
1614 CVC5_API_CHECK_NOT_NULL
;
1615 CVC5_API_CHECK(isArray()) << "Not an array sort.";
1616 //////// all checks before this line
1617 return Sort(d_solver
, d_type
->getArrayConstituentType());
1619 CVC5_API_TRY_CATCH_END
;
1622 /* Set sort ------------------------------------------------------------ */
1624 Sort
Sort::getSetElementSort() const
1626 CVC5_API_TRY_CATCH_BEGIN
;
1627 CVC5_API_CHECK_NOT_NULL
;
1628 CVC5_API_CHECK(isSet()) << "Not a set sort.";
1629 //////// all checks before this line
1630 return Sort(d_solver
, d_type
->getSetElementType());
1632 CVC5_API_TRY_CATCH_END
;
1635 /* Bag sort ------------------------------------------------------------ */
1637 Sort
Sort::getBagElementSort() const
1639 CVC5_API_TRY_CATCH_BEGIN
;
1640 CVC5_API_CHECK_NOT_NULL
;
1641 CVC5_API_CHECK(isBag()) << "Not a bag sort.";
1642 //////// all checks before this line
1643 return Sort(d_solver
, d_type
->getBagElementType());
1645 CVC5_API_TRY_CATCH_END
;
1648 /* Sequence sort ------------------------------------------------------- */
1650 Sort
Sort::getSequenceElementSort() const
1652 CVC5_API_TRY_CATCH_BEGIN
;
1653 CVC5_API_CHECK_NOT_NULL
;
1654 CVC5_API_CHECK(isSequence()) << "Not a sequence sort.";
1655 //////// all checks before this line
1656 return Sort(d_solver
, d_type
->getSequenceElementType());
1658 CVC5_API_TRY_CATCH_END
;
1661 /* Uninterpreted sort -------------------------------------------------- */
1663 std::string
Sort::getUninterpretedSortName() const
1665 CVC5_API_TRY_CATCH_BEGIN
;
1666 CVC5_API_CHECK_NOT_NULL
;
1667 CVC5_API_CHECK(isUninterpretedSort()) << "Not an uninterpreted sort.";
1668 //////// all checks before this line
1669 return d_type
->getName();
1671 CVC5_API_TRY_CATCH_END
;
1674 bool Sort::isUninterpretedSortParameterized() const
1676 CVC5_API_TRY_CATCH_BEGIN
;
1677 CVC5_API_CHECK_NOT_NULL
;
1678 CVC5_API_CHECK(isUninterpretedSort()) << "Not an uninterpreted sort.";
1679 //////// all checks before this line
1681 /* This method is not implemented in the NodeManager, since whether a
1682 * uninterpreted sort is parameterized is irrelevant for solving. */
1683 return d_type
->getNumChildren() > 0;
1685 CVC5_API_TRY_CATCH_END
;
1688 std::vector
<Sort
> Sort::getUninterpretedSortParamSorts() const
1690 CVC5_API_TRY_CATCH_BEGIN
;
1691 CVC5_API_CHECK_NOT_NULL
;
1692 CVC5_API_CHECK(isUninterpretedSort()) << "Not an uninterpreted sort.";
1693 //////// all checks before this line
1695 /* This method is not implemented in the NodeManager, since whether a
1696 * uninterpreted sort is parameterized is irrelevant for solving. */
1697 std::vector
<TypeNode
> params
;
1698 for (size_t i
= 0, nchildren
= d_type
->getNumChildren(); i
< nchildren
; i
++)
1700 params
.push_back((*d_type
)[i
]);
1702 return typeNodeVectorToSorts(d_solver
, params
);
1704 CVC5_API_TRY_CATCH_END
;
1707 /* Sort constructor sort ----------------------------------------------- */
1709 std::string
Sort::getSortConstructorName() const
1711 CVC5_API_TRY_CATCH_BEGIN
;
1712 CVC5_API_CHECK_NOT_NULL
;
1713 CVC5_API_CHECK(isSortConstructor()) << "Not a sort constructor sort.";
1714 //////// all checks before this line
1715 return d_type
->getName();
1717 CVC5_API_TRY_CATCH_END
;
1720 size_t Sort::getSortConstructorArity() const
1722 CVC5_API_TRY_CATCH_BEGIN
;
1723 CVC5_API_CHECK_NOT_NULL
;
1724 CVC5_API_CHECK(isSortConstructor()) << "Not a sort constructor sort.";
1725 //////// all checks before this line
1726 return d_type
->getSortConstructorArity();
1728 CVC5_API_TRY_CATCH_END
;
1731 /* Bit-vector sort ----------------------------------------------------- */
1733 uint32_t Sort::getBitVectorSize() const
1735 CVC5_API_TRY_CATCH_BEGIN
;
1736 CVC5_API_CHECK_NOT_NULL
;
1737 CVC5_API_CHECK(isBitVector()) << "Not a bit-vector sort.";
1738 //////// all checks before this line
1739 return d_type
->getBitVectorSize();
1741 CVC5_API_TRY_CATCH_END
;
1744 /* Floating-point sort ------------------------------------------------- */
1746 uint32_t Sort::getFloatingPointExponentSize() const
1748 CVC5_API_TRY_CATCH_BEGIN
;
1749 CVC5_API_CHECK_NOT_NULL
;
1750 CVC5_API_CHECK(isFloatingPoint()) << "Not a floating-point sort.";
1751 //////// all checks before this line
1752 return d_type
->getFloatingPointExponentSize();
1754 CVC5_API_TRY_CATCH_END
;
1757 uint32_t Sort::getFloatingPointSignificandSize() const
1759 CVC5_API_TRY_CATCH_BEGIN
;
1760 CVC5_API_CHECK_NOT_NULL
;
1761 CVC5_API_CHECK(isFloatingPoint()) << "Not a floating-point sort.";
1762 //////// all checks before this line
1763 return d_type
->getFloatingPointSignificandSize();
1765 CVC5_API_TRY_CATCH_END
;
1768 /* Datatype sort ------------------------------------------------------- */
1770 std::vector
<Sort
> Sort::getDatatypeParamSorts() const
1772 CVC5_API_TRY_CATCH_BEGIN
;
1773 CVC5_API_CHECK_NOT_NULL
;
1774 CVC5_API_CHECK(isParametricDatatype()) << "Not a parametric datatype sort.";
1775 //////// all checks before this line
1776 return typeNodeVectorToSorts(d_solver
, d_type
->getParamTypes());
1778 CVC5_API_TRY_CATCH_END
;
1781 size_t Sort::getDatatypeArity() const
1783 CVC5_API_TRY_CATCH_BEGIN
;
1784 CVC5_API_CHECK_NOT_NULL
;
1785 CVC5_API_CHECK(isDatatype()) << "Not a datatype sort.";
1786 //////// all checks before this line
1787 return d_type
->isParametricDatatype() ? d_type
->getNumChildren() - 1 : 0;
1789 CVC5_API_TRY_CATCH_END
;
1792 /* Tuple sort ---------------------------------------------------------- */
1794 size_t Sort::getTupleLength() const
1796 CVC5_API_TRY_CATCH_BEGIN
;
1797 CVC5_API_CHECK_NOT_NULL
;
1798 CVC5_API_CHECK(isTuple()) << "Not a tuple sort.";
1799 //////// all checks before this line
1800 return d_type
->getTupleLength();
1802 CVC5_API_TRY_CATCH_END
;
1805 std::vector
<Sort
> Sort::getTupleSorts() const
1807 CVC5_API_TRY_CATCH_BEGIN
;
1808 CVC5_API_CHECK_NOT_NULL
;
1809 CVC5_API_CHECK(isTuple()) << "Not a tuple sort.";
1810 //////// all checks before this line
1811 return typeNodeVectorToSorts(d_solver
, d_type
->getTupleTypes());
1813 CVC5_API_TRY_CATCH_END
;
1816 /* --------------------------------------------------------------------- */
1818 std::ostream
& operator<<(std::ostream
& out
, const Sort
& s
)
1820 out
<< s
.toString();
1825 /* -------------------------------------------------------------------------- */
1827 /* Split out to avoid nested API calls (problematic with API tracing). */
1828 /* .......................................................................... */
1830 bool Sort::isNullHelper() const { return d_type
->isNull(); }
1832 /* -------------------------------------------------------------------------- */
1834 /* -------------------------------------------------------------------------- */
1836 Op::Op() : d_solver(nullptr), d_kind(NULL_EXPR
), d_node(new cvc5::Node()) {}
1838 Op::Op(const Solver
* slv
, const Kind k
)
1839 : d_solver(slv
), d_kind(k
), d_node(new cvc5::Node())
1843 Op::Op(const Solver
* slv
, const Kind k
, const cvc5::Node
& n
)
1844 : d_solver(slv
), d_kind(k
), d_node(new cvc5::Node(n
))
1850 if (d_solver
!= nullptr)
1852 // Ensure that the correct node manager is in scope when the type node is
1858 /* Public methods */
1859 bool Op::operator==(const Op
& t
) const
1861 CVC5_API_TRY_CATCH_BEGIN
;
1862 //////// all checks before this line
1863 if (d_node
->isNull() && t
.d_node
->isNull())
1865 return (d_kind
== t
.d_kind
);
1867 else if (d_node
->isNull() || t
.d_node
->isNull())
1871 return (d_kind
== t
.d_kind
) && (*d_node
== *t
.d_node
);
1873 CVC5_API_TRY_CATCH_END
;
1876 bool Op::operator!=(const Op
& t
) const
1878 CVC5_API_TRY_CATCH_BEGIN
;
1879 //////// all checks before this line
1880 return !(*this == t
);
1882 CVC5_API_TRY_CATCH_END
;
1885 Kind
Op::getKind() const
1887 CVC5_API_CHECK(d_kind
!= NULL_EXPR
) << "Expecting a non-null Kind";
1888 //////// all checks before this line
1892 bool Op::isNull() const
1894 CVC5_API_TRY_CATCH_BEGIN
;
1895 //////// all checks before this line
1896 return isNullHelper();
1898 CVC5_API_TRY_CATCH_END
;
1901 bool Op::isIndexed() const
1903 CVC5_API_TRY_CATCH_BEGIN
;
1904 //////// all checks before this line
1905 return isIndexedHelper();
1907 CVC5_API_TRY_CATCH_END
;
1910 size_t Op::getNumIndices() const
1912 CVC5_API_TRY_CATCH_BEGIN
;
1913 CVC5_API_CHECK_NOT_NULL
;
1914 //////// all checks before this line
1915 return getNumIndicesHelper();
1917 CVC5_API_TRY_CATCH_END
;
1920 size_t Op::getNumIndicesHelper() const
1922 if (!isIndexedHelper())
1927 Kind k
= intToExtKind(d_node
->getKind());
1931 case DIVISIBLE
: size
= 1; break;
1932 case BITVECTOR_REPEAT
: size
= 1; break;
1933 case BITVECTOR_ZERO_EXTEND
: size
= 1; break;
1934 case BITVECTOR_SIGN_EXTEND
: size
= 1; break;
1935 case BITVECTOR_ROTATE_LEFT
: size
= 1; break;
1936 case BITVECTOR_ROTATE_RIGHT
: size
= 1; break;
1937 case INT_TO_BITVECTOR
: size
= 1; break;
1938 case IAND
: size
= 1; break;
1939 case FLOATINGPOINT_TO_UBV
: size
= 1; break;
1940 case FLOATINGPOINT_TO_SBV
: size
= 1; break;
1941 case REGEXP_REPEAT
: size
= 1; break;
1942 case BITVECTOR_EXTRACT
: size
= 2; break;
1943 case FLOATINGPOINT_TO_FP_IEEE_BITVECTOR
: size
= 2; break;
1944 case FLOATINGPOINT_TO_FP_FLOATINGPOINT
: size
= 2; break;
1945 case FLOATINGPOINT_TO_FP_REAL
: size
= 2; break;
1946 case FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR
: size
= 2; break;
1947 case FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR
: size
= 2; break;
1948 case FLOATINGPOINT_TO_FP_GENERIC
: size
= 2; break;
1949 case REGEXP_LOOP
: size
= 2; break;
1951 size
= d_node
->getConst
<TupleProjectOp
>().getIndices().size();
1953 default: CVC5_API_CHECK(false) << "Unhandled kind " << kindToString(k
);
1958 Term
Op::operator[](size_t index
) const
1960 return getIndexHelper(index
);
1963 Term
Op::getIndexHelper(size_t index
) const
1965 CVC5_API_TRY_CATCH_BEGIN
;
1966 CVC5_API_CHECK_NOT_NULL
;
1967 CVC5_API_CHECK(!d_node
->isNull())
1968 << "Expecting a non-null internal expression. This Op is not indexed.";
1969 CVC5_API_CHECK(index
< getNumIndicesHelper()) << "index out of bound";
1970 Kind k
= intToExtKind(d_node
->getKind());
1976 t
= d_solver
->mkRationalValHelper(
1977 Rational(d_node
->getConst
<Divisible
>().k
));
1980 case BITVECTOR_REPEAT
:
1982 t
= d_solver
->mkRationalValHelper(
1983 d_node
->getConst
<BitVectorRepeat
>().d_repeatAmount
);
1986 case BITVECTOR_ZERO_EXTEND
:
1988 t
= d_solver
->mkRationalValHelper(
1989 d_node
->getConst
<BitVectorZeroExtend
>().d_zeroExtendAmount
);
1992 case BITVECTOR_SIGN_EXTEND
:
1994 t
= d_solver
->mkRationalValHelper(
1995 d_node
->getConst
<BitVectorSignExtend
>().d_signExtendAmount
);
1998 case BITVECTOR_ROTATE_LEFT
:
2000 t
= d_solver
->mkRationalValHelper(
2001 d_node
->getConst
<BitVectorRotateLeft
>().d_rotateLeftAmount
);
2004 case BITVECTOR_ROTATE_RIGHT
:
2006 t
= d_solver
->mkRationalValHelper(
2007 d_node
->getConst
<BitVectorRotateRight
>().d_rotateRightAmount
);
2010 case INT_TO_BITVECTOR
:
2012 t
= d_solver
->mkRationalValHelper(
2013 d_node
->getConst
<IntToBitVector
>().d_size
);
2018 t
= d_solver
->mkRationalValHelper(d_node
->getConst
<IntAnd
>().d_size
);
2021 case FLOATINGPOINT_TO_UBV
:
2023 t
= d_solver
->mkRationalValHelper(
2024 d_node
->getConst
<FloatingPointToUBV
>().d_bv_size
.d_size
);
2027 case FLOATINGPOINT_TO_SBV
:
2029 t
= d_solver
->mkRationalValHelper(
2030 d_node
->getConst
<FloatingPointToSBV
>().d_bv_size
.d_size
);
2035 t
= d_solver
->mkRationalValHelper(
2036 d_node
->getConst
<RegExpRepeat
>().d_repeatAmount
);
2039 case BITVECTOR_EXTRACT
:
2041 cvc5::BitVectorExtract ext
= d_node
->getConst
<BitVectorExtract
>();
2042 t
= index
== 0 ? d_solver
->mkRationalValHelper(ext
.d_high
)
2043 : d_solver
->mkRationalValHelper(ext
.d_low
);
2046 case FLOATINGPOINT_TO_FP_IEEE_BITVECTOR
:
2048 cvc5::FloatingPointToFPIEEEBitVector ext
=
2049 d_node
->getConst
<FloatingPointToFPIEEEBitVector
>();
2052 ? d_solver
->mkRationalValHelper(ext
.getSize().exponentWidth())
2053 : d_solver
->mkRationalValHelper(ext
.getSize().significandWidth());
2056 case FLOATINGPOINT_TO_FP_FLOATINGPOINT
:
2058 cvc5::FloatingPointToFPFloatingPoint ext
=
2059 d_node
->getConst
<FloatingPointToFPFloatingPoint
>();
2061 ? d_solver
->mkRationalValHelper(ext
.getSize().exponentWidth())
2062 : d_solver
->mkRationalValHelper(ext
.getSize().significandWidth());
2065 case FLOATINGPOINT_TO_FP_REAL
:
2067 cvc5::FloatingPointToFPReal ext
=
2068 d_node
->getConst
<FloatingPointToFPReal
>();
2071 ? d_solver
->mkRationalValHelper(ext
.getSize().exponentWidth())
2072 : d_solver
->mkRationalValHelper(ext
.getSize().significandWidth());
2075 case FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR
:
2077 cvc5::FloatingPointToFPSignedBitVector ext
=
2078 d_node
->getConst
<FloatingPointToFPSignedBitVector
>();
2080 ? d_solver
->mkRationalValHelper(ext
.getSize().exponentWidth())
2081 : d_solver
->mkRationalValHelper(ext
.getSize().significandWidth());
2084 case FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR
:
2086 cvc5::FloatingPointToFPUnsignedBitVector ext
=
2087 d_node
->getConst
<FloatingPointToFPUnsignedBitVector
>();
2089 ? d_solver
->mkRationalValHelper(ext
.getSize().exponentWidth())
2090 : d_solver
->mkRationalValHelper(ext
.getSize().significandWidth());
2093 case FLOATINGPOINT_TO_FP_GENERIC
:
2095 cvc5::FloatingPointToFPGeneric ext
=
2096 d_node
->getConst
<FloatingPointToFPGeneric
>();
2098 ? d_solver
->mkRationalValHelper(ext
.getSize().exponentWidth())
2099 : d_solver
->mkRationalValHelper(ext
.getSize().significandWidth());
2104 cvc5::RegExpLoop ext
= d_node
->getConst
<RegExpLoop
>();
2105 t
= index
== 0 ? d_solver
->mkRationalValHelper(ext
.d_loopMinOcc
)
2106 : d_solver
->mkRationalValHelper(ext
.d_loopMaxOcc
);
2113 const std::vector
<uint32_t>& projectionIndices
=
2114 d_node
->getConst
<TupleProjectOp
>().getIndices();
2115 t
= d_solver
->mkRationalValHelper(projectionIndices
[index
]);
2120 CVC5_API_CHECK(false) << "Unhandled kind " << kindToString(k
);
2125 //////// all checks before this line
2128 CVC5_API_TRY_CATCH_END
;
2132 std::string
Op::getIndices() const
2134 CVC5_API_TRY_CATCH_BEGIN
;
2135 CVC5_API_CHECK_NOT_NULL
;
2136 CVC5_API_CHECK(!d_node
->isNull())
2137 << "Expecting a non-null internal expression. This Op is not indexed.";
2138 Kind k
= intToExtKind(d_node
->getKind());
2139 CVC5_API_CHECK(k
== DIVISIBLE
) << "Can't get string index from"
2140 << " kind " << kindToString(k
);
2141 //////// all checks before this line
2142 return d_node
->getConst
<Divisible
>().k
.toString();
2144 CVC5_API_TRY_CATCH_END
;
2148 uint32_t Op::getIndices() const
2150 CVC5_API_TRY_CATCH_BEGIN
;
2151 CVC5_API_CHECK_NOT_NULL
;
2152 CVC5_API_CHECK(!d_node
->isNull())
2153 << "Expecting a non-null internal expression. This Op is not indexed.";
2154 //////// all checks before this line
2157 Kind k
= intToExtKind(d_node
->getKind());
2160 case BITVECTOR_REPEAT
:
2161 i
= d_node
->getConst
<BitVectorRepeat
>().d_repeatAmount
;
2163 case BITVECTOR_ZERO_EXTEND
:
2164 i
= d_node
->getConst
<BitVectorZeroExtend
>().d_zeroExtendAmount
;
2166 case BITVECTOR_SIGN_EXTEND
:
2167 i
= d_node
->getConst
<BitVectorSignExtend
>().d_signExtendAmount
;
2169 case BITVECTOR_ROTATE_LEFT
:
2170 i
= d_node
->getConst
<BitVectorRotateLeft
>().d_rotateLeftAmount
;
2172 case BITVECTOR_ROTATE_RIGHT
:
2173 i
= d_node
->getConst
<BitVectorRotateRight
>().d_rotateRightAmount
;
2175 case INT_TO_BITVECTOR
: i
= d_node
->getConst
<IntToBitVector
>().d_size
; break;
2176 case IAND
: i
= d_node
->getConst
<IntAnd
>().d_size
; break;
2177 case FLOATINGPOINT_TO_UBV
:
2178 i
= d_node
->getConst
<FloatingPointToUBV
>().d_bv_size
.d_size
;
2180 case FLOATINGPOINT_TO_SBV
:
2181 i
= d_node
->getConst
<FloatingPointToSBV
>().d_bv_size
.d_size
;
2184 i
= d_node
->getConst
<RegExpRepeat
>().d_repeatAmount
;
2187 CVC5_API_CHECK(false) << "Can't get uint32_t index from"
2188 << " kind " << kindToString(k
);
2192 CVC5_API_TRY_CATCH_END
;
2196 std::pair
<uint32_t, uint32_t> Op::getIndices() const
2198 CVC5_API_TRY_CATCH_BEGIN
;
2199 CVC5_API_CHECK_NOT_NULL
;
2200 CVC5_API_CHECK(!d_node
->isNull())
2201 << "Expecting a non-null internal expression. This Op is not indexed.";
2202 //////// all checks before this line
2204 std::pair
<uint32_t, uint32_t> indices
;
2205 Kind k
= intToExtKind(d_node
->getKind());
2207 // using if/else instead of case statement because want local variables
2208 if (k
== BITVECTOR_EXTRACT
)
2210 cvc5::BitVectorExtract ext
= d_node
->getConst
<BitVectorExtract
>();
2211 indices
= std::make_pair(ext
.d_high
, ext
.d_low
);
2213 else if (k
== FLOATINGPOINT_TO_FP_IEEE_BITVECTOR
)
2215 cvc5::FloatingPointToFPIEEEBitVector ext
=
2216 d_node
->getConst
<FloatingPointToFPIEEEBitVector
>();
2217 indices
= std::make_pair(ext
.getSize().exponentWidth(),
2218 ext
.getSize().significandWidth());
2220 else if (k
== FLOATINGPOINT_TO_FP_FLOATINGPOINT
)
2222 cvc5::FloatingPointToFPFloatingPoint ext
=
2223 d_node
->getConst
<FloatingPointToFPFloatingPoint
>();
2224 indices
= std::make_pair(ext
.getSize().exponentWidth(),
2225 ext
.getSize().significandWidth());
2227 else if (k
== FLOATINGPOINT_TO_FP_REAL
)
2229 cvc5::FloatingPointToFPReal ext
= d_node
->getConst
<FloatingPointToFPReal
>();
2230 indices
= std::make_pair(ext
.getSize().exponentWidth(),
2231 ext
.getSize().significandWidth());
2233 else if (k
== FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR
)
2235 cvc5::FloatingPointToFPSignedBitVector ext
=
2236 d_node
->getConst
<FloatingPointToFPSignedBitVector
>();
2237 indices
= std::make_pair(ext
.getSize().exponentWidth(),
2238 ext
.getSize().significandWidth());
2240 else if (k
== FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR
)
2242 cvc5::FloatingPointToFPUnsignedBitVector ext
=
2243 d_node
->getConst
<FloatingPointToFPUnsignedBitVector
>();
2244 indices
= std::make_pair(ext
.getSize().exponentWidth(),
2245 ext
.getSize().significandWidth());
2247 else if (k
== FLOATINGPOINT_TO_FP_GENERIC
)
2249 cvc5::FloatingPointToFPGeneric ext
=
2250 d_node
->getConst
<FloatingPointToFPGeneric
>();
2251 indices
= std::make_pair(ext
.getSize().exponentWidth(),
2252 ext
.getSize().significandWidth());
2254 else if (k
== REGEXP_LOOP
)
2256 cvc5::RegExpLoop ext
= d_node
->getConst
<RegExpLoop
>();
2257 indices
= std::make_pair(ext
.d_loopMinOcc
, ext
.d_loopMaxOcc
);
2261 CVC5_API_CHECK(false) << "Can't get pair<uint32_t, uint32_t> indices from"
2262 << " kind " << kindToString(k
);
2266 CVC5_API_TRY_CATCH_END
;
2270 std::vector
<api::Term
> Op::getIndices() const
2272 CVC5_API_TRY_CATCH_BEGIN
;
2273 CVC5_API_CHECK_NOT_NULL
;
2274 CVC5_API_CHECK(!d_node
->isNull())
2275 << "Expecting a non-null internal expression. This Op is not indexed.";
2276 size_t size
= getNumIndicesHelper();
2277 std::vector
<Term
> terms(getNumIndices());
2278 for (size_t i
= 0; i
< size
; i
++)
2280 terms
[i
] = getIndexHelper(i
);
2282 //////// all checks before this line
2285 CVC5_API_TRY_CATCH_END
;
2288 std::string
Op::toString() const
2290 CVC5_API_TRY_CATCH_BEGIN
;
2291 //////// all checks before this line
2292 if (d_node
->isNull())
2294 return kindToString(d_kind
);
2298 CVC5_API_CHECK(!d_node
->isNull())
2299 << "Expecting a non-null internal expression";
2300 if (d_solver
!= nullptr)
2302 return d_node
->toString();
2304 return d_node
->toString();
2307 CVC5_API_TRY_CATCH_END
;
2310 std::ostream
& operator<<(std::ostream
& out
, const Op
& t
)
2312 out
<< t
.toString();
2317 /* -------------------------------------------------------------------------- */
2319 /* Split out to avoid nested API calls (problematic with API tracing). */
2320 /* .......................................................................... */
2322 bool Op::isNullHelper() const
2324 return (d_node
->isNull() && (d_kind
== NULL_EXPR
));
2327 bool Op::isIndexedHelper() const { return !d_node
->isNull(); }
2329 /* -------------------------------------------------------------------------- */
2331 /* -------------------------------------------------------------------------- */
2333 Term::Term() : d_solver(nullptr), d_node(new cvc5::Node()) {}
2335 Term::Term(const Solver
* slv
, const cvc5::Node
& n
) : d_solver(slv
)
2337 d_node
.reset(new cvc5::Node(n
));
2342 if (d_solver
!= nullptr)
2348 bool Term::operator==(const Term
& t
) const
2350 CVC5_API_TRY_CATCH_BEGIN
;
2351 //////// all checks before this line
2352 return *d_node
== *t
.d_node
;
2354 CVC5_API_TRY_CATCH_END
;
2357 bool Term::operator!=(const Term
& t
) const
2359 CVC5_API_TRY_CATCH_BEGIN
;
2360 //////// all checks before this line
2361 return *d_node
!= *t
.d_node
;
2363 CVC5_API_TRY_CATCH_END
;
2366 bool Term::operator<(const Term
& t
) const
2368 CVC5_API_TRY_CATCH_BEGIN
;
2369 //////// all checks before this line
2370 return *d_node
< *t
.d_node
;
2372 CVC5_API_TRY_CATCH_END
;
2375 bool Term::operator>(const Term
& t
) const
2377 CVC5_API_TRY_CATCH_BEGIN
;
2378 //////// all checks before this line
2379 return *d_node
> *t
.d_node
;
2381 CVC5_API_TRY_CATCH_END
;
2384 bool Term::operator<=(const Term
& t
) const
2386 CVC5_API_TRY_CATCH_BEGIN
;
2387 //////// all checks before this line
2388 return *d_node
<= *t
.d_node
;
2390 CVC5_API_TRY_CATCH_END
;
2393 bool Term::operator>=(const Term
& t
) const
2395 CVC5_API_TRY_CATCH_BEGIN
;
2396 //////// all checks before this line
2397 return *d_node
>= *t
.d_node
;
2399 CVC5_API_TRY_CATCH_END
;
2402 size_t Term::getNumChildren() const
2404 CVC5_API_TRY_CATCH_BEGIN
;
2405 CVC5_API_CHECK_NOT_NULL
;
2406 //////// all checks before this line
2408 // special case for apply kinds
2409 if (isApplyKind(d_node
->getKind()))
2411 return d_node
->getNumChildren() + 1;
2417 return d_node
->getNumChildren();
2419 CVC5_API_TRY_CATCH_END
;
2422 Term
Term::operator[](size_t index
) const
2424 CVC5_API_TRY_CATCH_BEGIN
;
2425 CVC5_API_CHECK_NOT_NULL
;
2426 CVC5_API_CHECK(index
< getNumChildren()) << "index out of bound";
2427 CVC5_API_CHECK(!isApplyKind(d_node
->getKind()) || d_node
->hasOperator())
2428 << "Expected apply kind to have operator when accessing child of Term";
2429 //////// all checks before this line
2431 // special cases for apply kinds
2432 if (isApplyKind(d_node
->getKind()))
2436 // return the operator
2437 return Term(d_solver
, d_node
->getOperator());
2444 // otherwise we are looking up child at (index-1)
2445 return Term(d_solver
, (*d_node
)[index
]);
2447 CVC5_API_TRY_CATCH_END
;
2450 uint64_t Term::getId() const
2452 CVC5_API_TRY_CATCH_BEGIN
;
2453 CVC5_API_CHECK_NOT_NULL
;
2454 //////// all checks before this line
2455 return d_node
->getId();
2457 CVC5_API_TRY_CATCH_END
;
2460 Kind
Term::getKind() const
2462 CVC5_API_TRY_CATCH_BEGIN
;
2463 CVC5_API_CHECK_NOT_NULL
;
2464 //////// all checks before this line
2465 return getKindHelper();
2467 CVC5_API_TRY_CATCH_END
;
2470 Sort
Term::getSort() const
2472 CVC5_API_TRY_CATCH_BEGIN
;
2473 CVC5_API_CHECK_NOT_NULL
;
2474 //////// all checks before this line
2475 return Sort(d_solver
, d_node
->getType());
2477 CVC5_API_TRY_CATCH_END
;
2480 Term
Term::substitute(const Term
& term
, const Term
& replacement
) const
2482 CVC5_API_TRY_CATCH_BEGIN
;
2483 CVC5_API_CHECK_NOT_NULL
;
2484 CVC5_API_CHECK_TERM(term
);
2485 CVC5_API_CHECK_TERM(replacement
);
2486 CVC5_API_CHECK(term
.getSort().isComparableTo(replacement
.getSort()))
2487 << "Expecting terms of comparable sort in substitute";
2488 //////// all checks before this line
2491 d_node
->substitute(TNode(*term
.d_node
), TNode(*replacement
.d_node
)));
2493 CVC5_API_TRY_CATCH_END
;
2496 Term
Term::substitute(const std::vector
<Term
>& terms
,
2497 const std::vector
<Term
>& replacements
) const
2499 CVC5_API_TRY_CATCH_BEGIN
;
2500 CVC5_API_CHECK_NOT_NULL
;
2501 CVC5_API_CHECK(terms
.size() == replacements
.size())
2502 << "Expecting vectors of the same arity in substitute";
2503 CVC5_API_TERM_CHECK_TERMS_WITH_TERMS_COMPARABLE_TO(terms
, replacements
);
2504 //////// all checks before this line
2505 std::vector
<Node
> nodes
= Term::termVectorToNodes(terms
);
2506 std::vector
<Node
> nodeReplacements
= Term::termVectorToNodes(replacements
);
2507 return Term(d_solver
,
2508 d_node
->substitute(nodes
.begin(),
2510 nodeReplacements
.begin(),
2511 nodeReplacements
.end()));
2513 CVC5_API_TRY_CATCH_END
;
2516 bool Term::hasOp() const
2518 CVC5_API_TRY_CATCH_BEGIN
;
2519 CVC5_API_CHECK_NOT_NULL
;
2520 //////// all checks before this line
2521 return d_node
->hasOperator();
2523 CVC5_API_TRY_CATCH_END
;
2526 Op
Term::getOp() const
2528 CVC5_API_TRY_CATCH_BEGIN
;
2529 CVC5_API_CHECK_NOT_NULL
;
2530 CVC5_API_CHECK(d_node
->hasOperator())
2531 << "Expecting Term to have an Op when calling getOp()";
2532 //////// all checks before this line
2534 // special cases for parameterized operators that are not indexed operators
2535 // the API level differs from the internal structure
2536 // indexed operators are stored in Ops
2537 // whereas functions and datatype operators are terms, and the Op
2538 // is one of the APPLY_* kinds
2539 if (isApplyKind(d_node
->getKind()))
2541 return Op(d_solver
, intToExtKind(d_node
->getKind()));
2543 else if (d_node
->getMetaKind() == kind::metakind::PARAMETERIZED
)
2545 // it's an indexed operator
2546 // so we should return the indexed op
2547 cvc5::Node op
= d_node
->getOperator();
2548 return Op(d_solver
, intToExtKind(d_node
->getKind()), op
);
2550 // Notice this is the only case where getKindHelper is used, since the
2551 // cases above do not have special cases for intToExtKind.
2552 return Op(d_solver
, getKindHelper());
2554 CVC5_API_TRY_CATCH_END
;
2557 bool Term::hasSymbol() const
2559 CVC5_API_TRY_CATCH_BEGIN
;
2560 CVC5_API_CHECK_NOT_NULL
;
2561 //////// all checks before this line
2562 return d_node
->hasAttribute(expr::VarNameAttr());
2564 CVC5_API_TRY_CATCH_END
;
2567 std::string
Term::getSymbol() const
2569 CVC5_API_TRY_CATCH_BEGIN
;
2570 CVC5_API_CHECK_NOT_NULL
;
2571 CVC5_API_CHECK(d_node
->hasAttribute(expr::VarNameAttr()))
2572 << "Invalid call to '" << __PRETTY_FUNCTION__
2573 << "', expected the term to have a symbol.";
2574 //////// all checks before this line
2575 return d_node
->getAttribute(expr::VarNameAttr());
2577 CVC5_API_TRY_CATCH_END
;
2580 bool Term::isNull() const
2582 CVC5_API_TRY_CATCH_BEGIN
;
2583 //////// all checks before this line
2584 return isNullHelper();
2586 CVC5_API_TRY_CATCH_END
;
2589 Term
Term::notTerm() const
2591 CVC5_API_TRY_CATCH_BEGIN
;
2592 CVC5_API_CHECK_NOT_NULL
;
2593 //////// all checks before this line
2594 Node res
= d_node
->notNode();
2595 (void)res
.getType(true); /* kick off type checking */
2596 return Term(d_solver
, res
);
2598 CVC5_API_TRY_CATCH_END
;
2601 Term
Term::andTerm(const Term
& t
) const
2603 CVC5_API_TRY_CATCH_BEGIN
;
2604 CVC5_API_CHECK_NOT_NULL
;
2605 CVC5_API_CHECK_TERM(t
);
2606 //////// all checks before this line
2607 Node res
= d_node
->andNode(*t
.d_node
);
2608 (void)res
.getType(true); /* kick off type checking */
2609 return Term(d_solver
, res
);
2611 CVC5_API_TRY_CATCH_END
;
2614 Term
Term::orTerm(const Term
& t
) const
2616 CVC5_API_TRY_CATCH_BEGIN
;
2617 CVC5_API_CHECK_NOT_NULL
;
2618 CVC5_API_CHECK_TERM(t
);
2619 //////// all checks before this line
2620 Node res
= d_node
->orNode(*t
.d_node
);
2621 (void)res
.getType(true); /* kick off type checking */
2622 return Term(d_solver
, res
);
2624 CVC5_API_TRY_CATCH_END
;
2627 Term
Term::xorTerm(const Term
& t
) const
2629 CVC5_API_TRY_CATCH_BEGIN
;
2630 CVC5_API_CHECK_NOT_NULL
;
2631 CVC5_API_CHECK_TERM(t
);
2632 //////// all checks before this line
2633 Node res
= d_node
->xorNode(*t
.d_node
);
2634 (void)res
.getType(true); /* kick off type checking */
2635 return Term(d_solver
, res
);
2637 CVC5_API_TRY_CATCH_END
;
2640 Term
Term::eqTerm(const Term
& t
) const
2642 CVC5_API_TRY_CATCH_BEGIN
;
2643 CVC5_API_CHECK_NOT_NULL
;
2644 CVC5_API_CHECK_TERM(t
);
2645 //////// all checks before this line
2646 Node res
= d_node
->eqNode(*t
.d_node
);
2647 (void)res
.getType(true); /* kick off type checking */
2648 return Term(d_solver
, res
);
2650 CVC5_API_TRY_CATCH_END
;
2653 Term
Term::impTerm(const Term
& t
) const
2655 CVC5_API_TRY_CATCH_BEGIN
;
2656 CVC5_API_CHECK_NOT_NULL
;
2657 CVC5_API_CHECK_TERM(t
);
2658 //////// all checks before this line
2659 Node res
= d_node
->impNode(*t
.d_node
);
2660 (void)res
.getType(true); /* kick off type checking */
2661 return Term(d_solver
, res
);
2663 CVC5_API_TRY_CATCH_END
;
2666 Term
Term::iteTerm(const Term
& then_t
, const Term
& else_t
) const
2668 CVC5_API_TRY_CATCH_BEGIN
;
2669 CVC5_API_CHECK_NOT_NULL
;
2670 CVC5_API_CHECK_TERM(then_t
);
2671 CVC5_API_CHECK_TERM(else_t
);
2672 //////// all checks before this line
2673 Node res
= d_node
->iteNode(*then_t
.d_node
, *else_t
.d_node
);
2674 (void)res
.getType(true); /* kick off type checking */
2675 return Term(d_solver
, res
);
2677 CVC5_API_TRY_CATCH_END
;
2680 std::string
Term::toString() const
2682 CVC5_API_TRY_CATCH_BEGIN
;
2683 //////// all checks before this line
2684 return d_node
->toString();
2686 CVC5_API_TRY_CATCH_END
;
2689 Term::const_iterator::const_iterator()
2690 : d_solver(nullptr), d_origNode(nullptr), d_pos(0)
2694 Term::const_iterator::const_iterator(const Solver
* slv
,
2695 const std::shared_ptr
<cvc5::Node
>& n
,
2697 : d_solver(slv
), d_origNode(n
), d_pos(p
)
2701 Term::const_iterator::const_iterator(const const_iterator
& it
)
2702 : d_solver(nullptr), d_origNode(nullptr)
2704 if (it
.d_origNode
!= nullptr)
2706 d_solver
= it
.d_solver
;
2707 d_origNode
= it
.d_origNode
;
2712 Term::const_iterator
& Term::const_iterator::operator=(const const_iterator
& it
)
2714 d_solver
= it
.d_solver
;
2715 d_origNode
= it
.d_origNode
;
2720 bool Term::const_iterator::operator==(const const_iterator
& it
) const
2722 if (d_origNode
== nullptr || it
.d_origNode
== nullptr)
2726 return (d_solver
== it
.d_solver
&& *d_origNode
== *it
.d_origNode
)
2727 && (d_pos
== it
.d_pos
);
2730 bool Term::const_iterator::operator!=(const const_iterator
& it
) const
2732 return !(*this == it
);
2735 Term::const_iterator
& Term::const_iterator::operator++()
2737 Assert(d_origNode
!= nullptr);
2742 Term::const_iterator
Term::const_iterator::operator++(int)
2744 Assert(d_origNode
!= nullptr);
2745 const_iterator it
= *this;
2750 Term
Term::const_iterator::operator*() const
2752 Assert(d_origNode
!= nullptr);
2753 // this term has an extra child (mismatch between API and internal structure)
2754 // the extra child will be the first child
2755 bool extra_child
= isApplyKind(d_origNode
->getKind());
2757 if (!d_pos
&& extra_child
)
2759 return Term(d_solver
, d_origNode
->getOperator());
2763 uint32_t idx
= d_pos
;
2770 return Term(d_solver
, (*d_origNode
)[idx
]);
2774 Term::const_iterator
Term::begin() const
2776 return Term::const_iterator(d_solver
, d_node
, 0);
2779 Term::const_iterator
Term::end() const
2781 int endpos
= d_node
->getNumChildren();
2782 // special cases for APPLY_*
2783 // the API differs from the internal structure
2784 // the API takes a "higher-order" perspective and the applied
2785 // function or datatype constructor/selector/tester is a Term
2786 // which means it needs to be one of the children, even though
2787 // internally it is not
2788 if (isApplyKind(d_node
->getKind()))
2790 // one more child if this is a UF application (count the UF as a child)
2793 return Term::const_iterator(d_solver
, d_node
, endpos
);
2796 const cvc5::Node
& Term::getNode(void) const { return *d_node
; }
2799 const Rational
& getRational(const cvc5::Node
& node
)
2801 switch (node
.getKind())
2803 case cvc5::Kind::CAST_TO_REAL
: return node
[0].getConst
<Rational
>();
2804 case cvc5::Kind::CONST_RATIONAL
: return node
.getConst
<Rational
>();
2806 CVC5_API_CHECK(false) << "Node is not a rational.";
2807 return node
.getConst
<Rational
>();
2810 Integer
getInteger(const cvc5::Node
& node
)
2812 return node
.getConst
<Rational
>().getNumerator();
2814 template <typename T
>
2815 bool checkIntegerBounds(const Integer
& i
)
2817 return i
>= std::numeric_limits
<T
>::min()
2818 && i
<= std::numeric_limits
<T
>::max();
2820 bool checkReal32Bounds(const Rational
& r
)
2822 return checkIntegerBounds
<std::int32_t>(r
.getNumerator())
2823 && checkIntegerBounds
<std::uint32_t>(r
.getDenominator());
2825 bool checkReal64Bounds(const Rational
& r
)
2827 return checkIntegerBounds
<std::int64_t>(r
.getNumerator())
2828 && checkIntegerBounds
<std::uint64_t>(r
.getDenominator());
2831 bool isReal(const Node
& node
)
2833 return node
.getKind() == cvc5::Kind::CONST_RATIONAL
2834 || node
.getKind() == cvc5::Kind::CAST_TO_REAL
;
2836 bool isReal32(const Node
& node
)
2838 return isReal(node
) && checkReal32Bounds(getRational(node
));
2840 bool isReal64(const Node
& node
)
2842 return isReal(node
) && checkReal64Bounds(getRational(node
));
2845 bool isInteger(const Node
& node
)
2847 return node
.getKind() == cvc5::Kind::CONST_RATIONAL
2848 && node
.getConst
<Rational
>().isIntegral();
2850 bool isInt32(const Node
& node
)
2852 return isInteger(node
) && checkIntegerBounds
<std::int32_t>(getInteger(node
));
2854 bool isUInt32(const Node
& node
)
2856 return isInteger(node
) && checkIntegerBounds
<std::uint32_t>(getInteger(node
));
2858 bool isInt64(const Node
& node
)
2860 return isInteger(node
) && checkIntegerBounds
<std::int64_t>(getInteger(node
));
2862 bool isUInt64(const Node
& node
)
2864 return isInteger(node
) && checkIntegerBounds
<std::uint64_t>(getInteger(node
));
2866 } // namespace detail
2868 int32_t Term::getRealOrIntegerValueSign() const
2870 CVC5_API_TRY_CATCH_BEGIN
;
2871 CVC5_API_CHECK_NOT_NULL
;
2872 //////// all checks before this line
2873 const Rational
& r
= detail::getRational(*d_node
);
2874 return static_cast<int32_t>(r
.sgn());
2876 CVC5_API_TRY_CATCH_END
;
2879 bool Term::isInt32Value() const
2881 CVC5_API_TRY_CATCH_BEGIN
;
2882 CVC5_API_CHECK_NOT_NULL
;
2883 //////// all checks before this line
2884 return detail::isInt32(*d_node
);
2886 CVC5_API_TRY_CATCH_END
;
2889 std::int32_t Term::getInt32Value() const
2891 CVC5_API_TRY_CATCH_BEGIN
;
2892 CVC5_API_CHECK_NOT_NULL
;
2893 CVC5_API_ARG_CHECK_EXPECTED(detail::isInt32(*d_node
), *d_node
)
2894 << "Term to be a 32-bit integer value when calling getInt32Value()";
2895 //////// all checks before this line
2896 return detail::getInteger(*d_node
).getSignedInt();
2898 CVC5_API_TRY_CATCH_END
;
2901 bool Term::isUInt32Value() const
2903 CVC5_API_TRY_CATCH_BEGIN
;
2904 CVC5_API_CHECK_NOT_NULL
;
2905 //////// all checks before this line
2906 return detail::isUInt32(*d_node
);
2908 CVC5_API_TRY_CATCH_END
;
2910 std::uint32_t Term::getUInt32Value() const
2912 CVC5_API_TRY_CATCH_BEGIN
;
2913 CVC5_API_CHECK_NOT_NULL
;
2914 CVC5_API_ARG_CHECK_EXPECTED(detail::isUInt32(*d_node
), *d_node
)
2915 << "Term to be a unsigned 32-bit integer value when calling "
2917 //////// all checks before this line
2918 return detail::getInteger(*d_node
).getUnsignedInt();
2920 CVC5_API_TRY_CATCH_END
;
2923 bool Term::isInt64Value() const
2925 CVC5_API_TRY_CATCH_BEGIN
;
2926 CVC5_API_CHECK_NOT_NULL
;
2927 //////// all checks before this line
2928 return detail::isInt64(*d_node
);
2930 CVC5_API_TRY_CATCH_END
;
2932 std::int64_t Term::getInt64Value() const
2934 CVC5_API_TRY_CATCH_BEGIN
;
2935 CVC5_API_CHECK_NOT_NULL
;
2936 CVC5_API_ARG_CHECK_EXPECTED(detail::isInt64(*d_node
), *d_node
)
2937 << "Term to be a 64-bit integer value when calling getInt64Value()";
2938 //////// all checks before this line
2939 return detail::getInteger(*d_node
).getSigned64();
2941 CVC5_API_TRY_CATCH_END
;
2944 bool Term::isUInt64Value() const
2946 CVC5_API_TRY_CATCH_BEGIN
;
2947 CVC5_API_CHECK_NOT_NULL
;
2948 //////// all checks before this line
2949 return detail::isUInt64(*d_node
);
2951 CVC5_API_TRY_CATCH_END
;
2954 std::uint64_t Term::getUInt64Value() const
2956 CVC5_API_TRY_CATCH_BEGIN
;
2957 CVC5_API_CHECK_NOT_NULL
;
2958 CVC5_API_ARG_CHECK_EXPECTED(detail::isUInt64(*d_node
), *d_node
)
2959 << "Term to be a unsigned 64-bit integer value when calling "
2961 //////// all checks before this line
2962 return detail::getInteger(*d_node
).getUnsigned64();
2964 CVC5_API_TRY_CATCH_END
;
2967 bool Term::isIntegerValue() const
2969 CVC5_API_TRY_CATCH_BEGIN
;
2970 CVC5_API_CHECK_NOT_NULL
;
2971 //////// all checks before this line
2972 return detail::isInteger(*d_node
);
2974 CVC5_API_TRY_CATCH_END
;
2976 std::string
Term::getIntegerValue() const
2978 CVC5_API_TRY_CATCH_BEGIN
;
2979 CVC5_API_CHECK_NOT_NULL
;
2980 CVC5_API_ARG_CHECK_EXPECTED(detail::isInteger(*d_node
), *d_node
)
2981 << "Term to be an integer value when calling getIntegerValue()";
2982 //////// all checks before this line
2983 return detail::getInteger(*d_node
).toString();
2985 CVC5_API_TRY_CATCH_END
;
2988 bool Term::isStringValue() const
2990 CVC5_API_TRY_CATCH_BEGIN
;
2991 CVC5_API_CHECK_NOT_NULL
;
2992 //////// all checks before this line
2993 return d_node
->getKind() == cvc5::Kind::CONST_STRING
;
2995 CVC5_API_TRY_CATCH_END
;
2998 std::wstring
Term::getStringValue() const
3000 CVC5_API_TRY_CATCH_BEGIN
;
3001 CVC5_API_CHECK_NOT_NULL
;
3002 CVC5_API_ARG_CHECK_EXPECTED(d_node
->getKind() == cvc5::Kind::CONST_STRING
,
3004 << "Term to be a string value when calling getStringValue()";
3005 //////// all checks before this line
3006 return d_node
->getConst
<cvc5::String
>().toWString();
3008 CVC5_API_TRY_CATCH_END
;
3011 std::vector
<Node
> Term::termVectorToNodes(const std::vector
<Term
>& terms
)
3013 std::vector
<Node
> res
;
3014 for (const Term
& t
: terms
)
3016 res
.push_back(t
.getNode());
3021 bool Term::isReal32Value() const
3023 CVC5_API_TRY_CATCH_BEGIN
;
3024 CVC5_API_CHECK_NOT_NULL
;
3025 //////// all checks before this line
3026 return detail::isReal32(*d_node
);
3028 CVC5_API_TRY_CATCH_END
;
3030 std::pair
<std::int32_t, std::uint32_t> Term::getReal32Value() const
3032 CVC5_API_TRY_CATCH_BEGIN
;
3033 CVC5_API_CHECK_NOT_NULL
;
3034 CVC5_API_ARG_CHECK_EXPECTED(detail::isReal32(*d_node
), *d_node
)
3035 << "Term to be a 32-bit rational value when calling getReal32Value()";
3036 //////// all checks before this line
3037 const Rational
& r
= detail::getRational(*d_node
);
3038 return std::make_pair(r
.getNumerator().getSignedInt(),
3039 r
.getDenominator().getUnsignedInt());
3041 CVC5_API_TRY_CATCH_END
;
3043 bool Term::isReal64Value() const
3045 CVC5_API_TRY_CATCH_BEGIN
;
3046 CVC5_API_CHECK_NOT_NULL
;
3047 //////// all checks before this line
3048 return detail::isReal64(*d_node
);
3050 CVC5_API_TRY_CATCH_END
;
3052 std::pair
<std::int64_t, std::uint64_t> Term::getReal64Value() const
3054 CVC5_API_TRY_CATCH_BEGIN
;
3055 CVC5_API_CHECK_NOT_NULL
;
3056 CVC5_API_ARG_CHECK_EXPECTED(detail::isReal64(*d_node
), *d_node
)
3057 << "Term to be a 64-bit rational value when calling getReal64Value()";
3058 //////// all checks before this line
3059 const Rational
& r
= detail::getRational(*d_node
);
3060 return std::make_pair(r
.getNumerator().getSigned64(),
3061 r
.getDenominator().getUnsigned64());
3063 CVC5_API_TRY_CATCH_END
;
3065 bool Term::isRealValue() const
3067 CVC5_API_TRY_CATCH_BEGIN
;
3068 CVC5_API_CHECK_NOT_NULL
;
3069 //////// all checks before this line
3070 return detail::isReal(*d_node
);
3072 CVC5_API_TRY_CATCH_END
;
3074 std::string
Term::getRealValue() const
3076 CVC5_API_TRY_CATCH_BEGIN
;
3077 CVC5_API_CHECK_NOT_NULL
;
3078 CVC5_API_ARG_CHECK_EXPECTED(detail::isReal(*d_node
), *d_node
)
3079 << "Term to be a rational value when calling getRealValue()";
3080 //////// all checks before this line
3081 const Rational
& rat
= detail::getRational(*d_node
);
3082 std::string res
= rat
.toString();
3083 if (rat
.isIntegral())
3089 CVC5_API_TRY_CATCH_END
;
3092 bool Term::isConstArray() const
3094 CVC5_API_TRY_CATCH_BEGIN
;
3095 CVC5_API_CHECK_NOT_NULL
;
3096 //////// all checks before this line
3097 return d_node
->getKind() == cvc5::Kind::STORE_ALL
;
3099 CVC5_API_TRY_CATCH_END
;
3101 Term
Term::getConstArrayBase() const
3103 CVC5_API_TRY_CATCH_BEGIN
;
3104 CVC5_API_CHECK_NOT_NULL
;
3105 CVC5_API_ARG_CHECK_EXPECTED(d_node
->getKind() == cvc5::Kind::STORE_ALL
,
3107 << "Term to be a constant array when calling getConstArrayBase()";
3108 //////// all checks before this line
3109 const auto& ar
= d_node
->getConst
<ArrayStoreAll
>();
3110 return Term(d_solver
, ar
.getValue());
3112 CVC5_API_TRY_CATCH_END
;
3115 bool Term::isBooleanValue() const
3117 CVC5_API_TRY_CATCH_BEGIN
;
3118 CVC5_API_CHECK_NOT_NULL
;
3119 //////// all checks before this line
3120 return d_node
->getKind() == cvc5::Kind::CONST_BOOLEAN
;
3122 CVC5_API_TRY_CATCH_END
;
3124 bool Term::getBooleanValue() const
3126 CVC5_API_TRY_CATCH_BEGIN
;
3127 CVC5_API_CHECK_NOT_NULL
;
3128 CVC5_API_ARG_CHECK_EXPECTED(d_node
->getKind() == cvc5::Kind::CONST_BOOLEAN
,
3130 << "Term to be a Boolean value when calling getBooleanValue()";
3131 //////// all checks before this line
3132 return d_node
->getConst
<bool>();
3134 CVC5_API_TRY_CATCH_END
;
3137 bool Term::isBitVectorValue() const
3139 CVC5_API_TRY_CATCH_BEGIN
;
3140 CVC5_API_CHECK_NOT_NULL
;
3141 //////// all checks before this line
3142 return d_node
->getKind() == cvc5::Kind::CONST_BITVECTOR
;
3144 CVC5_API_TRY_CATCH_END
;
3146 std::string
Term::getBitVectorValue(std::uint32_t base
) const
3148 CVC5_API_TRY_CATCH_BEGIN
;
3149 CVC5_API_CHECK_NOT_NULL
;
3150 CVC5_API_ARG_CHECK_EXPECTED(d_node
->getKind() == cvc5::Kind::CONST_BITVECTOR
,
3152 << "Term to be a bit-vector value when calling getBitVectorValue()";
3153 //////// all checks before this line
3154 return d_node
->getConst
<BitVector
>().toString(base
);
3156 CVC5_API_TRY_CATCH_END
;
3159 bool Term::isAbstractValue() const
3161 CVC5_API_TRY_CATCH_BEGIN
;
3162 CVC5_API_CHECK_NOT_NULL
;
3163 //////// all checks before this line
3164 return d_node
->getKind() == cvc5::Kind::ABSTRACT_VALUE
;
3166 CVC5_API_TRY_CATCH_END
;
3168 std::string
Term::getAbstractValue() const
3170 CVC5_API_TRY_CATCH_BEGIN
;
3171 CVC5_API_CHECK_NOT_NULL
;
3172 CVC5_API_ARG_CHECK_EXPECTED(d_node
->getKind() == cvc5::Kind::ABSTRACT_VALUE
,
3174 << "Term to be an abstract value when calling "
3175 "getAbstractValue()";
3176 //////// all checks before this line
3177 return d_node
->getConst
<AbstractValue
>().getIndex().toString();
3179 CVC5_API_TRY_CATCH_END
;
3182 bool Term::isTupleValue() const
3184 CVC5_API_TRY_CATCH_BEGIN
;
3185 CVC5_API_CHECK_NOT_NULL
;
3186 //////// all checks before this line
3187 return d_node
->getKind() == cvc5::Kind::APPLY_CONSTRUCTOR
&& d_node
->isConst()
3188 && d_node
->getType().getDType().isTuple();
3190 CVC5_API_TRY_CATCH_END
;
3192 std::vector
<Term
> Term::getTupleValue() const
3194 CVC5_API_TRY_CATCH_BEGIN
;
3195 CVC5_API_CHECK_NOT_NULL
;
3196 CVC5_API_ARG_CHECK_EXPECTED(d_node
->getKind() == cvc5::Kind::APPLY_CONSTRUCTOR
3197 && d_node
->isConst()
3198 && d_node
->getType().getDType().isTuple(),
3200 << "Term to be a tuple value when calling getTupleValue()";
3201 //////// all checks before this line
3202 std::vector
<Term
> res
;
3203 for (size_t i
= 0, n
= d_node
->getNumChildren(); i
< n
; ++i
)
3205 res
.emplace_back(Term(d_solver
, (*d_node
)[i
]));
3209 CVC5_API_TRY_CATCH_END
;
3212 bool Term::isFloatingPointPosZero() const
3214 CVC5_API_TRY_CATCH_BEGIN
;
3215 CVC5_API_CHECK_NOT_NULL
;
3216 //////// all checks before this line
3217 if (d_node
->getKind() == cvc5::Kind::CONST_FLOATINGPOINT
)
3219 const auto& fp
= d_node
->getConst
<FloatingPoint
>();
3220 return fp
.isZero() && fp
.isPositive();
3224 CVC5_API_TRY_CATCH_END
;
3226 bool Term::isFloatingPointNegZero() const
3228 CVC5_API_TRY_CATCH_BEGIN
;
3229 CVC5_API_CHECK_NOT_NULL
;
3230 //////// all checks before this line
3231 if (d_node
->getKind() == cvc5::Kind::CONST_FLOATINGPOINT
)
3233 const auto& fp
= d_node
->getConst
<FloatingPoint
>();
3234 return fp
.isZero() && fp
.isNegative();
3238 CVC5_API_TRY_CATCH_END
;
3240 bool Term::isFloatingPointPosInf() const
3242 CVC5_API_TRY_CATCH_BEGIN
;
3243 CVC5_API_CHECK_NOT_NULL
;
3244 //////// all checks before this line
3245 if (d_node
->getKind() == cvc5::Kind::CONST_FLOATINGPOINT
)
3247 const auto& fp
= d_node
->getConst
<FloatingPoint
>();
3248 return fp
.isInfinite() && fp
.isPositive();
3252 CVC5_API_TRY_CATCH_END
;
3254 bool Term::isFloatingPointNegInf() const
3256 CVC5_API_TRY_CATCH_BEGIN
;
3257 CVC5_API_CHECK_NOT_NULL
;
3258 //////// all checks before this line
3259 if (d_node
->getKind() == cvc5::Kind::CONST_FLOATINGPOINT
)
3261 const auto& fp
= d_node
->getConst
<FloatingPoint
>();
3262 return fp
.isInfinite() && fp
.isNegative();
3266 CVC5_API_TRY_CATCH_END
;
3268 bool Term::isFloatingPointNaN() const
3270 CVC5_API_TRY_CATCH_BEGIN
;
3271 CVC5_API_CHECK_NOT_NULL
;
3272 //////// all checks before this line
3273 return d_node
->getKind() == cvc5::Kind::CONST_FLOATINGPOINT
3274 && d_node
->getConst
<FloatingPoint
>().isNaN();
3276 CVC5_API_TRY_CATCH_END
;
3278 bool Term::isFloatingPointValue() const
3280 CVC5_API_TRY_CATCH_BEGIN
;
3281 CVC5_API_CHECK_NOT_NULL
;
3282 //////// all checks before this line
3283 return d_node
->getKind() == cvc5::Kind::CONST_FLOATINGPOINT
;
3285 CVC5_API_TRY_CATCH_END
;
3287 std::tuple
<std::uint32_t, std::uint32_t, Term
> Term::getFloatingPointValue()
3290 CVC5_API_TRY_CATCH_BEGIN
;
3291 CVC5_API_CHECK_NOT_NULL
;
3292 CVC5_API_ARG_CHECK_EXPECTED(
3293 d_node
->getKind() == cvc5::Kind::CONST_FLOATINGPOINT
, *d_node
)
3294 << "Term to be a floating-point value when calling "
3295 "getFloatingPointValue()";
3296 //////// all checks before this line
3297 const auto& fp
= d_node
->getConst
<FloatingPoint
>();
3298 return std::make_tuple(fp
.getSize().exponentWidth(),
3299 fp
.getSize().significandWidth(),
3300 d_solver
->mkValHelper
<BitVector
>(fp
.pack()));
3302 CVC5_API_TRY_CATCH_END
;
3305 bool Term::isSetValue() const
3307 CVC5_API_TRY_CATCH_BEGIN
;
3308 CVC5_API_CHECK_NOT_NULL
;
3309 //////// all checks before this line
3310 return d_node
->getType().isSet() && d_node
->isConst();
3312 CVC5_API_TRY_CATCH_END
;
3315 void Term::collectSet(std::set
<Term
>& set
,
3316 const cvc5::Node
& node
,
3319 // We asserted that node has a set type, and node.isConst()
3320 // Thus, node only contains of SET_EMPTY, SET_UNION and SET_SINGLETON.
3321 switch (node
.getKind())
3323 case cvc5::Kind::SET_EMPTY
: break;
3324 case cvc5::Kind::SET_SINGLETON
: set
.emplace(Term(slv
, node
[0])); break;
3325 case cvc5::Kind::SET_UNION
:
3327 for (const auto& sub
: node
)
3329 collectSet(set
, sub
, slv
);
3334 CVC5_API_ARG_CHECK_EXPECTED(false, node
)
3335 << "Term to be a set value when calling getSetValue()";
3340 std::set
<Term
> Term::getSetValue() const
3342 CVC5_API_TRY_CATCH_BEGIN
;
3343 CVC5_API_CHECK_NOT_NULL
;
3344 CVC5_API_ARG_CHECK_EXPECTED(d_node
->getType().isSet() && d_node
->isConst(),
3346 << "Term to be a set value when calling getSetValue()";
3347 //////// all checks before this line
3349 Term::collectSet(res
, *d_node
, d_solver
);
3352 CVC5_API_TRY_CATCH_END
;
3355 bool Term::isSequenceValue() const
3357 CVC5_API_TRY_CATCH_BEGIN
;
3358 CVC5_API_CHECK_NOT_NULL
;
3359 //////// all checks before this line
3360 return d_node
->getKind() == cvc5::Kind::CONST_SEQUENCE
;
3362 CVC5_API_TRY_CATCH_END
;
3364 std::vector
<Term
> Term::getSequenceValue() const
3366 CVC5_API_TRY_CATCH_BEGIN
;
3367 CVC5_API_CHECK_NOT_NULL
;
3368 CVC5_API_ARG_CHECK_EXPECTED(d_node
->getKind() == cvc5::Kind::CONST_SEQUENCE
,
3370 << "Term to be a sequence value when calling getSequenceValue()";
3371 //////// all checks before this line
3372 std::vector
<Term
> res
;
3373 const Sequence
& seq
= d_node
->getConst
<Sequence
>();
3374 for (const auto& node
: seq
.getVec())
3376 res
.emplace_back(Term(d_solver
, node
));
3380 CVC5_API_TRY_CATCH_END
;
3383 bool Term::isUninterpretedValue() const
3385 CVC5_API_TRY_CATCH_BEGIN
;
3386 CVC5_API_CHECK_NOT_NULL
;
3387 //////// all checks before this line
3388 return d_node
->getKind() == cvc5::Kind::UNINTERPRETED_CONSTANT
;
3390 CVC5_API_TRY_CATCH_END
;
3392 std::pair
<Sort
, std::int32_t> Term::getUninterpretedValue() const
3394 CVC5_API_TRY_CATCH_BEGIN
;
3395 CVC5_API_CHECK_NOT_NULL
;
3396 CVC5_API_ARG_CHECK_EXPECTED(
3397 d_node
->getKind() == cvc5::Kind::UNINTERPRETED_CONSTANT
, *d_node
)
3398 << "Term to be an uninterpreted value when calling "
3399 "getUninterpretedValue()";
3400 //////// all checks before this line
3401 const auto& uc
= d_node
->getConst
<UninterpretedConstant
>();
3402 return std::make_pair(Sort(d_solver
, uc
.getType()),
3403 uc
.getIndex().toUnsignedInt());
3405 CVC5_API_TRY_CATCH_END
;
3408 std::ostream
& operator<<(std::ostream
& out
, const Term
& t
)
3410 out
<< t
.toString();
3414 std::ostream
& operator<<(std::ostream
& out
, const std::vector
<Term
>& vector
)
3416 container_to_stream(out
, vector
);
3420 std::ostream
& operator<<(std::ostream
& out
, const std::set
<Term
>& set
)
3422 container_to_stream(out
, set
);
3426 std::ostream
& operator<<(std::ostream
& out
,
3427 const std::unordered_set
<Term
>& unordered_set
)
3429 container_to_stream(out
, unordered_set
);
3433 template <typename V
>
3434 std::ostream
& operator<<(std::ostream
& out
, const std::map
<Term
, V
>& map
)
3436 container_to_stream(out
, map
);
3440 template <typename V
>
3441 std::ostream
& operator<<(std::ostream
& out
,
3442 const std::unordered_map
<Term
, V
>& unordered_map
)
3444 container_to_stream(out
, unordered_map
);
3449 /* -------------------------------------------------------------------------- */
3451 /* Split out to avoid nested API calls (problematic with API tracing). */
3452 /* .......................................................................... */
3454 bool Term::isNullHelper() const
3456 /* Split out to avoid nested API calls (problematic with API tracing). */
3457 return d_node
->isNull();
3460 Kind
Term::getKindHelper() const
3462 /* Sequence kinds do not exist internally, so we must convert their internal
3463 * (string) versions back to sequence. All operators where this is
3464 * necessary are such that their first child is of sequence type, which
3466 if (d_node
->getNumChildren() > 0 && (*d_node
)[0].getType().isSequence())
3468 switch (d_node
->getKind())
3470 case cvc5::Kind::STRING_CONCAT
: return SEQ_CONCAT
;
3471 case cvc5::Kind::STRING_LENGTH
: return SEQ_LENGTH
;
3472 case cvc5::Kind::STRING_SUBSTR
: return SEQ_EXTRACT
;
3473 case cvc5::Kind::STRING_UPDATE
: return SEQ_UPDATE
;
3474 case cvc5::Kind::STRING_CHARAT
: return SEQ_AT
;
3475 case cvc5::Kind::STRING_CONTAINS
: return SEQ_CONTAINS
;
3476 case cvc5::Kind::STRING_INDEXOF
: return SEQ_INDEXOF
;
3477 case cvc5::Kind::STRING_REPLACE
: return SEQ_REPLACE
;
3478 case cvc5::Kind::STRING_REPLACE_ALL
: return SEQ_REPLACE_ALL
;
3479 case cvc5::Kind::STRING_REV
: return SEQ_REV
;
3480 case cvc5::Kind::STRING_PREFIX
: return SEQ_PREFIX
;
3481 case cvc5::Kind::STRING_SUFFIX
: return SEQ_SUFFIX
;
3483 // fall through to conversion below
3487 // Notice that kinds like APPLY_TYPE_ASCRIPTION will be converted to
3491 return CONST_RATIONAL
;
3493 return intToExtKind(d_node
->getKind());
3496 bool Term::isCastedReal() const
3498 if (d_node
->getKind() == kind::CAST_TO_REAL
)
3500 return (*d_node
)[0].isConst() && (*d_node
)[0].getType().isInteger();
3505 /* -------------------------------------------------------------------------- */
3507 /* -------------------------------------------------------------------------- */
3509 /* DatatypeConstructorDecl -------------------------------------------------- */
3511 DatatypeConstructorDecl::DatatypeConstructorDecl()
3512 : d_solver(nullptr), d_ctor(nullptr)
3516 DatatypeConstructorDecl::DatatypeConstructorDecl(const Solver
* slv
,
3517 const std::string
& name
)
3518 : d_solver(slv
), d_ctor(new cvc5::DTypeConstructor(name
))
3521 DatatypeConstructorDecl::~DatatypeConstructorDecl()
3523 if (d_ctor
!= nullptr)
3529 void DatatypeConstructorDecl::addSelector(const std::string
& name
,
3532 CVC5_API_TRY_CATCH_BEGIN
;
3533 CVC5_API_CHECK_NOT_NULL
;
3534 CVC5_API_CHECK_SORT(sort
);
3535 CVC5_API_ARG_CHECK_EXPECTED(!sort
.isNull(), sort
)
3536 << "non-null codomain sort for selector";
3537 //////// all checks before this line
3538 d_ctor
->addArg(name
, *sort
.d_type
);
3540 CVC5_API_TRY_CATCH_END
;
3543 void DatatypeConstructorDecl::addSelectorSelf(const std::string
& name
)
3545 CVC5_API_TRY_CATCH_BEGIN
;
3546 CVC5_API_CHECK_NOT_NULL
;
3547 //////// all checks before this line
3548 d_ctor
->addArgSelf(name
);
3550 CVC5_API_TRY_CATCH_END
;
3553 bool DatatypeConstructorDecl::isNull() const
3555 CVC5_API_TRY_CATCH_BEGIN
;
3556 //////// all checks before this line
3557 return isNullHelper();
3559 CVC5_API_TRY_CATCH_END
;
3562 std::string
DatatypeConstructorDecl::toString() const
3564 CVC5_API_TRY_CATCH_BEGIN
;
3565 //////// all checks before this line
3566 std::stringstream ss
;
3570 CVC5_API_TRY_CATCH_END
;
3573 std::ostream
& operator<<(std::ostream
& out
,
3574 const DatatypeConstructorDecl
& ctordecl
)
3576 out
<< ctordecl
.toString();
3580 std::ostream
& operator<<(std::ostream
& out
,
3581 const std::vector
<DatatypeConstructorDecl
>& vector
)
3583 container_to_stream(out
, vector
);
3587 bool DatatypeConstructorDecl::isNullHelper() const { return d_ctor
== nullptr; }
3589 bool DatatypeConstructorDecl::isResolved() const
3591 return d_ctor
== nullptr || d_ctor
->isResolved();
3594 /* DatatypeDecl ------------------------------------------------------------- */
3596 DatatypeDecl::DatatypeDecl() : d_solver(nullptr), d_dtype(nullptr) {}
3598 DatatypeDecl::DatatypeDecl(const Solver
* slv
,
3599 const std::string
& name
,
3601 : d_solver(slv
), d_dtype(new cvc5::DType(name
, isCoDatatype
))
3605 DatatypeDecl::DatatypeDecl(const Solver
* slv
,
3606 const std::string
& name
,
3610 d_dtype(new cvc5::DType(
3611 name
, std::vector
<TypeNode
>{*param
.d_type
}, isCoDatatype
))
3615 DatatypeDecl::DatatypeDecl(const Solver
* slv
,
3616 const std::string
& name
,
3617 const std::vector
<Sort
>& params
,
3621 std::vector
<TypeNode
> tparams
= Sort::sortVectorToTypeNodes(params
);
3622 d_dtype
= std::shared_ptr
<cvc5::DType
>(
3623 new cvc5::DType(name
, tparams
, isCoDatatype
));
3626 bool DatatypeDecl::isNullHelper() const { return !d_dtype
; }
3628 DatatypeDecl::~DatatypeDecl()
3630 if (d_dtype
!= nullptr)
3636 void DatatypeDecl::addConstructor(const DatatypeConstructorDecl
& ctor
)
3638 CVC5_API_TRY_CATCH_BEGIN
;
3639 CVC5_API_CHECK_NOT_NULL
;
3640 CVC5_API_ARG_CHECK_NOT_NULL(ctor
);
3641 CVC5_API_ARG_CHECK_SOLVER("datatype constructor declaration", ctor
);
3642 //////// all checks before this line
3643 d_dtype
->addConstructor(ctor
.d_ctor
);
3645 CVC5_API_TRY_CATCH_END
;
3648 size_t DatatypeDecl::getNumConstructors() const
3650 CVC5_API_TRY_CATCH_BEGIN
;
3651 CVC5_API_CHECK_NOT_NULL
;
3652 //////// all checks before this line
3653 return d_dtype
->getNumConstructors();
3655 CVC5_API_TRY_CATCH_END
;
3658 bool DatatypeDecl::isParametric() const
3660 CVC5_API_TRY_CATCH_BEGIN
;
3661 CVC5_API_CHECK_NOT_NULL
;
3662 //////// all checks before this line
3663 return d_dtype
->isParametric();
3665 CVC5_API_TRY_CATCH_END
;
3668 std::string
DatatypeDecl::toString() const
3670 CVC5_API_TRY_CATCH_BEGIN
;
3671 CVC5_API_CHECK_NOT_NULL
;
3672 //////// all checks before this line
3673 std::stringstream ss
;
3677 CVC5_API_TRY_CATCH_END
;
3680 std::string
DatatypeDecl::getName() const
3682 CVC5_API_TRY_CATCH_BEGIN
;
3683 CVC5_API_CHECK_NOT_NULL
;
3684 //////// all checks before this line
3685 return d_dtype
->getName();
3687 CVC5_API_TRY_CATCH_END
;
3690 bool DatatypeDecl::isNull() const
3692 CVC5_API_TRY_CATCH_BEGIN
;
3693 //////// all checks before this line
3694 return isNullHelper();
3696 CVC5_API_TRY_CATCH_END
;
3699 std::ostream
& operator<<(std::ostream
& out
, const DatatypeDecl
& dtdecl
)
3701 out
<< dtdecl
.toString();
3705 cvc5::DType
& DatatypeDecl::getDatatype(void) const { return *d_dtype
; }
3707 /* DatatypeSelector --------------------------------------------------------- */
3709 DatatypeSelector::DatatypeSelector() : d_solver(nullptr), d_stor(nullptr) {}
3711 DatatypeSelector::DatatypeSelector(const Solver
* slv
,
3712 const cvc5::DTypeSelector
& stor
)
3713 : d_solver(slv
), d_stor(new cvc5::DTypeSelector(stor
))
3715 CVC5_API_CHECK(d_stor
->isResolved()) << "Expected resolved datatype selector";
3718 DatatypeSelector::~DatatypeSelector()
3720 if (d_stor
!= nullptr)
3726 std::string
DatatypeSelector::getName() const
3728 CVC5_API_TRY_CATCH_BEGIN
;
3729 CVC5_API_CHECK_NOT_NULL
;
3730 //////// all checks before this line
3731 return d_stor
->getName();
3733 CVC5_API_TRY_CATCH_END
;
3736 Term
DatatypeSelector::getSelectorTerm() const
3738 CVC5_API_TRY_CATCH_BEGIN
;
3739 CVC5_API_CHECK_NOT_NULL
;
3740 //////// all checks before this line
3741 return Term(d_solver
, d_stor
->getSelector());
3743 CVC5_API_TRY_CATCH_END
;
3745 Term
DatatypeSelector::getUpdaterTerm() const
3747 CVC5_API_TRY_CATCH_BEGIN
;
3748 CVC5_API_CHECK_NOT_NULL
;
3749 //////// all checks before this line
3750 return Term(d_solver
, d_stor
->getUpdater());
3752 CVC5_API_TRY_CATCH_END
;
3755 Sort
DatatypeSelector::getCodomainSort() const
3757 CVC5_API_TRY_CATCH_BEGIN
;
3758 CVC5_API_CHECK_NOT_NULL
;
3759 //////// all checks before this line
3760 return Sort(d_solver
, d_stor
->getRangeType());
3762 CVC5_API_TRY_CATCH_END
;
3765 bool DatatypeSelector::isNull() const
3767 CVC5_API_TRY_CATCH_BEGIN
;
3768 //////// all checks before this line
3769 return isNullHelper();
3771 CVC5_API_TRY_CATCH_END
;
3774 std::string
DatatypeSelector::toString() const
3776 CVC5_API_TRY_CATCH_BEGIN
;
3777 //////// all checks before this line
3778 std::stringstream ss
;
3782 CVC5_API_TRY_CATCH_END
;
3785 std::ostream
& operator<<(std::ostream
& out
, const DatatypeSelector
& stor
)
3787 out
<< stor
.toString();
3791 bool DatatypeSelector::isNullHelper() const { return d_stor
== nullptr; }
3793 /* DatatypeConstructor ------------------------------------------------------ */
3795 DatatypeConstructor::DatatypeConstructor() : d_solver(nullptr), d_ctor(nullptr)
3799 DatatypeConstructor::DatatypeConstructor(const Solver
* slv
,
3800 const cvc5::DTypeConstructor
& ctor
)
3801 : d_solver(slv
), d_ctor(new cvc5::DTypeConstructor(ctor
))
3803 CVC5_API_CHECK(d_ctor
->isResolved())
3804 << "Expected resolved datatype constructor";
3807 DatatypeConstructor::~DatatypeConstructor()
3809 if (d_ctor
!= nullptr)
3815 std::string
DatatypeConstructor::getName() const
3817 CVC5_API_TRY_CATCH_BEGIN
;
3818 CVC5_API_CHECK_NOT_NULL
;
3819 //////// all checks before this line
3820 return d_ctor
->getName();
3822 CVC5_API_TRY_CATCH_END
;
3825 Term
DatatypeConstructor::getConstructorTerm() const
3827 CVC5_API_TRY_CATCH_BEGIN
;
3828 CVC5_API_CHECK_NOT_NULL
;
3829 //////// all checks before this line
3830 return Term(d_solver
, d_ctor
->getConstructor());
3832 CVC5_API_TRY_CATCH_END
;
3835 Term
DatatypeConstructor::getInstantiatedConstructorTerm(
3836 const Sort
& retSort
) const
3838 CVC5_API_TRY_CATCH_BEGIN
;
3839 CVC5_API_CHECK_NOT_NULL
;
3840 CVC5_API_CHECK(d_ctor
->isResolved())
3841 << "Expected resolved datatype constructor";
3842 CVC5_API_CHECK(retSort
.isDatatype())
3843 << "Cannot get specialized constructor type for non-datatype type "
3845 //////// all checks before this line
3846 Node ret
= d_ctor
->getInstantiatedConstructor(*retSort
.d_type
);
3847 (void)ret
.getType(true); /* kick off type checking */
3848 // apply type ascription to the operator
3849 Term sctor
= api::Term(d_solver
, ret
);
3852 CVC5_API_TRY_CATCH_END
;
3855 Term
DatatypeConstructor::getTesterTerm() const
3857 CVC5_API_TRY_CATCH_BEGIN
;
3858 CVC5_API_CHECK_NOT_NULL
;
3859 //////// all checks before this line
3860 return Term(d_solver
, d_ctor
->getTester());
3862 CVC5_API_TRY_CATCH_END
;
3865 size_t DatatypeConstructor::getNumSelectors() const
3867 CVC5_API_TRY_CATCH_BEGIN
;
3868 CVC5_API_CHECK_NOT_NULL
;
3869 //////// all checks before this line
3870 return d_ctor
->getNumArgs();
3872 CVC5_API_TRY_CATCH_END
;
3875 DatatypeSelector
DatatypeConstructor::operator[](size_t index
) const
3877 CVC5_API_TRY_CATCH_BEGIN
;
3878 CVC5_API_CHECK_NOT_NULL
;
3879 //////// all checks before this line
3880 return DatatypeSelector(d_solver
, (*d_ctor
)[index
]);
3882 CVC5_API_TRY_CATCH_END
;
3885 DatatypeSelector
DatatypeConstructor::operator[](const std::string
& name
) const
3887 CVC5_API_TRY_CATCH_BEGIN
;
3888 CVC5_API_CHECK_NOT_NULL
;
3889 //////// all checks before this line
3890 return getSelectorForName(name
);
3892 CVC5_API_TRY_CATCH_END
;
3895 DatatypeSelector
DatatypeConstructor::getSelector(const std::string
& name
) const
3897 CVC5_API_TRY_CATCH_BEGIN
;
3898 CVC5_API_CHECK_NOT_NULL
;
3899 //////// all checks before this line
3900 return getSelectorForName(name
);
3902 CVC5_API_TRY_CATCH_END
;
3905 Term
DatatypeConstructor::getSelectorTerm(const std::string
& name
) const
3907 CVC5_API_TRY_CATCH_BEGIN
;
3908 CVC5_API_CHECK_NOT_NULL
;
3909 //////// all checks before this line
3910 return getSelector(name
).getSelectorTerm();
3912 CVC5_API_TRY_CATCH_END
;
3915 DatatypeConstructor::const_iterator
DatatypeConstructor::begin() const
3917 return DatatypeConstructor::const_iterator(d_solver
, *d_ctor
, true);
3920 DatatypeConstructor::const_iterator
DatatypeConstructor::end() const
3922 return DatatypeConstructor::const_iterator(d_solver
, *d_ctor
, false);
3925 DatatypeConstructor::const_iterator::const_iterator(
3926 const Solver
* slv
, const cvc5::DTypeConstructor
& ctor
, bool begin
)
3929 d_int_stors
= &ctor
.getArgs();
3931 const std::vector
<std::shared_ptr
<cvc5::DTypeSelector
>>& sels
=
3933 for (const std::shared_ptr
<cvc5::DTypeSelector
>& s
: sels
)
3935 /* Can not use emplace_back here since constructor is private. */
3936 d_stors
.push_back(DatatypeSelector(d_solver
, *s
.get()));
3938 d_idx
= begin
? 0 : sels
.size();
3941 DatatypeConstructor::const_iterator::const_iterator()
3942 : d_solver(nullptr), d_int_stors(nullptr), d_idx(0)
3946 DatatypeConstructor::const_iterator
&
3947 DatatypeConstructor::const_iterator::operator=(
3948 const DatatypeConstructor::const_iterator
& it
)
3950 d_solver
= it
.d_solver
;
3951 d_int_stors
= it
.d_int_stors
;
3952 d_stors
= it
.d_stors
;
3957 const DatatypeSelector
& DatatypeConstructor::const_iterator::operator*() const
3959 return d_stors
[d_idx
];
3962 const DatatypeSelector
* DatatypeConstructor::const_iterator::operator->() const
3964 return &d_stors
[d_idx
];
3967 DatatypeConstructor::const_iterator
&
3968 DatatypeConstructor::const_iterator::operator++()
3974 DatatypeConstructor::const_iterator
3975 DatatypeConstructor::const_iterator::operator++(int)
3977 DatatypeConstructor::const_iterator
it(*this);
3982 bool DatatypeConstructor::const_iterator::operator==(
3983 const DatatypeConstructor::const_iterator
& other
) const
3985 return d_int_stors
== other
.d_int_stors
&& d_idx
== other
.d_idx
;
3988 bool DatatypeConstructor::const_iterator::operator!=(
3989 const DatatypeConstructor::const_iterator
& other
) const
3991 return d_int_stors
!= other
.d_int_stors
|| d_idx
!= other
.d_idx
;
3994 bool DatatypeConstructor::isNull() const
3996 CVC5_API_TRY_CATCH_BEGIN
;
3997 //////// all checks before this line
3998 return isNullHelper();
4000 CVC5_API_TRY_CATCH_END
;
4003 std::string
DatatypeConstructor::toString() const
4005 CVC5_API_TRY_CATCH_BEGIN
;
4006 //////// all checks before this line
4007 std::stringstream ss
;
4011 CVC5_API_TRY_CATCH_END
;
4014 bool DatatypeConstructor::isNullHelper() const { return d_ctor
== nullptr; }
4016 DatatypeSelector
DatatypeConstructor::getSelectorForName(
4017 const std::string
& name
) const
4019 bool foundSel
= false;
4021 for (size_t i
= 0, nsels
= getNumSelectors(); i
< nsels
; i
++)
4023 if ((*d_ctor
)[i
].getName() == name
)
4032 std::stringstream snames
;
4034 for (size_t i
= 0, ncons
= getNumSelectors(); i
< ncons
; i
++)
4036 snames
<< (*d_ctor
)[i
].getName() << " ";
4039 CVC5_API_CHECK(foundSel
) << "No selector " << name
<< " for constructor "
4040 << getName() << " exists among " << snames
.str();
4042 return DatatypeSelector(d_solver
, (*d_ctor
)[index
]);
4045 std::ostream
& operator<<(std::ostream
& out
, const DatatypeConstructor
& ctor
)
4047 out
<< ctor
.toString();
4051 /* Datatype ----------------------------------------------------------------- */
4053 Datatype::Datatype(const Solver
* slv
, const cvc5::DType
& dtype
)
4054 : d_solver(slv
), d_dtype(new cvc5::DType(dtype
))
4056 CVC5_API_CHECK(d_dtype
->isResolved()) << "Expected resolved datatype";
4059 Datatype::Datatype() : d_solver(nullptr), d_dtype(nullptr) {}
4061 Datatype::~Datatype()
4063 if (d_dtype
!= nullptr)
4069 DatatypeConstructor
Datatype::operator[](size_t idx
) const
4071 CVC5_API_TRY_CATCH_BEGIN
;
4072 CVC5_API_CHECK_NOT_NULL
;
4073 CVC5_API_CHECK(idx
< getNumConstructors()) << "Index out of bounds.";
4074 //////// all checks before this line
4075 return DatatypeConstructor(d_solver
, (*d_dtype
)[idx
]);
4077 CVC5_API_TRY_CATCH_END
;
4080 DatatypeConstructor
Datatype::operator[](const std::string
& name
) const
4082 CVC5_API_TRY_CATCH_BEGIN
;
4083 CVC5_API_CHECK_NOT_NULL
;
4084 //////// all checks before this line
4085 return getConstructorForName(name
);
4087 CVC5_API_TRY_CATCH_END
;
4090 DatatypeConstructor
Datatype::getConstructor(const std::string
& name
) const
4092 CVC5_API_TRY_CATCH_BEGIN
;
4093 CVC5_API_CHECK_NOT_NULL
;
4094 //////// all checks before this line
4095 return getConstructorForName(name
);
4097 CVC5_API_TRY_CATCH_END
;
4100 Term
Datatype::getConstructorTerm(const std::string
& name
) const
4102 CVC5_API_TRY_CATCH_BEGIN
;
4103 CVC5_API_CHECK_NOT_NULL
;
4104 //////// all checks before this line
4105 return getConstructorForName(name
).getConstructorTerm();
4107 CVC5_API_TRY_CATCH_END
;
4110 DatatypeSelector
Datatype::getSelector(const std::string
& name
) const
4112 CVC5_API_TRY_CATCH_BEGIN
;
4113 CVC5_API_CHECK_NOT_NULL
;
4114 //////// all checks before this line
4115 return getSelectorForName(name
);
4117 CVC5_API_TRY_CATCH_END
;
4120 std::string
Datatype::getName() const
4122 CVC5_API_TRY_CATCH_BEGIN
;
4123 CVC5_API_CHECK_NOT_NULL
;
4124 //////// all checks before this line
4125 return d_dtype
->getName();
4127 CVC5_API_TRY_CATCH_END
;
4130 size_t Datatype::getNumConstructors() const
4132 CVC5_API_TRY_CATCH_BEGIN
;
4133 CVC5_API_CHECK_NOT_NULL
;
4134 //////// all checks before this line
4135 return d_dtype
->getNumConstructors();
4137 CVC5_API_TRY_CATCH_END
;
4140 std::vector
<Sort
> Datatype::getParameters() const
4142 CVC5_API_TRY_CATCH_BEGIN
;
4143 CVC5_API_CHECK_NOT_NULL
;
4144 CVC5_API_CHECK(isParametric()) << "Expected parametric datatype";
4145 //////// all checks before this line
4146 std::vector
<cvc5::TypeNode
> params
= d_dtype
->getParameters();
4147 return Sort::typeNodeVectorToSorts(d_solver
, params
);
4149 CVC5_API_TRY_CATCH_END
;
4152 bool Datatype::isParametric() const
4154 CVC5_API_TRY_CATCH_BEGIN
;
4155 CVC5_API_CHECK_NOT_NULL
;
4156 //////// all checks before this line
4157 return d_dtype
->isParametric();
4159 CVC5_API_TRY_CATCH_END
;
4162 bool Datatype::isCodatatype() const
4164 CVC5_API_TRY_CATCH_BEGIN
;
4165 CVC5_API_CHECK_NOT_NULL
;
4166 //////// all checks before this line
4167 return d_dtype
->isCodatatype();
4169 CVC5_API_TRY_CATCH_END
;
4172 bool Datatype::isTuple() const
4174 CVC5_API_TRY_CATCH_BEGIN
;
4175 CVC5_API_CHECK_NOT_NULL
;
4176 //////// all checks before this line
4177 return d_dtype
->isTuple();
4179 CVC5_API_TRY_CATCH_END
;
4182 bool Datatype::isRecord() const
4184 CVC5_API_TRY_CATCH_BEGIN
;
4185 CVC5_API_CHECK_NOT_NULL
;
4186 //////// all checks before this line
4187 return d_dtype
->isRecord();
4189 CVC5_API_TRY_CATCH_END
;
4192 bool Datatype::isFinite() const
4194 CVC5_API_TRY_CATCH_BEGIN
;
4195 CVC5_API_CHECK_NOT_NULL
;
4196 //////// all checks before this line
4197 // we assume that finite model finding is disabled by passing false as the
4199 return isCardinalityClassFinite(d_dtype
->getCardinalityClass(), false);
4201 CVC5_API_TRY_CATCH_END
;
4204 bool Datatype::isWellFounded() const
4206 CVC5_API_TRY_CATCH_BEGIN
;
4207 CVC5_API_CHECK_NOT_NULL
;
4208 //////// all checks before this line
4209 return d_dtype
->isWellFounded();
4211 CVC5_API_TRY_CATCH_END
;
4213 bool Datatype::hasNestedRecursion() const
4215 CVC5_API_TRY_CATCH_BEGIN
;
4216 CVC5_API_CHECK_NOT_NULL
;
4217 //////// all checks before this line
4218 return d_dtype
->hasNestedRecursion();
4220 CVC5_API_TRY_CATCH_END
;
4223 bool Datatype::isNull() const
4225 CVC5_API_TRY_CATCH_BEGIN
;
4226 //////// all checks before this line
4227 return isNullHelper();
4229 CVC5_API_TRY_CATCH_END
;
4232 std::string
Datatype::toString() const
4234 CVC5_API_TRY_CATCH_BEGIN
;
4235 CVC5_API_CHECK_NOT_NULL
;
4236 //////// all checks before this line
4237 return d_dtype
->getName();
4239 CVC5_API_TRY_CATCH_END
;
4242 Datatype::const_iterator
Datatype::begin() const
4244 return Datatype::const_iterator(d_solver
, *d_dtype
, true);
4247 Datatype::const_iterator
Datatype::end() const
4249 return Datatype::const_iterator(d_solver
, *d_dtype
, false);
4252 DatatypeConstructor
Datatype::getConstructorForName(
4253 const std::string
& name
) const
4255 bool foundCons
= false;
4257 for (size_t i
= 0, ncons
= getNumConstructors(); i
< ncons
; i
++)
4259 if ((*d_dtype
)[i
].getName() == name
)
4268 std::stringstream snames
;
4270 for (size_t i
= 0, ncons
= getNumConstructors(); i
< ncons
; i
++)
4272 snames
<< (*d_dtype
)[i
].getName() << " ";
4275 CVC5_API_CHECK(foundCons
) << "No constructor " << name
<< " for datatype "
4276 << getName() << " exists, among " << snames
.str();
4278 return DatatypeConstructor(d_solver
, (*d_dtype
)[index
]);
4281 DatatypeSelector
Datatype::getSelectorForName(const std::string
& name
) const
4283 bool foundSel
= false;
4286 for (size_t i
= 0, ncons
= getNumConstructors(); i
< ncons
; i
++)
4288 int si
= (*d_dtype
)[i
].getSelectorIndexForName(name
);
4291 sindex
= static_cast<size_t>(si
);
4299 CVC5_API_CHECK(foundSel
)
4300 << "No select " << name
<< " for datatype " << getName() << " exists";
4302 return DatatypeSelector(d_solver
, (*d_dtype
)[index
][sindex
]);
4305 Datatype::const_iterator::const_iterator(const Solver
* slv
,
4306 const cvc5::DType
& dtype
,
4308 : d_solver(slv
), d_int_ctors(&dtype
.getConstructors())
4310 const std::vector
<std::shared_ptr
<DTypeConstructor
>>& cons
=
4311 dtype
.getConstructors();
4312 for (const std::shared_ptr
<DTypeConstructor
>& c
: cons
)
4314 /* Can not use emplace_back here since constructor is private. */
4315 d_ctors
.push_back(DatatypeConstructor(d_solver
, *c
.get()));
4317 d_idx
= begin
? 0 : cons
.size();
4320 Datatype::const_iterator::const_iterator()
4321 : d_solver(nullptr), d_int_ctors(nullptr), d_idx(0)
4325 Datatype::const_iterator
& Datatype::const_iterator::operator=(
4326 const Datatype::const_iterator
& it
)
4328 d_solver
= it
.d_solver
;
4329 d_int_ctors
= it
.d_int_ctors
;
4330 d_ctors
= it
.d_ctors
;
4335 const DatatypeConstructor
& Datatype::const_iterator::operator*() const
4337 return d_ctors
[d_idx
];
4340 const DatatypeConstructor
* Datatype::const_iterator::operator->() const
4342 return &d_ctors
[d_idx
];
4345 Datatype::const_iterator
& Datatype::const_iterator::operator++()
4351 Datatype::const_iterator
Datatype::const_iterator::operator++(int)
4353 Datatype::const_iterator
it(*this);
4358 bool Datatype::const_iterator::operator==(
4359 const Datatype::const_iterator
& other
) const
4361 return d_int_ctors
== other
.d_int_ctors
&& d_idx
== other
.d_idx
;
4364 bool Datatype::const_iterator::operator!=(
4365 const Datatype::const_iterator
& other
) const
4367 return d_int_ctors
!= other
.d_int_ctors
|| d_idx
!= other
.d_idx
;
4370 bool Datatype::isNullHelper() const { return d_dtype
== nullptr; }
4372 /* -------------------------------------------------------------------------- */
4374 /* -------------------------------------------------------------------------- */
4377 : d_solver(nullptr),
4387 Grammar::Grammar(const Solver
* slv
,
4388 const std::vector
<Term
>& sygusVars
,
4389 const std::vector
<Term
>& ntSymbols
)
4391 d_sygusVars(sygusVars
),
4392 d_ntSyms(ntSymbols
),
4393 d_ntsToTerms(ntSymbols
.size()),
4398 for (Term ntsymbol
: d_ntSyms
)
4400 d_ntsToTerms
.emplace(ntsymbol
, std::vector
<Term
>());
4404 void Grammar::addRule(const Term
& ntSymbol
, const Term
& rule
)
4406 CVC5_API_TRY_CATCH_BEGIN
;
4407 CVC5_API_CHECK(!d_isResolved
) << "Grammar cannot be modified after passing "
4408 "it as an argument to synthFun/synthInv";
4409 CVC5_API_CHECK_TERM(ntSymbol
);
4410 CVC5_API_CHECK_TERM(rule
);
4411 CVC5_API_ARG_CHECK_EXPECTED(
4412 d_ntsToTerms
.find(ntSymbol
) != d_ntsToTerms
.cend(), ntSymbol
)
4413 << "ntSymbol to be one of the non-terminal symbols given in the "
4415 CVC5_API_CHECK(ntSymbol
.d_node
->getType() == rule
.d_node
->getType())
4416 << "Expected ntSymbol and rule to have the same sort";
4417 CVC5_API_ARG_CHECK_EXPECTED(!containsFreeVariables(rule
), rule
)
4418 << "a term whose free variables are limited to synthFun/synthInv "
4419 "parameters and non-terminal symbols of the grammar";
4420 //////// all checks before this line
4421 d_ntsToTerms
[ntSymbol
].push_back(rule
);
4423 CVC5_API_TRY_CATCH_END
;
4426 void Grammar::addRules(const Term
& ntSymbol
, const std::vector
<Term
>& rules
)
4428 CVC5_API_TRY_CATCH_BEGIN
;
4429 CVC5_API_CHECK(!d_isResolved
) << "Grammar cannot be modified after passing "
4430 "it as an argument to synthFun/synthInv";
4431 CVC5_API_CHECK_TERM(ntSymbol
);
4432 CVC5_API_CHECK_TERMS_WITH_SORT(rules
, ntSymbol
.getSort());
4433 CVC5_API_ARG_CHECK_EXPECTED(
4434 d_ntsToTerms
.find(ntSymbol
) != d_ntsToTerms
.cend(), ntSymbol
)
4435 << "ntSymbol to be one of the non-terminal symbols given in the "
4437 for (size_t i
= 0, n
= rules
.size(); i
< n
; ++i
)
4439 CVC5_API_ARG_AT_INDEX_CHECK_EXPECTED(
4440 !containsFreeVariables(rules
[i
]), rules
[i
], rules
, i
)
4441 << "a term whose free variables are limited to synthFun/synthInv "
4442 "parameters and non-terminal symbols of the grammar";
4444 //////// all checks before this line
4445 d_ntsToTerms
[ntSymbol
].insert(
4446 d_ntsToTerms
[ntSymbol
].cend(), rules
.cbegin(), rules
.cend());
4448 CVC5_API_TRY_CATCH_END
;
4451 void Grammar::addAnyConstant(const Term
& ntSymbol
)
4453 CVC5_API_TRY_CATCH_BEGIN
;
4454 CVC5_API_CHECK(!d_isResolved
) << "Grammar cannot be modified after passing "
4455 "it as an argument to synthFun/synthInv";
4456 CVC5_API_CHECK_TERM(ntSymbol
);
4457 CVC5_API_ARG_CHECK_EXPECTED(
4458 d_ntsToTerms
.find(ntSymbol
) != d_ntsToTerms
.cend(), ntSymbol
)
4459 << "ntSymbol to be one of the non-terminal symbols given in the "
4461 //////// all checks before this line
4462 d_allowConst
.insert(ntSymbol
);
4464 CVC5_API_TRY_CATCH_END
;
4467 void Grammar::addAnyVariable(const Term
& ntSymbol
)
4469 CVC5_API_TRY_CATCH_BEGIN
;
4470 CVC5_API_CHECK(!d_isResolved
) << "Grammar cannot be modified after passing "
4471 "it as an argument to synthFun/synthInv";
4472 CVC5_API_CHECK_TERM(ntSymbol
);
4473 CVC5_API_ARG_CHECK_EXPECTED(
4474 d_ntsToTerms
.find(ntSymbol
) != d_ntsToTerms
.cend(), ntSymbol
)
4475 << "ntSymbol to be one of the non-terminal symbols given in the "
4477 //////// all checks before this line
4478 d_allowVars
.insert(ntSymbol
);
4480 CVC5_API_TRY_CATCH_END
;
4484 * This function concatenates the outputs of calling f on each element between
4485 * first and last, seperated by sep.
4486 * @param first the beginning of the range
4487 * @param last the end of the range
4488 * @param f the function to call on each element in the range, its output must
4489 * be overloaded for operator<<
4490 * @param sep the string to add between successive calls to f
4492 template <typename Iterator
, typename Function
>
4493 std::string
join(Iterator first
, Iterator last
, Function f
, std::string sep
)
4495 std::stringstream ss
;
4513 std::string
Grammar::toString() const
4515 CVC5_API_TRY_CATCH_BEGIN
;
4516 //////// all checks before this line
4517 std::stringstream ss
;
4518 ss
<< " (" // pre-declaration
4523 std::stringstream s
;
4524 s
<< '(' << t
<< ' ' << t
.getSort() << ')';
4528 << ")\n (" // grouped rule listing
4532 [this](const Term
& t
) {
4533 bool allowConst
= d_allowConst
.find(t
) != d_allowConst
.cend(),
4534 allowVars
= d_allowVars
.find(t
) != d_allowVars
.cend();
4535 const std::vector
<Term
>& rules
= d_ntsToTerms
.at(t
);
4536 std::stringstream s
;
4537 s
<< '(' << t
<< ' ' << t
.getSort() << " ("
4538 << (allowConst
? "(Constant " + t
.getSort().toString() + ")"
4540 << (allowConst
&& allowVars
? " " : "")
4541 << (allowVars
? "(Var " + t
.getSort().toString() + ")" : "")
4542 << ((allowConst
|| allowVars
) && !rules
.empty() ? " " : "")
4546 [](const Term
& rule
) { return rule
.toString(); },
4556 CVC5_API_TRY_CATCH_END
;
4559 Sort
Grammar::resolve()
4561 CVC5_API_TRY_CATCH_BEGIN
;
4562 //////// all checks before this line
4564 d_isResolved
= true;
4568 if (!d_sygusVars
.empty())
4572 d_solver
->getNodeManager()->mkNode(
4573 cvc5::kind::BOUND_VAR_LIST
, Term::termVectorToNodes(d_sygusVars
)));
4576 std::unordered_map
<Term
, Sort
> ntsToUnres(d_ntSyms
.size());
4578 for (Term ntsymbol
: d_ntSyms
)
4580 // make the unresolved type, used for referencing the final version of
4581 // the ntsymbol's datatype
4582 ntsToUnres
[ntsymbol
] =
4583 Sort(d_solver
, d_solver
->getNodeManager()->mkSort(ntsymbol
.toString()));
4586 std::vector
<cvc5::DType
> datatypes
;
4587 std::set
<TypeNode
> unresTypes
;
4589 datatypes
.reserve(d_ntSyms
.size());
4591 for (const Term
& ntSym
: d_ntSyms
)
4593 // make the datatype, which encodes terms generated by this non-terminal
4594 DatatypeDecl
dtDecl(d_solver
, ntSym
.toString());
4596 for (const Term
& consTerm
: d_ntsToTerms
[ntSym
])
4598 addSygusConstructorTerm(dtDecl
, consTerm
, ntsToUnres
);
4601 if (d_allowVars
.find(ntSym
) != d_allowVars
.cend())
4603 addSygusConstructorVariables(dtDecl
,
4604 Sort(d_solver
, ntSym
.d_node
->getType()));
4607 bool aci
= d_allowConst
.find(ntSym
) != d_allowConst
.end();
4608 TypeNode btt
= ntSym
.d_node
->getType();
4609 dtDecl
.d_dtype
->setSygus(btt
, *bvl
.d_node
, aci
, false);
4611 // We can be in a case where the only rule specified was (Variable T)
4612 // and there are no variables of type T, in which case this is a bogus
4613 // grammar. This results in the error below.
4614 CVC5_API_CHECK(dtDecl
.d_dtype
->getNumConstructors() != 0)
4615 << "Grouped rule listing for " << *dtDecl
.d_dtype
4616 << " produced an empty rule list";
4618 datatypes
.push_back(*dtDecl
.d_dtype
);
4619 unresTypes
.insert(*ntsToUnres
[ntSym
].d_type
);
4622 std::vector
<TypeNode
> datatypeTypes
=
4623 d_solver
->getNodeManager()->mkMutualDatatypeTypes(
4624 datatypes
, unresTypes
, NodeManager::DATATYPE_FLAG_PLACEHOLDER
);
4626 // return is the first datatype
4627 return Sort(d_solver
, datatypeTypes
[0]);
4629 CVC5_API_TRY_CATCH_END
;
4632 void Grammar::addSygusConstructorTerm(
4635 const std::unordered_map
<Term
, Sort
>& ntsToUnres
) const
4637 CVC5_API_TRY_CATCH_BEGIN
;
4638 CVC5_API_CHECK_DTDECL(dt
);
4639 CVC5_API_CHECK_TERM(term
);
4640 CVC5_API_CHECK_TERMS_MAP(ntsToUnres
);
4641 //////// all checks before this line
4643 // At this point, we should know that dt is well founded, and that its
4644 // builtin sygus operators are well-typed.
4645 // Now, purify each occurrence of a non-terminal symbol in term, replace by
4646 // free variables. These become arguments to constructors. Notice we must do
4647 // a tree traversal in this function, since unique paths to the same term
4648 // should be treated as distinct terms.
4649 // Notice that let expressions are forbidden in the input syntax of term, so
4650 // this does not lead to exponential behavior with respect to input size.
4651 std::vector
<Term
> args
;
4652 std::vector
<Sort
> cargs
;
4653 Term op
= purifySygusGTerm(term
, args
, cargs
, ntsToUnres
);
4654 std::stringstream ssCName
;
4655 ssCName
<< op
.getKind();
4660 d_solver
->getNodeManager()->mkNode(cvc5::kind::BOUND_VAR_LIST
,
4661 Term::termVectorToNodes(args
)));
4662 // its operator is a lambda
4664 d_solver
->getNodeManager()->mkNode(
4665 cvc5::kind::LAMBDA
, *lbvl
.d_node
, *op
.d_node
));
4667 std::vector
<TypeNode
> cargst
= Sort::sortVectorToTypeNodes(cargs
);
4668 dt
.d_dtype
->addSygusConstructor(*op
.d_node
, ssCName
.str(), cargst
);
4670 CVC5_API_TRY_CATCH_END
;
4673 Term
Grammar::purifySygusGTerm(
4675 std::vector
<Term
>& args
,
4676 std::vector
<Sort
>& cargs
,
4677 const std::unordered_map
<Term
, Sort
>& ntsToUnres
) const
4679 CVC5_API_TRY_CATCH_BEGIN
;
4680 CVC5_API_CHECK_TERM(term
);
4681 CVC5_API_CHECK_TERMS(args
);
4682 CVC5_API_CHECK_SORTS(cargs
);
4683 CVC5_API_CHECK_TERMS_MAP(ntsToUnres
);
4684 //////// all checks before this line
4686 std::unordered_map
<Term
, Sort
>::const_iterator itn
= ntsToUnres
.find(term
);
4687 if (itn
!= ntsToUnres
.cend())
4691 d_solver
->getNodeManager()->mkBoundVar(term
.d_node
->getType()));
4692 args
.push_back(ret
);
4693 cargs
.push_back(itn
->second
);
4696 std::vector
<Term
> pchildren
;
4697 bool childChanged
= false;
4698 for (unsigned i
= 0, nchild
= term
.d_node
->getNumChildren(); i
< nchild
; i
++)
4700 Term ptermc
= purifySygusGTerm(
4701 Term(d_solver
, (*term
.d_node
)[i
]), args
, cargs
, ntsToUnres
);
4702 pchildren
.push_back(ptermc
);
4703 childChanged
= childChanged
|| *ptermc
.d_node
!= (*term
.d_node
)[i
];
4712 if (term
.d_node
->getMetaKind() == kind::metakind::PARAMETERIZED
)
4714 // it's an indexed operator so we should provide the op
4715 NodeBuilder
nb(term
.d_node
->getKind());
4716 nb
<< term
.d_node
->getOperator();
4717 nb
.append(Term::termVectorToNodes(pchildren
));
4718 nret
= nb
.constructNode();
4722 nret
= d_solver
->getNodeManager()->mkNode(
4723 term
.d_node
->getKind(), Term::termVectorToNodes(pchildren
));
4726 return Term(d_solver
, nret
);
4728 CVC5_API_TRY_CATCH_END
;
4731 void Grammar::addSygusConstructorVariables(DatatypeDecl
& dt
,
4732 const Sort
& sort
) const
4734 CVC5_API_TRY_CATCH_BEGIN
;
4735 CVC5_API_CHECK_DTDECL(dt
);
4736 CVC5_API_CHECK_SORT(sort
);
4737 //////// all checks before this line
4739 // each variable of appropriate type becomes a sygus constructor in dt.
4740 for (unsigned i
= 0, size
= d_sygusVars
.size(); i
< size
; i
++)
4742 Term v
= d_sygusVars
[i
];
4743 if (v
.d_node
->getType() == *sort
.d_type
)
4745 std::stringstream ss
;
4747 std::vector
<TypeNode
> cargs
;
4748 dt
.d_dtype
->addSygusConstructor(*v
.d_node
, ss
.str(), cargs
);
4752 CVC5_API_TRY_CATCH_END
;
4755 bool Grammar::containsFreeVariables(const Term
& rule
) const
4757 // we allow the argument list and non-terminal symbols to be in scope
4758 std::unordered_set
<TNode
> scope
;
4760 for (const Term
& sygusVar
: d_sygusVars
)
4762 scope
.emplace(*sygusVar
.d_node
);
4765 for (const Term
& ntsymbol
: d_ntSyms
)
4767 scope
.emplace(*ntsymbol
.d_node
);
4770 return expr::hasFreeVariablesScope(*rule
.d_node
, scope
);
4773 std::ostream
& operator<<(std::ostream
& out
, const Grammar
& grammar
)
4775 return out
<< grammar
.toString();
4778 /* -------------------------------------------------------------------------- */
4779 /* Rounding Mode for Floating Points */
4780 /* -------------------------------------------------------------------------- */
4782 const static std::unordered_map
<RoundingMode
, cvc5::RoundingMode
> s_rmodes
{
4783 {ROUND_NEAREST_TIES_TO_EVEN
,
4784 cvc5::RoundingMode::ROUND_NEAREST_TIES_TO_EVEN
},
4785 {ROUND_TOWARD_POSITIVE
, cvc5::RoundingMode::ROUND_TOWARD_POSITIVE
},
4786 {ROUND_TOWARD_NEGATIVE
, cvc5::RoundingMode::ROUND_TOWARD_NEGATIVE
},
4787 {ROUND_TOWARD_ZERO
, cvc5::RoundingMode::ROUND_TOWARD_ZERO
},
4788 {ROUND_NEAREST_TIES_TO_AWAY
,
4789 cvc5::RoundingMode::ROUND_NEAREST_TIES_TO_AWAY
},
4792 const static std::unordered_map
<cvc5::RoundingMode
,
4794 cvc5::RoundingModeHashFunction
>
4796 {cvc5::RoundingMode::ROUND_NEAREST_TIES_TO_EVEN
,
4797 ROUND_NEAREST_TIES_TO_EVEN
},
4798 {cvc5::RoundingMode::ROUND_TOWARD_POSITIVE
, ROUND_TOWARD_POSITIVE
},
4799 {cvc5::RoundingMode::ROUND_TOWARD_POSITIVE
, ROUND_TOWARD_NEGATIVE
},
4800 {cvc5::RoundingMode::ROUND_TOWARD_ZERO
, ROUND_TOWARD_ZERO
},
4801 {cvc5::RoundingMode::ROUND_NEAREST_TIES_TO_AWAY
,
4802 ROUND_NEAREST_TIES_TO_AWAY
},
4805 /* -------------------------------------------------------------------------- */
4807 /* -------------------------------------------------------------------------- */
4809 DriverOptions::DriverOptions(const Solver
& solver
) : d_solver(solver
) {}
4811 std::istream
& DriverOptions::in() const
4813 return *d_solver
.d_slv
->getOptions().base
.in
;
4815 std::ostream
& DriverOptions::err() const
4817 return *d_solver
.d_slv
->getOptions().base
.err
;
4819 std::ostream
& DriverOptions::out() const
4821 return *d_solver
.d_slv
->getOptions().base
.out
;
4824 /* -------------------------------------------------------------------------- */
4826 /* -------------------------------------------------------------------------- */
4828 struct Stat::StatData
4830 cvc5::StatExportData data
;
4831 template <typename T
>
4832 StatData(T
&& t
) : data(std::forward
<T
>(t
))
4835 StatData() : data() {}
4839 Stat::Stat(const Stat
& s
)
4840 : d_expert(s
.d_expert
),
4841 d_default(s
.d_default
),
4842 d_data(std::make_unique
<StatData
>(s
.d_data
->data
))
4845 Stat
& Stat::operator=(const Stat
& s
)
4847 d_expert
= s
.d_expert
;
4848 d_data
= std::make_unique
<StatData
>(s
.d_data
->data
);
4852 bool Stat::isExpert() const { return d_expert
; }
4853 bool Stat::isDefault() const { return d_default
; }
4855 bool Stat::isInt() const
4857 return std::holds_alternative
<int64_t>(d_data
->data
);
4859 int64_t Stat::getInt() const
4861 CVC5_API_TRY_CATCH_BEGIN
;
4862 CVC5_API_RECOVERABLE_CHECK(isInt()) << "Expected Stat of type int64_t.";
4863 return std::get
<int64_t>(d_data
->data
);
4864 CVC5_API_TRY_CATCH_END
;
4866 bool Stat::isDouble() const
4868 return std::holds_alternative
<double>(d_data
->data
);
4870 double Stat::getDouble() const
4872 CVC5_API_TRY_CATCH_BEGIN
;
4873 CVC5_API_RECOVERABLE_CHECK(isDouble()) << "Expected Stat of type double.";
4874 return std::get
<double>(d_data
->data
);
4875 CVC5_API_TRY_CATCH_END
;
4877 bool Stat::isString() const
4879 return std::holds_alternative
<std::string
>(d_data
->data
);
4881 const std::string
& Stat::getString() const
4883 CVC5_API_TRY_CATCH_BEGIN
;
4884 CVC5_API_RECOVERABLE_CHECK(isString())
4885 << "Expected Stat of type std::string.";
4886 return std::get
<std::string
>(d_data
->data
);
4887 CVC5_API_TRY_CATCH_END
;
4889 bool Stat::isHistogram() const
4891 return std::holds_alternative
<HistogramData
>(d_data
->data
);
4893 const Stat::HistogramData
& Stat::getHistogram() const
4895 CVC5_API_TRY_CATCH_BEGIN
;
4896 CVC5_API_RECOVERABLE_CHECK(isHistogram())
4897 << "Expected Stat of type histogram.";
4898 return std::get
<HistogramData
>(d_data
->data
);
4899 CVC5_API_TRY_CATCH_END
;
4902 Stat::Stat(bool expert
, bool defaulted
, StatData
&& sd
)
4904 d_default(defaulted
),
4905 d_data(std::make_unique
<StatData
>(std::move(sd
)))
4909 std::ostream
& operator<<(std::ostream
& os
, const Stat
& sv
)
4911 return cvc5::detail::print(os
, sv
.d_data
->data
);
4914 Statistics::BaseType::const_reference
Statistics::iterator::operator*() const
4916 return d_it
.operator*();
4918 Statistics::BaseType::const_pointer
Statistics::iterator::operator->() const
4920 return d_it
.operator->();
4922 Statistics::iterator
& Statistics::iterator::operator++()
4927 } while (!isVisible());
4930 Statistics::iterator
Statistics::iterator::operator++(int)
4932 iterator tmp
= *this;
4936 } while (!isVisible());
4939 Statistics::iterator
& Statistics::iterator::operator--()
4944 } while (!isVisible());
4947 Statistics::iterator
Statistics::iterator::operator--(int)
4949 iterator tmp
= *this;
4953 } while (!isVisible());
4956 bool Statistics::iterator::operator==(const Statistics::iterator
& rhs
) const
4958 return d_it
== rhs
.d_it
;
4960 bool Statistics::iterator::operator!=(const Statistics::iterator
& rhs
) const
4962 return d_it
!= rhs
.d_it
;
4964 Statistics::iterator::iterator(Statistics::BaseType::const_iterator it
,
4965 const Statistics::BaseType
& base
,
4968 : d_it(it
), d_base(&base
), d_showExpert(expert
), d_showDefault(defaulted
)
4970 while (!isVisible())
4975 bool Statistics::iterator::isVisible() const
4977 if (d_it
== d_base
->end()) return true;
4978 if (!d_showExpert
&& d_it
->second
.isExpert()) return false;
4979 if (!d_showDefault
&& d_it
->second
.isDefault()) return false;
4983 const Stat
& Statistics::get(const std::string
& name
)
4985 CVC5_API_TRY_CATCH_BEGIN
;
4986 auto it
= d_stats
.find(name
);
4987 CVC5_API_RECOVERABLE_CHECK(it
!= d_stats
.end())
4988 << "No stat with name \"" << name
<< "\" exists.";
4990 CVC5_API_TRY_CATCH_END
;
4993 Statistics::iterator
Statistics::begin(bool expert
, bool defaulted
) const
4995 return iterator(d_stats
.begin(), d_stats
, expert
, defaulted
);
4997 Statistics::iterator
Statistics::end() const
4999 return iterator(d_stats
.end(), d_stats
, false, false);
5002 Statistics::Statistics(const StatisticsRegistry
& reg
)
5004 for (const auto& svp
: reg
)
5006 d_stats
.emplace(svp
.first
,
5007 Stat(svp
.second
->d_expert
,
5008 svp
.second
->isDefault(),
5009 svp
.second
->getViewer()));
5013 std::ostream
& operator<<(std::ostream
& out
, const Statistics
& stats
)
5015 for (const auto& stat
: stats
)
5017 out
<< stat
.first
<< " = " << stat
.second
<< std::endl
;
5022 /* -------------------------------------------------------------------------- */
5024 /* -------------------------------------------------------------------------- */
5026 Solver::Solver(std::unique_ptr
<Options
>&& original
)
5028 d_nodeMgr
= NodeManager::currentNM();
5030 d_originalOptions
= std::move(original
);
5031 d_slv
.reset(new SolverEngine(d_nodeMgr
, d_originalOptions
.get()));
5032 d_slv
->setSolver(this);
5033 d_rng
.reset(new Random(d_slv
->getOptions().driver
.seed
));
5037 Solver::Solver() : Solver(std::make_unique
<Options
>()) {}
5039 Solver::~Solver() {}
5041 /* Helpers and private functions */
5042 /* -------------------------------------------------------------------------- */
5044 NodeManager
* Solver::getNodeManager(void) const { return d_nodeMgr
; }
5046 void Solver::increment_term_stats(Kind kind
) const
5048 if constexpr (Configuration::isStatisticsBuild())
5050 d_stats
->d_terms
<< kind
;
5054 void Solver::increment_vars_consts_stats(const Sort
& sort
, bool is_var
) const
5056 if constexpr (Configuration::isStatisticsBuild())
5058 const TypeNode tn
= sort
.getTypeNode();
5059 TypeConstant tc
= tn
.getKind() == cvc5::kind::TYPE_CONSTANT
5060 ? tn
.getConst
<TypeConstant
>()
5064 d_stats
->d_vars
<< tc
;
5068 d_stats
->d_consts
<< tc
;
5073 /* Split out to avoid nested API calls (problematic with API tracing). */
5074 /* .......................................................................... */
5076 template <typename T
>
5077 Term
Solver::mkValHelper(const T
& t
) const
5079 //////// all checks before this line
5080 Node res
= getNodeManager()->mkConst(t
);
5081 (void)res
.getType(true); /* kick off type checking */
5082 return Term(this, res
);
5085 Term
Solver::mkRationalValHelper(const Rational
& r
, bool isInt
) const
5087 //////// all checks before this line
5088 NodeManager
* nm
= getNodeManager();
5089 Node res
= isInt
? nm
->mkConstInt(r
) : nm
->mkConstReal(r
);
5090 (void)res
.getType(true); /* kick off type checking */
5091 api::Term t
= Term(this, res
);
5092 // NOTE: this block will be eliminated when arithmetic subtyping is eliminated
5095 t
= ensureRealSort(t
);
5100 Term
Solver::mkRealOrIntegerFromStrHelper(const std::string
& s
,
5103 //////// all checks before this line
5106 cvc5::Rational r
= s
.find('/') != std::string::npos
5108 : cvc5::Rational::fromDecimal(s
);
5109 return mkRationalValHelper(r
, isInt
);
5111 catch (const std::invalid_argument
& e
)
5113 /* Catch to throw with a more meaningful error message. To be caught in
5114 * enclosing CVC5_API_TRY_CATCH_* block to throw CVC5ApiException. */
5115 std::stringstream message
;
5116 message
<< "Cannot construct Real or Int from string argument '" << s
<< "'"
5118 throw std::invalid_argument(message
.str());
5122 Term
Solver::mkBVFromIntHelper(uint32_t size
, uint64_t val
) const
5124 CVC5_API_ARG_CHECK_EXPECTED(size
> 0, size
) << "a bit-width > 0";
5125 //////// all checks before this line
5126 return mkValHelper
<cvc5::BitVector
>(cvc5::BitVector(size
, val
));
5129 Term
Solver::mkBVFromStrHelper(uint32_t size
,
5130 const std::string
& s
,
5131 uint32_t base
) const
5133 CVC5_API_ARG_CHECK_EXPECTED(size
> 0, size
) << "a bit-width > 0";
5134 CVC5_API_ARG_CHECK_EXPECTED(!s
.empty(), s
) << "a non-empty string";
5135 CVC5_API_ARG_CHECK_EXPECTED(base
== 2 || base
== 10 || base
== 16, base
)
5136 << "base 2, 10, or 16";
5137 //////// all checks before this line
5139 Integer
val(s
, base
);
5141 if (val
.strictlyNegative())
5143 CVC5_API_CHECK(val
>= -Integer(2).pow(size
- 1))
5144 << "Overflow in bitvector construction (specified bitvector size "
5145 << size
<< " too small to hold value " << s
<< ")";
5149 CVC5_API_CHECK(val
.modByPow2(size
) == val
)
5150 << "Overflow in bitvector construction (specified bitvector size "
5151 << size
<< " too small to hold value " << s
<< ")";
5153 return mkValHelper
<cvc5::BitVector
>(cvc5::BitVector(size
, val
));
5156 Term
Solver::getValueHelper(const Term
& term
) const
5158 // Note: Term is checked in the caller to avoid double checks
5159 bool wasShadow
= false;
5160 bool freeOrShadowedVar
=
5161 expr::hasFreeOrShadowedVar(term
.getNode(), wasShadow
);
5162 CVC5_API_RECOVERABLE_CHECK(!freeOrShadowedVar
)
5163 << "Cannot get value of term containing "
5164 << (wasShadow
? "shadowed" : "free") << " variables";
5165 //////// all checks before this line
5166 Node value
= d_slv
->getValue(*term
.d_node
);
5167 Term res
= Term(this, value
);
5168 // May need to wrap in real cast so that user know this is a real.
5169 TypeNode tn
= (*term
.d_node
).getType();
5170 if (!tn
.isInteger() && value
.getType().isInteger())
5172 return ensureRealSort(res
);
5177 Sort
Solver::mkTupleSortHelper(const std::vector
<Sort
>& sorts
) const
5179 // Note: Sorts are checked in the caller to avoid double checks
5180 //////// all checks before this line
5181 std::vector
<TypeNode
> typeNodes
= Sort::sortVectorToTypeNodes(sorts
);
5182 return Sort(this, getNodeManager()->mkTupleType(typeNodes
));
5185 Term
Solver::mkTermFromKind(Kind kind
) const
5187 CVC5_API_KIND_CHECK_EXPECTED(kind
== PI
|| kind
== REGEXP_NONE
5188 || kind
== REGEXP_ALLCHAR
|| kind
== SEP_EMP
,
5190 << "PI, REGEXP_NONE, REGEXP_ALLCHAR or SEP_EMP";
5191 //////// all checks before this line
5193 cvc5::Kind k
= extToIntKind(kind
);
5194 if (kind
== REGEXP_NONE
|| kind
== REGEXP_ALLCHAR
)
5196 Assert(isDefinedIntKind(k
));
5197 res
= d_nodeMgr
->mkNode(k
, std::vector
<Node
>());
5199 else if (kind
== SEP_EMP
)
5201 res
= d_nodeMgr
->mkNullaryOperator(d_nodeMgr
->booleanType(), k
);
5206 res
= d_nodeMgr
->mkNullaryOperator(d_nodeMgr
->realType(), k
);
5208 (void)res
.getType(true); /* kick off type checking */
5209 increment_term_stats(kind
);
5210 return Term(this, res
);
5213 Term
Solver::mkTermHelper(Kind kind
, const std::vector
<Term
>& children
) const
5215 // Note: Kind and children are checked in the caller to avoid double checks
5216 //////// all checks before this line
5217 if (children
.size() == 0)
5219 return mkTermFromKind(kind
);
5221 std::vector
<Node
> echildren
= Term::termVectorToNodes(children
);
5222 cvc5::Kind k
= extToIntKind(kind
);
5224 if (echildren
.size() > 2)
5226 if (kind
== INTS_DIVISION
|| kind
== XOR
|| kind
== MINUS
5227 || kind
== DIVISION
|| kind
== HO_APPLY
|| kind
== REGEXP_DIFF
)
5229 // left-associative, but cvc5 internally only supports 2 args
5230 res
= d_nodeMgr
->mkLeftAssociative(k
, echildren
);
5232 else if (kind
== IMPLIES
)
5234 // right-associative, but cvc5 internally only supports 2 args
5235 res
= d_nodeMgr
->mkRightAssociative(k
, echildren
);
5237 else if (kind
== EQUAL
|| kind
== LT
|| kind
== GT
|| kind
== LEQ
5240 // "chainable", but cvc5 internally only supports 2 args
5241 res
= d_nodeMgr
->mkChain(k
, echildren
);
5243 else if (kind::isAssociative(k
))
5245 // mkAssociative has special treatment for associative operators with lots
5247 res
= d_nodeMgr
->mkAssociative(k
, echildren
);
5251 // default case, must check kind
5252 checkMkTerm(kind
, children
.size());
5253 res
= d_nodeMgr
->mkNode(k
, echildren
);
5256 else if (kind::isAssociative(k
))
5258 // associative case, same as above
5259 res
= d_nodeMgr
->mkAssociative(k
, echildren
);
5263 // default case, same as above
5264 checkMkTerm(kind
, children
.size());
5265 if (kind
== api::SET_SINGLETON
)
5267 // the type of the term is the same as the type of the internal node
5268 // see Term::getSort()
5269 TypeNode type
= children
[0].d_node
->getType();
5270 // Internally NodeManager::mkSingleton needs a type argument
5271 // to construct a singleton, since there is no difference between
5272 // integers and reals (both are Rationals).
5273 // At the API, mkReal and mkInteger are different and therefore the
5274 // element type can be used safely here.
5275 res
= getNodeManager()->mkSingleton(type
, *children
[0].d_node
);
5277 else if (kind
== api::BAG_MAKE
)
5279 // the type of the term is the same as the type of the internal node
5280 // see Term::getSort()
5281 TypeNode type
= children
[0].d_node
->getType();
5282 // Internally NodeManager::mkBag needs a type argument
5283 // to construct a bag, since there is no difference between
5284 // integers and reals (both are Rationals).
5285 // At the API, mkReal and mkInteger are different and therefore the
5286 // element type can be used safely here.
5287 res
= getNodeManager()->mkBag(
5288 type
, *children
[0].d_node
, *children
[1].d_node
);
5292 res
= d_nodeMgr
->mkNode(k
, echildren
);
5296 (void)res
.getType(true); /* kick off type checking */
5297 increment_term_stats(kind
);
5298 return Term(this, res
);
5301 Term
Solver::mkTermHelper(const Op
& op
, const std::vector
<Term
>& children
) const
5303 if (!op
.isIndexedHelper())
5305 return mkTermHelper(op
.d_kind
, children
);
5308 // Note: Op and children are checked in the caller to avoid double checks
5309 checkMkTerm(op
.d_kind
, children
.size());
5310 //////// all checks before this line
5312 const cvc5::Kind int_kind
= extToIntKind(op
.d_kind
);
5313 std::vector
<Node
> echildren
= Term::termVectorToNodes(children
);
5315 NodeBuilder
nb(int_kind
);
5317 nb
.append(echildren
);
5318 Node res
= nb
.constructNode();
5320 (void)res
.getType(true); /* kick off type checking */
5321 return Term(this, res
);
5324 std::vector
<Sort
> Solver::mkDatatypeSortsInternal(
5325 const std::vector
<DatatypeDecl
>& dtypedecls
,
5326 const std::set
<Sort
>& unresolvedSorts
) const
5328 // Note: dtypedecls and unresolvedSorts are checked in the caller to avoid
5330 //////// all checks before this line
5332 std::vector
<cvc5::DType
> datatypes
;
5333 for (size_t i
= 0, ndts
= dtypedecls
.size(); i
< ndts
; ++i
)
5335 datatypes
.push_back(dtypedecls
[i
].getDatatype());
5338 std::set
<TypeNode
> utypes
= Sort::sortSetToTypeNodes(unresolvedSorts
);
5339 std::vector
<cvc5::TypeNode
> dtypes
=
5340 getNodeManager()->mkMutualDatatypeTypes(datatypes
, utypes
);
5341 std::vector
<Sort
> retTypes
= Sort::typeNodeVectorToSorts(this, dtypes
);
5345 Term
Solver::synthFunHelper(const std::string
& symbol
,
5346 const std::vector
<Term
>& boundVars
,
5349 Grammar
* grammar
) const
5351 // Note: boundVars, sort and grammar are checked in the caller to avoid
5353 std::vector
<TypeNode
> varTypes
;
5354 for (const auto& bv
: boundVars
)
5358 CVC5_API_CHECK(grammar
->d_ntSyms
[0].d_node
->getType() == *sort
.d_type
)
5359 << "Invalid Start symbol for grammar, Expected Start's sort to be "
5360 << *sort
.d_type
<< " but found "
5361 << grammar
->d_ntSyms
[0].d_node
->getType();
5363 varTypes
.push_back(bv
.d_node
->getType());
5365 //////// all checks before this line
5367 TypeNode funType
= varTypes
.empty() ? *sort
.d_type
5368 : getNodeManager()->mkFunctionType(
5369 varTypes
, *sort
.d_type
);
5371 Node fun
= getNodeManager()->mkBoundVar(symbol
, funType
);
5372 (void)fun
.getType(true); /* kick off type checking */
5374 std::vector
<Node
> bvns
= Term::termVectorToNodes(boundVars
);
5376 d_slv
->declareSynthFun(
5378 grammar
== nullptr ? funType
: *grammar
->resolve().d_type
,
5382 return Term(this, fun
);
5385 Term
Solver::ensureTermSort(const Term
& term
, const Sort
& sort
) const
5387 // Note: Term and sort are checked in the caller to avoid double checks
5388 CVC5_API_CHECK(term
.getSort() == sort
5389 || (term
.getSort().isInteger() && sort
.isReal()))
5390 << "Expected conversion from Int to Real";
5391 //////// all checks before this line
5393 Sort t
= term
.getSort();
5394 if (term
.getSort() == sort
)
5399 // Integers are reals, too
5400 Assert(t
.d_type
->isReal());
5404 // Must cast to Real to ensure correct type is passed to parametric type
5405 // constructors. We do this cast using division with 1. This has the
5406 // advantage wrt using TO_REAL since (constant) division is always included
5409 d_nodeMgr
->mkNode(extToIntKind(DIVISION
),
5411 d_nodeMgr
->mkConst(kind::CONST_RATIONAL
,
5412 cvc5::Rational(1))));
5414 Assert(res
.getSort() == sort
);
5418 Term
Solver::ensureRealSort(const Term
& t
) const
5420 Assert(this == t
.d_solver
);
5421 CVC5_API_ARG_CHECK_EXPECTED(
5422 t
.getSort() == getIntegerSort() || t
.getSort() == getRealSort(),
5423 " an integer or real term");
5424 // Note: Term is checked in the caller to avoid double checks
5425 //////// all checks before this line
5426 if (t
.getSort() == getIntegerSort())
5428 Node n
= getNodeManager()->mkNode(kind::CAST_TO_REAL
, *t
.d_node
);
5429 return Term(this, n
);
5434 bool Solver::isValidInteger(const std::string
& s
) const
5436 //////// all checks before this line
5437 if (s
.length() == 0)
5439 // string should not be empty
5444 if (s
[index
] == '-')
5446 if (s
.length() == 1)
5448 // negative integers should contain at least one digit
5454 if (s
[index
] == '0' && s
.length() > (index
+ 1))
5456 // From SMT-Lib 2.6: A <numeral> is the digit 0 or a non-empty sequence of
5457 // digits not starting with 0. So integers like 001, 000 are not allowed
5461 // all remaining characters should be decimal digits
5462 for (; index
< s
.length(); ++index
)
5464 if (!std::isdigit(s
[index
]))
5473 void Solver::resetStatistics()
5475 if constexpr (Configuration::isStatisticsBuild())
5477 d_stats
.reset(new APIStatistics
{
5478 d_slv
->getStatisticsRegistry().registerHistogram
<TypeConstant
>(
5480 d_slv
->getStatisticsRegistry().registerHistogram
<TypeConstant
>(
5482 d_slv
->getStatisticsRegistry().registerHistogram
<Kind
>("api::TERM"),
5487 void Solver::printStatisticsSafe(int fd
) const
5489 d_slv
->printStatisticsSafe(fd
);
5492 /* Helpers for mkTerm checks. */
5493 /* .......................................................................... */
5495 void Solver::checkMkTerm(Kind kind
, uint32_t nchildren
) const
5497 CVC5_API_KIND_CHECK(kind
);
5498 Assert(isDefinedIntKind(extToIntKind(kind
)));
5499 const cvc5::kind::MetaKind mk
= kind::metaKindOf(extToIntKind(kind
));
5500 CVC5_API_KIND_CHECK_EXPECTED(
5501 mk
== kind::metakind::PARAMETERIZED
|| mk
== kind::metakind::OPERATOR
,
5503 << "Only operator-style terms are created with mkTerm(), "
5504 "to create variables, constants and values see mkVar(), mkConst() "
5505 "and the respective theory-specific functions to create values, "
5506 "e.g., mkBitVector().";
5507 CVC5_API_KIND_CHECK_EXPECTED(
5508 nchildren
>= minArity(kind
) && nchildren
<= maxArity(kind
), kind
)
5509 << "Terms with kind " << kindToString(kind
) << " must have at least "
5510 << minArity(kind
) << " children and at most " << maxArity(kind
)
5511 << " children (the one under construction has " << nchildren
<< ")";
5514 /* Sorts Handling */
5515 /* -------------------------------------------------------------------------- */
5517 Sort
Solver::getNullSort(void) const
5519 CVC5_API_TRY_CATCH_BEGIN
;
5520 //////// all checks before this line
5521 return Sort(this, TypeNode());
5523 CVC5_API_TRY_CATCH_END
;
5526 Sort
Solver::getBooleanSort(void) const
5528 CVC5_API_TRY_CATCH_BEGIN
;
5529 //////// all checks before this line
5530 return Sort(this, getNodeManager()->booleanType());
5532 CVC5_API_TRY_CATCH_END
;
5535 Sort
Solver::getIntegerSort(void) const
5537 CVC5_API_TRY_CATCH_BEGIN
;
5538 //////// all checks before this line
5539 return Sort(this, getNodeManager()->integerType());
5541 CVC5_API_TRY_CATCH_END
;
5544 Sort
Solver::getRealSort(void) const
5546 CVC5_API_TRY_CATCH_BEGIN
;
5547 //////// all checks before this line
5548 return Sort(this, getNodeManager()->realType());
5550 CVC5_API_TRY_CATCH_END
;
5553 Sort
Solver::getRegExpSort(void) const
5555 CVC5_API_TRY_CATCH_BEGIN
;
5556 //////// all checks before this line
5557 return Sort(this, getNodeManager()->regExpType());
5559 CVC5_API_TRY_CATCH_END
;
5562 Sort
Solver::getStringSort(void) const
5564 CVC5_API_TRY_CATCH_BEGIN
;
5565 //////// all checks before this line
5566 return Sort(this, getNodeManager()->stringType());
5568 CVC5_API_TRY_CATCH_END
;
5571 Sort
Solver::getRoundingModeSort(void) const
5573 CVC5_API_TRY_CATCH_BEGIN
;
5574 //////// all checks before this line
5575 return Sort(this, getNodeManager()->roundingModeType());
5577 CVC5_API_TRY_CATCH_END
;
5580 /* Create sorts ------------------------------------------------------- */
5582 Sort
Solver::mkArraySort(const Sort
& indexSort
, const Sort
& elemSort
) const
5584 CVC5_API_TRY_CATCH_BEGIN
;
5585 CVC5_API_SOLVER_CHECK_SORT(indexSort
);
5586 CVC5_API_SOLVER_CHECK_SORT(elemSort
);
5587 //////// all checks before this line
5589 this, getNodeManager()->mkArrayType(*indexSort
.d_type
, *elemSort
.d_type
));
5591 CVC5_API_TRY_CATCH_END
;
5594 Sort
Solver::mkBitVectorSort(uint32_t size
) const
5596 CVC5_API_TRY_CATCH_BEGIN
;
5597 CVC5_API_ARG_CHECK_EXPECTED(size
> 0, size
) << "size > 0";
5598 //////// all checks before this line
5599 return Sort(this, getNodeManager()->mkBitVectorType(size
));
5601 CVC5_API_TRY_CATCH_END
;
5604 Sort
Solver::mkFloatingPointSort(uint32_t exp
, uint32_t sig
) const
5606 CVC5_API_TRY_CATCH_BEGIN
;
5607 CVC5_API_ARG_CHECK_EXPECTED(exp
> 0, exp
) << "exponent size > 0";
5608 CVC5_API_ARG_CHECK_EXPECTED(sig
> 0, sig
) << "significand size > 0";
5609 //////// all checks before this line
5610 return Sort(this, getNodeManager()->mkFloatingPointType(exp
, sig
));
5612 CVC5_API_TRY_CATCH_END
;
5615 Sort
Solver::mkDatatypeSort(const DatatypeDecl
& dtypedecl
) const
5617 CVC5_API_TRY_CATCH_BEGIN
;
5618 CVC5_API_SOLVER_CHECK_DTDECL(dtypedecl
);
5619 //////// all checks before this line
5620 return Sort(this, getNodeManager()->mkDatatypeType(*dtypedecl
.d_dtype
));
5622 CVC5_API_TRY_CATCH_END
;
5625 std::vector
<Sort
> Solver::mkDatatypeSorts(
5626 const std::vector
<DatatypeDecl
>& dtypedecls
) const
5628 CVC5_API_SOLVER_CHECK_DTDECLS(dtypedecls
);
5629 CVC5_API_TRY_CATCH_BEGIN
;
5630 //////// all checks before this line
5631 return mkDatatypeSortsInternal(dtypedecls
, {});
5633 CVC5_API_TRY_CATCH_END
;
5636 std::vector
<Sort
> Solver::mkDatatypeSorts(
5637 const std::vector
<DatatypeDecl
>& dtypedecls
,
5638 const std::set
<Sort
>& unresolvedSorts
) const
5640 CVC5_API_TRY_CATCH_BEGIN
;
5641 CVC5_API_SOLVER_CHECK_DTDECLS(dtypedecls
);
5642 CVC5_API_SOLVER_CHECK_SORTS(unresolvedSorts
);
5643 //////// all checks before this line
5644 return mkDatatypeSortsInternal(dtypedecls
, unresolvedSorts
);
5646 CVC5_API_TRY_CATCH_END
;
5649 Sort
Solver::mkFunctionSort(const Sort
& domain
, const Sort
& codomain
) const
5651 CVC5_API_TRY_CATCH_BEGIN
;
5652 CVC5_API_SOLVER_CHECK_DOMAIN_SORT(domain
);
5653 CVC5_API_SOLVER_CHECK_CODOMAIN_SORT(codomain
);
5654 //////// all checks before this line
5656 this, getNodeManager()->mkFunctionType(*domain
.d_type
, *codomain
.d_type
));
5658 CVC5_API_TRY_CATCH_END
;
5661 Sort
Solver::mkFunctionSort(const std::vector
<Sort
>& sorts
,
5662 const Sort
& codomain
) const
5664 CVC5_API_TRY_CATCH_BEGIN
;
5665 CVC5_API_ARG_SIZE_CHECK_EXPECTED(sorts
.size() >= 1, sorts
)
5666 << "at least one parameter sort for function sort";
5667 CVC5_API_SOLVER_CHECK_DOMAIN_SORTS(sorts
);
5668 CVC5_API_SOLVER_CHECK_CODOMAIN_SORT(codomain
);
5669 //////// all checks before this line
5670 std::vector
<TypeNode
> argTypes
= Sort::sortVectorToTypeNodes(sorts
);
5672 getNodeManager()->mkFunctionType(argTypes
, *codomain
.d_type
));
5674 CVC5_API_TRY_CATCH_END
;
5677 Sort
Solver::mkParamSort(const std::string
& symbol
) const
5679 CVC5_API_TRY_CATCH_BEGIN
;
5680 //////// all checks before this line
5683 getNodeManager()->mkSort(symbol
, NodeManager::SORT_FLAG_PLACEHOLDER
));
5685 CVC5_API_TRY_CATCH_END
;
5688 Sort
Solver::mkPredicateSort(const std::vector
<Sort
>& sorts
) const
5690 CVC5_API_TRY_CATCH_BEGIN
;
5691 CVC5_API_ARG_SIZE_CHECK_EXPECTED(sorts
.size() >= 1, sorts
)
5692 << "at least one parameter sort for predicate sort";
5693 CVC5_API_SOLVER_CHECK_DOMAIN_SORTS(sorts
);
5694 //////// all checks before this line
5697 getNodeManager()->mkPredicateType(Sort::sortVectorToTypeNodes(sorts
)));
5699 CVC5_API_TRY_CATCH_END
;
5702 Sort
Solver::mkRecordSort(
5703 const std::vector
<std::pair
<std::string
, Sort
>>& fields
) const
5705 CVC5_API_TRY_CATCH_BEGIN
;
5706 std::vector
<std::pair
<std::string
, TypeNode
>> f
;
5707 for (size_t i
= 0, size
= fields
.size(); i
< size
; ++i
)
5709 const auto& p
= fields
[i
];
5710 CVC5_API_ARG_AT_INDEX_CHECK_EXPECTED(!p
.second
.isNull(), "sort", fields
, i
)
5712 CVC5_API_ARG_AT_INDEX_CHECK_EXPECTED(
5713 this == p
.second
.d_solver
, "sort", fields
, i
)
5714 << "sort associated with this solver object";
5715 f
.emplace_back(p
.first
, *p
.second
.d_type
);
5717 //////// all checks before this line
5718 return Sort(this, getNodeManager()->mkRecordType(f
));
5720 CVC5_API_TRY_CATCH_END
;
5723 Sort
Solver::mkSetSort(const Sort
& elemSort
) const
5725 CVC5_API_TRY_CATCH_BEGIN
;
5726 CVC5_API_SOLVER_CHECK_SORT(elemSort
);
5727 //////// all checks before this line
5728 return Sort(this, getNodeManager()->mkSetType(*elemSort
.d_type
));
5730 CVC5_API_TRY_CATCH_END
;
5733 Sort
Solver::mkBagSort(const Sort
& elemSort
) const
5735 CVC5_API_TRY_CATCH_BEGIN
;
5736 CVC5_API_SOLVER_CHECK_SORT(elemSort
);
5737 //////// all checks before this line
5738 return Sort(this, getNodeManager()->mkBagType(*elemSort
.d_type
));
5740 CVC5_API_TRY_CATCH_END
;
5743 Sort
Solver::mkSequenceSort(const Sort
& elemSort
) const
5745 CVC5_API_TRY_CATCH_BEGIN
;
5746 CVC5_API_SOLVER_CHECK_SORT(elemSort
);
5747 //////// all checks before this line
5748 return Sort(this, getNodeManager()->mkSequenceType(*elemSort
.d_type
));
5750 CVC5_API_TRY_CATCH_END
;
5753 Sort
Solver::mkUninterpretedSort(const std::string
& symbol
) const
5755 CVC5_API_TRY_CATCH_BEGIN
;
5756 //////// all checks before this line
5757 return Sort(this, getNodeManager()->mkSort(symbol
));
5759 CVC5_API_TRY_CATCH_END
;
5762 Sort
Solver::mkUnresolvedSort(const std::string
& symbol
, size_t arity
) const
5764 CVC5_API_TRY_CATCH_BEGIN
;
5765 //////// all checks before this line
5768 return Sort(this, getNodeManager()->mkSortConstructor(symbol
, arity
));
5770 return Sort(this, getNodeManager()->mkSort(symbol
));
5772 CVC5_API_TRY_CATCH_END
;
5775 Sort
Solver::mkSortConstructorSort(const std::string
& symbol
,
5778 CVC5_API_TRY_CATCH_BEGIN
;
5779 CVC5_API_ARG_CHECK_EXPECTED(arity
> 0, arity
) << "an arity > 0";
5780 //////// all checks before this line
5781 return Sort(this, getNodeManager()->mkSortConstructor(symbol
, arity
));
5783 CVC5_API_TRY_CATCH_END
;
5786 Sort
Solver::mkTupleSort(const std::vector
<Sort
>& sorts
) const
5788 CVC5_API_TRY_CATCH_BEGIN
;
5789 CVC5_API_SOLVER_CHECK_SORTS_NOT_FUNCTION_LIKE(sorts
);
5790 //////// all checks before this line
5791 return mkTupleSortHelper(sorts
);
5793 CVC5_API_TRY_CATCH_END
;
5797 /* -------------------------------------------------------------------------- */
5799 Term
Solver::mkTrue(void) const
5801 CVC5_API_TRY_CATCH_BEGIN
;
5802 //////// all checks before this line
5803 return Term(this, d_nodeMgr
->mkConst
<bool>(true));
5805 CVC5_API_TRY_CATCH_END
;
5808 Term
Solver::mkFalse(void) const
5810 CVC5_API_TRY_CATCH_BEGIN
;
5811 //////// all checks before this line
5812 return Term(this, d_nodeMgr
->mkConst
<bool>(false));
5814 CVC5_API_TRY_CATCH_END
;
5817 Term
Solver::mkBoolean(bool val
) const
5819 CVC5_API_TRY_CATCH_BEGIN
;
5820 //////// all checks before this line
5821 return Term(this, d_nodeMgr
->mkConst
<bool>(val
));
5823 CVC5_API_TRY_CATCH_END
;
5826 Term
Solver::mkPi() const
5828 CVC5_API_TRY_CATCH_BEGIN
;
5829 //////// all checks before this line
5831 d_nodeMgr
->mkNullaryOperator(d_nodeMgr
->realType(), cvc5::kind::PI
);
5832 (void)res
.getType(true); /* kick off type checking */
5833 return Term(this, res
);
5835 CVC5_API_TRY_CATCH_END
;
5838 Term
Solver::mkInteger(const std::string
& s
) const
5840 CVC5_API_TRY_CATCH_BEGIN
;
5841 CVC5_API_ARG_CHECK_EXPECTED(isValidInteger(s
), s
) << " an integer ";
5842 Term integer
= mkRealOrIntegerFromStrHelper(s
);
5843 CVC5_API_ARG_CHECK_EXPECTED(integer
.getSort() == getIntegerSort(), s
)
5844 << " a string representing an integer";
5845 //////// all checks before this line
5848 CVC5_API_TRY_CATCH_END
;
5851 Term
Solver::mkInteger(int64_t val
) const
5853 CVC5_API_TRY_CATCH_BEGIN
;
5854 //////// all checks before this line
5855 Term integer
= mkRationalValHelper(cvc5::Rational(val
));
5856 Assert(integer
.getSort() == getIntegerSort());
5859 CVC5_API_TRY_CATCH_END
;
5862 Term
Solver::mkReal(const std::string
& s
) const
5864 CVC5_API_TRY_CATCH_BEGIN
;
5865 /* CLN and GMP handle this case differently, CLN interprets it as 0, GMP
5866 * throws an std::invalid_argument exception. For consistency, we treat it
5868 CVC5_API_ARG_CHECK_EXPECTED(s
!= ".", s
)
5869 << "a string representing a real or rational value.";
5870 //////// all checks before this line
5871 return mkRealOrIntegerFromStrHelper(s
, false);
5873 CVC5_API_TRY_CATCH_END
;
5876 Term
Solver::mkReal(int64_t val
) const
5878 CVC5_API_TRY_CATCH_BEGIN
;
5879 //////// all checks before this line
5880 return mkRationalValHelper(cvc5::Rational(val
), false);
5882 CVC5_API_TRY_CATCH_END
;
5885 Term
Solver::mkReal(int64_t num
, int64_t den
) const
5887 CVC5_API_TRY_CATCH_BEGIN
;
5888 //////// all checks before this line
5889 return mkRationalValHelper(cvc5::Rational(num
, den
), false);
5891 CVC5_API_TRY_CATCH_END
;
5894 Term
Solver::mkRegexpAll() const
5896 CVC5_API_TRY_CATCH_BEGIN
;
5897 //////// all checks before this line
5898 Node res
= d_nodeMgr
->mkNode(
5899 cvc5::kind::REGEXP_STAR
,
5900 d_nodeMgr
->mkNode(cvc5::kind::REGEXP_ALLCHAR
, std::vector
<cvc5::Node
>()));
5901 (void)res
.getType(true); /* kick off type checking */
5902 return Term(this, res
);
5904 CVC5_API_TRY_CATCH_END
;
5907 Term
Solver::mkRegexpNone() const
5909 CVC5_API_TRY_CATCH_BEGIN
;
5910 //////// all checks before this line
5912 d_nodeMgr
->mkNode(cvc5::kind::REGEXP_NONE
, std::vector
<cvc5::Node
>());
5913 (void)res
.getType(true); /* kick off type checking */
5914 return Term(this, res
);
5916 CVC5_API_TRY_CATCH_END
;
5919 Term
Solver::mkRegexpAllchar() const
5921 CVC5_API_TRY_CATCH_BEGIN
;
5922 //////// all checks before this line
5924 d_nodeMgr
->mkNode(cvc5::kind::REGEXP_ALLCHAR
, std::vector
<cvc5::Node
>());
5925 (void)res
.getType(true); /* kick off type checking */
5926 return Term(this, res
);
5928 CVC5_API_TRY_CATCH_END
;
5931 Term
Solver::mkEmptySet(const Sort
& sort
) const
5933 CVC5_API_TRY_CATCH_BEGIN
;
5934 CVC5_API_ARG_CHECK_EXPECTED(sort
.isNull() || sort
.isSet(), sort
)
5935 << "null sort or set sort";
5936 CVC5_API_ARG_CHECK_EXPECTED(sort
.isNull() || this == sort
.d_solver
, sort
)
5937 << "set sort associated with this solver object";
5938 //////// all checks before this line
5939 return mkValHelper
<cvc5::EmptySet
>(cvc5::EmptySet(*sort
.d_type
));
5941 CVC5_API_TRY_CATCH_END
;
5944 Term
Solver::mkEmptyBag(const Sort
& sort
) const
5946 CVC5_API_TRY_CATCH_BEGIN
;
5947 CVC5_API_ARG_CHECK_EXPECTED(sort
.isNull() || sort
.isBag(), sort
)
5948 << "null sort or bag sort";
5949 CVC5_API_ARG_CHECK_EXPECTED(sort
.isNull() || this == sort
.d_solver
, sort
)
5950 << "bag sort associated with this solver object";
5951 //////// all checks before this line
5952 return mkValHelper
<cvc5::EmptyBag
>(cvc5::EmptyBag(*sort
.d_type
));
5954 CVC5_API_TRY_CATCH_END
;
5957 Term
Solver::mkSepEmp() const
5959 CVC5_API_TRY_CATCH_BEGIN
;
5960 //////// all checks before this line
5961 Node res
= getNodeManager()->mkNullaryOperator(d_nodeMgr
->booleanType(),
5962 cvc5::Kind::SEP_EMP
);
5963 (void)res
.getType(true); /* kick off type checking */
5964 return Term(this, res
);
5966 CVC5_API_TRY_CATCH_END
;
5969 Term
Solver::mkSepNil(const Sort
& sort
) const
5971 CVC5_API_TRY_CATCH_BEGIN
;
5972 CVC5_API_SOLVER_CHECK_SORT(sort
);
5973 //////// all checks before this line
5975 getNodeManager()->mkNullaryOperator(*sort
.d_type
, cvc5::kind::SEP_NIL
);
5976 (void)res
.getType(true); /* kick off type checking */
5977 return Term(this, res
);
5979 CVC5_API_TRY_CATCH_END
;
5982 Term
Solver::mkString(const std::string
& s
, bool useEscSequences
) const
5984 CVC5_API_TRY_CATCH_BEGIN
;
5985 //////// all checks before this line
5986 return mkValHelper
<cvc5::String
>(cvc5::String(s
, useEscSequences
));
5988 CVC5_API_TRY_CATCH_END
;
5991 Term
Solver::mkString(const std::wstring
& s
) const
5993 CVC5_API_TRY_CATCH_BEGIN
;
5994 //////// all checks before this line
5995 return mkValHelper
<cvc5::String
>(cvc5::String(s
));
5997 CVC5_API_TRY_CATCH_END
;
6000 Term
Solver::mkEmptySequence(const Sort
& sort
) const
6002 CVC5_API_TRY_CATCH_BEGIN
;
6003 CVC5_API_SOLVER_CHECK_SORT(sort
);
6004 //////// all checks before this line
6005 std::vector
<Node
> seq
;
6006 Node res
= d_nodeMgr
->mkConst(Sequence(*sort
.d_type
, seq
));
6007 return Term(this, res
);
6009 CVC5_API_TRY_CATCH_END
;
6012 Term
Solver::mkUniverseSet(const Sort
& sort
) const
6014 CVC5_API_TRY_CATCH_BEGIN
;
6015 CVC5_API_SOLVER_CHECK_SORT(sort
);
6016 //////// all checks before this line
6018 Node res
= getNodeManager()->mkNullaryOperator(*sort
.d_type
,
6019 cvc5::kind::SET_UNIVERSE
);
6020 // TODO(#2771): Reenable?
6021 // (void)res->getType(true); /* kick off type checking */
6022 return Term(this, res
);
6024 CVC5_API_TRY_CATCH_END
;
6027 Term
Solver::mkBitVector(uint32_t size
, uint64_t val
) const
6029 CVC5_API_TRY_CATCH_BEGIN
;
6030 //////// all checks before this line
6031 return mkBVFromIntHelper(size
, val
);
6033 CVC5_API_TRY_CATCH_END
;
6036 Term
Solver::mkBitVector(uint32_t size
,
6037 const std::string
& s
,
6038 uint32_t base
) const
6040 CVC5_API_TRY_CATCH_BEGIN
;
6041 //////// all checks before this line
6042 return mkBVFromStrHelper(size
, s
, base
);
6044 CVC5_API_TRY_CATCH_END
;
6047 Term
Solver::mkConstArray(const Sort
& sort
, const Term
& val
) const
6049 CVC5_API_TRY_CATCH_BEGIN
;
6050 CVC5_API_SOLVER_CHECK_SORT(sort
);
6051 CVC5_API_SOLVER_CHECK_TERM(val
);
6052 CVC5_API_ARG_CHECK_EXPECTED(sort
.isArray(), sort
) << "an array sort";
6053 CVC5_API_CHECK(val
.getSort().isSubsortOf(sort
.getArrayElementSort()))
6054 << "Value does not match element sort";
6055 //////// all checks before this line
6057 // handle the special case of (CAST_TO_REAL n) where n is an integer
6058 Node n
= *val
.d_node
;
6059 if (val
.isCastedReal())
6061 // this is safe because the constant array stores its type
6065 mkValHelper
<cvc5::ArrayStoreAll
>(cvc5::ArrayStoreAll(*sort
.d_type
, n
));
6068 CVC5_API_TRY_CATCH_END
;
6071 Term
Solver::mkPosInf(uint32_t exp
, uint32_t sig
) const
6073 CVC5_API_TRY_CATCH_BEGIN
;
6074 //////// all checks before this line
6075 return mkValHelper
<cvc5::FloatingPoint
>(
6076 FloatingPoint::makeInf(FloatingPointSize(exp
, sig
), false));
6078 CVC5_API_TRY_CATCH_END
;
6081 Term
Solver::mkNegInf(uint32_t exp
, uint32_t sig
) const
6083 CVC5_API_TRY_CATCH_BEGIN
;
6084 //////// all checks before this line
6085 return mkValHelper
<cvc5::FloatingPoint
>(
6086 FloatingPoint::makeInf(FloatingPointSize(exp
, sig
), true));
6088 CVC5_API_TRY_CATCH_END
;
6091 Term
Solver::mkNaN(uint32_t exp
, uint32_t sig
) const
6093 CVC5_API_TRY_CATCH_BEGIN
;
6094 //////// all checks before this line
6095 return mkValHelper
<cvc5::FloatingPoint
>(
6096 FloatingPoint::makeNaN(FloatingPointSize(exp
, sig
)));
6098 CVC5_API_TRY_CATCH_END
;
6101 Term
Solver::mkPosZero(uint32_t exp
, uint32_t sig
) const
6103 CVC5_API_TRY_CATCH_BEGIN
;
6104 //////// all checks before this line
6105 return mkValHelper
<cvc5::FloatingPoint
>(
6106 FloatingPoint::makeZero(FloatingPointSize(exp
, sig
), false));
6108 CVC5_API_TRY_CATCH_END
;
6111 Term
Solver::mkNegZero(uint32_t exp
, uint32_t sig
) const
6113 CVC5_API_TRY_CATCH_BEGIN
;
6114 //////// all checks before this line
6115 return mkValHelper
<cvc5::FloatingPoint
>(
6116 FloatingPoint::makeZero(FloatingPointSize(exp
, sig
), true));
6118 CVC5_API_TRY_CATCH_END
;
6121 Term
Solver::mkRoundingMode(RoundingMode rm
) const
6123 CVC5_API_TRY_CATCH_BEGIN
;
6124 //////// all checks before this line
6125 return mkValHelper
<cvc5::RoundingMode
>(s_rmodes
.at(rm
));
6127 CVC5_API_TRY_CATCH_END
;
6130 Term
Solver::mkUninterpretedConst(const Sort
& sort
, int32_t index
) const
6132 CVC5_API_TRY_CATCH_BEGIN
;
6133 CVC5_API_SOLVER_CHECK_SORT(sort
);
6134 //////// all checks before this line
6135 return mkValHelper
<cvc5::UninterpretedConstant
>(
6136 cvc5::UninterpretedConstant(*sort
.d_type
, index
));
6138 CVC5_API_TRY_CATCH_END
;
6141 Term
Solver::mkAbstractValue(const std::string
& index
) const
6143 CVC5_API_TRY_CATCH_BEGIN
;
6144 CVC5_API_ARG_CHECK_EXPECTED(!index
.empty(), index
) << "a non-empty string";
6146 cvc5::Integer
idx(index
, 10);
6147 CVC5_API_ARG_CHECK_EXPECTED(idx
> 0, index
)
6148 << "a string representing an integer > 0";
6149 //////// all checks before this line
6150 return Term(this, getNodeManager()->mkConst(cvc5::AbstractValue(idx
)));
6151 // do not call getType(), for abstract values, type can not be computed
6152 // until it is substituted away
6154 CVC5_API_TRY_CATCH_END
;
6157 Term
Solver::mkAbstractValue(uint64_t index
) const
6159 CVC5_API_TRY_CATCH_BEGIN
;
6160 CVC5_API_ARG_CHECK_EXPECTED(index
> 0, index
) << "an integer > 0";
6161 //////// all checks before this line
6163 getNodeManager()->mkConst(cvc5::AbstractValue(Integer(index
))));
6164 // do not call getType(), for abstract values, type can not be computed
6165 // until it is substituted away
6167 CVC5_API_TRY_CATCH_END
;
6170 Term
Solver::mkFloatingPoint(uint32_t exp
, uint32_t sig
, Term val
) const
6172 CVC5_API_TRY_CATCH_BEGIN
;
6173 CVC5_API_SOLVER_CHECK_TERM(val
);
6174 CVC5_API_ARG_CHECK_EXPECTED(exp
> 0, exp
) << "a value > 0";
6175 CVC5_API_ARG_CHECK_EXPECTED(sig
> 0, sig
) << "a value > 0";
6176 uint32_t bw
= exp
+ sig
;
6177 CVC5_API_ARG_CHECK_EXPECTED(bw
== val
.d_node
->getType().getBitVectorSize(),
6179 << "a bit-vector constant with bit-width '" << bw
<< "'";
6180 CVC5_API_ARG_CHECK_EXPECTED(
6181 val
.d_node
->getType().isBitVector() && val
.d_node
->isConst(), val
)
6182 << "bit-vector constant";
6183 //////// all checks before this line
6184 return mkValHelper
<cvc5::FloatingPoint
>(
6185 cvc5::FloatingPoint(exp
, sig
, val
.d_node
->getConst
<BitVector
>()));
6187 CVC5_API_TRY_CATCH_END
;
6190 Term
Solver::mkCardinalityConstraint(const Sort
& sort
, uint32_t upperBound
) const
6192 CVC5_API_TRY_CATCH_BEGIN
;
6193 CVC5_API_SOLVER_CHECK_SORT(sort
);
6194 CVC5_API_ARG_CHECK_EXPECTED(sort
.isUninterpretedSort(), sort
)
6195 << "an uninterpreted sort";
6196 CVC5_API_ARG_CHECK_EXPECTED(upperBound
> 0, upperBound
) << "a value > 0";
6197 //////// all checks before this line
6199 d_nodeMgr
->mkConst(cvc5::CardinalityConstraint(*sort
.d_type
, upperBound
));
6200 Node cc
= d_nodeMgr
->mkNode(cvc5::Kind::CARDINALITY_CONSTRAINT
, cco
);
6201 return Term(this, cc
);
6203 CVC5_API_TRY_CATCH_END
;
6206 /* Create constants */
6207 /* -------------------------------------------------------------------------- */
6209 Term
Solver::mkConst(const Sort
& sort
, const std::string
& symbol
) const
6211 CVC5_API_TRY_CATCH_BEGIN
;
6212 CVC5_API_SOLVER_CHECK_SORT(sort
);
6213 //////// all checks before this line
6214 Node res
= d_nodeMgr
->mkVar(symbol
, *sort
.d_type
);
6215 (void)res
.getType(true); /* kick off type checking */
6216 increment_vars_consts_stats(sort
, false);
6217 return Term(this, res
);
6219 CVC5_API_TRY_CATCH_END
;
6222 Term
Solver::mkConst(const Sort
& sort
) const
6224 CVC5_API_TRY_CATCH_BEGIN
;
6225 CVC5_API_SOLVER_CHECK_SORT(sort
);
6226 //////// all checks before this line
6227 Node res
= d_nodeMgr
->mkVar(*sort
.d_type
);
6228 (void)res
.getType(true); /* kick off type checking */
6229 increment_vars_consts_stats(sort
, false);
6230 return Term(this, res
);
6232 CVC5_API_TRY_CATCH_END
;
6235 /* Create variables */
6236 /* -------------------------------------------------------------------------- */
6238 Term
Solver::mkVar(const Sort
& sort
, const std::string
& symbol
) const
6240 CVC5_API_TRY_CATCH_BEGIN
;
6241 CVC5_API_SOLVER_CHECK_SORT(sort
);
6242 //////// all checks before this line
6243 Node res
= symbol
.empty() ? d_nodeMgr
->mkBoundVar(*sort
.d_type
)
6244 : d_nodeMgr
->mkBoundVar(symbol
, *sort
.d_type
);
6245 (void)res
.getType(true); /* kick off type checking */
6246 increment_vars_consts_stats(sort
, true);
6247 return Term(this, res
);
6249 CVC5_API_TRY_CATCH_END
;
6252 /* Create datatype constructor declarations */
6253 /* -------------------------------------------------------------------------- */
6255 DatatypeConstructorDecl
Solver::mkDatatypeConstructorDecl(
6256 const std::string
& name
)
6258 CVC5_API_TRY_CATCH_BEGIN
;
6259 //////// all checks before this line
6260 return DatatypeConstructorDecl(this, name
);
6262 CVC5_API_TRY_CATCH_END
;
6265 /* Create datatype declarations */
6266 /* -------------------------------------------------------------------------- */
6268 DatatypeDecl
Solver::mkDatatypeDecl(const std::string
& name
, bool isCoDatatype
)
6270 CVC5_API_TRY_CATCH_BEGIN
;
6271 //////// all checks before this line
6272 return DatatypeDecl(this, name
, isCoDatatype
);
6274 CVC5_API_TRY_CATCH_END
;
6277 DatatypeDecl
Solver::mkDatatypeDecl(const std::string
& name
,
6281 CVC5_API_TRY_CATCH_BEGIN
;
6282 CVC5_API_SOLVER_CHECK_SORT(param
);
6283 //////// all checks before this line
6284 return DatatypeDecl(this, name
, param
, isCoDatatype
);
6286 CVC5_API_TRY_CATCH_END
;
6289 DatatypeDecl
Solver::mkDatatypeDecl(const std::string
& name
,
6290 const std::vector
<Sort
>& params
,
6293 CVC5_API_TRY_CATCH_BEGIN
;
6294 CVC5_API_SOLVER_CHECK_SORTS(params
);
6295 //////// all checks before this line
6296 return DatatypeDecl(this, name
, params
, isCoDatatype
);
6298 CVC5_API_TRY_CATCH_END
;
6302 /* -------------------------------------------------------------------------- */
6304 Term
Solver::mkTerm(Kind kind
) const
6306 CVC5_API_TRY_CATCH_BEGIN
;
6307 CVC5_API_KIND_CHECK(kind
);
6308 //////// all checks before this line
6309 return mkTermFromKind(kind
);
6311 CVC5_API_TRY_CATCH_END
;
6314 Term
Solver::mkTerm(Kind kind
, const Term
& child
) const
6316 CVC5_API_TRY_CATCH_BEGIN
;
6317 CVC5_API_KIND_CHECK(kind
);
6318 CVC5_API_SOLVER_CHECK_TERM(child
);
6319 //////// all checks before this line
6320 return mkTermHelper(kind
, std::vector
<Term
>{child
});
6322 CVC5_API_TRY_CATCH_END
;
6325 Term
Solver::mkTerm(Kind kind
, const Term
& child1
, const Term
& child2
) const
6327 CVC5_API_TRY_CATCH_BEGIN
;
6328 CVC5_API_KIND_CHECK(kind
);
6329 CVC5_API_SOLVER_CHECK_TERM(child1
);
6330 CVC5_API_SOLVER_CHECK_TERM(child2
);
6331 //////// all checks before this line
6332 return mkTermHelper(kind
, std::vector
<Term
>{child1
, child2
});
6334 CVC5_API_TRY_CATCH_END
;
6337 Term
Solver::mkTerm(Kind kind
,
6340 const Term
& child3
) const
6342 CVC5_API_TRY_CATCH_BEGIN
;
6343 CVC5_API_KIND_CHECK(kind
);
6344 CVC5_API_SOLVER_CHECK_TERM(child1
);
6345 CVC5_API_SOLVER_CHECK_TERM(child2
);
6346 CVC5_API_SOLVER_CHECK_TERM(child3
);
6347 //////// all checks before this line
6348 // need to use internal term call to check e.g. associative construction
6349 return mkTermHelper(kind
, std::vector
<Term
>{child1
, child2
, child3
});
6351 CVC5_API_TRY_CATCH_END
;
6354 Term
Solver::mkTerm(Kind kind
, const std::vector
<Term
>& children
) const
6356 CVC5_API_TRY_CATCH_BEGIN
;
6357 CVC5_API_KIND_CHECK(kind
);
6358 CVC5_API_SOLVER_CHECK_TERMS(children
);
6359 //////// all checks before this line
6360 return mkTermHelper(kind
, children
);
6362 CVC5_API_TRY_CATCH_END
;
6365 Term
Solver::mkTerm(const Op
& op
) const
6367 CVC5_API_TRY_CATCH_BEGIN
;
6368 CVC5_API_SOLVER_CHECK_OP(op
);
6369 if (!op
.isIndexedHelper())
6371 return mkTermFromKind(op
.d_kind
);
6373 checkMkTerm(op
.d_kind
, 0);
6374 //////// all checks before this line
6375 const cvc5::Kind int_kind
= extToIntKind(op
.d_kind
);
6376 Term res
= Term(this, getNodeManager()->mkNode(int_kind
, *op
.d_node
));
6378 (void)res
.d_node
->getType(true); /* kick off type checking */
6381 CVC5_API_TRY_CATCH_END
;
6384 Term
Solver::mkTerm(const Op
& op
, const Term
& child
) const
6386 CVC5_API_TRY_CATCH_BEGIN
;
6387 CVC5_API_SOLVER_CHECK_OP(op
);
6388 CVC5_API_SOLVER_CHECK_TERM(child
);
6389 //////// all checks before this line
6390 return mkTermHelper(op
, std::vector
<Term
>{child
});
6392 CVC5_API_TRY_CATCH_END
;
6395 Term
Solver::mkTerm(const Op
& op
, const Term
& child1
, const Term
& child2
) const
6397 CVC5_API_TRY_CATCH_BEGIN
;
6398 CVC5_API_SOLVER_CHECK_OP(op
);
6399 CVC5_API_SOLVER_CHECK_TERM(child1
);
6400 CVC5_API_SOLVER_CHECK_TERM(child2
);
6401 //////// all checks before this line
6402 return mkTermHelper(op
, std::vector
<Term
>{child1
, child2
});
6404 CVC5_API_TRY_CATCH_END
;
6407 Term
Solver::mkTerm(const Op
& op
,
6410 const Term
& child3
) const
6412 CVC5_API_TRY_CATCH_BEGIN
;
6413 CVC5_API_SOLVER_CHECK_OP(op
);
6414 CVC5_API_SOLVER_CHECK_TERM(child1
);
6415 CVC5_API_SOLVER_CHECK_TERM(child2
);
6416 CVC5_API_SOLVER_CHECK_TERM(child3
);
6417 //////// all checks before this line
6418 return mkTermHelper(op
, std::vector
<Term
>{child1
, child2
, child3
});
6420 CVC5_API_TRY_CATCH_END
;
6423 Term
Solver::mkTerm(const Op
& op
, const std::vector
<Term
>& children
) const
6425 CVC5_API_TRY_CATCH_BEGIN
;
6426 CVC5_API_SOLVER_CHECK_OP(op
);
6427 CVC5_API_SOLVER_CHECK_TERMS(children
);
6428 //////// all checks before this line
6429 return mkTermHelper(op
, children
);
6431 CVC5_API_TRY_CATCH_END
;
6434 Term
Solver::mkTuple(const std::vector
<Sort
>& sorts
,
6435 const std::vector
<Term
>& terms
) const
6437 CVC5_API_TRY_CATCH_BEGIN
;
6438 CVC5_API_CHECK(sorts
.size() == terms
.size())
6439 << "Expected the same number of sorts and elements";
6440 CVC5_API_SOLVER_CHECK_SORTS(sorts
);
6441 CVC5_API_SOLVER_CHECK_TERMS(terms
);
6442 //////// all checks before this line
6443 std::vector
<cvc5::Node
> args
;
6444 for (size_t i
= 0, size
= sorts
.size(); i
< size
; i
++)
6446 args
.push_back(*(ensureTermSort(terms
[i
], sorts
[i
])).d_node
);
6449 Sort s
= mkTupleSortHelper(sorts
);
6450 Datatype dt
= s
.getDatatype();
6451 NodeBuilder
nb(extToIntKind(APPLY_CONSTRUCTOR
));
6452 nb
<< *dt
[0].getConstructorTerm().d_node
;
6454 Node res
= nb
.constructNode();
6455 (void)res
.getType(true); /* kick off type checking */
6456 return Term(this, res
);
6458 CVC5_API_TRY_CATCH_END
;
6461 /* Create operators */
6462 /* -------------------------------------------------------------------------- */
6464 Op
Solver::mkOp(Kind kind
) const
6466 CVC5_API_TRY_CATCH_BEGIN
;
6467 CVC5_API_KIND_CHECK(kind
);
6468 CVC5_API_CHECK(s_indexed_kinds
.find(kind
) == s_indexed_kinds
.end())
6469 << "Expected a kind for a non-indexed operator.";
6470 //////// all checks before this line
6471 return Op(this, kind
);
6473 CVC5_API_TRY_CATCH_END
6476 Op
Solver::mkOp(Kind kind
, const std::string
& arg
) const
6478 CVC5_API_TRY_CATCH_BEGIN
;
6479 CVC5_API_KIND_CHECK(kind
);
6480 CVC5_API_KIND_CHECK_EXPECTED((kind
== DIVISIBLE
), kind
) << "DIVISIBLE";
6481 //////// all checks before this line
6483 /* CLN and GMP handle this case differently, CLN interprets it as 0, GMP
6484 * throws an std::invalid_argument exception. For consistency, we treat it
6486 CVC5_API_ARG_CHECK_EXPECTED(arg
!= ".", arg
)
6487 << "a string representing an integer, real or rational value.";
6490 *mkValHelper
<cvc5::Divisible
>(cvc5::Divisible(cvc5::Integer(arg
)))
6494 CVC5_API_TRY_CATCH_END
;
6497 Op
Solver::mkOp(Kind kind
, uint32_t arg
) const
6499 CVC5_API_TRY_CATCH_BEGIN
;
6500 CVC5_API_KIND_CHECK(kind
);
6501 //////// all checks before this line
6508 *mkValHelper
<cvc5::Divisible
>(cvc5::Divisible(arg
)).d_node
);
6510 case BITVECTOR_REPEAT
:
6513 *mkValHelper
<cvc5::BitVectorRepeat
>(cvc5::BitVectorRepeat(arg
))
6516 case BITVECTOR_ZERO_EXTEND
:
6519 *mkValHelper
<cvc5::BitVectorZeroExtend
>(
6520 cvc5::BitVectorZeroExtend(arg
))
6523 case BITVECTOR_SIGN_EXTEND
:
6526 *mkValHelper
<cvc5::BitVectorSignExtend
>(
6527 cvc5::BitVectorSignExtend(arg
))
6530 case BITVECTOR_ROTATE_LEFT
:
6533 *mkValHelper
<cvc5::BitVectorRotateLeft
>(
6534 cvc5::BitVectorRotateLeft(arg
))
6537 case BITVECTOR_ROTATE_RIGHT
:
6540 *mkValHelper
<cvc5::BitVectorRotateRight
>(
6541 cvc5::BitVectorRotateRight(arg
))
6544 case INT_TO_BITVECTOR
:
6548 *mkValHelper
<cvc5::IntToBitVector
>(cvc5::IntToBitVector(arg
)).d_node
);
6552 Op(this, kind
, *mkValHelper
<cvc5::IntAnd
>(cvc5::IntAnd(arg
)).d_node
);
6554 case FLOATINGPOINT_TO_UBV
:
6558 *mkValHelper
<cvc5::FloatingPointToUBV
>(cvc5::FloatingPointToUBV(arg
))
6561 case FLOATINGPOINT_TO_SBV
:
6565 *mkValHelper
<cvc5::FloatingPointToSBV
>(cvc5::FloatingPointToSBV(arg
))
6572 *mkValHelper
<cvc5::RegExpRepeat
>(cvc5::RegExpRepeat(arg
)).d_node
);
6575 CVC5_API_KIND_CHECK_EXPECTED(false, kind
)
6576 << "operator kind with uint32_t argument";
6578 Assert(!res
.isNull());
6581 CVC5_API_TRY_CATCH_END
;
6584 Op
Solver::mkOp(Kind kind
, uint32_t arg1
, uint32_t arg2
) const
6586 CVC5_API_TRY_CATCH_BEGIN
;
6587 CVC5_API_KIND_CHECK(kind
);
6588 //////// all checks before this line
6593 case BITVECTOR_EXTRACT
:
6596 *mkValHelper
<cvc5::BitVectorExtract
>(
6597 cvc5::BitVectorExtract(arg1
, arg2
))
6600 case FLOATINGPOINT_TO_FP_IEEE_BITVECTOR
:
6603 *mkValHelper
<cvc5::FloatingPointToFPIEEEBitVector
>(
6604 cvc5::FloatingPointToFPIEEEBitVector(arg1
, arg2
))
6607 case FLOATINGPOINT_TO_FP_FLOATINGPOINT
:
6610 *mkValHelper
<cvc5::FloatingPointToFPFloatingPoint
>(
6611 cvc5::FloatingPointToFPFloatingPoint(arg1
, arg2
))
6614 case FLOATINGPOINT_TO_FP_REAL
:
6617 *mkValHelper
<cvc5::FloatingPointToFPReal
>(
6618 cvc5::FloatingPointToFPReal(arg1
, arg2
))
6621 case FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR
:
6624 *mkValHelper
<cvc5::FloatingPointToFPSignedBitVector
>(
6625 cvc5::FloatingPointToFPSignedBitVector(arg1
, arg2
))
6628 case FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR
:
6631 *mkValHelper
<cvc5::FloatingPointToFPUnsignedBitVector
>(
6632 cvc5::FloatingPointToFPUnsignedBitVector(arg1
, arg2
))
6635 case FLOATINGPOINT_TO_FP_GENERIC
:
6638 *mkValHelper
<cvc5::FloatingPointToFPGeneric
>(
6639 cvc5::FloatingPointToFPGeneric(arg1
, arg2
))
6646 *mkValHelper
<cvc5::RegExpLoop
>(cvc5::RegExpLoop(arg1
, arg2
)).d_node
);
6649 CVC5_API_KIND_CHECK_EXPECTED(false, kind
)
6650 << "operator kind with two uint32_t arguments";
6652 Assert(!res
.isNull());
6655 CVC5_API_TRY_CATCH_END
;
6658 Op
Solver::mkOp(Kind kind
, const std::vector
<uint32_t>& args
) const
6660 CVC5_API_TRY_CATCH_BEGIN
;
6661 CVC5_API_KIND_CHECK(kind
);
6662 //////// all checks before this line
6671 *mkValHelper
<cvc5::TupleProjectOp
>(cvc5::TupleProjectOp(args
))
6677 std::string message
= "operator kind with " + std::to_string(args
.size())
6678 + " uint32_t arguments";
6679 CVC5_API_KIND_CHECK_EXPECTED(false, kind
) << message
;
6682 Assert(!res
.isNull());
6685 CVC5_API_TRY_CATCH_END
;
6688 /* Non-SMT-LIB commands */
6689 /* -------------------------------------------------------------------------- */
6691 Term
Solver::simplify(const Term
& term
)
6693 CVC5_API_TRY_CATCH_BEGIN
;
6694 CVC5_API_SOLVER_CHECK_TERM(term
);
6695 //////// all checks before this line
6696 return Term(this, d_slv
->simplify(*term
.d_node
));
6698 CVC5_API_TRY_CATCH_END
;
6701 Result
Solver::checkEntailed(const Term
& term
) const
6703 CVC5_API_TRY_CATCH_BEGIN
;
6704 CVC5_API_CHECK(!d_slv
->isQueryMade()
6705 || d_slv
->getOptions().base
.incrementalSolving
)
6706 << "Cannot make multiple queries unless incremental solving is enabled "
6707 "(try --incremental)";
6708 CVC5_API_SOLVER_CHECK_TERM(term
);
6709 //////// all checks before this line
6710 return d_slv
->checkEntailed(*term
.d_node
);
6712 CVC5_API_TRY_CATCH_END
;
6715 Result
Solver::checkEntailed(const std::vector
<Term
>& terms
) const
6717 CVC5_API_TRY_CATCH_BEGIN
;
6718 CVC5_API_CHECK(!d_slv
->isQueryMade()
6719 || d_slv
->getOptions().base
.incrementalSolving
)
6720 << "Cannot make multiple queries unless incremental solving is enabled "
6721 "(try --incremental)";
6722 CVC5_API_SOLVER_CHECK_TERMS(terms
);
6723 //////// all checks before this line
6724 return d_slv
->checkEntailed(Term::termVectorToNodes(terms
));
6726 CVC5_API_TRY_CATCH_END
;
6729 /* SMT-LIB commands */
6730 /* -------------------------------------------------------------------------- */
6732 void Solver::assertFormula(const Term
& term
) const
6734 CVC5_API_TRY_CATCH_BEGIN
;
6735 CVC5_API_SOLVER_CHECK_TERM(term
);
6736 CVC5_API_SOLVER_CHECK_TERM_WITH_SORT(term
, getBooleanSort());
6737 //////// all checks before this line
6738 d_slv
->assertFormula(*term
.d_node
);
6740 CVC5_API_TRY_CATCH_END
;
6743 Result
Solver::checkSat(void) const
6745 CVC5_API_TRY_CATCH_BEGIN
;
6746 CVC5_API_CHECK(!d_slv
->isQueryMade()
6747 || d_slv
->getOptions().base
.incrementalSolving
)
6748 << "Cannot make multiple queries unless incremental solving is enabled "
6749 "(try --incremental)";
6750 //////// all checks before this line
6751 return d_slv
->checkSat();
6753 CVC5_API_TRY_CATCH_END
;
6756 Result
Solver::checkSatAssuming(const Term
& assumption
) const
6758 CVC5_API_TRY_CATCH_BEGIN
;
6759 CVC5_API_CHECK(!d_slv
->isQueryMade()
6760 || d_slv
->getOptions().base
.incrementalSolving
)
6761 << "Cannot make multiple queries unless incremental solving is enabled "
6762 "(try --incremental)";
6763 CVC5_API_SOLVER_CHECK_TERM_WITH_SORT(assumption
, getBooleanSort());
6764 //////// all checks before this line
6765 return d_slv
->checkSat(*assumption
.d_node
);
6767 CVC5_API_TRY_CATCH_END
;
6770 Result
Solver::checkSatAssuming(const std::vector
<Term
>& assumptions
) const
6772 CVC5_API_TRY_CATCH_BEGIN
;
6773 CVC5_API_CHECK(!d_slv
->isQueryMade() || assumptions
.size() == 0
6774 || d_slv
->getOptions().base
.incrementalSolving
)
6775 << "Cannot make multiple queries unless incremental solving is enabled "
6776 "(try --incremental)";
6777 CVC5_API_SOLVER_CHECK_TERMS_WITH_SORT(assumptions
, getBooleanSort());
6778 //////// all checks before this line
6779 for (const Term
& term
: assumptions
)
6781 CVC5_API_SOLVER_CHECK_TERM(term
);
6783 std::vector
<Node
> eassumptions
= Term::termVectorToNodes(assumptions
);
6784 return d_slv
->checkSat(eassumptions
);
6786 CVC5_API_TRY_CATCH_END
;
6789 Sort
Solver::declareDatatype(
6790 const std::string
& symbol
,
6791 const std::vector
<DatatypeConstructorDecl
>& ctors
) const
6793 CVC5_API_TRY_CATCH_BEGIN
;
6794 CVC5_API_ARG_CHECK_EXPECTED(ctors
.size() > 0, ctors
)
6795 << "a datatype declaration with at least one constructor";
6796 CVC5_API_SOLVER_CHECK_DTCTORDECLS(ctors
);
6797 for (size_t i
= 0, size
= ctors
.size(); i
< size
; i
++)
6799 CVC5_API_CHECK(!ctors
[i
].isResolved())
6800 << "cannot use a constructor for multiple datatypes";
6802 //////// all checks before this line
6803 DatatypeDecl
dtdecl(this, symbol
);
6804 for (size_t i
= 0, size
= ctors
.size(); i
< size
; i
++)
6806 dtdecl
.addConstructor(ctors
[i
]);
6808 return Sort(this, getNodeManager()->mkDatatypeType(*dtdecl
.d_dtype
));
6810 CVC5_API_TRY_CATCH_END
;
6813 Term
Solver::declareFun(const std::string
& symbol
,
6814 const std::vector
<Sort
>& sorts
,
6815 const Sort
& sort
) const
6817 CVC5_API_TRY_CATCH_BEGIN
;
6818 CVC5_API_SOLVER_CHECK_DOMAIN_SORTS(sorts
);
6819 CVC5_API_SOLVER_CHECK_CODOMAIN_SORT(sort
);
6820 //////// all checks before this line
6822 TypeNode type
= *sort
.d_type
;
6825 std::vector
<TypeNode
> types
= Sort::sortVectorToTypeNodes(sorts
);
6826 type
= getNodeManager()->mkFunctionType(types
, type
);
6828 return Term(this, d_nodeMgr
->mkVar(symbol
, type
));
6830 CVC5_API_TRY_CATCH_END
;
6833 Sort
Solver::declareSort(const std::string
& symbol
, uint32_t arity
) const
6835 CVC5_API_TRY_CATCH_BEGIN
;
6836 //////// all checks before this line
6839 return Sort(this, getNodeManager()->mkSort(symbol
));
6841 return Sort(this, getNodeManager()->mkSortConstructor(symbol
, arity
));
6843 CVC5_API_TRY_CATCH_END
;
6846 Term
Solver::defineFun(const std::string
& symbol
,
6847 const std::vector
<Term
>& bound_vars
,
6852 CVC5_API_TRY_CATCH_BEGIN
;
6853 CVC5_API_SOLVER_CHECK_CODOMAIN_SORT(sort
);
6854 CVC5_API_SOLVER_CHECK_TERM(term
);
6855 CVC5_API_CHECK(term
.getSort().isSubsortOf(sort
))
6856 << "Invalid sort of function body '" << term
<< "', expected '" << sort
6859 std::vector
<Sort
> domain_sorts
;
6860 for (const auto& bv
: bound_vars
)
6862 domain_sorts
.push_back(bv
.getSort());
6865 domain_sorts
.empty()
6868 getNodeManager()->mkFunctionType(
6869 Sort::sortVectorToTypeNodes(domain_sorts
), *sort
.d_type
));
6870 Term fun
= mkConst(fun_sort
, symbol
);
6872 CVC5_API_SOLVER_CHECK_BOUND_VARS_DEF_FUN(fun
, bound_vars
, domain_sorts
);
6873 //////// all checks before this line
6875 d_slv
->defineFunction(
6876 *fun
.d_node
, Term::termVectorToNodes(bound_vars
), *term
.d_node
, global
);
6879 CVC5_API_TRY_CATCH_END
;
6882 Term
Solver::defineFunRec(const std::string
& symbol
,
6883 const std::vector
<Term
>& bound_vars
,
6888 CVC5_API_TRY_CATCH_BEGIN
;
6890 CVC5_API_CHECK(d_slv
->getUserLogicInfo().isQuantified())
6891 << "recursive function definitions require a logic with quantifiers";
6892 CVC5_API_CHECK(d_slv
->getUserLogicInfo().isTheoryEnabled(theory::THEORY_UF
))
6893 << "recursive function definitions require a logic with uninterpreted "
6896 CVC5_API_SOLVER_CHECK_TERM(term
);
6897 CVC5_API_SOLVER_CHECK_CODOMAIN_SORT(sort
);
6898 CVC5_API_CHECK(sort
== term
.getSort())
6899 << "Invalid sort of function body '" << term
<< "', expected '" << sort
6902 std::vector
<Sort
> domain_sorts
;
6903 for (const auto& bv
: bound_vars
)
6905 domain_sorts
.push_back(bv
.getSort());
6908 domain_sorts
.empty()
6911 getNodeManager()->mkFunctionType(
6912 Sort::sortVectorToTypeNodes(domain_sorts
), *sort
.d_type
));
6913 Term fun
= mkConst(fun_sort
, symbol
);
6915 CVC5_API_SOLVER_CHECK_BOUND_VARS_DEF_FUN(fun
, bound_vars
, domain_sorts
);
6916 //////// all checks before this line
6918 d_slv
->defineFunctionRec(
6919 *fun
.d_node
, Term::termVectorToNodes(bound_vars
), *term
.d_node
, global
);
6923 CVC5_API_TRY_CATCH_END
;
6926 Term
Solver::defineFunRec(const Term
& fun
,
6927 const std::vector
<Term
>& bound_vars
,
6931 CVC5_API_TRY_CATCH_BEGIN
;
6933 CVC5_API_CHECK(d_slv
->getUserLogicInfo().isQuantified())
6934 << "recursive function definitions require a logic with quantifiers";
6935 CVC5_API_CHECK(d_slv
->getUserLogicInfo().isTheoryEnabled(theory::THEORY_UF
))
6936 << "recursive function definitions require a logic with uninterpreted "
6939 CVC5_API_SOLVER_CHECK_TERM(fun
);
6940 CVC5_API_SOLVER_CHECK_TERM(term
);
6941 if (fun
.getSort().isFunction())
6943 std::vector
<Sort
> domain_sorts
= fun
.getSort().getFunctionDomainSorts();
6944 CVC5_API_SOLVER_CHECK_BOUND_VARS_DEF_FUN(fun
, bound_vars
, domain_sorts
);
6945 Sort codomain
= fun
.getSort().getFunctionCodomainSort();
6946 CVC5_API_CHECK(codomain
== term
.getSort())
6947 << "Invalid sort of function body '" << term
<< "', expected '"
6952 CVC5_API_SOLVER_CHECK_BOUND_VARS(bound_vars
);
6953 CVC5_API_ARG_CHECK_EXPECTED(bound_vars
.size() == 0, fun
)
6954 << "function or nullary symbol";
6956 //////// all checks before this line
6958 std::vector
<Node
> ebound_vars
= Term::termVectorToNodes(bound_vars
);
6959 d_slv
->defineFunctionRec(*fun
.d_node
, ebound_vars
, *term
.d_node
, global
);
6962 CVC5_API_TRY_CATCH_END
;
6965 void Solver::defineFunsRec(const std::vector
<Term
>& funs
,
6966 const std::vector
<std::vector
<Term
>>& bound_vars
,
6967 const std::vector
<Term
>& terms
,
6970 CVC5_API_TRY_CATCH_BEGIN
;
6972 CVC5_API_CHECK(d_slv
->getUserLogicInfo().isQuantified())
6973 << "recursive function definitions require a logic with quantifiers";
6974 CVC5_API_CHECK(d_slv
->getUserLogicInfo().isTheoryEnabled(theory::THEORY_UF
))
6975 << "recursive function definitions require a logic with uninterpreted "
6977 CVC5_API_SOLVER_CHECK_TERMS(funs
);
6978 CVC5_API_SOLVER_CHECK_TERMS(terms
);
6980 size_t funs_size
= funs
.size();
6981 CVC5_API_ARG_SIZE_CHECK_EXPECTED(funs_size
== bound_vars
.size(), bound_vars
)
6982 << "'" << funs_size
<< "'";
6983 CVC5_API_ARG_SIZE_CHECK_EXPECTED(funs_size
== terms
.size(), terms
)
6984 << "'" << funs_size
<< "'";
6986 for (size_t j
= 0; j
< funs_size
; ++j
)
6988 const Term
& fun
= funs
[j
];
6989 const std::vector
<Term
>& bvars
= bound_vars
[j
];
6990 const Term
& term
= terms
[j
];
6992 CVC5_API_ARG_AT_INDEX_CHECK_EXPECTED(
6993 this == fun
.d_solver
, "function", funs
, j
)
6994 << "function associated with this solver object";
6995 CVC5_API_ARG_AT_INDEX_CHECK_EXPECTED(
6996 this == term
.d_solver
, "term", terms
, j
)
6997 << "term associated with this solver object";
6999 if (fun
.getSort().isFunction())
7001 std::vector
<Sort
> domain_sorts
= fun
.getSort().getFunctionDomainSorts();
7002 CVC5_API_SOLVER_CHECK_BOUND_VARS_DEF_FUN(fun
, bvars
, domain_sorts
);
7003 Sort codomain
= fun
.getSort().getFunctionCodomainSort();
7004 CVC5_API_ARG_AT_INDEX_CHECK_EXPECTED(
7005 codomain
== term
.getSort(), "sort of function body", terms
, j
)
7006 << "'" << codomain
<< "'";
7010 CVC5_API_SOLVER_CHECK_BOUND_VARS(bvars
);
7011 CVC5_API_ARG_CHECK_EXPECTED(bvars
.size() == 0, fun
)
7012 << "function or nullary symbol";
7015 //////// all checks before this line
7016 std::vector
<Node
> efuns
= Term::termVectorToNodes(funs
);
7017 std::vector
<std::vector
<Node
>> ebound_vars
;
7018 for (const auto& v
: bound_vars
)
7020 ebound_vars
.push_back(Term::termVectorToNodes(v
));
7022 std::vector
<Node
> nodes
= Term::termVectorToNodes(terms
);
7023 d_slv
->defineFunctionsRec(efuns
, ebound_vars
, nodes
, global
);
7025 CVC5_API_TRY_CATCH_END
;
7028 void Solver::echo(std::ostream
& out
, const std::string
& str
) const
7033 std::vector
<Term
> Solver::getAssertions(void) const
7035 CVC5_API_TRY_CATCH_BEGIN
;
7036 //////// all checks before this line
7037 std::vector
<Node
> assertions
= d_slv
->getAssertions();
7039 * return std::vector<Term>(assertions.begin(), assertions.end());
7040 * here since constructor is private */
7041 std::vector
<Term
> res
;
7042 for (const Node
& e
: assertions
)
7044 res
.push_back(Term(this, e
));
7048 CVC5_API_TRY_CATCH_END
;
7051 std::string
Solver::getInfo(const std::string
& flag
) const
7053 CVC5_API_TRY_CATCH_BEGIN
;
7054 CVC5_API_UNSUPPORTED_CHECK(d_slv
->isValidGetInfoFlag(flag
))
7055 << "Unrecognized flag: " << flag
<< ".";
7056 //////// all checks before this line
7057 return d_slv
->getInfo(flag
);
7059 CVC5_API_TRY_CATCH_END
;
7062 std::string
Solver::getOption(const std::string
& option
) const
7066 return d_slv
->getOption(option
);
7068 catch (OptionException
& e
)
7070 throw CVC5ApiUnsupportedException(e
.getMessage());
7074 // Supports a visitor from a list of lambdas
7075 // Taken from https://en.cppreference.com/w/cpp/utility/variant/visit
7076 template<class... Ts
> struct overloaded
: Ts
... { using Ts::operator()...; };
7077 template<class... Ts
> overloaded(Ts
...) -> overloaded
<Ts
...>;
7079 bool OptionInfo::boolValue() const
7081 CVC5_API_TRY_CATCH_BEGIN
;
7082 CVC5_API_RECOVERABLE_CHECK(std::holds_alternative
<ValueInfo
<bool>>(valueInfo
))
7083 << name
<< " is not a bool option";
7084 //////// all checks before this line
7085 return std::get
<ValueInfo
<bool>>(valueInfo
).currentValue
;
7087 CVC5_API_TRY_CATCH_END
;
7089 std::string
OptionInfo::stringValue() const
7091 CVC5_API_TRY_CATCH_BEGIN
;
7092 CVC5_API_RECOVERABLE_CHECK(
7093 std::holds_alternative
<ValueInfo
<std::string
>>(valueInfo
))
7094 << name
<< " is not a string option";
7095 //////// all checks before this line
7096 return std::get
<ValueInfo
<std::string
>>(valueInfo
).currentValue
;
7098 CVC5_API_TRY_CATCH_END
;
7100 int64_t OptionInfo::intValue() const
7102 CVC5_API_TRY_CATCH_BEGIN
;
7103 CVC5_API_RECOVERABLE_CHECK(
7104 std::holds_alternative
<NumberInfo
<int64_t>>(valueInfo
))
7105 << name
<< " is not an int option";
7106 //////// all checks before this line
7107 return std::get
<NumberInfo
<int64_t>>(valueInfo
).currentValue
;
7109 CVC5_API_TRY_CATCH_END
;
7111 uint64_t OptionInfo::uintValue() const
7113 CVC5_API_TRY_CATCH_BEGIN
;
7114 CVC5_API_RECOVERABLE_CHECK(
7115 std::holds_alternative
<NumberInfo
<uint64_t>>(valueInfo
))
7116 << name
<< " is not a uint option";
7117 //////// all checks before this line
7118 return std::get
<NumberInfo
<uint64_t>>(valueInfo
).currentValue
;
7120 CVC5_API_TRY_CATCH_END
;
7122 double OptionInfo::doubleValue() const
7124 CVC5_API_TRY_CATCH_BEGIN
;
7125 CVC5_API_RECOVERABLE_CHECK(
7126 std::holds_alternative
<NumberInfo
<double>>(valueInfo
))
7127 << name
<< " is not a double option";
7128 //////// all checks before this line
7129 return std::get
<NumberInfo
<double>>(valueInfo
).currentValue
;
7131 CVC5_API_TRY_CATCH_END
;
7134 std::ostream
& operator<<(std::ostream
& os
, const OptionInfo
& oi
)
7136 os
<< "OptionInfo{ " << oi
.name
;
7139 os
<< " | set by user";
7141 if (!oi
.aliases
.empty())
7143 container_to_stream(os
, oi
.aliases
, ", ", "", ", ");
7145 auto printNum
= [&os
](const std::string
& type
, const auto& vi
) {
7146 os
<< " | " << type
<< " | " << vi
.currentValue
<< " | default "
7148 if (vi
.minimum
|| vi
.maximum
)
7153 os
<< " " << *vi
.minimum
<< " <=";
7158 os
<< " <= " << *vi
.maximum
;
7162 std::visit(overloaded
{
7163 [&os
](const OptionInfo::VoidInfo
& vi
) { os
<< " | void"; },
7164 [&os
](const OptionInfo::ValueInfo
<bool>& vi
) {
7165 os
<< " | bool | " << vi
.currentValue
<< " | default "
7168 [&os
](const OptionInfo::ValueInfo
<std::string
>& vi
) {
7169 os
<< " | string | " << vi
.currentValue
<< " | default "
7172 [&printNum
](const OptionInfo::NumberInfo
<int64_t>& vi
) {
7173 printNum("int64_t", vi
);
7175 [&printNum
](const OptionInfo::NumberInfo
<uint64_t>& vi
) {
7176 printNum("uint64_t", vi
);
7178 [&printNum
](const OptionInfo::NumberInfo
<double>& vi
) {
7179 printNum("double", vi
);
7181 [&os
](const OptionInfo::ModeInfo
& vi
) {
7182 os
<< " | mode | " << vi
.currentValue
<< " | default "
7183 << vi
.defaultValue
<< " | modes: ";
7184 container_to_stream(os
, vi
.modes
, "", "", ", ");
7192 std::vector
<std::string
> Solver::getOptionNames() const
7194 CVC5_API_TRY_CATCH_BEGIN
;
7195 //////// all checks before this line
7196 return options::getNames();
7198 CVC5_API_TRY_CATCH_END
;
7201 OptionInfo
Solver::getOptionInfo(const std::string
& option
) const
7203 CVC5_API_TRY_CATCH_BEGIN
;
7204 //////// all checks before this line
7205 auto info
= options::getInfo(d_slv
->getOptions(), option
);
7206 CVC5_API_CHECK(info
.name
!= "")
7207 << "Querying invalid or unknown option " << option
;
7210 [&info
](const options::OptionInfo::VoidInfo
& vi
) {
7211 return OptionInfo
{info
.name
,
7214 OptionInfo::VoidInfo
{}};
7216 [&info
](const options::OptionInfo::ValueInfo
<bool>& vi
) {
7221 OptionInfo::ValueInfo
<bool>{vi
.defaultValue
, vi
.currentValue
}};
7223 [&info
](const options::OptionInfo::ValueInfo
<std::string
>& vi
) {
7224 return OptionInfo
{info
.name
,
7227 OptionInfo::ValueInfo
<std::string
>{
7228 vi
.defaultValue
, vi
.currentValue
}};
7230 [&info
](const options::OptionInfo::NumberInfo
<int64_t>& vi
) {
7235 OptionInfo::NumberInfo
<int64_t>{
7236 vi
.defaultValue
, vi
.currentValue
, vi
.minimum
, vi
.maximum
}};
7238 [&info
](const options::OptionInfo::NumberInfo
<uint64_t>& vi
) {
7243 OptionInfo::NumberInfo
<uint64_t>{
7244 vi
.defaultValue
, vi
.currentValue
, vi
.minimum
, vi
.maximum
}};
7246 [&info
](const options::OptionInfo::NumberInfo
<double>& vi
) {
7251 OptionInfo::NumberInfo
<double>{
7252 vi
.defaultValue
, vi
.currentValue
, vi
.minimum
, vi
.maximum
}};
7254 [&info
](const options::OptionInfo::ModeInfo
& vi
) {
7255 return OptionInfo
{info
.name
,
7258 OptionInfo::ModeInfo
{
7259 vi
.defaultValue
, vi
.currentValue
, vi
.modes
}};
7264 CVC5_API_TRY_CATCH_END
;
7267 DriverOptions
Solver::getDriverOptions() const { return DriverOptions(*this); }
7269 std::vector
<Term
> Solver::getUnsatAssumptions(void) const
7271 CVC5_API_TRY_CATCH_BEGIN
;
7272 CVC5_API_CHECK(d_slv
->getOptions().base
.incrementalSolving
)
7273 << "Cannot get unsat assumptions unless incremental solving is enabled "
7274 "(try --incremental)";
7275 CVC5_API_CHECK(d_slv
->getOptions().smt
.unsatAssumptions
)
7276 << "Cannot get unsat assumptions unless explicitly enabled "
7277 "(try --produce-unsat-assumptions)";
7278 CVC5_API_CHECK(d_slv
->getSmtMode() == SmtMode::UNSAT
)
7279 << "Cannot get unsat assumptions unless in unsat mode.";
7280 //////// all checks before this line
7282 std::vector
<Node
> uassumptions
= d_slv
->getUnsatAssumptions();
7284 * return std::vector<Term>(uassumptions.begin(), uassumptions.end());
7285 * here since constructor is private */
7286 std::vector
<Term
> res
;
7287 for (const Node
& n
: uassumptions
)
7289 res
.push_back(Term(this, n
));
7293 CVC5_API_TRY_CATCH_END
;
7296 std::vector
<Term
> Solver::getUnsatCore(void) const
7298 CVC5_API_TRY_CATCH_BEGIN
;
7299 CVC5_API_CHECK(d_slv
->getOptions().smt
.unsatCores
)
7300 << "Cannot get unsat core unless explicitly enabled "
7301 "(try --produce-unsat-cores)";
7302 CVC5_API_RECOVERABLE_CHECK(d_slv
->getSmtMode() == SmtMode::UNSAT
)
7303 << "Cannot get unsat core unless in unsat mode.";
7304 //////// all checks before this line
7305 UnsatCore core
= d_slv
->getUnsatCore();
7307 * return std::vector<Term>(core.begin(), core.end());
7308 * here since constructor is private */
7309 std::vector
<Term
> res
;
7310 for (const Node
& e
: core
)
7312 res
.push_back(Term(this, e
));
7316 CVC5_API_TRY_CATCH_END
;
7319 std::map
<Term
, Term
> Solver::getDifficulty() const
7321 CVC5_API_TRY_CATCH_BEGIN
;
7322 CVC5_API_RECOVERABLE_CHECK(d_slv
->getSmtMode() == SmtMode::UNSAT
7323 || d_slv
->getSmtMode() == SmtMode::SAT
7324 || d_slv
->getSmtMode() == SmtMode::SAT_UNKNOWN
)
7325 << "Cannot get difficulty unless after a UNSAT, SAT or UNKNOWN response.";
7326 //////// all checks before this line
7327 std::map
<Term
, Term
> res
;
7328 std::map
<Node
, Node
> dmap
;
7329 d_slv
->getDifficultyMap(dmap
);
7330 for (const std::pair
<const Node
, Node
>& d
: dmap
)
7332 res
[Term(this, d
.first
)] = Term(this, d
.second
);
7336 CVC5_API_TRY_CATCH_END
;
7339 std::string
Solver::getProof(void) const
7341 CVC5_API_TRY_CATCH_BEGIN
;
7342 CVC5_API_CHECK(d_slv
->getOptions().smt
.produceProofs
)
7343 << "Cannot get proof unless proofs are enabled (try --produce-proofs)";
7344 CVC5_API_RECOVERABLE_CHECK(d_slv
->getSmtMode() == SmtMode::UNSAT
)
7345 << "Cannot get proof unless in unsat mode.";
7346 return d_slv
->getProof();
7347 CVC5_API_TRY_CATCH_END
;
7350 Term
Solver::getValue(const Term
& term
) const
7352 CVC5_API_TRY_CATCH_BEGIN
;
7353 CVC5_API_RECOVERABLE_CHECK(d_slv
->getOptions().smt
.produceModels
)
7354 << "Cannot get value unless model generation is enabled "
7355 "(try --produce-models)";
7356 CVC5_API_RECOVERABLE_CHECK(d_slv
->isSmtModeSat())
7357 << "Cannot get value unless after a SAT or UNKNOWN response.";
7358 CVC5_API_SOLVER_CHECK_TERM(term
);
7359 CVC5_API_RECOVERABLE_CHECK(term
.getSort().isFirstClass())
7360 << "Cannot get value of a term that is not first class.";
7361 CVC5_API_RECOVERABLE_CHECK(!term
.getSort().isDatatype()
7362 || term
.getSort().getDatatype().isWellFounded())
7363 << "Cannot get value of a term of non-well-founded datatype sort.";
7364 //////// all checks before this line
7365 return getValueHelper(term
);
7367 CVC5_API_TRY_CATCH_END
;
7370 std::vector
<Term
> Solver::getValue(const std::vector
<Term
>& terms
) const
7372 CVC5_API_TRY_CATCH_BEGIN
;
7373 CVC5_API_RECOVERABLE_CHECK(d_slv
->getOptions().smt
.produceModels
)
7374 << "Cannot get value unless model generation is enabled "
7375 "(try --produce-models)";
7376 CVC5_API_RECOVERABLE_CHECK(d_slv
->isSmtModeSat())
7377 << "Cannot get value unless after a SAT or UNKNOWN response.";
7378 for (const Term
& t
: terms
)
7380 CVC5_API_RECOVERABLE_CHECK(t
.getSort().isFirstClass())
7381 << "Cannot get value of a term that is not first class.";
7382 CVC5_API_RECOVERABLE_CHECK(!t
.getSort().isDatatype()
7383 || t
.getSort().getDatatype().isWellFounded())
7384 << "Cannot get value of a term of non-well-founded datatype sort.";
7386 CVC5_API_SOLVER_CHECK_TERMS(terms
);
7387 //////// all checks before this line
7389 std::vector
<Term
> res
;
7390 for (size_t i
= 0, n
= terms
.size(); i
< n
; ++i
)
7392 /* Can not use emplace_back here since constructor is private. */
7393 res
.push_back(getValueHelper(terms
[i
]));
7397 CVC5_API_TRY_CATCH_END
;
7400 std::vector
<Term
> Solver::getModelDomainElements(const Sort
& s
) const
7402 CVC5_API_TRY_CATCH_BEGIN
;
7403 CVC5_API_RECOVERABLE_CHECK(d_slv
->getOptions().smt
.produceModels
)
7404 << "Cannot get domain elements unless model generation is enabled "
7405 "(try --produce-models)";
7406 CVC5_API_RECOVERABLE_CHECK(d_slv
->isSmtModeSat())
7407 << "Cannot get domain elements unless after a SAT or UNKNOWN response.";
7408 CVC5_API_SOLVER_CHECK_SORT(s
);
7409 CVC5_API_RECOVERABLE_CHECK(s
.isUninterpretedSort())
7410 << "Expecting an uninterpreted sort as argument to "
7411 "getModelDomainElements.";
7412 //////// all checks before this line
7413 std::vector
<Term
> res
;
7414 std::vector
<Node
> elements
= d_slv
->getModelDomainElements(s
.getTypeNode());
7415 for (const Node
& n
: elements
)
7417 res
.push_back(Term(this, n
));
7421 CVC5_API_TRY_CATCH_END
;
7424 bool Solver::isModelCoreSymbol(const Term
& v
) const
7426 CVC5_API_TRY_CATCH_BEGIN
;
7427 CVC5_API_RECOVERABLE_CHECK(d_slv
->getOptions().smt
.produceModels
)
7428 << "Cannot check if model core symbol unless model generation is enabled "
7429 "(try --produce-models)";
7430 CVC5_API_RECOVERABLE_CHECK(d_slv
->isSmtModeSat())
7431 << "Cannot check if model core symbol unless after a SAT or UNKNOWN "
7433 CVC5_API_SOLVER_CHECK_TERM(v
);
7434 CVC5_API_RECOVERABLE_CHECK(v
.getKind() == CONSTANT
)
7435 << "Expecting a free constant as argument to isModelCoreSymbol.";
7436 //////// all checks before this line
7437 return d_slv
->isModelCoreSymbol(v
.getNode());
7439 CVC5_API_TRY_CATCH_END
;
7442 std::string
Solver::getModel(const std::vector
<Sort
>& sorts
,
7443 const std::vector
<Term
>& vars
) const
7445 CVC5_API_TRY_CATCH_BEGIN
;
7446 CVC5_API_RECOVERABLE_CHECK(d_slv
->getOptions().smt
.produceModels
)
7447 << "Cannot get model unless model generation is enabled "
7448 "(try --produce-models)";
7449 CVC5_API_RECOVERABLE_CHECK(d_slv
->isSmtModeSat())
7450 << "Cannot get model unless after a SAT or UNKNOWN response.";
7451 CVC5_API_SOLVER_CHECK_SORTS(sorts
);
7452 for (const Sort
& s
: sorts
)
7454 CVC5_API_RECOVERABLE_CHECK(s
.isUninterpretedSort())
7455 << "Expecting an uninterpreted sort as argument to "
7458 CVC5_API_SOLVER_CHECK_TERMS(vars
);
7459 for (const Term
& v
: vars
)
7461 CVC5_API_RECOVERABLE_CHECK(v
.getKind() == CONSTANT
)
7462 << "Expecting a free constant as argument to getModel.";
7464 //////// all checks before this line
7465 return d_slv
->getModel(Sort::sortVectorToTypeNodes(sorts
),
7466 Term::termVectorToNodes(vars
));
7468 CVC5_API_TRY_CATCH_END
;
7471 Term
Solver::getQuantifierElimination(const Term
& q
) const
7473 CVC5_API_TRY_CATCH_BEGIN
;
7474 CVC5_API_SOLVER_CHECK_TERM(q
);
7475 //////// all checks before this line
7476 return Term(this, d_slv
->getQuantifierElimination(q
.getNode(), true, true));
7478 CVC5_API_TRY_CATCH_END
;
7481 Term
Solver::getQuantifierEliminationDisjunct(const Term
& q
) const
7483 CVC5_API_TRY_CATCH_BEGIN
;
7484 CVC5_API_SOLVER_CHECK_TERM(q
);
7485 //////// all checks before this line
7486 return Term(this, d_slv
->getQuantifierElimination(q
.getNode(), false, true));
7488 CVC5_API_TRY_CATCH_END
;
7491 void Solver::declareSepHeap(const Sort
& locSort
, const Sort
& dataSort
) const
7493 CVC5_API_TRY_CATCH_BEGIN
;
7494 CVC5_API_SOLVER_CHECK_SORT(locSort
);
7495 CVC5_API_SOLVER_CHECK_SORT(dataSort
);
7496 CVC5_API_CHECK(d_slv
->getLogicInfo().isTheoryEnabled(theory::THEORY_SEP
))
7497 << "Cannot obtain separation logic expressions if not using the "
7498 "separation logic theory.";
7499 //////// all checks before this line
7500 d_slv
->declareSepHeap(locSort
.getTypeNode(), dataSort
.getTypeNode());
7502 CVC5_API_TRY_CATCH_END
;
7505 Term
Solver::getValueSepHeap() const
7507 CVC5_API_TRY_CATCH_BEGIN
;
7508 CVC5_API_CHECK(d_slv
->getLogicInfo().isTheoryEnabled(theory::THEORY_SEP
))
7509 << "Cannot obtain separation logic expressions if not using the "
7510 "separation logic theory.";
7511 CVC5_API_CHECK(d_slv
->getOptions().smt
.produceModels
)
7512 << "Cannot get separation heap term unless model generation is enabled "
7513 "(try --produce-models)";
7514 CVC5_API_RECOVERABLE_CHECK(d_slv
->isSmtModeSat())
7515 << "Can only get separtion heap term after SAT or UNKNOWN response.";
7516 //////// all checks before this line
7517 return Term(this, d_slv
->getSepHeapExpr());
7519 CVC5_API_TRY_CATCH_END
;
7522 Term
Solver::getValueSepNil() const
7524 CVC5_API_TRY_CATCH_BEGIN
;
7525 CVC5_API_CHECK(d_slv
->getLogicInfo().isTheoryEnabled(theory::THEORY_SEP
))
7526 << "Cannot obtain separation logic expressions if not using the "
7527 "separation logic theory.";
7528 CVC5_API_CHECK(d_slv
->getOptions().smt
.produceModels
)
7529 << "Cannot get separation nil term unless model generation is enabled "
7530 "(try --produce-models)";
7531 CVC5_API_RECOVERABLE_CHECK(d_slv
->isSmtModeSat())
7532 << "Can only get separtion nil term after SAT or UNKNOWN response.";
7533 //////// all checks before this line
7534 return Term(this, d_slv
->getSepNilExpr());
7536 CVC5_API_TRY_CATCH_END
;
7539 Term
Solver::declarePool(const std::string
& symbol
,
7541 const std::vector
<Term
>& initValue
) const
7543 CVC5_API_TRY_CATCH_BEGIN
;
7544 CVC5_API_SOLVER_CHECK_SORT(sort
);
7545 CVC5_API_SOLVER_CHECK_TERMS(initValue
);
7546 //////// all checks before this line
7547 TypeNode setType
= getNodeManager()->mkSetType(*sort
.d_type
);
7548 Node pool
= getNodeManager()->mkBoundVar(symbol
, setType
);
7549 std::vector
<Node
> initv
= Term::termVectorToNodes(initValue
);
7550 d_slv
->declarePool(pool
, initv
);
7551 return Term(this, pool
);
7553 CVC5_API_TRY_CATCH_END
;
7556 void Solver::pop(uint32_t nscopes
) const
7558 CVC5_API_TRY_CATCH_BEGIN
;
7559 CVC5_API_CHECK(d_slv
->getOptions().base
.incrementalSolving
)
7560 << "Cannot pop when not solving incrementally (use --incremental)";
7561 CVC5_API_CHECK(nscopes
<= d_slv
->getNumUserLevels())
7562 << "Cannot pop beyond first pushed context";
7563 //////// all checks before this line
7564 for (uint32_t n
= 0; n
< nscopes
; ++n
)
7569 CVC5_API_TRY_CATCH_END
;
7572 bool Solver::getInterpolant(const Term
& conj
, Term
& output
) const
7574 CVC5_API_TRY_CATCH_BEGIN
;
7575 CVC5_API_SOLVER_CHECK_TERM(conj
);
7576 CVC5_API_CHECK(d_slv
->getOptions().smt
.produceInterpols
7577 != options::ProduceInterpols::NONE
)
7578 << "Cannot get interpolant unless interpolants are enabled (try "
7579 "--produce-interpols=mode)";
7580 //////// all checks before this line
7583 bool success
= d_slv
->getInterpolant(*conj
.d_node
, nullType
, result
);
7586 output
= Term(this, result
);
7590 CVC5_API_TRY_CATCH_END
;
7593 bool Solver::getInterpolant(const Term
& conj
,
7597 CVC5_API_TRY_CATCH_BEGIN
;
7598 CVC5_API_SOLVER_CHECK_TERM(conj
);
7599 CVC5_API_CHECK(d_slv
->getOptions().smt
.produceInterpols
7600 != options::ProduceInterpols::NONE
)
7601 << "Cannot get interpolant unless interpolants are enabled (try "
7602 "--produce-interpols=mode)";
7603 //////// all checks before this line
7606 d_slv
->getInterpolant(*conj
.d_node
, *grammar
.resolve().d_type
, result
);
7609 output
= Term(this, result
);
7613 CVC5_API_TRY_CATCH_END
;
7616 bool Solver::getInterpolantNext(Term
& output
) const
7618 CVC5_API_TRY_CATCH_BEGIN
;
7619 CVC5_API_CHECK(d_slv
->getOptions().smt
.produceInterpols
7620 != options::ProduceInterpols::NONE
)
7621 << "Cannot get interpolant unless interpolants are enabled (try "
7622 "--produce-interpols=mode)";
7623 CVC5_API_CHECK(d_slv
->getOptions().base
.incrementalSolving
)
7624 << "Cannot get next interpolant when not solving incrementally (try "
7626 //////// all checks before this line
7628 bool success
= d_slv
->getInterpolantNext(result
);
7631 output
= Term(this, result
);
7635 CVC5_API_TRY_CATCH_END
;
7638 bool Solver::getAbduct(const Term
& conj
, Term
& output
) const
7640 CVC5_API_TRY_CATCH_BEGIN
;
7641 CVC5_API_SOLVER_CHECK_TERM(conj
);
7642 CVC5_API_CHECK(d_slv
->getOptions().smt
.produceAbducts
)
7643 << "Cannot get abduct unless abducts are enabled (try --produce-abducts)";
7644 //////// all checks before this line
7647 bool success
= d_slv
->getAbduct(*conj
.d_node
, nullType
, result
);
7650 output
= Term(this, result
);
7654 CVC5_API_TRY_CATCH_END
;
7657 bool Solver::getAbduct(const Term
& conj
, Grammar
& grammar
, Term
& output
) const
7659 CVC5_API_TRY_CATCH_BEGIN
;
7660 CVC5_API_SOLVER_CHECK_TERM(conj
);
7661 CVC5_API_CHECK(d_slv
->getOptions().smt
.produceAbducts
)
7662 << "Cannot get abduct unless abducts are enabled (try --produce-abducts)";
7663 //////// all checks before this line
7666 d_slv
->getAbduct(*conj
.d_node
, *grammar
.resolve().d_type
, result
);
7669 output
= Term(this, result
);
7673 CVC5_API_TRY_CATCH_END
;
7676 bool Solver::getAbductNext(Term
& output
) const
7678 CVC5_API_TRY_CATCH_BEGIN
;
7679 CVC5_API_CHECK(d_slv
->getOptions().smt
.produceAbducts
)
7680 << "Cannot get next abduct unless abducts are enabled (try "
7681 "--produce-abducts)";
7682 CVC5_API_CHECK(d_slv
->getOptions().base
.incrementalSolving
)
7683 << "Cannot get next abduct when not solving incrementally (try "
7685 //////// all checks before this line
7687 bool success
= d_slv
->getAbductNext(result
);
7690 output
= Term(this, result
);
7694 CVC5_API_TRY_CATCH_END
;
7697 void Solver::blockModel() const
7699 CVC5_API_TRY_CATCH_BEGIN
;
7700 CVC5_API_CHECK(d_slv
->getOptions().smt
.produceModels
)
7701 << "Cannot get value unless model generation is enabled "
7702 "(try --produce-models)";
7703 CVC5_API_RECOVERABLE_CHECK(d_slv
->isSmtModeSat())
7704 << "Can only block model after SAT or UNKNOWN response.";
7705 //////// all checks before this line
7706 d_slv
->blockModel();
7708 CVC5_API_TRY_CATCH_END
;
7711 void Solver::blockModelValues(const std::vector
<Term
>& terms
) const
7713 CVC5_API_TRY_CATCH_BEGIN
;
7714 CVC5_API_CHECK(d_slv
->getOptions().smt
.produceModels
)
7715 << "Cannot get value unless model generation is enabled "
7716 "(try --produce-models)";
7717 CVC5_API_RECOVERABLE_CHECK(d_slv
->isSmtModeSat())
7718 << "Can only block model values after SAT or UNKNOWN response.";
7719 CVC5_API_ARG_SIZE_CHECK_EXPECTED(!terms
.empty(), terms
)
7720 << "a non-empty set of terms";
7721 CVC5_API_SOLVER_CHECK_TERMS(terms
);
7722 //////// all checks before this line
7723 d_slv
->blockModelValues(Term::termVectorToNodes(terms
));
7725 CVC5_API_TRY_CATCH_END
;
7728 void Solver::printInstantiations(std::ostream
& out
) const
7730 CVC5_API_TRY_CATCH_BEGIN
;
7731 //////// all checks before this line
7732 d_slv
->printInstantiations(out
);
7734 CVC5_API_TRY_CATCH_END
;
7737 void Solver::push(uint32_t nscopes
) const
7739 CVC5_API_TRY_CATCH_BEGIN
;
7740 CVC5_API_CHECK(d_slv
->getOptions().base
.incrementalSolving
)
7741 << "Cannot push when not solving incrementally (use --incremental)";
7742 //////// all checks before this line
7743 for (uint32_t n
= 0; n
< nscopes
; ++n
)
7748 CVC5_API_TRY_CATCH_END
;
7751 void Solver::resetAssertions(void) const
7753 CVC5_API_TRY_CATCH_BEGIN
;
7754 //////// all checks before this line
7755 d_slv
->resetAssertions();
7757 CVC5_API_TRY_CATCH_END
;
7760 void Solver::setInfo(const std::string
& keyword
, const std::string
& value
) const
7762 CVC5_API_TRY_CATCH_BEGIN
;
7763 CVC5_API_UNSUPPORTED_CHECK(
7764 keyword
== "source" || keyword
== "category" || keyword
== "difficulty"
7765 || keyword
== "filename" || keyword
== "license" || keyword
== "name"
7766 || keyword
== "notes" || keyword
== "smt-lib-version"
7767 || keyword
== "status")
7768 << "Unrecognized keyword: " << keyword
7769 << ", expected 'source', 'category', 'difficulty', "
7770 "'filename', 'license', 'name', "
7771 "'notes', 'smt-lib-version' or 'status'";
7772 CVC5_API_RECOVERABLE_ARG_CHECK_EXPECTED(
7773 keyword
!= "smt-lib-version" || value
== "2" || value
== "2.0"
7774 || value
== "2.5" || value
== "2.6",
7776 << "'2.0', '2.5', '2.6'";
7777 CVC5_API_ARG_CHECK_EXPECTED(keyword
!= "status" || value
== "sat"
7778 || value
== "unsat" || value
== "unknown",
7780 << "'sat', 'unsat' or 'unknown'";
7781 //////// all checks before this line
7782 d_slv
->setInfo(keyword
, value
);
7784 CVC5_API_TRY_CATCH_END
;
7787 void Solver::setLogic(const std::string
& logic
) const
7789 CVC5_API_TRY_CATCH_BEGIN
;
7790 CVC5_API_CHECK(!d_slv
->isFullyInited())
7791 << "Invalid call to 'setLogic', solver is already fully initialized";
7792 cvc5::LogicInfo
logic_info(logic
);
7793 //////// all checks before this line
7794 d_slv
->setLogic(logic_info
);
7796 CVC5_API_TRY_CATCH_END
;
7799 void Solver::setOption(const std::string
& option
,
7800 const std::string
& value
) const
7802 CVC5_API_TRY_CATCH_BEGIN
;
7803 std::vector
<std::string
> options
= options::getNames();
7804 CVC5_API_UNSUPPORTED_CHECK(
7805 option
.find("command-verbosity") != std::string::npos
7806 || std::find(options
.cbegin(), options
.cend(), option
) != options
.cend())
7807 << "Unrecognized option: " << option
<< '.';
7808 static constexpr auto mutableOpts
= {"diagnostic-output-channel",
7810 "regular-output-channel",
7811 "reproducible-resource-limit",
7813 if (std::find(mutableOpts
.begin(), mutableOpts
.end(), option
)
7814 == mutableOpts
.end())
7816 CVC5_API_CHECK(!d_slv
->isFullyInited())
7817 << "Invalid call to 'setOption' for option '" << option
7818 << "', solver is already fully initialized";
7820 //////// all checks before this line
7821 d_slv
->setOption(option
, value
);
7823 CVC5_API_TRY_CATCH_END
;
7826 Term
Solver::mkSygusVar(const Sort
& sort
, const std::string
& symbol
) const
7828 CVC5_API_TRY_CATCH_BEGIN
;
7829 CVC5_API_SOLVER_CHECK_SORT(sort
);
7830 //////// all checks before this line
7831 Node res
= getNodeManager()->mkBoundVar(symbol
, *sort
.d_type
);
7832 (void)res
.getType(true); /* kick off type checking */
7834 d_slv
->declareSygusVar(res
);
7836 return Term(this, res
);
7838 CVC5_API_TRY_CATCH_END
;
7841 Grammar
Solver::mkSygusGrammar(const std::vector
<Term
>& boundVars
,
7842 const std::vector
<Term
>& ntSymbols
) const
7844 CVC5_API_TRY_CATCH_BEGIN
;
7845 CVC5_API_ARG_SIZE_CHECK_EXPECTED(!ntSymbols
.empty(), ntSymbols
)
7846 << "a non-empty vector";
7847 CVC5_API_SOLVER_CHECK_BOUND_VARS(boundVars
);
7848 CVC5_API_SOLVER_CHECK_BOUND_VARS(ntSymbols
);
7849 //////// all checks before this line
7850 return Grammar(this, boundVars
, ntSymbols
);
7852 CVC5_API_TRY_CATCH_END
;
7855 Term
Solver::synthFun(const std::string
& symbol
,
7856 const std::vector
<Term
>& boundVars
,
7857 const Sort
& sort
) const
7859 CVC5_API_TRY_CATCH_BEGIN
;
7860 CVC5_API_SOLVER_CHECK_BOUND_VARS(boundVars
);
7861 CVC5_API_SOLVER_CHECK_SORT(sort
);
7862 //////// all checks before this line
7863 return synthFunHelper(symbol
, boundVars
, sort
);
7865 CVC5_API_TRY_CATCH_END
;
7868 Term
Solver::synthFun(const std::string
& symbol
,
7869 const std::vector
<Term
>& boundVars
,
7871 Grammar
& grammar
) const
7873 CVC5_API_TRY_CATCH_BEGIN
;
7874 CVC5_API_SOLVER_CHECK_BOUND_VARS(boundVars
);
7875 CVC5_API_SOLVER_CHECK_SORT(sort
);
7876 //////// all checks before this line
7877 return synthFunHelper(symbol
, boundVars
, sort
, false, &grammar
);
7879 CVC5_API_TRY_CATCH_END
;
7882 Term
Solver::synthInv(const std::string
& symbol
,
7883 const std::vector
<Term
>& boundVars
) const
7885 CVC5_API_TRY_CATCH_BEGIN
;
7886 CVC5_API_SOLVER_CHECK_BOUND_VARS(boundVars
);
7887 //////// all checks before this line
7888 return synthFunHelper(
7889 symbol
, boundVars
, Sort(this, getNodeManager()->booleanType()), true);
7891 CVC5_API_TRY_CATCH_END
;
7894 Term
Solver::synthInv(const std::string
& symbol
,
7895 const std::vector
<Term
>& boundVars
,
7896 Grammar
& grammar
) const
7898 CVC5_API_TRY_CATCH_BEGIN
;
7899 CVC5_API_SOLVER_CHECK_BOUND_VARS(boundVars
);
7900 //////// all checks before this line
7901 return synthFunHelper(symbol
,
7903 Sort(this, getNodeManager()->booleanType()),
7907 CVC5_API_TRY_CATCH_END
;
7910 void Solver::addSygusConstraint(const Term
& term
) const
7912 CVC5_API_TRY_CATCH_BEGIN
;
7913 CVC5_API_SOLVER_CHECK_TERM(term
);
7914 CVC5_API_ARG_CHECK_EXPECTED(
7915 term
.d_node
->getType() == getNodeManager()->booleanType(), term
)
7917 //////// all checks before this line
7918 d_slv
->assertSygusConstraint(*term
.d_node
, false);
7920 CVC5_API_TRY_CATCH_END
;
7923 void Solver::addSygusAssume(const Term
& term
) const
7925 CVC5_API_TRY_CATCH_BEGIN
;
7926 CVC5_API_SOLVER_CHECK_TERM(term
);
7927 CVC5_API_ARG_CHECK_EXPECTED(
7928 term
.d_node
->getType() == getNodeManager()->booleanType(), term
)
7930 //////// all checks before this line
7931 d_slv
->assertSygusConstraint(*term
.d_node
, true);
7933 CVC5_API_TRY_CATCH_END
;
7936 void Solver::addSygusInvConstraint(Term inv
,
7941 CVC5_API_TRY_CATCH_BEGIN
;
7942 CVC5_API_SOLVER_CHECK_TERM(inv
);
7943 CVC5_API_SOLVER_CHECK_TERM(pre
);
7944 CVC5_API_SOLVER_CHECK_TERM(trans
);
7945 CVC5_API_SOLVER_CHECK_TERM(post
);
7947 CVC5_API_ARG_CHECK_EXPECTED(inv
.d_node
->getType().isFunction(), inv
)
7950 TypeNode invType
= inv
.d_node
->getType();
7952 CVC5_API_ARG_CHECK_EXPECTED(invType
.getRangeType().isBoolean(), inv
)
7955 CVC5_API_CHECK(pre
.d_node
->getType() == invType
)
7956 << "Expected inv and pre to have the same sort";
7958 CVC5_API_CHECK(post
.d_node
->getType() == invType
)
7959 << "Expected inv and post to have the same sort";
7960 //////// all checks before this line
7962 const std::vector
<TypeNode
>& invArgTypes
= invType
.getArgTypes();
7964 std::vector
<TypeNode
> expectedTypes
;
7965 expectedTypes
.reserve(2 * invArgTypes
.size() + 1);
7967 for (size_t i
= 0, n
= invArgTypes
.size(); i
< 2 * n
; i
+= 2)
7969 expectedTypes
.push_back(invArgTypes
[i
% n
]);
7970 expectedTypes
.push_back(invArgTypes
[(i
+ 1) % n
]);
7973 expectedTypes
.push_back(invType
.getRangeType());
7974 TypeNode expectedTransType
= getNodeManager()->mkFunctionType(expectedTypes
);
7976 CVC5_API_CHECK(trans
.d_node
->getType() == expectedTransType
)
7977 << "Expected trans's sort to be " << invType
;
7979 d_slv
->assertSygusInvConstraint(
7980 *inv
.d_node
, *pre
.d_node
, *trans
.d_node
, *post
.d_node
);
7982 CVC5_API_TRY_CATCH_END
;
7985 Result
Solver::checkSynth() const
7987 CVC5_API_TRY_CATCH_BEGIN
;
7988 //////// all checks before this line
7989 return d_slv
->checkSynth();
7991 CVC5_API_TRY_CATCH_END
;
7994 Result
Solver::checkSynthNext() const
7996 CVC5_API_TRY_CATCH_BEGIN
;
7997 CVC5_API_CHECK(d_slv
->getOptions().base
.incrementalSolving
)
7998 << "Cannot checkSynthNext when not solving incrementally (use "
8000 //////// all checks before this line
8001 return d_slv
->checkSynth(true);
8003 CVC5_API_TRY_CATCH_END
;
8006 Term
Solver::getSynthSolution(Term term
) const
8008 CVC5_API_TRY_CATCH_BEGIN
;
8009 CVC5_API_SOLVER_CHECK_TERM(term
);
8011 std::map
<cvc5::Node
, cvc5::Node
> map
;
8012 CVC5_API_CHECK(d_slv
->getSynthSolutions(map
))
8013 << "The solver is not in a state immediately preceded by a "
8014 "successful call to checkSynth";
8016 std::map
<cvc5::Node
, cvc5::Node
>::const_iterator it
= map
.find(*term
.d_node
);
8018 CVC5_API_CHECK(it
!= map
.cend()) << "Synth solution not found for given term";
8019 //////// all checks before this line
8020 return Term(this, it
->second
);
8022 CVC5_API_TRY_CATCH_END
;
8025 std::vector
<Term
> Solver::getSynthSolutions(
8026 const std::vector
<Term
>& terms
) const
8028 CVC5_API_TRY_CATCH_BEGIN
;
8029 CVC5_API_ARG_SIZE_CHECK_EXPECTED(!terms
.empty(), terms
) << "non-empty vector";
8030 CVC5_API_SOLVER_CHECK_TERMS(terms
);
8032 std::map
<cvc5::Node
, cvc5::Node
> map
;
8033 CVC5_API_CHECK(d_slv
->getSynthSolutions(map
))
8034 << "The solver is not in a state immediately preceded by a "
8035 "successful call to checkSynth";
8036 //////// all checks before this line
8038 std::vector
<Term
> synthSolution
;
8039 synthSolution
.reserve(terms
.size());
8041 for (size_t i
= 0, n
= terms
.size(); i
< n
; ++i
)
8043 std::map
<cvc5::Node
, cvc5::Node
>::const_iterator it
=
8044 map
.find(*terms
[i
].d_node
);
8046 CVC5_API_CHECK(it
!= map
.cend())
8047 << "Synth solution not found for term at index " << i
;
8049 synthSolution
.push_back(Term(this, it
->second
));
8052 return synthSolution
;
8054 CVC5_API_TRY_CATCH_END
;
8057 Statistics
Solver::getStatistics() const
8059 return Statistics(d_slv
->getStatisticsRegistry());
8062 bool Solver::isOutputOn(const std::string
& tag
) const
8064 // `isOutputOn(tag)` may raise an `OptionException`, which we do not want to
8065 // forward as such. We thus do not use the standard exception handling macros
8066 // here but roll our own.
8069 return d_slv
->getEnv().isOutputOn(tag
);
8071 catch (const cvc5::Exception
& e
)
8073 throw CVC5ApiException("Invalid output tag " + tag
);
8077 std::ostream
& Solver::getOutput(const std::string
& tag
) const
8079 // `output(tag)` may raise an `OptionException`, which we do not want to
8080 // forward as such. We thus do not use the standard exception handling macros
8081 // here but roll our own.
8084 return d_slv
->getEnv().output(tag
);
8086 catch (const cvc5::Exception
& e
)
8088 throw CVC5ApiException("Invalid output tag " + tag
);
8098 size_t hash
<cvc5::api::Kind
>::operator()(cvc5::api::Kind k
) const
8100 return static_cast<size_t>(k
);
8103 size_t hash
<cvc5::api::Op
>::operator()(const cvc5::api::Op
& t
) const
8105 if (t
.isIndexedHelper())
8107 return std::hash
<cvc5::Node
>()(*t
.d_node
);
8111 return std::hash
<cvc5::api::Kind
>()(t
.d_kind
);
8115 size_t std::hash
<cvc5::api::RoundingMode
>::operator()(
8116 cvc5::api::RoundingMode rm
) const
8118 return static_cast<size_t>(rm
);
8121 size_t std::hash
<cvc5::api::Sort
>::operator()(const cvc5::api::Sort
& s
) const
8123 return std::hash
<cvc5::TypeNode
>()(*s
.d_type
);
8126 size_t std::hash
<cvc5::api::Term
>::operator()(const cvc5::api::Term
& t
) const
8128 return std::hash
<cvc5::Node
>()(*t
.d_node
);