CVC3
Public Member Functions | Private Member Functions | Private Attributes | Friends

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]
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) [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

Ref. counter.

Definition at line 46 of file clause.h.

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

Ref. counter of ClauseOwner classes holding it.

Definition at line 48 of file clause.h.

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

Definition at line 50 of file clause.h.

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

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().

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: