cprover
|
#include <aig.h>
Public Types | |
typedef aig_nodet | nodet |
typedef std::vector< nodet > | nodest |
typedef std::set< literalt::var_not > | terminal_sett |
typedef std::map< literalt::var_not, terminal_sett > | terminalst |
Public Member Functions | |
aigt () | |
~aigt () | |
void | clear () |
void | get_terminals (terminalst &terminals) const |
const aig_nodet & | get_node (literalt l) const |
aig_nodet & | get_node (literalt l) |
nodest::size_type | number_of_nodes () const |
void | swap (aigt &g) |
literalt | new_node () |
literalt | new_var_node () |
literalt | new_and_node (literalt a, literalt b) |
bool | empty () const |
void | print (std::ostream &out) const |
void | print (std::ostream &out, literalt a) const |
void | output_dot_node (std::ostream &out, nodest::size_type v) const |
void | output_dot_edge (std::ostream &out, nodest::size_type v, literalt l) const |
void | output_dot (std::ostream &out) const |
std::string | label (nodest::size_type v) const |
std::string | dot_label (nodest::size_type v) const |
Public Attributes | |
nodest | nodes |
Protected Member Functions | |
const std::set< literalt::var_not > & | get_terminals_rec (literalt::var_not n, terminalst &terminals) const |
typedef std::vector<nodet> aigt::nodest |
typedef aig_nodet aigt::nodet |
typedef std::set<literalt::var_not> aigt::terminal_sett |
typedef std::map<literalt::var_not, terminal_sett> aigt::terminalst |
|
inline |
Definition at line 67 of file aig.h.
Referenced by aig_plus_constraintst::clear().
std::string aigt::dot_label | ( | nodest::size_type | v | ) | const |
Definition at line 20 of file aig.cpp.
Referenced by output_dot_node().
|
inline |
Definition at line 121 of file aig.h.
References aig_nodet::a, operator<<(), and size_type().
Definition at line 79 of file aig.h.
References literalt::var_no().
Definition at line 84 of file aig.h.
References literalt::var_no().
void aigt::get_terminals | ( | terminalst & | terminals | ) | const |
Definition at line 25 of file aig.cpp.
References get_terminals_rec(), nodes, and size_type().
|
protected |
Definition at line 31 of file aig.cpp.
References aig_nodet::a, aig_nodet::b, aig_nodet::is_and(), literalt::is_constant(), nodes, and literalt::var_no().
Referenced by get_terminals().
std::string aigt::label | ( | nodest::size_type | v | ) | const |
Definition at line 114 of file aig.h.
Referenced by aig_prop_baset::land().
|
inline |
Definition at line 99 of file aig.h.
References aig_nodet::aig_nodet(), and literalt::set().
Referenced by aig_prop_baset::new_variable().
|
inline |
Definition at line 89 of file aig.h.
Referenced by aig_prop_baset::no_variables(), output_dot(), and print().
void aigt::output_dot | ( | std::ostream & | out | ) | const |
Definition at line 157 of file aig.cpp.
References number_of_nodes(), output_dot_node(), and size_type().
void aigt::output_dot_edge | ( | std::ostream & | out, |
nodest::size_type | v, | ||
literalt | l | ||
) | const |
Definition at line 133 of file aig.cpp.
References literalt::is_false(), literalt::is_true(), literalt::sign(), and literalt::var_no().
Referenced by output_dot_node().
void aigt::output_dot_node | ( | std::ostream & | out, |
nodest::size_type | v | ||
) | const |
Definition at line 114 of file aig.cpp.
References aig_nodet::a, aig_nodet::b, dot_label(), aig_nodet::is_and(), nodes, and output_dot_edge().
Referenced by output_dot().
void aigt::print | ( | std::ostream & | out | ) | const |
Definition at line 167 of file aig.cpp.
References number_of_nodes(), literalt::set(), and size_type().
Referenced by operator<<(), and print().
void aigt::print | ( | std::ostream & | out, |
literalt | a | ||
) | const |
Definition at line 69 of file aig.cpp.
References aig_nodet::a, aig_nodet::b, const_literal(), aig_nodet::is_and(), aig_nodet::is_var(), label(), nodes, print(), literalt::sign(), and literalt::var_no().
nodest aigt::nodes |
Definition at line 65 of file aig.h.
Referenced by get_terminals(), get_terminals_rec(), output_dot_node(), print(), and swap().