CVC3: MiniSat::Clause Class Reference

CVC3

#include <minisat_types.h>

Collaboration diagram for MiniSat::Clause:

Collaboration graph

List of all members.

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
Lit & operator[] (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 Clause * Decision ()
static Clause * TheoryImplication ()

Private Attributes

Static Private Attributes

static Clause * s_decision = NULL
static Clause * s_theoryImplication = NULL

Friends

Clause * Clause_new (const std::vector< Lit > &ps, CVC3::Theorem theorem, int id)
Clause * Lemma_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]

Definition at line 133 of file minisat_types.h.

References d_size_learnt.

Referenced by MiniSat::Solver::addClause(), MiniSat::Solver::allClausesSatisfied(), MiniSat::Solver::analyze(), MiniSat::Solver::analyze_minimize(), MiniSat::Solver::checkClause(), MiniSat::Solver::checkTrail(), MiniSat::Solver::checkWatched(), MiniSat::Derivation::computeRootReason(), contains(), MiniSat::Derivation::finish(), MiniSat::Solver::getConflictLevel(), MiniSat::Solver::getImplicationLevel(), MiniSat::Solver::insertClause(), MiniSat::Solver::insertLemma(), MiniSat::Solver::isPermSatisfied(), MiniSat::Solver::isReason(), reduceDB_lt::operator()(), MiniSat::Solver::pop(), MiniSat::Derivation::pop(), MiniSat::Solver::printDIMACS(), MiniSat::Solver::propagate(), MiniSat::Solver::push(), MiniSat::Derivation::registerClause(), MiniSat::Solver::remove(), MiniSat::Solver::resolveTheoryImplication(), MiniSat::Solver::setPushID(), MiniSat::Solver::simplifyDB(), toString(), and MiniSat::Solver::updateConflict().

bool MiniSat::Clause::learnt ( ) const [inline]

Definition at line 134 of file minisat_types.h.

References d_size_learnt.

Referenced by activity(), MiniSat::Solver::addClause(), Clause(), MiniSat::Solver::insertClause(), MiniSat::Solver::remove(), and setActivity().

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]

Definition at line 138 of file minisat_types.h.

References d_id.

Referenced by MiniSat::Inference::add(), MiniSat::Solver::addClause(), MiniSat::Solver::analyze(), MiniSat::Derivation::checkDerivation(), Clause(), MiniSat::Derivation::computeRootReason(), MiniSat::Derivation::createProof(), MiniSat::Derivation::finish(), MiniSat::Derivation::pop(), MiniSat::Derivation::printDerivation(), MiniSat::Solver::push(), and MiniSat::Derivation::registerClause().

int MiniSat::Clause::pushID ( ) const [inline]

Definition at line 143 of file minisat_types.h.

References d_pushID.

Referenced by MiniSat::Solver::analyze(), Clause(), MiniSat::Solver::isPermSatisfied(), MiniSat::Solver::pop(), MiniSat::Derivation::pop(), MiniSat::Solver::push(), MiniSat::Solver::setPushID(), and MiniSat::Solver::simplifyDB().

float MiniSat::Clause::activity ( ) const [inline]

Definition at line 144 of file minisat_types.h.

References d_activity, DebugAssert, and learnt().

Referenced by MiniSat::Solver::claBumpActivity(), MiniSat::Solver::insertLemma(), reduceDB_lt::operator()(), and setActivity().

void MiniSat::Clause::setActivity ( float activity ) [inline]

Definition at line 148 of file minisat_types.h.

References activity(), d_activity, DebugAssert, and learnt().

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

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 ( ) [inline, static]

Definition at line 155 of file minisat_types.h.

Clause * MiniSat::Clause::Decision ( ) [static]

Definition at line 54 of file minisat_types.cpp.

References MiniSat::Clause_new().

Referenced by MiniSat::Solver::analyze(), MiniSat::Solver::analyze_minimize(), MiniSat::Solver::analyze_removable(), MiniSat::Solver::assume(), MiniSat::Solver::checkTrail(), MiniSat::Derivation::computeRootReason(), MiniSat::Solver::printDIMACS(), MiniSat::Solver::printState(), MiniSat::Solver::protocolPropagation(), and MiniSat::Solver::setPushID().

Clause * MiniSat::Clause::TheoryImplication ( ) [static]

Definition at line 63 of file minisat_types.cpp.

References MiniSat::Clause_new().

Referenced by MiniSat::Solver::analyze(), MiniSat::Solver::analyze_removable(), MiniSat::Solver::checkTrail(), MiniSat::Solver::getReason(), MiniSat::Solver::push(), MiniSat::Solver::resolveTheoryImplication(), MiniSat::Solver::search(), and MiniSat::Solver::setPushID().

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 [static, private]

Definition at line 110 of file minisat_types.h.

Clause * MiniSat::Clause::s_theoryImplication = NULL [static, private]

Definition at line 111 of file minisat_types.h.

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