Header for new C++ API. (#1697)

1 files changed, 2334 insertions, 0 deletions

diff --git a/src/api/cvc4cppkind.h b/src/api/cvc4cppkind.h
new file mode 100644
index 000000000..afa1e29f9
--- /dev/null
+++ b/src/api/cvc4cppkind.h
@@ -0,0 +1,2334 @@
+/*********************                                                        */
+/*! \file cvc4cpp.h
+ ** \verbatim
+ ** Top authors (to current version): Aina Niemetz
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief The term kinds of the CVC4 C++ API.
+ **
+ ** The term kinds of the CVC4 C++ API.
+ **/
+
+#include "cvc4_public.h"
+
+#ifndef __CVC4__API__CVC4CPPKIND_H
+#define __CVC4__API__CVC4CPPKIND_H
+
+#include <ostream>
+
+namespace CVC4 {
+namespace api {
+
+/* -------------------------------------------------------------------------- */
+/* Kind                                                                       */
+/* -------------------------------------------------------------------------- */
+
+/**
+ * The kind of a CVC4 term.
+ */
+enum CVC4_PUBLIC Kind
+{
+  /**
+   * Internal kind.
+   * Should never be exposed or created via the API.
+   */
+  INTERNAL_KIND = -2,
+  /**
+   * Undefined kind.
+   * Should never be exposed or created via the API.
+   */
+  UNDEFINED_KIND = -1,
+  /**
+   * Null kind (kind of null term Term()).
+   * Do not explicitly create via API functions other than Term().
+   */
+  NULL_EXPR,
+
+  /* Builtin --------------------------------------------------------------- */
+
+  /**
+   * Uninterpreted constant.
+   * Parameters: 2
+   *   -[1]: Sort of the constant
+   *   -[2]: Index of the constant
+   * Create with:
+   *   mkConst(Kind, Sort, int32_t)
+   */
+  UNINTERPRETED_CONSTANT,
+  /**
+   * Abstract value (other than uninterpreted sort constants).
+   * Parameters: 1
+   *   -[1]: Index of the abstract value
+   * Create with:
+   *   mkConst(Kind kind, const char* s, uint32_t base = 10)
+   *   mkConst(Kind kind, const std::string& s, uint32_t base = 10)
+   *   mkConst(Kind kind, uint32_t arg)
+   *   mkConst(Kind kind, int32_t arg)
+   *   mkConst(Kind kind, int64_t arg)
+   *   mkConst(Kind kind, uint64_t arg)
+   */
+  ABSTRACT_VALUE,
+#if 0
+  /* Built-in operator */
+  BUILTIN,
+#endif
+  /**
+   * Defined function.
+   * Parameters: 3 (4)
+   *   See defineFun().
+   * Create with:
+   *   defineFun(const std::string& symbol,
+   *             const std::vector<Term>& bound_vars,
+   *             Sort sort,
+   *             Term term)
+   *   defineFun(Term fun,
+   *             const std::vector<Term>& bound_vars,
+   *             Term term)
+   */
+  FUNCTION,
+  /**
+   * Application of a defined function.
+   * Parameters: n > 1
+   *   -[1]..[n]: Function argument instantiation Terms
+   * Create with:
+   *   mkTerm(Kind kind, Term child)
+   *   mkTerm(Kind kind, Term child1, Term child2)
+   *   mkTerm(Kind kind, Term child1, Term child2, Term child3)
+   *   mkTerm(Kind kind, const std::vector<Term>& children)
+   */
+  APPLY,
+  /**
+   * Equality.
+   * Parameters: 2
+   *   -[1]..[2]: Terms with same sort
+   * Create with:
+   *   mkTerm(Kind kind, Term child1, Term child2)
+   *   mkTerm(Kind kind, const std::vector<Term>& children)
+   */
+  EQUAL,
+  /**
+   * Disequality.
+   * Parameters: n > 1
+   *   -[1]..[n]: Terms with same sort
+   * Create with:
+   *   mkTerm(Kind kind, Term child1, Term child2)
+   *   mkTerm(Kind kind, Term child1, Term child2, Term child3)
+   *   mkTerm(Kind kind, const std::vector<Term>& children)
+   */
+  DISTINCT,
+  /**
+   * Variable.
+   * Not permitted in bindings (forall, exists, ...).
+   * Parameters:
+   *   See mkVar().
+   * Create with:
+   *   mkVar(const std::string& symbol, Sort sort)
+   *   mkVar(Sort sort)
+   */
+  VARIABLE,
+  /**
+   * Bound variable.
+   * Permitted in bindings and in the lambda and quantifier bodies only.
+   * Parameters:
+   *   See mkBoundVar().
+   * Create with:
+   *   mkBoundVar(const std::string& symbol, Sort sort)
+   *   mkBoundVar(Sort sort)
+   */
+  BOUND_VARIABLE,
+#if 0
+  /* Skolem variable (internal only) */
+  SKOLEM,
+  /* Symbolic expression (any arity) */
+  SEXPR,
+#endif
+  /**
+   * Lambda expression.
+   * Parameters: 2
+   *   -[1]: BOUND_VAR_LIST
+   *   -[2]: Lambda body
+   * Create with:
+   *   mkTerm(Kind kind, Term child1, Term child2)
+   *   mkTerm(Kind kind, const std::vector<Term>& children)
+   */
+  LAMBDA,
+  /**
+   * Hilbert choice (epsilon) expression.
+   * Parameters: 2
+   *   -[1]: BOUND_VAR_LIST
+   *   -[2]: Hilbert choice body
+   * Create with:
+   *   mkTerm(Kind kind, Term child1, Term child2)
+   *   mkTerm(Kind kind, const std::vector<Term>& children)
+   */
+  CHOICE,
+  /**
+   * Chained operation.
+   * Parameters: n > 1
+   *   -[1]: Term of kind CHAIN_OP (represents a binary op)
+   *   -[2]..[n]: Arguments to that operator
+   * Create with:
+   *   mkTerm(Kind kind, Term child1, Term child2)
+   *   mkTerm(Kind kind, Term child1, Term child2, Term child3)
+   *   mkTerm(Kind kind, const std::vector<Term>& children)
+   * Turned into a conjunction of binary applications of the operator on
+   * adjoining parameters.
+   */
+  CHAIN,
+  /**
+   * Chained operator.
+   * Parameters: 1
+   *   -[1]: Kind of the binary operation
+   * Create with:
+   *   mkOpTerm(Kind opkind, Kind kind)
+   */
+  CHAIN_OP,
+
+  /* Boolean --------------------------------------------------------------- */
+
+  /**
+   * Boolean constant.
+   * Parameters: 1
+   *   -[1]: Boolean value of the constant
+   * Create with:
+   *   mkTrue()
+   *   mkFalse()
+   *   mkBoolean(bool val)
+   *   mkConst(Kind kind, bool arg)
+   */
+  CONST_BOOLEAN,
+  /* Logical not.
+   * Parameters: 1
+   *   -[1]: Boolean Term to negate
+   * Create with:
+   *   mkTerm(Kind kind, Term child)
+   */
+  NOT,
+  /* Logical and.
+   * Parameters: n > 1
+   *   -[1]..[n]: Boolean Term of the conjunction
+   * Create with:
+   *   mkTerm(Kind kind, Term child1, Term child2)
+   *   mkTerm(Kind kind, Term child1, Term child2, Term child3)
+   *   mkTerm(Kind kind, const std::vector<Term>& children)
+   */
+  AND,
+  /**
+   * Logical implication.
+   * Parameters: 2
+   *   -[1]..[2]: Boolean Terms, [1] implies [2]
+   * Create with:
+   *   mkTerm(Kind kind, Term child1, Term child2)
+   *   mkTerm(Kind kind, const std::vector<Term>& children)
+   */
+  IMPLIES,
+  /* Logical or.
+   * Parameters: n > 1
+   *   -[1]..[n]: Boolean Term of the disjunction
+   * Create with:
+   *   mkTerm(Kind kind, Term child1, Term child2)
+   *   mkTerm(Kind kind, Term child1, Term child2, Term child3)
+   *   mkTerm(Kind kind, const std::vector<Term>& children)
+   */
+  OR,
+  /* Logical exclusive or.
+   * Parameters: 2
+   *   -[1]..[2]: Boolean Terms, [1] xor [2]
+   * Create with:
+   *   mkTerm(Kind kind, Term child1, Term child2)
+   *   mkTerm(Kind kind, const std::vector<Term>& children)
+   */
+  XOR,
+  /* If-then-else.
+   * Parameters: 3
+   *   -[1] is a Boolean condition Term
+   *   -[2] the 'then' Term
+   *   -[3] the 'else' Term
+   * 'then' and 'else' term must have same base sort.
+   * Create with:
+   *   mkTerm(Kind kind, Term child1, Term child2, Term child3)
+   *   mkTerm(Kind kind, const std::vector<Term>& children)
+   */
+  ITE,
+
+  /* UF -------------------------------------------------------------------- */
+
+  /* Application of an uninterpreted function.
+   * Parameters: n > 1
+   *   -[1]: Function Term
+   *   -[2]..[n]: Function argument instantiation Terms
+   * Create with:
+   *   mkTerm(Kind kind, Term child1, Term child2)
+   *   mkTerm(Kind kind, Term child1, Term child2, Term child3)
+   *   mkTerm(Kind kind, const std::vector<Term>& children)
+   */
+  APPLY_UF,
+#if 0
+  /* Boolean term variable */
+  BOOLEAN_TERM_VARIABLE,
+#endif
+  /**
+   * Cardinality constraint on sort S.
+   * Parameters: 2
+   *   -[1]: Term of sort S
+   *   -[2]: Positive integer constant that bounds the cardinality of sort S
+   * Create with:
+   *   mkTerm(Kind kind, Term child1, Term child2)
+   *   mkTerm(Kind kind, const std::vector<Term>& children)
+   */
+  CARDINALITY_CONSTRAINT,
+#if 0
+  /* Combined cardinality constraint.  */
+  COMBINED_CARDINALITY_CONSTRAINT,
+  /* Partial uninterpreted function application.  */
+  PARTIAL_APPLY_UF,
+  /* cardinality value of sort S:
+   * first parameter is (any) term of sort S */
+   CARDINALITY_VALUE,
+#endif
+  /**
+   * Higher-order applicative encoding of function application.
+   * Parameters: 2
+   *   -[1]: Function to apply
+   *   -[2]: Argument of the function
+   * Create with:
+   *   mkTerm(Kind kind, Term child1, Term child2)
+   *   mkTerm(Kind kind, const std::vector<Term>& children)
+   */
+  HO_APPLY,
+
+  /* Arithmetic ------------------------------------------------------------ */
+
+  /**
+   * Arithmetic addition.
+   * Parameters: n > 1
+   *   -[1]..[n]: Terms of sort Integer, Real (sorts must match)
+   * Create with:
+   *   mkTerm(Kind kind, Term child1, Term child2)
+   *   mkTerm(Kind kind, Term child1, Term child2, Term child3)
+   *   mkTerm(Kind kind, const std::vector<Term>& children)
+   */
+  PLUS,
+  /**
+   * Arithmetic multiplication.
+   * Parameters: n > 1
+   *   -[1]..[n]: Terms of sort Integer, Real (sorts must match)
+   * Create with:
+   *   mkTerm(Kind kind, Term child1, Term child2)
+   *   mkTerm(Kind kind, Term child1, Term child2, Term child3)
+   *   mkTerm(Kind kind, const std::vector<Term>& children)
+   */
+  MULT,
+#if 0
+  /* Synonym for MULT.  */
+  NONLINEAR_MULT,
+#endif
+  /**
+   * Arithmetic subtraction.
+   * Parameters: 2
+   *   -[1]..[2]: Terms of sort Integer, Real (sorts must match)
+   * Create with:
+   *   mkTerm(Kind kind, Term child1, Term child2)
+   *   mkTerm(Kind kind, const std::vector<Term>& children)
+   */
+  MINUS,
+  /**
+   * Arithmetic negation.
+   * Parameters: 1
+   *   -[1]: Term of sort Integer, Real
+   * Create with:
+   *   mkTerm(Kind kind, Term child)
+   */
+  UMINUS,
+  /**
+   * Real division, division by 0 undefined
+   * Parameters: 2
+   *   -[1]..[2]: Terms of sort Integer, Real
+   * Create with:
+   *   mkTerm(Kind kind, Term child1, Term child2)
+   *   mkTerm(Kind kind, const std::vector<Term>& children)
+   */
+  DIVISION,
+  /**
+   * Real division with interpreted division by 0
+   * Parameters: 2
+   *   -[1]..[2]: Terms of sort Integer, Real
+   * Create with:
+   *   mkTerm(Kind kind, Term child1, Term child2)
+   *   mkTerm(Kind kind, const std::vector<Term>& children)
+   */
+  DIVISION_TOTAL,
+  /**
+   * Integer division, division by 0 undefined.
+   * Parameters: 2
+   *   -[1]..[2]: Terms of sort Integer
+   * Create with:
+   *   mkTerm(Kind kind, Term child1, Term child2)
+   *   mkTerm(Kind kind, const std::vector<Term>& children)
+   */
+  INTS_DIVISION,
+  /**
+   * Integer division with interpreted division by 0.
+   * Parameters: 2
+   *   -[1]..[2]: Terms of sort Integer
+   * Create with:
+   *   mkTerm(Kind kind, Term child1, Term child2)
+   *   mkTerm(Kind kind, const std::vector<Term>& children)
+   */
+  INTS_DIVISION_TOTAL,
+  /**
+   * Integer modulus, division by 0 undefined.
+   * Parameters: 2
+   *   -[1]..[2]: Terms of sort Integer
+   * Create with:
+   *   mkTerm(Kind kind, Term child1, Term child2)
+   *   mkTerm(Kind kind, const std::vector<Term>& children)
+   */
+  INTS_MODULUS,
+  /**
+   * Integer modulus with interpreted division by 0.
+   * Parameters: 2
+   *   -[1]..[2]: Terms of sort Integer
+   * Create with:
+   *   mkTerm(Kind kind, Term child1, Term child2)
+   *   mkTerm(Kind kind, const std::vector<Term>& children)
+   */
+  INTS_MODULUS_TOTAL,
+  /**
+   * Absolute value.
+   * Parameters: 1
+   *   -[1]: Term of sort Integer
+   * Create with:
+   *   mkTerm(Kind kind, Term child)
+   */
+  ABS,
+  /**
+   * Divisibility-by-k predicate.
+   * Parameters: 2
+   *   -[1]: DIVISIBLE_OP Term
+   *   -[2]: Integer Term
+   * Create with:
+   *   mkTerm(Kind kind, Term child1, Term child2)
+   *   mkTerm(Kind kind, const std::vector<Term>& children)
+   */
+  DIVISIBLE,
+  /**
+   * Arithmetic power.
+   * Parameters: 2
+   *   -[1]..[2]: Terms of sort Integer, Real
+   * Create with:
+   *   mkTerm(Kind kind, Term child1, Term child2)
+   *   mkTerm(Kind kind, const std::vector<Term>& children)
+   */
+  POW,
+  /**
+   * Exponential.
+   * Parameters: 1
+   *   -[1]: Term of sort Integer, Real
+   * Create with:
+   *   mkTerm(Kind kind, Term child)
+   */
+  EXPONENTIAL,
+  /**
+   * Sine.
+   * Parameters: 1
+   *   -[1]: Term of sort Integer, Real
+   * Create with:
+   *   mkTerm(Kind kind, Term child)
+   */
+  SINE,
+  /**
+   * Cosine.
+   * Parameters: 1
+   *   -[1]: Term of sort Integer, Real
+   * Create with:
+   *   mkTerm(Kind kind, Term child)
+   */
+  COSINE,
+  /**
+   * Tangent.
+   * Parameters: 1
+   *   -[1]: Term of sort Integer, Real
+   * Create with:
+   *   mkTerm(Kind kind, Term child)
+   */
+  TANGENT,
+  /**
+   * Cosecant.
+   * Parameters: 1
+   *   -[1]: Term of sort Integer, Real
+   * Create with:
+   *   mkTerm(Kind kind, Term child)
+   */
+  COSECANT,
+  /**
+   * Secant.
+   * Parameters: 1
+   *   -[1]: Term of sort Integer, Real
+   * Create with:
+   *   mkTerm(Kind kind, Term child)
+   */
+  SECANT,
+  /**
+   * Cotangent.
+   * Parameters: 1
+   *   -[1]: Term of sort Integer, Real
+   * Create with:
+   *   mkTerm(Kind kind, Term child)
+   */
+  COTANGENT,
+  /**
+   * Arc sine.
+   * Parameters: 1
+   *   -[1]: Term of sort Integer, Real
+   * Create with:
+   *   mkTerm(Kind kind, Term child)
+   */
+  ARCSINE,
+  /**
+   * Arc cosine.
+   * Parameters: 1
+   *   -[1]: Term of sort Integer, Real
+   * Create with:
+   *   mkTerm(Kind kind, Term child)
+   */
+  ARCCOSINE,
+  /**
+   * Arc tangent.
+   * Parameters: 1
+   *   -[1]: Term of sort Integer, Real
+   * Create with:
+   *   mkTerm(Kind kind, Term child)
+   */
+  ARCTANGENT,
+  /**
+   * Arc cosecant.
+   * Parameters: 1
+   *   -[1]: Term of sort Integer, Real
+   * Create with:
+   *   mkTerm(Kind kind, Term child)
+   */
+  ARCCOSECANT,
+  /**
+   * Arc secant.
+   * Parameters: 1
+   *   -[1]: Term of sort Integer, Real
+   * Create with:
+   *   mkTerm(Kind kind, Term child)
+   */
+  ARCSECANT,
+  /**
+   * Arc cotangent.
+   * Parameters: 1
+   *   -[1]: Term of sort Integer, Real
+   * Create with:
+   *   mkTerm(Kind kind, Term child)
+   */
+  ARCCOTANGENT,
+  /**
+   * Square root.
+   * Parameters: 1
+   *   -[1]: Term of sort Integer, Real
+   * Create with:
+   *   mkTerm(Kind kind, Term child)
+   */
+  SQRT,
+  /**
+   * Operator for the divisibility-by-k predicate.
+   * Parameter: 1
+   *   -[1]: The k to divide by (sort Integer)
+   * Create with:
+   *   mkOpTerm(Kind kind, uint32_t param)
+   */
+  DIVISIBLE_OP,
+  /**
+   * Multiple-precision rational constant.
+   * Parameters:
+   *   See mkInteger(), mkReal(), mkRational()
+   * Create with:
+   *   mkInteger(const char* s, uint32_t base = 10)
+   *   mkInteger(const std::string& s, uint32_t base = 10)
+   *   mkInteger(int32_t val)
+   *   mkInteger(uint32_t val)
+   *   mkInteger(int64_t val)
+   *   mkInteger(uint64_t val)
+   *   mkReal(const char* s, uint32_t base = 10)
+   *   mkReal(const std::string& s, uint32_t base = 10)
+   *   mkReal(int32_t val)
+   *   mkReal(int64_t val)
+   *   mkReal(uint32_t val)
+   *   mkReal(uint64_t val)
+   *   mkRational(int32_t num, int32_t den)
+   *   mkRational(int64_t num, int64_t den)
+   *   mkRational(uint32_t num, uint32_t den)
+   *   mkRational(uint64_t num, uint64_t den)
+   *   mkConst(Kind kind, const char* s, uint32_t base = 10)
+   *   mkConst(Kind kind, const std::string& s, uint32_t base = 10)
+   *   mkConst(Kind kind, uint32_t arg)
+   *   mkConst(Kind kind, int64_t arg)
+   *   mkConst(Kind kind, uint64_t arg)
+   *   mkConst(Kind kind, int32_t arg)
+   *   mkConst(Kind kind, int32_t arg1, int32_t arg2)
+   *   mkConst(Kind kind, int64_t arg1, int64_t arg2)
+   *   mkConst(Kind kind, uint32_t arg1, uint32_t arg2)
+   *   mkConst(Kind kind, uint64_t arg1, uint64_t arg2)
+   */
+  CONST_RATIONAL,
+  /**
+   * Less than.
+   * Parameters: 2
+   *   -[1]..[2]: Terms of sort Integer, Real; [1] < [2]
+   * Create with:
+   *   mkTerm(Kind kind, Term child1, Term child2)
+   *   mkTerm(Kind kind, const std::vector<Term>& children)
+   */
+  LT,
+  /**
+   * Less than or equal.
+   * Parameters: 2
+   *   -[1]..[2]: Terms of sort Integer, Real; [1] <= [2]
+   * Create with:
+   *   mkTerm(Kind kind, Term child1, Term child2)
+   *   mkTerm(Kind kind, const std::vector<Term>& children)
+   */
+  LEQ,
+  /**
+   * Greater than.
+   * Parameters: 2
+   *   -[1]..[2]: Terms of sort Integer, Real, [1] > [2]
+   * Create with:
+   *   mkTerm(Kind kind, Term child1, Term child2)
+   *   mkTerm(Kind kind, const std::vector<Term>& children)
+   */
+  GT,
+  /**
+   * Greater than or equal.
+   * Parameters: 2
+   *   -[1]..[2]: Terms of sort Integer, Real; [1] >= [2]
+   * Create with:
+   *   mkTerm(Kind kind, Term child1, Term child2)
+   *   mkTerm(Kind kind, const std::vector<Term>& children)
+   */
+  GEQ,
+  /**
+   * Is-integer predicate.
+   * Parameters: 1
+   *   -[1]: Term of sort Integer, Real
+   * Create with:
+   *   mkTerm(Kind kind, Term child)
+   */
+  IS_INTEGER,
+  /**
+   * Convert Term to Integer by the floor function.
+   * Parameters: 1
+   *   -[1]: Term of sort Integer, Real
+   * Create with:
+   *   mkTerm(Kind kind, Term child)
+   */
+  TO_INTEGER,
+  /**
+   * Convert Term to Real.
+   * Parameters: 1
+   *   -[1]: Term of sort Integer, Real
+   * This is a no-op in CVC4, as Integer is a subtype of Real.
+   */
+  TO_REAL,
+  /**
+   * Pi constant.
+   * Create with:
+   *   mkPi()
+   *   mkTerm(Kind kind)
+   */
+  PI,
+
+  /* BV -------------------------------------------------------------------- */
+
+  /**
+   * Fixed-size bit-vector constant.
+   * Parameters:
+   *   See mkBitVector().
+   * Create with:
+   *   mkBitVector(uint32_t size)
+   *   mkBitVector(uint32_t size, uint32_t val)
+   *   mkBitVector(uint32_t size, uint64_t val)
+   *   mkBitVector(const char* s, uint32_t base = 2)
+   *   mkBitVector(std::string& s, uint32_t base = 2)
+   *   mkConst(Kind kind, const char* s, uint32_t base = 10)
+   *   mkConst(Kind kind, const std::string& s, uint32_t base = 10)
+   *   mkConst(Kind kind, uint32_t arg)
+   *   mkConst(Kind kind, uint32_t arg1, uint64_t arg2)
+   */
+  CONST_BITVECTOR,
+  /**
+   * Concatenation of two or more bit-vectors.
+   * Parameters: n > 1
+   *   -[1]..[n]: Terms of bit-vector sort
+   * Create with:
+   *   mkTerm(Kind kind, Term child1, Term child2)
+   *   mkTerm(Kind kind, Term child1, Term child2, Term child3)
+   *   mkTerm(Kind kind, const std::vector<Term>& children)
+   */
+  BITVECTOR_CONCAT,
+  /**
+   * Bit-wise and.
+   * Parameters: n > 1
+   *   -[1]..[n]: Terms of bit-vector sort (sorts must match)
+   * Create with:
+   *   mkTerm(Kind kind, Term child1, Term child2)
+   *   mkTerm(Kind kind, Term child1, Term child2, Term child3)
+   *   mkTerm(Kind kind, const std::vector<Term>& children)
+   */
+  BITVECTOR_AND,
+  /**
+   * Bit-wise or.
+   * Parameters: n > 1
+   *   -[1]..[n]: Terms of bit-vector sort (sorts must match)
+   * Create with:
+   *   mkTerm(Kind kind, Term child1, Term child2)
+   *   mkTerm(Kind kind, Term child1, Term child2, Term child3)
+   *   mkTerm(Kind kind, const std::vector<Term>& children)
+   */
+  BITVECTOR_OR,
+  /**
+   * Bit-wise xor.
+   * Parameters: n > 1
+   *   -[1]..[n]: Terms of bit-vector sort (sorts must match)
+   * Create with:
+   *   mkTerm(Kind kind, Term child1, Term child2)
+   *   mkTerm(Kind kind, Term child1, Term child2, Term child3)
+   *   mkTerm(Kind kind, const std::vector<Term>& children)
+   */
+  BITVECTOR_XOR,
+  /**
+   * Bit-wise negation.
+   * Parameters: 1
+   *   -[1]: Term of bit-vector sort
+   * Create with:
+   *   mkTerm(Kind kind, Term child)
+   */
+  BITVECTOR_NOT,
+  /**
+   * Bit-wise nand.
+   * Parameters: 2
+   *   -[1]..[2]: Terms of bit-vector sort (sorts must match)
+   * Create with:
+   *   mkTerm(Kind kind, Term child1, Term child2)
+   *   mkTerm(Kind kind, const std::vector<Term>& children)
+   */
+  BITVECTOR_NAND,
+  /**
+   * Bit-wise nor.
+   * Parameters: 2
+   *   -[1]..[2]: Terms of bit-vector sort (sorts must match)
+   * Create with:
+   *   mkTerm(Kind kind, Term child1, Term child2)
+   *   mkTerm(Kind kind, const std::vector<Term>& children)
+   */
+  BITVECTOR_NOR,
+  /**
+   * Bit-wise xnor.
+   * Parameters: 2
+   *   -[1]..[2]: Terms of bit-vector sort (sorts must match)
+   * Create with:
+   *   mkTerm(Kind kind, Term child1, Term child2)
+   *   mkTerm(Kind kind, const std::vector<Term>& children)
+   */
+  BITVECTOR_XNOR,
+  /**
+   * Equality comparison (returns bit-vector of size 1).
+   * Parameters: 2
+   *   -[1]..[2]: Terms of bit-vector sort (sorts must match)
+   * Create with:
+   *   mkTerm(Kind kind, Term child1, Term child2)
+   *   mkTerm(Kind kind, const std::vector<Term>& children)
+   */
+  BITVECTOR_COMP,
+  /**
+   * Multiplication of two or more bit-vectors.
+   * Parameters: n > 1
+   *   -[1]..[n]: Terms of bit-vector sort (sorts must match)
+   * Create with:
+   *   mkTerm(Kind kind, Term child1, Term child2)
+   *   mkTerm(Kind kind, Term child1, Term child2, Term child3)
+   *   mkTerm(Kind kind, const std::vector<Term>& children)
+   */
+  BITVECTOR_MULT,
+  /**
+   * Addition of two or more bit-vectors.
+   * Parameters: n > 1
+   *   -[1]..[n]: Terms of bit-vector sort (sorts must match)
+   * Create with:
+   *   mkTerm(Kind kind, Term child1, Term child2)
+   *   mkTerm(Kind kind, Term child1, Term child2, Term child3)
+   *   mkTerm(Kind kind, const std::vector<Term>& children)
+   */
+  BITVECTOR_PLUS,
+  /**
+   * Subtraction of two bit-vectors.
+   * Parameters: 2
+   *   -[1]..[2]: Terms of bit-vector sort (sorts must match)
+   * Create with:
+   *   mkTerm(Kind kind, Term child1, Term child2)
+   *   mkTerm(Kind kind, const std::vector<Term>& children)
+   */
+  BITVECTOR_SUB,
+  /**
+   * Negation of a bit-vector (two's complement).
+   * Parameters: 1
+   *   -[1]: Term of bit-vector sort
+   * Create with:
+   *   mkTerm(Kind kind, Term child)
+   */
+  BITVECTOR_NEG,
+  /**
+   * Unsigned division of two bit-vectors, truncating towards 0.
+   * Parameters: 2
+   *   -[1]..[2]: Terms of bit-vector sort (sorts must match)
+   * Create with:
+   *   mkTerm(Kind kind, Term child1, Term child2)
+   *   mkTerm(Kind kind, const std::vector<Term>& children)
+   */
+  BITVECTOR_UDIV,
+  /**
+   * Unsigned remainder from truncating division of two bit-vectors.
+   * Parameters: 2
+   *   -[1]..[2]: Terms of bit-vector sort (sorts must match)
+   * Create with:
+   *   mkTerm(Kind kind, Term child1, Term child2)
+   *   mkTerm(Kind kind, const std::vector<Term>& children)
+   */
+  BITVECTOR_UREM,
+  /**
+   * Two's complement signed division of two bit-vectors.
+   * Parameters: 2
+   *   -[1]..[2]: Terms of bit-vector sort (sorts must match)
+   * Create with:
+   *   mkTerm(Kind kind, Term child1, Term child2)
+   *   mkTerm(Kind kind, const std::vector<Term>& children)
+   */
+  BITVECTOR_SDIV,
+  /**
+   * Two's complement signed remainder of two bit-vectors
+   * (sign follows dividend).
+   * Parameters: 2
+   *   -[1]..[2]: Terms of bit-vector sort (sorts must match)
+   * Create with:
+   *   mkTerm(Kind kind, Term child1, Term child2)
+   *   mkTerm(Kind kind, const std::vector<Term>& children)
+   */
+  BITVECTOR_SREM,
+  /**
+   * Two's complement signed remainder
+   * (sign follows divisor).
+   * Parameters: 2
+   *   -[1]..[2]: Terms of bit-vector sort (sorts must match)
+   * Create with:
+   *   mkTerm(Kind kind, Term child1, Term child2)
+   *   mkTerm(Kind kind, const std::vector<Term>& children)
+   */
+  BITVECTOR_SMOD,
+  /**
+   * Unsigned division of two bit-vectors, truncating towards 0
+   * (defined to be the all-ones bit pattern, if divisor is 0).
+   * Parameters: 2
+   *   -[1]..[2]: Terms of bit-vector sort (sorts must match)
+   * Create with:
+   *   mkTerm(Kind kind, Term child1, Term child2)
+   *   mkTerm(Kind kind, const std::vector<Term>& children)
+   */
+  BITVECTOR_UDIV_TOTAL,
+  /**
+   * Unsigned remainder from truncating division of two bit-vectors
+   * (defined to be equal to the dividend, if divisor is 0).
+   * Parameters: 2
+   *   -[1]..[2]: Terms of bit-vector sort (sorts must match)
+   * Create with:
+   *   mkTerm(Kind kind, Term child1, Term child2)
+   *   mkTerm(Kind kind, const std::vector<Term>& children)
+   */
+  BITVECTOR_UREM_TOTAL,
+  /**
+   * Bit-vector shift left.
+   * The two bit-vector parameters must have same width.
+   * Parameters: 2
+   *   -[1]..[2]: Terms of bit-vector sort (sorts must match)
+   * Create with:
+   *   mkTerm(Kind kind, Term child1, Term child2)
+   *   mkTerm(Kind kind, const std::vector<Term>& children)
+   */
+  BITVECTOR_SHL,
+  /**
+   * Bit-vector logical shift right.
+   * The two bit-vector parameters must have same width.
+   * Parameters: 2
+   *   -[1]..[2]: Terms of bit-vector sort (sorts must match)
+   * Create with:
+   *   mkTerm(Kind kind, Term child1, Term child2)
+   *   mkTerm(Kind kind, const std::vector<Term>& children)
+   */
+  BITVECTOR_LSHR,
+  /**
+   * Bit-vector arithmetic shift right.
+   * The two bit-vector parameters must have same width.
+   * Parameters: 2
+   *   -[1]..[2]: Terms of bit-vector sort (sorts must match)
+   * Create with:
+   *   mkTerm(Kind kind, Term child1, Term child2)
+   *   mkTerm(Kind kind, const std::vector<Term>& children)
+   */
+  BITVECTOR_ASHR,
+  /**
+   * Bit-vector unsigned less than.
+   * The two bit-vector parameters must have same width.
+   * Parameters: 2
+   *   -[1]..[2]: Terms of bit-vector sort (sorts must match)
+   * Create with:
+   *   mkTerm(Kind kind, Term child1, Term child2)
+   *   mkTerm(Kind kind, const std::vector<Term>& children)
+   */
+  BITVECTOR_ULT,
+  /**
+   * Bit-vector unsigned less than or equal.
+   * The two bit-vector parameters must have same width.
+   * Parameters: 2
+   *   -[1]..[2]: Terms of bit-vector sort (sorts must match)
+   * Create with:
+   *   mkTerm(Kind kind, Term child1, Term child2)
+   *   mkTerm(Kind kind, const std::vector<Term>& children)
+   */
+  BITVECTOR_ULE,
+  /**
+   * Bit-vector unsigned greater than.
+   * The two bit-vector parameters must have same width.
+   * Parameters: 2
+   *   -[1]..[2]: Terms of bit-vector sort (sorts must match)
+   * Create with:
+   *   mkTerm(Kind kind, Term child1, Term child2)
+   *   mkTerm(Kind kind, const std::vector<Term>& children)
+   */
+  BITVECTOR_UGT,
+  /**
+   * Bit-vector unsigned greater than or equal.
+   * The two bit-vector parameters must have same width.
+   * Parameters: 2
+   * Create with:
+   *   mkTerm(Kind kind, Term child1, Term child2)
+   *   mkTerm(Kind kind, const std::vector<Term>& children)
+   */
+  BITVECTOR_UGE,
+  /* Bit-vector signed less than.
+   * The two bit-vector parameters must have same width.
+   * Parameters: 2
+   * Create with:
+   *   mkTerm(Kind kind, Term child1, Term child2)
+   *   mkTerm(Kind kind, const std::vector<Term>& children)
+   */
+  BITVECTOR_SLT,
+  /**
+   * Bit-vector signed less than or equal.
+   * The two bit-vector parameters must have same width.
+   * Parameters: 2
+   *   -[1]..[2]: Terms of bit-vector sort (sorts must match)
+   * Create with:
+   *   mkTerm(Kind kind, Term child1, Term child2)
+   *   mkTerm(Kind kind, const std::vector<Term>& children)
+   */
+  BITVECTOR_SLE,
+  /**
+   * Bit-vector signed greater than.
+   * The two bit-vector parameters must have same width.
+   * Parameters: 2
+   *   -[1]..[2]: Terms of bit-vector sort (sorts must match)
+   * Create with:
+   *   mkTerm(Kind kind, Term child1, Term child2)
+   *   mkTerm(Kind kind, const std::vector<Term>& children)
+   */
+  BITVECTOR_SGT,
+  /**
+   * Bit-vector signed greater than or equal.
+   * The two bit-vector parameters must have same width.
+   * Parameters: 2
+   *   -[1]..[2]: Terms of bit-vector sort (sorts must match)
+   * Create with:
+   *   mkTerm(Kind kind, Term child1, Term child2)
+   *   mkTerm(Kind kind, const std::vector<Term>& children)
+   */
+  BITVECTOR_SGE,
+  /**
+   * Bit-vector unsigned less than, returns bit-vector of size 1.
+   * Parameters: 2
+   *   -[1]..[2]: Terms of bit-vector sort (sorts must match)
+   * Create with:
+   *   mkTerm(Kind kind, Term child1, Term child2)
+   *   mkTerm(Kind kind, const std::vector<Term>& children)
+   */
+  BITVECTOR_ULTBV,
+  /**
+   * Bit-vector signed less than. returns bit-vector of size 1.
+   * Parameters: 2
+   *   -[1]..[2]: Terms of bit-vector sort (sorts must match)
+   * Create with:
+   *   mkTerm(Kind kind, Term child1, Term child2)
+   *   mkTerm(Kind kind, const std::vector<Term>& children)
+   */
+  BITVECTOR_SLTBV,
+  /**
+   * Same semantics as regular ITE, but condition is bit-vector of size 1.
+   * Parameters: 3
+   *   -[1]: Term of bit-vector sort of size 1, representing the condition
+   *   -[2]: Term reprsenting the 'then' branch
+   *   -[3]: Term representing the 'else' branch
+   * 'then' and 'else' term must have same base sort.
+   * Create with:
+   *   mkTerm(Kind kind, Term child1, Term child2, Term child3)
+   *   mkTerm(Kind kind, const std::vector<Term>& children)
+   */
+  BITVECTOR_ITE,
+  /**
+   * Bit-vector redor.
+   * Parameters: 1
+   *   -[1]: Term of bit-vector sort
+   * Create with:
+   *   mkTerm(Kind kind, Term child)
+   */
+  BITVECTOR_REDOR,
+  /**
+   * Bit-vector redand.
+   * Parameters: 1
+   *   -[1]: Term of bit-vector sort
+   * Create with:
+   *   mkTerm(Kind kind, Term child)
+   */
+  BITVECTOR_REDAND,
+#if 0
+  /* formula to be treated as a bv atom via eager bit-blasting
+   * (internal-only symbol) */
+  BITVECTOR_EAGER_ATOM,
+  /* term to be treated as a variable. used for eager bit-blasting Ackermann
+   * expansion of bvudiv (internal-only symbol) */
+  BITVECTOR_ACKERMANIZE_UDIV,
+  /* term to be treated as a variable. used for eager bit-blasting Ackermann
+   * expansion of bvurem (internal-only symbol) */
+  BITVECTOR_ACKERMANIZE_UREM,
+  /* operator for the bit-vector boolean bit extract.
+   * One parameter, parameter is the index of the bit to extract */
+  BITVECTOR_BITOF_OP,
+#endif
+  /**
+   * Operator for bit-vector extract (from index 'high' to 'low').
+   * Parameters: 2
+   *   -[1]: The 'high' index
+   *   -[2]: The 'low' index
+   * Create with:
+   *   mkOpTerm(Kind kind, uint32_t param, uint32_t param)
+   */
+  BITVECTOR_EXTRACT_OP,
+  /**
+   * Operator for bit-vector repeat.
+   * Parameter 1:
+   *   -[1]: Number of times to repeat a given bit-vector
+   * Create with:
+   *   mkOpTerm(Kind kind, uint32_t param).
+   */
+  BITVECTOR_REPEAT_OP,
+  /**
+   * Operator for bit-vector zero-extend.
+   * Parameter 1:
+   *   -[1]: Number of bits by which a given bit-vector is to be extended
+   * Create with:
+   *   mkOpTerm(Kind kind, uint32_t param).
+   */
+  BITVECTOR_ZERO_EXTEND_OP,
+  /**
+   * Operator for bit-vector sign-extend.
+   * Parameter 1:
+   *   -[1]: Number of bits by which a given bit-vector is to be extended
+   * Create with:
+   *   mkOpTerm(Kind kind, uint32_t param).
+   */
+  BITVECTOR_SIGN_EXTEND_OP,
+  /**
+   * Operator for bit-vector rotate left.
+   * Parameter 1:
+   *   -[1]: Number of bits by which a given bit-vector is to be rotated
+   * Create with:
+   *   mkOpTerm(Kind kind, uint32_t param).
+   */
+  BITVECTOR_ROTATE_LEFT_OP,
+  /**
+   * Operator for bit-vector rotate right.
+   * Parameter 1:
+   *   -[1]: Number of bits by which a given bit-vector is to be rotated
+   * Create with:
+   *   mkOpTerm(Kind kind, uint32_t param).
+   */
+  BITVECTOR_ROTATE_RIGHT_OP,
+#if 0
+  /* bit-vector boolean bit extract.
+   * first parameter is a BITVECTOR_BITOF_OP, second is a bit-vector term */
+  BITVECTOR_BITOF,
+#endif
+  /* Bit-vector extract.
+   * Parameters: 2
+   *   -[1]: BITVECTOR_EXTRACT_OP Term
+   *   -[2]: Term of bit-vector sort
+   * Create with:
+   *   mkTerm(Term opTerm, Term child)
+   *   mkTerm(Term opTerm, const std::vector<Term>& children)
+   */
+  BITVECTOR_EXTRACT,
+  /* Bit-vector repeat.
+   * Parameters: 2
+   *   -[1]: BITVECTOR_REPEAT_OP Term
+   *   -[2]: Term of bit-vector sort
+   * Create with:
+   *   mkTerm(Term opTerm, Term child)
+   *   mkTerm(Term opTerm, const std::vector<Term>& children)
+   */
+  BITVECTOR_REPEAT,
+  /* Bit-vector zero-extend.
+   * Parameters: 2
+   *   -[1]: BITVECTOR_ZERO_EXTEND_OP Term
+   *   -[2]: Term of bit-vector sort
+   * Create with:
+   *   mkTerm(Term opTerm, Term child)
+   *   mkTerm(Term opTerm, const std::vector<Term>& children)
+   */
+  BITVECTOR_ZERO_EXTEND,
+  /* Bit-vector sign-extend.
+   * Parameters: 2
+   *   -[1]: BITVECTOR_SIGN_EXTEND_OP Term
+   *   -[2]: Term of bit-vector sort
+   * Create with:
+   *   mkTerm(Term opTerm, Term child)
+   *   mkTerm(Term opTerm, const std::vector<Term>& children)
+   */
+  BITVECTOR_SIGN_EXTEND,
+  /* Bit-vector rotate left.
+   * Parameters: 2
+   *   -[1]: BITVECTOR_ROTATE_LEFT_OP Term
+   *   -[2]: Term of bit-vector sort
+   * Create with:
+   *   mkTerm(Term opTerm, Term child)
+   *   mkTerm(Term opTerm, const std::vector<Term>& children)
+   */
+  BITVECTOR_ROTATE_LEFT,
+  /**
+   * Bit-vector rotate right.
+   * Parameters: 2
+   *   -[1]: BITVECTOR_ROTATE_RIGHT_OP Term
+   *   -[2]: Term of bit-vector sort
+   * Create with:
+   *   mkTerm(Term opTerm, Term child)
+   *   mkTerm(Term opTerm, const std::vector<Term>& children)
+   */
+  BITVECTOR_ROTATE_RIGHT,
+  /**
+   * Operator for the conversion from Integer to bit-vector.
+   * Parameter: 1
+   *   -[1]: Size of the bit-vector to convert to
+   * Create with:
+   *   mkOpTerm(Kind kind, uint32_t param).
+   */
+  INT_TO_BITVECTOR_OP,
+  /**
+   * Integer conversion to bit-vector.
+   * Parameters: 2
+   *   -[1]: INT_TO_BITVECTOR_OP Term
+   *   -[2]: Integer term
+   * Create with:
+   *   mkTerm(Kind kind, Term child1, Term child2)
+   *   mkTerm(Kind kind, const std::vector<Term>& children)
+   */
+  INT_TO_BITVECTOR,
+  /**
+   * Bit-vector conversion to (nonnegative) integer.
+   * Parameter: 1
+   *   -[1]: Term of bit-vector sort
+   * Create with:
+   *   mkTerm(Kind kind, Term child)
+   */
+  BITVECTOR_TO_NAT,
+
+  /* FP -------------------------------------------------------------------- */
+
+  /**
+   * Floating-point constant, constructed from a double or string.
+   * Parameters: 3
+   *   -[1]: Size of the exponent
+   *   -[2]: Size of the significand
+   *   -[3]: Value of the floating-point constant as a bit-vector term
+   * Create with:
+   *   mkConst(Kind kind, uint32_t arg1, uint32_t arg2, Term arg3)
+   */
+  CONST_FLOATINGPOINT,
+  /**
+   * Floating-point rounding mode term.
+   * Create with:
+   *   mkConst(RoundingMode rm)
+   */
+  CONST_ROUNDINGMODE,
+  /**
+   * Create floating-point literal from bit-vector triple.
+   * Parameters: 3
+   *   -[1]: Sign bit as a bit-vector term
+   *   -[2]: Exponent bits as a bit-vector term
+   *   -[3]: Significand bits as a bit-vector term (without hidden bit)
+   * Create with:
+   *   mkTerm(Kind kind, Term child1, Term child2, Term child3)
+   *   mkTerm(Kind kind, const std::vector<Term>& children)
+   */
+  FLOATINGPOINT_FP,
+  /**
+   * Floating-point equality.
+   * Parameters: 2
+   *   -[1]..[2]: Terms of floating point sort
+   * Create with:
+   *   mkTerm(Kind kind, Term child1, Term child2)
+   *   mkTerm(Kind kind, const std::vector<Term>& children)
+   */
+  FLOATINGPOINT_EQ,
+  /**
+   * Floating-point absolute value.
+   * Parameters: 1
+   *   -[1]: Term of floating point sort
+   * Create with:
+   *   mkTerm(Kind kind, Term child)
+   */
+  FLOATINGPOINT_ABS,
+  /**
+   * Floating-point negation.
+   * Parameters: 1
+   *   -[1]: Term of floating point sort
+   * Create with:
+   *   mkTerm(Kind kind, Term child)
+   */
+  FLOATINGPOINT_NEG,
+  /**
+   * Floating-point addition.
+   * Parameters: 3
+   *   -[1]: CONST_ROUNDINGMODE
+   *   -[2]: Term of sort FloatingPoint
+   *   -[3]: Term of sort FloatingPoint
+   * Create with:
+   *   mkTerm(Kind kind, Term child1, Term child2, child3)
+   *   mkTerm(Kind kind, const std::vector<Term>& children)
+   */
+  FLOATINGPOINT_PLUS,
+  /**
+   * Floating-point sutraction.
+   * Parameters: 3
+   *   -[1]: CONST_ROUNDINGMODE
+   *   -[2]: Term of sort FloatingPoint
+   *   -[3]: Term of sort FloatingPoint
+   * Create with:
+   *   mkTerm(Kind kind, Term child1, Term child2, Term child3)
+   *   mkTerm(Kind kind, const std::vector<Term>& children)
+   */
+  FLOATINGPOINT_SUB,
+  /**
+   * Floating-point multiply.
+   * Parameters: 3
+   *   -[1]: CONST_ROUNDINGMODE
+   *   -[2]: Term of sort FloatingPoint
+   *   -[3]: Term of sort FloatingPoint
+   * Create with:
+   *   mkTerm(Kind kind, Term child1, Term child2, Term child3)
+   *   mkTerm(Kind kind, const std::vector<Term>& children)
+   */
+  FLOATINGPOINT_MULT,
+  /**
+   * Floating-point division.
+   * Parameters: 3
+   *   -[1]: CONST_ROUNDINGMODE
+   *   -[2]: Term of sort FloatingPoint
+   *   -[3]: Term of sort FloatingPoint
+   * Create with:
+   *   mkTerm(Kind kind, Term child1, Term child2, Term child3)
+   *   mkTerm(Kind kind, const std::vector<Term>& children)
+   */
+  FLOATINGPOINT_DIV,
+  /**
+   * Floating-point fused multiply and add.
+   * Parameters: 4
+   *   -[1]: CONST_ROUNDINGMODE
+   *   -[2]: Term of sort FloatingPoint
+   *   -[3]: Term of sort FloatingPoint
+   *   -[4]: Term of sort FloatingPoint
+   * Create with:
+   *   mkTerm(Kind kind, const std::vector<Term>& children)
+   */
+  FLOATINGPOINT_FMA,
+  /**
+   * Floating-point square root.
+   * Parameters: 2
+   *   -[1]: CONST_ROUNDINGMODE
+   *   -[2]: Term of sort FloatingPoint
+   * Create with:
+   *   mkTerm(Kind kind, Term child1, Term child2)
+   *   mkTerm(Kind kind, const std::vector<Term>& children)
+   */
+  FLOATINGPOINT_SQRT,
+  /**
+   * Floating-point remainder.
+   * Parameters: 2
+   *   -[1]..[2]: Terms of floating point sort
+   * Create with:
+   *   mkTerm(Kind kind, Term child1, Term child2)
+   *   mkTerm(Kind kind, const std::vector<Term>& children)
+   */
+  FLOATINGPOINT_REM,
+  /**
+   * Floating-point round to integral.
+   * Parameters: 2
+   *   -[1]..[2]: Terms of floating point sort
+   * Create with:
+   *   mkTerm(Kind kind, Term child1, Term child2)
+   *   mkTerm(Kind kind, const std::vector<Term>& children)
+   */
+  FLOATINGPOINT_RTI,
+  /**
+   * Floating-point minimum.
+   * Parameters: 2
+   *   -[1]..[2]: Terms of floating point sort
+   * Create with:
+   *   mkTerm(Kind kind, Term child1, Term child2)
+   *   mkTerm(Kind kind, const std::vector<Term>& children)
+   */
+  FLOATINGPOINT_MIN,
+  /**
+   * Floating-point maximum.
+   * Parameters: 2
+   *   -[1]..[2]: Terms of floating point sort
+   * Create with:
+   *   mkTerm(Kind kind, Term child1, Term child2)
+   *   mkTerm(Kind kind, const std::vector<Term>& children)
+   */
+  FLOATINGPOINT_MAX,
+#if 0
+  /* floating-point minimum (defined for all inputs) */
+  FLOATINGPOINT_MIN_TOTAL,
+  /* floating-point maximum (defined for all inputs) */
+  FLOATINGPOINT_MAX_TOTAL,
+#endif
+  /**
+   * Floating-point less than or equal.
+   * Parameters: 2
+   *   -[1]..[2]: Terms of floating point sort
+   * Create with:
+   *   mkTerm(Kind kind, Term child1, Term child2)
+   *   mkTerm(Kind kind, const std::vector<Term>& children)
+   */
+  FLOATINGPOINT_LEQ,
+  /**
+   * Floating-point less than.
+   * Parameters: 2
+   *   -[1]..[2]: Terms of floating point sort
+   * Create with:
+   *   mkTerm(Kind kind, Term child1, Term child2)
+   *   mkTerm(Kind kind, const std::vector<Term>& children)
+   */
+  FLOATINGPOINT_LT,
+  /**
+   * Floating-point greater than or equal.
+   * Parameters: 2
+   *   -[1]..[2]: Terms of floating point sort
+   * Create with:
+   *   mkTerm(Kind kind, Term child1, Term child2)
+   *   mkTerm(Kind kind, const std::vector<Term>& children)
+   */
+  FLOATINGPOINT_GEQ,
+  /**
+   * Floating-point greater than.
+   * Parameters: 2
+   * Create with:
+   *   mkTerm(Kind kind, Term child1, Term child2)
+   *   mkTerm(Kind kind, const std::vector<Term>& children)
+   */
+  FLOATINGPOINT_GT,
+  /**
+   * Floating-point is normal.
+   * Parameters: 1
+   *   -[1]: Term of floating point sort
+   * Create with:
+   *   mkTerm(Kind kind, Term child)
+   */
+  FLOATINGPOINT_ISN,
+  /**
+   * Floating-point is sub-normal.
+   * Parameters: 1
+   *   -[1]: Term of floating point sort
+   * Create with:
+   *   mkTerm(Kind kind, Term child)
+   */
+  FLOATINGPOINT_ISSN,
+  /**
+   * Floating-point is zero.
+   * Parameters: 1
+   *   -[1]: Term of floating point sort
+   * Create with:
+   *   mkTerm(Kind kind, Term child)
+   */
+  FLOATINGPOINT_ISZ,
+  /**
+   * Floating-point is infinite.
+   * Parameters: 1
+   *   -[1]: Term of floating point sort
+   * Create with:
+   *   mkTerm(Kind kind, Term child)
+   */
+  FLOATINGPOINT_ISINF,
+  /**
+   * Floating-point is NaN.
+   * Parameters: 1
+   *   -[1]: Term of floating point sort
+   * Create with:
+   *   mkTerm(Kind kind, Term child)
+   */
+  FLOATINGPOINT_ISNAN,
+  /**
+   * Floating-point is negative.
+   * Parameters: 1
+   *   -[1]: Term of floating point sort
+   * Create with:
+   *   mkTerm(Kind kind, Term child)
+   */
+  FLOATINGPOINT_ISNEG,
+  /**
+   * Floating-point is positive.
+   * Parameters: 1
+   *   -[1]: Term of floating point sort
+   * Create with:
+   *   mkTerm(Kind kind, Term child)
+   */
+  FLOATINGPOINT_ISPOS,
+  /**
+   * Operator for to_fp from bit vector.
+   * Parameters: 2
+   *   -[1]: Exponent size
+   *   -[2]: Significand size
+   * Create with:
+   *   mkOpTerm(Kind kind, uint32_t param1, uint32_t param2)
+   */
+  FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP,
+  /**
+   * Conversion from an IEEE-754 bit vector to floating-point.
+   * Parameters: 2
+   *   -[1]: FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP Term
+   *   -[2]: Term of sort FloatingPoint
+   * Create with:
+   *   mkTerm(Term opTerm, Term child)
+   *   mkTerm(Term opTerm, const std::vector<Term>& children)
+   */
+  FLOATINGPOINT_TO_FP_IEEE_BITVECTOR,
+  /**
+   * Operator for to_fp from floating point.
+   * Parameters: 2
+   *   -[1]: Exponent size
+   *   -[2]: Significand size
+   * Create with:
+   *   mkOpTerm(Kind kind, uint32_t param1, uint32_t param2)
+   */
+  FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP,
+  /**
+   * Conversion between floating-point sorts.
+   * Parameters: 2
+   *   -[1]: FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP Term
+   *   -[2]: Term of sort FloatingPoint
+   * Create with:
+   *   mkTerm(Term opTerm, Term child)
+   *   mkTerm(Term opTerm, const std::vector<Term>& children)
+   */
+  FLOATINGPOINT_TO_FP_FLOATINGPOINT,
+  /**
+   * Operator for to_fp from real.
+   * Parameters: 2
+   *   -[1]: Exponent size
+   *   -[2]: Significand size
+   * Create with:
+   *   mkOpTerm(Kind kind, uint32_t param1, uint32_t param2)
+   */
+  FLOATINGPOINT_TO_FP_REAL_OP,
+  /**
+   * Conversion from a real to floating-point.
+   * Parameters: 2
+   *   -[1]: FLOATINGPOINT_TO_FP_REAL_OP Term
+   *   -[2]: Term of sort FloatingPoint
+   * Create with:
+   *   mkTerm(Term opTerm, Term child)
+   *   mkTerm(Term opTerm, const std::vector<Term>& children)
+   */
+  FLOATINGPOINT_TO_FP_REAL,
+  /*
+   * Operator for to_fp from signed bit vector.
+   * Parameters: 2
+   *   -[1]: Exponent size
+   *   -[2]: Significand size
+   * Create with:
+   *   mkOpTerm(Kind kind, uint32_t param1, uint32_t param2)
+   */
+  FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP,
+  /**
+   * Conversion from a signed bit vector to floating-point.
+   * Parameters: 2
+   *   -[1]: FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP Term
+   *   -[2]: Term of sort FloatingPoint
+   * Create with:
+   *   mkTerm(Term opTerm, Term child)
+   *   mkTerm(Term opTerm, const std::vector<Term>& children)
+   */
+  FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR,
+  /**
+   * Operator for to_fp from unsigned bit vector.
+   * Parameters: 2
+   *   -[1]: Exponent size
+   *   -[2]: Significand size
+   * Create with:
+   *   mkOpTerm(Kind kind, uint32_t param1, uint32_t param2)
+   */
+  FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP,
+  /**
+   * Operator for converting an unsigned bit vector to floating-point.
+   * Parameters: 2
+   *   -[1]: FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP Term
+   *   -[2]: Term of sort FloatingPoint
+   * Create with:
+   *   mkTerm(Term opTerm, Term child)
+   *   mkTerm(Term opTerm, const std::vector<Term>& children)
+   */
+  FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR,
+  /**
+   * Operator for a generic to_fp.
+   * Parameters: 2
+   *   -[1]: exponent size
+   *   -[2]: Significand size
+   * Create with:
+   *   mkOpTerm(Kind kind, uint32_t param1, uint32_t param2)
+   */
+  FLOATINGPOINT_TO_FP_GENERIC_OP,
+  /**
+   * Generic conversion to floating-point, used in parsing only.
+   * Parameters: 2
+   *   -[1]: FLOATINGPOINT_TO_FP_GENERIC_OP Term
+   *   -[2]: Term of sort FloatingPoint
+   * Create with:
+   *   mkTerm(Term opTerm, Term child)
+   *   mkTerm(Term opTerm, const std::vector<Term>& children)
+   */
+  FLOATINGPOINT_TO_FP_GENERIC,
+  /**
+   * Operator for to_ubv.
+   * Parameters: 1
+   *   -[1]: Size of the bit-vector to convert to
+   * Create with:
+   *   mkOpTerm(Kind kind, uint32_t param)
+   */
+  FLOATINGPOINT_TO_UBV_OP,
+  /**
+   * Conversion from a floating-point value to an unsigned bit vector.
+   * Parameters: 2
+   *   -[1]: FLOATINGPOINT_TO_FP_TO_UBV_OP Term
+   *   -[2]: Term of sort FloatingPoint
+   * Create with:
+   *   mkTerm(Term opTerm, Term child)
+   *   mkTerm(Term opTerm, const std::vector<Term>& children)
+   */
+  FLOATINGPOINT_TO_UBV,
+  /**
+   * Operator for to_ubv_total.
+   * Parameters: 1
+   *   -[1]: Size of the bit-vector to convert to
+   * Create with:
+   *   mkOpTerm(Kind kind, uint32_t param)
+   */
+  FLOATINGPOINT_TO_UBV_TOTAL_OP,
+  /**
+   * Conversion from  a floating-point value to an unsigned bit vector
+   * (defined for all inputs).
+   * Parameters: 2
+   *   -[1]: FLOATINGPOINT_TO_FP_TO_UBV_TOTAL_OP Term
+   *   -[2]: Term of sort FloatingPoint
+   * Create with:
+   *   mkTerm(Term opTerm, Term child)
+   *   mkTerm(Term opTerm, const std::vector<Term>& children)
+   */
+  FLOATINGPOINT_TO_UBV_TOTAL,
+  /**
+   * Operator for to_sbv.
+   * Parameters: 1
+   *   -[1]: Size of the bit-vector to convert to
+   * Create with:
+   *   mkOpTerm(Kind kind, uint32_t param)
+   */
+  FLOATINGPOINT_TO_SBV_OP,
+  /**
+   * Conversion from a floating-point value to a signed bit vector.
+   * Parameters: 2
+   *   -[1]: FLOATINGPOINT_TO_FP_TO_SBV_OP Term
+   *   -[2]: Term of sort FloatingPoint
+   * Create with:
+   *   mkTerm(Term opTerm, Term child)
+   *   mkTerm(Term opTerm, const std::vector<Term>& children)
+   */
+  FLOATINGPOINT_TO_SBV,
+  /**
+   * Operator for to_sbv_total.
+   * Parameters: 1
+   *   -[1]: Size of the bit-vector to convert to
+   * Create with:
+   *   mkOpTerm(Kind kind, uint32_t param)
+   */
+  FLOATINGPOINT_TO_SBV_TOTAL_OP,
+  /**
+   * Conversion from a floating-point value to a signed bit vector
+   * (defined for all inputs).
+   * Parameters: 2
+   *   -[1]: FLOATINGPOINT_TO_FP_TO_SBV_TOTAL_OP Term
+   *   -[2]: Term of sort FloatingPoint
+   * Create with:
+   *   mkTerm(Term opTerm, Term child)
+   *   mkTerm(Term opTerm, const std::vector<Term>& children)
+   */
+  FLOATINGPOINT_TO_SBV_TOTAL,
+  /**
+   * Floating-point to real.
+   * Parameters: 1
+   *   -[1]: Term of sort FloatingPoint
+   * Create with:
+   *   mkTerm(Kind kind, Term child)
+   */
+  FLOATINGPOINT_TO_REAL,
+  /**
+   * Floating-point to real (defined for all inputs).
+   * Parameters: 1
+   *   -[1]: Term of sort FloatingPoint
+   * Create with:
+   *   mkTerm(Kind kind, Term child)
+   */
+  FLOATINGPOINT_TO_REAL_TOTAL,
+
+  /* Arrays ---------------------------------------------------------------- */
+
+  /**
+   * Aarray select.
+   * Parameters: 2
+   *   -[1]: Term of array sort
+   *   -[2]: Selection index
+   * Create with:
+   *   mkTerm(Term opTerm, Term child1, Term child2)
+   *   mkTerm(Term opTerm, const std::vector<Term>& children)
+   */
+  SELECT,
+  /**
+   * Array store.
+   * Parameters: 3
+   *   -[1]: Term of array sort
+   *   -[2]: Store index
+   *   -[3]: Term to store at the index
+   * Create with:
+   *   mkTerm(Term opTerm, Term child1, Term child2, Term child3)
+   *   mkTerm(Term opTerm, const std::vector<Term>& children)
+   */
+  STORE,
+  /**
+   * Constant array.
+   * Parameters: 2
+   *   -[1]: Array sort
+   *   -[2]: Term representing a constant
+   * Create with:
+   *   mkTerm(Term opTerm, Term child1, Term child2)
+   *   mkTerm(Term opTerm, const std::vector<Term>& children)
+   *
+   * Note: We currently support the creation of constant arrays, but under some
+   * conditions when there is a chain of equalities connecting two constant
+   * arrays, the solver doesn't know what to do and aborts (Issue #1667).
+   */
+  STORE_ALL,
+#if 0
+  /* array table function (internal-only symbol) */
+  ARR_TABLE_FUN,
+  /* array lambda (internal-only symbol) */
+  ARRAY_LAMBDA,
+  /* partial array select, for internal use only */
+  PARTIAL_SELECT_0,
+  /* partial array select, for internal use only */
+  PARTIAL_SELECT_1,
+#endif
+
+  /* Datatypes ------------------------------------------------------------- */
+
+  /**
+   * Constructor application.
+   * Paramters: n > 0
+   *   -[1]: Constructor
+   *   -[2]..[n]: Parameters to the constructor
+   * Create with:
+   *   mkTerm(Kind kind)
+   *   mkTerm(Kind kind, Term child)
+   *   mkTerm(Kind kind, Term child1, Term child2)
+   *   mkTerm(Kind kind, Term child1, Term child2, Term child3)
+   *   mkTerm(Kind kind, const std::vector<Term>& children)
+   */
+  APPLY_SELECTOR,
+  /**
+   * Datatype selector application.
+   * Parameters: 1
+   *   -[1]: Datatype term (undefined if mis-applied)
+   * Create with:
+   *   mkTerm(Kind kind, Term child)
+   */
+  APPLY_CONSTRUCTOR,
+  /**
+   * Datatype selector application.
+   * Parameters: 1
+   *   -[1]: Datatype term (defined rigidly if mis-applied)
+   * Create with:
+   *   mkTerm(Kind kind, Term child)
+   */
+  APPLY_SELECTOR_TOTAL,
+  /**
+   * Datatype tester application.
+   * Parameters: 2
+   *   -[1]: Tester term
+   *   -[2]: Datatype term
+   * Create with:
+   *   mkTerm(Kind kind, Term child1, Term child2)
+   *   mkTerm(Kind kind, const std::vector<Term>& children)
+   */
+  APPLY_TESTER,
+#if 0
+  /* Parametric datatype term.  */
+  PARAMETRIC_DATATYPE,
+  /* type ascription, for datatype constructor applications;
+   * first parameter is an ASCRIPTION_TYPE, second is the datatype constructor
+   * application being ascribed */
+  APPLY_TYPE_ASCRIPTION,
+#endif
+  /**
+   * Operator for a tuple update.
+   * Parameters: 1
+   *   -[1]: Index of the tuple to be updated
+   * Create with:
+   *   mkOpTerm(Kind kind, uint32_t param)
+   */
+  TUPLE_UPDATE_OP,
+  /**
+   * Tuple update.
+   * Parameters: 3
+   *   -[1]: TUPLE_UPDATE_OP (which references an index)
+   *   -[2]: Tuple
+   *   -[3]: Element to store in the tuple at the given index
+   * Create with:
+   *   mkTerm(Kind kind, Term child1, Term child2, Term child3)
+   *   mkTerm(Kind kind, const std::vector<Term>& children)
+   */
+  TUPLE_UPDATE,
+  /**
+   * Operator for a record update.
+   * Parameters: 1
+   *   -[1]: Name of the field to be updated
+   * Create with:
+   *   mkOpTerm(Kind kind, const std::string& param)
+   */
+  RECORD_UPDATE_OP,
+  /**
+   * Record update.
+   * Parameters: 3
+   *   -[1]: RECORD_UPDATE_OP Term (which references a field)
+   *   -[2]: Record term to update
+   *   -[3]: Element to store in the record in the given field
+   * Create with:
+   *   mkTerm(Kind kind, Term child1, Term child2)
+   *   mkTerm(Kind kind, const std::vector<Term>& children)
+   */
+  RECORD_UPDATE,
+#if 0
+  /* datatypes size */
+  DT_SIZE,
+  /* datatypes height bound */
+  DT_HEIGHT_BOUND,
+  /* datatypes height bound */
+  DT_SIZE_BOUND,
+  /* datatypes sygus bound */
+  DT_SYGUS_BOUND,
+  /* datatypes sygus term order */
+  DT_SYGUS_TERM_ORDER,
+  /* datatypes sygus is constant */
+  DT_SYGUS_IS_CONST,
+#endif
+
+  /* Separation Logic ------------------------------------------------------ */
+
+  /**
+   * Separation logic nil term.
+   * Parameters: 0
+   * Create with:
+   *   mkSepNil(Sort sort)
+   *   mkTerm(Kind kind, Sort sort)
+   */
+  SEP_NIL,
+  /**
+   * Separation logic empty heap.
+   * Parameters: 2
+   *   -[1]: Term of the same sort as the sort of the location of the heap
+   *         that is constrained to be empty
+   *   -[2]: Term of the same sort as the data sort of the heap that is
+   *         that is constrained to be empty
+   * Create with:
+   *   mkTerm(Kind kind, Term child1, Term child2)
+   *   mkTerm(Kind kind, const std::vector<Term>& children)
+   */
+  SEP_EMP,
+  /**
+   * Separation logic points-to relation.
+   * Parameters: 2
+   *   -[1]: Location of the points-to constraint
+   *   -[2]: Data of the points-to constraint
+   * Create with:
+   *   mkTerm(Kind kind, Term child1, Term child2)
+   *   mkTerm(Kind kind, const std::vector<Term>& children)
+   */
+  SEP_PTO,
+  /**
+   * Separation logic star.
+   * Parameters: n >= 2
+   *   -[1]..[n]: Child constraints that hold in disjoint (separated) heaps
+   * Create with:
+   *   mkTerm(Kind kind, Term child1, Term child2)
+   *   mkTerm(Kind kind, Term child1, Term child2, Term child3)
+   *   mkTerm(Kind kind, const std::vector<Term>& children)
+   */
+  SEP_STAR,
+  /**
+   * Separation logic magic wand.
+   * Parameters: 2
+   *   -[1]: Antecendant of the magic wand constraint
+   *   -[2]: Conclusion of the magic wand constraint, which is asserted to
+   *         hold in all heaps that are disjoint extensions of the antecedent.
+   * Create with:
+   *   mkTerm(Kind kind, Term child1, Term child2)
+   *   mkTerm(Kind kind, const std::vector<Term>& children)
+   */
+  SEP_WAND,
+#if 0
+  /* separation label (internal use only) */
+  SEP_LABEL,
+#endif
+
+  /* Sets ------------------------------------------------------------------ */
+
+  /**
+   * Empty set constant.
+   * Parameters: 1
+   *   -[1]: Sort of the set elements
+   * Create with:
+   *   mkEmptySet(Sort sort)
+   *   mkConst(Sort sort)
+   */
+  EMPTYSET,
+  /**
+   * Set union.
+   * Parameters: 2
+   *   -[1]..[2]: Terms of set sort
+   * Create with:
+   *   mkTerm(Kind kind, Term child1, Term child2)
+   *   mkTerm(Kind kind, const std::vector<Term>& children)
+   */
+  UNION,
+  /**
+   * Set intersection.
+   * Parameters: 2
+   *   -[1]..[2]: Terms of set sort
+   * Create with:
+   *   mkTerm(Kind kind, Term child1, Term child2)
+   *   mkTerm(Kind kind, const std::vector<Term>& children)
+   */
+  INTERSECTION,
+  /**
+   * Set subtraction.
+   * Parameters: 2
+   *   -[1]..[2]: Terms of set sort
+   * Create with:
+   *   mkTerm(Kind kind, Term child1, Term child2)
+   *   mkTerm(Kind kind, const std::vector<Term>& children)
+   */
+  SETMINUS,
+  /**
+   * Subset predicate.
+   * Parameters: 2
+   *   -[1]..[2]: Terms of set sort, [1] a subset of set [2]?
+   * Create with:
+   *   mkTerm(Kind kind, Term child1, Term child2)
+   *   mkTerm(Kind kind, const std::vector<Term>& children)
+   */
+  SUBSET,
+  /**
+   * Set membership predicate.
+   * Parameters: 2
+   *   -[1]..[2]: Terms of set sort, [1] a member of set [2]?
+   * Create with:
+   *   mkTerm(Kind kind, Term child1, Term child2)
+   *   mkTerm(Kind kind, const std::vector<Term>& children)
+   */
+  MEMBER,
+  /**
+   * The set of the single element given as a parameter.
+   * Parameters: 1
+   *   -[1]: Single element
+   * Create with:
+   *   mkTerm(Kind kind, Term child)
+   */
+  SINGLETON,
+  /**
+   * The set obtained by inserting elements;
+   * Parameters: n > 0
+   *   -[1]..[n-1]: Elements inserted into set [n]
+   *   -[n]: Set Term
+   * Create with:
+   *   mkTerm(Kind kind, Term child)
+   *   mkTerm(Kind kind, Term child1, Term child2)
+   *   mkTerm(Kind kind, Term child1, Term child2, Term child3)
+   *   mkTerm(Kind kind, const std::vector<Term>& children)
+   */
+  INSERT,
+  /**
+   * Set cardinality.
+   * Parameters: 1
+   *   -[1]: Set to determine the cardinality of
+   * Create with:
+   *   mkTerm(Kind kind, Term child)
+   */
+  CARD,
+  /**
+   * Set complement with respect to finite universe.
+   * Parameters: 1
+   *   -[1]: Set to complement
+   * Create with:
+   *   mkTerm(Kind kind, Term child)
+   */
+  COMPLEMENT,
+  /**
+   * Finite universe set.
+   * All set variables must be interpreted as subsets of it.
+   * Create with:
+   *   mkUniverseSet(Sort sort)
+   *   mkTerm(Kind kind, Sort sort)
+   */
+  UNIVERSE_SET,
+  /**
+   * Set join.
+   * Parameters: 2
+   *   -[1]..[2]: Terms of set sort
+   * Create with:
+   *   mkTerm(Kind kind, Term child1, Term child2)
+   *   mkTerm(Kind kind, const std::vector<Term>& children)
+   */
+  JOIN,
+  /**
+   * Set cartesian product.
+   * Parameters: 2
+   *   -[1]..[2]: Terms of set sort
+   * Create with:
+   *   mkTerm(Kind kind, Term child1, Term child2)
+   *   mkTerm(Kind kind, const std::vector<Term>& children)
+   */
+  PRODUCT,
+  /**
+   * Set transpose.
+   * Parameters: 1
+   *   -[1]: Term of set sort
+   * Create with:
+   *   mkTerm(Kind kind, Term child)
+   */
+  TRANSPOSE,
+  /**
+   * Set transitive closure.
+   * Parameters: 1
+   *   -[1]: Term of set sort
+   * Create with:
+   *   mkTerm(Kind kind, Term child)
+   */
+  TCLOSURE,
+  /**
+   * Set join image.
+   * Parameters: 2
+   *   -[1]..[2]: Terms of set sort
+   * Create with:
+   *   mkTerm(Kind kind, Term child1, Term child2)
+   *   mkTerm(Kind kind, const std::vector<Term>& children)
+   */
+  JOIN_IMAGE,
+  /**
+   * Set identity.
+   * Parameters: 1
+   *   -[1]: Term of set sort
+   * Create with:
+   *   mkTerm(Kind kind, Term child)
+   */
+  IDEN,
+
+  /* Strings --------------------------------------------------------------- */
+
+  /**
+   * String concat.
+   * Parameters: n > 1
+   *   -[1]..[n]: Terms of String sort
+   * Create with:
+   *   mkTerm(Kind kind, Term child1, Term child2)
+   *   mkTerm(Kind kind, Term child1, Term child2, Term child3)
+   *   mkTerm(Kind kind, const std::vector<Term>& children)
+   */
+  STRING_CONCAT,
+  /**
+   * String membership.
+   * Parameters: 2
+   *   -[1]..[2]: Terms of String sort
+   * Create with:
+   *   mkTerm(Kind kind, Term child1, Term child2)
+   *   mkTerm(Kind kind, const std::vector<Term>& children)
+   */
+  STRING_IN_REGEXP,
+  /**
+   * String length.
+   * Parameters: 1
+   *   -[1]: Term of String sort
+   * Create with:
+   *   mkTerm(Kind kind, Term child)
+   */
+  STRING_LENGTH,
+  /**
+   * String substring.
+   * Extracts a substring, starting at index i and of length l, from a string
+   * s.  If the start index is negative, the start index is greater than the
+   * length of the string, or the length is negative, the result is the empty
+   * string.
+   * Parameters: 3
+   *   -[1]: Term of sort String
+   *   -[2]: Term of sort Integer (index i)
+   *   -[3]: Term of sort Integer (length l)
+   * Create with:
+   *   mkTerm(Kind kind, Term child1, Term child2, Term child3)
+   *   mkTerm(Kind kind, const std::vector<Term>& children)
+   */
+  STRING_SUBSTR,
+  /**
+   * String character at.
+   * Returns the character at index i from a string s. If the index is negative
+   * or the index is greater than the length of the string, the result is the
+   * empty string. Otherwise the result is a string of length 1.
+   * Parameters: 2
+   *   -[1]: Term of sort String (string s)
+   *   -[2]: Term of sort Integer (index i)
+   * Create with:
+   *   mkTerm(Kind kind, Term child1, Term child2)
+   *   mkTerm(Kind kind, const std::vector<Term>& children)
+   */
+  STRING_CHARAT,
+  /**
+   * String contains.
+   * Checks whether a string s1 contains another string s2. If s2 is empty, the
+   * result is always true.
+   * Parameters: 2
+   *   -[1]: Term of sort String (the string s1)
+   *   -[2]: Term of sort String (the string s2)
+   * Create with:
+   *   mkTerm(Kind kind, Term child1, Term child2)
+   *   mkTerm(Kind kind, const std::vector<Term>& children)
+   */
+  STRING_STRCTN,
+  /**
+   * String index-of.
+   * Returns the index of a substring s2 in a string s1 starting at index i. If
+   * the index is negative or greater than the length of string s1 or the
+   * substring s2 does not appear in string s1 after index i, the result is -1.
+   * Parameters: 3
+   *   -[1]: Term of sort String (substring s1)
+   *   -[2]: Term of sort String (substring s2)
+   *   -[3]: Term of sort Integer (index i)
+   * Create with:
+   *   mkTerm(Kind kind, Term child1, Term child2, Term child3)
+   *   mkTerm(Kind kind, const std::vector<Term>& children)
+   */
+  STRING_STRIDOF,
+  /**
+   * String replace.
+   * Replaces a string s2 in a string s1 with string s3. If s2 does not appear
+   * in s1, s1 is returned unmodified.
+   * Parameters: 3
+   *   -[1]: Term of sort String (string s1)
+   *   -[2]: Term of sort String (string s2)
+   *   -[3]: Term of sort String (string s3)
+   * Create with:
+   *   mkTerm(Kind kind, Term child1, Term child2, Term child3)
+   *   mkTerm(Kind kind, const std::vector<Term>& children)
+   */
+  STRING_STRREPL,
+  /**
+   * String prefix-of.
+   * Checks whether a string s1 is a prefix of string s2. If string s1 is
+   * empty, this operator returns true.
+   * Parameters: 2
+   *   -[1]: Term of sort String (string s1)
+   *   -[2]: Term of sort String (string s2)
+   * Create with:
+   *   mkTerm(Kind kind, Term child1, Term child2)
+   *   mkTerm(Kind kind, const std::vector<Term>& children)
+   */
+  STRING_PREFIX,
+  /**
+   * String suffix-of.
+   * Checks whether a string s1 is a suffix of string 2. If string s1 is empty,
+   * this operator returns true.
+   * Parameters: 2
+   *   -[1]: Term of sort String (string s1)
+   *   -[2]: Term of sort String (string s2)
+   * Create with:
+   *   mkTerm(Kind kind, Term child1, Term child2)
+   *   mkTerm(Kind kind, const std::vector<Term>& children)
+   */
+  STRING_SUFFIX,
+  /**
+   * Integer to string.
+   * If the integer is negative this operator returns the empty string.
+   * Parameters: 1
+   *   -[1]: Term of sort Integer
+   * Create with:
+   *   mkTerm(Kind kind, Term child)
+   */
+  STRING_ITOS,
+  /**
+   * String to integer (total function).
+   * If the string does not contain an integer or the integer is negative, the
+   * operator returns -1.
+   * Parameters: 1
+   *   -[1]: Term of sort String
+   * Create with:
+   *   mkTerm(Kind kind, Term child)
+   */
+  STRING_STOI,
+  /**
+   * Constant string.
+   * Parameters:
+   *   See mkString()
+   * Create with:
+   *   mkString(const char* s)
+   *   mkString(const std::string& s)
+   *   mkString(const unsigned char c)
+   *   mkString(const std::vector<unsigned>& s)
+   *   mkConst(Kind kind, const char* s)
+   *   mkConst(Kind kind, const std::string& s)
+   */
+  CONST_STRING,
+  /**
+   * Conversion from string to regexp.
+   * Parameters: 1
+   *   -[1]: Term of sort String
+   * Create with:
+   *   mkTerm(Kind kind, Term child)
+   */
+  STRING_TO_REGEXP,
+  /**
+   * Regexp Concatenation .
+   * Parameters: 2
+   *   -[1]..[2]: Terms of Regexp sort
+   * Create with:
+   *   mkTerm(Kind kind, Term child1, Term child2)
+   *   mkTerm(Kind kind, const std::vector<Term>& children)
+   */
+  REGEXP_CONCAT,
+  /**
+   * Regexp union.
+   * Parameters: 2
+   *   -[1]..[2]: Terms of Regexp sort
+   * Create with:
+   *   mkTerm(Kind kind, Term child1, Term child2)
+   *   mkTerm(Kind kind, const std::vector<Term>& children)
+   */
+  REGEXP_UNION,
+  /**
+   * Regexp intersection.
+   * Parameters: 2
+   *   -[1]..[2]: Terms of Regexp sort
+   * Create with:
+   *   mkTerm(Kind kind, Term child1, Term child2)
+   *   mkTerm(Kind kind, const std::vector<Term>& children)
+   */
+  REGEXP_INTER,
+  /**
+   * Regexp *.
+   * Parameters: 1
+   *   -[1]: Term of sort Regexp
+   * Create with:
+   *   mkTerm(Kind kind, Term child)
+   */
+  REGEXP_STAR,
+  /**
+   * Regexp +.
+   * Parameters: 1
+   *   -[1]: Term of sort Regexp
+   * Create with:
+   *   mkTerm(Kind kind, Term child)
+   */
+  REGEXP_PLUS,
+  /**
+   * Regexp ?.
+   * Parameters: 1
+   *   -[1]: Term of sort Regexp
+   * Create with:
+   *   mkTerm(Kind kind, Term child)
+   */
+  REGEXP_OPT,
+  /**
+   * Regexp range.
+   * Parameters: 2
+   *   -[1]: Lower bound character for the range
+   *   -[2]: Upper bound character for the range
+   * Create with:
+   *   mkTerm(Kind kind, Term child1, Term child2)
+   *   mkTerm(Kind kind, const std::vector<Term>& children)
+   */
+  REGEXP_RANGE,
+  /**
+   * Regexp loop.
+   * Parameters: 2 (3)
+   *   -[1]: Term of sort RegExp
+   *   -[2]: Lower bound for the number of repetitions of the first argument
+   *   -[3]: Upper bound for the number of repetitions of the first argument
+   * Create with:
+   *   mkTerm(Kind kind, Term child1, Term child2)
+   *   mkTerm(Kind kind, Term child1, Term child2, Term child3)
+   *   mkTerm(Kind kind, const std::vector<Term>& children)
+   */
+  REGEXP_LOOP,
+  /**
+   * Regexp empty.
+   * Parameters: 0
+   * Create with:
+   *   mkRegexpEmpty()
+   *   mkTerm(Kind kind)
+   */
+  REGEXP_EMPTY,
+  /**
+   * Regexp all characters.
+   * Parameters: 0
+   * Create with:
+   *   mkRegexpSigma()
+   *   mkTerm(Kind kind)
+   */
+  REGEXP_SIGMA,
+#if 0
+  /* regexp rv (internal use only) */
+  REGEXP_RV,
+#endif
+
+  /* Quantifiers ----------------------------------------------------------- */
+
+  /**
+   * Universally quantified formula.
+   * Parameters: 2 (3)
+   *   -[1]: BOUND_VAR_LIST Term
+   *   -[2]: Quantifier body
+   *   -[3]: (optional) INST_PATTERN_LIST Term
+   * Create with:
+   *   mkTerm(Kind kind, Term child1, Term child2)
+   *   mkTerm(Kind kind, Term child1, Term child2, Term child3)
+   *   mkTerm(Kind kind, const std::vector<Term>& children)
+   */
+  FORALL,
+  /**
+   * Existentially quantified formula.
+   * Parameters: 2 (3)
+   *   -[1]: BOUND_VAR_LIST Term
+   *   -[2]: Quantifier body
+   *   -[3]: (optional) INST_PATTERN_LIST Term
+   * Create with:
+   *   mkTerm(Kind kind, Term child1, Term child2)
+   *   mkTerm(Kind kind, Term child1, Term child2, Term child3)
+   *   mkTerm(Kind kind, const std::vector<Term>& children)
+   */
+  EXISTS,
+#if 0
+  /* instantiation constant */
+  INST_CONSTANT,
+  /* instantiation pattern */
+  INST_PATTERN,
+  /* a list of bound variables (used to bind variables under a quantifier) */
+  BOUND_VAR_LIST,
+  /* instantiation no-pattern */
+  INST_NO_PATTERN,
+  /* instantiation attribute */
+  INST_ATTRIBUTE,
+  /* a list of instantiation patterns */
+  INST_PATTERN_LIST,
+  /* predicate for specifying term in instantiation closure. */
+  INST_CLOSURE,
+  /* general rewrite rule (for rewrite-rules theory) */
+  REWRITE_RULE,
+  /* actual rewrite rule (for rewrite-rules theory) */
+  RR_REWRITE,
+  /* actual reduction rule (for rewrite-rules theory) */
+  RR_REDUCTION,
+  /* actual deduction rule (for rewrite-rules theory) */
+  RR_DEDUCTION,
+
+  /* Sort Kinds ------------------------------------------------------------ */
+
+  /* array type */
+   ARRAY_TYPE,
+  /* a type parameter for type ascription */
+  ASCRIPTION_TYPE,
+  /* constructor */
+  CONSTRUCTOR_TYPE,
+  /* a datatype type index */
+  DATATYPE_TYPE,
+  /* selector */
+  SELECTOR_TYPE,
+  /* set type, takes as parameter the type of the elements */
+  SET_TYPE,
+  /* sort tag */
+  SORT_TAG,
+  /* specifies types of user-declared 'uninterpreted' sorts */
+  SORT_TYPE,
+  /* tester */
+  TESTER_TYPE,
+  /* a representation for basic types */
+  TYPE_CONSTANT,
+  /* a function type */
+  FUNCTION_TYPE,
+  /* the type of a symbolic expression */
+  SEXPR_TYPE,
+  /* bit-vector type */
+  BITVECTOR_TYPE,
+  /* floating-point type */
+  FLOATINGPOINT_TYPE,
+#endif
+
+  /* ----------------------------------------------------------------------- */
+  /* marks the upper-bound of this enumeration */
+  LAST_KIND
+};
+
+/**
+ * Serialize a kind to given stream.
+ * @param out the output stream
+ * @param k the kind to be serialized to the given output stream
+ * @return the output stream
+ */
+std::ostream& operator<<(std::ostream& out, Kind k) CVC4_PUBLIC;
+
+/**
+ * Hash function for Kinds.
+ */
+struct CVC4_PUBLIC KindHashFunction
+{
+  size_t operator()(Kind k) const;
+};
+
+}  // namespace api
+}  // namespace CVC4
+
+#endif