CVC3  2.4.1
Public Types | Public Member Functions | Protected Member Functions | Protected Attributes
SAT::CNF_Formula Class Reference

#include <cnf.h>

Inheritance diagram for SAT::CNF_Formula:
SAT::CD_CNF_Formula SAT::CNF_Formula_Impl

List of all members.

Public Types

Public Member Functions

Protected Member Functions

Protected Attributes


Member Typedef Documentation

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::CD_CNF_Formula, and SAT::CNF_Formula_Impl.

Referenced by addLiteral().

void CNF_Formula::copy ( const CNF_Formula cnf) [protected]

Definition at line 60 of file cnf.cpp.

References numClauses(), and d_current.

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

virtual bool SAT::CNF_Formula::empty ( ) const [pure virtual]
virtual const Clause& SAT::CNF_Formula::operator[] ( int  i) const [pure virtual]
virtual const_iterator SAT::CNF_Formula::begin ( ) const [pure virtual]
virtual const_iterator SAT::CNF_Formula::end ( ) const [pure virtual]
virtual unsigned SAT::CNF_Formula::numVars ( ) const [pure virtual]

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

Referenced by addLiteral().

virtual unsigned SAT::CNF_Formula::numClauses ( ) const [pure virtual]

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

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

virtual void SAT::CNF_Formula::newClause ( ) [pure virtual]
virtual void SAT::CNF_Formula::registerUnit ( ) [pure virtual]
void SAT::CNF_Formula::addLiteral ( Lit  l,
bool  invert = false 
) [inline]
Clause& SAT::CNF_Formula::getCurrentClause ( ) [inline]
void CNF_Formula::print ( ) const

Definition at line 85 of file cnf.cpp.

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

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

Definition at line 94 of file cnf.cpp.

References numClauses(), and SAT::Clause::getClauseTheorem().

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

Member Data Documentation

Definition at line 114 of file cnf.h.

Referenced by copy(), addLiteral(), and getCurrentClause().


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