SMT-RAT  24.02
Toolbox for Strategic and Parallel Satisfiability-Modulo-Theories Solving
Public Member Functions | Protected Attributes
smtrat::VarSchedulerBase Class Reference

Base class for variable schedulers. More...

#include <VarScheduler.h>

Inheritance diagram for smtrat::VarSchedulerBase:
Inheritance graph
[legend]

Public Member Functions

template<typename BaseModule >
 VarSchedulerBase (BaseModule &baseModule)
 
void rebuild ()
 Rebuild heap. More...
 
void insert (Minisat::Var)
 Insert a variable. More...
 
Minisat::Lit pop ()
 Returns the next variable to be decided. More...
 
bool empty ()
 Check if empty. More...
 
void print () const
 Check if variable is contained. More...
 
void increaseActivity (Minisat::Var)
 
void decreaseActivity (Minisat::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 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
 

Detailed Description

Base class for variable schedulers.

Removes the need to implement stubs.

During instantiation, the Scheduler is constructed with a const SATModule& as parameter.

Definition at line 15 of file VarScheduler.h.

Constructor & Destructor Documentation

◆ VarSchedulerBase()

template<typename BaseModule >
smtrat::VarSchedulerBase::VarSchedulerBase ( BaseModule &  baseModule)
inline

Definition at line 36 of file VarScheduler.h.

Member Function Documentation

◆ attachClause()

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

Definition at line 104 of file VarScheduler.h.

◆ decreaseActivity()

void smtrat::VarSchedulerBase::decreaseActivity ( Minisat::Var  )
inline

Definition at line 94 of file VarScheduler.h.

◆ detachClause()

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

Definition at line 107 of file VarScheduler.h.

◆ empty()

bool smtrat::VarSchedulerBase::empty ( )
inline

Check if empty.

Definition at line 77 of file VarScheduler.h.

◆ increaseActivity()

void smtrat::VarSchedulerBase::increaseActivity ( Minisat::Var  )
inline

Definition at line 91 of file VarScheduler.h.

◆ insert()

void smtrat::VarSchedulerBase::insert ( Minisat::Var  )
inline

Insert a variable.

If already contained, do nothing.

Definition at line 62 of file VarScheduler.h.

◆ pop()

Minisat::Lit smtrat::VarSchedulerBase::pop ( )
inline

Returns the next variable to be decided.

Returns and removes the next variable to be decided.

Definition at line 72 of file VarScheduler.h.

Here is the call graph for this function:

◆ print()

void smtrat::VarSchedulerBase::print ( ) const
inline

Check if variable is contained.

Print.

Definition at line 87 of file VarScheduler.h.

◆ rebuild()

void smtrat::VarSchedulerBase::rebuild ( )
inline

Rebuild heap.

Definition at line 57 of file VarScheduler.h.

◆ rebuildActivities()

void smtrat::VarSchedulerBase::rebuildActivities ( )
inline

Definition at line 97 of file VarScheduler.h.

◆ rebuildTheoryVars()

template<typename Constraints >
void smtrat::VarSchedulerBase::rebuildTheoryVars ( const Constraints &  )
inline

Definition at line 101 of file VarScheduler.h.

◆ relocateClauses()

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

Definition at line 110 of file VarScheduler.h.

Field Documentation

◆ abstractLiteral

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

Definition at line 31 of file VarScheduler.h.

◆ abstractVariable

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

Definition at line 30 of file VarScheduler.h.

◆ currentlySatisfiedByBackend

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

Definition at line 29 of file VarScheduler.h.

◆ getActivity

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

Definition at line 18 of file VarScheduler.h.

◆ getBoolLitValue

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

Definition at line 28 of file VarScheduler.h.

◆ getBoolVarValue

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

Definition at line 27 of file VarScheduler.h.

◆ getClause

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

Definition at line 26 of file VarScheduler.h.

◆ getPolarity

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

Definition at line 19 of file VarScheduler.h.

◆ isAbstractedFormula

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

Definition at line 32 of file VarScheduler.h.

◆ isBoolValueUndef

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

Definition at line 22 of file VarScheduler.h.

◆ isDecisionVar

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

Definition at line 21 of file VarScheduler.h.

◆ isTheoryAbstraction

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

Definition at line 23 of file VarScheduler.h.

◆ reabstractLiteral

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

Definition at line 25 of file VarScheduler.h.

◆ reabstractVariable

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

Definition at line 24 of file VarScheduler.h.

◆ setPolarity

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

Definition at line 20 of file VarScheduler.h.

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