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.