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 
)
Returned add array has the same width as the given word number

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

array_t* 
AddArray_get_array(
  AddArray_ptr  self 
)
Do not change the returned array, which belongs to self

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_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_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" 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

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_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_signed_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_signed_extend(
  DdManager* dd, 
  AddArray_ptr  arg, 
  AddArray_ptr  arg_repeat 
)
This extension means that the sign (highest) bit is added 'arg_repeat' times on the left. 'arg_repeat' has to be a constant number.

See Also AddArray_word_extend
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_signed_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_signed_resize(
  DdManager* dd, 
  AddArray_ptr  word, 
  AddArray_ptr  new_size 
)
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.

See Also AddArray_word_unsigned_resize
Defined in AddArray.c

AddArray_ptr 
AddArray_word_signed_right_shift(
  DdManager* dd, 
  AddArray_ptr  arg, 
  AddArray_ptr  number 
)
See add_array_word_right_shift.

See Also add_array_word_right_shift
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_unary_minus(
  DdManager* dd, 
  AddArray_ptr  arg 
)
The return expression is equal to (0 - arg)

Defined in AddArray.c

AddArray_ptr 
AddArray_word_unsigned_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_unsigned_extend(
  DdManager* dd, 
  AddArray_ptr  arg, 
  AddArray_ptr  arg_repeat 
)
This extension means that the zero bit is added 'arg_repeat' times on the left. 'arg_repeat' has to be a constant number.

See Also AddArray_word_signed_extend
Defined in AddArray.c

AddArray_ptr 
AddArray_word_unsigned_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_unsigned_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_unsigned_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_unsigned_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_unsigned_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_unsigned_resize(
  DdManager* dd, 
  AddArray_ptr  word, 
  AddArray_ptr  new_size 
)
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.

See Also AddArray_word_signed_resize
Defined in AddArray.c

AddArray_ptr 
AddArray_word_unsigned_right_shift(
  DdManager* dd, 
  AddArray_ptr  arg, 
  AddArray_ptr  number 
)
See add_array_word_right_shift.

See Also add_array_word_right_shift
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

OrdGroups_ptr 
OrdGroups_copy(
  const OrdGroups_ptr  self 
)
Returned instance is a copy of self

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 add_ptr 
add_array_create_default_value_of_shift_operation(
  DdManager* dd, 
  AddArray_ptr  number, 
  int  width, 
  add_ptr  defaultBit, 
  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. 'defaultBit' is a bit which pads the shifted bit. '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_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 inline boolean 
add_array_is_word(
  DdManager* dd, 
  const AddArray_ptr  number 
)
Checks whether the given AddArray is a word or not.

Defined in AddArray.c

static AddArray_ptr 
add_array_negate_bits(
  DdManager* dd, 
  AddArray_ptr  arg 
)
the result of the functions is a new array [!arg[0

Defined in AddArray.c

static void 
add_array_signed_division_remainder_hardware(
  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. NOTE FOR DEVELOPER: the provided functionality was implemented in two forms: as function add_array_signed_division_remainder_simple (which is the simplest) and as function add_array_signed_division_remainder_harware (which resembles the hardware implemenation of signed division). Preliminary benchmarking showed that add_array_signed_division_remainder_harware runs quicker (so it is used now). Proper benchmarks are still needed to choose one and remove the other one.

See Also add_array_signed_division_remainder_simple
Defined in AddArray.c

static void 
add_array_signed_division_remainder_simple(
  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. NOTE FOR DEVELOPER: the provided functionality was implemented in two forms: as function add_array_signed_division_remainder_simple (which is the simplest) and as function add_array_signed_division_remainder_harware (which resembles the hardware implemenation of signed division). Preliminary benchmarking showed that add_array_signed_division_remainder_harware runs quicker (so it is used now). Proper benchmarks are still needed to choose one and remove the other one.

See Also add_array_unsigned_division_remainder add_array_signed_division_remainder_harware
Defined in AddArray.c

static void 
add_array_unsigned_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.

See Also add_array_signed_division_remainder
Defined in AddArray.c

static AddArray_ptr 
add_array_word_extend(
  DdManager* dd, 
  AddArray_ptr  arg, 
  AddArray_ptr  arg_repeat, 
  add_ptr  paddingBit 
)
This extension means that a padding bit (paddingBit) is added 'arg_repeat' times on the left. 'arg_repeat' has to be a constant number.

See Also AddArray_word_signed_extend AddArray_word_unsigned_extend
Defined in AddArray.c

AddArray_ptr 
add_array_word_plus_negated_and_one(
  DdManager* dd, 
  AddArray_ptr  arg1, 
  AddArray_ptr  arg2, 
  add_ptr* carry 
)
The size of both arguments should be the same. 'carry' must be not zero and is used to return carry bit of performed operation. Note the overflow or underflow can be detected by checking (not carry-bit).

Defined in AddArray.c

AddArray_ptr 
add_array_word_right_shift(
  DdManager* dd, 
  AddArray_ptr  arg, 
  AddArray_ptr  number, 
  boolean  isSigned 
)
The "number" argument represent the number of bits to shift. "number" should have only one ADD. "isSigned" is a flag that the word is signed or unsigned. NB: The invoker should destroy the returned array. Every i-th bit of returned array will be: ITE(number=0 , arg[i

Defined in AddArray.c

static AddArray_ptr 
add_array_word_signed_comparison(
  DdManager* dd, 
  APFDAA  op, 
  AddArray_ptr  arg1, 
  AddArray_ptr  arg2 
)
op can be: any signed relational functions such as AddArray_word_less, AddArray_word_less_equal, etc

See Also AddArray_word_signed_less AddArray_word_signed_less_equal AddArray_word_signed_greater AddArray_word_signed_greater_equal
Defined in AddArray.c

OrdGroups_ptr 
enc_utils_create_vars_ord_groups(
  BoolEnc_ptr  bool_enc, 
  NodeList_ptr  vars 
)
The returned instance belongs to the caller. It is a caller's responsability to destroy it.

Defined in utils.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_copy(
  const OrdGroups_ptr  self, 
  OrdGroups_ptr  other 
)
Private class copier

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 2012/11/18 14h:16