CVC4::kind Namespace Reference

Data Structures
struct	KindHashFunction

Enumerations
enum	Kind_t {   UNDEFINED_KIND, NULL_EXPR, SORT_TAG, SORT_TYPE,   UNINTERPRETED_CONSTANT, ABSTRACT_VALUE, BUILTIN, FUNCTION,   APPLY, EQUAL, DISTINCT, VARIABLE,   BOUND_VARIABLE, SKOLEM, SEXPR, LAMBDA,   CHAIN, CHAIN_OP, TYPE_CONSTANT, FUNCTION_TYPE,   SEXPR_TYPE, SUBTYPE_TYPE, CONST_BOOLEAN, NOT,   AND, IFF, IMPLIES, OR,   XOR, ITE, APPLY_UF, CARDINALITY_CONSTRAINT,   COMBINED_CARDINALITY_CONSTRAINT, PLUS, MULT, MINUS,   UMINUS, DIVISION, DIVISION_TOTAL, INTS_DIVISION,   INTS_DIVISION_TOTAL, INTS_MODULUS, INTS_MODULUS_TOTAL, ABS,   DIVISIBLE, POW, DIVISIBLE_OP, SUBRANGE_TYPE,   CONST_RATIONAL, LT, LEQ, GT,   GEQ, IS_INTEGER, TO_INTEGER, TO_REAL,   BITVECTOR_TYPE, CONST_BITVECTOR, BITVECTOR_CONCAT, BITVECTOR_AND,   BITVECTOR_OR, BITVECTOR_XOR, BITVECTOR_NOT, BITVECTOR_NAND,   BITVECTOR_NOR, BITVECTOR_XNOR, BITVECTOR_COMP, BITVECTOR_MULT,   BITVECTOR_PLUS, BITVECTOR_SUB, BITVECTOR_NEG, BITVECTOR_UDIV,   BITVECTOR_UREM, BITVECTOR_SDIV, BITVECTOR_SREM, BITVECTOR_SMOD,   BITVECTOR_UDIV_TOTAL, BITVECTOR_UREM_TOTAL, BITVECTOR_SHL, BITVECTOR_LSHR,   BITVECTOR_ASHR, BITVECTOR_ULT, BITVECTOR_ULE, BITVECTOR_UGT,   BITVECTOR_UGE, BITVECTOR_SLT, BITVECTOR_SLE, BITVECTOR_SGT,   BITVECTOR_SGE, BITVECTOR_BITOF_OP, BITVECTOR_EXTRACT_OP, BITVECTOR_REPEAT_OP,   BITVECTOR_ZERO_EXTEND_OP, BITVECTOR_SIGN_EXTEND_OP, BITVECTOR_ROTATE_LEFT_OP, BITVECTOR_ROTATE_RIGHT_OP,   BITVECTOR_BITOF, BITVECTOR_EXTRACT, BITVECTOR_REPEAT, BITVECTOR_ZERO_EXTEND,   BITVECTOR_SIGN_EXTEND, BITVECTOR_ROTATE_LEFT, BITVECTOR_ROTATE_RIGHT, INT_TO_BITVECTOR_OP,   INT_TO_BITVECTOR, BITVECTOR_TO_NAT, ARRAY_TYPE, SELECT,   STORE, STORE_ALL, ARR_TABLE_FUN, CONSTRUCTOR_TYPE,   SELECTOR_TYPE, TESTER_TYPE, APPLY_CONSTRUCTOR, APPLY_SELECTOR,   APPLY_TESTER, DATATYPE_TYPE, PARAMETRIC_DATATYPE, APPLY_TYPE_ASCRIPTION,   ASCRIPTION_TYPE, TUPLE_TYPE, TUPLE, TUPLE_SELECT_OP,   TUPLE_SELECT, TUPLE_UPDATE_OP, TUPLE_UPDATE, RECORD_TYPE,   RECORD, RECORD_SELECT_OP, RECORD_SELECT, RECORD_UPDATE_OP,   RECORD_UPDATE, FORALL, EXISTS, INST_CONSTANT,   BOUND_VAR_LIST, INST_PATTERN, INST_PATTERN_LIST, REWRITE_RULE,   RR_REWRITE, RR_REDUCTION, RR_DEDUCTION, STRING_CONCAT,   STRING_IN_REGEXP, STRING_LENGTH, STRING_SUBSTR, CONST_STRING,   CONST_REGEXP, STRING_TO_REGEXP, REGEXP_CONCAT, REGEXP_OR,   REGEXP_INTER, REGEXP_STAR, REGEXP_PLUS, REGEXP_OPT,   REGEXP_RANGE, LAST_KIND }

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)

Enumeration Type Documentation

enum CVC4::kind::Kind_t

