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