MiniSat Namespace Reference

Classes

• class Inference
• class Derivation
• 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)
• bool cvcToMiniSat (const SAT::Clause &clause, std::vector< Lit > &literals)
• Clause * cvcToMiniSat (const SAT::Clause &clause, int id)
• Var cvcToMiniSat (const SAT::Var &var)
• SAT::Var miniSatToCVC (Var var)
• Lit cvcToMiniSat (const SAT::Lit &literal)
• SAT::Lit miniSatToCVC (Lit literal)
• Clause * Clause_new (const vector< Lit > &ps, int id)
• Clause * Lemma_new (const vector< Lit > &ps, int id, int pushID)

Variables

• const lbool l_True = toLbool( 1)
• const lbool l_False = toLbool(-1)
• const lbool l_Undef = toLbool( 0)
• const int var_Undef = -1
• const Lit lit_Undef (var_Undef, false)
• const Lit lit_Error (var_Undef, true)

---

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 54 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::DecisionEngineCaching::goalSatisfied(), CVC3::TheoryArithOld::pickIntEqMonomial(), and CVC3::TheoryArithNew::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(), SAT::Clause::getMaxVar(), CVC3::DecisionEngineMBTF::goalSatisfied(), MiniSat::Solver::insertClause(), 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::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::divideExpr(), CVC3::TheoryArithOld::findBounds(), CVC3::TheoryArithNew::findBounds(), CVC3::TheoryArithNew::findCoefficient(), CVC3::VCL::funExpr(), CVC3::VCL::geExpr(), CVC3::geExpr(), CVC3::VCL::gtExpr(), CVC3::gtExpr(), MiniSat::Heap< MiniSat::VarOrder_lt >::heapProperty(), CVC3::VCL::iffExpr(), CVC3::ArithTheoremProducerOld::intVarEqnConst(), CVC3::ArithTheoremProducer::intVarEqnConst(), 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< MiniSat::VarOrder_lt >::percolateDown(), CVC3::VCL::plusExpr(), CVC3::plusExpr(), CVC3::ArithTheoremProducerOld::plusPredicate(), CVC3::ArithTheoremProducer::plusPredicate(), printUsage(), CVC3::TheoryArithOld::processRealEq(), CVC3::TheoryArithNew::processRealEq(), CVC3::TheoryArray::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::computeNormalFactor(), CVC3::TheoryArithNew::computeNormalFactor(), CVC3::divideExpr(), CVC3::TheoryArithOld::doSolve(), CVC3::TheoryArithNew::doSolve(), CVC3::Expr::eqExpr(), CVC3::TheoryArithOld::findBounds(), CVC3::TheoryArithNew::findBounds(), CVC3::TheoryArithNew::findCoefficient(), CVC3::VCL::funExpr(), CVC3::VCL::geExpr(), CVC3::geExpr(), CVC3::VCL::gtExpr(), CVC3::gtExpr(), MiniSat::Heap< MiniSat::VarOrder_lt >::heapProperty(), CVC3::VCL::iffExpr(), CVC3::Expr::iffExpr(), CVC3::Expr::impExpr(), CVC3::ArithTheoremProducerOld::intVarEqnConst(), CVC3::ArithTheoremProducer::intVarEqnConst(), CVC3::TheoryArithOld::isolateVariable(), CVC3::VCL::leExpr(), CVC3::leExpr(), CVC3::VCL::ltExpr(), CVC3::ltExpr(), CVC3::VCL::minusExpr(), CVC3::minusExpr(), CVC3::ArithTheoremProducerOld::moveSumConstantRight(), CVC3::ArithTheoremProducer::moveSumConstantRight(), CVC3::VCL::multExpr(), CVC3::multExpr(), CVC3::TheoryArithOld::normalizeProjectIneqs(), CVC3::Expr::operator &&(), CVC3::operator *(), CVC3::operator+(), CVC3::operator-(), CVC3::operator/(), CVC3::Expr::operator||(), CVC3::VCL::orExpr(), CVC3::Expr::orExpr(), MiniSat::Heap< MiniSat::VarOrder_lt >::percolateDown(), CVC3::TheoryArithOld::pickIntEqMonomial(), CVC3::TheoryArithNew::pickIntEqMonomial(), CVC3::TheoryArithOld::pickMonomial(), CVC3::VCL::plusExpr(), CVC3::plusExpr(), CVC3::ArithTheoremProducerOld::plusPredicate(), CVC3::ArithTheoremProducer::plusPredicate(), CVC3::TheoryArithOld::processRealEq(), CVC3::TheoryArithNew::processRealEq(), CVC3::TheoryArithOld::processSimpleIntEq(), CVC3::TheoryArithNew::processSimpleIntEq(), CVC3::TheoryArray::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 CVC3::TheoryQuant::add_parent(), MiniSat::Heap< MiniSat::VarOrder_lt >::heapProperty(), and MiniSat::Heap< MiniSat::VarOrder_lt >::percolateUp().

bool MiniSat::cvcToMiniSat	(	const SAT::Clause &	clause,
		std::vector< Lit > &	literals
	)

conversions between MiniSat and CVC data types:

Definition at line 119 of file minisat_solver.cpp.

References SAT::Clause::begin(), and SAT::Clause::end().

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

Clause * MiniSat::cvcToMiniSat	(	const SAT::Clause &	clause,
		int	id
	)

Definition at line 137 of file minisat_solver.cpp.

References Clause_new(), and cvcToMiniSat().

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 miniSatToCVC(), MiniSat::Solver::propagate(), MiniSat::Solver::push(), MiniSat::Solver::resolveTheoryImplication(), 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().

Clause * MiniSat::Clause_new	(	const vector< Lit > &	ps,
		int	id
	)

Definition at line 33 of file minisat_types.cpp.

References DebugAssert.

Referenced by MiniSat::Solver::addClause(), MiniSat::Derivation::computeRootReason(), cvcToMiniSat(), and MiniSat::Derivation::finish().

Clause * MiniSat::Lemma_new	(	const vector< Lit > &	ps,
		int	id,
		int	pushID
	)

Definition at line 45 of file minisat_types.cpp.

References DebugAssert, and MiniSat::Clause::pushID().

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::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::var_Undef = -1

Definition at line 55 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)

---