From 3d37060fa97d25337334b1a0c1afeb3001ccb13c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 20 Oct 2018 10:24:36 -0700 Subject: [PATCH] remove dependencies on contracts Signed-off-by: Nikolaj Bjorner --- src/api/dotnet/AST.cs | 14 +- src/api/dotnet/ASTMap.cs | 18 +- src/api/dotnet/ASTVector.cs | 14 +- src/api/dotnet/AlgebraicNum.cs | 8 +- src/api/dotnet/ApplyResult.cs | 7 +- src/api/dotnet/ArithExpr.cs | 4 +- src/api/dotnet/ArithSort.cs | 4 +- src/api/dotnet/ArrayExpr.cs | 4 +- src/api/dotnet/ArraySort.cs | 19 +- src/api/dotnet/BitVecExpr.cs | 4 +- src/api/dotnet/BitVecNum.cs | 5 +- src/api/dotnet/BitVecSort.cs | 4 +- src/api/dotnet/BoolExpr.cs | 4 +- src/api/dotnet/BoolSort.cs | 6 +- src/api/dotnet/Constructor.cs | 12 +- src/api/dotnet/ConstructorList.cs | 8 +- src/api/dotnet/Context.cs | 1203 ++++++++++----------------- src/api/dotnet/DatatypeExpr.cs | 4 +- src/api/dotnet/DatatypeSort.cs | 14 +- src/api/dotnet/Deprecated.cs | 3 +- src/api/dotnet/EnumSort.cs | 12 +- src/api/dotnet/Expr.cs | 52 +- src/api/dotnet/FPExpr.cs | 4 +- src/api/dotnet/FPNum.cs | 5 +- src/api/dotnet/FPRMExpr.cs | 4 +- src/api/dotnet/FPRMNum.cs | 4 +- src/api/dotnet/FPRMSort.cs | 6 +- src/api/dotnet/FPSort.cs | 6 +- src/api/dotnet/FiniteDomainExpr.cs | 4 +- src/api/dotnet/FiniteDomainNum.cs | 5 +- src/api/dotnet/FiniteDomainSort.cs | 9 +- src/api/dotnet/Fixedpoint.cs | 37 +- src/api/dotnet/FuncDecl.cs | 25 +- src/api/dotnet/FuncInterp.cs | 13 +- src/api/dotnet/Global.cs | 2 +- src/api/dotnet/Goal.cs | 18 +- src/api/dotnet/IDecRefQueue.cs | 15 +- src/api/dotnet/IntExpr.cs | 4 +- src/api/dotnet/IntNum.cs | 5 +- src/api/dotnet/IntSort.cs | 6 +- src/api/dotnet/IntSymbol.cs | 7 +- src/api/dotnet/Lambda.cs | 31 +- src/api/dotnet/ListSort.cs | 16 +- src/api/dotnet/Log.cs | 6 +- src/api/dotnet/Model.cs | 24 +- src/api/dotnet/Optimize.cs | 20 +- src/api/dotnet/ParamDescrs.cs | 11 +- src/api/dotnet/Params.cs | 23 +- src/api/dotnet/Pattern.cs | 6 +- src/api/dotnet/Probe.cs | 11 +- src/api/dotnet/Quantifier.cs | 41 +- src/api/dotnet/RatNum.cs | 7 +- src/api/dotnet/ReExpr.cs | 4 +- src/api/dotnet/ReSort.cs | 6 +- src/api/dotnet/RealExpr.cs | 4 +- src/api/dotnet/RealSort.cs | 6 +- src/api/dotnet/RelationSort.cs | 6 +- src/api/dotnet/SeqExpr.cs | 4 +- src/api/dotnet/SeqSort.cs | 6 +- src/api/dotnet/SetSort.cs | 9 +- src/api/dotnet/Solver.cs | 30 +- src/api/dotnet/Sort.cs | 10 +- src/api/dotnet/Statistics.cs | 11 +- src/api/dotnet/Status.cs | 1 + src/api/dotnet/StringSymbol.cs | 8 +- src/api/dotnet/Symbol.cs | 8 +- src/api/dotnet/Tactic.cs | 15 +- src/api/dotnet/TupleSort.cs | 9 +- src/api/dotnet/UninterpretedSort.cs | 8 +- src/api/dotnet/Version.cs | 4 +- src/api/dotnet/Z3Exception.cs | 1 + src/api/dotnet/Z3Object.cs | 18 +- 72 files changed, 734 insertions(+), 1232 deletions(-) diff --git a/src/api/dotnet/AST.cs b/src/api/dotnet/AST.cs index 2460c50f0..0afff2c42 100644 --- a/src/api/dotnet/AST.cs +++ b/src/api/dotnet/AST.cs @@ -17,17 +17,16 @@ Notes: --*/ +using System.Diagnostics; using System; using System.Collections; using System.Collections.Generic; -using System.Diagnostics.Contracts; namespace Microsoft.Z3 { /// /// The abstract syntax tree (AST) class. /// - [ContractVerification(true)] public class AST : Z3Object, IComparable { /// @@ -114,8 +113,7 @@ namespace Microsoft.Z3 /// A copy of the AST which is associated with public AST Translate(Context ctx) { - Contract.Requires(ctx != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(ctx != null); if (ReferenceEquals(Context, ctx)) return this; @@ -202,14 +200,13 @@ namespace Microsoft.Z3 /// public string SExpr() { - Contract.Ensures(Contract.Result() != null); return Native.Z3_ast_to_string(Context.nCtx, NativeObject); } #region Internal - internal AST(Context ctx) : base(ctx) { Contract.Requires(ctx != null); } - internal AST(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); } + internal AST(Context ctx) : base(ctx) { Debug.Assert(ctx != null); } + internal AST(Context ctx, IntPtr obj) : base(ctx, obj) { Debug.Assert(ctx != null); } internal class DecRefQueue : IDecRefQueue { @@ -246,8 +243,7 @@ namespace Microsoft.Z3 internal static AST Create(Context ctx, IntPtr obj) { - Contract.Requires(ctx != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(ctx != null); switch ((Z3_ast_kind)Native.Z3_get_ast_kind(ctx.nCtx, obj)) { diff --git a/src/api/dotnet/ASTMap.cs b/src/api/dotnet/ASTMap.cs index f7c1c5914..f678f71c3 100644 --- a/src/api/dotnet/ASTMap.cs +++ b/src/api/dotnet/ASTMap.cs @@ -17,15 +17,14 @@ Notes: --*/ +using System.Diagnostics; using System; -using System.Diagnostics.Contracts; namespace Microsoft.Z3 { /// /// Map from AST to AST /// - [ContractVerification(true)] internal class ASTMap : Z3Object { /// @@ -35,7 +34,7 @@ namespace Microsoft.Z3 /// True if is a key in the map, false otherwise. public bool Contains(AST k) { - Contract.Requires(k != null); + Debug.Assert(k != null); return 0 != Native.Z3_ast_map_contains(Context.nCtx, NativeObject, k.NativeObject); } @@ -49,8 +48,7 @@ namespace Microsoft.Z3 /// An AST public AST Find(AST k) { - Contract.Requires(k != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(k != null); return new AST(Context, Native.Z3_ast_map_find(Context.nCtx, NativeObject, k.NativeObject)); } @@ -62,8 +60,8 @@ namespace Microsoft.Z3 /// The value AST public void Insert(AST k, AST v) { - Contract.Requires(k != null); - Contract.Requires(v != null); + Debug.Assert(k != null); + Debug.Assert(v != null); Native.Z3_ast_map_insert(Context.nCtx, NativeObject, k.NativeObject, v.NativeObject); } @@ -74,7 +72,7 @@ namespace Microsoft.Z3 /// An AST public void Erase(AST k) { - Contract.Requires(k != null); + Debug.Assert(k != null); Native.Z3_ast_map_erase(Context.nCtx, NativeObject, k.NativeObject); } @@ -119,12 +117,12 @@ namespace Microsoft.Z3 internal ASTMap(Context ctx, IntPtr obj) : base(ctx, obj) { - Contract.Requires(ctx != null); + Debug.Assert(ctx != null); } internal ASTMap(Context ctx) : base(ctx, Native.Z3_mk_ast_map(ctx.nCtx)) { - Contract.Requires(ctx != null); + Debug.Assert(ctx != null); } internal class DecRefQueue : IDecRefQueue diff --git a/src/api/dotnet/ASTVector.cs b/src/api/dotnet/ASTVector.cs index 8b599ca48..fcfa6bd65 100644 --- a/src/api/dotnet/ASTVector.cs +++ b/src/api/dotnet/ASTVector.cs @@ -17,8 +17,8 @@ Notes: --*/ +using System.Diagnostics; using System; -using System.Diagnostics.Contracts; namespace Microsoft.Z3 { @@ -45,13 +45,12 @@ namespace Microsoft.Z3 { get { - Contract.Ensures(Contract.Result() != null); return new AST(Context, Native.Z3_ast_vector_get(Context.nCtx, NativeObject, i)); } set { - Contract.Requires(value != null); + Debug.Assert(value != null); Native.Z3_ast_vector_set(Context.nCtx, NativeObject, i, value.NativeObject); } @@ -73,7 +72,7 @@ namespace Microsoft.Z3 /// An AST public void Push(AST a) { - Contract.Requires(a != null); + Debug.Assert(a != null); Native.Z3_ast_vector_push(Context.nCtx, NativeObject, a.NativeObject); } @@ -85,8 +84,7 @@ namespace Microsoft.Z3 /// A new ASTVector public ASTVector Translate(Context ctx) { - Contract.Requires(ctx != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(ctx != null); return new ASTVector(Context, Native.Z3_ast_vector_translate(Context.nCtx, NativeObject, ctx.nCtx)); } @@ -232,8 +230,8 @@ namespace Microsoft.Z3 } #region Internal - internal ASTVector(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); } - internal ASTVector(Context ctx) : base(ctx, Native.Z3_mk_ast_vector(ctx.nCtx)) { Contract.Requires(ctx != null); } + internal ASTVector(Context ctx, IntPtr obj) : base(ctx, obj) { Debug.Assert(ctx != null); } + internal ASTVector(Context ctx) : base(ctx, Native.Z3_mk_ast_vector(ctx.nCtx)) { Debug.Assert(ctx != null); } internal class DecRefQueue : IDecRefQueue { diff --git a/src/api/dotnet/AlgebraicNum.cs b/src/api/dotnet/AlgebraicNum.cs index 3687e1f83..cd1e4e922 100644 --- a/src/api/dotnet/AlgebraicNum.cs +++ b/src/api/dotnet/AlgebraicNum.cs @@ -16,8 +16,8 @@ Author: Notes: --*/ +using System.Diagnostics; using System; -using System.Diagnostics.Contracts; #if !FRAMEWORK_LT_4 using System.Numerics; @@ -28,7 +28,6 @@ namespace Microsoft.Z3 /// /// Algebraic numbers /// - [ContractVerification(true)] public class AlgebraicNum : ArithExpr { /// @@ -40,7 +39,6 @@ namespace Microsoft.Z3 /// A numeral Expr of sort Real public RatNum ToUpper(uint precision) { - Contract.Ensures(Contract.Result() != null); return new RatNum(Context, Native.Z3_get_algebraic_number_upper(Context.nCtx, NativeObject, precision)); } @@ -54,7 +52,6 @@ namespace Microsoft.Z3 /// A numeral Expr of sort Real public RatNum ToLower(uint precision) { - Contract.Ensures(Contract.Result() != null); return new RatNum(Context, Native.Z3_get_algebraic_number_lower(Context.nCtx, NativeObject, precision)); } @@ -65,7 +62,6 @@ namespace Microsoft.Z3 /// The result has at most decimal places. public string ToDecimal(uint precision) { - Contract.Ensures(Contract.Result() != null); return Native.Z3_get_numeral_decimal_string(Context.nCtx, NativeObject, precision); } @@ -74,7 +70,7 @@ namespace Microsoft.Z3 internal AlgebraicNum(Context ctx, IntPtr obj) : base(ctx, obj) { - Contract.Requires(ctx != null); + Debug.Assert(ctx != null); } #endregion } diff --git a/src/api/dotnet/ApplyResult.cs b/src/api/dotnet/ApplyResult.cs index db2922460..342bf3216 100644 --- a/src/api/dotnet/ApplyResult.cs +++ b/src/api/dotnet/ApplyResult.cs @@ -17,8 +17,8 @@ Notes: --*/ +using System.Diagnostics; using System; -using System.Diagnostics.Contracts; namespace Microsoft.Z3 { @@ -26,7 +26,6 @@ namespace Microsoft.Z3 /// ApplyResult objects represent the result of an application of a /// tactic to a goal. It contains the subgoals that were produced. /// - [ContractVerification(true)] public class ApplyResult : Z3Object { /// @@ -44,8 +43,6 @@ namespace Microsoft.Z3 { get { - Contract.Ensures(Contract.Result() != null); - Contract.Ensures(Contract.Result().Length == this.NumSubgoals); uint n = NumSubgoals; Goal[] res = new Goal[n]; @@ -67,7 +64,7 @@ namespace Microsoft.Z3 internal ApplyResult(Context ctx, IntPtr obj) : base(ctx, obj) { - Contract.Requires(ctx != null); + Debug.Assert(ctx != null); } internal class DecRefQueue : IDecRefQueue diff --git a/src/api/dotnet/ArithExpr.cs b/src/api/dotnet/ArithExpr.cs index 1c42fd78a..53b9db21d 100644 --- a/src/api/dotnet/ArithExpr.cs +++ b/src/api/dotnet/ArithExpr.cs @@ -16,12 +16,12 @@ Author: Notes: --*/ +using System.Diagnostics; using System; using System.Collections.Generic; using System.Linq; using System.Text; -using System.Diagnostics.Contracts; namespace Microsoft.Z3 { @@ -35,7 +35,7 @@ namespace Microsoft.Z3 internal ArithExpr(Context ctx, IntPtr obj) : base(ctx, obj) { - Contract.Requires(ctx != null); + Debug.Assert(ctx != null); } #endregion diff --git a/src/api/dotnet/ArithSort.cs b/src/api/dotnet/ArithSort.cs index f19774246..985aec7a9 100644 --- a/src/api/dotnet/ArithSort.cs +++ b/src/api/dotnet/ArithSort.cs @@ -17,8 +17,8 @@ Notes: --*/ +using System.Diagnostics; using System; -using System.Diagnostics.Contracts; namespace Microsoft.Z3 { @@ -28,7 +28,7 @@ namespace Microsoft.Z3 public class ArithSort : Sort { #region Internal - internal ArithSort(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); } + internal ArithSort(Context ctx, IntPtr obj) : base(ctx, obj) { Debug.Assert(ctx != null); } #endregion }; } diff --git a/src/api/dotnet/ArrayExpr.cs b/src/api/dotnet/ArrayExpr.cs index 6c51bfc5b..c53763886 100644 --- a/src/api/dotnet/ArrayExpr.cs +++ b/src/api/dotnet/ArrayExpr.cs @@ -16,12 +16,12 @@ Author: Notes: --*/ +using System.Diagnostics; using System; using System.Collections.Generic; using System.Linq; using System.Text; -using System.Diagnostics.Contracts; namespace Microsoft.Z3 { @@ -35,7 +35,7 @@ namespace Microsoft.Z3 internal ArrayExpr(Context ctx, IntPtr obj) : base(ctx, obj) { - Contract.Requires(ctx != null); + Debug.Assert(ctx != null); } #endregion } diff --git a/src/api/dotnet/ArraySort.cs b/src/api/dotnet/ArraySort.cs index 47a73ae1f..c5d15938e 100644 --- a/src/api/dotnet/ArraySort.cs +++ b/src/api/dotnet/ArraySort.cs @@ -17,15 +17,14 @@ Notes: --*/ +using System.Diagnostics; using System; -using System.Diagnostics.Contracts; namespace Microsoft.Z3 { /// /// Array sorts. /// - [ContractVerification(true)] public class ArraySort : Sort { /// @@ -35,7 +34,6 @@ namespace Microsoft.Z3 { get { - Contract.Ensures(Contract.Result() != null); return Sort.Create(Context, Native.Z3_get_array_sort_domain(Context.nCtx, NativeObject)); } @@ -48,27 +46,26 @@ namespace Microsoft.Z3 { get { - Contract.Ensures(Contract.Result() != null); return Sort.Create(Context, Native.Z3_get_array_sort_range(Context.nCtx, NativeObject)); } } #region Internal - internal ArraySort(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); } + internal ArraySort(Context ctx, IntPtr obj) : base(ctx, obj) { Debug.Assert(ctx != null); } internal ArraySort(Context ctx, Sort domain, Sort range) : base(ctx, Native.Z3_mk_array_sort(ctx.nCtx, domain.NativeObject, range.NativeObject)) { - Contract.Requires(ctx != null); - Contract.Requires(domain != null); - Contract.Requires(range != null); + Debug.Assert(ctx != null); + Debug.Assert(domain != null); + Debug.Assert(range != null); } internal ArraySort(Context ctx, Sort[] domain, Sort range) : base(ctx, Native.Z3_mk_array_sort_n(ctx.nCtx, (uint)domain.Length, AST.ArrayToNative(domain), range.NativeObject)) { - Contract.Requires(ctx != null); - Contract.Requires(domain != null); - Contract.Requires(range != null); + Debug.Assert(ctx != null); + Debug.Assert(domain != null); + Debug.Assert(range != null); } #endregion }; diff --git a/src/api/dotnet/BitVecExpr.cs b/src/api/dotnet/BitVecExpr.cs index b019f8845..3efa0e9bd 100644 --- a/src/api/dotnet/BitVecExpr.cs +++ b/src/api/dotnet/BitVecExpr.cs @@ -16,12 +16,12 @@ Author: Notes: --*/ +using System.Diagnostics; using System; using System.Collections.Generic; using System.Linq; using System.Text; -using System.Diagnostics.Contracts; namespace Microsoft.Z3 { @@ -41,7 +41,7 @@ namespace Microsoft.Z3 #region Internal /// Constructor for BitVecExpr - internal BitVecExpr(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); } + internal BitVecExpr(Context ctx, IntPtr obj) : base(ctx, obj) { Debug.Assert(ctx != null); } #endregion } } diff --git a/src/api/dotnet/BitVecNum.cs b/src/api/dotnet/BitVecNum.cs index 66054761a..5ee2d2ed8 100644 --- a/src/api/dotnet/BitVecNum.cs +++ b/src/api/dotnet/BitVecNum.cs @@ -16,8 +16,8 @@ Author: Notes: --*/ +using System.Diagnostics; using System; -using System.Diagnostics.Contracts; #if !FRAMEWORK_LT_4 using System.Numerics; @@ -28,7 +28,6 @@ namespace Microsoft.Z3 /// /// Bit-vector numerals /// - [ContractVerification(true)] public class BitVecNum : BitVecExpr { /// @@ -109,7 +108,7 @@ namespace Microsoft.Z3 } #region Internal - internal BitVecNum(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); } + internal BitVecNum(Context ctx, IntPtr obj) : base(ctx, obj) { Debug.Assert(ctx != null); } #endregion } } diff --git a/src/api/dotnet/BitVecSort.cs b/src/api/dotnet/BitVecSort.cs index d865159f4..fb41e76fe 100644 --- a/src/api/dotnet/BitVecSort.cs +++ b/src/api/dotnet/BitVecSort.cs @@ -17,8 +17,8 @@ Notes: --*/ +using System.Diagnostics; using System; -using System.Diagnostics.Contracts; namespace Microsoft.Z3 { @@ -36,7 +36,7 @@ namespace Microsoft.Z3 } #region Internal - internal BitVecSort(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); } + internal BitVecSort(Context ctx, IntPtr obj) : base(ctx, obj) { Debug.Assert(ctx != null); } #endregion }; } diff --git a/src/api/dotnet/BoolExpr.cs b/src/api/dotnet/BoolExpr.cs index c52109352..906090d2a 100644 --- a/src/api/dotnet/BoolExpr.cs +++ b/src/api/dotnet/BoolExpr.cs @@ -16,12 +16,12 @@ Author: Notes: --*/ +using System.Diagnostics; using System; using System.Collections.Generic; using System.Linq; using System.Text; -using System.Diagnostics.Contracts; namespace Microsoft.Z3 { @@ -32,7 +32,7 @@ namespace Microsoft.Z3 { #region Internal /// Constructor for BoolExpr - internal BoolExpr(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); } + internal BoolExpr(Context ctx, IntPtr obj) : base(ctx, obj) { Debug.Assert(ctx != null); } #endregion #region Operators diff --git a/src/api/dotnet/BoolSort.cs b/src/api/dotnet/BoolSort.cs index 50f44c858..7fd6706a3 100644 --- a/src/api/dotnet/BoolSort.cs +++ b/src/api/dotnet/BoolSort.cs @@ -17,8 +17,8 @@ Notes: --*/ +using System.Diagnostics; using System; -using System.Diagnostics.Contracts; namespace Microsoft.Z3 { @@ -28,8 +28,8 @@ namespace Microsoft.Z3 public class BoolSort : Sort { #region Internal - internal BoolSort(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); } - internal BoolSort(Context ctx) : base(ctx, Native.Z3_mk_bool_sort(ctx.nCtx)) { Contract.Requires(ctx != null); } + internal BoolSort(Context ctx, IntPtr obj) : base(ctx, obj) { Debug.Assert(ctx != null); } + internal BoolSort(Context ctx) : base(ctx, Native.Z3_mk_bool_sort(ctx.nCtx)) { Debug.Assert(ctx != null); } #endregion }; } diff --git a/src/api/dotnet/Constructor.cs b/src/api/dotnet/Constructor.cs index 527b8bc13..f635d78e4 100644 --- a/src/api/dotnet/Constructor.cs +++ b/src/api/dotnet/Constructor.cs @@ -17,15 +17,14 @@ Notes: --*/ +using System.Diagnostics; using System; -using System.Diagnostics.Contracts; namespace Microsoft.Z3 { /// /// Constructors are used for datatype sorts. /// - [ContractVerification(true)] public class Constructor : Z3Object { /// @@ -46,7 +45,6 @@ namespace Microsoft.Z3 { get { - Contract.Ensures(Contract.Result() != null); IntPtr constructor = IntPtr.Zero; IntPtr tester = IntPtr.Zero; IntPtr[] accessors = new IntPtr[n]; @@ -62,7 +60,6 @@ namespace Microsoft.Z3 { get { - Contract.Ensures(Contract.Result() != null); IntPtr constructor = IntPtr.Zero; IntPtr tester = IntPtr.Zero; IntPtr[] accessors = new IntPtr[n]; @@ -78,7 +75,6 @@ namespace Microsoft.Z3 { get { - Contract.Ensures(Contract.Result() != null); IntPtr constructor = IntPtr.Zero; IntPtr tester = IntPtr.Zero; IntPtr[] accessors = new IntPtr[n]; @@ -105,9 +101,9 @@ namespace Microsoft.Z3 Sort[] sorts, uint[] sortRefs) : base(ctx) { - Contract.Requires(ctx != null); - Contract.Requires(name != null); - Contract.Requires(recognizer != null); + Debug.Assert(ctx != null); + Debug.Assert(name != null); + Debug.Assert(recognizer != null); n = AST.ArrayLength(fieldNames); diff --git a/src/api/dotnet/ConstructorList.cs b/src/api/dotnet/ConstructorList.cs index d625b5ade..9b9ba8561 100644 --- a/src/api/dotnet/ConstructorList.cs +++ b/src/api/dotnet/ConstructorList.cs @@ -17,12 +17,12 @@ Notes: --*/ +using System.Diagnostics; using System; using System.Collections.Generic; using System.Linq; using System.Text; -using System.Diagnostics.Contracts; namespace Microsoft.Z3 { @@ -43,14 +43,14 @@ namespace Microsoft.Z3 internal ConstructorList(Context ctx, IntPtr obj) : base(ctx, obj) { - Contract.Requires(ctx != null); + Debug.Assert(ctx != null); } internal ConstructorList(Context ctx, Constructor[] constructors) : base(ctx) { - Contract.Requires(ctx != null); - Contract.Requires(constructors != null); + Debug.Assert(ctx != null); + Debug.Assert(constructors != null); NativeObject = Native.Z3_mk_constructor_list(Context.nCtx, (uint)constructors.Length, Constructor.ArrayToNative(constructors)); } diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs index ef85a8713..97541e31f 100644 --- a/src/api/dotnet/Context.cs +++ b/src/api/dotnet/Context.cs @@ -18,9 +18,9 @@ Notes: --*/ using System; +using System.Diagnostics; using System.Collections.Generic; using System.Runtime.InteropServices; -using System.Diagnostics.Contracts; using System.Linq; namespace Microsoft.Z3 @@ -28,7 +28,6 @@ namespace Microsoft.Z3 /// /// The main interaction with Z3 happens via the Context. /// - [ContractVerification(true)] public class Context : IDisposable { #region Constructors @@ -66,7 +65,7 @@ namespace Microsoft.Z3 public Context(Dictionary settings) : base() { - Contract.Requires(settings != null); + Debug.Assert(settings != null); lock (creation_lock) { @@ -90,7 +89,6 @@ namespace Microsoft.Z3 /// public IntSymbol MkSymbol(int i) { - Contract.Ensures(Contract.Result() != null); return new IntSymbol(this, i); } @@ -100,7 +98,6 @@ namespace Microsoft.Z3 /// public StringSymbol MkSymbol(string name) { - Contract.Ensures(Contract.Result() != null); return new StringSymbol(this, name); } @@ -110,10 +107,6 @@ namespace Microsoft.Z3 /// internal Symbol[] MkSymbols(string[] names) { - Contract.Ensures(names == null || Contract.Result() != null); - Contract.Ensures(names != null || Contract.Result() == null); - Contract.Ensures(Contract.Result() == null || Contract.Result().Length == names.Length); - Contract.Ensures(Contract.Result() == null || Contract.ForAll(Contract.Result(), s => s != null)); if (names == null) return null; Symbol[] result = new Symbol[names.Length]; @@ -135,7 +128,6 @@ namespace Microsoft.Z3 { get { - Contract.Ensures(Contract.Result() != null); if (m_boolSort == null) m_boolSort = new BoolSort(this); return m_boolSort; } } @@ -147,7 +139,6 @@ namespace Microsoft.Z3 { get { - Contract.Ensures(Contract.Result() != null); if (m_intSort == null) m_intSort = new IntSort(this); return m_intSort; } } @@ -160,7 +151,6 @@ namespace Microsoft.Z3 { get { - Contract.Ensures(Contract.Result() != null); if (m_realSort == null) m_realSort = new RealSort(this); return m_realSort; } } @@ -172,7 +162,6 @@ namespace Microsoft.Z3 { get { - Contract.Ensures(Contract.Result() != null); if (m_stringSort == null) m_stringSort = new SeqSort(this, Native.Z3_mk_string_sort(nCtx)); return m_stringSort; } @@ -184,7 +173,6 @@ namespace Microsoft.Z3 /// public BoolSort MkBoolSort() { - Contract.Ensures(Contract.Result() != null); return new BoolSort(this); } @@ -193,8 +181,7 @@ namespace Microsoft.Z3 /// public UninterpretedSort MkUninterpretedSort(Symbol s) { - Contract.Requires(s != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(s != null); CheckContextMatch(s); return new UninterpretedSort(this, s); @@ -205,7 +192,6 @@ namespace Microsoft.Z3 /// public UninterpretedSort MkUninterpretedSort(string str) { - Contract.Ensures(Contract.Result() != null); return MkUninterpretedSort(MkSymbol(str)); } @@ -215,7 +201,6 @@ namespace Microsoft.Z3 /// public IntSort MkIntSort() { - Contract.Ensures(Contract.Result() != null); return new IntSort(this); } @@ -225,7 +210,6 @@ namespace Microsoft.Z3 /// public RealSort MkRealSort() { - Contract.Ensures(Contract.Result() != null); return new RealSort(this); } @@ -234,7 +218,6 @@ namespace Microsoft.Z3 /// public BitVecSort MkBitVecSort(uint size) { - Contract.Ensures(Contract.Result() != null); return new BitVecSort(this, Native.Z3_mk_bv_sort(nCtx, size)); } @@ -245,8 +228,7 @@ namespace Microsoft.Z3 /// public SeqSort MkSeqSort(Sort s) { - Contract.Requires(s != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(s != null); return new SeqSort(this, Native.Z3_mk_seq_sort(nCtx, s.NativeObject)); } @@ -255,8 +237,7 @@ namespace Microsoft.Z3 /// public ReSort MkReSort(SeqSort s) { - Contract.Requires(s != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(s != null); return new ReSort(this, Native.Z3_mk_re_sort(nCtx, s.NativeObject)); } @@ -265,9 +246,8 @@ namespace Microsoft.Z3 /// public ArraySort MkArraySort(Sort domain, Sort range) { - Contract.Requires(domain != null); - Contract.Requires(range != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(domain != null); + Debug.Assert(range != null); CheckContextMatch(domain); CheckContextMatch(range); @@ -279,9 +259,8 @@ namespace Microsoft.Z3 /// public ArraySort MkArraySort(Sort[] domain, Sort range) { - Contract.Requires(domain != null); - Contract.Requires(range != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(domain != null); + Debug.Assert(range != null); CheckContextMatch(domain); CheckContextMatch(range); @@ -293,11 +272,10 @@ namespace Microsoft.Z3 /// public TupleSort MkTupleSort(Symbol name, Symbol[] fieldNames, Sort[] fieldSorts) { - Contract.Requires(name != null); - Contract.Requires(fieldNames != null); - Contract.Requires(Contract.ForAll(fieldNames, fn => fn != null)); - Contract.Requires(fieldSorts == null || Contract.ForAll(fieldSorts, fs => fs != null)); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(name != null); + Debug.Assert(fieldNames != null); + Debug.Assert(fieldNames.All(fn => fn != null)); + Debug.Assert(fieldSorts == null || fieldSorts.All(fs => fs != null)); CheckContextMatch(name); CheckContextMatch(fieldNames); @@ -310,11 +288,10 @@ namespace Microsoft.Z3 /// public EnumSort MkEnumSort(Symbol name, params Symbol[] enumNames) { - Contract.Requires(name != null); - Contract.Requires(enumNames != null); - Contract.Requires(Contract.ForAll(enumNames, f => f != null)); + Debug.Assert(name != null); + Debug.Assert(enumNames != null); + Debug.Assert(enumNames.All(f => f != null)); - Contract.Ensures(Contract.Result() != null); CheckContextMatch(name); CheckContextMatch(enumNames); @@ -326,8 +303,7 @@ namespace Microsoft.Z3 /// public EnumSort MkEnumSort(string name, params string[] enumNames) { - Contract.Requires(enumNames != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(enumNames != null); return new EnumSort(this, MkSymbol(name), MkSymbols(enumNames)); } @@ -337,9 +313,8 @@ namespace Microsoft.Z3 /// public ListSort MkListSort(Symbol name, Sort elemSort) { - Contract.Requires(name != null); - Contract.Requires(elemSort != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(name != null); + Debug.Assert(elemSort != null); CheckContextMatch(name); CheckContextMatch(elemSort); @@ -351,8 +326,7 @@ namespace Microsoft.Z3 /// public ListSort MkListSort(string name, Sort elemSort) { - Contract.Requires(elemSort != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(elemSort != null); CheckContextMatch(elemSort); return new ListSort(this, MkSymbol(name), elemSort); @@ -366,8 +340,7 @@ namespace Microsoft.Z3 /// The size of the sort public FiniteDomainSort MkFiniteDomainSort(Symbol name, ulong size) { - Contract.Requires(name != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(name != null); CheckContextMatch(name); return new FiniteDomainSort(this, name, size); @@ -383,7 +356,6 @@ namespace Microsoft.Z3 /// The size of the sort public FiniteDomainSort MkFiniteDomainSort(string name, ulong size) { - Contract.Ensures(Contract.Result() != null); return new FiniteDomainSort(this, MkSymbol(name), size); } @@ -402,9 +374,8 @@ namespace Microsoft.Z3 /// referring to one of the recursive datatypes that is declared. public Constructor MkConstructor(Symbol name, Symbol recognizer, Symbol[] fieldNames = null, Sort[] sorts = null, uint[] sortRefs = null) { - Contract.Requires(name != null); - Contract.Requires(recognizer != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(name != null); + Debug.Assert(recognizer != null); return new Constructor(this, name, recognizer, fieldNames, sorts, sortRefs); } @@ -420,7 +391,6 @@ namespace Microsoft.Z3 /// public Constructor MkConstructor(string name, string recognizer, string[] fieldNames = null, Sort[] sorts = null, uint[] sortRefs = null) { - Contract.Ensures(Contract.Result() != null); return new Constructor(this, MkSymbol(name), MkSymbol(recognizer), MkSymbols(fieldNames), sorts, sortRefs); } @@ -430,11 +400,10 @@ namespace Microsoft.Z3 /// public DatatypeSort MkDatatypeSort(Symbol name, Constructor[] constructors) { - Contract.Requires(name != null); - Contract.Requires(constructors != null); - Contract.Requires(Contract.ForAll(constructors, c => c != null)); + Debug.Assert(name != null); + Debug.Assert(constructors != null); + Debug.Assert(constructors.All(c => c != null)); - Contract.Ensures(Contract.Result() != null); CheckContextMatch(name); CheckContextMatch(constructors); @@ -446,9 +415,8 @@ namespace Microsoft.Z3 /// public DatatypeSort MkDatatypeSort(string name, Constructor[] constructors) { - Contract.Requires(constructors != null); - Contract.Requires(Contract.ForAll(constructors, c => c != null)); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(constructors != null); + Debug.Assert(constructors.All(c => c != null)); CheckContextMatch(constructors); return new DatatypeSort(this, MkSymbol(name), constructors); @@ -461,12 +429,11 @@ namespace Microsoft.Z3 /// list of constructors, one list per sort. public DatatypeSort[] MkDatatypeSorts(Symbol[] names, Constructor[][] c) { - Contract.Requires(names != null); - Contract.Requires(c != null); - Contract.Requires(names.Length == c.Length); - Contract.Requires(Contract.ForAll(0, c.Length, j => c[j] != null)); - Contract.Requires(Contract.ForAll(names, name => name != null)); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(names != null); + Debug.Assert(c != null); + Debug.Assert(names.Length == c.Length); + //Debug.Assert(Contract.ForAll(0, c.Length, j => c[j] != null)); + Debug.Assert(names.All(name => name != null)); CheckContextMatch(names); uint n = (uint)names.Length; @@ -475,7 +442,6 @@ namespace Microsoft.Z3 for (uint i = 0; i < n; i++) { Constructor[] constructor = c[i]; - Contract.Assume(Contract.ForAll(constructor, arr => arr != null), "Clousot does not support yet quantified formula on multidimensional arrays"); CheckContextMatch(constructor); cla[i] = new ConstructorList(this, constructor); n_constr[i] = cla[i].NativeObject; @@ -496,12 +462,11 @@ namespace Microsoft.Z3 /// public DatatypeSort[] MkDatatypeSorts(string[] names, Constructor[][] c) { - Contract.Requires(names != null); - Contract.Requires(c != null); - Contract.Requires(names.Length == c.Length); - Contract.Requires(Contract.ForAll(0, c.Length, j => c[j] != null)); - Contract.Requires(Contract.ForAll(names, name => name != null)); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(names != null); + Debug.Assert(c != null); + Debug.Assert(names.Length == c.Length); + //Debug.Assert(Contract.ForAll(0, c.Length, j => c[j] != null)); + //Debug.Assert(names.All(name => name != null)); return MkDatatypeSorts(MkSymbols(names), c); } @@ -528,10 +493,9 @@ namespace Microsoft.Z3 /// public FuncDecl MkFuncDecl(Symbol name, Sort[] domain, Sort range) { - Contract.Requires(name != null); - Contract.Requires(range != null); - Contract.Requires(Contract.ForAll(domain, d => d != null)); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(name != null); + Debug.Assert(range != null); + Debug.Assert(domain.All(d => d != null)); CheckContextMatch(name); CheckContextMatch(domain); @@ -544,10 +508,9 @@ namespace Microsoft.Z3 /// public FuncDecl MkFuncDecl(Symbol name, Sort domain, Sort range) { - Contract.Requires(name != null); - Contract.Requires(domain != null); - Contract.Requires(range != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(name != null); + Debug.Assert(domain != null); + Debug.Assert(range != null); CheckContextMatch(name); CheckContextMatch(domain); @@ -561,9 +524,8 @@ namespace Microsoft.Z3 /// public FuncDecl MkFuncDecl(string name, Sort[] domain, Sort range) { - Contract.Requires(range != null); - Contract.Requires(Contract.ForAll(domain, d => d != null)); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(range != null); + Debug.Assert(domain.All(d => d != null)); CheckContextMatch(domain); CheckContextMatch(range); @@ -575,9 +537,8 @@ namespace Microsoft.Z3 /// public FuncDecl MkFuncDecl(string name, Sort domain, Sort range) { - Contract.Requires(range != null); - Contract.Requires(domain != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(range != null); + Debug.Assert(domain != null); CheckContextMatch(domain); CheckContextMatch(range); @@ -592,9 +553,8 @@ namespace Microsoft.Z3 /// public FuncDecl MkFreshFuncDecl(string prefix, Sort[] domain, Sort range) { - Contract.Requires(range != null); - Contract.Requires(Contract.ForAll(domain, d => d != null)); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(range != null); + Debug.Assert(domain.All(d => d != null)); CheckContextMatch(domain); CheckContextMatch(range); @@ -606,9 +566,8 @@ namespace Microsoft.Z3 /// public FuncDecl MkConstDecl(Symbol name, Sort range) { - Contract.Requires(name != null); - Contract.Requires(range != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(name != null); + Debug.Assert(range != null); CheckContextMatch(name); CheckContextMatch(range); @@ -620,8 +579,7 @@ namespace Microsoft.Z3 /// public FuncDecl MkConstDecl(string name, Sort range) { - Contract.Requires(range != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(range != null); CheckContextMatch(range); return new FuncDecl(this, MkSymbol(name), null, range); @@ -634,8 +592,7 @@ namespace Microsoft.Z3 /// public FuncDecl MkFreshConstDecl(string prefix, Sort range) { - Contract.Requires(range != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(range != null); CheckContextMatch(range); return new FuncDecl(this, prefix, null, range); @@ -650,8 +607,7 @@ namespace Microsoft.Z3 /// The sort of the variable public Expr MkBound(uint index, Sort ty) { - Contract.Requires(ty != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(ty != null); return Expr.Create(this, Native.Z3_mk_bound(nCtx, index, ty.NativeObject)); } @@ -663,14 +619,10 @@ namespace Microsoft.Z3 /// public Pattern MkPattern(params Expr[] terms) { - Contract.Requires(terms != null); + Debug.Assert(terms != null); if (terms.Length == 0) throw new Z3Exception("Cannot create a pattern from zero terms"); - Contract.Ensures(Contract.Result() != null); - - Contract.EndContractBlock(); - IntPtr[] termsNative = AST.ArrayToNative(terms); return new Pattern(this, Native.Z3_mk_pattern(nCtx, (uint)terms.Length, termsNative)); } @@ -682,9 +634,8 @@ namespace Microsoft.Z3 /// public Expr MkConst(Symbol name, Sort range) { - Contract.Requires(name != null); - Contract.Requires(range != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(name != null); + Debug.Assert(range != null); CheckContextMatch(name); CheckContextMatch(range); @@ -697,8 +648,7 @@ namespace Microsoft.Z3 /// public Expr MkConst(string name, Sort range) { - Contract.Requires(range != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(range != null); return MkConst(MkSymbol(name), range); } @@ -709,8 +659,7 @@ namespace Microsoft.Z3 /// public Expr MkFreshConst(string prefix, Sort range) { - Contract.Requires(range != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(range != null); CheckContextMatch(range); return Expr.Create(this, Native.Z3_mk_fresh_const(nCtx, prefix, range.NativeObject)); @@ -722,8 +671,7 @@ namespace Microsoft.Z3 /// A decl of a 0-arity function public Expr MkConst(FuncDecl f) { - Contract.Requires(f != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(f != null); return MkApp(f); } @@ -733,8 +681,7 @@ namespace Microsoft.Z3 /// public BoolExpr MkBoolConst(Symbol name) { - Contract.Requires(name != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(name != null); return (BoolExpr)MkConst(name, BoolSort); } @@ -744,7 +691,6 @@ namespace Microsoft.Z3 /// public BoolExpr MkBoolConst(string name) { - Contract.Ensures(Contract.Result() != null); return (BoolExpr)MkConst(MkSymbol(name), BoolSort); } @@ -754,8 +700,7 @@ namespace Microsoft.Z3 /// public IntExpr MkIntConst(Symbol name) { - Contract.Requires(name != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(name != null); return (IntExpr)MkConst(name, IntSort); } @@ -765,8 +710,7 @@ namespace Microsoft.Z3 /// public IntExpr MkIntConst(string name) { - Contract.Requires(name != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(name != null); return (IntExpr)MkConst(name, IntSort); } @@ -776,8 +720,7 @@ namespace Microsoft.Z3 /// public RealExpr MkRealConst(Symbol name) { - Contract.Requires(name != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(name != null); return (RealExpr)MkConst(name, RealSort); } @@ -787,7 +730,6 @@ namespace Microsoft.Z3 /// public RealExpr MkRealConst(string name) { - Contract.Ensures(Contract.Result() != null); return (RealExpr)MkConst(name, RealSort); } @@ -797,8 +739,7 @@ namespace Microsoft.Z3 /// public BitVecExpr MkBVConst(Symbol name, uint size) { - Contract.Requires(name != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(name != null); return (BitVecExpr)MkConst(name, MkBitVecSort(size)); } @@ -808,7 +749,6 @@ namespace Microsoft.Z3 /// public BitVecExpr MkBVConst(string name, uint size) { - Contract.Ensures(Contract.Result() != null); return (BitVecExpr)MkConst(name, MkBitVecSort(size)); } @@ -820,9 +760,8 @@ namespace Microsoft.Z3 /// public Expr MkApp(FuncDecl f, params Expr[] args) { - Contract.Requires(f != null); - Contract.Requires(args == null || Contract.ForAll(args, a => a != null)); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(f != null); + Debug.Assert(args == null || args.All(a => a != null)); CheckContextMatch(f); CheckContextMatch(args); @@ -834,9 +773,8 @@ namespace Microsoft.Z3 /// public Expr MkApp(FuncDecl f, IEnumerable args) { - Contract.Requires(f != null); - Contract.Requires(args == null || Contract.ForAll(args, a => a != null)); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(f != null); + Debug.Assert(args == null || args.All( a => a != null)); CheckContextMatch(f); CheckContextMatch(args); @@ -849,7 +787,6 @@ namespace Microsoft.Z3 /// public BoolExpr MkTrue() { - Contract.Ensures(Contract.Result() != null); return new BoolExpr(this, Native.Z3_mk_true(nCtx)); } @@ -859,7 +796,6 @@ namespace Microsoft.Z3 /// public BoolExpr MkFalse() { - Contract.Ensures(Contract.Result() != null); return new BoolExpr(this, Native.Z3_mk_false(nCtx)); } @@ -869,7 +805,6 @@ namespace Microsoft.Z3 /// public BoolExpr MkBool(bool value) { - Contract.Ensures(Contract.Result() != null); return value ? MkTrue() : MkFalse(); } @@ -879,9 +814,8 @@ namespace Microsoft.Z3 /// public BoolExpr MkEq(Expr x, Expr y) { - Contract.Requires(x != null); - Contract.Requires(y != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(x != null); + Debug.Assert(y != null); CheckContextMatch(x); CheckContextMatch(y); @@ -893,10 +827,9 @@ namespace Microsoft.Z3 /// public BoolExpr MkDistinct(params Expr[] args) { - Contract.Requires(args != null); - Contract.Requires(Contract.ForAll(args, a => a != null)); + Debug.Assert(args != null); + Debug.Assert(args.All(a => a != null)); - Contract.Ensures(Contract.Result() != null); CheckContextMatch(args); return new BoolExpr(this, Native.Z3_mk_distinct(nCtx, (uint)args.Length, AST.ArrayToNative(args))); @@ -907,8 +840,7 @@ namespace Microsoft.Z3 /// public BoolExpr MkNot(BoolExpr a) { - Contract.Requires(a != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(a != null); CheckContextMatch(a); return new BoolExpr(this, Native.Z3_mk_not(nCtx, a.NativeObject)); @@ -922,10 +854,9 @@ namespace Microsoft.Z3 /// An expression with the same sort as public Expr MkITE(BoolExpr t1, Expr t2, Expr t3) { - Contract.Requires(t1 != null); - Contract.Requires(t2 != null); - Contract.Requires(t3 != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(t1 != null); + Debug.Assert(t2 != null); + Debug.Assert(t3 != null); CheckContextMatch(t1); CheckContextMatch(t2); @@ -938,9 +869,8 @@ namespace Microsoft.Z3 /// public BoolExpr MkIff(BoolExpr t1, BoolExpr t2) { - Contract.Requires(t1 != null); - Contract.Requires(t2 != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(t1 != null); + Debug.Assert(t2 != null); CheckContextMatch(t1); CheckContextMatch(t2); @@ -952,9 +882,8 @@ namespace Microsoft.Z3 /// public BoolExpr MkImplies(BoolExpr t1, BoolExpr t2) { - Contract.Requires(t1 != null); - Contract.Requires(t2 != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(t1 != null); + Debug.Assert(t2 != null); CheckContextMatch(t1); CheckContextMatch(t2); @@ -966,9 +895,8 @@ namespace Microsoft.Z3 /// public BoolExpr MkXor(BoolExpr t1, BoolExpr t2) { - Contract.Requires(t1 != null); - Contract.Requires(t2 != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(t1 != null); + Debug.Assert(t2 != null); CheckContextMatch(t1); CheckContextMatch(t2); @@ -980,9 +908,8 @@ namespace Microsoft.Z3 /// public BoolExpr MkAnd(params BoolExpr[] t) { - Contract.Requires(t != null); - Contract.Requires(Contract.ForAll(t, a => a != null)); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(t != null); + Debug.Assert(t.All(a => a != null)); CheckContextMatch(t); return new BoolExpr(this, Native.Z3_mk_and(nCtx, (uint)t.Length, AST.ArrayToNative(t))); @@ -993,9 +920,8 @@ namespace Microsoft.Z3 /// public BoolExpr MkAnd(IEnumerable t) { - Contract.Requires(t != null); - Contract.Requires(Contract.ForAll(t, a => a != null)); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(t != null); + Debug.Assert(t.All(a => a != null)); CheckContextMatch(t); return new BoolExpr(this, Native.Z3_mk_and(nCtx, (uint)t.Count(), AST.EnumToNative(t))); } @@ -1005,9 +931,8 @@ namespace Microsoft.Z3 /// public BoolExpr MkOr(params BoolExpr[] t) { - Contract.Requires(t != null); - Contract.Requires(Contract.ForAll(t, a => a != null)); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(t != null); + Debug.Assert(t.All(a => a != null)); CheckContextMatch(t); return new BoolExpr(this, Native.Z3_mk_or(nCtx, (uint)t.Length, AST.ArrayToNative(t))); @@ -1019,9 +944,8 @@ namespace Microsoft.Z3 /// public BoolExpr MkOr(IEnumerable t) { - Contract.Requires(t != null); - Contract.Requires(Contract.ForAll(t, a => a != null)); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(t != null); + Debug.Assert(t.All(a => a != null)); CheckContextMatch(t); return new BoolExpr(this, Native.Z3_mk_or(nCtx, (uint)t.Count(), AST.EnumToNative(t))); @@ -1035,9 +959,8 @@ namespace Microsoft.Z3 /// public ArithExpr MkAdd(params ArithExpr[] t) { - Contract.Requires(t != null); - Contract.Requires(Contract.ForAll(t, a => a != null)); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(t != null); + Debug.Assert(t.All(a => a != null)); CheckContextMatch(t); return (ArithExpr)Expr.Create(this, Native.Z3_mk_add(nCtx, (uint)t.Length, AST.ArrayToNative(t))); @@ -1048,9 +971,8 @@ namespace Microsoft.Z3 /// public ArithExpr MkAdd(IEnumerable t) { - Contract.Requires(t != null); - Contract.Requires(Contract.ForAll(t, a => a != null)); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(t != null); + Debug.Assert(t.All(a => a != null)); CheckContextMatch(t); return (ArithExpr)Expr.Create(this, Native.Z3_mk_add(nCtx, (uint)t.Count(), AST.EnumToNative(t))); @@ -1061,9 +983,8 @@ namespace Microsoft.Z3 /// public ArithExpr MkMul(params ArithExpr[] t) { - Contract.Requires(t != null); - Contract.Requires(Contract.ForAll(t, a => a != null)); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(t != null); + Debug.Assert(t.All(a => a != null)); CheckContextMatch(t); return (ArithExpr)Expr.Create(this, Native.Z3_mk_mul(nCtx, (uint)t.Length, AST.ArrayToNative(t))); @@ -1074,9 +995,8 @@ namespace Microsoft.Z3 /// public ArithExpr MkMul(IEnumerable t) { - Contract.Requires(t != null); - Contract.Requires(Contract.ForAll(t, a => a != null)); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(t != null); + Debug.Assert(t.All(a => a != null)); CheckContextMatch(t); return (ArithExpr)Expr.Create(this, Native.Z3_mk_mul(nCtx, (uint)t.Count(), AST.EnumToNative(t))); @@ -1087,9 +1007,8 @@ namespace Microsoft.Z3 /// public ArithExpr MkSub(params ArithExpr[] t) { - Contract.Requires(t != null); - Contract.Requires(Contract.ForAll(t, a => a != null)); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(t != null); + Debug.Assert(t.All(a => a != null)); CheckContextMatch(t); return (ArithExpr)Expr.Create(this, Native.Z3_mk_sub(nCtx, (uint)t.Length, AST.ArrayToNative(t))); @@ -1100,8 +1019,7 @@ namespace Microsoft.Z3 /// public ArithExpr MkUnaryMinus(ArithExpr t) { - Contract.Requires(t != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(t != null); CheckContextMatch(t); return (ArithExpr)Expr.Create(this, Native.Z3_mk_unary_minus(nCtx, t.NativeObject)); @@ -1112,9 +1030,8 @@ namespace Microsoft.Z3 /// public ArithExpr MkDiv(ArithExpr t1, ArithExpr t2) { - Contract.Requires(t1 != null); - Contract.Requires(t2 != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(t1 != null); + Debug.Assert(t2 != null); CheckContextMatch(t1); CheckContextMatch(t2); @@ -1127,9 +1044,8 @@ namespace Microsoft.Z3 /// The arguments must have int type. public IntExpr MkMod(IntExpr t1, IntExpr t2) { - Contract.Requires(t1 != null); - Contract.Requires(t2 != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(t1 != null); + Debug.Assert(t2 != null); CheckContextMatch(t1); CheckContextMatch(t2); @@ -1142,9 +1058,8 @@ namespace Microsoft.Z3 /// The arguments must have int type. public IntExpr MkRem(IntExpr t1, IntExpr t2) { - Contract.Requires(t1 != null); - Contract.Requires(t2 != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(t1 != null); + Debug.Assert(t2 != null); CheckContextMatch(t1); CheckContextMatch(t2); @@ -1156,9 +1071,8 @@ namespace Microsoft.Z3 /// public ArithExpr MkPower(ArithExpr t1, ArithExpr t2) { - Contract.Requires(t1 != null); - Contract.Requires(t2 != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(t1 != null); + Debug.Assert(t2 != null); CheckContextMatch(t1); CheckContextMatch(t2); @@ -1170,9 +1084,8 @@ namespace Microsoft.Z3 /// public BoolExpr MkLt(ArithExpr t1, ArithExpr t2) { - Contract.Requires(t1 != null); - Contract.Requires(t2 != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(t1 != null); + Debug.Assert(t2 != null); CheckContextMatch(t1); CheckContextMatch(t2); @@ -1184,9 +1097,8 @@ namespace Microsoft.Z3 /// public BoolExpr MkLe(ArithExpr t1, ArithExpr t2) { - Contract.Requires(t1 != null); - Contract.Requires(t2 != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(t1 != null); + Debug.Assert(t2 != null); CheckContextMatch(t1); CheckContextMatch(t2); @@ -1198,9 +1110,8 @@ namespace Microsoft.Z3 /// public BoolExpr MkGt(ArithExpr t1, ArithExpr t2) { - Contract.Requires(t1 != null); - Contract.Requires(t2 != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(t1 != null); + Debug.Assert(t2 != null); CheckContextMatch(t1); CheckContextMatch(t2); @@ -1212,9 +1123,8 @@ namespace Microsoft.Z3 /// public BoolExpr MkGe(ArithExpr t1, ArithExpr t2) { - Contract.Requires(t1 != null); - Contract.Requires(t2 != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(t1 != null); + Debug.Assert(t2 != null); CheckContextMatch(t1); CheckContextMatch(t2); @@ -1233,8 +1143,7 @@ namespace Microsoft.Z3 /// public RealExpr MkInt2Real(IntExpr t) { - Contract.Requires(t != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(t != null); CheckContextMatch(t); return new RealExpr(this, Native.Z3_mk_int2real(nCtx, t.NativeObject)); @@ -1249,8 +1158,7 @@ namespace Microsoft.Z3 /// public IntExpr MkReal2Int(RealExpr t) { - Contract.Requires(t != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(t != null); CheckContextMatch(t); return new IntExpr(this, Native.Z3_mk_real2int(nCtx, t.NativeObject)); @@ -1261,8 +1169,7 @@ namespace Microsoft.Z3 /// public BoolExpr MkIsInteger(RealExpr t) { - Contract.Requires(t != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(t != null); CheckContextMatch(t); return new BoolExpr(this, Native.Z3_mk_is_int(nCtx, t.NativeObject)); @@ -1276,8 +1183,7 @@ namespace Microsoft.Z3 /// The argument must have a bit-vector sort. public BitVecExpr MkBVNot(BitVecExpr t) { - Contract.Requires(t != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(t != null); CheckContextMatch(t); return new BitVecExpr(this, Native.Z3_mk_bvnot(nCtx, t.NativeObject)); @@ -1289,8 +1195,7 @@ namespace Microsoft.Z3 /// The argument must have a bit-vector sort. public BitVecExpr MkBVRedAND(BitVecExpr t) { - Contract.Requires(t != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(t != null); CheckContextMatch(t); return new BitVecExpr(this, Native.Z3_mk_bvredand(nCtx, t.NativeObject)); @@ -1302,8 +1207,7 @@ namespace Microsoft.Z3 /// The argument must have a bit-vector sort. public BitVecExpr MkBVRedOR(BitVecExpr t) { - Contract.Requires(t != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(t != null); CheckContextMatch(t); return new BitVecExpr(this, Native.Z3_mk_bvredor(nCtx, t.NativeObject)); @@ -1315,9 +1219,8 @@ namespace Microsoft.Z3 /// The arguments must have a bit-vector sort. public BitVecExpr MkBVAND(BitVecExpr t1, BitVecExpr t2) { - Contract.Requires(t1 != null); - Contract.Requires(t2 != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(t1 != null); + Debug.Assert(t2 != null); CheckContextMatch(t1); CheckContextMatch(t2); @@ -1330,9 +1233,8 @@ namespace Microsoft.Z3 /// The arguments must have a bit-vector sort. public BitVecExpr MkBVOR(BitVecExpr t1, BitVecExpr t2) { - Contract.Requires(t1 != null); - Contract.Requires(t2 != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(t1 != null); + Debug.Assert(t2 != null); CheckContextMatch(t1); CheckContextMatch(t2); @@ -1345,9 +1247,8 @@ namespace Microsoft.Z3 /// The arguments must have a bit-vector sort. public BitVecExpr MkBVXOR(BitVecExpr t1, BitVecExpr t2) { - Contract.Requires(t1 != null); - Contract.Requires(t2 != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(t1 != null); + Debug.Assert(t2 != null); CheckContextMatch(t1); CheckContextMatch(t2); @@ -1360,9 +1261,8 @@ namespace Microsoft.Z3 /// The arguments must have a bit-vector sort. public BitVecExpr MkBVNAND(BitVecExpr t1, BitVecExpr t2) { - Contract.Requires(t1 != null); - Contract.Requires(t2 != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(t1 != null); + Debug.Assert(t2 != null); CheckContextMatch(t1); CheckContextMatch(t2); @@ -1375,9 +1275,8 @@ namespace Microsoft.Z3 /// The arguments must have a bit-vector sort. public BitVecExpr MkBVNOR(BitVecExpr t1, BitVecExpr t2) { - Contract.Requires(t1 != null); - Contract.Requires(t2 != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(t1 != null); + Debug.Assert(t2 != null); CheckContextMatch(t1); CheckContextMatch(t2); @@ -1390,9 +1289,8 @@ namespace Microsoft.Z3 /// The arguments must have a bit-vector sort. public BitVecExpr MkBVXNOR(BitVecExpr t1, BitVecExpr t2) { - Contract.Requires(t1 != null); - Contract.Requires(t2 != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(t1 != null); + Debug.Assert(t2 != null); CheckContextMatch(t1); CheckContextMatch(t2); @@ -1405,8 +1303,7 @@ namespace Microsoft.Z3 /// The arguments must have a bit-vector sort. public BitVecExpr MkBVNeg(BitVecExpr t) { - Contract.Requires(t != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(t != null); CheckContextMatch(t); return new BitVecExpr(this, Native.Z3_mk_bvneg(nCtx, t.NativeObject)); @@ -1418,9 +1315,8 @@ namespace Microsoft.Z3 /// The arguments must have the same bit-vector sort. public BitVecExpr MkBVAdd(BitVecExpr t1, BitVecExpr t2) { - Contract.Requires(t1 != null); - Contract.Requires(t2 != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(t1 != null); + Debug.Assert(t2 != null); CheckContextMatch(t1); CheckContextMatch(t2); @@ -1433,9 +1329,8 @@ namespace Microsoft.Z3 /// The arguments must have the same bit-vector sort. public BitVecExpr MkBVSub(BitVecExpr t1, BitVecExpr t2) { - Contract.Requires(t1 != null); - Contract.Requires(t2 != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(t1 != null); + Debug.Assert(t2 != null); CheckContextMatch(t1); CheckContextMatch(t2); @@ -1448,9 +1343,8 @@ namespace Microsoft.Z3 /// The arguments must have the same bit-vector sort. public BitVecExpr MkBVMul(BitVecExpr t1, BitVecExpr t2) { - Contract.Requires(t1 != null); - Contract.Requires(t2 != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(t1 != null); + Debug.Assert(t2 != null); CheckContextMatch(t1); CheckContextMatch(t2); @@ -1468,9 +1362,8 @@ namespace Microsoft.Z3 /// public BitVecExpr MkBVUDiv(BitVecExpr t1, BitVecExpr t2) { - Contract.Requires(t1 != null); - Contract.Requires(t2 != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(t1 != null); + Debug.Assert(t2 != null); CheckContextMatch(t1); CheckContextMatch(t2); @@ -1492,9 +1385,8 @@ namespace Microsoft.Z3 /// public BitVecExpr MkBVSDiv(BitVecExpr t1, BitVecExpr t2) { - Contract.Requires(t1 != null); - Contract.Requires(t2 != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(t1 != null); + Debug.Assert(t2 != null); CheckContextMatch(t1); CheckContextMatch(t2); @@ -1511,9 +1403,8 @@ namespace Microsoft.Z3 /// public BitVecExpr MkBVURem(BitVecExpr t1, BitVecExpr t2) { - Contract.Requires(t1 != null); - Contract.Requires(t2 != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(t1 != null); + Debug.Assert(t2 != null); CheckContextMatch(t1); CheckContextMatch(t2); @@ -1532,9 +1423,8 @@ namespace Microsoft.Z3 /// public BitVecExpr MkBVSRem(BitVecExpr t1, BitVecExpr t2) { - Contract.Requires(t1 != null); - Contract.Requires(t2 != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(t1 != null); + Debug.Assert(t2 != null); CheckContextMatch(t1); CheckContextMatch(t2); @@ -1550,9 +1440,8 @@ namespace Microsoft.Z3 /// public BitVecExpr MkBVSMod(BitVecExpr t1, BitVecExpr t2) { - Contract.Requires(t1 != null); - Contract.Requires(t2 != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(t1 != null); + Debug.Assert(t2 != null); CheckContextMatch(t1); CheckContextMatch(t2); @@ -1567,9 +1456,8 @@ namespace Microsoft.Z3 /// public BoolExpr MkBVULT(BitVecExpr t1, BitVecExpr t2) { - Contract.Requires(t1 != null); - Contract.Requires(t2 != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(t1 != null); + Debug.Assert(t2 != null); CheckContextMatch(t1); CheckContextMatch(t2); @@ -1584,9 +1472,8 @@ namespace Microsoft.Z3 /// public BoolExpr MkBVSLT(BitVecExpr t1, BitVecExpr t2) { - Contract.Requires(t1 != null); - Contract.Requires(t2 != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(t1 != null); + Debug.Assert(t2 != null); CheckContextMatch(t1); CheckContextMatch(t2); @@ -1601,9 +1488,8 @@ namespace Microsoft.Z3 /// public BoolExpr MkBVULE(BitVecExpr t1, BitVecExpr t2) { - Contract.Requires(t1 != null); - Contract.Requires(t2 != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(t1 != null); + Debug.Assert(t2 != null); CheckContextMatch(t1); CheckContextMatch(t2); @@ -1618,9 +1504,8 @@ namespace Microsoft.Z3 /// public BoolExpr MkBVSLE(BitVecExpr t1, BitVecExpr t2) { - Contract.Requires(t1 != null); - Contract.Requires(t2 != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(t1 != null); + Debug.Assert(t2 != null); CheckContextMatch(t1); CheckContextMatch(t2); @@ -1635,9 +1520,8 @@ namespace Microsoft.Z3 /// public BoolExpr MkBVUGE(BitVecExpr t1, BitVecExpr t2) { - Contract.Requires(t1 != null); - Contract.Requires(t2 != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(t1 != null); + Debug.Assert(t2 != null); CheckContextMatch(t1); CheckContextMatch(t2); @@ -1652,9 +1536,8 @@ namespace Microsoft.Z3 /// public BoolExpr MkBVSGE(BitVecExpr t1, BitVecExpr t2) { - Contract.Requires(t1 != null); - Contract.Requires(t2 != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(t1 != null); + Debug.Assert(t2 != null); CheckContextMatch(t1); CheckContextMatch(t2); @@ -1669,9 +1552,8 @@ namespace Microsoft.Z3 /// public BoolExpr MkBVUGT(BitVecExpr t1, BitVecExpr t2) { - Contract.Requires(t1 != null); - Contract.Requires(t2 != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(t1 != null); + Debug.Assert(t2 != null); CheckContextMatch(t1); CheckContextMatch(t2); @@ -1686,9 +1568,8 @@ namespace Microsoft.Z3 /// public BoolExpr MkBVSGT(BitVecExpr t1, BitVecExpr t2) { - Contract.Requires(t1 != null); - Contract.Requires(t2 != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(t1 != null); + Debug.Assert(t2 != null); CheckContextMatch(t1); CheckContextMatch(t2); @@ -1707,9 +1588,8 @@ namespace Microsoft.Z3 /// public BitVecExpr MkConcat(BitVecExpr t1, BitVecExpr t2) { - Contract.Requires(t1 != null); - Contract.Requires(t2 != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(t1 != null); + Debug.Assert(t2 != null); CheckContextMatch(t1); CheckContextMatch(t2); @@ -1727,8 +1607,7 @@ namespace Microsoft.Z3 /// public BitVecExpr MkExtract(uint high, uint low, BitVecExpr t) { - Contract.Requires(t != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(t != null); CheckContextMatch(t); return new BitVecExpr(this, Native.Z3_mk_extract(nCtx, high, low, t.NativeObject)); @@ -1744,8 +1623,7 @@ namespace Microsoft.Z3 /// public BitVecExpr MkSignExt(uint i, BitVecExpr t) { - Contract.Requires(t != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(t != null); CheckContextMatch(t); return new BitVecExpr(this, Native.Z3_mk_sign_ext(nCtx, i, t.NativeObject)); @@ -1762,8 +1640,7 @@ namespace Microsoft.Z3 /// public BitVecExpr MkZeroExt(uint i, BitVecExpr t) { - Contract.Requires(t != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(t != null); CheckContextMatch(t); return new BitVecExpr(this, Native.Z3_mk_zero_ext(nCtx, i, t.NativeObject)); @@ -1777,8 +1654,7 @@ namespace Microsoft.Z3 /// public BitVecExpr MkRepeat(uint i, BitVecExpr t) { - Contract.Requires(t != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(t != null); CheckContextMatch(t); return new BitVecExpr(this, Native.Z3_mk_repeat(nCtx, i, t.NativeObject)); @@ -1798,9 +1674,8 @@ namespace Microsoft.Z3 /// public BitVecExpr MkBVSHL(BitVecExpr t1, BitVecExpr t2) { - Contract.Requires(t1 != null); - Contract.Requires(t2 != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(t1 != null); + Debug.Assert(t2 != null); CheckContextMatch(t1); CheckContextMatch(t2); @@ -1821,9 +1696,8 @@ namespace Microsoft.Z3 /// public BitVecExpr MkBVLSHR(BitVecExpr t1, BitVecExpr t2) { - Contract.Requires(t1 != null); - Contract.Requires(t2 != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(t1 != null); + Debug.Assert(t2 != null); CheckContextMatch(t1); CheckContextMatch(t2); @@ -1846,9 +1720,8 @@ namespace Microsoft.Z3 /// public BitVecExpr MkBVASHR(BitVecExpr t1, BitVecExpr t2) { - Contract.Requires(t1 != null); - Contract.Requires(t2 != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(t1 != null); + Debug.Assert(t2 != null); CheckContextMatch(t1); CheckContextMatch(t2); @@ -1864,8 +1737,7 @@ namespace Microsoft.Z3 /// public BitVecExpr MkBVRotateLeft(uint i, BitVecExpr t) { - Contract.Requires(t != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(t != null); CheckContextMatch(t); return new BitVecExpr(this, Native.Z3_mk_rotate_left(nCtx, i, t.NativeObject)); @@ -1880,8 +1752,7 @@ namespace Microsoft.Z3 /// public BitVecExpr MkBVRotateRight(uint i, BitVecExpr t) { - Contract.Requires(t != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(t != null); CheckContextMatch(t); return new BitVecExpr(this, Native.Z3_mk_rotate_right(nCtx, i, t.NativeObject)); @@ -1896,9 +1767,8 @@ namespace Microsoft.Z3 /// public BitVecExpr MkBVRotateLeft(BitVecExpr t1, BitVecExpr t2) { - Contract.Requires(t1 != null); - Contract.Requires(t2 != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(t1 != null); + Debug.Assert(t2 != null); CheckContextMatch(t1); CheckContextMatch(t2); @@ -1914,9 +1784,8 @@ namespace Microsoft.Z3 /// public BitVecExpr MkBVRotateRight(BitVecExpr t1, BitVecExpr t2) { - Contract.Requires(t1 != null); - Contract.Requires(t2 != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(t1 != null); + Debug.Assert(t2 != null); CheckContextMatch(t1); CheckContextMatch(t2); @@ -1935,8 +1804,7 @@ namespace Microsoft.Z3 /// public BitVecExpr MkInt2BV(uint n, IntExpr t) { - Contract.Requires(t != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(t != null); CheckContextMatch(t); return new BitVecExpr(this, Native.Z3_mk_int2bv(nCtx, n, t.NativeObject)); @@ -1959,8 +1827,7 @@ namespace Microsoft.Z3 /// public IntExpr MkBV2Int(BitVecExpr t, bool signed) { - Contract.Requires(t != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(t != null); CheckContextMatch(t); return new IntExpr(this, Native.Z3_mk_bv2int(nCtx, t.NativeObject, (byte)(signed ? 1 : 0))); @@ -1974,9 +1841,8 @@ namespace Microsoft.Z3 /// public BoolExpr MkBVAddNoOverflow(BitVecExpr t1, BitVecExpr t2, bool isSigned) { - Contract.Requires(t1 != null); - Contract.Requires(t2 != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(t1 != null); + Debug.Assert(t2 != null); CheckContextMatch(t1); CheckContextMatch(t2); @@ -1991,9 +1857,8 @@ namespace Microsoft.Z3 /// public BoolExpr MkBVAddNoUnderflow(BitVecExpr t1, BitVecExpr t2) { - Contract.Requires(t1 != null); - Contract.Requires(t2 != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(t1 != null); + Debug.Assert(t2 != null); CheckContextMatch(t1); CheckContextMatch(t2); @@ -2008,9 +1873,8 @@ namespace Microsoft.Z3 /// public BoolExpr MkBVSubNoOverflow(BitVecExpr t1, BitVecExpr t2) { - Contract.Requires(t1 != null); - Contract.Requires(t2 != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(t1 != null); + Debug.Assert(t2 != null); CheckContextMatch(t1); CheckContextMatch(t2); @@ -2025,9 +1889,8 @@ namespace Microsoft.Z3 /// public BoolExpr MkBVSubNoUnderflow(BitVecExpr t1, BitVecExpr t2, bool isSigned) { - Contract.Requires(t1 != null); - Contract.Requires(t2 != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(t1 != null); + Debug.Assert(t2 != null); CheckContextMatch(t1); CheckContextMatch(t2); @@ -2042,9 +1905,8 @@ namespace Microsoft.Z3 /// public BoolExpr MkBVSDivNoOverflow(BitVecExpr t1, BitVecExpr t2) { - Contract.Requires(t1 != null); - Contract.Requires(t2 != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(t1 != null); + Debug.Assert(t2 != null); CheckContextMatch(t1); CheckContextMatch(t2); @@ -2059,8 +1921,7 @@ namespace Microsoft.Z3 /// public BoolExpr MkBVNegNoOverflow(BitVecExpr t) { - Contract.Requires(t != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(t != null); CheckContextMatch(t); return new BoolExpr(this, Native.Z3_mk_bvneg_no_overflow(nCtx, t.NativeObject)); @@ -2074,9 +1935,8 @@ namespace Microsoft.Z3 /// public BoolExpr MkBVMulNoOverflow(BitVecExpr t1, BitVecExpr t2, bool isSigned) { - Contract.Requires(t1 != null); - Contract.Requires(t2 != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(t1 != null); + Debug.Assert(t2 != null); CheckContextMatch(t1); CheckContextMatch(t2); @@ -2091,9 +1951,8 @@ namespace Microsoft.Z3 /// public BoolExpr MkBVMulNoUnderflow(BitVecExpr t1, BitVecExpr t2) { - Contract.Requires(t1 != null); - Contract.Requires(t2 != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(t1 != null); + Debug.Assert(t2 != null); CheckContextMatch(t1); CheckContextMatch(t2); @@ -2107,10 +1966,9 @@ namespace Microsoft.Z3 /// public ArrayExpr MkArrayConst(Symbol name, Sort domain, Sort range) { - Contract.Requires(name != null); - Contract.Requires(domain != null); - Contract.Requires(range != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(name != null); + Debug.Assert(domain != null); + Debug.Assert(range != null); return (ArrayExpr)MkConst(name, MkArraySort(domain, range)); } @@ -2120,9 +1978,8 @@ namespace Microsoft.Z3 /// public ArrayExpr MkArrayConst(string name, Sort domain, Sort range) { - Contract.Requires(domain != null); - Contract.Requires(range != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(domain != null); + Debug.Assert(range != null); return (ArrayExpr)MkConst(MkSymbol(name), MkArraySort(domain, range)); } @@ -2143,9 +2000,8 @@ namespace Microsoft.Z3 /// public Expr MkSelect(ArrayExpr a, Expr i) { - Contract.Requires(a != null); - Contract.Requires(i != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(a != null); + Debug.Assert(i != null); CheckContextMatch(a); CheckContextMatch(i); @@ -2167,9 +2023,8 @@ namespace Microsoft.Z3 /// public Expr MkSelect(ArrayExpr a, params Expr[] args) { - Contract.Requires(a != null); - Contract.Requires(args != null && Contract.ForAll(args, n => n != null)); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(a != null); + Debug.Assert(args != null && args.All(n => n != null)); CheckContextMatch(a); CheckContextMatch(args); @@ -2196,10 +2051,9 @@ namespace Microsoft.Z3 /// public ArrayExpr MkStore(ArrayExpr a, Expr i, Expr v) { - Contract.Requires(a != null); - Contract.Requires(i != null); - Contract.Requires(v != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(a != null); + Debug.Assert(i != null); + Debug.Assert(v != null); CheckContextMatch(a); CheckContextMatch(i); @@ -2227,10 +2081,9 @@ namespace Microsoft.Z3 /// public ArrayExpr MkStore(ArrayExpr a, Expr[] args, Expr v) { - Contract.Requires(a != null); - Contract.Requires(args != null); - Contract.Requires(v != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(a != null); + Debug.Assert(args != null); + Debug.Assert(v != null); CheckContextMatch(args); CheckContextMatch(a); @@ -2249,9 +2102,8 @@ namespace Microsoft.Z3 /// public ArrayExpr MkConstArray(Sort domain, Expr v) { - Contract.Requires(domain != null); - Contract.Requires(v != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(domain != null); + Debug.Assert(v != null); CheckContextMatch(domain); CheckContextMatch(v); @@ -2271,9 +2123,8 @@ namespace Microsoft.Z3 /// public ArrayExpr MkMap(FuncDecl f, params ArrayExpr[] args) { - Contract.Requires(f != null); - Contract.Requires(args == null || Contract.ForAll(args, a => a != null)); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(f != null); + Debug.Assert(args == null || args.All(a => a != null)); CheckContextMatch(f); CheckContextMatch(args); @@ -2289,8 +2140,7 @@ namespace Microsoft.Z3 /// public Expr MkTermArray(ArrayExpr array) { - Contract.Requires(array != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(array != null); CheckContextMatch(array); return Expr.Create(this, Native.Z3_mk_array_default(nCtx, array.NativeObject)); @@ -2301,9 +2151,8 @@ namespace Microsoft.Z3 /// public Expr MkArrayExt(ArrayExpr arg1, ArrayExpr arg2) { - Contract.Requires(arg1 != null); - Contract.Requires(arg2 != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(arg1 != null); + Debug.Assert(arg2 != null); CheckContextMatch(arg1); CheckContextMatch(arg2); @@ -2318,8 +2167,7 @@ namespace Microsoft.Z3 /// public SetSort MkSetSort(Sort ty) { - Contract.Requires(ty != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(ty != null); CheckContextMatch(ty); return new SetSort(this, ty); @@ -2330,8 +2178,7 @@ namespace Microsoft.Z3 /// public ArrayExpr MkEmptySet(Sort domain) { - Contract.Requires(domain != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(domain != null); CheckContextMatch(domain); return (ArrayExpr)Expr.Create(this, Native.Z3_mk_empty_set(nCtx, domain.NativeObject)); @@ -2342,8 +2189,7 @@ namespace Microsoft.Z3 /// public ArrayExpr MkFullSet(Sort domain) { - Contract.Requires(domain != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(domain != null); CheckContextMatch(domain); return (ArrayExpr)Expr.Create(this, Native.Z3_mk_full_set(nCtx, domain.NativeObject)); @@ -2354,9 +2200,8 @@ namespace Microsoft.Z3 /// public ArrayExpr MkSetAdd(ArrayExpr set, Expr element) { - Contract.Requires(set != null); - Contract.Requires(element != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(set != null); + Debug.Assert(element != null); CheckContextMatch(set); CheckContextMatch(element); @@ -2369,9 +2214,8 @@ namespace Microsoft.Z3 /// public ArrayExpr MkSetDel(ArrayExpr set, Expr element) { - Contract.Requires(set != null); - Contract.Requires(element != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(set != null); + Debug.Assert(element != null); CheckContextMatch(set); CheckContextMatch(element); @@ -2383,8 +2227,8 @@ namespace Microsoft.Z3 /// public ArrayExpr MkSetUnion(params ArrayExpr[] args) { - Contract.Requires(args != null); - Contract.Requires(Contract.ForAll(args, a => a != null)); + Debug.Assert(args != null); + Debug.Assert(args.All(a => a != null)); CheckContextMatch(args); return (ArrayExpr)Expr.Create(this, Native.Z3_mk_set_union(nCtx, (uint)args.Length, AST.ArrayToNative(args))); @@ -2395,9 +2239,8 @@ namespace Microsoft.Z3 /// public ArrayExpr MkSetIntersection(params ArrayExpr[] args) { - Contract.Requires(args != null); - Contract.Requires(Contract.ForAll(args, a => a != null)); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(args != null); + Debug.Assert(args.All(a => a != null)); CheckContextMatch(args); return (ArrayExpr)Expr.Create(this, Native.Z3_mk_set_intersect(nCtx, (uint)args.Length, AST.ArrayToNative(args))); @@ -2408,9 +2251,8 @@ namespace Microsoft.Z3 /// public ArrayExpr MkSetDifference(ArrayExpr arg1, ArrayExpr arg2) { - Contract.Requires(arg1 != null); - Contract.Requires(arg2 != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(arg1 != null); + Debug.Assert(arg2 != null); CheckContextMatch(arg1); CheckContextMatch(arg2); @@ -2422,8 +2264,7 @@ namespace Microsoft.Z3 /// public ArrayExpr MkSetComplement(ArrayExpr arg) { - Contract.Requires(arg != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(arg != null); CheckContextMatch(arg); return (ArrayExpr)Expr.Create(this, Native.Z3_mk_set_complement(nCtx, arg.NativeObject)); @@ -2434,9 +2275,8 @@ namespace Microsoft.Z3 /// public BoolExpr MkSetMembership(Expr elem, ArrayExpr set) { - Contract.Requires(elem != null); - Contract.Requires(set != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(elem != null); + Debug.Assert(set != null); CheckContextMatch(elem); CheckContextMatch(set); @@ -2448,9 +2288,8 @@ namespace Microsoft.Z3 /// public BoolExpr MkSetSubset(ArrayExpr arg1, ArrayExpr arg2) { - Contract.Requires(arg1 != null); - Contract.Requires(arg2 != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(arg1 != null); + Debug.Assert(arg2 != null); CheckContextMatch(arg1); CheckContextMatch(arg2); @@ -2466,8 +2305,7 @@ namespace Microsoft.Z3 /// public SeqExpr MkEmptySeq(Sort s) { - Contract.Requires(s != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(s != null); return new SeqExpr(this, Native.Z3_mk_seq_empty(nCtx, s.NativeObject)); } @@ -2476,8 +2314,7 @@ namespace Microsoft.Z3 /// public SeqExpr MkUnit(Expr elem) { - Contract.Requires(elem != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(elem != null); return new SeqExpr(this, Native.Z3_mk_seq_unit(nCtx, elem.NativeObject)); } @@ -2486,8 +2323,7 @@ namespace Microsoft.Z3 /// public SeqExpr MkString(string s) { - Contract.Requires(s != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(s != null); return new SeqExpr(this, Native.Z3_mk_string(nCtx, s)); } @@ -2496,9 +2332,8 @@ namespace Microsoft.Z3 /// public SeqExpr IntToString(Expr e) { - Contract.Requires(e != null); - Contract.Requires(e is ArithExpr); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(e != null); + Debug.Assert(e is ArithExpr); return new SeqExpr(this, Native.Z3_mk_int_to_str(nCtx, e.NativeObject)); } @@ -2507,9 +2342,8 @@ namespace Microsoft.Z3 /// public IntExpr StringToInt(Expr e) { - Contract.Requires(e != null); - Contract.Requires(e is SeqExpr); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(e != null); + Debug.Assert(e is SeqExpr); return new IntExpr(this, Native.Z3_mk_str_to_int(nCtx, e.NativeObject)); } @@ -2519,9 +2353,8 @@ namespace Microsoft.Z3 /// public SeqExpr MkConcat(params SeqExpr[] t) { - Contract.Requires(t != null); - Contract.Requires(Contract.ForAll(t, a => a != null)); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(t != null); + Debug.Assert(t.All(a => a != null)); CheckContextMatch(t); return new SeqExpr(this, Native.Z3_mk_seq_concat(nCtx, (uint)t.Length, AST.ArrayToNative(t))); @@ -2533,8 +2366,7 @@ namespace Microsoft.Z3 /// public IntExpr MkLength(SeqExpr s) { - Contract.Requires(s != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(s != null); return (IntExpr) Expr.Create(this, Native.Z3_mk_seq_length(nCtx, s.NativeObject)); } @@ -2543,9 +2375,8 @@ namespace Microsoft.Z3 /// public BoolExpr MkPrefixOf(SeqExpr s1, SeqExpr s2) { - Contract.Requires(s1 != null); - Contract.Requires(s2 != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(s1 != null); + Debug.Assert(s2 != null); CheckContextMatch(s1, s2); return new BoolExpr(this, Native.Z3_mk_seq_prefix(nCtx, s1.NativeObject, s2.NativeObject)); } @@ -2555,9 +2386,8 @@ namespace Microsoft.Z3 /// public BoolExpr MkSuffixOf(SeqExpr s1, SeqExpr s2) { - Contract.Requires(s1 != null); - Contract.Requires(s2 != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(s1 != null); + Debug.Assert(s2 != null); CheckContextMatch(s1, s2); return new BoolExpr(this, Native.Z3_mk_seq_suffix(nCtx, s1.NativeObject, s2.NativeObject)); } @@ -2567,9 +2397,8 @@ namespace Microsoft.Z3 /// public BoolExpr MkContains(SeqExpr s1, SeqExpr s2) { - Contract.Requires(s1 != null); - Contract.Requires(s2 != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(s1 != null); + Debug.Assert(s2 != null); CheckContextMatch(s1, s2); return new BoolExpr(this, Native.Z3_mk_seq_contains(nCtx, s1.NativeObject, s2.NativeObject)); } @@ -2579,9 +2408,8 @@ namespace Microsoft.Z3 /// public SeqExpr MkAt(SeqExpr s, IntExpr index) { - Contract.Requires(s != null); - Contract.Requires(index != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(s != null); + Debug.Assert(index != null); CheckContextMatch(s, index); return new SeqExpr(this, Native.Z3_mk_seq_at(nCtx, s.NativeObject, index.NativeObject)); } @@ -2591,10 +2419,9 @@ namespace Microsoft.Z3 /// public SeqExpr MkExtract(SeqExpr s, IntExpr offset, IntExpr length) { - Contract.Requires(s != null); - Contract.Requires(offset != null); - Contract.Requires(length != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(s != null); + Debug.Assert(offset != null); + Debug.Assert(length != null); CheckContextMatch(s, offset, length); return new SeqExpr(this, Native.Z3_mk_seq_extract(nCtx, s.NativeObject, offset.NativeObject, length.NativeObject)); } @@ -2604,10 +2431,9 @@ namespace Microsoft.Z3 /// public IntExpr MkIndexOf(SeqExpr s, SeqExpr substr, ArithExpr offset) { - Contract.Requires(s != null); - Contract.Requires(offset != null); - Contract.Requires(substr != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(s != null); + Debug.Assert(offset != null); + Debug.Assert(substr != null); CheckContextMatch(s, substr, offset); return new IntExpr(this, Native.Z3_mk_seq_index(nCtx, s.NativeObject, substr.NativeObject, offset.NativeObject)); } @@ -2617,10 +2443,9 @@ namespace Microsoft.Z3 /// public SeqExpr MkReplace(SeqExpr s, SeqExpr src, SeqExpr dst) { - Contract.Requires(s != null); - Contract.Requires(src != null); - Contract.Requires(dst != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(s != null); + Debug.Assert(src != null); + Debug.Assert(dst != null); CheckContextMatch(s, src, dst); return new SeqExpr(this, Native.Z3_mk_seq_replace(nCtx, s.NativeObject, src.NativeObject, dst.NativeObject)); } @@ -2630,8 +2455,7 @@ namespace Microsoft.Z3 /// public ReExpr MkToRe(SeqExpr s) { - Contract.Requires(s != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(s != null); return new ReExpr(this, Native.Z3_mk_seq_to_re(nCtx, s.NativeObject)); } @@ -2641,9 +2465,8 @@ namespace Microsoft.Z3 /// public BoolExpr MkInRe(SeqExpr s, ReExpr re) { - Contract.Requires(s != null); - Contract.Requires(re != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(s != null); + Debug.Assert(re != null); CheckContextMatch(s, re); return new BoolExpr(this, Native.Z3_mk_seq_in_re(nCtx, s.NativeObject, re.NativeObject)); } @@ -2653,8 +2476,7 @@ namespace Microsoft.Z3 /// public ReExpr MkStar(ReExpr re) { - Contract.Requires(re != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(re != null); return new ReExpr(this, Native.Z3_mk_re_star(nCtx, re.NativeObject)); } @@ -2663,8 +2485,7 @@ namespace Microsoft.Z3 /// public ReExpr MkLoop(ReExpr re, uint lo, uint hi = 0) { - Contract.Requires(re != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(re != null); return new ReExpr(this, Native.Z3_mk_re_loop(nCtx, re.NativeObject, lo, hi)); } @@ -2673,8 +2494,7 @@ namespace Microsoft.Z3 /// public ReExpr MkPlus(ReExpr re) { - Contract.Requires(re != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(re != null); return new ReExpr(this, Native.Z3_mk_re_plus(nCtx, re.NativeObject)); } @@ -2683,8 +2503,7 @@ namespace Microsoft.Z3 /// public ReExpr MkOption(ReExpr re) { - Contract.Requires(re != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(re != null); return new ReExpr(this, Native.Z3_mk_re_option(nCtx, re.NativeObject)); } @@ -2693,8 +2512,7 @@ namespace Microsoft.Z3 /// public ReExpr MkComplement(ReExpr re) { - Contract.Requires(re != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(re != null); return new ReExpr(this, Native.Z3_mk_re_complement(nCtx, re.NativeObject)); } @@ -2703,9 +2521,8 @@ namespace Microsoft.Z3 /// public ReExpr MkConcat(params ReExpr[] t) { - Contract.Requires(t != null); - Contract.Requires(Contract.ForAll(t, a => a != null)); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(t != null); + Debug.Assert(t.All(a => a != null)); CheckContextMatch(t); return new ReExpr(this, Native.Z3_mk_re_concat(nCtx, (uint)t.Length, AST.ArrayToNative(t))); @@ -2716,9 +2533,8 @@ namespace Microsoft.Z3 /// public ReExpr MkUnion(params ReExpr[] t) { - Contract.Requires(t != null); - Contract.Requires(Contract.ForAll(t, a => a != null)); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(t != null); + Debug.Assert(t.All(a => a != null)); CheckContextMatch(t); return new ReExpr(this, Native.Z3_mk_re_union(nCtx, (uint)t.Length, AST.ArrayToNative(t))); @@ -2729,9 +2545,8 @@ namespace Microsoft.Z3 /// public ReExpr MkIntersect(params ReExpr[] t) { - Contract.Requires(t != null); - Contract.Requires(Contract.ForAll(t, a => a != null)); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(t != null); + Debug.Assert(t.All(a => a != null)); CheckContextMatch(t); return new ReExpr(this, Native.Z3_mk_re_intersect(nCtx, (uint)t.Length, AST.ArrayToNative(t))); @@ -2742,8 +2557,7 @@ namespace Microsoft.Z3 /// public ReExpr MkEmptyRe(Sort s) { - Contract.Requires(s != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(s != null); return new ReExpr(this, Native.Z3_mk_re_empty(nCtx, s.NativeObject)); } @@ -2752,8 +2566,7 @@ namespace Microsoft.Z3 /// public ReExpr MkFullRe(Sort s) { - Contract.Requires(s != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(s != null); return new ReExpr(this, Native.Z3_mk_re_full(nCtx, s.NativeObject)); } @@ -2763,9 +2576,8 @@ namespace Microsoft.Z3 /// public ReExpr MkRange(SeqExpr lo, SeqExpr hi) { - Contract.Requires(lo != null); - Contract.Requires(hi != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(lo != null); + Debug.Assert(hi != null); CheckContextMatch(lo, hi); return new ReExpr(this, Native.Z3_mk_re_range(nCtx, lo.NativeObject, hi.NativeObject)); } @@ -2779,8 +2591,7 @@ namespace Microsoft.Z3 /// public BoolExpr MkAtMost(IEnumerable args, uint k) { - Contract.Requires(args != null); - Contract.Requires(Contract.Result() != null); + Debug.Assert(args != null); CheckContextMatch(args); return new BoolExpr(this, Native.Z3_mk_atmost(nCtx, (uint) args.Count(), AST.EnumToNative(args), k)); @@ -2791,8 +2602,7 @@ namespace Microsoft.Z3 /// public BoolExpr MkAtLeast(IEnumerable args, uint k) { - Contract.Requires(args != null); - Contract.Requires(Contract.Result() != null); + Debug.Assert(args != null); CheckContextMatch(args); return new BoolExpr(this, Native.Z3_mk_atleast(nCtx, (uint) args.Count(), AST.EnumToNative(args), k)); @@ -2803,10 +2613,9 @@ namespace Microsoft.Z3 /// public BoolExpr MkPBLe(int[] coeffs, BoolExpr[] args, int k) { - Contract.Requires(args != null); - Contract.Requires(coeffs != null); - Contract.Requires(args.Length == coeffs.Length); - Contract.Requires(Contract.Result() != null); + Debug.Assert(args != null); + Debug.Assert(coeffs != null); + Debug.Assert(args.Length == coeffs.Length); CheckContextMatch(args); return new BoolExpr(this, Native.Z3_mk_pble(nCtx, (uint) args.Length, AST.ArrayToNative(args), @@ -2818,10 +2627,9 @@ namespace Microsoft.Z3 /// public BoolExpr MkPBGe(int[] coeffs, BoolExpr[] args, int k) { - Contract.Requires(args != null); - Contract.Requires(coeffs != null); - Contract.Requires(args.Length == coeffs.Length); - Contract.Requires(Contract.Result() != null); + Debug.Assert(args != null); + Debug.Assert(coeffs != null); + Debug.Assert(args.Length == coeffs.Length); CheckContextMatch(args); return new BoolExpr(this, Native.Z3_mk_pbge(nCtx, (uint) args.Length, AST.ArrayToNative(args), @@ -2832,10 +2640,9 @@ namespace Microsoft.Z3 /// public BoolExpr MkPBEq(int[] coeffs, BoolExpr[] args, int k) { - Contract.Requires(args != null); - Contract.Requires(coeffs != null); - Contract.Requires(args.Length == coeffs.Length); - Contract.Requires(Contract.Result() != null); + Debug.Assert(args != null); + Debug.Assert(coeffs != null); + Debug.Assert(args.Length == coeffs.Length); CheckContextMatch(args); return new BoolExpr(this, Native.Z3_mk_pbeq(nCtx, (uint) args.Length, AST.ArrayToNative(args), @@ -2854,8 +2661,7 @@ namespace Microsoft.Z3 /// A Term with value and sort public Expr MkNumeral(string v, Sort ty) { - Contract.Requires(ty != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(ty != null); CheckContextMatch(ty); return Expr.Create(this, Native.Z3_mk_numeral(nCtx, v, ty.NativeObject)); @@ -2870,8 +2676,7 @@ namespace Microsoft.Z3 /// A Term with value and type public Expr MkNumeral(int v, Sort ty) { - Contract.Requires(ty != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(ty != null); CheckContextMatch(ty); return Expr.Create(this, Native.Z3_mk_int(nCtx, v, ty.NativeObject)); @@ -2886,8 +2691,7 @@ namespace Microsoft.Z3 /// A Term with value and type public Expr MkNumeral(uint v, Sort ty) { - Contract.Requires(ty != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(ty != null); CheckContextMatch(ty); return Expr.Create(this, Native.Z3_mk_unsigned_int(nCtx, v, ty.NativeObject)); @@ -2902,8 +2706,7 @@ namespace Microsoft.Z3 /// A Term with value and type public Expr MkNumeral(long v, Sort ty) { - Contract.Requires(ty != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(ty != null); CheckContextMatch(ty); return Expr.Create(this, Native.Z3_mk_int64(nCtx, v, ty.NativeObject)); @@ -2918,8 +2721,7 @@ namespace Microsoft.Z3 /// A Term with value and type public Expr MkNumeral(ulong v, Sort ty) { - Contract.Requires(ty != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(ty != null); CheckContextMatch(ty); return Expr.Create(this, Native.Z3_mk_unsigned_int64(nCtx, v, ty.NativeObject)); @@ -2939,9 +2741,6 @@ namespace Microsoft.Z3 if (den == 0) throw new Z3Exception("Denominator is zero"); - Contract.Ensures(Contract.Result() != null); - Contract.EndContractBlock(); - return new RatNum(this, Native.Z3_mk_real(nCtx, num, den)); } @@ -2952,7 +2751,6 @@ namespace Microsoft.Z3 /// A Term with value and sort Real public RatNum MkReal(string v) { - Contract.Ensures(Contract.Result() != null); return new RatNum(this, Native.Z3_mk_numeral(nCtx, v, RealSort.NativeObject)); } @@ -2964,7 +2762,6 @@ namespace Microsoft.Z3 /// A Term with value and sort Real public RatNum MkReal(int v) { - Contract.Ensures(Contract.Result() != null); return new RatNum(this, Native.Z3_mk_int(nCtx, v, RealSort.NativeObject)); } @@ -2976,7 +2773,6 @@ namespace Microsoft.Z3 /// A Term with value and sort Real public RatNum MkReal(uint v) { - Contract.Ensures(Contract.Result() != null); return new RatNum(this, Native.Z3_mk_unsigned_int(nCtx, v, RealSort.NativeObject)); } @@ -2988,7 +2784,6 @@ namespace Microsoft.Z3 /// A Term with value and sort Real public RatNum MkReal(long v) { - Contract.Ensures(Contract.Result() != null); return new RatNum(this, Native.Z3_mk_int64(nCtx, v, RealSort.NativeObject)); } @@ -3000,7 +2795,6 @@ namespace Microsoft.Z3 /// A Term with value and sort Real public RatNum MkReal(ulong v) { - Contract.Ensures(Contract.Result() != null); return new RatNum(this, Native.Z3_mk_unsigned_int64(nCtx, v, RealSort.NativeObject)); } @@ -3013,7 +2807,6 @@ namespace Microsoft.Z3 /// A string representing the Term value in decimal notation. public IntNum MkInt(string v) { - Contract.Ensures(Contract.Result() != null); return new IntNum(this, Native.Z3_mk_numeral(nCtx, v, IntSort.NativeObject)); } @@ -3025,7 +2818,6 @@ namespace Microsoft.Z3 /// A Term with value and sort Integer public IntNum MkInt(int v) { - Contract.Ensures(Contract.Result() != null); return new IntNum(this, Native.Z3_mk_int(nCtx, v, IntSort.NativeObject)); } @@ -3037,7 +2829,6 @@ namespace Microsoft.Z3 /// A Term with value and sort Integer public IntNum MkInt(uint v) { - Contract.Ensures(Contract.Result() != null); return new IntNum(this, Native.Z3_mk_unsigned_int(nCtx, v, IntSort.NativeObject)); } @@ -3049,7 +2840,6 @@ namespace Microsoft.Z3 /// A Term with value and sort Integer public IntNum MkInt(long v) { - Contract.Ensures(Contract.Result() != null); return new IntNum(this, Native.Z3_mk_int64(nCtx, v, IntSort.NativeObject)); } @@ -3061,7 +2851,6 @@ namespace Microsoft.Z3 /// A Term with value and sort Integer public IntNum MkInt(ulong v) { - Contract.Ensures(Contract.Result() != null); return new IntNum(this, Native.Z3_mk_unsigned_int64(nCtx, v, IntSort.NativeObject)); } @@ -3075,7 +2864,6 @@ namespace Microsoft.Z3 /// the size of the bit-vector public BitVecNum MkBV(string v, uint size) { - Contract.Ensures(Contract.Result() != null); return (BitVecNum)MkNumeral(v, MkBitVecSort(size)); } @@ -3087,7 +2875,6 @@ namespace Microsoft.Z3 /// the size of the bit-vector public BitVecNum MkBV(int v, uint size) { - Contract.Ensures(Contract.Result() != null); return (BitVecNum)MkNumeral(v, MkBitVecSort(size)); } @@ -3099,7 +2886,6 @@ namespace Microsoft.Z3 /// the size of the bit-vector public BitVecNum MkBV(uint v, uint size) { - Contract.Ensures(Contract.Result() != null); return (BitVecNum)MkNumeral(v, MkBitVecSort(size)); } @@ -3111,7 +2897,6 @@ namespace Microsoft.Z3 /// the size of the bit-vector public BitVecNum MkBV(long v, uint size) { - Contract.Ensures(Contract.Result() != null); return (BitVecNum)MkNumeral(v, MkBitVecSort(size)); } @@ -3123,7 +2908,6 @@ namespace Microsoft.Z3 /// the size of the bit-vector public BitVecNum MkBV(ulong v, uint size) { - Contract.Ensures(Contract.Result() != null); return (BitVecNum)MkNumeral(v, MkBitVecSort(size)); } @@ -3134,7 +2918,6 @@ namespace Microsoft.Z3 /// An array of bits representing the bit-vector. Least significant bit is at position 0. public BitVecNum MkBV(bool[] bits) { - Contract.Ensures(Contract.Result() != null); byte[] _bits = new byte[bits.Length]; for (int i = 0; i < bits.Length; ++i) _bits[i] = (byte)(bits[i] ? 1 : 0); return (BitVecNum)Expr.Create(this, Native.Z3_mk_bv_numeral(nCtx, (uint)bits.Length, _bits)); @@ -3172,16 +2955,15 @@ namespace Microsoft.Z3 /// optional symbol to track skolem constants. public Quantifier MkForall(Sort[] sorts, Symbol[] names, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null) { - Contract.Requires(sorts != null); - Contract.Requires(names != null); - Contract.Requires(body != null); - Contract.Requires(sorts.Length == names.Length); - Contract.Requires(Contract.ForAll(sorts, s => s != null)); - Contract.Requires(Contract.ForAll(names, n => n != null)); - Contract.Requires(patterns == null || Contract.ForAll(patterns, p => p != null)); - Contract.Requires(noPatterns == null || Contract.ForAll(noPatterns, np => np != null)); + Debug.Assert(sorts != null); + Debug.Assert(names != null); + Debug.Assert(body != null); + Debug.Assert(sorts.Length == names.Length); + Debug.Assert(sorts.All(s => s != null)); + Debug.Assert(names.All(n => n != null)); + Debug.Assert(patterns == null || patterns.All(p => p != null)); + Debug.Assert(noPatterns == null || noPatterns.All(np => np != null)); - Contract.Ensures(Contract.Result() != null); return new Quantifier(this, true, sorts, names, body, weight, patterns, noPatterns, quantifierID, skolemID); } @@ -3197,12 +2979,11 @@ namespace Microsoft.Z3 /// public Quantifier MkForall(Expr[] boundConstants, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null) { - Contract.Requires(body != null); - Contract.Requires(boundConstants == null || Contract.ForAll(boundConstants, b => b != null)); - Contract.Requires(patterns == null || Contract.ForAll(patterns, p => p != null)); - Contract.Requires(noPatterns == null || Contract.ForAll(noPatterns, np => np != null)); + Debug.Assert(body != null); + Debug.Assert(boundConstants == null || boundConstants.All(b => b != null)); + Debug.Assert(patterns == null || patterns.All(p => p != null)); + Debug.Assert(noPatterns == null || noPatterns.All(np => np != null)); - Contract.Ensures(Contract.Result() != null); return new Quantifier(this, true, boundConstants, body, weight, patterns, noPatterns, quantifierID, skolemID); } @@ -3216,15 +2997,14 @@ namespace Microsoft.Z3 /// public Quantifier MkExists(Sort[] sorts, Symbol[] names, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null) { - Contract.Requires(sorts != null); - Contract.Requires(names != null); - Contract.Requires(body != null); - Contract.Requires(sorts.Length == names.Length); - Contract.Requires(Contract.ForAll(sorts, s => s != null)); - Contract.Requires(Contract.ForAll(names, n => n != null)); - Contract.Requires(patterns == null || Contract.ForAll(patterns, p => p != null)); - Contract.Requires(noPatterns == null || Contract.ForAll(noPatterns, np => np != null)); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(sorts != null); + Debug.Assert(names != null); + Debug.Assert(body != null); + Debug.Assert(sorts.Length == names.Length); + Debug.Assert(sorts.All(s => s != null)); + Debug.Assert(names.All(n => n != null)); + Debug.Assert(patterns == null || patterns.All(p => p != null)); + Debug.Assert(noPatterns == null || noPatterns.All(np => np != null)); return new Quantifier(this, false, sorts, names, body, weight, patterns, noPatterns, quantifierID, skolemID); } @@ -3239,11 +3019,10 @@ namespace Microsoft.Z3 /// public Quantifier MkExists(Expr[] boundConstants, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null) { - Contract.Requires(body != null); - Contract.Requires(boundConstants == null || Contract.ForAll(boundConstants, n => n != null)); - Contract.Requires(patterns == null || Contract.ForAll(patterns, p => p != null)); - Contract.Requires(noPatterns == null || Contract.ForAll(noPatterns, np => np != null)); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(body != null); + Debug.Assert(boundConstants == null || boundConstants.All(n => n != null)); + Debug.Assert(patterns == null || patterns.All(p => p != null)); + Debug.Assert(noPatterns == null || noPatterns.All(np => np != null)); return new Quantifier(this, false, boundConstants, body, weight, patterns, noPatterns, quantifierID, skolemID); } @@ -3255,16 +3034,15 @@ namespace Microsoft.Z3 /// public Quantifier MkQuantifier(bool universal, Sort[] sorts, Symbol[] names, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null) { - Contract.Requires(body != null); - Contract.Requires(names != null); - Contract.Requires(sorts != null); - Contract.Requires(sorts.Length == names.Length); - Contract.Requires(Contract.ForAll(sorts, s => s != null)); - Contract.Requires(Contract.ForAll(names, n => n != null)); - Contract.Requires(patterns == null || Contract.ForAll(patterns, p => p != null)); - Contract.Requires(noPatterns == null || Contract.ForAll(noPatterns, np => np != null)); + Debug.Assert(body != null); + Debug.Assert(names != null); + Debug.Assert(sorts != null); + Debug.Assert(sorts.Length == names.Length); + Debug.Assert(sorts.All(s => s != null)); + Debug.Assert(names.All(n => n != null)); + Debug.Assert(patterns == null || patterns.All(p => p != null)); + Debug.Assert(noPatterns == null || noPatterns.All(np => np != null)); - Contract.Ensures(Contract.Result() != null); if (universal) return MkForall(sorts, names, body, weight, patterns, noPatterns, quantifierID, skolemID); @@ -3279,12 +3057,11 @@ namespace Microsoft.Z3 /// public Quantifier MkQuantifier(bool universal, Expr[] boundConstants, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null) { - Contract.Requires(body != null); - Contract.Requires(boundConstants == null || Contract.ForAll(boundConstants, n => n != null)); - Contract.Requires(patterns == null || Contract.ForAll(patterns, p => p != null)); - Contract.Requires(noPatterns == null || Contract.ForAll(noPatterns, np => np != null)); + Debug.Assert(body != null); + Debug.Assert(boundConstants == null || boundConstants.All(n => n != null)); + Debug.Assert(patterns == null || patterns.All(p => p != null)); + Debug.Assert(noPatterns == null || noPatterns.All(np => np != null)); - Contract.Ensures(Contract.Result() != null); if (universal) return MkForall(boundConstants, body, weight, patterns, noPatterns, quantifierID, skolemID); @@ -3312,13 +3089,12 @@ namespace Microsoft.Z3 /// the body of the quantifier. public Lambda MkLambda(Sort[] sorts, Symbol[] names, Expr body) { - Contract.Requires(sorts != null); - Contract.Requires(names != null); - Contract.Requires(body != null); - Contract.Requires(sorts.Length == names.Length); - Contract.Requires(Contract.ForAll(sorts, s => s != null)); - Contract.Requires(Contract.ForAll(names, n => n != null)); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(sorts != null); + Debug.Assert(names != null); + Debug.Assert(body != null); + Debug.Assert(sorts.Length == names.Length); + Debug.Assert(sorts.All(s => s != null)); + Debug.Assert(names.All(n => n != null)); return new Lambda(this, sorts, names, body); } @@ -3332,9 +3108,8 @@ namespace Microsoft.Z3 /// public Lambda MkLambda(Expr[] boundConstants, Expr body) { - Contract.Requires(body != null); - Contract.Requires(boundConstants != null && Contract.ForAll(boundConstants, b => b != null)); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(body != null); + Debug.Assert(boundConstants != null && boundConstants.All(b => b != null)); return new Lambda(this, boundConstants, body); } @@ -3374,7 +3149,6 @@ namespace Microsoft.Z3 /// A conjunction of assertions in the scope (up to push/pop) at the end of the string. public BoolExpr[] ParseSMTLIB2String(string str, Symbol[] sortNames = null, Sort[] sorts = null, Symbol[] declNames = null, FuncDecl[] decls = null) { - Contract.Ensures(Contract.Result() != null); uint csn = Symbol.ArrayLength(sortNames); uint cs = Sort.ArrayLength(sorts); @@ -3394,7 +3168,6 @@ namespace Microsoft.Z3 /// public BoolExpr[] ParseSMTLIB2File(string fileName, Symbol[] sortNames = null, Sort[] sorts = null, Symbol[] declNames = null, FuncDecl[] decls = null) { - Contract.Ensures(Contract.Result() != null); uint csn = Symbol.ArrayLength(sortNames); uint cs = Sort.ArrayLength(sorts); @@ -3422,7 +3195,6 @@ namespace Microsoft.Z3 /// Indicates whether proof generation should be enabled. public Goal MkGoal(bool models = true, bool unsatCores = false, bool proofs = false) { - Contract.Ensures(Contract.Result() != null); return new Goal(this, models, unsatCores, proofs); } @@ -3434,7 +3206,6 @@ namespace Microsoft.Z3 /// public Params MkParams() { - Contract.Ensures(Contract.Result() != null); return new Params(this); } @@ -3456,7 +3227,6 @@ namespace Microsoft.Z3 { get { - Contract.Ensures(Contract.Result() != null); uint n = NumTactics; string[] res = new string[n]; @@ -3471,7 +3241,6 @@ namespace Microsoft.Z3 /// public string TacticDescription(string name) { - Contract.Ensures(Contract.Result() != null); return Native.Z3_tactic_get_descr(nCtx, name); } @@ -3481,7 +3250,6 @@ namespace Microsoft.Z3 /// public Tactic MkTactic(string name) { - Contract.Ensures(Contract.Result() != null); return new Tactic(this, name); } @@ -3492,10 +3260,9 @@ namespace Microsoft.Z3 /// public Tactic AndThen(Tactic t1, Tactic t2, params Tactic[] ts) { - Contract.Requires(t1 != null); - Contract.Requires(t2 != null); - Contract.Requires(ts == null || Contract.ForAll(0, ts.Length, j => ts[j] != null)); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(t1 != null); + Debug.Assert(t2 != null); + // Debug.Assert(ts == null || Contract.ForAll(0, ts.Length, j => ts[j] != null)); CheckContextMatch(t1); @@ -3527,10 +3294,9 @@ namespace Microsoft.Z3 /// public Tactic Then(Tactic t1, Tactic t2, params Tactic[] ts) { - Contract.Requires(t1 != null); - Contract.Requires(t2 != null); - Contract.Requires(ts == null || Contract.ForAll(0, ts.Length, j => ts[j] != null)); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(t1 != null); + Debug.Assert(t2 != null); + // Debug.Assert(ts == null || Contract.ForAll(0, ts.Length, j => ts[j] != null)); return AndThen(t1, t2, ts); } @@ -3541,9 +3307,8 @@ namespace Microsoft.Z3 /// public Tactic OrElse(Tactic t1, Tactic t2) { - Contract.Requires(t1 != null); - Contract.Requires(t2 != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(t1 != null); + Debug.Assert(t2 != null); CheckContextMatch(t1); CheckContextMatch(t2); @@ -3558,8 +3323,7 @@ namespace Microsoft.Z3 /// public Tactic TryFor(Tactic t, uint ms) { - Contract.Requires(t != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(t != null); CheckContextMatch(t); return new Tactic(this, Native.Z3_tactic_try_for(nCtx, t.NativeObject, ms)); @@ -3574,9 +3338,8 @@ namespace Microsoft.Z3 /// public Tactic When(Probe p, Tactic t) { - Contract.Requires(p != null); - Contract.Requires(t != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(p != null); + Debug.Assert(t != null); CheckContextMatch(t); CheckContextMatch(p); @@ -3589,10 +3352,9 @@ namespace Microsoft.Z3 /// public Tactic Cond(Probe p, Tactic t1, Tactic t2) { - Contract.Requires(p != null); - Contract.Requires(t1 != null); - Contract.Requires(t2 != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(p != null); + Debug.Assert(t1 != null); + Debug.Assert(t2 != null); CheckContextMatch(p); CheckContextMatch(t1); @@ -3606,8 +3368,7 @@ namespace Microsoft.Z3 /// public Tactic Repeat(Tactic t, uint max = uint.MaxValue) { - Contract.Requires(t != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(t != null); CheckContextMatch(t); return new Tactic(this, Native.Z3_tactic_repeat(nCtx, t.NativeObject, max)); @@ -3618,7 +3379,6 @@ namespace Microsoft.Z3 /// public Tactic Skip() { - Contract.Ensures(Contract.Result() != null); return new Tactic(this, Native.Z3_tactic_skip(nCtx)); } @@ -3628,7 +3388,6 @@ namespace Microsoft.Z3 /// public Tactic Fail() { - Contract.Ensures(Contract.Result() != null); return new Tactic(this, Native.Z3_tactic_fail(nCtx)); } @@ -3638,8 +3397,7 @@ namespace Microsoft.Z3 /// public Tactic FailIf(Probe p) { - Contract.Requires(p != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(p != null); CheckContextMatch(p); return new Tactic(this, Native.Z3_tactic_fail_if(nCtx, p.NativeObject)); @@ -3651,7 +3409,6 @@ namespace Microsoft.Z3 /// public Tactic FailIfNotDecided() { - Contract.Ensures(Contract.Result() != null); return new Tactic(this, Native.Z3_tactic_fail_if_not_decided(nCtx)); } @@ -3661,9 +3418,8 @@ namespace Microsoft.Z3 /// public Tactic UsingParams(Tactic t, Params p) { - Contract.Requires(t != null); - Contract.Requires(p != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(t != null); + Debug.Assert(p != null); CheckContextMatch(t); CheckContextMatch(p); @@ -3676,9 +3432,8 @@ namespace Microsoft.Z3 /// Alias for UsingParams public Tactic With(Tactic t, Params p) { - Contract.Requires(t != null); - Contract.Requires(p != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(t != null); + Debug.Assert(p != null); return UsingParams(t, p); } @@ -3688,8 +3443,7 @@ namespace Microsoft.Z3 /// public Tactic ParOr(params Tactic[] t) { - Contract.Requires(t == null || Contract.ForAll(t, tactic => tactic != null)); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(t == null || t.All(tactic => tactic != null)); CheckContextMatch(t); return new Tactic(this, Native.Z3_tactic_par_or(nCtx, Tactic.ArrayLength(t), Tactic.ArrayToNative(t))); @@ -3701,9 +3455,8 @@ namespace Microsoft.Z3 /// public Tactic ParAndThen(Tactic t1, Tactic t2) { - Contract.Requires(t1 != null); - Contract.Requires(t2 != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(t1 != null); + Debug.Assert(t2 != null); CheckContextMatch(t1); CheckContextMatch(t2); @@ -3736,7 +3489,6 @@ namespace Microsoft.Z3 { get { - Contract.Ensures(Contract.Result() != null); uint n = NumProbes; string[] res = new string[n]; @@ -3751,7 +3503,6 @@ namespace Microsoft.Z3 /// public string ProbeDescription(string name) { - Contract.Ensures(Contract.Result() != null); return Native.Z3_probe_get_descr(nCtx, name); } @@ -3761,7 +3512,6 @@ namespace Microsoft.Z3 /// public Probe MkProbe(string name) { - Contract.Ensures(Contract.Result() != null); return new Probe(this, name); } @@ -3771,7 +3521,6 @@ namespace Microsoft.Z3 /// public Probe ConstProbe(double val) { - Contract.Ensures(Contract.Result() != null); return new Probe(this, Native.Z3_probe_const(nCtx, val)); } @@ -3782,9 +3531,8 @@ namespace Microsoft.Z3 /// public Probe Lt(Probe p1, Probe p2) { - Contract.Requires(p1 != null); - Contract.Requires(p2 != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(p1 != null); + Debug.Assert(p2 != null); CheckContextMatch(p1); CheckContextMatch(p2); @@ -3797,9 +3545,8 @@ namespace Microsoft.Z3 /// public Probe Gt(Probe p1, Probe p2) { - Contract.Requires(p1 != null); - Contract.Requires(p2 != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(p1 != null); + Debug.Assert(p2 != null); CheckContextMatch(p1); CheckContextMatch(p2); @@ -3812,9 +3559,8 @@ namespace Microsoft.Z3 /// public Probe Le(Probe p1, Probe p2) { - Contract.Requires(p1 != null); - Contract.Requires(p2 != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(p1 != null); + Debug.Assert(p2 != null); CheckContextMatch(p1); CheckContextMatch(p2); @@ -3827,9 +3573,8 @@ namespace Microsoft.Z3 /// public Probe Ge(Probe p1, Probe p2) { - Contract.Requires(p1 != null); - Contract.Requires(p2 != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(p1 != null); + Debug.Assert(p2 != null); CheckContextMatch(p1); CheckContextMatch(p2); @@ -3842,9 +3587,8 @@ namespace Microsoft.Z3 /// public Probe Eq(Probe p1, Probe p2) { - Contract.Requires(p1 != null); - Contract.Requires(p2 != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(p1 != null); + Debug.Assert(p2 != null); CheckContextMatch(p1); CheckContextMatch(p2); @@ -3857,9 +3601,8 @@ namespace Microsoft.Z3 /// public Probe And(Probe p1, Probe p2) { - Contract.Requires(p1 != null); - Contract.Requires(p2 != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(p1 != null); + Debug.Assert(p2 != null); CheckContextMatch(p1); CheckContextMatch(p2); @@ -3872,9 +3615,8 @@ namespace Microsoft.Z3 /// public Probe Or(Probe p1, Probe p2) { - Contract.Requires(p1 != null); - Contract.Requires(p2 != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(p1 != null); + Debug.Assert(p2 != null); CheckContextMatch(p1); CheckContextMatch(p2); @@ -3887,8 +3629,7 @@ namespace Microsoft.Z3 /// public Probe Not(Probe p) { - Contract.Requires(p != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(p != null); CheckContextMatch(p); return new Probe(this, Native.Z3_probe_not(nCtx, p.NativeObject)); @@ -3906,7 +3647,6 @@ namespace Microsoft.Z3 /// public Solver MkSolver(Symbol logic = null) { - Contract.Ensures(Contract.Result() != null); if (logic == null) return new Solver(this, Native.Z3_mk_solver(nCtx)); @@ -3920,7 +3660,6 @@ namespace Microsoft.Z3 /// public Solver MkSolver(string logic) { - Contract.Ensures(Contract.Result() != null); return MkSolver(MkSymbol(logic)); } @@ -3930,7 +3669,6 @@ namespace Microsoft.Z3 /// public Solver MkSimpleSolver() { - Contract.Ensures(Contract.Result() != null); return new Solver(this, Native.Z3_mk_simple_solver(nCtx)); } @@ -3944,8 +3682,7 @@ namespace Microsoft.Z3 /// public Solver MkSolver(Tactic t) { - Contract.Requires(t != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(t != null); return new Solver(this, Native.Z3_mk_solver_from_tactic(nCtx, t.NativeObject)); } @@ -3957,7 +3694,6 @@ namespace Microsoft.Z3 /// public Fixedpoint MkFixedpoint() { - Contract.Ensures(Contract.Result() != null); return new Fixedpoint(this); } @@ -3969,7 +3705,6 @@ namespace Microsoft.Z3 /// public Optimize MkOptimize() { - Contract.Ensures(Contract.Result() != null); return new Optimize(this); } @@ -3984,7 +3719,6 @@ namespace Microsoft.Z3 /// public FPRMSort MkFPRoundingModeSort() { - Contract.Ensures(Contract.Result() != null); return new FPRMSort(this); } #endregion @@ -3995,7 +3729,6 @@ namespace Microsoft.Z3 /// public FPRMExpr MkFPRoundNearestTiesToEven() { - Contract.Ensures(Contract.Result() != null); return new FPRMExpr(this, Native.Z3_mk_fpa_round_nearest_ties_to_even(nCtx)); } @@ -4004,7 +3737,6 @@ namespace Microsoft.Z3 /// public FPRMNum MkFPRNE() { - Contract.Ensures(Contract.Result() != null); return new FPRMNum(this, Native.Z3_mk_fpa_rne(nCtx)); } @@ -4013,7 +3745,6 @@ namespace Microsoft.Z3 /// public FPRMNum MkFPRoundNearestTiesToAway() { - Contract.Ensures(Contract.Result() != null); return new FPRMNum(this, Native.Z3_mk_fpa_round_nearest_ties_to_away(nCtx)); } @@ -4022,7 +3753,6 @@ namespace Microsoft.Z3 /// public FPRMNum MkFPRNA() { - Contract.Ensures(Contract.Result() != null); return new FPRMNum(this, Native.Z3_mk_fpa_rna(nCtx)); } @@ -4031,7 +3761,6 @@ namespace Microsoft.Z3 /// public FPRMNum MkFPRoundTowardPositive() { - Contract.Ensures(Contract.Result() != null); return new FPRMNum(this, Native.Z3_mk_fpa_round_toward_positive(nCtx)); } @@ -4040,7 +3769,6 @@ namespace Microsoft.Z3 /// public FPRMNum MkFPRTP() { - Contract.Ensures(Contract.Result() != null); return new FPRMNum(this, Native.Z3_mk_fpa_rtp(nCtx)); } @@ -4049,7 +3777,6 @@ namespace Microsoft.Z3 /// public FPRMNum MkFPRoundTowardNegative() { - Contract.Ensures(Contract.Result() != null); return new FPRMNum(this, Native.Z3_mk_fpa_round_toward_negative(nCtx)); } @@ -4058,7 +3785,6 @@ namespace Microsoft.Z3 /// public FPRMNum MkFPRTN() { - Contract.Ensures(Contract.Result() != null); return new FPRMNum(this, Native.Z3_mk_fpa_rtn(nCtx)); } @@ -4067,7 +3793,6 @@ namespace Microsoft.Z3 /// public FPRMNum MkFPRoundTowardZero() { - Contract.Ensures(Contract.Result() != null); return new FPRMNum(this, Native.Z3_mk_fpa_round_toward_zero(nCtx)); } @@ -4076,7 +3801,6 @@ namespace Microsoft.Z3 /// public FPRMNum MkFPRTZ() { - Contract.Ensures(Contract.Result() != null); return new FPRMNum(this, Native.Z3_mk_fpa_rtz(nCtx)); } #endregion @@ -4090,7 +3814,6 @@ namespace Microsoft.Z3 /// significand bits in the FloatingPoint sort. public FPSort MkFPSort(uint ebits, uint sbits) { - Contract.Ensures(Contract.Result() != null); return new FPSort(this, ebits, sbits); } @@ -4099,7 +3822,6 @@ namespace Microsoft.Z3 /// public FPSort MkFPSortHalf() { - Contract.Ensures(Contract.Result() != null); return new FPSort(this, Native.Z3_mk_fpa_sort_half(nCtx)); } @@ -4108,7 +3830,6 @@ namespace Microsoft.Z3 /// public FPSort MkFPSort16() { - Contract.Ensures(Contract.Result() != null); return new FPSort(this, Native.Z3_mk_fpa_sort_16(nCtx)); } @@ -4117,7 +3838,6 @@ namespace Microsoft.Z3 /// public FPSort MkFPSortSingle() { - Contract.Ensures(Contract.Result() != null); return new FPSort(this, Native.Z3_mk_fpa_sort_single(nCtx)); } @@ -4126,7 +3846,6 @@ namespace Microsoft.Z3 /// public FPSort MkFPSort32() { - Contract.Ensures(Contract.Result() != null); return new FPSort(this, Native.Z3_mk_fpa_sort_32(nCtx)); } @@ -4135,7 +3854,6 @@ namespace Microsoft.Z3 /// public FPSort MkFPSortDouble() { - Contract.Ensures(Contract.Result() != null); return new FPSort(this, Native.Z3_mk_fpa_sort_double(nCtx)); } @@ -4144,7 +3862,6 @@ namespace Microsoft.Z3 /// public FPSort MkFPSort64() { - Contract.Ensures(Contract.Result() != null); return new FPSort(this, Native.Z3_mk_fpa_sort_64(nCtx)); } @@ -4153,7 +3870,6 @@ namespace Microsoft.Z3 /// public FPSort MkFPSortQuadruple() { - Contract.Ensures(Contract.Result() != null); return new FPSort(this, Native.Z3_mk_fpa_sort_quadruple(nCtx)); } @@ -4162,7 +3878,6 @@ namespace Microsoft.Z3 /// public FPSort MkFPSort128() { - Contract.Ensures(Contract.Result() != null); return new FPSort(this, Native.Z3_mk_fpa_sort_128(nCtx)); } #endregion @@ -4174,7 +3889,6 @@ namespace Microsoft.Z3 /// FloatingPoint sort. public FPNum MkFPNaN(FPSort s) { - Contract.Ensures(Contract.Result() != null); return new FPNum(this, Native.Z3_mk_fpa_nan(nCtx, s.NativeObject)); } @@ -4185,7 +3899,6 @@ namespace Microsoft.Z3 /// indicates whether the result should be negative. public FPNum MkFPInf(FPSort s, bool negative) { - Contract.Ensures(Contract.Result() != null); return new FPNum(this, Native.Z3_mk_fpa_inf(nCtx, s.NativeObject, (byte)(negative ? 1 : 0))); } @@ -4196,7 +3909,6 @@ namespace Microsoft.Z3 /// indicates whether the result should be negative. public FPNum MkFPZero(FPSort s, bool negative) { - Contract.Ensures(Contract.Result() != null); return new FPNum(this, Native.Z3_mk_fpa_zero(nCtx, s.NativeObject, (byte)(negative ? 1 : 0))); } @@ -4207,7 +3919,6 @@ namespace Microsoft.Z3 /// FloatingPoint sort. public FPNum MkFPNumeral(float v, FPSort s) { - Contract.Ensures(Contract.Result() != null); return new FPNum(this, Native.Z3_mk_fpa_numeral_float(nCtx, v, s.NativeObject)); } @@ -4218,7 +3929,6 @@ namespace Microsoft.Z3 /// FloatingPoint sort. public FPNum MkFPNumeral(double v, FPSort s) { - Contract.Ensures(Contract.Result() != null); return new FPNum(this, Native.Z3_mk_fpa_numeral_double(nCtx, v, s.NativeObject)); } @@ -4229,7 +3939,6 @@ namespace Microsoft.Z3 /// FloatingPoint sort. public FPNum MkFPNumeral(int v, FPSort s) { - Contract.Ensures(Contract.Result() != null); return new FPNum(this, Native.Z3_mk_fpa_numeral_int(nCtx, v, s.NativeObject)); } @@ -4242,7 +3951,6 @@ namespace Microsoft.Z3 /// FloatingPoint sort. public FPNum MkFPNumeral(bool sgn, uint sig, int exp, FPSort s) { - Contract.Ensures(Contract.Result() != null); return new FPNum(this, Native.Z3_mk_fpa_numeral_int_uint(nCtx, (byte)(sgn ? 1 : 0), exp, sig, s.NativeObject)); } @@ -4255,7 +3963,6 @@ namespace Microsoft.Z3 /// FloatingPoint sort. public FPNum MkFPNumeral(bool sgn, Int64 exp, UInt64 sig, FPSort s) { - Contract.Ensures(Contract.Result() != null); return new FPNum(this, Native.Z3_mk_fpa_numeral_int64_uint64(nCtx, (byte)(sgn ? 1 : 0), exp, sig, s.NativeObject)); } @@ -4266,7 +3973,6 @@ namespace Microsoft.Z3 /// FloatingPoint sort. public FPNum MkFP(float v, FPSort s) { - Contract.Ensures(Contract.Result() != null); return MkFPNumeral(v, s); } @@ -4277,7 +3983,6 @@ namespace Microsoft.Z3 /// FloatingPoint sort. public FPNum MkFP(double v, FPSort s) { - Contract.Ensures(Contract.Result() != null); return MkFPNumeral(v, s); } @@ -4288,7 +3993,6 @@ namespace Microsoft.Z3 /// FloatingPoint sort. public FPNum MkFP(int v, FPSort s) { - Contract.Ensures(Contract.Result() != null); return MkFPNumeral(v, s); } @@ -4301,7 +4005,6 @@ namespace Microsoft.Z3 /// FloatingPoint sort. public FPNum MkFP(bool sgn, int exp, uint sig, FPSort s) { - Contract.Ensures(Contract.Result() != null); return MkFPNumeral(sgn, exp, sig, s); } @@ -4314,7 +4017,6 @@ namespace Microsoft.Z3 /// FloatingPoint sort. public FPNum MkFP(bool sgn, Int64 exp, UInt64 sig, FPSort s) { - Contract.Ensures(Contract.Result() != null); return MkFPNumeral(sgn, exp, sig, s); } @@ -4327,7 +4029,6 @@ namespace Microsoft.Z3 /// floating-point term public FPExpr MkFPAbs(FPExpr t) { - Contract.Ensures(Contract.Result() != null); return new FPExpr(this, Native.Z3_mk_fpa_abs(this.nCtx, t.NativeObject)); } @@ -4337,7 +4038,6 @@ namespace Microsoft.Z3 /// floating-point term public FPExpr MkFPNeg(FPExpr t) { - Contract.Ensures(Contract.Result() != null); return new FPExpr(this, Native.Z3_mk_fpa_neg(this.nCtx, t.NativeObject)); } @@ -4349,7 +4049,6 @@ namespace Microsoft.Z3 /// floating-point term public 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)); } @@ -4361,7 +4060,6 @@ namespace Microsoft.Z3 /// floating-point term public 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)); } @@ -4373,7 +4071,6 @@ namespace Microsoft.Z3 /// floating-point term public 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)); } @@ -4385,7 +4082,6 @@ namespace Microsoft.Z3 /// floating-point term public 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)); } @@ -4401,7 +4097,6 @@ namespace Microsoft.Z3 /// floating-point term public 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)); } @@ -4412,7 +4107,6 @@ namespace Microsoft.Z3 /// floating-point term public 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)); } @@ -4423,7 +4117,6 @@ namespace Microsoft.Z3 /// floating-point term public 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)); } @@ -4435,7 +4128,6 @@ namespace Microsoft.Z3 /// floating-point term public FPExpr MkFPRoundToIntegral(FPRMExpr rm, FPExpr t) { - Contract.Ensures(Contract.Result() != null); return new FPExpr(this, Native.Z3_mk_fpa_round_to_integral(this.nCtx, rm.NativeObject, t.NativeObject)); } @@ -4446,7 +4138,6 @@ namespace Microsoft.Z3 /// floating-point term public 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)); } @@ -4457,7 +4148,6 @@ namespace Microsoft.Z3 /// floating-point term public 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)); } @@ -4468,7 +4158,6 @@ namespace Microsoft.Z3 /// floating-point term public BoolExpr MkFPLEq(FPExpr t1, FPExpr t2) { - Contract.Ensures(Contract.Result() != null); return new BoolExpr(this, Native.Z3_mk_fpa_leq(this.nCtx, t1.NativeObject, t2.NativeObject)); } @@ -4479,7 +4168,6 @@ namespace Microsoft.Z3 /// floating-point term public 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)); } @@ -4490,7 +4178,6 @@ namespace Microsoft.Z3 /// floating-point term public BoolExpr MkFPGEq(FPExpr t1, FPExpr t2) { - Contract.Ensures(Contract.Result() != null); return new BoolExpr(this, Native.Z3_mk_fpa_geq(this.nCtx, t1.NativeObject, t2.NativeObject)); } @@ -4501,7 +4188,6 @@ namespace Microsoft.Z3 /// floating-point term public 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)); } @@ -4515,7 +4201,6 @@ namespace Microsoft.Z3 /// floating-point term public 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)); } @@ -4525,7 +4210,6 @@ namespace Microsoft.Z3 /// floating-point term public BoolExpr MkFPIsNormal(FPExpr t) { - Contract.Ensures(Contract.Result() != null); return new BoolExpr(this, Native.Z3_mk_fpa_is_normal(this.nCtx, t.NativeObject)); } @@ -4535,7 +4219,6 @@ namespace Microsoft.Z3 /// floating-point term public BoolExpr MkFPIsSubnormal(FPExpr t) { - Contract.Ensures(Contract.Result() != null); return new BoolExpr(this, Native.Z3_mk_fpa_is_subnormal(this.nCtx, t.NativeObject)); } @@ -4545,7 +4228,6 @@ namespace Microsoft.Z3 /// floating-point term public BoolExpr MkFPIsZero(FPExpr t) { - Contract.Ensures(Contract.Result() != null); return new BoolExpr(this, Native.Z3_mk_fpa_is_zero(this.nCtx, t.NativeObject)); } @@ -4555,7 +4237,6 @@ namespace Microsoft.Z3 /// floating-point term public BoolExpr MkFPIsInfinite(FPExpr t) { - Contract.Ensures(Contract.Result() != null); return new BoolExpr(this, Native.Z3_mk_fpa_is_infinite(this.nCtx, t.NativeObject)); } @@ -4565,7 +4246,6 @@ namespace Microsoft.Z3 /// floating-point term public BoolExpr MkFPIsNaN(FPExpr t) { - Contract.Ensures(Contract.Result() != null); return new BoolExpr(this, Native.Z3_mk_fpa_is_nan(this.nCtx, t.NativeObject)); } @@ -4575,7 +4255,6 @@ namespace Microsoft.Z3 /// floating-point term public BoolExpr MkFPIsNegative(FPExpr t) { - Contract.Ensures(Contract.Result() != null); return new BoolExpr(this, Native.Z3_mk_fpa_is_negative(this.nCtx, t.NativeObject)); } @@ -4585,7 +4264,6 @@ namespace Microsoft.Z3 /// floating-point term public BoolExpr MkFPIsPositive(FPExpr t) { - Contract.Ensures(Contract.Result() != null); return new BoolExpr(this, Native.Z3_mk_fpa_is_positive(this.nCtx, t.NativeObject)); } #endregion @@ -4606,7 +4284,6 @@ namespace Microsoft.Z3 /// bit-vector term representing the exponent. public FPExpr MkFP(BitVecExpr sgn, BitVecExpr sig, BitVecExpr exp) { - Contract.Ensures(Contract.Result() != null); return new FPExpr(this, Native.Z3_mk_fpa_fp(this.nCtx, sgn.NativeObject, sig.NativeObject, exp.NativeObject)); } @@ -4623,7 +4300,6 @@ namespace Microsoft.Z3 /// FloatingPoint sort (ebits+sbits == m) public FPExpr MkFPToFP(BitVecExpr bv, FPSort s) { - Contract.Ensures(Contract.Result() != null); return new FPExpr(this, Native.Z3_mk_fpa_to_fp_bv(this.nCtx, bv.NativeObject, s.NativeObject)); } @@ -4640,7 +4316,6 @@ namespace Microsoft.Z3 /// FloatingPoint sort. public FPExpr MkFPToFP(FPRMExpr rm, FPExpr t, FPSort s) { - Contract.Ensures(Contract.Result() != null); return new FPExpr(this, Native.Z3_mk_fpa_to_fp_float(this.nCtx, rm.NativeObject, t.NativeObject, s.NativeObject)); } @@ -4657,7 +4332,6 @@ namespace Microsoft.Z3 /// FloatingPoint sort. public FPExpr MkFPToFP(FPRMExpr rm, RealExpr t, FPSort s) { - Contract.Ensures(Contract.Result() != null); return new FPExpr(this, Native.Z3_mk_fpa_to_fp_real(this.nCtx, rm.NativeObject, t.NativeObject, s.NativeObject)); } @@ -4676,7 +4350,6 @@ namespace Microsoft.Z3 /// flag indicating whether t is interpreted as signed or unsigned bit-vector. public FPExpr MkFPToFP(FPRMExpr rm, BitVecExpr t, FPSort s, bool signed) { - Contract.Ensures(Contract.Result() != null); if (signed) return new FPExpr(this, Native.Z3_mk_fpa_to_fp_signed(this.nCtx, rm.NativeObject, t.NativeObject, s.NativeObject)); else @@ -4695,7 +4368,6 @@ namespace Microsoft.Z3 /// floating-point term public FPExpr MkFPToFP(FPSort s, FPRMExpr rm, FPExpr t) { - Contract.Ensures(Contract.Result() != null); return new FPExpr(this, Native.Z3_mk_fpa_to_fp_float(this.nCtx, s.NativeObject, rm.NativeObject, t.NativeObject)); } #endregion @@ -4715,7 +4387,6 @@ namespace Microsoft.Z3 /// Indicates whether the result is a signed or unsigned bit-vector. public BitVecExpr MkFPToBV(FPRMExpr rm, FPExpr t, uint sz, bool signed) { - Contract.Ensures(Contract.Result() != null); if (signed) return new BitVecExpr(this, Native.Z3_mk_fpa_to_sbv(this.nCtx, rm.NativeObject, t.NativeObject, sz)); else @@ -4733,7 +4404,6 @@ namespace Microsoft.Z3 /// FloatingPoint term public RealExpr MkFPToReal(FPExpr t) { - Contract.Ensures(Contract.Result() != null); return new RealExpr(this, Native.Z3_mk_fpa_to_real(this.nCtx, t.NativeObject)); } #endregion @@ -4751,7 +4421,6 @@ namespace Microsoft.Z3 /// FloatingPoint term. public BitVecExpr MkFPToIEEEBV(FPExpr t) { - Contract.Ensures(Contract.Result() != null); return new BitVecExpr(this, Native.Z3_mk_fpa_to_ieee_bv(this.nCtx, t.NativeObject)); } @@ -4769,7 +4438,6 @@ namespace Microsoft.Z3 /// FloatingPoint sort. public BitVecExpr MkFPToFP(FPRMExpr rm, IntExpr exp, RealExpr sig, FPSort s) { - Contract.Ensures(Contract.Result() != null); return new BitVecExpr(this, Native.Z3_mk_fpa_to_fp_int_real(this.nCtx, rm.NativeObject, exp.NativeObject, sig.NativeObject, s.NativeObject)); } #endregion @@ -4788,7 +4456,6 @@ namespace Microsoft.Z3 /// The native pointer to wrap. public AST WrapAST(IntPtr nativeObject) { - Contract.Ensures(Contract.Result() != null); return AST.Create(this, nativeObject); } @@ -4813,7 +4480,6 @@ namespace Microsoft.Z3 /// public string SimplifyHelp() { - Contract.Ensures(Contract.Result() != null); return Native.Z3_simplify_get_help(nCtx); } @@ -4879,84 +4545,78 @@ namespace Microsoft.Z3 GC.SuppressFinalize(this); } - [Pure] internal void CheckContextMatch(Z3Object other) { - Contract.Requires(other != null); + Debug.Assert(other != null); if (!ReferenceEquals(this, other.Context)) throw new Z3Exception("Context mismatch"); } - [Pure] internal void CheckContextMatch(Z3Object other1, Z3Object other2) { - Contract.Requires(other1 != null); - Contract.Requires(other2 != null); + Debug.Assert(other1 != null); + Debug.Assert(other2 != null); CheckContextMatch(other1); CheckContextMatch(other2); } - [Pure] internal void CheckContextMatch(Z3Object other1, Z3Object other2, Z3Object other3) { - Contract.Requires(other1 != null); - Contract.Requires(other2 != null); - Contract.Requires(other3 != null); + Debug.Assert(other1 != null); + Debug.Assert(other2 != null); + Debug.Assert(other3 != null); CheckContextMatch(other1); CheckContextMatch(other2); CheckContextMatch(other3); } - [Pure] internal void CheckContextMatch(Z3Object[] arr) { - Contract.Requires(arr == null || Contract.ForAll(arr, a => a != null)); + Debug.Assert(arr == null || arr.All(a => a != null)); if (arr != null) { foreach (Z3Object a in arr) { - Contract.Assert(a != null); // It was an assume, now we added the precondition, and we made it into an assert + Debug.Assert(a != null); // It was an assume, now we added the precondition, and we made it into an assert CheckContextMatch(a); } } } - [Pure] internal void CheckContextMatch(IEnumerable arr) where T : Z3Object { - Contract.Requires(arr == null || Contract.ForAll(arr, a => a != null)); + Debug.Assert(arr == null || arr.All(a => a != null)); if (arr != null) { foreach (Z3Object a in arr) { - Contract.Assert(a != null); // It was an assume, now we added the precondition, and we made it into an assert + Debug.Assert(a != null); // It was an assume, now we added the precondition, and we made it into an assert CheckContextMatch(a); } } } - [ContractInvariantMethod] private void ObjectInvariant() { - Contract.Invariant(m_AST_DRQ != null); - Contract.Invariant(m_ASTMap_DRQ != null); - Contract.Invariant(m_ASTVector_DRQ != null); - Contract.Invariant(m_ApplyResult_DRQ != null); - Contract.Invariant(m_FuncEntry_DRQ != null); - Contract.Invariant(m_FuncInterp_DRQ != null); - Contract.Invariant(m_Goal_DRQ != null); - Contract.Invariant(m_Model_DRQ != null); - Contract.Invariant(m_Params_DRQ != null); - Contract.Invariant(m_ParamDescrs_DRQ != null); - Contract.Invariant(m_Probe_DRQ != null); - Contract.Invariant(m_Solver_DRQ != null); - Contract.Invariant(m_Statistics_DRQ != null); - Contract.Invariant(m_Tactic_DRQ != null); - Contract.Invariant(m_Fixedpoint_DRQ != null); - Contract.Invariant(m_Optimize_DRQ != null); + Debug.Assert(m_AST_DRQ != null); + Debug.Assert(m_ASTMap_DRQ != null); + Debug.Assert(m_ASTVector_DRQ != null); + Debug.Assert(m_ApplyResult_DRQ != null); + Debug.Assert(m_FuncEntry_DRQ != null); + Debug.Assert(m_FuncInterp_DRQ != null); + Debug.Assert(m_Goal_DRQ != null); + Debug.Assert(m_Model_DRQ != null); + Debug.Assert(m_Params_DRQ != null); + Debug.Assert(m_ParamDescrs_DRQ != null); + Debug.Assert(m_Probe_DRQ != null); + Debug.Assert(m_Solver_DRQ != null); + Debug.Assert(m_Statistics_DRQ != null); + Debug.Assert(m_Tactic_DRQ != null); + Debug.Assert(m_Fixedpoint_DRQ != null); + Debug.Assert(m_Optimize_DRQ != null); } readonly private AST.DecRefQueue m_AST_DRQ = new AST.DecRefQueue(); @@ -4979,83 +4639,82 @@ namespace Microsoft.Z3 /// /// AST DRQ /// - public IDecRefQueue AST_DRQ { get { Contract.Ensures(Contract.Result() != null); return m_AST_DRQ; } } + public IDecRefQueue AST_DRQ { get { return m_AST_DRQ; } } /// /// ASTMap DRQ /// - public IDecRefQueue ASTMap_DRQ { get { Contract.Ensures(Contract.Result() != null); return m_ASTMap_DRQ; } } + public IDecRefQueue ASTMap_DRQ { get { return m_ASTMap_DRQ; } } /// /// ASTVector DRQ /// - public IDecRefQueue ASTVector_DRQ { get { Contract.Ensures(Contract.Result() != null); return m_ASTVector_DRQ; } } + public IDecRefQueue ASTVector_DRQ { get { return m_ASTVector_DRQ; } } /// /// ApplyResult DRQ /// - public IDecRefQueue ApplyResult_DRQ { get { Contract.Ensures(Contract.Result() != null); return m_ApplyResult_DRQ; } } + public IDecRefQueue ApplyResult_DRQ { get { return m_ApplyResult_DRQ; } } /// /// FuncEntry DRQ /// - public IDecRefQueue FuncEntry_DRQ { get { Contract.Ensures(Contract.Result() != null); return m_FuncEntry_DRQ; } } + public IDecRefQueue FuncEntry_DRQ { get { return m_FuncEntry_DRQ; } } /// /// FuncInterp DRQ /// - public IDecRefQueue FuncInterp_DRQ { get { Contract.Ensures(Contract.Result() != null); return m_FuncInterp_DRQ; } } + public IDecRefQueue FuncInterp_DRQ { get { return m_FuncInterp_DRQ; } } /// /// Goal DRQ /// - public IDecRefQueue Goal_DRQ { get { Contract.Ensures(Contract.Result() != null); return m_Goal_DRQ; } } + public IDecRefQueue Goal_DRQ { get { return m_Goal_DRQ; } } /// /// Model DRQ /// - public IDecRefQueue Model_DRQ { get { Contract.Ensures(Contract.Result() != null); return m_Model_DRQ; } } + public IDecRefQueue Model_DRQ { get { return m_Model_DRQ; } } /// /// Params DRQ /// - public IDecRefQueue Params_DRQ { get { Contract.Ensures(Contract.Result() != null); return m_Params_DRQ; } } + public IDecRefQueue Params_DRQ { get { return m_Params_DRQ; } } /// /// ParamDescrs DRQ /// - public IDecRefQueue ParamDescrs_DRQ { get { Contract.Ensures(Contract.Result() != null); return m_ParamDescrs_DRQ; } } + public IDecRefQueue ParamDescrs_DRQ { get { return m_ParamDescrs_DRQ; } } /// /// Probe DRQ /// - public IDecRefQueue Probe_DRQ { get { Contract.Ensures(Contract.Result() != null); return m_Probe_DRQ; } } + public IDecRefQueue Probe_DRQ { get { return m_Probe_DRQ; } } /// /// Solver DRQ /// - public IDecRefQueue Solver_DRQ { get { Contract.Ensures(Contract.Result() != null); return m_Solver_DRQ; } } + public IDecRefQueue Solver_DRQ { get { return m_Solver_DRQ; } } /// /// Statistics DRQ /// - public IDecRefQueue Statistics_DRQ { get { Contract.Ensures(Contract.Result() != null); return m_Statistics_DRQ; } } + public IDecRefQueue Statistics_DRQ { get { return m_Statistics_DRQ; } } /// /// Tactic DRQ /// - public IDecRefQueue Tactic_DRQ { get { Contract.Ensures(Contract.Result() != null); return m_Tactic_DRQ; } } + public IDecRefQueue Tactic_DRQ { get { return m_Tactic_DRQ; } } /// /// FixedPoint DRQ /// - public IDecRefQueue Fixedpoint_DRQ { get { Contract.Ensures(Contract.Result() != null); return m_Fixedpoint_DRQ; } } + public IDecRefQueue Fixedpoint_DRQ { get { return m_Fixedpoint_DRQ; } } /// /// Optimize DRQ /// - public IDecRefQueue Optimize_DRQ { get { Contract.Ensures(Contract.Result() != null); return m_Fixedpoint_DRQ; } } - + public IDecRefQueue Optimize_DRQ { get { return m_Fixedpoint_DRQ; } } internal long refCount = 0; diff --git a/src/api/dotnet/DatatypeExpr.cs b/src/api/dotnet/DatatypeExpr.cs index ba3a9d478..03595c349 100644 --- a/src/api/dotnet/DatatypeExpr.cs +++ b/src/api/dotnet/DatatypeExpr.cs @@ -16,12 +16,12 @@ Author: Notes: --*/ +using System.Diagnostics; using System; using System.Collections.Generic; using System.Linq; using System.Text; -using System.Diagnostics.Contracts; namespace Microsoft.Z3 { @@ -35,7 +35,7 @@ namespace Microsoft.Z3 internal DatatypeExpr(Context ctx, IntPtr obj) : base(ctx, obj) { - Contract.Requires(ctx != null); + Debug.Assert(ctx != null); } #endregion } diff --git a/src/api/dotnet/DatatypeSort.cs b/src/api/dotnet/DatatypeSort.cs index e47545d68..943d3753f 100644 --- a/src/api/dotnet/DatatypeSort.cs +++ b/src/api/dotnet/DatatypeSort.cs @@ -17,15 +17,14 @@ Notes: --*/ +using System.Diagnostics; using System; -using System.Diagnostics.Contracts; namespace Microsoft.Z3 { /// /// Datatype sorts. /// - [ContractVerification(true)] public class DatatypeSort : Sort { /// @@ -43,7 +42,6 @@ namespace Microsoft.Z3 { get { - Contract.Ensures(Contract.Result() != null); uint n = NumConstructors; FuncDecl[] res = new FuncDecl[n]; @@ -60,7 +58,6 @@ namespace Microsoft.Z3 { get { - Contract.Ensures(Contract.Result() != null); uint n = NumConstructors; FuncDecl[] res = new FuncDecl[n]; @@ -77,7 +74,6 @@ namespace Microsoft.Z3 { get { - Contract.Ensures(Contract.Result() != null); uint n = NumConstructors; FuncDecl[][] res = new FuncDecl[n][]; @@ -95,14 +91,14 @@ namespace Microsoft.Z3 } #region Internal - internal DatatypeSort(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); } + internal DatatypeSort(Context ctx, IntPtr obj) : base(ctx, obj) { Debug.Assert(ctx != null); } internal DatatypeSort(Context ctx, Symbol name, Constructor[] constructors) : base(ctx, Native.Z3_mk_datatype(ctx.nCtx, name.NativeObject, (uint)constructors.Length, ArrayToNative(constructors))) { - Contract.Requires(ctx != null); - Contract.Requires(name != null); - Contract.Requires(constructors != null); + Debug.Assert(ctx != null); + Debug.Assert(name != null); + Debug.Assert(constructors != null); } #endregion }; diff --git a/src/api/dotnet/Deprecated.cs b/src/api/dotnet/Deprecated.cs index feb5b1555..64255cea2 100644 --- a/src/api/dotnet/Deprecated.cs +++ b/src/api/dotnet/Deprecated.cs @@ -17,17 +17,16 @@ Author: Notes: --*/ +using System.Diagnostics; using System; using System.Collections.Generic; using System.Runtime.InteropServices; -using System.Diagnostics.Contracts; namespace Microsoft.Z3 { /// /// The main interaction with Z3 happens via the Context. /// - [ContractVerification(true)] public class Deprecated { diff --git a/src/api/dotnet/EnumSort.cs b/src/api/dotnet/EnumSort.cs index 62be48a2c..08c85361e 100644 --- a/src/api/dotnet/EnumSort.cs +++ b/src/api/dotnet/EnumSort.cs @@ -17,15 +17,14 @@ Notes: --*/ +using System.Diagnostics; using System; -using System.Diagnostics.Contracts; namespace Microsoft.Z3 { /// /// Enumeration sorts. /// - [ContractVerification(true)] public class EnumSort : Sort { /// @@ -35,7 +34,6 @@ namespace Microsoft.Z3 { get { - Contract.Ensures(Contract.Result() != null); uint n = Native.Z3_get_datatype_sort_num_constructors(Context.nCtx, NativeObject); FuncDecl[] t = new FuncDecl[n]; for (uint i = 0; i < n; i++) @@ -61,7 +59,6 @@ namespace Microsoft.Z3 { get { - Contract.Ensures(Contract.Result() != null); FuncDecl[] cds = ConstDecls; Expr[] t = new Expr[cds.Length]; for (uint i = 0; i < t.Length; i++) @@ -87,7 +84,6 @@ namespace Microsoft.Z3 { get { - Contract.Ensures(Contract.Result() != null); uint n = Native.Z3_get_datatype_sort_num_constructors(Context.nCtx, NativeObject); FuncDecl[] t = new FuncDecl[n]; for (uint i = 0; i < n; i++) @@ -110,9 +106,9 @@ namespace Microsoft.Z3 internal EnumSort(Context ctx, Symbol name, Symbol[] enumNames) : base(ctx, IntPtr.Zero) { - Contract.Requires(ctx != null); - Contract.Requires(name != null); - Contract.Requires(enumNames != null); + Debug.Assert(ctx != null); + Debug.Assert(name != null); + Debug.Assert(enumNames != null); int n = enumNames.Length; IntPtr[] n_constdecls = new IntPtr[n]; diff --git a/src/api/dotnet/Expr.cs b/src/api/dotnet/Expr.cs index 5d1896221..f735401d8 100644 --- a/src/api/dotnet/Expr.cs +++ b/src/api/dotnet/Expr.cs @@ -17,15 +17,16 @@ Notes: --*/ +using System.Diagnostics; using System; -using System.Diagnostics.Contracts; +using System.Linq; + namespace Microsoft.Z3 { /// /// Expressions are terms. /// - [ContractVerification(true)] public class Expr : AST { /// @@ -35,7 +36,6 @@ namespace Microsoft.Z3 /// public Expr Simplify(Params p = null) { - Contract.Ensures(Contract.Result() != null); if (p == null) return Expr.Create(Context, Native.Z3_simplify(Context.nCtx, NativeObject)); @@ -50,7 +50,6 @@ namespace Microsoft.Z3 { get { - Contract.Ensures(Contract.Result() != null); return new FuncDecl(Context, Native.Z3_get_app_decl(Context.nCtx, NativeObject)); } } @@ -79,7 +78,6 @@ namespace Microsoft.Z3 { get { - Contract.Ensures(Contract.Result() != null); uint n = NumArgs; Expr[] res = new Expr[n]; @@ -94,7 +92,6 @@ namespace Microsoft.Z3 /// public Expr Arg(uint i) { - Contract.Ensures(Contract.Result() != null); return Expr.Create(Context, Native.Z3_get_app_arg(Context.nCtx, NativeObject, i)); } @@ -104,8 +101,8 @@ namespace Microsoft.Z3 /// public void Update(Expr[] args) { - Contract.Requires(args != null); - Contract.Requires(Contract.ForAll(args, a => a != null)); + Debug.Assert(args != null); + Debug.Assert(args.All(a => a != null)); Context.CheckContextMatch(args); if (IsApp && args.Length != NumArgs) @@ -123,11 +120,10 @@ namespace Microsoft.Z3 /// public Expr Substitute(Expr[] from, Expr[] to) { - Contract.Requires(from != null); - Contract.Requires(to != null); - Contract.Requires(Contract.ForAll(from, f => f != null)); - Contract.Requires(Contract.ForAll(to, t => t != null)); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(from != null); + Debug.Assert(to != null); + Debug.Assert(from.All(f => f != null)); + Debug.Assert(to.All(t => t != null)); Context.CheckContextMatch(from); Context.CheckContextMatch(to); @@ -142,9 +138,8 @@ namespace Microsoft.Z3 /// public Expr Substitute(Expr from, Expr to) { - Contract.Requires(from != null); - Contract.Requires(to != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(from != null); + Debug.Assert(to != null); return Substitute(new Expr[] { from }, new Expr[] { to }); } @@ -157,9 +152,8 @@ namespace Microsoft.Z3 /// public Expr SubstituteVars(Expr[] to) { - Contract.Requires(to != null); - Contract.Requires(Contract.ForAll(to, t => t != null)); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(to != null); + Debug.Assert(to.All(t => t != null)); Context.CheckContextMatch(to); return Expr.Create(Context, Native.Z3_substitute_vars(Context.nCtx, NativeObject, (uint)to.Length, Expr.ArrayToNative(to))); @@ -207,7 +201,6 @@ namespace Microsoft.Z3 { get { - Contract.Ensures(Contract.Result() != null); return Sort.Create(Context, Native.Z3_get_sort(Context.nCtx, NativeObject)); } } @@ -332,7 +325,7 @@ namespace Microsoft.Z3 /// /// Retrieve bound of at-most /// - public uint AtMostBound { get { Contract.Requires(IsAtMost); return (uint)FuncDecl.Parameters[0].Int; } } + public uint AtMostBound { get { Debug.Assert(IsAtMost); return (uint)FuncDecl.Parameters[0].Int; } } /// /// Indicates whether the term is at-least @@ -342,7 +335,7 @@ namespace Microsoft.Z3 /// /// Retrieve bound of at-least /// - public uint AtLeastBound { get { Contract.Requires(IsAtLeast); return (uint)FuncDecl.Parameters[0].Int; } } + public uint AtLeastBound { get { Debug.Assert(IsAtLeast); return (uint)FuncDecl.Parameters[0].Int; } } /// /// Indicates whether the term is pbeq @@ -1816,8 +1809,6 @@ namespace Microsoft.Z3 if (!IsVar) throw new Z3Exception("Term is not a bound variable."); - Contract.EndContractBlock(); - return Native.Z3_get_index_value(Context.nCtx, NativeObject); } } @@ -1827,10 +1818,9 @@ namespace Microsoft.Z3 /// /// Constructor for Expr /// - internal protected Expr(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); } + internal protected Expr(Context ctx, IntPtr obj) : base(ctx, obj) { Debug.Assert(ctx != null); } #if DEBUG - [Pure] internal override void CheckNativeObject(IntPtr obj) { if (Native.Z3_is_app(Context.nCtx, obj) == 0 && @@ -1841,12 +1831,10 @@ namespace Microsoft.Z3 } #endif - [Pure] internal static Expr Create(Context ctx, FuncDecl f, params Expr[] arguments) { - Contract.Requires(ctx != null); - Contract.Requires(f != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(ctx != null); + Debug.Assert(f != null); IntPtr obj = Native.Z3_mk_app(ctx.nCtx, f.NativeObject, AST.ArrayLength(arguments), @@ -1854,11 +1842,9 @@ namespace Microsoft.Z3 return Create(ctx, obj); } - [Pure] new internal static Expr Create(Context ctx, IntPtr obj) { - Contract.Requires(ctx != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(ctx != null); Z3_ast_kind k = (Z3_ast_kind)Native.Z3_get_ast_kind(ctx.nCtx, obj); if (k == Z3_ast_kind.Z3_QUANTIFIER_AST) diff --git a/src/api/dotnet/FPExpr.cs b/src/api/dotnet/FPExpr.cs index 85fdf2603..03ae0bff1 100644 --- a/src/api/dotnet/FPExpr.cs +++ b/src/api/dotnet/FPExpr.cs @@ -16,12 +16,12 @@ Author: Notes: --*/ +using System.Diagnostics; using System; using System.Collections.Generic; using System.Linq; using System.Text; -using System.Diagnostics.Contracts; namespace Microsoft.Z3 { @@ -45,7 +45,7 @@ namespace Microsoft.Z3 internal FPExpr(Context ctx, IntPtr obj) : base(ctx, obj) { - Contract.Requires(ctx != null); + Debug.Assert(ctx != null); } #endregion } diff --git a/src/api/dotnet/FPNum.cs b/src/api/dotnet/FPNum.cs index b6d349149..e21355f72 100644 --- a/src/api/dotnet/FPNum.cs +++ b/src/api/dotnet/FPNum.cs @@ -16,15 +16,14 @@ Author: Notes: --*/ +using System.Diagnostics; using System; -using System.Diagnostics.Contracts; namespace Microsoft.Z3 { /// /// FloatiungPoint Numerals /// - [ContractVerification(true)] public class FPNum : FPExpr { /// @@ -175,7 +174,7 @@ namespace Microsoft.Z3 internal FPNum(Context ctx, IntPtr obj) : base(ctx, obj) { - Contract.Requires(ctx != null); + Debug.Assert(ctx != null); } #endregion diff --git a/src/api/dotnet/FPRMExpr.cs b/src/api/dotnet/FPRMExpr.cs index 896c3e6b9..4c4ae602f 100644 --- a/src/api/dotnet/FPRMExpr.cs +++ b/src/api/dotnet/FPRMExpr.cs @@ -16,12 +16,12 @@ Author: Notes: --*/ +using System.Diagnostics; using System; using System.Collections.Generic; using System.Linq; using System.Text; -using System.Diagnostics.Contracts; namespace Microsoft.Z3 { @@ -35,7 +35,7 @@ namespace Microsoft.Z3 internal FPRMExpr(Context ctx, IntPtr obj) : base(ctx, obj) { - Contract.Requires(ctx != null); + Debug.Assert(ctx != null); } #endregion } diff --git a/src/api/dotnet/FPRMNum.cs b/src/api/dotnet/FPRMNum.cs index 81cff167e..af1c8b888 100644 --- a/src/api/dotnet/FPRMNum.cs +++ b/src/api/dotnet/FPRMNum.cs @@ -16,12 +16,12 @@ Author: Notes: --*/ +using System.Diagnostics; using System; using System.Collections.Generic; using System.Linq; using System.Text; -using System.Diagnostics.Contracts; namespace Microsoft.Z3 { @@ -93,7 +93,7 @@ namespace Microsoft.Z3 internal FPRMNum(Context ctx, IntPtr obj) : base(ctx, obj) { - Contract.Requires(ctx != null); + Debug.Assert(ctx != null); } #endregion } diff --git a/src/api/dotnet/FPRMSort.cs b/src/api/dotnet/FPRMSort.cs index 1d8334eb5..4e04a2586 100644 --- a/src/api/dotnet/FPRMSort.cs +++ b/src/api/dotnet/FPRMSort.cs @@ -17,8 +17,8 @@ Notes: --*/ +using System.Diagnostics; using System; -using System.Diagnostics.Contracts; namespace Microsoft.Z3 { @@ -31,12 +31,12 @@ namespace Microsoft.Z3 internal FPRMSort(Context ctx, IntPtr obj) : base(ctx, obj) { - Contract.Requires(ctx != null); + Debug.Assert(ctx != null); } internal FPRMSort(Context ctx) : base(ctx, Native.Z3_mk_fpa_rounding_mode_sort(ctx.nCtx)) { - Contract.Requires(ctx != null); + Debug.Assert(ctx != null); } #endregion } diff --git a/src/api/dotnet/FPSort.cs b/src/api/dotnet/FPSort.cs index e1ad62d49..56a738e65 100644 --- a/src/api/dotnet/FPSort.cs +++ b/src/api/dotnet/FPSort.cs @@ -16,8 +16,8 @@ Author: Notes: --*/ +using System.Diagnostics; using System; -using System.Diagnostics.Contracts; namespace Microsoft.Z3 { @@ -40,12 +40,12 @@ namespace Microsoft.Z3 internal FPSort(Context ctx, IntPtr obj) : base(ctx, obj) { - Contract.Requires(ctx != null); + Debug.Assert(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); + Debug.Assert(ctx != null); } #endregion } diff --git a/src/api/dotnet/FiniteDomainExpr.cs b/src/api/dotnet/FiniteDomainExpr.cs index 59ccb9f32..1a689d59f 100644 --- a/src/api/dotnet/FiniteDomainExpr.cs +++ b/src/api/dotnet/FiniteDomainExpr.cs @@ -16,8 +16,8 @@ Author: Notes: --*/ +using System.Diagnostics; using System; -using System.Diagnostics.Contracts; namespace Microsoft.Z3 { @@ -31,7 +31,7 @@ namespace Microsoft.Z3 internal FiniteDomainExpr(Context ctx, IntPtr obj) : base(ctx, obj) { - Contract.Requires(ctx != null); + Debug.Assert(ctx != null); } #endregion } diff --git a/src/api/dotnet/FiniteDomainNum.cs b/src/api/dotnet/FiniteDomainNum.cs index 52c0af8bd..39d94ddbd 100644 --- a/src/api/dotnet/FiniteDomainNum.cs +++ b/src/api/dotnet/FiniteDomainNum.cs @@ -16,8 +16,8 @@ Author: Notes: --*/ +using System.Diagnostics; using System; -using System.Diagnostics.Contracts; #if !FRAMEWORK_LT_4 using System.Numerics; @@ -28,7 +28,6 @@ namespace Microsoft.Z3 /// /// Finite-domain numerals /// - [ContractVerification(true)] public class FiniteDomainNum : FiniteDomainExpr { /// @@ -109,7 +108,7 @@ namespace Microsoft.Z3 } #region Internal - internal FiniteDomainNum(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); } + internal FiniteDomainNum(Context ctx, IntPtr obj) : base(ctx, obj) { Debug.Assert(ctx != null); } #endregion } } diff --git a/src/api/dotnet/FiniteDomainSort.cs b/src/api/dotnet/FiniteDomainSort.cs index 93540ff87..5392aede2 100644 --- a/src/api/dotnet/FiniteDomainSort.cs +++ b/src/api/dotnet/FiniteDomainSort.cs @@ -17,15 +17,14 @@ Notes: --*/ +using System.Diagnostics; using System; -using System.Diagnostics.Contracts; namespace Microsoft.Z3 { /// /// Finite domain sorts. /// - [ContractVerification(true)] public class FiniteDomainSort : Sort { /// @@ -45,13 +44,13 @@ namespace Microsoft.Z3 internal FiniteDomainSort(Context ctx, IntPtr obj) : base(ctx, obj) { - Contract.Requires(ctx != null); + Debug.Assert(ctx != null); } internal FiniteDomainSort(Context ctx, Symbol name, ulong size) : base(ctx, Native.Z3_mk_finite_domain_sort(ctx.nCtx, name.NativeObject, size)) { - Contract.Requires(ctx != null); - Contract.Requires(name != null); + Debug.Assert(ctx != null); + Debug.Assert(name != null); } #endregion diff --git a/src/api/dotnet/Fixedpoint.cs b/src/api/dotnet/Fixedpoint.cs index 102a96ac5..51ee79b55 100644 --- a/src/api/dotnet/Fixedpoint.cs +++ b/src/api/dotnet/Fixedpoint.cs @@ -18,14 +18,14 @@ Notes: --*/ using System; -using System.Diagnostics.Contracts; +using System.Diagnostics; +using System.Linq; namespace Microsoft.Z3 { /// /// Object for managing fixedpoints /// - [ContractVerification(true)] public class Fixedpoint : Z3Object { @@ -36,7 +36,6 @@ namespace Microsoft.Z3 { get { - Contract.Ensures(Contract.Result() != null); return Native.Z3_fixedpoint_get_help(Context.nCtx, NativeObject); } } @@ -48,7 +47,7 @@ namespace Microsoft.Z3 { set { - Contract.Requires(value != null); + Debug.Assert(value != null); Context.CheckContextMatch(value); Native.Z3_fixedpoint_set_params(Context.nCtx, NativeObject, value.NativeObject); } @@ -68,8 +67,8 @@ namespace Microsoft.Z3 /// public void Assert(params BoolExpr[] constraints) { - Contract.Requires(constraints != null); - Contract.Requires(Contract.ForAll(constraints, c => c != null)); + Debug.Assert(constraints != null); + Debug.Assert(constraints.All(c => c != null)); Context.CheckContextMatch(constraints); foreach (BoolExpr a in constraints) @@ -91,7 +90,7 @@ namespace Microsoft.Z3 /// public void RegisterRelation(FuncDecl f) { - Contract.Requires(f != null); + Debug.Assert(f != null); Context.CheckContextMatch(f); Native.Z3_fixedpoint_register_relation(Context.nCtx, NativeObject, f.NativeObject); @@ -102,7 +101,7 @@ namespace Microsoft.Z3 /// public void AddRule(BoolExpr rule, Symbol name = null) { - Contract.Requires(rule != null); + Debug.Assert(rule != null); Context.CheckContextMatch(rule); Native.Z3_fixedpoint_add_rule(Context.nCtx, NativeObject, rule.NativeObject, AST.GetNativeObject(name)); @@ -113,8 +112,8 @@ namespace Microsoft.Z3 /// public void AddFact(FuncDecl pred, params uint[] args) { - Contract.Requires(pred != null); - Contract.Requires(args != null); + Debug.Assert(pred != null); + Debug.Assert(args != null); Context.CheckContextMatch(pred); Native.Z3_fixedpoint_add_fact(Context.nCtx, NativeObject, pred.NativeObject, (uint)args.Length, args); @@ -128,7 +127,7 @@ namespace Microsoft.Z3 /// public Status Query(BoolExpr query) { - Contract.Requires(query != null); + Debug.Assert(query != null); Context.CheckContextMatch(query); Z3_lbool r = (Z3_lbool)Native.Z3_fixedpoint_query(Context.nCtx, NativeObject, query.NativeObject); @@ -148,8 +147,8 @@ namespace Microsoft.Z3 /// public Status Query(params FuncDecl[] relations) { - Contract.Requires(relations != null); - Contract.Requires(Contract.ForAll(0, relations.Length, i => relations[i] != null)); + Debug.Assert(relations != null); + Debug.Assert(relations.All(rel => rel != null)); Context.CheckContextMatch(relations); Z3_lbool r = (Z3_lbool)Native.Z3_fixedpoint_query_relations(Context.nCtx, NativeObject, @@ -187,7 +186,7 @@ namespace Microsoft.Z3 /// public void UpdateRule(BoolExpr rule, Symbol name) { - Contract.Requires(rule != null); + Debug.Assert(rule != null); Context.CheckContextMatch(rule); Native.Z3_fixedpoint_update_rule(Context.nCtx, NativeObject, rule.NativeObject, AST.GetNativeObject(name)); @@ -208,7 +207,6 @@ namespace Microsoft.Z3 /// public string GetReasonUnknown() { - Contract.Ensures(Contract.Result() != null); return Native.Z3_fixedpoint_get_reason_unknown(Context.nCtx, NativeObject); } @@ -252,7 +250,7 @@ namespace Microsoft.Z3 /// public void SetPredicateRepresentation(FuncDecl f, Symbol[] kinds) { - Contract.Requires(f != null); + Debug.Assert(f != null); Native.Z3_fixedpoint_set_predicate_representation(Context.nCtx, NativeObject, f.NativeObject, AST.ArrayLength(kinds), Symbol.ArrayToNative(kinds)); @@ -276,7 +274,6 @@ namespace Microsoft.Z3 { get { - Contract.Ensures(Contract.Result() != null); ASTVector av = new ASTVector(Context, Native.Z3_fixedpoint_get_rules(Context.nCtx, NativeObject)); return av.ToBoolExprArray(); @@ -290,7 +287,6 @@ namespace Microsoft.Z3 { get { - Contract.Ensures(Contract.Result() != null); ASTVector av = new ASTVector(Context, Native.Z3_fixedpoint_get_assertions(Context.nCtx, NativeObject)); return av.ToBoolExprArray(); @@ -304,7 +300,6 @@ namespace Microsoft.Z3 { get { - Contract.Ensures(Contract.Result() != null); return new Statistics(Context, Native.Z3_fixedpoint_get_statistics(Context.nCtx, NativeObject)); } @@ -335,12 +330,12 @@ namespace Microsoft.Z3 internal Fixedpoint(Context ctx, IntPtr obj) : base(ctx, obj) { - Contract.Requires(ctx != null); + Debug.Assert(ctx != null); } internal Fixedpoint(Context ctx) : base(ctx, Native.Z3_mk_fixedpoint(ctx.nCtx)) { - Contract.Requires(ctx != null); + Debug.Assert(ctx != null); } internal class DecRefQueue : IDecRefQueue diff --git a/src/api/dotnet/FuncDecl.cs b/src/api/dotnet/FuncDecl.cs index 0587a2276..24ae456d8 100644 --- a/src/api/dotnet/FuncDecl.cs +++ b/src/api/dotnet/FuncDecl.cs @@ -18,14 +18,15 @@ Notes: --*/ using System; -using System.Diagnostics.Contracts; +using System.Diagnostics; +using System.Linq; + namespace Microsoft.Z3 { /// /// Function declarations. /// - [ContractVerification(true)] public class FuncDecl : AST { /// @@ -108,7 +109,6 @@ namespace Microsoft.Z3 { get { - Contract.Ensures(Contract.Result() != null); uint n = DomainSize; @@ -126,7 +126,6 @@ namespace Microsoft.Z3 { get { - Contract.Ensures(Contract.Result() != null); return Sort.Create(Context, Native.Z3_get_range(Context.nCtx, NativeObject)); } } @@ -146,7 +145,6 @@ namespace Microsoft.Z3 { get { - Contract.Ensures(Contract.Result() != null); return Symbol.Create(Context, Native.Z3_get_decl_name(Context.nCtx, NativeObject)); } } @@ -166,7 +164,6 @@ namespace Microsoft.Z3 { get { - Contract.Ensures(Contract.Result() != null); uint num = NumParameters; Parameter[] res = new Parameter[num]; @@ -287,22 +284,22 @@ namespace Microsoft.Z3 internal FuncDecl(Context ctx, IntPtr obj) : base(ctx, obj) { - Contract.Requires(ctx != null); + Debug.Assert(ctx != null); } internal FuncDecl(Context ctx, Symbol name, Sort[] domain, Sort range) : base(ctx, Native.Z3_mk_func_decl(ctx.nCtx, name.NativeObject, AST.ArrayLength(domain), AST.ArrayToNative(domain), range.NativeObject)) { - Contract.Requires(ctx != null); - Contract.Requires(name != null); - Contract.Requires(range != null); + Debug.Assert(ctx != null); + Debug.Assert(name != null); + Debug.Assert(range != null); } internal FuncDecl(Context ctx, string prefix, Sort[] domain, Sort range) : base(ctx, Native.Z3_mk_fresh_func_decl(ctx.nCtx, prefix, AST.ArrayLength(domain), AST.ArrayToNative(domain), range.NativeObject)) { - Contract.Requires(ctx != null); - Contract.Requires(range != null); + Debug.Assert(ctx != null); + Debug.Assert(range != null); } #if DEBUG @@ -335,7 +332,7 @@ namespace Microsoft.Z3 { get { - Contract.Requires(args == null || Contract.ForAll(args, a => a != null)); + Debug.Assert(args == null || args.All(a => a != null)); return Apply(args); } @@ -348,7 +345,7 @@ namespace Microsoft.Z3 /// public Expr Apply(params Expr[] args) { - Contract.Requires(args == null || Contract.ForAll(args, a => a != null)); + Debug.Assert(args == null || args.All(a => a != null)); Context.CheckContextMatch(args); return Expr.Create(Context, this, args); diff --git a/src/api/dotnet/FuncInterp.cs b/src/api/dotnet/FuncInterp.cs index 449d460f9..6924049d3 100644 --- a/src/api/dotnet/FuncInterp.cs +++ b/src/api/dotnet/FuncInterp.cs @@ -17,8 +17,8 @@ Notes: --*/ +using System.Diagnostics; using System; -using System.Diagnostics.Contracts; namespace Microsoft.Z3 { @@ -26,7 +26,6 @@ namespace Microsoft.Z3 /// A function interpretation is represented as a finite map and an 'else' value. /// Each entry in the finite map represents the value of a function given a set of arguments. /// - [ContractVerification(true)] public class FuncInterp : Z3Object { /// @@ -42,7 +41,6 @@ namespace Microsoft.Z3 { get { - Contract.Ensures(Contract.Result() != null); return Expr.Create(Context, Native.Z3_func_entry_get_value(Context.nCtx, NativeObject)); } } @@ -62,8 +60,6 @@ namespace Microsoft.Z3 { get { - Contract.Ensures(Contract.Result() != null); - Contract.Ensures(Contract.Result().Length == this.NumArgs); uint n = NumArgs; Expr[] res = new Expr[n]; @@ -87,7 +83,7 @@ namespace Microsoft.Z3 } #region Internal - internal Entry(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); } + internal Entry(Context ctx, IntPtr obj) : base(ctx, obj) { Debug.Assert(ctx != null); } internal class DecRefQueue : IDecRefQueue { @@ -133,8 +129,6 @@ namespace Microsoft.Z3 { get { - Contract.Ensures(Contract.Result() != null); - Contract.Ensures(Contract.ForAll(0, Contract.Result().Length, j => Contract.Result()[j] != null)); uint n = NumEntries; Entry[] res = new Entry[n]; @@ -151,7 +145,6 @@ namespace Microsoft.Z3 { get { - Contract.Ensures(Contract.Result() != null); return Expr.Create(Context, Native.Z3_func_interp_get_else(Context.nCtx, NativeObject)); } @@ -194,7 +187,7 @@ namespace Microsoft.Z3 internal FuncInterp(Context ctx, IntPtr obj) : base(ctx, obj) { - Contract.Requires(ctx != null); + Debug.Assert(ctx != null); } internal class DecRefQueue : IDecRefQueue diff --git a/src/api/dotnet/Global.cs b/src/api/dotnet/Global.cs index 17963b33d..207498760 100644 --- a/src/api/dotnet/Global.cs +++ b/src/api/dotnet/Global.cs @@ -17,9 +17,9 @@ Notes: --*/ +using System.Diagnostics; using System; using System.Runtime.InteropServices; -using System.Diagnostics.Contracts; namespace Microsoft.Z3 { diff --git a/src/api/dotnet/Goal.cs b/src/api/dotnet/Goal.cs index ef2e9a5da..4dbc78b7e 100644 --- a/src/api/dotnet/Goal.cs +++ b/src/api/dotnet/Goal.cs @@ -18,7 +18,8 @@ Notes: --*/ using System; -using System.Diagnostics.Contracts; +using System.Diagnostics; +using System.Linq; namespace Microsoft.Z3 { @@ -27,7 +28,6 @@ namespace Microsoft.Z3 /// of formulas, that can be solved and/or transformed using /// tactics and solvers. /// - [ContractVerification(true)] public class Goal : Z3Object { /// @@ -79,13 +79,13 @@ namespace Microsoft.Z3 /// public void Assert(params BoolExpr[] constraints) { - Contract.Requires(constraints != null); - Contract.Requires(Contract.ForAll(constraints, c => c != null)); + Debug.Assert(constraints != null); + Debug.Assert(constraints.All(c => c != null)); Context.CheckContextMatch(constraints); foreach (BoolExpr c in constraints) { - Contract.Assert(c != null); // It was an assume, now made an assert just to be sure we do not regress + Debug.Assert(c != null); // It was an assume, now made an assert just to be sure we do not regress Native.Z3_goal_assert(Context.nCtx, NativeObject, c.NativeObject); } } @@ -140,7 +140,6 @@ namespace Microsoft.Z3 { get { - Contract.Ensures(Contract.Result() != null); uint n = Size; BoolExpr[] res = new BoolExpr[n]; @@ -181,7 +180,6 @@ namespace Microsoft.Z3 /// A model for g public Model ConvertModel(Model m) { - Contract.Ensures(Contract.Result() != null); if (m != null) return new Model(Context, Native.Z3_goal_convert_model(Context.nCtx, NativeObject, m.NativeObject)); else @@ -194,7 +192,7 @@ namespace Microsoft.Z3 /// public Goal Translate(Context ctx) { - Contract.Requires(ctx != null); + Debug.Assert(ctx != null); return new Goal(ctx, Native.Z3_goal_translate(Context.nCtx, NativeObject, ctx.nCtx)); } @@ -248,12 +246,12 @@ namespace Microsoft.Z3 } #region Internal - internal Goal(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); } + internal Goal(Context ctx, IntPtr obj) : base(ctx, obj) { Debug.Assert(ctx != null); } internal Goal(Context ctx, bool models, bool unsatCores, bool proofs) : base(ctx, Native.Z3_mk_goal(ctx.nCtx, (byte)(models ? 1 : 0), (byte)(unsatCores ? 1 : 0), (byte)(proofs ? 1 : 0))) { - Contract.Requires(ctx != null); + Debug.Assert(ctx != null); } internal class DecRefQueue : IDecRefQueue diff --git a/src/api/dotnet/IDecRefQueue.cs b/src/api/dotnet/IDecRefQueue.cs index 43506fabf..8af0973d6 100644 --- a/src/api/dotnet/IDecRefQueue.cs +++ b/src/api/dotnet/IDecRefQueue.cs @@ -17,26 +17,24 @@ Notes: --*/ +using System.Diagnostics; using System; using System.Collections; using System.Collections.Generic; using System.Threading; -using System.Diagnostics.Contracts; namespace Microsoft.Z3 { /// /// DecRefQueue interface /// - [ContractClass(typeof(DecRefQueueContracts))] public abstract class IDecRefQueue { #region Object invariant - [ContractInvariantMethod] private void ObjectInvariant() { - Contract.Invariant(this.m_queue != null); + Debug.Assert(this.m_queue != null); } #endregion @@ -61,7 +59,7 @@ namespace Microsoft.Z3 internal void IncAndClear(Context ctx, IntPtr o) { - Contract.Requires(ctx != null); + Debug.Assert(ctx != null); IncRef(ctx, o); if (m_queue.Count >= m_move_limit) Clear(ctx); @@ -79,7 +77,7 @@ namespace Microsoft.Z3 internal void Clear(Context ctx) { - Contract.Requires(ctx != null); + Debug.Assert(ctx != null); lock (m_lock) { @@ -90,17 +88,16 @@ namespace Microsoft.Z3 } } - [ContractClassFor(typeof(IDecRefQueue))] abstract class DecRefQueueContracts : IDecRefQueue { internal override void IncRef(Context ctx, IntPtr obj) { - Contract.Requires(ctx != null); + Debug.Assert(ctx != null); } internal override void DecRef(Context ctx, IntPtr obj) { - Contract.Requires(ctx != null); + Debug.Assert(ctx != null); } } } diff --git a/src/api/dotnet/IntExpr.cs b/src/api/dotnet/IntExpr.cs index 622be7bd5..3ca5398ea 100644 --- a/src/api/dotnet/IntExpr.cs +++ b/src/api/dotnet/IntExpr.cs @@ -16,12 +16,12 @@ Author: Notes: --*/ +using System.Diagnostics; using System; using System.Collections.Generic; using System.Linq; using System.Text; -using System.Diagnostics.Contracts; namespace Microsoft.Z3 { @@ -35,7 +35,7 @@ namespace Microsoft.Z3 internal IntExpr(Context ctx, IntPtr obj) : base(ctx, obj) { - Contract.Requires(ctx != null); + Debug.Assert(ctx != null); } #endregion } diff --git a/src/api/dotnet/IntNum.cs b/src/api/dotnet/IntNum.cs index 64fd78ad2..36f209cab 100644 --- a/src/api/dotnet/IntNum.cs +++ b/src/api/dotnet/IntNum.cs @@ -16,8 +16,8 @@ Author: Notes: --*/ +using System.Diagnostics; using System; -using System.Diagnostics.Contracts; #if !FRAMEWORK_LT_4 using System.Numerics; @@ -28,7 +28,6 @@ namespace Microsoft.Z3 /// /// Integer Numerals /// - [ContractVerification(true)] public class IntNum : IntExpr { @@ -36,7 +35,7 @@ namespace Microsoft.Z3 internal IntNum(Context ctx, IntPtr obj) : base(ctx, obj) { - Contract.Requires(ctx != null); + Debug.Assert(ctx != null); } #endregion diff --git a/src/api/dotnet/IntSort.cs b/src/api/dotnet/IntSort.cs index d0c25ac79..289be4bcc 100644 --- a/src/api/dotnet/IntSort.cs +++ b/src/api/dotnet/IntSort.cs @@ -17,8 +17,8 @@ Notes: --*/ +using System.Diagnostics; using System; -using System.Diagnostics.Contracts; namespace Microsoft.Z3 { @@ -31,12 +31,12 @@ namespace Microsoft.Z3 internal IntSort(Context ctx, IntPtr obj) : base(ctx, obj) { - Contract.Requires(ctx != null); + Debug.Assert(ctx != null); } internal IntSort(Context ctx) : base(ctx, Native.Z3_mk_int_sort(ctx.nCtx)) { - Contract.Requires(ctx != null); + Debug.Assert(ctx != null); } #endregion } diff --git a/src/api/dotnet/IntSymbol.cs b/src/api/dotnet/IntSymbol.cs index df2d9da52..1bb3b3f13 100644 --- a/src/api/dotnet/IntSymbol.cs +++ b/src/api/dotnet/IntSymbol.cs @@ -18,15 +18,14 @@ Notes: --*/ using System; +using System.Diagnostics; using System.Runtime.InteropServices; -using System.Diagnostics.Contracts; namespace Microsoft.Z3 { /// /// Numbered symbols /// - [ContractVerification(true)] public class IntSymbol : Symbol { /// @@ -47,12 +46,12 @@ namespace Microsoft.Z3 internal IntSymbol(Context ctx, IntPtr obj) : base(ctx, obj) { - Contract.Requires(ctx != null); + Debug.Assert(ctx != null); } internal IntSymbol(Context ctx, int i) : base(ctx, Native.Z3_mk_int_symbol(ctx.nCtx, i)) { - Contract.Requires(ctx != null); + Debug.Assert(ctx != null); } #if DEBUG diff --git a/src/api/dotnet/Lambda.cs b/src/api/dotnet/Lambda.cs index b3dc6c01c..35497f88f 100644 --- a/src/api/dotnet/Lambda.cs +++ b/src/api/dotnet/Lambda.cs @@ -18,14 +18,14 @@ Notes: --*/ using System; -using System.Diagnostics.Contracts; +using System.Diagnostics; +using System.Linq; namespace Microsoft.Z3 { /// /// Lambda expressions. /// - [ContractVerification(true)] public class Lambda : ArrayExpr { /// @@ -43,7 +43,6 @@ namespace Microsoft.Z3 { get { - Contract.Ensures(Contract.Result() != null); uint n = NumBound; Symbol[] res = new Symbol[n]; @@ -60,7 +59,6 @@ namespace Microsoft.Z3 { get { - Contract.Ensures(Contract.Result() != null); uint n = NumBound; Sort[] res = new Sort[n]; @@ -77,7 +75,6 @@ namespace Microsoft.Z3 { get { - Contract.Ensures(Contract.Result() != null); return new BoolExpr(Context, Native.Z3_get_quantifier_body(Context.nCtx, NativeObject)); } @@ -94,17 +91,16 @@ namespace Microsoft.Z3 } #region Internal - [ContractVerification(false)] // F: Clousot ForAll decompilation gets confused below. Setting verification off until I fixed the bug internal Lambda(Context ctx, Sort[] sorts, Symbol[] names, Expr body) : base(ctx, IntPtr.Zero) { - Contract.Requires(ctx != null); - Contract.Requires(sorts != null); - Contract.Requires(names != null); - Contract.Requires(body != null); - Contract.Requires(sorts.Length == names.Length); - Contract.Requires(Contract.ForAll(sorts, s => s != null)); - Contract.Requires(Contract.ForAll(names, n => n != null)); + Debug.Assert(ctx != null); + Debug.Assert(sorts != null); + Debug.Assert(names != null); + Debug.Assert(body != null); + Debug.Assert(sorts.Length == names.Length); + Debug.Assert(sorts.All(s => s != null)); + Debug.Assert(names.All(n => n != null)); Context.CheckContextMatch(sorts); Context.CheckContextMatch(names); Context.CheckContextMatch(body); @@ -119,14 +115,13 @@ namespace Microsoft.Z3 } - [ContractVerification(false)] // F: Clousot ForAll decompilation gets confused below. Setting verification off until I fixed the bug internal Lambda(Context ctx, Expr[] bound, Expr body) : base(ctx, IntPtr.Zero) { - Contract.Requires(ctx != null); - Contract.Requires(body != null); + Debug.Assert(ctx != null); + Debug.Assert(body != null); - Contract.Requires(bound != null && bound.Length > 0 && Contract.ForAll(bound, n => n != null)); + Debug.Assert(bound != null && bound.Length > 0 && bound.All(n => n != null)); Context.CheckContextMatch(bound); Context.CheckContextMatch(body); @@ -137,7 +132,7 @@ namespace Microsoft.Z3 } - internal Lambda(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); } + internal Lambda(Context ctx, IntPtr obj) : base(ctx, obj) { Debug.Assert(ctx != null); } #if DEBUG internal override void CheckNativeObject(IntPtr obj) diff --git a/src/api/dotnet/ListSort.cs b/src/api/dotnet/ListSort.cs index e860e4d4b..575f2a9bb 100644 --- a/src/api/dotnet/ListSort.cs +++ b/src/api/dotnet/ListSort.cs @@ -17,15 +17,14 @@ Notes: --*/ +using System.Diagnostics; using System; -using System.Diagnostics.Contracts; namespace Microsoft.Z3 { /// /// List sorts. /// - [ContractVerification(true)] public class ListSort : Sort { /// @@ -35,7 +34,6 @@ namespace Microsoft.Z3 { get { - Contract.Ensures(Contract.Result() != null); return new FuncDecl(Context, Native.Z3_get_datatype_sort_constructor(Context.nCtx, NativeObject, 0)); } } @@ -47,7 +45,6 @@ namespace Microsoft.Z3 { get { - Contract.Ensures(Contract.Result() != null); return Context.MkApp(NilDecl); } } @@ -59,7 +56,6 @@ namespace Microsoft.Z3 { get { - Contract.Ensures(Contract.Result() != null); return new FuncDecl(Context, Native.Z3_get_datatype_sort_recognizer(Context.nCtx, NativeObject, 0)); } } @@ -71,7 +67,6 @@ namespace Microsoft.Z3 { get { - Contract.Ensures(Contract.Result() != null); return new FuncDecl(Context, Native.Z3_get_datatype_sort_constructor(Context.nCtx, NativeObject, 1)); } } @@ -84,7 +79,6 @@ namespace Microsoft.Z3 { get { - Contract.Ensures(Contract.Result() != null); return new FuncDecl(Context, Native.Z3_get_datatype_sort_recognizer(Context.nCtx, NativeObject, 1)); } } @@ -96,7 +90,6 @@ namespace Microsoft.Z3 { get { - Contract.Ensures(Contract.Result() != null); return new FuncDecl(Context, Native.Z3_get_datatype_sort_constructor_accessor(Context.nCtx, NativeObject, 1, 0)); } } @@ -108,7 +101,6 @@ namespace Microsoft.Z3 { get { - Contract.Ensures(Contract.Result() != null); return new FuncDecl(Context, Native.Z3_get_datatype_sort_constructor_accessor(Context.nCtx, NativeObject, 1, 1)); } } @@ -117,9 +109,9 @@ namespace Microsoft.Z3 internal ListSort(Context ctx, Symbol name, Sort elemSort) : base(ctx, IntPtr.Zero) { - Contract.Requires(ctx != null); - Contract.Requires(name != null); - Contract.Requires(elemSort != null); + Debug.Assert(ctx != null); + Debug.Assert(name != null); + Debug.Assert(elemSort != null); IntPtr inil = IntPtr.Zero, iisnil = IntPtr.Zero, icons = IntPtr.Zero, iiscons = IntPtr.Zero, diff --git a/src/api/dotnet/Log.cs b/src/api/dotnet/Log.cs index f8b2ea88b..a94c29bc6 100644 --- a/src/api/dotnet/Log.cs +++ b/src/api/dotnet/Log.cs @@ -17,8 +17,8 @@ Notes: --*/ +using System.Diagnostics; using System; -using System.Diagnostics.Contracts; namespace Microsoft.Z3 { @@ -29,7 +29,6 @@ namespace Microsoft.Z3 /// Note that this is a global, static log and if multiple Context /// objects are created, it logs the interaction with all of them. /// - [ContractVerification(true)] public static class Log { private static bool m_is_open = false; @@ -59,7 +58,7 @@ namespace Microsoft.Z3 /// public static void Append(string s) { - Contract.Requires(isOpen()); + Debug.Assert(isOpen()); if (!m_is_open) throw new Z3Exception("Log cannot be closed."); @@ -70,7 +69,6 @@ namespace Microsoft.Z3 /// Checks whether the interaction log is opened. /// /// True if the interaction log is open, false otherwise. - [Pure] public static bool isOpen() { return m_is_open; diff --git a/src/api/dotnet/Model.cs b/src/api/dotnet/Model.cs index 96f62c9fb..c24516c22 100644 --- a/src/api/dotnet/Model.cs +++ b/src/api/dotnet/Model.cs @@ -18,7 +18,7 @@ Notes: --*/ using System; -using System.Diagnostics.Contracts; +using System.Diagnostics; using System.Collections.Generic; namespace Microsoft.Z3 @@ -26,7 +26,6 @@ namespace Microsoft.Z3 /// /// A Model contains interpretations (assignments) of constants and functions. /// - [ContractVerification(true)] public class Model : Z3Object { /// @@ -36,7 +35,7 @@ namespace Microsoft.Z3 /// An expression if the constant has an interpretation in the model, null otherwise. public Expr ConstInterp(Expr a) { - Contract.Requires(a != null); + Debug.Assert(a != null); Context.CheckContextMatch(a); return ConstInterp(a.FuncDecl); @@ -49,7 +48,7 @@ namespace Microsoft.Z3 /// An expression if the function has an interpretation in the model, null otherwise. public Expr ConstInterp(FuncDecl f) { - Contract.Requires(f != null); + Debug.Assert(f != null); Context.CheckContextMatch(f); if (f.Arity != 0 || @@ -70,7 +69,7 @@ namespace Microsoft.Z3 /// A FunctionInterpretation if the function has an interpretation in the model, null otherwise. public FuncInterp FuncInterp(FuncDecl f) { - Contract.Requires(f != null); + Debug.Assert(f != null); Context.CheckContextMatch(f); @@ -122,7 +121,6 @@ namespace Microsoft.Z3 { get { - Contract.Ensures(Contract.Result() != null); uint n = NumConsts; FuncDecl[] res = new FuncDecl[n]; @@ -165,7 +163,6 @@ namespace Microsoft.Z3 { get { - Contract.Ensures(Contract.Result() != null); uint n = NumFuncs; FuncDecl[] res = new FuncDecl[n]; @@ -182,7 +179,6 @@ namespace Microsoft.Z3 { get { - Contract.Ensures(Contract.Result() != null); uint nFuncs = NumFuncs; uint nConsts = NumConsts; @@ -223,8 +219,7 @@ namespace Microsoft.Z3 /// The evaluation of in the model. public Expr Eval(Expr t, bool completion = false) { - Contract.Requires(t != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(t != null); IntPtr v = IntPtr.Zero; if (Native.Z3_model_eval(Context.nCtx, NativeObject, t.NativeObject, (byte)(completion ? 1 : 0), ref v) == (byte)0) @@ -238,8 +233,7 @@ namespace Microsoft.Z3 /// public Expr Evaluate(Expr t, bool completion = false) { - Contract.Requires(t != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(t != null); return Eval(t, completion); } @@ -263,7 +257,6 @@ namespace Microsoft.Z3 { get { - Contract.Ensures(Contract.Result() != null); uint n = NumSorts; Sort[] res = new Sort[n]; @@ -281,8 +274,7 @@ namespace Microsoft.Z3 /// An array of expressions, where each is an element of the universe of public Expr[] SortUniverse(Sort s) { - Contract.Requires(s != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(s != null); ASTVector av = new ASTVector(Context, Native.Z3_model_get_sort_universe(Context.nCtx, NativeObject, s.NativeObject)); return av.ToExprArray(); @@ -301,7 +293,7 @@ namespace Microsoft.Z3 internal Model(Context ctx, IntPtr obj) : base(ctx, obj) { - Contract.Requires(ctx != null); + Debug.Assert(ctx != null); } internal class DecRefQueue : IDecRefQueue diff --git a/src/api/dotnet/Optimize.cs b/src/api/dotnet/Optimize.cs index ce3cc55f7..4713f414a 100644 --- a/src/api/dotnet/Optimize.cs +++ b/src/api/dotnet/Optimize.cs @@ -19,14 +19,14 @@ Notes: using System; using System.Collections.Generic; -using System.Diagnostics.Contracts; +using System.Diagnostics; +using System.Linq; namespace Microsoft.Z3 { /// /// Object for managing optimizization context /// - [ContractVerification(true)] public class Optimize : Z3Object { /// @@ -36,7 +36,6 @@ namespace Microsoft.Z3 { get { - Contract.Ensures(Contract.Result() != null); return Native.Z3_optimize_get_help(Context.nCtx, NativeObject); } } @@ -48,7 +47,7 @@ namespace Microsoft.Z3 { set { - Contract.Requires(value != null); + Debug.Assert(value != null); Context.CheckContextMatch(value); Native.Z3_optimize_set_params(Context.nCtx, NativeObject, value.NativeObject); } @@ -99,8 +98,8 @@ namespace Microsoft.Z3 /// private void AddConstraints(IEnumerable constraints) { - Contract.Requires(constraints != null); - Contract.Requires(Contract.ForAll(constraints, c => c != null)); + Debug.Assert(constraints != null); + Debug.Assert(constraints.All(c => c != null)); Context.CheckContextMatch(constraints); foreach (BoolExpr a in constraints) @@ -248,7 +247,6 @@ namespace Microsoft.Z3 { get { - Contract.Ensures(Contract.Result() != null); ASTVector core = new ASTVector(Context, Native.Z3_optimize_get_unsat_core(Context.nCtx, NativeObject)); return core.ToBoolExprArray(); @@ -319,7 +317,6 @@ namespace Microsoft.Z3 { get { - Contract.Ensures(Contract.Result() != null); return Native.Z3_optimize_get_reason_unknown(Context.nCtx, NativeObject); } } @@ -357,7 +354,6 @@ namespace Microsoft.Z3 { get { - Contract.Ensures(Contract.Result() != null); ASTVector assertions = new ASTVector(Context, Native.Z3_optimize_get_assertions(Context.nCtx, NativeObject)); return assertions.ToBoolExprArray(); @@ -371,7 +367,6 @@ namespace Microsoft.Z3 { get { - Contract.Ensures(Contract.Result() != null); ASTVector objectives = new ASTVector(Context, Native.Z3_optimize_get_objectives(Context.nCtx, NativeObject)); return objectives.ToExprArray(); @@ -386,7 +381,6 @@ namespace Microsoft.Z3 { get { - Contract.Ensures(Contract.Result() != null); return new Statistics(Context, Native.Z3_optimize_get_statistics(Context.nCtx, NativeObject)); } @@ -397,12 +391,12 @@ namespace Microsoft.Z3 internal Optimize(Context ctx, IntPtr obj) : base(ctx, obj) { - Contract.Requires(ctx != null); + Debug.Assert(ctx != null); } internal Optimize(Context ctx) : base(ctx, Native.Z3_mk_optimize(ctx.nCtx)) { - Contract.Requires(ctx != null); + Debug.Assert(ctx != null); } internal class DecRefQueue : IDecRefQueue diff --git a/src/api/dotnet/ParamDescrs.cs b/src/api/dotnet/ParamDescrs.cs index 1809518e1..fbfb9cd16 100644 --- a/src/api/dotnet/ParamDescrs.cs +++ b/src/api/dotnet/ParamDescrs.cs @@ -17,15 +17,14 @@ Notes: --*/ +using System.Diagnostics; using System; -using System.Diagnostics.Contracts; namespace Microsoft.Z3 { /// /// A ParamDescrs describes a set of parameters. /// - [ContractVerification(true)] public class ParamDescrs : Z3Object { /// @@ -33,7 +32,7 @@ namespace Microsoft.Z3 /// public void Validate(Params p) { - Contract.Requires(p != null); + Debug.Assert(p != null); Native.Z3_params_validate(Context.nCtx, p.NativeObject, NativeObject); } @@ -42,7 +41,7 @@ namespace Microsoft.Z3 /// public Z3_param_kind GetKind(Symbol name) { - Contract.Requires(name != null); + Debug.Assert(name != null); return (Z3_param_kind)Native.Z3_param_descrs_get_kind(Context.nCtx, NativeObject, name.NativeObject); } @@ -51,7 +50,7 @@ namespace Microsoft.Z3 /// public string GetDocumentation(Symbol name) { - Contract.Requires(name != null); + Debug.Assert(name != null); return Native.Z3_param_descrs_get_documentation(Context.nCtx, NativeObject, name.NativeObject); } @@ -91,7 +90,7 @@ namespace Microsoft.Z3 internal ParamDescrs(Context ctx, IntPtr obj) : base(ctx, obj) { - Contract.Requires(ctx != null); + Debug.Assert(ctx != null); } internal class DecRefQueue : IDecRefQueue diff --git a/src/api/dotnet/Params.cs b/src/api/dotnet/Params.cs index f0f28d8d3..e5926934a 100644 --- a/src/api/dotnet/Params.cs +++ b/src/api/dotnet/Params.cs @@ -17,15 +17,14 @@ Notes: --*/ +using System.Diagnostics; using System; -using System.Diagnostics.Contracts; namespace Microsoft.Z3 { /// /// A Params objects represents a configuration in the form of Symbol/value pairs. /// - [ContractVerification(true)] public class Params : Z3Object { /// @@ -33,7 +32,7 @@ namespace Microsoft.Z3 /// public Params Add(Symbol name, bool value) { - Contract.Requires(name != null); + Debug.Assert(name != null); Native.Z3_params_set_bool(Context.nCtx, NativeObject, name.NativeObject, (byte)(value ? 1 : 0)); return this; @@ -44,7 +43,7 @@ namespace Microsoft.Z3 /// public Params Add(Symbol name, uint value) { - Contract.Requires(name != null); + Debug.Assert(name != null); Native.Z3_params_set_uint(Context.nCtx, NativeObject, name.NativeObject, value); return this; @@ -55,7 +54,7 @@ namespace Microsoft.Z3 /// public Params Add(Symbol name, double value) { - Contract.Requires(name != null); + Debug.Assert(name != null); Native.Z3_params_set_double(Context.nCtx, NativeObject, name.NativeObject, value); return this; @@ -66,7 +65,7 @@ namespace Microsoft.Z3 /// public Params Add(Symbol name, string value) { - Contract.Requires(value != null); + Debug.Assert(value != null); Native.Z3_params_set_symbol(Context.nCtx, NativeObject, name.NativeObject, Context.MkSymbol(value).NativeObject); return this; @@ -77,8 +76,8 @@ namespace Microsoft.Z3 /// public Params Add(Symbol name, Symbol value) { - Contract.Requires(name != null); - Contract.Requires(value != null); + Debug.Assert(name != null); + Debug.Assert(value != null); Native.Z3_params_set_symbol(Context.nCtx, NativeObject, name.NativeObject, value.NativeObject); return this; @@ -117,7 +116,7 @@ namespace Microsoft.Z3 /// public Params Add(string name, Symbol value) { - Contract.Requires(value != null); + Debug.Assert(value != null); Native.Z3_params_set_symbol(Context.nCtx, NativeObject, Context.MkSymbol(name).NativeObject, value.NativeObject); return this; @@ -128,8 +127,8 @@ namespace Microsoft.Z3 /// public Params Add(string name, string value) { - Contract.Requires(name != null); - Contract.Requires(value != null); + Debug.Assert(name != null); + Debug.Assert(value != null); Native.Z3_params_set_symbol(Context.nCtx, NativeObject, Context.MkSymbol(name).NativeObject, Context.MkSymbol(value).NativeObject); return this; @@ -147,7 +146,7 @@ namespace Microsoft.Z3 internal Params(Context ctx) : base(ctx, Native.Z3_mk_params(ctx.nCtx)) { - Contract.Requires(ctx != null); + Debug.Assert(ctx != null); } internal class DecRefQueue : IDecRefQueue diff --git a/src/api/dotnet/Pattern.cs b/src/api/dotnet/Pattern.cs index 1ea7bdb38..c33a38a1d 100644 --- a/src/api/dotnet/Pattern.cs +++ b/src/api/dotnet/Pattern.cs @@ -17,9 +17,9 @@ Notes: --*/ +using System.Diagnostics; using System; using System.Runtime.InteropServices; -using System.Diagnostics.Contracts; namespace Microsoft.Z3 { @@ -28,7 +28,6 @@ namespace Microsoft.Z3 /// non-empty. If the list comprises of more than one term, it is /// also called a multi-pattern. /// - [ContractVerification(true)] public class Pattern : AST { /// @@ -46,7 +45,6 @@ namespace Microsoft.Z3 { get { - Contract.Ensures(Contract.Result() != null); uint n = NumTerms; Expr[] res = new Expr[n]; @@ -68,7 +66,7 @@ namespace Microsoft.Z3 internal Pattern(Context ctx, IntPtr obj) : base(ctx, obj) { - Contract.Requires(ctx != null); + Debug.Assert(ctx != null); } #endregion } diff --git a/src/api/dotnet/Probe.cs b/src/api/dotnet/Probe.cs index 3c5e5adc9..5cdee79a2 100644 --- a/src/api/dotnet/Probe.cs +++ b/src/api/dotnet/Probe.cs @@ -17,9 +17,9 @@ Notes: --*/ +using System.Diagnostics; using System; using System.Runtime.InteropServices; -using System.Diagnostics.Contracts; namespace Microsoft.Z3 { @@ -30,7 +30,6 @@ namespace Microsoft.Z3 /// and Context.ProbeNames. /// It may also be obtained using the command (help-tactic) in the SMT 2.0 front-end. /// - [ContractVerification(true)] public class Probe : Z3Object { /// @@ -40,7 +39,7 @@ namespace Microsoft.Z3 /// "Boolean" probes return 0.0 for false, and a value different from 0.0 for true. public double Apply(Goal g) { - Contract.Requires(g != null); + Debug.Assert(g != null); Context.CheckContextMatch(g); return Native.Z3_probe_apply(Context.nCtx, NativeObject, g.NativeObject); @@ -53,7 +52,7 @@ namespace Microsoft.Z3 { get { - Contract.Requires(g != null); + Debug.Assert(g != null); return Apply(g); } @@ -63,12 +62,12 @@ namespace Microsoft.Z3 internal Probe(Context ctx, IntPtr obj) : base(ctx, obj) { - Contract.Requires(ctx != null); + Debug.Assert(ctx != null); } internal Probe(Context ctx, string name) : base(ctx, Native.Z3_mk_probe(ctx.nCtx, name)) { - Contract.Requires(ctx != null); + Debug.Assert(ctx != null); } internal class DecRefQueue : IDecRefQueue diff --git a/src/api/dotnet/Quantifier.cs b/src/api/dotnet/Quantifier.cs index d13ca4003..f4a889092 100644 --- a/src/api/dotnet/Quantifier.cs +++ b/src/api/dotnet/Quantifier.cs @@ -18,14 +18,14 @@ Notes: --*/ using System; -using System.Diagnostics.Contracts; +using System.Diagnostics; +using System.Linq; namespace Microsoft.Z3 { /// /// Quantifier expressions. /// - [ContractVerification(true)] public class Quantifier : BoolExpr { /// @@ -67,7 +67,6 @@ namespace Microsoft.Z3 { get { - Contract.Ensures(Contract.Result() != null); uint n = NumPatterns; Pattern[] res = new Pattern[n]; @@ -92,7 +91,6 @@ namespace Microsoft.Z3 { get { - Contract.Ensures(Contract.Result() != null); uint n = NumNoPatterns; Pattern[] res = new Pattern[n]; @@ -117,7 +115,6 @@ namespace Microsoft.Z3 { get { - Contract.Ensures(Contract.Result() != null); uint n = NumBound; Symbol[] res = new Symbol[n]; @@ -134,7 +131,6 @@ namespace Microsoft.Z3 { get { - Contract.Ensures(Contract.Result() != null); uint n = NumBound; Sort[] res = new Sort[n]; @@ -151,7 +147,6 @@ namespace Microsoft.Z3 { get { - Contract.Ensures(Contract.Result() != null); return new BoolExpr(Context, Native.Z3_get_quantifier_body(Context.nCtx, NativeObject)); } @@ -168,19 +163,18 @@ namespace Microsoft.Z3 } #region Internal - [ContractVerification(false)] // F: Clousot ForAll decompilation gets confused below. Setting verification off until I fixed the bug internal Quantifier(Context ctx, bool isForall, Sort[] sorts, Symbol[] names, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null) : base(ctx, IntPtr.Zero) { - Contract.Requires(ctx != null); - Contract.Requires(sorts != null); - Contract.Requires(names != null); - Contract.Requires(body != null); - Contract.Requires(sorts.Length == names.Length); - Contract.Requires(Contract.ForAll(sorts, s => s != null)); - Contract.Requires(Contract.ForAll(names, n => n != null)); - Contract.Requires(patterns == null || Contract.ForAll(patterns, p => p != null)); - Contract.Requires(noPatterns == null || Contract.ForAll(noPatterns, np => np != null)); + Debug.Assert(ctx != null); + Debug.Assert(sorts != null); + Debug.Assert(names != null); + Debug.Assert(body != null); + Debug.Assert(sorts.Length == names.Length); + Debug.Assert(sorts.All(s => s != null)); + Debug.Assert(names.All(n => n != null)); + Debug.Assert(patterns == null || patterns.All(p => p != null)); + Debug.Assert(noPatterns == null || noPatterns.All(np => np != null)); Context.CheckContextMatch(patterns); Context.CheckContextMatch(noPatterns); @@ -211,16 +205,15 @@ namespace Microsoft.Z3 } } - [ContractVerification(false)] // F: Clousot ForAll decompilation gets confused below. Setting verification off until I fixed the bug internal Quantifier(Context ctx, bool isForall, Expr[] bound, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null) : base(ctx, IntPtr.Zero) { - Contract.Requires(ctx != null); - Contract.Requires(body != null); + Debug.Assert(ctx != null); + Debug.Assert(body != null); - Contract.Requires(patterns == null || Contract.ForAll(patterns, p => p != null)); - Contract.Requires(noPatterns == null || Contract.ForAll(noPatterns, np => np != null)); - Contract.Requires(bound == null || Contract.ForAll(bound, n => n != null)); + Debug.Assert(patterns == null || patterns.All(p => p != null)); + Debug.Assert(noPatterns == null || noPatterns.All(np => np != null)); + Debug.Assert(bound == null || bound.All(n => n != null)); Context.CheckContextMatch(noPatterns); Context.CheckContextMatch(patterns); @@ -246,7 +239,7 @@ namespace Microsoft.Z3 } - internal Quantifier(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); } + internal Quantifier(Context ctx, IntPtr obj) : base(ctx, obj) { Debug.Assert(ctx != null); } #if DEBUG internal override void CheckNativeObject(IntPtr obj) diff --git a/src/api/dotnet/RatNum.cs b/src/api/dotnet/RatNum.cs index ef5f1a867..1d485a347 100644 --- a/src/api/dotnet/RatNum.cs +++ b/src/api/dotnet/RatNum.cs @@ -16,8 +16,8 @@ Author: Notes: --*/ +using System.Diagnostics; using System; -using System.Diagnostics.Contracts; #if !FRAMEWORK_LT_4 using System.Numerics; @@ -28,7 +28,6 @@ namespace Microsoft.Z3 /// /// Rational Numerals /// - [ContractVerification(true)] public class RatNum : RealExpr { /// @@ -38,7 +37,6 @@ namespace Microsoft.Z3 { get { - Contract.Ensures(Contract.Result() != null); return new IntNum(Context, Native.Z3_get_numerator(Context.nCtx, NativeObject)); } @@ -51,7 +49,6 @@ namespace Microsoft.Z3 { get { - Contract.Ensures(Contract.Result() != null); return new IntNum(Context, Native.Z3_get_denominator(Context.nCtx, NativeObject)); } @@ -112,7 +109,7 @@ namespace Microsoft.Z3 internal RatNum(Context ctx, IntPtr obj) : base(ctx, obj) { - Contract.Requires(ctx != null); + Debug.Assert(ctx != null); } #endregion } diff --git a/src/api/dotnet/ReExpr.cs b/src/api/dotnet/ReExpr.cs index 6a10d535f..7ab9aaffc 100644 --- a/src/api/dotnet/ReExpr.cs +++ b/src/api/dotnet/ReExpr.cs @@ -16,12 +16,12 @@ Author: Notes: --*/ +using System.Diagnostics; using System; using System.Collections.Generic; using System.Linq; using System.Text; -using System.Diagnostics.Contracts; namespace Microsoft.Z3 { @@ -35,7 +35,7 @@ namespace Microsoft.Z3 internal ReExpr(Context ctx, IntPtr obj) : base(ctx, obj) { - Contract.Requires(ctx != null); + Debug.Assert(ctx != null); } #endregion } diff --git a/src/api/dotnet/ReSort.cs b/src/api/dotnet/ReSort.cs index bc420603d..98659c697 100644 --- a/src/api/dotnet/ReSort.cs +++ b/src/api/dotnet/ReSort.cs @@ -17,8 +17,8 @@ Notes: --*/ +using System.Diagnostics; using System; -using System.Diagnostics.Contracts; namespace Microsoft.Z3 { @@ -31,12 +31,12 @@ namespace Microsoft.Z3 internal ReSort(Context ctx, IntPtr obj) : base(ctx, obj) { - Contract.Requires(ctx != null); + Debug.Assert(ctx != null); } internal ReSort(Context ctx) : base(ctx, Native.Z3_mk_int_sort(ctx.nCtx)) { - Contract.Requires(ctx != null); + Debug.Assert(ctx != null); } #endregion } diff --git a/src/api/dotnet/RealExpr.cs b/src/api/dotnet/RealExpr.cs index 8ee8c8e76..1c3a55189 100644 --- a/src/api/dotnet/RealExpr.cs +++ b/src/api/dotnet/RealExpr.cs @@ -16,12 +16,12 @@ Author: Notes: --*/ +using System.Diagnostics; using System; using System.Collections.Generic; using System.Linq; using System.Text; -using System.Diagnostics.Contracts; namespace Microsoft.Z3 { @@ -35,7 +35,7 @@ namespace Microsoft.Z3 internal RealExpr(Context ctx, IntPtr obj) : base(ctx, obj) { - Contract.Requires(ctx != null); + Debug.Assert(ctx != null); } #endregion } diff --git a/src/api/dotnet/RealSort.cs b/src/api/dotnet/RealSort.cs index 97f1cae11..38fe469ce 100644 --- a/src/api/dotnet/RealSort.cs +++ b/src/api/dotnet/RealSort.cs @@ -17,8 +17,8 @@ Notes: --*/ +using System.Diagnostics; using System; -using System.Diagnostics.Contracts; namespace Microsoft.Z3 { @@ -31,12 +31,12 @@ namespace Microsoft.Z3 internal RealSort(Context ctx, IntPtr obj) : base(ctx, obj) { - Contract.Requires(ctx != null); + Debug.Assert(ctx != null); } internal RealSort(Context ctx) : base(ctx, Native.Z3_mk_real_sort(ctx.nCtx)) { - Contract.Requires(ctx != null); + Debug.Assert(ctx != null); } #endregion } diff --git a/src/api/dotnet/RelationSort.cs b/src/api/dotnet/RelationSort.cs index cfd7a592a..6bea5c6e1 100644 --- a/src/api/dotnet/RelationSort.cs +++ b/src/api/dotnet/RelationSort.cs @@ -17,15 +17,14 @@ Notes: --*/ +using System.Diagnostics; using System; -using System.Diagnostics.Contracts; namespace Microsoft.Z3 { /// /// Relation sorts. /// - [ContractVerification(true)] public class RelationSort : Sort { /// @@ -43,7 +42,6 @@ namespace Microsoft.Z3 { get { - Contract.Ensures(Contract.Result() != null); if (m_columnSorts != null) return m_columnSorts; @@ -62,7 +60,7 @@ namespace Microsoft.Z3 internal RelationSort(Context ctx, IntPtr obj) : base(ctx, obj) { - Contract.Requires(ctx != null); + Debug.Assert(ctx != null); } #endregion } diff --git a/src/api/dotnet/SeqExpr.cs b/src/api/dotnet/SeqExpr.cs index c9fdd03a8..bfab1fa36 100644 --- a/src/api/dotnet/SeqExpr.cs +++ b/src/api/dotnet/SeqExpr.cs @@ -16,12 +16,12 @@ Author: Notes: --*/ +using System.Diagnostics; using System; using System.Collections.Generic; using System.Linq; using System.Text; -using System.Diagnostics.Contracts; namespace Microsoft.Z3 { @@ -35,7 +35,7 @@ namespace Microsoft.Z3 internal SeqExpr(Context ctx, IntPtr obj) : base(ctx, obj) { - Contract.Requires(ctx != null); + Debug.Assert(ctx != null); } #endregion } diff --git a/src/api/dotnet/SeqSort.cs b/src/api/dotnet/SeqSort.cs index b2be11291..2902b1e9e 100644 --- a/src/api/dotnet/SeqSort.cs +++ b/src/api/dotnet/SeqSort.cs @@ -17,8 +17,8 @@ Notes: --*/ +using System.Diagnostics; using System; -using System.Diagnostics.Contracts; namespace Microsoft.Z3 { @@ -31,12 +31,12 @@ namespace Microsoft.Z3 internal SeqSort(Context ctx, IntPtr obj) : base(ctx, obj) { - Contract.Requires(ctx != null); + Debug.Assert(ctx != null); } internal SeqSort(Context ctx) : base(ctx, Native.Z3_mk_int_sort(ctx.nCtx)) { - Contract.Requires(ctx != null); + Debug.Assert(ctx != null); } #endregion } diff --git a/src/api/dotnet/SetSort.cs b/src/api/dotnet/SetSort.cs index bdba3899f..9f55c8edb 100644 --- a/src/api/dotnet/SetSort.cs +++ b/src/api/dotnet/SetSort.cs @@ -17,28 +17,27 @@ Notes: --*/ +using System.Diagnostics; using System; -using System.Diagnostics.Contracts; namespace Microsoft.Z3 { /// /// Set sorts. /// - [ContractVerification(true)] public class SetSort : Sort { #region Internal internal SetSort(Context ctx, IntPtr obj) : base(ctx, obj) { - Contract.Requires(ctx != null); + Debug.Assert(ctx != null); } internal SetSort(Context ctx, Sort ty) : base(ctx, Native.Z3_mk_set_sort(ctx.nCtx, ty.NativeObject)) { - Contract.Requires(ctx != null); - Contract.Requires(ty != null); + Debug.Assert(ctx != null); + Debug.Assert(ty != null); } #endregion } diff --git a/src/api/dotnet/Solver.cs b/src/api/dotnet/Solver.cs index a288990a2..ec53b14de 100644 --- a/src/api/dotnet/Solver.cs +++ b/src/api/dotnet/Solver.cs @@ -18,16 +18,15 @@ Notes: --*/ using System; +using System.Diagnostics; using System.Linq; using System.Collections.Generic; -using System.Diagnostics.Contracts; namespace Microsoft.Z3 { /// /// Solvers. /// - [ContractVerification(true)] public class Solver : Z3Object { /// @@ -37,7 +36,6 @@ namespace Microsoft.Z3 { get { - Contract.Ensures(Contract.Result() != null); return Native.Z3_solver_get_help(Context.nCtx, NativeObject); } @@ -50,7 +48,7 @@ namespace Microsoft.Z3 { set { - Contract.Requires(value != null); + Debug.Assert(value != null); Context.CheckContextMatch(value); Native.Z3_solver_set_params(Context.nCtx, NativeObject, value.NativeObject); @@ -152,8 +150,8 @@ namespace Microsoft.Z3 /// public void Assert(params BoolExpr[] constraints) { - Contract.Requires(constraints != null); - Contract.Requires(Contract.ForAll(constraints, c => c != null)); + Debug.Assert(constraints != null); + Debug.Assert(constraints.All(c => c != null)); Context.CheckContextMatch(constraints); foreach (BoolExpr a in constraints) @@ -191,9 +189,9 @@ namespace Microsoft.Z3 /// public void AssertAndTrack(BoolExpr[] constraints, BoolExpr[] ps) { - Contract.Requires(constraints != null); - Contract.Requires(Contract.ForAll(constraints, c => c != null)); - Contract.Requires(Contract.ForAll(ps, c => c != null)); + Debug.Assert(constraints != null); + Debug.Assert(constraints.All(c => c != null)); + Debug.Assert(ps.All(c => c != null)); Context.CheckContextMatch(constraints); Context.CheckContextMatch(ps); if (constraints.Length != ps.Length) @@ -216,8 +214,8 @@ namespace Microsoft.Z3 /// public void AssertAndTrack(BoolExpr constraint, BoolExpr p) { - Contract.Requires(constraint != null); - Contract.Requires(p != null); + Debug.Assert(constraint != null); + Debug.Assert(p != null); Context.CheckContextMatch(constraint); Context.CheckContextMatch(p); @@ -259,7 +257,6 @@ namespace Microsoft.Z3 { get { - Contract.Ensures(Contract.Result() != null); ASTVector assertions = new ASTVector(Context, Native.Z3_solver_get_assertions(Context.nCtx, NativeObject)); return assertions.ToBoolExprArray(); @@ -273,7 +270,6 @@ namespace Microsoft.Z3 { get { - Contract.Ensures(Contract.Result() != null); ASTVector assertions = new ASTVector(Context, Native.Z3_solver_get_units(Context.nCtx, NativeObject)); return assertions.ToBoolExprArray(); @@ -394,7 +390,6 @@ namespace Microsoft.Z3 { get { - Contract.Ensures(Contract.Result() != null); ASTVector core = new ASTVector(Context, Native.Z3_solver_get_unsat_core(Context.nCtx, NativeObject)); return core.ToBoolExprArray(); @@ -408,7 +403,6 @@ namespace Microsoft.Z3 { get { - Contract.Ensures(Contract.Result() != null); return Native.Z3_solver_get_reason_unknown(Context.nCtx, NativeObject); } @@ -455,8 +449,7 @@ namespace Microsoft.Z3 /// public Solver Translate(Context ctx) { - Contract.Requires(ctx != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(ctx != null); return new Solver(ctx, Native.Z3_solver_translate(Context.nCtx, NativeObject, ctx.nCtx)); } @@ -475,7 +468,6 @@ namespace Microsoft.Z3 { get { - Contract.Ensures(Contract.Result() != null); return new Statistics(Context, Native.Z3_solver_get_statistics(Context.nCtx, NativeObject)); } @@ -493,7 +485,7 @@ namespace Microsoft.Z3 internal Solver(Context ctx, IntPtr obj) : base(ctx, obj) { - Contract.Requires(ctx != null); + Debug.Assert(ctx != null); this.BacktrackLevel = uint.MaxValue; } diff --git a/src/api/dotnet/Sort.cs b/src/api/dotnet/Sort.cs index e32fd1eb3..cf70bbf73 100644 --- a/src/api/dotnet/Sort.cs +++ b/src/api/dotnet/Sort.cs @@ -17,15 +17,14 @@ Notes: --*/ +using System.Diagnostics; using System; -using System.Diagnostics.Contracts; namespace Microsoft.Z3 { /// /// The Sort class implements type information for ASTs. /// - [ContractVerification(true)] public class Sort : AST { /// @@ -100,7 +99,6 @@ namespace Microsoft.Z3 { get { - Contract.Ensures(Contract.Result() != null); return Symbol.Create(Context, Native.Z3_get_sort_name(Context.nCtx, NativeObject)); } } @@ -127,7 +125,7 @@ namespace Microsoft.Z3 /// /// Sort constructor /// - internal Sort(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); } + internal Sort(Context ctx, IntPtr obj) : base(ctx, obj) { Debug.Assert(ctx != null); } #if DEBUG internal override void CheckNativeObject(IntPtr obj) @@ -138,11 +136,9 @@ namespace Microsoft.Z3 } #endif - [ContractVerification(true)] new internal static Sort Create(Context ctx, IntPtr obj) { - Contract.Requires(ctx != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(ctx != null); switch ((Z3_sort_kind)Native.Z3_get_sort_kind(ctx.nCtx, obj)) { diff --git a/src/api/dotnet/Statistics.cs b/src/api/dotnet/Statistics.cs index c94af625c..8b664913a 100644 --- a/src/api/dotnet/Statistics.cs +++ b/src/api/dotnet/Statistics.cs @@ -18,14 +18,14 @@ Notes: --*/ using System; -using System.Diagnostics.Contracts; +using System.Diagnostics; + namespace Microsoft.Z3 { /// /// Objects of this class track statistical information about solvers. /// - [ContractVerification(true)] public class Statistics : Z3Object { /// @@ -62,7 +62,6 @@ namespace Microsoft.Z3 { get { - Contract.Ensures(Contract.Result() != null); if (IsUInt) return m_uint.ToString(); @@ -124,9 +123,6 @@ namespace Microsoft.Z3 { get { - Contract.Ensures(Contract.Result() != null); - Contract.Ensures(Contract.Result().Length == this.Size); - Contract.Ensures(Contract.ForAll(0, Contract.Result().Length, j => Contract.Result()[j] != null)); uint n = Size; Entry[] res = new Entry[n]; @@ -153,7 +149,6 @@ namespace Microsoft.Z3 { get { - Contract.Ensures(Contract.Result() != null); uint n = Size; string[] res = new string[n]; @@ -184,7 +179,7 @@ namespace Microsoft.Z3 internal Statistics(Context ctx, IntPtr obj) : base(ctx, obj) { - Contract.Requires(ctx != null); + Debug.Assert(ctx != null); } internal class DecRefQueue : IDecRefQueue diff --git a/src/api/dotnet/Status.cs b/src/api/dotnet/Status.cs index 5847f098b..d44cffd56 100644 --- a/src/api/dotnet/Status.cs +++ b/src/api/dotnet/Status.cs @@ -17,6 +17,7 @@ Notes: --*/ +using System.Diagnostics; using System; namespace Microsoft.Z3 diff --git a/src/api/dotnet/StringSymbol.cs b/src/api/dotnet/StringSymbol.cs index e311fb958..447e0be5f 100644 --- a/src/api/dotnet/StringSymbol.cs +++ b/src/api/dotnet/StringSymbol.cs @@ -18,8 +18,8 @@ Notes: --*/ using System; +using System.Diagnostics; using System.Runtime.InteropServices; -using System.Diagnostics.Contracts; namespace Microsoft.Z3 { @@ -27,7 +27,6 @@ namespace Microsoft.Z3 /// /// Named symbols /// - [ContractVerification(true)] public class StringSymbol : Symbol { /// @@ -38,7 +37,6 @@ namespace Microsoft.Z3 { get { - Contract.Ensures(Contract.Result() != null); if (!IsStringSymbol()) throw new Z3Exception("String requested from non-String symbol"); @@ -50,13 +48,13 @@ namespace Microsoft.Z3 internal StringSymbol(Context ctx, IntPtr obj) : base(ctx, obj) { - Contract.Requires(ctx != null); + Debug.Assert(ctx != null); } internal StringSymbol(Context ctx, string s) : base(ctx, Native.Z3_mk_string_symbol(ctx.nCtx, s)) { - Contract.Requires(ctx != null); + Debug.Assert(ctx != null); } #if DEBUG diff --git a/src/api/dotnet/Symbol.cs b/src/api/dotnet/Symbol.cs index 2a1fdf6c5..7df0986fe 100644 --- a/src/api/dotnet/Symbol.cs +++ b/src/api/dotnet/Symbol.cs @@ -18,15 +18,14 @@ Notes: --*/ using System; +using System.Diagnostics; using System.Runtime.InteropServices; -using System.Diagnostics.Contracts; namespace Microsoft.Z3 { /// /// Symbols are used to name several term and type constructors. /// - [ContractVerification(true)] public class Symbol : Z3Object { /// @@ -113,13 +112,12 @@ namespace Microsoft.Z3 /// internal protected Symbol(Context ctx, IntPtr obj) : base(ctx, obj) { - Contract.Requires(ctx != null); + Debug.Assert(ctx != null); } internal static Symbol Create(Context ctx, IntPtr obj) { - Contract.Requires(ctx != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(ctx != null); switch ((Z3_symbol_kind)Native.Z3_get_symbol_kind(ctx.nCtx, obj)) { diff --git a/src/api/dotnet/Tactic.cs b/src/api/dotnet/Tactic.cs index 0a6f79494..96b6da170 100644 --- a/src/api/dotnet/Tactic.cs +++ b/src/api/dotnet/Tactic.cs @@ -18,7 +18,7 @@ Notes: --*/ using System; -using System.Diagnostics.Contracts; +using System.Diagnostics; namespace Microsoft.Z3 { @@ -28,7 +28,6 @@ namespace Microsoft.Z3 /// and Context.TacticNames. /// It may also be obtained using the command (help-tactic) in the SMT 2.0 front-end. /// - [ContractVerification(true)] public class Tactic : Z3Object { /// @@ -38,7 +37,6 @@ namespace Microsoft.Z3 { get { - Contract.Ensures(Contract.Result() != null); return Native.Z3_tactic_get_help(Context.nCtx, NativeObject); } @@ -59,8 +57,7 @@ namespace Microsoft.Z3 /// public ApplyResult Apply(Goal g, Params p = null) { - Contract.Requires(g != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(g != null); Context.CheckContextMatch(g); if (p == null) @@ -79,8 +76,7 @@ namespace Microsoft.Z3 { get { - Contract.Requires(g != null); - Contract.Ensures(Contract.Result() != null); + Debug.Assert(g != null); return Apply(g); } @@ -94,7 +90,6 @@ namespace Microsoft.Z3 { get { - Contract.Ensures(Contract.Result() != null); return Context.MkSolver(this); } @@ -104,12 +99,12 @@ namespace Microsoft.Z3 internal Tactic(Context ctx, IntPtr obj) : base(ctx, obj) { - Contract.Requires(ctx != null); + Debug.Assert(ctx != null); } internal Tactic(Context ctx, string name) : base(ctx, Native.Z3_mk_tactic(ctx.nCtx, name)) { - Contract.Requires(ctx != null); + Debug.Assert(ctx != null); } /// diff --git a/src/api/dotnet/TupleSort.cs b/src/api/dotnet/TupleSort.cs index ea99f3855..adbc4f904 100644 --- a/src/api/dotnet/TupleSort.cs +++ b/src/api/dotnet/TupleSort.cs @@ -18,14 +18,13 @@ Notes: --*/ using System; -using System.Diagnostics.Contracts; +using System.Diagnostics; namespace Microsoft.Z3 { /// /// Tuple sorts. /// - [ContractVerification(true)] public class TupleSort : Sort { /// @@ -35,7 +34,6 @@ namespace Microsoft.Z3 { get { - Contract.Ensures(Contract.Result() != null); return new FuncDecl(Context, Native.Z3_get_tuple_sort_mk_decl(Context.nCtx, NativeObject)); } @@ -56,7 +54,6 @@ namespace Microsoft.Z3 { get { - Contract.Ensures(Contract.Result() != null); uint n = NumFields; FuncDecl[] res = new FuncDecl[n]; @@ -70,8 +67,8 @@ namespace Microsoft.Z3 internal TupleSort(Context ctx, Symbol name, uint numFields, Symbol[] fieldNames, Sort[] fieldSorts) : base(ctx, IntPtr.Zero) { - Contract.Requires(ctx != null); - Contract.Requires(name != null); + Debug.Assert(ctx != null); + Debug.Assert(name != null); IntPtr t = IntPtr.Zero; IntPtr[] f = new IntPtr[numFields]; diff --git a/src/api/dotnet/UninterpretedSort.cs b/src/api/dotnet/UninterpretedSort.cs index 154818faf..9f940468d 100644 --- a/src/api/dotnet/UninterpretedSort.cs +++ b/src/api/dotnet/UninterpretedSort.cs @@ -18,7 +18,7 @@ Notes: --*/ using System; -using System.Diagnostics.Contracts; +using System.Diagnostics; namespace Microsoft.Z3 { @@ -31,13 +31,13 @@ namespace Microsoft.Z3 internal UninterpretedSort(Context ctx, IntPtr obj) : base(ctx, obj) { - Contract.Requires(ctx != null); + Debug.Assert(ctx != null); } internal UninterpretedSort(Context ctx, Symbol s) : base(ctx, Native.Z3_mk_uninterpreted_sort(ctx.nCtx, s.NativeObject)) { - Contract.Requires(ctx != null); - Contract.Requires(s != null); + Debug.Assert(ctx != null); + Debug.Assert(s != null); } #endregion } diff --git a/src/api/dotnet/Version.cs b/src/api/dotnet/Version.cs index 364ada781..2099959eb 100644 --- a/src/api/dotnet/Version.cs +++ b/src/api/dotnet/Version.cs @@ -17,8 +17,8 @@ Notes: --*/ +using System.Diagnostics; using System; -using System.Diagnostics.Contracts; namespace Microsoft.Z3 { @@ -26,7 +26,6 @@ namespace Microsoft.Z3 /// Version information. /// /// Note that this class is static. - [ContractVerification(true)] public static class Version { static Version() { } @@ -99,7 +98,6 @@ namespace Microsoft.Z3 /// new public static string ToString() { - Contract.Ensures(Contract.Result() != null); uint major = 0, minor = 0, build = 0, revision = 0; Native.Z3_get_version(ref major, ref minor, ref build, ref revision); diff --git a/src/api/dotnet/Z3Exception.cs b/src/api/dotnet/Z3Exception.cs index b0e05900c..79f6185da 100644 --- a/src/api/dotnet/Z3Exception.cs +++ b/src/api/dotnet/Z3Exception.cs @@ -17,6 +17,7 @@ Notes: --*/ +using System.Diagnostics; using System; namespace Microsoft.Z3 diff --git a/src/api/dotnet/Z3Object.cs b/src/api/dotnet/Z3Object.cs index f32ba30af..9a61a0119 100644 --- a/src/api/dotnet/Z3Object.cs +++ b/src/api/dotnet/Z3Object.cs @@ -17,8 +17,8 @@ Notes: --*/ +using System.Diagnostics; using System; -using System.Diagnostics.Contracts; using System.Threading; using System.Collections.Generic; using System.Linq; @@ -29,7 +29,6 @@ namespace Microsoft.Z3 /// Internal base class for interfacing with native Z3 objects. /// Should not be used externally. /// - [ContractVerification(true)] public class Z3Object : IDisposable { /// @@ -63,10 +62,9 @@ namespace Microsoft.Z3 #region Object Invariant - [ContractInvariantMethod] private void ObjectInvariant() { - Contract.Invariant(this.m_ctx != null); + Debug.Assert(this.m_ctx != null); } #endregion @@ -77,7 +75,7 @@ namespace Microsoft.Z3 internal Z3Object(Context ctx) { - Contract.Requires(ctx != null); + Debug.Assert(ctx != null); Interlocked.Increment(ref ctx.refCount); m_ctx = ctx; @@ -85,7 +83,7 @@ namespace Microsoft.Z3 internal Z3Object(Context ctx, IntPtr obj) { - Contract.Requires(ctx != null); + Debug.Assert(ctx != null); Interlocked.Increment(ref ctx.refCount); m_ctx = ctx; @@ -119,16 +117,12 @@ namespace Microsoft.Z3 { get { - Contract.Ensures(Contract.Result() != null); return m_ctx; } } - [Pure] internal static IntPtr[] ArrayToNative(Z3Object[] a) { - Contract.Ensures(a == null || Contract.Result() != null); - Contract.Ensures(a == null || Contract.Result().Length == a.Length); if (a == null) return null; IntPtr[] an = new IntPtr[a.Length]; @@ -137,11 +131,8 @@ namespace Microsoft.Z3 return an; } - [Pure] internal static IntPtr[] EnumToNative(IEnumerable a) where T : Z3Object { - Contract.Ensures(a == null || Contract.Result() != null); - Contract.Ensures(a == null || Contract.Result().Length == a.Count()); if (a == null) return null; IntPtr[] an = new IntPtr[a.Count()]; @@ -154,7 +145,6 @@ namespace Microsoft.Z3 return an; } - [Pure] internal static uint ArrayLength(Z3Object[] a) { return (a == null)?0:(uint)a.Length;