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 109 of file cnf.h.


Member Typedef Documentation

Definition at line 120 of file cnf.h.


Constructor & Destructor Documentation

SAT::CNF_Formula::CNF_Formula (  )  [inline]

Definition at line 117 of file cnf.h.

virtual SAT::CNF_Formula::~CNF_Formula (  )  [inline, virtual]

Definition at line 118 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(), and getCurrentClause().

void CNF_Formula::copy ( const CNF_Formula cnf  )  [protected]
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 unsigned SAT::CNF_Formula::numVars (  )  const [pure virtual]

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

Referenced by getCurrentClause().

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

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  ) 

Member Data Documentation


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