From d652155ae013f36a1ee17653a8e458baad2d9c2c Mon Sep 17 00:00:00 2001 From: Checkmate50 Date: Mon, 6 Jun 2016 23:14:18 -0600 Subject: Merging complete. Everything looks good *crosses fingers* --- Source/Basetypes/Basetypes.csproj | 406 ++++++++++---------- Source/Basetypes/BigDec.cs | 760 +++++++++++++++++++------------------- Source/Basetypes/BigNum.cs | 722 ++++++++++++++++++------------------ Source/Basetypes/Rational.cs | 496 ++++++++++++------------- Source/Basetypes/Set.cs | 570 ++++++++++++++-------------- Source/Basetypes/cce.cs | 384 +++++++++---------- 6 files changed, 1669 insertions(+), 1669 deletions(-) (limited to 'Source/Basetypes') diff --git a/Source/Basetypes/Basetypes.csproj b/Source/Basetypes/Basetypes.csproj index 4ecdee8d..5b425bc5 100644 --- a/Source/Basetypes/Basetypes.csproj +++ b/Source/Basetypes/Basetypes.csproj @@ -1,204 +1,204 @@ - - - - Debug - AnyCPU - 9.0.21022 - 2.0 - {43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0} - Library - Properties - Basetypes - Basetypes - v4.0 - 512 - 1 - true - ..\InterimKey.snk - - - 3.5 - - publish\ - true - Disk - false - Foreground - 7 - Days - false - false - true - 0 - 1.0.0.%2a - false - false - true - Client - - - true - full - false - bin\Debug\ - DEBUG;TRACE - prompt - 4 - False - False - True - False - False - False - False - False - False - False - False - True - False - False - False - - - - - - - - - - - - - Full - %28none%29 - AllRules.ruleset - - - pdbonly - true - bin\Release\ - TRACE - prompt - 4 - AllRules.ruleset - - - true - bin\z3apidebug\ - DEBUG;TRACE - full - AnyCPU - - - true - GlobalSuppressions.cs - prompt - Migrated rules for Basetypes.ruleset - true - 4 - false - - - true - bin\Checked\ - DEBUG;TRACE - full - AnyCPU - bin\Debug\Basetypes.dll.CodeAnalysisLog.xml - true - GlobalSuppressions.cs - prompt - AllRules.ruleset - ;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets - ;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules - True - False - True - False - False - False - False - False - False - False - False - False - True - False - False - False - - - - - - - False - Full - Build - 0 - 4 - false - - - true - bin\QED\ - DEBUG;TRACE - full - AnyCPU - prompt - AllRules.ruleset - - - - - - - - - - version.cs - - - - - - - - - - {ACCC0156-0921-43ED-8F67-AD8BDC8CDE31} - CodeContractsExtender - - - - - - - - False - .NET Framework 3.5 SP1 Client Profile - false - - - False - .NET Framework 3.5 SP1 - true - - - False - Windows Installer 3.1 - true - - - - + + + + Debug + AnyCPU + 9.0.21022 + 2.0 + {43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0} + Library + Properties + Basetypes + BoogieBasetypes + v4.0 + 512 + 1 + true + ..\InterimKey.snk + + + 3.5 + + publish\ + true + Disk + false + Foreground + 7 + Days + false + false + true + 0 + 1.0.0.%2a + false + false + true + Client + + + true + full + false + bin\Debug\ + DEBUG;TRACE + prompt + 4 + False + False + True + False + False + False + False + False + False + False + False + True + False + False + False + + + + + + + + + + + + + Full + %28none%29 + AllRules.ruleset + + + pdbonly + true + bin\Release\ + TRACE + prompt + 4 + AllRules.ruleset + + + true + bin\z3apidebug\ + DEBUG;TRACE + full + AnyCPU + + + true + GlobalSuppressions.cs + prompt + Migrated rules for Basetypes.ruleset + true + 4 + false + + + true + bin\Checked\ + DEBUG;TRACE + full + AnyCPU + bin\Debug\Basetypes.dll.CodeAnalysisLog.xml + true + GlobalSuppressions.cs + prompt + AllRules.ruleset + ;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets + ;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules + True + False + True + False + False + False + False + False + False + False + False + False + True + False + False + False + + + + + + + False + Full + Build + 0 + 4 + false + + + true + bin\QED\ + DEBUG;TRACE + full + AnyCPU + prompt + AllRules.ruleset + + + + + + + + + + version.cs + + + + + + + + + + {ACCC0156-0921-43ED-8F67-AD8BDC8CDE31} + CodeContractsExtender + + + + + + + + False + .NET Framework 3.5 SP1 Client Profile + false + + + False + .NET Framework 3.5 SP1 + true + + + False + Windows Installer 3.1 + true + + + + \ No newline at end of file diff --git a/Source/Basetypes/BigDec.cs b/Source/Basetypes/BigDec.cs index 0aeea8b1..e4666793 100644 --- a/Source/Basetypes/BigDec.cs +++ b/Source/Basetypes/BigDec.cs @@ -1,380 +1,380 @@ -//----------------------------------------------------------------------------- -// -// Copyright (C) Microsoft Corporation. All Rights Reserved. -// -//----------------------------------------------------------------------------- -using System; -using System.Text; -using System.Diagnostics.Contracts; -using System.Diagnostics; - - -namespace Microsoft.Basetypes { - using BIM = System.Numerics.BigInteger; - - - /// - /// A representation of decimal values. - /// - public struct BigDec { - - // the internal representation - [Rep] - internal readonly BIM mantissa; - [Rep] - internal readonly int exponent; - - public BIM Mantissa { - get { - return mantissa; - } - } - - public int Exponent { - get { - return exponent; - } - } - - public static readonly BigDec ZERO = FromInt(0); - private static readonly BIM ten = new BIM(10); - - - //////////////////////////////////////////////////////////////////////////// - // Constructors - - [Pure] - public static BigDec FromInt(int v) { - return new BigDec(v, 0); - } - - [Pure] - public static BigDec FromBigInt(BIM v) { - return new BigDec(v, 0); - } - - [Pure] - public static BigDec FromString(string v) { - if (v == null) throw new FormatException(); - - BIM integral = BIM.Zero; - BIM fraction = BIM.Zero; - int exponent = 0; - - int len = v.Length; - - int i = v.IndexOf('e'); - if (i >= 0) { - if (i + 1 == v.Length) throw new FormatException(); - exponent = Int32.Parse(v.Substring(i + 1, len - i - 1)); - len = i; - } - - int fractionLen = 0; - i = v.IndexOf('.'); - if (i >= 0) { - if (i + 1 == v.Length) throw new FormatException(); - fractionLen = len - i - 1; - fraction = BIM.Parse(v.Substring(i + 1, fractionLen)); - len = i; - } - - integral = BIM.Parse(v.Substring(0, len)); - - if (!fraction.IsZero) { - while (fractionLen > 0) { - integral = integral * ten; - exponent = exponent - 1; - fractionLen = fractionLen - 1; - } - } - - if (integral.Sign == -1) { - return new BigDec(integral - fraction, exponent); - } - else { - return new BigDec(integral + fraction, exponent); - } - } - - internal BigDec(BIM mantissa, int exponent) { - if (mantissa.IsZero) { - this.mantissa = mantissa; - this.exponent = 0; - } - else { - while (mantissa % ten == BIM.Zero) { - mantissa = mantissa / ten; - exponent = exponent + 1; - } - this.mantissa = mantissa; - this.exponent = exponent; - } - } - - - //////////////////////////////////////////////////////////////////////////// - // Basic object operations - - [Pure] - [Reads(ReadsAttribute.Reads.Nothing)] - public override bool Equals(object obj) { - if (obj == null) - return false; - if (!(obj is BigDec)) - return false; - - return (this == (BigDec)obj); - } - - [Pure] - public override int GetHashCode() { - return this.mantissa.GetHashCode() * 13 + this.exponent.GetHashCode(); - } - - [Pure] - public override string/*!*/ ToString() { - Contract.Ensures(Contract.Result() != null); - return String.Format("{0}e{1}", this.mantissa.ToString(), this.exponent.ToString()); - } - - - //////////////////////////////////////////////////////////////////////////// - // Conversion operations - - // ``floor`` rounds towards negative infinity (like SMT-LIBv2's to_int). - /// - /// Computes the floor and ceiling of this BigDec. Note the choice of rounding towards negative - /// infinity rather than zero for floor is because SMT-LIBv2's to_int function floors this way. - /// - /// The Floor (rounded towards negative infinity) - /// Ceiling (rounded towards positive infinity) - public void FloorCeiling(out BIM floor, out BIM ceiling) { - BIM n = this.mantissa; - int e = this.exponent; - if (n.IsZero) { - floor = ceiling = n; - } else if (0 <= e) { - // it's an integer - for (; 0 < e; e--) { - n = n * ten; - } - 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 / ten; // Division rounds towards negative infinity - } - - if (this.mantissa >= 0) { - 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) { - string s = this.mantissa.ToString(); - int digits = (this.mantissa >= 0) ? s.Length : s.Length - 1; - BIM max = BIM.Pow(10, maxDigits); - BIM min = -max; - - if (this.exponent >= 0) { - if (maxDigits < digits || maxDigits - digits < this.exponent) { - return String.Format("{0}.0", (this.mantissa >= 0) ? max.ToString() : min.ToString()); - } - else { - return String.Format("{0}{1}.0", s, new string('0', this.exponent)); - } - } - else { - int exp = -this.exponent; - - if (exp < digits) { - int intDigits = digits - exp; - if (maxDigits < intDigits) { - return String.Format("{0}.0", (this.mantissa >= 0) ? 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() { - string m = this.mantissa.ToString(); - var e = this.exponent; - if (0 <= this.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) { - 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 BigDec Abs { - get { - return new BigDec(BIM.Abs(this.mantissa), this.exponent); - } - } - - [Pure] - public BigDec Negate { - get { - return new BigDec(BIM.Negate(this.mantissa), this.exponent); - } - } - - [Pure] - public static BigDec operator -(BigDec x) { - return x.Negate; - } - - [Pure] - public static BigDec operator +(BigDec x, BigDec y) { - BIM m1 = x.mantissa; - int e1 = x.exponent; - BIM m2 = y.mantissa; - int e2 = y.exponent; - if (e2 < e1) { - m1 = y.mantissa; - e1 = y.exponent; - m2 = x.mantissa; - e2 = x.exponent; - } - - while (e2 > e1) { - m2 = m2 * ten; - e2 = e2 - 1; - } - - return new BigDec(m1 + m2, e1); - } - - [Pure] - public static BigDec operator -(BigDec x, BigDec y) { - return x + y.Negate; - } - - [Pure] - public static BigDec operator *(BigDec x, BigDec y) { - return new BigDec(x.mantissa * y.mantissa, x.exponent + y.exponent); - } - - - //////////////////////////////////////////////////////////////////////////// - // Some basic comparison operations - - public bool IsPositive { - get { - return (this.mantissa > BIM.Zero); - } - } - - public bool IsNegative { - get { - return (this.mantissa < BIM.Zero); - } - } - - public bool IsZero { - get { - return this.mantissa.IsZero; - } - } - - [Pure] - public int CompareTo(BigDec that) { - if (this.mantissa == that.mantissa && this.exponent == that.exponent) { - return 0; - } - else { - BigDec d = this - that; - return d.IsNegative ? -1 : 1; - } - } - - [Pure] - public static bool operator ==(BigDec x, BigDec y) { - return x.CompareTo(y) == 0; - } - - [Pure] - public static bool operator !=(BigDec x, BigDec y) { - return x.CompareTo(y) != 0; - } - - [Pure] - public static bool operator <(BigDec x, BigDec y) { - return x.CompareTo(y) < 0; - } - - [Pure] - public static bool operator >(BigDec x, BigDec y) { - return x.CompareTo(y) > 0; - } - - [Pure] - public static bool operator <=(BigDec x, BigDec y) { - return x.CompareTo(y) <= 0; - } - - [Pure] - public static bool operator >=(BigDec x, BigDec y) { - return x.CompareTo(y) >= 0; - } - } -} +//----------------------------------------------------------------------------- +// +// Copyright (C) Microsoft Corporation. All Rights Reserved. +// +//----------------------------------------------------------------------------- +using System; +using System.Text; +using System.Diagnostics.Contracts; +using System.Diagnostics; + + +namespace Microsoft.Basetypes { + using BIM = System.Numerics.BigInteger; + + + /// + /// A representation of decimal values. + /// + public struct BigDec { + + // the internal representation + [Rep] + internal readonly BIM mantissa; + [Rep] + internal readonly int exponent; + + public BIM Mantissa { + get { + return mantissa; + } + } + + public int Exponent { + get { + return exponent; + } + } + + public static readonly BigDec ZERO = FromInt(0); + private static readonly BIM ten = new BIM(10); + + + //////////////////////////////////////////////////////////////////////////// + // Constructors + + [Pure] + public static BigDec FromInt(int v) { + return new BigDec(v, 0); + } + + [Pure] + public static BigDec FromBigInt(BIM v) { + return new BigDec(v, 0); + } + + [Pure] + public static BigDec FromString(string v) { + if (v == null) throw new FormatException(); + + BIM integral = BIM.Zero; + BIM fraction = BIM.Zero; + int exponent = 0; + + int len = v.Length; + + int i = v.IndexOf('e'); + if (i >= 0) { + if (i + 1 == v.Length) throw new FormatException(); + exponent = Int32.Parse(v.Substring(i + 1, len - i - 1)); + len = i; + } + + int fractionLen = 0; + i = v.IndexOf('.'); + if (i >= 0) { + if (i + 1 == v.Length) throw new FormatException(); + fractionLen = len - i - 1; + fraction = BIM.Parse(v.Substring(i + 1, fractionLen)); + len = i; + } + + integral = BIM.Parse(v.Substring(0, len)); + + if (!fraction.IsZero) { + while (fractionLen > 0) { + integral = integral * ten; + exponent = exponent - 1; + fractionLen = fractionLen - 1; + } + } + + if (integral.Sign == -1) { + return new BigDec(integral - fraction, exponent); + } + else { + return new BigDec(integral + fraction, exponent); + } + } + + internal BigDec(BIM mantissa, int exponent) { + if (mantissa.IsZero) { + this.mantissa = mantissa; + this.exponent = 0; + } + else { + while (mantissa % ten == BIM.Zero) { + mantissa = mantissa / ten; + exponent = exponent + 1; + } + this.mantissa = mantissa; + this.exponent = exponent; + } + } + + + //////////////////////////////////////////////////////////////////////////// + // Basic object operations + + [Pure] + [Reads(ReadsAttribute.Reads.Nothing)] + public override bool Equals(object obj) { + if (obj == null) + return false; + if (!(obj is BigDec)) + return false; + + return (this == (BigDec)obj); + } + + [Pure] + public override int GetHashCode() { + return this.mantissa.GetHashCode() * 13 + this.exponent.GetHashCode(); + } + + [Pure] + public override string/*!*/ ToString() { + Contract.Ensures(Contract.Result() != null); + return String.Format("{0}e{1}", this.mantissa.ToString(), this.exponent.ToString()); + } + + + //////////////////////////////////////////////////////////////////////////// + // Conversion operations + + // ``floor`` rounds towards negative infinity (like SMT-LIBv2's to_int). + /// + /// Computes the floor and ceiling of this BigDec. Note the choice of rounding towards negative + /// infinity rather than zero for floor is because SMT-LIBv2's to_int function floors this way. + /// + /// The Floor (rounded towards negative infinity) + /// Ceiling (rounded towards positive infinity) + public void FloorCeiling(out BIM floor, out BIM ceiling) { + BIM n = this.mantissa; + int e = this.exponent; + if (n.IsZero) { + floor = ceiling = n; + } else if (0 <= e) { + // it's an integer + for (; 0 < e; e--) { + n = n * ten; + } + 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 / ten; // Division rounds towards negative infinity + } + + if (this.mantissa >= 0) { + 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) { + string s = this.mantissa.ToString(); + int digits = (this.mantissa >= 0) ? s.Length : s.Length - 1; + BIM max = BIM.Pow(10, maxDigits); + BIM min = -max; + + if (this.exponent >= 0) { + if (maxDigits < digits || maxDigits - digits < this.exponent) { + return String.Format("{0}.0", (this.mantissa >= 0) ? max.ToString() : min.ToString()); + } + else { + return String.Format("{0}{1}.0", s, new string('0', this.exponent)); + } + } + else { + int exp = -this.exponent; + + if (exp < digits) { + int intDigits = digits - exp; + if (maxDigits < intDigits) { + return String.Format("{0}.0", (this.mantissa >= 0) ? 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() { + string m = this.mantissa.ToString(); + var e = this.exponent; + if (0 <= this.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) { + 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 BigDec Abs { + get { + return new BigDec(BIM.Abs(this.mantissa), this.exponent); + } + } + + [Pure] + public BigDec Negate { + get { + return new BigDec(BIM.Negate(this.mantissa), this.exponent); + } + } + + [Pure] + public static BigDec operator -(BigDec x) { + return x.Negate; + } + + [Pure] + public static BigDec operator +(BigDec x, BigDec y) { + BIM m1 = x.mantissa; + int e1 = x.exponent; + BIM m2 = y.mantissa; + int e2 = y.exponent; + if (e2 < e1) { + m1 = y.mantissa; + e1 = y.exponent; + m2 = x.mantissa; + e2 = x.exponent; + } + + while (e2 > e1) { + m2 = m2 * ten; + e2 = e2 - 1; + } + + return new BigDec(m1 + m2, e1); + } + + [Pure] + public static BigDec operator -(BigDec x, BigDec y) { + return x + y.Negate; + } + + [Pure] + public static BigDec operator *(BigDec x, BigDec y) { + return new BigDec(x.mantissa * y.mantissa, x.exponent + y.exponent); + } + + + //////////////////////////////////////////////////////////////////////////// + // Some basic comparison operations + + public bool IsPositive { + get { + return (this.mantissa > BIM.Zero); + } + } + + public bool IsNegative { + get { + return (this.mantissa < BIM.Zero); + } + } + + public bool IsZero { + get { + return this.mantissa.IsZero; + } + } + + [Pure] + public int CompareTo(BigDec that) { + if (this.mantissa == that.mantissa && this.exponent == that.exponent) { + return 0; + } + else { + BigDec d = this - that; + return d.IsNegative ? -1 : 1; + } + } + + [Pure] + public static bool operator ==(BigDec x, BigDec y) { + return x.CompareTo(y) == 0; + } + + [Pure] + public static bool operator !=(BigDec x, BigDec y) { + return x.CompareTo(y) != 0; + } + + [Pure] + public static bool operator <(BigDec x, BigDec y) { + return x.CompareTo(y) < 0; + } + + [Pure] + public static bool operator >(BigDec x, BigDec y) { + return x.CompareTo(y) > 0; + } + + [Pure] + public static bool operator <=(BigDec x, BigDec y) { + return x.CompareTo(y) <= 0; + } + + [Pure] + public static bool operator >=(BigDec x, BigDec y) { + return x.CompareTo(y) >= 0; + } + } +} diff --git a/Source/Basetypes/BigNum.cs b/Source/Basetypes/BigNum.cs index ff676bc6..4469f149 100644 --- a/Source/Basetypes/BigNum.cs +++ b/Source/Basetypes/BigNum.cs @@ -1,361 +1,361 @@ -//----------------------------------------------------------------------------- -// -// Copyright (C) Microsoft Corporation. All Rights Reserved. -// -//----------------------------------------------------------------------------- -using System; -using System.Text; -using System.Diagnostics.Contracts; - - -namespace Microsoft.Basetypes { - using BIM = System.Numerics.BigInteger; - - /// - /// A thin wrapper around System.Numerics.BigInteger - /// (to be able to define equality, etc. properly) - /// - public struct BigNum { - - // the internal representation - [Rep] - internal readonly System.Numerics.BigInteger val; - public static readonly BigNum ZERO = new BigNum(BIM.Zero); - public static readonly BigNum ONE = new BigNum(BIM.One); - public static readonly BigNum MINUS_ONE = new BigNum(-BIM.One); - - [Pure] - public static BigNum FromInt(int v) { - return new BigNum(new BIM(v)); - } - - [Pure] - public static BigNum FromUInt(uint v) { - return new BigNum(new BIM((long)v)); - } - - [Pure] - public static BigNum FromLong(long v) { - return new BigNum(new BIM(v)); - } - - [Pure] - public static BigNum FromBigInt(System.Numerics.BigInteger v) { - return new BigNum(v); - } - - [Pure] - public static BigNum FromULong(ulong v) { - return FromString("" + v); - } - - [Pure] - public static BigNum FromString(string v) { - try { - return new BigNum(BIM.Parse(v)); - } catch (System.ArgumentException) { - throw new FormatException(); - } - } - - public static bool TryParse(string v, out BigNum res) { - try { - res = BigNum.FromString(v); - return true; - } catch (FormatException) { - res = ZERO; - return false; - } - } - - // Convert to int, without checking whether overflows occur - public int ToInt { - get { - return (int)val; - } - } - - public BIM ToBigInteger { - get { - return val; - } - } - - // Convert to int; assert that no overflows occur - public int ToIntSafe { - get { - Contract.Assert(this.InInt32); - return this.ToInt; - } - } - - public Rational ToRational { - get { - return Rational.FromBignum(this); - } - } - - public byte[] ToByteArray() - { - return this.val.ToByteArray(); - } - - internal BigNum(System.Numerics.BigInteger val) { - this.val = val; - } - - public static bool operator ==(BigNum x, BigNum y) { - return (x.val == y.val); - } - - public static bool operator !=(BigNum x, BigNum y) { - return !(x.val == y.val); - } - - [Pure] - [Reads(ReadsAttribute.Reads.Nothing)] - public override bool Equals(object obj) { - if (obj == null) - return false; - if (!(obj is BigNum)) - return false; - - BigNum other = (BigNum)obj; - return (this.val == other.val); - } - - [Pure] - public override int GetHashCode() { - return this.val.GetHashCode(); - } - - [Pure] - public override string/*!*/ ToString() { - Contract.Ensures(Contract.Result() != null); - return cce.NonNull(val.ToString()); - } - - ////////////////////////////////////////////////////////////////////////////// - // Very limited support for format strings - // Note: Negative integers are linearised with a minus "-" in hexadecimal, - // not in 2-complement notation (in contrast to what the method - // int32.ToString(format) does) - - [Pure] - public string/*!*/ ToString(string/*!*/ format) { - Contract.Requires(format != null); - Contract.Ensures(Contract.Result() != null); - if (format.StartsWith("d") || format.StartsWith("D")) { - string res = this.Abs.ToString(); - Contract.Assert(res != null); - return addMinus(this.Signum, - prefixWithZeros(extractPrecision(format), res)); - } else if (format.StartsWith("x") || format.StartsWith("X")) { - string res = this.toHex(format.Substring(0, 1)); - Contract.Assert(res != null); - return addMinus(this.Signum, - prefixWithZeros(extractPrecision(format), res)); - } else { - throw new FormatException("Format " + format + " is not supported"); - } - } - - private static readonly System.Numerics.BigInteger BI_2_TO_24 = new BIM(0x1000000); - - [Pure] - private string/*!*/ toHex(string/*!*/ format) { - Contract.Requires(format != null); - Contract.Ensures(Contract.Result() != null); - string res = ""; - System.Numerics.BigInteger rem = this.Abs.val; - - while (rem > BIM.Zero) { - res = ((int)(rem % BI_2_TO_24)).ToString(format) + res; - rem = rem / BI_2_TO_24; - } - - return res; - } - - [Pure] - private int extractPrecision(string/*!*/ format) { - Contract.Requires(format != null); - if (format.Length > 1) - // will throw a FormatException if the precision is invalid; - // that is ok - return Int32.Parse(format.Substring(1)); - // always output at least one digit - return 1; - } - - [Pure] - private string/*!*/ addMinus(int signum, string/*!*/ suffix) { - Contract.Requires(suffix != null); - Contract.Ensures(Contract.Result() != null); - if (signum < 0) - return "-" + suffix; - return suffix; - } - - [Pure] - private string/*!*/ prefixWithZeros(int minLength, string/*!*/ suffix) { - Contract.Requires(suffix != null); - Contract.Ensures(Contract.Result() != null); - StringBuilder res = new StringBuilder(); - while (res.Length + suffix.Length < minLength) - res.Append("0"); - res.Append(suffix); - return res.ToString(); - } - - //////////////////////////////////////////////////////////////////////////// - // Basic arithmetic operations - - public BigNum Abs { - get { - return new BigNum(BIM.Abs(this.val)); - } - } - - public BigNum Neg { - get { - return new BigNum(-this.val); - } - } - - [Pure] - public static BigNum operator -(BigNum x) { - return x.Neg; - } - - [Pure] - public static BigNum operator +(BigNum x, BigNum y) { - return new BigNum(x.val + y.val); - } - - [Pure] - public static BigNum operator -(BigNum x, BigNum y) { - return new BigNum(x.val - y.val); - } - - [Pure] - public static BigNum operator *(BigNum x, BigNum y) { - return new BigNum(x.val * y.val); - } - - // TODO: check that this has a proper semantics (which? :-)) - [Pure] - public static BigNum operator /(BigNum x, BigNum y) { - return new BigNum(x.val / y.val); - } - - // TODO: check that this has a proper semantics (which? :-)) - [Pure] - public static BigNum operator %(BigNum x, BigNum y) { - return new BigNum(x.val - ((x.val / y.val) * y.val)); - } - - [Pure] - public BigNum Min(BigNum that) { - return new BigNum(this.val <= that.val ? this.val : that.val); - } - - [Pure] - public BigNum Max(BigNum that) { - return new BigNum(this.val >= that.val ? this.val : that.val); - } - - /// - /// Returns the greatest common divisor of this and _y. - /// - /// - /// - public BigNum Gcd(BigNum _y) { - Contract.Ensures(!Contract.Result().IsNegative); - BigNum x = this.Abs; - BigNum y = _y.Abs; - - while (true) { - if (x < y) { - y = y % x; - if (y.IsZero) { - return x; - } - } else { - x = x % y; - if (x.IsZero) { - return y; - } - } - } - } - - //////////////////////////////////////////////////////////////////////////// - // Some basic comparison operations - - public int Signum { - get { - return this.val.Sign; - } - } - - public bool IsPositive { - get { - return (this.val > BIM.Zero); - } - } - - public bool IsNegative { - get { - return (this.val < BIM.Zero); - } - } - - public bool IsZero { - get { - return this.val.IsZero; - } - } - - [Pure] - public int CompareTo(BigNum that) { - if (this.val == that.val) - return 0; - if (this.val < that.val) - return -1; - return 1; - } - - [Pure] - public static bool operator <(BigNum x, BigNum y) { - return (x.val < y.val); - } - - [Pure] - public static bool operator >(BigNum x, BigNum y) { - return (x.val > y.val); - } - - [Pure] - public static bool operator <=(BigNum x, BigNum y) { - return (x.val <= y.val); - } - - [Pure] - public static bool operator >=(BigNum x, BigNum y) { - return (x.val >= y.val); - } - - - private static readonly System.Numerics.BigInteger MaxInt32 = - new BIM(Int32.MaxValue); - private static readonly System.Numerics.BigInteger MinInt32 = - new BIM(Int32.MinValue); - - public bool InInt32 { - get { - return (val >= MinInt32) && (val <= MaxInt32); - } - } - } -} +//----------------------------------------------------------------------------- +// +// Copyright (C) Microsoft Corporation. All Rights Reserved. +// +//----------------------------------------------------------------------------- +using System; +using System.Text; +using System.Diagnostics.Contracts; + + +namespace Microsoft.Basetypes { + using BIM = System.Numerics.BigInteger; + + /// + /// A thin wrapper around System.Numerics.BigInteger + /// (to be able to define equality, etc. properly) + /// + public struct BigNum { + + // the internal representation + [Rep] + internal readonly System.Numerics.BigInteger val; + public static readonly BigNum ZERO = new BigNum(BIM.Zero); + public static readonly BigNum ONE = new BigNum(BIM.One); + public static readonly BigNum MINUS_ONE = new BigNum(-BIM.One); + + [Pure] + public static BigNum FromInt(int v) { + return new BigNum(new BIM(v)); + } + + [Pure] + public static BigNum FromUInt(uint v) { + return new BigNum(new BIM((long)v)); + } + + [Pure] + public static BigNum FromLong(long v) { + return new BigNum(new BIM(v)); + } + + [Pure] + public static BigNum FromBigInt(System.Numerics.BigInteger v) { + return new BigNum(v); + } + + [Pure] + public static BigNum FromULong(ulong v) { + return FromString("" + v); + } + + [Pure] + public static BigNum FromString(string v) { + try { + return new BigNum(BIM.Parse(v)); + } catch (System.ArgumentException) { + throw new FormatException(); + } + } + + public static bool TryParse(string v, out BigNum res) { + try { + res = BigNum.FromString(v); + return true; + } catch (FormatException) { + res = ZERO; + return false; + } + } + + // Convert to int, without checking whether overflows occur + public int ToInt { + get { + return (int)val; + } + } + + public BIM ToBigInteger { + get { + return val; + } + } + + // Convert to int; assert that no overflows occur + public int ToIntSafe { + get { + Contract.Assert(this.InInt32); + return this.ToInt; + } + } + + public Rational ToRational { + get { + return Rational.FromBignum(this); + } + } + + public byte[] ToByteArray() + { + return this.val.ToByteArray(); + } + + internal BigNum(System.Numerics.BigInteger val) { + this.val = val; + } + + public static bool operator ==(BigNum x, BigNum y) { + return (x.val == y.val); + } + + public static bool operator !=(BigNum x, BigNum y) { + return !(x.val == y.val); + } + + [Pure] + [Reads(ReadsAttribute.Reads.Nothing)] + public override bool Equals(object obj) { + if (obj == null) + return false; + if (!(obj is BigNum)) + return false; + + BigNum other = (BigNum)obj; + return (this.val == other.val); + } + + [Pure] + public override int GetHashCode() { + return this.val.GetHashCode(); + } + + [Pure] + public override string/*!*/ ToString() { + Contract.Ensures(Contract.Result() != null); + return cce.NonNull(val.ToString()); + } + + ////////////////////////////////////////////////////////////////////////////// + // Very limited support for format strings + // Note: Negative integers are linearised with a minus "-" in hexadecimal, + // not in 2-complement notation (in contrast to what the method + // int32.ToString(format) does) + + [Pure] + public string/*!*/ ToString(string/*!*/ format) { + Contract.Requires(format != null); + Contract.Ensures(Contract.Result() != null); + if (format.StartsWith("d") || format.StartsWith("D")) { + string res = this.Abs.ToString(); + Contract.Assert(res != null); + return addMinus(this.Signum, + prefixWithZeros(extractPrecision(format), res)); + } else if (format.StartsWith("x") || format.StartsWith("X")) { + string res = this.toHex(format.Substring(0, 1)); + Contract.Assert(res != null); + return addMinus(this.Signum, + prefixWithZeros(extractPrecision(format), res)); + } else { + throw new FormatException("Format " + format + " is not supported"); + } + } + + private static readonly System.Numerics.BigInteger BI_2_TO_24 = new BIM(0x1000000); + + [Pure] + private string/*!*/ toHex(string/*!*/ format) { + Contract.Requires(format != null); + Contract.Ensures(Contract.Result() != null); + string res = ""; + System.Numerics.BigInteger rem = this.Abs.val; + + while (rem > BIM.Zero) { + res = ((int)(rem % BI_2_TO_24)).ToString(format) + res; + rem = rem / BI_2_TO_24; + } + + return res; + } + + [Pure] + private int extractPrecision(string/*!*/ format) { + Contract.Requires(format != null); + if (format.Length > 1) + // will throw a FormatException if the precision is invalid; + // that is ok + return Int32.Parse(format.Substring(1)); + // always output at least one digit + return 1; + } + + [Pure] + private string/*!*/ addMinus(int signum, string/*!*/ suffix) { + Contract.Requires(suffix != null); + Contract.Ensures(Contract.Result() != null); + if (signum < 0) + return "-" + suffix; + return suffix; + } + + [Pure] + private string/*!*/ prefixWithZeros(int minLength, string/*!*/ suffix) { + Contract.Requires(suffix != null); + Contract.Ensures(Contract.Result() != null); + StringBuilder res = new StringBuilder(); + while (res.Length + suffix.Length < minLength) + res.Append("0"); + res.Append(suffix); + return res.ToString(); + } + + //////////////////////////////////////////////////////////////////////////// + // Basic arithmetic operations + + public BigNum Abs { + get { + return new BigNum(BIM.Abs(this.val)); + } + } + + public BigNum Neg { + get { + return new BigNum(-this.val); + } + } + + [Pure] + public static BigNum operator -(BigNum x) { + return x.Neg; + } + + [Pure] + public static BigNum operator +(BigNum x, BigNum y) { + return new BigNum(x.val + y.val); + } + + [Pure] + public static BigNum operator -(BigNum x, BigNum y) { + return new BigNum(x.val - y.val); + } + + [Pure] + public static BigNum operator *(BigNum x, BigNum y) { + return new BigNum(x.val * y.val); + } + + // TODO: check that this has a proper semantics (which? :-)) + [Pure] + public static BigNum operator /(BigNum x, BigNum y) { + return new BigNum(x.val / y.val); + } + + // TODO: check that this has a proper semantics (which? :-)) + [Pure] + public static BigNum operator %(BigNum x, BigNum y) { + return new BigNum(x.val - ((x.val / y.val) * y.val)); + } + + [Pure] + public BigNum Min(BigNum that) { + return new BigNum(this.val <= that.val ? this.val : that.val); + } + + [Pure] + public BigNum Max(BigNum that) { + return new BigNum(this.val >= that.val ? this.val : that.val); + } + + /// + /// Returns the greatest common divisor of this and _y. + /// + /// + /// + public BigNum Gcd(BigNum _y) { + Contract.Ensures(!Contract.Result().IsNegative); + BigNum x = this.Abs; + BigNum y = _y.Abs; + + while (true) { + if (x < y) { + y = y % x; + if (y.IsZero) { + return x; + } + } else { + x = x % y; + if (x.IsZero) { + return y; + } + } + } + } + + //////////////////////////////////////////////////////////////////////////// + // Some basic comparison operations + + public int Signum { + get { + return this.val.Sign; + } + } + + public bool IsPositive { + get { + return (this.val > BIM.Zero); + } + } + + public bool IsNegative { + get { + return (this.val < BIM.Zero); + } + } + + public bool IsZero { + get { + return this.val.IsZero; + } + } + + [Pure] + public int CompareTo(BigNum that) { + if (this.val == that.val) + return 0; + if (this.val < that.val) + return -1; + return 1; + } + + [Pure] + public static bool operator <(BigNum x, BigNum y) { + return (x.val < y.val); + } + + [Pure] + public static bool operator >(BigNum x, BigNum y) { + return (x.val > y.val); + } + + [Pure] + public static bool operator <=(BigNum x, BigNum y) { + return (x.val <= y.val); + } + + [Pure] + public static bool operator >=(BigNum x, BigNum y) { + return (x.val >= y.val); + } + + + private static readonly System.Numerics.BigInteger MaxInt32 = + new BIM(Int32.MaxValue); + private static readonly System.Numerics.BigInteger MinInt32 = + new BIM(Int32.MinValue); + + public bool InInt32 { + get { + return (val >= MinInt32) && (val <= MaxInt32); + } + } + } +} diff --git a/Source/Basetypes/Rational.cs b/Source/Basetypes/Rational.cs index cd0eddce..ef59cf4f 100644 --- a/Source/Basetypes/Rational.cs +++ b/Source/Basetypes/Rational.cs @@ -1,248 +1,248 @@ -//----------------------------------------------------------------------------- -// -// Copyright (C) Microsoft Corporation. All Rights Reserved. -// -//----------------------------------------------------------------------------- -using System; -using System.Diagnostics.Contracts; - -namespace Microsoft.Basetypes { - /// - /// The representation of a rational number. - /// - public struct Rational { - public static readonly Rational ZERO = Rational.FromInts(0, 1); - public static readonly Rational ONE = Rational.FromInts(1, 1); - public static readonly Rational MINUS_ONE = Rational.FromInts(-1, 1); - - private BigNum numerator, denominator; - - // int numerator; - // int denominator; - - - // invariant: 0 < denominator || (numerator == 0 && denominator == 0); - // invariant: numerator != 0 ==> gcd(abs(numerator),denominator) == 1; - // invariant: numerator == 0 ==> denominator == 1 || denominator == 0; - - public static Rational FromInt(int x) { - return FromBignum(BigNum.FromInt(x)); - } - - public static Rational FromBignum(BigNum n) - { - return new Rational(n, BigNum.ONE); - } - - private Rational(BigNum num, BigNum den) - { - Contract.Assert(den.Signum > 0); - Contract.Assert(num == BigNum.ZERO || num.Gcd(den) == BigNum.ONE); - numerator = num; - denominator = den; - } - - public static Rational FromBignums(BigNum num, BigNum den) { - Contract.Assert(!den.IsZero); - if (num == BigNum.ZERO) - return ZERO; - if (den.Signum < 0) { - den = -den; - num = -num; - } - if (den == BigNum.ONE) - return new Rational(num, den); - var gcd = num.Gcd(den); - if (gcd == BigNum.ONE) - return new Rational(num, den); - return new Rational(num / gcd, den / gcd); - } - - public static Rational FromInts(int num, int den) { - return FromBignums(BigNum.FromInt(num), BigNum.FromInt(den)); - } - - /// - /// Returns the absolute value of the rational. - /// - public Rational Abs() { - Contract.Ensures(Contract.Result().IsNonNegative); - if (IsNonNegative) { - return this; - } else { - return -this; - } - } - - /// - /// Returns a rational whose numerator and denominator, resepctively, are the Gcd - /// of the numerators and denominators of r and s. If one of r and s is 0, the absolute - /// value of the other is returned. If both are 0, 1 is returned. - /// - public static Rational Gcd(Rational r, Rational s) { - Contract.Ensures(Contract.Result().IsPositive); - if (r.IsZero) { - if (s.IsZero) { - return ONE; - } else { - return s.Abs(); - } - } else if (s.IsZero) { - return r.Abs(); - } else { - return new Rational(r.Numerator.Gcd(s.Numerator), - r.Denominator.Gcd(s.Denominator)); - } - } - - public BigNum Numerator { get { return numerator; } } - public BigNum Denominator { get { return denominator == BigNum.ZERO ? BigNum.ONE : denominator; } } - - public override string/*!*/ ToString() { - Contract.Ensures(Contract.Result() != null); - return String.Format("{0}/{1}", Numerator, Denominator); - } - - - public static bool operator ==(Rational r, Rational s) { - return r.Numerator == s.Numerator && r.Denominator == s.Denominator; - } - - public static bool operator !=(Rational r, Rational s) { - return !(r == s); - } - - public override bool Equals(object obj) { - if (obj == null) - return false; - return obj is Rational && (Rational)obj == this; - } - - public override int GetHashCode() { - return this.Numerator.GetHashCode() * 13 + this.Denominator.GetHashCode(); - } - - public int Signum { - get { - return this.Numerator.Signum; - } - } - - public bool IsZero { - get { - return Signum == 0; - } - } - - public bool IsNonZero { - get { - return Signum != 0; - } - } - - public bool IsIntegral { - get { - return Denominator == BigNum.ONE; - } - } - - - [Pure] - [Reads(ReadsAttribute.Reads.Nothing)] - public bool HasValue(int n) { - return this == FromInt(n); - } - - /// - /// Returns the rational as an integer. Requires the rational to be integral. - /// - public int AsInteger { - get { - Contract.Assert(this.IsIntegral); - return Numerator.ToIntSafe; - } - } - - public BigNum AsBigNum { - get { - Contract.Assert(this.IsIntegral); - return Numerator; - } - } - - public double AsDouble { - [Pure] - get { - if (this.IsZero) { - return 0.0; - } else { - return (double)Numerator.ToIntSafe / (double)Denominator.ToIntSafe; - } - } - } - - public bool IsNegative { - [Pure] - get { - return Signum < 0; - } - } - - public bool IsPositive { - [Pure] - get { - return 0 < Signum; - } - } - - public bool IsNonNegative { - [Pure] - get { - return 0 <= Signum; - } - } - - public static Rational operator -(Rational r) - { - return new Rational(-r.Numerator, r.Denominator); - } - - public static Rational operator /(Rational r, Rational s) - { - return FromBignums(r.Numerator * s.Denominator, r.Denominator * s.Numerator); - } - - public static Rational operator -(Rational r, Rational s) - { - return r + (-s); - } - - public static Rational operator +(Rational r, Rational s) - { - return FromBignums(r.Numerator * s.Denominator + s.Numerator * r.Denominator, r.Denominator * s.Denominator); - } - - public static Rational operator *(Rational r, Rational s) - { - return FromBignums(r.Numerator * s.Numerator, r.Denominator * s.Denominator); - } - - public static bool operator <(Rational r, Rational s) - { - return (r - s).Signum < 0; - } - - public static bool operator <=(Rational r, Rational s) - { - return !(r > s); - } - - public static bool operator >=(Rational r, Rational s) { - return !(r < s); - } - - public static bool operator >(Rational r, Rational s) { - return s < r; - } - } -} +//----------------------------------------------------------------------------- +// +// Copyright (C) Microsoft Corporation. All Rights Reserved. +// +//----------------------------------------------------------------------------- +using System; +using System.Diagnostics.Contracts; + +namespace Microsoft.Basetypes { + /// + /// The representation of a rational number. + /// + public struct Rational { + public static readonly Rational ZERO = Rational.FromInts(0, 1); + public static readonly Rational ONE = Rational.FromInts(1, 1); + public static readonly Rational MINUS_ONE = Rational.FromInts(-1, 1); + + private BigNum numerator, denominator; + + // int numerator; + // int denominator; + + + // invariant: 0 < denominator || (numerator == 0 && denominator == 0); + // invariant: numerator != 0 ==> gcd(abs(numerator),denominator) == 1; + // invariant: numerator == 0 ==> denominator == 1 || denominator == 0; + + public static Rational FromInt(int x) { + return FromBignum(BigNum.FromInt(x)); + } + + public static Rational FromBignum(BigNum n) + { + return new Rational(n, BigNum.ONE); + } + + private Rational(BigNum num, BigNum den) + { + Contract.Assert(den.Signum > 0); + Contract.Assert(num == BigNum.ZERO || num.Gcd(den) == BigNum.ONE); + numerator = num; + denominator = den; + } + + public static Rational FromBignums(BigNum num, BigNum den) { + Contract.Assert(!den.IsZero); + if (num == BigNum.ZERO) + return ZERO; + if (den.Signum < 0) { + den = -den; + num = -num; + } + if (den == BigNum.ONE) + return new Rational(num, den); + var gcd = num.Gcd(den); + if (gcd == BigNum.ONE) + return new Rational(num, den); + return new Rational(num / gcd, den / gcd); + } + + public static Rational FromInts(int num, int den) { + return FromBignums(BigNum.FromInt(num), BigNum.FromInt(den)); + } + + /// + /// Returns the absolute value of the rational. + /// + public Rational Abs() { + Contract.Ensures(Contract.Result().IsNonNegative); + if (IsNonNegative) { + return this; + } else { + return -this; + } + } + + /// + /// Returns a rational whose numerator and denominator, resepctively, are the Gcd + /// of the numerators and denominators of r and s. If one of r and s is 0, the absolute + /// value of the other is returned. If both are 0, 1 is returned. + /// + public static Rational Gcd(Rational r, Rational s) { + Contract.Ensures(Contract.Result().IsPositive); + if (r.IsZero) { + if (s.IsZero) { + return ONE; + } else { + return s.Abs(); + } + } else if (s.IsZero) { + return r.Abs(); + } else { + return new Rational(r.Numerator.Gcd(s.Numerator), + r.Denominator.Gcd(s.Denominator)); + } + } + + public BigNum Numerator { get { return numerator; } } + public BigNum Denominator { get { return denominator == BigNum.ZERO ? BigNum.ONE : denominator; } } + + public override string/*!*/ ToString() { + Contract.Ensures(Contract.Result() != null); + return String.Format("{0}/{1}", Numerator, Denominator); + } + + + public static bool operator ==(Rational r, Rational s) { + return r.Numerator == s.Numerator && r.Denominator == s.Denominator; + } + + public static bool operator !=(Rational r, Rational s) { + return !(r == s); + } + + public override bool Equals(object obj) { + if (obj == null) + return false; + return obj is Rational && (Rational)obj == this; + } + + public override int GetHashCode() { + return this.Numerator.GetHashCode() * 13 + this.Denominator.GetHashCode(); + } + + public int Signum { + get { + return this.Numerator.Signum; + } + } + + public bool IsZero { + get { + return Signum == 0; + } + } + + public bool IsNonZero { + get { + return Signum != 0; + } + } + + public bool IsIntegral { + get { + return Denominator == BigNum.ONE; + } + } + + + [Pure] + [Reads(ReadsAttribute.Reads.Nothing)] + public bool HasValue(int n) { + return this == FromInt(n); + } + + /// + /// Returns the rational as an integer. Requires the rational to be integral. + /// + public int AsInteger { + get { + Contract.Assert(this.IsIntegral); + return Numerator.ToIntSafe; + } + } + + public BigNum AsBigNum { + get { + Contract.Assert(this.IsIntegral); + return Numerator; + } + } + + public double AsDouble { + [Pure] + get { + if (this.IsZero) { + return 0.0; + } else { + return (double)Numerator.ToIntSafe / (double)Denominator.ToIntSafe; + } + } + } + + public bool IsNegative { + [Pure] + get { + return Signum < 0; + } + } + + public bool IsPositive { + [Pure] + get { + return 0 < Signum; + } + } + + public bool IsNonNegative { + [Pure] + get { + return 0 <= Signum; + } + } + + public static Rational operator -(Rational r) + { + return new Rational(-r.Numerator, r.Denominator); + } + + public static Rational operator /(Rational r, Rational s) + { + return FromBignums(r.Numerator * s.Denominator, r.Denominator * s.Numerator); + } + + public static Rational operator -(Rational r, Rational s) + { + return r + (-s); + } + + public static Rational operator +(Rational r, Rational s) + { + return FromBignums(r.Numerator * s.Denominator + s.Numerator * r.Denominator, r.Denominator * s.Denominator); + } + + public static Rational operator *(Rational r, Rational s) + { + return FromBignums(r.Numerator * s.Numerator, r.Denominator * s.Denominator); + } + + public static bool operator <(Rational r, Rational s) + { + return (r - s).Signum < 0; + } + + public static bool operator <=(Rational r, Rational s) + { + return !(r > s); + } + + public static bool operator >=(Rational r, Rational s) { + return !(r < s); + } + + public static bool operator >(Rational r, Rational s) { + return s < r; + } + } +} diff --git a/Source/Basetypes/Set.cs b/Source/Basetypes/Set.cs index dfd65b4b..0cc1d103 100644 --- a/Source/Basetypes/Set.cs +++ b/Source/Basetypes/Set.cs @@ -1,286 +1,286 @@ -//----------------------------------------------------------------------------- -// -// Copyright (C) Microsoft Corporation. All Rights Reserved. -// -//----------------------------------------------------------------------------- -namespace Microsoft.Boogie { - using System; - using System.IO; - using System.Collections; - using System.Collections.Generic; - using System.Diagnostics.Contracts; - - /// - /// A class representing a mathematical set. - /// - public class GSet : ICloneable, IEnumerable, IEnumerable { - /*[Own]*/ - Dictionary ht; - List arr; // keep elements in a well-defined order; otherwise iteration is non-deterministic - - [ContractInvariantMethod] - void ObjectInvariant() { - Contract.Invariant(ht != null); - Contract.Invariant(arr != null); - Contract.Invariant(ht.Count == arr.Count); - } - - - public GSet() { - ht = new Dictionary(); - arr = new List(); - //:base(); - } - - private GSet(Dictionary/*!*/ ht, List arr) { - Contract.Requires(ht != null); - Contract.Requires(arr != null); - this.ht = ht; - this.arr = arr; - //:base(); - } - - public GSet(int capacity) { - ht = new Dictionary(capacity); - arr = new List(capacity); - //:base(); - } - - - public readonly static GSet/*!*/ Empty = new GSet(); - - public void Clear() { - ht.Clear(); - arr.Clear(); - } - - /// - /// This method idempotently adds "o" to the set. - /// In notation: - /// this.SetElements = this.SetElements_old \union {o}; - /// - public void Add(T o) { - if (!ht.ContainsKey(o)) { - ht[o] = arr.Count; - arr.Add(o); - } - } - - /// - /// this.SetElements = this.SetElements_old \union s.GSetElements; - /// - public void AddRange(IEnumerable s) { - foreach (T o in s) { - Add(o); - } - } - - /// - /// this.SetElements = this.SetElements_old \setminus {o}; - /// - public void Remove(T o) { - int idx; - if (ht.TryGetValue(o, out idx)) { - var last = arr[arr.Count - 1]; - arr.RemoveAt(arr.Count - 1); - if (idx != arr.Count) { - arr[idx] = last; - ht[last] = idx; - } - ht.Remove(o); - } - } - - /// - /// this.SetElements = this.SetElements_old \setminus s.SetElements; - /// - public void RemoveRange(IEnumerable s) { - Contract.Requires(s != null); - if (s == this) { - ht.Clear(); - arr.Clear(); - } else { - foreach (T o in s) { - Remove(o); - } - } - } - - /// - /// Returns an arbitrary element from the set. - /// - public T Choose() { - Contract.Requires((Count > 0)); - foreach(var e in this) - return e; - return default(T); - } - - /// - /// Picks an arbitrary element from the set, removes it, and returns it. - /// - public T Take() { - Contract.Requires((Count > 0)); - Contract.Ensures(Count == Contract.OldValue(Count) - 1); - T r = Choose(); - Remove(r); - return r; - } - - public void Intersect(GSet/*!*/ s) { - Contract.Requires(s != null); - if (s == this) return; - ht.Clear(); - var newArr = new List(); - foreach (T key in arr) { - if (s.ht.ContainsKey(key)) { - ht[key] = newArr.Count; - newArr.Add(key); - } - } - arr = newArr; - } - - /// - /// The getter returns true iff "o" is in the set. - /// The setter adds the value "o" (for "true") or removes "o" (for "false") - /// - public bool this[T o] { - get { - return ht.ContainsKey(o); - } - set { - if (value) { - Add(o); - } else { - Remove(o); - } - } - } - - /// - /// Returns true iff "o" is an element of "this". - /// - /// - /// - [Pure] - public bool Contains(T o) { - return this.ht.ContainsKey(o); - } - - /// - /// Returns true iff every element of "s" is an element of "this", that is, if - /// "s" is a subset of "this". - /// - /// - /// - public bool ContainsRange(IEnumerable s) { - Contract.Requires(s != null); - if (s != this) { - foreach (T key in s) { - if (!this.ht.ContainsKey(key)) { - return false; - } - } - } - return true; - } - - public object/*!*/ Clone() { - Contract.Ensures(Contract.Result() != null); - return new GSet(new Dictionary(ht), new List(arr)); - } - - public virtual int Count { - get { - return ht.Count; - } - } - - [Pure] - public override string/*!*/ ToString() { - Contract.Ensures(Contract.Result() != null); - string s = null; - foreach (object/*!*/ key in ht.Keys) { - Contract.Assert(key != null); - if (s == null) { - s = "{"; - } else { - s += ", "; - } - s += key.ToString(); - } - if (s == null) { - return "{}"; - } else { - return s + "}"; - } - } - - //----------------------------- Static Methods --------------------------------- - - // Functional Intersect - public static GSet/*!*/ Intersect(GSet/*!*/ a, GSet/*!*/ b) { - Contract.Requires(b != null); - Contract.Requires(a != null); - Contract.Ensures(Contract.Result>() != null); - //Contract.Ensures(Contract.ForAll(result, x => a[x] && b[x] )); - GSet/*!*/ res = (GSet/*!*/)cce.NonNull(a.Clone()); - res.Intersect(b); - return res; - } - // Functional Union - public static GSet/*!*/ Union(GSet/*!*/ a, GSet/*!*/ b) { - Contract.Requires(a != null); - Contract.Requires(b != null); - Contract.Ensures(Contract.Result>() != null); - // Contract.Ensures(Contract.ForAll(result, x => a[x] || b[x] )); - GSet/*!*/ res = (GSet/*!*/)cce.NonNull(a.Clone()); - res.AddRange(b); - return res; - } - - public delegate bool SetFilter(object/*!*/ obj); - - public static GSet/*!*/ Filter(GSet/*!*/ a, Func filter) { - Contract.Requires(filter != null); - Contract.Requires(a != null); - Contract.Ensures(Contract.Result>() != null); - GSet inter = new GSet(); - - foreach (T elem in a) { - Contract.Assert(elem != null); - if (filter(elem)) { - inter.Add(elem); - } - } - return inter; - } - - public IEnumerator GetEnumerator() - { - return arr.GetEnumerator(); - } - - IEnumerator IEnumerable.GetEnumerator() - { - return ((IEnumerable)arr).GetEnumerator(); - } - - public bool AddAll(IEnumerable s) - { - foreach (T e in s) Add(e); - return true; - } - } - - - public interface IWorkList : ICollection { - bool Add(object o); - bool AddAll(IEnumerable objs); - bool IsEmpty(); - object Pull(); - } - - +//----------------------------------------------------------------------------- +// +// Copyright (C) Microsoft Corporation. All Rights Reserved. +// +//----------------------------------------------------------------------------- +namespace Microsoft.Boogie { + using System; + using System.IO; + using System.Collections; + using System.Collections.Generic; + using System.Diagnostics.Contracts; + + /// + /// A class representing a mathematical set. + /// + public class GSet : ICloneable, IEnumerable, IEnumerable { + /*[Own]*/ + Dictionary ht; + List arr; // keep elements in a well-defined order; otherwise iteration is non-deterministic + + [ContractInvariantMethod] + void ObjectInvariant() { + Contract.Invariant(ht != null); + Contract.Invariant(arr != null); + Contract.Invariant(ht.Count == arr.Count); + } + + + public GSet() { + ht = new Dictionary(); + arr = new List(); + //:base(); + } + + private GSet(Dictionary/*!*/ ht, List arr) { + Contract.Requires(ht != null); + Contract.Requires(arr != null); + this.ht = ht; + this.arr = arr; + //:base(); + } + + public GSet(int capacity) { + ht = new Dictionary(capacity); + arr = new List(capacity); + //:base(); + } + + + public readonly static GSet/*!*/ Empty = new GSet(); + + public void Clear() { + ht.Clear(); + arr.Clear(); + } + + /// + /// This method idempotently adds "o" to the set. + /// In notation: + /// this.SetElements = this.SetElements_old \union {o}; + /// + public void Add(T o) { + if (!ht.ContainsKey(o)) { + ht[o] = arr.Count; + arr.Add(o); + } + } + + /// + /// this.SetElements = this.SetElements_old \union s.GSetElements; + /// + public void AddRange(IEnumerable s) { + foreach (T o in s) { + Add(o); + } + } + + /// + /// this.SetElements = this.SetElements_old \setminus {o}; + /// + public void Remove(T o) { + int idx; + if (ht.TryGetValue(o, out idx)) { + var last = arr[arr.Count - 1]; + arr.RemoveAt(arr.Count - 1); + if (idx != arr.Count) { + arr[idx] = last; + ht[last] = idx; + } + ht.Remove(o); + } + } + + /// + /// this.SetElements = this.SetElements_old \setminus s.SetElements; + /// + public void RemoveRange(IEnumerable s) { + Contract.Requires(s != null); + if (s == this) { + ht.Clear(); + arr.Clear(); + } else { + foreach (T o in s) { + Remove(o); + } + } + } + + /// + /// Returns an arbitrary element from the set. + /// + public T Choose() { + Contract.Requires((Count > 0)); + foreach(var e in this) + return e; + return default(T); + } + + /// + /// Picks an arbitrary element from the set, removes it, and returns it. + /// + public T Take() { + Contract.Requires((Count > 0)); + Contract.Ensures(Count == Contract.OldValue(Count) - 1); + T r = Choose(); + Remove(r); + return r; + } + + public void Intersect(GSet/*!*/ s) { + Contract.Requires(s != null); + if (s == this) return; + ht.Clear(); + var newArr = new List(); + foreach (T key in arr) { + if (s.ht.ContainsKey(key)) { + ht[key] = newArr.Count; + newArr.Add(key); + } + } + arr = newArr; + } + + /// + /// The getter returns true iff "o" is in the set. + /// The setter adds the value "o" (for "true") or removes "o" (for "false") + /// + public bool this[T o] { + get { + return ht.ContainsKey(o); + } + set { + if (value) { + Add(o); + } else { + Remove(o); + } + } + } + + /// + /// Returns true iff "o" is an element of "this". + /// + /// + /// + [Pure] + public bool Contains(T o) { + return this.ht.ContainsKey(o); + } + + /// + /// Returns true iff every element of "s" is an element of "this", that is, if + /// "s" is a subset of "this". + /// + /// + /// + public bool ContainsRange(IEnumerable s) { + Contract.Requires(s != null); + if (s != this) { + foreach (T key in s) { + if (!this.ht.ContainsKey(key)) { + return false; + } + } + } + return true; + } + + public object/*!*/ Clone() { + Contract.Ensures(Contract.Result() != null); + return new GSet(new Dictionary(ht), new List(arr)); + } + + public virtual int Count { + get { + return ht.Count; + } + } + + [Pure] + public override string/*!*/ ToString() { + Contract.Ensures(Contract.Result() != null); + string s = null; + foreach (object/*!*/ key in ht.Keys) { + Contract.Assert(key != null); + if (s == null) { + s = "{"; + } else { + s += ", "; + } + s += key.ToString(); + } + if (s == null) { + return "{}"; + } else { + return s + "}"; + } + } + + //----------------------------- Static Methods --------------------------------- + + // Functional Intersect + public static GSet/*!*/ Intersect(GSet/*!*/ a, GSet/*!*/ b) { + Contract.Requires(b != null); + Contract.Requires(a != null); + Contract.Ensures(Contract.Result>() != null); + //Contract.Ensures(Contract.ForAll(result, x => a[x] && b[x] )); + GSet/*!*/ res = (GSet/*!*/)cce.NonNull(a.Clone()); + res.Intersect(b); + return res; + } + // Functional Union + public static GSet/*!*/ Union(GSet/*!*/ a, GSet/*!*/ b) { + Contract.Requires(a != null); + Contract.Requires(b != null); + Contract.Ensures(Contract.Result>() != null); + // Contract.Ensures(Contract.ForAll(result, x => a[x] || b[x] )); + GSet/*!*/ res = (GSet/*!*/)cce.NonNull(a.Clone()); + res.AddRange(b); + return res; + } + + public delegate bool SetFilter(object/*!*/ obj); + + public static GSet/*!*/ Filter(GSet/*!*/ a, Func filter) { + Contract.Requires(filter != null); + Contract.Requires(a != null); + Contract.Ensures(Contract.Result>() != null); + GSet inter = new GSet(); + + foreach (T elem in a) { + Contract.Assert(elem != null); + if (filter(elem)) { + inter.Add(elem); + } + } + return inter; + } + + public IEnumerator GetEnumerator() + { + return arr.GetEnumerator(); + } + + IEnumerator IEnumerable.GetEnumerator() + { + return ((IEnumerable)arr).GetEnumerator(); + } + + public bool AddAll(IEnumerable s) + { + foreach (T e in s) Add(e); + return true; + } + } + + + public interface IWorkList : ICollection { + bool Add(object o); + bool AddAll(IEnumerable objs); + bool IsEmpty(); + object Pull(); + } + + } \ No newline at end of file diff --git a/Source/Basetypes/cce.cs b/Source/Basetypes/cce.cs index ef594484..1e0b12a5 100644 --- a/Source/Basetypes/cce.cs +++ b/Source/Basetypes/cce.cs @@ -1,193 +1,193 @@ -using System; -using SA=System.Attribute; -using System.Collections.Generic; -using System.Diagnostics.Contracts; -using System.Text; -//using Microsoft.Boogie; - -/// -/// A class containing static methods to extend the functionality of Code Contracts -/// - -public static class cce { - //[Pure] - //public static bool NonNullElements(Microsoft.Dafny.Graph collection) { - // return collection != null && cce.NonNullElements(collection.TopologicallySortedComponents()); - //} - [Pure] - public static T NonNull(T t) { - Contract.Assert(t != null); - return t; - } - [Pure] - public static bool NonNullElements(IEnumerable collection) { - return collection != null && Contract.ForAll(collection, c => c != null); - } - [Pure] - public static bool NonNullElements(IDictionary collection) { - return collection != null && Contract.ForAll(collection, pair => NonNullElements(pair)); - } - //[Pure] - //public static bool NonNullElements(VariableSeq collection) { - // return collection != null && Contract.ForAll(0, collection.Length, i => collection[i] != null); - //} - /// - /// For possibly-null lists of non-null elements - /// - /// - /// - /// If true, the collection is treated as an IEnumerable<T!>?, rather than an IEnumerable<T!>! - /// - [Pure] - public static bool NonNullElements(IEnumerable collection, bool nullability) { - return (nullability && collection == null) || cce.NonNullElements(collection); - //Should be the same as: - /*if(nullability&&collection==null) - * return true; - * return cce.NonNullElements(collection) - */ - - } - [Pure] - public static bool NonNullElements(KeyValuePair kvp) { - return kvp.Key != null && kvp.Value != null; - } - [Pure] - public static bool NonNullElements(IEnumerator iEnumerator) { - return iEnumerator != null; - } - //[Pure] - //public static bool NonNullElements(Graphing.Graph graph) { - // return cce.NonNullElements(graph.TopologicalSort()); - //} - [Pure] - public static void BeginExpose(object o) { - } - [Pure] - public static void EndExpose() { - } - [Pure] - public static bool IsPeerConsistent(object o) { - return true; - } - [Pure] - public static bool IsConsistent(object o) { - return true; - } - [Pure] - public static bool IsExposable(object o) { - return true; - } - [Pure] - public static bool IsExposed(object o) { - return true; - } - [Pure] - public static bool IsNew(object o) { - return true; - } - public static class Owner { - [Pure] - public static bool Same(object o, object p) { - return true; - } - [Pure] - public static void AssignSame(object o, object p) { - } - [Pure] - public static object ElementProxy(object o) { - return o; - } - [Pure] - public static bool None(object o) { - return true; - } - [Pure] - public static bool Different(object o, object p) { - return true; - } - [Pure] - public static bool New(object o) { - return true; - } - } - [Pure] - public static void LoopInvariant(bool p) { - Contract.Assert(p); - } - public class UnreachableException : Exception { - public UnreachableException() { - } - } - //[Pure] - //public static bool IsValid(Microsoft.Dafny.Expression expression) { - // return true; - //} - //public static List toList(PureCollections.Sequence s) { - // List toRet = new List(); - // foreach (T t in s.elems) - // if(t!=null) - // toRet.Add(t); - // return toRet; - //} - - //internal static bool NonNullElements(Set set) { - // return set != null && Contract.ForAll(0,set.Count, i => set[i] != null); - //} -} - -public class PeerAttribute : SA { -} -public class RepAttribute : SA { -} -public class CapturedAttribute : SA { -} -public class NotDelayedAttribute : SA { -} -public class NoDefaultContractAttribute : SA { -} -public class VerifyAttribute : SA { - public VerifyAttribute(bool b) { - - } -} -public class StrictReadonlyAttribute : SA { -} -public class AdditiveAttribute : SA { -} -public class ReadsAttribute : SA { - public enum Reads { - Nothing, - Everything, - }; - public ReadsAttribute(object o) { - } -} -public class GlobalAccessAttribute : SA { - public GlobalAccessAttribute(bool b) { - } -} -public class EscapesAttribute : SA { - public EscapesAttribute(bool b, bool b_2) { - } -} -public class NeedsContractsAttribute : SA { - public NeedsContractsAttribute() { - } - public NeedsContractsAttribute(bool ret, bool parameters) { - } - public NeedsContractsAttribute(bool ret, int[] parameters) { - } -} -public class ImmutableAttribute : SA { -} -public class InsideAttribute : SA { -} -public class SpecPublicAttribute : SA { -} -public class ElementsPeerAttribute : SA { -} -public class ResultNotNewlyAllocatedAttribute : SA { -} -public class OnceAttribute : SA { +using System; +using SA=System.Attribute; +using System.Collections.Generic; +using System.Diagnostics.Contracts; +using System.Text; +//using Microsoft.Boogie; + +/// +/// A class containing static methods to extend the functionality of Code Contracts +/// + +public static class cce { + //[Pure] + //public static bool NonNullElements(Microsoft.Dafny.Graph collection) { + // return collection != null && cce.NonNullElements(collection.TopologicallySortedComponents()); + //} + [Pure] + public static T NonNull(T t) { + Contract.Assert(t != null); + return t; + } + [Pure] + public static bool NonNullElements(IEnumerable collection) { + return collection != null && Contract.ForAll(collection, c => c != null); + } + [Pure] + public static bool NonNullElements(IDictionary collection) { + return collection != null && Contract.ForAll(collection, pair => NonNullElements(pair)); + } + //[Pure] + //public static bool NonNullElements(VariableSeq collection) { + // return collection != null && Contract.ForAll(0, collection.Length, i => collection[i] != null); + //} + /// + /// For possibly-null lists of non-null elements + /// + /// + /// + /// If true, the collection is treated as an IEnumerable<T!>?, rather than an IEnumerable<T!>! + /// + [Pure] + public static bool NonNullElements(IEnumerable collection, bool nullability) { + return (nullability && collection == null) || cce.NonNullElements(collection); + //Should be the same as: + /*if(nullability&&collection==null) + * return true; + * return cce.NonNullElements(collection) + */ + + } + [Pure] + public static bool NonNullElements(KeyValuePair kvp) { + return kvp.Key != null && kvp.Value != null; + } + [Pure] + public static bool NonNullElements(IEnumerator iEnumerator) { + return iEnumerator != null; + } + //[Pure] + //public static bool NonNullElements(Graphing.Graph graph) { + // return cce.NonNullElements(graph.TopologicalSort()); + //} + [Pure] + public static void BeginExpose(object o) { + } + [Pure] + public static void EndExpose() { + } + [Pure] + public static bool IsPeerConsistent(object o) { + return true; + } + [Pure] + public static bool IsConsistent(object o) { + return true; + } + [Pure] + public static bool IsExposable(object o) { + return true; + } + [Pure] + public static bool IsExposed(object o) { + return true; + } + [Pure] + public static bool IsNew(object o) { + return true; + } + public static class Owner { + [Pure] + public static bool Same(object o, object p) { + return true; + } + [Pure] + public static void AssignSame(object o, object p) { + } + [Pure] + public static object ElementProxy(object o) { + return o; + } + [Pure] + public static bool None(object o) { + return true; + } + [Pure] + public static bool Different(object o, object p) { + return true; + } + [Pure] + public static bool New(object o) { + return true; + } + } + [Pure] + public static void LoopInvariant(bool p) { + Contract.Assert(p); + } + public class UnreachableException : Exception { + public UnreachableException() { + } + } + //[Pure] + //public static bool IsValid(Microsoft.Dafny.Expression expression) { + // return true; + //} + //public static List toList(PureCollections.Sequence s) { + // List toRet = new List(); + // foreach (T t in s.elems) + // if(t!=null) + // toRet.Add(t); + // return toRet; + //} + + //internal static bool NonNullElements(Set set) { + // return set != null && Contract.ForAll(0,set.Count, i => set[i] != null); + //} +} + +public class PeerAttribute : SA { +} +public class RepAttribute : SA { +} +public class CapturedAttribute : SA { +} +public class NotDelayedAttribute : SA { +} +public class NoDefaultContractAttribute : SA { +} +public class VerifyAttribute : SA { + public VerifyAttribute(bool b) { + + } +} +public class StrictReadonlyAttribute : SA { +} +public class AdditiveAttribute : SA { +} +public class ReadsAttribute : SA { + public enum Reads { + Nothing, + Everything, + }; + public ReadsAttribute(object o) { + } +} +public class GlobalAccessAttribute : SA { + public GlobalAccessAttribute(bool b) { + } +} +public class EscapesAttribute : SA { + public EscapesAttribute(bool b, bool b_2) { + } +} +public class NeedsContractsAttribute : SA { + public NeedsContractsAttribute() { + } + public NeedsContractsAttribute(bool ret, bool parameters) { + } + public NeedsContractsAttribute(bool ret, int[] parameters) { + } +} +public class ImmutableAttribute : SA { +} +public class InsideAttribute : SA { +} +public class SpecPublicAttribute : SA { +} +public class ElementsPeerAttribute : SA { +} +public class ResultNotNewlyAllocatedAttribute : SA { +} +public class OnceAttribute : SA { } \ No newline at end of file -- cgit v1.2.3