MiniSat::Inference Class Reference

#include <minisat_derivation.h>

Collaboration diagram for MiniSat::Inference:

[legend]List of all members.

Public Types

• typedef std::vector< std::pair<
  Lit, int > > TSteps

Public Member Functions

• Inference (int clauseID)
• void add (Lit lit, int clauseID)
• void add (Lit lit, Clause *clause)
• int getStart () const
• const TSteps & getSteps () const
• std::string toString () const

Private Attributes

• int d_start
• TSteps d_steps

---

Detailed Description

Definition at line 35 of file minisat_derivation.h.

---

Member Typedef Documentation

typedef std::vector<std::pair<Lit, int> > MiniSat::Inference::TSteps

Definition at line 37 of file minisat_derivation.h.

---

Constructor & Destructor Documentation

MiniSat::Inference::Inference

(

int

clauseID

)

[inline]

Definition at line 49 of file minisat_derivation.h.

---

Member Function Documentation

void MiniSat::Inference::add	(	Lit	lit,
		int	clauseID
	)			[inline]

Definition at line 51 of file minisat_derivation.h.

References d_steps.

Referenced by add(), MiniSat::Solver::addClause(), MiniSat::Solver::analyze(), MiniSat::Solver::analyze_minimize(), MiniSat::Derivation::computeRootReason(), and MiniSat::Derivation::finish().

void MiniSat::Inference::add	(	Lit	lit,
		Clause *	clause
	)			[inline]

Definition at line 55 of file minisat_derivation.h.

References add(), and MiniSat::Clause::id().

int MiniSat::Inference::getStart

(

)

const [inline]

Definition at line 59 of file minisat_derivation.h.

References d_start.

Referenced by MiniSat::Derivation::printProof(), and toString().

const TSteps& MiniSat::Inference::getSteps

(

)

const [inline]

Definition at line 63 of file minisat_derivation.h.

References d_steps.

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

std::string Inference::toString

(

)

const

Definition at line 30 of file minisat_derivation.cpp.

References d_steps, and getStart().

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

---

Member Data Documentation

int MiniSat::Inference::d_start [private]

Definition at line 41 of file minisat_derivation.h.

Referenced by getStart().

TSteps MiniSat::Inference::d_steps [private]

Definition at line 46 of file minisat_derivation.h.

Referenced by add(), getSteps(), and toString().

---

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

• minisat_derivation.h
• minisat_derivation.cpp

---