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)

1 files changed, 17 insertions, 0 deletions

diff --git a/Test/test21/Real.bpl b/Test/test21/Real.bpl
new file mode 100644
index 00000000..3dcf3ea3
--- /dev/null
+++ b/Test/test21/Real.bpl
@@ -0,0 +1,17 @@
+axiom (forall r: real :: r == 0.0 || r / r == 1.0);

+

+procedure P(a: real, b: real) returns () {

+  assume a >= b && a != 0.0 && a >= 1.3579;

+

+  assert 2e0 * (a + 3.0) - 0.5 >= b;

+  assert 2e0 * (a + 3.0) - 0.5 > b;

+  assert b <= 2e0 * (a + 3.0) - 0.5;

+  assert b < 2e0 * (a + 3.0) - 0.5;

+

+  assert 1/2 <= 0.65;

+  assert a > 100e-2 ==> 1 / a <= a;

+  assert a / 2 != a || a == 0.00;

+  assert a != 0.0 ==> a / a == 1.0;

+

+  assert int(a) >= 0 ==> real(3) * a > a;

+}
\ No newline at end of file