MiniSat::Clause Class Reference

#include <minisat_types.h>

Collaboration diagram for MiniSat::Clause:

[legend]

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

• 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 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, and d_theorem.

---

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::createProof(), 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::Derivation::printDerivation(), MiniSat::Solver::printDIMACS(), MiniSat::Solver::propagate(), MiniSat::Solver::push(), MiniSat::Derivation::registerClause(), MiniSat::Solver::remove(), MiniSat::Solver::resolveTheoryImplication(), MiniSat::Solver::setPushID(), MiniSat::Solver::simplifyDB(), toLit(), 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(), 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::Solver::addClause(), MiniSat::Solver::analyze(), MiniSat::Derivation::checkDerivation(), 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(), 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(), and reduceDB_lt::operator()().

void MiniSat::Clause::setActivity

(

float

activity

)

[inline]

Definition at line 148 of file minisat_types.h.

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

References d_data, and size().

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 Clause_new, and s_decision.

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 Clause_new, and s_theoryImplication.

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.

Referenced by Decision(), and TheoryImplication().

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[](), toLit(), and toString().

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

Definition at line 110 of file minisat_types.h.

Referenced by Decision().

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

Definition at line 111 of file minisat_types.h.

Referenced by TheoryImplication().

---

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

• minisat_types.h
• minisat_types.cpp