Stores assignment related information. More...

#include <solver_types.h>

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 > ::typ	ReasonVec )
typedef ReasonVec::value_type	ReasonWithData
Public Member Functions
Var	addVar ()
	Adds a var to assignment - initially the new var is unassigned.
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.
bool	assign (Literal p, uint32 lev, Constraint *c, uint32 data)
uint32	assigned () const
	Number of assigned variables.
	Assignment ()
uint32	data (Var v) const
	Returns the reason data associated with v.
void	eliminate (Var v)
	Eliminates v from the assignment.
uint32	free () const
	Number of free variables.
Literal	last () const
	Returns the last assignment as a true literal.
Literal &	last ()
uint32	level (Var v) const
	Returns the decision level on which v was assigned if value(v) != value_free.
uint32	maxLevel () const
	Returns the largest possible decision level.
uint32	numData () const
	Returns the number of allocated data slots.
uint32	numVars () const
	Number of variables in the three-valued assignment.
const ValueSet	pref (Var v) const
	Returns the set of preferred values of v.
bool	qEmpty () const
Literal	qPop ()
void	qReset ()
uint32	qSize () const
const Antecedent &	reason (Var v) const
	Returns the reason for v being assigned if value(v) != value_free.
void	requestData (uint32 nv)
	Allocates data slots for nv variables to be used for storing additional reason data.
void	requestPrefs ()
	Allocates space for storing preferred values for all variables.
void	resize (uint32 nv)
	Resize to nv variables.
void	undoLast ()
	Undos the last assignment.
void	undoTrail (LitVec::size_type first, bool save)
	Undos all assignments in the range trail[first, last).
bool	valid (Var v) const
	Returns true if v was not eliminated from the assignment.
ValueRep	value (Var v) const
	Returns v's value in the three-valued assignment.
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::size_type	front
LitVec	trail
Private Member Functions
	Assignment (const Assignment &)
void	clear (Var v)
Assignment &	operator= (const Assignment &)
template<void(Assignment::*)(Var v) op>
void	popUntil (Literal stop)
void	saveAndClear (Var v)
Private Attributes
AssignVec	assign_
uint32	elims_
PrefVec	pref_
ReasonVec	reason_
uint32	units_
Static Private Attributes
static const uint32	elim_mask = uint32(0xFFFFFFF0u)

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.

Definition at line 653 of file solver_types.h.

Member Typedef Documentation

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

Definition at line 655 of file solver_types.h.

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

Definition at line 656 of file solver_types.h.

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

Definition at line 660 of file solver_types.h.

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

Definition at line 661 of file solver_types.h.

Constructor & Destructor Documentation

Clasp::Assignment::Assignment ( ) [inline]

Definition at line 662 of file solver_types.h.

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

Member Function Documentation

Var Clasp::Assignment::addVar ( ) [inline]

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

Definition at line 699 of file solver_types.h.

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.

Definition at line 722 of file solver_types.h.

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

Definition at line 734 of file solver_types.h.

uint32 Clasp::Assignment::assigned ( ) const [inline]

Number of assigned variables.

Definition at line 673 of file solver_types.h.

void Clasp::Assignment::clear ( Var v ) [inline, private]

Definition at line 788 of file solver_types.h.

void Clasp::Assignment::clearSeen ( Var v ) [inline]

Definition at line 771 of file solver_types.h.

void Clasp::Assignment::clearValue ( Var v ) [inline]

Definition at line 772 of file solver_types.h.

void Clasp::Assignment::copyAssignment ( Assignment & o ) const [inline]

Definition at line 780 of file solver_types.h.

uint32 Clasp::Assignment::data ( Var v ) const [inline]

Returns the reason data associated with v.

Definition at line 691 of file solver_types.h.

void Clasp::Assignment::eliminate ( Var v ) [inline]

Eliminates v from the assignment.

Definition at line 713 of file solver_types.h.

uint32 Clasp::Assignment::free ( ) const [inline]

Number of free variables.

Definition at line 675 of file solver_types.h.

Literal Clasp::Assignment::last ( ) const [inline]

Returns the last assignment as a true literal.

Definition at line 760 of file solver_types.h.

Literal& Clasp::Assignment::last ( ) [inline]

Definition at line 761 of file solver_types.h.

uint32 Clasp::Assignment::level ( Var v ) const [inline]

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

Definition at line 681 of file solver_types.h.

bool Clasp::Assignment::markUnits ( ) [inline]

Definition at line 781 of file solver_types.h.

uint32 Clasp::Assignment::maxLevel ( ) const [inline]

Returns the largest possible decision level.

Definition at line 677 of file solver_types.h.

uint32 Clasp::Assignment::numData ( ) const [inline]

Returns the number of allocated data slots.

Definition at line 689 of file solver_types.h.

uint32 Clasp::Assignment::numVars ( ) const [inline]

Number of variables in the three-valued assignment.

Definition at line 671 of file solver_types.h.

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

template<void(Assignment::*)(Var v) op>

void Clasp::Assignment::popUntil ( Literal stop ) [inline, private]

Definition at line 791 of file solver_types.h.

const ValueSet Clasp::Assignment::pref ( Var v ) const [inline]

Returns the set of preferred values of v.

Definition at line 685 of file solver_types.h.

bool Clasp::Assignment::qEmpty ( ) const [inline]

Definition at line 665 of file solver_types.h.

Literal Clasp::Assignment::qPop ( ) [inline]

Definition at line 667 of file solver_types.h.

void Clasp::Assignment::qReset ( ) [inline]

Definition at line 668 of file solver_types.h.

uint32 Clasp::Assignment::qSize ( ) const [inline]

Definition at line 666 of file solver_types.h.

const Antecedent& Clasp::Assignment::reason ( Var v ) const [inline]

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

Definition at line 687 of file solver_types.h.

void Clasp::Assignment::requestData ( uint32 nv ) [inline]

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

Definition at line 709 of file solver_types.h.

void Clasp::Assignment::requestPrefs ( ) [inline]

Allocates space for storing preferred values for all variables.

Definition at line 705 of file solver_types.h.

void Clasp::Assignment::resize ( uint32 nv ) [inline]

Resize to nv variables.

Definition at line 694 of file solver_types.h.

void Clasp::Assignment::saveAndClear ( Var v ) [inline, private]

Definition at line 789 of file solver_types.h.

bool Clasp::Assignment::seen	(	Var	v,
		uint8	m
	)		const `[inline]`

Definition at line 769 of file solver_types.h.

void Clasp::Assignment::setData	(	Var	v,
		uint32	data
	)		`[inline]`

Definition at line 778 of file solver_types.h.

void Clasp::Assignment::setPref	(	Var	v,
		ValueSet::Value	which,
		ValueRep	to
	)		`[inline]`

Definition at line 779 of file solver_types.h.

void Clasp::Assignment::setReason	(	Var	v,
		const Antecedent &	a
	)		`[inline]`

Definition at line 777 of file solver_types.h.

void Clasp::Assignment::setSeen	(	Var	v,
		uint8	m
	)		`[inline]`

Definition at line 770 of file solver_types.h.

void Clasp::Assignment::setUnits ( uint32 ts ) [inline]

Definition at line 782 of file solver_types.h.

void Clasp::Assignment::setValue	(	Var	v,
		ValueRep	val
	)		`[inline]`

Definition at line 773 of file solver_types.h.

void Clasp::Assignment::undoLast ( ) [inline]

Undos the last assignment.

Definition at line 758 of file solver_types.h.

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.

Definition at line 752 of file solver_types.h.

uint32 Clasp::Assignment::units ( ) const [inline]

Definition at line 768 of file solver_types.h.

bool Clasp::Assignment::valid ( Var v ) const [inline]

Returns true if v was not eliminated from the assignment.

Definition at line 683 of file solver_types.h.

ValueRep Clasp::Assignment::value ( Var v ) const [inline]

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

Definition at line 679 of file solver_types.h.

Member Data Documentation

AssignVec Clasp::Assignment::assign_ [private]

Definition at line 798 of file solver_types.h.

const uint32 Clasp::Assignment::elim_mask = uint32(0xFFFFFFF0u) [static, private]

Definition at line 785 of file solver_types.h.

uint32 Clasp::Assignment::elims_ [private]

Definition at line 801 of file solver_types.h.

LitVec::size_type Clasp::Assignment::front

Definition at line 664 of file solver_types.h.

PrefVec Clasp::Assignment::pref_ [private]

Definition at line 800 of file solver_types.h.

ReasonVec Clasp::Assignment::reason_ [private]

Definition at line 799 of file solver_types.h.

LitVec Clasp::Assignment::trail

Definition at line 663 of file solver_types.h.

uint32 Clasp::Assignment::units_ [private]

Definition at line 802 of file solver_types.h.

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

solver_types.h

Public Types

Public Member Functions

Public Attributes

Private Member Functions

Private Attributes

Static Private Attributes

Detailed Description

Member Typedef Documentation

Constructor & Destructor Documentation

Member Function Documentation

Member Data Documentation