src/api/cvc4cppkind.h

   1 /*********************                                                        */
   2 /*! \file cvc4cppkind.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Aina Niemetz
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
   8  ** in the top-level source directory) and their institutional affiliations.
   9  ** All rights reserved.  See the file COPYING in the top-level source
  10  ** directory for licensing information.\endverbatim
  11  **
  12  ** \brief The term kinds of the CVC4 C++ API.
  13  **
  14  ** The term kinds of the CVC4 C++ API.
  15  **/
  16
  17 #include "cvc4_public.h"
  18
  19 #ifndef CVC4__API__CVC4CPPKIND_H
  20 #define CVC4__API__CVC4CPPKIND_H
  21
  22 #include <ostream>
  23
  24 namespace CVC4 {
  25 namespace api {
  26
  27 /* -------------------------------------------------------------------------- */
  28 /* Kind                                                                       */
  29 /* -------------------------------------------------------------------------- */
  30
  31 /**
  32  * The kind of a CVC4 term.
  33  *
  34  * Note that the underlying type of Kind must be signed (to enable range
  35  * checks for validity). The size of this type depends on the size of
  36  * CVC4::Kind (CVC4__EXPR__NODE_VALUE__NBITS__KIND, currently 10 bits,
  37  * see expr/metakind_template.h).
  38  */
  39 enum CVC4_PUBLIC Kind : int32_t
  40 {
  41   /**
  42    * Internal kind.
  43    * Should never be exposed or created via the API.
  44    */
  45   INTERNAL_KIND = -2,
  46   /**
  47    * Undefined kind.
  48    * Should never be exposed or created via the API.
  49    */
  50   UNDEFINED_KIND = -1,
  51   /**
  52    * Null kind (kind of null term Term()).
  53    * Do not explicitly create via API functions other than Term().
  54    */
  55   NULL_EXPR,
  56
  57   /* Builtin --------------------------------------------------------------- */
  58
  59   /**
  60    * Uninterpreted constant.
  61    * Parameters: 2
  62    *   -[1]: Sort of the constant
  63    *   -[2]: Index of the constant
  64    * Create with:
  65    *   mkUninterpretedConst(Sort sort, int32_t index)
  66    */
  67   UNINTERPRETED_CONSTANT,
  68   /**
  69    * Abstract value (other than uninterpreted sort constants).
  70    * Parameters: 1
  71    *   -[1]: Index of the abstract value
  72    * Create with:
  73    *   mkAbstractValue(const std::string& index);
  74    *   mkAbstractValue(uint64_t index);
  75    */
  76   ABSTRACT_VALUE,
  77 #if 0
  78   /* Built-in operator */
  79   BUILTIN,
  80 #endif
  81   /**
  82    * Equality.
  83    * Parameters: 2
  84    *   -[1]..[2]: Terms with same sort
  85    * Create with:
  86    *   mkTerm(Kind kind, Term child1, Term child2)
  87    *   mkTerm(Kind kind, const std::vector<Term>& children)
  88    */
  89   EQUAL,
  90   /**
  91    * Disequality.
  92    * Parameters: n > 1
  93    *   -[1]..[n]: Terms with same sort
  94    * Create with:
  95    *   mkTerm(Kind kind, Term child1, Term child2)
  96    *   mkTerm(Kind kind, Term child1, Term child2, Term child3)
  97    *   mkTerm(Kind kind, const std::vector<Term>& children)
  98    */
  99   DISTINCT,
 100   /**
 101    * First-order constant.
 102    * Not permitted in bindings (forall, exists, ...).
 103    * Parameters:
 104    *   See mkConst().
 105    * Create with:
 106    *   mkConst(const std::string& symbol, Sort sort)
 107    *   mkConst(Sort sort)
 108    */
 109   CONSTANT,
 110   /**
 111    * (Bound) variable.
 112    * Permitted in bindings and in the lambda and quantifier bodies only.
 113    * Parameters:
 114    *   See mkVar().
 115    * Create with:
 116    *   mkVar(const std::string& symbol, Sort sort)
 117    *   mkVar(Sort sort)
 118    */
 119   VARIABLE,
 120 #if 0
 121   /* Skolem variable (internal only) */
 122   SKOLEM,
 123   /* Symbolic expression (any arity) */
 124   SEXPR,
 125 #endif
 126   /**
 127    * Lambda expression.
 128    * Parameters: 2
 129    *   -[1]: BOUND_VAR_LIST
 130    *   -[2]: Lambda body
 131    * Create with:
 132    *   mkTerm(Kind kind, Term child1, Term child2)
 133    *   mkTerm(Kind kind, const std::vector<Term>& children)
 134    */
 135   LAMBDA,
 136   /**
 137    * Hilbert choice (epsilon) expression.
 138    * Parameters: 2
 139    *   -[1]: BOUND_VAR_LIST
 140    *   -[2]: Hilbert choice body
 141    * Create with:
 142    *   mkTerm(Kind kind, Term child1, Term child2)
 143    *   mkTerm(Kind kind, const std::vector<Term>& children)
 144    */
 145   CHOICE,
 146   /**
 147    * Chained operation.
 148    * Parameters: n > 1
 149    *   -[1]: Term of kind CHAIN_OP (represents a binary op)
 150    *   -[2]..[n]: Arguments to that operator
 151    * Create with:
 152    *   mkTerm(Kind kind, Term child1, Term child2)
 153    *   mkTerm(Kind kind, Term child1, Term child2, Term child3)
 154    *   mkTerm(Kind kind, const std::vector<Term>& children)
 155    * Turned into a conjunction of binary applications of the operator on
 156    * adjoining parameters.
 157    */
 158   CHAIN,
 159   /**
 160    * Chained operator.
 161    * Parameters: 1
 162    *   -[1]: Kind of the binary operation
 163    * Create with:
 164    *   mkOpTerm(Kind opkind, Kind kind)
 165    */
 166   CHAIN_OP,
 167
 168   /* Boolean --------------------------------------------------------------- */
 169
 170   /**
 171    * Boolean constant.
 172    * Parameters: 1
 173    *   -[1]: Boolean value of the constant
 174    * Create with:
 175    *   mkTrue()
 176    *   mkFalse()
 177    *   mkBoolean(bool val)
 178    */
 179   CONST_BOOLEAN,
 180   /* Logical not.
 181    * Parameters: 1
 182    *   -[1]: Boolean Term to negate
 183    * Create with:
 184    *   mkTerm(Kind kind, Term child)
 185    */
 186   NOT,
 187   /* Logical and.
 188    * Parameters: n > 1
 189    *   -[1]..[n]: Boolean Term of the conjunction
 190    * Create with:
 191    *   mkTerm(Kind kind, Term child1, Term child2)
 192    *   mkTerm(Kind kind, Term child1, Term child2, Term child3)
 193    *   mkTerm(Kind kind, const std::vector<Term>& children)
 194    */
 195   AND,
 196   /**
 197    * Logical implication.
 198    * Parameters: 2
 199    *   -[1]..[2]: Boolean Terms, [1] implies [2]
 200    * Create with:
 201    *   mkTerm(Kind kind, Term child1, Term child2)
 202    *   mkTerm(Kind kind, const std::vector<Term>& children)
 203    */
 204   IMPLIES,
 205   /* Logical or.
 206    * Parameters: n > 1
 207    *   -[1]..[n]: Boolean Term of the disjunction
 208    * Create with:
 209    *   mkTerm(Kind kind, Term child1, Term child2)
 210    *   mkTerm(Kind kind, Term child1, Term child2, Term child3)
 211    *   mkTerm(Kind kind, const std::vector<Term>& children)
 212    */
 213   OR,
 214   /* Logical exclusive or.
 215    * Parameters: 2
 216    *   -[1]..[2]: Boolean Terms, [1] xor [2]
 217    * Create with:
 218    *   mkTerm(Kind kind, Term child1, Term child2)
 219    *   mkTerm(Kind kind, const std::vector<Term>& children)
 220    */
 221   XOR,
 222   /* If-then-else.
 223    * Parameters: 3
 224    *   -[1] is a Boolean condition Term
 225    *   -[2] the 'then' Term
 226    *   -[3] the 'else' Term
 227    * 'then' and 'else' term must have same base sort.
 228    * Create with:
 229    *   mkTerm(Kind kind, Term child1, Term child2, Term child3)
 230    *   mkTerm(Kind kind, const std::vector<Term>& children)
 231    */
 232   ITE,
 233
 234   /* UF -------------------------------------------------------------------- */
 235
 236   /* Application of an uninterpreted function.
 237    * Parameters: n > 1
 238    *   -[1]: Function Term
 239    *   -[2]..[n]: Function argument instantiation Terms
 240    * Create with:
 241    *   mkTerm(Kind kind, Term child1, Term child2)
 242    *   mkTerm(Kind kind, Term child1, Term child2, Term child3)
 243    *   mkTerm(Kind kind, const std::vector<Term>& children)
 244    */
 245   APPLY_UF,
 246 #if 0
 247   /* Boolean term variable */
 248   BOOLEAN_TERM_VARIABLE,
 249 #endif
 250   /**
 251    * Cardinality constraint on sort S.
 252    * Parameters: 2
 253    *   -[1]: Term of sort S
 254    *   -[2]: Positive integer constant that bounds the cardinality of sort S
 255    * Create with:
 256    *   mkTerm(Kind kind, Term child1, Term child2)
 257    *   mkTerm(Kind kind, const std::vector<Term>& children)
 258    */
 259   CARDINALITY_CONSTRAINT,
 260 #if 0
 261   /* Combined cardinality constraint.  */
 262   COMBINED_CARDINALITY_CONSTRAINT,
 263   /* Partial uninterpreted function application.  */
 264   PARTIAL_APPLY_UF,
 265   /* cardinality value of sort S:
 266    * first parameter is (any) term of sort S */
 267    CARDINALITY_VALUE,
 268 #endif
 269   /**
 270    * Higher-order applicative encoding of function application.
 271    * Parameters: 2
 272    *   -[1]: Function to apply
 273    *   -[2]: Argument of the function
 274    * Create with:
 275    *   mkTerm(Kind kind, Term child1, Term child2)
 276    *   mkTerm(Kind kind, const std::vector<Term>& children)
 277    */
 278   HO_APPLY,
 279
 280   /* Arithmetic ------------------------------------------------------------ */
 281
 282   /**
 283    * Arithmetic addition.
 284    * Parameters: n > 1
 285    *   -[1]..[n]: Terms of sort Integer, Real (sorts must match)
 286    * Create with:
 287    *   mkTerm(Kind kind, Term child1, Term child2)
 288    *   mkTerm(Kind kind, Term child1, Term child2, Term child3)
 289    *   mkTerm(Kind kind, const std::vector<Term>& children)
 290    */
 291   PLUS,
 292   /**
 293    * Arithmetic multiplication.
 294    * Parameters: n > 1
 295    *   -[1]..[n]: Terms of sort Integer, Real (sorts must match)
 296    * Create with:
 297    *   mkTerm(Kind kind, Term child1, Term child2)
 298    *   mkTerm(Kind kind, Term child1, Term child2, Term child3)
 299    *   mkTerm(Kind kind, const std::vector<Term>& children)
 300    */
 301   MULT,
 302 #if 0
 303   /* Synonym for MULT.  */
 304   NONLINEAR_MULT,
 305 #endif
 306   /**
 307    * Arithmetic subtraction.
 308    * Parameters: 2
 309    *   -[1]..[2]: Terms of sort Integer, Real (sorts must match)
 310    * Create with:
 311    *   mkTerm(Kind kind, Term child1, Term child2)
 312    *   mkTerm(Kind kind, const std::vector<Term>& children)
 313    */
 314   MINUS,
 315   /**
 316    * Arithmetic negation.
 317    * Parameters: 1
 318    *   -[1]: Term of sort Integer, Real
 319    * Create with:
 320    *   mkTerm(Kind kind, Term child)
 321    */
 322   UMINUS,
 323   /**
 324    * Real division, division by 0 undefined
 325    * Parameters: 2
 326    *   -[1]..[2]: Terms of sort Integer, Real
 327    * Create with:
 328    *   mkTerm(Kind kind, Term child1, Term child2)
 329    *   mkTerm(Kind kind, const std::vector<Term>& children)
 330    */
 331   DIVISION,
 332   /**
 333    * Real division with interpreted division by 0
 334    * Parameters: 2
 335    *   -[1]..[2]: Terms of sort Integer, Real
 336    * Create with:
 337    *   mkTerm(Kind kind, Term child1, Term child2)
 338    *   mkTerm(Kind kind, const std::vector<Term>& children)
 339    */
 340   DIVISION_TOTAL,
 341   /**
 342    * Integer division, division by 0 undefined.
 343    * Parameters: 2
 344    *   -[1]..[2]: Terms of sort Integer
 345    * Create with:
 346    *   mkTerm(Kind kind, Term child1, Term child2)
 347    *   mkTerm(Kind kind, const std::vector<Term>& children)
 348    */
 349   INTS_DIVISION,
 350   /**
 351    * Integer division with interpreted division by 0.
 352    * Parameters: 2
 353    *   -[1]..[2]: Terms of sort Integer
 354    * Create with:
 355    *   mkTerm(Kind kind, Term child1, Term child2)
 356    *   mkTerm(Kind kind, const std::vector<Term>& children)
 357    */
 358   INTS_DIVISION_TOTAL,
 359   /**
 360    * Integer modulus, division by 0 undefined.
 361    * Parameters: 2
 362    *   -[1]..[2]: Terms of sort Integer
 363    * Create with:
 364    *   mkTerm(Kind kind, Term child1, Term child2)
 365    *   mkTerm(Kind kind, const std::vector<Term>& children)
 366    */
 367   INTS_MODULUS,
 368   /**
 369    * Integer modulus with interpreted division by 0.
 370    * Parameters: 2
 371    *   -[1]..[2]: Terms of sort Integer
 372    * Create with:
 373    *   mkTerm(Kind kind, Term child1, Term child2)
 374    *   mkTerm(Kind kind, const std::vector<Term>& children)
 375    */
 376   INTS_MODULUS_TOTAL,
 377   /**
 378    * Absolute value.
 379    * Parameters: 1
 380    *   -[1]: Term of sort Integer
 381    * Create with:
 382    *   mkTerm(Kind kind, Term child)
 383    */
 384   ABS,
 385   /**
 386    * Divisibility-by-k predicate.
 387    * Parameters: 2
 388    *   -[1]: DIVISIBLE_OP Term
 389    *   -[2]: Integer Term
 390    * Create with:
 391    *   mkTerm(Kind kind, Term child1, Term child2)
 392    *   mkTerm(Kind kind, const std::vector<Term>& children)
 393    */
 394   DIVISIBLE,
 395   /**
 396    * Arithmetic power.
 397    * Parameters: 2
 398    *   -[1]..[2]: Terms of sort Integer, Real
 399    * Create with:
 400    *   mkTerm(Kind kind, Term child1, Term child2)
 401    *   mkTerm(Kind kind, const std::vector<Term>& children)
 402    */
 403   POW,
 404   /**
 405    * Exponential.
 406    * Parameters: 1
 407    *   -[1]: Term of sort Integer, Real
 408    * Create with:
 409    *   mkTerm(Kind kind, Term child)
 410    */
 411   EXPONENTIAL,
 412   /**
 413    * Sine.
 414    * Parameters: 1
 415    *   -[1]: Term of sort Integer, Real
 416    * Create with:
 417    *   mkTerm(Kind kind, Term child)
 418    */
 419   SINE,
 420   /**
 421    * Cosine.
 422    * Parameters: 1
 423    *   -[1]: Term of sort Integer, Real
 424    * Create with:
 425    *   mkTerm(Kind kind, Term child)
 426    */
 427   COSINE,
 428   /**
 429    * Tangent.
 430    * Parameters: 1
 431    *   -[1]: Term of sort Integer, Real
 432    * Create with:
 433    *   mkTerm(Kind kind, Term child)
 434    */
 435   TANGENT,
 436   /**
 437    * Cosecant.
 438    * Parameters: 1
 439    *   -[1]: Term of sort Integer, Real
 440    * Create with:
 441    *   mkTerm(Kind kind, Term child)
 442    */
 443   COSECANT,
 444   /**
 445    * Secant.
 446    * Parameters: 1
 447    *   -[1]: Term of sort Integer, Real
 448    * Create with:
 449    *   mkTerm(Kind kind, Term child)
 450    */
 451   SECANT,
 452   /**
 453    * Cotangent.
 454    * Parameters: 1
 455    *   -[1]: Term of sort Integer, Real
 456    * Create with:
 457    *   mkTerm(Kind kind, Term child)
 458    */
 459   COTANGENT,
 460   /**
 461    * Arc sine.
 462    * Parameters: 1
 463    *   -[1]: Term of sort Integer, Real
 464    * Create with:
 465    *   mkTerm(Kind kind, Term child)
 466    */
 467   ARCSINE,
 468   /**
 469    * Arc cosine.
 470    * Parameters: 1
 471    *   -[1]: Term of sort Integer, Real
 472    * Create with:
 473    *   mkTerm(Kind kind, Term child)
 474    */
 475   ARCCOSINE,
 476   /**
 477    * Arc tangent.
 478    * Parameters: 1
 479    *   -[1]: Term of sort Integer, Real
 480    * Create with:
 481    *   mkTerm(Kind kind, Term child)
 482    */
 483   ARCTANGENT,
 484   /**
 485    * Arc cosecant.
 486    * Parameters: 1
 487    *   -[1]: Term of sort Integer, Real
 488    * Create with:
 489    *   mkTerm(Kind kind, Term child)
 490    */
 491   ARCCOSECANT,
 492   /**
 493    * Arc secant.
 494    * Parameters: 1
 495    *   -[1]: Term of sort Integer, Real
 496    * Create with:
 497    *   mkTerm(Kind kind, Term child)
 498    */
 499   ARCSECANT,
 500   /**
 501    * Arc cotangent.
 502    * Parameters: 1
 503    *   -[1]: Term of sort Integer, Real
 504    * Create with:
 505    *   mkTerm(Kind kind, Term child)
 506    */
 507   ARCCOTANGENT,
 508   /**
 509    * Square root.
 510    * Parameters: 1
 511    *   -[1]: Term of sort Integer, Real
 512    * Create with:
 513    *   mkTerm(Kind kind, Term child)
 514    */
 515   SQRT,
 516   /**
 517    * Operator for the divisibility-by-k predicate.
 518    * Parameter: 1
 519    *   -[1]: The k to divide by (sort Integer)
 520    * Create with:
 521    *   mkOpTerm(Kind kind, uint32_t param)
 522    */
 523   DIVISIBLE_OP,
 524   /**
 525    * Multiple-precision rational constant.
 526    * Parameters:
 527    *   See mkInteger(), mkReal(), mkRational()
 528    * Create with:
 529    *   mkInteger(const char* s, uint32_t base = 10)
 530    *   mkInteger(const std::string& s, uint32_t base = 10)
 531    *   mkInteger(int32_t val)
 532    *   mkInteger(uint32_t val)
 533    *   mkInteger(int64_t val)
 534    *   mkInteger(uint64_t val)
 535    *   mkReal(const char* s, uint32_t base = 10)
 536    *   mkReal(const std::string& s, uint32_t base = 10)
 537    *   mkReal(int32_t val)
 538    *   mkReal(int64_t val)
 539    *   mkReal(uint32_t val)
 540    *   mkReal(uint64_t val)
 541    *   mkReal(int32_t num, int32_t den)
 542    *   mkReal(int64_t num, int64_t den)
 543    *   mkReal(uint32_t num, uint32_t den)
 544    *   mkReal(uint64_t num, uint64_t den)
 545    */
 546   CONST_RATIONAL,
 547   /**
 548    * Less than.
 549    * Parameters: 2
 550    *   -[1]..[2]: Terms of sort Integer, Real; [1] < [2]
 551    * Create with:
 552    *   mkTerm(Kind kind, Term child1, Term child2)
 553    *   mkTerm(Kind kind, const std::vector<Term>& children)
 554    */
 555   LT,
 556   /**
 557    * Less than or equal.
 558    * Parameters: 2
 559    *   -[1]..[2]: Terms of sort Integer, Real; [1] <= [2]
 560    * Create with:
 561    *   mkTerm(Kind kind, Term child1, Term child2)
 562    *   mkTerm(Kind kind, const std::vector<Term>& children)
 563    */
 564   LEQ,
 565   /**
 566    * Greater than.
 567    * Parameters: 2
 568    *   -[1]..[2]: Terms of sort Integer, Real, [1] > [2]
 569    * Create with:
 570    *   mkTerm(Kind kind, Term child1, Term child2)
 571    *   mkTerm(Kind kind, const std::vector<Term>& children)
 572    */
 573   GT,
 574   /**
 575    * Greater than or equal.
 576    * Parameters: 2
 577    *   -[1]..[2]: Terms of sort Integer, Real; [1] >= [2]
 578    * Create with:
 579    *   mkTerm(Kind kind, Term child1, Term child2)
 580    *   mkTerm(Kind kind, const std::vector<Term>& children)
 581    */
 582   GEQ,
 583   /**
 584    * Is-integer predicate.
 585    * Parameters: 1
 586    *   -[1]: Term of sort Integer, Real
 587    * Create with:
 588    *   mkTerm(Kind kind, Term child)
 589    */
 590   IS_INTEGER,
 591   /**
 592    * Convert Term to Integer by the floor function.
 593    * Parameters: 1
 594    *   -[1]: Term of sort Integer, Real
 595    * Create with:
 596    *   mkTerm(Kind kind, Term child)
 597    */
 598   TO_INTEGER,
 599   /**
 600    * Convert Term to Real.
 601    * Parameters: 1
 602    *   -[1]: Term of sort Integer, Real
 603    * This is a no-op in CVC4, as Integer is a subtype of Real.
 604    */
 605   TO_REAL,
 606   /**
 607    * Pi constant.
 608    * Create with:
 609    *   mkPi()
 610    *   mkTerm(Kind kind)
 611    */
 612   PI,
 613
 614   /* BV -------------------------------------------------------------------- */
 615
 616   /**
 617    * Fixed-size bit-vector constant.
 618    * Parameters:
 619    *   See mkBitVector().
 620    * Create with:
 621    *   mkBitVector(uint32_t size, uint64_t val)
 622    *   mkBitVector(const char* s, uint32_t base = 2)
 623    *   mkBitVector(std::string& s, uint32_t base = 2)
 624    */
 625   CONST_BITVECTOR,
 626   /**
 627    * Concatenation of two or more bit-vectors.
 628    * Parameters: n > 1
 629    *   -[1]..[n]: Terms of bit-vector sort
 630    * Create with:
 631    *   mkTerm(Kind kind, Term child1, Term child2)
 632    *   mkTerm(Kind kind, Term child1, Term child2, Term child3)
 633    *   mkTerm(Kind kind, const std::vector<Term>& children)
 634    */
 635   BITVECTOR_CONCAT,
 636   /**
 637    * Bit-wise and.
 638    * Parameters: n > 1
 639    *   -[1]..[n]: Terms of bit-vector sort (sorts must match)
 640    * Create with:
 641    *   mkTerm(Kind kind, Term child1, Term child2)
 642    *   mkTerm(Kind kind, Term child1, Term child2, Term child3)
 643    *   mkTerm(Kind kind, const std::vector<Term>& children)
 644    */
 645   BITVECTOR_AND,
 646   /**
 647    * Bit-wise or.
 648    * Parameters: n > 1
 649    *   -[1]..[n]: Terms of bit-vector sort (sorts must match)
 650    * Create with:
 651    *   mkTerm(Kind kind, Term child1, Term child2)
 652    *   mkTerm(Kind kind, Term child1, Term child2, Term child3)
 653    *   mkTerm(Kind kind, const std::vector<Term>& children)
 654    */
 655   BITVECTOR_OR,
 656   /**
 657    * Bit-wise xor.
 658    * Parameters: n > 1
 659    *   -[1]..[n]: Terms of bit-vector sort (sorts must match)
 660    * Create with:
 661    *   mkTerm(Kind kind, Term child1, Term child2)
 662    *   mkTerm(Kind kind, Term child1, Term child2, Term child3)
 663    *   mkTerm(Kind kind, const std::vector<Term>& children)
 664    */
 665   BITVECTOR_XOR,
 666   /**
 667    * Bit-wise negation.
 668    * Parameters: 1
 669    *   -[1]: Term of bit-vector sort
 670    * Create with:
 671    *   mkTerm(Kind kind, Term child)
 672    */
 673   BITVECTOR_NOT,
 674   /**
 675    * Bit-wise nand.
 676    * Parameters: 2
 677    *   -[1]..[2]: Terms of bit-vector sort (sorts must match)
 678    * Create with:
 679    *   mkTerm(Kind kind, Term child1, Term child2)
 680    *   mkTerm(Kind kind, const std::vector<Term>& children)
 681    */
 682   BITVECTOR_NAND,
 683   /**
 684    * Bit-wise nor.
 685    * Parameters: 2
 686    *   -[1]..[2]: Terms of bit-vector sort (sorts must match)
 687    * Create with:
 688    *   mkTerm(Kind kind, Term child1, Term child2)
 689    *   mkTerm(Kind kind, const std::vector<Term>& children)
 690    */
 691   BITVECTOR_NOR,
 692   /**
 693    * Bit-wise xnor.
 694    * Parameters: 2
 695    *   -[1]..[2]: Terms of bit-vector sort (sorts must match)
 696    * Create with:
 697    *   mkTerm(Kind kind, Term child1, Term child2)
 698    *   mkTerm(Kind kind, const std::vector<Term>& children)
 699    */
 700   BITVECTOR_XNOR,
 701   /**
 702    * Equality comparison (returns bit-vector of size 1).
 703    * Parameters: 2
 704    *   -[1]..[2]: Terms of bit-vector sort (sorts must match)
 705    * Create with:
 706    *   mkTerm(Kind kind, Term child1, Term child2)
 707    *   mkTerm(Kind kind, const std::vector<Term>& children)
 708    */
 709   BITVECTOR_COMP,
 710   /**
 711    * Multiplication of two or more bit-vectors.
 712    * Parameters: n > 1
 713    *   -[1]..[n]: Terms of bit-vector sort (sorts must match)
 714    * Create with:
 715    *   mkTerm(Kind kind, Term child1, Term child2)
 716    *   mkTerm(Kind kind, Term child1, Term child2, Term child3)
 717    *   mkTerm(Kind kind, const std::vector<Term>& children)
 718    */
 719   BITVECTOR_MULT,
 720   /**
 721    * Addition of two or more bit-vectors.
 722    * Parameters: n > 1
 723    *   -[1]..[n]: Terms of bit-vector sort (sorts must match)
 724    * Create with:
 725    *   mkTerm(Kind kind, Term child1, Term child2)
 726    *   mkTerm(Kind kind, Term child1, Term child2, Term child3)
 727    *   mkTerm(Kind kind, const std::vector<Term>& children)
 728    */
 729   BITVECTOR_PLUS,
 730   /**
 731    * Subtraction of two bit-vectors.
 732    * Parameters: 2
 733    *   -[1]..[2]: Terms of bit-vector sort (sorts must match)
 734    * Create with:
 735    *   mkTerm(Kind kind, Term child1, Term child2)
 736    *   mkTerm(Kind kind, const std::vector<Term>& children)
 737    */
 738   BITVECTOR_SUB,
 739   /**
 740    * Negation of a bit-vector (two's complement).
 741    * Parameters: 1
 742    *   -[1]: Term of bit-vector sort
 743    * Create with:
 744    *   mkTerm(Kind kind, Term child)
 745    */
 746   BITVECTOR_NEG,
 747   /**
 748    * Unsigned division of two bit-vectors, truncating towards 0.
 749    * Parameters: 2
 750    *   -[1]..[2]: Terms of bit-vector sort (sorts must match)
 751    * Create with:
 752    *   mkTerm(Kind kind, Term child1, Term child2)
 753    *   mkTerm(Kind kind, const std::vector<Term>& children)
 754    */
 755   BITVECTOR_UDIV,
 756   /**
 757    * Unsigned remainder from truncating division of two bit-vectors.
 758    * Parameters: 2
 759    *   -[1]..[2]: Terms of bit-vector sort (sorts must match)
 760    * Create with:
 761    *   mkTerm(Kind kind, Term child1, Term child2)
 762    *   mkTerm(Kind kind, const std::vector<Term>& children)
 763    */
 764   BITVECTOR_UREM,
 765   /**
 766    * Two's complement signed division of two bit-vectors.
 767    * Parameters: 2
 768    *   -[1]..[2]: Terms of bit-vector sort (sorts must match)
 769    * Create with:
 770    *   mkTerm(Kind kind, Term child1, Term child2)
 771    *   mkTerm(Kind kind, const std::vector<Term>& children)
 772    */
 773   BITVECTOR_SDIV,
 774   /**
 775    * Two's complement signed remainder of two bit-vectors
 776    * (sign follows dividend).
 777    * Parameters: 2
 778    *   -[1]..[2]: Terms of bit-vector sort (sorts must match)
 779    * Create with:
 780    *   mkTerm(Kind kind, Term child1, Term child2)
 781    *   mkTerm(Kind kind, const std::vector<Term>& children)
 782    */
 783   BITVECTOR_SREM,
 784   /**
 785    * Two's complement signed remainder
 786    * (sign follows divisor).
 787    * Parameters: 2
 788    *   -[1]..[2]: Terms of bit-vector sort (sorts must match)
 789    * Create with:
 790    *   mkTerm(Kind kind, Term child1, Term child2)
 791    *   mkTerm(Kind kind, const std::vector<Term>& children)
 792    */
 793   BITVECTOR_SMOD,
 794   /**
 795    * Unsigned division of two bit-vectors, truncating towards 0
 796    * (defined to be the all-ones bit pattern, if divisor is 0).
 797    * Parameters: 2
 798    *   -[1]..[2]: Terms of bit-vector sort (sorts must match)
 799    * Create with:
 800    *   mkTerm(Kind kind, Term child1, Term child2)
 801    *   mkTerm(Kind kind, const std::vector<Term>& children)
 802    */
 803   BITVECTOR_UDIV_TOTAL,
 804   /**
 805    * Unsigned remainder from truncating division of two bit-vectors
 806    * (defined to be equal to the dividend, if divisor is 0).
 807    * Parameters: 2
 808    *   -[1]..[2]: Terms of bit-vector sort (sorts must match)
 809    * Create with:
 810    *   mkTerm(Kind kind, Term child1, Term child2)
 811    *   mkTerm(Kind kind, const std::vector<Term>& children)
 812    */
 813   BITVECTOR_UREM_TOTAL,
 814   /**
 815    * Bit-vector shift left.
 816    * The two bit-vector parameters must have same width.
 817    * Parameters: 2
 818    *   -[1]..[2]: Terms of bit-vector sort (sorts must match)
 819    * Create with:
 820    *   mkTerm(Kind kind, Term child1, Term child2)
 821    *   mkTerm(Kind kind, const std::vector<Term>& children)
 822    */
 823   BITVECTOR_SHL,
 824   /**
 825    * Bit-vector logical shift right.
 826    * The two bit-vector parameters must have same width.
 827    * Parameters: 2
 828    *   -[1]..[2]: Terms of bit-vector sort (sorts must match)
 829    * Create with:
 830    *   mkTerm(Kind kind, Term child1, Term child2)
 831    *   mkTerm(Kind kind, const std::vector<Term>& children)
 832    */
 833   BITVECTOR_LSHR,
 834   /**
 835    * Bit-vector arithmetic shift right.
 836    * The two bit-vector parameters must have same width.
 837    * Parameters: 2
 838    *   -[1]..[2]: Terms of bit-vector sort (sorts must match)
 839    * Create with:
 840    *   mkTerm(Kind kind, Term child1, Term child2)
 841    *   mkTerm(Kind kind, const std::vector<Term>& children)
 842    */
 843   BITVECTOR_ASHR,
 844   /**
 845    * Bit-vector unsigned less than.
 846    * The two bit-vector parameters must have same width.
 847    * Parameters: 2
 848    *   -[1]..[2]: Terms of bit-vector sort (sorts must match)
 849    * Create with:
 850    *   mkTerm(Kind kind, Term child1, Term child2)
 851    *   mkTerm(Kind kind, const std::vector<Term>& children)
 852    */
 853   BITVECTOR_ULT,
 854   /**
 855    * Bit-vector unsigned less than or equal.
 856    * The two bit-vector parameters must have same width.
 857    * Parameters: 2
 858    *   -[1]..[2]: Terms of bit-vector sort (sorts must match)
 859    * Create with:
 860    *   mkTerm(Kind kind, Term child1, Term child2)
 861    *   mkTerm(Kind kind, const std::vector<Term>& children)
 862    */
 863   BITVECTOR_ULE,
 864   /**
 865    * Bit-vector unsigned greater than.
 866    * The two bit-vector parameters must have same width.
 867    * Parameters: 2
 868    *   -[1]..[2]: Terms of bit-vector sort (sorts must match)
 869    * Create with:
 870    *   mkTerm(Kind kind, Term child1, Term child2)
 871    *   mkTerm(Kind kind, const std::vector<Term>& children)
 872    */
 873   BITVECTOR_UGT,
 874   /**
 875    * Bit-vector unsigned greater than or equal.
 876    * The two bit-vector parameters must have same width.
 877    * Parameters: 2
 878    * Create with:
 879    *   mkTerm(Kind kind, Term child1, Term child2)
 880    *   mkTerm(Kind kind, const std::vector<Term>& children)
 881    */
 882   BITVECTOR_UGE,
 883   /* Bit-vector signed less than.
 884    * The two bit-vector parameters must have same width.
 885    * Parameters: 2
 886    * Create with:
 887    *   mkTerm(Kind kind, Term child1, Term child2)
 888    *   mkTerm(Kind kind, const std::vector<Term>& children)
 889    */
 890   BITVECTOR_SLT,
 891   /**
 892    * Bit-vector signed less than or equal.
 893    * The two bit-vector parameters must have same width.
 894    * Parameters: 2
 895    *   -[1]..[2]: Terms of bit-vector sort (sorts must match)
 896    * Create with:
 897    *   mkTerm(Kind kind, Term child1, Term child2)
 898    *   mkTerm(Kind kind, const std::vector<Term>& children)
 899    */
 900   BITVECTOR_SLE,
 901   /**
 902    * Bit-vector signed greater than.
 903    * The two bit-vector parameters must have same width.
 904    * Parameters: 2
 905    *   -[1]..[2]: Terms of bit-vector sort (sorts must match)
 906    * Create with:
 907    *   mkTerm(Kind kind, Term child1, Term child2)
 908    *   mkTerm(Kind kind, const std::vector<Term>& children)
 909    */
 910   BITVECTOR_SGT,
 911   /**
 912    * Bit-vector signed greater than or equal.
 913    * The two bit-vector parameters must have same width.
 914    * Parameters: 2
 915    *   -[1]..[2]: Terms of bit-vector sort (sorts must match)
 916    * Create with:
 917    *   mkTerm(Kind kind, Term child1, Term child2)
 918    *   mkTerm(Kind kind, const std::vector<Term>& children)
 919    */
 920   BITVECTOR_SGE,
 921   /**
 922    * Bit-vector unsigned less than, returns bit-vector of size 1.
 923    * Parameters: 2
 924    *   -[1]..[2]: Terms of bit-vector sort (sorts must match)
 925    * Create with:
 926    *   mkTerm(Kind kind, Term child1, Term child2)
 927    *   mkTerm(Kind kind, const std::vector<Term>& children)
 928    */
 929   BITVECTOR_ULTBV,
 930   /**
 931    * Bit-vector signed less than. returns bit-vector of size 1.
 932    * Parameters: 2
 933    *   -[1]..[2]: Terms of bit-vector sort (sorts must match)
 934    * Create with:
 935    *   mkTerm(Kind kind, Term child1, Term child2)
 936    *   mkTerm(Kind kind, const std::vector<Term>& children)
 937    */
 938   BITVECTOR_SLTBV,
 939   /**
 940    * Same semantics as regular ITE, but condition is bit-vector of size 1.
 941    * Parameters: 3
 942    *   -[1]: Term of bit-vector sort of size 1, representing the condition
 943    *   -[2]: Term reprsenting the 'then' branch
 944    *   -[3]: Term representing the 'else' branch
 945    * 'then' and 'else' term must have same base sort.
 946    * Create with:
 947    *   mkTerm(Kind kind, Term child1, Term child2, Term child3)
 948    *   mkTerm(Kind kind, const std::vector<Term>& children)
 949    */
 950   BITVECTOR_ITE,
 951   /**
 952    * Bit-vector redor.
 953    * Parameters: 1
 954    *   -[1]: Term of bit-vector sort
 955    * Create with:
 956    *   mkTerm(Kind kind, Term child)
 957    */
 958   BITVECTOR_REDOR,
 959   /**
 960    * Bit-vector redand.
 961    * Parameters: 1
 962    *   -[1]: Term of bit-vector sort
 963    * Create with:
 964    *   mkTerm(Kind kind, Term child)
 965    */
 966   BITVECTOR_REDAND,
 967 #if 0
 968   /* formula to be treated as a bv atom via eager bit-blasting
 969    * (internal-only symbol) */
 970   BITVECTOR_EAGER_ATOM,
 971   /* term to be treated as a variable. used for eager bit-blasting Ackermann
 972    * expansion of bvudiv (internal-only symbol) */
 973   BITVECTOR_ACKERMANIZE_UDIV,
 974   /* term to be treated as a variable. used for eager bit-blasting Ackermann
 975    * expansion of bvurem (internal-only symbol) */
 976   BITVECTOR_ACKERMANIZE_UREM,
 977   /* operator for the bit-vector boolean bit extract.
 978    * One parameter, parameter is the index of the bit to extract */
 979   BITVECTOR_BITOF_OP,
 980 #endif
 981   /**
 982    * Operator for bit-vector extract (from index 'high' to 'low').
 983    * Parameters: 2
 984    *   -[1]: The 'high' index
 985    *   -[2]: The 'low' index
 986    * Create with:
 987    *   mkOpTerm(Kind kind, uint32_t param, uint32_t param)
 988    */
 989   BITVECTOR_EXTRACT_OP,
 990   /**
 991    * Operator for bit-vector repeat.
 992    * Parameter 1:
 993    *   -[1]: Number of times to repeat a given bit-vector
 994    * Create with:
 995    *   mkOpTerm(Kind kind, uint32_t param).
 996    */
 997   BITVECTOR_REPEAT_OP,
 998   /**
 999    * Operator for bit-vector zero-extend.
1000    * Parameter 1:
1001    *   -[1]: Number of bits by which a given bit-vector is to be extended
1002    * Create with:
1003    *   mkOpTerm(Kind kind, uint32_t param).
1004    */
1005   BITVECTOR_ZERO_EXTEND_OP,
1006   /**
1007    * Operator for bit-vector sign-extend.
1008    * Parameter 1:
1009    *   -[1]: Number of bits by which a given bit-vector is to be extended
1010    * Create with:
1011    *   mkOpTerm(Kind kind, uint32_t param).
1012    */
1013   BITVECTOR_SIGN_EXTEND_OP,
1014   /**
1015    * Operator for bit-vector rotate left.
1016    * Parameter 1:
1017    *   -[1]: Number of bits by which a given bit-vector is to be rotated
1018    * Create with:
1019    *   mkOpTerm(Kind kind, uint32_t param).
1020    */
1021   BITVECTOR_ROTATE_LEFT_OP,
1022   /**
1023    * Operator for bit-vector rotate right.
1024    * Parameter 1:
1025    *   -[1]: Number of bits by which a given bit-vector is to be rotated
1026    * Create with:
1027    *   mkOpTerm(Kind kind, uint32_t param).
1028    */
1029   BITVECTOR_ROTATE_RIGHT_OP,
1030 #if 0
1031   /* bit-vector boolean bit extract.
1032    * first parameter is a BITVECTOR_BITOF_OP, second is a bit-vector term */
1033   BITVECTOR_BITOF,
1034 #endif
1035   /* Bit-vector extract.
1036    * Parameters: 2
1037    *   -[1]: BITVECTOR_EXTRACT_OP Term
1038    *   -[2]: Term of bit-vector sort
1039    * Create with:
1040    *   mkTerm(Term opTerm, Term child)
1041    *   mkTerm(Term opTerm, const std::vector<Term>& children)
1042    */
1043   BITVECTOR_EXTRACT,
1044   /* Bit-vector repeat.
1045    * Parameters: 2
1046    *   -[1]: BITVECTOR_REPEAT_OP Term
1047    *   -[2]: Term of bit-vector sort
1048    * Create with:
1049    *   mkTerm(Term opTerm, Term child)
1050    *   mkTerm(Term opTerm, const std::vector<Term>& children)
1051    */
1052   BITVECTOR_REPEAT,
1053   /* Bit-vector zero-extend.
1054    * Parameters: 2
1055    *   -[1]: BITVECTOR_ZERO_EXTEND_OP Term
1056    *   -[2]: Term of bit-vector sort
1057    * Create with:
1058    *   mkTerm(Term opTerm, Term child)
1059    *   mkTerm(Term opTerm, const std::vector<Term>& children)
1060    */
1061   BITVECTOR_ZERO_EXTEND,
1062   /* Bit-vector sign-extend.
1063    * Parameters: 2
1064    *   -[1]: BITVECTOR_SIGN_EXTEND_OP Term
1065    *   -[2]: Term of bit-vector sort
1066    * Create with:
1067    *   mkTerm(Term opTerm, Term child)
1068    *   mkTerm(Term opTerm, const std::vector<Term>& children)
1069    */
1070   BITVECTOR_SIGN_EXTEND,
1071   /* Bit-vector rotate left.
1072    * Parameters: 2
1073    *   -[1]: BITVECTOR_ROTATE_LEFT_OP Term
1074    *   -[2]: Term of bit-vector sort
1075    * Create with:
1076    *   mkTerm(Term opTerm, Term child)
1077    *   mkTerm(Term opTerm, const std::vector<Term>& children)
1078    */
1079   BITVECTOR_ROTATE_LEFT,
1080   /**
1081    * Bit-vector rotate right.
1082    * Parameters: 2
1083    *   -[1]: BITVECTOR_ROTATE_RIGHT_OP Term
1084    *   -[2]: Term of bit-vector sort
1085    * Create with:
1086    *   mkTerm(Term opTerm, Term child)
1087    *   mkTerm(Term opTerm, const std::vector<Term>& children)
1088    */
1089   BITVECTOR_ROTATE_RIGHT,
1090   /**
1091    * Operator for the conversion from Integer to bit-vector.
1092    * Parameter: 1
1093    *   -[1]: Size of the bit-vector to convert to
1094    * Create with:
1095    *   mkOpTerm(Kind kind, uint32_t param).
1096    */
1097   INT_TO_BITVECTOR_OP,
1098   /**
1099    * Integer conversion to bit-vector.
1100    * Parameters: 2
1101    *   -[1]: INT_TO_BITVECTOR_OP Term
1102    *   -[2]: Integer term
1103    * Create with:
1104    *   mkTerm(Kind kind, Term child1, Term child2)
1105    *   mkTerm(Kind kind, const std::vector<Term>& children)
1106    */
1107   INT_TO_BITVECTOR,
1108   /**
1109    * Bit-vector conversion to (nonnegative) integer.
1110    * Parameter: 1
1111    *   -[1]: Term of bit-vector sort
1112    * Create with:
1113    *   mkTerm(Kind kind, Term child)
1114    */
1115   BITVECTOR_TO_NAT,
1116
1117   /* FP -------------------------------------------------------------------- */
1118
1119   /**
1120    * Floating-point constant, constructed from a double or string.
1121    * Parameters: 3
1122    *   -[1]: Size of the exponent
1123    *   -[2]: Size of the significand
1124    *   -[3]: Value of the floating-point constant as a bit-vector term
1125    * Create with:
1126    *   mkFloatingPoint(uint32_t sig, uint32_t exp, Term val)
1127    */
1128   CONST_FLOATINGPOINT,
1129   /**
1130    * Floating-point rounding mode term.
1131    * Create with:
1132    *   mkRoundingMode(RoundingMode rm)
1133    */
1134   CONST_ROUNDINGMODE,
1135   /**
1136    * Create floating-point literal from bit-vector triple.
1137    * Parameters: 3
1138    *   -[1]: Sign bit as a bit-vector term
1139    *   -[2]: Exponent bits as a bit-vector term
1140    *   -[3]: Significand bits as a bit-vector term (without hidden bit)
1141    * Create with:
1142    *   mkTerm(Kind kind, Term child1, Term child2, Term child3)
1143    *   mkTerm(Kind kind, const std::vector<Term>& children)
1144    */
1145   FLOATINGPOINT_FP,
1146   /**
1147    * Floating-point equality.
1148    * Parameters: 2
1149    *   -[1]..[2]: Terms of floating point sort
1150    * Create with:
1151    *   mkTerm(Kind kind, Term child1, Term child2)
1152    *   mkTerm(Kind kind, const std::vector<Term>& children)
1153    */
1154   FLOATINGPOINT_EQ,
1155   /**
1156    * Floating-point absolute value.
1157    * Parameters: 1
1158    *   -[1]: Term of floating point sort
1159    * Create with:
1160    *   mkTerm(Kind kind, Term child)
1161    */
1162   FLOATINGPOINT_ABS,
1163   /**
1164    * Floating-point negation.
1165    * Parameters: 1
1166    *   -[1]: Term of floating point sort
1167    * Create with:
1168    *   mkTerm(Kind kind, Term child)
1169    */
1170   FLOATINGPOINT_NEG,
1171   /**
1172    * Floating-point addition.
1173    * Parameters: 3
1174    *   -[1]: CONST_ROUNDINGMODE
1175    *   -[2]: Term of sort FloatingPoint
1176    *   -[3]: Term of sort FloatingPoint
1177    * Create with:
1178    *   mkTerm(Kind kind, Term child1, Term child2, child3)
1179    *   mkTerm(Kind kind, const std::vector<Term>& children)
1180    */
1181   FLOATINGPOINT_PLUS,
1182   /**
1183    * Floating-point sutraction.
1184    * Parameters: 3
1185    *   -[1]: CONST_ROUNDINGMODE
1186    *   -[2]: Term of sort FloatingPoint
1187    *   -[3]: Term of sort FloatingPoint
1188    * Create with:
1189    *   mkTerm(Kind kind, Term child1, Term child2, Term child3)
1190    *   mkTerm(Kind kind, const std::vector<Term>& children)
1191    */
1192   FLOATINGPOINT_SUB,
1193   /**
1194    * Floating-point multiply.
1195    * Parameters: 3
1196    *   -[1]: CONST_ROUNDINGMODE
1197    *   -[2]: Term of sort FloatingPoint
1198    *   -[3]: Term of sort FloatingPoint
1199    * Create with:
1200    *   mkTerm(Kind kind, Term child1, Term child2, Term child3)
1201    *   mkTerm(Kind kind, const std::vector<Term>& children)
1202    */
1203   FLOATINGPOINT_MULT,
1204   /**
1205    * Floating-point division.
1206    * Parameters: 3
1207    *   -[1]: CONST_ROUNDINGMODE
1208    *   -[2]: Term of sort FloatingPoint
1209    *   -[3]: Term of sort FloatingPoint
1210    * Create with:
1211    *   mkTerm(Kind kind, Term child1, Term child2, Term child3)
1212    *   mkTerm(Kind kind, const std::vector<Term>& children)
1213    */
1214   FLOATINGPOINT_DIV,
1215   /**
1216    * Floating-point fused multiply and add.
1217    * Parameters: 4
1218    *   -[1]: CONST_ROUNDINGMODE
1219    *   -[2]: Term of sort FloatingPoint
1220    *   -[3]: Term of sort FloatingPoint
1221    *   -[4]: Term of sort FloatingPoint
1222    * Create with:
1223    *   mkTerm(Kind kind, const std::vector<Term>& children)
1224    */
1225   FLOATINGPOINT_FMA,
1226   /**
1227    * Floating-point square root.
1228    * Parameters: 2
1229    *   -[1]: CONST_ROUNDINGMODE
1230    *   -[2]: Term of sort FloatingPoint
1231    * Create with:
1232    *   mkTerm(Kind kind, Term child1, Term child2)
1233    *   mkTerm(Kind kind, const std::vector<Term>& children)
1234    */
1235   FLOATINGPOINT_SQRT,
1236   /**
1237    * Floating-point remainder.
1238    * Parameters: 2
1239    *   -[1]..[2]: Terms of floating point sort
1240    * Create with:
1241    *   mkTerm(Kind kind, Term child1, Term child2)
1242    *   mkTerm(Kind kind, const std::vector<Term>& children)
1243    */
1244   FLOATINGPOINT_REM,
1245   /**
1246    * Floating-point round to integral.
1247    * Parameters: 2
1248    *   -[1]..[2]: Terms of floating point sort
1249    * Create with:
1250    *   mkTerm(Kind kind, Term child1, Term child2)
1251    *   mkTerm(Kind kind, const std::vector<Term>& children)
1252    */
1253   FLOATINGPOINT_RTI,
1254   /**
1255    * Floating-point minimum.
1256    * Parameters: 2
1257    *   -[1]..[2]: Terms of floating point sort
1258    * Create with:
1259    *   mkTerm(Kind kind, Term child1, Term child2)
1260    *   mkTerm(Kind kind, const std::vector<Term>& children)
1261    */
1262   FLOATINGPOINT_MIN,
1263   /**
1264    * Floating-point maximum.
1265    * Parameters: 2
1266    *   -[1]..[2]: Terms of floating point sort
1267    * Create with:
1268    *   mkTerm(Kind kind, Term child1, Term child2)
1269    *   mkTerm(Kind kind, const std::vector<Term>& children)
1270    */
1271   FLOATINGPOINT_MAX,
1272 #if 0
1273   /* floating-point minimum (defined for all inputs) */
1274   FLOATINGPOINT_MIN_TOTAL,
1275   /* floating-point maximum (defined for all inputs) */
1276   FLOATINGPOINT_MAX_TOTAL,
1277 #endif
1278   /**
1279    * Floating-point less than or equal.
1280    * Parameters: 2
1281    *   -[1]..[2]: Terms of floating point sort
1282    * Create with:
1283    *   mkTerm(Kind kind, Term child1, Term child2)
1284    *   mkTerm(Kind kind, const std::vector<Term>& children)
1285    */
1286   FLOATINGPOINT_LEQ,
1287   /**
1288    * Floating-point less than.
1289    * Parameters: 2
1290    *   -[1]..[2]: Terms of floating point sort
1291    * Create with:
1292    *   mkTerm(Kind kind, Term child1, Term child2)
1293    *   mkTerm(Kind kind, const std::vector<Term>& children)
1294    */
1295   FLOATINGPOINT_LT,
1296   /**
1297    * Floating-point greater than or equal.
1298    * Parameters: 2
1299    *   -[1]..[2]: Terms of floating point sort
1300    * Create with:
1301    *   mkTerm(Kind kind, Term child1, Term child2)
1302    *   mkTerm(Kind kind, const std::vector<Term>& children)
1303    */
1304   FLOATINGPOINT_GEQ,
1305   /**
1306    * Floating-point greater than.
1307    * Parameters: 2
1308    * Create with:
1309    *   mkTerm(Kind kind, Term child1, Term child2)
1310    *   mkTerm(Kind kind, const std::vector<Term>& children)
1311    */
1312   FLOATINGPOINT_GT,
1313   /**
1314    * Floating-point is normal.
1315    * Parameters: 1
1316    *   -[1]: Term of floating point sort
1317    * Create with:
1318    *   mkTerm(Kind kind, Term child)
1319    */
1320   FLOATINGPOINT_ISN,
1321   /**
1322    * Floating-point is sub-normal.
1323    * Parameters: 1
1324    *   -[1]: Term of floating point sort
1325    * Create with:
1326    *   mkTerm(Kind kind, Term child)
1327    */
1328   FLOATINGPOINT_ISSN,
1329   /**
1330    * Floating-point is zero.
1331    * Parameters: 1
1332    *   -[1]: Term of floating point sort
1333    * Create with:
1334    *   mkTerm(Kind kind, Term child)
1335    */
1336   FLOATINGPOINT_ISZ,
1337   /**
1338    * Floating-point is infinite.
1339    * Parameters: 1
1340    *   -[1]: Term of floating point sort
1341    * Create with:
1342    *   mkTerm(Kind kind, Term child)
1343    */
1344   FLOATINGPOINT_ISINF,
1345   /**
1346    * Floating-point is NaN.
1347    * Parameters: 1
1348    *   -[1]: Term of floating point sort
1349    * Create with:
1350    *   mkTerm(Kind kind, Term child)
1351    */
1352   FLOATINGPOINT_ISNAN,
1353   /**
1354    * Floating-point is negative.
1355    * Parameters: 1
1356    *   -[1]: Term of floating point sort
1357    * Create with:
1358    *   mkTerm(Kind kind, Term child)
1359    */
1360   FLOATINGPOINT_ISNEG,
1361   /**
1362    * Floating-point is positive.
1363    * Parameters: 1
1364    *   -[1]: Term of floating point sort
1365    * Create with:
1366    *   mkTerm(Kind kind, Term child)
1367    */
1368   FLOATINGPOINT_ISPOS,
1369   /**
1370    * Operator for to_fp from bit vector.
1371    * Parameters: 2
1372    *   -[1]: Exponent size
1373    *   -[2]: Significand size
1374    * Create with:
1375    *   mkOpTerm(Kind kind, uint32_t param1, uint32_t param2)
1376    */
1377   FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP,
1378   /**
1379    * Conversion from an IEEE-754 bit vector to floating-point.
1380    * Parameters: 2
1381    *   -[1]: FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP Term
1382    *   -[2]: Term of sort FloatingPoint
1383    * Create with:
1384    *   mkTerm(Term opTerm, Term child)
1385    *   mkTerm(Term opTerm, const std::vector<Term>& children)
1386    */
1387   FLOATINGPOINT_TO_FP_IEEE_BITVECTOR,
1388   /**
1389    * Operator for to_fp from floating point.
1390    * Parameters: 2
1391    *   -[1]: Exponent size
1392    *   -[2]: Significand size
1393    * Create with:
1394    *   mkOpTerm(Kind kind, uint32_t param1, uint32_t param2)
1395    */
1396   FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP,
1397   /**
1398    * Conversion between floating-point sorts.
1399    * Parameters: 2
1400    *   -[1]: FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP Term
1401    *   -[2]: Term of sort FloatingPoint
1402    * Create with:
1403    *   mkTerm(Term opTerm, Term child)
1404    *   mkTerm(Term opTerm, const std::vector<Term>& children)
1405    */
1406   FLOATINGPOINT_TO_FP_FLOATINGPOINT,
1407   /**
1408    * Operator for to_fp from real.
1409    * Parameters: 2
1410    *   -[1]: Exponent size
1411    *   -[2]: Significand size
1412    * Create with:
1413    *   mkOpTerm(Kind kind, uint32_t param1, uint32_t param2)
1414    */
1415   FLOATINGPOINT_TO_FP_REAL_OP,
1416   /**
1417    * Conversion from a real to floating-point.
1418    * Parameters: 2
1419    *   -[1]: FLOATINGPOINT_TO_FP_REAL_OP Term
1420    *   -[2]: Term of sort FloatingPoint
1421    * Create with:
1422    *   mkTerm(Term opTerm, Term child)
1423    *   mkTerm(Term opTerm, const std::vector<Term>& children)
1424    */
1425   FLOATINGPOINT_TO_FP_REAL,
1426   /*
1427    * Operator for to_fp from signed bit vector.
1428    * Parameters: 2
1429    *   -[1]: Exponent size
1430    *   -[2]: Significand size
1431    * Create with:
1432    *   mkOpTerm(Kind kind, uint32_t param1, uint32_t param2)
1433    */
1434   FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP,
1435   /**
1436    * Conversion from a signed bit vector to floating-point.
1437    * Parameters: 2
1438    *   -[1]: FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP Term
1439    *   -[2]: Term of sort FloatingPoint
1440    * Create with:
1441    *   mkTerm(Term opTerm, Term child)
1442    *   mkTerm(Term opTerm, const std::vector<Term>& children)
1443    */
1444   FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR,
1445   /**
1446    * Operator for to_fp from unsigned bit vector.
1447    * Parameters: 2
1448    *   -[1]: Exponent size
1449    *   -[2]: Significand size
1450    * Create with:
1451    *   mkOpTerm(Kind kind, uint32_t param1, uint32_t param2)
1452    */
1453   FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP,
1454   /**
1455    * Operator for converting an unsigned bit vector to floating-point.
1456    * Parameters: 2
1457    *   -[1]: FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP Term
1458    *   -[2]: Term of sort FloatingPoint
1459    * Create with:
1460    *   mkTerm(Term opTerm, Term child)
1461    *   mkTerm(Term opTerm, const std::vector<Term>& children)
1462    */
1463   FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR,
1464   /**
1465    * Operator for a generic to_fp.
1466    * Parameters: 2
1467    *   -[1]: exponent size
1468    *   -[2]: Significand size
1469    * Create with:
1470    *   mkOpTerm(Kind kind, uint32_t param1, uint32_t param2)
1471    */
1472   FLOATINGPOINT_TO_FP_GENERIC_OP,
1473   /**
1474    * Generic conversion to floating-point, used in parsing only.
1475    * Parameters: 2
1476    *   -[1]: FLOATINGPOINT_TO_FP_GENERIC_OP Term
1477    *   -[2]: Term of sort FloatingPoint
1478    * Create with:
1479    *   mkTerm(Term opTerm, Term child)
1480    *   mkTerm(Term opTerm, const std::vector<Term>& children)
1481    */
1482   FLOATINGPOINT_TO_FP_GENERIC,
1483   /**
1484    * Operator for to_ubv.
1485    * Parameters: 1
1486    *   -[1]: Size of the bit-vector to convert to
1487    * Create with:
1488    *   mkOpTerm(Kind kind, uint32_t param)
1489    */
1490   FLOATINGPOINT_TO_UBV_OP,
1491   /**
1492    * Conversion from a floating-point value to an unsigned bit vector.
1493    * Parameters: 2
1494    *   -[1]: FLOATINGPOINT_TO_FP_TO_UBV_OP Term
1495    *   -[2]: Term of sort FloatingPoint
1496    * Create with:
1497    *   mkTerm(Term opTerm, Term child)
1498    *   mkTerm(Term opTerm, const std::vector<Term>& children)
1499    */
1500   FLOATINGPOINT_TO_UBV,
1501   /**
1502    * Operator for to_ubv_total.
1503    * Parameters: 1
1504    *   -[1]: Size of the bit-vector to convert to
1505    * Create with:
1506    *   mkOpTerm(Kind kind, uint32_t param)
1507    */
1508   FLOATINGPOINT_TO_UBV_TOTAL_OP,
1509   /**
1510    * Conversion from  a floating-point value to an unsigned bit vector
1511    * (defined for all inputs).
1512    * Parameters: 2
1513    *   -[1]: FLOATINGPOINT_TO_FP_TO_UBV_TOTAL_OP Term
1514    *   -[2]: Term of sort FloatingPoint
1515    * Create with:
1516    *   mkTerm(Term opTerm, Term child)
1517    *   mkTerm(Term opTerm, const std::vector<Term>& children)
1518    */
1519   FLOATINGPOINT_TO_UBV_TOTAL,
1520   /**
1521    * Operator for to_sbv.
1522    * Parameters: 1
1523    *   -[1]: Size of the bit-vector to convert to
1524    * Create with:
1525    *   mkOpTerm(Kind kind, uint32_t param)
1526    */
1527   FLOATINGPOINT_TO_SBV_OP,
1528   /**
1529    * Conversion from a floating-point value to a signed bit vector.
1530    * Parameters: 2
1531    *   -[1]: FLOATINGPOINT_TO_FP_TO_SBV_OP Term
1532    *   -[2]: Term of sort FloatingPoint
1533    * Create with:
1534    *   mkTerm(Term opTerm, Term child)
1535    *   mkTerm(Term opTerm, const std::vector<Term>& children)
1536    */
1537   FLOATINGPOINT_TO_SBV,
1538   /**
1539    * Operator for to_sbv_total.
1540    * Parameters: 1
1541    *   -[1]: Size of the bit-vector to convert to
1542    * Create with:
1543    *   mkOpTerm(Kind kind, uint32_t param)
1544    */
1545   FLOATINGPOINT_TO_SBV_TOTAL_OP,
1546   /**
1547    * Conversion from a floating-point value to a signed bit vector
1548    * (defined for all inputs).
1549    * Parameters: 2
1550    *   -[1]: FLOATINGPOINT_TO_FP_TO_SBV_TOTAL_OP Term
1551    *   -[2]: Term of sort FloatingPoint
1552    * Create with:
1553    *   mkTerm(Term opTerm, Term child)
1554    *   mkTerm(Term opTerm, const std::vector<Term>& children)
1555    */
1556   FLOATINGPOINT_TO_SBV_TOTAL,
1557   /**
1558    * Floating-point to real.
1559    * Parameters: 1
1560    *   -[1]: Term of sort FloatingPoint
1561    * Create with:
1562    *   mkTerm(Kind kind, Term child)
1563    */
1564   FLOATINGPOINT_TO_REAL,
1565   /**
1566    * Floating-point to real (defined for all inputs).
1567    * Parameters: 1
1568    *   -[1]: Term of sort FloatingPoint
1569    * Create with:
1570    *   mkTerm(Kind kind, Term child)
1571    */
1572   FLOATINGPOINT_TO_REAL_TOTAL,
1573
1574   /* Arrays ---------------------------------------------------------------- */
1575
1576   /**
1577    * Aarray select.
1578    * Parameters: 2
1579    *   -[1]: Term of array sort
1580    *   -[2]: Selection index
1581    * Create with:
1582    *   mkTerm(Term opTerm, Term child1, Term child2)
1583    *   mkTerm(Term opTerm, const std::vector<Term>& children)
1584    */
1585   SELECT,
1586   /**
1587    * Array store.
1588    * Parameters: 3
1589    *   -[1]: Term of array sort
1590    *   -[2]: Store index
1591    *   -[3]: Term to store at the index
1592    * Create with:
1593    *   mkTerm(Term opTerm, Term child1, Term child2, Term child3)
1594    *   mkTerm(Term opTerm, const std::vector<Term>& children)
1595    */
1596   STORE,
1597   /**
1598    * Constant array.
1599    * Parameters: 2
1600    *   -[1]: Array sort
1601    *   -[2]: Term representing a constant
1602    * Create with:
1603    *   mkTerm(Term opTerm, Term child1, Term child2)
1604    *   mkTerm(Term opTerm, const std::vector<Term>& children)
1605    *
1606    * Note: We currently support the creation of constant arrays, but under some
1607    * conditions when there is a chain of equalities connecting two constant
1608    * arrays, the solver doesn't know what to do and aborts (Issue #1667).
1609    */
1610   STORE_ALL,
1611 #if 0
1612   /* array table function (internal-only symbol) */
1613   ARR_TABLE_FUN,
1614   /* array lambda (internal-only symbol) */
1615   ARRAY_LAMBDA,
1616   /* partial array select, for internal use only */
1617   PARTIAL_SELECT_0,
1618   /* partial array select, for internal use only */
1619   PARTIAL_SELECT_1,
1620 #endif
1621
1622   /* Datatypes ------------------------------------------------------------- */
1623
1624   /**
1625    * Constructor application.
1626    * Paramters: n > 0
1627    *   -[1]: Constructor (operator term)
1628    *   -[2]..[n]: Parameters to the constructor
1629    * Create with:
1630    *   mkTerm(Kind kind, OpTerm opTerm)
1631    *   mkTerm(Kind kind, OpTerm opTerm, Term child)
1632    *   mkTerm(Kind kind, OpTerm opTerm, Term child1, Term child2)
1633    *   mkTerm(Kind kind, OpTerm opTerm, Term child1, Term child2, Term child3)
1634    *   mkTerm(Kind kind, OpTerm opTerm, const std::vector<Term>& children)
1635    */
1636   APPLY_CONSTRUCTOR,
1637   /**
1638    * Datatype selector application.
1639    * Parameters: 1
1640    *   -[1]: Selector (operator term)
1641    *   -[2]: Datatype term (undefined if mis-applied)
1642    * Create with:
1643    *   mkTerm(Kind kind, OpTerm opTerm, Term child)
1644    */
1645   APPLY_SELECTOR,
1646   /**
1647    * Datatype selector application.
1648    * Parameters: 1
1649    *   -[1]: Selector (operator term)
1650    *   -[2]: Datatype term (defined rigidly if mis-applied)
1651    * Create with:
1652    *   mkTerm(Kind kind, OpTerm opTerm, Term child)
1653    */
1654   APPLY_SELECTOR_TOTAL,
1655   /**
1656    * Datatype tester application.
1657    * Parameters: 2
1658    *   -[1]: Tester term
1659    *   -[2]: Datatype term
1660    * Create with:
1661    *   mkTerm(Kind kind, Term child1, Term child2)
1662    *   mkTerm(Kind kind, const std::vector<Term>& children)
1663    */
1664   APPLY_TESTER,
1665 #if 0
1666   /* Parametric datatype term.  */
1667   PARAMETRIC_DATATYPE,
1668   /* type ascription, for datatype constructor applications;
1669    * first parameter is an ASCRIPTION_TYPE, second is the datatype constructor
1670    * application being ascribed */
1671   APPLY_TYPE_ASCRIPTION,
1672 #endif
1673   /**
1674    * Operator for a tuple update.
1675    * Parameters: 1
1676    *   -[1]: Index of the tuple to be updated
1677    * Create with:
1678    *   mkOpTerm(Kind kind, uint32_t param)
1679    */
1680   TUPLE_UPDATE_OP,
1681   /**
1682    * Tuple update.
1683    * Parameters: 3
1684    *   -[1]: TUPLE_UPDATE_OP (which references an index)
1685    *   -[2]: Tuple
1686    *   -[3]: Element to store in the tuple at the given index
1687    * Create with:
1688    *   mkTerm(Kind kind, Term child1, Term child2, Term child3)
1689    *   mkTerm(Kind kind, const std::vector<Term>& children)
1690    */
1691   TUPLE_UPDATE,
1692   /**
1693    * Operator for a record update.
1694    * Parameters: 1
1695    *   -[1]: Name of the field to be updated
1696    * Create with:
1697    *   mkOpTerm(Kind kind, const std::string& param)
1698    */
1699   RECORD_UPDATE_OP,
1700   /**
1701    * Record update.
1702    * Parameters: 3
1703    *   -[1]: RECORD_UPDATE_OP Term (which references a field)
1704    *   -[2]: Record term to update
1705    *   -[3]: Element to store in the record in the given field
1706    * Create with:
1707    *   mkTerm(Kind kind, Term child1, Term child2)
1708    *   mkTerm(Kind kind, const std::vector<Term>& children)
1709    */
1710   RECORD_UPDATE,
1711 #if 0
1712   /* datatypes size */
1713   DT_SIZE,
1714   /* datatypes height bound */
1715   DT_HEIGHT_BOUND,
1716   /* datatypes height bound */
1717   DT_SIZE_BOUND,
1718   /* datatypes sygus bound */
1719   DT_SYGUS_BOUND,
1720   /* datatypes sygus term order */
1721   DT_SYGUS_TERM_ORDER,
1722   /* datatypes sygus is constant */
1723   DT_SYGUS_IS_CONST,
1724 #endif
1725
1726   /* Separation Logic ------------------------------------------------------ */
1727
1728   /**
1729    * Separation logic nil term.
1730    * Parameters: 0
1731    * Create with:
1732    *   mkSepNil(Sort sort)
1733    */
1734   SEP_NIL,
1735   /**
1736    * Separation logic empty heap.
1737    * Parameters: 2
1738    *   -[1]: Term of the same sort as the sort of the location of the heap
1739    *         that is constrained to be empty
1740    *   -[2]: Term of the same sort as the data sort of the heap that is
1741    *         that is constrained to be empty
1742    * Create with:
1743    *   mkTerm(Kind kind, Term child1, Term child2)
1744    *   mkTerm(Kind kind, const std::vector<Term>& children)
1745    */
1746   SEP_EMP,
1747   /**
1748    * Separation logic points-to relation.
1749    * Parameters: 2
1750    *   -[1]: Location of the points-to constraint
1751    *   -[2]: Data of the points-to constraint
1752    * Create with:
1753    *   mkTerm(Kind kind, Term child1, Term child2)
1754    *   mkTerm(Kind kind, const std::vector<Term>& children)
1755    */
1756   SEP_PTO,
1757   /**
1758    * Separation logic star.
1759    * Parameters: n >= 2
1760    *   -[1]..[n]: Child constraints that hold in disjoint (separated) heaps
1761    * Create with:
1762    *   mkTerm(Kind kind, Term child1, Term child2)
1763    *   mkTerm(Kind kind, Term child1, Term child2, Term child3)
1764    *   mkTerm(Kind kind, const std::vector<Term>& children)
1765    */
1766   SEP_STAR,
1767   /**
1768    * Separation logic magic wand.
1769    * Parameters: 2
1770    *   -[1]: Antecendant of the magic wand constraint
1771    *   -[2]: Conclusion of the magic wand constraint, which is asserted to
1772    *         hold in all heaps that are disjoint extensions of the antecedent.
1773    * Create with:
1774    *   mkTerm(Kind kind, Term child1, Term child2)
1775    *   mkTerm(Kind kind, const std::vector<Term>& children)
1776    */
1777   SEP_WAND,
1778 #if 0
1779   /* separation label (internal use only) */
1780   SEP_LABEL,
1781 #endif
1782
1783   /* Sets ------------------------------------------------------------------ */
1784
1785   /**
1786    * Empty set constant.
1787    * Parameters: 1
1788    *   -[1]: Sort of the set elements
1789    * Create with:
1790    *   mkEmptySet(Sort sort)
1791    */
1792   EMPTYSET,
1793   /**
1794    * Set union.
1795    * Parameters: 2
1796    *   -[1]..[2]: Terms of set sort
1797    * Create with:
1798    *   mkTerm(Kind kind, Term child1, Term child2)
1799    *   mkTerm(Kind kind, const std::vector<Term>& children)
1800    */
1801   UNION,
1802   /**
1803    * Set intersection.
1804    * Parameters: 2
1805    *   -[1]..[2]: Terms of set sort
1806    * Create with:
1807    *   mkTerm(Kind kind, Term child1, Term child2)
1808    *   mkTerm(Kind kind, const std::vector<Term>& children)
1809    */
1810   INTERSECTION,
1811   /**
1812    * Set subtraction.
1813    * Parameters: 2
1814    *   -[1]..[2]: Terms of set sort
1815    * Create with:
1816    *   mkTerm(Kind kind, Term child1, Term child2)
1817    *   mkTerm(Kind kind, const std::vector<Term>& children)
1818    */
1819   SETMINUS,
1820   /**
1821    * Subset predicate.
1822    * Parameters: 2
1823    *   -[1]..[2]: Terms of set sort, [1] a subset of set [2]?
1824    * Create with:
1825    *   mkTerm(Kind kind, Term child1, Term child2)
1826    *   mkTerm(Kind kind, const std::vector<Term>& children)
1827    */
1828   SUBSET,
1829   /**
1830    * Set membership predicate.
1831    * Parameters: 2
1832    *   -[1]..[2]: Terms of set sort, [1] a member of set [2]?
1833    * Create with:
1834    *   mkTerm(Kind kind, Term child1, Term child2)
1835    *   mkTerm(Kind kind, const std::vector<Term>& children)
1836    */
1837   MEMBER,
1838   /**
1839    * The set of the single element given as a parameter.
1840    * Parameters: 1
1841    *   -[1]: Single element
1842    * Create with:
1843    *   mkTerm(Kind kind, Term child)
1844    */
1845   SINGLETON,
1846   /**
1847    * The set obtained by inserting elements;
1848    * Parameters: n > 0
1849    *   -[1]..[n-1]: Elements inserted into set [n]
1850    *   -[n]: Set Term
1851    * Create with:
1852    *   mkTerm(Kind kind, Term child)
1853    *   mkTerm(Kind kind, Term child1, Term child2)
1854    *   mkTerm(Kind kind, Term child1, Term child2, Term child3)
1855    *   mkTerm(Kind kind, const std::vector<Term>& children)
1856    */
1857   INSERT,
1858   /**
1859    * Set cardinality.
1860    * Parameters: 1
1861    *   -[1]: Set to determine the cardinality of
1862    * Create with:
1863    *   mkTerm(Kind kind, Term child)
1864    */
1865   CARD,
1866   /**
1867    * Set complement with respect to finite universe.
1868    * Parameters: 1
1869    *   -[1]: Set to complement
1870    * Create with:
1871    *   mkTerm(Kind kind, Term child)
1872    */
1873   COMPLEMENT,
1874   /**
1875    * Finite universe set.
1876    * All set variables must be interpreted as subsets of it.
1877    * Create with:
1878    *   mkUniverseSet(Sort sort)
1879    */
1880   UNIVERSE_SET,
1881   /**
1882    * Set join.
1883    * Parameters: 2
1884    *   -[1]..[2]: Terms of set sort
1885    * Create with:
1886    *   mkTerm(Kind kind, Term child1, Term child2)
1887    *   mkTerm(Kind kind, const std::vector<Term>& children)
1888    */
1889   JOIN,
1890   /**
1891    * Set cartesian product.
1892    * Parameters: 2
1893    *   -[1]..[2]: Terms of set sort
1894    * Create with:
1895    *   mkTerm(Kind kind, Term child1, Term child2)
1896    *   mkTerm(Kind kind, const std::vector<Term>& children)
1897    */
1898   PRODUCT,
1899   /**
1900    * Set transpose.
1901    * Parameters: 1
1902    *   -[1]: Term of set sort
1903    * Create with:
1904    *   mkTerm(Kind kind, Term child)
1905    */
1906   TRANSPOSE,
1907   /**
1908    * Set transitive closure.
1909    * Parameters: 1
1910    *   -[1]: Term of set sort
1911    * Create with:
1912    *   mkTerm(Kind kind, Term child)
1913    */
1914   TCLOSURE,
1915   /**
1916    * Set join image.
1917    * Parameters: 2
1918    *   -[1]..[2]: Terms of set sort
1919    * Create with:
1920    *   mkTerm(Kind kind, Term child1, Term child2)
1921    *   mkTerm(Kind kind, const std::vector<Term>& children)
1922    */
1923   JOIN_IMAGE,
1924   /**
1925    * Set identity.
1926    * Parameters: 1
1927    *   -[1]: Term of set sort
1928    * Create with:
1929    *   mkTerm(Kind kind, Term child)
1930    */
1931   IDEN,
1932
1933   /* Strings --------------------------------------------------------------- */
1934
1935   /**
1936    * String concat.
1937    * Parameters: n > 1
1938    *   -[1]..[n]: Terms of String sort
1939    * Create with:
1940    *   mkTerm(Kind kind, Term child1, Term child2)
1941    *   mkTerm(Kind kind, Term child1, Term child2, Term child3)
1942    *   mkTerm(Kind kind, const std::vector<Term>& children)
1943    */
1944   STRING_CONCAT,
1945   /**
1946    * String membership.
1947    * Parameters: 2
1948    *   -[1]..[2]: Terms of String sort
1949    * Create with:
1950    *   mkTerm(Kind kind, Term child1, Term child2)
1951    *   mkTerm(Kind kind, const std::vector<Term>& children)
1952    */
1953   STRING_IN_REGEXP,
1954   /**
1955    * String length.
1956    * Parameters: 1
1957    *   -[1]: Term of String sort
1958    * Create with:
1959    *   mkTerm(Kind kind, Term child)
1960    */
1961   STRING_LENGTH,
1962   /**
1963    * String substring.
1964    * Extracts a substring, starting at index i and of length l, from a string
1965    * s.  If the start index is negative, the start index is greater than the
1966    * length of the string, or the length is negative, the result is the empty
1967    * string.
1968    * Parameters: 3
1969    *   -[1]: Term of sort String
1970    *   -[2]: Term of sort Integer (index i)
1971    *   -[3]: Term of sort Integer (length l)
1972    * Create with:
1973    *   mkTerm(Kind kind, Term child1, Term child2, Term child3)
1974    *   mkTerm(Kind kind, const std::vector<Term>& children)
1975    */
1976   STRING_SUBSTR,
1977   /**
1978    * String character at.
1979    * Returns the character at index i from a string s. If the index is negative
1980    * or the index is greater than the length of the string, the result is the
1981    * empty string. Otherwise the result is a string of length 1.
1982    * Parameters: 2
1983    *   -[1]: Term of sort String (string s)
1984    *   -[2]: Term of sort Integer (index i)
1985    * Create with:
1986    *   mkTerm(Kind kind, Term child1, Term child2)
1987    *   mkTerm(Kind kind, const std::vector<Term>& children)
1988    */
1989   STRING_CHARAT,
1990   /**
1991    * String contains.
1992    * Checks whether a string s1 contains another string s2. If s2 is empty, the
1993    * result is always true.
1994    * Parameters: 2
1995    *   -[1]: Term of sort String (the string s1)
1996    *   -[2]: Term of sort String (the string s2)
1997    * Create with:
1998    *   mkTerm(Kind kind, Term child1, Term child2)
1999    *   mkTerm(Kind kind, const std::vector<Term>& children)
2000    */
2001   STRING_STRCTN,
2002   /**
2003    * String index-of.
2004    * Returns the index of a substring s2 in a string s1 starting at index i. If
2005    * the index is negative or greater than the length of string s1 or the
2006    * substring s2 does not appear in string s1 after index i, the result is -1.
2007    * Parameters: 3
2008    *   -[1]: Term of sort String (substring s1)
2009    *   -[2]: Term of sort String (substring s2)
2010    *   -[3]: Term of sort Integer (index i)
2011    * Create with:
2012    *   mkTerm(Kind kind, Term child1, Term child2, Term child3)
2013    *   mkTerm(Kind kind, const std::vector<Term>& children)
2014    */
2015   STRING_STRIDOF,
2016   /**
2017    * String replace.
2018    * Replaces a string s2 in a string s1 with string s3. If s2 does not appear
2019    * in s1, s1 is returned unmodified.
2020    * Parameters: 3
2021    *   -[1]: Term of sort String (string s1)
2022    *   -[2]: Term of sort String (string s2)
2023    *   -[3]: Term of sort String (string s3)
2024    * Create with:
2025    *   mkTerm(Kind kind, Term child1, Term child2, Term child3)
2026    *   mkTerm(Kind kind, const std::vector<Term>& children)
2027    */
2028   STRING_STRREPL,
2029   /**
2030    * String prefix-of.
2031    * Checks whether a string s1 is a prefix of string s2. If string s1 is
2032    * empty, this operator returns true.
2033    * Parameters: 2
2034    *   -[1]: Term of sort String (string s1)
2035    *   -[2]: Term of sort String (string s2)
2036    * Create with:
2037    *   mkTerm(Kind kind, Term child1, Term child2)
2038    *   mkTerm(Kind kind, const std::vector<Term>& children)
2039    */
2040   STRING_PREFIX,
2041   /**
2042    * String suffix-of.
2043    * Checks whether a string s1 is a suffix of string 2. If string s1 is empty,
2044    * this operator returns true.
2045    * Parameters: 2
2046    *   -[1]: Term of sort String (string s1)
2047    *   -[2]: Term of sort String (string s2)
2048    * Create with:
2049    *   mkTerm(Kind kind, Term child1, Term child2)
2050    *   mkTerm(Kind kind, const std::vector<Term>& children)
2051    */
2052   STRING_SUFFIX,
2053   /**
2054    * Integer to string.
2055    * If the integer is negative this operator returns the empty string.
2056    * Parameters: 1
2057    *   -[1]: Term of sort Integer
2058    * Create with:
2059    *   mkTerm(Kind kind, Term child)
2060    */
2061   STRING_ITOS,
2062   /**
2063    * String to integer (total function).
2064    * If the string does not contain an integer or the integer is negative, the
2065    * operator returns -1.
2066    * Parameters: 1
2067    *   -[1]: Term of sort String
2068    * Create with:
2069    *   mkTerm(Kind kind, Term child)
2070    */
2071   STRING_STOI,
2072   /**
2073    * Constant string.
2074    * Parameters:
2075    *   See mkString()
2076    * Create with:
2077    *   mkString(const char* s)
2078    *   mkString(const std::string& s)
2079    *   mkString(const unsigned char c)
2080    *   mkString(const std::vector<unsigned>& s)
2081    */
2082   CONST_STRING,
2083   /**
2084    * Conversion from string to regexp.
2085    * Parameters: 1
2086    *   -[1]: Term of sort String
2087    * Create with:
2088    *   mkTerm(Kind kind, Term child)
2089    */
2090   STRING_TO_REGEXP,
2091   /**
2092    * Regexp Concatenation .
2093    * Parameters: 2
2094    *   -[1]..[2]: Terms of Regexp sort
2095    * Create with:
2096    *   mkTerm(Kind kind, Term child1, Term child2)
2097    *   mkTerm(Kind kind, const std::vector<Term>& children)
2098    */
2099   REGEXP_CONCAT,
2100   /**
2101    * Regexp union.
2102    * Parameters: 2
2103    *   -[1]..[2]: Terms of Regexp sort
2104    * Create with:
2105    *   mkTerm(Kind kind, Term child1, Term child2)
2106    *   mkTerm(Kind kind, const std::vector<Term>& children)
2107    */
2108   REGEXP_UNION,
2109   /**
2110    * Regexp intersection.
2111    * Parameters: 2
2112    *   -[1]..[2]: Terms of Regexp sort
2113    * Create with:
2114    *   mkTerm(Kind kind, Term child1, Term child2)
2115    *   mkTerm(Kind kind, const std::vector<Term>& children)
2116    */
2117   REGEXP_INTER,
2118   /**
2119    * Regexp *.
2120    * Parameters: 1
2121    *   -[1]: Term of sort Regexp
2122    * Create with:
2123    *   mkTerm(Kind kind, Term child)
2124    */
2125   REGEXP_STAR,
2126   /**
2127    * Regexp +.
2128    * Parameters: 1
2129    *   -[1]: Term of sort Regexp
2130    * Create with:
2131    *   mkTerm(Kind kind, Term child)
2132    */
2133   REGEXP_PLUS,
2134   /**
2135    * Regexp ?.
2136    * Parameters: 1
2137    *   -[1]: Term of sort Regexp
2138    * Create with:
2139    *   mkTerm(Kind kind, Term child)
2140    */
2141   REGEXP_OPT,
2142   /**
2143    * Regexp range.
2144    * Parameters: 2
2145    *   -[1]: Lower bound character for the range
2146    *   -[2]: Upper bound character for the range
2147    * Create with:
2148    *   mkTerm(Kind kind, Term child1, Term child2)
2149    *   mkTerm(Kind kind, const std::vector<Term>& children)
2150    */
2151   REGEXP_RANGE,
2152   /**
2153    * Regexp loop.
2154    * Parameters: 2 (3)
2155    *   -[1]: Term of sort RegExp
2156    *   -[2]: Lower bound for the number of repetitions of the first argument
2157    *   -[3]: Upper bound for the number of repetitions of the first argument
2158    * Create with:
2159    *   mkTerm(Kind kind, Term child1, Term child2)
2160    *   mkTerm(Kind kind, Term child1, Term child2, Term child3)
2161    *   mkTerm(Kind kind, const std::vector<Term>& children)
2162    */
2163   REGEXP_LOOP,
2164   /**
2165    * Regexp empty.
2166    * Parameters: 0
2167    * Create with:
2168    *   mkRegexpEmpty()
2169    *   mkTerm(Kind kind)
2170    */
2171   REGEXP_EMPTY,
2172   /**
2173    * Regexp all characters.
2174    * Parameters: 0
2175    * Create with:
2176    *   mkRegexpSigma()
2177    *   mkTerm(Kind kind)
2178    */
2179   REGEXP_SIGMA,
2180 #if 0
2181   /* regexp rv (internal use only) */
2182   REGEXP_RV,
2183 #endif
2184
2185   /* Quantifiers ----------------------------------------------------------- */
2186
2187   /**
2188    * Universally quantified formula.
2189    * Parameters: 2 (3)
2190    *   -[1]: BOUND_VAR_LIST Term
2191    *   -[2]: Quantifier body
2192    *   -[3]: (optional) INST_PATTERN_LIST Term
2193    * Create with:
2194    *   mkTerm(Kind kind, Term child1, Term child2)
2195    *   mkTerm(Kind kind, Term child1, Term child2, Term child3)
2196    *   mkTerm(Kind kind, const std::vector<Term>& children)
2197    */
2198   FORALL,
2199   /**
2200    * Existentially quantified formula.
2201    * Parameters: 2 (3)
2202    *   -[1]: BOUND_VAR_LIST Term
2203    *   -[2]: Quantifier body
2204    *   -[3]: (optional) INST_PATTERN_LIST Term
2205    * Create with:
2206    *   mkTerm(Kind kind, Term child1, Term child2)
2207    *   mkTerm(Kind kind, Term child1, Term child2, Term child3)
2208    *   mkTerm(Kind kind, const std::vector<Term>& children)
2209    */
2210   EXISTS,
2211 #if 0
2212   /* instantiation constant */
2213   INST_CONSTANT,
2214   /* instantiation pattern */
2215   INST_PATTERN,
2216   /* a list of bound variables (used to bind variables under a quantifier) */
2217   BOUND_VAR_LIST,
2218   /* instantiation no-pattern */
2219   INST_NO_PATTERN,
2220   /* instantiation attribute */
2221   INST_ATTRIBUTE,
2222   /* a list of instantiation patterns */
2223   INST_PATTERN_LIST,
2224   /* predicate for specifying term in instantiation closure. */
2225   INST_CLOSURE,
2226   /* general rewrite rule (for rewrite-rules theory) */
2227   REWRITE_RULE,
2228   /* actual rewrite rule (for rewrite-rules theory) */
2229   RR_REWRITE,
2230   /* actual reduction rule (for rewrite-rules theory) */
2231   RR_REDUCTION,
2232   /* actual deduction rule (for rewrite-rules theory) */
2233   RR_DEDUCTION,
2234
2235   /* Sort Kinds ------------------------------------------------------------ */
2236
2237   /* array type */
2238    ARRAY_TYPE,
2239   /* a type parameter for type ascription */
2240   ASCRIPTION_TYPE,
2241   /* constructor */
2242   CONSTRUCTOR_TYPE,
2243   /* a datatype type index */
2244   DATATYPE_TYPE,
2245   /* selector */
2246   SELECTOR_TYPE,
2247   /* set type, takes as parameter the type of the elements */
2248   SET_TYPE,
2249   /* sort tag */
2250   SORT_TAG,
2251   /* specifies types of user-declared 'uninterpreted' sorts */
2252   SORT_TYPE,
2253   /* tester */
2254   TESTER_TYPE,
2255   /* a representation for basic types */
2256   TYPE_CONSTANT,
2257   /* a function type */
2258   FUNCTION_TYPE,
2259   /* the type of a symbolic expression */
2260   SEXPR_TYPE,
2261   /* bit-vector type */
2262   BITVECTOR_TYPE,
2263   /* floating-point type */
2264   FLOATINGPOINT_TYPE,
2265 #endif
2266
2267   /* ----------------------------------------------------------------------- */
2268   /* marks the upper-bound of this enumeration */
2269   LAST_KIND
2270 };
2271
2272 /**
2273  * Get the string representation of a given kind.
2274  * @param k the kind
2275  * @return the string representation of kind k
2276  */
2277 std::string kindToString(Kind k) CVC4_PUBLIC;
2278
2279 /**
2280  * Serialize a kind to given stream.
2281  * @param out the output stream
2282  * @param k the kind to be serialized to the given output stream
2283  * @return the output stream
2284  */
2285 std::ostream& operator<<(std::ostream& out, Kind k) CVC4_PUBLIC;
2286
2287 /**
2288  * Hash function for Kinds.
2289  */
2290 struct CVC4_PUBLIC KindHashFunction
2291 {
2292   size_t operator()(Kind k) const;
2293 };
2294
2295 }  // namespace api
2296 }  // namespace CVC4
2297
2298 #endif