3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 18:31:49 +00:00

Managed API: Refactoring and formatting.

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger 2012-11-23 18:30:51 +00:00
parent edc9dccbcf
commit 7defd469bb
52 changed files with 2006 additions and 1657 deletions

View file

@ -203,7 +203,7 @@ namespace Microsoft.Z3
internal AST(Context ctx) : base(ctx) { Contract.Requires(ctx != null); }
internal AST(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); }
internal class DecRefQueue : Z3.DecRefQueue
internal class DecRefQueue : IDecRefQueue
{
public override void IncRef(Context ctx, IntPtr obj)
{

View file

@ -126,7 +126,7 @@ namespace Microsoft.Z3
Contract.Requires(ctx != null);
}
internal class DecRefQueue : Z3.DecRefQueue
internal class DecRefQueue : IDecRefQueue
{
public override void IncRef(Context ctx, IntPtr obj)
{

View file

@ -103,7 +103,7 @@ namespace Microsoft.Z3
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 class DecRefQueue : Z3.DecRefQueue
internal class DecRefQueue : IDecRefQueue
{
public override void IncRef(Context ctx, IntPtr obj)
{

View file

@ -0,0 +1,81 @@
/*++
Copyright (c) 2012 Microsoft Corporation
Module Name:
IntNum.cs
Abstract:
Z3 Managed API: Int Numerals
Author:
Christoph Wintersteiger (cwinter) 2012-03-20
Notes:
--*/
using System;
using System.Diagnostics.Contracts;
#if !FRAMEWORK_LT_4
using System.Numerics;
#endif
namespace Microsoft.Z3
{
/// <summary>
/// Algebraic numbers
/// </summary>
[ContractVerification(true)]
public class AlgebraicNum : ArithExpr
{
/// <summary>
/// Return a upper bound for a given real algebraic number.
/// The interval isolating the number is smaller than 1/10^<paramref name="precision"/>.
/// <seealso cref="Expr.IsAlgebraicNumber"/>
/// </summary>
/// <param name="precision">the precision of the result</param>
/// <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));
}
/// <summary>
/// Return a lower bound for the given real algebraic number.
/// The interval isolating the number is smaller than 1/10^<paramref name="precision"/>.
/// <seealso cref="Expr.IsAlgebraicNumber"/>
/// </summary>
/// <param name="precision"></param>
/// <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));
}
/// <summary>
/// Returns a string representation in decimal notation.
/// </summary>
/// <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);
}
#region Internal
internal AlgebraicNum(Context ctx, IntPtr obj)
: base(ctx, obj)
{
Contract.Requires(ctx != null);
}
#endregion
}
}

View file

@ -44,8 +44,8 @@ namespace Microsoft.Z3
{
get
{
Contract.Ensures(Contract.Result<Goal[]>() != null);
Contract.Ensures(Contract.Result<Goal[]>().Length == this.NumSubgoals);
Contract.Ensures(Contract.Result<Goal[]>() != null);
Contract.Ensures(Contract.Result<Goal[]>().Length == this.NumSubgoals);
uint n = NumSubgoals;
Goal[] res = new Goal[n];
@ -77,12 +77,13 @@ namespace Microsoft.Z3
}
#region Internal
internal ApplyResult(Context ctx, IntPtr obj) : base(ctx, obj)
internal ApplyResult(Context ctx, IntPtr obj)
: base(ctx, obj)
{
Contract.Requires(ctx != null);
}
internal class DecRefQueue : Z3.DecRefQueue
internal class DecRefQueue : IDecRefQueue
{
public override void IncRef(Context ctx, IntPtr obj)
{
@ -93,7 +94,7 @@ namespace Microsoft.Z3
{
Native.Z3_apply_result_dec_ref(ctx.nCtx, obj);
}
};
};
internal override void IncRef(IntPtr o)
{

View file

@ -0,0 +1,47 @@
/*++
Copyright (<c>) 2012 Microsoft Corporation
Module Name:
ArithExpr.cs
Abstract:
Z3 Managed API: Arith Expressions
Author:
Christoph Wintersteiger (cwinter) 2012-11-23
Notes:
--*/
using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;
using System.Diagnostics.Contracts;
namespace Microsoft.Z3
{
/// <summary>
/// Arithmetic expressions (int/real)
/// </summary>
public class ArithExpr : Expr
{
#region Internal
/// <summary> Constructor for ArithExpr </summary>
internal protected ArithExpr(Context ctx)
: base(ctx)
{
Contract.Requires(ctx != null);
}
internal ArithExpr(Context ctx, IntPtr obj)
: base(ctx, obj)
{
Contract.Requires(ctx != null);
}
#endregion
}
}

View file

@ -0,0 +1,34 @@
/*++
Copyright (c) 2012 Microsoft Corporation
Module Name:
ArithSort.cs
Abstract:
Z3 Managed API: Arith Sorts
Author:
Christoph Wintersteiger (cwinter) 2012-11-23
Notes:
--*/
using System;
using System.Diagnostics.Contracts;
namespace Microsoft.Z3
{
/// <summary>
/// An arithmetic sort, i.e., Int or Real.
/// </summary>
public class ArithSort : Sort
{
#region Internal
internal ArithSort(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); }
#endregion
};
}

View file

@ -0,0 +1,47 @@
/*++
Copyright (<c>) 2012 Microsoft Corporation
Module Name:
ArrayExpr.cs
Abstract:
Z3 Managed API: Array Expressions
Author:
Christoph Wintersteiger (cwinter) 2012-11-23
Notes:
--*/
using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;
using System.Diagnostics.Contracts;
namespace Microsoft.Z3
{
/// <summary>
/// Array expressions
/// </summary>
public class ArrayExpr : Expr
{
#region Internal
/// <summary> Constructor for ArrayExpr </summary>
internal protected ArrayExpr(Context ctx)
: base(ctx)
{
Contract.Requires(ctx != null);
}
internal ArrayExpr(Context ctx, IntPtr obj)
: base(ctx, obj)
{
Contract.Requires(ctx != null);
}
#endregion
}
}

View file

@ -0,0 +1,69 @@
/*++
Copyright (c) 2012 Microsoft Corporation
Module Name:
ArraySort.cs
Abstract:
Z3 Managed API: Array Sorts
Author:
Christoph Wintersteiger (cwinter) 2012-11-23
Notes:
--*/
using System;
using System.Diagnostics.Contracts;
namespace Microsoft.Z3
{
/// <summary>
/// Array sorts.
/// </summary>
[ContractVerification(true)]
public class ArraySort : Sort
{
/// <summary>
/// The domain of the array sort.
/// </summary>
public Sort Domain
{
get
{
Contract.Ensures(Contract.Result<Sort>() != null);
return Sort.Create(Context, Native.Z3_get_array_sort_domain(Context.nCtx, NativeObject));
}
}
/// <summary>
/// The range of the array sort.
/// </summary>
public Sort Range
{
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, 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);
}
#endregion
};
}

View file

@ -0,0 +1,48 @@
/*++
Copyright (<c>) 2012 Microsoft Corporation
Module Name:
BitVecExpr.cs
Abstract:
Z3 Managed API: BitVec Expressions
Author:
Christoph Wintersteiger (cwinter) 2012-11-23
Notes:
--*/
using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;
using System.Diagnostics.Contracts;
namespace Microsoft.Z3
{
/// <summary>
/// Bit-vector expressions
/// </summary>
public class BitVecExpr : Expr
{
/// <summary>
/// The size of the sort of a bit-vector term.
/// </summary>
public uint SortSize
{
get { return ((BitVecSort)Sort).Size; }
}
#region Internal
/// <summary> Constructor for BitVecExpr </summary>
internal protected BitVecExpr(Context ctx) : base(ctx) { Contract.Requires(ctx != null); }
internal BitVecExpr(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); }
#endregion
}
}

115
src/api/dotnet/BitVecNum.cs Normal file
View file

@ -0,0 +1,115 @@
/*++
Copyright (c) 2012 Microsoft Corporation
Module Name:
IntNum.cs
Abstract:
Z3 Managed API: Int Numerals
Author:
Christoph Wintersteiger (cwinter) 2012-03-20
Notes:
--*/
using System;
using System.Diagnostics.Contracts;
#if !FRAMEWORK_LT_4
using System.Numerics;
#endif
namespace Microsoft.Z3
{
/// <summary>
/// Bit-vector numerals
/// </summary>
[ContractVerification(true)]
public class BitVecNum : BitVecExpr
{
/// <summary>
/// Retrieve the 64-bit unsigned integer value.
/// </summary>
public UInt64 UInt64
{
get
{
UInt64 res = 0;
if (Native.Z3_get_numeral_uint64(Context.nCtx, NativeObject, ref res) == 0)
throw new Z3Exception("Numeral is not a 64 bit unsigned");
return res;
}
}
/// <summary>
/// Retrieve the int value.
/// </summary>
public int Int
{
get
{
int res = 0;
if (Native.Z3_get_numeral_int(Context.nCtx, NativeObject, ref res) == 0)
throw new Z3Exception("Numeral is not an int");
return res;
}
}
/// <summary>
/// Retrieve the 64-bit int value.
/// </summary>
public Int64 Int64
{
get
{
Int64 res = 0;
if (Native.Z3_get_numeral_int64(Context.nCtx, NativeObject, ref res) == 0)
throw new Z3Exception("Numeral is not an int64");
return res;
}
}
/// <summary>
/// Retrieve the int value.
/// </summary>
public uint UInt
{
get
{
uint res = 0;
if (Native.Z3_get_numeral_uint(Context.nCtx, NativeObject, ref res) == 0)
throw new Z3Exception("Numeral is not a uint");
return res;
}
}
#if !FRAMEWORK_LT_4
/// <summary>
/// Retrieve the BigInteger value.
/// </summary>
public BigInteger BigInteger
{
get
{
return BigInteger.Parse(this.ToString());
}
}
#endif
/// <summary>
/// Returns a string representation of the numeral.
/// </summary>
public override string ToString()
{
return Native.Z3_get_numeral_string(Context.nCtx, NativeObject);
}
#region Internal
internal BitVecNum(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); }
#endregion
}
}

View file

@ -0,0 +1,43 @@
/*++
Copyright (c) 2012 Microsoft Corporation
Module Name:
BitVecSort.cs
Abstract:
Z3 Managed API: BitVec Sorts
Author:
Christoph Wintersteiger (cwinter) 2012-11-23
Notes:
--*/
using System;
using System.Diagnostics.Contracts;
namespace Microsoft.Z3
{
/// <summary>
/// Bit-vector sorts.
/// </summary>
public class BitVecSort : Sort
{
/// <summary>
/// The size of the bit-vector sort.
/// </summary>
public uint Size
{
get { return Native.Z3_get_bv_sort_size(Context.nCtx, NativeObject); }
}
#region Internal
internal BitVecSort(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); }
internal BitVecSort(Context ctx, uint size) : base(ctx, Native.Z3_mk_bv_sort(ctx.nCtx, size)) { Contract.Requires(ctx != null); }
#endregion
};
}

View file

@ -0,0 +1,40 @@
/*++
Copyright (<c>) 2012 Microsoft Corporation
Module Name:
BoolExpr.cs
Abstract:
Z3 Managed API: Boolean Expressions
Author:
Christoph Wintersteiger (cwinter) 2012-11-23
Notes:
--*/
using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;
using System.Diagnostics.Contracts;
namespace Microsoft.Z3
{
/// <summary>
/// Boolean expressions
/// </summary>
public class BoolExpr : Expr
{
#region Internal
/// <summary> Constructor for BoolExpr </summary>
internal protected BoolExpr(Context ctx) : base(ctx) { Contract.Requires(ctx != null); }
/// <summary> Constructor for BoolExpr </summary>
internal BoolExpr(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); }
#endregion
}
}

View file

@ -0,0 +1,35 @@
/*++
Copyright (c) 2012 Microsoft Corporation
Module Name:
BoolSort.cs
Abstract:
Z3 Managed API: Bool Sorts
Author:
Christoph Wintersteiger (cwinter) 2012-11-23
Notes:
--*/
using System;
using System.Diagnostics.Contracts;
namespace Microsoft.Z3
{
/// <summary>
/// A Boolean sort.
/// </summary>
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); }
#endregion
};
}

View file

@ -149,35 +149,4 @@ namespace Microsoft.Z3
#endregion
}
/// <summary>
/// Lists of constructors
/// </summary>
public class ConstructorList : Z3Object
{
/// <summary>
/// Destructor.
/// </summary>
~ConstructorList()
{
Native.Z3_del_constructor_list(Context.nCtx, NativeObject);
}
#region Internal
internal ConstructorList(Context ctx, IntPtr obj)
: base(ctx, obj)
{
Contract.Requires(ctx != null);
}
internal ConstructorList(Context ctx, Constructor[] constructors)
: base(ctx)
{
Contract.Requires(ctx != null);
Contract.Requires(constructors != null);
NativeObject = Native.Z3_mk_constructor_list(Context.nCtx, (uint)constructors.Length, Constructor.ArrayToNative(constructors));
}
#endregion
}
}

View file

