projects / cvc5.git / blob
? search:
summary | shortlog | log | commit | commitdiff | tree
history | raw | HEAD
BV: Rename BITVECTOR_PLUS to BITVECTOR_ADD. (#6589)
[cvc5.git] / src / api / cpp / cvc5_kind.h
1 /******************************************************************************
2 * Top contributors (to current version):
3 * Aina Niemetz, Andrew Reynolds, Makai Mann
4 *
5 * This file is part of the cvc5 project.
6 *
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 * ****************************************************************************
12 *
13 * The term kinds of the cvc5 C++ API.
14 */
15
16 #include "cvc5_export.h"
17
18 #ifndef CVC5__API__CVC5_KIND_H
19 #define CVC5__API__CVC5_KIND_H
20
21 #include <ostream>
22
23 namespace cvc5 {
24 namespace api {
25
26 /* -------------------------------------------------------------------------- */
27 /* Kind */
28 /* -------------------------------------------------------------------------- */
29
30 // TODO(Gereon): Fix links that involve std::vector. See
31 // https://github.com/doxygen/doxygen/issues/8503
32 // clang-format off
33 /**
34 * The kind of a cvc5 term.
35 *
36 * Note that the underlying type of Kind must be signed (to enable range
37 * checks for validity). The size of this type depends on the size of
38 * cvc5::Kind (NodeValue::NBITS_KIND, currently 10 bits, see expr/node_value.h).
39 */
40 enum CVC5_EXPORT Kind : int32_t
41 {
42 /**
43 * Internal kind.
44 * Should never be exposed or created via the API.
45 */
46 INTERNAL_KIND = -2,
47 /**
48 * Undefined kind.
49 * Should never be exposed or created via the API.
50 */
51 UNDEFINED_KIND = -1,
52 /**
53 * Null kind (kind of null term `Term::Term()`).
54 * Do not explicitly create via API functions other than `Term::Term()`.
55 */
56 NULL_EXPR,
57
58 /* Builtin --------------------------------------------------------------- */
59
60 /**
61 * Uninterpreted constant.
62 *
63 * Parameters:
64 * - 1: Sort of the constant
65 * - 2: Index of the constant
66 *
67 * Create with:
68 * - `Solver::mkUninterpretedConst(const Sort& sort, int32_t index) const`
69 */
70 UNINTERPRETED_CONSTANT,
71 /**
72 * Abstract value (other than uninterpreted sort constants).
73 *
74 * Parameters:
75 * - 1: Index of the abstract value
76 *
77 * Create with:
78 * - `Solver::mkAbstractValue(const std::string& index) const`
79 * - `Solver::mkAbstractValue(uint64_t index) const`
80 */
81 ABSTRACT_VALUE,
82 #if 0
83 /* Built-in operator */
84 BUILTIN,
85 #endif
86 /**
87 * Equality, chainable.
88 *
89 * Parameters: n > 1
90 * - 1..n: Terms with same sorts
91 *
92 * Create with:
93 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
94 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
95 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
96 */
97 EQUAL,
98 /**
99 * Disequality.
100 *
101 * Parameters: n > 1
102 * - 1..n: Terms with same sorts
103 *
104 * Create with:
105 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
106 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
107 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
108 */
109 DISTINCT,
110 /**
111 * First-order constant.
112 *
113 * Not permitted in bindings (forall, exists, ...).
114 *
115 * Parameters:
116 * - See @ref cvc5::api::Solver::mkConst() "mkConst()".
117 *
118 * Create with:
119 * - `Solver::mkConst(const Sort& sort, const std::string& symbol) const`
120 * - `Solver::mkConst(const Sort& sort) const`
121 */
122 CONSTANT,
123 /**
124 * (Bound) variable.
125 *
126 * Permitted in bindings and in the lambda and quantifier bodies only.
127 *
128 * Parameters:
129 * - See @ref cvc5::api::Solver::mkVar() "mkVar()".
130 *
131 * Create with:
132 * - `Solver::mkVar(const Sort& sort, const std::string& symbol) const`
133 */
134 VARIABLE,
135 #if 0
136 /* Skolem variable (internal only) */
137 SKOLEM,
138 #endif
139 /**
140 * Symbolic expression.
141 *
142 * Parameters: n > 0
143 * - 1..n: terms
144 *
145 * Create with:
146 * - `Solver::mkTerm(Kind kind, const Term& child) const`
147 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
148 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
149 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
150 */
151 SEXPR,
152 /**
153 * Lambda expression.
154 *
155 * Parameters:
156 * - 1: BOUND_VAR_LIST
157 * - 2: Lambda body
158 *
159 * Create with:
160 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
161 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
162 */
163 LAMBDA,
164 /**
165 * The syntax of a witness term is similar to a quantified formula except that
166 * only one bound variable is allowed.
167 * The term `(witness ((x T)) F)` returns an element `x` of type `T`
168 * and asserts `F`.
169 *
170 * The witness operator behaves like the description operator
171 * (see https://planetmath.org/hilbertsvarepsilonoperator) if there is no x
172 * that satisfies F. But if such x exists, the witness operator does not
173 * enforce the axiom that ensures uniqueness up to logical equivalence:
174 *
175 * @f[
176 * \forall x. F \equiv G \Rightarrow witness~x. F = witness~x. G
177 * @f]
178 *
179 * For example if there are 2 elements of type T that satisfy F, then the
180 * following formula is satisfiable:
181 *
182 * (distinct
183 * (witness ((x Int)) F)
184 * (witness ((x Int)) F))
185 *
186 * This kind is primarily used internally, but may be returned in models
187 * (e.g. for arithmetic terms in non-linear queries). However, it is not
188 * supported by the parser. Moreover, the user of the API should be cautious
189 * when using this operator. In general, all witness terms
190 * `(witness ((x Int)) F)` should be such that `(exists ((x Int)) F)` is a
191 * valid formula. If this is not the case, then the semantics in formulas that
192 * use witness terms may be unintuitive. For example, the following formula is
193 * unsatisfiable:
194 * `(or (= (witness ((x Int)) false) 0) (not (= (witness ((x Int)) false) 0))`
195 * whereas notice that `(or (= z 0) (not (= z 0)))` is true for any `z`.
196 *
197 * Parameters:
198 * - 1: BOUND_VAR_LIST
199 * - 2: Witness body
200 *
201 * Create with:
202 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
203 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
204 */
205 WITNESS,
206
207 /* Boolean --------------------------------------------------------------- */
208
209 /**
210 * Boolean constant.
211 *
212 * Parameters:
213 * - 1: Boolean value of the constant
214 *
215 * Create with:
216 * - `Solver::mkTrue() const`
217 * - `Solver::mkFalse() const`
218 * - `Solver::mkBoolean(bool val) const`
219 */
220 CONST_BOOLEAN,
221 /**
222 * Logical negation.
223 *
224 * Parameters:
225 * - 1: Boolean Term to negate
226 *
227 * Create with:
228 * - `Solver::mkTerm(Kind kind, const Term& child) const`
229 */
230 NOT,
231 /**
232 * Logical conjunction.
233 *
234 * Parameters: n > 1
235 * - 1..n: Boolean Term of the conjunction
236 *
237 * Create with:
238 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
239 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
240 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
241 */
242 AND,
243 /**
244 * Logical implication.
245 *
246 * Parameters: n > 1
247 * - 1..n: Boolean Terms, right associative
248 *
249 * Create with:
250 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
251 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
252 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
253 */
254 IMPLIES,
255 /**
256 * Logical disjunction.
257 *
258 * Parameters: n > 1
259 * - 1..n: Boolean Term of the disjunction
260 *
261 * Create with:
262 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
263 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
264 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
265 */
266 OR,
267 /**
268 * Logical exclusive disjunction, left associative.
269 *
270 * Parameters: n > 1
271 * - 1..n: Boolean Terms, `[1] xor ... xor [n]`
272 *
273 * Create with:
274 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
275 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
276 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
277 */
278 XOR,
279 /**
280 * If-then-else.
281 *
282 * Parameters:
283 * - 1: is a Boolean condition Term
284 * - 2: the 'then' Term
285 * - 3: the 'else' Term
286 *
287 * 'then' and 'else' term must have same base sort.
288 *
289 * Create with:
290 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
291 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
292 */
293 ITE,
294
295 /* UF -------------------------------------------------------------------- */
296
297 /**
298 * Application of an uninterpreted function.
299 *
300 * Parameters: n > 1
301 * - 1: Function Term
302 * - 2..n: Function argument instantiation Terms
303 *
304 * Create with:
305 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
306 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
307 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
308 */
309 APPLY_UF,
310 #if 0
311 /* Boolean term variable */
312 BOOLEAN_TERM_VARIABLE,
313 #endif
314 /**
315 * Cardinality constraint on uninterpreted sort S.
316 * Interpreted as a predicate that is true when the cardinality of S
317 * is less than or equal to the value of the second argument.
318 *
319 * Parameters:
320 * - 1: Term of sort S
321 * - 2: Positive integer constant that bounds the cardinality of sort S
322 *
323 * Create with:
324 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
325 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
326 */
327 CARDINALITY_CONSTRAINT,
328 /**
329 * Cardinality value for uninterpreted sort S.
330 * An operator that returns an integer indicating the value of the cardinality
331 * of sort S.
332 *
333 * Parameters:
334 * - 1: Term of sort S
335 *
336 * Create with:
337 * - `Solver::mkTerm(Kind kind, const Term& child1) const`
338 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
339 */
340 CARDINALITY_VALUE,
341 #if 0
342 /* Combined cardinality constraint. */
343 COMBINED_CARDINALITY_CONSTRAINT,
344 /* Partial uninterpreted function application. */
345 PARTIAL_APPLY_UF,
346 #endif
347 /**
348 * Higher-order applicative encoding of function application, left
349 * associative.
350 *
351 * Parameters: n > 1
352 * - 1: Function to apply
353 * - 2..n: Arguments of the function
354 *
355 * Create with:
356 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
357 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
358 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
359 */
360 HO_APPLY,
361
362 /* Arithmetic ------------------------------------------------------------ */
363
364 /**
365 * Arithmetic addition.
366 *
367 * Parameters: n > 1
368 * - 1..n: Terms of sort Integer, Real (sorts must match)
369 *
370 * Create with:
371 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
372 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
373 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
374 */
375 PLUS,
376 /**
377 * Arithmetic multiplication.
378 *
379 * Parameters: n > 1
380 * - 1..n: Terms of sort Integer, Real (sorts must match)
381 *
382 * Create with:
383 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
384 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
385 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
386 */
387 MULT,
388 /**
389 * Operator for Integer AND
390 *
391 * Parameters:
392 * - 1: Size of the bit-vector that determines the semantics of the IAND
393 *
394 * Create with:
395 * - `Solver::mkOp(Kind kind, uint32_t param) const`
396 *
397 * Apply integer conversion to bit-vector.
398
399 * Parameters:
400 * - 1: Op of kind IAND
401 * - 2: Integer term
402 * - 3: Integer term
403 *
404 * Create with:
405 * - `Solver::mkTerm(const Op& op, const Term& child1, const Term& child2) const`
406 * - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const`
407 */
408 IAND,
409 #if 0
410 /* Synonym for MULT. */
411 NONLINEAR_MULT,
412 #endif
413 /**
414 * Arithmetic subtraction, left associative.
415 *
416 * Parameters:
417 * - 1..n: Terms of sort Integer, Real (sorts must match)
418 *
419 * Create with:
420 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
421 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
422 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
423 */
424 MINUS,
425 /**
426 * Arithmetic negation.
427 *
428 * Parameters:
429 * - 1: Term of sort Integer, Real
430 *
431 * Create with:
432 * - `Solver::mkTerm(Kind kind, const Term& child) const`
433 */
434 UMINUS,
435 /**
436 * Real division, division by 0 undefined, left associative.
437 *
438 * Parameters: n > 1
439 * - 1..n: Terms of sort Integer, Real
440 *
441 * Create with:
442 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
443 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
444 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
445 */
446 DIVISION,
447 /**
448 * Integer division, division by 0 undefined, left associative.
449 *
450 * Parameters: n > 1
451 * - 1..n: Terms of sort Integer
452 *
453 * Create with:
454 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
455 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
456 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
457 */
458 INTS_DIVISION,
459 /**
460 * Integer modulus, division by 0 undefined.
461 *
462 * Parameters:
463 * - 1: Term of sort Integer
464 * - 2: Term of sort Integer
465 *
466 * Create with:
467 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
468 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
469 */
470 INTS_MODULUS,
471 /**
472 * Absolute value.
473 *
474 * Parameters:
475 * - 1: Term of sort Integer
476 *
477 * Create with:
478 * - `Solver::mkTerm(Kind kind, const Term& child) const`
479 */
480 ABS,
481 /**
482 * Arithmetic power.
483 *
484 * Parameters:
485 * - 1: Term of sort Integer, Real
486 * - 2: Term of sort Integer, Real
487 *
488 * Create with:
489 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
490 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
491 */
492 POW,
493 /**
494 * Exponential function.
495 *
496 * Parameters:
497 * - 1: Term of sort Integer, Real
498 *
499 * Create with:
500 * - `Solver::mkTerm(Kind kind, const Term& child) const`
501 */
502 EXPONENTIAL,
503 /**
504 * Sine function.
505 *
506 * Parameters:
507 * - 1: Term of sort Integer, Real
508 *
509 * Create with:
510 * - `Solver::mkTerm(Kind kind, const Term& child) const`
511 */
512 SINE,
513 /**
514 * Cosine function.
515 *
516 * Parameters:
517 * - 1: Term of sort Integer, Real
518 *
519 * Create with:
520 * - `Solver::mkTerm(Kind kind, const Term& child) const`
521 */
522 COSINE,
523 /**
524 * Tangent function.
525 *
526 * Parameters:
527 * - 1: Term of sort Integer, Real
528 *
529 * Create with:
530 * - `Solver::mkTerm(Kind kind, const Term& child) const`
531 */
532 TANGENT,
533 /**
534 * Cosecant function.
535 *
536 * Parameters:
537 * - 1: Term of sort Integer, Real
538 *
539 * Create with:
540 * - `Solver::mkTerm(Kind kind, const Term& child) const`
541 */
542 COSECANT,
543 /**
544 * Secant function.
545 *
546 * Parameters:
547 * - 1: Term of sort Integer, Real
548 *
549 * Create with:
550 * - `Solver::mkTerm(Kind kind, const Term& child) const`
551 */
552 SECANT,
553 /**
554 * Cotangent function.
555 *
556 * Parameters:
557 * - 1: Term of sort Integer, Real
558 *
559 * Create with:
560 * - `Solver::mkTerm(Kind kind, const Term& child) const`
561 */
562 COTANGENT,
563 /**
564 * Arc sine function.
565 *
566 * Parameters:
567 * - 1: Term of sort Integer, Real
568 *
569 * Create with:
570 * - `Solver::mkTerm(Kind kind, const Term& child) const`
571 */
572 ARCSINE,
573 /**
574 * Arc cosine function.
575 *
576 * Parameters:
577 * - 1: Term of sort Integer, Real
578 *
579 * Create with:
580 * - `Solver::mkTerm(Kind kind, const Term& child) const`
581 */
582 ARCCOSINE,
583 /**
584 * Arc tangent function.
585 *
586 * Parameters:
587 * - 1: Term of sort Integer, Real
588 *
589 * Create with:
590 * - `Solver::mkTerm(Kind kind, const Term& child) const`
591 */
592 ARCTANGENT,
593 /**
594 * Arc cosecant function.
595 *
596 * Parameters:
597 * - 1: Term of sort Integer, Real
598 *
599 * Create with:
600 * - `Solver::mkTerm(Kind kind, const Term& child) const`
601 */
602 ARCCOSECANT,
603 /**
604 * Arc secant function.
605 *
606 * Parameters:
607 * - 1: Term of sort Integer, Real
608 *
609 * Create with:
610 * - `Solver::mkTerm(Kind kind, const Term& child) const`
611 */
612 ARCSECANT,
613 /**
614 * Arc cotangent function.
615 *
616 * Parameters:
617 * - 1: Term of sort Integer, Real
618 *
619 * Create with:
620 * - `Solver::mkTerm(Kind kind, const Term& child) const`
621 */
622 ARCCOTANGENT,
623 /**
624 * Square root.
625 *
626 * Parameters:
627 * - 1: Term of sort Integer, Real
628 *
629 * Create with:
630 * - `Solver::mkTerm(Kind kind, const Term& child) const`
631 */
632 SQRT,
633 /**
634 * Operator for the divisibility-by-k predicate.
635 *
636 * Parameter:
637 * - 1: The k to divide by (sort Integer)
638 *
639 * Create with:
640 * - `Solver::mkOp(Kind kind, uint32_t param) const`
641 *
642 * Apply divisibility-by-k predicate.
643 *
644 * Parameters:
645 * - 1: Op of kind DIVISIBLE
646 * - 2: Integer Term
647 *
648 * Create with:
649 * - `Solver::mkTerm(const Op& op, const Term& child1, const Term& child2) const`
650 * - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const`
651 */
652 DIVISIBLE,
653 /**
654 * Multiple-precision rational constant.
655 *
656 * Parameters:
657 * See @ref cvc5::api::Solver::mkInteger() "mkInteger()", @ref cvc5::api::Solver::mkReal() "mkReal()".
658 *
659 * Create with:
660 * - `Solver::mkInteger(const std::string& s) const`
661 * - `Solver::mkInteger(int64_t val) const`
662 * - `Solver::mkReal(const std::string& s) const`
663 * - `Solver::mkReal(int64_t val) const`
664 * - `Solver::mkReal(int64_t num, int64_t den) const`
665 */
666 CONST_RATIONAL,
667 /**
668 * Less than, chainable.
669 *
670 * Parameters: n
671 * - 1..n: Terms of sort Integer, Real; [1] < ... < [n]
672 *
673 * Create with:
674 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
675 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
676 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
677 */
678 LT,
679 /**
680 * Less than or equal, chainable.
681 *
682 * Parameters: n > 1
683 * - 1..n: Terms of sort Integer, Real; [1] <= ... <= [n]
684 *
685 * Create with:
686 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
687 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
688 */
689 LEQ,
690 /**
691 * Greater than, chainable.
692 *
693 * Parameters: n > 1
694 * - 1..n: Terms of sort Integer, Real, [1] > ... > [n]
695 *
696 * Create with:
697 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
698 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
699 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
700 */
701 GT,
702 /**
703 * Greater than or equal, chainable.
704 *
705 * Parameters: n > 1
706 * - 1..n: Terms of sort Integer, Real; [1] >= ... >= [n]
707 *
708 * Create with:
709 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
710 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
711 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
712 */
713 GEQ,
714 /**
715 * Is-integer predicate.
716 *
717 * Parameters:
718 * - 1: Term of sort Integer, Real
719 *
720 * Create with:
721 * - `Solver::mkTerm(Kind kind, const Term& child) const`
722 */
723 IS_INTEGER,
724 /**
725 * Convert Term to Integer by the floor function.
726 *
727 * Parameters:
728 * - 1: Term of sort Integer, Real
729 *
730 * Create with:
731 * - `Solver::mkTerm(Kind kind, const Term& child) const`
732 */
733 TO_INTEGER,
734 /**
735 * Convert Term to Real.
736 *
737 * Parameters:
738 *
739 * - 1: Term of sort Integer, Real
740 *
741 * This is a no-op in cvc5, as Integer is a subtype of Real.
742 */
743 TO_REAL,
744 /**
745 * Pi constant.
746 *
747 * Create with:
748 * - `Solver::mkPi() const`
749 * - `Solver::mkTerm(Kind kind) const`
750 */
751 PI,
752
753 /* BV -------------------------------------------------------------------- */
754
755 /**
756 * Fixed-size bit-vector constant.
757 *
758 * Parameters:
759 * See @ref cvc5::api::Solver::mkBitVector() "mkBitVector()".
760 *
761 * Create with:
762 * - `Solver::mkBitVector(uint32_t size, uint64_t val) const`
763 * - `Solver::mkBitVector(const std::string& s, uint32_t base) const`
764 * - `Solver::mkBitVector(uint32_t size, const std::string& s, uint32_t base) const`
765 */
766 CONST_BITVECTOR,
767 /**
768 * Concatenation of two or more bit-vectors.
769 *
770 * Parameters: n > 1
771 * - 1..n: Terms of bit-vector sort
772 *
773 * Create with:
774 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
775 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
776 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
777 */
778 BITVECTOR_CONCAT,
779 /**
780 * Bit-wise and.
781 *
782 * Parameters: n > 1
783 * - 1..n: Terms of bit-vector sort (sorts must match)
784 *
785 * Create with:
786 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
787 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
788 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
789 */
790 BITVECTOR_AND,
791 /**
792 * Bit-wise or.
793 *
794 * Parameters: n > 1
795 * - 1..n: Terms of bit-vector sort (sorts must match)
796 *
797 * Create with:
798 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
799 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
800 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
801 */
802 BITVECTOR_OR,
803 /**
804 * Bit-wise xor.
805 *
806 * Parameters: n > 1
807 * - 1..n: Terms of bit-vector sort (sorts must match)
808 *
809 * Create with:
810 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
811 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
812 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
813 */
814 BITVECTOR_XOR,
815 /**
816 * Bit-wise negation.
817 *
818 * Parameters:
819 * - 1: Term of bit-vector sort
820 *
821 * Create with:
822 * - `Solver::mkTerm(Kind kind, const Term& child) const`
823 */
824 BITVECTOR_NOT,
825 /**
826 * Bit-wise nand.
827 *
828 * Parameters:
829 * - 1..2: Terms of bit-vector sort (sorts must match)
830 *
831 * Create with:
832 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
833 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
834 */
835 BITVECTOR_NAND,
836 /**
837 * Bit-wise nor.
838 *
839 * Parameters:
840 * - 1..2: Terms of bit-vector sort (sorts must match)
841 *
842 * Create with:
843 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
844 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
845 */
846 BITVECTOR_NOR,
847 /**
848 * Bit-wise xnor, left associative.
849 *
850 * Parameters: n > 1
851 * - 1..n: Terms of bit-vector sort (sorts must match)
852 *
853 * Create with:
854 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
855 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
856 */
857 BITVECTOR_XNOR,
858 /**
859 * Equality comparison (returns bit-vector of size 1).
860 *
861 * Parameters:
862 * - 1..2: Terms of bit-vector sort (sorts must match)
863 *
864 * Create with:
865 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
866 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
867 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
868 */
869 BITVECTOR_COMP,
870 /**
871 * Multiplication of two or more bit-vectors.
872 *
873 * Parameters: n > 1
874 * - 1..n: Terms of bit-vector sort (sorts must match)
875 *
876 * Create with:
877 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
878 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
879 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
880 */
881 BITVECTOR_MULT,
882 /**
883 * Addition of two or more bit-vectors.
884 *
885 * Parameters: n > 1
886 * - 1..n: Terms of bit-vector sort (sorts must match)
887 *
888 * Create with:
889 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
890 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
891 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
892 */
893 BITVECTOR_ADD,
894 /**
895 * Subtraction of two bit-vectors.
896 *
897 * Parameters:
898 * - 1..2: Terms of bit-vector sort (sorts must match)
899 *
900 * Create with:
901 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
902 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
903 */
904 BITVECTOR_SUB,
905 /**
906 * Negation of a bit-vector (two's complement).
907 *
908 * Parameters:
909 * - 1: Term of bit-vector sort
910 *
911 * Create with:
912 * - `Solver::mkTerm(Kind kind, const Term& child) const`
913 */
914 BITVECTOR_NEG,
915 /**
916 * Unsigned division of two bit-vectors, truncating towards 0.
917 *
918 * Note: The semantics of this operator depends on `bv-div-zero-const`
919 * (default is true). Depending on the setting, a division by zero is
920 * treated as all ones (default, corresponds to SMT-LIB >=2.6) or an
921 * uninterpreted value (corresponds to SMT-LIB <2.6).
922 *
923 * Parameters:
924 * - 1..2: Terms of bit-vector sort (sorts must match)
925 *
926 * Create with:
927 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
928 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
929 */
930 BITVECTOR_UDIV,
931 /**
932 * Unsigned remainder from truncating division of two bit-vectors.
933 *
934 * Note: The semantics of this operator depends on `bv-div-zero-const`
935 * (default is true). Depending on the setting, if the modulus is zero, the
936 * result is either the dividend (default, corresponds to SMT-LIB >=2.6) or
937 * an uninterpreted value (corresponds to SMT-LIB <2.6).
938 *
939 * Parameters:
940 * - 1..2: Terms of bit-vector sort (sorts must match)
941 *
942 * Create with:
943 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
944 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
945 */
946 BITVECTOR_UREM,
947 /**
948 * Two's complement signed division of two bit-vectors.
949 *
950 * Note: The semantics of this operator depends on `bv-div-zero-const`
951 * (default is true). By default, the function returns all ones if the
952 * dividend is positive and one if the dividend is negative (corresponds to
953 * SMT-LIB >=2.6). If the option is disabled, a division by zero is treated
954 * as an uninterpreted value (corresponds to SMT-LIB <2.6).
955 *
956 * Parameters:
957 * - 1..2: Terms of bit-vector sort (sorts must match)
958 *
959 * Create with:
960 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
961 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
962 */
963 BITVECTOR_SDIV,
964 /**
965 * Two's complement signed remainder of two bit-vectors
966 * (sign follows dividend).
967 *
968 * Note: The semantics of this operator depends on `bv-div-zero-const`
969 * (default is true, corresponds to SMT-LIB >=2.6). Depending on the setting,
970 * if the modulus is zero, the result is either the dividend (default) or an
971 * uninterpreted value (corresponds to SMT-LIB <2.6).
972 *
973 * Parameters:
974 * - 1..2: Terms of bit-vector sort (sorts must match)
975 *
976 * Create with:
977 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
978 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
979 */
980 BITVECTOR_SREM,
981 /**
982 * Two's complement signed remainder
983 * (sign follows divisor).
984 *
985 * Note: The semantics of this operator depends on `bv-div-zero-const`
986 * (default is on). Depending on the setting, if the modulus is zero, the
987 * result is either the dividend (default, corresponds to SMT-LIB >=2.6) or
988 * an uninterpreted value (corresponds to SMT-LIB <2.6).
989 *
990 * Parameters:
991 * - 1..2: Terms of bit-vector sort (sorts must match)
992 *
993 * Create with:
994 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
995 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
996 */
997 BITVECTOR_SMOD,
998 /**
999 * Bit-vector shift left.
1000 * The two bit-vector parameters must have same width.
1001 *
1002 * Parameters:
1003 * - 1..2: Terms of bit-vector sort (sorts must match)
1004 *
1005 * Create with:
1006 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
1007 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
1008 */
1009 BITVECTOR_SHL,
1010 /**
1011 * Bit-vector logical shift right.
1012 * The two bit-vector parameters must have same width.
1013 *
1014 * Parameters:
1015 * - 1..2: Terms of bit-vector sort (sorts must match)
1016 *
1017 * Create with:
1018 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
1019 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
1020 */
1021 BITVECTOR_LSHR,
1022 /**
1023 * Bit-vector arithmetic shift right.
1024 * The two bit-vector parameters must have same width.
1025 *
1026 * Parameters:
1027 * - 1..2: Terms of bit-vector sort (sorts must match)
1028 *
1029 * Create with:
1030 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
1031 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
1032 */
1033 BITVECTOR_ASHR,
1034 /**
1035 * Bit-vector unsigned less than.
1036 * The two bit-vector parameters must have same width.
1037 *
1038 * Parameters:
1039 * - 1..2: Terms of bit-vector sort (sorts must match)
1040 *
1041 * Create with:
1042 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
1043 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
1044 */
1045 BITVECTOR_ULT,
1046 /**
1047 * Bit-vector unsigned less than or equal.
1048 * The two bit-vector parameters must have same width.
1049 *
1050 * Parameters:
1051 * - 1..2: Terms of bit-vector sort (sorts must match)
1052 *
1053 * Create with:
1054 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
1055 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
1056 */
1057 BITVECTOR_ULE,
1058 /**
1059 * Bit-vector unsigned greater than.
1060 * The two bit-vector parameters must have same width.
1061 *
1062 * Parameters:
1063 * - 1..2: Terms of bit-vector sort (sorts must match)
1064 *
1065 * Create with:
1066 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
1067 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
1068 */
1069 BITVECTOR_UGT,
1070 /**
1071 * Bit-vector unsigned greater than or equal.
1072 * The two bit-vector parameters must have same width.
1073 *
1074 * Parameters:
1075 * - 1..2: Terms of bit-vector sort (sorts must match)
1076 *
1077 * Create with:
1078 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
1079 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
1080 */
1081 BITVECTOR_UGE,
1082 /**
1083 * Bit-vector signed less than.
1084 * The two bit-vector parameters must have same width.
1085 *
1086 * Parameters:
1087 * - 1..2: Terms of bit-vector sort (sorts must match)
1088 *
1089 * Create with:
1090 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
1091 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
1092 */
1093 BITVECTOR_SLT,
1094 /**
1095 * Bit-vector signed less than or equal.
1096 * The two bit-vector parameters must have same width.
1097 *
1098 * Parameters:
1099 * - 1..2: Terms of bit-vector sort (sorts must match)
1100 *
1101 * Create with:
1102 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
1103 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
1104 */
1105 BITVECTOR_SLE,
1106 /**
1107 * Bit-vector signed greater than.
1108 * The two bit-vector parameters must have same width.
1109 *
1110 * Parameters:
1111 * - 1..2: Terms of bit-vector sort (sorts must match)
1112 *
1113 * Create with:
1114 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
1115 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
1116 */
1117 BITVECTOR_SGT,
1118 /**
1119 * Bit-vector signed greater than or equal.
1120 * The two bit-vector parameters must have same width.
1121 *
1122 * Parameters:
1123 * - 1..2: Terms of bit-vector sort (sorts must match)
1124 *
1125 * Create with:
1126 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
1127 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
1128 */
1129 BITVECTOR_SGE,
1130 /**
1131 * Bit-vector unsigned less than, returns bit-vector of size 1.
1132 *
1133 * Parameters:
1134 * - 1..2: Terms of bit-vector sort (sorts must match)
1135 *
1136 * Create with:
1137 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
1138 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
1139 */
1140 BITVECTOR_ULTBV,
1141 /**
1142 * Bit-vector signed less than. returns bit-vector of size 1.
1143 *
1144 * Parameters:
1145 * - 1..2: Terms of bit-vector sort (sorts must match)
1146 *
1147 * Create with:
1148 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
1149 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
1150 */
1151 BITVECTOR_SLTBV,
1152 /**
1153 * Same semantics as regular ITE, but condition is bit-vector of size 1.
1154 *
1155 * Parameters:
1156 * - 1: Term of bit-vector sort of size 1, representing the condition
1157 * - 2: Term reprsenting the 'then' branch
1158 * - 3: Term representing the 'else' branch
1159 *
1160 * 'then' and 'else' term must have same base sort.
1161 *
1162 * Create with:
1163 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
1164 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
1165 */
1166 BITVECTOR_ITE,
1167 /**
1168 * Bit-vector redor.
1169 *
1170 * Parameters:
1171 * - 1: Term of bit-vector sort
1172 *
1173 * Create with:
1174 * - `Solver::mkTerm(Kind kind, const Term& child) const`
1175 */
1176 BITVECTOR_REDOR,
1177 /**
1178 * Bit-vector redand.
1179 *
1180 * Parameters:
1181 * - 1: Term of bit-vector sort
1182 *
1183 * Create with:
1184 * - `Solver::mkTerm(Kind kind, const Term& child) const`
1185 */
1186 BITVECTOR_REDAND,
1187 #if 0
1188 /* formula to be treated as a bv atom via eager bit-blasting
1189 * (internal-only symbol) */
1190 BITVECTOR_EAGER_ATOM,
1191 /* term to be treated as a variable. used for eager bit-blasting Ackermann
1192 * expansion of bvudiv (internal-only symbol) */
1193 BITVECTOR_ACKERMANIZE_UDIV,
1194 /* term to be treated as a variable. used for eager bit-blasting Ackermann
1195 * expansion of bvurem (internal-only symbol) */
1196 BITVECTOR_ACKERMANIZE_UREM,
1197 #endif
1198 /**
1199 * Operator for bit-vector extract (from index 'high' to 'low').
1200 *
1201 * Parameters:
1202 * - 1: The 'high' index
1203 * - 2: The 'low' index
1204 *
1205 * Create with:
1206 * - `Solver::mkOp(Kind kind, uint32_t param, uint32_t param) const`
1207 *
1208 * Apply bit-vector extract.
1209 *
1210 * Parameters:
1211 * - 1: Op of kind BITVECTOR_EXTRACT
1212 * - 2: Term of bit-vector sort
1213 *
1214 * Create with:
1215 * - `Solver::mkTerm(const Op& op, const Term& child) const`
1216 * - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const`
1217 */
1218 BITVECTOR_EXTRACT,
1219 /**
1220 * Operator for bit-vector repeat.
1221 *
1222 * Parameter:
1223 * - 1: Number of times to repeat a given bit-vector
1224 *
1225 * Create with:
1226 * - `Solver::mkOp(Kind kind, uint32_t param) const`.
1227 *
1228 * Apply bit-vector repeat.
1229 *
1230 * Parameters:
1231 * - 1: Op of kind BITVECTOR_REPEAT
1232 * - 2: Term of bit-vector sort
1233 *
1234 * Create with:
1235 * - `Solver::mkTerm(const Op& op, const Term& child) const`
1236 * - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const`
1237 */
1238 BITVECTOR_REPEAT,
1239 /**
1240 * Operator for bit-vector zero-extend.
1241 *
1242 * Parameter:
1243 * - 1: Number of bits by which a given bit-vector is to be extended
1244 *
1245 * Create with:
1246 * - `Solver::mkOp(Kind kind, uint32_t param) const`.
1247 *
1248 * Apply bit-vector zero-extend.
1249 *
1250 * Parameters:
1251 * - 1: Op of kind BITVECTOR_ZERO_EXTEND
1252 * - 2: Term of bit-vector sort
1253 *
1254 * Create with:
1255 * - `Solver::mkTerm(const Op& op, const Term& child) const`
1256 * - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const`
1257 */
1258 BITVECTOR_ZERO_EXTEND,
1259 /**
1260 * Operator for bit-vector sign-extend.
1261 *
1262 * Parameter:
1263 * - 1: Number of bits by which a given bit-vector is to be extended
1264 *
1265 * Create with:
1266 * - `Solver::mkOp(Kind kind, uint32_t param) const`.
1267 *
1268 * Apply bit-vector sign-extend.
1269 *
1270 * Parameters:
1271 * - 1: Op of kind BITVECTOR_SIGN_EXTEND
1272 * - 2: Term of bit-vector sort
1273 *
1274 * Create with:
1275 * - `Solver::mkTerm(const Op& op, const Term& child) const`
1276 * - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const`
1277 */
1278 BITVECTOR_SIGN_EXTEND,
1279 /**
1280 * Operator for bit-vector rotate left.
1281 *
1282 * Parameter:
1283 * - 1: Number of bits by which a given bit-vector is to be rotated
1284 *
1285 * Create with:
1286 * - `Solver::mkOp(Kind kind, uint32_t param) const`.
1287 *
1288 * Apply bit-vector rotate left.
1289 *
1290 * Parameters:
1291 * - 1: Op of kind BITVECTOR_ROTATE_LEFT
1292 * - 2: Term of bit-vector sort
1293 *
1294 * Create with:
1295 * - `Solver::mkTerm(const Op& op, const Term& child) const`
1296 * - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const`
1297 */
1298 BITVECTOR_ROTATE_LEFT,
1299 /**
1300 * Operator for bit-vector rotate right.
1301 *
1302 * Parameter:
1303 * - 1: Number of bits by which a given bit-vector is to be rotated
1304 *
1305 * Create with:
1306 * - `Solver::mkOp(Kind kind, uint32_t param) const`.
1307 *
1308 * Apply bit-vector rotate right.
1309 *
1310 * Parameters:
1311 * - 1: Op of kind BITVECTOR_ROTATE_RIGHT
1312 * - 2: Term of bit-vector sort
1313 *
1314 * Create with:
1315 * - `Solver::mkTerm(const Op& op, const Term& child) const`
1316 * - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const`
1317 */
1318 BITVECTOR_ROTATE_RIGHT,
1319 #if 0
1320 /* bit-vector boolean bit extract. */
1321 BITVECTOR_BITOF,
1322 #endif
1323 /**
1324 * Operator for the conversion from Integer to bit-vector.
1325 *
1326 * Parameter:
1327 * - 1: Size of the bit-vector to convert to
1328 *
1329 * Create with:
1330 * - `Solver::mkOp(Kind kind, uint32_t param) const`.
1331 *
1332 * Apply integer conversion to bit-vector.
1333 *
1334 * Parameters:
1335 * - 1: Op of kind INT_TO_BITVECTOR
1336 * - 2: Integer term
1337 *
1338 * Create with:
1339 * - `Solver::mkTerm(const Op& op, const Term& child) const`
1340 * - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const`
1341 */
1342 INT_TO_BITVECTOR,
1343 /**
1344 * Bit-vector conversion to (nonnegative) integer.
1345 *
1346 * Parameter:
1347 * - 1: Term of bit-vector sort
1348 *
1349 * Create with:
1350 * - `Solver::mkTerm(Kind kind, const Term& child) const`
1351 */
1352 BITVECTOR_TO_NAT,
1353
1354 /* FP -------------------------------------------------------------------- */
1355
1356 /**
1357 * Floating-point constant, constructed from a double or string.
1358 *
1359 * Parameters:
1360 * - 1: Size of the exponent
1361 * - 2: Size of the significand
1362 * - 3: Value of the floating-point constant as a bit-vector term
1363 *
1364 * Create with:
1365 * - `Solver::mkFloatingPoint(uint32_t exp, uint32_t sig, Term val) const`
1366 */
1367 CONST_FLOATINGPOINT,
1368 /**
1369 * Floating-point rounding mode term.
1370 *
1371 * Create with:
1372 * - `Solver::mkRoundingMode(RoundingMode rm) const`
1373 */
1374 CONST_ROUNDINGMODE,
1375 /**
1376 * Create floating-point literal from bit-vector triple.
1377 *
1378 * Parameters:
1379 * - 1: Sign bit as a bit-vector term
1380 * - 2: Exponent bits as a bit-vector term
1381 * - 3: Significand bits as a bit-vector term (without hidden bit)
1382 *
1383 * Create with:
1384 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
1385 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
1386 */
1387 FLOATINGPOINT_FP,
1388 /**
1389 * Floating-point equality.
1390 *
1391 * Parameters:
1392 * - 1..2: Terms of floating point sort
1393 *
1394 * Create with:
1395 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
1396 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
1397 */
1398 FLOATINGPOINT_EQ,
1399 /**
1400 * Floating-point absolute value.
1401 *
1402 * Parameters:
1403 * - 1: Term of floating point sort
1404 *
1405 * Create with:
1406 * - `Solver::mkTerm(Kind kind, const Term& child) const`
1407 */
1408 FLOATINGPOINT_ABS,
1409 /**
1410 * Floating-point negation.
1411 *
1412 * Parameters:
1413 * - 1: Term of floating point sort
1414 *
1415 * Create with:
1416 * - `Solver::mkTerm(Kind kind, const Term& child) const`
1417 */
1418 FLOATINGPOINT_NEG,
1419 /**
1420 * Floating-point addition.
1421 *
1422 * Parameters:
1423 * - 1: CONST_ROUNDINGMODE
1424 * - 2: Term of sort FloatingPoint
1425 * - 3: Term of sort FloatingPoint
1426 *
1427 * Create with:
1428 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
1429 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
1430 */
1431 FLOATINGPOINT_PLUS,
1432 /**
1433 * Floating-point sutraction.
1434 *
1435 * Parameters:
1436 * - 1: CONST_ROUNDINGMODE
1437 * - 2: Term of sort FloatingPoint
1438 * - 3: Term of sort FloatingPoint
1439 *
1440 * Create with:
1441 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
1442 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
1443 */
1444 FLOATINGPOINT_SUB,
1445 /**
1446 * Floating-point multiply.
1447 *
1448 * Parameters:
1449 * - 1: CONST_ROUNDINGMODE
1450 * - 2: Term of sort FloatingPoint
1451 * - 3: Term of sort FloatingPoint
1452 *
1453 * Create with:
1454 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
1455 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
1456 */
1457 FLOATINGPOINT_MULT,
1458 /**
1459 * Floating-point division.
1460 *
1461 * Parameters:
1462 * - 1: CONST_ROUNDINGMODE
1463 * - 2: Term of sort FloatingPoint
1464 * - 3: Term of sort FloatingPoint
1465 *
1466 * Create with:
1467 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
1468 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
1469 */
1470 FLOATINGPOINT_DIV,
1471 /**
1472 * Floating-point fused multiply and add.
1473 *
1474 * Parameters:
1475 * - 1: CONST_ROUNDINGMODE
1476 * - 2: Term of sort FloatingPoint
1477 * - 3: Term of sort FloatingPoint
1478 * - 4: Term of sort FloatingPoint
1479 *
1480 * Create with:
1481 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
1482 */
1483 FLOATINGPOINT_FMA,
1484 /**
1485 * Floating-point square root.
1486 *
1487 * Parameters:
1488 * - 1: CONST_ROUNDINGMODE
1489 * - 2: Term of sort FloatingPoint
1490 *
1491 * Create with:
1492 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
1493 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
1494 */
1495 FLOATINGPOINT_SQRT,
1496 /**
1497 * Floating-point remainder.
1498 *
1499 * Parameters:
1500 * - 1..2: Terms of floating point sort
1501 *
1502 * Create with:
1503 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
1504 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
1505 */
1506 FLOATINGPOINT_REM,
1507 /**
1508 * Floating-point round to integral.
1509 *
1510 * Parameters:
1511 * -1..2: Terms of floating point sort
1512 *
1513 * Create with:
1514 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
1515 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
1516 */
1517 FLOATINGPOINT_RTI,
1518 /**
1519 * Floating-point minimum.
1520 *
1521 * Parameters:
1522 * - 1..2: Terms of floating point sort
1523 *
1524 * Create with:
1525 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
1526 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
1527 */
1528 FLOATINGPOINT_MIN,
1529 /**
1530 * Floating-point maximum.
1531 *
1532 * Parameters:
1533 * - 1..2: Terms of floating point sort
1534 *
1535 * Create with:
1536 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
1537 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
1538 */
1539 FLOATINGPOINT_MAX,
1540 /**
1541 * Floating-point less than or equal.
1542 *
1543 * Parameters:
1544 * - 1..2: Terms of floating point sort
1545 *
1546 * Create with:
1547 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
1548 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
1549 */
1550 FLOATINGPOINT_LEQ,
1551 /**
1552 * Floating-point less than.
1553 *
1554 * Parameters:
1555 * - 1..2: Terms of floating point sort
1556 *
1557 * Create with:
1558 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
1559 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
1560 */
1561 FLOATINGPOINT_LT,
1562 /**
1563 * Floating-point greater than or equal.
1564 *
1565 * Parameters:
1566 * - 1..2: Terms of floating point sort
1567 *
1568 * Create with:
1569 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
1570 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
1571 */
1572 FLOATINGPOINT_GEQ,
1573 /**
1574 * Floating-point greater than.
1575 *
1576 * Parameters:
1577 * - 1..2: Terms of floating point sort
1578 *
1579 * Create with:
1580 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
1581 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
1582 */
1583 FLOATINGPOINT_GT,
1584 /**
1585 * Floating-point is normal.
1586 *
1587 * Parameters:
1588 * - 1: Term of floating point sort
1589 *
1590 * Create with:
1591 * - `Solver::mkTerm(Kind kind, const Term& child) const`
1592 */
1593 FLOATINGPOINT_ISN,
1594 /**
1595 * Floating-point is sub-normal.
1596 *
1597 * Parameters:
1598 * - 1: Term of floating point sort
1599 *
1600 * Create with:
1601 * - `Solver::mkTerm(Kind kind, const Term& child) const`
1602 */
1603 FLOATINGPOINT_ISSN,
1604 /**
1605 * Floating-point is zero.
1606 *
1607 * Parameters:
1608 * - 1: Term of floating point sort
1609 *
1610 * Create with:
1611 * - `Solver::mkTerm(Kind kind, const Term& child) const`
1612 */
1613 FLOATINGPOINT_ISZ,
1614 /**
1615 * Floating-point is infinite.
1616 *
1617 * Parameters:
1618 * - 1: Term of floating point sort
1619 *
1620 * Create with:
1621 * - `Solver::mkTerm(Kind kind, const Term& child) const`
1622 */
1623 FLOATINGPOINT_ISINF,
1624 /**
1625 * Floating-point is NaN.
1626 *
1627 * Parameters:
1628 * - 1: Term of floating point sort
1629 *
1630 * Create with:
1631 * - `Solver::mkTerm(Kind kind, const Term& child) const`
1632 */
1633 FLOATINGPOINT_ISNAN,
1634 /**
1635 * Floating-point is negative.
1636 *
1637 * Parameters:
1638 * - 1: Term of floating point sort
1639 *
1640 * Create with:
1641 * - `Solver::mkTerm(Kind kind, const Term& child) const`
1642 */
1643 FLOATINGPOINT_ISNEG,
1644 /**
1645 * Floating-point is positive.
1646 *
1647 * Parameters:
1648 * - 1: Term of floating point sort
1649 *
1650 * Create with:
1651 * - `Solver::mkTerm(Kind kind, const Term& child) const`
1652 */
1653 FLOATINGPOINT_ISPOS,
1654 /**
1655 * Operator for to_fp from bit vector.
1656 *
1657 * Parameters:
1658 * - 1: Exponent size
1659 * - 2: Significand size
1660 *
1661 * Create with:
1662 * - `Solver::mkOp(Kind kind, uint32_t param1, uint32_t param2) const`
1663 *
1664 * Conversion from an IEEE-754 bit vector to floating-point.
1665 *
1666 * Parameters:
1667 * - 1: Op of kind FLOATINGPOINT_TO_FP_IEEE_BITVECTOR
1668 * - 2: Term of sort FloatingPoint
1669 *
1670 * Create with:
1671 * - `Solver::mkTerm(const Op& op, const Term& child) const`
1672 * - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const`
1673 */
1674 FLOATINGPOINT_TO_FP_IEEE_BITVECTOR,
1675 /**
1676 * Operator for to_fp from floating point.
1677 *
1678 * Parameters:
1679 * - 1: Exponent size
1680 * - 2: Significand size
1681 *
1682 * Create with:
1683 * - `Solver::mkOp(Kind kind, uint32_t param1, uint32_t param2) const`
1684 *
1685 * Conversion between floating-point sorts.
1686 *
1687 * Parameters:
1688 * - 1: Op of kind FLOATINGPOINT_TO_FP_FLOATINGPOINT
1689 * - 2: Term of sort FloatingPoint
1690 *
1691 * Create with:
1692 * - `Solver::mkTerm(const Op& op, const Term& child) const`
1693 * - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const`
1694 */
1695 FLOATINGPOINT_TO_FP_FLOATINGPOINT,
1696 /**
1697 * Operator for to_fp from real.
1698 *
1699 * Parameters:
1700 * - 1: Exponent size
1701 * - 2: Significand size
1702 *
1703 * Create with:
1704 * - `Solver::mkOp(Kind kind, uint32_t param1, uint32_t param2) const`
1705 *
1706 * Conversion from a real to floating-point.
1707 *
1708 * Parameters:
1709 * - 1: Op of kind FLOATINGPOINT_TO_FP_REAL
1710 * - 2: Term of sort FloatingPoint
1711 *
1712 * Create with:
1713 * - `Solver::mkTerm(const Op& op, const Term& child) const`
1714 * - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const`
1715 */
1716 FLOATINGPOINT_TO_FP_REAL,
1717 /**
1718 * Operator for to_fp from signed bit vector
1719 *
1720 * Parameters:
1721 * - 1: Exponent size
1722 * - 2: Significand size
1723 *
1724 * Create with:
1725 * - `Solver::mkOp(Kind kind, uint32_t param1, uint32_t param2) const`
1726 *
1727 * Conversion from a signed bit vector to floating-point.
1728 *
1729 * Parameters:
1730 * - 1: Op of kind FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR
1731 * - 2: Term of sort FloatingPoint
1732 *
1733 * Create with:
1734 * - `Solver::mkTerm(const Op& op, const Term& child) const`
1735 * - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const`
1736 */
1737 FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR,
1738 /**
1739 * Operator for to_fp from unsigned bit vector.
1740 *
1741 * Parameters:
1742 * - 1: Exponent size
1743 * - 2: Significand size
1744 *
1745 * Create with:
1746 * - `Solver::mkOp(Kind kind, uint32_t param1, uint32_t param2) const`
1747 *
1748 * Converting an unsigned bit vector to floating-point.
1749 *
1750 * Parameters:
1751 * - 1: Op of kind FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR
1752 * - 2: Term of sort FloatingPoint
1753 *
1754 * Create with:
1755 * - `Solver::mkTerm(const Op& op, const Term& child) const`
1756 * - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const`
1757 */
1758 FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR,
1759 /**
1760 * Operator for a generic to_fp.
1761 *
1762 * Parameters:
1763 * - 1: exponent size
1764 * - 2: Significand size
1765 *
1766 * Create with:
1767 * - `Solver::mkOp(Kind kind, uint32_t param1, uint32_t param2) const`
1768 *
1769 * Generic conversion to floating-point, used in parsing only.
1770 *
1771 * Parameters:
1772 * - 1: Op of kind FLOATINGPOINT_TO_FP_GENERIC
1773 * - 2: Term of sort FloatingPoint
1774 *
1775 * Create with:
1776 * - `Solver::mkTerm(const Op& op, const Term& child) const`
1777 * - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const`
1778 */
1779 FLOATINGPOINT_TO_FP_GENERIC,
1780 /**
1781 * Operator for to_ubv.
1782 *
1783 * Parameters:
1784 * - 1: Size of the bit-vector to convert to
1785 *
1786 * Create with:
1787 * - `Solver::mkOp(Kind kind, uint32_t param) const`
1788 *
1789 * Conversion from a floating-point value to an unsigned bit vector.
1790 *
1791 * Parameters:
1792 * - 1: Op of kind FLOATINGPOINT_TO_FP_TO_UBV
1793 * - 2: Term of sort FloatingPoint
1794 *
1795 * Create with:
1796 * - `Solver::mkTerm(const Op& op, const Term& child) const`
1797 * - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const`
1798 */
1799 FLOATINGPOINT_TO_UBV,
1800 /**
1801 * Operator for to_sbv.
1802 *
1803 * Parameters:
1804 * - 1: Size of the bit-vector to convert to
1805 *
1806 * Create with:
1807 * - `Solver::mkOp(Kind kind, uint32_t param) const`
1808 *
1809 * Conversion from a floating-point value to a signed bit vector.
1810 *
1811 * Parameters:
1812 * - 1: Op of kind FLOATINGPOINT_TO_FP_TO_SBV
1813 * - 2: Term of sort FloatingPoint
1814 *
1815 * Create with:
1816 * - `Solver::mkTerm(const Op& op, const Term& child) const`
1817 * - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const`
1818 */
1819 FLOATINGPOINT_TO_SBV,
1820 /**
1821 * Floating-point to real.
1822 *
1823 * Parameters:
1824 * - 1: Term of sort FloatingPoint
1825 *
1826 * Create with:
1827 * - `Solver::mkTerm(Kind kind, const Term& child) const`
1828 */
1829 FLOATINGPOINT_TO_REAL,
1830
1831 /* Arrays ---------------------------------------------------------------- */
1832
1833 /**
1834 * Array select.
1835 *
1836 * Parameters:
1837 * - 1: Term of array sort
1838 * - 2: Selection index
1839 *
1840 * Create with:
1841 * - `Solver::mkTerm(const Op& op, const Term& child1, const Term& child2) const`
1842 * - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const`
1843 */
1844 SELECT,
1845 /**
1846 * Array store.
1847 *
1848 * Parameters:
1849 * - 1: Term of array sort
1850 * - 2: Store index
1851 * - 3: Term to store at the index
1852 *
1853 * Create with:
1854 * - `Solver::mkTerm(const Op& op, const Term& child1, const Term& child2, const Term& child3) const`
1855 * - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const`
1856 */
1857 STORE,
1858 /**
1859 * Constant array.
1860 *
1861 * Parameters:
1862 * - 1: Array sort
1863 * - 2: Term representing a constant
1864 *
1865 * Create with:
1866 * - `Solver::mkTerm(const Op& op, const Term& child1, const Term& child2) const`
1867 * - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const`
1868 *
1869 * Note: We currently support the creation of constant arrays, but under some
1870 * conditions when there is a chain of equalities connecting two constant
1871 * arrays, the solver doesn't know what to do and aborts (Issue <a href="https://github.com/CVC4/CVC4/issues/1667">#1667</a>).
1872 */
1873 CONST_ARRAY,
1874 /**
1875 * Equality over arrays a and b over a given range [i,j], i.e.,
1876 * @f[
1877 * \forall k . i \leq k \leq j \Rightarrow a[k] = b[k]
1878 * @f]
1879 *
1880 * Parameters:
1881 * - 1: First array
1882 * - 2: Second array
1883 * - 3: Lower bound of range (inclusive)
1884 * - 4: Uppper bound of range (inclusive)
1885 *
1886 * Create with:
1887 * - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const`
1888 *
1889 * Note: We currently support the creation of array equalities over index
1890 * types bit-vector, floating-point, integer and real. Option --arrays-exp is
1891 * required to support this operator.
1892 */
1893 EQ_RANGE,
1894 #if 0
1895 /* array table function (internal-only symbol) */
1896 ARR_TABLE_FUN,
1897 /* array lambda (internal-only symbol) */
1898 ARRAY_LAMBDA,
1899 /* partial array select, for internal use only */
1900 PARTIAL_SELECT_0,
1901 /* partial array select, for internal use only */
1902 PARTIAL_SELECT_1,
1903 #endif
1904
1905 /* Datatypes ------------------------------------------------------------- */
1906
1907 /**
1908 * Constructor application.
1909 *
1910 * Paramters: n > 0
1911 * - 1: Constructor (operator)
1912 * - 2..n: Parameters to the constructor
1913 *
1914 * Create with:
1915 * - `Solver::mkTerm(const Op& op) const`
1916 * - `Solver::mkTerm(const Op& op, const Term& child) const`
1917 * - `Solver::mkTerm(const Op& op, const Term& child1, const Term& child2) const`
1918 * - `Solver::mkTerm(const Op& op, const Term& child1, const Term& child2, const Term& child3) const`
1919 * - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const`
1920 */
1921 APPLY_CONSTRUCTOR,
1922 /**
1923 * Datatype selector application, which is undefined if misapplied.
1924 *
1925 * Parameters:
1926 * - 1: Selector (operator)
1927 * - 2: Datatype term
1928 *
1929 * Create with:
1930 * - `Solver::mkTerm(const Op& op, const Term& child) const`
1931 */
1932 APPLY_SELECTOR,
1933 /**
1934 * Datatype tester application.
1935 *
1936 * Parameters:
1937 * - 1: Tester term
1938 * - 2: Datatype term
1939 *
1940 * Create with:
1941 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
1942 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
1943 */
1944 APPLY_TESTER,
1945 /**
1946 * Datatype update application, which does not change the argument if
1947 * misapplied.
1948 *
1949 * Parameters:
1950 * - 1: Updater (operator)
1951 * - 2: Datatype term
1952 * - 3: Value to update a field of the datatype term with
1953 *
1954 * Create with:
1955 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
1956 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
1957 */
1958 APPLY_UPDATER,
1959 /**
1960 * Match expressions.
1961 * For example, the smt2 syntax match term
1962 * `(match l (((cons h t) h) (nil 0)))`
1963 * is represented by the AST
1964 *
1965 * (MATCH l
1966 * (MATCH_BIND_CASE (BOUND_VAR_LIST h t) (cons h t) h)
1967 * (MATCH_CASE nil 0))
1968 *
1969 * The type of the last argument of each case term could be equal.
1970 *
1971 * Parameters: n > 1
1972 * - 1..n: Terms of kind MATCH_CASE or MATCH_BIND_CASE
1973 *
1974 * Create with:
1975 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
1976 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
1977 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
1978 *
1979 */
1980 MATCH,
1981 /**
1982 * Match case
1983 * A (constant) case expression to be used within a match expression.
1984 *
1985 * Parameters:
1986 * - 1: Term denoting the pattern expression
1987 * - 2: Term denoting the return value
1988 *
1989 * Create with:
1990 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
1991 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
1992 */
1993 MATCH_CASE,
1994 /**
1995 * Match bind case
1996 * A (non-constant) case expression to be used within a match expression.
1997 *
1998 * Parameters:
1999 * - 1: a BOUND_VAR_LIST Term containing the free variables of the case
2000 * - 2: Term denoting the pattern expression
2001 * - 3: Term denoting the return value
2002 *
2003 * Create with:
2004 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
2005 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
2006 */
2007 MATCH_BIND_CASE,
2008 /**
2009 * Datatypes size
2010 * An operator mapping datatypes to an integer denoting the number of
2011 * non-nullary applications of constructors they contain.
2012 *
2013 * Parameters:
2014 * - 1: Datatype term
2015 *
2016 * Create with:
2017 * - `Solver::mkTerm(Kind kind, const Term& child1) const`
2018 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
2019 */
2020 DT_SIZE,
2021 /**
2022 * Operator for tuple projection indices
2023 *
2024 * Parameters:
2025 * - 1: The tuple projection indices
2026 *
2027 * Create with:
2028 * - `Solver::mkOp(Kind TUPLE_PROJECT, std::vector<uint32_t> param) const`
2029 *
2030 * Constructs a new tuple from an existing one using the elements at the
2031 * given indices
2032 *
2033 * Parameters:
2034 * - 1: a term of tuple sort
2035 *
2036 * Create with:
2037 * - `Solver::mkTerm(const Op& op, const Term& child) const`
2038 * - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const`
2039 */
2040 TUPLE_PROJECT,
2041 #if 0
2042 /* datatypes height bound */
2043 DT_HEIGHT_BOUND,
2044 /* datatypes height bound */
2045 DT_SIZE_BOUND,
2046 /* datatypes sygus bound */
2047 DT_SYGUS_BOUND,
2048 /* datatypes sygus term order */
2049 DT_SYGUS_TERM_ORDER,
2050 /* datatypes sygus is constant */
2051 DT_SYGUS_IS_CONST,
2052 #endif
2053
2054 /* Separation Logic ------------------------------------------------------ */
2055
2056 /**
2057 * Separation logic nil term.
2058 *
2059 * Parameters: none
2060 *
2061 * Create with:
2062 * - `Solver::mkSepNil(const Sort& sort) const`
2063 */
2064 SEP_NIL,
2065 /**
2066 * Separation logic empty heap.
2067 *
2068 * Parameters:
2069 * - 1: Term of the same sort as the sort of the location of the heap
2070 * that is constrained to be empty
2071 * - 2: Term of the same sort as the data sort of the heap that is
2072 * that is constrained to be empty
2073 *
2074 * Create with:
2075 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
2076 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
2077 */
2078 SEP_EMP,
2079 /**
2080 * Separation logic points-to relation.
2081 *
2082 * Parameters:
2083 * - 1: Location of the points-to constraint
2084 * - 2: Data of the points-to constraint
2085 *
2086 * Create with:
2087 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
2088 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
2089 */
2090 SEP_PTO,
2091 /**
2092 * Separation logic star.
2093 *
2094 * Parameters: n > 1
2095 * - 1..n: Child constraints that hold in disjoint (separated) heaps
2096 *
2097 * Create with:
2098 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
2099 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
2100 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
2101 */
2102 SEP_STAR,
2103 /**
2104 * Separation logic magic wand.
2105 *
2106 * Parameters:
2107 * - 1: Antecendant of the magic wand constraint
2108 * - 2: Conclusion of the magic wand constraint, which is asserted to
2109 * hold in all heaps that are disjoint extensions of the antecedent.
2110 *
2111 * Create with:
2112 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
2113 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
2114 */
2115 SEP_WAND,
2116 #if 0
2117 /* separation label (internal use only) */
2118 SEP_LABEL,
2119 #endif
2120
2121 /* Sets ------------------------------------------------------------------ */
2122
2123 /**
2124 * Empty set constant.
2125 *
2126 * Parameters:
2127 * - 1: Sort of the set elements
2128 *
2129 * Create with:
2130 * - `Solver::mkEmptySet(const Sort& sort) const`
2131 */
2132 EMPTYSET,
2133 /**
2134 * Set union.
2135 *
2136 * Parameters:
2137 * - 1..2: Terms of set sort
2138 *
2139 * Create with:
2140 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
2141 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
2142 */
2143 UNION,
2144 /**
2145 * Set intersection.
2146 *
2147 * Parameters:
2148 * - 1..2: Terms of set sort
2149 *
2150 * Create with:
2151 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
2152 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
2153 */
2154 INTERSECTION,
2155 /**
2156 * Set subtraction.
2157 *
2158 * Parameters:
2159 * - 1..2: Terms of set sort
2160 *
2161 * Create with:
2162 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
2163 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
2164 */
2165 SETMINUS,
2166 /**
2167 * Subset predicate.
2168 *
2169 * Parameters:
2170 * - 1..2: Terms of set sort, [1] a subset of set [2]?
2171 *
2172 * Create with:
2173 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
2174 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
2175 */
2176 SUBSET,
2177 /**
2178 * Set membership predicate.
2179 *
2180 * Parameters:
2181 * - 1..2: Terms of set sort, [1] a member of set [2]?
2182 *
2183 * Create with:
2184 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
2185 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
2186 */
2187 MEMBER,
2188 /**
2189 * Construct a singleton set from an element given as a parameter.
2190 * The returned set has same type of the element.
2191 *
2192 * Parameters:
2193 * - 1: Single element
2194 *
2195 * Create with:
2196 * - `Solver::mkTerm(Kind kind, const Term& child) const`
2197 */
2198 SINGLETON,
2199 /**
2200 * The set obtained by inserting elements;
2201 *
2202 * Parameters: n > 0
2203 * - 1..n-1: Elements inserted into set [n]
2204 * - n: Set Term
2205 *
2206 * Create with:
2207 * - `Solver::mkTerm(Kind kind, const Term& child) const`
2208 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
2209 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
2210 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
2211 */
2212 INSERT,
2213 /**
2214 * Set cardinality.
2215 *
2216 * Parameters:
2217 * - 1: Set to determine the cardinality of
2218 *
2219 * Create with:
2220 * - `Solver::mkTerm(Kind kind, const Term& child) const`
2221 */
2222 CARD,
2223 /**
2224 * Set complement with respect to finite universe.
2225 *
2226 * Parameters:
2227 * - 1: Set to complement
2228 *
2229 * Create with:
2230 * - `Solver::mkTerm(Kind kind, const Term& child) const`
2231 */
2232 COMPLEMENT,
2233 /**
2234 * Finite universe set.
2235 * All set variables must be interpreted as subsets of it.
2236 *
2237 * Create with:
2238 * - `Solver::mkUniverseSet(const Sort& sort) const`
2239 */
2240 UNIVERSE_SET,
2241 /**
2242 * Set join.
2243 *
2244 * Parameters:
2245 * - 1..2: Terms of set sort
2246 *
2247 * Create with:
2248 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
2249 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
2250 */
2251 JOIN,
2252 /**
2253 * Set cartesian product.
2254 *
2255 * Parameters:
2256 * - 1..2: Terms of set sort
2257 *
2258 * Create with:
2259 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
2260 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
2261 */
2262 PRODUCT,
2263 /**
2264 * Set transpose.
2265 *
2266 * Parameters:
2267 * - 1: Term of set sort
2268 *
2269 * Create with:
2270 * - `Solver::mkTerm(Kind kind, const Term& child) const`
2271 */
2272 TRANSPOSE,
2273 /**
2274 * Set transitive closure.
2275 *
2276 * Parameters:
2277 * - 1: Term of set sort
2278 *
2279 * Create with:
2280 * - `Solver::mkTerm(Kind kind, const Term& child) const`
2281 */
2282 TCLOSURE,
2283 /**
2284 * Set join image.
2285 *
2286 * Parameters:
2287 * - 1..2: Terms of set sort
2288 *
2289 * Create with:
2290 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
2291 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
2292 */
2293 JOIN_IMAGE,
2294 /**
2295 * Set identity.
2296 *
2297 * Parameters:
2298 * - 1: Term of set sort
2299 *
2300 * Create with:
2301 * - `Solver::mkTerm(Kind kind, const Term& child) const`
2302 */
2303 IDEN,
2304 /**
2305 * Set comprehension
2306 * A set comprehension is specified by a bound variable list x1 ... xn,
2307 * a predicate P[x1...xn], and a term t[x1...xn]. A comprehension C with the
2308 * above form has members given by the following semantics:
2309 * @f[
2310 * \forall y. ( \exists x_1...x_n. P[x_1...x_n] \hat{} t[x_1...x_n] = y )
2311 * \Leftrightarrow (member y C)
2312 * @f]
2313 * where y ranges over the element type of the (set) type of the
2314 * comprehension. If @f$ t[x_1..x_n] @f$ is not provided, it is equivalent to
2315 * y in the above formula.
2316 *
2317 * Parameters:
2318 * - 1: Term BOUND_VAR_LIST
2319 * - 2: Term denoting the predicate of the comprehension
2320 * - 3: (optional) a Term denoting the generator for the comprehension
2321 *
2322 * Create with:
2323 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
2324 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
2325 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
2326 */
2327 COMPREHENSION,
2328 /**
2329 * Returns an element from a given set.
2330 * If a set A = {x}, then the term (choose A) is equivalent to the term x.
2331 * If the set is empty, then (choose A) is an arbitrary value.
2332 * If the set has cardinality > 1, then (choose A) will deterministically
2333 * return an element in A.
2334 *
2335 * Parameters:
2336 * - 1: Term of set sort
2337 *
2338 * Create with:
2339 * - `Solver::mkTerm(Kind kind, const Term& child) const`
2340 */
2341 CHOOSE,
2342 /**
2343 * Set is_singleton predicate.
2344 *
2345 * Parameters:
2346 * - 1: Term of set sort, is [1] a singleton set?
2347 *
2348 * Create with:
2349 * - `Solver::mkTerm(Kind kind, const Term& child) const`
2350 */
2351 IS_SINGLETON,
2352 /* Bags ------------------------------------------------------------------ */
2353 /**
2354 * Empty bag constant.
2355 *
2356 * Parameters:
2357 * - 1: Sort of the bag elements
2358 *
2359 * Create with:
2360 * mkEmptyBag(const Sort& sort)
2361 */
2362 EMPTYBAG,
2363 /**
2364 * Bag max union.
2365 * Parameters:
2366 * - 1..2: Terms of bag sort
2367 *
2368 * Create with:
2369 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
2370 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
2371 */
2372 UNION_MAX,
2373 /**
2374 * Bag disjoint union (sum).
2375 *
2376 * Parameters:
2377 * -1..2: Terms of bag sort
2378 *
2379 * Create with:
2380 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
2381 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
2382 */
2383 UNION_DISJOINT,
2384 /**
2385 * Bag intersection (min).
2386 *
2387 * Parameters:
2388 * - 1..2: Terms of bag sort
2389 *
2390 * Create with:
2391 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
2392 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
2393 */
2394 INTERSECTION_MIN,
2395 /**
2396 * Bag difference subtract (subtracts multiplicities of the second from the
2397 * first).
2398 *
2399 * Parameters:
2400 * - 1..2: Terms of bag sort
2401 *
2402 * Create with:
2403 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
2404 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
2405 */
2406 DIFFERENCE_SUBTRACT,
2407 /**
2408 * Bag difference 2 (removes shared elements in the two bags).
2409 *
2410 * Parameters:
2411 * - 1..2: Terms of bag sort
2412 *
2413 * Create with:
2414 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
2415 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
2416 */
2417 DIFFERENCE_REMOVE,
2418 /**
2419 * Inclusion predicate for bags
2420 * (multiplicities of the first bag <= multiplicities of the second bag).
2421 *
2422 * Parameters:
2423 * - 1..2: Terms of bag sort
2424 *
2425 * Create with:
2426 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
2427 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
2428 */
2429 SUBBAG,
2430 /**
2431 * Element multiplicity in a bag
2432 *
2433 * Parameters:
2434 * - 1..2: Terms of bag sort (Bag E), [1] an element of sort E
2435 *
2436 * Create with:
2437 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
2438 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
2439 */
2440 BAG_COUNT,
2441 /**
2442 * Eliminate duplicates in a given bag. The returned bag contains exactly the
2443 * same elements in the given bag, but with multiplicity one.
2444 *
2445 * Parameters:
2446 * - 1: a term of bag sort
2447 *
2448 * Create with:
2449 * - `Solver::mkTerm(Kind kind, const Term& child) const`
2450 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
2451 */
2452 DUPLICATE_REMOVAL,
2453 /**
2454 * The bag of the single element given as a parameter.
2455 *
2456 * Parameters:
2457 * - 1: Single element
2458 *
2459 * Create with:
2460 * - `Solver::mkTerm(Kind kind, const Term& child) const`
2461 */
2462 MK_BAG,
2463 /**
2464 * Bag cardinality.
2465 *
2466 * Parameters:
2467 * - 1: Bag to determine the cardinality of
2468 *
2469 * Create with:
2470 * - `Solver::mkTerm(Kind kind, const Term& child) const`
2471 */
2472 BAG_CARD,
2473 /**
2474 * Returns an element from a given bag.
2475 * If a bag A = {(x,n)} where n is the multiplicity, then the term (choose A)
2476 * is equivalent to the term x.
2477 * If the bag is empty, then (choose A) is an arbitrary value.
2478 * If the bag contains distinct elements, then (choose A) will
2479 * deterministically return an element in A.
2480 *
2481 * Parameters:
2482 * - 1: Term of bag sort
2483 *
2484 * Create with:
2485 * - `Solver::mkTerm(Kind kind, const Term& child) const`
2486 */
2487 BAG_CHOOSE,
2488 /**
2489 * Bag is_singleton predicate (single element with multiplicity exactly one).
2490 * Parameters:
2491 * - 1: Term of bag sort, is [1] a singleton bag?
2492 *
2493 * Create with:
2494 * - `Solver::mkTerm(Kind kind, const Term& child) const`
2495 */
2496 BAG_IS_SINGLETON,
2497 /**
2498 * Bag.from_set converts a set to a bag.
2499 *
2500 * Parameters:
2501 * - 1: Term of set sort
2502 *
2503 * Create with:
2504 * - `Solver::mkTerm(Kind kind, const Term& child) const`
2505 */
2506 BAG_FROM_SET,
2507 /**
2508 * Bag.to_set converts a bag to a set.
2509 *
2510 * Parameters:
2511 * - 1: Term of bag sort
2512 *
2513 * Create with:
2514 * - `Solver::mkTerm(Kind kind, const Term& child) const`
2515 */
2516 BAG_TO_SET,
2517
2518 /* Strings --------------------------------------------------------------- */
2519
2520 /**
2521 * String concat.
2522 *
2523 * Parameters: n > 1
2524 * - 1..n: Terms of String sort
2525 *
2526 * Create with:
2527 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
2528 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
2529 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
2530 */
2531 STRING_CONCAT,
2532 /**
2533 * String membership.
2534 *
2535 * Parameters:
2536 * - 1: Term of String sort
2537 * - 2: Term of RegExp sort
2538 *
2539 * Create with:
2540 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
2541 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
2542 */
2543 STRING_IN_REGEXP,
2544 /**
2545 * String length.
2546 *
2547 * Parameters:
2548 * - 1: Term of String sort
2549 *
2550 * Create with:
2551 * - `Solver::mkTerm(Kind kind, const Term& child) const`
2552 */
2553 STRING_LENGTH,
2554 /**
2555 * String substring.
2556 * Extracts a substring, starting at index i and of length l, from a string
2557 * s. If the start index is negative, the start index is greater than the
2558 * length of the string, or the length is negative, the result is the empty
2559 * string.
2560 *
2561 * Parameters:
2562 * - 1: Term of sort String
2563 * - 2: Term of sort Integer (index i)
2564 * - 3: Term of sort Integer (length l)
2565 *
2566 * Create with:
2567 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
2568 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
2569 */
2570 STRING_SUBSTR,
2571 /**
2572 * String update.
2573 * Updates a string s by replacing its context starting at an index with t.
2574 * If the start index is negative, the start index is greater than the
2575 * length of the string, the result is s. Otherwise, the length of the
2576 * original string is preserved.
2577 *
2578 * Parameters:
2579 * - 1: Term of sort String
2580 * - 2: Term of sort Integer (index i)
2581 * - 3: Term of sort String (replacement string t)
2582 *
2583 * Create with:
2584 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
2585 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
2586 */
2587 STRING_UPDATE,
2588 /**
2589 * String character at.
2590 * Returns the character at index i from a string s. If the index is negative
2591 * or the index is greater than the length of the string, the result is the
2592 * empty string. Otherwise the result is a string of length 1.
2593 *
2594 * Parameters:
2595 * - 1: Term of sort String (string s)
2596 * - 2: Term of sort Integer (index i)
2597 *
2598 * Create with:
2599 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
2600 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
2601 */
2602 STRING_CHARAT,
2603 /**
2604 * String contains.
2605 * Checks whether a string s1 contains another string s2. If s2 is empty, the
2606 * result is always true.
2607 *
2608 * Parameters:
2609 * - 1: Term of sort String (the string s1)
2610 * - 2: Term of sort String (the string s2)
2611 *
2612 * Create with:
2613 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
2614 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
2615 */
2616 STRING_CONTAINS,
2617 /**
2618 * String index-of.
2619 * Returns the index of a substring s2 in a string s1 starting at index i. If
2620 * the index is negative or greater than the length of string s1 or the
2621 * substring s2 does not appear in string s1 after index i, the result is -1.
2622 *
2623 * Parameters:
2624 * - 1: Term of sort String (substring s1)
2625 * - 2: Term of sort String (substring s2)
2626 * - 3: Term of sort Integer (index i)
2627 *
2628 * Create with:
2629 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
2630 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
2631 */
2632 STRING_INDEXOF,
2633 /**
2634 * String replace.
2635 * Replaces a string s2 in a string s1 with string s3. If s2 does not appear
2636 * in s1, s1 is returned unmodified.
2637 *
2638 * Parameters:
2639 * - 1: Term of sort String (string s1)
2640 * - 2: Term of sort String (string s2)
2641 * - 3: Term of sort String (string s3)
2642 *
2643 * Create with:
2644 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
2645 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
2646 */
2647 STRING_REPLACE,
2648 /**
2649 * String replace all.
2650 * Replaces all occurrences of a string s2 in a string s1 with string s3.
2651 * If s2 does not appear in s1, s1 is returned unmodified.
2652 *
2653 * Parameters:
2654 * - 1: Term of sort String (string s1)
2655 * - 2: Term of sort String (string s2)
2656 * - 3: Term of sort String (string s3)
2657 *
2658 * Create with:
2659 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
2660 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
2661 */
2662 STRING_REPLACE_ALL,
2663 /**
2664 * String replace regular expression match.
2665 * Replaces the first match of a regular expression r in string s1 with
2666 * string s2. If r does not match a substring of s1, s1 is returned
2667 * unmodified.
2668 *
2669 * Parameters:
2670 * - 1: Term of sort String (string s1)
2671 * - 2: Term of sort Regexp (regexp r)
2672 * - 3: Term of sort String (string s2)
2673 *
2674 * Create with:
2675 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
2676 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
2677 */
2678 STRING_REPLACE_RE,
2679 /**
2680 * String replace all regular expression matches.
2681 * Replaces all matches of a regular expression r in string s1 with string
2682 * s2. If r does not match a substring of s1, s1 is returned unmodified.
2683 *
2684 * Parameters:
2685 * - 1: Term of sort String (string s1)
2686 * - 2: Term of sort Regexp (regexp r)
2687 * - 3: Term of sort String (string s2)
2688 *
2689 * Create with:
2690 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
2691 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
2692 */
2693 STRING_REPLACE_RE_ALL,
2694 /**
2695 * String to lower case.
2696 *
2697 * Parameters:
2698 * - 1: Term of String sort
2699 *
2700 * Create with:
2701 * - `Solver::mkTerm(Kind kind, const Term& child) const`
2702 */
2703 STRING_TOLOWER,
2704 /**
2705 * String to upper case.
2706 *
2707 * Parameters:
2708 * - 1: Term of String sort
2709 *
2710 * Create with:
2711 * - `Solver::mkTerm(Kind kind, const Term& child) const`
2712 */
2713 STRING_TOUPPER,
2714 /**
2715 * String reverse.
2716 *
2717 * Parameters:
2718 * - 1: Term of String sort
2719 *
2720 * Create with:
2721 * - `Solver::mkTerm(Kind kind, const Term& child) const`
2722 */
2723 STRING_REV,
2724 /**
2725 * String to code.
2726 * Returns the code point of a string if it has length one, or returns -1
2727 * otherwise.
2728 *
2729 * Parameters:
2730 * - 1: Term of String sort
2731 *
2732 * Create with:
2733 * - `Solver::mkTerm(Kind kind, const Term& child) const`
2734 */
2735 STRING_TO_CODE,
2736 /**
2737 * String from code.
2738 * Returns a string containing a single character whose code point matches
2739 * the argument to this function, or the empty string if the argument is
2740 * out-of-bounds.
2741 *
2742 * Parameters:
2743 * - 1: Term of Integer sort
2744 *
2745 * Create with:
2746 * - `Solver::mkTerm(Kind kind, const Term& child) const`
2747 */
2748 STRING_FROM_CODE,
2749 /**
2750 * String less than.
2751 * Returns true if string s1 is (strictly) less than s2 based on a
2752 * lexiographic ordering over code points.
2753 *
2754 * Parameters:
2755 * - 1: Term of sort String (the string s1)
2756 * - 2: Term of sort String (the string s2)
2757 *
2758 * Create with:
2759 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
2760 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
2761 */
2762 STRING_LT,
2763 /**
2764 * String less than or equal.
2765 * Returns true if string s1 is less than or equal to s2 based on a
2766 * lexiographic ordering over code points.
2767 *
2768 * Parameters:
2769 * - 1: Term of sort String (the string s1)
2770 * - 2: Term of sort String (the string s2)
2771 *
2772 * Create with:
2773 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
2774 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
2775 */
2776 STRING_LEQ,
2777 /**
2778 * String prefix-of.
2779 * Checks whether a string s1 is a prefix of string s2. If string s1 is
2780 * empty, this operator returns true.
2781 *
2782 * Parameters:
2783 * - 1: Term of sort String (string s1)
2784 * - 2: Term of sort String (string s2)
2785 *
2786 * Create with:
2787 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
2788 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
2789 */
2790 STRING_PREFIX,
2791 /**
2792 * String suffix-of.
2793 * Checks whether a string s1 is a suffix of string 2. If string s1 is empty,
2794 * this operator returns true.
2795 *
2796 * Parameters:
2797 * - 1: Term of sort String (string s1)
2798 * - 2: Term of sort String (string s2)
2799 *
2800 * Create with:
2801 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
2802 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
2803 */
2804 STRING_SUFFIX,
2805 /**
2806 * String is-digit.
2807 * Returns true if string s is digit (it is one of "0", ..., "9").
2808 *
2809 * Parameters:
2810 * - 1: Term of sort String
2811 *
2812 * Create with:
2813 * - `Solver::mkTerm(Kind kind, const Term& child1) const`
2814 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
2815 */
2816 STRING_IS_DIGIT,
2817 /**
2818 * Integer to string.
2819 * If the integer is negative this operator returns the empty string.
2820 *
2821 * Parameters:
2822 * - 1: Term of sort Integer
2823 *
2824 * Create with:
2825 * - `Solver::mkTerm(Kind kind, const Term& child) const`
2826 */
2827 STRING_FROM_INT,
2828 /**
2829 * String to integer (total function).
2830 * If the string does not contain an integer or the integer is negative, the
2831 * operator returns -1.
2832 *
2833 * Parameters:
2834 * - 1: Term of sort String
2835 *
2836 * Create with:
2837 * - `Solver::mkTerm(Kind kind, const Term& child) const`
2838 */
2839 STRING_TO_INT,
2840 /**
2841 * Constant string.
2842 *
2843 * Parameters:
2844 * - See @ref cvc5::api::Solver::mkString() "mkString()".
2845 *
2846 * Create with:
2847 * - `Solver::mkString(const std::string& s, bool useEscSequences) const`
2848 * - `Solver::mkString(const unsigned char c) const`
2849 * - `Solver::mkString(const std::vector<uint32_t>& s) const`
2850 */
2851 CONST_STRING,
2852 /**
2853 * Conversion from string to regexp.
2854 *
2855 * Parameters:
2856 * - 1: Term of sort String
2857 *
2858 * Create with:
2859 * - `Solver::mkTerm(Kind kind, const Term& child) const`
2860 */
2861 STRING_TO_REGEXP,
2862 /**
2863 * Regexp Concatenation.
2864 *
2865 * Parameters:
2866 * - 1..2: Terms of Regexp sort
2867 *
2868 * Create with:
2869 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
2870 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
2871 */
2872 REGEXP_CONCAT,
2873 /**
2874 * Regexp union.
2875 *
2876 * Parameters:
2877 * - 1..2: Terms of Regexp sort
2878 *
2879 * Create with:
2880 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
2881 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
2882 */
2883 REGEXP_UNION,
2884 /**
2885 * Regexp intersection.
2886 *
2887 * Parameters:
2888 * - 1..2: Terms of Regexp sort
2889 *
2890 * Create with:
2891 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
2892 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
2893 */
2894 REGEXP_INTER,
2895 /**
2896 * Regexp difference.
2897 *
2898 * Parameters:
2899 * - 1..2: Terms of Regexp sort
2900 *
2901 * Create with:
2902 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
2903 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
2904 */
2905 REGEXP_DIFF,
2906 /**
2907 * Regexp *.
2908 *
2909 * Parameters:
2910 * - 1: Term of sort Regexp
2911 *
2912 * Create with:
2913 * - `Solver::mkTerm(Kind kind, const Term& child) const`
2914 */
2915 REGEXP_STAR,
2916 /**
2917 * Regexp +.
2918 *
2919 * Parameters:
2920 * - 1: Term of sort Regexp
2921 *
2922 * Create with:
2923 * - `Solver::mkTerm(Kind kind, const Term& child) const`
2924 */
2925 REGEXP_PLUS,
2926 /**
2927 * Regexp ?.
2928 *
2929 * Parameters:
2930 * - 1: Term of sort Regexp
2931 *
2932 * Create with:
2933 * - `Solver::mkTerm(Kind kind, const Term& child) const`
2934 */
2935 REGEXP_OPT,
2936 /**
2937 * Regexp range.
2938 *
2939 * Parameters:
2940 * - 1: Lower bound character for the range
2941 * - 2: Upper bound character for the range
2942 *
2943 * Create with:
2944 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
2945 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
2946 */
2947 REGEXP_RANGE,
2948 /**
2949 * Operator for regular expression repeat.
2950 *
2951 * Parameters:
2952 * - 1: The number of repetitions
2953 *
2954 * Create with:
2955 * - `Solver::mkOp(Kind kind, uint32_t param) const`
2956 *
2957 * Apply regular expression loop.
2958 *
2959 * Parameters:
2960 * - 1: Op of kind REGEXP_REPEAT
2961 * - 2: Term of regular expression sort
2962 *
2963 * Create with:
2964 * - `Solver::mkTerm(const Op& op, const Term& child) const`
2965 * - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const`
2966 */
2967 REGEXP_REPEAT,
2968 /**
2969 * Operator for regular expression loop, from lower bound to upper bound
2970 * number of repetitions.
2971 *
2972 * Parameters:
2973 * - 1: The lower bound
2974 * - 2: The upper bound
2975 *
2976 * Create with:
2977 * - `Solver::mkOp(Kind kind, uint32_t param, uint32_t param) const`
2978 *
2979 * Apply regular expression loop.
2980 *
2981 * Parameters:
2982 * - 1: Op of kind REGEXP_LOOP
2983 * - 2: Term of regular expression sort
2984 *
2985 * Create with:
2986 * - `Solver::mkTerm(const Op& op, const Term& child) const`
2987 * - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const`
2988 */
2989 REGEXP_LOOP,
2990 /**
2991 * Regexp empty.
2992 *
2993 * Parameters: none
2994 *
2995 * Create with:
2996 * - `Solver::mkRegexpEmpty() const`
2997 * - `Solver::mkTerm(Kind kind) const`
2998 */
2999 REGEXP_EMPTY,
3000 /**
3001 * Regexp all characters.
3002 *
3003 * Parameters: none
3004 *
3005 * Create with:
3006 * - `Solver::mkRegexpSigma() const`
3007 * - `Solver::mkTerm(Kind kind) const`
3008 */
3009 REGEXP_SIGMA,
3010 /**
3011 * Regexp complement.
3012 *
3013 * Parameters:
3014 * - 1: Term of sort RegExp
3015 *
3016 * Create with:
3017 * - `Solver::mkTerm(Kind kind, const Term& child1) const`
3018 */
3019 REGEXP_COMPLEMENT,
3020
3021 /**
3022 * Sequence concat.
3023 *
3024 * Parameters: n > 1
3025 * - 1..n: Terms of Sequence sort
3026 *
3027 * Create with:
3028 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
3029 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
3030 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
3031 */
3032 SEQ_CONCAT,
3033 /**
3034 * Sequence length.
3035 *
3036 * Parameters:
3037 * - 1: Term of Sequence sort
3038 *
3039 * Create with:
3040 * - `Solver::mkTerm(Kind kind, const Term& child) const`
3041 */
3042 SEQ_LENGTH,
3043 /**
3044 * Sequence extract.
3045 * Extracts a subsequence, starting at index i and of length l, from a
3046 * sequence s. If the start index is negative, the start index is greater
3047 * than the length of the sequence, or the length is negative, the result is
3048 * the empty sequence.
3049 *
3050 * Parameters:
3051 * - 1: Term of sort Sequence
3052 * - 2: Term of sort Integer (index i)
3053 * - 3: Term of sort Integer (length l)
3054 *
3055 * Create with:
3056 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
3057 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
3058 */
3059 SEQ_EXTRACT,
3060 /**
3061 * Sequence update.
3062 * Updates a sequence s by replacing its context starting at an index with t.
3063 * If the start index is negative, the start index is greater than the
3064 * length of the sequence, the result is s. Otherwise, the length of the
3065 * original sequence is preserved.
3066 *
3067 * Parameters:
3068 * - 1: Term of sort Sequence
3069 * - 2: Term of sort Integer (index i)
3070 * - 3: Term of sort Sequence (replacement sequence t)
3071 *
3072 * Create with:
3073 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
3074 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
3075 */
3076 SEQ_UPDATE,
3077 /**
3078 * Sequence element at.
3079 * Returns the element at index i from a sequence s. If the index is negative
3080 * or the index is greater or equal to the length of the sequence, the result
3081 * is the empty sequence. Otherwise the result is a sequence of length 1.
3082 *
3083 * Parameters:
3084 * - 1: Term of sequence sort (string s)
3085 * - 2: Term of sort Integer (index i)
3086 *
3087 * Create with:
3088 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
3089 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
3090 */
3091 SEQ_AT,
3092 /**
3093 * Sequence contains.
3094 * Checks whether a sequence s1 contains another sequence s2. If s2 is empty,
3095 * the result is always true.
3096 *
3097 * Parameters:
3098 * - 1: Term of sort Sequence (the sequence s1)
3099 * - 2: Term of sort Sequence (the sequence s2)
3100 *
3101 * Create with:
3102 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
3103 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
3104 */
3105 SEQ_CONTAINS,
3106 /**
3107 * Sequence index-of.
3108 * Returns the index of a subsequence s2 in a sequence s1 starting at index i.
3109 * If the index is negative or greater than the length of sequence s1 or the
3110 * subsequence s2 does not appear in sequence s1 after index i, the result is
3111 * -1.
3112 *
3113 * Parameters:
3114 * - 1: Term of sort Sequence (subsequence s1)
3115 * - 2: Term of sort Sequence (subsequence s2)
3116 * - 3: Term of sort Integer (index i)
3117 *
3118 * Create with:
3119 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
3120 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
3121 */
3122 SEQ_INDEXOF,
3123 /**
3124 * Sequence replace.
3125 * Replaces the first occurrence of a sequence s2 in a sequence s1 with
3126 * sequence s3. If s2 does not appear in s1, s1 is returned unmodified.
3127 *
3128 * Parameters:
3129 * - 1: Term of sort Sequence (sequence s1)
3130 * - 2: Term of sort Sequence (sequence s2)
3131 * - 3: Term of sort Sequence (sequence s3)
3132 *
3133 * Create with:
3134 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
3135 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
3136 */
3137 SEQ_REPLACE,
3138 /**
3139 * Sequence replace all.
3140 * Replaces all occurrences of a sequence s2 in a sequence s1 with sequence
3141 * s3. If s2 does not appear in s1, s1 is returned unmodified.
3142 *
3143 * Parameters:
3144 * - 1: Term of sort Sequence (sequence s1)
3145 * - 2: Term of sort Sequence (sequence s2)
3146 * - 3: Term of sort Sequence (sequence s3)
3147 *
3148 * Create with:
3149 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
3150 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
3151 */
3152 SEQ_REPLACE_ALL,
3153 /**
3154 * Sequence reverse.
3155 *
3156 * Parameters:
3157 * - 1: Term of Sequence sort
3158 *
3159 * Create with:
3160 * - `Solver::mkTerm(Kind kind, const Term& child) const`
3161 */
3162 SEQ_REV,
3163 /**
3164 * Sequence prefix-of.
3165 * Checks whether a sequence s1 is a prefix of sequence s2. If sequence s1 is
3166 * empty, this operator returns true.
3167 *
3168 * Parameters:
3169 * - 1: Term of sort Sequence (sequence s1)
3170 * - 2: Term of sort Sequence (sequence s2)
3171 *
3172 * Create with:
3173 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
3174 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
3175 */
3176 SEQ_PREFIX,
3177 /**
3178 * Sequence suffix-of.
3179 * Checks whether a sequence s1 is a suffix of sequence s2. If sequence s1 is
3180 * empty, this operator returns true.
3181 *
3182 * Parameters:
3183 * - 1: Term of sort Sequence (sequence s1)
3184 * - 2: Term of sort Sequence (sequence s2)
3185 *
3186 * Create with:
3187 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
3188 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
3189 */
3190 SEQ_SUFFIX,
3191 /**
3192 * Constant sequence.
3193 *
3194 * Parameters:
3195 * - See @ref cvc5::api::Solver::mkEmptySequence() "mkEmptySequence()".
3196 *
3197 * Create with:
3198 * - `Solver::mkEmptySequence(const Sort& sort) const`
3199 *
3200 * Note that a constant sequence is a term that is equivalent to:
3201 *
3202 * (seq.++ (seq.unit c1) ... (seq.unit cn))
3203 *
3204 * where n>=0 and c1, ..., cn are constants of some sort. The elements
3205 * can be extracted by `Term::getSequenceValue()`.
3206 */
3207 CONST_SEQUENCE,
3208 /**
3209 * Sequence unit, corresponding to a sequence of length one with the given
3210 * term.
3211 *
3212 * Parameters:
3213 * - 1: Element term.
3214 *
3215 * Create with:
3216 * - `Solver::mkTerm(Kind kind, const Term& child1) const`
3217 */
3218 SEQ_UNIT,
3219 /**
3220 * Sequence nth, corresponding to the nth element of a sequence.
3221 *
3222 * Parameters:
3223 * - 1: Sequence term.
3224 * - 2: Integer term.
3225 *
3226 * Create with:
3227 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
3228 */
3229 SEQ_NTH,
3230
3231 /* Quantifiers ----------------------------------------------------------- */
3232
3233 /**
3234 * Universally quantified formula.
3235 *
3236 * Parameters:
3237 * - 1: BOUND_VAR_LIST Term
3238 * - 2: Quantifier body
3239 * - 3: (optional) INST_PATTERN_LIST Term
3240 *
3241 * Create with:
3242 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
3243 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
3244 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
3245 */
3246 FORALL,
3247 /**
3248 * Existentially quantified formula.
3249 *
3250 * Parameters:
3251 * - 1: BOUND_VAR_LIST Term
3252 * - 2: Quantifier body
3253 * - 3: (optional) INST_PATTERN_LIST Term
3254 *
3255 * Create with:
3256 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
3257 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
3258 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
3259 */
3260 EXISTS,
3261 /**
3262 * A list of bound variables (used to bind variables under a quantifier)
3263 *
3264 * Parameters: n > 1
3265 * - 1..n: Terms with kind BOUND_VARIABLE
3266 *
3267 * Create with:
3268 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
3269 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
3270 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
3271 */
3272 BOUND_VAR_LIST,
3273 /**
3274 * An instantiation pattern.
3275 * Specifies a (list of) terms to be used as a pattern for quantifier
3276 * instantiation.
3277 *
3278 * Parameters: n > 1
3279 * - 1..n: Terms with kind BOUND_VARIABLE
3280 *
3281 * Create with:
3282 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
3283 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
3284 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
3285 */
3286 INST_PATTERN,
3287 /**
3288 * An instantiation no-pattern.
3289 * Specifies a (list of) terms that should not be used as a pattern for
3290 * quantifier instantiation.
3291 *
3292 * Parameters: n > 1
3293 * - 1..n: Terms with kind BOUND_VARIABLE
3294 *
3295 * Create with:
3296 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
3297 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
3298 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
3299 */
3300 INST_NO_PATTERN,
3301 /*
3302 * An instantiation pool.
3303 * Specifies an annotation for pool based instantiation.
3304 * Parameters: n > 1
3305 * - 1..n: Terms that comprise the pools, which are one-to-one with
3306 * the variables of the quantified formula to be instantiated.
3307 * Create with:
3308 * - `mkTerm(Kind kind, Term child1, Term child2)
3309 * - `mkTerm(Kind kind, Term child1, Term child2, Term child3)
3310 * - `mkTerm(Kind kind, const std::vector<Term>& children)
3311 */
3312 INST_POOL,
3313 /*
3314 * A instantantiation-add-to-pool annotation.
3315 * Parameters: n = 1
3316 * - 1: The pool to add to.
3317 * Create with:
3318 * - `mkTerm(Kind kind, Term child)
3319 */
3320 INST_ADD_TO_POOL,
3321 /*
3322 * A skolemization-add-to-pool annotation.
3323 * Parameters: n = 1
3324 * - 1: The pool to add to.
3325 * Create with:
3326 * - `mkTerm(Kind kind, Term child)
3327 */
3328 SKOLEM_ADD_TO_POOL,
3329 /**
3330 * An instantiation attribute
3331 * Specifies a custom property for a quantified formula given by a
3332 * term that is ascribed a user attribute.
3333 *
3334 * Parameters:
3335 * - 1: Term with a user attribute.
3336 *
3337 * Create with:
3338 * - `Solver::mkTerm(Kind kind, const Term& child) const`
3339 */
3340 INST_ATTRIBUTE,
3341 /**
3342 * A list of instantiation patterns and/or attributes.
3343 *
3344 * Parameters: n > 1
3345 * - 1..n: Terms with kind INST_PATTERN, INST_NO_PATTERN, or
3346 * INST_ATTRIBUTE.
3347 *
3348 * Create with:
3349 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
3350 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
3351 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
3352 */
3353 INST_PATTERN_LIST,
3354 #if 0
3355
3356 /* Sort Kinds ------------------------------------------------------------ */
3357
3358 /* array type */
3359 ARRAY_TYPE,
3360 /* a type parameter for type ascription */
3361 ASCRIPTION_TYPE,
3362 /* constructor */
3363 CONSTRUCTOR_TYPE,
3364 /* a datatype type index */
3365 DATATYPE_TYPE,
3366 /* selector */
3367 SELECTOR_TYPE,
3368 /* set type, takes as parameter the type of the elements */
3369 SET_TYPE,
3370 /* bag type, takes as parameter the type of the elements */
3371 BAG_TYPE,
3372 /* sort tag */
3373 SORT_TAG,
3374 /* specifies types of user-declared 'uninterpreted' sorts */
3375 SORT_TYPE,
3376 /* tester */
3377 TESTER_TYPE,
3378 /* a representation for basic types */
3379 TYPE_CONSTANT,
3380 /* a function type */
3381 FUNCTION_TYPE,
3382 /* the type of a symbolic expression */
3383 SEXPR_TYPE,
3384 /* bit-vector type */
3385 BITVECTOR_TYPE,
3386 /* floating-point type */
3387 FLOATINGPOINT_TYPE,
3388 #endif
3389
3390 /* ----------------------------------------------------------------------- */
3391 /** Marks the upper-bound of this enumeration. */
3392 LAST_KIND
3393 };
3394 // clang-format on
3395
3396 /**
3397 * Get the string representation of a given kind.
3398 * @param k the kind
3399 * @return the string representation of kind k
3400 */
3401 std::string kindToString(Kind k) CVC5_EXPORT;
3402
3403 /**
3404 * Serialize a kind to given stream.
3405 * @param out the output stream
3406 * @param k the kind to be serialized to the given output stream
3407 * @return the output stream
3408 */
3409 std::ostream& operator<<(std::ostream& out, Kind k) CVC5_EXPORT;
3410
3411 } // namespace api
3412 } // namespace cvc5
3413
3414 namespace std {
3415
3416 /**
3417 * Hash function for Kinds.
3418 */
3419 template<>
3420 struct CVC5_EXPORT hash<cvc5::api::Kind>
3421 {
3422 /**
3423 * Hashes a Kind to a size_t.
3424 */
3425 size_t operator()(cvc5::api::Kind k) const;
3426 };
3427
3428 }
3429
3430 #endif