CVC3::Theorem Member List

This is the complete list of members for CVC3::Theorem, including all inherited members.

clearAllFlags() constCVC3::Theorem
compare(const Theorem &t1, const Theorem &t2)CVC3::Theorem [friend]
compare(const Theorem &t1, const Expr &e2)CVC3::Theorem [friend]
compareByPtr(const Theorem &t1, const Theorem &t2)CVC3::Theorem [friend]
d_exprCVC3::Theorem [private]
d_thmCVC3::Theorem [private]
exprValue() constCVC3::Theorem [inline, private]
getAssumptionsRec(std::set< Expr > &assumptions) const CVC3::Theorem [private]
getAssumptionsRef() constCVC3::Theorem
getCachedValue() constCVC3::Theorem
getExpandFlag() constCVC3::Theorem
getExpr() constCVC3::Theorem
getLeafAssumptions(std::vector< Expr > &assumptions, bool negate=false) const CVC3::Theorem
getLHS() constCVC3::Theorem
getLitFlag() constCVC3::Theorem
getProof() constCVC3::Theorem
getQuantLevel() constCVC3::Theorem
getRHS() constCVC3::Theorem
getScope() constCVC3::Theorem
hash() constCVC3::Theorem
isAbsLiteral() constCVC3::Theorem
isAssump() constCVC3::Theorem
isFlagged() constCVC3::Theorem
isNull() constCVC3::Theorem [inline]
isRefl() constCVC3::Theorem [inline]
isRewrite() constCVC3::Theorem
matches(const Expr &e) const CVC3::Theorem [inline]
operator!=(const Theorem &t1, const Theorem &t2)CVC3::Theorem [friend]
operator<<(std::ostream &os, const Theorem &t)CVC3::Theorem [friend]
operator=(const Theorem &th)CVC3::Theorem
operator==(const Theorem &t1, const Theorem &t2)CVC3::Theorem [friend]
pprintx() constCVC3::Theorem
pprintxnodag() constCVC3::Theorem
print() constCVC3::Theorem
print(std::ostream &os, const std::string &name) const CVC3::Theorem
printDebug() constCVC3::Theorem [inline]
printx() constCVC3::Theorem
printxnodag() constCVC3::Theorem
proves(const Expr &e) const CVC3::Theorem [inline]
recursivePrint(int &i) const CVC3::Theorem [private]
refutes(const Expr &e) const CVC3::Theorem [inline]
RegTheoremValue classCVC3::Theorem [friend]
RWTheoremValue classCVC3::Theorem [friend]
setCachedValue(int value) const CVC3::Theorem
setExpandFlag(bool val) const CVC3::Theorem
setFlag() constCVC3::Theorem
setLitFlag(bool val) const CVC3::Theorem
setQuantLevel(unsigned level)CVC3::Theorem
Theorem(TheoremValue *thm)CVC3::Theorem [inline, private]
Theorem(TheoremManager *tm, const Expr &thm, const Assumptions &assump, const Proof &pf, bool isAssump=false, int scope=-1)CVC3::Theorem [private]
Theorem(TheoremManager *tm, const Expr &lhs, const Expr &rhs, const Assumptions &assump, const Proof &pf, bool isAssump=false, int scope=-1)CVC3::Theorem [private]
Theorem(const Expr &e)CVC3::Theorem [private]
Theorem()CVC3::Theorem [inline]
Theorem(const Theorem &th)CVC3::Theorem
Theorem3 classCVC3::Theorem [friend]
TheoremEq(const Theorem &t1, const Theorem &t2)CVC3::Theorem [inline, static]
TheoremProducer classCVC3::Theorem [friend]
thm() constCVC3::Theorem [inline, private]
toString() constCVC3::Theorem [inline]
withAssumptions() constCVC3::Theorem
withProof() constCVC3::Theorem
~Theorem()CVC3::Theorem

Generated on Tue Jul 3 14:37:38 2007 for CVC3 by  doxygen 1.5.1