diff --git a/src/api/dotnet/CMakeLists.txt b/src/api/dotnet/CMakeLists.txt index 25b3136ad..e2055cd7a 100644 --- a/src/api/dotnet/CMakeLists.txt +++ b/src/api/dotnet/CMakeLists.txt @@ -88,6 +88,7 @@ set(Z3_DOTNET_ASSEMBLY_SOURCES_IN_SRC_TREE NativeContext.cs NativeFuncInterp.cs NativeModel.cs + NativeSolver.cs Optimize.cs ParamDescrs.cs Params.cs diff --git a/src/api/dotnet/NativeContext.cs b/src/api/dotnet/NativeContext.cs index a8676e05b..a13e48bf7 100644 --- a/src/api/dotnet/NativeContext.cs +++ b/src/api/dotnet/NativeContext.cs @@ -179,5 +179,23 @@ namespace Microsoft.Z3 #endregion + + /// + /// Utility to convert a vector object of ast to a .Net array + /// + /// + /// + public Z3_ast[] ToArray(Z3_ast_vector vec) + { + Native.Z3_ast_vector_inc_ref(nCtx, vec); + var sz = Native.Z3_ast_vector_size(nCtx, vec); + var result = new Z3_ast[sz]; + for (uint i = 0; i < sz; ++i) + result[i] = Native.Z3_ast_vector_get(nCtx, vec, i); + Native.Z3_ast_vector_dec_ref(nCtx, vec); + return result; + + } + } } \ No newline at end of file diff --git a/src/api/dotnet/NativeSolver.cs b/src/api/dotnet/NativeSolver.cs new file mode 100644 index 000000000..0c494fa33 --- /dev/null +++ b/src/api/dotnet/NativeSolver.cs @@ -0,0 +1,540 @@ +/*++ +Copyright (c) 2012 Microsoft Corporation + +Module Name: + + NativeSolver.cs + +Abstract: + + Z3 Managed API: Native Solver + +Author: + + Christoph Wintersteiger (cwinter) 2012-03-22 + Nikolaj Bjorner (nbjorner) 2022-03-01 + +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_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; + + /// + /// Solvers. + /// + public class NativeSolver : IDisposable + { + /// + /// A string that describes all available solver parameters. + /// + public string Help + { + get + { + + return Native.Z3_solver_get_help(Context.nCtx, NativeObject); + } + } + + /// + /// Sets the solver parameters. + /// + public Params Parameters + { + set + { + Debug.Assert(value != null); + + Native.Z3_solver_set_params(Context.nCtx, NativeObject, value.NativeObject); + } + } + +#if false + /// + /// Sets parameter on the solver + /// + public void Set(string name, bool value) { Parameters = Context.MkParams().Add(name, value); } + /// + /// Sets parameter on the solver + /// + public void Set(string name, uint value) { Parameters = Context.MkParams().Add(name, value); } + /// + /// Sets parameter on the solver + /// + public void Set(string name, double value) { Parameters = Context.MkParams().Add(name, value); } + /// + /// Sets parameter on the solver + /// + public void Set(string name, string 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)); } + } + +#endif + + /// + /// The current number of backtracking points (scopes). + /// + /// + /// + public uint NumScopes + { + get { return Native.Z3_solver_get_num_scopes(Context.nCtx, NativeObject); } + } + + /// + /// Creates a backtracking point. + /// + /// + public void Push() + { + Native.Z3_solver_push(Context.nCtx, NativeObject); + } + + /// + /// 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); + } + + /// + /// Resets the Solver. + /// + /// This removes all assertions from the solver. + public void Reset() + { + Native.Z3_solver_reset(Context.nCtx, NativeObject); + } + + /// + /// Assert a constraint (or multiple) into the solver. + /// + public void Assert(params Z3_ast[] constraints) + { + Debug.Assert(constraints != null); + Debug.Assert(constraints.All(c => c != IntPtr.Zero)); + + foreach (Z3_ast a in constraints) + { + Native.Z3_solver_assert(Context.nCtx, NativeObject, a); + } + } + + /// + /// Alias for Assert. + /// + public void Add(params Z3_ast[] constraints) + { + Assert(constraints); + } + + /// + /// Alias for Assert. + /// + public void Add(IEnumerable constraints) + { + Assert(constraints.ToArray()); + } + + /// + /// Assert multiple constraints into the solver, and track them (in the unsat) core + /// using the Boolean constants in ps. + /// + /// + /// This API is an alternative to with assumptions for extracting unsat cores. + /// Both APIs can be used in the same solver. The unsat core will contain a combination + /// of the Boolean variables provided using + /// and the Boolean literals + /// provided using with assumptions. + /// + public void AssertAndTrack(Z3_ast[] constraints, Z3_ast[] ps) + { + Debug.Assert(constraints != null); + Debug.Assert(constraints.All(c => c != IntPtr.Zero)); + Debug.Assert(ps.All(c => c != IntPtr.Zero)); + if (constraints.Length != ps.Length) + 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]); + } + + /// + /// Assert a constraint into the solver, and track it (in the unsat) core + /// using the Boolean constant p. + /// + /// + /// This API is an alternative to with assumptions for extracting unsat cores. + /// Both APIs can be used in the same solver. The unsat core will contain a combination + /// of the Boolean variables provided using + /// and the Boolean literals + /// provided using with assumptions. + /// + public void AssertAndTrack(Z3_ast constraint, Z3_ast p) + { + Debug.Assert(constraint != null); + Debug.Assert(p != null); + + Native.Z3_solver_assert_and_track(Context.nCtx, NativeObject, constraint, p); + } + + /// + /// Load solver assertions from a file. + /// + public void FromFile(string file) + { + Native.Z3_solver_from_file(Context.nCtx, NativeObject, file); + } + + /// + /// Load solver assertions from a string. + /// + public void FromString(string str) + { + Native.Z3_solver_from_string(Context.nCtx, NativeObject, str); + } + + /// + /// The number of assertions in the solver. + /// + public uint NumAssertions + { + 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; + } + } + + /// + /// The set of asserted formulas. + /// + public Z3_ast[] Assertions + { + get + { + var assertions = Native.Z3_solver_get_assertions(Context.nCtx, NativeObject); + return Context.ToArray(assertions); + } + } + + /// + /// Currently inferred units. + /// + public Z3_ast[] Units + { + get + { + var units = Native.Z3_solver_get_units(Context.nCtx, NativeObject); + return Context.ToArray(units); + } + } + + /// + /// Checks whether the assertions in the solver are consistent or not. + /// + /// + /// + /// + /// + /// + public Status Check(params Z3_ast[] assumptions) + { + Z3_lbool r; + if (assumptions == null || assumptions.Length == 0) + r = (Z3_lbool)Native.Z3_solver_check(Context.nCtx, NativeObject); + else + r = (Z3_lbool)Native.Z3_solver_check_assumptions(Context.nCtx, NativeObject, (uint)assumptions.Length, assumptions); + return lboolToStatus(r); + } + + /// + /// Checks whether the assertions in the solver are consistent or not. + /// + /// + /// + /// + /// + /// + public Status Check(IEnumerable assumptions) + { + Z3_lbool r; + Z3_ast[] asms = assumptions.ToArray(); + if (asms.Length == 0) + r = (Z3_lbool)Native.Z3_solver_check(Context.nCtx, NativeObject); + else + r = (Z3_lbool)Native.Z3_solver_check_assumptions(Context.nCtx, NativeObject, (uint)asms.Length, asms); + 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). + /// + /// + /// The result is null if Check(params Expr[] assumptions) was not invoked before, + /// if its results was not SATISFIABLE, or if model production is not enabled. + /// + public NativeModel Model + { + get + { + IntPtr x = Native.Z3_solver_get_model(Context.nCtx, NativeObject); + if (x == IntPtr.Zero) + return null; + else + return new NativeModel(Context, x); + } + } + + /// + /// The proof of the last Check(params Expr[] assumptions). + /// + /// + /// The result is null if Check(params Expr[] assumptions) was not invoked before, + /// 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); + } + } + + /// + /// The unsat core of the last Check. + /// + /// + /// The unsat core is a subset of Assertions + /// The result is empty if Check was not invoked before, + /// 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)); + } + } + + /// + /// 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); + } + } + + /// + /// 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. + /// + public NativeSolver Translate(NativeContext ctx) + { + Debug.Assert(ctx != null); + return new NativeSolver(ctx, Native.Z3_solver_translate(Context.nCtx, NativeObject, ctx.nCtx)); + } + + /// + /// Import model converter from other solver. + /// + public void ImportModelConverter(NativeSolver src) + { + Native.Z3_solver_import_model_converter(Context.nCtx, src.NativeObject, NativeObject); + } + +#if false + /// + /// Solver statistics. + /// + public Statistics Statistics + { + get + { + + return new Statistics(Context, Native.Z3_solver_get_statistics(Context.nCtx, NativeObject)); + } + } +#endif + + /// + /// A string representation of the solver. + /// + public override string ToString() + { + return Native.Z3_solver_to_string(Context.nCtx, NativeObject); + } + +#region Internal + NativeContext Context; + IntPtr NativeObject; + internal NativeSolver(NativeContext ctx, Z3_solver obj) + { + Context = ctx; + NativeObject = obj; + + Debug.Assert(ctx != null); + this.BacktrackLevel = uint.MaxValue; + Native.Z3_solver_inc_ref(ctx.nCtx, obj); + } + + /// + /// Finalizer. + /// + ~NativeSolver() + { + Dispose(); + } + + /// + /// Disposes of the underlying native Z3 object. + /// + public void Dispose() + { + if (NativeObject != IntPtr.Zero) + { + Native.Z3_solver_dec_ref(Context.nCtx, NativeObject); + NativeObject = IntPtr.Zero; + } + GC.SuppressFinalize(this); + } + + + private Status lboolToStatus(Z3_lbool r) + { + switch (r) + { + case Z3_lbool.Z3_L_TRUE: return Status.SATISFIABLE; + case Z3_lbool.Z3_L_FALSE: return Status.UNSATISFIABLE; + default: return Status.UNKNOWN; + } + } + +#endregion + } +}