diff options
| author |  boehmes <unknown> | 2012-09-27 17:13:45 +0200 |
|---|---|---|
| committer | boehmes <unknown> | 2012-09-27 17:13:45 +0200 |
| commit | 43b80b13bd24bb789849aac3385df6ac4a8233be (patch) | |
| tree | 499b3dffd74fd84fdf8aedffacbca424d25680b2 /Test/test0 | |
| parent | dfb77ee06c82cf8b9c465f3a2acbc5ceb035c6e5 (diff) | |
Boogie: added type 'real' with overloaded arithmetic operations plus real division '/' and (uninterpreted) real exponentiation '**', real literals and coercion functions 'int' and 'real';
Integer operations 'div' and 'mod' are now mapped to corresponding SMT-LIB operations instead of treating them uninterpreted;
Made unary minus valid Boogie syntax again (the expression '- e' used to be rewritten by the parser to '0 - e', now this is done when generating VCs);
Extended the BigDec class with additional functionality;
Added test cases for SMT-LIB prover backend (the Z3 API interface has been adapted accordingly, but is untested)
Diffstat (limited to 'Test/test0')
| -rw-r--r-- | Test/test0/Answer | 36 | ||||
| -rw-r--r-- | Test/test0/ModifiedBag.bpl | 2 | ||||
| -rw-r--r-- | Test/test0/PrettyPrint.bpl | 22 | ||||
| -rw-r--r-- | Test/test0/Prog0.bpl | 2 |
4 files changed, 60 insertions, 2 deletions
diff --git a/Test/test0/Answer b/Test/test0/Answer index d57e7647..0eda9e2e 100644 --- a/Test/test0/Answer +++ b/Test/test0/Answer @@ -34,6 +34,12 @@ const y: int; const z: int;
+const r: real;
+
+const s: real;
+
+const t: real;
+
const P: bool;
const Q: bool;
@@ -56,6 +62,36 @@ axiom x + y mod z == y mod z + x; axiom (x + y) mod z == x mod z + y mod z;
+axiom x / y / z == x / (y / z);
+
+axiom x / y / (z / x) == x / y / z;
+
+axiom x / s / z == x / (s / z);
+
+axiom x / s / (z / x) == x / s / z;
+
+axiom r / s / t == r / (s / t);
+
+axiom r / s / (t / r) == r / s / t;
+
+axiom r * s / t == r * s / t;
+
+axiom r / s * t == r / s * t;
+
+axiom (r * s) ** t == r ** t * s ** t;
+
+axiom r ** (s + t) == r ** s * r ** t;
+
+axiom int(real(x)) == x;
+
+axiom r >= 0e0 ==> real(int(r)) <= r;
+
+axiom int(0e0 - 2e-2) == 0;
+
+axiom int(0e0 - 35e0) == -35;
+
+axiom int(27e-1) == 2;
+
axiom x - y - z == x - (y - z);
axiom x - y - (z - x) == x - y - z;
diff --git a/Test/test0/ModifiedBag.bpl b/Test/test0/ModifiedBag.bpl index cb69aa5f..5fffc20a 100644 --- a/Test/test0/ModifiedBag.bpl +++ b/Test/test0/ModifiedBag.bpl @@ -1,5 +1,5 @@ // ----------- BEGIN PRELUDE
-type real;
+
type elements;
diff --git a/Test/test0/PrettyPrint.bpl b/Test/test0/PrettyPrint.bpl index 955faad8..7e4a9ce7 100644 --- a/Test/test0/PrettyPrint.bpl +++ b/Test/test0/PrettyPrint.bpl @@ -1,6 +1,9 @@ const x: int;
const y: int;
const z: int;
+const r: real;
+const s: real;
+const t: real;
const P: bool;
const Q: bool;
const R: bool;
@@ -17,6 +20,25 @@ axiom (x div y) div (z div x) == (x div y) div z; axiom x + y mod z == ((y mod z) + x);
axiom (x + y) mod z == (x mod z) + (y mod z);
+axiom x / y / z == (x / (y / z));
+axiom (x / y) / (z / x) == (x / y) / z;
+axiom x / s / z == (x / (s / z));
+axiom (x / s) / (z / x) == (x / s) / z;
+axiom r / s / t == (r / (s / t));
+axiom (r / s) / (t / r) == (r / s) / t;
+
+axiom ((r * s) / t) == r * s / t;
+axiom ((r / s) * t) == (r / s) * t;
+
+axiom (r * s) ** t == (r ** t) * (s ** t);
+axiom r ** (s + t) == r ** s * r ** t;
+
+axiom int(real(x)) == x;
+axiom r >= 0.0 ==> real(int(r)) <= r;
+axiom int(0e-3 - 0.02) == 0;
+axiom int(0e2 - 3.5e1) == -35;
+axiom int(27e-1) == 2;
+
axiom x - y - z == (x - (y - z));
axiom (x - y) - (z - x) == (x - y) - z;
diff --git a/Test/test0/Prog0.bpl b/Test/test0/Prog0.bpl index ac87476f..79a4d2ab 100644 --- a/Test/test0/Prog0.bpl +++ b/Test/test0/Prog0.bpl @@ -1,5 +1,5 @@ // BoogiePL Examples
-type real;
+
type elements;
var x:int; var y:real; var z:ref; // Variables
|