20 #define forall_nodes(it) \
21 for(nodest::const_iterator it = nodes.begin(); it != nodes.end(); it++)
50 out <<
"digraph BDD {\n";
52 out <<
"center = true;\n";
54 out <<
"{ rank = same; { node [style=invis]; \"T\" };\n";
57 out <<
" { node [shape=box,fontsize=24]; \"0\"; }\n";
59 out <<
" { node [shape=box,fontsize=24]; \"1\"; }\n"
62 for(
unsigned v = 0; v <
var_table.size(); v++)
64 out <<
"{ rank=same; "
65 "{ node [shape=plaintext,fontname=\"Times Italic\",fontsize=24] \" "
69 if(u->var == (v + 1) && u->reference_counter != 0)
70 out <<
'"' << u->node_number <<
"\"; ";
77 out <<
"{ edge [style = invis];";
79 for(
unsigned v = 0; v <
var_table.size(); v++)
80 out <<
" \" " <<
var_table[v].label <<
" \" ->";
88 if(u->reference_counter == 0)
90 if(u->node_number <= 1)
93 if(!suppress_zero || u->high.node_number() != 0)
94 out <<
'"' << u->node_number <<
'"' <<
" -> " <<
'"'
95 << u->high.node_number() <<
'"'
96 <<
" [style=solid,arrowsize=\".75\"];\n";
98 if(!suppress_zero || u->low.node_number() != 0)
99 out <<
'"' << u->node_number <<
'"' <<
" -> " <<
'"'
100 << u->low.node_number() <<
'"'
101 <<
" [style=dashed,arrowsize=\".75\"];\n";
112 bool node_numbers)
const
114 out <<
"\\begin{tikzpicture}[node distance=1cm]\n";
116 out <<
" \\tikzstyle{BDDnode}=[circle,draw=black,"
117 "inner sep=0pt,minimum size=5mm]\n";
119 for(
unsigned v = 0; v <
var_table.size(); v++)
124 out <<
"below of=v" <<
var_table[v - 1].label;
129 unsigned previous = 0;
133 if(u->var == (v + 1) && u->reference_counter != 0)
135 out <<
" \\node[xshift=0cm, BDDnode, ";
138 out <<
"right of=v" <<
var_table[v].label;
140 out <<
"right of=n" << previous;
142 out <<
"] (n" << u->node_number <<
") {";
144 out <<
"\\small $" << u->node_number <<
"$";
146 previous = u->node_number;
155 out <<
" % terminals\n";
156 out <<
" \\node[draw=black, style=rectangle, below of=v"
157 <<
var_table.back().label <<
", xshift=1cm] (n1) {$1$};\n";
160 out <<
" \\node[draw=black, style=rectangle, left of=n1] (n0) {$0$};\n";
169 if(u->reference_counter != 0 && u->node_number >= 2)
171 if(!suppress_zero || u->low.node_number() != 0)
172 out <<
" \\draw[->,dashed] (n" << u->node_number <<
") -> (n"
173 << u->low.node_number() <<
");\n";
175 if(!suppress_zero || u->high.node_number() != 0)
176 out <<
" \\draw[->] (n" << u->node_number <<
") -> (n"
177 << u->high.node_number() <<
");\n";
183 out <<
"\\end{tikzpicture}\n";
211 "apply can only be called on initialized BDDs");
214 "apply can only be called on BDDs with the same manager");
218 Gt::const_iterator G_it =
G.find(key);
228 else if(x.
var() == y.
var())
231 else if(x.
var() < y.
var())
243 struct stack_elementt
249 key(x.node_number(), y.node_number()),
255 std::pair<unsigned, unsigned> key;
266 std::stack<stack_elementt> stack;
267 stack.push(stack_elementt(u, _x, _y));
269 while(!stack.empty())
271 auto &t = stack.top();
277 "apply can only be called on initialized BDDs");
280 "apply can only be called on BDDs with the same manager");
284 case stack_elementt::phaset::INIT:
287 Gt::const_iterator G_it =
G.find(t.key);
290 t.result = G_it->second;
299 t.result = result_truth ? mgr.
True() : mgr.
False();
302 else if(x.
var() == y.
var())
305 t.phase = stack_elementt::phaset::FINISH;
308 x.
low().
var() > t.var,
"applying won't break variable order");
310 y.
low().
var() > t.var,
"applying won't break variable order");
312 x.
high().
var() > t.var,
"applying won't break variable order");
314 y.
high().
var() > t.var,
"applying won't break variable order");
316 stack.push(stack_elementt(t.lr, x.
low(), y.
low()));
317 stack.push(stack_elementt(t.hr, x.
high(), y.
high()));
319 else if(x.
var() < y.
var())
322 t.phase = stack_elementt::phaset::FINISH;
325 x.
low().
var() > t.var,
"applying won't break variable order");
327 x.
high().
var() > t.var,
"applying won't break variable order");
329 stack.push(stack_elementt(t.lr, x.
low(), y));
330 stack.push(stack_elementt(t.hr, x.
high(), y));
335 t.phase = stack_elementt::phaset::FINISH;
338 y.
low().
var() > t.var,
"applying won't break variable order");
340 y.
high().
var() > t.var,
"applying won't break variable order");
342 stack.push(stack_elementt(t.lr, x, y.
low()));
343 stack.push(stack_elementt(t.hr, x, y.
high()));
349 case stack_elementt::phaset::FINISH:
352 t.result = mgr->
mk(t.var, t.lr, t.hr);
430 var <=
var_table.size(),
"cannot make a BDD for an unknown variable");
432 low.
var() > var,
"low-edge would break variable ordering");
435 high.
var() > var,
"high-edge would break variable ordering");
442 reverse_mapt::const_iterator it =
reverse_map.find(reverse_key);
452 unsigned new_number =
nodes.back().node_number + 1;
490 out <<
"\\# & \\mathit{var} & \\mathit{low} &"
491 " \\mathit{high} \\\\\\hline\n";
495 out << it->node_number <<
" & ";
497 if(it->node_number == 0 || it->node_number == 1)
498 out << it->var <<
" & & \\\\";
499 else if(it->reference_counter == 0)
500 out <<
"- & - & - \\\\";
502 out << it->var <<
"\\," <<
var_table[it->var - 1].label <<
" & "
503 << it->low.node_number() <<
" & " << it->high.node_number()
506 if(it->node_number == 1)
509 out <<
" % " << it->reference_counter <<
'\n';
516 inline restrictt(
const unsigned _var,
const bool _value)
517 : var(_var), value(_value)
539 "restricting variables can only be done in initialized BDDs");
546 else if(u.
var() < var)
549 t = RES(value ? u.
high() : u.
low());
586 std::string path_low = path;
587 std::string path_high = path;
608 cubes(u,
"", result);
622 assignment[v.
var()] =
true;
625 assignment[v.
var()] =
false;