CVCL::Clause

CVCL::Clause Class Reference

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

#include <clause.h>

Collaboration diagram for CVCL::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::string &getFile() const {return d_clause->d_file;}) IF_DEBUG(int getLine() const

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 91 of file clause.h.

Constructor & Destructor Documentation

CVCL::Clause::Clause ( ) [inline]

Definition at line 102 of file clause.h.

CVCL::Clause::Clause ( TheoryCore * core,

VariableManager * vm,

const Theorem & clause,

int scope,

const std::string & file = "",

int line = 0

) [inline]

Definition at line 104 of file clause.h.
References d_clause, CVCL::ClauseValue::d_refcount, and IF_DEBUG().

CVCL::Clause::Clause ( const Clause & c ) [inline]

Definition at line 111 of file clause.h.
References d_clause, and CVCL::ClauseValue::d_refcount.

CVCL::Clause::~Clause ( )

Definition at line 93 of file clause.cpp.
References d_clause, CVCL::ClauseValue::d_refcount, and CVCL::int2string().

Member Function Documentation

int& CVCL::Clause::countOwner ( ) [inline, private]

Export owner refcounting to ClauseOwner.

Definition at line 97 of file clause.h.
References d_clause, and CVCL::ClauseValue::d_refcountOwner.
Referenced by CVCL::ClauseOwner::operator=().

Clause & CVCL::Clause::operator= ( const Clause & c )

Definition at line 123 of file clause.cpp.
References d_clause, CVCL::ClauseValue::d_refcount, and CVCL::int2string().

bool CVCL::Clause::isNull ( ) const [inline]

Definition at line 119 of file clause.h.
References d_clause.
Referenced by CVCL::SearchEngineFast::analyzeUIPs(), deleted(), dir(), CVCL::SearchEngineFast::fixConflict(), getLiteral(), getLiterals(), getScope(), getTheorem(), markDeleted(), markSat(), CVCL::operator<<(), sat(), CVCL::VariableValue::setValue(), and wp().

size_t CVCL::Clause::size ( ) const [inline]

Definition at line 121 of file clause.h.
References d_clause, and CVCL::ClauseValue::d_literals.
Referenced by CVCL::SearchEngineFast::addNewClause(), CVCL::SearchEngineFast::analyzeUIPs(), CVCL::SearchEngineFast::findSplitter(), CVCL::SearchEngineFast::fixConflict(), getLiteral(), CVCL::operator<<(), CVCL::SearchEngineFast::propagate(), CVCL::VariableValue::setValue(), CVCL::SearchEngineFast::unitPropagation(), CVCL::SearchEngineFast::updateLitCounts(), and wp().

const Theorem& CVCL::Clause::getTheorem ( ) const [inline]

Definition at line 125 of file clause.h.
References d_clause, CVCL::ClauseValue::d_thm, and isNull().
Referenced by CVCL::Variable::deriveThmRec(), CVCL::SearchEngineFast::fixConflict(), CVCL::operator<<(), CVCL::SearchEngineFast::propagate(), and CVCL::SearchEngineFast::unitPropagation().

int CVCL::Clause::getScope ( ) const [inline]

Definition at line 130 of file clause.h.
References d_clause, CVCL::ClauseValue::d_scope, and isNull().
Referenced by CVCL::SearchEngineFast::analyzeUIPs(), CVCL::SearchEngineFast::fixConflict(), and CVCL::VariableValue::setValue().

const Literal& CVCL::Clause::getLiteral ( size_t i ) const [inline]

Definition at line 135 of file clause.h.
References d_clause, CVCL::ClauseValue::d_literals, CVCL::int2string(), isNull(), and size().
Referenced by operator[](), and watched().

const Literal& CVCL::Clause::operator[] ( size_t i ) const [inline]

Definition at line 143 of file clause.h.
References getLiteral().

const std::vector<Literal>& CVCL::Clause::getLiterals ( ) const [inline]

Definition at line 146 of file clause.h.
References d_clause, CVCL::ClauseValue::d_literals, and isNull().
Referenced by CVCL::Variable::deriveThmRec(), and CVCL::operator<<().

size_t CVCL::Clause::wp ( int i ) const [inline]

Definition at line 151 of file clause.h.
References d_clause, CVCL::ClauseValue::d_wp, CVCL::int2string(), and isNull().
Referenced by CVCL::SearchEngineFast::addNewClause(), CVCL::SearchEngineFast::analyzeUIPs(), CVCL::operator<<(), CVCL::SearchEngineFast::propagate(), and watched().

const Literal& CVCL::Clause::watched ( int i ) const [inline]

Definition at line 159 of file clause.h.
References getLiteral(), and wp().
Referenced by CVCL::SearchEngineFast::addNewClause(), CVCL::SearchEngineFast::analyzeUIPs(), CVCL::SearchEngineFast::bcp(), and CVCL::SearchEngineFast::propagate().

size_t CVCL::Clause::wp ( int i,

size_t l

) const [inline]

Definition at line 161 of file clause.h.
References d_clause, CVCL::ClauseValue::d_wp, CVCL::int2string(), isNull(), size(), and CVCL::TRACE.

int CVCL::Clause::dir ( int i ) const [inline]

Definition at line 176 of file clause.h.
References d_clause, CVCL::ClauseValue::d_dir, CVCL::int2string(), and isNull().
Referenced by CVCL::operator<<(), and CVCL::SearchEngineFast::propagate().

int CVCL::Clause::dir ( int i,

int d

) const [inline]

Definition at line 184 of file clause.h.
References d_clause, CVCL::ClauseValue::d_dir, CVCL::int2string(), and isNull().

bool CVCL::Clause::sat ( ) const [inline]

Check if the clause marked as SAT.

Definition at line 195 of file clause.h.
References d_clause, CVCL::ClauseValue::d_sat, and isNull().
Referenced by CVCL::SearchEngineFast::bcp(), and CVCL::operator<<().

bool CVCL::Clause::sat ( bool ignored ) const [inline]

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

Definition at line 200 of file clause.h.
References d_clause, CVCL::ClauseValue::d_literals, CVCL::ClauseValue::d_sat, isNull(), and markSat().

void CVCL::Clause::markSat ( ) const [inline]

Definition at line 215 of file clause.h.
References d_clause, CVCL::ClauseValue::d_sat, and isNull().
Referenced by CVCL::SearchEngineFast::propagate(), and sat().

bool CVCL::Clause::deleted ( ) const [inline]

Definition at line 220 of file clause.h.
References d_clause, CVCL::ClauseValue::d_deleted, and isNull().
Referenced by CVCL::SearchEngineFast::bcp(), and CVCL::operator<<().

void CVCL::Clause::markDeleted ( ) const

Definition at line 104 of file clause.cpp.
References d_clause, CVCL::ClauseValue::d_deleted, CVCL::ClauseValue::d_literals, IF_DEBUG(), isNull(), and CVCL::TRACE.

size_t CVCL::Clause::id ( ) const [inline]

Definition at line 227 of file clause.h.
References d_clause.
Referenced by CVCL::operator<<().

bool CVCL::Clause::operator== ( const Clause & c ) const [inline]

Definition at line 230 of file clause.h.
References d_clause.

int CVCL::Clause::owners ( ) const [inline]

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

Definition at line 233 of file clause.h.
References d_clause, and CVCL::ClauseValue::d_refcountOwner.
Referenced by CVCL::operator<<().

string CVCL::Clause::toString ( ) const

Definition at line 137 of file clause.cpp.
Referenced by CVCL::SearchEngineFast::fixConflict(), CVCL::SearchEngineFast::propagate(), CVCL::VariableValue::setValue(), and CVCL::SearchEngineFast::unitPropagation().

CVCL::Clause::IF_DEBUG ( bool wpCheck() const )

CVCL::Clause::IF_DEBUG ( ) const [inline]

Definition at line 241 of file clause.h.
Referenced by Clause(), and markDeleted().

Friends And Related Function Documentation

friend class ClauseOwner [friend]

Definition at line 93 of file clause.h.

std::ostream& operator<< ( std::ostream & os,

const Clause & c

) [friend]

Member Data Documentation

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

The only value member.

Definition at line 95 of file clause.h.
Referenced by Clause(), countOwner(), deleted(), dir(), getLiteral(), getLiterals(), getScope(), getTheorem(), id(), isNull(), markDeleted(), markSat(), operator=(), operator==(), owners(), sat(), size(), wp(), and ~Clause().

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

Generated on Thu Apr 13 16:57:42 2006 for CVC Lite by

1.4.4