Schedules theory variables statically. More...

#include <VarSchedulerMcsat.h>

Inheritance diagram for smtrat::TheoryVarSchedulerStatic< vot >:

Collaboration diagram for smtrat::TheoryVarSchedulerStatic< vot >:

[legend]

Public Member Functions
template<typename BaseModule >
	TheoryVarSchedulerStatic (BaseModule &baseModule)

void	insert (Minisat::Var var)

bool	empty ()

Minisat::Lit	pop ()

void	print () const

template<typename Constraints >
void	rebuildTheoryVars (const Constraints &c)

size_t	level ()
	Level of the next theory variable. More...

size_t	univariateLevel (Minisat::Var v)
	Returns the level in which the given constraint is univariate. More...

void	rebuild ()
	Rebuild heap. More...

void	increaseActivity (Minisat::Var)

void	decreaseActivity (Minisat::Var)

void	rebuildActivities ()

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 Attributes
std::vector< Minisat::Var >	ordering

std::vector< Minisat::Var >::const_iterator	nextTheoryVar = ordering.end()

bool	initialized = false

Detailed Description

template<mcsat::VariableOrdering vot>
class smtrat::TheoryVarSchedulerStatic< vot >

Schedules theory variables statically.

Should not be used directly.

Definition at line 39 of file VarSchedulerMcsat.h.

Constructor & Destructor Documentation

◆ TheoryVarSchedulerStatic()

template<mcsat::VariableOrdering vot>

template<typename BaseModule >

smtrat::TheoryVarSchedulerStatic< vot >::TheoryVarSchedulerStatic ( BaseModule & baseModule )

inlineexplicit

Definition at line 47 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()

template<mcsat::VariableOrdering vot>

bool smtrat::TheoryVarSchedulerStatic< vot >::empty ( )

inline

Definition at line 60 of file VarSchedulerMcsat.h.

Here is the caller graph for this function:

◆ increaseActivity()

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

inlineinherited

Definition at line 91 of file VarScheduler.h.

◆ insert()

template<mcsat::VariableOrdering vot>

void smtrat::TheoryVarSchedulerStatic< vot >::insert ( Minisat::Var var )

inline

Definition at line 51 of file VarSchedulerMcsat.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ level()

template<mcsat::VariableOrdering vot>

size_t smtrat::TheoryVarSchedulerStatic< vot >::level ( )

inline

Level of the next theory variable.

Definition at line 107 of file VarSchedulerMcsat.h.

◆ pop()

template<mcsat::VariableOrdering vot>

Minisat::Lit smtrat::TheoryVarSchedulerStatic< vot >::pop ( )

inline

Definition at line 70 of file VarSchedulerMcsat.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ print()

template<mcsat::VariableOrdering vot>

void smtrat::TheoryVarSchedulerStatic< vot >::print ( ) const

inline

Definition at line 85 of file VarSchedulerMcsat.h.

Here is the caller graph for this function:

◆ 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<mcsat::VariableOrdering vot>

template<typename Constraints >

void smtrat::TheoryVarSchedulerStatic< vot >::rebuildTheoryVars ( const Constraints & c )

inline

Definition at line 90 of file VarSchedulerMcsat.h.

Here is the caller graph for this function:

◆ relocateClauses()

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

inlineinherited

Definition at line 110 of file VarScheduler.h.

◆ univariateLevel()

template<mcsat::VariableOrdering vot>

size_t smtrat::TheoryVarSchedulerStatic< vot >::univariateLevel ( Minisat::Var v )

inline

Returns the level in which the given constraint is univariate.

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

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

◆ initialized

template<mcsat::VariableOrdering vot>

bool smtrat::TheoryVarSchedulerStatic< vot >::initialized = false

private

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

◆ nextTheoryVar

template<mcsat::VariableOrdering vot>

std::vector<Minisat::Var>::const_iterator smtrat::TheoryVarSchedulerStatic< vot >::nextTheoryVar = ordering.end()

private

Definition at line 41 of file VarSchedulerMcsat.h.

◆ ordering

template<mcsat::VariableOrdering vot>

std::vector<Minisat::Var> smtrat::TheoryVarSchedulerStatic< vot >::ordering

private

Definition at line 40 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:

smtrat-modules/SATModule/mcsat/VarSchedulerMcsat.h

Public Member Functions

Protected Attributes

Private Attributes

Detailed Description

template<mcsat::VariableOrdering vot> class smtrat::TheoryVarSchedulerStatic< vot >

Constructor & Destructor Documentation

◆ TheoryVarSchedulerStatic()

Member Function Documentation

◆ attachClause()

◆ decreaseActivity()

◆ detachClause()

◆ empty()

◆ increaseActivity()

◆ insert()

◆ level()

◆ pop()

◆ print()

◆ rebuild()

◆ rebuildActivities()

◆ rebuildTheoryVars()

◆ relocateClauses()

◆ univariateLevel()

Field Documentation

◆ abstractLiteral

◆ abstractVariable

◆ carlVar

◆ currentlySatisfiedByBackend

◆ currentModel

◆ getActivity

◆ getBoolLitValue

◆ getBoolVarValue

◆ getClause

◆ getPolarity

◆ initialized

◆ isAbstractedFormula

◆ isBoolValueUndef

◆ isDecisionVar

◆ isTheoryAbstraction

◆ isTheoryVar

◆ minisatVar

◆ nextTheoryVar

◆ ordering

◆ reabstractLiteral

◆ reabstractVariable

◆ setPolarity

template<mcsat::VariableOrdering vot>
class smtrat::TheoryVarSchedulerStatic< vot >