cprover
simplify_expr_boolean.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 "simplify_expr_class.h"
10 
11 #include <cassert>
12 #include <unordered_set>
13 
14 #include "expr.h"
15 #include "namespace.h"
16 #include "std_expr.h"
17 
19 {
20  if(!expr.has_operands())
21  return true;
22 
23  exprt::operandst &operands=expr.operands();
24 
25  if(expr.type().id()!=ID_bool)
26  return true;
27 
28  if(expr.id()==ID_implies)
29  {
30  if(operands.size()!=2 ||
31  operands.front().type().id()!=ID_bool ||
32  operands.back().type().id()!=ID_bool)
33  return true;
34 
35  // turn a => b into !a || b
36 
37  expr.id(ID_or);
38  expr.op0().make_not();
39  simplify_node(expr.op0());
40  simplify_node(expr);
41  return false;
42  }
43  else if(expr.id()==ID_iff)
44  {
45  if(operands.size()!=2 ||
46  operands.front().type().id()!=ID_bool ||
47  operands.back().type().id()!=ID_bool)
48  return true;
49 
50  if(operands.front().is_false())
51  {
52  expr.id(ID_not);
53  operands.erase(operands.begin());
54  return false;
55  }
56  else if(operands.front().is_true())
57  {
58  exprt tmp(operands.back());
59  expr.swap(tmp);
60  return false;
61  }
62  else if(operands.back().is_false())
63  {
64  expr.id(ID_not);
65  operands.erase(++operands.begin());
66  return false;
67  }
68  else if(operands.back().is_true())
69  {
70  exprt tmp(operands.front());
71  expr.swap(tmp);
72  return false;
73  }
74  }
75  else if(expr.id()==ID_or ||
76  expr.id()==ID_and ||
77  expr.id()==ID_xor)
78  {
79  if(operands.empty())
80  return true;
81 
82  bool result=true;
83 
84  exprt::operandst::const_iterator last;
85  bool last_set=false;
86 
87  bool negate=false;
88 
89  for(exprt::operandst::iterator it=operands.begin();
90  it!=operands.end();)
91  {
92  if(it->type().id()!=ID_bool)
93  return true;
94 
95  bool is_true=it->is_true();
96  bool is_false=it->is_false();
97 
98  if(expr.id()==ID_and && is_false)
99  {
100  expr=false_exprt();
101  return false;
102  }
103  else if(expr.id()==ID_or && is_true)
104  {
105  expr=true_exprt();
106  return false;
107  }
108 
109  bool erase;
110 
111  if(expr.id()==ID_and)
112  erase=is_true;
113  else if(is_true && expr.id()==ID_xor)
114  {
115  erase=true;
116  negate=!negate;
117  }
118  else
119  erase=is_false;
120 
121  if(last_set && *it==*last &&
122  (expr.id()==ID_or || expr.id()==ID_and))
123  erase=true; // erase duplicate operands
124 
125  if(erase)
126  {
127  it=operands.erase(it);
128  result=false;
129  }
130  else
131  {
132  last=it;
133  last_set=true;
134  it++;
135  }
136  }
137 
138  // search for a and !a
139  if(expr.id()==ID_and || expr.id()==ID_or)
140  {
141  // first gather all the a's with !a
142 
143  std::unordered_set<exprt, irep_hash> expr_set;
144 
145  forall_operands(it, expr)
146  if(it->id()==ID_not &&
147  it->operands().size()==1 &&
148  it->type().id()==ID_bool)
149  expr_set.insert(it->op0());
150 
151  // now search for a
152 
153  if(!expr_set.empty())
154  {
155  forall_operands(it, expr)
156  {
157  if(it->id()!=ID_not &&
158  expr_set.find(*it)!=expr_set.end())
159  {
160  expr.make_bool(expr.id()==ID_or);
161  return false;
162  }
163  }
164  }
165  }
166 
167  if(operands.empty())
168  {
169  if(expr.id()==ID_and || negate)
170  expr=true_exprt();
171  else
172  expr=false_exprt();
173 
174  return false;
175  }
176  else if(operands.size()==1)
177  {
178  if(negate)
179  expr.op0().make_not();
180  exprt tmp(operands.front());
181  expr.swap(tmp);
182  return false;
183  }
184 
185  return result;
186  }
187 
188  return true;
189 }
190 
192 {
193  if(expr.operands().size()!=1)
194  return true;
195 
196  exprt &op=expr.op0();
197 
198  if(expr.type().id()!=ID_bool ||
199  op.type().id()!=ID_bool)
200  return true;
201 
202  if(op.id()==ID_not) // (not not a) == a
203  {
204  if(op.operands().size()==1)
205  {
206  exprt tmp;
207  tmp.swap(op.op0());
208  expr.swap(tmp);
209  return false;
210  }
211  }
212  else if(op.is_false())
213  {
214  expr=true_exprt();
215  return false;
216  }
217  else if(op.is_true())
218  {
219  expr=false_exprt();
220  return false;
221  }
222  else if(op.id()==ID_and ||
223  op.id()==ID_or)
224  {
225  exprt tmp;
226  tmp.swap(op);
227  expr.swap(tmp);
228 
229  Forall_operands(it, expr)
230  {
231  it->make_not();
232  simplify_node(*it);
233  }
234 
235  expr.id(expr.id()==ID_and?ID_or:ID_and);
236 
237  return false;
238  }
239  else if(op.id()==ID_notequal) // !(a!=b) <-> a==b
240  {
241  exprt tmp;
242  tmp.swap(op);
243  expr.swap(tmp);
244  expr.id(ID_equal);
245  return false;
246  }
247  else if(op.id()==ID_exists) // !(exists: a) <-> forall: not a
248  {
249  assert(op.operands().size()==2);
250  exprt tmp;
251  tmp.swap(op);
252  expr.swap(tmp);
253  expr.id(ID_forall);
254  expr.op1().make_not();
255  simplify_node(expr.op1());
256  return false;
257  }
258 
259  return true;
260 }
bool simplify_node(exprt &expr)
exprt & op0()
Definition: expr.h:84
bool is_false() const
Definition: expr.cpp:140
bool is_true() const
Definition: expr.cpp:133
typet & type()
Definition: expr.h:60
void make_bool(bool value)
Definition: expr.cpp:147
const irep_idt & id() const
Definition: irep.h:189
The boolean constant true.
Definition: std_expr.h:3742
bool simplify_boolean(exprt &expr)
API to expression classes.
exprt & op1()
Definition: expr.h:87
#define forall_operands(it, expr)
Definition: expr.h:17
bool has_operands() const
Definition: expr.h:67
The boolean constant false.
Definition: std_expr.h:3753
std::vector< exprt > operandst
Definition: expr.h:49
void make_not()
Definition: expr.cpp:100
Base class for all expressions.
Definition: expr.h:46
void swap(irept &irep)
Definition: irep.h:231
#define Forall_operands(it, expr)
Definition: expr.h:23
bool simplify_not(exprt &expr)
operandst & operands()
Definition: expr.h:70