- Generated by
1.8.11
|
cvc4-1.4
|
Data Structures | |
| struct | KindHashFunction |
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) |
| enum CVC4::kind::Kind_t |
| 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 |
|
inline |
|
inline |
|
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.
1.8.11