cprover
simplify_expr_boolean.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
10
11#include <unordered_set>
12
13#include "expr_util.h"
14#include "mathematical_expr.h"
15#include "std_expr.h"
16
18{
19 if(!expr.has_operands())
20 return unchanged(expr);
21
22 if(expr.type().id()!=ID_bool)
23 return unchanged(expr);
24
25 if(expr.id()==ID_implies)
26 {
27 const auto &implies_expr = to_implies_expr(expr);
28
29 if(
30 implies_expr.op0().type().id() != ID_bool ||
31 implies_expr.op1().type().id() != ID_bool)
32 {
33 return unchanged(expr);
34 }
35
36 // turn a => b into !a || b
37
38 binary_exprt new_expr = implies_expr;
39 new_expr.id(ID_or);
40 new_expr.op0() = simplify_not(not_exprt(new_expr.op0()));
41 return changed(simplify_boolean(new_expr));
42 }
43 else if(expr.id()==ID_xor)
44 {
45 bool no_change = true;
46 bool negate = false;
47
48 exprt::operandst new_operands = expr.operands();
49
50 for(exprt::operandst::const_iterator it = new_operands.begin();
51 it != new_operands.end();)
52 {
53 if(it->type().id()!=ID_bool)
54 return unchanged(expr);
55
56 bool erase;
57
58 if(it->is_true())
59 {
60 erase=true;
61 negate=!negate;
62 }
63 else
64 erase=it->is_false();
65
66 if(erase)
67 {
68 it = new_operands.erase(it);
69 no_change = false;
70 }
71 else
72 it++;
73 }
74
75 if(new_operands.empty())
76 {
77 return make_boolean_expr(negate);
78 }
79 else if(new_operands.size() == 1)
80 {
81 if(negate)
82 return changed(simplify_not(not_exprt(new_operands.front())));
83 else
84 return std::move(new_operands.front());
85 }
86
87 if(!no_change)
88 {
89 auto tmp = expr;
90 tmp.operands() = std::move(new_operands);
91 return std::move(tmp);
92 }
93 }
94 else if(expr.id()==ID_and || expr.id()==ID_or)
95 {
96 std::unordered_set<exprt, irep_hash> expr_set;
97
98 bool no_change = true;
99
100 exprt::operandst new_operands = expr.operands();
101
102 for(exprt::operandst::const_iterator it = new_operands.begin();
103 it != new_operands.end();)
104 {
105 if(it->type().id()!=ID_bool)
106 return unchanged(expr);
107
108 bool is_true=it->is_true();
109 bool is_false=it->is_false();
110
111 if(expr.id()==ID_and && is_false)
112 {
113 return false_exprt();
114 }
115 else if(expr.id()==ID_or && is_true)
116 {
117 return true_exprt();
118 }
119
120 bool erase=
121 (expr.id()==ID_and ? is_true : is_false) ||
122 !expr_set.insert(*it).second;
123
124 if(erase)
125 {
126 it = new_operands.erase(it);
127 no_change = false;
128 }
129 else
130 it++;
131 }
132
133 // search for a and !a
134 for(const exprt &op : new_operands)
135 if(
136 op.id() == ID_not && op.type().id() == ID_bool &&
137 expr_set.find(to_not_expr(op).op()) != expr_set.end())
138 {
139 return make_boolean_expr(expr.id() == ID_or);
140 }
141
142 if(new_operands.empty())
143 {
144 return make_boolean_expr(expr.id() == ID_and);
145 }
146 else if(new_operands.size() == 1)
147 {
148 return std::move(new_operands.front());
149 }
150
151 if(!no_change)
152 {
153 auto tmp = expr;
154 tmp.operands() = std::move(new_operands);
155 return std::move(tmp);
156 }
157 }
158
159 return unchanged(expr);
160}
161
163{
164 const exprt &op = expr.op();
165
166 if(expr.type().id()!=ID_bool ||
167 op.type().id()!=ID_bool)
168 {
169 return unchanged(expr);
170 }
171
172 if(op.id()==ID_not) // (not not a) == a
173 {
174 return to_not_expr(op).op();
175 }
176 else if(op.is_false())
177 {
178 return true_exprt();
179 }
180 else if(op.is_true())
181 {
182 return false_exprt();
183 }
184 else if(op.id()==ID_and ||
185 op.id()==ID_or)
186 {
187 exprt tmp = op;
188
189 Forall_operands(it, tmp)
190 {
191 *it = simplify_not(not_exprt(*it));
192 }
193
194 tmp.id(tmp.id() == ID_and ? ID_or : ID_and);
195
196 return std::move(tmp);
197 }
198 else if(op.id()==ID_notequal) // !(a!=b) <-> a==b
199 {
200 exprt tmp = op;
201 tmp.id(ID_equal);
202 return std::move(tmp);
203 }
204 else if(op.id()==ID_exists) // !(exists: a) <-> forall: not a
205 {
206 auto const &op_as_exists = to_exists_expr(op);
207 return forall_exprt{op_as_exists.variables(),
208 simplify_not(not_exprt(op_as_exists.where()))};
209 }
210 else if(op.id() == ID_forall) // !(forall: a) <-> exists: not a
211 {
212 auto const &op_as_forall = to_forall_expr(op);
213 return exists_exprt{op_as_forall.variables(),
214 simplify_not(not_exprt(op_as_forall.where()))};
215 }
216
217 return unchanged(expr);
218}
A base class for binary expressions.
Definition: std_expr.h:550
exprt & op0()
Definition: expr.h:99
variablest & variables()
Definition: std_expr.h:2921
An exists expression.
Base class for all expressions.
Definition: expr.h:54
std::vector< exprt > operandst
Definition: expr.h:56
bool has_operands() const
Return true if there is at least one operand.
Definition: expr.h:89
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:33
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:42
typet & type()
Return the type of the expression.
Definition: expr.h:82
operandst & operands()
Definition: expr.h:92
The Boolean constant false.
Definition: std_expr.h:2865
A forall expression.
const irep_idt & id() const
Definition: irep.h:396
Boolean negation.
Definition: std_expr.h:2181
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:2856
const exprt & op() const
Definition: std_expr.h:293
#define Forall_operands(it, expr)
Definition: expr.h:25
constant_exprt make_boolean_expr(bool value)
returns true_exprt if given true and false_exprt otherwise
Definition: expr_util.cpp:283
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)
API to expression classes.
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
Definition: std_expr.h:2206
const implies_exprt & to_implies_expr(const exprt &expr)
Cast an exprt to a implies_exprt.
Definition: std_expr.h:2062