Interface for supporting enumeration of models. More...

#include <enumerator.h>

Inheritance diagram for Clasp::Enumerator:

Public Types
typedef EnumerationConstraint *	ConPtr
typedef const EnumerationConstraint *	ConPtrConst
typedef const SharedMinimizeData *	Minimizer
typedef EnumOptions::OptMode	OptMode
Public Member Functions
uint8	commit (Solver &s)
	Commits the state stored in the given solver.
bool	commitComplete ()
	Marks current enumeration phase as completed.
bool	commitModel (Solver &s)
	Commits the model stored in the given solver.
bool	commitSymmetric (Solver &s)
	Expands the next symmetric model if any.
bool	commitUnsat (Solver &s)
	Commits an unsatisfiable path stored in the given solver.
void	end (Solver &s) const
	Removes from s the path that was passed to start() and any active (minimization) bound.
uint64	enumerated () const
	Returns the number of models enumerated so far.
	Enumerator ()
virtual bool	exhaustive () const
	Returns whether this enumerator requires exhaustive search to produce a definite answer.
int	init (SharedContext &problem, SharedMinimizeData *min=0, int limit=0)
	Prepares the problem for enumeration.
const Model &	lastModel () const
	Returns the last model enumerated.
Minimizer	minimizer () const
virtual int	modelType () const
	Returns the type of models this enumerator computes.
bool	optimize () const
	Returns whether optimization is active.
void	reset ()
void	setDisjoint (Solver &s, bool b) const
	Sets whether the search path stored in s is disjoint from all others.
void	setIgnoreSymmetric (bool b)
	Sets whether symmetric should be ignored.
bool	start (Solver &s, const LitVec &path=LitVec(), bool disjointPath=false) const
	Prepares the given solver for enumeration under the given path.
virtual bool	supportsParallel () const
	Returns whether or not this enumerator supports parallel search.
virtual bool	supportsRestarts () const
	Returns whether or not this enumerator supports full restarts once a model was found.
bool	tentative () const
	Returns whether computed models are still tentative.
bool	update (Solver &s) const
	Updates the given solver with enumeration-related information.
virtual	~Enumerator ()
Protected Member Functions
ConPtr	constraint (const Solver &s) const
virtual ConPtr	doInit (SharedContext &ctx, MinimizeConstraint *m, int numModels)=0
	Shall prepare the enumerator and freeze any enumeration-related variable.
virtual void	doReset ()
Private Member Functions
	Enumerator (const Enumerator &)
Enumerator &	operator= (const Enumerator &)
Private Attributes
SharedMinimizeData *	mini_
Model	model_

Detailed Description

Interface for supporting enumeration of models.

Enumerators are global w.r.t a solve algorithm. That is, even if the solve algorithm itself uses a parallel search, there shall be only one enumerator and it is the user's responsibility to protect the enumerator with appropriate locking.

Concrete enumerators must implement a function for preparing a problem for enumeration and an EnumerationConstraint to be added to each solver attached to the problem. It is then the job of the actual solve algorithm to commit models to the enumerator and to integrate new information into attached solvers via appropriate calls to Enumerator::update().

Definition at line 94 of file enumerator.h.

Member Typedef Documentation

typedef EnumerationConstraint* Clasp::Enumerator::ConPtr

Definition at line 96 of file enumerator.h.

typedef const EnumerationConstraint* Clasp::Enumerator::ConPtrConst

Definition at line 97 of file enumerator.h.

typedef const SharedMinimizeData* Clasp::Enumerator::Minimizer

Definition at line 98 of file enumerator.h.

typedef EnumOptions::OptMode Clasp::Enumerator::OptMode

Definition at line 99 of file enumerator.h.

Constructor & Destructor Documentation

Clasp::Enumerator::Enumerator ( ) [explicit]

Definition at line 96 of file enumerator.cpp.

Clasp::Enumerator::~Enumerator ( ) [virtual]

Definition at line 97 of file enumerator.cpp.

Clasp::Enumerator::Enumerator ( const Enumerator & ) [private]

Member Function Documentation

ValueRep Clasp::Enumerator::commit ( Solver & s )

Commits the state stored in the given solver.

Calls commitModel() or commitUnsat() depending on the state of s. The function returns value_true, to signal that s stores a valid and unique model, value_false to signal that search shall be stopped, and value_free otherwise.

See also:: commitModel(); commitUnsat()

Definition at line 140 of file enumerator.cpp.

bool Clasp::Enumerator::commitComplete ( )

Marks current enumeration phase as completed.

If the enumerator was initialized with a minimization constraint and optimization mode MinimizeMode_t::enumOpt, the optimal bound is committed, the enumerator is prepared for enumerating optimal models, and the function returns false. Otherwise, the function returns true and search shall be stopped.

Definition at line 158 of file enumerator.cpp.

bool Clasp::Enumerator::commitModel ( Solver & s )

Commits the model stored in the given solver.

If the model is valid and unique, the function returns true and the model can be accessed via a call to Enumerator::lastModel(). Otherwise, the function returns false. In either case, Enumerator::update(s) shall be called in order to continue search for further models.

Precondition:: The solver's assignment is total.

Note:: The function is *not* concurrency-safe, i.e. in a parallel search at most one solver shall call the function at any one time.

Definition at line 145 of file enumerator.cpp.

bool Clasp::Enumerator::commitSymmetric ( Solver & s )

Expands the next symmetric model if any.

Definition at line 156 of file enumerator.cpp.

bool Clasp::Enumerator::commitUnsat ( Solver & s )

Commits an unsatisfiable path stored in the given solver.

The return value determines how search should proceed. If true is returned, the enumerator has relaxed an enumeration constraint and search may continue after a call to Enumerator::update(s). Otherwise, the search shall be stopped.

Note:: The function is *not* concurrency-safe, i.e. in a parallel search at most one solver shall call the function at any one time.

Definition at line 157 of file enumerator.cpp.

Enumerator::ConPtr Clasp::Enumerator::constraint ( const Solver & s ) const [protected]

Definition at line 134 of file enumerator.cpp.

virtual ConPtr Clasp::Enumerator::doInit	(	SharedContext &	ctx,
		MinimizeConstraint *	m,
		int	numModels
	)		`[protected, pure virtual]`

Shall prepare the enumerator and freeze any enumeration-related variable.

Returns:: A prototypical enumeration constraint to be used in the master solver.

Implemented in Clasp::ModelEnumerator, and Clasp::CBConsequences.

void Clasp::Enumerator::doReset ( ) [protected, virtual]

Definition at line 101 of file enumerator.cpp.

void Clasp::Enumerator::end ( Solver & s ) const

Removes from s the path that was passed to start() and any active (minimization) bound.

Definition at line 100 of file enumerator.cpp.

uint64 Clasp::Enumerator::enumerated ( ) const [inline]

Returns the number of models enumerated so far.

Definition at line 191 of file enumerator.h.

virtual bool Clasp::Enumerator::exhaustive ( ) const [inline, virtual]

Returns whether this enumerator requires exhaustive search to produce a definite answer.

Reimplemented in Clasp::CBConsequences.

Definition at line 208 of file enumerator.h.

int Clasp::Enumerator::init	(	SharedContext &	problem,
		SharedMinimizeData *	min = `0`,
		int	limit = `0`
	)

Prepares the problem for enumeration.

The function shall be called once before search is started and before SharedContext::endInit() was called. It freezes enumeration-related variables and adds a suitable enumeration constraint to the master solver.

Precondition:: The problem is not yet frozen, i.e. SharedContext::endInit() was not yet called.

Parameters:

problem	The problem on which this enumerator should work.
min	Optional minimization constraint to be applied during enumeration.
limit	Optional hint on max number of models to compute.

Note:: In the incremental setting, init() must be called once for each incremental step.; The enumerator takes ownership of the minimize constraint (if any). That is, it does not increase its reference count.

Definition at line 113 of file enumerator.cpp.

const Model& Clasp::Enumerator::lastModel ( ) const [inline]

Returns the last model enumerated.

Note:: If enumerated() is equal to 0, the returned object is in an indeterminate state.

Definition at line 196 of file enumerator.h.

Minimizer Clasp::Enumerator::minimizer ( ) const [inline]

Definition at line 213 of file enumerator.h.

virtual int Clasp::Enumerator::modelType ( ) const [inline, virtual]

Returns the type of models this enumerator computes.

Reimplemented in Clasp::CBConsequences.

Definition at line 202 of file enumerator.h.

Enumerator& Clasp::Enumerator::operator= ( const Enumerator & ) [private]

bool Clasp::Enumerator::optimize ( ) const [inline]

Returns whether optimization is active.

Definition at line 198 of file enumerator.h.

void Clasp::Enumerator::reset ( )

Definition at line 102 of file enumerator.cpp.

void Clasp::Enumerator::setDisjoint	(	Solver &	s,
		bool	b
	)		const

Sets whether the search path stored in s is disjoint from all others.

Definition at line 98 of file enumerator.cpp.

void Clasp::Enumerator::setIgnoreSymmetric ( bool b )

Sets whether symmetric should be ignored.

Definition at line 99 of file enumerator.cpp.

bool Clasp::Enumerator::start	(	Solver &	s,
		const LitVec &	path = `LitVec()`,
		bool	disjointPath = `false`
	)		const

Prepares the given solver for enumeration under the given path.

The function shall be called once before solving is started. It pushes the given path to the solver by calling Solver::pushRoot() and prepares s for enumeration/optimization.

Returns:: true if path was added.

Definition at line 137 of file enumerator.cpp.

virtual bool Clasp::Enumerator::supportsParallel ( ) const [inline, virtual]

Returns whether or not this enumerator supports parallel search.

Reimplemented in Clasp::ModelEnumerator.

Definition at line 206 of file enumerator.h.

virtual bool Clasp::Enumerator::supportsRestarts ( ) const [inline, virtual]

Returns whether or not this enumerator supports full restarts once a model was found.

Reimplemented in Clasp::ModelEnumerator.

Definition at line 204 of file enumerator.h.

bool Clasp::Enumerator::tentative ( ) const [inline]

Returns whether computed models are still tentative.

Definition at line 200 of file enumerator.h.

bool Clasp::Enumerator::update ( Solver & s ) const

Updates the given solver with enumeration-related information.

The function is used to integrate enumeration-related information, like minimization bounds or previously committed models, into the search space of s. It shall be called after each commit.

Parameters:

s	The solver to update.

Note:: The function is concurrency-safe, i.e. can be called concurrently by different solvers.

Definition at line 175 of file enumerator.cpp.

Member Data Documentation

SharedMinimizeData* Clasp::Enumerator::mini_ [private]

Definition at line 225 of file enumerator.h.

Model Clasp::Enumerator::model_ [private]

Definition at line 226 of file enumerator.h.

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

Public Types

Public Member Functions

Protected Member Functions

Private Member Functions

Private Attributes

Detailed Description

Member Typedef Documentation

Constructor & Destructor Documentation

Member Function Documentation

Member Data Documentation