#include <ogdf/lib/minisat/simp/SimpSolver.h>

Inheritance diagram for Minisat::Internal::SimpSolver:

Classes
struct	ClauseDeleted

struct	ElimLt

Public Member Functions
	SimpSolver ()

	~SimpSolver ()

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

bool	eliminate (bool turn_off_elim=false)

virtual void	garbageCollect () override

bool	isEliminated (Var v) const

Var	newVar (bool polarity=true, bool dvar=true)

void	setFrozen (Var v, bool b)

bool	solve (bool do_simp=true, bool turn_off_simp=false)

bool	solve (const vec< Lit > &assumps, bool do_simp=true, bool turn_off_simp=false)

bool	solve (Lit p, bool do_simp=true, bool turn_off_simp=false)

bool	solve (Lit p, Lit q, bool do_simp=true, bool turn_off_simp=false)

bool	solve (Lit p, Lit q, Lit r, bool do_simp=true, bool turn_off_simp=false)

lbool	solveLimited (const vec< Lit > &assumps, bool do_simp=true, bool turn_off_simp=false)

bool	substitute (Var v, Lit x)

Public Member Functions inherited from Minisat::Internal::Solver
	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 ()

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	asymm_lits

int	clause_lim

int	eliminated_vars

int	grow

int	merges

double	simp_garbage_frac

int	subsumption_lim

bool	use_asymm

bool	use_elim

bool	use_rcheck

Public Attributes inherited from Minisat::Internal::Solver
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
bool	asymm (Var v, CRef cr)

bool	asymmVar (Var v)

bool	backwardSubsumptionCheck (bool verbose=false)

void	cleanUpClauses ()

bool	eliminateVar (Var v)

void	extendModel ()

void	gatherTouchedClauses ()

bool	implied (const vec< Lit > &c)

bool	merge (const Clause &_ps, const Clause &_qs, Var v, int &size)

bool	merge (const Clause &_ps, const Clause &_qs, Var v, vec< Lit > &out_clause)

void	relocAll (ClauseAllocator &to)

void	removeClause (CRef cr)

lbool	solve_ (bool do_simp=true, bool turn_off_simp=false)

bool	strengthenClause (CRef cr, Lit l)

void	updateElimHeap (Var v)

Protected Member Functions inherited from Minisat::Internal::Solver
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

Protected Attributes
int	bwdsub_assigns

CRef	bwdsub_tmpunit

Heap< ElimLt >	elim_heap

vec< uint32_t >	elimclauses

vec< char >	eliminated

int	elimorder

vec< char >	frozen

vec< int >	n_occ

int	n_touched

OccLists< Var, vec< CRef >, ClauseDeleted >	occurs

Queue< CRef >	subsumption_queue

vec< char >	touched

bool	use_simplification

Protected Attributes inherited from Minisat::Internal::Solver
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

Additional Inherited Members
Public Types inherited from Minisat::Internal::Solver
enum	AnswerType { A_TRUE , A_FALSE , A_UNDEF }

Static Protected Member Functions inherited from Minisat::Internal::Solver
static double	drand (double &seed)

static int	irand (double &seed, int size)

static VarData	mkVarData (CRef cr, int l)

Detailed Description

Definition at line 33 of file SimpSolver.h.

Constructor & Destructor Documentation

◆ SimpSolver()

Minisat::Internal::SimpSolver::SimpSolver ( )

◆ ~SimpSolver()

Minisat::Internal::SimpSolver::~SimpSolver ( )

Member Function Documentation

◆ addClause() [1/4]

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

inline

Definition at line 181 of file SimpSolver.h.

◆ addClause() [2/4]

bool Minisat::Internal::SimpSolver::addClause ( Lit p )

inline

Definition at line 183 of file SimpSolver.h.

◆ addClause() [3/4]

bool Minisat::Internal::SimpSolver::addClause	(	Lit	p,
		Lit	q
	)

inline

Definition at line 184 of file SimpSolver.h.

◆ addClause() [4/4]

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

inline

Definition at line 185 of file SimpSolver.h.

◆ addClause_()

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

◆ addEmptyClause()

bool Minisat::Internal::SimpSolver::addEmptyClause ( )

inline

Definition at line 182 of file SimpSolver.h.

◆ asymm()

bool Minisat::Internal::SimpSolver::asymm	(	Var	v,
		CRef	cr
	)

protected

◆ asymmVar()

bool Minisat::Internal::SimpSolver::asymmVar ( Var v )

protected

◆ backwardSubsumptionCheck()

bool Minisat::Internal::SimpSolver::backwardSubsumptionCheck ( bool verbose = false )

