CBMC
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 "arith_tools.h"
12 #include "c_types.h"
13 #include "expr_util.h"
14 #include "mathematical_expr.h"
15 #include "namespace.h"
16 #include "std_expr.h"
17 
18 #include <unordered_set>
19 
21 {
22  if(!expr.has_operands())
23  return unchanged(expr);
24 
25  if(!expr.is_boolean())
26  return unchanged(expr);
27 
28  if(expr.id()==ID_implies)
29  {
30  const auto &implies_expr = to_implies_expr(expr);
31 
32  if(!implies_expr.op0().is_boolean() || !implies_expr.op1().is_boolean())
33  {
34  return unchanged(expr);
35  }
36 
37  // turn a => b into !a || b
38 
39  binary_exprt new_expr = implies_expr;
40  new_expr.id(ID_or);
41  new_expr.op0() = simplify_not(not_exprt(new_expr.op0()));
42  return changed(simplify_boolean(new_expr));
43  }
44  else if(expr.id()==ID_xor)
45  {
46  bool no_change = true;
47  bool negate = false;
48 
49  exprt::operandst new_operands = expr.operands();
50 
51  for(exprt::operandst::const_iterator it = new_operands.begin();
52  it != new_operands.end();)
53  {
54  if(!it->is_boolean())
55  return unchanged(expr);
56 
57  bool erase;
58 
59  if(it->is_true())
60  {
61  erase=true;
62  negate=!negate;
63  }
64  else
65  erase=it->is_false();
66 
67  if(erase)
68  {
69  it = new_operands.erase(it);
70  no_change = false;
71  }
72  else
73  it++;
74  }
75 
76  if(new_operands.empty())
77  {
78  return make_boolean_expr(negate);
79  }
80  else if(new_operands.size() == 1)
81  {
82  if(negate)
83  return changed(simplify_not(not_exprt(new_operands.front())));
84  else
85  return std::move(new_operands.front());
86  }
87 
88  if(!no_change)
89  {
90  auto tmp = expr;
91  tmp.operands() = std::move(new_operands);
92  return std::move(tmp);
93  }
94  }
95  else if(expr.id()==ID_and || expr.id()==ID_or)
96  {
97  std::unordered_set<exprt, irep_hash> expr_set;
98 
99  bool no_change = true;
100  bool may_be_reducible_to_interval =
101  expr.id() == ID_or && expr.operands().size() > 2;
102  bool may_be_reducible_to_singleton_interval =
103  expr.id() == ID_and && expr.operands().size() == 2;
104 
105  exprt::operandst new_operands = expr.operands();
106 
107  for(exprt::operandst::const_iterator it = new_operands.begin();
108  it != new_operands.end();)
109  {
110  if(!it->is_boolean())
111  return unchanged(expr);
112 
113  bool is_true=it->is_true();
114  bool is_false=it->is_false();
115 
116  if(expr.id()==ID_and && is_false)
117  {
118  return false_exprt();
119  }
120  else if(expr.id()==ID_or && is_true)
121  {
122  return true_exprt();
123  }
124 
125  bool erase=
126  (expr.id()==ID_and ? is_true : is_false) ||
127  !expr_set.insert(*it).second;
128 
129  if(erase)
130  {
131  it = new_operands.erase(it);
132  no_change = false;
133  }
134  else
135  {
136  if(may_be_reducible_to_interval)
137  may_be_reducible_to_interval = it->id() == ID_equal;
138  it++;
139  }
140  }
141 
142  // NOLINTNEXTLINE(whitespace/line_length)
143  // This block reduces singleton intervals like (value >= 255 && value <= 255)
144  // to just (value == 255). We also need to be careful with the operands
145  // as some of them are erased in the previous step. We proceed only if
146  // no operands have been erased (i.e. the expression structure has been
147  // preserved by previous simplification rounds.)
148  if(may_be_reducible_to_singleton_interval && new_operands.size() == 2)
149  {
150  struct boundst
151  {
152  mp_integer lower;
153  mp_integer higher;
154  exprt non_const_value;
155  };
156  boundst bounds;
157 
158  // Before we do anything else, we need to "pattern match" against the
159  // expression and make sure that it has the structure we're looking for.
160  // The structure we're looking for is going to be
161  // (value >= 255 && !(value >= 256)) -- 255, 256 values indicative.
162  // (this is because previous simplification runs will have transformed
163  // the less_than_or_equal expression to a not(greater_than_or_equal)
164  // expression)
165 
166  // matching (value >= 255)
167  auto const match_first_operand = [&bounds](const exprt &op) -> bool {
168  if(
169  const auto ge_expr =
170  expr_try_dynamic_cast<greater_than_or_equal_exprt>(op))
171  {
172  // The construction of these expressions ensures that the RHS
173  // is constant, therefore if we don't have a constant, it's a
174  // different expression, so we bail.
175  if(!ge_expr->rhs().is_constant())
176  return false;
177  if(
178  auto int_opt =
179  numeric_cast<mp_integer>(to_constant_expr(ge_expr->rhs())))
180  {
181  bounds.non_const_value = ge_expr->lhs();
182  bounds.lower = *int_opt;
183  return true;
184  }
185  return false;
186  }
187  return false;
188  };
189 
190  // matching !(value >= 256)
191  auto const match_second_operand = [&bounds](const exprt &op) -> bool {
192  if(const auto not_expr = expr_try_dynamic_cast<not_exprt>(op))
193  {
194  PRECONDITION(not_expr->operands().size() == 1);
195  if(
196  const auto ge_expr =
197  expr_try_dynamic_cast<greater_than_or_equal_exprt>(
198  not_expr->op()))
199  {
200  // If the rhs() is not constant, it has a different structure
201  // (e.g. i >= j)
202  if(!ge_expr->rhs().is_constant())
203  return false;
204  if(ge_expr->lhs() != bounds.non_const_value)
205  return false;
206  if(
207  auto int_opt =
208  numeric_cast<mp_integer>(to_constant_expr(ge_expr->rhs())))
209  {
210  bounds.higher = *int_opt - 1;
211  return true;
212  }
213  return false;
214  }
215  return false;
216  }
217  return false;
218  };
219 
220  // We need to match both operands, at the particular sequence we expect.
221  bool structure_matched = match_first_operand(new_operands[0]) &&
222  match_second_operand(new_operands[1]);
223 
224  if(structure_matched && bounds.lower == bounds.higher)
225  {
226  // If we are here, we have matched the structure we expected, so we can
227  // make some reasonable assumptions about where certain info we need is
228  // located at.
229  const auto ge_expr =
230  expr_dynamic_cast<greater_than_or_equal_exprt>(new_operands[0]);
231  equal_exprt new_expr{ge_expr.lhs(), ge_expr.rhs()};
232  return changed(new_expr);
233  }
234  }
235 
236  if(may_be_reducible_to_interval)
237  {
238  std::optional<symbol_exprt> symbol_opt;
239  std::set<mp_integer> values;
240  for(const exprt &op : new_operands)
241  {
242  equal_exprt eq = to_equal_expr(op);
243  if(eq.lhs().is_constant())
244  std::swap(eq.lhs(), eq.rhs());
245  if(auto s = expr_try_dynamic_cast<symbol_exprt>(eq.lhs()))
246  {
247  if(!symbol_opt.has_value())
248  symbol_opt = *s;
249 
250  if(*s == *symbol_opt)
251  {
252  if(auto c = expr_try_dynamic_cast<constant_exprt>(eq.rhs()))
253  {
254  constant_exprt c_tmp = *c;
255  if(c_tmp.type().id() == ID_c_enum_tag)
256  c_tmp.type() = ns.follow_tag(to_c_enum_tag_type(c_tmp.type()));
257  if(auto int_opt = numeric_cast<mp_integer>(c_tmp))
258  {
259  values.insert(*int_opt);
260  continue;
261  }
262  }
263  }
264  }
265 
266  symbol_opt.reset();
267  break;
268  }
269 
270  if(symbol_opt.has_value() && values.size() >= 3)
271  {
272  mp_integer lower = *values.begin();
273  mp_integer upper = *std::prev(values.end());
274  if(upper - lower + 1 == mp_integer{values.size()})
275  {
276  typet type = symbol_opt->type();
277  if(symbol_opt->type().id() == ID_c_enum_tag)
278  {
279  type = ns.follow_tag(to_c_enum_tag_type(symbol_opt->type()))
280  .underlying_type();
281  }
282 
284  from_integer(lower, type),
285  typecast_exprt::conditional_cast(*symbol_opt, type)};
287  typecast_exprt::conditional_cast(*symbol_opt, type),
288  from_integer(upper, type)};
289 
290  return and_exprt{lb, ub};
291  }
292  }
293  }
294 
295  // search for a and !a
296  for(const exprt &op : new_operands)
297  if(
298  op.id() == ID_not && op.is_boolean() &&
299  expr_set.find(to_not_expr(op).op()) != expr_set.end())
300  {
301  return make_boolean_expr(expr.id() == ID_or);
302  }
303 
304  if(new_operands.empty())
305  {
306  return make_boolean_expr(expr.id() == ID_and);
307  }
308  else if(new_operands.size() == 1)
309  {
310  return std::move(new_operands.front());
311  }
312 
313  if(!no_change)
314  {
315  auto tmp = expr;
316  tmp.operands() = std::move(new_operands);
317  return std::move(tmp);
318  }
319  }
320 
321  return unchanged(expr);
322 }
323 
325 {
326  const exprt &op = expr.op();
327 
328  if(!expr.is_boolean() || !op.is_boolean())
329  {
330  return unchanged(expr);
331  }
332 
333  if(op.id()==ID_not) // (not not a) == a
334  {
335  return to_not_expr(op).op();
336  }
337  else if(op.is_false())
338  {
339  return true_exprt();
340  }
341  else if(op.is_true())
342  {
343  return false_exprt();
344  }
345  else if(op.id()==ID_and ||
346  op.id()==ID_or)
347  {
348  exprt tmp = op;
349 
350  Forall_operands(it, tmp)
351  {
352  *it = simplify_not(not_exprt(*it));
353  }
354 
355  tmp.id(tmp.id() == ID_and ? ID_or : ID_and);
356 
357  return std::move(tmp);
358  }
359  else if(op.id()==ID_notequal) // !(a!=b) <-> a==b
360  {
361  exprt tmp = op;
362  tmp.id(ID_equal);
363  return std::move(tmp);
364  }
365  else if(op.id()==ID_exists) // !(exists: a) <-> forall: not a
366  {
367  auto const &op_as_exists = to_exists_expr(op);
368  return forall_exprt{op_as_exists.variables(),
369  simplify_not(not_exprt(op_as_exists.where()))};
370  }
371  else if(op.id() == ID_forall) // !(forall: a) <-> exists: not a
372  {
373  auto const &op_as_forall = to_forall_expr(op);
374  return exists_exprt{op_as_forall.variables(),
375  simplify_not(not_exprt(op_as_forall.where()))};
376  }
377 
378  return unchanged(expr);
379 }
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a typet to a c_enum_tag_typet.
Definition: c_types.h:377
Boolean AND.
Definition: std_expr.h:2120
A base class for binary expressions.
Definition: std_expr.h:638
exprt & lhs()
Definition: std_expr.h:668
exprt & op0()
Definition: expr.h:133
exprt & rhs()
Definition: std_expr.h:678
variablest & variables()
Definition: std_expr.h:3128
A constant literal expression.
Definition: std_expr.h:2990
Equality.
Definition: std_expr.h:1361
An exists expression.
Base class for all expressions.
Definition: expr.h:56
std::vector< exprt > operandst
Definition: expr.h:58
bool has_operands() const
Return true if there is at least one operand.
Definition: expr.h:91
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:27
bool is_boolean() const
Return whether the expression represents a Boolean.
Definition: expr.h:224
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:34
typet & type()
Return the type of the expression.
Definition: expr.h:84
bool is_constant() const
Return whether the expression is a constant.
Definition: expr.h:212
operandst & operands()
Definition: expr.h:94
The Boolean constant false.
Definition: std_expr.h:3072
A forall expression.
const irep_idt & id() const
Definition: irep.h:388
Binary less than or equal operator expression.
Definition: std_expr.h:870
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition: namespace.cpp:63
Boolean negation.
Definition: std_expr.h:2327
const namespacet & ns
static resultt changed(resultt<> result)
resultt simplify_boolean(const exprt &)
resultt simplify_not(const not_exprt &)
static resultt unchanged(exprt expr)
The Boolean constant true.
Definition: std_expr.h:3063
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:2076
The type of an expression, extends irept.
Definition: type.h:29
const exprt & op() const
Definition: std_expr.h:391
#define Forall_operands(it, expr)
Definition: expr.h:27
constant_exprt make_boolean_expr(bool value)
returns true_exprt if given true and false_exprt otherwise
Definition: expr_util.cpp:313
Deprecated expression utility functions.
bool is_false(const literalt &l)
Definition: literal.h:197
bool is_true(const literalt &l)
Definition: literal.h:198
API to expression classes for 'mathematical' expressions.
const exists_exprt & to_exists_expr(const exprt &expr)
const forall_exprt & to_forall_expr(const exprt &expr)
BigInt mp_integer
Definition: smt_terms.h:17
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
API to expression classes.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:3045
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
Definition: std_expr.h:2352
const equal_exprt & to_equal_expr(const exprt &expr)
Cast an exprt to an equal_exprt.
Definition: std_expr.h:1402
const implies_exprt & to_implies_expr(const exprt &expr)
Cast an exprt to a implies_exprt.
Definition: std_expr.h:2208