CBMC
guard_expr.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Symbolic Execution
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "guard_expr.h"
13 
14 #include <util/expr_util.h>
15 #include <util/invariant.h>
16 #include <util/std_expr.h>
17 
19 {
20  if(is_true())
21  {
22  // do nothing
23  return expr;
24  }
25  else
26  {
27  if(expr.is_false())
28  {
29  return boolean_negate(as_expr());
30  }
31  else
32  {
33  return implies_exprt{as_expr(), expr};
34  }
35  }
36 }
37 
38 void guard_exprt::add(const exprt &expr)
39 {
41 
42  if(is_false() || expr.is_true())
43  return;
44  else if(is_true() || expr.is_false())
45  {
46  this->expr = expr;
47 
48  return;
49  }
50  else if(this->expr.id() != ID_and)
51  {
52  and_exprt a({this->expr});
53  this->expr = a;
54  }
55 
56  exprt::operandst &op = this->expr.operands();
57 
58  if(expr.id() == ID_and)
59  op.insert(op.end(), expr.operands().begin(), expr.operands().end());
60  else
61  op.push_back(expr);
62 }
63 
65 {
66  if(g1.expr.id() != ID_and)
67  {
68  if(g2.expr.id() != ID_and)
69  {
70  if(g1.expr == g2.expr)
71  g1.expr = true_exprt{};
72  }
73  else
74  {
75  for(const auto &op : g2.expr.operands())
76  {
77  if(g1.expr == op)
78  {
79  g1.expr = true_exprt{};
80  break;
81  }
82  }
83  }
84 
85  return g1;
86  }
87 
88  if(g2.expr.id() != ID_and)
89  {
90  exprt::operandst &op1 = g1.expr.operands();
91  for(exprt::operandst::iterator it = op1.begin(); it != op1.end(); ++it)
92  {
93  if(g1.expr == g2.expr)
94  {
95  op1.erase(it);
96  break;
97  }
98  }
99 
100  return g1;
101  }
102 
103  exprt g2_sorted = g2.as_expr();
104 
105  exprt::operandst &op1 = g1.expr.operands();
106  const exprt::operandst &op2 = g2_sorted.operands();
107 
108  exprt::operandst::iterator it1 = op1.begin();
109  for(exprt::operandst::const_iterator it2 = op2.begin(); it2 != op2.end();
110  ++it2)
111  {
112  if(it1 != op1.end() && *it1 == *it2)
113  it1 = op1.erase(it1);
114  else
115  break;
116  }
117 
118  g1.expr = conjunction(op1);
119 
120  return g1;
121 }
122 
124 {
125  if(is_true() || is_false() || other_guard.is_true() || other_guard.is_false())
126  return true;
127  if(expr.id() == ID_and && other_guard.expr.id() == ID_and)
128  return true;
129  if(other_guard.expr == boolean_negate(expr))
130  return true;
131  return false;
132 }
133 
135 {
136  if(g2.is_false() || g1.is_true())
137  return g1;
138  if(g1.is_false() || g2.is_true())
139  {
140  g1.expr = g2.expr;
141  return g1;
142  }
143 
144  if(g1.expr.id() != ID_and || g2.expr.id() != ID_and)
145  {
146  exprt tmp(boolean_negate(g2.as_expr()));
147 
148  if(tmp == g1.as_expr())
149  g1.expr = true_exprt();
150  else
151  g1.expr = or_exprt(g1.as_expr(), g2.as_expr());
152 
153  // TODO: make simplify more capable and apply here
154 
155  return g1;
156  }
157 
158  // find common prefix
159  exprt g2_sorted = g2.as_expr();
160 
161  exprt::operandst &op1 = g1.expr.operands();
162  const exprt::operandst &op2 = g2_sorted.operands();
163 
164  exprt::operandst n_op1, n_op2;
165  n_op1.reserve(op1.size());
166  n_op2.reserve(op2.size());
167 
168  exprt::operandst::iterator it1 = op1.begin();
169  for(exprt::operandst::const_iterator it2 = op2.begin(); it2 != op2.end();
170  ++it2)
171  {
172  while(it1 != op1.end() && *it1 < *it2)
173  {
174  n_op1.push_back(*it1);
175  it1 = op1.erase(it1);
176  }
177  if(it1 != op1.end() && *it1 == *it2)
178  ++it1;
179  else
180  n_op2.push_back(*it2);
181  }
182  while(it1 != op1.end())
183  {
184  n_op1.push_back(*it1);
185  it1 = op1.erase(it1);
186  }
187 
188  if(n_op2.empty())
189  return g1;
190 
191  // end of common prefix
192  exprt and_expr1 = conjunction(n_op1);
193  exprt and_expr2 = conjunction(n_op2);
194 
195  g1.expr = conjunction(op1);
196 
197  exprt tmp(boolean_negate(and_expr2));
198 
199  if(tmp != and_expr1)
200  {
201  if(and_expr1.is_true() || and_expr2.is_true())
202  {
203  }
204  else
205  // TODO: make simplify more capable and apply here
206  g1.add(or_exprt(and_expr1, and_expr2));
207  }
208 
209  return g1;
210 }
Boolean AND.
Definition: std_expr.h:2120
Base class for all expressions.
Definition: expr.h:56
std::vector< exprt > operandst
Definition: expr.h:58
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:27
bool is_boolean() const
Return whether the expression represents a Boolean.
Definition: expr.h:224
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:34
operandst & operands()
Definition: expr.h:94
void add(const exprt &expr)
Definition: guard_expr.cpp:38
bool is_true() const
Definition: guard_expr.h:60
bool disjunction_may_simplify(const guard_exprt &other_guard)
Returns true if operator|= with other_guard may result in a simpler expression.
Definition: guard_expr.cpp:123
exprt as_expr() const
Definition: guard_expr.h:46
bool is_false() const
Definition: guard_expr.h:65
exprt guard_expr(exprt expr) const
Return guard => dest or a simplified variant thereof if either guard or dest are trivial.
Definition: guard_expr.cpp:18
exprt expr
Definition: guard_expr.h:79
Boolean implication.
Definition: std_expr.h:2183
const irep_idt & id() const
Definition: irep.h:388
Boolean OR.
Definition: std_expr.h:2228
The Boolean constant true.
Definition: std_expr.h:3063
exprt boolean_negate(const exprt &src)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true
Definition: expr_util.cpp:103
Deprecated expression utility functions.
guard_exprt & operator-=(guard_exprt &g1, const guard_exprt &g2)
Definition: guard_expr.cpp:64
guard_exprt & operator|=(guard_exprt &g1, const guard_exprt &g2)
Definition: guard_expr.cpp:134
Guard Data Structure.
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
exprt conjunction(const exprt::operandst &op)
1) generates a conjunction for two or more operands 2) for one operand, returns the operand 3) return...
Definition: std_expr.cpp:83
API to expression classes.