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 +#include +#include + +#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 +#include +#include +#include +#include + +#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 +#include +#include + +#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 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 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 +#include +#include +#include +#include +#include +#include +#include +#include + +#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_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 inputs, cvo_t *&cvo, cvo_init_t opt, + std::vector input_order = std::vector()) { + cvo = new std::vector(inputs.size()); + std::vector 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 +#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()(k.f->index) ^ (std::hash()(k.g->index) << 1) ^ + (std::hash()(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 +#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()(k.f) ^ (std::hash()(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 +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include + +#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 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=<≠>]\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 var_rel, + node_index_t inputs, std::vector &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 var_rel, + node_index_t inputs, std::vector &tt) { + std::vector neq_rel = var_rel; + std::vector 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 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 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; + std::vector signal_map; + cvo_t *cvo; + uint32_t num_inputs; + std::unordered_map computed_table; + std::unordered_map 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 inputs, cvo_init_t cvo_opt, + std::vector input_cvo = std::vector()) { + cvo = reinterpret_cast(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 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( + 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 tt(std::pow(2, this->num_inputs), false); + std::vector 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=<≠>, " + "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 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=<≠>, " + "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)); + } + } +};