<commit_before>#include "bdd_mgr.h"

static node_t *
create_node_array (unsigned capacity)
{
    unsigned i;
    node_t *nodes;
    nodes = (node_t *) checked_malloc (capacity * sizeof(node_t));
    for (i = 0; i < capacity; i += 1)
        nodes[i].idx = INT_MAX;
    return nodes;
}

static void
add_false_node (bdd_mgr_t *mgr)
{
    mgr->nodes[0].idx = mgr->num_vars;
    mgr->nodes[0].low = 1;
    mgr->nodes[0].high = 0;
    mgr->num_nodes += 1;
}

static void
add_true_node (bdd_mgr_t *mgr)
{
    mgr->nodes[1].idx = mgr->num_vars;
    mgr->nodes[1].low = 0;
    mgr->nodes[1].high = 1;
    mgr->num_nodes += 1;
}

static bdd_cache_stats_t
make_cache_stats ()
{
    bdd_cache_stats_t res;
    res.num_lookups = 0;
    res.num_hits = 0;
    res.num_inserts = 0;
    res.num_replacements = 0;
    return res;
}

/* Converts the given size hint into the smallest valid size greater
 * than or equal to the hint.  A valid size is a power of two greater
 * than or equal to 128. */
static unsigned
size_hint_to_size (unsigned hint)
{
    unsigned i;
    for (i = 1; i < hint; i *= 2) {}
    return 128u > i ? 128u : i;
}

/* Copies the BDD subgraph with the given root from the old node array
 * into the manager, returning the new index.  This must not be called
 * on a terminal or empty node.
 * 
 * The node corresponding to 'old_root' in the old node array is
 * modified during this copy operation to memoize copying: if the
 * 'low' field of the node denoted by 'old_root' equals 'UINT_MAX',
 * the the 'high' field contains the value of the new index. */
static raw_bdd_t
copy_bdd_rec (bdd_mgr_t *mgr, node_t *old_nodes, raw_bdd_t old_root)
{
    node_t old_root_node;
    assert (!raw_bdd_is_terminal (old_root));
    old_root_node = old_nodes[old_root];
    assert (!node_is_empty (old_root_node));
    if (old_root_node.low == UINT_MAX)
        return old_root_node.high;
    else {
        raw_bdd_t new_low, new_high, new_root;
        new_low = raw_bdd_is_terminal (old_root_node.low)
            ? old_root_node.low
            : copy_bdd_rec (mgr, old_nodes, old_root_node.low);
        new_high = raw_bdd_is_terminal (old_root_node.high)
            ? old_root_node.high
            : copy_bdd_rec (mgr, old_nodes, old_root_node.high);
        assert (new_low != new_high);
        /* FIXME: don't use '_bdd_make_node' here */
        /* It could (but definitely shouldn't) result in recursive
         * resizing, and does more work than necessary. */
        new_root = _bdd_make_node (mgr, old_root_node.idx, new_low, new_high);
        old_nodes[old_root].low = UINT_MAX;
        old_nodes[old_root].high = new_root;
        return new_root;
    }
}

static void
patch_bdd_indirection (
    bdd_mgr_t *mgr,
    bdd_rtu_ht_t *old_raw_bdd_map,
    usr_bdd_ht_t *old_usr_bdd_map,
    raw_bdd_t old_i,
    raw_bdd_t new_i
    )
{
    bdd_t **usr_bdd;
    assert (node_is_live (raw_bdd_to_node (mgr, new_i)));
    usr_bdd = bdd_rtu_ht_lookup (old_raw_bdd_map, old_i);
    if (usr_bdd != NULL) {
        usr_bdd_entry_t new_entry;
        new_entry = *usr_bdd_ht_lookup (old_usr_bdd_map, *usr_bdd);
        new_entry.raw_bdd = new_i;
        usr_bdd_ht_insert (mgr->usr_bdd_map, *usr_bdd, new_entry);
        bdd_rtu_ht_insert (mgr->raw_bdd_map, new_i, *usr_bdd);
    }
}

