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, 3 insertions, 3 deletions

diff --git a/Source/Provers/SMTLib/SMTLibNamer.cs b/Source/Provers/SMTLib/SMTLibNamer.cs
index 5629c0d6..101b07a0 100644
--- a/Source/Provers/SMTLib/SMTLibNamer.cs
+++ b/Source/Provers/SMTLib/SMTLibNamer.cs
@@ -22,8 +22,8 @@ namespace Microsoft.Boogie.SMTLib
       // Core theory:

       "and", "or", "not", "iff", "true", "false", "xor", "distinct", "ite", "=", "Bool",

       "=>", // implies (sic!)

-      // Integers

-      "Int", "*", "/", "-", "+", "<", "<=", ">", ">=",

+      // Integers and reals

+      "Int", "Real", "*", "/", "-", "+", "<", "<=", ">", ">=", "div", "mod",

       // Bitvectors

       "extract", "concat", 

       "bvnot", "bvneg", "bvand", "bvor", "bvadd", "bvmul", "bvudiv", "bvurem", "bvshl", "bvlshr", "bvult",

@@ -48,7 +48,7 @@ namespace Microsoft.Boogie.SMTLib
       "lblneg", "lblpos", "lbl-lit",

       "if", "&&", "||", "equals", "equiv", "bool",

       // Boogie-defined

-      "int_mod", "int_div", "UOrdering2", "UOrdering3", 

+      "real_pow", "UOrdering2", "UOrdering3", 

     };

 

     static HashSet<string> reservedSmtWords;