1 /******************************************************************************
2 * Top contributors (to current version):
3 * Aina Niemetz, Andrew Reynolds, Andres Noetzli
5 * This file is part of the cvc5 project.
7 * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
8 * in the top-level source directory and their institutional affiliations.
9 * All rights reserved. See the file COPYING in the top-level source
10 * directory for licensing information.
11 * ****************************************************************************
15 * A brief note on how to guard API functions:
17 * In general, we think of API guards as a fence -- they are supposed to make
18 * sure that no invalid arguments get passed into internal realms of cvc5.
19 * Thus we always want to catch such cases on the API level (and can then
20 * assert internally that no invalid argument is passed in).
22 * The only special case is when we use 3rd party back-ends we have no control
23 * over, and which throw (invalid_argument) exceptions anyways. In this case,
24 * we do not replicate argument checks but delegate them to the back-end,
25 * catch thrown exceptions, and raise a CVC5ApiException.
27 * Our Integer implementation, e.g., is such a special case since we support
28 * two different back end implementations (GMP, CLN). Be aware that they do
29 * not fully agree on what is (in)valid input, which requires extra checks for
30 * consistent behavior (see Solver::mkRealFromStrHelper for an example).
33 #include "api/cpp/cvc5.h"
38 #include "api/cpp/cvc5_checks.h"
39 #include "base/check.h"
40 #include "base/configuration.h"
41 #include "base/modal_exception.h"
42 #include "expr/array_store_all.h"
43 #include "expr/ascription_type.h"
44 #include "expr/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/sequence.h"
57 #include "expr/type_node.h"
58 #include "expr/uninterpreted_constant.h"
59 #include "options/base_options.h"
60 #include "options/main_options.h"
61 #include "options/option_exception.h"
62 #include "options/options.h"
63 #include "options/options_public.h"
64 #include "options/smt_options.h"
65 #include "proof/unsat_core.h"
67 #include "smt/model.h"
68 #include "smt/smt_mode.h"
69 #include "smt/solver_engine.h"
70 #include "theory/datatypes/tuple_project_op.h"
71 #include "theory/logic_info.h"
72 #include "theory/theory_model.h"
73 #include "util/abstract_value.h"
74 #include "util/bitvector.h"
75 #include "util/divisible.h"
76 #include "util/floatingpoint.h"
77 #include "util/iand.h"
78 #include "util/random.h"
79 #include "util/regexp.h"
80 #include "util/result.h"
81 #include "util/roundingmode.h"
82 #include "util/statistics_registry.h"
83 #include "util/statistics_stats.h"
84 #include "util/statistics_value.h"
85 #include "util/string.h"
86 #include "util/utility.h"
91 /* -------------------------------------------------------------------------- */
93 /* -------------------------------------------------------------------------- */
97 HistogramStat
<TypeConstant
> d_consts
;
98 HistogramStat
<TypeConstant
> d_vars
;
99 HistogramStat
<Kind
> d_terms
;
102 /* -------------------------------------------------------------------------- */
104 /* -------------------------------------------------------------------------- */
106 /* Mapping from external (API) kind to internal kind. */
107 const static std::unordered_map
<Kind
, cvc5::Kind
> s_kinds
{
108 {INTERNAL_KIND
, cvc5::Kind::UNDEFINED_KIND
},
109 {UNDEFINED_KIND
, cvc5::Kind::UNDEFINED_KIND
},
110 {NULL_EXPR
, cvc5::Kind::NULL_EXPR
},
111 /* Builtin ------------------------------------------------------------- */
112 {UNINTERPRETED_CONSTANT
, cvc5::Kind::UNINTERPRETED_CONSTANT
},
113 {ABSTRACT_VALUE
, cvc5::Kind::ABSTRACT_VALUE
},
114 {EQUAL
, cvc5::Kind::EQUAL
},
115 {DISTINCT
, cvc5::Kind::DISTINCT
},
116 {CONSTANT
, cvc5::Kind::VARIABLE
},
117 {VARIABLE
, cvc5::Kind::BOUND_VARIABLE
},
118 {SEXPR
, cvc5::Kind::SEXPR
},
119 {LAMBDA
, cvc5::Kind::LAMBDA
},
120 {WITNESS
, cvc5::Kind::WITNESS
},
121 /* Boolean ------------------------------------------------------------- */
122 {CONST_BOOLEAN
, cvc5::Kind::CONST_BOOLEAN
},
123 {NOT
, cvc5::Kind::NOT
},
124 {AND
, cvc5::Kind::AND
},
125 {IMPLIES
, cvc5::Kind::IMPLIES
},
126 {OR
, cvc5::Kind::OR
},
127 {XOR
, cvc5::Kind::XOR
},
128 {ITE
, cvc5::Kind::ITE
},
129 {MATCH
, cvc5::Kind::MATCH
},
130 {MATCH_CASE
, cvc5::Kind::MATCH_CASE
},
131 {MATCH_BIND_CASE
, cvc5::Kind::MATCH_BIND_CASE
},
132 /* UF ------------------------------------------------------------------ */
133 {APPLY_UF
, cvc5::Kind::APPLY_UF
},
134 {CARDINALITY_CONSTRAINT
, cvc5::Kind::CARDINALITY_CONSTRAINT
},
135 {HO_APPLY
, cvc5::Kind::HO_APPLY
},
136 /* Arithmetic ---------------------------------------------------------- */
137 {PLUS
, cvc5::Kind::PLUS
},
138 {MULT
, cvc5::Kind::MULT
},
139 {IAND
, cvc5::Kind::IAND
},
140 {POW2
, cvc5::Kind::POW2
},
141 {MINUS
, cvc5::Kind::MINUS
},
142 {UMINUS
, cvc5::Kind::UMINUS
},
143 {DIVISION
, cvc5::Kind::DIVISION
},
144 {INTS_DIVISION
, cvc5::Kind::INTS_DIVISION
},
145 {INTS_MODULUS
, cvc5::Kind::INTS_MODULUS
},
146 {ABS
, cvc5::Kind::ABS
},
147 {DIVISIBLE
, cvc5::Kind::DIVISIBLE
},
148 {POW
, cvc5::Kind::POW
},
149 {EXPONENTIAL
, cvc5::Kind::EXPONENTIAL
},
150 {SINE
, cvc5::Kind::SINE
},
151 {COSINE
, cvc5::Kind::COSINE
},
152 {TANGENT
, cvc5::Kind::TANGENT
},
153 {COSECANT
, cvc5::Kind::COSECANT
},
154 {SECANT
, cvc5::Kind::SECANT
},
155 {COTANGENT
, cvc5::Kind::COTANGENT
},
156 {ARCSINE
, cvc5::Kind::ARCSINE
},
157 {ARCCOSINE
, cvc5::Kind::ARCCOSINE
},
158 {ARCTANGENT
, cvc5::Kind::ARCTANGENT
},
159 {ARCCOSECANT
, cvc5::Kind::ARCCOSECANT
},
160 {ARCSECANT
, cvc5::Kind::ARCSECANT
},
161 {ARCCOTANGENT
, cvc5::Kind::ARCCOTANGENT
},
162 {SQRT
, cvc5::Kind::SQRT
},
163 {CONST_RATIONAL
, cvc5::Kind::CONST_RATIONAL
},
164 {LT
, cvc5::Kind::LT
},
165 {LEQ
, cvc5::Kind::LEQ
},
166 {GT
, cvc5::Kind::GT
},
167 {GEQ
, cvc5::Kind::GEQ
},
168 {IS_INTEGER
, cvc5::Kind::IS_INTEGER
},
169 {TO_INTEGER
, cvc5::Kind::TO_INTEGER
},
170 {TO_REAL
, cvc5::Kind::TO_REAL
},
171 {PI
, cvc5::Kind::PI
},
172 /* BV ------------------------------------------------------------------ */
173 {CONST_BITVECTOR
, cvc5::Kind::CONST_BITVECTOR
},
174 {BITVECTOR_CONCAT
, cvc5::Kind::BITVECTOR_CONCAT
},
175 {BITVECTOR_AND
, cvc5::Kind::BITVECTOR_AND
},
176 {BITVECTOR_OR
, cvc5::Kind::BITVECTOR_OR
},
177 {BITVECTOR_XOR
, cvc5::Kind::BITVECTOR_XOR
},
178 {BITVECTOR_NOT
, cvc5::Kind::BITVECTOR_NOT
},
179 {BITVECTOR_NAND
, cvc5::Kind::BITVECTOR_NAND
},
180 {BITVECTOR_NOR
, cvc5::Kind::BITVECTOR_NOR
},
181 {BITVECTOR_XNOR
, cvc5::Kind::BITVECTOR_XNOR
},
182 {BITVECTOR_COMP
, cvc5::Kind::BITVECTOR_COMP
},
183 {BITVECTOR_MULT
, cvc5::Kind::BITVECTOR_MULT
},
184 {BITVECTOR_ADD
, cvc5::Kind::BITVECTOR_ADD
},
185 {BITVECTOR_SUB
, cvc5::Kind::BITVECTOR_SUB
},
186 {BITVECTOR_NEG
, cvc5::Kind::BITVECTOR_NEG
},
187 {BITVECTOR_UDIV
, cvc5::Kind::BITVECTOR_UDIV
},
188 {BITVECTOR_UREM
, cvc5::Kind::BITVECTOR_UREM
},
189 {BITVECTOR_SDIV
, cvc5::Kind::BITVECTOR_SDIV
},
190 {BITVECTOR_SREM
, cvc5::Kind::BITVECTOR_SREM
},
191 {BITVECTOR_SMOD
, cvc5::Kind::BITVECTOR_SMOD
},
192 {BITVECTOR_SHL
, cvc5::Kind::BITVECTOR_SHL
},
193 {BITVECTOR_LSHR
, cvc5::Kind::BITVECTOR_LSHR
},
194 {BITVECTOR_ASHR
, cvc5::Kind::BITVECTOR_ASHR
},
195 {BITVECTOR_ULT
, cvc5::Kind::BITVECTOR_ULT
},
196 {BITVECTOR_ULE
, cvc5::Kind::BITVECTOR_ULE
},
197 {BITVECTOR_UGT
, cvc5::Kind::BITVECTOR_UGT
},
198 {BITVECTOR_UGE
, cvc5::Kind::BITVECTOR_UGE
},
199 {BITVECTOR_SLT
, cvc5::Kind::BITVECTOR_SLT
},
200 {BITVECTOR_SLE
, cvc5::Kind::BITVECTOR_SLE
},
201 {BITVECTOR_SGT
, cvc5::Kind::BITVECTOR_SGT
},
202 {BITVECTOR_SGE
, cvc5::Kind::BITVECTOR_SGE
},
203 {BITVECTOR_ULTBV
, cvc5::Kind::BITVECTOR_ULTBV
},
204 {BITVECTOR_SLTBV
, cvc5::Kind::BITVECTOR_SLTBV
},
205 {BITVECTOR_ITE
, cvc5::Kind::BITVECTOR_ITE
},
206 {BITVECTOR_REDOR
, cvc5::Kind::BITVECTOR_REDOR
},
207 {BITVECTOR_REDAND
, cvc5::Kind::BITVECTOR_REDAND
},
208 {BITVECTOR_EXTRACT
, cvc5::Kind::BITVECTOR_EXTRACT
},
209 {BITVECTOR_REPEAT
, cvc5::Kind::BITVECTOR_REPEAT
},
210 {BITVECTOR_ZERO_EXTEND
, cvc5::Kind::BITVECTOR_ZERO_EXTEND
},
211 {BITVECTOR_SIGN_EXTEND
, cvc5::Kind::BITVECTOR_SIGN_EXTEND
},
212 {BITVECTOR_ROTATE_LEFT
, cvc5::Kind::BITVECTOR_ROTATE_LEFT
},
213 {BITVECTOR_ROTATE_RIGHT
, cvc5::Kind::BITVECTOR_ROTATE_RIGHT
},
214 {INT_TO_BITVECTOR
, cvc5::Kind::INT_TO_BITVECTOR
},
215 {BITVECTOR_TO_NAT
, cvc5::Kind::BITVECTOR_TO_NAT
},
216 /* FP ------------------------------------------------------------------ */
217 {CONST_FLOATINGPOINT
, cvc5::Kind::CONST_FLOATINGPOINT
},
218 {CONST_ROUNDINGMODE
, cvc5::Kind::CONST_ROUNDINGMODE
},
219 {FLOATINGPOINT_FP
, cvc5::Kind::FLOATINGPOINT_FP
},
220 {FLOATINGPOINT_EQ
, cvc5::Kind::FLOATINGPOINT_EQ
},
221 {FLOATINGPOINT_ABS
, cvc5::Kind::FLOATINGPOINT_ABS
},
222 {FLOATINGPOINT_NEG
, cvc5::Kind::FLOATINGPOINT_NEG
},
223 {FLOATINGPOINT_ADD
, cvc5::Kind::FLOATINGPOINT_ADD
},
224 {FLOATINGPOINT_SUB
, cvc5::Kind::FLOATINGPOINT_SUB
},
225 {FLOATINGPOINT_MULT
, cvc5::Kind::FLOATINGPOINT_MULT
},
226 {FLOATINGPOINT_DIV
, cvc5::Kind::FLOATINGPOINT_DIV
},
227 {FLOATINGPOINT_FMA
, cvc5::Kind::FLOATINGPOINT_FMA
},
228 {FLOATINGPOINT_SQRT
, cvc5::Kind::FLOATINGPOINT_SQRT
},
229 {FLOATINGPOINT_REM
, cvc5::Kind::FLOATINGPOINT_REM
},
230 {FLOATINGPOINT_RTI
, cvc5::Kind::FLOATINGPOINT_RTI
},
231 {FLOATINGPOINT_MIN
, cvc5::Kind::FLOATINGPOINT_MIN
},
232 {FLOATINGPOINT_MAX
, cvc5::Kind::FLOATINGPOINT_MAX
},
233 {FLOATINGPOINT_LEQ
, cvc5::Kind::FLOATINGPOINT_LEQ
},
234 {FLOATINGPOINT_LT
, cvc5::Kind::FLOATINGPOINT_LT
},
235 {FLOATINGPOINT_GEQ
, cvc5::Kind::FLOATINGPOINT_GEQ
},
236 {FLOATINGPOINT_GT
, cvc5::Kind::FLOATINGPOINT_GT
},
237 {FLOATINGPOINT_ISN
, cvc5::Kind::FLOATINGPOINT_ISN
},
238 {FLOATINGPOINT_ISSN
, cvc5::Kind::FLOATINGPOINT_ISSN
},
239 {FLOATINGPOINT_ISZ
, cvc5::Kind::FLOATINGPOINT_ISZ
},
240 {FLOATINGPOINT_ISINF
, cvc5::Kind::FLOATINGPOINT_ISINF
},
241 {FLOATINGPOINT_ISNAN
, cvc5::Kind::FLOATINGPOINT_ISNAN
},
242 {FLOATINGPOINT_ISNEG
, cvc5::Kind::FLOATINGPOINT_ISNEG
},
243 {FLOATINGPOINT_ISPOS
, cvc5::Kind::FLOATINGPOINT_ISPOS
},
244 {FLOATINGPOINT_TO_FP_FLOATINGPOINT
,
245 cvc5::Kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT
},
246 {FLOATINGPOINT_TO_FP_IEEE_BITVECTOR
,
247 cvc5::Kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR
},
248 {FLOATINGPOINT_TO_FP_REAL
, cvc5::Kind::FLOATINGPOINT_TO_FP_REAL
},
249 {FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR
,
250 cvc5::Kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR
},
251 {FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR
,
252 cvc5::Kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR
},
253 {FLOATINGPOINT_TO_FP_GENERIC
, cvc5::Kind::FLOATINGPOINT_TO_FP_GENERIC
},
254 {FLOATINGPOINT_TO_UBV
, cvc5::Kind::FLOATINGPOINT_TO_UBV
},
255 {FLOATINGPOINT_TO_SBV
, cvc5::Kind::FLOATINGPOINT_TO_SBV
},
256 {FLOATINGPOINT_TO_REAL
, cvc5::Kind::FLOATINGPOINT_TO_REAL
},
257 /* Arrays -------------------------------------------------------------- */
258 {SELECT
, cvc5::Kind::SELECT
},
259 {STORE
, cvc5::Kind::STORE
},
260 {CONST_ARRAY
, cvc5::Kind::STORE_ALL
},
261 {EQ_RANGE
, cvc5::Kind::EQ_RANGE
},
262 /* Datatypes ----------------------------------------------------------- */
263 {APPLY_SELECTOR
, cvc5::Kind::APPLY_SELECTOR
},
264 {APPLY_CONSTRUCTOR
, cvc5::Kind::APPLY_CONSTRUCTOR
},
265 {APPLY_TESTER
, cvc5::Kind::APPLY_TESTER
},
266 {APPLY_UPDATER
, cvc5::Kind::APPLY_UPDATER
},
267 {DT_SIZE
, cvc5::Kind::DT_SIZE
},
268 {TUPLE_PROJECT
, cvc5::Kind::TUPLE_PROJECT
},
269 /* Separation Logic ---------------------------------------------------- */
270 {SEP_NIL
, cvc5::Kind::SEP_NIL
},
271 {SEP_EMP
, cvc5::Kind::SEP_EMP
},
272 {SEP_PTO
, cvc5::Kind::SEP_PTO
},
273 {SEP_STAR
, cvc5::Kind::SEP_STAR
},
274 {SEP_WAND
, cvc5::Kind::SEP_WAND
},
275 /* Sets ---------------------------------------------------------------- */
276 {EMPTYSET
, cvc5::Kind::EMPTYSET
},
277 {UNION
, cvc5::Kind::UNION
},
278 {INTERSECTION
, cvc5::Kind::INTERSECTION
},
279 {SETMINUS
, cvc5::Kind::SETMINUS
},
280 {SUBSET
, cvc5::Kind::SUBSET
},
281 {MEMBER
, cvc5::Kind::MEMBER
},
282 {SINGLETON
, cvc5::Kind::SINGLETON
},
283 {INSERT
, cvc5::Kind::INSERT
},
284 {CARD
, cvc5::Kind::CARD
},
285 {COMPLEMENT
, cvc5::Kind::COMPLEMENT
},
286 {UNIVERSE_SET
, cvc5::Kind::UNIVERSE_SET
},
287 {JOIN
, cvc5::Kind::JOIN
},
288 {PRODUCT
, cvc5::Kind::PRODUCT
},
289 {TRANSPOSE
, cvc5::Kind::TRANSPOSE
},
290 {TCLOSURE
, cvc5::Kind::TCLOSURE
},
291 {JOIN_IMAGE
, cvc5::Kind::JOIN_IMAGE
},
292 {IDEN
, cvc5::Kind::IDEN
},
293 {COMPREHENSION
, cvc5::Kind::COMPREHENSION
},
294 {CHOOSE
, cvc5::Kind::CHOOSE
},
295 {IS_SINGLETON
, cvc5::Kind::IS_SINGLETON
},
296 /* Bags ---------------------------------------------------------------- */
297 {UNION_MAX
, cvc5::Kind::UNION_MAX
},
298 {UNION_DISJOINT
, cvc5::Kind::UNION_DISJOINT
},
299 {INTERSECTION_MIN
, cvc5::Kind::INTERSECTION_MIN
},
300 {DIFFERENCE_SUBTRACT
, cvc5::Kind::DIFFERENCE_SUBTRACT
},
301 {DIFFERENCE_REMOVE
, cvc5::Kind::DIFFERENCE_REMOVE
},
302 {SUBBAG
, cvc5::Kind::SUBBAG
},
303 {BAG_COUNT
, cvc5::Kind::BAG_COUNT
},
304 {DUPLICATE_REMOVAL
, cvc5::Kind::DUPLICATE_REMOVAL
},
305 {MK_BAG
, cvc5::Kind::MK_BAG
},
306 {EMPTYBAG
, cvc5::Kind::EMPTYBAG
},
307 {BAG_CARD
, cvc5::Kind::BAG_CARD
},
308 {BAG_CHOOSE
, cvc5::Kind::BAG_CHOOSE
},
309 {BAG_IS_SINGLETON
, cvc5::Kind::BAG_IS_SINGLETON
},
310 {BAG_FROM_SET
, cvc5::Kind::BAG_FROM_SET
},
311 {BAG_TO_SET
, cvc5::Kind::BAG_TO_SET
},
312 {BAG_MAP
, cvc5::Kind::BAG_MAP
},
313 /* Strings ------------------------------------------------------------- */
314 {STRING_CONCAT
, cvc5::Kind::STRING_CONCAT
},
315 {STRING_IN_REGEXP
, cvc5::Kind::STRING_IN_REGEXP
},
316 {STRING_LENGTH
, cvc5::Kind::STRING_LENGTH
},
317 {STRING_SUBSTR
, cvc5::Kind::STRING_SUBSTR
},
318 {STRING_UPDATE
, cvc5::Kind::STRING_UPDATE
},
319 {STRING_CHARAT
, cvc5::Kind::STRING_CHARAT
},
320 {STRING_CONTAINS
, cvc5::Kind::STRING_CONTAINS
},
321 {STRING_INDEXOF
, cvc5::Kind::STRING_INDEXOF
},
322 {STRING_INDEXOF_RE
, cvc5::Kind::STRING_INDEXOF_RE
},
323 {STRING_REPLACE
, cvc5::Kind::STRING_REPLACE
},
324 {STRING_REPLACE_ALL
, cvc5::Kind::STRING_REPLACE_ALL
},
325 {STRING_REPLACE_RE
, cvc5::Kind::STRING_REPLACE_RE
},
326 {STRING_REPLACE_RE_ALL
, cvc5::Kind::STRING_REPLACE_RE_ALL
},
327 {STRING_TOLOWER
, cvc5::Kind::STRING_TOLOWER
},
328 {STRING_TOUPPER
, cvc5::Kind::STRING_TOUPPER
},
329 {STRING_REV
, cvc5::Kind::STRING_REV
},
330 {STRING_FROM_CODE
, cvc5::Kind::STRING_FROM_CODE
},
331 {STRING_TO_CODE
, cvc5::Kind::STRING_TO_CODE
},
332 {STRING_LT
, cvc5::Kind::STRING_LT
},
333 {STRING_LEQ
, cvc5::Kind::STRING_LEQ
},
334 {STRING_PREFIX
, cvc5::Kind::STRING_PREFIX
},
335 {STRING_SUFFIX
, cvc5::Kind::STRING_SUFFIX
},
336 {STRING_IS_DIGIT
, cvc5::Kind::STRING_IS_DIGIT
},
337 {STRING_FROM_INT
, cvc5::Kind::STRING_ITOS
},
338 {STRING_TO_INT
, cvc5::Kind::STRING_STOI
},
339 {CONST_STRING
, cvc5::Kind::CONST_STRING
},
340 {STRING_TO_REGEXP
, cvc5::Kind::STRING_TO_REGEXP
},
341 {REGEXP_CONCAT
, cvc5::Kind::REGEXP_CONCAT
},
342 {REGEXP_UNION
, cvc5::Kind::REGEXP_UNION
},
343 {REGEXP_INTER
, cvc5::Kind::REGEXP_INTER
},
344 {REGEXP_DIFF
, cvc5::Kind::REGEXP_DIFF
},
345 {REGEXP_STAR
, cvc5::Kind::REGEXP_STAR
},
346 {REGEXP_PLUS
, cvc5::Kind::REGEXP_PLUS
},
347 {REGEXP_OPT
, cvc5::Kind::REGEXP_OPT
},
348 {REGEXP_RANGE
, cvc5::Kind::REGEXP_RANGE
},
349 {REGEXP_REPEAT
, cvc5::Kind::REGEXP_REPEAT
},
350 {REGEXP_LOOP
, cvc5::Kind::REGEXP_LOOP
},
351 {REGEXP_EMPTY
, cvc5::Kind::REGEXP_EMPTY
},
352 {REGEXP_SIGMA
, cvc5::Kind::REGEXP_SIGMA
},
353 {REGEXP_COMPLEMENT
, cvc5::Kind::REGEXP_COMPLEMENT
},
354 // maps to the same kind as the string versions
355 {SEQ_CONCAT
, cvc5::Kind::STRING_CONCAT
},
356 {SEQ_LENGTH
, cvc5::Kind::STRING_LENGTH
},
357 {SEQ_EXTRACT
, cvc5::Kind::STRING_SUBSTR
},
358 {SEQ_UPDATE
, cvc5::Kind::STRING_UPDATE
},
359 {SEQ_AT
, cvc5::Kind::STRING_CHARAT
},
360 {SEQ_CONTAINS
, cvc5::Kind::STRING_CONTAINS
},
361 {SEQ_INDEXOF
, cvc5::Kind::STRING_INDEXOF
},
362 {SEQ_REPLACE
, cvc5::Kind::STRING_REPLACE
},
363 {SEQ_REPLACE_ALL
, cvc5::Kind::STRING_REPLACE_ALL
},
364 {SEQ_REV
, cvc5::Kind::STRING_REV
},
365 {SEQ_PREFIX
, cvc5::Kind::STRING_PREFIX
},
366 {SEQ_SUFFIX
, cvc5::Kind::STRING_SUFFIX
},
367 {CONST_SEQUENCE
, cvc5::Kind::CONST_SEQUENCE
},
368 {SEQ_UNIT
, cvc5::Kind::SEQ_UNIT
},
369 {SEQ_NTH
, cvc5::Kind::SEQ_NTH
},
370 /* Quantifiers --------------------------------------------------------- */
371 {FORALL
, cvc5::Kind::FORALL
},
372 {EXISTS
, cvc5::Kind::EXISTS
},
373 {BOUND_VAR_LIST
, cvc5::Kind::BOUND_VAR_LIST
},
374 {INST_PATTERN
, cvc5::Kind::INST_PATTERN
},
375 {INST_NO_PATTERN
, cvc5::Kind::INST_NO_PATTERN
},
376 {INST_POOL
, cvc5::Kind::INST_POOL
},
377 {INST_ADD_TO_POOL
, cvc5::Kind::INST_ADD_TO_POOL
},
378 {SKOLEM_ADD_TO_POOL
, cvc5::Kind::SKOLEM_ADD_TO_POOL
},
379 {INST_ATTRIBUTE
, cvc5::Kind::INST_ATTRIBUTE
},
380 {INST_PATTERN_LIST
, cvc5::Kind::INST_PATTERN_LIST
},
381 {LAST_KIND
, cvc5::Kind::LAST_KIND
},
384 /* Mapping from internal kind to external (API) kind. */
385 const static std::unordered_map
<cvc5::Kind
, Kind
, cvc5::kind::KindHashFunction
>
387 {cvc5::Kind::UNDEFINED_KIND
, UNDEFINED_KIND
},
388 {cvc5::Kind::NULL_EXPR
, NULL_EXPR
},
389 /* Builtin --------------------------------------------------------- */
390 {cvc5::Kind::UNINTERPRETED_CONSTANT
, UNINTERPRETED_CONSTANT
},
391 {cvc5::Kind::ABSTRACT_VALUE
, ABSTRACT_VALUE
},
392 {cvc5::Kind::EQUAL
, EQUAL
},
393 {cvc5::Kind::DISTINCT
, DISTINCT
},
394 {cvc5::Kind::VARIABLE
, CONSTANT
},
395 {cvc5::Kind::BOUND_VARIABLE
, VARIABLE
},
396 {cvc5::Kind::SEXPR
, SEXPR
},
397 {cvc5::Kind::LAMBDA
, LAMBDA
},
398 {cvc5::Kind::WITNESS
, WITNESS
},
399 /* Boolean --------------------------------------------------------- */
400 {cvc5::Kind::CONST_BOOLEAN
, CONST_BOOLEAN
},
401 {cvc5::Kind::NOT
, NOT
},
402 {cvc5::Kind::AND
, AND
},
403 {cvc5::Kind::IMPLIES
, IMPLIES
},
404 {cvc5::Kind::OR
, OR
},
405 {cvc5::Kind::XOR
, XOR
},
406 {cvc5::Kind::ITE
, ITE
},
407 {cvc5::Kind::MATCH
, MATCH
},
408 {cvc5::Kind::MATCH_CASE
, MATCH_CASE
},
409 {cvc5::Kind::MATCH_BIND_CASE
, MATCH_BIND_CASE
},
410 /* UF -------------------------------------------------------------- */
411 {cvc5::Kind::APPLY_UF
, APPLY_UF
},
412 {cvc5::Kind::CARDINALITY_CONSTRAINT
, CARDINALITY_CONSTRAINT
},
413 {cvc5::Kind::HO_APPLY
, HO_APPLY
},
414 /* Arithmetic ------------------------------------------------------ */
415 {cvc5::Kind::PLUS
, PLUS
},
416 {cvc5::Kind::MULT
, MULT
},
417 {cvc5::Kind::IAND
, IAND
},
418 {cvc5::Kind::POW2
, POW2
},
419 {cvc5::Kind::MINUS
, MINUS
},
420 {cvc5::Kind::UMINUS
, UMINUS
},
421 {cvc5::Kind::DIVISION
, DIVISION
},
422 {cvc5::Kind::DIVISION_TOTAL
, INTERNAL_KIND
},
423 {cvc5::Kind::INTS_DIVISION
, INTS_DIVISION
},
424 {cvc5::Kind::INTS_DIVISION_TOTAL
, INTERNAL_KIND
},
425 {cvc5::Kind::INTS_MODULUS
, INTS_MODULUS
},
426 {cvc5::Kind::INTS_MODULUS_TOTAL
, INTERNAL_KIND
},
427 {cvc5::Kind::ABS
, ABS
},
428 {cvc5::Kind::DIVISIBLE
, DIVISIBLE
},
429 {cvc5::Kind::POW
, POW
},
430 {cvc5::Kind::EXPONENTIAL
, EXPONENTIAL
},
431 {cvc5::Kind::SINE
, SINE
},
432 {cvc5::Kind::COSINE
, COSINE
},
433 {cvc5::Kind::TANGENT
, TANGENT
},
434 {cvc5::Kind::COSECANT
, COSECANT
},
435 {cvc5::Kind::SECANT
, SECANT
},
436 {cvc5::Kind::COTANGENT
, COTANGENT
},
437 {cvc5::Kind::ARCSINE
, ARCSINE
},
438 {cvc5::Kind::ARCCOSINE
, ARCCOSINE
},
439 {cvc5::Kind::ARCTANGENT
, ARCTANGENT
},
440 {cvc5::Kind::ARCCOSECANT
, ARCCOSECANT
},
441 {cvc5::Kind::ARCSECANT
, ARCSECANT
},
442 {cvc5::Kind::ARCCOTANGENT
, ARCCOTANGENT
},
443 {cvc5::Kind::SQRT
, SQRT
},
444 {cvc5::Kind::DIVISIBLE_OP
, DIVISIBLE
},
445 {cvc5::Kind::CONST_RATIONAL
, CONST_RATIONAL
},
446 {cvc5::Kind::LT
, LT
},
447 {cvc5::Kind::LEQ
, LEQ
},
448 {cvc5::Kind::GT
, GT
},
449 {cvc5::Kind::GEQ
, GEQ
},
450 {cvc5::Kind::IS_INTEGER
, IS_INTEGER
},
451 {cvc5::Kind::TO_INTEGER
, TO_INTEGER
},
452 {cvc5::Kind::TO_REAL
, TO_REAL
},
453 {cvc5::Kind::PI
, PI
},
454 {cvc5::Kind::IAND_OP
, IAND
},
455 /* BV -------------------------------------------------------------- */
456 {cvc5::Kind::CONST_BITVECTOR
, CONST_BITVECTOR
},
457 {cvc5::Kind::BITVECTOR_CONCAT
, BITVECTOR_CONCAT
},
458 {cvc5::Kind::BITVECTOR_AND
, BITVECTOR_AND
},
459 {cvc5::Kind::BITVECTOR_OR
, BITVECTOR_OR
},
460 {cvc5::Kind::BITVECTOR_XOR
, BITVECTOR_XOR
},
461 {cvc5::Kind::BITVECTOR_NOT
, BITVECTOR_NOT
},
462 {cvc5::Kind::BITVECTOR_NAND
, BITVECTOR_NAND
},
463 {cvc5::Kind::BITVECTOR_NOR
, BITVECTOR_NOR
},
464 {cvc5::Kind::BITVECTOR_XNOR
, BITVECTOR_XNOR
},
465 {cvc5::Kind::BITVECTOR_COMP
, BITVECTOR_COMP
},
466 {cvc5::Kind::BITVECTOR_MULT
, BITVECTOR_MULT
},
467 {cvc5::Kind::BITVECTOR_ADD
, BITVECTOR_ADD
},
468 {cvc5::Kind::BITVECTOR_SUB
, BITVECTOR_SUB
},
469 {cvc5::Kind::BITVECTOR_NEG
, BITVECTOR_NEG
},
470 {cvc5::Kind::BITVECTOR_UDIV
, BITVECTOR_UDIV
},
471 {cvc5::Kind::BITVECTOR_UREM
, BITVECTOR_UREM
},
472 {cvc5::Kind::BITVECTOR_SDIV
, BITVECTOR_SDIV
},
473 {cvc5::Kind::BITVECTOR_SREM
, BITVECTOR_SREM
},
474 {cvc5::Kind::BITVECTOR_SMOD
, BITVECTOR_SMOD
},
475 {cvc5::Kind::BITVECTOR_SHL
, BITVECTOR_SHL
},
476 {cvc5::Kind::BITVECTOR_LSHR
, BITVECTOR_LSHR
},
477 {cvc5::Kind::BITVECTOR_ASHR
, BITVECTOR_ASHR
},
478 {cvc5::Kind::BITVECTOR_ULT
, BITVECTOR_ULT
},
479 {cvc5::Kind::BITVECTOR_ULE
, BITVECTOR_ULE
},
480 {cvc5::Kind::BITVECTOR_UGT
, BITVECTOR_UGT
},
481 {cvc5::Kind::BITVECTOR_UGE
, BITVECTOR_UGE
},
482 {cvc5::Kind::BITVECTOR_SLT
, BITVECTOR_SLT
},
483 {cvc5::Kind::BITVECTOR_SLE
, BITVECTOR_SLE
},
484 {cvc5::Kind::BITVECTOR_SGT
, BITVECTOR_SGT
},
485 {cvc5::Kind::BITVECTOR_SGE
, BITVECTOR_SGE
},
486 {cvc5::Kind::BITVECTOR_ULTBV
, BITVECTOR_ULTBV
},
487 {cvc5::Kind::BITVECTOR_SLTBV
, BITVECTOR_SLTBV
},
488 {cvc5::Kind::BITVECTOR_ITE
, BITVECTOR_ITE
},
489 {cvc5::Kind::BITVECTOR_REDOR
, BITVECTOR_REDOR
},
490 {cvc5::Kind::BITVECTOR_REDAND
, BITVECTOR_REDAND
},
491 {cvc5::Kind::BITVECTOR_EXTRACT_OP
, BITVECTOR_EXTRACT
},
492 {cvc5::Kind::BITVECTOR_REPEAT_OP
, BITVECTOR_REPEAT
},
493 {cvc5::Kind::BITVECTOR_ZERO_EXTEND_OP
, BITVECTOR_ZERO_EXTEND
},
494 {cvc5::Kind::BITVECTOR_SIGN_EXTEND_OP
, BITVECTOR_SIGN_EXTEND
},
495 {cvc5::Kind::BITVECTOR_ROTATE_LEFT_OP
, BITVECTOR_ROTATE_LEFT
},
496 {cvc5::Kind::BITVECTOR_ROTATE_RIGHT_OP
, BITVECTOR_ROTATE_RIGHT
},
497 {cvc5::Kind::BITVECTOR_EXTRACT
, BITVECTOR_EXTRACT
},
498 {cvc5::Kind::BITVECTOR_REPEAT
, BITVECTOR_REPEAT
},
499 {cvc5::Kind::BITVECTOR_ZERO_EXTEND
, BITVECTOR_ZERO_EXTEND
},
500 {cvc5::Kind::BITVECTOR_SIGN_EXTEND
, BITVECTOR_SIGN_EXTEND
},
501 {cvc5::Kind::BITVECTOR_ROTATE_LEFT
, BITVECTOR_ROTATE_LEFT
},
502 {cvc5::Kind::BITVECTOR_ROTATE_RIGHT
, BITVECTOR_ROTATE_RIGHT
},
503 {cvc5::Kind::INT_TO_BITVECTOR_OP
, INT_TO_BITVECTOR
},
504 {cvc5::Kind::INT_TO_BITVECTOR
, INT_TO_BITVECTOR
},
505 {cvc5::Kind::BITVECTOR_TO_NAT
, BITVECTOR_TO_NAT
},
506 /* FP -------------------------------------------------------------- */
507 {cvc5::Kind::CONST_FLOATINGPOINT
, CONST_FLOATINGPOINT
},
508 {cvc5::Kind::CONST_ROUNDINGMODE
, CONST_ROUNDINGMODE
},
509 {cvc5::Kind::FLOATINGPOINT_FP
, FLOATINGPOINT_FP
},
510 {cvc5::Kind::FLOATINGPOINT_EQ
, FLOATINGPOINT_EQ
},
511 {cvc5::Kind::FLOATINGPOINT_ABS
, FLOATINGPOINT_ABS
},
512 {cvc5::Kind::FLOATINGPOINT_NEG
, FLOATINGPOINT_NEG
},
513 {cvc5::Kind::FLOATINGPOINT_ADD
, FLOATINGPOINT_ADD
},
514 {cvc5::Kind::FLOATINGPOINT_SUB
, FLOATINGPOINT_SUB
},
515 {cvc5::Kind::FLOATINGPOINT_MULT
, FLOATINGPOINT_MULT
},
516 {cvc5::Kind::FLOATINGPOINT_DIV
, FLOATINGPOINT_DIV
},
517 {cvc5::Kind::FLOATINGPOINT_FMA
, FLOATINGPOINT_FMA
},
518 {cvc5::Kind::FLOATINGPOINT_SQRT
, FLOATINGPOINT_SQRT
},
519 {cvc5::Kind::FLOATINGPOINT_REM
, FLOATINGPOINT_REM
},
520 {cvc5::Kind::FLOATINGPOINT_RTI
, FLOATINGPOINT_RTI
},
521 {cvc5::Kind::FLOATINGPOINT_MIN
, FLOATINGPOINT_MIN
},
522 {cvc5::Kind::FLOATINGPOINT_MAX
, FLOATINGPOINT_MAX
},
523 {cvc5::Kind::FLOATINGPOINT_LEQ
, FLOATINGPOINT_LEQ
},
524 {cvc5::Kind::FLOATINGPOINT_LT
, FLOATINGPOINT_LT
},
525 {cvc5::Kind::FLOATINGPOINT_GEQ
, FLOATINGPOINT_GEQ
},
526 {cvc5::Kind::FLOATINGPOINT_GT
, FLOATINGPOINT_GT
},
527 {cvc5::Kind::FLOATINGPOINT_ISN
, FLOATINGPOINT_ISN
},
528 {cvc5::Kind::FLOATINGPOINT_ISSN
, FLOATINGPOINT_ISSN
},
529 {cvc5::Kind::FLOATINGPOINT_ISZ
, FLOATINGPOINT_ISZ
},
530 {cvc5::Kind::FLOATINGPOINT_ISINF
, FLOATINGPOINT_ISINF
},
531 {cvc5::Kind::FLOATINGPOINT_ISNAN
, FLOATINGPOINT_ISNAN
},
532 {cvc5::Kind::FLOATINGPOINT_ISNEG
, FLOATINGPOINT_ISNEG
},
533 {cvc5::Kind::FLOATINGPOINT_ISPOS
, FLOATINGPOINT_ISPOS
},
534 {cvc5::Kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP
,
535 FLOATINGPOINT_TO_FP_IEEE_BITVECTOR
},
536 {cvc5::Kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR
,
537 FLOATINGPOINT_TO_FP_IEEE_BITVECTOR
},
538 {cvc5::Kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP
,
539 FLOATINGPOINT_TO_FP_FLOATINGPOINT
},
540 {cvc5::Kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT
,
541 FLOATINGPOINT_TO_FP_FLOATINGPOINT
},
542 {cvc5::Kind::FLOATINGPOINT_TO_FP_REAL_OP
, FLOATINGPOINT_TO_FP_REAL
},
543 {cvc5::Kind::FLOATINGPOINT_TO_FP_REAL
, FLOATINGPOINT_TO_FP_REAL
},
544 {cvc5::Kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP
,
545 FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR
},
546 {cvc5::Kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR
,
547 FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR
},
548 {cvc5::Kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP
,
549 FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR
},
550 {cvc5::Kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR
,
551 FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR
},
552 {cvc5::Kind::FLOATINGPOINT_TO_FP_GENERIC_OP
,
553 FLOATINGPOINT_TO_FP_GENERIC
},
554 {cvc5::Kind::FLOATINGPOINT_TO_FP_GENERIC
, FLOATINGPOINT_TO_FP_GENERIC
},
555 {cvc5::Kind::FLOATINGPOINT_TO_UBV_OP
, FLOATINGPOINT_TO_UBV
},
556 {cvc5::Kind::FLOATINGPOINT_TO_UBV
, FLOATINGPOINT_TO_UBV
},
557 {cvc5::Kind::FLOATINGPOINT_TO_UBV_TOTAL_OP
, INTERNAL_KIND
},
558 {cvc5::Kind::FLOATINGPOINT_TO_UBV_TOTAL
, INTERNAL_KIND
},
559 {cvc5::Kind::FLOATINGPOINT_TO_SBV_OP
, FLOATINGPOINT_TO_SBV
},
560 {cvc5::Kind::FLOATINGPOINT_TO_SBV
, FLOATINGPOINT_TO_SBV
},
561 {cvc5::Kind::FLOATINGPOINT_TO_SBV_TOTAL_OP
, INTERNAL_KIND
},
562 {cvc5::Kind::FLOATINGPOINT_TO_SBV_TOTAL
, INTERNAL_KIND
},
563 {cvc5::Kind::FLOATINGPOINT_TO_REAL
, FLOATINGPOINT_TO_REAL
},
564 {cvc5::Kind::FLOATINGPOINT_TO_REAL_TOTAL
, INTERNAL_KIND
},
565 /* Arrays ---------------------------------------------------------- */
566 {cvc5::Kind::SELECT
, SELECT
},
567 {cvc5::Kind::STORE
, STORE
},
568 {cvc5::Kind::STORE_ALL
, CONST_ARRAY
},
569 /* Datatypes ------------------------------------------------------- */
570 {cvc5::Kind::APPLY_SELECTOR
, APPLY_SELECTOR
},
571 {cvc5::Kind::APPLY_CONSTRUCTOR
, APPLY_CONSTRUCTOR
},
572 {cvc5::Kind::APPLY_SELECTOR_TOTAL
, INTERNAL_KIND
},
573 {cvc5::Kind::APPLY_TESTER
, APPLY_TESTER
},
574 {cvc5::Kind::APPLY_UPDATER
, APPLY_UPDATER
},
575 {cvc5::Kind::DT_SIZE
, DT_SIZE
},
576 {cvc5::Kind::TUPLE_PROJECT
, TUPLE_PROJECT
},
577 {cvc5::Kind::TUPLE_PROJECT_OP
, TUPLE_PROJECT
},
578 /* Separation Logic ------------------------------------------------ */
579 {cvc5::Kind::SEP_NIL
, SEP_NIL
},
580 {cvc5::Kind::SEP_EMP
, SEP_EMP
},
581 {cvc5::Kind::SEP_PTO
, SEP_PTO
},
582 {cvc5::Kind::SEP_STAR
, SEP_STAR
},
583 {cvc5::Kind::SEP_WAND
, SEP_WAND
},
584 /* Sets ------------------------------------------------------------ */
585 {cvc5::Kind::EMPTYSET
, EMPTYSET
},
586 {cvc5::Kind::UNION
, UNION
},
587 {cvc5::Kind::INTERSECTION
, INTERSECTION
},
588 {cvc5::Kind::SETMINUS
, SETMINUS
},
589 {cvc5::Kind::SUBSET
, SUBSET
},
590 {cvc5::Kind::MEMBER
, MEMBER
},
591 {cvc5::Kind::SINGLETON
, SINGLETON
},
592 {cvc5::Kind::INSERT
, INSERT
},
593 {cvc5::Kind::CARD
, CARD
},
594 {cvc5::Kind::COMPLEMENT
, COMPLEMENT
},
595 {cvc5::Kind::UNIVERSE_SET
, UNIVERSE_SET
},
596 {cvc5::Kind::JOIN
, JOIN
},
597 {cvc5::Kind::PRODUCT
, PRODUCT
},
598 {cvc5::Kind::TRANSPOSE
, TRANSPOSE
},
599 {cvc5::Kind::TCLOSURE
, TCLOSURE
},
600 {cvc5::Kind::JOIN_IMAGE
, JOIN_IMAGE
},
601 {cvc5::Kind::IDEN
, IDEN
},
602 {cvc5::Kind::COMPREHENSION
, COMPREHENSION
},
603 {cvc5::Kind::CHOOSE
, CHOOSE
},
604 {cvc5::Kind::IS_SINGLETON
, IS_SINGLETON
},
605 /* Bags ------------------------------------------------------------ */
606 {cvc5::Kind::UNION_MAX
, UNION_MAX
},
607 {cvc5::Kind::UNION_DISJOINT
, UNION_DISJOINT
},
608 {cvc5::Kind::INTERSECTION_MIN
, INTERSECTION_MIN
},
609 {cvc5::Kind::DIFFERENCE_SUBTRACT
, DIFFERENCE_SUBTRACT
},
610 {cvc5::Kind::DIFFERENCE_REMOVE
, DIFFERENCE_REMOVE
},
611 {cvc5::Kind::SUBBAG
, SUBBAG
},
612 {cvc5::Kind::BAG_COUNT
, BAG_COUNT
},
613 {cvc5::Kind::DUPLICATE_REMOVAL
, DUPLICATE_REMOVAL
},
614 {cvc5::Kind::MK_BAG
, MK_BAG
},
615 {cvc5::Kind::EMPTYBAG
, EMPTYBAG
},
616 {cvc5::Kind::BAG_CARD
, BAG_CARD
},
617 {cvc5::Kind::BAG_CHOOSE
, BAG_CHOOSE
},
618 {cvc5::Kind::BAG_IS_SINGLETON
, BAG_IS_SINGLETON
},
619 {cvc5::Kind::BAG_FROM_SET
, BAG_FROM_SET
},
620 {cvc5::Kind::BAG_TO_SET
, BAG_TO_SET
},
621 {cvc5::Kind::BAG_MAP
,BAG_MAP
},
622 /* Strings --------------------------------------------------------- */
623 {cvc5::Kind::STRING_CONCAT
, STRING_CONCAT
},
624 {cvc5::Kind::STRING_IN_REGEXP
, STRING_IN_REGEXP
},
625 {cvc5::Kind::STRING_LENGTH
, STRING_LENGTH
},
626 {cvc5::Kind::STRING_SUBSTR
, STRING_SUBSTR
},
627 {cvc5::Kind::STRING_UPDATE
, STRING_UPDATE
},
628 {cvc5::Kind::STRING_CHARAT
, STRING_CHARAT
},
629 {cvc5::Kind::STRING_CONTAINS
, STRING_CONTAINS
},
630 {cvc5::Kind::STRING_INDEXOF
, STRING_INDEXOF
},
631 {cvc5::Kind::STRING_INDEXOF_RE
, STRING_INDEXOF_RE
},
632 {cvc5::Kind::STRING_REPLACE
, STRING_REPLACE
},
633 {cvc5::Kind::STRING_REPLACE_ALL
, STRING_REPLACE_ALL
},
634 {cvc5::Kind::STRING_REPLACE_RE
, STRING_REPLACE_RE
},
635 {cvc5::Kind::STRING_REPLACE_RE_ALL
, STRING_REPLACE_RE_ALL
},
636 {cvc5::Kind::STRING_TOLOWER
, STRING_TOLOWER
},
637 {cvc5::Kind::STRING_TOUPPER
, STRING_TOUPPER
},
638 {cvc5::Kind::STRING_REV
, STRING_REV
},
639 {cvc5::Kind::STRING_FROM_CODE
, STRING_FROM_CODE
},
640 {cvc5::Kind::STRING_TO_CODE
, STRING_TO_CODE
},
641 {cvc5::Kind::STRING_LT
, STRING_LT
},
642 {cvc5::Kind::STRING_LEQ
, STRING_LEQ
},
643 {cvc5::Kind::STRING_PREFIX
, STRING_PREFIX
},
644 {cvc5::Kind::STRING_SUFFIX
, STRING_SUFFIX
},
645 {cvc5::Kind::STRING_IS_DIGIT
, STRING_IS_DIGIT
},
646 {cvc5::Kind::STRING_ITOS
, STRING_FROM_INT
},
647 {cvc5::Kind::STRING_STOI
, STRING_TO_INT
},
648 {cvc5::Kind::CONST_STRING
, CONST_STRING
},
649 {cvc5::Kind::STRING_TO_REGEXP
, STRING_TO_REGEXP
},
650 {cvc5::Kind::REGEXP_CONCAT
, REGEXP_CONCAT
},
651 {cvc5::Kind::REGEXP_UNION
, REGEXP_UNION
},
652 {cvc5::Kind::REGEXP_INTER
, REGEXP_INTER
},
653 {cvc5::Kind::REGEXP_DIFF
, REGEXP_DIFF
},
654 {cvc5::Kind::REGEXP_STAR
, REGEXP_STAR
},
655 {cvc5::Kind::REGEXP_PLUS
, REGEXP_PLUS
},
656 {cvc5::Kind::REGEXP_OPT
, REGEXP_OPT
},
657 {cvc5::Kind::REGEXP_RANGE
, REGEXP_RANGE
},
658 {cvc5::Kind::REGEXP_REPEAT
, REGEXP_REPEAT
},
659 {cvc5::Kind::REGEXP_REPEAT_OP
, REGEXP_REPEAT
},
660 {cvc5::Kind::REGEXP_LOOP
, REGEXP_LOOP
},
661 {cvc5::Kind::REGEXP_LOOP_OP
, REGEXP_LOOP
},
662 {cvc5::Kind::REGEXP_EMPTY
, REGEXP_EMPTY
},
663 {cvc5::Kind::REGEXP_SIGMA
, REGEXP_SIGMA
},
664 {cvc5::Kind::REGEXP_COMPLEMENT
, REGEXP_COMPLEMENT
},
665 {cvc5::Kind::CONST_SEQUENCE
, CONST_SEQUENCE
},
666 {cvc5::Kind::SEQ_UNIT
, SEQ_UNIT
},
667 {cvc5::Kind::SEQ_NTH
, SEQ_NTH
},
668 /* Quantifiers ----------------------------------------------------- */
669 {cvc5::Kind::FORALL
, FORALL
},
670 {cvc5::Kind::EXISTS
, EXISTS
},
671 {cvc5::Kind::BOUND_VAR_LIST
, BOUND_VAR_LIST
},
672 {cvc5::Kind::INST_PATTERN
, INST_PATTERN
},
673 {cvc5::Kind::INST_NO_PATTERN
, INST_NO_PATTERN
},
674 {cvc5::Kind::INST_POOL
, INST_POOL
},
675 {cvc5::Kind::INST_ADD_TO_POOL
, INST_ADD_TO_POOL
},
676 {cvc5::Kind::SKOLEM_ADD_TO_POOL
, SKOLEM_ADD_TO_POOL
},
677 {cvc5::Kind::INST_ATTRIBUTE
, INST_ATTRIBUTE
},
678 {cvc5::Kind::INST_PATTERN_LIST
, INST_PATTERN_LIST
},
679 /* ----------------------------------------------------------------- */
680 {cvc5::Kind::LAST_KIND
, LAST_KIND
},
683 /* Set of kinds for indexed operators */
684 const static std::unordered_set
<Kind
> s_indexed_kinds(
688 BITVECTOR_ZERO_EXTEND
,
689 BITVECTOR_SIGN_EXTEND
,
690 BITVECTOR_ROTATE_LEFT
,
691 BITVECTOR_ROTATE_RIGHT
,
693 FLOATINGPOINT_TO_UBV
,
694 FLOATINGPOINT_TO_SBV
,
696 FLOATINGPOINT_TO_FP_IEEE_BITVECTOR
,
697 FLOATINGPOINT_TO_FP_FLOATINGPOINT
,
698 FLOATINGPOINT_TO_FP_REAL
,
699 FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR
,
700 FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR
,
701 FLOATINGPOINT_TO_FP_GENERIC
});
705 /** Convert a cvc5::Kind (internal) to a cvc5::api::Kind (external). */
706 cvc5::api::Kind
intToExtKind(cvc5::Kind k
)
708 auto it
= api::s_kinds_internal
.find(k
);
709 if (it
== api::s_kinds_internal
.end())
711 return api::INTERNAL_KIND
;
716 /** Convert a cvc5::api::Kind (external) to a cvc5::Kind (internal). */
717 cvc5::Kind
extToIntKind(cvc5::api::Kind k
)
719 auto it
= api::s_kinds
.find(k
);
720 if (it
== api::s_kinds
.end())
722 return cvc5::Kind::UNDEFINED_KIND
;
727 /** Return true if given kind is a defined external kind. */
728 bool isDefinedKind(Kind k
) { return k
> UNDEFINED_KIND
&& k
< LAST_KIND
; }
731 * Return true if the internal kind is one where the API term structure
732 * differs from internal structure. This happens for APPLY_* kinds.
733 * The API takes a "higher-order" perspective and treats functions as well
734 * as datatype constructors/selectors/testers as terms
735 * but interally they are not
737 bool isApplyKind(cvc5::Kind k
)
739 return (k
== cvc5::Kind::APPLY_UF
|| k
== cvc5::Kind::APPLY_CONSTRUCTOR
740 || k
== cvc5::Kind::APPLY_SELECTOR
|| k
== cvc5::Kind::APPLY_TESTER
741 || k
== cvc5::Kind::APPLY_UPDATER
);
744 #ifdef CVC5_ASSERTIONS
745 /** Return true if given kind is a defined internal kind. */
746 bool isDefinedIntKind(cvc5::Kind k
)
748 return k
!= cvc5::Kind::UNDEFINED_KIND
&& k
!= cvc5::Kind::LAST_KIND
;
752 /** Return the minimum arity of given kind. */
753 uint32_t minArity(Kind k
)
755 Assert(isDefinedKind(k
));
756 Assert(isDefinedIntKind(extToIntKind(k
)));
757 uint32_t min
= cvc5::kind::metakind::getMinArityForKind(extToIntKind(k
));
759 // At the API level, we treat functions/constructors/selectors/testers as
760 // normal terms instead of making them part of the operator
761 if (isApplyKind(extToIntKind(k
)))
768 /** Return the maximum arity of given kind. */
769 uint32_t maxArity(Kind k
)
771 Assert(isDefinedKind(k
));
772 Assert(isDefinedIntKind(extToIntKind(k
)));
773 uint32_t max
= cvc5::kind::metakind::getMaxArityForKind(extToIntKind(k
));
775 // At the API level, we treat functions/constructors/selectors/testers as
776 // normal terms instead of making them part of the operator
777 if (isApplyKind(extToIntKind(k
))
778 && max
!= std::numeric_limits
<uint32_t>::max()) // be careful not to
788 std::string
kindToString(Kind k
)
790 return k
== INTERNAL_KIND
? "INTERNAL_KIND"
791 : cvc5::kind::kindToString(extToIntKind(k
));
794 const char* toString(Kind k
)
796 return k
== INTERNAL_KIND
? "INTERNAL_KIND"
797 : cvc5::kind::toString(extToIntKind(k
));
800 std::ostream
& operator<<(std::ostream
& out
, Kind k
)
804 case INTERNAL_KIND
: out
<< "INTERNAL_KIND"; break;
805 default: out
<< extToIntKind(k
);
810 /* -------------------------------------------------------------------------- */
811 /* API guard helpers */
812 /* -------------------------------------------------------------------------- */
816 class CVC5ApiExceptionStream
819 CVC5ApiExceptionStream() {}
820 /* Note: This needs to be explicitly set to 'noexcept(false)' since it is
821 * a destructor that throws an exception and in C++11 all destructors
822 * default to noexcept(true) (else this triggers a call to std::terminate). */
823 ~CVC5ApiExceptionStream() noexcept(false)
825 if (std::uncaught_exceptions() == 0)
827 throw CVC5ApiException(d_stream
.str());
831 std::ostream
& ostream() { return d_stream
; }
834 std::stringstream d_stream
;
837 class CVC5ApiRecoverableExceptionStream
840 CVC5ApiRecoverableExceptionStream() {}
841 /* Note: This needs to be explicitly set to 'noexcept(false)' since it is
842 * a destructor that throws an exception and in C++11 all destructors
843 * default to noexcept(true) (else this triggers a call to std::terminate). */
844 ~CVC5ApiRecoverableExceptionStream() noexcept(false)
846 if (std::uncaught_exceptions() == 0)
848 throw CVC5ApiRecoverableException(d_stream
.str());
852 std::ostream
& ostream() { return d_stream
; }
855 std::stringstream d_stream
;
858 #define CVC5_API_TRY_CATCH_BEGIN \
861 #define CVC5_API_TRY_CATCH_END \
863 catch (const OptionException& e) \
865 throw CVC5ApiOptionException(e.getMessage()); \
867 catch (const cvc5::RecoverableModalException& e) \
869 throw CVC5ApiRecoverableException(e.getMessage()); \
871 catch (const cvc5::Exception& e) { throw CVC5ApiException(e.getMessage()); } \
872 catch (const std::invalid_argument& e) { throw CVC5ApiException(e.what()); }
876 /* -------------------------------------------------------------------------- */
878 /* -------------------------------------------------------------------------- */
880 Result::Result(const cvc5::Result
& r
) : d_result(new cvc5::Result(r
)) {}
882 Result::Result() : d_result(new cvc5::Result()) {}
884 bool Result::isNull() const
886 return d_result
->getType() == cvc5::Result::TYPE_NONE
;
889 bool Result::isSat(void) const
891 return d_result
->getType() == cvc5::Result::TYPE_SAT
892 && d_result
->isSat() == cvc5::Result::SAT
;
895 bool Result::isUnsat(void) const
897 return d_result
->getType() == cvc5::Result::TYPE_SAT
898 && d_result
->isSat() == cvc5::Result::UNSAT
;
901 bool Result::isSatUnknown(void) const
903 return d_result
->getType() == cvc5::Result::TYPE_SAT
904 && d_result
->isSat() == cvc5::Result::SAT_UNKNOWN
;
907 bool Result::isEntailed(void) const
909 return d_result
->getType() == cvc5::Result::TYPE_ENTAILMENT
910 && d_result
->isEntailed() == cvc5::Result::ENTAILED
;
913 bool Result::isNotEntailed(void) const
915 return d_result
->getType() == cvc5::Result::TYPE_ENTAILMENT
916 && d_result
->isEntailed() == cvc5::Result::NOT_ENTAILED
;
919 bool Result::isEntailmentUnknown(void) const
921 return d_result
->getType() == cvc5::Result::TYPE_ENTAILMENT
922 && d_result
->isEntailed() == cvc5::Result::ENTAILMENT_UNKNOWN
;
925 bool Result::operator==(const Result
& r
) const
927 return *d_result
== *r
.d_result
;
930 bool Result::operator!=(const Result
& r
) const
932 return *d_result
!= *r
.d_result
;
935 Result::UnknownExplanation
Result::getUnknownExplanation(void) const
937 cvc5::Result::UnknownExplanation expl
= d_result
->whyUnknown();
940 case cvc5::Result::REQUIRES_FULL_CHECK
: return REQUIRES_FULL_CHECK
;
941 case cvc5::Result::INCOMPLETE
: return INCOMPLETE
;
942 case cvc5::Result::TIMEOUT
: return TIMEOUT
;
943 case cvc5::Result::RESOURCEOUT
: return RESOURCEOUT
;
944 case cvc5::Result::MEMOUT
: return MEMOUT
;
945 case cvc5::Result::INTERRUPTED
: return INTERRUPTED
;
946 case cvc5::Result::NO_STATUS
: return NO_STATUS
;
947 case cvc5::Result::UNSUPPORTED
: return UNSUPPORTED
;
948 case cvc5::Result::OTHER
: return OTHER
;
949 default: return UNKNOWN_REASON
;
951 return UNKNOWN_REASON
;
954 std::string
Result::toString(void) const { return d_result
->toString(); }
956 std::ostream
& operator<<(std::ostream
& out
, const Result
& r
)
962 std::ostream
& operator<<(std::ostream
& out
, enum Result::UnknownExplanation e
)
966 case Result::REQUIRES_FULL_CHECK
: out
<< "REQUIRES_FULL_CHECK"; break;
967 case Result::INCOMPLETE
: out
<< "INCOMPLETE"; break;
968 case Result::TIMEOUT
: out
<< "TIMEOUT"; break;
969 case Result::RESOURCEOUT
: out
<< "RESOURCEOUT"; break;
970 case Result::MEMOUT
: out
<< "MEMOUT"; break;
971 case Result::INTERRUPTED
: out
<< "INTERRUPTED"; break;
972 case Result::NO_STATUS
: out
<< "NO_STATUS"; break;
973 case Result::UNSUPPORTED
: out
<< "UNSUPPORTED"; break;
974 case Result::OTHER
: out
<< "OTHER"; break;
975 case Result::UNKNOWN_REASON
: out
<< "UNKNOWN_REASON"; break;
976 default: Unhandled() << e
;
981 /* -------------------------------------------------------------------------- */
983 /* -------------------------------------------------------------------------- */
985 Sort::Sort(const Solver
* slv
, const cvc5::TypeNode
& t
)
986 : d_solver(slv
), d_type(new cvc5::TypeNode(t
))
990 Sort::Sort() : d_solver(nullptr), d_type(new cvc5::TypeNode()) {}
994 if (d_solver
!= nullptr)
1000 std::set
<TypeNode
> Sort::sortSetToTypeNodes(const std::set
<Sort
>& sorts
)
1002 std::set
<TypeNode
> types
;
1003 for (const Sort
& s
: sorts
)
1005 types
.insert(s
.getTypeNode());
1010 std::vector
<TypeNode
> Sort::sortVectorToTypeNodes(
1011 const std::vector
<Sort
>& sorts
)
1013 std::vector
<TypeNode
> typeNodes
;
1014 for (const Sort
& sort
: sorts
)
1016 typeNodes
.push_back(sort
.getTypeNode());
1021 std::vector
<Sort
> Sort::typeNodeVectorToSorts(
1022 const Solver
* slv
, const std::vector
<TypeNode
>& types
)
1024 std::vector
<Sort
> sorts
;
1025 for (size_t i
= 0, tsize
= types
.size(); i
< tsize
; i
++)
1027 sorts
.push_back(Sort(slv
, types
[i
]));
1032 bool Sort::operator==(const Sort
& s
) const
1034 CVC5_API_TRY_CATCH_BEGIN
;
1035 //////// all checks before this line
1036 return *d_type
== *s
.d_type
;
1038 CVC5_API_TRY_CATCH_END
;
1041 bool Sort::operator!=(const Sort
& s
) const
1043 CVC5_API_TRY_CATCH_BEGIN
;
1044 //////// all checks before this line
1045 return *d_type
!= *s
.d_type
;
1047 CVC5_API_TRY_CATCH_END
;
1050 bool Sort::operator<(const Sort
& s
) const
1052 CVC5_API_TRY_CATCH_BEGIN
;
1053 //////// all checks before this line
1054 return *d_type
< *s
.d_type
;
1056 CVC5_API_TRY_CATCH_END
;
1059 bool Sort::operator>(const Sort
& s
) const
1061 CVC5_API_TRY_CATCH_BEGIN
;
1062 //////// all checks before this line
1063 return *d_type
> *s
.d_type
;
1065 CVC5_API_TRY_CATCH_END
;
1068 bool Sort::operator<=(const Sort
& s
) const
1070 CVC5_API_TRY_CATCH_BEGIN
;
1071 //////// all checks before this line
1072 return *d_type
<= *s
.d_type
;
1074 CVC5_API_TRY_CATCH_END
;
1077 bool Sort::operator>=(const Sort
& s
) const
1079 CVC5_API_TRY_CATCH_BEGIN
;
1080 //////// all checks before this line
1081 return *d_type
>= *s
.d_type
;
1083 CVC5_API_TRY_CATCH_END
;
1086 bool Sort::isNull() const
1088 CVC5_API_TRY_CATCH_BEGIN
;
1089 //////// all checks before this line
1090 return isNullHelper();
1092 CVC5_API_TRY_CATCH_END
;
1095 bool Sort::isBoolean() const
1097 CVC5_API_TRY_CATCH_BEGIN
;
1098 //////// all checks before this line
1099 return d_type
->isBoolean();
1101 CVC5_API_TRY_CATCH_END
;
1104 bool Sort::isInteger() const
1106 CVC5_API_TRY_CATCH_BEGIN
;
1107 //////// all checks before this line
1108 return d_type
->isInteger();
1110 CVC5_API_TRY_CATCH_END
;
1113 bool Sort::isReal() const
1115 CVC5_API_TRY_CATCH_BEGIN
;
1116 //////// all checks before this line
1117 // notice that we do not expose internal subtyping to the user
1118 return d_type
->isReal() && !d_type
->isInteger();
1120 CVC5_API_TRY_CATCH_END
;
1123 bool Sort::isString() const
1125 CVC5_API_TRY_CATCH_BEGIN
;
1126 //////// all checks before this line
1127 return d_type
->isString();
1129 CVC5_API_TRY_CATCH_END
;
1132 bool Sort::isRegExp() const
1134 CVC5_API_TRY_CATCH_BEGIN
;
1135 //////// all checks before this line
1136 return d_type
->isRegExp();
1138 CVC5_API_TRY_CATCH_END
;
1141 bool Sort::isRoundingMode() const
1143 CVC5_API_TRY_CATCH_BEGIN
;
1144 //////// all checks before this line
1145 return d_type
->isRoundingMode();
1147 CVC5_API_TRY_CATCH_END
;
1150 bool Sort::isBitVector() const
1152 CVC5_API_TRY_CATCH_BEGIN
;
1153 //////// all checks before this line
1154 return d_type
->isBitVector();
1156 CVC5_API_TRY_CATCH_END
;
1159 bool Sort::isFloatingPoint() const
1161 CVC5_API_TRY_CATCH_BEGIN
;
1162 //////// all checks before this line
1163 return d_type
->isFloatingPoint();
1165 CVC5_API_TRY_CATCH_END
;
1168 bool Sort::isDatatype() const
1170 CVC5_API_TRY_CATCH_BEGIN
;
1171 //////// all checks before this line
1172 return d_type
->isDatatype();
1174 CVC5_API_TRY_CATCH_END
;
1177 bool Sort::isParametricDatatype() const
1179 CVC5_API_TRY_CATCH_BEGIN
;
1180 //////// all checks before this line
1181 if (!d_type
->isDatatype()) return false;
1182 return d_type
->isParametricDatatype();
1184 CVC5_API_TRY_CATCH_END
;
1187 bool Sort::isConstructor() const
1189 CVC5_API_TRY_CATCH_BEGIN
;
1190 //////// all checks before this line
1191 return d_type
->isConstructor();
1193 CVC5_API_TRY_CATCH_END
;
1196 bool Sort::isSelector() const
1198 CVC5_API_TRY_CATCH_BEGIN
;
1199 //////// all checks before this line
1200 return d_type
->isSelector();
1202 CVC5_API_TRY_CATCH_END
;
1205 bool Sort::isTester() const
1207 CVC5_API_TRY_CATCH_BEGIN
;
1208 //////// all checks before this line
1209 return d_type
->isTester();
1211 CVC5_API_TRY_CATCH_END
;
1214 bool Sort::isUpdater() const
1216 CVC5_API_TRY_CATCH_BEGIN
;
1217 //////// all checks before this line
1218 return d_type
->isUpdater();
1220 CVC5_API_TRY_CATCH_END
;
1223 bool Sort::isFunction() const
1225 CVC5_API_TRY_CATCH_BEGIN
;
1226 //////// all checks before this line
1227 return d_type
->isFunction();
1229 CVC5_API_TRY_CATCH_END
;
1232 bool Sort::isPredicate() const
1234 CVC5_API_TRY_CATCH_BEGIN
;
1235 //////// all checks before this line
1236 return d_type
->isPredicate();
1238 CVC5_API_TRY_CATCH_END
;
1241 bool Sort::isTuple() const
1243 CVC5_API_TRY_CATCH_BEGIN
;
1244 //////// all checks before this line
1245 return d_type
->isTuple();
1247 CVC5_API_TRY_CATCH_END
;
1250 bool Sort::isRecord() const
1252 CVC5_API_TRY_CATCH_BEGIN
;
1253 //////// all checks before this line
1254 return d_type
->isRecord();
1256 CVC5_API_TRY_CATCH_END
;
1259 bool Sort::isArray() const
1261 CVC5_API_TRY_CATCH_BEGIN
;
1262 //////// all checks before this line
1263 return d_type
->isArray();
1265 CVC5_API_TRY_CATCH_END
;
1268 bool Sort::isSet() const
1270 CVC5_API_TRY_CATCH_BEGIN
;
1271 //////// all checks before this line
1272 return d_type
->isSet();
1274 CVC5_API_TRY_CATCH_END
;
1277 bool Sort::isBag() const
1279 CVC5_API_TRY_CATCH_BEGIN
;
1280 //////// all checks before this line
1281 return d_type
->isBag();
1283 CVC5_API_TRY_CATCH_END
;
1286 bool Sort::isSequence() const
1288 CVC5_API_TRY_CATCH_BEGIN
;
1289 //////// all checks before this line
1290 return d_type
->isSequence();
1292 CVC5_API_TRY_CATCH_END
;
1295 bool Sort::isUninterpretedSort() const
1297 CVC5_API_TRY_CATCH_BEGIN
;
1298 //////// all checks before this line
1299 return d_type
->isSort();
1301 CVC5_API_TRY_CATCH_END
;
1304 bool Sort::isSortConstructor() const
1306 CVC5_API_TRY_CATCH_BEGIN
;
1307 //////// all checks before this line
1308 return d_type
->isSortConstructor();
1310 CVC5_API_TRY_CATCH_END
;
1313 bool Sort::isFirstClass() const
1315 CVC5_API_TRY_CATCH_BEGIN
;
1316 //////// all checks before this line
1317 return d_type
->isFirstClass();
1319 CVC5_API_TRY_CATCH_END
;
1322 bool Sort::isFunctionLike() const
1324 CVC5_API_TRY_CATCH_BEGIN
;
1325 //////// all checks before this line
1326 return d_type
->isFunctionLike();
1328 CVC5_API_TRY_CATCH_END
;
1331 bool Sort::isSubsortOf(const Sort
& s
) const
1333 CVC5_API_TRY_CATCH_BEGIN
;
1334 CVC5_API_ARG_CHECK_SOLVER("sort", s
);
1335 //////// all checks before this line
1336 return d_type
->isSubtypeOf(*s
.d_type
);
1338 CVC5_API_TRY_CATCH_END
;
1341 bool Sort::isComparableTo(const Sort
& s
) const
1343 CVC5_API_TRY_CATCH_BEGIN
;
1344 CVC5_API_ARG_CHECK_SOLVER("sort", s
);
1345 //////// all checks before this line
1346 return d_type
->isComparableTo(*s
.d_type
);
1348 CVC5_API_TRY_CATCH_END
;
1351 Datatype
Sort::getDatatype() const
1353 CVC5_API_TRY_CATCH_BEGIN
;
1354 CVC5_API_CHECK_NOT_NULL
;
1355 CVC5_API_CHECK(isDatatype()) << "Expected datatype sort.";
1356 //////// all checks before this line
1357 return Datatype(d_solver
, d_type
->getDType());
1359 CVC5_API_TRY_CATCH_END
;
1362 Sort
Sort::instantiate(const std::vector
<Sort
>& params
) const
1364 CVC5_API_TRY_CATCH_BEGIN
;
1365 CVC5_API_CHECK_NOT_NULL
;
1366 CVC5_API_CHECK_SORTS(params
);
1367 CVC5_API_CHECK(isParametricDatatype() || isSortConstructor())
1368 << "Expected parametric datatype or sort constructor sort.";
1369 //////// all checks before this line
1370 std::vector
<cvc5::TypeNode
> tparams
= sortVectorToTypeNodes(params
);
1371 if (d_type
->isDatatype())
1373 return Sort(d_solver
, d_type
->instantiateParametricDatatype(tparams
));
1375 Assert(d_type
->isSortConstructor());
1376 return Sort(d_solver
, d_solver
->getNodeManager()->mkSort(*d_type
, tparams
));
1378 CVC5_API_TRY_CATCH_END
;
1381 Sort
Sort::substitute(const Sort
& sort
, const Sort
& replacement
) const
1383 CVC5_API_TRY_CATCH_BEGIN
;
1384 CVC5_API_CHECK_NOT_NULL
;
1385 CVC5_API_CHECK_SORT(sort
);
1386 CVC5_API_CHECK_SORT(replacement
);
1387 //////// all checks before this line
1390 d_type
->substitute(sort
.getTypeNode(), replacement
.getTypeNode()));
1392 CVC5_API_TRY_CATCH_END
;
1395 Sort
Sort::substitute(const std::vector
<Sort
>& sorts
,
1396 const std::vector
<Sort
>& replacements
) const
1398 CVC5_API_TRY_CATCH_BEGIN
;
1399 CVC5_API_CHECK_NOT_NULL
;
1400 CVC5_API_CHECK_SORTS(sorts
);
1401 CVC5_API_CHECK_SORTS(replacements
);
1402 //////// all checks before this line
1404 std::vector
<cvc5::TypeNode
> tSorts
= sortVectorToTypeNodes(sorts
),
1406 sortVectorToTypeNodes(replacements
);
1407 return Sort(d_solver
,
1408 d_type
->substitute(tSorts
.begin(),
1410 tReplacements
.begin(),
1411 tReplacements
.end()));
1413 CVC5_API_TRY_CATCH_END
;
1416 std::string
Sort::toString() const
1418 CVC5_API_TRY_CATCH_BEGIN
;
1419 //////// all checks before this line
1420 if (d_solver
!= nullptr)
1422 return d_type
->toString();
1424 return d_type
->toString();
1426 CVC5_API_TRY_CATCH_END
;
1429 const cvc5::TypeNode
& Sort::getTypeNode(void) const { return *d_type
; }
1431 /* Constructor sort ------------------------------------------------------- */
1433 size_t Sort::getConstructorArity() const
1435 CVC5_API_TRY_CATCH_BEGIN
;
1436 CVC5_API_CHECK_NOT_NULL
;
1437 CVC5_API_CHECK(isConstructor()) << "Not a constructor sort: " << (*this);
1438 //////// all checks before this line
1439 return d_type
->getNumChildren() - 1;
1441 CVC5_API_TRY_CATCH_END
;
1444 std::vector
<Sort
> Sort::getConstructorDomainSorts() const
1446 CVC5_API_TRY_CATCH_BEGIN
;
1447 CVC5_API_CHECK_NOT_NULL
;
1448 CVC5_API_CHECK(isConstructor()) << "Not a constructor sort: " << (*this);
1449 //////// all checks before this line
1450 return typeNodeVectorToSorts(d_solver
, d_type
->getArgTypes());
1452 CVC5_API_TRY_CATCH_END
;
1455 Sort
Sort::getConstructorCodomainSort() const
1457 CVC5_API_TRY_CATCH_BEGIN
;
1458 CVC5_API_CHECK_NOT_NULL
;
1459 CVC5_API_CHECK(isConstructor()) << "Not a constructor sort: " << (*this);
1460 //////// all checks before this line
1461 return Sort(d_solver
, d_type
->getConstructorRangeType());
1463 CVC5_API_TRY_CATCH_END
;
1466 /* Selector sort ------------------------------------------------------- */
1468 Sort
Sort::getSelectorDomainSort() const
1470 CVC5_API_TRY_CATCH_BEGIN
;
1471 CVC5_API_CHECK_NOT_NULL
;
1472 CVC5_API_CHECK(isSelector()) << "Not a selector sort: " << (*this);
1473 //////// all checks before this line
1474 return Sort(d_solver
, d_type
->getSelectorDomainType());
1476 CVC5_API_TRY_CATCH_END
;
1479 Sort
Sort::getSelectorCodomainSort() const
1481 CVC5_API_TRY_CATCH_BEGIN
;
1482 CVC5_API_CHECK_NOT_NULL
;
1483 CVC5_API_CHECK(isSelector()) << "Not a selector sort: " << (*this);
1484 //////// all checks before this line
1485 return Sort(d_solver
, d_type
->getSelectorRangeType());
1487 CVC5_API_TRY_CATCH_END
;
1490 /* Tester sort ------------------------------------------------------- */
1492 Sort
Sort::getTesterDomainSort() const
1494 CVC5_API_TRY_CATCH_BEGIN
;
1495 CVC5_API_CHECK_NOT_NULL
;
1496 CVC5_API_CHECK(isTester()) << "Not a tester sort: " << (*this);
1497 //////// all checks before this line
1498 return Sort(d_solver
, d_type
->getTesterDomainType());
1500 CVC5_API_TRY_CATCH_END
;
1503 Sort
Sort::getTesterCodomainSort() const
1505 CVC5_API_TRY_CATCH_BEGIN
;
1506 CVC5_API_CHECK_NOT_NULL
;
1507 CVC5_API_CHECK(isTester()) << "Not a tester sort: " << (*this);
1508 //////// all checks before this line
1509 return d_solver
->getBooleanSort();
1511 CVC5_API_TRY_CATCH_END
;
1514 /* Function sort ------------------------------------------------------- */
1516 size_t Sort::getFunctionArity() const
1518 CVC5_API_TRY_CATCH_BEGIN
;
1519 CVC5_API_CHECK_NOT_NULL
;
1520 CVC5_API_CHECK(isFunction()) << "Not a function sort: " << (*this);
1521 //////// all checks before this line
1522 return d_type
->getNumChildren() - 1;
1524 CVC5_API_TRY_CATCH_END
;
1527 std::vector
<Sort
> Sort::getFunctionDomainSorts() const
1529 CVC5_API_TRY_CATCH_BEGIN
;
1530 CVC5_API_CHECK_NOT_NULL
;
1531 CVC5_API_CHECK(isFunction()) << "Not a function sort: " << (*this);
1532 //////// all checks before this line
1533 return typeNodeVectorToSorts(d_solver
, d_type
->getArgTypes());
1535 CVC5_API_TRY_CATCH_END
;
1538 Sort
Sort::getFunctionCodomainSort() const
1540 CVC5_API_TRY_CATCH_BEGIN
;
1541 CVC5_API_CHECK_NOT_NULL
;
1542 CVC5_API_CHECK(isFunction()) << "Not a function sort" << (*this);
1543 //////// all checks before this line
1544 return Sort(d_solver
, d_type
->getRangeType());
1546 CVC5_API_TRY_CATCH_END
;
1549 /* Array sort ---------------------------------------------------------- */
1551 Sort
Sort::getArrayIndexSort() const
1553 CVC5_API_TRY_CATCH_BEGIN
;
1554 CVC5_API_CHECK_NOT_NULL
;
1555 CVC5_API_CHECK(isArray()) << "Not an array sort.";
1556 //////// all checks before this line
1557 return Sort(d_solver
, d_type
->getArrayIndexType());
1559 CVC5_API_TRY_CATCH_END
;
1562 Sort
Sort::getArrayElementSort() const
1564 CVC5_API_TRY_CATCH_BEGIN
;
1565 CVC5_API_CHECK_NOT_NULL
;
1566 CVC5_API_CHECK(isArray()) << "Not an array sort.";
1567 //////// all checks before this line
1568 return Sort(d_solver
, d_type
->getArrayConstituentType());
1570 CVC5_API_TRY_CATCH_END
;
1573 /* Set sort ------------------------------------------------------------ */
1575 Sort
Sort::getSetElementSort() const
1577 CVC5_API_TRY_CATCH_BEGIN
;
1578 CVC5_API_CHECK_NOT_NULL
;
1579 CVC5_API_CHECK(isSet()) << "Not a set sort.";
1580 //////// all checks before this line
1581 return Sort(d_solver
, d_type
->getSetElementType());
1583 CVC5_API_TRY_CATCH_END
;
1586 /* Bag sort ------------------------------------------------------------ */
1588 Sort
Sort::getBagElementSort() const
1590 CVC5_API_TRY_CATCH_BEGIN
;
1591 CVC5_API_CHECK_NOT_NULL
;
1592 CVC5_API_CHECK(isBag()) << "Not a bag sort.";
1593 //////// all checks before this line
1594 return Sort(d_solver
, d_type
->getBagElementType());
1596 CVC5_API_TRY_CATCH_END
;
1599 /* Sequence sort ------------------------------------------------------- */
1601 Sort
Sort::getSequenceElementSort() const
1603 CVC5_API_TRY_CATCH_BEGIN
;
1604 CVC5_API_CHECK_NOT_NULL
;
1605 CVC5_API_CHECK(isSequence()) << "Not a sequence sort.";
1606 //////// all checks before this line
1607 return Sort(d_solver
, d_type
->getSequenceElementType());
1609 CVC5_API_TRY_CATCH_END
;
1612 /* Uninterpreted sort -------------------------------------------------- */
1614 std::string
Sort::getUninterpretedSortName() const
1616 CVC5_API_TRY_CATCH_BEGIN
;
1617 CVC5_API_CHECK_NOT_NULL
;
1618 CVC5_API_CHECK(isUninterpretedSort()) << "Not an uninterpreted sort.";
1619 //////// all checks before this line
1620 return d_type
->getName();
1622 CVC5_API_TRY_CATCH_END
;
1625 bool Sort::isUninterpretedSortParameterized() const
1627 CVC5_API_TRY_CATCH_BEGIN
;
1628 CVC5_API_CHECK_NOT_NULL
;
1629 CVC5_API_CHECK(isUninterpretedSort()) << "Not an uninterpreted sort.";
1630 //////// all checks before this line
1632 /* This method is not implemented in the NodeManager, since whether a
1633 * uninterpreted sort is parameterized is irrelevant for solving. */
1634 return d_type
->getNumChildren() > 0;
1636 CVC5_API_TRY_CATCH_END
;
1639 std::vector
<Sort
> Sort::getUninterpretedSortParamSorts() const
1641 CVC5_API_TRY_CATCH_BEGIN
;
1642 CVC5_API_CHECK_NOT_NULL
;
1643 CVC5_API_CHECK(isUninterpretedSort()) << "Not an uninterpreted sort.";
1644 //////// all checks before this line
1646 /* This method is not implemented in the NodeManager, since whether a
1647 * uninterpreted sort is parameterized is irrelevant for solving. */
1648 std::vector
<TypeNode
> params
;
1649 for (size_t i
= 0, nchildren
= d_type
->getNumChildren(); i
< nchildren
; i
++)
1651 params
.push_back((*d_type
)[i
]);
1653 return typeNodeVectorToSorts(d_solver
, params
);
1655 CVC5_API_TRY_CATCH_END
;
1658 /* Sort constructor sort ----------------------------------------------- */
1660 std::string
Sort::getSortConstructorName() const
1662 CVC5_API_TRY_CATCH_BEGIN
;
1663 CVC5_API_CHECK_NOT_NULL
;
1664 CVC5_API_CHECK(isSortConstructor()) << "Not a sort constructor sort.";
1665 //////// all checks before this line
1666 return d_type
->getName();
1668 CVC5_API_TRY_CATCH_END
;
1671 size_t Sort::getSortConstructorArity() const
1673 CVC5_API_TRY_CATCH_BEGIN
;
1674 CVC5_API_CHECK_NOT_NULL
;
1675 CVC5_API_CHECK(isSortConstructor()) << "Not a sort constructor sort.";
1676 //////// all checks before this line
1677 return d_type
->getSortConstructorArity();
1679 CVC5_API_TRY_CATCH_END
;
1682 /* Bit-vector sort ----------------------------------------------------- */
1684 uint32_t Sort::getBitVectorSize() const
1686 CVC5_API_TRY_CATCH_BEGIN
;
1687 CVC5_API_CHECK_NOT_NULL
;
1688 CVC5_API_CHECK(isBitVector()) << "Not a bit-vector sort.";
1689 //////// all checks before this line
1690 return d_type
->getBitVectorSize();
1692 CVC5_API_TRY_CATCH_END
;
1695 /* Floating-point sort ------------------------------------------------- */
1697 uint32_t Sort::getFloatingPointExponentSize() const
1699 CVC5_API_TRY_CATCH_BEGIN
;
1700 CVC5_API_CHECK_NOT_NULL
;
1701 CVC5_API_CHECK(isFloatingPoint()) << "Not a floating-point sort.";
1702 //////// all checks before this line
1703 return d_type
->getFloatingPointExponentSize();
1705 CVC5_API_TRY_CATCH_END
;
1708 uint32_t Sort::getFloatingPointSignificandSize() const
1710 CVC5_API_TRY_CATCH_BEGIN
;
1711 CVC5_API_CHECK_NOT_NULL
;
1712 CVC5_API_CHECK(isFloatingPoint()) << "Not a floating-point sort.";
1713 //////// all checks before this line
1714 return d_type
->getFloatingPointSignificandSize();
1716 CVC5_API_TRY_CATCH_END
;
1719 /* Datatype sort ------------------------------------------------------- */
1721 std::vector
<Sort
> Sort::getDatatypeParamSorts() const
1723 CVC5_API_TRY_CATCH_BEGIN
;
1724 CVC5_API_CHECK_NOT_NULL
;
1725 CVC5_API_CHECK(isParametricDatatype()) << "Not a parametric datatype sort.";
1726 //////// all checks before this line
1727 return typeNodeVectorToSorts(d_solver
, d_type
->getParamTypes());
1729 CVC5_API_TRY_CATCH_END
;
1732 size_t Sort::getDatatypeArity() const
1734 CVC5_API_TRY_CATCH_BEGIN
;
1735 CVC5_API_CHECK_NOT_NULL
;
1736 CVC5_API_CHECK(isDatatype()) << "Not a datatype sort.";
1737 //////// all checks before this line
1738 return d_type
->getNumChildren() - 1;
1740 CVC5_API_TRY_CATCH_END
;
1743 /* Tuple sort ---------------------------------------------------------- */
1745 size_t Sort::getTupleLength() const
1747 CVC5_API_TRY_CATCH_BEGIN
;
1748 CVC5_API_CHECK_NOT_NULL
;
1749 CVC5_API_CHECK(isTuple()) << "Not a tuple sort.";
1750 //////// all checks before this line
1751 return d_type
->getTupleLength();
1753 CVC5_API_TRY_CATCH_END
;
1756 std::vector
<Sort
> Sort::getTupleSorts() const
1758 CVC5_API_TRY_CATCH_BEGIN
;
1759 CVC5_API_CHECK_NOT_NULL
;
1760 CVC5_API_CHECK(isTuple()) << "Not a tuple sort.";
1761 //////// all checks before this line
1762 return typeNodeVectorToSorts(d_solver
, d_type
->getTupleTypes());
1764 CVC5_API_TRY_CATCH_END
;
1767 /* --------------------------------------------------------------------- */
1769 std::ostream
& operator<<(std::ostream
& out
, const Sort
& s
)
1771 out
<< s
.toString();
1776 /* -------------------------------------------------------------------------- */
1778 /* Split out to avoid nested API calls (problematic with API tracing). */
1779 /* .......................................................................... */
1781 bool Sort::isNullHelper() const { return d_type
->isNull(); }
1783 /* -------------------------------------------------------------------------- */
1785 /* -------------------------------------------------------------------------- */
1787 Op::Op() : d_solver(nullptr), d_kind(NULL_EXPR
), d_node(new cvc5::Node()) {}
1789 Op::Op(const Solver
* slv
, const Kind k
)
1790 : d_solver(slv
), d_kind(k
), d_node(new cvc5::Node())
1794 Op::Op(const Solver
* slv
, const Kind k
, const cvc5::Node
& n
)
1795 : d_solver(slv
), d_kind(k
), d_node(new cvc5::Node(n
))
1801 if (d_solver
!= nullptr)
1803 // Ensure that the correct node manager is in scope when the type node is
1809 /* Public methods */
1810 bool Op::operator==(const Op
& t
) const
1812 CVC5_API_TRY_CATCH_BEGIN
;
1813 //////// all checks before this line
1814 if (d_node
->isNull() && t
.d_node
->isNull())
1816 return (d_kind
== t
.d_kind
);
1818 else if (d_node
->isNull() || t
.d_node
->isNull())
1822 return (d_kind
== t
.d_kind
) && (*d_node
== *t
.d_node
);
1824 CVC5_API_TRY_CATCH_END
;
1827 bool Op::operator!=(const Op
& t
) const
1829 CVC5_API_TRY_CATCH_BEGIN
;
1830 //////// all checks before this line
1831 return !(*this == t
);
1833 CVC5_API_TRY_CATCH_END
;
1836 Kind
Op::getKind() const
1838 CVC5_API_CHECK(d_kind
!= NULL_EXPR
) << "Expecting a non-null Kind";
1839 //////// all checks before this line
1843 bool Op::isNull() const
1845 CVC5_API_TRY_CATCH_BEGIN
;
1846 //////// all checks before this line
1847 return isNullHelper();
1849 CVC5_API_TRY_CATCH_END
;
1852 bool Op::isIndexed() const
1854 CVC5_API_TRY_CATCH_BEGIN
;
1855 //////// all checks before this line
1856 return isIndexedHelper();
1858 CVC5_API_TRY_CATCH_END
;
1861 size_t Op::getNumIndices() const
1863 CVC5_API_TRY_CATCH_BEGIN
;
1864 CVC5_API_CHECK_NOT_NULL
;
1865 //////// all checks before this line
1866 return getNumIndicesHelper();
1868 CVC5_API_TRY_CATCH_END
;
1871 size_t Op::getNumIndicesHelper() const
1873 if (!isIndexedHelper())
1878 Kind k
= intToExtKind(d_node
->getKind());
1882 case DIVISIBLE
: size
= 1; break;
1883 case BITVECTOR_REPEAT
: size
= 1; break;
1884 case BITVECTOR_ZERO_EXTEND
: size
= 1; break;
1885 case BITVECTOR_SIGN_EXTEND
: size
= 1; break;
1886 case BITVECTOR_ROTATE_LEFT
: size
= 1; break;
1887 case BITVECTOR_ROTATE_RIGHT
: size
= 1; break;
1888 case INT_TO_BITVECTOR
: size
= 1; break;
1889 case IAND
: size
= 1; break;
1890 case FLOATINGPOINT_TO_UBV
: size
= 1; break;
1891 case FLOATINGPOINT_TO_SBV
: size
= 1; break;
1892 case REGEXP_REPEAT
: size
= 1; break;
1893 case BITVECTOR_EXTRACT
: size
= 2; break;
1894 case FLOATINGPOINT_TO_FP_IEEE_BITVECTOR
: size
= 2; break;
1895 case FLOATINGPOINT_TO_FP_FLOATINGPOINT
: size
= 2; break;
1896 case FLOATINGPOINT_TO_FP_REAL
: size
= 2; break;
1897 case FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR
: size
= 2; break;
1898 case FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR
: size
= 2; break;
1899 case FLOATINGPOINT_TO_FP_GENERIC
: size
= 2; break;
1900 case REGEXP_LOOP
: size
= 2; break;
1902 size
= d_node
->getConst
<TupleProjectOp
>().getIndices().size();
1904 default: CVC5_API_CHECK(false) << "Unhandled kind " << kindToString(k
);
1909 Term
Op::operator[](size_t index
) const
1911 return getIndexHelper(index
);
1914 Term
Op::getIndexHelper(size_t index
) const
1916 CVC5_API_TRY_CATCH_BEGIN
;
1917 CVC5_API_CHECK_NOT_NULL
;
1918 CVC5_API_CHECK(!d_node
->isNull())
1919 << "Expecting a non-null internal expression. This Op is not indexed.";
1920 CVC5_API_CHECK(index
< getNumIndicesHelper()) << "index out of bound";
1921 Kind k
= intToExtKind(d_node
->getKind());
1927 t
= d_solver
->mkValHelper
<Rational
>(
1928 Rational(d_node
->getConst
<Divisible
>().k
));
1931 case BITVECTOR_REPEAT
:
1933 t
= d_solver
->mkValHelper
<cvc5::Rational
>(
1934 d_node
->getConst
<BitVectorRepeat
>().d_repeatAmount
);
1937 case BITVECTOR_ZERO_EXTEND
:
1939 t
= d_solver
->mkValHelper
<cvc5::Rational
>(
1940 d_node
->getConst
<BitVectorZeroExtend
>().d_zeroExtendAmount
);
1943 case BITVECTOR_SIGN_EXTEND
:
1945 t
= d_solver
->mkValHelper
<cvc5::Rational
>(
1946 d_node
->getConst
<BitVectorSignExtend
>().d_signExtendAmount
);
1949 case BITVECTOR_ROTATE_LEFT
:
1951 t
= d_solver
->mkValHelper
<cvc5::Rational
>(
1952 d_node
->getConst
<BitVectorRotateLeft
>().d_rotateLeftAmount
);
1955 case BITVECTOR_ROTATE_RIGHT
:
1957 t
= d_solver
->mkValHelper
<cvc5::Rational
>(
1958 d_node
->getConst
<BitVectorRotateRight
>().d_rotateRightAmount
);
1961 case INT_TO_BITVECTOR
:
1963 t
= d_solver
->mkValHelper
<cvc5::Rational
>(
1964 d_node
->getConst
<IntToBitVector
>().d_size
);
1969 t
= d_solver
->mkValHelper
<cvc5::Rational
>(
1970 d_node
->getConst
<IntAnd
>().d_size
);
1973 case FLOATINGPOINT_TO_UBV
:
1975 t
= d_solver
->mkValHelper
<cvc5::Rational
>(
1976 d_node
->getConst
<FloatingPointToUBV
>().d_bv_size
.d_size
);
1979 case FLOATINGPOINT_TO_SBV
:
1981 t
= d_solver
->mkValHelper
<cvc5::Rational
>(
1982 d_node
->getConst
<FloatingPointToSBV
>().d_bv_size
.d_size
);
1987 t
= d_solver
->mkValHelper
<cvc5::Rational
>(
1988 d_node
->getConst
<RegExpRepeat
>().d_repeatAmount
);
1991 case BITVECTOR_EXTRACT
:
1993 cvc5::BitVectorExtract ext
= d_node
->getConst
<BitVectorExtract
>();
1994 t
= index
== 0 ? d_solver
->mkValHelper
<cvc5::Rational
>(ext
.d_high
)
1995 : d_solver
->mkValHelper
<cvc5::Rational
>(ext
.d_low
);
1998 case FLOATINGPOINT_TO_FP_IEEE_BITVECTOR
:
2000 cvc5::FloatingPointToFPIEEEBitVector ext
=
2001 d_node
->getConst
<FloatingPointToFPIEEEBitVector
>();
2003 t
= index
== 0 ? d_solver
->mkValHelper
<cvc5::Rational
>(
2004 ext
.getSize().exponentWidth())
2005 : d_solver
->mkValHelper
<cvc5::Rational
>(
2006 ext
.getSize().significandWidth());
2009 case FLOATINGPOINT_TO_FP_FLOATINGPOINT
:
2011 cvc5::FloatingPointToFPFloatingPoint ext
=
2012 d_node
->getConst
<FloatingPointToFPFloatingPoint
>();
2013 t
= index
== 0 ? d_solver
->mkValHelper
<cvc5::Rational
>(
2014 ext
.getSize().exponentWidth())
2015 : d_solver
->mkValHelper
<cvc5::Rational
>(
2016 ext
.getSize().significandWidth());
2019 case FLOATINGPOINT_TO_FP_REAL
:
2021 cvc5::FloatingPointToFPReal ext
=
2022 d_node
->getConst
<FloatingPointToFPReal
>();
2024 t
= index
== 0 ? d_solver
->mkValHelper
<cvc5::Rational
>(
2025 ext
.getSize().exponentWidth())
2026 : d_solver
->mkValHelper
<cvc5::Rational
>(
2027 ext
.getSize().significandWidth());
2030 case FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR
:
2032 cvc5::FloatingPointToFPSignedBitVector ext
=
2033 d_node
->getConst
<FloatingPointToFPSignedBitVector
>();
2034 t
= index
== 0 ? d_solver
->mkValHelper
<cvc5::Rational
>(
2035 ext
.getSize().exponentWidth())
2036 : d_solver
->mkValHelper
<cvc5::Rational
>(
2037 ext
.getSize().significandWidth());
2040 case FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR
:
2042 cvc5::FloatingPointToFPUnsignedBitVector ext
=
2043 d_node
->getConst
<FloatingPointToFPUnsignedBitVector
>();
2044 t
= index
== 0 ? d_solver
->mkValHelper
<cvc5::Rational
>(
2045 ext
.getSize().exponentWidth())
2046 : d_solver
->mkValHelper
<cvc5::Rational
>(
2047 ext
.getSize().significandWidth());
2050 case FLOATINGPOINT_TO_FP_GENERIC
:
2052 cvc5::FloatingPointToFPGeneric ext
=
2053 d_node
->getConst
<FloatingPointToFPGeneric
>();
2054 t
= index
== 0 ? d_solver
->mkValHelper
<cvc5::Rational
>(
2055 ext
.getSize().exponentWidth())
2056 : d_solver
->mkValHelper
<cvc5::Rational
>(
2057 ext
.getSize().significandWidth());
2062 cvc5::RegExpLoop ext
= d_node
->getConst
<RegExpLoop
>();
2063 t
= index
== 0 ? d_solver
->mkValHelper
<cvc5::Rational
>(ext
.d_loopMinOcc
)
2064 : d_solver
->mkValHelper
<cvc5::Rational
>(ext
.d_loopMaxOcc
);
2071 const std::vector
<uint32_t>& projectionIndices
=
2072 d_node
->getConst
<TupleProjectOp
>().getIndices();
2073 t
= d_solver
->mkValHelper
<cvc5::Rational
>(projectionIndices
[index
]);
2078 CVC5_API_CHECK(false) << "Unhandled kind " << kindToString(k
);
2083 //////// all checks before this line
2086 CVC5_API_TRY_CATCH_END
;
2090 std::string
Op::getIndices() const
2092 CVC5_API_TRY_CATCH_BEGIN
;
2093 CVC5_API_CHECK_NOT_NULL
;
2094 CVC5_API_CHECK(!d_node
->isNull())
2095 << "Expecting a non-null internal expression. This Op is not indexed.";
2096 Kind k
= intToExtKind(d_node
->getKind());
2097 CVC5_API_CHECK(k
== DIVISIBLE
) << "Can't get string index from"
2098 << " kind " << kindToString(k
);
2099 //////// all checks before this line
2100 return d_node
->getConst
<Divisible
>().k
.toString();
2102 CVC5_API_TRY_CATCH_END
;
2106 uint32_t Op::getIndices() const
2108 CVC5_API_TRY_CATCH_BEGIN
;
2109 CVC5_API_CHECK_NOT_NULL
;
2110 CVC5_API_CHECK(!d_node
->isNull())
2111 << "Expecting a non-null internal expression. This Op is not indexed.";
2112 //////// all checks before this line
2115 Kind k
= intToExtKind(d_node
->getKind());
2118 case BITVECTOR_REPEAT
:
2119 i
= d_node
->getConst
<BitVectorRepeat
>().d_repeatAmount
;
2121 case BITVECTOR_ZERO_EXTEND
:
2122 i
= d_node
->getConst
<BitVectorZeroExtend
>().d_zeroExtendAmount
;
2124 case BITVECTOR_SIGN_EXTEND
:
2125 i
= d_node
->getConst
<BitVectorSignExtend
>().d_signExtendAmount
;
2127 case BITVECTOR_ROTATE_LEFT
:
2128 i
= d_node
->getConst
<BitVectorRotateLeft
>().d_rotateLeftAmount
;
2130 case BITVECTOR_ROTATE_RIGHT
:
2131 i
= d_node
->getConst
<BitVectorRotateRight
>().d_rotateRightAmount
;
2133 case INT_TO_BITVECTOR
: i
= d_node
->getConst
<IntToBitVector
>().d_size
; break;
2134 case IAND
: i
= d_node
->getConst
<IntAnd
>().d_size
; break;
2135 case FLOATINGPOINT_TO_UBV
:
2136 i
= d_node
->getConst
<FloatingPointToUBV
>().d_bv_size
.d_size
;
2138 case FLOATINGPOINT_TO_SBV
:
2139 i
= d_node
->getConst
<FloatingPointToSBV
>().d_bv_size
.d_size
;
2142 i
= d_node
->getConst
<RegExpRepeat
>().d_repeatAmount
;
2145 CVC5_API_CHECK(false) << "Can't get uint32_t index from"
2146 << " kind " << kindToString(k
);
2150 CVC5_API_TRY_CATCH_END
;
2154 std::pair
<uint32_t, uint32_t> Op::getIndices() const
2156 CVC5_API_TRY_CATCH_BEGIN
;
2157 CVC5_API_CHECK_NOT_NULL
;
2158 CVC5_API_CHECK(!d_node
->isNull())
2159 << "Expecting a non-null internal expression. This Op is not indexed.";
2160 //////// all checks before this line
2162 std::pair
<uint32_t, uint32_t> indices
;
2163 Kind k
= intToExtKind(d_node
->getKind());
2165 // using if/else instead of case statement because want local variables
2166 if (k
== BITVECTOR_EXTRACT
)
2168 cvc5::BitVectorExtract ext
= d_node
->getConst
<BitVectorExtract
>();
2169 indices
= std::make_pair(ext
.d_high
, ext
.d_low
);
2171 else if (k
== FLOATINGPOINT_TO_FP_IEEE_BITVECTOR
)
2173 cvc5::FloatingPointToFPIEEEBitVector ext
=
2174 d_node
->getConst
<FloatingPointToFPIEEEBitVector
>();
2175 indices
= std::make_pair(ext
.getSize().exponentWidth(),
2176 ext
.getSize().significandWidth());
2178 else if (k
== FLOATINGPOINT_TO_FP_FLOATINGPOINT
)
2180 cvc5::FloatingPointToFPFloatingPoint ext
=
2181 d_node
->getConst
<FloatingPointToFPFloatingPoint
>();
2182 indices
= std::make_pair(ext
.getSize().exponentWidth(),
2183 ext
.getSize().significandWidth());
2185 else if (k
== FLOATINGPOINT_TO_FP_REAL
)
2187 cvc5::FloatingPointToFPReal ext
= d_node
->getConst
<FloatingPointToFPReal
>();
2188 indices
= std::make_pair(ext
.getSize().exponentWidth(),
2189 ext
.getSize().significandWidth());
2191 else if (k
== FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR
)
2193 cvc5::FloatingPointToFPSignedBitVector ext
=
2194 d_node
->getConst
<FloatingPointToFPSignedBitVector
>();
2195 indices
= std::make_pair(ext
.getSize().exponentWidth(),
2196 ext
.getSize().significandWidth());
2198 else if (k
== FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR
)
2200 cvc5::FloatingPointToFPUnsignedBitVector ext
=
2201 d_node
->getConst
<FloatingPointToFPUnsignedBitVector
>();
2202 indices
= std::make_pair(ext
.getSize().exponentWidth(),
2203 ext
.getSize().significandWidth());
2205 else if (k
== FLOATINGPOINT_TO_FP_GENERIC
)
2207 cvc5::FloatingPointToFPGeneric ext
=
2208 d_node
->getConst
<FloatingPointToFPGeneric
>();
2209 indices
= std::make_pair(ext
.getSize().exponentWidth(),
2210 ext
.getSize().significandWidth());
2212 else if (k
== REGEXP_LOOP
)
2214 cvc5::RegExpLoop ext
= d_node
->getConst
<RegExpLoop
>();
2215 indices
= std::make_pair(ext
.d_loopMinOcc
, ext
.d_loopMaxOcc
);
2219 CVC5_API_CHECK(false) << "Can't get pair<uint32_t, uint32_t> indices from"
2220 << " kind " << kindToString(k
);
2224 CVC5_API_TRY_CATCH_END
;
2228 std::vector
<api::Term
> Op::getIndices() const
2230 CVC5_API_TRY_CATCH_BEGIN
;
2231 CVC5_API_CHECK_NOT_NULL
;
2232 CVC5_API_CHECK(!d_node
->isNull())
2233 << "Expecting a non-null internal expression. This Op is not indexed.";
2234 size_t size
= getNumIndicesHelper();
2235 std::vector
<Term
> terms(getNumIndices());
2236 for (size_t i
= 0; i
< size
; i
++)
2238 terms
[i
] = getIndexHelper(i
);
2240 //////// all checks before this line
2243 CVC5_API_TRY_CATCH_END
;
2246 std::string
Op::toString() const
2248 CVC5_API_TRY_CATCH_BEGIN
;
2249 //////// all checks before this line
2250 if (d_node
->isNull())
2252 return kindToString(d_kind
);
2256 CVC5_API_CHECK(!d_node
->isNull())
2257 << "Expecting a non-null internal expression";
2258 if (d_solver
!= nullptr)
2260 return d_node
->toString();
2262 return d_node
->toString();
2265 CVC5_API_TRY_CATCH_END
;
2268 std::ostream
& operator<<(std::ostream
& out
, const Op
& t
)
2270 out
<< t
.toString();
2275 /* -------------------------------------------------------------------------- */
2277 /* Split out to avoid nested API calls (problematic with API tracing). */
2278 /* .......................................................................... */
2280 bool Op::isNullHelper() const
2282 return (d_node
->isNull() && (d_kind
== NULL_EXPR
));
2285 bool Op::isIndexedHelper() const { return !d_node
->isNull(); }
2287 /* -------------------------------------------------------------------------- */
2289 /* -------------------------------------------------------------------------- */
2291 Term::Term() : d_solver(nullptr), d_node(new cvc5::Node()) {}
2293 Term::Term(const Solver
* slv
, const cvc5::Node
& n
) : d_solver(slv
)
2295 d_node
.reset(new cvc5::Node(n
));
2300 if (d_solver
!= nullptr)
2306 bool Term::operator==(const Term
& t
) const
2308 CVC5_API_TRY_CATCH_BEGIN
;
2309 //////// all checks before this line
2310 return *d_node
== *t
.d_node
;
2312 CVC5_API_TRY_CATCH_END
;
2315 bool Term::operator!=(const Term
& t
) const
2317 CVC5_API_TRY_CATCH_BEGIN
;
2318 //////// all checks before this line
2319 return *d_node
!= *t
.d_node
;
2321 CVC5_API_TRY_CATCH_END
;
2324 bool Term::operator<(const Term
& t
) const
2326 CVC5_API_TRY_CATCH_BEGIN
;
2327 //////// all checks before this line
2328 return *d_node
< *t
.d_node
;
2330 CVC5_API_TRY_CATCH_END
;
2333 bool Term::operator>(const Term
& t
) const
2335 CVC5_API_TRY_CATCH_BEGIN
;
2336 //////// all checks before this line
2337 return *d_node
> *t
.d_node
;
2339 CVC5_API_TRY_CATCH_END
;
2342 bool Term::operator<=(const Term
& t
) const
2344 CVC5_API_TRY_CATCH_BEGIN
;
2345 //////// all checks before this line
2346 return *d_node
<= *t
.d_node
;
2348 CVC5_API_TRY_CATCH_END
;
2351 bool Term::operator>=(const Term
& t
) const
2353 CVC5_API_TRY_CATCH_BEGIN
;
2354 //////// all checks before this line
2355 return *d_node
>= *t
.d_node
;
2357 CVC5_API_TRY_CATCH_END
;
2360 size_t Term::getNumChildren() const
2362 CVC5_API_TRY_CATCH_BEGIN
;
2363 CVC5_API_CHECK_NOT_NULL
;
2364 //////// all checks before this line
2366 // special case for apply kinds
2367 if (isApplyKind(d_node
->getKind()))
2369 return d_node
->getNumChildren() + 1;
2375 return d_node
->getNumChildren();
2377 CVC5_API_TRY_CATCH_END
;
2380 Term
Term::operator[](size_t index
) const
2382 CVC5_API_TRY_CATCH_BEGIN
;
2383 CVC5_API_CHECK_NOT_NULL
;
2384 CVC5_API_CHECK(index
< getNumChildren()) << "index out of bound";
2385 CVC5_API_CHECK(!isApplyKind(d_node
->getKind()) || d_node
->hasOperator())
2386 << "Expected apply kind to have operator when accessing child of Term";
2387 //////// all checks before this line
2389 // special cases for apply kinds
2390 if (isApplyKind(d_node
->getKind()))
2394 // return the operator
2395 return Term(d_solver
, d_node
->getOperator());
2402 // otherwise we are looking up child at (index-1)
2403 return Term(d_solver
, (*d_node
)[index
]);
2405 CVC5_API_TRY_CATCH_END
;
2408 uint64_t Term::getId() const
2410 CVC5_API_TRY_CATCH_BEGIN
;
2411 CVC5_API_CHECK_NOT_NULL
;
2412 //////// all checks before this line
2413 return d_node
->getId();
2415 CVC5_API_TRY_CATCH_END
;
2418 Kind
Term::getKind() const
2420 CVC5_API_TRY_CATCH_BEGIN
;
2421 CVC5_API_CHECK_NOT_NULL
;
2422 //////// all checks before this line
2423 return getKindHelper();
2425 CVC5_API_TRY_CATCH_END
;
2428 Sort
Term::getSort() const
2430 CVC5_API_TRY_CATCH_BEGIN
;
2431 CVC5_API_CHECK_NOT_NULL
;
2432 //////// all checks before this line
2433 return Sort(d_solver
, d_node
->getType());
2435 CVC5_API_TRY_CATCH_END
;
2438 Term
Term::substitute(const Term
& term
, const Term
& replacement
) const
2440 CVC5_API_TRY_CATCH_BEGIN
;
2441 CVC5_API_CHECK_NOT_NULL
;
2442 CVC5_API_CHECK_TERM(term
);
2443 CVC5_API_CHECK_TERM(replacement
);
2444 CVC5_API_CHECK(term
.getSort().isComparableTo(replacement
.getSort()))
2445 << "Expecting terms of comparable sort in substitute";
2446 //////// all checks before this line
2449 d_node
->substitute(TNode(*term
.d_node
), TNode(*replacement
.d_node
)));
2451 CVC5_API_TRY_CATCH_END
;
2454 Term
Term::substitute(const std::vector
<Term
>& terms
,
2455 const std::vector
<Term
>& replacements
) const
2457 CVC5_API_TRY_CATCH_BEGIN
;
2458 CVC5_API_CHECK_NOT_NULL
;
2459 CVC5_API_CHECK(terms
.size() == replacements
.size())
2460 << "Expecting vectors of the same arity in substitute";
2461 CVC5_API_TERM_CHECK_TERMS_WITH_TERMS_COMPARABLE_TO(terms
, replacements
);
2462 //////// all checks before this line
2463 std::vector
<Node
> nodes
= Term::termVectorToNodes(terms
);
2464 std::vector
<Node
> nodeReplacements
= Term::termVectorToNodes(replacements
);
2465 return Term(d_solver
,
2466 d_node
->substitute(nodes
.begin(),
2468 nodeReplacements
.begin(),
2469 nodeReplacements
.end()));
2471 CVC5_API_TRY_CATCH_END
;
2474 bool Term::hasOp() const
2476 CVC5_API_TRY_CATCH_BEGIN
;
2477 CVC5_API_CHECK_NOT_NULL
;
2478 //////// all checks before this line
2479 return d_node
->hasOperator();
2481 CVC5_API_TRY_CATCH_END
;
2484 Op
Term::getOp() const
2486 CVC5_API_TRY_CATCH_BEGIN
;
2487 CVC5_API_CHECK_NOT_NULL
;
2488 CVC5_API_CHECK(d_node
->hasOperator())
2489 << "Expecting Term to have an Op when calling getOp()";
2490 //////// all checks before this line
2492 // special cases for parameterized operators that are not indexed operators
2493 // the API level differs from the internal structure
2494 // indexed operators are stored in Ops
2495 // whereas functions and datatype operators are terms, and the Op
2496 // is one of the APPLY_* kinds
2497 if (isApplyKind(d_node
->getKind()))
2499 return Op(d_solver
, intToExtKind(d_node
->getKind()));
2501 else if (d_node
->getMetaKind() == kind::metakind::PARAMETERIZED
)
2503 // it's an indexed operator
2504 // so we should return the indexed op
2505 cvc5::Node op
= d_node
->getOperator();
2506 return Op(d_solver
, intToExtKind(d_node
->getKind()), op
);
2508 // Notice this is the only case where getKindHelper is used, since the
2509 // cases above do not have special cases for intToExtKind.
2510 return Op(d_solver
, getKindHelper());
2512 CVC5_API_TRY_CATCH_END
;
2515 bool Term::isNull() const
2517 CVC5_API_TRY_CATCH_BEGIN
;
2518 //////// all checks before this line
2519 return isNullHelper();
2521 CVC5_API_TRY_CATCH_END
;
2524 Term
Term::notTerm() const
2526 CVC5_API_TRY_CATCH_BEGIN
;
2527 CVC5_API_CHECK_NOT_NULL
;
2528 //////// all checks before this line
2529 Node res
= d_node
->notNode();
2530 (void)res
.getType(true); /* kick off type checking */
2531 return Term(d_solver
, res
);
2533 CVC5_API_TRY_CATCH_END
;
2536 Term
Term::andTerm(const Term
& t
) const
2538 CVC5_API_TRY_CATCH_BEGIN
;
2539 CVC5_API_CHECK_NOT_NULL
;
2540 CVC5_API_CHECK_TERM(t
);
2541 //////// all checks before this line
2542 Node res
= d_node
->andNode(*t
.d_node
);
2543 (void)res
.getType(true); /* kick off type checking */
2544 return Term(d_solver
, res
);
2546 CVC5_API_TRY_CATCH_END
;
2549 Term
Term::orTerm(const Term
& t
) const
2551 CVC5_API_TRY_CATCH_BEGIN
;
2552 CVC5_API_CHECK_NOT_NULL
;
2553 CVC5_API_CHECK_TERM(t
);
2554 //////// all checks before this line
2555 Node res
= d_node
->orNode(*t
.d_node
);
2556 (void)res
.getType(true); /* kick off type checking */
2557 return Term(d_solver
, res
);
2559 CVC5_API_TRY_CATCH_END
;
2562 Term
Term::xorTerm(const Term
& t
) const
2564 CVC5_API_TRY_CATCH_BEGIN
;
2565 CVC5_API_CHECK_NOT_NULL
;
2566 CVC5_API_CHECK_TERM(t
);
2567 //////// all checks before this line
2568 Node res
= d_node
->xorNode(*t
.d_node
);
2569 (void)res
.getType(true); /* kick off type checking */
2570 return Term(d_solver
, res
);
2572 CVC5_API_TRY_CATCH_END
;
2575 Term
Term::eqTerm(const Term
& t
) const
2577 CVC5_API_TRY_CATCH_BEGIN
;
2578 CVC5_API_CHECK_NOT_NULL
;
2579 CVC5_API_CHECK_TERM(t
);
2580 //////// all checks before this line
2581 Node res
= d_node
->eqNode(*t
.d_node
);
2582 (void)res
.getType(true); /* kick off type checking */
2583 return Term(d_solver
, res
);
2585 CVC5_API_TRY_CATCH_END
;
2588 Term
Term::impTerm(const Term
& t
) const
2590 CVC5_API_TRY_CATCH_BEGIN
;
2591 CVC5_API_CHECK_NOT_NULL
;
2592 CVC5_API_CHECK_TERM(t
);
2593 //////// all checks before this line
2594 Node res
= d_node
->impNode(*t
.d_node
);
2595 (void)res
.getType(true); /* kick off type checking */
2596 return Term(d_solver
, res
);
2598 CVC5_API_TRY_CATCH_END
;
2601 Term
Term::iteTerm(const Term
& then_t
, const Term
& else_t
) const
2603 CVC5_API_TRY_CATCH_BEGIN
;
2604 CVC5_API_CHECK_NOT_NULL
;
2605 CVC5_API_CHECK_TERM(then_t
);
2606 CVC5_API_CHECK_TERM(else_t
);
2607 //////// all checks before this line
2608 Node res
= d_node
->iteNode(*then_t
.d_node
, *else_t
.d_node
);
2609 (void)res
.getType(true); /* kick off type checking */
2610 return Term(d_solver
, res
);
2612 CVC5_API_TRY_CATCH_END
;
2615 std::string
Term::toString() const
2617 CVC5_API_TRY_CATCH_BEGIN
;
2618 //////// all checks before this line
2619 if (d_solver
!= nullptr)
2621 return d_node
->toString();
2623 return d_node
->toString();
2625 CVC5_API_TRY_CATCH_END
;
2628 Term::const_iterator::const_iterator()
2629 : d_solver(nullptr), d_origNode(nullptr), d_pos(0)
2633 Term::const_iterator::const_iterator(const Solver
* slv
,
2634 const std::shared_ptr
<cvc5::Node
>& n
,
2636 : d_solver(slv
), d_origNode(n
), d_pos(p
)
2640 Term::const_iterator::const_iterator(const const_iterator
& it
)
2641 : d_solver(nullptr), d_origNode(nullptr)
2643 if (it
.d_origNode
!= nullptr)
2645 d_solver
= it
.d_solver
;
2646 d_origNode
= it
.d_origNode
;
2651 Term::const_iterator
& Term::const_iterator::operator=(const const_iterator
& it
)
2653 d_solver
= it
.d_solver
;
2654 d_origNode
= it
.d_origNode
;
2659 bool Term::const_iterator::operator==(const const_iterator
& it
) const
2661 if (d_origNode
== nullptr || it
.d_origNode
== nullptr)
2665 return (d_solver
== it
.d_solver
&& *d_origNode
== *it
.d_origNode
)
2666 && (d_pos
== it
.d_pos
);
2669 bool Term::const_iterator::operator!=(const const_iterator
& it
) const
2671 return !(*this == it
);
2674 Term::const_iterator
& Term::const_iterator::operator++()
2676 Assert(d_origNode
!= nullptr);
2681 Term::const_iterator
Term::const_iterator::operator++(int)
2683 Assert(d_origNode
!= nullptr);
2684 const_iterator it
= *this;
2689 Term
Term::const_iterator::operator*() const
2691 Assert(d_origNode
!= nullptr);
2692 // this term has an extra child (mismatch between API and internal structure)
2693 // the extra child will be the first child
2694 bool extra_child
= isApplyKind(d_origNode
->getKind());
2696 if (!d_pos
&& extra_child
)
2698 return Term(d_solver
, d_origNode
->getOperator());
2702 uint32_t idx
= d_pos
;
2709 return Term(d_solver
, (*d_origNode
)[idx
]);
2713 Term::const_iterator
Term::begin() const
2715 return Term::const_iterator(d_solver
, d_node
, 0);
2718 Term::const_iterator
Term::end() const
2720 int endpos
= d_node
->getNumChildren();
2721 // special cases for APPLY_*
2722 // the API differs from the internal structure
2723 // the API takes a "higher-order" perspective and the applied
2724 // function or datatype constructor/selector/tester is a Term
2725 // which means it needs to be one of the children, even though
2726 // internally it is not
2727 if (isApplyKind(d_node
->getKind()))
2729 // one more child if this is a UF application (count the UF as a child)
2732 return Term::const_iterator(d_solver
, d_node
, endpos
);
2735 const cvc5::Node
& Term::getNode(void) const { return *d_node
; }
2738 const Rational
& getRational(const cvc5::Node
& node
)
2740 switch (node
.getKind())
2742 case cvc5::Kind::CAST_TO_REAL
: return node
[0].getConst
<Rational
>();
2743 case cvc5::Kind::CONST_RATIONAL
: return node
.getConst
<Rational
>();
2745 CVC5_API_CHECK(false) << "Node is not a rational.";
2746 return node
.getConst
<Rational
>();
2749 Integer
getInteger(const cvc5::Node
& node
)
2751 return node
.getConst
<Rational
>().getNumerator();
2753 template <typename T
>
2754 bool checkIntegerBounds(const Integer
& i
)
2756 return i
>= std::numeric_limits
<T
>::min()
2757 && i
<= std::numeric_limits
<T
>::max();
2759 bool checkReal32Bounds(const Rational
& r
)
2761 return checkIntegerBounds
<std::int32_t>(r
.getNumerator())
2762 && checkIntegerBounds
<std::uint32_t>(r
.getDenominator());
2764 bool checkReal64Bounds(const Rational
& r
)
2766 return checkIntegerBounds
<std::int64_t>(r
.getNumerator())
2767 && checkIntegerBounds
<std::uint64_t>(r
.getDenominator());
2770 bool isReal(const Node
& node
)
2772 return node
.getKind() == cvc5::Kind::CONST_RATIONAL
2773 || node
.getKind() == cvc5::Kind::CAST_TO_REAL
;
2775 bool isReal32(const Node
& node
)
2777 return isReal(node
) && checkReal32Bounds(getRational(node
));
2779 bool isReal64(const Node
& node
)
2781 return isReal(node
) && checkReal64Bounds(getRational(node
));
2784 bool isInteger(const Node
& node
)
2786 return node
.getKind() == cvc5::Kind::CONST_RATIONAL
2787 && node
.getConst
<Rational
>().isIntegral();
2789 bool isInt32(const Node
& node
)
2791 return isInteger(node
) && checkIntegerBounds
<std::int32_t>(getInteger(node
));
2793 bool isUInt32(const Node
& node
)
2795 return isInteger(node
) && checkIntegerBounds
<std::uint32_t>(getInteger(node
));
2797 bool isInt64(const Node
& node
)
2799 return isInteger(node
) && checkIntegerBounds
<std::int64_t>(getInteger(node
));
2801 bool isUInt64(const Node
& node
)
2803 return isInteger(node
) && checkIntegerBounds
<std::uint64_t>(getInteger(node
));
2805 } // namespace detail
2807 bool Term::isInt32Value() const
2809 CVC5_API_TRY_CATCH_BEGIN
;
2810 CVC5_API_CHECK_NOT_NULL
;
2811 //////// all checks before this line
2812 return detail::isInt32(*d_node
);
2814 CVC5_API_TRY_CATCH_END
;
2817 std::int32_t Term::getInt32Value() const
2819 CVC5_API_TRY_CATCH_BEGIN
;
2820 CVC5_API_CHECK_NOT_NULL
;
2821 CVC5_API_ARG_CHECK_EXPECTED(detail::isInt32(*d_node
), *d_node
)
2822 << "Term to be a 32-bit integer value when calling getInt32Value()";
2823 //////// all checks before this line
2824 return detail::getInteger(*d_node
).getSignedInt();
2826 CVC5_API_TRY_CATCH_END
;
2829 bool Term::isUInt32Value() const
2831 CVC5_API_TRY_CATCH_BEGIN
;
2832 CVC5_API_CHECK_NOT_NULL
;
2833 //////// all checks before this line
2834 return detail::isUInt32(*d_node
);
2836 CVC5_API_TRY_CATCH_END
;
2838 std::uint32_t Term::getUInt32Value() const
2840 CVC5_API_TRY_CATCH_BEGIN
;
2841 CVC5_API_CHECK_NOT_NULL
;
2842 CVC5_API_ARG_CHECK_EXPECTED(detail::isUInt32(*d_node
), *d_node
)
2843 << "Term to be a unsigned 32-bit integer value when calling "
2845 //////// all checks before this line
2846 return detail::getInteger(*d_node
).getUnsignedInt();
2848 CVC5_API_TRY_CATCH_END
;
2851 bool Term::isInt64Value() const
2853 CVC5_API_TRY_CATCH_BEGIN
;
2854 CVC5_API_CHECK_NOT_NULL
;
2855 //////// all checks before this line
2856 return detail::isInt64(*d_node
);
2858 CVC5_API_TRY_CATCH_END
;
2860 std::int64_t Term::getInt64Value() const
2862 CVC5_API_TRY_CATCH_BEGIN
;
2863 CVC5_API_CHECK_NOT_NULL
;
2864 CVC5_API_ARG_CHECK_EXPECTED(detail::isInt64(*d_node
), *d_node
)
2865 << "Term to be a 64-bit integer value when calling getInt64Value()";
2866 //////// all checks before this line
2867 return detail::getInteger(*d_node
).getLong();
2869 CVC5_API_TRY_CATCH_END
;
2872 bool Term::isUInt64Value() const
2874 CVC5_API_TRY_CATCH_BEGIN
;
2875 CVC5_API_CHECK_NOT_NULL
;
2876 //////// all checks before this line
2877 return detail::isUInt64(*d_node
);
2879 CVC5_API_TRY_CATCH_END
;
2882 std::uint64_t Term::getUInt64Value() const
2884 CVC5_API_TRY_CATCH_BEGIN
;
2885 CVC5_API_CHECK_NOT_NULL
;
2886 CVC5_API_ARG_CHECK_EXPECTED(detail::isUInt64(*d_node
), *d_node
)
2887 << "Term to be a unsigned 64-bit integer value when calling "
2889 //////// all checks before this line
2890 return detail::getInteger(*d_node
).getUnsignedLong();
2892 CVC5_API_TRY_CATCH_END
;
2895 bool Term::isIntegerValue() const
2897 CVC5_API_TRY_CATCH_BEGIN
;
2898 CVC5_API_CHECK_NOT_NULL
;
2899 //////// all checks before this line
2900 return detail::isInteger(*d_node
);
2902 CVC5_API_TRY_CATCH_END
;
2904 std::string
Term::getIntegerValue() const
2906 CVC5_API_TRY_CATCH_BEGIN
;
2907 CVC5_API_CHECK_NOT_NULL
;
2908 CVC5_API_ARG_CHECK_EXPECTED(detail::isInteger(*d_node
), *d_node
)
2909 << "Term to be an integer value when calling getIntegerValue()";
2910 //////// all checks before this line
2911 return detail::getInteger(*d_node
).toString();
2913 CVC5_API_TRY_CATCH_END
;
2916 bool Term::isStringValue() const
2918 CVC5_API_TRY_CATCH_BEGIN
;
2919 CVC5_API_CHECK_NOT_NULL
;
2920 //////// all checks before this line
2921 return d_node
->getKind() == cvc5::Kind::CONST_STRING
;
2923 CVC5_API_TRY_CATCH_END
;
2926 std::wstring
Term::getStringValue() const
2928 CVC5_API_TRY_CATCH_BEGIN
;
2929 CVC5_API_CHECK_NOT_NULL
;
2930 CVC5_API_ARG_CHECK_EXPECTED(d_node
->getKind() == cvc5::Kind::CONST_STRING
,
2932 << "Term to be a string value when calling getStringValue()";
2933 //////// all checks before this line
2934 return d_node
->getConst
<cvc5::String
>().toWString();
2936 CVC5_API_TRY_CATCH_END
;
2939 std::vector
<Node
> Term::termVectorToNodes(const std::vector
<Term
>& terms
)
2941 std::vector
<Node
> res
;
2942 for (const Term
& t
: terms
)
2944 res
.push_back(t
.getNode());
2949 bool Term::isReal32Value() const
2951 CVC5_API_TRY_CATCH_BEGIN
;
2952 CVC5_API_CHECK_NOT_NULL
;
2953 //////// all checks before this line
2954 return detail::isReal32(*d_node
);
2956 CVC5_API_TRY_CATCH_END
;
2958 std::pair
<std::int32_t, std::uint32_t> Term::getReal32Value() const
2960 CVC5_API_TRY_CATCH_BEGIN
;
2961 CVC5_API_CHECK_NOT_NULL
;
2962 CVC5_API_ARG_CHECK_EXPECTED(detail::isReal32(*d_node
), *d_node
)
2963 << "Term to be a 32-bit rational value when calling getReal32Value()";
2964 //////// all checks before this line
2965 const Rational
& r
= detail::getRational(*d_node
);
2966 return std::make_pair(r
.getNumerator().getSignedInt(),
2967 r
.getDenominator().getUnsignedInt());
2969 CVC5_API_TRY_CATCH_END
;
2971 bool Term::isReal64Value() const
2973 CVC5_API_TRY_CATCH_BEGIN
;
2974 CVC5_API_CHECK_NOT_NULL
;
2975 //////// all checks before this line
2976 return detail::isReal64(*d_node
);
2978 CVC5_API_TRY_CATCH_END
;
2980 std::pair
<std::int64_t, std::uint64_t> Term::getReal64Value() const
2982 CVC5_API_TRY_CATCH_BEGIN
;
2983 CVC5_API_CHECK_NOT_NULL
;
2984 CVC5_API_ARG_CHECK_EXPECTED(detail::isReal64(*d_node
), *d_node
)
2985 << "Term to be a 64-bit rational value when calling getReal64Value()";
2986 //////// all checks before this line
2987 const Rational
& r
= detail::getRational(*d_node
);
2988 return std::make_pair(r
.getNumerator().getLong(),
2989 r
.getDenominator().getUnsignedLong());
2991 CVC5_API_TRY_CATCH_END
;
2993 bool Term::isRealValue() const
2995 CVC5_API_TRY_CATCH_BEGIN
;
2996 CVC5_API_CHECK_NOT_NULL
;
2997 //////// all checks before this line
2998 return detail::isReal(*d_node
);
3000 CVC5_API_TRY_CATCH_END
;
3002 std::string
Term::getRealValue() const
3004 CVC5_API_TRY_CATCH_BEGIN
;
3005 CVC5_API_CHECK_NOT_NULL
;
3006 CVC5_API_ARG_CHECK_EXPECTED(detail::isReal(*d_node
), *d_node
)
3007 << "Term to be a rational value when calling getRealValue()";
3008 //////// all checks before this line
3009 const Rational
& rat
= detail::getRational(*d_node
);
3010 std::string res
= rat
.toString();
3011 if (rat
.isIntegral())
3017 CVC5_API_TRY_CATCH_END
;
3020 bool Term::isConstArray() const
3022 CVC5_API_TRY_CATCH_BEGIN
;
3023 CVC5_API_CHECK_NOT_NULL
;
3024 //////// all checks before this line
3025 return d_node
->getKind() == cvc5::Kind::STORE_ALL
;
3027 CVC5_API_TRY_CATCH_END
;
3029 Term
Term::getConstArrayBase() const
3031 CVC5_API_TRY_CATCH_BEGIN
;
3032 CVC5_API_CHECK_NOT_NULL
;
3033 CVC5_API_ARG_CHECK_EXPECTED(d_node
->getKind() == cvc5::Kind::STORE_ALL
,
3035 << "Term to be a constant array when calling getConstArrayBase()";
3036 //////// all checks before this line
3037 const auto& ar
= d_node
->getConst
<ArrayStoreAll
>();
3038 return Term(d_solver
, ar
.getValue());
3040 CVC5_API_TRY_CATCH_END
;
3043 bool Term::isBooleanValue() const
3045 CVC5_API_TRY_CATCH_BEGIN
;
3046 CVC5_API_CHECK_NOT_NULL
;
3047 //////// all checks before this line
3048 return d_node
->getKind() == cvc5::Kind::CONST_BOOLEAN
;
3050 CVC5_API_TRY_CATCH_END
;
3052 bool Term::getBooleanValue() const
3054 CVC5_API_TRY_CATCH_BEGIN
;
3055 CVC5_API_CHECK_NOT_NULL
;
3056 CVC5_API_ARG_CHECK_EXPECTED(d_node
->getKind() == cvc5::Kind::CONST_BOOLEAN
,
3058 << "Term to be a Boolean value when calling getBooleanValue()";
3059 //////// all checks before this line
3060 return d_node
->getConst
<bool>();
3062 CVC5_API_TRY_CATCH_END
;
3065 bool Term::isBitVectorValue() const
3067 CVC5_API_TRY_CATCH_BEGIN
;
3068 CVC5_API_CHECK_NOT_NULL
;
3069 //////// all checks before this line
3070 return d_node
->getKind() == cvc5::Kind::CONST_BITVECTOR
;
3072 CVC5_API_TRY_CATCH_END
;
3074 std::string
Term::getBitVectorValue(std::uint32_t base
) const
3076 CVC5_API_TRY_CATCH_BEGIN
;
3077 CVC5_API_CHECK_NOT_NULL
;
3078 CVC5_API_ARG_CHECK_EXPECTED(d_node
->getKind() == cvc5::Kind::CONST_BITVECTOR
,
3080 << "Term to be a bit-vector value when calling getBitVectorValue()";
3081 //////// all checks before this line
3082 return d_node
->getConst
<BitVector
>().toString(base
);
3084 CVC5_API_TRY_CATCH_END
;
3087 bool Term::isAbstractValue() const
3089 CVC5_API_TRY_CATCH_BEGIN
;
3090 CVC5_API_CHECK_NOT_NULL
;
3091 //////// all checks before this line
3092 return d_node
->getKind() == cvc5::Kind::ABSTRACT_VALUE
;
3094 CVC5_API_TRY_CATCH_END
;
3096 std::string
Term::getAbstractValue() const
3098 CVC5_API_TRY_CATCH_BEGIN
;
3099 CVC5_API_CHECK_NOT_NULL
;
3100 CVC5_API_ARG_CHECK_EXPECTED(d_node
->getKind() == cvc5::Kind::ABSTRACT_VALUE
,
3102 << "Term to be an abstract value when calling "
3103 "getAbstractValue()";
3104 //////// all checks before this line
3105 return d_node
->getConst
<AbstractValue
>().getIndex().toString();
3107 CVC5_API_TRY_CATCH_END
;
3110 bool Term::isTupleValue() const
3112 CVC5_API_TRY_CATCH_BEGIN
;
3113 CVC5_API_CHECK_NOT_NULL
;
3114 //////// all checks before this line
3115 return d_node
->getKind() == cvc5::Kind::APPLY_CONSTRUCTOR
&& d_node
->isConst()
3116 && d_node
->getType().getDType().isTuple();
3118 CVC5_API_TRY_CATCH_END
;
3120 std::vector
<Term
> Term::getTupleValue() const
3122 CVC5_API_TRY_CATCH_BEGIN
;
3123 CVC5_API_CHECK_NOT_NULL
;
3124 CVC5_API_ARG_CHECK_EXPECTED(d_node
->getKind() == cvc5::Kind::APPLY_CONSTRUCTOR
3125 && d_node
->isConst()
3126 && d_node
->getType().getDType().isTuple(),
3128 << "Term to be a tuple value when calling getTupleValue()";
3129 //////// all checks before this line
3130 std::vector
<Term
> res
;
3131 for (size_t i
= 0, n
= d_node
->getNumChildren(); i
< n
; ++i
)
3133 res
.emplace_back(Term(d_solver
, (*d_node
)[i
]));
3137 CVC5_API_TRY_CATCH_END
;
3140 bool Term::isFloatingPointPosZero() const
3142 CVC5_API_TRY_CATCH_BEGIN
;
3143 CVC5_API_CHECK_NOT_NULL
;
3144 //////// all checks before this line
3145 if (d_node
->getKind() == cvc5::Kind::CONST_FLOATINGPOINT
)
3147 const auto& fp
= d_node
->getConst
<FloatingPoint
>();
3148 return fp
.isZero() && fp
.isPositive();
3152 CVC5_API_TRY_CATCH_END
;
3154 bool Term::isFloatingPointNegZero() const
3156 CVC5_API_TRY_CATCH_BEGIN
;
3157 CVC5_API_CHECK_NOT_NULL
;
3158 //////// all checks before this line
3159 if (d_node
->getKind() == cvc5::Kind::CONST_FLOATINGPOINT
)
3161 const auto& fp
= d_node
->getConst
<FloatingPoint
>();
3162 return fp
.isZero() && fp
.isNegative();
3166 CVC5_API_TRY_CATCH_END
;
3168 bool Term::isFloatingPointPosInf() const
3170 CVC5_API_TRY_CATCH_BEGIN
;
3171 CVC5_API_CHECK_NOT_NULL
;
3172 //////// all checks before this line
3173 if (d_node
->getKind() == cvc5::Kind::CONST_FLOATINGPOINT
)
3175 const auto& fp
= d_node
->getConst
<FloatingPoint
>();
3176 return fp
.isInfinite() && fp
.isPositive();
3180 CVC5_API_TRY_CATCH_END
;
3182 bool Term::isFloatingPointNegInf() const
3184 CVC5_API_TRY_CATCH_BEGIN
;
3185 CVC5_API_CHECK_NOT_NULL
;
3186 //////// all checks before this line
3187 if (d_node
->getKind() == cvc5::Kind::CONST_FLOATINGPOINT
)
3189 const auto& fp
= d_node
->getConst
<FloatingPoint
>();
3190 return fp
.isInfinite() && fp
.isNegative();
3194 CVC5_API_TRY_CATCH_END
;
3196 bool Term::isFloatingPointNaN() const
3198 CVC5_API_TRY_CATCH_BEGIN
;
3199 CVC5_API_CHECK_NOT_NULL
;
3200 //////// all checks before this line
3201 return d_node
->getKind() == cvc5::Kind::CONST_FLOATINGPOINT
3202 && d_node
->getConst
<FloatingPoint
>().isNaN();
3204 CVC5_API_TRY_CATCH_END
;
3206 bool Term::isFloatingPointValue() const
3208 CVC5_API_TRY_CATCH_BEGIN
;
3209 CVC5_API_CHECK_NOT_NULL
;
3210 //////// all checks before this line
3211 return d_node
->getKind() == cvc5::Kind::CONST_FLOATINGPOINT
;
3213 CVC5_API_TRY_CATCH_END
;
3215 std::tuple
<std::uint32_t, std::uint32_t, Term
> Term::getFloatingPointValue()
3218 CVC5_API_TRY_CATCH_BEGIN
;
3219 CVC5_API_CHECK_NOT_NULL
;
3220 CVC5_API_ARG_CHECK_EXPECTED(
3221 d_node
->getKind() == cvc5::Kind::CONST_FLOATINGPOINT
, *d_node
)
3222 << "Term to be a floating-point value when calling "
3223 "getFloatingPointValue()";
3224 //////// all checks before this line
3225 const auto& fp
= d_node
->getConst
<FloatingPoint
>();
3226 return std::make_tuple(fp
.getSize().exponentWidth(),
3227 fp
.getSize().significandWidth(),
3228 d_solver
->mkValHelper
<BitVector
>(fp
.pack()));
3230 CVC5_API_TRY_CATCH_END
;
3233 bool Term::isSetValue() const
3235 CVC5_API_TRY_CATCH_BEGIN
;
3236 CVC5_API_CHECK_NOT_NULL
;
3237 //////// all checks before this line
3238 return d_node
->getType().isSet() && d_node
->isConst();
3240 CVC5_API_TRY_CATCH_END
;
3243 void Term::collectSet(std::set
<Term
>& set
,
3244 const cvc5::Node
& node
,
3247 // We asserted that node has a set type, and node.isConst()
3248 // Thus, node only contains of EMPTYSET, UNION and SINGLETON.
3249 switch (node
.getKind())
3251 case cvc5::Kind::EMPTYSET
: break;
3252 case cvc5::Kind::SINGLETON
: set
.emplace(Term(slv
, node
[0])); break;
3253 case cvc5::Kind::UNION
:
3255 for (const auto& sub
: node
)
3257 collectSet(set
, sub
, slv
);
3262 CVC5_API_ARG_CHECK_EXPECTED(false, node
)
3263 << "Term to be a set value when calling getSetValue()";
3268 std::set
<Term
> Term::getSetValue() const
3270 CVC5_API_TRY_CATCH_BEGIN
;
3271 CVC5_API_CHECK_NOT_NULL
;
3272 CVC5_API_ARG_CHECK_EXPECTED(d_node
->getType().isSet() && d_node
->isConst(),
3274 << "Term to be a set value when calling getSetValue()";
3275 //////// all checks before this line
3277 Term::collectSet(res
, *d_node
, d_solver
);
3280 CVC5_API_TRY_CATCH_END
;
3283 bool Term::isSequenceValue() const
3285 CVC5_API_TRY_CATCH_BEGIN
;
3286 CVC5_API_CHECK_NOT_NULL
;
3287 //////// all checks before this line
3288 return d_node
->getKind() == cvc5::Kind::CONST_SEQUENCE
;
3290 CVC5_API_TRY_CATCH_END
;
3292 std::vector
<Term
> Term::getSequenceValue() const
3294 CVC5_API_TRY_CATCH_BEGIN
;
3295 CVC5_API_CHECK_NOT_NULL
;
3296 CVC5_API_ARG_CHECK_EXPECTED(d_node
->getKind() == cvc5::Kind::CONST_SEQUENCE
,
3298 << "Term to be a sequence value when calling getSequenceValue()";
3299 //////// all checks before this line
3300 std::vector
<Term
> res
;
3301 const Sequence
& seq
= d_node
->getConst
<Sequence
>();
3302 for (const auto& node
: seq
.getVec())
3304 res
.emplace_back(Term(d_solver
, node
));
3308 CVC5_API_TRY_CATCH_END
;
3311 bool Term::isUninterpretedValue() const
3313 CVC5_API_TRY_CATCH_BEGIN
;
3314 CVC5_API_CHECK_NOT_NULL
;
3315 //////// all checks before this line
3316 return d_node
->getKind() == cvc5::Kind::UNINTERPRETED_CONSTANT
;
3318 CVC5_API_TRY_CATCH_END
;
3320 std::pair
<Sort
, std::int32_t> Term::getUninterpretedValue() const
3322 CVC5_API_TRY_CATCH_BEGIN
;
3323 CVC5_API_CHECK_NOT_NULL
;
3324 CVC5_API_ARG_CHECK_EXPECTED(
3325 d_node
->getKind() == cvc5::Kind::UNINTERPRETED_CONSTANT
, *d_node
)
3326 << "Term to be an uninterpreted value when calling "
3327 "getUninterpretedValue()";
3328 //////// all checks before this line
3329 const auto& uc
= d_node
->getConst
<UninterpretedConstant
>();
3330 return std::make_pair(Sort(d_solver
, uc
.getType()),
3331 uc
.getIndex().toUnsignedInt());
3333 CVC5_API_TRY_CATCH_END
;
3336 std::ostream
& operator<<(std::ostream
& out
, const Term
& t
)
3338 out
<< t
.toString();
3342 std::ostream
& operator<<(std::ostream
& out
, const std::vector
<Term
>& vector
)
3344 container_to_stream(out
, vector
);
3348 std::ostream
& operator<<(std::ostream
& out
, const std::set
<Term
>& set
)
3350 container_to_stream(out
, set
);
3354 std::ostream
& operator<<(std::ostream
& out
,
3355 const std::unordered_set
<Term
>& unordered_set
)
3357 container_to_stream(out
, unordered_set
);
3361 template <typename V
>
3362 std::ostream
& operator<<(std::ostream
& out
, const std::map
<Term
, V
>& map
)
3364 container_to_stream(out
, map
);
3368 template <typename V
>
3369 std::ostream
& operator<<(std::ostream
& out
,
3370 const std::unordered_map
<Term
, V
>& unordered_map
)
3372 container_to_stream(out
, unordered_map
);
3377 /* -------------------------------------------------------------------------- */
3379 /* Split out to avoid nested API calls (problematic with API tracing). */
3380 /* .......................................................................... */
3382 bool Term::isNullHelper() const
3384 /* Split out to avoid nested API calls (problematic with API tracing). */
3385 return d_node
->isNull();
3388 Kind
Term::getKindHelper() const
3390 /* Sequence kinds do not exist internally, so we must convert their internal
3391 * (string) versions back to sequence. All operators where this is
3392 * necessary are such that their first child is of sequence type, which
3394 if (d_node
->getNumChildren() > 0 && (*d_node
)[0].getType().isSequence())
3396 switch (d_node
->getKind())
3398 case cvc5::Kind::STRING_CONCAT
: return SEQ_CONCAT
;
3399 case cvc5::Kind::STRING_LENGTH
: return SEQ_LENGTH
;
3400 case cvc5::Kind::STRING_SUBSTR
: return SEQ_EXTRACT
;
3401 case cvc5::Kind::STRING_UPDATE
: return SEQ_UPDATE
;
3402 case cvc5::Kind::STRING_CHARAT
: return SEQ_AT
;
3403 case cvc5::Kind::STRING_CONTAINS
: return SEQ_CONTAINS
;
3404 case cvc5::Kind::STRING_INDEXOF
: return SEQ_INDEXOF
;
3405 case cvc5::Kind::STRING_REPLACE
: return SEQ_REPLACE
;
3406 case cvc5::Kind::STRING_REPLACE_ALL
: return SEQ_REPLACE_ALL
;
3407 case cvc5::Kind::STRING_REV
: return SEQ_REV
;
3408 case cvc5::Kind::STRING_PREFIX
: return SEQ_PREFIX
;
3409 case cvc5::Kind::STRING_SUFFIX
: return SEQ_SUFFIX
;
3411 // fall through to conversion below
3415 // Notice that kinds like APPLY_TYPE_ASCRIPTION will be converted to
3419 return CONST_RATIONAL
;
3421 return intToExtKind(d_node
->getKind());
3424 bool Term::isCastedReal() const
3426 if (d_node
->getKind() == kind::CAST_TO_REAL
)
3428 return (*d_node
)[0].isConst() && (*d_node
)[0].getType().isInteger();
3433 /* -------------------------------------------------------------------------- */
3435 /* -------------------------------------------------------------------------- */
3437 /* DatatypeConstructorDecl -------------------------------------------------- */
3439 DatatypeConstructorDecl::DatatypeConstructorDecl()
3440 : d_solver(nullptr), d_ctor(nullptr)
3444 DatatypeConstructorDecl::DatatypeConstructorDecl(const Solver
* slv
,
3445 const std::string
& name
)
3446 : d_solver(slv
), d_ctor(new cvc5::DTypeConstructor(name
))
3449 DatatypeConstructorDecl::~DatatypeConstructorDecl()
3451 if (d_ctor
!= nullptr)
3457 void DatatypeConstructorDecl::addSelector(const std::string
& name
,
3460 CVC5_API_TRY_CATCH_BEGIN
;
3461 CVC5_API_CHECK_NOT_NULL
;
3462 CVC5_API_CHECK_SORT(sort
);
3463 CVC5_API_ARG_CHECK_EXPECTED(!sort
.isNull(), sort
)
3464 << "non-null range sort for selector";
3465 //////// all checks before this line
3466 d_ctor
->addArg(name
, *sort
.d_type
);
3468 CVC5_API_TRY_CATCH_END
;
3471 void DatatypeConstructorDecl::addSelectorSelf(const std::string
& name
)
3473 CVC5_API_TRY_CATCH_BEGIN
;
3474 CVC5_API_CHECK_NOT_NULL
;
3475 //////// all checks before this line
3476 d_ctor
->addArgSelf(name
);
3478 CVC5_API_TRY_CATCH_END
;
3481 bool DatatypeConstructorDecl::isNull() const
3483 CVC5_API_TRY_CATCH_BEGIN
;
3484 //////// all checks before this line
3485 return isNullHelper();
3487 CVC5_API_TRY_CATCH_END
;
3490 std::string
DatatypeConstructorDecl::toString() const
3492 CVC5_API_TRY_CATCH_BEGIN
;
3493 //////// all checks before this line
3494 std::stringstream ss
;
3498 CVC5_API_TRY_CATCH_END
;
3501 std::ostream
& operator<<(std::ostream
& out
,
3502 const DatatypeConstructorDecl
& ctordecl
)
3504 out
<< ctordecl
.toString();
3508 std::ostream
& operator<<(std::ostream
& out
,
3509 const std::vector
<DatatypeConstructorDecl
>& vector
)
3511 container_to_stream(out
, vector
);
3515 bool DatatypeConstructorDecl::isNullHelper() const { return d_ctor
== nullptr; }
3517 /* DatatypeDecl ------------------------------------------------------------- */
3519 DatatypeDecl::DatatypeDecl() : d_solver(nullptr), d_dtype(nullptr) {}
3521 DatatypeDecl::DatatypeDecl(const Solver
* slv
,
3522 const std::string
& name
,
3524 : d_solver(slv
), d_dtype(new cvc5::DType(name
, isCoDatatype
))
3528 DatatypeDecl::DatatypeDecl(const Solver
* slv
,
3529 const std::string
& name
,
3533 d_dtype(new cvc5::DType(
3534 name
, std::vector
<TypeNode
>{*param
.d_type
}, isCoDatatype
))
3538 DatatypeDecl::DatatypeDecl(const Solver
* slv
,
3539 const std::string
& name
,
3540 const std::vector
<Sort
>& params
,
3544 std::vector
<TypeNode
> tparams
= Sort::sortVectorToTypeNodes(params
);
3545 d_dtype
= std::shared_ptr
<cvc5::DType
>(
3546 new cvc5::DType(name
, tparams
, isCoDatatype
));
3549 bool DatatypeDecl::isNullHelper() const { return !d_dtype
; }
3551 DatatypeDecl::~DatatypeDecl()
3553 if (d_dtype
!= nullptr)
3559 void DatatypeDecl::addConstructor(const DatatypeConstructorDecl
& ctor
)
3561 CVC5_API_TRY_CATCH_BEGIN
;
3562 CVC5_API_CHECK_NOT_NULL
;
3563 CVC5_API_ARG_CHECK_NOT_NULL(ctor
);
3564 CVC5_API_ARG_CHECK_SOLVER("datatype constructor declaration", ctor
);
3565 //////// all checks before this line
3566 d_dtype
->addConstructor(ctor
.d_ctor
);
3568 CVC5_API_TRY_CATCH_END
;
3571 size_t DatatypeDecl::getNumConstructors() const
3573 CVC5_API_TRY_CATCH_BEGIN
;
3574 CVC5_API_CHECK_NOT_NULL
;
3575 //////// all checks before this line
3576 return d_dtype
->getNumConstructors();
3578 CVC5_API_TRY_CATCH_END
;
3581 bool DatatypeDecl::isParametric() const
3583 CVC5_API_TRY_CATCH_BEGIN
;
3584 CVC5_API_CHECK_NOT_NULL
;
3585 //////// all checks before this line
3586 return d_dtype
->isParametric();
3588 CVC5_API_TRY_CATCH_END
;
3591 std::string
DatatypeDecl::toString() const
3593 CVC5_API_TRY_CATCH_BEGIN
;
3594 CVC5_API_CHECK_NOT_NULL
;
3595 //////// all checks before this line
3596 std::stringstream ss
;
3600 CVC5_API_TRY_CATCH_END
;
3603 std::string
DatatypeDecl::getName() const
3605 CVC5_API_TRY_CATCH_BEGIN
;
3606 CVC5_API_CHECK_NOT_NULL
;
3607 //////// all checks before this line
3608 return d_dtype
->getName();
3610 CVC5_API_TRY_CATCH_END
;
3613 bool DatatypeDecl::isNull() const
3615 CVC5_API_TRY_CATCH_BEGIN
;
3616 //////// all checks before this line
3617 return isNullHelper();
3619 CVC5_API_TRY_CATCH_END
;
3622 std::ostream
& operator<<(std::ostream
& out
, const DatatypeDecl
& dtdecl
)
3624 out
<< dtdecl
.toString();
3628 cvc5::DType
& DatatypeDecl::getDatatype(void) const { return *d_dtype
; }
3630 /* DatatypeSelector --------------------------------------------------------- */
3632 DatatypeSelector::DatatypeSelector() : d_solver(nullptr), d_stor(nullptr) {}
3634 DatatypeSelector::DatatypeSelector(const Solver
* slv
,
3635 const cvc5::DTypeSelector
& stor
)
3636 : d_solver(slv
), d_stor(new cvc5::DTypeSelector(stor
))
3638 CVC5_API_CHECK(d_stor
->isResolved()) << "Expected resolved datatype selector";
3641 DatatypeSelector::~DatatypeSelector()
3643 if (d_stor
!= nullptr)
3649 std::string
DatatypeSelector::getName() const
3651 CVC5_API_TRY_CATCH_BEGIN
;
3652 CVC5_API_CHECK_NOT_NULL
;
3653 //////// all checks before this line
3654 return d_stor
->getName();
3656 CVC5_API_TRY_CATCH_END
;
3659 Term
DatatypeSelector::getSelectorTerm() const
3661 CVC5_API_TRY_CATCH_BEGIN
;
3662 CVC5_API_CHECK_NOT_NULL
;
3663 //////// all checks before this line
3664 return Term(d_solver
, d_stor
->getSelector());
3666 CVC5_API_TRY_CATCH_END
;
3668 Term
DatatypeSelector::getUpdaterTerm() const
3670 CVC5_API_TRY_CATCH_BEGIN
;
3671 CVC5_API_CHECK_NOT_NULL
;
3672 //////// all checks before this line
3673 return Term(d_solver
, d_stor
->getUpdater());
3675 CVC5_API_TRY_CATCH_END
;
3678 Sort
DatatypeSelector::getRangeSort() const
3680 CVC5_API_TRY_CATCH_BEGIN
;
3681 CVC5_API_CHECK_NOT_NULL
;
3682 //////// all checks before this line
3683 return Sort(d_solver
, d_stor
->getRangeType());
3685 CVC5_API_TRY_CATCH_END
;
3688 bool DatatypeSelector::isNull() const
3690 CVC5_API_TRY_CATCH_BEGIN
;
3691 //////// all checks before this line
3692 return isNullHelper();
3694 CVC5_API_TRY_CATCH_END
;
3697 std::string
DatatypeSelector::toString() const
3699 CVC5_API_TRY_CATCH_BEGIN
;
3700 //////// all checks before this line
3701 std::stringstream ss
;
3705 CVC5_API_TRY_CATCH_END
;
3708 std::ostream
& operator<<(std::ostream
& out
, const DatatypeSelector
& stor
)
3710 out
<< stor
.toString();
3714 bool DatatypeSelector::isNullHelper() const { return d_stor
== nullptr; }
3716 /* DatatypeConstructor ------------------------------------------------------ */
3718 DatatypeConstructor::DatatypeConstructor() : d_solver(nullptr), d_ctor(nullptr)
3722 DatatypeConstructor::DatatypeConstructor(const Solver
* slv
,
3723 const cvc5::DTypeConstructor
& ctor
)
3724 : d_solver(slv
), d_ctor(new cvc5::DTypeConstructor(ctor
))
3726 CVC5_API_CHECK(d_ctor
->isResolved())
3727 << "Expected resolved datatype constructor";
3730 DatatypeConstructor::~DatatypeConstructor()
3732 if (d_ctor
!= nullptr)
3738 std::string
DatatypeConstructor::getName() const
3740 CVC5_API_TRY_CATCH_BEGIN
;
3741 CVC5_API_CHECK_NOT_NULL
;
3742 //////// all checks before this line
3743 return d_ctor
->getName();
3745 CVC5_API_TRY_CATCH_END
;
3748 Term
DatatypeConstructor::getConstructorTerm() const
3750 CVC5_API_TRY_CATCH_BEGIN
;
3751 CVC5_API_CHECK_NOT_NULL
;
3752 //////// all checks before this line
3753 return Term(d_solver
, d_ctor
->getConstructor());
3755 CVC5_API_TRY_CATCH_END
;
3758 Term
DatatypeConstructor::getSpecializedConstructorTerm(
3759 const Sort
& retSort
) const
3761 CVC5_API_TRY_CATCH_BEGIN
;
3762 CVC5_API_CHECK_NOT_NULL
;
3763 CVC5_API_CHECK(d_ctor
->isResolved())
3764 << "Expected resolved datatype constructor";
3765 CVC5_API_CHECK(retSort
.isDatatype())
3766 << "Cannot get specialized constructor type for non-datatype type "
3768 //////// all checks before this line
3770 NodeManager
* nm
= d_solver
->getNodeManager();
3772 nm
->mkNode(kind::APPLY_TYPE_ASCRIPTION
,
3773 nm
->mkConst(AscriptionType(
3774 d_ctor
->getSpecializedConstructorType(*retSort
.d_type
))),
3775 d_ctor
->getConstructor());
3776 (void)ret
.getType(true); /* kick off type checking */
3777 // apply type ascription to the operator
3778 Term sctor
= api::Term(d_solver
, ret
);
3781 CVC5_API_TRY_CATCH_END
;
3784 Term
DatatypeConstructor::getTesterTerm() const
3786 CVC5_API_TRY_CATCH_BEGIN
;
3787 CVC5_API_CHECK_NOT_NULL
;
3788 //////// all checks before this line
3789 return Term(d_solver
, d_ctor
->getTester());
3791 CVC5_API_TRY_CATCH_END
;
3794 size_t DatatypeConstructor::getNumSelectors() const
3796 CVC5_API_TRY_CATCH_BEGIN
;
3797 CVC5_API_CHECK_NOT_NULL
;
3798 //////// all checks before this line
3799 return d_ctor
->getNumArgs();
3801 CVC5_API_TRY_CATCH_END
;
3804 DatatypeSelector
DatatypeConstructor::operator[](size_t index
) const
3806 CVC5_API_TRY_CATCH_BEGIN
;
3807 CVC5_API_CHECK_NOT_NULL
;
3808 //////// all checks before this line
3809 return DatatypeSelector(d_solver
, (*d_ctor
)[index
]);
3811 CVC5_API_TRY_CATCH_END
;
3814 DatatypeSelector
DatatypeConstructor::operator[](const std::string
& name
) const
3816 CVC5_API_TRY_CATCH_BEGIN
;
3817 CVC5_API_CHECK_NOT_NULL
;
3818 //////// all checks before this line
3819 return getSelectorForName(name
);
3821 CVC5_API_TRY_CATCH_END
;
3824 DatatypeSelector
DatatypeConstructor::getSelector(const std::string
& name
) const
3826 CVC5_API_TRY_CATCH_BEGIN
;
3827 CVC5_API_CHECK_NOT_NULL
;
3828 //////// all checks before this line
3829 return getSelectorForName(name
);
3831 CVC5_API_TRY_CATCH_END
;
3834 Term
DatatypeConstructor::getSelectorTerm(const std::string
& name
) const
3836 CVC5_API_TRY_CATCH_BEGIN
;
3837 CVC5_API_CHECK_NOT_NULL
;
3838 //////// all checks before this line
3839 return getSelector(name
).getSelectorTerm();
3841 CVC5_API_TRY_CATCH_END
;
3844 DatatypeConstructor::const_iterator
DatatypeConstructor::begin() const
3846 return DatatypeConstructor::const_iterator(d_solver
, *d_ctor
, true);
3849 DatatypeConstructor::const_iterator
DatatypeConstructor::end() const
3851 return DatatypeConstructor::const_iterator(d_solver
, *d_ctor
, false);
3854 DatatypeConstructor::const_iterator::const_iterator(
3855 const Solver
* slv
, const cvc5::DTypeConstructor
& ctor
, bool begin
)
3858 d_int_stors
= &ctor
.getArgs();
3860 const std::vector
<std::shared_ptr
<cvc5::DTypeSelector
>>& sels
=
3862 for (const std::shared_ptr
<cvc5::DTypeSelector
>& s
: sels
)
3864 /* Can not use emplace_back here since constructor is private. */
3865 d_stors
.push_back(DatatypeSelector(d_solver
, *s
.get()));
3867 d_idx
= begin
? 0 : sels
.size();
3870 DatatypeConstructor::const_iterator::const_iterator()
3871 : d_solver(nullptr), d_int_stors(nullptr), d_idx(0)
3875 DatatypeConstructor::const_iterator
&
3876 DatatypeConstructor::const_iterator::operator=(
3877 const DatatypeConstructor::const_iterator
& it
)
3879 d_solver
= it
.d_solver
;
3880 d_int_stors
= it
.d_int_stors
;
3881 d_stors
= it
.d_stors
;
3886 const DatatypeSelector
& DatatypeConstructor::const_iterator::operator*() const
3888 return d_stors
[d_idx
];
3891 const DatatypeSelector
* DatatypeConstructor::const_iterator::operator->() const
3893 return &d_stors
[d_idx
];
3896 DatatypeConstructor::const_iterator
&
3897 DatatypeConstructor::const_iterator::operator++()
3903 DatatypeConstructor::const_iterator
3904 DatatypeConstructor::const_iterator::operator++(int)
3906 DatatypeConstructor::const_iterator
it(*this);
3911 bool DatatypeConstructor::const_iterator::operator==(
3912 const DatatypeConstructor::const_iterator
& other
) const
3914 return d_int_stors
== other
.d_int_stors
&& d_idx
== other
.d_idx
;
3917 bool DatatypeConstructor::const_iterator::operator!=(
3918 const DatatypeConstructor::const_iterator
& other
) const
3920 return d_int_stors
!= other
.d_int_stors
|| d_idx
!= other
.d_idx
;
3923 bool DatatypeConstructor::isNull() const
3925 CVC5_API_TRY_CATCH_BEGIN
;
3926 //////// all checks before this line
3927 return isNullHelper();
3929 CVC5_API_TRY_CATCH_END
;
3932 std::string
DatatypeConstructor::toString() const
3934 CVC5_API_TRY_CATCH_BEGIN
;
3935 //////// all checks before this line
3936 std::stringstream ss
;
3940 CVC5_API_TRY_CATCH_END
;
3943 bool DatatypeConstructor::isNullHelper() const { return d_ctor
== nullptr; }
3945 DatatypeSelector
DatatypeConstructor::getSelectorForName(
3946 const std::string
& name
) const
3948 bool foundSel
= false;
3950 for (size_t i
= 0, nsels
= getNumSelectors(); i
< nsels
; i
++)
3952 if ((*d_ctor
)[i
].getName() == name
)
3961 std::stringstream snames
;
3963 for (size_t i
= 0, ncons
= getNumSelectors(); i
< ncons
; i
++)
3965 snames
<< (*d_ctor
)[i
].getName() << " ";
3968 CVC5_API_CHECK(foundSel
) << "No selector " << name
<< " for constructor "
3969 << getName() << " exists among " << snames
.str();
3971 return DatatypeSelector(d_solver
, (*d_ctor
)[index
]);
3974 std::ostream
& operator<<(std::ostream
& out
, const DatatypeConstructor
& ctor
)
3976 out
<< ctor
.toString();
3980 /* Datatype ----------------------------------------------------------------- */
3982 Datatype::Datatype(const Solver
* slv
, const cvc5::DType
& dtype
)
3983 : d_solver(slv
), d_dtype(new cvc5::DType(dtype
))
3985 CVC5_API_CHECK(d_dtype
->isResolved()) << "Expected resolved datatype";
3988 Datatype::Datatype() : d_solver(nullptr), d_dtype(nullptr) {}
3990 Datatype::~Datatype()
3992 if (d_dtype
!= nullptr)
3998 DatatypeConstructor
Datatype::operator[](size_t idx
) const
4000 CVC5_API_TRY_CATCH_BEGIN
;
4001 CVC5_API_CHECK_NOT_NULL
;
4002 CVC5_API_CHECK(idx
< getNumConstructors()) << "Index out of bounds.";
4003 //////// all checks before this line
4004 return DatatypeConstructor(d_solver
, (*d_dtype
)[idx
]);
4006 CVC5_API_TRY_CATCH_END
;
4009 DatatypeConstructor
Datatype::operator[](const std::string
& name
) const
4011 CVC5_API_TRY_CATCH_BEGIN
;
4012 CVC5_API_CHECK_NOT_NULL
;
4013 //////// all checks before this line
4014 return getConstructorForName(name
);
4016 CVC5_API_TRY_CATCH_END
;
4019 DatatypeConstructor
Datatype::getConstructor(const std::string
& name
) const
4021 CVC5_API_TRY_CATCH_BEGIN
;
4022 CVC5_API_CHECK_NOT_NULL
;
4023 //////// all checks before this line
4024 return getConstructorForName(name
);
4026 CVC5_API_TRY_CATCH_END
;
4029 Term
Datatype::getConstructorTerm(const std::string
& name
) const
4031 CVC5_API_TRY_CATCH_BEGIN
;
4032 CVC5_API_CHECK_NOT_NULL
;
4033 //////// all checks before this line
4034 return getConstructorForName(name
).getConstructorTerm();
4036 CVC5_API_TRY_CATCH_END
;
4039 DatatypeSelector
Datatype::getSelector(const std::string
& name
) const
4041 CVC5_API_TRY_CATCH_BEGIN
;
4042 CVC5_API_CHECK_NOT_NULL
;
4043 //////// all checks before this line
4044 return getSelectorForName(name
);
4046 CVC5_API_TRY_CATCH_END
;
4049 std::string
Datatype::getName() const
4051 CVC5_API_TRY_CATCH_BEGIN
;
4052 CVC5_API_CHECK_NOT_NULL
;
4053 //////// all checks before this line
4054 return d_dtype
->getName();
4056 CVC5_API_TRY_CATCH_END
;
4059 size_t Datatype::getNumConstructors() const
4061 CVC5_API_TRY_CATCH_BEGIN
;
4062 CVC5_API_CHECK_NOT_NULL
;
4063 //////// all checks before this line
4064 return d_dtype
->getNumConstructors();
4066 CVC5_API_TRY_CATCH_END
;
4069 bool Datatype::isParametric() const
4071 CVC5_API_TRY_CATCH_BEGIN
;
4072 CVC5_API_CHECK_NOT_NULL
;
4073 //////// all checks before this line
4074 return d_dtype
->isParametric();
4076 CVC5_API_TRY_CATCH_END
;
4079 bool Datatype::isCodatatype() const
4081 CVC5_API_TRY_CATCH_BEGIN
;
4082 CVC5_API_CHECK_NOT_NULL
;
4083 //////// all checks before this line
4084 return d_dtype
->isCodatatype();
4086 CVC5_API_TRY_CATCH_END
;
4089 bool Datatype::isTuple() const
4091 CVC5_API_TRY_CATCH_BEGIN
;
4092 CVC5_API_CHECK_NOT_NULL
;
4093 //////// all checks before this line
4094 return d_dtype
->isTuple();
4096 CVC5_API_TRY_CATCH_END
;
4099 bool Datatype::isRecord() const
4101 CVC5_API_TRY_CATCH_BEGIN
;
4102 CVC5_API_CHECK_NOT_NULL
;
4103 //////// all checks before this line
4104 return d_dtype
->isRecord();
4106 CVC5_API_TRY_CATCH_END
;
4109 bool Datatype::isFinite() const
4111 CVC5_API_TRY_CATCH_BEGIN
;
4112 CVC5_API_CHECK_NOT_NULL
;
4113 //////// all checks before this line
4114 // we assume that finite model finding is disabled by passing false as the
4116 return isCardinalityClassFinite(d_dtype
->getCardinalityClass(), false);
4118 CVC5_API_TRY_CATCH_END
;
4121 bool Datatype::isWellFounded() const
4123 CVC5_API_TRY_CATCH_BEGIN
;
4124 CVC5_API_CHECK_NOT_NULL
;
4125 //////// all checks before this line
4126 return d_dtype
->isWellFounded();
4128 CVC5_API_TRY_CATCH_END
;
4130 bool Datatype::hasNestedRecursion() const
4132 CVC5_API_TRY_CATCH_BEGIN
;
4133 CVC5_API_CHECK_NOT_NULL
;
4134 //////// all checks before this line
4135 return d_dtype
->hasNestedRecursion();
4137 CVC5_API_TRY_CATCH_END
;
4140 bool Datatype::isNull() const
4142 CVC5_API_TRY_CATCH_BEGIN
;
4143 //////// all checks before this line
4144 return isNullHelper();
4146 CVC5_API_TRY_CATCH_END
;
4149 std::string
Datatype::toString() const
4151 CVC5_API_TRY_CATCH_BEGIN
;
4152 CVC5_API_CHECK_NOT_NULL
;
4153 //////// all checks before this line
4154 return d_dtype
->getName();
4156 CVC5_API_TRY_CATCH_END
;
4159 Datatype::const_iterator
Datatype::begin() const
4161 return Datatype::const_iterator(d_solver
, *d_dtype
, true);
4164 Datatype::const_iterator
Datatype::end() const
4166 return Datatype::const_iterator(d_solver
, *d_dtype
, false);
4169 DatatypeConstructor
Datatype::getConstructorForName(
4170 const std::string
& name
) const
4172 bool foundCons
= false;
4174 for (size_t i
= 0, ncons
= getNumConstructors(); i
< ncons
; i
++)
4176 if ((*d_dtype
)[i
].getName() == name
)
4185 std::stringstream snames
;
4187 for (size_t i
= 0, ncons
= getNumConstructors(); i
< ncons
; i
++)
4189 snames
<< (*d_dtype
)[i
].getName() << " ";
4192 CVC5_API_CHECK(foundCons
) << "No constructor " << name
<< " for datatype "
4193 << getName() << " exists, among " << snames
.str();
4195 return DatatypeConstructor(d_solver
, (*d_dtype
)[index
]);
4198 DatatypeSelector
Datatype::getSelectorForName(const std::string
& name
) const
4200 bool foundSel
= false;
4203 for (size_t i
= 0, ncons
= getNumConstructors(); i
< ncons
; i
++)
4205 int si
= (*d_dtype
)[i
].getSelectorIndexForName(name
);
4208 sindex
= static_cast<size_t>(si
);
4216 CVC5_API_CHECK(foundSel
)
4217 << "No select " << name
<< " for datatype " << getName() << " exists";
4219 return DatatypeSelector(d_solver
, (*d_dtype
)[index
][sindex
]);
4222 Datatype::const_iterator::const_iterator(const Solver
* slv
,
4223 const cvc5::DType
& dtype
,
4225 : d_solver(slv
), d_int_ctors(&dtype
.getConstructors())
4227 const std::vector
<std::shared_ptr
<DTypeConstructor
>>& cons
=
4228 dtype
.getConstructors();
4229 for (const std::shared_ptr
<DTypeConstructor
>& c
: cons
)
4231 /* Can not use emplace_back here since constructor is private. */
4232 d_ctors
.push_back(DatatypeConstructor(d_solver
, *c
.get()));
4234 d_idx
= begin
? 0 : cons
.size();
4237 Datatype::const_iterator::const_iterator()
4238 : d_solver(nullptr), d_int_ctors(nullptr), d_idx(0)
4242 Datatype::const_iterator
& Datatype::const_iterator::operator=(
4243 const Datatype::const_iterator
& it
)
4245 d_solver
= it
.d_solver
;
4246 d_int_ctors
= it
.d_int_ctors
;
4247 d_ctors
= it
.d_ctors
;
4252 const DatatypeConstructor
& Datatype::const_iterator::operator*() const
4254 return d_ctors
[d_idx
];
4257 const DatatypeConstructor
* Datatype::const_iterator::operator->() const
4259 return &d_ctors
[d_idx
];
4262 Datatype::const_iterator
& Datatype::const_iterator::operator++()
4268 Datatype::const_iterator
Datatype::const_iterator::operator++(int)
4270 Datatype::const_iterator
it(*this);
4275 bool Datatype::const_iterator::operator==(
4276 const Datatype::const_iterator
& other
) const
4278 return d_int_ctors
== other
.d_int_ctors
&& d_idx
== other
.d_idx
;
4281 bool Datatype::const_iterator::operator!=(
4282 const Datatype::const_iterator
& other
) const
4284 return d_int_ctors
!= other
.d_int_ctors
|| d_idx
!= other
.d_idx
;
4287 bool Datatype::isNullHelper() const { return d_dtype
== nullptr; }
4289 /* -------------------------------------------------------------------------- */
4291 /* -------------------------------------------------------------------------- */
4294 : d_solver(nullptr),
4304 Grammar::Grammar(const Solver
* slv
,
4305 const std::vector
<Term
>& sygusVars
,
4306 const std::vector
<Term
>& ntSymbols
)
4308 d_sygusVars(sygusVars
),
4309 d_ntSyms(ntSymbols
),
4310 d_ntsToTerms(ntSymbols
.size()),
4315 for (Term ntsymbol
: d_ntSyms
)
4317 d_ntsToTerms
.emplace(ntsymbol
, std::vector
<Term
>());
4321 void Grammar::addRule(const Term
& ntSymbol
, const Term
& rule
)
4323 CVC5_API_TRY_CATCH_BEGIN
;
4324 CVC5_API_CHECK(!d_isResolved
) << "Grammar cannot be modified after passing "
4325 "it as an argument to synthFun/synthInv";
4326 CVC5_API_CHECK_TERM(ntSymbol
);
4327 CVC5_API_CHECK_TERM(rule
);
4328 CVC5_API_ARG_CHECK_EXPECTED(
4329 d_ntsToTerms
.find(ntSymbol
) != d_ntsToTerms
.cend(), ntSymbol
)
4330 << "ntSymbol to be one of the non-terminal symbols given in the "
4332 CVC5_API_CHECK(ntSymbol
.d_node
->getType() == rule
.d_node
->getType())
4333 << "Expected ntSymbol and rule to have the same sort";
4334 CVC5_API_ARG_CHECK_EXPECTED(!containsFreeVariables(rule
), rule
)
4335 << "a term whose free variables are limited to synthFun/synthInv "
4336 "parameters and non-terminal symbols of the grammar";
4337 //////// all checks before this line
4338 d_ntsToTerms
[ntSymbol
].push_back(rule
);
4340 CVC5_API_TRY_CATCH_END
;
4343 void Grammar::addRules(const Term
& ntSymbol
, const std::vector
<Term
>& rules
)
4345 CVC5_API_TRY_CATCH_BEGIN
;
4346 CVC5_API_CHECK(!d_isResolved
) << "Grammar cannot be modified after passing "
4347 "it as an argument to synthFun/synthInv";
4348 CVC5_API_CHECK_TERM(ntSymbol
);
4349 CVC5_API_CHECK_TERMS_WITH_SORT(rules
, ntSymbol
.getSort());
4350 CVC5_API_ARG_CHECK_EXPECTED(
4351 d_ntsToTerms
.find(ntSymbol
) != d_ntsToTerms
.cend(), ntSymbol
)
4352 << "ntSymbol to be one of the non-terminal symbols given in the "
4354 for (size_t i
= 0, n
= rules
.size(); i
< n
; ++i
)
4356 CVC5_API_ARG_AT_INDEX_CHECK_EXPECTED(
4357 !containsFreeVariables(rules
[i
]), rules
[i
], rules
, i
)
4358 << "a term whose free variables are limited to synthFun/synthInv "
4359 "parameters and non-terminal symbols of the grammar";
4361 //////// all checks before this line
4362 d_ntsToTerms
[ntSymbol
].insert(
4363 d_ntsToTerms
[ntSymbol
].cend(), rules
.cbegin(), rules
.cend());
4365 CVC5_API_TRY_CATCH_END
;
4368 void Grammar::addAnyConstant(const Term
& ntSymbol
)
4370 CVC5_API_TRY_CATCH_BEGIN
;
4371 CVC5_API_CHECK(!d_isResolved
) << "Grammar cannot be modified after passing "
4372 "it as an argument to synthFun/synthInv";
4373 CVC5_API_CHECK_TERM(ntSymbol
);
4374 CVC5_API_ARG_CHECK_EXPECTED(
4375 d_ntsToTerms
.find(ntSymbol
) != d_ntsToTerms
.cend(), ntSymbol
)
4376 << "ntSymbol to be one of the non-terminal symbols given in the "
4378 //////// all checks before this line
4379 d_allowConst
.insert(ntSymbol
);
4381 CVC5_API_TRY_CATCH_END
;
4384 void Grammar::addAnyVariable(const Term
& ntSymbol
)
4386 CVC5_API_TRY_CATCH_BEGIN
;
4387 CVC5_API_CHECK(!d_isResolved
) << "Grammar cannot be modified after passing "
4388 "it as an argument to synthFun/synthInv";
4389 CVC5_API_CHECK_TERM(ntSymbol
);
4390 CVC5_API_ARG_CHECK_EXPECTED(
4391 d_ntsToTerms
.find(ntSymbol
) != d_ntsToTerms
.cend(), ntSymbol
)
4392 << "ntSymbol to be one of the non-terminal symbols given in the "
4394 //////// all checks before this line
4395 d_allowVars
.insert(ntSymbol
);
4397 CVC5_API_TRY_CATCH_END
;
4401 * This function concatenates the outputs of calling f on each element between
4402 * first and last, seperated by sep.
4403 * @param first the beginning of the range
4404 * @param last the end of the range
4405 * @param f the function to call on each element in the range, its output must
4406 * be overloaded for operator<<
4407 * @param sep the string to add between successive calls to f
4409 template <typename Iterator
, typename Function
>
4410 std::string
join(Iterator first
, Iterator last
, Function f
, std::string sep
)
4412 std::stringstream ss
;
4430 std::string
Grammar::toString() const
4432 CVC5_API_TRY_CATCH_BEGIN
;
4433 //////// all checks before this line
4434 std::stringstream ss
;
4435 ss
<< " (" // pre-declaration
4440 std::stringstream s
;
4441 s
<< '(' << t
<< ' ' << t
.getSort() << ')';
4445 << ")\n (" // grouped rule listing
4449 [this](const Term
& t
) {
4450 bool allowConst
= d_allowConst
.find(t
) != d_allowConst
.cend(),
4451 allowVars
= d_allowVars
.find(t
) != d_allowVars
.cend();
4452 const std::vector
<Term
>& rules
= d_ntsToTerms
.at(t
);
4453 std::stringstream s
;
4454 s
<< '(' << t
<< ' ' << t
.getSort() << " ("
4455 << (allowConst
? "(Constant " + t
.getSort().toString() + ")"
4457 << (allowConst
&& allowVars
? " " : "")
4458 << (allowVars
? "(Var " + t
.getSort().toString() + ")" : "")
4459 << ((allowConst
|| allowVars
) && !rules
.empty() ? " " : "")
4463 [](const Term
& rule
) { return rule
.toString(); },
4473 CVC5_API_TRY_CATCH_END
;
4476 Sort
Grammar::resolve()
4478 CVC5_API_TRY_CATCH_BEGIN
;
4479 //////// all checks before this line
4481 d_isResolved
= true;
4485 if (!d_sygusVars
.empty())
4489 d_solver
->getNodeManager()->mkNode(
4490 cvc5::kind::BOUND_VAR_LIST
, Term::termVectorToNodes(d_sygusVars
)));
4493 std::unordered_map
<Term
, Sort
> ntsToUnres(d_ntSyms
.size());
4495 for (Term ntsymbol
: d_ntSyms
)
4497 // make the unresolved type, used for referencing the final version of
4498 // the ntsymbol's datatype
4499 ntsToUnres
[ntsymbol
] =
4500 Sort(d_solver
, d_solver
->getNodeManager()->mkSort(ntsymbol
.toString()));
4503 std::vector
<cvc5::DType
> datatypes
;
4504 std::set
<TypeNode
> unresTypes
;
4506 datatypes
.reserve(d_ntSyms
.size());
4508 for (const Term
& ntSym
: d_ntSyms
)
4510 // make the datatype, which encodes terms generated by this non-terminal
4511 DatatypeDecl
dtDecl(d_solver
, ntSym
.toString());
4513 for (const Term
& consTerm
: d_ntsToTerms
[ntSym
])
4515 addSygusConstructorTerm(dtDecl
, consTerm
, ntsToUnres
);
4518 if (d_allowVars
.find(ntSym
) != d_allowVars
.cend())
4520 addSygusConstructorVariables(dtDecl
,
4521 Sort(d_solver
, ntSym
.d_node
->getType()));
4524 bool aci
= d_allowConst
.find(ntSym
) != d_allowConst
.end();
4525 TypeNode btt
= ntSym
.d_node
->getType();
4526 dtDecl
.d_dtype
->setSygus(btt
, *bvl
.d_node
, aci
, false);
4528 // We can be in a case where the only rule specified was (Variable T)
4529 // and there are no variables of type T, in which case this is a bogus
4530 // grammar. This results in the error below.
4531 CVC5_API_CHECK(dtDecl
.d_dtype
->getNumConstructors() != 0)
4532 << "Grouped rule listing for " << *dtDecl
.d_dtype
4533 << " produced an empty rule list";
4535 datatypes
.push_back(*dtDecl
.d_dtype
);
4536 unresTypes
.insert(*ntsToUnres
[ntSym
].d_type
);
4539 std::vector
<TypeNode
> datatypeTypes
=
4540 d_solver
->getNodeManager()->mkMutualDatatypeTypes(
4541 datatypes
, unresTypes
, NodeManager::DATATYPE_FLAG_PLACEHOLDER
);
4543 // return is the first datatype
4544 return Sort(d_solver
, datatypeTypes
[0]);
4546 CVC5_API_TRY_CATCH_END
;
4549 void Grammar::addSygusConstructorTerm(
4552 const std::unordered_map
<Term
, Sort
>& ntsToUnres
) const
4554 CVC5_API_TRY_CATCH_BEGIN
;
4555 CVC5_API_CHECK_DTDECL(dt
);
4556 CVC5_API_CHECK_TERM(term
);
4557 CVC5_API_CHECK_TERMS_MAP(ntsToUnres
);
4558 //////// all checks before this line
4560 // At this point, we should know that dt is well founded, and that its
4561 // builtin sygus operators are well-typed.
4562 // Now, purify each occurrence of a non-terminal symbol in term, replace by
4563 // free variables. These become arguments to constructors. Notice we must do
4564 // a tree traversal in this function, since unique paths to the same term
4565 // should be treated as distinct terms.
4566 // Notice that let expressions are forbidden in the input syntax of term, so
4567 // this does not lead to exponential behavior with respect to input size.
4568 std::vector
<Term
> args
;
4569 std::vector
<Sort
> cargs
;
4570 Term op
= purifySygusGTerm(term
, args
, cargs
, ntsToUnres
);
4571 std::stringstream ssCName
;
4572 ssCName
<< op
.getKind();
4577 d_solver
->getNodeManager()->mkNode(cvc5::kind::BOUND_VAR_LIST
,
4578 Term::termVectorToNodes(args
)));
4579 // its operator is a lambda
4581 d_solver
->getNodeManager()->mkNode(
4582 cvc5::kind::LAMBDA
, *lbvl
.d_node
, *op
.d_node
));
4584 std::vector
<TypeNode
> cargst
= Sort::sortVectorToTypeNodes(cargs
);
4585 dt
.d_dtype
->addSygusConstructor(*op
.d_node
, ssCName
.str(), cargst
);
4587 CVC5_API_TRY_CATCH_END
;
4590 Term
Grammar::purifySygusGTerm(
4592 std::vector
<Term
>& args
,
4593 std::vector
<Sort
>& cargs
,
4594 const std::unordered_map
<Term
, Sort
>& ntsToUnres
) const
4596 CVC5_API_TRY_CATCH_BEGIN
;
4597 CVC5_API_CHECK_TERM(term
);
4598 CVC5_API_CHECK_TERMS(args
);
4599 CVC5_API_CHECK_SORTS(cargs
);
4600 CVC5_API_CHECK_TERMS_MAP(ntsToUnres
);
4601 //////// all checks before this line
4603 std::unordered_map
<Term
, Sort
>::const_iterator itn
= ntsToUnres
.find(term
);
4604 if (itn
!= ntsToUnres
.cend())
4608 d_solver
->getNodeManager()->mkBoundVar(term
.d_node
->getType()));
4609 args
.push_back(ret
);
4610 cargs
.push_back(itn
->second
);
4613 std::vector
<Term
> pchildren
;
4614 bool childChanged
= false;
4615 for (unsigned i
= 0, nchild
= term
.d_node
->getNumChildren(); i
< nchild
; i
++)
4617 Term ptermc
= purifySygusGTerm(
4618 Term(d_solver
, (*term
.d_node
)[i
]), args
, cargs
, ntsToUnres
);
4619 pchildren
.push_back(ptermc
);
4620 childChanged
= childChanged
|| *ptermc
.d_node
!= (*term
.d_node
)[i
];
4629 if (term
.d_node
->getMetaKind() == kind::metakind::PARAMETERIZED
)
4631 // it's an indexed operator so we should provide the op
4632 NodeBuilder
nb(term
.d_node
->getKind());
4633 nb
<< term
.d_node
->getOperator();
4634 nb
.append(Term::termVectorToNodes(pchildren
));
4635 nret
= nb
.constructNode();
4639 nret
= d_solver
->getNodeManager()->mkNode(
4640 term
.d_node
->getKind(), Term::termVectorToNodes(pchildren
));
4643 return Term(d_solver
, nret
);
4645 CVC5_API_TRY_CATCH_END
;
4648 void Grammar::addSygusConstructorVariables(DatatypeDecl
& dt
,
4649 const Sort
& sort
) const
4651 CVC5_API_TRY_CATCH_BEGIN
;
4652 CVC5_API_CHECK_DTDECL(dt
);
4653 CVC5_API_CHECK_SORT(sort
);
4654 //////// all checks before this line
4656 // each variable of appropriate type becomes a sygus constructor in dt.
4657 for (unsigned i
= 0, size
= d_sygusVars
.size(); i
< size
; i
++)
4659 Term v
= d_sygusVars
[i
];
4660 if (v
.d_node
->getType() == *sort
.d_type
)
4662 std::stringstream ss
;
4664 std::vector
<TypeNode
> cargs
;
4665 dt
.d_dtype
->addSygusConstructor(*v
.d_node
, ss
.str(), cargs
);
4669 CVC5_API_TRY_CATCH_END
;
4672 bool Grammar::containsFreeVariables(const Term
& rule
) const
4674 std::unordered_set
<TNode
> scope
;
4676 for (const Term
& sygusVar
: d_sygusVars
)
4678 scope
.emplace(*sygusVar
.d_node
);
4681 for (const Term
& ntsymbol
: d_ntSyms
)
4683 scope
.emplace(*ntsymbol
.d_node
);
4686 std::unordered_set
<Node
> fvs
;
4687 return expr::getFreeVariablesScope(*rule
.d_node
, fvs
, scope
, false);
4690 std::ostream
& operator<<(std::ostream
& out
, const Grammar
& grammar
)
4692 return out
<< grammar
.toString();
4695 /* -------------------------------------------------------------------------- */
4696 /* Rounding Mode for Floating Points */
4697 /* -------------------------------------------------------------------------- */
4699 const static std::unordered_map
<RoundingMode
, cvc5::RoundingMode
> s_rmodes
{
4700 {ROUND_NEAREST_TIES_TO_EVEN
,
4701 cvc5::RoundingMode::ROUND_NEAREST_TIES_TO_EVEN
},
4702 {ROUND_TOWARD_POSITIVE
, cvc5::RoundingMode::ROUND_TOWARD_POSITIVE
},
4703 {ROUND_TOWARD_NEGATIVE
, cvc5::RoundingMode::ROUND_TOWARD_NEGATIVE
},
4704 {ROUND_TOWARD_ZERO
, cvc5::RoundingMode::ROUND_TOWARD_ZERO
},
4705 {ROUND_NEAREST_TIES_TO_AWAY
,
4706 cvc5::RoundingMode::ROUND_NEAREST_TIES_TO_AWAY
},
4709 const static std::unordered_map
<cvc5::RoundingMode
,
4711 cvc5::RoundingModeHashFunction
>
4713 {cvc5::RoundingMode::ROUND_NEAREST_TIES_TO_EVEN
,
4714 ROUND_NEAREST_TIES_TO_EVEN
},
4715 {cvc5::RoundingMode::ROUND_TOWARD_POSITIVE
, ROUND_TOWARD_POSITIVE
},
4716 {cvc5::RoundingMode::ROUND_TOWARD_POSITIVE
, ROUND_TOWARD_NEGATIVE
},
4717 {cvc5::RoundingMode::ROUND_TOWARD_ZERO
, ROUND_TOWARD_ZERO
},
4718 {cvc5::RoundingMode::ROUND_NEAREST_TIES_TO_AWAY
,
4719 ROUND_NEAREST_TIES_TO_AWAY
},
4722 /* -------------------------------------------------------------------------- */
4724 /* -------------------------------------------------------------------------- */
4726 DriverOptions::DriverOptions(const Solver
& solver
) : d_solver(solver
) {}
4728 std::istream
& DriverOptions::in() const
4730 return *d_solver
.d_slv
->getOptions().base
.in
;
4732 std::ostream
& DriverOptions::err() const
4734 return *d_solver
.d_slv
->getOptions().base
.err
;
4736 std::ostream
& DriverOptions::out() const
4738 return *d_solver
.d_slv
->getOptions().base
.out
;
4741 /* -------------------------------------------------------------------------- */
4743 /* -------------------------------------------------------------------------- */
4745 struct Stat::StatData
4747 cvc5::StatExportData data
;
4748 template <typename T
>
4749 StatData(T
&& t
) : data(std::forward
<T
>(t
))
4752 StatData() : data() {}
4756 Stat::Stat(const Stat
& s
)
4757 : d_expert(s
.d_expert
),
4758 d_default(s
.d_default
),
4759 d_data(std::make_unique
<StatData
>(s
.d_data
->data
))
4762 Stat
& Stat::operator=(const Stat
& s
)
4764 d_expert
= s
.d_expert
;
4765 d_data
= std::make_unique
<StatData
>(s
.d_data
->data
);
4769 bool Stat::isExpert() const { return d_expert
; }
4770 bool Stat::isDefault() const { return d_default
; }
4772 bool Stat::isInt() const
4774 return std::holds_alternative
<int64_t>(d_data
->data
);
4776 int64_t Stat::getInt() const
4778 CVC5_API_TRY_CATCH_BEGIN
;
4779 CVC5_API_RECOVERABLE_CHECK(isInt()) << "Expected Stat of type int64_t.";
4780 return std::get
<int64_t>(d_data
->data
);
4781 CVC5_API_TRY_CATCH_END
;
4783 bool Stat::isDouble() const
4785 return std::holds_alternative
<double>(d_data
->data
);
4787 double Stat::getDouble() const
4789 CVC5_API_TRY_CATCH_BEGIN
;
4790 CVC5_API_RECOVERABLE_CHECK(isDouble()) << "Expected Stat of type double.";
4791 return std::get
<double>(d_data
->data
);
4792 CVC5_API_TRY_CATCH_END
;
4794 bool Stat::isString() const
4796 return std::holds_alternative
<std::string
>(d_data
->data
);
4798 const std::string
& Stat::getString() const
4800 CVC5_API_TRY_CATCH_BEGIN
;
4801 CVC5_API_RECOVERABLE_CHECK(isString())
4802 << "Expected Stat of type std::string.";
4803 return std::get
<std::string
>(d_data
->data
);
4804 CVC5_API_TRY_CATCH_END
;
4806 bool Stat::isHistogram() const
4808 return std::holds_alternative
<HistogramData
>(d_data
->data
);
4810 const Stat::HistogramData
& Stat::getHistogram() const
4812 CVC5_API_TRY_CATCH_BEGIN
;
4813 CVC5_API_RECOVERABLE_CHECK(isHistogram())
4814 << "Expected Stat of type histogram.";
4815 return std::get
<HistogramData
>(d_data
->data
);
4816 CVC5_API_TRY_CATCH_END
;
4819 Stat::Stat(bool expert
, bool defaulted
, StatData
&& sd
)
4821 d_default(defaulted
),
4822 d_data(std::make_unique
<StatData
>(std::move(sd
)))
4826 std::ostream
& operator<<(std::ostream
& os
, const Stat
& sv
)
4828 return cvc5::detail::print(os
, sv
.d_data
->data
);
4831 Statistics::BaseType::const_reference
Statistics::iterator::operator*() const
4833 return d_it
.operator*();
4835 Statistics::BaseType::const_pointer
Statistics::iterator::operator->() const
4837 return d_it
.operator->();
4839 Statistics::iterator
& Statistics::iterator::operator++()
4844 } while (!isVisible());
4847 Statistics::iterator
Statistics::iterator::operator++(int)
4849 iterator tmp
= *this;
4853 } while (!isVisible());
4856 Statistics::iterator
& Statistics::iterator::operator--()
4861 } while (!isVisible());
4864 Statistics::iterator
Statistics::iterator::operator--(int)
4866 iterator tmp
= *this;
4870 } while (!isVisible());
4873 bool Statistics::iterator::operator==(const Statistics::iterator
& rhs
) const
4875 return d_it
== rhs
.d_it
;
4877 bool Statistics::iterator::operator!=(const Statistics::iterator
& rhs
) const
4879 return d_it
!= rhs
.d_it
;
4881 Statistics::iterator::iterator(Statistics::BaseType::const_iterator it
,
4882 const Statistics::BaseType
& base
,
4885 : d_it(it
), d_base(&base
), d_showExpert(expert
), d_showDefault(defaulted
)
4887 while (!isVisible())
4892 bool Statistics::iterator::isVisible() const
4894 if (d_it
== d_base
->end()) return true;
4895 if (!d_showExpert
&& d_it
->second
.isExpert()) return false;
4896 if (!d_showDefault
&& d_it
->second
.isDefault()) return false;
4900 const Stat
& Statistics::get(const std::string
& name
)
4902 CVC5_API_TRY_CATCH_BEGIN
;
4903 auto it
= d_stats
.find(name
);
4904 CVC5_API_RECOVERABLE_CHECK(it
!= d_stats
.end())
4905 << "No stat with name \"" << name
<< "\" exists.";
4907 CVC5_API_TRY_CATCH_END
;
4910 Statistics::iterator
Statistics::begin(bool expert
, bool defaulted
) const
4912 return iterator(d_stats
.begin(), d_stats
, expert
, defaulted
);
4914 Statistics::iterator
Statistics::end() const
4916 return iterator(d_stats
.end(), d_stats
, false, false);
4919 Statistics::Statistics(const StatisticsRegistry
& reg
)
4921 for (const auto& svp
: reg
)
4923 d_stats
.emplace(svp
.first
,
4924 Stat(svp
.second
->d_expert
,
4925 svp
.second
->isDefault(),
4926 svp
.second
->getViewer()));
4930 std::ostream
& operator<<(std::ostream
& out
, const Statistics
& stats
)
4932 for (const auto& stat
: stats
)
4934 out
<< stat
.first
<< " = " << stat
.second
<< std::endl
;
4939 /* -------------------------------------------------------------------------- */
4941 /* -------------------------------------------------------------------------- */
4943 Solver::Solver(std::unique_ptr
<Options
>&& original
)
4945 d_nodeMgr
= NodeManager::currentNM();
4947 d_originalOptions
= std::move(original
);
4948 d_slv
.reset(new SolverEngine(d_nodeMgr
, d_originalOptions
.get()));
4949 d_slv
->setSolver(this);
4950 d_rng
.reset(new Random(d_slv
->getOptions().driver
.seed
));
4954 Solver::Solver() : Solver(std::make_unique
<Options
>()) {}
4956 Solver::~Solver() {}
4958 /* Helpers and private functions */
4959 /* -------------------------------------------------------------------------- */
4961 NodeManager
* Solver::getNodeManager(void) const { return d_nodeMgr
; }
4963 void Solver::increment_term_stats(Kind kind
) const
4965 if constexpr (Configuration::isStatisticsBuild())
4967 d_stats
->d_terms
<< kind
;
4971 void Solver::increment_vars_consts_stats(const Sort
& sort
, bool is_var
) const
4973 if constexpr (Configuration::isStatisticsBuild())
4975 const TypeNode tn
= sort
.getTypeNode();
4976 TypeConstant tc
= tn
.getKind() == cvc5::kind::TYPE_CONSTANT
4977 ? tn
.getConst
<TypeConstant
>()
4981 d_stats
->d_vars
<< tc
;
4985 d_stats
->d_consts
<< tc
;
4990 /* Split out to avoid nested API calls (problematic with API tracing). */
4991 /* .......................................................................... */
4993 template <typename T
>
4994 Term
Solver::mkValHelper(T t
) const
4996 //////// all checks before this line
4997 Node res
= getNodeManager()->mkConst(t
);
4998 (void)res
.getType(true); /* kick off type checking */
4999 return Term(this, res
);
5002 Term
Solver::mkRealFromStrHelper(const std::string
& s
) const
5004 //////// all checks before this line
5007 cvc5::Rational r
= s
.find('/') != std::string::npos
5009 : cvc5::Rational::fromDecimal(s
);
5010 return mkValHelper
<cvc5::Rational
>(r
);
5012 catch (const std::invalid_argument
& e
)
5014 /* Catch to throw with a more meaningful error message. To be caught in
5015 * enclosing CVC5_API_TRY_CATCH_* block to throw CVC5ApiException. */
5016 std::stringstream message
;
5017 message
<< "Cannot construct Real or Int from string argument '" << s
<< "'"
5019 throw std::invalid_argument(message
.str());
5023 Term
Solver::mkBVFromIntHelper(uint32_t size
, uint64_t val
) const
5025 CVC5_API_ARG_CHECK_EXPECTED(size
> 0, size
) << "a bit-width > 0";
5026 //////// all checks before this line
5027 return mkValHelper
<cvc5::BitVector
>(cvc5::BitVector(size
, val
));
5030 Term
Solver::mkBVFromStrHelper(uint32_t size
,
5031 const std::string
& s
,
5032 uint32_t base
) const
5034 CVC5_API_ARG_CHECK_EXPECTED(!s
.empty(), s
) << "a non-empty string";
5035 CVC5_API_ARG_CHECK_EXPECTED(base
== 2 || base
== 10 || base
== 16, base
)
5036 << "base 2, 10, or 16";
5037 //////// all checks before this line
5039 Integer
val(s
, base
);
5041 if (val
.strictlyNegative())
5043 CVC5_API_CHECK(val
>= -Integer("2", 10).pow(size
- 1))
5044 << "Overflow in bitvector construction (specified bitvector size "
5045 << size
<< " too small to hold value " << s
<< ")";
5049 CVC5_API_CHECK(val
.modByPow2(size
) == val
)
5050 << "Overflow in bitvector construction (specified bitvector size "
5051 << size
<< " too small to hold value " << s
<< ")";
5053 return mkValHelper
<cvc5::BitVector
>(cvc5::BitVector(size
, val
));
5056 Term
Solver::getValueHelper(const Term
& term
) const
5058 // Note: Term is checked in the caller to avoid double checks
5059 //////// all checks before this line
5060 Node value
= d_slv
->getValue(*term
.d_node
);
5061 Term res
= Term(this, value
);
5062 // May need to wrap in real cast so that user know this is a real.
5063 TypeNode tn
= (*term
.d_node
).getType();
5064 if (!tn
.isInteger() && value
.getType().isInteger())
5066 return ensureRealSort(res
);
5071 Sort
Solver::mkTupleSortHelper(const std::vector
<Sort
>& sorts
) const
5073 // Note: Sorts are checked in the caller to avoid double checks
5074 //////// all checks before this line
5075 std::vector
<TypeNode
> typeNodes
= Sort::sortVectorToTypeNodes(sorts
);
5076 return Sort(this, getNodeManager()->mkTupleType(typeNodes
));
5079 Term
Solver::mkTermFromKind(Kind kind
) const
5081 CVC5_API_KIND_CHECK_EXPECTED(kind
== PI
|| kind
== REGEXP_EMPTY
5082 || kind
== REGEXP_SIGMA
|| kind
== SEP_EMP
,
5084 << "PI, REGEXP_EMPTY, REGEXP_SIGMA or SEP_EMP";
5085 //////// all checks before this line
5087 cvc5::Kind k
= extToIntKind(kind
);
5088 if (kind
== REGEXP_EMPTY
|| kind
== REGEXP_SIGMA
)
5090 Assert(isDefinedIntKind(k
));
5091 res
= d_nodeMgr
->mkNode(k
, std::vector
<Node
>());
5093 else if (kind
== SEP_EMP
)
5095 res
= d_nodeMgr
->mkNullaryOperator(d_nodeMgr
->booleanType(), k
);
5100 res
= d_nodeMgr
->mkNullaryOperator(d_nodeMgr
->realType(), k
);
5102 (void)res
.getType(true); /* kick off type checking */
5103 increment_term_stats(kind
);
5104 return Term(this, res
);
5107 Term
Solver::mkTermHelper(Kind kind
, const std::vector
<Term
>& children
) const
5109 // Note: Kind and children are checked in the caller to avoid double checks
5110 //////// all checks before this line
5112 std::vector
<Node
> echildren
= Term::termVectorToNodes(children
);
5113 cvc5::Kind k
= extToIntKind(kind
);
5115 if (echildren
.size() > 2)
5117 if (kind
== INTS_DIVISION
|| kind
== XOR
|| kind
== MINUS
5118 || kind
== DIVISION
|| kind
== HO_APPLY
|| kind
== REGEXP_DIFF
)
5120 // left-associative, but cvc5 internally only supports 2 args
5121 res
= d_nodeMgr
->mkLeftAssociative(k
, echildren
);
5123 else if (kind
== IMPLIES
)
5125 // right-associative, but cvc5 internally only supports 2 args
5126 res
= d_nodeMgr
->mkRightAssociative(k
, echildren
);
5128 else if (kind
== EQUAL
|| kind
== LT
|| kind
== GT
|| kind
== LEQ
5131 // "chainable", but cvc5 internally only supports 2 args
5132 res
= d_nodeMgr
->mkChain(k
, echildren
);
5134 else if (kind::isAssociative(k
))
5136 // mkAssociative has special treatment for associative operators with lots
5138 res
= d_nodeMgr
->mkAssociative(k
, echildren
);
5142 // default case, must check kind
5143 checkMkTerm(kind
, children
.size());
5144 res
= d_nodeMgr
->mkNode(k
, echildren
);
5147 else if (kind::isAssociative(k
))
5149 // associative case, same as above
5150 res
= d_nodeMgr
->mkAssociative(k
, echildren
);
5154 // default case, same as above
5155 checkMkTerm(kind
, children
.size());
5156 if (kind
== api::SINGLETON
)
5158 // the type of the term is the same as the type of the internal node
5159 // see Term::getSort()
5160 TypeNode type
= children
[0].d_node
->getType();
5161 // Internally NodeManager::mkSingleton needs a type argument
5162 // to construct a singleton, since there is no difference between
5163 // integers and reals (both are Rationals).
5164 // At the API, mkReal and mkInteger are different and therefore the
5165 // element type can be used safely here.
5166 res
= getNodeManager()->mkSingleton(type
, *children
[0].d_node
);
5168 else if (kind
== api::MK_BAG
)
5170 // the type of the term is the same as the type of the internal node
5171 // see Term::getSort()
5172 TypeNode type
= children
[0].d_node
->getType();
5173 // Internally NodeManager::mkBag needs a type argument
5174 // to construct a bag, since there is no difference between
5175 // integers and reals (both are Rationals).
5176 // At the API, mkReal and mkInteger are different and therefore the
5177 // element type can be used safely here.
5178 res
= getNodeManager()->mkBag(
5179 type
, *children
[0].d_node
, *children
[1].d_node
);
5183 res
= d_nodeMgr
->mkNode(k
, echildren
);
5187 (void)res
.getType(true); /* kick off type checking */
5188 increment_term_stats(kind
);
5189 return Term(this, res
);
5192 Term
Solver::mkTermHelper(const Op
& op
, const std::vector
<Term
>& children
) const
5194 // Note: Op and children are checked in the caller to avoid double checks
5195 checkMkTerm(op
.d_kind
, children
.size());
5196 //////// all checks before this line
5198 if (!op
.isIndexedHelper())
5200 return mkTermHelper(op
.d_kind
, children
);
5203 const cvc5::Kind int_kind
= extToIntKind(op
.d_kind
);
5204 std::vector
<Node
> echildren
= Term::termVectorToNodes(children
);
5206 NodeBuilder
nb(int_kind
);
5208 nb
.append(echildren
);
5209 Node res
= nb
.constructNode();
5211 (void)res
.getType(true); /* kick off type checking */
5212 return Term(this, res
);
5215 std::vector
<Sort
> Solver::mkDatatypeSortsInternal(
5216 const std::vector
<DatatypeDecl
>& dtypedecls
,
5217 const std::set
<Sort
>& unresolvedSorts
) const
5219 // Note: dtypedecls and unresolvedSorts are checked in the caller to avoid
5221 //////// all checks before this line
5223 std::vector
<cvc5::DType
> datatypes
;
5224 for (size_t i
= 0, ndts
= dtypedecls
.size(); i
< ndts
; ++i
)
5226 datatypes
.push_back(dtypedecls
[i
].getDatatype());
5229 std::set
<TypeNode
> utypes
= Sort::sortSetToTypeNodes(unresolvedSorts
);
5230 std::vector
<cvc5::TypeNode
> dtypes
=
5231 getNodeManager()->mkMutualDatatypeTypes(datatypes
, utypes
);
5232 std::vector
<Sort
> retTypes
= Sort::typeNodeVectorToSorts(this, dtypes
);
5236 Term
Solver::synthFunHelper(const std::string
& symbol
,
5237 const std::vector
<Term
>& boundVars
,
5240 Grammar
* grammar
) const
5242 // Note: boundVars, sort and grammar are checked in the caller to avoid
5244 std::vector
<TypeNode
> varTypes
;
5245 for (const auto& bv
: boundVars
)
5249 CVC5_API_CHECK(grammar
->d_ntSyms
[0].d_node
->getType() == *sort
.d_type
)
5250 << "Invalid Start symbol for grammar, Expected Start's sort to be "
5251 << *sort
.d_type
<< " but found "
5252 << grammar
->d_ntSyms
[0].d_node
->getType();
5254 varTypes
.push_back(bv
.d_node
->getType());
5256 //////// all checks before this line
5258 TypeNode funType
= varTypes
.empty() ? *sort
.d_type
5259 : getNodeManager()->mkFunctionType(
5260 varTypes
, *sort
.d_type
);
5262 Node fun
= getNodeManager()->mkBoundVar(symbol
, funType
);
5263 (void)fun
.getType(true); /* kick off type checking */
5265 std::vector
<Node
> bvns
= Term::termVectorToNodes(boundVars
);
5267 d_slv
->declareSynthFun(
5269 grammar
== nullptr ? funType
: *grammar
->resolve().d_type
,
5273 return Term(this, fun
);
5276 Term
Solver::ensureTermSort(const Term
& term
, const Sort
& sort
) const
5278 // Note: Term and sort are checked in the caller to avoid double checks
5279 CVC5_API_CHECK(term
.getSort() == sort
5280 || (term
.getSort().isInteger() && sort
.isReal()))
5281 << "Expected conversion from Int to Real";
5282 //////// all checks before this line
5284 Sort t
= term
.getSort();
5285 if (term
.getSort() == sort
)
5290 // Integers are reals, too
5291 Assert(t
.d_type
->isReal());
5295 // Must cast to Real to ensure correct type is passed to parametric type
5296 // constructors. We do this cast using division with 1. This has the
5297 // advantage wrt using TO_REAL since (constant) division is always included
5300 d_nodeMgr
->mkNode(extToIntKind(DIVISION
),
5302 d_nodeMgr
->mkConst(cvc5::Rational(1))));
5304 Assert(res
.getSort() == sort
);
5308 Term
Solver::ensureRealSort(const Term
& t
) const
5310 Assert(this == t
.d_solver
);
5311 CVC5_API_ARG_CHECK_EXPECTED(
5312 t
.getSort() == getIntegerSort() || t
.getSort() == getRealSort(),
5313 " an integer or real term");
5314 // Note: Term is checked in the caller to avoid double checks
5315 //////// all checks before this line
5316 if (t
.getSort() == getIntegerSort())
5318 Node n
= getNodeManager()->mkNode(kind::CAST_TO_REAL
, *t
.d_node
);
5319 return Term(this, n
);
5324 bool Solver::isValidInteger(const std::string
& s
) const
5326 //////// all checks before this line
5327 if (s
.length() == 0)
5329 // string should not be empty
5334 if (s
[index
] == '-')
5336 if (s
.length() == 1)
5338 // negative integers should contain at least one digit
5344 if (s
[index
] == '0' && s
.length() > (index
+ 1))
5346 // From SMT-Lib 2.6: A <numeral> is the digit 0 or a non-empty sequence of
5347 // digits not starting with 0. So integers like 001, 000 are not allowed
5351 // all remaining characters should be decimal digits
5352 for (; index
< s
.length(); ++index
)
5354 if (!std::isdigit(s
[index
]))
5363 void Solver::resetStatistics()
5365 if constexpr (Configuration::isStatisticsBuild())
5367 d_stats
.reset(new APIStatistics
{
5368 d_slv
->getStatisticsRegistry().registerHistogram
<TypeConstant
>(
5370 d_slv
->getStatisticsRegistry().registerHistogram
<TypeConstant
>(
5372 d_slv
->getStatisticsRegistry().registerHistogram
<Kind
>("api::TERM"),
5377 void Solver::printStatisticsSafe(int fd
) const
5379 d_slv
->printStatisticsSafe(fd
);
5382 /* Helpers for mkTerm checks. */
5383 /* .......................................................................... */
5385 void Solver::checkMkTerm(Kind kind
, uint32_t nchildren
) const
5387 CVC5_API_KIND_CHECK(kind
);
5388 Assert(isDefinedIntKind(extToIntKind(kind
)));
5389 const cvc5::kind::MetaKind mk
= kind::metaKindOf(extToIntKind(kind
));
5390 CVC5_API_KIND_CHECK_EXPECTED(
5391 mk
== kind::metakind::PARAMETERIZED
|| mk
== kind::metakind::OPERATOR
,
5393 << "Only operator-style terms are created with mkTerm(), "
5394 "to create variables, constants and values see mkVar(), mkConst() "
5395 "and the respective theory-specific functions to create values, "
5396 "e.g., mkBitVector().";
5397 CVC5_API_KIND_CHECK_EXPECTED(
5398 nchildren
>= minArity(kind
) && nchildren
<= maxArity(kind
), kind
)
5399 << "Terms with kind " << kindToString(kind
) << " must have at least "
5400 << minArity(kind
) << " children and at most " << maxArity(kind
)
5401 << " children (the one under construction has " << nchildren
<< ")";
5404 /* Sorts Handling */
5405 /* -------------------------------------------------------------------------- */
5407 Sort
Solver::getNullSort(void) const
5409 CVC5_API_TRY_CATCH_BEGIN
;
5410 //////// all checks before this line
5411 return Sort(this, TypeNode());
5413 CVC5_API_TRY_CATCH_END
;
5416 Sort
Solver::getBooleanSort(void) const
5418 CVC5_API_TRY_CATCH_BEGIN
;
5419 //////// all checks before this line
5420 return Sort(this, getNodeManager()->booleanType());
5422 CVC5_API_TRY_CATCH_END
;
5425 Sort
Solver::getIntegerSort(void) const
5427 CVC5_API_TRY_CATCH_BEGIN
;
5428 //////// all checks before this line
5429 return Sort(this, getNodeManager()->integerType());
5431 CVC5_API_TRY_CATCH_END
;
5434 Sort
Solver::getRealSort(void) const
5436 CVC5_API_TRY_CATCH_BEGIN
;
5437 //////// all checks before this line
5438 return Sort(this, getNodeManager()->realType());
5440 CVC5_API_TRY_CATCH_END
;
5443 Sort
Solver::getRegExpSort(void) const
5445 CVC5_API_TRY_CATCH_BEGIN
;
5446 //////// all checks before this line
5447 return Sort(this, getNodeManager()->regExpType());
5449 CVC5_API_TRY_CATCH_END
;
5452 Sort
Solver::getStringSort(void) const
5454 CVC5_API_TRY_CATCH_BEGIN
;
5455 //////// all checks before this line
5456 return Sort(this, getNodeManager()->stringType());
5458 CVC5_API_TRY_CATCH_END
;
5461 Sort
Solver::getRoundingModeSort(void) const
5463 CVC5_API_TRY_CATCH_BEGIN
;
5464 //////// all checks before this line
5465 return Sort(this, getNodeManager()->roundingModeType());
5467 CVC5_API_TRY_CATCH_END
;
5470 /* Create sorts ------------------------------------------------------- */
5472 Sort
Solver::mkArraySort(const Sort
& indexSort
, const Sort
& elemSort
) const
5474 CVC5_API_TRY_CATCH_BEGIN
;
5475 CVC5_API_SOLVER_CHECK_SORT(indexSort
);
5476 CVC5_API_SOLVER_CHECK_SORT(elemSort
);
5477 //////// all checks before this line
5479 this, getNodeManager()->mkArrayType(*indexSort
.d_type
, *elemSort
.d_type
));
5481 CVC5_API_TRY_CATCH_END
;
5484 Sort
Solver::mkBitVectorSort(uint32_t size
) const
5486 CVC5_API_TRY_CATCH_BEGIN
;
5487 CVC5_API_ARG_CHECK_EXPECTED(size
> 0, size
) << "size > 0";
5488 //////// all checks before this line
5489 return Sort(this, getNodeManager()->mkBitVectorType(size
));
5491 CVC5_API_TRY_CATCH_END
;
5494 Sort
Solver::mkFloatingPointSort(uint32_t exp
, uint32_t sig
) const
5496 CVC5_API_TRY_CATCH_BEGIN
;
5497 CVC5_API_ARG_CHECK_EXPECTED(exp
> 0, exp
) << "exponent size > 0";
5498 CVC5_API_ARG_CHECK_EXPECTED(sig
> 0, sig
) << "significand size > 0";
5499 //////// all checks before this line
5500 return Sort(this, getNodeManager()->mkFloatingPointType(exp
, sig
));
5502 CVC5_API_TRY_CATCH_END
;
5505 Sort
Solver::mkDatatypeSort(const DatatypeDecl
& dtypedecl
) const
5507 CVC5_API_TRY_CATCH_BEGIN
;
5508 CVC5_API_SOLVER_CHECK_DTDECL(dtypedecl
);
5509 //////// all checks before this line
5510 return Sort(this, getNodeManager()->mkDatatypeType(*dtypedecl
.d_dtype
));
5512 CVC5_API_TRY_CATCH_END
;
5515 std::vector
<Sort
> Solver::mkDatatypeSorts(
5516 const std::vector
<DatatypeDecl
>& dtypedecls
) const
5518 CVC5_API_SOLVER_CHECK_DTDECLS(dtypedecls
);
5519 CVC5_API_TRY_CATCH_BEGIN
;
5520 //////// all checks before this line
5521 return mkDatatypeSortsInternal(dtypedecls
, {});
5523 CVC5_API_TRY_CATCH_END
;
5526 std::vector
<Sort
> Solver::mkDatatypeSorts(
5527 const std::vector
<DatatypeDecl
>& dtypedecls
,
5528 const std::set
<Sort
>& unresolvedSorts
) const
5530 CVC5_API_TRY_CATCH_BEGIN
;
5531 CVC5_API_SOLVER_CHECK_DTDECLS(dtypedecls
);
5532 CVC5_API_SOLVER_CHECK_SORTS(unresolvedSorts
);
5533 //////// all checks before this line
5534 return mkDatatypeSortsInternal(dtypedecls
, unresolvedSorts
);
5536 CVC5_API_TRY_CATCH_END
;
5539 Sort
Solver::mkFunctionSort(const Sort
& domain
, const Sort
& codomain
) const
5541 CVC5_API_TRY_CATCH_BEGIN
;
5542 CVC5_API_SOLVER_CHECK_DOMAIN_SORT(domain
);
5543 CVC5_API_SOLVER_CHECK_CODOMAIN_SORT(codomain
);
5544 //////// all checks before this line
5546 this, getNodeManager()->mkFunctionType(*domain
.d_type
, *codomain
.d_type
));
5548 CVC5_API_TRY_CATCH_END
;
5551 Sort
Solver::mkFunctionSort(const std::vector
<Sort
>& sorts
,
5552 const Sort
& codomain
) const
5554 CVC5_API_TRY_CATCH_BEGIN
;
5555 CVC5_API_ARG_SIZE_CHECK_EXPECTED(sorts
.size() >= 1, sorts
)
5556 << "at least one parameter sort for function sort";
5557 CVC5_API_SOLVER_CHECK_DOMAIN_SORTS(sorts
);
5558 CVC5_API_SOLVER_CHECK_CODOMAIN_SORT(codomain
);
5559 //////// all checks before this line
5560 std::vector
<TypeNode
> argTypes
= Sort::sortVectorToTypeNodes(sorts
);
5562 getNodeManager()->mkFunctionType(argTypes
, *codomain
.d_type
));
5564 CVC5_API_TRY_CATCH_END
;
5567 Sort
Solver::mkParamSort(const std::string
& symbol
) const
5569 CVC5_API_TRY_CATCH_BEGIN
;
5570 //////// all checks before this line
5573 getNodeManager()->mkSort(symbol
, NodeManager::SORT_FLAG_PLACEHOLDER
));
5575 CVC5_API_TRY_CATCH_END
;
5578 Sort
Solver::mkPredicateSort(const std::vector
<Sort
>& sorts
) const
5580 CVC5_API_TRY_CATCH_BEGIN
;
5581 CVC5_API_ARG_SIZE_CHECK_EXPECTED(sorts
.size() >= 1, sorts
)
5582 << "at least one parameter sort for predicate sort";
5583 CVC5_API_SOLVER_CHECK_DOMAIN_SORTS(sorts
);
5584 //////// all checks before this line
5587 getNodeManager()->mkPredicateType(Sort::sortVectorToTypeNodes(sorts
)));
5589 CVC5_API_TRY_CATCH_END
;
5592 Sort
Solver::mkRecordSort(
5593 const std::vector
<std::pair
<std::string
, Sort
>>& fields
) const
5595 CVC5_API_TRY_CATCH_BEGIN
;
5596 std::vector
<std::pair
<std::string
, TypeNode
>> f
;
5597 for (size_t i
= 0, size
= fields
.size(); i
< size
; ++i
)
5599 const auto& p
= fields
[i
];
5600 CVC5_API_ARG_AT_INDEX_CHECK_EXPECTED(!p
.second
.isNull(), "sort", fields
, i
)
5602 CVC5_API_ARG_AT_INDEX_CHECK_EXPECTED(
5603 this == p
.second
.d_solver
, "sort", fields
, i
)
5604 << "sort associated with this solver object";
5605 f
.emplace_back(p
.first
, *p
.second
.d_type
);
5607 //////// all checks before this line
5608 return Sort(this, getNodeManager()->mkRecordType(f
));
5610 CVC5_API_TRY_CATCH_END
;
5613 Sort
Solver::mkSetSort(const Sort
& elemSort
) const
5615 CVC5_API_TRY_CATCH_BEGIN
;
5616 CVC5_API_SOLVER_CHECK_SORT(elemSort
);
5617 //////// all checks before this line
5618 return Sort(this, getNodeManager()->mkSetType(*elemSort
.d_type
));
5620 CVC5_API_TRY_CATCH_END
;
5623 Sort
Solver::mkBagSort(const Sort
& elemSort
) const
5625 CVC5_API_TRY_CATCH_BEGIN
;
5626 CVC5_API_SOLVER_CHECK_SORT(elemSort
);
5627 //////// all checks before this line
5628 return Sort(this, getNodeManager()->mkBagType(*elemSort
.d_type
));
5630 CVC5_API_TRY_CATCH_END
;
5633 Sort
Solver::mkSequenceSort(const Sort
& elemSort
) const
5635 CVC5_API_TRY_CATCH_BEGIN
;
5636 CVC5_API_SOLVER_CHECK_SORT(elemSort
);
5637 //////// all checks before this line
5638 return Sort(this, getNodeManager()->mkSequenceType(*elemSort
.d_type
));
5640 CVC5_API_TRY_CATCH_END
;
5643 Sort
Solver::mkUninterpretedSort(const std::string
& symbol
) const
5645 CVC5_API_TRY_CATCH_BEGIN
;
5646 //////// all checks before this line
5647 return Sort(this, getNodeManager()->mkSort(symbol
));
5649 CVC5_API_TRY_CATCH_END
;
5652 Sort
Solver::mkSortConstructorSort(const std::string
& symbol
,
5655 CVC5_API_TRY_CATCH_BEGIN
;
5656 CVC5_API_ARG_CHECK_EXPECTED(arity
> 0, arity
) << "an arity > 0";
5657 //////// all checks before this line
5658 return Sort(this, getNodeManager()->mkSortConstructor(symbol
, arity
));
5660 CVC5_API_TRY_CATCH_END
;
5663 Sort
Solver::mkTupleSort(const std::vector
<Sort
>& sorts
) const
5665 CVC5_API_TRY_CATCH_BEGIN
;
5666 CVC5_API_SOLVER_CHECK_SORTS_NOT_FUNCTION_LIKE(sorts
);
5667 //////// all checks before this line
5668 return mkTupleSortHelper(sorts
);
5670 CVC5_API_TRY_CATCH_END
;
5674 /* -------------------------------------------------------------------------- */
5676 Term
Solver::mkTrue(void) const
5678 CVC5_API_TRY_CATCH_BEGIN
;
5679 //////// all checks before this line
5680 return Term(this, d_nodeMgr
->mkConst
<bool>(true));
5682 CVC5_API_TRY_CATCH_END
;
5685 Term
Solver::mkFalse(void) const
5687 CVC5_API_TRY_CATCH_BEGIN
;
5688 //////// all checks before this line
5689 return Term(this, d_nodeMgr
->mkConst
<bool>(false));
5691 CVC5_API_TRY_CATCH_END
;
5694 Term
Solver::mkBoolean(bool val
) const
5696 CVC5_API_TRY_CATCH_BEGIN
;
5697 //////// all checks before this line
5698 return Term(this, d_nodeMgr
->mkConst
<bool>(val
));
5700 CVC5_API_TRY_CATCH_END
;
5703 Term
Solver::mkPi() const
5705 CVC5_API_TRY_CATCH_BEGIN
;
5706 //////// all checks before this line
5708 d_nodeMgr
->mkNullaryOperator(d_nodeMgr
->realType(), cvc5::kind::PI
);
5709 (void)res
.getType(true); /* kick off type checking */
5710 return Term(this, res
);
5712 CVC5_API_TRY_CATCH_END
;
5715 Term
Solver::mkInteger(const std::string
& s
) const
5717 CVC5_API_TRY_CATCH_BEGIN
;
5718 CVC5_API_ARG_CHECK_EXPECTED(isValidInteger(s
), s
) << " an integer ";
5719 Term integer
= mkRealFromStrHelper(s
);
5720 CVC5_API_ARG_CHECK_EXPECTED(integer
.getSort() == getIntegerSort(), s
)
5721 << " a string representing an integer";
5722 //////// all checks before this line
5725 CVC5_API_TRY_CATCH_END
;
5728 Term
Solver::mkInteger(int64_t val
) const
5730 CVC5_API_TRY_CATCH_BEGIN
;
5731 //////// all checks before this line
5732 Term integer
= mkValHelper
<cvc5::Rational
>(cvc5::Rational(val
));
5733 Assert(integer
.getSort() == getIntegerSort());
5736 CVC5_API_TRY_CATCH_END
;
5739 Term
Solver::mkReal(const std::string
& s
) const
5741 CVC5_API_TRY_CATCH_BEGIN
;
5742 /* CLN and GMP handle this case differently, CLN interprets it as 0, GMP
5743 * throws an std::invalid_argument exception. For consistency, we treat it
5745 CVC5_API_ARG_CHECK_EXPECTED(s
!= ".", s
)
5746 << "a string representing a real or rational value.";
5747 //////// all checks before this line
5748 Term rational
= mkRealFromStrHelper(s
);
5749 return ensureRealSort(rational
);
5751 CVC5_API_TRY_CATCH_END
;
5754 Term
Solver::mkReal(int64_t val
) const
5756 CVC5_API_TRY_CATCH_BEGIN
;
5757 //////// all checks before this line
5758 Term rational
= mkValHelper
<cvc5::Rational
>(cvc5::Rational(val
));
5759 return ensureRealSort(rational
);
5761 CVC5_API_TRY_CATCH_END
;
5764 Term
Solver::mkReal(int64_t num
, int64_t den
) const
5766 CVC5_API_TRY_CATCH_BEGIN
;
5767 //////// all checks before this line
5768 Term rational
= mkValHelper
<cvc5::Rational
>(cvc5::Rational(num
, den
));
5769 return ensureRealSort(rational
);
5771 CVC5_API_TRY_CATCH_END
;
5774 Term
Solver::mkRegexpEmpty() const
5776 CVC5_API_TRY_CATCH_BEGIN
;
5777 //////// all checks before this line
5779 d_nodeMgr
->mkNode(cvc5::kind::REGEXP_EMPTY
, std::vector
<cvc5::Node
>());
5780 (void)res
.getType(true); /* kick off type checking */
5781 return Term(this, res
);
5783 CVC5_API_TRY_CATCH_END
;
5786 Term
Solver::mkRegexpSigma() const
5788 CVC5_API_TRY_CATCH_BEGIN
;
5789 //////// all checks before this line
5791 d_nodeMgr
->mkNode(cvc5::kind::REGEXP_SIGMA
, std::vector
<cvc5::Node
>());
5792 (void)res
.getType(true); /* kick off type checking */
5793 return Term(this, res
);
5795 CVC5_API_TRY_CATCH_END
;
5798 Term
Solver::mkEmptySet(const Sort
& sort
) const
5800 CVC5_API_TRY_CATCH_BEGIN
;
5801 CVC5_API_ARG_CHECK_EXPECTED(sort
.isNull() || sort
.isSet(), sort
)
5802 << "null sort or set sort";
5803 CVC5_API_ARG_CHECK_EXPECTED(sort
.isNull() || this == sort
.d_solver
, sort
)
5804 << "set sort associated with this solver object";
5805 //////// all checks before this line
5806 return mkValHelper
<cvc5::EmptySet
>(cvc5::EmptySet(*sort
.d_type
));
5808 CVC5_API_TRY_CATCH_END
;
5811 Term
Solver::mkEmptyBag(const Sort
& sort
) const
5813 CVC5_API_TRY_CATCH_BEGIN
;
5814 CVC5_API_ARG_CHECK_EXPECTED(sort
.isNull() || sort
.isBag(), sort
)
5815 << "null sort or bag sort";
5816 CVC5_API_ARG_CHECK_EXPECTED(sort
.isNull() || this == sort
.d_solver
, sort
)
5817 << "bag sort associated with this solver object";
5818 //////// all checks before this line
5819 return mkValHelper
<cvc5::EmptyBag
>(cvc5::EmptyBag(*sort
.d_type
));
5821 CVC5_API_TRY_CATCH_END
;
5824 Term
Solver::mkSepEmp() const
5826 CVC5_API_TRY_CATCH_BEGIN
;
5827 //////// all checks before this line
5828 Node res
= getNodeManager()->mkNullaryOperator(d_nodeMgr
->booleanType(),
5829 cvc5::Kind::SEP_EMP
);
5830 (void)res
.getType(true); /* kick off type checking */
5831 return Term(this, res
);
5833 CVC5_API_TRY_CATCH_END
;
5836 Term
Solver::mkSepNil(const Sort
& sort
) const
5838 CVC5_API_TRY_CATCH_BEGIN
;
5839 CVC5_API_SOLVER_CHECK_SORT(sort
);
5840 //////// all checks before this line
5842 getNodeManager()->mkNullaryOperator(*sort
.d_type
, cvc5::kind::SEP_NIL
);
5843 (void)res
.getType(true); /* kick off type checking */
5844 return Term(this, res
);
5846 CVC5_API_TRY_CATCH_END
;
5849 Term
Solver::mkString(const std::string
& s
, bool useEscSequences
) const
5851 CVC5_API_TRY_CATCH_BEGIN
;
5852 //////// all checks before this line
5853 return mkValHelper
<cvc5::String
>(cvc5::String(s
, useEscSequences
));
5855 CVC5_API_TRY_CATCH_END
;
5858 Term
Solver::mkString(const std::wstring
& s
) const
5860 CVC5_API_TRY_CATCH_BEGIN
;
5861 //////// all checks before this line
5862 return mkValHelper
<cvc5::String
>(cvc5::String(s
));
5864 CVC5_API_TRY_CATCH_END
;
5867 Term
Solver::mkEmptySequence(const Sort
& sort
) const
5869 CVC5_API_TRY_CATCH_BEGIN
;
5870 CVC5_API_SOLVER_CHECK_SORT(sort
);
5871 //////// all checks before this line
5872 std::vector
<Node
> seq
;
5873 Node res
= d_nodeMgr
->mkConst(Sequence(*sort
.d_type
, seq
));
5874 return Term(this, res
);
5876 CVC5_API_TRY_CATCH_END
;
5879 Term
Solver::mkUniverseSet(const Sort
& sort
) const
5881 CVC5_API_TRY_CATCH_BEGIN
;
5882 CVC5_API_SOLVER_CHECK_SORT(sort
);
5883 //////// all checks before this line
5885 Node res
= getNodeManager()->mkNullaryOperator(*sort
.d_type
,
5886 cvc5::kind::UNIVERSE_SET
);
5887 // TODO(#2771): Reenable?
5888 // (void)res->getType(true); /* kick off type checking */
5889 return Term(this, res
);
5891 CVC5_API_TRY_CATCH_END
;
5894 Term
Solver::mkBitVector(uint32_t size
, uint64_t val
) const
5896 CVC5_API_TRY_CATCH_BEGIN
;
5897 //////// all checks before this line
5898 return mkBVFromIntHelper(size
, val
);
5900 CVC5_API_TRY_CATCH_END
;
5903 Term
Solver::mkBitVector(uint32_t size
,
5904 const std::string
& s
,
5905 uint32_t base
) const
5907 CVC5_API_TRY_CATCH_BEGIN
;
5908 //////// all checks before this line
5909 return mkBVFromStrHelper(size
, s
, base
);
5911 CVC5_API_TRY_CATCH_END
;
5914 Term
Solver::mkConstArray(const Sort
& sort
, const Term
& val
) const
5916 CVC5_API_TRY_CATCH_BEGIN
;
5917 CVC5_API_SOLVER_CHECK_SORT(sort
);
5918 CVC5_API_SOLVER_CHECK_TERM(val
);
5919 CVC5_API_ARG_CHECK_EXPECTED(sort
.isArray(), sort
) << "an array sort";
5920 CVC5_API_CHECK(val
.getSort().isSubsortOf(sort
.getArrayElementSort()))
5921 << "Value does not match element sort";
5922 //////// all checks before this line
5924 // handle the special case of (CAST_TO_REAL n) where n is an integer
5925 Node n
= *val
.d_node
;
5926 if (val
.isCastedReal())
5928 // this is safe because the constant array stores its type
5932 mkValHelper
<cvc5::ArrayStoreAll
>(cvc5::ArrayStoreAll(*sort
.d_type
, n
));
5935 CVC5_API_TRY_CATCH_END
;
5938 Term
Solver::mkPosInf(uint32_t exp
, uint32_t sig
) const
5940 CVC5_API_TRY_CATCH_BEGIN
;
5941 //////// all checks before this line
5942 return mkValHelper
<cvc5::FloatingPoint
>(
5943 FloatingPoint::makeInf(FloatingPointSize(exp
, sig
), false));
5945 CVC5_API_TRY_CATCH_END
;
5948 Term
Solver::mkNegInf(uint32_t exp
, uint32_t sig
) const
5950 CVC5_API_TRY_CATCH_BEGIN
;
5951 //////// all checks before this line
5952 return mkValHelper
<cvc5::FloatingPoint
>(
5953 FloatingPoint::makeInf(FloatingPointSize(exp
, sig
), true));
5955 CVC5_API_TRY_CATCH_END
;
5958 Term
Solver::mkNaN(uint32_t exp
, uint32_t sig
) const
5960 CVC5_API_TRY_CATCH_BEGIN
;
5961 //////// all checks before this line
5962 return mkValHelper
<cvc5::FloatingPoint
>(
5963 FloatingPoint::makeNaN(FloatingPointSize(exp
, sig
)));
5965 CVC5_API_TRY_CATCH_END
;
5968 Term
Solver::mkPosZero(uint32_t exp
, uint32_t sig
) const
5970 CVC5_API_TRY_CATCH_BEGIN
;
5971 //////// all checks before this line
5972 return mkValHelper
<cvc5::FloatingPoint
>(
5973 FloatingPoint::makeZero(FloatingPointSize(exp
, sig
), false));
5975 CVC5_API_TRY_CATCH_END
;
5978 Term
Solver::mkNegZero(uint32_t exp
, uint32_t sig
) const
5980 CVC5_API_TRY_CATCH_BEGIN
;
5981 //////// all checks before this line
5982 return mkValHelper
<cvc5::FloatingPoint
>(
5983 FloatingPoint::makeZero(FloatingPointSize(exp
, sig
), true));
5985 CVC5_API_TRY_CATCH_END
;
5988 Term
Solver::mkRoundingMode(RoundingMode rm
) const
5990 CVC5_API_TRY_CATCH_BEGIN
;
5991 //////// all checks before this line
5992 return mkValHelper
<cvc5::RoundingMode
>(s_rmodes
.at(rm
));
5994 CVC5_API_TRY_CATCH_END
;
5997 Term
Solver::mkUninterpretedConst(const Sort
& sort
, int32_t index
) const
5999 CVC5_API_TRY_CATCH_BEGIN
;
6000 CVC5_API_SOLVER_CHECK_SORT(sort
);
6001 //////// all checks before this line
6002 return mkValHelper
<cvc5::UninterpretedConstant
>(
6003 cvc5::UninterpretedConstant(*sort
.d_type
, index
));
6005 CVC5_API_TRY_CATCH_END
;
6008 Term
Solver::mkAbstractValue(const std::string
& index
) const
6010 CVC5_API_TRY_CATCH_BEGIN
;
6011 CVC5_API_ARG_CHECK_EXPECTED(!index
.empty(), index
) << "a non-empty string";
6013 cvc5::Integer
idx(index
, 10);
6014 CVC5_API_ARG_CHECK_EXPECTED(idx
> 0, index
)
6015 << "a string representing an integer > 0";
6016 //////// all checks before this line
6017 return Term(this, getNodeManager()->mkConst(cvc5::AbstractValue(idx
)));
6018 // do not call getType(), for abstract values, type can not be computed
6019 // until it is substituted away
6021 CVC5_API_TRY_CATCH_END
;
6024 Term
Solver::mkAbstractValue(uint64_t index
) const
6026 CVC5_API_TRY_CATCH_BEGIN
;
6027 CVC5_API_ARG_CHECK_EXPECTED(index
> 0, index
) << "an integer > 0";
6028 //////// all checks before this line
6030 getNodeManager()->mkConst(cvc5::AbstractValue(Integer(index
))));
6031 // do not call getType(), for abstract values, type can not be computed
6032 // until it is substituted away
6034 CVC5_API_TRY_CATCH_END
;
6037 Term
Solver::mkFloatingPoint(uint32_t exp
, uint32_t sig
, Term val
) const
6039 CVC5_API_TRY_CATCH_BEGIN
;
6040 CVC5_API_SOLVER_CHECK_TERM(val
);
6041 CVC5_API_ARG_CHECK_EXPECTED(exp
> 0, exp
) << "a value > 0";
6042 CVC5_API_ARG_CHECK_EXPECTED(sig
> 0, sig
) << "a value > 0";
6043 uint32_t bw
= exp
+ sig
;
6044 CVC5_API_ARG_CHECK_EXPECTED(bw
== val
.d_node
->getType().getBitVectorSize(),
6046 << "a bit-vector constant with bit-width '" << bw
<< "'";
6047 CVC5_API_ARG_CHECK_EXPECTED(
6048 val
.d_node
->getType().isBitVector() && val
.d_node
->isConst(), val
)
6049 << "bit-vector constant";
6050 //////// all checks before this line
6051 return mkValHelper
<cvc5::FloatingPoint
>(
6052 cvc5::FloatingPoint(exp
, sig
, val
.d_node
->getConst
<BitVector
>()));
6054 CVC5_API_TRY_CATCH_END
;
6057 Term
Solver::mkCardinalityConstraint(const Sort
& sort
, uint32_t upperBound
) const
6059 CVC5_API_TRY_CATCH_BEGIN
;
6060 CVC5_API_SOLVER_CHECK_SORT(sort
);
6061 CVC5_API_ARG_CHECK_EXPECTED(sort
.isUninterpretedSort(), sort
)
6062 << "an uninterpreted sort";
6063 CVC5_API_ARG_CHECK_EXPECTED(upperBound
> 0, upperBound
) << "a value > 0";
6064 //////// all checks before this line
6066 d_nodeMgr
->mkConst(cvc5::CardinalityConstraint(*sort
.d_type
, upperBound
));
6067 Node cc
= d_nodeMgr
->mkNode(cvc5::Kind::CARDINALITY_CONSTRAINT
, cco
);
6068 return Term(this, cc
);
6070 CVC5_API_TRY_CATCH_END
;
6073 /* Create constants */
6074 /* -------------------------------------------------------------------------- */
6076 Term
Solver::mkConst(const Sort
& sort
, const std::string
& symbol
) const
6078 CVC5_API_TRY_CATCH_BEGIN
;
6079 CVC5_API_SOLVER_CHECK_SORT(sort
);
6080 //////// all checks before this line
6081 Node res
= d_nodeMgr
->mkVar(symbol
, *sort
.d_type
);
6082 (void)res
.getType(true); /* kick off type checking */
6083 increment_vars_consts_stats(sort
, false);
6084 return Term(this, res
);
6086 CVC5_API_TRY_CATCH_END
;
6089 Term
Solver::mkConst(const Sort
& sort
) const
6091 CVC5_API_TRY_CATCH_BEGIN
;
6092 CVC5_API_SOLVER_CHECK_SORT(sort
);
6093 //////// all checks before this line
6094 Node res
= d_nodeMgr
->mkVar(*sort
.d_type
);
6095 (void)res
.getType(true); /* kick off type checking */
6096 increment_vars_consts_stats(sort
, false);
6097 return Term(this, res
);
6099 CVC5_API_TRY_CATCH_END
;
6102 /* Create variables */
6103 /* -------------------------------------------------------------------------- */
6105 Term
Solver::mkVar(const Sort
& sort
, const std::string
& symbol
) const
6107 CVC5_API_TRY_CATCH_BEGIN
;
6108 CVC5_API_SOLVER_CHECK_SORT(sort
);
6109 //////// all checks before this line
6110 Node res
= symbol
.empty() ? d_nodeMgr
->mkBoundVar(*sort
.d_type
)
6111 : d_nodeMgr
->mkBoundVar(symbol
, *sort
.d_type
);
6112 (void)res
.getType(true); /* kick off type checking */
6113 increment_vars_consts_stats(sort
, true);
6114 return Term(this, res
);
6116 CVC5_API_TRY_CATCH_END
;
6119 /* Create datatype constructor declarations */
6120 /* -------------------------------------------------------------------------- */
6122 DatatypeConstructorDecl
Solver::mkDatatypeConstructorDecl(
6123 const std::string
& name
)
6125 CVC5_API_TRY_CATCH_BEGIN
;
6126 //////// all checks before this line
6127 return DatatypeConstructorDecl(this, name
);
6129 CVC5_API_TRY_CATCH_END
;
6132 /* Create datatype declarations */
6133 /* -------------------------------------------------------------------------- */
6135 DatatypeDecl
Solver::mkDatatypeDecl(const std::string
& name
, bool isCoDatatype
)
6137 CVC5_API_TRY_CATCH_BEGIN
;
6138 //////// all checks before this line
6139 return DatatypeDecl(this, name
, isCoDatatype
);
6141 CVC5_API_TRY_CATCH_END
;
6144 DatatypeDecl
Solver::mkDatatypeDecl(const std::string
& name
,
6148 CVC5_API_TRY_CATCH_BEGIN
;
6149 CVC5_API_SOLVER_CHECK_SORT(param
);
6150 //////// all checks before this line
6151 return DatatypeDecl(this, name
, param
, isCoDatatype
);
6153 CVC5_API_TRY_CATCH_END
;
6156 DatatypeDecl
Solver::mkDatatypeDecl(const std::string
& name
,
6157 const std::vector
<Sort
>& params
,
6160 CVC5_API_TRY_CATCH_BEGIN
;
6161 CVC5_API_SOLVER_CHECK_SORTS(params
);
6162 //////// all checks before this line
6163 return DatatypeDecl(this, name
, params
, isCoDatatype
);
6165 CVC5_API_TRY_CATCH_END
;
6169 /* -------------------------------------------------------------------------- */
6171 Term
Solver::mkTerm(Kind kind
) const
6173 CVC5_API_TRY_CATCH_BEGIN
;
6174 CVC5_API_KIND_CHECK(kind
);
6175 //////// all checks before this line
6176 return mkTermFromKind(kind
);
6178 CVC5_API_TRY_CATCH_END
;
6181 Term
Solver::mkTerm(Kind kind
, const Term
& child
) const
6183 CVC5_API_TRY_CATCH_BEGIN
;
6184 CVC5_API_KIND_CHECK(kind
);
6185 CVC5_API_SOLVER_CHECK_TERM(child
);
6186 //////// all checks before this line
6187 return mkTermHelper(kind
, std::vector
<Term
>{child
});
6189 CVC5_API_TRY_CATCH_END
;
6192 Term
Solver::mkTerm(Kind kind
, const Term
& child1
, const Term
& child2
) const
6194 CVC5_API_TRY_CATCH_BEGIN
;
6195 CVC5_API_KIND_CHECK(kind
);
6196 CVC5_API_SOLVER_CHECK_TERM(child1
);
6197 CVC5_API_SOLVER_CHECK_TERM(child2
);
6198 //////// all checks before this line
6199 return mkTermHelper(kind
, std::vector
<Term
>{child1
, child2
});
6201 CVC5_API_TRY_CATCH_END
;
6204 Term
Solver::mkTerm(Kind kind
,
6207 const Term
& child3
) const
6209 CVC5_API_TRY_CATCH_BEGIN
;
6210 CVC5_API_KIND_CHECK(kind
);
6211 CVC5_API_SOLVER_CHECK_TERM(child1
);
6212 CVC5_API_SOLVER_CHECK_TERM(child2
);
6213 CVC5_API_SOLVER_CHECK_TERM(child3
);
6214 //////// all checks before this line
6215 // need to use internal term call to check e.g. associative construction
6216 return mkTermHelper(kind
, std::vector
<Term
>{child1
, child2
, child3
});
6218 CVC5_API_TRY_CATCH_END
;
6221 Term
Solver::mkTerm(Kind kind
, const std::vector
<Term
>& children
) const
6223 CVC5_API_TRY_CATCH_BEGIN
;
6224 CVC5_API_KIND_CHECK(kind
);
6225 CVC5_API_SOLVER_CHECK_TERMS(children
);
6226 //////// all checks before this line
6227 return mkTermHelper(kind
, children
);
6229 CVC5_API_TRY_CATCH_END
;
6232 Term
Solver::mkTerm(const Op
& op
) const
6234 CVC5_API_TRY_CATCH_BEGIN
;
6235 CVC5_API_SOLVER_CHECK_OP(op
);
6236 checkMkTerm(op
.d_kind
, 0);
6237 //////// all checks before this line
6239 if (!op
.isIndexedHelper())
6241 return mkTermFromKind(op
.d_kind
);
6244 const cvc5::Kind int_kind
= extToIntKind(op
.d_kind
);
6245 Term res
= Term(this, getNodeManager()->mkNode(int_kind
, *op
.d_node
));
6247 (void)res
.d_node
->getType(true); /* kick off type checking */
6250 CVC5_API_TRY_CATCH_END
;
6253 Term
Solver::mkTerm(const Op
& op
, const Term
& child
) const
6255 CVC5_API_TRY_CATCH_BEGIN
;
6256 CVC5_API_SOLVER_CHECK_OP(op
);
6257 CVC5_API_SOLVER_CHECK_TERM(child
);
6258 //////// all checks before this line
6259 return mkTermHelper(op
, std::vector
<Term
>{child
});
6261 CVC5_API_TRY_CATCH_END
;
6264 Term
Solver::mkTerm(const Op
& op
, const Term
& child1
, const Term
& child2
) const
6266 CVC5_API_TRY_CATCH_BEGIN
;
6267 CVC5_API_SOLVER_CHECK_OP(op
);
6268 CVC5_API_SOLVER_CHECK_TERM(child1
);
6269 CVC5_API_SOLVER_CHECK_TERM(child2
);
6270 //////// all checks before this line
6271 return mkTermHelper(op
, std::vector
<Term
>{child1
, child2
});
6273 CVC5_API_TRY_CATCH_END
;
6276 Term
Solver::mkTerm(const Op
& op
,
6279 const Term
& child3
) const
6281 CVC5_API_TRY_CATCH_BEGIN
;
6282 CVC5_API_SOLVER_CHECK_OP(op
);
6283 CVC5_API_SOLVER_CHECK_TERM(child1
);
6284 CVC5_API_SOLVER_CHECK_TERM(child2
);
6285 CVC5_API_SOLVER_CHECK_TERM(child3
);
6286 //////// all checks before this line
6287 return mkTermHelper(op
, std::vector
<Term
>{child1
, child2
, child3
});
6289 CVC5_API_TRY_CATCH_END
;
6292 Term
Solver::mkTerm(const Op
& op
, const std::vector
<Term
>& children
) const
6294 CVC5_API_TRY_CATCH_BEGIN
;
6295 CVC5_API_SOLVER_CHECK_OP(op
);
6296 CVC5_API_SOLVER_CHECK_TERMS(children
);
6297 //////// all checks before this line
6298 return mkTermHelper(op
, children
);
6300 CVC5_API_TRY_CATCH_END
;
6303 Term
Solver::mkTuple(const std::vector
<Sort
>& sorts
,
6304 const std::vector
<Term
>& terms
) const
6306 CVC5_API_TRY_CATCH_BEGIN
;
6307 CVC5_API_CHECK(sorts
.size() == terms
.size())
6308 << "Expected the same number of sorts and elements";
6309 CVC5_API_SOLVER_CHECK_SORTS(sorts
);
6310 CVC5_API_SOLVER_CHECK_TERMS(terms
);
6311 //////// all checks before this line
6312 std::vector
<cvc5::Node
> args
;
6313 for (size_t i
= 0, size
= sorts
.size(); i
< size
; i
++)
6315 args
.push_back(*(ensureTermSort(terms
[i
], sorts
[i
])).d_node
);
6318 Sort s
= mkTupleSortHelper(sorts
);
6319 Datatype dt
= s
.getDatatype();
6320 NodeBuilder
nb(extToIntKind(APPLY_CONSTRUCTOR
));
6321 nb
<< *dt
[0].getConstructorTerm().d_node
;
6323 Node res
= nb
.constructNode();
6324 (void)res
.getType(true); /* kick off type checking */
6325 return Term(this, res
);
6327 CVC5_API_TRY_CATCH_END
;
6330 /* Create operators */
6331 /* -------------------------------------------------------------------------- */
6333 Op
Solver::mkOp(Kind kind
) const
6335 CVC5_API_TRY_CATCH_BEGIN
;
6336 CVC5_API_KIND_CHECK(kind
);
6337 CVC5_API_CHECK(s_indexed_kinds
.find(kind
) == s_indexed_kinds
.end())
6338 << "Expected a kind for a non-indexed operator.";
6339 //////// all checks before this line
6340 return Op(this, kind
);
6342 CVC5_API_TRY_CATCH_END
6345 Op
Solver::mkOp(Kind kind
, const std::string
& arg
) const
6347 CVC5_API_TRY_CATCH_BEGIN
;
6348 CVC5_API_KIND_CHECK(kind
);
6349 CVC5_API_KIND_CHECK_EXPECTED((kind
== DIVISIBLE
), kind
) << "DIVISIBLE";
6350 //////// all checks before this line
6352 /* CLN and GMP handle this case differently, CLN interprets it as 0, GMP
6353 * throws an std::invalid_argument exception. For consistency, we treat it
6355 CVC5_API_ARG_CHECK_EXPECTED(arg
!= ".", arg
)
6356 << "a string representing an integer, real or rational value.";
6359 *mkValHelper
<cvc5::Divisible
>(cvc5::Divisible(cvc5::Integer(arg
)))
6363 CVC5_API_TRY_CATCH_END
;
6366 Op
Solver::mkOp(Kind kind
, uint32_t arg
) const
6368 CVC5_API_TRY_CATCH_BEGIN
;
6369 CVC5_API_KIND_CHECK(kind
);
6370 //////// all checks before this line
6377 *mkValHelper
<cvc5::Divisible
>(cvc5::Divisible(arg
)).d_node
);
6379 case BITVECTOR_REPEAT
:
6382 *mkValHelper
<cvc5::BitVectorRepeat
>(cvc5::BitVectorRepeat(arg
))
6385 case BITVECTOR_ZERO_EXTEND
:
6388 *mkValHelper
<cvc5::BitVectorZeroExtend
>(
6389 cvc5::BitVectorZeroExtend(arg
))
6392 case BITVECTOR_SIGN_EXTEND
:
6395 *mkValHelper
<cvc5::BitVectorSignExtend
>(
6396 cvc5::BitVectorSignExtend(arg
))
6399 case BITVECTOR_ROTATE_LEFT
:
6402 *mkValHelper
<cvc5::BitVectorRotateLeft
>(
6403 cvc5::BitVectorRotateLeft(arg
))
6406 case BITVECTOR_ROTATE_RIGHT
:
6409 *mkValHelper
<cvc5::BitVectorRotateRight
>(
6410 cvc5::BitVectorRotateRight(arg
))
6413 case INT_TO_BITVECTOR
:
6417 *mkValHelper
<cvc5::IntToBitVector
>(cvc5::IntToBitVector(arg
)).d_node
);
6421 Op(this, kind
, *mkValHelper
<cvc5::IntAnd
>(cvc5::IntAnd(arg
)).d_node
);
6423 case FLOATINGPOINT_TO_UBV
:
6427 *mkValHelper
<cvc5::FloatingPointToUBV
>(cvc5::FloatingPointToUBV(arg
))
6430 case FLOATINGPOINT_TO_SBV
:
6434 *mkValHelper
<cvc5::FloatingPointToSBV
>(cvc5::FloatingPointToSBV(arg
))
6441 *mkValHelper
<cvc5::RegExpRepeat
>(cvc5::RegExpRepeat(arg
)).d_node
);
6444 CVC5_API_KIND_CHECK_EXPECTED(false, kind
)
6445 << "operator kind with uint32_t argument";
6447 Assert(!res
.isNull());
6450 CVC5_API_TRY_CATCH_END
;
6453 Op
Solver::mkOp(Kind kind
, uint32_t arg1
, uint32_t arg2
) const
6455 CVC5_API_TRY_CATCH_BEGIN
;
6456 CVC5_API_KIND_CHECK(kind
);
6457 //////// all checks before this line
6462 case BITVECTOR_EXTRACT
:
6465 *mkValHelper
<cvc5::BitVectorExtract
>(
6466 cvc5::BitVectorExtract(arg1
, arg2
))
6469 case FLOATINGPOINT_TO_FP_IEEE_BITVECTOR
:
6472 *mkValHelper
<cvc5::FloatingPointToFPIEEEBitVector
>(
6473 cvc5::FloatingPointToFPIEEEBitVector(arg1
, arg2
))
6476 case FLOATINGPOINT_TO_FP_FLOATINGPOINT
:
6479 *mkValHelper
<cvc5::FloatingPointToFPFloatingPoint
>(
6480 cvc5::FloatingPointToFPFloatingPoint(arg1
, arg2
))
6483 case FLOATINGPOINT_TO_FP_REAL
:
6486 *mkValHelper
<cvc5::FloatingPointToFPReal
>(
6487 cvc5::FloatingPointToFPReal(arg1
, arg2
))
6490 case FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR
:
6493 *mkValHelper
<cvc5::FloatingPointToFPSignedBitVector
>(
6494 cvc5::FloatingPointToFPSignedBitVector(arg1
, arg2
))
6497 case FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR
:
6500 *mkValHelper
<cvc5::FloatingPointToFPUnsignedBitVector
>(
6501 cvc5::FloatingPointToFPUnsignedBitVector(arg1
, arg2
))
6504 case FLOATINGPOINT_TO_FP_GENERIC
:
6507 *mkValHelper
<cvc5::FloatingPointToFPGeneric
>(
6508 cvc5::FloatingPointToFPGeneric(arg1
, arg2
))
6515 *mkValHelper
<cvc5::RegExpLoop
>(cvc5::RegExpLoop(arg1
, arg2
)).d_node
);
6518 CVC5_API_KIND_CHECK_EXPECTED(false, kind
)
6519 << "operator kind with two uint32_t arguments";
6521 Assert(!res
.isNull());
6524 CVC5_API_TRY_CATCH_END
;
6527 Op
Solver::mkOp(Kind kind
, const std::vector
<uint32_t>& args
) const
6529 CVC5_API_TRY_CATCH_BEGIN
;
6530 CVC5_API_KIND_CHECK(kind
);
6531 //////// all checks before this line
6540 *mkValHelper
<cvc5::TupleProjectOp
>(cvc5::TupleProjectOp(args
))
6546 std::string message
= "operator kind with " + std::to_string(args
.size())
6547 + " uint32_t arguments";
6548 CVC5_API_KIND_CHECK_EXPECTED(false, kind
) << message
;
6551 Assert(!res
.isNull());
6554 CVC5_API_TRY_CATCH_END
;
6557 /* Non-SMT-LIB commands */
6558 /* -------------------------------------------------------------------------- */
6560 Term
Solver::simplify(const Term
& term
)
6562 CVC5_API_TRY_CATCH_BEGIN
;
6563 CVC5_API_SOLVER_CHECK_TERM(term
);
6564 //////// all checks before this line
6565 return Term(this, d_slv
->simplify(*term
.d_node
));
6567 CVC5_API_TRY_CATCH_END
;
6570 Result
Solver::checkEntailed(const Term
& term
) const
6572 CVC5_API_TRY_CATCH_BEGIN
;
6573 CVC5_API_CHECK(!d_slv
->isQueryMade()
6574 || d_slv
->getOptions().base
.incrementalSolving
)
6575 << "Cannot make multiple queries unless incremental solving is enabled "
6576 "(try --incremental)";
6577 CVC5_API_SOLVER_CHECK_TERM(term
);
6578 //////// all checks before this line
6579 return d_slv
->checkEntailed(*term
.d_node
);
6581 CVC5_API_TRY_CATCH_END
;
6584 Result
Solver::checkEntailed(const std::vector
<Term
>& terms
) const
6586 CVC5_API_TRY_CATCH_BEGIN
;
6587 CVC5_API_CHECK(!d_slv
->isQueryMade()
6588 || d_slv
->getOptions().base
.incrementalSolving
)
6589 << "Cannot make multiple queries unless incremental solving is enabled "
6590 "(try --incremental)";
6591 CVC5_API_SOLVER_CHECK_TERMS(terms
);
6592 //////// all checks before this line
6593 return d_slv
->checkEntailed(Term::termVectorToNodes(terms
));
6595 CVC5_API_TRY_CATCH_END
;
6598 /* SMT-LIB commands */
6599 /* -------------------------------------------------------------------------- */
6601 void Solver::assertFormula(const Term
& term
) const
6603 CVC5_API_TRY_CATCH_BEGIN
;
6604 CVC5_API_SOLVER_CHECK_TERM(term
);
6605 CVC5_API_SOLVER_CHECK_TERM_WITH_SORT(term
, getBooleanSort());
6606 //////// all checks before this line
6607 d_slv
->assertFormula(*term
.d_node
);
6609 CVC5_API_TRY_CATCH_END
;
6612 Result
Solver::checkSat(void) const
6614 CVC5_API_TRY_CATCH_BEGIN
;
6615 CVC5_API_CHECK(!d_slv
->isQueryMade()
6616 || d_slv
->getOptions().base
.incrementalSolving
)
6617 << "Cannot make multiple queries unless incremental solving is enabled "
6618 "(try --incremental)";
6619 //////// all checks before this line
6620 return d_slv
->checkSat();
6622 CVC5_API_TRY_CATCH_END
;
6625 Result
Solver::checkSatAssuming(const Term
& assumption
) const
6627 CVC5_API_TRY_CATCH_BEGIN
;
6628 CVC5_API_CHECK(!d_slv
->isQueryMade()
6629 || d_slv
->getOptions().base
.incrementalSolving
)
6630 << "Cannot make multiple queries unless incremental solving is enabled "
6631 "(try --incremental)";
6632 CVC5_API_SOLVER_CHECK_TERM_WITH_SORT(assumption
, getBooleanSort());
6633 //////// all checks before this line
6634 return d_slv
->checkSat(*assumption
.d_node
);
6636 CVC5_API_TRY_CATCH_END
;
6639 Result
Solver::checkSatAssuming(const std::vector
<Term
>& assumptions
) const
6641 CVC5_API_TRY_CATCH_BEGIN
;
6642 CVC5_API_CHECK(!d_slv
->isQueryMade() || assumptions
.size() == 0
6643 || d_slv
->getOptions().base
.incrementalSolving
)
6644 << "Cannot make multiple queries unless incremental solving is enabled "
6645 "(try --incremental)";
6646 CVC5_API_SOLVER_CHECK_TERMS_WITH_SORT(assumptions
, getBooleanSort());
6647 //////// all checks before this line
6648 for (const Term
& term
: assumptions
)
6650 CVC5_API_SOLVER_CHECK_TERM(term
);
6652 std::vector
<Node
> eassumptions
= Term::termVectorToNodes(assumptions
);
6653 return d_slv
->checkSat(eassumptions
);
6655 CVC5_API_TRY_CATCH_END
;
6658 Sort
Solver::declareDatatype(
6659 const std::string
& symbol
,
6660 const std::vector
<DatatypeConstructorDecl
>& ctors
) const
6662 CVC5_API_TRY_CATCH_BEGIN
;
6663 CVC5_API_ARG_CHECK_EXPECTED(ctors
.size() > 0, ctors
)
6664 << "a datatype declaration with at least one constructor";
6665 CVC5_API_SOLVER_CHECK_DTCTORDECLS(ctors
);
6666 //////// all checks before this line
6667 DatatypeDecl
dtdecl(this, symbol
);
6668 for (size_t i
= 0, size
= ctors
.size(); i
< size
; i
++)
6670 dtdecl
.addConstructor(ctors
[i
]);
6672 return Sort(this, getNodeManager()->mkDatatypeType(*dtdecl
.d_dtype
));
6674 CVC5_API_TRY_CATCH_END
;
6677 Term
Solver::declareFun(const std::string
& symbol
,
6678 const std::vector
<Sort
>& sorts
,
6679 const Sort
& sort
) const
6681 CVC5_API_TRY_CATCH_BEGIN
;
6682 CVC5_API_SOLVER_CHECK_DOMAIN_SORTS(sorts
);
6683 CVC5_API_SOLVER_CHECK_CODOMAIN_SORT(sort
);
6684 //////// all checks before this line
6686 TypeNode type
= *sort
.d_type
;
6689 std::vector
<TypeNode
> types
= Sort::sortVectorToTypeNodes(sorts
);
6690 type
= getNodeManager()->mkFunctionType(types
, type
);
6692 return Term(this, d_nodeMgr
->mkVar(symbol
, type
));
6694 CVC5_API_TRY_CATCH_END
;
6697 Sort
Solver::declareSort(const std::string
& symbol
, uint32_t arity
) const
6699 CVC5_API_TRY_CATCH_BEGIN
;
6700 //////// all checks before this line
6703 return Sort(this, getNodeManager()->mkSort(symbol
));
6705 return Sort(this, getNodeManager()->mkSortConstructor(symbol
, arity
));
6707 CVC5_API_TRY_CATCH_END
;
6710 Term
Solver::defineFun(const std::string
& symbol
,
6711 const std::vector
<Term
>& bound_vars
,
6716 CVC5_API_TRY_CATCH_BEGIN
;
6717 CVC5_API_SOLVER_CHECK_CODOMAIN_SORT(sort
);
6718 CVC5_API_SOLVER_CHECK_TERM(term
);
6719 CVC5_API_CHECK(sort
== term
.getSort())
6720 << "Invalid sort of function body '" << term
<< "', expected '" << sort
6723 std::vector
<Sort
> domain_sorts
;
6724 for (const auto& bv
: bound_vars
)
6726 domain_sorts
.push_back(bv
.getSort());
6729 domain_sorts
.empty()
6732 getNodeManager()->mkFunctionType(
6733 Sort::sortVectorToTypeNodes(domain_sorts
), *sort
.d_type
));
6734 Term fun
= mkConst(fun_sort
, symbol
);
6736 CVC5_API_SOLVER_CHECK_BOUND_VARS_DEF_FUN(fun
, bound_vars
, domain_sorts
);
6737 //////// all checks before this line
6739 d_slv
->defineFunction(
6740 *fun
.d_node
, Term::termVectorToNodes(bound_vars
), *term
.d_node
, global
);
6743 CVC5_API_TRY_CATCH_END
;
6746 Term
Solver::defineFun(const Term
& fun
,
6747 const std::vector
<Term
>& bound_vars
,
6751 CVC5_API_TRY_CATCH_BEGIN
;
6752 CVC5_API_SOLVER_CHECK_TERM(fun
);
6753 CVC5_API_SOLVER_CHECK_TERM(term
);
6754 if (fun
.getSort().isFunction())
6756 std::vector
<Sort
> domain_sorts
= fun
.getSort().getFunctionDomainSorts();
6757 CVC5_API_SOLVER_CHECK_BOUND_VARS_DEF_FUN(fun
, bound_vars
, domain_sorts
);
6758 Sort codomain
= fun
.getSort().getFunctionCodomainSort();
6759 CVC5_API_CHECK(codomain
== term
.getSort())
6760 << "Invalid sort of function body '" << term
<< "', expected '"
6765 CVC5_API_SOLVER_CHECK_BOUND_VARS(bound_vars
);
6766 CVC5_API_ARG_CHECK_EXPECTED(bound_vars
.size() == 0, fun
)
6767 << "function or nullary symbol";
6769 //////// all checks before this line
6770 std::vector
<Node
> ebound_vars
= Term::termVectorToNodes(bound_vars
);
6771 d_slv
->defineFunction(*fun
.d_node
, ebound_vars
, *term
.d_node
, global
);
6774 CVC5_API_TRY_CATCH_END
;
6777 Term
Solver::defineFunRec(const std::string
& symbol
,
6778 const std::vector
<Term
>& bound_vars
,
6783 CVC5_API_TRY_CATCH_BEGIN
;
6785 CVC5_API_CHECK(d_slv
->getUserLogicInfo().isQuantified())
6786 << "recursive function definitions require a logic with quantifiers";
6787 CVC5_API_CHECK(d_slv
->getUserLogicInfo().isTheoryEnabled(theory::THEORY_UF
))
6788 << "recursive function definitions require a logic with uninterpreted "
6791 CVC5_API_SOLVER_CHECK_TERM(term
);
6792 CVC5_API_SOLVER_CHECK_CODOMAIN_SORT(sort
);
6793 CVC5_API_CHECK(sort
== term
.getSort())
6794 << "Invalid sort of function body '" << term
<< "', expected '" << sort
6797 std::vector
<Sort
> domain_sorts
;
6798 for (const auto& bv
: bound_vars
)
6800 domain_sorts
.push_back(bv
.getSort());
6803 domain_sorts
.empty()
6806 getNodeManager()->mkFunctionType(
6807 Sort::sortVectorToTypeNodes(domain_sorts
), *sort
.d_type
));
6808 Term fun
= mkConst(fun_sort
, symbol
);
6810 CVC5_API_SOLVER_CHECK_BOUND_VARS_DEF_FUN(fun
, bound_vars
, domain_sorts
);
6811 //////// all checks before this line
6813 d_slv
->defineFunctionRec(
6814 *fun
.d_node
, Term::termVectorToNodes(bound_vars
), *term
.d_node
, global
);
6818 CVC5_API_TRY_CATCH_END
;
6821 Term
Solver::defineFunRec(const Term
& fun
,
6822 const std::vector
<Term
>& bound_vars
,
6826 CVC5_API_TRY_CATCH_BEGIN
;
6828 CVC5_API_CHECK(d_slv
->getUserLogicInfo().isQuantified())
6829 << "recursive function definitions require a logic with quantifiers";
6830 CVC5_API_CHECK(d_slv
->getUserLogicInfo().isTheoryEnabled(theory::THEORY_UF
))
6831 << "recursive function definitions require a logic with uninterpreted "
6834 CVC5_API_SOLVER_CHECK_TERM(fun
);
6835 CVC5_API_SOLVER_CHECK_TERM(term
);
6836 if (fun
.getSort().isFunction())
6838 std::vector
<Sort
> domain_sorts
= fun
.getSort().getFunctionDomainSorts();
6839 CVC5_API_SOLVER_CHECK_BOUND_VARS_DEF_FUN(fun
, bound_vars
, domain_sorts
);
6840 Sort codomain
= fun
.getSort().getFunctionCodomainSort();
6841 CVC5_API_CHECK(codomain
== term
.getSort())
6842 << "Invalid sort of function body '" << term
<< "', expected '"
6847 CVC5_API_SOLVER_CHECK_BOUND_VARS(bound_vars
);
6848 CVC5_API_ARG_CHECK_EXPECTED(bound_vars
.size() == 0, fun
)
6849 << "function or nullary symbol";
6851 //////// all checks before this line
6853 std::vector
<Node
> ebound_vars
= Term::termVectorToNodes(bound_vars
);
6854 d_slv
->defineFunctionRec(*fun
.d_node
, ebound_vars
, *term
.d_node
, global
);
6857 CVC5_API_TRY_CATCH_END
;
6860 void Solver::defineFunsRec(const std::vector
<Term
>& funs
,
6861 const std::vector
<std::vector
<Term
>>& bound_vars
,
6862 const std::vector
<Term
>& terms
,
6865 CVC5_API_TRY_CATCH_BEGIN
;
6867 CVC5_API_CHECK(d_slv
->getUserLogicInfo().isQuantified())
6868 << "recursive function definitions require a logic with quantifiers";
6869 CVC5_API_CHECK(d_slv
->getUserLogicInfo().isTheoryEnabled(theory::THEORY_UF
))
6870 << "recursive function definitions require a logic with uninterpreted "
6872 CVC5_API_SOLVER_CHECK_TERMS(funs
);
6873 CVC5_API_SOLVER_CHECK_TERMS(terms
);
6875 size_t funs_size
= funs
.size();
6876 CVC5_API_ARG_SIZE_CHECK_EXPECTED(funs_size
== bound_vars
.size(), bound_vars
)
6877 << "'" << funs_size
<< "'";
6878 CVC5_API_ARG_SIZE_CHECK_EXPECTED(funs_size
== terms
.size(), terms
)
6879 << "'" << funs_size
<< "'";
6881 for (size_t j
= 0; j
< funs_size
; ++j
)
6883 const Term
& fun
= funs
[j
];
6884 const std::vector
<Term
>& bvars
= bound_vars
[j
];
6885 const Term
& term
= terms
[j
];
6887 CVC5_API_ARG_AT_INDEX_CHECK_EXPECTED(
6888 this == fun
.d_solver
, "function", funs
, j
)
6889 << "function associated with this solver object";
6890 CVC5_API_ARG_AT_INDEX_CHECK_EXPECTED(
6891 this == term
.d_solver
, "term", terms
, j
)
6892 << "term associated with this solver object";
6894 if (fun
.getSort().isFunction())
6896 std::vector
<Sort
> domain_sorts
= fun
.getSort().getFunctionDomainSorts();
6897 CVC5_API_SOLVER_CHECK_BOUND_VARS_DEF_FUN(fun
, bvars
, domain_sorts
);
6898 Sort codomain
= fun
.getSort().getFunctionCodomainSort();
6899 CVC5_API_ARG_AT_INDEX_CHECK_EXPECTED(
6900 codomain
== term
.getSort(), "sort of function body", terms
, j
)
6901 << "'" << codomain
<< "'";
6905 CVC5_API_SOLVER_CHECK_BOUND_VARS(bvars
);
6906 CVC5_API_ARG_CHECK_EXPECTED(bvars
.size() == 0, fun
)
6907 << "function or nullary symbol";
6910 //////// all checks before this line
6911 std::vector
<Node
> efuns
= Term::termVectorToNodes(funs
);
6912 std::vector
<std::vector
<Node
>> ebound_vars
;
6913 for (const auto& v
: bound_vars
)
6915 ebound_vars
.push_back(Term::termVectorToNodes(v
));
6917 std::vector
<Node
> nodes
= Term::termVectorToNodes(terms
);
6918 d_slv
->defineFunctionsRec(efuns
, ebound_vars
, nodes
, global
);
6920 CVC5_API_TRY_CATCH_END
;
6923 void Solver::echo(std::ostream
& out
, const std::string
& str
) const
6928 std::vector
<Term
> Solver::getAssertions(void) const
6930 CVC5_API_TRY_CATCH_BEGIN
;
6931 //////// all checks before this line
6932 std::vector
<Node
> assertions
= d_slv
->getAssertions();
6934 * return std::vector<Term>(assertions.begin(), assertions.end());
6935 * here since constructor is private */
6936 std::vector
<Term
> res
;
6937 for (const Node
& e
: assertions
)
6939 res
.push_back(Term(this, e
));
6943 CVC5_API_TRY_CATCH_END
;
6946 std::string
Solver::getInfo(const std::string
& flag
) const
6948 CVC5_API_TRY_CATCH_BEGIN
;
6949 CVC5_API_RECOVERABLE_CHECK(d_slv
->isValidGetInfoFlag(flag
))
6950 << "Unrecognized flag for getInfo.";
6951 //////// all checks before this line
6952 return d_slv
->getInfo(flag
);
6954 CVC5_API_TRY_CATCH_END
;
6957 std::string
Solver::getOption(const std::string
& option
) const
6959 CVC5_API_TRY_CATCH_BEGIN
;
6960 //////// all checks before this line
6961 return d_slv
->getOption(option
);
6963 CVC5_API_TRY_CATCH_END
;
6966 // Supports a visitor from a list of lambdas
6967 // Taken from https://en.cppreference.com/w/cpp/utility/variant/visit
6968 template<class... Ts
> struct overloaded
: Ts
... { using Ts::operator()...; };
6969 template<class... Ts
> overloaded(Ts
...) -> overloaded
<Ts
...>;
6971 bool OptionInfo::boolValue() const
6973 CVC5_API_TRY_CATCH_BEGIN
;
6974 CVC5_API_RECOVERABLE_CHECK(std::holds_alternative
<ValueInfo
<bool>>(valueInfo
))
6975 << name
<< " is not a bool option";
6976 //////// all checks before this line
6977 return std::get
<ValueInfo
<bool>>(valueInfo
).currentValue
;
6979 CVC5_API_TRY_CATCH_END
;
6981 std::string
OptionInfo::stringValue() const
6983 CVC5_API_TRY_CATCH_BEGIN
;
6984 CVC5_API_RECOVERABLE_CHECK(
6985 std::holds_alternative
<ValueInfo
<std::string
>>(valueInfo
))
6986 << name
<< " is not a string option";
6987 //////// all checks before this line
6988 return std::get
<ValueInfo
<std::string
>>(valueInfo
).currentValue
;
6990 CVC5_API_TRY_CATCH_END
;
6992 int64_t OptionInfo::intValue() const
6994 CVC5_API_TRY_CATCH_BEGIN
;
6995 CVC5_API_RECOVERABLE_CHECK(
6996 std::holds_alternative
<NumberInfo
<int64_t>>(valueInfo
))
6997 << name
<< " is not an int option";
6998 //////// all checks before this line
6999 return std::get
<NumberInfo
<int64_t>>(valueInfo
).currentValue
;
7001 CVC5_API_TRY_CATCH_END
;
7003 uint64_t OptionInfo::uintValue() const
7005 CVC5_API_TRY_CATCH_BEGIN
;
7006 CVC5_API_RECOVERABLE_CHECK(
7007 std::holds_alternative
<NumberInfo
<uint64_t>>(valueInfo
))
7008 << name
<< " is not a uint option";
7009 //////// all checks before this line
7010 return std::get
<NumberInfo
<uint64_t>>(valueInfo
).currentValue
;
7012 CVC5_API_TRY_CATCH_END
;
7014 double OptionInfo::doubleValue() const
7016 CVC5_API_TRY_CATCH_BEGIN
;
7017 CVC5_API_RECOVERABLE_CHECK(
7018 std::holds_alternative
<NumberInfo
<double>>(valueInfo
))
7019 << name
<< " is not a double option";
7020 //////// all checks before this line
7021 return std::get
<NumberInfo
<double>>(valueInfo
).currentValue
;
7023 CVC5_API_TRY_CATCH_END
;
7026 std::ostream
& operator<<(std::ostream
& os
, const OptionInfo
& oi
)
7028 os
<< "OptionInfo{ " << oi
.name
;
7031 os
<< " | set by user";
7033 if (!oi
.aliases
.empty())
7035 container_to_stream(os
, oi
.aliases
, ", ", "", ", ");
7037 auto printNum
= [&os
](const std::string
& type
, const auto& vi
) {
7038 os
<< " | " << type
<< " | " << vi
.currentValue
<< " | default "
7040 if (vi
.minimum
|| vi
.maximum
)
7045 os
<< " " << *vi
.minimum
<< " <=";
7050 os
<< " <= " << *vi
.maximum
;
7054 std::visit(overloaded
{
7055 [&os
](const OptionInfo::VoidInfo
& vi
) { os
<< " | void"; },
7056 [&os
](const OptionInfo::ValueInfo
<bool>& vi
) {
7057 os
<< " | bool | " << vi
.currentValue
<< " | default "
7060 [&os
](const OptionInfo::ValueInfo
<std::string
>& vi
) {
7061 os
<< " | string | " << vi
.currentValue
<< " | default "
7064 [&printNum
](const OptionInfo::NumberInfo
<int64_t>& vi
) {
7065 printNum("int64_t", vi
);
7067 [&printNum
](const OptionInfo::NumberInfo
<uint64_t>& vi
) {
7068 printNum("uint64_t", vi
);
7070 [&printNum
](const OptionInfo::NumberInfo
<double>& vi
) {
7071 printNum("double", vi
);
7073 [&os
](const OptionInfo::ModeInfo
& vi
) {
7074 os
<< " | mode | " << vi
.currentValue
<< " | default "
7075 << vi
.defaultValue
<< " | modes: ";
7076 container_to_stream(os
, vi
.modes
, "", "", ", ");
7084 std::vector
<std::string
> Solver::getOptionNames() const
7086 CVC5_API_TRY_CATCH_BEGIN
;
7087 //////// all checks before this line
7088 return options::getNames();
7090 CVC5_API_TRY_CATCH_END
;
7093 OptionInfo
Solver::getOptionInfo(const std::string
& option
) const
7095 CVC5_API_TRY_CATCH_BEGIN
;
7096 //////// all checks before this line
7097 auto info
= options::getInfo(d_slv
->getOptions(), option
);
7098 CVC5_API_CHECK(info
.name
!= "")
7099 << "Querying invalid or unknown option " << option
;
7102 [&info
](const options::OptionInfo::VoidInfo
& vi
) {
7103 return OptionInfo
{info
.name
,
7106 OptionInfo::VoidInfo
{}};
7108 [&info
](const options::OptionInfo::ValueInfo
<bool>& vi
) {
7113 OptionInfo::ValueInfo
<bool>{vi
.defaultValue
, vi
.currentValue
}};
7115 [&info
](const options::OptionInfo::ValueInfo
<std::string
>& vi
) {
7116 return OptionInfo
{info
.name
,
7119 OptionInfo::ValueInfo
<std::string
>{
7120 vi
.defaultValue
, vi
.currentValue
}};
7122 [&info
](const options::OptionInfo::NumberInfo
<int64_t>& vi
) {
7127 OptionInfo::NumberInfo
<int64_t>{
7128 vi
.defaultValue
, vi
.currentValue
, vi
.minimum
, vi
.maximum
}};
7130 [&info
](const options::OptionInfo::NumberInfo
<uint64_t>& vi
) {
7135 OptionInfo::NumberInfo
<uint64_t>{
7136 vi
.defaultValue
, vi
.currentValue
, vi
.minimum
, vi
.maximum
}};
7138 [&info
](const options::OptionInfo::NumberInfo
<double>& vi
) {
7143 OptionInfo::NumberInfo
<double>{
7144 vi
.defaultValue
, vi
.currentValue
, vi
.minimum
, vi
.maximum
}};
7146 [&info
](const options::OptionInfo::ModeInfo
& vi
) {
7147 return OptionInfo
{info
.name
,
7150 OptionInfo::ModeInfo
{
7151 vi
.defaultValue
, vi
.currentValue
, vi
.modes
}};
7156 CVC5_API_TRY_CATCH_END
;
7159 DriverOptions
Solver::getDriverOptions() const { return DriverOptions(*this); }
7161 std::vector
<Term
> Solver::getUnsatAssumptions(void) const
7163 CVC5_API_TRY_CATCH_BEGIN
;
7164 CVC5_API_CHECK(d_slv
->getOptions().base
.incrementalSolving
)
7165 << "Cannot get unsat assumptions unless incremental solving is enabled "
7166 "(try --incremental)";
7167 CVC5_API_CHECK(d_slv
->getOptions().smt
.unsatAssumptions
)
7168 << "Cannot get unsat assumptions unless explicitly enabled "
7169 "(try --produce-unsat-assumptions)";
7170 CVC5_API_CHECK(d_slv
->getSmtMode() == SmtMode::UNSAT
)
7171 << "Cannot get unsat assumptions unless in unsat mode.";
7172 //////// all checks before this line
7174 std::vector
<Node
> uassumptions
= d_slv
->getUnsatAssumptions();
7176 * return std::vector<Term>(uassumptions.begin(), uassumptions.end());
7177 * here since constructor is private */
7178 std::vector
<Term
> res
;
7179 for (const Node
& n
: uassumptions
)
7181 res
.push_back(Term(this, n
));
7185 CVC5_API_TRY_CATCH_END
;
7188 std::vector
<Term
> Solver::getUnsatCore(void) const
7190 CVC5_API_TRY_CATCH_BEGIN
;
7191 CVC5_API_CHECK(d_slv
->getOptions().smt
.unsatCores
)
7192 << "Cannot get unsat core unless explicitly enabled "
7193 "(try --produce-unsat-cores)";
7194 CVC5_API_RECOVERABLE_CHECK(d_slv
->getSmtMode() == SmtMode::UNSAT
)
7195 << "Cannot get unsat core unless in unsat mode.";
7196 //////// all checks before this line
7197 UnsatCore core
= d_slv
->getUnsatCore();
7199 * return std::vector<Term>(core.begin(), core.end());
7200 * here since constructor is private */
7201 std::vector
<Term
> res
;
7202 for (const Node
& e
: core
)
7204 res
.push_back(Term(this, e
));
7208 CVC5_API_TRY_CATCH_END
;
7211 std::map
<Term
, Term
> Solver::getDifficulty() const
7213 CVC5_API_TRY_CATCH_BEGIN
;
7214 CVC5_API_RECOVERABLE_CHECK(d_slv
->getSmtMode() == SmtMode::UNSAT
7215 || d_slv
->getSmtMode() == SmtMode::SAT
7216 || d_slv
->getSmtMode() == SmtMode::SAT_UNKNOWN
)
7217 << "Cannot get difficulty unless after a UNSAT, SAT or UNKNOWN response.";
7218 //////// all checks before this line
7219 std::map
<Term
, Term
> res
;
7220 std::map
<Node
, Node
> dmap
;
7221 d_slv
->getDifficultyMap(dmap
);
7222 for (const std::pair
<const Node
, Node
>& d
: dmap
)
7224 res
[Term(this, d
.first
)] = Term(this, d
.second
);
7228 CVC5_API_TRY_CATCH_END
;
7231 std::string
Solver::getProof(void) const
7233 CVC5_API_TRY_CATCH_BEGIN
;
7234 CVC5_API_CHECK(d_slv
->getOptions().smt
.produceProofs
)
7235 << "Cannot get proof unless proofs are enabled (try --produce-proofs)";
7236 CVC5_API_RECOVERABLE_CHECK(d_slv
->getSmtMode() == SmtMode::UNSAT
)
7237 << "Cannot get proof unless in unsat mode.";
7238 return d_slv
->getProof();
7239 CVC5_API_TRY_CATCH_END
;
7242 Term
Solver::getValue(const Term
& term
) const
7244 CVC5_API_TRY_CATCH_BEGIN
;
7245 CVC5_API_RECOVERABLE_CHECK(d_slv
->getOptions().smt
.produceModels
)
7246 << "Cannot get value unless model generation is enabled "
7247 "(try --produce-models)";
7248 CVC5_API_RECOVERABLE_CHECK(d_slv
->isSmtModeSat())
7249 << "Cannot get value unless after a SAT or UNKNOWN response.";
7250 CVC5_API_SOLVER_CHECK_TERM(term
);
7251 CVC5_API_RECOVERABLE_CHECK(term
.getSort().isFirstClass())
7252 << "Cannot get value of a term that is not first class.";
7253 //////// all checks before this line
7254 return getValueHelper(term
);
7256 CVC5_API_TRY_CATCH_END
;
7259 std::vector
<Term
> Solver::getValue(const std::vector
<Term
>& terms
) const
7261 CVC5_API_TRY_CATCH_BEGIN
;
7262 CVC5_API_RECOVERABLE_CHECK(d_slv
->getOptions().smt
.produceModels
)
7263 << "Cannot get value unless model generation is enabled "
7264 "(try --produce-models)";
7265 CVC5_API_RECOVERABLE_CHECK(d_slv
->isSmtModeSat())
7266 << "Cannot get value unless after a SAT or UNKNOWN response.";
7267 for (const Term
& t
: terms
)
7269 CVC5_API_RECOVERABLE_CHECK(t
.getSort().isFirstClass())
7270 << "Cannot get value of a term that is not first class.";
7272 CVC5_API_SOLVER_CHECK_TERMS(terms
);
7273 //////// all checks before this line
7275 std::vector
<Term
> res
;
7276 for (size_t i
= 0, n
= terms
.size(); i
< n
; ++i
)
7278 /* Can not use emplace_back here since constructor is private. */
7279 res
.push_back(getValueHelper(terms
[i
]));
7283 CVC5_API_TRY_CATCH_END
;
7286 std::vector
<Term
> Solver::getModelDomainElements(const Sort
& s
) const
7288 CVC5_API_TRY_CATCH_BEGIN
;
7289 CVC5_API_RECOVERABLE_CHECK(d_slv
->getOptions().smt
.produceModels
)
7290 << "Cannot get domain elements unless model generation is enabled "
7291 "(try --produce-models)";
7292 CVC5_API_RECOVERABLE_CHECK(d_slv
->isSmtModeSat())
7293 << "Cannot get domain elements unless after a SAT or UNKNOWN response.";
7294 CVC5_API_SOLVER_CHECK_SORT(s
);
7295 CVC5_API_RECOVERABLE_CHECK(s
.isUninterpretedSort())
7296 << "Expecting an uninterpreted sort as argument to "
7297 "getModelDomainElements.";
7298 //////// all checks before this line
7299 std::vector
<Term
> res
;
7300 std::vector
<Node
> elements
= d_slv
->getModelDomainElements(s
.getTypeNode());
7301 for (const Node
& n
: elements
)
7303 res
.push_back(Term(this, n
));
7307 CVC5_API_TRY_CATCH_END
;
7310 bool Solver::isModelCoreSymbol(const Term
& v
) const
7312 CVC5_API_TRY_CATCH_BEGIN
;
7313 CVC5_API_RECOVERABLE_CHECK(d_slv
->getOptions().smt
.produceModels
)
7314 << "Cannot check if model core symbol unless model generation is enabled "
7315 "(try --produce-models)";
7316 CVC5_API_RECOVERABLE_CHECK(d_slv
->isSmtModeSat())
7317 << "Cannot check if model core symbol unless after a SAT or UNKNOWN "
7319 CVC5_API_SOLVER_CHECK_TERM(v
);
7320 CVC5_API_RECOVERABLE_CHECK(v
.getKind() == CONSTANT
)
7321 << "Expecting a free constant as argument to isModelCoreSymbol.";
7322 //////// all checks before this line
7323 return d_slv
->isModelCoreSymbol(v
.getNode());
7325 CVC5_API_TRY_CATCH_END
;
7328 std::string
Solver::getModel(const std::vector
<Sort
>& sorts
,
7329 const std::vector
<Term
>& vars
) const
7331 CVC5_API_TRY_CATCH_BEGIN
;
7332 CVC5_API_RECOVERABLE_CHECK(d_slv
->getOptions().smt
.produceModels
)
7333 << "Cannot get model unless model generation is enabled "
7334 "(try --produce-models)";
7335 CVC5_API_RECOVERABLE_CHECK(d_slv
->isSmtModeSat())
7336 << "Cannot get model unless after a SAT or UNKNOWN response.";
7337 CVC5_API_SOLVER_CHECK_SORTS(sorts
);
7338 for (const Sort
& s
: sorts
)
7340 CVC5_API_RECOVERABLE_CHECK(s
.isUninterpretedSort())
7341 << "Expecting an uninterpreted sort as argument to "
7344 CVC5_API_SOLVER_CHECK_TERMS(vars
);
7345 for (const Term
& v
: vars
)
7347 CVC5_API_RECOVERABLE_CHECK(v
.getKind() == CONSTANT
)
7348 << "Expecting a free constant as argument to getModel.";
7350 //////// all checks before this line
7351 return d_slv
->getModel(Sort::sortVectorToTypeNodes(sorts
),
7352 Term::termVectorToNodes(vars
));
7354 CVC5_API_TRY_CATCH_END
;
7357 Term
Solver::getQuantifierElimination(const Term
& q
) const
7359 CVC5_API_TRY_CATCH_BEGIN
;
7360 CVC5_API_SOLVER_CHECK_TERM(q
);
7361 //////// all checks before this line
7362 return Term(this, d_slv
->getQuantifierElimination(q
.getNode(), true, true));
7364 CVC5_API_TRY_CATCH_END
;
7367 Term
Solver::getQuantifierEliminationDisjunct(const Term
& q
) const
7369 CVC5_API_TRY_CATCH_BEGIN
;
7370 CVC5_API_SOLVER_CHECK_TERM(q
);
7371 //////// all checks before this line
7372 return Term(this, d_slv
->getQuantifierElimination(q
.getNode(), false, true));
7374 CVC5_API_TRY_CATCH_END
;
7377 void Solver::declareSeparationHeap(const Sort
& locSort
,
7378 const Sort
& dataSort
) const
7380 CVC5_API_TRY_CATCH_BEGIN
;
7381 CVC5_API_SOLVER_CHECK_SORT(locSort
);
7382 CVC5_API_SOLVER_CHECK_SORT(dataSort
);
7383 CVC5_API_CHECK(d_slv
->getLogicInfo().isTheoryEnabled(theory::THEORY_SEP
))
7384 << "Cannot obtain separation logic expressions if not using the "
7385 "separation logic theory.";
7386 //////// all checks before this line
7387 d_slv
->declareSepHeap(locSort
.getTypeNode(), dataSort
.getTypeNode());
7389 CVC5_API_TRY_CATCH_END
;
7392 Term
Solver::getSeparationHeap() const
7394 CVC5_API_TRY_CATCH_BEGIN
;
7395 CVC5_API_CHECK(d_slv
->getLogicInfo().isTheoryEnabled(theory::THEORY_SEP
))
7396 << "Cannot obtain separation logic expressions if not using the "
7397 "separation logic theory.";
7398 CVC5_API_CHECK(d_slv
->getOptions().smt
.produceModels
)
7399 << "Cannot get separation heap term unless model generation is enabled "
7400 "(try --produce-models)";
7401 CVC5_API_RECOVERABLE_CHECK(d_slv
->isSmtModeSat())
7402 << "Can only get separtion heap term after SAT or UNKNOWN response.";
7403 //////// all checks before this line
7404 return Term(this, d_slv
->getSepHeapExpr());
7406 CVC5_API_TRY_CATCH_END
;
7409 Term
Solver::getSeparationNilTerm() const
7411 CVC5_API_TRY_CATCH_BEGIN
;
7412 CVC5_API_CHECK(d_slv
->getLogicInfo().isTheoryEnabled(theory::THEORY_SEP
))
7413 << "Cannot obtain separation logic expressions if not using the "
7414 "separation logic theory.";
7415 CVC5_API_CHECK(d_slv
->getOptions().smt
.produceModels
)
7416 << "Cannot get separation nil term unless model generation is enabled "
7417 "(try --produce-models)";
7418 CVC5_API_RECOVERABLE_CHECK(d_slv
->isSmtModeSat())
7419 << "Can only get separtion nil term after SAT or UNKNOWN response.";
7420 //////// all checks before this line
7421 return Term(this, d_slv
->getSepNilExpr());
7423 CVC5_API_TRY_CATCH_END
;
7426 Term
Solver::declarePool(const std::string
& symbol
,
7428 const std::vector
<Term
>& initValue
) const
7430 CVC5_API_TRY_CATCH_BEGIN
;
7431 CVC5_API_SOLVER_CHECK_SORT(sort
);
7432 CVC5_API_SOLVER_CHECK_TERMS(initValue
);
7433 //////// all checks before this line
7434 TypeNode setType
= getNodeManager()->mkSetType(*sort
.d_type
);
7435 Node pool
= getNodeManager()->mkBoundVar(symbol
, setType
);
7436 std::vector
<Node
> initv
= Term::termVectorToNodes(initValue
);
7437 d_slv
->declarePool(pool
, initv
);
7438 return Term(this, pool
);
7440 CVC5_API_TRY_CATCH_END
;
7443 void Solver::pop(uint32_t nscopes
) const
7445 CVC5_API_TRY_CATCH_BEGIN
;
7446 CVC5_API_CHECK(d_slv
->getOptions().base
.incrementalSolving
)
7447 << "Cannot pop when not solving incrementally (use --incremental)";
7448 CVC5_API_CHECK(nscopes
<= d_slv
->getNumUserLevels())
7449 << "Cannot pop beyond first pushed context";
7450 //////// all checks before this line
7451 for (uint32_t n
= 0; n
< nscopes
; ++n
)
7456 CVC5_API_TRY_CATCH_END
;
7459 bool Solver::getInterpolant(const Term
& conj
, Term
& output
) const
7461 CVC5_API_TRY_CATCH_BEGIN
;
7462 CVC5_API_SOLVER_CHECK_TERM(conj
);
7463 //////// all checks before this line
7465 bool success
= d_slv
->getInterpol(*conj
.d_node
, result
);
7468 output
= Term(this, result
);
7472 CVC5_API_TRY_CATCH_END
;
7475 bool Solver::getInterpolant(const Term
& conj
,
7479 CVC5_API_TRY_CATCH_BEGIN
;
7480 CVC5_API_SOLVER_CHECK_TERM(conj
);
7481 //////// all checks before this line
7484 d_slv
->getInterpol(*conj
.d_node
, *grammar
.resolve().d_type
, result
);
7487 output
= Term(this, result
);
7491 CVC5_API_TRY_CATCH_END
;
7494 bool Solver::getAbduct(const Term
& conj
, Term
& output
) const
7496 CVC5_API_TRY_CATCH_BEGIN
;
7497 CVC5_API_SOLVER_CHECK_TERM(conj
);
7498 CVC5_API_CHECK(d_slv
->getOptions().smt
.produceAbducts
)
7499 << "Cannot get abduct unless abducts are enabled (try --produce-abducts)";
7500 //////// all checks before this line
7502 bool success
= d_slv
->getAbduct(*conj
.d_node
, result
);
7505 output
= Term(this, result
);
7509 CVC5_API_TRY_CATCH_END
;
7512 bool Solver::getAbduct(const Term
& conj
, Grammar
& grammar
, Term
& output
) const
7514 CVC5_API_TRY_CATCH_BEGIN
;
7515 CVC5_API_SOLVER_CHECK_TERM(conj
);
7516 CVC5_API_CHECK(d_slv
->getOptions().smt
.produceAbducts
)
7517 << "Cannot get abduct unless abducts are enabled (try --produce-abducts)";
7518 //////// all checks before this line
7521 d_slv
->getAbduct(*conj
.d_node
, *grammar
.resolve().d_type
, result
);
7524 output
= Term(this, result
);
7528 CVC5_API_TRY_CATCH_END
;
7531 void Solver::blockModel() const
7533 CVC5_API_TRY_CATCH_BEGIN
;
7534 CVC5_API_CHECK(d_slv
->getOptions().smt
.produceModels
)
7535 << "Cannot get value unless model generation is enabled "
7536 "(try --produce-models)";
7537 CVC5_API_RECOVERABLE_CHECK(d_slv
->isSmtModeSat())
7538 << "Can only block model after SAT or UNKNOWN response.";
7539 //////// all checks before this line
7540 d_slv
->blockModel();
7542 CVC5_API_TRY_CATCH_END
;
7545 void Solver::blockModelValues(const std::vector
<Term
>& terms
) const
7547 CVC5_API_TRY_CATCH_BEGIN
;
7548 CVC5_API_CHECK(d_slv
->getOptions().smt
.produceModels
)
7549 << "Cannot get value unless model generation is enabled "
7550 "(try --produce-models)";
7551 CVC5_API_RECOVERABLE_CHECK(d_slv
->isSmtModeSat())
7552 << "Can only block model values after SAT or UNKNOWN response.";
7553 CVC5_API_ARG_SIZE_CHECK_EXPECTED(!terms
.empty(), terms
)
7554 << "a non-empty set of terms";
7555 CVC5_API_SOLVER_CHECK_TERMS(terms
);
7556 //////// all checks before this line
7557 d_slv
->blockModelValues(Term::termVectorToNodes(terms
));
7559 CVC5_API_TRY_CATCH_END
;
7562 void Solver::printInstantiations(std::ostream
& out
) const
7564 CVC5_API_TRY_CATCH_BEGIN
;
7565 //////// all checks before this line
7566 d_slv
->printInstantiations(out
);
7568 CVC5_API_TRY_CATCH_END
;
7571 void Solver::push(uint32_t nscopes
) const
7573 CVC5_API_TRY_CATCH_BEGIN
;
7574 CVC5_API_CHECK(d_slv
->getOptions().base
.incrementalSolving
)
7575 << "Cannot push when not solving incrementally (use --incremental)";
7576 //////// all checks before this line
7577 for (uint32_t n
= 0; n
< nscopes
; ++n
)
7582 CVC5_API_TRY_CATCH_END
;
7585 void Solver::resetAssertions(void) const
7587 CVC5_API_TRY_CATCH_BEGIN
;
7588 //////// all checks before this line
7589 d_slv
->resetAssertions();
7591 CVC5_API_TRY_CATCH_END
;
7594 void Solver::setInfo(const std::string
& keyword
, const std::string
& value
) const
7596 CVC5_API_TRY_CATCH_BEGIN
;
7597 CVC5_API_RECOVERABLE_ARG_CHECK_EXPECTED(
7598 keyword
== "source" || keyword
== "category" || keyword
== "difficulty"
7599 || keyword
== "filename" || keyword
== "license" || keyword
== "name"
7600 || keyword
== "notes" || keyword
== "smt-lib-version"
7601 || keyword
== "status",
7603 << "'source', 'category', 'difficulty', 'filename', 'license', 'name', "
7604 "'notes', 'smt-lib-version' or 'status'";
7605 CVC5_API_RECOVERABLE_ARG_CHECK_EXPECTED(
7606 keyword
!= "smt-lib-version" || value
== "2" || value
== "2.0"
7607 || value
== "2.5" || value
== "2.6",
7609 << "'2.0', '2.5', '2.6'";
7610 CVC5_API_ARG_CHECK_EXPECTED(keyword
!= "status" || value
== "sat"
7611 || value
== "unsat" || value
== "unknown",
7613 << "'sat', 'unsat' or 'unknown'";
7614 //////// all checks before this line
7615 d_slv
->setInfo(keyword
, value
);
7617 CVC5_API_TRY_CATCH_END
;
7620 void Solver::setLogic(const std::string
& logic
) const
7622 CVC5_API_TRY_CATCH_BEGIN
;
7623 CVC5_API_CHECK(!d_slv
->isFullyInited())
7624 << "Invalid call to 'setLogic', solver is already fully initialized";
7625 cvc5::LogicInfo
logic_info(logic
);
7626 //////// all checks before this line
7627 d_slv
->setLogic(logic_info
);
7629 CVC5_API_TRY_CATCH_END
;
7632 void Solver::setOption(const std::string
& option
,
7633 const std::string
& value
) const
7635 CVC5_API_TRY_CATCH_BEGIN
;
7636 static constexpr auto mutableOpts
= {"diagnostic-output-channel",
7638 "regular-output-channel",
7639 "reproducible-resource-limit",
7641 if (std::find(mutableOpts
.begin(), mutableOpts
.end(), option
)
7642 == mutableOpts
.end())
7644 CVC5_API_CHECK(!d_slv
->isFullyInited())
7645 << "Invalid call to 'setOption' for option '" << option
7646 << "', solver is already fully initialized";
7648 //////// all checks before this line
7649 d_slv
->setOption(option
, value
);
7651 CVC5_API_TRY_CATCH_END
;
7654 Term
Solver::mkSygusVar(const Sort
& sort
, const std::string
& symbol
) const
7656 CVC5_API_TRY_CATCH_BEGIN
;
7657 CVC5_API_SOLVER_CHECK_SORT(sort
);
7658 //////// all checks before this line
7659 Node res
= getNodeManager()->mkBoundVar(symbol
, *sort
.d_type
);
7660 (void)res
.getType(true); /* kick off type checking */
7662 d_slv
->declareSygusVar(res
);
7664 return Term(this, res
);
7666 CVC5_API_TRY_CATCH_END
;
7669 Grammar
Solver::mkSygusGrammar(const std::vector
<Term
>& boundVars
,
7670 const std::vector
<Term
>& ntSymbols
) const
7672 CVC5_API_TRY_CATCH_BEGIN
;
7673 CVC5_API_ARG_SIZE_CHECK_EXPECTED(!ntSymbols
.empty(), ntSymbols
)
7674 << "a non-empty vector";
7675 CVC5_API_SOLVER_CHECK_BOUND_VARS(boundVars
);
7676 CVC5_API_SOLVER_CHECK_BOUND_VARS(ntSymbols
);
7677 //////// all checks before this line
7678 return Grammar(this, boundVars
, ntSymbols
);
7680 CVC5_API_TRY_CATCH_END
;
7683 Term
Solver::synthFun(const std::string
& symbol
,
7684 const std::vector
<Term
>& boundVars
,
7685 const Sort
& sort
) const
7687 CVC5_API_TRY_CATCH_BEGIN
;
7688 CVC5_API_SOLVER_CHECK_BOUND_VARS(boundVars
);
7689 CVC5_API_SOLVER_CHECK_SORT(sort
);
7690 //////// all checks before this line
7691 return synthFunHelper(symbol
, boundVars
, sort
);
7693 CVC5_API_TRY_CATCH_END
;
7696 Term
Solver::synthFun(const std::string
& symbol
,
7697 const std::vector
<Term
>& boundVars
,
7699 Grammar
& grammar
) const
7701 CVC5_API_TRY_CATCH_BEGIN
;
7702 CVC5_API_SOLVER_CHECK_BOUND_VARS(boundVars
);
7703 CVC5_API_SOLVER_CHECK_SORT(sort
);
7704 //////// all checks before this line
7705 return synthFunHelper(symbol
, boundVars
, sort
, false, &grammar
);
7707 CVC5_API_TRY_CATCH_END
;
7710 Term
Solver::synthInv(const std::string
& symbol
,
7711 const std::vector
<Term
>& boundVars
) const
7713 CVC5_API_TRY_CATCH_BEGIN
;
7714 CVC5_API_SOLVER_CHECK_BOUND_VARS(boundVars
);
7715 //////// all checks before this line
7716 return synthFunHelper(
7717 symbol
, boundVars
, Sort(this, getNodeManager()->booleanType()), true);
7719 CVC5_API_TRY_CATCH_END
;
7722 Term
Solver::synthInv(const std::string
& symbol
,
7723 const std::vector
<Term
>& boundVars
,
7724 Grammar
& grammar
) const
7726 CVC5_API_TRY_CATCH_BEGIN
;
7727 CVC5_API_SOLVER_CHECK_BOUND_VARS(boundVars
);
7728 //////// all checks before this line
7729 return synthFunHelper(symbol
,
7731 Sort(this, getNodeManager()->booleanType()),
7735 CVC5_API_TRY_CATCH_END
;
7738 void Solver::addSygusConstraint(const Term
& term
) const
7740 CVC5_API_TRY_CATCH_BEGIN
;
7741 CVC5_API_SOLVER_CHECK_TERM(term
);
7742 CVC5_API_ARG_CHECK_EXPECTED(
7743 term
.d_node
->getType() == getNodeManager()->booleanType(), term
)
7745 //////// all checks before this line
7746 d_slv
->assertSygusConstraint(*term
.d_node
, false);
7748 CVC5_API_TRY_CATCH_END
;
7751 void Solver::addSygusAssume(const Term
& term
) const
7753 CVC5_API_TRY_CATCH_BEGIN
;
7754 CVC5_API_SOLVER_CHECK_TERM(term
);
7755 CVC5_API_ARG_CHECK_EXPECTED(
7756 term
.d_node
->getType() == getNodeManager()->booleanType(), term
)
7758 //////// all checks before this line
7759 d_slv
->assertSygusConstraint(*term
.d_node
, true);
7761 CVC5_API_TRY_CATCH_END
;
7764 void Solver::addSygusInvConstraint(Term inv
,
7769 CVC5_API_TRY_CATCH_BEGIN
;
7770 CVC5_API_SOLVER_CHECK_TERM(inv
);
7771 CVC5_API_SOLVER_CHECK_TERM(pre
);
7772 CVC5_API_SOLVER_CHECK_TERM(trans
);
7773 CVC5_API_SOLVER_CHECK_TERM(post
);
7775 CVC5_API_ARG_CHECK_EXPECTED(inv
.d_node
->getType().isFunction(), inv
)
7778 TypeNode invType
= inv
.d_node
->getType();
7780 CVC5_API_ARG_CHECK_EXPECTED(invType
.getRangeType().isBoolean(), inv
)
7783 CVC5_API_CHECK(pre
.d_node
->getType() == invType
)
7784 << "Expected inv and pre to have the same sort";
7786 CVC5_API_CHECK(post
.d_node
->getType() == invType
)
7787 << "Expected inv and post to have the same sort";
7788 //////// all checks before this line
7790 const std::vector
<TypeNode
>& invArgTypes
= invType
.getArgTypes();
7792 std::vector
<TypeNode
> expectedTypes
;
7793 expectedTypes
.reserve(2 * invArgTypes
.size() + 1);
7795 for (size_t i
= 0, n
= invArgTypes
.size(); i
< 2 * n
; i
+= 2)
7797 expectedTypes
.push_back(invArgTypes
[i
% n
]);
7798 expectedTypes
.push_back(invArgTypes
[(i
+ 1) % n
]);
7801 expectedTypes
.push_back(invType
.getRangeType());
7802 TypeNode expectedTransType
= getNodeManager()->mkFunctionType(expectedTypes
);
7804 CVC5_API_CHECK(trans
.d_node
->getType() == expectedTransType
)
7805 << "Expected trans's sort to be " << invType
;
7807 d_slv
->assertSygusInvConstraint(
7808 *inv
.d_node
, *pre
.d_node
, *trans
.d_node
, *post
.d_node
);
7810 CVC5_API_TRY_CATCH_END
;
7813 Result
Solver::checkSynth() const
7815 CVC5_API_TRY_CATCH_BEGIN
;
7816 //////// all checks before this line
7817 return d_slv
->checkSynth();
7819 CVC5_API_TRY_CATCH_END
;
7822 Term
Solver::getSynthSolution(Term term
) const
7824 CVC5_API_TRY_CATCH_BEGIN
;
7825 CVC5_API_SOLVER_CHECK_TERM(term
);
7827 std::map
<cvc5::Node
, cvc5::Node
> map
;
7828 CVC5_API_CHECK(d_slv
->getSynthSolutions(map
))
7829 << "The solver is not in a state immediately preceded by a "
7830 "successful call to checkSynth";
7832 std::map
<cvc5::Node
, cvc5::Node
>::const_iterator it
= map
.find(*term
.d_node
);
7834 CVC5_API_CHECK(it
!= map
.cend()) << "Synth solution not found for given term";
7835 //////// all checks before this line
7836 return Term(this, it
->second
);
7838 CVC5_API_TRY_CATCH_END
;
7841 std::vector
<Term
> Solver::getSynthSolutions(
7842 const std::vector
<Term
>& terms
) const
7844 CVC5_API_TRY_CATCH_BEGIN
;
7845 CVC5_API_ARG_SIZE_CHECK_EXPECTED(!terms
.empty(), terms
) << "non-empty vector";
7846 CVC5_API_SOLVER_CHECK_TERMS(terms
);
7848 std::map
<cvc5::Node
, cvc5::Node
> map
;
7849 CVC5_API_CHECK(d_slv
->getSynthSolutions(map
))
7850 << "The solver is not in a state immediately preceded by a "
7851 "successful call to checkSynth";
7852 //////// all checks before this line
7854 std::vector
<Term
> synthSolution
;
7855 synthSolution
.reserve(terms
.size());
7857 for (size_t i
= 0, n
= terms
.size(); i
< n
; ++i
)
7859 std::map
<cvc5::Node
, cvc5::Node
>::const_iterator it
=
7860 map
.find(*terms
[i
].d_node
);
7862 CVC5_API_CHECK(it
!= map
.cend())
7863 << "Synth solution not found for term at index " << i
;
7865 synthSolution
.push_back(Term(this, it
->second
));
7868 return synthSolution
;
7870 CVC5_API_TRY_CATCH_END
;
7873 Statistics
Solver::getStatistics() const
7875 return Statistics(d_slv
->getStatisticsRegistry());
7878 bool Solver::isOutputOn(const std::string
& tag
) const
7880 // `isOutputOn(tag)` may raise an `OptionException`, which we do not want to
7881 // forward as such. We thus do not use the standard exception handling macros
7882 // here but roll our own.
7885 return d_slv
->getEnv().isOutputOn(tag
);
7887 catch (const cvc5::Exception
& e
)
7889 throw CVC5ApiException("Invalid output tag " + tag
);
7893 std::ostream
& Solver::getOutput(const std::string
& tag
) const
7895 // `getOutput(tag)` may raise an `OptionException`, which we do not want to
7896 // forward as such. We thus do not use the standard exception handling macros
7897 // here but roll our own.
7900 return d_slv
->getEnv().getOutput(tag
);
7902 catch (const cvc5::Exception
& e
)
7904 throw CVC5ApiException("Invalid output tag " + tag
);
7914 size_t hash
<cvc5::api::Kind
>::operator()(cvc5::api::Kind k
) const
7916 return static_cast<size_t>(k
);
7919 size_t hash
<cvc5::api::Op
>::operator()(const cvc5::api::Op
& t
) const
7921 if (t
.isIndexedHelper())
7923 return std::hash
<cvc5::Node
>()(*t
.d_node
);
7927 return std::hash
<cvc5::api::Kind
>()(t
.d_kind
);
7931 size_t std::hash
<cvc5::api::RoundingMode
>::operator()(
7932 cvc5::api::RoundingMode rm
) const
7934 return static_cast<size_t>(rm
);
7937 size_t std::hash
<cvc5::api::Sort
>::operator()(const cvc5::api::Sort
& s
) const
7939 return std::hash
<cvc5::TypeNode
>()(*s
.d_type
);
7942 size_t std::hash
<cvc5::api::Term
>::operator()(const cvc5::api::Term
& t
) const
7944 return std::hash
<cvc5::Node
>()(*t
.d_node
);