ExprMgr Struct Reference

Definition of the public accessor for class ExprMgr. More...

#include <ExprMgr.h>

Related Functions
(Note that these are not member functions.)
Expr_ptr	ExprMgr_and (const ExprMgr_ptr self, const Expr_ptr a, const Expr_ptr b)
	Builds the logical/bitwise AND of given operators.
Expr_ptr	ExprMgr_and_from_list (const ExprMgr_ptr self, node_ptr list, const SymbTable_ptr st)
	Builds the logical/bitwise AND of all elements in the list.
Expr_ptr	ExprMgr_and_nil (const ExprMgr_ptr self, const Expr_ptr a, const Expr_ptr b)
	Builds the logical/bitwise AND of given operators, considering Nil as the true value.
Expr_ptr	ExprMgr_array_const (const ExprMgr_ptr self, const Expr_ptr a, const Expr_ptr v)
	Builds the node for CONSTARRAY (array const) of given variable a and value v.
Expr_ptr	ExprMgr_array_read (const ExprMgr_ptr self, const Expr_ptr a, const Expr_ptr i)
	Builds the node for READ (array read) of given array a and index i.
Expr_ptr	ExprMgr_array_write (const ExprMgr_ptr self, const Expr_ptr a, const Expr_ptr i, const Expr_ptr v)
	Builds the node for WRITE (array write) of given array a, index i, and value v.
Expr_ptr	ExprMgr_attime (const ExprMgr_ptr self, Expr_ptr e, int time, const SymbTable_ptr st)
	Creates a ATTIME node.
int	ExprMgr_attime_get_time (const ExprMgr_ptr self, Expr_ptr e)
	Retrieves the time out of an ATTIME node.
Expr_ptr	ExprMgr_attime_get_untimed (const ExprMgr_ptr self, Expr_ptr e)
	Retrieves the untimed node out of an ATTIME node.
Expr_ptr	ExprMgr_bool_to_word1 (const ExprMgr_ptr self, Expr_ptr a)
	Builds the node for casting boolean to word1.
Expr_ptr	ExprMgr_boolean_range (const ExprMgr_ptr self)
	Returns the false:true range value.
Expr_ptr	ExprMgr_cast_to_unsigned_word (const ExprMgr_ptr self, Expr_ptr width, Expr_ptr arg)
	Builds the node for CAST_TO_UNSIGNED_WORD.
Expr_ptr	ExprMgr_cast_toint (const ExprMgr_ptr self, Expr_ptr l, Expr_ptr r)
	Builds the node for CAST_TOINT.
ExprMgr_ptr	ExprMgr_create (const NuSMVEnv_ptr env)
	The ExprMgr class constructor.
void	ExprMgr_destroy (ExprMgr_ptr self)
	The ExprMgr class destructor.
Expr_ptr	ExprMgr_divide (const ExprMgr_ptr self, const Expr_ptr a, const Expr_ptr b)
	Builds the scalar node for DIVIDE of given operators.
Expr_ptr	ExprMgr_equal (const ExprMgr_ptr self, const Expr_ptr a, const Expr_ptr b, const SymbTable_ptr st)
	Builds the logical EQUAL of given operators.
Expr_ptr	ExprMgr_false (const ExprMgr_ptr self)
	Returns the false expression value.
Expr_ptr	ExprMgr_floor (const ExprMgr_ptr self, Expr_ptr l)
	Builds the node for FLOOR.
Expr_ptr	ExprMgr_function (const ExprMgr_ptr self, const Expr_ptr name, const Expr_ptr params)
	Builds an Uninterpreted function.
Expr_ptr	ExprMgr_ge (const ExprMgr_ptr self, const Expr_ptr a, const Expr_ptr b, const SymbTable_ptr st)
	Builds the predicate GE (greater-then-equal) of given operators.
NodeMgr_ptr	ExprMgr_get_node_manager (const ExprMgr_ptr self)
	Returns the internal NodeMgr.
int	ExprMgr_get_time (const ExprMgr_ptr self, SymbTable_ptr st, Expr_ptr expr)
	Obtain the base time of an expression.
int *	ExprMgr_get_time_interval (const ExprMgr_ptr self, const SymbTable_ptr st, Expr_ptr expr)
	Obtain the time interval of an expression.
Expr_ptr	ExprMgr_gt (const ExprMgr_ptr self, const Expr_ptr a, const Expr_ptr b)
	Builds the predicate GT (greater-then) of given operators.
Expr_ptr	ExprMgr_iff (const ExprMgr_ptr self, const Expr_ptr a, const Expr_ptr b)
	Builds the logical/bitwise IFF of given operators.
Expr_ptr	ExprMgr_implies (const ExprMgr_ptr self, const Expr_ptr a, const Expr_ptr b)
	Builds the logical/bitwise IMPLIES of given operators.
boolean	ExprMgr_is_boolean_range (const ExprMgr_ptr self, Expr_ptr expr)
	Checks whether the given expression is the false:true range value.
boolean	ExprMgr_is_equal_to_zero (const ExprMgr_ptr self, const Expr_ptr input)
	Checks if a costant number is zero.
boolean	ExprMgr_is_false (const ExprMgr_ptr self, const Expr_ptr expr)
	Checks whether given value is the false value.
boolean	ExprMgr_is_ge_to_number (const ExprMgr_ptr self, const Expr_ptr input, const Expr_ptr number)
	Compares a NUMBER to a constant number.
boolean	ExprMgr_is_number (const ExprMgr_ptr self, const Expr_ptr expr, const int value)
	Checks whether given value is the given scalar number.
boolean	ExprMgr_is_timed (const ExprMgr_ptr self, Expr_ptr expr, hash_ptr cache)
	Determines whether a formula has ATTIME nodes in it.
boolean	ExprMgr_is_true (const ExprMgr_ptr self, const Expr_ptr expr)
	Checks whether given value is the true value.
Expr_ptr	ExprMgr_ite (const ExprMgr_ptr self, const Expr_ptr cond, const Expr_ptr t, const Expr_ptr e, const SymbTable_ptr st)
	Builds the If-Then-Else node with given operators.
Expr_ptr	ExprMgr_le (const ExprMgr_ptr self, const Expr_ptr a, const Expr_ptr b, const SymbTable_ptr st)
	Builds the predicate LE (less-then-equal) of given operators.
Expr_ptr	ExprMgr_lt (const ExprMgr_ptr self, const Expr_ptr a, const Expr_ptr b)
	Builds the predicate LT (less-then) of given operators.
Expr_ptr	ExprMgr_minus (const ExprMgr_ptr self, const Expr_ptr a, const Expr_ptr b)
	Builds the scalar node for MINUS of given operators.
Expr_ptr	ExprMgr_minus_one (const ExprMgr_ptr self, const Expr_ptr a)
	Substracts one to a costant number.
Expr_ptr	ExprMgr_mod (const ExprMgr_ptr self, const Expr_ptr a, const Expr_ptr b)
	Builds the scalar node for MODule of given operators.
Expr_ptr	ExprMgr_move_next_to_leaves (const ExprMgr_ptr self, SymbTable_ptr st, Expr_ptr expr)
	Moves the next operator to the tree leafs (i.e. on identifiers).
Expr_ptr	ExprMgr_next (const ExprMgr_ptr self, const Expr_ptr a, const SymbTable_ptr st)
	Constructs a NEXT node of given expression.
Expr_ptr	ExprMgr_not (const ExprMgr_ptr self, const Expr_ptr expr)
	Builds the logical/bitwise NOT of given operator.
Expr_ptr	ExprMgr_notequal (const ExprMgr_ptr self, const Expr_ptr a, const Expr_ptr b, const SymbTable_ptr st)
	Builds the logical NOTEQUAL of given operators.
Expr_ptr	ExprMgr_number (const ExprMgr_ptr self, int value)
	Returns the scalar number expression with the given value.
Expr_ptr	ExprMgr_or (const ExprMgr_ptr self, const Expr_ptr a, const Expr_ptr b)
	Builds the logical/bitwise OR of given operators.
Expr_ptr	ExprMgr_plus (const ExprMgr_ptr self, const Expr_ptr a, const Expr_ptr b)
	Builds the scalar node for PLUS of given operators.
Expr_ptr	ExprMgr_plus_number (const ExprMgr_ptr self, const Expr_ptr a, const Expr_ptr b)
	Sums a NUMBER to a constant number.
Expr_ptr	ExprMgr_plus_one (const ExprMgr_ptr self, const Expr_ptr a)
	Sums one to a costant number.
Expr_ptr	ExprMgr_range (const ExprMgr_ptr self, const Expr_ptr a, const Expr_ptr b)
	Makes a TWODOTS node, representing an integer range.
Expr_ptr	ExprMgr_resolve (const ExprMgr_ptr self, SymbTable_ptr st, int type, Expr_ptr left, Expr_ptr right)
	This is the top-level function that simplifiers can use to simplify expressions. This evaluates constant values in operands left and right with respect to the operation required with parameter type.
Expr_ptr	ExprMgr_setin (const ExprMgr_ptr self, const Expr_ptr a, const Expr_ptr b, const SymbTable_ptr st)
	Makes a setin node, with possible syntactic simplification.
Expr_ptr	ExprMgr_signed_word_to_unsigned (const ExprMgr_ptr self, Expr_ptr w)
	Builds the node for casting signed words to unsigned words.
Expr_ptr	ExprMgr_simplify (const ExprMgr_ptr self, SymbTable_ptr st, Expr_ptr expr)
	Top-level simplifier that evaluates constants and simplifies syntactically the given expression.
Expr_ptr	ExprMgr_simplify_floor (const ExprMgr_ptr self, const SymbTable_ptr symb_table, Expr_ptr body)
	Builds the node for FLOOR.
Expr_ptr	ExprMgr_simplify_gt (const ExprMgr_ptr self, const SymbTable_ptr st, const Expr_ptr a, const Expr_ptr b)
	Builds the predicate GT (greater-then) of given operators.
Expr_ptr	ExprMgr_simplify_iff (const ExprMgr_ptr self, const SymbTable_ptr st, const Expr_ptr a, const Expr_ptr b)
	Builds the logical/bitwise IFF of given operators.
Expr_ptr	ExprMgr_simplify_lt (const ExprMgr_ptr self, const SymbTable_ptr st, const Expr_ptr a, const Expr_ptr b)
	Builds the predicate LT (less-then) of given operators.
Expr_ptr	ExprMgr_simplify_word_bit_select (const ExprMgr_ptr self, const SymbTable_ptr st, const Expr_ptr w, const Expr_ptr r)
	Builds the node for bit selection of words.
Expr_ptr	ExprMgr_simplify_word_extend (const ExprMgr_ptr self, const SymbTable_ptr st, Expr_ptr w, Expr_ptr i)
	Builds the node for extending a word.
Expr_ptr	ExprMgr_simplify_word_resize (const ExprMgr_ptr self, const SymbTable_ptr st, Expr_ptr w, Expr_ptr i)
	Builds the node for resizing a word.
boolean	ExprMgr_time_is_current (const ExprMgr_ptr self, int time)
	Returns true if the time (obtained by Expr_get_time) is current.
boolean	ExprMgr_time_is_dont_care (const ExprMgr_ptr self, int time)
	Returns true if the time (obtained by Expr_get_time) is dont't care.
boolean	ExprMgr_time_is_next (const ExprMgr_ptr self, int time)
	Returns true if the time (obtained by Expr_get_time) is next.
Expr_ptr	ExprMgr_times (const ExprMgr_ptr self, const Expr_ptr a, const Expr_ptr b)
	Builds the scalar node for TIMES of given operators.
Expr_ptr	ExprMgr_true (const ExprMgr_ptr self)
	Returns the true expression value.
Expr_ptr	ExprMgr_unary_minus (const ExprMgr_ptr self, const Expr_ptr a)
	Builds the scalar node for UMINUS (unary minus) of given operators.
Expr_ptr	ExprMgr_union (const ExprMgr_ptr self, const Expr_ptr a, const Expr_ptr b)
	Makes a union node.
Expr_ptr	ExprMgr_unsigned_word_to_signed (const ExprMgr_ptr self, Expr_ptr w)
	Builds the node for casting unsigned words to signed words.
Expr_ptr	ExprMgr_untimed (const ExprMgr_ptr self, SymbTable_ptr st, Expr_ptr expr)
	Returns the untimed version of an expression.
Expr_ptr	ExprMgr_untimed_explicit_time (const ExprMgr_ptr self, SymbTable_ptr st, Expr_ptr expr, int time)
	Returns the untimed version of an expression without searching for the current time.
Expr_ptr	ExprMgr_word1_to_bool (const ExprMgr_ptr self, Expr_ptr w)
	Builds the node for casting word1 to boolean.
Expr_ptr	ExprMgr_word_bit_select (const ExprMgr_ptr self, const Expr_ptr w, const Expr_ptr r)
	Builds the node for bit selection of words.
Expr_ptr	ExprMgr_word_concatenate (const ExprMgr_ptr self, const Expr_ptr a, const Expr_ptr b)
	Builds the node for word concatenation.
Expr_ptr	ExprMgr_word_constant (const ExprMgr_ptr self, const SymbTable_ptr st, int type, Expr_ptr w, Expr_ptr i)
	Builds the node for UWCONST or SWCONST.
Expr_ptr	ExprMgr_word_extend (const ExprMgr_ptr self, Expr_ptr w, Expr_ptr i, const SymbTable_ptr st)
	Builds the node for extending a word.
Expr_ptr	ExprMgr_word_left_rotate (const ExprMgr_ptr self, const Expr_ptr a, const Expr_ptr b)
	Builds the node left rotation of words.
Expr_ptr	ExprMgr_word_left_shift (const ExprMgr_ptr self, const Expr_ptr a, const Expr_ptr b)
	Builds the node left shifting of words.
Expr_ptr	ExprMgr_word_max_value (const ExprMgr_ptr self, const int size, const int type)
	Returns the word number expression corresponding to the max value for the given word size.
Expr_ptr	ExprMgr_word_right_rotate (const ExprMgr_ptr self, const Expr_ptr a, const Expr_ptr b)
	Builds the node right rotation of words.
Expr_ptr	ExprMgr_word_right_shift (const ExprMgr_ptr self, const Expr_ptr a, const Expr_ptr b)
	Builds the node right shifting of words.
Expr_ptr	ExprMgr_wsizeof (const ExprMgr_ptr self, Expr_ptr l, Expr_ptr r)
	Builds the node for WSIZEOF.
Expr_ptr	ExprMgr_xnor (const ExprMgr_ptr self, const Expr_ptr a, const Expr_ptr b)
	Builds the logical/bitwise XNOR of given operators.
Expr_ptr	ExprMgr_xor (const ExprMgr_ptr self, const Expr_ptr a, const Expr_ptr b)
	Builds the logical/bitwise XOR of given operators.

---

Detailed Description

Definition of the public accessor for class ExprMgr.

---

Friends And Related Function Documentation

Expr_ptr ExprMgr_and	(	const ExprMgr_ptr	self,
		const Expr_ptr	a,
		const Expr_ptr	b
	)			[related]

Builds the logical/bitwise AND of given operators.

Performs local syntactic simplification

None

Expr_ptr ExprMgr_and_from_list	(	const ExprMgr_ptr	self,
		node_ptr	list,
		const SymbTable_ptr	st
	)			[related]

Builds the logical/bitwise AND of all elements in the list.

Performs local syntactic simplification. Nil value is considered as true value

TODO[AT] inefficient implementation: loop is better than recursion

None

Expr_ptr ExprMgr_and_nil	(	const ExprMgr_ptr	self,
		const Expr_ptr	a,
		const Expr_ptr	b
	)			[related]

Builds the logical/bitwise AND of given operators, considering Nil as the true value.

Performs local syntactic simplification

None

Expr_ptr ExprMgr_array_const	(	const ExprMgr_ptr	self,
		const Expr_ptr	a,
		const Expr_ptr	v
	)			[related]

Builds the node for CONSTARRAY (array const) of given variable a and value v.

Works with wordarray and intarray.

None

Expr_ptr ExprMgr_array_read	(	const ExprMgr_ptr	self,
		const Expr_ptr	a,
		const Expr_ptr	i
	)			[related]

Builds the node for READ (array read) of given array a and index i.

Works with wordarray and intarray.

None

Expr_ptr ExprMgr_array_write	(	const ExprMgr_ptr	self,
		const Expr_ptr	a,
		const Expr_ptr	i,
		const Expr_ptr	v
	)			[related]

Builds the node for WRITE (array write) of given array a, index i, and value v.

Works with wordarray and intarray.

None

Expr_ptr ExprMgr_attime	(	const ExprMgr_ptr	self,
		Expr_ptr	e,
		int	time,
		const SymbTable_ptr	st
	)			[related]

Creates a ATTIME node.

None

int ExprMgr_attime_get_time	(	const ExprMgr_ptr	self,
		Expr_ptr	e
	)			[related]

Retrieves the time out of an ATTIME node.

None

Expr_ptr ExprMgr_attime_get_untimed	(	const ExprMgr_ptr	self,
		Expr_ptr	e
	)			[related]

Retrieves the untimed node out of an ATTIME node.

None

Expr_ptr ExprMgr_bool_to_word1	(	const ExprMgr_ptr	self,
		Expr_ptr	a
	)			[related]

Builds the node for casting boolean to word1.

Description [Works with booleans. Performs local syntactic simplification]

SideEffects [None]

SeeAlso []

[EXTRACT_DOC_NOTE: * /]

Works with booleans. Performs local syntactic simplification

None

Expr_ptr ExprMgr_boolean_range

(

const ExprMgr_ptr

self

)

[related]

Returns the false:true range value.

None

Expr_ptr ExprMgr_cast_to_unsigned_word	(	const ExprMgr_ptr	self,
		Expr_ptr	width,
		Expr_ptr	arg
	)			[related]

Builds the node for CAST_TO_UNSIGNED_WORD.

Does not perform any simplification

Expr_ptr ExprMgr_cast_toint	(	const ExprMgr_ptr	self,
		Expr_ptr	l,
		Expr_ptr	r
	)			[related]

Builds the node for CAST_TOINT.

Works with scalars. Performs local syntactic simplification.

See also:

Expr_resolve

ExprMgr_ptr ExprMgr_create

(

const NuSMVEnv_ptr

env

)

[related]

The ExprMgr class constructor.

AutomaticStart

The ExprMgr class constructor

See also:

ExprMgr_destroy

void ExprMgr_destroy

(

ExprMgr_ptr

self

)

[related]

The ExprMgr class destructor.

The ExprMgr class destructor

See also:

ExprMgr_create

Expr_ptr ExprMgr_divide	(	const ExprMgr_ptr	self,
		const Expr_ptr	a,
		const Expr_ptr	b
	)			[related]

Builds the scalar node for DIVIDE of given operators.

Works with boolean, scalar and words. Performs local syntactic simplification

None

Expr_ptr ExprMgr_equal	(	const ExprMgr_ptr	self,
		const Expr_ptr	a,
		const Expr_ptr	b,
		const SymbTable_ptr	st
	)			[related]

Builds the logical EQUAL of given operators.

Works with boolean, scalar and words. Performs local syntactic simplification

None

Expr_ptr ExprMgr_false

(

const ExprMgr_ptr

self

)

[related]

Returns the false expression value.

None

Expr_ptr ExprMgr_floor	(	const ExprMgr_ptr	self,
		Expr_ptr	l
	)			[related]

Builds the node for FLOOR.

Works with integers and reals.

See also:

Expr_resolve

Expr_ptr ExprMgr_function	(	const ExprMgr_ptr	self,
		const Expr_ptr	name,
		const Expr_ptr	params
	)			[related]

Builds an Uninterpreted function.

Builds an uninterpreted function named "name" with "params" as parameters. "params" must be a cons list of expressions (Created with find_node)

None

Expr_ptr ExprMgr_ge	(	const ExprMgr_ptr	self,
		const Expr_ptr	a,
		const Expr_ptr	b,
		const SymbTable_ptr	st
	)			[related]

Builds the predicate GE (greater-then-equal) of given operators.

Works with boolean, scalar and words. Performs local syntactic simplification

None

NodeMgr_ptr ExprMgr_get_node_manager

(

const ExprMgr_ptr

self

)

[related]

Returns the internal NodeMgr.

Do not destroy the returned object, it belongs to self.

int ExprMgr_get_time	(	const ExprMgr_ptr	self,
		SymbTable_ptr	st,
		Expr_ptr	expr
	)			[related]

Obtain the base time of an expression.

Current time is recursively calculated as follows:

1. EXPR_UNTIMED_CURRENT for Nil and leaves; 2. UNTIMED_FROZEN if all vars are frozen; 3. Time specified for an ATTIME node, assuming that the inner expression is untimed.

Nesting of ATTIME nodes is _not_ allowed; 4. Minimum time for left and right children assuming

EXPR_UNTIMED_CURRENT < EXPR_UNTIMED_NEXT < t, for any t >= 0.

None

int * ExprMgr_get_time_interval	(	const ExprMgr_ptr	self,
		const SymbTable_ptr	st,
		Expr_ptr	expr
	)			[related]

Obtain the time interval of an expression.

Returns an array of two elements s.t.

• interval[0] = <min>,
• interval[1] = <max>.

Time interval is recursively calculated as follows:

1. EXPR_UNTIMED_CURRENT for Nil and leaves; 2. EXPR_UNTIMED_DONTCARE if all vars are frozen; 3. Time specified for an ATTIME node, assuming that the inner expression is untimed.

Nesting of ATTIME nodes is _not_ allowed; 4. The value <min> is the minimum time between left and right children, the value <max> is the maximum.

For untimed expressions we assume: EXPR_UNTIMED_CURRENT < EXPR_UNTIMED_NEXT

The returned value is allocated and must be freed by the user.

See also:

Expr_get_time

Expr_ptr ExprMgr_gt	(	const ExprMgr_ptr	self,
		const Expr_ptr	a,
		const Expr_ptr	b
	)			[related]

Builds the predicate GT (greater-then) of given operators.

Works with scalar and words. Performs local syntactic simplification

None

Expr_ptr ExprMgr_iff	(	const ExprMgr_ptr	self,
		const Expr_ptr	a,
		const Expr_ptr	b
	)			[related]

Builds the logical/bitwise IFF of given operators.

Performs local syntactic simplification

None

Expr_ptr ExprMgr_implies	(	const ExprMgr_ptr	self,
		const Expr_ptr	a,
		const Expr_ptr	b
	)			[related]

Builds the logical/bitwise IMPLIES of given operators.

Performs local syntactic simplification

None

boolean ExprMgr_is_boolean_range	(	const ExprMgr_ptr	self,
		Expr_ptr	expr
	)			[related]

Checks whether the given expression is the false:true range value.

None

boolean ExprMgr_is_equal_to_zero	(	const ExprMgr_ptr	self,
		const Expr_ptr	input
	)			[related]

Checks if a costant number is zero.

Checks if a costant number is zero

None

boolean ExprMgr_is_false	(	const ExprMgr_ptr	self,
		const Expr_ptr	expr
	)			[related]

Checks whether given value is the false value.

None

boolean ExprMgr_is_ge_to_number	(	const ExprMgr_ptr	self,
		const Expr_ptr	input,
		const Expr_ptr	number
	)			[related]

Compares a NUMBER to a constant number.

Compares a NUMBER to a constant number

boolean ExprMgr_is_number	(	const ExprMgr_ptr	self,
		const Expr_ptr	expr,
		const int	value
	)			[related]

Checks whether given value is the given scalar number.

None

boolean ExprMgr_is_timed	(	const ExprMgr_ptr	self,
		Expr_ptr	expr,
		hash_ptr	cache
	)			[related]

Determines whether a formula has ATTIME nodes in it.

Determines whether a formula has ATTIME nodes in it If cache is not null whenever we encounter a formula in the cache we simply return the previously computed value, otherwise an internal and temporary map is used.

NOTE: the internal representation of cache is private so the user should provide only caches generated by this function!

cache can be updated

boolean ExprMgr_is_true	(	const ExprMgr_ptr	self,
		const Expr_ptr	expr
	)			[related]

Checks whether given value is the true value.

None

Expr_ptr ExprMgr_ite	(	const ExprMgr_ptr	self,
		const Expr_ptr	cond,
		const Expr_ptr	t,
		const Expr_ptr	e,
		const SymbTable_ptr	st
	)			[related]

Builds the If-Then-Else node with given operators.

Performs local syntactic simplification. 'cond' is the case/ite condition, 't' is the THEN expression, 'e' is the ELSE expression

None

Expr_ptr ExprMgr_le	(	const ExprMgr_ptr	self,
		const Expr_ptr	a,
		const Expr_ptr	b,
		const SymbTable_ptr	st
	)			[related]

Builds the predicate LE (less-then-equal) of given operators.

Works with scalar and words. Performs local syntactic simplification

None

Expr_ptr ExprMgr_lt	(	const ExprMgr_ptr	self,
		const Expr_ptr	a,
		const Expr_ptr	b
	)			[related]

Builds the predicate LT (less-then) of given operators.

Works with scalar and words. Performs local syntactic simplification

None

Expr_ptr ExprMgr_minus	(	const ExprMgr_ptr	self,
		const Expr_ptr	a,
		const Expr_ptr	b
	)			[related]

Builds the scalar node for MINUS of given operators.

Works with boolean, scalar and words. Performs local syntactic simplification

None

Expr_ptr ExprMgr_minus_one	(	const ExprMgr_ptr	self,
		const Expr_ptr	a
	)			[related]

Substracts one to a costant number.

Substracts one to a costant number

None

Expr_ptr ExprMgr_mod	(	const ExprMgr_ptr	self,
		const Expr_ptr	a,
		const Expr_ptr	b
	)			[related]

Builds the scalar node for MODule of given operators.

Works with boolean, scalar and words. Performs local syntactic simplification

None

Expr_ptr ExprMgr_move_next_to_leaves	(	const ExprMgr_ptr	self,
		SymbTable_ptr	st,
		Expr_ptr	expr
	)			[related]

Moves the next operator to the tree leafs (i.e. on identifiers).

Moves the next operator to the tree leafs (i.e. on identifiers)

Expr_ptr ExprMgr_next	(	const ExprMgr_ptr	self,
		const Expr_ptr	a,
		const SymbTable_ptr	st
	)			[related]

Constructs a NEXT node of given expression.

None

Expr_ptr ExprMgr_not	(	const ExprMgr_ptr	self,
		const Expr_ptr	expr
	)			[related]

Builds the logical/bitwise NOT of given operator.

Performs local syntactic simplification

None

Expr_ptr ExprMgr_notequal	(	const ExprMgr_ptr	self,
		const Expr_ptr	a,
		const Expr_ptr	b,
		const SymbTable_ptr	st
	)			[related]

Builds the logical NOTEQUAL of given operators.

Works with boolean, scalar and words. Performs local syntactic simplification

None

Expr_ptr ExprMgr_number	(	const ExprMgr_ptr	self,
		int	value
	)			[related]

Returns the scalar number expression with the given value.

Returns the scalar number expression with the given value

None

Expr_ptr ExprMgr_or	(	const ExprMgr_ptr	self,
		const Expr_ptr	a,
		const Expr_ptr	b
	)			[related]

Builds the logical/bitwise OR of given operators.

Performs local syntactic simplification

None

Expr_ptr ExprMgr_plus	(	const ExprMgr_ptr	self,
		const Expr_ptr	a,
		const Expr_ptr	b
	)			[related]

Builds the scalar node for PLUS of given operators.

Works with boolean, scalar and words. Performs local syntactic simplification

None

Expr_ptr ExprMgr_plus_number	(	const ExprMgr_ptr	self,
		const Expr_ptr	a,
		const Expr_ptr	b
	)			[related]

Sums a NUMBER to a constant number.

Calls ExprMgr_plus after having converted b to the proper type (the same of a).

Expr_ptr ExprMgr_plus_one	(	const ExprMgr_ptr	self,
		const Expr_ptr	a
	)			[related]

Sums one to a costant number.

Sums one to a costant number

None

Expr_ptr ExprMgr_range	(	const ExprMgr_ptr	self,
		const Expr_ptr	a,
		const Expr_ptr	b
	)			[related]

Makes a TWODOTS node, representing an integer range.

None

Expr_ptr ExprMgr_resolve	(	const ExprMgr_ptr	self,
		SymbTable_ptr	st,
		int	type,
		Expr_ptr	left,
		Expr_ptr	right
	)			[related]

This is the top-level function that simplifiers can use to simplify expressions. This evaluates constant values in operands left and right with respect to the operation required with parameter type.

Given an expression node E (handled at simplifier-level) the simplifier call this function in post order after having simplified car(E) and cdr(E). It calls it by passing node_get_type(E) as type, and simplified sub expressions for left and right. The function Expr_resolve does not traverses further the structures, it simply combine given operation encoded in type with given already simplified operands left and right.

For example, suppose E is AND(exp1, exp2). The simplifier:

1. Simplifies recursively exp1 to exp1' and exp2 to exp2' (lazyness might be taken into account if exp1 is found to be a false constant).

2. Calls in postorder ExprMgr_resolve(self, AND, exp1', exp2')

ExprMgr_resolve will simplify sintactically the conjunction of (self, exp1', exp2')

None

See also:

Expr_simplify

Expr_ptr ExprMgr_setin	(	const ExprMgr_ptr	self,
		const Expr_ptr	a,
		const Expr_ptr	b,
		const SymbTable_ptr	st
	)			[related]

Makes a setin node, with possible syntactic simplification.

None

Expr_ptr ExprMgr_signed_word_to_unsigned	(	const ExprMgr_ptr	self,
		Expr_ptr	w
	)			[related]

Builds the node for casting signed words to unsigned words.

Description [Works with words. Performs local syntactic simplification]

SideEffects [None]

SeeAlso []

[EXTRACT_DOC_NOTE: * /]

Works with words. Performs local syntactic simplification

None

Expr_ptr ExprMgr_simplify	(	const ExprMgr_ptr	self,
		SymbTable_ptr	st,
		Expr_ptr	expr
	)			[related]

Top-level simplifier that evaluates constants and simplifies syntactically the given expression.

Top-level simplifier that evaluates constants and simplifies syntactically the given expression. Simplification is trivial, no lemma learning nor sintactic implication is carried out at the moment.

WARNING: the results of simplifications are memoized in a hash stored in the symbol table provided. Be very careful not to free/modify the input expression or make sure that the input expressions are find_node-ed. Otherwise, it is very easy to introduce a bug which will be difficult to catch. The hash in the symbol table is reset when any layer is removed.

NOTE FOR DEVELOPERS: if you think that memoization the simplification results may cause some bugs you always can try without global memoization. See the function body below for info.

None

Expr_ptr ExprMgr_simplify_floor	(	const ExprMgr_ptr	self,
		const SymbTable_ptr	symb_table,
		Expr_ptr	body
	)			[related]

Builds the node for FLOOR.

Works with integers and reals. Performs local syntactic simplification.

See also:

Expr_resolve

Expr_ptr ExprMgr_simplify_gt	(	const ExprMgr_ptr	self,
		const SymbTable_ptr	st,
		const Expr_ptr	a,
		const Expr_ptr	b
	)			[related]

Builds the predicate GT (greater-then) of given operators.

Works with boolean, scalar and words. Performs local syntactic simplification

None

Expr_ptr ExprMgr_simplify_iff	(	const ExprMgr_ptr	self,
		const SymbTable_ptr	st,
		const Expr_ptr	a,
		const Expr_ptr	b
	)			[related]

Builds the logical/bitwise IFF of given operators.

Performs local syntactic simplification

None

Expr_ptr ExprMgr_simplify_lt	(	const ExprMgr_ptr	self,
		const SymbTable_ptr	st,
		const Expr_ptr	a,
		const Expr_ptr	b
	)			[related]

Builds the predicate LT (less-then) of given operators.

Works with scalar and words. Performs local syntactic simplification

None

Expr_ptr ExprMgr_simplify_word_bit_select	(	const ExprMgr_ptr	self,
		const SymbTable_ptr	st,
		const Expr_ptr	w,
		const Expr_ptr	r
	)			[related]

Builds the node for bit selection of words.

Description [Works with words. Performs local semantic and syntactic simplification]

SideEffects [None]

SeeAlso []

[EXTRACT_DOC_NOTE: * /]

Works with words. Performs local semantic and syntactic simplification

None

Expr_ptr ExprMgr_simplify_word_extend	(	const ExprMgr_ptr	self,
		const SymbTable_ptr	st,
		Expr_ptr	w,
		Expr_ptr	i
	)			[related]

Builds the node for extending a word.

Works with words. Performs local syntactic simplification

None

Expr_ptr ExprMgr_simplify_word_resize	(	const ExprMgr_ptr	self,
		const SymbTable_ptr	st,
		Expr_ptr	w,
		Expr_ptr	i
	)			[related]

Builds the node for resizing a word.

Works with words. Performs local syntactic simplification

None

boolean ExprMgr_time_is_current	(	const ExprMgr_ptr	self,
		int	time
	)			[related]

Returns true if the time (obtained by Expr_get_time) is current.

Expr_get_time

boolean ExprMgr_time_is_dont_care	(	const ExprMgr_ptr	self,
		int	time
	)			[related]

Returns true if the time (obtained by Expr_get_time) is dont't care.

Expr_get_time

boolean ExprMgr_time_is_next	(	const ExprMgr_ptr	self,
		int	time
	)			[related]

Returns true if the time (obtained by Expr_get_time) is next.

Expr_get_time

Expr_ptr ExprMgr_times	(	const ExprMgr_ptr	self,
		const Expr_ptr	a,
		const Expr_ptr	b
	)			[related]

Builds the scalar node for TIMES of given operators.

Works with boolean, scalar and words. Performs local syntactic simplification

None

Expr_ptr ExprMgr_true

(

const ExprMgr_ptr

self

)

[related]

Returns the true expression value.

None

Expr_ptr ExprMgr_unary_minus	(	const ExprMgr_ptr	self,
		const Expr_ptr	a
	)			[related]

Builds the scalar node for UMINUS (unary minus) of given operators.

Works with scalar and words. Performs local syntactic simplification

None

Expr_ptr ExprMgr_union	(	const ExprMgr_ptr	self,
		const Expr_ptr	a,
		const Expr_ptr	b
	)			[related]

Makes a union node.

[AT] this function may be extremely inefficient If expression is recursively constructed of many UNION, see issue 4483.

None

Expr_ptr ExprMgr_unsigned_word_to_signed	(	const ExprMgr_ptr	self,
		Expr_ptr	w
	)			[related]

Builds the node for casting unsigned words to signed words.

Description [Works with words. Performs local syntactic simplification]

SideEffects [None]

SeeAlso []

[EXTRACT_DOC_NOTE: * /]

Works with words. Performs local syntactic simplification

None

Expr_ptr ExprMgr_untimed	(	const ExprMgr_ptr	self,
		SymbTable_ptr	st,
		Expr_ptr	expr
	)			[related]

Returns the untimed version of an expression.

Expr_get_time

Expr_ptr ExprMgr_untimed_explicit_time	(	const ExprMgr_ptr	self,
		SymbTable_ptr	st,
		Expr_ptr	expr,
		int	time
	)			[related]

Returns the untimed version of an expression without searching for the current time.

Returns the untimed version of an expression using the current time provided as an argument.

Expr_get_time

Expr_ptr ExprMgr_word1_to_bool	(	const ExprMgr_ptr	self,
		Expr_ptr	w
	)			[related]

Builds the node for casting word1 to boolean.

Description [Works with words with width 1. Performs local syntactic simplification]

SideEffects [None]

SeeAlso []

[EXTRACT_DOC_NOTE: * /]

Works with words with width 1. Performs local syntactic simplification

None

Expr_ptr ExprMgr_word_bit_select	(	const ExprMgr_ptr	self,
		const Expr_ptr	w,
		const Expr_ptr	r
	)			[related]

Builds the node for bit selection of words.

Description [Works with words. Performs local syntactic simplification]

SideEffects [None]

SeeAlso []

[EXTRACT_DOC_NOTE: * /]

Works with words. Performs local syntactic simplification

None

Expr_ptr ExprMgr_word_concatenate	(	const ExprMgr_ptr	self,
		const Expr_ptr	a,
		const Expr_ptr	b
	)			[related]

Builds the node for word concatenation.

Description [Works with words. Performs local syntactic simplification]

SideEffects [None]

SeeAlso []

[EXTRACT_DOC_NOTE: * /]

Works with words. Performs local syntactic simplification

None

Expr_ptr ExprMgr_word_constant	(	const ExprMgr_ptr	self,
		const SymbTable_ptr	st,
		int	type,
		Expr_ptr	w,
		Expr_ptr	i
	)			[related]

Builds the node for UWCONST or SWCONST.

Works with words and scalars. Performs local syntactic simplification.

None

See also:

ExprMgr_resolve

Expr_ptr ExprMgr_word_extend	(	const ExprMgr_ptr	self,
		Expr_ptr	w,
		Expr_ptr	i,
		const SymbTable_ptr	st
	)			[related]

Builds the node for extending a word.

Works with words. Performs local syntactic simplification

None

Expr_ptr ExprMgr_word_left_rotate	(	const ExprMgr_ptr	self,
		const Expr_ptr	a,
		const Expr_ptr	b
	)			[related]

Builds the node left rotation of words.

Description [Works with words. Performs local syntactic simplification]

SideEffects [None]

SeeAlso []

[EXTRACT_DOC_NOTE: * /]

Works with words. Performs local syntactic simplification

None

Expr_ptr ExprMgr_word_left_shift	(	const ExprMgr_ptr	self,
		const Expr_ptr	a,
		const Expr_ptr	b
	)			[related]

Builds the node left shifting of words.

Description [Works with words. Performs local syntactic simplification]

SideEffects [None]

SeeAlso []

[EXTRACT_DOC_NOTE: * /]

Works with words. Performs local syntactic simplification

None

Expr_ptr ExprMgr_word_max_value	(	const ExprMgr_ptr	self,
		const int	size,
		const int	type
	)			[related]

Returns the word number expression corresponding to the max value for the given word size.

Returns the word number expression corresponding to the max value for the given word size and word type (signed, unsigned).

None

Expr_ptr ExprMgr_word_right_rotate	(	const ExprMgr_ptr	self,
		const Expr_ptr	a,
		const Expr_ptr	b
	)			[related]

Builds the node right rotation of words.

Description [Works with words. Performs local syntactic simplification]

SideEffects [None]

SeeAlso []

[EXTRACT_DOC_NOTE: * /]

Works with words. Performs local syntactic simplification

None

Expr_ptr ExprMgr_word_right_shift	(	const ExprMgr_ptr	self,
		const Expr_ptr	a,
		const Expr_ptr	b
	)			[related]

Builds the node right shifting of words.

Description [Works with words. Performs local syntactic simplification]

SideEffects [None]

SeeAlso []

[EXTRACT_DOC_NOTE: * /]

Works with words. Performs local syntactic simplification

None

Expr_ptr ExprMgr_wsizeof	(	const ExprMgr_ptr	self,
		Expr_ptr	l,
		Expr_ptr	r
	)			[related]

Builds the node for WSIZEOF.

Works with words. Performs local syntactic simplification.

None

See also:

Expr_resolve

Expr_ptr ExprMgr_xnor	(	const ExprMgr_ptr	self,
		const Expr_ptr	a,
		const Expr_ptr	b
	)			[related]

Builds the logical/bitwise XNOR of given operators.

Performs local syntactic simplification

None

Expr_ptr ExprMgr_xor	(	const ExprMgr_ptr	self,
		const Expr_ptr	a,
		const Expr_ptr	b
	)			[related]

Builds the logical/bitwise XOR of given operators.

Performs local syntactic simplification

None

---

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

• NuSMV/code/nusmv/core/wff/ExprMgr.h