CVC3  2.4.1
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::Theoremfriend
compare(const Theorem &t1, const Expr &e2)CVC3::Theoremfriend
compareByPtr(const Theorem &t1, const Theorem &t2)CVC3::Theoremfriend
d_exprCVC3::Theorem
d_thmCVC3::Theorem
exprValue() const CVC3::Theoreminlineprivate
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::Theoremprivate
getAssumptionsRec(std::set< Expr > &assumptions) const CVC3::Theoremprivate
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::Theoremprivate
getScope() const CVC3::Theorem
hash() const CVC3::Theorem
isAbsLiteral() const CVC3::Theorem
isAssump() const CVC3::Theorem
isFlagged() const CVC3::Theorem
isNull() const CVC3::Theoreminline
isRefl() const CVC3::Theoreminline
isRewrite() const CVC3::Theorem
isSubst() const CVC3::Theorem
matches(const Expr &e) const CVC3::Theoreminline
operator!=(const Theorem &t1, const Theorem &t2)CVC3::Theoremfriend
operator<<(std::ostream &os, const Theorem &t)CVC3::Theoremfriend
operator=(const Theorem &th)CVC3::Theorem
operator==(const Theorem &t1, const Theorem &t2)CVC3::Theoremfriend
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::Theoreminline
printx() const CVC3::Theorem
printxnodag() const CVC3::Theorem
proves(const Expr &e) const CVC3::Theoreminline
recursivePrint(int &i) const CVC3::Theoremprivate
refutes(const Expr &e) const CVC3::Theoreminline
RegTheoremValue classCVC3::Theoremfriend
RWTheoremValue classCVC3::Theoremfriend
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::Theoreminlineprivate
Theorem(TheoremManager *tm, const Expr &thm, const Assumptions &assump, const Proof &pf, bool isAssump=false, int scope=-1)CVC3::Theoremprivate
Theorem(TheoremManager *tm, const Expr &lhs, const Expr &rhs, const Assumptions &assump, const Proof &pf, bool isAssump=false, int scope=-1)CVC3::Theoremprivate
Theorem(const Expr &e)CVC3::Theoremprivate
Theorem()CVC3::Theoreminline
Theorem(const Theorem &th)CVC3::Theorem
Theorem3 classCVC3::Theoremfriend
TheoremEq(const Theorem &t1, const Theorem &t2)CVC3::Theoreminlinestatic
TheoremProducer classCVC3::Theoremfriend
thm() const CVC3::Theoreminlineprivate
toString() const CVC3::Theoreminline
withAssumptions() const CVC3::Theorem
withProof() const CVC3::Theorem
~Theorem()CVC3::Theorem