CVC3::Clause Class Reference

A class representing a CNF clause (a smart pointer). More...

#include <clause.h>

Collaboration diagram for CVC3::Clause:

[legend]List of all members.

Public Member Functions

• Clause ()
• Clause (TheoryCore *core, VariableManager *vm, const Theorem &clause, int scope, const std::string &file="", int line=0)
• Clause (const Clause &c)
• ~Clause ()
• Clause & operator= (const Clause &c)
• bool isNull () const
• size_t size () const
• const Theorem & getTheorem () const
• int getScope () const
• const Literal & getLiteral (size_t i) const
• const Literal & operator[] (size_t i) const
• const std::vector< Literal > & getLiterals () const
• size_t wp (int i) const
• const Literal & watched (int i) const
• size_t wp (int i, size_t l) const
• int dir (int i) const
• int dir (int i, int d) const
• bool sat () const

  Check if the clause marked as SAT.
  

• bool sat (bool ignored) const

  Precise version of sat(): check all the literals and cache the result.
  

• void markSat () const
• bool deleted () const
• void markDeleted () const
• size_t id () const
• bool operator== (const Clause &c) const
• int owners () const

  Tell how many owners this clause has (for debugging).
  

• std::string toString () const
• IF_DEBUG (bool wpCheck() const ;) IF_DEBUG(const std

Private Member Functions

• int & countOwner ()

  Export owner refcounting to ClauseOwner.
  

Private Attributes

• ClauseValue * d_clause

  The only value member.
  

Friends

• class ClauseOwner
• std::ostream & operator<< (std::ostream &os, const Clause &c)

---

Detailed Description

A class representing a CNF clause (a smart pointer).

Definition at line 83 of file clause.h.

---

Constructor & Destructor Documentation

CVC3::Clause::Clause

(

)

[inline]

Definition at line 94 of file clause.h.

CVC3::Clause::Clause	(	TheoryCore *	core,
		VariableManager *	vm,
		const Theorem &	clause,
		int	scope,
		const std::string &	file = "",
		int	line = 0
	)			[inline]

Definition at line 96 of file clause.h.

References d_clause, CVC3::ClauseValue::d_refcount, and IF_DEBUG().

CVC3::Clause::Clause

(

const Clause &

c

)

[inline]

Definition at line 103 of file clause.h.

References d_clause, and CVC3::ClauseValue::d_refcount.

CVC3::Clause::~Clause

(

)

Definition at line 85 of file clause.cpp.

References d_clause, CVC3::ClauseValue::d_refcount, and FatalAssert.

---

Member Function Documentation

int& CVC3::Clause::countOwner

(

)

[inline, private]

Export owner refcounting to ClauseOwner.

Definition at line 89 of file clause.h.

References d_clause, CVC3::ClauseValue::d_refcountOwner, and DebugAssert.

Clause & CVC3::Clause::operator=

(

const Clause &

c

)

Definition at line 115 of file clause.cpp.

References d_clause, CVC3::ClauseValue::d_refcount, and DebugAssert.

bool CVC3::Clause::isNull

(

)

const [inline]

Definition at line 111 of file clause.h.

References d_clause.

Referenced by CVC3::SearchEngineFast::analyzeUIPs(), deleted(), dir(), CVC3::SearchEngineFast::fixConflict(), getLiteral(), getLiterals(), getScope(), getTheorem(), markDeleted(), markSat(), CVC3::operator<<(), sat(), and wp().

size_t CVC3::Clause::size

(

)

const [inline]

Definition at line 113 of file clause.h.

References d_clause, and CVC3::ClauseValue::d_literals.

Referenced by CVC3::SearchEngineFast::addNewClause(), CVC3::SearchEngineFast::analyzeUIPs(), CVC3::SearchEngineFast::findSplitter(), CVC3::SearchEngineFast::fixConflict(), getLiteral(), CVC3::operator<<(), CVC3::SearchEngineFast::propagate(), CVC3::VariableValue::setValue(), CVC3::SearchEngineFast::traceConflict(), CVC3::SearchEngineFast::unitPropagation(), CVC3::SearchEngineFast::updateLitCounts(), and wp().

const Theorem& CVC3::Clause::getTheorem

(

)

const [inline]

Definition at line 117 of file clause.h.

References d_clause, CVC3::ClauseValue::d_thm, DebugAssert, and isNull().

Referenced by CVC3::Variable::deriveThmRec(), CVC3::SearchEngineFast::fixConflict(), CVC3::operator<<(), CVC3::SearchEngineFast::propagate(), and CVC3::SearchEngineFast::unitPropagation().

int CVC3::Clause::getScope

(

)

const [inline]

Definition at line 122 of file clause.h.

References d_clause, CVC3::ClauseValue::d_scope, and isNull().

Referenced by CVC3::SearchEngineFast::analyzeUIPs(), and CVC3::VariableValue::setValue().

const Literal& CVC3::Clause::getLiteral

(

size_t

i

)

const [inline]

Definition at line 127 of file clause.h.

References d_clause, CVC3::ClauseValue::d_literals, DebugAssert, isNull(), and size().

Referenced by operator[](), and watched().

const Literal& CVC3::Clause::operator[]

(

size_t

i

)

const [inline]

Definition at line 135 of file clause.h.

References getLiteral().

const std::vector<Literal>& CVC3::Clause::getLiterals

(

)

const [inline]

Definition at line 138 of file clause.h.

References d_clause, CVC3::ClauseValue::d_literals, DebugAssert, and isNull().

Referenced by CVC3::Variable::deriveThmRec(), and CVC3::operator<<().

size_t CVC3::Clause::wp

(

int

i

)

const [inline]

Definition at line 143 of file clause.h.

References d_clause, CVC3::ClauseValue::d_wp, DebugAssert, and isNull().

Referenced by CVC3::SearchEngineFast::addNewClause(), CVC3::SearchEngineFast::analyzeUIPs(), CVC3::operator<<(), CVC3::SearchEngineFast::propagate(), and watched().

const Literal& CVC3::Clause::watched

(

int

i

)

const [inline]

Definition at line 151 of file clause.h.

References getLiteral(), and wp().

Referenced by CVC3::SearchEngineFast::addNewClause(), CVC3::SearchEngineFast::analyzeUIPs(), and CVC3::SearchEngineFast::propagate().

size_t CVC3::Clause::wp	(	int	i,
		size_t	l
	)			const [inline]

Definition at line 153 of file clause.h.

References d_clause, CVC3::ClauseValue::d_wp, DebugAssert, isNull(), size(), and CVC3::TRACE.

int CVC3::Clause::dir

(

int

i

)

const [inline]

Definition at line 168 of file clause.h.

References d_clause, CVC3::ClauseValue::d_dir, DebugAssert, and isNull().

Referenced by CVC3::operator<<(), and CVC3::SearchEngineFast::propagate().

int CVC3::Clause::dir	(	int	i,
		int	d
	)			const [inline]

Definition at line 176 of file clause.h.

References d_clause, CVC3::ClauseValue::d_dir, DebugAssert, and isNull().

bool CVC3::Clause::sat

(

)

const [inline]

Check if the clause marked as SAT.

Definition at line 187 of file clause.h.

References d_clause, CVC3::ClauseValue::d_sat, DebugAssert, and isNull().

Referenced by CVC3::operator<<().

bool CVC3::Clause::sat

(

bool

ignored

)

const [inline]

Precise version of sat(): check all the literals and cache the result.

Definition at line 192 of file clause.h.

References d_clause, CVC3::ClauseValue::d_literals, CVC3::ClauseValue::d_sat, DebugAssert, isNull(), and markSat().

void CVC3::Clause::markSat

(

)

const [inline]

Definition at line 207 of file clause.h.

References d_clause, CVC3::ClauseValue::d_sat, DebugAssert, and isNull().

Referenced by CVC3::SearchEngineFast::propagate(), and sat().

bool CVC3::Clause::deleted

(

)

const [inline]

Definition at line 212 of file clause.h.

References d_clause, CVC3::ClauseValue::d_deleted, DebugAssert, and isNull().

Referenced by CVC3::operator<<().

void CVC3::Clause::markDeleted

(

)

const

Definition at line 96 of file clause.cpp.

References d_clause, CVC3::ClauseValue::d_deleted, CVC3::ClauseValue::d_literals, DebugAssert, IF_DEBUG(), isNull(), CVC3::TRACE, and TRACE_MSG.

size_t CVC3::Clause::id

(

)

const [inline]

Definition at line 219 of file clause.h.

References d_clause.

Referenced by CVC3::operator<<().

bool CVC3::Clause::operator==

(

const Clause &

c

)

const [inline]

Definition at line 222 of file clause.h.

References d_clause.

int CVC3::Clause::owners

(

)

const [inline]

Tell how many owners this clause has (for debugging).

Definition at line 225 of file clause.h.

References d_clause, and CVC3::ClauseValue::d_refcountOwner.

Referenced by CVC3::operator<<().

string CVC3::Clause::toString

(

)

const

Definition at line 129 of file clause.cpp.

Referenced by CVC3::SearchEngineFast::propagate(), CVC3::VariableValue::setValue(), and CVC3::SearchEngineFast::unitPropagation().

CVC3::Clause::IF_DEBUG

(

bool wpCheck() const ;

)

const [inline]

Definition at line 232 of file clause.h.

References d_clause.

Referenced by Clause(), markDeleted(), and CVC3::operator<<().

---

Friends And Related Function Documentation

friend class ClauseOwner [friend]

Definition at line 85 of file clause.h.

std::ostream& operator<<	(	std::ostream &	os,
		const Clause &	c
	)			[friend]

Definition at line 135 of file clause.cpp.

---

Member Data Documentation

ClauseValue* CVC3::Clause::d_clause [private]

The only value member.

Definition at line 87 of file clause.h.

Referenced by Clause(), CVC3::ClauseOwner::ClauseOwner(), countOwner(), deleted(), dir(), getLiteral(), getLiterals(), getScope(), getTheorem(), id(), IF_DEBUG(), isNull(), markDeleted(), markSat(), CVC3::ClauseOwner::operator Clause &(), CVC3::ClauseOwner::operator const Clause &(), CVC3::ClauseOwner::operator=(), operator=(), operator==(), owners(), sat(), size(), wp(), ~Clause(), and CVC3::ClauseOwner::~ClauseOwner().

---

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

• clause.h
• clause.cpp

---