Clasp's default unfounded set checker. More...

#include <unfounded_check.h>

Inheritance diagram for Clasp::DefaultUnfoundedCheck:

Classes
struct	AddReasonLit
struct	AddSource
struct	AtomData
struct	BodyData
struct	BodyPtr
struct	ExtData
struct	ExtWatch
struct	InitExtWatches
struct	MinimalityCheck
struct	RemoveSource
Public Types
typedef DependencyGraph::AtomNode	AtomNode
typedef DependencyGraph::BodyNode	BodyNode
typedef SharedDependencyGraph	DependencyGraph
typedef DependencyGraph::NodeId	NodeId
enum	ReasonStrategy { common_reason, distinct_reason, shared_reason, only_reason, no_reason }
	Defines the supported reasons for explaining assignments. More...
Public Member Functions
	DefaultUnfoundedCheck ()
DependencyGraph *	graph () const
bool	init (Solver &)
	Called during initialization of s.
bool	isModel (Solver &s)
	Is the current total assignment a model?
uint32	nodes () const
uint32	priority () const
	Shall return a value representing the priority of this propagator.
bool	propagateFixpoint (Solver &s, PostPropagator *ctx)
	Shall enqueue and propagate new assignments implied by this propagator.
ReasonStrategy	reasonStrategy () const
void	reset ()
	Aborts an active propagation operation.
bool	valid (Solver &s)
	Shall return whether the constraint is valid (i.e. not conflicting) w.r.t the current assignment in s.
	~DefaultUnfoundedCheck ()
Private Types
typedef PodVector< AtomData >::type	AtomVec
typedef PodVector< BodyData >::type	BodyVec
typedef PodVector< ExtData * > ::type	ExtVec
typedef PodQueue< NodeId >	IdQueue
typedef SingleOwnerPtr < MinimalityCheck >	MiniPtr
enum	UfsType { ufs_none, ufs_poly, ufs_non_poly }
enum	WatchType { watch_source_false = 0, watch_head_false = 1, watch_head_true = 2, watch_subgoal_false = 3 }
typedef PodVector< ExtWatch >::type	WatchVec
Private Member Functions
void	addDeltaReason (const BodyPtr &body, uint32 uScc)
void	addExtWatch (Literal p, const BodyPtr &n, uint32 data)
void	addIfReason (const BodyPtr &, uint32 uScc)
void	addReasonLit (Literal)
void	addUnsourced (const BodyPtr &)
void	addWatch (Literal, uint32 data, WatchType type)
bool	assertAtom (Literal a, UfsType t)
void	computeReason (UfsType t)
void	createLoopFormula ()
	DefaultUnfoundedCheck (const DefaultUnfoundedCheck &)
bool	falsifyUfs (UfsType t)
UfsType	findNonHcfUfs (Solver &s)
bool	findSource (NodeId atom)
UfsType	findUfs (Solver &s, bool checkNonHcf)
void	forwardSource (const BodyPtr &n)
void	forwardUnsource (const BodyPtr &n, bool add)
BodyPtr	getBody (NodeId bId) const
void	initBody (const BodyPtr &n)
void	initExtBody (const BodyPtr &n)
void	initSuccessors (const BodyPtr &n, weight_t lower)
bool	isValidSource (const BodyPtr &)
DefaultUnfoundedCheck &	operator= (const DefaultUnfoundedCheck &)
PropResult	propagate (Solver &, Literal, uint32 &data)
void	propagateSource ()
bool	pushTodo (NodeId at)
bool	pushUfs (NodeId at)
void	reason (Solver &s, Literal, LitVec &)
void	removeSource (NodeId bodyId)
void	resetTodo ()
void	resetUfs ()
void	setSource (NodeId atom, const BodyPtr &b)
void	updateAssignment (Solver &s)
void	updateSource (AtomData &atom, const BodyPtr &n)
Private Attributes
LitVec	activeClause_
AtomVec	atoms_
BodyVec	bodies_
ExtVec	extended_
DependencyGraph *	graph_
ClauseInfo	info_
VarVec	invalidQ_
LitVec	loopAtoms_
MiniPtr	mini_
VarVec	pickedExt_
LitVec *	reasons_
Solver *	solver_
VarVec	sourceQ_
ReasonStrategy	strategy_
IdQueue	todo_
IdQueue	ufs_
WatchVec	watches_

