Public Member Functions | Private Member Functions | Private Attributes

SAT::CD_CNF_Formula Class Reference

#include <cnf.h>

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

List of all members.

Public Member Functions

Private Member Functions

Private Attributes


Detailed Description

Definition at line 168 of file cnf.h.


Constructor & Destructor Documentation

SAT::CD_CNF_Formula::CD_CNF_Formula ( CVC3::Context context  )  [inline]

Definition at line 174 of file cnf.h.

References d_numVars.

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

Definition at line 176 of file cnf.h.


Member Function Documentation

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

Implements SAT::CNF_Formula.

Definition at line 172 of file cnf.h.

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

Implements SAT::CNF_Formula.

Definition at line 178 of file cnf.h.

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

Implements SAT::CNF_Formula.

Definition at line 179 of file cnf.h.

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

Implements SAT::CNF_Formula.

Definition at line 180 of file cnf.h.

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

Implements SAT::CNF_Formula.

Definition at line 181 of file cnf.h.

References d_formula, and CVC3::CDList< T >::empty().

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

Implements SAT::CNF_Formula.

Definition at line 182 of file cnf.h.

References d_formula.

unsigned SAT::CD_CNF_Formula::numClauses (  )  const [inline, virtual]
void SAT::CD_CNF_Formula::deleteLast (  )  [inline]

Definition at line 184 of file cnf.h.

References d_formula, and CVC3::CDList< T >::end().

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

void CD_CNF_Formula::newClause (  )  [virtual]

Implements SAT::CNF_Formula.

Definition at line 183 of file cnf.cpp.

References SAT::CNF_Formula::d_current, d_formula, and CVC3::CDList< T >::push_back().

void CD_CNF_Formula::registerUnit (  )  [virtual]

Member Data Documentation

Definition at line 169 of file cnf.h.

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

Definition at line 170 of file cnf.h.

Referenced by CD_CNF_Formula().


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