#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

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 ( void )

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:

include/ogdf/lib/minisat/core/Solver.h

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

OpenGraph DrawingFramework

Classes

Public Types

Public Member Functions

Public Attributes

Protected Member Functions

Static Protected Member Functions

Protected Attributes

Detailed Description

Member Enumeration Documentation

◆ AnswerType

Constructor & Destructor Documentation

◆ Solver()

◆ ~Solver()

Member Function Documentation

◆ abstractLevel()

◆ addClause() [1/4]

◆ addClause() [2/4]

◆ addClause() [3/4]

◆ addClause() [4/4]

◆ addClause_()

◆ addEmptyClause()

◆ analyze()

◆ analyzeFinal()

◆ attachClause()

◆ budgetOff()

◆ cancelUntil()

◆ checkGarbage() [1/2]

◆ checkGarbage() [2/2]

◆ claBumpActivity()

◆ claDecayActivity()

◆ clearInterrupt()

◆ decisionLevel()

◆ detachClause()

◆ drand()

◆ enqueue()

◆ garbageCollect()

◆ insertVarOrder()

◆ interrupt()

◆ irand()

◆ level()

◆ litRedundant()

◆ locked()

◆ mkVarData()

◆ modelValue() [1/2]

◆ modelValue() [2/2]

◆ nAssigns()

◆ nClauses()

◆ newDecisionLevel()

◆ newVar()

◆ nFreeVars()

◆ nLearnts()

◆ nVars()

◆ okay()

◆ pickBranchLit()

◆ progressEstimate()

◆ propagate()

◆ reason()

◆ rebuildOrderHeap()

◆ reduceDB()

◆ relocAll()

◆ removeClause()

◆ removeSatisfied()

◆ satisfied()

◆ search() [1/2]

◆ search() [2/2]

◆ setConfBudget()

◆ setDecisionVar()

◆ setPolarity()

◆ setPropBudget()

◆ simplify()

◆ solve() [1/6]

◆ solve() [2/6]

◆ solve() [3/6]

◆ solve() [4/6]

◆ solve() [5/6]

◆ solve() [6/6]

◆ solve_() [1/2]

◆ solve_() [2/2]

◆ solveLimited()

Open
Graph Drawing
Framework