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
|
//-----------------------------------------------------------------------------
//
// Copyright (C) Microsoft Corporation. All Rights Reserved.
//
//-----------------------------------------------------------------------------
using System;
using System.Collections;
using System.Collections.Generic;
using System.Diagnostics;
using Microsoft.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) {
this(gen, false, false);
}
public Let2ImpliesMutator(VCExpressionGenerator! gen, bool keepLetTerm, bool keepLetFormula) {
base(gen);
this.keepLetTerm = keepLetTerm;
this.keepLetFormula = keepLetFormula;
}
readonly bool keepLetTerm;
readonly bool keepLetFormula;
public VCExpr! Mutate(VCExpr! expr) {
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>();
////////////////////////////////////////////////////////////////////////////
public override VCExpr! Visit(VCExprVar! node,
VCExprSubstitution! substitution) {
VCExpr! res = base.Visit(node, substitution);
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) {
// 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);
polarity = -polarity;
VCExpr! newArg1 = Mutate(node[1], substitution);
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) {
// first sort the bindings to be able to apply substitutions
LetBindingSorter! letSorter = new LetBindingSorter (Gen);
VCExpr! newNode = letSorter.Mutate(originalNode, true);
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) {
// in all cases we apply the substitution up to this point
// to the bound formula
VCExpr! newE = Mutate(binding.E, substitution);
if (binding.V.Type.IsBool) {
// a bound formula is handled using an implication; we introduce
// a fresh variable to avoid clashes
assert polarity > 0;
if (keepLetFormula) {
keepBindings.Add(Gen.LetBinding(binding.V, newE));
} else {
VCExprVar! newVar = Gen.Variable(binding.V.Name, Type.Bool);
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);
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) {
OccurrenceTypes occ;
if (VarOccurrences.TryGetValue(b.V, out occ))
assert occ == OccurrenceTypes.None || occ == OccurrenceTypes.Pos;
}
return Gen.ImpliesSimp(Gen.AsImplications(bindings), newBody);
} finally {
substitution.PopScope();
}
}
}
}
|
