35 #include "../DdSpec.hpp" 39 class GraphillionZdd:
public tdzdd::DdSpec<GraphillionZdd,uint64_t,2> {
45 std::vector<Node> table;
52 : root(0), minIndex(INT_MAX), maxIndex(INT_MIN) {
55 void read(std::string
const& filename =
"") {
56 tdzdd::MessageHandler mh;
59 if (filename.empty()) {
64 mh <<
" \"" << filename <<
"\" ...";
65 std::ifstream fin(filename.c_str(), std::ios::in);
66 if (!fin)
throw std::runtime_error(strerror(errno));
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;
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);
87 void read(std::istream& is) {
89 if (isdigit(skipSpace(is))) {
95 node.child[0] = readID(is);
96 node.child[1] = readID(is);
104 static uint64_t readID(std::istream& is) {
107 while (isspace(c = is.get()))
115 id = (c ==
'T' || c ==
't') ? 1 : 0;
120 static int skipSpace(std::istream& is) {
122 while (isspace(c = is.get()))
128 static void skipLine(std::istream& is) {
129 while (is && is.get() !=
'\n')
134 int getRoot(uint64_t& f)
const {
136 if (f == 0)
return 0;
137 if (f == 1)
return -1;
138 return maxIndex - table.at(f).index + 1;
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;
Abstract class of DD specifications using scalar states.