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