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

Last updated on 2009/03/04 12h:51