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 97 of file cnf.h.

---

Member Typedef Documentation

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

Definition at line 108 of file cnf.h.

---

Constructor & Destructor Documentation

SAT::CNF_Formula::CNF_Formula (   )  [inline]

Definition at line 105 of file cnf.h.

virtual SAT::CNF_Formula::~CNF_Formula (   )  [inline, virtual]

Definition at line 106 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 51 of file cnf.cpp. References addLiteral(), begin(), d_current, end(), newClause(), numClauses(), registerUnit(), 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.

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 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 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(), 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(), copy(), operator+=(), and SAT::CNF_Manager::translateExpr().

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

Definition at line 119 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(), copy(), operator+=(), SAT::CNF_Manager::translateExpr(), and SAT::CNF_Manager::translateExprRec().

Clause& SAT::CNF_Formula::getCurrentClause (   )  [inline]

Definition at line 123 of file cnf.h. References d_current. Referenced by SAT::CNF_Manager::addAssumption(), SAT::CNF_Manager::addLemma(), and SAT::CNF_Manager::translateExpr().

void CNF_Formula::print (   )  const

Definition at line 70 of file cnf.cpp. References begin(), and end().

const CNF_Formula & CNF_Formula::operator+= (  const CNF_Formula &  cnf  )

Definition at line 79 of file cnf.cpp. References addLiteral(), begin(), d_current, end(), newClause(), numClauses(), and registerUnit().

const CNF_Formula & CNF_Formula::operator+= (  const Clause &  c  )

Definition at line 97 of file cnf.cpp. References addLiteral(), SAT::Clause::begin(), d_current, SAT::Clause::end(), SAT::Clause::isUnit(), newClause(), and registerUnit().

---

Member Data Documentation

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

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

---