cprover
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 <ostream>
15 
16 #include <util/invariant.h>
17 #include <util/simplify_utils.h>
18 #include <util/std_expr.h>
19 
21 {
22  if(is_true())
23  {
24  // do nothing
25  return expr;
26  }
27  else
28  {
29  if(expr.is_false())
30  {
31  return boolean_negate(as_expr());
32  }
33  else
34  {
35  return implies_exprt{as_expr(), expr};
36  }
37  }
38 }
39 
40 void guard_exprt::add(const exprt &expr)
41 {
42  PRECONDITION(expr.type().id() == ID_bool);
43 
44  if(is_false() || expr.is_true())
45  return;
46  else if(is_true() || expr.is_false())
47  {
48  this->expr = expr;
49 
50  return;
51  }
52  else if(this->expr.id() != ID_and)
53  {
54  and_exprt a({this->expr});
55  this->expr = a;
56  }
57 
58  exprt::operandst &op = this->expr.operands();
59 
60  if(expr.id() == ID_and)
61  op.insert(op.end(), expr.operands().begin(), expr.operands().end());
62  else
63  op.push_back(expr);
64 }
65 
67 {
68  if(g1.expr.id() != ID_and)
69  {
70  if(g2.expr.id() != ID_and)
71  {
72  if(g1.expr == g2.expr)
73  g1.expr = true_exprt{};
74  }
75  else
76  {
77  for(const auto &op : g2.expr.operands())
78  {
79  if(g1.expr == op)
80  {
81  g1.expr = true_exprt{};
82  break;
83  }
84  }
85  }
86 
87  return g1;
88  }
89 
90  if(g2.expr.id() != ID_and)
91  {
92  exprt::operandst &op1 = g1.expr.operands();
93  for(exprt::operandst::iterator it = op1.begin(); it != op1.end(); ++it)
94  {
95  if(g1.expr == g2.expr)
96  {
97  op1.erase(it);
98  break;
99  }
100  }
101 
102  return g1;
103  }
104 
105  sort_and_join(g1.expr);
106  exprt g2_sorted = g2.as_expr();
107  sort_and_join(g2_sorted);
108 
109  exprt::operandst &op1 = g1.expr.operands();
110  const exprt::operandst &op2 = g2_sorted.operands();
111 
112  exprt::operandst::iterator it1 = op1.begin();
113  for(exprt::operandst::const_iterator it2 = op2.begin(); it2 != op2.end();
114  ++it2)
115  {
116  while(it1 != op1.end() && *it1 < *it2)
117  ++it1;
118  if(it1 != op1.end() && *it1 == *it2)
119  it1 = op1.erase(it1);
120  }
121 
122  g1.expr = conjunction(op1);
123 
124  return g1;
125 }
126 
128 {
129  if(is_true() || is_false() || other_guard.is_true() || other_guard.is_false())
130  return true;
131  if(expr.id() == ID_and && other_guard.expr.id() == ID_and)
132  return true;
133  if(other_guard.expr == boolean_negate(expr))
134  return true;
135  return false;
136 }
137 
139 {
140  if(g2.is_false() || g1.is_true())
141  return g1;
142  if(g1.is_false() || g2.is_true())
143  {
144  g1.expr = g2.expr;
145  return g1;
146  }
147 
148  if(g1.expr.id() != ID_and || g2.expr.id() != ID_and)
149  {
150  exprt tmp(boolean_negate(g2.as_expr()));
151 
152  if(tmp == g1.as_expr())
153  g1.expr = true_exprt();
154  else
155  g1.expr = or_exprt(g1.as_expr(), g2.as_expr());
156 
157  // TODO: make simplify more capable and apply here
158 
159  return g1;
160  }
161 
162  // find common prefix
163  sort_and_join(g1.expr);
164  exprt g2_sorted = g2.as_expr();
165  sort_and_join(g2_sorted);
166 
167  exprt::operandst &op1 = g1.expr.operands();
168  const exprt::operandst &op2 = g2_sorted.operands();
169 
170  exprt::operandst n_op1, n_op2;
171  n_op1.reserve(op1.size());
172  n_op2.reserve(op2.size());
173 
174  exprt::operandst::iterator it1 = op1.begin();
175  for(exprt::operandst::const_iterator it2 = op2.begin(); it2 != op2.end();
176  ++it2)
177  {
178  while(it1 != op1.end() && *it1 < *it2)
179  {
180  n_op1.push_back(*it1);
181  it1 = op1.erase(it1);
182  }
183  if(it1 != op1.end() && *it1 == *it2)
184  ++it1;
185  else
186  n_op2.push_back(*it2);
187  }
188  while(it1 != op1.end())
189  {
190  n_op1.push_back(*it1);
191  it1 = op1.erase(it1);
192  }
193 
194  if(n_op2.empty())
195  return g1;
196 
197  // end of common prefix
198  exprt and_expr1 = conjunction(n_op1);
199  exprt and_expr2 = conjunction(n_op2);
200 
201  g1.expr = conjunction(op1);
202 
203  exprt tmp(boolean_negate(and_expr2));
204 
205  if(tmp != and_expr1)
206  {
207  if(and_expr1.is_true() || and_expr2.is_true())
208  {
209  }
210  else
211  // TODO: make simplify more capable and apply here
212  g1.add(or_exprt(and_expr1, and_expr2));
213  }
214 
215  return g1;
216 }
Boolean AND.
Definition: std_expr.h:1835
Base class for all expressions.
Definition: expr.h:54
std::vector< exprt > operandst
Definition: expr.h:56
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:47
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:56
typet & type()
Return the type of the expression.
Definition: expr.h:82
operandst & operands()
Definition: expr.h:96
void add(const exprt &expr)
Definition: guard_expr.cpp:40
bool is_true() const
Definition: guard_expr.h:63
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:127
exprt as_expr() const
Definition: guard_expr.h:49
bool is_false() const
Definition: guard_expr.h:68
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:20
exprt expr
Definition: guard_expr.h:82
Boolean implication.
Definition: std_expr.h:1898
const irep_idt & id() const
Definition: irep.h:407
Boolean OR.
Definition: std_expr.h:1943
The Boolean constant true.
Definition: std_expr.h:2717
exprt boolean_negate(const exprt &src)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true
Definition: expr_util.cpp:128
guard_exprt & operator-=(guard_exprt &g1, const guard_exprt &g2)
Definition: guard_expr.cpp:66
guard_exprt & operator|=(guard_exprt &g1, const guard_exprt &g2)
Definition: guard_expr.cpp:138
Guard Data Structure.
static bool sort_and_join(exprt &expr, bool do_sort)
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
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:41
API to expression classes.