CVC3
|
#include <cnf.h>
Inherits SAT::CNF_Formula.
Public Member Functions | |
CD_CNF_Formula (CVC3::Context *context) | |
~CD_CNF_Formula () | |
bool | empty () const |
const Clause & | operator[] (int i) const |
const_iterator | begin () const |
const_iterator | end () const |
unsigned | numVars () const |
unsigned | numClauses () const |
void | deleteLast () |
void | newClause () |
void | registerUnit () |
![]() | |
CNF_Formula () | |
virtual | ~CNF_Formula () |
void | addLiteral (Lit l, bool invert=false) |
Clause & | getCurrentClause () |
void | print () const |
const CNF_Formula & | operator+= (const CNF_Formula &cnf) |
const CNF_Formula & | operator+= (const Clause &c) |
Private Member Functions | |
void | setNumVars (unsigned numVars) |
Private Attributes | |
CVC3::CDList< Clause > | d_formula |
CVC3::CDO< unsigned > | d_numVars |
Additional Inherited Members | |
![]() | |
typedef std::deque< Clause > ::const_iterator | const_iterator |
![]() | |
void | copy (const CNF_Formula &cnf) |
![]() | |
Clause * | d_current |
|
inline |
|
inlineprivatevirtual |
Implements SAT::CNF_Formula.
|
inlinevirtual |
Implements SAT::CNF_Formula.
Definition at line 181 of file cnf.h.
References d_formula, and CVC3::CDList< T >::empty().
|
inlinevirtual |
|
inlinevirtual |
Implements SAT::CNF_Formula.
Definition at line 183 of file cnf.h.
References CVC3::CDList< T >::begin(), and d_formula.
|
inlinevirtual |
Implements SAT::CNF_Formula.
Definition at line 184 of file cnf.h.
References d_formula, and CVC3::CDList< T >::end().
|
inlinevirtual |
Implements SAT::CNF_Formula.
Definition at line 185 of file cnf.h.
References d_numVars, and CVC3::CDO< T >::get().
Referenced by setNumVars().
|
inlinevirtual |
Implements SAT::CNF_Formula.
Definition at line 186 of file cnf.h.
References d_formula, and CVC3::CDList< T >::size().
Referenced by SAT::DPLLTBasic::checkSat(), and SAT::DPLLTBasic::continueCheck().
|
inline |
Definition at line 187 of file cnf.h.
References d_formula, and CVC3::CDList< T >::pop_back().
|
virtual |
Implements SAT::CNF_Formula.
|
virtual |
|
private |
Definition at line 172 of file cnf.h.
Referenced by begin(), deleteLast(), empty(), end(), numClauses(), and operator[]().
|
private |
Definition at line 173 of file cnf.h.
Referenced by numVars(), and setNumVars().