CVC3  2.4.1
Public Member Functions | Protected Attributes | Private Member Functions | Friends | List of all members
CVC3::TheoremValue Class Referenceabstract

#include <theorem_value.h>

Inheritance diagram for CVC3::TheoremValue:
CVC3::RegTheoremValue CVC3::RWTheoremValue

Public Member Functions

virtual ~TheoremValue ()
 
std::string toString () const
 
virtual MemoryManagergetMM ()=0
 

Protected Attributes

TheoremManagerd_tm
 Theorem Manager. More...
 
Expr d_thm
 The expression representing a theorem. More...
 
Proof d_proof
 Proof of the theorem. More...
 
unsigned d_refcount
 How many pointers to this theorem value. More...
 
int d_scopeLevel
 Largest scope level of the assumptions. More...
 
unsigned d_quantLevel
 Quantification level of this theorem. More...
 
unsigned d_flag
 debug quantlevel, this one is from proof, not from assumption list More...
 
int d_cachedValue: 28
 Temporary cache used during traversals. More...
 
bool d_isSubst: 1
 whether this theorem was generated by substitution More...
 
bool d_isAssump: 1
 
bool d_expand: 1
 whether it should this be expanded in graph traversal More...
 
bool d_clauselit: 1
 whether it belongs to the conflict clause More...
 

Private Member Functions

 TheoremValue (TheoremManager *tm, const Expr &thm, const Proof &pf, bool isAssump)
 
 TheoremValue (const TheoremValue &t)
 
TheoremValueoperator= (const TheoremValue &t)
 
bool isFlagged () const
 
void clearAllFlags ()
 
void setFlag ()
 
void setCachedValue (int value)
 
int getCachedValue () const
 
void setSubst ()
 
bool isSubst ()
 
void setExpandFlag (bool val)
 
bool getExpandFlag ()
 
void setLitFlag (bool val)
 
bool getLitFlag ()
 
int getScope ()
 
unsigned getQuantLevel ()
 
unsigned getQuantLevelDebug ()
 
void setQuantLevel (unsigned level)
 
unsigned recQuantLevel (Expr proof)
 
unsigned findQuantLevelDebug ()
 
virtual bool isRewrite () const
 
virtual const ExprgetExpr () const
 
virtual const ExprgetLHS () const
 
virtual const ExprgetRHS () const
 
virtual const AssumptionsgetAssumptionsRef () const =0
 
bool isAssump () const
 
const ProofgetProof ()
 

Friends

class Theorem
 
class RegTheoremValue
 
class RWTheoremValue
 

Detailed Description

Definition at line 56 of file theorem_value.h.

Constructor & Destructor Documentation

CVC3::TheoremValue::TheoremValue ( TheoremManager tm,
const Expr thm,
const Proof pf,
bool  isAssump 
)
inlineprivate

NOTE: it is private; only friend classes can call it.

If the assumptions refer to only one theorem, grab the assumptions of that theorem instead.

Definition at line 110 of file theorem_value.h.

CVC3::TheoremValue::TheoremValue ( const TheoremValue t)
inlineprivate

Definition at line 117 of file theorem_value.h.

References FatalAssert.

virtual CVC3::TheoremValue::~TheoremValue ( )
inlinevirtual

Definition at line 320 of file theorem_value.h.

References d_refcount, FatalAssert, and IF_DEBUG.

Member Function Documentation

TheoremValue& CVC3::TheoremValue::operator= ( const TheoremValue t)
inlineprivate

Definition at line 120 of file theorem_value.h.

References FatalAssert.

bool CVC3::TheoremValue::isFlagged ( ) const
inlineprivate

Definition at line 125 of file theorem_value.h.

References d_flag, d_tm, and CVC3::TheoremManager::getFlag().

Referenced by CVC3::Theorem::isFlagged().

void CVC3::TheoremValue::clearAllFlags ( )
inlineprivate

