From 43b80b13bd24bb789849aac3385df6ac4a8233be Mon Sep 17 00:00:00 2001 From: boehmes Date: Thu, 27 Sep 2012 17:13:45 +0200 Subject: 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) --- Source/VCExpr/TypeErasure.cs | 48 ++++++++++++++++++++++++++++++++++---------- 1 file changed, 37 insertions(+), 11 deletions(-) (limited to 'Source/VCExpr/TypeErasure.cs') diff --git a/Source/VCExpr/TypeErasure.cs b/Source/VCExpr/TypeErasure.cs index fb91d326..9d366c9f 100644 --- a/Source/VCExpr/TypeErasure.cs +++ b/Source/VCExpr/TypeErasure.cs @@ -524,6 +524,7 @@ namespace Microsoft.Boogie.TypeErasure { public virtual void Setup() { GetBasicTypeRepr(Type.Int); + GetBasicTypeRepr(Type.Real); GetBasicTypeRepr(Type.Bool); } @@ -625,6 +626,7 @@ namespace Microsoft.Boogie.TypeErasure { base.Setup(); GetTypeCasts(Type.Int); + GetTypeCasts(Type.Real); GetTypeCasts(Type.Bool); } @@ -730,7 +732,7 @@ namespace Microsoft.Boogie.TypeErasure { //////////////////////////////////////////////////////////////////////////// // the only types that we allow in "untyped" expressions are U, - // Type.Int, and Type.Bool + // Type.Int, Type.Real, and Type.Bool public override Type TypeAfterErasure(Type type) { //Contract.Requires(type != null); @@ -746,7 +748,7 @@ namespace Microsoft.Boogie.TypeErasure { [Pure] public override bool UnchangedType(Type type) { //Contract.Requires(type != null); - return type.IsInt || type.IsBool || type.IsBv || (type.IsMap && CommandLineOptions.Clo.MonomorphicArrays); + return type.IsInt || type.IsReal || type.IsBool || type.IsBv || (type.IsMap && CommandLineOptions.Clo.MonomorphicArrays); } public VCExpr Cast(VCExpr expr, Type toType) { @@ -1143,7 +1145,7 @@ namespace Microsoft.Boogie.TypeErasure { Contract.Requires(bindings != null); Contract.Requires(node != null); Contract.Ensures(Contract.Result() != null); - Contract.Assume(node.Type == Type.Bool || node.Type == Type.Int); + Contract.Assume(node.Type == Type.Bool || node.Type == Type.Int || node.Type == Type.Real); return node; } @@ -1360,7 +1362,7 @@ namespace Microsoft.Boogie.TypeErasure { } // Cast the arguments of the node to their old type if necessary and possible; otherwise use - // their new type (int, bool, or U) + // their new type (int, real, bool, or U) private VCExpr CastArgumentsToOldType(VCExprNAry node, VariableBindings bindings, int newPolarity) { Contract.Requires(bindings != null); Contract.Requires(node != null); @@ -1448,19 +1450,19 @@ namespace Microsoft.Boogie.TypeErasure { Contract.Requires((bindings != null)); Contract.Requires((node != null)); Contract.Ensures(Contract.Result() != null); - return CastArguments(node, Type.Int, bindings, 0); + return CastArguments(node, node.Type, bindings, 0); } public override VCExpr VisitSubOp(VCExprNAry node, VariableBindings bindings) { Contract.Requires((bindings != null)); Contract.Requires((node != null)); Contract.Ensures(Contract.Result() != null); - return CastArguments(node, Type.Int, bindings, 0); + return CastArguments(node, node.Type, bindings, 0); } public override VCExpr VisitMulOp(VCExprNAry node, VariableBindings bindings) { Contract.Requires((bindings != null)); Contract.Requires((node != null)); Contract.Ensures(Contract.Result() != null); - return CastArguments(node, Type.Int, bindings, 0); + return CastArguments(node, node.Type, bindings, 0); } public override VCExpr VisitDivOp(VCExprNAry node, VariableBindings bindings) { Contract.Requires((bindings != null)); @@ -1474,29 +1476,41 @@ namespace Microsoft.Boogie.TypeErasure { Contract.Ensures(Contract.Result() != null); return CastArguments(node, Type.Int, bindings, 0); } + public override VCExpr VisitRealDivOp(VCExprNAry node, VariableBindings bindings) { + Contract.Requires((bindings != null)); + Contract.Requires((node != null)); + Contract.Ensures(Contract.Result() != null); + return CastArguments(node, Type.Real, bindings, 0); + } + public override VCExpr VisitPowOp(VCExprNAry node, VariableBindings bindings) { + Contract.Requires((bindings != null)); + Contract.Requires((node != null)); + Contract.Ensures(Contract.Result() != null); + return CastArguments(node, Type.Real, bindings, 0); + } public override VCExpr VisitLtOp(VCExprNAry node, VariableBindings bindings) { Contract.Requires((bindings != null)); Contract.Requires((node != null)); Contract.Ensures(Contract.Result() != null); - return CastArguments(node, Type.Int, bindings, 0); + return CastArgumentsToOldType(node, bindings, 0); } public override VCExpr VisitLeOp(VCExprNAry node, VariableBindings bindings) { Contract.Requires((bindings != null)); Contract.Requires((node != null)); Contract.Ensures(Contract.Result() != null); - return CastArguments(node, Type.Int, bindings, 0); + return CastArgumentsToOldType(node, bindings, 0); } public override VCExpr VisitGtOp(VCExprNAry node, VariableBindings bindings) { Contract.Requires((bindings != null)); Contract.Requires((node != null)); Contract.Ensures(Contract.Result() != null); - return CastArguments(node, Type.Int, bindings, 0); + return CastArgumentsToOldType(node, bindings, 0); } public override VCExpr VisitGeOp(VCExprNAry node, VariableBindings bindings) { Contract.Requires((bindings != null)); Contract.Requires((node != null)); Contract.Ensures(Contract.Result() != null); - return CastArguments(node, Type.Int, bindings, 0); + return CastArgumentsToOldType(node, bindings, 0); } public override VCExpr VisitSubtypeOp(VCExprNAry node, VariableBindings bindings) { Contract.Requires((bindings != null)); @@ -1504,6 +1518,18 @@ namespace Microsoft.Boogie.TypeErasure { Contract.Ensures(Contract.Result() != null); return CastArguments(node, AxBuilder.U, bindings, 0); } + public override VCExpr VisitToIntOp(VCExprNAry node, VariableBindings bindings) { + Contract.Requires((bindings != null)); + Contract.Requires((node != null)); + Contract.Ensures(Contract.Result() != null); + return CastArgumentsToOldType(node, bindings, 0); + } + public override VCExpr VisitToRealOp(VCExprNAry node, VariableBindings bindings) { + Contract.Requires((bindings != null)); + Contract.Requires((node != null)); + Contract.Ensures(Contract.Result() != null); + return CastArgumentsToOldType(node, bindings, 0); + } public override VCExpr VisitBvOp(VCExprNAry node, VariableBindings bindings) { Contract.Requires((bindings != null)); Contract.Requires((node != null)); -- cgit v1.2.3