14 #ifndef CPROVER_SOLVERS_MINIBDD_MINIBDD_H 15 #define CPROVER_SOLVERS_MINIBDD_MINIBDD_H 74 unsigned _var,
unsigned _node_number,
89 void DumpDot(std::ostream &out,
bool supress_zero=
false)
const;
92 bool supress_zero=
false,
93 bool node_numbers=
true)
const;
116 typedef std::list<mini_bdd_nodet>
nodest;
133 typedef std::stack<mini_bdd_nodet *>
freet;
147 #include "miniBDD.inc" 149 #endif // CPROVER_SOLVERS_MINIBDD_MINIBDD_H
std::vector< var_table_entryt > var_tablet
mini_bddt & operator=(const mini_bddt &)
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
std::list< mini_bdd_nodet > nodest
mini_bddt substitute(const mini_bddt &where, unsigned var, const mini_bddt &by_what)
mini_bddt operator!() const
bool is_initialized() const
mini_bdd_nodet(class mini_bdd_mgrt *_mgr, unsigned _var, unsigned _node_number, const mini_bddt &_low, const mini_bddt &_high)
mini_bddt restrict(const mini_bddt &u, unsigned var, const bool value)
class mini_bdd_nodet * node
bool OneSat(const mini_bddt &v, std::map< unsigned, bool > &assignment)
var_table_entryt(const std::string &_label)
std::string cubes(const mini_bddt &u)
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
mini_bddt mk(unsigned var, const mini_bddt &low, const mini_bddt &high)
reverse_keyt(unsigned _var, const mini_bddt &_low, const mini_bddt &_high)
void DumpTable(std::ostream &out) const
const mini_bddt & low() const
class mini_bdd_mgrt * mgr
mini_bddt operator|(const mini_bddt &) const
std::stack< mini_bdd_nodet * > freet
std::size_t number_of_nodes()
bool operator<(const reverse_keyt &) const
mini_bddt exists(const mini_bddt &u, unsigned var)
std::map< reverse_keyt, mini_bdd_nodet * > reverse_mapt
void DumpDot(std::ostream &out, bool supress_zero=false) const