cprover
aigt Class Reference

#include <aig.h>

Inheritance diagram for aigt:
[legend]
Collaboration diagram for aigt:
[legend]

Public Types

typedef aig_nodet nodet
 
typedef std::vector< nodetnodest
 
typedef std::set< literalt::var_notterminal_sett
 
typedef std::map< literalt::var_not, terminal_settterminalst
 

Public Member Functions

 aigt ()
 
 ~aigt ()
 
void clear ()
 
void get_terminals (terminalst &terminals) const
 
const aig_nodetget_node (literalt l) const
 
aig_nodetget_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
 

Detailed Description

Definition at line 52 of file aig.h.

Member Typedef Documentation

§ nodest

typedef std::vector<nodet> aigt::nodest

Definition at line 64 of file aig.h.

§ nodet

Definition at line 63 of file aig.h.

§ terminal_sett

Definition at line 72 of file aig.h.

§ terminalst

Definition at line 73 of file aig.h.

Constructor & Destructor Documentation

§ aigt()

aigt::aigt ( )
inline

Definition at line 55 of file aig.h.

§ ~aigt()

aigt::~aigt ( )
inline

Definition at line 59 of file aig.h.

Member Function Documentation

§ clear()

void aigt::clear ( void  )
inline

Definition at line 67 of file aig.h.

Referenced by aig_plus_constraintst::clear().

§ dot_label()

std::string aigt::dot_label ( nodest::size_type  v) const

Definition at line 20 of file aig.cpp.

Referenced by output_dot_node().

§ empty()

bool aigt::empty ( ) const
inline

Definition at line 121 of file aig.h.

References aig_nodet::a, operator<<(), and size_type().

§ get_node() [1/2]

const aig_nodet& aigt::get_node ( literalt  l) const
inline

Definition at line 79 of file aig.h.

References literalt::var_no().

§ get_node() [2/2]

aig_nodet& aigt::get_node ( literalt  l)
inline

Definition at line 84 of file aig.h.

References literalt::var_no().

§ get_terminals()

void aigt::get_terminals ( terminalst terminals) const

Definition at line 25 of file aig.cpp.

References get_terminals_rec(), nodes, and size_type().

§ get_terminals_rec()

const aigt::terminal_sett & aigt::get_terminals_rec ( literalt::var_not  n,
terminalst terminals 
) const
protected

§ label()

std::string aigt::label ( nodest::size_type  v) const

Definition at line 15 of file aig.cpp.

Referenced by print().

§ new_and_node()

literalt aigt::new_and_node ( literalt  a,
literalt  b 
)
inline

Definition at line 114 of file aig.h.

Referenced by aig_prop_baset::land().

§ new_node()

literalt aigt::new_node ( )
inline

Definition at line 99 of file aig.h.

References aig_nodet::aig_nodet(), and literalt::set().

Referenced by aig_prop_baset::new_variable().

§ new_var_node()

literalt aigt::new_var_node ( )
inline

Definition at line 107 of file aig.h.

§ number_of_nodes()

nodest::size_type aigt::number_of_nodes ( ) const
inline

Definition at line 89 of file aig.h.

Referenced by aig_prop_baset::no_variables(), output_dot(), and print().

§ output_dot()

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().

§ output_dot_edge()

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().

§ 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().

§ print() [1/2]

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().

§ print() [2/2]

void aigt::print ( std::ostream &  out,
literalt  a 
) const

§ swap()

void aigt::swap ( aigt g)
inline

Definition at line 94 of file aig.h.

References nodes.

Member Data Documentation

§ nodes

nodest aigt::nodes

Definition at line 65 of file aig.h.

Referenced by get_terminals(), get_terminals_rec(), output_dot_node(), print(), and swap().


The documentation for this class was generated from the following files: