diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs index 94b69d206..3432c8028 100644 --- a/src/api/dotnet/Context.cs +++ b/src/api/dotnet/Context.cs @@ -231,7 +231,6 @@ namespace Microsoft.Z3 return new BitVecSort(this, Native.Z3_mk_bv_sort(nCtx, size)); } - /// /// Create a new sequence sort. /// @@ -485,7 +484,7 @@ namespace Microsoft.Z3 /// The function performs a record update at t. The field /// that is passed in as argument is updated with value v, /// the remaining fields of t are unchanged. - /// + /// public Expr MkUpdateField(FuncDecl field, Expr t, Expr v) { return Expr.Create(this, Native.Z3_datatype_update_field( @@ -560,14 +559,14 @@ namespace Microsoft.Z3 /// MkRecFuncDecl. The body may contain recursive uses of the function or /// other mutually recursive functions. /// - public void AddRecDef(FuncDecl f, Expr[] args, Expr body) - { - CheckContextMatch(f); - CheckContextMatch(args); - CheckContextMatch(body); + public void AddRecDef(FuncDecl f, Expr[] args, Expr body) + { + CheckContextMatch(f); + CheckContextMatch(args); + CheckContextMatch(body); IntPtr[] argsNative = AST.ArrayToNative(args); - Native.Z3_add_rec_def(nCtx, f.NativeObject, (uint)args.Length, argsNative, body.NativeObject); - } + Native.Z3_add_rec_def(nCtx, f.NativeObject, (uint)args.Length, argsNative, body.NativeObject); + } /// /// Creates a new function declaration. @@ -811,7 +810,7 @@ namespace Microsoft.Z3 public Expr MkApp(FuncDecl f, IEnumerable args) { Debug.Assert(f != null); - Debug.Assert(args == null || args.All( a => a != null)); + Debug.Assert(args == null || args.All(a => a != null)); CheckContextMatch(f); CheckContextMatch(args); @@ -949,14 +948,15 @@ namespace Microsoft.Z3 Debug.Assert(ts.All(a => a != null)); CheckContextMatch(ts); BoolExpr r = null; - foreach (var t in ts) { - if (r == null) - r = t; + foreach (var t in ts) + { + if (r == null) + r = t; else - r = MkXor(r, t); + r = MkXor(r, t); } - if (r == null) - r = MkTrue(); + if (r == null) + r = MkTrue(); return r; } @@ -2343,7 +2343,7 @@ namespace Microsoft.Z3 CheckContextMatch(elem); CheckContextMatch(set); - return (BoolExpr) Expr.Create(this, Native.Z3_mk_set_member(nCtx, elem.NativeObject, set.NativeObject)); + return (BoolExpr)Expr.Create(this, Native.Z3_mk_set_member(nCtx, elem.NativeObject, set.NativeObject)); } /// @@ -2356,7 +2356,7 @@ namespace Microsoft.Z3 CheckContextMatch(arg1); CheckContextMatch(arg2); - return (BoolExpr) Expr.Create(this, Native.Z3_mk_set_subset(nCtx, arg1.NativeObject, arg2.NativeObject)); + return (BoolExpr)Expr.Create(this, Native.Z3_mk_set_subset(nCtx, arg1.NativeObject, arg2.NativeObject)); } #endregion @@ -2366,7 +2366,7 @@ namespace Microsoft.Z3 /// /// Create the empty sequence. /// - public SeqExpr MkEmptySeq(Sort s) + public SeqExpr MkEmptySeq(Sort s) { Debug.Assert(s != null); return new SeqExpr(this, Native.Z3_mk_seq_empty(nCtx, s.NativeObject)); @@ -2375,7 +2375,7 @@ namespace Microsoft.Z3 /// /// Create the singleton sequence. /// - public SeqExpr MkUnit(Expr elem) + public SeqExpr MkUnit(Expr elem) { Debug.Assert(elem != null); return new SeqExpr(this, Native.Z3_mk_seq_unit(nCtx, elem.NativeObject)); @@ -2384,7 +2384,7 @@ namespace Microsoft.Z3 /// /// Create a string constant. /// - public SeqExpr MkString(string s) + public SeqExpr MkString(string s) { Debug.Assert(s != null); return new SeqExpr(this, Native.Z3_mk_string(nCtx, s)); @@ -2393,7 +2393,7 @@ namespace Microsoft.Z3 /// /// Convert an integer expression to a string. /// - public SeqExpr IntToString(Expr e) + public SeqExpr IntToString(Expr e) { Debug.Assert(e != null); Debug.Assert(e is ArithExpr); @@ -2413,7 +2413,8 @@ namespace Microsoft.Z3 /// /// Convert a bit-vector expression, represented as an signed number, to a string. /// - public SeqExpr SbvToString(Expr e) { + public SeqExpr SbvToString(Expr e) + { Debug.Assert(e != null); Debug.Assert(e is ArithExpr); return new SeqExpr(this, Native.Z3_mk_sbv_to_str(nCtx, e.NativeObject)); @@ -2422,7 +2423,7 @@ namespace Microsoft.Z3 /// /// Convert an integer expression to a string. /// - public IntExpr StringToInt(Expr e) + public IntExpr StringToInt(Expr e) { Debug.Assert(e != null); Debug.Assert(e is SeqExpr); @@ -2449,13 +2450,13 @@ namespace Microsoft.Z3 public IntExpr MkLength(SeqExpr s) { Debug.Assert(s != null); - return (IntExpr) Expr.Create(this, Native.Z3_mk_seq_length(nCtx, s.NativeObject)); + return (IntExpr)Expr.Create(this, Native.Z3_mk_seq_length(nCtx, s.NativeObject)); } /// /// Check for sequence prefix. /// - public BoolExpr MkPrefixOf(SeqExpr s1, SeqExpr s2) + public BoolExpr MkPrefixOf(SeqExpr s1, SeqExpr s2) { Debug.Assert(s1 != null); Debug.Assert(s2 != null); @@ -2466,7 +2467,7 @@ namespace Microsoft.Z3 /// /// Check for sequence suffix. /// - public BoolExpr MkSuffixOf(SeqExpr s1, SeqExpr s2) + public BoolExpr MkSuffixOf(SeqExpr s1, SeqExpr s2) { Debug.Assert(s1 != null); Debug.Assert(s2 != null); @@ -2477,7 +2478,7 @@ namespace Microsoft.Z3 /// /// Check for sequence containment of s2 in s1. /// - public BoolExpr MkContains(SeqExpr s1, SeqExpr s2) + public BoolExpr MkContains(SeqExpr s1, SeqExpr s2) { Debug.Assert(s1 != null); Debug.Assert(s2 != null); @@ -2488,7 +2489,7 @@ namespace Microsoft.Z3 /// /// Check if the string s1 is lexicographically strictly less than s2. /// - public BoolExpr MkStringLt(SeqExpr s1, SeqExpr s2) + public BoolExpr MkStringLt(SeqExpr s1, SeqExpr s2) { Debug.Assert(s1 != null); Debug.Assert(s2 != null); @@ -2499,7 +2500,7 @@ namespace Microsoft.Z3 /// /// Check if the string s1 is lexicographically less or equal to s2. /// - public BoolExpr MkStringLe(SeqExpr s1, SeqExpr s2) + public BoolExpr MkStringLe(SeqExpr s1, SeqExpr s2) { Debug.Assert(s1 != null); Debug.Assert(s2 != null); @@ -2568,10 +2569,10 @@ namespace Microsoft.Z3 /// /// Convert a regular expression that accepts sequence s. /// - public ReExpr MkToRe(SeqExpr s) + public ReExpr MkToRe(SeqExpr s) { Debug.Assert(s != null); - return new ReExpr(this, Native.Z3_mk_seq_to_re(nCtx, s.NativeObject)); + return new ReExpr(this, Native.Z3_mk_seq_to_re(nCtx, s.NativeObject)); } @@ -2583,7 +2584,7 @@ namespace Microsoft.Z3 Debug.Assert(s != null); Debug.Assert(re != null); CheckContextMatch(s, re); - return new BoolExpr(this, Native.Z3_mk_seq_in_re(nCtx, s.NativeObject, re.NativeObject)); + return new BoolExpr(this, Native.Z3_mk_seq_in_re(nCtx, s.NativeObject, re.NativeObject)); } /// @@ -2592,7 +2593,7 @@ namespace Microsoft.Z3 public ReExpr MkStar(ReExpr re) { Debug.Assert(re != null); - return new ReExpr(this, Native.Z3_mk_re_star(nCtx, re.NativeObject)); + return new ReExpr(this, Native.Z3_mk_re_star(nCtx, re.NativeObject)); } /// @@ -2601,7 +2602,7 @@ namespace Microsoft.Z3 public ReExpr MkLoop(ReExpr re, uint lo, uint hi = 0) { Debug.Assert(re != null); - return new ReExpr(this, Native.Z3_mk_re_loop(nCtx, re.NativeObject, lo, hi)); + return new ReExpr(this, Native.Z3_mk_re_loop(nCtx, re.NativeObject, lo, hi)); } /// @@ -2610,7 +2611,7 @@ namespace Microsoft.Z3 public ReExpr MkPlus(ReExpr re) { Debug.Assert(re != null); - return new ReExpr(this, Native.Z3_mk_re_plus(nCtx, re.NativeObject)); + return new ReExpr(this, Native.Z3_mk_re_plus(nCtx, re.NativeObject)); } /// @@ -2619,7 +2620,7 @@ namespace Microsoft.Z3 public ReExpr MkOption(ReExpr re) { Debug.Assert(re != null); - return new ReExpr(this, Native.Z3_mk_re_option(nCtx, re.NativeObject)); + return new ReExpr(this, Native.Z3_mk_re_option(nCtx, re.NativeObject)); } /// @@ -2628,7 +2629,7 @@ namespace Microsoft.Z3 public ReExpr MkComplement(ReExpr re) { Debug.Assert(re != null); - return new ReExpr(this, Native.Z3_mk_re_complement(nCtx, re.NativeObject)); + return new ReExpr(this, Native.Z3_mk_re_complement(nCtx, re.NativeObject)); } /// @@ -2670,7 +2671,7 @@ namespace Microsoft.Z3 /// /// Create a difference regular expression. /// - public ReExpr MkDiff(ReExpr a, ReExpr b) + public ReExpr MkDiff(ReExpr a, ReExpr b) { Debug.Assert(a != null); Debug.Assert(b != null); @@ -2682,7 +2683,7 @@ namespace Microsoft.Z3 /// Create the empty regular expression. /// The sort s should be a regular expression. /// - public ReExpr MkEmptyRe(Sort s) + public ReExpr MkEmptyRe(Sort s) { Debug.Assert(s != null); return new ReExpr(this, Native.Z3_mk_re_empty(nCtx, s.NativeObject)); @@ -2692,7 +2693,7 @@ namespace Microsoft.Z3 /// Create the full regular expression. /// The sort s should be a regular expression. /// - public ReExpr MkFullRe(Sort s) + public ReExpr MkFullRe(Sort s) { Debug.Assert(s != null); return new ReExpr(this, Native.Z3_mk_re_full(nCtx, s.NativeObject)); @@ -2702,7 +2703,7 @@ namespace Microsoft.Z3 /// /// Create a range expression. /// - public ReExpr MkRange(SeqExpr lo, SeqExpr hi) + public ReExpr MkRange(SeqExpr lo, SeqExpr hi) { Debug.Assert(lo != null); Debug.Assert(hi != null); @@ -2713,7 +2714,7 @@ namespace Microsoft.Z3 /// /// Create less than or equal to between two characters. /// - public BoolExpr MkCharLe(Expr ch1, Expr ch2) + public BoolExpr MkCharLe(Expr ch1, Expr ch2) { Debug.Assert(ch1 != null); Debug.Assert(ch2 != null); @@ -2723,7 +2724,7 @@ namespace Microsoft.Z3 /// /// Create an integer (code point) from character. /// - public IntExpr CharToInt(Expr ch) + public IntExpr CharToInt(Expr ch) { Debug.Assert(ch != null); return new IntExpr(this, Native.Z3_mk_char_to_int(nCtx, ch.NativeObject)); @@ -2732,7 +2733,7 @@ namespace Microsoft.Z3 /// /// Create a bit-vector (code point) from character. /// - public BitVecExpr CharToBV(Expr ch) + public BitVecExpr CharToBV(Expr ch) { Debug.Assert(ch != null); return new BitVecExpr(this, Native.Z3_mk_char_to_bv(nCtx, ch.NativeObject)); @@ -2741,7 +2742,7 @@ namespace Microsoft.Z3 /// /// Create a character from a bit-vector (code point). /// - public Expr CharFromBV(BitVecExpr bv) + public Expr CharFromBV(BitVecExpr bv) { Debug.Assert(bv != null); return new Expr(this, Native.Z3_mk_char_from_bv(nCtx, bv.NativeObject)); @@ -2750,7 +2751,7 @@ namespace Microsoft.Z3 /// /// Create a check if the character is a digit. /// - public BoolExpr MkIsDigit(Expr ch) + public BoolExpr MkIsDigit(Expr ch) { Debug.Assert(ch != null); return new BoolExpr(this, Native.Z3_mk_char_is_digit(nCtx, ch.NativeObject)); @@ -2768,7 +2769,7 @@ namespace Microsoft.Z3 Debug.Assert(args != null); CheckContextMatch(args); var ts = args.ToArray(); - return new BoolExpr(this, Native.Z3_mk_atmost(nCtx, (uint) ts.Length, + return new BoolExpr(this, Native.Z3_mk_atmost(nCtx, (uint)ts.Length, AST.ArrayToNative(ts), k)); } @@ -2780,7 +2781,7 @@ namespace Microsoft.Z3 Debug.Assert(args != null); CheckContextMatch(args); var ts = args.ToArray(); - return new BoolExpr(this, Native.Z3_mk_atleast(nCtx, (uint) ts.Length, + return new BoolExpr(this, Native.Z3_mk_atleast(nCtx, (uint)ts.Length, AST.ArrayToNative(ts), k)); } @@ -2789,13 +2790,13 @@ namespace Microsoft.Z3 /// public BoolExpr MkPBLe(int[] coeffs, BoolExpr[] args, int k) { - Debug.Assert(args != null); - Debug.Assert(coeffs != null); - Debug.Assert(args.Length == coeffs.Length); - CheckContextMatch(args); - return new BoolExpr(this, Native.Z3_mk_pble(nCtx, (uint) args.Length, - AST.ArrayToNative(args), - coeffs, k)); + Debug.Assert(args != null); + Debug.Assert(coeffs != null); + Debug.Assert(args.Length == coeffs.Length); + CheckContextMatch(args); + return new BoolExpr(this, Native.Z3_mk_pble(nCtx, (uint)args.Length, + AST.ArrayToNative(args), + coeffs, k)); } /// @@ -2803,26 +2804,26 @@ namespace Microsoft.Z3 /// public BoolExpr MkPBGe(int[] coeffs, BoolExpr[] args, int k) { - Debug.Assert(args != null); - Debug.Assert(coeffs != null); - Debug.Assert(args.Length == coeffs.Length); - CheckContextMatch(args); - return new BoolExpr(this, Native.Z3_mk_pbge(nCtx, (uint) args.Length, - AST.ArrayToNative(args), - coeffs, k)); + Debug.Assert(args != null); + Debug.Assert(coeffs != null); + Debug.Assert(args.Length == coeffs.Length); + CheckContextMatch(args); + return new BoolExpr(this, Native.Z3_mk_pbge(nCtx, (uint)args.Length, + AST.ArrayToNative(args), + coeffs, k)); } /// /// Create a pseudo-Boolean equal constraint. /// public BoolExpr MkPBEq(int[] coeffs, BoolExpr[] args, int k) { - Debug.Assert(args != null); - Debug.Assert(coeffs != null); - Debug.Assert(args.Length == coeffs.Length); - CheckContextMatch(args); - return new BoolExpr(this, Native.Z3_mk_pbeq(nCtx, (uint) args.Length, - AST.ArrayToNative(args), - coeffs, k)); + Debug.Assert(args != null); + Debug.Assert(coeffs != null); + Debug.Assert(args.Length == coeffs.Length); + CheckContextMatch(args); + return new BoolExpr(this, Native.Z3_mk_pbeq(nCtx, (uint)args.Length, + AST.ArrayToNative(args), + coeffs, k)); } #endregion @@ -4085,7 +4086,7 @@ namespace Microsoft.Z3 /// indicates whether the result should be negative. public FPNum MkFPZero(FPSort s, bool negative) { - return new FPNum(this, Native.Z3_mk_fpa_zero(nCtx, s.NativeObject, (byte)(negative ? 1 : 0))); + return new FPNum(this, Native.Z3_mk_fpa_zero(nCtx, s.NativeObject, (byte)(negative ? 1 : 0))); } /// @@ -4127,7 +4128,7 @@ namespace Microsoft.Z3 /// FloatingPoint sort. public FPNum MkFPNumeral(bool sgn, uint sig, int exp, FPSort s) { - return new FPNum(this, Native.Z3_mk_fpa_numeral_int_uint(nCtx, (byte)(sgn ? 1 : 0), exp, sig, s.NativeObject)); + return new FPNum(this, Native.Z3_mk_fpa_numeral_int_uint(nCtx, (byte)(sgn ? 1 : 0), exp, sig, s.NativeObject)); } /// @@ -4139,7 +4140,7 @@ namespace Microsoft.Z3 /// FloatingPoint sort. public FPNum MkFPNumeral(bool sgn, Int64 exp, UInt64 sig, FPSort s) { - return new FPNum(this, Native.Z3_mk_fpa_numeral_int64_uint64(nCtx, (byte)(sgn ? 1 : 0), exp, sig, s.NativeObject)); + return new FPNum(this, Native.Z3_mk_fpa_numeral_int64_uint64(nCtx, (byte)(sgn ? 1 : 0), exp, sig, s.NativeObject)); } /// @@ -4825,12 +4826,12 @@ namespace Microsoft.Z3 /// /// ASTVector DRQ /// - public IDecRefQueue ASTVector_DRQ { get { return m_ASTVector_DRQ; } } + public IDecRefQueue ASTVector_DRQ { get { return m_ASTVector_DRQ; } } /// /// ApplyResult DRQ /// - public IDecRefQueue ApplyResult_DRQ { get { return m_ApplyResult_DRQ; } } + public IDecRefQueue ApplyResult_DRQ { get { return m_ApplyResult_DRQ; } } /// /// FuncEntry DRQ @@ -4937,7 +4938,7 @@ namespace Microsoft.Z3 m_ctx = IntPtr.Zero; Native.Z3_del_context(ctx); } - else + else GC.ReRegisterForFinalize(this); } #endregion diff --git a/src/api/dotnet/NativeContext.cs b/src/api/dotnet/NativeContext.cs index a19e0c5af..42a9bab90 100644 --- a/src/api/dotnet/NativeContext.cs +++ b/src/api/dotnet/NativeContext.cs @@ -1,48 +1,55 @@ -using System; -using System.Diagnostics; -using System.Collections.Generic; -using System.Runtime.InteropServices; -using System.Linq; - namespace Microsoft.Z3 { - using Z3_symbol = System.IntPtr; - using Z3_config = System.IntPtr; - using Z3_context = System.IntPtr; - using Z3_ast = System.IntPtr; using Z3_app = System.IntPtr; - using Z3_sort = System.IntPtr; + using Z3_ast = System.IntPtr; + using Z3_ast_vector = System.IntPtr; using Z3_func_decl = System.IntPtr; using Z3_pattern = System.IntPtr; - using Z3_model = System.IntPtr; - using Z3_literals = System.IntPtr; - using Z3_constructor = System.IntPtr; - using Z3_constructor_list = System.IntPtr; using Z3_solver = System.IntPtr; - using Z3_solver_callback = System.IntPtr; - using Z3_goal = System.IntPtr; - using Z3_tactic = System.IntPtr; - using Z3_params = System.IntPtr; - using Z3_probe = System.IntPtr; + using Z3_sort = System.IntPtr; using Z3_stats = System.IntPtr; - using Z3_ast_vector = System.IntPtr; - using Z3_ast_map = System.IntPtr; - using Z3_apply_result = System.IntPtr; - using Z3_func_interp = System.IntPtr; - using Z3_func_entry = System.IntPtr; - using Z3_fixedpoint = System.IntPtr; - using Z3_optimize = System.IntPtr; - using Z3_param_descrs = System.IntPtr; - using Z3_rcf_num = System.IntPtr; + using Z3_symbol = System.IntPtr; /// /// The main interaction with Z3 happens via the Context. /// NativeContext allows for efficient wrapper-reduced interaction with Z3 /// expressions. /// - - public class NativeContext + public class NativeContext : IDisposable { + /// + /// Constructor. + /// + /// + /// The following parameters can be set: + /// - proof (Boolean) Enable proof generation + /// - debug_ref_count (Boolean) Enable debug support for Z3_ast reference counting + /// - trace (Boolean) Tracing support for VCC + /// - trace_file_name (String) Trace out file for VCC traces + /// - timeout (unsigned) default timeout (in milliseconds) used for solvers + /// - well_sorted_check type checker + /// - auto_config use heuristics to automatically select solver and configure it + /// - model model generation for solvers, this parameter can be overwritten when creating a solver + /// - model_validate validate models produced by solvers + /// - unsat_core unsat-core generation for solvers, this parameter can be overwritten when creating a solver + /// Note that in previous versions of Z3, this constructor was also used to set global and module parameters. + /// For this purpose we should now use + /// + public NativeContext(Dictionary settings) + : base() + { + Debug.Assert(settings != null); + + lock (creation_lock) + { + IntPtr cfg = Native.Z3_mk_config(); + foreach (KeyValuePair kv in settings) + Native.Z3_set_param_value(cfg, kv.Key, kv.Value); + m_ctx = Native.Z3_mk_context_rc(cfg); + Native.Z3_del_config(cfg); + InitContext(); + } + } #region Arithmetic /// @@ -53,9 +60,669 @@ namespace Microsoft.Z3 { Debug.Assert(t != null); Debug.Assert(t.All(a => a != IntPtr.Zero)); - return Native.Z3_mk_add(nCtx, (uint)t.Length, t); + + return Native.Z3_mk_add(nCtx, (uint)(t?.Length ?? 0), t); } + /// + /// Create an expression representing t[0] * t[1] * .... + /// + public Z3_ast MkMul(params Z3_ast[] t) + { + Debug.Assert(t != null); + Debug.Assert(t.All(a => a != IntPtr.Zero)); + + var ts = t.ToArray(); + return Native.Z3_mk_mul(nCtx, (uint)(ts?.Length ?? 0), ts); + } + + /// + /// Create an expression representing t1 / t2. + /// + public Z3_ast MkDiv(Z3_ast t1, Z3_ast t2) + { + Debug.Assert(t1 != IntPtr.Zero); + Debug.Assert(t2 != IntPtr.Zero); + + return Native.Z3_mk_div(nCtx, t1, t2); + } + + /// + /// Create an expression representing t1 <= t2 + /// + public Z3_ast MkLe(Z3_ast t1, Z3_ast t2) + { + Debug.Assert(t1 != IntPtr.Zero); + Debug.Assert(t2 != IntPtr.Zero); + + return Native.Z3_mk_le(nCtx, t1, t2); + } + + /// + /// Create an expression representing t1 < t2 + /// + public Z3_ast MkLt(Z3_ast t1, Z3_ast t2) + { + Debug.Assert(t1 != IntPtr.Zero); + Debug.Assert(t2 != IntPtr.Zero); + + return Native.Z3_mk_lt(nCtx, t1, t2); + } + + /// + /// Create an expression representing t1 >= t2 + /// + public Z3_ast MkGe(Z3_ast t1, Z3_ast t2) + { + Debug.Assert(t1 != IntPtr.Zero); + Debug.Assert(t2 != IntPtr.Zero); + + return Native.Z3_mk_ge(nCtx, t1, t2); + } + + /// + /// Create an expression representing t1 > t2 + /// + public Z3_ast MkGt(Z3_ast t1, Z3_ast t2) + { + Debug.Assert(t1 != IntPtr.Zero); + Debug.Assert(t2 != IntPtr.Zero); + + return Native.Z3_mk_gt(nCtx, t1, t2); + } + + /// + /// Unsigned less-than + /// + /// + /// The arguments must have the same bit-vector sort. + /// + public Z3_ast MkBvUlt(Z3_ast t1, Z3_ast t2) + { + Debug.Assert(t1 != IntPtr.Zero); + Debug.Assert(t2 != IntPtr.Zero); + + return Native.Z3_mk_bvult(nCtx, t1, t2); + } + + /// + /// Unsigned less-than-equal + /// + /// + /// The arguments must have the same bit-vector sort. + /// + public Z3_ast MkBvUle(Z3_ast t1, Z3_ast t2) + { + Debug.Assert(t1 != IntPtr.Zero); + Debug.Assert(t2 != IntPtr.Zero); + + return Native.Z3_mk_bvule(nCtx, t1, t2); + } + + /// + /// Creates the equality = . + /// + public Z3_ast MkEq(Z3_ast x, Z3_ast y) + { + Debug.Assert(x != IntPtr.Zero); + Debug.Assert(y != IntPtr.Zero); + + return Native.Z3_mk_eq(nCtx, x, y); + } + + /// + /// Mk an expression representing not(a). + /// + public Z3_ast MkNot(Z3_ast a) + { + Debug.Assert(a != IntPtr.Zero); + + return Native.Z3_mk_not(nCtx, a); + } + + /// + /// Create an expression representing t[0] and t[1] and .... + /// + public Z3_ast MkAnd(params Z3_ast[] t) + { + Debug.Assert(t != null); + Debug.Assert(t.All(a => a != IntPtr.Zero)); + + return Native.Z3_mk_and(nCtx, (uint)(t?.Length ?? 0), t); + } + + /// + /// Create an expression representing t[0] or t[1] or .... + /// + public Z3_ast MkOr(params Z3_ast[] t) + { + Debug.Assert(t != null); + Debug.Assert(t.All(a => a != IntPtr.Zero)); + + return Native.Z3_mk_or(nCtx, (uint)(t?.Length ?? 0), t); + } + + + /// + /// Create a real numeral. + /// + /// A string representing the Term value in decimal notation. + /// A Term with value and sort Real + public Z3_ast MkReal(string v, Z3_sort realSort) + { + Debug.Assert(!string.IsNullOrEmpty(v)); + + return Native.Z3_mk_numeral(nCtx, v, realSort); + } + + /// + /// Create a Term of a given sort. This function can be used to create numerals that fit in a machine integer. + /// + /// Value of the numeral + /// Sort of the numeral + public Z3_ast MkNumeral(int v, Z3_sort sort) + { + Debug.Assert(sort != IntPtr.Zero); + + return Native.Z3_mk_int(nCtx, v, sort); + } + + /// + /// Create a Term of a given sort. This function can be used to create numerals that fit in a machine integer. + /// + /// Value of the numeral + /// Sort of the numeral + public Z3_ast MkNumeral(uint v, Z3_sort sort) + { + Debug.Assert(sort != null); + + return Native.Z3_mk_unsigned_int(nCtx, v, sort); + } + + /// + /// Create a Term of a given sort. This function can be used to create numerals that fit in a machine integer. + /// + /// Value of the numeral + /// Sort of the numeral + public Z3_ast MkNumeral(long v, Z3_sort sort) + { + Debug.Assert(sort != null); + + return Native.Z3_mk_int64(nCtx, v, sort); + } + + /// + /// Create an expression representing an if-then-else: ite(t1, t2, t3). + /// + /// An expression with Boolean sort + /// An expression + /// An expression with the same sort as + public Z3_ast MkIte(Z3_ast t1, Z3_ast t2, Z3_ast t3) + { + Debug.Assert(t1 != IntPtr.Zero); + Debug.Assert(t2 != IntPtr.Zero); + Debug.Assert(t3 != IntPtr.Zero); + + return Native.Z3_mk_ite(nCtx, t1, t2, t3); + } + + /// + /// Create an expression representing t1 -> t2. + /// + public Z3_ast MkImplies(Z3_ast t1, Z3_ast t2) + { + Debug.Assert(t1 != IntPtr.Zero); + Debug.Assert(t2 != IntPtr.Zero); + + return Native.Z3_mk_implies(nCtx, t1, t2); + } + + #endregion + + #region Sort + + public Z3_sort MkIntSort() => Native.Z3_mk_int_sort(nCtx); + public Z3_sort MkBoolSort() => Native.Z3_mk_bool_sort(nCtx); + public Z3_sort MkBvSort(uint size) => Native.Z3_mk_bv_sort(nCtx, size); + public Z3_sort MkRealSort() => Native.Z3_mk_real_sort(nCtx); + + public Z3_sort MkListSort(string name, Z3_sort elemSort, + out Z3_func_decl inil, out Z3_func_decl iisnil, + out Z3_func_decl icons, out Z3_func_decl iiscons, + out Z3_func_decl ihead, out Z3_func_decl itail) + { + Debug.Assert(!string.IsNullOrEmpty(name)); + Debug.Assert(elemSort != IntPtr.Zero); + + IntPtr nil = IntPtr.Zero, isnil = IntPtr.Zero, + cons = IntPtr.Zero, iscons = IntPtr.Zero, + head = IntPtr.Zero, tail = IntPtr.Zero; + + var symbol = Native.Z3_mk_string_symbol(nCtx, name); + var sort = Native.Z3_mk_list_sort(nCtx, symbol, elemSort, + ref nil, ref isnil, ref cons, ref iscons, ref head, ref tail); + + inil = nil; + iisnil = isnil; + icons = cons; + iiscons = iscons; + ihead = head; + itail = tail; + + return sort; + } + + /// + /// Create a new array sort. + /// + public Z3_sort MkArraySort(Z3_sort domain, Z3_sort range) + { + Debug.Assert(domain != IntPtr.Zero); + Debug.Assert(range != IntPtr.Zero); + + return Native.Z3_mk_array_sort(nCtx, domain, range); + } + + /// + /// Create a new tuple sort. + /// + public Z3_sort MkTupleSort(Z3_symbol name, Z3_symbol[] fieldNames, Z3_sort[] fieldSorts, out Z3_func_decl constructor, Z3_func_decl[] projections) + { + Debug.Assert(name != IntPtr.Zero); + Debug.Assert(fieldNames != null); + Debug.Assert(fieldNames.All(fn => fn != IntPtr.Zero)); + Debug.Assert(fieldSorts == null || fieldSorts.All(fs => fs != IntPtr.Zero)); + + var numFields = (uint)(fieldNames?.Length ?? 0); + constructor = IntPtr.Zero; + return Native.Z3_mk_tuple_sort(nCtx, name, numFields, fieldNames, fieldSorts, ref constructor, projections); + } + + #endregion + + #region Propositional + /// + /// The true Term. + /// + public Z3_ast MkTrue() => Native.Z3_mk_true(nCtx); + + /// + /// The false Term. + /// + public Z3_ast MkFalse() => Native.Z3_mk_false(nCtx); + + /// + /// Creates a Boolean value. + /// + public Z3_ast MkBool(bool value) + { + + return value ? MkTrue() : MkFalse(); + } + + /// + /// Create an expression representing t1 iff t2. + /// + public Z3_ast MkIff(Z3_ast t1, Z3_ast t2) + { + Debug.Assert(t1 != IntPtr.Zero); + Debug.Assert(t2 != IntPtr.Zero); + + return Native.Z3_mk_iff(nCtx, t1, t2); + } + #endregion + + #region Constants + /// + /// Creates a new Constant of sort and named . + /// + public Z3_ast MkConst(string name, Z3_sort range) + { + Debug.Assert(!string.IsNullOrEmpty(name)); + Debug.Assert(range != IntPtr.Zero); + + return Native.Z3_mk_const(nCtx, MkStringSymbol(name), range); + } + + #endregion + + #region Symbol + public Z3_symbol MkStringSymbol(string name) + { + Debug.Assert(!string.IsNullOrEmpty(name)); + + return Native.Z3_mk_string_symbol(nCtx, name); + } + #endregion + + #region Terms + /// + /// Create a new function application. + /// + public Z3_ast MkApp(Z3_func_decl f, params Z3_ast[] args) + { + Debug.Assert(f != IntPtr.Zero); + Debug.Assert(args == null || args.All(a => a != IntPtr.Zero)); + + return Native.Z3_mk_app(nCtx, f, (uint)(args?.Length ?? 0), args); + } + + #endregion + + #region Bound Variables + /// + /// Creates a new bound variable. + /// + /// The de-Bruijn index of the variable + /// The sort of the variable + public Z3_ast MkBound(uint index, Z3_sort sort) + { + Debug.Assert(sort != IntPtr.Zero); + + return Native.Z3_mk_bound(nCtx, index, sort); + } + #endregion + + #region Bit-vectors + /// + /// Bitwise conjunction. + /// + /// The arguments must have a bit-vector sort. + public Z3_ast_vector MkBvAnd(Z3_ast_vector t1, Z3_ast_vector t2) + { + Debug.Assert(t1 != IntPtr.Zero); + Debug.Assert(t2 != IntPtr.Zero); + + return Native.Z3_mk_bvand(nCtx, t1, t2); + } + + /// + /// Bitwise negation. + /// + /// The argument must have a bit-vector sort. + public Z3_ast_vector MkBvNot(Z3_ast_vector t) + { + Debug.Assert(t != IntPtr.Zero); + + return Native.Z3_mk_bvnot(nCtx, t); + } + + /// + /// Standard two's complement unary minus. + /// + /// The arguments must have a bit-vector sort. + public Z3_ast_vector MkBvNeg(Z3_ast_vector t) + { + Debug.Assert(t != IntPtr.Zero); + + return Native.Z3_mk_bvneg(nCtx, t); + } + + /// + /// Standard two's complement unary minus. + /// + /// The arguments must have a bit-vector sort. + public Z3_ast_vector MkBVNeg(Z3_ast_vector t) + { + Debug.Assert(t != IntPtr.Zero); + + return Native.Z3_mk_bvneg(nCtx, t); + } + + /// + /// Two's complement addition. + /// + /// The arguments must have the same bit-vector sort. + public Z3_ast_vector MkBvAdd(Z3_ast_vector t1, Z3_ast_vector t2) + { + Debug.Assert(t1 != IntPtr.Zero); + Debug.Assert(t2 != IntPtr.Zero); + + return Native.Z3_mk_bvadd(nCtx, t1, t2); + } + + /// + /// Bit-vector extraction. + /// + /// + /// Extract the bits down to from a bitvector of + /// size m to yield a new bitvector of size n, where + /// n = high - low + 1. + /// The argument must have a bit-vector sort. + /// + public Z3_ast_vector MkBvExtract(uint high, uint low, Z3_ast_vector t) + { + Debug.Assert(t != IntPtr.Zero); + + return Native.Z3_mk_extract(nCtx, high, low, t); + } + + /// + /// Bit-vector sign extension. + /// + /// + /// Sign-extends the given bit-vector to the (signed) equivalent bitvector of + /// size m+i, where \c m is the size of the given bit-vector. + /// The argument must have a bit-vector sort. + /// + public Z3_ast_vector MkBvSignExt(uint i, Z3_ast_vector t) + { + Debug.Assert(t != IntPtr.Zero); + + return Native.Z3_mk_sign_ext(nCtx, i, t); + } + + /// + /// Bit-vector zero extension. + /// + /// + /// Extend the given bit-vector with zeros to the (unsigned) equivalent + /// bitvector of size m+i, where \c m is the size of the + /// given bit-vector. + /// The argument must have a bit-vector sort. + /// + public Z3_ast_vector MkBvZeroExt(uint i, Z3_ast_vector t) + { + Debug.Assert(t != IntPtr.Zero); + + return Native.Z3_mk_zero_ext(nCtx, i, t); + } + + /// + /// Shift left. + /// + /// + /// It is equivalent to multiplication by 2^x where \c x is the value of . + /// + /// NB. The semantics of shift operations varies between environments. This + /// definition does not necessarily capture directly the semantics of the + /// programming language or assembly architecture you are modeling. + /// + /// The arguments must have a bit-vector sort. + /// + public Z3_ast_vector MkBvShl(Z3_ast_vector t1, Z3_ast_vector t2) + { + Debug.Assert(t1 != IntPtr.Zero); + Debug.Assert(t2 != IntPtr.Zero); + + return Native.Z3_mk_bvshl(nCtx, t1, t2); + } + + /// + /// Logical shift right + /// + /// + /// It is equivalent to unsigned division by 2^x where \c x is the value of . + /// + /// NB. The semantics of shift operations varies between environments. This + /// definition does not necessarily capture directly the semantics of the + /// programming language or assembly architecture you are modeling. + /// + /// The arguments must have a bit-vector sort. + /// + public Z3_ast_vector MkBvLshr(Z3_ast_vector t1, Z3_ast_vector t2) + { + Debug.Assert(t1 != IntPtr.Zero); + Debug.Assert(t2 != IntPtr.Zero); + + return Native.Z3_mk_bvlshr(nCtx, t1, t2); + } + + /// + /// Arithmetic shift right + /// + /// + /// It is like logical shift right except that the most significant + /// bits of the result always copy the most significant bit of the + /// second argument. + /// + /// NB. The semantics of shift operations varies between environments. This + /// definition does not necessarily capture directly the semantics of the + /// programming language or assembly architecture you are modeling. + /// + /// The arguments must have a bit-vector sort. + /// + public Z3_ast_vector MkBvAshr(Z3_ast_vector t1, Z3_ast_vector t2) + { + Debug.Assert(t1 != IntPtr.Zero); + Debug.Assert(t2 != IntPtr.Zero); + + return Native.Z3_mk_bvashr(nCtx, t1, t2); + } + + /// + /// Two's complement signed less-than + /// + /// + /// The arguments must have the same bit-vector sort. + /// + public Z3_ast MkBvSlt(Z3_ast_vector t1, Z3_ast_vector t2) + { + Debug.Assert(t1 != IntPtr.Zero); + Debug.Assert(t2 != IntPtr.Zero); + + return Native.Z3_mk_bvslt(nCtx, t1, t2); + } + + /// + /// Two's complement multiplication. + /// + /// The arguments must have the same bit-vector sort. + public Z3_ast_vector MkBvMul(Z3_ast_vector t1, Z3_ast_vector t2) + { + Debug.Assert(t1 != IntPtr.Zero); + Debug.Assert(t2 != IntPtr.Zero); + + return Native.Z3_mk_bvmul(nCtx, t1, t2); + } + + /// + /// Unsigned division. + /// + /// + /// It is defined as the floor of t1/t2 if \c t2 is + /// different from zero. If t2 is zero, then the result + /// is undefined. + /// The arguments must have the same bit-vector sort. + /// + public Z3_ast_vector MkBvUdiv(Z3_ast_vector t1, Z3_ast_vector t2) + { + Debug.Assert(t1 != IntPtr.Zero); + Debug.Assert(t2 != IntPtr.Zero); + + return Native.Z3_mk_bvudiv(nCtx, t1, t2); + } + + /// + /// Signed division. + /// + /// + /// It is defined in the following way: + /// + /// - The \c floor of t1/t2 if \c t2 is different from zero, and t1*t2 >= 0. + /// + /// - The \c ceiling of t1/t2 if \c t2 is different from zero, and t1*t2 < 0. + /// + /// If t2 is zero, then the result is undefined. + /// The arguments must have the same bit-vector sort. + /// + public Z3_ast_vector MkBvSdiv(Z3_ast_vector t1, Z3_ast_vector t2) + { + Debug.Assert(t1 != IntPtr.Zero); + Debug.Assert(t2 != IntPtr.Zero); + + return Native.Z3_mk_bvsdiv(nCtx, t1, t2); + } + + /// + /// Unsigned remainder. + /// + /// + /// It is defined as t1 - (t1 /u t2) * t2, where /u represents unsigned division. + /// If t2 is zero, then the result is undefined. + /// The arguments must have the same bit-vector sort. + /// + public Z3_ast_vector MkBvUrem(Z3_ast_vector t1, Z3_ast_vector t2) + { + Debug.Assert(t1 != IntPtr.Zero); + Debug.Assert(t2 != IntPtr.Zero); + + return Native.Z3_mk_bvurem(nCtx, t1, t2); + } + + /// + /// Signed remainder. + /// + /// + /// It is defined as t1 - (t1 /s t2) * t2, where /s represents signed division. + /// The most significant bit (sign) of the result is equal to the most significant bit of \c t1. + /// + /// If t2 is zero, then the result is undefined. + /// The arguments must have the same bit-vector sort. + /// + public Z3_ast_vector MkBvSrem(Z3_ast_vector t1, Z3_ast_vector t2) + { + Debug.Assert(t1 != IntPtr.Zero); + Debug.Assert(t2 != IntPtr.Zero); + + return Native.Z3_mk_bvsrem(nCtx, t1, t2); + } + + /// + /// Two's complement subtraction. + /// + /// The arguments must have the same bit-vector sort. + public Z3_ast_vector MkBvSub(Z3_ast_vector t1, Z3_ast_vector t2) + { + Debug.Assert(t1 != IntPtr.Zero); + Debug.Assert(t2 != IntPtr.Zero); + + return Native.Z3_mk_bvsub(nCtx, t1, t2); + } + + /// + /// Bitwise disjunction. + /// + /// The arguments must have a bit-vector sort. + public Z3_ast_vector MkBvOr(Z3_ast_vector t1, Z3_ast_vector t2) + { + Debug.Assert(t1 != IntPtr.Zero); + Debug.Assert(t2 != IntPtr.Zero); + + return Native.Z3_mk_bvor(nCtx, t1, t2); + } + + /// + /// Bitwise XOR. + /// + /// The arguments must have a bit-vector sort. + public Z3_ast_vector MkBvXor(Z3_ast_vector t1, Z3_ast_vector t2) + { + Debug.Assert(t1 != null); + Debug.Assert(t2 != IntPtr.Zero); + + return Native.Z3_mk_bvxor(nCtx, t1, t2); + } #endregion #region Quantifiers @@ -83,11 +750,16 @@ namespace Microsoft.Z3 /// array containing the anti-patterns created using MkPattern. /// optional symbol to track quantifier. /// optional symbol to track skolem constants. - public Z3_ast MkForall(Z3_sort[] sorts, Symbol[] names, Z3_ast body, uint weight = 1, Z3_ast[] patterns = null, Z3_ast[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null) + public Z3_ast MkForall(Z3_sort[] sorts, Z3_symbol[] names, Z3_ast body, uint weight = 1, Z3_ast[] patterns = null, Z3_ast[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null) { return MkQuantifier(true, sorts, names, body, weight, patterns, noPatterns, quantifierID, skolemID); } + public Z3_ast MkExists(Z3_sort[] sorts, Z3_symbol[] names, Z3_ast body, uint weight = 1, Z3_ast[] patterns = null, Z3_ast[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null) + { + return MkQuantifier(false, sorts, names, body, weight, patterns, noPatterns, quantifierID, skolemID); + } + /// /// Create a quantified expression either forall or exists /// @@ -101,34 +773,33 @@ namespace Microsoft.Z3 /// /// /// - private Z3_ast MkQuantifier(bool is_forall, Z3_sort[] sorts, Symbol[] names, Z3_ast body, uint weight, Z3_ast[] patterns, Z3_ast[] noPatterns, Symbol quantifierID, Symbol skolemID) + private Z3_ast MkQuantifier(bool is_forall, Z3_sort[] sorts, Z3_symbol[] names, Z3_ast body, uint weight, Z3_ast[] patterns, Z3_ast[] noPatterns, Symbol quantifierID, Symbol skolemID) { Debug.Assert(sorts != null); Debug.Assert(names != null); Debug.Assert(body != null); Debug.Assert(sorts.Length == names.Length); Debug.Assert(sorts.All(s => s != IntPtr.Zero)); - Debug.Assert(names.All(n => n != null)); + Debug.Assert(names.All(n => n != IntPtr.Zero)); Debug.Assert(patterns == null || patterns.All(p => p != IntPtr.Zero)); Debug.Assert(noPatterns == null || noPatterns.All(np => np != IntPtr.Zero)); - uint numPatterns = patterns == null ? 0 : (uint)patterns.Length; - uint numNoPatterns = noPatterns == null ? 0 : (uint)noPatterns.Length; + if (noPatterns == null && quantifierID == null && skolemID == null) { return Native.Z3_mk_quantifier(nCtx, (byte)(is_forall ? 1 : 0), weight, - numPatterns, patterns, - (uint)sorts.Length, sorts, - Symbol.ArrayToNative(names), + (uint)(patterns?.Length ?? 0), patterns, + (uint)(sorts?.Length ?? 0), sorts, + names, body); } else { return Native.Z3_mk_quantifier_ex(nCtx, (byte)(is_forall ? 1 : 0), weight, AST.GetNativeObject(quantifierID), AST.GetNativeObject(skolemID), - numPatterns, patterns, - numNoPatterns, noPatterns, - (uint)sorts.Length, sorts, - Symbol.ArrayToNative(names), + (uint)(patterns?.Length ?? 0), patterns, + (uint)(noPatterns?.Length ?? 0), noPatterns, + (uint)(sorts?.Length ?? 0), sorts, + names, body); } } @@ -156,10 +827,421 @@ namespace Microsoft.Z3 { set { Native.Z3_set_ast_print_mode(nCtx, (uint)value); } } + #endregion + #region Arrays + + + /// + /// Create a constant array. + /// + /// + /// The resulting term is an array, such that a selecton an arbitrary index + /// produces the value v. + /// + public Z3_ast MkConstArray(Z3_sort domain, Z3_ast v) + { + Debug.Assert(domain != IntPtr.Zero); + Debug.Assert(v != IntPtr.Zero); + + return Native.Z3_mk_const_array(nCtx, domain, v); + } + + /// + /// Array update. + /// + /// + /// The node a must have an array sort [domain -> range], + /// i must have sort domain, + /// v must have sort range. The sort of the result is [domain -> range]. + /// The semantics of this function is given by the theory of arrays described in the SMT-LIB + /// standard. See http://smtlib.org for more details. + /// The result of this function is an array that is equal to a + /// (with respect to select) + /// on all indices except for i, where it maps to v + /// (and the select of a with + /// respect to i may be a different value). + /// + public Z3_ast MkStore(Z3_ast a, Z3_ast i, Z3_ast v) + { + Debug.Assert(a != IntPtr.Zero); + Debug.Assert(i != IntPtr.Zero); + Debug.Assert(v != IntPtr.Zero); + + return Native.Z3_mk_store(nCtx, a, i, v); + } + + /// + /// Array read. + /// + /// + /// The argument array is the array and index is the index + /// of the array that gets read. + /// + /// The node array must have an array sort [domain -> range], + /// and index must have the sort domain. + /// The sort of the result is range. + /// + public Z3_ast MkSelect(Z3_ast array, Z3_ast index) + { + Debug.Assert(array != IntPtr.Zero); + Debug.Assert(index != IntPtr.Zero); + + return Native.Z3_mk_select(nCtx, array, index); + } + + /// + /// Access the array default value. + /// + /// + /// Produces the default range value, for arrays that can be represented as + /// finite maps with a default range value. + /// + public Z3_ast MkDefault(Z3_ast a) + { + Debug.Assert(a != null); + + return Native.Z3_mk_array_default(nCtx, a); + } + + #endregion + + #region Function Declarations + + /// + /// Creates a new function declaration. + /// + public Z3_func_decl MkFuncDecl(string name, Z3_sort[] domain, Z3_sort range) + { + Debug.Assert(!string.IsNullOrEmpty(name)); + Debug.Assert(range != IntPtr.Zero); + Debug.Assert(domain != null); + Debug.Assert(domain.All(d => d != IntPtr.Zero)); + + var symbol = Native.Z3_mk_string_symbol(nCtx, name); + return Native.Z3_mk_func_decl(nCtx, symbol, (uint)(domain?.Length ?? 0), domain, range); + } + + /// + /// Creates a new function declaration. + /// + public Z3_func_decl MkFuncDecl(string name, Z3_sort domain, Z3_sort range) + { + Debug.Assert(!string.IsNullOrEmpty(name)); + Debug.Assert(range != IntPtr.Zero); + Debug.Assert(domain != IntPtr.Zero); + + var symbol = Native.Z3_mk_string_symbol(nCtx, name); + var q = new Z3_sort[] { domain }; + return Native.Z3_mk_func_decl(nCtx, symbol, (uint)q.Length, q, range); + } + + /// + /// Creates a fresh function declaration with a name prefixed with . + /// + public Z3_func_decl MkFreshFuncDecl(string prefix, Z3_sort[] domain, Z3_sort range) + { + Debug.Assert(domain != null); + Debug.Assert(range != IntPtr.Zero); + Debug.Assert(domain.All(d => d != IntPtr.Zero)); + + return Native.Z3_mk_fresh_func_decl(nCtx, prefix, (uint)(domain?.Length ?? 0), domain, range); + } + + /// + /// Creates a new constant function declaration. + /// + public Z3_func_decl MkConstDecl(string name, Z3_sort range) + { + Debug.Assert(range != IntPtr.Zero); + + var symbol = Native.Z3_mk_string_symbol(nCtx, name); + return Native.Z3_mk_func_decl(nCtx, symbol, 0, new IntPtr[0], range); + } + + /// + /// Get domain for a funcdecl + /// + /// + /// + public Z3_sort[] GetDomain(Z3_func_decl fdecl) + { + Debug.Assert(fdecl != IntPtr.Zero); + + var sz = Native.Z3_get_domain_size(nCtx, fdecl); + var domain = new Z3_sort[sz]; + for (uint i = 0; i < sz; i++) + { + domain[i] = Native.Z3_get_domain(nCtx, fdecl, i); + } + return domain; + } + + /// + /// Get range for a funcdecl + /// + /// + /// + public Z3_sort GetRange(Z3_func_decl fdecl) + { + Debug.Assert(fdecl != IntPtr.Zero); + + return Native.Z3_get_range(nCtx, fdecl); + } + + #endregion + + #region Quantifier Patterns + /// + /// Create a quantifier pattern. + /// + public Z3_pattern MkPattern(params Z3_ast[] terms) + { + Debug.Assert(terms != null); + if (terms == null || terms.Length == 0) + throw new Z3Exception("Cannot create a pattern from zero terms"); + + return Native.Z3_mk_pattern(nCtx, (uint)terms.Length, terms); + } + #endregion + + #region Solver + + /// + /// Creates a new (incremental) solver. + /// + public NativeSolver MkSimpleSolver() + { + Z3_solver nSolver = Native.Z3_mk_simple_solver(nCtx); + return new NativeSolver(this, nSolver); + } + + #endregion + + #region Utilities + /// + /// Get the sort kind from IntPtr + /// + public Z3_sort_kind GetSortKind(Z3_sort sort) + { + Debug.Assert(sort != IntPtr.Zero); + + return (Z3_sort_kind)Native.Z3_get_sort_kind(nCtx, sort); + } + + /// + /// Get the AST kind from IntPtr + /// + public Z3_ast_kind GetAstKind(Z3_ast ast) + { + Debug.Assert(ast != IntPtr.Zero); + + return (Z3_ast_kind)Native.Z3_get_ast_kind(nCtx, ast); + } + + /// + /// Get the Decl kind from IntPtr + /// + public Z3_decl_kind GetDeclKind(Z3_func_decl decl) + { + Debug.Assert(decl != IntPtr.Zero); + + return (Z3_decl_kind)Native.Z3_get_decl_kind(nCtx, decl); + } + + /// + /// Get Sort for AST + /// + public Z3_sort GetSort(Z3_ast ast) + { + Debug.Assert(ast != IntPtr.Zero); + + return Native.Z3_get_sort(nCtx, ast); + } + + /// + /// Get the arguments for app + /// + /// + /// + public Z3_ast[] GetAppArgs(Z3_app app) + { + Debug.Assert(app != IntPtr.Zero); + + var numArgs = Native.Z3_get_app_num_args(nCtx, app); + var args = new Z3_ast[numArgs]; + for (uint i = 0; i < numArgs; i++) + { + args[i] = Native.Z3_get_app_arg(nCtx, app, i); + } + return args; + } + + /// + /// Get App Decl from IntPtr + /// + public Z3_func_decl GetAppDecl(Z3_ast ast) + { + Debug.Assert(ast != IntPtr.Zero); + + return Native.Z3_get_app_decl(nCtx, ast); + } + + /// + /// Get string name for Decl + /// + /// + /// + public string GetDeclName(Z3_func_decl decl) + { + Debug.Assert(decl != IntPtr.Zero); + + var namePtr = Native.Z3_get_decl_name(nCtx, decl); + return Marshal.PtrToStringAnsi(namePtr); + } + + /// + /// Get size of BitVector Sort + /// + public uint GetBvSortSize(Z3_sort bvSort) + { + Debug.Assert(bvSort != IntPtr.Zero); + + return Native.Z3_get_bv_sort_size(nCtx, bvSort); + } + + /// + /// Get the domain IntPtr for Sort + /// + public Z3_sort GetArraySortDomain(Z3_ast array) + { + Debug.Assert(array != IntPtr.Zero); + + return Native.Z3_get_array_sort_domain(nCtx, array); + } + + /// + /// Get the range IntPtr for Sort + /// + public Z3_sort GetArraySortRange(Z3_ast array) + { + Debug.Assert(array != IntPtr.Zero); + + return Native.Z3_get_array_sort_range(nCtx, array); + } + + /// + /// Try to get integer from AST + /// + /// + /// + /// + public bool TryGetNumeralInt(Z3_ast v, out int i) + { + Debug.Assert(v != IntPtr.Zero); + + int result = i = 0; + if (Native.Z3_get_numeral_int(nCtx, v, ref result) == 0) ; + { + return false; + } + i = result; + return true; + } + + /// + /// Try to get uint from AST + /// + /// + /// + /// + public bool TryGetNumeralUInt(Z3_ast v, out uint u) + { + Debug.Assert(v != IntPtr.Zero); + + uint result = u = 0; + if (Native.Z3_get_numeral_uint(nCtx, v, ref result) == 0) + { + return false; + } + u = result; + return true; + } + + /// + /// Try to get long from AST + /// + /// + /// + /// + /// + public bool TryGetNumeralInt64(Z3_ast v, out long i) + { + Debug.Assert(v != IntPtr.Zero); + + long result = i = 0; + if (Native.Z3_get_numeral_int64(nCtx, v, ref result) == 0) + { + return false; + } + i = result; + return true; + } + + /// + /// Try get ulong from AST + /// + /// + /// + /// + public bool TryGetNumeralUInt64(Z3_ast v, out ulong u) + { + Debug.Assert(v != IntPtr.Zero); + + ulong result = u = 0; + if (Native.Z3_get_numeral_uint64(nCtx, v, ref result) == 0) + { + return false; + } + u = result; + return true; + } + + /// + /// Get string for numeral ast + /// + /// + /// + public string GetNumeralString(Z3_ast v) + { + Debug.Assert(v != IntPtr.Zero); + return Native.Z3_get_numeral_string(nCtx, v); + } + + /// + /// Get printable string representing Z3_ast + /// + /// + /// + public string ToString(Z3_ast ast) + { + Debug.Assert(ast != IntPtr.Zero); + + return Native.Z3_ast_to_string(nCtx, ast); + } + + /// + /// Enable or disable warning messages + /// + /// + public void ToggleWarningMessages(bool turnOn) + => Native.Z3_toggle_warning_messages(turnOn ? (byte)1 : (byte)0); + + #endregion #region Internal + internal static Object creation_lock = new Object(); internal IntPtr m_ctx = IntPtr.Zero; internal Native.Z3_error_handler m_n_err_handler = null; internal IntPtr nCtx { get { return m_ctx; } } @@ -174,11 +1256,44 @@ namespace Microsoft.Z3 PrintMode = Z3_ast_print_mode.Z3_PRINT_SMTLIB2_COMPLIANT; m_n_err_handler = new Native.Z3_error_handler(NativeErrorHandler); // keep reference so it doesn't get collected. Native.Z3_set_error_handler(m_ctx, m_n_err_handler); + GC.SuppressFinalize(this); } #endregion + #region Tracing + /// + /// Enable tracint to file + /// + /// + public void TraceToFile(string file) + { + Debug.Assert(!string.IsNullOrEmpty(file)); + Native.Z3_enable_trace(file); + } + + #endregion + + #region Dispose + + /// + /// Disposes of the context. + /// + public void Dispose() + { + if (m_ctx != IntPtr.Zero) + { + m_n_err_handler = null; + IntPtr ctx = m_ctx; + m_ctx = IntPtr.Zero; + Native.Z3_del_context(ctx); + } + else + GC.ReRegisterForFinalize(this); + } + #endregion + /// /// Utility to convert a vector object of ast to a .Net array @@ -194,7 +1309,6 @@ namespace Microsoft.Z3 result[i] = Native.Z3_ast_vector_get(nCtx, vec, i); Native.Z3_ast_vector_dec_ref(nCtx, vec); return result; - } /// @@ -205,7 +1319,7 @@ namespace Microsoft.Z3 public Statistics.Entry[] GetStatistics(Z3_stats stats) { Native.Z3_stats_inc_ref(nCtx, stats); - var result = Statistics.NativeEntries(nCtx, stats); + var result = Statistics.NativeEntries(nCtx, stats); Native.Z3_stats_dec_ref(nCtx, stats); return result; } diff --git a/src/api/dotnet/NativeModel.cs b/src/api/dotnet/NativeModel.cs index 417426b3b..dc2be0cc8 100644 --- a/src/api/dotnet/NativeModel.cs +++ b/src/api/dotnet/NativeModel.cs @@ -19,20 +19,11 @@ Notes: --*/ -using System; -using System.Diagnostics; -using System.Collections.Generic; - namespace Microsoft.Z3 { - using Z3_context = System.IntPtr; using Z3_ast = System.IntPtr; - using Z3_app = System.IntPtr; - using Z3_sort = System.IntPtr; using Z3_func_decl = System.IntPtr; - using Z3_model = System.IntPtr; - using Z3_func_interp = System.IntPtr; - using Z3_func_entry = System.IntPtr; + using Z3_sort = System.IntPtr; /// /// A Model contains interpretations (assignments) of constants and functions. @@ -67,7 +58,6 @@ namespace Microsoft.Z3 /// A FunctionInterpretation if the function has an interpretation in the model, null otherwise. public NativeFuncInterp FuncInterp(Z3_func_decl f) { - Z3_sort_kind sk = (Z3_sort_kind)Native.Z3_get_sort_kind(Context.nCtx, Native.Z3_get_range(Context.nCtx, f)); if (Native.Z3_get_arity(Context.nCtx, f) == 0) @@ -235,7 +225,6 @@ namespace Microsoft.Z3 /// public Z3_ast Evaluate(Z3_ast t, bool completion = false) => Eval(t, completion); - /// /// Evaluate expression to a double, assuming it is a numeral already. /// @@ -253,12 +242,16 @@ namespace Microsoft.Z3 /// /// One dimensional array of indices where the array is updated /// - public KeyValuePair[] Updates; + public KeyValuePair[] Updates; /// /// default Else case /// public Z3_ast Else; + + public Z3_sort[] Domain; + + public Z3_sort[] Range; } /// @@ -266,26 +259,34 @@ namespace Microsoft.Z3 /// /// /// null if the argument does evaluate to a sequence of stores to an array - public ArrayValue TryGetArrayValue(Z3_ast t) + public bool TryGetArrayValue(Z3_ast t, out ArrayValue result) { var r = Eval(t, true); // check that r is a sequence of store over a constant default array. var updates = new List>(); - var result = new ArrayValue(); - while (true) - { - // check that r is an app, and the decl-kind is Z3_OP_ARRAY_CONST or Z3_OP_ARRAY_STORE - // if it is Z3_OP_ARRAY_CONST then set result.Else and break; - // if it is ARRAY_STORE, then append to 'updates' and continue - // in other cases return null - return null; + //while (true) + //{ + // // check that r is an app, and the decl-kind is Z3_OP_ARRAY_CONST or Z3_OP_ARRAY_STORE + // // if it is Z3_OP_ARRAY_CONST then set result.Else and break; + // // if it is ARRAY_STORE, then append to 'updates' and continue + // // in other cases return null + // return false; + + //} + + if (updates.Any()) + { + result = new ArrayValue() + { + Updates = updates.ToArray() + }; + + return true; } -#if false - result.Updates = updates.ToArray(); - - return null; -#endif + + result = null; + return false; } /// diff --git a/src/api/dotnet/NativeSolver.cs b/src/api/dotnet/NativeSolver.cs index 01e761e18..20d6a8e6f 100644 --- a/src/api/dotnet/NativeSolver.cs +++ b/src/api/dotnet/NativeSolver.cs @@ -18,24 +18,16 @@ Notes: --*/ -using System; -using System.Diagnostics; -using System.Linq; -using System.Collections.Generic; - namespace Microsoft.Z3 { - using Z3_context = System.IntPtr; using Z3_ast = System.IntPtr; - using Z3_app = System.IntPtr; - using Z3_sort = System.IntPtr; + using Z3_context = System.IntPtr; using Z3_func_decl = System.IntPtr; - using Z3_model = System.IntPtr; - using Z3_ast_vector = System.IntPtr; - using Z3_solver = System.IntPtr; - using Z3_symbol = System.IntPtr; using Z3_params = System.IntPtr; + using Z3_solver = System.IntPtr; + using Z3_sort = System.IntPtr; + using Z3_symbol = System.IntPtr; /// /// Solvers. @@ -45,21 +37,15 @@ namespace Microsoft.Z3 /// /// A string that describes all available solver parameters. /// - public string Help - { - get - { - return Native.Z3_solver_get_help(Context.nCtx, NativeObject); - } - } + public string Help => Native.Z3_solver_get_help(nCtx, z3solver); private void SetParam(Action setter) { - Z3_params p = Native.Z3_mk_params(Context.nCtx); - Native.Z3_params_inc_ref(Context.nCtx, p); + Z3_params p = Native.Z3_mk_params(nCtx); + Native.Z3_params_inc_ref(nCtx, p); setter(p); - Native.Z3_solver_set_params(Context.nCtx, NativeObject, p); - Native.Z3_params_dec_ref(Context.nCtx, p); + Native.Z3_solver_set_params(nCtx, z3solver, p); + Native.Z3_params_dec_ref(nCtx, p); } /// @@ -67,7 +53,7 @@ namespace Microsoft.Z3 /// public void Set(string name, bool value) { - SetParam((Z3_params p) => Native.Z3_params_set_bool(Context.nCtx, p, Native.Z3_mk_string_symbol(Context.nCtx, name), (byte)(value ? 1 : 0))); + SetParam((Z3_params p) => Native.Z3_params_set_bool(nCtx, p, Native.Z3_mk_string_symbol(nCtx, name), (byte)(value ? 1 : 0))); } /// @@ -75,7 +61,7 @@ namespace Microsoft.Z3 /// public void Set(string name, uint value) { - SetParam((Z3_params p) => Native.Z3_params_set_uint(Context.nCtx, p, Native.Z3_mk_string_symbol(Context.nCtx, name), value)); + SetParam((Z3_params p) => Native.Z3_params_set_uint(nCtx, p, Native.Z3_mk_string_symbol(nCtx, name), value)); } /// @@ -83,7 +69,7 @@ namespace Microsoft.Z3 /// public void Set(string name, double value) { - SetParam((Z3_params p) => Native.Z3_params_set_double(Context.nCtx, p, Native.Z3_mk_string_symbol(Context.nCtx, name), value)); + SetParam((Z3_params p) => Native.Z3_params_set_double(nCtx, p, Native.Z3_mk_string_symbol(nCtx, name), value)); } /// @@ -91,43 +77,43 @@ namespace Microsoft.Z3 /// public void Set(string name, string value) { - var value_sym = Native.Z3_mk_string_symbol(Context.nCtx, value); - SetParam((Z3_params p) => Native.Z3_params_set_symbol(Context.nCtx, p, Native.Z3_mk_string_symbol(Context.nCtx, name), value_sym)); + var value_sym = Native.Z3_mk_string_symbol(nCtx, value); + SetParam((Z3_params p) => Native.Z3_params_set_symbol(nCtx, p, Native.Z3_mk_string_symbol(nCtx, name), value_sym)); } + #if false - /// - /// Sets parameter on the solver - /// - public void Set(string name, Symbol value) { Parameters = Context.MkParams().Add(name, value); } - /// - /// Sets parameter on the solver - /// - public void Set(Symbol name, bool value) { Parameters = Context.MkParams().Add(name, value); } - /// - /// Sets parameter on the solver - /// - public void Set(Symbol name, uint value) { Parameters = Context.MkParams().Add(name, value); } - /// - /// Sets parameter on the solver - /// - public void Set(Symbol name, double value) { Parameters = Context.MkParams().Add(name, value); } - /// - /// Sets parameter on the solver - /// - public void Set(Symbol name, string value) { Parameters = Context.MkParams().Add(name, value); } - /// - /// Sets parameter on the solver - /// - public void Set(Symbol name, Symbol value) { Parameters = Context.MkParams().Add(name, value); } + /// + /// Sets parameter on the solver + /// + public void Set(string name, Symbol value) { Parameters = Context.MkParams().Add(name, value); } + /// + /// Sets parameter on the solver + /// + public void Set(Symbol name, bool value) { Parameters = Context.MkParams().Add(name, value); } + /// + /// Sets parameter on the solver + /// + public void Set(Symbol name, uint value) { Parameters = Context.MkParams().Add(name, value); } + /// + /// Sets parameter on the solver + /// + public void Set(Symbol name, double value) { Parameters = Context.MkParams().Add(name, value); } + /// + /// Sets parameter on the solver + /// + public void Set(Symbol name, string value) { Parameters = Context.MkParams().Add(name, value); } + /// + /// Sets parameter on the solver + /// + public void Set(Symbol name, Symbol value) { Parameters = Context.MkParams().Add(name, value); } /// /// Retrieves parameter descriptions for solver. /// public ParamDescrs ParameterDescriptions { - get { return new ParamDescrs(Context, Native.Z3_solver_get_param_descrs(Context.nCtx, NativeObject)); } + get { return new ParamDescrs(Context, Native.Z3_solver_get_param_descrs(nCtx, NativeObject)); } } - #endif /// @@ -135,38 +121,26 @@ namespace Microsoft.Z3 /// /// /// - public uint NumScopes - { - get { return Native.Z3_solver_get_num_scopes(Context.nCtx, NativeObject); } - } + public uint NumScopes => Native.Z3_solver_get_num_scopes(nCtx, z3solver); /// /// Creates a backtracking point. /// /// - public void Push() - { - Native.Z3_solver_push(Context.nCtx, NativeObject); - } + public void Push() => Native.Z3_solver_push(nCtx, z3solver); /// /// Backtracks backtracking points. /// /// Note that an exception is thrown if is not smaller than NumScopes /// - public void Pop(uint n = 1) - { - Native.Z3_solver_pop(Context.nCtx, NativeObject, n); - } + public void Pop(uint n = 1) => Native.Z3_solver_pop(nCtx, z3solver, n); /// /// Resets the Solver. /// /// This removes all assertions from the solver. - public void Reset() - { - Native.Z3_solver_reset(Context.nCtx, NativeObject); - } + public void Reset() => Native.Z3_solver_reset(nCtx, z3solver); /// /// Assert a constraint (or multiple) into the solver. @@ -178,25 +152,19 @@ namespace Microsoft.Z3 foreach (Z3_ast a in constraints) { - Native.Z3_solver_assert(Context.nCtx, NativeObject, a); + Native.Z3_solver_assert(nCtx, z3solver, a); } } /// /// Alias for Assert. /// - public void Add(params Z3_ast[] constraints) - { - Assert(constraints); - } + public void Add(params Z3_ast[] constraints) => Assert(constraints); /// /// Alias for Assert. /// - public void Add(IEnumerable constraints) - { - Assert(constraints.ToArray()); - } + public void Add(IEnumerable constraints) => Assert(constraints.ToArray()); /// /// Add constraints to ensure the function f can only be injective. @@ -209,28 +177,26 @@ namespace Microsoft.Z3 /// public void AssertInjective(Z3_func_decl f) { - uint arity = Native.Z3_get_arity(Context.nCtx, f); - Z3_sort range = Native.Z3_get_range(Context.nCtx, f); + uint arity = Native.Z3_get_arity(nCtx, f); + Z3_sort range = Native.Z3_get_range(nCtx, f); Z3_ast[] vars = new Z3_ast[arity]; Z3_sort[] sorts = new Z3_sort[arity]; Z3_symbol[] names = new Z3_symbol[arity]; for (uint i = 0; i < arity; ++i) { - Z3_sort domain = Native.Z3_get_domain(Context.nCtx, f, i); - //vars[i] = Context.MkBound(arity - i - 1, domain); + Z3_sort domain = Native.Z3_get_domain(nCtx, f, i); + vars[i] = ntvContext.MkBound(arity - i - 1, domain); sorts[i] = domain; - names[i] = Native.Z3_mk_int_symbol(Context.nCtx, (int)i); + names[i] = Native.Z3_mk_int_symbol(nCtx, (int)i); } Z3_ast app_f = IntPtr.Zero; // Context.MkApp(f, vars); for (uint i = 0; i < arity; ++i) { - Z3_sort domain = Native.Z3_get_domain(Context.nCtx, f, i); -#if false - Z3_func_decl proj = Native.Z3_mk_fresh_func_decl("inv", new Z3_sort[] { range }, domain); - Z3_ast body = Context.MkEq(vars[i], Context.MkApp(proj, app_f)); - Z3_ast q = Context.MkForall(names, sorts, body); + Z3_sort domain = Native.Z3_get_domain(nCtx, f, i); + Z3_func_decl proj = ntvContext.MkFreshFuncDecl("inv", new Z3_sort[] { range }, domain); + Z3_ast body = ntvContext.MkEq(vars[i], ntvContext.MkApp(proj, app_f)); + Z3_ast q = ntvContext.MkForall(names, sorts, body); Assert(q); -#endif } } @@ -254,7 +220,7 @@ namespace Microsoft.Z3 throw new Z3Exception("Argument size mismatch"); for (int i = 0; i < constraints.Length; i++) - Native.Z3_solver_assert_and_track(Context.nCtx, NativeObject, constraints[i], ps[i]); + Native.Z3_solver_assert_and_track(nCtx, z3solver, constraints[i], ps[i]); } /// @@ -273,57 +239,38 @@ namespace Microsoft.Z3 Debug.Assert(constraint != null); Debug.Assert(p != null); - Native.Z3_solver_assert_and_track(Context.nCtx, NativeObject, constraint, p); + Native.Z3_solver_assert_and_track(nCtx, z3solver, constraint, p); } /// /// Load solver assertions from a file. /// public void FromFile(string file) - { - Native.Z3_solver_from_file(Context.nCtx, NativeObject, file); - } + => Native.Z3_solver_from_file(nCtx, z3solver, file); /// /// Load solver assertions from a string. /// public void FromString(string str) - { - Native.Z3_solver_from_string(Context.nCtx, NativeObject, str); - } + => Native.Z3_solver_from_string(nCtx, z3solver, str); /// /// The number of assertions in the solver. /// public uint NumAssertions - { - get - { - return (uint)Context.ToArray(Native.Z3_solver_get_assertions(Context.nCtx, NativeObject)).Length; - } - } + => (uint)ntvContext.ToArray(Native.Z3_solver_get_assertions(nCtx, z3solver)).Length; /// /// The set of asserted formulas. /// public Z3_ast[] Assertions - { - get - { - return Context.ToArray(Native.Z3_solver_get_assertions(Context.nCtx, NativeObject)); - } - } + => ntvContext.ToArray(Native.Z3_solver_get_assertions(nCtx, z3solver)); /// /// Currently inferred units. /// public Z3_ast[] Units - { - get - { - return Context.ToArray(Native.Z3_solver_get_units(Context.nCtx, NativeObject)); - } - } + => ntvContext.ToArray(Native.Z3_solver_get_units(nCtx, z3solver)); /// /// Checks whether the assertions in the solver are consistent or not. @@ -337,9 +284,9 @@ namespace Microsoft.Z3 { Z3_lbool r; if (assumptions == null || assumptions.Length == 0) - r = (Z3_lbool)Native.Z3_solver_check(Context.nCtx, NativeObject); + r = (Z3_lbool)Native.Z3_solver_check(nCtx, z3solver); else - r = (Z3_lbool)Native.Z3_solver_check_assumptions(Context.nCtx, NativeObject, (uint)assumptions.Length, assumptions); + r = (Z3_lbool)Native.Z3_solver_check_assumptions(nCtx, z3solver, (uint)assumptions.Length, assumptions); return lboolToStatus(r); } @@ -356,13 +303,12 @@ namespace Microsoft.Z3 Z3_lbool r; Z3_ast[] asms = assumptions.ToArray(); if (asms.Length == 0) - r = (Z3_lbool)Native.Z3_solver_check(Context.nCtx, NativeObject); + r = (Z3_lbool)Native.Z3_solver_check(nCtx, z3solver); else - r = (Z3_lbool)Native.Z3_solver_check_assumptions(Context.nCtx, NativeObject, (uint)asms.Length, asms); + r = (Z3_lbool)Native.Z3_solver_check_assumptions(nCtx, z3solver, (uint)asms.Length, asms); return lboolToStatus(r); } - /// /// The model of the last Check(params Expr[] assumptions). /// @@ -374,11 +320,10 @@ namespace Microsoft.Z3 { get { - IntPtr x = Native.Z3_solver_get_model(Context.nCtx, NativeObject); - if (x == IntPtr.Zero) - return null; - else - return new NativeModel(Context, x); + IntPtr x = Native.Z3_solver_get_model(nCtx, z3solver); + return x == IntPtr.Zero + ? null + : new NativeModel(ntvContext, x); } } @@ -390,12 +335,7 @@ namespace Microsoft.Z3 /// if its results was not UNSATISFIABLE, or if proof production is disabled. /// public Z3_ast Proof - { - get - { - return Native.Z3_solver_get_proof(Context.nCtx, NativeObject); - } - } + => Native.Z3_solver_get_proof(nCtx, z3solver); /// /// The unsat core of the last Check. @@ -406,23 +346,13 @@ namespace Microsoft.Z3 /// if its results was not UNSATISFIABLE, or if core production is disabled. /// public Z3_ast[] UnsatCore - { - get - { - return Context.ToArray(Native.Z3_solver_get_unsat_core(Context.nCtx, NativeObject)); - } - } + => ntvContext.ToArray(Native.Z3_solver_get_unsat_core(nCtx, z3solver)); /// /// A brief justification of why the last call to Check returned UNKNOWN. /// public string ReasonUnknown - { - get - { - return Native.Z3_solver_get_reason_unknown(Context.nCtx, NativeObject); - } - } + => Native.Z3_solver_get_reason_unknown(nCtx, z3solver); /// /// Create a clone of the current solver with respect to ctx. @@ -430,7 +360,7 @@ namespace Microsoft.Z3 public NativeSolver Translate(NativeContext ctx) { Debug.Assert(ctx != null); - return new NativeSolver(ctx, Native.Z3_solver_translate(Context.nCtx, NativeObject, ctx.nCtx)); + return new NativeSolver(ctx, Native.Z3_solver_translate(nCtx, z3solver, ctx.nCtx)); } /// @@ -438,9 +368,10 @@ namespace Microsoft.Z3 /// public void ImportModelConverter(NativeSolver src) { - Native.Z3_solver_import_model_converter(Context.nCtx, src.NativeObject, NativeObject); - } + Debug.Assert(src != null); + Native.Z3_solver_import_model_converter(nCtx, src.z3solver, z3solver); + } /// /// Solver statistics. @@ -449,8 +380,8 @@ namespace Microsoft.Z3 { get { - var stats = Native.Z3_solver_get_statistics(Context.nCtx, NativeObject); - return Context.GetStatistics(stats); + var stats = Native.Z3_solver_get_statistics(nCtx, z3solver); + return ntvContext.GetStatistics(stats); } } @@ -459,19 +390,23 @@ namespace Microsoft.Z3 /// public override string ToString() { - return Native.Z3_solver_to_string(Context.nCtx, NativeObject); + return Native.Z3_solver_to_string(nCtx, z3solver); } #region Internal - NativeContext Context; - IntPtr NativeObject; - internal NativeSolver(NativeContext ctx, Z3_solver obj) - { - Context = ctx; - NativeObject = obj; + readonly NativeContext ntvContext; + Z3_solver z3solver; + Z3_context nCtx => ntvContext.nCtx; - Debug.Assert(ctx != null); - Native.Z3_solver_inc_ref(ctx.nCtx, obj); + internal NativeSolver(NativeContext nativeCtx, Z3_solver z3solver) + { + Debug.Assert(nCtx != IntPtr.Zero); + Debug.Assert(z3solver != IntPtr.Zero); + + this.ntvContext = nativeCtx; + this.z3solver = z3solver; + + Native.Z3_solver_inc_ref(nCtx, z3solver); } /// @@ -487,10 +422,10 @@ namespace Microsoft.Z3 /// public void Dispose() { - if (NativeObject != IntPtr.Zero) + if (z3solver != IntPtr.Zero) { - Native.Z3_solver_dec_ref(Context.nCtx, NativeObject); - NativeObject = IntPtr.Zero; + Native.Z3_solver_dec_ref(nCtx, z3solver); + z3solver = IntPtr.Zero; } GC.SuppressFinalize(this); }