Dafny: added heuristics for finding witnesses in assign-such-that checking

3 files changed, 202 insertions, 26 deletions

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index 98319473..1c43a530 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -3490,6 +3490,11 @@ namespace Microsoft.Dafny {
       public readonly Expression Set;

       public SetBoundedPool(Expression set) { Set = set; }

     }

+    public class SuperSetBoundedPool : BoundedPool

+    {

+      public readonly Expression LowerBound;

+      public SuperSetBoundedPool(Expression set) { LowerBound = set; }

+    }

     public class MapBoundedPool : BoundedPool

     {

       public readonly Expression Map;

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 17f35b1e..b9cc8a55 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -2870,7 +2870,7 @@ namespace Microsoft.Dafny
         bool bodyMustBeSpecOnly = specContextOnly || (prevErrorCount == ErrorCount && UsesSpecFeatures(s.Range));

         if (!bodyMustBeSpecOnly && prevErrorCount == ErrorCount) {

           var missingBounds = new List<BoundVar>();

-          s.Bounds = DiscoverBounds(s.Tok, s.BoundVars, s.Range, true, missingBounds);

+          s.Bounds = DiscoverBounds(s.Tok, s.BoundVars, s.Range, true, false, missingBounds);

           if (missingBounds.Count != 0) {

             bodyMustBeSpecOnly = true;

           }

@@ -4198,7 +4198,7 @@ namespace Microsoft.Dafny
 

         if (prevErrorCount == ErrorCount) {

           var missingBounds = new List<BoundVar>();

-          e.Bounds = DiscoverBounds(e.tok, e.BoundVars, e.LogicalBody(), e is ExistsExpr, missingBounds);

+          e.Bounds = DiscoverBounds(e.tok, e.BoundVars, e.LogicalBody(), e is ExistsExpr, false, missingBounds);

           if (missingBounds.Count != 0) {

             // Report errors here about quantifications that depend on the allocation state.

             var mb = missingBounds;

@@ -4242,7 +4242,7 @@ namespace Microsoft.Dafny
 

         if (prevErrorCount == ErrorCount) {

           var missingBounds = new List<BoundVar>();

-          e.Bounds = DiscoverBounds(e.tok, e.BoundVars, e.Range, true, missingBounds);

+          e.Bounds = DiscoverBounds(e.tok, e.BoundVars, e.Range, true, false, missingBounds);

           if (missingBounds.Count != 0) {

             e.MissingBounds = missingBounds;

             foreach (var bv in e.MissingBounds) {

@@ -4278,7 +4278,7 @@ namespace Microsoft.Dafny
 

         if (prevErrorCount == ErrorCount) {

           var missingBounds = new List<BoundVar>();

-          e.Bounds = DiscoverBounds(e.tok, e.BoundVars, e.Range, true, missingBounds);

+          e.Bounds = DiscoverBounds(e.tok, e.BoundVars, e.Range, true, false, missingBounds);

           if (missingBounds.Count != 0) {

             e.MissingBounds = missingBounds;

             foreach (var bv in e.MissingBounds) {

@@ -4990,19 +4990,31 @@ namespace Microsoft.Dafny
     /// <summary>

     /// Tries to find a bounded pool for each of the bound variables "bvars" of "expr".  If this process

     /// fails, then "null" is returned and the bound variables for which the process fails are added to "missingBounds".

+    /// If "returnAllBounds" is false, then:

+    ///   -- at most one BoundedPool per variable is returned

+    ///   -- every IntBoundedPool returned has both a lower and an upper bound

+    ///   -- no SuperSetBoundedPool is returned

+    /// If "returnAllBounds" is true, then:

+    ///   -- a variable may give rise to BoundedPool's

+    ///   -- IntBoundedPool bounds may have just one component

+    ///   -- a non-null return value means that some bound were found for each variable (but, for example, perhaps one

+    ///      variable only has lower bounds, no upper bounds)

     /// Requires "expr" to be successfully resolved.

     /// </summary>

-    List<QuantifierExpr.BoundedPool> DiscoverBounds(IToken tok, List<BoundVar> bvars, Expression expr, bool polarity, List<BoundVar> missingBounds) {

+    public static List<QuantifierExpr.BoundedPool> DiscoverBounds(IToken tok, List<BoundVar> bvars, Expression expr, bool polarity, bool returnAllBounds, List<BoundVar> missingBounds) {

       Contract.Requires(tok != null);

       Contract.Requires(bvars != null);

       Contract.Requires(missingBounds != null);

       Contract.Requires(expr != null);

       Contract.Requires(expr.Type != null);  // a sanity check (but not a complete proof) that "expr" has been resolved

       Contract.Ensures(

-        (Contract.Result<List<QuantifierExpr.BoundedPool>>() != null &&

+        (returnAllBounds && Contract.OldValue(missingBounds.Count) <= missingBounds.Count) ||

+        (!returnAllBounds &&

+         Contract.Result<List<QuantifierExpr.BoundedPool>>() != null &&

          Contract.Result<List<QuantifierExpr.BoundedPool>>().Count == bvars.Count &&

          Contract.OldValue(missingBounds.Count) == missingBounds.Count) ||

-        (Contract.Result<List<QuantifierExpr.BoundedPool>>() == null &&

+        (!returnAllBounds &&

+         Contract.Result<List<QuantifierExpr.BoundedPool>>() == null &&

          Contract.OldValue(missingBounds.Count) < missingBounds.Count));

 

       var bounds = new List<QuantifierExpr.BoundedPool>();

@@ -5018,6 +5030,12 @@ namespace Microsoft.Dafny
           // Go through the conjuncts of the range expression to look for bounds.

           Expression lowerBound = bv.Type is NatType ? new LiteralExpr(bv.tok, new BigInteger(0)) : null;

           Expression upperBound = null;

+          bool foundBoundsForBv = false;

+          if (lowerBound != null) {

+            bounds.Add(new QuantifierExpr.IntBoundedPool(lowerBound, upperBound));

+            lowerBound = null;

+            foundBoundsForBv = true;

+          }

           foreach (var conjunct in NormalizedConjuncts(expr, polarity)) {

             var c = conjunct as BinaryExpr;

             if (c == null) {

@@ -5033,32 +5051,47 @@ namespace Microsoft.Dafny
               case BinaryExpr.ResolvedOpcode.InSet:

                 if (whereIsBv == 0) {

                   bounds.Add(new QuantifierExpr.SetBoundedPool(e1));

-                  goto CHECK_NEXT_BOUND_VARIABLE;

+                  foundBoundsForBv = true;

+                  if (!returnAllBounds) goto CHECK_NEXT_BOUND_VARIABLE;

+                }

+                break;

+              case BinaryExpr.ResolvedOpcode.Subset:

+                if (returnAllBounds && whereIsBv == 1) {

+                  bounds.Add(new QuantifierExpr.SuperSetBoundedPool(e0));

+                  foundBoundsForBv = true;

                 }

                 break;

               case BinaryExpr.ResolvedOpcode.InMultiSet:

                 if (whereIsBv == 0) {

                   bounds.Add(new QuantifierExpr.SetBoundedPool(e1));

-                  goto CHECK_NEXT_BOUND_VARIABLE;

+                  foundBoundsForBv = true;

+                  if (!returnAllBounds) goto CHECK_NEXT_BOUND_VARIABLE;

                 }

                 break;

               case BinaryExpr.ResolvedOpcode.InSeq:

                 if (whereIsBv == 0) {

                   bounds.Add(new QuantifierExpr.SeqBoundedPool(e1));

-                  goto CHECK_NEXT_BOUND_VARIABLE;

+                  foundBoundsForBv = true;

+                  if (!returnAllBounds) goto CHECK_NEXT_BOUND_VARIABLE;

                 }

                 break;

               case BinaryExpr.ResolvedOpcode.InMap:

                 if (whereIsBv == 0) {

                   bounds.Add(new QuantifierExpr.SetBoundedPool(e1));

-                  goto CHECK_NEXT_BOUND_VARIABLE;

+                  foundBoundsForBv = true;

+                  if (!returnAllBounds) goto CHECK_NEXT_BOUND_VARIABLE;

                 }

                 break;

               case BinaryExpr.ResolvedOpcode.EqCommon:

                 if (bv.Type is IntType) {

                   var otherOperand = whereIsBv == 0 ? e1 : e0;

                   bounds.Add(new QuantifierExpr.IntBoundedPool(otherOperand, Plus(otherOperand, 1)));

-                  goto CHECK_NEXT_BOUND_VARIABLE;

+                  foundBoundsForBv = true;

+                  if (!returnAllBounds) goto CHECK_NEXT_BOUND_VARIABLE;

+                } else if (returnAllBounds && bv.Type is SetType) {

+                  var otherOperand = whereIsBv == 0 ? e1 : e0;

+                  bounds.Add(new QuantifierExpr.SuperSetBoundedPool(otherOperand));

+                  foundBoundsForBv = true;

                 }

                 break;

               case BinaryExpr.ResolvedOpcode.Gt:

@@ -5081,16 +5114,22 @@ namespace Microsoft.Dafny
               default:

                 break;

             }

-            if (lowerBound != null && upperBound != null) {

+            if ((lowerBound != null && upperBound != null) ||

+                (returnAllBounds && (lowerBound != null || upperBound != null))) {

               // we have found two halves

               bounds.Add(new QuantifierExpr.IntBoundedPool(lowerBound, upperBound));

-              goto CHECK_NEXT_BOUND_VARIABLE;

+              lowerBound = null;

+              upperBound = null;

+              foundBoundsForBv = true;

+              if (!returnAllBounds) goto CHECK_NEXT_BOUND_VARIABLE;

             }

           CHECK_NEXT_CONJUNCT: ;

           }

-          // we have checked every conjunct in the range expression and still have not discovered good bounds

-          missingBounds.Add(bv);  // record failing bound variable

-          foundError = true;

+          if (!foundBoundsForBv) {

+            // we have checked every conjunct in the range expression and still have not discovered good bounds

+            missingBounds.Add(bv);  // record failing bound variable

+            foundError = true;

+          }

         }

       CHECK_NEXT_BOUND_VARIABLE: ;  // should goto here only if the bound for the current variable has been discovered (otherwise, return with null from this method)

       }

@@ -5105,7 +5144,7 @@ namespace Microsoft.Dafny
     /// The other of "e0" and "e1" is an expression whose free variables are not among "boundVars[bvi..]".

     /// Ensures that the resulting "e0" and "e1" are not ConcreteSyntaxExpression's.

     /// </summary>

-    int SanitizeForBoundDiscovery(List<BoundVar> boundVars, int bvi, BinaryExpr.ResolvedOpcode op, ref Expression e0, ref Expression e1) {

+    static int SanitizeForBoundDiscovery(List<BoundVar> boundVars, int bvi, BinaryExpr.ResolvedOpcode op, ref Expression e0, ref Expression e1) {

       Contract.Requires(e0 != null);

       Contract.Requires(e1 != null);

       Contract.Requires(boundVars != null);

@@ -5229,7 +5268,7 @@ namespace Microsoft.Dafny
     /// Requires "expr" to be successfully resolved.

     /// Ensures that what is returned is not a ConcreteSyntaxExpression.

     /// </summary>

-    IEnumerable<Expression> NormalizedConjuncts(Expression expr, bool polarity) {

+    static IEnumerable<Expression> NormalizedConjuncts(Expression expr, bool polarity) {

       // We consider 5 cases.  To describe them, define P(e)=Conjuncts(e,true) and N(e)=Conjuncts(e,false).

       //   *  X ==> Y    is treated as a shorthand for !X || Y, and so is described by the remaining cases

       //   *  X && Y     P(_) = P(X),P(Y)    and    N(_) = !(X && Y)

@@ -5332,7 +5371,7 @@ namespace Microsoft.Dafny
       }

     }

 

-    Expression Plus(Expression e, int n) {

+    public static Expression Plus(Expression e, int n) {

       Contract.Requires(0 <= n);

 

       var nn = new LiteralExpr(e.tok, n);

@@ -5343,12 +5382,23 @@ namespace Microsoft.Dafny
       return p;

     }

 

+    public static Expression Minus(Expression e, int n) {

+      Contract.Requires(0 <= n);

+

+      var nn = new LiteralExpr(e.tok, n);

+      nn.Type = Type.Int;

+      var p = new BinaryExpr(e.tok, BinaryExpr.Opcode.Sub, e, nn);

+      p.ResolvedOp = BinaryExpr.ResolvedOpcode.Sub;

+      p.Type = Type.Int;

+      return p;

+    }

+

     /// <summary>

     /// Returns the set of free variables in "expr".

     /// Requires "expr" to be successfully resolved.

     /// Ensures that the set returned has no aliases.

     /// </summary>

-    ISet<IVariable> FreeVariables(Expression expr) {

+    static ISet<IVariable> FreeVariables(Expression expr) {

       Contract.Requires(expr != null);

       Contract.Ensures(expr.Type != null);

 

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index b476e7b4..1b8a23ee 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -2154,6 +2154,20 @@ namespace Microsoft.Dafny {
       }

     }

 

+    Bpl.Expr BplOr(Bpl.Expr a, Bpl.Expr b) {

+      Contract.Requires(a != null);

+      Contract.Requires(b != null);

+      Contract.Ensures(Contract.Result<Bpl.Expr>() != null);

+

+      if (a == Bpl.Expr.False) {

+        return b;

+      } else if (b == Bpl.Expr.False) {

+        return a;

+      } else {

+        return Bpl.Expr.Or(a, b);

+      }

+    }

+

     Bpl.Expr BplImp(Bpl.Expr a, Bpl.Expr b) {

       Contract.Requires(a != null);

       Contract.Requires(b != null);

@@ -2161,6 +2175,8 @@ namespace Microsoft.Dafny {
 

       if (a == Bpl.Expr.True || b == Bpl.Expr.True) {

         return b;

+      } else if (a == Bpl.Expr.False) {

+        return Bpl.Expr.True;

       } else {

         return Bpl.Expr.Imp(a, b);

       }

@@ -3791,11 +3807,19 @@ namespace Microsoft.Dafny {
               Contract.Assume(false);  // unexpected case

             }

           }

-          var bvs = new VariableSeq();

-          var typeAntecedent = etran.TrBoundVariables(bvars, bvs);

-          var substE = etran.TrExpr(Substitute(s.Expr, null, substMap));

-          var ex = new Bpl.ExistsExpr(s.Tok, bvs, BplAnd(typeAntecedent, substE));

-          builder.Add(Assert(s.Tok, ex, "cannot establish the existence of LHS values that satisfy the such-that predicate"));

+

+          List<Tuple<List<BoundVar>, Expression>> partialGuesses = GeneratePartialGuesses(bvars, Substitute(s.Expr, null, substMap));

+          Bpl.Expr w = Bpl.Expr.False;

+          foreach (var tup in partialGuesses) {

+            var body = etran.TrExpr(tup.Item2);

+            if (tup.Item1.Count != 0) {

+              var bvs = new VariableSeq();

+              var typeAntecedent = etran.TrBoundVariables(tup.Item1, bvs);

+              body = new Bpl.ExistsExpr(s.Tok, bvs, BplAnd(typeAntecedent, body));

+            }

+            w = BplOr(body, w);

+          }

+          builder.Add(Assert(s.Tok, w, "cannot establish the existence of LHS values that satisfy the such-that predicate"));

         }

         // End by doing the assume

         builder.Add(new Bpl.AssumeCmd(s.Tok, etran.TrExpr(s.Expr)));

@@ -4025,6 +4049,103 @@ namespace Microsoft.Dafny {
       }

     }

 

+    List<Tuple<List<BoundVar>, Expression>> GeneratePartialGuesses(List<BoundVar> bvars, Expression expression) {

+      if (bvars.Count == 0) {

+        var tup = new Tuple<List<BoundVar>, Expression>(new List<BoundVar>(), expression);

+        return new List<Tuple<List<BoundVar>, Expression>>() { tup };

+      }

+      var result = new List<Tuple<List<BoundVar>, Expression>>();

+      var x = bvars[0];

+      var otherBvars = bvars.GetRange(1, bvars.Count - 1);

+      foreach (var tup in GeneratePartialGuesses(otherBvars, expression)) {

+        // in the special case that x does not even occur in expression, we can just ignore x

+        if (!ContainsFreeVariable(tup.Item2, false, x)) {

+          result.Add(tup);

+          continue;

+        }

+        // one possible result is to quantify over all the variables

+        var vs = new List<BoundVar>() { x };

+        vs.AddRange(tup.Item1);

+        result.Add(new Tuple<List<BoundVar>, Expression>(vs, tup.Item2));

+        // other possibilities involve guessing a value for x

+        foreach (var guess in GuessWitnesses(x, tup.Item2)) {

+          var substMap = new Dictionary<IVariable, Expression>();

+          substMap.Add(x, guess);

+          result.Add(new Tuple<List<BoundVar>, Expression>(tup.Item1, Substitute(tup.Item2, null, substMap)));

+        }

+      }

+      return result;

+    }

+

+    IEnumerable<Expression> GuessWitnesses(BoundVar x, Expression expr) {

+      Contract.Requires(x != null);

+      Contract.Requires(expr != null);

+      var lookForBounds = false;

+      if (x.Type is BoolType) {

+        var lit = new LiteralExpr(x.tok, false);

+        lit.Type = Type.Bool;  // resolve here

+        yield return lit;

+        lit = new LiteralExpr(x.tok, true);

+        lit.Type = Type.Bool;  // resolve here

+        yield return lit;

+      } else if (x.Type.IsRefType) {

+        var lit = new LiteralExpr(x.tok);

+        lit.Type = x.Type;

+        yield return lit;

+      } else if (x.Type.IsIndDatatype) {

+        var dt = x.Type.AsIndDatatype;

+        Expression zero = Zero(x.tok, x.Type);

+        if (zero != null) {

+          yield return zero;

+        }

+      } else if (x.Type is SetType) {

+        var empty = new SetDisplayExpr(x.tok, new List<Expression>());

+        empty.Type = x.Type;

+        yield return empty;

+        lookForBounds = true;

+      } else if (x.Type is MultiSetType) {

+        var empty = new MultiSetDisplayExpr(x.tok, new List<Expression>());

+        empty.Type = x.Type;

+        yield return empty;

+        lookForBounds = true;

+      } else if (x.Type is SeqType) {

+        var empty = new SeqDisplayExpr(x.tok, new List<Expression>());

+        empty.Type = x.Type;

+        yield return empty;

+        lookForBounds = true;

+      } else if (x.Type is IntType) {

+        var lit = new LiteralExpr(x.tok, 0);

+        lit.Type = Type.Int;  // resolve here

+        yield return lit;

+        lookForBounds = true;

+      }

+      if (lookForBounds) {

+        var missingBounds = new List<BoundVar>();

+        var bounds = Resolver.DiscoverBounds(x.tok, new List<BoundVar>() { x }, expr, true, true, missingBounds);

+        if (missingBounds.Count == 0) {

+          foreach (var bound in bounds) {

+            if (bound is ComprehensionExpr.IntBoundedPool) {

+              var bnd = (ComprehensionExpr.IntBoundedPool)bound;

+              if (bnd.LowerBound != null) yield return bnd.LowerBound;

+              if (bnd.UpperBound != null) yield return Resolver.Minus(bnd.UpperBound, 1);

+            } else if (bound is ComprehensionExpr.SuperSetBoundedPool) {

+              var bnd = (ComprehensionExpr.SuperSetBoundedPool)bound;

+              yield return bnd.LowerBound;

+            }

+          }

+        }

+      }

+    }

+

+    /// <summary>

+    /// Return a zero-equivalent value for "typ", or return null (for any reason whatsoever).

+    /// </summary>

+    Expression Zero(Bpl.IToken tok, Type typ) {

+      Contract.Requires(tok != null);

+      Contract.Requires(typ != null);

+      return null;  // TODO: this can be improved

+    }

+

     void TrParallelAssign(ParallelStmt s, AssignStmt s0,

       Bpl.StmtListBuilder definedness, Bpl.StmtListBuilder updater, Bpl.VariableSeq locals, ExpressionTranslator etran) {

       // The statement: