Page MenuHomePhorge
Files F27032944

bbdd.hpp
No OneTemporary
Actions

Authored By
Unknown
Size
29 KB
Referenced Files
None
Subscribers
None

bbdd.hpp
View Options

// Copyright 2025 Oliver Theimer
#pragma once
#include <cstdint>
#include <cstdio>
#include <iostream>
#include "./bbdd_node.hpp"
#include "./bbdd_types.hpp"
#include "./chain_variable_ordering.hpp"
#include "./unique_table.hpp"
/**
* @brief decrement external reference count for a given bbdd node
*
* @param table hash table in which the node is stored
* @param node for which the external reference count is supposed to be
* decremented
* @return the same node with the new external reference value
*/
inline bbdd_node_t *del_ref(Unique_table *table, bbdd_node_t *node) {
if (node->ref > 0) {
node->ref--;
}
return node;
}
/**
* @brief increment external reference value for given node
*
* @param node whose external reference count is supposed to be incremented
* @return the same node with the new external reference value
*/
inline bbdd_node_t *add_ref(bbdd_node_t *node) {
node->ref++;
return node;
}
/**
* @brief revursively negate the bbdd given by a bbdd node
*
* @param table in which the bbdd nodes are stored
* @param f root node for which the subtree should be negated
* @return new bbdd node that is the root for the resulting diagram
*/
inline bbdd_node_t *negate_recursive(Unique_table *table, bbdd_node_t *f) {
if (IS_TERM(f->index)) {
if (f->index == 0) {
return table->get_node_p(1);
} else {
return table->get_node_p(0);
}
}
bbdd_node_t *neq, *eq, *new_root;
neq = negate_recursive(table, table->get_node_p(f->neq_child));
eq = negate_recursive(table, table->get_node_p(f->eq_child));
assert(f->cvo_lvl.sv == INT_MAX ||
POS(f->cvo_lvl.pv, table->cvo) < POS(f->cvo_lvl.sv, table->cvo));
new_root = table->insert_node({f->cvo_lvl, neq->index, eq->index});
return new_root;
}
/**
* @brief returns bbdd for two given inputs and a Boolean operation
*
* @param table table in which the result should be stored
* @param c1_i first input
* @param c2_i second input
* @param op boolean operation which combines the two inputs
* @return bbdd node that is the root to the resulting bbdd
*/
inline bbdd_node_t *base_case_two_inputs(Unique_table *table, node_index_t c1_i,
node_index_t c2_i,
const bbdd_op_t op) {
#ifdef DEBUG_BBDD
std::cout << "[INFO] TWO INPUT BASE CASE: " << c1_i << " " << bbdd_op_s[op]
<< " " << c2_i << "\n";
#endif
assert(c1_i != c2_i);
uint32_t pv, sv;
// define pv and sv based on position in ordering
if (POS(c1_i, table->cvo) < POS(c2_i, table->cvo)) {
pv = c1_i;
sv = c2_i;
} else {
pv = c2_i;
sv = c1_i;
}
assert(POS(pv, table->cvo) < POS(sv, table->cvo));
bbdd_node_t *root, *child;
switch (op) {
case bbdd_and:
child = table->insert_node({{sv, INT_MAX}, 0, 1});
root = table->insert_node({{pv, sv}, 0, child->index});
break;
case bbdd_or:
child = table->insert_node({{sv, INT_MAX}, 0, 1});
root = table->insert_node({{pv, sv}, 1, child->index});
break;
case bbdd_xor:
// cvo, eq, neq
root = table->insert_node({{pv, sv}, 1, 0});
break;
case bbdd_xnor:
root = table->insert_node({{pv, sv}, 0, 1});
break;
case bbdd_nand:
child = table->insert_node({{sv, INT_MAX}, 1, 0});
root = table->insert_node({{pv, sv}, 1, child->index});
break;
case bbdd_nor:
child = table->insert_node({{sv, INT_MAX}, 1, 0});
root = table->insert_node({{pv, sv}, 0, child->index});
break;
case bbdd_andnot:
child = table->insert_node({{sv, INT_MAX}, 1, 0});
root = table->insert_node({{pv, sv}, child->index, 0});
break;
case bbdd_notand:
child = table->insert_node({{sv, INT_MAX}, 0, 1});
root = table->insert_node({{pv, sv}, child->index, 0});
break;
default:
std::cout << "[ERROR] MERGE: base case " << bbdd_op_s[op].c_str()
<< " not implemented \n";
assert(false && "base case not implemented yet :");
}
return root;
}
/**
* @brief returns bbdd that is the result of combining a bbdd with a primary
* input and a given Boolean operation
*
* @param table in whicht the result should be stored and the given bbdd is
* stored
* @param f bbdd root node
* @param g_i primary input index
* @param op Boolean operation which should be used for the calculation
* @return root node to the calculated bbdd
*/
inline bbdd_node_t *merge_one_terminal_base_case(Unique_table *table,
bbdd_node_t *f,
node_index_t g_i,
bbdd_op_t op) {
assert(g_i == 0 || g_i == 1);
#ifdef DEBUG_BBDD
std::cout << "[INFO] MERGE: one terminal " << f->index << " and " << g_i
<< " = " << bbdd_op_s[op].c_str() << "\n";
#endif
bbdd_node_t *neg_f;
if (g_i == 1) {
switch (op) {
case bbdd_and:
case bbdd_xnor:
return f;
case bbdd_or:
return table->get_node_p(1);
case bbdd_xor:
case bbdd_nand:
return negate_recursive(table, f);
case bbdd_nor:
return table->get_node_p(0);
case bbdd_notand:
return negate_recursive(table, f);
break;
default:
std::cout << "[ERROR] MERGE: one terminal " << bbdd_op_s[op].c_str()
<< " not implemented \n";
assert(false && "one terminal base case not implemented");
return 0;
}
} else {
switch (op) {
case bbdd_and:
case bbdd_notand:
return table->get_node_p(0);
case bbdd_or:
case bbdd_xor:
case bbdd_nand:
return f;
case bbdd_xnor:
case bbdd_nor:
return negate_recursive(table, f);
default:
std::cout << "[ERROR] MERGE: one terminal " << bbdd_op_s[op].c_str()
<< " not implemented \n";
assert(false);
return 0;
}
}
}
/**
* @brief merge two terminal bbdd nodes
*
* @param c1 first terminal node
* @param c2 second terminal node
* @param op Boolean operation which is used to combine the terminal node
* @return terminal bbdd node (either 0 or 1)
*/
inline node_index_t
merge_two_terminal_base_case(node_index_t c1, node_index_t c2, bbdd_op_t op) {
assert((c1 == 0 || c1 == 1) && (c2 == 0 || c2 == 1));
#ifdef DEBUG_BBDD
std::cout << "[INFO] MERGE: two terminal " << c1 << " and " << c2 << " = "
<< bbdd_op_s[op].c_str() << "\n";
#endif
switch (op) {
case bbdd_and:
return c1 && c2;
case bbdd_nand:
if (c1 && c2) {
return 0;
} else {
return 1;
}
case bbdd_or:
return c1 || c2;
case bbdd_nor:
if (c1 || c2) {
return 0;
} else {
return 1;
}
case bbdd_xor:
return c1 != c2;
case bbdd_xnor:
return c1 == c2;
case bbdd_notand:
if (c1 == 1) {
return 0;
} else {
return c2;
}
default:
std::cout << "[ERROR] MERGE: two terminal " << bbdd_op_s[op].c_str()
<< " not implemented \n";
assert(false);
return 0;
}
return 0;
}
/**
* @brief merge two bbdd nodes that are identical with the fiven Boolean
* operation
*
* @param table
* @param f
* @param op
* @return
*/
inline bbdd_node_t *merge_equal_base_case(Unique_table *table, bbdd_node_t *f,
bbdd_op_t op) {
#ifdef DEBUG_BBDD
std::cout << "[INFO] MERGE: equal base case " << f->index << " with "
<< bbdd_op_s[op].c_str() << "\n";
#endif
switch (op) {
case bbdd_and:
case bbdd_or:
return f;
case bbdd_xor:
case bbdd_notand:
return table->get_node_p(0);
case bbdd_xnor:
return table->get_node_p(1);
case bbdd_nand:
case bbdd_nor:
return negate_recursive(table, f);
default:
std::cout << "[ERROR] MERGE: equal case " << bbdd_op_s[op].c_str()
<< " not implemented \n";
assert(false);
return 0;
}
}
/**
* @brief extend bbdd node based on a second bbdd and an extend case
*
* @param table hash table in which the two bbdd must be stored and the result
* will be inserted
* @param f bbdd node to be extended
* @param g bbdd node to be used for case
* @param extend_case case in which the two bbdd cvo intervals intersect
* @return root node of newly created bbdd
*/
static bbdd_node_t *extend_node(Unique_table *table, bbdd_node_t *f,
bbdd_node_t *g, bbdd_cases_t extend_case) {
bbdd_node_t *new_root, *neq, *eq, *c_neq_eq, *c_eq_neq, *c_neq_neq, *c_eq_eq;
bool update_neq, update_eq;
#ifdef DEBUG_BBDD
printf("[INFO] EXTEND: extending %d and %d with %s\n", f->index, g->index,
bbdd_cases_s[extend_case].c_str());
#endif
assert(g->cvo_lvl.sv == INT_MAX ||
POS(g->cvo_lvl.pv, table->cvo) < POS(g->cvo_lvl.sv, table->cvo));
assert(f->cvo_lvl.sv == INT_MAX ||
POS(f->cvo_lvl.pv, table->cvo) < POS(f->cvo_lvl.sv, table->cvo));
switch (extend_case) {
case case_2f:
assert(POS(g->cvo_lvl.pv, table->cvo) < POS(f->cvo_lvl.sv, table->cvo) ||
f->cvo_lvl.sv == INT_MAX);
c_eq_neq = table->insert_node(
{{g->cvo_lvl.pv, f->cvo_lvl.sv}, f->eq_child, f->neq_child});
c_neq_eq = table->insert_node(
{{g->cvo_lvl.pv, f->cvo_lvl.sv}, f->neq_child, f->eq_child});
assert(POS(f->cvo_lvl.pv, table->cvo) < POS(g->cvo_lvl.pv, table->cvo));
return table->insert_node(
{{f->cvo_lvl.pv, g->cvo_lvl.pv}, c_eq_neq->index, c_neq_eq->index});
case case_2g:
assert(POS(g->cvo_lvl.sv, table->cvo) < POS(f->cvo_lvl.sv, table->cvo) ||
f->cvo_lvl.sv == INT_MAX);
c_eq_neq = table->insert_node(
{{g->cvo_lvl.sv, f->cvo_lvl.sv}, f->eq_child, f->neq_child});
c_neq_eq = table->insert_node(
{{g->cvo_lvl.sv, f->cvo_lvl.sv}, f->neq_child, f->eq_child});
assert(POS(f->cvo_lvl.pv, table->cvo) < POS(g->cvo_lvl.sv, table->cvo));
return table->insert_node(
{{f->cvo_lvl.pv, g->cvo_lvl.sv}, c_eq_neq->index, c_neq_eq->index});
case case_3f:
c_eq_neq = table->insert_node({g->cvo_lvl, f->eq_child, f->neq_child});
c_neq_eq = table->insert_node({g->cvo_lvl, f->neq_child, f->eq_child});
assert(POS(f->cvo_lvl.pv, table->cvo) < POS(g->cvo_lvl.pv, table->cvo));
return table->insert_node(
{{f->cvo_lvl.pv, g->cvo_lvl.pv}, c_eq_neq->index, c_neq_eq->index});
case case_4f:
assert(POS(g->cvo_lvl.pv, table->cvo) < POS(f->cvo_lvl.sv, table->cvo) ||
f->cvo_lvl.sv == INT_MAX);
neq = table->insert_node(
{{g->cvo_lvl.pv, f->cvo_lvl.sv}, f->eq_child, f->neq_child});
eq = table->insert_node(
{{g->cvo_lvl.pv, f->cvo_lvl.sv}, f->neq_child, f->eq_child});
assert(POS(f->cvo_lvl.pv, table->cvo) < POS(g->cvo_lvl.pv, table->cvo));
return table->insert_node(
{{f->cvo_lvl.pv, g->cvo_lvl.pv}, neq->index, eq->index});
case case_5f:
assert(POS(g->cvo_lvl.sv, table->cvo) < POS(f->cvo_lvl.sv, table->cvo) ||
f->cvo_lvl.sv == INT_MAX);
neq = table->insert_node(
{{g->cvo_lvl.sv, f->cvo_lvl.sv}, f->eq_child, f->neq_child});
eq = table->insert_node(
{{g->cvo_lvl.sv, f->cvo_lvl.sv}, f->neq_child, f->eq_child});
assert(POS(f->cvo_lvl.pv, table->cvo) < POS(g->cvo_lvl.sv, table->cvo));
return table->insert_node(
{{f->cvo_lvl.pv, g->cvo_lvl.sv}, neq->index, eq->index});
default:
std::cout << "[ERROR] EXTEND " << bbdd_cases_s[extend_case].c_str()
<< " not implemented \n";
assert(false);
}
return NULL;
}
/**
* @brief extend two bbdds in order that they have the same levels of nodes
*
* @param table in which the two bbdds are stored and the result should be
* inserted
* @param f first bbdd node
* @param g second bbdd node
* @return pair of newly created root nodes after the extension
*/
inline bbdd_node_ppair_t extend_bbdds(Unique_table *table, bbdd_node_t *f,
bbdd_node_t *g) {
extend_key key = {f->index, g->index};
auto res = table->extend_table.find(key);
#ifdef CACHE_STATS
table->cache_stats.extend_lookups++;
#endif
if (res != table->extend_table.end()) {
#ifdef CACHE_STATS
table->cache_stats.extend_hits++;
#endif
return res->second;
}
assert(g->cvo_lvl.sv == INT_MAX ||
POS(g->cvo_lvl.pv, table->cvo) < POS(g->cvo_lvl.sv, table->cvo));
assert(f->cvo_lvl.sv == INT_MAX ||
POS(f->cvo_lvl.pv, table->cvo) < POS(f->cvo_lvl.sv, table->cvo));
if (g->index == f->index) {
return {f, g};
}
if (IS_TERM(g->index) || IS_TERM(f->index)) {
return {f, g};
}
bbdd_cases_t extend_case = compare_nodes(f, g, table->cvo);
bbdd_node_t *f_neq = table->get_node_p(f->neq_child),
*f_eq = table->get_node_p(f->eq_child),
*g_neq = table->get_node_p(g->neq_child),
*g_eq = table->get_node_p(g->eq_child);
bbdd_node_t *new_f, *new_g, *extended_f, *extended_g;
bbdd_node_ppair_t new_neq, new_eq;
switch (extend_case) {
case case_0:
new_neq = extend_bbdds(table, f_neq, g_neq);
new_eq = extend_bbdds(table, f_eq, g_eq);
new_f = table->insert_node({f->cvo_lvl, new_neq.f->index, new_eq.f->index});
new_g = table->insert_node({g->cvo_lvl, new_neq.g->index, new_eq.g->index});
table->extend_table[key] = {new_f, new_g};
return {new_f, new_g};
case case_1f:
new_neq = extend_bbdds(table, f_neq, g);
new_eq = extend_bbdds(table, f_eq, g);
new_f = table->insert_node({f->cvo_lvl, new_neq.f->index, new_eq.f->index});
new_g = table->insert_node({f->cvo_lvl, new_neq.g->index, new_eq.g->index});
table->extend_table[key] = {new_f, new_g};
return {new_f, new_g};
case case_1g:
new_neq = extend_bbdds(table, f, g_neq);
new_eq = extend_bbdds(table, f, g_eq);
new_f = table->insert_node({g->cvo_lvl, new_neq.f->index, new_eq.f->index});
new_g = table->insert_node({g->cvo_lvl, new_neq.g->index, new_eq.g->index});
table->extend_table[key] = {new_f, new_g};
return {new_f, new_g};
case case_2f:
extended_f = extend_node(table, f, g, case_2f);
extended_g = extend_node(table, g, f, case_2g);
new_neq = extend_bbdds(table, table->get_node_p(extended_f->neq_child),
extended_g);
new_eq = extend_bbdds(table, table->get_node_p(extended_f->eq_child),
extended_g);
new_f = table->insert_node(
{extended_f->cvo_lvl, new_neq.f->index, new_eq.f->index});
new_g = table->insert_node(
{extended_f->cvo_lvl, new_neq.g->index, new_eq.g->index});
table->extend_table[key] = {new_f, new_g};
return {new_f, new_g};
case case_2g:
extended_f = extend_node(table, f, g, case_2g);
extended_g = extend_node(table, g, f, case_2f);
new_neq = extend_bbdds(table, extended_f,
table->get_node_p(extended_g->neq_child));
new_eq = extend_bbdds(table, extended_f,
table->get_node_p(extended_g->eq_child));
new_f = table->insert_node(
{extended_g->cvo_lvl, new_neq.f->index, new_eq.f->index});
new_g = table->insert_node(
{extended_g->cvo_lvl, new_neq.g->index, new_eq.g->index});
table->extend_table[key] = {new_f, new_g};
return {new_f, new_g};
case case_3f:
extended_f = extend_node(table, f, g, case_3f);
new_neq = extend_bbdds(table, table->get_node_p(extended_f->neq_child), g);
new_eq = extend_bbdds(table, table->get_node_p(extended_f->eq_child), g);
new_f = table->insert_node(
{extended_f->cvo_lvl, new_neq.f->index, new_eq.f->index});
new_g = table->insert_node(
{extended_f->cvo_lvl, new_neq.g->index, new_eq.g->index});
table->extend_table[key] = {new_f, new_g};
return {new_f, new_g};
case case_3g:
extended_g = extend_node(table, g, f, case_3f);
new_neq = extend_bbdds(table, f, table->get_node_p(extended_g->neq_child));
new_eq = extend_bbdds(table, f, table->get_node_p(extended_g->eq_child));
new_f = table->insert_node(
{extended_g->cvo_lvl, new_neq.f->index, new_eq.f->index});
new_g = table->insert_node(
{extended_g->cvo_lvl, new_neq.g->index, new_eq.g->index});
table->extend_table[key] = {new_f, new_g};
return {new_f, new_g};
case case_4f:
extended_f = extend_node(table, f, g, case_4f);
new_neq = extend_bbdds(table, table->get_node_p(extended_f->neq_child), g);
new_eq = extend_bbdds(table, table->get_node_p(extended_f->eq_child), g);
new_f = table->insert_node(
{extended_f->cvo_lvl, new_neq.f->index, new_eq.f->index});
new_g = table->insert_node(
{extended_f->cvo_lvl, new_neq.g->index, new_eq.g->index});
table->extend_table[key] = {new_f, new_g};
return {new_f, new_g};
case case_4g:
extended_g = extend_node(table, g, f, case_4f);
new_neq = extend_bbdds(table, f, table->get_node_p(extended_g->neq_child));
new_eq = extend_bbdds(table, f, table->get_node_p(extended_g->eq_child));
new_f = table->insert_node(
{extended_g->cvo_lvl, new_neq.f->index, new_eq.f->index});
new_g = table->insert_node(
{extended_g->cvo_lvl, new_neq.g->index, new_eq.g->index});
table->extend_table[key] = {new_f, new_g};
return {new_f, new_g};
case case_5f:
extended_f = extend_node(table, f, g, case_5f);
new_neq =
extend_bbdds(table, table->get_node_p(extended_f->neq_child), g_neq);
new_eq = extend_bbdds(table, table->get_node_p(extended_f->eq_child), g_eq);
new_f = table->insert_node(
{extended_f->cvo_lvl, new_neq.f->index, new_eq.f->index});
new_g = table->insert_node(
{extended_f->cvo_lvl, new_neq.g->index, new_eq.g->index});
table->extend_table[key] = {new_f, new_g};
return {new_f, new_g};
case case_5g:
extended_g = extend_node(table, g, f, case_5f);
new_neq =
extend_bbdds(table, f_neq, table->get_node_p(extended_g->neq_child));
new_eq = extend_bbdds(table, f_eq, table->get_node_p(extended_g->eq_child));
new_f = table->insert_node(
{extended_g->cvo_lvl, new_neq.f->index, new_eq.f->index});
new_g = table->insert_node(
{extended_g->cvo_lvl, new_neq.g->index, new_eq.g->index});
table->extend_table[key] = {new_f, new_g};
return {new_f, new_g};
default:
assert(false && "not implemented");
}
}
/**
* @brief recursive helper function to merge two bbdds
*
* @param table in which the two bbdds are stored and in which the result should
* be inserted
* @param f first bbdd root node
* @param g second bbdd root node
* @param op Boolean operation that should be used to merge the two bbdds
* @return root node to subgraph that is the result of the merge
*/
static bbdd_node_t *merge_recursive(Unique_table *table, bbdd_node_t *f,
bbdd_node_t *g, bbdd_op_t op) {
bbdd_node_t *new_root, *new_neq, *new_eq, *insert_neq, *insert_eq;
if (IS_TERM(g->index)) {
if (IS_TERM(f->index)) {
return table->get_node_p(
merge_two_terminal_base_case(f->index, g->index, op));
} else {
return merge_one_terminal_base_case(table, f, g->index, op);
}
} else if (IS_TERM(f->index)) {
return merge_one_terminal_base_case(table, g, f->index, op);
}
if (f == g) {
return merge_equal_base_case(table, f, op);
}
bbdd_cases_t bbdd_case = compare_nodes(f, g, table->cvo);
if (bbdd_case != case_0) {
printf("[ERROR] MERGE: error case %s should not happen with %d and %d\n",
bbdd_cases_s[bbdd_case].c_str(), f->index, g->index);
dump_node(f);
std::cout << "\n";
dump_node(g);
std::cout << "\n";
table->dump_table();
}
assert(bbdd_case == case_0);
assert(f->cvo_lvl.pv == g->cvo_lvl.pv && f->cvo_lvl.sv == g->cvo_lvl.sv);
assert(f->cvo_lvl.sv == INT_MAX ||
POS(f->cvo_lvl.pv, table->cvo) < POS(f->cvo_lvl.sv, table->cvo));
new_neq = merge_recursive(table, table->get_node_p(f->neq_child),
table->get_node_p(g->neq_child), op);
new_eq = merge_recursive(table, table->get_node_p(f->eq_child),
table->get_node_p(g->eq_child), op);
new_root = table->insert_node({f->cvo_lvl, new_neq->index, new_eq->index});
return new_root;
}
/**
* @brief delete the bbdd from the table if it does not have any other external
* references
*
* @param table in which the bbdd is stored
* @param f root node of a bbdd that should be deleted
*/
inline void delete_bbdd(Unique_table *table, bbdd_node_t *f) {
if (IS_TERM(f->index)) {
return;
}
if (f->ref == 0) {
table->delete_node(f);
del_ref(table, table->get_node_p(f->neq_child));
delete_bbdd(table, table->get_node_p(f->neq_child));
del_ref(table, table->get_node_p(f->eq_child));
delete_bbdd(table, table->get_node_p(f->eq_child));
}
}
/**
* @brief merge two existing bbdds into a single one based on a given Boolean
* operation
*
* @param table hash table in which both bbdds are stored
* @param f first bbdd
* @param g second bbdd
* @param op Boolean operation that is used for the merge
* @return root node of the resulting bbdd
*/
inline bbdd_node_t *merge_bbdds(Unique_table *table, bbdd_node_t *f,
bbdd_node_t *g, bbdd_op_t op) {
#ifdef DEBUG_BBDD
printf("[INFO]-----------------------------------------------\n");
printf("[INFO] Extending %d\n", f->index);
dump_node(f);
printf("\n");
printf("[INFO]-----------------------------------------------\n");
printf("[INFO] Extending %d \n", g->index);
dump_node(g);
printf("\n");
#endif
merge_key key = {f, g, op};
auto res = table->computed_table.find(key);
#ifdef CACHE_STATS
table->cache_stats.merge_lookups++;
#endif
if (res != table->computed_table.end()) {
#ifdef CACHE_STATS
table->cache_stats.merge_hits++;
#endif
#ifdef DEBUG
printf("[INFO] UNIQUE TABLE: %d %s %d\n", f->index, bbdd_op_s[op].c_str(),
g->index);
#endif
bbdd_node_t *node = table->get_node_p(res->second);
assert(node->cvo_lvl.sv == INT_MAX ||
POS(node->cvo_lvl.pv, table->cvo) <
POS(node->cvo_lvl.sv, table->cvo));
return node;
}
bbdd_node_ppair_t extended_nodes = extend_bbdds(table, f, g);
bbdd_node_t *new_root =
merge_recursive(table, extended_nodes.f, extended_nodes.g, op);
table->computed_table[key] = new_root->index;
return table->reduce_bbdd(new_root);
}
/**
* @brief merge bbdd with a primary input based on a given Boolean operation
*
* @param table in which the provided bbdd is stored and the newly created is
* inserted
* @param f root node to the bbdd that should be merged
* @param g_i primary input to be used for the merge
* @param op Boolean operation for the merge operation
* @return root node to the resulting bbdd
*/
inline bbdd_node_t *merge_bbdds(Unique_table *table, bbdd_node_t *f,
node_index_t g_i, bbdd_op_t op) {
bbdd_node_t *g = table->insert_node({{g_i, INT_MAX}, 0, 1});
return merge_bbdds(table, f, g, op);
}
/**
* @brief sifting algorithm based on a given target function. Implementation is
* based on the original paper by Bryant
*
* @param table hash table in which the bbdd nodes should be sifted
* @param obj target function which should be minimized
*/
inline void sift(Unique_table *table, uint32_t (Unique_table::*f)(),
Unique_table *obj) {
table->clear_computed_table();
table->clear_extend_table();
for (int variable = 0; variable < table->cvo->size(); variable++) {
int original_pos = POS(variable, table->cvo);
int best_pos = original_pos;
uint32_t initial_height = (obj->*f)();
uint32_t best_height = (obj->*f)();
#ifdef DEBUG_SIFT
printf("initial best height for variable %d: %d at %d\n", variable,
best_height, best_pos);
table->dump_outputs();
#endif
// Move variable up step by step
int current_pos = original_pos;
while (current_pos > 0) {
table->swap_all_positions(current_pos - 1, current_pos);
uint32_t current_height = (obj->*f)();
#ifdef DEBUG_SIFT
printf("height: %d at pos: %d\n", current_height, current_pos - 1);
#endif
if (current_height < best_height) {
best_height = current_height;
best_pos = current_pos - 1;
}
current_pos--;
}
assert(current_pos == 0);
// Move variable down step by step
while (current_pos < table->cvo->size() - 1) {
table->swap_all_positions(current_pos, current_pos + 1);
uint32_t current_height = (obj->*f)();
#ifdef DEBUG_SIFT
printf("height: %d at pos: %d\n", current_height, current_pos + 1);
#endif
if (current_height < best_height) {
best_height = current_height;
best_pos = current_pos + 1;
}
current_pos++;
}
assert(current_pos == table->cvo->size() - 1);
// Restore best position
while (current_pos > best_pos) {
table->swap_all_positions(current_pos - 1, current_pos);
current_pos--;
}
#ifdef DEBUG_SIFT
printf("best pos of variable %d: %d with height: %d\n", variable, best_pos,
table->get_total_height());
dump_ordering(table->cvo);
table->dump_outputs();
#endif
}
}
/**
* @brief sift algorithm that uses the bbdd height as a target function.
* Implementation is based on the work by Bryant
*
* @param table in which the bbdd nodes should be sifted
*/
inline void sift(Unique_table *table) {
for (int variable = 0; variable < table->cvo->size(); variable++) {
int original_pos = POS(variable, table->cvo);
int best_pos = original_pos;
uint32_t initial_height = table->get_total_height();
uint32_t best_height = table->get_total_height();
#ifdef DEBUG_SIFT
printf("initial best height for variable %d: %d at %d\n", variable,
best_height, best_pos);
table->dump_outputs();
#endif
// Move variable up step by step
int current_pos = original_pos;
while (current_pos > 0) {
table->swap_all_positions(current_pos - 1, current_pos);
uint32_t current_height = table->get_total_height();
#ifdef DEBUG_SIFT
printf("height: %d at pos: %d\n", current_height, current_pos - 1);
#endif
if (current_height < best_height) {
best_height = current_height;
best_pos = current_pos - 1;
}
current_pos--;
}
assert(current_pos == 0);
// Move variable down step by step
while (current_pos < table->cvo->size() - 1) {
table->swap_all_positions(current_pos, current_pos + 1);
uint32_t current_height = table->get_total_height();
#ifdef DEBUG_SIFT
printf("height: %d at pos: %d\n", current_height, current_pos + 1);
#endif
if (current_height < best_height) {
best_height = current_height;
best_pos = current_pos + 1;
}
current_pos++;
}
assert(current_pos == table->cvo->size() - 1);
// Restore best position
/*while (current_pos < best_pos) {
table->swap_all_positions(current_pos, current_pos + 1);
current_pos++;
}*/
while (current_pos > best_pos) {
table->swap_all_positions(current_pos - 1, current_pos);
current_pos--;
}
#ifdef DEBUG_SIFT
printf("best pos of variable %d: %d with height: %d\n", variable, best_pos,
table->get_total_height());
dump_ordering(table->cvo);
table->dump_outputs();
#endif
}
}
/**
* @brief sift a single bbdd
*
* @param table hash table in which the bbdd is stored and the result will be inserted
* @param node root node of the input bbdd
* @return root node of the resulting bbdd
*/
inline bbdd_node_t *sift_bbdd(Unique_table *table, bbdd_node_t *node) {
bbdd_node_t *new_root = node;
for (int variable = 0; variable < table->cvo->size(); variable++) {
int original_pos = POS(variable, table->cvo);
int best_pos = original_pos;
uint32_t best_height = table->get_tree_height(new_root);
printf("initial best height: %d\n", best_height);
// Move variable up step by step
int current_pos = original_pos;
while (current_pos > 0) {
new_root = table->reduce_bbdd(
table->swap_positions(new_root, current_pos - 1, current_pos));
uint32_t current_height = table->get_tree_height(node);
if (current_height < best_height) {
best_height = current_height;
best_pos = current_pos - 1;
}
current_pos--;
}
// Restore variable to original position
while (current_pos < original_pos) {
new_root = table->reduce_bbdd(
table->swap_positions(new_root, current_pos, current_pos + 1));
current_pos++;
}
// Move variable down step by step
current_pos = original_pos;
while (current_pos < table->cvo->size() - 1) {
new_root = table->reduce_bbdd(
table->swap_positions(new_root, current_pos, current_pos + 1));
uint32_t current_height = table->get_tree_height(new_root);
if (current_height < best_height) {
best_height = current_height;
best_pos = current_pos + 1;
}
current_pos++;
}
// Restore variable to original position
while (current_pos > original_pos) {
new_root = table->reduce_bbdd(
table->swap_positions(new_root, current_pos - 1, current_pos));
current_pos--;
}
// Finally move variable to best position
while (original_pos < best_pos) {
new_root = table->reduce_bbdd(
table->swap_positions(new_root, original_pos, original_pos + 1));
original_pos++;
}
while (original_pos > best_pos) {
new_root = table->reduce_bbdd(
table->swap_positions(new_root, original_pos - 1, original_pos));
original_pos--;
}
// printf("best pos of variable %d: %d with height: %d\n", variable,
// best_pos, table->get_tree_height(new_root)); dump_ordering(table->cvo);
}
return new_root;
}

File Metadata

Mime Type
text/x-c
Expires
Tue, Oct 27, 3:30 PM (22 h, 6 m)
Storage Engine
blob
Storage Format
Raw Data
Storage Handle
404727
Default Alt Text
bbdd.hpp (29 KB)

Event Timeline