diff --git a/src/api/dotnet/AST.cs b/src/api/dotnet/AST.cs index e3b8fc3ec..2c4c964df 100644 --- a/src/api/dotnet/AST.cs +++ b/src/api/dotnet/AST.cs @@ -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) { diff --git a/src/api/dotnet/ASTMap.cs b/src/api/dotnet/ASTMap.cs index d945b3d44..9de3b8358 100644 --- a/src/api/dotnet/ASTMap.cs +++ b/src/api/dotnet/ASTMap.cs @@ -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) { diff --git a/src/api/dotnet/ASTVector.cs b/src/api/dotnet/ASTVector.cs index f2ca58170..bbba3de90 100644 --- a/src/api/dotnet/ASTVector.cs +++ b/src/api/dotnet/ASTVector.cs @@ -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) { diff --git a/src/api/dotnet/AlgebraicNum.cs b/src/api/dotnet/AlgebraicNum.cs new file mode 100644 index 000000000..66552f1a0 --- /dev/null +++ b/src/api/dotnet/AlgebraicNum.cs @@ -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 +{ + /// + /// Algebraic numbers + /// + [ContractVerification(true)] + public class AlgebraicNum : ArithExpr + { + /// + /// Return a upper bound for a given real algebraic number. + /// The interval isolating the number is smaller than 1/10^. + /// + /// + /// the precision of the result + /// A numeral Expr of sort Real + public RatNum ToUpper(uint precision) + { + Contract.Ensures(Contract.Result() != null); + + return new RatNum(Context, Native.Z3_get_algebraic_number_upper(Context.nCtx, NativeObject, precision)); + } + + /// + /// Return a lower bound for the given real algebraic number. + /// The interval isolating the number is smaller than 1/10^. + /// + /// + /// + /// A numeral Expr of sort Real + public RatNum ToLower(uint precision) + { + Contract.Ensures(Contract.Result() != null); + + return new RatNum(Context, Native.Z3_get_algebraic_number_lower(Context.nCtx, NativeObject, precision)); + } + + /// + /// Returns a string representation in decimal notation. + /// + /// The result has at most decimal places. + public string ToDecimal(uint precision) + { + Contract.Ensures(Contract.Result() != null); + + return Native.Z3_get_numeral_decimal_string(Context.nCtx, NativeObject, precision); + } + + #region Internal + internal AlgebraicNum(Context ctx, IntPtr obj) + : base(ctx, obj) + { + Contract.Requires(ctx != null); + } + #endregion + } +} diff --git a/src/api/dotnet/ApplyResult.cs b/src/api/dotnet/ApplyResult.cs index 21a515643..d64dccb4b 100644 --- a/src/api/dotnet/ApplyResult.cs +++ b/src/api/dotnet/ApplyResult.cs @@ -44,8 +44,8 @@ namespace Microsoft.Z3 { get { - Contract.Ensures(Contract.Result() != null); - Contract.Ensures(Contract.Result().Length == this.NumSubgoals); + Contract.Ensures(Contract.Result() != null); + Contract.Ensures(Contract.Result().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) { diff --git a/src/api/dotnet/ArithExpr.cs b/src/api/dotnet/ArithExpr.cs new file mode 100644 index 000000000..bdfa7a3f0 --- /dev/null +++ b/src/api/dotnet/ArithExpr.cs @@ -0,0 +1,47 @@ +/*++ +Copyright () 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 +{ + /// + /// Arithmetic expressions (int/real) + /// + public class ArithExpr : Expr + { + #region Internal + /// Constructor for ArithExpr + 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 + } +} diff --git a/src/api/dotnet/ArithSort.cs b/src/api/dotnet/ArithSort.cs new file mode 100644 index 000000000..f19774246 --- /dev/null +++ b/src/api/dotnet/ArithSort.cs @@ -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 +{ + /// + /// An arithmetic sort, i.e., Int or Real. + /// + public class ArithSort : Sort + { + #region Internal + internal ArithSort(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); } + #endregion + }; +} diff --git a/src/api/dotnet/ArrayExpr.cs b/src/api/dotnet/ArrayExpr.cs new file mode 100644 index 000000000..915bfd0f1 --- /dev/null +++ b/src/api/dotnet/ArrayExpr.cs @@ -0,0 +1,47 @@ +/*++ +Copyright () 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 +{ + /// + /// Array expressions + /// + public class ArrayExpr : Expr + { + #region Internal + /// Constructor for ArrayExpr + 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 + } +} diff --git a/src/api/dotnet/ArraySort.cs b/src/api/dotnet/ArraySort.cs new file mode 100644 index 000000000..ddd27785c --- /dev/null +++ b/src/api/dotnet/ArraySort.cs @@ -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 +{ + /// + /// Array sorts. + /// + [ContractVerification(true)] + public class ArraySort : Sort + { + /// + /// The domain of the array sort. + /// + public Sort Domain + { + get + { + Contract.Ensures(Contract.Result() != null); + + return Sort.Create(Context, Native.Z3_get_array_sort_domain(Context.nCtx, NativeObject)); + } + } + + /// + /// The range of the array sort. + /// + public Sort Range + { + get + { + Contract.Ensures(Contract.Result() != null); + + return Sort.Create(Context, Native.Z3_get_array_sort_range(Context.nCtx, NativeObject)); + } + } + + #region Internal + internal ArraySort(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); } + internal ArraySort(Context ctx, 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 + }; + +} diff --git a/src/api/dotnet/BitVecExpr.cs b/src/api/dotnet/BitVecExpr.cs new file mode 100644 index 000000000..a146e7a19 --- /dev/null +++ b/src/api/dotnet/BitVecExpr.cs @@ -0,0 +1,48 @@ +/*++ +Copyright () 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 +{ + /// + /// Bit-vector expressions + /// + public class BitVecExpr : Expr + { + + /// + /// The size of the sort of a bit-vector term. + /// + public uint SortSize + { + get { return ((BitVecSort)Sort).Size; } + } + + #region Internal + /// Constructor for BitVecExpr + 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 + } +} diff --git a/src/api/dotnet/BitVecNum.cs b/src/api/dotnet/BitVecNum.cs new file mode 100644 index 000000000..c6ac471f6 --- /dev/null +++ b/src/api/dotnet/BitVecNum.cs @@ -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 +{ + /// + /// Bit-vector numerals + /// + [ContractVerification(true)] + public class BitVecNum : BitVecExpr + { + /// + /// Retrieve the 64-bit unsigned integer value. + /// + 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; + } + } + + /// + /// Retrieve the int value. + /// + 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; + } + } + + /// + /// Retrieve the 64-bit int value. + /// + 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; + } + } + + /// + /// Retrieve the int value. + /// + 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 + /// + /// Retrieve the BigInteger value. + /// + public BigInteger BigInteger + { + get + { + return BigInteger.Parse(this.ToString()); + } + } +#endif + + /// + /// Returns a string representation of the numeral. + /// + 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 + } +} diff --git a/src/api/dotnet/BitVecSort.cs b/src/api/dotnet/BitVecSort.cs new file mode 100644 index 000000000..55ef4ae49 --- /dev/null +++ b/src/api/dotnet/BitVecSort.cs @@ -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 +{ + /// + /// Bit-vector sorts. + /// + public class BitVecSort : Sort + { + /// + /// The size of the bit-vector sort. + /// + 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 + }; +} diff --git a/src/api/dotnet/BoolExpr.cs b/src/api/dotnet/BoolExpr.cs new file mode 100644 index 000000000..cbe3b1868 --- /dev/null +++ b/src/api/dotnet/BoolExpr.cs @@ -0,0 +1,40 @@ +/*++ +Copyright () 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 +{ + /// + /// Boolean expressions + /// + public class BoolExpr : Expr + { + #region Internal + /// Constructor for BoolExpr + internal protected BoolExpr(Context ctx) : base(ctx) { Contract.Requires(ctx != null); } + /// Constructor for BoolExpr + internal BoolExpr(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); } + #endregion + } +} diff --git a/src/api/dotnet/BoolSort.cs b/src/api/dotnet/BoolSort.cs new file mode 100644 index 000000000..50f44c858 --- /dev/null +++ b/src/api/dotnet/BoolSort.cs @@ -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 +{ + /// + /// A Boolean sort. + /// + 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 + }; +} diff --git a/src/api/dotnet/Constructor.cs b/src/api/dotnet/Constructor.cs index 93d283771..043eb3a1e 100644 --- a/src/api/dotnet/Constructor.cs +++ b/src/api/dotnet/Constructor.cs @@ -149,35 +149,4 @@ namespace Microsoft.Z3 #endregion } - - /// - /// Lists of constructors - /// - public class ConstructorList : Z3Object - { - /// - /// Destructor. - /// - ~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 - } } diff --git a/src/api/dotnet/ConstructorList.cs b/src/api/dotnet/ConstructorList.cs new file mode 100644 index 000000000..d625b5ade --- /dev/null +++ b/src/api/dotnet/ConstructorList.cs @@ -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 +{ + /// + /// Lists of constructors + /// + public class ConstructorList : Z3Object + { + /// + /// Destructor. + /// + ~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 + } +} diff --git a/src/api/dotnet/DatatypeExpr.cs b/src/api/dotnet/DatatypeExpr.cs new file mode 100644 index 000000000..93cea54f5 --- /dev/null +++ b/src/api/dotnet/DatatypeExpr.cs @@ -0,0 +1,47 @@ +/*++ +Copyright () 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 +{ + /// + /// Datatype expressions + /// + public class DatatypeExpr : Expr + { + #region Internal + /// Constructor for DatatypeExpr + 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 + } +} diff --git a/src/api/dotnet/DatatypeSort.cs b/src/api/dotnet/DatatypeSort.cs new file mode 100644 index 000000000..e47545d68 --- /dev/null +++ b/src/api/dotnet/DatatypeSort.cs @@ -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 +{ + /// + /// Datatype sorts. + /// + [ContractVerification(true)] + public class DatatypeSort : Sort + { + /// + /// The number of constructors of the datatype sort. + /// + public uint NumConstructors + { + get { return Native.Z3_get_datatype_sort_num_constructors(Context.nCtx, NativeObject); } + } + + /// + /// The constructors. + /// + public FuncDecl[] Constructors + { + get + { + Contract.Ensures(Contract.Result() != 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; + } + } + + /// + /// The recognizers. + /// + public FuncDecl[] Recognizers + { + get + { + Contract.Ensures(Contract.Result() != 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; + } + } + + /// + /// The constructor accessors. + /// + public FuncDecl[][] Accessors + { + get + { + Contract.Ensures(Contract.Result() != 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 + }; +} diff --git a/src/api/dotnet/EnumSort.cs b/src/api/dotnet/EnumSort.cs new file mode 100644 index 000000000..1a9b0536c --- /dev/null +++ b/src/api/dotnet/EnumSort.cs @@ -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 +{ + /// + /// Enumeration sorts. + /// + [ContractVerification(true)] + public class EnumSort : Sort + { + /// + /// The function declarations of the constants in the enumeration. + /// + public FuncDecl[] ConstDecls + { + get + { + Contract.Ensures(Contract.Result() != null); + + return _constdecls; + } + } + + /// + /// The constants in the enumeration. + /// + public Expr[] Consts + { + get + { + Contract.Ensures(Contract.Result() != null); + + return _consts; + } + } + + /// + /// The test predicates for the constants in the enumeration. + /// + public FuncDecl[] TesterDecls + { + get + { + Contract.Ensures(Contract.Result() != 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 + }; +} diff --git a/src/api/dotnet/Expr.cs b/src/api/dotnet/Expr.cs index c559e61e9..22a506c71 100644 --- a/src/api/dotnet/Expr.cs +++ b/src/api/dotnet/Expr.cs @@ -1548,138 +1548,4 @@ namespace Microsoft.Z3 } #endregion } - - /// - /// Boolean expressions - /// - public class BoolExpr : Expr - { - #region Internal - /// Constructor for BoolExpr - internal protected BoolExpr(Context ctx) : base(ctx) { Contract.Requires(ctx != null); } - /// Constructor for BoolExpr - internal BoolExpr(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); } - #endregion - } - - /// - /// Arithmetic expressions (int/real) - /// - public class ArithExpr : Expr - { - #region Internal - /// Constructor for ArithExpr - 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 - } - - /// - /// Int expressions - /// - public class IntExpr : ArithExpr - { - #region Internal - /// Constructor for IntExpr - 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 - } - - /// - /// Real expressions - /// - public class RealExpr : ArithExpr - { - #region Internal - /// Constructor for RealExpr - 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 - } - - /// - /// Bit-vector expressions - /// - public class BitVecExpr : Expr - { - - /// - /// The size of the sort of a bit-vector term. - /// - public uint SortSize - { - get { return ((BitVecSort)Sort).Size; } - } - - #region Internal - /// Constructor for BitVecExpr - 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 - } - - /// - /// Array expressions - /// - public class ArrayExpr : Expr - { - #region Internal - /// Constructor for ArrayExpr - 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 - } - - /// - /// Datatype expressions - /// - public class DatatypeExpr : Expr - { - #region Internal - /// Constructor for DatatypeExpr - 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 - } } diff --git a/src/api/dotnet/FiniteDomainSort.cs b/src/api/dotnet/FiniteDomainSort.cs new file mode 100644 index 000000000..93540ff87 --- /dev/null +++ b/src/api/dotnet/FiniteDomainSort.cs @@ -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 +{ + /// + /// Finite domain sorts. + /// + [ContractVerification(true)] + public class FiniteDomainSort : Sort + { + /// + /// The size of the finite domain sort. + /// + 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 + } +} diff --git a/src/api/dotnet/Fixedpoint.cs b/src/api/dotnet/Fixedpoint.cs index c19a7cb04..8d13fcb43 100644 --- a/src/api/dotnet/Fixedpoint.cs +++ b/src/api/dotnet/Fixedpoint.cs @@ -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) { diff --git a/src/api/dotnet/FuncDecl.cs b/src/api/dotnet/FuncDecl.cs index ef64ce767..37929e88f 100644 --- a/src/api/dotnet/FuncDecl.cs +++ b/src/api/dotnet/FuncDecl.cs @@ -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); diff --git a/src/api/dotnet/FuncInterp.cs b/src/api/dotnet/FuncInterp.cs index b6b794028..a6628af28 100644 --- a/src/api/dotnet/FuncInterp.cs +++ b/src/api/dotnet/FuncInterp.cs @@ -40,9 +40,11 @@ namespace Microsoft.Z3 /// public Expr Value { - get { + get + { Contract.Ensures(Contract.Result() != 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)); + } } /// @@ -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() != null); - Contract.Ensures(Contract.ForAll(0, Contract.Result().Length, - j => Contract.Result()[j] != null)); + Contract.Ensures(Contract.ForAll(0, Contract.Result().Length, j => Contract.Result()[j] != null)); uint n = NumEntries; Entry[] res = new Entry[n]; @@ -146,10 +147,12 @@ namespace Microsoft.Z3 /// public Expr Else { - get { + get + { Contract.Ensures(Contract.Result() != 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)); + } } /// @@ -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) { diff --git a/src/api/dotnet/Goal.cs b/src/api/dotnet/Goal.cs index 02edee77f..6a0b253bb 100644 --- a/src/api/dotnet/Goal.cs +++ b/src/api/dotnet/Goal.cs @@ -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) { diff --git a/src/api/dotnet/DecRefQUeue.cs b/src/api/dotnet/IDecRefQueue.cs similarity index 93% rename from src/api/dotnet/DecRefQUeue.cs rename to src/api/dotnet/IDecRefQueue.cs index 777a5d5af..e6276c4f4 100644 --- a/src/api/dotnet/DecRefQUeue.cs +++ b/src/api/dotnet/IDecRefQueue.cs @@ -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) { diff --git a/src/api/dotnet/IntExpr.cs b/src/api/dotnet/IntExpr.cs new file mode 100644 index 000000000..4c52ec79f --- /dev/null +++ b/src/api/dotnet/IntExpr.cs @@ -0,0 +1,47 @@ +/*++ +Copyright () 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 +{ + /// + /// Int expressions + /// + public class IntExpr : ArithExpr + { + #region Internal + /// Constructor for IntExpr + 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 + } +} diff --git a/src/api/dotnet/IntNum.cs b/src/api/dotnet/IntNum.cs new file mode 100644 index 000000000..64fd78ad2 --- /dev/null +++ b/src/api/dotnet/IntNum.cs @@ -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 +{ + /// + /// Integer Numerals + /// + [ContractVerification(true)] + public class IntNum : IntExpr + { + + #region Internal + internal IntNum(Context ctx, IntPtr obj) + : base(ctx, obj) + { + Contract.Requires(ctx != null); + } + #endregion + + + /// + /// Retrieve the 64-bit unsigned integer value. + /// + 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; + } + } + + /// + /// Retrieve the int value. + /// + 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; + } + } + + /// + /// Retrieve the 64-bit int value. + /// + 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; + } + } + + /// + /// Retrieve the int value. + /// + 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 + /// + /// Retrieve the BigInteger value. + /// + public BigInteger BigInteger + { + get + { + return BigInteger.Parse(this.ToString()); + } + } +#endif + + /// + /// Returns a string representation of the numeral. + /// + public override string ToString() + { + return Native.Z3_get_numeral_string(Context.nCtx, NativeObject); + } + } +} diff --git a/src/api/dotnet/IntSort.cs b/src/api/dotnet/IntSort.cs new file mode 100644 index 000000000..d0c25ac79 --- /dev/null +++ b/src/api/dotnet/IntSort.cs @@ -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 +{ + /// + /// An Integer sort + /// + 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 + } +} diff --git a/src/api/dotnet/IntSymbol.cs b/src/api/dotnet/IntSymbol.cs new file mode 100644 index 000000000..df2d9da52 --- /dev/null +++ b/src/api/dotnet/IntSymbol.cs @@ -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 +{ + /// + /// Numbered symbols + /// + [ContractVerification(true)] + public class IntSymbol : Symbol + { + /// + /// The int value of the symbol. + /// + /// Throws an exception if the symbol is not of int kind. + 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 + } +} diff --git a/src/api/dotnet/ListSort.cs b/src/api/dotnet/ListSort.cs new file mode 100644 index 000000000..c099259a2 --- /dev/null +++ b/src/api/dotnet/ListSort.cs @@ -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 +{ + /// + /// List sorts. + /// + [ContractVerification(true)] + public class ListSort : Sort + { + /// + /// The declaration of the nil function of this list sort. + /// + public FuncDecl NilDecl + { + get + { + Contract.Ensures(Contract.Result() != null); + return nilDecl; + } + } + + /// + /// The empty list. + /// + public Expr Nil + { + get + { + Contract.Ensures(Contract.Result() != null); + return nilConst; + } + } + + /// + /// The declaration of the isNil function of this list sort. + /// + public FuncDecl IsNilDecl + { + get + { + Contract.Ensures(Contract.Result() != null); + return isNilDecl; + } + } + + /// + /// The declaration of the cons function of this list sort. + /// + public FuncDecl ConsDecl + { + get + { + Contract.Ensures(Contract.Result() != null); + return consDecl; + } + } + + /// + /// The declaration of the isCons function of this list sort. + /// + /// + public FuncDecl IsConsDecl + { + get + { + Contract.Ensures(Contract.Result() != null); + return isConsDecl; + } + } + + /// + /// The declaration of the head function of this list sort. + /// + public FuncDecl HeadDecl + { + get + { + Contract.Ensures(Contract.Result() != null); + return headDecl; + } + } + + /// + /// The declaration of the tail function of this list sort. + /// + public FuncDecl TailDecl + { + get + { + Contract.Ensures(Contract.Result() != 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 + }; +} diff --git a/src/api/dotnet/Microsoft.Z3.csproj b/src/api/dotnet/Microsoft.Z3.csproj index 62ec169b0..762b83b28 100644 --- a/src/api/dotnet/Microsoft.Z3.csproj +++ b/src/api/dotnet/Microsoft.Z3.csproj @@ -258,29 +258,56 @@ + + + + + + + + + + - + + + + + + + + + + + - + + + + + + + + diff --git a/src/api/dotnet/Microsoft.Z3_35.csproj b/src/api/dotnet/Microsoft.Z3_35.csproj deleted file mode 100644 index 8cfe8a532..000000000 --- a/src/api/dotnet/Microsoft.Z3_35.csproj +++ /dev/null @@ -1,403 +0,0 @@ - - - - Debug - AnyCPU - 8.0.30703 - 2.0 - {EC3DB697-B734-42F7-9468-5B62821EEB5A} - Library - Properties - Microsoft.Z3 - Microsoft.Z3 - v3.5 - 512 - Client - 0 - - - true - full - false - bin35\Debug\ - DEBUG;TRACE - prompt - 4 - true - - - False - False - True - False - False - True - False - True - True - False - False - False - True - False - False - False - True - False - False - True - True - True - False - False - - - - - - - True - Full - %28none%29 - 2 - - - pdbonly - true - bin35\external\bin\ - FRAMEWORK_LT_4 - prompt - 4 - true - ..\external\Microsoft.Z3.xml - - - bin35\external\bin\ - true - ..\external\Microsoft.Z3.xml - true - pdbonly - AnyCPU - bin\Release\Microsoft.Z3.dll.CodeAnalysisLog.xml - true - GlobalSuppressions.cs - prompt - MinimumRecommendedRules.ruleset - ;C:\Program Files\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets - true - ;C:\Program Files\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules - true - false - FRAMEWORK_LT_4 - - - bin35\external\bin\ - true - ..\external\Microsoft.Z3.xml - true - pdbonly - AnyCPU - bin\Release\Microsoft.Z3.dll.CodeAnalysisLog.xml - true - GlobalSuppressions.cs - prompt - MinimumRecommendedRules.ruleset - ;C:\Program Files\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets - true - ;C:\Program Files\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules - true - false - FRAMEWORK_LT_4 - - - true - bin35\x64\Debug\ - DEBUG;TRACE - true - full - x64 - ..\Debug\Microsoft.Z3.dll.CodeAnalysisLog.xml - true - GlobalSuppressions.cs - prompt - MinimumRecommendedRules.ruleset - ;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets - true - ;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules - true - True - False - True - False - False - False - False - False - False - False - False - False - False - False - False - False - True - False - False - True - False - False - False - - - - - - - False - Full - %28none%29 - 0 - - - bin35\external\x64\ - true - ..\x64\external_64\Microsoft.Z3.xml - true - pdbonly - x64 - ..\release\Microsoft.Z3.dll.CodeAnalysisLog.xml - true - GlobalSuppressions.cs - prompt - MinimumRecommendedRules.ruleset - ;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets - true - ;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules - True - False - True - False - False - True - True - True - False - False - False - True - True - False - False - False - True - False - False - True - True - False - False - - - - - -repro - - True - Full - %28none%29 - 2 - - - bin35\external\x64 - true - ..\external\Microsoft.Z3.xml - true - pdbonly - x64 - bin\Release\Microsoft.Z3.dll.CodeAnalysisLog.xml - true - GlobalSuppressions.cs - prompt - MinimumRecommendedRules.ruleset - ;C:\Program Files\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets - true - ;C:\Program Files\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules - true - - - bin35\external_64\x64 - true - ..\x64\external_64\Microsoft.Z3.xml - FRAMEWORK_LT_4 - true - pdbonly - AnyCPU - bin\Release\Microsoft.Z3.dll.CodeAnalysisLog.xml - true - GlobalSuppressions.cs - prompt - MinimumRecommendedRules.ruleset - ;C:\Program Files\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets - true - ;C:\Program Files\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules - true - false - - - bin35\external_64\x64 - true - ..\x64\external_64\Microsoft.Z3.xml - true - pdbonly - x64 - bin\Release\Microsoft.Z3.dll.CodeAnalysisLog.xml - true - GlobalSuppressions.cs - prompt - MinimumRecommendedRules.ruleset - ;C:\Program Files\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets - true - ;C:\Program Files\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules - true - false - True - False - True - False - False - False - False - False - False - False - False - False - False - False - False - False - True - False - False - True - False - False - False - - - - - - - False - Full - %28none%29 - 0 - FRAMEWORK_LT_4 - - - true - - - z3.snk - - - false - - - bin35\Release_delaysign\ - true - ..\Release_delaysign\Microsoft.Z3.xml - true - pdbonly - AnyCPU - ..\release\Microsoft.Z3.dll.CodeAnalysisLog.xml - true - GlobalSuppressions.cs - prompt - MinimumRecommendedRules.ruleset - ;C:\Program Files\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets - true - ;C:\Program Files\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules - true - DELAYSIGN - - - bin\x64\Release_delaysign\ - true - ..\x64\external_64\Microsoft.Z3.xml - true - pdbonly - x64 - ..\release\Microsoft.Z3.dll.CodeAnalysisLog.xml - true - GlobalSuppressions.cs - prompt - MinimumRecommendedRules.ruleset - ;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets - true - ;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 - true - - - - False - ..\..\..\..\Program Files\Microsoft\Contracts\Contracts\v3.5\Microsoft.Contracts.dll - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - \ No newline at end of file diff --git a/src/api/dotnet/Model.cs b/src/api/dotnet/Model.cs index d5bcd34b0..5529677dd 100644 --- a/src/api/dotnet/Model.cs +++ b/src/api/dotnet/Model.cs @@ -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) { diff --git a/src/api/dotnet/Numeral.cs b/src/api/dotnet/Numeral.cs deleted file mode 100644 index fb8af747b..000000000 --- a/src/api/dotnet/Numeral.cs +++ /dev/null @@ -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 -{ - /// - /// Integer Numerals - /// - [ContractVerification(true)] - public class IntNum : IntExpr - { - - #region Internal - internal IntNum(Context ctx, IntPtr obj) - : base(ctx, obj) - { - Contract.Requires(ctx != null); - } - #endregion - - - /// - /// Retrieve the 64-bit unsigned integer value. - /// - 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; - } - } - - /// - /// Retrieve the int value. - /// - 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; - } - } - - /// - /// Retrieve the 64-bit int value. - /// - 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; - } - } - - /// - /// Retrieve the int value. - /// - 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 - /// - /// Retrieve the BigInteger value. - /// - public BigInteger BigInteger - { - get - { - return BigInteger.Parse(this.ToString()); - } - } -#endif - - /// - /// Returns a string representation of the numeral. - /// - public override string ToString() - { - return Native.Z3_get_numeral_string(Context.nCtx, NativeObject); - } - } - - /// - /// Rational Numerals - /// - [ContractVerification(true)] - public class RatNum : RealExpr - { - /// - /// The numerator of a rational numeral. - /// - public IntNum Numerator - { - get { - Contract.Ensures(Contract.Result() != null); - - return new IntNum(Context, Native.Z3_get_numerator(Context.nCtx, NativeObject)); } - } - - /// - /// The denominator of a rational numeral. - /// - public IntNum Denominator - { - get { - Contract.Ensures(Contract.Result() != null); - - return new IntNum(Context, Native.Z3_get_denominator(Context.nCtx, NativeObject)); } - } - -#if !FRAMEWORK_LT_4 - /// - /// Converts the numerator of the rational to a BigInteger - /// - public BigInteger BigIntNumerator - { - get - { - IntNum n = Numerator; - return BigInteger.Parse(n.ToString()); - } - } - - /// - /// Converts the denominator of the rational to a BigInteger - /// - public BigInteger BigIntDenominator - { - get - { - IntNum n = Denominator; - return BigInteger.Parse(n.ToString()); - } - } -#endif - - /// - /// Returns a string representation in decimal notation. - /// - /// The result has at most decimal places. - public string ToDecimalString(uint precision) - { - return Native.Z3_get_numeral_decimal_string(Context.nCtx, NativeObject, precision); - } - - /// - /// Returns a string representation of the numeral. - /// - 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 - } - - - /// - /// Bit-vector numerals - /// - [ContractVerification(true)] - public class BitVecNum : BitVecExpr - { - /// - /// Retrieve the 64-bit unsigned integer value. - /// - 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; - } - } - - /// - /// Retrieve the int value. - /// - 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; - } - } - - /// - /// Retrieve the 64-bit int value. - /// - 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; - } - } - - /// - /// Retrieve the int value. - /// - 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 - /// - /// Retrieve the BigInteger value. - /// - public BigInteger BigInteger - { - get - { - return BigInteger.Parse(this.ToString()); - } - } -#endif - - /// - /// Returns a string representation of the numeral. - /// - 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 - } - - /// - /// Algebraic numbers - /// - [ContractVerification(true)] - public class AlgebraicNum : ArithExpr - { - /// - /// Return a upper bound for a given real algebraic number. - /// The interval isolating the number is smaller than 1/10^. - /// - /// - /// the precision of the result - /// A numeral Expr of sort Real - public RatNum ToUpper(uint precision) - { - Contract.Ensures(Contract.Result() != null); - - return new RatNum(Context, Native.Z3_get_algebraic_number_upper(Context.nCtx, NativeObject, precision)); - } - - /// - /// Return a lower bound for the given real algebraic number. - /// The interval isolating the number is smaller than 1/10^. - /// - /// - /// - /// A numeral Expr of sort Real - public RatNum ToLower(uint precision) - { - Contract.Ensures(Contract.Result() != null); - - return new RatNum(Context, Native.Z3_get_algebraic_number_lower(Context.nCtx, NativeObject, precision)); - } - - /// - /// Returns a string representation in decimal notation. - /// - /// The result has at most decimal places. - public string ToDecimal(uint precision) - { - Contract.Ensures(Contract.Result() != null); - - return Native.Z3_get_numeral_decimal_string(Context.nCtx, NativeObject, precision); - } - - #region Internal - internal AlgebraicNum(Context ctx, IntPtr obj) - : base(ctx, obj) - { - Contract.Requires(ctx != null); - } - #endregion - } -} diff --git a/src/api/dotnet/ParamDescrs.cs b/src/api/dotnet/ParamDescrs.cs index ca6db9abf..acfae1b85 100644 --- a/src/api/dotnet/ParamDescrs.cs +++ b/src/api/dotnet/ParamDescrs.cs @@ -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) { diff --git a/src/api/dotnet/Params.cs b/src/api/dotnet/Params.cs index babe46a74..56a7a891f 100644 --- a/src/api/dotnet/Params.cs +++ b/src/api/dotnet/Params.cs @@ -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) { diff --git a/src/api/dotnet/Probe.cs b/src/api/dotnet/Probe.cs index 5bd38bd3c..1ae7ee064 100644 --- a/src/api/dotnet/Probe.cs +++ b/src/api/dotnet/Probe.cs @@ -49,10 +49,15 @@ namespace Microsoft.Z3 /// /// Apply the probe to a goal. /// - 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) { diff --git a/src/api/dotnet/Quantifier.cs b/src/api/dotnet/Quantifier.cs index c1f3bc42d..c6754e570 100644 --- a/src/api/dotnet/Quantifier.cs +++ b/src/api/dotnet/Quantifier.cs @@ -149,18 +149,17 @@ namespace Microsoft.Z3 /// public BoolExpr Body { - get { + get + { Contract.Ensures(Contract.Result() != 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 } } diff --git a/src/api/dotnet/RatNum.cs b/src/api/dotnet/RatNum.cs new file mode 100644 index 000000000..bad6b323d --- /dev/null +++ b/src/api/dotnet/RatNum.cs @@ -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 +{ + /// + /// Rational Numerals + /// + [ContractVerification(true)] + public class RatNum : RealExpr + { + /// + /// The numerator of a rational numeral. + /// + public IntNum Numerator + { + get + { + Contract.Ensures(Contract.Result() != null); + + return new IntNum(Context, Native.Z3_get_numerator(Context.nCtx, NativeObject)); + } + } + + /// + /// The denominator of a rational numeral. + /// + public IntNum Denominator + { + get + { + Contract.Ensures(Contract.Result() != null); + + return new IntNum(Context, Native.Z3_get_denominator(Context.nCtx, NativeObject)); + } + } + +#if !FRAMEWORK_LT_4 + /// + /// Converts the numerator of the rational to a BigInteger + /// + public BigInteger BigIntNumerator + { + get + { + IntNum n = Numerator; + return BigInteger.Parse(n.ToString()); + } + } + + /// + /// Converts the denominator of the rational to a BigInteger + /// + public BigInteger BigIntDenominator + { + get + { + IntNum n = Denominator; + return BigInteger.Parse(n.ToString()); + } + } +#endif + + /// + /// Returns a string representation in decimal notation. + /// + /// The result has at most decimal places. + public string ToDecimalString(uint precision) + { + return Native.Z3_get_numeral_decimal_string(Context.nCtx, NativeObject, precision); + } + + /// + /// Returns a string representation of the numeral. + /// + 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 + } +} diff --git a/src/api/dotnet/RealExpr.cs b/src/api/dotnet/RealExpr.cs new file mode 100644 index 000000000..26adc1fc6 --- /dev/null +++ b/src/api/dotnet/RealExpr.cs @@ -0,0 +1,47 @@ +/*++ +Copyright () 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 +{ + /// + /// Real expressions + /// + public class RealExpr : ArithExpr + { + #region Internal + /// Constructor for RealExpr + 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 + } +} diff --git a/src/api/dotnet/RealSort.cs b/src/api/dotnet/RealSort.cs new file mode 100644 index 000000000..97f1cae11 --- /dev/null +++ b/src/api/dotnet/RealSort.cs @@ -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 +{ + /// + /// A real sort + /// + 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 + } +} diff --git a/src/api/dotnet/RelationSort.cs b/src/api/dotnet/RelationSort.cs new file mode 100644 index 000000000..cfd7a592a --- /dev/null +++ b/src/api/dotnet/RelationSort.cs @@ -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 +{ + /// + /// Relation sorts. + /// + [ContractVerification(true)] + public class RelationSort : Sort + { + /// + /// The arity of the relation sort. + /// + public uint Arity + { + get { return Native.Z3_get_relation_arity(Context.nCtx, NativeObject); } + } + + /// + /// The sorts of the columns of the relation sort. + /// + public Sort[] ColumnSorts + { + get + { + Contract.Ensures(Contract.Result() != 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 + } +} diff --git a/src/api/dotnet/SetSort.cs b/src/api/dotnet/SetSort.cs new file mode 100644 index 000000000..bdba3899f --- /dev/null +++ b/src/api/dotnet/SetSort.cs @@ -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 +{ + /// + /// Set sorts. + /// + [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 + } +} diff --git a/src/api/dotnet/Solver.cs b/src/api/dotnet/Solver.cs index dc261bfd8..fe3a42fa4 100644 --- a/src/api/dotnet/Solver.cs +++ b/src/api/dotnet/Solver.cs @@ -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) { diff --git a/src/api/dotnet/Sort.cs b/src/api/dotnet/Sort.cs index 6df3200cf..9dc23ea09 100644 --- a/src/api/dotnet/Sort.cs +++ b/src/api/dotnet/Sort.cs @@ -98,9 +98,11 @@ namespace Microsoft.Z3 /// public Symbol Name { - get { + get + { Contract.Ensures(Contract.Result() != 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)); + } } /// @@ -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 - } - - /// - /// A Boolean sort. - /// - 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 - }; - - /// - /// An arithmetic sort, i.e., Int or Real. - /// - public class ArithSort : Sort - { - #region Internal - internal ArithSort(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); } - #endregion - }; - - /// - /// An Integer sort - /// - 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 - } - - /// - /// A real sort - /// - 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 - } - - /// - /// Bit-vector sorts. - /// - public class BitVecSort : Sort - { - /// - /// The size of the bit-vector sort. - /// - 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 - }; - - /// - /// Array sorts. - /// - [ContractVerification(true)] - public class ArraySort : Sort - { - /// - /// The domain of the array sort. - /// - public Sort Domain - { - get { - Contract.Ensures(Contract.Result() != null); - - return Sort.Create(Context, Native.Z3_get_array_sort_domain(Context.nCtx, NativeObject)); } - } - - /// - /// The range of the array sort. - /// - public Sort Range - { - get { - Contract.Ensures(Contract.Result() != null); - - return Sort.Create(Context, Native.Z3_get_array_sort_range(Context.nCtx, NativeObject)); } - } - - #region Internal - internal ArraySort(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); } - internal ArraySort(Context ctx, 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 - }; - - /// - /// Datatype sorts. - /// - [ContractVerification(true)] - public class DatatypeSort : Sort - { - /// - /// The number of constructors of the datatype sort. - /// - public uint NumConstructors - { - get { return Native.Z3_get_datatype_sort_num_constructors(Context.nCtx, NativeObject); } - } - - /// - /// The constructors. - /// - public FuncDecl[] Constructors - { - get - { - Contract.Ensures(Contract.Result() != 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; - } - } - - /// - /// The recognizers. - /// - public FuncDecl[] Recognizers - { - get - { - Contract.Ensures(Contract.Result() != 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; - } - } - - /// - /// The constructor accessors. - /// - public FuncDecl[][] Accessors - { - get - { - Contract.Ensures(Contract.Result() != 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 - }; - - /// - /// Uninterpreted Sorts - /// - 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 - } - - /// - /// Tuple sorts. - /// - [ContractVerification(true)] - public class TupleSort : Sort - { - /// - /// The constructor function of the tuple. - /// - public FuncDecl MkDecl - { - get { - Contract.Ensures(Contract.Result() != null); - - return new FuncDecl(Context, Native.Z3_get_tuple_sort_mk_decl(Context.nCtx, NativeObject)); } - } - - /// - /// The number of fields in the tuple. - /// - public uint NumFields - { - get { return Native.Z3_get_tuple_sort_num_fields(Context.nCtx, NativeObject); } - } - - /// - /// The field declarations. - /// - public FuncDecl[] FieldDecls - { - get - { - Contract.Ensures(Contract.Result() != 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 - }; - - /// - /// Enumeration sorts. - /// - [ContractVerification(true)] - public class EnumSort : Sort - { - /// - /// The function declarations of the constants in the enumeration. - /// - public FuncDecl[] ConstDecls - { - get { - Contract.Ensures(Contract.Result() != null); - - return _constdecls; } - } - - /// - /// The constants in the enumeration. - /// - public Expr[] Consts - { - get { - Contract.Ensures(Contract.Result() != null); - - return _consts; } - } - - /// - /// The test predicates for the constants in the enumeration. - /// - public FuncDecl[] TesterDecls - { - get { - Contract.Ensures(Contract.Result() != 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 - }; - - /// - /// List sorts. - /// - [ContractVerification(true)] - public class ListSort : Sort - { - /// - /// The declaration of the nil function of this list sort. - /// - public FuncDecl NilDecl { get { - Contract.Ensures(Contract.Result() != null); - return nilDecl; } } - - /// - /// The empty list. - /// - public Expr Nil - { - get - { - Contract.Ensures(Contract.Result() != null); - return nilConst; - } - } - - /// - /// The declaration of the isNil function of this list sort. - /// - public FuncDecl IsNilDecl - { - get - { - Contract.Ensures(Contract.Result() != null); - return isNilDecl; - } - } - - /// - /// The declaration of the cons function of this list sort. - /// - public FuncDecl ConsDecl - { - get - { - Contract.Ensures(Contract.Result() != null); - return consDecl; - } - } - - /// - /// The declaration of the isCons function of this list sort. - /// - /// - public FuncDecl IsConsDecl - { - get - { - Contract.Ensures(Contract.Result() != null); - return isConsDecl; - } - } - - /// - /// The declaration of the head function of this list sort. - /// - public FuncDecl HeadDecl - { - get - { - Contract.Ensures(Contract.Result() != null); - return headDecl; - } - } - - /// - /// The declaration of the tail function of this list sort. - /// - public FuncDecl TailDecl - { - get - { - Contract.Ensures(Contract.Result() != 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 - }; - - /// - /// Relation sorts. - /// - [ContractVerification(true)] - public class RelationSort : Sort - { - /// - /// The arity of the relation sort. - /// - public uint Arity - { - get { return Native.Z3_get_relation_arity(Context.nCtx, NativeObject); } - } - - /// - /// The sorts of the columns of the relation sort. - /// - public Sort[] ColumnSorts - { - get - { - Contract.Ensures(Contract.Result() != 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 - } - - /// - /// Finite domain sorts. - /// - [ContractVerification(true)] - public class FiniteDomainSort : Sort - { - /// - /// The size of the finite domain sort. - /// - 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 - } - - /// - /// Set sorts. - /// - [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 - } + } } diff --git a/src/api/dotnet/Statistics.cs b/src/api/dotnet/Statistics.cs index 0897c31ee..408995140 100644 --- a/src/api/dotnet/Statistics.cs +++ b/src/api/dotnet/Statistics.cs @@ -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) { diff --git a/src/api/dotnet/StringSymbol.cs b/src/api/dotnet/StringSymbol.cs new file mode 100644 index 000000000..e311fb958 --- /dev/null +++ b/src/api/dotnet/StringSymbol.cs @@ -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 +{ + + /// + /// Named symbols + /// + [ContractVerification(true)] + public class StringSymbol : Symbol + { + /// + /// The string value of the symbol. + /// + /// Throws an exception if the symbol is not of string kind. + public string String + { + get + { + Contract.Ensures(Contract.Result() != 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 + } +} diff --git a/src/api/dotnet/Symbol.cs b/src/api/dotnet/Symbol.cs index ba991cdaa..783647d3f 100644 --- a/src/api/dotnet/Symbol.cs +++ b/src/api/dotnet/Symbol.cs @@ -90,92 +90,4 @@ namespace Microsoft.Z3 } #endregion } - - /// - /// Numbered symbols - /// - [ContractVerification(true)] - public class IntSymbol : Symbol - { - /// - /// The int value of the symbol. - /// - /// Throws an exception if the symbol is not of int kind. - 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 - } - - /// - /// Named symbols - /// - [ContractVerification(true)] - public class StringSymbol : Symbol - { - /// - /// The string value of the symbol. - /// - /// Throws an exception if the symbol is not of string kind. - public string String - { - get - { - Contract.Ensures(Contract.Result() != 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 - } } diff --git a/src/api/dotnet/Tactic.cs b/src/api/dotnet/Tactic.cs index 6340c9b41..eb4ef085c 100644 --- a/src/api/dotnet/Tactic.cs +++ b/src/api/dotnet/Tactic.cs @@ -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) { diff --git a/src/api/dotnet/TupleSort.cs b/src/api/dotnet/TupleSort.cs new file mode 100644 index 000000000..1e4af5cd7 --- /dev/null +++ b/src/api/dotnet/TupleSort.cs @@ -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 +{ + /// + /// Tuple sorts. + /// + [ContractVerification(true)] + public class TupleSort : Sort + { + /// + /// The constructor function of the tuple. + /// + public FuncDecl MkDecl + { + get + { + Contract.Ensures(Contract.Result() != null); + + return new FuncDecl(Context, Native.Z3_get_tuple_sort_mk_decl(Context.nCtx, NativeObject)); + } + } + + /// + /// The number of fields in the tuple. + /// + public uint NumFields + { + get { return Native.Z3_get_tuple_sort_num_fields(Context.nCtx, NativeObject); } + } + + /// + /// The field declarations. + /// + public FuncDecl[] FieldDecls + { + get + { + Contract.Ensures(Contract.Result() != 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 + }; +} diff --git a/src/api/dotnet/UninterpretedSort.cs b/src/api/dotnet/UninterpretedSort.cs new file mode 100644 index 000000000..154818faf --- /dev/null +++ b/src/api/dotnet/UninterpretedSort.cs @@ -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 +{ + /// + /// Uninterpreted Sorts + /// + 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 + } +}