CVC3
2.4.1
|
This is the complete list of members for CVC3::TheoryRecords, including all inherited members.
addBoundVar(const std::string &name, const Type &type) | CVC3::Theory | |
addBoundVar(const std::string &name, const Type &type, const Expr &def) | CVC3::Theory | |
addGlobalLemma(const Theorem &thm, int priority=0) | CVC3::Theory | |
addSharedTerm(const Expr &e) | CVC3::Theory | inlinevirtual |
addSplitter(const Expr &e, int priority=0) | CVC3::Theory | |
assertEqualities(const Theorem &e) | CVC3::Theory | virtual |
assertFact(const Theorem &e) | CVC3::TheoryRecords | virtual |
assertTypePred(const Expr &e, const Theorem &pred) | CVC3::Theory | inlinevirtual |
assignValue(const Expr &t, const Expr &val) | CVC3::Theory | virtual |
assignValue(const Theorem &thm) | CVC3::Theory | virtual |
boolType() | CVC3::Theory | inline |
checkAssertEqInvariant(const Theorem &e) | CVC3::Theory | inlinevirtual |
checkSat(bool fullEffort) | CVC3::TheoryRecords | inlinevirtual |
checkType(const Expr &e) | CVC3::TheoryRecords | virtual |
computeBaseType(const Type &t) | CVC3::TheoryRecords | virtual |
computeModel(const Expr &e, std::vector< Expr > &vars) | CVC3::TheoryRecords | virtual |
computeModelBasic(const std::vector< Expr > &v) | CVC3::Theory | inlinevirtual |
computeModelTerm(const Expr &e, std::vector< Expr > &v) | CVC3::TheoryRecords | virtual |
computeTCC(const Expr &e) | CVC3::TheoryRecords | virtual |
computeType(const Expr &e) | CVC3::TheoryRecords | virtual |
computeTypePred(const Type &t, const Expr &e) | CVC3::TheoryRecords | virtual |
createProofRules() | CVC3::TheoryRecords | |
d_rules | CVC3::TheoryRecords | private |
d_theoryUsed | CVC3::Theory | protected |
enqueueFact(const Theorem &e) | CVC3::Theory | virtual |
enqueueSE(const Theorem &e) | CVC3::Theory | virtual |
falseExpr() | CVC3::Theory | inline |
find(const Expr &e) | CVC3::Theory | |
findExpr(const Expr &e) | CVC3::Theory | inline |
findReduce(const Expr &e) | CVC3::Theory | |
findReduced(const Expr &e) | CVC3::Theory | |
findRef(const Expr &e) | CVC3::Theory | |
finiteTypeInfo(Expr &e, Unsigned &n, bool enumerate, bool computeSize) | CVC3::TheoryRecords | virtual |
getBaseType(const Expr &e) | CVC3::Theory | |
getBaseType(const Type &tp) | CVC3::Theory | |
getCommonRules() | CVC3::Theory | inline |
getEM() | CVC3::Theory | inline |
getField(const Expr &e, int i) | CVC3::TheoryRecords | |
getField(const Expr &e) | CVC3::TheoryRecords | |
getFieldIndex(const Expr &e, const std::string &field) | CVC3::TheoryRecords | |
getFields(const Expr &r) | CVC3::TheoryRecords | |
getIndex(const Expr &e) | CVC3::TheoryRecords | |
getModelTerm(const Expr &e, std::vector< Expr > &v) | CVC3::Theory | |
getModelValue(const Expr &e) | CVC3::Theory | |
getName() const | CVC3::Theory | inline |
getNumTheories() | CVC3::Theory | |
getTCC(const Expr &e) | CVC3::Theory | |
getTypePred(const Type &t, const Expr &e) | CVC3::Theory | |
hasTheory(int kind) | CVC3::Theory | |
iffMP(const Theorem &e1, const Theorem &e1_iff_e2) | CVC3::Theory | inline |
inconsistent() | CVC3::Theory | virtual |
installID(const std::string &name, const Expr &e) | CVC3::Theory | |
isLeaf(const Expr &e) | CVC3::Theory | inline |
isLeafIn(const Expr &e1, const Expr &e2) | CVC3::Theory | |
isRecord(const Expr &e) | CVC3::TheoryRecords | inline |
isRecordAccess(const Expr &e) | CVC3::TheoryRecords | inline |
isRecordType(const Expr &e) | CVC3::TheoryRecords | inline |
isRecordType(const Type &t) | CVC3::TheoryRecords | inline |
isTuple(const Expr &e) | CVC3::TheoryRecords | inline |
isTupleAccess(const Expr &e) | CVC3::TheoryRecords | inline |
isTupleType(const Expr &e) | CVC3::TheoryRecords | inline |
isTupleType(const Type &tp) | CVC3::TheoryRecords | inline |
leavesAreSimp(const Expr &e) | CVC3::Theory | |
lookupFunction(const std::string &name, Type *type) | CVC3::Theory | |
lookupTypeExpr(const std::string &name) | CVC3::Theory | |
lookupVar(const std::string &name, Type *type) | CVC3::Theory | |
newFunction(const std::string &name, const Type &type, bool computeTransClosure) | CVC3::Theory | |
newFunction(const std::string &name, const Type &type, const Expr &def) | CVC3::Theory | |
newSubtypeExpr(const Expr &pred, const Expr &witness) | CVC3::Theory | |
newTypeExpr(const std::string &name) | CVC3::Theory | |
newTypeExpr(const std::string &name, const Type &def) | CVC3::Theory | |
newVar(const std::string &name, const Type &type) | CVC3::Theory | |
newVar(const std::string &name, const Type &type, const Expr &def) | CVC3::Theory | |
notifyInconsistent(const Theorem &thm) | CVC3::Theory | inlinevirtual |
parseExpr(const Expr &e) | CVC3::Theory | virtual |
parseExprOp(const Expr &e) | CVC3::TheoryRecords | virtual |
print(ExprStream &os, const Expr &e) | CVC3::TheoryRecords | virtual |
recordExpr(const std::vector< std::string > &fields, const std::vector< Expr > &kids) | CVC3::TheoryRecords | |
recordExpr(const std::vector< Expr > &fields, const std::vector< Expr > &kids) | CVC3::TheoryRecords | |
recordSelect(const Expr &r, const std::string &field) | CVC3::TheoryRecords | |
recordType(const std::vector< std::string > &fields, const std::vector< Type > &types) | CVC3::TheoryRecords | |
recordType(const std::vector< std::string > &fields, const std::vector< Expr > &types) | CVC3::TheoryRecords | |
recordType(const std::vector< Expr > &fields, const std::vector< Expr > &types) | CVC3::TheoryRecords | |
recordUpdate(const Expr &r, const std::string &field, const Expr &val) | CVC3::TheoryRecords | |
refineCounterExample() | CVC3::Theory | inlinevirtual |
reflexivityRule(const Expr &a) | CVC3::Theory | inline |
registerAtom(const Expr &e, const Theorem &thm) | CVC3::Theory | virtual |
registerAtom(const Expr &e) | CVC3::Theory | inlinevirtual |
registerKinds(Theory *theory, std::vector< int > &kinds) | CVC3::Theory | |
registerTheory(Theory *theory, std::vector< int > &kinds, bool hasSolver=false) | CVC3::Theory | |
renameExpr(const Expr &e) | CVC3::Theory | |
resolveID(const std::string &name) | CVC3::Theory | |
rewrite(const Expr &e) | CVC3::TheoryRecords | virtual |
rewriteAnd(const Expr &e) | CVC3::Theory | inline |
rewriteAtomic(const Expr &e) | CVC3::Theory | inlinevirtual |
rewriteAux(const Expr &e) | CVC3::TheoryRecords | private |
rewriteAux(const Theorem &thm) | CVC3::TheoryRecords | private |
rewriteCC(const Expr &e) | CVC3::Theory | |
rewriteIte(const Expr &e) | CVC3::Theory | |
rewriteOr(const Expr &e) | CVC3::Theory | inline |
setIncomplete(const std::string &reason) | CVC3::Theory | virtual |
setInconsistent(const Theorem &e) | CVC3::Theory | virtual |
setup(const Expr &e) | CVC3::TheoryRecords | virtual |
setupCC(const Expr &e) | CVC3::Theory | |
setUsed() | CVC3::Theory | inlinevirtual |
simplify(const Expr &e) | CVC3::Theory | virtual |
simplifyExpr(const Expr &e) | CVC3::Theory | inline |
simplifyOp(const Expr &e) | CVC3::Theory | virtual |
solve(const Theorem &e) | CVC3::Theory | inlinevirtual |
substitutivityRule(const Op &op, const std::vector< Theorem > &thms) | CVC3::Theory | inline |
substitutivityRule(const Expr &e, const Theorem &t) | CVC3::Theory | inline |
substitutivityRule(const Expr &e, const Theorem &t1, const Theorem &t2) | CVC3::Theory | inline |
substitutivityRule(const Expr &e, const std::vector< unsigned > &changed, const std::vector< Theorem > &thms) | CVC3::Theory | inline |
substitutivityRule(const Expr &e, int changed, const Theorem &thm) | CVC3::Theory | inline |
symmetryRule(const Theorem &a1_eq_a2) | CVC3::Theory | inline |
Theory(TheoryCore *theoryCore, const std::string &name) | CVC3::Theory | |
theoryCore() | CVC3::Theory | inline |
theoryOf(int kind) | CVC3::Theory | |
theoryOf(const Type &e) | CVC3::Theory | |
theoryOf(const Expr &e) | CVC3::Theory | |
theoryPreprocess(const Expr &e) | CVC3::Theory | inlinevirtual |
TheoryRecords(TheoryCore *core) | CVC3::TheoryRecords | |
theoryUsed() | CVC3::Theory | inlinevirtual |
transitivityRule(const Theorem &a1_eq_a2, const Theorem &a2_eq_a3) | CVC3::Theory | inline |
trueExpr() | CVC3::Theory | inline |
tupleExpr(const std::vector< Expr > &kids) | CVC3::TheoryRecords | |
tupleSelect(const Expr &tup, int i) | CVC3::TheoryRecords | |
tupleType(const std::vector< Type > &types) | CVC3::TheoryRecords | |
tupleType(const std::vector< Expr > &types) | CVC3::TheoryRecords | |
tupleUpdate(const Expr &tup, int i, const Expr &val) | CVC3::TheoryRecords | |
typePred(const Expr &e) | CVC3::Theory | |
unregisterKinds(Theory *theory, std::vector< int > &kinds) | CVC3::Theory | |
unregisterTheory(Theory *theory, std::vector< int > &kinds, bool hasSolver) | CVC3::Theory | |
update(const Theorem &e, const Expr &d) | CVC3::TheoryRecords | virtual |
updateCC(const Theorem &e, const Expr &d) | CVC3::Theory | |
updateHelper(const Expr &e) | CVC3::Theory | |
~Theory(void) | CVC3::Theory | virtual |
~TheoryRecords() | CVC3::TheoryRecords |