cvc4-1.4
CVC4::kind Namespace Reference

Data Structures

struct  KindHashFunction
 

Enumerations

enum  Kind_t {
  UNDEFINED_KIND, NULL_EXPR, SORT_TAG, SORT_TYPE,
  UNINTERPRETED_CONSTANT, ABSTRACT_VALUE, BUILTIN, FUNCTION,
  APPLY, EQUAL, DISTINCT, VARIABLE,
  BOUND_VARIABLE, SKOLEM, SEXPR, LAMBDA,
  CHAIN, CHAIN_OP, TYPE_CONSTANT, FUNCTION_TYPE,
  SEXPR_TYPE, SUBTYPE_TYPE, CONST_BOOLEAN, NOT,
  AND, IFF, IMPLIES, OR,
  XOR, ITE, APPLY_UF, CARDINALITY_CONSTRAINT,
  COMBINED_CARDINALITY_CONSTRAINT, PLUS, MULT, MINUS,
  UMINUS, DIVISION, DIVISION_TOTAL, INTS_DIVISION,
  INTS_DIVISION_TOTAL, INTS_MODULUS, INTS_MODULUS_TOTAL, ABS,
  DIVISIBLE, POW, DIVISIBLE_OP, SUBRANGE_TYPE,
  CONST_RATIONAL, LT, LEQ, GT,
  GEQ, IS_INTEGER, TO_INTEGER, TO_REAL,
  BITVECTOR_TYPE, CONST_BITVECTOR, BITVECTOR_CONCAT, BITVECTOR_AND,
  BITVECTOR_OR, BITVECTOR_XOR, BITVECTOR_NOT, BITVECTOR_NAND,
  BITVECTOR_NOR, BITVECTOR_XNOR, BITVECTOR_COMP, BITVECTOR_MULT,
  BITVECTOR_PLUS, BITVECTOR_SUB, BITVECTOR_NEG, BITVECTOR_UDIV,
  BITVECTOR_UREM, BITVECTOR_SDIV, BITVECTOR_SREM, BITVECTOR_SMOD,
  BITVECTOR_UDIV_TOTAL, BITVECTOR_UREM_TOTAL, BITVECTOR_SHL, BITVECTOR_LSHR,
  BITVECTOR_ASHR, BITVECTOR_ULT, BITVECTOR_ULE, BITVECTOR_UGT,
  BITVECTOR_UGE, BITVECTOR_SLT, BITVECTOR_SLE, BITVECTOR_SGT,
  BITVECTOR_SGE, BITVECTOR_EAGER_ATOM, BITVECTOR_ACKERMANIZE_UDIV, BITVECTOR_ACKERMANIZE_UREM,
  BITVECTOR_BITOF_OP, BITVECTOR_EXTRACT_OP, BITVECTOR_REPEAT_OP, BITVECTOR_ZERO_EXTEND_OP,
  BITVECTOR_SIGN_EXTEND_OP, BITVECTOR_ROTATE_LEFT_OP, BITVECTOR_ROTATE_RIGHT_OP, BITVECTOR_BITOF,
  BITVECTOR_EXTRACT, BITVECTOR_REPEAT, BITVECTOR_ZERO_EXTEND, BITVECTOR_SIGN_EXTEND,
  BITVECTOR_ROTATE_LEFT, BITVECTOR_ROTATE_RIGHT, INT_TO_BITVECTOR_OP, INT_TO_BITVECTOR,
  BITVECTOR_TO_NAT, ARRAY_TYPE, SELECT, STORE,
  STORE_ALL, ARR_TABLE_FUN, ARRAY_LAMBDA, CONSTRUCTOR_TYPE,
  SELECTOR_TYPE, TESTER_TYPE, APPLY_CONSTRUCTOR, APPLY_SELECTOR,
  APPLY_SELECTOR_TOTAL, APPLY_TESTER, DATATYPE_TYPE, PARAMETRIC_DATATYPE,
  APPLY_TYPE_ASCRIPTION, ASCRIPTION_TYPE, TUPLE_TYPE, TUPLE,
  TUPLE_SELECT_OP, TUPLE_SELECT, TUPLE_UPDATE_OP, TUPLE_UPDATE,
  RECORD_TYPE, RECORD, RECORD_SELECT_OP, RECORD_SELECT,
  RECORD_UPDATE_OP, RECORD_UPDATE, EMPTYSET, SET_TYPE,
  UNION, INTERSECTION, SETMINUS, SUBSET,
  MEMBER, SINGLETON, INSERT, STRING_CONCAT,
  STRING_IN_REGEXP, STRING_LENGTH, STRING_SUBSTR, STRING_SUBSTR_TOTAL,
  STRING_CHARAT, STRING_STRCTN, STRING_STRIDOF, STRING_STRREPL,
  STRING_PREFIX, STRING_SUFFIX, STRING_ITOS, STRING_STOI,
  STRING_U16TOS, STRING_STOU16, STRING_U32TOS, STRING_STOU32,
  CONST_STRING, CONST_REGEXP, STRING_TO_REGEXP, REGEXP_CONCAT,
  REGEXP_UNION, REGEXP_INTER, REGEXP_STAR, REGEXP_PLUS,
  REGEXP_OPT, REGEXP_RANGE, REGEXP_LOOP, REGEXP_EMPTY,
  REGEXP_SIGMA, FORALL, EXISTS, INST_CONSTANT,
  BOUND_VAR_LIST, INST_PATTERN, INST_PATTERN_LIST, REWRITE_RULE,
  RR_REWRITE, RR_REDUCTION, RR_DEDUCTION, LAST_KIND
}
 

