SAT::CNF_Formula Class Reference

#include <cnf.h>

Inheritance diagram for SAT::CNF_Formula:

Inheritance graph
[legend]
Collaboration diagram for SAT::CNF_Formula:

Collaboration graph
[legend]
List of all members.

Public Types

Public Member Functions

Protected Member Functions

Protected Attributes


Detailed Description

Definition at line 107 of file cnf.h.


Member Typedef Documentation

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

Definition at line 118 of file cnf.h.


Constructor & Destructor Documentation

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

Definition at line 115 of file cnf.h.

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

Definition at line 116 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(), 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 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(), 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 129 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 133 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 79 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 88 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 106 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 109 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:
Generated on Tue Jul 3 14:42:21 2007 for CVC3 by  doxygen 1.5.1