CVC3  2.4.1
Public Member Functions | Private Member Functions | Private Attributes | Friends | List of all members
CVC3::Clause Class Reference

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

#include <clause.h>

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. More...
 
bool sat (bool ignored) const
 Precise version of sat(): check all the literals and cache the result. More...
 
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) More...
 
std::string toString () const
 

Private Member Functions

int & countOwner ()
 Export owner refcounting to ClauseOwner. More...
 

Private Attributes

ClauseValued_clause
 The only value member. More...
 

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 CVC3::ClauseValue::d_refcount, and IF_DEBUG.

CVC3::Clause::Clause ( const Clause c)
inline

Definition at line 103 of file clause.h.

References 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
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 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

Definition at line 138 of file clause.h.

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

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

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 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 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 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 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 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 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.

Referenced by CVC3::ClauseOwner::operator=(), and CVC3::ClauseOwner::~ClauseOwner().

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 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 only value member.

Definition at line 87 of file clause.h.

Referenced by id(), CVC3::ClauseOwner::operator Clause &(), CVC3::ClauseOwner::operator const Clause &(), operator=(), and operator==().


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