CVC3
2.4.1
|
#include <cnf.h>
Public Types | |
typedef std::deque< Clause > ::const_iterator | const_iterator |
Public Member Functions | |
CNF_Formula () | |
virtual | ~CNF_Formula () |
virtual bool | empty () const =0 |
virtual const Clause & | operator[] (int i) const =0 |
virtual const_iterator | begin () const =0 |
virtual const_iterator | end () const =0 |
virtual unsigned | numVars () const =0 |
virtual unsigned | numClauses () const =0 |
virtual void | newClause ()=0 |
virtual void | registerUnit ()=0 |
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) |
Protected Member Functions | |
virtual void | setNumVars (unsigned numVars)=0 |
void | copy (const CNF_Formula &cnf) |
Protected Attributes | |
Clause * | d_current |
typedef std::deque<Clause>::const_iterator SAT::CNF_Formula::const_iterator |
|
protectedpure virtual |
Referenced by addLiteral().
|
protected |
Definition at line 60 of file cnf.cpp.
References d_current, and numClauses().
Referenced by SAT::CNF_Formula_Impl::CNF_Formula_Impl().
|
pure virtual |
Implemented in SAT::CD_CNF_Formula, and SAT::CNF_Formula_Impl.
Referenced by SAT::CNF_Manager::convertLemma(), and CVC3::SearchSat::getExplanation().
|
pure virtual |
Implemented in SAT::CD_CNF_Formula, and SAT::CNF_Formula_Impl.
|
pure virtual |
Implemented in SAT::CD_CNF_Formula, and SAT::CNF_Formula_Impl.
Referenced by SAT::DPLLTBasic::addAssertion(), SAT::DPLLTMiniSat::addAssertion(), and MiniSat::Solver::addFormula().
|
pure virtual |
Implemented in SAT::CD_CNF_Formula, and SAT::CNF_Formula_Impl.
Referenced by SAT::DPLLTBasic::addAssertion(), SAT::DPLLTMiniSat::addAssertion(), and MiniSat::Solver::addFormula().
|
pure virtual |
Implemented in SAT::CD_CNF_Formula, and SAT::CNF_Formula_Impl.
Referenced by addLiteral().
|
pure virtual |
Implemented in SAT::CD_CNF_Formula, and SAT::CNF_Formula_Impl.
Referenced by copy(), and operator+=().
|
pure virtual |
|
pure virtual |
Implemented in SAT::CD_CNF_Formula, and SAT::CNF_Formula_Impl.
Referenced by SAT::CNF_Manager::addAssumption(), SAT::CNF_Manager::addLemma(), SAT::CNF_Manager::convertLemma(), and SAT::CNF_Manager::translateExpr().
|
inline |
Definition at line 134 of file cnf.h.
References SAT::Clause::addLiteral(), d_current, SAT::Lit::getVar(), SAT::Lit::isVar(), numVars(), and setNumVars().
Referenced by SAT::CNF_Manager::addAssumption(), SAT::CNF_Manager::addLemma(), SAT::DPLLTBasic::checkSat(), SAT::CNF_Manager::convertLemma(), SAT::CNF_Manager::translateExpr(), and SAT::CNF_Manager::translateExprRec().
|
inline |
Definition at line 138 of file cnf.h.
References d_current.
Referenced by SAT::CNF_Manager::addAssumption(), SAT::CNF_Manager::addLemma(), SAT::CNF_Manager::convertLemma(), SAT::CNF_Manager::translateExpr(), and SAT::CNF_Manager::translateExprRec().
void CNF_Formula::print | ( | ) | const |
Definition at line 85 of file cnf.cpp.
References SAT::Clause::print().
Referenced by MiniSat::Solver::push(), and MiniSat::Solver::search().
const CNF_Formula & CNF_Formula::operator+= | ( | const CNF_Formula & | cnf | ) |
Definition at line 94 of file cnf.cpp.
References SAT::Clause::getClauseTheorem(), and numClauses().
const CNF_Formula & CNF_Formula::operator+= | ( | const Clause & | c | ) |
Definition at line 117 of file cnf.cpp.
References SAT::Clause::begin(), SAT::Clause::end(), SAT::Clause::getClauseTheorem(), and SAT::Clause::isUnit().
|
protected |
Definition at line 114 of file cnf.h.
Referenced by addLiteral(), copy(), and getCurrentClause().