49 #ifndef __CVC4__KIND_H
50 #define __CVC4__KIND_H
255 using namespace CVC4::kind;
264 case SORT_TAG: out <<
"SORT_TAG";
break;
265 case SORT_TYPE: out <<
"SORT_TYPE";
break;
268 case BUILTIN: out <<
"BUILTIN";
break;
269 case FUNCTION: out <<
"FUNCTION";
break;
270 case APPLY: out <<
"APPLY";
break;
271 case EQUAL: out <<
"EQUAL";
break;
272 case DISTINCT: out <<
"DISTINCT";
break;
273 case VARIABLE: out <<
"VARIABLE";
break;
275 case SKOLEM: out <<
"SKOLEM";
break;
276 case SEXPR: out <<
"SEXPR";
break;
277 case LAMBDA: out <<
"LAMBDA";
break;
278 case CHAIN: out <<
"CHAIN";
break;
279 case CHAIN_OP: out <<
"CHAIN_OP";
break;
287 case NOT: out <<
"NOT";
break;
288 case AND: out <<
"AND";
break;
289 case IFF: out <<
"IFF";
break;
290 case IMPLIES: out <<
"IMPLIES";
break;
291 case OR: out <<
"OR";
break;
292 case XOR: out <<
"XOR";
break;
293 case ITE: out <<
"ITE";
break;
296 case APPLY_UF: out <<
"APPLY_UF";
break;
301 case PLUS: out <<
"PLUS";
break;
302 case MULT: out <<
"MULT";
break;
303 case MINUS: out <<
"MINUS";
break;
304 case UMINUS: out <<
"UMINUS";
break;
305 case DIVISION: out <<
"DIVISION";
break;
311 case ABS: out <<
"ABS";
break;
312 case DIVISIBLE: out <<
"DIVISIBLE";
break;
313 case POW: out <<
"POW";
break;
317 case LT: out <<
"LT";
break;
318 case LEQ: out <<
"LEQ";
break;
319 case GT: out <<
"GT";
break;
320 case GEQ: out <<
"GEQ";
break;
323 case TO_REAL: out <<
"TO_REAL";
break;
379 case SELECT: out <<
"SELECT";
break;
380 case STORE: out <<
"STORE";
break;
381 case STORE_ALL: out <<
"STORE_ALL";
break;
396 case TUPLE: out <<
"TUPLE";
break;
402 case RECORD: out <<
"RECORD";
break;
409 case FORALL: out <<
"FORALL";
break;
410 case EXISTS: out <<
"EXISTS";
break;
433 case REGEXP_OR: out <<
"REGEXP_OR";
break;
440 case LAST_KIND: out <<
"LAST_KIND";
break;
441 default: out <<
"UNKNOWNKIND!" << int(k);
break;
447 #line 64 "/builddir/build/BUILD/cvc4-1.3/builds/aarch64-redhat-linux-gnu/default-proof/../../../src/expr/kind_template.h"
467 std::stringstream ss;
495 #line 102 "/builddir/build/BUILD/cvc4-1.3/builds/aarch64-redhat-linux-gnu/default-proof/../../../src/expr/kind_template.h"
509 switch(typeConstant) {
512 case REAL_TYPE: out <<
"Real type";
break;
517 case RRHB_TYPE: out <<
"head and body of the rule type";
break;
521 #line 118 "/builddir/build/BUILD/cvc4-1.3/builds/aarch64-redhat-linux-gnu/default-proof/../../../src/expr/kind_template.h"
523 out <<
"UNKNOWN_TYPE_CONSTANT";
543 #line 130 "/builddir/build/BUILD/cvc4-1.3/builds/aarch64-redhat-linux-gnu/default-proof/../../../src/expr/kind_template.h"
551 return id =
static_cast<TheoryId>(((int)
id) + 1);
558 case THEORY_UF: out <<
"THEORY_UF";
break;
560 case THEORY_BV: out <<
"THEORY_BV";
break;
567 #line 144 "/builddir/build/BUILD/cvc4-1.3/builds/aarch64-redhat-linux-gnu/default-proof/../../../src/expr/kind_template.h"
569 out <<
"UNKNOWN_THEORY";
736 #line 158 "/builddir/build/BUILD/cvc4-1.3/builds/aarch64-redhat-linux-gnu/default-proof/../../../src/expr/kind_template.h"
744 switch(typeConstant) {
756 #line 168 "/builddir/build/BUILD/cvc4-1.3/builds/aarch64-redhat-linux-gnu/default-proof/../../../src/expr/kind_template.h"
bit-vector unary negation
ints modulus with interpreted division by 0 (internal symbol)
TypeConstant
The enumeration for the built-in atomic types.
bit-vector multiplication
The kind of expressions representing abstract values (other than uninterpreted sort constants) ...
bit-vector arithmetic shift right
existentially quantified formula
a multiple-precision rational constant
operator for a record update
ints modulus (user symbol)
operator for the bit-vector zero-extend
divisibility-by-k predicate
bit-vector 2's complement signed remainder (sign follows dividend)
arithmetic unary negation
signed greater than or equal
TheoryId kindToTheoryId(::CVC4::Kind k)
const TheoryId THEORY_SAT_SOLVER
operator for the bit-vector repeat
head and body of the rule type
instantiation pattern list
bool isAssociative(::CVC4::Kind k)
Returns true if the given kind is associative.
ints division (user symbol)
Built in type for built in operators.
::CVC4::kind::Kind_t Kind
bit-vector unsigned greater than
size_t operator()(TypeConstant tc) const
operator for the divisibility-by-k predicate
bit-vector signed less than
operator for a tuple select
operator for the integer conversion to bit-vector
bit-vector boolean bit extract
bit-vector unsigned less than
TheoryId & operator++(TheoryId &id)
const TheoryId THEORY_FIRST
CVC4's exception base class and some associated utilities.
real division with interpreted division by 0 (internal symbol)
operator for the bit-vector extract
This is CVC4 release version For build and installation please see the INSTALL file included with this distribution This first official release of CVC4 is the result of more than three years of efforts by researchers at New York University and The University of Iowa The project leaders are Clark please refer to the AUTHORS file in the source distribution CVC4 is a tool for determining the satisfiability of a first order formula modulo a first order CVC CVC3 but does not directly incorporate code from any previous version CVC4 is intended to be an open and extensible SMT engine It can be used as a stand alone tool or as a library It has been designed to increase the performance and reduce the memory overhead of its predecessors It is written entirely in C and is released under a free software see the INSTALL file that comes with this distribution We recommend that you visit our CVC4 tutorials online please write to the cvc users cs nyu edu mailing list *if you need to report a bug with CVC4
a fixed-width bit-vector constant
marks the upper-bound of this enumeration
uninterpreted function application
This is CVC4 release version For build and installation please see the INSTALL file included with this distribution This first official release of CVC4 is the result of more than three years of efforts by researchers at New York University and The University of Iowa The project leaders are Clark please refer to the AUTHORS file in the source distribution CVC4 is a tool for determining the satisfiability of a first order formula modulo a first order theory(or a combination of such theories).It is the fourth in the Cooperating Validity Checker family of tools(CVC
bit-vector signed greater than
arithmetic multiplication
std::ostream & operator<<(std::ostream &, CVC4::Kind)
operator for the bit-vector rotate right
bit-vector signed less than or equal
type ascription, for datatype constructor applications
arithmetic binary subtraction operator
real division (user symbol)
The kind of expressions representing uninterpreted constants.
the type of an integer subrange
bit-vector total unsigned remainder from truncating division (undefined if divisor is 0) ...
bit-vector 2's complement signed remainder (sign follows divisor)
operator for the bit-vector rotate left
Macros that should be defined everywhere during the building of the libraries and driver binary...
array table function (internal symbol)
greater than or equal, x >= y
operator for the bit-vector sign-extend
less than or equal, x <= y
defined function application
Instantiation pattern list type.
ints division with interpreted division by 0 (internal symbol)
bit-vector 2's complement signed division
bit-vector unsigned division, truncating towards 0 (undefined if divisor is 0)
bit-vector total unsigned division, truncating towards 0 (undefined if divisor is 0) ...
std::string kindToString(::CVC4::Kind k)
TheoryId typeConstantToTheoryId(::CVC4::TypeConstant typeConstant)
operator for a tuple update
struct CVC4::options::out__option_t out
Instantiation pattern type.
operator for a record select
size_t operator()(::CVC4::Kind k) const
bit-vector unsigned less than or equal
combined cardinality constraint
The kind of expressions representing built-in operators.
a type parameter for type ascription
operator for the bit-vector boolean bit extract
bit-vector conversion to (nonnegative) integer
integer conversion to bit-vector
bit-vector unsigned remainder from truncating division (undefined if divisor is 0) ...
equality comparison (returns one bit)
bit-vector unsigned greater than or equal
We hash the constants with their values.
universally quantified formula
bit-vector logical shift right