CVC3::Clause Class Reference

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

#include <clause.h>

Collaboration diagram for CVC3::Clause:

Collaboration graph
[legend]
List of all members.

Public Member Functions

Private Member Functions

Private Attributes

Friends


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:
Generated on Wed Nov 18 16:14:35 2009 for CVC3 by  doxygen 1.5.2