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 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 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().

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.

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::Lit::getVar(), and SAT::Lit::isVar().

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().

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

Definition at line 138 of file cnf.h.

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 copy(), 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 Wed Nov 18 16:18:51 2009 for CVC3 by  doxygen 1.5.2