Detailed Description

Clasp's default unfounded set checker.

Searches for unfounded atoms by checking the positive dependency graph (PDG) Basic Idea:

For each (non-false) atom a, let source(a) be a body B in body(a) that provides an external support for a
- If no such B exists, a must be false
If source(a) becomes false and a is not false:
- Let Q = {};
- add a to Q
- For each B' s.th B' is not external to Q
  - add { a' | source(a') = B } to Q
Try to find new sources for all atoms a in Q

Definition at line 48 of file unfounded_check.h.

Member Typedef Documentation

typedef DependencyGraph::AtomNode Clasp::DefaultUnfoundedCheck::AtomNode

Definition at line 53 of file unfounded_check.h.

typedef PodVector<AtomData>::type Clasp::DefaultUnfoundedCheck::AtomVec [private]

Definition at line 256 of file unfounded_check.h.

typedef DependencyGraph::BodyNode Clasp::DefaultUnfoundedCheck::BodyNode

Definition at line 52 of file unfounded_check.h.

typedef PodVector<BodyData>::type Clasp::DefaultUnfoundedCheck::BodyVec [private]

Definition at line 257 of file unfounded_check.h.

typedef SharedDependencyGraph Clasp::DefaultUnfoundedCheck::DependencyGraph

Definition at line 50 of file unfounded_check.h.

typedef PodVector<ExtData*>::type Clasp::DefaultUnfoundedCheck::ExtVec [private]

Definition at line 258 of file unfounded_check.h.

typedef PodQueue<NodeId> Clasp::DefaultUnfoundedCheck::IdQueue [private]

Definition at line 260 of file unfounded_check.h.

typedef SingleOwnerPtr<MinimalityCheck> Clasp::DefaultUnfoundedCheck::MiniPtr [private]

Definition at line 261 of file unfounded_check.h.

typedef DependencyGraph::NodeId Clasp::DefaultUnfoundedCheck::NodeId

Definition at line 51 of file unfounded_check.h.

typedef PodVector<ExtWatch>::type Clasp::DefaultUnfoundedCheck::WatchVec [private]

Definition at line 259 of file unfounded_check.h.

Member Enumeration Documentation

enum Clasp::DefaultUnfoundedCheck::ReasonStrategy

Defines the supported reasons for explaining assignments.

Enumerator:

common_reason	one reason for each unfounded set but one clause for each atom
distinct_reason	distinct reason and clause for each unfounded atom
shared_reason	one shared loop formula for each unfounded set
only_reason	store only the reason but don't learn a nogood
no_reason	do no compute reasons for unfounded sets (only valid if learning is disabled!)

Definition at line 55 of file unfounded_check.h.

enum Clasp::DefaultUnfoundedCheck::UfsType [private]

Enumerator:

ufs_none
ufs_poly
ufs_non_poly

Definition at line 81 of file unfounded_check.h.

enum Clasp::DefaultUnfoundedCheck::WatchType [private]

Enumerator:

watch_source_false
watch_head_false
watch_head_true
watch_subgoal_false

Definition at line 86 of file unfounded_check.h.

Constructor & Destructor Documentation

Clasp::DefaultUnfoundedCheck::DefaultUnfoundedCheck ( )

Definition at line 72 of file unfounded_check.cpp.

Clasp::DefaultUnfoundedCheck::~DefaultUnfoundedCheck ( )

Definition at line 80 of file unfounded_check.cpp.

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

Member Function Documentation

void Clasp::DefaultUnfoundedCheck::addDeltaReason	(	const BodyPtr &	body,
		uint32	uScc
	)		`[private]`

