Clasp::SharedContext Class Reference

Aggregates information to be shared between solver objects. More...

#include <shared_context.h>

List of all members.

Classes
struct	Share
struct	SharedSymTab
Public Types
typedef Configuration *	ConfigPtr
typedef SingleOwnerPtr < Distributor >	DistrPtr
typedef ShortImplicationsGraph	ImpGraph
typedef const ImpGraph &	ImpGraphRef
enum	InitMode { init_share_symbols, init_copy_symbols }
typedef EventHandler *	LogPtr
typedef SingleOwnerPtr < SatPreprocessor >	SatPrePtr
typedef SingleOwnerPtr< SDG >	SccGraph
typedef SharedDependencyGraph	SDG
typedef LitVec::size_type	size_type
typedef PodVector< Solver * >::type	SolverVec
typedef const ProblemStats &	StatsRef
typedef SymbolTable &	SymbolsRef
Public Member Functions
Problem introspection
Functions for querying information about the problem.
bool	ok () const
	Returns true unless the master has an unresolvable top-level conflict.
bool	frozen () const
	Returns whether the problem is currently frozen and therefore ready for being solved.
bool	isShared () const
	Returns whether more than one solver is actively working on the problem.
bool	isExtended () const
bool	hasSolver (uint32 id) const
	Returns whether this object has a solver associcated with the given id.
Solver *	master () const
	Returns the master solver associated with this object.
Solver *	solver (uint32 id) const
	Returns the solver with the given id.
uint32	numVars () const
	Returns the number of problem variables.
uint32	numEliminatedVars () const
	Returns the number of eliminated vars.
bool	validVar (Var var) const
	Returns true if var represents a valid variable in this problem.
VarInfo	varInfo (Var v) const
	Returns information about the given variable.
bool	eliminated (Var v) const
	Returns true if v is currently eliminated, i.e. no longer part of the problem.
bool	marked (Literal p) const
Literal	stepLiteral () const
uint32	numConstraints () const
	Returns the number of problem constraints.
uint32	numBinary () const
	Returns the number of binary constraints.
uint32	numTernary () const
	Returns the number of ternary constraints.
uint32	numUnary () const
	Returns the number of unary constraints.
uint32	problemComplexity () const
	Returns an estimate of the problem complexity based on the number and type of constraints.
StatsRef	stats () const
SymbolsRef	symbolTable () const
Problem setup
Functions for specifying the problem. Problem specification is a four-stage process: Add variables to the SharedContext object. Call startAddConstraints(). Add problem constraints to the master solver. Call endInit() to finish the initialization process. Note: After endInit() was called, other solvers can be attached to this object. In incremental setting, the process must be repeated for each incremental step. Problem specification is *not* thread-safe, i.e. during initialization no other thread shall access the context. !frozen() is a precondition for all functions in this group!
bool	unfreeze ()
	Unfreezes a frozen program and prepares it for updates.
void	cloneVars (const SharedContext &other, InitMode m=init_copy_symbols)
	Clones vars and symbol table from other.
void	resizeVars (uint32 maxVar)
	Sets the range of problem variables to [1, maxVar)
Var	addVar (VarType t, bool eq=false)
	Adds a new variable of type t.
void	requestStepVar ()
	Requests a special variable for tagging volatile knowledge in incremental setting.
void	requestData (Var v)
	Request additional reason data slot for variable v.
void	setFrozen (Var v, bool b)
	Freezes/defreezes a variable (a frozen var is exempt from Sat-preprocessing).
void	setNant (Var v, bool b)
	Marks/unmarks v as contained in a negative loop or head of a choice rule.
void	setInDisj (Var v, bool b)
	Marks/unmarks v as contained in a non-hcf disjunction.
void	setProject (Var v, bool b)
	Marks/unmarks v as projection variable.
void	setVarEq (Var v, bool b)
void	mark (Literal p)
void	unmark (Var v)
void	eliminate (Var v)
	Eliminates the variable v from the problem.
