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