1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
|
//-----------------------------------------------------------------------------
//
// Copyright (C) Microsoft Corporation. All Rights Reserved.
//
//-----------------------------------------------------------------------------
using System;
using System.Collections;
using System.Collections.Generic;
using System.Diagnostics;
using System.Diagnostics.Contracts;
using Microsoft.Boogie.VCExprAST;
namespace Microsoft.Boogie.Simplify
{
// Simplify does not understand the LET operator, so we have to replace
// it with implications (previously, this was done in the VCExprGenerator), or
// we have to apply the let as a substitution (in the case of terms)
// This visitor expects that let-bindings are sorted, so that bound
// variables only occur after their declaration
public class Let2ImpliesMutator : SubstitutingVCExprVisitor {
public Let2ImpliesMutator(VCExpressionGenerator gen) :base(gen) {
Contract.Requires(gen!=null);
this.keepLetFormula = this.keepLetTerm = false;
}
public Let2ImpliesMutator(VCExpressionGenerator gen, bool keepLetTerm, bool keepLetFormula):base(gen) {
Contract.Requires(gen!=null);
this.keepLetTerm = keepLetTerm;
this.keepLetFormula = keepLetFormula;
}
readonly bool keepLetTerm;
readonly bool keepLetFormula;
public VCExpr Mutate(VCExpr expr) {
Contract.Requires(expr != null);
Contract.Ensures(Contract.Result<VCExpr>() != null);
return Mutate(expr, new VCExprSubstitution ());
}
////////////////////////////////////////////////////////////////////////////
private int polarity = 1; // 1 for positive, -1 for negative, 0 for both
// we also track which variables occur in positive, negative, or
// in both positions (to decide whether implications or equations
// have to be used to define such a variable)
private enum OccurrenceTypes { None, Pos, Neg, PosNeg };
private OccurrenceTypes Union(OccurrenceTypes o1, OccurrenceTypes o2) {
switch(o1) {
case OccurrenceTypes.None: return o2;
case OccurrenceTypes.Pos:
switch(o2) {
case OccurrenceTypes.None:
case OccurrenceTypes.Pos:
return OccurrenceTypes.Pos;
default:
return OccurrenceTypes.PosNeg;
}
case OccurrenceTypes.Neg:
switch(o2) {
case OccurrenceTypes.None:
case OccurrenceTypes.Neg:
return OccurrenceTypes.Neg;
default:
return OccurrenceTypes.PosNeg;
}
default:
return OccurrenceTypes.PosNeg;
}
}
private IDictionary<VCExprVar/*!*/, OccurrenceTypes>/*!*/ VarOccurrences =
new Dictionary<VCExprVar/*!*/, OccurrenceTypes>();
[ContractInvariantMethod]
void ObjectInvariant()
{
Contract.Invariant(cce.NonNullElements(VarOccurrences));
}
////////////////////////////////////////////////////////////////////////////
public override VCExpr Visit(VCExprVar node,
VCExprSubstitution substitution) {
Contract.Requires(node!= null);
Contract.Requires(substitution != null);
Contract.Ensures(Contract.Result<VCExpr>() != null);
VCExpr res = base.Visit(node, substitution);
Contract.Assert(res!=null);
VCExprVar resAsVar = res as VCExprVar;
if (resAsVar != null) {
OccurrenceTypes occ;
if (polarity > 0)
occ = OccurrenceTypes.Pos;
else if (polarity < 0)
occ = OccurrenceTypes.Neg;
else
occ = OccurrenceTypes.PosNeg;
OccurrenceTypes oldOcc;
if (VarOccurrences.TryGetValue(resAsVar, out oldOcc))
occ = Union(occ, oldOcc);
VarOccurrences[resAsVar] = occ;
}
return res;
}
public override VCExpr Visit(VCExprNAry node,
VCExprSubstitution substitution) {
Contract.Requires(node != null);
Contract.Requires(substitution != null);
Contract.Ensures(Contract.Result<VCExpr>() != null);
// track the polarity to ensure that no implications are introduced
// in negative positions
// UGLY: the code for tracking polarities should be factored out
// (similar code is used in the TypeEraser)
VCExpr res;
if (node.Op.Equals(VCExpressionGenerator.NotOp)) {
polarity = -polarity;
res = base.Visit(node, substitution);
polarity = -polarity;
} else if (node.Op.Equals(VCExpressionGenerator.ImpliesOp)) {
polarity = -polarity;
VCExpr newArg0 = Mutate(node[0], substitution);
Contract.Assert(newArg0 != null);
polarity = -polarity;
VCExpr newArg1 = Mutate(node[1], substitution);
Contract.Assert(newArg1 != null);
res = Gen.Implies(newArg0, newArg1);
} else if (!node.Op.Equals(VCExpressionGenerator.AndOp) &&
!node.Op.Equals(VCExpressionGenerator.OrOp) &&
!(node.Op is VCExprLabelOp)) {
// standard is to set the polarity to 0 (fits most operators)
int oldPolarity = polarity;
polarity = 0;
res = base.Visit(node, substitution);
polarity = oldPolarity;
} else {
res = base.Visit(node, substitution);
}
return res;
}
public override VCExpr Visit(VCExprLet originalNode,
VCExprSubstitution substitution) {
Contract.Requires(originalNode != null);
Contract.Requires(substitution != null);
Contract.Ensures(Contract.Result<VCExpr>() != null);
// first sort the bindings to be able to apply substitutions
LetBindingSorter letSorter = new LetBindingSorter (Gen);
Contract.Assert(letSorter != null);
VCExpr newNode = letSorter.Mutate(originalNode, true);
Contract.Assert(newNode != null);
VCExprLet node = newNode as VCExprLet;
if (node == null)
// it can happen that the complete let-expressions gets eliminated by the
// sorter, which also checks whether let-bindings are actually used
return newNode;
substitution.PushScope(); try {
// the bindings that remain and that are later handled using an implication
List<VCExprLetBinding> bindings = new List<VCExprLetBinding> ();
List<VCExprLetBinding> keepBindings = new List<VCExprLetBinding> ();
foreach (VCExprLetBinding binding in node) {
Contract.Assert(binding != null);
// in all cases we apply the substitution up to this point
// to the bound formula
VCExpr newE = Mutate(binding.E, substitution);
Contract.Assert(newE != null);
if (binding.V.Type.IsBool) {
// a bound formula is handled using an implication; we introduce
// a fresh variable to avoid clashes
Contract.Assert( polarity > 0);
if (keepLetFormula) {
keepBindings.Add(Gen.LetBinding(binding.V, newE));
} else {
VCExprVar newVar = Gen.Variable(binding.V.Name, Type.Bool);
Contract.Assert(newVar != null);
substitution[binding.V] = newVar;
bindings.Add(Gen.LetBinding(newVar, newE));
}
} else {
if (keepLetTerm) {
keepBindings.Add(Gen.LetBinding(binding.V, newE));
} else {
// a bound term is substituted
substitution[binding.V] = newE;
}
}
}
VCExpr newBody = Mutate(node.Body, substitution);
Contract.Assert(newBody != null);
if (keepBindings.Count > 0) {
newBody = Gen.Let(keepBindings, newBody);
}
// Depending on the places where the variable occurs, we would
// have to introduce implications or equations to define the
// bound variables. For the time being, we just assert that all
// occurrences are positive
foreach (VCExprLetBinding b in bindings) {
Contract.Assert(b != null);
OccurrenceTypes occ;
if (VarOccurrences.TryGetValue(b.V, out occ))
Contract.Assert( occ == OccurrenceTypes.None || occ == OccurrenceTypes.Pos);
}
return Gen.ImpliesSimp(Gen.AsImplications(bindings), newBody);
} finally {
substitution.PopScope();
}
}
}
}
|
