CVC3  2.4.1
Public Member Functions | Private Member Functions | Private Attributes | Friends
CVC3::Clause Class Reference

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

#include <clause.h>

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 ()
Clauseoperator= (const Clause &c)
bool isNull () const
size_t size () const
const TheoremgetTheorem () const
int getScope () const
const LiteralgetLiteral (size_t i) const
const Literaloperator[] (size_t i) const
const std::vector< Literal > & getLiterals () const
size_t wp (int i) const
const Literalwatched (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

Private Member Functions

int & countOwner ()
 Export owner refcounting to ClauseOwner.

Private Attributes

ClauseValued_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 FatalAssert, and CVC3::int2string().


Member Function Documentation

int& CVC3::Clause::countOwner ( )
inlineprivate

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, DebugAssert, and CVC3::int2string().

bool CVC3::Clause::isNull ( ) const
inline
size_t CVC3::Clause::size ( ) const
inline
const Theorem& CVC3::Clause::getTheorem ( ) const
inline
int CVC3::Clause::getScope ( ) const
inline
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, CVC3::int2string(), 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
size_t CVC3::Clause::wp ( int  i) const
inline
const Literal& CVC3::Clause::watched ( int  i) const
inline
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, CVC3::int2string(), isNull(), size(), and TRACE.

int CVC3::Clause::dir ( int  i) const
inline
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, CVC3::int2string(), 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::SearchEngineFast::bcp(), and 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::SearchEngineFast::bcp(), and CVC3::operator<<().

void CVC3::Clause::markDeleted ( ) const

Definition at line 96 of file clause.cpp.

References DebugAssert, IF_DEBUG, 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

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 documentation for this class was generated from the following files: