cvc4-1.4
|
Enumerations | |
enum | TheoryId { THEORY_BUILTIN, THEORY_BOOL, THEORY_UF, THEORY_ARITH, THEORY_BV, THEORY_ARRAY, THEORY_DATATYPES, THEORY_SETS, THEORY_STRINGS, THEORY_QUANTIFIERS, THEORY_LAST } |
enum | TheoryOfMode { THEORY_OF_TYPE_BASED, THEORY_OF_TERM_BASED } |
How do we associate theories with the terms. More... | |
Functions | |
TheoryId & | operator++ (TheoryId &id) |
std::ostream & | operator<< (std::ostream &out, TheoryId theoryId) |
TheoryId | kindToTheoryId (::CVC4::Kind k) |
TheoryId | typeConstantToTheoryId (::CVC4::TypeConstant typeConstant) |
std::ostream & | operator<< (std::ostream &out, TheoryOfMode m) throw () |
Variables | |
const TheoryId | THEORY_FIRST |
const TheoryId | THEORY_SAT_SOLVER |
How do we associate theories with the terms.
Definition at line 25 of file theoryof_mode.h.
|
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.
Definition at line 610 of file kind.h.
Referenced by CVC4::Expr::const_iterator::operator!=().
|
inline |
Definition at line 34 of file theoryof_mode.h.
References CVC4::options::out, THEORY_OF_TERM_BASED, and THEORY_OF_TYPE_BASED.
|
inline |
Definition at line 614 of file kind.h.
References CVC4::options::out, THEORY_ARITH, THEORY_ARRAY, THEORY_BOOL, THEORY_BUILTIN, THEORY_BV, THEORY_DATATYPES, THEORY_QUANTIFIERS, THEORY_SETS, THEORY_STRINGS, and THEORY_UF.
|
inline |
Definition at line 833 of file kind.h.
References CVC4::BOOLEAN_TYPE, CVC4::BOUND_VAR_LIST_TYPE, CVC4::BUILTIN_OPERATOR_TYPE, CVC4::INST_PATTERN_LIST_TYPE, CVC4::INST_PATTERN_TYPE, CVC4::INTEGER_TYPE, CVC4::LAST_TYPE, CVC4::REAL_TYPE, CVC4::REGEXP_TYPE, CVC4::RRHB_TYPE, CVC4::STRING_TYPE, THEORY_ARITH, THEORY_BOOL, THEORY_BUILTIN, THEORY_QUANTIFIERS, and THEORY_STRINGS.
const TheoryId CVC4::theory::THEORY_FIRST |
Definition at line 607 of file kind.h.
Referenced by CVC4::LogicInfo::operator<=(), CVC4::LogicInfo::operator==(), and CVC4::LogicInfo::operator>=().