12 #ifndef CPROVER_SOLVERS_PROP_AIG_H 13 #define CPROVER_SOLVERS_PROP_AIG_H 73 typedef std::map<literalt::var_not, terminal_sett>
terminalst;
77 void get_terminals(terminalst &terminals)
const;
103 l.
set(nodes.size()-1,
false);
110 nodes.back().make_var();
117 nodes.back().make_and(a, b);
123 return nodes.empty();
126 void print(std::ostream &out)
const;
127 void print(std::ostream &out,
literalt a)
const;
129 void output_dot_edge(
131 void output_dot(std::ostream &out)
const;
137 const std::set<literalt::var_not> &get_terminals_rec(
139 terminalst &terminals)
const;
157 #endif // CPROVER_SOLVERS_PROP_AIG_H
static var_not unused_var_no()
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 make_and(literalt _a, literalt _b)
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