protected

◆ cleanUpClauses()

void Minisat::Internal::SimpSolver::cleanUpClauses ( )

protected

◆ eliminate()

bool Minisat::Internal::SimpSolver::eliminate ( bool turn_off_elim = false )

◆ eliminateVar()

bool Minisat::Internal::SimpSolver::eliminateVar ( Var v )

protected

◆ extendModel()

void Minisat::Internal::SimpSolver::extendModel ( )

protected

◆ garbageCollect()

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

overridevirtual

Reimplemented from Minisat::Internal::Solver.

◆ gatherTouchedClauses()

void Minisat::Internal::SimpSolver::gatherTouchedClauses ( )

protected

◆ implied()

bool Minisat::Internal::SimpSolver::implied ( const vec< Lit > & c )

protected

◆ isEliminated()

bool Minisat::Internal::SimpSolver::isEliminated ( Var v ) const

inline

Definition at line 171 of file SimpSolver.h.

◆ merge() [1/2]

bool Minisat::Internal::SimpSolver::merge	(	const Clause &	_ps,
		const Clause &	_qs,
		Var	v,
		int &	size
	)

protected

◆ merge() [2/2]

bool Minisat::Internal::SimpSolver::merge	(	const Clause &	_ps,
		const Clause &	_qs,
		Var	v,
		vec< Lit > &	out_clause
	)

protected

◆ newVar()

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

◆ relocAll()

void Minisat::Internal::SimpSolver::relocAll ( ClauseAllocator & to )

protected

◆ removeClause()

void Minisat::Internal::SimpSolver::removeClause ( CRef cr )

protected

◆ setFrozen()

void Minisat::Internal::SimpSolver::setFrozen	(	Var	v,
		bool	b
	)

inline

Definition at line 186 of file SimpSolver.h.

◆ solve() [1/5]

bool Minisat::Internal::SimpSolver::solve	(	bool	do_simp = `true`,
		bool	turn_off_simp = `false`
	)

inline

Definition at line 188 of file SimpSolver.h.

◆ solve() [2/5]

bool Minisat::Internal::SimpSolver::solve	(	const vec< Lit > &	assumps,
		bool	do_simp = `true`,
		bool	turn_off_simp = `false`
	)

inline

Definition at line 192 of file SimpSolver.h.

◆ solve() [3/5]

bool Minisat::Internal::SimpSolver::solve	(	Lit	p,
		bool	do_simp = `true`,
		bool	turn_off_simp = `false`
	)

inline

Definition at line 189 of file SimpSolver.h.

◆ solve() [4/5]

bool Minisat::Internal::SimpSolver::solve	(	Lit	p,
		Lit	q,
		bool	do_simp = `true`,
		bool	turn_off_simp = `false`
	)

inline

Definition at line 190 of file SimpSolver.h.

◆ solve() [5/5]

bool Minisat::Internal::SimpSolver::solve	(	Lit	p,
		Lit	q,
		Lit	r,
		bool	do_simp = `true`,
		bool	turn_off_simp = `false`
	)

inline

Definition at line 191 of file SimpSolver.h.

◆ solve_()

lbool Minisat::Internal::SimpSolver::solve_	(	bool	do_simp = `true`,
		bool	turn_off_simp = `false`
	)

protected

◆ solveLimited()

lbool Minisat::Internal::SimpSolver::solveLimited	(	const vec< Lit > &	assumps,
		bool	do_simp = `true`,
		bool	turn_off_simp = `false`
	)

inline

Definition at line 195 of file SimpSolver.h.

◆ strengthenClause()

bool Minisat::Internal::SimpSolver::strengthenClause	(	CRef	cr,
		Lit	l
	)

protected

◆ substitute()

bool Minisat::Internal::SimpSolver::substitute	(	Var	v,
		Lit	x
	)

◆ updateElimHeap()

void Minisat::Internal::SimpSolver::updateElimHeap ( Var v )

inlineprotected

Definition at line 172 of file SimpSolver.h.

Member Data Documentation

◆ asymm_lits

int Minisat::Internal::SimpSolver::asymm_lits

Definition at line 96 of file SimpSolver.h.

◆ bwdsub_assigns

int Minisat::Internal::SimpSolver::bwdsub_assigns

protected

Definition at line 139 of file SimpSolver.h.

◆ bwdsub_tmpunit

CRef Minisat::Internal::SimpSolver::bwdsub_tmpunit

protected

Definition at line 144 of file SimpSolver.h.

◆ clause_lim

int Minisat::Internal::SimpSolver::clause_lim

Definition at line 84 of file SimpSolver.h.

◆ elim_heap

Heap<ElimLt> Minisat::Internal::SimpSolver::elim_heap

protected

Definition at line 135 of file SimpSolver.h.

◆ elimclauses

vec<uint32_t> Minisat::Internal::SimpSolver::elimclauses

protected

Definition at line 130 of file SimpSolver.h.

◆ eliminated

vec<char> Minisat::Internal::SimpSolver::eliminated

protected

Definition at line 138 of file SimpSolver.h.

◆ eliminated_vars

int Minisat::Internal::SimpSolver::eliminated_vars

Definition at line 97 of file SimpSolver.h.

◆ elimorder

int Minisat::Internal::SimpSolver::elimorder

protected

Definition at line 128 of file SimpSolver.h.

◆ frozen

vec<char> Minisat::Internal::SimpSolver::frozen

protected

Definition at line 137 of file SimpSolver.h.

◆ grow

int Minisat::Internal::SimpSolver::grow

Definition at line 83 of file SimpSolver.h.

◆ merges

int Minisat::Internal::SimpSolver::merges

Definition at line 95 of file SimpSolver.h.

◆ n_occ

vec<int> Minisat::Internal::SimpSolver::n_occ

protected

Definition at line 134 of file SimpSolver.h.

◆ n_touched

int Minisat::Internal::SimpSolver::n_touched

protected

Definition at line 140 of file SimpSolver.h.

◆ occurs

OccLists<Var, vec<CRef>, ClauseDeleted> Minisat::Internal::SimpSolver::occurs

protected

Definition at line 133 of file SimpSolver.h.

◆ simp_garbage_frac

double Minisat::Internal::SimpSolver::simp_garbage_frac

Definition at line 87 of file SimpSolver.h.

◆ subsumption_lim

int Minisat::Internal::SimpSolver::subsumption_lim

Definition at line 86 of file SimpSolver.h.

◆ subsumption_queue

Queue<CRef> Minisat::Internal::SimpSolver::subsumption_queue

protected

Definition at line 136 of file SimpSolver.h.

◆ touched

vec<char> Minisat::Internal::SimpSolver::touched

protected

Definition at line 131 of file SimpSolver.h.

◆ use_asymm

bool Minisat::Internal::SimpSolver::use_asymm

Definition at line 89 of file SimpSolver.h.

◆ use_elim

bool Minisat::Internal::SimpSolver::use_elim

Definition at line 91 of file SimpSolver.h.

◆ use_rcheck

bool Minisat::Internal::SimpSolver::use_rcheck

Definition at line 90 of file SimpSolver.h.

◆ use_simplification

bool Minisat::Internal::SimpSolver::use_simplification

protected

Definition at line 129 of file SimpSolver.h.

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

include/ogdf/lib/minisat/simp/SimpSolver.h

OpenGraph DrawingFramework

Classes

Public Member Functions

Public Attributes

Protected Member Functions

Protected Attributes

Additional Inherited Members

Detailed Description

Constructor & Destructor Documentation

◆ SimpSolver()

◆ ~SimpSolver()

Member Function Documentation

◆ addClause() [1/4]

◆ addClause() [2/4]

◆ addClause() [3/4]

◆ addClause() [4/4]

◆ addClause_()

◆ addEmptyClause()

◆ asymm()

◆ asymmVar()

◆ backwardSubsumptionCheck()

◆ cleanUpClauses()

◆ eliminate()

◆ eliminateVar()

◆ extendModel()

◆ garbageCollect()

◆ gatherTouchedClauses()

◆ implied()

◆ isEliminated()

◆ merge() [1/2]

◆ merge() [2/2]

◆ newVar()

◆ relocAll()

◆ removeClause()

◆ setFrozen()

◆ solve() [1/5]

◆ solve() [2/5]

◆ solve() [3/5]

◆ solve() [4/5]

◆ solve() [5/5]

◆ solve_()

◆ solveLimited()

◆ strengthenClause()

◆ substitute()

◆ updateElimHeap()

Member Data Documentation

◆ asymm_lits

◆ bwdsub_assigns

◆ bwdsub_tmpunit

◆ clause_lim

◆ elim_heap

◆ elimclauses

◆ eliminated

◆ eliminated_vars

◆ elimorder

◆ frozen

◆ grow

◆ merges

◆ n_occ

◆ n_touched

◆ occurs

◆ simp_garbage_frac

◆ subsumption_lim

◆ subsumption_queue

◆ touched

◆ use_asymm

◆ use_elim

◆ use_rcheck

◆ use_simplification

Open
Graph Drawing
Framework