summaryrefslogtreecommitdiff
path: root/Binaries
diff options
context:
space:
mode:
authorGravatar Unknown <namin@idea>2013-07-04 00:54:04 -0700
committerGravatar Unknown <namin@idea>2013-07-04 00:54:04 -0700
commitd2d39ff37467249c3dcb7b9318b71955d62330bf (patch)
treec479f227e4d415645bee7aae0bdfdd90d5c93769 /Binaries
parentd702c16829fd403ba9533263df7b140fabd9ec9f (diff)
Computations!
Generates 'computing' axioms for both all formals and just decreasing formals. Supported are literal datatypes, booleans and numbers. The axioms are given a weight of 10, which seems enough for Z3 to give up when it is sane to do so.
Diffstat (limited to 'Binaries')
-rw-r--r--Binaries/DafnyPrelude.bpl6
1 files changed, 6 insertions, 0 deletions
diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl
index 5d0b647f..349da0fd 100644
--- a/Binaries/DafnyPrelude.bpl
+++ b/Binaries/DafnyPrelude.bpl
@@ -8,6 +8,12 @@ const $$Language$Dafny: bool; // To be recognizable to the ModelViewer as
axiom $$Language$Dafny; // coming from a Dafny program.
// ---------------------------------------------------------------
+// -- Literals ---------------------------------------------------
+// ---------------------------------------------------------------
+function {:identity} Lit<T>(x: T): T { x }
+axiom (forall<T> x: T :: { $Box(Lit(x)) } $Box(Lit(x)) == Lit($Box(x)) );
+
+// ---------------------------------------------------------------
// -- References -------------------------------------------------
// ---------------------------------------------------------------