wali::witness::Witness Class Reference

List of all members.

Public Member Functions
	Witness (sem_elem_t se)
virtual	~Witness ()
bool	isZero ()
bool	isOne ()
virtual sem_elem_t	one () const
virtual sem_elem_t	zero () const
virtual sem_elem_t	extend (SemElem *se)
virtual sem_elem_t	combine (SemElem *se)
virtual bool	equal (SemElem *se) const
virtual std::ostream &	print (std::ostream &o) const
	Print the Witness to the parameter o.
virtual void	accept (Visitor &v, bool visitOnce=false)
virtual std::ostream &	prettyPrint (std::ostream &o, size_t depth) const
	Pretty print in a DAG like structure to the ostream.
std::ostream &	formatDepth (std::ostream &o, size_t depth) const
	Prints " |" to parameter o for each level of depth.
sem_elem_t	weight ()
virtual void	reset_marks () const
	Reset all marks (recursively).
Static Public Attributes
static int	COUNT = 0
Protected Attributes
sem_elem_t	user_se
	The user SemElem value.
bool	isEmpty
	True if type == Witness. Cheap reflection.

---

Constructor & Destructor Documentation

wali::witness::Witness::Witness

(

sem_elem_t

se

)

References COUNT.

Referenced by one(), and zero().

wali::witness::Witness::~Witness

(

)

[virtual]

References COUNT.

---

Member Function Documentation

bool wali::witness::Witness::isZero

(

)

Test if the Witness has user weight ZERO

References user_se.

Referenced by wali::witness::WitnessCombine::combine(), and combine().

bool wali::witness::Witness::isOne

(

)

Test if the Witness has user weight ONE

References user_se.

Referenced by extend().

sem_elem_t wali::witness::Witness::one

(

)

const [virtual]

Returns a new Witness whose user_se is a sem_elem_t ONE element of the user's weight domain.

See also:

SemElem

sem_elem_t

References user_se, and Witness().

sem_elem_t wali::witness::Witness::zero

(

)

const [virtual]

Returns a new Witness whose user_se is a sem_elem_t ZERO element of the user's weight domain.

See also:

SemElem

sem_elem_t

References user_se, and Witness().

sem_elem_t wali::witness::Witness::extend

(

SemElem *

se

)

[virtual]

Extend the user supplied weight and create a new WitnessExtend.

See also:

WitnessExtend

References isEmpty, isOne(), wali::SemElem::print(), user_se, and wali::waliErr.

sem_elem_t wali::witness::Witness::combine

(

SemElem *

se

)

[virtual]

Combines the user's weight and creates a WitnessCombine if parameter "se" is not already a WitnessCombine.

See also:

SemElem

sem_elem_t

WitnessCombine

Reimplemented in wali::witness::WitnessCombine.

References wali::witness::WitnessCombine::addChild(), isZero(), user_se, and wali::waliErr.

bool wali::witness::Witness::equal

(

SemElem *

se

)

const [virtual]

Test for equality of user supplied weight. The Witness is simply along for the ride.

References user_se.

std::ostream & wali::witness::Witness::print

(

std::ostream &

o

)

const [virtual]

Print the Witness to the parameter o.

References prettyPrint().

void wali::witness::Witness::accept	(	Visitor &	v,
		bool visitOnce	ATTR_UNUSED = false
	)			[virtual]

Accept method allows for different behaviors to be applied to the Witness DAG.

See also:

Visitor

Implements wali::witness::Visitable.

Reimplemented in wali::witness::WitnessCombine, wali::witness::WitnessExtend, wali::witness::WitnessMerge, wali::witness::WitnessRule, and wali::witness::WitnessTrans.

References wali::Markable::mark(), and wali::witness::Visitor::visit().

Referenced by wali::witness::WitnessCombine::combine(), and opennwa::query::getSomeAcceptedWordInternal().

std::ostream & wali::witness::Witness::prettyPrint	(	std::ostream &	o,
		size_t	depth
	)			const [virtual]

Pretty print in a DAG like structure to the ostream.

Reimplemented in wali::witness::WitnessCombine, wali::witness::WitnessExtend, wali::witness::WitnessMerge, wali::witness::WitnessRule, and wali::witness::WitnessTrans.

References formatDepth(), and user_se.

Referenced by print().

std::ostream & wali::witness::Witness::formatDepth	(	std::ostream &	o,
		size_t	depth
	)			const

Prints " |" to parameter o for each level of depth.

Referenced by wali::witness::WitnessTrans::prettyPrint(), wali::witness::WitnessRule::prettyPrint(), wali::witness::WitnessMerge::prettyPrint(), wali::witness::WitnessExtend::prettyPrint(), wali::witness::WitnessCombine::prettyPrint(), and prettyPrint().

sem_elem_t wali::witness::Witness::weight

(

)

Returns protected sem_elem_t se member variable that is the user supplied weight or from a computation involving the user defined semiring.

See also:

sem_elem_t

References user_se.

Referenced by wali::witness::WitnessCombine::combine(), wali::witness::VisitorDot::printNode(), wali::witness::WitnessMergeFn::priv_do_apply(), wali::witness::WitnessWrapper::unwrap(), wali::witness::VisitorPrinter::visitCombine(), wali::witness::VisitorDot::visitCombine(), wali::witness::VisitorPrinter::visitExtend(), wali::witness::VisitorDot::visitExtend(), wali::witness::VisitorPrinter::visitMerge(), and wali::witness::VisitorDot::visitMerge().

void wali::witness::Witness::reset_marks

(

)

const [virtual]

Reset all marks (recursively).

Reimplemented in wali::witness::WitnessCombine, wali::witness::WitnessExtend, and wali::witness::WitnessMerge.

References wali::Markable::unmark().

---

Member Data Documentation

int wali::witness::Witness::COUNT = 0 [static]

Referenced by Witness(), and ~Witness().

sem_elem_t wali::witness::Witness::user_se [protected]

The user SemElem value.

Referenced by wali::witness::WitnessCombine::combine(), combine(), equal(), extend(), isOne(), isZero(), one(), wali::witness::WitnessMerge::prettyPrint(), wali::witness::WitnessExtend::prettyPrint(), wali::witness::WitnessCombine::prettyPrint(), prettyPrint(), weight(), and zero().

bool wali::witness::Witness::isEmpty [protected]

True if type == Witness. Cheap reflection.

Referenced by extend().

---

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

• Source/wali/witness/Witness.hpp
• Source/wali/witness/Witness.cpp