cvc4-1.4
CVC4::theory Namespace Reference

Enumerations

enum  TheoryOfMode { THEORY_OF_TYPE_BASED, THEORY_OF_TERM_BASED }
 How do we associate theories with the terms. More...
 
enum  TheoryId {
  THEORY_BUILTIN, THEORY_BOOL, THEORY_UF, THEORY_ARITH,
  THEORY_BV, THEORY_ARRAY, THEORY_DATATYPES, THEORY_SETS,
  THEORY_STRINGS, THEORY_QUANTIFIERS, THEORY_LAST
}
 

Functions

std::ostream & operator<< (std::ostream &out, TheoryOfMode m) throw ()
 
TheoryIdoperator++ (TheoryId &id)
 
std::ostream & operator<< (std::ostream &out, TheoryId theoryId)
 
TheoryId kindToTheoryId (::CVC4::Kind k)
 
TheoryId typeConstantToTheoryId (::CVC4::TypeConstant typeConstant)
 

Variables

const TheoryId THEORY_FIRST
 
const TheoryId THEORY_SAT_SOLVER
 

Enumeration Type Documentation

◆ TheoryId

Enumerator
THEORY_BUILTIN 
THEORY_BOOL 
THEORY_UF 
THEORY_ARITH 
THEORY_BV 
THEORY_ARRAY 
THEORY_DATATYPES 
THEORY_SETS 
THEORY_STRINGS 
THEORY_QUANTIFIERS 
THEORY_LAST 

Definition at line 591 of file kind.h.

◆ TheoryOfMode

How do we associate theories with the terms.

Enumerator
THEORY_OF_TYPE_BASED 

Equality, variables and constants are associated with the types.

THEORY_OF_TERM_BASED 

Variables are uninterpreted, constants are with the type, equalities prefer parametric.

Definition at line 25 of file theoryof_mode.h.

Function Documentation

◆ kindToTheoryId()

TheoryId CVC4::theory::kindToTheoryId ( ::CVC4::Kind  k)
inline

Definition at line 635 of file kind.h.