@ -0,0 +1,59 @@
/*++
Copyright (c) 2012 Microsoft Corporation
Module Name:
ConstructorList.cs
Abstract:
Z3 Managed API: Constructor Lists
Author:
Christoph Wintersteiger (cwinter) 2012-11-23
Notes:
--*/
using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;
using System.Diagnostics.Contracts;
namespace Microsoft.Z3
{
/// <summary>
/// Lists of constructors
/// </summary>
public class ConstructorList : Z3Object
{
/// <summary>
/// Destructor.
/// </summary>
~ConstructorList()
{
Native.Z3_del_constructor_list(Context.nCtx, NativeObject);
}
#region Internal
internal ConstructorList(Context ctx, IntPtr obj)
: base(ctx, obj)
{
Contract.Requires(ctx != null);
}
internal ConstructorList(Context ctx, Constructor[] constructors)
: base(ctx)
{
Contract.Requires(ctx != null);
Contract.Requires(constructors != null);
NativeObject = Native.Z3_mk_constructor_list(Context.nCtx, (uint)constructors.Length, Constructor.ArrayToNative(constructors));
}
#endregion
}
}

View file

@ -0,0 +1,47 @@
/*++
Copyright (<c>) 2012 Microsoft Corporation
Module Name:
DatatypeExpr.cs
Abstract:
Z3 Managed API: Datatype Expressions
Author:
Christoph Wintersteiger (cwinter) 2012-11-23
Notes:
--*/
using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;
using System.Diagnostics.Contracts;
namespace Microsoft.Z3
{
/// <summary>
/// Datatype expressions
/// </summary>
public class DatatypeExpr : Expr
{
#region Internal
/// <summary> Constructor for DatatypeExpr </summary>
internal protected DatatypeExpr(Context ctx)
: base(ctx)
{
Contract.Requires(ctx != null);
}
internal DatatypeExpr(Context ctx, IntPtr obj)
: base(ctx, obj)
{
Contract.Requires(ctx != null);
}
#endregion
}
}

View file

@ -0,0 +1,109 @@
/*++
Copyright (c) 2012 Microsoft Corporation
Module Name:
DatatypeSort.cs
Abstract:
Z3 Managed API: Datatype Sorts
Author:
Christoph Wintersteiger (cwinter) 2012-11-23
Notes:
--*/
using System;
using System.Diagnostics.Contracts;
namespace Microsoft.Z3
{
/// <summary>
/// Datatype sorts.
/// </summary>
[ContractVerification(true)]
public class DatatypeSort : Sort
{
/// <summary>
/// The number of constructors of the datatype sort.
/// </summary>
public uint NumConstructors
{
get { return Native.Z3_get_datatype_sort_num_constructors(Context.nCtx, NativeObject); }
}
/// <summary>
/// The constructors.
/// </summary>
public FuncDecl[] Constructors
{
get
{
Contract.Ensures(Contract.Result<FuncDecl[]>() != null);
uint n = NumConstructors;
FuncDecl[] res = new FuncDecl[n];
for (uint i = 0; i < n; i++)
res[i] = new FuncDecl(Context, Native.Z3_get_datatype_sort_constructor(Context.nCtx, NativeObject, i));
return res;
}
}
/// <summary>
/// The recognizers.
/// </summary>
public FuncDecl[] Recognizers
{
get
{
Contract.Ensures(Contract.Result<FuncDecl[]>() != null);
uint n = NumConstructors;
FuncDecl[] res = new FuncDecl[n];
for (uint i = 0; i < n; i++)
res[i] = new FuncDecl(Context, Native.Z3_get_datatype_sort_recognizer(Context.nCtx, NativeObject, i));
return res;
}
}
/// <summary>
/// The constructor accessors.
/// </summary>
public FuncDecl[][] Accessors
{
get
{
Contract.Ensures(Contract.Result<FuncDecl[][]>() != null);
uint n = NumConstructors;
FuncDecl[][] res = new FuncDecl[n][];
for (uint i = 0; i < n; i++)
{
FuncDecl fd = new FuncDecl(Context, Native.Z3_get_datatype_sort_constructor(Context.nCtx, NativeObject, i));
uint ds = fd.DomainSize;
FuncDecl[] tmp = new FuncDecl[ds];
for (uint j = 0; j < ds; j++)
tmp[j] = new FuncDecl(Context, Native.Z3_get_datatype_sort_constructor_accessor(Context.nCtx, NativeObject, i, j));
res[i] = tmp;
}
return res;
}
}
#region Internal
internal DatatypeSort(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(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);
}
#endregion
};
}

111
src/api/dotnet/EnumSort.cs Normal file
View file

@ -0,0 +1,111 @@
/*++
Copyright (c) 2012 Microsoft Corporation
Module Name:
EnumSort.cs
Abstract:
Z3 Managed API: Enum Sorts
Author:
Christoph Wintersteiger (cwinter) 2012-11-23
Notes:
--*/
using System;
using System.Diagnostics.Contracts;
namespace Microsoft.Z3
{
/// <summary>
/// Enumeration sorts.
/// </summary>
[ContractVerification(true)]
public class EnumSort : Sort
{
/// <summary>
/// The function declarations of the constants in the enumeration.
/// </summary>
public FuncDecl[] ConstDecls
{
get
{
Contract.Ensures(Contract.Result<FuncDecl[]>() != null);
return _constdecls;
}
}
/// <summary>
/// The constants in the enumeration.
/// </summary>
public Expr[] Consts
{
get
{
Contract.Ensures(Contract.Result<Expr[]>() != null);
return _consts;
}
}
/// <summary>
/// The test predicates for the constants in the enumeration.
/// </summary>
public FuncDecl[] TesterDecls
{
get
{
Contract.Ensures(Contract.Result<FuncDecl[]>() != null);
return _testerdecls;
}
}
#region Object Invariant
[ContractInvariantMethod]
private void ObjectInvariant()
{
Contract.Invariant(this._constdecls != null);
Contract.Invariant(this._testerdecls != null);
Contract.Invariant(this._consts != null);
}
#endregion
#region Internal
readonly private FuncDecl[] _constdecls = null, _testerdecls = null;
readonly private Expr[] _consts = null;
internal EnumSort(Context ctx, Symbol name, Symbol[] enumNames)
: base(ctx)
{
Contract.Requires(ctx != null);
Contract.Requires(name != null);
Contract.Requires(enumNames != null);
int n = enumNames.Length;
IntPtr[] n_constdecls = new IntPtr[n];
IntPtr[] n_testers = new IntPtr[n];
NativeObject = Native.Z3_mk_enumeration_sort(ctx.nCtx, name.NativeObject, (uint)n,
Symbol.ArrayToNative(enumNames), n_constdecls, n_testers);
_constdecls = new FuncDecl[n];
for (uint i = 0; i < n; i++)
_constdecls[i] = new FuncDecl(ctx, n_constdecls[i]);
_testerdecls = new FuncDecl[n];
for (uint i = 0; i < n; i++)
_testerdecls[i] = new FuncDecl(ctx, n_testers[i]);
_consts = new Expr[n];
for (uint i = 0; i < n; i++)
_consts[i] = ctx.MkApp(_constdecls[i]);
}
#endregion
};
}

View file

@ -1548,138 +1548,4 @@ namespace Microsoft.Z3
}
#endregion
}
/// <summary>
/// Boolean expressions
/// </summary>
public class BoolExpr : Expr
{
#region Internal
/// <summary> Constructor for BoolExpr </summary>
internal protected BoolExpr(Context ctx) : base(ctx) { Contract.Requires(ctx != null); }
/// <summary> Constructor for BoolExpr </summary>
internal BoolExpr(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); }
#endregion
}
/// <summary>
/// Arithmetic expressions (int/real)
/// </summary>
public class ArithExpr : Expr
{
#region Internal
/// <summary> Constructor for ArithExpr </summary>
internal protected ArithExpr(Context ctx)
: base(ctx)
{
Contract.Requires(ctx != null);
}
internal ArithExpr(Context ctx, IntPtr obj)
: base(ctx, obj)
{
Contract.Requires(ctx != null);
}
#endregion
}
/// <summary>
/// Int expressions
/// </summary>
public class IntExpr : ArithExpr
{
#region Internal
/// <summary> Constructor for IntExpr </summary>
internal protected IntExpr(Context ctx)
: base(ctx)
{
Contract.Requires(ctx != null);
}
internal IntExpr(Context ctx, IntPtr obj)
: base(ctx, obj)
{
Contract.Requires(ctx != null);
}
#endregion
}
/// <summary>
/// Real expressions
/// </summary>
public class RealExpr : ArithExpr
{
#region Internal
/// <summary> Constructor for RealExpr </summary>
internal protected RealExpr(Context ctx)
: base(ctx)
{
Contract.Requires(ctx != null);
}
internal RealExpr(Context ctx, IntPtr obj)
: base(ctx, obj)
{
Contract.Requires(ctx != null);
}
#endregion
}
/// <summary>
/// Bit-vector expressions
/// </summary>
public class BitVecExpr : Expr
{
/// <summary>
/// The size of the sort of a bit-vector term.
/// </summary>
public uint SortSize
{
get { return ((BitVecSort)Sort).Size; }
}
#region Internal
/// <summary> Constructor for BitVecExpr </summary>
internal protected BitVecExpr(Context ctx) : base(ctx) { Contract.Requires(ctx != null); }
internal BitVecExpr(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); }
#endregion
}
/// <summary>
/// Array expressions
/// </summary>
public class ArrayExpr : Expr
{
#region Internal
/// <summary> Constructor for ArrayExpr </summary>
internal protected ArrayExpr(Context ctx)
: base(ctx)
{
Contract.Requires(ctx != null);
}
internal ArrayExpr(Context ctx, IntPtr obj)
: base(ctx, obj)
{
Contract.Requires(ctx != null);
}
#endregion
}
/// <summary>
/// Datatype expressions
/// </summary>
public class DatatypeExpr : Expr
{
#region Internal
/// <summary> Constructor for DatatypeExpr </summary>
internal protected DatatypeExpr(Context ctx)
: base(ctx)
{
Contract.Requires(ctx != null);
}
internal DatatypeExpr(Context ctx, IntPtr obj)
: base(ctx, obj)
{
Contract.Requires(ctx != null);
}
#endregion
}
}

View file

@ -0,0 +1,59 @@
/*++
Copyright (c) 2012 Microsoft Corporation
Module Name:
FiniteDomainSort.cs
Abstract:
Z3 Managed API: Finite Domain Sorts
Author:
Christoph Wintersteiger (cwinter) 2012-11-23
Notes:
--*/
using System;
using System.Diagnostics.Contracts;
namespace Microsoft.Z3
{
/// <summary>
/// Finite domain sorts.
/// </summary>
[ContractVerification(true)]
public class FiniteDomainSort : Sort
{
/// <summary>
/// The size of the finite domain sort.
/// </summary>
public ulong Size
{
get
{
ulong res = 0;
Native.Z3_get_finite_domain_sort_size(Context.nCtx, NativeObject, ref res);
return res;
}
}
#region Internal
internal FiniteDomainSort(Context ctx, IntPtr obj)
: base(ctx, obj)
{
Contract.Requires(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);
}
#endregion
}
}

View file

@ -310,7 +310,7 @@ namespace Microsoft.Z3
Contract.Requires(ctx != null);
}
internal class DecRefQueue : Z3.DecRefQueue
internal class DecRefQueue : IDecRefQueue
{
public override void IncRef(Context ctx, IntPtr obj)
{

View file

@ -291,9 +291,7 @@ namespace Microsoft.Z3
}
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))
: 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);
@ -301,9 +299,7 @@ namespace Microsoft.Z3
}
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))
: 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);

View file

