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