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
237
238
239
240
241
242
243
244
245
246
247
248
|
//-----------------------------------------------------------------------------
//
// Copyright (C) Microsoft Corporation. All Rights Reserved.
//
//-----------------------------------------------------------------------------
using System;
using System.Text;
using System.IO;
using System.Linq;
using System.Collections;
using System.Collections.Generic;
using System.Diagnostics.Contracts;
using Microsoft.Basetypes;
using Microsoft.Boogie.VCExprAST;
// Ensure that no formulas (expressions of type boolean that are not
// just a variable) occur with terms (expressions of some other
// type). This is done by introducing let-binders for boolean
// variables.
namespace Microsoft.Boogie.VCExprAST
{
public struct FlattenerState {
public readonly int Polarity;
public readonly bool InTerm;
public static FlattenerState INITIAL = new FlattenerState(1, false);
public FlattenerState(int polarity, bool inTerm) {
Polarity = polarity;
InTerm = inTerm;
}
public FlattenerState TogglePolarity { get {
return new FlattenerState(-Polarity, InTerm);
} }
public FlattenerState ZeroPolarity { get {
return new FlattenerState(0, InTerm);
} }
public FlattenerState EnterTerm { get {
return new FlattenerState(Polarity, true);
} }
}
//////////////////////////////////////////////////////////////////////////////
public class TermFormulaFlattener : MutatingVCExprVisitor<FlattenerState> {
public TermFormulaFlattener(VCExpressionGenerator gen):base(gen){
Contract.Requires(gen != null);
}
private readonly IDictionary<VCExpr/*!*/, VCExprVar/*!*/>/*!*/ Bindings =
new Dictionary<VCExpr/*!*/, VCExprVar/*!*/> ();
private int varNameCounter = 0;
public VCExpr Flatten(VCExpr expr){
Contract.Requires(expr != null);
Contract.Ensures(Contract.Result<VCExpr>() != null);
VCExpr/*!*/ res = Mutate(expr, FlattenerState.INITIAL);
Contract.Assert(res != null);
while (Bindings.Count > 0) {
List<VCExprLetBinding/*!*/>/*!*/ letBindings = new List<VCExprLetBinding/*!*/> ();
foreach (KeyValuePair<VCExpr/*!*/, VCExprVar/*!*/> pair in Bindings){Contract.Assert(cce.NonNullElements(pair));
letBindings.Add(Gen.LetBinding(pair.Value, pair.Key));}
Bindings.Clear();
res = AddBindings(letBindings, res, FlattenerState.INITIAL);
}
return res;
}
private VCExprVar GetVarFor(VCExpr expr){
Contract.Requires(expr != null);
Contract.Requires((expr.Type.IsBool));
Contract.Ensures(Contract.Result<VCExprVar>() != null);
VCExprVar res;
if (!Bindings.TryGetValue(expr, out res)) {
string name = "flt" + varNameCounter;
varNameCounter = varNameCounter + 1;
res = Gen.Variable(name, Type.Bool);
Bindings.Add(expr, res);
}
return cce.NonNull(res);
}
// Remove all let-bindings from the field bindings whose rhs
// contains any of the specified variables
private List<VCExprLetBinding/*!*/>/*!*/ RemoveBindingsWithVars(List<VCExprVar/*!*/>/*!*/ boundVars, List<TypeVariable/*!*/>/*!*/ boundTypeVars){
Contract.Requires(cce.NonNullElements(boundTypeVars));
Contract.Requires(cce.NonNullElements(boundVars));
Contract.Ensures(cce.NonNullElements(Contract.Result<List<VCExprLetBinding>>()));
List<VCExprLetBinding/*!*/>/*!*/ res = new List<VCExprLetBinding/*!*/> ();
FreeVariableCollector/*!*/ coll = new FreeVariableCollector ();
foreach (KeyValuePair<VCExpr, VCExprVar> pair in Bindings) {
Contract.Assert(cce.NonNullElements(pair));
coll.Collect(pair.Key);
if (boundVars.Any(var => coll.FreeTermVars.ContainsKey(var)) ||
boundTypeVars.Any(var => coll.FreeTypeVars.Contains(var)))
res.Add(Gen.LetBinding(pair.Value, pair.Key));
coll.Reset();
}
foreach (VCExprLetBinding b in res){Contract.Assert(b != null);
Bindings.Remove(b.E);}
return res;
}
// Add bindings to a formula using an implication or
// conjunction. The bindings themselves will be flattened as well,
// which might introduce further bindings
private VCExpr AddBindings(List<VCExprLetBinding/*!*/>/*!*/ bindings, VCExpr body, FlattenerState state){
Contract.Requires(body != null);
Contract.Requires(cce.NonNullElements(bindings));
Contract.Requires((body.Type.IsBool));
Contract.Ensures(Contract.Result<VCExpr>() != null);
List<VCExprLetBinding/*!*/>/*!*/ mutatedBindings = FlattenBindings(bindings, state);
Contract.Assert(mutatedBindings != null);
VCExpr/*!*/ bindingEquations = Gen.AsEquations(mutatedBindings);
Contract.Assert(bindingEquations != null);
switch(state.Polarity) {
case 1:
return Gen.Implies(bindingEquations, body);
case -1:
return Gen.And(bindingEquations, body);
case 0:
// also add explicit quantifiers for the bound variables
List<VCExprVar/*!*/>/*!*/ vars = new List<VCExprVar/*!*/> ();
foreach (VCExprLetBinding/*!*/ binding in mutatedBindings){Contract.Assert(binding != null);
vars.Add(binding.V);}
return Gen.Forall(vars, new List<VCTrigger/*!*/>(),
Gen.Implies(bindingEquations, body));
}
Contract.Assert(false); throw new cce.UnreachableException();
}
private List<VCExprLetBinding/*!*/>/*!*/ FlattenBindings(List<VCExprLetBinding/*!*/>/*!*/ bindings, FlattenerState state){
Contract.Requires(cce.NonNullElements(bindings));
Contract.Ensures(cce.NonNullElements(Contract.Result<List<VCExprLetBinding>>()));
FlattenerState stateInBindings = state.ZeroPolarity;
List<VCExprLetBinding/*!*/>/*!*/ mutatedBindings = new List<VCExprLetBinding/*!*/> ();
foreach (VCExprLetBinding/*!*/ b in bindings) {
Contract.Assert(b != null);
mutatedBindings.Add(Gen.LetBinding(b.V, Mutate(b.E, stateInBindings)));
}
return mutatedBindings;
}
////////////////////////////////////////////////////////////////////////////
public override bool AvoidVisit(VCExprNAry node, FlattenerState arg)
{
return node.Op.Equals(VCExpressionGenerator.AndOp) ||
node.Op.Equals(VCExpressionGenerator.OrOp);
}
public override VCExpr Visit(VCExprNAry node, FlattenerState state){
Contract.Requires(node != null);
Contract.Ensures(Contract.Result<VCExpr>() != null);
// track the polarity to know whether implications or conjunctions
// are to be introduced
if (node.Op.Equals(VCExpressionGenerator.NotOp))
return Gen.Not(Mutate(node[0], state.TogglePolarity));
if (node.Op.Equals(VCExpressionGenerator.ImpliesOp)) {
VCExpr newArg0 = Mutate(node[0], state.TogglePolarity);
VCExpr newArg1 = Mutate(node[1], state);
return Gen.Implies(newArg0, newArg1);
}
if (!node.Type.IsBool)
state = state.EnterTerm;
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)
return base.Visit(node, state.ZeroPolarity);
return base.Visit(node, state);
}
public override VCExpr Visit(VCExprQuantifier node, FlattenerState state){
Contract.Requires(node != null);
Contract.Ensures(Contract.Result<VCExpr>() != null);
if (state.InTerm)
return GetVarFor(node);
// we only flatten within the matrix of the quantified formula,
// not within the triggers (since SMT-solvers do not seem to
// appreciate triggers with let-binders)
VCExpr newBody = Mutate(node.Body, state);
// Check whether any of the extracted terms contain variables
// bound by this quantifier. In this case, we have to add
// let-binders and remove the extracted terms
bool cont = true;
while (cont) {
List<VCExprLetBinding/*!*/>/*!*/ localBindings =
RemoveBindingsWithVars(node.BoundVars, node.TypeParameters);
Contract.Assert(cce.NonNullElements(localBindings));
if (localBindings.Count > 0)
newBody = AddBindings(localBindings, newBody, state);
else
cont = false;
}
return Gen.Quantify(node.Quan, node.TypeParameters, node.BoundVars, node.Triggers, node.Infos, newBody);
}
public override VCExpr Visit(VCExprLet node, FlattenerState state){
Contract.Requires(node != null);
Contract.Ensures(Contract.Result<VCExpr>() != null);
if (state.InTerm)
return GetVarFor(node);
VCExprLet prelimRes = (VCExprLet)cce.NonNull(base.Visit(node, state));
List<VCExprLetBinding/*!*/>/*!*/ allBindings = new List<VCExprLetBinding/*!*/> ();
allBindings.AddRange(prelimRes);
// Check whether any of the extracted terms contain variables
// bound by this binder. In this case, we have to add
// let-binders and remove the extracted terms
bool cont = true;
while (cont) {
List<VCExprLetBinding/*!*/>/*!*/ localBindings =
RemoveBindingsWithVars(prelimRes.BoundVars, new List<TypeVariable/*!*/>());
if (localBindings.Count > 0)
allBindings.AddRange(FlattenBindings(localBindings, state));
else
cont = false;
}
return Gen.Let(allBindings, prelimRes.Body);
}
}
}
|
