SMT-RAT  24.02
Toolbox for Strategic and Parallel Satisfiability-Modulo-Theories Solving
Data Structures | Public Member Functions | Protected Attributes | Private Member Functions | Private Attributes
smtrat::VarSchedulerMcsatUnivariateClausesOnly< TheoryScheduler, respectActivities > Class Template Reference

Decides only Constraints occuring in clauses that are univariate in the current theory variable while the theory ordering is static. More...

#include <VarSchedulerMcsat.h>

Inheritance diagram for smtrat::VarSchedulerMcsatUnivariateClausesOnly< TheoryScheduler, respectActivities >:
Inheritance graph
[legend]
Collaboration diagram for smtrat::VarSchedulerMcsatUnivariateClausesOnly< TheoryScheduler, respectActivities >:
Collaboration graph
[legend]

Data Structures

struct  TheoryLevel
 

Public Member Functions

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

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 univariate (Minisat::CRef cl)
 
bool decidedByTheory (Minisat::CRef cl)
 
Minisat::Lit undefLitIn (Minisat::CRef cl)
 
Minisat::Lit pickBooleanVarFromCurrentLevel ()
 
Minisat::Lit pickBooleanVarFromUndecided ()
 
carl::Variable theoryDecision ()
 
bool pickNextTheoryVar ()
 
void popTheoryLevel ()
 

Private Attributes

std::vector< Minisat::CRef > mUndecidedClauses
 
std::vector< TheoryLevel > mTheoryLevels
 
TheoryScheduler theory_ordering
 

Detailed Description

template<typename TheoryScheduler, bool respectActivities>
class smtrat::VarSchedulerMcsatUnivariateClausesOnly< TheoryScheduler, respectActivities >

Decides only Constraints occuring in clauses that are univariate in the current theory variable while the theory ordering is static.

This corresponds to the original NLSAT strategy.

Definition at line 443 of file VarSchedulerMcsat.h.

Constructor & Destructor Documentation

◆ VarSchedulerMcsatUnivariateClausesOnly()

template<typename TheoryScheduler , bool respectActivities>
template<typename BaseModule >
smtrat::VarSchedulerMcsatUnivariateClausesOnly< TheoryScheduler, respectActivities >::VarSchedulerMcsatUnivariateClausesOnly ( BaseModule &  baseModule)
inlineexplicit

Definition at line 637 of file VarSchedulerMcsat.h.

Member Function Documentation

◆ attachClause()

template<typename TheoryScheduler , bool respectActivities>
void smtrat::VarSchedulerMcsatUnivariateClausesOnly< TheoryScheduler, respectActivities >::attachClause ( Minisat::CRef  cl)
inline

Definition at line 605 of file VarSchedulerMcsat.h.

◆ decidedByTheory()

template<typename TheoryScheduler , bool respectActivities>
bool smtrat::VarSchedulerMcsatUnivariateClausesOnly< TheoryScheduler, respectActivities >::decidedByTheory ( Minisat::CRef  cl)
inlineprivate

Definition at line 476 of file VarSchedulerMcsat.h.

Here is the call graph for this function:

◆ decreaseActivity()

template<typename TheoryScheduler , bool respectActivities>
void smtrat::VarSchedulerMcsatUnivariateClausesOnly< TheoryScheduler, respectActivities >::decreaseActivity ( Minisat::Var  var)
inline

Definition at line 695 of file VarSchedulerMcsat.h.

Here is the call graph for this function:

◆ detachClause()

template<typename TheoryScheduler , bool respectActivities>
void smtrat::VarSchedulerMcsatUnivariateClausesOnly< TheoryScheduler, respectActivities >::detachClause ( Minisat::CRef  cl)
inline

Definition at line 616 of file VarSchedulerMcsat.h.

Here is the call graph for this function:

◆ empty()

template<typename TheoryScheduler , bool respectActivities>
bool smtrat::VarSchedulerMcsatUnivariateClausesOnly< TheoryScheduler, respectActivities >::empty ( )
inline

Definition at line 677 of file VarSchedulerMcsat.h.

◆ increaseActivity()

template<typename TheoryScheduler , bool respectActivities>
void smtrat::VarSchedulerMcsatUnivariateClausesOnly< TheoryScheduler, respectActivities >::increaseActivity ( Minisat::Var  var)
inline

Definition at line 691 of file VarSchedulerMcsat.h.

Here is the call graph for this function:

◆ insert()

template<typename TheoryScheduler , bool respectActivities>
void smtrat::VarSchedulerMcsatUnivariateClausesOnly< TheoryScheduler, respectActivities >::insert ( Minisat::Var  var)
inline

Definition at line 648 of file VarSchedulerMcsat.h.

Here is the call graph for this function:

◆ pickBooleanVarFromCurrentLevel()

template<typename TheoryScheduler , bool respectActivities>
Minisat::Lit smtrat::VarSchedulerMcsatUnivariateClausesOnly< TheoryScheduler, respectActivities >::pickBooleanVarFromCurrentLevel ( )
inlineprivate

