resolving conflicts

5 files changed, 13 insertions, 108 deletions

diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs
index b980a22b..7ffd5f7f 100644
--- a/Source/Core/AbsyExpr.cs
+++ b/Source/Core/AbsyExpr.cs
@@ -313,13 +313,6 @@ 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);
@@ -363,11 +356,6 @@ 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 {
@@ -526,7 +514,7 @@ namespace Microsoft.Boogie {
   }
 
   public class LiteralExpr : Expr {
-    public readonly object/*!*/ Val;  // false, true, a BigNum, a BigDec, a BigFloat, or a BvConst
+    public readonly object/*!*/ Val;  // false, true, a BigNum, a BigDec, or a BvConst
     [ContractInvariantMethod]
     void ObjectInvariant() {
       Contract.Invariant(Val != null);
@@ -575,21 +563,6 @@ 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)
@@ -660,9 +633,6 @@ 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 {
@@ -711,14 +681,6 @@ namespace Microsoft.Boogie {
       }
     }
 
-    public bool isBigFloat
-    {
-      get
-      {
-        return Val is BigFloat;
-      }
-    }
-
     public BigDec asBigDec {
       get {
         Contract.Assert(isBigDec);
@@ -726,13 +688,6 @@ namespace Microsoft.Boogie {
       }
     }
 
-    public BigFloat asBigFloat {
-      get {
-        Contract.Assert(isBigFloat);
-        return (BigFloat)cce.NonNull(Val);
-      }
-    }
-
     public bool isBool {
       get {
         return Val is bool;
@@ -1400,9 +1355,6 @@ 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)) {
@@ -1447,9 +1399,6 @@ 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) {
@@ -1482,7 +1431,6 @@ namespace Microsoft.Boogie {
       Div,
       Mod,
       RealDiv,
-      FloatDiv,
       Pow,
       Eq,
       Neq,
@@ -1723,12 +1671,6 @@ 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:
@@ -1741,12 +1683,6 @@ 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)) {
@@ -1779,9 +1715,6 @@ 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:
@@ -1892,9 +1825,6 @@ 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) {
@@ -1903,9 +1833,6 @@ 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) {
@@ -1914,9 +1841,6 @@ 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) {
@@ -1931,9 +1855,6 @@ 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;
@@ -1944,9 +1865,6 @@ 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) {
@@ -1955,9 +1873,6 @@ 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) {
@@ -1966,9 +1881,6 @@ 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) {
@@ -1977,9 +1889,6 @@ 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:
@@ -2081,7 +1990,7 @@ namespace Microsoft.Boogie {
       }
       else
       {
-      this.name.Emit(stream, 0xF0, false);
+        this.name.Emit(stream, 0xF0, false);
       }
       if (stream.UseForComputingChecksums)
       {
@@ -2268,8 +2177,7 @@ namespace Microsoft.Boogie {
   public class ArithmeticCoercion : IAppliable {
     public enum CoercionType {
       ToInt,
-      ToReal,
-      ToFloat
+      ToReal
     }
 
     private IToken/*!*/ tok;
@@ -2277,7 +2185,6 @@ 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) {
@@ -2357,9 +2264,8 @@ namespace Microsoft.Boogie {
 
       tpInstantiation = SimpleTypeParamInstantiation.EMPTY;
 
-      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);
+      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);
       }
 
       return this.type;
diff --git a/Source/Provers/SMTLib/SMTLibProcess.cs b/Source/Provers/SMTLib/SMTLibProcess.cs
index a2fe4d4e..9fda36e7 100644
--- a/Source/Provers/SMTLib/SMTLibProcess.cs
+++ b/Source/Provers/SMTLib/SMTLibProcess.cs
@@ -91,8 +91,8 @@ namespace Microsoft.Boogie.SMTLib
 
          // Give it a chance to exit cleanly (e.g. to flush buffers)
         if (!prover.WaitForExit(timeout)) {
-        prover.Kill();
-      }
+          prover.Kill();
+        }
       } catch { /* Swallow errors */ }
     }
 
@@ -105,7 +105,6 @@ namespace Microsoft.Boogie.SMTLib
         log = log.Replace("\r", "").Replace("\n", " ");
         Console.WriteLine("[SMT-INP-{0}] {1}", smtProcessId, log);
       }
-      //Console.WriteLine(cmd);
       toProver.WriteLine(cmd);
     }
 
diff --git a/Source/Provers/SMTLib/TypeDeclCollector.cs b/Source/Provers/SMTLib/TypeDeclCollector.cs
index d7c56d90..eaed83e9 100644
--- a/Source/Provers/SMTLib/TypeDeclCollector.cs
+++ b/Source/Provers/SMTLib/TypeDeclCollector.cs
@@ -268,7 +268,7 @@ void ObjectInvariant()
           "(declare-fun " + printedName + " () " + TypeToString(node.Type) + ")";
         if (!(printedName.StartsWith("assume$$") || printedName.StartsWith("soft$$") || printedName.StartsWith("try$$")))
         {
-        AddDeclaration(decl);
+          AddDeclaration(decl);
         }
         KnownVariables.Add(node);
 		if(declHandler != null)
@@ -311,7 +311,7 @@ void ObjectInvariant()
         return;
       }
 
-      if (type.IsBool || type.IsInt || type.IsReal || type.IsFloat || type.IsBv)
+      if (type.IsBool || type.IsInt || type.IsReal || type.IsBv)
         return;
 
       CtorType ctorType = type as CtorType;
diff --git a/Test/floats/float3.bpl.expect b/Test/floats/float3.bpl.expect
index 6abb715b..37fad75c 100644
--- a/Test/floats/float3.bpl.expect
+++ b/Test/floats/float3.bpl.expect
@@ -1,2 +1,2 @@
-

-Boogie program verifier finished with 1 verified, 0 errors

+
+Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/floats/float4.bpl.expect b/Test/floats/float4.bpl.expect
index 6abb715b..37fad75c 100644
--- a/Test/floats/float4.bpl.expect
+++ b/Test/floats/float4.bpl.expect
@@ -1,2 +1,2 @@
-

-Boogie program verifier finished with 1 verified, 0 errors

+
+Boogie program verifier finished with 1 verified, 0 errors