47 out <<
"digraph BDD {\n";
49 out <<
"center = true;\n";
51 out <<
"{ rank = same; { node [style=invis]; \"T\" };\n";
54 out <<
" { node [shape=box,fontsize=24]; \"0\"; }\n";
56 out <<
" { node [shape=box,fontsize=24]; \"1\"; }\n"
59 for(
unsigned v = 0; v <
var_table.size(); v++)
61 out <<
"{ rank=same; "
62 "{ node [shape=plaintext,fontname=\"Times Italic\",fontsize=24] \" "
67 if(
u.var == (v + 1) &&
u.reference_counter != 0)
68 out <<
'"' <<
u.node_number <<
"\"; ";
76 out <<
"{ edge [style = invis];";
78 for(
unsigned v = 0; v <
var_table.size(); v++)
79 out <<
" \" " <<
var_table[v].label <<
" \" ->";
87 if(
u.reference_counter == 0)
89 if(
u.node_number <= 1)
93 out <<
'"' <<
u.node_number <<
'"' <<
" -> " <<
'"'
94 <<
u.high.node_number() <<
'"'
95 <<
" [style=solid,arrowsize=\".75\"];\n";
98 out <<
'"' <<
u.node_number <<
'"' <<
" -> " <<
'"' <<
u.low.node_number()
99 <<
'"' <<
" [style=dashed,arrowsize=\".75\"];\n";
112 out <<
"\\begin{tikzpicture}[node distance=1cm]\n";
114 out <<
" \\tikzstyle{BDDnode}=[circle,draw=black,"
115 "inner sep=0pt,minimum size=5mm]\n";
117 for(
unsigned v = 0; v <
var_table.size(); v++)
122 out <<
"below of=v" <<
var_table[v - 1].label;
127 unsigned previous = 0;
129 for(
const auto &
u :
nodes)
131 if(
u.var == (v + 1) &&
u.reference_counter != 0)
133 out <<
" \\node[xshift=0cm, BDDnode, ";
136 out <<
"right of=v" <<
var_table[v].label;
138 out <<
"right of=n" << previous;
140 out <<
"] (n" <<
u.node_number <<
") {";
142 out <<
"\\small $" <<
u.node_number <<
"$";
144 previous =
u.node_number;
153 out <<
" % terminals\n";
154 out <<
" \\node[draw=black, style=rectangle, below of=v"
155 <<
var_table.back().label <<
", xshift=1cm] (n1) {$1$};\n";
158 out <<
" \\node[draw=black, style=rectangle, left of=n1] (n0) {$0$};\n";
165 for(
const auto &
u :
nodes)
167 if(
u.reference_counter != 0 &&
u.node_number >= 2)
170 out <<
" \\draw[->,dashed] (n" <<
u.node_number <<
") -> (n"
171 <<
u.low.node_number() <<
");\n";
174 out <<
" \\draw[->] (n" <<
u.node_number <<
") -> (n"
175 <<
u.high.node_number() <<
");\n";
181 out <<
"\\end{tikzpicture}\n";
208 x.is_initialized() &&
y.is_initialized(),
209 "apply can only be called on initialized BDDs");
211 x.node->mgr ==
y.node->mgr,
212 "apply can only be called on BDDs with the same manager");
215 std::pair<unsigned, unsigned>
key(
x.node_number(),
y.node_number());
216 Gt::const_iterator
G_it =
G.find(
key);
224 if(
x.is_constant() &&
y.is_constant())
226 else if(
x.var() ==
y.var())
229 else if(
x.var() <
y.var())
247 key(
x.node_number(),
y.node_number()),
253 std::pair<unsigned, unsigned>
key;
264 std::stack<stack_elementt> stack;
267 while(!stack.empty())
269 auto &t = stack.top();
274 x.is_initialized() &&
y.is_initialized(),
275 "apply can only be called on initialized BDDs");
277 x.node->mgr ==
y.node->mgr,
278 "apply can only be called on BDDs with the same manager");
282 case stack_elementt::phaset::INIT:
285 Gt::const_iterator
G_it =
G.find(t.key);
288 t.result =
G_it->second;
293 if(
x.is_constant() &&
y.is_constant())
300 else if(
x.var() ==
y.var())
303 t.phase = stack_elementt::phaset::FINISH;
306 x.low().var() > t.var,
"applying won't break variable order");
308 y.low().var() > t.var,
"applying won't break variable order");
310 x.high().var() > t.var,
"applying won't break variable order");
312 y.high().var() > t.var,
"applying won't break variable order");
317 else if(
x.var() <
y.var())
320 t.phase = stack_elementt::phaset::FINISH;
323 x.low().var() > t.var,
"applying won't break variable order");
325 x.high().var() > t.var,
"applying won't break variable order");
333 t.phase = stack_elementt::phaset::FINISH;
336 y.low().var() > t.var,
"applying won't break variable order");
338 y.high().var() > t.var,
"applying won't break variable order");
347 case stack_elementt::phaset::FINISH:
350 t.result = mgr->
mk(t.var, t.lr, t.hr);
359 u.is_initialized(),
"the resulting BDD is initialized");
388 return node->mgr->True() ^ *
this;
428 var <=
var_table.size(),
"cannot make a BDD for an unknown variable");
430 low.
var() > var,
"low-edge would break variable ordering");
433 high.
var() > var,
"high-edge would break variable ordering");
476 else if(
x.var >
y.var)
478 else if(
x.low <
y.low)
480 else if(
x.low >
y.low)
483 return x.high <
y.high;
488 out <<
"\\# & \\mathit{var} & \\mathit{low} &"
489 " \\mathit{high} \\\\\\hline\n";
491 for(
const auto &
n :
nodes)
493 out <<
n.node_number <<
" & ";
495 if(
n.node_number == 0 ||
n.node_number == 1)
496 out <<
n.var <<
" & & \\\\";
497 else if(
n.reference_counter == 0)
498 out <<
"- & - & - \\\\";
500 out <<
n.var <<
"\\," <<
var_table[
n.var - 1].label <<
" & "
501 <<
n.low.node_number() <<
" & " <<
n.high.node_number() <<
" \\\\";
503 if(
n.node_number == 1)
506 out <<
" % " <<
n.reference_counter <<
'\n';
514 : var(
_var), value(_value)
536 "restricting variables can only be done in initialized BDDs");
543 else if(
u.var() < var)
544 t = mgr->
mk(
u.var(), RES(
u.low()), RES(
u.high()));
546 t = RES(value ?
u.high() :
u.low());
619 assignment[v.
var()] =
true;
622 assignment[v.
var()] =
false;
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
mini_bddt operator()(const mini_bddt &x, const mini_bddt &y)
std::map< std::pair< unsigned, unsigned >, mini_bddt > Gt
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)
mini_bdd_applyt(bool(*_fkt)(bool, bool))
mini_bddt Var(const std::string &label)
const mini_bddt & False() const
void DumpTable(std::ostream &out) const
void DumpDot(std::ostream &out, bool supress_zero=false) const
friend class mini_bdd_nodet
void DumpTikZ(std::ostream &out, bool supress_zero=false, bool node_numbers=true) const
mini_bddt mk(unsigned var, const mini_bddt &low, const mini_bddt &high)
const mini_bddt & True() const
class mini_bdd_mgrt * mgr
unsigned reference_counter
mini_bddt operator!() const
const mini_bddt & high() const
bool is_initialized() const
const mini_bddt & low() const
mini_bddt operator&(const mini_bddt &) const
mini_bddt operator^(const mini_bddt &) const
mini_bddt operator|(const mini_bddt &) const
unsigned node_number() const
class mini_bdd_nodet * node
mini_bddt operator==(const mini_bddt &) const
restrictt(const unsigned _var, const bool _value)
mini_bddt operator()(const mini_bddt &u)
mini_bddt RES(const mini_bddt &u)
bool and_fkt(bool x, bool y)
bool equal_fkt(bool x, bool y)
bool xor_fkt(bool x, bool y)
bool or_fkt(bool x, bool y)
A minimalistic BDD library, following Bryant's original paper and Andersen's lecture notes.
mini_bddt restrict(const mini_bddt &u, unsigned var, const bool value)
mini_bddt exists(const mini_bddt &u, unsigned var)
std::string cubes(const mini_bddt &u)
bool OneSat(const mini_bddt &v, std::map< unsigned, bool > &assignment)
mini_bddt substitute(const mini_bddt &where, unsigned var, const mini_bddt &by_what)
#define PRECONDITION_WITH_DIAGNOSTICS(CONDITION,...)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
#define POSTCONDITION_WITH_DIAGNOSTICS(CONDITION,...)
bool operator<(const reverse_keyt &) const