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


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 ( ) [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 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::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]
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

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: