diff options
author | 2012-09-27 17:13:45 +0200 | |
---|---|---|
committer | 2012-09-27 17:13:45 +0200 | |
commit | 43b80b13bd24bb789849aac3385df6ac4a8233be (patch) | |
tree | 499b3dffd74fd84fdf8aedffacbca424d25680b2 /Source/Core/Util.cs | |
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 'Source/Core/Util.cs')
-rw-r--r-- | Source/Core/Util.cs | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/Source/Core/Util.cs b/Source/Core/Util.cs index f8b8b82b..9a7fec0c 100644 --- a/Source/Core/Util.cs +++ b/Source/Core/Util.cs @@ -486,6 +486,12 @@ namespace Microsoft.Boogie { case Microsoft.Boogie.BinaryOperator.Opcode.Or:
op = " || ";
break;
+ case Microsoft.Boogie.BinaryOperator.Opcode.Pow:
+ op = " ** ";
+ break;
+ case Microsoft.Boogie.BinaryOperator.Opcode.RealDiv:
+ op = " / ";
+ break;
case Microsoft.Boogie.BinaryOperator.Opcode.Sub:
op = " - ";
break;
|