MiniSat Namespace Reference

Classes

Typedefs

Functions

Variables

Typedef Documentation

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.

Function Documentation

template<class T>
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().

template<class T>
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(), CVC3::TheoryArithOld::fixCurrentMaxCoefficient(), CVC3::TheoryArith3::fixCurrentMaxCoefficient(), SAT::Clause::getMaxVar(), MiniSat::Solver::insertClause(), malloc_clause(), and MiniSat::Solver::setPushID().

template<class T>
static T* MiniSat::xmalloc ( size_t  size  )  [inline, static]

Definition at line 70 of file minisat_global.h.

References DebugAssert.

template<class T>
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().

template<class T>
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]

Definition at line 89 of file minisat_global.h.

Referenced by irand().

static int MiniSat::irand ( double &  seed,
int  size 
) [inline, static]

Definition at line 96 of file minisat_global.h.

References drand().

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().

template<class T>
static bool MiniSat::operator!= ( const T &  x,
const T &  y 
) [inline, static]

Definition at line 225 of file minisat_global.h.

template<class T>
static bool MiniSat::operator> ( const T &  x,
const T &  y 
) [inline, static]

Definition at line 226 of file minisat_global.h.

template<class T>
static bool MiniSat::operator<= ( const T &  x,
const T &  y 
) [inline, static]

Definition at line 227 of file minisat_global.h.

template<class T>
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::VCL::andExpr(), CVC3::CompleteInstPreProcessor::collect_forall_index(), MiniSat::Derivation::createProof(), CVC3::divideExpr(), CVC3::TheoryArith3::doSolve(), CVC3::TheoryArithOld::findBounds(), CVC3::TheoryArithNew::findBounds(), CVC3::TheoryArith3::findBounds(), CVC3::TheoryArithNew::findCoefficient(), CVC3::VCL::funExpr(), CVC3::VCL::geExpr(), CVC3::geExpr(), CVC3::VCL::gtExpr(), CVC3::gtExpr(), MiniSat::Heap< VarOrder_lt >::heapProperty(), CVC3::VCL::iffExpr(), CVC3::ArithTheoremProducerOld::intVarEqnConst(), CVC3::ArithTheoremProducer3::intVarEqnConst(), CVC3::ArithTheoremProducer::intVarEqnConst(), CVC3::CompleteInstPreProcessor::isGoodQuant(), CVC3::CompleteInstPreProcessor::isMacro(), CVC3::VCL::leExpr(), CVC3::leExpr(), CVC3::VCL::ltExpr(), CVC3::ltExpr(), CVC3::VCL::minusExpr(), CVC3::minusExpr(), CVC3::VCL::multExpr(), CVC3::multExpr(), CVC3::operator *(), CVC3::operator+(), CVC3::operator-(), CVC3::operator/(), CVC3::VCL::orExpr(), MiniSat::Heap< VarOrder_lt >::percolateDown(), CVC3::VCL::plusExpr(), CVC3::plusExpr(), CVC3::ArithTheoremProducerOld::plusPredicate(), CVC3::ArithTheoremProducer3::plusPredicate(), CVC3::ArithTheoremProducer::plusPredicate(), printUsage(), CVC3::TheoryArithOld::processRealEq(), CVC3::TheoryArithNew::processRealEq(), CVC3::TheoryArith3::processRealEq(), SAT::SatProof::registerNode(), 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::VCL::andExpr(), CVC3::Expr::andExpr(), CVC3::TheoryArithOld::canPickEqMonomial(), CVC3::CompleteInstPreProcessor::collect_forall_index(), CVC3::TheoryArithOld::computeNormalFactor(), CVC3::TheoryArithNew::computeNormalFactor(), CVC3::TheoryArith3::computeNormalFactor(), MiniSat::Derivation::createProof(), CVC3::divideExpr(), CVC3::TheoryArithOld::doSolve(), CVC3::TheoryArithNew::doSolve(), CVC3::TheoryArith3::doSolve(), CVC3::Expr::eqExpr(), CVC3::TheoryArithOld::findBounds(), CVC3::TheoryArithNew::findBounds(), CVC3::TheoryArith3::findBounds(), CVC3::TheoryArithNew::findCoefficient(), CVC3::VCL::funExpr(), CVC3::VCL::geExpr(), CVC3::geExpr(), CVC3::VCL::gtExpr(), CVC3::gtExpr(), MiniSat::Heap< VarOrder_lt >::heapProperty(), CVC3::VCL::iffExpr(), CVC3::Expr::iffExpr(), CVC3::Expr::impExpr(), CVC3::ArithTheoremProducerOld::intVarEqnConst(), CVC3::ArithTheoremProducer3::intVarEqnConst(), CVC3::ArithTheoremProducer::intVarEqnConst(), CVC3::CompleteInstPreProcessor::isGoodQuant(), CVC3::CompleteInstPreProcessor::isMacro(), CVC3::TheoryArithOld::isolateVariable(), CVC3::TheoryArith3::isolateVariable(), CVC3::VCL::leExpr(), CVC3::leExpr(), CVC3::VCL::ltExpr(), CVC3::ltExpr(), CVC3::VCL::minusExpr(), CVC3::minusExpr(), CVC3::ArithTheoremProducerOld::moveSumConstantRight(), CVC3::ArithTheoremProducer3::moveSumConstantRight(), CVC3::ArithTheoremProducer::moveSumConstantRight(), CVC3::VCL::multExpr(), CVC3::multExpr(), CVC3::TheoryArithOld::normalizeProjectIneqs(), CVC3::TheoryArith3::normalizeProjectIneqs(), CVC3::Expr::operator &&(), CVC3::operator *(), CVC3::operator+(), CVC3::operator-(), CVC3::operator/(), CVC3::Expr::operator||(), CVC3::VCL::orExpr(), CVC3::Expr::orExpr(), MiniSat::Heap< VarOrder_lt >::percolateDown(), CVC3::TheoryArithOld::pickIntEqMonomial(), CVC3::TheoryArithNew::pickIntEqMonomial(), CVC3::TheoryArith3::pickIntEqMonomial(), CVC3::TheoryArithOld::pickMonomial(), CVC3::TheoryArith3::pickMonomial(), CVC3::VCL::plusExpr(), CVC3::plusExpr(), 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(), SAT::SatProof::registerNode(), CVC3::TheoryArray::rewrite(), CVC3::TheoryArithOld::rewrite(), CVC3::ArrayTheoremProducer::rewriteWriteWrite(), CVC3::TheoryArithNew::substAndCanonizeTableaux(), and CVC3::Expr::xorExpr().

static int MiniSat::parent ( int  i  )  [inline, static]

Definition at line 55 of file minisat_heap.h.

Referenced by CVC3::TheoryQuant::add_parent(), MiniSat::Heap< VarOrder_lt >::heapProperty(), and MiniSat::Heap< VarOrder_lt >::percolateUp().

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(), and SAT::Clause::end().

Referenced by MiniSat::Solver::addClause(), cvcToMiniSat(), MiniSat::Solver::cvcToMiniSat(), SAT::DPLLTMiniSat::getValue(), MiniSat::Solver::push(), and MiniSat::Solver::search().

Var MiniSat::cvcToMiniSat ( const SAT::Var &  var  )  [inline]

conversions between MiniSat and CVC data types:

Definition at line 128 of file minisat_solver.h.

References SAT::Var::getIndex().

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().

Lit MiniSat::cvcToMiniSat ( const SAT::Lit &  literal  )  [inline]

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().

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().

Variable Documentation

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().

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)

Generated on Wed Nov 18 16:18:43 2009 for CVC3 by  doxygen 1.5.2