30 #include "../DdSpec.hpp" 34 template<
typename T,
typename S,
bool ZDD>
35 class Unreduction_:
public PodArrayDdSpec<T,size_t,S::ARITY> {
40 static size_t const levelWords = (
sizeof(int) +
sizeof(Word) - 1)
47 static int wordSize(
int size) {
48 return (size +
sizeof(Word) - 1) /
sizeof(Word);
51 int& level(
void* p)
const {
52 return *
static_cast<int*
>(p);
55 int level(
void const* p)
const {
56 return *
static_cast<int const*
>(p);
59 void* state(
void* p)
const {
60 return static_cast<Word*
>(p) + levelWords;
63 void const* state(
void const* p)
const {
64 return static_cast<Word const*
>(p) + levelWords;
68 Unreduction_(S
const& s,
int numVars)
69 : spec(s), stateWords(wordSize(spec.datasize())), numVars(numVars) {
70 Unreduction_::setArraySize(levelWords + stateWords);
73 int getRoot(Word* p) {
74 level(p) = spec.get_root(state(p));
75 if (level(p) == 0)
return 0;
76 if (level(p) >= numVars) numVars = level(p);
77 return (numVars > 0) ? numVars : -1;
80 int getChild(Word* p,
int i,
int value) {
82 level(p) = spec.get_child(state(p), i, value);
83 if (level(p) == 0)
return 0;
85 else if (ZDD && value) {
90 assert(level(p) <= i);
91 return (i > 0) ? i : level(p);
94 void get_copy(
void* to,
void const* from) {
95 level(to) = level(from);
96 spec.get_copy(state(to), state(from));
99 void destruct(
void* p) {
100 spec.destruct(state(p));
103 void destructLevel(
int level) {
104 spec.destructLevel(level);
107 int merge_states(
void* p1,
void* p2) {
108 return spec.merge_states(state(p1), state(p2));
111 size_t hash_code(
void const* p,
int i)
const {
112 size_t h = size_t(level(p)) * 314159257;
113 if (level(p) > 0) h += spec.hash_code(state(p), level(p)) * 271828171;
117 bool equal_to(
void const* p,
void const* q,
int i)
const {
118 if (level(p) != level(q))
return false;
119 if (level(p) > 0 && !spec.equal_to(state(p), state(q), level(p)))
return false;
123 void print_state(std::ostream& os,
void const* p,
int l)
const {
124 Word
const* q =
static_cast<Word const*
>(p);
125 os <<
"<" << level(q) <<
",";
126 spec.print_state(os, state(q), l);
132 struct BddUnreduction:
public Unreduction_<BddUnreduction<S>,S,false> {
133 BddUnreduction(S
const& s,
int numVars)
134 : Unreduction_<BddUnreduction<S>,S,false>(s, numVars) {
139 struct ZddUnreduction:
public Unreduction_<ZddUnreduction<S>,S,true> {
140 ZddUnreduction(S
const& s,
int numVars)
141 : Unreduction_<ZddUnreduction<S>,S,true>(s, numVars) {