Definition at line 606 of file unfounded_check.cpp.

void Clasp::DefaultUnfoundedCheck::addExtWatch	(	Literal	p,
		const BodyPtr &	n,
		uint32	data
	)		`[private]`

Definition at line 194 of file unfounded_check.cpp.

void Clasp::DefaultUnfoundedCheck::addIfReason	(	const BodyPtr &	n,
		uint32	uScc
	)		`[private]`

Definition at line 639 of file unfounded_check.cpp.

void Clasp::DefaultUnfoundedCheck::addReasonLit ( Literal p ) [private]

Definition at line 691 of file unfounded_check.cpp.

void Clasp::DefaultUnfoundedCheck::addUnsourced ( const BodyPtr & n ) [private]

Definition at line 499 of file unfounded_check.cpp.

void Clasp::DefaultUnfoundedCheck::addWatch	(	Literal	p,
		uint32	data,
		WatchType	type
	)		`[private]`

Definition at line 89 of file unfounded_check.cpp.

bool Clasp::DefaultUnfoundedCheck::assertAtom	(	Literal	a,
		UfsType	t
	)		`[private]`

Definition at line 531 of file unfounded_check.cpp.

void Clasp::DefaultUnfoundedCheck::computeReason ( UfsType t ) [private]

Definition at line 578 of file unfounded_check.cpp.

void Clasp::DefaultUnfoundedCheck::createLoopFormula ( ) [private]

Definition at line 555 of file unfounded_check.cpp.

bool Clasp::DefaultUnfoundedCheck::falsifyUfs ( UfsType t ) [private]

Definition at line 509 of file unfounded_check.cpp.

DefaultUnfoundedCheck::UfsType Clasp::DefaultUnfoundedCheck::findNonHcfUfs ( Solver & s ) [private]

Definition at line 705 of file unfounded_check.cpp.

bool Clasp::DefaultUnfoundedCheck::findSource ( NodeId atom ) [private]

Definition at line 415 of file unfounded_check.cpp.

DefaultUnfoundedCheck::UfsType Clasp::DefaultUnfoundedCheck::findUfs	(	Solver &	s,
		bool	checkNonHcf
	)		`[private]`

Definition at line 395 of file unfounded_check.cpp.

void Clasp::DefaultUnfoundedCheck::forwardSource ( const BodyPtr & n ) [private]

Definition at line 297 of file unfounded_check.cpp.

void Clasp::DefaultUnfoundedCheck::forwardUnsource	(	const BodyPtr &	n,
		bool	add
	)		`[private]`

Definition at line 304 of file unfounded_check.cpp.

BodyPtr Clasp::DefaultUnfoundedCheck::getBody ( NodeId bId ) const [inline, private]

Definition at line 182 of file unfounded_check.h.

DependencyGraph* Clasp::DefaultUnfoundedCheck::graph ( ) const [inline]

Definition at line 68 of file unfounded_check.h.

bool Clasp::DefaultUnfoundedCheck::init ( Solver & s ) [virtual]

Called during initialization of s.

Note:: During initialization a post propagator may assign variables but it must not yet propagate them.

Reimplemented from Clasp::PostPropagator.

Definition at line 98 of file unfounded_check.cpp.

void Clasp::DefaultUnfoundedCheck::initBody ( const BodyPtr & n ) [private]

Definition at line 156 of file unfounded_check.cpp.

void Clasp::DefaultUnfoundedCheck::initExtBody ( const BodyPtr & n ) [private]

Definition at line 167 of file unfounded_check.cpp.

void Clasp::DefaultUnfoundedCheck::initSuccessors	(	const BodyPtr &	n,
		weight_t	lower
	)		`[private]`

Definition at line 182 of file unfounded_check.cpp.

bool Clasp::DefaultUnfoundedCheck::isModel ( Solver & s ) [virtual]

Is the current total assignment a model?

Precondition:: The assignment is total and not conflicting.

Returns:

true if the assignment is a model w.r.t this post propagator
false otherwise

Postcondition:: If the function returned true: s.numFreeVars() == 0 && !s.hasConflict(). If the function returned false: s.numFreeVars() > 0 || s.hasConflict().

Note:: The default implementation returns Constraint::valid(s);

Reimplemented from Clasp::PostPropagator.

Definition at line 241 of file unfounded_check.cpp.

bool Clasp::DefaultUnfoundedCheck::isValidSource ( const BodyPtr & n ) [private]

Definition at line 465 of file unfounded_check.cpp.

uint32 Clasp::DefaultUnfoundedCheck::nodes ( ) const [inline]

Definition at line 69 of file unfounded_check.h.

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

uint32 Clasp::DefaultUnfoundedCheck::priority ( ) const [inline, virtual]

Shall return a value representing the priority of this propagator.

The priority is used to order sequences of post propagators and to classify post propagators w.r.t the classes: class_simple and class_general.

Note:: See class description for an overview of the two priority classes.

Implements Clasp::PostPropagator.

Definition at line 72 of file unfounded_check.h.

PropResult Clasp::DefaultUnfoundedCheck::propagate	(	Solver &	s,
		Literal	p,
		uint32 &	data
	)		`[inline, private, 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.

Reimplemented from Clasp::PostPropagator.

Definition at line 171 of file unfounded_check.h.

bool Clasp::DefaultUnfoundedCheck::propagateFixpoint	(	Solver &	s,
		PostPropagator *	ctx
	)		`[virtual]`

Shall enqueue and propagate new assignments implied by this propagator.

This function shall enqueue and propagate all assignments currently implied by this propagator until a fixpoint is reached w.r.t this post propagator or a conflict is detected.

Precondition:: The assignment is fully propagated w.r.t any previous post propagator.

Parameters:

s	The solver in which this post propagator is used.
ctx	The post propagator from which this post propagator is called or 0 if no other post propagator is currently active.

Postcondition:: s.queueSize() == 0 || s.hasConflict()

Returns:: false if propagation led to conflict, true otherwise

Note:: The function shall not call Solver::propagate() or any other function that would result in a recursive chain of propagate() calls. On the other hand, it shall call Solver::propagateUntil(this) after enqueuing new assignments to initiate propagation up to this propagator.

Typically, propagateFixpoint() should implemet a loop like this:

 for (;;) {
   if (!assign_newly_implied_literals(s)){ return false; }
   if (s.queueSize() == 0)               { return true;  }
   if (!s.propagateUntil(this))          { return false; }
 }

Implements Clasp::PostPropagator.

Definition at line 216 of file unfounded_check.cpp.

void Clasp::DefaultUnfoundedCheck::propagateSource ( ) [private]

Definition at line 248 of file unfounded_check.cpp.

bool Clasp::DefaultUnfoundedCheck::pushTodo ( NodeId at ) [inline, private]

Definition at line 251 of file unfounded_check.h.

bool Clasp::DefaultUnfoundedCheck::pushUfs ( NodeId at ) [inline, private]

Definition at line 252 of file unfounded_check.h.

void Clasp::DefaultUnfoundedCheck::reason	(	Solver &	s,
		Literal	p,
		LitVec &	lits
	)		`[private, virtual]`

Precondition:: This constraint is the reason for p being true in s.

Postcondition:: The literals implying p were added to lits.

Reimplemented from Clasp::PostPropagator.

Definition at line 202 of file unfounded_check.cpp.

ReasonStrategy Clasp::DefaultUnfoundedCheck::reasonStrategy ( ) const [inline]

Definition at line 66 of file unfounded_check.h.

void Clasp::DefaultUnfoundedCheck::removeSource ( NodeId bodyId ) [private]

Definition at line 334 of file unfounded_check.cpp.

void Clasp::DefaultUnfoundedCheck::reset ( ) [virtual]

Aborts an active propagation operation.

The function reset() is called whenever propagation on the current decision level is stopped before a fixpoint is reached. In particular, a solver calls reset() when a conflict is detected during propagation.