No OneTemporary
Actions

Size

85 KB

Referenced Files

None

Subscribers

None

View Options

	diff --git a/include/bbdd.hpp b/include/bbdd.hpp
	new file mode 100644
	index 0000000..5125652
	--- /dev/null
	+++ b/include/bbdd.hpp
	@@ -0,0 +1,849 @@
	+// 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;
	+}
	diff --git a/include/bbdd_node.hpp b/include/bbdd_node.hpp
	new file mode 100644
	index 0000000..0f320e4
	--- /dev/null
	+++ b/include/bbdd_node.hpp
	@@ -0,0 +1,203 @@
	+// Copyright 2025 Oliver Theimer
	+#pragma once
	+
	+#include <cassert>
	+#include <climits>
	+#include <cstdint>
	+#include <cstdio>
	+#include <iostream>
	+
	+#include "./bbdd_types.hpp"
	+#include "./chain_variable_ordering.hpp"
	+
	+#define IS_TERM(n) n == 0 \|\| n == 1
	+
	+#define MARK_ON 0x80000000
	+#define MARK_OFF 0x7FFFFFFF
	+#define MARKED(n) n->index &MARK_ON
	+#define GET_INDEX(n) n->index &MARK_OFF
	+#define SET_MARKED(n) n->index \|= MARK_ON
	+#define CLEAR_MARKED(n) n->index &= MARK_OFF
	+
	+/**
	+ * @class bbdd_node_t
	+ * @brief main bbdd storage element
	+ *
	+ */
	+struct bbdd_node_t {
	+ uint32_t ref;
	+ node_index_t index;
	+ cvo_pair_t cvo_lvl;
	+ bbdd_halfword_t neq_child;
	+ bbdd_halfword_t eq_child;
	+};
	+
	+/**
	+ * @class bbdd_node_template_t
	+ * @brief minimal storage element with information that is needed to insert a
	+ * bbdd node into the hash table
	+ *
	+ */
	+struct bbdd_node_template_t {
	+ cvo_pair_t cvo_lvl;
	+ node_index_t neq_child;
	+ node_index_t eq_child;
	+};
	+
	+/**
	+ * @class bbdd_node_ppair_t
	+ * @brief combination of two pointers to bbdd_nodes. Only used for the extension
	+ * of the bbdds
	+ *
	+ */
	+struct bbdd_node_ppair_t {
	+ bbdd_node_t *f;
	+ bbdd_node_t *g;
	+};
	+
	+/**
	+ * @brief comparison of a bbdd_node_t and a bbdd_node_template_t that wants to
	+ * be inserted into the hash table
	+ *
	+ * @param lhs bbdd node
	+ * @param rhs bbdd node template
	+ * @return boolean whether or not the two equal
	+ */
	+bool inline node_eq(bbdd_node_t lhs, bbdd_node_template_t rhs) {
	+ return lhs.cvo_lvl.pv == rhs.cvo_lvl.pv && lhs.cvo_lvl.sv == rhs.cvo_lvl.sv &&
	+ lhs.eq_child == rhs.eq_child && lhs.neq_child == rhs.neq_child;
	+}
	+
	+/**
	+ * @brief checks the equivalence of two bbdd nodes
	+ *
	+ * @param lhs bbdd node
	+ * @param rhs bbdd node
	+ * @return boolean whether or not the two equal
	+ */
	+bool inline node_eq(bbdd_node_t lhs, bbdd_node_t rhs) {
	+ return lhs.cvo_lvl.pv == rhs.cvo_lvl.pv && lhs.cvo_lvl.sv == rhs.cvo_lvl.sv &&
	+ lhs.eq_child == rhs.eq_child && lhs.neq_child == rhs.neq_child;
	+}
	+
	+/**
	+ * @brief cantor pairing implementation based on the original paper on bbdd by
	+ * Amaru et al.
	+ *
	+ * @param i value for calculation
	+ * @param j value for calculation
	+ * @return result of the cantor_pairing function
	+ */
	+static bbdd_halfword_t inline cantor_pairing(uint32_t i, uint32_t j) {
	+ return (bbdd_halfword_t)(0.5f * (i + j) * (i + j + 1)) + i;
	+}
	+
	+/**
	+ * @brief hashing function a bbdd node template
	+ *
	+ * @param node_t bbdd node template information
	+ * @param capacity capacity of the hash table
	+ * @return hashing value for the given node and capacity
	+ */
	+uint32_t inline hash_node(bbdd_node_template_t node_t, uint64_t capacity) {
	+ return cantor_pairing(node_t.neq_child,
	+ cantor_pairing(node_t.cvo_lvl.pv,
	+ cantor_pairing(node_t.cvo_lvl.sv,
	+ node_t.eq_child))) %
	+ capacity;
	+}
	+
	+/**
	+ * @brief hashing function for a bbdd node
	+ *
	+ * @param node bbdd node to be hashed
	+ * @param capacity capacity of the hash table
	+ * @return
	+ */
	+uint32_t inline hash_node(bbdd_node_t node, uint64_t capacity) {
	+ return hash_node({node.cvo_lvl, node.neq_child, node.eq_child}, capacity);
	+}
	+
	+/**
	+ * @brief dump formatted node information to stdout
	+ *
	+ * @param node to be printed
	+ */
	+void inline dump_node(bbdd_node_t *node) {
	+ fprintf(stdout, "%3d: (%3d, (%3d, %3d), %3d, %3d)", GET_INDEX(node),
	+ node->ref, node->cvo_lvl.pv == INT_MAX ? 1 : node->cvo_lvl.pv,
	+ node->cvo_lvl.sv == INT_MAX ? 1 : node->cvo_lvl.sv, node->neq_child,
	+ node->eq_child);
	+}
	+
	+/**
	+ * @brief compare two nodes based on there primary and secondary variable and
	+ * return the information how these intervals intersect
	+ *
	+ * @param f first bbdd node
	+ * @param g second bbdd node
	+ * @param cvo chain variable ordering for which the two bbdds should be assessed
	+ * @return case in which way the two intervals intersect
	+ */
	+inline bbdd_cases_t compare_nodes(bbdd_node_t f, bbdd_node_t g, cvo_t *cvo) {
	+#ifdef DEBUG
	+ printf("[INFO] COMPARE: ");
	+ dump_node(f);
	+ std::cout << " and ";
	+ dump_node(g);
	+ std::cout << "\n";
	+#endif
	+ // f.pv = i, f.sv = j
	+ // g.pv = k, g.sv = l
	+ uint32_t i = POS(f->cvo_lvl.pv, cvo), k = POS(g->cvo_lvl.pv, cvo);
	+ uint32_t j, l;
	+ if (f->cvo_lvl.sv != INT_MAX) {
	+ j = POS(f->cvo_lvl.sv, cvo);
	+ } else {
	+ j = INT_MAX;
	+ }
	+ if (g->cvo_lvl.sv != INT_MAX) {
	+ l = POS(g->cvo_lvl.sv, cvo);
	+ } else {
	+ l = INT_MAX;
	+ }
	+ if (!((i < j) && (k < l))) {
	+ dump_ordering(cvo);
	+ printf("i:%d, j:%d, k:%d, l:%d\n", i, j, k, l);
	+ dump_node(f);
	+ printf("\n");
	+ dump_node(g);
	+ printf("\n");
	+ }
	+ assert((i < j) && (k < l));
	+ // assumption i < j and k < j
	+ if ((i == k) && (j == l)) {
	+ return case_0;
	+ // Case 1
	+ } else if (j <= k) {
	+ return case_1f;
	+ } else if (l <= i) {
	+ return case_1g;
	+ // Case 2
	+ } else if ((i < k) && (k < j) && (j < l)) {
	+ return case_2f;
	+ } else if ((k < i) && (i < l) && (l < j)) {
	+ return case_2g;
	+ // Case 3
	+ } else if ((i < k) && (j == l)) {
	+ return case_3f;
	+ } else if ((k < i) && (j == l)) {
	+ return case_3g;
	+ // Case 4
	+ } else if ((i < k) && (k < l) && (l < j)) {
	+ return case_4f;
	+ } else if ((k < i) && (i < j) && (j < l)) {
	+ return case_4g;
	+ // Case 5
	+ } else if ((i == k) && (l < j)) {
	+ return case_5f;
	+ } else if ((i == k) && (j < l)) {
	+ return case_5g;
	+ }
	+ return case_not_implemented;
	+}
	diff --git a/include/bbdd_types.hpp b/include/bbdd_types.hpp
	new file mode 100644
	index 0000000..d3005c0
	--- /dev/null
	+++ b/include/bbdd_types.hpp
	@@ -0,0 +1,64 @@
	+// Copyright 2025 Oliver Theimer
	+#pragma once
	+
	+#include <cstdint>
	+#include <string>
	+#include <vector>
	+
	+#define SIZEOF_VOID_P 8
	+#define SIZEOF_INT 4
	+#if SIZEOF_VOID_P == 8 && SIZEOF_INT == 4
	+typedef uint32_t bbdd_halfword_t;
	+#else
	+typedef uint16_t bbdd_halfword_t;
	+#endif
	+
	+typedef uint32_t input_type_t;
	+typedef uint32_t node_type_t;
	+typedef uint32_t node_index_t;
	+
	+enum bbdd_cases {
	+ case_0,
	+ case_1f,
	+ case_1g,
	+ case_2f,
	+ case_2g,
	+ case_3f,
	+ case_3g,
	+ case_4f,
	+ case_4g,
	+ case_5f,
	+ case_5g,
	+ case_not_implemented
	+};
	+typedef enum bbdd_cases bbdd_cases_t;
	+
	+const std::vector<std::string> bbdd_cases_s = {"case_0", "case_1f", "case_1g",
	+ "case_2f", "case_2g", "case_3f",
	+ "case_3g", "case_4f", "case_4g",
	+ "case_5f", "case_5g", "case_not_implemented"};
	+
	+enum bbdd_op {
	+ bbdd_none,
	+ bbdd_and,
	+ bbdd_or,
	+ bbdd_nand,
	+ bbdd_nor,
	+ bbdd_xor,
	+ bbdd_xnor,
	+ bbdd_inv,
	+ bbdd_notand,
	+ bbdd_andnot,
	+ bbdd_notor,
	+ bbdd_ornot,
	+ bbdd_buf,
	+ bbdd_one,
	+ bbdd_zero
	+};
	+
	+typedef enum bbdd_op bbdd_op_t;
	+
	+const std::vector<std::string> bbdd_op_s = {
	+ "none", "and", "or", "nand", "nor", "xor", "xnor", "inv",
	+ "not and", "and not", "not or", "or not", "buf", "one", "zero"};
	+
	diff --git a/include/chain_variable_ordering.hpp b/include/chain_variable_ordering.hpp
	new file mode 100644
	index 0000000..de47cad
	--- /dev/null
	+++ b/include/chain_variable_ordering.hpp
	@@ -0,0 +1,153 @@
	+// Copyright 2025 Oliver Theimer
	+#pragma once
	+
	+#include <algorithm>
	+#include <cassert>
	+#include <cstdint>
	+#include <cstdio>
	+#include <cstdlib>
	+#include <fstream>
	+#include <iostream>
	+#include <random>
	+#include <vector>
	+
	+#define POS(in, cvo) (*cvo)[in % cvo->size()].pos
	+#define VAR(pos, cvo) (*cvo)[pos].in
	+
	+typedef uint32_t cvo_index_t;
	+
	+enum cvo_init_type {
	+ cvo_none,
	+ cvo_random,
	+ cvo_even,
	+ cvo_even_reversed,
	+ cvo_input
	+};
	+typedef enum cvo_init_type cvo_init_t;
	+
	+/**
	+ * @class cvo_pair_t
	+ * @brief stores primary and secondary variable
	+ *
	+ */
	+struct cvo_pair_t {
	+ cvo_index_t pv;
	+ cvo_index_t sv;
	+};
	+
	+/**
	+ * @class cvo_element_t
	+ * @brief stores the of the position of the current variable in the chainvariable ordering and the input at the current position
	+ *
	+ */
	+struct cvo_element_t {
	+ // references the position of the variable in ordering
	+ cvo_index_t pos;
	+ // references the input at this element index
	+ cvo_index_t in;
	+};
	+typedef std::vector<cvo_element_t> cvo_t;
	+
	+/**
	+ * @brief dumps the current ordering to stdout in the format IN: followed by the
	+ * indices of the inputs and pos followed by the positions of the inputs in
	+ * ascending order
	+ *
	+ * @param cvo chain variable ordering that should be dumped
	+ */
	+inline void dump_ordering(cvo_t *cvo) {
	+ std::cout << "IN: \|";
	+ for (uint32_t i = 0; i < cvo->size(); i++) {
	+ printf(" %d \|", (*cvo)[i].in);
	+ }
	+ std::cout << "\nPOS: \|";
	+ for (uint32_t i = 0; i < cvo->size(); i++) {
	+ printf(" %d \|", (*cvo)[i].pos);
	+ }
	+ std::cout << "\n";
	+}
	+
	+/**
	+ * @brief appends the chain variable ordering split into two comma seperated
	+ * lists into the given file. The first list represents the ordering of the
	+ * input, the second list prints the position of the input at the current index
	+ *
	+ * @param cvo chain variable ordering that should be printed
	+ * @param file outputfile in which the output should be appended
	+ */
	+inline void dump_ordering(cvo_t *cvo, std::ofstream &file) {
	+ file << std::to_string((*cvo)[0].in);
	+ for (uint32_t i = 1; i < cvo->size(); i++) {
	+ file << "," << std::to_string((*cvo)[i].in);
	+ }
	+ file << ";" << std::to_string((*cvo)[0].pos);
	+ for (uint32_t i = 1; i < cvo->size(); i++) {
	+ file << "," << std::to_string((*cvo)[i].pos);
	+ }
	+}
	+
	+/**
	+ * @brief initialise ordering based on a strategy.
	+ *
	+ * @param inputs list of input variables
	+ * @param cvo pointer to chain variable ordering that should be initialised
	+ * @param opt option of the initial ordering strategy. The options are cvo_none,
	+ * cvo_even_reversed, cvo_even, cvo_input
	+ * @param input_order if the cvo_inout option is given, the ordering given by
	+ * this parameter is used to initialize the ordering
	+ */
	+inline void init_ordering(
	+ std::vector<uint64_t> inputs, cvo_t *&cvo, cvo_init_t opt,
	+ std::vector<cvo_index_t> input_order = std::vector<cvo_index_t>()) {
	+ cvo = new std::vector<cvo_element_t>(inputs.size());
	+ std::vector<uint32_t> new_order;
	+ if (opt == cvo_none) {
	+ for (uint32_t i = 0; i < inputs.size(); i++) {
	+ uint32_t input = inputs[i];
	+ (*cvo)[i].in = input;
	+ (*cvo)[input % inputs.size()].pos = i;
	+ }
	+ } else if (opt == cvo_random) {
	+ for (uint32_t i = 0; i < inputs.size(); i++) {
	+ new_order.push_back(i + 2);
	+ }
	+ unsigned seed = time(NULL);
	+ printf("seed: %d\n", seed);
	+ std::shuffle(new_order.begin(), new_order.end(),
	+ std::default_random_engine(seed));
	+ for (uint32_t i = 0; i < new_order.size(); i++) {
	+ (*cvo)[i].in = new_order[i];
	+ (*cvo)[new_order[i] % cvo->size()].pos = i;
	+ }
	+ } else if (opt == cvo_even \|\| opt == cvo_even_reversed) {
	+ assert(inputs.size() % 2 == 0);
	+ for (uint32_t i = 0; i < inputs.size() / 2; i++) {
	+ uint32_t input1 = inputs[i];
	+ uint32_t input2 = inputs[i + (inputs.size() / 2)];
	+ (cvo)[(2 i)].in = input1;
	+ (cvo)[input1 % inputs.size()].pos = (2 i);
	+ (cvo)[(2 i) + 1].in = input2;
	+ (cvo)[input2 % inputs.size()].pos = (2 i) + 1;
	+ }
	+ if (opt == cvo_even_reversed) {
	+ std::reverse((cvo).begin(), (cvo).end());
	+ for (uint32_t i = 0; i < (*cvo).size(); i++) {
	+ (cvo)[(cvo)[i].in % cvo->size()].pos = i;
	+ }
	+ }
	+ } else if (opt == cvo_input) {
	+ assert(inputs.size() == input_order.size());
	+ for (uint32_t i = 0; i < input_order.size(); i++) {
	+ (*cvo)[i].in = input_order[i];
	+ (*cvo)[input_order[i] % cvo->size()].pos = i;
	+ }
	+ }
	+ dump_ordering(cvo);
	+ // correctness check
	+ for (uint32_t i = 0; i < cvo->size(); i++) {
	+ assert((cvo)[(cvo)[(i + 2) % cvo->size()].pos].in == i + 2);
	+ }
	+#ifdef DEBUG
	+ dump_ordering(cvo);
	+#endif
	+}
	diff --git a/include/computed_table.hpp b/include/computed_table.hpp
	new file mode 100644
	index 0000000..9a76128
	--- /dev/null
	+++ b/include/computed_table.hpp
	@@ -0,0 +1,28 @@
	+// Copyright 2025 Oliver Theimer
	+#pragma once
	+
	+#include <cstddef>
	+#include "./bbdd_node.hpp"
	+#include "./bbdd_types.hpp"
	+
	+struct merge_key {
	+ bbdd_node_t f, g;
	+ bbdd_op_t op;
	+
	+ bool operator==(const merge_key &key) const {
	+ return f->cvo_lvl.pv == key.f->cvo_lvl.pv &&
	+ f->cvo_lvl.sv == key.f->cvo_lvl.sv &&
	+ f->neq_child == key.f->neq_child && f->eq_child == key.f->eq_child &&
	+ g->cvo_lvl.pv == key.g->cvo_lvl.pv &&
	+ g->cvo_lvl.sv == key.g->cvo_lvl.sv &&
	+ g->neq_child == key.g->neq_child && g->eq_child == key.g->eq_child &&
	+ op == key.op;
	+ }
	+};
	+
	+struct merge_hash {
	+ std::size_t operator()(const merge_key &k) const {
	+ return std::hash<int>()(k.f->index) ^ (std::hash<int>()(k.g->index) << 1) ^
	+ (std::hash<char>()(k.op) << 2);
	+ }
	+};
	diff --git a/include/extend_table.hpp b/include/extend_table.hpp
	new file mode 100644
	index 0000000..ac93063
	--- /dev/null
	+++ b/include/extend_table.hpp
	@@ -0,0 +1,19 @@
	+// Copyright 2025 Oliver Theimer
	+#pragma once
	+
	+#include <cstddef>
	+#include "./bbdd_types.hpp"
	+
	+struct extend_key {
	+ node_index_t f, g;
	+
	+ bool operator==(const extend_key &key) const {
	+ return f == key.f && g == key.g;
	+ }
	+};
	+
	+struct extend_hash {
	+ std::size_t operator()(const extend_key &k) const {
	+ return std::hash<int>()(k.f) ^ (std::hash<int>()(k.g) << 1);
	+ }
	+};
	diff --git a/include/unique_table.hpp b/include/unique_table.hpp
	new file mode 100644
	index 0000000..dd358de
	--- /dev/null
	+++ b/include/unique_table.hpp
	@@ -0,0 +1,1249 @@
	+// Copyright 2025 Oliver Theimer
	+#pragma once
	+#include <algorithm>
	+#include <cassert>
	+#include <climits>
	+#include <cmath>
	+#include <cstdint>
	+#include <cstdio>
	+#include <fstream>
	+#include <iostream>
	+#include <string>
	+#include <unordered_map>
	+#include <vector>
	+
	+#include "./bbdd_node.hpp"
	+#include "./bbdd_types.hpp"
	+#include "./chain_variable_ordering.hpp"
	+#include "./computed_table.hpp"
	+#include "./extend_table.hpp"
	+
	+// idea from CUDD package
	+#define SIZEOF_VOID_P 8
	+#define SIZEOF_INT 4
	+#if SIZEOF_VOID_P == 8 && SIZEOF_INT == 4
	+typedef uint32_t bbdd_halfword_t;
	+#else
	+typedef uint16_t bbdd_halfword_t;
	+#endif
	+
	+#define REF(n) entries[n].ref
	+#define LEVEL(n) entries[n].node.cvo_lvl
	+#define EQ(n) entries[n].node.eq_child
	+#define NEQ(n) entries[n].node.neq_child
	+#define INDEX(n) entries[n].node.index
	+#define NEXT(n) entries[n].next
	+#define NEXT_ENTRY(n) entries[n->next]
	+
	+typedef uint32_t node_index_t;
	+
	+/**
	+ * @class variable_relation_t
	+ * @brief struct used to store information about a bbdd to generate its truth
	+ * table
	+ *
	+ */
	+struct variable_relation_t {
	+ node_index_t pv;
	+ node_index_t sv;
	+ bool eq;
	+};
	+
	+/**
	+ * @class table_entry_t
	+ * @brief struct that stored a single entry of the hash table
	+ *
	+ */
	+struct table_entry_t {
	+ bbdd_node_t node;
	+ bbdd_halfword_t next;
	+ bbdd_halfword_t ref;
	+};
	+
	+/**
	+ * @class output_map_t
	+ * @brief struct that maps a bbdd root node to a human readable string
	+ *
	+ */
	+struct output_map_t {
	+ std::string output;
	+ bbdd_node_t *bbdd;
	+};
	+
	+class Unique_table {
	+ enum return_codes { SUCCESS, OUT_OF_MEMORY, TABLE_FULL };
	+
	+#define NODE(n) entries[n].node
	+#define ENTRY(n) entries[n]
	+
	+private:
	+ table_entry_t *entries;
	+ node_index_t free_pos;
	+ uint32_t capacity;
	+ std::string module_name;
	+ std::vector<node_index_t> free_slots;
	+
	+ /**
	+ * @brief swap two adhacent variables in variable ordering
	+ *
	+ * @param pos_b position of the first variable
	+ * @param pos_c position of the second variable
	+ */
	+ void swap_variable_order(node_index_t pos_b, node_index_t pos_c) {
	+ assert(pos_b + 1 == pos_c);
	+ node_index_t temp = (*cvo)[pos_b].in;
	+ (cvo)[pos_b].in = (cvo)[pos_c].in;
	+ (*cvo)[pos_c].in = temp;
	+ (cvo)[(cvo)[pos_b].in % num_inputs].pos = pos_b;
	+ (cvo)[(cvo)[pos_c].in % num_inputs].pos = pos_c;
	+ }
	+
	+ /**
	+ * @brief recursive helper function to count the number of nodes in bbdd
	+ *
	+ * @param node bbdd root node whose size should be evaluated
	+ * @return number of nodes in subgraph denoted by root node
	+ */
	+ uint32_t get_number_nodes_recursive(bbdd_node_t *node) {
	+ if (IS_TERM(node->index) \|\| MARKED(node)) {
	+ return 0;
	+ }
	+ SET_MARKED(node);
	+ uint32_t neq_size = get_number_nodes_recursive(get_node_p(node->neq_child));
	+ uint32_t eq_size = get_number_nodes_recursive(get_node_p(node->eq_child));
	+ return (neq_size + eq_size) + 1;
	+ }
	+
	+ /**
	+ * @brief recursive helper function to dump a bbdd into a dot file format
	+ *
	+ * @param file dot file in which the output should be written to
	+ * @param node root node whose subgraph should be printed into dot file format
	+ * @return node index used for recursive print
	+ */
	+ node_index_t recursive_dump_dot(std::ofstream &file, bbdd_node_t *node) {
	+ if (IS_TERM(node->index) \|\| MARKED(node)) {
	+ return node->index;
	+ }
	+ if (node->cvo_lvl.sv != INT_MAX) {
	+ file << "\n\t" << (GET_INDEX(node)) << " [label=\"" << node->ref << ""
	+ << (GET_INDEX(node)) << ": " << node->cvo_lvl.pv << ","
	+ << node->cvo_lvl.sv << "\"]\n";
	+ } else {
	+ file << "\n\t" << (GET_INDEX(node)) << " [label=\"" << node->ref << ""
	+ << (GET_INDEX(node)) << ": " << node->cvo_lvl.pv << "," << 1
	+ << "\"]\n";
	+ }
	+ SET_MARKED(node);
	+ recursive_dump_dot(file, get_node_p(node->neq_child));
	+ recursive_dump_dot(file, get_node_p(node->eq_child));
	+ file << "\t" << (GET_INDEX(node)) << " -- " << node->neq_child
	+ << "[style=\"dashed\"]\n";
	+ //<< "[style=\"dashed\", label=<<FONT POINT-SIZE=\"14\">≠</FONT>>]\n";
	+ file << "\t" << (GET_INDEX(node)) << " -- " << node->eq_child << "\n";
	+ return (GET_INDEX(node));
	+ }
	+
	+ /**
	+ * @brief return the ith bit of an integer
	+ *
	+ * @param integer integer from which the bit should be retrieved
	+ * @param bits number of bits in the integer
	+ * @param index position of bit that should be retrieved
	+ * @return boolean rather the bit is high (true) or low (false)
	+ */
	+ bool get_ith_bit(node_index_t integer, node_index_t bits, uint8_t index) {
	+ return integer & (1 << ((bits - 1) - index));
	+ }
	+
	+ /**
	+ * @brief helper function that is used to collect truth table entries based on
	+ * a variable relation list
	+ *
	+ * @param var_rel vector of variable relation entries retrieved from
	+ * traversing the bbdd
	+ * @param inputs number of inputs to the truth table
	+ * @param tt vector of truth table values that should be filled by this
	+ * function
	+ * @param value that should be inserted into the truth table
	+ */
	+ void insert_tt_value(std::vector<variable_relation_t> var_rel,
	+ node_index_t inputs, std::vector<bool> &tt, bool value) {
	+ if (!value) {
	+ return;
	+ }
	+ for (variable_relation_t rel : var_rel) {
	+#ifdef DEBUG_TABLE
	+ printf("%d %s %d\n", rel.pv, rel.eq ? "=" : "!=", rel.sv);
	+#endif
	+ }
	+ for (uint32_t i = 0; i < tt.size(); i++) {
	+ bool insert = true;
	+ for (variable_relation_t rel : var_rel) {
	+ if (rel.eq) {
	+ if (rel.sv == INT_MAX) {
	+ if (!get_ith_bit(i, inputs, rel.pv - 2)) {
	+ insert = false;
	+ }
	+ } else if (get_ith_bit(i, inputs, rel.pv - 2) !=
	+ get_ith_bit(i, inputs, rel.sv - 2)) {
	+ insert = false;
	+ }
	+ } else {
	+ if (rel.sv == INT_MAX) {
	+ if (get_ith_bit(i, inputs, rel.pv - 2)) {
	+ insert = false;
	+ }
	+ } else if (get_ith_bit(i, inputs, rel.pv - 2) ==
	+ get_ith_bit(i, inputs, rel.sv - 2)) {
	+ insert = false;
	+ }
	+ }
	+ }
	+ if (insert && value) {
	+#ifdef DEBUG_TABLE
	+ printf("INSERTED %d at : %d %d%d%d%d\n", value, i,
	+ get_ith_bit(i, inputs, 3), get_ith_bit(i, inputs, 2),
	+ get_ith_bit(i, inputs, 1), get_ith_bit(i, inputs, 0));
	+#endif
	+ tt[i] = value;
	+ }
	+ }
	+ }
	+
	+ /**
	+ * @brief helper function that is used to recursively fill the truth table of
	+ * the target bbdd
	+ *
	+ * @param node bbdd root node for which the truth table should be created
	+ * @param var_rel helper data structure that stores the relation between the
	+ * inputs
	+ * @param inputs number of inputs to be considered for the truth table
	+ * @param tt truth table data structure that should be filled by this function
	+ */
	+ void recursive_dump_tt(bbdd_node_t *node,
	+ std::vector<variable_relation_t> var_rel,
	+ node_index_t inputs, std::vector<bool> &tt) {
	+ std::vector<variable_relation_t> neq_rel = var_rel;
	+ std::vector<variable_relation_t> eq_rel = var_rel;
	+ if (IS_TERM(node->index)) {
	+ return;
	+ }
	+ neq_rel.push_back({node->cvo_lvl.pv, node->cvo_lvl.sv, false});
	+ eq_rel.push_back({node->cvo_lvl.pv, node->cvo_lvl.sv, true});
	+ if (node->neq_child == 1) {
	+ insert_tt_value(neq_rel, inputs, tt, true);
	+ }
	+ if (node->eq_child == 1) {
	+ insert_tt_value(eq_rel, inputs, tt, true);
	+ }
	+ recursive_dump_tt(get_node_p(node->neq_child), neq_rel, inputs, tt);
	+ recursive_dump_tt(get_node_p(node->eq_child), eq_rel, inputs, tt);
	+ }
	+
	+ /**
	+ * @brief recursive helper function that recursively writes the bbdd into a
	+ * blif file format uses only multiplexer and xor nodes
	+ *
	+ * @param blif_file output filestream in which the bbdd should be written to
	+ * @param node root node to the bbdd that should be converted
	+ * @param signal_map signal mal between internal indices and human readable
	+ * strings
	+ * @param output helper variable rather the current node is a output node or
	+ * internal node
	+ * @return index of the current bbdd node
	+ */
	+ uint32_t write_blif_recursive(std::ofstream &blif_file, bbdd_node_t *node,
	+ std::vector<std::string> signal_map,
	+ bool output) {
	+ if (IS_TERM(node->index) \|\| MARKED(node)) {
	+ return GET_INDEX(node);
	+ }
	+ SET_MARKED(node);
	+ uint32_t left_child = write_blif_recursive(
	+ blif_file, get_node_p(node->neq_child), signal_map, false);
	+ uint32_t right_child = write_blif_recursive(
	+ blif_file, get_node_p(node->eq_child), signal_map, false);
	+ if (node->cvo_lvl.sv != INT_MAX) {
	+ blif_file << ".names " << signal_map[node->cvo_lvl.pv - 2].c_str() << " "
	+ << signal_map[node->cvo_lvl.sv - 2].c_str() << " "
	+ << std::to_string(GET_INDEX(node)) << "s\n";
	+ } else {
	+ blif_file << ".names " << signal_map[node->cvo_lvl.pv - 2].c_str()
	+ << " $true " << std::to_string(GET_INDEX(node)) << "s\n";
	+ }
	+ blif_file << "00 1\n11 1\n";
	+ blif_file << ".names " << std::to_string(GET_INDEX(node)) << "s ";
	+ if (IS_TERM(right_child)) {
	+ if (right_child == 0) {
	+ blif_file << "$false ";
	+ } else {
	+ blif_file << "$true ";
	+ }
	+ } else {
	+ blif_file << std::to_string(right_child);
	+ }
	+ blif_file << " ";
	+ if (IS_TERM(left_child)) {
	+ if (left_child == 0) {
	+ blif_file << "$false ";
	+ } else {
	+ blif_file << "$true ";
	+ }
	+ } else {
	+ blif_file << std::to_string(left_child);
	+ }
	+ blif_file << " ";
	+ if (!output) {
	+ blif_file << std::to_string(GET_INDEX(node)) << "\n";
	+ }
	+ if (!output) {
	+ blif_file << "0-1 1\n11- 1\n";
	+ }
	+ return GET_INDEX(node);
	+ }
	+
	+ /**
	+ * @brief recursive helper function that dumps the bbdd node into a blif file
	+ * format and only uses NEMS specific muxxor nodes
	+ *
	+ * @param blif_file output file in which should the design by written to
	+ * @param node root node of the bbdd that should be dumped
	+ * @param signal_map map between the internal indices and human readable
	+ * string used for the design inputs
	+ * @param output boolean that represents if the current bbdd node is an output
	+ * or not
	+ * @return bbdd node index of the current bbdd node only used during recursion
	+ */
	+ uint32_t write_blif_recursive_muxxor(std::ofstream &blif_file,
	+ bbdd_node_t *node,
	+ std::vector<std::string> signal_map,
	+ bool output) {
	+ if (IS_TERM(node->index) \|\| MARKED(node)) {
	+ return GET_INDEX(node);
	+ }
	+ SET_MARKED(node);
	+ // format a, b, in0, in1, out
	+ // 00-1 1
	+ // 011- 1
	+ // 101- 1
	+ // 11-1 1
	+ uint32_t left_child = write_blif_recursive_muxxor(
	+ blif_file, get_node_p(node->neq_child), signal_map, false);
	+ uint32_t right_child = write_blif_recursive_muxxor(
	+ blif_file, get_node_p(node->eq_child), signal_map, false);
	+ // MUXXOR part
	+ std::string a, b, in0, in1, out;
	+ a = signal_map[node->cvo_lvl.pv - 2].c_str();
	+ if (node->cvo_lvl.sv != INT_MAX) {
	+ b = signal_map[node->cvo_lvl.sv - 2].c_str();
	+ } else {
	+ b = "$true";
	+ }
	+ if (IS_TERM(right_child)) {
	+ in1 = right_child == 0 ? "$false" : "$true";
	+ } else {
	+ in1 = std::to_string(right_child);
	+ }
	+ if (IS_TERM(left_child)) {
	+ in0 = left_child == 0 ? "$false" : "$true";
	+ } else {
	+ in0 = std::to_string(left_child);
	+ }
	+ blif_file << ".names " << a << " " << b << " " << in0 << " " << in1 << " ";
	+ if (!output) {
	+ blif_file << std::to_string(GET_INDEX(node)) << "\n";
	+ // blif_file << "0-1 1\n11- 1\n";
	+ blif_file << "00-1 1\n011- 1\n101- 1\n11-1 1\n";
	+ }
	+ return GET_INDEX(node);
	+ }
	+
	+public:
	+#ifdef CACHE_STATS
	+ struct cache_stats_t {
	+ uint32_t hits;
	+ uint32_t inserts;
	+ uint32_t misses;
	+ uint32_t chain;
	+ uint32_t current_chain;
	+ uint32_t extend_hits;
	+ uint32_t extend_lookups;
	+ uint32_t merge_hits;
	+ uint32_t merge_lookups;
	+ };
	+ cache_stats_t cache_stats;
	+#endif
	+
	+ std::vector<output_map_t> output_map;
	+ std::vector<std::string> signal_map;
	+ cvo_t *cvo;
	+ uint32_t num_inputs;
	+ std::unordered_map<merge_key, node_index_t, merge_hash> computed_table;
	+ std::unordered_map<extend_key, bbdd_node_ppair_t, extend_hash> extend_table;
	+ Unique_table() {}
	+
	+ /**
	+ * @brief return bbdd node based on given index
	+ *
	+ * @param index for which the bbdd node should be retrieved
	+ * @return bbdd node at index
	+ */
	+ bbdd_node_t get_node(node_index_t index) { return entries[index].node; }
	+ /**
	+ * @brief return pointer to node at given index
	+ *
	+ * @param index for which the pointer to the bbdd node should be retrieved
	+ * @return pointer to bbdd node at index
	+ */
	+ bbdd_node_t *get_node_p(node_index_t index) { return &entries[index].node; }
	+
	+ /**
	+ * @brief initialize cvo based on input list, cvo initial ordering strategy
	+ * and optional ordering that should be used
	+ *
	+ * @param inputs list of inputs that should are going to be used in design
	+ * @param cvo_opt chain variable ordering initial ordering strategy. Currently
	+ * strategies available: cvo_none, cvo_even, cvo_even_reversed, cvo_random,
	+ * cvo_input
	+ * @param input_cvo list of initial ordering only considered when cvo_opt is
	+ * cvo_input
	+ */
	+ void
	+ init_cvo(std::vector<uint64_t> inputs, cvo_init_t cvo_opt,
	+ std::vector<node_index_t> input_cvo = std::vector<node_index_t>()) {
	+ cvo = reinterpret_cast<cvo_t *>(malloc(sizeof(cvo_t)));
	+ num_inputs = inputs.size();
	+ init_ordering(inputs, cvo, cvo_opt, input_cvo);
	+ }
	+
	+ /**
	+ * @brief initial signal map with a list of input name strings. Only required
	+ * if output should be written to blif file
	+ *
	+ * @param input_names list of input name strings
	+ */
	+ void init_signal_map(std::vector<std::string> input_names) {
	+ for (std::string input : input_names) {
	+ this->signal_map.emplace_back(input);
	+ }
	+ }
	+
	+ /**
	+ * @brief Clear cache that is used during merge operations
	+ */
	+ void clear_computed_table() { computed_table.clear(); }
	+
	+ /**
	+ * @brief Clear cache that is used during extend operations
	+ */
	+ void clear_extend_table() { extend_table.clear(); }
	+
	+ /**
	+ * @brief Get next free position in the hash table
	+ *
	+ * @return index of next free position
	+ */
	+ uint32_t get_free_pos() { return free_pos; }
	+
	+ /**
	+ * @brief initialise has table that stores the node information
	+ *
	+ * @param init_node_count capacity of the hash table
	+ * @param module_name name of the module that is represented by the bbdds,
	+ * only required for writing the design into blif file format
	+ * @return status code depending if the operations was succesful
	+ */
	+ int8_t init_table(uint64_t init_node_count, std::string module_name) {
	+ if (init_node_count > pow(2, 31)) {
	+ std::cerr << "[ERROR] init table: node count is too large\n";
	+ return -1;
	+ }
	+ this->module_name = module_name;
	+ entries = reinterpret_cast<table_entry_t *>(
	+ malloc(sizeof(table_entry_t) * init_node_count));
	+ if (entries == NULL) {
	+ std::cerr << "[ERROR] init failed, because out of memeory\n";
	+ return OUT_OF_MEMORY;
	+ }
	+ capacity = init_node_count;
	+ for (node_index_t i = 0; i < init_node_count; i++) {
	+ // init with zero
	+ LEVEL(i).pv = 0;
	+ LEVEL(i).sv = 0;
	+ EQ(i) = 0;
	+ NEQ(i) = 0;
	+ NEXT(i) = 0;
	+ REF(i) = 0;
	+ INDEX(i) = 0;
	+ }
	+ LEVEL(0).pv = INT_MAX;
	+ LEVEL(0).sv = INT_MAX;
	+ INDEX(0) = 0;
	+ // Constant 1
	+ LEVEL(1).pv = INT_MAX;
	+ LEVEL(1).sv = INT_MAX;
	+ INDEX(1) = 1;
	+ REF(1) = 1;
	+ // first empty space after constants
	+ free_pos = 2;
	+#ifdef CACHE_STATS
	+ cache_stats.hits = 0;
	+ cache_stats.inserts = 0;
	+ cache_stats.misses = 0;
	+ cache_stats.chain = 0;
	+ cache_stats.current_chain = 0;
	+ cache_stats.extend_lookups = 0;
	+ cache_stats.extend_hits = 0;
	+ cache_stats.merge_lookups = 0;
	+ cache_stats.merge_hits = 0;
	+#endif
	+ return SUCCESS;
	+ }
	+
	+ /**
	+ * @brief free hash table
	+ */
	+ void free_table() { free(entries); }
	+
	+ /**
	+ * @brief insert bbdd node into the hash table
	+ *
	+ * @param node_t bbdd node template that should be inserted
	+ * @return pointer to bbdd node in the hash table
	+ */
	+ bbdd_node_t *insert_node(bbdd_node_template_t node_t) {
	+#ifdef CACHE_STATS
	+ cache_stats.inserts++;
	+#endif
	+ assert(node_t.cvo_lvl.sv == INT_MAX \|\|
	+ POS(node_t.cvo_lvl.pv, cvo) < POS(node_t.cvo_lvl.sv, cvo));
	+ node_index_t hash = hash_node(node_t, capacity);
	+#ifdef DEBUG_TABLE
	+ printf("[INFO] INSERT: trying (%d, %d) %d %d hash: %d\n", node_t.cvo_lvl.pv,
	+ node_t.cvo_lvl.sv, node_t.neq_child, node_t.eq_child, hash);
	+#endif
	+ if (free_pos >= capacity && free_slots.empty()) {
	+ // resize not implemented yet
	+ std::cerr << "[ERROR] Unique Table is full resize not implemented yet";
	+ int count = 0;
	+ for (int i = 0; i < capacity; i++) {
	+ if (entries[i].ref == 0) {
	+ count++;
	+ }
	+ }
	+ assert(false);
	+ return 0;
	+ }
	+ table_entry_t *entry = &entries[hash];
	+ node_index_t chain_i = -1;
	+ if (entry->ref != 0) {
	+ // there is already a node with this hash
	+ chain_i = entry->ref;
	+#ifdef CACHE_STATS
	+ cache_stats.current_chain = 0;
	+#endif
	+ while (true) {
	+ // see if that is the node we currently want to insert
	+ if (node_eq(entries[chain_i].node, node_t)) {
	+#ifdef DEBUG_TABLE
	+ std::cout << "[INFO] INSERT: node hit ";
	+ dump_node(&entries[chain_i].node);
	+ std::cout << "\n";
	+#endif
	+#ifdef CACHE_STATS
	+ cache_stats.hits++;
	+#endif
	+ return &entries[chain_i].node;
	+ }
	+ // if there is no more node in the chain break and insert at that
	+ // position
	+ if (NEXT(chain_i) == 0) {
	+#ifdef CACHE_STATS
	+ if (cache_stats.current_chain > cache_stats.chain) {
	+ cache_stats.chain = cache_stats.current_chain;
	+ }
	+#endif
	+ break;
	+ }
	+ chain_i = NEXT(chain_i);
	+#ifdef CACHE_STATS
	+ cache_stats.current_chain++;
	+#endif
	+ }
	+ }
	+ node_index_t insert_pos;
	+ if (free_slots.empty()) {
	+ insert_pos = free_pos;
	+ free_pos++;
	+ } else {
	+ insert_pos = free_slots.back();
	+ free_slots.pop_back();
	+ }
	+ // insert node
	+ bbdd_node_t node = {0, insert_pos, node_t.cvo_lvl, node_t.neq_child,
	+ node_t.eq_child};
	+ get_node_p(node_t.eq_child)->ref++;
	+ get_node_p(node_t.neq_child)->ref++;
	+ NODE(insert_pos) = node;
	+ // extend chain
	+ if (chain_i != -1) {
	+#ifdef DEBUG_TABLE
	+ std::cout << "[INFO] INSERT: extending chain at " << chain_i << " ";
	+ dump_node(&NODE(insert_pos));
	+ std::cout << "\n";
	+#endif
	+ entries[chain_i].next = insert_pos;
	+ } else {
	+ entry->ref = insert_pos;
	+#ifdef DEBUG_TABLE
	+ printf("[INFO] INSERT: no chain ");
	+ dump_node(&NODE(insert_pos));
	+ std::cout << "\n";
	+#endif
	+ }
	+#ifdef CACHE_STATS
	+ cache_stats.misses++;
	+#endif
	+ return &NODE(insert_pos);
	+ }
	+
	+ /**
	+ * @brief delte bbdd node from the hash table
	+ *
	+ * @param node pointer to bbdd node that should be deleted from the hash table
	+ */
	+ void delete_node(bbdd_node_t *node) {
	+ node_index_t hash = hash_node(*node, capacity);
	+ // assert(entries[hash].ref != 0);
	+ node_index_t ref = entries[hash].ref;
	+ if (ref == node->index) {
	+ // not part of a chain
	+#ifdef DEBUG_TABLE
	+ printf("[INFO] DELETE: no chain replacing %d with %d\n", node->index,
	+ entries[ref].next);
	+#endif
	+ entries[hash].ref = entries[ref].next;
	+ free_slots.emplace_back(node->index);
	+ } else {
	+ // part of a chain get first element
	+ table_entry_t *chain_entry = &entries[entries[hash].ref];
	+ for (int i = 0; i < capacity; i++) {
	+ if (node_eq(entries[chain_entry->next].node, *node)) {
	+ // remove node from chain
	+#ifdef DEBUG_TABLE
	+ printf("[INFO] DELETE: chain replacing at %d with %d\n",
	+ chain_entry->node.index, entries[node->index].next);
	+#endif
	+ chain_entry->next = entries[node->index].next;
	+ entries[node->index].next = 0;
	+ entries[node->index].node = {0, 0, {0, 0}, 0, 0};
	+ free_slots.emplace_back(node->index);
	+ return;
	+ }
	+ chain_entry = &entries[chain_entry->next];
	+ }
	+ dump_table();
	+ std::cout << "[ERROR] Node Node found: " << node->index << "\n";
	+ dump_node(node);
	+ std::cout << " with hash " << hash << "\n";
	+ fflush(stdout);
	+ assert(false && "node not found");
	+ }
	+ }
	+
	+ /**
	+ * @brief add output map from bbdd node pointer to a string, used for
	+ * displaying and blif file purposes
	+ *
	+ * @param output string to human readable output
	+ * @param bbdd root bbdd node that represents output function
	+ */
	+ void add_output(std::string output, bbdd_node_t *bbdd) {
	+ output_map_t map = {output, bbdd};
	+ bbdd->ref++;
	+ output_map.emplace_back(map);
	+ }
	+
	+ /**
	+ * @brief recursively clears marks from bbdd
	+ *
	+ * @param bbdd root bbdd node for which all marks should be cleared
	+ */
	+ void clear_marks(bbdd_node_t *bbdd) {
	+ if (IS_TERM(bbdd->index)) {
	+ return;
	+ }
	+ CLEAR_MARKED(bbdd);
	+ clear_marks(get_node_p(bbdd->neq_child));
	+ clear_marks(get_node_p(bbdd->eq_child));
	+ }
	+
	+ /**
	+ * @brief dump hash table entries, only entries with data are printed
	+ */
	+ void dump_table() {
	+ for (uint64_t i = 0; i < free_pos; i++) {
	+ printf("Hash: %6d Ref: %3d Next: %4d Node: ",
	+ hash_node(entries[i].node, capacity), entries[i].ref,
	+ entries[i].next);
	+ dump_node(&entries[i].node);
	+ std::cout << "\n";
	+ }
	+ for (uint64_t i = free_pos; i < capacity; i++) {
	+ if (entries[i].ref != 0) {
	+ printf("i: %3lu Ref: %2d Next: %4d Node: \n", i, entries[i].ref,
	+ entries[i].next);
	+ }
	+ }
	+ }
	+
	+ /**
	+ * @brief dump the truth table of given bbdd
	+ *
	+ * @param output pointer to the root of a bbdd for which the truth table
	+ * should be printed
	+ * @return string of the output tt
	+ */
	+ std::string dump_tt(bbdd_node_t *output) {
	+ std::vector<bool> tt(std::pow(2, this->num_inputs), false);
	+ std::vector<variable_relation_t> var_rel;
	+ recursive_dump_tt(output, var_rel, this->num_inputs, tt);
	+ for (int i = 0; i < tt.size(); i++) {
	+ for (int j = 0; j < this->num_inputs; j++) {
	+ printf("%d", get_ith_bit(i, this->num_inputs, j));
	+ }
	+ printf(" \| %s\n", tt[i] ? "1" : "0");
	+ }
	+ std::string out_string = "";
	+ for (int i = 0; i < tt.size(); i++) {
	+ out_string += tt[i] ? "1" : "0";
	+ }
	+ return out_string;
	+ }
	+
	+ /**
	+ * @brief dump truth table for output string name
	+ *
	+ * @param output name of the output in the output map
	+ * @return string of the tt, empty if output name does not exist in output map
	+ */
	+ std::string dump_tt(std::string output) {
	+ std::printf("Truth table of output %s\n", output.c_str());
	+ for (output_map_t out_map : this->output_map) {
	+ if (out_map.output == output) {
	+ return dump_tt(out_map.bbdd);
	+ }
	+ }
	+ return "";
	+ }
	+
	+ /**
	+ * @brief dump bbdd of given output into a dot file format
	+ *
	+ * @param filename name of the file in which the output will be dumped
	+ * @param output name of the output which should be dumped, dot file only
	+ * consists of terminal node if output name is not in the output map
	+ */
	+ void dump_dot(std::string filename, std::string output) {
	+ std::ofstream dot_file(filename);
	+ dot_file << "graph bbdd {\n";
	+ // terminal nodes
	+ dot_file << "\t0 [shape=square]\n";
	+ dot_file << "\t1 [shape=square]";
	+ bbdd_node_t *root_node;
	+ for (output_map_t map : output_map) {
	+ if (map.output == output) {
	+ root_node = map.bbdd;
	+ break;
	+ }
	+ }
	+ node_index_t root = recursive_dump_dot(dot_file, root_node);
	+ clear_marks(root_node);
	+ dot_file << "\n\t" << free_pos + 1 << " [shape=plaintext, label=\""
	+ << output << "\"]\n";
	+ dot_file << "\t" << free_pos + 1 << " -- " << root_node->index << "\n";
	+ dot_file << "}\n";
	+ }
	+
	+ /**
	+ * @brief dump all bbdd nodes that have a defined output of the module into a
	+ * dot file format
	+ *
	+ * @param filename name in which the design should be printed to
	+ */
	+ void dump_dot(std::string filename) {
	+ std::ofstream dot_file(filename);
	+ dot_file << "graph bbdd {\n";
	+ // terminal nodes
	+ dot_file << "\t0 [shape=square]\n";
	+ dot_file << "\t1 [shape=square]\n";
	+ // insert nodes
	+ for (uint64_t i = 2; i < free_pos; i++) {
	+ table_entry_t entry = entries[i];
	+ if (entry.node.cvo_lvl.sv != INT_MAX) {
	+ dot_file << "\n"
	+ << i << " [label=\"" << entry.node.ref << "\n"
	+ << i << ": " << entry.node.cvo_lvl.pv << ","
	+ << entry.node.cvo_lvl.sv << "\"]";
	+ } else {
	+ dot_file << "\n"
	+ << i << " [label=\"" << entry.node.ref << "\n"
	+ << i << ": " << entry.node.cvo_lvl.pv << ",1" << "\"]";
	+ }
	+ dot_file << "\t" << i << " -- " << entry.node.neq_child
	+ << "[label=<<FONT POINT-SIZE=\"14\">≠</FONT>>, "
	+ "style=\"dashed\"]\n";
	+ dot_file << "\t" << i << " -- " << entry.node.eq_child
	+ << "[label=\"=\"]\n";
	+ }
	+ for (output_map_t map : output_map) {
	+ dot_file << "\n"
	+ << map.output << " [shape=plaintext, label=\"" << map.output
	+ << "\"]";
	+ dot_file << "\t" << map.output << " -- " << map.bbdd->index << "\n";
	+ }
	+ dot_file << "}\n";
	+ }
	+
	+ /**
	+ * @brief same as previous dump_dot function but it uses a signal map that
	+ * maps primary and secondary variables to human readable strings
	+ *
	+ * @param filename in which the design should be written to
	+ * @param signal_map maps indices of primary and secondary variables to human
	+ * readable strings
	+ */
	+ void dump_dot(std::string filename, std::vector<std::string> signal_map) {
	+ std::ofstream dot_file(filename);
	+ dot_file << "graph bbdd {\n";
	+ // terminal nodes
	+ dot_file << "\t0 [shape=square]";
	+ dot_file << "\t1 [shape=square]";
	+ // insert nodes
	+ for (uint64_t i = 2; i < free_pos; i++) {
	+ table_entry_t entry = entries[i];
	+ if (entry.node.ref == 0) {
	+ continue;
	+ }
	+ if (entry.node.cvo_lvl.sv != INT_MAX) {
	+ dot_file << "\n"
	+ << i << " [label=\"" << entry.node.ref << "\n"
	+ << i << ": " << signal_map[entry.node.cvo_lvl.pv - 2] << ","
	+ << signal_map[entry.node.cvo_lvl.sv - 2] << "\"]";
	+ } else {
	+ dot_file << "\n"
	+ << i << " [label=\"" << entry.node.ref << "\n"
	+ << i << ": " << signal_map[entry.node.cvo_lvl.pv - 2] << ",1"
	+ << "\"]";
	+ }
	+ dot_file << "\t" << i << " -- " << entry.node.neq_child
	+ << "[label=<<FONT POINT-SIZE=\"14\">≠</FONT>>, "
	+ "style=\"dashed\"]\n";
	+ dot_file << "\t" << i << " -- " << entry.node.eq_child
	+ << "[label=\"=\"]\n";
	+ }
	+ for (output_map_t map : output_map) {
	+ dot_file << "\n"
	+ << map.output << " [shape=plaintext, label=\"" << map.output
	+ << "\"]";
	+ dot_file << "\t" << map.output << " -- " << map.bbdd->index << "\n";
	+ }
	+ dot_file << "}\n";
	+ }
	+
	+ /**
	+ * @brief dump the current module into blif file format
	+ *
	+ * @param filename name of the file in which the diagrams should be dumped
	+ * into, only outputs are considered that are present in the output map
	+ */
	+ void write_blif(std::string filename) {
	+ std::ofstream blif_file(filename);
	+ blif_file << ".model " + this->module_name + "\n";
	+ blif_file << ".inputs";
	+ for (int i = 0; i < this->signal_map.size(); i++) {
	+ blif_file << " " << this->signal_map[i];
	+ }
	+ blif_file << "\n.outputs";
	+ for (output_map_t output : this->output_map) {
	+ blif_file << " " << output.output;
	+ }
	+ blif_file << "\n.names $true\n1\n";
	+ blif_file << ".names $false\n";
	+ for (output_map_t map : this->output_map) {
	+ if (IS_TERM(map.bbdd->index)) {
	+ if (map.bbdd->index == 0) {
	+ blif_file << ".names " << map.output << "\n";
	+ } else {
	+ blif_file << ".names " << map.output << "\n1\n";
	+ }
	+ } else if (MARKED(map.bbdd)) {
	+ blif_file << ".names " << (GET_INDEX(map.bbdd)) << " " << map.output
	+ << "\n1 1\n";
	+ } else {
	+ // write_blif_recursive(blif_file, map.bbdd, cover.signal_map, true);
	+ // blif_file << map.output << "\n0-1 1\n11- 1\n";
	+ write_blif_recursive_muxxor(blif_file, map.bbdd, signal_map, true);
	+ blif_file << map.output << "\n00-1 1\n011- 1\n101- 1\n11-1 1\n";
	+ }
	+ }
	+ blif_file << ".end\n";
	+ }
	+
	+#ifdef CACHE_STATS
	+ void print_cache_stats() {
	+ printf(
	+ "[INFO] CACHE STATS: inserts: %d, hits: %d, misses %d, max chain: %d\n",
	+ cache_stats.inserts, cache_stats.hits, cache_stats.misses,
	+ cache_stats.chain);
	+ }
	+
	+ void dump_cache_stats(std::string path) {
	+ std::ofstream csv_file(path);
	+ csv_file << "inserts;hits;misses;max_chain;extend_lookups;extend_hits;"
	+ "merge_lookups;merge_hits\n";
	+ csv_file << std::to_string(cache_stats.inserts) << ";"
	+ << std::to_string(cache_stats.hits) << ";"
	+ << std::to_string(cache_stats.misses) << ";"
	+ << std::to_string(cache_stats.chain) << ";"
	+ << std::to_string(cache_stats.extend_lookups) << ";"
	+ << std::to_string(cache_stats.extend_hits) << ";"
	+ << std::to_string(cache_stats.merge_lookups) << ";"
	+ << std::to_string(cache_stats.merge_hits) << "\n";
	+ csv_file.close();
	+ }
	+#endif
	+
	+ /**
	+ * @brief get maximum tree height of a bbdd
	+ *
	+ * @param root root node of bbdd node for which the height should be
	+ * calculated
	+ * @param height intermediate values used for the recursion
	+ * @return maximum height of the current bbdd node to any terminal node
	+ */
	+ uint32_t get_tree_height(bbdd_node_t *root, uint32_t height) {
	+ if (IS_TERM(root->index)) {
	+ return 0;
	+ }
	+ bbdd_node_t *neq = get_node_p(root->neq_child);
	+ bbdd_node_t *eq = get_node_p(root->eq_child);
	+ return std::max(get_tree_height(neq, height) + 1,
	+ get_tree_height(eq, height) + 1);
	+ }
	+
	+ /**
	+ * @brief gets maximum tree height of a bbdd
	+ *
	+ * @param node root node of bbdd node for which the height should be
	+ * calculated
	+ * @return maximum height of the current bbdd node to any terminal node
	+ */
	+ uint32_t get_tree_height(bbdd_node_t *node) {
	+ return get_tree_height(node, 0);
	+ }
	+
	+ /**
	+ * @brief return the maximum tree height of all bbdds registered in the output
	+ * map
	+ *
	+ * @return maximum tree height of all bbdds in the design
	+ */
	+ uint32_t get_max_height() {
	+ uint32_t max_height = -1;
	+ uint32_t current_height;
	+ for (output_map_t out_map : output_map) {
	+ current_height = get_tree_height(out_map.bbdd);
	+ if (current_height > max_height) {
	+ max_height = current_height;
	+ }
	+ }
	+ return max_height;
	+ }
	+
	+ /**
	+ * @brief return the sum of all maximum tree heights of all bbdd nodes that
	+ * have registered an output in the output map
	+ *
	+ * @return sum of all maximum tree heights
	+ */
	+ uint32_t get_total_height() {
	+ uint32_t sum = 0;
	+ for (output_map_t out_map : output_map) {
	+ sum += get_tree_height(out_map.bbdd);
	+ }
	+ return sum;
	+ }
	+
	+ /**
	+ * @brief reorders a bbdd based on two variables that are swapped
	+ *
	+ * @param node root node to the bbdd which should be reordered
	+ * @param b first variable
	+ * @param c second variable
	+ * @return newly created bbdd based on the swapped varaibles inserted into the
	+ * hash table
	+ */
	+ bbdd_node_t reorder_bbdd(bbdd_node_t node, node_index_t b, node_index_t c) {
	+#ifdef DEBUG_REORDER
	+ printf("reorder: ");
	+ dump_node(node);
	+ printf("\n");
	+#endif
	+ if (IS_TERM(node->index)) {
	+ return node;
	+ }
	+ bbdd_node_t *neq_child = get_node_p(node->neq_child);
	+ bbdd_node_t *eq_child = get_node_p(node->eq_child);
	+ bbdd_node_t new_neq, new_eq, new_neq_neq, new_neq_eq, *new_eq_neq,
	+ *new_eq_eq;
	+ bbdd_node_t neq_neq_child, neq_eq_child, eq_neq_child, eq_eq_child;
	+ node_index_t nnn, nne, nen, nee, enn, ene, een, eee;
	+ uint32_t nn_sv, ne_sv, en_sv, ee_sv;
	+ // b no SV
	+ if (node->cvo_lvl.pv == b) {
	+ // c not present in this bbdd
	+ if (node->cvo_lvl.sv != c) {
	+ return node;
	+ }
	+ // NEQ-Child
	+ if (neq_child->cvo_lvl.pv != c) {
	+ new_neq = neq_child;
	+ } else {
	+ new_neq = insert_node({{b, neq_child->cvo_lvl.sv},
	+ neq_child->eq_child,
	+ neq_child->neq_child});
	+ }
	+ // EQ-Child
	+ if (eq_child->cvo_lvl.pv != c) {
	+ new_eq = eq_child;
	+ } else {
	+ new_eq = insert_node({{b, eq_child->cvo_lvl.sv},
	+ eq_child->neq_child,
	+ eq_child->eq_child});
	+ }
	+ assert(new_neq->cvo_lvl.sv == INT_MAX \|\|
	+ POS(new_neq->cvo_lvl.pv, cvo) < POS(new_neq->cvo_lvl.sv, cvo));
	+ assert(new_eq->cvo_lvl.sv == INT_MAX \|\|
	+ POS(new_eq->cvo_lvl.pv, cvo) < POS(new_eq->cvo_lvl.sv, cvo));
	+ assert(POS(c, cvo) < POS(b, cvo));
	+ return insert_node({{c, b}, new_neq->index, new_eq->index});
	+ }
	+ // b SV
	+ if (node->cvo_lvl.sv == b) {
	+ // NEQ-Child
	+ if (neq_child->cvo_lvl.pv == b) {
	+ if (neq_child->cvo_lvl.sv != c) {
	+ nnn = nee = neq_child->eq_child;
	+ nne = nen = neq_child->neq_child;
	+ nn_sv = ne_sv = neq_child->cvo_lvl.sv;
	+ } else {
	+ // c SV in neq_child
	+ neq_neq_child = get_node_p(neq_child->neq_child);
	+ neq_eq_child = get_node_p(neq_child->eq_child);
	+ // full neq neq
	+ if (neq_neq_child->cvo_lvl.pv == c) {
	+ nnn = neq_neq_child->neq_child;
	+ nne = neq_neq_child->eq_child;
	+ nn_sv = neq_neq_child->cvo_lvl.sv;
	+ // c no neq neq PV
	+ } else {
	+ nnn = nne = neq_neq_child->index;
	+ nn_sv = neq_neq_child->cvo_lvl.pv;
	+ }
	+ // full neq eq
	+ if (neq_eq_child->cvo_lvl.pv == c) {
	+ nen = neq_eq_child->neq_child;
	+ nee = neq_eq_child->eq_child;
	+ ne_sv = neq_eq_child->cvo_lvl.sv;
	+ // c no neq eq PV
	+ } else {
	+ nen = nee = neq_eq_child->index;
	+ ne_sv = neq_eq_child->cvo_lvl.pv;
	+ }
	+ }
	+ } else {
	+ // b no PV in neq_child
	+ if (neq_child->cvo_lvl.pv == c) {
	+ // c PV in neq_child
	+ nnn = nen = neq_child->neq_child;
	+ nne = nee = neq_child->eq_child;
	+ nn_sv = ne_sv = neq_child->cvo_lvl.sv;
	+ } else {
	+ nnn = nne = nen = nee = neq_child->index;
	+ nn_sv = ne_sv = neq_child->cvo_lvl.pv;
	+ }
	+ }
	+ // EQ-Child
	+ if (eq_child->cvo_lvl.pv == b) {
	+ if (eq_child->cvo_lvl.sv != c) {
	+ ene = een = eq_child->neq_child;
	+ enn = eee = eq_child->eq_child;
	+ en_sv = ee_sv = eq_child->cvo_lvl.sv;
	+ } else {
	+ // c is sv in eq_child
	+ eq_neq_child = get_node_p(eq_child->neq_child);
	+ eq_eq_child = get_node_p(eq_child->eq_child);
	+ if (eq_neq_child->cvo_lvl.pv == c) {
	+ enn = eq_neq_child->neq_child;
	+ ene = eq_neq_child->eq_child;
	+ en_sv = eq_neq_child->cvo_lvl.sv;
	+ } else {
	+ enn = ene = eq_neq_child->index;
	+ en_sv = eq_neq_child->cvo_lvl.pv;
	+ }
	+ if (eq_eq_child->cvo_lvl.pv == c) {
	+ een = eq_eq_child->neq_child;
	+ eee = eq_eq_child->eq_child;
	+ ee_sv = eq_eq_child->cvo_lvl.sv;
	+ } else {
	+ een = eee = eq_eq_child->index;
	+ ee_sv = eq_eq_child->cvo_lvl.pv;
	+ }
	+ }
	+ } else {
	+ // b is not pv in eq_child
	+ if (eq_child->cvo_lvl.pv == c) {
	+ enn = een = eq_child->neq_child;
	+ ene = eee = eq_child->eq_child;
	+ en_sv = ee_sv = eq_child->cvo_lvl.sv;
	+ } else {
	+ enn = ene = een = eee = eq_child->index;
	+ en_sv = ee_sv = eq_child->cvo_lvl.pv;
	+ }
	+ }
	+ // create new bbdd
	+ // new neq
	+ assert(en_sv == INT_MAX \|\| ene == enn \|\| POS(b, cvo) < POS(en_sv, cvo));
	+ assert(ne_sv == INT_MAX \|\| nen == nee \|\| POS(b, cvo) < POS(ne_sv, cvo));
	+ assert(POS(c, cvo) < POS(b, cvo));
	+ new_neq_neq = insert_node({{b, en_sv}, ene, enn});
	+ new_neq_eq = insert_node({{b, ne_sv}, nen, nee});
	+ new_neq = insert_node({{c, b}, new_neq_neq->index, new_neq_eq->index});
	+ // new eq
	+ assert(nn_sv == INT_MAX \|\| nne == nnn \|\| POS(b, cvo) < POS(nn_sv, cvo));
	+ assert(ee_sv == INT_MAX \|\| een == eee \|\| POS(b, cvo) < POS(ee_sv, cvo));
	+ assert(POS(c, cvo) < POS(b, cvo));
	+ new_eq_neq = insert_node({{b, nn_sv}, nne, nnn});
	+ new_eq_eq = insert_node({{b, ee_sv}, een, eee});
	+ new_eq = insert_node({{c, b}, new_eq_neq->index, new_eq_eq->index});
	+ // new root
	+ assert(POS(node->cvo_lvl.pv, cvo) < POS(c, cvo));
	+ return insert_node(
	+ {{node->cvo_lvl.pv, c}, new_neq->index, new_eq->index});
	+ }
	+ new_neq = reorder_bbdd(get_node_p(node->neq_child), b, c);
	+ new_eq = reorder_bbdd(get_node_p(node->eq_child), b, c);
	+ if (!(node->cvo_lvl.sv == INT_MAX \|\|
	+ POS(node->cvo_lvl.pv, cvo) < POS(node->cvo_lvl.sv, cvo))) {
	+ dump_node(node);
	+ std::cout << "\n";
	+ }
	+ assert(node->cvo_lvl.sv == INT_MAX \|\|
	+ POS(node->cvo_lvl.pv, cvo) < POS(node->cvo_lvl.sv, cvo));
	+ return insert_node({{node->cvo_lvl}, new_neq->index, new_eq->index});
	+ }
	+
	+ /**
	+ * @brief return the total number of nodes in a bbdd
	+ *
	+ * @return total number od nodes in a bbdd
	+ */
	+ uint32_t get_total_number_nodes() {
	+ uint32_t count = 0;
	+ for (output_map_t out_map : output_map) {
	+ count += get_number_nodes_recursive(out_map.bbdd);
	+ }
	+ for (output_map_t out_map : output_map) {
	+ clear_marks(out_map.bbdd);
	+ }
	+ return count;
	+ }
	+
	+ /**
	+ * @brief dump information stored in the output map: name of the output and
	+ * the index of the bbdd node that is the root noddump information stored in
	+ * the output map: name of the output and the index of the bbdd node that is
	+ * the root node for that output
	+ */
	+ void dump_outputs() {
	+ for (output_map_t out_map : output_map) {
	+ printf("Output: %s: ", out_map.output.c_str());
	+ dump_node(out_map.bbdd);
	+ printf("\n");
	+ }
	+ }
	+
	+ /**
	+ * @brief swap two inputs in the variable ordering and reorder bbdd based on the new ordering
	+ *
	+ * @param root root bbdd node that should be reordered after variable swap
	+ * @param b first variable
	+ * @param c second variable
	+ * @return newly created bbdd node based on new variable order
	+ */
	+ bbdd_node_t swap_positions(bbdd_node_t root, node_index_t b,
	+ node_index_t c) {
	+ // assert(POS(b, cvo) + 1 == POS(c, cvo));
	+ assert(b + 1 == c);
	+ node_index_t temp = (*cvo)[b].in;
	+ (cvo)[b].in = (cvo)[c].in;
	+ (*cvo)[c].in = temp;
	+ (cvo)[(cvo)[b].in % num_inputs].pos = b;
	+ (cvo)[(cvo)[c].in % num_inputs].pos = c;
	+ return reorder_bbdd(root, VAR(c, cvo), VAR(b, cvo));
	+ }
	+
	+ /**
	+ * @brief reduce size of the bbdd node based on reduction rules
	+ *
	+ * @param f root node to bbdd that should be reduced
	+ * @return pointer to reduced bbdd
	+ */
	+ bbdd_node_t reduce_bbdd(bbdd_node_t f) {
	+ if (IS_TERM(f->index)) {
	+ return f;
	+ }
	+ bbdd_node_t *child_neq = get_node_p(f->neq_child),
	+ *child_eq = get_node_p(f->eq_child);
	+ bbdd_node_t new_neq, new_eq, new_root;
	+ new_neq = reduce_bbdd(child_neq);
	+ new_eq = reduce_bbdd(child_eq);
	+ if (new_neq->index == new_eq->index) {
	+#ifdef DEBUG_BBDD
	+ printf("[INFO] REDUCE: node %d\n", f->index);
	+#endif
	+ return new_neq;
	+ }
	+ if (!(IS_TERM(new_neq->index)) && !(IS_TERM(new_eq->index)) &&
	+ new_neq->cvo_lvl.pv == new_eq->cvo_lvl.pv &&
	+ new_neq->cvo_lvl.sv == new_eq->cvo_lvl.sv &&
	+ f->cvo_lvl.sv == new_neq->cvo_lvl.pv &&
	+ new_neq->neq_child == new_eq->eq_child &&
	+ new_neq->eq_child == new_eq->neq_child) {
	+ return insert_node({{f->cvo_lvl.pv, new_neq->cvo_lvl.sv},
	+ new_neq->eq_child,
	+ new_neq->neq_child});
	+ }
	+ assert(f->cvo_lvl.sv == INT_MAX \|\|
	+ POS(f->cvo_lvl.pv, cvo) < POS(f->cvo_lvl.sv, cvo));
	+ return insert_node({f->cvo_lvl, new_neq->index, new_eq->index});
	+ }
	+
	+ /**
	+ * @brief swap two adjacent variables in ordering and reorder all bbdd that have a registered output
	+ *
	+ * @param pos_b position of first variable
	+ * @param pos_c position of second variable
	+ */
	+ void swap_all_positions(node_index_t pos_b, node_index_t pos_c) {
	+ node_index_t var_b = (*cvo)[pos_b].in;
	+ node_index_t var_c = (*cvo)[pos_c].in;
	+ swap_variable_order(pos_b, pos_c);
	+ for (uint32_t i = 0; i < output_map.size(); i++) {
	+ output_map[i].bbdd =
	+ reduce_bbdd(reorder_bbdd(output_map[i].bbdd, var_b, var_c));
	+ }
	+ }
	+};

File Metadata

Mime Type: text/x-diff
Expires: Mon, Oct 20, 8:14 AM (19 h, 34 m)
Storage Engine: blob
Storage Format: Raw Data
Storage Handle: 199672
Default Alt Text: (85 KB)

No OneTemporaryActions

View Options

File Metadata

Event Timeline

No OneTemporary
Actions