Enumerator
UNDEFINED_KIND	undefined
NULL_EXPR	Null kind.
SORT_TAG	sort tag
SORT_TYPE	sort type
UNINTERPRETED_CONSTANT	The kind of expressions representing uninterpreted constants.
ABSTRACT_VALUE	The kind of expressions representing abstract values (other than uninterpreted sort constants)
BUILTIN	The kind of expressions representing built-in operators.
FUNCTION	function
APPLY	defined function application
EQUAL	equality
DISTINCT	disequality
VARIABLE	variable
BOUND_VARIABLE	bound variable
SKOLEM	skolem var
SEXPR	a symbolic expression
LAMBDA	lambda
CHAIN	chained operator
CHAIN_OP	the chained operator
TYPE_CONSTANT	basic types
FUNCTION_TYPE	function type
SEXPR_TYPE	symbolic expression type
SUBTYPE_TYPE	predicate subtype
CONST_BOOLEAN	truth and falsity
NOT	logical not
AND	logical and
IFF	logical equivalence
IMPLIES	logical implication
OR	logical or
XOR	exclusive or
ITE	if-then-else
APPLY_UF	uninterpreted function application
CARDINALITY_CONSTRAINT	cardinality constraint
COMBINED_CARDINALITY_CONSTRAINT	combined cardinality constraint
PLUS	arithmetic addition
MULT	arithmetic multiplication
MINUS	arithmetic binary subtraction operator
UMINUS	arithmetic unary negation
DIVISION	real division (user symbol)
DIVISION_TOTAL	real division with interpreted division by 0 (internal symbol)
INTS_DIVISION	ints division (user symbol)
INTS_DIVISION_TOTAL	ints division with interpreted division by 0 (internal symbol)
INTS_MODULUS	ints modulus (user symbol)
INTS_MODULUS_TOTAL	ints modulus with interpreted division by 0 (internal symbol)
ABS	absolute value
DIVISIBLE	divisibility-by-k predicate
POW	arithmetic power
DIVISIBLE_OP	operator for the divisibility-by-k predicate
SUBRANGE_TYPE	the type of an integer subrange
CONST_RATIONAL	a multiple-precision rational constant
LT	less than, x < y
LEQ	less than or equal, x <= y
GT	greater than, x > y
GEQ	greater than or equal, x >= y
IS_INTEGER	term is integer
TO_INTEGER	cast term to integer
TO_REAL	cast term to real
BITVECTOR_TYPE	bit-vector type
CONST_BITVECTOR	a fixed-width bit-vector constant
BITVECTOR_CONCAT	bit-vector concatenation
BITVECTOR_AND	bitwise and
BITVECTOR_OR	bitwise or
BITVECTOR_XOR	bitwise xor
BITVECTOR_NOT	bitwise not
BITVECTOR_NAND	bitwise nand
BITVECTOR_NOR	bitwise nor
BITVECTOR_XNOR	bitwise xnor
BITVECTOR_COMP	equality comparison (returns one bit)
BITVECTOR_MULT	bit-vector multiplication
BITVECTOR_PLUS	bit-vector addition
BITVECTOR_SUB	bit-vector subtraction
BITVECTOR_NEG	bit-vector unary negation
BITVECTOR_UDIV	bit-vector unsigned division, truncating towards 0 (undefined if divisor is 0)
BITVECTOR_UREM	bit-vector unsigned remainder from truncating division (undefined if divisor is 0)
BITVECTOR_SDIV	bit-vector 2's complement signed division
BITVECTOR_SREM	bit-vector 2's complement signed remainder (sign follows dividend)
BITVECTOR_SMOD	bit-vector 2's complement signed remainder (sign follows divisor)
BITVECTOR_UDIV_TOTAL	bit-vector total unsigned division, truncating towards 0 (undefined if divisor is 0)
BITVECTOR_UREM_TOTAL	bit-vector total unsigned remainder from truncating division (undefined if divisor is 0)
BITVECTOR_SHL	bit-vector left shift
BITVECTOR_LSHR	bit-vector logical shift right
BITVECTOR_ASHR	bit-vector arithmetic shift right
BITVECTOR_ULT	bit-vector unsigned less than
BITVECTOR_ULE	bit-vector unsigned less than or equal
BITVECTOR_UGT	bit-vector unsigned greater than
BITVECTOR_UGE	bit-vector unsigned greater than or equal
BITVECTOR_SLT	bit-vector signed less than
BITVECTOR_SLE	bit-vector signed less than or equal
BITVECTOR_SGT	bit-vector signed greater than
BITVECTOR_SGE	signed greater than or equal
BITVECTOR_BITOF_OP	operator for the bit-vector boolean bit extract
BITVECTOR_EXTRACT_OP	operator for the bit-vector extract
BITVECTOR_REPEAT_OP	operator for the bit-vector repeat
BITVECTOR_ZERO_EXTEND_OP	operator for the bit-vector zero-extend
BITVECTOR_SIGN_EXTEND_OP	operator for the bit-vector sign-extend
BITVECTOR_ROTATE_LEFT_OP	operator for the bit-vector rotate left
BITVECTOR_ROTATE_RIGHT_OP	operator for the bit-vector rotate right
BITVECTOR_BITOF	bit-vector boolean bit extract
BITVECTOR_EXTRACT	bit-vector extract
BITVECTOR_REPEAT	bit-vector repeat
BITVECTOR_ZERO_EXTEND	bit-vector zero-extend
BITVECTOR_SIGN_EXTEND	bit-vector sign-extend
BITVECTOR_ROTATE_LEFT	bit-vector rotate left
BITVECTOR_ROTATE_RIGHT	bit-vector rotate right
INT_TO_BITVECTOR_OP	operator for the integer conversion to bit-vector
INT_TO_BITVECTOR	integer conversion to bit-vector
BITVECTOR_TO_NAT	bit-vector conversion to (nonnegative) integer
ARRAY_TYPE	array type
SELECT	array select
STORE	array store
STORE_ALL	array store-all
ARR_TABLE_FUN	array table function (internal symbol)
CONSTRUCTOR_TYPE	constructor
SELECTOR_TYPE	selector
TESTER_TYPE	tester
APPLY_CONSTRUCTOR	constructor application
APPLY_SELECTOR	selector application
APPLY_TESTER	tester application
DATATYPE_TYPE	datatype type
PARAMETRIC_DATATYPE	parametric datatype
APPLY_TYPE_ASCRIPTION	type ascription, for datatype constructor applications
ASCRIPTION_TYPE	a type parameter for type ascription
TUPLE_TYPE	tuple type
TUPLE	a tuple
TUPLE_SELECT_OP	operator for a tuple select
TUPLE_SELECT	tuple select
TUPLE_UPDATE_OP	operator for a tuple update
TUPLE_UPDATE	tuple update
RECORD_TYPE	record type
RECORD	a record
RECORD_SELECT_OP	operator for a record select
RECORD_SELECT	record select
RECORD_UPDATE_OP	operator for a record update
RECORD_UPDATE	record update
FORALL	universally quantified formula
EXISTS	existentially quantified formula
INST_CONSTANT	instantiation constant
BOUND_VAR_LIST	bound variables
INST_PATTERN	instantiation pattern
INST_PATTERN_LIST	instantiation pattern list
REWRITE_RULE	general rewrite rule
RR_REWRITE	actual rewrite rule
RR_REDUCTION	actual reduction rule
RR_DEDUCTION	actual deduction rule
STRING_CONCAT	string concat
STRING_IN_REGEXP	membership
STRING_LENGTH	string length
STRING_SUBSTR	string substr
CONST_STRING	a string of characters
CONST_REGEXP	a regular expression
STRING_TO_REGEXP	convert string to regexp
REGEXP_CONCAT	regexp concat
REGEXP_OR	regexp or
REGEXP_INTER	regexp intersection
REGEXP_STAR	regexp *
REGEXP_PLUS	regexp +
REGEXP_OPT	regexp ?
REGEXP_RANGE	regexp range
LAST_KIND	marks the upper-bound of this enumeration

