Reduce array allocation in if-then-else-patterns
In the Btor2 benchmark set, almost all write
operations appear in the following pattern:
id1 state sid1
id2 write sid1 id1 index_id element_id
cond_id redor sid2 nid
id3 ite sid1 cond_id id2 id1
The ite
operation (id3
) takes the array with the nid id1
and a modified version of id1
that has been overwritten at index_id
(id2
). The ite operation returns the modified version if the condition cond_id
is true, or the original version if it is false.
Because both arrays are arguments of the same operation, the algorithm implemented for #17 (closed) in !7 (merged) needs a copy for the write operation to preserve the topological order.
Currently, Btor2C translates these patterns as
SORT_2 new_arr;
for(i = 0; i < len(old_arr); ++i){
new_arr[i] = old_arr[i];
}
new_arr[arg_1] = value;
final_arr = cond ? new_arr : old_arr;
In order to avoid having to create a new copy, one could implement the following workaround:
SORT_2* final_arr = old_arr;
final_arr[arg_1] = cond ? old_arr[arg_1] : value;
This workaround avoids allocating a new array and writes into the already existing one, depending on whether the given condition is true or false.
This translation method is only valid if the topological order is preserved, which means that the old or new (write
) array cannot be accessed after the ite
operation.