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

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

Public Member Functions

 CNF_Formula ()
virtual ~CNF_Formula ()
virtual bool empty () const =0
virtual const Clauseoperator[] (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)
ClausegetCurrentClause ()
void print () const
const CNF_Formulaoperator+= (const CNF_Formula &cnf)
const CNF_Formulaoperator+= (const Clause &c)

Protected Member Functions

virtual void setNumVars (unsigned numVars)=0
void copy (const CNF_Formula &cnf)

Protected Attributes

Claused_current

Detailed Description

Definition at line 112 of file cnf.h.


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

Definition at line 121 of file cnf.h.


Member Function Documentation

virtual void SAT::CNF_Formula::setNumVars ( unsigned  numVars)
protectedpure 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 d_current, and numClauses().

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.

References SAT::Clause::print().

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 SAT::Clause::getClauseTheorem(), and numClauses().

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

Member Data Documentation

Clause* SAT::CNF_Formula::d_current
protected

Definition at line 114 of file cnf.h.

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


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