summaryrefslogtreecommitdiff
path: root/Source
diff options
context:
space:
mode:
authorGravatar leino <unknown>2015-11-27 18:03:34 -0800
committerGravatar leino <unknown>2015-11-27 18:03:34 -0800
commit33ae6b4bf0dc3f2c80abbd3c26356f16ded3aaee (patch)
tree5754d8d56d31a14b20736a09227c4b253e9e2c4f /Source
parent66d8663d16def735d8983f67aaffbf342e88a5f5 (diff)
parentb8fad094ad74180ca16670bebe602737d856b5da (diff)
Merge
Diffstat (limited to 'Source')
-rw-r--r--Source/Dafny/Cloner.cs4
-rw-r--r--Source/Dafny/DafnyAst.cs1
-rw-r--r--Source/Dafny/Printer.cs15
-rw-r--r--Source/Dafny/Resolver.cs1
-rw-r--r--Source/Dafny/Rewriter.cs273
-rw-r--r--Source/Dafny/Translator.cs340
-rw-r--r--Source/Dafny/Triggers/QuantifierSplitter.cs12
-rw-r--r--Source/Dafny/Triggers/QuantifiersCollector.cs13
8 files changed, 401 insertions, 258 deletions
diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs
index 1a6dfecb..6b3b0caa 100644
--- a/Source/Dafny/Cloner.cs
+++ b/Source/Dafny/Cloner.cs
@@ -552,7 +552,9 @@ namespace Microsoft.Dafny
} else if (stmt is ForallStmt) {
var s = (ForallStmt)stmt;
r = new ForallStmt(Tok(s.Tok), Tok(s.EndTok), s.BoundVars.ConvertAll(CloneBoundVar), null, CloneExpr(s.Range), s.Ens.ConvertAll(CloneMayBeFreeExpr), CloneStmt(s.Body));
-
+ if (s.ForallExpressions != null) {
+ ((ForallStmt)r).ForallExpressions = s.ForallExpressions.ConvertAll(CloneExpr);
+ }
} else if (stmt is CalcStmt) {
var s = (CalcStmt)stmt;
// calc statements have the unusual property that the last line is duplicated. If that is the case (which
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index 847617aa..4c1e2bd7 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -4693,6 +4693,7 @@ namespace Microsoft.Dafny {
public readonly Expression Range;
public readonly List<MaybeFreeExpression> Ens;
public readonly Statement Body;
+ public List<Expression> ForallExpressions; // fill in by rewriter.
public List<ComprehensionExpr.BoundedPool> Bounds; // initialized and filled in by resolver
// invariant: if successfully resolved, Bounds.Count == BoundVars.Count;
diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs
index 145e82e7..0a25b941 100644
--- a/Source/Dafny/Printer.cs
+++ b/Source/Dafny/Printer.cs
@@ -841,11 +841,22 @@ namespace Microsoft.Dafny {
wr.Write("}");
} else if (stmt is ForallStmt) {
- var s = (ForallStmt)stmt;
+ var s = (ForallStmt)stmt;
+ Attributes attributes = s.Attributes;
+ if (attributes == null && s.ForallExpressions != null) {
+ foreach (Expression expr in s.ForallExpressions) {
+ ForallExpr e = (ForallExpr)expr;
+ while (e != null && attributes == null) {
+ attributes = e.Attributes;
+ e = (ForallExpr)e.SplitQuantifierExpression;
+ }
+ if (attributes != null) { break; }
+ }
+ }
wr.Write("forall");
if (s.BoundVars.Count != 0) {
wr.Write(" ");
- PrintQuantifierDomain(s.BoundVars, s.Attributes, s.Range);
+ PrintQuantifierDomain(s.BoundVars, attributes, s.Range);
}
if (s.Ens.Count == 0) {
wr.Write(" ");
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 315b823a..eff7d97d 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -235,6 +235,7 @@ namespace Microsoft.Dafny
rewriters.Add(new AutoReqFunctionRewriter(this.reporter, opaqueRewriter));
rewriters.Add(opaqueRewriter);
rewriters.Add(new TimeLimitRewriter(reporter));
+ rewriters.Add(new ForallStmtRewriter(reporter));
if (DafnyOptions.O.AutoTriggers) {
rewriters.Add(new QuantifierSplittingRewriter(reporter));
diff --git a/Source/Dafny/Rewriter.cs b/Source/Dafny/Rewriter.cs
index d9db03c7..9a898cbe 100644
--- a/Source/Dafny/Rewriter.cs
+++ b/Source/Dafny/Rewriter.cs
@@ -72,6 +72,279 @@ namespace Microsoft.Dafny
}
}
+ // write out the quantifier for ForallStmt
+ public class ForallStmtRewriter : IRewriter
+ {
+ public ForallStmtRewriter(ErrorReporter reporter) : base(reporter) {
+ Contract.Requires(reporter != null);
+ }
+
+ internal override void PostResolve(ModuleDefinition m) {
+ var forallvisiter = new ForAllStmtVisitor();
+ foreach (var decl in ModuleDefinition.AllCallables(m.TopLevelDecls)) {
+ forallvisiter.Visit(decl, true);
+ }
+ }
+
+ internal class ForAllStmtVisitor : TopDownVisitor<bool>
+ {
+ protected override bool VisitOneStmt(Statement stmt, ref bool st) {
+ Contract.Requires(stmt != null);
+ if (stmt is ForallStmt) {
+ ForallStmt s = (ForallStmt)stmt;
+ if (s.Kind == ForallStmt.ParBodyKind.Proof) {
+ Expression term = s.Ens.Count != 0 ? s.Ens[0].E : new LiteralExpr(s.Tok, true);
+ for (int i = 1; i < s.Ens.Count; i++) {
+ term = new BinaryExpr(s.Tok, BinaryExpr.ResolvedOpcode.And, term, s.Ens[i].E);
+ }
+ List<Expression> exprList = new List<Expression>();
+ ForallExpr expr = new ForallExpr(s.Tok, s.BoundVars, s.Range, term, s.Attributes);
+ expr.Type = Type.Bool; // resolve here
+ exprList.Add(expr);
+ s.ForallExpressions = exprList;
+ } else if (s.Kind == ForallStmt.ParBodyKind.Assign) {
+ if (s.BoundVars.Count != 0) {
+ var s0 = (AssignStmt)s.S0;
+ if (s0.Rhs is ExprRhs) {
+ List<Expression> exprList = new List<Expression>();
+ Expression Fi = null;
+ Func<Expression, Expression> lhsBuilder = null;
+ var lhs = s0.Lhs.Resolved;
+ var i = s.BoundVars[0];
+ if (s.BoundVars.Count == 1) {
+ //var lhsContext = null;
+ // Detect the following cases:
+ // 0: forall i | R(i) { F(i).f := E(i); }
+ // 1: forall i | R(i) { A[F(i)] := E(i); }
+ // 2: forall i | R(i) { F(i)[N] := E(i); }
+ if (lhs is MemberSelectExpr) {
+ var ll = (MemberSelectExpr)lhs;
+ Fi = ll.Obj;
+ lhsBuilder = e => { var l = new MemberSelectExpr(ll.tok, e, ll.MemberName); l.Member = ll.Member; l.Type = ll.Type; return l; };
+ } else if (lhs is SeqSelectExpr) {
+ var ll = (SeqSelectExpr)lhs;
+ Contract.Assert(ll.SelectOne);
+ if (!Translator.ContainsFreeVariable(ll.Seq, false, i)) {
+ Fi = ll.E0;
+ lhsBuilder = e => { var l = new SeqSelectExpr(ll.tok, true, ll.Seq, e, null); l.Type = ll.Type; return l; };
+ } else if (!Translator.ContainsFreeVariable(ll.E0, false, i)) {
+ Fi = ll.Seq;
+ lhsBuilder = e => { var l = new SeqSelectExpr(ll.tok, true, e, ll.E0, null); l.Type = ll.Type; return l; };
+ }
+ }
+ }
+ var rhs = ((ExprRhs)s0.Rhs).Expr;
+ bool usedInversion = false;
+ if (Fi != null) {
+ var j = new BoundVar(i.tok, i.Name + "#inv", Fi.Type);
+ var jj = Expression.CreateIdentExpr(j);
+ var jList = new List<BoundVar>() { j };
+ var vals = InvertExpression(i, j, s.Range, Fi);
+#if DEBUG_PRINT
+ Console.WriteLine("DEBUG: Trying to invert:");
+ Console.WriteLine("DEBUG: " + Printer.ExprToString(s.Range) + " && " + j.Name + " == " + Printer.ExprToString(Fi));
+ if (vals == null) {
+ Console.WriteLine("DEBUG: Can't");
+ } else {
+ Console.WriteLine("DEBUG: The inverse is the disjunction of the following:");
+ foreach (var val in vals) {
+ Console.WriteLine("DEBUG: " + Printer.ExprToString(val.Range) + " && " + Printer.ExprToString(val.FInverse) + " == " + i.Name);
+ }
+ }
+#endif
+ if (vals != null) {
+ foreach (var val in vals) {
+ lhs = lhsBuilder(jj);
+ Attributes attributes = new Attributes("trigger", new List<Expression>() { lhs }, s.Attributes);
+ var expr = new ForallExpr(s.Tok, jList, val.Range, new BinaryExpr(s.Tok, BinaryExpr.ResolvedOpcode.EqCommon, lhs, Substitute(rhs, i, val.FInverse)), attributes);
+ expr.Type = Type.Bool; //resolve here
+ exprList.Add(expr);
+ }
+ usedInversion = true;
+ }
+ }
+ if (!usedInversion) {
+ var expr = new ForallExpr(s.Tok, s.BoundVars, s.Range, new BinaryExpr(s.Tok, BinaryExpr.ResolvedOpcode.EqCommon, lhs, rhs), s.Attributes);
+ expr.Type = Type.Bool; // resolve here
+ exprList.Add(expr);
+ }
+ s.ForallExpressions = exprList;
+ }
+ }
+ } else if (s.Kind == ForallStmt.ParBodyKind.Call) {
+ var s0 = (CallStmt)s.S0;
+ Expression term = s0.Method.Ens.Count != 0 ? s0.Method.Ens[0].E : new LiteralExpr(s.Tok, true);
+ for (int i = 1; i < s0.Method.Ens.Count; i++) {
+ term = new BinaryExpr(s.Tok, BinaryExpr.ResolvedOpcode.And, term, s0.Method.Ens[i].E);
+ }
+ List<Expression> exprList = new List<Expression>();
+ ForallExpr expr = new ForallExpr(s.Tok, s.BoundVars, s.Range, term, s.Attributes);
+ expr.Type = Type.Bool; // resolve here
+ exprList.Add(expr);
+ } else {
+ Contract.Assert(false); // unexpected kind
+ }
+ }
+ return true; //visit the sub-parts with the same "st"
+ }
+
+ internal class ForallStmtTranslationValues
+ {
+ public readonly Expression Range;
+ public readonly Expression FInverse;
+ public ForallStmtTranslationValues(Expression range, Expression fInverse) {
+ Contract.Requires(range != null);
+ Contract.Requires(fInverse != null);
+ Range = range;
+ FInverse = fInverse;
+ }
+ public ForallStmtTranslationValues Subst(IVariable j, Expression e) {
+ Contract.Requires(j != null);
+ Contract.Requires(e != null);
+ Dictionary<TypeParameter, Type> typeMap = new Dictionary<TypeParameter, Type>();
+ var substMap = new Dictionary<IVariable, Expression>();
+ substMap.Add(j, e);
+ Translator.Substituter sub = new Translator.Substituter(null, substMap, typeMap, null);
+ var v = new ForallStmtTranslationValues(sub.Substitute(Range), sub.Substitute(FInverse));
+ return v;
+ }
+ }
+
+ /// <summary>
+ /// Find piecewise inverse of F under R. More precisely, find lists of expressions P and F-1
+ /// such that
+ /// R(i) && j == F(i)
+ /// holds iff the disjunction of the following predicates holds:
+ /// P_0(j) && F-1_0(j) == i
+ /// ...
+ /// P_{n-1}(j) && F-1_{n-1}(j) == i
+ /// If no such disjunction is found, return null.
+ /// If such a disjunction is found, return for each disjunct:
+ /// * The predicate P_k(j), which is an expression that may have free occurrences of j (but no free occurrences of i)
+ /// * The expression F-1_k(j), which also may have free occurrences of j but not of i
+ /// </summary>
+ private List<ForallStmtTranslationValues> InvertExpression(BoundVar i, BoundVar j, Expression R, Expression F) {
+ Contract.Requires(i != null);
+ Contract.Requires(j != null);
+ Contract.Requires(R != null);
+ Contract.Requires(F != null);
+ var vals = new List<ForallStmtTranslationValues>(InvertExpressionIter(i, j, R, F));
+ if (vals.Count == 0) {
+ return null;
+ } else {
+ return vals;
+ }
+ }
+ /// <summary>
+ /// See InvertExpression.
+ /// </summary>
+ private IEnumerable<ForallStmtTranslationValues> InvertExpressionIter(BoundVar i, BoundVar j, Expression R, Expression F) {
+ Contract.Requires(i != null);
+ Contract.Requires(j != null);
+ Contract.Requires(R != null);
+ Contract.Requires(F != null);
+ F = F.Resolved;
+ if (!Translator.ContainsFreeVariable(F, false, i)) {
+ // We're looking at R(i) && j == K.
+ // We cannot invert j == K, but if we're lucky, R(i) contains a conjunct i==G.
+ Expression r = Expression.CreateBoolLiteral(R.tok, true);
+ Expression G = null;
+ foreach (var c in Expression.Conjuncts(R)) {
+ if (G == null && c is BinaryExpr) {
+ var bin = (BinaryExpr)c;
+ if (BinaryExpr.IsEqualityOp(bin.ResolvedOp)) {
+ var id = bin.E0.Resolved as IdentifierExpr;
+ if (id != null && id.Var == i) {
+ G = bin.E1;
+ continue;
+ }
+ id = bin.E1.Resolved as IdentifierExpr;
+ if (id != null && id.Var == i) {
+ G = bin.E0;
+ continue;
+ }
+ }
+ }
+ r = Expression.CreateAnd(r, c);
+ }
+ if (G != null) {
+ var jIsK = Expression.CreateEq(Expression.CreateIdentExpr(j), F, j.Type);
+ var rr = Substitute(r, i, G);
+ yield return new ForallStmtTranslationValues(Expression.CreateAnd(rr, jIsK), G);
+ }
+ } else if (F is IdentifierExpr) {
+ var e = (IdentifierExpr)F;
+ if (e.Var == i) {
+ // We're looking at R(i) && j == i, which is particularly easy to invert: R(j) && j == i
+ var jj = Expression.CreateIdentExpr(j);
+ yield return new ForallStmtTranslationValues(Substitute(R, i, jj), jj);
+ }
+ } else if (F is BinaryExpr) {
+ var bin = (BinaryExpr)F;
+ if (bin.ResolvedOp == BinaryExpr.ResolvedOpcode.Add && (bin.E0.Type.IsIntegerType || bin.E0.Type.IsRealType)) {
+ if (!Translator.ContainsFreeVariable(bin.E1, false, i)) {
+ // We're looking at: R(i) && j == f(i) + K.
+ // By a recursive call, we'll ask to invert: R(i) && j' == f(i).
+ // For each P_0(j') && f-1_0(j') == i we get back, we yield:
+ // P_0(j - K) && f-1_0(j - K) == i
+ var jMinusK = Expression.CreateSubtract(Expression.CreateIdentExpr(j), bin.E1);
+ foreach (var val in InvertExpression(i, j, R, bin.E0)) {
+ yield return val.Subst(j, jMinusK);
+ }
+ } else if (!Translator.ContainsFreeVariable(bin.E0, false, i)) {
+ // We're looking at: R(i) && j == K + f(i)
+ // Do as in previous case, but with operands reversed.
+ var jMinusK = Expression.CreateSubtract(Expression.CreateIdentExpr(j), bin.E0);
+ foreach (var val in InvertExpression(i, j, R, bin.E1)) {
+ yield return val.Subst(j, jMinusK);
+ }
+ }
+ } else if (bin.ResolvedOp == BinaryExpr.ResolvedOpcode.Sub && (bin.E0.Type.IsIntegerType || bin.E0.Type.IsRealType)) {
+ if (!Translator.ContainsFreeVariable(bin.E1, false, i)) {
+ // We're looking at: R(i) && j == f(i) - K
+ // Recurse on f(i) and then replace j := j + K
+ var jPlusK = Expression.CreateAdd(Expression.CreateIdentExpr(j), bin.E1);
+ foreach (var val in InvertExpression(i, j, R, bin.E0)) {
+ yield return val.Subst(j, jPlusK);
+ }
+ } else if (!Translator.ContainsFreeVariable(bin.E0, false, i)) {
+ // We're looking at: R(i) && j == K - f(i)
+ // Recurse on f(i) and then replace j := K - j
+ var kMinusJ = Expression.CreateAdd(Expression.CreateIdentExpr(j), bin.E0);
+ foreach (var val in InvertExpression(i, j, R, bin.E1)) {
+ yield return val.Subst(j, kMinusJ);
+ }
+ }
+ }
+ } else if (F is ITEExpr) {
+ var ife = (ITEExpr)F;
+ // We're looking at R(i) && j == if A(i) then B(i) else C(i), which is equivalent to the disjunction of:
+ // R(i) && A(i) && j == B(i)
+ // R(i) && !A(i) && j == C(i)
+ // We recurse on each one, yielding the results
+ var r = Expression.CreateAnd(R, ife.Test);
+ var valsThen = InvertExpression(i, j, r, ife.Thn);
+ if (valsThen != null) {
+ r = Expression.CreateAnd(R, Expression.CreateNot(ife.tok, ife.Test));
+ var valsElse = InvertExpression(i, j, r, ife.Els);
+ if (valsElse != null) {
+ foreach (var val in valsThen) { yield return val; }
+ foreach (var val in valsElse) { yield return val; }
+ }
+ }
+ }
+ }
+
+ Expression Substitute(Expression expr, IVariable v, Expression e) {
+ Dictionary<IVariable, Expression/*!*/> substMap = new Dictionary<IVariable, Expression>();
+ Dictionary<TypeParameter, Type> typeMap = new Dictionary<TypeParameter, Type>();
+ substMap.Add(v, e);
+ Translator.Substituter sub = new Translator.Substituter(null, substMap, typeMap, null);
+ return sub.Substitute(expr);
+ }
+ }
+ }
+
/// <summary>
/// AutoContracts is an experimental feature that will fill much of the dynamic-frames boilerplate
/// into a class. From the user's perspective, what needs to be done is simply:
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index e3915e6d..a1fbe646 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -2860,11 +2860,11 @@ namespace Microsoft.Dafny {
#if VERIFY_CORRECTNESS_OF_TRANSLATION_FORALL_STATEMENT_RANGE
var definedness = new Bpl.StmtListBuilder();
var exporter = new Bpl.StmtListBuilder();
- TrForallStmtCall(m.tok, parBoundVars, parRange, decrCheck, recursiveCall, definedness, exporter, localVariables, etran);
+ TrForallStmtCall(m.tok, parBoundVars, parRange, decrCheck, null, recursiveCall, definedness, exporter, localVariables, etran);
// All done, so put the two pieces together
builder.Add(new Bpl.IfCmd(m.tok, null, definedness.Collect(m.tok), null, exporter.Collect(m.tok)));
#else
- TrForallStmtCall(m.tok, parBoundVars, parRange, decrCheck, recursiveCall, null, builder, localVariables, etran);
+ TrForallStmtCall(m.tok, parBoundVars, parRange, decrCheck, null, recursiveCall, null, builder, localVariables, etran);
#endif
}
// translate the body of the method
@@ -7418,7 +7418,7 @@ namespace Microsoft.Dafny {
var s0 = (CallStmt)s.S0;
var definedness = new Bpl.StmtListBuilder();
var exporter = new Bpl.StmtListBuilder();
- TrForallStmtCall(s.Tok, s.BoundVars, s.Range, null, s0, definedness, exporter, locals, etran);
+ TrForallStmtCall(s.Tok, s.BoundVars, s.Range, null, s.ForallExpressions, s0, definedness, exporter, locals, etran);
// All done, so put the two pieces together
builder.Add(new Bpl.IfCmd(s.Tok, null, definedness.Collect(s.Tok), null, exporter.Collect(s.Tok)));
builder.Add(CaptureState(stmt));
@@ -8043,65 +8043,16 @@ namespace Microsoft.Dafny {
Bpl.Expr qq = new Bpl.ForallExpr(s.Tok, new List<TypeVariable> { alpha }, new List<Variable> { oVar, fVar }, null, tr, body);
updater.Add(new Bpl.AssumeCmd(s.Tok, qq));
- if (s0.Rhs is ExprRhs) {
- Expression Fi = null;
- Func<Expression,Expression> lhsBuilder = null;
- lhs = s0.Lhs.Resolved;
- var i = s.BoundVars[0];
- if (s.BoundVars.Count == 1) {
- //var lhsContext = null;
- // Detect the following cases:
- // 0: forall i | R(i) { F(i).f := E(i); }
- // 1: forall i | R(i) { A[F(i)] := E(i); }
- // 2: forall i | R(i) { F(i)[N] := E(i); }
- if (lhs is MemberSelectExpr) {
- var ll = (MemberSelectExpr)lhs;
- Fi = ll.Obj;
- lhsBuilder = e => { var l = new MemberSelectExpr(ll.tok, e, ll.MemberName); l.Member = ll.Member; l.Type = ll.Type; return l; };
- } else if (lhs is SeqSelectExpr) {
- var ll = (SeqSelectExpr)lhs;
- Contract.Assert(ll.SelectOne);
- if (!ContainsFreeVariable(ll.Seq, false, i)) {
- Fi = ll.E0;
- lhsBuilder = e => { var l = new SeqSelectExpr(ll.tok, true, ll.Seq, e, null); l.Type = ll.Type; return l; };
- } else if (!ContainsFreeVariable(ll.E0, false, i)) {
- Fi = ll.Seq;
- lhsBuilder = e => { var l = new SeqSelectExpr(ll.tok, true, e, ll.E0, null); l.Type = ll.Type; return l; };
- }
- }
- }
- var rhs = ((ExprRhs)s0.Rhs).Expr;
- bool usedInversion = false;
- if (Fi != null) {
- var j = new BoundVar(i.tok, i.Name + "#inv", Fi.Type);
- var jj = Expression.CreateIdentExpr(j);
- var jList = new List<BoundVar>() { j };
- var vals = InvertExpression(i, j, s.Range, Fi);
-#if DEBUG_PRINT
- Console.WriteLine("DEBUG: Trying to invert:");
- Console.WriteLine("DEBUG: " + Printer.ExprToString(s.Range) + " && " + j.Name + " == " + Printer.ExprToString(Fi));
- if (vals == null) {
- Console.WriteLine("DEBUG: Can't");
- } else {
- Console.WriteLine("DEBUG: The inverse is the disjunction of the following:");
- foreach (var val in vals) {
- Console.WriteLine("DEBUG: " + Printer.ExprToString(val.Range) + " && " + Printer.ExprToString(val.FInverse) + " == " + i.Name);
- }
- }
-#endif
- if (vals != null) {
- foreach (var val in vals) {
- qq = TrForall_NewValueAssumption(s.Tok, jList, val.Range, lhsBuilder(jj), Substitute(rhs, i, val.FInverse), true, etran, prevEtran);
- updater.Add(new Bpl.AssumeCmd(s.Tok, qq));
- }
- usedInversion = true;
- }
- }
- if (!usedInversion) {
- qq = TrForall_NewValueAssumption(s.Tok, s.BoundVars, s.Range, lhs, rhs, false, etran, prevEtran);
+ if (s.ForallExpressions != null) {
+ foreach (ForallExpr expr in s.ForallExpressions) {
+ BinaryExpr term = (BinaryExpr)expr.Term;
+ Contract.Assert(term != null);
+ var e0 = Substitute(((BinaryExpr)term).E0.Resolved, null, substMap);
+ var e1 = Substitute(((BinaryExpr)term).E1, null, substMap);
+ qq = TrForall_NewValueAssumption(expr.tok, expr.BoundVars, expr.Range, e0, e1, expr.Attributes, etran, prevEtran);
updater.Add(new Bpl.AssumeCmd(s.Tok, qq));
}
- }
+ }
}
/// <summary>
@@ -8115,7 +8066,7 @@ namespace Microsoft.Dafny {
/// G is rhs
/// If lhsAsTrigger is true, then use the LHS of the equality above as the trigger; otherwise, don't specify any trigger.
/// </summary>
- private Bpl.Expr TrForall_NewValueAssumption(IToken tok, List<BoundVar> boundVars, Expression range, Expression lhs, Expression rhs, bool lhsAsTrigger, ExpressionTranslator etran, ExpressionTranslator prevEtran) {
+ private Bpl.Expr TrForall_NewValueAssumption(IToken tok, List<BoundVar> boundVars, Expression range, Expression lhs, Expression rhs, Attributes attributes, ExpressionTranslator etran, ExpressionTranslator prevEtran) {
Contract.Requires(tok != null);
Contract.Requires(boundVars != null);
Contract.Requires(range != null);
@@ -8135,159 +8086,27 @@ namespace Microsoft.Dafny {
Type lhsType = lhs is MemberSelectExpr ? ((MemberSelectExpr)lhs).Type : null;
g = CondApplyBox(rhs.tok, g, rhs.Type, lhsType);
- Trigger tr = lhsAsTrigger ? new Trigger(tok, true, new List<Bpl.Expr>() { xHeapOF }) : null;
- return new Bpl.ForallExpr(tok, xBvars, tr, Bpl.Expr.Imp(xAnte, Bpl.Expr.Eq(xHeapOF, g)));
- }
-
- class ForallStmtTranslationValues
- {
- public readonly Expression Range;
- public readonly Expression FInverse;
- public ForallStmtTranslationValues(Expression range, Expression fInverse) {
- Contract.Requires(range != null);
- Contract.Requires(fInverse != null);
- Range = range;
- FInverse = fInverse;
- }
- public ForallStmtTranslationValues Subst(IVariable j, Expression e, Translator translator) {
- Contract.Requires(j != null);
- Contract.Requires(e != null);
- Contract.Requires(translator != null);
- var substMap = new Dictionary<IVariable, Expression>();
- substMap.Add(j, e);
- var v = new ForallStmtTranslationValues(translator.Substitute(Range, null, substMap), translator.Substitute(FInverse, null, substMap));
- return v;
- }
- }
-
- /// <summary>
- /// Find piecewise inverse of F under R. More precisely, find lists of expressions P and F-1
- /// such that
- /// R(i) && j == F(i)
- /// holds iff the disjunction of the following predicates holds:
- /// P_0(j) && F-1_0(j) == i
- /// ...
- /// P_{n-1}(j) && F-1_{n-1}(j) == i
- /// If no such disjunction is found, return null.
- /// If such a disjunction is found, return for each disjunct:
- /// * The predicate P_k(j), which is an expression that may have free occurrences of j (but no free occurrences of i)
- /// * The expression F-1_k(j), which also may have free occurrences of j but not of i
- /// </summary>
- private List<ForallStmtTranslationValues> InvertExpression(BoundVar i, BoundVar j, Expression R, Expression F) {
- Contract.Requires(i != null);
- Contract.Requires(j != null);
- Contract.Requires(R != null);
- Contract.Requires(F != null);
- var vals = new List<ForallStmtTranslationValues>(InvertExpressionIter(i, j, R, F));
- if (vals.Count == 0) {
- return null;
- } else {
- return vals;
- }
- }
- /// <summary>
- /// See InvertExpression.
- /// </summary>
- private IEnumerable<ForallStmtTranslationValues> InvertExpressionIter(BoundVar i, BoundVar j, Expression R, Expression F) {
- Contract.Requires(i != null);
- Contract.Requires(j != null);
- Contract.Requires(R != null);
- Contract.Requires(F != null);
- F = F.Resolved;
- if (!ContainsFreeVariable(F, false, i)) {
- // We're looking at R(i) && j == K.
- // We cannot invert j == K, but if we're lucky, R(i) contains a conjunct i==G.
- Expression r = Expression.CreateBoolLiteral(R.tok, true);
- Expression G = null;
- foreach (var c in Expression.Conjuncts(R)) {
- if (G == null && c is BinaryExpr) {
- var bin = (BinaryExpr)c;
- if (BinaryExpr.IsEqualityOp(bin.ResolvedOp)) {
- var id = bin.E0.Resolved as IdentifierExpr;
- if (id != null && id.Var == i) {
- G = bin.E1;
- continue;
- }
- id = bin.E1.Resolved as IdentifierExpr;
- if (id != null && id.Var == i) {
- G = bin.E0;
- continue;
- }
+ Bpl.Trigger tr = null;
+ var argsEtran = etran.WithNoLits();
+ foreach (var aa in attributes.AsEnumerable()) {
+ if (aa.Name == "trigger") {
+ List<Bpl.Expr> tt = new List<Bpl.Expr>();
+ foreach (var arg in aa.Args) {
+ if (arg == lhs) {
+ tt.Add(xHeapOF);
+ } else {
+ tt.Add(argsEtran.TrExpr(arg));
}
}
- r = Expression.CreateAnd(r, c);
- }
- if (G != null) {
- var jIsK = Expression.CreateEq(Expression.CreateIdentExpr(j), F, j.Type);
- var rr = Substitute(r, i, G);
- yield return new ForallStmtTranslationValues(Expression.CreateAnd(rr, jIsK), G);
- }
- } else if (F is IdentifierExpr) {
- var e = (IdentifierExpr)F;
- if (e.Var == i) {
- // We're looking at R(i) && j == i, which is particularly easy to invert: R(j) && j == i
- var jj = Expression.CreateIdentExpr(j);
- yield return new ForallStmtTranslationValues(Substitute(R, i, jj), jj);
- }
- } else if (F is BinaryExpr) {
- var bin = (BinaryExpr)F;
- if (bin.ResolvedOp == BinaryExpr.ResolvedOpcode.Add && (bin.E0.Type.IsIntegerType || bin.E0.Type.IsRealType)) {
- if (!ContainsFreeVariable(bin.E1, false, i)) {
- // We're looking at: R(i) && j == f(i) + K.
- // By a recursive call, we'll ask to invert: R(i) && j' == f(i).
- // For each P_0(j') && f-1_0(j') == i we get back, we yield:
- // P_0(j - K) && f-1_0(j - K) == i
- var jMinusK = Expression.CreateSubtract(Expression.CreateIdentExpr(j), bin.E1);
- foreach (var val in InvertExpression(i, j, R, bin.E0)) {
- yield return val.Subst(j, jMinusK, this);
- }
- } else if (!ContainsFreeVariable(bin.E0, false, i)) {
- // We're looking at: R(i) && j == K + f(i)
- // Do as in previous case, but with operands reversed.
- var jMinusK = Expression.CreateSubtract(Expression.CreateIdentExpr(j), bin.E0);
- foreach (var val in InvertExpression(i, j, R, bin.E1)) {
- yield return val.Subst(j, jMinusK, this);
- }
- }
- } else if (bin.ResolvedOp == BinaryExpr.ResolvedOpcode.Sub && (bin.E0.Type.IsIntegerType || bin.E0.Type.IsRealType)) {
- if (!ContainsFreeVariable(bin.E1, false, i)) {
- // We're looking at: R(i) && j == f(i) - K
- // Recurse on f(i) and then replace j := j + K
- var jPlusK = Expression.CreateAdd(Expression.CreateIdentExpr(j), bin.E1);
- foreach (var val in InvertExpression(i, j, R, bin.E0)) {
- yield return val.Subst(j, jPlusK, this);
- }
- } else if (!ContainsFreeVariable(bin.E0, false, i)) {
- // We're looking at: R(i) && j == K - f(i)
- // Recurse on f(i) and then replace j := K - j
- var kMinusJ = Expression.CreateAdd(Expression.CreateIdentExpr(j), bin.E0);
- foreach (var val in InvertExpression(i, j, R, bin.E1)) {
- yield return val.Subst(j, kMinusJ, this);
- }
- }
- }
- } else if (F is ITEExpr) {
- var ife = (ITEExpr)F;
- // We're looking at R(i) && j == if A(i) then B(i) else C(i), which is equivalent to the disjunction of:
- // R(i) && A(i) && j == B(i)
- // R(i) && !A(i) && j == C(i)
- // We recurse on each one, yielding the results
- var r = Expression.CreateAnd(R, ife.Test);
- var valsThen = InvertExpression(i, j, r, ife.Thn);
- if (valsThen != null) {
- r = Expression.CreateAnd(R, Expression.CreateNot(ife.tok, ife.Test));
- var valsElse = InvertExpression(i, j, r, ife.Els);
- if (valsElse != null) {
- foreach (var val in valsThen) { yield return val; }
- foreach (var val in valsElse) { yield return val; }
- }
+ tr = new Bpl.Trigger(tok, true, tt, tr);
}
}
+ return new Bpl.ForallExpr(tok, xBvars, tr, Bpl.Expr.Imp(xAnte, Bpl.Expr.Eq(xHeapOF, g)));
}
delegate Bpl.Expr ExpressionConverter(Dictionary<IVariable, Expression> substMap, ExpressionTranslator etran);
- void TrForallStmtCall(IToken tok, List<BoundVar> boundVars, Expression range, ExpressionConverter additionalRange, CallStmt s0,
+ void TrForallStmtCall(IToken tok, List<BoundVar> boundVars, Expression range, ExpressionConverter additionalRange, List<Expression> forallExpressions, CallStmt s0,
Bpl.StmtListBuilder definedness, Bpl.StmtListBuilder exporter, List<Variable> locals, ExpressionTranslator etran) {
Contract.Requires(tok != null);
Contract.Requires(boundVars != null);
@@ -8370,38 +8189,56 @@ namespace Microsoft.Dafny {
RecordNewObjectsIn_New(tok, iter, initHeap, heapIdExpr, exporter, locals, etran);
}
- var bvars = new List<Variable>();
- Dictionary<IVariable, Expression> substMap;
- var ante = initEtran.TrBoundVariablesRename(boundVars, bvars, out substMap);
- ante = BplAnd(ante, initEtran.TrExpr(Substitute(range, null, substMap)));
- if (additionalRange != null) {
- ante = BplAnd(ante, additionalRange(substMap, initEtran));
- }
-
// Note, in the following, we need to do a bit of a song and dance. The actual arguments of the
// call should be translated using "initEtran", whereas the method postcondition should be translated
// using "callEtran". To accomplish this, we translate the argument and then tuck the resulting
// Boogie expressions into BoogieExprWrappers that are used in the DafnyExpr-to-DafnyExpr substitution.
- // TODO
- var argsSubstMap = new Dictionary<IVariable, Expression>(); // maps formal arguments to actuals
- Contract.Assert(s0.Method.Ins.Count == s0.Args.Count);
- for (int i = 0; i < s0.Method.Ins.Count; i++) {
- var arg = Substitute(s0.Args[i], null, substMap, s0.MethodSelect.TypeArgumentSubstitutions()); // substitute the renamed bound variables for the declared ones
- argsSubstMap.Add(s0.Method.Ins[i], new BoogieWrapper(initEtran.TrExpr(arg), s0.Args[i].Type));
- }
- var receiver = new BoogieWrapper(initEtran.TrExpr(Substitute(s0.Receiver, null, substMap, s0.MethodSelect.TypeArgumentSubstitutions())), s0.Receiver.Type);
- var callEtran = new ExpressionTranslator(this, predef, etran.HeapExpr, initHeap);
- Bpl.Expr post = Bpl.Expr.True;
- foreach (var ens in s0.Method.Ens) {
- var p = Substitute(ens.E, receiver, argsSubstMap, s0.MethodSelect.TypeArgumentSubstitutions()); // substitute the call's actuals for the method's formals
- post = BplAnd(post, callEtran.TrExpr(p));
- }
-
- // TRIG (forall $ih#s0#0: Seq Box :: $Is($ih#s0#0, TSeq(TChar)) && $IsAlloc($ih#s0#0, TSeq(TChar), $initHeapForallStmt#0) && Seq#Length($ih#s0#0) != 0 && Seq#Rank($ih#s0#0) < Seq#Rank(s#0) ==> (forall i#2: int :: true ==> LitInt(0) <= i#2 && i#2 < Seq#Length($ih#s0#0) ==> char#ToInt(_module.CharChar.MinChar($LS($LZ), $Heap, this, $ih#s0#0)) <= char#ToInt($Unbox(Seq#Index($ih#s0#0, i#2)): char)))
- // TRIG (forall $ih#pat0#0: Seq Box, $ih#a0#0: Seq Box :: $Is($ih#pat0#0, TSeq(_module._default.Same0$T)) && $IsAlloc($ih#pat0#0, TSeq(_module._default.Same0$T), $initHeapForallStmt#0) && $Is($ih#a0#0, TSeq(_module._default.Same0$T)) && $IsAlloc($ih#a0#0, TSeq(_module._default.Same0$T), $initHeapForallStmt#0) && Seq#Length($ih#pat0#0) <= Seq#Length($ih#a0#0) && Seq#SameUntil($ih#pat0#0, $ih#a0#0, Seq#Length($ih#pat0#0)) && (Seq#Rank($ih#pat0#0) < Seq#Rank(pat#0) || (Seq#Rank($ih#pat0#0) == Seq#Rank(pat#0) && Seq#Rank($ih#a0#0) < Seq#Rank(a#0))) ==> _module.__default.IsRelaxedPrefixAux(_module._default.Same0$T, $LS($LZ), $Heap, $ih#pat0#0, $ih#a0#0, LitInt(1)))'
- // TRIG (forall $ih#m0#0: DatatypeType, $ih#n0#0: DatatypeType :: $Is($ih#m0#0, Tclass._module.Nat()) && $IsAlloc($ih#m0#0, Tclass._module.Nat(), $initHeapForallStmt#0) && $Is($ih#n0#0, Tclass._module.Nat()) && $IsAlloc($ih#n0#0, Tclass._module.Nat(), $initHeapForallStmt#0) && Lit(true) && (DtRank($ih#m0#0) < DtRank(m#0) || (DtRank($ih#m0#0) == DtRank(m#0) && DtRank($ih#n0#0) < DtRank(n#0))) ==> _module.__default.mult($LS($LZ), $Heap, $ih#m0#0, _module.__default.plus($LS($LZ), $Heap, $ih#n0#0, $ih#n0#0)) == _module.__default.mult($LS($LZ), $Heap, _module.__default.plus($LS($LZ), $Heap, $ih#m0#0, $ih#m0#0), $ih#n0#0))
- Bpl.Expr qq = new Bpl.ForallExpr(tok, bvars, Bpl.Expr.Imp(ante, post)); // SMART_TRIGGER
- exporter.Add(new Bpl.AssumeCmd(tok, qq));
+ // TODO
+ Bpl.Expr qq;
+ if (forallExpressions != null) {
+ var callEtran = new ExpressionTranslator(this, predef, etran.HeapExpr, initHeap);
+ foreach (Expression expr in forallExpressions) {
+ Dictionary<IVariable, Expression> substMap = new Dictionary<IVariable, Expression>();
+ var e = Substitute(expr, null, substMap, null);
+ var argsSubstMap = new Dictionary<IVariable, Expression>();
+ Contract.Assert(s0.Method.Ins.Count == s0.Args.Count);
+ for (int i = 0; i < s0.Method.Ins.Count; i++) {
+ var arg = Substitute(s0.Args[i], null, substMap, s0.MethodSelect.TypeArgumentSubstitutions()); // substitute the renamed bound variables for the declared ones
+ argsSubstMap.Add(s0.Method.Ins[i], new BoogieWrapper(initEtran.TrExpr(arg), s0.Args[i].Type));
+ }
+ var receiver = new BoogieWrapper(initEtran.TrExpr(Substitute(s0.Receiver, null, substMap, s0.MethodSelect.TypeArgumentSubstitutions())), s0.Receiver.Type);
+ var p = Substitute(e, receiver, argsSubstMap, s0.MethodSelect.TypeArgumentSubstitutions()); // substitute the call's actuals for the method's formals
+ qq = callEtran.TrExpr(p, initEtran);
+ exporter.Add(new Bpl.AssumeCmd(tok, qq));
+ }
+ } else {
+ var bvars = new List<Variable>();
+ Dictionary<IVariable, Expression> substMap;
+ var ante = initEtran.TrBoundVariablesRename(boundVars, bvars, out substMap);
+ var argsSubstMap = new Dictionary<IVariable, Expression>(); // maps formal arguments to actuals
+ Contract.Assert(s0.Method.Ins.Count == s0.Args.Count);
+ for (int i = 0; i < s0.Method.Ins.Count; i++) {
+ var arg = Substitute(s0.Args[i], null, substMap, s0.MethodSelect.TypeArgumentSubstitutions()); // substitute the renamed bound variables for the declared ones
+ argsSubstMap.Add(s0.Method.Ins[i], new BoogieWrapper(initEtran.TrExpr(arg), s0.Args[i].Type));
+ }
+ var callEtran = new ExpressionTranslator(this, predef, etran.HeapExpr, initHeap);
+ ante = BplAnd(ante, initEtran.TrExpr(Substitute(range, null, substMap)));
+ if (additionalRange != null) {
+ ante = BplAnd(ante, additionalRange(substMap, initEtran));
+ }
+ var receiver = new BoogieWrapper(initEtran.TrExpr(Substitute(s0.Receiver, null, substMap, s0.MethodSelect.TypeArgumentSubstitutions())), s0.Receiver.Type);
+ Bpl.Expr post = Bpl.Expr.True;
+ foreach (var ens in s0.Method.Ens) {
+ var p = Substitute(ens.E, receiver, argsSubstMap, s0.MethodSelect.TypeArgumentSubstitutions()); // substitute the call's actuals for the method's formals
+ post = BplAnd(post, callEtran.TrExpr(p));
+ }
+
+ // TRIG (forall $ih#s0#0: Seq Box :: $Is($ih#s0#0, TSeq(TChar)) && $IsAlloc($ih#s0#0, TSeq(TChar), $initHeapForallStmt#0) && Seq#Length($ih#s0#0) != 0 && Seq#Rank($ih#s0#0) < Seq#Rank(s#0) ==> (forall i#2: int :: true ==> LitInt(0) <= i#2 && i#2 < Seq#Length($ih#s0#0) ==> char#ToInt(_module.CharChar.MinChar($LS($LZ), $Heap, this, $ih#s0#0)) <= char#ToInt($Unbox(Seq#Index($ih#s0#0, i#2)): char)))
+ // TRIG (forall $ih#pat0#0: Seq Box, $ih#a0#0: Seq Box :: $Is($ih#pat0#0, TSeq(_module._default.Same0$T)) && $IsAlloc($ih#pat0#0, TSeq(_module._default.Same0$T), $initHeapForallStmt#0) && $Is($ih#a0#0, TSeq(_module._default.Same0$T)) && $IsAlloc($ih#a0#0, TSeq(_module._default.Same0$T), $initHeapForallStmt#0) && Seq#Length($ih#pat0#0) <= Seq#Length($ih#a0#0) && Seq#SameUntil($ih#pat0#0, $ih#a0#0, Seq#Length($ih#pat0#0)) && (Seq#Rank($ih#pat0#0) < Seq#Rank(pat#0) || (Seq#Rank($ih#pat0#0) == Seq#Rank(pat#0) && Seq#Rank($ih#a0#0) < Seq#Rank(a#0))) ==> _module.__default.IsRelaxedPrefixAux(_module._default.Same0$T, $LS($LZ), $Heap, $ih#pat0#0, $ih#a0#0, LitInt(1)))'
+ // TRIG (forall $ih#m0#0: DatatypeType, $ih#n0#0: DatatypeType :: $Is($ih#m0#0, Tclass._module.Nat()) && $IsAlloc($ih#m0#0, Tclass._module.Nat(), $initHeapForallStmt#0) && $Is($ih#n0#0, Tclass._module.Nat()) && $IsAlloc($ih#n0#0, Tclass._module.Nat(), $initHeapForallStmt#0) && Lit(true) && (DtRank($ih#m0#0) < DtRank(m#0) || (DtRank($ih#m0#0) == DtRank(m#0) && DtRank($ih#n0#0) < DtRank(n#0))) ==> _module.__default.mult($LS($LZ), $Heap, $ih#m0#0, _module.__default.plus($LS($LZ), $Heap, $ih#n0#0, $ih#n0#0)) == _module.__default.mult($LS($LZ), $Heap, _module.__default.plus($LS($LZ), $Heap, $ih#m0#0, $ih#m0#0), $ih#n0#0))
+ qq = new Bpl.ForallExpr(tok, bvars, Bpl.Expr.Imp(ante, post)); // SMART_TRIGGER
+ exporter.Add(new Bpl.AssumeCmd(tok, qq));
+ }
}
}
@@ -8506,24 +8343,14 @@ namespace Microsoft.Dafny {
}
}
- var bvars = new List<Variable>();
- Dictionary<IVariable, Expression> substMap;
- var ante = initEtran.TrBoundVariablesRename(s.BoundVars, bvars, out substMap);
- var range = Substitute(s.Range, null, substMap);
- ante = BplAnd(ante, initEtran.TrExpr(range));
-
- Bpl.Expr post = Bpl.Expr.True;
- foreach (var ens in s.Ens) {
- var p = Substitute(ens.E, null, substMap);
- post = BplAnd(post, etran.TrExpr(p));
- }
-
- Bpl.Expr qq = Bpl.Expr.Imp(ante, post);
- if (bvars.Count != 0) {
- var triggers = TrTrigger(etran, s.Attributes, s.Tok, substMap);
- qq = new Bpl.ForallExpr(s.Tok, bvars, triggers, qq);
+ Dictionary<IVariable, Expression> substMap = new Dictionary<IVariable, Expression>();
+ var p = Substitute(s.ForallExpressions[0], null, substMap);
+ Bpl.Expr qq = etran.TrExpr(p, initEtran);
+ if (s.BoundVars.Count != 0) {
+ exporter.Add(new Bpl.AssumeCmd(s.Tok, qq));
+ } else {
+ exporter.Add(new Bpl.AssumeCmd(s.Tok, ((Bpl.ForallExpr)qq).Body));
}
- exporter.Add(new Bpl.AssumeCmd(s.Tok, qq));
}
private string GetObjFieldDetails(Expression lhs, ExpressionTranslator etran, out Bpl.Expr obj, out Bpl.Expr F) {
@@ -10873,7 +10700,10 @@ namespace Microsoft.Dafny {
/// filled in, but it is really necessary for anything that may show up in a Boogie assert, since that location may
/// then show up in an error message).
/// </summary>
- public Bpl.Expr TrExpr(Expression expr)
+ public Bpl.Expr TrExpr(Expression expr) {
+ return TrExpr(expr, null);
+ }
+ public Bpl.Expr TrExpr(Expression expr, ExpressionTranslator etran)
{
Contract.Requires(expr != null);
Contract.Requires(predef != null);
@@ -11688,7 +11518,7 @@ namespace Microsoft.Dafny {
List<Variable> tyvars = translator.MkTyParamBinders(e.TypeArgs);
List<Variable> bvars = new List<Variable>();
- var initEtran = this;
+ var initEtran = (etran == null) ? this : etran;
var bodyEtran = this;
bool _scratch = true;
@@ -11709,7 +11539,7 @@ namespace Microsoft.Dafny {
});
}
- antecedent = BplAnd(antecedent, bodyEtran.TrBoundVariables(e.BoundVars, bvars));
+ antecedent = BplAnd(antecedent, initEtran.TrBoundVariables(e.BoundVars, bvars));
Bpl.QKeyValue kv = TrAttributes(e.Attributes, "trigger");
Bpl.Trigger tr = null;
@@ -11724,7 +11554,7 @@ namespace Microsoft.Dafny {
}
}
if (e.Range != null) {
- antecedent = BplAnd(antecedent, bodyEtran.TrExpr(e.Range));
+ antecedent = BplAnd(antecedent, initEtran.TrExpr(e.Range));
}
Bpl.Expr body = bodyEtran.TrExpr(e.Term);
diff --git a/Source/Dafny/Triggers/QuantifierSplitter.cs b/Source/Dafny/Triggers/QuantifierSplitter.cs
index 865aa33e..e46b64fb 100644
--- a/Source/Dafny/Triggers/QuantifierSplitter.cs
+++ b/Source/Dafny/Triggers/QuantifierSplitter.cs
@@ -114,6 +114,18 @@ namespace Microsoft.Dafny.Triggers {
}
}
+ protected override void VisitOneStmt(Statement stmt) {
+ Contract.Requires(stmt != null);
+ if (stmt is ForallStmt) {
+ ForallStmt s = (ForallStmt)stmt;
+ if (s.ForallExpressions != null) {
+ foreach (Expression expr in s.ForallExpressions) {
+ VisitOneExpr(expr);
+ }
+ }
+ }
+ }
+
/// <summary>
/// See comments above definition of splits for reason why this method exists
/// </summary>
diff --git a/Source/Dafny/Triggers/QuantifiersCollector.cs b/Source/Dafny/Triggers/QuantifiersCollector.cs
index 1f37dcfa..789e7614 100644
--- a/Source/Dafny/Triggers/QuantifiersCollector.cs
+++ b/Source/Dafny/Triggers/QuantifiersCollector.cs
@@ -40,5 +40,18 @@ namespace Microsoft.Dafny.Triggers {
return true;
}
+
+ protected override bool VisitOneStmt(Statement stmt, ref bool st) {
+ Contract.Requires(stmt != null);
+ if (stmt is ForallStmt) {
+ ForallStmt s = (ForallStmt)stmt;
+ if (s.ForallExpressions != null) {
+ foreach (Expression expr in s.ForallExpressions) {
+ VisitOneExpr(expr, ref st);
+ }
+ }
+ }
+ return true;
+ }
}
}