CBMC: /home/runner/work/cbmc/cbmc/src/util/simplify_expr_boolean.cpp Source File

CBMC
Loading...
Searching...
No Matches
simplify_expr_boolean.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: 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
40 new_expr.id(ID_or);
43 }
44 else if(expr.id()==ID_xor)
45 {
46 bool no_change = true;
47 bool negate = false;
48
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 == true)
60 {
61 erase=true;
62 negate=!negate;
63 }
64 else
65 erase = *it == 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)
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;
101 expr.id() == ID_or && expr.operands().size() > 2;
103 expr.id() == ID_and && expr.operands().size() == 2;
104
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 == true;
114 bool is_false = *it == 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 {
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.)
149 {
150 struct boundst
151 {
152 mp_integer lower;
155 };
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 =
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 =
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 =
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 =
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.
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 =
231 equal_exprt new_expr{ge_expr.lhs(), ge_expr.rhs()};
232 return changed(new_expr);
233 }
234 }
235
237 {
238 std::optional<symbol_exprt> symbol_opt;
239 std::set<mp_integer> values;
240 for(const exprt &op : new_operands)
241 {
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 {
253 {
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()));
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),
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 == false)
338 {
339 return true_exprt();
340 }
341 else if(op == 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
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(),
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(),
376 }
377
378 return unchanged(expr);
379}
380
381simplify_exprt::resultt<>
383{
384 const exprt &where = expr.where();
385
386 if(!expr.is_boolean() || !where.is_boolean())
387 {
388 return unchanged(expr);
389 }
390
391 // the following simplification only holds when the domain is non-empty
392 if(
393 (where == false || where == true) &&
394 std::all_of(
395 expr.variables().begin(),
396 expr.variables().end(),
397 [](const symbol_exprt &v)
398 {
399 return v.type().id() == ID_integer || v.type().id() == ID_rational ||
400 v.type().id() == ID_real || v.type().id() == ID_bool ||
401 (can_cast_type<bitvector_typet>(v.type()) &&
402 to_bitvector_type(v.type()).get_width() > 0);
403 }))
404 {
405 return where;
406 }
407
408 return unchanged(expr);
409}
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
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:566
Boolean AND All operands must be boolean, and the result is always boolean.
Definition std_expr.h:2043
A base class for binary expressions.
Definition std_expr.h:649
exprt & where()
Definition std_expr.h:3201
variablest & variables()
Definition std_expr.h:3191
A constant literal expression.
Definition std_expr.h:3007
Equality.
Definition std_expr.h:1339
An exists expression.
Base class for all expressions.
Definition expr.h:57
std::vector< exprt > operandst
Definition expr.h:59
bool has_operands() const
Return true if there is at least one operand.
Definition expr.h:92
bool is_boolean() const
Return whether the expression represents a Boolean.
Definition expr.h:229
operandst & operands()
Definition expr.h:95
The Boolean constant false.
Definition std_expr.h:3135
A forall expression.
const irep_idt & id() const
Definition irep.h:388
Binary less than or equal operator expression.
Definition std_expr.h:891
Boolean negation.
Definition std_expr.h:2388
A base class for quantifier expressions.
const namespacet & ns
resultt simplify_quantifier_expr(const quantifier_exprt &)
Try to simplify exists/forall to a constant expression.
static resultt changed(resultt<> result)
resultt simplify_boolean(const exprt &)
resultt simplify_not(const not_exprt &)
static resultt unchanged(exprt expr)
Expression to hold a symbol (variable)
Definition std_expr.h:132
The Boolean constant true.
Definition std_expr.h:3126
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition std_expr.h:2003
The type of an expression, extends irept.
Definition type.h:29
const exprt & op() const
Definition std_expr.h:394
#define Forall_operands(it, expr)
Definition expr.h:28
constant_exprt make_boolean_expr(bool value)
returns true_exprt if given true and false_exprt otherwise
Definition expr_util.cpp:308
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)
#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:3078
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
Definition std_expr.h:2408
const implies_exprt & to_implies_expr(const exprt &expr)
Cast an exprt to a implies_exprt.
Definition std_expr.h:2174
const equal_exprt & to_equal_expr(const exprt &expr)
Cast an exprt to an equal_exprt.
Definition std_expr.h:1375

AltStyle によって変換されたページ (->オリジナル) /