@ -40,9 +40,11 @@ namespace Microsoft.Z3
/// </summary>
public Expr Value
{
get {
get
{
Contract.Ensures(Contract.Result<Expr>() != null);
return Expr.Create(Context, Native.Z3_func_entry_get_value(Context.nCtx, NativeObject)); }
return Expr.Create(Context, Native.Z3_func_entry_get_value(Context.nCtx, NativeObject));
}
}
/// <summary>
@ -87,7 +89,7 @@ namespace Microsoft.Z3
#region Internal
internal Entry(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); }
internal class DecRefQueue : Z3.DecRefQueue
internal class DecRefQueue : IDecRefQueue
{
public override void IncRef(Context ctx, IntPtr obj)
{
@ -130,8 +132,7 @@ 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));
Contract.Ensures(Contract.ForAll(0, Contract.Result<Entry[]>().Length, j => Contract.Result<Entry[]>()[j] != null));
uint n = NumEntries;
Entry[] res = new Entry[n];
@ -146,10 +147,12 @@ namespace Microsoft.Z3
/// </summary>
public Expr Else
{
get {
get
{
Contract.Ensures(Contract.Result<Expr>() != null);
return Expr.Create(Context, Native.Z3_func_interp_get_else(Context.nCtx, NativeObject)); }
return Expr.Create(Context, Native.Z3_func_interp_get_else(Context.nCtx, NativeObject));
}
}
/// <summary>
@ -169,7 +172,7 @@ namespace Microsoft.Z3
res += "[";
foreach (Entry e in Entries)
{
uint n = e.NumArgs;
uint n = e.NumArgs;
if (n > 1) res += "[";
Expr[] args = e.Args;
for (uint i = 0; i < n; i++)
@ -192,7 +195,7 @@ namespace Microsoft.Z3
Contract.Requires(ctx != null);
}
internal class DecRefQueue : Z3.DecRefQueue
internal class DecRefQueue : IDecRefQueue
{
public override void IncRef(Context ctx, IntPtr obj)
{
@ -203,7 +206,7 @@ namespace Microsoft.Z3
{
Native.Z3_func_interp_dec_ref(ctx.nCtx, obj);
}
};
};
internal override void IncRef(IntPtr o)
{

View file

@ -209,7 +209,7 @@ namespace Microsoft.Z3
Contract.Requires(ctx != null);
}
internal class DecRefQueue : Z3.DecRefQueue
internal class DecRefQueue : IDecRefQueue
{
public override void IncRef(Context ctx, IntPtr obj)
{

View file

@ -26,7 +26,7 @@ using System.Diagnostics.Contracts;
namespace Microsoft.Z3
{
[ContractClass(typeof(DecRefQueueContracts))]
internal abstract class DecRefQueue
internal abstract class IDecRefQueue
{
#region Object invariant
@ -76,8 +76,8 @@ namespace Microsoft.Z3
}
}
[ContractClassFor(typeof(DecRefQueue))]
abstract class DecRefQueueContracts : DecRefQueue
[ContractClassFor(typeof(IDecRefQueue))]
abstract class DecRefQueueContracts : IDecRefQueue
{
public override void IncRef(Context ctx, IntPtr obj)
{

47
src/api/dotnet/IntExpr.cs Normal file
View file

@ -0,0 +1,47 @@
/*++
Copyright (<c>) 2012 Microsoft Corporation
Module Name:
IntExpr.cs
Abstract:
Z3 Managed API: Int Expressions
Author:
Christoph Wintersteiger (cwinter) 2012-11-23
Notes:
--*/
using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;
using System.Diagnostics.Contracts;
namespace Microsoft.Z3
{
/// <summary>
/// Int expressions
/// </summary>
public class IntExpr : ArithExpr
{
#region Internal
/// <summary> Constructor for IntExpr </summary>
internal protected IntExpr(Context ctx)
: base(ctx)
{
Contract.Requires(ctx != null);
}
internal IntExpr(Context ctx, IntPtr obj)
: base(ctx, obj)
{
Contract.Requires(ctx != null);
}
#endregion
}
}

121
src/api/dotnet/IntNum.cs Normal file
View file

@ -0,0 +1,121 @@
/*++
Copyright (c) 2012 Microsoft Corporation
Module Name:
IntNum.cs
Abstract:
Z3 Managed API: Int Numerals
Author:
Christoph Wintersteiger (cwinter) 2012-03-20
Notes:
--*/
using System;
using System.Diagnostics.Contracts;
#if !FRAMEWORK_LT_4
using System.Numerics;
#endif
namespace Microsoft.Z3
{
/// <summary>
/// Integer Numerals
/// </summary>
[ContractVerification(true)]
public class IntNum : IntExpr
{
#region Internal
internal IntNum(Context ctx, IntPtr obj)
: base(ctx, obj)
{
Contract.Requires(ctx != null);
}
#endregion
/// <summary>
/// Retrieve the 64-bit unsigned integer value.
/// </summary>
public UInt64 UInt64
{
get
{
UInt64 res = 0;
if (Native.Z3_get_numeral_uint64(Context.nCtx, NativeObject, ref res) == 0)
throw new Z3Exception("Numeral is not a 64 bit unsigned");
return res;
}
}
/// <summary>
/// Retrieve the int value.
/// </summary>
public int Int
{
get
{
int res = 0;
if (Native.Z3_get_numeral_int(Context.nCtx, NativeObject, ref res) == 0)
throw new Z3Exception("Numeral is not an int");
return res;
}
}
/// <summary>
/// Retrieve the 64-bit int value.
/// </summary>
public Int64 Int64
{
get
{
Int64 res = 0;
if (Native.Z3_get_numeral_int64(Context.nCtx, NativeObject, ref res) == 0)
throw new Z3Exception("Numeral is not an int64");
return res;
}
}
/// <summary>
/// Retrieve the int value.
/// </summary>
public uint UInt
{
get
{
uint res = 0;
if (Native.Z3_get_numeral_uint(Context.nCtx, NativeObject, ref res) == 0)
throw new Z3Exception("Numeral is not a uint");
return res;
}
}
#if !FRAMEWORK_LT_4
/// <summary>
/// Retrieve the BigInteger value.
/// </summary>
public BigInteger BigInteger
{
get
{
return BigInteger.Parse(this.ToString());
}
}
#endif
/// <summary>
/// Returns a string representation of the numeral.
/// </summary>
public override string ToString()
{
return Native.Z3_get_numeral_string(Context.nCtx, NativeObject);
}
}
}

43
src/api/dotnet/IntSort.cs Normal file
View file

@ -0,0 +1,43 @@
/*++
Copyright (c) 2012 Microsoft Corporation
Module Name:
IntSort.cs
Abstract:
Z3 Managed API: Int Sorts
Author:
Christoph Wintersteiger (cwinter) 2012-11-23
Notes:
--*/
using System;
using System.Diagnostics.Contracts;
namespace Microsoft.Z3
{
/// <summary>
/// An Integer sort
/// </summary>
public class IntSort : ArithSort
{
#region Internal
internal IntSort(Context ctx, IntPtr obj)
: base(ctx, obj)
{
Contract.Requires(ctx != null);
}
internal IntSort(Context ctx)
: base(ctx, Native.Z3_mk_int_sort(ctx.nCtx))
{
Contract.Requires(ctx != null);
}
#endregion
}
}

View file

@ -0,0 +1,68 @@
/*++
Copyright (c) 2012 Microsoft Corporation
Module Name:
IntSymbol.cs
Abstract:
Z3 Managed API: Int Symbols
Author:
Christoph Wintersteiger (cwinter) 2012-11-23
Notes:
--*/
using System;
using System.Runtime.InteropServices;
using System.Diagnostics.Contracts;
namespace Microsoft.Z3
{
/// <summary>
/// Numbered symbols
/// </summary>
[ContractVerification(true)]
public class IntSymbol : Symbol
{
/// <summary>
/// The int value of the symbol.
/// </summary>
/// <remarks>Throws an exception if the symbol is not of int kind. </remarks>
public int Int
{
get
{
if (!IsIntSymbol())
throw new Z3Exception("Int requested from non-Int symbol");
return Native.Z3_get_symbol_int(Context.nCtx, NativeObject);
}
}
#region Internal
internal IntSymbol(Context ctx, IntPtr obj)
: base(ctx, obj)
{
Contract.Requires(ctx != null);
}
internal IntSymbol(Context ctx, int i)
: base(ctx, Native.Z3_mk_int_symbol(ctx.nCtx, i))
{
Contract.Requires(ctx != null);
}
#if DEBUG
internal override void CheckNativeObject(IntPtr obj)
{
if ((Z3_symbol_kind)Native.Z3_get_symbol_kind(Context.nCtx, obj) != Z3_symbol_kind.Z3_INT_SYMBOL)
throw new Z3Exception("Symbol is not of integer kind");
base.CheckNativeObject(obj);
}
#endif
#endregion
}
}

163
src/api/dotnet/ListSort.cs Normal file
View file

@ -0,0 +1,163 @@
/*++
Copyright (c) 2012 Microsoft Corporation
Module Name:
ListSort.cs
Abstract:
Z3 Managed API: List Sorts
Author:
Christoph Wintersteiger (cwinter) 2012-11-23
Notes:
--*/
using System;
using System.Diagnostics.Contracts;
namespace Microsoft.Z3
{
/// <summary>
/// List sorts.
/// </summary>
[ContractVerification(true)]
public class ListSort : Sort
{
/// <summary>
/// The declaration of the nil function of this list sort.
/// </summary>
public FuncDecl NilDecl
{
get
{
Contract.Ensures(Contract.Result<FuncDecl>() != null);
return nilDecl;
}
}
/// <summary>
/// The empty list.
/// </summary>
public Expr Nil
{
get
{
Contract.Ensures(Contract.Result<Expr>() != null);
return nilConst;
}
}
/// <summary>
/// The declaration of the isNil function of this list sort.
/// </summary>
public FuncDecl IsNilDecl
{
get
{
Contract.Ensures(Contract.Result<FuncDecl>() != null);
return isNilDecl;
}
}
/// <summary>
/// The declaration of the cons function of this list sort.
/// </summary>
public FuncDecl ConsDecl
{
get
{
Contract.Ensures(Contract.Result<FuncDecl>() != null);
return consDecl;
}
}
/// <summary>
/// The declaration of the isCons function of this list sort.
/// </summary>
///
public FuncDecl IsConsDecl
{
get
{
Contract.Ensures(Contract.Result<FuncDecl>() != null);
return isConsDecl;
}
}
/// <summary>
/// The declaration of the head function of this list sort.
/// </summary>
public FuncDecl HeadDecl
{
get
{
Contract.Ensures(Contract.Result<FuncDecl>() != null);
return headDecl;
}
}
/// <summary>
/// The declaration of the tail function of this list sort.
/// </summary>
public FuncDecl TailDecl
{
get
{
Contract.Ensures(Contract.Result<FuncDecl>() != null);
return tailDecl;
}
}
#region Object Invariant
[ContractInvariantMethod]
private void ObjectInvariant()
{
Contract.Invariant(nilConst != null);
Contract.Invariant(nilDecl != null);
Contract.Invariant(isNilDecl != null);
Contract.Invariant(consDecl != null);
Contract.Invariant(isConsDecl != null);
Contract.Invariant(headDecl != null);
Contract.Invariant(tailDecl != null);
}
#endregion
#region Internal
readonly private FuncDecl nilDecl, isNilDecl, consDecl, isConsDecl, headDecl, tailDecl;
readonly private Expr nilConst;
internal ListSort(Context ctx, Symbol name, Sort elemSort)
: base(ctx)
{
Contract.Requires(ctx != null);
Contract.Requires(name != null);
Contract.Requires(elemSort != null);
IntPtr inil = IntPtr.Zero,
iisnil = IntPtr.Zero,
icons = IntPtr.Zero,
iiscons = IntPtr.Zero,
ihead = IntPtr.Zero,
itail = IntPtr.Zero;
NativeObject = Native.Z3_mk_list_sort(ctx.nCtx, name.NativeObject, elemSort.NativeObject,
ref inil, ref iisnil, ref icons, ref iiscons, ref ihead, ref itail);
nilDecl = new FuncDecl(ctx, inil);
isNilDecl = new FuncDecl(ctx, iisnil);
consDecl = new FuncDecl(ctx, icons);
isConsDecl = new FuncDecl(ctx, iiscons);
headDecl = new FuncDecl(ctx, ihead);
tailDecl = new FuncDecl(ctx, itail);
nilConst = ctx.MkConst(nilDecl);
}
#endregion
};
}

View file

@ -258,29 +258,56 @@
<Reference Include="System.Numerics" />
</ItemGroup>
<ItemGroup>
<Compile Include="AlgebraicNum.cs" />
<Compile Include="ApplyResult.cs" />
<Compile Include="ArithExpr.cs" />
<Compile Include="ArithSort.cs" />
<Compile Include="ArrayExpr.cs" />
<Compile Include="ArraySort.cs" />
<Compile Include="AST.cs" />
<Compile Include="ASTMap.cs" />
<Compile Include="ASTVector.cs" />
<Compile Include="BitVecExpr.cs" />
<Compile Include="BitVecNum.cs" />
<Compile Include="BitVecSort.cs" />
<Compile Include="BoolExpr.cs" />
<Compile Include="BoolSort.cs" />
<Compile Include="Constructor.cs" />
<Compile Include="DecRefQueue.cs" />
<Compile Include="ConstructorList.cs" />
<Compile Include="DatatypeExpr.cs" />
<Compile Include="DatatypeSort.cs" />
<Compile Include="IDecRefQueue.cs" />
<Compile Include="Enumerations.cs" />
<Compile Include="EnumSort.cs" />
<Compile Include="Expr.cs" />
<Compile Include="FiniteDomainSort.cs" />
<Compile Include="Fixedpoint.cs" />
<Compile Include="FuncDecl.cs" />
<Compile Include="FuncInterp.cs" />
<Compile Include="Goal.cs" />
<Compile Include="IntExpr.cs" />
<Compile Include="IntNum.cs" />
<Compile Include="IntSort.cs" />
<Compile Include="IntSymbol.cs" />
<Compile Include="ListSort.cs" />
<Compile Include="Model.cs" />
<Compile Include="Numeral.cs" />
<Compile Include="Params.cs" />
<Compile Include="ParamDescrs.cs" />
<Compile Include="Pattern.cs" />
<Compile Include="RatNum.cs" />
<Compile Include="RealExpr.cs" />
<Compile Include="RealSort.cs" />
<Compile Include="RelationSort.cs" />
<Compile Include="SetSort.cs" />
<Compile Include="Statistics.cs" />
<Compile Include="Status.cs" />
<Compile Include="Context.cs" />
<Compile Include="Probe.cs" />
<Compile Include="Solver.cs" />
<Compile Include="StringSymbol.cs" />
<Compile Include="Tactic.cs" />
<Compile Include="TupleSort.cs" />
<Compile Include="UninterpretedSort.cs" />
<Compile Include="Z3Exception.cs" />
<Compile Include="Log.cs" />
<Compile Include="Native.cs" />

View file

@ -1,403 +0,0 @@
<?xml version="1.0" encoding="utf-8"?>
<Project ToolsVersion="4.0" DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">
<PropertyGroup>
<Configuration Condition=" '$(Configuration)' == '' ">Debug</Configuration>
<Platform Condition=" '$(Platform)' == '' ">AnyCPU</Platform>
<ProductVersion>8.0.30703</ProductVersion>
<SchemaVersion>2.0</SchemaVersion>
<ProjectGuid>{EC3DB697-B734-42F7-9468-5B62821EEB5A}</ProjectGuid>
<OutputType>Library</OutputType>
<AppDesignerFolder>Properties</AppDesignerFolder>
<RootNamespace>Microsoft.Z3</RootNamespace>
<AssemblyName>Microsoft.Z3</AssemblyName>
<TargetFrameworkVersion>v3.5</TargetFrameworkVersion>
<FileAlignment>512</FileAlignment>
<TargetFrameworkProfile>Client</TargetFrameworkProfile>
<CodeContractsAssemblyMode>0</CodeContractsAssemblyMode>
</PropertyGroup>
<PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|AnyCPU' ">
<DebugSymbols>true</DebugSymbols>
<DebugType>full</DebugType>
<Optimize>false</Optimize>
<OutputPath>bin35\Debug\</OutputPath>
<DefineConstants>DEBUG;TRACE</DefineConstants>
<ErrorReport>prompt</ErrorReport>
<WarningLevel>4</WarningLevel>
<AllowUnsafeBlocks>true</AllowUnsafeBlocks>
<DocumentationFile>
</DocumentationFile>
<CodeContractsEnableRuntimeChecking>False</CodeContractsEnableRuntimeChecking>
<CodeContractsRuntimeOnlyPublicSurface>False</CodeContractsRuntimeOnlyPublicSurface>
<CodeContractsRuntimeThrowOnFailure>True</CodeContractsRuntimeThrowOnFailure>
<CodeContractsRuntimeCallSiteRequires>False</CodeContractsRuntimeCallSiteRequires>
<CodeContractsRuntimeSkipQuantifiers>False</CodeContractsRuntimeSkipQuantifiers>
<CodeContractsRunCodeAnalysis>True</CodeContractsRunCodeAnalysis>
<CodeContractsNonNullObligations>False</CodeContractsNonNullObligations>
<CodeContractsBoundsObligations>True</CodeContractsBoundsObligations>
<CodeContractsArithmeticObligations>True</CodeContractsArithmeticObligations>
<CodeContractsEnumObligations>False</CodeContractsEnumObligations>
<CodeContractsPointerObligations>False</CodeContractsPointerObligations>
<CodeContractsRedundantAssumptions>False</CodeContractsRedundantAssumptions>
<CodeContractsInferRequires>True</CodeContractsInferRequires>
<CodeContractsInferEnsures>False</CodeContractsInferEnsures>
<CodeContractsInferObjectInvariants>False</CodeContractsInferObjectInvariants>
<CodeContractsSuggestAssumptions>False</CodeContractsSuggestAssumptions>
<CodeContractsSuggestRequires>True</CodeContractsSuggestRequires>
<CodeContractsSuggestEnsures>False</CodeContractsSuggestEnsures>
<CodeContractsSuggestObjectInvariants>False</CodeContractsSuggestObjectInvariants>
<CodeContractsDisjunctiveRequires>True</CodeContractsDisjunctiveRequires>
<CodeContractsRunInBackground>True</CodeContractsRunInBackground>
<CodeContractsShowSquigglies>True</CodeContractsShowSquigglies>
<CodeContractsUseBaseLine>False</CodeContractsUseBaseLine>
<CodeContractsEmitXMLDocs>False</CodeContractsEmitXMLDocs>
<CodeContractsCustomRewriterAssembly />
<CodeContractsCustomRewriterClass />
<CodeContractsLibPaths />
<CodeContractsExtraRewriteOptions />
<CodeContractsExtraAnalysisOptions />
<CodeContractsBaseLineFile />
<CodeContractsCacheAnalysisResults>True</CodeContractsCacheAnalysisResults>
<CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>
<CodeContractsReferenceAssembly>%28none%29</CodeContractsReferenceAssembly>
<CodeContractsAnalysisWarningLevel>2</CodeContractsAnalysisWarningLevel>
</PropertyGroup>
<PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Release|AnyCPU' ">
<DebugType>pdbonly</DebugType>
<Optimize>true</Optimize>
<OutputPath>bin35\external\bin\</OutputPath>
<DefineConstants>FRAMEWORK_LT_4</DefineConstants>
<ErrorReport>prompt</ErrorReport>
<WarningLevel>4</WarningLevel>
<AllowUnsafeBlocks>true</AllowUnsafeBlocks>
<DocumentationFile>..\external\Microsoft.Z3.xml</DocumentationFile>
</PropertyGroup>
<PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'external|AnyCPU' ">
<OutputPath>bin35\external\bin\</OutputPath>
<AllowUnsafeBlocks>true</AllowUnsafeBlocks>
<DocumentationFile>..\external\Microsoft.Z3.xml</DocumentationFile>
<Optimize>true</Optimize>
<DebugType>pdbonly</DebugType>
<PlatformTarget>AnyCPU</PlatformTarget>
<CodeAnalysisLogFile>bin\Release\Microsoft.Z3.dll.CodeAnalysisLog.xml</CodeAnalysisLogFile>
<CodeAnalysisUseTypeNameInSuppression>true</CodeAnalysisUseTypeNameInSuppression>
<CodeAnalysisModuleSuppressionsFile>GlobalSuppressions.cs</CodeAnalysisModuleSuppressionsFile>
<ErrorReport>prompt</ErrorReport>
<CodeAnalysisRuleSet>MinimumRecommendedRules.ruleset</CodeAnalysisRuleSet>
<CodeAnalysisRuleSetDirectories>;C:\Program Files\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets</CodeAnalysisRuleSetDirectories>
<CodeAnalysisIgnoreBuiltInRuleSets>true</CodeAnalysisIgnoreBuiltInRuleSets>
<CodeAnalysisRuleDirectories>;C:\Program Files\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules</CodeAnalysisRuleDirectories>
<CodeAnalysisIgnoreBuiltInRules>true</CodeAnalysisIgnoreBuiltInRules>
<CodeAnalysisFailOnMissingRules>false</CodeAnalysisFailOnMissingRules>
<DefineConstants>FRAMEWORK_LT_4</DefineConstants>
</PropertyGroup>
<PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'external|Win32' ">
<OutputPath>bin35\external\bin\</OutputPath>
<AllowUnsafeBlocks>true</AllowUnsafeBlocks>
<DocumentationFile>..\external\Microsoft.Z3.xml</DocumentationFile>
<Optimize>true</Optimize>
<DebugType>pdbonly</DebugType>
<PlatformTarget>AnyCPU</PlatformTarget>
<CodeAnalysisLogFile>bin\Release\Microsoft.Z3.dll.CodeAnalysisLog.xml</CodeAnalysisLogFile>
<CodeAnalysisUseTypeNameInSuppression>true</CodeAnalysisUseTypeNameInSuppression>
<CodeAnalysisModuleSuppressionsFile>GlobalSuppressions.cs</CodeAnalysisModuleSuppressionsFile>
<ErrorReport>prompt</ErrorReport>
<CodeAnalysisRuleSet>MinimumRecommendedRules.ruleset</CodeAnalysisRuleSet>
<CodeAnalysisRuleSetDirectories>;C:\Program Files\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets</CodeAnalysisRuleSetDirectories>
<CodeAnalysisIgnoreBuiltInRuleSets>true</CodeAnalysisIgnoreBuiltInRuleSets>
<CodeAnalysisRuleDirectories>;C:\Program Files\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules</CodeAnalysisRuleDirectories>
<CodeAnalysisIgnoreBuiltInRules>true</CodeAnalysisIgnoreBuiltInRules>
<CodeAnalysisFailOnMissingRules>false</CodeAnalysisFailOnMissingRules>
<DefineConstants>FRAMEWORK_LT_4</DefineConstants>
</PropertyGroup>
<PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'Debug|x64'">
<DebugSymbols>true</DebugSymbols>
<OutputPath>bin35\x64\Debug\</OutputPath>
<DefineConstants>DEBUG;TRACE</DefineConstants>
<AllowUnsafeBlocks>true</AllowUnsafeBlocks>
<DebugType>full</DebugType>
<PlatformTarget>x64</PlatformTarget>
<CodeAnalysisLogFile>..\Debug\Microsoft.Z3.dll.CodeAnalysisLog.xml</CodeAnalysisLogFile>
<CodeAnalysisUseTypeNameInSuppression>true</CodeAnalysisUseTypeNameInSuppression>
<CodeAnalysisModuleSuppressionsFile>GlobalSuppressions.cs</CodeAnalysisModuleSuppressionsFile>
<ErrorReport>prompt</ErrorReport>
<CodeAnalysisRuleSet>MinimumRecommendedRules.ruleset</CodeAnalysisRuleSet>
<CodeAnalysisRuleSetDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets</CodeAnalysisRuleSetDirectories>
<CodeAnalysisIgnoreBuiltInRuleSets>true</CodeAnalysisIgnoreBuiltInRuleSets>
<CodeAnalysisRuleDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules</CodeAnalysisRuleDirectories>
<CodeAnalysisIgnoreBuiltInRules>true</CodeAnalysisIgnoreBuiltInRules>
<CodeContractsEnableRuntimeChecking>True</CodeContractsEnableRuntimeChecking>
<CodeContractsRuntimeOnlyPublicSurface>False</CodeContractsRuntimeOnlyPublicSurface>
<CodeContractsRuntimeThrowOnFailure>True</CodeContractsRuntimeThrowOnFailure>
<CodeContractsRuntimeCallSiteRequires>False</CodeContractsRuntimeCallSiteRequires>
<CodeContractsRuntimeSkipQuantifiers>False</CodeContractsRuntimeSkipQuantifiers>
<CodeContractsRunCodeAnalysis>False</CodeContractsRunCodeAnalysis>
<CodeContractsNonNullObligations>False</CodeContractsNonNullObligations>
<CodeContractsBoundsObligations>False</CodeContractsBoundsObligations>
<CodeContractsArithmeticObligations>False</CodeContractsArithmeticObligations>
<CodeContractsEnumObligations>False</CodeContractsEnumObligations>
<CodeContractsPointerObligations>False</CodeContractsPointerObligations>
<CodeContractsRedundantAssumptions>False</CodeContractsRedundantAssumptions>
<CodeContractsInferRequires>False</CodeContractsInferRequires>
<CodeContractsInferEnsures>False</CodeContractsInferEnsures>
<CodeContractsInferObjectInvariants>False</CodeContractsInferObjectInvariants>
<CodeContractsSuggestAssumptions>False</CodeContractsSuggestAssumptions>
<CodeContractsSuggestRequires>True</CodeContractsSuggestRequires>
<CodeContractsSuggestEnsures>False</CodeContractsSuggestEnsures>
<CodeContractsSuggestObjectInvariants>False</CodeContractsSuggestObjectInvariants>
<CodeContractsRunInBackground>True</CodeContractsRunInBackground>
<CodeContractsShowSquigglies>False</CodeContractsShowSquigglies>
<CodeContractsUseBaseLine>False</CodeContractsUseBaseLine>
<CodeContractsEmitXMLDocs>False</CodeContractsEmitXMLDocs>
<CodeContractsCustomRewriterAssembly />
<CodeContractsCustomRewriterClass />
<CodeContractsLibPaths />
<CodeContractsExtraRewriteOptions />
<CodeContractsExtraAnalysisOptions />
<CodeContractsBaseLineFile />
<CodeContractsCacheAnalysisResults>False</CodeContractsCacheAnalysisResults>
<CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>
<CodeContractsReferenceAssembly>%28none%29</CodeContractsReferenceAssembly>
<CodeContractsAnalysisWarningLevel>0</CodeContractsAnalysisWarningLevel>
</PropertyGroup>
<PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'Release|x64'">
<OutputPath>bin35\external\x64\</OutputPath>
<AllowUnsafeBlocks>true</AllowUnsafeBlocks>
<DocumentationFile>..\x64\external_64\Microsoft.Z3.xml</DocumentationFile>
<Optimize>true</Optimize>
<DebugType>pdbonly</DebugType>
<PlatformTarget>x64</PlatformTarget>
<CodeAnalysisLogFile>..\release\Microsoft.Z3.dll.CodeAnalysisLog.xml</CodeAnalysisLogFile>
<CodeAnalysisUseTypeNameInSuppression>true</CodeAnalysisUseTypeNameInSuppression>
<CodeAnalysisModuleSuppressionsFile>GlobalSuppressions.cs</CodeAnalysisModuleSuppressionsFile>
<ErrorReport>prompt</ErrorReport>
<CodeAnalysisRuleSet>MinimumRecommendedRules.ruleset</CodeAnalysisRuleSet>
<CodeAnalysisRuleSetDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets</CodeAnalysisRuleSetDirectories>
<CodeAnalysisIgnoreBuiltInRuleSets>true</CodeAnalysisIgnoreBuiltInRuleSets>
<CodeAnalysisRuleDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules</CodeAnalysisRuleDirectories>
<CodeContractsEnableRuntimeChecking>True</CodeContractsEnableRuntimeChecking>
<CodeContractsRuntimeOnlyPublicSurface>False</CodeContractsRuntimeOnlyPublicSurface>
<CodeContractsRuntimeThrowOnFailure>True</CodeContractsRuntimeThrowOnFailure>
<CodeContractsRuntimeCallSiteRequires>False</CodeContractsRuntimeCallSiteRequires>
<CodeContractsRuntimeSkipQuantifiers>False</CodeContractsRuntimeSkipQuantifiers>
<CodeContractsRunCodeAnalysis>True</CodeContractsRunCodeAnalysis>
<CodeContractsNonNullObligations>True</CodeContractsNonNullObligations>
<CodeContractsBoundsObligations>True</CodeContractsBoundsObligations>
<CodeContractsArithmeticObligations>False</CodeContractsArithmeticObligations>
<CodeContractsEnumObligations>False</CodeContractsEnumObligations>
<CodeContractsPointerObligations>False</CodeContractsPointerObligations>
<CodeContractsRedundantAssumptions>True</CodeContractsRedundantAssumptions>
<CodeContractsInferRequires>True</CodeContractsInferRequires>
<CodeContractsInferEnsures>False</CodeContractsInferEnsures>
<CodeContractsInferObjectInvariants>False</CodeContractsInferObjectInvariants>
<CodeContractsSuggestAssumptions>False</CodeContractsSuggestAssumptions>
<CodeContractsSuggestRequires>True</CodeContractsSuggestRequires>
<CodeContractsSuggestEnsures>False</CodeContractsSuggestEnsures>
<CodeContractsSuggestObjectInvariants>False</CodeContractsSuggestObjectInvariants>
<CodeContractsRunInBackground>True</CodeContractsRunInBackground>
<CodeContractsShowSquigglies>True</CodeContractsShowSquigglies>
<CodeContractsUseBaseLine>False</CodeContractsUseBaseLine>
<CodeContractsEmitXMLDocs>False</CodeContractsEmitXMLDocs>
<CodeContractsCustomRewriterAssembly />
<CodeContractsCustomRewriterClass />
<CodeContractsLibPaths />
<CodeContractsExtraRewriteOptions />
<CodeContractsExtraAnalysisOptions>-repro</CodeContractsExtraAnalysisOptions>
<CodeContractsBaseLineFile />
<CodeContractsCacheAnalysisResults>True</CodeContractsCacheAnalysisResults>
<CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>
<CodeContractsReferenceAssembly>%28none%29</CodeContractsReferenceAssembly>
<CodeContractsAnalysisWarningLevel>2</CodeContractsAnalysisWarningLevel>
</PropertyGroup>
<PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'external|x64'">
<OutputPath>bin35\external\x64</OutputPath>
<AllowUnsafeBlocks>true</AllowUnsafeBlocks>
<DocumentationFile>..\external\Microsoft.Z3.xml</DocumentationFile>
<Optimize>true</Optimize>
<DebugType>pdbonly</DebugType>
<PlatformTarget>x64</PlatformTarget>
<CodeAnalysisLogFile>bin\Release\Microsoft.Z3.dll.CodeAnalysisLog.xml</CodeAnalysisLogFile>
<CodeAnalysisUseTypeNameInSuppression>true</CodeAnalysisUseTypeNameInSuppression>
<CodeAnalysisModuleSuppressionsFile>GlobalSuppressions.cs</CodeAnalysisModuleSuppressionsFile>
<ErrorReport>prompt</ErrorReport>
<CodeAnalysisRuleSet>MinimumRecommendedRules.ruleset</CodeAnalysisRuleSet>
<CodeAnalysisRuleSetDirectories>;C:\Program Files\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets</CodeAnalysisRuleSetDirectories>
<CodeAnalysisIgnoreBuiltInRuleSets>true</CodeAnalysisIgnoreBuiltInRuleSets>
<CodeAnalysisRuleDirectories>;C:\Program Files\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules</CodeAnalysisRuleDirectories>
<CodeAnalysisIgnoreBuiltInRules>true</CodeAnalysisIgnoreBuiltInRules>
</PropertyGroup>
<PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'external_64|AnyCPU'">
<OutputPath>bin35\external_64\x64</OutputPath>
<AllowUnsafeBlocks>true</AllowUnsafeBlocks>
<DocumentationFile>..\x64\external_64\Microsoft.Z3.xml</DocumentationFile>
<DefineConstants>FRAMEWORK_LT_4</DefineConstants>
<Optimize>true</Optimize>
<DebugType>pdbonly</DebugType>
<PlatformTarget>AnyCPU</PlatformTarget>
<CodeAnalysisLogFile>bin\Release\Microsoft.Z3.dll.CodeAnalysisLog.xml</CodeAnalysisLogFile>
<CodeAnalysisUseTypeNameInSuppression>true</CodeAnalysisUseTypeNameInSuppression>
<CodeAnalysisModuleSuppressionsFile>GlobalSuppressions.cs</CodeAnalysisModuleSuppressionsFile>
<ErrorReport>prompt</ErrorReport>
<CodeAnalysisRuleSet>MinimumRecommendedRules.ruleset</CodeAnalysisRuleSet>
<CodeAnalysisRuleSetDirectories>;C:\Program Files\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets</CodeAnalysisRuleSetDirectories>
<CodeAnalysisIgnoreBuiltInRuleSets>true</CodeAnalysisIgnoreBuiltInRuleSets>
<CodeAnalysisRuleDirectories>;C:\Program Files\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules</CodeAnalysisRuleDirectories>
<CodeAnalysisIgnoreBuiltInRules>true</CodeAnalysisIgnoreBuiltInRules>
<CodeAnalysisFailOnMissingRules>false</CodeAnalysisFailOnMissingRules>
</PropertyGroup>
<PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'external_64|x64'">
<OutputPath>bin35\external_64\x64</OutputPath>
<AllowUnsafeBlocks>true</AllowUnsafeBlocks>
<DocumentationFile>..\x64\external_64\Microsoft.Z3.xml</DocumentationFile>
<Optimize>true</Optimize>
<DebugType>pdbonly</DebugType>
<PlatformTarget>x64</PlatformTarget>
<CodeAnalysisLogFile>bin\Release\Microsoft.Z3.dll.CodeAnalysisLog.xml</CodeAnalysisLogFile>
<CodeAnalysisUseTypeNameInSuppression>true</CodeAnalysisUseTypeNameInSuppression>
<CodeAnalysisModuleSuppressionsFile>GlobalSuppressions.cs</CodeAnalysisModuleSuppressionsFile>
<ErrorReport>prompt</ErrorReport>
<CodeAnalysisRuleSet>MinimumRecommendedRules.ruleset</CodeAnalysisRuleSet>
<CodeAnalysisRuleSetDirectories>;C:\Program Files\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets</CodeAnalysisRuleSetDirectories>
<CodeAnalysisIgnoreBuiltInRuleSets>true</CodeAnalysisIgnoreBuiltInRuleSets>
<CodeAnalysisRuleDirectories>;C:\Program Files\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules</CodeAnalysisRuleDirectories>
<CodeAnalysisIgnoreBuiltInRules>true</CodeAnalysisIgnoreBuiltInRules>
<CodeAnalysisFailOnMissingRules>false</CodeAnalysisFailOnMissingRules>
<CodeContractsEnableRuntimeChecking>True</CodeContractsEnableRuntimeChecking>
<CodeContractsRuntimeOnlyPublicSurface>False</CodeContractsRuntimeOnlyPublicSurface>
<CodeContractsRuntimeThrowOnFailure>True</CodeContractsRuntimeThrowOnFailure>
<CodeContractsRuntimeCallSiteRequires>False</CodeContractsRuntimeCallSiteRequires>
<CodeContractsRuntimeSkipQuantifiers>False</CodeContractsRuntimeSkipQuantifiers>
<CodeContractsRunCodeAnalysis>False</CodeContractsRunCodeAnalysis>
<CodeContractsNonNullObligations>False</CodeContractsNonNullObligations>
<CodeContractsBoundsObligations>False</CodeContractsBoundsObligations>
<CodeContractsArithmeticObligations>False</CodeContractsArithmeticObligations>
<CodeContractsEnumObligations>False</CodeContractsEnumObligations>
<CodeContractsPointerObligations>False</CodeContractsPointerObligations>
<CodeContractsRedundantAssumptions>False</CodeContractsRedundantAssumptions>
<CodeContractsInferRequires>False</CodeContractsInferRequires>
<CodeContractsInferEnsures>False</CodeContractsInferEnsures>
<CodeContractsInferObjectInvariants>False</CodeContractsInferObjectInvariants>
<CodeContractsSuggestAssumptions>False</CodeContractsSuggestAssumptions>
<CodeContractsSuggestRequires>True</CodeContractsSuggestRequires>
<CodeContractsSuggestEnsures>False</CodeContractsSuggestEnsures>
<CodeContractsSuggestObjectInvariants>False</CodeContractsSuggestObjectInvariants>
<CodeContractsRunInBackground>True</CodeContractsRunInBackground>
<CodeContractsShowSquigglies>False</CodeContractsShowSquigglies>
<CodeContractsUseBaseLine>False</CodeContractsUseBaseLine>
<CodeContractsEmitXMLDocs>False</CodeContractsEmitXMLDocs>
<CodeContractsCustomRewriterAssembly />
<CodeContractsCustomRewriterClass />
<CodeContractsLibPaths />
<CodeContractsExtraRewriteOptions />
<CodeContractsExtraAnalysisOptions />
<CodeContractsBaseLineFile />
<CodeContractsCacheAnalysisResults>False</CodeContractsCacheAnalysisResults>
<CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>
<CodeContractsReferenceAssembly>%28none%29</CodeContractsReferenceAssembly>
<CodeContractsAnalysisWarningLevel>0</CodeContractsAnalysisWarningLevel>
<DefineConstants>FRAMEWORK_LT_4</DefineConstants>
</PropertyGroup>
<PropertyGroup>
<SignAssembly>true</SignAssembly>
</PropertyGroup>
<PropertyGroup>
<AssemblyOriginatorKeyFile>z3.snk</AssemblyOriginatorKeyFile>
</PropertyGroup>
<PropertyGroup>
<DelaySign>false</DelaySign>
</PropertyGroup>
<PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'Release_delaysign|AnyCPU'">
<OutputPath>bin35\Release_delaysign\</OutputPath>
<AllowUnsafeBlocks>true</AllowUnsafeBlocks>
<DocumentationFile>..\Release_delaysign\Microsoft.Z3.xml</DocumentationFile>
<Optimize>true</Optimize>
<DebugType>pdbonly</DebugType>
<PlatformTarget>AnyCPU</PlatformTarget>
<CodeAnalysisLogFile>..\release\Microsoft.Z3.dll.CodeAnalysisLog.xml</CodeAnalysisLogFile>
<CodeAnalysisUseTypeNameInSuppression>true</CodeAnalysisUseTypeNameInSuppression>
<CodeAnalysisModuleSuppressionsFile>GlobalSuppressions.cs</CodeAnalysisModuleSuppressionsFile>
<ErrorReport>prompt</ErrorReport>
<CodeAnalysisRuleSet>MinimumRecommendedRules.ruleset</CodeAnalysisRuleSet>
<CodeAnalysisRuleSetDirectories>;C:\Program Files\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets</CodeAnalysisRuleSetDirectories>
<CodeAnalysisIgnoreBuiltInRuleSets>true</CodeAnalysisIgnoreBuiltInRuleSets>
<CodeAnalysisRuleDirectories>;C:\Program Files\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules</CodeAnalysisRuleDirectories>
<CodeAnalysisIgnoreBuiltInRules>true</CodeAnalysisIgnoreBuiltInRules>
<DefineConstants>DELAYSIGN</DefineConstants>
</PropertyGroup>
<PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'Release_delaysign|x64'">
<OutputPath>bin\x64\Release_delaysign\</OutputPath>
<AllowUnsafeBlocks>true</AllowUnsafeBlocks>
<DocumentationFile>..\x64\external_64\Microsoft.Z3.xml</DocumentationFile>
<Optimize>true</Optimize>
<DebugType>pdbonly</DebugType>
<PlatformTarget>x64</PlatformTarget>
<CodeAnalysisLogFile>..\release\Microsoft.Z3.dll.CodeAnalysisLog.xml</CodeAnalysisLogFile>
<CodeAnalysisUseTypeNameInSuppression>true</CodeAnalysisUseTypeNameInSuppression>
<CodeAnalysisModuleSuppressionsFile>GlobalSuppressions.cs</CodeAnalysisModuleSuppressionsFile>
<ErrorReport>prompt</ErrorReport>
<CodeAnalysisRuleSet>MinimumRecommendedRules.ruleset</CodeAnalysisRuleSet>
<CodeAnalysisRuleSetDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets</CodeAnalysisRuleSetDirectories>
<CodeAnalysisIgnoreBuiltInRuleSets>true</CodeAnalysisIgnoreBuiltInRuleSets>
<CodeAnalysisRuleDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules;C:\Program Files\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules</CodeAnalysisRuleDirectories>
<CodeAnalysisIgnoreBuiltInRules>true</CodeAnalysisIgnoreBuiltInRules>
</PropertyGroup>
<ItemGroup>
<Reference Include="Microsoft.Contracts, Version=1.0.0.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">
<SpecificVersion>False</SpecificVersion>
<HintPath>..\..\..\..\Program Files\Microsoft\Contracts\Contracts\v3.5\Microsoft.Contracts.dll</HintPath>
</Reference>
<Reference Include="System" />
<Reference Include="System.Core" />
</ItemGroup>
<ItemGroup>
<Compile Include="ApplyResult.cs" />
<Compile Include="AST.cs" />
<Compile Include="ASTMap.cs" />
<Compile Include="ASTVector.cs" />
<Compile Include="Constructor.cs" />
<Compile Include="DecRefQueue.cs" />
<Compile Include="Enumerations.cs" />
<Compile Include="Expr.cs" />
<Compile Include="Fixedpoint.cs" />
<Compile Include="FuncDecl.cs" />
<Compile Include="FuncInterp.cs" />
<Compile Include="Goal.cs" />
<Compile Include="Model.cs" />
<Compile Include="Numeral.cs" />
<Compile Include="Params.cs" />
<Compile Include="Pattern.cs" />
<Compile Include="Statistics.cs" />
<Compile Include="Status.cs" />
<Compile Include="Context.cs" />
<Compile Include="Probe.cs" />
<Compile Include="Solver.cs" />
<Compile Include="Tactic.cs" />
<Compile Include="Z3Exception.cs" />
<Compile Include="Log.cs" />
<Compile Include="Native.cs" />
<Compile Include="Properties\AssemblyInfo.cs" />
<Compile Include="Quantifier.cs" />
<Compile Include="Sort.cs" />
<Compile Include="Symbol.cs" />
<Compile Include="Util.cs" />
<Compile Include="Version.cs" />
<Compile Include="Z3Object.cs" />
</ItemGroup>
<ItemGroup>
<WCFMetadata Include="Service References\" />
</ItemGroup>
<ItemGroup>
<None Include="z3.snk" />
</ItemGroup>
<Import Project="$(MSBuildToolsPath)\Microsoft.CSharp.targets" />
<PropertyGroup>
<PostBuildEvent>
</PostBuildEvent>
</PropertyGroup>
<!-- To modify your build process, add your task inside one of the targets below and uncomment it.
Other similar extension points exist, see Microsoft.Common.targets.
<Target Name="BeforeBuild">
</Target>
<Target Name="AfterBuild">
</Target>
-->
</Project>

View file

@ -289,7 +289,7 @@ namespace Microsoft.Z3
Contract.Requires(ctx != null);
}
internal class DecRefQueue : Z3.DecRefQueue
internal class DecRefQueue : IDecRefQueue
{
public override void IncRef(Context ctx, IntPtr obj)
{

View file

@ -1,344 +0,0 @@
/*++
Copyright (c) 2012 Microsoft Corporation
Module Name:
Numeral.cs
Abstract:
Z3 Managed API: Numerals
Author:
Christoph Wintersteiger (cwinter) 2012-03-20
Notes:
--*/
using System;
using System.Diagnostics.Contracts;
#if !FRAMEWORK_LT_4
using System.Numerics;
#endif
namespace Microsoft.Z3
{
/// <summary>
/// Integer Numerals
/// </summary>
[ContractVerification(true)]
public class IntNum : IntExpr
{
#region Internal
internal IntNum(Context ctx, IntPtr obj)
: base(ctx, obj)
{
Contract.Requires(ctx != null);
}
#endregion
/// <summary>
/// Retrieve the 64-bit unsigned integer value.
/// </summary>
public UInt64 UInt64
{
get
{
UInt64 res = 0;
if (Native.Z3_get_numeral_uint64(Context.nCtx, NativeObject, ref res) == 0)
throw new Z3Exception("Numeral is not a 64 bit unsigned");
return res;
}
}
/// <summary>
/// Retrieve the int value.
/// </summary>
public int Int
{
get
{
int res = 0;
if (Native.Z3_get_numeral_int(Context.nCtx, NativeObject, ref res) == 0)
throw new Z3Exception("Numeral is not an int");
return res;
}
}
/// <summary>
/// Retrieve the 64-bit int value.
/// </summary>
public Int64 Int64
{
get
{
Int64 res = 0;
if (Native.Z3_get_numeral_int64(Context.nCtx, NativeObject, ref res) == 0)
throw new Z3Exception("Numeral is not an int64");
return res;
}
}
/// <summary>
/// Retrieve the int value.
/// </summary>
public uint UInt
{
get
{
uint res = 0;
if (Native.Z3_get_numeral_uint(Context.nCtx, NativeObject, ref res) == 0)
throw new Z3Exception("Numeral is not a uint");
return res;
}
}
#if !FRAMEWORK_LT_4
/// <summary>
/// Retrieve the BigInteger value.
/// </summary>
public BigInteger BigInteger
{
get
{
return BigInteger.Parse(this.ToString());
}
}
#endif
/// <summary>
/// Returns a string representation of the numeral.
/// </summary>
public override string ToString()
{
return Native.Z3_get_numeral_string(Context.nCtx, NativeObject);
}
}
/// <summary>
/// Rational Numerals
/// </summary>
[ContractVerification(true)]
public class RatNum : RealExpr
{
/// <summary>
/// The numerator of a rational numeral.
/// </summary>
public IntNum Numerator
{
get {
Contract.Ensures(Contract.Result<IntNum>() != null);
return new IntNum(Context, Native.Z3_get_numerator(Context.nCtx, NativeObject)); }
}
/// <summary>
/// The denominator of a rational numeral.
/// </summary>
public IntNum Denominator
{
get {
Contract.Ensures(Contract.Result<IntNum>() != null);
return new IntNum(Context, Native.Z3_get_denominator(Context.nCtx, NativeObject)); }
}
#if !FRAMEWORK_LT_4
/// <summary>
/// Converts the numerator of the rational to a BigInteger
/// </summary>
public BigInteger BigIntNumerator
{
get
{
IntNum n = Numerator;
return BigInteger.Parse(n.ToString());
}
}
/// <summary>
/// Converts the denominator of the rational to a BigInteger
/// </summary>
public BigInteger BigIntDenominator
{
get
{
IntNum n = Denominator;
return BigInteger.Parse(n.ToString());
}
}
#endif
/// <summary>
/// Returns a string representation in decimal notation.
/// </summary>
/// <remarks>The result has at most <paramref name="precision"/> decimal places.</remarks>
public string ToDecimalString(uint precision)
{
return Native.Z3_get_numeral_decimal_string(Context.nCtx, NativeObject, precision);
}
/// <summary>
/// Returns a string representation of the numeral.
/// </summary>
public override string ToString()
{
return Native.Z3_get_numeral_string(Context.nCtx, NativeObject);
}
#region Internal
internal RatNum(Context ctx, IntPtr obj)
: base(ctx, obj)
{
Contract.Requires(ctx != null);
}
#endregion
}
/// <summary>
/// Bit-vector numerals
/// </summary>
[ContractVerification(true)]
public class BitVecNum : BitVecExpr
{
/// <summary>
/// Retrieve the 64-bit unsigned integer value.
/// </summary>
public UInt64 UInt64
{
get
{
UInt64 res = 0;
if (Native.Z3_get_numeral_uint64(Context.nCtx, NativeObject, ref res) == 0)
throw new Z3Exception("Numeral is not a 64 bit unsigned");
return res;
}
}
/// <summary>
/// Retrieve the int value.
/// </summary>
public int Int
{
get
{
int res = 0;
if (Native.Z3_get_numeral_int(Context.nCtx, NativeObject, ref res) == 0)
throw new Z3Exception("Numeral is not an int");
return res;
}
}
/// <summary>
/// Retrieve the 64-bit int value.
/// </summary>
public Int64 Int64
{
get
{
Int64 res = 0;
if (Native.Z3_get_numeral_int64(Context.nCtx, NativeObject, ref res) == 0)
throw new Z3Exception("Numeral is not an int64");
return res;
}
}
/// <summary>
/// Retrieve the int value.
/// </summary>
public uint UInt
{
get
{
uint res = 0;
if (Native.Z3_get_numeral_uint(Context.nCtx, NativeObject, ref res) == 0)
throw new Z3Exception("Numeral is not a uint");
return res;
}
}
#if !FRAMEWORK_LT_4
/// <summary>
/// Retrieve the BigInteger value.
/// </summary>
public BigInteger BigInteger
{
get
{
return BigInteger.Parse(this.ToString());
}
}
#endif
/// <summary>
/// Returns a string representation of the numeral.
/// </summary>
public override string ToString()
{
return Native.Z3_get_numeral_string(Context.nCtx, NativeObject);
}
#region Internal
internal BitVecNum(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); }
#endregion
}
/// <summary>
/// Algebraic numbers
/// </summary>
[ContractVerification(true)]
public class AlgebraicNum : ArithExpr
{
/// <summary>
/// Return a upper bound for a given real algebraic number.
/// The interval isolating the number is smaller than 1/10^<paramref name="precision"/>.
/// <seealso cref="Expr.IsAlgebraicNumber"/>
/// </summary>
/// <param name="precision">the precision of the result</param>
/// <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));
}
/// <summary>
/// Return a lower bound for the given real algebraic number.
/// The interval isolating the number is smaller than 1/10^<paramref name="precision"/>.
/// <seealso cref="Expr.IsAlgebraicNumber"/>
/// </summary>
/// <param name="precision"></param>
/// <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));
}
/// <summary>
/// Returns a string representation in decimal notation.
/// </summary>
/// <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);
}
#region Internal
internal AlgebraicNum(Context ctx, IntPtr obj)
: base(ctx, obj)
{
Contract.Requires(ctx != null);
}
#endregion
}
}

View file

@ -85,7 +85,7 @@ namespace Microsoft.Z3
Contract.Requires(ctx != null);
}
internal class DecRefQueue : Z3.DecRefQueue
internal class DecRefQueue : IDecRefQueue
{
public override void IncRef(Context ctx, IntPtr obj)
{

View file

@ -118,7 +118,7 @@ namespace Microsoft.Z3
Contract.Requires(ctx != null);
}
internal class DecRefQueue : Z3.DecRefQueue
internal class DecRefQueue : IDecRefQueue
{
public override void IncRef(Context ctx, IntPtr obj)
{

View file

@ -49,10 +49,15 @@ namespace Microsoft.Z3
/// <summary>
/// Apply the probe to a goal.
/// </summary>
public double this[Goal g] { get {
Contract.Requires(g != null);
public double this[Goal g]
{
get
{
Contract.Requires(g != null);
return Apply(g); } }
return Apply(g);
}
}
#region Internal
internal Probe(Context ctx, IntPtr obj)
@ -66,7 +71,7 @@ namespace Microsoft.Z3
Contract.Requires(ctx != null);
}
internal class DecRefQueue : Z3.DecRefQueue
internal class DecRefQueue : IDecRefQueue
{
public override void IncRef(Context ctx, IntPtr obj)
{
@ -77,7 +82,7 @@ namespace Microsoft.Z3
{
Native.Z3_probe_dec_ref(ctx.nCtx, obj);
}
};
};
internal override void IncRef(IntPtr o)
{

View file

@ -149,18 +149,17 @@ namespace Microsoft.Z3
/// </summary>
public BoolExpr Body
{
get {
get
{
Contract.Ensures(Contract.Result<BoolExpr>() != null);
return new BoolExpr(Context, Native.Z3_get_quantifier_body(Context.nCtx, NativeObject)); }
return new BoolExpr(Context, Native.Z3_get_quantifier_body(Context.nCtx, NativeObject));
}
}
#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
)
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)
{
Contract.Requires(ctx != null);
@ -187,7 +186,7 @@ namespace Microsoft.Z3
if (noPatterns == null && quantifierID == null && skolemID == null)
{
NativeObject = Native.Z3_mk_quantifier(ctx.nCtx, (isForall) ? 1 : 0, weight,
AST.ArrayLength(patterns), AST.ArrayToNative(patterns),
AST.ArrayLength(patterns), AST.ArrayToNative(patterns),
AST.ArrayLength(sorts), AST.ArrayToNative(sorts),
Symbol.ArrayToNative(names),
body.NativeObject);
@ -205,16 +204,13 @@ 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
)
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)
{
Contract.Requires(ctx != null);
Contract.Requires(body != null);
Contract.Requires(patterns == null || Contract.ForAll(patterns, p => p != 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));
@ -222,7 +218,7 @@ namespace Microsoft.Z3
Context.CheckContextMatch(patterns);
//Context.CheckContextMatch(bound);
Context.CheckContextMatch(body);
if (noPatterns == null && quantifierID == null && skolemID == null)
{
NativeObject = Native.Z3_mk_quantifier_const(ctx.nCtx, (isForall) ? 1 : 0, weight,
@ -244,14 +240,14 @@ namespace Microsoft.Z3
internal Quantifier(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); }
#if DEBUG
#if DEBUG
internal override void CheckNativeObject(IntPtr obj)
{
if ((Z3_ast_kind)Native.Z3_get_ast_kind(Context.nCtx, obj) != Z3_ast_kind.Z3_QUANTIFIER_AST)
throw new Z3Exception("Underlying object is not a quantifier");
base.CheckNativeObject(obj);
}
#endif
#endif
#endregion
}
}

111
src/api/dotnet/RatNum.cs Normal file
View file

@ -0,0 +1,111 @@
/*++
Copyright (c) 2012 Microsoft Corporation
Module Name:
IntNum.cs
Abstract:
Z3 Managed API: Int Numerals
Author:
Christoph Wintersteiger (cwinter) 2012-03-20
Notes:
--*/
using System;
using System.Diagnostics.Contracts;
#if !FRAMEWORK_LT_4
using System.Numerics;
#endif
namespace Microsoft.Z3
{
/// <summary>
/// Rational Numerals
/// </summary>
[ContractVerification(true)]
public class RatNum : RealExpr
{
/// <summary>
/// The numerator of a rational numeral.
/// </summary>
public IntNum Numerator
{
get
{
Contract.Ensures(Contract.Result<IntNum>() != null);
return new IntNum(Context, Native.Z3_get_numerator(Context.nCtx, NativeObject));
}
}
/// <summary>
/// The denominator of a rational numeral.
/// </summary>
public IntNum Denominator
{
get
{
Contract.Ensures(Contract.Result<IntNum>() != null);
return new IntNum(Context, Native.Z3_get_denominator(Context.nCtx, NativeObject));
}
}
#if !FRAMEWORK_LT_4
/// <summary>
/// Converts the numerator of the rational to a BigInteger
/// </summary>
public BigInteger BigIntNumerator
{
get
{
IntNum n = Numerator;
return BigInteger.Parse(n.ToString());
}
}
/// <summary>
/// Converts the denominator of the rational to a BigInteger
/// </summary>
public BigInteger BigIntDenominator
{
get
{
IntNum n = Denominator;
return BigInteger.Parse(n.ToString());
}
}
#endif
/// <summary>
/// Returns a string representation in decimal notation.
/// </summary>
/// <remarks>The result has at most <paramref name="precision"/> decimal places.</remarks>
public string ToDecimalString(uint precision)
{
return Native.Z3_get_numeral_decimal_string(Context.nCtx, NativeObject, precision);
}
/// <summary>
/// Returns a string representation of the numeral.
/// </summary>
public override string ToString()
{
return Native.Z3_get_numeral_string(Context.nCtx, NativeObject);
}
#region Internal
internal RatNum(Context ctx, IntPtr obj)
: base(ctx, obj)
{
Contract.Requires(ctx != null);
}
#endregion
}
}

View file

@ -0,0 +1,47 @@
/*++
Copyright (<c>) 2012 Microsoft Corporation
Module Name:
RealExpr.cs
Abstract:
Z3 Managed API: Real Expressions
Author:
Christoph Wintersteiger (cwinter) 2012-11-23
Notes:
--*/
using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;
using System.Diagnostics.Contracts;
namespace Microsoft.Z3
{
/// <summary>
/// Real expressions
/// </summary>
public class RealExpr : ArithExpr
{
#region Internal
/// <summary> Constructor for RealExpr </summary>
internal protected RealExpr(Context ctx)
: base(ctx)
{
Contract.Requires(ctx != null);
}
internal RealExpr(Context ctx, IntPtr obj)
: base(ctx, obj)
{
Contract.Requires(ctx != null);
}
#endregion
}
}

View file

@ -0,0 +1,43 @@
/*++
Copyright (c) 2012 Microsoft Corporation
Module Name:
RealSort.cs
Abstract:
Z3 Managed API: Real Sorts
Author:
Christoph Wintersteiger (cwinter) 2012-11-23
Notes:
--*/
using System;
using System.Diagnostics.Contracts;
namespace Microsoft.Z3
{
/// <summary>
/// A real sort
/// </summary>
public class RealSort : ArithSort
{
#region Internal
internal RealSort(Context ctx, IntPtr obj)
: base(ctx, obj)
{
Contract.Requires(ctx != null);
}
internal RealSort(Context ctx)
: base(ctx, Native.Z3_mk_real_sort(ctx.nCtx))
{
Contract.Requires(ctx != null);
}
#endregion
}
}

View file

@ -0,0 +1,69 @@
/*++
Copyright (c) 2012 Microsoft Corporation
Module Name:
RelationSort.cs
Abstract:
Z3 Managed API: Relation Sorts
Author:
Christoph Wintersteiger (cwinter) 2012-11-23
Notes:
--*/
using System;
using System.Diagnostics.Contracts;
namespace Microsoft.Z3
{
/// <summary>
/// Relation sorts.
/// </summary>
[ContractVerification(true)]
public class RelationSort : Sort
{
/// <summary>
/// The arity of the relation sort.
/// </summary>
public uint Arity
{
get { return Native.Z3_get_relation_arity(Context.nCtx, NativeObject); }
}
/// <summary>
/// The sorts of the columns of the relation sort.
/// </summary>
public Sort[] ColumnSorts
{
get
{
Contract.Ensures(Contract.Result<Sort[]>() != null);
if (m_columnSorts != null)
return m_columnSorts;
uint n = Arity;
Sort[] res = new Sort[n];
for (uint i = 0; i < n; i++)
res[i] = Sort.Create(Context, Native.Z3_get_relation_column(Context.nCtx, NativeObject, i));
return res;
}
}
#region Internal
private Sort[] m_columnSorts = null;
internal RelationSort(Context ctx, IntPtr obj)
: base(ctx, obj)
{
Contract.Requires(ctx != null);
}
#endregion
}
}

45
src/api/dotnet/SetSort.cs Normal file
View file

@ -0,0 +1,45 @@
/*++
Copyright (c) 2012 Microsoft Corporation
Module Name:
SetSort.cs
Abstract:
Z3 Managed API: Set Sorts
Author:
Christoph Wintersteiger (cwinter) 2012-11-23
Notes:
--*/
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);
}
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);
}
#endregion
}
}

View file

@ -272,7 +272,7 @@ namespace Microsoft.Z3
Contract.Requires(ctx != null);
}
internal class DecRefQueue : Z3.DecRefQueue
internal class DecRefQueue : IDecRefQueue
{
public override void IncRef(Context ctx, IntPtr obj)
{

View file

@ -98,9 +98,11 @@ namespace Microsoft.Z3
/// </summary>
public Symbol Name
{
get {
get
{
Contract.Ensures(Contract.Result<Symbol>() != null);
return Symbol.Create(Context, Native.Z3_get_sort_name(Context.nCtx, NativeObject)); }
return Symbol.Create(Context, Native.Z3_get_sort_name(Context.nCtx, NativeObject));
}
}
/// <summary>
@ -118,14 +120,14 @@ namespace Microsoft.Z3
internal protected Sort(Context ctx) : base(ctx) { Contract.Requires(ctx != null); }
internal Sort(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); }
#if DEBUG
#if DEBUG
internal override void CheckNativeObject(IntPtr obj)
{
if (Native.Z3_get_ast_kind(Context.nCtx, obj) != (uint)Z3_ast_kind.Z3_SORT_AST)
throw new Z3Exception("Underlying object is not a sort");
base.CheckNativeObject(obj);
}
#endif
#endif
[ContractVerification(true)]
new internal static Sort Create(Context ctx, IntPtr obj)
@ -149,597 +151,5 @@ namespace Microsoft.Z3
}
}
#endregion
}
/// <summary>
/// A Boolean sort.
/// </summary>
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); }
#endregion
};
/// <summary>
/// An arithmetic sort, i.e., Int or Real.
/// </summary>
public class ArithSort : Sort
{
#region Internal
internal ArithSort(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); }
#endregion
};
/// <summary>
/// An Integer sort
/// </summary>
public class IntSort : ArithSort
{
#region Internal
internal IntSort(Context ctx, IntPtr obj)
: base(ctx, obj)
{
Contract.Requires(ctx != null);
}
internal IntSort(Context ctx)
: base(ctx, Native.Z3_mk_int_sort(ctx.nCtx))
{
Contract.Requires(ctx != null);
}
#endregion
}
/// <summary>
/// A real sort
/// </summary>
public class RealSort : ArithSort
{
#region Internal
internal RealSort(Context ctx, IntPtr obj)
: base(ctx, obj)
{
Contract.Requires(ctx != null);
}
internal RealSort(Context ctx)
: base(ctx, Native.Z3_mk_real_sort(ctx.nCtx))
{
Contract.Requires(ctx != null);
}
#endregion
}
/// <summary>
/// Bit-vector sorts.
/// </summary>
public class BitVecSort : Sort
{
/// <summary>
/// The size of the bit-vector sort.
/// </summary>
public uint Size
{
get { return Native.Z3_get_bv_sort_size(Context.nCtx, NativeObject); }
}
#region Internal
internal BitVecSort(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); }
internal BitVecSort(Context ctx, uint size) : base(ctx, Native.Z3_mk_bv_sort(ctx.nCtx, size)) { Contract.Requires(ctx != null); }
#endregion
};
/// <summary>
/// Array sorts.
/// </summary>
[ContractVerification(true)]
public class ArraySort : Sort
{
/// <summary>
/// The domain of the array sort.
/// </summary>
public Sort Domain
{
get {
Contract.Ensures(Contract.Result<Sort>() != null);
return Sort.Create(Context, Native.Z3_get_array_sort_domain(Context.nCtx, NativeObject)); }
}
/// <summary>
/// The range of the array sort.
/// </summary>
public Sort Range
{
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, 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);
}
#endregion
};
/// <summary>
/// Datatype sorts.
/// </summary>
[ContractVerification(true)]
public class DatatypeSort : Sort
{
/// <summary>
/// The number of constructors of the datatype sort.
/// </summary>
public uint NumConstructors
{
get { return Native.Z3_get_datatype_sort_num_constructors(Context.nCtx, NativeObject); }
}
/// <summary>
/// The constructors.
/// </summary>
public FuncDecl[] Constructors
{
get
{
Contract.Ensures(Contract.Result<FuncDecl[]>() != null);
uint n = NumConstructors;
FuncDecl[] res = new FuncDecl[n];
for (uint i = 0; i < n; i++)
res[i] = new FuncDecl(Context, Native.Z3_get_datatype_sort_constructor(Context.nCtx, NativeObject, i));
return res;
}
}
/// <summary>
/// The recognizers.
/// </summary>
public FuncDecl[] Recognizers
{
get
{
Contract.Ensures(Contract.Result<FuncDecl[]>() != null);
uint n = NumConstructors;
FuncDecl[] res = new FuncDecl[n];
for (uint i = 0; i < n; i++)
res[i] = new FuncDecl(Context, Native.Z3_get_datatype_sort_recognizer(Context.nCtx, NativeObject, i));
return res;
}
}
/// <summary>
/// The constructor accessors.
/// </summary>
public FuncDecl[][] Accessors
{
get
{
Contract.Ensures(Contract.Result<FuncDecl[][]>() != null);
uint n = NumConstructors;
FuncDecl[][] res = new FuncDecl[n][];
for (uint i = 0; i < n; i++)
{
FuncDecl fd = new FuncDecl(Context, Native.Z3_get_datatype_sort_constructor(Context.nCtx, NativeObject, i));
uint ds = fd.DomainSize;
FuncDecl[] tmp = new FuncDecl[ds];
for (uint j = 0; j < ds; j++)
tmp[j] = new FuncDecl(Context, Native.Z3_get_datatype_sort_constructor_accessor(Context.nCtx, NativeObject, i, j));
res[i] = tmp;
}
return res;
}
}
#region Internal
internal DatatypeSort(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(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);
}
#endregion
};
/// <summary>
/// Uninterpreted Sorts
/// </summary>
public class UninterpretedSort : Sort
{
#region Internal
internal UninterpretedSort(Context ctx, IntPtr obj)
: base(ctx, obj)
{
Contract.Requires(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);
}
#endregion
}
/// <summary>
/// Tuple sorts.
/// </summary>
[ContractVerification(true)]
public class TupleSort : Sort
{
/// <summary>
/// The constructor function of the tuple.
/// </summary>
public FuncDecl MkDecl
{
get {
Contract.Ensures(Contract.Result<FuncDecl>() != null);
return new FuncDecl(Context, Native.Z3_get_tuple_sort_mk_decl(Context.nCtx, NativeObject)); }
}
/// <summary>
/// The number of fields in the tuple.
/// </summary>
public uint NumFields
{
get { return Native.Z3_get_tuple_sort_num_fields(Context.nCtx, NativeObject); }
}
/// <summary>
/// The field declarations.
/// </summary>
public FuncDecl[] FieldDecls
{
get
{
Contract.Ensures(Contract.Result<FuncDecl[]>() != null);
uint n = NumFields;
FuncDecl[] res = new FuncDecl[n];
for (uint i = 0; i < n; i++)
res[i] = new FuncDecl(Context, Native.Z3_get_tuple_sort_field_decl(Context.nCtx, NativeObject, i));
return res;
}
}
#region Internal
internal TupleSort(Context ctx, Symbol name, uint numFields, Symbol[] fieldNames, Sort[] fieldSorts)
: base(ctx)
{
Contract.Requires(ctx != null);
Contract.Requires(name != null);
IntPtr t = IntPtr.Zero;
NativeObject = Native.Z3_mk_tuple_sort(ctx.nCtx, name.NativeObject, numFields,
Symbol.ArrayToNative(fieldNames), AST.ArrayToNative(fieldSorts),
ref t, new IntPtr[numFields]);
}
#endregion
};
/// <summary>
/// Enumeration sorts.
/// </summary>
[ContractVerification(true)]
public class EnumSort : Sort
{
/// <summary>
/// The function declarations of the constants in the enumeration.
/// </summary>
public FuncDecl[] ConstDecls
{
get {
Contract.Ensures(Contract.Result<FuncDecl[]>() != null);
return _constdecls; }
}
/// <summary>
/// The constants in the enumeration.
/// </summary>
public Expr[] Consts
{
get {
Contract.Ensures(Contract.Result<Expr[]>() != null);
return _consts; }
}
/// <summary>
/// The test predicates for the constants in the enumeration.
/// </summary>
public FuncDecl[] TesterDecls
{
get {
Contract.Ensures(Contract.Result<FuncDecl[]>() != null);
return _testerdecls;
}
}
#region Object Invariant
[ContractInvariantMethod]
private void ObjectInvariant()
{
Contract.Invariant(this._constdecls != null);
Contract.Invariant(this._testerdecls != null);
Contract.Invariant(this._consts != null);
}
#endregion
#region Internal
readonly private FuncDecl[] _constdecls = null, _testerdecls = null;
readonly private Expr[] _consts = null;
internal EnumSort(Context ctx, Symbol name, Symbol[] enumNames)
: base(ctx)
{
Contract.Requires(ctx != null);
Contract.Requires(name != null);
Contract.Requires(enumNames != null);
int n = enumNames.Length;
IntPtr[] n_constdecls = new IntPtr[n];
IntPtr[] n_testers = new IntPtr[n];
NativeObject = Native.Z3_mk_enumeration_sort(ctx.nCtx, name.NativeObject, (uint)n,
Symbol.ArrayToNative(enumNames), n_constdecls, n_testers);
_constdecls = new FuncDecl[n];
for (uint i = 0; i < n; i++)
_constdecls[i] = new FuncDecl(ctx, n_constdecls[i]);
_testerdecls = new FuncDecl[n];
for (uint i = 0; i < n; i++)
_testerdecls[i] = new FuncDecl(ctx, n_testers[i]);
_consts = new Expr[n];
for (uint i = 0; i < n; i++)
_consts[i] = ctx.MkApp(_constdecls[i]);
}
#endregion
};
/// <summary>
/// List sorts.
/// </summary>
[ContractVerification(true)]
public class ListSort : Sort
{
/// <summary>
/// The declaration of the nil function of this list sort.
/// </summary>
public FuncDecl NilDecl { get {
Contract.Ensures(Contract.Result<FuncDecl>() != null);
return nilDecl; } }
/// <summary>
/// The empty list.
/// </summary>
public Expr Nil
{
get
{
Contract.Ensures(Contract.Result<Expr>() != null);
return nilConst;
}
}
/// <summary>
/// The declaration of the isNil function of this list sort.
/// </summary>
public FuncDecl IsNilDecl
{
get
{
Contract.Ensures(Contract.Result<FuncDecl>() != null);
return isNilDecl;
}
}
/// <summary>
/// The declaration of the cons function of this list sort.
/// </summary>
public FuncDecl ConsDecl
{
get
{
Contract.Ensures(Contract.Result<FuncDecl>() != null);
return consDecl;
}
}
/// <summary>
/// The declaration of the isCons function of this list sort.
/// </summary>
///
public FuncDecl IsConsDecl
{
get
{
Contract.Ensures(Contract.Result<FuncDecl>() != null);
return isConsDecl;
}
}
/// <summary>
/// The declaration of the head function of this list sort.
/// </summary>
public FuncDecl HeadDecl
{
get
{
Contract.Ensures(Contract.Result<FuncDecl>() != null);
return headDecl;
}
}
/// <summary>
/// The declaration of the tail function of this list sort.
/// </summary>
public FuncDecl TailDecl
{
get
{
Contract.Ensures(Contract.Result<FuncDecl>() != null);
return tailDecl;
}
}
#region Object Invariant
[ContractInvariantMethod]
private void ObjectInvariant()
{
Contract.Invariant(nilConst != null);
Contract.Invariant(nilDecl != null);
Contract.Invariant(isNilDecl != null);
Contract.Invariant(consDecl != null);
Contract.Invariant(isConsDecl != null);
Contract.Invariant(headDecl != null);
Contract.Invariant(tailDecl != null);
}
#endregion
#region Internal
readonly private FuncDecl nilDecl, isNilDecl, consDecl, isConsDecl, headDecl, tailDecl;
readonly private Expr nilConst;
internal ListSort(Context ctx, Symbol name, Sort elemSort)
: base(ctx)
{
Contract.Requires(ctx != null);
Contract.Requires(name != null);
Contract.Requires(elemSort != null);
IntPtr inil = IntPtr.Zero,
iisnil = IntPtr.Zero,
icons = IntPtr.Zero,
iiscons = IntPtr.Zero,
ihead = IntPtr.Zero,
itail = IntPtr.Zero;
NativeObject = Native.Z3_mk_list_sort(ctx.nCtx, name.NativeObject, elemSort.NativeObject,
ref inil, ref iisnil, ref icons, ref iiscons, ref ihead, ref itail);
nilDecl = new FuncDecl(ctx, inil);
isNilDecl = new FuncDecl(ctx, iisnil);
consDecl = new FuncDecl(ctx, icons);
isConsDecl = new FuncDecl(ctx, iiscons);
headDecl = new FuncDecl(ctx, ihead);
tailDecl = new FuncDecl(ctx, itail);
nilConst = ctx.MkConst(nilDecl);
}
#endregion
};
/// <summary>
/// Relation sorts.
/// </summary>
[ContractVerification(true)]
public class RelationSort : Sort
{
/// <summary>
/// The arity of the relation sort.
/// </summary>
public uint Arity
{
get { return Native.Z3_get_relation_arity(Context.nCtx, NativeObject); }
}
/// <summary>
/// The sorts of the columns of the relation sort.
/// </summary>
public Sort[] ColumnSorts
{
get
{
Contract.Ensures(Contract.Result<Sort[]>() != null);
if (m_columnSorts != null)
return m_columnSorts;
uint n = Arity;
Sort[] res = new Sort[n];
for (uint i = 0; i < n; i++)
res[i] = Sort.Create(Context, Native.Z3_get_relation_column(Context.nCtx, NativeObject, i));
return res;
}
}
#region Internal
private Sort[] m_columnSorts = null;
internal RelationSort(Context ctx, IntPtr obj)
: base(ctx, obj)
{
Contract.Requires(ctx != null);
}
#endregion
}
/// <summary>
/// Finite domain sorts.
/// </summary>
[ContractVerification(true)]
public class FiniteDomainSort : Sort
{
/// <summary>
/// The size of the finite domain sort.
/// </summary>
public ulong Size
{
get { ulong res = 0; Native.Z3_get_finite_domain_sort_size(Context.nCtx, NativeObject, ref res); return res; }
}
#region Internal
internal FiniteDomainSort(Context ctx, IntPtr obj)
: base(ctx, obj)
{
Contract.Requires(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);
}
#endregion
}
/// <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);
}
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);
}
#endregion
}
}
}

