cvc4-1.3
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

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.