From 743be23f3961e02f1d556860f9fb0e17b98ab54d Mon Sep 17 00:00:00 2001 From: Checkmate50 Date: Tue, 7 Jun 2016 01:01:49 -0600 Subject: fixed some merging issues --- Source/Core/AbsyExpr.cs | 104 +++++++++++++++++++++++++++-- Source/Provers/SMTLib/TypeDeclCollector.cs | 2 +- 2 files changed, 100 insertions(+), 6 deletions(-) diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs index 7ffd5f7f..b980a22b 100644 --- a/Source/Core/AbsyExpr.cs +++ b/Source/Core/AbsyExpr.cs @@ -313,6 +313,13 @@ namespace Microsoft.Boogie { Contract.Ensures(Contract.Result() != null); return Binary(BinaryOperator.Opcode.RealDiv, e1, e2); } + public static NAryExpr FloatDiv(Expr e1, Expr e2) + { + Contract.Requires(e2 != null); + Contract.Requires(e1 != null); + Contract.Ensures(Contract.Result() != null); + return Binary(BinaryOperator.Opcode.FloatDiv, e1, e2); + } public static NAryExpr Pow(Expr e1, Expr e2) { Contract.Requires(e2 != null); Contract.Requires(e1 != null); @@ -356,6 +363,11 @@ namespace Microsoft.Boogie { Contract.Ensures(Contract.Result() != null); return new LiteralExpr(Token.NoToken, value); } + public static LiteralExpr Literal(BigFloat value) + { + Contract.Ensures(Contract.Result() != null); + return new LiteralExpr(Token.NoToken, value); + } private static LiteralExpr/*!*/ true_ = Literal(true); public static LiteralExpr/*!*/ True { @@ -514,7 +526,7 @@ namespace Microsoft.Boogie { } public class LiteralExpr : Expr { - public readonly object/*!*/ Val; // false, true, a BigNum, a BigDec, or a BvConst + public readonly object/*!*/ Val; // false, true, a BigNum, a BigDec, a BigFloat, or a BvConst [ContractInvariantMethod] void ObjectInvariant() { Contract.Invariant(Val != null); @@ -562,6 +574,21 @@ namespace Microsoft.Boogie { CachedHashCode = ComputeHashCode(); } + /// + /// Creates a literal expression for the floating point value "v". + /// + /// + /// + public LiteralExpr(IToken/*!*/ tok, BigFloat v, bool immutable = false) + : base(tok, immutable) + { + Contract.Requires(tok != null); + Val = v; + Type = Type.GetFloatType(v.ExponentSize, v.SignificandSize); + if (immutable) + CachedHashCode = ComputeHashCode(); + } + /// /// Creates a literal expression for the bitvector value "v". /// @@ -633,6 +660,9 @@ namespace Microsoft.Boogie { return Type.Int; } else if (Val is BigDec) { return Type.Real; + } else if (Val is BigFloat) { + BigFloat temp = (BigFloat)Val; + return Type.GetFloatType(temp.ExponentSize, temp.SignificandSize); } else if (Val is BvConst) { return Type.GetBvType(((BvConst)Val).Bits); } else { @@ -681,6 +711,14 @@ namespace Microsoft.Boogie { } } + public bool isBigFloat + { + get + { + return Val is BigFloat; + } + } + public BigDec asBigDec { get { Contract.Assert(isBigDec); @@ -688,6 +726,13 @@ namespace Microsoft.Boogie { } } + public BigFloat asBigFloat { + get { + Contract.Assert(isBigFloat); + return (BigFloat)cce.NonNull(Val); + } + } + public bool isBool { get { return Val is bool; @@ -1355,6 +1400,9 @@ namespace Microsoft.Boogie { if (arg0type.Unify(Type.Real)) { return Type.Real; } + //if (arg0type.Unify(Type.Float)) { + //return Type.Float; + //} goto BAD_TYPE; case Opcode.Not: if (arg0type.Unify(Type.Bool)) { @@ -1399,6 +1447,9 @@ namespace Microsoft.Boogie { if (argument is BigDec) { return -((BigDec)argument); } + if (argument is BigFloat) { + return -((BigFloat)argument); + } break; case Opcode.Not: if (argument is bool) { @@ -1431,6 +1482,7 @@ namespace Microsoft.Boogie { Div, Mod, RealDiv, + FloatDiv, Pow, Eq, Neq, @@ -1671,6 +1723,12 @@ namespace Microsoft.Boogie { if (arg0type.Unify(Type.Real) && arg1type.Unify(Type.Real)) { return Type.Real; } + if (arg0type.IsFloat && arg0type.Unify(arg1type)) { + return Type.GetFloatType(arg0.Type.FloatExponent, arg0.Type.FloatMantissa); + } + if (arg1type.IsFloat && arg1type.Unify(arg0type)) { + return Type.GetFloatType(arg1.Type.FloatExponent, arg1.Type.FloatMantissa); + } goto BAD_TYPE; case Opcode.Div: case Opcode.Mod: @@ -1683,6 +1741,12 @@ namespace Microsoft.Boogie { (arg1type.Unify(Type.Int) || arg1type.Unify(Type.Real))) { return Type.Real; } + if (arg0type.IsFloat && arg0type.Unify(arg1type)) { + return Type.GetFloatType(arg0.Type.FloatExponent, arg0.Type.FloatMantissa); + } + if (arg1type.IsFloat && arg1type.Unify(arg0type)) { + return Type.GetFloatType(arg1.Type.FloatExponent, arg1.Type.FloatMantissa); + } goto BAD_TYPE; case Opcode.Pow: if (arg0type.Unify(Type.Real) && arg1type.Unify(Type.Real)) { @@ -1715,6 +1779,9 @@ namespace Microsoft.Boogie { if (arg0type.Unify(Type.Real) && arg1type.Unify(Type.Real)) { return Type.Bool; } + if ((arg0type.IsFloat && arg0type.Unify(arg1type)) || (arg1type.IsFloat && arg1type.Unify(arg0type))) { + return Type.Bool; + } goto BAD_TYPE; case Opcode.And: case Opcode.Or: @@ -1825,6 +1892,9 @@ namespace Microsoft.Boogie { if (e1 is BigDec && e2 is BigDec) { return ((BigDec)e1) + ((BigDec)e2); } + if (e1 is BigFloat && e2 is BigFloat) { + return ((BigFloat)e1) + ((BigFloat)e2); + } break; case Opcode.Sub: if (e1 is BigNum && e2 is BigNum) { @@ -1833,6 +1903,9 @@ namespace Microsoft.Boogie { if (e1 is BigDec && e2 is BigDec) { return ((BigDec)e1) - ((BigDec)e2); } + if (e1 is BigFloat && e2 is BigFloat) { + return ((BigFloat)e1) - ((BigFloat)e2); + } break; case Opcode.Mul: if (e1 is BigNum && e2 is BigNum) { @@ -1841,6 +1914,9 @@ namespace Microsoft.Boogie { if (e1 is BigDec && e2 is BigDec) { return ((BigDec)e1) * ((BigDec)e2); } + if (e1 is BigFloat && e2 is BigFloat) { + return ((BigFloat)e1) * ((BigFloat)e2); + } break; case Opcode.Div: if (e1 is BigNum && e2 is BigNum) { @@ -1855,6 +1931,9 @@ namespace Microsoft.Boogie { case Opcode.RealDiv: // TODO: add partial evaluation fro real division break; + case Opcode.FloatDiv: + //TODO: add float division + break; case Opcode.Pow: // TODO: add partial evaluation fro real exponentiation break; @@ -1865,6 +1944,9 @@ namespace Microsoft.Boogie { if (e1 is BigDec && e2 is BigDec) { return ((BigDec)e1) < ((BigDec)e2); } + if (e1 is BigFloat && e2 is BigFloat) { + return ((BigFloat)e1) < ((BigFloat)e2); + } break; case Opcode.Le: if (e1 is BigNum && e2 is BigNum) { @@ -1873,6 +1955,9 @@ namespace Microsoft.Boogie { if (e1 is BigDec && e2 is BigDec) { return ((BigDec)e1) <= ((BigDec)e2); } + if (e1 is BigFloat && e2 is BigFloat) { + return ((BigFloat)e1) <= ((BigFloat)e2); + } break; case Opcode.Gt: if (e1 is BigNum && e2 is BigNum) { @@ -1881,6 +1966,9 @@ namespace Microsoft.Boogie { if (e1 is BigDec && e2 is BigDec) { return ((BigDec)e1) > ((BigDec)e2); } + if (e1 is BigFloat && e2 is BigFloat) { + return ((BigFloat)e1) > ((BigFloat)e2); + } break; case Opcode.Ge: if (e1 is BigNum && e2 is BigNum) { @@ -1889,6 +1977,9 @@ namespace Microsoft.Boogie { if (e1 is BigDec && e2 is BigDec) { return ((BigDec)e1) >= ((BigDec)e2); } + if (e1 is BigFloat && e2 is BigFloat) { + return ((BigFloat)e1) >= ((BigFloat)e2); + } break; case Opcode.And: @@ -1990,7 +2081,7 @@ namespace Microsoft.Boogie { } else { - this.name.Emit(stream, 0xF0, false); + this.name.Emit(stream, 0xF0, false); } if (stream.UseForComputingChecksums) { @@ -2177,7 +2268,8 @@ namespace Microsoft.Boogie { public class ArithmeticCoercion : IAppliable { public enum CoercionType { ToInt, - ToReal + ToReal, + ToFloat } private IToken/*!*/ tok; @@ -2185,6 +2277,7 @@ namespace Microsoft.Boogie { private readonly string name; private readonly Type type; private readonly Type argType; + private readonly Type argType2; private readonly int hashCode; public ArithmeticCoercion(IToken tok, CoercionType coercion) { @@ -2264,8 +2357,9 @@ namespace Microsoft.Boogie { tpInstantiation = SimpleTypeParamInstantiation.EMPTY; - if (!cce.NonNull(cce.NonNull(args[0]).Type).Unify(argType)) { - tc.Error(this.tok, "argument type {0} does not match expected type {1}", cce.NonNull(args[0]).Type, this.argType); + if (!(cce.NonNull(cce.NonNull(args[0]).Type).Unify(argType) || cce.NonNull(cce.NonNull(args[0]).Type).Unify(argType2))) + { + tc.Error(this.tok, "argument type {0} does not match expected type {1} or type {2}", cce.NonNull(args[0]).Type, this.argType, this.argType2); } return this.type; diff --git a/Source/Provers/SMTLib/TypeDeclCollector.cs b/Source/Provers/SMTLib/TypeDeclCollector.cs index eaed83e9..1d63fa5d 100644 --- a/Source/Provers/SMTLib/TypeDeclCollector.cs +++ b/Source/Provers/SMTLib/TypeDeclCollector.cs @@ -311,7 +311,7 @@ void ObjectInvariant() return; } - if (type.IsBool || type.IsInt || type.IsReal || type.IsBv) + if (type.IsBool || type.IsInt || type.IsReal || type.IsBv || type.IsFloat) return; CtorType ctorType = type as CtorType; -- cgit v1.2.3