fixed some merging issues

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<NAryExpr>() != 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<NAryExpr>() != 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<LiteralExpr>() != null);
       return new LiteralExpr(Token.NoToken, value);
     }
+    public static LiteralExpr Literal(BigFloat value)
+    {
+      Contract.Ensures(Contract.Result<LiteralExpr>() != 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);
@@ -563,6 +575,21 @@ namespace Microsoft.Boogie {
     }
 
     /// <summary>
+    /// Creates a literal expression for the floating point value "v".
+    /// </summary>
+    /// <param name="tok"></param>
+    /// <param name="v"></param>
+    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();
+    }
+
+    /// <summary>
     /// Creates a literal expression for the bitvector value "v".
     /// </summary>
     public LiteralExpr(IToken/*!*/ tok, BigNum v, int b, bool immutable=false)
@@ -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;