20 #define forall_nodes(it) for(nodest::const_iterator it=nodes.begin(); \
21 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] \" "
70 if(u->var==(v+1) && u->reference_counter!=0)
71 out <<
'"' << u->node_number <<
"\"; ";
78 out <<
"{ edge [style = invis];";
80 for(
unsigned v=0; v<
var_table.size(); v++)
90 if(u->reference_counter==0)
95 if(!suppress_zero || u->high.node_number()!=0)
96 out <<
'"' << u->node_number <<
'"' <<
" -> "
97 <<
'"' << u->high.node_number() <<
'"'
98 <<
" [style=solid,arrowsize=\".75\"];\n";
100 if(!suppress_zero || u->low.node_number()!=0)
101 out <<
'"' << u->node_number <<
'"' <<
" -> "
102 <<
'"' << u->low.node_number() <<
'"'
103 <<
" [style=dashed,arrowsize=\".75\"];\n";
114 bool node_numbers)
const
116 out <<
"\\begin{tikzpicture}[node distance=1cm]\n";
118 out <<
" \\tikzstyle{BDDnode}=[circle,draw=black,"
119 "inner sep=0pt,minimum size=5mm]\n";
121 for(
unsigned v=0; v<
var_table.size(); v++)
126 out <<
"below of=v" <<
var_table[v-1].label;
128 out <<
"] (v" <<
var_table[v].label <<
") {$\\mathit{"
135 if(u->var==(v+1) && u->reference_counter!=0)
137 out <<
" \\node[xshift=0cm, BDDnode, ";
140 out <<
"right of=v" <<
var_table[v].label;
142 out <<
"right of=n" << previous;
144 out <<
"] (n" << u->node_number <<
") {";
146 out <<
"\\small $" << u->node_number <<
"$";
148 previous=u->node_number;
157 out <<
" % terminals\n";
158 out <<
" \\node[draw=black, style=rectangle, below of=v"
160 <<
", xshift=1cm] (n1) {$1$};\n";
163 out <<
" \\node[draw=black, style=rectangle, left of=n1] (n0) {$0$};\n";
172 if(u->reference_counter!=0 && u->node_number>=2)
174 if(!suppress_zero || u->low.node_number()!=0)
175 out <<
" \\draw[->,dashed] (n" << u->node_number <<
") -> (n"
176 << u->low.node_number() <<
");\n";
178 if(!suppress_zero || u->high.node_number()!=0)
179 out <<
" \\draw[->] (n" << u->node_number <<
") -> (n"
180 << u->high.node_number() <<
");\n";
186 out <<
"\\end{tikzpicture}\n";
214 "apply can only be called on initialized BDDs");
217 "apply can only be called on BDDs with the same manager");
221 Gt::const_iterator G_it=
G.find(key);
253 struct stack_elementt
259 result(_result), x(_x), y(_y),
260 key(x.node_number(), y.node_number()),
261 var(0), phase(phaset::INIT) { }
263 std::pair<unsigned, unsigned> key;
265 enum class phaset { INIT, FINISH } phase;
270 std::stack<stack_elementt>
stack;
271 stack.push(stack_elementt(u, _x, _y));
273 while(!
stack.empty())
281 "apply can only be called on initialized BDDs");
284 "apply can only be called on BDDs with the same manager");
288 case stack_elementt::phaset::INIT:
291 Gt::const_iterator G_it=
G.find(t.key);
294 t.result=G_it->second;
303 t.result=result_truth?mgr.
True():mgr.False();
309 t.phase=stack_elementt::phaset::FINISH;
312 x.
low().
var() > t.var,
"applying won't break variable order");
314 y.
low().
var() > t.var,
"applying won't break variable order");
316 x.
high().
var() > t.var,
"applying won't break variable order");
318 y.
high().
var() > t.var,
"applying won't break variable order");
320 stack.push(stack_elementt(t.lr, x.
low(), y.
low()));
326 t.phase=stack_elementt::phaset::FINISH;
329 x.
low().
var() > t.var,
"applying won't break variable order");
331 x.
high().
var() > t.var,
"applying won't break variable order");
333 stack.push(stack_elementt(t.lr, x.
low(), y));
334 stack.push(stack_elementt(t.hr, x.
high(), y));
339 t.phase=stack_elementt::phaset::FINISH;
342 y.
low().
var() > t.var,
"applying won't break variable order");
344 y.
high().
var() > t.var,
"applying won't break variable order");
346 stack.push(stack_elementt(t.lr, x, y.
low()));
347 stack.push(stack_elementt(t.hr, x, y.
high()));
353 case stack_elementt::phaset::FINISH:
356 t.result=mgr->
mk(t.var, t.lr, t.hr);
436 var <=
var_table.size(),
"cannot make a BDD for an unknown variable");
438 low.
var() > var,
"low-edge would break variable ordering");
441 high.
var() > var,
"high-edge would break variable ordering");
448 reverse_mapt::const_iterator it=
reverse_map.find(reverse_key);
458 unsigned new_number=
nodes.back().node_number+1;
496 out <<
"\\# & \\mathit{var} & \\mathit{low} &"
497 " \\mathit{high} \\\\\\hline\n";
501 out << it->node_number <<
" & ";
503 if(it->node_number==0 || it->node_number==1)
504 out << it->var <<
" & & \\\\";
505 else if(it->reference_counter==0)
506 out <<
"- & - & - \\\\";
508 out << it->var <<
"\\," <<
var_table[it->var-1].label <<
" & "
509 << it->low.node_number() <<
" & " << it->high.node_number()
512 if(it->node_number==1)
515 out <<
" % " << it->reference_counter <<
'\n';
522 inline restrictt(
const unsigned _var,
const bool _value):
523 var(_var), value(_value)
542 "restricting variables can only be done in initialized BDDs");
550 t=mgr->mk(u.
var(), RES(u.
low()), RES(u.
high()));
575 return ( tp &
restrict(t, var,
true)) |
591 std::string path_low=path;
592 std::string path_high=path;
613 cubes(u,
"", result);
627 assignment[v.
var()]=
true;
630 assignment[v.
var()]=
false;