SMT-RAT
24.02
Toolbox for Strategic and Parallel Satisfiability-Modulo-Theories Solving
|
Activity-based scheduler preferring initially theory variables. More...
#include <VarSchedulerMcsat.h>
Public Member Functions | |
template<typename BaseModule > | |
VarSchedulerMcsatActivityPreferTheory (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 &)>) |
Private Member Functions | |
auto | compareVars (Minisat::Var x, Minisat::Var y) |
Private Attributes | |
bool | initialized = false |
std::vector< Minisat::Var > | theory_ordering |
VarSchedulerMinisat | ordering |
Activity-based scheduler preferring initially theory variables.
Definition at line 716 of file VarSchedulerMcsat.h.
|
inlineexplicit |
Definition at line 740 of file VarSchedulerMcsat.h.
|
inlineinherited |
Definition at line 104 of file VarScheduler.h.
|
inlineprivate |
|
inline |
|
inlineinherited |
Definition at line 107 of file VarScheduler.h.
|
inline |
|
inline |
|
inline |
|
inline |
|
inline |
|
inline |
|
inline |
|
inline |
Definition at line 792 of file VarSchedulerMcsat.h.
|
inlineinherited |
Definition at line 110 of file VarScheduler.h.
|
protectedinherited |
Definition at line 31 of file VarScheduler.h.
|
protectedinherited |
Definition at line 30 of file VarScheduler.h.
|
protectedinherited |
Definition at line 16 of file VarSchedulerMcsat.h.
|
protectedinherited |
Definition at line 29 of file VarScheduler.h.
|
protectedinherited |
Definition at line 18 of file VarSchedulerMcsat.h.
|
protectedinherited |
Definition at line 18 of file VarScheduler.h.
|
protectedinherited |
Definition at line 28 of file VarScheduler.h.
|
protectedinherited |
Definition at line 27 of file VarScheduler.h.
|
protectedinherited |
Definition at line 26 of file VarScheduler.h.
|
protectedinherited |
Definition at line 19 of file VarScheduler.h.
|
private |
Definition at line 717 of file VarSchedulerMcsat.h.
|
protectedinherited |
Definition at line 32 of file VarScheduler.h.
|
protectedinherited |
Definition at line 22 of file VarScheduler.h.
|
protectedinherited |
Definition at line 21 of file VarScheduler.h.
|
protectedinherited |
Definition at line 23 of file VarScheduler.h.
|
protectedinherited |
Definition at line 15 of file VarSchedulerMcsat.h.
|
protectedinherited |
Definition at line 17 of file VarSchedulerMcsat.h.
|
private |
Definition at line 719 of file VarSchedulerMcsat.h.
|
protectedinherited |
Definition at line 25 of file VarScheduler.h.
|
protectedinherited |
Definition at line 24 of file VarScheduler.h.
|
protectedinherited |
Definition at line 20 of file VarScheduler.h.
|
private |
Definition at line 718 of file VarSchedulerMcsat.h.