smtrat::VarSchedulerMinisat Class Reference

Minisat's activity-based variable scheduling. More...

#include <VarScheduler.h>

Inheritance diagram for smtrat::VarSchedulerMinisat:

Collaboration diagram for smtrat::VarSchedulerMinisat:

Data Structures
struct	VarOrderLt

Public Member Functions
template<typename BaseModule >
	VarSchedulerMinisat (BaseModule &baseModule, std::function< bool(Minisat::Var, Minisat::Var)> cmp)
template<typename BaseModule >
	VarSchedulerMinisat (BaseModule &baseModule)
void	rebuild ()
void	insert (Minisat::Var var)
Minisat::Var	top ()
Minisat::Lit	pop ()
bool	empty ()
void	print () const
void	increaseActivity (Minisat::Var var)
void	decreaseActivity (Minisat::Var var)
void	rebuildActivities ()
template<typename Constraints >
void	rebuildTheoryVars (const Constraints &)
void	attachClause (Minisat::CRef)
void	detachClause (Minisat::CRef)
void	relocateClauses (std::function< void(Minisat::CRef &)>)

Protected Member Functions
bool	valid (Minisat::Var var)

Protected Attributes
std::function< double(Minisat::Var)>	getActivity
std::function< char(Minisat::Var)>	getPolarity
std::function< void(Minisat::Var, bool)>	setPolarity
std::function< bool(Minisat::Var)>	isDecisionVar
std::function< bool(Minisat::Var)>	isBoolValueUndef
std::function< bool(Minisat::Var)>	isTheoryAbstraction
std::function< const FormulaT &(Minisat::Var)>	reabstractVariable
std::function< const FormulaT &(Minisat::Lit)>	reabstractLiteral
std::function< const Minisat::Clause &(Minisat::CRef)>	getClause
std::function< Minisat::lbool(Minisat::Var)>	getBoolVarValue
std::function< Minisat::lbool(Minisat::Lit)>	getBoolLitValue
std::function< unsigned(const FormulaT &)>	currentlySatisfiedByBackend
std::function< Minisat::Var(const FormulaT &)>	abstractVariable
std::function< const Minisat::Lit(const FormulaT &)>	abstractLiteral
std::function< bool(const FormulaT &)>	isAbstractedFormula

Private Attributes
Minisat::Heap< VarOrderLt >	order_heap

Detailed Description

Minisat's activity-based variable scheduling.

Definition at line 117 of file VarScheduler.h.

Constructor & Destructor Documentation

VarSchedulerMinisat() [1/2]

template<typename BaseModule >

smtrat::VarSchedulerMinisat::VarSchedulerMinisat ( BaseModule &  baseModule, std::function< bool(Minisat::Var, Minisat::Var)>  cmp  )

inlineexplicit

Definition at line 141 of file VarScheduler.h.

VarSchedulerMinisat() [2/2]

template<typename BaseModule >

smtrat::VarSchedulerMinisat::VarSchedulerMinisat ( BaseModule &  baseModule )

inlineexplicit

Definition at line 147 of file VarScheduler.h.

Member Function Documentation

attachClause()

void smtrat::VarSchedulerBase::attachClause ( Minisat::CRef  )

inlineinherited

Definition at line 104 of file VarScheduler.h.

decreaseActivity()

void smtrat::VarSchedulerMinisat::decreaseActivity ( Minisat::Var  var )

inline

Definition at line 200 of file VarScheduler.h.

Here is the call graph for this function:

Here is the caller graph for this function:

detachClause()

void smtrat::VarSchedulerBase::detachClause ( Minisat::CRef  )

inlineinherited

Definition at line 107 of file VarScheduler.h.

empty()

bool smtrat::VarSchedulerMinisat::empty ( )

inline

Definition at line 177 of file VarScheduler.h.

Here is the call graph for this function:

Here is the caller graph for this function:

increaseActivity()

void smtrat::VarSchedulerMinisat::increaseActivity ( Minisat::Var  var )

inline

Definition at line 195 of file VarScheduler.h.

Here is the call graph for this function:

Here is the caller graph for this function:

insert()

void smtrat::VarSchedulerMinisat::insert ( Minisat::Var  var )

inline

Definition at line 159 of file VarScheduler.h.

Here is the call graph for this function:

Here is the caller graph for this function:

pop()

Minisat::Lit smtrat::VarSchedulerMinisat::pop ( )

inline

Definition at line 170 of file VarScheduler.h.

Here is the call graph for this function:

Here is the caller graph for this function:

print()

