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

Base class for all MCSAT variable scheduler. More...

#include <VarSchedulerMcsat.h>

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

Public Member Functions

template<typename BaseModule >
 VarSchedulerMcsatBase (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< bool(Minisat::Var)> isTheoryVar
 
std::function< carl::Variable(Minisat::Var)> carlVar
 
std::function< Minisat::Var(carl::Variable)> minisatVar
 
std::function< Model()> currentModel
 
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 all MCSAT variable scheduler.

Should not be used directly.

Definition at line 12 of file VarSchedulerMcsat.h.

Constructor & Destructor Documentation

◆ VarSchedulerMcsatBase()

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

Definition at line 23 of file VarSchedulerMcsat.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::VarSchedulerBase::empty ( )
inlineinherited

Check if empty.

Definition at line 77 of file VarScheduler.h.

◆ increaseActivity()

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

Definition at line 91 of file VarScheduler.h.

◆ insert()

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

Insert a variable.

If already contained, do nothing.

Definition at line 62 of file VarScheduler.h.

◆ pop()

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

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
inlineinherited

Check if variable is contained.

Print.

Definition at line 87 of file VarScheduler.h.

◆ rebuild()

void smtrat::VarSchedulerBase::rebuild ( )
inlineinherited

Rebuild heap.

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

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.

◆ carlVar

std::function<carl::Variable(Minisat::Var)> smtrat::VarSchedulerMcsatBase::carlVar
protected

Definition at line 16 of file VarSchedulerMcsat.h.

◆ currentlySatisfiedByBackend

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

Definition at line 29 of file VarScheduler.h.

◆ currentModel

std::function<Model()> smtrat::VarSchedulerMcsatBase::currentModel
protected

Definition at line 18 of file VarSchedulerMcsat.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.

◆ isTheoryVar

std::function<bool(Minisat::Var)> smtrat::VarSchedulerMcsatBase::isTheoryVar
protected

Definition at line 15 of file VarSchedulerMcsat.h.

◆ minisatVar

std::function<Minisat::Var(carl::Variable)> smtrat::VarSchedulerMcsatBase::minisatVar
protected

Definition at line 17 of file VarSchedulerMcsat.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: