Open
Graph Drawing
Framework

  v. 2023.09 (Elderberry)
 
Overview Class Hierarchy Class Index Class List Members Namespaces Source Files

Classes | Public Types | Public Member Functions | Public Attributes | Protected Member Functions | Static Protected Member Functions | Protected Attributes | List of all members
Minisat::Internal::Solver Class Reference

#include <ogdf/lib/minisat/core/Solver.h>

+ Inheritance diagram for Minisat::Internal::Solver:

Classes

struct  SolverStatus
 
struct  VarData
 
struct  VarOrderLt
 
struct  Watcher
 
struct  WatcherDeleted
 

Public Types

enum  AnswerType { A_TRUE, A_FALSE, A_UNDEF }
 

Public Member Functions

 Solver ()
 
virtual ~Solver ()
 
bool addClause (const vec< Lit > &ps)
 
bool addClause (Lit p)
 
bool addClause (Lit p, Lit q)
 
bool addClause (Lit p, Lit q, Lit r)
 
bool addClause_ (vec< Lit > &ps)
 
bool addEmptyClause ()
 
void budgetOff ()
 
void checkGarbage ()
 
void checkGarbage (double gf)
 
void clearInterrupt ()
 
virtual void garbageCollect ()
 
void interrupt ()
 
lbool modelValue (Lit p) const
 
lbool modelValue (Var x) const
 
int nAssigns () const
 
int nClauses () const
 
Var newVar (bool polarity=true, bool dvar=true)
 
int nFreeVars () const
 
int nLearnts () const
 
int nVars () const
 
bool okay () const
 
void setConfBudget (int64_t x)
 
void setDecisionVar (Var v, bool b)
 
void setPolarity (Var v, bool b)
 
void setPropBudget (int64_t x)
 
bool simplify ()
 
bool solve ()
 
bool solve (const vec< Lit > &assumps)
 
bool solve (double t, SolverStatus &st)
 
bool solve (Lit p)
 
bool solve (Lit p, Lit q)
 
bool solve (Lit p, Lit q, Lit r)
 
lbool solveLimited (const vec< Lit > &assumps)
 
void toDimacs (const char *file)
 
void toDimacs (const char *file, const vec< Lit > &assumps)
 
void toDimacs (const char *file, Lit p)
 
void toDimacs (const char *file, Lit p, Lit q)
 
void toDimacs (const char *file, Lit p, Lit q, Lit r)
 
void toDimacs (std::ostream &out, Clause &c, vec< Var > &map, Var &max)
 
void toDimacs (std::ostream &out, const vec< Lit > &assumps)
 
lbool value (Lit p) const
 
lbool value (Var x) const
 

Public Attributes

int ccmin_mode
 
double clause_decay
 
uint64_t clauses_literals
 
vec< Lit > conflict
 
uint64_t conflicts
 
uint64_t dec_vars
 
uint64_t decisions
 
double garbage_frac
 
uint64_t learnts_literals
 
double learntsize_adjust_inc
 
int learntsize_adjust_start_confl
 
double learntsize_factor
 
double learntsize_inc
 
bool luby_restart
 
uint64_t max_literals
 
vec< lbool > model
 
int phase_saving
 
uint64_t propagations
 
double random_seed
 
double random_var_freq
 
int restart_first
 
double restart_inc
 
uint64_t rnd_decisions
 
bool rnd_init_act
 
bool rnd_pol
 
uint64_t solves
 
uint64_t starts
 
uint64_t tot_literals
 
double var_decay
 
int verbosity
 

Protected Member Functions

uint32_t abstractLevel (Var x) const
 
void analyze (CRef confl, vec< Lit > &out_learnt, int &out_btlevel)
 
void analyzeFinal (Lit p, vec< Lit > &out_conflict)
 
void attachClause (CRef cr)
 
void cancelUntil (int level)
 
void claBumpActivity (Clause &c)
 
void claDecayActivity ()
 
int decisionLevel () const
 
void detachClause (CRef cr, bool strict=false)
 
bool enqueue (Lit p, CRef from=CRef_Undef)
 
void insertVarOrder (Var x)
 
int level (Var x) const
 
bool litRedundant (Lit p, uint32_t abstract_levels)
 
bool locked (const Clause &c) const
 
void newDecisionLevel ()
 
Lit pickBranchLit ()
 
double progressEstimate () const
 
CRef propagate ()
 
CRef reason (Var x) const
 
void rebuildOrderHeap ()
 
void reduceDB ()
 
void relocAll (ClauseAllocator &to)
 
void removeClause (CRef cr)
 
void removeSatisfied (vec< CRef > &cs)
 
bool satisfied (const Clause &c) const
 
lbool search (int nof_conflicts)
 
lbool search (int nof_conflicts, double &time)
 
lbool solve_ ()
 
lbool solve_ (double &t)
 
void uncheckedEnqueue (Lit p, CRef from=CRef_Undef)
 
void varBumpActivity (Var v)
 
void varBumpActivity (Var v, double inc)
 
void varDecayActivity ()
 
bool withinBudget () const
 

Static Protected Member Functions

static double drand (double &seed)
 
static int irand (double &seed, int size)
 
static VarData mkVarData (CRef cr, int l)
 

Protected Attributes

vec< double > activity
 
vec< Lit > add_tmp
 
vec< Lit > analyze_stack
 
vec< Lit > analyze_toclear
 
vec< lbool > assigns
 
vec< Lit > assumptions
 
bool asynch_interrupt
 
ClauseAllocator ca
 
double cla_inc
 
vec< CRef > clauses
 
int64_t conflict_budget
 
vec< char > decision
 
vec< CRef > learnts
 
int learntsize_adjust_cnt
 
double learntsize_adjust_confl
 
double max_learnts
 
bool ok
 
Heap< VarOrderLt > order_heap
 
vec< char > polarity
 
double progress_estimate
 
int64_t propagation_budget
 
int qhead
 
bool remove_satisfied
 
vec< char > seen
 
int simpDB_assigns
 
int64_t simpDB_props
 
vec< Lit > trail
 
vec< int > trail_lim
 
double var_inc
 
vec< VarData > vardata
 
OccLists< Lit, vec< Watcher >, WatcherDeleted > watches
 

Detailed Description

Definition at line 36 of file Solver.h.

Member Enumeration Documentation

◆ AnswerType

enum Minisat::Internal::Solver::AnswerType
Enumerator
A_TRUE 
A_FALSE 
A_UNDEF 

Definition at line 57 of file Solver.h.

Constructor & Destructor Documentation

◆ Solver()

Minisat::Internal::Solver::Solver ( )

◆ ~Solver()

virtual Minisat::Internal::Solver::~Solver ( )
virtual

Member Function Documentation

◆ abstractLevel()

uint32_t Minisat::Internal::Solver::abstractLevel ( Var  x) const
inlineprotected

Definition at line 338 of file Solver.h.

◆ addClause() [1/4]

bool Minisat::Internal::Solver::addClause ( const vec< Lit > &  ps)
inline

Definition at line 329 of file Solver.h.

◆ addClause() [2/4]

bool Minisat::Internal::Solver::addClause ( Lit  p)
inline

Definition at line 331 of file Solver.h.

◆ addClause() [3/4]

bool Minisat::Internal::Solver::addClause ( Lit  p,
Lit  q 
)
inline

Definition at line 332 of file Solver.h.

◆ addClause() [4/4]

bool Minisat::Internal::Solver::addClause ( Lit  p,
Lit  q,
Lit  r 
)
inline

Definition at line 333 of file Solver.h.

◆ addClause_()

bool Minisat::Internal::Solver::addClause_ ( vec< Lit > &  ps)

◆ addEmptyClause()

bool Minisat::Internal::Solver::addEmptyClause ( )
inline

Definition at line 330 of file Solver.h.

◆ analyze()

void Minisat::Internal::Solver::analyze ( CRef  confl,
vec< Lit > &  out_learnt,
int &  out_btlevel 
)
protected

◆ analyzeFinal()

void Minisat::Internal::Solver::analyzeFinal ( Lit  p,
vec< Lit > &  out_conflict 
)
protected

◆ attachClause()

void Minisat::Internal::Solver::attachClause ( CRef  cr)
protected

◆ budgetOff()

void Minisat::Internal::Solver::budgetOff ( )
inline

Definition at line 361 of file Solver.h.

◆ cancelUntil()

void Minisat::Internal::Solver::cancelUntil ( int  level)
protected

◆ checkGarbage() [1/2]

void Minisat::Internal::Solver::checkGarbage ( )
inline

Definition at line 322 of file Solver.h.

◆ checkGarbage() [2/2]

void Minisat::Internal::Solver::checkGarbage ( double  gf)
inline

Definition at line 323 of file Solver.h.

◆ claBumpActivity()

void Minisat::Internal::Solver::claBumpActivity ( Clause &  c)
inlineprotected

Definition at line 315 of file Solver.h.

◆ claDecayActivity()

void Minisat::Internal::Solver::claDecayActivity ( )
inlineprotected

Definition at line 314 of file Solver.h.

◆ clearInterrupt()

void Minisat::Internal::Solver::clearInterrupt ( )
inline

Definition at line 360 of file Solver.h.

◆ decisionLevel()

int Minisat::Internal::Solver::decisionLevel ( ) const
inlineprotected

Definition at line 337 of file Solver.h.

◆ detachClause()

void Minisat::Internal::Solver::detachClause ( CRef  cr,
bool  strict = false 
)
protected

◆ drand()

static double Minisat::Internal::Solver::drand ( double &  seed)
inlinestaticprotected

Definition at line 280 of file Solver.h.

◆ enqueue()

bool Minisat::Internal::Solver::enqueue ( Lit  p,
CRef  from = CRef_Undef 
)
inlineprotected

Definition at line 328 of file Solver.h.

◆ garbageCollect()

virtual void Minisat::Internal::Solver::garbageCollect ( )
virtual

Reimplemented in Minisat::Internal::SimpSolver.

◆ insertVarOrder()

void Minisat::Internal::Solver::insertVarOrder ( Var  x)
inlineprotected

Definition at line 298 of file Solver.h.

◆ interrupt()

void Minisat::Internal::Solver::interrupt ( )
inline

Definition at line 359 of file Solver.h.

◆ irand()

static int Minisat::Internal::Solver::irand ( double &  seed,
int  size 
)
inlinestaticprotected

Definition at line 287 of file Solver.h.

◆ level()

int Minisat::Internal::Solver::level ( Var  x) const
inlineprotected

Definition at line 296 of file Solver.h.

◆ litRedundant()

bool Minisat::Internal::Solver::litRedundant ( Lit  p,
uint32_t  abstract_levels 
)
protected

◆ locked()

bool Minisat::Internal::Solver::locked ( const Clause &  c) const
inlineprotected

Definition at line 334 of file Solver.h.

◆ mkVarData()

static VarData Minisat::Internal::Solver::mkVarData ( CRef  cr,
int  l 
)
inlinestaticprotected

Definition at line 162 of file Solver.h.

◆ modelValue() [1/2]

lbool Minisat::Internal::Solver::modelValue ( Lit  p) const
inline

Definition at line 342 of file Solver.h.

◆ modelValue() [2/2]

lbool Minisat::Internal::Solver::modelValue ( Var  x) const
inline

Definition at line 341 of file Solver.h.

◆ nAssigns()

int Minisat::Internal::Solver::nAssigns ( ) const
inline

Definition at line 343 of file Solver.h.

◆ nClauses()

int Minisat::Internal::Solver::nClauses ( ) const
inline

Definition at line 344 of file Solver.h.

◆ newDecisionLevel()

void Minisat::Internal::Solver::newDecisionLevel ( )
inlineprotected

Definition at line 335 of file Solver.h.

◆ newVar()

Var Minisat::Internal::Solver::newVar ( bool  polarity = true,
bool  dvar = true 
)

◆ nFreeVars()

int Minisat::Internal::Solver::nFreeVars ( ) const
inline

Definition at line 347 of file Solver.h.

◆ nLearnts()

int Minisat::Internal::Solver::nLearnts ( ) const
inline

Definition at line 345 of file Solver.h.

◆ nVars()

int Minisat::Internal::Solver::nVars ( ) const
inline

Definition at line 346 of file Solver.h.

◆ okay()

bool Minisat::Internal::Solver::okay ( ) const
inline

Definition at line 400 of file Solver.h.

◆ pickBranchLit()

Lit Minisat::Internal::Solver::pickBranchLit ( )
protected

◆ progressEstimate()

double Minisat::Internal::Solver::progressEstimate ( ) const
protected

◆ propagate()

CRef Minisat::Internal::Solver::propagate ( )
protected

◆ reason()

CRef Minisat::Internal::Solver::reason ( Var  x) const
inlineprotected

Definition at line 295 of file Solver.h.

◆ rebuildOrderHeap()

void Minisat::Internal::Solver::rebuildOrderHeap ( )
protected

◆ reduceDB()

void Minisat::Internal::Solver::reduceDB ( )
protected

◆ relocAll()

void Minisat::Internal::Solver::relocAll ( ClauseAllocator &  to)
protected

◆ removeClause()

void Minisat::Internal::Solver::removeClause ( CRef  cr)
protected

◆ removeSatisfied()

void Minisat::Internal::Solver::removeSatisfied ( vec< CRef > &  cs)
protected

◆ satisfied()

bool Minisat::Internal::Solver::satisfied ( const Clause &  c) const
protected

◆ search() [1/2]

lbool Minisat::Internal::Solver::search ( int  nof_conflicts)
protected

◆ search() [2/2]

lbool Minisat::Internal::Solver::search ( int  nof_conflicts,
double &  time 
)
protected

◆ setConfBudget()

void Minisat::Internal::Solver::setConfBudget ( int64_t  x)
inline

Definition at line 357 of file Solver.h.

◆ setDecisionVar()

void Minisat::Internal::Solver::setDecisionVar ( Var  v,
bool  b 
)
inline

Definition at line 349 of file Solver.h.

◆ setPolarity()

void Minisat::Internal::Solver::setPolarity ( Var  v,
bool  b 
)
inline

Definition at line 348 of file Solver.h.

◆ setPropBudget()

void Minisat::Internal::Solver::setPropBudget ( int64_t  x)
inline

Definition at line 358 of file Solver.h.

◆ simplify()

bool Minisat::Internal::Solver::simplify ( )

◆ solve() [1/6]

bool Minisat::Internal::Solver::solve ( )
inline

Definition at line 370 of file Solver.h.

◆ solve() [2/6]

bool Minisat::Internal::Solver::solve ( const vec< Lit > &  assumps)
inline

Definition at line 398 of file Solver.h.

◆ solve() [3/6]

bool Minisat::Internal::Solver::solve ( double  t,
SolverStatus &  st 
)
inline

Definition at line 371 of file Solver.h.

◆ solve() [4/6]

bool Minisat::Internal::Solver::solve ( Lit  p)
inline

Definition at line 395 of file Solver.h.

◆ solve() [5/6]

bool Minisat::Internal::Solver::solve ( Lit  p,
Lit  q 
)
inline

Definition at line 396 of file Solver.h.

◆ solve() [6/6]

bool Minisat::Internal::Solver::solve ( Lit  p,
Lit  q,
Lit  r 
)
inline

Definition at line 397 of file Solver.h.

◆ solve_() [1/2]

lbool Minisat::Internal::Solver::solve_ ( )
protected

◆ solve_() [2/2]

lbool Minisat::Internal::Solver::solve_ ( double &  t)
protected

◆ solveLimited()

lbool Minisat::Internal::Solver::solveLimited ( const vec< Lit > &  assumps)
inline

Definition at line 399 of file Solver.h.

◆ toDimacs() [1/7]

void Minisat::Internal::Solver::toDimacs ( const char *  file)
inline

Definition at line 402 of file Solver.h.

◆ toDimacs() [2/7]

void Minisat::Internal::Solver::toDimacs ( const char *  file,
const vec< Lit > &  assumps 
)

◆ toDimacs() [3/7]

void Minisat::Internal::Solver::toDimacs ( const char *  file,
Lit  p 
)
inline

Definition at line 403 of file Solver.h.

◆ toDimacs() [4/7]

void Minisat::Internal::Solver::toDimacs ( const char *  file,
Lit  p,
Lit  q 
)
inline

Definition at line 404 of file Solver.h.

◆ toDimacs() [5/7]

void Minisat::Internal::Solver::toDimacs ( const char *  file,
Lit  p,
Lit  q,
Lit  r 
)
inline

Definition at line 405 of file Solver.h.

◆ toDimacs() [6/7]

void Minisat::Internal::Solver::toDimacs ( std::ostream &  out,
Clause &  c,
vec< Var > &  map,
Var &  max 
)

◆ toDimacs() [7/7]

void Minisat::Internal::Solver::toDimacs ( std::ostream &  out,
const vec< Lit > &  assumps 
)

◆ uncheckedEnqueue()

void Minisat::Internal::Solver::uncheckedEnqueue ( Lit  p,
CRef  from = CRef_Undef 
)
protected

◆ value() [1/2]

lbool Minisat::Internal::Solver::value ( Lit  p) const
inline

Definition at line 340 of file Solver.h.

◆ value() [2/2]

lbool Minisat::Internal::Solver::value ( Var  x) const
inline

Definition at line 339 of file Solver.h.

◆ varBumpActivity() [1/2]

void Minisat::Internal::Solver::varBumpActivity ( Var  v)
inlineprotected

Definition at line 302 of file Solver.h.

◆ varBumpActivity() [2/2]

void Minisat::Internal::Solver::varBumpActivity ( Var  v,
double  inc 
)
inlineprotected

Definition at line 303 of file Solver.h.

◆ varDecayActivity()

void Minisat::Internal::Solver::varDecayActivity ( )
inlineprotected

Definition at line 301 of file Solver.h.

◆ withinBudget()

bool Minisat::Internal::Solver::withinBudget ( ) const
inlineprotected

Definition at line 362 of file Solver.h.

Member Data Documentation

◆ activity

vec<double> Minisat::Internal::Solver::activity
protected

Definition at line 191 of file Solver.h.

◆ add_tmp

vec<Lit> Minisat::Internal::Solver::add_tmp
protected

Definition at line 217 of file Solver.h.

◆ analyze_stack

vec<Lit> Minisat::Internal::Solver::analyze_stack
protected

Definition at line 215 of file Solver.h.

◆ analyze_toclear

vec<Lit> Minisat::Internal::Solver::analyze_toclear
protected

Definition at line 216 of file Solver.h.

◆ assigns

vec<lbool> Minisat::Internal::Solver::assigns
protected

Definition at line 195 of file Solver.h.

◆ assumptions

vec<Lit> Minisat::Internal::Solver::assumptions
protected

Definition at line 204 of file Solver.h.

◆ asynch_interrupt

bool Minisat::Internal::Solver::asynch_interrupt
protected

Definition at line 227 of file Solver.h.

◆ ca

ClauseAllocator Minisat::Internal::Solver::ca
protected

Definition at line 209 of file Solver.h.

◆ ccmin_mode

int Minisat::Internal::Solver::ccmin_mode

Definition at line 138 of file Solver.h.

◆ cla_inc

double Minisat::Internal::Solver::cla_inc
protected

Definition at line 190 of file Solver.h.

◆ clause_decay

double Minisat::Internal::Solver::clause_decay

Definition at line 134 of file Solver.h.

◆ clauses

vec<CRef> Minisat::Internal::Solver::clauses
protected

Definition at line 188 of file Solver.h.

◆ clauses_literals

uint64_t Minisat::Internal::Solver::clauses_literals

Definition at line 155 of file Solver.h.

◆ conflict

vec<Lit> Minisat::Internal::Solver::conflict

Definition at line 127 of file Solver.h.

◆ conflict_budget

int64_t Minisat::Internal::Solver::conflict_budget
protected

Definition at line 225 of file Solver.h.

◆ conflicts

uint64_t Minisat::Internal::Solver::conflicts

Definition at line 154 of file Solver.h.

◆ dec_vars

uint64_t Minisat::Internal::Solver::dec_vars

Definition at line 155 of file Solver.h.

◆ decision

vec<char> Minisat::Internal::Solver::decision
protected

Definition at line 197 of file Solver.h.

◆ decisions

uint64_t Minisat::Internal::Solver::decisions

Definition at line 154 of file Solver.h.

◆ garbage_frac

double Minisat::Internal::Solver::garbage_frac

Definition at line 142 of file Solver.h.

◆ learnts

vec<CRef> Minisat::Internal::Solver::learnts
protected

Definition at line 189 of file Solver.h.

◆ learnts_literals

uint64_t Minisat::Internal::Solver::learnts_literals

Definition at line 155 of file Solver.h.

◆ learntsize_adjust_cnt

int Minisat::Internal::Solver::learntsize_adjust_cnt
protected

Definition at line 221 of file Solver.h.

◆ learntsize_adjust_confl

double Minisat::Internal::Solver::learntsize_adjust_confl
protected

Definition at line 220 of file Solver.h.

◆ learntsize_adjust_inc

double Minisat::Internal::Solver::learntsize_adjust_inc

Definition at line 150 of file Solver.h.

◆ learntsize_adjust_start_confl

int Minisat::Internal::Solver::learntsize_adjust_start_confl

Definition at line 149 of file Solver.h.

◆ learntsize_factor

double Minisat::Internal::Solver::learntsize_factor

Definition at line 146 of file Solver.h.

◆ learntsize_inc

double Minisat::Internal::Solver::learntsize_inc

Definition at line 147 of file Solver.h.

◆ luby_restart

bool Minisat::Internal::Solver::luby_restart

Definition at line 137 of file Solver.h.

◆ max_learnts

double Minisat::Internal::Solver::max_learnts
protected

Definition at line 219 of file Solver.h.

◆ max_literals

uint64_t Minisat::Internal::Solver::max_literals

Definition at line 155 of file Solver.h.

◆ model

vec<lbool> Minisat::Internal::Solver::model

Definition at line 126 of file Solver.h.

◆ ok

bool Minisat::Internal::Solver::ok
protected

Definition at line 187 of file Solver.h.

◆ order_heap

Heap<VarOrderLt> Minisat::Internal::Solver::order_heap
protected

Definition at line 205 of file Solver.h.

◆ phase_saving

int Minisat::Internal::Solver::phase_saving

Definition at line 139 of file Solver.h.

◆ polarity

vec<char> Minisat::Internal::Solver::polarity
protected

Definition at line 196 of file Solver.h.

◆ progress_estimate

double Minisat::Internal::Solver::progress_estimate
protected

Definition at line 206 of file Solver.h.

◆ propagation_budget

int64_t Minisat::Internal::Solver::propagation_budget
protected

Definition at line 226 of file Solver.h.

◆ propagations

uint64_t Minisat::Internal::Solver::propagations

Definition at line 154 of file Solver.h.

◆ qhead

int Minisat::Internal::Solver::qhead
protected

Definition at line 201 of file Solver.h.

◆ random_seed

double Minisat::Internal::Solver::random_seed

Definition at line 136 of file Solver.h.

◆ random_var_freq

double Minisat::Internal::Solver::random_var_freq

Definition at line 135 of file Solver.h.

◆ remove_satisfied

bool Minisat::Internal::Solver::remove_satisfied
protected

Definition at line 207 of file Solver.h.

◆ restart_first

int Minisat::Internal::Solver::restart_first

Definition at line 144 of file Solver.h.

◆ restart_inc

double Minisat::Internal::Solver::restart_inc

Definition at line 145 of file Solver.h.

◆ rnd_decisions

uint64_t Minisat::Internal::Solver::rnd_decisions

Definition at line 154 of file Solver.h.

◆ rnd_init_act

bool Minisat::Internal::Solver::rnd_init_act

Definition at line 141 of file Solver.h.

◆ rnd_pol

bool Minisat::Internal::Solver::rnd_pol

Definition at line 140 of file Solver.h.

◆ seen

vec<char> Minisat::Internal::Solver::seen
protected

Definition at line 214 of file Solver.h.

◆ simpDB_assigns

int Minisat::Internal::Solver::simpDB_assigns
protected

Definition at line 202 of file Solver.h.

◆ simpDB_props

int64_t Minisat::Internal::Solver::simpDB_props
protected

Definition at line 203 of file Solver.h.

◆ solves

uint64_t Minisat::Internal::Solver::solves

Definition at line 154 of file Solver.h.

◆ starts

uint64_t Minisat::Internal::Solver::starts

Definition at line 154 of file Solver.h.

◆ tot_literals

uint64_t Minisat::Internal::Solver::tot_literals

Definition at line 155 of file Solver.h.

◆ trail

vec<Lit> Minisat::Internal::Solver::trail
protected

Definition at line 198 of file Solver.h.

◆ trail_lim

vec<int> Minisat::Internal::Solver::trail_lim
protected

Definition at line 199 of file Solver.h.

◆ var_decay

double Minisat::Internal::Solver::var_decay

Definition at line 133 of file Solver.h.

◆ var_inc

double Minisat::Internal::Solver::var_inc
protected

Definition at line 192 of file Solver.h.

◆ vardata

vec<VarData> Minisat::Internal::Solver::vardata
protected

Definition at line 200 of file Solver.h.

◆ verbosity

int Minisat::Internal::Solver::verbosity

Definition at line 132 of file Solver.h.

◆ watches

OccLists<Lit, vec<Watcher>, WatcherDeleted> Minisat::Internal::Solver::watches
protected

Definition at line 194 of file Solver.h.

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