From f3d609f0f6ef889bb066cc31ee514bb9671f4799 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Tue, 10 Mar 2015 15:33:11 -0700 Subject: Beefed up collection axioms (in particular, for maps) to improve the chance of proving the existence check of let-such-that and assign-such-that --- Binaries/DafnyPrelude.bpl | 13 +++++++++++-- 1 file changed, 11 insertions(+), 2 deletions(-) (limited to 'Binaries') diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl index 0e91bf95..4972517b 100644 --- a/Binaries/DafnyPrelude.bpl +++ b/Binaries/DafnyPrelude.bpl @@ -686,7 +686,14 @@ axiom (forall s: Seq T :: { Seq#Length(s) } 0 <= Seq#Length(s)); function Seq#Empty(): Seq T; axiom (forall :: Seq#Length(Seq#Empty(): Seq T) == 0); -axiom (forall s: Seq T :: { Seq#Length(s) } Seq#Length(s) == 0 ==> s == Seq#Empty()); +axiom (forall s: Seq T :: { Seq#Length(s) } + (Seq#Length(s) == 0 ==> s == Seq#Empty()) +// The following would be a nice fact to include, because it would enable verifying the +// GenericPick.SeqPick* methods in Test/dafny0/SmallTests.dfy. However, it substantially +// slows down performance on some other tests, including running seemingly forever on +// some. +// && (Seq#Length(s) != 0 ==> (exists x: T :: Seq#Contains(s, x))) + ); // The empty sequence $Is any type axiom (forall t: Ty :: {$Is(Seq#Empty(): Seq T, t)} $Is(Seq#Empty(): Seq T, t)); @@ -887,7 +894,9 @@ function Map#Empty(): Map U V; axiom (forall u: U :: { Map#Domain(Map#Empty(): Map U V)[u] } !Map#Domain(Map#Empty(): Map U V)[u]); -axiom (forall m: Map U V :: { Map#Card(m) } Map#Card(m) == 0 <==> m == Map#Empty()); +axiom (forall m: Map U V :: { Map#Card(m) } + (Map#Card(m) == 0 <==> m == Map#Empty()) && + (Map#Card(m) != 0 ==> (exists x: U :: Map#Domain(m)[x]))); function Map#Glue([U] bool, [U]V, Ty): Map U V; axiom (forall a: [U] bool, b:[U]V, t:Ty :: -- cgit v1.2.3