#include <clause.h>

Collaboration diagram for CVC3::ClauseValue:

[legend]

List of all members.

Public Member Functions

~ClauseValue ()

Private Member Functions

ClauseValue (const ClauseValue &c)
ClauseValue & operator= (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< Literal > d_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]`

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::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

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]

Definition at line 55 of file clause.h.

Referenced by ClauseValue(), CVC3::Clause::getLiteral(), CVC3::Clause::getLiterals(), 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(), and ~ClauseValue().

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

CVC3::ClauseValue Class Reference