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_xor)
76  {
77  bool result=true;
78 
79  bool negate=false;
80 
81  for(exprt::operandst::const_iterator it=operands.begin();
82  it!=operands.end();)
83  {
84  if(it->type().id()!=ID_bool)
85  return true;
86 
87  bool erase;
88 
89  if(it->is_true())
90  {
91  erase=true;
92  negate=!negate;
93  }
94  else
95  erase=it->is_false();
96 
97  if(erase)
98  {
99  it=operands.erase(it);
100  result=false;
101  }
102  else
103  it++;
104  }
105 
106  if(operands.empty())
107  {
108  expr.make_bool(negate);
109  return false;
110  }
111  else if(operands.size()==1)
112  {
113  exprt tmp(operands.front());
114  if(negate)
115  tmp.make_not();
116  expr.swap(tmp);
117  return false;
118  }
119 
120  return result;
121  }
122  else if(expr.id()==ID_and || expr.id()==ID_or)
123  {
124  std::unordered_set<exprt, irep_hash> expr_set;
125 
126  bool result=true;
127 
128  for(exprt::operandst::const_iterator it=operands.begin();
129  it!=operands.end();)
130  {
131  if(it->type().id()!=ID_bool)
132  return true;
133 
134  bool is_true=it->is_true();
135  bool is_false=it->is_false();
136 
137  if(expr.id()==ID_and && is_false)
138  {
139  expr=false_exprt();
140  return false;
141  }
142  else if(expr.id()==ID_or && is_true)
143  {
144  expr=true_exprt();
145  return false;
146  }
147 
148  bool erase=
149  (expr.id()==ID_and ? is_true : is_false) ||
150  !expr_set.insert(*it).second;
151 
152  if(erase)
153  {
154  it=operands.erase(it);
155  result=false;
156  }
157  else
158  it++;
159  }
160 
161  // search for a and !a
162  for(const exprt &op : operands)
163  if(op.id()==ID_not &&
164  op.operands().size()==1 &&
165  op.type().id()==ID_bool &&
166  expr_set.find(op.op0())!=expr_set.end())
167  {
168  expr.make_bool(expr.id()==ID_or);
169  return false;
170  }
171 
172  if(operands.empty())
173  {
174  expr.make_bool(expr.id()==ID_and);
175  return false;
176  }
177  else if(operands.size()==1)
178  {
179  exprt tmp(operands.front());
180  expr.swap(tmp);
181  return false;
182  }
183 
184  return result;
185  }
186 
187  return true;
188 }
189 
191 {
192  if(expr.operands().size()!=1)
193  return true;
194 
195  exprt &op=expr.op0();
196 
197  if(expr.type().id()!=ID_bool ||
198  op.type().id()!=ID_bool)
199  return true;
200 
201  if(op.id()==ID_not) // (not not a) == a
202  {
203  if(op.operands().size()==1)
204  {
205  exprt tmp;
206  tmp.swap(op.op0());
207  expr.swap(tmp);
208  return false;
209  }
210  }
211  else if(op.is_false())
212  {
213  expr=true_exprt();
214  return false;
215  }
216  else if(op.is_true())
217  {
218  expr=false_exprt();
219  return false;
220  }
221  else if(op.id()==ID_and ||
222  op.id()==ID_or)
223  {
224  exprt tmp;
225  tmp.swap(op);
226  expr.swap(tmp);
227 
228  Forall_operands(it, expr)
229  {
230  it->make_not();
231  simplify_node(*it);
232  }
233 
234  expr.id(expr.id()==ID_and?ID_or:ID_and);
235 
236  return false;
237  }
238  else if(op.id()==ID_notequal) // !(a!=b) <-> a==b
239  {
240  exprt tmp;
241  tmp.swap(op);
242  expr.swap(tmp);
243  expr.id(ID_equal);
244  return false;
245  }
246  else if(op.id()==ID_exists) // !(exists: a) <-> forall: not a
247  {
248  assert(op.operands().size()==2);
249  exprt tmp;
250  tmp.swap(op);
251  expr.swap(tmp);
252  expr.id(ID_forall);
253  expr.op1().make_not();
254  simplify_node(expr.op1());
255  return false;
256  }
257 
258  return true;
259 }
bool is_true(const literalt &l)
Definition: literal.h:197
bool simplify_node(exprt &expr)
exprt & op0()
Definition: expr.h:72
bool is_false() const
Definition: expr.cpp:131
bool is_true() const
Definition: expr.cpp:124
typet & type()
Definition: expr.h:56
void make_bool(bool value)
Definition: expr.cpp:138
const irep_idt & id() const
Definition: irep.h:189
bool is_false(const literalt &l)
Definition: literal.h:196
The boolean constant true.
Definition: std_expr.h:4488
bool simplify_boolean(exprt &expr)
API to expression classes.
exprt & op1()
Definition: expr.h:75
bool has_operands() const
Definition: expr.h:63
The boolean constant false.
Definition: std_expr.h:4499
std::vector< exprt > operandst
Definition: expr.h:45
void make_not()
Definition: expr.cpp:91
Base class for all expressions.
Definition: expr.h:42
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:66