CVC3
Public Member Functions | Protected Attributes | Private Member Functions | Friends | List of all members
CVC3::RegTheoremValue Class Reference

#include <theorem_value.h>

Inherits CVC3::TheoremValue.

Collaboration diagram for CVC3::RegTheoremValue:
Collaboration graph

Public Member Functions

 ~RegTheoremValue ()
 
const AssumptionsgetAssumptionsRef () const
 
MemoryManagergetMM ()
 
void * operator new (size_t size, MemoryManager *mm)
 
void operator delete (void *pMem, MemoryManager *mm)
 
void operator delete (void *d)
 
- Public Member Functions inherited from CVC3::TheoremValue
virtual ~TheoremValue ()
 
std::string toString () const
 

Protected Attributes

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

Private Member Functions

 RegTheoremValue (TheoremManager *tm, const Expr &thm, const Assumptions &assump, const Proof &pf, bool isAssump, int scope=-1)
 

Friends

class Theorem
 

Detailed Description

Definition at line 343 of file theorem_value.h.

Constructor & Destructor Documentation

CVC3::RegTheoremValue::RegTheoremValue ( TheoremManager tm,
const Expr thm,
const Assumptions assump,
const Proof pf,
bool  isAssump,
int  scope = -1 
)
inlineprivate
CVC3::RegTheoremValue::~RegTheoremValue ( )
inline

Definition at line 397 of file theorem_value.h.

References CVC3::TheoremValue::d_isAssump, FatalAssert, and IF_DEBUG.

Member Function Documentation

const Assumptions& CVC3::RegTheoremValue::getAssumptionsRef ( ) const
inlinevirtual

Implements CVC3::TheoremValue.

Definition at line 405 of file theorem_value.h.

MemoryManager* CVC3::RegTheoremValue::getMM ( )
inlinevirtual

Implements CVC3::TheoremValue.

Definition at line 408 of file theorem_value.h.

References CVC3::TheoremValue::d_tm, and CVC3::TheoremManager::getMM().

void* CVC3::RegTheoremValue::operator new ( size_t  size,
MemoryManager mm 
)
inline

Definition at line 410 of file theorem_value.h.

References CVC3::MemoryManager::newData().

void CVC3::RegTheoremValue::operator delete ( void *  pMem,
MemoryManager mm 
)
inline

Definition at line 413 of file theorem_value.h.

void CVC3::RegTheoremValue::operator delete ( void *  d)
inline

Definition at line 417 of file theorem_value.h.

Friends And Related Function Documentation

friend class Theorem
friend

Definition at line 345 of file theorem_value.h.

Member Data Documentation

Assumptions CVC3::RegTheoremValue::d_assump
protected

The assumptions for the theorem.

Definition at line 349 of file theorem_value.h.


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