cprover
aig.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: AND-Inverter Graph
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_SOLVERS_PROP_AIG_H
13 #define CPROVER_SOLVERS_PROP_AIG_H
14 
15 #include <vector>
16 #include <set>
17 #include <map>
18 
19 #include <solvers/prop/literal.h>
20 
21 class aig_nodet
22 {
23 public:
25 
27  {
28  }
29 
30  bool is_and() const
31  {
32  return a.var_no()!=literalt::unused_var_no();
33  }
34 
35  bool is_var() const
36  {
37  return a.var_no()==literalt::unused_var_no();
38  }
39 
40  void make_and(literalt _a, literalt _b)
41  {
42  a=_a;
43  b=_b;
44  }
45 
46  void make_var()
47  {
48  a.set(literalt::unused_var_no(), false);
49  }
50 };
51 
52 class aigt
53 {
54 public:
55  aigt()
56  {
57  }
58 
60  {
61  }
62 
63  typedef aig_nodet nodet;
64  typedef std::vector<nodet> nodest;
65  nodest nodes;
66 
67  void clear()
68  {
69  nodes.clear();
70  }
71 
72  typedef std::set<literalt::var_not> terminal_sett;
73  typedef std::map<literalt::var_not, terminal_sett> terminalst;
74 
75  // produces the support set
76  // should get re-written
77  void get_terminals(terminalst &terminals) const;
78 
79  const aig_nodet &get_node(literalt l) const
80  {
81  return nodes[l.var_no()];
82  }
83 
85  {
86  return nodes[l.var_no()];
87  }
88 
90  {
91  return nodes.size();
92  }
93 
94  void swap(aigt &g)
95  {
96  nodes.swap(g.nodes);
97  }
98 
100  {
101  nodes.push_back(aig_nodet());
102  literalt l;
103  l.set(nodes.size()-1, false);
104  return l;
105  }
106 
108  {
109  literalt l=new_node();
110  nodes.back().make_var();
111  return l;
112  }
113 
115  {
116  literalt l=new_node();
117  nodes.back().make_and(a, b);
118  return l;
119  }
120 
121  bool empty() const
122  {
123  return nodes.empty();
124  }
125 
126  void print(std::ostream &out) const;
127  void print(std::ostream &out, literalt a) const;
128  void output_dot_node(std::ostream &out, nodest::size_type v) const;
129  void output_dot_edge(
130  std::ostream &out, nodest::size_type v, literalt l) const;
131  void output_dot(std::ostream &out) const;
132 
133  std::string label(nodest::size_type v) const;
134  std::string dot_label(nodest::size_type v) const;
135 
136 protected:
137  const std::set<literalt::var_not> &get_terminals_rec(
139  terminalst &terminals) const;
140 };
141 
142 std::ostream &operator << (std::ostream &, const aigt &);
143 
145 {
146 public:
147  typedef std::vector<literalt> constraintst;
148  constraintst constraints;
149 
150  void clear()
151  {
152  aigt::clear();
153  constraints.clear();
154  }
155 };
156 
157 #endif // CPROVER_SOLVERS_PROP_AIG_H
void make_var()
Definition: aig.h:46
literalt b
Definition: aig.h:24
unsigned var_not
Definition: literal.h:30
Definition: aig.h:52
static var_not unused_var_no()
Definition: literal.h:175
literalt new_var_node()
Definition: aig.h:107
unsignedbv_typet size_type()
Definition: c_types.cpp:57
std::vector< literalt > constraintst
Definition: aig.h:147
aig_nodet nodet
Definition: aig.h:63
aig_nodet & get_node(literalt l)
Definition: aig.h:84
bool is_and() const
Definition: aig.h:30
nodest::size_type number_of_nodes() const
Definition: aig.h:89
literalt a
Definition: aig.h:24
literalt new_and_node(literalt a, literalt b)
Definition: aig.h:114
void clear()
Definition: aig.h:67
Definition: aig.h:21
var_not var_no() const
Definition: literal.h:82
void set(var_not _l)
Definition: literal.h:92
~aigt()
Definition: aig.h:59
void make_and(literalt _a, literalt _b)
Definition: aig.h:40
literalt new_node()
Definition: aig.h:99
aig_nodet()
Definition: aig.h:26
aigt()
Definition: aig.h:55
bool is_var() const
Definition: aig.h:35
std::set< literalt::var_not > terminal_sett
Definition: aig.h:72
bool empty() const
Definition: aig.h:121
std::ostream & operator<<(std::ostream &, const aigt &)
Definition: aig.cpp:179
std::vector< nodet > nodest
Definition: aig.h:64
const aig_nodet & get_node(literalt l) const
Definition: aig.h:79
std::map< literalt::var_not, terminal_sett > terminalst
Definition: aig.h:73
nodest nodes
Definition: aig.h:65
void swap(aigt &g)
Definition: aig.h:94
constraintst constraints
Definition: aig.h:148