SMT-RAT  24.02
Toolbox for Strategic and Parallel Satisfiability-Modulo-Theories Solving
Public Member Functions | Protected Attributes | Private Member Functions | Private Attributes
smtrat::VarSchedulerMcsatUnivariateConstraintsOnly< lookahead, vot > Class Template Reference

Decides only Constraints univariate in the current theory variable while the theory ordering is static. More...

#include <VarSchedulerMcsat.h>

Inheritance diagram for smtrat::VarSchedulerMcsatUnivariateConstraintsOnly< lookahead, vot >:
Inheritance graph
[legend]
Collaboration diagram for smtrat::VarSchedulerMcsatUnivariateConstraintsOnly< lookahead, vot >:
Collaboration graph
[legend]

Public Member Functions

template<typename BaseModule >
 VarSchedulerMcsatUnivariateConstraintsOnly (BaseModule &baseModule)
 
void rebuild ()
 
void insert (Minisat::Var var)
 
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 &c)
 
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
 

Private Member Functions

bool varCmp (Minisat::Var x, Minisat::Var y)
 
bool varDecidable (Minisat::Var x)
 

Private Attributes

VarSchedulerMinisat boolean_ordering
 
TheoryVarSchedulerStatic< vot > theory_ordering
 

Detailed Description

template<int lookahead, mcsat::VariableOrdering vot>
class smtrat::VarSchedulerMcsatUnivariateConstraintsOnly< lookahead, vot >

Decides only Constraints univariate in the current theory variable while the theory ordering is static.

Definition at line 329 of file VarSchedulerMcsat.h.

Constructor & Destructor Documentation

◆ VarSchedulerMcsatUnivariateConstraintsOnly()

template<int lookahead, mcsat::VariableOrdering vot>
template<typename BaseModule >
smtrat::VarSchedulerMcsatUnivariateConstraintsOnly< lookahead, vot >::VarSchedulerMcsatUnivariateConstraintsOnly ( BaseModule &  baseModule)
inlineexplicit

Definition at line 346 of file VarSchedulerMcsat.h.

Member Function Documentation

◆ attachClause()

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

Definition at line 104 of file VarScheduler.h.

◆ decreaseActivity()

template<int lookahead, mcsat::VariableOrdering vot>
void smtrat::VarSchedulerMcsatUnivariateConstraintsOnly< lookahead, vot >::decreaseActivity ( Minisat::Var  var)
inline

Definition at line 422 of file VarSchedulerMcsat.h.

Here is the call graph for this function:

◆ detachClause()

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

Definition at line 107 of file VarScheduler.h.

◆ empty()

template<int lookahead, mcsat::VariableOrdering vot>
bool smtrat::VarSchedulerMcsatUnivariateConstraintsOnly< lookahead, vot >::empty ( )
inline

Definition at line 397 of file VarSchedulerMcsat.h.

Here is the call graph for this function:

◆ increaseActivity()

template<int lookahead, mcsat::VariableOrdering vot>
void smtrat::VarSchedulerMcsatUnivariateConstraintsOnly< lookahead, vot >::increaseActivity ( Minisat::Var  var)
inline

Definition at line 418 of file VarSchedulerMcsat.h.

Here is the call graph for this function:

◆ insert()

template<int lookahead, mcsat::VariableOrdering vot>
void smtrat::VarSchedulerMcsatUnivariateConstraintsOnly< lookahead, vot >::insert ( Minisat::Var  var)
inline

Definition at line 356 of file VarSchedulerMcsat.h.

Here is the call graph for this function:

◆ pop()

template<int lookahead, mcsat::VariableOrdering vot>
Minisat::Lit smtrat::VarSchedulerMcsatUnivariateConstraintsOnly< lookahead, vot >::pop ( )
inline

Definition at line 379 of file VarSchedulerMcsat.h.

Here is the call graph for this function:

◆ print()

template<int lookahead, mcsat::VariableOrdering vot>
void smtrat::VarSchedulerMcsatUnivariateConstraintsOnly< lookahead, vot >::print ( ) const
inline

Definition at line 411 of file VarSchedulerMcsat.h.

Here is the call graph for this function:

◆ rebuild()

template<int lookahead, mcsat::VariableOrdering vot>
void smtrat::VarSchedulerMcsatUnivariateConstraintsOnly< lookahead, vot >::rebuild ( )
inline

Definition at line 352 of file VarSchedulerMcsat.h.

Here is the call graph for this function:

◆ rebuildActivities()

template<int lookahead, mcsat::VariableOrdering vot>
void smtrat::VarSchedulerMcsatUnivariateConstraintsOnly< lookahead, vot >::rebuildActivities ( )
inline

Definition at line 426 of file VarSchedulerMcsat.h.

Here is the call graph for this function:

◆ rebuildTheoryVars()

template<int lookahead, mcsat::VariableOrdering vot>
template<typename Constraints >
void smtrat::VarSchedulerMcsatUnivariateConstraintsOnly< lookahead, vot >::rebuildTheoryVars ( const Constraints &  c)
inline

Definition at line 431 of file VarSchedulerMcsat.h.

Here is the call graph for this function:

◆ relocateClauses()

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

Definition at line 110 of file VarScheduler.h.

◆ varCmp()

template<int lookahead, mcsat::VariableOrdering vot>
bool smtrat::VarSchedulerMcsatUnivariateConstraintsOnly< lookahead, vot >::varCmp ( Minisat::Var  x,
Minisat::Var  y 
)
inlineprivate

Definition at line 333 of file VarSchedulerMcsat.h.

◆ varDecidable()

template<int lookahead, mcsat::VariableOrdering vot>
bool smtrat::VarSchedulerMcsatUnivariateConstraintsOnly< lookahead, vot >::varDecidable ( Minisat::Var  x)
inlineprivate

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

◆ boolean_ordering

template<int lookahead, mcsat::VariableOrdering vot>
VarSchedulerMinisat smtrat::VarSchedulerMcsatUnivariateConstraintsOnly< lookahead, vot >::boolean_ordering
private

Definition at line 330 of file VarSchedulerMcsat.h.

◆ carlVar

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

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
protectedinherited

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
protectedinherited

Definition at line 15 of file VarSchedulerMcsat.h.

◆ minisatVar

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

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.

◆ theory_ordering

template<int lookahead, mcsat::VariableOrdering vot>
TheoryVarSchedulerStatic<vot> smtrat::VarSchedulerMcsatUnivariateConstraintsOnly< lookahead, vot >::theory_ordering
private

Definition at line 331 of file VarSchedulerMcsat.h.

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