12 #ifndef CPROVER_SOLVERS_PROP_AIG_H 13 #define CPROVER_SOLVERS_PROP_AIG_H 73 typedef std::map<literalt::var_not, terminal_sett>
terminalst;
110 nodes.back().make_var();
117 nodes.back().make_and(a, b);
123 return nodes.empty();
126 void print(std::ostream &out)
const;
157 #endif // CPROVER_SOLVERS_PROP_AIG_H
const std::set< literalt::var_not > & get_terminals_rec(literalt::var_not n, terminalst &terminals) const
void output_dot(std::ostream &out) const
static var_not unused_var_no()
void print(std::ostream &out) const
unsignedbv_typet size_type()
std::vector< literalt > constraintst
aig_nodet & get_node(literalt l)
nodest::size_type number_of_nodes() const
literalt new_and_node(literalt a, literalt b)
void output_dot_node(std::ostream &out, nodest::size_type v) const
std::string label(nodest::size_type v) const
void make_and(literalt _a, literalt _b)
std::string dot_label(nodest::size_type v) const
void get_terminals(terminalst &terminals) const
std::set< literalt::var_not > terminal_sett
std::ostream & operator<<(std::ostream &, const aigt &)
std::vector< nodet > nodest
const aig_nodet & get_node(literalt l) const
std::map< literalt::var_not, terminal_sett > terminalst
void output_dot_edge(std::ostream &out, nodest::size_type v, literalt l) const