SAT::CNF_Formula_Impl Class Reference

#include <cnf.h>

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

List of all members.

Public Member Functions

Private Member Functions

Private Attributes


Detailed Description

Definition at line 142 of file cnf.h.


Constructor & Destructor Documentation

SAT::CNF_Formula_Impl::CNF_Formula_Impl (  )  [inline]

Definition at line 149 of file cnf.h.

SAT::CNF_Formula_Impl::CNF_Formula_Impl ( const CNF_Formula cnf  )  [inline]

Definition at line 150 of file cnf.h.

References d_numVars.

SAT::CNF_Formula_Impl::~CNF_Formula_Impl (  )  [inline]

Definition at line 151 of file cnf.h.


Member Function Documentation

void SAT::CNF_Formula_Impl::setNumVars ( unsigned  numVars  )  [inline, private, virtual]

Implements SAT::CNF_Formula.

Definition at line 147 of file cnf.h.

bool SAT::CNF_Formula_Impl::empty (  )  const [inline, virtual]

Implements SAT::CNF_Formula.

Definition at line 153 of file cnf.h.

References SAT::CNF_Formula::copy().

const Clause& SAT::CNF_Formula_Impl::operator[] ( int  i  )  const [inline, virtual]

Implements SAT::CNF_Formula.

Definition at line 154 of file cnf.h.

const_iterator SAT::CNF_Formula_Impl::begin (  )  const [inline, virtual]

Implements SAT::CNF_Formula.

Definition at line 155 of file cnf.h.

Referenced by SAT::DPLLTBasic::addNewClauses(), and SAT::DPLLTBasic::generate_CDB().

const_iterator SAT::CNF_Formula_Impl::end (  )  const [inline, virtual]

Implements SAT::CNF_Formula.

Definition at line 156 of file cnf.h.

References d_formula.

Referenced by SAT::DPLLTBasic::addNewClauses(), and SAT::DPLLTBasic::generate_CDB().

unsigned SAT::CNF_Formula_Impl::numVars (  )  const [inline, virtual]

Implements SAT::CNF_Formula.

Definition at line 157 of file cnf.h.

References d_formula.

Referenced by SAT::DPLLTBasic::addNewClauses(), and SAT::DPLLTBasic::generate_CDB().

unsigned SAT::CNF_Formula_Impl::numClauses (  )  const [inline, virtual]

Implements SAT::CNF_Formula.

Definition at line 158 of file cnf.h.

References d_formula.

void SAT::CNF_Formula_Impl::deleteLast (  )  [inline]

Definition at line 159 of file cnf.h.

References d_formula.

Referenced by CVC3::SearchSat::newUserAssumptionIntHelper().

void CNF_Formula_Impl::newClause (  )  [virtual]

Implements SAT::CNF_Formula.

Definition at line 137 of file cnf.cpp.

References SAT::CNF_Formula::d_current, and d_formula.

Referenced by SAT::DPLLTBasic::checkSat().

void CNF_Formula_Impl::registerUnit (  )  [virtual]
void CNF_Formula_Impl::simplify (  ) 
void CNF_Formula_Impl::reset (  ) 

Member Data Documentation

Definition at line 143 of file cnf.h.

Referenced by registerUnit(), reset(), and simplify().

Definition at line 144 of file cnf.h.

Referenced by deleteLast(), end(), newClause(), numClauses(), numVars(), reset(), and simplify().

Definition at line 145 of file cnf.h.

Referenced by CNF_Formula_Impl(), and reset().


The documentation for this class was generated from the following files:
Generated by  doxygen 1.6.2-20100208