Functions

std::ostream & operator<< (std::ostream &, CVC4::Kind)
 
bool isAssociative (::CVC4::Kind k)
 Returns true if the given kind is associative. More...
 
std::string kindToString (::CVC4::Kind k)
 

Enumeration Type Documentation

Enumerator
UNDEFINED_KIND 

undefined

NULL_EXPR 

Null kind.

SORT_TAG 

sort tag (1)

SORT_TYPE 

specifies types of user-declared 'uninterpreted' sorts (2)

UNINTERPRETED_CONSTANT 

the kind of expressions representing uninterpreted constants; payload is an instance of the CVC4::UninterpretedConstant class (used in models) (3)

ABSTRACT_VALUE 

the kind of expressions representing abstract values (other than uninterpreted sort constants); payload is an instance of the CVC4::AbstractValue class (used in models) (4)

BUILTIN 

the kind of expressions representing built-in operators (5)

FUNCTION 

a defined function (6)

APPLY 

application of a defined function (7)

EQUAL 

equality (two parameters only, sorts must match) (8)

DISTINCT 

disequality (N-ary, sorts must match) (9)

VARIABLE 

a variable (not permitted in bindings) (10)

BOUND_VARIABLE 

a bound variable (permitted in bindings and the associated lambda and quantifier bodies only) (11)

SKOLEM 

a Skolem variable (internal only) (12)

SEXPR 

a symbolic expression (any arity) (13)

LAMBDA 

a lambda expression; first parameter is a BOUND_VAR_LIST, second is lambda body (14)

CHAIN 

chained operator (N-ary), turned into a conjuction of binary applications of the operator on adjoining parameters; first parameter is a CHAIN_OP representing a binary operator, rest are arguments to that operator (15)

CHAIN_OP 

the chained operator; payload is an instance of the CVC4::Chain class (16)

TYPE_CONSTANT 

a representation for basic types (17)

FUNCTION_TYPE 

a function type (18)

SEXPR_TYPE 

the type of a symbolic expression (19)

SUBTYPE_TYPE 

predicate subtype; payload is an instance of the CVC4::Predicate class (20)

CONST_BOOLEAN 

truth and falsity; payload is a (C++) bool (21)

NOT 

logical not (22)

AND 

logical and (N-ary) (23)

IFF 

logical equivalence (exactly two parameters) (24)

IMPLIES 

logical implication (exactly two parameters) (25)

OR 

logical or (N-ary) (26)

XOR 

exclusive or (exactly two parameters) (27)

ITE 

if-then-else, used for both Boolean and term ITE constructs; first parameter is (Boolean-sorted) condition, second is 'then', third is 'else' and these two parameters must have same base sort (28)

