From 35d26bc28210f3177f47293d7f93c22d5a595d21 Mon Sep 17 00:00:00 2001 From: John Fleisher Date: Thu, 3 Mar 2022 16:06:30 -0500 Subject: [PATCH] NativeModel: TryGetArrayValue (#5881) * WiP: Disposable, MkAdd, MkApp, MkBool, MkBoolSort, MkBound, MkBvSort, MkFalse, MkTrue, MkIntSort * WiP: Native z3 mk_ functions * WiP: mk_ functions for NativeContext * WiP: add utility functions for getting values * WiP: Adding more native utility functions * native model pull * WiP: NativeContext additions for array access * WiP: use Z3_symbol in place of managed Symbol * WiP: add solver, model, and array methods * WiP: MkSimpleSolver, MkReal * WiP: GetDomain GetRange * WiP: MkExists * Override for MkFuncDecl * MkConstArray, MkSelect * WiP: code cleanup * migrate Context reference to NativeContext * remove local signing from PR * minor code cleanup * Sorts to properties, fix usings, * make IntSort property * sort using * IntSort, RealSort - properties * WiP: get array value update Co-authored-by: jfleisher --- src/api/dotnet/NativeContext.cs | 27 +++++++---- src/api/dotnet/NativeModel.cs | 81 +++++++++++++++------------------ src/api/dotnet/NativeSolver.cs | 2 +- 3 files changed, 56 insertions(+), 54 deletions(-) diff --git a/src/api/dotnet/NativeContext.cs b/src/api/dotnet/NativeContext.cs index 6961b39dd..96e0487de 100644 --- a/src/api/dotnet/NativeContext.cs +++ b/src/api/dotnet/NativeContext.cs @@ -235,7 +235,7 @@ namespace Microsoft.Z3 public Z3_ast MkReal(string v) { Debug.Assert(!string.IsNullOrEmpty(v)); - return Native.Z3_mk_numeral(nCtx, v, MkRealSort()); + return Native.Z3_mk_numeral(nCtx, v, RealSort); } /// @@ -304,10 +304,14 @@ namespace Microsoft.Z3 #region Sort - public Z3_sort MkIntSort() => Native.Z3_mk_int_sort(nCtx); - public Z3_sort MkBoolSort() => Native.Z3_mk_bool_sort(nCtx); + /// + /// Sorts return same ptr for subsequent calls + /// + public Z3_sort IntSort => Native.Z3_mk_int_sort(nCtx); + public Z3_sort BoolSort => Native.Z3_mk_bool_sort(nCtx); + public Z3_sort RealSort => Native.Z3_mk_real_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, @@ -1086,17 +1090,24 @@ namespace Microsoft.Z3 /// public Z3_ast[] GetAppArgs(Z3_app app) { - Debug.Assert(app != IntPtr.Zero); - - var numArgs = Native.Z3_get_app_num_args(nCtx, app); + var numArgs = GetNumArgs(app); var args = new Z3_ast[numArgs]; for (uint i = 0; i < numArgs; i++) { - args[i] = Native.Z3_get_app_arg(nCtx, app, i); + args[i] = GetAppArg(app, i); } return args; } + public uint GetNumArgs(Z3_app app) + { + Debug.Assert(app != IntPtr.Zero); + + return Native.Z3_get_app_num_args(nCtx, app); + } + + internal Z3_ast GetAppArg(Z3_app app, uint i) => Native.Z3_get_app_arg(nCtx, app, i); + /// /// Get App Decl from IntPtr /// diff --git a/src/api/dotnet/NativeModel.cs b/src/api/dotnet/NativeModel.cs index ffd4e0faf..96eb13cd2 100644 --- a/src/api/dotnet/NativeModel.cs +++ b/src/api/dotnet/NativeModel.cs @@ -41,7 +41,7 @@ namespace Microsoft.Z3 /// /// A Constant /// An expression if the constant has an interpretation in the model, null otherwise. - public Z3_ast ConstInterp(Z3_ast a) => ConstFuncInterp(Native.Z3_get_app_decl(Context.nCtx, a)); + public Z3_ast ConstInterp(Z3_ast a) => ConstFuncInterp(Native.Z3_get_app_decl(ntvContext.nCtx, a)); /// /// Retrieves the interpretation (the assignment) of in the model. @@ -50,10 +50,10 @@ namespace Microsoft.Z3 /// An expression if the function has an interpretation in the model, null otherwise. public Z3_ast ConstFuncInterp(Z3_func_decl f) { - if (Native.Z3_get_arity(Context.nCtx, f) != 0) + if (Native.Z3_get_arity(ntvContext.nCtx, f) != 0) throw new Z3Exception("Non-zero arity functions have FunctionInterpretations as a model. Use FuncInterp."); - return Native.Z3_model_get_const_interp(Context.nCtx, NativeObject, f); + return Native.Z3_model_get_const_interp(ntvContext.nCtx, NativeObject, f); } /// @@ -63,11 +63,11 @@ 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)); + Z3_sort_kind sk = (Z3_sort_kind)Native.Z3_get_sort_kind(ntvContext.nCtx, Native.Z3_get_range(ntvContext.nCtx, f)); - if (Native.Z3_get_arity(Context.nCtx, f) == 0) + if (Native.Z3_get_arity(ntvContext.nCtx, f) == 0) { - IntPtr n = Native.Z3_model_get_const_interp(Context.nCtx, NativeObject, f); + IntPtr n = Native.Z3_model_get_const_interp(ntvContext.nCtx, NativeObject, f); if (sk == Z3_sort_kind.Z3_ARRAY_SORT) { @@ -75,10 +75,10 @@ namespace Microsoft.Z3 return null; else { - if (Native.Z3_is_as_array(Context.nCtx, n) == 0) + if (Native.Z3_is_as_array(ntvContext.nCtx, n) == 0) throw new Z3Exception("Argument was not an array constant"); - var fd = Native.Z3_get_as_array_func_decl(Context.nCtx, n); - return new NativeFuncInterp(Context, this, f, fd); + var fd = Native.Z3_get_as_array_func_decl(ntvContext.nCtx, n); + return new NativeFuncInterp(ntvContext, this, f, fd); } } else @@ -88,11 +88,11 @@ namespace Microsoft.Z3 } else { - IntPtr n = Native.Z3_model_get_func_interp(Context.nCtx, NativeObject, f); + IntPtr n = Native.Z3_model_get_func_interp(ntvContext.nCtx, NativeObject, f); if (n == IntPtr.Zero) return null; else - return new NativeFuncInterp(Context, this, f, n); + return new NativeFuncInterp(ntvContext, this, f, n); } } @@ -103,7 +103,7 @@ namespace Microsoft.Z3 /// public uint NumConsts { - get { return Native.Z3_model_get_num_consts(Context.nCtx, NativeObject); } + get { return Native.Z3_model_get_num_consts(ntvContext.nCtx, NativeObject); } } @@ -118,7 +118,7 @@ namespace Microsoft.Z3 uint n = NumConsts; Z3_func_decl[] res = new Z3_func_decl[n]; for (uint i = 0; i < n; i++) - res[i] = Native.Z3_model_get_const_decl(Context.nCtx, NativeObject, i); + res[i] = Native.Z3_model_get_const_decl(ntvContext.nCtx, NativeObject, i); return res; } } @@ -134,24 +134,22 @@ namespace Microsoft.Z3 uint nc = NumConsts; for (uint i = 0; i < nc; ++i) { - var f = Native.Z3_model_get_const_decl(Context.nCtx, NativeObject, i); - IntPtr n = Native.Z3_model_get_const_interp(Context.nCtx, NativeObject, f); + var f = Native.Z3_model_get_const_decl(ntvContext.nCtx, NativeObject, i); + IntPtr n = Native.Z3_model_get_const_interp(ntvContext.nCtx, NativeObject, f); if (n == IntPtr.Zero) continue; yield return new KeyValuePair(f, n); } } } - /// /// The number of function interpretations in the model. /// public uint NumFuncs { - get { return Native.Z3_model_get_num_funcs(Context.nCtx, NativeObject); } + get { return Native.Z3_model_get_num_funcs(ntvContext.nCtx, NativeObject); } } - /// /// The function declarations of the function interpretations in the model. /// @@ -163,12 +161,11 @@ namespace Microsoft.Z3 uint n = NumFuncs; Z3_func_decl[] res = new Z3_func_decl[n]; for (uint i = 0; i < n; i++) - res[i] = Native.Z3_model_get_func_decl(Context.nCtx, NativeObject, i); + res[i] = Native.Z3_model_get_func_decl(ntvContext.nCtx, NativeObject, i); return res; } } - /// /// All symbols that have an interpretation in the model. /// @@ -182,9 +179,9 @@ namespace Microsoft.Z3 uint n = nFuncs + nConsts; Z3_func_decl[] res = new Z3_func_decl[n]; for (uint i = 0; i < nConsts; i++) - res[i] = Native.Z3_model_get_const_decl(Context.nCtx, NativeObject, i); + res[i] = Native.Z3_model_get_const_decl(ntvContext.nCtx, NativeObject, i); for (uint i = 0; i < nFuncs; i++) - res[nConsts + i] = Native.Z3_model_get_func_decl(Context.nCtx, NativeObject, i); + res[nConsts + i] = Native.Z3_model_get_func_decl(ntvContext.nCtx, NativeObject, i); return res; } } @@ -200,7 +197,6 @@ namespace Microsoft.Z3 public ModelEvaluationFailedException() : base() { } } - /// /// Evaluates the expression in the current model. /// @@ -219,7 +215,7 @@ namespace Microsoft.Z3 { IntPtr v = IntPtr.Zero; - if (Native.Z3_model_eval(Context.nCtx, NativeObject, t, (byte)(completion ? 1 : 0), ref v) == (byte)0) + if (Native.Z3_model_eval(ntvContext.nCtx, NativeObject, t, (byte)(completion ? 1 : 0), ref v) == (byte)0) throw new ModelEvaluationFailedException(); else return v; @@ -236,7 +232,7 @@ namespace Microsoft.Z3 public double Double(Z3_ast t) { var r = Eval(t, true); - return Native.Z3_get_numeral_double(Context.nCtx, r); + return Native.Z3_get_numeral_double(ntvContext.nCtx, r); } /// @@ -269,33 +265,28 @@ namespace Microsoft.Z3 { var r = Eval(t, true); // check that r is a sequence of store over a constant default array. - var updates = new List>(); + var updates = new Dictionary(); result = null; while (true) { - if (Context.GetAstKind(r) != Z3_ast_kind.Z3_APP_AST) + if (ntvContext.GetAstKind(r) != Z3_ast_kind.Z3_APP_AST) return false; - Z3_func_decl f = Context.GetAppDecl(r); - var kind = Context.GetDeclKind(f); + Z3_func_decl f = ntvContext.GetAppDecl(r); + var kind = ntvContext.GetDeclKind(f); if (kind == Z3_decl_kind.Z3_OP_CONST_ARRAY) { -#if false -// TODO result = new ArrayValue(); result.Else = r; result.Updates = updates.ToArray(); - result.Domain = updates.Select((x, y) => x).ToArray(); - result.Range = updates.Select((x, y) => y).ToArray(); -#endif + result.Domain = updates.Keys.ToArray(); + result.Range = updates.Values.ToArray(); return true; } else if (kind == Z3_decl_kind.Z3_OP_STORE) { -#if false - Debug.Assert(Context.NumArgs(r) == 3); - updates.Add(new KeyValuePair(Context.GetArg(r, 1), Context.GetArg(r, 2))); - r = Context.GetArg(r, 0); -#endif + Debug.Assert(ntvContext.GetNumArgs(r) == 3); + updates[ntvContext.GetAppArg(r, 1)] = ntvContext.GetAppArg(r, 2); + r = ntvContext.GetAppArg(r, 0); } else { @@ -308,7 +299,7 @@ namespace Microsoft.Z3 /// /// The number of uninterpreted sorts that the model has an interpretation for. /// - public uint NumSorts { get { return Native.Z3_model_get_num_sorts(Context.nCtx, NativeObject); } } + public uint NumSorts { get { return Native.Z3_model_get_num_sorts(ntvContext.nCtx, NativeObject); } } /// @@ -328,7 +319,7 @@ namespace Microsoft.Z3 uint n = NumSorts; Z3_sort[] res = new Z3_sort[n]; for (uint i = 0; i < n; i++) - res[i] = Native.Z3_model_get_sort(Context.nCtx, NativeObject, i); + res[i] = Native.Z3_model_get_sort(ntvContext.nCtx, NativeObject, i); return res; } } @@ -340,16 +331,16 @@ namespace Microsoft.Z3 /// A string representation of the model. public override string ToString() { - return Native.Z3_model_to_string(Context.nCtx, NativeObject); + return Native.Z3_model_to_string(ntvContext.nCtx, NativeObject); } IntPtr NativeObject; - NativeContext Context; + NativeContext ntvContext; internal NativeModel(NativeContext ctx, IntPtr obj) { - Context = ctx; + ntvContext = ctx; NativeObject = obj; Debug.Assert(ctx != null); Native.Z3_model_inc_ref(ctx.nCtx, obj); @@ -371,7 +362,7 @@ namespace Microsoft.Z3 { if (NativeObject != IntPtr.Zero) { - Native.Z3_model_dec_ref(Context.nCtx, NativeObject); + Native.Z3_model_dec_ref(ntvContext.nCtx, NativeObject); NativeObject = IntPtr.Zero; } GC.SuppressFinalize(this); diff --git a/src/api/dotnet/NativeSolver.cs b/src/api/dotnet/NativeSolver.cs index 00110d550..40444804a 100644 --- a/src/api/dotnet/NativeSolver.cs +++ b/src/api/dotnet/NativeSolver.cs @@ -19,9 +19,9 @@ Notes: --*/ using System; +using System.Diagnostics; using System.Collections.Generic; using System.Linq; -using System.Diagnostics; namespace Microsoft.Z3 {