CVC3::Theorem Member List

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

clearAllFlags() const CVC3::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
d_thmCVC3::Theorem
exprValue() const CVC3::Theorem [inline, private]
getAssumptionsAndCong(std::vector< Expr > &assumptions, std::vector< Expr > &congruences, bool negate=false) const CVC3::Theorem
getAssumptionsAndCongRec(std::set< Expr > &assumptions, std::vector< Expr > &congruences) const CVC3::Theorem [private]
getAssumptionsRec(std::set< Expr > &assumptions) const CVC3::Theorem [private]
getAssumptionsRef() const CVC3::Theorem
getCachedValue() const CVC3::Theorem
getExpandFlag() const CVC3::Theorem
getExpr() const CVC3::Theorem
getLeafAssumptions(std::vector< Expr > &assumptions, bool negate=false) const CVC3::Theorem
getLHS() const CVC3::Theorem
getLitFlag() const CVC3::Theorem
getProof() const CVC3::Theorem
getQuantLevel() const CVC3::Theorem
getQuantLevelDebug() const CVC3::Theorem
getRHS() const CVC3::Theorem
GetSatAssumptions(std::vector< Theorem > &assumptions) const CVC3::Theorem
GetSatAssumptionsRec(std::vector< Theorem > &assumptions) const CVC3::Theorem [private]
getScope() const CVC3::Theorem
hash() const CVC3::Theorem
isAbsLiteral() const CVC3::Theorem
isAssump() const CVC3::Theorem
isFlagged() const CVC3::Theorem
isNull() const CVC3::Theorem [inline]
isRefl() const CVC3::Theorem [inline]
isRewrite() const CVC3::Theorem
isSubst() const CVC3::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() const CVC3::Theorem
pprintxnodag() const CVC3::Theorem
print() const CVC3::Theorem
print(std::ostream &os, const std::string &name) const CVC3::Theorem
printDebug() const CVC3::Theorem [inline]
printx() const CVC3::Theorem
printxnodag() const CVC3::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() const CVC3::Theorem
setLitFlag(bool val) const CVC3::Theorem
setQuantLevel(unsigned level)CVC3::Theorem
setSubst() const 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() const CVC3::Theorem [inline, private]
toString() const CVC3::Theorem [inline]
withAssumptions() const CVC3::Theorem
withProof() const CVC3::Theorem
~Theorem()CVC3::Theorem


Generated on Thu Oct 15 22:20:31 2009 for CVC3 by  doxygen 1.5.8