projects / cvc5.git / blob
? search:
summary | shortlog | log | commit | commitdiff | tree
history | raw | HEAD
docs: Fix `Kind` description (#6712)
[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 * \internal
37 *
38 * Note that the API type `cvc5::api::Kind` roughly corresponds to
39 * `cvc5::Kind`, but is a different type. It hides internal kinds that should
40 * not be exported to the API, and maps all kinds that we want to export to its
41 * corresponding internal kinds. The underlying type of `cvc5::api::Kind` must
42 * be signed (to enable range checks for validity). The size of this type
43 * depends on the size of `cvc5::Kind` (`NodeValue::NBITS_KIND`, currently 10
44 * bits, see expr/node_value.h).
45 */
46 enum CVC5_EXPORT Kind : int32_t
47 {
48 /**
49 * Internal kind.
50 * Should never be exposed or created via the API.
51 */
52 INTERNAL_KIND = -2,
53 /**
54 * Undefined kind.
55 * Should never be exposed or created via the API.
56 */
57 UNDEFINED_KIND = -1,
58 /**
59 * Null kind (kind of null term `Term::Term()`).
60 * Do not explicitly create via API functions other than `Term::Term()`.
61 */
62 NULL_EXPR,
63
64 /* Builtin --------------------------------------------------------------- */
65
66 /**
67 * Uninterpreted constant.
68 *
69 * Parameters:
70 * - 1: Sort of the constant
71 * - 2: Index of the constant
72 *
73 * Create with:
74 * - `Solver::mkUninterpretedConst(const Sort& sort, int32_t index) const`
75 */
76 UNINTERPRETED_CONSTANT,
77 /**
78 * Abstract value (other than uninterpreted sort constants).
79 *
80 * Parameters:
81 * - 1: Index of the abstract value
82 *
83 * Create with:
84 * - `Solver::mkAbstractValue(const std::string& index) const`
85 * - `Solver::mkAbstractValue(uint64_t index) const`
86 */
87 ABSTRACT_VALUE,
88 #if 0
89 /* Built-in operator */
90 BUILTIN,
91 #endif
92 /**
93 * Equality, chainable.
94 *
95 * Parameters: n > 1
96 * - 1..n: Terms with same sorts
97 *
98 * Create with:
99 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
100 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
101 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
102 */
103 EQUAL,
104 /**
105 * Disequality.
106 *
107 * Parameters: n > 1
108 * - 1..n: Terms with same sorts
109 *
110 * Create with:
111 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
112 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
113 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
114 */
115 DISTINCT,
116 /**
117 * First-order constant.
118 *
119 * Not permitted in bindings (forall, exists, ...).
120 *
121 * Parameters:
122 * - See @ref cvc5::api::Solver::mkConst() "mkConst()".
123 *
124 * Create with:
125 * - `Solver::mkConst(const Sort& sort, const std::string& symbol) const`
126 * - `Solver::mkConst(const Sort& sort) const`
127 */
128 CONSTANT,
129 /**
130 * (Bound) variable.
131 *
132 * Permitted in bindings and in the lambda and quantifier bodies only.
133 *
134 * Parameters:
135 * - See @ref cvc5::api::Solver::mkVar() "mkVar()".
136 *
137 * Create with:
138 * - `Solver::mkVar(const Sort& sort, const std::string& symbol) const`
139 */
140 VARIABLE,
141 #if 0
142 /* Skolem variable (internal only) */
143 SKOLEM,
144 #endif
145 /**
146 * Symbolic expression.
147 *
148 * Parameters: n > 0
149 * - 1..n: terms
150 *
151 * Create with:
152 * - `Solver::mkTerm(Kind kind, const Term& child) const`
153 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
154 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
155 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
156 */
157 SEXPR,
158 /**
159 * Lambda expression.
160 *
161 * Parameters:
162 * - 1: BOUND_VAR_LIST
163 * - 2: Lambda body
164 *
165 * Create with:
166 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
167 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
168 */
169 LAMBDA,
170 /**
171 * The syntax of a witness term is similar to a quantified formula except that
172 * only one bound variable is allowed.
173 * The term `(witness ((x T)) F)` returns an element `x` of type `T`
174 * and asserts `F`.
175 *
176 * The witness operator behaves like the description operator
177 * (see https://planetmath.org/hilbertsvarepsilonoperator) if there is no x
178 * that satisfies F. But if such x exists, the witness operator does not
179 * enforce the axiom that ensures uniqueness up to logical equivalence:
180 *
181 * @f[
182 * \forall x. F \equiv G \Rightarrow witness~x. F = witness~x. G
183 * @f]
184 *
185 * For example if there are 2 elements of type T that satisfy F, then the
186 * following formula is satisfiable:
187 *
188 * (distinct
189 * (witness ((x Int)) F)
190 * (witness ((x Int)) F))
191 *
192 * This kind is primarily used internally, but may be returned in models
193 * (e.g. for arithmetic terms in non-linear queries). However, it is not
194 * supported by the parser. Moreover, the user of the API should be cautious
195 * when using this operator. In general, all witness terms
196 * `(witness ((x Int)) F)` should be such that `(exists ((x Int)) F)` is a
197 * valid formula. If this is not the case, then the semantics in formulas that
198 * use witness terms may be unintuitive. For example, the following formula is
199 * unsatisfiable:
200 * `(or (= (witness ((x Int)) false) 0) (not (= (witness ((x Int)) false) 0))`
201 * whereas notice that `(or (= z 0) (not (= z 0)))` is true for any `z`.
202 *
203 * Parameters:
204 * - 1: BOUND_VAR_LIST
205 * - 2: Witness body
206 *
207 * Create with:
208 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
209 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
210 */
211 WITNESS,
212
213 /* Boolean --------------------------------------------------------------- */
214
215 /**
216 * Boolean constant.
217 *
218 * Parameters:
219 * - 1: Boolean value of the constant
220 *
221 * Create with:
222 * - `Solver::mkTrue() const`
223 * - `Solver::mkFalse() const`
224 * - `Solver::mkBoolean(bool val) const`
225 */
226 CONST_BOOLEAN,
227 /**
228 * Logical negation.
229 *
230 * Parameters:
231 * - 1: Boolean Term to negate
232 *
233 * Create with:
234 * - `Solver::mkTerm(Kind kind, const Term& child) const`
235 */
236 NOT,
237 /**
238 * Logical conjunction.
239 *
240 * Parameters: n > 1
241 * - 1..n: Boolean Term of the conjunction
242 *
243 * Create with:
244 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
245 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
246 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
247 */
248 AND,
249 /**
250 * Logical implication.
251 *
252 * Parameters: n > 1
253 * - 1..n: Boolean Terms, right associative
254 *
255 * Create with:
256 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
257 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
258 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
259 */
260 IMPLIES,
261 /**
262 * Logical disjunction.
263 *
264 * Parameters: n > 1
265 * - 1..n: Boolean Term of the disjunction
266 *
267 * Create with:
268 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
269 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
270 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
271 */
272 OR,
273 /**
274 * Logical exclusive disjunction, left associative.
275 *
276 * Parameters: n > 1
277 * - 1..n: Boolean Terms, `[1] xor ... xor [n]`
278 *
279 * Create with:
280 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
281 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
282 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
283 */
284 XOR,
285 /**
286 * If-then-else.
287 *
288 * Parameters:
289 * - 1: is a Boolean condition Term
290 * - 2: the 'then' Term
291 * - 3: the 'else' Term
292 *
293 * 'then' and 'else' term must have same base sort.
294 *
295 * Create with:
296 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
297 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
298 */
299 ITE,
300
301 /* UF -------------------------------------------------------------------- */
302
303 /**
304 * Application of an uninterpreted function.
305 *
306 * Parameters: n > 1
307 * - 1: Function Term
308 * - 2..n: Function argument instantiation Terms
309 *
310 * Create with:
311 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
312 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
313 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
314 */
315 APPLY_UF,
316 #if 0
317 /* Boolean term variable */
318 BOOLEAN_TERM_VARIABLE,
319 #endif
320 /**
321 * Cardinality constraint on uninterpreted sort S.
322 * Interpreted as a predicate that is true when the cardinality of S
323 * is less than or equal to the value of the second argument.
324 *
325 * Parameters:
326 * - 1: Term of sort S
327 * - 2: Positive integer constant that bounds the cardinality of sort S
328 *
329 * Create with:
330 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
331 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
332 */
333 CARDINALITY_CONSTRAINT,
334 /**
335 * Cardinality value for uninterpreted sort S.
336 * An operator that returns an integer indicating the value of the cardinality
337 * of sort S.
338 *
339 * Parameters:
340 * - 1: Term of sort S
341 *
342 * Create with:
343 * - `Solver::mkTerm(Kind kind, const Term& child1) const`
344 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
345 */
346 CARDINALITY_VALUE,
347 #if 0
348 /* Combined cardinality constraint. */
349 COMBINED_CARDINALITY_CONSTRAINT,
350 /* Partial uninterpreted function application. */
351 PARTIAL_APPLY_UF,
352 #endif
353 /**
354 * Higher-order applicative encoding of function application, left
355 * associative.
356 *
357 * Parameters: n > 1
358 * - 1: Function to apply
359 * - 2..n: Arguments of the function
360 *
361 * Create with:
362 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
363 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
364 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
365 */
366 HO_APPLY,
367
368 /* Arithmetic ------------------------------------------------------------ */
369
370 /**
371 * Arithmetic addition.
372 *
373 * Parameters: n > 1
374 * - 1..n: Terms of sort Integer, Real (sorts must match)
375 *
376 * Create with:
377 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
378 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
379 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
380 */
381 PLUS,
382 /**
383 * Arithmetic multiplication.
384 *
385 * Parameters: n > 1
386 * - 1..n: Terms of sort Integer, Real (sorts must match)
387 *
388 * Create with:
389 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
390 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
391 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
392 */
393 MULT,
394 /**
395 * Operator for Integer AND
396 *
397 * Parameters:
398 * - 1: Size of the bit-vector that determines the semantics of the IAND
399 *
400 * Create with:
401 * - `Solver::mkOp(Kind kind, uint32_t param) const`
402 *
403 * Apply integer conversion to bit-vector.
404
405 * Parameters:
406 * - 1: Op of kind IAND
407 * - 2: Integer term
408 * - 3: Integer term
409 *
410 * Create with:
411 * - `Solver::mkTerm(const Op& op, const Term& child1, const Term& child2) const`
412 * - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const`
413 */
414 IAND,
415 #if 0
416 /* Synonym for MULT. */
417 NONLINEAR_MULT,
418 #endif
419 /**
420 * Arithmetic subtraction, left associative.
421 *
422 * Parameters:
423 * - 1..n: Terms of sort Integer, Real (sorts must match)
424 *
425 * Create with:
426 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
427 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
428 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
429 */
430 MINUS,
431 /**
432 * Arithmetic negation.
433 *
434 * Parameters:
435 * - 1: Term of sort Integer, Real
436 *
437 * Create with:
438 * - `Solver::mkTerm(Kind kind, const Term& child) const`
439 */
440 UMINUS,
441 /**
442 * Real division, division by 0 undefined, left associative.
443 *
444 * Parameters: n > 1
445 * - 1..n: Terms of sort Integer, Real
446 *
447 * Create with:
448 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
449 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
450 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
451 */
452 DIVISION,
453 /**
454 * Integer division, division by 0 undefined, left associative.
455 *
456 * Parameters: n > 1
457 * - 1..n: Terms of sort Integer
458 *
459 * Create with:
460 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
461 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
462 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
463 */
464 INTS_DIVISION,
465 /**
466 * Integer modulus, division by 0 undefined.
467 *
468 * Parameters:
469 * - 1: Term of sort Integer
470 * - 2: Term of sort Integer
471 *
472 * Create with:
473 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
474 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
475 */
476 INTS_MODULUS,
477 /**
478 * Absolute value.
479 *
480 * Parameters:
481 * - 1: Term of sort Integer
482 *
483 * Create with:
484 * - `Solver::mkTerm(Kind kind, const Term& child) const`
485 */
486 ABS,
487 /**
488 * Arithmetic power.
489 *
490 * Parameters:
491 * - 1: Term of sort Integer, Real
492 * - 2: Term of sort Integer, Real
493 *
494 * Create with:
495 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
496 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
497 */
498 POW,
499 /**
500 * Exponential function.
501 *
502 * Parameters:
503 * - 1: Term of sort Integer, Real
504 *
505 * Create with:
506 * - `Solver::mkTerm(Kind kind, const Term& child) const`
507 */
508 EXPONENTIAL,
509 /**
510 * Sine function.
511 *
512 * Parameters:
513 * - 1: Term of sort Integer, Real
514 *
515 * Create with:
516 * - `Solver::mkTerm(Kind kind, const Term& child) const`
517 */
518 SINE,
519 /**
520 * Cosine function.
521 *
522 * Parameters:
523 * - 1: Term of sort Integer, Real
524 *
525 * Create with:
526 * - `Solver::mkTerm(Kind kind, const Term& child) const`
527 */
528 COSINE,
529 /**
530 * Tangent function.
531 *
532 * Parameters:
533 * - 1: Term of sort Integer, Real
534 *
535 * Create with:
536 * - `Solver::mkTerm(Kind kind, const Term& child) const`
537 */
538 TANGENT,
539 /**
540 * Cosecant function.
541 *
542 * Parameters:
543 * - 1: Term of sort Integer, Real
544 *
545 * Create with:
546 * - `Solver::mkTerm(Kind kind, const Term& child) const`
547 */
548 COSECANT,
549 /**
550 * Secant function.
551 *
552 * Parameters:
553 * - 1: Term of sort Integer, Real
554 *
555 * Create with:
556 * - `Solver::mkTerm(Kind kind, const Term& child) const`
557 */
558 SECANT,
559 /**
560 * Cotangent function.
561 *
562 * Parameters:
563 * - 1: Term of sort Integer, Real
564 *
565 * Create with:
566 * - `Solver::mkTerm(Kind kind, const Term& child) const`
567 */
568 COTANGENT,
569 /**
570 * Arc sine function.
571 *
572 * Parameters:
573 * - 1: Term of sort Integer, Real
574 *
575 * Create with:
576 * - `Solver::mkTerm(Kind kind, const Term& child) const`
577 */
578 ARCSINE,
579 /**
580 * Arc cosine function.
581 *
582 * Parameters:
583 * - 1: Term of sort Integer, Real
584 *
585 * Create with:
586 * - `Solver::mkTerm(Kind kind, const Term& child) const`
587 */
588 ARCCOSINE,
589 /**
590 * Arc tangent function.
591 *
592 * Parameters:
593 * - 1: Term of sort Integer, Real
594 *
595 * Create with:
596 * - `Solver::mkTerm(Kind kind, const Term& child) const`
597 */
598 ARCTANGENT,
599 /**
600 * Arc cosecant function.
601 *
602 * Parameters:
603 * - 1: Term of sort Integer, Real
604 *
605 * Create with:
606 * - `Solver::mkTerm(Kind kind, const Term& child) const`
607 */
608 ARCCOSECANT,
609 /**
610 * Arc secant function.
611 *
612 * Parameters:
613 * - 1: Term of sort Integer, Real
614 *
615 * Create with:
616 * - `Solver::mkTerm(Kind kind, const Term& child) const`
617 */
618 ARCSECANT,
619 /**
620 * Arc cotangent function.
621 *
622 * Parameters:
623 * - 1: Term of sort Integer, Real
624 *
625 * Create with:
626 * - `Solver::mkTerm(Kind kind, const Term& child) const`
627 */
628 ARCCOTANGENT,
629 /**
630 * Square root.
631 *
632 * Parameters:
633 * - 1: Term of sort Integer, Real
634 *
635 * Create with:
636 * - `Solver::mkTerm(Kind kind, const Term& child) const`
637 */
638 SQRT,
639 /**
640 * Operator for the divisibility-by-k predicate.
641 *
642 * Parameter:
643 * - 1: The k to divide by (sort Integer)
644 *
645 * Create with:
646 * - `Solver::mkOp(Kind kind, uint32_t param) const`
647 *
648 * Apply divisibility-by-k predicate.
649 *
650 * Parameters:
651 * - 1: Op of kind DIVISIBLE
652 * - 2: Integer Term
653 *
654 * Create with:
655 * - `Solver::mkTerm(const Op& op, const Term& child1, const Term& child2) const`
656 * - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const`
657 */
658 DIVISIBLE,
659 /**
660 * Multiple-precision rational constant.
661 *
662 * Parameters:
663 * See @ref cvc5::api::Solver::mkInteger() "mkInteger()", @ref cvc5::api::Solver::mkReal() "mkReal()".
664 *
665 * Create with:
666 * - `Solver::mkInteger(const std::string& s) const`
667 * - `Solver::mkInteger(int64_t val) const`
668 * - `Solver::mkReal(const std::string& s) const`
669 * - `Solver::mkReal(int64_t val) const`
670 * - `Solver::mkReal(int64_t num, int64_t den) const`
671 */
672 CONST_RATIONAL,
673 /**
674 * Less than, chainable.
675 *
676 * Parameters: n
677 * - 1..n: Terms of sort Integer, Real; [1] < ... < [n]
678 *
679 * Create with:
680 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
681 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
682 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
683 */
684 LT,
685 /**
686 * Less than or equal, chainable.
687 *
688 * Parameters: n > 1
689 * - 1..n: Terms of sort Integer, Real; [1] <= ... <= [n]
690 *
691 * Create with:
692 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
693 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
694 */
695 LEQ,
696 /**
697 * Greater than, chainable.
698 *
699 * Parameters: n > 1
700 * - 1..n: Terms of sort Integer, Real, [1] > ... > [n]
701 *
702 * Create with:
703 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
704 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
705 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
706 */
707 GT,
708 /**
709 * Greater than or equal, chainable.
710 *
711 * Parameters: n > 1
712 * - 1..n: Terms of sort Integer, Real; [1] >= ... >= [n]
713 *
714 * Create with:
715 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
716 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
717 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
718 */
719 GEQ,
720 /**
721 * Is-integer predicate.
722 *
723 * Parameters:
724 * - 1: Term of sort Integer, Real
725 *
726 * Create with:
727 * - `Solver::mkTerm(Kind kind, const Term& child) const`
728 */
729 IS_INTEGER,
730 /**
731 * Convert Term to Integer by the floor function.
732 *
733 * Parameters:
734 * - 1: Term of sort Integer, Real
735 *
736 * Create with:
737 * - `Solver::mkTerm(Kind kind, const Term& child) const`
738 */
739 TO_INTEGER,
740 /**
741 * Convert Term to Real.
742 *
743 * Parameters:
744 *
745 * - 1: Term of sort Integer, Real
746 *
747 * This is a no-op in cvc5, as Integer is a subtype of Real.
748 */
749 TO_REAL,
750 /**
751 * Pi constant.
752 *
753 * Create with:
754 * - `Solver::mkPi() const`
755 * - `Solver::mkTerm(Kind kind) const`
756 */
757 PI,
758
759 /* BV -------------------------------------------------------------------- */
760
761 /**
762 * Fixed-size bit-vector constant.
763 *
764 * Parameters:
765 * See @ref cvc5::api::Solver::mkBitVector() "mkBitVector()".
766 *
767 * Create with:
768 * - `Solver::mkBitVector(uint32_t size, uint64_t val) const`
769 * - `Solver::mkBitVector(const std::string& s, uint32_t base) const`
770 * - `Solver::mkBitVector(uint32_t size, const std::string& s, uint32_t base) const`
771 */
772 CONST_BITVECTOR,
773 /**
774 * Concatenation of two or more bit-vectors.
775 *
776 * Parameters: n > 1
777 * - 1..n: Terms of bit-vector sort
778 *
779 * Create with:
780 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
781 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
782 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
783 */
784 BITVECTOR_CONCAT,
785 /**
786 * Bit-wise and.
787 *
788 * Parameters: n > 1
789 * - 1..n: Terms of bit-vector sort (sorts must match)
790 *
791 * Create with:
792 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
793 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
794 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
795 */
796 BITVECTOR_AND,
797 /**
798 * Bit-wise or.
799 *
800 * Parameters: n > 1
801 * - 1..n: Terms of bit-vector sort (sorts must match)
802 *
803 * Create with:
804 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
805 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
806 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
807 */
808 BITVECTOR_OR,
809 /**
810 * Bit-wise xor.
811 *
812 * Parameters: n > 1
813 * - 1..n: Terms of bit-vector sort (sorts must match)
814 *
815 * Create with:
816 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
817 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
818 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
819 */
820 BITVECTOR_XOR,
821 /**
822 * Bit-wise negation.
823 *
824 * Parameters:
825 * - 1: Term of bit-vector sort
826 *
827 * Create with:
828 * - `Solver::mkTerm(Kind kind, const Term& child) const`
829 */
830 BITVECTOR_NOT,
831 /**
832 * Bit-wise nand.
833 *
834 * Parameters:
835 * - 1..2: Terms of bit-vector sort (sorts must match)
836 *
837 * Create with:
838 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
839 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
840 */
841 BITVECTOR_NAND,
842 /**
843 * Bit-wise nor.
844 *
845 * Parameters:
846 * - 1..2: Terms of bit-vector sort (sorts must match)
847 *
848 * Create with:
849 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
850 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
851 */
852 BITVECTOR_NOR,
853 /**
854 * Bit-wise xnor, left associative.
855 *
856 * Parameters: n > 1
857 * - 1..n: Terms of bit-vector sort (sorts must match)
858 *
859 * Create with:
860 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
861 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
862 */
863 BITVECTOR_XNOR,
864 /**
865 * Equality comparison (returns bit-vector of size 1).
866 *
867 * Parameters:
868 * - 1..2: Terms of bit-vector sort (sorts must match)
869 *
870 * Create with:
871 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
872 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
873 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
874 */
875 BITVECTOR_COMP,
876 /**
877 * Multiplication of two or more bit-vectors.
878 *
879 * Parameters: n > 1
880 * - 1..n: Terms of bit-vector sort (sorts must match)
881 *
882 * Create with:
883 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
884 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
885 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
886 */
887 BITVECTOR_MULT,
888 /**
889 * Addition of two or more bit-vectors.
890 *
891 * Parameters: n > 1
892 * - 1..n: Terms of bit-vector sort (sorts must match)
893 *
894 * Create with:
895 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
896 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
897 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
898 */
899 BITVECTOR_ADD,
900 /**
901 * Subtraction of two bit-vectors.
902 *
903 * Parameters:
904 * - 1..2: Terms of bit-vector sort (sorts must match)
905 *
906 * Create with:
907 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
908 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
909 */
910 BITVECTOR_SUB,
911 /**
912 * Negation of a bit-vector (two's complement).
913 *
914 * Parameters:
915 * - 1: Term of bit-vector sort
916 *
917 * Create with:
918 * - `Solver::mkTerm(Kind kind, const Term& child) const`
919 */
920 BITVECTOR_NEG,
921 /**
922 * Unsigned division of two bit-vectors, truncating towards 0. If the divisor
923 * is zero, the result is all ones.
924 *
925 * Parameters:
926 * - 1..2: Terms of bit-vector sort (sorts must match)
927 *
928 * Create with:
929 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
930 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
931 */
932 BITVECTOR_UDIV,
933 /**
934 * Unsigned remainder from truncating division of two bit-vectors. If the
935 * modulus is zero, the result is the dividend.
936 *
937 * Parameters:
938 * - 1..2: Terms of bit-vector sort (sorts must match)
939 *
940 * Create with:
941 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
942 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
943 */
944 BITVECTOR_UREM,
945 /**
946 * Two's complement signed division of two bit-vectors. If the divisor is
947 * zero and the dividend is positive, the result is all ones. If the divisor
948 * is zero and the dividend is negative, the result is one.
949 *
950 * Parameters:
951 * - 1..2: Terms of bit-vector sort (sorts must match)
952 *
953 * Create with:
954 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
955 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
956 */
957 BITVECTOR_SDIV,
958 /**
959 * Two's complement signed remainder of two bit-vectors (sign follows
960 * dividend). If the modulus is zero, the result is the dividend.
961 *
962 * Parameters:
963 * - 1..2: Terms of bit-vector sort (sorts must match)
964 *
965 * Create with:
966 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
967 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
968 */
969 BITVECTOR_SREM,
970 /**
971 * Two's complement signed remainder (sign follows divisor). If the modulus
972 * is zero, the result is the dividend.
973 *
974 * Parameters:
975 * - 1..2: Terms of bit-vector sort (sorts must match)
976 *
977 * Create with:
978 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
979 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
980 */
981 BITVECTOR_SMOD,
982 /**
983 * Bit-vector shift left.
984 * The two bit-vector parameters must have same width.
985 *
986 * Parameters:
987 * - 1..2: Terms of bit-vector sort (sorts must match)
988 *
989 * Create with:
990 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
991 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
992 */
993 BITVECTOR_SHL,
994 /**
995 * Bit-vector logical shift right.
996 * The two bit-vector parameters must have same width.
997 *
998 * Parameters:
999 * - 1..2: Terms of bit-vector sort (sorts must match)
1000 *
1001 * Create with:
1002 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
1003 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
1004 */
1005 BITVECTOR_LSHR,
1006 /**
1007 * Bit-vector arithmetic shift right.
1008 * The two bit-vector parameters must have same width.
1009 *
1010 * Parameters:
1011 * - 1..2: Terms of bit-vector sort (sorts must match)
1012 *
1013 * Create with:
1014 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
1015 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
1016 */
1017 BITVECTOR_ASHR,
1018 /**
1019 * Bit-vector unsigned less than.
1020 * The two bit-vector parameters must have same width.
1021 *
1022 * Parameters:
1023 * - 1..2: Terms of bit-vector sort (sorts must match)
1024 *
1025 * Create with:
1026 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
1027 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
1028 */
1029 BITVECTOR_ULT,
1030 /**
1031 * Bit-vector unsigned less than or equal.
1032 * The two bit-vector parameters must have same width.
1033 *
1034 * Parameters:
1035 * - 1..2: Terms of bit-vector sort (sorts must match)
1036 *
1037 * Create with:
1038 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
1039 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
1040 */
1041 BITVECTOR_ULE,
1042 /**
1043 * Bit-vector unsigned greater than.
1044 * The two bit-vector parameters must have same width.
1045 *
1046 * Parameters:
1047 * - 1..2: Terms of bit-vector sort (sorts must match)
1048 *
1049 * Create with:
1050 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
1051 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
1052 */
1053 BITVECTOR_UGT,
1054 /**
1055 * Bit-vector unsigned greater than or equal.
1056 * The two bit-vector parameters must have same width.
1057 *
1058 * Parameters:
1059 * - 1..2: Terms of bit-vector sort (sorts must match)
1060 *
1061 * Create with:
1062 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
1063 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
1064 */
1065 BITVECTOR_UGE,
1066 /**
1067 * Bit-vector signed less than.
1068 * The two bit-vector parameters must have same width.
1069 *
1070 * Parameters:
1071 * - 1..2: Terms of bit-vector sort (sorts must match)
1072 *
1073 * Create with:
1074 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
1075 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
1076 */
1077 BITVECTOR_SLT,
1078 /**
1079 * Bit-vector signed less than or equal.
1080 * The two bit-vector parameters must have same width.
1081 *
1082 * Parameters:
1083 * - 1..2: Terms of bit-vector sort (sorts must match)
1084 *
1085 * Create with:
1086 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
1087 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
1088 */
1089 BITVECTOR_SLE,
1090 /**
1091 * Bit-vector signed greater than.
1092 * The two bit-vector parameters must have same width.
1093 *
1094 * Parameters:
1095 * - 1..2: Terms of bit-vector sort (sorts must match)
1096 *
1097 * Create with:
1098 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
1099 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
1100 */
1101 BITVECTOR_SGT,
1102 /**
1103 * Bit-vector signed greater than or equal.
1104 * The two bit-vector parameters must have same width.
1105 *
1106 * Parameters:
1107 * - 1..2: Terms of bit-vector sort (sorts must match)
1108 *
1109 * Create with:
1110 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
1111 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
1112 */
1113 BITVECTOR_SGE,
1114 /**
1115 * Bit-vector unsigned less than, returns bit-vector of size 1.
1116 *
1117 * Parameters:
1118 * - 1..2: Terms of bit-vector sort (sorts must match)
1119 *
1120 * Create with:
1121 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
1122 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
1123 */
1124 BITVECTOR_ULTBV,
1125 /**
1126 * Bit-vector signed less than. returns bit-vector of size 1.
1127 *
1128 * Parameters:
1129 * - 1..2: Terms of bit-vector sort (sorts must match)
1130 *
1131 * Create with:
1132 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
1133 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
1134 */
1135 BITVECTOR_SLTBV,
1136 /**
1137 * Same semantics as regular ITE, but condition is bit-vector of size 1.
1138 *
1139 * Parameters:
1140 * - 1: Term of bit-vector sort of size 1, representing the condition
1141 * - 2: Term reprsenting the 'then' branch
1142 * - 3: Term representing the 'else' branch
1143 *
1144 * 'then' and 'else' term must have same base sort.
1145 *
1146 * Create with:
1147 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
1148 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
1149 */
1150 BITVECTOR_ITE,
1151 /**
1152 * Bit-vector redor.
1153 *
1154 * Parameters:
1155 * - 1: Term of bit-vector sort
1156 *
1157 * Create with:
1158 * - `Solver::mkTerm(Kind kind, const Term& child) const`
1159 */
1160 BITVECTOR_REDOR,
1161 /**
1162 * Bit-vector redand.
1163 *
1164 * Parameters:
1165 * - 1: Term of bit-vector sort
1166 *
1167 * Create with:
1168 * - `Solver::mkTerm(Kind kind, const Term& child) const`
1169 */
1170 BITVECTOR_REDAND,
1171 #if 0
1172 /* formula to be treated as a bv atom via eager bit-blasting
1173 * (internal-only symbol) */
1174 BITVECTOR_EAGER_ATOM,
1175 /* term to be treated as a variable. used for eager bit-blasting Ackermann
1176 * expansion of bvudiv (internal-only symbol) */
1177 BITVECTOR_ACKERMANIZE_UDIV,
1178 /* term to be treated as a variable. used for eager bit-blasting Ackermann
1179 * expansion of bvurem (internal-only symbol) */
1180 BITVECTOR_ACKERMANIZE_UREM,
1181 #endif
1182 /**
1183 * Operator for bit-vector extract (from index 'high' to 'low').
1184 *
1185 * Parameters:
1186 * - 1: The 'high' index
1187 * - 2: The 'low' index
1188 *
1189 * Create with:
1190 * - `Solver::mkOp(Kind kind, uint32_t param, uint32_t param) const`
1191 *
1192 * Apply bit-vector extract.
1193 *
1194 * Parameters:
1195 * - 1: Op of kind BITVECTOR_EXTRACT
1196 * - 2: Term of bit-vector sort
1197 *
1198 * Create with:
1199 * - `Solver::mkTerm(const Op& op, const Term& child) const`
1200 * - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const`
1201 */
1202 BITVECTOR_EXTRACT,
1203 /**
1204 * Operator for bit-vector repeat.
1205 *
1206 * Parameter:
1207 * - 1: Number of times to repeat a given bit-vector
1208 *
1209 * Create with:
1210 * - `Solver::mkOp(Kind kind, uint32_t param) const`.
1211 *
1212 * Apply bit-vector repeat.
1213 *
1214 * Parameters:
1215 * - 1: Op of kind BITVECTOR_REPEAT
1216 * - 2: Term of bit-vector sort
1217 *
1218 * Create with:
1219 * - `Solver::mkTerm(const Op& op, const Term& child) const`
1220 * - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const`
1221 */
1222 BITVECTOR_REPEAT,
1223 /**
1224 * Operator for bit-vector zero-extend.
1225 *
1226 * Parameter:
1227 * - 1: Number of bits by which a given bit-vector is to be extended
1228 *
1229 * Create with:
1230 * - `Solver::mkOp(Kind kind, uint32_t param) const`.
1231 *
1232 * Apply bit-vector zero-extend.
1233 *
1234 * Parameters:
1235 * - 1: Op of kind BITVECTOR_ZERO_EXTEND
1236 * - 2: Term of bit-vector sort
1237 *
1238 * Create with:
1239 * - `Solver::mkTerm(const Op& op, const Term& child) const`
1240 * - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const`
1241 */
1242 BITVECTOR_ZERO_EXTEND,
1243 /**
1244 * Operator for bit-vector sign-extend.
1245 *
1246 * Parameter:
1247 * - 1: Number of bits by which a given bit-vector is to be extended
1248 *
1249 * Create with:
1250 * - `Solver::mkOp(Kind kind, uint32_t param) const`.
1251 *
1252 * Apply bit-vector sign-extend.
1253 *
1254 * Parameters:
1255 * - 1: Op of kind BITVECTOR_SIGN_EXTEND
1256 * - 2: Term of bit-vector sort
1257 *
1258 * Create with:
1259 * - `Solver::mkTerm(const Op& op, const Term& child) const`
1260 * - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const`
1261 */
1262 BITVECTOR_SIGN_EXTEND,
1263 /**
1264 * Operator for bit-vector rotate left.
1265 *
1266 * Parameter:
1267 * - 1: Number of bits by which a given bit-vector is to be rotated
1268 *
1269 * Create with:
1270 * - `Solver::mkOp(Kind kind, uint32_t param) const`.
1271 *
1272 * Apply bit-vector rotate left.
1273 *
1274 * Parameters:
1275 * - 1: Op of kind BITVECTOR_ROTATE_LEFT
1276 * - 2: Term of bit-vector sort
1277 *
1278 * Create with:
1279 * - `Solver::mkTerm(const Op& op, const Term& child) const`
1280 * - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const`
1281 */
1282 BITVECTOR_ROTATE_LEFT,
1283 /**
1284 * Operator for bit-vector rotate right.
1285 *
1286 * Parameter:
1287 * - 1: Number of bits by which a given bit-vector is to be rotated
1288 *
1289 * Create with:
1290 * - `Solver::mkOp(Kind kind, uint32_t param) const`.
1291 *
1292 * Apply bit-vector rotate right.
1293 *
1294 * Parameters:
1295 * - 1: Op of kind BITVECTOR_ROTATE_RIGHT
1296 * - 2: Term of bit-vector sort
1297 *
1298 * Create with:
1299 * - `Solver::mkTerm(const Op& op, const Term& child) const`
1300 * - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const`
1301 */
1302 BITVECTOR_ROTATE_RIGHT,
1303 #if 0
1304 /* bit-vector boolean bit extract. */
1305 BITVECTOR_BITOF,
1306 #endif
1307 /**
1308 * Operator for the conversion from Integer to bit-vector.
1309 *
1310 * Parameter:
1311 * - 1: Size of the bit-vector to convert to
1312 *
1313 * Create with:
1314 * - `Solver::mkOp(Kind kind, uint32_t param) const`.
1315 *
1316 * Apply integer conversion to bit-vector.
1317 *
1318 * Parameters:
1319 * - 1: Op of kind INT_TO_BITVECTOR
1320 * - 2: Integer term
1321 *
1322 * Create with:
1323 * - `Solver::mkTerm(const Op& op, const Term& child) const`
1324 * - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const`
1325 */
1326 INT_TO_BITVECTOR,
1327 /**
1328 * Bit-vector conversion to (nonnegative) integer.
1329 *
1330 * Parameter:
1331 * - 1: Term of bit-vector sort
1332 *
1333 * Create with:
1334 * - `Solver::mkTerm(Kind kind, const Term& child) const`
1335 */
1336 BITVECTOR_TO_NAT,
1337
1338 /* FP -------------------------------------------------------------------- */
1339
1340 /**
1341 * Floating-point constant, constructed from a double or string.
1342 *
1343 * Parameters:
1344 * - 1: Size of the exponent
1345 * - 2: Size of the significand
1346 * - 3: Value of the floating-point constant as a bit-vector term
1347 *
1348 * Create with:
1349 * - `Solver::mkFloatingPoint(uint32_t exp, uint32_t sig, Term val) const`
1350 */
1351 CONST_FLOATINGPOINT,
1352 /**
1353 * Floating-point rounding mode term.
1354 *
1355 * Create with:
1356 * - `Solver::mkRoundingMode(RoundingMode rm) const`
1357 */
1358 CONST_ROUNDINGMODE,
1359 /**
1360 * Create floating-point literal from bit-vector triple.
1361 *
1362 * Parameters:
1363 * - 1: Sign bit as a bit-vector term
1364 * - 2: Exponent bits as a bit-vector term
1365 * - 3: Significand bits as a bit-vector term (without hidden bit)
1366 *
1367 * Create with:
1368 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
1369 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
1370 */
1371 FLOATINGPOINT_FP,
1372 /**
1373 * Floating-point equality.
1374 *
1375 * Parameters:
1376 * - 1..2: Terms of floating point sort
1377 *
1378 * Create with:
1379 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
1380 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
1381 */
1382 FLOATINGPOINT_EQ,
1383 /**
1384 * Floating-point absolute value.
1385 *
1386 * Parameters:
1387 * - 1: Term of floating point sort
1388 *
1389 * Create with:
1390 * - `Solver::mkTerm(Kind kind, const Term& child) const`
1391 */
1392 FLOATINGPOINT_ABS,
1393 /**
1394 * Floating-point negation.
1395 *
1396 * Parameters:
1397 * - 1: Term of floating point sort
1398 *
1399 * Create with:
1400 * - `Solver::mkTerm(Kind kind, const Term& child) const`
1401 */
1402 FLOATINGPOINT_NEG,
1403 /**
1404 * Floating-point addition.
1405 *
1406 * Parameters:
1407 * - 1: CONST_ROUNDINGMODE
1408 * - 2: Term of sort FloatingPoint
1409 * - 3: Term of sort FloatingPoint
1410 *
1411 * Create with:
1412 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
1413 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
1414 */
1415 FLOATINGPOINT_ADD,
1416 /**
1417 * Floating-point sutraction.
1418 *
1419 * Parameters:
1420 * - 1: CONST_ROUNDINGMODE
1421 * - 2: Term of sort FloatingPoint
1422 * - 3: Term of sort FloatingPoint
1423 *
1424 * Create with:
1425 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
1426 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
1427 */
1428 FLOATINGPOINT_SUB,
1429 /**
1430 * Floating-point multiply.
1431 *
1432 * Parameters:
1433 * - 1: CONST_ROUNDINGMODE
1434 * - 2: Term of sort FloatingPoint
1435 * - 3: Term of sort FloatingPoint
1436 *
1437 * Create with:
1438 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
1439 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
1440 */
1441 FLOATINGPOINT_MULT,
1442 /**
1443 * Floating-point division.
1444 *
1445 * Parameters:
1446 * - 1: CONST_ROUNDINGMODE
1447 * - 2: Term of sort FloatingPoint
1448 * - 3: Term of sort FloatingPoint
1449 *
1450 * Create with:
1451 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
1452 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
1453 */
1454 FLOATINGPOINT_DIV,
1455 /**
1456 * Floating-point fused multiply and add.
1457 *
1458 * Parameters:
1459 * - 1: CONST_ROUNDINGMODE
1460 * - 2: Term of sort FloatingPoint
1461 * - 3: Term of sort FloatingPoint
1462 * - 4: Term of sort FloatingPoint
1463 *
1464 * Create with:
1465 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
1466 */
1467 FLOATINGPOINT_FMA,
1468 /**
1469 * Floating-point square root.
1470 *
1471 * Parameters:
1472 * - 1: CONST_ROUNDINGMODE
1473 * - 2: Term of sort FloatingPoint
1474 *
1475 * Create with:
1476 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
1477 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
1478 */
1479 FLOATINGPOINT_SQRT,
1480 /**
1481 * Floating-point remainder.
1482 *
1483 * Parameters:
1484 * - 1..2: Terms of floating point sort
1485 *
1486 * Create with:
1487 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
1488 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
1489 */
1490 FLOATINGPOINT_REM,
1491 /**
1492 * Floating-point round to integral.
1493 *
1494 * Parameters:
1495 * -1..2: Terms of floating point sort
1496 *
1497 * Create with:
1498 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
1499 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
1500 */
1501 FLOATINGPOINT_RTI,
1502 /**
1503 * Floating-point minimum.
1504 *
1505 * Parameters:
1506 * - 1..2: Terms of floating point sort
1507 *
1508 * Create with:
1509 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
1510 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
1511 */
1512 FLOATINGPOINT_MIN,
1513 /**
1514 * Floating-point maximum.
1515 *
1516 * Parameters:
1517 * - 1..2: Terms of floating point sort
1518 *
1519 * Create with:
1520 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
1521 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
1522 */
1523 FLOATINGPOINT_MAX,
1524 /**
1525 * Floating-point less than or equal.
1526 *
1527 * Parameters:
1528 * - 1..2: Terms of floating point sort
1529 *
1530 * Create with:
1531 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
1532 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
1533 */
1534 FLOATINGPOINT_LEQ,
1535 /**
1536 * Floating-point less than.
1537 *
1538 * Parameters:
1539 * - 1..2: Terms of floating point sort
1540 *
1541 * Create with:
1542 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
1543 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
1544 */
1545 FLOATINGPOINT_LT,
1546 /**
1547 * Floating-point greater than or equal.
1548 *
1549 * Parameters:
1550 * - 1..2: Terms of floating point sort
1551 *
1552 * Create with:
1553 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
1554 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
1555 */
1556 FLOATINGPOINT_GEQ,
1557 /**
1558 * Floating-point greater than.
1559 *
1560 * Parameters:
1561 * - 1..2: Terms of floating point sort
1562 *
1563 * Create with:
1564 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
1565 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
1566 */
1567 FLOATINGPOINT_GT,
1568 /**
1569 * Floating-point is normal.
1570 *
1571 * Parameters:
1572 * - 1: Term of floating point sort
1573 *
1574 * Create with:
1575 * - `Solver::mkTerm(Kind kind, const Term& child) const`
1576 */
1577 FLOATINGPOINT_ISN,
1578 /**
1579 * Floating-point is sub-normal.
1580 *
1581 * Parameters:
1582 * - 1: Term of floating point sort
1583 *
1584 * Create with:
1585 * - `Solver::mkTerm(Kind kind, const Term& child) const`
1586 */
1587 FLOATINGPOINT_ISSN,
1588 /**
1589 * Floating-point is zero.
1590 *
1591 * Parameters:
1592 * - 1: Term of floating point sort
1593 *
1594 * Create with:
1595 * - `Solver::mkTerm(Kind kind, const Term& child) const`
1596 */
1597 FLOATINGPOINT_ISZ,
1598 /**
1599 * Floating-point is infinite.
1600 *
1601 * Parameters:
1602 * - 1: Term of floating point sort
1603 *
1604 * Create with:
1605 * - `Solver::mkTerm(Kind kind, const Term& child) const`
1606 */
1607 FLOATINGPOINT_ISINF,
1608 /**
1609 * Floating-point is NaN.
1610 *
1611 * Parameters:
1612 * - 1: Term of floating point sort
1613 *
1614 * Create with:
1615 * - `Solver::mkTerm(Kind kind, const Term& child) const`
1616 */
1617 FLOATINGPOINT_ISNAN,
1618 /**
1619 * Floating-point is negative.
1620 *
1621 * Parameters:
1622 * - 1: Term of floating point sort
1623 *
1624 * Create with:
1625 * - `Solver::mkTerm(Kind kind, const Term& child) const`
1626 */
1627 FLOATINGPOINT_ISNEG,
1628 /**
1629 * Floating-point is positive.
1630 *
1631 * Parameters:
1632 * - 1: Term of floating point sort
1633 *
1634 * Create with:
1635 * - `Solver::mkTerm(Kind kind, const Term& child) const`
1636 */
1637 FLOATINGPOINT_ISPOS,
1638 /**
1639 * Operator for to_fp from bit vector.
1640 *
1641 * Parameters:
1642 * - 1: Exponent size
1643 * - 2: Significand size
1644 *
1645 * Create with:
1646 * - `Solver::mkOp(Kind kind, uint32_t param1, uint32_t param2) const`
1647 *
1648 * Conversion from an IEEE-754 bit vector to floating-point.
1649 *
1650 * Parameters:
1651 * - 1: Op of kind FLOATINGPOINT_TO_FP_IEEE_BITVECTOR
1652 * - 2: Term of sort FloatingPoint
1653 *
1654 * Create with:
1655 * - `Solver::mkTerm(const Op& op, const Term& child) const`
1656 * - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const`
1657 */
1658 FLOATINGPOINT_TO_FP_IEEE_BITVECTOR,
1659 /**
1660 * Operator for to_fp from floating point.
1661 *
1662 * Parameters:
1663 * - 1: Exponent size
1664 * - 2: Significand size
1665 *
1666 * Create with:
1667 * - `Solver::mkOp(Kind kind, uint32_t param1, uint32_t param2) const`
1668 *
1669 * Conversion between floating-point sorts.
1670 *
1671 * Parameters:
1672 * - 1: Op of kind FLOATINGPOINT_TO_FP_FLOATINGPOINT
1673 * - 2: Term of sort FloatingPoint
1674 *
1675 * Create with:
1676 * - `Solver::mkTerm(const Op& op, const Term& child) const`
1677 * - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const`
1678 */
1679 FLOATINGPOINT_TO_FP_FLOATINGPOINT,
1680 /**
1681 * Operator for to_fp from real.
1682 *
1683 * Parameters:
1684 * - 1: Exponent size
1685 * - 2: Significand size
1686 *
1687 * Create with:
1688 * - `Solver::mkOp(Kind kind, uint32_t param1, uint32_t param2) const`
1689 *
1690 * Conversion from a real to floating-point.
1691 *
1692 * Parameters:
1693 * - 1: Op of kind FLOATINGPOINT_TO_FP_REAL
1694 * - 2: Term of sort FloatingPoint
1695 *
1696 * Create with:
1697 * - `Solver::mkTerm(const Op& op, const Term& child) const`
1698 * - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const`
1699 */
1700 FLOATINGPOINT_TO_FP_REAL,
1701 /**
1702 * Operator for to_fp from signed bit vector
1703 *
1704 * Parameters:
1705 * - 1: Exponent size
1706 * - 2: Significand size
1707 *
1708 * Create with:
1709 * - `Solver::mkOp(Kind kind, uint32_t param1, uint32_t param2) const`
1710 *
1711 * Conversion from a signed bit vector to floating-point.
1712 *
1713 * Parameters:
1714 * - 1: Op of kind FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR
1715 * - 2: Term of sort FloatingPoint
1716 *
1717 * Create with:
1718 * - `Solver::mkTerm(const Op& op, const Term& child) const`
1719 * - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const`
1720 */
1721 FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR,
1722 /**
1723 * Operator for to_fp from unsigned bit vector.
1724 *
1725 * Parameters:
1726 * - 1: Exponent size
1727 * - 2: Significand size
1728 *
1729 * Create with:
1730 * - `Solver::mkOp(Kind kind, uint32_t param1, uint32_t param2) const`
1731 *
1732 * Converting an unsigned bit vector to floating-point.
1733 *
1734 * Parameters:
1735 * - 1: Op of kind FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR
1736 * - 2: Term of sort FloatingPoint
1737 *
1738 * Create with:
1739 * - `Solver::mkTerm(const Op& op, const Term& child) const`
1740 * - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const`
1741 */
1742 FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR,
1743 /**
1744 * Operator for a generic to_fp.
1745 *
1746 * Parameters:
1747 * - 1: exponent size
1748 * - 2: Significand size
1749 *
1750 * Create with:
1751 * - `Solver::mkOp(Kind kind, uint32_t param1, uint32_t param2) const`
1752 *
1753 * Generic conversion to floating-point, used in parsing only.
1754 *
1755 * Parameters:
1756 * - 1: Op of kind FLOATINGPOINT_TO_FP_GENERIC
1757 * - 2: Term of sort FloatingPoint
1758 *
1759 * Create with:
1760 * - `Solver::mkTerm(const Op& op, const Term& child) const`
1761 * - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const`
1762 */
1763 FLOATINGPOINT_TO_FP_GENERIC,
1764 /**
1765 * Operator for to_ubv.
1766 *
1767 * Parameters:
1768 * - 1: Size of the bit-vector to convert to
1769 *
1770 * Create with:
1771 * - `Solver::mkOp(Kind kind, uint32_t param) const`
1772 *
1773 * Conversion from a floating-point value to an unsigned bit vector.
1774 *
1775 * Parameters:
1776 * - 1: Op of kind FLOATINGPOINT_TO_FP_TO_UBV
1777 * - 2: Term of sort FloatingPoint
1778 *
1779 * Create with:
1780 * - `Solver::mkTerm(const Op& op, const Term& child) const`
1781 * - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const`
1782 */
1783 FLOATINGPOINT_TO_UBV,
1784 /**
1785 * Operator for to_sbv.
1786 *
1787 * Parameters:
1788 * - 1: Size of the bit-vector to convert to
1789 *
1790 * Create with:
1791 * - `Solver::mkOp(Kind kind, uint32_t param) const`
1792 *
1793 * Conversion from a floating-point value to a signed bit vector.
1794 *
1795 * Parameters:
1796 * - 1: Op of kind FLOATINGPOINT_TO_FP_TO_SBV
1797 * - 2: Term of sort FloatingPoint
1798 *
1799 * Create with:
1800 * - `Solver::mkTerm(const Op& op, const Term& child) const`
1801 * - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const`
1802 */
1803 FLOATINGPOINT_TO_SBV,
1804 /**
1805 * Floating-point to real.
1806 *
1807 * Parameters:
1808 * - 1: Term of sort FloatingPoint
1809 *
1810 * Create with:
1811 * - `Solver::mkTerm(Kind kind, const Term& child) const`
1812 */
1813 FLOATINGPOINT_TO_REAL,
1814
1815 /* Arrays ---------------------------------------------------------------- */
1816
1817 /**
1818 * Array select.
1819 *
1820 * Parameters:
1821 * - 1: Term of array sort
1822 * - 2: Selection index
1823 *
1824 * Create with:
1825 * - `Solver::mkTerm(const Op& op, const Term& child1, const Term& child2) const`
1826 * - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const`
1827 */
1828 SELECT,
1829 /**
1830 * Array store.
1831 *
1832 * Parameters:
1833 * - 1: Term of array sort
1834 * - 2: Store index
1835 * - 3: Term to store at the index
1836 *
1837 * Create with:
1838 * - `Solver::mkTerm(const Op& op, const Term& child1, const Term& child2, const Term& child3) const`
1839 * - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const`
1840 */
1841 STORE,
1842 /**
1843 * Constant array.
1844 *
1845 * Parameters:
1846 * - 1: Array sort
1847 * - 2: Term representing a constant
1848 *
1849 * Create with:
1850 * - `Solver::mkTerm(const Op& op, const Term& child1, const Term& child2) const`
1851 * - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const`
1852 *
1853 * Note: We currently support the creation of constant arrays, but under some
1854 * conditions when there is a chain of equalities connecting two constant
1855 * arrays, the solver doesn't know what to do and aborts (Issue <a href="https://github.com/CVC4/CVC4/issues/1667">#1667</a>).
1856 */
1857 CONST_ARRAY,
1858 /**
1859 * Equality over arrays a and b over a given range [i,j], i.e.,
1860 * @f[
1861 * \forall k . i \leq k \leq j \Rightarrow a[k] = b[k]
1862 * @f]
1863 *
1864 * Parameters:
1865 * - 1: First array
1866 * - 2: Second array
1867 * - 3: Lower bound of range (inclusive)
1868 * - 4: Uppper bound of range (inclusive)
1869 *
1870 * Create with:
1871 * - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const`
1872 *
1873 * Note: We currently support the creation of array equalities over index
1874 * types bit-vector, floating-point, integer and real. Option --arrays-exp is
1875 * required to support this operator.
1876 */
1877 EQ_RANGE,
1878 #if 0
1879 /* array table function (internal-only symbol) */
1880 ARR_TABLE_FUN,
1881 /* array lambda (internal-only symbol) */
1882 ARRAY_LAMBDA,
1883 /* partial array select, for internal use only */
1884 PARTIAL_SELECT_0,
1885 /* partial array select, for internal use only */
1886 PARTIAL_SELECT_1,
1887 #endif
1888
1889 /* Datatypes ------------------------------------------------------------- */
1890
1891 /**
1892 * Constructor application.
1893 *
1894 * Paramters: n > 0
1895 * - 1: Constructor (operator)
1896 * - 2..n: Parameters to the constructor
1897 *
1898 * Create with:
1899 * - `Solver::mkTerm(const Op& op) const`
1900 * - `Solver::mkTerm(const Op& op, const Term& child) const`
1901 * - `Solver::mkTerm(const Op& op, const Term& child1, const Term& child2) const`
1902 * - `Solver::mkTerm(const Op& op, const Term& child1, const Term& child2, const Term& child3) const`
1903 * - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const`
1904 */
1905 APPLY_CONSTRUCTOR,
1906 /**
1907 * Datatype selector application, which is undefined if misapplied.
1908 *
1909 * Parameters:
1910 * - 1: Selector (operator)
1911 * - 2: Datatype term
1912 *
1913 * Create with:
1914 * - `Solver::mkTerm(const Op& op, const Term& child) const`
1915 */
1916 APPLY_SELECTOR,
1917 /**
1918 * Datatype tester application.
1919 *
1920 * Parameters:
1921 * - 1: Tester term
1922 * - 2: Datatype term
1923 *
1924 * Create with:
1925 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
1926 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
1927 */
1928 APPLY_TESTER,
1929 /**
1930 * Datatype update application, which does not change the argument if
1931 * misapplied.
1932 *
1933 * Parameters:
1934 * - 1: Updater (operator)
1935 * - 2: Datatype term
1936 * - 3: Value to update a field of the datatype term with
1937 *
1938 * Create with:
1939 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
1940 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
1941 */
1942 APPLY_UPDATER,
1943 /**
1944 * Match expressions.
1945 * For example, the smt2 syntax match term
1946 * `(match l (((cons h t) h) (nil 0)))`
1947 * is represented by the AST
1948 *
1949 * (MATCH l
1950 * (MATCH_BIND_CASE (BOUND_VAR_LIST h t) (cons h t) h)
1951 * (MATCH_CASE nil 0))
1952 *
1953 * The type of the last argument of each case term could be equal.
1954 *
1955 * Parameters: n > 1
1956 * - 1..n: Terms of kind MATCH_CASE or MATCH_BIND_CASE
1957 *
1958 * Create with:
1959 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
1960 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
1961 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
1962 *
1963 */
1964 MATCH,
1965 /**
1966 * Match case
1967 * A (constant) case expression to be used within a match expression.
1968 *
1969 * Parameters:
1970 * - 1: Term denoting the pattern expression
1971 * - 2: Term denoting the return value
1972 *
1973 * Create with:
1974 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
1975 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
1976 */
1977 MATCH_CASE,
1978 /**
1979 * Match bind case
1980 * A (non-constant) case expression to be used within a match expression.
1981 *
1982 * Parameters:
1983 * - 1: a BOUND_VAR_LIST Term containing the free variables of the case
1984 * - 2: Term denoting the pattern expression
1985 * - 3: Term denoting the return value
1986 *
1987 * Create with:
1988 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
1989 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
1990 */
1991 MATCH_BIND_CASE,
1992 /**
1993 * Datatypes size
1994 * An operator mapping datatypes to an integer denoting the number of
1995 * non-nullary applications of constructors they contain.
1996 *
1997 * Parameters:
1998 * - 1: Datatype term
1999 *
2000 * Create with:
2001 * - `Solver::mkTerm(Kind kind, const Term& child1) const`
2002 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
2003 */
2004 DT_SIZE,
2005 /**
2006 * Operator for tuple projection indices
2007 *
2008 * Parameters:
2009 * - 1: The tuple projection indices
2010 *
2011 * Create with:
2012 * - `Solver::mkOp(Kind TUPLE_PROJECT, std::vector<uint32_t> param) const`
2013 *
2014 * Constructs a new tuple from an existing one using the elements at the
2015 * given indices
2016 *
2017 * Parameters:
2018 * - 1: a term of tuple sort
2019 *
2020 * Create with:
2021 * - `Solver::mkTerm(const Op& op, const Term& child) const`
2022 * - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const`
2023 */
2024 TUPLE_PROJECT,
2025 #if 0
2026 /* datatypes height bound */
2027 DT_HEIGHT_BOUND,
2028 /* datatypes height bound */
2029 DT_SIZE_BOUND,
2030 /* datatypes sygus bound */
2031 DT_SYGUS_BOUND,
2032 /* datatypes sygus term order */
2033 DT_SYGUS_TERM_ORDER,
2034 /* datatypes sygus is constant */
2035 DT_SYGUS_IS_CONST,
2036 #endif
2037
2038 /* Separation Logic ------------------------------------------------------ */
2039
2040 /**
2041 * Separation logic nil term.
2042 *
2043 * Parameters: none
2044 *
2045 * Create with:
2046 * - `Solver::mkSepNil(const Sort& sort) const`
2047 */
2048 SEP_NIL,
2049 /**
2050 * Separation logic empty heap.
2051 *
2052 * Parameters:
2053 * - 1: Term of the same sort as the sort of the location of the heap
2054 * that is constrained to be empty
2055 * - 2: Term of the same sort as the data sort of the heap that is
2056 * that is constrained to be empty
2057 *
2058 * Create with:
2059 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
2060 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
2061 */
2062 SEP_EMP,
2063 /**
2064 * Separation logic points-to relation.
2065 *
2066 * Parameters:
2067 * - 1: Location of the points-to constraint
2068 * - 2: Data of the points-to constraint
2069 *
2070 * Create with:
2071 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
2072 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
2073 */
2074 SEP_PTO,
2075 /**
2076 * Separation logic star.
2077 *
2078 * Parameters: n > 1
2079 * - 1..n: Child constraints that hold in disjoint (separated) heaps
2080 *
2081 * Create with:
2082 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
2083 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
2084 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
2085 */
2086 SEP_STAR,
2087 /**
2088 * Separation logic magic wand.
2089 *
2090 * Parameters:
2091 * - 1: Antecendant of the magic wand constraint
2092 * - 2: Conclusion of the magic wand constraint, which is asserted to
2093 * hold in all heaps that are disjoint extensions of the antecedent.
2094 *
2095 * Create with:
2096 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
2097 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
2098 */
2099 SEP_WAND,
2100 #if 0
2101 /* separation label (internal use only) */
2102 SEP_LABEL,
2103 #endif
2104
2105 /* Sets ------------------------------------------------------------------ */
2106
2107 /**
2108 * Empty set constant.
2109 *
2110 * Parameters:
2111 * - 1: Sort of the set elements
2112 *
2113 * Create with:
2114 * - `Solver::mkEmptySet(const Sort& sort) const`
2115 */
2116 EMPTYSET,
2117 /**
2118 * Set union.
2119 *
2120 * Parameters:
2121 * - 1..2: Terms of set sort
2122 *
2123 * Create with:
2124 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
2125 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
2126 */
2127 UNION,
2128 /**
2129 * Set intersection.
2130 *
2131 * Parameters:
2132 * - 1..2: Terms of set sort
2133 *
2134 * Create with:
2135 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
2136 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
2137 */
2138 INTERSECTION,
2139 /**
2140 * Set subtraction.
2141 *
2142 * Parameters:
2143 * - 1..2: Terms of set sort
2144 *
2145 * Create with:
2146 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
2147 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
2148 */
2149 SETMINUS,
2150 /**
2151 * Subset predicate.
2152 *
2153 * Parameters:
2154 * - 1..2: Terms of set sort, [1] a subset of set [2]?
2155 *
2156 * Create with:
2157 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
2158 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
2159 */
2160 SUBSET,
2161 /**
2162 * Set membership predicate.
2163 *
2164 * Parameters:
2165 * - 1..2: Terms of set sort, [1] a member of set [2]?
2166 *
2167 * Create with:
2168 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
2169 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
2170 */
2171 MEMBER,
2172 /**
2173 * Construct a singleton set from an element given as a parameter.
2174 * The returned set has same type of the element.
2175 *
2176 * Parameters:
2177 * - 1: Single element
2178 *
2179 * Create with:
2180 * - `Solver::mkTerm(Kind kind, const Term& child) const`
2181 */
2182 SINGLETON,
2183 /**
2184 * The set obtained by inserting elements;
2185 *
2186 * Parameters: n > 0
2187 * - 1..n-1: Elements inserted into set [n]
2188 * - n: Set Term
2189 *
2190 * Create with:
2191 * - `Solver::mkTerm(Kind kind, const Term& child) const`
2192 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
2193 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
2194 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
2195 */
2196 INSERT,
2197 /**
2198 * Set cardinality.
2199 *
2200 * Parameters:
2201 * - 1: Set to determine the cardinality of
2202 *
2203 * Create with:
2204 * - `Solver::mkTerm(Kind kind, const Term& child) const`
2205 */
2206 CARD,
2207 /**
2208 * Set complement with respect to finite universe.
2209 *
2210 * Parameters:
2211 * - 1: Set to complement
2212 *
2213 * Create with:
2214 * - `Solver::mkTerm(Kind kind, const Term& child) const`
2215 */
2216 COMPLEMENT,
2217 /**
2218 * Finite universe set.
2219 * All set variables must be interpreted as subsets of it.
2220 *
2221 * Create with:
2222 * - `Solver::mkUniverseSet(const Sort& sort) const`
2223 */
2224 UNIVERSE_SET,
2225 /**
2226 * Set join.
2227 *
2228 * Parameters:
2229 * - 1..2: Terms of set sort
2230 *
2231 * Create with:
2232 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
2233 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
2234 */
2235 JOIN,
2236 /**
2237 * Set cartesian product.
2238 *
2239 * Parameters:
2240 * - 1..2: Terms of set sort
2241 *
2242 * Create with:
2243 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
2244 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
2245 */
2246 PRODUCT,
2247 /**
2248 * Set transpose.
2249 *
2250 * Parameters:
2251 * - 1: Term of set sort
2252 *
2253 * Create with:
2254 * - `Solver::mkTerm(Kind kind, const Term& child) const`
2255 */
2256 TRANSPOSE,
2257 /**
2258 * Set transitive closure.
2259 *
2260 * Parameters:
2261 * - 1: Term of set sort
2262 *
2263 * Create with:
2264 * - `Solver::mkTerm(Kind kind, const Term& child) const`
2265 */
2266 TCLOSURE,
2267 /**
2268 * Set join image.
2269 *
2270 * Parameters:
2271 * - 1..2: Terms of set sort
2272 *
2273 * Create with:
2274 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
2275 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
2276 */
2277 JOIN_IMAGE,
2278 /**
2279 * Set identity.
2280 *
2281 * Parameters:
2282 * - 1: Term of set sort
2283 *
2284 * Create with:
2285 * - `Solver::mkTerm(Kind kind, const Term& child) const`
2286 */
2287 IDEN,
2288 /**
2289 * Set comprehension
2290 * A set comprehension is specified by a bound variable list x1 ... xn,
2291 * a predicate P[x1...xn], and a term t[x1...xn]. A comprehension C with the
2292 * above form has members given by the following semantics:
2293 * @f[
2294 * \forall y. ( \exists x_1...x_n. P[x_1...x_n] \hat{} t[x_1...x_n] = y )
2295 * \Leftrightarrow (member y C)
2296 * @f]
2297 * where y ranges over the element type of the (set) type of the
2298 * comprehension. If @f$ t[x_1..x_n] @f$ is not provided, it is equivalent to
2299 * y in the above formula.
2300 *
2301 * Parameters:
2302 * - 1: Term BOUND_VAR_LIST
2303 * - 2: Term denoting the predicate of the comprehension
2304 * - 3: (optional) a Term denoting the generator for the comprehension
2305 *
2306 * Create with:
2307 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
2308 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
2309 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
2310 */
2311 COMPREHENSION,
2312 /**
2313 * Returns an element from a given set.
2314 * If a set A = {x}, then the term (choose A) is equivalent to the term x.
2315 * If the set is empty, then (choose A) is an arbitrary value.
2316 * If the set has cardinality > 1, then (choose A) will deterministically
2317 * return an element in A.
2318 *
2319 * Parameters:
2320 * - 1: Term of set sort
2321 *
2322 * Create with:
2323 * - `Solver::mkTerm(Kind kind, const Term& child) const`
2324 */
2325 CHOOSE,
2326 /**
2327 * Set is_singleton predicate.
2328 *
2329 * Parameters:
2330 * - 1: Term of set sort, is [1] a singleton set?
2331 *
2332 * Create with:
2333 * - `Solver::mkTerm(Kind kind, const Term& child) const`
2334 */
2335 IS_SINGLETON,
2336 /* Bags ------------------------------------------------------------------ */
2337 /**
2338 * Empty bag constant.
2339 *
2340 * Parameters:
2341 * - 1: Sort of the bag elements
2342 *
2343 * Create with:
2344 * mkEmptyBag(const Sort& sort)
2345 */
2346 EMPTYBAG,
2347 /**
2348 * Bag max union.
2349 * Parameters:
2350 * - 1..2: Terms of bag sort
2351 *
2352 * Create with:
2353 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
2354 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
2355 */
2356 UNION_MAX,
2357 /**
2358 * Bag disjoint union (sum).
2359 *
2360 * Parameters:
2361 * -1..2: Terms of bag sort
2362 *
2363 * Create with:
2364 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
2365 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
2366 */
2367 UNION_DISJOINT,
2368 /**
2369 * Bag intersection (min).
2370 *
2371 * Parameters:
2372 * - 1..2: Terms of bag sort
2373 *
2374 * Create with:
2375 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
2376 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
2377 */
2378 INTERSECTION_MIN,
2379 /**
2380 * Bag difference subtract (subtracts multiplicities of the second from the
2381 * first).
2382 *
2383 * Parameters:
2384 * - 1..2: Terms of bag sort
2385 *
2386 * Create with:
2387 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
2388 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
2389 */
2390 DIFFERENCE_SUBTRACT,
2391 /**
2392 * Bag difference 2 (removes shared elements in the two bags).
2393 *
2394 * Parameters:
2395 * - 1..2: Terms of bag sort
2396 *
2397 * Create with:
2398 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
2399 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
2400 */
2401 DIFFERENCE_REMOVE,
2402 /**
2403 * Inclusion predicate for bags
2404 * (multiplicities of the first bag <= multiplicities of the second bag).
2405 *
2406 * Parameters:
2407 * - 1..2: Terms of bag sort
2408 *
2409 * Create with:
2410 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
2411 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
2412 */
2413 SUBBAG,
2414 /**
2415 * Element multiplicity in a bag
2416 *
2417 * Parameters:
2418 * - 1..2: Terms of bag sort (Bag E), [1] an element of sort E
2419 *
2420 * Create with:
2421 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
2422 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
2423 */
2424 BAG_COUNT,
2425 /**
2426 * Eliminate duplicates in a given bag. The returned bag contains exactly the
2427 * same elements in the given bag, but with multiplicity one.
2428 *
2429 * Parameters:
2430 * - 1: a term of bag sort
2431 *
2432 * Create with:
2433 * - `Solver::mkTerm(Kind kind, const Term& child) const`
2434 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
2435 */
2436 DUPLICATE_REMOVAL,
2437 /**
2438 * The bag of the single element given as a parameter.
2439 *
2440 * Parameters:
2441 * - 1: Single element
2442 *
2443 * Create with:
2444 * - `Solver::mkTerm(Kind kind, const Term& child) const`
2445 */
2446 MK_BAG,
2447 /**
2448 * Bag cardinality.
2449 *
2450 * Parameters:
2451 * - 1: Bag to determine the cardinality of
2452 *
2453 * Create with:
2454 * - `Solver::mkTerm(Kind kind, const Term& child) const`
2455 */
2456 BAG_CARD,
2457 /**
2458 * Returns an element from a given bag.
2459 * If a bag A = {(x,n)} where n is the multiplicity, then the term (choose A)
2460 * is equivalent to the term x.
2461 * If the bag is empty, then (choose A) is an arbitrary value.
2462 * If the bag contains distinct elements, then (choose A) will
2463 * deterministically return an element in A.
2464 *
2465 * Parameters:
2466 * - 1: Term of bag sort
2467 *
2468 * Create with:
2469 * - `Solver::mkTerm(Kind kind, const Term& child) const`
2470 */
2471 BAG_CHOOSE,
2472 /**
2473 * Bag is_singleton predicate (single element with multiplicity exactly one).
2474 * Parameters:
2475 * - 1: Term of bag sort, is [1] a singleton bag?
2476 *
2477 * Create with:
2478 * - `Solver::mkTerm(Kind kind, const Term& child) const`
2479 */
2480 BAG_IS_SINGLETON,
2481 /**
2482 * Bag.from_set converts a set to a bag.
2483 *
2484 * Parameters:
2485 * - 1: Term of set sort
2486 *
2487 * Create with:
2488 * - `Solver::mkTerm(Kind kind, const Term& child) const`
2489 */
2490 BAG_FROM_SET,
2491 /**
2492 * Bag.to_set converts a bag to a set.
2493 *
2494 * Parameters:
2495 * - 1: Term of bag sort
2496 *
2497 * Create with:
2498 * - `Solver::mkTerm(Kind kind, const Term& child) const`
2499 */
2500 BAG_TO_SET,
2501
2502 /* Strings --------------------------------------------------------------- */
2503
2504 /**
2505 * String concat.
2506 *
2507 * Parameters: n > 1
2508 * - 1..n: Terms of String sort
2509 *
2510 * Create with:
2511 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
2512 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
2513 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
2514 */
2515 STRING_CONCAT,
2516 /**
2517 * String membership.
2518 *
2519 * Parameters:
2520 * - 1: Term of String sort
2521 * - 2: Term of RegExp sort
2522 *
2523 * Create with:
2524 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
2525 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
2526 */
2527 STRING_IN_REGEXP,
2528 /**
2529 * String length.
2530 *
2531 * Parameters:
2532 * - 1: Term of String sort
2533 *
2534 * Create with:
2535 * - `Solver::mkTerm(Kind kind, const Term& child) const`
2536 */
2537 STRING_LENGTH,
2538 /**
2539 * String substring.
2540 * Extracts a substring, starting at index i and of length l, from a string
2541 * s. If the start index is negative, the start index is greater than the
2542 * length of the string, or the length is negative, the result is the empty
2543 * string.
2544 *
2545 * Parameters:
2546 * - 1: Term of sort String
2547 * - 2: Term of sort Integer (index i)
2548 * - 3: Term of sort Integer (length l)
2549 *
2550 * Create with:
2551 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
2552 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
2553 */
2554 STRING_SUBSTR,
2555 /**
2556 * String update.
2557 * Updates a string s by replacing its context starting at an index with t.
2558 * If the start index is negative, the start index is greater than the
2559 * length of the string, the result is s. Otherwise, the length of the
2560 * original string is preserved.
2561 *
2562 * Parameters:
2563 * - 1: Term of sort String
2564 * - 2: Term of sort Integer (index i)
2565 * - 3: Term of sort String (replacement string t)
2566 *
2567 * Create with:
2568 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
2569 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
2570 */
2571 STRING_UPDATE,
2572 /**
2573 * String character at.
2574 * Returns the character at index i from a string s. If the index is negative
2575 * or the index is greater than the length of the string, the result is the
2576 * empty string. Otherwise the result is a string of length 1.
2577 *
2578 * Parameters:
2579 * - 1: Term of sort String (string s)
2580 * - 2: Term of sort Integer (index i)
2581 *
2582 * Create with:
2583 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
2584 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
2585 */
2586 STRING_CHARAT,
2587 /**
2588 * String contains.
2589 * Checks whether a string s1 contains another string s2. If s2 is empty, the
2590 * result is always true.
2591 *
2592 * Parameters:
2593 * - 1: Term of sort String (the string s1)
2594 * - 2: Term of sort String (the string s2)
2595 *
2596 * Create with:
2597 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
2598 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
2599 */
2600 STRING_CONTAINS,
2601 /**
2602 * String index-of.
2603 * Returns the index of a substring s2 in a string s1 starting at index i. If
2604 * the index is negative or greater than the length of string s1 or the
2605 * substring s2 does not appear in string s1 after index i, the result is -1.
2606 *
2607 * Parameters:
2608 * - 1: Term of sort String (substring s1)
2609 * - 2: Term of sort String (substring s2)
2610 * - 3: Term of sort Integer (index i)
2611 *
2612 * Create with:
2613 * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
2614 * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
2615 */
2616 STRING_INDEXOF,
2617 /**
2618 * String index-of regular expression match.
2619 * Returns the first match of a regular expression r in a string s. If the
2620 * index is negative or greater than the length of string s1, or r does not
2621 * match a substring in s after index i, the result is -1.
2622 *
2623 * Parameters:
2624 * - 1: Term of sort String (string s)
2625 * - 2: Term of sort RegLan (regular expression r)
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_RE,
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