APPLY_UF 

application of an uninterpreted function; first parameter is the function, remaining ones are parameters to that function (29)

CARDINALITY_CONSTRAINT 

cardinality constraint on sort S: first parameter is (any) term of sort S, second is a positive integer constant k that bounds the cardinality of S (30)

COMBINED_CARDINALITY_CONSTRAINT 

combined cardinality constraint; parameter is a positive integer constant k that bounds the sum of the cardinalities of all sorts in the signature (31)

PLUS 

arithmetic addition (N-ary) (32)

MULT 

arithmetic multiplication (N-ary) (33)

MINUS 

arithmetic binary subtraction operator (34)

UMINUS 

arithmetic unary negation (35)

DIVISION 

real division, division by 0 undefined (user symbol) (36)

DIVISION_TOTAL 

real division with interpreted division by 0 (internal symbol) (37)

INTS_DIVISION 

integer division, division by 0 undefined (user symbol) (38)

INTS_DIVISION_TOTAL 

integer division with interpreted division by 0 (internal symbol) (39)

INTS_MODULUS 

integer modulus, division by 0 undefined (user symbol) (40)

INTS_MODULUS_TOTAL 

integer modulus with interpreted division by 0 (internal symbol) (41)

ABS 

absolute value (42)

DIVISIBLE 

divisibility-by-k predicate; first parameter is a DIVISIBLE_OP, second is integer term (43)

POW 

arithmetic power (44)

DIVISIBLE_OP 

operator for the divisibility-by-k predicate; payload is an instance of the CVC4::Divisible class (45)

SUBRANGE_TYPE 

the type of an integer subrange (46)

CONST_RATIONAL 

a multiple-precision rational constant; payload is an instance of the CVC4::Rational class (47)

LT 

less than, x < y (48)

LEQ 

less than or equal, x <= y (49)

GT 

greater than, x > y (50)

GEQ 

greater than or equal, x >= y (51)

IS_INTEGER 

term-is-integer predicate (parameter is a real-sorted term) (52)

TO_INTEGER 

convert term to integer by the floor function (parameter is a real-sorted term) (53)

TO_REAL 

cast term to real (parameter is an integer-sorted term; this is a no-op in CVC4, as integer is a subtype of real) (54)

BITVECTOR_TYPE 

bit-vector type (55)

CONST_BITVECTOR 

a fixed-width bit-vector constant; payload is an instance of the CVC4::BitVector class (56)

BITVECTOR_CONCAT 

concatenation of two or more bit-vectors (57)

BITVECTOR_AND 

bitwise and of two or more bit-vectors (58)

BITVECTOR_OR 

bitwise or of two or more bit-vectors (59)

BITVECTOR_XOR 

bitwise xor of two or more bit-vectors (60)

BITVECTOR_NOT 

bitwise not of a bit-vector (61)

BITVECTOR_NAND 

bitwise nand of two bit-vectors (62)

BITVECTOR_NOR 

bitwise nor of two bit-vectors (63)

BITVECTOR_XNOR 

bitwise xnor of two bit-vectors (64)

BITVECTOR_COMP 

equality comparison of two bit-vectors (returns one bit) (65)

BITVECTOR_MULT 

multiplication of two or more bit-vectors (66)

BITVECTOR_PLUS 

addition of two or more bit-vectors (67)

BITVECTOR_SUB 

subtraction of two bit-vectors (68)

BITVECTOR_NEG 

unary negation of a bit-vector (69)

BITVECTOR_UDIV 

unsigned division of two bit-vectors, truncating towards 0 (undefined if divisor is 0) (70)

BITVECTOR_UREM 

unsigned remainder from truncating division of two bit-vectors (undefined if divisor is 0) (71)

BITVECTOR_SDIV 

2's complement signed division (72)

BITVECTOR_SREM 

2's complement signed remainder (sign follows dividend) (73)

BITVECTOR_SMOD 

2's complement signed remainder (sign follows divisor) (74)

BITVECTOR_UDIV_TOTAL 

unsigned division of two bit-vectors, truncating towards 0 (defined to be the all-ones bit pattern, if divisor is 0) (75)

BITVECTOR_UREM_TOTAL 

unsigned remainder from truncating division of two bit-vectors (defined to be equal to the dividend, if divisor is 0) (76)

BITVECTOR_SHL 

bit-vector shift left (the two bit-vector parameters must have same width) (77)

BITVECTOR_LSHR 

bit-vector logical shift right (the two bit-vector parameters must have same width) (78)

BITVECTOR_ASHR 

bit-vector arithmetic shift right (the two bit-vector parameters must have same width) (79)

BITVECTOR_ULT 

bit-vector unsigned less than (the two bit-vector parameters must have same width) (80)

BITVECTOR_ULE 

bit-vector unsigned less than or equal (the two bit-vector parameters must have same width) (81)

BITVECTOR_UGT 

bit-vector unsigned greater than (the two bit-vector parameters must have same width) (82)

BITVECTOR_UGE 

bit-vector unsigned greater than or equal (the two bit-vector parameters must have same width) (83)

BITVECTOR_SLT 

bit-vector signed less than (the two bit-vector parameters must have same width) (84)

BITVECTOR_SLE 

bit-vector signed less than or equal (the two bit-vector parameters must have same width) (85)

BITVECTOR_SGT 

bit-vector signed greater than (the two bit-vector parameters must have same width) (86)

BITVECTOR_SGE 

bit-vector signed greater than or equal (the two bit-vector parameters must have same width) (87)

BITVECTOR_EAGER_ATOM 

formula to be treated as a bv atom via eager bit-blasting (internal-only symbol) (88)

BITVECTOR_ACKERMANIZE_UDIV 

term to be treated as a variable; used for eager bit-blasting Ackermann expansion of bvudiv (internal-only symbol) (89)

BITVECTOR_ACKERMANIZE_UREM 

term to be treated as a variable; used for eager bit-blasting Ackermann expansion of bvurem (internal-only symbol) (90)

BITVECTOR_BITOF_OP 

operator for the bit-vector boolean bit extract; payload is an instance of the CVC4::BitVectorBitOf class (91)

BITVECTOR_EXTRACT_OP 

operator for the bit-vector extract; payload is an instance of the CVC4::BitVectorExtract class (92)

BITVECTOR_REPEAT_OP 

operator for the bit-vector repeat; payload is an instance of the CVC4::BitVectorRepeat class (93)

BITVECTOR_ZERO_EXTEND_OP 

operator for the bit-vector zero-extend; payload is an instance of the CVC4::BitVectorZeroExtend class (94)

BITVECTOR_SIGN_EXTEND_OP 

operator for the bit-vector sign-extend; payload is an instance of the CVC4::BitVectorSignExtend class (95)

BITVECTOR_ROTATE_LEFT_OP 

operator for the bit-vector rotate left; payload is an instance of the CVC4::BitVectorRotateLeft class (96)

BITVECTOR_ROTATE_RIGHT_OP 

operator for the bit-vector rotate right; payload is an instance of the CVC4::BitVectorRotateRight class (97)

BITVECTOR_BITOF 

bit-vector boolean bit extract; first parameter is a BITVECTOR_BITOF_OP, second is a bit-vector term (98)

BITVECTOR_EXTRACT 

bit-vector extract; first parameter is a BITVECTOR_EXTRACT_OP, second is a bit-vector term (99)

BITVECTOR_REPEAT 

bit-vector repeat; first parameter is a BITVECTOR_REPEAT_OP, second is a bit-vector term (100)

BITVECTOR_ZERO_EXTEND 

bit-vector zero-extend; first parameter is a BITVECTOR_ZERO_EXTEND_OP, second is a bit-vector term (101)

BITVECTOR_SIGN_EXTEND 

bit-vector sign-extend; first parameter is a BITVECTOR_SIGN_EXTEND_OP, second is a bit-vector term (102)

BITVECTOR_ROTATE_LEFT 

bit-vector rotate left; first parameter is a BITVECTOR_ROTATE_LEFT_OP, second is a bit-vector term (103)

BITVECTOR_ROTATE_RIGHT 

bit-vector rotate right; first parameter is a BITVECTOR_ROTATE_RIGHT_OP, second is a bit-vector term (104)

INT_TO_BITVECTOR_OP 

operator for the integer conversion to bit-vector; payload is an instance of the CVC4::IntToBitVector class (105)

INT_TO_BITVECTOR 

integer conversion to bit-vector; first parameter is an INT_TO_BITVECTOR_OP, second is an integer term (106)

BITVECTOR_TO_NAT 

bit-vector conversion to (nonnegative) integer; parameter is a bit-vector (107)

ARRAY_TYPE 

array type (108)

SELECT 

array select; first parameter is an array term, second is the selection index (109)

STORE 

array store; first parameter is an array term, second is the store index, third is the term to store at the index (110)

STORE_ALL 

array store-all; payload is an instance of the CVC4::ArrayStoreAll class (this is not supported by arrays decision procedure yet, but it is used for returned array models) (111)

ARR_TABLE_FUN 

array table function (internal-only symbol) (112)

ARRAY_LAMBDA 

array lambda (internal-only symbol) (113)

CONSTRUCTOR_TYPE 

constructor (114)

SELECTOR_TYPE 

selector (115)

TESTER_TYPE 

tester (116)

APPLY_CONSTRUCTOR 

constructor application; first parameter is the constructor, remaining parameters (if any) are parameters to the constructor (117)

APPLY_SELECTOR 

selector application; parameter is a datatype term (undefined if mis-applied) (118)

APPLY_SELECTOR_TOTAL 

selector application; parameter is a datatype term (defined rigidly if mis-applied) (119)

APPLY_TESTER 

tester application; first parameter is a tester, second is a datatype term (120)

DATATYPE_TYPE 

a datatype type (121)

PARAMETRIC_DATATYPE 

parametric datatype (122)

APPLY_TYPE_ASCRIPTION 

type ascription, for datatype constructor applications; first parameter is an ASCRIPTION_TYPE, second is the datatype constructor application being ascribed (123)

ASCRIPTION_TYPE 

a type parameter for type ascription; payload is an instance of the CVC4::AscriptionType class (124)

TUPLE_TYPE 

tuple type (125)

TUPLE 

a tuple (N-ary) (126)

TUPLE_SELECT_OP 

operator for a tuple select; payload is an instance of the CVC4::TupleSelect class (127)

TUPLE_SELECT 

tuple select; first parameter is a TUPLE_SELECT_OP, second is the tuple (128)

TUPLE_UPDATE_OP 

operator for a tuple update; payload is an instance of the CVC4::TupleUpdate class (129)

TUPLE_UPDATE 

tuple update; first parameter is a TUPLE_UPDATE_OP (which references an index), second is the tuple, third is the element to store in the tuple at the given index (130)

RECORD_TYPE 

record type (131)

RECORD 

a record; first parameter is a RECORD_TYPE; remaining parameters (if any) are the individual values for fields, in order (132)

RECORD_SELECT_OP 

operator for a record select; payload is an instance CVC4::RecordSelect class (133)

RECORD_SELECT 

record select; first parameter is a RECORD_SELECT_OP, second is a record term to select from (134)

RECORD_UPDATE_OP 

operator for a record update; payload is an instance CVC4::RecordSelect class (135)

RECORD_UPDATE 

record update; first parameter is a RECORD_UPDATE_OP (which references a field), second is a record term to update, third is the element to store in the record in the given field (136)

EMPTYSET 

the empty set constant; payload is an instance of the CVC4::EmptySet class (137)

SET_TYPE 

set type, takes as parameter the type of the elements (138)

UNION 

set union (139)

INTERSECTION 

set intersection (140)

SETMINUS 

set subtraction (141)

SUBSET 

subset predicate; first parameter a subset of second (142)

MEMBER 

set membership predicate; first parameter a member of second (143)

SINGLETON 

the set of the single element given as a parameter (144)

INSERT 

set obtained by inserting elements (first N-1 parameters) into a set (the last parameter) (145)

STRING_CONCAT 

string concat (N-ary) (146)

STRING_IN_REGEXP 

membership (147)

STRING_LENGTH 

string length (148)

STRING_SUBSTR 

string substr (user symbol) (149)

