CVC3
Public Member Functions | Private Member Functions | Private Attributes

SAT::CNF_Formula_Impl Class Reference

#include <cnf.h>

Inherits SAT::CNF_Formula.

Collaboration diagram for SAT::CNF_Formula_Impl:
Collaboration graph
[legend]

List of all members.

Public Member Functions

Private Member Functions

Private Attributes


Detailed Description

Definition at line 146 of file cnf.h.


Constructor & Destructor Documentation

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

Definition at line 153 of file cnf.h.

References SAT::CNF_Formula::copy().

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

Definition at line 154 of file cnf.h.

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

Definition at line 155 of file cnf.h.

References d_formula.


Member Function Documentation

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

Implements SAT::CNF_Formula.

Definition at line 151 of file cnf.h.

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

Implements SAT::CNF_Formula.

Definition at line 157 of file cnf.h.

References d_formula.

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

Implements SAT::CNF_Formula.

Definition at line 158 of file cnf.h.

References d_formula.

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

Implements SAT::CNF_Formula.

Definition at line 159 of file cnf.h.

References d_formula.

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

References d_numVars.

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

References d_formula, and DebugAssert.

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

Definition at line 163 of file cnf.h.

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

void CNF_Formula_Impl::newClause ( ) [virtual]

Implements SAT::CNF_Formula.

Definition at line 137 of file cnf.cpp.

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

void CNF_Formula_Impl::registerUnit ( ) [virtual]

Implements SAT::CNF_Formula.

Definition at line 144 of file cnf.cpp.

References DebugAssert, and SAT::Lit::getID().

void CNF_Formula_Impl::simplify ( )
void CNF_Formula_Impl::reset ( )

Definition at line 174 of file cnf.cpp.

Referenced by MiniSat::Solver::push(), SATDeductionHook(), and MiniSat::Solver::search().


Member Data Documentation

Definition at line 147 of file cnf.h.

Definition at line 148 of file cnf.h.

Referenced by begin(), empty(), numClauses(), numVars(), operator[](), and ~CNF_Formula_Impl().

Definition at line 149 of file cnf.h.

Referenced by end().


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