summaryrefslogtreecommitdiff
path: root/Source
diff options
context:
space:
mode:
authorGravatar Checkmate50 <dgeisler50@gmail.com>2015-09-23 04:08:00 -0600
committerGravatar Checkmate50 <dgeisler50@gmail.com>2015-09-23 04:08:00 -0600
commit80f3d4ed1bb221adbd3c7162acea10920b9fab73 (patch)
tree218275e91b58fdb3cbce0376a4b423fa34e4e763 /Source
parent28a20e6eba2919e008f70874b4c12a3ce7ad049c (diff)
Modified BigFloat to avoid evaluating the floating point value before sending it to z3
Diffstat (limited to 'Source')
-rw-r--r--Source/Basetypes/BigFloat.cs1006
-rw-r--r--Source/Core/AbsyExpr.cs20
-rw-r--r--Source/Provers/SMTLib/SMTLibLineariser.cs12
-rw-r--r--Source/VCExpr/VCExprASTPrinter.cs12
4 files changed, 501 insertions, 549 deletions
diff --git a/Source/Basetypes/BigFloat.cs b/Source/Basetypes/BigFloat.cs
index 33860a4f..e9d5e670 100644
--- a/Source/Basetypes/BigFloat.cs
+++ b/Source/Basetypes/BigFloat.cs
@@ -1,516 +1,490 @@
-//-----------------------------------------------------------------------------
-//
-// Copyright (C) Microsoft Corporation. All Rights Reserved.
-//
-//-----------------------------------------------------------------------------
-
-using System;
-using System.Collections.Generic;
-using System.Linq;
-using System.Text;
-using System.Diagnostics.Contracts;
-using System.Diagnostics;
-
-namespace Microsoft.Basetypes
-{
- using BIM = System.Numerics.BigInteger;
-
- /// <summary>
- /// A representation of a 32-bit floating point value
- /// Note that this value has a 1-bit sign, 8-bit exponent, and 24-bit mantissa
- /// </summary>
- public struct BigFloat
- {
- //Please note that this code outline is copy-pasted from BigDec.cs
-
- // the internal representation
- [Rep]
- internal readonly BIM mantissa; //Note that the mantissa arrangement matches standard fp arrangement (most significant bit is farthest left)
- [Rep]
- internal readonly Boolean isNegative; //The left-most (sign) bit in the float representation
- [Rep]
- internal readonly int mantissaSize;
- [Rep]
- internal readonly int exponent; //The value of the exponent is always positive as per fp representation requirements
- [Rep]
- internal readonly int exponentSize; //The bit size of the exponent
-
- public BIM Mantissa {
- get {
- return isNegative ? -mantissa : mantissa;
- }
- }
-
- public int Exponent {
- get {
- return exponent - (int)Math.Pow(2, exponentSize - 1); //account for shift
- }
- }
-
- public int MantissaSize
- {
- get
- {
- return mantissaSize;
- }
- }
-
- public int ExponentSize
- {
- get
- {
- return exponentSize;
- }
- }
-
- public static BigFloat ZERO(int mantissaSize, int exponentSize) { return new BigFloat(0, 0, mantissaSize, exponentSize); } //Does not include negative zero
- public static BigFloat INF(int mantissaSize, int exponentSize) { return new BigFloat(0, 0, mantissaSize, exponentSize); } //Modify for IEEE standard
- public static BigFloat NEGINF(int mantissaSize, int exponentSize) { return new BigFloat(0, 0, mantissaSize, exponentSize); } //Modify for IEEE standard
- public static BigFloat NAN(int mantissaSize, int exponentSize) { return new BigFloat(0, 0, mantissaSize, exponentSize); } //Modify for IEEE standard
-
- private static readonly BIM two = new BIM(2);
- private static BIM two_n(int n) {
- BIM toReturn = new BIM(1);
- for (int i = 0; i < n; i++)
- toReturn = toReturn * two;
- return toReturn;
- }
-
-
- ////////////////////////////////////////////////////////////////////////////
- // Constructors
-
- //Please note that these constructors will be called throughout boogie
- //For a complete summary of where this class has been added, simply view constructor references
-
- [Pure]
- public static BigFloat FromInt(int v) {
- return new BigFloat(v, 0, 24, 8); //TODO: modify for correct fp representation
- }
-
- [Pure]
- public static BigFloat FromBigInt(BIM v) {
- return new BigFloat(0, v, 8, 24); //TODO: modify for correct fp representation
- }
-
- public static BigFloat FromBigDec(BIM v)
- {
- return new BigFloat(0, v, 8, 24); //TODO: modify for correct fp representation
- }
-
- [Pure]
- public static BigFloat FromString(string v) {
- String[] vals = v.Split(' ');
- if (vals.Length == 0 || vals.Length > 4)
- throw new FormatException();
- try
- {
- switch (vals.Length) {
- case 1:
- return Round(vals[0], 8, 24);
- case 2:
- return new BigFloat(Int32.Parse(vals[0]), BIM.Parse(vals[1]), 8, 24);
- case 3:
- return Round(vals[0], Int32.Parse(vals[1]), Int32.Parse(vals[2]));
- case 4:
- return new BigFloat(Int32.Parse(vals[0]), BIM.Parse(vals[1]), Int32.Parse(vals[2]), Int32.Parse(vals[3]));
- default:
- throw new FormatException(); //Unreachable
- }
- }
- catch (Exception) { //Catch parsing errors
- throw new FormatException();
- }
- }
-
- internal BigFloat(int exponent, BIM mantissa, int exponentSize, int mantissaSize) {
- this.exponentSize = exponentSize;
- this.exponent = exponent + (int)Math.Pow(2, exponentSize - 1);
- this.mantissa = mantissa;
- this.mantissaSize = mantissaSize;
- if (exponent < 0) { //ZERO case since the exponent is less than the minimum
- mantissa = 0;
- exponent = 0;
- this.isNegative = false;
- return;
- }
-
- this.isNegative = mantissa < 0;
- if (this.isNegative)
- mantissa = -mantissa; // ==> mantissa > 0
-
- BIM max = maxMantissa();
- while (this.mantissa > max) {
- this.mantissa = this.mantissa / two;
- this.exponent++;
- }
-
- //TODO: Add overflow check for exponent vs exponent size
- //this.exponent = this.exponent % this.exponentSize; ??
- }
-
- private BIM maxMantissa()
- {
- BIM result = new BIM(1);
- for (int i = 0; i < mantissaSize; i++)
- result = result * two;
- return result - 1;
- }
- private int maxExponent() { return (int)Math.Pow(2, exponentSize) - 1; }
-
-
-
- ////////////////////////////////////////////////////////////////////////////
- // Basic object operations
-
- [Pure]
- [Reads(ReadsAttribute.Reads.Nothing)]
- public override bool Equals(object obj) {
- if (obj == null)
- return false;
- if (!(obj is BigFloat))
- return false;
-
- return (this == (BigFloat)obj);
- }
-
- [Pure]
- public override int GetHashCode() {
- return Mantissa.GetHashCode() * 13 + Exponent.GetHashCode();
- }
-
- [Pure]
- public override string/*!*/ ToString() {
- Contract.Ensures(Contract.Result<string>() != null);
- return String.Format("{0}x2^{1}", Mantissa.ToString(), Exponent.ToString());
- }
-
-
- ////////////////////////////////////////////////////////////////////////////
- // Conversion operations
-
- /// <summary>
- /// Converts the given decimal value (provided as a string) to the nearest floating point approximation
- /// the returned fp assumes the given mantissa and exponent size
- /// </summary>
- /// <param name="value"></param>
- /// <param name="mantissaSize"></param>
- /// <param name="exponentSize"></param>
- /// <returns></returns>
- public static BigFloat Round(String value, int exponentSize, int mantissaSize)
- {
- int i = value.IndexOf('.');
- if (i == -1)
- return Round(BIM.Parse(value), 0, exponentSize, mantissaSize);
- return Round(i == 0 ? 0 : BIM.Parse(value.Substring(0, i)), BIM.Parse(value.Substring(i + 1, value.Length - i - 1)), exponentSize, mantissaSize);
- }
-
- /// <summary>
- /// Converts value.dec_value to a the closest float approximation with the given mantissaSize, exponentSize
- /// Returns the result of this calculation
- /// </summary>
- /// <param name="value"></param>
- /// <param name="power"></param>
- /// <param name="mantissaSize"></param>
- /// <param name="exponentSize"></param>
- /// <returns></returns>
- public static BigFloat Round(BIM value, BIM dec_value, int exponentSize, int mantissaSize)
- {
- int exp = 0;
- BIM one = new BIM(1);
- BIM ten = new BIM(10);
- BIM dec_max = new BIM(0); //represents the order of magnitude of dec_value for carrying during calculations
-
- //First, determine the exponent
- while (value > one) { //Divide by two, increment exponent by 1
- if (!(value % two).IsZero) { //Add "1.0" to the decimal
- dec_max = new BIM(10);
- while (dec_max < dec_value)
- dec_max = dec_max * ten;
- dec_value = dec_value + dec_max;
- }
- value = value / two;
- if (!(dec_value % ten).IsZero)
- dec_value = dec_value * ten; //Creates excess zeroes to avoid losing data during division
- dec_value = dec_value / two;
- exp++;
- }
- if (value.IsZero && !dec_value.IsZero) {
- dec_max = new BIM(10);
- while (dec_max < dec_value)
- dec_max = dec_max * ten;
- while (value.IsZero) {//Multiply by two, decrement exponent by 1
- dec_value = dec_value * two;
- if (dec_value >= dec_max) {
- dec_value = dec_value - dec_max;
- value = value + one;
- }
- exp--;
- }
- }
-
- //Second, calculate the mantissa
- value = new BIM(0); //remove implicit bit
- dec_max = new BIM(10);
- while (dec_max < dec_value)
- dec_max = dec_max * ten;
- for (int i = mantissaSize; i > 0 && !dec_value.IsZero; i--) { //Multiply by two until the mantissa is fully calculated
- dec_value = dec_value * two;
- if (dec_value >= dec_max) {
- dec_value = dec_value - dec_max;
- value = value + two_n(i); //Note that i is decrementing so that the most significant bit is left-most in the representation
- }
- }
-
- return new BigFloat(exp, value, exponentSize, mantissaSize);
- }
-
- // ``floor`` rounds towards negative infinity (like SMT-LIBv2's to_int).
- /// <summary>
- /// Computes the floor and ceiling of this BigFloat. Note the choice of rounding towards negative
- /// infinity rather than zero for floor is because SMT-LIBv2's to_int function floors this way.
- /// </summary>
- /// <param name="floor">The Floor (rounded towards negative infinity)</param>
- /// <param name="ceiling">Ceiling (rounded towards positive infinity)</param>
- public void FloorCeiling(out BIM floor, out BIM ceiling) {
- //TODO: fix for fp functionality
- BIM n = Mantissa;
- int e = Exponent;
- if (n.IsZero) {
- floor = ceiling = n;
- } else if (0 <= e) {
- // it's an integer
- for (; 0 < e; e--) {
- n = n * two;
- }
- floor = ceiling = n;
- } else {
- // it's a non-zero integer, so the ceiling is one more than the floor
- for (; e < 0 && !n.IsZero; e++) {
- n = n / two; // Division rounds towards negative infinity
- }
-
- if (!isNegative) {
- floor = n;
- ceiling = n + 1;
- } else {
- ceiling = n;
- floor = n - 1;
- }
- }
- Debug.Assert(floor <= ceiling, "Invariant was not maintained");
- }
-
- [Pure]
- public String ToDecimalString(int maxDigits) {
- //TODO: fix for fp functionality
- string s = Mantissa.ToString();
- int digits = (isNegative) ? s.Length - 1 : s.Length;
- BIM max = BIM.Pow(10, maxDigits);
- BIM min = -max;
-
- if (Exponent >= 0) {
- if (maxDigits < digits || maxDigits - digits < Exponent) {
- return String.Format("{0}.0", (!isNegative) ? max.ToString() : min.ToString());
- }
- else {
- return String.Format("{0}{1}.0", s, new string('0', Exponent));
- }
- }
- else {
- int exp = -Exponent;
-
- if (exp < digits) {
- int intDigits = digits - exp;
- if (maxDigits < intDigits) {
- return String.Format("{0}.0", (!isNegative) ? max.ToString() : min.ToString());
- }
- else {
- int fracDigits = Math.Min(maxDigits, digits - intDigits);
- return String.Format("{0}.{1}", s.Substring(0, intDigits), s.Substring(intDigits, fracDigits));
- }
- }
- else {
- int fracDigits = Math.Min(maxDigits, digits);
- return String.Format("0.{0}{1}", new string('0', exp - fracDigits), s.Substring(0, fracDigits));
- }
- }
- }
-
- [Pure]
- public string ToDecimalString() {
- //TODO: fix for fp functionality
- string m = Mantissa.ToString();
- var e = Exponent;
- if (0 <= Exponent) {
- return m + Zeros(e) + ".0";
- } else {
- e = -e;
- // compute k to be the longest suffix of m consisting of all zeros (but no longer than e, and not the entire string)
- var maxK = e < m.Length ? e : m.Length - 1;
- var last = m.Length - 1;
- var k = 0;
- while (k < maxK && m[last - k] == '0') {
- k++;
- }
- if (0 < k) {
- // chop off the suffix of k zeros from m and adjust e accordingly
- m = m.Substring(0, m.Length - k);
- e -= k;
- }
- if (e == 0) {
- return m;
- } else if (e < m.Length) {
- var n = m.Length - e;
- return m.Substring(0, n) + "." + m.Substring(n);
- } else {
- return "0." + Zeros(e - m.Length) + m;
- }
- }
- }
-
- [Pure]
- public static string Zeros(int n) {
- //TODO: fix for fp functionality
- Contract.Requires(0 <= n);
- if (n <= 10) {
- var tenZeros = "0000000000";
- return tenZeros.Substring(0, n);
- } else {
- var d = n / 2;
- var s = Zeros(d);
- if (n % 2 == 0) {
- return s + s;
- } else {
- return s + s + "0";
- }
- }
- }
-
-
- ////////////////////////////////////////////////////////////////////////////
- // Basic arithmetic operations
-
- [Pure]
- public BigFloat Abs {
- //TODO: fix for fp functionality
- get {
- return new BigFloat(Exponent, BIM.Abs(Mantissa), ExponentSize, MantissaSize);
- }
- }
-
- [Pure]
- public BigFloat Negate {
- //TODO: Modify for correct fp functionality
- get {
- return new BigFloat(Exponent, BIM.Negate(Mantissa), ExponentSize, MantissaSize);
- }
- }
-
- [Pure]
- public static BigFloat operator -(BigFloat x) {
- return x.Negate;
- }
-
- [Pure]
- public static BigFloat operator +(BigFloat x, BigFloat y) {
- //TODO: Modify for correct fp functionality
- Contract.Requires(x.ExponentSize == y.ExponentSize);
- Contract.Requires(x.MantissaSize == y.MantissaSize);
- BIM m1 = x.Mantissa;
- int e1 = x.Exponent;
- BIM m2 = y.Mantissa;
- int e2 = y.Exponent;
- m1 = m1 + two_n(x.mantissaSize + 1); //Add implicit bit
- m2 = m2 + two_n(y.mantissaSize + 1);
- if (e2 > e1) {
- m1 = y.Mantissa;
- e1 = y.Exponent;
- m2 = x.Mantissa;
- e2 = x.Exponent;
- }
-
- while (e2 < e1) {
- m2 = m2 / two;
- e2++;
- }
-
- return new BigFloat(e1, m1 + m2, x.MantissaSize, x.ExponentSize);
- }
-
- [Pure]
- public static BigFloat operator -(BigFloat x, BigFloat y) {
- return x + y.Negate;
- }
-
- [Pure]
- public static BigFloat operator *(BigFloat x, BigFloat y) {
- Contract.Requires(x.ExponentSize == y.ExponentSize);
- Contract.Requires(x.MantissaSize == y.MantissaSize);
- return new BigFloat(x.Exponent + y.Exponent, x.Mantissa * y.Mantissa, x.MantissaSize, x.ExponentSize);
- }
-
-
- ////////////////////////////////////////////////////////////////////////////
- // Some basic comparison operations
-
- public bool IsPositive {
- get {
- return (!isNegative);
- }
- }
-
- public bool IsNegative {
- get {
- return (isNegative);
- }
- }
-
- public bool IsZero {
- get {
- return Mantissa.IsZero && Exponent == 0;
- }
- }
-
- [Pure]
- public int CompareTo(BigFloat that) {
- if (this.exponent > that.exponent)
- return 1;
- if (this.exponent < that.exponent)
- return -1;
- if (this.Mantissa == that.Mantissa)
- return 0;
- return this.Mantissa > that.Mantissa ? 1 : -1;
- }
-
- [Pure]
- public static bool operator ==(BigFloat x, BigFloat y) {
- return x.CompareTo(y) == 0;
- }
-
- [Pure]
- public static bool operator !=(BigFloat x, BigFloat y) {
- return x.CompareTo(y) != 0;
- }
-
- [Pure]
- public static bool operator <(BigFloat x, BigFloat y) {
- return x.CompareTo(y) < 0;
- }
-
- [Pure]
- public static bool operator >(BigFloat x, BigFloat y) {
- return x.CompareTo(y) > 0;
- }
-
- [Pure]
- public static bool operator <=(BigFloat x, BigFloat y) {
- return x.CompareTo(y) <= 0;
- }
-
- [Pure]
- public static bool operator >=(BigFloat x, BigFloat y) {
- return x.CompareTo(y) >= 0;
- }
- }
-}
+//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation. All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+
+using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+using System.Diagnostics.Contracts;
+using System.Diagnostics;
+
+namespace Microsoft.Basetypes
+{
+ using BIM = System.Numerics.BigInteger;
+
+ /// <summary>
+ /// A representation of a 32-bit floating point value
+ /// Note that this value has a 1-bit sign, 8-bit exponent, and 24-bit mantissa
+ /// </summary>
+ public struct BigFloat
+ {
+ //Please note that this code outline is copy-pasted from BigDec.cs
+
+ // the internal representation
+ [Rep]
+ internal readonly BIM mantissa; //Note that the mantissa arrangement matches standard fp arrangement (most significant bit is farthest left)
+ [Rep]
+ internal readonly int mantissaSize;
+ [Rep]
+ internal readonly int exponent; //The value of the exponent is always positive as per fp representation requirements
+ [Rep]
+ internal readonly int exponentSize; //The bit size of the exponent
+ [Rep]
+ internal readonly BigDec dec_value;
+ [Rep]
+ internal readonly bool isDec;
+
+ public BIM Mantissa {
+ get {
+ return mantissa;
+ }
+ }
+
+ public int Exponent {
+ get {
+ return exponent;
+ }
+ }
+
+ public int MantissaSize {
+ get {
+ return mantissaSize;
+ }
+ }
+
+ public int ExponentSize {
+ get {
+ return exponentSize;
+ }
+ }
+
+ public BigDec Decimal {
+ get {
+ return dec_value;
+ }
+ }
+
+ public bool IsDec {
+ get {
+ return IsDec;
+ }
+ }
+
+ public static BigFloat ZERO(int mantissaSize, int exponentSize) { return new BigFloat(0, 0, mantissaSize, exponentSize); } //Does not include negative zero
+
+ private static readonly BIM two = new BIM(2);
+ private static BIM two_n(int n) {
+ BIM toReturn = new BIM(1);
+ for (int i = 0; i < n; i++)
+ toReturn = toReturn * two;
+ return toReturn;
+ }
+
+
+ ////////////////////////////////////////////////////////////////////////////
+ // Constructors
+
+ //Please note that these constructors will be called throughout boogie
+ //For a complete summary of where this class has been added, simply view constructor references
+
+ [Pure]
+ public static BigFloat FromInt(int v) {
+ return new BigFloat(v, 0, 24, 8);
+ }
+
+ [Pure]
+ public static BigFloat FromBigInt(BIM v) {
+ return new BigFloat(0, v, 8, 24);
+ }
+
+ public static BigFloat FromBigDec(BigDec v)
+ {
+ return new BigFloat(v, 8, 24);
+ }
+
+ [Pure]
+ public static BigFloat FromString(string v) {
+ String[] vals = v.Split(' ');
+ if (vals.Length == 0 || vals.Length > 4)
+ throw new FormatException();
+ try
+ {
+ switch (vals.Length) {
+ case 1:
+ return new BigFloat(BigDec.FromString(vals[0]), 8, 24);
+ case 2:
+ return new BigFloat(Int32.Parse(vals[0]), BIM.Parse(vals[1]), 8, 24);
+ case 3:
+ return new BigFloat(BigDec.FromString(vals[0]), Int32.Parse(vals[1]), Int32.Parse(vals[2]));
+ case 4:
+ return new BigFloat(Int32.Parse(vals[0]), BIM.Parse(vals[1]), Int32.Parse(vals[2]), Int32.Parse(vals[3]));
+ default:
+ throw new FormatException(); //Unreachable
+ }
+ }
+ catch (Exception) { //Catch parsing errors
+ throw new FormatException();
+ }
+ }
+
+ internal BigFloat(int exponent, BIM mantissa, int exponentSize, int mantissaSize) {
+ this.exponentSize = exponentSize;
+ this.exponent = exponent;
+ this.mantissa = mantissa;
+ this.mantissaSize = mantissaSize;
+ this.isDec = false;
+ this.dec_value = BigDec.ZERO;
+ }
+
+ internal BigFloat(BigDec dec_value, int exponentSize, int mantissaSize) {
+ this.exponentSize = exponentSize;
+ this.mantissaSize = mantissaSize;
+ this.exponent = 0;
+ this.mantissa = 0;
+ this.isDec = true;
+ this.dec_value = dec_value;
+ }
+
+ private BIM maxMantissa()
+ {
+ BIM result = new BIM(1);
+ for (int i = 0; i < mantissaSize; i++)
+ result = result * two;
+ return result - 1;
+ }
+ private int maxExponent() { return (int)Math.Pow(2, exponentSize) - 1; }
+
+
+
+ ////////////////////////////////////////////////////////////////////////////
+ // Basic object operations
+
+ [Pure]
+ [Reads(ReadsAttribute.Reads.Nothing)]
+ public override bool Equals(object obj) {
+ if (obj == null)
+ return false;
+ if (!(obj is BigFloat))
+ return false;
+
+ return (this == (BigFloat)obj);
+ }
+
+ [Pure]
+ public override int GetHashCode() {
+ return Mantissa.GetHashCode() * 13 + Exponent.GetHashCode();
+ }
+
+ [Pure]
+ public override string/*!*/ ToString() {
+ Contract.Ensures(Contract.Result<string>() != null);
+ return String.Format("{0}x2^{1}", Mantissa.ToString(), Exponent.ToString());
+ }
+
+
+ ////////////////////////////////////////////////////////////////////////////
+ // Conversion operations
+
+ /// <summary>
+ /// NOTE: THIS METHOD MAY NOT WORK AS EXPECTED!!!
+ /// Converts the given decimal value (provided as a string) to the nearest floating point approximation
+ /// the returned fp assumes the given mantissa and exponent size
+ /// </summary>
+ /// <param name="value"></param>
+ /// <param name="mantissaSize"></param>
+ /// <param name="exponentSize"></param>
+ /// <returns></returns>
+ public static BigFloat Round(String value, int exponentSize, int mantissaSize)
+ {
+ int i = value.IndexOf('.');
+ if (i == -1)
+ return Round(BIM.Parse(value), 0, exponentSize, mantissaSize);
+ return Round(i == 0 ? 0 : BIM.Parse(value.Substring(0, i)), BIM.Parse(value.Substring(i + 1, value.Length - i - 1)), exponentSize, mantissaSize);
+ }
+
+ /// <summary>
+ /// NOTE: THIS METHOD MAY NOT WORK AS EXPECTED!!!!
+ /// Converts value.dec_value to a the closest float approximation with the given mantissaSize, exponentSize
+ /// Returns the result of this calculation
+ /// </summary>
+ /// <param name="value"></param>
+ /// <param name="power"></param>
+ /// <param name="mantissaSize"></param>
+ /// <param name="exponentSize"></param>
+ /// <returns></returns>
+ public static BigFloat Round(BIM value, BIM dec_value, int exponentSize, int mantissaSize)
+ {
+ int exp = 0;
+ BIM one = new BIM(1);
+ BIM ten = new BIM(10);
+ BIM dec_max = new BIM(0); //represents the order of magnitude of dec_value for carrying during calculations
+
+ //First, determine the exponent
+ while (value > one) { //Divide by two, increment exponent by 1
+ if (!(value % two).IsZero) { //Add "1.0" to the decimal
+ dec_max = new BIM(10);
+ while (dec_max < dec_value)
+ dec_max = dec_max * ten;
+ dec_value = dec_value + dec_max;
+ }
+ value = value / two;
+ if (!(dec_value % ten).IsZero)
+ dec_value = dec_value * ten; //Creates excess zeroes to avoid losing data during division
+ dec_value = dec_value / two;
+ exp++;
+ }
+ if (value.IsZero && !dec_value.IsZero) {
+ dec_max = new BIM(10);
+ while (dec_max < dec_value)
+ dec_max = dec_max * ten;
+ while (value.IsZero) {//Multiply by two, decrement exponent by 1
+ dec_value = dec_value * two;
+ if (dec_value >= dec_max) {
+ dec_value = dec_value - dec_max;
+ value = value + one;
+ }
+ exp--;
+ }
+ }
+
+ //Second, calculate the mantissa
+ value = new BIM(0); //remove implicit bit
+ dec_max = new BIM(10);
+ while (dec_max < dec_value)
+ dec_max = dec_max * ten;
+ for (int i = mantissaSize; i > 0 && !dec_value.IsZero; i--) { //Multiply by two until the mantissa is fully calculated
+ dec_value = dec_value * two;
+ if (dec_value >= dec_max) {
+ dec_value = dec_value - dec_max;
+ value = value + two_n(i); //Note that i is decrementing so that the most significant bit is left-most in the representation
+ }
+ }
+
+ return new BigFloat(exp, value, exponentSize, mantissaSize);
+ }
+
+ // ``floor`` rounds towards negative infinity (like SMT-LIBv2's to_int).
+ /// <summary>
+ /// NOTE: THIS PROBABLY WON'T GIVE USEFUL OUTPUT!!!
+ /// Computes the floor and ceiling of this BigFloat. Note the choice of rounding towards negative
+ /// infinity rather than zero for floor is because SMT-LIBv2's to_int function floors this way.
+ /// </summary>
+ /// <param name="floor">The Floor (rounded towards negative infinity)</param>
+ /// <param name="ceiling">Ceiling (rounded towards positive infinity)</param>
+ public void FloorCeiling(out BIM floor, out BIM ceiling) {
+ //TODO: fix for fp functionality
+ BIM n = Mantissa;
+ int e = Exponent;
+ if (n.IsZero) {
+ floor = ceiling = n;
+ } else if (0 <= e) {
+ // it's an integer
+ for (; 0 < e; e--) {
+ n = n * two;
+ }
+ floor = ceiling = n;
+ } else {
+ // it's a non-zero integer, so the ceiling is one more than the floor
+ for (; e < 0 && !n.IsZero; e++) {
+ n = n / two; // Division rounds towards negative infinity
+ }
+
+ if (!IsNegative) {
+ floor = n;
+ ceiling = n + 1;
+ } else {
+ ceiling = n;
+ floor = n - 1;
+ }
+ }
+ Debug.Assert(floor <= ceiling, "Invariant was not maintained");
+ }
+
+ [Pure]
+ public String ToDecimalString(int maxDigits) {
+ //TODO: fix for fp functionality
+ {
+ throw new NotImplementedException();
+ }
+ }
+
+ [Pure]
+ public string ToDecimalString() {
+ //TODO: fix for fp functionality
+ string m = Mantissa.ToString();
+ var e = Exponent;
+ if (0 <= Exponent) {
+ return m + Zeros(e) + ".0";
+ } else {
+ e = -e;
+ // compute k to be the longest suffix of m consisting of all zeros (but no longer than e, and not the entire string)
+ var maxK = e < m.Length ? e : m.Length - 1;
+ var last = m.Length - 1;
+ var k = 0;
+ while (k < maxK && m[last - k] == '0') {
+ k++;
+ }
+ if (0 < k) {
+ // chop off the suffix of k zeros from m and adjust e accordingly
+ m = m.Substring(0, m.Length - k);
+ e -= k;
+ }
+ if (e == 0) {
+ return m;
+ } else if (e < m.Length) {
+ var n = m.Length - e;
+ return m.Substring(0, n) + "." + m.Substring(n);
+ } else {
+ return "0." + Zeros(e - m.Length) + m;
+ }
+ }
+ }
+
+ [Pure]
+ public static string Zeros(int n) {
+ //TODO: fix for fp functionality
+ Contract.Requires(0 <= n);
+ if (n <= 10) {
+ var tenZeros = "0000000000";
+ return tenZeros.Substring(0, n);
+ } else {
+ var d = n / 2;
+ var s = Zeros(d);
+ if (n % 2 == 0) {
+ return s + s;
+ } else {
+ return s + s + "0";
+ }
+ }
+ }
+
+
+ ////////////////////////////////////////////////////////////////////////////
+ // Basic arithmetic operations
+
+ [Pure]
+ public BigFloat Abs {
+ //TODO: fix for fp functionality
+ get {
+ return new BigFloat(Exponent, BIM.Abs(Mantissa), ExponentSize, MantissaSize);
+ }
+ }
+
+ [Pure]
+ public BigFloat Negate {
+ //TODO: Modify for correct fp functionality
+ get {
+ return new BigFloat(Exponent, BIM.Negate(Mantissa), ExponentSize, MantissaSize);
+ }
+ }
+
+ [Pure]
+ public static BigFloat operator -(BigFloat x) {
+ return x.Negate;
+ }
+
+ [Pure]
+ public static BigFloat operator +(BigFloat x, BigFloat y) {
+ //TODO: Modify for correct fp functionality
+ Contract.Requires(x.ExponentSize == y.ExponentSize);
+ Contract.Requires(x.MantissaSize == y.MantissaSize);
+ BIM m1 = x.Mantissa;
+ int e1 = x.Exponent;
+ BIM m2 = y.Mantissa;
+ int e2 = y.Exponent;
+ m1 = m1 + two_n(x.mantissaSize + 1); //Add implicit bit
+ m2 = m2 + two_n(y.mantissaSize + 1);
+ if (e2 > e1) {
+ m1 = y.Mantissa;
+ e1 = y.Exponent;
+ m2 = x.Mantissa;
+ e2 = x.Exponent;
+ }
+
+ while (e2 < e1) {
+ m2 = m2 / two;
+ e2++;
+ }
+
+ return new BigFloat(e1, m1 + m2, x.MantissaSize, x.ExponentSize);
+ }
+
+ [Pure]
+ public static BigFloat operator -(BigFloat x, BigFloat y) {
+ return x + y.Negate;
+ }
+
+ [Pure]
+ public static BigFloat operator *(BigFloat x, BigFloat y) {
+ Contract.Requires(x.ExponentSize == y.ExponentSize);
+ Contract.Requires(x.MantissaSize == y.MantissaSize);
+ return new BigFloat(x.Exponent + y.Exponent, x.Mantissa * y.Mantissa, x.MantissaSize, x.ExponentSize);
+ }
+
+
+ ////////////////////////////////////////////////////////////////////////////
+ // Some basic comparison operations
+
+ public bool IsPositive {
+ get {
+ return !IsNegative;
+ }
+ }
+
+ public bool IsNegative {
+ get {
+ return (isDec && dec_value >= BigDec.ZERO) || mantissa >= 0;
+ }
+ }
+
+ public bool IsZero {
+ get {
+ return Mantissa.IsZero && Exponent == 0;
+ }
+ }
+
+ [Pure]
+ public int CompareTo(BigFloat that) {
+ if (this.exponent > that.exponent)
+ return 1;
+ if (this.exponent < that.exponent)
+ return -1;
+ if (this.Mantissa == that.Mantissa)
+ return 0;
+ return this.Mantissa > that.Mantissa ? 1 : -1;
+ }
+
+ [Pure]
+ public static bool operator ==(BigFloat x, BigFloat y) {
+ return x.CompareTo(y) == 0;
+ }
+
+ [Pure]
+ public static bool operator !=(BigFloat x, BigFloat y) {
+ return x.CompareTo(y) != 0;
+ }
+
+ [Pure]
+ public static bool operator <(BigFloat x, BigFloat y) {
+ return x.CompareTo(y) < 0;
+ }
+
+ [Pure]
+ public static bool operator >(BigFloat x, BigFloat y) {
+ return x.CompareTo(y) > 0;
+ }
+
+ [Pure]
+ public static bool operator <=(BigFloat x, BigFloat y) {
+ return x.CompareTo(y) <= 0;
+ }
+
+ [Pure]
+ public static bool operator >=(BigFloat x, BigFloat y) {
+ return x.CompareTo(y) >= 0;
+ }
+ }
+}
diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs
index 181076a7..cf6fb922 100644
--- a/Source/Core/AbsyExpr.cs
+++ b/Source/Core/AbsyExpr.cs
@@ -1702,10 +1702,10 @@ namespace Microsoft.Boogie {
return Type.Real;
}
if (arg0type.IsFloat && arg0type.Unify(arg1type)) {
- return new FloatType(arg0.Type.FloatExponent, arg0.Type.FloatMantissa);
+ return Type.GetFloatType(arg0.Type.FloatExponent, arg0.Type.FloatMantissa);
}
if (arg1type.IsFloat && arg1type.Unify(arg0type)) {
- return new FloatType(arg1.Type.FloatExponent, arg1.Type.FloatMantissa);
+ return Type.GetFloatType(arg1.Type.FloatExponent, arg1.Type.FloatMantissa);
}
goto BAD_TYPE;
case Opcode.Div:
@@ -1719,6 +1719,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)) {
@@ -1751,10 +1757,9 @@ namespace Microsoft.Boogie {
if (arg0type.Unify(Type.Real) && arg1type.Unify(Type.Real)) {
return Type.Bool;
}
- //if (arg0type.Unify(Type.Float) && arg1type.Unify(Type.Float))
- //{
- //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:
@@ -1799,9 +1804,6 @@ namespace Microsoft.Boogie {
case Opcode.Pow:
return Type.Real;
- //case Opcode.FloatDiv:
- //return Type.Float;
-
case Opcode.Eq:
case Opcode.Neq:
case Opcode.Gt:
diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs
index 3633a9c0..f030870e 100644
--- a/Source/Provers/SMTLib/SMTLibLineariser.cs
+++ b/Source/Provers/SMTLib/SMTLibLineariser.cs
@@ -689,12 +689,6 @@ namespace Microsoft.Boogie.SMTLib
return true;
}
- public bool VisitFloatDivOp(VCExprNAry node, LineariserOptions options)
- { //TODO: match z3
- WriteApplication("/f", node, options);
- return true;
- }
-
public bool VisitPowOp(VCExprNAry node, LineariserOptions options) {
WriteApplication("real_pow", node, options);
return true;
@@ -746,12 +740,6 @@ namespace Microsoft.Boogie.SMTLib
return true;
}
- public bool VisitToFloatOp(VCExprNAry node, LineariserOptions options)
- {
- WriteApplication("to_float", node, options);
- return true;
- }
-
private string ExtractDatatype(Function func) {
if (func is DatatypeSelector) {
DatatypeSelector selector = (DatatypeSelector) func;
diff --git a/Source/VCExpr/VCExprASTPrinter.cs b/Source/VCExpr/VCExprASTPrinter.cs
index 8b79b0e5..00e6fb9c 100644
--- a/Source/VCExpr/VCExprASTPrinter.cs
+++ b/Source/VCExpr/VCExprASTPrinter.cs
@@ -302,12 +302,6 @@ namespace Microsoft.Boogie.VCExprAST {
//Contract.Requires(node != null);
return PrintNAry("/", node, wr);
}
- public bool VisitFloatDivOp(VCExprNAry node, TextWriter wr)
- {
- //Contract.Requires(wr != null);
- //Contract.Requires(node != null);
- return PrintNAry("/f", node, wr);
- }
public bool VisitPowOp(VCExprNAry node, TextWriter wr) {
//Contract.Requires(wr != null);
//Contract.Requires(node != null);
@@ -353,12 +347,6 @@ namespace Microsoft.Boogie.VCExprAST {
//Contract.Requires(node != null);
return PrintNAry("real", node, wr);
}
- public bool VisitToFloatOp(VCExprNAry node, TextWriter wr)
- {
- //Contract.Requires(wr != null);
- //Contract.Requires(node != null);
- return PrintNAry("float", node, wr);
- }
public bool VisitBoogieFunctionOp(VCExprNAry node, TextWriter wr) {
//Contract.Requires(wr != null);
//Contract.Requires(node != null);