Definition at line 60 of file kind.h.

Function Documentation

bool CVC4::kind::isAssociative ( ::CVC4::Kind  k )

inline

Returns true if the given kind is associative.

This is used by ExprManager to decide whether it's safe to modify big expressions by changing the grouping of the arguments.

Definition at line 453 of file kind.h.

References AND, MULT, OR, and PLUS.

std::string CVC4::kind::kindToString ( ::CVC4::Kind  k )

inline

Definition at line 466 of file kind.h.

std::ostream & CVC4::kind::operator<< ( std::ostream &  out, CVC4::Kind  k  )

inline

Definition at line 254 of file kind.h.

References ABS, ABSTRACT_VALUE, AND, APPLY, APPLY_CONSTRUCTOR, APPLY_SELECTOR, APPLY_TESTER, APPLY_TYPE_ASCRIPTION, APPLY_UF, ARR_TABLE_FUN, ARRAY_TYPE, ASCRIPTION_TYPE, BITVECTOR_AND, BITVECTOR_ASHR, BITVECTOR_BITOF, BITVECTOR_BITOF_OP, BITVECTOR_COMP, BITVECTOR_CONCAT, 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, EQUAL, EXISTS, FORALL, FUNCTION, FUNCTION_TYPE, GEQ, GT, IFF, IMPLIES, INST_CONSTANT, INST_PATTERN, INST_PATTERN_LIST, INT_TO_BITVECTOR, INT_TO_BITVECTOR_OP, INTS_DIVISION, INTS_DIVISION_TOTAL, INTS_MODULUS, INTS_MODULUS_TOTAL, IS_INTEGER, ITE, LAMBDA, LAST_KIND, LEQ, LT, 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_INTER, REGEXP_OPT, REGEXP_OR, REGEXP_PLUS, REGEXP_RANGE, REGEXP_STAR, REWRITE_RULE, RR_DEDUCTION, RR_REDUCTION, RR_REWRITE, SELECT, SELECTOR_TYPE, SEXPR, SEXPR_TYPE, SKOLEM, SORT_TAG, SORT_TYPE, STORE, STORE_ALL, STRING_CONCAT, STRING_IN_REGEXP, STRING_LENGTH, STRING_SUBSTR, STRING_TO_REGEXP, SUBRANGE_TYPE, 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, VARIABLE, and XOR.