1 /******************************************************************************
2 * Top contributors (to current version):
3 * Aina Niemetz, Andrew Reynolds, Andres Noetzli
5 * This file is part of the cvc5 project.
7 * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
8 * in the top-level source directory and their institutional affiliations.
9 * All rights reserved. See the file COPYING in the top-level source
10 * directory for licensing information.
11 * ****************************************************************************
15 * A brief note on how to guard API functions:
17 * In general, we think of API guards as a fence -- they are supposed to make
18 * sure that no invalid arguments get passed into internal realms of cvc5.
19 * Thus we always want to catch such cases on the API level (and can then
20 * assert internally that no invalid argument is passed in).
22 * The only special case is when we use 3rd party back-ends we have no control
23 * over, and which throw (invalid_argument) exceptions anyways. In this case,
24 * we do not replicate argument checks but delegate them to the back-end,
25 * catch thrown exceptions, and raise a CVC5ApiException.
27 * Our Integer implementation, e.g., is such a special case since we support
28 * two different back end implementations (GMP, CLN). Be aware that they do
29 * not fully agree on what is (in)valid input, which requires extra checks for
30 * consistent behavior (see Solver::mkRealOrIntegerFromStrHelper for example).
33 #include "api/cpp/cvc5.h"
38 #include "api/cpp/cvc5_checks.h"
39 #include "base/check.h"
40 #include "base/configuration.h"
41 #include "base/modal_exception.h"
42 #include "expr/array_store_all.h"
43 #include "expr/ascription_type.h"
44 #include "expr/cardinality_constraint.h"
45 #include "expr/dtype.h"
46 #include "expr/dtype_cons.h"
47 #include "expr/dtype_selector.h"
48 #include "expr/emptybag.h"
49 #include "expr/emptyset.h"
50 #include "expr/kind.h"
51 #include "expr/metakind.h"
52 #include "expr/node.h"
53 #include "expr/node_algorithm.h"
54 #include "expr/node_builder.h"
55 #include "expr/node_manager.h"
56 #include "expr/node_manager_attributes.h"
57 #include "expr/sequence.h"
58 #include "expr/type_node.h"
59 #include "options/base_options.h"
60 #include "options/expr_options.h"
61 #include "options/main_options.h"
62 #include "options/option_exception.h"
63 #include "options/options.h"
64 #include "options/options_public.h"
65 #include "options/smt_options.h"
66 #include "proof/unsat_core.h"
68 #include "smt/model.h"
69 #include "smt/smt_mode.h"
70 #include "smt/solver_engine.h"
71 #include "theory/datatypes/tuple_project_op.h"
72 #include "theory/logic_info.h"
73 #include "theory/theory_model.h"
74 #include "util/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/uninterpreted_sort_value.h"
87 #include "util/utility.h"
92 /* -------------------------------------------------------------------------- */
94 /* -------------------------------------------------------------------------- */
98 HistogramStat
<TypeConstant
> d_consts
;
99 HistogramStat
<TypeConstant
> d_vars
;
100 HistogramStat
<Kind
> d_terms
;
103 /* -------------------------------------------------------------------------- */
105 /* -------------------------------------------------------------------------- */
107 /* Mapping from external (API) kind to internal kind. */
108 const static std::unordered_map
<Kind
, cvc5::Kind
> s_kinds
{
109 {INTERNAL_KIND
, cvc5::Kind::UNDEFINED_KIND
},
110 {UNDEFINED_KIND
, cvc5::Kind::UNDEFINED_KIND
},
111 {NULL_EXPR
, cvc5::Kind::NULL_EXPR
},
112 /* Builtin ------------------------------------------------------------- */
113 {UNINTERPRETED_SORT_VALUE
, cvc5::Kind::UNINTERPRETED_SORT_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 /* UF ------------------------------------------------------------------ */
130 {APPLY_UF
, cvc5::Kind::APPLY_UF
},
131 {CARDINALITY_CONSTRAINT
, cvc5::Kind::CARDINALITY_CONSTRAINT
},
132 {HO_APPLY
, cvc5::Kind::HO_APPLY
},
133 /* Arithmetic ---------------------------------------------------------- */
134 {ADD
, cvc5::Kind::ADD
},
135 {MULT
, cvc5::Kind::MULT
},
136 {IAND
, cvc5::Kind::IAND
},
137 {POW2
, cvc5::Kind::POW2
},
138 {SUB
, cvc5::Kind::SUB
},
139 {NEG
, cvc5::Kind::NEG
},
140 {DIVISION
, cvc5::Kind::DIVISION
},
141 {INTS_DIVISION
, cvc5::Kind::INTS_DIVISION
},
142 {INTS_MODULUS
, cvc5::Kind::INTS_MODULUS
},
143 {ABS
, cvc5::Kind::ABS
},
144 {DIVISIBLE
, cvc5::Kind::DIVISIBLE
},
145 {POW
, cvc5::Kind::POW
},
146 {EXPONENTIAL
, cvc5::Kind::EXPONENTIAL
},
147 {SINE
, cvc5::Kind::SINE
},
148 {COSINE
, cvc5::Kind::COSINE
},
149 {TANGENT
, cvc5::Kind::TANGENT
},
150 {COSECANT
, cvc5::Kind::COSECANT
},
151 {SECANT
, cvc5::Kind::SECANT
},
152 {COTANGENT
, cvc5::Kind::COTANGENT
},
153 {ARCSINE
, cvc5::Kind::ARCSINE
},
154 {ARCCOSINE
, cvc5::Kind::ARCCOSINE
},
155 {ARCTANGENT
, cvc5::Kind::ARCTANGENT
},
156 {ARCCOSECANT
, cvc5::Kind::ARCCOSECANT
},
157 {ARCSECANT
, cvc5::Kind::ARCSECANT
},
158 {ARCCOTANGENT
, cvc5::Kind::ARCCOTANGENT
},
159 {SQRT
, cvc5::Kind::SQRT
},
160 {CONST_RATIONAL
, cvc5::Kind::CONST_RATIONAL
},
161 {LT
, cvc5::Kind::LT
},
162 {LEQ
, cvc5::Kind::LEQ
},
163 {GT
, cvc5::Kind::GT
},
164 {GEQ
, cvc5::Kind::GEQ
},
165 {IS_INTEGER
, cvc5::Kind::IS_INTEGER
},
166 {TO_INTEGER
, cvc5::Kind::TO_INTEGER
},
167 {TO_REAL
, cvc5::Kind::TO_REAL
},
168 {PI
, cvc5::Kind::PI
},
169 /* BV ------------------------------------------------------------------ */
170 {CONST_BITVECTOR
, cvc5::Kind::CONST_BITVECTOR
},
171 {BITVECTOR_CONCAT
, cvc5::Kind::BITVECTOR_CONCAT
},
172 {BITVECTOR_AND
, cvc5::Kind::BITVECTOR_AND
},
173 {BITVECTOR_OR
, cvc5::Kind::BITVECTOR_OR
},
174 {BITVECTOR_XOR
, cvc5::Kind::BITVECTOR_XOR
},
175 {BITVECTOR_NOT
, cvc5::Kind::BITVECTOR_NOT
},
176 {BITVECTOR_NAND
, cvc5::Kind::BITVECTOR_NAND
},
177 {BITVECTOR_NOR
, cvc5::Kind::BITVECTOR_NOR
},
178 {BITVECTOR_XNOR
, cvc5::Kind::BITVECTOR_XNOR
},
179 {BITVECTOR_COMP
, cvc5::Kind::BITVECTOR_COMP
},
180 {BITVECTOR_MULT
, cvc5::Kind::BITVECTOR_MULT
},
181 {BITVECTOR_ADD
, cvc5::Kind::BITVECTOR_ADD
},
182 {BITVECTOR_SUB
, cvc5::Kind::BITVECTOR_SUB
},
183 {BITVECTOR_NEG
, cvc5::Kind::BITVECTOR_NEG
},
184 {BITVECTOR_UDIV
, cvc5::Kind::BITVECTOR_UDIV
},
185 {BITVECTOR_UREM
, cvc5::Kind::BITVECTOR_UREM
},
186 {BITVECTOR_SDIV
, cvc5::Kind::BITVECTOR_SDIV
},
187 {BITVECTOR_SREM
, cvc5::Kind::BITVECTOR_SREM
},
188 {BITVECTOR_SMOD
, cvc5::Kind::BITVECTOR_SMOD
},
189 {BITVECTOR_SHL
, cvc5::Kind::BITVECTOR_SHL
},
190 {BITVECTOR_LSHR
, cvc5::Kind::BITVECTOR_LSHR
},
191 {BITVECTOR_ASHR
, cvc5::Kind::BITVECTOR_ASHR
},
192 {BITVECTOR_ULT
, cvc5::Kind::BITVECTOR_ULT
},
193 {BITVECTOR_ULE
, cvc5::Kind::BITVECTOR_ULE
},
194 {BITVECTOR_UGT
, cvc5::Kind::BITVECTOR_UGT
},
195 {BITVECTOR_UGE
, cvc5::Kind::BITVECTOR_UGE
},
196 {BITVECTOR_SLT
, cvc5::Kind::BITVECTOR_SLT
},
197 {BITVECTOR_SLE
, cvc5::Kind::BITVECTOR_SLE
},
198 {BITVECTOR_SGT
, cvc5::Kind::BITVECTOR_SGT
},
199 {BITVECTOR_SGE
, cvc5::Kind::BITVECTOR_SGE
},
200 {BITVECTOR_ULTBV
, cvc5::Kind::BITVECTOR_ULTBV
},
201 {BITVECTOR_SLTBV
, cvc5::Kind::BITVECTOR_SLTBV
},
202 {BITVECTOR_ITE
, cvc5::Kind::BITVECTOR_ITE
},
203 {BITVECTOR_REDOR
, cvc5::Kind::BITVECTOR_REDOR
},
204 {BITVECTOR_REDAND
, cvc5::Kind::BITVECTOR_REDAND
},
205 {BITVECTOR_EXTRACT
, cvc5::Kind::BITVECTOR_EXTRACT
},
206 {BITVECTOR_REPEAT
, cvc5::Kind::BITVECTOR_REPEAT
},
207 {BITVECTOR_ZERO_EXTEND
, cvc5::Kind::BITVECTOR_ZERO_EXTEND
},
208 {BITVECTOR_SIGN_EXTEND
, cvc5::Kind::BITVECTOR_SIGN_EXTEND
},
209 {BITVECTOR_ROTATE_LEFT
, cvc5::Kind::BITVECTOR_ROTATE_LEFT
},
210 {BITVECTOR_ROTATE_RIGHT
, cvc5::Kind::BITVECTOR_ROTATE_RIGHT
},
211 {INT_TO_BITVECTOR
, cvc5::Kind::INT_TO_BITVECTOR
},
212 {BITVECTOR_TO_NAT
, cvc5::Kind::BITVECTOR_TO_NAT
},
213 /* FP ------------------------------------------------------------------ */
214 {CONST_FLOATINGPOINT
, cvc5::Kind::CONST_FLOATINGPOINT
},
215 {CONST_ROUNDINGMODE
, cvc5::Kind::CONST_ROUNDINGMODE
},
216 {FLOATINGPOINT_FP
, cvc5::Kind::FLOATINGPOINT_FP
},
217 {FLOATINGPOINT_EQ
, cvc5::Kind::FLOATINGPOINT_EQ
},
218 {FLOATINGPOINT_ABS
, cvc5::Kind::FLOATINGPOINT_ABS
},
219 {FLOATINGPOINT_NEG
, cvc5::Kind::FLOATINGPOINT_NEG
},
220 {FLOATINGPOINT_ADD
, cvc5::Kind::FLOATINGPOINT_ADD
},
221 {FLOATINGPOINT_SUB
, cvc5::Kind::FLOATINGPOINT_SUB
},
222 {FLOATINGPOINT_MULT
, cvc5::Kind::FLOATINGPOINT_MULT
},
223 {FLOATINGPOINT_DIV
, cvc5::Kind::FLOATINGPOINT_DIV
},
224 {FLOATINGPOINT_FMA
, cvc5::Kind::FLOATINGPOINT_FMA
},
225 {FLOATINGPOINT_SQRT
, cvc5::Kind::FLOATINGPOINT_SQRT
},
226 {FLOATINGPOINT_REM
, cvc5::Kind::FLOATINGPOINT_REM
},
227 {FLOATINGPOINT_RTI
, cvc5::Kind::FLOATINGPOINT_RTI
},
228 {FLOATINGPOINT_MIN
, cvc5::Kind::FLOATINGPOINT_MIN
},
229 {FLOATINGPOINT_MAX
, cvc5::Kind::FLOATINGPOINT_MAX
},
230 {FLOATINGPOINT_LEQ
, cvc5::Kind::FLOATINGPOINT_LEQ
},
231 {FLOATINGPOINT_LT
, cvc5::Kind::FLOATINGPOINT_LT
},
232 {FLOATINGPOINT_GEQ
, cvc5::Kind::FLOATINGPOINT_GEQ
},
233 {FLOATINGPOINT_GT
, cvc5::Kind::FLOATINGPOINT_GT
},
234 {FLOATINGPOINT_IS_NORMAL
, cvc5::Kind::FLOATINGPOINT_IS_NORMAL
},
235 {FLOATINGPOINT_IS_SUBNORMAL
, cvc5::Kind::FLOATINGPOINT_IS_SUBNORMAL
},
236 {FLOATINGPOINT_IS_ZERO
, cvc5::Kind::FLOATINGPOINT_IS_ZERO
},
237 {FLOATINGPOINT_IS_INF
, cvc5::Kind::FLOATINGPOINT_IS_INF
},
238 {FLOATINGPOINT_IS_NAN
, cvc5::Kind::FLOATINGPOINT_IS_NAN
},
239 {FLOATINGPOINT_IS_NEG
, cvc5::Kind::FLOATINGPOINT_IS_NEG
},
240 {FLOATINGPOINT_IS_POS
, cvc5::Kind::FLOATINGPOINT_IS_POS
},
241 {FLOATINGPOINT_TO_FP_FLOATINGPOINT
,
242 cvc5::Kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT
},
243 {FLOATINGPOINT_TO_FP_IEEE_BITVECTOR
,
244 cvc5::Kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR
},
245 {FLOATINGPOINT_TO_FP_REAL
, cvc5::Kind::FLOATINGPOINT_TO_FP_REAL
},
246 {FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR
,
247 cvc5::Kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR
},
248 {FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR
,
249 cvc5::Kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR
},
250 {FLOATINGPOINT_TO_FP_GENERIC
, cvc5::Kind::FLOATINGPOINT_TO_FP_GENERIC
},
251 {FLOATINGPOINT_TO_UBV
, cvc5::Kind::FLOATINGPOINT_TO_UBV
},
252 {FLOATINGPOINT_TO_SBV
, cvc5::Kind::FLOATINGPOINT_TO_SBV
},
253 {FLOATINGPOINT_TO_REAL
, cvc5::Kind::FLOATINGPOINT_TO_REAL
},
254 /* Arrays -------------------------------------------------------------- */
255 {SELECT
, cvc5::Kind::SELECT
},
256 {STORE
, cvc5::Kind::STORE
},
257 {CONST_ARRAY
, cvc5::Kind::STORE_ALL
},
258 {EQ_RANGE
, cvc5::Kind::EQ_RANGE
},
259 /* Datatypes ----------------------------------------------------------- */
260 {APPLY_SELECTOR
, cvc5::Kind::APPLY_SELECTOR
},
261 {APPLY_CONSTRUCTOR
, cvc5::Kind::APPLY_CONSTRUCTOR
},
262 {APPLY_TESTER
, cvc5::Kind::APPLY_TESTER
},
263 {APPLY_UPDATER
, cvc5::Kind::APPLY_UPDATER
},
264 {DT_SIZE
, cvc5::Kind::DT_SIZE
},
265 {MATCH
, cvc5::Kind::MATCH
},
266 {MATCH_CASE
, cvc5::Kind::MATCH_CASE
},
267 {MATCH_BIND_CASE
, cvc5::Kind::MATCH_BIND_CASE
},
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 {SET_EMPTY
, cvc5::Kind::SET_EMPTY
},
277 {SET_UNION
, cvc5::Kind::SET_UNION
},
278 {SET_INTER
, cvc5::Kind::SET_INTER
},
279 {SET_MINUS
, cvc5::Kind::SET_MINUS
},
280 {SET_SUBSET
, cvc5::Kind::SET_SUBSET
},
281 {SET_MEMBER
, cvc5::Kind::SET_MEMBER
},
282 {SET_SINGLETON
, cvc5::Kind::SET_SINGLETON
},
283 {SET_INSERT
, cvc5::Kind::SET_INSERT
},
284 {SET_CARD
, cvc5::Kind::SET_CARD
},
285 {SET_COMPLEMENT
, cvc5::Kind::SET_COMPLEMENT
},
286 {SET_UNIVERSE
, cvc5::Kind::SET_UNIVERSE
},
287 {SET_COMPREHENSION
, cvc5::Kind::SET_COMPREHENSION
},
288 {SET_CHOOSE
, cvc5::Kind::SET_CHOOSE
},
289 {SET_IS_SINGLETON
, cvc5::Kind::SET_IS_SINGLETON
},
290 {SET_MAP
, cvc5::Kind::SET_MAP
},
291 /* Relations ----------------------------------------------------------- */
292 {RELATION_JOIN
, cvc5::Kind::RELATION_JOIN
},
293 {RELATION_PRODUCT
, cvc5::Kind::RELATION_PRODUCT
},
294 {RELATION_TRANSPOSE
, cvc5::Kind::RELATION_TRANSPOSE
},
295 {RELATION_TCLOSURE
, cvc5::Kind::RELATION_TCLOSURE
},
296 {RELATION_JOIN_IMAGE
, cvc5::Kind::RELATION_JOIN_IMAGE
},
297 {RELATION_IDEN
, cvc5::Kind::RELATION_IDEN
},
298 /* Bags ---------------------------------------------------------------- */
299 {BAG_UNION_MAX
, cvc5::Kind::BAG_UNION_MAX
},
300 {BAG_UNION_DISJOINT
, cvc5::Kind::BAG_UNION_DISJOINT
},
301 {BAG_INTER_MIN
, cvc5::Kind::BAG_INTER_MIN
},
302 {BAG_DIFFERENCE_SUBTRACT
, cvc5::Kind::BAG_DIFFERENCE_SUBTRACT
},
303 {BAG_DIFFERENCE_REMOVE
, cvc5::Kind::BAG_DIFFERENCE_REMOVE
},
304 {BAG_SUBBAG
, cvc5::Kind::BAG_SUBBAG
},
305 {BAG_COUNT
, cvc5::Kind::BAG_COUNT
},
306 {BAG_MEMBER
, cvc5::Kind::BAG_MEMBER
},
307 {BAG_DUPLICATE_REMOVAL
, cvc5::Kind::BAG_DUPLICATE_REMOVAL
},
308 {BAG_MAKE
, cvc5::Kind::BAG_MAKE
},
309 {BAG_EMPTY
, cvc5::Kind::BAG_EMPTY
},
310 {BAG_CARD
, cvc5::Kind::BAG_CARD
},
311 {BAG_CHOOSE
, cvc5::Kind::BAG_CHOOSE
},
312 {BAG_IS_SINGLETON
, cvc5::Kind::BAG_IS_SINGLETON
},
313 {BAG_FROM_SET
, cvc5::Kind::BAG_FROM_SET
},
314 {BAG_TO_SET
, cvc5::Kind::BAG_TO_SET
},
315 {BAG_MAP
, cvc5::Kind::BAG_MAP
},
316 {BAG_FILTER
, cvc5::Kind::BAG_FILTER
},
317 {BAG_FOLD
, cvc5::Kind::BAG_FOLD
},
318 {TABLE_PRODUCT
, cvc5::Kind::TABLE_PRODUCT
},
319 /* Strings ------------------------------------------------------------- */
320 {STRING_CONCAT
, cvc5::Kind::STRING_CONCAT
},
321 {STRING_IN_REGEXP
, cvc5::Kind::STRING_IN_REGEXP
},
322 {STRING_LENGTH
, cvc5::Kind::STRING_LENGTH
},
323 {STRING_SUBSTR
, cvc5::Kind::STRING_SUBSTR
},
324 {STRING_UPDATE
, cvc5::Kind::STRING_UPDATE
},
325 {STRING_CHARAT
, cvc5::Kind::STRING_CHARAT
},
326 {STRING_CONTAINS
, cvc5::Kind::STRING_CONTAINS
},
327 {STRING_INDEXOF
, cvc5::Kind::STRING_INDEXOF
},
328 {STRING_INDEXOF_RE
, cvc5::Kind::STRING_INDEXOF_RE
},
329 {STRING_REPLACE
, cvc5::Kind::STRING_REPLACE
},
330 {STRING_REPLACE_ALL
, cvc5::Kind::STRING_REPLACE_ALL
},
331 {STRING_REPLACE_RE
, cvc5::Kind::STRING_REPLACE_RE
},
332 {STRING_REPLACE_RE_ALL
, cvc5::Kind::STRING_REPLACE_RE_ALL
},
333 {STRING_TOLOWER
, cvc5::Kind::STRING_TOLOWER
},
334 {STRING_TOUPPER
, cvc5::Kind::STRING_TOUPPER
},
335 {STRING_REV
, cvc5::Kind::STRING_REV
},
336 {STRING_FROM_CODE
, cvc5::Kind::STRING_FROM_CODE
},
337 {STRING_TO_CODE
, cvc5::Kind::STRING_TO_CODE
},
338 {STRING_LT
, cvc5::Kind::STRING_LT
},
339 {STRING_LEQ
, cvc5::Kind::STRING_LEQ
},
340 {STRING_PREFIX
, cvc5::Kind::STRING_PREFIX
},
341 {STRING_SUFFIX
, cvc5::Kind::STRING_SUFFIX
},
342 {STRING_IS_DIGIT
, cvc5::Kind::STRING_IS_DIGIT
},
343 {STRING_FROM_INT
, cvc5::Kind::STRING_ITOS
},
344 {STRING_TO_INT
, cvc5::Kind::STRING_STOI
},
345 {CONST_STRING
, cvc5::Kind::CONST_STRING
},
346 {STRING_TO_REGEXP
, cvc5::Kind::STRING_TO_REGEXP
},
347 {REGEXP_CONCAT
, cvc5::Kind::REGEXP_CONCAT
},
348 {REGEXP_UNION
, cvc5::Kind::REGEXP_UNION
},
349 {REGEXP_INTER
, cvc5::Kind::REGEXP_INTER
},
350 {REGEXP_DIFF
, cvc5::Kind::REGEXP_DIFF
},
351 {REGEXP_STAR
, cvc5::Kind::REGEXP_STAR
},
352 {REGEXP_PLUS
, cvc5::Kind::REGEXP_PLUS
},
353 {REGEXP_OPT
, cvc5::Kind::REGEXP_OPT
},
354 {REGEXP_RANGE
, cvc5::Kind::REGEXP_RANGE
},
355 {REGEXP_REPEAT
, cvc5::Kind::REGEXP_REPEAT
},
356 {REGEXP_LOOP
, cvc5::Kind::REGEXP_LOOP
},
357 {REGEXP_NONE
, cvc5::Kind::REGEXP_NONE
},
358 {REGEXP_ALL
, cvc5::Kind::REGEXP_ALL
},
359 {REGEXP_ALLCHAR
, cvc5::Kind::REGEXP_ALLCHAR
},
360 {REGEXP_COMPLEMENT
, cvc5::Kind::REGEXP_COMPLEMENT
},
361 // maps to the same kind as the string versions
362 {SEQ_CONCAT
, cvc5::Kind::STRING_CONCAT
},
363 {SEQ_LENGTH
, cvc5::Kind::STRING_LENGTH
},
364 {SEQ_EXTRACT
, cvc5::Kind::STRING_SUBSTR
},
365 {SEQ_UPDATE
, cvc5::Kind::STRING_UPDATE
},
366 {SEQ_AT
, cvc5::Kind::STRING_CHARAT
},
367 {SEQ_CONTAINS
, cvc5::Kind::STRING_CONTAINS
},
368 {SEQ_INDEXOF
, cvc5::Kind::STRING_INDEXOF
},
369 {SEQ_REPLACE
, cvc5::Kind::STRING_REPLACE
},
370 {SEQ_REPLACE_ALL
, cvc5::Kind::STRING_REPLACE_ALL
},
371 {SEQ_REV
, cvc5::Kind::STRING_REV
},
372 {SEQ_PREFIX
, cvc5::Kind::STRING_PREFIX
},
373 {SEQ_SUFFIX
, cvc5::Kind::STRING_SUFFIX
},
374 {CONST_SEQUENCE
, cvc5::Kind::CONST_SEQUENCE
},
375 {SEQ_UNIT
, cvc5::Kind::SEQ_UNIT
},
376 {SEQ_NTH
, cvc5::Kind::SEQ_NTH
},
377 /* Quantifiers --------------------------------------------------------- */
378 {FORALL
, cvc5::Kind::FORALL
},
379 {EXISTS
, cvc5::Kind::EXISTS
},
380 {VARIABLE_LIST
, cvc5::Kind::BOUND_VAR_LIST
},
381 {INST_PATTERN
, cvc5::Kind::INST_PATTERN
},
382 {INST_NO_PATTERN
, cvc5::Kind::INST_NO_PATTERN
},
383 {INST_POOL
, cvc5::Kind::INST_POOL
},
384 {INST_ADD_TO_POOL
, cvc5::Kind::INST_ADD_TO_POOL
},
385 {SKOLEM_ADD_TO_POOL
, cvc5::Kind::SKOLEM_ADD_TO_POOL
},
386 {INST_ATTRIBUTE
, cvc5::Kind::INST_ATTRIBUTE
},
387 {INST_PATTERN_LIST
, cvc5::Kind::INST_PATTERN_LIST
},
388 {LAST_KIND
, cvc5::Kind::LAST_KIND
},
391 /* Mapping from internal kind to external (API) kind. */
392 const static std::unordered_map
<cvc5::Kind
, Kind
, cvc5::kind::KindHashFunction
>
394 {cvc5::Kind::UNDEFINED_KIND
, UNDEFINED_KIND
},
395 {cvc5::Kind::NULL_EXPR
, NULL_EXPR
},
396 /* Builtin --------------------------------------------------------- */
397 {cvc5::Kind::UNINTERPRETED_SORT_VALUE
, UNINTERPRETED_SORT_VALUE
},
398 {cvc5::Kind::EQUAL
, EQUAL
},
399 {cvc5::Kind::DISTINCT
, DISTINCT
},
400 {cvc5::Kind::VARIABLE
, CONSTANT
},
401 {cvc5::Kind::BOUND_VARIABLE
, VARIABLE
},
402 {cvc5::Kind::SEXPR
, SEXPR
},
403 {cvc5::Kind::LAMBDA
, LAMBDA
},
404 {cvc5::Kind::WITNESS
, WITNESS
},
405 /* Boolean --------------------------------------------------------- */
406 {cvc5::Kind::CONST_BOOLEAN
, CONST_BOOLEAN
},
407 {cvc5::Kind::NOT
, NOT
},
408 {cvc5::Kind::AND
, AND
},
409 {cvc5::Kind::IMPLIES
, IMPLIES
},
410 {cvc5::Kind::OR
, OR
},
411 {cvc5::Kind::XOR
, XOR
},
412 {cvc5::Kind::ITE
, ITE
},
413 /* UF -------------------------------------------------------------- */
414 {cvc5::Kind::APPLY_UF
, APPLY_UF
},
415 {cvc5::Kind::CARDINALITY_CONSTRAINT
, CARDINALITY_CONSTRAINT
},
416 {cvc5::Kind::HO_APPLY
, HO_APPLY
},
417 /* Arithmetic ------------------------------------------------------ */
418 {cvc5::Kind::ADD
, ADD
},
419 {cvc5::Kind::MULT
, MULT
},
420 {cvc5::Kind::IAND
, IAND
},
421 {cvc5::Kind::POW2
, POW2
},
422 {cvc5::Kind::SUB
, SUB
},
423 {cvc5::Kind::NEG
, NEG
},
424 {cvc5::Kind::DIVISION
, DIVISION
},
425 {cvc5::Kind::DIVISION_TOTAL
, INTERNAL_KIND
},
426 {cvc5::Kind::INTS_DIVISION
, INTS_DIVISION
},
427 {cvc5::Kind::INTS_DIVISION_TOTAL
, INTERNAL_KIND
},
428 {cvc5::Kind::INTS_MODULUS
, INTS_MODULUS
},
429 {cvc5::Kind::INTS_MODULUS_TOTAL
, INTERNAL_KIND
},
430 {cvc5::Kind::ABS
, ABS
},
431 {cvc5::Kind::DIVISIBLE
, DIVISIBLE
},
432 {cvc5::Kind::POW
, POW
},
433 {cvc5::Kind::EXPONENTIAL
, EXPONENTIAL
},
434 {cvc5::Kind::SINE
, SINE
},
435 {cvc5::Kind::COSINE
, COSINE
},
436 {cvc5::Kind::TANGENT
, TANGENT
},
437 {cvc5::Kind::COSECANT
, COSECANT
},
438 {cvc5::Kind::SECANT
, SECANT
},
439 {cvc5::Kind::COTANGENT
, COTANGENT
},
440 {cvc5::Kind::ARCSINE
, ARCSINE
},
441 {cvc5::Kind::ARCCOSINE
, ARCCOSINE
},
442 {cvc5::Kind::ARCTANGENT
, ARCTANGENT
},
443 {cvc5::Kind::ARCCOSECANT
, ARCCOSECANT
},
444 {cvc5::Kind::ARCSECANT
, ARCSECANT
},
445 {cvc5::Kind::ARCCOTANGENT
, ARCCOTANGENT
},
446 {cvc5::Kind::SQRT
, SQRT
},
447 {cvc5::Kind::DIVISIBLE_OP
, DIVISIBLE
},
448 {cvc5::Kind::CONST_RATIONAL
, CONST_RATIONAL
},
449 {cvc5::Kind::LT
, LT
},
450 {cvc5::Kind::LEQ
, LEQ
},
451 {cvc5::Kind::GT
, GT
},
452 {cvc5::Kind::GEQ
, GEQ
},
453 {cvc5::Kind::IS_INTEGER
, IS_INTEGER
},
454 {cvc5::Kind::TO_INTEGER
, TO_INTEGER
},
455 {cvc5::Kind::TO_REAL
, TO_REAL
},
456 {cvc5::Kind::PI
, PI
},
457 {cvc5::Kind::IAND_OP
, IAND
},
458 /* BV -------------------------------------------------------------- */
459 {cvc5::Kind::CONST_BITVECTOR
, CONST_BITVECTOR
},
460 {cvc5::Kind::BITVECTOR_CONCAT
, BITVECTOR_CONCAT
},
461 {cvc5::Kind::BITVECTOR_AND
, BITVECTOR_AND
},
462 {cvc5::Kind::BITVECTOR_OR
, BITVECTOR_OR
},
463 {cvc5::Kind::BITVECTOR_XOR
, BITVECTOR_XOR
},
464 {cvc5::Kind::BITVECTOR_NOT
, BITVECTOR_NOT
},
465 {cvc5::Kind::BITVECTOR_NAND
, BITVECTOR_NAND
},
466 {cvc5::Kind::BITVECTOR_NOR
, BITVECTOR_NOR
},
467 {cvc5::Kind::BITVECTOR_XNOR
, BITVECTOR_XNOR
},
468 {cvc5::Kind::BITVECTOR_COMP
, BITVECTOR_COMP
},
469 {cvc5::Kind::BITVECTOR_MULT
, BITVECTOR_MULT
},
470 {cvc5::Kind::BITVECTOR_ADD
, BITVECTOR_ADD
},
471 {cvc5::Kind::BITVECTOR_SUB
, BITVECTOR_SUB
},
472 {cvc5::Kind::BITVECTOR_NEG
, BITVECTOR_NEG
},
473 {cvc5::Kind::BITVECTOR_UDIV
, BITVECTOR_UDIV
},
474 {cvc5::Kind::BITVECTOR_UREM
, BITVECTOR_UREM
},
475 {cvc5::Kind::BITVECTOR_SDIV
, BITVECTOR_SDIV
},
476 {cvc5::Kind::BITVECTOR_SREM
, BITVECTOR_SREM
},
477 {cvc5::Kind::BITVECTOR_SMOD
, BITVECTOR_SMOD
},
478 {cvc5::Kind::BITVECTOR_SHL
, BITVECTOR_SHL
},
479 {cvc5::Kind::BITVECTOR_LSHR
, BITVECTOR_LSHR
},
480 {cvc5::Kind::BITVECTOR_ASHR
, BITVECTOR_ASHR
},
481 {cvc5::Kind::BITVECTOR_ULT
, BITVECTOR_ULT
},
482 {cvc5::Kind::BITVECTOR_ULE
, BITVECTOR_ULE
},
483 {cvc5::Kind::BITVECTOR_UGT
, BITVECTOR_UGT
},
484 {cvc5::Kind::BITVECTOR_UGE
, BITVECTOR_UGE
},
485 {cvc5::Kind::BITVECTOR_SLT
, BITVECTOR_SLT
},
486 {cvc5::Kind::BITVECTOR_SLE
, BITVECTOR_SLE
},
487 {cvc5::Kind::BITVECTOR_SGT
, BITVECTOR_SGT
},
488 {cvc5::Kind::BITVECTOR_SGE
, BITVECTOR_SGE
},
489 {cvc5::Kind::BITVECTOR_ULTBV
, BITVECTOR_ULTBV
},
490 {cvc5::Kind::BITVECTOR_SLTBV
, BITVECTOR_SLTBV
},
491 {cvc5::Kind::BITVECTOR_ITE
, BITVECTOR_ITE
},
492 {cvc5::Kind::BITVECTOR_REDOR
, BITVECTOR_REDOR
},
493 {cvc5::Kind::BITVECTOR_REDAND
, BITVECTOR_REDAND
},
494 {cvc5::Kind::BITVECTOR_EXTRACT_OP
, BITVECTOR_EXTRACT
},
495 {cvc5::Kind::BITVECTOR_REPEAT_OP
, BITVECTOR_REPEAT
},
496 {cvc5::Kind::BITVECTOR_ZERO_EXTEND_OP
, BITVECTOR_ZERO_EXTEND
},
497 {cvc5::Kind::BITVECTOR_SIGN_EXTEND_OP
, BITVECTOR_SIGN_EXTEND
},
498 {cvc5::Kind::BITVECTOR_ROTATE_LEFT_OP
, BITVECTOR_ROTATE_LEFT
},
499 {cvc5::Kind::BITVECTOR_ROTATE_RIGHT_OP
, BITVECTOR_ROTATE_RIGHT
},
500 {cvc5::Kind::BITVECTOR_EXTRACT
, BITVECTOR_EXTRACT
},
501 {cvc5::Kind::BITVECTOR_REPEAT
, BITVECTOR_REPEAT
},
502 {cvc5::Kind::BITVECTOR_ZERO_EXTEND
, BITVECTOR_ZERO_EXTEND
},
503 {cvc5::Kind::BITVECTOR_SIGN_EXTEND
, BITVECTOR_SIGN_EXTEND
},
504 {cvc5::Kind::BITVECTOR_ROTATE_LEFT
, BITVECTOR_ROTATE_LEFT
},
505 {cvc5::Kind::BITVECTOR_ROTATE_RIGHT
, BITVECTOR_ROTATE_RIGHT
},
506 {cvc5::Kind::INT_TO_BITVECTOR_OP
, INT_TO_BITVECTOR
},
507 {cvc5::Kind::INT_TO_BITVECTOR
, INT_TO_BITVECTOR
},
508 {cvc5::Kind::BITVECTOR_TO_NAT
, BITVECTOR_TO_NAT
},
509 /* FP -------------------------------------------------------------- */
510 {cvc5::Kind::CONST_FLOATINGPOINT
, CONST_FLOATINGPOINT
},
511 {cvc5::Kind::CONST_ROUNDINGMODE
, CONST_ROUNDINGMODE
},
512 {cvc5::Kind::FLOATINGPOINT_FP
, FLOATINGPOINT_FP
},
513 {cvc5::Kind::FLOATINGPOINT_EQ
, FLOATINGPOINT_EQ
},
514 {cvc5::Kind::FLOATINGPOINT_ABS
, FLOATINGPOINT_ABS
},
515 {cvc5::Kind::FLOATINGPOINT_NEG
, FLOATINGPOINT_NEG
},
516 {cvc5::Kind::FLOATINGPOINT_ADD
, FLOATINGPOINT_ADD
},
517 {cvc5::Kind::FLOATINGPOINT_SUB
, FLOATINGPOINT_SUB
},
518 {cvc5::Kind::FLOATINGPOINT_MULT
, FLOATINGPOINT_MULT
},
519 {cvc5::Kind::FLOATINGPOINT_DIV
, FLOATINGPOINT_DIV
},
520 {cvc5::Kind::FLOATINGPOINT_FMA
, FLOATINGPOINT_FMA
},
521 {cvc5::Kind::FLOATINGPOINT_SQRT
, FLOATINGPOINT_SQRT
},
522 {cvc5::Kind::FLOATINGPOINT_REM
, FLOATINGPOINT_REM
},
523 {cvc5::Kind::FLOATINGPOINT_RTI
, FLOATINGPOINT_RTI
},
524 {cvc5::Kind::FLOATINGPOINT_MIN
, FLOATINGPOINT_MIN
},
525 {cvc5::Kind::FLOATINGPOINT_MAX
, FLOATINGPOINT_MAX
},
526 {cvc5::Kind::FLOATINGPOINT_LEQ
, FLOATINGPOINT_LEQ
},
527 {cvc5::Kind::FLOATINGPOINT_LT
, FLOATINGPOINT_LT
},
528 {cvc5::Kind::FLOATINGPOINT_GEQ
, FLOATINGPOINT_GEQ
},
529 {cvc5::Kind::FLOATINGPOINT_GT
, FLOATINGPOINT_GT
},
530 {cvc5::Kind::FLOATINGPOINT_IS_NORMAL
, FLOATINGPOINT_IS_NORMAL
},
531 {cvc5::Kind::FLOATINGPOINT_IS_SUBNORMAL
, FLOATINGPOINT_IS_SUBNORMAL
},
532 {cvc5::Kind::FLOATINGPOINT_IS_ZERO
, FLOATINGPOINT_IS_ZERO
},
533 {cvc5::Kind::FLOATINGPOINT_IS_INF
, FLOATINGPOINT_IS_INF
},
534 {cvc5::Kind::FLOATINGPOINT_IS_NAN
, FLOATINGPOINT_IS_NAN
},
535 {cvc5::Kind::FLOATINGPOINT_IS_NEG
, FLOATINGPOINT_IS_NEG
},
536 {cvc5::Kind::FLOATINGPOINT_IS_POS
, FLOATINGPOINT_IS_POS
},
537 {cvc5::Kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP
,
538 FLOATINGPOINT_TO_FP_IEEE_BITVECTOR
},
539 {cvc5::Kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR
,
540 FLOATINGPOINT_TO_FP_IEEE_BITVECTOR
},
541 {cvc5::Kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP
,
542 FLOATINGPOINT_TO_FP_FLOATINGPOINT
},
543 {cvc5::Kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT
,
544 FLOATINGPOINT_TO_FP_FLOATINGPOINT
},
545 {cvc5::Kind::FLOATINGPOINT_TO_FP_REAL_OP
, FLOATINGPOINT_TO_FP_REAL
},
546 {cvc5::Kind::FLOATINGPOINT_TO_FP_REAL
, FLOATINGPOINT_TO_FP_REAL
},
547 {cvc5::Kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP
,
548 FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR
},
549 {cvc5::Kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR
,
550 FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR
},
551 {cvc5::Kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP
,
552 FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR
},
553 {cvc5::Kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR
,
554 FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR
},
555 {cvc5::Kind::FLOATINGPOINT_TO_FP_GENERIC_OP
,
556 FLOATINGPOINT_TO_FP_GENERIC
},
557 {cvc5::Kind::FLOATINGPOINT_TO_FP_GENERIC
, FLOATINGPOINT_TO_FP_GENERIC
},
558 {cvc5::Kind::FLOATINGPOINT_TO_UBV_OP
, FLOATINGPOINT_TO_UBV
},
559 {cvc5::Kind::FLOATINGPOINT_TO_UBV
, FLOATINGPOINT_TO_UBV
},
560 {cvc5::Kind::FLOATINGPOINT_TO_UBV_TOTAL_OP
, INTERNAL_KIND
},
561 {cvc5::Kind::FLOATINGPOINT_TO_UBV_TOTAL
, INTERNAL_KIND
},
562 {cvc5::Kind::FLOATINGPOINT_TO_SBV_OP
, FLOATINGPOINT_TO_SBV
},
563 {cvc5::Kind::FLOATINGPOINT_TO_SBV
, FLOATINGPOINT_TO_SBV
},
564 {cvc5::Kind::FLOATINGPOINT_TO_SBV_TOTAL_OP
, INTERNAL_KIND
},
565 {cvc5::Kind::FLOATINGPOINT_TO_SBV_TOTAL
, INTERNAL_KIND
},
566 {cvc5::Kind::FLOATINGPOINT_TO_REAL
, FLOATINGPOINT_TO_REAL
},
567 {cvc5::Kind::FLOATINGPOINT_TO_REAL_TOTAL
, INTERNAL_KIND
},
568 /* Arrays ---------------------------------------------------------- */
569 {cvc5::Kind::SELECT
, SELECT
},
570 {cvc5::Kind::STORE
, STORE
},
571 {cvc5::Kind::STORE_ALL
, CONST_ARRAY
},
572 /* Datatypes ------------------------------------------------------- */
573 {cvc5::Kind::APPLY_SELECTOR
, APPLY_SELECTOR
},
574 {cvc5::Kind::APPLY_CONSTRUCTOR
, APPLY_CONSTRUCTOR
},
575 {cvc5::Kind::APPLY_TESTER
, APPLY_TESTER
},
576 {cvc5::Kind::APPLY_UPDATER
, APPLY_UPDATER
},
577 {cvc5::Kind::DT_SIZE
, DT_SIZE
},
578 {cvc5::Kind::MATCH
, MATCH
},
579 {cvc5::Kind::MATCH_CASE
, MATCH_CASE
},
580 {cvc5::Kind::MATCH_BIND_CASE
, MATCH_BIND_CASE
},
581 {cvc5::Kind::TUPLE_PROJECT
, TUPLE_PROJECT
},
582 {cvc5::Kind::TUPLE_PROJECT_OP
, TUPLE_PROJECT
},
583 /* Separation Logic ------------------------------------------------ */
584 {cvc5::Kind::SEP_NIL
, SEP_NIL
},
585 {cvc5::Kind::SEP_EMP
, SEP_EMP
},
586 {cvc5::Kind::SEP_PTO
, SEP_PTO
},
587 {cvc5::Kind::SEP_STAR
, SEP_STAR
},
588 {cvc5::Kind::SEP_WAND
, SEP_WAND
},
589 /* Sets ------------------------------------------------------------ */
590 {cvc5::Kind::SET_EMPTY
, SET_EMPTY
},
591 {cvc5::Kind::SET_UNION
, SET_UNION
},
592 {cvc5::Kind::SET_INTER
, SET_INTER
},
593 {cvc5::Kind::SET_MINUS
, SET_MINUS
},
594 {cvc5::Kind::SET_SUBSET
, SET_SUBSET
},
595 {cvc5::Kind::SET_MEMBER
, SET_MEMBER
},
596 {cvc5::Kind::SET_SINGLETON
, SET_SINGLETON
},
597 {cvc5::Kind::SET_INSERT
, SET_INSERT
},
598 {cvc5::Kind::SET_CARD
, SET_CARD
},
599 {cvc5::Kind::SET_COMPLEMENT
, SET_COMPLEMENT
},
600 {cvc5::Kind::SET_UNIVERSE
, SET_UNIVERSE
},
601 {cvc5::Kind::SET_COMPREHENSION
, SET_COMPREHENSION
},
602 {cvc5::Kind::SET_CHOOSE
, SET_CHOOSE
},
603 {cvc5::Kind::SET_IS_SINGLETON
, SET_IS_SINGLETON
},
604 {cvc5::Kind::SET_MAP
, SET_MAP
},
605 /* Relations ------------------------------------------------------- */
606 {cvc5::Kind::RELATION_JOIN
, RELATION_JOIN
},
607 {cvc5::Kind::RELATION_PRODUCT
, RELATION_PRODUCT
},
608 {cvc5::Kind::RELATION_TRANSPOSE
, RELATION_TRANSPOSE
},
609 {cvc5::Kind::RELATION_TCLOSURE
, RELATION_TCLOSURE
},
610 {cvc5::Kind::RELATION_JOIN_IMAGE
, RELATION_JOIN_IMAGE
},
611 {cvc5::Kind::RELATION_IDEN
, RELATION_IDEN
},
612 /* Bags ------------------------------------------------------------ */
613 {cvc5::Kind::BAG_UNION_MAX
, BAG_UNION_MAX
},
614 {cvc5::Kind::BAG_UNION_DISJOINT
, BAG_UNION_DISJOINT
},
615 {cvc5::Kind::BAG_INTER_MIN
, BAG_INTER_MIN
},
616 {cvc5::Kind::BAG_DIFFERENCE_SUBTRACT
, BAG_DIFFERENCE_SUBTRACT
},
617 {cvc5::Kind::BAG_DIFFERENCE_REMOVE
, BAG_DIFFERENCE_REMOVE
},
618 {cvc5::Kind::BAG_SUBBAG
, BAG_SUBBAG
},
619 {cvc5::Kind::BAG_COUNT
, BAG_COUNT
},
620 {cvc5::Kind::BAG_MEMBER
, BAG_MEMBER
},
621 {cvc5::Kind::BAG_DUPLICATE_REMOVAL
, BAG_DUPLICATE_REMOVAL
},
622 {cvc5::Kind::BAG_MAKE
, BAG_MAKE
},
623 {cvc5::Kind::BAG_EMPTY
, BAG_EMPTY
},
624 {cvc5::Kind::BAG_CARD
, BAG_CARD
},
625 {cvc5::Kind::BAG_CHOOSE
, BAG_CHOOSE
},
626 {cvc5::Kind::BAG_IS_SINGLETON
, BAG_IS_SINGLETON
},
627 {cvc5::Kind::BAG_FROM_SET
, BAG_FROM_SET
},
628 {cvc5::Kind::BAG_TO_SET
, BAG_TO_SET
},
629 {cvc5::Kind::BAG_MAP
, BAG_MAP
},
630 {cvc5::Kind::BAG_FILTER
, BAG_FILTER
},
631 {cvc5::Kind::BAG_FOLD
, BAG_FOLD
},
632 {cvc5::Kind::TABLE_PRODUCT
, TABLE_PRODUCT
},
633 /* Strings --------------------------------------------------------- */
634 {cvc5::Kind::STRING_CONCAT
, STRING_CONCAT
},
635 {cvc5::Kind::STRING_IN_REGEXP
, STRING_IN_REGEXP
},
636 {cvc5::Kind::STRING_LENGTH
, STRING_LENGTH
},
637 {cvc5::Kind::STRING_SUBSTR
, STRING_SUBSTR
},
638 {cvc5::Kind::STRING_UPDATE
, STRING_UPDATE
},
639 {cvc5::Kind::STRING_CHARAT
, STRING_CHARAT
},
640 {cvc5::Kind::STRING_CONTAINS
, STRING_CONTAINS
},
641 {cvc5::Kind::STRING_INDEXOF
, STRING_INDEXOF
},
642 {cvc5::Kind::STRING_INDEXOF_RE
, STRING_INDEXOF_RE
},
643 {cvc5::Kind::STRING_REPLACE
, STRING_REPLACE
},
644 {cvc5::Kind::STRING_REPLACE_ALL
, STRING_REPLACE_ALL
},
645 {cvc5::Kind::STRING_REPLACE_RE
, STRING_REPLACE_RE
},
646 {cvc5::Kind::STRING_REPLACE_RE_ALL
, STRING_REPLACE_RE_ALL
},
647 {cvc5::Kind::STRING_TOLOWER
, STRING_TOLOWER
},
648 {cvc5::Kind::STRING_TOUPPER
, STRING_TOUPPER
},
649 {cvc5::Kind::STRING_REV
, STRING_REV
},
650 {cvc5::Kind::STRING_FROM_CODE
, STRING_FROM_CODE
},
651 {cvc5::Kind::STRING_TO_CODE
, STRING_TO_CODE
},
652 {cvc5::Kind::STRING_LT
, STRING_LT
},
653 {cvc5::Kind::STRING_LEQ
, STRING_LEQ
},
654 {cvc5::Kind::STRING_PREFIX
, STRING_PREFIX
},
655 {cvc5::Kind::STRING_SUFFIX
, STRING_SUFFIX
},
656 {cvc5::Kind::STRING_IS_DIGIT
, STRING_IS_DIGIT
},
657 {cvc5::Kind::STRING_ITOS
, STRING_FROM_INT
},
658 {cvc5::Kind::STRING_STOI
, STRING_TO_INT
},
659 {cvc5::Kind::CONST_STRING
, CONST_STRING
},
660 {cvc5::Kind::STRING_TO_REGEXP
, STRING_TO_REGEXP
},
661 {cvc5::Kind::REGEXP_CONCAT
, REGEXP_CONCAT
},
662 {cvc5::Kind::REGEXP_UNION
, REGEXP_UNION
},
663 {cvc5::Kind::REGEXP_INTER
, REGEXP_INTER
},
664 {cvc5::Kind::REGEXP_DIFF
, REGEXP_DIFF
},
665 {cvc5::Kind::REGEXP_STAR
, REGEXP_STAR
},
666 {cvc5::Kind::REGEXP_PLUS
, REGEXP_PLUS
},
667 {cvc5::Kind::REGEXP_OPT
, REGEXP_OPT
},
668 {cvc5::Kind::REGEXP_RANGE
, REGEXP_RANGE
},
669 {cvc5::Kind::REGEXP_REPEAT
, REGEXP_REPEAT
},
670 {cvc5::Kind::REGEXP_REPEAT_OP
, REGEXP_REPEAT
},
671 {cvc5::Kind::REGEXP_LOOP
, REGEXP_LOOP
},
672 {cvc5::Kind::REGEXP_LOOP_OP
, REGEXP_LOOP
},
673 {cvc5::Kind::REGEXP_NONE
, REGEXP_NONE
},
674 {cvc5::Kind::REGEXP_ALL
, REGEXP_ALL
},
675 {cvc5::Kind::REGEXP_ALLCHAR
, REGEXP_ALLCHAR
},
676 {cvc5::Kind::REGEXP_COMPLEMENT
, REGEXP_COMPLEMENT
},
677 {cvc5::Kind::CONST_SEQUENCE
, CONST_SEQUENCE
},
678 {cvc5::Kind::SEQ_UNIT
, SEQ_UNIT
},
679 {cvc5::Kind::SEQ_NTH
, SEQ_NTH
},
680 /* Quantifiers ----------------------------------------------------- */
681 {cvc5::Kind::FORALL
, FORALL
},
682 {cvc5::Kind::EXISTS
, EXISTS
},
683 {cvc5::Kind::BOUND_VAR_LIST
, VARIABLE_LIST
},
684 {cvc5::Kind::INST_PATTERN
, INST_PATTERN
},
685 {cvc5::Kind::INST_NO_PATTERN
, INST_NO_PATTERN
},
686 {cvc5::Kind::INST_POOL
, INST_POOL
},
687 {cvc5::Kind::INST_ADD_TO_POOL
, INST_ADD_TO_POOL
},
688 {cvc5::Kind::SKOLEM_ADD_TO_POOL
, SKOLEM_ADD_TO_POOL
},
689 {cvc5::Kind::INST_ATTRIBUTE
, INST_ATTRIBUTE
},
690 {cvc5::Kind::INST_PATTERN_LIST
, INST_PATTERN_LIST
},
691 /* ----------------------------------------------------------------- */
692 {cvc5::Kind::LAST_KIND
, LAST_KIND
},
695 /* Set of kinds for indexed operators */
696 const static std::unordered_set
<Kind
> s_indexed_kinds(
700 BITVECTOR_ZERO_EXTEND
,
701 BITVECTOR_SIGN_EXTEND
,
702 BITVECTOR_ROTATE_LEFT
,
703 BITVECTOR_ROTATE_RIGHT
,
705 FLOATINGPOINT_TO_UBV
,
706 FLOATINGPOINT_TO_SBV
,
708 FLOATINGPOINT_TO_FP_IEEE_BITVECTOR
,
709 FLOATINGPOINT_TO_FP_FLOATINGPOINT
,
710 FLOATINGPOINT_TO_FP_REAL
,
711 FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR
,
712 FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR
,
713 FLOATINGPOINT_TO_FP_GENERIC
});
717 /** Convert a cvc5::Kind (internal) to a cvc5::api::Kind (external). */
718 cvc5::api::Kind
intToExtKind(cvc5::Kind k
)
720 auto it
= api::s_kinds_internal
.find(k
);
721 if (it
== api::s_kinds_internal
.end())
723 return api::INTERNAL_KIND
;
728 /** Convert a cvc5::api::Kind (external) to a cvc5::Kind (internal). */
729 cvc5::Kind
extToIntKind(cvc5::api::Kind k
)
731 auto it
= api::s_kinds
.find(k
);
732 if (it
== api::s_kinds
.end())
734 return cvc5::Kind::UNDEFINED_KIND
;
739 /** Return true if given kind is a defined external kind. */
740 bool isDefinedKind(Kind k
) { return k
> UNDEFINED_KIND
&& k
< LAST_KIND
; }
743 * Return true if the internal kind is one where the API term structure
744 * differs from internal structure. This happens for APPLY_* kinds.
745 * The API takes a "higher-order" perspective and treats functions as well
746 * as datatype constructors/selectors/testers as terms
747 * but interally they are not
749 bool isApplyKind(cvc5::Kind k
)
751 return (k
== cvc5::Kind::APPLY_UF
|| k
== cvc5::Kind::APPLY_CONSTRUCTOR
752 || k
== cvc5::Kind::APPLY_SELECTOR
|| k
== cvc5::Kind::APPLY_TESTER
753 || k
== cvc5::Kind::APPLY_UPDATER
);
756 #ifdef CVC5_ASSERTIONS
757 /** Return true if given kind is a defined internal kind. */
758 bool isDefinedIntKind(cvc5::Kind k
)
760 return k
!= cvc5::Kind::UNDEFINED_KIND
&& k
!= cvc5::Kind::LAST_KIND
;
764 /** Return the minimum arity of given kind. */
765 uint32_t minArity(Kind k
)
767 Assert(isDefinedKind(k
));
768 Assert(isDefinedIntKind(extToIntKind(k
)));
769 uint32_t min
= cvc5::kind::metakind::getMinArityForKind(extToIntKind(k
));
771 // At the API level, we treat functions/constructors/selectors/testers as
772 // normal terms instead of making them part of the operator
773 if (isApplyKind(extToIntKind(k
)))
780 /** Return the maximum arity of given kind. */
781 uint32_t maxArity(Kind k
)
783 Assert(isDefinedKind(k
));
784 Assert(isDefinedIntKind(extToIntKind(k
)));
785 uint32_t max
= cvc5::kind::metakind::getMaxArityForKind(extToIntKind(k
));
787 // At the API level, we treat functions/constructors/selectors/testers as
788 // normal terms instead of making them part of the operator
789 if (isApplyKind(extToIntKind(k
))
790 && max
!= std::numeric_limits
<uint32_t>::max()) // be careful not to
800 std::string
kindToString(Kind k
)
802 return k
== INTERNAL_KIND
? "INTERNAL_KIND"
803 : cvc5::kind::kindToString(extToIntKind(k
));
806 const char* toString(Kind k
)
808 return k
== INTERNAL_KIND
? "INTERNAL_KIND"
809 : cvc5::kind::toString(extToIntKind(k
));
812 std::ostream
& operator<<(std::ostream
& out
, Kind k
)
816 case INTERNAL_KIND
: out
<< "INTERNAL_KIND"; break;
817 default: out
<< extToIntKind(k
);
822 /* -------------------------------------------------------------------------- */
823 /* API guard helpers */
824 /* -------------------------------------------------------------------------- */
828 class CVC5ApiExceptionStream
831 CVC5ApiExceptionStream() {}
832 /* Note: This needs to be explicitly set to 'noexcept(false)' since it is
833 * a destructor that throws an exception and in C++11 all destructors
834 * default to noexcept(true) (else this triggers a call to std::terminate). */
835 ~CVC5ApiExceptionStream() noexcept(false)
837 if (std::uncaught_exceptions() == 0)
839 throw CVC5ApiException(d_stream
.str());
843 std::ostream
& ostream() { return d_stream
; }
846 std::stringstream d_stream
;
849 class CVC5ApiRecoverableExceptionStream
852 CVC5ApiRecoverableExceptionStream() {}
853 /* Note: This needs to be explicitly set to 'noexcept(false)' since it is
854 * a destructor that throws an exception and in C++11 all destructors
855 * default to noexcept(true) (else this triggers a call to std::terminate). */
856 ~CVC5ApiRecoverableExceptionStream() noexcept(false)
858 if (std::uncaught_exceptions() == 0)
860 throw CVC5ApiRecoverableException(d_stream
.str());
864 std::ostream
& ostream() { return d_stream
; }
867 std::stringstream d_stream
;
870 class CVC5ApiUnsupportedExceptionStream
873 CVC5ApiUnsupportedExceptionStream() {}
874 /* Note: This needs to be explicitly set to 'noexcept(false)' since it is
875 * a destructor that throws an exception and in C++11 all destructors
876 * default to noexcept(true) (else this triggers a call to std::terminate). */
877 ~CVC5ApiUnsupportedExceptionStream() noexcept(false)
879 if (std::uncaught_exceptions() == 0)
881 throw CVC5ApiUnsupportedException(d_stream
.str());
885 std::ostream
& ostream() { return d_stream
; }
888 std::stringstream d_stream
;
891 #define CVC5_API_TRY_CATCH_BEGIN \
894 #define CVC5_API_TRY_CATCH_END \
896 catch (const OptionException& e) \
898 throw CVC5ApiOptionException(e.getMessage()); \
900 catch (const cvc5::RecoverableModalException& e) \
902 throw CVC5ApiRecoverableException(e.getMessage()); \
904 catch (const cvc5::Exception& e) { throw CVC5ApiException(e.getMessage()); } \
905 catch (const std::invalid_argument& e) { throw CVC5ApiException(e.what()); }
909 /* -------------------------------------------------------------------------- */
911 /* -------------------------------------------------------------------------- */
913 Result::Result(const cvc5::Result
& r
) : d_result(new cvc5::Result(r
)) {}
915 Result::Result() : d_result(new cvc5::Result()) {}
917 bool Result::isNull() const
919 return d_result
->getType() == cvc5::Result::TYPE_NONE
;
922 bool Result::isSat(void) const
924 return d_result
->getType() == cvc5::Result::TYPE_SAT
925 && d_result
->isSat() == cvc5::Result::SAT
;
928 bool Result::isUnsat(void) const
930 return d_result
->getType() == cvc5::Result::TYPE_SAT
931 && d_result
->isSat() == cvc5::Result::UNSAT
;
934 bool Result::isSatUnknown(void) const
936 return d_result
->getType() == cvc5::Result::TYPE_SAT
937 && d_result
->isSat() == cvc5::Result::SAT_UNKNOWN
;
940 bool Result::isEntailed(void) const
942 return d_result
->getType() == cvc5::Result::TYPE_ENTAILMENT
943 && d_result
->isEntailed() == cvc5::Result::ENTAILED
;
946 bool Result::isNotEntailed(void) const
948 return d_result
->getType() == cvc5::Result::TYPE_ENTAILMENT
949 && d_result
->isEntailed() == cvc5::Result::NOT_ENTAILED
;
952 bool Result::isEntailmentUnknown(void) const
954 return d_result
->getType() == cvc5::Result::TYPE_ENTAILMENT
955 && d_result
->isEntailed() == cvc5::Result::ENTAILMENT_UNKNOWN
;
958 bool Result::operator==(const Result
& r
) const
960 return *d_result
== *r
.d_result
;
963 bool Result::operator!=(const Result
& r
) const
965 return *d_result
!= *r
.d_result
;
968 Result::UnknownExplanation
Result::getUnknownExplanation(void) const
970 cvc5::Result::UnknownExplanation expl
= d_result
->whyUnknown();
973 case cvc5::Result::REQUIRES_FULL_CHECK
: return REQUIRES_FULL_CHECK
;
974 case cvc5::Result::INCOMPLETE
: return INCOMPLETE
;
975 case cvc5::Result::TIMEOUT
: return TIMEOUT
;
976 case cvc5::Result::RESOURCEOUT
: return RESOURCEOUT
;
977 case cvc5::Result::MEMOUT
: return MEMOUT
;
978 case cvc5::Result::INTERRUPTED
: return INTERRUPTED
;
979 case cvc5::Result::NO_STATUS
: return NO_STATUS
;
980 case cvc5::Result::UNSUPPORTED
: return UNSUPPORTED
;
981 case cvc5::Result::OTHER
: return OTHER
;
982 default: return UNKNOWN_REASON
;
984 return UNKNOWN_REASON
;
987 std::string
Result::toString(void) const { return d_result
->toString(); }
989 std::ostream
& operator<<(std::ostream
& out
, const Result
& r
)
995 std::ostream
& operator<<(std::ostream
& out
, enum Result::UnknownExplanation e
)
999 case Result::REQUIRES_FULL_CHECK
: out
<< "REQUIRES_FULL_CHECK"; break;
1000 case Result::INCOMPLETE
: out
<< "INCOMPLETE"; break;
1001 case Result::TIMEOUT
: out
<< "TIMEOUT"; break;
1002 case Result::RESOURCEOUT
: out
<< "RESOURCEOUT"; break;
1003 case Result::MEMOUT
: out
<< "MEMOUT"; break;
1004 case Result::INTERRUPTED
: out
<< "INTERRUPTED"; break;
1005 case Result::NO_STATUS
: out
<< "NO_STATUS"; break;
1006 case Result::UNSUPPORTED
: out
<< "UNSUPPORTED"; break;
1007 case Result::OTHER
: out
<< "OTHER"; break;
1008 case Result::UNKNOWN_REASON
: out
<< "UNKNOWN_REASON"; break;
1009 default: Unhandled() << e
;
1014 /* -------------------------------------------------------------------------- */
1016 /* -------------------------------------------------------------------------- */
1018 Sort::Sort(const Solver
* slv
, const cvc5::TypeNode
& t
)
1019 : d_solver(slv
), d_type(new cvc5::TypeNode(t
))
1023 Sort::Sort() : d_solver(nullptr), d_type(new cvc5::TypeNode()) {}
1027 if (d_solver
!= nullptr)
1033 std::set
<TypeNode
> Sort::sortSetToTypeNodes(const std::set
<Sort
>& sorts
)
1035 std::set
<TypeNode
> types
;
1036 for (const Sort
& s
: sorts
)
1038 types
.insert(s
.getTypeNode());
1043 std::vector
<TypeNode
> Sort::sortVectorToTypeNodes(
1044 const std::vector
<Sort
>& sorts
)
1046 std::vector
<TypeNode
> typeNodes
;
1047 for (const Sort
& sort
: sorts
)
1049 typeNodes
.push_back(sort
.getTypeNode());
1054 std::vector
<Sort
> Sort::typeNodeVectorToSorts(
1055 const Solver
* slv
, const std::vector
<TypeNode
>& types
)
1057 std::vector
<Sort
> sorts
;
1058 for (size_t i
= 0, tsize
= types
.size(); i
< tsize
; i
++)
1060 sorts
.push_back(Sort(slv
, types
[i
]));
1065 bool Sort::operator==(const Sort
& s
) const
1067 CVC5_API_TRY_CATCH_BEGIN
;
1068 //////// all checks before this line
1069 return *d_type
== *s
.d_type
;
1071 CVC5_API_TRY_CATCH_END
;
1074 bool Sort::operator!=(const Sort
& s
) const
1076 CVC5_API_TRY_CATCH_BEGIN
;
1077 //////// all checks before this line
1078 return *d_type
!= *s
.d_type
;
1080 CVC5_API_TRY_CATCH_END
;
1083 bool Sort::operator<(const Sort
& s
) const
1085 CVC5_API_TRY_CATCH_BEGIN
;
1086 //////// all checks before this line
1087 return *d_type
< *s
.d_type
;
1089 CVC5_API_TRY_CATCH_END
;
1092 bool Sort::operator>(const Sort
& s
) const
1094 CVC5_API_TRY_CATCH_BEGIN
;
1095 //////// all checks before this line
1096 return *d_type
> *s
.d_type
;
1098 CVC5_API_TRY_CATCH_END
;
1101 bool Sort::operator<=(const Sort
& s
) const
1103 CVC5_API_TRY_CATCH_BEGIN
;
1104 //////// all checks before this line
1105 return *d_type
<= *s
.d_type
;
1107 CVC5_API_TRY_CATCH_END
;
1110 bool Sort::operator>=(const Sort
& s
) const
1112 CVC5_API_TRY_CATCH_BEGIN
;
1113 //////// all checks before this line
1114 return *d_type
>= *s
.d_type
;
1116 CVC5_API_TRY_CATCH_END
;
1119 bool Sort::hasSymbol() const
1121 CVC5_API_TRY_CATCH_BEGIN
;
1122 CVC5_API_CHECK_NOT_NULL
;
1123 //////// all checks before this line
1124 return d_type
->hasAttribute(expr::VarNameAttr());
1126 CVC5_API_TRY_CATCH_END
;
1129 std::string
Sort::getSymbol() const
1131 CVC5_API_TRY_CATCH_BEGIN
;
1132 CVC5_API_CHECK_NOT_NULL
;
1133 CVC5_API_CHECK(d_type
->hasAttribute(expr::VarNameAttr()))
1134 << "Invalid call to '" << __PRETTY_FUNCTION__
1135 << "', expected the sort to have a symbol.";
1136 //////// all checks before this line
1137 return d_type
->getAttribute(expr::VarNameAttr());
1139 CVC5_API_TRY_CATCH_END
;
1142 bool Sort::isNull() const
1144 CVC5_API_TRY_CATCH_BEGIN
;
1145 //////// all checks before this line
1146 return isNullHelper();
1148 CVC5_API_TRY_CATCH_END
;
1151 bool Sort::isBoolean() const
1153 CVC5_API_TRY_CATCH_BEGIN
;
1154 //////// all checks before this line
1155 return d_type
->isBoolean();
1157 CVC5_API_TRY_CATCH_END
;
1160 bool Sort::isInteger() const
1162 CVC5_API_TRY_CATCH_BEGIN
;
1163 //////// all checks before this line
1164 return d_type
->isInteger();
1166 CVC5_API_TRY_CATCH_END
;
1169 bool Sort::isReal() const
1171 CVC5_API_TRY_CATCH_BEGIN
;
1172 //////// all checks before this line
1173 // notice that we do not expose internal subtyping to the user
1174 return d_type
->isReal() && !d_type
->isInteger();
1176 CVC5_API_TRY_CATCH_END
;
1179 bool Sort::isString() const
1181 CVC5_API_TRY_CATCH_BEGIN
;
1182 //////// all checks before this line
1183 return d_type
->isString();
1185 CVC5_API_TRY_CATCH_END
;
1188 bool Sort::isRegExp() const
1190 CVC5_API_TRY_CATCH_BEGIN
;
1191 //////// all checks before this line
1192 return d_type
->isRegExp();
1194 CVC5_API_TRY_CATCH_END
;
1197 bool Sort::isRoundingMode() const
1199 CVC5_API_TRY_CATCH_BEGIN
;
1200 //////// all checks before this line
1201 return d_type
->isRoundingMode();
1203 CVC5_API_TRY_CATCH_END
;
1206 bool Sort::isBitVector() const
1208 CVC5_API_TRY_CATCH_BEGIN
;
1209 //////// all checks before this line
1210 return d_type
->isBitVector();
1212 CVC5_API_TRY_CATCH_END
;
1215 bool Sort::isFloatingPoint() const
1217 CVC5_API_TRY_CATCH_BEGIN
;
1218 //////// all checks before this line
1219 return d_type
->isFloatingPoint();
1221 CVC5_API_TRY_CATCH_END
;
1224 bool Sort::isDatatype() const
1226 CVC5_API_TRY_CATCH_BEGIN
;
1227 //////// all checks before this line
1228 return d_type
->isDatatype();
1230 CVC5_API_TRY_CATCH_END
;
1233 bool Sort::isParametricDatatype() const
1235 CVC5_API_TRY_CATCH_BEGIN
;
1236 //////// all checks before this line
1237 if (!d_type
->isDatatype()) return false;
1238 return d_type
->isParametricDatatype();
1240 CVC5_API_TRY_CATCH_END
;
1243 bool Sort::isConstructor() const
1245 CVC5_API_TRY_CATCH_BEGIN
;
1246 //////// all checks before this line
1247 return d_type
->isConstructor();
1249 CVC5_API_TRY_CATCH_END
;
1252 bool Sort::isSelector() const
1254 CVC5_API_TRY_CATCH_BEGIN
;
1255 //////// all checks before this line
1256 return d_type
->isSelector();
1258 CVC5_API_TRY_CATCH_END
;
1261 bool Sort::isTester() const
1263 CVC5_API_TRY_CATCH_BEGIN
;
1264 //////// all checks before this line
1265 return d_type
->isTester();
1267 CVC5_API_TRY_CATCH_END
;
1270 bool Sort::isUpdater() const
1272 CVC5_API_TRY_CATCH_BEGIN
;
1273 //////// all checks before this line
1274 return d_type
->isUpdater();
1276 CVC5_API_TRY_CATCH_END
;
1279 bool Sort::isFunction() const
1281 CVC5_API_TRY_CATCH_BEGIN
;
1282 //////// all checks before this line
1283 return d_type
->isFunction();
1285 CVC5_API_TRY_CATCH_END
;
1288 bool Sort::isPredicate() const
1290 CVC5_API_TRY_CATCH_BEGIN
;
1291 //////// all checks before this line
1292 return d_type
->isPredicate();
1294 CVC5_API_TRY_CATCH_END
;
1297 bool Sort::isTuple() const
1299 CVC5_API_TRY_CATCH_BEGIN
;
1300 //////// all checks before this line
1301 return d_type
->isTuple();
1303 CVC5_API_TRY_CATCH_END
;
1306 bool Sort::isRecord() const
1308 CVC5_API_TRY_CATCH_BEGIN
;
1309 //////// all checks before this line
1310 return d_type
->isRecord();
1312 CVC5_API_TRY_CATCH_END
;
1315 bool Sort::isArray() const
1317 CVC5_API_TRY_CATCH_BEGIN
;
1318 //////// all checks before this line
1319 return d_type
->isArray();
1321 CVC5_API_TRY_CATCH_END
;
1324 bool Sort::isSet() const
1326 CVC5_API_TRY_CATCH_BEGIN
;
1327 //////// all checks before this line
1328 return d_type
->isSet();
1330 CVC5_API_TRY_CATCH_END
;
1333 bool Sort::isBag() const
1335 CVC5_API_TRY_CATCH_BEGIN
;
1336 //////// all checks before this line
1337 return d_type
->isBag();
1339 CVC5_API_TRY_CATCH_END
;
1342 bool Sort::isSequence() const
1344 CVC5_API_TRY_CATCH_BEGIN
;
1345 //////// all checks before this line
1346 return d_type
->isSequence();
1348 CVC5_API_TRY_CATCH_END
;
1351 bool Sort::isUninterpretedSort() const
1353 CVC5_API_TRY_CATCH_BEGIN
;
1354 //////// all checks before this line
1355 return d_type
->isSort();
1357 CVC5_API_TRY_CATCH_END
;
1360 bool Sort::isSortConstructor() const
1362 CVC5_API_TRY_CATCH_BEGIN
;
1363 //////// all checks before this line
1364 return d_type
->isSortConstructor();
1366 CVC5_API_TRY_CATCH_END
;
1369 bool Sort::isFirstClass() const
1371 CVC5_API_TRY_CATCH_BEGIN
;
1372 //////// all checks before this line
1373 return d_type
->isFirstClass();
1375 CVC5_API_TRY_CATCH_END
;
1378 bool Sort::isFunctionLike() const
1380 CVC5_API_TRY_CATCH_BEGIN
;
1381 //////// all checks before this line
1382 return d_type
->isFunctionLike();
1384 CVC5_API_TRY_CATCH_END
;
1387 bool Sort::isSubsortOf(const Sort
& s
) const
1389 CVC5_API_TRY_CATCH_BEGIN
;
1390 CVC5_API_ARG_CHECK_SOLVER("sort", s
);
1391 //////// all checks before this line
1392 return d_type
->isSubtypeOf(*s
.d_type
);
1394 CVC5_API_TRY_CATCH_END
;
1397 Datatype
Sort::getDatatype() const
1399 CVC5_API_TRY_CATCH_BEGIN
;
1400 CVC5_API_CHECK_NOT_NULL
;
1401 CVC5_API_CHECK(isDatatype()) << "Expected datatype sort.";
1402 //////// all checks before this line
1403 return Datatype(d_solver
, d_type
->getDType());
1405 CVC5_API_TRY_CATCH_END
;
1408 Sort
Sort::instantiate(const std::vector
<Sort
>& params
) const
1410 CVC5_API_TRY_CATCH_BEGIN
;
1411 CVC5_API_CHECK_NOT_NULL
;
1412 CVC5_API_CHECK_SORTS(params
);
1413 CVC5_API_CHECK(isParametricDatatype() || isSortConstructor())
1414 << "Expected parametric datatype or sort constructor sort.";
1415 CVC5_API_CHECK(isSortConstructor()
1416 || d_type
->getNumChildren() == params
.size() + 1)
1417 << "Arity mismatch for instantiated parametric datatype";
1418 //////// all checks before this line
1419 std::vector
<cvc5::TypeNode
> tparams
= sortVectorToTypeNodes(params
);
1420 if (d_type
->isDatatype())
1422 return Sort(d_solver
, d_type
->instantiateParametricDatatype(tparams
));
1424 Assert(d_type
->isSortConstructor());
1425 return Sort(d_solver
, d_solver
->getNodeManager()->mkSort(*d_type
, tparams
));
1427 CVC5_API_TRY_CATCH_END
;
1430 Sort
Sort::substitute(const Sort
& sort
, const Sort
& replacement
) const
1432 CVC5_API_TRY_CATCH_BEGIN
;
1433 CVC5_API_CHECK_NOT_NULL
;
1434 CVC5_API_CHECK_SORT(sort
);
1435 CVC5_API_CHECK_SORT(replacement
);
1436 //////// all checks before this line
1439 d_type
->substitute(sort
.getTypeNode(), replacement
.getTypeNode()));
1441 CVC5_API_TRY_CATCH_END
;
1444 Sort
Sort::substitute(const std::vector
<Sort
>& sorts
,
1445 const std::vector
<Sort
>& replacements
) const
1447 CVC5_API_TRY_CATCH_BEGIN
;
1448 CVC5_API_CHECK_NOT_NULL
;
1449 CVC5_API_CHECK_SORTS(sorts
);
1450 CVC5_API_CHECK_SORTS(replacements
);
1451 //////// all checks before this line
1453 std::vector
<cvc5::TypeNode
> tSorts
= sortVectorToTypeNodes(sorts
),
1455 sortVectorToTypeNodes(replacements
);
1456 return Sort(d_solver
,
1457 d_type
->substitute(tSorts
.begin(),
1459 tReplacements
.begin(),
1460 tReplacements
.end()));
1462 CVC5_API_TRY_CATCH_END
;
1465 std::string
Sort::toString() const
1467 CVC5_API_TRY_CATCH_BEGIN
;
1468 //////// all checks before this line
1469 return d_type
->toString();
1471 CVC5_API_TRY_CATCH_END
;
1474 const cvc5::TypeNode
& Sort::getTypeNode(void) const { return *d_type
; }
1476 /* Constructor sort ------------------------------------------------------- */
1478 size_t Sort::getConstructorArity() const
1480 CVC5_API_TRY_CATCH_BEGIN
;
1481 CVC5_API_CHECK_NOT_NULL
;
1482 CVC5_API_CHECK(isConstructor()) << "Not a constructor sort: " << (*this);
1483 //////// all checks before this line
1484 return d_type
->getNumChildren() - 1;
1486 CVC5_API_TRY_CATCH_END
;
1489 std::vector
<Sort
> Sort::getConstructorDomainSorts() const
1491 CVC5_API_TRY_CATCH_BEGIN
;
1492 CVC5_API_CHECK_NOT_NULL
;
1493 CVC5_API_CHECK(isConstructor()) << "Not a constructor sort: " << (*this);
1494 //////// all checks before this line
1495 return typeNodeVectorToSorts(d_solver
, d_type
->getArgTypes());
1497 CVC5_API_TRY_CATCH_END
;
1500 Sort
Sort::getConstructorCodomainSort() const
1502 CVC5_API_TRY_CATCH_BEGIN
;
1503 CVC5_API_CHECK_NOT_NULL
;
1504 CVC5_API_CHECK(isConstructor()) << "Not a constructor sort: " << (*this);
1505 //////// all checks before this line
1506 return Sort(d_solver
, d_type
->getConstructorRangeType());
1508 CVC5_API_TRY_CATCH_END
;
1511 /* Selector sort ------------------------------------------------------- */
1513 Sort
Sort::getSelectorDomainSort() const
1515 CVC5_API_TRY_CATCH_BEGIN
;
1516 CVC5_API_CHECK_NOT_NULL
;
1517 CVC5_API_CHECK(isSelector()) << "Not a selector sort: " << (*this);
1518 //////// all checks before this line
1519 return Sort(d_solver
, d_type
->getSelectorDomainType());
1521 CVC5_API_TRY_CATCH_END
;
1524 Sort
Sort::getSelectorCodomainSort() const
1526 CVC5_API_TRY_CATCH_BEGIN
;
1527 CVC5_API_CHECK_NOT_NULL
;
1528 CVC5_API_CHECK(isSelector()) << "Not a selector sort: " << (*this);
1529 //////// all checks before this line
1530 return Sort(d_solver
, d_type
->getSelectorRangeType());
1532 CVC5_API_TRY_CATCH_END
;
1535 /* Tester sort ------------------------------------------------------- */
1537 Sort
Sort::getTesterDomainSort() const
1539 CVC5_API_TRY_CATCH_BEGIN
;
1540 CVC5_API_CHECK_NOT_NULL
;
1541 CVC5_API_CHECK(isTester()) << "Not a tester sort: " << (*this);
1542 //////// all checks before this line
1543 return Sort(d_solver
, d_type
->getTesterDomainType());
1545 CVC5_API_TRY_CATCH_END
;
1548 Sort
Sort::getTesterCodomainSort() const
1550 CVC5_API_TRY_CATCH_BEGIN
;
1551 CVC5_API_CHECK_NOT_NULL
;
1552 CVC5_API_CHECK(isTester()) << "Not a tester sort: " << (*this);
1553 //////// all checks before this line
1554 return d_solver
->getBooleanSort();
1556 CVC5_API_TRY_CATCH_END
;
1559 /* Function sort ------------------------------------------------------- */
1561 size_t Sort::getFunctionArity() const
1563 CVC5_API_TRY_CATCH_BEGIN
;
1564 CVC5_API_CHECK_NOT_NULL
;
1565 CVC5_API_CHECK(isFunction()) << "Not a function sort: " << (*this);
1566 //////// all checks before this line
1567 return d_type
->getNumChildren() - 1;
1569 CVC5_API_TRY_CATCH_END
;
1572 std::vector
<Sort
> Sort::getFunctionDomainSorts() const
1574 CVC5_API_TRY_CATCH_BEGIN
;
1575 CVC5_API_CHECK_NOT_NULL
;
1576 CVC5_API_CHECK(isFunction()) << "Not a function sort: " << (*this);
1577 //////// all checks before this line
1578 return typeNodeVectorToSorts(d_solver
, d_type
->getArgTypes());
1580 CVC5_API_TRY_CATCH_END
;
1583 Sort
Sort::getFunctionCodomainSort() const
1585 CVC5_API_TRY_CATCH_BEGIN
;
1586 CVC5_API_CHECK_NOT_NULL
;
1587 CVC5_API_CHECK(isFunction()) << "Not a function sort" << (*this);
1588 //////// all checks before this line
1589 return Sort(d_solver
, d_type
->getRangeType());
1591 CVC5_API_TRY_CATCH_END
;
1594 /* Array sort ---------------------------------------------------------- */
1596 Sort
Sort::getArrayIndexSort() const
1598 CVC5_API_TRY_CATCH_BEGIN
;
1599 CVC5_API_CHECK_NOT_NULL
;
1600 CVC5_API_CHECK(isArray()) << "Not an array sort.";
1601 //////// all checks before this line
1602 return Sort(d_solver
, d_type
->getArrayIndexType());
1604 CVC5_API_TRY_CATCH_END
;
1607 Sort
Sort::getArrayElementSort() const
1609 CVC5_API_TRY_CATCH_BEGIN
;
1610 CVC5_API_CHECK_NOT_NULL
;
1611 CVC5_API_CHECK(isArray()) << "Not an array sort.";
1612 //////// all checks before this line
1613 return Sort(d_solver
, d_type
->getArrayConstituentType());
1615 CVC5_API_TRY_CATCH_END
;
1618 /* Set sort ------------------------------------------------------------ */
1620 Sort
Sort::getSetElementSort() const
1622 CVC5_API_TRY_CATCH_BEGIN
;
1623 CVC5_API_CHECK_NOT_NULL
;
1624 CVC5_API_CHECK(isSet()) << "Not a set sort.";
1625 //////// all checks before this line
1626 return Sort(d_solver
, d_type
->getSetElementType());
1628 CVC5_API_TRY_CATCH_END
;
1631 /* Bag sort ------------------------------------------------------------ */
1633 Sort
Sort::getBagElementSort() const
1635 CVC5_API_TRY_CATCH_BEGIN
;
1636 CVC5_API_CHECK_NOT_NULL
;
1637 CVC5_API_CHECK(isBag()) << "Not a bag sort.";
1638 //////// all checks before this line
1639 return Sort(d_solver
, d_type
->getBagElementType());
1641 CVC5_API_TRY_CATCH_END
;
1644 /* Sequence sort ------------------------------------------------------- */
1646 Sort
Sort::getSequenceElementSort() const
1648 CVC5_API_TRY_CATCH_BEGIN
;
1649 CVC5_API_CHECK_NOT_NULL
;
1650 CVC5_API_CHECK(isSequence()) << "Not a sequence sort.";
1651 //////// all checks before this line
1652 return Sort(d_solver
, d_type
->getSequenceElementType());
1654 CVC5_API_TRY_CATCH_END
;
1657 /* Uninterpreted sort -------------------------------------------------- */
1659 std::string
Sort::getUninterpretedSortName() const
1661 CVC5_API_TRY_CATCH_BEGIN
;
1662 CVC5_API_CHECK_NOT_NULL
;
1663 CVC5_API_CHECK(isUninterpretedSort()) << "Not an uninterpreted sort.";
1664 //////// all checks before this line
1665 return d_type
->getName();
1667 CVC5_API_TRY_CATCH_END
;
1670 bool Sort::isUninterpretedSortParameterized() const
1672 CVC5_API_TRY_CATCH_BEGIN
;
1673 CVC5_API_CHECK_NOT_NULL
;
1674 CVC5_API_CHECK(isUninterpretedSort()) << "Not an uninterpreted sort.";
1675 //////// all checks before this line
1677 /* This method is not implemented in the NodeManager, since whether a
1678 * uninterpreted sort is parameterized is irrelevant for solving. */
1679 return d_type
->getNumChildren() > 0;
1681 CVC5_API_TRY_CATCH_END
;
1684 std::vector
<Sort
> Sort::getUninterpretedSortParamSorts() const
1686 CVC5_API_TRY_CATCH_BEGIN
;
1687 CVC5_API_CHECK_NOT_NULL
;
1688 CVC5_API_CHECK(isUninterpretedSort()) << "Not an uninterpreted sort.";
1689 //////// all checks before this line
1691 /* This method is not implemented in the NodeManager, since whether a
1692 * uninterpreted sort is parameterized is irrelevant for solving. */
1693 std::vector
<TypeNode
> params
;
1694 for (size_t i
= 0, nchildren
= d_type
->getNumChildren(); i
< nchildren
; i
++)
1696 params
.push_back((*d_type
)[i
]);
1698 return typeNodeVectorToSorts(d_solver
, params
);
1700 CVC5_API_TRY_CATCH_END
;
1703 /* Sort constructor sort ----------------------------------------------- */
1705 std::string
Sort::getSortConstructorName() const
1707 CVC5_API_TRY_CATCH_BEGIN
;
1708 CVC5_API_CHECK_NOT_NULL
;
1709 CVC5_API_CHECK(isSortConstructor()) << "Not a sort constructor sort.";
1710 //////// all checks before this line
1711 return d_type
->getName();
1713 CVC5_API_TRY_CATCH_END
;
1716 size_t Sort::getSortConstructorArity() const
1718 CVC5_API_TRY_CATCH_BEGIN
;
1719 CVC5_API_CHECK_NOT_NULL
;
1720 CVC5_API_CHECK(isSortConstructor()) << "Not a sort constructor sort.";
1721 //////// all checks before this line
1722 return d_type
->getSortConstructorArity();
1724 CVC5_API_TRY_CATCH_END
;
1727 /* Bit-vector sort ----------------------------------------------------- */
1729 uint32_t Sort::getBitVectorSize() const
1731 CVC5_API_TRY_CATCH_BEGIN
;
1732 CVC5_API_CHECK_NOT_NULL
;
1733 CVC5_API_CHECK(isBitVector()) << "Not a bit-vector sort.";
1734 //////// all checks before this line
1735 return d_type
->getBitVectorSize();
1737 CVC5_API_TRY_CATCH_END
;
1740 /* Floating-point sort ------------------------------------------------- */
1742 uint32_t Sort::getFloatingPointExponentSize() const
1744 CVC5_API_TRY_CATCH_BEGIN
;
1745 CVC5_API_CHECK_NOT_NULL
;
1746 CVC5_API_CHECK(isFloatingPoint()) << "Not a floating-point sort.";
1747 //////// all checks before this line
1748 return d_type
->getFloatingPointExponentSize();
1750 CVC5_API_TRY_CATCH_END
;
1753 uint32_t Sort::getFloatingPointSignificandSize() const
1755 CVC5_API_TRY_CATCH_BEGIN
;
1756 CVC5_API_CHECK_NOT_NULL
;
1757 CVC5_API_CHECK(isFloatingPoint()) << "Not a floating-point sort.";
1758 //////// all checks before this line
1759 return d_type
->getFloatingPointSignificandSize();
1761 CVC5_API_TRY_CATCH_END
;
1764 /* Datatype sort ------------------------------------------------------- */
1766 std::vector
<Sort
> Sort::getDatatypeParamSorts() const
1768 CVC5_API_TRY_CATCH_BEGIN
;
1769 CVC5_API_CHECK_NOT_NULL
;
1770 CVC5_API_CHECK(isParametricDatatype()) << "Not a parametric datatype sort.";
1771 //////// all checks before this line
1772 return typeNodeVectorToSorts(d_solver
, d_type
->getParamTypes());
1774 CVC5_API_TRY_CATCH_END
;
1777 size_t Sort::getDatatypeArity() const
1779 CVC5_API_TRY_CATCH_BEGIN
;
1780 CVC5_API_CHECK_NOT_NULL
;
1781 CVC5_API_CHECK(isDatatype()) << "Not a datatype sort.";
1782 //////// all checks before this line
1783 return d_type
->isParametricDatatype() ? d_type
->getNumChildren() - 1 : 0;
1785 CVC5_API_TRY_CATCH_END
;
1788 /* Tuple sort ---------------------------------------------------------- */
1790 size_t Sort::getTupleLength() const
1792 CVC5_API_TRY_CATCH_BEGIN
;
1793 CVC5_API_CHECK_NOT_NULL
;
1794 CVC5_API_CHECK(isTuple()) << "Not a tuple sort.";
1795 //////// all checks before this line
1796 return d_type
->getTupleLength();
1798 CVC5_API_TRY_CATCH_END
;
1801 std::vector
<Sort
> Sort::getTupleSorts() const
1803 CVC5_API_TRY_CATCH_BEGIN
;
1804 CVC5_API_CHECK_NOT_NULL
;
1805 CVC5_API_CHECK(isTuple()) << "Not a tuple sort.";
1806 //////// all checks before this line
1807 return typeNodeVectorToSorts(d_solver
, d_type
->getTupleTypes());
1809 CVC5_API_TRY_CATCH_END
;
1812 /* --------------------------------------------------------------------- */
1814 std::ostream
& operator<<(std::ostream
& out
, const Sort
& s
)
1816 out
<< s
.toString();
1821 /* -------------------------------------------------------------------------- */
1823 /* Split out to avoid nested API calls (problematic with API tracing). */
1824 /* .......................................................................... */
1826 bool Sort::isNullHelper() const { return d_type
->isNull(); }
1828 /* -------------------------------------------------------------------------- */
1830 /* -------------------------------------------------------------------------- */
1832 Op::Op() : d_solver(nullptr), d_kind(NULL_EXPR
), d_node(new cvc5::Node()) {}
1834 Op::Op(const Solver
* slv
, const Kind k
)
1835 : d_solver(slv
), d_kind(k
), d_node(new cvc5::Node())
1839 Op::Op(const Solver
* slv
, const Kind k
, const cvc5::Node
& n
)
1840 : d_solver(slv
), d_kind(k
), d_node(new cvc5::Node(n
))
1846 if (d_solver
!= nullptr)
1848 // Ensure that the correct node manager is in scope when the type node is
1854 /* Public methods */
1855 bool Op::operator==(const Op
& t
) const
1857 CVC5_API_TRY_CATCH_BEGIN
;
1858 //////// all checks before this line
1859 if (d_node
->isNull() && t
.d_node
->isNull())
1861 return (d_kind
== t
.d_kind
);
1863 else if (d_node
->isNull() || t
.d_node
->isNull())
1867 return (d_kind
== t
.d_kind
) && (*d_node
== *t
.d_node
);
1869 CVC5_API_TRY_CATCH_END
;
1872 bool Op::operator!=(const Op
& t
) const
1874 CVC5_API_TRY_CATCH_BEGIN
;
1875 //////// all checks before this line
1876 return !(*this == t
);
1878 CVC5_API_TRY_CATCH_END
;
1881 Kind
Op::getKind() const
1883 CVC5_API_CHECK(d_kind
!= NULL_EXPR
) << "Expecting a non-null Kind";
1884 //////// all checks before this line
1888 bool Op::isNull() const
1890 CVC5_API_TRY_CATCH_BEGIN
;
1891 //////// all checks before this line
1892 return isNullHelper();
1894 CVC5_API_TRY_CATCH_END
;
1897 bool Op::isIndexed() const
1899 CVC5_API_TRY_CATCH_BEGIN
;
1900 //////// all checks before this line
1901 return isIndexedHelper();
1903 CVC5_API_TRY_CATCH_END
;
1906 size_t Op::getNumIndices() const
1908 CVC5_API_TRY_CATCH_BEGIN
;
1909 CVC5_API_CHECK_NOT_NULL
;
1910 //////// all checks before this line
1911 return getNumIndicesHelper();
1913 CVC5_API_TRY_CATCH_END
;
1916 size_t Op::getNumIndicesHelper() const
1918 if (!isIndexedHelper())
1923 Kind k
= intToExtKind(d_node
->getKind());
1927 case DIVISIBLE
: size
= 1; break;
1928 case BITVECTOR_REPEAT
: size
= 1; break;
1929 case BITVECTOR_ZERO_EXTEND
: size
= 1; break;
1930 case BITVECTOR_SIGN_EXTEND
: size
= 1; break;
1931 case BITVECTOR_ROTATE_LEFT
: size
= 1; break;
1932 case BITVECTOR_ROTATE_RIGHT
: size
= 1; break;
1933 case INT_TO_BITVECTOR
: size
= 1; break;
1934 case IAND
: size
= 1; break;
1935 case FLOATINGPOINT_TO_UBV
: size
= 1; break;
1936 case FLOATINGPOINT_TO_SBV
: size
= 1; break;
1937 case REGEXP_REPEAT
: size
= 1; break;
1938 case BITVECTOR_EXTRACT
: size
= 2; break;
1939 case FLOATINGPOINT_TO_FP_IEEE_BITVECTOR
: size
= 2; break;
1940 case FLOATINGPOINT_TO_FP_FLOATINGPOINT
: size
= 2; break;
1941 case FLOATINGPOINT_TO_FP_REAL
: size
= 2; break;
1942 case FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR
: size
= 2; break;
1943 case FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR
: size
= 2; break;
1944 case FLOATINGPOINT_TO_FP_GENERIC
: size
= 2; break;
1945 case REGEXP_LOOP
: size
= 2; break;
1947 size
= d_node
->getConst
<TupleProjectOp
>().getIndices().size();
1949 default: CVC5_API_CHECK(false) << "Unhandled kind " << kindToString(k
);
1954 Term
Op::operator[](size_t index
) const
1956 return getIndexHelper(index
);
1959 Term
Op::getIndexHelper(size_t index
) const
1961 CVC5_API_TRY_CATCH_BEGIN
;
1962 CVC5_API_CHECK_NOT_NULL
;
1963 CVC5_API_CHECK(!d_node
->isNull())
1964 << "Expecting a non-null internal expression. This Op is not indexed.";
1965 CVC5_API_CHECK(index
< getNumIndicesHelper()) << "index out of bound";
1966 Kind k
= intToExtKind(d_node
->getKind());
1972 t
= d_solver
->mkRationalValHelper(
1973 Rational(d_node
->getConst
<Divisible
>().k
));
1976 case BITVECTOR_REPEAT
:
1978 t
= d_solver
->mkRationalValHelper(
1979 d_node
->getConst
<BitVectorRepeat
>().d_repeatAmount
);
1982 case BITVECTOR_ZERO_EXTEND
:
1984 t
= d_solver
->mkRationalValHelper(
1985 d_node
->getConst
<BitVectorZeroExtend
>().d_zeroExtendAmount
);
1988 case BITVECTOR_SIGN_EXTEND
:
1990 t
= d_solver
->mkRationalValHelper(
1991 d_node
->getConst
<BitVectorSignExtend
>().d_signExtendAmount
);
1994 case BITVECTOR_ROTATE_LEFT
:
1996 t
= d_solver
->mkRationalValHelper(
1997 d_node
->getConst
<BitVectorRotateLeft
>().d_rotateLeftAmount
);
2000 case BITVECTOR_ROTATE_RIGHT
:
2002 t
= d_solver
->mkRationalValHelper(
2003 d_node
->getConst
<BitVectorRotateRight
>().d_rotateRightAmount
);
2006 case INT_TO_BITVECTOR
:
2008 t
= d_solver
->mkRationalValHelper(
2009 d_node
->getConst
<IntToBitVector
>().d_size
);
2014 t
= d_solver
->mkRationalValHelper(d_node
->getConst
<IntAnd
>().d_size
);
2017 case FLOATINGPOINT_TO_UBV
:
2019 t
= d_solver
->mkRationalValHelper(
2020 d_node
->getConst
<FloatingPointToUBV
>().d_bv_size
.d_size
);
2023 case FLOATINGPOINT_TO_SBV
:
2025 t
= d_solver
->mkRationalValHelper(
2026 d_node
->getConst
<FloatingPointToSBV
>().d_bv_size
.d_size
);
2031 t
= d_solver
->mkRationalValHelper(
2032 d_node
->getConst
<RegExpRepeat
>().d_repeatAmount
);
2035 case BITVECTOR_EXTRACT
:
2037 cvc5::BitVectorExtract ext
= d_node
->getConst
<BitVectorExtract
>();
2038 t
= index
== 0 ? d_solver
->mkRationalValHelper(ext
.d_high
)
2039 : d_solver
->mkRationalValHelper(ext
.d_low
);
2042 case FLOATINGPOINT_TO_FP_IEEE_BITVECTOR
:
2044 cvc5::FloatingPointToFPIEEEBitVector ext
=
2045 d_node
->getConst
<FloatingPointToFPIEEEBitVector
>();
2048 ? d_solver
->mkRationalValHelper(ext
.getSize().exponentWidth())
2049 : d_solver
->mkRationalValHelper(ext
.getSize().significandWidth());
2052 case FLOATINGPOINT_TO_FP_FLOATINGPOINT
:
2054 cvc5::FloatingPointToFPFloatingPoint ext
=
2055 d_node
->getConst
<FloatingPointToFPFloatingPoint
>();
2057 ? d_solver
->mkRationalValHelper(ext
.getSize().exponentWidth())
2058 : d_solver
->mkRationalValHelper(ext
.getSize().significandWidth());
2061 case FLOATINGPOINT_TO_FP_REAL
:
2063 cvc5::FloatingPointToFPReal ext
=
2064 d_node
->getConst
<FloatingPointToFPReal
>();
2067 ? d_solver
->mkRationalValHelper(ext
.getSize().exponentWidth())
2068 : d_solver
->mkRationalValHelper(ext
.getSize().significandWidth());
2071 case FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR
:
2073 cvc5::FloatingPointToFPSignedBitVector ext
=
2074 d_node
->getConst
<FloatingPointToFPSignedBitVector
>();
2076 ? d_solver
->mkRationalValHelper(ext
.getSize().exponentWidth())
2077 : d_solver
->mkRationalValHelper(ext
.getSize().significandWidth());
2080 case FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR
:
2082 cvc5::FloatingPointToFPUnsignedBitVector ext
=
2083 d_node
->getConst
<FloatingPointToFPUnsignedBitVector
>();
2085 ? d_solver
->mkRationalValHelper(ext
.getSize().exponentWidth())
2086 : d_solver
->mkRationalValHelper(ext
.getSize().significandWidth());
2089 case FLOATINGPOINT_TO_FP_GENERIC
:
2091 cvc5::FloatingPointToFPGeneric ext
=
2092 d_node
->getConst
<FloatingPointToFPGeneric
>();
2094 ? d_solver
->mkRationalValHelper(ext
.getSize().exponentWidth())
2095 : d_solver
->mkRationalValHelper(ext
.getSize().significandWidth());
2100 cvc5::RegExpLoop ext
= d_node
->getConst
<RegExpLoop
>();
2101 t
= index
== 0 ? d_solver
->mkRationalValHelper(ext
.d_loopMinOcc
)
2102 : d_solver
->mkRationalValHelper(ext
.d_loopMaxOcc
);
2109 const std::vector
<uint32_t>& projectionIndices
=
2110 d_node
->getConst
<TupleProjectOp
>().getIndices();
2111 t
= d_solver
->mkRationalValHelper(projectionIndices
[index
]);
2116 CVC5_API_CHECK(false) << "Unhandled kind " << kindToString(k
);
2121 //////// all checks before this line
2124 CVC5_API_TRY_CATCH_END
;
2128 std::string
Op::getIndices() const
2130 CVC5_API_TRY_CATCH_BEGIN
;
2131 CVC5_API_CHECK_NOT_NULL
;
2132 CVC5_API_CHECK(!d_node
->isNull())
2133 << "Expecting a non-null internal expression. This Op is not indexed.";
2134 Kind k
= intToExtKind(d_node
->getKind());
2135 CVC5_API_CHECK(k
== DIVISIBLE
) << "Can't get string index from"
2136 << " kind " << kindToString(k
);
2137 //////// all checks before this line
2138 return d_node
->getConst
<Divisible
>().k
.toString();
2140 CVC5_API_TRY_CATCH_END
;
2144 uint32_t Op::getIndices() const
2146 CVC5_API_TRY_CATCH_BEGIN
;
2147 CVC5_API_CHECK_NOT_NULL
;
2148 CVC5_API_CHECK(!d_node
->isNull())
2149 << "Expecting a non-null internal expression. This Op is not indexed.";
2150 //////// all checks before this line
2153 Kind k
= intToExtKind(d_node
->getKind());
2156 case BITVECTOR_REPEAT
:
2157 i
= d_node
->getConst
<BitVectorRepeat
>().d_repeatAmount
;
2159 case BITVECTOR_ZERO_EXTEND
:
2160 i
= d_node
->getConst
<BitVectorZeroExtend
>().d_zeroExtendAmount
;
2162 case BITVECTOR_SIGN_EXTEND
:
2163 i
= d_node
->getConst
<BitVectorSignExtend
>().d_signExtendAmount
;
2165 case BITVECTOR_ROTATE_LEFT
:
2166 i
= d_node
->getConst
<BitVectorRotateLeft
>().d_rotateLeftAmount
;
2168 case BITVECTOR_ROTATE_RIGHT
:
2169 i
= d_node
->getConst
<BitVectorRotateRight
>().d_rotateRightAmount
;
2171 case INT_TO_BITVECTOR
: i
= d_node
->getConst
<IntToBitVector
>().d_size
; break;
2172 case IAND
: i
= d_node
->getConst
<IntAnd
>().d_size
; break;
2173 case FLOATINGPOINT_TO_UBV
:
2174 i
= d_node
->getConst
<FloatingPointToUBV
>().d_bv_size
.d_size
;
2176 case FLOATINGPOINT_TO_SBV
:
2177 i
= d_node
->getConst
<FloatingPointToSBV
>().d_bv_size
.d_size
;
2180 i
= d_node
->getConst
<RegExpRepeat
>().d_repeatAmount
;
2183 CVC5_API_CHECK(false) << "Can't get uint32_t index from"
2184 << " kind " << kindToString(k
);
2188 CVC5_API_TRY_CATCH_END
;
2192 std::pair
<uint32_t, uint32_t> Op::getIndices() const
2194 CVC5_API_TRY_CATCH_BEGIN
;
2195 CVC5_API_CHECK_NOT_NULL
;
2196 CVC5_API_CHECK(!d_node
->isNull())
2197 << "Expecting a non-null internal expression. This Op is not indexed.";
2198 //////// all checks before this line
2200 std::pair
<uint32_t, uint32_t> indices
;
2201 Kind k
= intToExtKind(d_node
->getKind());
2203 // using if/else instead of case statement because want local variables
2204 if (k
== BITVECTOR_EXTRACT
)
2206 cvc5::BitVectorExtract ext
= d_node
->getConst
<BitVectorExtract
>();
2207 indices
= std::make_pair(ext
.d_high
, ext
.d_low
);
2209 else if (k
== FLOATINGPOINT_TO_FP_IEEE_BITVECTOR
)
2211 cvc5::FloatingPointToFPIEEEBitVector ext
=
2212 d_node
->getConst
<FloatingPointToFPIEEEBitVector
>();
2213 indices
= std::make_pair(ext
.getSize().exponentWidth(),
2214 ext
.getSize().significandWidth());
2216 else if (k
== FLOATINGPOINT_TO_FP_FLOATINGPOINT
)
2218 cvc5::FloatingPointToFPFloatingPoint ext
=
2219 d_node
->getConst
<FloatingPointToFPFloatingPoint
>();
2220 indices
= std::make_pair(ext
.getSize().exponentWidth(),
2221 ext
.getSize().significandWidth());
2223 else if (k
== FLOATINGPOINT_TO_FP_REAL
)
2225 cvc5::FloatingPointToFPReal ext
= d_node
->getConst
<FloatingPointToFPReal
>();
2226 indices
= std::make_pair(ext
.getSize().exponentWidth(),
2227 ext
.getSize().significandWidth());
2229 else if (k
== FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR
)
2231 cvc5::FloatingPointToFPSignedBitVector ext
=
2232 d_node
->getConst
<FloatingPointToFPSignedBitVector
>();
2233 indices
= std::make_pair(ext
.getSize().exponentWidth(),
2234 ext
.getSize().significandWidth());
2236 else if (k
== FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR
)
2238 cvc5::FloatingPointToFPUnsignedBitVector ext
=
2239 d_node
->getConst
<FloatingPointToFPUnsignedBitVector
>();
2240 indices
= std::make_pair(ext
.getSize().exponentWidth(),
2241 ext
.getSize().significandWidth());
2243 else if (k
== FLOATINGPOINT_TO_FP_GENERIC
)
2245 cvc5::FloatingPointToFPGeneric ext
=
2246 d_node
->getConst
<FloatingPointToFPGeneric
>();
2247 indices
= std::make_pair(ext
.getSize().exponentWidth(),
2248 ext
.getSize().significandWidth());
2250 else if (k
== REGEXP_LOOP
)
2252 cvc5::RegExpLoop ext
= d_node
->getConst
<RegExpLoop
>();
2253 indices
= std::make_pair(ext
.d_loopMinOcc
, ext
.d_loopMaxOcc
);
2257 CVC5_API_CHECK(false) << "Can't get pair<uint32_t, uint32_t> indices from"
2258 << " kind " << kindToString(k
);
2262 CVC5_API_TRY_CATCH_END
;
2266 std::vector
<api::Term
> Op::getIndices() const
2268 CVC5_API_TRY_CATCH_BEGIN
;
2269 CVC5_API_CHECK_NOT_NULL
;
2270 CVC5_API_CHECK(!d_node
->isNull())
2271 << "Expecting a non-null internal expression. This Op is not indexed.";
2272 size_t size
= getNumIndicesHelper();
2273 std::vector
<Term
> terms(getNumIndices());
2274 for (size_t i
= 0; i
< size
; i
++)
2276 terms
[i
] = getIndexHelper(i
);
2278 //////// all checks before this line
2281 CVC5_API_TRY_CATCH_END
;
2284 std::string
Op::toString() const
2286 CVC5_API_TRY_CATCH_BEGIN
;
2287 //////// all checks before this line
2288 if (d_node
->isNull())
2290 return kindToString(d_kind
);
2294 CVC5_API_CHECK(!d_node
->isNull())
2295 << "Expecting a non-null internal expression";
2296 if (d_solver
!= nullptr)
2298 return d_node
->toString();
2300 return d_node
->toString();
2303 CVC5_API_TRY_CATCH_END
;
2306 std::ostream
& operator<<(std::ostream
& out
, const Op
& t
)
2308 out
<< t
.toString();
2313 /* -------------------------------------------------------------------------- */
2315 /* Split out to avoid nested API calls (problematic with API tracing). */
2316 /* .......................................................................... */
2318 bool Op::isNullHelper() const
2320 return (d_node
->isNull() && (d_kind
== NULL_EXPR
));
2323 bool Op::isIndexedHelper() const { return !d_node
->isNull(); }
2325 /* -------------------------------------------------------------------------- */
2327 /* -------------------------------------------------------------------------- */
2329 Term::Term() : d_solver(nullptr), d_node(new cvc5::Node()) {}
2331 Term::Term(const Solver
* slv
, const cvc5::Node
& n
) : d_solver(slv
)
2333 d_node
.reset(new cvc5::Node(n
));
2338 if (d_solver
!= nullptr)
2344 bool Term::operator==(const Term
& t
) const
2346 CVC5_API_TRY_CATCH_BEGIN
;
2347 //////// all checks before this line
2348 return *d_node
== *t
.d_node
;
2350 CVC5_API_TRY_CATCH_END
;
2353 bool Term::operator!=(const Term
& t
) const
2355 CVC5_API_TRY_CATCH_BEGIN
;
2356 //////// all checks before this line
2357 return *d_node
!= *t
.d_node
;
2359 CVC5_API_TRY_CATCH_END
;
2362 bool Term::operator<(const Term
& t
) const
2364 CVC5_API_TRY_CATCH_BEGIN
;
2365 //////// all checks before this line
2366 return *d_node
< *t
.d_node
;
2368 CVC5_API_TRY_CATCH_END
;
2371 bool Term::operator>(const Term
& t
) const
2373 CVC5_API_TRY_CATCH_BEGIN
;
2374 //////// all checks before this line
2375 return *d_node
> *t
.d_node
;
2377 CVC5_API_TRY_CATCH_END
;
2380 bool Term::operator<=(const Term
& t
) const
2382 CVC5_API_TRY_CATCH_BEGIN
;
2383 //////// all checks before this line
2384 return *d_node
<= *t
.d_node
;
2386 CVC5_API_TRY_CATCH_END
;
2389 bool Term::operator>=(const Term
& t
) const
2391 CVC5_API_TRY_CATCH_BEGIN
;
2392 //////// all checks before this line
2393 return *d_node
>= *t
.d_node
;
2395 CVC5_API_TRY_CATCH_END
;
2398 size_t Term::getNumChildren() const
2400 CVC5_API_TRY_CATCH_BEGIN
;
2401 CVC5_API_CHECK_NOT_NULL
;
2402 //////// all checks before this line
2404 // special case for apply kinds
2405 if (isApplyKind(d_node
->getKind()))
2407 return d_node
->getNumChildren() + 1;
2413 return d_node
->getNumChildren();
2415 CVC5_API_TRY_CATCH_END
;
2418 Term
Term::operator[](size_t index
) const
2420 CVC5_API_TRY_CATCH_BEGIN
;
2421 CVC5_API_CHECK_NOT_NULL
;
2422 CVC5_API_CHECK(index
< getNumChildren()) << "index out of bound";
2423 CVC5_API_CHECK(!isApplyKind(d_node
->getKind()) || d_node
->hasOperator())
2424 << "Expected apply kind to have operator when accessing child of Term";
2425 //////// all checks before this line
2427 // special cases for apply kinds
2428 if (isApplyKind(d_node
->getKind()))
2432 // return the operator
2433 return Term(d_solver
, d_node
->getOperator());
2440 // otherwise we are looking up child at (index-1)
2441 return Term(d_solver
, (*d_node
)[index
]);
2443 CVC5_API_TRY_CATCH_END
;
2446 uint64_t Term::getId() const
2448 CVC5_API_TRY_CATCH_BEGIN
;
2449 CVC5_API_CHECK_NOT_NULL
;
2450 //////// all checks before this line
2451 return d_node
->getId();
2453 CVC5_API_TRY_CATCH_END
;
2456 Kind
Term::getKind() const
2458 CVC5_API_TRY_CATCH_BEGIN
;
2459 CVC5_API_CHECK_NOT_NULL
;
2460 //////// all checks before this line
2461 return getKindHelper();
2463 CVC5_API_TRY_CATCH_END
;
2466 Sort
Term::getSort() const
2468 CVC5_API_TRY_CATCH_BEGIN
;
2469 CVC5_API_CHECK_NOT_NULL
;
2470 //////// all checks before this line
2471 return Sort(d_solver
, d_node
->getType());
2473 CVC5_API_TRY_CATCH_END
;
2476 Term
Term::substitute(const Term
& term
, const Term
& replacement
) const
2478 CVC5_API_TRY_CATCH_BEGIN
;
2479 CVC5_API_CHECK_NOT_NULL
;
2480 CVC5_API_CHECK_TERM(term
);
2481 CVC5_API_CHECK_TERM(replacement
);
2482 CVC5_API_CHECK(term
.getSort() == replacement
.getSort())
2483 << "Expecting terms of the same sort in substitute";
2484 //////// all checks before this line
2487 d_node
->substitute(TNode(*term
.d_node
), TNode(*replacement
.d_node
)));
2489 CVC5_API_TRY_CATCH_END
;
2492 Term
Term::substitute(const std::vector
<Term
>& terms
,
2493 const std::vector
<Term
>& replacements
) const
2495 CVC5_API_TRY_CATCH_BEGIN
;
2496 CVC5_API_CHECK_NOT_NULL
;
2497 CVC5_API_CHECK(terms
.size() == replacements
.size())
2498 << "Expecting vectors of the same arity in substitute";
2499 CVC5_API_TERM_CHECK_TERMS_WITH_TERMS_SORT_EQUAL_TO(terms
, replacements
);
2500 //////// all checks before this line
2501 std::vector
<Node
> nodes
= Term::termVectorToNodes(terms
);
2502 std::vector
<Node
> nodeReplacements
= Term::termVectorToNodes(replacements
);
2503 return Term(d_solver
,
2504 d_node
->substitute(nodes
.begin(),
2506 nodeReplacements
.begin(),
2507 nodeReplacements
.end()));
2509 CVC5_API_TRY_CATCH_END
;
2512 bool Term::hasOp() const
2514 CVC5_API_TRY_CATCH_BEGIN
;
2515 CVC5_API_CHECK_NOT_NULL
;
2516 //////// all checks before this line
2517 return d_node
->hasOperator();
2519 CVC5_API_TRY_CATCH_END
;
2522 Op
Term::getOp() const
2524 CVC5_API_TRY_CATCH_BEGIN
;
2525 CVC5_API_CHECK_NOT_NULL
;
2526 CVC5_API_CHECK(d_node
->hasOperator())
2527 << "Expecting Term to have an Op when calling getOp()";
2528 //////// all checks before this line
2530 // special cases for parameterized operators that are not indexed operators
2531 // the API level differs from the internal structure
2532 // indexed operators are stored in Ops
2533 // whereas functions and datatype operators are terms, and the Op
2534 // is one of the APPLY_* kinds
2535 if (isApplyKind(d_node
->getKind()))
2537 return Op(d_solver
, intToExtKind(d_node
->getKind()));
2539 else if (d_node
->getMetaKind() == kind::metakind::PARAMETERIZED
)
2541 // it's an indexed operator
2542 // so we should return the indexed op
2543 cvc5::Node op
= d_node
->getOperator();
2544 return Op(d_solver
, intToExtKind(d_node
->getKind()), op
);
2546 // Notice this is the only case where getKindHelper is used, since the
2547 // cases above do not have special cases for intToExtKind.
2548 return Op(d_solver
, getKindHelper());
2550 CVC5_API_TRY_CATCH_END
;
2553 bool Term::hasSymbol() const
2555 CVC5_API_TRY_CATCH_BEGIN
;
2556 CVC5_API_CHECK_NOT_NULL
;
2557 //////// all checks before this line
2558 return d_node
->hasAttribute(expr::VarNameAttr());
2560 CVC5_API_TRY_CATCH_END
;
2563 std::string
Term::getSymbol() const
2565 CVC5_API_TRY_CATCH_BEGIN
;
2566 CVC5_API_CHECK_NOT_NULL
;
2567 CVC5_API_CHECK(d_node
->hasAttribute(expr::VarNameAttr()))
2568 << "Invalid call to '" << __PRETTY_FUNCTION__
2569 << "', expected the term to have a symbol.";
2570 //////// all checks before this line
2571 return d_node
->getAttribute(expr::VarNameAttr());
2573 CVC5_API_TRY_CATCH_END
;
2576 bool Term::isNull() const
2578 CVC5_API_TRY_CATCH_BEGIN
;
2579 //////// all checks before this line
2580 return isNullHelper();
2582 CVC5_API_TRY_CATCH_END
;
2585 Term
Term::notTerm() const
2587 CVC5_API_TRY_CATCH_BEGIN
;
2588 CVC5_API_CHECK_NOT_NULL
;
2589 //////// all checks before this line
2590 Node res
= d_node
->notNode();
2591 (void)res
.getType(true); /* kick off type checking */
2592 return Term(d_solver
, res
);
2594 CVC5_API_TRY_CATCH_END
;
2597 Term
Term::andTerm(const Term
& t
) const
2599 CVC5_API_TRY_CATCH_BEGIN
;
2600 CVC5_API_CHECK_NOT_NULL
;
2601 CVC5_API_CHECK_TERM(t
);
2602 //////// all checks before this line
2603 Node res
= d_node
->andNode(*t
.d_node
);
2604 (void)res
.getType(true); /* kick off type checking */
2605 return Term(d_solver
, res
);
2607 CVC5_API_TRY_CATCH_END
;
2610 Term
Term::orTerm(const Term
& t
) const
2612 CVC5_API_TRY_CATCH_BEGIN
;
2613 CVC5_API_CHECK_NOT_NULL
;
2614 CVC5_API_CHECK_TERM(t
);
2615 //////// all checks before this line
2616 Node res
= d_node
->orNode(*t
.d_node
);
2617 (void)res
.getType(true); /* kick off type checking */
2618 return Term(d_solver
, res
);
2620 CVC5_API_TRY_CATCH_END
;
2623 Term
Term::xorTerm(const Term
& t
) const
2625 CVC5_API_TRY_CATCH_BEGIN
;
2626 CVC5_API_CHECK_NOT_NULL
;
2627 CVC5_API_CHECK_TERM(t
);
2628 //////// all checks before this line
2629 Node res
= d_node
->xorNode(*t
.d_node
);
2630 (void)res
.getType(true); /* kick off type checking */
2631 return Term(d_solver
, res
);
2633 CVC5_API_TRY_CATCH_END
;
2636 Term
Term::eqTerm(const Term
& t
) const
2638 CVC5_API_TRY_CATCH_BEGIN
;
2639 CVC5_API_CHECK_NOT_NULL
;
2640 CVC5_API_CHECK_TERM(t
);
2641 //////// all checks before this line
2642 Node res
= d_node
->eqNode(*t
.d_node
);
2643 (void)res
.getType(true); /* kick off type checking */
2644 return Term(d_solver
, res
);
2646 CVC5_API_TRY_CATCH_END
;
2649 Term
Term::impTerm(const Term
& t
) const
2651 CVC5_API_TRY_CATCH_BEGIN
;
2652 CVC5_API_CHECK_NOT_NULL
;
2653 CVC5_API_CHECK_TERM(t
);
2654 //////// all checks before this line
2655 Node res
= d_node
->impNode(*t
.d_node
);
2656 (void)res
.getType(true); /* kick off type checking */
2657 return Term(d_solver
, res
);
2659 CVC5_API_TRY_CATCH_END
;
2662 Term
Term::iteTerm(const Term
& then_t
, const Term
& else_t
) const
2664 CVC5_API_TRY_CATCH_BEGIN
;
2665 CVC5_API_CHECK_NOT_NULL
;
2666 CVC5_API_CHECK_TERM(then_t
);
2667 CVC5_API_CHECK_TERM(else_t
);
2668 //////// all checks before this line
2669 Node res
= d_node
->iteNode(*then_t
.d_node
, *else_t
.d_node
);
2670 (void)res
.getType(true); /* kick off type checking */
2671 return Term(d_solver
, res
);
2673 CVC5_API_TRY_CATCH_END
;
2676 std::string
Term::toString() const
2678 CVC5_API_TRY_CATCH_BEGIN
;
2679 //////// all checks before this line
2680 return d_node
->toString();
2682 CVC5_API_TRY_CATCH_END
;
2685 Term::const_iterator::const_iterator()
2686 : d_solver(nullptr), d_origNode(nullptr), d_pos(0)
2690 Term::const_iterator::const_iterator(const Solver
* slv
,
2691 const std::shared_ptr
<cvc5::Node
>& n
,
2693 : d_solver(slv
), d_origNode(n
), d_pos(p
)
2697 Term::const_iterator::const_iterator(const const_iterator
& it
)
2698 : d_solver(nullptr), d_origNode(nullptr)
2700 if (it
.d_origNode
!= nullptr)
2702 d_solver
= it
.d_solver
;
2703 d_origNode
= it
.d_origNode
;
2708 Term::const_iterator
& Term::const_iterator::operator=(const const_iterator
& it
)
2710 d_solver
= it
.d_solver
;
2711 d_origNode
= it
.d_origNode
;
2716 bool Term::const_iterator::operator==(const const_iterator
& it
) const
2718 if (d_origNode
== nullptr || it
.d_origNode
== nullptr)
2722 return (d_solver
== it
.d_solver
&& *d_origNode
== *it
.d_origNode
)
2723 && (d_pos
== it
.d_pos
);
2726 bool Term::const_iterator::operator!=(const const_iterator
& it
) const
2728 return !(*this == it
);
2731 Term::const_iterator
& Term::const_iterator::operator++()
2733 Assert(d_origNode
!= nullptr);
2738 Term::const_iterator
Term::const_iterator::operator++(int)
2740 Assert(d_origNode
!= nullptr);
2741 const_iterator it
= *this;
2746 Term
Term::const_iterator::operator*() const
2748 Assert(d_origNode
!= nullptr);
2749 // this term has an extra child (mismatch between API and internal structure)
2750 // the extra child will be the first child
2751 bool extra_child
= isApplyKind(d_origNode
->getKind());
2753 if (!d_pos
&& extra_child
)
2755 return Term(d_solver
, d_origNode
->getOperator());
2759 uint32_t idx
= d_pos
;
2766 return Term(d_solver
, (*d_origNode
)[idx
]);
2770 Term::const_iterator
Term::begin() const
2772 return Term::const_iterator(d_solver
, d_node
, 0);
2775 Term::const_iterator
Term::end() const
2777 int endpos
= d_node
->getNumChildren();
2778 // special cases for APPLY_*
2779 // the API differs from the internal structure
2780 // the API takes a "higher-order" perspective and the applied
2781 // function or datatype constructor/selector/tester is a Term
2782 // which means it needs to be one of the children, even though
2783 // internally it is not
2784 if (isApplyKind(d_node
->getKind()))
2786 // one more child if this is a UF application (count the UF as a child)
2789 return Term::const_iterator(d_solver
, d_node
, endpos
);
2792 const cvc5::Node
& Term::getNode(void) const { return *d_node
; }
2795 const Rational
& getRational(const cvc5::Node
& node
)
2797 switch (node
.getKind())
2799 case cvc5::Kind::CAST_TO_REAL
: return node
[0].getConst
<Rational
>();
2800 case cvc5::Kind::CONST_RATIONAL
: return node
.getConst
<Rational
>();
2802 CVC5_API_CHECK(false) << "Node is not a rational.";
2803 return node
.getConst
<Rational
>();
2806 Integer
getInteger(const cvc5::Node
& node
)
2808 return node
.getConst
<Rational
>().getNumerator();
2810 template <typename T
>
2811 bool checkIntegerBounds(const Integer
& i
)
2813 return i
>= std::numeric_limits
<T
>::min()
2814 && i
<= std::numeric_limits
<T
>::max();
2816 bool checkReal32Bounds(const Rational
& r
)
2818 return checkIntegerBounds
<std::int32_t>(r
.getNumerator())
2819 && checkIntegerBounds
<std::uint32_t>(r
.getDenominator());
2821 bool checkReal64Bounds(const Rational
& r
)
2823 return checkIntegerBounds
<std::int64_t>(r
.getNumerator())
2824 && checkIntegerBounds
<std::uint64_t>(r
.getDenominator());
2827 bool isReal(const Node
& node
)
2829 return node
.getKind() == cvc5::Kind::CONST_RATIONAL
2830 || node
.getKind() == cvc5::Kind::CAST_TO_REAL
;
2832 bool isReal32(const Node
& node
)
2834 return isReal(node
) && checkReal32Bounds(getRational(node
));
2836 bool isReal64(const Node
& node
)
2838 return isReal(node
) && checkReal64Bounds(getRational(node
));
2841 bool isInteger(const Node
& node
)
2843 return node
.getKind() == cvc5::Kind::CONST_RATIONAL
2844 && node
.getConst
<Rational
>().isIntegral();
2846 bool isInt32(const Node
& node
)
2848 return isInteger(node
) && checkIntegerBounds
<std::int32_t>(getInteger(node
));
2850 bool isUInt32(const Node
& node
)
2852 return isInteger(node
) && checkIntegerBounds
<std::uint32_t>(getInteger(node
));
2854 bool isInt64(const Node
& node
)
2856 return isInteger(node
) && checkIntegerBounds
<std::int64_t>(getInteger(node
));
2858 bool isUInt64(const Node
& node
)
2860 return isInteger(node
) && checkIntegerBounds
<std::uint64_t>(getInteger(node
));
2862 } // namespace detail
2864 int32_t Term::getRealOrIntegerValueSign() const
2866 CVC5_API_TRY_CATCH_BEGIN
;
2867 CVC5_API_CHECK_NOT_NULL
;
2868 //////// all checks before this line
2869 const Rational
& r
= detail::getRational(*d_node
);
2870 return static_cast<int32_t>(r
.sgn());
2872 CVC5_API_TRY_CATCH_END
;
2875 bool Term::isInt32Value() const
2877 CVC5_API_TRY_CATCH_BEGIN
;
2878 CVC5_API_CHECK_NOT_NULL
;
2879 //////// all checks before this line
2880 return detail::isInt32(*d_node
);
2882 CVC5_API_TRY_CATCH_END
;
2885 std::int32_t Term::getInt32Value() const
2887 CVC5_API_TRY_CATCH_BEGIN
;
2888 CVC5_API_CHECK_NOT_NULL
;
2889 CVC5_API_ARG_CHECK_EXPECTED(detail::isInt32(*d_node
), *d_node
)
2890 << "Term to be a 32-bit integer value when calling getInt32Value()";
2891 //////// all checks before this line
2892 return detail::getInteger(*d_node
).getSignedInt();
2894 CVC5_API_TRY_CATCH_END
;
2897 bool Term::isUInt32Value() const
2899 CVC5_API_TRY_CATCH_BEGIN
;
2900 CVC5_API_CHECK_NOT_NULL
;
2901 //////// all checks before this line
2902 return detail::isUInt32(*d_node
);
2904 CVC5_API_TRY_CATCH_END
;
2906 std::uint32_t Term::getUInt32Value() const
2908 CVC5_API_TRY_CATCH_BEGIN
;
2909 CVC5_API_CHECK_NOT_NULL
;
2910 CVC5_API_ARG_CHECK_EXPECTED(detail::isUInt32(*d_node
), *d_node
)
2911 << "Term to be a unsigned 32-bit integer value when calling "
2913 //////// all checks before this line
2914 return detail::getInteger(*d_node
).getUnsignedInt();
2916 CVC5_API_TRY_CATCH_END
;
2919 bool Term::isInt64Value() const
2921 CVC5_API_TRY_CATCH_BEGIN
;
2922 CVC5_API_CHECK_NOT_NULL
;
2923 //////// all checks before this line
2924 return detail::isInt64(*d_node
);
2926 CVC5_API_TRY_CATCH_END
;
2928 std::int64_t Term::getInt64Value() const
2930 CVC5_API_TRY_CATCH_BEGIN
;
2931 CVC5_API_CHECK_NOT_NULL
;
2932 CVC5_API_ARG_CHECK_EXPECTED(detail::isInt64(*d_node
), *d_node
)
2933 << "Term to be a 64-bit integer value when calling getInt64Value()";
2934 //////// all checks before this line
2935 return detail::getInteger(*d_node
).getSigned64();
2937 CVC5_API_TRY_CATCH_END
;
2940 bool Term::isUInt64Value() const
2942 CVC5_API_TRY_CATCH_BEGIN
;
2943 CVC5_API_CHECK_NOT_NULL
;
2944 //////// all checks before this line
2945 return detail::isUInt64(*d_node
);
2947 CVC5_API_TRY_CATCH_END
;
2950 std::uint64_t Term::getUInt64Value() const
2952 CVC5_API_TRY_CATCH_BEGIN
;
2953 CVC5_API_CHECK_NOT_NULL
;
2954 CVC5_API_ARG_CHECK_EXPECTED(detail::isUInt64(*d_node
), *d_node
)
2955 << "Term to be a unsigned 64-bit integer value when calling "
2957 //////// all checks before this line
2958 return detail::getInteger(*d_node
).getUnsigned64();
2960 CVC5_API_TRY_CATCH_END
;
2963 bool Term::isIntegerValue() const
2965 CVC5_API_TRY_CATCH_BEGIN
;
2966 CVC5_API_CHECK_NOT_NULL
;
2967 //////// all checks before this line
2968 return detail::isInteger(*d_node
);
2970 CVC5_API_TRY_CATCH_END
;
2972 std::string
Term::getIntegerValue() const
2974 CVC5_API_TRY_CATCH_BEGIN
;
2975 CVC5_API_CHECK_NOT_NULL
;
2976 CVC5_API_ARG_CHECK_EXPECTED(detail::isInteger(*d_node
), *d_node
)
2977 << "Term to be an integer value when calling getIntegerValue()";
2978 //////// all checks before this line
2979 return detail::getInteger(*d_node
).toString();
2981 CVC5_API_TRY_CATCH_END
;
2984 bool Term::isStringValue() const
2986 CVC5_API_TRY_CATCH_BEGIN
;
2987 CVC5_API_CHECK_NOT_NULL
;
2988 //////// all checks before this line
2989 return d_node
->getKind() == cvc5::Kind::CONST_STRING
;
2991 CVC5_API_TRY_CATCH_END
;
2994 std::wstring
Term::getStringValue() const
2996 CVC5_API_TRY_CATCH_BEGIN
;
2997 CVC5_API_CHECK_NOT_NULL
;
2998 CVC5_API_ARG_CHECK_EXPECTED(d_node
->getKind() == cvc5::Kind::CONST_STRING
,
3000 << "Term to be a string value when calling getStringValue()";
3001 //////// all checks before this line
3002 return d_node
->getConst
<cvc5::String
>().toWString();
3004 CVC5_API_TRY_CATCH_END
;
3007 std::vector
<Node
> Term::termVectorToNodes(const std::vector
<Term
>& terms
)
3009 std::vector
<Node
> res
;
3010 for (const Term
& t
: terms
)
3012 res
.push_back(t
.getNode());
3017 std::vector
<Term
> Term::nodeVectorToTerms(const Solver
* slv
,
3018 const std::vector
<Node
>& nodes
)
3020 std::vector
<Term
> res
;
3021 for (const Node
& n
: nodes
)
3023 res
.push_back(Term(slv
, n
));
3028 bool Term::isReal32Value() const
3030 CVC5_API_TRY_CATCH_BEGIN
;
3031 CVC5_API_CHECK_NOT_NULL
;
3032 //////// all checks before this line
3033 return detail::isReal32(*d_node
);
3035 CVC5_API_TRY_CATCH_END
;
3037 std::pair
<std::int32_t, std::uint32_t> Term::getReal32Value() const
3039 CVC5_API_TRY_CATCH_BEGIN
;
3040 CVC5_API_CHECK_NOT_NULL
;
3041 CVC5_API_ARG_CHECK_EXPECTED(detail::isReal32(*d_node
), *d_node
)
3042 << "Term to be a 32-bit rational value when calling getReal32Value()";
3043 //////// all checks before this line
3044 const Rational
& r
= detail::getRational(*d_node
);
3045 return std::make_pair(r
.getNumerator().getSignedInt(),
3046 r
.getDenominator().getUnsignedInt());
3048 CVC5_API_TRY_CATCH_END
;
3050 bool Term::isReal64Value() const
3052 CVC5_API_TRY_CATCH_BEGIN
;
3053 CVC5_API_CHECK_NOT_NULL
;
3054 //////// all checks before this line
3055 return detail::isReal64(*d_node
);
3057 CVC5_API_TRY_CATCH_END
;
3059 std::pair
<std::int64_t, std::uint64_t> Term::getReal64Value() const
3061 CVC5_API_TRY_CATCH_BEGIN
;
3062 CVC5_API_CHECK_NOT_NULL
;
3063 CVC5_API_ARG_CHECK_EXPECTED(detail::isReal64(*d_node
), *d_node
)
3064 << "Term to be a 64-bit rational value when calling getReal64Value()";
3065 //////// all checks before this line
3066 const Rational
& r
= detail::getRational(*d_node
);
3067 return std::make_pair(r
.getNumerator().getSigned64(),
3068 r
.getDenominator().getUnsigned64());
3070 CVC5_API_TRY_CATCH_END
;
3072 bool Term::isRealValue() const
3074 CVC5_API_TRY_CATCH_BEGIN
;
3075 CVC5_API_CHECK_NOT_NULL
;
3076 //////// all checks before this line
3077 return detail::isReal(*d_node
);
3079 CVC5_API_TRY_CATCH_END
;
3081 std::string
Term::getRealValue() const
3083 CVC5_API_TRY_CATCH_BEGIN
;
3084 CVC5_API_CHECK_NOT_NULL
;
3085 CVC5_API_ARG_CHECK_EXPECTED(detail::isReal(*d_node
), *d_node
)
3086 << "Term to be a rational value when calling getRealValue()";
3087 //////// all checks before this line
3088 const Rational
& rat
= detail::getRational(*d_node
);
3089 std::string res
= rat
.toString();
3090 if (rat
.isIntegral())
3096 CVC5_API_TRY_CATCH_END
;
3099 bool Term::isConstArray() const
3101 CVC5_API_TRY_CATCH_BEGIN
;
3102 CVC5_API_CHECK_NOT_NULL
;
3103 //////// all checks before this line
3104 return d_node
->getKind() == cvc5::Kind::STORE_ALL
;
3106 CVC5_API_TRY_CATCH_END
;
3108 Term
Term::getConstArrayBase() const
3110 CVC5_API_TRY_CATCH_BEGIN
;
3111 CVC5_API_CHECK_NOT_NULL
;
3112 CVC5_API_ARG_CHECK_EXPECTED(d_node
->getKind() == cvc5::Kind::STORE_ALL
,
3114 << "Term to be a constant array when calling getConstArrayBase()";
3115 //////// all checks before this line
3116 const auto& ar
= d_node
->getConst
<ArrayStoreAll
>();
3117 return Term(d_solver
, ar
.getValue());
3119 CVC5_API_TRY_CATCH_END
;
3122 bool Term::isBooleanValue() const
3124 CVC5_API_TRY_CATCH_BEGIN
;
3125 CVC5_API_CHECK_NOT_NULL
;
3126 //////// all checks before this line
3127 return d_node
->getKind() == cvc5::Kind::CONST_BOOLEAN
;
3129 CVC5_API_TRY_CATCH_END
;
3131 bool Term::getBooleanValue() const
3133 CVC5_API_TRY_CATCH_BEGIN
;
3134 CVC5_API_CHECK_NOT_NULL
;
3135 CVC5_API_ARG_CHECK_EXPECTED(d_node
->getKind() == cvc5::Kind::CONST_BOOLEAN
,
3137 << "Term to be a Boolean value when calling getBooleanValue()";
3138 //////// all checks before this line
3139 return d_node
->getConst
<bool>();
3141 CVC5_API_TRY_CATCH_END
;
3144 bool Term::isBitVectorValue() const
3146 CVC5_API_TRY_CATCH_BEGIN
;
3147 CVC5_API_CHECK_NOT_NULL
;
3148 //////// all checks before this line
3149 return d_node
->getKind() == cvc5::Kind::CONST_BITVECTOR
;
3151 CVC5_API_TRY_CATCH_END
;
3153 std::string
Term::getBitVectorValue(std::uint32_t base
) const
3155 CVC5_API_TRY_CATCH_BEGIN
;
3156 CVC5_API_CHECK_NOT_NULL
;
3157 CVC5_API_ARG_CHECK_EXPECTED(d_node
->getKind() == cvc5::Kind::CONST_BITVECTOR
,
3159 << "Term to be a bit-vector value when calling getBitVectorValue()";
3160 //////// all checks before this line
3161 return d_node
->getConst
<BitVector
>().toString(base
);
3163 CVC5_API_TRY_CATCH_END
;
3166 bool Term::isUninterpretedSortValue() const
3168 CVC5_API_TRY_CATCH_BEGIN
;
3169 CVC5_API_CHECK_NOT_NULL
;
3170 //////// all checks before this line
3171 return d_node
->getKind() == cvc5::Kind::UNINTERPRETED_SORT_VALUE
;
3173 CVC5_API_TRY_CATCH_END
;
3175 std::string
Term::getUninterpretedSortValue() const
3177 CVC5_API_TRY_CATCH_BEGIN
;
3178 CVC5_API_CHECK_NOT_NULL
;
3179 CVC5_API_ARG_CHECK_EXPECTED(
3180 d_node
->getKind() == cvc5::Kind::UNINTERPRETED_SORT_VALUE
, *d_node
)
3181 << "Term to be an abstract value when calling "
3182 "getUninterpretedSortValue()";
3183 //////// all checks before this line
3184 std::stringstream ss
;
3185 ss
<< d_node
->getConst
<UninterpretedSortValue
>();
3188 CVC5_API_TRY_CATCH_END
;
3191 bool Term::isTupleValue() const
3193 CVC5_API_TRY_CATCH_BEGIN
;
3194 CVC5_API_CHECK_NOT_NULL
;
3195 //////// all checks before this line
3196 return d_node
->getKind() == cvc5::Kind::APPLY_CONSTRUCTOR
&& d_node
->isConst()
3197 && d_node
->getType().getDType().isTuple();
3199 CVC5_API_TRY_CATCH_END
;
3201 std::vector
<Term
> Term::getTupleValue() const
3203 CVC5_API_TRY_CATCH_BEGIN
;
3204 CVC5_API_CHECK_NOT_NULL
;
3205 CVC5_API_ARG_CHECK_EXPECTED(d_node
->getKind() == cvc5::Kind::APPLY_CONSTRUCTOR
3206 && d_node
->isConst()
3207 && d_node
->getType().getDType().isTuple(),
3209 << "Term to be a tuple value when calling getTupleValue()";
3210 //////// all checks before this line
3211 std::vector
<Term
> res
;
3212 for (size_t i
= 0, n
= d_node
->getNumChildren(); i
< n
; ++i
)
3214 res
.emplace_back(Term(d_solver
, (*d_node
)[i
]));
3218 CVC5_API_TRY_CATCH_END
;
3221 bool Term::isFloatingPointPosZero() const
3223 CVC5_API_TRY_CATCH_BEGIN
;
3224 CVC5_API_CHECK_NOT_NULL
;
3225 //////// all checks before this line
3226 if (d_node
->getKind() == cvc5::Kind::CONST_FLOATINGPOINT
)
3228 const auto& fp
= d_node
->getConst
<FloatingPoint
>();
3229 return fp
.isZero() && fp
.isPositive();
3233 CVC5_API_TRY_CATCH_END
;
3235 bool Term::isFloatingPointNegZero() const
3237 CVC5_API_TRY_CATCH_BEGIN
;
3238 CVC5_API_CHECK_NOT_NULL
;
3239 //////// all checks before this line
3240 if (d_node
->getKind() == cvc5::Kind::CONST_FLOATINGPOINT
)
3242 const auto& fp
= d_node
->getConst
<FloatingPoint
>();
3243 return fp
.isZero() && fp
.isNegative();
3247 CVC5_API_TRY_CATCH_END
;
3249 bool Term::isFloatingPointPosInf() const
3251 CVC5_API_TRY_CATCH_BEGIN
;
3252 CVC5_API_CHECK_NOT_NULL
;
3253 //////// all checks before this line
3254 if (d_node
->getKind() == cvc5::Kind::CONST_FLOATINGPOINT
)
3256 const auto& fp
= d_node
->getConst
<FloatingPoint
>();
3257 return fp
.isInfinite() && fp
.isPositive();
3261 CVC5_API_TRY_CATCH_END
;
3263 bool Term::isFloatingPointNegInf() const
3265 CVC5_API_TRY_CATCH_BEGIN
;
3266 CVC5_API_CHECK_NOT_NULL
;
3267 //////// all checks before this line
3268 if (d_node
->getKind() == cvc5::Kind::CONST_FLOATINGPOINT
)
3270 const auto& fp
= d_node
->getConst
<FloatingPoint
>();
3271 return fp
.isInfinite() && fp
.isNegative();
3275 CVC5_API_TRY_CATCH_END
;
3277 bool Term::isFloatingPointNaN() const
3279 CVC5_API_TRY_CATCH_BEGIN
;
3280 CVC5_API_CHECK_NOT_NULL
;
3281 //////// all checks before this line
3282 return d_node
->getKind() == cvc5::Kind::CONST_FLOATINGPOINT
3283 && d_node
->getConst
<FloatingPoint
>().isNaN();
3285 CVC5_API_TRY_CATCH_END
;
3287 bool Term::isFloatingPointValue() const
3289 CVC5_API_TRY_CATCH_BEGIN
;
3290 CVC5_API_CHECK_NOT_NULL
;
3291 //////// all checks before this line
3292 return d_node
->getKind() == cvc5::Kind::CONST_FLOATINGPOINT
;
3294 CVC5_API_TRY_CATCH_END
;
3296 std::tuple
<std::uint32_t, std::uint32_t, Term
> Term::getFloatingPointValue()
3299 CVC5_API_TRY_CATCH_BEGIN
;
3300 CVC5_API_CHECK_NOT_NULL
;
3301 CVC5_API_ARG_CHECK_EXPECTED(
3302 d_node
->getKind() == cvc5::Kind::CONST_FLOATINGPOINT
, *d_node
)
3303 << "Term to be a floating-point value when calling "
3304 "getFloatingPointValue()";
3305 //////// all checks before this line
3306 const auto& fp
= d_node
->getConst
<FloatingPoint
>();
3307 return std::make_tuple(fp
.getSize().exponentWidth(),
3308 fp
.getSize().significandWidth(),
3309 d_solver
->mkValHelper
<BitVector
>(fp
.pack()));
3311 CVC5_API_TRY_CATCH_END
;
3314 bool Term::isSetValue() const
3316 CVC5_API_TRY_CATCH_BEGIN
;
3317 CVC5_API_CHECK_NOT_NULL
;
3318 //////// all checks before this line
3319 return d_node
->getType().isSet() && d_node
->isConst();
3321 CVC5_API_TRY_CATCH_END
;
3324 void Term::collectSet(std::set
<Term
>& set
,
3325 const cvc5::Node
& node
,
3328 // We asserted that node has a set type, and node.isConst()
3329 // Thus, node only contains of SET_EMPTY, SET_UNION and SET_SINGLETON.
3330 switch (node
.getKind())
3332 case cvc5::Kind::SET_EMPTY
: break;
3333 case cvc5::Kind::SET_SINGLETON
: set
.emplace(Term(slv
, node
[0])); break;
3334 case cvc5::Kind::SET_UNION
:
3336 for (const auto& sub
: node
)
3338 collectSet(set
, sub
, slv
);
3343 CVC5_API_ARG_CHECK_EXPECTED(false, node
)
3344 << "Term to be a set value when calling getSetValue()";
3349 std::set
<Term
> Term::getSetValue() const
3351 CVC5_API_TRY_CATCH_BEGIN
;
3352 CVC5_API_CHECK_NOT_NULL
;
3353 CVC5_API_ARG_CHECK_EXPECTED(d_node
->getType().isSet() && d_node
->isConst(),
3355 << "Term to be a set value when calling getSetValue()";
3356 //////// all checks before this line
3358 Term::collectSet(res
, *d_node
, d_solver
);
3361 CVC5_API_TRY_CATCH_END
;
3364 bool Term::isSequenceValue() const
3366 CVC5_API_TRY_CATCH_BEGIN
;
3367 CVC5_API_CHECK_NOT_NULL
;
3368 //////// all checks before this line
3369 return d_node
->getKind() == cvc5::Kind::CONST_SEQUENCE
;
3371 CVC5_API_TRY_CATCH_END
;
3373 std::vector
<Term
> Term::getSequenceValue() const
3375 CVC5_API_TRY_CATCH_BEGIN
;
3376 CVC5_API_CHECK_NOT_NULL
;
3377 CVC5_API_ARG_CHECK_EXPECTED(d_node
->getKind() == cvc5::Kind::CONST_SEQUENCE
,
3379 << "Term to be a sequence value when calling getSequenceValue()";
3380 //////// all checks before this line
3381 std::vector
<Term
> res
;
3382 const Sequence
& seq
= d_node
->getConst
<Sequence
>();
3383 for (const auto& node
: seq
.getVec())
3385 res
.emplace_back(Term(d_solver
, node
));
3389 CVC5_API_TRY_CATCH_END
;
3392 std::ostream
& operator<<(std::ostream
& out
, const Term
& t
)
3394 out
<< t
.toString();
3398 std::ostream
& operator<<(std::ostream
& out
, const std::vector
<Term
>& vector
)
3400 container_to_stream(out
, vector
);
3404 std::ostream
& operator<<(std::ostream
& out
, const std::set
<Term
>& set
)
3406 container_to_stream(out
, set
);
3410 std::ostream
& operator<<(std::ostream
& out
,
3411 const std::unordered_set
<Term
>& unordered_set
)
3413 container_to_stream(out
, unordered_set
);
3417 template <typename V
>
3418 std::ostream
& operator<<(std::ostream
& out
, const std::map
<Term
, V
>& map
)
3420 container_to_stream(out
, map
);
3424 template <typename V
>
3425 std::ostream
& operator<<(std::ostream
& out
,
3426 const std::unordered_map
<Term
, V
>& unordered_map
)
3428 container_to_stream(out
, unordered_map
);
3433 /* -------------------------------------------------------------------------- */
3435 /* Split out to avoid nested API calls (problematic with API tracing). */
3436 /* .......................................................................... */
3438 bool Term::isNullHelper() const
3440 /* Split out to avoid nested API calls (problematic with API tracing). */
3441 return d_node
->isNull();
3444 Kind
Term::getKindHelper() const
3446 /* Sequence kinds do not exist internally, so we must convert their internal
3447 * (string) versions back to sequence. All operators where this is
3448 * necessary are such that their first child is of sequence type, which
3450 if (d_node
->getNumChildren() > 0 && (*d_node
)[0].getType().isSequence())
3452 switch (d_node
->getKind())
3454 case cvc5::Kind::STRING_CONCAT
: return SEQ_CONCAT
;
3455 case cvc5::Kind::STRING_LENGTH
: return SEQ_LENGTH
;
3456 case cvc5::Kind::STRING_SUBSTR
: return SEQ_EXTRACT
;
3457 case cvc5::Kind::STRING_UPDATE
: return SEQ_UPDATE
;
3458 case cvc5::Kind::STRING_CHARAT
: return SEQ_AT
;
3459 case cvc5::Kind::STRING_CONTAINS
: return SEQ_CONTAINS
;
3460 case cvc5::Kind::STRING_INDEXOF
: return SEQ_INDEXOF
;
3461 case cvc5::Kind::STRING_REPLACE
: return SEQ_REPLACE
;
3462 case cvc5::Kind::STRING_REPLACE_ALL
: return SEQ_REPLACE_ALL
;
3463 case cvc5::Kind::STRING_REV
: return SEQ_REV
;
3464 case cvc5::Kind::STRING_PREFIX
: return SEQ_PREFIX
;
3465 case cvc5::Kind::STRING_SUFFIX
: return SEQ_SUFFIX
;
3467 // fall through to conversion below
3471 // Notice that kinds like APPLY_TYPE_ASCRIPTION will be converted to
3475 return CONST_RATIONAL
;
3477 return intToExtKind(d_node
->getKind());
3480 bool Term::isCastedReal() const
3482 if (d_node
->getKind() == kind::CAST_TO_REAL
)
3484 return (*d_node
)[0].isConst() && (*d_node
)[0].getType().isInteger();
3489 /* -------------------------------------------------------------------------- */
3491 /* -------------------------------------------------------------------------- */
3493 /* DatatypeConstructorDecl -------------------------------------------------- */
3495 DatatypeConstructorDecl::DatatypeConstructorDecl()
3496 : d_solver(nullptr), d_ctor(nullptr)
3500 DatatypeConstructorDecl::DatatypeConstructorDecl(const Solver
* slv
,
3501 const std::string
& name
)
3502 : d_solver(slv
), d_ctor(new cvc5::DTypeConstructor(name
))
3505 DatatypeConstructorDecl::~DatatypeConstructorDecl()
3507 if (d_ctor
!= nullptr)
3513 void DatatypeConstructorDecl::addSelector(const std::string
& name
,
3516 CVC5_API_TRY_CATCH_BEGIN
;
3517 CVC5_API_CHECK_NOT_NULL
;
3518 CVC5_API_CHECK_SORT(sort
);
3519 CVC5_API_ARG_CHECK_EXPECTED(!sort
.isNull(), sort
)
3520 << "non-null codomain sort for selector";
3521 //////// all checks before this line
3522 d_ctor
->addArg(name
, *sort
.d_type
);
3524 CVC5_API_TRY_CATCH_END
;
3527 void DatatypeConstructorDecl::addSelectorSelf(const std::string
& name
)
3529 CVC5_API_TRY_CATCH_BEGIN
;
3530 CVC5_API_CHECK_NOT_NULL
;
3531 //////// all checks before this line
3532 d_ctor
->addArgSelf(name
);
3534 CVC5_API_TRY_CATCH_END
;
3537 bool DatatypeConstructorDecl::isNull() const
3539 CVC5_API_TRY_CATCH_BEGIN
;
3540 //////// all checks before this line
3541 return isNullHelper();
3543 CVC5_API_TRY_CATCH_END
;
3546 std::string
DatatypeConstructorDecl::toString() const
3548 CVC5_API_TRY_CATCH_BEGIN
;
3549 //////// all checks before this line
3550 std::stringstream ss
;
3554 CVC5_API_TRY_CATCH_END
;
3557 std::ostream
& operator<<(std::ostream
& out
,
3558 const DatatypeConstructorDecl
& ctordecl
)
3560 out
<< ctordecl
.toString();
3564 std::ostream
& operator<<(std::ostream
& out
,
3565 const std::vector
<DatatypeConstructorDecl
>& vector
)
3567 container_to_stream(out
, vector
);
3571 bool DatatypeConstructorDecl::isNullHelper() const { return d_ctor
== nullptr; }
3573 bool DatatypeConstructorDecl::isResolved() const
3575 return d_ctor
== nullptr || d_ctor
->isResolved();
3578 /* DatatypeDecl ------------------------------------------------------------- */
3580 DatatypeDecl::DatatypeDecl() : d_solver(nullptr), d_dtype(nullptr) {}
3582 DatatypeDecl::DatatypeDecl(const Solver
* slv
,
3583 const std::string
& name
,
3585 : d_solver(slv
), d_dtype(new cvc5::DType(name
, isCoDatatype
))
3589 DatatypeDecl::DatatypeDecl(const Solver
* slv
,
3590 const std::string
& name
,
3594 d_dtype(new cvc5::DType(
3595 name
, std::vector
<TypeNode
>{*param
.d_type
}, isCoDatatype
))
3599 DatatypeDecl::DatatypeDecl(const Solver
* slv
,
3600 const std::string
& name
,
3601 const std::vector
<Sort
>& params
,
3605 std::vector
<TypeNode
> tparams
= Sort::sortVectorToTypeNodes(params
);
3606 d_dtype
= std::shared_ptr
<cvc5::DType
>(
3607 new cvc5::DType(name
, tparams
, isCoDatatype
));
3610 bool DatatypeDecl::isNullHelper() const { return !d_dtype
; }
3612 DatatypeDecl::~DatatypeDecl()
3614 if (d_dtype
!= nullptr)
3620 void DatatypeDecl::addConstructor(const DatatypeConstructorDecl
& ctor
)
3622 CVC5_API_TRY_CATCH_BEGIN
;
3623 CVC5_API_CHECK_NOT_NULL
;
3624 CVC5_API_ARG_CHECK_NOT_NULL(ctor
);
3625 CVC5_API_ARG_CHECK_SOLVER("datatype constructor declaration", ctor
);
3626 //////// all checks before this line
3627 d_dtype
->addConstructor(ctor
.d_ctor
);
3629 CVC5_API_TRY_CATCH_END
;
3632 size_t DatatypeDecl::getNumConstructors() const
3634 CVC5_API_TRY_CATCH_BEGIN
;
3635 CVC5_API_CHECK_NOT_NULL
;
3636 //////// all checks before this line
3637 return d_dtype
->getNumConstructors();
3639 CVC5_API_TRY_CATCH_END
;
3642 bool DatatypeDecl::isParametric() const
3644 CVC5_API_TRY_CATCH_BEGIN
;
3645 CVC5_API_CHECK_NOT_NULL
;
3646 //////// all checks before this line
3647 return d_dtype
->isParametric();
3649 CVC5_API_TRY_CATCH_END
;
3652 std::string
DatatypeDecl::toString() const
3654 CVC5_API_TRY_CATCH_BEGIN
;
3655 CVC5_API_CHECK_NOT_NULL
;
3656 //////// all checks before this line
3657 std::stringstream ss
;
3661 CVC5_API_TRY_CATCH_END
;
3664 std::string
DatatypeDecl::getName() const
3666 CVC5_API_TRY_CATCH_BEGIN
;
3667 CVC5_API_CHECK_NOT_NULL
;
3668 //////// all checks before this line
3669 return d_dtype
->getName();
3671 CVC5_API_TRY_CATCH_END
;
3674 bool DatatypeDecl::isNull() const
3676 CVC5_API_TRY_CATCH_BEGIN
;
3677 //////// all checks before this line
3678 return isNullHelper();
3680 CVC5_API_TRY_CATCH_END
;
3683 std::ostream
& operator<<(std::ostream
& out
, const DatatypeDecl
& dtdecl
)
3685 out
<< dtdecl
.toString();
3689 cvc5::DType
& DatatypeDecl::getDatatype(void) const { return *d_dtype
; }
3691 /* DatatypeSelector --------------------------------------------------------- */
3693 DatatypeSelector::DatatypeSelector() : d_solver(nullptr), d_stor(nullptr) {}
3695 DatatypeSelector::DatatypeSelector(const Solver
* slv
,
3696 const cvc5::DTypeSelector
& stor
)
3697 : d_solver(slv
), d_stor(new cvc5::DTypeSelector(stor
))
3699 CVC5_API_CHECK(d_stor
->isResolved()) << "Expected resolved datatype selector";
3702 DatatypeSelector::~DatatypeSelector()
3704 if (d_stor
!= nullptr)
3710 std::string
DatatypeSelector::getName() const
3712 CVC5_API_TRY_CATCH_BEGIN
;
3713 CVC5_API_CHECK_NOT_NULL
;
3714 //////// all checks before this line
3715 return d_stor
->getName();
3717 CVC5_API_TRY_CATCH_END
;
3720 Term
DatatypeSelector::getSelectorTerm() const
3722 CVC5_API_TRY_CATCH_BEGIN
;
3723 CVC5_API_CHECK_NOT_NULL
;
3724 //////// all checks before this line
3725 return Term(d_solver
, d_stor
->getSelector());
3727 CVC5_API_TRY_CATCH_END
;
3729 Term
DatatypeSelector::getUpdaterTerm() const
3731 CVC5_API_TRY_CATCH_BEGIN
;
3732 CVC5_API_CHECK_NOT_NULL
;
3733 //////// all checks before this line
3734 return Term(d_solver
, d_stor
->getUpdater());
3736 CVC5_API_TRY_CATCH_END
;
3739 Sort
DatatypeSelector::getCodomainSort() const
3741 CVC5_API_TRY_CATCH_BEGIN
;
3742 CVC5_API_CHECK_NOT_NULL
;
3743 //////// all checks before this line
3744 return Sort(d_solver
, d_stor
->getRangeType());
3746 CVC5_API_TRY_CATCH_END
;
3749 bool DatatypeSelector::isNull() const
3751 CVC5_API_TRY_CATCH_BEGIN
;
3752 //////// all checks before this line
3753 return isNullHelper();
3755 CVC5_API_TRY_CATCH_END
;
3758 std::string
DatatypeSelector::toString() const
3760 CVC5_API_TRY_CATCH_BEGIN
;
3761 //////// all checks before this line
3762 std::stringstream ss
;
3766 CVC5_API_TRY_CATCH_END
;
3769 std::ostream
& operator<<(std::ostream
& out
, const DatatypeSelector
& stor
)
3771 out
<< stor
.toString();
3775 bool DatatypeSelector::isNullHelper() const { return d_stor
== nullptr; }
3777 /* DatatypeConstructor ------------------------------------------------------ */
3779 DatatypeConstructor::DatatypeConstructor() : d_solver(nullptr), d_ctor(nullptr)
3783 DatatypeConstructor::DatatypeConstructor(const Solver
* slv
,
3784 const cvc5::DTypeConstructor
& ctor
)
3785 : d_solver(slv
), d_ctor(new cvc5::DTypeConstructor(ctor
))
3787 CVC5_API_CHECK(d_ctor
->isResolved())
3788 << "Expected resolved datatype constructor";
3791 DatatypeConstructor::~DatatypeConstructor()
3793 if (d_ctor
!= nullptr)
3799 std::string
DatatypeConstructor::getName() const
3801 CVC5_API_TRY_CATCH_BEGIN
;
3802 CVC5_API_CHECK_NOT_NULL
;
3803 //////// all checks before this line
3804 return d_ctor
->getName();
3806 CVC5_API_TRY_CATCH_END
;
3809 Term
DatatypeConstructor::getConstructorTerm() const
3811 CVC5_API_TRY_CATCH_BEGIN
;
3812 CVC5_API_CHECK_NOT_NULL
;
3813 //////// all checks before this line
3814 return Term(d_solver
, d_ctor
->getConstructor());
3816 CVC5_API_TRY_CATCH_END
;
3819 Term
DatatypeConstructor::getInstantiatedConstructorTerm(
3820 const Sort
& retSort
) const
3822 CVC5_API_TRY_CATCH_BEGIN
;
3823 CVC5_API_CHECK_NOT_NULL
;
3824 CVC5_API_CHECK(d_ctor
->isResolved())
3825 << "Expected resolved datatype constructor";
3826 CVC5_API_CHECK(retSort
.isDatatype())
3827 << "Cannot get specialized constructor type for non-datatype type "
3829 //////// all checks before this line
3830 Node ret
= d_ctor
->getInstantiatedConstructor(*retSort
.d_type
);
3831 (void)ret
.getType(true); /* kick off type checking */
3832 // apply type ascription to the operator
3833 Term sctor
= api::Term(d_solver
, ret
);
3836 CVC5_API_TRY_CATCH_END
;
3839 Term
DatatypeConstructor::getTesterTerm() const
3841 CVC5_API_TRY_CATCH_BEGIN
;
3842 CVC5_API_CHECK_NOT_NULL
;
3843 //////// all checks before this line
3844 return Term(d_solver
, d_ctor
->getTester());
3846 CVC5_API_TRY_CATCH_END
;
3849 size_t DatatypeConstructor::getNumSelectors() const
3851 CVC5_API_TRY_CATCH_BEGIN
;
3852 CVC5_API_CHECK_NOT_NULL
;
3853 //////// all checks before this line
3854 return d_ctor
->getNumArgs();
3856 CVC5_API_TRY_CATCH_END
;
3859 DatatypeSelector
DatatypeConstructor::operator[](size_t index
) const
3861 CVC5_API_TRY_CATCH_BEGIN
;
3862 CVC5_API_CHECK_NOT_NULL
;
3863 //////// all checks before this line
3864 return DatatypeSelector(d_solver
, (*d_ctor
)[index
]);
3866 CVC5_API_TRY_CATCH_END
;
3869 DatatypeSelector
DatatypeConstructor::operator[](const std::string
& name
) const
3871 CVC5_API_TRY_CATCH_BEGIN
;
3872 CVC5_API_CHECK_NOT_NULL
;
3873 //////// all checks before this line
3874 return getSelectorForName(name
);
3876 CVC5_API_TRY_CATCH_END
;
3879 DatatypeSelector
DatatypeConstructor::getSelector(const std::string
& name
) const
3881 CVC5_API_TRY_CATCH_BEGIN
;
3882 CVC5_API_CHECK_NOT_NULL
;
3883 //////// all checks before this line
3884 return getSelectorForName(name
);
3886 CVC5_API_TRY_CATCH_END
;
3889 Term
DatatypeConstructor::getSelectorTerm(const std::string
& name
) const
3891 CVC5_API_TRY_CATCH_BEGIN
;
3892 CVC5_API_CHECK_NOT_NULL
;
3893 //////// all checks before this line
3894 return getSelector(name
).getSelectorTerm();
3896 CVC5_API_TRY_CATCH_END
;
3899 DatatypeConstructor::const_iterator
DatatypeConstructor::begin() const
3901 return DatatypeConstructor::const_iterator(d_solver
, *d_ctor
, true);
3904 DatatypeConstructor::const_iterator
DatatypeConstructor::end() const
3906 return DatatypeConstructor::const_iterator(d_solver
, *d_ctor
, false);
3909 DatatypeConstructor::const_iterator::const_iterator(
3910 const Solver
* slv
, const cvc5::DTypeConstructor
& ctor
, bool begin
)
3913 d_int_stors
= &ctor
.getArgs();
3915 const std::vector
<std::shared_ptr
<cvc5::DTypeSelector
>>& sels
=
3917 for (const std::shared_ptr
<cvc5::DTypeSelector
>& s
: sels
)
3919 /* Can not use emplace_back here since constructor is private. */
3920 d_stors
.push_back(DatatypeSelector(d_solver
, *s
.get()));
3922 d_idx
= begin
? 0 : sels
.size();
3925 DatatypeConstructor::const_iterator::const_iterator()
3926 : d_solver(nullptr), d_int_stors(nullptr), d_idx(0)
3930 DatatypeConstructor::const_iterator
&
3931 DatatypeConstructor::const_iterator::operator=(
3932 const DatatypeConstructor::const_iterator
& it
)
3934 d_solver
= it
.d_solver
;
3935 d_int_stors
= it
.d_int_stors
;
3936 d_stors
= it
.d_stors
;
3941 const DatatypeSelector
& DatatypeConstructor::const_iterator::operator*() const
3943 return d_stors
[d_idx
];
3946 const DatatypeSelector
* DatatypeConstructor::const_iterator::operator->() const
3948 return &d_stors
[d_idx
];
3951 DatatypeConstructor::const_iterator
&
3952 DatatypeConstructor::const_iterator::operator++()
3958 DatatypeConstructor::const_iterator
3959 DatatypeConstructor::const_iterator::operator++(int)
3961 DatatypeConstructor::const_iterator
it(*this);
3966 bool DatatypeConstructor::const_iterator::operator==(
3967 const DatatypeConstructor::const_iterator
& other
) const
3969 return d_int_stors
== other
.d_int_stors
&& d_idx
== other
.d_idx
;
3972 bool DatatypeConstructor::const_iterator::operator!=(
3973 const DatatypeConstructor::const_iterator
& other
) const
3975 return d_int_stors
!= other
.d_int_stors
|| d_idx
!= other
.d_idx
;
3978 bool DatatypeConstructor::isNull() const
3980 CVC5_API_TRY_CATCH_BEGIN
;
3981 //////// all checks before this line
3982 return isNullHelper();
3984 CVC5_API_TRY_CATCH_END
;
3987 std::string
DatatypeConstructor::toString() const
3989 CVC5_API_TRY_CATCH_BEGIN
;
3990 //////// all checks before this line
3991 std::stringstream ss
;
3995 CVC5_API_TRY_CATCH_END
;
3998 bool DatatypeConstructor::isNullHelper() const { return d_ctor
== nullptr; }
4000 DatatypeSelector
DatatypeConstructor::getSelectorForName(
4001 const std::string
& name
) const
4003 bool foundSel
= false;
4005 for (size_t i
= 0, nsels
= getNumSelectors(); i
< nsels
; i
++)
4007 if ((*d_ctor
)[i
].getName() == name
)
4016 std::stringstream snames
;
4018 for (size_t i
= 0, ncons
= getNumSelectors(); i
< ncons
; i
++)
4020 snames
<< (*d_ctor
)[i
].getName() << " ";
4023 CVC5_API_CHECK(foundSel
) << "No selector " << name
<< " for constructor "
4024 << getName() << " exists among " << snames
.str();
4026 return DatatypeSelector(d_solver
, (*d_ctor
)[index
]);
4029 std::ostream
& operator<<(std::ostream
& out
, const DatatypeConstructor
& ctor
)
4031 out
<< ctor
.toString();
4035 /* Datatype ----------------------------------------------------------------- */
4037 Datatype::Datatype(const Solver
* slv
, const cvc5::DType
& dtype
)
4038 : d_solver(slv
), d_dtype(new cvc5::DType(dtype
))
4040 CVC5_API_CHECK(d_dtype
->isResolved()) << "Expected resolved datatype";
4043 Datatype::Datatype() : d_solver(nullptr), d_dtype(nullptr) {}
4045 Datatype::~Datatype()
4047 if (d_dtype
!= nullptr)
4053 DatatypeConstructor
Datatype::operator[](size_t idx
) const
4055 CVC5_API_TRY_CATCH_BEGIN
;
4056 CVC5_API_CHECK_NOT_NULL
;
4057 CVC5_API_CHECK(idx
< getNumConstructors()) << "Index out of bounds.";
4058 //////// all checks before this line
4059 return DatatypeConstructor(d_solver
, (*d_dtype
)[idx
]);
4061 CVC5_API_TRY_CATCH_END
;
4064 DatatypeConstructor
Datatype::operator[](const std::string
& name
) const
4066 CVC5_API_TRY_CATCH_BEGIN
;
4067 CVC5_API_CHECK_NOT_NULL
;
4068 //////// all checks before this line
4069 return getConstructorForName(name
);
4071 CVC5_API_TRY_CATCH_END
;
4074 DatatypeConstructor
Datatype::getConstructor(const std::string
& name
) const
4076 CVC5_API_TRY_CATCH_BEGIN
;
4077 CVC5_API_CHECK_NOT_NULL
;
4078 //////// all checks before this line
4079 return getConstructorForName(name
);
4081 CVC5_API_TRY_CATCH_END
;
4084 Term
Datatype::getConstructorTerm(const std::string
& name
) const
4086 CVC5_API_TRY_CATCH_BEGIN
;
4087 CVC5_API_CHECK_NOT_NULL
;
4088 //////// all checks before this line
4089 return getConstructorForName(name
).getConstructorTerm();
4091 CVC5_API_TRY_CATCH_END
;
4094 DatatypeSelector
Datatype::getSelector(const std::string
& name
) const
4096 CVC5_API_TRY_CATCH_BEGIN
;
4097 CVC5_API_CHECK_NOT_NULL
;
4098 //////// all checks before this line
4099 return getSelectorForName(name
);
4101 CVC5_API_TRY_CATCH_END
;
4104 std::string
Datatype::getName() const
4106 CVC5_API_TRY_CATCH_BEGIN
;
4107 CVC5_API_CHECK_NOT_NULL
;
4108 //////// all checks before this line
4109 return d_dtype
->getName();
4111 CVC5_API_TRY_CATCH_END
;
4114 size_t Datatype::getNumConstructors() const
4116 CVC5_API_TRY_CATCH_BEGIN
;
4117 CVC5_API_CHECK_NOT_NULL
;
4118 //////// all checks before this line
4119 return d_dtype
->getNumConstructors();
4121 CVC5_API_TRY_CATCH_END
;
4124 std::vector
<Sort
> Datatype::getParameters() const
4126 CVC5_API_TRY_CATCH_BEGIN
;
4127 CVC5_API_CHECK_NOT_NULL
;
4128 CVC5_API_CHECK(isParametric()) << "Expected parametric datatype";
4129 //////// all checks before this line
4130 std::vector
<cvc5::TypeNode
> params
= d_dtype
->getParameters();
4131 return Sort::typeNodeVectorToSorts(d_solver
, params
);
4133 CVC5_API_TRY_CATCH_END
;
4136 bool Datatype::isParametric() const
4138 CVC5_API_TRY_CATCH_BEGIN
;
4139 CVC5_API_CHECK_NOT_NULL
;
4140 //////// all checks before this line
4141 return d_dtype
->isParametric();
4143 CVC5_API_TRY_CATCH_END
;
4146 bool Datatype::isCodatatype() const
4148 CVC5_API_TRY_CATCH_BEGIN
;
4149 CVC5_API_CHECK_NOT_NULL
;
4150 //////// all checks before this line
4151 return d_dtype
->isCodatatype();
4153 CVC5_API_TRY_CATCH_END
;
4156 bool Datatype::isTuple() const
4158 CVC5_API_TRY_CATCH_BEGIN
;
4159 CVC5_API_CHECK_NOT_NULL
;
4160 //////// all checks before this line
4161 return d_dtype
->isTuple();
4163 CVC5_API_TRY_CATCH_END
;
4166 bool Datatype::isRecord() const
4168 CVC5_API_TRY_CATCH_BEGIN
;
4169 CVC5_API_CHECK_NOT_NULL
;
4170 //////// all checks before this line
4171 return d_dtype
->isRecord();
4173 CVC5_API_TRY_CATCH_END
;
4176 bool Datatype::isFinite() const
4178 CVC5_API_TRY_CATCH_BEGIN
;
4179 CVC5_API_CHECK_NOT_NULL
;
4180 CVC5_API_CHECK(!d_dtype
->isParametric())
4181 << "Invalid call to 'isFinite()', expected non-parametric Datatype";
4182 //////// all checks before this line
4183 // we assume that finite model finding is disabled by passing false as the
4185 return isCardinalityClassFinite(d_dtype
->getCardinalityClass(), false);
4187 CVC5_API_TRY_CATCH_END
;
4190 bool Datatype::isWellFounded() const
4192 CVC5_API_TRY_CATCH_BEGIN
;
4193 CVC5_API_CHECK_NOT_NULL
;
4194 //////// all checks before this line
4195 return d_dtype
->isWellFounded();
4197 CVC5_API_TRY_CATCH_END
;
4200 bool Datatype::isNull() const
4202 CVC5_API_TRY_CATCH_BEGIN
;
4203 //////// all checks before this line
4204 return isNullHelper();
4206 CVC5_API_TRY_CATCH_END
;
4209 std::string
Datatype::toString() const
4211 CVC5_API_TRY_CATCH_BEGIN
;
4212 CVC5_API_CHECK_NOT_NULL
;
4213 //////// all checks before this line
4214 return d_dtype
->getName();
4216 CVC5_API_TRY_CATCH_END
;
4219 Datatype::const_iterator
Datatype::begin() const
4221 return Datatype::const_iterator(d_solver
, *d_dtype
, true);
4224 Datatype::const_iterator
Datatype::end() const
4226 return Datatype::const_iterator(d_solver
, *d_dtype
, false);
4229 DatatypeConstructor
Datatype::getConstructorForName(
4230 const std::string
& name
) const
4232 bool foundCons
= false;
4234 for (size_t i
= 0, ncons
= getNumConstructors(); i
< ncons
; i
++)
4236 if ((*d_dtype
)[i
].getName() == name
)
4245 std::stringstream snames
;
4247 for (size_t i
= 0, ncons
= getNumConstructors(); i
< ncons
; i
++)
4249 snames
<< (*d_dtype
)[i
].getName() << " ";
4252 CVC5_API_CHECK(foundCons
) << "No constructor " << name
<< " for datatype "
4253 << getName() << " exists, among " << snames
.str();
4255 return DatatypeConstructor(d_solver
, (*d_dtype
)[index
]);
4258 DatatypeSelector
Datatype::getSelectorForName(const std::string
& name
) const
4260 bool foundSel
= false;
4263 for (size_t i
= 0, ncons
= getNumConstructors(); i
< ncons
; i
++)
4265 int si
= (*d_dtype
)[i
].getSelectorIndexForName(name
);
4268 sindex
= static_cast<size_t>(si
);
4276 CVC5_API_CHECK(foundSel
)
4277 << "No select " << name
<< " for datatype " << getName() << " exists";
4279 return DatatypeSelector(d_solver
, (*d_dtype
)[index
][sindex
]);
4282 Datatype::const_iterator::const_iterator(const Solver
* slv
,
4283 const cvc5::DType
& dtype
,
4285 : d_solver(slv
), d_int_ctors(&dtype
.getConstructors())
4287 const std::vector
<std::shared_ptr
<DTypeConstructor
>>& cons
=
4288 dtype
.getConstructors();
4289 for (const std::shared_ptr
<DTypeConstructor
>& c
: cons
)
4291 /* Can not use emplace_back here since constructor is private. */
4292 d_ctors
.push_back(DatatypeConstructor(d_solver
, *c
.get()));
4294 d_idx
= begin
? 0 : cons
.size();
4297 Datatype::const_iterator::const_iterator()
4298 : d_solver(nullptr), d_int_ctors(nullptr), d_idx(0)
4302 Datatype::const_iterator
& Datatype::const_iterator::operator=(
4303 const Datatype::const_iterator
& it
)
4305 d_solver
= it
.d_solver
;
4306 d_int_ctors
= it
.d_int_ctors
;
4307 d_ctors
= it
.d_ctors
;
4312 const DatatypeConstructor
& Datatype::const_iterator::operator*() const
4314 return d_ctors
[d_idx
];
4317 const DatatypeConstructor
* Datatype::const_iterator::operator->() const
4319 return &d_ctors
[d_idx
];
4322 Datatype::const_iterator
& Datatype::const_iterator::operator++()
4328 Datatype::const_iterator
Datatype::const_iterator::operator++(int)
4330 Datatype::const_iterator
it(*this);
4335 bool Datatype::const_iterator::operator==(
4336 const Datatype::const_iterator
& other
) const
4338 return d_int_ctors
== other
.d_int_ctors
&& d_idx
== other
.d_idx
;
4341 bool Datatype::const_iterator::operator!=(
4342 const Datatype::const_iterator
& other
) const
4344 return d_int_ctors
!= other
.d_int_ctors
|| d_idx
!= other
.d_idx
;
4347 bool Datatype::isNullHelper() const { return d_dtype
== nullptr; }
4349 /* -------------------------------------------------------------------------- */
4351 /* -------------------------------------------------------------------------- */
4354 : d_solver(nullptr),
4364 Grammar::Grammar(const Solver
* slv
,
4365 const std::vector
<Term
>& sygusVars
,
4366 const std::vector
<Term
>& ntSymbols
)
4368 d_sygusVars(sygusVars
),
4369 d_ntSyms(ntSymbols
),
4370 d_ntsToTerms(ntSymbols
.size()),
4375 for (Term ntsymbol
: d_ntSyms
)
4377 d_ntsToTerms
.emplace(ntsymbol
, std::vector
<Term
>());
4381 void Grammar::addRule(const Term
& ntSymbol
, const Term
& rule
)
4383 CVC5_API_TRY_CATCH_BEGIN
;
4384 CVC5_API_CHECK(!d_isResolved
) << "Grammar cannot be modified after passing "
4385 "it as an argument to synthFun/synthInv";
4386 CVC5_API_CHECK_TERM(ntSymbol
);
4387 CVC5_API_CHECK_TERM(rule
);
4388 CVC5_API_ARG_CHECK_EXPECTED(
4389 d_ntsToTerms
.find(ntSymbol
) != d_ntsToTerms
.cend(), ntSymbol
)
4390 << "ntSymbol to be one of the non-terminal symbols given in the "
4392 CVC5_API_CHECK(ntSymbol
.d_node
->getType() == rule
.d_node
->getType())
4393 << "Expected ntSymbol and rule to have the same sort";
4394 CVC5_API_ARG_CHECK_EXPECTED(!containsFreeVariables(rule
), rule
)
4395 << "a term whose free variables are limited to synthFun/synthInv "
4396 "parameters and non-terminal symbols of the grammar";
4397 //////// all checks before this line
4398 d_ntsToTerms
[ntSymbol
].push_back(rule
);
4400 CVC5_API_TRY_CATCH_END
;
4403 void Grammar::addRules(const Term
& ntSymbol
, const std::vector
<Term
>& rules
)
4405 CVC5_API_TRY_CATCH_BEGIN
;
4406 CVC5_API_CHECK(!d_isResolved
) << "Grammar cannot be modified after passing "
4407 "it as an argument to synthFun/synthInv";
4408 CVC5_API_CHECK_TERM(ntSymbol
);
4409 CVC5_API_CHECK_TERMS_WITH_SORT(rules
, ntSymbol
.getSort());
4410 CVC5_API_ARG_CHECK_EXPECTED(
4411 d_ntsToTerms
.find(ntSymbol
) != d_ntsToTerms
.cend(), ntSymbol
)
4412 << "ntSymbol to be one of the non-terminal symbols given in the "
4414 for (size_t i
= 0, n
= rules
.size(); i
< n
; ++i
)
4416 CVC5_API_ARG_AT_INDEX_CHECK_EXPECTED(
4417 !containsFreeVariables(rules
[i
]), rules
[i
], rules
, i
)
4418 << "a term whose free variables are limited to synthFun/synthInv "
4419 "parameters and non-terminal symbols of the grammar";
4421 //////// all checks before this line
4422 d_ntsToTerms
[ntSymbol
].insert(
4423 d_ntsToTerms
[ntSymbol
].cend(), rules
.cbegin(), rules
.cend());
4425 CVC5_API_TRY_CATCH_END
;
4428 void Grammar::addAnyConstant(const Term
& ntSymbol
)
4430 CVC5_API_TRY_CATCH_BEGIN
;
4431 CVC5_API_CHECK(!d_isResolved
) << "Grammar cannot be modified after passing "
4432 "it as an argument to synthFun/synthInv";
4433 CVC5_API_CHECK_TERM(ntSymbol
);
4434 CVC5_API_ARG_CHECK_EXPECTED(
4435 d_ntsToTerms
.find(ntSymbol
) != d_ntsToTerms
.cend(), ntSymbol
)
4436 << "ntSymbol to be one of the non-terminal symbols given in the "
4438 //////// all checks before this line
4439 d_allowConst
.insert(ntSymbol
);
4441 CVC5_API_TRY_CATCH_END
;
4444 void Grammar::addAnyVariable(const Term
& ntSymbol
)
4446 CVC5_API_TRY_CATCH_BEGIN
;
4447 CVC5_API_CHECK(!d_isResolved
) << "Grammar cannot be modified after passing "
4448 "it as an argument to synthFun/synthInv";
4449 CVC5_API_CHECK_TERM(ntSymbol
);
4450 CVC5_API_ARG_CHECK_EXPECTED(
4451 d_ntsToTerms
.find(ntSymbol
) != d_ntsToTerms
.cend(), ntSymbol
)
4452 << "ntSymbol to be one of the non-terminal symbols given in the "
4454 //////// all checks before this line
4455 d_allowVars
.insert(ntSymbol
);
4457 CVC5_API_TRY_CATCH_END
;
4461 * This function concatenates the outputs of calling f on each element between
4462 * first and last, seperated by sep.
4463 * @param first the beginning of the range
4464 * @param last the end of the range
4465 * @param f the function to call on each element in the range, its output must
4466 * be overloaded for operator<<
4467 * @param sep the string to add between successive calls to f
4469 template <typename Iterator
, typename Function
>
4470 std::string
join(Iterator first
, Iterator last
, Function f
, std::string sep
)
4472 std::stringstream ss
;
4490 std::string
Grammar::toString() const
4492 CVC5_API_TRY_CATCH_BEGIN
;
4493 //////// all checks before this line
4494 std::stringstream ss
;
4495 ss
<< " (" // pre-declaration
4500 std::stringstream s
;
4501 s
<< '(' << t
<< ' ' << t
.getSort() << ')';
4505 << ")\n (" // grouped rule listing
4509 [this](const Term
& t
) {
4510 bool allowConst
= d_allowConst
.find(t
) != d_allowConst
.cend(),
4511 allowVars
= d_allowVars
.find(t
) != d_allowVars
.cend();
4512 const std::vector
<Term
>& rules
= d_ntsToTerms
.at(t
);
4513 std::stringstream s
;
4514 s
<< '(' << t
<< ' ' << t
.getSort() << " ("
4515 << (allowConst
? "(Constant " + t
.getSort().toString() + ")"
4517 << (allowConst
&& allowVars
? " " : "")
4518 << (allowVars
? "(Var " + t
.getSort().toString() + ")" : "")
4519 << ((allowConst
|| allowVars
) && !rules
.empty() ? " " : "")
4523 [](const Term
& rule
) { return rule
.toString(); },
4533 CVC5_API_TRY_CATCH_END
;
4536 Sort
Grammar::resolve()
4538 CVC5_API_TRY_CATCH_BEGIN
;
4539 //////// all checks before this line
4541 d_isResolved
= true;
4545 if (!d_sygusVars
.empty())
4549 d_solver
->getNodeManager()->mkNode(
4550 cvc5::kind::BOUND_VAR_LIST
, Term::termVectorToNodes(d_sygusVars
)));
4553 std::unordered_map
<Term
, Sort
> ntsToUnres(d_ntSyms
.size());
4555 for (Term ntsymbol
: d_ntSyms
)
4557 // make the unresolved type, used for referencing the final version of
4558 // the ntsymbol's datatype
4559 ntsToUnres
[ntsymbol
] =
4560 Sort(d_solver
, d_solver
->getNodeManager()->mkSort(ntsymbol
.toString()));
4563 std::vector
<cvc5::DType
> datatypes
;
4564 std::set
<TypeNode
> unresTypes
;
4566 datatypes
.reserve(d_ntSyms
.size());
4568 for (const Term
& ntSym
: d_ntSyms
)
4570 // make the datatype, which encodes terms generated by this non-terminal
4571 DatatypeDecl
dtDecl(d_solver
, ntSym
.toString());
4573 for (const Term
& consTerm
: d_ntsToTerms
[ntSym
])
4575 addSygusConstructorTerm(dtDecl
, consTerm
, ntsToUnres
);
4578 if (d_allowVars
.find(ntSym
) != d_allowVars
.cend())
4580 addSygusConstructorVariables(dtDecl
,
4581 Sort(d_solver
, ntSym
.d_node
->getType()));
4584 bool aci
= d_allowConst
.find(ntSym
) != d_allowConst
.end();
4585 TypeNode btt
= ntSym
.d_node
->getType();
4586 dtDecl
.d_dtype
->setSygus(btt
, *bvl
.d_node
, aci
, false);
4588 // We can be in a case where the only rule specified was (Variable T)
4589 // and there are no variables of type T, in which case this is a bogus
4590 // grammar. This results in the error below.
4591 CVC5_API_CHECK(dtDecl
.d_dtype
->getNumConstructors() != 0)
4592 << "Grouped rule listing for " << *dtDecl
.d_dtype
4593 << " produced an empty rule list";
4595 datatypes
.push_back(*dtDecl
.d_dtype
);
4596 unresTypes
.insert(*ntsToUnres
[ntSym
].d_type
);
4599 std::vector
<TypeNode
> datatypeTypes
=
4600 d_solver
->getNodeManager()->mkMutualDatatypeTypes(
4601 datatypes
, unresTypes
, NodeManager::DATATYPE_FLAG_PLACEHOLDER
);
4603 // return is the first datatype
4604 return Sort(d_solver
, datatypeTypes
[0]);
4606 CVC5_API_TRY_CATCH_END
;
4609 void Grammar::addSygusConstructorTerm(
4612 const std::unordered_map
<Term
, Sort
>& ntsToUnres
) const
4614 CVC5_API_TRY_CATCH_BEGIN
;
4615 CVC5_API_CHECK_DTDECL(dt
);
4616 CVC5_API_CHECK_TERM(term
);
4617 CVC5_API_CHECK_TERMS_MAP(ntsToUnres
);
4618 //////// all checks before this line
4620 // At this point, we should know that dt is well founded, and that its
4621 // builtin sygus operators are well-typed.
4622 // Now, purify each occurrence of a non-terminal symbol in term, replace by
4623 // free variables. These become arguments to constructors. Notice we must do
4624 // a tree traversal in this function, since unique paths to the same term
4625 // should be treated as distinct terms.
4626 // Notice that let expressions are forbidden in the input syntax of term, so
4627 // this does not lead to exponential behavior with respect to input size.
4628 std::vector
<Term
> args
;
4629 std::vector
<Sort
> cargs
;
4630 Term op
= purifySygusGTerm(term
, args
, cargs
, ntsToUnres
);
4631 std::stringstream ssCName
;
4632 ssCName
<< op
.getKind();
4637 d_solver
->getNodeManager()->mkNode(cvc5::kind::BOUND_VAR_LIST
,
4638 Term::termVectorToNodes(args
)));
4639 // its operator is a lambda
4641 d_solver
->getNodeManager()->mkNode(
4642 cvc5::kind::LAMBDA
, *lbvl
.d_node
, *op
.d_node
));
4644 std::vector
<TypeNode
> cargst
= Sort::sortVectorToTypeNodes(cargs
);
4645 dt
.d_dtype
->addSygusConstructor(*op
.d_node
, ssCName
.str(), cargst
);
4647 CVC5_API_TRY_CATCH_END
;
4650 Term
Grammar::purifySygusGTerm(
4652 std::vector
<Term
>& args
,
4653 std::vector
<Sort
>& cargs
,
4654 const std::unordered_map
<Term
, Sort
>& ntsToUnres
) const
4656 CVC5_API_TRY_CATCH_BEGIN
;
4657 CVC5_API_CHECK_TERM(term
);
4658 CVC5_API_CHECK_TERMS(args
);
4659 CVC5_API_CHECK_SORTS(cargs
);
4660 CVC5_API_CHECK_TERMS_MAP(ntsToUnres
);
4661 //////// all checks before this line
4663 std::unordered_map
<Term
, Sort
>::const_iterator itn
= ntsToUnres
.find(term
);
4664 if (itn
!= ntsToUnres
.cend())
4668 d_solver
->getNodeManager()->mkBoundVar(term
.d_node
->getType()));
4669 args
.push_back(ret
);
4670 cargs
.push_back(itn
->second
);
4673 std::vector
<Term
> pchildren
;
4674 bool childChanged
= false;
4675 for (unsigned i
= 0, nchild
= term
.d_node
->getNumChildren(); i
< nchild
; i
++)
4677 Term ptermc
= purifySygusGTerm(
4678 Term(d_solver
, (*term
.d_node
)[i
]), args
, cargs
, ntsToUnres
);
4679 pchildren
.push_back(ptermc
);
4680 childChanged
= childChanged
|| *ptermc
.d_node
!= (*term
.d_node
)[i
];
4689 if (term
.d_node
->getMetaKind() == kind::metakind::PARAMETERIZED
)
4691 // it's an indexed operator so we should provide the op
4692 NodeBuilder
nb(term
.d_node
->getKind());
4693 nb
<< term
.d_node
->getOperator();
4694 nb
.append(Term::termVectorToNodes(pchildren
));
4695 nret
= nb
.constructNode();
4699 nret
= d_solver
->getNodeManager()->mkNode(
4700 term
.d_node
->getKind(), Term::termVectorToNodes(pchildren
));
4703 return Term(d_solver
, nret
);
4705 CVC5_API_TRY_CATCH_END
;
4708 void Grammar::addSygusConstructorVariables(DatatypeDecl
& dt
,
4709 const Sort
& sort
) const
4711 CVC5_API_TRY_CATCH_BEGIN
;
4712 CVC5_API_CHECK_DTDECL(dt
);
4713 CVC5_API_CHECK_SORT(sort
);
4714 //////// all checks before this line
4716 // each variable of appropriate type becomes a sygus constructor in dt.
4717 for (unsigned i
= 0, size
= d_sygusVars
.size(); i
< size
; i
++)
4719 Term v
= d_sygusVars
[i
];
4720 if (v
.d_node
->getType() == *sort
.d_type
)
4722 std::stringstream ss
;
4724 std::vector
<TypeNode
> cargs
;
4725 dt
.d_dtype
->addSygusConstructor(*v
.d_node
, ss
.str(), cargs
);
4729 CVC5_API_TRY_CATCH_END
;
4732 bool Grammar::containsFreeVariables(const Term
& rule
) const
4734 // we allow the argument list and non-terminal symbols to be in scope
4735 std::unordered_set
<TNode
> scope
;
4737 for (const Term
& sygusVar
: d_sygusVars
)
4739 scope
.emplace(*sygusVar
.d_node
);
4742 for (const Term
& ntsymbol
: d_ntSyms
)
4744 scope
.emplace(*ntsymbol
.d_node
);
4747 return expr::hasFreeVariablesScope(*rule
.d_node
, scope
);
4750 std::ostream
& operator<<(std::ostream
& out
, const Grammar
& grammar
)
4752 return out
<< grammar
.toString();
4755 /* -------------------------------------------------------------------------- */
4756 /* Rounding Mode for Floating Points */
4757 /* -------------------------------------------------------------------------- */
4759 const static std::unordered_map
<RoundingMode
, cvc5::RoundingMode
> s_rmodes
{
4760 {ROUND_NEAREST_TIES_TO_EVEN
,
4761 cvc5::RoundingMode::ROUND_NEAREST_TIES_TO_EVEN
},
4762 {ROUND_TOWARD_POSITIVE
, cvc5::RoundingMode::ROUND_TOWARD_POSITIVE
},
4763 {ROUND_TOWARD_NEGATIVE
, cvc5::RoundingMode::ROUND_TOWARD_NEGATIVE
},
4764 {ROUND_TOWARD_ZERO
, cvc5::RoundingMode::ROUND_TOWARD_ZERO
},
4765 {ROUND_NEAREST_TIES_TO_AWAY
,
4766 cvc5::RoundingMode::ROUND_NEAREST_TIES_TO_AWAY
},
4769 const static std::unordered_map
<cvc5::RoundingMode
,
4771 cvc5::RoundingModeHashFunction
>
4773 {cvc5::RoundingMode::ROUND_NEAREST_TIES_TO_EVEN
,
4774 ROUND_NEAREST_TIES_TO_EVEN
},
4775 {cvc5::RoundingMode::ROUND_TOWARD_POSITIVE
, ROUND_TOWARD_POSITIVE
},
4776 {cvc5::RoundingMode::ROUND_TOWARD_POSITIVE
, ROUND_TOWARD_NEGATIVE
},
4777 {cvc5::RoundingMode::ROUND_TOWARD_ZERO
, ROUND_TOWARD_ZERO
},
4778 {cvc5::RoundingMode::ROUND_NEAREST_TIES_TO_AWAY
,
4779 ROUND_NEAREST_TIES_TO_AWAY
},
4782 /* -------------------------------------------------------------------------- */
4784 /* -------------------------------------------------------------------------- */
4786 DriverOptions::DriverOptions(const Solver
& solver
) : d_solver(solver
) {}
4788 std::istream
& DriverOptions::in() const
4790 return *d_solver
.d_slv
->getOptions().base
.in
;
4792 std::ostream
& DriverOptions::err() const
4794 return *d_solver
.d_slv
->getOptions().base
.err
;
4796 std::ostream
& DriverOptions::out() const
4798 return *d_solver
.d_slv
->getOptions().base
.out
;
4801 /* -------------------------------------------------------------------------- */
4803 /* -------------------------------------------------------------------------- */
4805 struct Stat::StatData
4807 cvc5::StatExportData data
;
4808 template <typename T
>
4809 StatData(T
&& t
) : data(std::forward
<T
>(t
))
4812 StatData() : data() {}
4816 Stat::Stat(const Stat
& s
)
4817 : d_expert(s
.d_expert
),
4818 d_default(s
.d_default
),
4819 d_data(std::make_unique
<StatData
>(s
.d_data
->data
))
4822 Stat
& Stat::operator=(const Stat
& s
)
4824 d_expert
= s
.d_expert
;
4825 d_data
= std::make_unique
<StatData
>(s
.d_data
->data
);
4829 bool Stat::isExpert() const { return d_expert
; }
4830 bool Stat::isDefault() const { return d_default
; }
4832 bool Stat::isInt() const
4834 return std::holds_alternative
<int64_t>(d_data
->data
);
4836 int64_t Stat::getInt() const
4838 CVC5_API_TRY_CATCH_BEGIN
;
4839 CVC5_API_RECOVERABLE_CHECK(isInt()) << "Expected Stat of type int64_t.";
4840 return std::get
<int64_t>(d_data
->data
);
4841 CVC5_API_TRY_CATCH_END
;
4843 bool Stat::isDouble() const
4845 return std::holds_alternative
<double>(d_data
->data
);
4847 double Stat::getDouble() const
4849 CVC5_API_TRY_CATCH_BEGIN
;
4850 CVC5_API_RECOVERABLE_CHECK(isDouble()) << "Expected Stat of type double.";
4851 return std::get
<double>(d_data
->data
);
4852 CVC5_API_TRY_CATCH_END
;
4854 bool Stat::isString() const
4856 return std::holds_alternative
<std::string
>(d_data
->data
);
4858 const std::string
& Stat::getString() const
4860 CVC5_API_TRY_CATCH_BEGIN
;
4861 CVC5_API_RECOVERABLE_CHECK(isString())
4862 << "Expected Stat of type std::string.";
4863 return std::get
<std::string
>(d_data
->data
);
4864 CVC5_API_TRY_CATCH_END
;
4866 bool Stat::isHistogram() const
4868 return std::holds_alternative
<HistogramData
>(d_data
->data
);
4870 const Stat::HistogramData
& Stat::getHistogram() const
4872 CVC5_API_TRY_CATCH_BEGIN
;
4873 CVC5_API_RECOVERABLE_CHECK(isHistogram())
4874 << "Expected Stat of type histogram.";
4875 return std::get
<HistogramData
>(d_data
->data
);
4876 CVC5_API_TRY_CATCH_END
;
4879 Stat::Stat(bool expert
, bool defaulted
, StatData
&& sd
)
4881 d_default(defaulted
),
4882 d_data(std::make_unique
<StatData
>(std::move(sd
)))
4886 std::ostream
& operator<<(std::ostream
& os
, const Stat
& sv
)
4888 return cvc5::detail::print(os
, sv
.d_data
->data
);
4891 Statistics::BaseType::const_reference
Statistics::iterator::operator*() const
4893 return d_it
.operator*();
4895 Statistics::BaseType::const_pointer
Statistics::iterator::operator->() const
4897 return d_it
.operator->();
4899 Statistics::iterator
& Statistics::iterator::operator++()
4904 } while (!isVisible());
4907 Statistics::iterator
Statistics::iterator::operator++(int)
4909 iterator tmp
= *this;
4913 } while (!isVisible());
4916 Statistics::iterator
& Statistics::iterator::operator--()
4921 } while (!isVisible());
4924 Statistics::iterator
Statistics::iterator::operator--(int)
4926 iterator tmp
= *this;
4930 } while (!isVisible());
4933 bool Statistics::iterator::operator==(const Statistics::iterator
& rhs
) const
4935 return d_it
== rhs
.d_it
;
4937 bool Statistics::iterator::operator!=(const Statistics::iterator
& rhs
) const
4939 return d_it
!= rhs
.d_it
;
4941 Statistics::iterator::iterator(Statistics::BaseType::const_iterator it
,
4942 const Statistics::BaseType
& base
,
4945 : d_it(it
), d_base(&base
), d_showExpert(expert
), d_showDefault(defaulted
)
4947 while (!isVisible())
4952 bool Statistics::iterator::isVisible() const
4954 if (d_it
== d_base
->end()) return true;
4955 if (!d_showExpert
&& d_it
->second
.isExpert()) return false;
4956 if (!d_showDefault
&& d_it
->second
.isDefault()) return false;
4960 const Stat
& Statistics::get(const std::string
& name
)
4962 CVC5_API_TRY_CATCH_BEGIN
;
4963 auto it
= d_stats
.find(name
);
4964 CVC5_API_RECOVERABLE_CHECK(it
!= d_stats
.end())
4965 << "No stat with name \"" << name
<< "\" exists.";
4967 CVC5_API_TRY_CATCH_END
;
4970 Statistics::iterator
Statistics::begin(bool expert
, bool defaulted
) const
4972 return iterator(d_stats
.begin(), d_stats
, expert
, defaulted
);
4974 Statistics::iterator
Statistics::end() const
4976 return iterator(d_stats
.end(), d_stats
, false, false);
4979 Statistics::Statistics(const StatisticsRegistry
& reg
)
4981 for (const auto& svp
: reg
)
4983 d_stats
.emplace(svp
.first
,
4984 Stat(svp
.second
->d_expert
,
4985 svp
.second
->isDefault(),
4986 svp
.second
->getViewer()));
4990 std::ostream
& operator<<(std::ostream
& out
, const Statistics
& stats
)
4992 for (const auto& stat
: stats
)
4994 out
<< stat
.first
<< " = " << stat
.second
<< std::endl
;
4999 /* -------------------------------------------------------------------------- */
5001 /* -------------------------------------------------------------------------- */
5003 Solver::Solver(std::unique_ptr
<Options
>&& original
)
5005 d_nodeMgr
= NodeManager::currentNM();
5007 d_originalOptions
= std::move(original
);
5008 d_slv
.reset(new SolverEngine(d_nodeMgr
, d_originalOptions
.get()));
5009 d_slv
->setSolver(this);
5010 d_rng
.reset(new Random(d_slv
->getOptions().driver
.seed
));
5014 Solver::Solver() : Solver(std::make_unique
<Options
>()) {}
5016 Solver::~Solver() {}
5018 /* Helpers and private functions */
5019 /* -------------------------------------------------------------------------- */
5021 NodeManager
* Solver::getNodeManager(void) const { return d_nodeMgr
; }
5023 void Solver::increment_term_stats(Kind kind
) const
5025 if constexpr (configuration::isStatisticsBuild())
5027 d_stats
->d_terms
<< kind
;
5031 void Solver::increment_vars_consts_stats(const Sort
& sort
, bool is_var
) const
5033 if constexpr (configuration::isStatisticsBuild())
5035 const TypeNode tn
= sort
.getTypeNode();
5036 TypeConstant tc
= tn
.getKind() == cvc5::kind::TYPE_CONSTANT
5037 ? tn
.getConst
<TypeConstant
>()
5041 d_stats
->d_vars
<< tc
;
5045 d_stats
->d_consts
<< tc
;
5050 /* Split out to avoid nested API calls (problematic with API tracing). */
5051 /* .......................................................................... */
5053 template <typename T
>
5054 Term
Solver::mkValHelper(const T
& t
) const
5056 //////// all checks before this line
5057 Node res
= getNodeManager()->mkConst(t
);
5058 (void)res
.getType(true); /* kick off type checking */
5059 return Term(this, res
);
5062 Term
Solver::mkRationalValHelper(const Rational
& r
, bool isInt
) const
5064 //////// all checks before this line
5065 NodeManager
* nm
= getNodeManager();
5066 Node res
= isInt
? nm
->mkConstInt(r
) : nm
->mkConstReal(r
);
5067 (void)res
.getType(true); /* kick off type checking */
5068 api::Term t
= Term(this, res
);
5069 // NOTE: this block will be eliminated when arithmetic subtyping is eliminated
5072 t
= ensureRealSort(t
);
5077 Term
Solver::mkRealOrIntegerFromStrHelper(const std::string
& s
,
5080 //////// all checks before this line
5083 cvc5::Rational r
= s
.find('/') != std::string::npos
5085 : cvc5::Rational::fromDecimal(s
);
5086 return mkRationalValHelper(r
, isInt
);
5088 catch (const std::invalid_argument
& e
)
5090 /* Catch to throw with a more meaningful error message. To be caught in
5091 * enclosing CVC5_API_TRY_CATCH_* block to throw CVC5ApiException. */
5092 std::stringstream message
;
5093 message
<< "Cannot construct Real or Int from string argument '" << s
<< "'"
5095 throw std::invalid_argument(message
.str());
5099 Term
Solver::mkBVFromIntHelper(uint32_t size
, uint64_t val
) const
5101 CVC5_API_ARG_CHECK_EXPECTED(size
> 0, size
) << "a bit-width > 0";
5102 //////// all checks before this line
5103 return mkValHelper
<cvc5::BitVector
>(cvc5::BitVector(size
, val
));
5106 Term
Solver::mkBVFromStrHelper(uint32_t size
,
5107 const std::string
& s
,
5108 uint32_t base
) const
5110 CVC5_API_ARG_CHECK_EXPECTED(size
> 0, size
) << "a bit-width > 0";
5111 CVC5_API_ARG_CHECK_EXPECTED(!s
.empty(), s
) << "a non-empty string";
5112 CVC5_API_ARG_CHECK_EXPECTED(base
== 2 || base
== 10 || base
== 16, base
)
5113 << "base 2, 10, or 16";
5114 //////// all checks before this line
5116 Integer
val(s
, base
);
5118 if (val
.strictlyNegative())
5120 CVC5_API_CHECK(val
>= -Integer(2).pow(size
- 1))
5121 << "Overflow in bitvector construction (specified bitvector size "
5122 << size
<< " too small to hold value " << s
<< ")";
5126 CVC5_API_CHECK(val
.modByPow2(size
) == val
)
5127 << "Overflow in bitvector construction (specified bitvector size "
5128 << size
<< " too small to hold value " << s
<< ")";
5130 return mkValHelper
<cvc5::BitVector
>(cvc5::BitVector(size
, val
));
5133 Term
Solver::getValueHelper(const Term
& term
) const
5135 // Note: Term is checked in the caller to avoid double checks
5136 bool wasShadow
= false;
5137 bool freeOrShadowedVar
=
5138 expr::hasFreeOrShadowedVar(term
.getNode(), wasShadow
);
5139 CVC5_API_RECOVERABLE_CHECK(!freeOrShadowedVar
)
5140 << "Cannot get value of term containing "
5141 << (wasShadow
? "shadowed" : "free") << " variables";
5142 //////// all checks before this line
5143 Node value
= d_slv
->getValue(*term
.d_node
);
5144 Term res
= Term(this, value
);
5145 // May need to wrap in real cast so that user know this is a real.
5146 TypeNode tn
= (*term
.d_node
).getType();
5147 if (!tn
.isInteger() && value
.getType().isInteger())
5149 return ensureRealSort(res
);
5154 Sort
Solver::mkTupleSortHelper(const std::vector
<Sort
>& sorts
) const
5156 // Note: Sorts are checked in the caller to avoid double checks
5157 //////// all checks before this line
5158 std::vector
<TypeNode
> typeNodes
= Sort::sortVectorToTypeNodes(sorts
);
5159 return Sort(this, getNodeManager()->mkTupleType(typeNodes
));
5162 Term
Solver::mkTermFromKind(Kind kind
) const
5164 CVC5_API_KIND_CHECK_EXPECTED(kind
== PI
|| kind
== REGEXP_NONE
5165 || kind
== REGEXP_ALL
5166 || kind
== REGEXP_ALLCHAR
|| kind
== SEP_EMP
,
5168 << "PI, REGEXP_NONE, REGEXP_ALL, REGEXP_ALLCHAR or SEP_EMP";
5169 //////// all checks before this line
5171 cvc5::Kind k
= extToIntKind(kind
);
5172 if (kind
== REGEXP_NONE
|| kind
== REGEXP_ALL
|| kind
== REGEXP_ALLCHAR
)
5174 Assert(isDefinedIntKind(k
));
5175 res
= d_nodeMgr
->mkNode(k
, std::vector
<Node
>());
5177 else if (kind
== SEP_EMP
)
5179 res
= d_nodeMgr
->mkNullaryOperator(d_nodeMgr
->booleanType(), k
);
5184 res
= d_nodeMgr
->mkNullaryOperator(d_nodeMgr
->realType(), k
);
5186 (void)res
.getType(true); /* kick off type checking */
5187 increment_term_stats(kind
);
5188 return Term(this, res
);
5191 Term
Solver::mkTermHelper(Kind kind
, const std::vector
<Term
>& children
) const
5193 // Note: Kind and children are checked in the caller to avoid double checks
5194 //////// all checks before this line
5195 if (children
.size() == 0)
5197 return mkTermFromKind(kind
);
5199 std::vector
<Node
> echildren
= Term::termVectorToNodes(children
);
5200 cvc5::Kind k
= extToIntKind(kind
);
5202 if (echildren
.size() > 2)
5204 if (kind
== INTS_DIVISION
|| kind
== XOR
|| kind
== SUB
|| kind
== DIVISION
5205 || kind
== HO_APPLY
|| kind
== REGEXP_DIFF
)
5207 // left-associative, but cvc5 internally only supports 2 args
5208 res
= d_nodeMgr
->mkLeftAssociative(k
, echildren
);
5210 else if (kind
== IMPLIES
)
5212 // right-associative, but cvc5 internally only supports 2 args
5213 res
= d_nodeMgr
->mkRightAssociative(k
, echildren
);
5215 else if (kind
== EQUAL
|| kind
== LT
|| kind
== GT
|| kind
== LEQ
5218 // "chainable", but cvc5 internally only supports 2 args
5219 res
= d_nodeMgr
->mkChain(k
, echildren
);
5221 else if (kind::isAssociative(k
))
5223 // mkAssociative has special treatment for associative operators with lots
5225 res
= d_nodeMgr
->mkAssociative(k
, echildren
);
5229 // default case, must check kind
5230 checkMkTerm(kind
, children
.size());
5231 res
= d_nodeMgr
->mkNode(k
, echildren
);
5234 else if (kind::isAssociative(k
))
5236 // associative case, same as above
5237 checkMkTerm(kind
, children
.size());
5238 res
= d_nodeMgr
->mkAssociative(k
, echildren
);
5242 // default case, same as above
5243 checkMkTerm(kind
, children
.size());
5244 if (kind
== api::SET_SINGLETON
)
5246 // the type of the term is the same as the type of the internal node
5247 // see Term::getSort()
5248 TypeNode type
= children
[0].d_node
->getType();
5249 // Internally NodeManager::mkSingleton needs a type argument
5250 // to construct a singleton, since there is no difference between
5251 // integers and reals (both are Rationals).
5252 // At the API, mkReal and mkInteger are different and therefore the
5253 // element type can be used safely here.
5254 res
= getNodeManager()->mkSingleton(type
, *children
[0].d_node
);
5256 else if (kind
== api::BAG_MAKE
)
5258 // the type of the term is the same as the type of the internal node
5259 // see Term::getSort()
5260 TypeNode type
= children
[0].d_node
->getType();
5261 // Internally NodeManager::mkBag needs a type argument
5262 // to construct a bag, since there is no difference between
5263 // integers and reals (both are Rationals).
5264 // At the API, mkReal and mkInteger are different and therefore the
5265 // element type can be used safely here.
5266 res
= getNodeManager()->mkBag(
5267 type
, *children
[0].d_node
, *children
[1].d_node
);
5269 else if (kind
== api::SEQ_UNIT
)
5271 // the type of the term is the same as the type of the internal node
5272 // see Term::getSort()
5273 TypeNode type
= children
[0].d_node
->getType();
5274 res
= getNodeManager()->mkSeqUnit(type
, *children
[0].d_node
);
5278 res
= d_nodeMgr
->mkNode(k
, echildren
);
5282 (void)res
.getType(true); /* kick off type checking */
5283 increment_term_stats(kind
);
5284 return Term(this, res
);
5287 Term
Solver::mkTermHelper(const Op
& op
, const std::vector
<Term
>& children
) const
5289 if (!op
.isIndexedHelper())
5291 return mkTermHelper(op
.d_kind
, children
);
5294 // Note: Op and children are checked in the caller to avoid double checks
5295 checkMkTerm(op
.d_kind
, children
.size());
5296 //////// all checks before this line
5298 const cvc5::Kind int_kind
= extToIntKind(op
.d_kind
);
5299 std::vector
<Node
> echildren
= Term::termVectorToNodes(children
);
5301 NodeBuilder
nb(int_kind
);
5303 nb
.append(echildren
);
5304 Node res
= nb
.constructNode();
5306 (void)res
.getType(true); /* kick off type checking */
5307 return Term(this, res
);
5310 std::vector
<Sort
> Solver::mkDatatypeSortsInternal(
5311 const std::vector
<DatatypeDecl
>& dtypedecls
,
5312 const std::set
<Sort
>& unresolvedSorts
) const
5314 // Note: dtypedecls and unresolvedSorts are checked in the caller to avoid
5316 //////// all checks before this line
5318 std::vector
<cvc5::DType
> datatypes
;
5319 for (size_t i
= 0, ndts
= dtypedecls
.size(); i
< ndts
; ++i
)
5321 datatypes
.push_back(dtypedecls
[i
].getDatatype());
5324 std::set
<TypeNode
> utypes
= Sort::sortSetToTypeNodes(unresolvedSorts
);
5325 std::vector
<cvc5::TypeNode
> dtypes
=
5326 getNodeManager()->mkMutualDatatypeTypes(datatypes
, utypes
);
5327 std::vector
<Sort
> retTypes
= Sort::typeNodeVectorToSorts(this, dtypes
);
5331 Term
Solver::synthFunHelper(const std::string
& symbol
,
5332 const std::vector
<Term
>& boundVars
,
5335 Grammar
* grammar
) const
5337 // Note: boundVars, sort and grammar are checked in the caller to avoid
5339 std::vector
<TypeNode
> varTypes
;
5340 for (const auto& bv
: boundVars
)
5344 CVC5_API_CHECK(grammar
->d_ntSyms
[0].d_node
->getType() == *sort
.d_type
)
5345 << "Invalid Start symbol for grammar, Expected Start's sort to be "
5346 << *sort
.d_type
<< " but found "
5347 << grammar
->d_ntSyms
[0].d_node
->getType();
5349 varTypes
.push_back(bv
.d_node
->getType());
5351 //////// all checks before this line
5353 TypeNode funType
= varTypes
.empty() ? *sort
.d_type
5354 : getNodeManager()->mkFunctionType(
5355 varTypes
, *sort
.d_type
);
5357 Node fun
= getNodeManager()->mkBoundVar(symbol
, funType
);
5358 (void)fun
.getType(true); /* kick off type checking */
5360 std::vector
<Node
> bvns
= Term::termVectorToNodes(boundVars
);
5362 d_slv
->declareSynthFun(
5364 grammar
== nullptr ? funType
: *grammar
->resolve().d_type
,
5368 return Term(this, fun
);
5371 Term
Solver::ensureTermSort(const Term
& term
, const Sort
& sort
) const
5373 // Note: Term and sort are checked in the caller to avoid double checks
5374 CVC5_API_CHECK(term
.getSort() == sort
5375 || (term
.getSort().isInteger() && sort
.isReal()))
5376 << "Expected conversion from Int to Real";
5377 //////// all checks before this line
5379 Sort t
= term
.getSort();
5380 if (term
.getSort() == sort
)
5385 // Integers are reals, too
5386 Assert(t
.d_type
->isReal());
5390 // Must cast to Real to ensure correct type is passed to parametric type
5391 // constructors. We do this cast using division with 1. This has the
5392 // advantage wrt using TO_REAL since (constant) division is always included
5395 d_nodeMgr
->mkNode(extToIntKind(DIVISION
),
5397 d_nodeMgr
->mkConst(kind::CONST_RATIONAL
,
5398 cvc5::Rational(1))));
5400 Assert(res
.getSort() == sort
);
5404 Term
Solver::ensureRealSort(const Term
& t
) const
5406 Assert(this == t
.d_solver
);
5407 CVC5_API_ARG_CHECK_EXPECTED(
5408 t
.getSort() == getIntegerSort() || t
.getSort() == getRealSort(),
5409 " an integer or real term");
5410 // Note: Term is checked in the caller to avoid double checks
5411 //////// all checks before this line
5412 if (t
.getSort() == getIntegerSort())
5414 Node n
= getNodeManager()->mkNode(kind::CAST_TO_REAL
, *t
.d_node
);
5415 return Term(this, n
);
5420 bool Solver::isValidInteger(const std::string
& s
) const
5422 //////// all checks before this line
5423 if (s
.length() == 0)
5425 // string should not be empty
5430 if (s
[index
] == '-')
5432 if (s
.length() == 1)
5434 // negative integers should contain at least one digit
5440 if (s
[index
] == '0' && s
.length() > (index
+ 1))
5442 // From SMT-Lib 2.6: A <numeral> is the digit 0 or a non-empty sequence of
5443 // digits not starting with 0. So integers like 001, 000 are not allowed
5447 // all remaining characters should be decimal digits
5448 for (; index
< s
.length(); ++index
)
5450 if (!std::isdigit(s
[index
]))
5459 void Solver::ensureWellFormedTerm(const Term
& t
) const
5461 // only check if option is set
5462 if (d_slv
->getOptions().expr
.wellFormedChecking
)
5464 bool wasShadow
= false;
5465 if (expr::hasFreeOrShadowedVar(*t
.d_node
, wasShadow
))
5467 std::stringstream se
;
5468 se
<< "Cannot process term with " << (wasShadow
? "shadowed" : "free")
5470 throw CVC5ApiException(se
.str().c_str());
5475 void Solver::ensureWellFormedTerms(const std::vector
<Term
>& ts
) const
5477 // only check if option is set
5478 if (d_slv
->getOptions().expr
.wellFormedChecking
)
5480 for (const Term
& t
: ts
)
5482 ensureWellFormedTerm(t
);
5487 void Solver::resetStatistics()
5489 if constexpr (configuration::isStatisticsBuild())
5491 d_stats
.reset(new APIStatistics
{
5492 d_slv
->getStatisticsRegistry().registerHistogram
<TypeConstant
>(
5494 d_slv
->getStatisticsRegistry().registerHistogram
<TypeConstant
>(
5496 d_slv
->getStatisticsRegistry().registerHistogram
<Kind
>("api::TERM"),
5501 void Solver::printStatisticsSafe(int fd
) const
5503 d_slv
->printStatisticsSafe(fd
);
5506 /* Helpers for mkTerm checks. */
5507 /* .......................................................................... */
5509 void Solver::checkMkTerm(Kind kind
, uint32_t nchildren
) const
5511 CVC5_API_KIND_CHECK(kind
);
5512 Assert(isDefinedIntKind(extToIntKind(kind
)));
5513 const cvc5::kind::MetaKind mk
= kind::metaKindOf(extToIntKind(kind
));
5514 CVC5_API_KIND_CHECK_EXPECTED(
5515 mk
== kind::metakind::PARAMETERIZED
|| mk
== kind::metakind::OPERATOR
,
5517 << "Only operator-style terms are created with mkTerm(), "
5518 "to create variables, constants and values see mkVar(), mkConst() "
5519 "and the respective theory-specific functions to create values, "
5520 "e.g., mkBitVector().";
5521 CVC5_API_KIND_CHECK_EXPECTED(
5522 nchildren
>= minArity(kind
) && nchildren
<= maxArity(kind
), kind
)
5523 << "Terms with kind " << kindToString(kind
) << " must have at least "
5524 << minArity(kind
) << " children and at most " << maxArity(kind
)
5525 << " children (the one under construction has " << nchildren
<< ")";
5528 /* Sorts Handling */
5529 /* -------------------------------------------------------------------------- */
5531 Sort
Solver::getNullSort(void) const
5533 CVC5_API_TRY_CATCH_BEGIN
;
5534 //////// all checks before this line
5535 return Sort(this, TypeNode());
5537 CVC5_API_TRY_CATCH_END
;
5540 Sort
Solver::getBooleanSort(void) const
5542 CVC5_API_TRY_CATCH_BEGIN
;
5543 //////// all checks before this line
5544 return Sort(this, getNodeManager()->booleanType());
5546 CVC5_API_TRY_CATCH_END
;
5549 Sort
Solver::getIntegerSort(void) const
5551 CVC5_API_TRY_CATCH_BEGIN
;
5552 //////// all checks before this line
5553 return Sort(this, getNodeManager()->integerType());
5555 CVC5_API_TRY_CATCH_END
;
5558 Sort
Solver::getRealSort(void) const
5560 CVC5_API_TRY_CATCH_BEGIN
;
5561 //////// all checks before this line
5562 return Sort(this, getNodeManager()->realType());
5564 CVC5_API_TRY_CATCH_END
;
5567 Sort
Solver::getRegExpSort(void) const
5569 CVC5_API_TRY_CATCH_BEGIN
;
5570 //////// all checks before this line
5571 return Sort(this, getNodeManager()->regExpType());
5573 CVC5_API_TRY_CATCH_END
;
5576 Sort
Solver::getStringSort(void) const
5578 CVC5_API_TRY_CATCH_BEGIN
;
5579 //////// all checks before this line
5580 return Sort(this, getNodeManager()->stringType());
5582 CVC5_API_TRY_CATCH_END
;
5585 Sort
Solver::getRoundingModeSort(void) const
5587 CVC5_API_TRY_CATCH_BEGIN
;
5588 //////// all checks before this line
5589 return Sort(this, getNodeManager()->roundingModeType());
5591 CVC5_API_TRY_CATCH_END
;
5594 /* Create sorts ------------------------------------------------------- */
5596 Sort
Solver::mkArraySort(const Sort
& indexSort
, const Sort
& elemSort
) const
5598 CVC5_API_TRY_CATCH_BEGIN
;
5599 CVC5_API_SOLVER_CHECK_SORT(indexSort
);
5600 CVC5_API_SOLVER_CHECK_SORT(elemSort
);
5601 //////// all checks before this line
5603 this, getNodeManager()->mkArrayType(*indexSort
.d_type
, *elemSort
.d_type
));
5605 CVC5_API_TRY_CATCH_END
;
5608 Sort
Solver::mkBitVectorSort(uint32_t size
) const
5610 CVC5_API_TRY_CATCH_BEGIN
;
5611 CVC5_API_ARG_CHECK_EXPECTED(size
> 0, size
) << "size > 0";
5612 //////// all checks before this line
5613 return Sort(this, getNodeManager()->mkBitVectorType(size
));
5615 CVC5_API_TRY_CATCH_END
;
5618 Sort
Solver::mkFloatingPointSort(uint32_t exp
, uint32_t sig
) const
5620 CVC5_API_TRY_CATCH_BEGIN
;
5621 CVC5_API_ARG_CHECK_EXPECTED(exp
> 0, exp
) << "exponent size > 0";
5622 CVC5_API_ARG_CHECK_EXPECTED(sig
> 0, sig
) << "significand size > 0";
5623 //////// all checks before this line
5624 return Sort(this, getNodeManager()->mkFloatingPointType(exp
, sig
));
5626 CVC5_API_TRY_CATCH_END
;
5629 Sort
Solver::mkDatatypeSort(const DatatypeDecl
& dtypedecl
) const
5631 CVC5_API_TRY_CATCH_BEGIN
;
5632 CVC5_API_SOLVER_CHECK_DTDECL(dtypedecl
);
5633 //////// all checks before this line
5634 return Sort(this, getNodeManager()->mkDatatypeType(*dtypedecl
.d_dtype
));
5636 CVC5_API_TRY_CATCH_END
;
5639 std::vector
<Sort
> Solver::mkDatatypeSorts(
5640 const std::vector
<DatatypeDecl
>& dtypedecls
) const
5642 CVC5_API_SOLVER_CHECK_DTDECLS(dtypedecls
);
5643 CVC5_API_TRY_CATCH_BEGIN
;
5644 //////// all checks before this line
5645 return mkDatatypeSortsInternal(dtypedecls
, {});
5647 CVC5_API_TRY_CATCH_END
;
5650 std::vector
<Sort
> Solver::mkDatatypeSorts(
5651 const std::vector
<DatatypeDecl
>& dtypedecls
,
5652 const std::set
<Sort
>& unresolvedSorts
) const
5654 CVC5_API_TRY_CATCH_BEGIN
;
5655 CVC5_API_SOLVER_CHECK_DTDECLS(dtypedecls
);
5656 CVC5_API_SOLVER_CHECK_SORTS(unresolvedSorts
);
5657 //////// all checks before this line
5658 return mkDatatypeSortsInternal(dtypedecls
, unresolvedSorts
);
5660 CVC5_API_TRY_CATCH_END
;
5663 Sort
Solver::mkFunctionSort(const Sort
& domain
, const Sort
& codomain
) const
5665 CVC5_API_TRY_CATCH_BEGIN
;
5666 CVC5_API_SOLVER_CHECK_DOMAIN_SORT(domain
);
5667 CVC5_API_SOLVER_CHECK_CODOMAIN_SORT(codomain
);
5668 //////// all checks before this line
5670 this, getNodeManager()->mkFunctionType(*domain
.d_type
, *codomain
.d_type
));
5672 CVC5_API_TRY_CATCH_END
;
5675 Sort
Solver::mkFunctionSort(const std::vector
<Sort
>& sorts
,
5676 const Sort
& codomain
) const
5678 CVC5_API_TRY_CATCH_BEGIN
;
5679 CVC5_API_ARG_SIZE_CHECK_EXPECTED(sorts
.size() >= 1, sorts
)
5680 << "at least one parameter sort for function sort";
5681 CVC5_API_SOLVER_CHECK_DOMAIN_SORTS(sorts
);
5682 CVC5_API_SOLVER_CHECK_CODOMAIN_SORT(codomain
);
5683 //////// all checks before this line
5684 std::vector
<TypeNode
> argTypes
= Sort::sortVectorToTypeNodes(sorts
);
5686 getNodeManager()->mkFunctionType(argTypes
, *codomain
.d_type
));
5688 CVC5_API_TRY_CATCH_END
;
5691 Sort
Solver::mkParamSort(const std::string
& symbol
) const
5693 CVC5_API_TRY_CATCH_BEGIN
;
5694 //////// all checks before this line
5697 getNodeManager()->mkSort(symbol
, NodeManager::SORT_FLAG_PLACEHOLDER
));
5699 CVC5_API_TRY_CATCH_END
;
5702 Sort
Solver::mkPredicateSort(const std::vector
<Sort
>& sorts
) const
5704 CVC5_API_TRY_CATCH_BEGIN
;
5705 CVC5_API_ARG_SIZE_CHECK_EXPECTED(sorts
.size() >= 1, sorts
)
5706 << "at least one parameter sort for predicate sort";
5707 CVC5_API_SOLVER_CHECK_DOMAIN_SORTS(sorts
);
5708 //////// all checks before this line
5711 getNodeManager()->mkPredicateType(Sort::sortVectorToTypeNodes(sorts
)));
5713 CVC5_API_TRY_CATCH_END
;
5716 Sort
Solver::mkRecordSort(
5717 const std::vector
<std::pair
<std::string
, Sort
>>& fields
) const
5719 CVC5_API_TRY_CATCH_BEGIN
;
5720 std::vector
<std::pair
<std::string
, TypeNode
>> f
;
5721 for (size_t i
= 0, size
= fields
.size(); i
< size
; ++i
)
5723 const auto& p
= fields
[i
];
5724 CVC5_API_ARG_AT_INDEX_CHECK_EXPECTED(!p
.second
.isNull(), "sort", fields
, i
)
5726 CVC5_API_ARG_AT_INDEX_CHECK_EXPECTED(
5727 this == p
.second
.d_solver
, "sort", fields
, i
)
5728 << "sort associated with this solver object";
5729 f
.emplace_back(p
.first
, *p
.second
.d_type
);
5731 //////// all checks before this line
5732 return Sort(this, getNodeManager()->mkRecordType(f
));
5734 CVC5_API_TRY_CATCH_END
;
5737 Sort
Solver::mkSetSort(const Sort
& elemSort
) const
5739 CVC5_API_TRY_CATCH_BEGIN
;
5740 CVC5_API_SOLVER_CHECK_SORT(elemSort
);
5741 //////// all checks before this line
5742 return Sort(this, getNodeManager()->mkSetType(*elemSort
.d_type
));
5744 CVC5_API_TRY_CATCH_END
;
5747 Sort
Solver::mkBagSort(const Sort
& elemSort
) const
5749 CVC5_API_TRY_CATCH_BEGIN
;
5750 CVC5_API_SOLVER_CHECK_SORT(elemSort
);
5751 //////// all checks before this line
5752 return Sort(this, getNodeManager()->mkBagType(*elemSort
.d_type
));
5754 CVC5_API_TRY_CATCH_END
;
5757 Sort
Solver::mkSequenceSort(const Sort
& elemSort
) const
5759 CVC5_API_TRY_CATCH_BEGIN
;
5760 CVC5_API_SOLVER_CHECK_SORT(elemSort
);
5761 //////// all checks before this line
5762 return Sort(this, getNodeManager()->mkSequenceType(*elemSort
.d_type
));
5764 CVC5_API_TRY_CATCH_END
;
5767 Sort
Solver::mkUninterpretedSort(const std::string
& symbol
) const
5769 CVC5_API_TRY_CATCH_BEGIN
;
5770 //////// all checks before this line
5771 return Sort(this, getNodeManager()->mkSort(symbol
));
5773 CVC5_API_TRY_CATCH_END
;
5776 Sort
Solver::mkUnresolvedSort(const std::string
& symbol
, size_t arity
) const
5778 CVC5_API_TRY_CATCH_BEGIN
;
5779 //////// all checks before this line
5782 return Sort(this, getNodeManager()->mkSortConstructor(symbol
, arity
));
5784 return Sort(this, getNodeManager()->mkSort(symbol
));
5786 CVC5_API_TRY_CATCH_END
;
5789 Sort
Solver::mkSortConstructorSort(const std::string
& symbol
,
5792 CVC5_API_TRY_CATCH_BEGIN
;
5793 CVC5_API_ARG_CHECK_EXPECTED(arity
> 0, arity
) << "an arity > 0";
5794 //////// all checks before this line
5795 return Sort(this, getNodeManager()->mkSortConstructor(symbol
, arity
));
5797 CVC5_API_TRY_CATCH_END
;
5800 Sort
Solver::mkTupleSort(const std::vector
<Sort
>& sorts
) const
5802 CVC5_API_TRY_CATCH_BEGIN
;
5803 CVC5_API_SOLVER_CHECK_SORTS_NOT_FUNCTION_LIKE(sorts
);
5804 //////// all checks before this line
5805 return mkTupleSortHelper(sorts
);
5807 CVC5_API_TRY_CATCH_END
;
5811 /* -------------------------------------------------------------------------- */
5813 Term
Solver::mkTrue(void) const
5815 CVC5_API_TRY_CATCH_BEGIN
;
5816 //////// all checks before this line
5817 return Term(this, d_nodeMgr
->mkConst
<bool>(true));
5819 CVC5_API_TRY_CATCH_END
;
5822 Term
Solver::mkFalse(void) const
5824 CVC5_API_TRY_CATCH_BEGIN
;
5825 //////// all checks before this line
5826 return Term(this, d_nodeMgr
->mkConst
<bool>(false));
5828 CVC5_API_TRY_CATCH_END
;
5831 Term
Solver::mkBoolean(bool val
) const
5833 CVC5_API_TRY_CATCH_BEGIN
;
5834 //////// all checks before this line
5835 return Term(this, d_nodeMgr
->mkConst
<bool>(val
));
5837 CVC5_API_TRY_CATCH_END
;
5840 Term
Solver::mkPi() const
5842 CVC5_API_TRY_CATCH_BEGIN
;
5843 //////// all checks before this line
5845 d_nodeMgr
->mkNullaryOperator(d_nodeMgr
->realType(), cvc5::kind::PI
);
5846 (void)res
.getType(true); /* kick off type checking */
5847 return Term(this, res
);
5849 CVC5_API_TRY_CATCH_END
;
5852 Term
Solver::mkInteger(const std::string
& s
) const
5854 CVC5_API_TRY_CATCH_BEGIN
;
5855 CVC5_API_ARG_CHECK_EXPECTED(isValidInteger(s
), s
) << " an integer ";
5856 Term integer
= mkRealOrIntegerFromStrHelper(s
);
5857 CVC5_API_ARG_CHECK_EXPECTED(integer
.getSort() == getIntegerSort(), s
)
5858 << " a string representing an integer";
5859 //////// all checks before this line
5862 CVC5_API_TRY_CATCH_END
;
5865 Term
Solver::mkInteger(int64_t val
) const
5867 CVC5_API_TRY_CATCH_BEGIN
;
5868 //////// all checks before this line
5869 Term integer
= mkRationalValHelper(cvc5::Rational(val
));
5870 Assert(integer
.getSort() == getIntegerSort());
5873 CVC5_API_TRY_CATCH_END
;
5876 Term
Solver::mkReal(const std::string
& s
) const
5878 CVC5_API_TRY_CATCH_BEGIN
;
5879 /* CLN and GMP handle this case differently, CLN interprets it as 0, GMP
5880 * throws an std::invalid_argument exception. For consistency, we treat it
5882 CVC5_API_ARG_CHECK_EXPECTED(s
!= ".", s
)
5883 << "a string representing a real or rational value.";
5884 //////// all checks before this line
5885 return mkRealOrIntegerFromStrHelper(s
, false);
5887 CVC5_API_TRY_CATCH_END
;
5890 Term
Solver::mkReal(int64_t val
) const
5892 CVC5_API_TRY_CATCH_BEGIN
;
5893 //////// all checks before this line
5894 return mkRationalValHelper(cvc5::Rational(val
), false);
5896 CVC5_API_TRY_CATCH_END
;
5899 Term
Solver::mkReal(int64_t num
, int64_t den
) const
5901 CVC5_API_TRY_CATCH_BEGIN
;
5902 //////// all checks before this line
5903 return mkRationalValHelper(cvc5::Rational(num
, den
), false);
5905 CVC5_API_TRY_CATCH_END
;
5908 Term
Solver::mkRegexpAll() const
5910 CVC5_API_TRY_CATCH_BEGIN
;
5911 //////// all checks before this line
5913 d_nodeMgr
->mkNode(cvc5::kind::REGEXP_ALL
, std::vector
<cvc5::Node
>());
5914 (void)res
.getType(true); /* kick off type checking */
5915 return Term(this, res
);
5917 CVC5_API_TRY_CATCH_END
;
5920 Term
Solver::mkRegexpNone() const
5922 CVC5_API_TRY_CATCH_BEGIN
;
5923 //////// all checks before this line
5925 d_nodeMgr
->mkNode(cvc5::kind::REGEXP_NONE
, std::vector
<cvc5::Node
>());
5926 (void)res
.getType(true); /* kick off type checking */
5927 return Term(this, res
);
5929 CVC5_API_TRY_CATCH_END
;
5932 Term
Solver::mkRegexpAllchar() const
5934 CVC5_API_TRY_CATCH_BEGIN
;
5935 //////// all checks before this line
5937 d_nodeMgr
->mkNode(cvc5::kind::REGEXP_ALLCHAR
, std::vector
<cvc5::Node
>());
5938 (void)res
.getType(true); /* kick off type checking */
5939 return Term(this, res
);
5941 CVC5_API_TRY_CATCH_END
;
5944 Term
Solver::mkEmptySet(const Sort
& sort
) const
5946 CVC5_API_TRY_CATCH_BEGIN
;
5947 CVC5_API_ARG_CHECK_EXPECTED(sort
.isNull() || sort
.isSet(), sort
)
5948 << "null sort or set sort";
5949 CVC5_API_ARG_CHECK_EXPECTED(sort
.isNull() || this == sort
.d_solver
, sort
)
5950 << "set sort associated with this solver object";
5951 //////// all checks before this line
5952 return mkValHelper
<cvc5::EmptySet
>(cvc5::EmptySet(*sort
.d_type
));
5954 CVC5_API_TRY_CATCH_END
;
5957 Term
Solver::mkEmptyBag(const Sort
& sort
) const
5959 CVC5_API_TRY_CATCH_BEGIN
;
5960 CVC5_API_ARG_CHECK_EXPECTED(sort
.isNull() || sort
.isBag(), sort
)
5961 << "null sort or bag sort";
5962 CVC5_API_ARG_CHECK_EXPECTED(sort
.isNull() || this == sort
.d_solver
, sort
)
5963 << "bag sort associated with this solver object";
5964 //////// all checks before this line
5965 return mkValHelper
<cvc5::EmptyBag
>(cvc5::EmptyBag(*sort
.d_type
));
5967 CVC5_API_TRY_CATCH_END
;
5970 Term
Solver::mkSepEmp() const
5972 CVC5_API_TRY_CATCH_BEGIN
;
5973 //////// all checks before this line
5974 Node res
= getNodeManager()->mkNullaryOperator(d_nodeMgr
->booleanType(),
5975 cvc5::Kind::SEP_EMP
);
5976 (void)res
.getType(true); /* kick off type checking */
5977 return Term(this, res
);
5979 CVC5_API_TRY_CATCH_END
;
5982 Term
Solver::mkSepNil(const Sort
& sort
) const
5984 CVC5_API_TRY_CATCH_BEGIN
;
5985 CVC5_API_SOLVER_CHECK_SORT(sort
);
5986 //////// all checks before this line
5988 getNodeManager()->mkNullaryOperator(*sort
.d_type
, cvc5::kind::SEP_NIL
);
5989 (void)res
.getType(true); /* kick off type checking */
5990 return Term(this, res
);
5992 CVC5_API_TRY_CATCH_END
;
5995 Term
Solver::mkString(const std::string
& s
, bool useEscSequences
) const
5997 CVC5_API_TRY_CATCH_BEGIN
;
5998 //////// all checks before this line
5999 return mkValHelper
<cvc5::String
>(cvc5::String(s
, useEscSequences
));
6001 CVC5_API_TRY_CATCH_END
;
6004 Term
Solver::mkString(const std::wstring
& s
) const
6006 CVC5_API_TRY_CATCH_BEGIN
;
6007 //////// all checks before this line
6008 return mkValHelper
<cvc5::String
>(cvc5::String(s
));
6010 CVC5_API_TRY_CATCH_END
;
6013 Term
Solver::mkEmptySequence(const Sort
& sort
) const
6015 CVC5_API_TRY_CATCH_BEGIN
;
6016 CVC5_API_SOLVER_CHECK_SORT(sort
);
6017 //////// all checks before this line
6018 std::vector
<Node
> seq
;
6019 Node res
= d_nodeMgr
->mkConst(Sequence(*sort
.d_type
, seq
));
6020 return Term(this, res
);
6022 CVC5_API_TRY_CATCH_END
;
6025 Term
Solver::mkUniverseSet(const Sort
& sort
) const
6027 CVC5_API_TRY_CATCH_BEGIN
;
6028 CVC5_API_SOLVER_CHECK_SORT(sort
);
6029 //////// all checks before this line
6031 Node res
= getNodeManager()->mkNullaryOperator(*sort
.d_type
,
6032 cvc5::kind::SET_UNIVERSE
);
6033 // TODO(#2771): Reenable?
6034 // (void)res->getType(true); /* kick off type checking */
6035 return Term(this, res
);
6037 CVC5_API_TRY_CATCH_END
;
6040 Term
Solver::mkBitVector(uint32_t size
, uint64_t val
) const
6042 CVC5_API_TRY_CATCH_BEGIN
;
6043 //////// all checks before this line
6044 return mkBVFromIntHelper(size
, val
);
6046 CVC5_API_TRY_CATCH_END
;
6049 Term
Solver::mkBitVector(uint32_t size
,
6050 const std::string
& s
,
6051 uint32_t base
) const
6053 CVC5_API_TRY_CATCH_BEGIN
;
6054 //////// all checks before this line
6055 return mkBVFromStrHelper(size
, s
, base
);
6057 CVC5_API_TRY_CATCH_END
;
6060 Term
Solver::mkConstArray(const Sort
& sort
, const Term
& val
) const
6062 CVC5_API_TRY_CATCH_BEGIN
;
6063 CVC5_API_SOLVER_CHECK_SORT(sort
);
6064 CVC5_API_SOLVER_CHECK_TERM(val
);
6065 CVC5_API_ARG_CHECK_EXPECTED(sort
.isArray(), sort
) << "an array sort";
6066 CVC5_API_CHECK(val
.getSort().isSubsortOf(sort
.getArrayElementSort()))
6067 << "Value does not match element sort";
6068 //////// all checks before this line
6070 // handle the special case of (CAST_TO_REAL n) where n is an integer
6071 Node n
= *val
.d_node
;
6072 if (val
.isCastedReal())
6074 // this is safe because the constant array stores its type
6078 mkValHelper
<cvc5::ArrayStoreAll
>(cvc5::ArrayStoreAll(*sort
.d_type
, n
));
6081 CVC5_API_TRY_CATCH_END
;
6084 Term
Solver::mkFloatingPointPosInf(uint32_t exp
, uint32_t sig
) const
6086 CVC5_API_TRY_CATCH_BEGIN
;
6087 //////// all checks before this line
6088 return mkValHelper
<cvc5::FloatingPoint
>(
6089 FloatingPoint::makeInf(FloatingPointSize(exp
, sig
), false));
6091 CVC5_API_TRY_CATCH_END
;
6094 Term
Solver::mkFloatingPointNegInf(uint32_t exp
, uint32_t sig
) const
6096 CVC5_API_TRY_CATCH_BEGIN
;
6097 //////// all checks before this line
6098 return mkValHelper
<cvc5::FloatingPoint
>(
6099 FloatingPoint::makeInf(FloatingPointSize(exp
, sig
), true));
6101 CVC5_API_TRY_CATCH_END
;
6104 Term
Solver::mkFloatingPointNaN(uint32_t exp
, uint32_t sig
) const
6106 CVC5_API_TRY_CATCH_BEGIN
;
6107 //////// all checks before this line
6108 return mkValHelper
<cvc5::FloatingPoint
>(
6109 FloatingPoint::makeNaN(FloatingPointSize(exp
, sig
)));
6111 CVC5_API_TRY_CATCH_END
;
6114 Term
Solver::mkFloatingPointPosZero(uint32_t exp
, uint32_t sig
) const
6116 CVC5_API_TRY_CATCH_BEGIN
;
6117 //////// all checks before this line
6118 return mkValHelper
<cvc5::FloatingPoint
>(
6119 FloatingPoint::makeZero(FloatingPointSize(exp
, sig
), false));
6121 CVC5_API_TRY_CATCH_END
;
6124 Term
Solver::mkFloatingPointNegZero(uint32_t exp
, uint32_t sig
) const
6126 CVC5_API_TRY_CATCH_BEGIN
;
6127 //////// all checks before this line
6128 return mkValHelper
<cvc5::FloatingPoint
>(
6129 FloatingPoint::makeZero(FloatingPointSize(exp
, sig
), true));
6131 CVC5_API_TRY_CATCH_END
;
6134 Term
Solver::mkRoundingMode(RoundingMode rm
) const
6136 CVC5_API_TRY_CATCH_BEGIN
;
6137 //////// all checks before this line
6138 return mkValHelper
<cvc5::RoundingMode
>(s_rmodes
.at(rm
));
6140 CVC5_API_TRY_CATCH_END
;
6143 Term
Solver::mkFloatingPoint(uint32_t exp
, uint32_t sig
, Term val
) const
6145 CVC5_API_TRY_CATCH_BEGIN
;
6146 CVC5_API_SOLVER_CHECK_TERM(val
);
6147 CVC5_API_ARG_CHECK_EXPECTED(exp
> 0, exp
) << "a value > 0";
6148 CVC5_API_ARG_CHECK_EXPECTED(sig
> 0, sig
) << "a value > 0";
6149 uint32_t bw
= exp
+ sig
;
6150 CVC5_API_ARG_CHECK_EXPECTED(bw
== val
.d_node
->getType().getBitVectorSize(),
6152 << "a bit-vector constant with bit-width '" << bw
<< "'";
6153 CVC5_API_ARG_CHECK_EXPECTED(
6154 val
.d_node
->getType().isBitVector() && val
.d_node
->isConst(), val
)
6155 << "bit-vector constant";
6156 //////// all checks before this line
6157 return mkValHelper
<cvc5::FloatingPoint
>(
6158 cvc5::FloatingPoint(exp
, sig
, val
.d_node
->getConst
<BitVector
>()));
6160 CVC5_API_TRY_CATCH_END
;
6163 Term
Solver::mkCardinalityConstraint(const Sort
& sort
, uint32_t upperBound
) const
6165 CVC5_API_TRY_CATCH_BEGIN
;
6166 CVC5_API_SOLVER_CHECK_SORT(sort
);
6167 CVC5_API_ARG_CHECK_EXPECTED(sort
.isUninterpretedSort(), sort
)
6168 << "an uninterpreted sort";
6169 CVC5_API_ARG_CHECK_EXPECTED(upperBound
> 0, upperBound
) << "a value > 0";
6170 //////// all checks before this line
6172 d_nodeMgr
->mkConst(cvc5::CardinalityConstraint(*sort
.d_type
, upperBound
));
6173 Node cc
= d_nodeMgr
->mkNode(cvc5::Kind::CARDINALITY_CONSTRAINT
, cco
);
6174 return Term(this, cc
);
6176 CVC5_API_TRY_CATCH_END
;
6179 /* Create constants */
6180 /* -------------------------------------------------------------------------- */
6182 Term
Solver::mkConst(const Sort
& sort
, const std::string
& symbol
) const
6184 CVC5_API_TRY_CATCH_BEGIN
;
6185 CVC5_API_SOLVER_CHECK_SORT(sort
);
6186 //////// all checks before this line
6187 Node res
= d_nodeMgr
->mkVar(symbol
, *sort
.d_type
);
6188 (void)res
.getType(true); /* kick off type checking */
6189 increment_vars_consts_stats(sort
, false);
6190 return Term(this, res
);
6192 CVC5_API_TRY_CATCH_END
;
6195 Term
Solver::mkConst(const Sort
& sort
) const
6197 CVC5_API_TRY_CATCH_BEGIN
;
6198 CVC5_API_SOLVER_CHECK_SORT(sort
);
6199 //////// all checks before this line
6200 Node res
= d_nodeMgr
->mkVar(*sort
.d_type
);
6201 (void)res
.getType(true); /* kick off type checking */
6202 increment_vars_consts_stats(sort
, false);
6203 return Term(this, res
);
6205 CVC5_API_TRY_CATCH_END
;
6208 /* Create variables */
6209 /* -------------------------------------------------------------------------- */
6211 Term
Solver::mkVar(const Sort
& sort
, const std::string
& symbol
) const
6213 CVC5_API_TRY_CATCH_BEGIN
;
6214 CVC5_API_SOLVER_CHECK_SORT(sort
);
6215 //////// all checks before this line
6216 Node res
= symbol
.empty() ? d_nodeMgr
->mkBoundVar(*sort
.d_type
)
6217 : d_nodeMgr
->mkBoundVar(symbol
, *sort
.d_type
);
6218 (void)res
.getType(true); /* kick off type checking */
6219 increment_vars_consts_stats(sort
, true);
6220 return Term(this, res
);
6222 CVC5_API_TRY_CATCH_END
;
6225 /* Create datatype constructor declarations */
6226 /* -------------------------------------------------------------------------- */
6228 DatatypeConstructorDecl
Solver::mkDatatypeConstructorDecl(
6229 const std::string
& name
)
6231 CVC5_API_TRY_CATCH_BEGIN
;
6232 //////// all checks before this line
6233 return DatatypeConstructorDecl(this, name
);
6235 CVC5_API_TRY_CATCH_END
;
6238 /* Create datatype declarations */
6239 /* -------------------------------------------------------------------------- */
6241 DatatypeDecl
Solver::mkDatatypeDecl(const std::string
& name
, bool isCoDatatype
)
6243 CVC5_API_TRY_CATCH_BEGIN
;
6244 //////// all checks before this line
6245 return DatatypeDecl(this, name
, isCoDatatype
);
6247 CVC5_API_TRY_CATCH_END
;
6250 DatatypeDecl
Solver::mkDatatypeDecl(const std::string
& name
,
6254 CVC5_API_TRY_CATCH_BEGIN
;
6255 CVC5_API_SOLVER_CHECK_SORT(param
);
6256 //////// all checks before this line
6257 return DatatypeDecl(this, name
, param
, isCoDatatype
);
6259 CVC5_API_TRY_CATCH_END
;
6262 DatatypeDecl
Solver::mkDatatypeDecl(const std::string
& name
,
6263 const std::vector
<Sort
>& params
,
6266 CVC5_API_TRY_CATCH_BEGIN
;
6267 CVC5_API_SOLVER_CHECK_SORTS(params
);
6268 //////// all checks before this line
6269 return DatatypeDecl(this, name
, params
, isCoDatatype
);
6271 CVC5_API_TRY_CATCH_END
;
6275 /* -------------------------------------------------------------------------- */
6277 Term
Solver::mkTerm(Kind kind
) const
6279 CVC5_API_TRY_CATCH_BEGIN
;
6280 CVC5_API_KIND_CHECK(kind
);
6281 //////// all checks before this line
6282 return mkTermFromKind(kind
);
6284 CVC5_API_TRY_CATCH_END
;
6287 Term
Solver::mkTerm(Kind kind
, const Term
& child
) const
6289 CVC5_API_TRY_CATCH_BEGIN
;
6290 CVC5_API_KIND_CHECK(kind
);
6291 CVC5_API_SOLVER_CHECK_TERM(child
);
6292 //////// all checks before this line
6293 return mkTermHelper(kind
, std::vector
<Term
>{child
});
6295 CVC5_API_TRY_CATCH_END
;
6298 Term
Solver::mkTerm(Kind kind
, const Term
& child1
, const Term
& child2
) const
6300 CVC5_API_TRY_CATCH_BEGIN
;
6301 CVC5_API_KIND_CHECK(kind
);
6302 CVC5_API_SOLVER_CHECK_TERM(child1
);
6303 CVC5_API_SOLVER_CHECK_TERM(child2
);
6304 //////// all checks before this line
6305 return mkTermHelper(kind
, std::vector
<Term
>{child1
, child2
});
6307 CVC5_API_TRY_CATCH_END
;
6310 Term
Solver::mkTerm(Kind kind
,
6313 const Term
& child3
) const
6315 CVC5_API_TRY_CATCH_BEGIN
;
6316 CVC5_API_KIND_CHECK(kind
);
6317 CVC5_API_SOLVER_CHECK_TERM(child1
);
6318 CVC5_API_SOLVER_CHECK_TERM(child2
);
6319 CVC5_API_SOLVER_CHECK_TERM(child3
);
6320 //////// all checks before this line
6321 // need to use internal term call to check e.g. associative construction
6322 return mkTermHelper(kind
, std::vector
<Term
>{child1
, child2
, child3
});
6324 CVC5_API_TRY_CATCH_END
;
6327 Term
Solver::mkTerm(Kind kind
, const std::vector
<Term
>& children
) const
6329 CVC5_API_TRY_CATCH_BEGIN
;
6330 CVC5_API_KIND_CHECK(kind
);
6331 CVC5_API_SOLVER_CHECK_TERMS(children
);
6332 //////// all checks before this line
6333 return mkTermHelper(kind
, children
);
6335 CVC5_API_TRY_CATCH_END
;
6338 Term
Solver::mkTerm(const Op
& op
) const
6340 CVC5_API_TRY_CATCH_BEGIN
;
6341 CVC5_API_SOLVER_CHECK_OP(op
);
6342 if (!op
.isIndexedHelper())
6344 return mkTermFromKind(op
.d_kind
);
6346 checkMkTerm(op
.d_kind
, 0);
6347 //////// all checks before this line
6348 const cvc5::Kind int_kind
= extToIntKind(op
.d_kind
);
6349 Term res
= Term(this, getNodeManager()->mkNode(int_kind
, *op
.d_node
));
6351 (void)res
.d_node
->getType(true); /* kick off type checking */
6354 CVC5_API_TRY_CATCH_END
;
6357 Term
Solver::mkTerm(const Op
& op
, const Term
& child
) const
6359 CVC5_API_TRY_CATCH_BEGIN
;
6360 CVC5_API_SOLVER_CHECK_OP(op
);
6361 CVC5_API_SOLVER_CHECK_TERM(child
);
6362 //////// all checks before this line
6363 return mkTermHelper(op
, std::vector
<Term
>{child
});
6365 CVC5_API_TRY_CATCH_END
;
6368 Term
Solver::mkTerm(const Op
& op
, const Term
& child1
, const Term
& child2
) const
6370 CVC5_API_TRY_CATCH_BEGIN
;
6371 CVC5_API_SOLVER_CHECK_OP(op
);
6372 CVC5_API_SOLVER_CHECK_TERM(child1
);
6373 CVC5_API_SOLVER_CHECK_TERM(child2
);
6374 //////// all checks before this line
6375 return mkTermHelper(op
, std::vector
<Term
>{child1
, child2
});
6377 CVC5_API_TRY_CATCH_END
;
6380 Term
Solver::mkTerm(const Op
& op
,
6383 const Term
& child3
) const
6385 CVC5_API_TRY_CATCH_BEGIN
;
6386 CVC5_API_SOLVER_CHECK_OP(op
);
6387 CVC5_API_SOLVER_CHECK_TERM(child1
);
6388 CVC5_API_SOLVER_CHECK_TERM(child2
);
6389 CVC5_API_SOLVER_CHECK_TERM(child3
);
6390 //////// all checks before this line
6391 return mkTermHelper(op
, std::vector
<Term
>{child1
, child2
, child3
});
6393 CVC5_API_TRY_CATCH_END
;
6396 Term
Solver::mkTerm(const Op
& op
, const std::vector
<Term
>& children
) const
6398 CVC5_API_TRY_CATCH_BEGIN
;
6399 CVC5_API_SOLVER_CHECK_OP(op
);
6400 CVC5_API_SOLVER_CHECK_TERMS(children
);
6401 //////// all checks before this line
6402 return mkTermHelper(op
, children
);
6404 CVC5_API_TRY_CATCH_END
;
6407 Term
Solver::mkTuple(const std::vector
<Sort
>& sorts
,
6408 const std::vector
<Term
>& terms
) const
6410 CVC5_API_TRY_CATCH_BEGIN
;
6411 CVC5_API_CHECK(sorts
.size() == terms
.size())
6412 << "Expected the same number of sorts and elements";
6413 CVC5_API_SOLVER_CHECK_SORTS(sorts
);
6414 CVC5_API_SOLVER_CHECK_TERMS(terms
);
6415 //////// all checks before this line
6416 std::vector
<cvc5::Node
> args
;
6417 for (size_t i
= 0, size
= sorts
.size(); i
< size
; i
++)
6419 args
.push_back(*(ensureTermSort(terms
[i
], sorts
[i
])).d_node
);
6422 Sort s
= mkTupleSortHelper(sorts
);
6423 Datatype dt
= s
.getDatatype();
6424 NodeBuilder
nb(extToIntKind(APPLY_CONSTRUCTOR
));
6425 nb
<< *dt
[0].getConstructorTerm().d_node
;
6427 Node res
= nb
.constructNode();
6428 (void)res
.getType(true); /* kick off type checking */
6429 return Term(this, res
);
6431 CVC5_API_TRY_CATCH_END
;
6434 /* Create operators */
6435 /* -------------------------------------------------------------------------- */
6437 Op
Solver::mkOp(Kind kind
) const
6439 CVC5_API_TRY_CATCH_BEGIN
;
6440 CVC5_API_KIND_CHECK(kind
);
6441 CVC5_API_CHECK(s_indexed_kinds
.find(kind
) == s_indexed_kinds
.end())
6442 << "Expected a kind for a non-indexed operator.";
6443 //////// all checks before this line
6444 return Op(this, kind
);
6446 CVC5_API_TRY_CATCH_END
6449 Op
Solver::mkOp(Kind kind
, const std::string
& arg
) const
6451 CVC5_API_TRY_CATCH_BEGIN
;
6452 CVC5_API_KIND_CHECK(kind
);
6453 CVC5_API_KIND_CHECK_EXPECTED((kind
== DIVISIBLE
), kind
) << "DIVISIBLE";
6454 //////// all checks before this line
6456 /* CLN and GMP handle this case differently, CLN interprets it as 0, GMP
6457 * throws an std::invalid_argument exception. For consistency, we treat it
6459 CVC5_API_ARG_CHECK_EXPECTED(arg
!= ".", arg
)
6460 << "a string representing an integer, real or rational value.";
6463 *mkValHelper
<cvc5::Divisible
>(cvc5::Divisible(cvc5::Integer(arg
)))
6467 CVC5_API_TRY_CATCH_END
;
6470 Op
Solver::mkOp(Kind kind
, uint32_t arg
) const
6472 CVC5_API_TRY_CATCH_BEGIN
;
6473 CVC5_API_KIND_CHECK(kind
);
6474 //////// all checks before this line
6481 *mkValHelper
<cvc5::Divisible
>(cvc5::Divisible(arg
)).d_node
);
6483 case BITVECTOR_REPEAT
:
6486 *mkValHelper
<cvc5::BitVectorRepeat
>(cvc5::BitVectorRepeat(arg
))
6489 case BITVECTOR_ZERO_EXTEND
:
6492 *mkValHelper
<cvc5::BitVectorZeroExtend
>(
6493 cvc5::BitVectorZeroExtend(arg
))
6496 case BITVECTOR_SIGN_EXTEND
:
6499 *mkValHelper
<cvc5::BitVectorSignExtend
>(
6500 cvc5::BitVectorSignExtend(arg
))
6503 case BITVECTOR_ROTATE_LEFT
:
6506 *mkValHelper
<cvc5::BitVectorRotateLeft
>(
6507 cvc5::BitVectorRotateLeft(arg
))
6510 case BITVECTOR_ROTATE_RIGHT
:
6513 *mkValHelper
<cvc5::BitVectorRotateRight
>(
6514 cvc5::BitVectorRotateRight(arg
))
6517 case INT_TO_BITVECTOR
:
6521 *mkValHelper
<cvc5::IntToBitVector
>(cvc5::IntToBitVector(arg
)).d_node
);
6525 Op(this, kind
, *mkValHelper
<cvc5::IntAnd
>(cvc5::IntAnd(arg
)).d_node
);
6527 case FLOATINGPOINT_TO_UBV
:
6531 *mkValHelper
<cvc5::FloatingPointToUBV
>(cvc5::FloatingPointToUBV(arg
))
6534 case FLOATINGPOINT_TO_SBV
:
6538 *mkValHelper
<cvc5::FloatingPointToSBV
>(cvc5::FloatingPointToSBV(arg
))
6545 *mkValHelper
<cvc5::RegExpRepeat
>(cvc5::RegExpRepeat(arg
)).d_node
);
6548 CVC5_API_KIND_CHECK_EXPECTED(false, kind
)
6549 << "operator kind with uint32_t argument";
6551 Assert(!res
.isNull());
6554 CVC5_API_TRY_CATCH_END
;
6557 Op
Solver::mkOp(Kind kind
, uint32_t arg1
, uint32_t arg2
) const
6559 CVC5_API_TRY_CATCH_BEGIN
;
6560 CVC5_API_KIND_CHECK(kind
);
6561 //////// all checks before this line
6566 case BITVECTOR_EXTRACT
:
6569 *mkValHelper
<cvc5::BitVectorExtract
>(
6570 cvc5::BitVectorExtract(arg1
, arg2
))
6573 case FLOATINGPOINT_TO_FP_IEEE_BITVECTOR
:
6576 *mkValHelper
<cvc5::FloatingPointToFPIEEEBitVector
>(
6577 cvc5::FloatingPointToFPIEEEBitVector(arg1
, arg2
))
6580 case FLOATINGPOINT_TO_FP_FLOATINGPOINT
:
6583 *mkValHelper
<cvc5::FloatingPointToFPFloatingPoint
>(
6584 cvc5::FloatingPointToFPFloatingPoint(arg1
, arg2
))
6587 case FLOATINGPOINT_TO_FP_REAL
:
6590 *mkValHelper
<cvc5::FloatingPointToFPReal
>(
6591 cvc5::FloatingPointToFPReal(arg1
, arg2
))
6594 case FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR
:
6597 *mkValHelper
<cvc5::FloatingPointToFPSignedBitVector
>(
6598 cvc5::FloatingPointToFPSignedBitVector(arg1
, arg2
))
6601 case FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR
:
6604 *mkValHelper
<cvc5::FloatingPointToFPUnsignedBitVector
>(
6605 cvc5::FloatingPointToFPUnsignedBitVector(arg1
, arg2
))
6608 case FLOATINGPOINT_TO_FP_GENERIC
:
6611 *mkValHelper
<cvc5::FloatingPointToFPGeneric
>(
6612 cvc5::FloatingPointToFPGeneric(arg1
, arg2
))
6619 *mkValHelper
<cvc5::RegExpLoop
>(cvc5::RegExpLoop(arg1
, arg2
)).d_node
);
6622 CVC5_API_KIND_CHECK_EXPECTED(false, kind
)
6623 << "operator kind with two uint32_t arguments";
6625 Assert(!res
.isNull());
6628 CVC5_API_TRY_CATCH_END
;
6631 Op
Solver::mkOp(Kind kind
, const std::vector
<uint32_t>& args
) const
6633 CVC5_API_TRY_CATCH_BEGIN
;
6634 CVC5_API_KIND_CHECK(kind
);
6635 //////// all checks before this line
6644 *mkValHelper
<cvc5::TupleProjectOp
>(cvc5::TupleProjectOp(args
))
6650 std::string message
= "operator kind with " + std::to_string(args
.size())
6651 + " uint32_t arguments";
6652 CVC5_API_KIND_CHECK_EXPECTED(false, kind
) << message
;
6655 Assert(!res
.isNull());
6658 CVC5_API_TRY_CATCH_END
;
6661 /* Non-SMT-LIB commands */
6662 /* -------------------------------------------------------------------------- */
6664 Term
Solver::simplify(const Term
& term
)
6666 CVC5_API_TRY_CATCH_BEGIN
;
6667 CVC5_API_SOLVER_CHECK_TERM(term
);
6668 //////// all checks before this line
6669 return Term(this, d_slv
->simplify(*term
.d_node
));
6671 CVC5_API_TRY_CATCH_END
;
6674 Result
Solver::checkEntailed(const Term
& term
) const
6676 CVC5_API_TRY_CATCH_BEGIN
;
6677 CVC5_API_CHECK(!d_slv
->isQueryMade()
6678 || d_slv
->getOptions().base
.incrementalSolving
)
6679 << "Cannot make multiple queries unless incremental solving is enabled "
6680 "(try --incremental)";
6681 CVC5_API_SOLVER_CHECK_TERM(term
);
6682 ensureWellFormedTerm(term
);
6683 //////// all checks before this line
6684 return d_slv
->checkEntailed(*term
.d_node
);
6686 CVC5_API_TRY_CATCH_END
;
6689 Result
Solver::checkEntailed(const std::vector
<Term
>& terms
) const
6691 CVC5_API_TRY_CATCH_BEGIN
;
6692 CVC5_API_CHECK(!d_slv
->isQueryMade()
6693 || d_slv
->getOptions().base
.incrementalSolving
)
6694 << "Cannot make multiple queries unless incremental solving is enabled "
6695 "(try --incremental)";
6696 CVC5_API_SOLVER_CHECK_TERMS(terms
);
6697 ensureWellFormedTerms(terms
);
6698 //////// all checks before this line
6699 return d_slv
->checkEntailed(Term::termVectorToNodes(terms
));
6701 CVC5_API_TRY_CATCH_END
;
6704 /* SMT-LIB commands */
6705 /* -------------------------------------------------------------------------- */
6707 void Solver::assertFormula(const Term
& term
) const
6709 CVC5_API_TRY_CATCH_BEGIN
;
6710 CVC5_API_SOLVER_CHECK_TERM(term
);
6711 CVC5_API_SOLVER_CHECK_TERM_WITH_SORT(term
, getBooleanSort());
6712 ensureWellFormedTerm(term
);
6713 //////// all checks before this line
6714 d_slv
->assertFormula(*term
.d_node
);
6716 CVC5_API_TRY_CATCH_END
;
6719 Result
Solver::checkSat(void) const
6721 CVC5_API_TRY_CATCH_BEGIN
;
6722 CVC5_API_CHECK(!d_slv
->isQueryMade()
6723 || d_slv
->getOptions().base
.incrementalSolving
)
6724 << "Cannot make multiple queries unless incremental solving is enabled "
6725 "(try --incremental)";
6726 //////// all checks before this line
6727 return d_slv
->checkSat();
6729 CVC5_API_TRY_CATCH_END
;
6732 Result
Solver::checkSatAssuming(const Term
& assumption
) const
6734 CVC5_API_TRY_CATCH_BEGIN
;
6735 CVC5_API_CHECK(!d_slv
->isQueryMade()
6736 || d_slv
->getOptions().base
.incrementalSolving
)
6737 << "Cannot make multiple queries unless incremental solving is enabled "
6738 "(try --incremental)";
6739 CVC5_API_SOLVER_CHECK_TERM_WITH_SORT(assumption
, getBooleanSort());
6740 ensureWellFormedTerm(assumption
);
6741 //////// all checks before this line
6742 return d_slv
->checkSat(*assumption
.d_node
);
6744 CVC5_API_TRY_CATCH_END
;
6747 Result
Solver::checkSatAssuming(const std::vector
<Term
>& assumptions
) const
6749 CVC5_API_TRY_CATCH_BEGIN
;
6750 CVC5_API_CHECK(!d_slv
->isQueryMade() || assumptions
.size() == 0
6751 || d_slv
->getOptions().base
.incrementalSolving
)
6752 << "Cannot make multiple queries unless incremental solving is enabled "
6753 "(try --incremental)";
6754 CVC5_API_SOLVER_CHECK_TERMS_WITH_SORT(assumptions
, getBooleanSort());
6755 ensureWellFormedTerms(assumptions
);
6756 //////// all checks before this line
6757 for (const Term
& term
: assumptions
)
6759 CVC5_API_SOLVER_CHECK_TERM(term
);
6761 std::vector
<Node
> eassumptions
= Term::termVectorToNodes(assumptions
);
6762 return d_slv
->checkSat(eassumptions
);
6764 CVC5_API_TRY_CATCH_END
;
6767 Sort
Solver::declareDatatype(
6768 const std::string
& symbol
,
6769 const std::vector
<DatatypeConstructorDecl
>& ctors
) const
6771 CVC5_API_TRY_CATCH_BEGIN
;
6772 CVC5_API_ARG_CHECK_EXPECTED(ctors
.size() > 0, ctors
)
6773 << "a datatype declaration with at least one constructor";
6774 CVC5_API_SOLVER_CHECK_DTCTORDECLS(ctors
);
6775 for (size_t i
= 0, size
= ctors
.size(); i
< size
; i
++)
6777 CVC5_API_CHECK(!ctors
[i
].isResolved())
6778 << "cannot use a constructor for multiple datatypes";
6780 //////// all checks before this line
6781 DatatypeDecl
dtdecl(this, symbol
);
6782 for (size_t i
= 0, size
= ctors
.size(); i
< size
; i
++)
6784 dtdecl
.addConstructor(ctors
[i
]);
6786 return Sort(this, getNodeManager()->mkDatatypeType(*dtdecl
.d_dtype
));
6788 CVC5_API_TRY_CATCH_END
;
6791 Term
Solver::declareFun(const std::string
& symbol
,
6792 const std::vector
<Sort
>& sorts
,
6793 const Sort
& sort
) const
6795 CVC5_API_TRY_CATCH_BEGIN
;
6796 CVC5_API_SOLVER_CHECK_DOMAIN_SORTS(sorts
);
6797 CVC5_API_SOLVER_CHECK_CODOMAIN_SORT(sort
);
6798 //////// all checks before this line
6800 TypeNode type
= *sort
.d_type
;
6803 std::vector
<TypeNode
> types
= Sort::sortVectorToTypeNodes(sorts
);
6804 type
= getNodeManager()->mkFunctionType(types
, type
);
6806 return Term(this, d_nodeMgr
->mkVar(symbol
, type
));
6808 CVC5_API_TRY_CATCH_END
;
6811 Sort
Solver::declareSort(const std::string
& symbol
, uint32_t arity
) const
6813 CVC5_API_TRY_CATCH_BEGIN
;
6814 //////// all checks before this line
6817 return Sort(this, getNodeManager()->mkSort(symbol
));
6819 return Sort(this, getNodeManager()->mkSortConstructor(symbol
, arity
));
6821 CVC5_API_TRY_CATCH_END
;
6824 Term
Solver::defineFun(const std::string
& symbol
,
6825 const std::vector
<Term
>& bound_vars
,
6830 CVC5_API_TRY_CATCH_BEGIN
;
6831 CVC5_API_SOLVER_CHECK_CODOMAIN_SORT(sort
);
6832 CVC5_API_SOLVER_CHECK_TERM(term
);
6833 CVC5_API_CHECK(term
.getSort().isSubsortOf(sort
))
6834 << "Invalid sort of function body '" << term
<< "', expected '" << sort
6837 std::vector
<Sort
> domain_sorts
;
6838 for (const auto& bv
: bound_vars
)
6840 domain_sorts
.push_back(bv
.getSort());
6843 domain_sorts
.empty()
6846 getNodeManager()->mkFunctionType(
6847 Sort::sortVectorToTypeNodes(domain_sorts
), *sort
.d_type
));
6848 Term fun
= mkConst(fun_sort
, symbol
);
6850 CVC5_API_SOLVER_CHECK_BOUND_VARS_DEF_FUN(fun
, bound_vars
, domain_sorts
);
6851 //////// all checks before this line
6853 d_slv
->defineFunction(
6854 *fun
.d_node
, Term::termVectorToNodes(bound_vars
), *term
.d_node
, global
);
6857 CVC5_API_TRY_CATCH_END
;
6860 Term
Solver::defineFunRec(const std::string
& symbol
,
6861 const std::vector
<Term
>& bound_vars
,
6866 CVC5_API_TRY_CATCH_BEGIN
;
6868 CVC5_API_CHECK(d_slv
->getUserLogicInfo().isQuantified())
6869 << "recursive function definitions require a logic with quantifiers";
6870 CVC5_API_CHECK(d_slv
->getUserLogicInfo().isTheoryEnabled(theory::THEORY_UF
))
6871 << "recursive function definitions require a logic with uninterpreted "
6874 CVC5_API_SOLVER_CHECK_TERM(term
);
6875 CVC5_API_SOLVER_CHECK_CODOMAIN_SORT(sort
);
6876 CVC5_API_CHECK(sort
== term
.getSort())
6877 << "Invalid sort of function body '" << term
<< "', expected '" << sort
6880 std::vector
<Sort
> domain_sorts
;
6881 for (const auto& bv
: bound_vars
)
6883 domain_sorts
.push_back(bv
.getSort());
6886 domain_sorts
.empty()
6889 getNodeManager()->mkFunctionType(
6890 Sort::sortVectorToTypeNodes(domain_sorts
), *sort
.d_type
));
6891 Term fun
= mkConst(fun_sort
, symbol
);
6893 CVC5_API_SOLVER_CHECK_BOUND_VARS_DEF_FUN(fun
, bound_vars
, domain_sorts
);
6894 //////// all checks before this line
6896 d_slv
->defineFunctionRec(
6897 *fun
.d_node
, Term::termVectorToNodes(bound_vars
), *term
.d_node
, global
);
6901 CVC5_API_TRY_CATCH_END
;
6904 Term
Solver::defineFunRec(const Term
& fun
,
6905 const std::vector
<Term
>& bound_vars
,
6909 CVC5_API_TRY_CATCH_BEGIN
;
6911 CVC5_API_CHECK(d_slv
->getUserLogicInfo().isQuantified())
6912 << "recursive function definitions require a logic with quantifiers";
6913 CVC5_API_CHECK(d_slv
->getUserLogicInfo().isTheoryEnabled(theory::THEORY_UF
))
6914 << "recursive function definitions require a logic with uninterpreted "
6917 CVC5_API_SOLVER_CHECK_TERM(fun
);
6918 CVC5_API_SOLVER_CHECK_TERM(term
);
6919 if (fun
.getSort().isFunction())
6921 std::vector
<Sort
> domain_sorts
= fun
.getSort().getFunctionDomainSorts();
6922 CVC5_API_SOLVER_CHECK_BOUND_VARS_DEF_FUN(fun
, bound_vars
, domain_sorts
);
6923 Sort codomain
= fun
.getSort().getFunctionCodomainSort();
6924 CVC5_API_CHECK(codomain
== term
.getSort())
6925 << "Invalid sort of function body '" << term
<< "', expected '"
6930 CVC5_API_SOLVER_CHECK_BOUND_VARS(bound_vars
);
6931 CVC5_API_ARG_CHECK_EXPECTED(bound_vars
.size() == 0, fun
)
6932 << "function or nullary symbol";
6934 //////// all checks before this line
6936 std::vector
<Node
> ebound_vars
= Term::termVectorToNodes(bound_vars
);
6937 d_slv
->defineFunctionRec(*fun
.d_node
, ebound_vars
, *term
.d_node
, global
);
6940 CVC5_API_TRY_CATCH_END
;
6943 void Solver::defineFunsRec(const std::vector
<Term
>& funs
,
6944 const std::vector
<std::vector
<Term
>>& bound_vars
,
6945 const std::vector
<Term
>& terms
,
6948 CVC5_API_TRY_CATCH_BEGIN
;
6950 CVC5_API_CHECK(d_slv
->getUserLogicInfo().isQuantified())
6951 << "recursive function definitions require a logic with quantifiers";
6952 CVC5_API_CHECK(d_slv
->getUserLogicInfo().isTheoryEnabled(theory::THEORY_UF
))
6953 << "recursive function definitions require a logic with uninterpreted "
6955 CVC5_API_SOLVER_CHECK_TERMS(funs
);
6956 CVC5_API_SOLVER_CHECK_TERMS(terms
);
6958 size_t funs_size
= funs
.size();
6959 CVC5_API_ARG_SIZE_CHECK_EXPECTED(funs_size
== bound_vars
.size(), bound_vars
)
6960 << "'" << funs_size
<< "'";
6961 CVC5_API_ARG_SIZE_CHECK_EXPECTED(funs_size
== terms
.size(), terms
)
6962 << "'" << funs_size
<< "'";
6964 for (size_t j
= 0; j
< funs_size
; ++j
)
6966 const Term
& fun
= funs
[j
];
6967 const std::vector
<Term
>& bvars
= bound_vars
[j
];
6968 const Term
& term
= terms
[j
];
6970 CVC5_API_ARG_AT_INDEX_CHECK_EXPECTED(
6971 this == fun
.d_solver
, "function", funs
, j
)
6972 << "function associated with this solver object";
6973 CVC5_API_ARG_AT_INDEX_CHECK_EXPECTED(
6974 this == term
.d_solver
, "term", terms
, j
)
6975 << "term associated with this solver object";
6977 if (fun
.getSort().isFunction())
6979 std::vector
<Sort
> domain_sorts
= fun
.getSort().getFunctionDomainSorts();
6980 CVC5_API_SOLVER_CHECK_BOUND_VARS_DEF_FUN(fun
, bvars
, domain_sorts
);
6981 Sort codomain
= fun
.getSort().getFunctionCodomainSort();
6982 CVC5_API_ARG_AT_INDEX_CHECK_EXPECTED(
6983 codomain
== term
.getSort(), "sort of function body", terms
, j
)
6984 << "'" << codomain
<< "'";
6988 CVC5_API_SOLVER_CHECK_BOUND_VARS(bvars
);
6989 CVC5_API_ARG_CHECK_EXPECTED(bvars
.size() == 0, fun
)
6990 << "function or nullary symbol";
6993 //////// all checks before this line
6994 std::vector
<Node
> efuns
= Term::termVectorToNodes(funs
);
6995 std::vector
<std::vector
<Node
>> ebound_vars
;
6996 for (const auto& v
: bound_vars
)
6998 ebound_vars
.push_back(Term::termVectorToNodes(v
));
7000 std::vector
<Node
> nodes
= Term::termVectorToNodes(terms
);
7001 d_slv
->defineFunctionsRec(efuns
, ebound_vars
, nodes
, global
);
7003 CVC5_API_TRY_CATCH_END
;
7006 void Solver::echo(std::ostream
& out
, const std::string
& str
) const
7011 std::vector
<Term
> Solver::getAssertions(void) const
7013 CVC5_API_TRY_CATCH_BEGIN
;
7014 //////// all checks before this line
7015 std::vector
<Node
> assertions
= d_slv
->getAssertions();
7017 * return std::vector<Term>(assertions.begin(), assertions.end());
7018 * here since constructor is private */
7019 return Term::nodeVectorToTerms(this, assertions
);
7021 CVC5_API_TRY_CATCH_END
;
7024 std::string
Solver::getInfo(const std::string
& flag
) const
7026 CVC5_API_TRY_CATCH_BEGIN
;
7027 CVC5_API_UNSUPPORTED_CHECK(d_slv
->isValidGetInfoFlag(flag
))
7028 << "Unrecognized flag: " << flag
<< ".";
7029 //////// all checks before this line
7030 return d_slv
->getInfo(flag
);
7032 CVC5_API_TRY_CATCH_END
;
7035 std::string
Solver::getOption(const std::string
& option
) const
7039 return d_slv
->getOption(option
);
7041 catch (OptionException
& e
)
7043 throw CVC5ApiUnsupportedException(e
.getMessage());
7047 // Supports a visitor from a list of lambdas
7048 // Taken from https://en.cppreference.com/w/cpp/utility/variant/visit
7049 template<class... Ts
> struct overloaded
: Ts
... { using Ts::operator()...; };
7050 template<class... Ts
> overloaded(Ts
...) -> overloaded
<Ts
...>;
7052 bool OptionInfo::boolValue() const
7054 CVC5_API_TRY_CATCH_BEGIN
;
7055 CVC5_API_RECOVERABLE_CHECK(std::holds_alternative
<ValueInfo
<bool>>(valueInfo
))
7056 << name
<< " is not a bool option";
7057 //////// all checks before this line
7058 return std::get
<ValueInfo
<bool>>(valueInfo
).currentValue
;
7060 CVC5_API_TRY_CATCH_END
;
7062 std::string
OptionInfo::stringValue() const
7064 CVC5_API_TRY_CATCH_BEGIN
;
7065 CVC5_API_RECOVERABLE_CHECK(
7066 std::holds_alternative
<ValueInfo
<std::string
>>(valueInfo
))
7067 << name
<< " is not a string option";
7068 //////// all checks before this line
7069 return std::get
<ValueInfo
<std::string
>>(valueInfo
).currentValue
;
7071 CVC5_API_TRY_CATCH_END
;
7073 int64_t OptionInfo::intValue() const
7075 CVC5_API_TRY_CATCH_BEGIN
;
7076 CVC5_API_RECOVERABLE_CHECK(
7077 std::holds_alternative
<NumberInfo
<int64_t>>(valueInfo
))
7078 << name
<< " is not an int option";
7079 //////// all checks before this line
7080 return std::get
<NumberInfo
<int64_t>>(valueInfo
).currentValue
;
7082 CVC5_API_TRY_CATCH_END
;
7084 uint64_t OptionInfo::uintValue() const
7086 CVC5_API_TRY_CATCH_BEGIN
;
7087 CVC5_API_RECOVERABLE_CHECK(
7088 std::holds_alternative
<NumberInfo
<uint64_t>>(valueInfo
))
7089 << name
<< " is not a uint option";
7090 //////// all checks before this line
7091 return std::get
<NumberInfo
<uint64_t>>(valueInfo
).currentValue
;
7093 CVC5_API_TRY_CATCH_END
;
7095 double OptionInfo::doubleValue() const
7097 CVC5_API_TRY_CATCH_BEGIN
;
7098 CVC5_API_RECOVERABLE_CHECK(
7099 std::holds_alternative
<NumberInfo
<double>>(valueInfo
))
7100 << name
<< " is not a double option";
7101 //////// all checks before this line
7102 return std::get
<NumberInfo
<double>>(valueInfo
).currentValue
;
7104 CVC5_API_TRY_CATCH_END
;
7107 std::ostream
& operator<<(std::ostream
& os
, const OptionInfo
& oi
)
7109 os
<< "OptionInfo{ " << oi
.name
;
7112 os
<< " | set by user";
7114 if (!oi
.aliases
.empty())
7116 container_to_stream(os
, oi
.aliases
, ", ", "", ", ");
7118 auto printNum
= [&os
](const std::string
& type
, const auto& vi
) {
7119 os
<< " | " << type
<< " | " << vi
.currentValue
<< " | default "
7121 if (vi
.minimum
|| vi
.maximum
)
7126 os
<< " " << *vi
.minimum
<< " <=";
7131 os
<< " <= " << *vi
.maximum
;
7135 std::visit(overloaded
{
7136 [&os
](const OptionInfo::VoidInfo
& vi
) { os
<< " | void"; },
7137 [&os
](const OptionInfo::ValueInfo
<bool>& vi
) {
7138 os
<< " | bool | " << vi
.currentValue
<< " | default "
7141 [&os
](const OptionInfo::ValueInfo
<std::string
>& vi
) {
7142 os
<< " | string | " << vi
.currentValue
<< " | default "
7145 [&printNum
](const OptionInfo::NumberInfo
<int64_t>& vi
) {
7146 printNum("int64_t", vi
);
7148 [&printNum
](const OptionInfo::NumberInfo
<uint64_t>& vi
) {
7149 printNum("uint64_t", vi
);
7151 [&printNum
](const OptionInfo::NumberInfo
<double>& vi
) {
7152 printNum("double", vi
);
7154 [&os
](const OptionInfo::ModeInfo
& vi
) {
7155 os
<< " | mode | " << vi
.currentValue
<< " | default "
7156 << vi
.defaultValue
<< " | modes: ";
7157 container_to_stream(os
, vi
.modes
, "", "", ", ");
7165 std::vector
<std::string
> Solver::getOptionNames() const
7167 CVC5_API_TRY_CATCH_BEGIN
;
7168 //////// all checks before this line
7169 return options::getNames();
7171 CVC5_API_TRY_CATCH_END
;
7174 OptionInfo
Solver::getOptionInfo(const std::string
& option
) const
7176 CVC5_API_TRY_CATCH_BEGIN
;
7177 //////// all checks before this line
7178 auto info
= options::getInfo(d_slv
->getOptions(), option
);
7179 CVC5_API_CHECK(info
.name
!= "")
7180 << "Querying invalid or unknown option " << option
;
7183 [&info
](const options::OptionInfo::VoidInfo
& vi
) {
7184 return OptionInfo
{info
.name
,
7187 OptionInfo::VoidInfo
{}};
7189 [&info
](const options::OptionInfo::ValueInfo
<bool>& vi
) {
7194 OptionInfo::ValueInfo
<bool>{vi
.defaultValue
, vi
.currentValue
}};
7196 [&info
](const options::OptionInfo::ValueInfo
<std::string
>& vi
) {
7197 return OptionInfo
{info
.name
,
7200 OptionInfo::ValueInfo
<std::string
>{
7201 vi
.defaultValue
, vi
.currentValue
}};
7203 [&info
](const options::OptionInfo::NumberInfo
<int64_t>& vi
) {
7208 OptionInfo::NumberInfo
<int64_t>{
7209 vi
.defaultValue
, vi
.currentValue
, vi
.minimum
, vi
.maximum
}};
7211 [&info
](const options::OptionInfo::NumberInfo
<uint64_t>& vi
) {
7216 OptionInfo::NumberInfo
<uint64_t>{
7217 vi
.defaultValue
, vi
.currentValue
, vi
.minimum
, vi
.maximum
}};
7219 [&info
](const options::OptionInfo::NumberInfo
<double>& vi
) {
7224 OptionInfo::NumberInfo
<double>{
7225 vi
.defaultValue
, vi
.currentValue
, vi
.minimum
, vi
.maximum
}};
7227 [&info
](const options::OptionInfo::ModeInfo
& vi
) {
7228 return OptionInfo
{info
.name
,
7231 OptionInfo::ModeInfo
{
7232 vi
.defaultValue
, vi
.currentValue
, vi
.modes
}};
7237 CVC5_API_TRY_CATCH_END
;
7240 DriverOptions
Solver::getDriverOptions() const { return DriverOptions(*this); }
7242 std::vector
<Term
> Solver::getUnsatAssumptions(void) const
7244 CVC5_API_TRY_CATCH_BEGIN
;
7245 CVC5_API_CHECK(d_slv
->getOptions().base
.incrementalSolving
)
7246 << "Cannot get unsat assumptions unless incremental solving is enabled "
7247 "(try --incremental)";
7248 CVC5_API_CHECK(d_slv
->getOptions().smt
.unsatAssumptions
)
7249 << "Cannot get unsat assumptions unless explicitly enabled "
7250 "(try --produce-unsat-assumptions)";
7251 CVC5_API_CHECK(d_slv
->getSmtMode() == SmtMode::UNSAT
)
7252 << "Cannot get unsat assumptions unless in unsat mode.";
7253 //////// all checks before this line
7255 std::vector
<Node
> uassumptions
= d_slv
->getUnsatAssumptions();
7257 * return std::vector<Term>(uassumptions.begin(), uassumptions.end());
7258 * here since constructor is private */
7259 std::vector
<Term
> res
;
7260 for (const Node
& n
: uassumptions
)
7262 res
.push_back(Term(this, n
));
7266 CVC5_API_TRY_CATCH_END
;
7269 std::vector
<Term
> Solver::getUnsatCore(void) const
7271 CVC5_API_TRY_CATCH_BEGIN
;
7272 CVC5_API_CHECK(d_slv
->getOptions().smt
.unsatCores
)
7273 << "Cannot get unsat core unless explicitly enabled "
7274 "(try --produce-unsat-cores)";
7275 CVC5_API_RECOVERABLE_CHECK(d_slv
->getSmtMode() == SmtMode::UNSAT
)
7276 << "Cannot get unsat core unless in unsat mode.";
7277 //////// all checks before this line
7278 UnsatCore core
= d_slv
->getUnsatCore();
7280 * return std::vector<Term>(core.begin(), core.end());
7281 * here since constructor is private */
7282 std::vector
<Term
> res
;
7283 for (const Node
& e
: core
)
7285 res
.push_back(Term(this, e
));
7289 CVC5_API_TRY_CATCH_END
;
7292 std::map
<Term
, Term
> Solver::getDifficulty() const
7294 CVC5_API_TRY_CATCH_BEGIN
;
7295 CVC5_API_RECOVERABLE_CHECK(d_slv
->getSmtMode() == SmtMode::UNSAT
7296 || d_slv
->getSmtMode() == SmtMode::SAT
7297 || d_slv
->getSmtMode() == SmtMode::SAT_UNKNOWN
)
7298 << "Cannot get difficulty unless after a UNSAT, SAT or UNKNOWN response.";
7299 //////// all checks before this line
7300 std::map
<Term
, Term
> res
;
7301 std::map
<Node
, Node
> dmap
;
7302 d_slv
->getDifficultyMap(dmap
);
7303 for (const std::pair
<const Node
, Node
>& d
: dmap
)
7305 res
[Term(this, d
.first
)] = Term(this, d
.second
);
7309 CVC5_API_TRY_CATCH_END
;
7312 std::string
Solver::getProof(void) const
7314 CVC5_API_TRY_CATCH_BEGIN
;
7315 CVC5_API_CHECK(d_slv
->getOptions().smt
.produceProofs
)
7316 << "Cannot get proof unless proofs are enabled (try --produce-proofs)";
7317 CVC5_API_RECOVERABLE_CHECK(d_slv
->getSmtMode() == SmtMode::UNSAT
)
7318 << "Cannot get proof unless in unsat mode.";
7319 return d_slv
->getProof();
7320 CVC5_API_TRY_CATCH_END
;
7323 std::vector
<Term
> Solver::getLearnedLiterals(void) const
7325 CVC5_API_TRY_CATCH_BEGIN
;
7326 CVC5_API_CHECK(d_slv
->getOptions().smt
.produceLearnedLiterals
)
7327 << "Cannot get learned literals unless enabled (try "
7328 "--produce-learned-literals)";
7329 CVC5_API_RECOVERABLE_CHECK(d_slv
->getSmtMode() == SmtMode::UNSAT
7330 || d_slv
->getSmtMode() == SmtMode::SAT
7331 || d_slv
->getSmtMode() == SmtMode::SAT_UNKNOWN
)
7332 << "Cannot get learned literals unless after a UNSAT, SAT or UNKNOWN "
7334 //////// all checks before this line
7335 std::vector
<Node
> lits
= d_slv
->getLearnedLiterals();
7336 return Term::nodeVectorToTerms(this, lits
);
7338 CVC5_API_TRY_CATCH_END
;
7341 Term
Solver::getValue(const Term
& term
) const
7343 CVC5_API_TRY_CATCH_BEGIN
;
7344 CVC5_API_RECOVERABLE_CHECK(d_slv
->getOptions().smt
.produceModels
)
7345 << "Cannot get value unless model generation is enabled "
7346 "(try --produce-models)";
7347 CVC5_API_RECOVERABLE_CHECK(d_slv
->isSmtModeSat())
7348 << "Cannot get value unless after a SAT or UNKNOWN response.";
7349 CVC5_API_SOLVER_CHECK_TERM(term
);
7350 CVC5_API_RECOVERABLE_CHECK(term
.getSort().isFirstClass())
7351 << "Cannot get value of a term that is not first class.";
7352 CVC5_API_RECOVERABLE_CHECK(!term
.getSort().isDatatype()
7353 || term
.getSort().getDatatype().isWellFounded())
7354 << "Cannot get value of a term of non-well-founded datatype sort.";
7355 ensureWellFormedTerm(term
);
7356 //////// all checks before this line
7357 return getValueHelper(term
);
7359 CVC5_API_TRY_CATCH_END
;
7362 std::vector
<Term
> Solver::getValue(const std::vector
<Term
>& terms
) const
7364 CVC5_API_TRY_CATCH_BEGIN
;
7365 CVC5_API_RECOVERABLE_CHECK(d_slv
->getOptions().smt
.produceModels
)
7366 << "Cannot get value unless model generation is enabled "
7367 "(try --produce-models)";
7368 CVC5_API_RECOVERABLE_CHECK(d_slv
->isSmtModeSat())
7369 << "Cannot get value unless after a SAT or UNKNOWN response.";
7370 for (const Term
& t
: terms
)
7372 CVC5_API_RECOVERABLE_CHECK(t
.getSort().isFirstClass())
7373 << "Cannot get value of a term that is not first class.";
7374 CVC5_API_RECOVERABLE_CHECK(!t
.getSort().isDatatype()
7375 || t
.getSort().getDatatype().isWellFounded())
7376 << "Cannot get value of a term of non-well-founded datatype sort.";
7378 CVC5_API_SOLVER_CHECK_TERMS(terms
);
7379 ensureWellFormedTerms(terms
);
7380 //////// all checks before this line
7382 std::vector
<Term
> res
;
7383 for (size_t i
= 0, n
= terms
.size(); i
< n
; ++i
)
7385 /* Can not use emplace_back here since constructor is private. */
7386 res
.push_back(getValueHelper(terms
[i
]));
7390 CVC5_API_TRY_CATCH_END
;
7393 std::vector
<Term
> Solver::getModelDomainElements(const Sort
& s
) const
7395 CVC5_API_TRY_CATCH_BEGIN
;
7396 CVC5_API_RECOVERABLE_CHECK(d_slv
->getOptions().smt
.produceModels
)
7397 << "Cannot get domain elements unless model generation is enabled "
7398 "(try --produce-models)";
7399 CVC5_API_RECOVERABLE_CHECK(d_slv
->isSmtModeSat())
7400 << "Cannot get domain elements unless after a SAT or UNKNOWN response.";
7401 CVC5_API_SOLVER_CHECK_SORT(s
);
7402 CVC5_API_RECOVERABLE_CHECK(s
.isUninterpretedSort())
7403 << "Expecting an uninterpreted sort as argument to "
7404 "getModelDomainElements.";
7405 //////// all checks before this line
7406 std::vector
<Term
> res
;
7407 std::vector
<Node
> elements
= d_slv
->getModelDomainElements(s
.getTypeNode());
7408 for (const Node
& n
: elements
)
7410 res
.push_back(Term(this, n
));
7414 CVC5_API_TRY_CATCH_END
;
7417 bool Solver::isModelCoreSymbol(const Term
& v
) const
7419 CVC5_API_TRY_CATCH_BEGIN
;
7420 CVC5_API_RECOVERABLE_CHECK(d_slv
->getOptions().smt
.produceModels
)
7421 << "Cannot check if model core symbol unless model generation is enabled "
7422 "(try --produce-models)";
7423 CVC5_API_RECOVERABLE_CHECK(d_slv
->isSmtModeSat())
7424 << "Cannot check if model core symbol unless after a SAT or UNKNOWN "
7426 CVC5_API_SOLVER_CHECK_TERM(v
);
7427 CVC5_API_RECOVERABLE_CHECK(v
.getKind() == CONSTANT
)
7428 << "Expecting a free constant as argument to isModelCoreSymbol.";
7429 //////// all checks before this line
7430 return d_slv
->isModelCoreSymbol(v
.getNode());
7432 CVC5_API_TRY_CATCH_END
;
7435 std::string
Solver::getModel(const std::vector
<Sort
>& sorts
,
7436 const std::vector
<Term
>& vars
) const
7438 CVC5_API_TRY_CATCH_BEGIN
;
7439 CVC5_API_RECOVERABLE_CHECK(d_slv
->getOptions().smt
.produceModels
)
7440 << "Cannot get model unless model generation is enabled "
7441 "(try --produce-models)";
7442 CVC5_API_RECOVERABLE_CHECK(d_slv
->isSmtModeSat())
7443 << "Cannot get model unless after a SAT or UNKNOWN response.";
7444 CVC5_API_SOLVER_CHECK_SORTS(sorts
);
7445 for (const Sort
& s
: sorts
)
7447 CVC5_API_RECOVERABLE_CHECK(s
.isUninterpretedSort())
7448 << "Expecting an uninterpreted sort as argument to "
7451 CVC5_API_SOLVER_CHECK_TERMS(vars
);
7452 for (const Term
& v
: vars
)
7454 CVC5_API_RECOVERABLE_CHECK(v
.getKind() == CONSTANT
)
7455 << "Expecting a free constant as argument to getModel.";
7457 //////// all checks before this line
7458 return d_slv
->getModel(Sort::sortVectorToTypeNodes(sorts
),
7459 Term::termVectorToNodes(vars
));
7461 CVC5_API_TRY_CATCH_END
;
7464 Term
Solver::getQuantifierElimination(const Term
& q
) const
7466 CVC5_API_TRY_CATCH_BEGIN
;
7467 CVC5_API_SOLVER_CHECK_TERM(q
);
7468 //////// all checks before this line
7469 return Term(this, d_slv
->getQuantifierElimination(q
.getNode(), true));
7471 CVC5_API_TRY_CATCH_END
;
7474 Term
Solver::getQuantifierEliminationDisjunct(const Term
& q
) const
7476 CVC5_API_TRY_CATCH_BEGIN
;
7477 CVC5_API_SOLVER_CHECK_TERM(q
);
7478 //////// all checks before this line
7479 return Term(this, d_slv
->getQuantifierElimination(q
.getNode(), false));
7481 CVC5_API_TRY_CATCH_END
;
7484 void Solver::declareSepHeap(const Sort
& locSort
, const Sort
& dataSort
) const
7486 CVC5_API_TRY_CATCH_BEGIN
;
7487 CVC5_API_SOLVER_CHECK_SORT(locSort
);
7488 CVC5_API_SOLVER_CHECK_SORT(dataSort
);
7489 CVC5_API_CHECK(d_slv
->getLogicInfo().isTheoryEnabled(theory::THEORY_SEP
))
7490 << "Cannot obtain separation logic expressions if not using the "
7491 "separation logic theory.";
7492 //////// all checks before this line
7493 d_slv
->declareSepHeap(locSort
.getTypeNode(), dataSort
.getTypeNode());
7495 CVC5_API_TRY_CATCH_END
;
7498 Term
Solver::getValueSepHeap() const
7500 CVC5_API_TRY_CATCH_BEGIN
;
7501 CVC5_API_CHECK(d_slv
->getLogicInfo().isTheoryEnabled(theory::THEORY_SEP
))
7502 << "Cannot obtain separation logic expressions if not using the "
7503 "separation logic theory.";
7504 CVC5_API_CHECK(d_slv
->getOptions().smt
.produceModels
)
7505 << "Cannot get separation heap term unless model generation is enabled "
7506 "(try --produce-models)";
7507 CVC5_API_RECOVERABLE_CHECK(d_slv
->isSmtModeSat())
7508 << "Can only get separtion heap term after SAT or UNKNOWN response.";
7509 //////// all checks before this line
7510 return Term(this, d_slv
->getSepHeapExpr());
7512 CVC5_API_TRY_CATCH_END
;
7515 Term
Solver::getValueSepNil() const
7517 CVC5_API_TRY_CATCH_BEGIN
;
7518 CVC5_API_CHECK(d_slv
->getLogicInfo().isTheoryEnabled(theory::THEORY_SEP
))
7519 << "Cannot obtain separation logic expressions if not using the "
7520 "separation logic theory.";
7521 CVC5_API_CHECK(d_slv
->getOptions().smt
.produceModels
)
7522 << "Cannot get separation nil term unless model generation is enabled "
7523 "(try --produce-models)";
7524 CVC5_API_RECOVERABLE_CHECK(d_slv
->isSmtModeSat())
7525 << "Can only get separtion nil term after SAT or UNKNOWN response.";
7526 //////// all checks before this line
7527 return Term(this, d_slv
->getSepNilExpr());
7529 CVC5_API_TRY_CATCH_END
;
7532 Term
Solver::declarePool(const std::string
& symbol
,
7534 const std::vector
<Term
>& initValue
) const
7536 CVC5_API_TRY_CATCH_BEGIN
;
7537 CVC5_API_SOLVER_CHECK_SORT(sort
);
7538 CVC5_API_SOLVER_CHECK_TERMS(initValue
);
7539 //////// all checks before this line
7540 TypeNode setType
= getNodeManager()->mkSetType(*sort
.d_type
);
7541 Node pool
= getNodeManager()->mkBoundVar(symbol
, setType
);
7542 std::vector
<Node
> initv
= Term::termVectorToNodes(initValue
);
7543 d_slv
->declarePool(pool
, initv
);
7544 return Term(this, pool
);
7546 CVC5_API_TRY_CATCH_END
;
7549 void Solver::pop(uint32_t nscopes
) const
7551 CVC5_API_TRY_CATCH_BEGIN
;
7552 CVC5_API_CHECK(d_slv
->getOptions().base
.incrementalSolving
)
7553 << "Cannot pop when not solving incrementally (use --incremental)";
7554 CVC5_API_CHECK(nscopes
<= d_slv
->getNumUserLevels())
7555 << "Cannot pop beyond first pushed context";
7556 //////// all checks before this line
7557 for (uint32_t n
= 0; n
< nscopes
; ++n
)
7562 CVC5_API_TRY_CATCH_END
;
7565 bool Solver::getInterpolant(const Term
& conj
, Term
& output
) const
7567 CVC5_API_TRY_CATCH_BEGIN
;
7568 CVC5_API_SOLVER_CHECK_TERM(conj
);
7569 CVC5_API_CHECK(d_slv
->getOptions().smt
.produceInterpols
7570 != options::ProduceInterpols::NONE
)
7571 << "Cannot get interpolant unless interpolants are enabled (try "
7572 "--produce-interpols=mode)";
7573 //////// all checks before this line
7576 bool success
= d_slv
->getInterpolant(*conj
.d_node
, nullType
, result
);
7579 output
= Term(this, result
);
7583 CVC5_API_TRY_CATCH_END
;
7586 bool Solver::getInterpolant(const Term
& conj
,
7590 CVC5_API_TRY_CATCH_BEGIN
;
7591 CVC5_API_SOLVER_CHECK_TERM(conj
);
7592 CVC5_API_CHECK(d_slv
->getOptions().smt
.produceInterpols
7593 != options::ProduceInterpols::NONE
)
7594 << "Cannot get interpolant unless interpolants are enabled (try "
7595 "--produce-interpols=mode)";
7596 //////// all checks before this line
7599 d_slv
->getInterpolant(*conj
.d_node
, *grammar
.resolve().d_type
, result
);
7602 output
= Term(this, result
);
7606 CVC5_API_TRY_CATCH_END
;
7609 bool Solver::getInterpolantNext(Term
& output
) const
7611 CVC5_API_TRY_CATCH_BEGIN
;
7612 CVC5_API_CHECK(d_slv
->getOptions().smt
.produceInterpols
7613 != options::ProduceInterpols::NONE
)
7614 << "Cannot get interpolant unless interpolants are enabled (try "
7615 "--produce-interpols=mode)";
7616 CVC5_API_CHECK(d_slv
->getOptions().base
.incrementalSolving
)
7617 << "Cannot get next interpolant when not solving incrementally (try "
7619 //////// all checks before this line
7621 bool success
= d_slv
->getInterpolantNext(result
);
7624 output
= Term(this, result
);
7628 CVC5_API_TRY_CATCH_END
;
7631 bool Solver::getAbduct(const Term
& conj
, Term
& output
) const
7633 CVC5_API_TRY_CATCH_BEGIN
;
7634 CVC5_API_SOLVER_CHECK_TERM(conj
);
7635 CVC5_API_CHECK(d_slv
->getOptions().smt
.produceAbducts
)
7636 << "Cannot get abduct unless abducts are enabled (try --produce-abducts)";
7637 //////// all checks before this line
7640 bool success
= d_slv
->getAbduct(*conj
.d_node
, nullType
, result
);
7643 output
= Term(this, result
);
7647 CVC5_API_TRY_CATCH_END
;
7650 bool Solver::getAbduct(const Term
& conj
, Grammar
& grammar
, Term
& output
) const
7652 CVC5_API_TRY_CATCH_BEGIN
;
7653 CVC5_API_SOLVER_CHECK_TERM(conj
);
7654 CVC5_API_CHECK(d_slv
->getOptions().smt
.produceAbducts
)
7655 << "Cannot get abduct unless abducts are enabled (try --produce-abducts)";
7656 //////// all checks before this line
7659 d_slv
->getAbduct(*conj
.d_node
, *grammar
.resolve().d_type
, result
);
7662 output
= Term(this, result
);
7666 CVC5_API_TRY_CATCH_END
;
7669 bool Solver::getAbductNext(Term
& output
) const
7671 CVC5_API_TRY_CATCH_BEGIN
;
7672 CVC5_API_CHECK(d_slv
->getOptions().smt
.produceAbducts
)
7673 << "Cannot get next abduct unless abducts are enabled (try "
7674 "--produce-abducts)";
7675 CVC5_API_CHECK(d_slv
->getOptions().base
.incrementalSolving
)
7676 << "Cannot get next abduct when not solving incrementally (try "
7678 //////// all checks before this line
7680 bool success
= d_slv
->getAbductNext(result
);
7683 output
= Term(this, result
);
7687 CVC5_API_TRY_CATCH_END
;
7690 void Solver::blockModel() const
7692 CVC5_API_TRY_CATCH_BEGIN
;
7693 CVC5_API_CHECK(d_slv
->getOptions().smt
.produceModels
)
7694 << "Cannot get value unless model generation is enabled "
7695 "(try --produce-models)";
7696 CVC5_API_RECOVERABLE_CHECK(d_slv
->isSmtModeSat())
7697 << "Can only block model after SAT or UNKNOWN response.";
7698 //////// all checks before this line
7699 d_slv
->blockModel();
7701 CVC5_API_TRY_CATCH_END
;
7704 void Solver::blockModelValues(const std::vector
<Term
>& terms
) const
7706 CVC5_API_TRY_CATCH_BEGIN
;
7707 CVC5_API_CHECK(d_slv
->getOptions().smt
.produceModels
)
7708 << "Cannot get value unless model generation is enabled "
7709 "(try --produce-models)";
7710 CVC5_API_RECOVERABLE_CHECK(d_slv
->isSmtModeSat())
7711 << "Can only block model values after SAT or UNKNOWN response.";
7712 CVC5_API_ARG_SIZE_CHECK_EXPECTED(!terms
.empty(), terms
)
7713 << "a non-empty set of terms";
7714 CVC5_API_SOLVER_CHECK_TERMS(terms
);
7715 ensureWellFormedTerms(terms
);
7716 //////// all checks before this line
7717 d_slv
->blockModelValues(Term::termVectorToNodes(terms
));
7719 CVC5_API_TRY_CATCH_END
;
7722 void Solver::printInstantiations(std::ostream
& out
) const
7724 CVC5_API_TRY_CATCH_BEGIN
;
7725 //////// all checks before this line
7726 d_slv
->printInstantiations(out
);
7728 CVC5_API_TRY_CATCH_END
;
7731 void Solver::push(uint32_t nscopes
) const
7733 CVC5_API_TRY_CATCH_BEGIN
;
7734 CVC5_API_CHECK(d_slv
->getOptions().base
.incrementalSolving
)
7735 << "Cannot push when not solving incrementally (use --incremental)";
7736 //////// all checks before this line
7737 for (uint32_t n
= 0; n
< nscopes
; ++n
)
7742 CVC5_API_TRY_CATCH_END
;
7745 void Solver::resetAssertions(void) const
7747 CVC5_API_TRY_CATCH_BEGIN
;
7748 //////// all checks before this line
7749 d_slv
->resetAssertions();
7751 CVC5_API_TRY_CATCH_END
;
7754 void Solver::setInfo(const std::string
& keyword
, const std::string
& value
) const
7756 CVC5_API_TRY_CATCH_BEGIN
;
7757 CVC5_API_UNSUPPORTED_CHECK(
7758 keyword
== "source" || keyword
== "category" || keyword
== "difficulty"
7759 || keyword
== "filename" || keyword
== "license" || keyword
== "name"
7760 || keyword
== "notes" || keyword
== "smt-lib-version"
7761 || keyword
== "status")
7762 << "Unrecognized keyword: " << keyword
7763 << ", expected 'source', 'category', 'difficulty', "
7764 "'filename', 'license', 'name', "
7765 "'notes', 'smt-lib-version' or 'status'";
7766 CVC5_API_RECOVERABLE_ARG_CHECK_EXPECTED(
7767 keyword
!= "smt-lib-version" || value
== "2" || value
== "2.0"
7768 || value
== "2.5" || value
== "2.6",
7770 << "'2.0', '2.5', '2.6'";
7771 CVC5_API_ARG_CHECK_EXPECTED(keyword
!= "status" || value
== "sat"
7772 || value
== "unsat" || value
== "unknown",
7774 << "'sat', 'unsat' or 'unknown'";
7775 //////// all checks before this line
7776 d_slv
->setInfo(keyword
, value
);
7778 CVC5_API_TRY_CATCH_END
;
7781 void Solver::setLogic(const std::string
& logic
) const
7783 CVC5_API_TRY_CATCH_BEGIN
;
7784 CVC5_API_CHECK(!d_slv
->isFullyInited())
7785 << "Invalid call to 'setLogic', solver is already fully initialized";
7786 cvc5::LogicInfo
logic_info(logic
);
7787 //////// all checks before this line
7788 d_slv
->setLogic(logic_info
);
7790 CVC5_API_TRY_CATCH_END
;
7793 void Solver::setOption(const std::string
& option
,
7794 const std::string
& value
) const
7796 CVC5_API_TRY_CATCH_BEGIN
;
7797 std::vector
<std::string
> options
= options::getNames();
7798 CVC5_API_UNSUPPORTED_CHECK(
7799 option
.find("command-verbosity") != std::string::npos
7800 || std::find(options
.cbegin(), options
.cend(), option
) != options
.cend())
7801 << "Unrecognized option: " << option
<< '.';
7802 static constexpr auto mutableOpts
= {"diagnostic-output-channel",
7804 "regular-output-channel",
7805 "reproducible-resource-limit",
7807 if (std::find(mutableOpts
.begin(), mutableOpts
.end(), option
)
7808 == mutableOpts
.end())
7810 CVC5_API_CHECK(!d_slv
->isFullyInited())
7811 << "Invalid call to 'setOption' for option '" << option
7812 << "', solver is already fully initialized";
7814 //////// all checks before this line
7815 d_slv
->setOption(option
, value
);
7817 CVC5_API_TRY_CATCH_END
;
7820 Term
Solver::mkSygusVar(const Sort
& sort
, const std::string
& symbol
) const
7822 CVC5_API_TRY_CATCH_BEGIN
;
7823 CVC5_API_SOLVER_CHECK_SORT(sort
);
7824 //////// all checks before this line
7825 Node res
= getNodeManager()->mkBoundVar(symbol
, *sort
.d_type
);
7826 (void)res
.getType(true); /* kick off type checking */
7828 d_slv
->declareSygusVar(res
);
7830 return Term(this, res
);
7832 CVC5_API_TRY_CATCH_END
;
7835 Grammar
Solver::mkSygusGrammar(const std::vector
<Term
>& boundVars
,
7836 const std::vector
<Term
>& ntSymbols
) const
7838 CVC5_API_TRY_CATCH_BEGIN
;
7839 CVC5_API_ARG_SIZE_CHECK_EXPECTED(!ntSymbols
.empty(), ntSymbols
)
7840 << "a non-empty vector";
7841 CVC5_API_SOLVER_CHECK_BOUND_VARS(boundVars
);
7842 CVC5_API_SOLVER_CHECK_BOUND_VARS(ntSymbols
);
7843 //////// all checks before this line
7844 return Grammar(this, boundVars
, ntSymbols
);
7846 CVC5_API_TRY_CATCH_END
;
7849 Term
Solver::synthFun(const std::string
& symbol
,
7850 const std::vector
<Term
>& boundVars
,
7851 const Sort
& sort
) const
7853 CVC5_API_TRY_CATCH_BEGIN
;
7854 CVC5_API_SOLVER_CHECK_BOUND_VARS(boundVars
);
7855 CVC5_API_SOLVER_CHECK_SORT(sort
);
7856 //////// all checks before this line
7857 return synthFunHelper(symbol
, boundVars
, sort
);
7859 CVC5_API_TRY_CATCH_END
;
7862 Term
Solver::synthFun(const std::string
& symbol
,
7863 const std::vector
<Term
>& boundVars
,
7865 Grammar
& grammar
) const
7867 CVC5_API_TRY_CATCH_BEGIN
;
7868 CVC5_API_SOLVER_CHECK_BOUND_VARS(boundVars
);
7869 CVC5_API_SOLVER_CHECK_SORT(sort
);
7870 //////// all checks before this line
7871 return synthFunHelper(symbol
, boundVars
, sort
, false, &grammar
);
7873 CVC5_API_TRY_CATCH_END
;
7876 Term
Solver::synthInv(const std::string
& symbol
,
7877 const std::vector
<Term
>& boundVars
) const
7879 CVC5_API_TRY_CATCH_BEGIN
;
7880 CVC5_API_SOLVER_CHECK_BOUND_VARS(boundVars
);
7881 //////// all checks before this line
7882 return synthFunHelper(
7883 symbol
, boundVars
, Sort(this, getNodeManager()->booleanType()), true);
7885 CVC5_API_TRY_CATCH_END
;
7888 Term
Solver::synthInv(const std::string
& symbol
,
7889 const std::vector
<Term
>& boundVars
,
7890 Grammar
& grammar
) const
7892 CVC5_API_TRY_CATCH_BEGIN
;
7893 CVC5_API_SOLVER_CHECK_BOUND_VARS(boundVars
);
7894 //////// all checks before this line
7895 return synthFunHelper(symbol
,
7897 Sort(this, getNodeManager()->booleanType()),
7901 CVC5_API_TRY_CATCH_END
;
7904 void Solver::addSygusConstraint(const Term
& term
) const
7906 CVC5_API_TRY_CATCH_BEGIN
;
7907 CVC5_API_SOLVER_CHECK_TERM(term
);
7908 CVC5_API_ARG_CHECK_EXPECTED(
7909 term
.d_node
->getType() == getNodeManager()->booleanType(), term
)
7911 //////// all checks before this line
7912 d_slv
->assertSygusConstraint(*term
.d_node
, false);
7914 CVC5_API_TRY_CATCH_END
;
7917 void Solver::addSygusAssume(const Term
& term
) const
7919 CVC5_API_TRY_CATCH_BEGIN
;
7920 CVC5_API_SOLVER_CHECK_TERM(term
);
7921 CVC5_API_ARG_CHECK_EXPECTED(
7922 term
.d_node
->getType() == getNodeManager()->booleanType(), term
)
7924 //////// all checks before this line
7925 d_slv
->assertSygusConstraint(*term
.d_node
, true);
7927 CVC5_API_TRY_CATCH_END
;
7930 void Solver::addSygusInvConstraint(Term inv
,
7935 CVC5_API_TRY_CATCH_BEGIN
;
7936 CVC5_API_SOLVER_CHECK_TERM(inv
);
7937 CVC5_API_SOLVER_CHECK_TERM(pre
);
7938 CVC5_API_SOLVER_CHECK_TERM(trans
);
7939 CVC5_API_SOLVER_CHECK_TERM(post
);
7941 CVC5_API_ARG_CHECK_EXPECTED(inv
.d_node
->getType().isFunction(), inv
)
7944 TypeNode invType
= inv
.d_node
->getType();
7946 CVC5_API_ARG_CHECK_EXPECTED(invType
.getRangeType().isBoolean(), inv
)
7949 CVC5_API_CHECK(pre
.d_node
->getType() == invType
)
7950 << "Expected inv and pre to have the same sort";
7952 CVC5_API_CHECK(post
.d_node
->getType() == invType
)
7953 << "Expected inv and post to have the same sort";
7954 //////// all checks before this line
7956 const std::vector
<TypeNode
>& invArgTypes
= invType
.getArgTypes();
7958 std::vector
<TypeNode
> expectedTypes
;
7959 expectedTypes
.reserve(2 * invArgTypes
.size() + 1);
7961 for (size_t i
= 0, n
= invArgTypes
.size(); i
< 2 * n
; i
+= 2)
7963 expectedTypes
.push_back(invArgTypes
[i
% n
]);
7964 expectedTypes
.push_back(invArgTypes
[(i
+ 1) % n
]);
7967 expectedTypes
.push_back(invType
.getRangeType());
7968 TypeNode expectedTransType
= getNodeManager()->mkFunctionType(expectedTypes
);
7970 CVC5_API_CHECK(trans
.d_node
->getType() == expectedTransType
)
7971 << "Expected trans's sort to be " << invType
;
7973 d_slv
->assertSygusInvConstraint(
7974 *inv
.d_node
, *pre
.d_node
, *trans
.d_node
, *post
.d_node
);
7976 CVC5_API_TRY_CATCH_END
;
7979 Result
Solver::checkSynth() const
7981 CVC5_API_TRY_CATCH_BEGIN
;
7982 //////// all checks before this line
7983 return d_slv
->checkSynth();
7985 CVC5_API_TRY_CATCH_END
;
7988 Result
Solver::checkSynthNext() const
7990 CVC5_API_TRY_CATCH_BEGIN
;
7991 CVC5_API_CHECK(d_slv
->getOptions().base
.incrementalSolving
)
7992 << "Cannot checkSynthNext when not solving incrementally (use "
7994 //////// all checks before this line
7995 return d_slv
->checkSynth(true);
7997 CVC5_API_TRY_CATCH_END
;
8000 Term
Solver::getSynthSolution(Term term
) const
8002 CVC5_API_TRY_CATCH_BEGIN
;
8003 CVC5_API_SOLVER_CHECK_TERM(term
);
8005 std::map
<cvc5::Node
, cvc5::Node
> map
;
8006 CVC5_API_CHECK(d_slv
->getSynthSolutions(map
))
8007 << "The solver is not in a state immediately preceded by a "
8008 "successful call to checkSynth";
8010 std::map
<cvc5::Node
, cvc5::Node
>::const_iterator it
= map
.find(*term
.d_node
);
8012 CVC5_API_CHECK(it
!= map
.cend()) << "Synth solution not found for given term";
8013 //////// all checks before this line
8014 return Term(this, it
->second
);
8016 CVC5_API_TRY_CATCH_END
;
8019 std::vector
<Term
> Solver::getSynthSolutions(
8020 const std::vector
<Term
>& terms
) const
8022 CVC5_API_TRY_CATCH_BEGIN
;
8023 CVC5_API_ARG_SIZE_CHECK_EXPECTED(!terms
.empty(), terms
) << "non-empty vector";
8024 CVC5_API_SOLVER_CHECK_TERMS(terms
);
8026 std::map
<cvc5::Node
, cvc5::Node
> map
;
8027 CVC5_API_CHECK(d_slv
->getSynthSolutions(map
))
8028 << "The solver is not in a state immediately preceded by a "
8029 "successful call to checkSynth";
8030 //////// all checks before this line
8032 std::vector
<Term
> synthSolution
;
8033 synthSolution
.reserve(terms
.size());
8035 for (size_t i
= 0, n
= terms
.size(); i
< n
; ++i
)
8037 std::map
<cvc5::Node
, cvc5::Node
>::const_iterator it
=
8038 map
.find(*terms
[i
].d_node
);
8040 CVC5_API_CHECK(it
!= map
.cend())
8041 << "Synth solution not found for term at index " << i
;
8043 synthSolution
.push_back(Term(this, it
->second
));
8046 return synthSolution
;
8048 CVC5_API_TRY_CATCH_END
;
8051 Statistics
Solver::getStatistics() const
8053 return Statistics(d_slv
->getStatisticsRegistry());
8056 bool Solver::isOutputOn(const std::string
& tag
) const
8058 // `isOutputOn(tag)` may raise an `OptionException`, which we do not want to
8059 // forward as such. We thus do not use the standard exception handling macros
8060 // here but roll our own.
8063 return d_slv
->getEnv().isOutputOn(tag
);
8065 catch (const cvc5::Exception
& e
)
8067 throw CVC5ApiException("Invalid output tag " + tag
);
8071 std::ostream
& Solver::getOutput(const std::string
& tag
) const
8073 // `output(tag)` may raise an `OptionException`, which we do not want to
8074 // forward as such. We thus do not use the standard exception handling macros
8075 // here but roll our own.
8078 return d_slv
->getEnv().output(tag
);
8080 catch (const cvc5::Exception
& e
)
8082 throw CVC5ApiException("Invalid output tag " + tag
);
8092 size_t hash
<cvc5::api::Kind
>::operator()(cvc5::api::Kind k
) const
8094 return static_cast<size_t>(k
);
8097 size_t hash
<cvc5::api::Op
>::operator()(const cvc5::api::Op
& t
) const
8099 if (t
.isIndexedHelper())
8101 return std::hash
<cvc5::Node
>()(*t
.d_node
);
8105 return std::hash
<cvc5::api::Kind
>()(t
.d_kind
);
8109 size_t std::hash
<cvc5::api::RoundingMode
>::operator()(
8110 cvc5::api::RoundingMode rm
) const
8112 return static_cast<size_t>(rm
);
8115 size_t std::hash
<cvc5::api::Sort
>::operator()(const cvc5::api::Sort
& s
) const
8117 return std::hash
<cvc5::TypeNode
>()(*s
.d_type
);
8120 size_t std::hash
<cvc5::api::Term
>::operator()(const cvc5::api::Term
& t
) const
8122 return std::hash
<cvc5::Node
>()(*t
.d_node
);