CVC3  2.4.1
Public Member Functions | Private Member Functions | Private Attributes | Friends
CVC3::ClauseValue Class Reference

#include <clause.h>

List of all members.

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.
int d_refcountOwner
 Ref. counter of ClauseOwner classes holding it.
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: