diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs index 68cca046e..1e9bd1323 100644 --- a/src/api/dotnet/Context.cs +++ b/src/api/dotnet/Context.cs @@ -3428,6 +3428,371 @@ namespace Microsoft.Z3 } #endregion + #region Floating-Point Arithmetic + /// + /// Create a floating point rounding mode sort. + /// + public FPRMSort MkFPRMSort() + { + Contract.Ensures(Contract.Result() != null); + return new FPRMSort(this); + } + + /// + /// Create a NearestTiesToEven rounding mode numeral. + /// + public FPRMNum MkFPRMNearestTiesToEven() + { + Contract.Ensures(Contract.Result() != null); + return new FPRMNum(this, Native.Z3_mk_fpa_round_nearest_ties_to_even(nCtx)); + } + + /// + /// Create a NearestTiesToAway rounding mode numeral. + /// + public FPRMNum MkFPRMNearestTiesToAway() + { + Contract.Ensures(Contract.Result() != null); + return new FPRMNum(this, Native.Z3_mk_fpa_round_nearest_ties_to_away(nCtx)); + } + + /// + /// Create a TowardPositive rounding mode numeral. + /// + public FPRMNum MkFPRMTowardPositive() + { + Contract.Ensures(Contract.Result() != null); + return new FPRMNum(this, Native.Z3_mk_fpa_round_toward_positive(nCtx)); + } + + /// + /// Create a TowardNegative rounding mode numeral. + /// + public FPRMNum MkFPRMTowardNegative() + { + Contract.Ensures(Contract.Result() != null); + return new FPRMNum(this, Native.Z3_mk_fpa_round_toward_negative(nCtx)); + } + + /// + /// Create a TowardZero rounding mode numeral. + /// + public FPRMNum MkFPRMTowardZero() + { + Contract.Ensures(Contract.Result() != null); + return new FPRMNum(this, Native.Z3_mk_fpa_round_toward_zero(nCtx)); + } + + /// + /// Create a floating point sort. + /// + /// exponent bits in the floating point sort. + /// significand bits in the floating point sort. + public FPSort MkFPSort(uint ebits, uint sbits) + { + Contract.Ensures(Contract.Result() != null); + return new FPSort(this, ebits, sbits); + } + + /// + /// Create a floating point NaN numeral. + /// + /// A string representing the value in decimal notation. + /// floating point sort. + public FPNum MkFPNaN(double v, FPSort s) + { + Contract.Ensures(Contract.Result() != null); + return new FPNum(this, Native.Z3_mk_fpa_nan(nCtx, s.NativeObject)); + } + + /// + /// Create a floating point Inf numeral. + /// + /// A string representing the value in decimal notation. + /// floating point sort. + /// indicates whether the result should be negative. + public FPNum MkFPInf(double v, FPSort s, bool negative) + { + Contract.Ensures(Contract.Result() != null); + return new FPNum(this, Native.Z3_mk_fpa_inf(nCtx, s.NativeObject, negative ? 1 : 0)); + } + + /// + /// Create a floating point numeral. + /// + /// A string representing the value in decimal notation. + /// floating point sort + public FPNum MkFP(double v, FPSort s) + { + Contract.Ensures(Contract.Result() != null); + return new FPNum(this, Native.Z3_mk_double(this.nCtx, v, s.NativeObject)); + } + + /// + /// Floating-point absolute value + /// + /// floating point term + FPExpr MkFPAbs(FPExpr t) + { + Contract.Ensures(Contract.Result() != null); + return new FPExpr(this, Native.Z3_mk_fpa_abs(this.nCtx, t.NativeObject)); + } + + /// + /// Floating-point negation + /// + /// floating point term + FPExpr MkFPNeg(FPExpr t) + { + Contract.Ensures(Contract.Result() != null); + return new FPExpr(this, Native.Z3_mk_fpa_neg(this.nCtx, t.NativeObject)); + } + + /// + /// Floating-point addition + /// + /// rounding mode term + /// floating point term + /// floating point term + FPExpr MkFPAdd(FPRMExpr rm, FPExpr t1, FPExpr t2) + { + Contract.Ensures(Contract.Result() != null); + return new FPExpr(this, Native.Z3_mk_fpa_add(this.nCtx, rm.NativeObject, t1.NativeObject, t2.NativeObject)); + } + + /// + /// Floating-point subtraction + /// + /// rounding mode term + /// floating point term + /// floating point term + FPExpr MkFPSub(FPRMExpr rm, FPExpr t1, FPExpr t2) + { + Contract.Ensures(Contract.Result() != null); + return new FPExpr(this, Native.Z3_mk_fpa_sub(this.nCtx, rm.NativeObject, t1.NativeObject, t2.NativeObject)); + } + + /// + /// Floating-point multiplication + /// + /// rounding mode term + /// floating point term + /// floating point term + FPExpr MkFPMul(FPRMExpr rm, FPExpr t1, FPExpr t2) + { + Contract.Ensures(Contract.Result() != null); + return new FPExpr(this, Native.Z3_mk_fpa_mul(this.nCtx, rm.NativeObject, t1.NativeObject, t2.NativeObject)); + } + + /// + /// Floating-point division + /// + /// rounding mode term + /// floating point term + /// floating point term + FPExpr MkFPDiv(FPRMExpr rm, FPExpr t1, FPExpr t2) + { + Contract.Ensures(Contract.Result() != null); + return new FPExpr(this, Native.Z3_mk_fpa_div(this.nCtx, rm.NativeObject, t1.NativeObject, t2.NativeObject)); + } + + /// + /// Floating-point fused multiply-add + /// + /// + /// The result is round((t1 * t2) + t3) + /// + /// rounding mode term + /// floating point term + /// floating point term + /// floating point term + FPExpr MkFPFMA(FPRMExpr rm, FPExpr t1, FPExpr t2, FPExpr t3) + { + Contract.Ensures(Contract.Result() != null); + return new FPExpr(this, Native.Z3_mk_fpa_fma(this.nCtx, rm.NativeObject, t1.NativeObject, t2.NativeObject, t3.NativeObject)); + } + + /// + /// Floating-point square root + /// + /// floating point term + FPExpr MkFPSqrt(FPRMExpr rm, FPExpr t) + { + Contract.Ensures(Contract.Result() != null); + return new FPExpr(this, Native.Z3_mk_fpa_sqrt(this.nCtx, rm.NativeObject, t.NativeObject)); + } + + /// + /// Floating-point remainder + /// + /// floating point term + /// floating point term + FPExpr MkFPRem(FPExpr t1, FPExpr t2) + { + Contract.Ensures(Contract.Result() != null); + return new FPExpr(this, Native.Z3_mk_fpa_rem(this.nCtx, t1.NativeObject, t2.NativeObject)); + } + + /// + /// Floating-point equality + /// + /// + /// Note that this is IEEE 754 equality (as opposed to standard =). + /// + /// floating point term + /// floating point term + BoolExpr MkFPEq(FPExpr t1, FPExpr t2) + { + Contract.Ensures(Contract.Result() != null); + return new BoolExpr(this, Native.Z3_mk_fpa_eq(this.nCtx, t1.NativeObject, t2.NativeObject)); + } + + /// + /// Floating-point less than or equal + /// + /// floating point term + /// floating point term + BoolExpr MkFPLe(FPExpr t1, FPExpr t2) + { + Contract.Ensures(Contract.Result() != null); + return new BoolExpr(this, Native.Z3_mk_fpa_le(this.nCtx, t1.NativeObject, t2.NativeObject)); + } + + /// + /// Floating-point less than + /// + /// floating point term + /// floating point term + BoolExpr MkFPLt(FPExpr t1, FPExpr t2) + { + Contract.Ensures(Contract.Result() != null); + return new BoolExpr(this, Native.Z3_mk_fpa_lt(this.nCtx, t1.NativeObject, t2.NativeObject)); + } + + /// + /// Floating-point greater than or equal + /// + /// floating point term + /// floating point term + BoolExpr MkFPGe(FPExpr t1, FPExpr t2) + { + Contract.Ensures(Contract.Result() != null); + return new BoolExpr(this, Native.Z3_mk_fpa_ge(this.nCtx, t1.NativeObject, t2.NativeObject)); + } + + /// + /// Floating-point greater than + /// + /// floating point term + /// floating point term + BoolExpr MkFPGt(FPExpr t1, FPExpr t2) + { + Contract.Ensures(Contract.Result() != null); + return new BoolExpr(this, Native.Z3_mk_fpa_gt(this.nCtx, t1.NativeObject, t2.NativeObject)); + } + + /// + /// Predicate indicating whether t is a normal floating point number + /// + /// floating point term + BoolExpr MkFPIsNormal(FPExpr t) + { + Contract.Ensures(Contract.Result() != null); + return new BoolExpr(this, Native.Z3_mk_fpa_is_normal(this.nCtx, t.NativeObject)); + } + + /// + /// Predicate indicating whether t is a subnormal floating point number + /// + /// floating point term + BoolExpr MkFPIsSubnormal(FPExpr t) + { + Contract.Ensures(Contract.Result() != null); + return new BoolExpr(this, Native.Z3_mk_fpa_is_subnormal(this.nCtx, t.NativeObject)); + } + + /// + /// Predicate indicating whether t is a floating point number with zero value, i.e., +0 or -0. + /// + /// floating point term + BoolExpr MkFPIsZero(FPExpr t) + { + Contract.Ensures(Contract.Result() != null); + return new BoolExpr(this, Native.Z3_mk_fpa_is_zero(this.nCtx, t.NativeObject)); + } + + /// + /// Predicate indicating whether t is a floating point number representing +Inf or -Inf + /// + /// floating point term + BoolExpr MkFPIsInf(FPExpr t) + { + Contract.Ensures(Contract.Result() != null); + return new BoolExpr(this, Native.Z3_mk_fpa_is_inf(this.nCtx, t.NativeObject)); + } + + /// + /// Predicate indicating whether t is a NaN + /// + /// floating point term + BoolExpr MkFPIsNaN(FPExpr t) + { + Contract.Ensures(Contract.Result() != null); + return new BoolExpr(this, Native.Z3_mk_fpa_is_nan(this.nCtx, t.NativeObject)); + } + + /// + /// Floating-point minimum + /// + /// floating point term + /// floating point term + FPExpr MkFPMin(FPExpr t1, FPExpr t2) + { + Contract.Ensures(Contract.Result() != null); + return new FPExpr(this, Native.Z3_mk_fpa_min(this.nCtx, t1.NativeObject, t2.NativeObject)); + } + + /// + /// Floating-point maximium + /// + /// floating point term + /// floating point term + FPExpr MkFPMax(FPExpr t1, FPExpr t2) + { + Contract.Ensures(Contract.Result() != null); + return new FPExpr(this, Native.Z3_mk_fpa_max(this.nCtx, t1.NativeObject, t2.NativeObject)); + } + + /// + /// Conversion of a floating point number to another floating-point sort s. + /// + /// + /// Produces a term that represents the conversion of a floating-point term t to a different + /// floating point sort s. If necessary, rounding according to rm is applied. + /// + /// floating point sort + /// floating point rounding mode term + /// floating point term + FPExpr MkFPConvert(FPSort s, FPRMExpr rm, FPExpr t) + { + Contract.Ensures(Contract.Result() != null); + return new FPExpr(this, Native.Z3_mk_fpa_convert(this.nCtx, s.NativeObject, rm.NativeObject, t.NativeObject)); + } + + /// + /// Conversion of a floating point term to a bit-vector term in IEEE754 format. + /// + /// + /// The size of the resulting bit-vector is automatically determined. + /// + /// floating point term + FPExpr MkFPToIEEEBV(FPExpr t) + { + Contract.Ensures(Contract.Result() != null); + return new FPExpr(this, Native.Z3_mk_fpa_to_ieee_bv(this.nCtx, t.NativeObject)); + } + + #endregion #region Miscellaneous /// diff --git a/src/api/dotnet/FPExpr.cs b/src/api/dotnet/FPExpr.cs new file mode 100644 index 000000000..66b3fc10d --- /dev/null +++ b/src/api/dotnet/FPExpr.cs @@ -0,0 +1,46 @@ +/*++ +Copyright (c) 2013 Microsoft Corporation + +Module Name: + + FPExpr.cs + +Abstract: + + Z3 Managed API: Floating Point Expressions + +Author: + + Christoph Wintersteiger (cwinter) 2013-06-10 + +Notes: + +--*/ +using System; +using System.Collections.Generic; +using System.Linq; +using System.Text; + +using System.Diagnostics.Contracts; + +namespace Microsoft.Z3 +{ + /// + /// Floating Point Expressions + /// + public class FPExpr : Expr + { + #region Internal + internal protected FPExpr(Context ctx) + : base(ctx) + { + Contract.Requires(ctx != null); + } + internal FPExpr(Context ctx, IntPtr obj) + : base(ctx, obj) + { + Contract.Requires(ctx != null); + } + #endregion + } +} diff --git a/src/api/dotnet/FPNum.cs b/src/api/dotnet/FPNum.cs new file mode 100644 index 000000000..044598e58 --- /dev/null +++ b/src/api/dotnet/FPNum.cs @@ -0,0 +1,47 @@ +/*++ +Copyright (c) 2013 Microsoft Corporation + +Module Name: + + FPNum.cs + +Abstract: + + Z3 Managed API: Floating Point Numerals + +Author: + + Christoph Wintersteiger (cwinter) 2013-06-10 + +Notes: + +--*/ +using System; +using System.Diagnostics.Contracts; + +namespace Microsoft.Z3 +{ + /// + /// Floatiung Point Numerals + /// + [ContractVerification(true)] + public class FPNum : FPExpr + { + + #region Internal + internal FPNum(Context ctx, IntPtr obj) + : base(ctx, obj) + { + Contract.Requires(ctx != null); + } + #endregion + + /// + /// Returns a string representation of the numeral. + /// + public override string ToString() + { + return Native.Z3_get_numeral_string(Context.nCtx, NativeObject); + } + } +} diff --git a/src/api/dotnet/FPRMExpr.cs b/src/api/dotnet/FPRMExpr.cs new file mode 100644 index 000000000..fa43a346a --- /dev/null +++ b/src/api/dotnet/FPRMExpr.cs @@ -0,0 +1,46 @@ +/*++ +Copyright (c) 2013 Microsoft Corporation + +Module Name: + + FPRMExpr.cs + +Abstract: + + Z3 Managed API: Floating Point Expressions over Rounding Modes + +Author: + + Christoph Wintersteiger (cwinter) 2013-06-10 + +Notes: + +--*/ +using System; +using System.Collections.Generic; +using System.Linq; +using System.Text; + +using System.Diagnostics.Contracts; + +namespace Microsoft.Z3 +{ + /// + /// Floating Point Expressions + /// + public class FPRMExpr : Expr + { + #region Internal + internal protected FPRMExpr(Context ctx) + : base(ctx) + { + Contract.Requires(ctx != null); + } + internal FPRMExpr(Context ctx, IntPtr obj) + : base(ctx, obj) + { + Contract.Requires(ctx != null); + } + #endregion + } +} diff --git a/src/api/dotnet/FPRMNum.cs b/src/api/dotnet/FPRMNum.cs new file mode 100644 index 000000000..eaf105718 --- /dev/null +++ b/src/api/dotnet/FPRMNum.cs @@ -0,0 +1,47 @@ +/*++ +Copyright (c) 2013 Microsoft Corporation + +Module Name: + + FPRMNum.cs + +Abstract: + + Z3 Managed API: Floating Point Rounding Mode Numerals + +Author: + + Christoph Wintersteiger (cwinter) 2013-06-10 + +Notes: + +--*/ +using System; +using System.Diagnostics.Contracts; + +namespace Microsoft.Z3 +{ + /// + /// Floatiung Point Rounding Mode Numerals + /// + [ContractVerification(true)] + public class FPRMNum : FPRMExpr + { + + #region Internal + internal FPRMNum(Context ctx, IntPtr obj) + : base(ctx, obj) + { + Contract.Requires(ctx != null); + } + #endregion + + /// + /// Returns a string representation of the numeral. + /// + public override string ToString() + { + return Native.Z3_get_numeral_string(Context.nCtx, NativeObject); + } + } +} diff --git a/src/api/dotnet/FPRMSort.cs b/src/api/dotnet/FPRMSort.cs new file mode 100644 index 000000000..23d454a65 --- /dev/null +++ b/src/api/dotnet/FPRMSort.cs @@ -0,0 +1,43 @@ +/*++ +Copyright (c) 2013 Microsoft Corporation + +Module Name: + + FPRMSort.cs + +Abstract: + + Z3 Managed API: Floating Point Rounding Mode Sorts + +Author: + + Christoph Wintersteiger (cwinter) 2013-06-10 + +Notes: + +--*/ + +using System; +using System.Diagnostics.Contracts; + +namespace Microsoft.Z3 +{ + /// + /// A floating point rounding mode sort + /// + public class FPRMSort : Sort + { + #region Internal + internal FPRMSort(Context ctx, IntPtr obj) + : base(ctx, obj) + { + Contract.Requires(ctx != null); + } + internal FPRMSort(Context ctx) + : base(ctx, Native.Z3_mk_fpa_rounding_mode_sort(ctx.nCtx)) + { + Contract.Requires(ctx != null); + } + #endregion + } +} \ No newline at end of file diff --git a/src/api/dotnet/FPSort.cs b/src/api/dotnet/FPSort.cs new file mode 100644 index 000000000..a79557ae6 --- /dev/null +++ b/src/api/dotnet/FPSort.cs @@ -0,0 +1,43 @@ +/*++ +Copyright (c) 2013 Microsoft Corporation + +Module Name: + + FPSort.cs + +Abstract: + + Z3 Managed API: Floating Point Sorts + +Author: + + Christoph Wintersteiger (cwinter) 2013-06-10 + +Notes: + +--*/ + +using System; +using System.Diagnostics.Contracts; + +namespace Microsoft.Z3 +{ + /// + /// A floating point sort + /// + public class FPSort : Sort + { + #region Internal + internal FPSort(Context ctx, IntPtr obj) + : base(ctx, obj) + { + Contract.Requires(ctx != null); + } + internal FPSort(Context ctx, uint ebits, uint sbits) + : base(ctx, Native.Z3_mk_fpa_sort(ctx.nCtx, ebits, sbits)) + { + Contract.Requires(ctx != null); + } + #endregion + } +} diff --git a/src/api/dotnet/Microsoft.Z3.csproj b/src/api/dotnet/Microsoft.Z3.csproj index 9eb9eb660..083cd048f 100644 --- a/src/api/dotnet/Microsoft.Z3.csproj +++ b/src/api/dotnet/Microsoft.Z3.csproj @@ -341,6 +341,12 @@ + + + + + + @@ -399,4 +405,4 @@ --> - + \ No newline at end of file