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