Solver &	startAddConstraints (uint32 constraintGuess=100)
	Prepares the master solver so that constraints can be added.
bool	addUnary (Literal x)
	A convenience method for adding facts to the master.
bool	addBinary (Literal x, Literal y)
	A convenience method for adding binary clauses.
bool	addTernary (Literal x, Literal y, Literal z)
	A convenience method for adding ternary clauses.
void	add (Constraint *c)
	A convenience method for adding constraints to the master.
bool	endInit (bool attachAll=false)
	Finishes initialization of the master solver.
Private Types
typedef SingleOwnerPtr < Configuration >	Config
typedef PodVector< SolverStats * > ::type	StatsVec
typedef PodVector< VarInfo >::type	VarVec
Private Member Functions
Literal	addAuxLit ()
void	init ()
SharedContext &	operator= (const SharedContext &)
	SharedContext (const SharedContext &)
bool	unfreezeStep ()
Private Attributes
StatsVec	accu_
ImpGraph	btig_
Config	config_
uint32	lastTopLevel_
ProblemStats	problem_
LogPtr	progress_
struct Clasp::SharedContext::Share	share_
SolverVec	solvers_
Literal	step_
struct Clasp::SharedContext::SharedSymTab *	symTabPtr_
VarVec	varInfo_
Configuration
SatPrePtr	satPrepro
SccGraph	sccGraph
	SharedContext ()
	Creates a new object for sharing variables and the binary and ternary implication graph.
	~SharedContext ()
void	reset ()
	Resets this object to the state after default construction.
void	setEventHandler (EventHandler *r)
	Enables event reporting via the given event handler.
void	setShareMode (ContextParams::ShareMode m)
	Sets how to handle physical sharing of constraints.
void	setShortMode (ContextParams::ShortMode m)
	Sets whether the short implication graph should be used for storing short learnt constraints.
void	setConcurrency (uint32 numSolver)
	Sets maximal number of solvers sharing this object.
Solver &	addSolver ()
	Adds an additional solver to this object and returns it.
void	enableStats (uint32 level)
	Configures the statistic object of attached solvers.
void	accuStats ()
void	setPreserveModels (bool b=true)
	If b is true, sets preprocessing mode to model-preserving operations only.
void	setConfiguration (Configuration *c, bool own)
	Sets the configuration for this object and its attached solvers.
ConfigPtr	configuration () const
	Returns the current configuration used in this object.
LogPtr	eventHandler () const
	Returns the active event handler or 0 if none was set.
bool	seedSolvers () const
	Returns whether this object seeds the RNG of new solvers.
uint32	concurrency () const
	Returns the number of solvers that can share this object.
bool	preserveModels () const
bool	physicalShare (ConstraintType t) const
	Returns whether physical sharing is enabled for constraints of type t.
bool	physicalShareProblem () const
	Returns whether pyhiscal sharing of problem constraints is enabled.
bool	allowImplicit (ConstraintType t) const
	Returns whether short constraints of type t can be stored in the short implication graph.
(Parallel) solving
Functions to be called during (parallel) solving. Note: If not otherwise noted, the functions in this group can be safely called from multiple threads.
DistrPtr	distributor
bool	attach (uint32 id)
	Attaches the solver with the given id to this object.
bool	attach (Solver &s)
void	detach (uint32 id, bool reset=false)
	Detaches the solver with the given id from this object.
void	detach (Solver &s, bool reset=false)
uint32	winner () const
void	setWinner (uint32 sId)
void	simplify (bool shuffle)
	Simplifies the problem constraints w.r.t the master's assignment.
void	removeConstraint (uint32 idx, bool detach)
	Removes the constraint with the given idx from the master's db.
int	addImp (ImpGraph::ImpType t, const Literal *lits, ConstraintType ct)
	Adds the given short implication to the short implication graph if possible.
uint32	numLearntShort () const
	Returns the number of learnt short implications.
