is pointing to. - * TODO (?) return special node for when p == AADD_TERMINAL - */ -static inline aaddnode_t -AADD_GETNODE(AADD_TARG p) -{ - return (aaddnode_t) llmsset_index_to_ptr(nodes, p); -} - -/** - * Packs a AADD_TARG and AADD_WGT into a single 64 bit AADD. - */ -static inline AADD -aadd_bundle(AADD_TARG p, AADD_WGT a) -{ - if (larger_wgt_indices) { - assert (p <= 0x000000003ffffffe); // avoid clash with sylvan_invalid - assert (a <= (1LL<<33)); - return (a << 30 | p); - }else { - assert (p <= 0x000000fffffffffe); // avoid clash with sylvan_invalid - assert (a <= (1<<23)); - return (a << 40 | p); - } -} - -static void __attribute__((unused)) -aaddnode_unpack(aaddnode_t n, AADD_TARG *low, AADD_TARG *high, AADD_WGT *a, AADD_WGT *b) -{ - *low = aaddnode_getptrlow(n); - *high = aaddnode_getptrhigh(n); - bool norm_pos = (n->low & aadd_wgt_pos_mask) >> 54; - bool norm_val = (n->low & aadd_wgt_val_mask) >> 53; - - if (weight_norm_strat == NORM_L2) { - *b = AADD_WEIGHT(n->high); - *a = wgt_get_low_L2normed(*b); - } - else { - if (norm_pos == 0) { // low WGT is AADD_ZERO or AADD_ONE, high WGT in table - *a = (norm_val == 0) ? AADD_ZERO : AADD_ONE; - *b = AADD_WEIGHT(n->high); - } - else { // high WGT is AADD_ZERO or AADD_ONE, low WGT in table - *b = (norm_val == 0) ? AADD_ZERO : AADD_ONE; - *a = AADD_WEIGHT(n->high); - } - } -} - -static void __attribute__((unused)) -aaddnode_getchilderen(aaddnode_t n, AADD *low, AADD *high) -{ - AADD_TARG l, h; - AADD_WGT a, b; - aaddnode_unpack(n, &l, &h, &a, &b); - *low = aadd_bundle(l, a); - *high = aadd_bundle(h, b); -} - -static void __attribute__((unused)) -aaddnode_pack(aaddnode_t n, BDDVAR var, AADD_TARG low, AADD_TARG high, AADD_WGT a, AADD_WGT b) -{ - // We only want to store 1 edge weight per node (which has 2 outgoing - // edges). For NORM_LOW and NORM_MAX this is relatively easy because in - // both those cases there is at least one edge weight equal to 1 or 0. - // - // For NORM_L2 it is a bit more complicated: both edge weights can be - // outside of {0, 1}, but under the constraint that |low|^2 + |high|^2 = 1, - // (or both are 0) and that |low| \in R+, we only need to store high, and - // can derive low. - - // these will be set depending on the normalization strategy - // (retrieval of edge weights is also dependent on normalization strategy) - AADD_WGT wgt_high; - bool norm_pos; - bool norm_val; - - if (weight_norm_strat == NORM_L2) { - assert(!(a == AADD_ZERO && b == AADD_ZERO)); // redundant node (caught before) - norm_pos = 0; - norm_val = 0; - wgt_high = b; // we can derive a from b - } - else { - /// weight_norm_strat == NORM_LOW or NORM_MAX or NORM_MIN - assert(a == AADD_ZERO || a == AADD_ONE || b == AADD_ZERO || b == AADD_ONE); - norm_pos = (a == AADD_ZERO || a == AADD_ONE) ? 0 : 1; - if (norm_pos == 0) { - norm_val = (a == AADD_ZERO) ? 0 : 1; - wgt_high = b; - } - else { - norm_val = (b == AADD_ZERO) ? 0 : 1; - wgt_high = a; - } - } - - // organize the bit structure of low and high - n->low = ((uint64_t)var)<<55 | ((uint64_t)norm_pos)<<54 | ((uint64_t)norm_val)<<53 | low; - if (larger_wgt_indices) { - n->high = wgt_high<<30 | high; - } - else { - n->high = wgt_high<<40 | high; - } -} - -static AADD_TARG __attribute__((unused)) -_aadd_makenode(BDDVAR var, AADD_TARG low, AADD_TARG high, AADD_WGT a, AADD_WGT b) -{ - struct aaddnode n; - - aaddnode_pack(&n, var, low, high, a, b); - - AADD_TARG result; - int created; - AADD_TARG index = llmsset_lookup(nodes, n.low, n.high, &created); - if (index == 0) { - //printf("auto gc of node table triggered\n"); - - aadd_refs_push(low); - aadd_refs_push(high); - sylvan_gc(); - aadd_refs_pop(2); - - index = llmsset_lookup(nodes, n.low, n.high, &created); - if (index == 0) { - fprintf(stderr, "AADD/BDD Unique table full, %zu of %zu buckets filled!\n", llmsset_count_marked(nodes), llmsset_get_size(nodes)); - exit(1); - } - } - - if (created) sylvan_stats_count(AADD_NODES_CREATED); - else sylvan_stats_count(AADD_NODES_REUSED); - - result = index; - //return mark ? result | aadd_marked_mask : result; - return result; -} - -static AADD __attribute__((unused)) -aadd_makenode(BDDVAR var, AADD low, AADD high) -{ - AADD_TARG low_trg = AADD_TARGET(low); - AADD_WGT low_wgt = AADD_WEIGHT(low); - AADD_TARG high_trg = AADD_TARGET(high); - AADD_WGT high_wgt = AADD_WEIGHT(high); - - // Edges with weight 0 should point straight to terminal. - if (low_wgt == AADD_ZERO) low_trg = AADD_TERMINAL; - if (high_wgt == AADD_ZERO) high_trg = AADD_TERMINAL; - - // If both low and high are the same (both TARG and WGT) return low - if (low == high) return low; - else { - // If the edges are not the same - AADD_WGT norm = (*normalize_weights)(&low_wgt, &high_wgt); - AADD_TARG res = _aadd_makenode(var, low_trg, high_trg, low_wgt, high_wgt); - return aadd_bundle(res, norm); - } -} - -/****************
is pointing to. + * TODO (?) return special node for when p == EVBDD_TERMINAL + */ +static inline evbddnode_t +EVBDD_GETNODE(EVBDD_TARG p) +{ + return (evbddnode_t) llmsset_index_to_ptr(nodes, p); +} + +/** + * Packs a EVBDD_TARG and EVBDD_WGT into a single 64 bit EVBDD. + */ +static inline EVBDD +evbdd_bundle(EVBDD_TARG p, EVBDD_WGT a) +{ + if (larger_wgt_indices) { + assert (p <= 0x000000003ffffffe); // avoid clash with sylvan_invalid + assert (a <= (1LL<<33)); + return (a << 30 | p); + }else { + assert (p <= 0x000000fffffffffe); // avoid clash with sylvan_invalid + assert (a <= (1<<23)); + return (a << 40 | p); + } +} + +static void __attribute__((unused)) +evbddnode_unpack(evbddnode_t n, EVBDD_TARG *low, EVBDD_TARG *high, EVBDD_WGT *a, EVBDD_WGT *b) +{ + *low = evbddnode_getptrlow(n); + *high = evbddnode_getptrhigh(n); + bool norm_pos = (n->low & evbdd_wgt_pos_mask) >> 54; + bool norm_val = (n->low & evbdd_wgt_val_mask) >> 53; + + if (weight_norm_strat == NORM_L2) { + *b = EVBDD_WEIGHT(n->high); + *a = wgt_get_low_L2normed(*b); + } + else { + if (norm_pos == 0) { // low WGT is EVBDD_ZERO or EVBDD_ONE, high WGT in table + *a = (norm_val == 0) ? EVBDD_ZERO : EVBDD_ONE; + *b = EVBDD_WEIGHT(n->high); + } + else { // high WGT is EVBDD_ZERO or EVBDD_ONE, low WGT in table + *b = (norm_val == 0) ? EVBDD_ZERO : EVBDD_ONE; + *a = EVBDD_WEIGHT(n->high); + } + } +} + +static void __attribute__((unused)) +evbddnode_getchilderen(evbddnode_t n, EVBDD *low, EVBDD *high) +{ + EVBDD_TARG l, h; + EVBDD_WGT a, b; + evbddnode_unpack(n, &l, &h, &a, &b); + *low = evbdd_bundle(l, a); + *high = evbdd_bundle(h, b); +} + +static void __attribute__((unused)) +evbddnode_pack(evbddnode_t n, BDDVAR var, EVBDD_TARG low, EVBDD_TARG high, EVBDD_WGT a, EVBDD_WGT b) +{ + // We only want to store 1 edge weight per node (which has 2 outgoing + // edges). For NORM_LOW and NORM_MAX this is relatively easy because in + // both those cases there is at least one edge weight equal to 1 or 0. + // + // For NORM_L2 it is a bit more complicated: both edge weights can be + // outside of {0, 1}, but under the constraint that |low|^2 + |high|^2 = 1, + // (or both are 0) and that |low| \in R+, we only need to store high, and + // can derive low. + + // these will be set depending on the normalization strategy + // (retrieval of edge weights is also dependent on normalization strategy) + EVBDD_WGT wgt_high; + bool norm_pos; + bool norm_val; + + if (weight_norm_strat == NORM_L2) { + assert(!(a == EVBDD_ZERO && b == EVBDD_ZERO)); // redundant node (caught before) + norm_pos = 0; + norm_val = 0; + wgt_high = b; // we can derive a from b + } + else { + /// weight_norm_strat == NORM_LOW or NORM_MAX or NORM_MIN + assert(a == EVBDD_ZERO || a == EVBDD_ONE || b == EVBDD_ZERO || b == EVBDD_ONE); + norm_pos = (a == EVBDD_ZERO || a == EVBDD_ONE) ? 0 : 1; + if (norm_pos == 0) { + norm_val = (a == EVBDD_ZERO) ? 0 : 1; + wgt_high = b; + } + else { + norm_val = (b == EVBDD_ZERO) ? 0 : 1; + wgt_high = a; + } + } + + // organize the bit structure of low and high + n->low = ((uint64_t)var)<<55 | ((uint64_t)norm_pos)<<54 | ((uint64_t)norm_val)<<53 | low; + if (larger_wgt_indices) { + n->high = wgt_high<<30 | high; + } + else { + n->high = wgt_high<<40 | high; + } +} + +static EVBDD_TARG __attribute__((unused)) +_evbdd_makenode(BDDVAR var, EVBDD_TARG low, EVBDD_TARG high, EVBDD_WGT a, EVBDD_WGT b) +{ + struct evbddnode n; + + evbddnode_pack(&n, var, low, high, a, b); + + EVBDD_TARG result; + int created; + EVBDD_TARG index = llmsset_lookup(nodes, n.low, n.high, &created); + if (index == 0) { + //printf("auto gc of node table triggered\n"); + + evbdd_refs_push(low); + evbdd_refs_push(high); + sylvan_gc(); + evbdd_refs_pop(2); + + index = llmsset_lookup(nodes, n.low, n.high, &created); + if (index == 0) { + fprintf(stderr, "EVBDD/BDD Unique table full, %zu of %zu buckets filled!\n", llmsset_count_marked(nodes), llmsset_get_size(nodes)); + exit(1); + } + } + + if (created) sylvan_stats_count(EVBDD_NODES_CREATED); + else sylvan_stats_count(EVBDD_NODES_REUSED); + + result = index; + //return mark ? result | evbdd_marked_mask : result; + return result; +} + +static EVBDD __attribute__((unused)) +evbdd_makenode(BDDVAR var, EVBDD low, EVBDD high) +{ + EVBDD_TARG low_trg = EVBDD_TARGET(low); + EVBDD_WGT low_wgt = EVBDD_WEIGHT(low); + EVBDD_TARG high_trg = EVBDD_TARGET(high); + EVBDD_WGT high_wgt = EVBDD_WEIGHT(high); + + // Edges with weight 0 should point straight to terminal. + if (low_wgt == EVBDD_ZERO) low_trg = EVBDD_TERMINAL; + if (high_wgt == EVBDD_ZERO) high_trg = EVBDD_TERMINAL; + + // If both low and high are the same (both TARG and WGT) return low + if (low == high) return low; + else { + // If the edges are not the same + EVBDD_WGT norm = (*normalize_weights)(&low_wgt, &high_wgt); + EVBDD_TARG res = _evbdd_makenode(var, low_trg, high_trg, low_wgt, high_wgt); + return evbdd_bundle(res, norm); + } +} + +/****************