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 || g2.expr.id() != ID_and)
69  return g1;
70 
71  sort_and_join(g1.expr);
72  exprt g2_sorted = g2.as_expr();
73  sort_and_join(g2_sorted);
74 
75  exprt::operandst &op1 = g1.expr.operands();
76  const exprt::operandst &op2 = g2_sorted.operands();
77 
78  exprt::operandst::iterator it1 = op1.begin();
79  for(exprt::operandst::const_iterator it2 = op2.begin(); it2 != op2.end();
80  ++it2)
81  {
82  while(it1 != op1.end() && *it1 < *it2)
83  ++it1;
84  if(it1 != op1.end() && *it1 == *it2)
85  it1 = op1.erase(it1);
86  }
87 
88  g1.expr = conjunction(op1);
89 
90  return g1;
91 }
92 
94 {
95  if(is_true() || is_false() || other_guard.is_true() || other_guard.is_false())
96  return true;
97  if(expr.id() == ID_and && other_guard.expr.id() == ID_and)
98  return true;
99  if(other_guard.expr == boolean_negate(expr))
100  return true;
101  return false;
102 }
103 
105 {
106  if(g2.is_false() || g1.is_true())
107  return g1;
108  if(g1.is_false() || g2.is_true())
109  {
110  g1.expr = g2.expr;
111  return g1;
112  }
113 
114  if(g1.expr.id() != ID_and || g2.expr.id() != ID_and)
115  {
116  exprt tmp(boolean_negate(g2.as_expr()));
117 
118  if(tmp == g1.as_expr())
119  g1.expr = true_exprt();
120  else
121  g1.expr = or_exprt(g1.as_expr(), g2.as_expr());
122 
123  // TODO: make simplify more capable and apply here
124 
125  return g1;
126  }
127 
128  // find common prefix
129  sort_and_join(g1.expr);
130  exprt g2_sorted = g2.as_expr();
131  sort_and_join(g2_sorted);
132 
133  exprt::operandst &op1 = g1.expr.operands();
134  const exprt::operandst &op2 = g2_sorted.operands();
135 
136  exprt::operandst n_op1, n_op2;
137  n_op1.reserve(op1.size());
138  n_op2.reserve(op2.size());
139 
140  exprt::operandst::iterator it1 = op1.begin();
141  for(exprt::operandst::const_iterator it2 = op2.begin(); it2 != op2.end();
142  ++it2)
143  {
144  while(it1 != op1.end() && *it1 < *it2)
145  {
146  n_op1.push_back(*it1);
147  it1 = op1.erase(it1);
148  }
149  if(it1 != op1.end() && *it1 == *it2)
150  ++it1;
151  else
152  n_op2.push_back(*it2);
153  }
154  while(it1 != op1.end())
155  {
156  n_op1.push_back(*it1);
157  it1 = op1.erase(it1);
158  }
159 
160  if(n_op2.empty())
161  return g1;
162 
163  // end of common prefix
164  exprt and_expr1 = conjunction(n_op1);
165  exprt and_expr2 = conjunction(n_op2);
166 
167  g1.expr = conjunction(op1);
168 
169  exprt tmp(boolean_negate(and_expr2));
170 
171  if(tmp != and_expr1)
172  {
173  if(and_expr1.is_true() || and_expr2.is_true())
174  {
175  }
176  else
177  // TODO: make simplify more capable and apply here
178  g1.add(or_exprt(and_expr1, and_expr2));
179  }
180 
181  return g1;
182 }
guard_exprt
Definition: guard_expr.h:27
operator|=
guard_exprt & operator|=(guard_exprt &g1, const guard_exprt &g2)
Definition: guard_expr.cpp:104
conjunction
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:51
guard_exprt::guard_expr
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
invariant.h
and_exprt
Boolean AND.
Definition: std_expr.h:2137
exprt
Base class for all expressions.
Definition: expr.h:53
guard_exprt::is_true
bool is_true() const
Definition: guard_expr.h:63
exprt::is_true
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:92
guard_exprt::expr
exprt expr
Definition: guard_expr.h:82
exprt::is_false
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:101
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
or_exprt
Boolean OR.
Definition: std_expr.h:2245
guard_exprt::as_expr
exprt as_expr() const
Definition: guard_expr.h:49
guard_exprt::add
void add(const exprt &expr)
Definition: guard_expr.cpp:40
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
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
operator-=
guard_exprt & operator-=(guard_exprt &g1, const guard_exprt &g2)
Definition: guard_expr.cpp:66
guard_exprt::disjunction_may_simplify
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:93
irept::id
const irep_idt & id() const
Definition: irep.h:418
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:55
guard_exprt::is_false
bool is_false() const
Definition: guard_expr.h:68
sort_and_join
static bool sort_and_join(const struct saj_tablet &saj_entry, const irep_idt &type_id)
Definition: simplify_utils.cpp:98
implies_exprt
Boolean implication.
Definition: std_expr.h:2200
exprt::operands
operandst & operands()
Definition: expr.h:95
true_exprt
The Boolean constant true.
Definition: std_expr.h:3955
simplify_utils.h
std_expr.h
API to expression classes.
guard_expr.h
Guard Data Structure.