A solver-local (i.e. thread-local) constraint to support enumeration. More...

#include <enumerator.h>

Inheritance diagram for Clasp::EnumerationConstraint:

Public Types
typedef EnumerationConstraint *	ConPtr
typedef MinimizeConstraint *	MinPtr
Public Member Functions
bool	commitModel (Enumerator &ctx, Solver &s)
bool	commitUnsat (Enumerator &ctx, Solver &s)
bool	disjointPath () const
	Returns true if search-path is disjoint from all others.
void	end (Solver &s)
bool	integrateBound (Solver &s) const
MinPtr	minimizer () const
bool	optimize () const
	Returns true if optimization is active.
void	setDisjoint (bool x)
void	setMinimizer (MinPtr min)
bool	start (Solver &s, const LitVec &path, bool disjoint)
ValueRep	state () const
bool	update (Solver &s)
Protected Member Functions
MinimizeConstraint *	cloneMinimizer (Solver &s) const
virtual void	destroy (Solver *s, bool detach)
	Default is to call delete this.
virtual void	doCommitModel (Enumerator &, Solver &)
virtual bool	doUpdate (Solver &s)=0
	EnumerationConstraint (Solver &s, MinimizeConstraint *min)
virtual PropResult	propagate (Solver &, Literal, uint32 &)
virtual void	reason (Solver &, Literal, LitVec &)
virtual bool	simplify (Solver &s, bool reinit)
virtual bool	valid (Solver &s)
	Shall return whether the constraint is valid (i.e. not conflicting) w.r.t the current assignment in s.
virtual	~EnumerationConstraint ()
Private Types
enum	{ clear_state_mask = ~uint32(value_true\|value_false) }
enum	Flag { flag_path_disjoint = 4u }
Private Attributes
uint32	flags_: 4
MinimizeConstraint *	mini_
LitVec	next_
uint32	root_: 28

Detailed Description

A solver-local (i.e. thread-local) constraint to support enumeration.

An enumeration constraint is used to extract/store enumeration-related information from models.

Definition at line 234 of file enumerator.h.

Member Typedef Documentation

typedef EnumerationConstraint* Clasp::EnumerationConstraint::ConPtr

Definition at line 236 of file enumerator.h.

typedef MinimizeConstraint* Clasp::EnumerationConstraint::MinPtr

Definition at line 237 of file enumerator.h.

Member Enumeration Documentation

anonymous enum [private]

Enumerator:

clear_state_mask

Definition at line 269 of file enumerator.h.

enum Clasp::EnumerationConstraint::Flag [private]

Enumerator:

flag_path_disjoint

Definition at line 268 of file enumerator.h.

Constructor & Destructor Documentation

Clasp::EnumerationConstraint::EnumerationConstraint	(	Solver &	s,
		MinimizeConstraint *	min
	)		`[protected]`

Definition at line 27 of file enumerator.cpp.

Clasp::EnumerationConstraint::~EnumerationConstraint ( ) [protected, virtual]

Definition at line 33 of file enumerator.cpp.

Member Function Documentation

MinimizeConstraint * Clasp::EnumerationConstraint::cloneMinimizer ( Solver & s ) const [protected]

Definition at line 30 of file enumerator.cpp.

bool Clasp::EnumerationConstraint::commitModel	(	Enumerator &	ctx,
		Solver &	s
	)

Definition at line 80 of file enumerator.cpp.

bool Clasp::EnumerationConstraint::commitUnsat	(	Enumerator &	ctx,
		Solver &	s
	)

Definition at line 88 of file enumerator.cpp.

void Clasp::EnumerationConstraint::destroy	(	Solver *	s,
		bool	detach
	)		`[protected, virtual]`

Default is to call delete this.

Reimplemented from Clasp::Constraint.

Reimplemented in Clasp::CBConsequences::CBFinder, and Clasp::ModelEnumerator::ModelFinder.

Definition at line 34 of file enumerator.cpp.

bool Clasp::EnumerationConstraint::disjointPath ( ) const [inline]

Returns true if search-path is disjoint from all others.

Definition at line 239 of file enumerator.h.

virtual void Clasp::EnumerationConstraint::doCommitModel	(	Enumerator &	,
		Solver &
	)		`[inline, protected, virtual]`

Reimplemented in Clasp::ModelEnumerator::BacktrackFinder, Clasp::ModelEnumerator::RecordFinder, and Clasp::CBConsequences::CBFinder.

Definition at line 265 of file enumerator.h.

virtual bool Clasp::EnumerationConstraint::doUpdate ( Solver & s ) [protected, pure virtual]

Implemented in Clasp::ModelEnumerator::BacktrackFinder, Clasp::ModelEnumerator::RecordFinder, and Clasp::CBConsequences::CBFinder.

void Clasp::EnumerationConstraint::end ( Solver & s )

Definition at line 43 of file enumerator.cpp.

bool Clasp::EnumerationConstraint::integrateBound ( Solver & s ) const

Definition at line 37 of file enumerator.cpp.

MinPtr Clasp::EnumerationConstraint::minimizer ( ) const [inline]

Definition at line 243 of file enumerator.h.

bool Clasp::EnumerationConstraint::optimize ( ) const

Returns true if optimization is active.

Definition at line 38 of file enumerator.cpp.

virtual PropResult Clasp::EnumerationConstraint::propagate	(	Solver &	s,
		Literal	p,
		uint32 &	data
	)		`[inline, protected, virtual]`

Propagate is called for each constraint that watches p. It shall enqueue all consequences of p becoming true.

Precondition:: p is true in s

Parameters:

s	The solver in which p became true.
p	A literal watched by this constraint that recently became true.
data	The data-blob that this constraint passed when the watch for p was registered.

Implements Clasp::Constraint.

Reimplemented in Clasp::ModelEnumerator::BacktrackFinder.

Definition at line 259 of file enumerator.h.