Definition at line 129 of file theorem_value.h.

References CVC3::TheoremManager::clearAllFlags(), and d_tm.

Referenced by CVC3::Theorem::clearAllFlags().

void CVC3::TheoremValue::setFlag ( )
inlineprivate

Definition at line 133 of file theorem_value.h.

References d_flag, d_tm, and CVC3::TheoremManager::getFlag().

Referenced by CVC3::Theorem::setFlag().

void CVC3::TheoremValue::setCachedValue ( int  value)
inlineprivate

Definition at line 137 of file theorem_value.h.

References d_cachedValue.

Referenced by CVC3::Theorem::setCachedValue().

int CVC3::TheoremValue::getCachedValue ( ) const
inlineprivate

Definition at line 141 of file theorem_value.h.

References d_cachedValue.

Referenced by CVC3::Theorem::getCachedValue().

void CVC3::TheoremValue::setSubst ( )
inlineprivate

Definition at line 145 of file theorem_value.h.

References d_isSubst.

Referenced by CVC3::Theorem::setSubst().

bool CVC3::TheoremValue::isSubst ( )
inlineprivate

Definition at line 146 of file theorem_value.h.

References d_isSubst.

Referenced by CVC3::Theorem::isSubst().

void CVC3::TheoremValue::setExpandFlag ( bool  val)
inlineprivate

Definition at line 148 of file theorem_value.h.

References d_expand.

Referenced by CVC3::Theorem::setExpandFlag().

bool CVC3::TheoremValue::getExpandFlag ( )
inlineprivate

Definition at line 152 of file theorem_value.h.

References d_expand.

Referenced by CVC3::Theorem::getExpandFlag().

void CVC3::TheoremValue::setLitFlag ( bool  val)
inlineprivate

Definition at line 156 of file theorem_value.h.

References d_clauselit.

Referenced by CVC3::Theorem::setLitFlag().

bool CVC3::TheoremValue::getLitFlag ( )
inlineprivate

Definition at line 160 of file theorem_value.h.

References d_clauselit.

Referenced by CVC3::Theorem::getLitFlag().

int CVC3::TheoremValue::getScope ( )
inlineprivate

Definition at line 164 of file theorem_value.h.

References d_scopeLevel.

Referenced by CVC3::Theorem::getScope().

unsigned CVC3::TheoremValue::getQuantLevel ( )
inlineprivate

Definition at line 168 of file theorem_value.h.

References d_quantLevel.

Referenced by CVC3::Theorem::getQuantLevel().

unsigned CVC3::TheoremValue::getQuantLevelDebug ( )
inlineprivate

Definition at line 170 of file theorem_value.h.

Referenced by CVC3::Theorem::getQuantLevelDebug().

void CVC3::TheoremValue::setQuantLevel ( unsigned  level)
inlineprivate

Definition at line 175 of file theorem_value.h.

References d_quantLevel.

Referenced by CVC3::Theorem::setQuantLevel().

unsigned CVC3::TheoremValue::recQuantLevel ( Expr  proof)
inlineprivate

Definition at line 177 of file theorem_value.h.

References d_quantLevel.

unsigned CVC3::TheoremValue::findQuantLevelDebug ( )
inlineprivate

Definition at line 247 of file theorem_value.h.

References d_quantLevel.

virtual bool CVC3::TheoremValue::isRewrite ( ) const
inlineprivatevirtual

Reimplemented in CVC3::RWTheoremValue.

Definition at line 295 of file theorem_value.h.

Referenced by getLHS(), getRHS(), and CVC3::Theorem::isRewrite().

virtual const Expr& CVC3::TheoremValue::getExpr ( ) const
inlineprivatevirtual

Reimplemented in CVC3::RWTheoremValue.

Definition at line 297 of file theorem_value.h.

References d_thm.

Referenced by CVC3::VCL::deriveClosure(), CVC3::VCL::getAssumptions(), CVC3::Theorem::getExpr(), and toString().

