From c0826d58bf1d61783120dd1c73160709ca902e38 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 1 Mar 2022 12:11:02 -0800 Subject: [PATCH] add stubs for native model and func interp Signed-off-by: Nikolaj Bjorner --- src/api/dotnet/CMakeLists.txt | 2 + src/api/dotnet/NativeFuncInterp.cs | 225 ++++++++++++++++++++ src/api/dotnet/NativeModel.cs | 329 +++++++++++++++++++++++++++++ 3 files changed, 556 insertions(+) create mode 100644 src/api/dotnet/NativeFuncInterp.cs create mode 100644 src/api/dotnet/NativeModel.cs diff --git a/src/api/dotnet/CMakeLists.txt b/src/api/dotnet/CMakeLists.txt index 5c722c828..25b3136ad 100644 --- a/src/api/dotnet/CMakeLists.txt +++ b/src/api/dotnet/CMakeLists.txt @@ -86,6 +86,8 @@ set(Z3_DOTNET_ASSEMBLY_SOURCES_IN_SRC_TREE Log.cs Model.cs NativeContext.cs + NativeFuncInterp.cs + NativeModel.cs Optimize.cs ParamDescrs.cs Params.cs diff --git a/src/api/dotnet/NativeFuncInterp.cs b/src/api/dotnet/NativeFuncInterp.cs new file mode 100644 index 000000000..718462af9 --- /dev/null +++ b/src/api/dotnet/NativeFuncInterp.cs @@ -0,0 +1,225 @@ +/*++ +Copyright (c) 2012 Microsoft Corporation + +Module Name: + + NativeFuncInterp.cs + +Abstract: + + Z3 Managed API: Function Interpretations + +Author: + + Christoph Wintersteiger (cwinter) 2012-03-21 + +Notes: + +--*/ + +using System.Diagnostics; +using System; + +namespace Microsoft.Z3 +{ + /// + /// 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 + { + +#if false + /// + /// An Entry object represents an element in the finite map used to encode + /// a function interpretation. + /// + public class Entry : Z3Object + { + /// + /// Return the (symbolic) value of this entry. + /// + public Expr Value + { + get + { + return Expr.Create(Context, Native.Z3_func_entry_get_value(Context.nCtx, NativeObject)); + } + } + + /// + /// The number of arguments of the entry. + /// + 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 + }; + + /// + /// The number of entries in the function interpretation. + /// + public uint NumEntries + { + get { return Native.Z3_func_interp_get_num_entries(Context.nCtx, NativeObject); } + } + + /// + /// The entries in the function interpretation + /// + 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; + } + } + + /// + /// The (symbolic) `else' value of the function interpretation. + /// + public Expr Else + { + 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 + } + + /// + /// Finalizer. + /// + ~NativeFuncInterp() + { + Dispose(); + } + + /// + /// Disposes of the underlying native Z3 object. + /// + public void Dispose() + { + if (NativeObject != IntPtr.Zero) + { + Native.Z3_func_interp_dec_ref(Context.nCtx, NativeObject); + NativeObject = IntPtr.Zero; + } + GC.SuppressFinalize(this); + } + + + #endregion + } +} diff --git a/src/api/dotnet/NativeModel.cs b/src/api/dotnet/NativeModel.cs new file mode 100644 index 000000000..8a31af32f --- /dev/null +++ b/src/api/dotnet/NativeModel.cs @@ -0,0 +1,329 @@ +/*++ +Copyright (c) 2012 Microsoft Corporation + +Module Name: + + NativeModel.cs + +Abstract: + + Z3 Managed API: Models + Native interface to model objects. + +Author: + + Christoph Wintersteiger (cwinter) 2012-03-21 + Nikolaj Bjorner (nbjorner) 2022-03-01 + +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; + + /// + /// A Model contains interpretations (assignments) of constants and functions. + /// + public class NativeModel + { + /// + /// Retrieves the interpretation (the assignment) of in the model. + /// + /// A Constant + /// An expression if the constant has an interpretation in the model, null otherwise. + public Z3_ast ConstInterp(Z3_ast a) => ConstInterp(Native.Z3_get_app_decl(Context.nCtx, a)); + + /// + /// Retrieves the interpretation (the assignment) of in the model. + /// + /// A function declaration of zero arity + /// 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) + 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); + } + + /// + /// Retrieves the interpretation (the assignment) of a non-constant in the model. + /// + /// A function declaration of non-zero arity + /// 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) + { + IntPtr n = Native.Z3_model_get_const_interp(Context.nCtx, NativeObject, f); + + if (sk == Z3_sort_kind.Z3_ARRAY_SORT) + { + if (n == IntPtr.Zero) + return null; + else + { + 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); + } + } + else + { + throw new Z3Exception("Constant functions do not have a function interpretation; use ConstInterp"); + } + } + else + { + IntPtr n = Native.Z3_model_get_func_interp(Context.nCtx, NativeObject, f); + if (n == IntPtr.Zero) + return null; + else + return new NativeFuncInterp(Context, n); + } + } + + + + /// + /// The number of constants that have an interpretation in the model. + /// + public uint NumConsts + { + get { return Native.Z3_model_get_num_consts(Context.nCtx, NativeObject); } + } + + + /// + /// The function declarations of the constants in the model. + /// + public Z3_func_decl[] ConstDecls + { + get + { + + 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); + return res; + } + } + + + /// + /// Enumerate constants in model. + /// + public IEnumerable> Consts + { + get + { + 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); + 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); } + } + +#if false + + /// + /// The function declarations of the function interpretations in the model. + /// + public FuncDecl[] FuncDecls + { + get + { + + uint n = NumFuncs; + FuncDecl[] res = new FuncDecl[n]; + for (uint i = 0; i < n; i++) + res[i] = new FuncDecl(Context, Native.Z3_model_get_func_decl(Context.nCtx, NativeObject, i)); + return res; + } + } + + /// + /// All symbols that have an interpretation in the model. + /// + public FuncDecl[] Decls + { + get + { + + uint nFuncs = NumFuncs; + uint nConsts = NumConsts; + uint n = nFuncs + nConsts; + FuncDecl[] res = new FuncDecl[n]; + for (uint i = 0; i < nConsts; i++) + res[i] = new FuncDecl(Context, Native.Z3_model_get_const_decl(Context.nCtx, NativeObject, i)); + for (uint i = 0; i < nFuncs; i++) + res[nConsts + i] = new FuncDecl(Context, Native.Z3_model_get_func_decl(Context.nCtx, NativeObject, i)); + return res; + } + } + + /// + /// A ModelEvaluationFailedException is thrown when an expression cannot be evaluated by the model. + /// + public class ModelEvaluationFailedException : Z3Exception + { + /// + /// An exception that is thrown when model evaluation fails. + /// + public ModelEvaluationFailedException() : base() { } + } + + /// + /// Evaluates the expression in the current model. + /// + /// + /// This function may fail if contains quantifiers, + /// is partial (MODEL_PARTIAL enabled), or if is not well-sorted. + /// In this case a ModelEvaluationFailedException is thrown. + /// + /// An expression + /// + /// When this flag is enabled, a model value will be assigned to any constant + /// or function that does not have an interpretation in the model. + /// + /// The evaluation of in the model. + public Z3_ast Eval(Z3_ast t, bool completion = false) + { + Debug.Assert(t != null); + + IntPtr v = IntPtr.Zero; + if (Native.Z3_model_eval(Context.nCtx, NativeObject, t.NativeObject, (byte)(completion ? 1 : 0), ref v) == (byte)0) + throw new ModelEvaluationFailedException(); + else + return Z3_ast.Create(Context, v); + } + + /// + /// Alias for Eval. + /// + public Z3_ast Evaluate(Z3_ast t, bool completion = false) + { + Debug.Assert(t != null); + + return Eval(t, completion); + } + + /// + /// Evaluate expression to a double, assuming it is a numeral already. + /// + public double Double(Z3_ast t) { + var r = Eval(t, true); + return Native.Z3_get_numeral_double(Context.nCtx, r); + } + + /// + /// 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); } } + + /// + /// The uninterpreted sorts that the model has an interpretation for. + /// + /// + /// Z3 also provides an interpretation for uninterpreted sorts used in a formula. + /// The interpretation for a sort is a finite set of distinct values. We say this finite set is + /// the "universe" of the sort. + /// + /// + /// + public Sort[] Sorts + { + get + { + + uint n = NumSorts; + Sort[] res = new Sort[n]; + for (uint i = 0; i < n; i++) + res[i] = Sort.Create(Context, Native.Z3_model_get_sort(Context.nCtx, NativeObject, i)); + return res; + } + } + +#endif + + /// + /// Conversion of models to strings. + /// + /// A string representation of the model. + public override string ToString() + { + return Native.Z3_model_to_string(Context.nCtx, NativeObject); + } + + + + IntPtr NativeObject; + NativeContext Context; + + internal NativeModel(NativeContext ctx, IntPtr obj) + { + Context = ctx; + NativeObject = obj; + Debug.Assert(ctx != null); + Native.Z3_model_inc_ref(ctx.nCtx, obj); + } + + + /// + /// Finalizer. + /// + ~NativeModel() + { + Dispose(); + } + + /// + /// Disposes of the underlying native Z3 object. + /// + public void Dispose() + { + if (NativeObject != IntPtr.Zero) + { + Native.Z3_model_dec_ref(Context.nCtx, NativeObject); + NativeObject = IntPtr.Zero; + } + GC.SuppressFinalize(this); + } + + + } +} + + +