49 #ifndef __CVC4__KIND_H 50 #define __CVC4__KIND_H 294 case SORT_TAG: out <<
"SORT_TAG";
break;
295 case SORT_TYPE: out <<
"SORT_TYPE";
break;
298 case BUILTIN: out <<
"BUILTIN";
break;
299 case FUNCTION: out <<
"FUNCTION";
break;
300 case APPLY: out <<
"APPLY";
break;
301 case EQUAL: out <<
"EQUAL";
break;
302 case DISTINCT: out <<
"DISTINCT";
break;
303 case VARIABLE: out <<
"VARIABLE";
break;
305 case SKOLEM: out <<
"SKOLEM";
break;
306 case SEXPR: out <<
"SEXPR";
break;
307 case LAMBDA: out <<
"LAMBDA";
break;
308 case CHAIN: out <<
"CHAIN";
break;
309 case CHAIN_OP: out <<
"CHAIN_OP";
break;
317 case NOT: out <<
"NOT";
break;
318 case AND: out <<
"AND";
break;
319 case IFF: out <<
"IFF";
break;
320 case IMPLIES: out <<
"IMPLIES";
break;
321 case OR: out <<
"OR";
break;
322 case XOR: out <<
"XOR";
break;
323 case ITE: out <<
"ITE";
break;
326 case APPLY_UF: out <<
"APPLY_UF";
break;
331 case PLUS: out <<
"PLUS";
break;
332 case MULT: out <<
"MULT";
break;
333 case MINUS: out <<
"MINUS";
break;
334 case UMINUS: out <<
"UMINUS";
break;
335 case DIVISION: out <<
"DIVISION";
break;
341 case ABS: out <<
"ABS";
break;
342 case DIVISIBLE: out <<
"DIVISIBLE";
break;
343 case POW: out <<
"POW";
break;
347 case LT: out <<
"LT";
break;
348 case LEQ: out <<
"LEQ";
break;
349 case GT: out <<
"GT";
break;
350 case GEQ: out <<
"GEQ";
break;
353 case TO_REAL: out <<
"TO_REAL";
break;
412 case SELECT: out <<
"SELECT";
break;
413 case STORE: out <<
"STORE";
break;
414 case STORE_ALL: out <<
"STORE_ALL";
break;
431 case TUPLE: out <<
"TUPLE";
break;
437 case RECORD: out <<
"RECORD";
break;
444 case EMPTYSET: out <<
"EMPTYSET";
break;
445 case SET_TYPE: out <<
"SET_TYPE";
break;
446 case UNION: out <<
"UNION";
break;
448 case SETMINUS: out <<
"SETMINUS";
break;
449 case SUBSET: out <<
"SUBSET";
break;
450 case MEMBER: out <<
"MEMBER";
break;
451 case SINGLETON: out <<
"SINGLETON";
break;
452 case INSERT: out <<
"INSERT";
break;
487 case FORALL: out <<
"FORALL";
break;
488 case EXISTS: out <<
"EXISTS";
break;
500 case LAST_KIND: out <<
"LAST_KIND";
break;
501 default: out <<
"UNKNOWNKIND!" << int(k);
break;
507 #line 64 "/builddir/build/BUILD/cvc4-1.4/builds/x86_64-redhat-linux-gnu/production-abc-proof/../../../src/expr/kind_template.h" 527 std::stringstream ss;
555 #line 102 "/builddir/build/BUILD/cvc4-1.4/builds/x86_64-redhat-linux-gnu/production-abc-proof/../../../src/expr/kind_template.h" 569 switch(typeConstant) {
572 case REAL_TYPE: out <<
"real type";
break;
579 case RRHB_TYPE: out <<
"head and body of the rule type (for rewrite-rules theory)";
break;
581 #line 118 "/builddir/build/BUILD/cvc4-1.4/builds/x86_64-redhat-linux-gnu/production-abc-proof/../../../src/expr/kind_template.h" 583 out <<
"UNKNOWN_TYPE_CONSTANT";
603 #line 130 "/builddir/build/BUILD/cvc4-1.4/builds/x86_64-redhat-linux-gnu/production-abc-proof/../../../src/expr/kind_template.h" 611 return id =
static_cast<TheoryId>(((int)
id) + 1);
618 case THEORY_UF: out <<
"THEORY_UF";
break;
620 case THEORY_BV: out <<
"THEORY_BV";
break;
627 #line 144 "/builddir/build/BUILD/cvc4-1.4/builds/x86_64-redhat-linux-gnu/production-abc-proof/../../../src/expr/kind_template.h" 629 out <<
"UNKNOWN_THEORY";
826 #line 158 "/builddir/build/BUILD/cvc4-1.4/builds/x86_64-redhat-linux-gnu/production-abc-proof/../../../src/expr/kind_template.h" 834 switch(typeConstant) {
846 #line 168 "/builddir/build/BUILD/cvc4-1.4/builds/x86_64-redhat-linux-gnu/production-abc-proof/../../../src/expr/kind_template.h"
bit-vector rotate left; first parameter is a BITVECTOR_ROTATE_LEFT_OP, second is a bit-vector term (1...
unary negation of a bit-vector (69)
truth and falsity; payload is a (C++) bool (21)
integer modulus with interpreted division by 0 (internal symbol) (41)
TypeConstant
The enumeration for the built-in atomic types.
multiplication of two or more bit-vectors (66)
the kind of expressions representing abstract values (other than uninterpreted sort constants); paylo...
bit-vector arithmetic shift right (the two bit-vector parameters must have same width) (79) ...
general rewrite rule (for rewrite-rules theory) (182)
logical equivalence (exactly two parameters) (24)
existentially quantified formula; first parameter is an BOUND_VAR_LIST, second is quantifier body...
bitwise nand of two bit-vectors (62)
bitwise or of two or more bit-vectors (59)
a multiple-precision rational constant; payload is an instance of the CVC4::Rational class (47) ...
operator for a record update; payload is an instance CVC4::RecordSelect class (135) ...
specifies types of user-declared 'uninterpreted' sorts (2)
integer modulus, division by 0 undefined (user symbol) (40)
operator for the bit-vector zero-extend; payload is an instance of the CVC4::BitVectorZeroExtend clas...
regexp all characters (175)
divisibility-by-k predicate; first parameter is a DIVISIBLE_OP, second is integer term (43) ...
the set of the single element given as a parameter (144)
2's complement signed remainder (sign follows dividend) (73)
arithmetic unary negation (35)
bit-vector signed greater than or equal (the two bit-vector parameters must have same width) (87) ...
string concat (N-ary) (146)
TheoryId kindToTheoryId(::CVC4::Kind k)
const TheoryId THEORY_SAT_SOLVER
the chained operator; payload is an instance of the CVC4::Chain class (16)
operator for the bit-vector repeat; payload is an instance of the CVC4::BitVectorRepeat class (93) ...
string substr (user symbol) (149)
head and body of the rule type (for rewrite-rules theory)
exclusive or (exactly two parameters) (27)
a list of instantiation patterns (181)
bool isAssociative(::CVC4::Kind k)
Returns true if the given kind is associative.
string to integer (total function) (158)
a record; first parameter is a RECORD_TYPE; remaining parameters (if any) are the individual values f...
actual reduction rule (for rewrite-rules theory) (184)
predicate subtype; payload is an instance of the CVC4::Predicate class (20)
string substr (internal symbol) (150)
integer division, division by 0 undefined (user symbol) (38)
bit-vector rotate right; first parameter is a BITVECTOR_ROTATE_RIGHT_OP, second is a bit-vector term ...
the type for built-in operators
tester application; first parameter is a tester, second is a datatype term (120)
regexp intersection (168)
subtraction of two bit-vectors (68)
::CVC4::kind::Kind_t Kind
selector application; parameter is a datatype term (undefined if mis-applied) (118) ...
bit-vector unsigned greater than (the two bit-vector parameters must have same width) (82) ...
size_t operator()(TypeConstant tc) const
operator for the divisibility-by-k predicate; payload is an instance of the CVC4::Divisible class (45...
bit-vector signed less than (the two bit-vector parameters must have same width) (84) ...
chained operator (N-ary), turned into a conjuction of binary applications of the operator on adjoinin...
operator for a tuple select; payload is an instance of the CVC4::TupleSelect class (127) ...
operator for the integer conversion to bit-vector; payload is an instance of the CVC4::IntToBitVector...
bit-vector boolean bit extract; first parameter is a BITVECTOR_BITOF_OP, second is a bit-vector term ...
bit-vector unsigned less than (the two bit-vector parameters must have same width) (80) ...
TheoryId & operator++(TheoryId &id)
const TheoryId THEORY_FIRST
a variable (not permitted in bindings) (10)
CVC4's exception base class and some associated utilities.
a bound variable (permitted in bindings and the associated lambda and quantifier bodies only) (11) ...
bitwise xnor of two bit-vectors (64)
a string of characters (163)
array select; first parameter is an array term, second is the selection index (109) ...
array store-all; payload is an instance of the CVC4::ArrayStoreAll class (this is not supported by ar...
a regular expression (164)
real division with interpreted division by 0 (internal symbol) (37)
operator for the bit-vector extract; payload is an instance of the CVC4::BitVectorExtract class (92) ...
addition of two or more bit-vectors (67)
a fixed-width bit-vector constant; payload is an instance of the CVC4::BitVector class (56) ...
bit-vector repeat; first parameter is a BITVECTOR_REPEAT_OP, second is a bit-vector term (100) ...
marks the upper-bound of this enumeration
disequality (N-ary, sorts must match) (9)
application of an uninterpreted function; first parameter is the function, remaining ones are paramet...
bitwise nor of two bit-vectors (63)
bit-vector signed greater than (the two bit-vector parameters must have same width) (86) ...
arithmetic multiplication (N-ary) (33)
std::ostream & operator<<(std::ostream &, CVC4::Kind)
operator for the bit-vector rotate right; payload is an instance of the CVC4::BitVectorRotateRight cl...
bit-vector signed less than or equal (the two bit-vector parameters must have same width) (85) ...
actual rewrite rule (for rewrite-rules theory) (183)
set obtained by inserting elements (first N-1 parameters) into a set (the last parameter) (145) ...
type ascription, for datatype constructor applications; first parameter is an ASCRIPTION_TYPE, second is the datatype constructor application being ascribed (123)
bit-vector extract; first parameter is a BITVECTOR_EXTRACT_OP, second is a bit-vector term (99) ...
arithmetic binary subtraction operator (34)
set type, takes as parameter the type of the elements (138)
logical implication (exactly two parameters) (25)
real division, division by 0 undefined (user symbol) (36)
the kind of expressions representing uninterpreted constants; payload is an instance of the CVC4::Uni...
the type of an integer subrange (46)
a lambda expression; first parameter is a BOUND_VAR_LIST, second is lambda body (14) ...
record select; first parameter is a RECORD_SELECT_OP, second is a record term to select from (134) ...
unsigned remainder from truncating division of two bit-vectors (defined to be equal to the dividend...
bitwise xor of two or more bit-vectors (60)
2's complement signed remainder (sign follows divisor) (74)
operator for the bit-vector rotate left; payload is an instance of the CVC4::BitVectorRotateLeft clas...
constructor application; first parameter is the constructor, remaining parameters (if any) are parame...
Macros that should be defined everywhere during the building of the libraries and driver binary...
array table function (internal-only symbol) (112)
greater than or equal, x >= y (51)
operator for the bit-vector sign-extend; payload is an instance of the CVC4::BitVectorSignExtend clas...
less than or equal, x <= y (49)
bit-vector sign-extend; first parameter is a BITVECTOR_SIGN_EXTEND_OP, second is a bit-vector term (1...
application of a defined function (7)
instantiation constant (178)
the type of instantiation pattern lists
convert term to integer by the floor function (parameter is a real-sorted term) (53) ...
integer division with interpreted division by 0 (internal symbol) (39)
the type of a symbolic expression (19)
instantiation pattern (180)
term to be treated as a variable; used for eager bit-blasting Ackermann expansion of bvurem (internal...
arithmetic addition (N-ary) (32)
the type of bound variable lists
bitwise and of two or more bit-vectors (58)
a list of bound variables (used to bind variables under a quantifier) (179)
2's complement signed division (72)
equality (two parameters only, sorts must match) (8)
unsigned division of two bit-vectors, truncating towards 0 (undefined if divisor is 0) (70) ...
unsigned division of two bit-vectors, truncating towards 0 (defined to be the all-ones bit pattern...
term-is-integer predicate (parameter is a real-sorted term) (52)
std::string kindToString(::CVC4::Kind k)
term to be treated as a variable; used for eager bit-blasting Ackermann expansion of bvudiv (internal...
parametric datatype (122)
a symbolic expression (any arity) (13)
TheoryId typeConstantToTheoryId(::CVC4::TypeConstant typeConstant)
operator for a tuple update; payload is an instance of the CVC4::TupleUpdate class (129) ...
a Skolem variable (internal only) (12)
tuple select; first parameter is a TUPLE_SELECT_OP, second is the tuple (128)
struct CVC4::options::out__option_t out
array lambda (internal-only symbol) (113)
string charat (user symbol) (151)
bit-vector zero-extend; first parameter is a BITVECTOR_ZERO_EXTEND_OP, second is a bit-vector term (1...
instantiation pattern type
bit-vector shift left (the two bit-vector parameters must have same width) (77)
operator for a record select; payload is an instance CVC4::RecordSelect class (133) ...
cast term to real (parameter is an integer-sorted term; this is a no-op in CVC4, as integer is a subt...
tuple update; first parameter is a TUPLE_UPDATE_OP (which references an index), second is the tuple...
selector application; parameter is a datatype term (defined rigidly if mis-applied) (119) ...
size_t operator()(::CVC4::Kind k) const
concatenation of two or more bit-vectors (57)
subset predicate; first parameter a subset of second (142)
bit-vector unsigned less than or equal (the two bit-vector parameters must have same width) (81) ...
combined cardinality constraint; parameter is a positive integer constant k that bounds the sum of th...
the kind of expressions representing built-in operators (5)
a type parameter for type ascription; payload is an instance of the CVC4::AscriptionType class (124) ...
array store; first parameter is an array term, second is the store index, third is the term to store ...
operator for the bit-vector boolean bit extract; payload is an instance of the CVC4::BitVectorBitOf c...
bit-vector conversion to (nonnegative) integer; parameter is a bit-vector (107)
actual deduction rule (for rewrite-rules theory) (185)
record update; first parameter is a RECORD_UPDATE_OP (which references a field), second is a record t...
convert string to regexp (165)
set membership predicate; first parameter a member of second (143)
a representation for basic types (17)
integer conversion to bit-vector; first parameter is an INT_TO_BITVECTOR_OP, second is an integer ter...
unsigned remainder from truncating division of two bit-vectors (undefined if divisor is 0) (71) ...
bitwise not of a bit-vector (61)
the empty set constant; payload is an instance of the CVC4::EmptySet class (137)
equality comparison of two bit-vectors (returns one bit) (65)
bit-vector unsigned greater than or equal (the two bit-vector parameters must have same width) (83) ...
We hash the constants with their values.
universally quantified formula; first parameter is an BOUND_VAR_LIST, second is quantifier body...
formula to be treated as a bv atom via eager bit-blasting (internal-only symbol) (88) ...
if-then-else, used for both Boolean and term ITE constructs; first parameter is (Boolean-sorted) cond...
cardinality constraint on sort S: first parameter is (any) term of sort S, second is a positive integ...
bit-vector logical shift right (the two bit-vector parameters must have same width) (78) ...