void smtrat::VarSchedulerMinisat::print ( ) const

inline

Definition at line 189 of file VarScheduler.h.

Here is the call graph for this function:

Here is the caller graph for this function:

rebuild()

void smtrat::VarSchedulerMinisat::rebuild ( )

inline

Definition at line 151 of file VarScheduler.h.

Here is the call graph for this function:

Here is the caller graph for this function:

rebuildActivities()

void smtrat::VarSchedulerMinisat::rebuildActivities ( )

inline

Definition at line 205 of file VarScheduler.h.

Here is the caller graph for this function:

rebuildTheoryVars()

template<typename Constraints >

void smtrat::VarSchedulerBase::rebuildTheoryVars ( const Constraints &  )

inlineinherited

Definition at line 101 of file VarScheduler.h.

relocateClauses()

void smtrat::VarSchedulerBase::relocateClauses ( std::function< void(Minisat::CRef &)>  )

inlineinherited

Definition at line 110 of file VarScheduler.h.

top()

Minisat::Var smtrat::VarSchedulerMinisat::top ( )

inline

Definition at line 164 of file VarScheduler.h.

Here is the caller graph for this function:

valid()

bool smtrat::VarSchedulerMinisat::valid ( Minisat::Var  var )

inlineprotected

Definition at line 135 of file VarScheduler.h.

Here is the call graph for this function:

Field Documentation

abstractLiteral

std::function<const Minisat::Lit(const FormulaT&)> smtrat::VarSchedulerBase::abstractLiteral

protectedinherited

Definition at line 31 of file VarScheduler.h.

abstractVariable

std::function< Minisat::Var(const FormulaT&)> smtrat::VarSchedulerBase::abstractVariable

protectedinherited

Definition at line 30 of file VarScheduler.h.

currentlySatisfiedByBackend

std::function<unsigned(const FormulaT&)> smtrat::VarSchedulerBase::currentlySatisfiedByBackend

protectedinherited

Definition at line 29 of file VarScheduler.h.

getActivity

std::function<double(Minisat::Var)> smtrat::VarSchedulerBase::getActivity

protectedinherited

Definition at line 18 of file VarScheduler.h.

getBoolLitValue

std::function<Minisat::lbool(Minisat::Lit)> smtrat::VarSchedulerBase::getBoolLitValue

protectedinherited

Definition at line 28 of file VarScheduler.h.

getBoolVarValue

std::function<Minisat::lbool(Minisat::Var)> smtrat::VarSchedulerBase::getBoolVarValue

protectedinherited

Definition at line 27 of file VarScheduler.h.

getClause

std::function<const Minisat::Clause&(Minisat::CRef)> smtrat::VarSchedulerBase::getClause

protectedinherited

Definition at line 26 of file VarScheduler.h.

getPolarity

std::function<char(Minisat::Var)> smtrat::VarSchedulerBase::getPolarity

protectedinherited

Definition at line 19 of file VarScheduler.h.

isAbstractedFormula

std::function<bool(const FormulaT&)> smtrat::VarSchedulerBase::isAbstractedFormula

protectedinherited

Definition at line 32 of file VarScheduler.h.

isBoolValueUndef

std::function<bool(Minisat::Var)> smtrat::VarSchedulerBase::isBoolValueUndef

protectedinherited

Definition at line 22 of file VarScheduler.h.

isDecisionVar

std::function<bool(Minisat::Var)> smtrat::VarSchedulerBase::isDecisionVar

protectedinherited

Definition at line 21 of file VarScheduler.h.

isTheoryAbstraction

std::function<bool(Minisat::Var)> smtrat::VarSchedulerBase::isTheoryAbstraction

protectedinherited

Definition at line 23 of file VarScheduler.h.

order_heap

Minisat::Heap<VarOrderLt> smtrat::VarSchedulerMinisat::order_heap

private

Definition at line 132 of file VarScheduler.h.

reabstractLiteral

std::function<const FormulaT&(Minisat::Lit)> smtrat::VarSchedulerBase::reabstractLiteral

protectedinherited

Definition at line 25 of file VarScheduler.h.

reabstractVariable

std::function<const FormulaT&(Minisat::Var)> smtrat::VarSchedulerBase::reabstractVariable

protectedinherited

Definition at line 24 of file VarScheduler.h.

setPolarity

std::function<void(Minisat::Var,bool)> smtrat::VarSchedulerBase::setPolarity

protectedinherited

Definition at line 20 of file VarScheduler.h.

---

The documentation for this class was generated from the following file:

• smtrat-modules/SATModule/VarScheduler.h