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)
• 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 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(), 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::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::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(), CVC3::TheoryArithNew::substAndCanonizeTableaux(), and SAT::CNF_Manager::translateExprRec().

static int MiniSat::right

(

int

i

)

[inline, static]

Definition at line 54 of file minisat_heap.h.

Referenced by CVC3::VCL::andExpr(), 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::VCL::minusExpr(), CVC3::ArithTheoremProducerOld::moveSumConstantRight(), CVC3::ArithTheoremProducer3::moveSumConstantRight(), CVC3::ArithTheoremProducer::moveSumConstantRight(), CVC3::VCL::multExpr(), CVC3::TheoryArithOld::normalizeProjectIneqs(), CVC3::TheoryArith3::normalizeProjectIneqs(), CVC3::VCL::orExpr(), MiniSat::Heap< VarOrder_lt >::percolateDown(), CVC3::VCL::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(), CVC3::TheoryArray::rewrite(), CVC3::TheoryArithOld::rewrite(), CVC3::ArrayTheoremProducer::rewriteWriteWrite(), CVC3::TheoryArithNew::substAndCanonizeTableaux(), and SAT::CNF_Manager::translateExprRec().

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

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

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

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

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
	)

---

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