TdZdd  1.1
A top-down/breadth-first decision diagram manipulation framework
GraphillionZdd.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 <cerrno>
29 #include <climits>
30 #include <ostream>
31 #include <stdint.h>
32 #include <string>
33 #include <vector>
34 
35 #include "../DdSpec.hpp"
36 
37 namespace tdzdd {
38 
39 class GraphillionZdd: public tdzdd::DdSpec<GraphillionZdd,uint64_t,2> {
40  struct Node {
41  int index;
42  uint64_t child[2];
43  };
44 
45  std::vector<Node> table;
46  uint64_t root;
47  int minIndex;
48  int maxIndex;
49 
50 public:
51  GraphillionZdd()
52  : root(0), minIndex(INT_MAX), maxIndex(INT_MIN) {
53  }
54 
55  void read(std::string const& filename = "") {
56  tdzdd::MessageHandler mh;
57  mh.begin("reading");
58 
59  if (filename.empty()) {
60  mh << " STDIN ...";
61  read(std::cin);
62  }
63  else {
64  mh << " \"" << filename << "\" ...";
65  std::ifstream fin(filename.c_str(), std::ios::in);
66  if (!fin) throw std::runtime_error(strerror(errno));
67  read(fin);
68  }
69 
70  mh.end();
71  }
72 
73  void addNode(uint64_t id, Node const& node) {
74  if (minIndex > node.index) minIndex = node.index, root = id;
75  if (maxIndex < node.index) maxIndex = node.index;
76 
77  uint64_t n = table.size();
78  if (n <= id) n = id + 1;
79  if (n <= node.child[0]) n = node.child[0] + 1;
80  if (n <= node.child[1]) n = node.child[1] + 1;
81  if (n > table.size()) table.resize(n * 2);
82 
83  table.at(id) = node;
84  }
85 
86 private:
87  void read(std::istream& is) {
88  while (is) {
89  if (isdigit(skipSpace(is))) {
90  uint64_t id;
91  Node node;
92 
93  id = readID(is);
94  is >> node.index;
95  node.child[0] = readID(is);
96  node.child[1] = readID(is);
97 
98  addNode(id, node);
99  }
100  skipLine(is);
101  }
102  }
103 
104  static uint64_t readID(std::istream& is) {
105  int c;
106  uint64_t id;
107  while (isspace(c = is.get()))
108  ;
109  if (isdigit(c)) {
110  is.unget();
111  is >> id;
112  id += 2;
113  }
114  else {
115  id = (c == 'T' || c == 't') ? 1 : 0;
116  }
117  return id;
118  }
119 
120  static int skipSpace(std::istream& is) {
121  int c;
122  while (isspace(c = is.get()))
123  ;
124  is.unget();
125  return c;
126  }
127 
128  static void skipLine(std::istream& is) {
129  while (is && is.get() != '\n')
130  ;
131  }
132 
133 public:
134  int getRoot(uint64_t& f) const {
135  f = root;
136  if (f == 0) return 0;
137  if (f == 1) return -1;
138  return maxIndex - table.at(f).index + 1;
139  }
140 
141  int getChild(uint64_t& f, int level, int take) const {
142  f = table.at(f).child[take];
143  if (f == 0) return 0;
144  if (f == 1) return -1;
145  return maxIndex - table.at(f).index + 1;
146  }
147 };
148 
149 } // namespace tdzdd
Abstract class of DD specifications using scalar states.
Definition: DdSpec.hpp:257