CVCL::Theorem Member List

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

clearAllFlags() const	CVCL::Theorem
compare(const Theorem &t1, const Theorem &t2)	CVCL::Theorem	[friend]
compare(const Theorem &t1, const Expr &e2)	CVCL::Theorem	[friend]
compareByPtr(const Theorem &t1, const Theorem &t2)	CVCL::Theorem	[friend]
d_thm	CVCL::Theorem	[private]
getAssumptions() const	CVCL::Theorem
getAssumptionsCopy() const	CVCL::Theorem
getAssumptionsRec(std::set< Expr > &assumptions) const	CVCL::Theorem	[private]
getAssumptionsRef() const	CVCL::Theorem
getCachedValue() const	CVCL::Theorem
getExpandFlag() const	CVCL::Theorem
getExpr() const	CVCL::Theorem
getLeafAssumptions(std::vector< Expr > &assumptions, bool negate=false) const	CVCL::Theorem
getLHS() const	CVCL::Theorem
getLitFlag() const	CVCL::Theorem
getProof() const	CVCL::Theorem
getRHS() const	CVCL::Theorem
getScope() const	CVCL::Theorem
isAbsLiteral() const	CVCL::Theorem
isAssump() const	CVCL::Theorem
isFlagged() const	CVCL::Theorem
isNull() const	CVCL::Theorem	[inline]
isRewrite() const	CVCL::Theorem
matches(const Expr &e) const	CVCL::Theorem	[inline]
operator!=(const Theorem &t1, const Theorem &t2)	CVCL::Theorem	[friend]
operator<<(std::ostream &os, const Theorem &t)	CVCL::Theorem	[friend]
operator=(const Theorem &th)	CVCL::Theorem
operator==(const Theorem &t1, const Theorem &t2)	CVCL::Theorem	[friend]
print() const	CVCL::Theorem
print(std::ostream &os, const std::string &name) const	CVCL::Theorem
printDebug() const	CVCL::Theorem	[inline]
printx() const	CVCL::Theorem
proves(const Expr &e) const	CVCL::Theorem	[inline]
recursivePrint(int &i) const	CVCL::Theorem	[private]
refutes(const Expr &e) const	CVCL::Theorem	[inline]
setCachedValue(int value) const	CVCL::Theorem
setExpandFlag(bool val) const	CVCL::Theorem
setFlag() const	CVCL::Theorem
setLitFlag(bool val) const	CVCL::Theorem
Theorem(TheoremManager *tm, const Expr &thm, const Assumptions &assump, const Proof &pf, bool isAssump=false, int scope=-1)	CVCL::Theorem	[private]
Theorem(TheoremManager *tm, const Expr &lhs, const Expr &rhs, const Assumptions &assump, const Proof &pf, bool isAssump=false, int scope=-1)	CVCL::Theorem	[private]
Theorem(TheoremManager *tm, const Expr &e, const Proof &pf)	CVCL::Theorem	[private]
Theorem()	CVCL::Theorem	[inline]
Theorem(const Theorem &th)	CVCL::Theorem
Theorem3 class	CVCL::Theorem	[friend]
TheoremProducer class	CVCL::Theorem	[friend]
toString() const	CVCL::Theorem	[inline]
withAssumptions() const	CVCL::Theorem
withProof() const	CVCL::Theorem
~Theorem()	CVCL::Theorem	[virtual]

---