From e3fe80fd4d2e00af1b19ba437a384effa2167ab3 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 3 Dec 2013 20:20:24 -0800 Subject: [PATCH] add .NET interface and finish C interface for optimization Signed-off-by: Nikolaj Bjorner --- src/api/api_opt.cpp | 18 +++- src/api/dotnet/Context.cs | 16 ++++ src/api/dotnet/Optimize.cs | 166 +++++++++++++++++++++++++++++++++++++ src/opt/opt_context.cpp | 81 ++++++++++++------ src/opt/opt_context.h | 12 ++- 5 files changed, 261 insertions(+), 32 deletions(-) create mode 100644 src/api/dotnet/Optimize.cs diff --git a/src/api/api_opt.cpp b/src/api/api_opt.cpp index 497f988cf..afc33e396 100644 --- a/src/api/api_opt.cpp +++ b/src/api/api_opt.cpp @@ -147,14 +147,24 @@ extern "C" { // get lower value or current approximation Z3_ast Z3_API Z3_optimize_get_lower(Z3_context c, Z3_optimize o, unsigned idx) { - NOT_IMPLEMENTED_YET(); - return 0; + Z3_TRY; + LOG_Z3_optimize_get_lower(c, o, idx); + RESET_ERROR_CODE(); + expr_ref e = to_optimize_ref(o).get_lower(idx); + mk_c(c)->save_ast_trail(e); + RETURN_Z3(of_expr(e)); + Z3_CATCH_RETURN(0); } // get upper or current approximation Z3_ast Z3_API Z3_optimize_get_upper(Z3_context c, Z3_optimize o, unsigned idx) { - NOT_IMPLEMENTED_YET(); - return 0; + Z3_TRY; + LOG_Z3_optimize_get_upper(c, o, idx); + RESET_ERROR_CODE(); + expr_ref e = to_optimize_ref(o).get_upper(idx); + mk_c(c)->save_ast_trail(e); + RETURN_Z3(of_expr(e)); + Z3_CATCH_RETURN(0); } #if 0 diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs index 8ac0c8f98..5d3e1ad7a 100644 --- a/src/api/dotnet/Context.cs +++ b/src/api/dotnet/Context.cs @@ -3466,6 +3466,18 @@ namespace Microsoft.Z3 } #endregion + #region Optimization + /// + /// Create an Optimization context. + /// + public Optimize MkOptimize() + { + Contract.Ensures(Contract.Result() != null); + + return new Optimize(this); + } + #endregion + #region Miscellaneous /// @@ -3639,6 +3651,7 @@ namespace Microsoft.Z3 Contract.Invariant(m_Statistics_DRQ != null); Contract.Invariant(m_Tactic_DRQ != null); Contract.Invariant(m_Fixedpoint_DRQ != null); + Contract.Invariant(m_Optimize_DRQ != null); } readonly private AST.DecRefQueue m_AST_DRQ = new AST.DecRefQueue(); @@ -3656,6 +3669,7 @@ namespace Microsoft.Z3 readonly private Statistics.DecRefQueue m_Statistics_DRQ = new Statistics.DecRefQueue(); readonly private Tactic.DecRefQueue m_Tactic_DRQ = new Tactic.DecRefQueue(); readonly private Fixedpoint.DecRefQueue m_Fixedpoint_DRQ = new Fixedpoint.DecRefQueue(); + readonly private Optimize.DecRefQueue m_Optimize_DRQ = new Optimize.DecRefQueue(); internal AST.DecRefQueue AST_DRQ { get { Contract.Ensures(Contract.Result() != null); return m_AST_DRQ; } } internal ASTMap.DecRefQueue ASTMap_DRQ { get { Contract.Ensures(Contract.Result() != null); return m_ASTMap_DRQ; } } @@ -3672,6 +3686,7 @@ namespace Microsoft.Z3 internal Statistics.DecRefQueue Statistics_DRQ { get { Contract.Ensures(Contract.Result() != null); return m_Statistics_DRQ; } } internal Tactic.DecRefQueue Tactic_DRQ { get { Contract.Ensures(Contract.Result() != null); return m_Tactic_DRQ; } } internal Fixedpoint.DecRefQueue Fixedpoint_DRQ { get { Contract.Ensures(Contract.Result() != null); return m_Fixedpoint_DRQ; } } + internal Optimize.DecRefQueue Optimize_DRQ { get { Contract.Ensures(Contract.Result() != null); return m_Optimize_DRQ; } } internal uint refCount = 0; @@ -3715,6 +3730,7 @@ namespace Microsoft.Z3 Statistics_DRQ.Clear(this); Tactic_DRQ.Clear(this); Fixedpoint_DRQ.Clear(this); + Optimize_DRQ.Clear(this); m_boolSort = null; m_intSort = null; diff --git a/src/api/dotnet/Optimize.cs b/src/api/dotnet/Optimize.cs new file mode 100644 index 000000000..3b54dca20 --- /dev/null +++ b/src/api/dotnet/Optimize.cs @@ -0,0 +1,166 @@ +/*++ +Copyright (c) 2012 Microsoft Corporation + +Module Name: + + Optimize.cs + +Abstract: + + Z3 Managed API: Optimizes + +Author: + + Nikolaj Bjorner (nbjorner) 2013-12-03 + +Notes: + +--*/ + +using System; +using System.Diagnostics.Contracts; + +namespace Microsoft.Z3 +{ + /// + /// Object for managing optimizization context + /// + [ContractVerification(true)] + public class Optimize : Z3Object + { + +#if false + /// + /// A string that describes all available optimize solver parameters. + /// + public string Help + { + get + { + Contract.Ensures(Contract.Result() != null); + return Native.Z3_optimize_get_help(Context.nCtx, NativeObject); + } + } +#endif + + /// + /// Sets the optimize solver parameters. + /// + public Params Parameters + { + set + { + Contract.Requires(value != null); + Context.CheckContextMatch(value); + Native.Z3_optimize_set_params(Context.nCtx, NativeObject, value.NativeObject); + } + } + + /// + /// Retrieves parameter descriptions for Optimize solver. + /// + public ParamDescrs ParameterDescriptions + { + get { return new ParamDescrs(Context, Native.Z3_optimize_get_param_descrs(Context.nCtx, NativeObject)); } + } + + + /// + /// Assert a constraint (or multiple) into the optimize solver. + /// + public void Assert(params BoolExpr[] constraints) + { + Contract.Requires(constraints != null); + Contract.Requires(Contract.ForAll(constraints, c => c != null)); + + Context.CheckContextMatch(constraints); + foreach (BoolExpr a in constraints) + { + Native.Z3_optimize_assert(Context.nCtx, NativeObject, a.NativeObject); + } + } + + /// + /// Alias for Assert. + /// + public void Add(params BoolExpr[] constraints) + { + Assert(constraints); + } + + /// + /// Assert soft constraint + /// + public void AssertSoft(BoolExpr constraint, uint weight, string group) + { + Context.CheckContextMatch(constraint); + Symbol s = Context.MkSymbol(group); + Native.Z3_optimize_assert_soft(Context.nCtx, NativeObject, constraint.NativeObject, weight.ToString(), s.NativeObject); + } + + + public Status Check() { + Z3_lbool r = (Z3_lbool)Native.Z3_optimize_check(Context.nCtx, NativeObject); + switch (r) + { + case Z3_lbool.Z3_L_TRUE: return Status.SATISFIABLE; + case Z3_lbool.Z3_L_FALSE: return Status.UNSATISFIABLE; + default: return Status.UNKNOWN; + } + } + + public void Maximize(ArithExpr e) { + Native.Z3_optimize_maximize(Context.nCtx, NativeObject, e.NativeObject); + } + + public void Minimize(ArithExpr e) { + Native.Z3_optimize_minimize(Context.nCtx, NativeObject, e.NativeObject); + } + + public ArithExpr GetLower(uint index) { + return new ArithExpr(Context, Native.Z3_optimize_get_lower(Context.nCtx, NativeObject, index)); + } + + public ArithExpr GetUpper(uint index) { + return new ArithExpr(Context, Native.Z3_optimize_get_upper(Context.nCtx, NativeObject, index)); + } + + #region Internal + internal Optimize(Context ctx, IntPtr obj) + : base(ctx, obj) + { + Contract.Requires(ctx != null); + } + internal Optimize(Context ctx) + : base(ctx, Native.Z3_mk_optimize(ctx.nCtx)) + { + Contract.Requires(ctx != null); + } + + internal class DecRefQueue : IDecRefQueue + { + public override void IncRef(Context ctx, IntPtr obj) + { + Native.Z3_optimize_inc_ref(ctx.nCtx, obj); + } + + public override void DecRef(Context ctx, IntPtr obj) + { + Native.Z3_optimize_dec_ref(ctx.nCtx, obj); + } + }; + + internal override void IncRef(IntPtr o) + { + Context.Optimize_DRQ.IncAndClear(Context, o); + base.IncRef(o); + } + + internal override void DecRef(IntPtr o) + { + Context.Optimize_DRQ.Add(o); + base.DecRef(o); + } + #endregion + } +} diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index ff6955b7b..fafd88ecf 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -21,6 +21,7 @@ Notes: #include "ast_pp.h" #include "opt_solver.h" #include "opt_params.hpp" +#include "arith_decl_plugin.h" namespace opt { @@ -52,8 +53,10 @@ namespace opt { } void context::add_objective(app* t, bool is_max) { - app_ref tr(m); - m_objectives.push_back(objective(is_max, tr)); + app_ref tr(t, m); + unsigned index = m_optsmt.get_num_objectives(); + m_optsmt.add(t, is_max); + m_objectives.push_back(objective(is_max, tr, index)); } lbool context::optimize() { @@ -79,27 +82,26 @@ namespace opt { } } - lbool context::execute_min_max(app* obj, bool committed, bool is_max) { - // HACK: reuse m_optsmt but add only a single objective each round - m_optsmt.add(obj, is_max); + lbool context::execute_min_max(unsigned index, bool committed, bool is_max) { + // HACK: reuse m_optsmt without regard for box reuse and not considering + // use-case of lex. lbool result = m_optsmt(get_solver()); - if (committed) m_optsmt.commit_assignment(0); + if (committed) m_optsmt.commit_assignment(index); return result; } lbool context::execute_maxsat(symbol const& id, bool committed) { - maxsmt* ms; - VERIFY(m_maxsmts.find(id, ms)); - lbool result = (*ms)(get_solver()); - if (committed) ms->commit_assignment(); + maxsmt& ms = *m_maxsmts.find(id); + lbool result = ms(get_solver()); + if (committed) ms.commit_assignment(); return result; } lbool context::execute(objective const& obj, bool committed) { switch(obj.m_type) { - case O_MAXIMIZE: return execute_min_max(obj.m_term, committed, true); - case O_MINIMIZE: return execute_min_max(obj.m_term, committed, false); + case O_MAXIMIZE: return execute_min_max(obj.m_index, committed, true); + case O_MINIMIZE: return execute_min_max(obj.m_index, committed, false); case O_MAXSMT: return execute_maxsat(obj.m_id, committed); default: UNREACHABLE(); return l_undef; } @@ -181,28 +183,59 @@ namespace opt { } expr_ref context::get_lower(unsigned idx) { - NOT_IMPLEMENTED_YET(); if (idx > m_objectives.size()) { throw default_exception("index out of bounds"); } objective const& obj = m_objectives[idx]; switch(obj.m_type) { - case O_MAXSMT: { - maxsmt* ms = m_maxsmts.find(obj.m_id); - inf_eps l = ms->get_lower(); - break; - } - case O_MAXIMIZE: + case O_MAXSMT: + return to_expr(m_maxsmts.find(obj.m_id)->get_lower()); case O_MINIMIZE: - break; + case O_MAXIMIZE: + return to_expr(m_optsmt.get_lower(obj.m_index)); + default: + UNREACHABLE(); + return expr_ref(m); } - - return expr_ref(0,m); } expr_ref context::get_upper(unsigned idx) { - NOT_IMPLEMENTED_YET(); - return expr_ref(0, m); + if (idx > m_objectives.size()) { + throw default_exception("index out of bounds"); + } + objective const& obj = m_objectives[idx]; + switch(obj.m_type) { + case O_MAXSMT: + return to_expr(m_maxsmts.find(obj.m_id)->get_upper()); + case O_MINIMIZE: + case O_MAXIMIZE: + return to_expr(m_optsmt.get_upper(obj.m_index)); + default: + UNREACHABLE(); + return expr_ref(m); + } + } + + expr_ref context::to_expr(inf_eps const& n) { + rational inf = n.get_infinity(); + rational r = n.get_rational(); + rational eps = n.get_infinitesimal(); + expr_ref_vector args(m); + arith_util a(m); + if (!inf.is_zero()) { + args.push_back(a.mk_mul(a.mk_numeral(inf, inf.is_int()), m.mk_const(symbol("oo"), a.mk_int()))); + } + if (!r.is_zero()) { + args.push_back(a.mk_numeral(r, r.is_int())); + } + if (!eps.is_zero()) { + args.push_back(a.mk_mul(a.mk_numeral(eps, eps.is_int()), m.mk_const(symbol("epsilon"), a.mk_int()))); + } + switch(args.size()) { + case 0: return expr_ref(a.mk_numeral(rational(0), true), m); + case 1: return expr_ref(args[0].get(), m); + default: return expr_ref(a.mk_add(args.size(), args.c_ptr()), m); + } } void context::set_cancel(bool f) { diff --git a/src/opt/opt_context.h b/src/opt/opt_context.h index 30b7bf77b..9a0b49541 100644 --- a/src/opt/opt_context.h +++ b/src/opt/opt_context.h @@ -45,15 +45,18 @@ namespace opt { objective_t m_type; app_ref m_term; // for maximize, minimize symbol m_id; // for maxsmt - objective(bool is_max, app_ref& t): + unsigned m_index; + objective(bool is_max, app_ref& t, unsigned idx): m_type(is_max?O_MAXIMIZE:O_MINIMIZE), m_term(t), - m_id() + m_id(), + m_index(idx) {} objective(ast_manager& m, symbol id): m_type(O_MAXSMT), m_term(m), - m_id(id) + m_id(id), + m_index(0) {} }; ast_manager& m; @@ -88,11 +91,12 @@ namespace opt { void validate_feasibility(maxsmt& ms); lbool execute(objective const& obj, bool committed); - lbool execute_min_max(app* obj, bool committed, bool is_max); + lbool execute_min_max(unsigned index, bool committed, bool is_max); lbool execute_maxsat(symbol const& s, bool committed); lbool execute_lex(); lbool execute_box(); lbool execute_pareto(); + expr_ref to_expr(inf_eps const& n); void push(); void pop(unsigned sz);