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

Random scheduler. More...

#include <VarScheduler.h>

Inheritance diagram for smtrat::VarSchedulerRandom:
Inheritance graph
[legend]
Collaboration diagram for smtrat::VarSchedulerRandom:
Collaboration graph
[legend]

Public Member Functions

template<typename BaseModule >
 VarSchedulerRandom (BaseModule &baseModule)
 
void rebuild ()
 
void insert (Minisat::Var var)
 
Minisat::Lit pop ()
 
bool empty ()
 
void print () const
 
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 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

std::vector< Minisat::Var > vars
 

Detailed Description

Random scheduler.

Definition at line 242 of file VarScheduler.h.

Constructor & Destructor Documentation

◆ VarSchedulerRandom()

template<typename BaseModule >
smtrat::VarSchedulerRandom::VarSchedulerRandom ( BaseModule &  baseModule)
inlineexplicit

Definition at line 253 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::VarSchedulerBase::decreaseActivity ( Minisat::Var  )
inlineinherited

Definition at line 94 of file VarScheduler.h.

◆ detachClause()

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

Definition at line 107 of file VarScheduler.h.

◆ empty()

bool smtrat::VarSchedulerRandom::empty ( )
inline

Definition at line 286 of file VarScheduler.h.

Here is the call graph for this function:

◆ increaseActivity()

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

Definition at line 91 of file VarScheduler.h.

◆ insert()

void smtrat::VarSchedulerRandom::insert ( Minisat::Var  var)
inline

Definition at line 259 of file VarScheduler.h.

Here is the call graph for this function:

◆ pop()

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

Definition at line 278 of file VarScheduler.h.

Here is the call graph for this function:

◆ print()

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

Definition at line 298 of file VarScheduler.h.

Here is the call graph for this function:

◆ rebuild()

void smtrat::VarSchedulerRandom::rebuild ( )
inline

Definition at line 257 of file VarScheduler.h.

◆ rebuildActivities()

void smtrat::VarSchedulerBase::rebuildActivities ( )
inlineinherited

Definition at line 97 of file VarScheduler.h.

◆ 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.

◆ valid()

bool smtrat::VarSchedulerRandom::valid ( Minisat::Var  var)
inlineprotected

Definition at line 247 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.

◆ 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.

◆ vars

std::vector<Minisat::Var> smtrat::VarSchedulerRandom::vars
private

Definition at line 244 of file VarScheduler.h.

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