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    * The bag of the single element given as a parameter.
2463    *
2464    * Parameters:
2465    *   - 1: Single element
2466    *
2467    * Create with:
2468    *   - `Solver::mkTerm(Kind kind, const Term& child) const`
2469    */
2470   BAG_MAKE,
2471   /**
2472    * Bag cardinality.
2473    *
2474    * Parameters:
2475    *   - 1: Bag to determine the cardinality of
2476    *
2477    * Create with:
2478    *   - `Solver::mkTerm(Kind kind, const Term& child) const`
2479    */
2480   BAG_CARD,
2481   /**
2482    * Returns an element from a given bag.
2483    * If a bag A = {(x,n)} where n is the multiplicity, then the term (choose A)
2484    * is equivalent to the term x.
2485    * If the bag is empty, then (choose A) is an arbitrary value.
2486    * If the bag contains distinct elements, then (choose A) will
2487    * deterministically return an element in A.
2488    *
2489    * Parameters:
2490    *   - 1: Term of bag sort
2491    *
2492    * Create with:
2493    *   - `Solver::mkTerm(Kind kind, const Term& child) const`
2494    */
2495   BAG_CHOOSE,
2496   /**
2497    * Bag is_singleton predicate (single element with multiplicity exactly one).
2498    * Parameters:
2499    *   - 1: Term of bag sort, is [1] a singleton bag?
2500    *
2501    * Create with:
2502    *   - `Solver::mkTerm(Kind kind, const Term& child) const`
2503    */
2504   BAG_IS_SINGLETON,
2505   /**
2506    * Bag.from_set converts a set to a bag.
2507    *
2508    * Parameters:
2509    *   - 1: Term of set sort
2510    *
2511    * Create with:
2512    *   - `Solver::mkTerm(Kind kind, const Term& child) const`
2513    */
2514   BAG_FROM_SET,
2515   /**
2516    * Bag.to_set converts a bag to a set.
2517    *
2518    * Parameters:
2519    *   - 1: Term of bag sort
2520    *
2521    * Create with:
2522    *   - `Solver::mkTerm(Kind kind, const Term& child) const`
2523    */
2524   BAG_TO_SET,
2525   /**
2526    * bag.map operator applies the first argument, a function of type (-> T1 T2),
2527    * to every element of the second argument, a bag of type (Bag T1),
2528    * and returns a bag of type (Bag T2).
2529    *
2530    * Parameters:
2531    *   - 1: a function of type (-> T1 T2)
2532    *   - 2: a bag of type (Bag T1)
2533    *
2534    * Create with:
2535    *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2)
2536    * const`
2537    *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
2538    */
2539   BAG_MAP,
2540
2541   /* Strings --------------------------------------------------------------- */
2542
2543   /**
2544    * String concat.
2545    *
2546    * Parameters: n > 1
2547    *   - 1..n: Terms of String sort
2548    *
2549    * Create with:
2550    *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
2551    *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
2552    *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
2553    */
2554   STRING_CONCAT,
2555   /**
2556    * String membership.
2557    *
2558    * Parameters:
2559    *   - 1: Term of String sort
2560    *   - 2: Term of RegExp sort
2561    *
2562    * Create with:
2563    *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
2564    *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
2565    */
2566   STRING_IN_REGEXP,
2567   /**
2568    * String length.
2569    *
2570    * Parameters:
2571    *   - 1: Term of String sort
2572    *
2573    * Create with:
2574    *   - `Solver::mkTerm(Kind kind, const Term& child) const`
2575    */
2576   STRING_LENGTH,
2577   /**
2578    * String substring.
2579    * Extracts a substring, starting at index i and of length l, from a string
2580    * s.  If the start index is negative, the start index is greater than the
2581    * length of the string, or the length is negative, the result is the empty
2582    * string.
2583    *
2584    * Parameters:
2585    *   - 1: Term of sort String
2586    *   - 2: Term of sort Integer (index i)
2587    *   - 3: Term of sort Integer (length l)
2588    *
2589    * Create with:
2590    *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
2591    *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
2592    */
2593   STRING_SUBSTR,
2594   /**
2595    * String update.
2596    * Updates a string s by replacing its context starting at an index with t.
2597    * If the start index is negative, the start index is greater than the
2598    * length of the string, the result is s. Otherwise, the length of the
2599    * original string is preserved.
2600    *
2601    * Parameters:
2602    *   - 1: Term of sort String
2603    *   - 2: Term of sort Integer (index i)
2604    *   - 3: Term of sort String (replacement string t)
2605    *
2606    * Create with:
2607    *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
2608    *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
2609    */
2610   STRING_UPDATE,
2611   /**
2612    * String character at.
2613    * Returns the character at index i from a string s. If the index is negative
2614    * or the index is greater than the length of the string, the result is the
2615    * empty string. Otherwise the result is a string of length 1.
2616    *
2617    * Parameters:
2618    *   - 1: Term of sort String (string s)
2619    *   - 2: Term of sort Integer (index i)
2620    *
2621    * Create with:
2622    *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
2623    *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
2624    */
2625   STRING_CHARAT,
2626   /**
2627    * String contains.
2628    * Checks whether a string s1 contains another string s2. If s2 is empty, the
2629    * result is always true.
2630    *
2631    * Parameters:
2632    *   - 1: Term of sort String (the string s1)
2633    *   - 2: Term of sort String (the string s2)
2634    *
2635    * Create with:
2636    *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
2637    *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
2638    */
2639   STRING_CONTAINS,
2640   /**
2641    * String index-of.
2642    * Returns the index of a substring s2 in a string s1 starting at index i. If
2643    * the index is negative or greater than the length of string s1 or the
2644    * substring s2 does not appear in string s1 after index i, the result is -1.
2645    *
2646    * Parameters:
2647    *   - 1: Term of sort String (substring s1)
2648    *   - 2: Term of sort String (substring s2)
2649    *   - 3: Term of sort Integer (index i)
2650    *
2651    * Create with:
2652    *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
2653    *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
2654    */
2655   STRING_INDEXOF,
2656   /**
2657    * String index-of regular expression match.
2658    * Returns the first match of a regular expression r in a string s. If the
2659    * index is negative or greater than the length of string s1, or r does not
2660    * match a substring in s after index i, the result is -1.
2661    *
2662    * Parameters:
2663    *   - 1: Term of sort String (string s)
2664    *   - 2: Term of sort RegLan (regular expression r)
2665    *   - 3: Term of sort Integer (index i)
2666    *
2667    * Create with:
2668    *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
2669    *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
2670    */
2671   STRING_INDEXOF_RE,
2672   /**
2673    * String replace.
2674    * Replaces a string s2 in a string s1 with string s3. If s2 does not appear
2675    * in s1, s1 is returned unmodified.
2676    *
2677    * Parameters:
2678    *   - 1: Term of sort String (string s1)
2679    *   - 2: Term of sort String (string s2)
2680    *   - 3: Term of sort String (string s3)
2681    *
2682    * Create with:
2683    *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
2684    *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
2685    */
2686   STRING_REPLACE,
2687   /**
2688    * String replace all.
2689    * Replaces all occurrences of a string s2 in a string s1 with string s3.
2690    * If s2 does not appear in s1, s1 is returned unmodified.
2691    *
2692    * Parameters:
2693    *   - 1: Term of sort String (string s1)
2694    *   - 2: Term of sort String (string s2)
2695    *   - 3: Term of sort String (string s3)
2696    *
2697    * Create with:
2698    *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
2699    *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
2700    */
2701   STRING_REPLACE_ALL,
2702   /**
2703    * String replace regular expression match.
2704    * Replaces the first match of a regular expression r in string s1 with
2705    * string s2. If r does not match a substring of s1, s1 is returned
2706    * unmodified.
2707    *
2708    * Parameters:
2709    *   - 1: Term of sort String (string s1)
2710    *   - 2: Term of sort Regexp (regexp r)
2711    *   - 3: Term of sort String (string s2)
2712    *
2713    * Create with:
2714    *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
2715    *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
2716    */
2717   STRING_REPLACE_RE,
2718   /**
2719    * String replace all regular expression matches.
2720    * Replaces all matches of a regular expression r in string s1 with string
2721    * s2. If r does not match a substring of s1, s1 is returned unmodified.
2722    *
2723    * Parameters:
2724    *   - 1: Term of sort String (string s1)
2725    *   - 2: Term of sort Regexp (regexp r)
2726    *   - 3: Term of sort String (string s2)
2727    *
2728    * Create with:
2729    *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
2730    *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
2731    */
2732   STRING_REPLACE_RE_ALL,
2733   /**
2734    * String to lower case.
2735    *
2736    * Parameters:
2737    *   - 1: Term of String sort
2738    *
2739    * Create with:
2740    *   - `Solver::mkTerm(Kind kind, const Term& child) const`
2741    */
2742   STRING_TOLOWER,
2743   /**
2744    * String to upper case.
2745    *
2746    * Parameters:
2747    *   - 1: Term of String sort
2748    *
2749    * Create with:
2750    *   - `Solver::mkTerm(Kind kind, const Term& child) const`
2751    */
2752   STRING_TOUPPER,
2753   /**
2754    * String reverse.
2755    *
2756    * Parameters:
2757    *   - 1: Term of String sort
2758    *
2759    * Create with:
2760    *   - `Solver::mkTerm(Kind kind, const Term& child) const`
2761    */
2762   STRING_REV,
2763   /**
2764    * String to code.
2765    * Returns the code point of a string if it has length one, or returns -1
2766    * otherwise.
2767    *
2768    * Parameters:
2769    *   - 1: Term of String sort
2770    *
2771    * Create with:
2772    *   - `Solver::mkTerm(Kind kind, const Term& child) const`
2773    */
2774   STRING_TO_CODE,
2775   /**
2776    * String from code.
2777    * Returns a string containing a single character whose code point matches
2778    * the argument to this function, or the empty string if the argument is
2779    * out-of-bounds.
2780    *
2781    * Parameters:
2782    *   - 1: Term of Integer sort
2783    *
2784    * Create with:
2785    *   - `Solver::mkTerm(Kind kind, const Term& child) const`
2786    */
2787   STRING_FROM_CODE,
2788   /**
2789    * String less than.
2790    * Returns true if string s1 is (strictly) less than s2 based on a
2791    * lexiographic ordering over code points.
2792    *
2793    * Parameters:
2794    *   - 1: Term of sort String (the string s1)
2795    *   - 2: Term of sort String (the string s2)
2796    *
2797    * Create with:
2798    *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
2799    *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
2800    */
2801   STRING_LT,
2802   /**
2803    * String less than or equal.
2804    * Returns true if string s1 is less than or equal to s2 based on a
2805    * lexiographic ordering over code points.
2806    *
2807    * Parameters:
2808    *   - 1: Term of sort String (the string s1)
2809    *   - 2: Term of sort String (the string s2)
2810    *
2811    * Create with:
2812    *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
2813    *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
2814    */
2815   STRING_LEQ,
2816   /**
2817    * String prefix-of.
2818    * Checks whether a string s1 is a prefix of string s2. If string s1 is
2819    * empty, this operator returns true.
2820    *
2821    * Parameters:
2822    *   - 1: Term of sort String (string s1)
2823    *   - 2: Term of sort String (string s2)
2824    *
2825    * Create with:
2826    *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
2827    *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
2828    */
2829   STRING_PREFIX,
2830   /**
2831    * String suffix-of.
2832    * Checks whether a string s1 is a suffix of string 2. If string s1 is empty,
2833    * this operator returns true.
2834    *
2835    * Parameters:
2836    *   - 1: Term of sort String (string s1)
2837    *   - 2: Term of sort String (string s2)
2838    *
2839    * Create with:
2840    *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
2841    *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
2842    */
2843   STRING_SUFFIX,
2844   /**
2845    * String is-digit.
2846    * Returns true if string s is digit (it is one of "0", ..., "9").
2847    *
2848    * Parameters:
2849    *   - 1: Term of sort String
2850    *
2851    * Create with:
2852    *   - `Solver::mkTerm(Kind kind, const Term& child1) const`
2853    *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
2854    */
2855   STRING_IS_DIGIT,
2856   /**
2857    * Integer to string.
2858    * If the integer is negative this operator returns the empty string.
2859    *
2860    * Parameters:
2861    *   - 1: Term of sort Integer
2862    *
2863    * Create with:
2864    *   - `Solver::mkTerm(Kind kind, const Term& child) const`
2865    */
2866   STRING_FROM_INT,
2867   /**
2868    * String to integer (total function).
2869    * If the string does not contain an integer or the integer is negative, the
2870    * operator returns -1.
2871    *
2872    * Parameters:
2873    *   - 1: Term of sort String
2874    *
2875    * Create with:
2876    *   - `Solver::mkTerm(Kind kind, const Term& child) const`
2877    */
2878   STRING_TO_INT,
2879   /**
2880    * Constant string.
2881    *
2882    * Parameters:
2883    *   - See @ref cvc5::api::Solver::mkString() "mkString()".
2884    *
2885    * Create with:
2886    *   - `Solver::mkString(const std::string& s, bool useEscSequences) const`
2887    *   - `Solver::mkString(const unsigned char c) const`
2888    *   - `Solver::mkString(const std::vector<uint32_t>& s) const`
2889    */
2890   CONST_STRING,
2891   /**
2892    * Conversion from string to regexp.
2893    *
2894    * Parameters:
2895    *   - 1: Term of sort String
2896    *
2897    * Create with:
2898    *   - `Solver::mkTerm(Kind kind, const Term& child) const`
2899    */
2900   STRING_TO_REGEXP,
2901   /**
2902    * Regexp Concatenation.
2903    *
2904    * Parameters:
2905    *   - 1..2: Terms of Regexp sort
2906    *
2907    * Create with:
2908    *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
2909    *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
2910    */
2911   REGEXP_CONCAT,
2912   /**
2913    * Regexp union.
2914    *
2915    * Parameters:
2916    *   - 1..2: Terms of Regexp sort
2917    *
2918    * Create with:
2919    *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
2920    *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
2921    */
2922   REGEXP_UNION,
2923   /**
2924    * Regexp intersection.
2925    *
2926    * Parameters:
2927    *   - 1..2: Terms of Regexp sort
2928    *
2929    * Create with:
2930    *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
2931    *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
2932    */
2933   REGEXP_INTER,
2934   /**
2935    * Regexp difference.
2936    *
2937    * Parameters:
2938    *   - 1..2: Terms of Regexp sort
2939    *
2940    * Create with:
2941    *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
2942    *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
2943    */
2944   REGEXP_DIFF,
2945   /**
2946    * Regexp *.
2947    *
2948    * Parameters:
2949    *   - 1: Term of sort Regexp
2950    *
2951    * Create with:
2952    *   - `Solver::mkTerm(Kind kind, const Term& child) const`
2953    */
2954   REGEXP_STAR,
2955   /**
2956    * Regexp +.
2957    *
2958    * Parameters:
2959    *   - 1: Term of sort Regexp
2960    *
2961    * Create with:
2962    *   - `Solver::mkTerm(Kind kind, const Term& child) const`
2963    */
2964   REGEXP_PLUS,
2965   /**
2966    * Regexp ?.
2967    *
2968    * Parameters:
2969    *   - 1: Term of sort Regexp
2970    *
2971    * Create with:
2972    *   - `Solver::mkTerm(Kind kind, const Term& child) const`
2973    */
2974   REGEXP_OPT,
2975   /**
2976    * Regexp range.
2977    *
2978    * Parameters:
2979    *   - 1: Lower bound character for the range
2980    *   - 2: Upper bound character for the range
2981    *
2982    * Create with:
2983    *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
2984    *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
2985    */
2986   REGEXP_RANGE,
2987   /**
2988    * Operator for regular expression repeat.
2989    *
2990    * Parameters:
2991    *   - 1: The number of repetitions
2992    *
2993    * Create with:
2994    *   - `Solver::mkOp(Kind kind, uint32_t param) const`
2995    *
2996    * Apply regular expression loop.
2997    *
2998    * Parameters:
2999    *   - 1: Op of kind REGEXP_REPEAT
3000    *   - 2: Term of regular expression sort
3001    *
3002    * Create with:
3003    *   - `Solver::mkTerm(const Op& op, const Term& child) const`
3004    *   - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const`
3005    */
3006   REGEXP_REPEAT,
3007   /**
3008    * Operator for regular expression loop, from lower bound to upper bound
3009    * number of repetitions.
3010    *
3011    * Parameters:
3012    *   - 1: The lower bound
3013    *   - 2: The upper bound
3014    *
3015    * Create with:
3016    *   - `Solver::mkOp(Kind kind, uint32_t param, uint32_t param) const`
3017    *
3018    * Apply regular expression loop.
3019    *
3020    * Parameters:
3021    *   - 1: Op of kind REGEXP_LOOP
3022    *   - 2: Term of regular expression sort
3023    *
3024    * Create with:
3025    *   - `Solver::mkTerm(const Op& op, const Term& child) const`
3026    *   - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const`
3027    */
3028   REGEXP_LOOP,
3029   /**
3030    * Regexp none.
3031    *
3032    * Parameters: none
3033    *
3034    * Create with:
3035    *   - `Solver::mkRegexpNone() const`
3036    *   - `Solver::mkTerm(Kind kind) const`
3037    */
3038   REGEXP_NONE,
3039   /**
3040    * Regexp all characters.
3041    *
3042    * Parameters: none
3043    *
3044    * Create with:
3045    *   - `Solver::mkRegexpAllchar() const`
3046    *   - `Solver::mkTerm(Kind kind) const`
3047    */
3048   REGEXP_ALLCHAR,
3049   /**
3050    * Regexp complement.
3051    *
3052    * Parameters:
3053    *   - 1: Term of sort RegExp
3054    *
3055    * Create with:
3056    *   - `Solver::mkTerm(Kind kind, const Term& child1) const`
3057    */
3058   REGEXP_COMPLEMENT,
3059
3060   /**
3061    * Sequence concat.
3062    *
3063    * Parameters: n > 1
3064    *   - 1..n: Terms of Sequence sort
3065    *
3066    * Create with:
3067    *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
3068    *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
3069    *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
3070    */
3071   SEQ_CONCAT,
3072   /**
3073    * Sequence length.
3074    *
3075    * Parameters:
3076    *   - 1: Term of Sequence sort
3077    *
3078    * Create with:
3079    *   - `Solver::mkTerm(Kind kind, const Term& child) const`
3080    */
3081   SEQ_LENGTH,
3082   /**
3083    * Sequence extract.
3084    * Extracts a subsequence, starting at index i and of length l, from a
3085    * sequence s.  If the start index is negative, the start index is greater
3086    * than the length of the sequence, or the length is negative, the result is
3087    * the empty sequence.
3088    *
3089    * Parameters:
3090    *   - 1: Term of sort Sequence
3091    *   - 2: Term of sort Integer (index i)
3092    *   - 3: Term of sort Integer (length l)
3093    *
3094    * Create with:
3095    *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
3096    *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
3097    */
3098   SEQ_EXTRACT,
3099   /**
3100    * Sequence update.
3101    * Updates a sequence s by replacing its context starting at an index with t.
3102    * If the start index is negative, the start index is greater than the
3103    * length of the sequence, the result is s. Otherwise, the length of the
3104    * original sequence is preserved.
3105    *
3106    * Parameters:
3107    *   - 1: Term of sort Sequence
3108    *   - 2: Term of sort Integer (index i)
3109    *   - 3: Term of sort Sequence (replacement sequence t)
3110    *
3111    * Create with:
3112    *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
3113    *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
3114    */
3115   SEQ_UPDATE,
3116   /**
3117    * Sequence element at.
3118    * Returns the element at index i from a sequence s. If the index is negative
3119    * or the index is greater or equal to the length of the sequence, the result
3120    * is the empty sequence. Otherwise the result is a sequence of length 1.
3121    *
3122    * Parameters:
3123    *   - 1: Term of sequence sort (string s)
3124    *   - 2: Term of sort Integer (index i)
3125    *
3126    * Create with:
3127    *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
3128    *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
3129    */
3130   SEQ_AT,
3131   /**
3132    * Sequence contains.
3133    * Checks whether a sequence s1 contains another sequence s2. If s2 is empty,
3134    * the result is always true.
3135    *
3136    * Parameters:
3137    *   - 1: Term of sort Sequence (the sequence s1)
3138    *   - 2: Term of sort Sequence (the sequence s2)
3139    *
3140    * Create with:
3141    *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
3142    *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
3143    */
3144   SEQ_CONTAINS,
3145   /**
3146    * Sequence index-of.
3147    * Returns the index of a subsequence s2 in a sequence s1 starting at index i.
3148    * If the index is negative or greater than the length of sequence s1 or the
3149    * subsequence s2 does not appear in sequence s1 after index i, the result is
3150    * -1.
3151    *
3152    * Parameters:
3153    *   - 1: Term of sort Sequence (subsequence s1)
3154    *   - 2: Term of sort Sequence (subsequence s2)
3155    *   - 3: Term of sort Integer (index i)
3156    *
3157    * Create with:
3158    *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
3159    *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
3160    */
3161   SEQ_INDEXOF,
3162   /**
3163    * Sequence replace.
3164    * Replaces the first occurrence of a sequence s2 in a sequence s1 with
3165    * sequence s3. If s2 does not appear in s1, s1 is returned unmodified.
3166    *
3167    * Parameters:
3168    *   - 1: Term of sort Sequence (sequence s1)
3169    *   - 2: Term of sort Sequence (sequence s2)
3170    *   - 3: Term of sort Sequence (sequence s3)
3171    *
3172    * Create with:
3173    *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
3174    *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
3175    */
3176   SEQ_REPLACE,
3177   /**
3178    * Sequence replace all.
3179    * Replaces all occurrences of a sequence s2 in a sequence s1 with sequence
3180    * s3. If s2 does not appear in s1, s1 is returned unmodified.
3181    *
3182    * Parameters:
3183    *   - 1: Term of sort Sequence (sequence s1)
3184    *   - 2: Term of sort Sequence (sequence s2)
3185    *   - 3: Term of sort Sequence (sequence s3)
3186    *
3187    * Create with:
3188    *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
3189    *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
3190    */
3191   SEQ_REPLACE_ALL,
3192   /**
3193    * Sequence reverse.
3194    *
3195    * Parameters:
3196    *   - 1: Term of Sequence sort
3197    *
3198    * Create with:
3199    *   - `Solver::mkTerm(Kind kind, const Term& child) const`
3200    */
3201   SEQ_REV,
3202   /**
3203    * Sequence prefix-of.
3204    * Checks whether a sequence s1 is a prefix of sequence s2. If sequence s1 is
3205    * empty, this operator returns true.
3206    *
3207    * Parameters:
3208    *   - 1: Term of sort Sequence (sequence s1)
3209    *   - 2: Term of sort Sequence (sequence s2)
3210    *
3211    * Create with:
3212    *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
3213    *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
3214    */
3215   SEQ_PREFIX,
3216   /**
3217    * Sequence suffix-of.
3218    * Checks whether a sequence s1 is a suffix of sequence s2. If sequence s1 is
3219    * empty, this operator returns true.
3220    *
3221    * Parameters:
3222    *   - 1: Term of sort Sequence (sequence s1)
3223    *   - 2: Term of sort Sequence (sequence s2)
3224    *
3225    * Create with:
3226    *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
3227    *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
3228    */
3229   SEQ_SUFFIX,
3230   /**
3231    * Constant sequence.
3232    *
3233    * Parameters:
3234    *   - See @ref cvc5::api::Solver::mkEmptySequence() "mkEmptySequence()".
3235    *
3236    * Create with:
3237    *   - `Solver::mkEmptySequence(const Sort& sort) const`
3238    *
3239    * Note that a constant sequence is a term that is equivalent to:
3240    *
3241    *     (seq.++ (seq.unit c1) ... (seq.unit cn))
3242    *
3243    * where n>=0 and c1, ..., cn are constants of some sort. The elements
3244    * can be extracted by `Term::getSequenceValue()`.
3245    */
3246   CONST_SEQUENCE,
3247   /**
3248    * Sequence unit, corresponding to a sequence of length one with the given
3249    * term.
3250    *
3251    * Parameters:
3252    *   - 1: Element term.
3253    *
3254    * Create with:
3255    *   - `Solver::mkTerm(Kind kind, const Term& child1) const`
3256    */
3257   SEQ_UNIT,
3258   /**
3259    * Sequence nth, corresponding to the nth element of a sequence.
3260    *
3261    * Parameters:
3262    *   - 1: Sequence term.
3263    *   - 2: Integer term.
3264    *
3265    * Create with:
3266    *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
3267    */
3268   SEQ_NTH,
3269
3270   /* Quantifiers ----------------------------------------------------------- */
3271
3272   /**
3273    * Universally quantified formula.
3274    *
3275    * Parameters:
3276    *   - 1: VARIABLE_LIST Term
3277    *   - 2: Quantifier body
3278    *   - 3: (optional) INST_PATTERN_LIST Term
3279    *
3280    * Create with:
3281    *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
3282    *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
3283    *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
3284    */
3285   FORALL,
3286   /**
3287    * Existentially quantified formula.
3288    *
3289    * Parameters:
3290    *   - 1: VARIABLE_LIST Term
3291    *   - 2: Quantifier body
3292    *   - 3: (optional) INST_PATTERN_LIST Term
3293    *
3294    * Create with:
3295    *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
3296    *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
3297    *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
3298    */
3299   EXISTS,
3300   /**
3301    * A list of variables (used to bind variables under a quantifier)
3302    *
3303    * Parameters: n > 1
3304    *   - 1..n: Terms with kind VARIABLE
3305    *
3306    * Create with:
3307    *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
3308    *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
3309    *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
3310    */
3311   VARIABLE_LIST,
3312   /**
3313    * An instantiation pattern.
3314    * Specifies a (list of) terms to be used as a pattern for quantifier
3315    * instantiation.
3316    *
3317    * Parameters: n > 1
3318    *   - 1..n: Terms of any sort
3319    *
3320    * Create with:
3321    *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
3322    *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
3323    *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
3324    */
3325   INST_PATTERN,
3326   /**
3327    * An instantiation no-pattern.
3328    * Specifies a (list of) terms that should not be used as a pattern for
3329    * quantifier instantiation.
3330    *
3331    * Parameters: n > 1
3332    *   - 1..n: Terms of any sort
3333    *
3334    * Create with:
3335    *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
3336    *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
3337    *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
3338    */
3339   INST_NO_PATTERN,
3340   /*
3341    * An instantiation pool.
3342    * Specifies an annotation for pool based instantiation.
3343    * Parameters: n > 1
3344    *   - 1..n: Terms that comprise the pools, which are one-to-one with
3345    * the variables of the quantified formula to be instantiated.
3346    * Create with:
3347    *   - `mkTerm(Kind kind, Term child1, Term child2)
3348    *   - `mkTerm(Kind kind, Term child1, Term child2, Term child3)
3349    *   - `mkTerm(Kind kind, const std::vector<Term>& children)
3350    */
3351   INST_POOL,
3352   /*
3353    * A instantantiation-add-to-pool annotation.
3354    * Parameters: n = 1
3355    *   - 1: The pool to add to.
3356    * Create with:
3357    *   - `mkTerm(Kind kind, Term child)
3358    */
3359   INST_ADD_TO_POOL,
3360   /*
3361    * A skolemization-add-to-pool annotation.
3362    * Parameters: n = 1
3363    *   - 1: The pool to add to.
3364    * Create with:
3365    *   - `mkTerm(Kind kind, Term child)
3366    */
3367   SKOLEM_ADD_TO_POOL,
3368   /**
3369    * An instantiation attribute
3370    * Specifies a custom property for a quantified formula given by a
3371    * term that is ascribed a user attribute.
3372    *
3373    * Parameters: n >= 1
3374    *   - 1: The keyword of the attribute (a term with kind CONST_STRING).
3375    *   - 2...n: The values of the attribute.
3376    *
3377    * Create with:
3378    *   - `mkTerm(Kind kind, Term child1, Term child2)
3379    *   - `mkTerm(Kind kind, Term child1, Term child2, Term child3)
3380    *   - `mkTerm(Kind kind, const std::vector<Term>& children)
3381    */
3382   INST_ATTRIBUTE,
3383   /**
3384    * A list of instantiation patterns and/or attributes.
3385    *
3386    * Parameters: n > 1
3387    *   - 1..n: Terms with kind INST_PATTERN, INST_NO_PATTERN, or
3388    * INST_ATTRIBUTE.
3389    *
3390    * Create with:
3391    *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
3392    *   - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const`
3393    *   - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
3394    */
3395   INST_PATTERN_LIST,
3396 #if 0
3397
3398   /* Sort Kinds ------------------------------------------------------------ */
3399
3400   /* array type */
3401    ARRAY_TYPE,
3402   /* a type parameter for type ascription */
3403   ASCRIPTION_TYPE,
3404   /* constructor */
3405   CONSTRUCTOR_TYPE,
3406   /* a datatype type index */
3407   DATATYPE_TYPE,
3408   /* selector */
3409   SELECTOR_TYPE,
3410   /* set type, takes as parameter the type of the elements */
3411   SET_TYPE,
3412   /* bag type, takes as parameter the type of the elements */
3413   BAG_TYPE,
3414   /* sort tag */
3415   SORT_TAG,
3416   /* specifies types of user-declared 'uninterpreted' sorts */
3417   SORT_TYPE,
3418   /* tester */
3419   TESTER_TYPE,
3420   /* a representation for basic types */
3421   TYPE_CONSTANT,
3422   /* a function type */
3423   FUNCTION_TYPE,
3424   /* the type of a symbolic expression */
3425   SEXPR_TYPE,
3426   /* bit-vector type */
3427   BITVECTOR_TYPE,
3428   /* floating-point type */
3429   FLOATINGPOINT_TYPE,
3430 #endif
3431
3432   /* ----------------------------------------------------------------------- */
3433   /** Marks the upper-bound of this enumeration. */
3434   LAST_KIND
3435 };
3436 // clang-format on
3437
3438 /**
3439  * Get the string representation of a given kind.
3440  * @param k the kind
3441  * @return the string representation of kind k
3442  */
3443 std::string kindToString(Kind k) CVC5_EXPORT;
3444
3445 /**
3446  * Serialize a kind to given stream.
3447  * @param out the output stream
3448  * @param k the kind to be serialized to the given output stream
3449  * @return the output stream
3450  */
3451 std::ostream& operator<<(std::ostream& out, Kind k) CVC5_EXPORT;
3452
3453 }  // namespace api
3454 }  // namespace cvc5
3455
3456 namespace std {
3457
3458 /**
3459  * Hash function for Kinds.
3460  */
3461 template<>
3462 struct CVC5_EXPORT hash<cvc5::api::Kind>
3463 {
3464   /**
3465    * Hashes a Kind to a size_t.
3466    */
3467   size_t operator()(cvc5::api::Kind k) const;
3468 };
3469
3470 }
3471
3472 #endif