CVC3
2.4.1
|
#include <cnf.h>
Public Member Functions | |
CNF_Formula_Impl () | |
CNF_Formula_Impl (const CNF_Formula &cnf) | |
~CNF_Formula_Impl () | |
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 () |
void | simplify () |
void | reset () |
![]() | |
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 | |
std::hash_map< int, bool > | d_lits |
std::deque< Clause > | d_formula |
unsigned | d_numVars |
Additional Inherited Members | |
![]() | |
typedef std::deque< Clause > ::const_iterator | const_iterator |
![]() | |
void | copy (const CNF_Formula &cnf) |
![]() | |
Clause * | d_current |
|
inline |
Definition at line 153 of file cnf.h.
References SAT::CNF_Formula::copy().
|
inlineprivatevirtual |
Implements SAT::CNF_Formula.
|
inlinevirtual |
|
inlinevirtual |
|
inlinevirtual |
Implements SAT::CNF_Formula.
Definition at line 158 of file cnf.h.
References d_formula.
Referenced by SAT::DPLLTBasic::addNewClauses(), and SAT::DPLLTBasic::generate_CDB().
|
inlinevirtual |
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().
|
inlinevirtual |
Implements SAT::CNF_Formula.
Definition at line 160 of file cnf.h.
References d_numVars.
Referenced by SAT::DPLLTBasic::addNewClauses(), SAT::DPLLTBasic::generate_CDB(), and setNumVars().
|
inlinevirtual |
|
inline |
Definition at line 162 of file cnf.h.
References d_formula, and DebugAssert.
Referenced by CVC3::SearchSat::newUserAssumptionIntHelper().
|
virtual |
Implements SAT::CNF_Formula.
Definition at line 137 of file cnf.cpp.
Referenced by SAT::DPLLTBasic::checkSat().
|
virtual |
Implements SAT::CNF_Formula.
Definition at line 144 of file cnf.cpp.
References DebugAssert, and SAT::Lit::getID().
void CNF_Formula_Impl::simplify | ( | ) |
Definition at line 153 of file cnf.cpp.
References Hash::hash_map< _Key, _Data, _HashFcn, _EqualKey >::end(), and Hash::hash_map< _Key, _Data, _HashFcn, _EqualKey >::find().
Referenced by SAT::DPLLTBasic::addNewClauses(), and SAT::DPLLTBasic::generate_CDB().
void CNF_Formula_Impl::reset | ( | ) |
Definition at line 174 of file cnf.cpp.
Referenced by MiniSat::Solver::push(), SATDeductionHook(), and MiniSat::Solver::search().
|
private |
|
private |
Definition at line 147 of file cnf.h.
Referenced by begin(), deleteLast(), empty(), end(), numClauses(), and operator[]().
|
private |
Definition at line 148 of file cnf.h.
Referenced by numVars(), and setNumVars().