Commit 6354e8d7 authored by Philipp Meyer's avatar Philipp Meyer
Browse files

Compress duplicate and singular state label columns

parent 21f2ff3c
Loading
Loading
Loading
Loading
+46 −0
Original line number Diff line number Diff line
@@ -235,6 +235,51 @@ 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[i] != NODE_NONE) {
                    if (product_states[n][i] != product_states[n][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 +292,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;
    }