SAT::CNF_Formula Class Reference

#include <cnf.h>

Inheritance diagram for SAT::CNF_Formula:

[legend]

Collaboration diagram for SAT::CNF_Formula:

[legend]

List of all members.

Public Types

• typedef std::deque< Clause >
  ::const_iterator const_iterator

Public Member Functions

• CNF_Formula ()
• virtual ~CNF_Formula ()
• virtual bool empty () const =0
• virtual const Clause & operator[] (int i) const =0
• virtual const_iterator begin () const =0
• virtual const_iterator end () const =0
• virtual unsigned numVars () const =0
• virtual unsigned numClauses () const =0
• virtual void newClause ()=0
• virtual void registerUnit ()=0
• void addLiteral (Lit l, bool invert=false)
• Clause & getCurrentClause ()
• void print () const
• const CNF_Formula & operator+= (const CNF_Formula &cnf)
• const CNF_Formula & operator+= (const Clause &c)

Protected Member Functions

• virtual void setNumVars (unsigned numVars)=0
• void copy (const CNF_Formula &cnf)

Protected Attributes

• Clause * d_current

---

Detailed Description

Definition at line 112 of file cnf.h.

---

Member Typedef Documentation

typedef std::deque<Clause>::const_iterator SAT::CNF_Formula::const_iterator

Definition at line 123 of file cnf.h.

---

Constructor & Destructor Documentation

SAT::CNF_Formula::CNF_Formula

(

)

[inline]

Definition at line 120 of file cnf.h.

virtual SAT::CNF_Formula::~CNF_Formula

(

)

[inline, virtual]

Definition at line 121 of file cnf.h.

---

Member Function Documentation

virtual void SAT::CNF_Formula::setNumVars

(

unsigned

numVars

)

[protected, pure virtual]

Implemented in SAT::CNF_Formula_Impl, and SAT::CD_CNF_Formula.

Referenced by addLiteral(), and copy().

void CNF_Formula::copy

(

const CNF_Formula &

cnf

)

[protected]

Definition at line 60 of file cnf.cpp.

References addLiteral(), begin(), d_current, end(), getCurrentClause(), newClause(), numClauses(), registerUnit(), SAT::Clause::setClauseTheorem(), and setNumVars().

Referenced by SAT::CNF_Formula_Impl::CNF_Formula_Impl().

virtual bool SAT::CNF_Formula::empty

(

)

const [pure virtual]

Implemented in SAT::CNF_Formula_Impl, and SAT::CD_CNF_Formula.

Referenced by SAT::CNF_Manager::convertLemma(), and CVC3::SearchSat::getExplanation().

virtual const Clause& SAT::CNF_Formula::operator[]

(

int

i

)

const [pure virtual]

Implemented in SAT::CNF_Formula_Impl, and SAT::CD_CNF_Formula.

virtual const_iterator SAT::CNF_Formula::begin

(

)

const [pure virtual]

Implemented in SAT::CNF_Formula_Impl, and SAT::CD_CNF_Formula.

Referenced by SAT::DPLLTMiniSat::addAssertion(), SAT::DPLLTBasic::addAssertion(), MiniSat::Solver::addFormula(), copy(), operator+=(), and print().

virtual const_iterator SAT::CNF_Formula::end

(

)

const [pure virtual]

Implemented in SAT::CNF_Formula_Impl, and SAT::CD_CNF_Formula.

Referenced by SAT::DPLLTMiniSat::addAssertion(), SAT::DPLLTBasic::addAssertion(), MiniSat::Solver::addFormula(), copy(), operator+=(), and print().

virtual unsigned SAT::CNF_Formula::numVars

(

)

const [pure virtual]

Implemented in SAT::CNF_Formula_Impl, and SAT::CD_CNF_Formula.

Referenced by addLiteral().

virtual unsigned SAT::CNF_Formula::numClauses

(

)

const [pure virtual]

Implemented in SAT::CNF_Formula_Impl, and SAT::CD_CNF_Formula.

Referenced by copy(), and operator+=().

virtual void SAT::CNF_Formula::newClause

(

)

[pure virtual]

Implemented in SAT::CNF_Formula_Impl, and SAT::CD_CNF_Formula.

Referenced by SAT::CNF_Manager::addAssumption(), SAT::CNF_Manager::addLemma(), SAT::CNF_Manager::convertLemma(), copy(), operator+=(), SAT::CNF_Manager::translateExpr(), and SAT::CNF_Manager::translateExprRec().

virtual void SAT::CNF_Formula::registerUnit

(

)

[pure virtual]

Implemented in SAT::CNF_Formula_Impl, and SAT::CD_CNF_Formula.

Referenced by SAT::CNF_Manager::addAssumption(), SAT::CNF_Manager::addLemma(), SAT::CNF_Manager::convertLemma(), copy(), operator+=(), and SAT::CNF_Manager::translateExpr().

void SAT::CNF_Formula::addLiteral	(	Lit	l,
		bool	invert = false
	)			[inline]

Definition at line 134 of file cnf.h.

References SAT::Clause::addLiteral(), d_current, SAT::Lit::getVar(), SAT::Lit::isVar(), numVars(), and setNumVars().

Referenced by SAT::CNF_Manager::addAssumption(), SAT::CNF_Manager::addLemma(), SAT::DPLLTBasic::checkSat(), SAT::CNF_Manager::convertLemma(), copy(), operator+=(), SAT::CNF_Manager::translateExpr(), and SAT::CNF_Manager::translateExprRec().

Clause& SAT::CNF_Formula::getCurrentClause

(

)

[inline]

Definition at line 138 of file cnf.h.

References d_current.

Referenced by SAT::CNF_Manager::addAssumption(), SAT::CNF_Manager::addLemma(), SAT::CNF_Manager::convertLemma(), copy(), operator+=(), SAT::CNF_Manager::translateExpr(), and SAT::CNF_Manager::translateExprRec().

void CNF_Formula::print

(

)

const

Definition at line 85 of file cnf.cpp.

References begin(), and end().

Referenced by MiniSat::Solver::push(), and MiniSat::Solver::search().

const CNF_Formula & CNF_Formula::operator+=

(

const CNF_Formula &

cnf

)

Definition at line 94 of file cnf.cpp.

References addLiteral(), begin(), d_current, end(), SAT::Clause::getClauseTheorem(), getCurrentClause(), newClause(), numClauses(), registerUnit(), and SAT::Clause::setClauseTheorem().

const CNF_Formula & CNF_Formula::operator+=

(

const Clause &

c

)

Definition at line 117 of file cnf.cpp.

References addLiteral(), SAT::Clause::begin(), d_current, SAT::Clause::end(), SAT::Clause::getClauseTheorem(), getCurrentClause(), SAT::Clause::isUnit(), newClause(), registerUnit(), and SAT::Clause::setClauseTheorem().

---

Member Data Documentation

Clause* SAT::CNF_Formula::d_current [protected]

Definition at line 114 of file cnf.h.

Referenced by addLiteral(), copy(), getCurrentClause(), SAT::CD_CNF_Formula::newClause(), SAT::CNF_Formula_Impl::newClause(), operator+=(), SAT::CD_CNF_Formula::registerUnit(), SAT::CNF_Formula_Impl::registerUnit(), and SAT::CNF_Formula_Impl::reset().

---

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

• cnf.h
• cnf.cpp