From c812d1e89086ca9c23cad8148f76c2a5985810a9 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 1 Mar 2022 14:07:20 -0800 Subject: [PATCH] update native func interp Signed-off-by: Nikolaj Bjorner --- src/api/dotnet/NativeFuncInterp.cs | 211 ++++++----------------------- src/api/dotnet/NativeModel.cs | 40 +++--- 2 files changed, 64 insertions(+), 187 deletions(-) diff --git a/src/api/dotnet/NativeFuncInterp.cs b/src/api/dotnet/NativeFuncInterp.cs index bac3add04..86bb27c55 100644 --- a/src/api/dotnet/NativeFuncInterp.cs +++ b/src/api/dotnet/NativeFuncInterp.cs @@ -22,202 +22,79 @@ using System; 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; + /// /// A function interpretation is represented as a finite map and an 'else' value. /// Each entry in the finite map represents the value of a function given a set of arguments. /// - public class NativeFuncInterp : IDisposable + public class NativeFuncInterp { -#if false - /// - /// An Entry object represents an element in the finite map used to encode - /// a function interpretation. + /// Evaluation entry of a function /// - public class Entry : Z3Object + public class Entry { /// - /// Return the (symbolic) value of this entry. + /// Argument values that define entry /// - public Expr Value - { - get - { - return Expr.Create(Context, Native.Z3_func_entry_get_value(Context.nCtx, NativeObject)); - } - } + public Z3_ast[] Arguments; /// - /// The number of arguments of the entry. + /// Result of applying function to Arguments in the interpretation /// - public uint NumArgs - { - get { return Native.Z3_func_entry_get_num_args(Context.nCtx, NativeObject); } - } - - /// - /// The arguments of the function entry. - /// - public Expr[] Args - { - get - { - - uint n = NumArgs; - Expr[] res = new Expr[n]; - for (uint i = 0; i < n; i++) - res[i] = Expr.Create(Context, Native.Z3_func_entry_get_arg(Context.nCtx, NativeObject, i)); - return res; - } - } - - /// - /// A string representation of the function entry. - /// - public override string ToString() - { - uint n = NumArgs; - string res = "["; - Expr[] args = Args; - for (uint i = 0; i < n; i++) - res += args[i] + ", "; - return res + Value + "]"; - } - - #region Internal - internal Entry(Context ctx, IntPtr obj) : base(ctx, obj) { Debug.Assert(ctx != null); } - - internal class DecRefQueue : IDecRefQueue - { - public DecRefQueue() : base() { } - public DecRefQueue(uint move_limit) : base(move_limit) { } - internal override void IncRef(Context ctx, IntPtr obj) - { - Native.Z3_func_entry_inc_ref(ctx.nCtx, obj); - } - - internal override void DecRef(Context ctx, IntPtr obj) - { - Native.Z3_func_entry_dec_ref(ctx.nCtx, obj); - } - }; - - internal override void IncRef(IntPtr o) - { - Context.FuncEntry_DRQ.IncAndClear(Context, o); - base.IncRef(o); - } - - internal override void DecRef(IntPtr o) - { - Context.FuncEntry_DRQ.Add(o); - base.DecRef(o); - } - #endregion - }; + public Z3_ast Result; + } /// - /// The number of entries in the function interpretation. + /// Function that is interpreted /// - public uint NumEntries - { - get { return Native.Z3_func_interp_get_num_entries(Context.nCtx, NativeObject); } - } + public Z3_func_decl Declaration; /// - /// The entries in the function interpretation + /// Set of non-default entries defining the function graph /// - public Entry[] Entries - { - get - { - - uint n = NumEntries; - Entry[] res = new Entry[n]; - for (uint i = 0; i < n; i++) - res[i] = new Entry(Context, Native.Z3_func_interp_get_entry(Context.nCtx, NativeObject, i)); - return res; - } - } + public Entry[] Entries; /// - /// The (symbolic) `else' value of the function interpretation. + /// Default cause of the function interpretation /// - public Expr Else + public Z3_ast Else; + + #region Internal + internal NativeFuncInterp(NativeContext ctx, NativeModel mdl, Z3_func_decl decl, Z3_func_interp fi) { - get - { - - return Expr.Create(Context, Native.Z3_func_interp_get_else(Context.nCtx, NativeObject)); - } - } - - /// - /// The arity of the function interpretation - /// - public uint Arity - { - get { return Native.Z3_func_interp_get_arity(Context.nCtx, NativeObject); } - } - - /// - /// A string representation of the function interpretation. - /// - public override string ToString() - { - string res = ""; - res += "["; - foreach (Entry e in Entries) - { - uint n = e.NumArgs; - if (n > 1) res += "["; - Expr[] args = e.Args; - for (uint i = 0; i < n; i++) - { - if (i != 0) res += ", "; - res += args[i]; - } - if (n > 1) res += "]"; - res += " -> " + e.Value + ", "; - } - res += "else -> " + Else; - res += "]"; - return res; - } - -#endif - - #region Internal - NativeContext Context; - IntPtr NativeObject; - internal NativeFuncInterp(NativeContext ctx, IntPtr obj) - { - Context = ctx; - NativeObject = obj; Debug.Assert(ctx != null); - // inc-ref - } + Z3_context nCtx = ctx.nCtx; + Native.Z3_func_interp_inc_ref(nCtx, fi); - /// - /// Finalizer. - /// - ~NativeFuncInterp() - { - Dispose(); - } + Declaration = decl; + Else = Native.Z3_func_interp_get_else(nCtx, fi); + uint numEntries = Native.Z3_func_interp_get_num_entries(nCtx, fi); + uint numArgs = Native.Z3_func_interp_get_arity(nCtx, fi); + Entries = new Entry[numEntries]; - /// - /// Disposes of the underlying native Z3 object. - /// - public void Dispose() - { - if (NativeObject != IntPtr.Zero) + for (uint j = 0; j < numEntries; ++j) { - Native.Z3_func_interp_dec_ref(Context.nCtx, NativeObject); - NativeObject = IntPtr.Zero; + var entry = Native.Z3_func_interp_get_entry(nCtx, fi, j); + Native.Z3_func_entry_inc_ref(nCtx, entry); + Entries[j].Arguments = new Z3_ast[numArgs]; + for (uint i = 0; i < numArgs; ++i) + Entries[j].Arguments[i] = Native.Z3_func_entry_get_arg(nCtx, entry, i); + Entries[j].Result = Native.Z3_func_entry_get_value(nCtx, entry); + Native.Z3_func_entry_dec_ref(nCtx, entry); } - GC.SuppressFinalize(this); + + Native.Z3_func_interp_dec_ref(nCtx, fi); } diff --git a/src/api/dotnet/NativeModel.cs b/src/api/dotnet/NativeModel.cs index 234f3759d..fcb536a05 100644 --- a/src/api/dotnet/NativeModel.cs +++ b/src/api/dotnet/NativeModel.cs @@ -53,7 +53,7 @@ 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(Context.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); @@ -68,8 +68,8 @@ namespace Microsoft.Z3 { 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) + + if (Native.Z3_get_arity(Context.nCtx, f) == 0) { IntPtr n = Native.Z3_model_get_const_interp(Context.nCtx, NativeObject, f); @@ -82,7 +82,7 @@ namespace Microsoft.Z3 if (Native.Z3_is_as_array(Context.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, fd); + return new NativeFuncInterp(Context, this, f, fd); } } else @@ -96,7 +96,7 @@ namespace Microsoft.Z3 if (n == IntPtr.Zero) return null; else - return new NativeFuncInterp(Context, n); + return new NativeFuncInterp(Context, this, f, n); } } @@ -188,7 +188,7 @@ namespace Microsoft.Z3 for (uint i = 0; i < nConsts; i++) res[i] = Native.Z3_model_get_const_decl(Context.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(Context.nCtx, NativeObject, i); return res; } } @@ -238,9 +238,10 @@ namespace Microsoft.Z3 /// /// Evaluate expression to a double, assuming it is a numeral already. /// - public double Double(Z3_ast t) { + 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(Context.nCtx, r); } /// @@ -258,7 +259,6 @@ namespace Microsoft.Z3 /// the "universe" of the sort. /// /// - /// public Z3_sort[] Sorts { get @@ -283,15 +283,15 @@ namespace Microsoft.Z3 } - IntPtr NativeObject; - NativeContext Context; - + IntPtr NativeObject; + NativeContext Context; + internal NativeModel(NativeContext ctx, IntPtr obj) { - Context = ctx; - NativeObject = obj; + Context = ctx; + NativeObject = obj; Debug.Assert(ctx != null); - Native.Z3_model_inc_ref(ctx.nCtx, obj); + Native.Z3_model_inc_ref(ctx.nCtx, obj); } @@ -299,9 +299,9 @@ namespace Microsoft.Z3 /// Finalizer. /// ~NativeModel() - { - Dispose(); - } + { + Dispose(); + } /// /// Disposes of the underlying native Z3 object. @@ -310,8 +310,8 @@ namespace Microsoft.Z3 { if (NativeObject != IntPtr.Zero) { - Native.Z3_model_dec_ref(Context.nCtx, NativeObject); - NativeObject = IntPtr.Zero; + Native.Z3_model_dec_ref(Context.nCtx, NativeObject); + NativeObject = IntPtr.Zero; } GC.SuppressFinalize(this); }