ImpGraphRef	shortImplications () const
void	simplifyShort (const Solver &s, Literal p)
void	report (const Event &ev) const
bool	report (const Solver &s, const Model &m) const
void	initStats (Solver &s) const
const SolverStats &	stats (const Solver &s, bool accu) const

---

Detailed Description

Aggregates information to be shared between solver objects.

Among other things, SharedContext objects store static information on variables, the (possibly unused) symbol table, as well as the binary and ternary implication graph of the input problem.

Furthermore, a SharedContext object always stores a distinguished master solver that is used to store and simplify problem constraints. Additional solvers can be added via SharedContext::addSolver(). Once initialization is completed, any additional solvers must be attached to this object by calling SharedContext::attach().

Definition at line 396 of file shared_context.h.

---

Member Typedef Documentation

typedef SingleOwnerPtr<Configuration> Clasp::SharedContext::Config [private]

Definition at line 680 of file shared_context.h.

typedef Configuration* Clasp::SharedContext::ConfigPtr

Definition at line 401 of file shared_context.h.

typedef SingleOwnerPtr<Distributor> Clasp::SharedContext::DistrPtr

Definition at line 402 of file shared_context.h.

typedef ShortImplicationsGraph Clasp::SharedContext::ImpGraph

Definition at line 406 of file shared_context.h.

typedef const ImpGraph& Clasp::SharedContext::ImpGraphRef

Definition at line 407 of file shared_context.h.

typedef EventHandler* Clasp::SharedContext::LogPtr

Definition at line 408 of file shared_context.h.

typedef SingleOwnerPtr<SatPreprocessor> Clasp::SharedContext::SatPrePtr

Definition at line 409 of file shared_context.h.

typedef SingleOwnerPtr<SDG> Clasp::SharedContext::SccGraph

Definition at line 400 of file shared_context.h.

typedef SharedDependencyGraph Clasp::SharedContext::SDG

Definition at line 398 of file shared_context.h.

typedef LitVec::size_type Clasp::SharedContext::size_type

Definition at line 405 of file shared_context.h.

typedef PodVector<Solver*>::type Clasp::SharedContext::SolverVec

Definition at line 399 of file shared_context.h.

typedef const ProblemStats& Clasp::SharedContext::StatsRef

Definition at line 403 of file shared_context.h.

typedef PodVector<SolverStats*>::type Clasp::SharedContext::StatsVec [private]

Definition at line 682 of file shared_context.h.

typedef SymbolTable& Clasp::SharedContext::SymbolsRef

Definition at line 404 of file shared_context.h.

typedef PodVector<VarInfo>::type Clasp::SharedContext::VarVec [private]

Definition at line 681 of file shared_context.h.

---

Member Enumeration Documentation

enum Clasp::SharedContext::InitMode

Enumerator:

init_share_symbols
init_copy_symbols

Definition at line 410 of file shared_context.h.

---

Constructor & Destructor Documentation

Clasp::SharedContext::SharedContext

(

)

[explicit]

Creates a new object for sharing variables and the binary and ternary implication graph.

Definition at line 484 of file shared_context.cpp.

Clasp::SharedContext::~SharedContext

(

)

Definition at line 519 of file shared_context.cpp.

Clasp::SharedContext::SharedContext

(

const SharedContext &

)

[private]

---

Member Function Documentation

void Clasp::SharedContext::accuStats

(

)

Definition at line 764 of file shared_context.cpp.

void Clasp::SharedContext::add

(

Constraint *

c

)

A convenience method for adding constraints to the master.

Definition at line 681 of file shared_context.cpp.

Literal Clasp::SharedContext::addAuxLit

(

)

[private]

Definition at line 655 of file shared_context.cpp.

bool Clasp::SharedContext::addBinary	(	Literal	x,
		Literal	y
	)

A convenience method for adding binary clauses.

Definition at line 671 of file shared_context.cpp.

int Clasp::SharedContext::addImp	(	ImpGraph::ImpType	t,
		const Literal *	lits,
		ConstraintType	ct
	)

