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