STRING_SUBSTR_TOTAL 

string substr (internal symbol) (150)

STRING_CHARAT 

string charat (user symbol) (151)

STRING_STRCTN 

string contains (152)

STRING_STRIDOF 

string indexof (153)

STRING_STRREPL 

string replace (154)

STRING_PREFIX 

string prefixof (155)

STRING_SUFFIX 

string suffixof (156)

STRING_ITOS 

integer to string (157)

STRING_STOI 

string to integer (total function) (158)

STRING_U16TOS 

uint16 to string (159)

STRING_STOU16 

string to uint16 (160)

STRING_U32TOS 

uint32 to string (161)

STRING_STOU32 

string to uint32 (162)

CONST_STRING 

a string of characters (163)

CONST_REGEXP 

a regular expression (164)

STRING_TO_REGEXP 

convert string to regexp (165)

REGEXP_CONCAT 

regexp concat (166)

REGEXP_UNION 

regexp union (167)

REGEXP_INTER 

regexp intersection (168)

REGEXP_STAR 

regexp * (169)

REGEXP_PLUS 

regexp + (170)

REGEXP_OPT 

regexp ? (171)

REGEXP_RANGE 

regexp range (172)

REGEXP_LOOP 

regexp loop (173)

REGEXP_EMPTY 

regexp empty (174)

REGEXP_SIGMA 

regexp all characters (175)

FORALL 

universally quantified formula; first parameter is an BOUND_VAR_LIST, second is quantifier body, and an optional third parameter is an INST_PATTERN_LIST (176)

EXISTS 

existentially quantified formula; first parameter is an BOUND_VAR_LIST, second is quantifier body, and an optional third parameter is an INST_PATTERN_LIST (177)

INST_CONSTANT 

instantiation constant (178)

BOUND_VAR_LIST 

a list of bound variables (used to bind variables under a quantifier) (179)

INST_PATTERN 

instantiation pattern (180)

INST_PATTERN_LIST 

a list of instantiation patterns (181)

REWRITE_RULE 

general rewrite rule (for rewrite-rules theory) (182)

RR_REWRITE 

actual rewrite rule (for rewrite-rules theory) (183)

RR_REDUCTION 

actual reduction rule (for rewrite-rules theory) (184)

RR_DEDUCTION 

actual deduction rule (for rewrite-rules theory) (185)

LAST_KIND 

marks the upper-bound of this enumeration

Definition at line 60 of file kind.h.

Function Documentation

bool CVC4::kind::isAssociative ( ::CVC4::Kind  k)
inline

Returns true if the given kind is associative.

This is used by ExprManager to decide whether it's safe to modify big expressions by changing the grouping of the arguments.

Definition at line 513 of file kind.h.

References AND, MULT, OR, and PLUS.

std::string CVC4::kind::kindToString ( ::CVC4::Kind  k)
inline

Definition at line 526 of file kind.h.

std::ostream & CVC4::kind::operator<< ( std::ostream &  out,
CVC4::Kind  k 
)
inline

Definition at line 284 of file kind.h.

