mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
add .NET interface and finish C interface for optimization
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
9e2908c3f5
commit
e3fe80fd4d
|
@ -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
|
||||
|
|
|
@ -3466,6 +3466,18 @@ namespace Microsoft.Z3
|
|||
}
|
||||
#endregion
|
||||
|
||||
#region Optimization
|
||||
/// <summary>
|
||||
/// Create an Optimization context.
|
||||
/// </summary>
|
||||
public Optimize MkOptimize()
|
||||
{
|
||||
Contract.Ensures(Contract.Result<Optimize>() != null);
|
||||
|
||||
return new Optimize(this);
|
||||
}
|
||||
#endregion
|
||||
|
||||
|
||||
#region Miscellaneous
|
||||
/// <summary>
|
||||
|
@ -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<AST.DecRefQueue>() != null); return m_AST_DRQ; } }
|
||||
internal ASTMap.DecRefQueue ASTMap_DRQ { get { Contract.Ensures(Contract.Result<ASTMap.DecRefQueue>() != null); return m_ASTMap_DRQ; } }
|
||||
|
@ -3672,6 +3686,7 @@ namespace Microsoft.Z3
|
|||
internal Statistics.DecRefQueue Statistics_DRQ { get { Contract.Ensures(Contract.Result<Statistics.DecRefQueue>() != null); return m_Statistics_DRQ; } }
|
||||
internal Tactic.DecRefQueue Tactic_DRQ { get { Contract.Ensures(Contract.Result<Tactic.DecRefQueue>() != null); return m_Tactic_DRQ; } }
|
||||
internal Fixedpoint.DecRefQueue Fixedpoint_DRQ { get { Contract.Ensures(Contract.Result<Fixedpoint.DecRefQueue>() != null); return m_Fixedpoint_DRQ; } }
|
||||
internal Optimize.DecRefQueue Optimize_DRQ { get { Contract.Ensures(Contract.Result<Optimize.DecRefQueue>() != 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;
|
||||
|
|
166
src/api/dotnet/Optimize.cs
Normal file
166
src/api/dotnet/Optimize.cs
Normal file
|
@ -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
|
||||
{
|
||||
/// <summary>
|
||||
/// Object for managing optimizization context
|
||||
/// </summary>
|
||||
[ContractVerification(true)]
|
||||
public class Optimize : Z3Object
|
||||
{
|
||||
|
||||
#if false
|
||||
/// <summary>
|
||||
/// A string that describes all available optimize solver parameters.
|
||||
/// </summary>
|
||||
public string Help
|
||||
{
|
||||
get
|
||||
{
|
||||
Contract.Ensures(Contract.Result<string>() != null);
|
||||
return Native.Z3_optimize_get_help(Context.nCtx, NativeObject);
|
||||
}
|
||||
}
|
||||
#endif
|
||||
|
||||
/// <summary>
|
||||
/// Sets the optimize solver parameters.
|
||||
/// </summary>
|
||||
public Params Parameters
|
||||
{
|
||||
set
|
||||
{
|
||||
Contract.Requires(value != null);
|
||||
Context.CheckContextMatch(value);
|
||||
Native.Z3_optimize_set_params(Context.nCtx, NativeObject, value.NativeObject);
|
||||
}
|
||||
}
|
||||
|
||||
/// <summary>
|
||||
/// Retrieves parameter descriptions for Optimize solver.
|
||||
/// </summary>
|
||||
public ParamDescrs ParameterDescriptions
|
||||
{
|
||||
get { return new ParamDescrs(Context, Native.Z3_optimize_get_param_descrs(Context.nCtx, NativeObject)); }
|
||||
}
|
||||
|
||||
|
||||
/// <summary>
|
||||
/// Assert a constraint (or multiple) into the optimize solver.
|
||||
/// </summary>
|
||||
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);
|
||||
}
|
||||
}
|
||||
|
||||
/// <summary>
|
||||
/// Alias for Assert.
|
||||
/// </summary>
|
||||
public void Add(params BoolExpr[] constraints)
|
||||
{
|
||||
Assert(constraints);
|
||||
}
|
||||
|
||||
/// <summary>
|
||||
/// Assert soft constraint
|
||||
/// </summary>
|
||||
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
|
||||
}
|
||||
}
|
|
@ -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) {
|
||||
|
|
|
@ -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);
|
||||
|
|
Loading…
Reference in a new issue