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 <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