SAT::Clause Class Reference

#include <cnf.h>

List of all members.

Public Types

• typedef std::vector< Lit
  >::const_iterator const_iterator

Public Member Functions

• Clause ()
• const_iterator begin () const
• const_iterator end () const
• void clear ()
• unsigned size () const
• void addLiteral (Lit l)
• unsigned getMaxVar () const
• int getId () const
• bool isSatisfied () const
• bool isUnit () const
• bool isNull () const
• void setId (int id)
• void setSatisfied ()
• void setUnit ()
• void print () const

Private Attributes

• int d_id:30
• int d_satisfied:1
• int d_unit:1
• std::vector< Lit > d_lits

---

Detailed Description

Definition at line 65 of file cnf.h.

---

Member Typedef Documentation

typedef std::vector<Lit>::const_iterator SAT::Clause::const_iterator

Definition at line 76 of file cnf.h.

---

Constructor & Destructor Documentation

SAT::Clause::Clause (   )  [inline]

Definition at line 74 of file cnf.h.

---

Member Function Documentation

const_iterator SAT::Clause::begin (   )  const [inline]

Definition at line 77 of file cnf.h. References d_lits. Referenced by SAT::DPLLTBasic::addNewClause(), SAT::CNF_Formula::operator+=(), and SAT::CNF_Formula_Impl::registerUnit().

const_iterator SAT::Clause::end (   )  const [inline]

Definition at line 78 of file cnf.h. References d_lits. Referenced by SAT::DPLLTBasic::addNewClause(), and SAT::CNF_Formula::operator+=().

void SAT::Clause::clear (   )  [inline]

Definition at line 80 of file cnf.h. References d_id, d_lits, d_satisfied, and d_unit. Referenced by SAT::DPLLTBasic::generate_CDB().

unsigned SAT::Clause::size (   )  const [inline]

Definition at line 81 of file cnf.h. References d_lits. Referenced by SAT::DPLLTBasic::addNewClause(), SAT::CNF_Manager::convertLemma(), SAT::CD_CNF_Formula::registerUnit(), and SAT::CNF_Formula_Impl::registerUnit().

void SAT::Clause::addLiteral (  Lit  l  )  [inline]

Definition at line 82 of file cnf.h. References d_lits, and d_satisfied. Referenced by SAT::CNF_Formula::addLiteral(), and SAT::CNF_Manager::convertLemma().

unsigned SAT::Clause::getMaxVar (   )  const

Referenced by SAT::DPLLTBasic::addNewClause().

int SAT::Clause::getId (   )  const [inline]

Definition at line 85 of file cnf.h. References d_id.

bool SAT::Clause::isSatisfied (   )  const [inline]

Definition at line 86 of file cnf.h. References d_satisfied.

bool SAT::Clause::isUnit (   )  const [inline]

Definition at line 87 of file cnf.h. References d_unit. Referenced by SAT::CNF_Formula::operator+=().

bool SAT::Clause::isNull (   )  const [inline]

Definition at line 88 of file cnf.h. References d_lits.

void SAT::Clause::setId (  int  id  )  [inline]

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

void SAT::Clause::setSatisfied (   )  [inline]

Definition at line 91 of file cnf.h. References d_satisfied.

void SAT::Clause::setUnit (   )  [inline]

Definition at line 92 of file cnf.h. References d_unit. Referenced by SAT::CNF_Manager::convertLemma(), SAT::CD_CNF_Formula::registerUnit(), and SAT::CNF_Formula_Impl::registerUnit().

void SAT::Clause::print (   )  const

---

Member Data Documentation

int SAT::Clause::d_id [private]

If d_id is 0 then the clause is a translation clause and its theorem can be figured out lazily. Otherwise, d_id gives the index into d_theorems for the theorem justifying this clause. Definition at line 69 of file cnf.h. Referenced by clear(), getId(), and setId().

int SAT::Clause::d_satisfied [private]

Definition at line 70 of file cnf.h. Referenced by addLiteral(), clear(), isSatisfied(), and setSatisfied().

int SAT::Clause::d_unit [private]

Definition at line 71 of file cnf.h. Referenced by clear(), isUnit(), and setUnit().

std::vector<Lit> SAT::Clause::d_lits [private]

Definition at line 72 of file cnf.h. Referenced by addLiteral(), begin(), clear(), end(), isNull(), and size().

---

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

• cnf.h

---