cprover
aig.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 #include "aig.h"
10 
11 #include <cassert>
12 #include <ostream>
13 #include <string>
14 
15 std::string aigt::label(nodest::size_type v) const
16 {
17  return "var("+std::to_string(v)+")";
18 }
19 
20 std::string aigt::dot_label(nodest::size_type v) const
21 {
22  return "var("+std::to_string(v)+")";
23 }
24 
25 void aigt::get_terminals(terminalst &terminals) const
26 {
27  for(nodest::size_type n=0; n<nodes.size(); n++)
28  get_terminals_rec(n, terminals);
29 }
30 
33  terminalst &terminals) const
34 {
35  terminalst::iterator it=terminals.find(n);
36 
37  if(it!=terminals.end())
38  return it->second; // already done
39 
40  assert(n<nodes.size());
41  const aig_nodet &node=nodes[n];
42 
43  terminal_sett &t=terminals[n];
44 
45  if(node.is_and())
46  {
47  if(!node.a.is_constant())
48  {
49  const std::set<literalt::var_not> &ta=
50  get_terminals_rec(node.a.var_no(), terminals);
51  t.insert(ta.begin(), ta.end());
52  }
53 
54  if(!node.b.is_constant())
55  {
56  const std::set<literalt::var_not> &tb=
57  get_terminals_rec(node.b.var_no(), terminals);
58  t.insert(tb.begin(), tb.end());
59  }
60  }
61  else // this is a terminal
62  {
63  t.insert(n);
64  }
65 
66  return t;
67 }
68 
70  std::ostream &out,
71  literalt a) const
72 {
73  if(a==const_literal(false))
74  {
75  out << "FALSE";
76  return;
77  }
78  else if(a==const_literal(true))
79  {
80  out << "TRUE";
81  return;
82  }
83 
84  literalt::var_not node_nr=a.var_no();
85 
86  {
87  const aig_nodet &node=nodes[node_nr];
88 
89  if(node.is_and())
90  {
91  if(a.sign())
92  out << "!(";
93  print(out, node.a);
94  out << " & ";
95  print(out, node.b);
96  if(a.sign())
97  out << ")";
98  }
99  else if(node.is_var())
100  {
101  if(a.sign())
102  out << "!";
103  out << label(node_nr);\
104  }
105  else
106  {
107  if(a.sign())
108  out << "!";
109  out << "unknown(" << node_nr << ")";
110  }
111  }
112 }
113 
115  std::ostream &out,
116  nodest::size_type v) const
117 {
118  const aig_nodet &node=nodes[v];
119 
120  if(node.is_and())
121  {
122  out << v << " [label=\"" << v << "\"]" << "\n";
123  output_dot_edge(out, v, node.a);
124  output_dot_edge(out, v, node.b);
125  }
126  else // the node is a terminal
127  {
128  out << v << " [label=\"" << dot_label(v) << "\""
129  << ",shape=box]" << "\n";
130  }
131 }
132 
134  std::ostream &out,
136  literalt l) const
137 {
138  if(l.is_true())
139  {
140  out << "TRUE -> " << v;
141  }
142  else if(l.is_false())
143  {
144  out << "TRUE -> " << v;
145  out << " [arrowhead=odiamond]";
146  }
147  else
148  {
149  out << l.var_no() << " -> " << v;
150  if(l.sign())
151  out << " [arrowhead=odiamond]";
152  }
153 
154  out << "\n";
155 }
156 
157 void aigt::output_dot(std::ostream &out) const
158 {
159  // constant TRUE
160  out << "TRUE [label=\"TRUE\", shape=box]" << "\n";
161 
162  // now the nodes
163  for(nodest::size_type n=0; n<number_of_nodes(); n++)
164  output_dot_node(out, n);
165 }
166 
167 void aigt::print(std::ostream &out) const
168 {
169  for(nodest::size_type n=0; n<number_of_nodes(); n++)
170  {
171  out << "n" << n << " = ";
172  literalt l;
173  l.set(n, false);
174  print(out, l);
175  out << "\n";
176  }
177 }
178 
179 std::ostream &operator << (std::ostream &out, const aigt &aig)
180 {
181  aig.print(out);
182  return out;
183 }
const std::set< literalt::var_not > & get_terminals_rec(literalt::var_not n, terminalst &terminals) const
Definition: aig.cpp:31
void output_dot(std::ostream &out) const
Definition: aig.cpp:157
literalt b
Definition: aig.h:24
unsigned var_not
Definition: literal.h:30
Definition: aig.h:52
std::ostream & operator<<(std::ostream &out, const aigt &aig)
Definition: aig.cpp:179
void print(std::ostream &out) const
Definition: aig.cpp:167
unsignedbv_typet size_type()
Definition: c_types.cpp:57
bool is_and() const
Definition: aig.h:30
nodest::size_type number_of_nodes() const
Definition: aig.h:89
AND-Inverter Graph.
literalt a
Definition: aig.h:24
bool is_true() const
Definition: literal.h:155
Definition: aig.h:21
var_not var_no() const
Definition: literal.h:82
void set(var_not _l)
Definition: literal.h:92
void output_dot_node(std::ostream &out, nodest::size_type v) const
Definition: aig.cpp:114
std::string label(nodest::size_type v) const
Definition: aig.cpp:15
literalt const_literal(bool value)
Definition: literal.h:187
std::string dot_label(nodest::size_type v) const
Definition: aig.cpp:20
void get_terminals(terminalst &terminals) const
Definition: aig.cpp:25
bool is_constant() const
Definition: literal.h:165
bool sign() const
Definition: literal.h:87
bool is_var() const
Definition: aig.h:35
std::set< literalt::var_not > terminal_sett
Definition: aig.h:72
std::map< literalt::var_not, terminal_sett > terminalst
Definition: aig.h:73
void output_dot_edge(std::ostream &out, nodest::size_type v, literalt l) const
Definition: aig.cpp:133
nodest nodes
Definition: aig.h:65
bool is_false() const
Definition: literal.h:160