CVC3::ClauseValue Class Reference

#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)
• IF_DEBUG (std::string d_file;int d_line)
• 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(), d_dir, d_literals, d_sat, d_wp, DebugAssert, CVC3::Theorem::getExpr(), IF_DEBUG(), CVC3::Expr::isOr(), CVC3::ContextObj::setName(), 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.

CVC3::ClauseValue::IF_DEBUG

(

std::string d_file;int

d_line

)

[private]

Referenced by ClauseValue(), and ~ClauseValue().

---

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:

• clause.h
• clause.cpp

---