PredicateNormaliser Struct Reference

Public interface for a predicate-normaliser class. More...

#include <PredicateNormaliser.h>

Related Functions
(Note that these are not member functions.)
PredicateNormaliser_ptr	PredicateNormaliser_create (SymbTable_ptr st)
	The constructor creates a predicate-normaliser.
void	PredicateNormaliser_destroy (PredicateNormaliser_ptr self)
	Class PredicateNormaliser destructor.
void	PredicateNormaliser_get_predicates_only (const PredicateNormaliser_ptr self, Set_t *preds, node_ptr expr)
	The function adds to the given set the expression's predicates, i.e. subexpressions which have not-boolean operands.
node_ptr	PredicateNormaliser_normalise_expr (PredicateNormaliser_ptr self, node_ptr expr)
	The function performs predicate-normalisation of a generic boolean expression.
node_ptr	PredicateNormaliser_normalise_expr_no_expand (PredicateNormaliser_ptr self, node_ptr expr)
	The function performs predicate-normalisation of a generic boolean expression, but it does not expand the defines.
node_ptr	PredicateNormaliser_normalise_specification (PredicateNormaliser_ptr self, node_ptr expr)
	The function performs predicate-normalisation of specification (SPEC, LTLSPEC, etc).
void	PredicateNormaliser_print_predicates_only (const PredicateNormaliser_ptr self, FILE *stream, node_ptr expr)
	The function prints out the expressions's predicates, i.e. subexpressions which have not-boolean operands.

---

Detailed Description

Public interface for a predicate-normaliser class.

Author:

Andrei Tchaltsev The purpose of a predicate normaliser is to take a symbolic expression (node_ptr), normalise predicates and return a newly created expressions with normlised predicates. A predicate-normalised expression is an expression where none of not-boolean subexpressions may have a boolean subexpression, i.e. only boolean expressions may have boolean subexpressions. Normalisation is done by (creating and) pushing IfThenElse expression up to the root of not-boolean subexpression. For example,

"case a : 3; 1 : 4; esac + 2 = 7"

have boolean expression "a" as a subexpression of not-boolean expression "case ...". The normalised version will look like "case a : 3 + 2 = 7; 1 : 4 + 2 = 7; esac"

This is a stand-alone class. This class needs only a type checker -- to get the type of input expression and type check the generated (returned) expressions.

Preicate Normaliser class

---

Friends And Related Function Documentation

PredicateNormaliser_ptr PredicateNormaliser_create

(

SymbTable_ptr

st

)

[related]

The constructor creates a predicate-normaliser.

See PredicateNormaliser.h for more info on predicate normalisation. The paramer 'checker' is a type checker used during predication-normalisation, and subsequent type checking of generated expressions. NOTE that the type checker remember the type of checked expressions.

void PredicateNormaliser_destroy

(

PredicateNormaliser_ptr

self

)

[related]

Class PredicateNormaliser destructor.

void PredicateNormaliser_get_predicates_only	(	const PredicateNormaliser_ptr	self,
		Set_t *	preds,
		node_ptr	expr
	)			[related]

The function adds to the given set the expression's predicates, i.e. subexpressions which have not-boolean operands.

Only boolean expressions obtained with PredicateNormaliser_normalise_expr and with the same predicate-normaliser (i.e. 'self') can be given to this function.

See function PredicateNormaliser_compute_predicates_and_clusters if only predicates are required without normalization of a whole expression.

This function just walks the exressions, tries to find a subexpression with not-boolean operands then adds it to the given set. Every predicate is added only once.

node_ptr PredicateNormaliser_normalise_expr	(	PredicateNormaliser_ptr	self,
		node_ptr	expr
	)			[related]

The function performs predicate-normalisation of a generic boolean expression.

The function returns a new expression -- a predicate-normalised version of the given one. A predicate normalised expression is a symbolic expression (Sexp) whose not-boolean subexpressions do not encompass boolean subexpression. For example, not predicate-normalised expression "case a : 3; 1 : 4; esac + 2 = 7" after normalisatio becomes "case a : 3 + 2 = 7; 1 : 4 + 2 = 7; esac"

The provided expression should be scalar (since there is no meaning to normalise booleanised expressions). The given expression must be already type checked (by the type checker given to the constructor), but may be or may not be flattened and expanded.

During normalisation the type checker (given during construction) is used to distinguish boolean from not-boolean expressions. Note that the generated expressions may be type checked, i.e. the type checker remember their types.

The normaliser caches processed expressions. So, if the same expression is given, the same result will be returned.

The returned expression is always flattened and expanded. Also, it is created by find_node function, therefore it belongs to the node package (i.e. do not modify it).

NOTE: if only predicates are required at the end and not the whole normalized expressions, then it is better to use PredicateExtractor class.

node_ptr PredicateNormaliser_normalise_expr_no_expand	(	PredicateNormaliser_ptr	self,
		node_ptr	expr
	)			[related]

The function performs predicate-normalisation of a generic boolean expression, but it does not expand the defines.

This is similar to the PredicateNormaliser_normalise_expr, i.e. it returns a flattened expression with predicates on the leaves, but differently from PredicateNormaliser_normalise_expr, the defines are not expanded.

The returned expression is created by find_node function, therefore it belongs to the node package (i.e. do not modify it).

NOTE: if only predicates are required at the end and not the whole normalized expressions, then it is better to use PredicateExtractor class.

node_ptr PredicateNormaliser_normalise_specification	(	PredicateNormaliser_ptr	self,
		node_ptr	expr
	)			[related]

The function performs predicate-normalisation of specification (SPEC, LTLSPEC, etc).

This function does the same things as PredicateNormaliser_normalise_expr, except that the input expression must be a specification (such expression are returned by Prop_get_expr_core)

void PredicateNormaliser_print_predicates_only	(	const PredicateNormaliser_ptr	self,
		FILE *	stream,
		node_ptr	expr
	)			[related]

The function prints out the expressions's predicates, i.e. subexpressions which have not-boolean operands.

Only expressions obtained with PredicateNormaliser_normalise_expr and with the same predicate-normaliser (i.e. 'self') can be given to this function.

This function just walks the exressions, tries to find a subexpression with not-boolean operands then print it.

PredicateNormaliser_get_predicates_only

---

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

• NuSMV/code/nusmv/core/compile/PredicateNormaliser.h