14 #ifndef CPROVER_SOLVERS_MINIBDD_MINIBDD_H 15 #define CPROVER_SOLVERS_MINIBDD_MINIBDD_H 74 unsigned _var,
unsigned _node_number,
78 void remove_reference();
89 void DumpDot(std::ostream &out,
bool supress_zero=
false)
const;
92 bool supress_zero=
false,
93 bool node_numbers=
true)
const;
94 void DumpTable(std::ostream &out)
const;
104 std::size_t number_of_nodes();
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 &)
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
friend class mini_bdd_nodet
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)
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 operator^(const mini_bddt &) const
const mini_bddt & low() const
class mini_bdd_mgrt * mgr
mini_bddt operator|(const mini_bddt &) const
std::stack< mini_bdd_nodet * > freet
tvt operator<(const interval_templatet< T > &a, const interval_templatet< T > &b)
mini_bddt exists(const mini_bddt &u, unsigned var)
std::map< reverse_keyt, mini_bdd_nodet * > reverse_mapt