View file

@ -86,8 +86,18 @@ namespace Microsoft.Z3
readonly private bool m_is_double = false;
readonly private uint m_uint = 0;
readonly private double m_double = 0.0;
internal Entry(string k, uint v) { Key = k; m_is_uint = true; m_uint = v; }
internal Entry(string k, double v) { Key = k; m_is_double = true; m_double = v; }
internal Entry(string k, uint v)
{
Key = k;
m_is_uint = true;
m_uint = v;
}
internal Entry(string k, double v)
{
Key = k;
m_is_double = true;
m_double = v;
}
#endregion
}
@ -177,7 +187,7 @@ namespace Microsoft.Z3
Contract.Requires(ctx != null);
}
internal class DecRefQueue : Z3.DecRefQueue
internal class DecRefQueue : IDecRefQueue
{
public override void IncRef(Context ctx, IntPtr obj)
{

View file

@ -0,0 +1,73 @@
/*++
Copyright (c) 2012 Microsoft Corporation
Module Name:
StringSymbol.cs
Abstract:
Z3 Managed API: String Symbols
Author:
Christoph Wintersteiger (cwinter) 2012-11-23
Notes:
--*/
using System;
using System.Runtime.InteropServices;
using System.Diagnostics.Contracts;
namespace Microsoft.Z3
{
/// <summary>
/// Named symbols
/// </summary>
[ContractVerification(true)]
public class StringSymbol : Symbol
{
/// <summary>
/// The string value of the symbol.
/// </summary>
/// <remarks>Throws an exception if the symbol is not of string kind.</remarks>
public string String
{
get
{
Contract.Ensures(Contract.Result<string>() != null);
if (!IsStringSymbol())
throw new Z3Exception("String requested from non-String symbol");
return Native.Z3_get_symbol_string(Context.nCtx, NativeObject);
}
}
#region Internal
internal StringSymbol(Context ctx, IntPtr obj)
: base(ctx, obj)
{
Contract.Requires(ctx != null);
}
internal StringSymbol(Context ctx, string s)
: base(ctx, Native.Z3_mk_string_symbol(ctx.nCtx, s))
{
Contract.Requires(ctx != null);
}
#if DEBUG
internal override void CheckNativeObject(IntPtr obj)
{
if ((Z3_symbol_kind)Native.Z3_get_symbol_kind(Context.nCtx, obj) != Z3_symbol_kind.Z3_STRING_SYMBOL)
throw new Z3Exception("Symbol is not of string kind");
base.CheckNativeObject(obj);
}
#endif
#endregion
}
}

View file

@ -90,92 +90,4 @@ namespace Microsoft.Z3
}
#endregion
}
/// <summary>
/// Numbered symbols
/// </summary>
[ContractVerification(true)]
public class IntSymbol : Symbol
{
/// <summary>
/// The int value of the symbol.
/// </summary>
/// <remarks>Throws an exception if the symbol is not of int kind. </remarks>
public int Int
{
get
{
if (!IsIntSymbol())
throw new Z3Exception("Int requested from non-Int symbol");
return Native.Z3_get_symbol_int(Context.nCtx, NativeObject);
}
}
#region Internal
internal IntSymbol(Context ctx, IntPtr obj)
: base(ctx, obj)
{
Contract.Requires(ctx != null);
}
internal IntSymbol(Context ctx, int i)
: base(ctx, Native.Z3_mk_int_symbol(ctx.nCtx, i))
{
Contract.Requires(ctx != null);
}
#if DEBUG
internal override void CheckNativeObject(IntPtr obj)
{
if ((Z3_symbol_kind)Native.Z3_get_symbol_kind(Context.nCtx, obj) != Z3_symbol_kind.Z3_INT_SYMBOL)
throw new Z3Exception("Symbol is not of integer kind");
base.CheckNativeObject(obj);
}
#endif
#endregion
}
/// <summary>
/// Named symbols
/// </summary>
[ContractVerification(true)]
public class StringSymbol : Symbol
{
/// <summary>
/// The string value of the symbol.
/// </summary>
/// <remarks>Throws an exception if the symbol is not of string kind.</remarks>
public string String
{
get
{
Contract.Ensures(Contract.Result<string>() != null);
if (!IsStringSymbol())
throw new Z3Exception("String requested from non-String symbol");
return Native.Z3_get_symbol_string(Context.nCtx, NativeObject);
}
}
#region Internal
internal StringSymbol(Context ctx, IntPtr obj) : base(ctx, obj)
{
Contract.Requires(ctx != null);
}
internal StringSymbol(Context ctx, string s) : base(ctx, Native.Z3_mk_string_symbol(ctx.nCtx, s))
{
Contract.Requires(ctx != null);
}
#if DEBUG
internal override void CheckNativeObject(IntPtr obj)
{
if ((Z3_symbol_kind)Native.Z3_get_symbol_kind(Context.nCtx, obj) != Z3_symbol_kind.Z3_STRING_SYMBOL)
throw new Z3Exception("Symbol is not of string kind");
base.CheckNativeObject(obj);
}
#endif
#endregion
}
}

