CVC3::ClauseValue Class Reference

#include <clause.h>

Collaboration diagram for CVC3::ClauseValue:

Collaboration graph
[legend]
List of all members.

Public Member Functions

Private Member Functions

Private Attributes

Friends


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]

Definition at line 35 of file clause.cpp.

References CVC3::Expr::arity(), CVC3::Literal::count(), d_dir, d_literals, d_sat, d_wp, DebugAssert, CVC3::Theorem::getExpr(), IF_DEBUG, CVC3::Expr::isOr(), and CVC3::Theorem::toString().

CVC3::ClauseValue::~ClauseValue (  ) 

Definition at line 65 of file clause.cpp.

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


Member Function Documentation

ClauseValue& CVC3::ClauseValue::operator= ( const ClauseValue c  )  [inline, private]

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=(), CVC3::Clause::~Clause(), 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]

Definition at line 55 of file clause.h.

Referenced by ClauseValue(), CVC3::Clause::getLiteral(), CVC3::Clause::getLiterals(), CVC3::Clause::markDeleted(), CVC3::Clause::sat(), CVC3::Clause::size(), and ~ClauseValue().

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(), CVC3::Clause::markDeleted(), and ~ClauseValue().


The documentation for this class was generated from the following files:
Generated on Wed Nov 18 16:14:34 2009 for CVC3 by  doxygen 1.5.2