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

Scheduler for SMT, implementing theory guided heuristics. More...

#include <VarScheduler.h>

Inheritance diagram for smtrat::VarSchedulerSMTTheoryGuided< theory_conflict_guided_decision_heuristic >:
Inheritance graph
[legend]
Collaboration diagram for smtrat::VarSchedulerSMTTheoryGuided< theory_conflict_guided_decision_heuristic >:
Collaboration graph
[legend]

Public Member Functions

template<typename BaseModule >
 VarSchedulerSMTTheoryGuided (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 &)
 
void attachClause (Minisat::CRef)
 
void detachClause (Minisat::CRef)
 
void relocateClauses (std::function< void(Minisat::CRef &)>)
 

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

VarSchedulerMinisat minisat
 

Detailed Description

template<TheoryGuidedDecisionHeuristicLevel theory_conflict_guided_decision_heuristic>
class smtrat::VarSchedulerSMTTheoryGuided< theory_conflict_guided_decision_heuristic >

Scheduler for SMT, implementing theory guided heuristics.

Definition at line 308 of file VarScheduler.h.

Constructor & Destructor Documentation

◆ VarSchedulerSMTTheoryGuided()

template<TheoryGuidedDecisionHeuristicLevel theory_conflict_guided_decision_heuristic>
template<typename BaseModule >
smtrat::VarSchedulerSMTTheoryGuided< theory_conflict_guided_decision_heuristic >::VarSchedulerSMTTheoryGuided ( BaseModule &  baseModule)
inlineexplicit

Definition at line 313 of file VarScheduler.h.

Member Function Documentation

◆ attachClause()

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

Definition at line 104 of file VarScheduler.h.

◆ decreaseActivity()

template<TheoryGuidedDecisionHeuristicLevel theory_conflict_guided_decision_heuristic>
void smtrat::VarSchedulerSMTTheoryGuided< theory_conflict_guided_decision_heuristic >::decreaseActivity ( Minisat::Var  var)
inline

Definition at line 405 of file VarScheduler.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<TheoryGuidedDecisionHeuristicLevel theory_conflict_guided_decision_heuristic>
bool smtrat::VarSchedulerSMTTheoryGuided< theory_conflict_guided_decision_heuristic >::empty ( )
inline

Definition at line 391 of file VarScheduler.h.

Here is the call graph for this function:

◆ increaseActivity()

template<TheoryGuidedDecisionHeuristicLevel theory_conflict_guided_decision_heuristic>
void smtrat::VarSchedulerSMTTheoryGuided< theory_conflict_guided_decision_heuristic >::increaseActivity ( Minisat::Var  var)
inline

Definition at line 401 of file VarScheduler.h.

Here is the call graph for this function:

◆ insert()

template<TheoryGuidedDecisionHeuristicLevel theory_conflict_guided_decision_heuristic>
void smtrat::VarSchedulerSMTTheoryGuided< theory_conflict_guided_decision_heuristic >::insert ( Minisat::Var  var)
inline

Definition at line 322 of file VarScheduler.h.

Here is the call graph for this function:

◆ pop()

template<TheoryGuidedDecisionHeuristicLevel theory_conflict_guided_decision_heuristic>
Minisat::Lit smtrat::VarSchedulerSMTTheoryGuided< theory_conflict_guided_decision_heuristic >::pop ( )
inline

Definition at line 326 of file VarScheduler.h.

Here is the call graph for this function:

◆ print()

template<TheoryGuidedDecisionHeuristicLevel theory_conflict_guided_decision_heuristic>
void smtrat::VarSchedulerSMTTheoryGuided< theory_conflict_guided_decision_heuristic >::print ( ) const
inline

Definition at line 395 of file VarScheduler.h.

Here is the call graph for this function:

◆ rebuild()

template<TheoryGuidedDecisionHeuristicLevel theory_conflict_guided_decision_heuristic>
void smtrat::VarSchedulerSMTTheoryGuided< theory_conflict_guided_decision_heuristic >::rebuild ( )
inline

Definition at line 318 of file VarScheduler.h.

Here is the call graph for this function:

◆ rebuildActivities()

template<TheoryGuidedDecisionHeuristicLevel theory_conflict_guided_decision_heuristic>
void smtrat::VarSchedulerSMTTheoryGuided< theory_conflict_guided_decision_heuristic >::rebuildActivities ( )
inline

Definition at line 409 of file VarScheduler.h.

Here is the call graph for this function:

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

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

◆ minisat

template<TheoryGuidedDecisionHeuristicLevel theory_conflict_guided_decision_heuristic>
VarSchedulerMinisat smtrat::VarSchedulerSMTTheoryGuided< theory_conflict_guided_decision_heuristic >::minisat
private

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

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