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);