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