Adds the given short implication to the short implication graph if possible.

Returns:

• > 0 if implication was added.
• < 0 if implication can't be added because allowImplicit() is false for ct.
• = 0 if implication is subsumed by some constraint in the short implication graph.

Definition at line 685 of file shared_context.cpp.

Solver & Clasp::SharedContext::addSolver

(

)

Adds an additional solver to this object and returns it.

Definition at line 551 of file shared_context.cpp.

bool Clasp::SharedContext::addTernary	(	Literal	x,
		Literal	y,
		Literal	z
	)

A convenience method for adding ternary clauses.

Definition at line 676 of file shared_context.cpp.

bool Clasp::SharedContext::addUnary

(

Literal

x

)

A convenience method for adding facts to the master.

Definition at line 667 of file shared_context.cpp.

Var Clasp::SharedContext::addVar	(	VarType	t,
		bool	eq = false
	)

Adds a new variable of type t.

Parameters:

t	Type of the new variable (either Var_t::atom_var or Var_t::body_var).
eq	True if var represents both an atom and a body. In that case t is the variable's primary type and determines the preferred literal.

Returns:

The index of the new variable.

Note:

Problem variables are numbered from 1 onwards!

Definition at line 622 of file shared_context.cpp.

bool Clasp::SharedContext::allowImplicit

(

ConstraintType

t

)

const [inline]

Returns whether short constraints of type t can be stored in the short implication graph.

Definition at line 465 of file shared_context.h.

bool Clasp::SharedContext::attach

(

uint32

id

)

[inline]

Attaches the solver with the given id to this object.

Note:

It is safe to attach multiple solvers concurrently but the master solver shall not change during the whole operation.

Precondition:

hasSolver(id)

Definition at line 632 of file shared_context.h.

bool Clasp::SharedContext::attach

(

Solver &

s

)

Definition at line 720 of file shared_context.cpp.

void Clasp::SharedContext::cloneVars	(	const SharedContext &	other,
		InitMode	m = init_copy_symbols
	)

Clones vars and symbol table from other.

Definition at line 504 of file shared_context.cpp.

uint32 Clasp::SharedContext::concurrency

(

)

const [inline]

Returns the number of solvers that can share this object.

Definition at line 458 of file shared_context.h.

ConfigPtr Clasp::SharedContext::configuration

(

)

const [inline]

Returns the current configuration used in this object.

Definition at line 452 of file shared_context.h.

void Clasp::SharedContext::detach	(	uint32	id,
		bool	reset = false
	)		[inline]

Detaches the solver with the given id from this object.

The function removes any tentative constraints from s. Shall be called once after search has stopped.

Note:

The function is concurrency-safe w.r.t to different solver objects, i.e. in a parallel search different solvers may call detach() concurrently.

Definition at line 644 of file shared_context.h.

void Clasp::SharedContext::detach	(	Solver &	s,
		bool	reset = false
	)

Definition at line 751 of file shared_context.cpp.

void Clasp::SharedContext::eliminate

(

Var

v

)

Eliminates the variable v from the problem.

Precondition:

v must not occur in any constraint and frozen(v) == false and value(v) == value_free

Definition at line 646 of file shared_context.cpp.

bool Clasp::SharedContext::eliminated

(

Var

v

)

const

Returns true if v is currently eliminated, i.e. no longer part of the problem.

Definition at line 641 of file shared_context.cpp.

void Clasp::SharedContext::enableStats

(

uint32

level

)

Configures the statistic object of attached solvers.

The level determines the amount of extra statistics. Currently two levels are supported:

• Level 1 enables ExtendedStats
• Level 2 enables ExtendedStats and JumpStats

  See also:

  ExtendedStats

  JumpStats

Definition at line 500 of file shared_context.cpp.

bool Clasp::SharedContext::endInit

(

bool

attachAll = false

)

Finishes initialization of the master solver.

The function must be called once before search is started. After endInit() was called, previously added solvers can be attached to the shared context and learnt constraints may be added to solver.

