TdZdd  1.1
A top-down/breadth-first decision diagram manipulation framework
Unreduction.hpp
1 /*
2  * TdZdd: a Top-down/Breadth-first Decision Diagram Manipulation Framework
3  * by Hiroaki Iwashita <iwashita@erato.ist.hokudai.ac.jp>
4  * Copyright (c) 2014 ERATO MINATO Project
5  *
6  * Permission is hereby granted, free of charge, to any person obtaining a
7  * copy of this software and associated documentation files (the "Software"),
8  * to deal in the Software without restriction, including without limitation
9  * the rights to use, copy, modify, merge, publish, distribute, sublicense,
10  * and/or sell copies of the Software, and to permit persons to whom the
11  * Software is furnished to do so, subject to the following conditions:
12  *
13  * The above copyright notice and this permission notice shall be included in
14  * all copies or substantial portions of the Software.
15  *
16  * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
17  * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
18  * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
19  * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
20  * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
21  * FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER
22  * DEALINGS IN THE SOFTWARE.
23  */
24 
25 #pragma once
26 
27 #include <cassert>
28 #include <iostream>
29 
30 #include "../DdSpec.hpp"
31 
32 namespace tdzdd {
33 
34 template<typename T, typename S, bool ZDD>
35 class Unreduction_: public PodArrayDdSpec<T,size_t,S::ARITY> {
36 protected:
37  typedef S Spec;
38  typedef size_t Word;
39 
40  static size_t const levelWords = (sizeof(int) + sizeof(Word) - 1)
41  / sizeof(Word);
42 
43  Spec spec;
44  int const stateWords;
45  int numVars;
46 
47  static int wordSize(int size) {
48  return (size + sizeof(Word) - 1) / sizeof(Word);
49  }
50 
51  int& level(void* p) const {
52  return *static_cast<int*>(p);
53  }
54 
55  int level(void const* p) const {
56  return *static_cast<int const*>(p);
57  }
58 
59  void* state(void* p) const {
60  return static_cast<Word*>(p) + levelWords;
61  }
62 
63  void const* state(void const* p) const {
64  return static_cast<Word const*>(p) + levelWords;
65  }
66 
67 public:
68  Unreduction_(S const& s, int numVars)
69  : spec(s), stateWords(wordSize(spec.datasize())), numVars(numVars) {
70  Unreduction_::setArraySize(levelWords + stateWords);
71  }
72 
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;
78  }
79 
80  int getChild(Word* p, int i, int value) {
81  if (level(p) == i) {
82  level(p) = spec.get_child(state(p), i, value);
83  if (level(p) == 0) return 0;
84  }
85  else if (ZDD && value) {
86  return 0;
87  }
88 
89  --i;
90  assert(level(p) <= i);
91  return (i > 0) ? i : level(p);
92  }
93 
94  void get_copy(void* to, void const* from) {
95  level(to) = level(from);
96  spec.get_copy(state(to), state(from));
97  }
98 
99  void destruct(void* p) {
100  spec.destruct(state(p));
101  }
102 
103  void destructLevel(int level) {
104  spec.destructLevel(level);
105  }
106 
107  int merge_states(void* p1, void* p2) {
108  return spec.merge_states(state(p1), state(p2));
109  }
110 
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;
114  return h;
115  }
116 
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;
120  return true;
121  }
122 
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);
127  os << ">";
128  }
129 };
130 
131 template<typename S>
132 struct BddUnreduction: public Unreduction_<BddUnreduction<S>,S,false> {
133  BddUnreduction(S const& s, int numVars)
134  : Unreduction_<BddUnreduction<S>,S,false>(s, numVars) {
135  }
136 };
137 
138 template<typename S>
139 struct ZddUnreduction: public Unreduction_<ZddUnreduction<S>,S,true> {
140  ZddUnreduction(S const& s, int numVars)
141  : Unreduction_<ZddUnreduction<S>,S,true>(s, numVars) {
142  }
143 };
144 
145 } // namespace tdzdd