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