Parameters:

attachAll

If true, also calls attach() for all solvers that were added to this object.

Returns:

If the constraints are initially conflicting, false. Otherwise, true.

Note:

The master solver can't recover from top-level conflicts, i.e. if endInit() returned false, the solver is in an unusable state.

Postcondition:

frozen()

Definition at line 697 of file shared_context.cpp.

LogPtr Clasp::SharedContext::eventHandler

(

)

const [inline]

Returns the active event handler or 0 if none was set.

Definition at line 454 of file shared_context.h.

bool Clasp::SharedContext::frozen

(

)

const [inline]

Returns whether the problem is currently frozen and therefore ready for being solved.

Definition at line 476 of file shared_context.h.

bool Clasp::SharedContext::hasSolver

(

uint32

id

)

const [inline]

Returns whether this object has a solver associcated with the given id.

Definition at line 481 of file shared_context.h.

void Clasp::SharedContext::init

(

)

[private]

Definition at line 490 of file shared_context.cpp.

void Clasp::SharedContext::initStats

(

Solver &

s

)

const

Definition at line 757 of file shared_context.cpp.

bool Clasp::SharedContext::isExtended

(

)

const [inline]

Definition at line 479 of file shared_context.h.

bool Clasp::SharedContext::isShared

(

)

const [inline]

Returns whether more than one solver is actively working on the problem.

Definition at line 478 of file shared_context.h.

void Clasp::SharedContext::mark

(

Literal

p

)

[inline]

Definition at line 577 of file shared_context.h.

bool Clasp::SharedContext::marked

(

Literal

p

)

const [inline]

Definition at line 509 of file shared_context.h.

Solver* Clasp::SharedContext::master

(

)

const [inline]

Returns the master solver associated with this object.

Definition at line 483 of file shared_context.h.

uint32 Clasp::SharedContext::numBinary

(

)

const [inline]

Returns the number of binary constraints.

Definition at line 514 of file shared_context.h.

uint32 Clasp::SharedContext::numConstraints

(

)

const

Returns the number of problem constraints.

Definition at line 695 of file shared_context.cpp.

uint32 Clasp::SharedContext::numEliminatedVars

(

)

const [inline]

Returns the number of eliminated vars.

Definition at line 498 of file shared_context.h.

uint32 Clasp::SharedContext::numLearntShort

(

)

const [inline]

Returns the number of learnt short implications.

Definition at line 666 of file shared_context.h.

uint32 Clasp::SharedContext::numTernary

(

)

const [inline]

Returns the number of ternary constraints.

Definition at line 516 of file shared_context.h.

uint32 Clasp::SharedContext::numUnary

(

)

const [inline]

Returns the number of unary constraints.

Definition at line 518 of file shared_context.h.

uint32 Clasp::SharedContext::numVars

(

)

const [inline]

Returns the number of problem variables.

Note:

The special sentinel-var 0 is not counted, i.e. numVars() returns the number of problem-variables. To iterate over all problem variables use a loop like:

 for (Var i = 1; i <= numVars(); ++i) {...}

Definition at line 496 of file shared_context.h.

bool Clasp::SharedContext::ok

(

)

const

Returns true unless the master has an unresolvable top-level conflict.

Definition at line 499 of file shared_context.cpp.

SharedContext& Clasp::SharedContext::operator=

(

const SharedContext &

)

[private]

bool Clasp::SharedContext::physicalShare

(

ConstraintType

t

)

const [inline]

Returns whether physical sharing is enabled for constraints of type t.

Definition at line 461 of file shared_context.h.

bool Clasp::SharedContext::physicalShareProblem

(

)

const [inline]

Returns whether pyhiscal sharing of problem constraints is enabled.

Definition at line 463 of file shared_context.h.

bool Clasp::SharedContext::preserveModels

(

)

const [inline]

Definition at line 459 of file shared_context.h.

uint32 Clasp::SharedContext::problemComplexity

(

)

const

