Page MenuHomePhorge
Files F27037053

bbdd_node.hpp
No OneTemporary
Actions

Authored By
Unknown
Size
5 KB
Referenced Files
None
Subscribers
None

bbdd_node.hpp
View Options

// 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;
}

File Metadata

Mime Type
text/x-c
Expires
Tue, Oct 27, 8:25 PM (20 h, 26 m)
Storage Engine
blob
Storage Format
Raw Data
Storage Handle
402774
Default Alt Text
bbdd_node.hpp (5 KB)

Event Timeline