#include "nusmv/core/dd/DDMgr.h"#include "nusmv/core/dd/dd.h"#include "nusmv/core/utils/array.h"#include "nusmv/core/utils/WordNumber.h"Go to the source code of this file.
Defines | |
| #define | ADD_ARRAY(x) ((AddArray_ptr) (x)) |
| #define | ADD_ARRAY_CHECK_INSTANCE(x) (nusmv_assert(ADD_ARRAY(x) != ADD_ARRAY(NULL))) |
Typedefs | |
| typedef struct AddArray_TAG * | AddArray_ptr |
Functions | |
| void | AddArray_destroy (DDMgr_ptr dd, AddArray_ptr self) |
| destructor of the class | |
| AddArray_ptr | AddArray_from_add (add_ptr add) |
| given an ADD create an AddArray consisting of one element | |
| AddArray_ptr | AddArray_from_word_number (DDMgr_ptr dd, WordNumber_ptr wn) |
| Creates a new AddArray from given WordNumber. | |
| add_ptr | AddArray_make_conjunction (DDMgr_ptr dd, AddArray_ptr arg) |
| Returns an ADD that is the conjunction of all bits of arg. | |
| add_ptr | AddArray_make_disjunction (DDMgr_ptr dd, AddArray_ptr arg) |
| Returns an ADD that is the disjunction of all bits of arg. | |
| AddArray_ptr | AddArray_word_apply_binary (DDMgr_ptr dd, AddArray_ptr arg1, AddArray_ptr arg2, FP_A_DAA op) |
| Applies binary operator to each bits pair of given arguments, and returns resulting add array. | |
| AddArray_ptr | AddArray_word_apply_unary (DDMgr_ptr dd, AddArray_ptr arg1, FP_A_DA op) |
| Applies unary operator to each bit of given argument, and returns resulting add array. | |
| AddArray_ptr | AddArray_word_bit_selection (DDMgr_ptr dd, AddArray_ptr word, AddArray_ptr range) |
| Performs bit-selection operation on a Word expression represented as arrays of ADD. Every ADD corresponds to a bit of a Word expression. | |
| AddArray_ptr | AddArray_word_concatenation (DDMgr_ptr dd, AddArray_ptr arg1, AddArray_ptr arg2) |
| Performs concatenation operation on two Word expressions represented as arrays of ADD. Every ADD corresponds to a bit of a Word expression. | |
| AddArray_ptr | AddArray_word_equal (DDMgr_ptr dd, AddArray_ptr arg1, AddArray_ptr arg2) |
| Performs equal-operation on two Word expressions represented as arrays of ADD. Every ADD corresponds to a bit of a Word expression. | |
| AddArray_ptr | AddArray_word_ite (DDMgr_ptr dd, AddArray_ptr _if, AddArray_ptr _then, AddArray_ptr _else) |
| Creates a ITE word array: {ITE(_if, _then[N-1], _else[N-1]), ITE(_if, _then[N-2], _else[N-2]), ... ITE(_if, _then[1], _else[1]), ITE(_if, _then[0], _else[0])}. | |
| AddArray_ptr | AddArray_word_left_rotate (DDMgr_ptr dd, AddArray_ptr arg, AddArray_ptr number) |
| Performs left rotate operations on a Word expression represented as an array of ADD. Every ADD corresponds to a bit of a Word expression. | |
| AddArray_ptr | AddArray_word_left_shift (DDMgr_ptr dd, AddArray_ptr arg, AddArray_ptr number) |
| Performs left shift operations on a Word expression represented as an array of ADD. Every ADD corresponds to a bit of a Word expression. | |
| AddArray_ptr | AddArray_word_minus (DDMgr_ptr dd, AddArray_ptr arg1, AddArray_ptr arg2) |
| Perform the subtraction operations on two Word expressions represented as an array of ADD. Every ADD corresponds to a bit of a Word expression. | |
| AddArray_ptr | AddArray_word_not_equal (DDMgr_ptr dd, AddArray_ptr arg1, AddArray_ptr arg2) |
| Performs not-equal-operation on two Word expressions represented as arrays of ADD. Every ADD corresponds to a bit of a Word expression. | |
| AddArray_ptr | AddArray_word_plus (DDMgr_ptr dd, AddArray_ptr arg1, AddArray_ptr arg2) |
| Perform the addition operations on two Word expressions represented as an array of ADD. Every ADD corresponds to a bit of a Word expression. | |
| AddArray_ptr | AddArray_word_right_rotate (DDMgr_ptr dd, AddArray_ptr arg, AddArray_ptr number) |
| Performs right rotate operations on a Word expression represented as an array of ADD. Every ADD corresponds to a bit of a Word expression. | |
| AddArray_ptr | AddArray_word_signed_divide (DDMgr_ptr dd, AddArray_ptr arg1, AddArray_ptr arg2) |
| Perform the division operations on two singed Word expressions represented as an array of ADD. Every ADD corresponds to a bit of a Word expression. | |
| AddArray_ptr | AddArray_word_signed_extend (DDMgr_ptr dd, AddArray_ptr arg, AddArray_ptr repeat) |
| Extends the width of a signed Word expression keeping the value of the expression. | |
| AddArray_ptr | AddArray_word_signed_greater (DDMgr_ptr dd, AddArray_ptr arg1, AddArray_ptr arg2) |
| Performs _signed_ greater-then operation on two Word expressions represented as arrays of ADD. Every ADD corresponds to a bit of a Word expression. | |
| AddArray_ptr | AddArray_word_signed_greater_equal (DDMgr_ptr dd, AddArray_ptr arg1, AddArray_ptr arg2) |
| Performs _signed_ greater-equal-then operation on two Word expressions represented as arrays of ADD. Every ADD corresponds to a bit of a Word expression. | |
| AddArray_ptr | AddArray_word_signed_less (DDMgr_ptr dd, AddArray_ptr arg1, AddArray_ptr arg2) |
| Performs _signed_ less-then operation on two Word expressions represented as arrays of ADD. Every ADD corresponds to a bit of a Word expression. | |
| AddArray_ptr | AddArray_word_signed_less_equal (DDMgr_ptr dd, AddArray_ptr arg1, AddArray_ptr arg2) |
| Performs _signed_ less-equal-then operation on two Word expressions represented as arrays of ADD. Every ADD corresponds to a bit of a Word expression. | |
| AddArray_ptr | AddArray_word_signed_mod (DDMgr_ptr dd, AddArray_ptr arg1, AddArray_ptr arg2) |
| Perform the remainder operations on two signed Word expressions represented as an array of ADD. Every ADD corresponds to a bit of a Word expression. | |
| AddArray_ptr | AddArray_word_signed_resize (DDMgr_ptr dd, AddArray_ptr arg, AddArray_ptr new_size) |
| Performs signed resize operation on a Word expression represented as arrays of ADD. Every ADD corresponds to a bit of a Word expression. | |
| AddArray_ptr | AddArray_word_signed_right_shift (DDMgr_ptr dd, AddArray_ptr arg, AddArray_ptr number) |
| Invokes add_array_word_right_shift with isSigned set to true. | |
| AddArray_ptr | AddArray_word_times (DDMgr_ptr dd, AddArray_ptr arg1, AddArray_ptr arg2) |
| Perform the multiplication operations on two Word expressions represented as an array of ADD. Every ADD corresponds to a bit of a Word expression. | |
| AddArray_ptr | AddArray_word_unary_minus (DDMgr_ptr dd, AddArray_ptr arg) |
| Changes the sign of the given word. | |
| AddArray_ptr | AddArray_word_unsigned_divide (DDMgr_ptr dd, AddArray_ptr arg1, AddArray_ptr arg2) |
| Perform the division operations on two unsigned Word expressions represented as an array of ADD. Every ADD corresponds to a bit of a Word expression. | |
| AddArray_ptr | AddArray_word_unsigned_extend (DDMgr_ptr dd, AddArray_ptr arg, AddArray_ptr repeat) |
| Extends the width of an unsigned Word expression keeping the value of the expression. | |
| AddArray_ptr | AddArray_word_unsigned_greater (DDMgr_ptr dd, AddArray_ptr arg1, AddArray_ptr arg2) |
| Performs greater-then operation on two unsigned Word expressions represented as arrays of ADD. Every ADD corresponds to a bit of a Word expression. | |
| AddArray_ptr | AddArray_word_unsigned_greater_equal (DDMgr_ptr dd, AddArray_ptr arg1, AddArray_ptr arg2) |
| Performs greater-or-equal operation on two unsigned Word expressions represented as arrays of ADD. Every ADD corresponds to a bit of a Word expression. | |
| AddArray_ptr | AddArray_word_unsigned_less (DDMgr_ptr dd, AddArray_ptr arg1, AddArray_ptr arg2) |
| Performs less-then operation on two unsigned Word expressions represented as arrays of ADD. Every ADD corresponds to a bit of a Word expression. | |
| AddArray_ptr | AddArray_word_unsigned_less_equal (DDMgr_ptr dd, AddArray_ptr arg1, AddArray_ptr arg2) |
| Performs less-or-equal operation on two unsigned Word expressions represented as arrays of ADD. Every ADD corresponds to a bit of a Word expression. | |
| AddArray_ptr | AddArray_word_unsigned_mod (DDMgr_ptr dd, AddArray_ptr arg1, AddArray_ptr arg2) |
| Perform the remainder operations on two unsigned Word expressions represented as an array of ADD. Every ADD corresponds to a bit of a Word expression. | |
| AddArray_ptr | AddArray_word_unsigned_resize (DDMgr_ptr dd, AddArray_ptr arg, AddArray_ptr new_size) |
| Performs signed resize operation on a Word expression represented as arrays of ADD. Every ADD corresponds to a bit of a Word expression. | |
| AddArray_ptr | AddArray_word_unsigned_right_shift (DDMgr_ptr dd, AddArray_ptr arg, AddArray_ptr number) |
| Invokes add_array_word_right_shift with isSigned set to false. | |
| #define ADD_ARRAY | ( | x | ) | ((AddArray_ptr) (x)) |
| #define ADD_ARRAY_CHECK_INSTANCE | ( | x | ) | (nusmv_assert(ADD_ARRAY(x) != ADD_ARRAY(NULL))) |
| typedef struct AddArray_TAG* AddArray_ptr |
| void AddArray_destroy | ( | DDMgr_ptr | dd, | |
| AddArray_ptr | self | |||
| ) |
destructor of the class
The memory will be freed and all ADD will be de-referenced
| AddArray_ptr AddArray_from_add | ( | add_ptr | add | ) |
given an ADD create an AddArray consisting of one element
Given ADD must already be referenced.
| AddArray_ptr AddArray_from_word_number | ( | DDMgr_ptr | dd, | |
| WordNumber_ptr | wn | |||
| ) |
Creates a new AddArray from given WordNumber.
Returned add array has the same width as the given word number
| add_ptr AddArray_make_conjunction | ( | DDMgr_ptr | dd, | |
| AddArray_ptr | arg | |||
| ) |
Returns an ADD that is the conjunction of all bits of arg.
Returned ADD is referenced
| add_ptr AddArray_make_disjunction | ( | DDMgr_ptr | dd, | |
| AddArray_ptr | arg | |||
| ) |
Returns an ADD that is the disjunction of all bits of arg.
Returned ADD is referenced
| AddArray_ptr AddArray_word_apply_binary | ( | DDMgr_ptr | dd, | |
| AddArray_ptr | arg1, | |||
| AddArray_ptr | arg2, | |||
| FP_A_DAA | op | |||
| ) |
Applies binary operator to each bits pair of given arguments, and returns resulting add array.
Returned AddArray must be destroyed by the caller
| AddArray_ptr AddArray_word_apply_unary | ( | DDMgr_ptr | dd, | |
| AddArray_ptr | arg1, | |||
| FP_A_DA | op | |||
| ) |
Applies unary operator to each bit of given argument, and returns resulting add array.
Returned AddArray must be destroyed by the caller
| AddArray_ptr AddArray_word_bit_selection | ( | DDMgr_ptr | dd, | |
| AddArray_ptr | word, | |||
| AddArray_ptr | range | |||
| ) |
Performs bit-selection operation on a Word expression represented as arrays of ADD. Every ADD corresponds to a bit of a Word expression.
The high-bit and low-bit of selections are specified by "range". "range" must be ADD leafs with a RANGE node (holding two integer constants, and these constant must be in the range [width-1, 0]). NB: The invoker should destroy the returned array.
| AddArray_ptr AddArray_word_concatenation | ( | DDMgr_ptr | dd, | |
| AddArray_ptr | arg1, | |||
| AddArray_ptr | arg2 | |||
| ) |
Performs concatenation operation on two Word expressions represented as arrays of ADD. Every ADD corresponds to a bit of a Word expression.
NB: The invoker should destroy the returned array.
| AddArray_ptr AddArray_word_equal | ( | DDMgr_ptr | dd, | |
| AddArray_ptr | arg1, | |||
| AddArray_ptr | arg2 | |||
| ) |
Performs equal-operation on two Word expressions represented as arrays of ADD. Every ADD corresponds to a bit of a Word expression.
the size of arguments should be the same The returned array will constain only one (boolean) ADD. NB: The invoker should destroy the returned array.
| AddArray_ptr AddArray_word_ite | ( | DDMgr_ptr | dd, | |
| AddArray_ptr | _if, | |||
| AddArray_ptr | _then, | |||
| AddArray_ptr | _else | |||
| ) |
Creates a ITE word array: {ITE(_if, _then[N-1], _else[N-1]), ITE(_if, _then[N-2], _else[N-2]), ... ITE(_if, _then[1], _else[1]), ITE(_if, _then[0], _else[0])}.
If _else consist of 1 ADD but _then does not then the same _else[0] is used in all ITE. (this is used to pass FAILURE ADD). Otherwise size of _then and _else have to be the same. _if has to be of 1 bit width. Returned array width is as large as _then.
The invoker should destroy the returned array.
| AddArray_ptr AddArray_word_left_rotate | ( | DDMgr_ptr | dd, | |
| AddArray_ptr | arg, | |||
| AddArray_ptr | number | |||
| ) |
Performs left rotate operations on a Word expression represented as an array of ADD. Every ADD corresponds to a bit of a Word expression.
The "number" argument represent the number of bits to rotate. "number" should have only one ADD. NB: The invoker should destroy the returned array.
NB for developers: Every i-th bit of returned array will be: ITE(number=0 , arg[i], ITE(number=1, arg[i-1], ... ITE(number=i, arg[0], ITE(number=i+1, arg[width-1], ... ITE(number=width-1, arg[i+1], ITE(number=width, arg[i], FAILURE
| AddArray_ptr AddArray_word_left_shift | ( | DDMgr_ptr | dd, | |
| AddArray_ptr | arg, | |||
| AddArray_ptr | number | |||
| ) |
Performs left shift operations on a Word expression represented as an array of ADD. Every ADD corresponds to a bit of a Word expression.
The "number" argument represent the number of bits to shift. "number" can be a usual integer (and consist of one ADD) or be an unsigned word (and consist of many ADDs). NB: The invoker should destroy the returned array.
NB for developers: Every i-th bit of returned array will be: ITE(number=0 , arg[i], ITE(number=1, arg[i-1], ... ITE(number=i, arg[0], ITE(number >=0 && number <= width, zero, FAILURE) Does anyone know a better encoding?
| AddArray_ptr AddArray_word_minus | ( | DDMgr_ptr | dd, | |
| AddArray_ptr | arg1, | |||
| AddArray_ptr | arg2 | |||
| ) |
Perform the subtraction operations on two Word expressions represented as an array of ADD. Every ADD corresponds to a bit of a Word expression.
The size of both arguments should be the same.
| AddArray_ptr AddArray_word_not_equal | ( | DDMgr_ptr | dd, | |
| AddArray_ptr | arg1, | |||
| AddArray_ptr | arg2 | |||
| ) |
Performs not-equal-operation on two Word expressions represented as arrays of ADD. Every ADD corresponds to a bit of a Word expression.
the size of arguments should be the same The returned array will constain only one (boolean) ADD. NB: The invoker should destroy the returned array.
| AddArray_ptr AddArray_word_plus | ( | DDMgr_ptr | dd, | |
| AddArray_ptr | arg1, | |||
| AddArray_ptr | arg2 | |||
| ) |
Perform the addition operations on two Word expressions represented as an array of ADD. Every ADD corresponds to a bit of a Word expression.
The size of both arguments should be the same.
| AddArray_ptr AddArray_word_right_rotate | ( | DDMgr_ptr | dd, | |
| AddArray_ptr | arg, | |||
| AddArray_ptr | number | |||
| ) |
Performs right rotate operations on a Word expression represented as an array of ADD. Every ADD corresponds to a bit of a Word expression.
The "number" argument represent the number of bits to rotate. "number" should have only one ADD. NB: The invoker should destroy the returned array.
NB for developers: Every i-th bit of returned array will be: ITE(number=0 , arg[i], ITE(number=1, arg[i+1], ... ITE(number=width-1-i, arg[width-1], ITE(number=width-2-i, arg[0], ... ITE(number=width-1, arg[i-1], ITE(number=width, arg[i], FAILURE
| AddArray_ptr AddArray_word_signed_divide | ( | DDMgr_ptr | dd, | |
| AddArray_ptr | arg1, | |||
| AddArray_ptr | arg2 | |||
| ) |
Perform the division operations on two singed Word expressions represented as an array of ADD. Every ADD corresponds to a bit of a Word expression.
The size of both arguments should be the same.
| AddArray_ptr AddArray_word_signed_extend | ( | DDMgr_ptr | dd, | |
| AddArray_ptr | arg, | |||
| AddArray_ptr | repeat | |||
| ) |
Extends the width of a signed Word expression keeping the value of the expression.
This extension means that the sign (highest) bit is added 'arg_repeat' times on the left. 'arg_repeat' has to be a constant number.
| AddArray_ptr AddArray_word_signed_greater | ( | DDMgr_ptr | dd, | |
| AddArray_ptr | arg1, | |||
| AddArray_ptr | arg2 | |||
| ) |
Performs _signed_ greater-then operation on two Word expressions represented as arrays of ADD. Every ADD corresponds to a bit of a Word expression.
the size of arguments should be the same The returned array will constain only one (boolean) ADD. NB: The invoker should destroy the returned array.
| AddArray_ptr AddArray_word_signed_greater_equal | ( | DDMgr_ptr | dd, | |
| AddArray_ptr | arg1, | |||
| AddArray_ptr | arg2 | |||
| ) |
Performs _signed_ greater-equal-then operation on two Word expressions represented as arrays of ADD. Every ADD corresponds to a bit of a Word expression.
the size of arguments should be the same The returned array will constain only one (boolean) ADD. NB: The invoker should destroy the returned array.
| AddArray_ptr AddArray_word_signed_less | ( | DDMgr_ptr | dd, | |
| AddArray_ptr | arg1, | |||
| AddArray_ptr | arg2 | |||
| ) |
Performs _signed_ less-then operation on two Word expressions represented as arrays of ADD. Every ADD corresponds to a bit of a Word expression.
the size of arguments should be the same The returned array will constain only one (boolean) ADD. NB: The invoker should destroy the returned array.
| AddArray_ptr AddArray_word_signed_less_equal | ( | DDMgr_ptr | dd, | |
| AddArray_ptr | arg1, | |||
| AddArray_ptr | arg2 | |||
| ) |
Performs _signed_ less-equal-then operation on two Word expressions represented as arrays of ADD. Every ADD corresponds to a bit of a Word expression.
the size of arguments should be the same The returned array will constain only one (boolean) ADD. NB: The invoker should destroy the returned array.
| AddArray_ptr AddArray_word_signed_mod | ( | DDMgr_ptr | dd, | |
| AddArray_ptr | arg1, | |||
| AddArray_ptr | arg2 | |||
| ) |
Perform the remainder operations on two signed Word expressions represented as an array of ADD. Every ADD corresponds to a bit of a Word expression.
The size of both arguments should be the same.
| AddArray_ptr AddArray_word_signed_resize | ( | DDMgr_ptr | dd, | |
| AddArray_ptr | arg, | |||
| AddArray_ptr | new_size | |||
| ) |
Performs signed resize operation on a Word expression represented as arrays of ADD. Every ADD corresponds to a bit of a Word expression.
See note 3136 in issue #1787 for full description of signed resize semantics. "new_size" must be ADD leafs with a NUMBER node.NB: The invoker should destroy the returned array.
| AddArray_ptr AddArray_word_signed_right_shift | ( | DDMgr_ptr | dd, | |
| AddArray_ptr | arg, | |||
| AddArray_ptr | number | |||
| ) |
Invokes add_array_word_right_shift with isSigned set to true.
See add_array_word_right_shift.
| AddArray_ptr AddArray_word_times | ( | DDMgr_ptr | dd, | |
| AddArray_ptr | arg1, | |||
| AddArray_ptr | arg2 | |||
| ) |
Perform the multiplication operations on two Word expressions represented as an array of ADD. Every ADD corresponds to a bit of a Word expression.
The size of both arguments should be the same.
| AddArray_ptr AddArray_word_unary_minus | ( | DDMgr_ptr | dd, | |
| AddArray_ptr | arg | |||
| ) |
Changes the sign of the given word.
The return expression is equal to (0 - arg)
| AddArray_ptr AddArray_word_unsigned_divide | ( | DDMgr_ptr | dd, | |
| AddArray_ptr | arg1, | |||
| AddArray_ptr | arg2 | |||
| ) |
Perform the division operations on two unsigned Word expressions represented as an array of ADD. Every ADD corresponds to a bit of a Word expression.
The size of both arguments should be the same.
| AddArray_ptr AddArray_word_unsigned_extend | ( | DDMgr_ptr | dd, | |
| AddArray_ptr | arg, | |||
| AddArray_ptr | repeat | |||
| ) |
Extends the width of an unsigned Word expression keeping the value of the expression.
This extension means that the zero bit is added 'arg_repeat' times on the left. 'arg_repeat' has to be a constant number.
| AddArray_ptr AddArray_word_unsigned_greater | ( | DDMgr_ptr | dd, | |
| AddArray_ptr | arg1, | |||
| AddArray_ptr | arg2 | |||
| ) |
Performs greater-then operation on two unsigned Word expressions represented as arrays of ADD. Every ADD corresponds to a bit of a Word expression.
the size of arguments should be the same The returned array will constain only one (boolean) ADD. NB: The invoker should destroy the returned array.
| AddArray_ptr AddArray_word_unsigned_greater_equal | ( | DDMgr_ptr | dd, | |
| AddArray_ptr | arg1, | |||
| AddArray_ptr | arg2 | |||
| ) |
Performs greater-or-equal operation on two unsigned Word expressions represented as arrays of ADD. Every ADD corresponds to a bit of a Word expression.
the size of arguments should be the same The returned array will constain only one (boolean) ADD. NB: The invoker should destroy the returned array.
| AddArray_ptr AddArray_word_unsigned_less | ( | DDMgr_ptr | dd, | |
| AddArray_ptr | arg1, | |||
| AddArray_ptr | arg2 | |||
| ) |
Performs less-then operation on two unsigned Word expressions represented as arrays of ADD. Every ADD corresponds to a bit of a Word expression.
the size of arguments should be the same The returned array will constain only one (boolean) ADD. NB: The invoker should destroy the returned array.
| AddArray_ptr AddArray_word_unsigned_less_equal | ( | DDMgr_ptr | dd, | |
| AddArray_ptr | arg1, | |||
| AddArray_ptr | arg2 | |||
| ) |
Performs less-or-equal operation on two unsigned Word expressions represented as arrays of ADD. Every ADD corresponds to a bit of a Word expression.
the size of arguments should be the same The returned array will constain only one (boolean) ADD. NB: The invoker should destroy the returned array.
| AddArray_ptr AddArray_word_unsigned_mod | ( | DDMgr_ptr | dd, | |
| AddArray_ptr | arg1, | |||
| AddArray_ptr | arg2 | |||
| ) |
Perform the remainder operations on two unsigned Word expressions represented as an array of ADD. Every ADD corresponds to a bit of a Word expression.
The size of both arguments should be the same.
| AddArray_ptr AddArray_word_unsigned_resize | ( | DDMgr_ptr | dd, | |
| AddArray_ptr | arg, | |||
| AddArray_ptr | new_size | |||
| ) |
Performs signed resize operation on a Word expression represented as arrays of ADD. Every ADD corresponds to a bit of a Word expression.
See note 3136 in issue #1787 for full description of signed resize semantics. "new_size" must be ADD leafs with a NUMBER node.NB: The invoker should destroy the returned array.
| AddArray_ptr AddArray_word_unsigned_right_shift | ( | DDMgr_ptr | dd, | |
| AddArray_ptr | arg, | |||
| AddArray_ptr | number | |||
| ) |
Invokes add_array_word_right_shift with isSigned set to false.
See add_array_word_right_shift.
1.6.1