Returns an estimate of the problem complexity based on the number and type of constraints.

Definition at line 814 of file shared_context.cpp.

void Clasp::SharedContext::removeConstraint	(	uint32	idx,
		bool	detach
	)

Removes the constraint with the given idx from the master's db.

Definition at line 797 of file shared_context.cpp.

void Clasp::SharedContext::report

(

const Event &

ev

)

const [inline]

Definition at line 669 of file shared_context.h.

bool Clasp::SharedContext::report	(	const Solver &	s,
		const Model &	m
	)		const [inline]

Definition at line 670 of file shared_context.h.

void Clasp::SharedContext::requestData

(

Var

v

)

Request additional reason data slot for variable v.

Definition at line 632 of file shared_context.cpp.

void Clasp::SharedContext::requestStepVar

(

)

Requests a special variable for tagging volatile knowledge in incremental setting.

Definition at line 631 of file shared_context.cpp.

void Clasp::SharedContext::reset

(

)

Resets this object to the state after default construction.

Definition at line 525 of file shared_context.cpp.

void Clasp::SharedContext::resizeVars

(

uint32

maxVar

)

[inline]

Sets the range of problem variables to [1, maxVar)

Definition at line 554 of file shared_context.h.

bool Clasp::SharedContext::seedSolvers

(

)

const [inline]

Returns whether this object seeds the RNG of new solvers.

Definition at line 456 of file shared_context.h.

void Clasp::SharedContext::setConcurrency

(

uint32

numSolver

)

Sets maximal number of solvers sharing this object.

Definition at line 530 of file shared_context.cpp.

void Clasp::SharedContext::setConfiguration	(	Configuration *	c,
		bool	own
	)

Sets the configuration for this object and its attached solvers.

Note:

If own is true, ownership of c is transferred.

Definition at line 559 of file shared_context.cpp.

void Clasp::SharedContext::setEventHandler

(

EventHandler *

r

)

[inline]

Enables event reporting via the given event handler.

Definition at line 421 of file shared_context.h.

void Clasp::SharedContext::setFrozen	(	Var	v,
		bool	b
	)

Freezes/defreezes a variable (a frozen var is exempt from Sat-preprocessing).

Definition at line 634 of file shared_context.cpp.

void Clasp::SharedContext::setInDisj	(	Var	v,
		bool	b
	)		[inline]

Marks/unmarks v as contained in a non-hcf disjunction.

Definition at line 573 of file shared_context.h.

void Clasp::SharedContext::setNant	(	Var	v,
		bool	b
	)		[inline]

Marks/unmarks v as contained in a negative loop or head of a choice rule.

Definition at line 571 of file shared_context.h.

void Clasp::SharedContext::setPreserveModels

(

bool

b = true

)

[inline]

If b is true, sets preprocessing mode to model-preserving operations only.

Definition at line 442 of file shared_context.h.

void Clasp::SharedContext::setProject	(	Var	v,
		bool	b
	)		[inline]

Marks/unmarks v as projection variable.

Definition at line 575 of file shared_context.h.

void Clasp::SharedContext::setShareMode

(

ContextParams::ShareMode

m

)

Sets how to handle physical sharing of constraints.

Definition at line 542 of file shared_context.cpp.

void Clasp::SharedContext::setShortMode

(

ContextParams::ShortMode

m

)

Sets whether the short implication graph should be used for storing short learnt constraints.

Definition at line 547 of file shared_context.cpp.

void Clasp::SharedContext::setVarEq	(	Var	v,
		bool	b
	)		[inline]

Definition at line 576 of file shared_context.h.

void Clasp::SharedContext::setWinner

(

uint32

sId

)

[inline]

Definition at line 650 of file shared_context.h.

ImpGraphRef Clasp::SharedContext::shortImplications

(

)

const [inline]

Definition at line 667 of file shared_context.h.

void Clasp::SharedContext::simplify

(

bool

shuffle

)

Simplifies the problem constraints w.r.t the master's assignment.

