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