diff options
| -rw-r--r-- | Source/Dafny/DafnyAst.cs | 1 | ||||
| -rw-r--r-- | Source/Dafny/Triggers/QuantifiersCollection.cs | 17 | ||||
| -rw-r--r-- | Source/Dafny/Triggers/TriggerUtils.cs | 100 | ||||
| -rw-r--r-- | Source/Dafny/Triggers/TriggersCollector.cs | 5 | ||||
| -rw-r--r-- | Test/triggers/function-applications-are-triggers.dfy.expect | 2 | ||||
| -rw-r--r-- | Test/triggers/redundancy-detection-is-bidirectional.dfy | 29 | ||||
| -rw-r--r-- | Test/triggers/redundancy-detection-is-bidirectional.dfy.expect | 12 |
7 files changed, 143 insertions, 23 deletions
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index c7aae173..9bff2038 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -2965,6 +2965,7 @@ namespace Microsoft.Dafny { }
}
+ [DebuggerDisplay("Bound<{name}>")]
public class BoundVar : NonglobalVariable {
public override bool IsMutable {
get {
diff --git a/Source/Dafny/Triggers/QuantifiersCollection.cs b/Source/Dafny/Triggers/QuantifiersCollection.cs index 6555b52a..114d5f5d 100644 --- a/Source/Dafny/Triggers/QuantifiersCollection.cs +++ b/Source/Dafny/Triggers/QuantifiersCollection.cs @@ -47,15 +47,9 @@ namespace Microsoft.Dafny.Triggers { SelectTriggers();
}
- private bool SubsetGenerationPredicate(List<TriggerTerm> terms, TriggerTerm additionalTerm) {
- // Simple formulas like [P0(i) && P1(i) && P2(i) && P3(i) && P4(i)] yield very
- // large numbers of multi-triggers, most of which are useless. This filter
- // restricts subsets of terms so that we only generate sets of terms where each
- // element contributes at least one variable. In the example above, we'll only
- // get 5 triggers.
- // Note that this may still be an over-approximation, as in the following example:
- // forall a, b :: forall x :: a[x] || b[x] > 0.
- return additionalTerm.Variables.Where(v => v is BoundVar && !terms.Any(t => t.Variables.Contains(v))).Any();
+ private bool SubsetGenerationPredicate(TriggerUtils.SetOfTerms terms, TriggerTerm additionalTerm) {
+ return true; // FIXME Remove this
+ //return additionalTerm.Variables.Where(v => v is BoundVar && !terms.Any(t => t.Variables.Contains(v))).Any();
}
/// <summary>
@@ -68,11 +62,10 @@ namespace Microsoft.Dafny.Triggers { void CollectAndShareTriggers(TriggersCollector triggersCollector) {
var pool = quantifiers.SelectMany(q => triggersCollector.CollectTriggers(q.quantifier));
var distinctPool = pool.Deduplicate(TriggerTerm.Eq);
- var multiPool = TriggerUtils.AllNonEmptySubsets(distinctPool, SubsetGenerationPredicate).Select(candidates => new TriggerCandidate(candidates)).ToList();
foreach (var q in quantifiers) {
- q.CandidateTerms = distinctPool; //Candidate terms are immutable: no copy needed
- q.Candidates = multiPool.Select(candidate => new TriggerCandidate(candidate)).ToList();
+ q.CandidateTerms = distinctPool; // The list of candidate terms is immutable
+ q.Candidates = TriggerUtils.AllNonEmptySubsets(distinctPool, SubsetGenerationPredicate, q.quantifier.BoundVars).Select(set => set.ToTriggerCandidate()).ToList();
}
}
diff --git a/Source/Dafny/Triggers/TriggerUtils.cs b/Source/Dafny/Triggers/TriggerUtils.cs index 4fd139e2..efa1f167 100644 --- a/Source/Dafny/Triggers/TriggerUtils.cs +++ b/Source/Dafny/Triggers/TriggerUtils.cs @@ -15,29 +15,109 @@ namespace Microsoft.Dafny.Triggers { return copy;
}
- internal static IEnumerable<List<T>> AllSubsets<T>(IList<T> source, Func<List<T>, T, bool> predicate, int offset) {
+ internal class SetOfTerms {
+ internal bool IsRedundant { get; private set; }
+ internal List<TriggerTerm> Terms { get; set; }
+
+ private ISet<BoundVar> variables;
+ private Dictionary<BoundVar, TriggerTerm> termOwningAUniqueVar;
+ private Dictionary<TriggerTerm, ISet<BoundVar>> uniqueVarsOwnedByATerm;
+
+ public int Count { get { return Terms.Count; } }
+
+ private SetOfTerms() { }
+
+ internal TriggerCandidate ToTriggerCandidate() {
+ return new TriggerCandidate(Terms);
+ }
+
+ internal static SetOfTerms Empty() {
+ var newSet = new SetOfTerms();
+ newSet.IsRedundant = false;
+ newSet.Terms = new List<TriggerTerm>();
+ newSet.variables = new HashSet<BoundVar>();
+ newSet.termOwningAUniqueVar = new Dictionary<BoundVar, TriggerTerm>();
+ newSet.uniqueVarsOwnedByATerm = new Dictionary<TriggerTerm, ISet<BoundVar>>();
+ return newSet;
+ }
+
+ /// <summary>
+ /// Simple formulas like [P0(i) && P1(i) && P2(i) && P3(i) && P4(i)] yield very
+ /// large numbers of multi-triggers, most of which are useless. As it copies its
+ /// argument, this method updates various datastructures that allow it to
+ /// efficiently track ownership relations between formulae and bound variables,
+ /// and sets the IsRedundant flag of the returned set, allowing the caller to
+ /// discard that set of terms, and the ones that would have been built on top of
+ /// it, thus ensuring that the only sets of terms produced in the end are sets
+ /// of terms in which each element contributes (owns) at least one variable.
+ ///
+ /// Note that this is trickier than just checking every term for new variables;
+ /// indeed, a new term that does bring new variables in can make an existing
+ /// term redundant (see redundancy-detection-does-its-job-properly.dfy).
+ /// </summary>
+ internal SetOfTerms CopyWithAdd(TriggerTerm term, ISet<BoundVar> relevantVariables) {
+ var copy = new SetOfTerms();
+ copy.Terms = new List<TriggerTerm>(Terms);
+ copy.variables = new HashSet<BoundVar>(variables);
+ copy.termOwningAUniqueVar = new Dictionary<BoundVar, TriggerTerm>(termOwningAUniqueVar);
+ copy.uniqueVarsOwnedByATerm = new Dictionary<TriggerTerm, ISet<BoundVar>>(uniqueVarsOwnedByATerm);
+
+ copy.Terms.Add(term);
+
+ var varsInNewTerm = new HashSet<BoundVar>(term.BoundVars);
+ varsInNewTerm.IntersectWith(relevantVariables);
+
+ var ownedByNewTerm = new HashSet<BoundVar>();
+
+ // Check #0: does this term bring anything new?
+ copy.IsRedundant = IsRedundant || varsInNewTerm.All(bv => copy.variables.Contains(bv));
+ copy.variables.UnionWith(varsInNewTerm);
+
+ // Check #1: does this term claiming ownership of all its variables cause another term to become useless?
+ foreach (var v in varsInNewTerm) {
+ TriggerTerm originalOwner;
+ if (copy.termOwningAUniqueVar.TryGetValue(v, out originalOwner)) {
+ var alsoOwnedByOriginalOwner = copy.uniqueVarsOwnedByATerm[originalOwner];
+ alsoOwnedByOriginalOwner.Remove(v);
+ if (!alsoOwnedByOriginalOwner.Any()) {
+ copy.IsRedundant = true;
+ }
+ } else {
+ ownedByNewTerm.Add(v);
+ copy.termOwningAUniqueVar[v] = term;
+ }
+ }
+
+ // Actually claim ownership
+ copy.uniqueVarsOwnedByATerm[term] = ownedByNewTerm;
+
+ return copy;
+ }
+ }
+
+ internal static IEnumerable<SetOfTerms> AllSubsets(IList<TriggerTerm> source, Func<SetOfTerms, TriggerTerm, bool> predicate, int offset, ISet<BoundVar> relevantVariables) {
if (offset >= source.Count) {
- yield return new List<T>();
+ yield return SetOfTerms.Empty();
yield break;
}
- foreach (var subset in AllSubsets<T>(source, predicate, offset + 1)) {
- if (predicate(subset, source[offset])) {
- yield return CopyAndAdd(subset, source[offset]);
+ foreach (var subset in AllSubsets(source, predicate, offset + 1, relevantVariables)) {
+ var newSet = subset.CopyWithAdd(source[offset], relevantVariables);
+ if (!newSet.IsRedundant && predicate(subset, source[offset])) { // Fixme remove the predicate?
+ yield return newSet;
}
- yield return new List<T>(subset);
+ yield return subset;
}
}
- internal static IEnumerable<List<T>> AllNonEmptySubsets<T>(IEnumerable<T> source, Func<List<T>, T, bool> predicate) {
- List<T> all = new List<T>(source);
- foreach (var subset in AllSubsets(all, predicate, 0)) {
+ internal static IEnumerable<SetOfTerms> AllNonEmptySubsets(IList<TriggerTerm> source, Func<SetOfTerms, TriggerTerm, bool> predicate, IEnumerable<BoundVar> relevantVariables) {
+ foreach (var subset in AllSubsets(source, predicate, 0, new HashSet<BoundVar>(relevantVariables))) {
if (subset.Count > 0) {
yield return subset;
}
}
}
-
+
internal static List<T> MergeAlterFirst<T>(List<T> a, List<T> b) {
Contract.Requires(a != null);
Contract.Requires(b != null);
diff --git a/Source/Dafny/Triggers/TriggersCollector.cs b/Source/Dafny/Triggers/TriggersCollector.cs index 69c47d90..d78bcb9e 100644 --- a/Source/Dafny/Triggers/TriggersCollector.cs +++ b/Source/Dafny/Triggers/TriggersCollector.cs @@ -11,6 +11,11 @@ namespace Microsoft.Dafny.Triggers { internal Expression Expr { get; set; }
internal Expression OriginalExpr { get; set; }
internal ISet<IVariable> Variables { get; set; }
+ internal IEnumerable<BoundVar> BoundVars {
+ get {
+ return Variables.Select(v => v as BoundVar).Where(v => v != null);
+ }
+ }
public override string ToString() {
return Printer.ExprToString(Expr);
diff --git a/Test/triggers/function-applications-are-triggers.dfy.expect b/Test/triggers/function-applications-are-triggers.dfy.expect index 7922e88d..501cfa51 100644 --- a/Test/triggers/function-applications-are-triggers.dfy.expect +++ b/Test/triggers/function-applications-are-triggers.dfy.expect @@ -8,6 +8,6 @@ function-applications-are-triggers.dfy(10,9): Info: For expression {P(f) ==> f(1 function-applications-are-triggers.dfy(11,9): Info: Selected triggers:
{f(10)}, {f.requires(10)}
function-applications-are-triggers.dfy(12,5): Info: Selected triggers:
- {g(x), f(x)}, {g(x), f.requires(x)}, {g(x)}, {f(x)}, {g.requires(x), f.requires(x)}, {g.requires(x)}, {f.requires(x)}
+ {g(x)}, {f(x)}, {g.requires(x)}, {f.requires(x)}
Dafny program verifier finished with 2 verified, 0 errors
diff --git a/Test/triggers/redundancy-detection-is-bidirectional.dfy b/Test/triggers/redundancy-detection-is-bidirectional.dfy new file mode 100644 index 00000000..df1d78c3 --- /dev/null +++ b/Test/triggers/redundancy-detection-is-bidirectional.dfy @@ -0,0 +1,29 @@ +// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 /printTooltips "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+// This tests checks for tricky cases of redundancy suppression when building
+// triggers.
+
+predicate P(x: int, y: int)
+predicate Q(x: int)
+predicate R(x: int)
+
+method M() {
+ // For this term, it is enough to order the terms by number of variables
+ assert forall x, y :: true || P(x, y) || Q(y) || R(x);
+ assert forall x, y :: true || Q(y) || P(x, y) || R(x);
+ assert forall x, y :: true || Q(y) || R(x) || P(x, y);
+}
+
+predicate PP(x: int, y: int, z: int)
+predicate QQ(x: int, y: int)
+predicate RR(x: int, y: int)
+predicate SS(x: int, y: int)
+
+method MM() {
+ // Not for this one, though
+ assert forall x, y, z, u, v, w :: true || PP(x, y, z) || QQ(x, u) || RR(y, v) || SS(z, w);
+ assert forall x, y, z, u, v, w :: true || QQ(x, u) || PP(x, y, z) || RR(y, v) || SS(z, w);
+ assert forall x, y, z, u, v, w :: true || QQ(x, u) || RR(y, v) || PP(x, y, z) || SS(z, w);
+ assert forall x, y, z, u, v, w :: true || QQ(x, u) || RR(y, v) || SS(z, w) || PP(x, y, z);
+}
diff --git a/Test/triggers/redundancy-detection-is-bidirectional.dfy.expect b/Test/triggers/redundancy-detection-is-bidirectional.dfy.expect new file mode 100644 index 00000000..78c9e7ca --- /dev/null +++ b/Test/triggers/redundancy-detection-is-bidirectional.dfy.expect @@ -0,0 +1,12 @@ +redundancy-detection-is-bidirectional.dfy(13,9): Info: Selected triggers:
+ {R(x), Q(y)}, {P(x, y)}
+redundancy-detection-is-bidirectional.dfy(14,9): Info: Selected triggers:
+ {R(x), Q(y)}, {P(x, y)}
+redundancy-detection-is-bidirectional.dfy(15,9): Info: Selected triggers:
+ {P(x, y)}, {R(x), Q(y)}
+redundancy-detection-is-bidirectional.dfy(25,9): Info: Selected triggers: {SS(z, w), RR(y, v), QQ(x, u)}
+redundancy-detection-is-bidirectional.dfy(26,9): Info: Selected triggers: {SS(z, w), RR(y, v), QQ(x, u)}
+redundancy-detection-is-bidirectional.dfy(27,9): Info: Selected triggers: {SS(z, w), RR(y, v), QQ(x, u)}
+redundancy-detection-is-bidirectional.dfy(28,9): Info: Selected triggers: {SS(z, w), RR(y, v), QQ(x, u)}
+
+Dafny program verifier finished with 11 verified, 0 errors
|