References CVC4::kind::ABS, CVC4::kind::ABSTRACT_VALUE, CVC4::kind::AND, CVC4::kind::APPLY, CVC4::kind::APPLY_CONSTRUCTOR, CVC4::kind::APPLY_SELECTOR, CVC4::kind::APPLY_SELECTOR_TOTAL, CVC4::kind::APPLY_TESTER, CVC4::kind::APPLY_TYPE_ASCRIPTION, CVC4::kind::APPLY_UF, CVC4::kind::ARR_TABLE_FUN, CVC4::kind::ARRAY_LAMBDA, CVC4::kind::ARRAY_TYPE, CVC4::kind::ASCRIPTION_TYPE, CVC4::kind::BITVECTOR_ACKERMANIZE_UDIV, CVC4::kind::BITVECTOR_ACKERMANIZE_UREM, CVC4::kind::BITVECTOR_AND, CVC4::kind::BITVECTOR_ASHR, CVC4::kind::BITVECTOR_BITOF, CVC4::kind::BITVECTOR_BITOF_OP, CVC4::kind::BITVECTOR_COMP, CVC4::kind::BITVECTOR_CONCAT, CVC4::kind::BITVECTOR_EAGER_ATOM, CVC4::kind::BITVECTOR_EXTRACT, CVC4::kind::BITVECTOR_EXTRACT_OP, CVC4::kind::BITVECTOR_LSHR, CVC4::kind::BITVECTOR_MULT, CVC4::kind::BITVECTOR_NAND, CVC4::kind::BITVECTOR_NEG, CVC4::kind::BITVECTOR_NOR, CVC4::kind::BITVECTOR_NOT, CVC4::kind::BITVECTOR_OR, CVC4::kind::BITVECTOR_PLUS, CVC4::kind::BITVECTOR_REPEAT, CVC4::kind::BITVECTOR_REPEAT_OP, CVC4::kind::BITVECTOR_ROTATE_LEFT, CVC4::kind::BITVECTOR_ROTATE_LEFT_OP, CVC4::kind::BITVECTOR_ROTATE_RIGHT, CVC4::kind::BITVECTOR_ROTATE_RIGHT_OP, CVC4::kind::BITVECTOR_SDIV, CVC4::kind::BITVECTOR_SGE, CVC4::kind::BITVECTOR_SGT, CVC4::kind::BITVECTOR_SHL, CVC4::kind::BITVECTOR_SIGN_EXTEND, CVC4::kind::BITVECTOR_SIGN_EXTEND_OP, CVC4::kind::BITVECTOR_SLE, CVC4::kind::BITVECTOR_SLT, CVC4::kind::BITVECTOR_SMOD, CVC4::kind::BITVECTOR_SREM, CVC4::kind::BITVECTOR_SUB, CVC4::kind::BITVECTOR_TO_NAT, CVC4::kind::BITVECTOR_TYPE, CVC4::kind::BITVECTOR_UDIV, CVC4::kind::BITVECTOR_UDIV_TOTAL, CVC4::kind::BITVECTOR_UGE, CVC4::kind::BITVECTOR_UGT, CVC4::kind::BITVECTOR_ULE, CVC4::kind::BITVECTOR_ULT, CVC4::kind::BITVECTOR_UREM, CVC4::kind::BITVECTOR_UREM_TOTAL, CVC4::kind::BITVECTOR_XNOR, CVC4::kind::BITVECTOR_XOR, CVC4::kind::BITVECTOR_ZERO_EXTEND, CVC4::kind::BITVECTOR_ZERO_EXTEND_OP, CVC4::kind::BOUND_VAR_LIST, CVC4::kind::BOUND_VARIABLE, CVC4::kind::BUILTIN, CVC4::kind::CARDINALITY_CONSTRAINT, CVC4::kind::CHAIN, CVC4::kind::CHAIN_OP, CVC4::kind::COMBINED_CARDINALITY_CONSTRAINT, CVC4::kind::CONST_BITVECTOR, CVC4::kind::CONST_BOOLEAN, CVC4::kind::CONST_RATIONAL, CVC4::kind::CONST_REGEXP, CVC4::kind::CONST_STRING, CVC4::kind::CONSTRUCTOR_TYPE, CVC4::kind::DATATYPE_TYPE, CVC4::kind::DISTINCT, CVC4::kind::DIVISIBLE, CVC4::kind::DIVISIBLE_OP, CVC4::kind::DIVISION, CVC4::kind::DIVISION_TOTAL, CVC4::kind::EMPTYSET, CVC4::kind::EQUAL, CVC4::kind::EXISTS, CVC4::kind::FORALL, CVC4::kind::FUNCTION, CVC4::kind::FUNCTION_TYPE, CVC4::kind::GEQ, CVC4::kind::GT, CVC4::kind::IFF, CVC4::kind::IMPLIES, CVC4::kind::INSERT, CVC4::kind::INST_CONSTANT, CVC4::kind::INST_PATTERN, CVC4::kind::INST_PATTERN_LIST, CVC4::kind::INT_TO_BITVECTOR, CVC4::kind::INT_TO_BITVECTOR_OP, CVC4::kind::INTERSECTION, CVC4::kind::INTS_DIVISION, CVC4::kind::INTS_DIVISION_TOTAL, CVC4::kind::INTS_MODULUS, CVC4::kind::INTS_MODULUS_TOTAL, CVC4::kind::IS_INTEGER, CVC4::kind::ITE, CVC4::kind::LAMBDA, CVC4::kind::LAST_KIND, CVC4::kind::LEQ, CVC4::kind::LT, CVC4::kind::MEMBER, CVC4::kind::MINUS, CVC4::kind::MULT, CVC4::kind::NOT, CVC4::kind::NULL_EXPR, CVC4::kind::OR, CVC4::kind::PARAMETRIC_DATATYPE, CVC4::kind::PLUS, CVC4::kind::POW, CVC4::kind::RECORD, CVC4::kind::RECORD_SELECT, CVC4::kind::RECORD_SELECT_OP, CVC4::kind::RECORD_TYPE, CVC4::kind::RECORD_UPDATE, CVC4::kind::RECORD_UPDATE_OP, CVC4::kind::REGEXP_CONCAT, CVC4::kind::REGEXP_EMPTY, CVC4::kind::REGEXP_INTER, CVC4::kind::REGEXP_LOOP, CVC4::kind::REGEXP_OPT, CVC4::kind::REGEXP_PLUS, CVC4::kind::REGEXP_RANGE, CVC4::kind::REGEXP_SIGMA, CVC4::kind::REGEXP_STAR, CVC4::kind::REGEXP_UNION, CVC4::kind::REWRITE_RULE, CVC4::kind::RR_DEDUCTION, CVC4::kind::RR_REDUCTION, CVC4::kind::RR_REWRITE, CVC4::kind::SELECT, CVC4::kind::SELECTOR_TYPE, CVC4::kind::SET_TYPE, CVC4::kind::SETMINUS, CVC4::kind::SEXPR, CVC4::kind::SEXPR_TYPE, CVC4::kind::SINGLETON, CVC4::kind::SKOLEM, CVC4::kind::SORT_TAG, CVC4::kind::SORT_TYPE, CVC4::kind::STORE, CVC4::kind::STORE_ALL, CVC4::kind::STRING_CHARAT, CVC4::kind::STRING_CONCAT, CVC4::kind::STRING_IN_REGEXP, CVC4::kind::STRING_ITOS, CVC4::kind::STRING_LENGTH, CVC4::kind::STRING_PREFIX, CVC4::kind::STRING_STOI, CVC4::kind::STRING_STOU16, CVC4::kind::STRING_STOU32, CVC4::kind::STRING_STRCTN, CVC4::kind::STRING_STRIDOF, CVC4::kind::STRING_STRREPL, CVC4::kind::STRING_SUBSTR, CVC4::kind::STRING_SUBSTR_TOTAL, CVC4::kind::STRING_SUFFIX, CVC4::kind::STRING_TO_REGEXP, CVC4::kind::STRING_U16TOS, CVC4::kind::STRING_U32TOS, CVC4::kind::SUBRANGE_TYPE, CVC4::kind::SUBSET, CVC4::kind::SUBTYPE_TYPE, CVC4::kind::TESTER_TYPE, THEORY_ARITH, THEORY_ARRAY, THEORY_BOOL, THEORY_BUILTIN, THEORY_BV, THEORY_DATATYPES, THEORY_QUANTIFIERS, THEORY_SETS, THEORY_STRINGS, THEORY_UF, CVC4::kind::TO_INTEGER, CVC4::kind::TO_REAL, CVC4::kind::TUPLE, CVC4::kind::TUPLE_SELECT, CVC4::kind::TUPLE_SELECT_OP, CVC4::kind::TUPLE_TYPE, CVC4::kind::TUPLE_UPDATE, CVC4::kind::TUPLE_UPDATE_OP, CVC4::kind::TYPE_CONSTANT, CVC4::kind::UMINUS, CVC4::kind::UNDEFINED_KIND, CVC4::kind::UNINTERPRETED_CONSTANT, CVC4::kind::UNION, CVC4::kind::VARIABLE, and CVC4::kind::XOR.

◆ operator++()

TheoryId& CVC4::theory::operator++ ( TheoryId id)
inline

Definition at line 610 of file kind.h.

Referenced by CVC4::Expr::const_iterator::operator!=().

◆ operator<<() [1/2]

std::ostream & CVC4::theory::operator<< ( std::ostream &  out,
TheoryOfMode  m 
)
throw (
)
inline

Definition at line 34 of file theoryof_mode.h.

References CVC4::options::out, THEORY_OF_TERM_BASED, and THEORY_OF_TYPE_BASED.

◆ operator<<() [2/2]

std::ostream& CVC4::theory::operator<< ( std::ostream &  out,
TheoryId  theoryId 
)
inline

◆ typeConstantToTheoryId()

Variable Documentation

◆ THEORY_FIRST

const TheoryId CVC4::theory::THEORY_FIRST

◆ THEORY_SAT_SOLVER

const TheoryId CVC4::theory::THEORY_SAT_SOLVER

Definition at line 608 of file kind.h.