CVC3  2.4.1
Public Types | Public Member Functions | Protected Member Functions | Protected Attributes | List of all members
SAT::CNF_Formula Class Referenceabstract

#include <cnf.h>

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

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: