AddArray_ptr
AddArray_create(
int number
)
- number must be positive. The index of the
array goes from 0 to (number - 1).
- Defined in
AddArray.c
void
AddArray_destroy(
DdManager* dd,
AddArray_ptr self
)
- The memory will be freed and all ADD will be
de-referenced
- Defined in
AddArray.c
AddArray_ptr
AddArray_duplicate(
AddArray_ptr self
)
- During duplication all ADD will be referenced.
- Defined in
AddArray.c
AddArray_ptr
AddArray_from_add(
add_ptr add
)
- Given ADD must already be referenced.
- Defined in
AddArray.c
AddArray_ptr
AddArray_from_word_number(
DdManager* dd,
WordNumber_ptr wn
)
- If monolithic word encoding is disabled, returned add
array has the same width of the given word number; otherwise size
will be 1
- Defined in
AddArray.c
size_t
AddArray_get_add_size(
const AddArray_ptr self,
DdManager* dd
)
- Returns the sum of the sizes of the ADDs within self
- Defined in
AddArray.c
add_ptr
AddArray_get_add(
AddArray_ptr self
)
- The array should contain exactly one element
- Defined in
AddArray.c
add_ptr
AddArray_get_n(
AddArray_ptr self,
int number
)
- "n" can be from 0 to (size-1).
The returned ADD is NOT referenced.
- Defined in
AddArray.c
int
AddArray_get_size(
AddArray_ptr self
)
- returns the size (number of elements) of the array
- Defined in
AddArray.c
add_ptr
AddArray_make_conjunction(
DdManager* dd,
AddArray_ptr arg
)
- Returned ADD is referenced
- Defined in
AddArray.c
add_ptr
AddArray_make_disjunction(
DdManager* dd,
AddArray_ptr arg
)
- Returned ADD is referenced
- Defined in
AddArray.c
void
AddArray_set_n(
AddArray_ptr self,
int number,
add_ptr add
)
- The given ADD "add" must already be referenced.
The previous value should already be de-referenced if it is necessary.
- Defined in
AddArray.c
AddArray_ptr
AddArray_word_apply_binary(
DdManager* dd,
AddArray_ptr arg1,
AddArray_ptr arg2,
FP_A_DAA op
)
- Returned AddArray must be destroyed by the caller
- Defined in
AddArray.c
AddArray_ptr
AddArray_word_apply_unary(
DdManager* dd,
AddArray_ptr arg1,
FP_A_DA op
)
- Returned AddArray must be destroyed by the caller
- Defined in
AddArray.c
AddArray_ptr
AddArray_word_bit_selection(
DdManager* dd,
AddArray_ptr word,
AddArray_ptr range
)
- 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
- Defined in
AddArray.c
AddArray_ptr
AddArray_word_concatenation(
DdManager* dd,
AddArray_ptr arg1,
AddArray_ptr arg2
)
- NB: The invoker should destroy the returned array.
- Defined in
AddArray.c
AddArray_ptr
AddArray_word_divide(
DdManager* dd,
AddArray_ptr arg1,
AddArray_ptr arg2
)
- The size of both arguments should be the same.
- Defined in
AddArray.c
AddArray_ptr
AddArray_word_equal(
DdManager* dd,
AddArray_ptr arg1,
AddArray_ptr arg2
)
- 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.
- Defined in
AddArray.c
AddArray_ptr
AddArray_word_greater_equal(
DdManager* dd,
AddArray_ptr arg1,
AddArray_ptr arg2
)
- 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.
- Defined in
AddArray.c
AddArray_ptr
AddArray_word_greater(
DdManager* dd,
AddArray_ptr arg1,
AddArray_ptr arg2
)
- 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.
- Defined in
AddArray.c
AddArray_ptr
AddArray_word_ite(
DdManager* dd,
AddArray_ptr _if,
AddArray_ptr _then,
AddArray_ptr _else
)
- The invoker should destroy the returned array.
- Defined in
AddArray.c
AddArray_ptr
AddArray_word_left_rotate(
DdManager* dd,
AddArray_ptr arg,
AddArray_ptr number
)
- 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
- Defined in
AddArray.c
AddArray_ptr
AddArray_word_left_shift(
DdManager* dd,
AddArray_ptr arg,
AddArray_ptr number
)
- The "number" argument represent
the number of bits to shift. "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
- Defined in
AddArray.c
AddArray_ptr
AddArray_word_less_equal(
DdManager* dd,
AddArray_ptr arg1,
AddArray_ptr arg2
)
- 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.
- Defined in
AddArray.c
AddArray_ptr
AddArray_word_less(
DdManager* dd,
AddArray_ptr arg1,
AddArray_ptr arg2
)
- 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.
- Defined in
AddArray.c
AddArray_ptr
AddArray_word_minus(
DdManager* dd,
AddArray_ptr arg1,
AddArray_ptr arg2
)
- The size of both arguments should be the same.
- Defined in
AddArray.c
AddArray_ptr
AddArray_word_mod(
DdManager* dd,
AddArray_ptr arg1,
AddArray_ptr arg2
)
- The size of both arguments should be the same.
- Defined in
AddArray.c
AddArray_ptr
AddArray_word_not_equal(
DdManager* dd,
AddArray_ptr arg1,
AddArray_ptr arg2
)
- 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.
- Defined in
AddArray.c
AddArray_ptr
AddArray_word_plus(
DdManager* dd,
AddArray_ptr arg1,
AddArray_ptr arg2
)
- The size of both arguments should be the same.
- Defined in
AddArray.c
AddArray_ptr
AddArray_word_right_rotate(
DdManager* dd,
AddArray_ptr arg,
AddArray_ptr number
)
- 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
- Defined in
AddArray.c
AddArray_ptr
AddArray_word_right_shift(
DdManager* dd,
AddArray_ptr arg,
AddArray_ptr number
)
- The "number" argument represent
the number of bits to shift. "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
- Defined in
AddArray.c
AddArray_ptr
AddArray_word_sign_extend(
DdManager* dd,
AddArray_ptr arg,
AddArray_ptr arg_repeat
)
- arg_repeat must be a constant number
- Defined in
AddArray.c
AddArray_ptr
AddArray_word_signed_greater_equal(
DdManager* dd,
AddArray_ptr arg1,
AddArray_ptr arg2
)
- 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.
- Defined in
AddArray.c
AddArray_ptr
AddArray_word_signed_greater(
DdManager* dd,
AddArray_ptr arg1,
AddArray_ptr arg2
)
- 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.
- Defined in
AddArray.c
AddArray_ptr
AddArray_word_signed_less_equal(
DdManager* dd,
AddArray_ptr arg1,
AddArray_ptr arg2
)
- 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.
- Defined in
AddArray.c
AddArray_ptr
AddArray_word_signed_less(
DdManager* dd,
AddArray_ptr arg1,
AddArray_ptr arg2
)
- 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.
- Defined in
AddArray.c
AddArray_ptr
AddArray_word_times(
DdManager* dd,
AddArray_ptr arg1,
AddArray_ptr arg2
)
- The size of both arguments should be the same.
- Defined in
AddArray.c
AddArray_ptr
AddArray_word_uminus(
DdManager* dd,
AddArray_ptr arg
)
- Changes the sign of the given word.
- Defined in
AddArray.c
void
OrdGroups_add_variables(
OrdGroups_ptr self,
NodeList_ptr vars,
int group
)
- The addition of each variable is performed only if the
variable has not been already added to the same group. If the
variable has been already added but to a different group, an error
occurs. The group must be already existing.
- Defined in
OrdGroups.c
void
OrdGroups_add_variable(
OrdGroups_ptr self,
node_ptr name,
int group
)
- The addition is performed only if the variable has not
been already added to the same group. If the variable has been
already added but to a different group, an error occurs. The group
must be already existing.
- Defined in
OrdGroups.c
int
OrdGroups_create_group(
OrdGroups_ptr self
)
- Creates a new group, and returns the group ID for
future reference
- Defined in
OrdGroups.c
OrdGroups_ptr
OrdGroups_create(
)
- Class constructor
- Defined in
OrdGroups.c
void
OrdGroups_destroy(
OrdGroups_ptr self
)
- Class destructor
- Defined in
OrdGroups.c
int
OrdGroups_get_size(
const OrdGroups_ptr self
)
- Returns the number of available groups
- Defined in
OrdGroups.c
int
OrdGroups_get_var_group(
const OrdGroups_ptr self,
node_ptr name
)
- -1 is returned if the variable does not belong to any
group.
- Defined in
OrdGroups.c
NodeList_ptr
OrdGroups_get_vars_in_group(
const OrdGroups_ptr self,
int group
)
- Returned list instance still belongs to self.
- Defined in
OrdGroups.c
static void
add_array_adder(
DdManager* dd,
AddArray_ptr arg1,
AddArray_ptr arg2,
add_ptr carry_in,
AddArray_ptr* res,
add_ptr* carry_out
)
- The sum is returned by the parameter res (the invoker
must destroy this array), and the final carry-bit is returned by the
parameter carry_out (the ADD is referenced).
The size of input arrays must be equal(and positive).
- Defined in
AddArray.c
static AddArray_ptr
add_array_apply_on_bits(
DdManager* dd,
,
AddArray_ptr arg
)
- the result of the functions is a new array
[add_monadic_apply(op, arg[0
- Defined in
AddArray.c
static add_ptr
add_array_create_default_value_of_shift_operation(
DdManager* dd,
AddArray_ptr number,
int width,
const char* errMessage
)
- This function is used in shift operations.
See, for example, AddArray_word_left_shift.
The 'number' is ADD of the number of bit the Word is shifted.
'width' is the width of the given Word expression.
'errMessage' is the error message to print if number is out of range,
for example, "Right operand of left-shift is out of range".
NB: The returned ADD is referenced.
- Defined in
AddArray.c
static void
add_array_division_remainder(
DdManager* dd,
AddArray_ptr arg1,
AddArray_ptr arg2,
AddArray_ptr* quotient,
AddArray_ptr* remainder
)
- The quotient and the remainder is returned in the
parameters "quotient" and "remainder" respectively.
The invoker should free the returned arrays.
The size of arguments should be the same (and positive).
Every bit of the resulting arrays is wrapped in ITE which check
the second argument (of the operation) for not being zero.
- Defined in
AddArray.c
static void
add_array_full_adder(
DdManager* dd,
add_ptr arg1,
add_ptr arg2,
add_ptr carry_in,
add_ptr* sum,
add_ptr* carry_out
)
- The returned ADD (sum and carry_out) are referenced.
- Defined in
AddArray.c
static AddArray_ptr
add_array_word_signed_operator(
DdManager* dd,
APFDAA op,
AddArray_ptr arg1,
AddArray_ptr arg2
)
- op can be: AddArray_word_less or AddArray_word_less_equal
- See Also
AddArray_word_signed_less
AddArray_word_signed_less_equal
- Defined in
AddArray.c
OrdGroups_ptr
enc_utils_parse_ordering_file(
const char* order_filename,
const BoolEnc_ptr bool_enc
)
- The returned instance belongs to the caller. It is a
caller's responsability to destroy it. order_filename can be NULL
- Defined in
utils.c
static int
ord_groups_allocate_new_group(
OrdGroups_ptr self
)
- Extends the array of groups if needed. Extension is
performed with a grow factor.
- Defined in
OrdGroups.c
static void
ord_groups_associate_name_to_group(
OrdGroups_ptr self,
node_ptr name,
int group
)
- Use this method to access to the hash name_to_group,
as values are stored in a tricky way.
- Defined in
OrdGroups.c
static void
ord_groups_deinit(
OrdGroups_ptr self
)
- Private deinitializer
- Defined in
OrdGroups.c
static void
ord_groups_init(
OrdGroups_ptr self
)
- Private class initializer
- Defined in
OrdGroups.c
static int
ord_groups_name_to_group(
OrdGroups_ptr self,
node_ptr name
)
- use this method to access the hash table name_to_group,
as the way goups are stored within it is very tricky.
- Defined in
OrdGroups.c
(
)
- The type AddArray_ptr is used just to hide
array_t (to enable type-checking by compilers).
But the actuall data-structure used is array_t.
- Defined in
AddArray.c
(
)
- See array2AddArray
- Defined in
AddArray.c