Variable scheduling that all decides theory variables first before deciding any Boolean variable. More...

#include <VarSchedulerMcsat.h>

Inheritance diagram for smtrat::VarSchedulerMcsatTheoryFirst< TheoryScheduler >:

Collaboration diagram for smtrat::VarSchedulerMcsatTheoryFirst< TheoryScheduler >:

[legend]

Public Member Functions
template<typename BaseModule >
	VarSchedulerMcsatTheoryFirst (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 Attributes
VarSchedulerMinisat	boolean_ordering

TheoryScheduler	theory_ordering

Detailed Description

template<typename TheoryScheduler>
class smtrat::VarSchedulerMcsatTheoryFirst< TheoryScheduler >

Variable scheduling that all decides theory variables first before deciding any Boolean variable.

Definition at line 231 of file VarSchedulerMcsat.h.

Constructor & Destructor Documentation

◆ VarSchedulerMcsatTheoryFirst()

template<typename TheoryScheduler >

template<typename BaseModule >

smtrat::VarSchedulerMcsatTheoryFirst< TheoryScheduler >::VarSchedulerMcsatTheoryFirst ( BaseModule & baseModule )

inlineexplicit

Definition at line 238 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<typename TheoryScheduler >

void smtrat::VarSchedulerMcsatTheoryFirst< TheoryScheduler >::decreaseActivity ( Minisat::Var var )

inline

Definition at line 308 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<typename TheoryScheduler >

bool smtrat::VarSchedulerMcsatTheoryFirst< TheoryScheduler >::empty ( )

inline

Definition at line 282 of file VarSchedulerMcsat.h.

Here is the call graph for this function:

◆ increaseActivity()

template<typename TheoryScheduler >

void smtrat::VarSchedulerMcsatTheoryFirst< TheoryScheduler >::increaseActivity ( Minisat::Var var )

inline

Definition at line 303 of file VarSchedulerMcsat.h.

Here is the call graph for this function:

◆ insert()

template<typename TheoryScheduler >

void smtrat::VarSchedulerMcsatTheoryFirst< TheoryScheduler >::insert ( Minisat::Var var )

inline

Definition at line 249 of file VarSchedulerMcsat.h.

Here is the call graph for this function:

◆ pop()

template<typename TheoryScheduler >

Minisat::Lit smtrat::VarSchedulerMcsatTheoryFirst< TheoryScheduler >::pop ( )

inline

Definition at line 269 of file VarSchedulerMcsat.h.

Here is the call graph for this function:

◆ print()

template<typename TheoryScheduler >

void smtrat::VarSchedulerMcsatTheoryFirst< TheoryScheduler >::print ( ) const

inline

Definition at line 296 of file VarSchedulerMcsat.h.

Here is the call graph for this function:

◆ rebuild()

template<typename TheoryScheduler >

void smtrat::VarSchedulerMcsatTheoryFirst< TheoryScheduler >::rebuild ( )

inline

Definition at line 244 of file VarSchedulerMcsat.h.

Here is the call graph for this function:

◆ rebuildActivities()

template<typename TheoryScheduler >

void smtrat::VarSchedulerMcsatTheoryFirst< TheoryScheduler >::rebuildActivities ( )

inline

Definition at line 313 of file VarSchedulerMcsat.h.

Here is the call graph for this function:

◆ rebuildTheoryVars()

template<typename TheoryScheduler >

template<typename Constraints >

void smtrat::VarSchedulerMcsatTheoryFirst< TheoryScheduler >::rebuildTheoryVars ( const Constraints & c )

inline

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

◆ boolean_ordering

template<typename TheoryScheduler >

VarSchedulerMinisat smtrat::VarSchedulerMcsatTheoryFirst< TheoryScheduler >::boolean_ordering

private

Definition at line 232 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<typename TheoryScheduler >

TheoryScheduler smtrat::VarSchedulerMcsatTheoryFirst< TheoryScheduler >::theory_ordering

private

Definition at line 234 of file VarSchedulerMcsat.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<typename TheoryScheduler> class smtrat::VarSchedulerMcsatTheoryFirst< TheoryScheduler >

Constructor & Destructor Documentation

◆ VarSchedulerMcsatTheoryFirst()

Member Function Documentation

◆ attachClause()

◆ decreaseActivity()

◆ detachClause()

◆ empty()

◆ increaseActivity()

◆ insert()

◆ pop()

◆ print()

◆ rebuild()

◆ rebuildActivities()

◆ rebuildTheoryVars()

◆ relocateClauses()

Field Documentation

◆ abstractLiteral

◆ abstractVariable

◆ boolean_ordering

◆ carlVar

◆ currentlySatisfiedByBackend

◆ currentModel

◆ getActivity

◆ getBoolLitValue

◆ getBoolVarValue

◆ getClause

◆ getPolarity

◆ isAbstractedFormula

◆ isBoolValueUndef

◆ isDecisionVar

◆ isTheoryAbstraction

◆ isTheoryVar

◆ minisatVar

◆ reabstractLiteral

◆ reabstractVariable

◆ setPolarity

◆ theory_ordering

template<typename TheoryScheduler>
class smtrat::VarSchedulerMcsatTheoryFirst< TheoryScheduler >