mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

remove dependencies on contracts

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-10-20 10:24:36 -07:00
parent 12fc670839
commit 3d37060fa9
72 changed files with 734 additions and 1232 deletions
Download patch file Download diff file Expand all files Collapse all files

14
src/api/dotnet/AST.cs
View file

@ -17,17 +17,16 @@ Notes:
--*/
using System.Diagnostics;
using System;
using System.Collections;
using System.Collections.Generic;
using System.Diagnostics.Contracts;
namespace Microsoft.Z3
{
/// <summary>
/// The abstract syntax tree (AST) class.
/// </summary>
[ContractVerification(true)]
public class AST : Z3Object, IComparable
{
/// <summary>
@ -114,8 +113,7 @@ namespace Microsoft.Z3
/// <returns>A copy of the AST which is associated with <paramref name="ctx"/></returns>
public AST Translate(Context ctx)
{
Contract.Requires(ctx != null);
Contract.Ensures(Contract.Result<AST>() != null);
Debug.Assert(ctx != null);
if (ReferenceEquals(Context, ctx))
return this;
@ -202,14 +200,13 @@ namespace Microsoft.Z3
/// </summary>
public string SExpr()
{
Contract.Ensures(Contract.Result<string>() != 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<AST>() != null);
Debug.Assert(ctx != null);
switch ((Z3_ast_kind)Native.Z3_get_ast_kind(ctx.nCtx, obj))
{

18
src/api/dotnet/ASTMap.cs
View file

@ -17,15 +17,14 @@ Notes:
--*/
using System.Diagnostics;
using System;
using System.Diagnostics.Contracts;
namespace Microsoft.Z3
{
/// <summary>
/// Map from AST to AST
/// </summary>
[ContractVerification(true)]
internal class ASTMap : Z3Object
{
/// <summary>
@ -35,7 +34,7 @@ namespace Microsoft.Z3
/// <returns>True if <paramref name="k"/> is a key in the map, false otherwise.</returns>
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
/// <param name="k">An AST</param>
public AST Find(AST k)
{
Contract.Requires(k != null);
Contract.Ensures(Contract.Result<AST>() != 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
/// <param name="v">The value AST</param>
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
/// <param name="k">An AST</param>
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

14
src/api/dotnet/ASTVector.cs
View file

@ -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<AST>() != 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
/// <param name="a">An AST</param>
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
/// <returns>A new ASTVector</returns>
public ASTVector Translate(Context ctx)
{
Contract.Requires(ctx != null);
Contract.Ensures(Contract.Result<ASTVector>() != 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
{

8
src/api/dotnet/AlgebraicNum.cs
View file

@ -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
/// <summary>
/// Algebraic numbers
/// </summary>
[ContractVerification(true)]
public class AlgebraicNum : ArithExpr
{
/// <summary>
@ -40,7 +39,6 @@ namespace Microsoft.Z3
/// <returns>A numeral Expr of sort Real</returns>
public RatNum ToUpper(uint precision)
{
Contract.Ensures(Contract.Result<RatNum>() != null);
return new RatNum(Context, Native.Z3_get_algebraic_number_upper(Context.nCtx, NativeObject, precision));
}
@ -54,7 +52,6 @@ namespace Microsoft.Z3
/// <returns>A numeral Expr of sort Real</returns>
public RatNum ToLower(uint precision)
{
Contract.Ensures(Contract.Result<RatNum>() != null);
return new RatNum(Context, Native.Z3_get_algebraic_number_lower(Context.nCtx, NativeObject, precision));
}
@ -65,7 +62,6 @@ namespace Microsoft.Z3
/// <remarks>The result has at most <paramref name="precision"/> decimal places.</remarks>
public string ToDecimal(uint precision)
{
Contract.Ensures(Contract.Result<string>() != 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
}

7
src/api/dotnet/ApplyResult.cs
View file

@ -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.
/// </summary>
[ContractVerification(true)]
public class ApplyResult : Z3Object
{
/// <summary>
@ -44,8 +43,6 @@ namespace Microsoft.Z3
{
get
{
Contract.Ensures(Contract.Result<Goal[]>() != null);
Contract.Ensures(Contract.Result<Goal[]>().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

4
src/api/dotnet/ArithExpr.cs
View file

@ -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

4
src/api/dotnet/ArithSort.cs
View file

@ -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
};
}

4
src/api/dotnet/ArrayExpr.cs
View file

@ -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
}

19
src/api/dotnet/ArraySort.cs
View file

@ -17,15 +17,14 @@ Notes:
--*/
using System.Diagnostics;
using System;
using System.Diagnostics.Contracts;
namespace Microsoft.Z3
{
/// <summary>
/// Array sorts.
/// </summary>
[ContractVerification(true)]
public class ArraySort : Sort
{
/// <summary>
@ -35,7 +34,6 @@ namespace Microsoft.Z3
{
get
{
Contract.Ensures(Contract.Result<Sort>() != 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<Sort>() != 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
};

4
src/api/dotnet/BitVecExpr.cs
View file

@ -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
/// <summary> Constructor for BitVecExpr </summary>
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
}
}

5
src/api/dotnet/BitVecNum.cs
View file

@ -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
/// <summary>
/// Bit-vector numerals
/// </summary>
[ContractVerification(true)]
public class BitVecNum : BitVecExpr
{
/// <summary>
@ -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
}
}

4
src/api/dotnet/BitVecSort.cs
View file

@ -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
};
}

4
src/api/dotnet/BoolExpr.cs
View file

@ -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
/// <summary> Constructor for BoolExpr </summary>
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

6
src/api/dotnet/BoolSort.cs
View file

@ -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
};
}

12
src/api/dotnet/Constructor.cs
View file

@ -17,15 +17,14 @@ Notes:
--*/
using System.Diagnostics;
using System;
using System.Diagnostics.Contracts;
namespace Microsoft.Z3
{
/// <summary>
/// Constructors are used for datatype sorts.
/// </summary>
[ContractVerification(true)]
public class Constructor : Z3Object
{
/// <summary>
@ -46,7 +45,6 @@ namespace Microsoft.Z3
{
get
{
Contract.Ensures(Contract.Result<FuncDecl>() != 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<FuncDecl>() != 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<FuncDecl[]>() != 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);

8
src/api/dotnet/ConstructorList.cs
View file

@ -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));
}

1203
src/api/dotnet/Context.cs
View file

File diff suppressed because it is too large Load diff

4
src/api/dotnet/DatatypeExpr.cs
View file

@ -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
}

14
src/api/dotnet/DatatypeSort.cs
View file

@ -17,15 +17,14 @@ Notes:
--*/
using System.Diagnostics;
using System;
using System.Diagnostics.Contracts;
namespace Microsoft.Z3
{
/// <summary>
/// Datatype sorts.
/// </summary>
[ContractVerification(true)]
public class DatatypeSort : Sort
{
/// <summary>
@ -43,7 +42,6 @@ namespace Microsoft.Z3
{
get
{
Contract.Ensures(Contract.Result<FuncDecl[]>() != null);
uint n = NumConstructors;
FuncDecl[] res = new FuncDecl[n];
@ -60,7 +58,6 @@ namespace Microsoft.Z3
{
get
{
Contract.Ensures(Contract.Result<FuncDecl[]>() != null);
uint n = NumConstructors;
FuncDecl[] res = new FuncDecl[n];
@ -77,7 +74,6 @@ namespace Microsoft.Z3
{
get
{
Contract.Ensures(Contract.Result<FuncDecl[][]>() != 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
};

3
src/api/dotnet/Deprecated.cs
View file

@ -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
{
/// <summary>
/// The main interaction with Z3 happens via the Context.
/// </summary>
[ContractVerification(true)]
public class Deprecated
{

12
src/api/dotnet/EnumSort.cs
View file

@ -17,15 +17,14 @@ Notes:
--*/
using System.Diagnostics;
using System;
using System.Diagnostics.Contracts;
namespace Microsoft.Z3
{
/// <summary>
/// Enumeration sorts.
/// </summary>
[ContractVerification(true)]
public class EnumSort : Sort
{
/// <summary>
@ -35,7 +34,6 @@ namespace Microsoft.Z3
{
get
{
Contract.Ensures(Contract.Result<FuncDecl[]>() != 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<Expr[]>() != 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<FuncDecl[]>() != 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];

52
src/api/dotnet/Expr.cs
View file

@ -17,15 +17,16 @@ Notes:
--*/
using System.Diagnostics;
using System;
using System.Diagnostics.Contracts;
using System.Linq;
namespace Microsoft.Z3
{
/// <summary>
/// Expressions are terms.
/// </summary>
[ContractVerification(true)]
public class Expr : AST
{
/// <summary>
@ -35,7 +36,6 @@ namespace Microsoft.Z3
/// <seealso cref="Context.SimplifyHelp"/>
public Expr Simplify(Params p = null)
{
Contract.Ensures(Contract.Result<Expr>() != 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<FuncDecl>() != 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<Expr[]>() != null);
uint n = NumArgs;
Expr[] res = new Expr[n];
@ -94,7 +92,6 @@ namespace Microsoft.Z3
/// </summary>
public Expr Arg(uint i)
{
Contract.Ensures(Contract.Result<Expr>() != null);
return Expr.Create(Context, Native.Z3_get_app_arg(Context.nCtx, NativeObject, i));
}
@ -104,8 +101,8 @@ namespace Microsoft.Z3
/// </summary>
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<Expr>(args);
if (IsApp && args.Length != NumArgs)
@ -123,11 +120,10 @@ namespace Microsoft.Z3
/// </remarks>
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<Expr>() != 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<Expr>(from);
Context.CheckContextMatch<Expr>(to);
@ -142,9 +138,8 @@ namespace Microsoft.Z3
/// <seealso cref="Substitute(Expr[],Expr[])"/>
public Expr Substitute(Expr from, Expr to)
{
Contract.Requires(from != null);
Contract.Requires(to != null);
Contract.Ensures(Contract.Result<Expr>() != null);
Debug.Assert(from != null);
Debug.Assert(to != null);
return Substitute(new Expr[] { from }, new Expr[] { to });
}
@ -157,9 +152,8 @@ namespace Microsoft.Z3
/// </remarks>
public Expr SubstituteVars(Expr[] to)
{
Contract.Requires(to != null);
Contract.Requires(Contract.ForAll(to, t => t != null));
Contract.Ensures(Contract.Result<Expr>() != null);
Debug.Assert(to != null);
Debug.Assert(to.All(t => t != null));
Context.CheckContextMatch<Expr>(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<Sort>() != null);
return Sort.Create(Context, Native.Z3_get_sort(Context.nCtx, NativeObject));
}
}
@ -332,7 +325,7 @@ namespace Microsoft.Z3
/// <summary>
/// Retrieve bound of at-most
/// </summary>
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; } }
/// <summary>
/// Indicates whether the term is at-least
@ -342,7 +335,7 @@ namespace Microsoft.Z3
/// <summary>
/// Retrieve bound of at-least
/// </summary>
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; } }
/// <summary>
/// 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
/// <summary>
/// Constructor for Expr
/// </summary>
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<Expr>() != 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<Expr>() != 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)

4
src/api/dotnet/FPExpr.cs
View file

@ -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
}

5
src/api/dotnet/FPNum.cs
View file

@ -16,15 +16,14 @@ Author:
Notes:
--*/
using System.Diagnostics;
using System;
using System.Diagnostics.Contracts;
namespace Microsoft.Z3
{
/// <summary>
/// FloatiungPoint Numerals
/// </summary>
[ContractVerification(true)]
public class FPNum : FPExpr
{
/// <summary>
@ -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

4
src/api/dotnet/FPRMExpr.cs
View file

@ -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
}

4
src/api/dotnet/FPRMNum.cs
View file

@ -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
}

6
src/api/dotnet/FPRMSort.cs
View file

@ -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
}

6
src/api/dotnet/FPSort.cs
View file

@ -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
}

4
src/api/dotnet/FiniteDomainExpr.cs
View file

@ -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
}

5
src/api/dotnet/FiniteDomainNum.cs
View file

@ -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
/// <summary>
/// Finite-domain numerals
/// </summary>
[ContractVerification(true)]
public class FiniteDomainNum : FiniteDomainExpr
{
/// <summary>
@ -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
}
}

9
src/api/dotnet/FiniteDomainSort.cs
View file

@ -17,15 +17,14 @@ Notes:
--*/
using System.Diagnostics;
using System;
using System.Diagnostics.Contracts;
namespace Microsoft.Z3
{
/// <summary>
/// Finite domain sorts.
/// </summary>
[ContractVerification(true)]
public class FiniteDomainSort : Sort
{
/// <summary>
@ -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

37
src/api/dotnet/Fixedpoint.cs
View file

@ -18,14 +18,14 @@ Notes:
--*/
using System;
using System.Diagnostics.Contracts;
using System.Diagnostics;
using System.Linq;
namespace Microsoft.Z3
{
/// <summary>
/// Object for managing fixedpoints
/// </summary>
[ContractVerification(true)]
public class Fixedpoint : Z3Object
{
@ -36,7 +36,6 @@ namespace Microsoft.Z3
{
get
{
Contract.Ensures(Contract.Result<string>() != 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
/// </summary>
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<BoolExpr>(constraints);
foreach (BoolExpr a in constraints)
@ -91,7 +90,7 @@ namespace Microsoft.Z3
/// </summary>
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
/// </summary>
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
/// </summary>
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
/// </summary>
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
/// </summary>
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<FuncDecl>(relations);
Z3_lbool r = (Z3_lbool)Native.Z3_fixedpoint_query_relations(Context.nCtx, NativeObject,
@ -187,7 +186,7 @@ namespace Microsoft.Z3
/// </summary>
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
/// </summary>
public string GetReasonUnknown()
{
Contract.Ensures(Contract.Result<string>() != null);
return Native.Z3_fixedpoint_get_reason_unknown(Context.nCtx, NativeObject);
}
@ -252,7 +250,7 @@ namespace Microsoft.Z3
/// </summary>
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<BoolExpr[]>() != 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<BoolExpr[]>() != 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<Statistics>() != 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

25
src/api/dotnet/FuncDecl.cs
View file

@ -18,14 +18,15 @@ Notes:
--*/
using System;
using System.Diagnostics.Contracts;
using System.Diagnostics;
using System.Linq;
namespace Microsoft.Z3
{
/// <summary>
/// Function declarations.
/// </summary>
[ContractVerification(true)]
public class FuncDecl : AST
{
/// <summary>
@ -108,7 +109,6 @@ namespace Microsoft.Z3
{
get
{
Contract.Ensures(Contract.Result<Sort[]>() != null);
uint n = DomainSize;
@ -126,7 +126,6 @@ namespace Microsoft.Z3
{
get
{
Contract.Ensures(Contract.Result<Sort>() != null);
return Sort.Create(Context, Native.Z3_get_range(Context.nCtx, NativeObject));
}
}
@ -146,7 +145,6 @@ namespace Microsoft.Z3
{
get
{
Contract.Ensures(Contract.Result<Symbol>() != 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<Parameter[]>() != 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
/// <returns></returns>
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<Expr>(args);
return Expr.Create(Context, this, args);

13
src/api/dotnet/FuncInterp.cs
View file

@ -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.
/// </summary>
[ContractVerification(true)]
public class FuncInterp : Z3Object
{
/// <summary>
@ -42,7 +41,6 @@ namespace Microsoft.Z3
{
get
{
Contract.Ensures(Contract.Result<Expr>() != 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<Expr[]>() != null);
Contract.Ensures(Contract.Result<Expr[]>().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<Entry[]>() != null);
Contract.Ensures(Contract.ForAll(0, Contract.Result<Entry[]>().Length, j => Contract.Result<Entry[]>()[j] != null));
uint n = NumEntries;
Entry[] res = new Entry[n];
@ -151,7 +145,6 @@ namespace Microsoft.Z3
{
get
{
Contract.Ensures(Contract.Result<Expr>() != 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

2
src/api/dotnet/Global.cs
View file

@ -17,9 +17,9 @@ Notes:
--*/
using System.Diagnostics;
using System;
using System.Runtime.InteropServices;
using System.Diagnostics.Contracts;
namespace Microsoft.Z3
{

18
src/api/dotnet/Goal.cs
View file

@ -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.
/// </summary>
[ContractVerification(true)]
public class Goal : Z3Object
{
/// <summary>
@ -79,13 +79,13 @@ namespace Microsoft.Z3
/// </summary>
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<BoolExpr>(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<BoolExpr[]>() != null);
uint n = Size;
BoolExpr[] res = new BoolExpr[n];
@ -181,7 +180,6 @@ namespace Microsoft.Z3
/// <returns>A model for <c>g</c></returns>
public Model ConvertModel(Model m)
{
Contract.Ensures(Contract.Result<Model>() != 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
/// </summary>
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

15
src/api/dotnet/IDecRefQueue.cs
View file

@ -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
{
/// <summary>
/// DecRefQueue interface
/// </summary>
[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);
}
}
}

4
src/api/dotnet/IntExpr.cs
View file

@ -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
}

5
src/api/dotnet/IntNum.cs
View file

@ -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
/// <summary>
/// Integer Numerals
/// </summary>
[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

6
src/api/dotnet/IntSort.cs
View file

@ -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
}

7
src/api/dotnet/IntSymbol.cs
View file

@ -18,15 +18,14 @@ Notes:
--*/
using System;
using System.Diagnostics;
using System.Runtime.InteropServices;
using System.Diagnostics.Contracts;
namespace Microsoft.Z3
{
/// <summary>
/// Numbered symbols
/// </summary>
[ContractVerification(true)]
public class IntSymbol : Symbol
{
/// <summary>
@ -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

31
src/api/dotnet/Lambda.cs
View file

@ -18,14 +18,14 @@ Notes:
--*/
using System;
using System.Diagnostics.Contracts;
using System.Diagnostics;
using System.Linq;
namespace Microsoft.Z3
{
/// <summary>
/// Lambda expressions.
/// </summary>
[ContractVerification(true)]
public class Lambda : ArrayExpr
{
/// <summary>
@ -43,7 +43,6 @@ namespace Microsoft.Z3
{
get
{
Contract.Ensures(Contract.Result<Symbol[]>() != null);
uint n = NumBound;
Symbol[] res = new Symbol[n];
@ -60,7 +59,6 @@ namespace Microsoft.Z3
{
get
{
Contract.Ensures(Contract.Result<Sort[]>() != null);
uint n = NumBound;
Sort[] res = new Sort[n];
@ -77,7 +75,6 @@ namespace Microsoft.Z3
{
get
{
Contract.Ensures(Contract.Result<BoolExpr>() != 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<Sort>(sorts);
Context.CheckContextMatch<Symbol>(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<Expr>(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)

16
src/api/dotnet/ListSort.cs
View file

@ -17,15 +17,14 @@ Notes:
--*/
using System.Diagnostics;
using System;
using System.Diagnostics.Contracts;
namespace Microsoft.Z3
{
/// <summary>
/// List sorts.
/// </summary>
[ContractVerification(true)]
public class ListSort : Sort
{
/// <summary>
@ -35,7 +34,6 @@ namespace Microsoft.Z3
{
get
{
Contract.Ensures(Contract.Result<FuncDecl>() != 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<Expr>() != null);
return Context.MkApp(NilDecl);
}
}
@ -59,7 +56,6 @@ namespace Microsoft.Z3
{
get
{
Contract.Ensures(Contract.Result<FuncDecl>() != 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<FuncDecl>() != 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<FuncDecl>() != 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<FuncDecl>() != 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<FuncDecl>() != 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,

6
src/api/dotnet/Log.cs
View file

@ -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.
/// </remarks>
[ContractVerification(true)]
public static class Log
{
private static bool m_is_open = false;
@ -59,7 +58,7 @@ namespace Microsoft.Z3
/// </summary>
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.
/// </summary>
/// <returns>True if the interaction log is open, false otherwise.</returns>
[Pure]
public static bool isOpen()
{
return m_is_open;

24
src/api/dotnet/Model.cs
View file

@ -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
/// <summary>
/// A Model contains interpretations (assignments) of constants and functions.
/// </summary>
[ContractVerification(true)]
public class Model : Z3Object
{
/// <summary>
@ -36,7 +35,7 @@ namespace Microsoft.Z3
/// <returns>An expression if the constant has an interpretation in the model, null otherwise.</returns>
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
/// <returns>An expression if the function has an interpretation in the model, null otherwise.</returns>
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
/// <returns>A FunctionInterpretation if the function has an interpretation in the model, null otherwise.</returns>
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<FuncDecl[]>() != null);
uint n = NumConsts;
FuncDecl[] res = new FuncDecl[n];
@ -165,7 +163,6 @@ namespace Microsoft.Z3
{
get
{
Contract.Ensures(Contract.Result<FuncDecl[]>() != null);
uint n = NumFuncs;
FuncDecl[] res = new FuncDecl[n];
@ -182,7 +179,6 @@ namespace Microsoft.Z3
{
get
{
Contract.Ensures(Contract.Result<FuncDecl[]>() != null);
uint nFuncs = NumFuncs;
uint nConsts = NumConsts;
@ -223,8 +219,7 @@ namespace Microsoft.Z3
/// <returns>The evaluation of <paramref name="t"/> in the model.</returns>
public Expr Eval(Expr t, bool completion = false)
{
Contract.Requires(t != null);
Contract.Ensures(Contract.Result<Expr>() != 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
/// </summary>
public Expr Evaluate(Expr t, bool completion = false)
{
Contract.Requires(t != null);
Contract.Ensures(Contract.Result<Expr>() != null);
Debug.Assert(t != null);
return Eval(t, completion);
}
@ -263,7 +257,6 @@ namespace Microsoft.Z3
{
get
{
Contract.Ensures(Contract.Result<Sort[]>() != null);
uint n = NumSorts;
Sort[] res = new Sort[n];
@ -281,8 +274,7 @@ namespace Microsoft.Z3
/// <returns>An array of expressions, where each is an element of the universe of <paramref name="s"/></returns>
public Expr[] SortUniverse(Sort s)
{
Contract.Requires(s != null);
Contract.Ensures(Contract.Result<Expr[]>() != 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

20
src/api/dotnet/Optimize.cs
View file

@ -19,14 +19,14 @@ Notes:
using System;
using System.Collections.Generic;
using System.Diagnostics.Contracts;
using System.Diagnostics;
using System.Linq;
namespace Microsoft.Z3
{
/// <summary>
/// Object for managing optimizization context
/// </summary>
[ContractVerification(true)]
public class Optimize : Z3Object
{
/// <summary>
@ -36,7 +36,6 @@ namespace Microsoft.Z3
{
get
{
Contract.Ensures(Contract.Result<string>() != 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
/// </summary>
private void AddConstraints(IEnumerable<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)
@ -248,7 +247,6 @@ namespace Microsoft.Z3
{
get
{
Contract.Ensures(Contract.Result<Expr[]>() != 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<string>() != null);
return Native.Z3_optimize_get_reason_unknown(Context.nCtx, NativeObject);
}
}
@ -357,7 +354,6 @@ namespace Microsoft.Z3
{
get
{
Contract.Ensures(Contract.Result<BoolExpr[]>() != 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<Expr[]>() != 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<Statistics>() != 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

11
src/api/dotnet/ParamDescrs.cs
View file

@ -17,15 +17,14 @@ Notes:
--*/
using System.Diagnostics;
using System;
using System.Diagnostics.Contracts;
namespace Microsoft.Z3
{
/// <summary>
/// A ParamDescrs describes a set of parameters.
/// </summary>
[ContractVerification(true)]
public class ParamDescrs : Z3Object
{
/// <summary>
@ -33,7 +32,7 @@ namespace Microsoft.Z3
/// </summary>
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
/// </summary>
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
/// </summary>
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

23
src/api/dotnet/Params.cs
View file

@ -17,15 +17,14 @@ Notes:
--*/
using System.Diagnostics;
using System;
using System.Diagnostics.Contracts;
namespace Microsoft.Z3
{
/// <summary>
/// A Params objects represents a configuration in the form of Symbol/value pairs.
/// </summary>
[ContractVerification(true)]
public class Params : Z3Object
{
/// <summary>
@ -33,7 +32,7 @@ namespace Microsoft.Z3
/// </summary>
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
/// </summary>
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
/// </summary>
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
/// </summary>
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
/// </summary>
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
/// </summary>
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
/// </summary>
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

6
src/api/dotnet/Pattern.cs
View file

@ -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.
/// </summary>
[ContractVerification(true)]
public class Pattern : AST
{
/// <summary>
@ -46,7 +45,6 @@ namespace Microsoft.Z3
{
get
{
Contract.Ensures(Contract.Result<Expr[]>() != 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
}

11
src/api/dotnet/Probe.cs
View file

@ -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 <c>Context.ProbeNames</c>.
/// It may also be obtained using the command <c>(help-tactic)</c> in the SMT 2.0 front-end.
/// </summary>
[ContractVerification(true)]
public class Probe : Z3Object
{
/// <summary>
@ -40,7 +39,7 @@ namespace Microsoft.Z3
/// "Boolean" probes return 0.0 for false, and a value different from 0.0 for true.</returns>
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

41
src/api/dotnet/Quantifier.cs
View file

@ -18,14 +18,14 @@ Notes:
--*/
using System;
using System.Diagnostics.Contracts;
using System.Diagnostics;
using System.Linq;
namespace Microsoft.Z3
{
/// <summary>
/// Quantifier expressions.
/// </summary>
[ContractVerification(true)]
public class Quantifier : BoolExpr
{
/// <summary>
@ -67,7 +67,6 @@ namespace Microsoft.Z3
{
get
{
Contract.Ensures(Contract.Result<Pattern[]>() != null);
uint n = NumPatterns;
Pattern[] res = new Pattern[n];
@ -92,7 +91,6 @@ namespace Microsoft.Z3
{
get
{
Contract.Ensures(Contract.Result<Pattern[]>() != null);
uint n = NumNoPatterns;
Pattern[] res = new Pattern[n];
@ -117,7 +115,6 @@ namespace Microsoft.Z3
{
get
{
Contract.Ensures(Contract.Result<Symbol[]>() != null);
uint n = NumBound;
Symbol[] res = new Symbol[n];
@ -134,7 +131,6 @@ namespace Microsoft.Z3
{
get
{
Contract.Ensures(Contract.Result<Sort[]>() != null);
uint n = NumBound;
Sort[] res = new Sort[n];
@ -151,7 +147,6 @@ namespace Microsoft.Z3
{
get
{
Contract.Ensures(Contract.Result<BoolExpr>() != 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<Pattern>(patterns);
Context.CheckContextMatch<Expr>(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<Expr>(noPatterns);
Context.CheckContextMatch<Pattern>(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)

7
src/api/dotnet/RatNum.cs
View file

@ -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
/// <summary>
/// Rational Numerals
/// </summary>
[ContractVerification(true)]
public class RatNum : RealExpr
{
/// <summary>
@ -38,7 +37,6 @@ namespace Microsoft.Z3
{
get
{
Contract.Ensures(Contract.Result<IntNum>() != null);
return new IntNum(Context, Native.Z3_get_numerator(Context.nCtx, NativeObject));
}
@ -51,7 +49,6 @@ namespace Microsoft.Z3
{
get
{
Contract.Ensures(Contract.Result<IntNum>() != 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
}

4
src/api/dotnet/ReExpr.cs
View file

@ -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
}

6
src/api/dotnet/ReSort.cs
View file

@ -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
}

4
src/api/dotnet/RealExpr.cs
View file

@ -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
}

6
src/api/dotnet/RealSort.cs
View file

@ -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
}

6
src/api/dotnet/RelationSort.cs
View file

@ -17,15 +17,14 @@ Notes:
--*/
using System.Diagnostics;
using System;
using System.Diagnostics.Contracts;
namespace Microsoft.Z3
{
/// <summary>
/// Relation sorts.
/// </summary>
[ContractVerification(true)]
public class RelationSort : Sort
{
/// <summary>
@ -43,7 +42,6 @@ namespace Microsoft.Z3
{
get
{
Contract.Ensures(Contract.Result<Sort[]>() != 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
}

4
src/api/dotnet/SeqExpr.cs
View file

@ -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
}

6
src/api/dotnet/SeqSort.cs
View file

@ -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
}

9
src/api/dotnet/SetSort.cs
View file

@ -17,28 +17,27 @@ Notes:
--*/
using System.Diagnostics;
using System;
using System.Diagnostics.Contracts;
namespace Microsoft.Z3
{
/// <summary>
/// Set sorts.
/// </summary>
[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
}

30
src/api/dotnet/Solver.cs
View file

@ -18,16 +18,15 @@ Notes:
--*/
using System;
using System.Diagnostics;
using System.Linq;
using System.Collections.Generic;
using System.Diagnostics.Contracts;
namespace Microsoft.Z3
{
/// <summary>
/// Solvers.
/// </summary>
[ContractVerification(true)]
public class Solver : Z3Object
{
/// <summary>
@ -37,7 +36,6 @@ namespace Microsoft.Z3
{
get
{
Contract.Ensures(Contract.Result<string>() != 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
/// </summary>
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<BoolExpr>(constraints);
foreach (BoolExpr a in constraints)
@ -191,9 +189,9 @@ namespace Microsoft.Z3
/// </remarks>
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<BoolExpr>(constraints);
Context.CheckContextMatch<BoolExpr>(ps);
if (constraints.Length != ps.Length)
@ -216,8 +214,8 @@ namespace Microsoft.Z3
/// </remarks>
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<BoolExpr[]>() != 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<BoolExpr[]>() != 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<Expr[]>() != 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<string>() != null);
return Native.Z3_solver_get_reason_unknown(Context.nCtx, NativeObject);
}
@ -455,8 +449,7 @@ namespace Microsoft.Z3
/// </summary>
public Solver Translate(Context ctx)
{
Contract.Requires(ctx != null);
Contract.Ensures(Contract.Result<Solver>() != 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<Statistics>() != 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;
}

10
src/api/dotnet/Sort.cs
View file

@ -17,15 +17,14 @@ Notes:
--*/
using System.Diagnostics;
using System;
using System.Diagnostics.Contracts;
namespace Microsoft.Z3
{
/// <summary>
/// The Sort class implements type information for ASTs.
/// </summary>
[ContractVerification(true)]
public class Sort : AST
{
/// <summary>
@ -100,7 +99,6 @@ namespace Microsoft.Z3
{
get
{
Contract.Ensures(Contract.Result<Symbol>() != null);
return Symbol.Create(Context, Native.Z3_get_sort_name(Context.nCtx, NativeObject));
}
}
@ -127,7 +125,7 @@ namespace Microsoft.Z3
/// <summary>
/// Sort constructor
/// </summary>
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<Sort>() != null);
Debug.Assert(ctx != null);
switch ((Z3_sort_kind)Native.Z3_get_sort_kind(ctx.nCtx, obj))
{

11
src/api/dotnet/Statistics.cs
View file

@ -18,14 +18,14 @@ Notes:
--*/
using System;
using System.Diagnostics.Contracts;
using System.Diagnostics;
namespace Microsoft.Z3
{
/// <summary>
/// Objects of this class track statistical information about solvers.
/// </summary>
[ContractVerification(true)]
public class Statistics : Z3Object
{
/// <summary>
@ -62,7 +62,6 @@ namespace Microsoft.Z3
{
get
{
Contract.Ensures(Contract.Result<string>() != null);
if (IsUInt)
return m_uint.ToString();
@ -124,9 +123,6 @@ namespace Microsoft.Z3
{
get
{
Contract.Ensures(Contract.Result<Entry[]>() != null);
Contract.Ensures(Contract.Result<Entry[]>().Length == this.Size);
Contract.Ensures(Contract.ForAll(0, Contract.Result<Entry[]>().Length, j => Contract.Result<Entry[]>()[j] != null));
uint n = Size;
Entry[] res = new Entry[n];
@ -153,7 +149,6 @@ namespace Microsoft.Z3
{
get
{
Contract.Ensures(Contract.Result<string[]>() != 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

1
src/api/dotnet/Status.cs
View file

@ -17,6 +17,7 @@ Notes:
--*/
using System.Diagnostics;
using System;
namespace Microsoft.Z3

8
src/api/dotnet/StringSymbol.cs
View file

@ -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
/// <summary>
/// Named symbols
/// </summary>
[ContractVerification(true)]
public class StringSymbol : Symbol
{
/// <summary>
@ -38,7 +37,6 @@ namespace Microsoft.Z3
{
get
{
Contract.Ensures(Contract.Result<string>() != 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

8
src/api/dotnet/Symbol.cs
View file

@ -18,15 +18,14 @@ Notes:
--*/
using System;
using System.Diagnostics;
using System.Runtime.InteropServices;
using System.Diagnostics.Contracts;
namespace Microsoft.Z3
{
/// <summary>
/// Symbols are used to name several term and type constructors.
/// </summary>
[ContractVerification(true)]
public class Symbol : Z3Object
{
/// <summary>
@ -113,13 +112,12 @@ namespace Microsoft.Z3
/// </summary>
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<Symbol>() != null);
Debug.Assert(ctx != null);
switch ((Z3_symbol_kind)Native.Z3_get_symbol_kind(ctx.nCtx, obj))
{

15
src/api/dotnet/Tactic.cs
View file

@ -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 <c>Context.TacticNames</c>.
/// It may also be obtained using the command <c>(help-tactic)</c> in the SMT 2.0 front-end.
/// </summary>
[ContractVerification(true)]
public class Tactic : Z3Object
{
/// <summary>
@ -38,7 +37,6 @@ namespace Microsoft.Z3
{
get
{
Contract.Ensures(Contract.Result<string>() != null);
return Native.Z3_tactic_get_help(Context.nCtx, NativeObject);
}
@ -59,8 +57,7 @@ namespace Microsoft.Z3
/// </summary>
public ApplyResult Apply(Goal g, Params p = null)
{
Contract.Requires(g != null);
Contract.Ensures(Contract.Result<ApplyResult>() != 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<ApplyResult>() != null);
Debug.Assert(g != null);
return Apply(g);
}
@ -94,7 +90,6 @@ namespace Microsoft.Z3
{
get
{
Contract.Ensures(Contract.Result<Solver>() != 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);
}
/// <summary>

9
src/api/dotnet/TupleSort.cs
View file

@ -18,14 +18,13 @@ Notes:
--*/
using System;
using System.Diagnostics.Contracts;
using System.Diagnostics;
namespace Microsoft.Z3
{
/// <summary>
/// Tuple sorts.
/// </summary>
[ContractVerification(true)]
public class TupleSort : Sort
{
/// <summary>
@ -35,7 +34,6 @@ namespace Microsoft.Z3
{
get
{
Contract.Ensures(Contract.Result<FuncDecl>() != 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<FuncDecl[]>() != 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];

8
src/api/dotnet/UninterpretedSort.cs
View file

@ -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
}

4
src/api/dotnet/Version.cs
View file

@ -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.
/// </summary>
/// <remarks>Note that this class is static.</remarks>
[ContractVerification(true)]
public static class Version
{
static Version() { }
@ -99,7 +98,6 @@ namespace Microsoft.Z3
/// </summary>
new public static string ToString()
{
Contract.Ensures(Contract.Result<string>() != null);
uint major = 0, minor = 0, build = 0, revision = 0;
Native.Z3_get_version(ref major, ref minor, ref build, ref revision);

1
src/api/dotnet/Z3Exception.cs
View file

@ -17,6 +17,7 @@ Notes:
--*/
using System.Diagnostics;
using System;
namespace Microsoft.Z3

18
src/api/dotnet/Z3Object.cs
View file

@ -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.
/// </summary>
[ContractVerification(true)]
public class Z3Object : IDisposable
{
/// <summary>
@ -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<Context>() != null);
return m_ctx;
}
}
[Pure]
internal static IntPtr[] ArrayToNative(Z3Object[] a)
{
Contract.Ensures(a == null || Contract.Result<IntPtr[]>() != null);
Contract.Ensures(a == null || Contract.Result<IntPtr[]>().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<T>(IEnumerable<T> a) where T : Z3Object
{
Contract.Ensures(a == null || Contract.Result<IntPtr[]>() != null);
Contract.Ensures(a == null || Contract.Result<IntPtr[]>().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;