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.