virtual const Expr& CVC3::TheoremValue::getLHS ( ) const
inlineprivatevirtual

Reimplemented in CVC3::RWTheoremValue.

Definition at line 298 of file theorem_value.h.

References d_thm, DebugAssert, isRewrite(), and toString().

Referenced by CVC3::Theorem::getLHS().

virtual const Expr& CVC3::TheoremValue::getRHS ( ) const
inlineprivatevirtual

Reimplemented in CVC3::RWTheoremValue.

Definition at line 305 of file theorem_value.h.

References d_thm, DebugAssert, isRewrite(), and toString().

Referenced by CVC3::Theorem::getRHS().

virtual const Assumptions& CVC3::TheoremValue::getAssumptionsRef ( ) const
privatepure virtual
bool CVC3::TheoremValue::isAssump ( ) const
inlineprivate

Definition at line 315 of file theorem_value.h.

References d_isAssump.

Referenced by CVC3::Theorem::isAssump().

const Proof& CVC3::TheoremValue::getProof ( )
inlineprivate

Definition at line 316 of file theorem_value.h.

References d_proof.

Referenced by CVC3::Theorem::getProof().

std::string CVC3::TheoremValue::toString ( ) const
inline

Definition at line 325 of file theorem_value.h.

References getAssumptionsRef(), getExpr(), CVC3::Assumptions::toString(), and CVC3::Expr::toString().

Referenced by getLHS(), and getRHS().

virtual MemoryManager* CVC3::TheoremValue::getMM ( )
pure virtual

Friends And Related Function Documentation

friend class Theorem
friend

Definition at line 59 of file theorem_value.h.

friend class RegTheoremValue
friend

Definition at line 60 of file theorem_value.h.

friend class RWTheoremValue
friend

Definition at line 61 of file theorem_value.h.

Member Data Documentation

TheoremManager* CVC3::TheoremValue::d_tm
protected
Expr CVC3::TheoremValue::d_thm
protected

The expression representing a theorem.

Definition at line 68 of file theorem_value.h.

Referenced by getExpr(), CVC3::RWTheoremValue::getExpr(), getLHS(), and getRHS().

Proof CVC3::TheoremValue::d_proof
protected

Proof of the theorem.

Definition at line 71 of file theorem_value.h.

Referenced by getProof().

unsigned CVC3::TheoremValue::d_refcount
protected
int CVC3::TheoremValue::d_scopeLevel
protected

Largest scope level of the assumptions.

Definition at line 77 of file theorem_value.h.

Referenced by getScope(), CVC3::RWTheoremValue::init(), and CVC3::RegTheoremValue::RegTheoremValue().

unsigned CVC3::TheoremValue::d_quantLevel
protected
unsigned CVC3::TheoremValue::d_flag
protected

debug quantlevel, this one is from proof, not from assumption list

Temporary flag used during traversals

Definition at line 87 of file theorem_value.h.

Referenced by isFlagged(), and setFlag().

int CVC3::TheoremValue::d_cachedValue
protected

Temporary cache used during traversals.

Definition at line 90 of file theorem_value.h.

Referenced by getCachedValue(), and setCachedValue().

bool CVC3::TheoremValue::d_isSubst
protected

whether this theorem was generated by substitution

Definition at line 92 of file theorem_value.h.

Referenced by isSubst(), and setSubst().

bool CVC3::TheoremValue::d_isAssump
protected
bool CVC3::TheoremValue::d_expand
protected

whether it should this be expanded in graph traversal

Definition at line 94 of file theorem_value.h.

Referenced by getExpandFlag(), and setExpandFlag().

bool CVC3::TheoremValue::d_clauselit
protected

whether it belongs to the conflict clause

Definition at line 95 of file theorem_value.h.

Referenced by getLitFlag(), and setLitFlag().


The documentation for this class was generated from the following file: