cprover
aig_plus_constraintst Class Reference

#include <aig.h>

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

Public Types

typedef std::vector< literaltconstraintst
 
- Public Types inherited from aigt
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

void clear ()
 
- Public Member Functions inherited from aigt
 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

constraintst constraints
 
- Public Attributes inherited from aigt
nodest nodes
 

Additional Inherited Members

- Protected Member Functions inherited from aigt
const std::set< literalt::var_not > & get_terminals_rec (literalt::var_not n, terminalst &terminals) const
 

Detailed Description

Definition at line 144 of file aig.h.

Member Typedef Documentation

§ constraintst

Definition at line 147 of file aig.h.

Member Function Documentation

§ clear()

void aig_plus_constraintst::clear ( void  )
inline

Definition at line 150 of file aig.h.

References aigt::clear().

Member Data Documentation

§ constraints

constraintst aig_plus_constraintst::constraints

Definition at line 148 of file aig.h.

Referenced by aig_prop_constraintt::l_set_to().


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