CVC3
2.4.1
|
This is the complete list of members for CVC3::TheoryArray, 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::TheoryArray | virtual |
addSplitter(const Expr &e, int priority=0) | CVC3::Theory | |
assertEqualities(const Theorem &e) | CVC3::Theory | virtual |
assertFact(const Theorem &e) | CVC3::TheoryArray | 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::TheoryArray | virtual |
checkType(const Expr &e) | CVC3::TheoryArray | virtual |
computeBaseType(const Type &t) | CVC3::TheoryArray | virtual |
computeModel(const Expr &e, std::vector< Expr > &vars) | CVC3::TheoryArray | virtual |
computeModelBasic(const std::vector< Expr > &v) | CVC3::Theory | inlinevirtual |
computeModelTerm(const Expr &e, std::vector< Expr > &v) | CVC3::TheoryArray | virtual |
computeTCC(const Expr &e) | CVC3::TheoryArray | virtual |
computeType(const Expr &e) | CVC3::TheoryArray | virtual |
computeTypePred(const Type &t, const Expr &e) | CVC3::Theory | inlinevirtual |
createProofRules() | CVC3::TheoryArray | |
d_applicationsInModel | CVC3::TheoryArray | private |
d_inCheckSat | CVC3::TheoryArray | private |
d_index | CVC3::TheoryArray | private |
d_liftReadIte | CVC3::TheoryArray | private |
d_reads | CVC3::TheoryArray | private |
d_renameThms | CVC3::TheoryArray | private |
d_rules | CVC3::TheoryArray | private |
d_sharedIdx1 | CVC3::TheoryArray | private |
d_sharedIdx2 | CVC3::TheoryArray | private |
d_sharedSubterms | CVC3::TheoryArray | private |
d_sharedSubtermsList | CVC3::TheoryArray | 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::TheoryArray | virtual |
getBaseArray(const Expr &e) const | CVC3::TheoryArray | |
getBaseType(const Expr &e) | CVC3::Theory | |
getBaseType(const Type &tp) | CVC3::Theory | |
getCommonRules() | CVC3::Theory | inline |
getEM() | CVC3::Theory | inline |
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 | |
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::TheoryArray | virtual |
print(ExprStream &os, const Expr &e) | CVC3::TheoryArray | virtual |
pullIndex(const Expr &e, const Expr &index) | CVC3::TheoryArray | private |
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::TheoryArray | virtual |
rewriteAnd(const Expr &e) | CVC3::Theory | inline |
rewriteAtomic(const Expr &e) | CVC3::Theory | inlinevirtual |
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::TheoryArray | 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::TheoryArray | virtual |
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 | |
TheoryArray(TheoryCore *core) | CVC3::TheoryArray | |
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 |
theoryUsed() | CVC3::Theory | inlinevirtual |
transitivityRule(const Theorem &a1_eq_a2, const Theorem &a2_eq_a3) | CVC3::Theory | inline |
trueExpr() | CVC3::Theory | inline |
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::TheoryArray | virtual |
updateCC(const Theorem &e, const Expr &d) | CVC3::Theory | |
updateHelper(const Expr &e) | CVC3::Theory | |
~Theory(void) | CVC3::Theory | virtual |
~TheoryArray() | CVC3::TheoryArray |