View file

@ -112,7 +112,7 @@ namespace Microsoft.Z3
Contract.Requires(ctx != null);
}
internal class DecRefQueue : Z3.DecRefQueue
internal class DecRefQueue : IDecRefQueue
{
public override void IncRef(Context ctx, IntPtr obj)
{

View file

@ -0,0 +1,83 @@
/*++
Copyright (c) 2012 Microsoft Corporation
Module Name:
TupleSort.cs
Abstract:
Z3 Managed API: Tuple Sorts
Author:
Christoph Wintersteiger (cwinter) 2012-11-23
Notes:
--*/
using System;
using System.Diagnostics.Contracts;
namespace Microsoft.Z3
{
/// <summary>
/// Tuple sorts.
/// </summary>
[ContractVerification(true)]
public class TupleSort : Sort
{
/// <summary>
/// The constructor function of the tuple.
/// </summary>
public FuncDecl MkDecl
{
get
{
Contract.Ensures(Contract.Result<FuncDecl>() != null);
return new FuncDecl(Context, Native.Z3_get_tuple_sort_mk_decl(Context.nCtx, NativeObject));
}
}
/// <summary>
/// The number of fields in the tuple.
/// </summary>
public uint NumFields
{
get { return Native.Z3_get_tuple_sort_num_fields(Context.nCtx, NativeObject); }
}
/// <summary>
/// The field declarations.
/// </summary>
public FuncDecl[] FieldDecls
{
get
{
Contract.Ensures(Contract.Result<FuncDecl[]>() != null);
uint n = NumFields;
FuncDecl[] res = new FuncDecl[n];
for (uint i = 0; i < n; i++)
res[i] = new FuncDecl(Context, Native.Z3_get_tuple_sort_field_decl(Context.nCtx, NativeObject, i));
return res;
}
}
#region Internal
internal TupleSort(Context ctx, Symbol name, uint numFields, Symbol[] fieldNames, Sort[] fieldSorts)
: base(ctx)
{
Contract.Requires(ctx != null);
Contract.Requires(name != null);
IntPtr t = IntPtr.Zero;
NativeObject = Native.Z3_mk_tuple_sort(ctx.nCtx, name.NativeObject, numFields,
Symbol.ArrayToNative(fieldNames), AST.ArrayToNative(fieldSorts),
ref t, new IntPtr[numFields]);
}
#endregion
};
}

View file

@ -0,0 +1,44 @@
/*++
Copyright (c) 2012 Microsoft Corporation
Module Name:
UninterpretedSort.cs
Abstract:
Z3 Managed API: Uninterpreted Sorts
Author:
Christoph Wintersteiger (cwinter) 2012-11-23
Notes:
--*/
using System;
using System.Diagnostics.Contracts;
namespace Microsoft.Z3
{
/// <summary>
/// Uninterpreted Sorts
/// </summary>
public class UninterpretedSort : Sort
{
#region Internal
internal UninterpretedSort(Context ctx, IntPtr obj)
: base(ctx, obj)
{
Contract.Requires(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);
}
#endregion
}
}