20 #define forall_nodes(it) for(nodest::const_iterator it=nodes.begin(); \ 21 it!=nodes.end(); it++) 43 true_bdd.
node->
var=var_table.size()+1;
44 false_bdd.node->var=var_table.size()+1;
45 return mk(var_table.size(), false_bdd, true_bdd);
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++)
81 out <<
" \" " << var_table[v].label
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{" 129 << var_table[v].label <<
"}$};\n";
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" 159 << var_table.back().label
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";
198 return APP_non_rec(x, y);
202 bool (*fkt)(bool, bool);
219 Gt::const_iterator G_it=G.find(key);
231 APP_rec(x.
low(), y.
low()),
236 APP_rec(x.
high(), y));
240 APP_rec(x, y.
high()));
251 struct stack_elementt
257 result(_result), x(_x), y(_y),
258 key(x.node_number(), y.node_number()),
259 var(0), phase(phaset::INIT) { }
261 std::pair<unsigned, unsigned> key;
263 enum class phaset { INIT, FINISH } phase;
268 std::stack<stack_elementt>
stack;
269 stack.push(stack_elementt(u, _x, _y));
271 while(!stack.empty())
283 case stack_elementt::phaset::INIT:
286 Gt::const_iterator G_it=G.find(t.key);
289 t.result=G_it->second;
298 t.result=result_truth?mgr.
True():mgr.False();
304 t.phase=stack_elementt::phaset::FINISH;
306 assert(x.
low().
var()>t.var);
308 assert(y.
low().
var()>t.var);
313 stack.push(stack_elementt(t.lr, x.
low(), y.
low()));
314 stack.push(stack_elementt(t.hr, x.
high(), y.
high()));
319 t.phase=stack_elementt::phaset::FINISH;
321 assert(x.
low().
var()>t.var);
324 stack.push(stack_elementt(t.lr, x.
low(), y));
325 stack.push(stack_elementt(t.hr, x.
high(), y));
330 t.phase=stack_elementt::phaset::FINISH;
332 assert(y.
low().
var()>t.var);
335 stack.push(stack_elementt(t.lr, x, y.
low()));
336 stack.push(stack_elementt(t.hr, x, y.
high()));
342 case stack_elementt::phaset::FINISH:
345 t.result=mgr->
mk(t.var, t.lr, t.hr);
382 assert(is_initialized());
383 return node->mgr->True()^*
this;
425 assert(var<=var_table.size());
436 reverse_mapt::const_iterator it=reverse_map.find(reverse_key);
438 if(it!=reverse_map.end())
447 nodes.push_back(
mini_bdd_nodet(
this, var, new_number, low, high));
459 reverse_map[reverse_key]=n;
484 out <<
"\\# & \\mathit{var} & \\mathit{low} &" 485 " \\mathit{high} \\\\\\hline\n";
489 out << it->node_number <<
" & ";
491 if(it->node_number==0 || it->node_number==1)
492 out << it->var <<
" & & \\\\";
493 else if(it->reference_counter==0)
494 out <<
"- & - & - \\\\";
496 out << it->var <<
"\\," << var_table[it->var-1].label <<
" & " 497 << it->low.node_number() <<
" & " << it->high.node_number()
500 if(it->node_number==1)
503 out <<
" % " << it->reference_counter <<
'\n';
510 inline restrictt(
const unsigned _var,
const bool _value):
511 var(_var), value(_value)
537 t=mgr->mk(u.
var(), RES(u.
low()), RES(u.
high()));
562 return ( tp &
restrict(t, var,
true)) |
578 std::string path_low=path;
579 std::string path_high=path;
600 cubes(u,
"", result);
614 assignment[v.
var()]=
true;
617 assignment[v.
var()]=
false;
bool or_fkt(bool x, bool y)
void DumpTikZ(std::ostream &out, bool supress_zero=false, bool node_numbers=true) const
unsigned reference_counter
const mini_bddt & False() const
unsigned node_number() const
mini_bddt operator()(const mini_bddt &x, const mini_bddt &y)
bool equal_fkt(bool x, bool y)
mini_bddt operator!() const
bool is_initialized() const
void cubes(const mini_bddt &u, const std::string &path, std::string &result)
mini_bddt exists(const mini_bddt &u, const unsigned var)
mini_bddt substitute(const mini_bddt &t, unsigned var, const mini_bddt &tp)
mini_bdd_nodet(class mini_bdd_mgrt *_mgr, unsigned _var, unsigned _node_number, const mini_bddt &_low, const mini_bddt &_high)
class mini_bdd_nodet * node
bool xor_fkt(bool x, bool y)
mini_bddt operator==(const mini_bddt &) const
const mini_bddt & high() const
mini_bddt operator &(const mini_bddt &) const
mini_bddt Var(const std::string &label)
const mini_bddt & True() const
mini_bddt operator^(const mini_bddt &) const
A minimalistic BDD library, following Bryant's original paper and Andersen's lecture notes...
bool and_fkt(bool x, bool y)
mini_bddt operator()(const mini_bddt &u)
mini_bdd_applyt(bool(*_fkt)(bool, bool))
mini_bddt mk(unsigned var, const mini_bddt &low, const mini_bddt &high)
mini_bddt APP_non_rec(const mini_bddt &x, const mini_bddt &y)
mini_bddt APP_rec(const mini_bddt &x, const mini_bddt &y)
void DumpTable(std::ostream &out) const
const mini_bddt & low() const
class mini_bdd_mgrt * mgr
mini_bddt operator|(const mini_bddt &) const
restrictt(const unsigned _var, const bool _value)
std::map< std::pair< unsigned, unsigned >, mini_bddt > Gt
bool operator<(const reverse_keyt &) const
mini_bddt RES(const mini_bddt &u)
bool OneSat(const mini_bddt &v, std::map< unsigned, bool > &assignment)
void DumpDot(std::ostream &out, bool supress_zero=false) const
mini_bddt restrict(const mini_bddt &u, unsigned var, const bool value)