Definition at line 518 of file VarSchedulerMcsat.h.

Here is the call graph for this function:

◆ pickBooleanVarFromUndecided()

template<typename TheoryScheduler , bool respectActivities>
Minisat::Lit smtrat::VarSchedulerMcsatUnivariateClausesOnly< TheoryScheduler, respectActivities >::pickBooleanVarFromUndecided ( )
inlineprivate

Definition at line 536 of file VarSchedulerMcsat.h.

Here is the call graph for this function:

◆ pickNextTheoryVar()

template<typename TheoryScheduler , bool respectActivities>
bool smtrat::VarSchedulerMcsatUnivariateClausesOnly< TheoryScheduler, respectActivities >::pickNextTheoryVar ( )
inlineprivate

Definition at line 563 of file VarSchedulerMcsat.h.

Here is the call graph for this function:

◆ pop()

template<typename TheoryScheduler , bool respectActivities>
Minisat::Lit smtrat::VarSchedulerMcsatUnivariateClausesOnly< TheoryScheduler, respectActivities >::pop ( )
inline

Definition at line 661 of file VarSchedulerMcsat.h.

Here is the call graph for this function:

◆ popTheoryLevel()

template<typename TheoryScheduler , bool respectActivities>
void smtrat::VarSchedulerMcsatUnivariateClausesOnly< TheoryScheduler, respectActivities >::popTheoryLevel ( )
inlineprivate

Definition at line 589 of file VarSchedulerMcsat.h.

◆ print()

template<typename TheoryScheduler , bool respectActivities>
void smtrat::VarSchedulerMcsatUnivariateClausesOnly< TheoryScheduler, respectActivities >::print ( ) const
inline

Definition at line 681 of file VarSchedulerMcsat.h.

◆ rebuild()

template<typename TheoryScheduler , bool respectActivities>
void smtrat::VarSchedulerMcsatUnivariateClausesOnly< TheoryScheduler, respectActivities >::rebuild ( )
inline

Definition at line 644 of file VarSchedulerMcsat.h.

◆ rebuildActivities()

template<typename TheoryScheduler , bool respectActivities>
void smtrat::VarSchedulerMcsatUnivariateClausesOnly< TheoryScheduler, respectActivities >::rebuildActivities ( )
inline

Definition at line 699 of file VarSchedulerMcsat.h.

◆ rebuildTheoryVars()

template<typename TheoryScheduler , bool respectActivities>
template<typename Constraints >
void smtrat::VarSchedulerMcsatUnivariateClausesOnly< TheoryScheduler, respectActivities >::rebuildTheoryVars ( const Constraints &  c)
inline

Definition at line 704 of file VarSchedulerMcsat.h.

◆ relocateClauses()

template<typename TheoryScheduler , bool respectActivities>
void smtrat::VarSchedulerMcsatUnivariateClausesOnly< TheoryScheduler, respectActivities >::relocateClauses ( std::function< void(Minisat::CRef &)>  relocate)
inline

Definition at line 623 of file VarSchedulerMcsat.h.

◆ theoryDecision()

template<typename TheoryScheduler , bool respectActivities>
carl::Variable smtrat::VarSchedulerMcsatUnivariateClausesOnly< TheoryScheduler, respectActivities >::theoryDecision ( )
inlineprivate

Definition at line 554 of file VarSchedulerMcsat.h.

◆ undefLitIn()

template<typename TheoryScheduler , bool respectActivities>
Minisat::Lit smtrat::VarSchedulerMcsatUnivariateClausesOnly< TheoryScheduler, respectActivities >::undefLitIn ( Minisat::CRef  cl)
inlineprivate

Definition at line 491 of file VarSchedulerMcsat.h.

Here is the call graph for this function:

◆ univariate()

template<typename TheoryScheduler , bool respectActivities>
bool smtrat::VarSchedulerMcsatUnivariateClausesOnly< TheoryScheduler, respectActivities >::univariate ( Minisat::CRef  cl)
inlineprivate

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

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

◆ mTheoryLevels

template<typename TheoryScheduler , bool respectActivities>
std::vector<TheoryLevel> smtrat::VarSchedulerMcsatUnivariateClausesOnly< TheoryScheduler, respectActivities >::mTheoryLevels
private

Definition at line 513 of file VarSchedulerMcsat.h.

◆ mUndecidedClauses

template<typename TheoryScheduler , bool respectActivities>
std::vector<Minisat::CRef> smtrat::VarSchedulerMcsatUnivariateClausesOnly< TheoryScheduler, respectActivities >::mUndecidedClauses
private

Definition at line 512 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 , bool respectActivities>
TheoryScheduler smtrat::VarSchedulerMcsatUnivariateClausesOnly< TheoryScheduler, respectActivities >::theory_ordering
private

Definition at line 515 of file VarSchedulerMcsat.h.

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