References ABS, ABSTRACT_VALUE, AND, APPLY, APPLY_CONSTRUCTOR, APPLY_SELECTOR, APPLY_SELECTOR_TOTAL, APPLY_TESTER, APPLY_TYPE_ASCRIPTION, APPLY_UF, ARR_TABLE_FUN, ARRAY_LAMBDA, ARRAY_TYPE, ASCRIPTION_TYPE, BITVECTOR_ACKERMANIZE_UDIV, BITVECTOR_ACKERMANIZE_UREM, BITVECTOR_AND, BITVECTOR_ASHR, BITVECTOR_BITOF, BITVECTOR_BITOF_OP, BITVECTOR_COMP, BITVECTOR_CONCAT, BITVECTOR_EAGER_ATOM, BITVECTOR_EXTRACT, BITVECTOR_EXTRACT_OP, BITVECTOR_LSHR, BITVECTOR_MULT, BITVECTOR_NAND, BITVECTOR_NEG, BITVECTOR_NOR, BITVECTOR_NOT, BITVECTOR_OR, BITVECTOR_PLUS, BITVECTOR_REPEAT, BITVECTOR_REPEAT_OP, BITVECTOR_ROTATE_LEFT, BITVECTOR_ROTATE_LEFT_OP, BITVECTOR_ROTATE_RIGHT, BITVECTOR_ROTATE_RIGHT_OP, BITVECTOR_SDIV, BITVECTOR_SGE, BITVECTOR_SGT, BITVECTOR_SHL, BITVECTOR_SIGN_EXTEND, BITVECTOR_SIGN_EXTEND_OP, BITVECTOR_SLE, BITVECTOR_SLT, BITVECTOR_SMOD, BITVECTOR_SREM, BITVECTOR_SUB, BITVECTOR_TO_NAT, BITVECTOR_TYPE, BITVECTOR_UDIV, BITVECTOR_UDIV_TOTAL, BITVECTOR_UGE, BITVECTOR_UGT, BITVECTOR_ULE, BITVECTOR_ULT, BITVECTOR_UREM, BITVECTOR_UREM_TOTAL, BITVECTOR_XNOR, BITVECTOR_XOR, BITVECTOR_ZERO_EXTEND, BITVECTOR_ZERO_EXTEND_OP, BOUND_VAR_LIST, BOUND_VARIABLE, BUILTIN, CARDINALITY_CONSTRAINT, CHAIN, CHAIN_OP, COMBINED_CARDINALITY_CONSTRAINT, CONST_BITVECTOR, CONST_BOOLEAN, CONST_RATIONAL, CONST_REGEXP, CONST_STRING, CONSTRUCTOR_TYPE, DATATYPE_TYPE, DISTINCT, DIVISIBLE, DIVISIBLE_OP, DIVISION, DIVISION_TOTAL, EMPTYSET, EQUAL, EXISTS, FORALL, FUNCTION, FUNCTION_TYPE, GEQ, GT, IFF, IMPLIES, INSERT, INST_CONSTANT, INST_PATTERN, INST_PATTERN_LIST, INT_TO_BITVECTOR, INT_TO_BITVECTOR_OP, INTERSECTION, INTS_DIVISION, INTS_DIVISION_TOTAL, INTS_MODULUS, INTS_MODULUS_TOTAL, IS_INTEGER, ITE, LAMBDA, LAST_KIND, LEQ, LT, MEMBER, MINUS, MULT, NOT, NULL_EXPR, OR, CVC4::options::out, PARAMETRIC_DATATYPE, PLUS, POW, RECORD, RECORD_SELECT, RECORD_SELECT_OP, RECORD_TYPE, RECORD_UPDATE, RECORD_UPDATE_OP, REGEXP_CONCAT, REGEXP_EMPTY, REGEXP_INTER, REGEXP_LOOP, REGEXP_OPT, REGEXP_PLUS, REGEXP_RANGE, REGEXP_SIGMA, REGEXP_STAR, REGEXP_UNION, REWRITE_RULE, RR_DEDUCTION, RR_REDUCTION, RR_REWRITE, SELECT, SELECTOR_TYPE, SET_TYPE, SETMINUS, SEXPR, SEXPR_TYPE, SINGLETON, SKOLEM, SORT_TAG, SORT_TYPE, STORE, STORE_ALL, STRING_CHARAT, STRING_CONCAT, STRING_IN_REGEXP, STRING_ITOS, STRING_LENGTH, STRING_PREFIX, STRING_STOI, STRING_STOU16, STRING_STOU32, STRING_STRCTN, STRING_STRIDOF, STRING_STRREPL, STRING_SUBSTR, STRING_SUBSTR_TOTAL, STRING_SUFFIX, STRING_TO_REGEXP, STRING_U16TOS, STRING_U32TOS, SUBRANGE_TYPE, SUBSET, SUBTYPE_TYPE, TESTER_TYPE, TO_INTEGER, TO_REAL, TUPLE, TUPLE_SELECT, TUPLE_SELECT_OP, TUPLE_TYPE, TUPLE_UPDATE, TUPLE_UPDATE_OP, TYPE_CONSTANT, UMINUS, UNDEFINED_KIND, UNINTERPRETED_CONSTANT, UNION, VARIABLE, and XOR.