Commit 2e5e349a authored by Philipp Meyer's avatar Philipp Meyer

Compress duplicate and singular state label columns

parent 21f2ff3c
......@@ -192,7 +192,7 @@ int PGArena::computeStateLabels(std::vector<node_id_t>& visited_map, std::vector
std::cout << std::endl;
for (size_t j = 0; j < product_state_size; j++) {
// initially, need to set don't cares to 0
if (initial_product[j] == NODE_NONE) {
if (initial_product[j] == NODE_NONE || initial_product[j] == NODE_NONE_BOTTOM || initial_product[j] == NODE_NONE_TOP) {
initial_product[j] = 0;
}
}
......@@ -235,6 +235,53 @@ int PGArena::computeStateLabels(std::vector<node_id_t>& visited_map, std::vector
}
}
std::cout << "Using " << product_state_size << " components" << std::endl;
// identify singular and duplicate columns
std::vector<bool> used(product_state_size, true);
for (size_t i = 0; i < product_state_size; i++) {
if (visited_states[i].size() == 1) {
std::cout << "Column " << i << " singular" << std::endl;
used[i] = false;
continue;
}
for (size_t j = 0; j < i; j++) {
bool column_equal = true;
for (node_id_t n = 0; n < n_env_nodes; n++) {
if (visited_map[n] != NODE_NONE) {
const node_id_t local_state_i = inner_state_map[i][product_states[n][i]];
const node_id_t local_state_j = inner_state_map[j][product_states[n][j]];
if (local_state_i != local_state_j) {
column_equal = false;
break;
}
}
}
if (column_equal) {
std::cout << "Column " << i << " duplicate of " << j << std::endl;
used[i] = false;
break;
}
}
}
// compress states
size_t k = 0;
for (size_t j = 0; j < product_state_size; j++) {
if (used[j]) {
if (j != k) {
for (node_id_t i = 0; i < n_env_nodes; i++) {
if (visited_map[i] != NODE_NONE) {
product_states[i][k] = product_states[i][j];
}
}
visited_states[k] = std::move(visited_states[j]);
inner_state_map[k] = std::move(inner_state_map[j]);
}
k++;
}
}
product_state_size = k;
accumulated_bits.resize(product_state_size + 1);
// get number of bits
int state_label_bits = 0;
......@@ -247,6 +294,7 @@ int PGArena::computeStateLabels(std::vector<node_id_t>& visited_map, std::vector
}
accumulated_bits[product_state_size] = state_label_bits;
constexpr int node_id_t_bitwidth = std::numeric_limits<node_id_t>::digits + std::numeric_limits<node_id_t>::is_signed;
std::cout << "Using " << product_state_size << " components with a total of " << state_label_bits << " bits" << std::endl;
if (state_label_bits > node_id_t_bitwidth) {
return -1;
}
......@@ -267,6 +315,7 @@ int PGArena::computeStateLabels(std::vector<node_id_t>& visited_map, std::vector
}
}
state_labels[i] = SpecSeq<node_id_t>(id_number, id_dontcare);
std::cout << "State " << i << " gets label " << state_labels[i].toString(state_label_bits) << std::endl;
}
}
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment