CVC3  2.4.1
Public Member Functions | Private Member Functions | Private Attributes | Friends | List of all members
CVC3::ClauseValue Class Reference

#include <clause.h>

Public Member Functions

 ~ClauseValue ()
 

Private Member Functions

 ClauseValue (const ClauseValue &c)
 
ClauseValueoperator= (const ClauseValue &c)
 
 ClauseValue (TheoryCore *core, VariableManager *vm, const Theorem &clause, int scope)
 

Private Attributes

int d_refcount
 Ref. counter. More...
 
int d_refcountOwner
 Ref. counter of ClauseOwner classes holding it. More...
 
Theorem d_thm
 
int d_scope
 
std::vector< Literald_literals
 
size_t d_wp [2]
 
int d_dir [2]
 
CDO< bool > d_sat
 
bool d_deleted
 

Friends

class Clause
 

Detailed Description

Definition at line 42 of file clause.h.

Constructor & Destructor Documentation

CVC3::ClauseValue::ClauseValue ( const ClauseValue c)
private
CVC3::ClauseValue::ClauseValue ( TheoryCore core,
VariableManager vm,
const Theorem clause,
int  scope 
)
private
CVC3::ClauseValue::~ClauseValue ( )

Definition at line 65 of file clause.cpp.

References d_deleted, d_literals, d_refcount, FatalAssert, IF_DEBUG, CVC3::int2string(), TRACE, and TRACE_MSG.

Member Function Documentation

ClauseValue& CVC3::ClauseValue::operator= ( const ClauseValue c)
inlineprivate

Definition at line 58 of file clause.h.

Friends And Related Function Documentation

friend class Clause
friend

Definition at line 43 of file clause.h.

Member Data Documentation

int CVC3::ClauseValue::d_refcount
private

Ref. counter.

Definition at line 46 of file clause.h.

Referenced by CVC3::Clause::Clause(), CVC3::Clause::operator=(), and ~ClauseValue().

int CVC3::ClauseValue::d_refcountOwner
private

Ref. counter of ClauseOwner classes holding it.

Definition at line 48 of file clause.h.

Referenced by CVC3::Clause::countOwner(), and CVC3::Clause::owners().

Theorem CVC3::ClauseValue::d_thm
private

Definition at line 50 of file clause.h.

Referenced by CVC3::Clause::getTheorem().

int CVC3::ClauseValue::d_scope
private

Definition at line 52 of file clause.h.

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

std::vector<Literal> CVC3::ClauseValue::d_literals
private
size_t CVC3::ClauseValue::d_wp[2]
private

Definition at line 61 of file clause.h.

Referenced by ClauseValue(), and CVC3::Clause::wp().

int CVC3::ClauseValue::d_dir[2]
private

Definition at line 65 of file clause.h.

Referenced by ClauseValue(), and CVC3::Clause::dir().

CDO<bool> CVC3::ClauseValue::d_sat
private

Definition at line 67 of file clause.h.

Referenced by ClauseValue(), CVC3::Clause::markSat(), and CVC3::Clause::sat().

bool CVC3::ClauseValue::d_deleted
private

Definition at line 69 of file clause.h.

Referenced by CVC3::Clause::deleted(), and ~ClauseValue().


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