void
bdd_mgr_resize (bdd_mgr_t *mgr, unsigned new_capacity_hint)
{
    const unsigned old_capacity = mgr->capacity;
    bdd_rtu_ht_t *old_raw_bdd_map;
    usr_bdd_ht_t *old_usr_bdd_map;<commit_msg>A couple more asserts in the usr <-> raw BDD patching code.<commit_after>#include "bdd_mgr.h"

static node_t *
create_node_array (unsigned capacity)
{
    unsigned i;
    node_t *nodes;
    nodes = (node_t *) checked_malloc (capacity * sizeof(node_t));
    for (i = 0; i < capacity; i += 1)
        nodes[i].idx = INT_MAX;
    return nodes;
}

static void
add_false_node (bdd_mgr_t *mgr)
{
    mgr->nodes[0].idx = mgr->num_vars;
    mgr->nodes[0].low = 1;
    mgr->nodes[0].high = 0;
    mgr->num_nodes += 1;
}

static void
add_true_node (bdd_mgr_t *mgr)
{
    mgr->nodes[1].idx = mgr->num_vars;
    mgr->nodes[1].low = 0;
    mgr->nodes[1].high = 1;
    mgr->num_nodes += 1;
}

static bdd_cache_stats_t
make_cache_stats ()
{
    bdd_cache_stats_t res;
    res.num_lookups = 0;
    res.num_hits = 0;
    res.num_inserts = 0;
    res.num_replacements = 0;
    return res;
}

/* Converts the given size hint into the smallest valid size greater
 * than or equal to the hint.  A valid size is a power of two greater
 * than or equal to 128. */
static unsigned
size_hint_to_size (unsigned hint)
{
    unsigned i;
    for (i = 1; i < hint; i *= 2) {}
    return 128u > i ? 128u : i;
}

/* Copies the BDD subgraph with the given root from the old node array
 * into the manager, returning the new index.  This must not be called
 * on a terminal or empty node.
 * 
 * The node corresponding to 'old_root' in the old node array is
 * modified during this copy operation to memoize copying: if the
 * 'low' field of the node denoted by 'old_root' equals 'UINT_MAX',
 * the the 'high' field contains the value of the new index. */
static raw_bdd_t
copy_bdd_rec (bdd_mgr_t *mgr, node_t *old_nodes, raw_bdd_t old_root)
{
    node_t old_root_node;
    assert (!raw_bdd_is_terminal (old_root));
    old_root_node = old_nodes[old_root];
    assert (!node_is_empty (old_root_node));
    if (old_root_node.low == UINT_MAX)
        return old_root_node.high;
    else {
        raw_bdd_t new_low, new_high, new_root;
        new_low = raw_bdd_is_terminal (old_root_node.low)
            ? old_root_node.low
            : copy_bdd_rec (mgr, old_nodes, old_root_node.low);
        new_high = raw_bdd_is_terminal (old_root_node.high)
            ? old_root_node.high
            : copy_bdd_rec (mgr, old_nodes, old_root_node.high);
        assert (new_low != new_high);
        /* FIXME: don't use '_bdd_make_node' here */
        /* It could (but definitely shouldn't) result in recursive
         * resizing, and does more work than necessary. */
        new_root = _bdd_make_node (mgr, old_root_node.idx, new_low, new_high);
        old_nodes[old_root].low = UINT_MAX;
        old_nodes[old_root].high = new_root;
        return new_root;
    }
}

static void
patch_bdd_indirection (
    bdd_mgr_t *mgr,
    bdd_rtu_ht_t *old_raw_bdd_map,
    usr_bdd_ht_t *old_usr_bdd_map,
    raw_bdd_t old_i,
    raw_bdd_t new_i
    )
{
    bdd_t **usr_bdd;
    assert (node_is_live (raw_bdd_to_node (mgr, new_i)));
    usr_bdd = bdd_rtu_ht_lookup (old_raw_bdd_map, old_i);
    if (usr_bdd != NULL) {
        usr_bdd_entry_t new_entry;
        new_entry = *usr_bdd_ht_lookup (old_usr_bdd_map, *usr_bdd);
        new_entry.raw_bdd = new_i;
        assert (usr_bdd_ht_lookup (mgr->usr_bdd_map, *usr_bdd) == NULL);
        assert (bdd_rtu_ht_lookup (mgr->raw_bdd_map, new_i) == NULL);
        usr_bdd_ht_insert (mgr->usr_bdd_map, *usr_bdd, new_entry);
        bdd_rtu_ht_insert (mgr->raw_bdd_map, new_i, *usr_bdd);
    }
}

void
bdd_mgr_resize (bdd_mgr_t *mgr, unsigned new_capacity_hint)
{
    const unsigned old_capacity = mgr->capacity;
    bdd_rtu_ht_t *old_raw_bdd_map;
    usr_bdd_ht_t *old_usr_bdd_map;
{'fraction_non_alphanumeric': 0.10263929618768329, 'fraction_numerical': 0.008099427454266164, 'mean_word_length': 3.1208285385500574, 'pattern_counts': {'":': 0, '<': 8, '<?xml version=': 0, '>': 34, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '2716729', 'n_tokens_mistral': 2844, 'n_tokens_neox': 2809, 'n_words': 675}