From 80506dfdfa80b4845f572c9773d7a7f6e3a95ef4 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 2 Mar 2022 10:55:39 -0800 Subject: [PATCH] sketch ArrayValue, add statistics Signed-off-by: Nikolaj Bjorner --- src/api/dotnet/NativeContext.cs | 8 +++ src/api/dotnet/NativeModel.cs | 39 +++++++++++++ src/api/dotnet/NativeSolver.cs | 99 ++++----------------------------- src/api/dotnet/Statistics.cs | 39 +++++++------ 4 files changed, 81 insertions(+), 104 deletions(-) diff --git a/src/api/dotnet/NativeContext.cs b/src/api/dotnet/NativeContext.cs index a13e48bf7..1aca7fe55 100644 --- a/src/api/dotnet/NativeContext.cs +++ b/src/api/dotnet/NativeContext.cs @@ -197,5 +197,13 @@ namespace Microsoft.Z3 } + public Statistics.Entry[] GetStatistics(Z3_stats stats) + { + Native.Z3_stats_inc_ref(nCtx, stats); + var result = Statistics.NativeEntries(nCtx, stats); + Native.Z3_stats_dec_ref(nCtx, stats); + return result; + } + } } \ No newline at end of file diff --git a/src/api/dotnet/NativeModel.cs b/src/api/dotnet/NativeModel.cs index fcb536a05..9e5cc44a1 100644 --- a/src/api/dotnet/NativeModel.cs +++ b/src/api/dotnet/NativeModel.cs @@ -39,6 +39,7 @@ namespace Microsoft.Z3 /// public class NativeModel : IDisposable { + /// /// Retrieves the interpretation (the assignment) of in the model. /// @@ -244,6 +245,44 @@ namespace Microsoft.Z3 return Native.Z3_get_numeral_double(Context.nCtx, r); } + /// + /// An array value obtained by untangling a model assignment. + /// + public class ArrayValue + { + /// + /// One dimensional array of indices where the array is updated + /// + public KeyValuePair[] Updates; + + /// + /// default Else case + /// + public Z3_ast Else; + } + + public ArrayValue TryGetArrayValue(Z3_ast t) + { + 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; + + } +#if false + result.Updates = updates.ToArray(); + + return null; +#endif + } + /// /// The number of uninterpreted sorts that the model has an interpretation for. /// diff --git a/src/api/dotnet/NativeSolver.cs b/src/api/dotnet/NativeSolver.cs index 0c494fa33..c500356da 100644 --- a/src/api/dotnet/NativeSolver.cs +++ b/src/api/dotnet/NativeSolver.cs @@ -32,8 +32,6 @@ namespace Microsoft.Z3 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_ast_vector = System.IntPtr; using Z3_solver = System.IntPtr; @@ -54,6 +52,7 @@ namespace Microsoft.Z3 } } +#if false /// /// Sets the solver parameters. /// @@ -67,7 +66,7 @@ namespace Microsoft.Z3 } } -#if false + /// /// Sets parameter on the solver /// @@ -252,11 +251,7 @@ namespace Microsoft.Z3 { get { - var assertions = Native.Z3_solver_get_assertions(Context.nCtx, NativeObject); - Native.Z3_ast_vector_inc_ref(Context.nCtx, assertions); - var sz = Native.Z3_ast_vector_size(Context.nCtx, assertions); - Native.Z3_ast_vector_dec_ref(Context.nCtx, assertions); - return sz; + return (uint)Context.ToArray(Native.Z3_solver_get_assertions(Context.nCtx, NativeObject)).Length; } } @@ -267,8 +262,7 @@ namespace Microsoft.Z3 { get { - var assertions = Native.Z3_solver_get_assertions(Context.nCtx, NativeObject); - return Context.ToArray(assertions); + return Context.ToArray(Native.Z3_solver_get_assertions(Context.nCtx, NativeObject)); } } @@ -279,8 +273,7 @@ namespace Microsoft.Z3 { get { - var units = Native.Z3_solver_get_units(Context.nCtx, NativeObject); - return Context.ToArray(units); + return Context.ToArray(Native.Z3_solver_get_units(Context.nCtx, NativeObject)); } } @@ -321,34 +314,6 @@ namespace Microsoft.Z3 return lboolToStatus(r); } -#if false - /// - /// Retrieve fixed assignments to the set of variables in the form of consequences. - /// Each consequence is an implication of the form - /// - /// relevant-assumptions Implies variable = value - /// - /// where the relevant assumptions is a subset of the assumptions that are passed in - /// and the equality on the right side of the implication indicates how a variable - /// is fixed. - /// - /// - /// - /// - /// - /// - public Status Consequences(IEnumerable assumptions, IEnumerable variables, out Z3_ast[] consequences) - { - ASTVector result = new ASTVector(Context); - ASTVector asms = new ASTVector(Context); - ASTVector vars = new ASTVector(Context); - foreach (var asm in assumptions) asms.Push(asm); - foreach (var v in variables) vars.Push(v); - Z3_lbool r = (Z3_lbool)Native.Z3_solver_get_consequences(Context.nCtx, NativeObject, asms.NativeObject, vars.NativeObject, result.NativeObject); - consequences = result.ToBoolExprArray(); - return lboolToStatus(r); - } -#endif /// /// The model of the last Check(params Expr[] assumptions). @@ -411,46 +376,6 @@ namespace Microsoft.Z3 } } - /// - /// Backtrack level that can be adjusted by conquer process - /// - public uint BacktrackLevel { get; set; } - -#if false - /// - /// Variables available and returned by the cuber. - /// - public Z3_ast[] CubeVariables { get; set; } - - - /// - /// Return a set of cubes. - /// - public IEnumerable Cube() - { - ASTVector cv = new ASTVector(Context); - if (CubeVariables != null) - foreach (var b in CubeVariables) cv.Push(b); - - while (true) - { - var lvl = BacktrackLevel; - BacktrackLevel = uint.MaxValue; - ASTVector r = new ASTVector(Context, Native.Z3_solver_cube(Context.nCtx, NativeObject, cv.NativeObject, lvl)); - var v = r.ToBoolExprArray(); - CubeVariables = cv.ToBoolExprArray(); - if (v.Length == 1 && v[0].IsFalse) - { - break; - } - yield return v; - if (v.Length == 0) - { - break; - } - } - } -#endif /// /// Create a clone of the current solver with respect to ctx. /// @@ -468,19 +393,18 @@ namespace Microsoft.Z3 Native.Z3_solver_import_model_converter(Context.nCtx, src.NativeObject, NativeObject); } -#if false + /// /// Solver statistics. /// - public Statistics Statistics + public Statistics.Entry[] Statistics { get { - - return new Statistics(Context, Native.Z3_solver_get_statistics(Context.nCtx, NativeObject)); + var stats = Native.Z3_solver_get_statistics(Context.nCtx, NativeObject); + return Context.GetStatistics(stats); } } -#endif /// /// A string representation of the solver. @@ -490,7 +414,7 @@ namespace Microsoft.Z3 return Native.Z3_solver_to_string(Context.nCtx, NativeObject); } -#region Internal + #region Internal NativeContext Context; IntPtr NativeObject; internal NativeSolver(NativeContext ctx, Z3_solver obj) @@ -499,7 +423,6 @@ namespace Microsoft.Z3 NativeObject = obj; Debug.Assert(ctx != null); - this.BacktrackLevel = uint.MaxValue; Native.Z3_solver_inc_ref(ctx.nCtx, obj); } @@ -535,6 +458,6 @@ namespace Microsoft.Z3 } } -#endregion + #endregion } } diff --git a/src/api/dotnet/Statistics.cs b/src/api/dotnet/Statistics.cs index 8b664913a..f6d72e0c7 100644 --- a/src/api/dotnet/Statistics.cs +++ b/src/api/dotnet/Statistics.cs @@ -23,6 +23,9 @@ using System.Diagnostics; namespace Microsoft.Z3 { + + using Z3_context = System.IntPtr; + using Z3_stats = System.IntPtr; /// /// Objects of this class track statistical information about solvers. /// @@ -123,25 +126,29 @@ namespace Microsoft.Z3 { get { - - uint n = Size; - Entry[] res = new Entry[n]; - for (uint i = 0; i < n; i++) - { - Entry e; - string k = Native.Z3_stats_get_key(Context.nCtx, NativeObject, i); - if (Native.Z3_stats_is_uint(Context.nCtx, NativeObject, i) != 0) - e = new Entry(k, Native.Z3_stats_get_uint_value(Context.nCtx, NativeObject, i)); - else if (Native.Z3_stats_is_double(Context.nCtx, NativeObject, i) != 0) - e = new Entry(k, Native.Z3_stats_get_double_value(Context.nCtx, NativeObject, i)); - else - throw new Z3Exception("Unknown data entry value"); - res[i] = e; - } - return res; + return NativeEntries(Context.nCtx, NativeObject); } } + internal static Entry[] NativeEntries(Z3_context ctx, Z3_stats stats) + { + uint n = Native.Z3_stats_size(ctx, stats); + Entry[] res = new Entry[n]; + for (uint i = 0; i < n; i++) + { + Entry e; + string k = Native.Z3_stats_get_key(ctx, stats, i); + if (Native.Z3_stats_is_uint(ctx, stats, i) != 0) + e = new Entry(k, Native.Z3_stats_get_uint_value(ctx, stats, i)); + else if (Native.Z3_stats_is_double(ctx, stats, i) != 0) + e = new Entry(k, Native.Z3_stats_get_double_value(ctx, stats, i)); + else + throw new Z3Exception("Unknown data entry value"); + res[i] = e; + } + return res; + } + /// /// The statistical counters. ///