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/test1/IntReal.bpl | |
| 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/test1/IntReal.bpl')
| -rw-r--r-- | Test/test1/IntReal.bpl | 48 |
1 files changed, 48 insertions, 0 deletions
diff --git a/Test/test1/IntReal.bpl b/Test/test1/IntReal.bpl new file mode 100644 index 00000000..fac41d57 --- /dev/null +++ b/Test/test1/IntReal.bpl @@ -0,0 +1,48 @@ +const i: int;
+const r: real;
+
+axiom i == 0;
+axiom i >= 0.0; // type errror
+axiom i <= 0.0e0; // type errror
+axiom i < 0.0e-0; // type errror
+axiom i > 0.0e20; // type errror
+
+axiom -i == r; // type errror
+axiom i + r == 0.0; // type errror
+axiom i - r == 0.0; // type errror
+axiom i * r == 0.0; // type errror
+axiom i div r == 0; // type errror
+axiom i mod r == 0; // type errror
+
+axiom i / i == 0; // type errror
+axiom i / i == 0.0;
+axiom i / r == 0.0;
+axiom r / i == 0.0;
+axiom r / r == 0.0;
+
+axiom i ** r == 0.0; // type errror
+axiom r ** r == 0.0;
+
+axiom real(i) == 0.0;
+axiom real(i) == i; // type errror
+axiom int(r) == 0;
+axiom int(r) == r; // type errror
+axiom int(real(i)) == i;
+axiom real(int(r)) == r;
+axiom int(int(r)) == i; // type errror
+axiom real(real(i)) == r; // type errror
+
+axiom i == 0;
+axiom real(i) >= 0.0;
+axiom real(i) <= 0.0e0;
+axiom r < 0.0e-0;
+axiom r > 0.0e20;
+
+axiom -r == real(i);
+axiom real(i) + r == 0.0;
+axiom r - real(0) == 0.0;
+axiom r * r == 0.0;
+axiom r div 0 == 0; // type errror
+axiom r mod 0 == 0; // type errror
+
+axiom r ** r == 0.0;
|