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, int id_)
• 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 toLit (std::vector< Lit > &literals) const
• std::string toString () const

Static Public Member Functions

• static int ClauseIDNull ()
• static Clause * Decision ()
• static Clause * TheoryImplication ()

Private Attributes

• uint size_learnt
• Lit data [1]

Static Private Attributes

• static Clause * s_decision
• static Clause * s_theoryImplication

Friends

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

---

Detailed Description

Definition at line 100 of file minisat_types.h.

---

Constructor & Destructor Documentation

MiniSat::Clause::Clause	(	bool	learnt,
		const std::vector< Lit > &	ps,
		int	id_
	)			[inline]

Definition at line 118 of file minisat_types.h.

References activity(), data, id(), and size_learnt.

---

Member Function Documentation

int MiniSat::Clause::size

(

void

)

const [inline]

Definition at line 129 of file minisat_types.h.

References size_learnt.

Referenced by activity(), MiniSat::Solver::addClause(), MiniSat::Solver::analyze(), MiniSat::Solver::analyze_minimize(), MiniSat::Solver::checkClause(), MiniSat::Solver::checkTrail(), MiniSat::Solver::checkWatched(), MiniSat::Derivation::computeRootReason(), MiniSat::Derivation::finish(), MiniSat::Solver::getConflictLevel(), MiniSat::Solver::getImplicationLevel(), id(), MiniSat::Solver::insertClause(), MiniSat::Solver::insertLemma(), MiniSat::Solver::isPermSatisfied(), MiniSat::Solver::isReason(), reduceDB_lt::operator()(), MiniSat::Solver::propagate(), pushID(), MiniSat::Derivation::registerClause(), MiniSat::Solver::remove(), MiniSat::Solver::setPushID(), toLit(), toString(), and MiniSat::Solver::updateConflict().

bool MiniSat::Clause::learnt

(

)

const [inline]

Definition at line 130 of file minisat_types.h.

References size_learnt.

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

Lit MiniSat::Clause::operator[]

(

int

i

)

const [inline]

Definition at line 131 of file minisat_types.h.

References data.

Lit& MiniSat::Clause::operator[]

(

int

i

)

[inline]

Definition at line 132 of file minisat_types.h.

References data.

int& MiniSat::Clause::id

(

)

const [inline]

Definition at line 134 of file minisat_types.h.

References data, and size().

Referenced by MiniSat::Inference::add(), MiniSat::Solver::addClause(), MiniSat::Solver::analyze(), Clause(), MiniSat::Derivation::computeRootReason(), MiniSat::Derivation::finish(), MiniSat::Derivation::printProof(), pushID(), and MiniSat::Derivation::registerClause().

int& MiniSat::Clause::pushID

(

)

const [inline]

Definition at line 139 of file minisat_types.h.

References data, id(), learnt(), and size().

Referenced by MiniSat::Solver::analyze(), MiniSat::Lemma_new(), MiniSat::Derivation::pop(), and MiniSat::Solver::setPushID().

float& MiniSat::Clause::activity

(

)

const [inline]

Definition at line 145 of file minisat_types.h.

References data, DebugAssert, learnt(), and size().

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

void MiniSat::Clause::toLit

(

std::vector< Lit > &

literals

)

const

Definition at line 79 of file minisat_types.cpp.

References data, and size().

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

static int MiniSat::Clause::ClauseIDNull

(

)

[inline, static]

Definition at line 151 of file minisat_types.h.

Clause * MiniSat::Clause::Decision

(

)

[static]

Definition at line 61 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 70 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 159 of file minisat_types.h.

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

---

Friends And Related Function Documentation

Clause* Clause_new	(	const std::vector< Lit > &	ps,
		int	id
	)			[friend]

Definition at line 33 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 45 of file minisat_types.cpp.

---

Member Data Documentation

uint MiniSat::Clause::size_learnt [private]

Definition at line 101 of file minisat_types.h.

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

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

Definition at line 102 of file minisat_types.h.

Referenced by activity(), Clause(), id(), operator[](), pushID(), toLit(), and toString().

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

Definition at line 104 of file minisat_types.h.

Referenced by Decision().

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

Definition at line 105 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

---