Definition at line 774 of file shared_context.cpp.

void Clasp::SharedContext::simplifyShort	(	const Solver &	s,
		Literal	p
	)

Definition at line 810 of file shared_context.cpp.

Solver* Clasp::SharedContext::solver

(

uint32

id

)

const [inline]

Returns the solver with the given id.

Definition at line 485 of file shared_context.h.

Solver & Clasp::SharedContext::startAddConstraints

(

uint32

constraintGuess = 100

)

Prepares the master solver so that constraints can be added.

Must be called to publish previously added variables to master solver and before constraints over these variables can be added.

Returns:

The master solver associated with this object.

Definition at line 660 of file shared_context.cpp.

StatsRef Clasp::SharedContext::stats

(

)

const [inline]

Definition at line 521 of file shared_context.h.

const SolverStats & Clasp::SharedContext::stats	(	const Solver &	s,
		bool	accu
	)		const

Definition at line 761 of file shared_context.cpp.

Literal Clasp::SharedContext::stepLiteral

(

)

const [inline]

Definition at line 510 of file shared_context.h.

SymbolsRef Clasp::SharedContext::symbolTable

(

)

const [inline]

Definition at line 522 of file shared_context.h.

bool Clasp::SharedContext::unfreeze

(

)

Unfreezes a frozen program and prepares it for updates.

The function also triggers forgetting of volatile knowledge and removes any auxiliary variables.

See also:

requestStepVar()

Solver::popAuxVar()

Definition at line 585 of file shared_context.cpp.

bool Clasp::SharedContext::unfreezeStep

(

)

[private]

Definition at line 597 of file shared_context.cpp.

void Clasp::SharedContext::unmark

(

Var

v

)

[inline]

Definition at line 578 of file shared_context.h.

bool Clasp::SharedContext::validVar

(

Var

var

)

const [inline]

Returns true if var represents a valid variable in this problem.

Note:

The range of valid variables is [1..numVars()]. The variable 0 is a special sentinel variable.

Definition at line 504 of file shared_context.h.

VarInfo Clasp::SharedContext::varInfo

(

Var

v

)

const [inline]

Returns information about the given variable.

Definition at line 506 of file shared_context.h.

uint32 Clasp::SharedContext::winner

(

)

const [inline]

Definition at line 649 of file shared_context.h.

---

Member Data Documentation

StatsVec Clasp::SharedContext::accu_ [private]

Definition at line 706 of file shared_context.h.

ImpGraph Clasp::SharedContext::btig_ [private]

Definition at line 690 of file shared_context.h.

Config Clasp::SharedContext::config_ [private]

Definition at line 691 of file shared_context.h.

DistrPtr Clasp::SharedContext::distributor

Distributor object to use for distribution of learnt constraints.

Definition at line 647 of file shared_context.h.

uint32 Clasp::SharedContext::lastTopLevel_ [private]

Definition at line 695 of file shared_context.h.

ProblemStats Clasp::SharedContext::problem_ [private]

Definition at line 688 of file shared_context.h.

LogPtr Clasp::SharedContext::progress_ [private]

Definition at line 693 of file shared_context.h.

SatPrePtr Clasp::SharedContext::satPrepro

Preprocessor for simplifying problem.

Definition at line 448 of file shared_context.h.

SccGraph Clasp::SharedContext::sccGraph

Program dependency graph - only used for ASP-problems.

Definition at line 449 of file shared_context.h.

struct Clasp::SharedContext::Share Clasp::SharedContext::share_ [private]

SolverVec Clasp::SharedContext::solvers_ [private]

Definition at line 692 of file shared_context.h.

Literal Clasp::SharedContext::step_ [private]

Definition at line 694 of file shared_context.h.

struct Clasp::SharedContext::SharedSymTab* Clasp::SharedContext::symTabPtr_ [private]

VarVec Clasp::SharedContext::varInfo_ [private]

Definition at line 689 of file shared_context.h.

---

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

• shared_context.h
• shared_context.cpp