CVC3: CVC3::ClauseValue Class Reference

CVC3

#include <clause.h>

Collaboration diagram for CVC3::ClauseValue:

Collaboration graph

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 )

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

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: