CVC3
2.4.1
|
Classes | |
class | Inference |
class | Derivation |
struct | STATIC_ASSERTION_FAILURE |
struct | STATIC_ASSERTION_FAILURE< true > |
class | vec |
class | lbool |
class | Heap |
struct | SolverStats |
struct | PushEntry |
struct | SearchParams |
class | Solver |
class | Lit |
class | Clause |
struct | VarOrder_lt |
class | VarOrder |
Typedefs | |
typedef std::vector< int > ::size_type | size_type |
typedef int | Var |
Functions | |
template<class T > | |
static T | min (T x, T y) |
template<class T > | |
static T | max (T x, T y) |
template<class T > | |
static T * | xmalloc (size_t size) |
template<class T > | |
static T * | xrealloc (T *ptr, size_t size) |
template<class T > | |
static void | xfree (T *ptr) |
static double | drand (double &seed) |
static int | irand (double &seed, int size) |
int | toInt (lbool l) |
lbool | toLbool (int v) |
template<class T > | |
static bool | operator!= (const T &x, const T &y) |
template<class T > | |
static bool | operator> (const T &x, const T &y) |
template<class T > | |
static bool | operator<= (const T &x, const T &y) |
template<class T > | |
static bool | operator>= (const T &x, const T &y) |
static int | left (int i) |
static int | right (int i) |
static int | parent (int i) |
Var | cvcToMiniSat (const SAT::Var &var) |
SAT::Var | miniSatToCVC (Var var) |
Lit | cvcToMiniSat (const SAT::Lit &literal) |
SAT::Lit | miniSatToCVC (Lit literal) |
bool | cvcToMiniSat (const SAT::Clause &clause, std::vector< Lit > &literals) |
void * | malloc_clause (const vector< Lit > &ps) |
Clause * | Clause_new (const vector< Lit > &ps, CVC3::Theorem theorem, int id) |
Clause * | Lemma_new (const vector< Lit > &ps, int id, int pushID) |
const Lit | lit_Undef (var_Undef, false) |
const Lit | lit_Error (var_Undef, true) |
Variables | |
const lbool | l_True = toLbool( 1) |
const lbool | l_False = toLbool(-1) |
const lbool | l_Undef = toLbool( 0) |
const int | clause_mem_base |
const int | var_Undef = -1 |
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.
|
inlinestatic |
Definition at line 58 of file minisat_global.h.
Referenced by CVC3::TheoryArithNew::pickIntEqMonomial(), CVC3::TheoryArith3::pickIntEqMonomial(), and CVC3::TheoryArithOld::pickIntEqMonomial().
|
inlinestatic |
Definition at line 59 of file minisat_global.h.
Referenced by MiniSat::Solver::analyze(), MiniSat::Solver::analyze_minimize(), and MiniSat::Solver::insertClause().
|
inlinestatic |
Definition at line 70 of file minisat_global.h.
References DebugAssert.
|
inlinestatic |
Definition at line 75 of file minisat_global.h.
References DebugAssert.
Referenced by MiniSat::vec< T >::grow().
|
inlinestatic |
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().
|
inlinestatic |
Definition at line 89 of file minisat_global.h.
Referenced by irand().
|
inlinestatic |
Definition at line 96 of file minisat_global.h.
References drand().
|
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().
|
inline |
Definition at line 212 of file minisat_global.h.
Referenced by MiniSat::Solver::getValue(), and MiniSat::VarOrder::select().
|
inlinestatic |
Definition at line 225 of file minisat_global.h.
|
inlinestatic |
Definition at line 226 of file minisat_global.h.
|
inlinestatic |
Definition at line 227 of file minisat_global.h.
|
inlinestatic |
Definition at line 228 of file minisat_global.h.
|
inlinestatic |
Definition at line 53 of file minisat_heap.h.
Referenced by CVC3::CompleteInstPreProcessor::collect_forall_index(), MiniSat::Derivation::createProof(), CVC3::TheoryArith3::doSolve(), CVC3::TheoryArithNew::findBounds(), CVC3::TheoryArith3::findBounds(), CVC3::TheoryArithOld::findBounds(), CVC3::TheoryArithNew::findCoefficient(), MiniSat::Heap< MiniSat::VarOrder_lt >::heapProperty(), CVC3::ArithTheoremProducer3::intVarEqnConst(), CVC3::ArithTheoremProducer::intVarEqnConst(), CVC3::ArithTheoremProducerOld::intVarEqnConst(), CVC3::CompleteInstPreProcessor::isGoodQuant(), CVC3::CompleteInstPreProcessor::isMacro(), MiniSat::Heap< MiniSat::VarOrder_lt >::percolateDown(), CVC3::ArithTheoremProducerOld::plusPredicate(), CVC3::ArithTheoremProducer3::plusPredicate(), CVC3::ArithTheoremProducer::plusPredicate(), printUsage(), CVC3::TheoryArithNew::processRealEq(), CVC3::TheoryArith3::processRealEq(), CVC3::TheoryArithOld::processRealEq(), CVC3::TheoryArray::rewrite(), CVC3::TheoryArithOld::rewrite(), CVC3::ArrayTheoremProducer::rewriteWriteWrite(), CVC3::TheoryArithNew::substAndCanonizeTableaux(), and SAT::CNF_Manager::translateExprRec().
|
inlinestatic |
Definition at line 54 of file minisat_heap.h.
Referenced by CVC3::VCL::andExpr(), CVC3::CompleteInstPreProcessor::collect_forall_index(), MiniSat::Derivation::createProof(), CVC3::TheoryArithNew::doSolve(), CVC3::TheoryArith3::doSolve(), CVC3::TheoryArithOld::doSolve(), CVC3::TheoryArithNew::findBounds(), CVC3::TheoryArith3::findBounds(), CVC3::TheoryArithOld::findBounds(), CVC3::TheoryArithNew::findCoefficient(), MiniSat::Heap< MiniSat::VarOrder_lt >::heapProperty(), CVC3::ArithTheoremProducer3::intVarEqnConst(), CVC3::ArithTheoremProducerOld::intVarEqnConst(), CVC3::ArithTheoremProducer::intVarEqnConst(), CVC3::CompleteInstPreProcessor::isGoodQuant(), CVC3::CompleteInstPreProcessor::isMacro(), CVC3::TheoryArith3::isolateVariable(), CVC3::TheoryArithOld::isolateVariable(), CVC3::VCL::minusExpr(), CVC3::ArithTheoremProducer3::moveSumConstantRight(), CVC3::ArithTheoremProducerOld::moveSumConstantRight(), CVC3::ArithTheoremProducer::moveSumConstantRight(), CVC3::VCL::multExpr(), CVC3::TheoryArith3::normalizeProjectIneqs(), CVC3::TheoryArithOld::normalizeProjectIneqs(), CVC3::VCL::orExpr(), MiniSat::Heap< MiniSat::VarOrder_lt >::percolateDown(), CVC3::VCL::plusExpr(), CVC3::ArithTheoremProducer3::plusPredicate(), CVC3::ArithTheoremProducerOld::plusPredicate(), CVC3::ArithTheoremProducer::plusPredicate(), CVC3::TheoryArithNew::processRealEq(), CVC3::TheoryArith3::processRealEq(), CVC3::TheoryArithOld::processRealEq(), CVC3::TheoryArithNew::processSimpleIntEq(), CVC3::TheoryArith3::processSimpleIntEq(), CVC3::TheoryArithOld::processSimpleIntEq(), CVC3::TheoryArray::rewrite(), CVC3::TheoryArithOld::rewrite(), CVC3::ArrayTheoremProducer::rewriteWriteWrite(), CVC3::TheoryArithNew::substAndCanonizeTableaux(), and SAT::CNF_Manager::translateExprRec().
|
inlinestatic |
Definition at line 55 of file minisat_heap.h.
Referenced by MiniSat::Heap< MiniSat::VarOrder_lt >::heapProperty(), and MiniSat::Heap< MiniSat::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(), cvcToMiniSat(), MiniSat::Solver::cvcToMiniSat(), SAT::DPLLTMiniSat::getValue(), MiniSat::Solver::push(), and MiniSat::Solver::search().
|
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().
|
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 CVC3::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(), MiniSat::Clause::Decision(), MiniSat::Derivation::finish(), and MiniSat::Clause::TheoryImplication().
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 | |||
) |
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().
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().
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 |
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().