Stores assignment related information. More...

#include <solver_types.h>

Collaboration diagram for Clasp::Assignment:

Public Types
typedef PodVector< uint32 >::type	AssignVec

typedef PodVector< ValueSet >::type	PrefVec

typedef bk_lib::detail::if_then_else < sizeof(Constraint *)==sizeof(uint64), ReasonStore64, ReasonStore32 > ::type	ReasonVec

typedef ReasonVec::value_type	ReasonWithData

Public Member Functions
	Assignment ()

bool	qEmpty () const

uint32	qSize () const

Literal	qPop ()

void	qReset ()

uint32	numVars () const
	Number of variables in the three-valued assignment. More...

uint32	assigned () const
	Number of assigned variables. More...

uint32	free () const
	Number of free variables. More...

uint32	maxLevel () const
	Returns the largest possible decision level. More...

ValueRep	value (Var v) const
	Returns v's value in the three-valued assignment. More...

uint32	level (Var v) const
	Returns the decision level on which v was assigned if value(v) != value_free. More...

bool	valid (Var v) const
	Returns true if v was not eliminated from the assignment. More...

const ValueSet	pref (Var v) const
	Returns the set of preferred values of v. More...

const Antecedent &	reason (Var v) const
	Returns the reason for v being assigned if value(v) != value_free. More...

uint32	numData () const
	Returns the number of allocated data slots. More...

uint32	data (Var v) const
	Returns the reason data associated with v. More...

void	resize (uint32 nv)
	Resize to nv variables. More...

Var	addVar ()
	Adds a var to assignment - initially the new var is unassigned. More...

void	requestPrefs ()
	Allocates space for storing preferred values for all variables. More...

void	requestData (uint32 nv)
	Allocates data slots for nv variables to be used for storing additional reason data. More...

void	eliminate (Var v)
	Eliminates v from the assignment. More...

bool	assign (Literal p, uint32 lev, const Antecedent &x)
	Assigns p.var() on level lev to the value that makes p true and stores x as reason for the assignment. More...

bool	assign (Literal p, uint32 lev, Constraint *c, uint32 data)

void	undoTrail (LitVec::size_type first, bool save)
	Undos all assignments in the range trail[first, last). More...

void	undoLast ()
	Undos the last assignment. More...

Literal	last () const
	Returns the last assignment as a true literal. More...

Literal &	last ()

Implementation functions
Low-level implementation functions. Use with care and only if you know what you are doing!
uint32	units () const

bool	seen (Var v, uint8 m) const

void	setSeen (Var v, uint8 m)

void	clearSeen (Var v)

void	clearValue (Var v)

void	setValue (Var v, ValueRep val)

void	setReason (Var v, const Antecedent &a)

void	setData (Var v, uint32 data)

void	setPref (Var v, ValueSet::Value which, ValueRep to)

void	copyAssignment (Assignment &o) const

bool	markUnits ()

void	setUnits (uint32 ts)

Public Attributes
LitVec	trail

LitVec::size_type	front

Detailed Description

Stores assignment related information.

For each variable v, the class stores

v's current value (value_free if unassigned)
the decision level on which v was assign (only valid if value(v) != value_free)
the reason why v is in the assignment (only valid if value(v) != value_free)
(optionally) some additional data associated with the reason

Furthermore, the class stores the sequences of assignments as a set of true literals in its trail-member.

Member Typedef Documentation

typedef PodVector<uint32>::type Clasp::Assignment::AssignVec

typedef PodVector<ValueSet>::type Clasp::Assignment::PrefVec

typedef bk_lib::detail::if_then_else< sizeof(Constraint*)==sizeof(uint64) , ReasonStore64 , ReasonStore32>::type Clasp::Assignment::ReasonVec

typedef ReasonVec::value_type Clasp::Assignment::ReasonWithData

Constructor & Destructor Documentation

Clasp::Assignment::Assignment ( )

inline

Member Function Documentation

Var Clasp::Assignment::addVar ( )

inline

Adds a var to assignment - initially the new var is unassigned.

bool Clasp::Assignment::assign	(	Literal	p,
		uint32	lev,
		const Antecedent &	x
	)

inline

Assigns p.var() on level lev to the value that makes p true and stores x as reason for the assignment.

Returns: true if the assignment is consistent. False, otherwise.

Postcondition: If true is returned, p is in trail. Otherwise, ~p is.

Here is the call graph for this function:

bool Clasp::Assignment::assign	(	Literal	p,
		uint32	lev,
		Constraint *	c,
		uint32	data
	)

inline

Here is the call graph for this function:

uint32 Clasp::Assignment::assigned ( ) const

inline

Number of assigned variables.

void Clasp::Assignment::clearSeen ( Var v )

inline

void Clasp::Assignment::clearValue ( Var v )

inline

void Clasp::Assignment::copyAssignment ( Assignment & o ) const

inline

uint32 Clasp::Assignment::data ( Var v ) const

inline

Returns the reason data associated with v.

void Clasp::Assignment::eliminate ( Var v )

inline

Eliminates v from the assignment.

uint32 Clasp::Assignment::free ( ) const

inline

Number of free variables.

Literal Clasp::Assignment::last ( ) const

inline

Returns the last assignment as a true literal.

Literal& Clasp::Assignment::last ( )

inline

uint32 Clasp::Assignment::level ( Var v ) const

inline

Returns the decision level on which v was assigned if value(v) != value_free.

bool Clasp::Assignment::markUnits ( )

inline

uint32 Clasp::Assignment::maxLevel ( ) const

inline

Returns the largest possible decision level.

uint32 Clasp::Assignment::numData ( ) const

inline

Returns the number of allocated data slots.

uint32 Clasp::Assignment::numVars ( ) const

inline

Number of variables in the three-valued assignment.

const ValueSet Clasp::Assignment::pref ( Var v ) const

inline

Returns the set of preferred values of v.

bool Clasp::Assignment::qEmpty ( ) const

inline

Literal Clasp::Assignment::qPop ( )

inline

void Clasp::Assignment::qReset ( )

inline

uint32 Clasp::Assignment::qSize ( ) const

inline

const Antecedent& Clasp::Assignment::reason ( Var v ) const

inline

Returns the reason for v being assigned if value(v) != value_free.

void Clasp::Assignment::requestData ( uint32 nv )

inline

Allocates data slots for nv variables to be used for storing additional reason data.

void Clasp::Assignment::requestPrefs ( )

inline

Allocates space for storing preferred values for all variables.

void Clasp::Assignment::resize ( uint32 nv )

inline

Resize to nv variables.

bool Clasp::Assignment::seen	(	Var	v,
		uint8	m
	)		const

inline

void Clasp::Assignment::setData	(	Var	v,
		uint32	data
	)

inline

void Clasp::Assignment::setPref	(	Var	v,
		ValueSet::Value	which,
		ValueRep	to
	)

inline

void Clasp::Assignment::setReason	(	Var	v,
		const Antecedent &	a
	)

inline

void Clasp::Assignment::setSeen	(	Var	v,
		uint8	m
	)

inline

void Clasp::Assignment::setUnits ( uint32 ts )

inline

void Clasp::Assignment::setValue	(	Var	v,
		ValueRep	val
	)

inline

Here is the call graph for this function:

void Clasp::Assignment::undoLast ( )

inline

Undos the last assignment.

void Clasp::Assignment::undoTrail	(	LitVec::size_type	first,
		bool	save
	)

inline

Undos all assignments in the range trail[first, last).

Parameters

first	First assignment to be undone.
save	If true, previous assignment of a var is saved before it is undone.

uint32 Clasp::Assignment::units ( ) const

inline

bool Clasp::Assignment::valid ( Var v ) const

inline

Returns true if v was not eliminated from the assignment.

ValueRep Clasp::Assignment::value ( Var v ) const

inline

Returns v's value in the three-valued assignment.

Member Data Documentation

LitVec::size_type Clasp::Assignment::front

LitVec Clasp::Assignment::trail

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

/Users/danielbaeck/Dropbox/Uni Klagenfurt/Diplomarbeit/gringo44/libclasp/clasp/solver_types.h

Public Types

Public Member Functions

Public Attributes

Detailed Description

Member Typedef Documentation

Constructor & Destructor Documentation

Member Function Documentation

Member Data Documentation