#include <cnf.h>
Inheritance diagram for SAT::CNF_Formula:
Definition at line 107 of file cnf.h.
typedef std::deque<Clause>::const_iterator SAT::CNF_Formula::const_iterator |
virtual void SAT::CNF_Formula::setNumVars | ( | unsigned | numVars | ) | [protected, pure virtual] |
Implemented in SAT::CNF_Formula_Impl, and SAT::CD_CNF_Formula.
Referenced by addLiteral(), and copy().
void CNF_Formula::copy | ( | const CNF_Formula & | cnf | ) | [protected] |
Definition at line 60 of file cnf.cpp.
References addLiteral(), begin(), d_current, end(), newClause(), numClauses(), registerUnit(), and setNumVars().
Referenced by SAT::CNF_Formula_Impl::CNF_Formula_Impl().
virtual bool SAT::CNF_Formula::empty | ( | ) | const [pure virtual] |
Implemented in SAT::CNF_Formula_Impl, and SAT::CD_CNF_Formula.
virtual const Clause& SAT::CNF_Formula::operator[] | ( | int | i | ) | const [pure virtual] |
Implemented in SAT::CNF_Formula_Impl, and SAT::CD_CNF_Formula.
virtual const_iterator SAT::CNF_Formula::begin | ( | ) | const [pure virtual] |
Implemented in SAT::CNF_Formula_Impl, and SAT::CD_CNF_Formula.
Referenced by SAT::DPLLTMiniSat::addAssertion(), SAT::DPLLTBasic::addAssertion(), MiniSat::Solver::addFormula(), copy(), operator+=(), and print().
virtual const_iterator SAT::CNF_Formula::end | ( | ) | const [pure virtual] |
Implemented in SAT::CNF_Formula_Impl, and SAT::CD_CNF_Formula.
Referenced by SAT::DPLLTMiniSat::addAssertion(), SAT::DPLLTBasic::addAssertion(), MiniSat::Solver::addFormula(), copy(), operator+=(), and print().
virtual unsigned SAT::CNF_Formula::numVars | ( | ) | const [pure virtual] |
virtual unsigned SAT::CNF_Formula::numClauses | ( | ) | const [pure virtual] |
Implemented in SAT::CNF_Formula_Impl, and SAT::CD_CNF_Formula.
Referenced by copy(), and operator+=().
virtual void SAT::CNF_Formula::newClause | ( | ) | [pure virtual] |
Implemented in SAT::CNF_Formula_Impl, and SAT::CD_CNF_Formula.
Referenced by SAT::CNF_Manager::addAssumption(), SAT::CNF_Manager::addLemma(), copy(), operator+=(), SAT::CNF_Manager::translateExpr(), and SAT::CNF_Manager::translateExprRec().
virtual void SAT::CNF_Formula::registerUnit | ( | ) | [pure virtual] |
Implemented in SAT::CNF_Formula_Impl, and SAT::CD_CNF_Formula.
Referenced by SAT::CNF_Manager::addAssumption(), SAT::CNF_Manager::addLemma(), copy(), operator+=(), and SAT::CNF_Manager::translateExpr().
void SAT::CNF_Formula::addLiteral | ( | Lit | l, | |
bool | invert = false | |||
) | [inline] |
Definition at line 129 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(), copy(), operator+=(), SAT::CNF_Manager::translateExpr(), and SAT::CNF_Manager::translateExprRec().
Clause& SAT::CNF_Formula::getCurrentClause | ( | ) | [inline] |
Definition at line 133 of file cnf.h.
References d_current.
Referenced by SAT::CNF_Manager::addAssumption(), SAT::CNF_Manager::addLemma(), and SAT::CNF_Manager::translateExpr().
void CNF_Formula::print | ( | ) | const |
Definition at line 79 of file cnf.cpp.
References begin(), and end().
Referenced by MiniSat::Solver::push(), and MiniSat::Solver::search().
const CNF_Formula & CNF_Formula::operator+= | ( | const CNF_Formula & | cnf | ) |
Definition at line 88 of file cnf.cpp.
References addLiteral(), begin(), d_current, end(), newClause(), numClauses(), and registerUnit().
const CNF_Formula & CNF_Formula::operator+= | ( | const Clause & | c | ) |
Definition at line 106 of file cnf.cpp.
References addLiteral(), SAT::Clause::begin(), d_current, SAT::Clause::end(), SAT::Clause::isUnit(), newClause(), and registerUnit().
Clause* SAT::CNF_Formula::d_current [protected] |
Definition at line 109 of file cnf.h.
Referenced by addLiteral(), copy(), getCurrentClause(), SAT::CD_CNF_Formula::newClause(), SAT::CNF_Formula_Impl::newClause(), operator+=(), SAT::CD_CNF_Formula::registerUnit(), SAT::CNF_Formula_Impl::registerUnit(), and SAT::CNF_Formula_Impl::reset().