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

#include <theorem_value.h>

Inherits CVC3::TheoremValue.

Collaboration diagram for CVC3::RWTheoremValue:
Collaboration graph

Public Member Functions

 ~RWTheoremValue ()
 
bool isRewrite () const
 
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

Expr d_lhs
 
Expr d_rhs
 
Assumptionsd_assump
 
- 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

void init (const Assumptions &assump, int scope)
 
 RWTheoremValue (TheoremManager *tm, const Expr &lhs, const Expr &rhs, const Assumptions &assump, const Proof &pf, bool isAssump, int scope=-1)
 
 RWTheoremValue (TheoremManager *tm, const Expr &thm, const Assumptions &assump, const Proof &pf, bool isAssump, int scope=-1)
 
const ExprgetExpr () const
 
const ExprgetLHS () const
 
const ExprgetRHS () const
 

Friends

class Theorem
 

Detailed Description

Definition at line 432 of file theorem_value.h.

Constructor & Destructor Documentation

CVC3::RWTheoremValue::RWTheoremValue ( TheoremManager tm,
const Expr lhs,
const Expr rhs,
const Assumptions assump,
const Proof pf,
bool  isAssump,
int  scope = -1 
)
inlineprivate

Definition at line 487 of file theorem_value.h.

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

Definition at line 494 of file theorem_value.h.

CVC3::RWTheoremValue::~RWTheoremValue ( )
inline

Definition at line 516 of file theorem_value.h.

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

Member Function Documentation

void CVC3::RWTheoremValue::init ( const Assumptions assump,
int  scope 
)
inlineprivate
const Expr& CVC3::RWTheoremValue::getExpr ( ) const
inlineprivatevirtual
const Expr& CVC3::RWTheoremValue::getLHS ( ) const
inlineprivatevirtual

Reimplemented from CVC3::TheoremValue.

Definition at line 511 of file theorem_value.h.

const Expr& CVC3::RWTheoremValue::getRHS ( ) const
inlineprivatevirtual

Reimplemented from CVC3::TheoremValue.

Definition at line 512 of file theorem_value.h.

bool CVC3::RWTheoremValue::isRewrite ( ) const
inlinevirtual

Reimplemented from CVC3::TheoremValue.

Definition at line 525 of file theorem_value.h.

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

Implements CVC3::TheoremValue.

Definition at line 526 of file theorem_value.h.

References CVC3::Assumptions::emptyAssump().

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

Implements CVC3::TheoremValue.

Definition at line 532 of file theorem_value.h.

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

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

Definition at line 534 of file theorem_value.h.

References CVC3::MemoryManager::newData().

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

Definition at line 537 of file theorem_value.h.

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

Definition at line 541 of file theorem_value.h.

Friends And Related Function Documentation

friend class Theorem
friend

Definition at line 434 of file theorem_value.h.

Member Data Documentation

Expr CVC3::RWTheoremValue::d_lhs
protected

Definition at line 439 of file theorem_value.h.

Expr CVC3::RWTheoremValue::d_rhs
protected

Definition at line 440 of file theorem_value.h.

Assumptions* CVC3::RWTheoremValue::d_assump
protected

Definition at line 441 of file theorem_value.h.


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