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

#include <minisat_types.h>

Public Member Functions

 Clause (bool learnt, const std::vector< Lit > &ps, CVC3::Theorem theorem, int id, int pushID)
int size () const
bool learnt () const
Lit operator[] (int i) const
Litoperator[] (int i)
int id () const
int pushID () const
float activity () const
void setActivity (float activity)
void toLit (std::vector< Lit > &literals) const
CVC3::Theorem getTheorem () const
std::string toString () const
bool contains (Lit l)

Static Public Member Functions

static int ClauseIDNull ()
static ClauseDecision ()
static ClauseTheoryImplication ()

Private Attributes

unsigned int d_size_learnt
int d_id
int d_pushID
float d_activity
CVC3::Theorem d_theorem
Lit d_data [1]

Static Private Attributes

static Clauses_decision = NULL
static Clauses_theoryImplication = NULL

Friends

ClauseClause_new (const std::vector< Lit > &ps, CVC3::Theorem theorem, int id)
ClauseLemma_new (const std::vector< Lit > &ps, int id, int pushID)

Detailed Description

Definition at line 101 of file minisat_types.h.

Constructor & Destructor Documentation

MiniSat::Clause::Clause ( bool  learnt,
const std::vector< Lit > &  ps,
CVC3::Theorem  theorem,
int  id,
int  pushID 
)
inline

Definition at line 119 of file minisat_types.h.

References d_activity, d_data, d_id, d_pushID, d_size_learnt, d_theorem, id(), learnt(), and pushID().

Member Function Documentation

int MiniSat::Clause::size ( void  ) const
inline
bool MiniSat::Clause::learnt ( ) const
inline
Lit MiniSat::Clause::operator[] ( int  i) const
inline

Definition at line 135 of file minisat_types.h.

References d_data.

Lit& MiniSat::Clause::operator[] ( int  i)
inline

Definition at line 136 of file minisat_types.h.

References d_data.

int MiniSat::Clause::id ( ) const
inline
int MiniSat::Clause::pushID ( ) const
inline
float MiniSat::Clause::activity ( ) const
inline
void MiniSat::Clause::setActivity ( float  activity)
inline
void MiniSat::Clause::toLit ( std::vector< Lit > &  literals) const

Definition at line 72 of file minisat_types.cpp.

Referenced by MiniSat::Solver::insertLemma(), and MiniSat::Solver::toString().

CVC3::Theorem MiniSat::Clause::getTheorem ( ) const
inline

Definition at line 153 of file minisat_types.h.

References d_theorem.

Referenced by MiniSat::Solver::addClause(), and MiniSat::Derivation::createProof().

static int MiniSat::Clause::ClauseIDNull ( )
inlinestatic

Definition at line 155 of file minisat_types.h.

Clause * MiniSat::Clause::Decision ( )
static
Clause * MiniSat::Clause::TheoryImplication ( )
static
std::string MiniSat::Clause::toString ( ) const
inline

Definition at line 163 of file minisat_types.h.

References d_data, size(), and MiniSat::Lit::toString().

Referenced by MiniSat::Derivation::printDerivation().

bool MiniSat::Clause::contains ( Lit  l)
inline

Definition at line 174 of file minisat_types.h.

References d_data, and size().

Friends And Related Function Documentation

Clause* Clause_new ( const std::vector< Lit > &  ps,
CVC3::Theorem  theorem,
int  id 
)
friend

Definition at line 44 of file minisat_types.cpp.

Clause* Lemma_new ( const std::vector< Lit > &  ps,
int  id,
int  pushID 
)
friend

Definition at line 49 of file minisat_types.cpp.

Member Data Documentation

unsigned int MiniSat::Clause::d_size_learnt
private

Definition at line 102 of file minisat_types.h.

Referenced by Clause(), learnt(), and size().

int MiniSat::Clause::d_id
private

Definition at line 103 of file minisat_types.h.

Referenced by Clause(), and id().

int MiniSat::Clause::d_pushID
private

Definition at line 104 of file minisat_types.h.

Referenced by Clause(), and pushID().

float MiniSat::Clause::d_activity
private

Definition at line 105 of file minisat_types.h.

Referenced by activity(), Clause(), and setActivity().

CVC3::Theorem MiniSat::Clause::d_theorem
private

Definition at line 107 of file minisat_types.h.

Referenced by Clause(), and getTheorem().

Lit MiniSat::Clause::d_data[1]
private

Definition at line 108 of file minisat_types.h.

Referenced by Clause(), contains(), operator[](), and toString().

Clause * MiniSat::Clause::s_decision = NULL
staticprivate

Definition at line 110 of file minisat_types.h.

Clause * MiniSat::Clause::s_theoryImplication = NULL
staticprivate

Definition at line 111 of file minisat_types.h.


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