typedef std::vector<int>::size_type MiniSat::size_type |
Definition at line 110 of file minisat_solver.h.
typedef int MiniSat::Var |
Definition at line 55 of file minisat_types.h.
static T MiniSat::min | ( | T | x, | |
T | y | |||
) | [inline, static] |
Definition at line 58 of file minisat_global.h.
Referenced by CVC3::TheoryArithOld::pickIntEqMonomial(), CVC3::TheoryArithNew::pickIntEqMonomial(), and CVC3::TheoryArith3::pickIntEqMonomial().
static T MiniSat::max | ( | T | x, | |
T | y | |||
) | [inline, static] |
Definition at line 59 of file minisat_global.h.
Referenced by MiniSat::Solver::analyze(), MiniSat::Solver::analyze_minimize(), MiniSat::Solver::assume(), SAT::Clause::getMaxVar(), MiniSat::Solver::insertClause(), malloc_clause(), and MiniSat::Solver::setPushID().
static T* MiniSat::xmalloc | ( | size_t | size | ) | [inline, static] |
static T* MiniSat::xrealloc | ( | T * | ptr, | |
size_t | size | |||
) | [inline, static] |
Definition at line 75 of file minisat_global.h.
References DebugAssert.
Referenced by MiniSat::vec< T >::grow().
static void MiniSat::xfree | ( | T * | ptr | ) | [inline, static] |
Definition at line 80 of file minisat_global.h.
Referenced by MiniSat::Solver::backtrack(), MiniSat::vec< T >::clear(), MiniSat::Derivation::pop(), MiniSat::Solver::remove(), MiniSat::Solver::resolveTheoryImplication(), MiniSat::Derivation::~Derivation(), and MiniSat::Solver::~Solver().
static double MiniSat::drand | ( | double & | seed | ) | [inline, static] |
static int MiniSat::irand | ( | double & | seed, | |
int | size | |||
) | [inline, static] |
int MiniSat::toInt | ( | lbool | l | ) | [inline] |
Definition at line 211 of file minisat_global.h.
References MiniSat::lbool::toInt().
Referenced by MiniSat::Solver::backtrack(), MiniSat::Solver::checkTrail(), MiniSat::Solver::enqueue(), MiniSat::Solver::pop(), MiniSat::Solver::propLookahead(), and MiniSat::Solver::registerVar().
lbool MiniSat::toLbool | ( | int | v | ) | [inline] |
Definition at line 212 of file minisat_global.h.
Referenced by MiniSat::Solver::getValue(), and MiniSat::VarOrder::select().
static bool MiniSat::operator!= | ( | const T & | x, | |
const T & | y | |||
) | [inline, static] |
Definition at line 225 of file minisat_global.h.
static bool MiniSat::operator> | ( | const T & | x, | |
const T & | y | |||
) | [inline, static] |
Definition at line 226 of file minisat_global.h.
static bool MiniSat::operator<= | ( | const T & | x, | |
const T & | y | |||
) | [inline, static] |
Definition at line 227 of file minisat_global.h.
static bool MiniSat::operator>= | ( | const T & | x, | |
const T & | y | |||
) | [inline, static] |
Definition at line 228 of file minisat_global.h.
static int MiniSat::left | ( | int | i | ) | [inline, static] |
Definition at line 53 of file minisat_heap.h.
Referenced by CVC3::CompleteInstPreProcessor::collect_forall_index(), MiniSat::Derivation::createProof(), CVC3::TheoryArith3::doSolve(), CVC3::TheoryArithOld::findBounds(), CVC3::TheoryArithNew::findBounds(), CVC3::TheoryArith3::findBounds(), CVC3::TheoryArithNew::findCoefficient(), MiniSat::Heap< VarOrder_lt >::heapProperty(), CVC3::ArithTheoremProducerOld::intVarEqnConst(), CVC3::ArithTheoremProducer3::intVarEqnConst(), CVC3::ArithTheoremProducer::intVarEqnConst(), CVC3::CompleteInstPreProcessor::isGoodQuant(), CVC3::CompleteInstPreProcessor::isMacro(), MiniSat::Heap< VarOrder_lt >::percolateDown(), CVC3::ArithTheoremProducerOld::plusPredicate(), CVC3::ArithTheoremProducer3::plusPredicate(), CVC3::ArithTheoremProducer::plusPredicate(), printUsage(), CVC3::TheoryArithOld::processRealEq(), CVC3::TheoryArithNew::processRealEq(), CVC3::TheoryArith3::processRealEq(), CVC3::TheoryArray::rewrite(), CVC3::TheoryArithOld::rewrite(), CVC3::ArrayTheoremProducer::rewriteWriteWrite(), and CVC3::TheoryArithNew::substAndCanonizeTableaux().
static int MiniSat::right | ( | int | i | ) | [inline, static] |
Definition at line 54 of file minisat_heap.h.
Referenced by CVC3::CompleteInstPreProcessor::collect_forall_index(), MiniSat::Derivation::createProof(), CVC3::TheoryArithOld::doSolve(), CVC3::TheoryArithNew::doSolve(), CVC3::TheoryArith3::doSolve(), CVC3::TheoryArithOld::findBounds(), CVC3::TheoryArithNew::findBounds(), CVC3::TheoryArith3::findBounds(), CVC3::TheoryArithNew::findCoefficient(), MiniSat::Heap< VarOrder_lt >::heapProperty(), CVC3::ArithTheoremProducerOld::intVarEqnConst(), CVC3::ArithTheoremProducer3::intVarEqnConst(), CVC3::ArithTheoremProducer::intVarEqnConst(), CVC3::CompleteInstPreProcessor::isGoodQuant(), CVC3::CompleteInstPreProcessor::isMacro(), CVC3::TheoryArithOld::isolateVariable(), CVC3::TheoryArith3::isolateVariable(), CVC3::ArithTheoremProducerOld::moveSumConstantRight(), CVC3::ArithTheoremProducer3::moveSumConstantRight(), CVC3::ArithTheoremProducer::moveSumConstantRight(), CVC3::TheoryArithOld::normalizeProjectIneqs(), CVC3::TheoryArith3::normalizeProjectIneqs(), MiniSat::Heap< VarOrder_lt >::percolateDown(), CVC3::ArithTheoremProducerOld::plusPredicate(), CVC3::ArithTheoremProducer3::plusPredicate(), CVC3::ArithTheoremProducer::plusPredicate(), CVC3::TheoryArithOld::processRealEq(), CVC3::TheoryArithNew::processRealEq(), CVC3::TheoryArith3::processRealEq(), CVC3::TheoryArithOld::processSimpleIntEq(), CVC3::TheoryArithNew::processSimpleIntEq(), CVC3::TheoryArith3::processSimpleIntEq(), CVC3::TheoryArray::rewrite(), CVC3::TheoryArithOld::rewrite(), CVC3::ArrayTheoremProducer::rewriteWriteWrite(), and CVC3::TheoryArithNew::substAndCanonizeTableaux().
static int MiniSat::parent | ( | int | i | ) | [inline, static] |
Definition at line 55 of file minisat_heap.h.
Referenced by MiniSat::Heap< VarOrder_lt >::heapProperty(), and MiniSat::Heap< VarOrder_lt >::percolateUp().
conversions between MiniSat and CVC data types:
Definition at line 128 of file minisat_solver.h.
References SAT::Var::getIndex().
Referenced by MiniSat::Solver::addClause(), MiniSat::Solver::cvcToMiniSat(), cvcToMiniSat(), and SAT::DPLLTMiniSat::getValue().
SAT::Var MiniSat::miniSatToCVC | ( | Var | var | ) | [inline] |
Definition at line 132 of file minisat_solver.h.
Referenced by MiniSat::Derivation::createProof(), MiniSat::Solver::curAssigns(), MiniSat::Solver::curClauses(), miniSatToCVC(), MiniSat::Solver::propagate(), MiniSat::Solver::push(), and MiniSat::Solver::search().
Definition at line 137 of file minisat_solver.h.
References cvcToMiniSat(), SAT::Lit::getVar(), and SAT::Lit::isPositive().
SAT::Lit MiniSat::miniSatToCVC | ( | Lit | literal | ) | [inline] |
Definition at line 141 of file minisat_solver.h.
References miniSatToCVC(), MiniSat::Lit::sign(), and MiniSat::Lit::var().
bool MiniSat::cvcToMiniSat | ( | const SAT::Clause & | clause, | |
std::vector< Lit > & | literals | |||
) |
conversions between MiniSat and CVC data types:
Definition at line 121 of file minisat_solver.cpp.
References SAT::Clause::begin(), cvcToMiniSat(), SAT::Clause::end(), SAT::Lit::isFalse(), and SAT::Lit::isTrue().
void* MiniSat::malloc_clause | ( | const vector< Lit > & | ps | ) |
Definition at line 39 of file minisat_types.cpp.
References clause_mem_base, and max().
Referenced by Clause_new(), and Lemma_new().
Clause * MiniSat::Clause_new | ( | const vector< Lit > & | ps, | |
CVC3::Theorem | theorem, | |||
int | id | |||
) |
Definition at line 44 of file minisat_types.cpp.
References malloc_clause().
Referenced by MiniSat::Solver::addClause(), MiniSat::Derivation::computeRootReason(), MiniSat::Solver::cvcToMiniSat(), and MiniSat::Derivation::finish().
Clause * MiniSat::Lemma_new | ( | const vector< Lit > & | ps, | |
int | id, | |||
int | pushID | |||
) |
Definition at line 49 of file minisat_types.cpp.
References malloc_clause().
Referenced by MiniSat::Solver::analyze(), and MiniSat::Solver::insertLemma().
const Lit MiniSat::lit_Undef | ( | var_Undef | , | |
false | ||||
) |
Referenced by MiniSat::Solver::analyze(), and MiniSat::Solver::search().
const Lit MiniSat::lit_Error | ( | var_Undef | , | |
true | ||||
) |
const lbool MiniSat::l_True = toLbool( 1) |
Definition at line 214 of file minisat_global.h.
Referenced by MiniSat::Solver::allClausesSatisfied(), MiniSat::Solver::checkClause(), MiniSat::Derivation::computeRootReason(), MiniSat::Solver::getReason(), SAT::DPLLTMiniSat::getValue(), MiniSat::Solver::insertClause(), MiniSat::Solver::isPermSatisfied(), MiniSat::Solver::orderClause(), MiniSat::Solver::propagate(), MiniSat::Solver::resolveTheoryImplication(), MiniSat::Solver::simplifyClause(), MiniSat::Solver::simplifyDB(), and MiniSat::Solver::toString().
const lbool MiniSat::l_False = toLbool(-1) |
Definition at line 215 of file minisat_global.h.
Referenced by MiniSat::Solver::analyze(), MiniSat::Solver::checkClause(), MiniSat::Derivation::computeRootReason(), MiniSat::Solver::enqueue(), MiniSat::Solver::getConflictLevel(), MiniSat::Solver::getImplicationLevel(), SAT::DPLLTMiniSat::getValue(), MiniSat::Solver::insertClause(), MiniSat::Solver::insertLemma(), MiniSat::Solver::orderClause(), MiniSat::Solver::propagate(), MiniSat::Solver::resolveTheoryImplication(), MiniSat::Solver::simplifyClause(), MiniSat::Solver::simplifyDB(), MiniSat::Solver::toString(), and MiniSat::Solver::updateConflict().
const lbool MiniSat::l_Undef = toLbool( 0) |
Definition at line 216 of file minisat_global.h.
Referenced by MiniSat::Solver::backtrack(), MiniSat::Solver::checkClause(), MiniSat::Solver::enqueue(), MiniSat::Solver::insertClause(), MiniSat::Solver::pop(), MiniSat::Solver::propLookahead(), MiniSat::Solver::registerVar(), MiniSat::Solver::search(), and MiniSat::VarOrder::select().
const int MiniSat::clause_mem_base |
Initial value:
sizeof(unsigned int) + 2 * sizeof(int) + sizeof(float) + sizeof (CVC3::Theorem)
Definition at line 33 of file minisat_types.cpp.
Referenced by malloc_clause().
const int MiniSat::var_Undef = -1 |
Definition at line 56 of file minisat_types.h.
Referenced by MiniSat::Solver::propLookahead(), MiniSat::Solver::search(), and MiniSat::VarOrder::select().