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 "namespace.h"
17 #include "std_expr.h"
18 
20 {
21  if(!expr.has_operands())
22  return true;
23 
24  exprt::operandst &operands=expr.operands();
25 
26  if(expr.type().id()!=ID_bool)
27  return true;
28 
29  if(expr.id()==ID_implies)
30  {
31  if(operands.size()!=2 ||
32  operands.front().type().id()!=ID_bool ||
33  operands.back().type().id()!=ID_bool)
34  return true;
35 
36  // turn a => b into !a || b
37 
38  expr.id(ID_or);
39  expr.op0() = boolean_negate(expr.op0());
40  simplify_node(expr.op0());
41  simplify_node(expr);
42  return false;
43  }
44  else if(expr.id()==ID_xor)
45  {
46  bool result=true;
47 
48  bool negate=false;
49 
50  for(exprt::operandst::const_iterator it=operands.begin();
51  it!=operands.end();)
52  {
53  if(it->type().id()!=ID_bool)
54  return true;
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=operands.erase(it);
69  result=false;
70  }
71  else
72  it++;
73  }
74 
75  if(operands.empty())
76  {
77  expr.make_bool(negate);
78  return false;
79  }
80  else if(operands.size()==1)
81  {
82  exprt tmp(operands.front());
83  if(negate)
84  tmp = boolean_negate(operands.front());
85  expr.swap(tmp);
86  return false;
87  }
88 
89  return result;
90  }
91  else if(expr.id()==ID_and || expr.id()==ID_or)
92  {
93  std::unordered_set<exprt, irep_hash> expr_set;
94 
95  bool result=true;
96 
97  for(exprt::operandst::const_iterator it=operands.begin();
98  it!=operands.end();)
99  {
100  if(it->type().id()!=ID_bool)
101  return true;
102 
103  bool is_true=it->is_true();
104  bool is_false=it->is_false();
105 
106  if(expr.id()==ID_and && is_false)
107  {
108  expr=false_exprt();
109  return false;
110  }
111  else if(expr.id()==ID_or && is_true)
112  {
113  expr=true_exprt();
114  return false;
115  }
116 
117  bool erase=
118  (expr.id()==ID_and ? is_true : is_false) ||
119  !expr_set.insert(*it).second;
120 
121  if(erase)
122  {
123  it=operands.erase(it);
124  result=false;
125  }
126  else
127  it++;
128  }
129 
130  // search for a and !a
131  for(const exprt &op : operands)
132  if(op.id()==ID_not &&
133  op.operands().size()==1 &&
134  op.type().id()==ID_bool &&
135  expr_set.find(op.op0())!=expr_set.end())
136  {
137  expr.make_bool(expr.id()==ID_or);
138  return false;
139  }
140 
141  if(operands.empty())
142  {
143  expr.make_bool(expr.id()==ID_and);
144  return false;
145  }
146  else if(operands.size()==1)
147  {
148  exprt tmp(operands.front());
149  expr.swap(tmp);
150  return false;
151  }
152 
153  return result;
154  }
155 
156  return true;
157 }
158 
160 {
161  if(expr.operands().size()!=1)
162  return true;
163 
164  exprt &op=expr.op0();
165 
166  if(expr.type().id()!=ID_bool ||
167  op.type().id()!=ID_bool)
168  return true;
169 
170  if(op.id()==ID_not) // (not not a) == a
171  {
172  if(op.operands().size()==1)
173  {
174  exprt tmp;
175  tmp.swap(op.op0());
176  expr.swap(tmp);
177  return false;
178  }
179  }
180  else if(op.is_false())
181  {
182  expr=true_exprt();
183  return false;
184  }
185  else if(op.is_true())
186  {
187  expr=false_exprt();
188  return false;
189  }
190  else if(op.id()==ID_and ||
191  op.id()==ID_or)
192  {
193  exprt tmp;
194  tmp.swap(op);
195  expr.swap(tmp);
196 
197  Forall_operands(it, expr)
198  {
199  *it = boolean_negate(*it);
200  simplify_node(*it);
201  }
202 
203  expr.id(expr.id()==ID_and?ID_or:ID_and);
204 
205  return false;
206  }
207  else if(op.id()==ID_notequal) // !(a!=b) <-> a==b
208  {
209  exprt tmp;
210  tmp.swap(op);
211  expr.swap(tmp);
212  expr.id(ID_equal);
213  return false;
214  }
215  else if(op.id()==ID_exists) // !(exists: a) <-> forall: not a
216  {
217  auto const &op_as_exists = to_exists_expr(op);
218  forall_exprt rewritten_op(
219  op_as_exists.symbol(), not_exprt(op_as_exists.where()));
220  simplify_node(rewritten_op.where());
221  expr = rewritten_op;
222  return false;
223  }
224 
225  return true;
226 }
simplify_exprt::simplify_node
bool simplify_node(exprt &expr)
Definition: simplify_expr.cpp:2113
simplify_expr_class.h
Forall_operands
#define Forall_operands(it, expr)
Definition: expr.h:26
forall_exprt
A forall expression.
Definition: std_expr.h:4777
exprt::make_bool
void make_bool(bool value)
Replace the expression by a Boolean expression representing value.
Definition: expr.cpp:109
exprt
Base class for all expressions.
Definition: expr.h:54
exprt::op0
exprt & op0()
Definition: expr.h:84
invariant.h
exprt::is_true
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:90
simplify_exprt::simplify_boolean
bool simplify_boolean(exprt &expr)
Definition: simplify_expr_boolean.cpp:19
namespace.h
exprt::is_false
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:99
expr.h
is_false
bool is_false(const literalt &l)
Definition: literal.h:196
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:68
quantifier_exprt::where
exprt & where()
Definition: std_expr.h:4729
exprt::has_operands
bool has_operands() const
Return true if there is at least one operand.
Definition: expr.h:75
simplify_exprt::simplify_not
bool simplify_not(exprt &expr)
Definition: simplify_expr_boolean.cpp:159
boolean_negate
exprt boolean_negate(const exprt &src)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true
Definition: expr_util.cpp:127
irept::swap
void swap(irept &irep)
Definition: irep.h:303
irept::id
const irep_idt & id() const
Definition: irep.h:259
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:57
false_exprt
The Boolean constant false.
Definition: std_expr.h:4452
expr_util.h
Deprecated expression utility functions.
exprt::operands
operandst & operands()
Definition: expr.h:78
to_exists_expr
const exists_exprt & to_exists_expr(const exprt &expr)
Definition: std_expr.h:4796
true_exprt
The Boolean constant true.
Definition: std_expr.h:4443
is_true
bool is_true(const literalt &l)
Definition: literal.h:197
std_expr.h
not_exprt
Boolean negation.
Definition: std_expr.h:3308