mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 19:27:06 +00:00
Code Activity

Expose objective indices to .NET API

Browse source
This commit is contained in:
Anh-Dung Phan 2013-12-05 17:30:40 -08:00
parent 5fc429c501
commit d38e2b9b78
5 changed files with 90 additions and 44 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

24
src/api/api_opt.cpp
View file

@ -72,32 +72,32 @@ extern "C" {
Z3_CATCH;
}
void Z3_API Z3_optimize_assert_soft(Z3_context c, Z3_optimize o, Z3_ast a, Z3_string weight, Z3_symbol id) {
unsigned Z3_API Z3_optimize_assert_soft(Z3_context c, Z3_optimize o, Z3_ast a, Z3_string weight, Z3_symbol id) {
Z3_TRY;
LOG_Z3_optimize_assert_soft(c, o, a, weight, id);
RESET_ERROR_CODE();
CHECK_FORMULA(a,);
CHECK_FORMULA(a,0);
rational w("weight");
to_optimize_ref(o).add_soft_constraint(to_expr(a), w, to_symbol(id));
Z3_CATCH;
return to_optimize_ref(o).add_soft_constraint(to_expr(a), w, to_symbol(id));
Z3_CATCH_RETURN(0);
}
void Z3_API Z3_optimize_maximize(Z3_context c, Z3_optimize o, Z3_ast t) {
unsigned Z3_API Z3_optimize_maximize(Z3_context c, Z3_optimize o, Z3_ast t) {
Z3_TRY;
LOG_Z3_optimize_maximize(c, o, t);
RESET_ERROR_CODE();
CHECK_VALID_AST(t,);
to_optimize_ref(o).add_objective(to_app(t), true);
Z3_CATCH;
CHECK_VALID_AST(t,0);
return to_optimize_ref(o).add_objective(to_app(t), true);
Z3_CATCH_RETURN(0);
}
void Z3_API Z3_optimize_minimize(Z3_context c, Z3_optimize o, Z3_ast t) {
unsigned Z3_API Z3_optimize_minimize(Z3_context c, Z3_optimize o, Z3_ast t) {
Z3_TRY;
LOG_Z3_optimize_minimize(c, o, t);
RESET_ERROR_CODE();
CHECK_VALID_AST(t,);
to_optimize_ref(o).add_objective(to_app(t), false);
Z3_CATCH;
CHECK_VALID_AST(t,0);
return to_optimize_ref(o).add_objective(to_app(t), false);
Z3_CATCH_RETURN(0);
}
Z3_lbool Z3_API Z3_optimize_check(Z3_context c, Z3_optimize o) {

82
src/api/dotnet/Optimize.cs
View file

@ -18,6 +18,7 @@ Notes:
--*/
using System;
using System.Collections.Generic;
using System.Diagnostics.Contracts;
namespace Microsoft.Z3
@ -28,6 +29,7 @@ namespace Microsoft.Z3
[ContractVerification(true)]
public class Optimize : Z3Object
{
HashSet<uint> indices;
#if false
/// <summary>
@ -64,6 +66,26 @@ namespace Microsoft.Z3
get { return new ParamDescrs(Context, Native.Z3_optimize_get_param_descrs(Context.nCtx, NativeObject)); }
}
/// <summary>
/// Get the number of objectives.
/// </summary>
public uint ObjectiveCount
{
get { return (uint)indices.Count; }
}
/// <summary>
/// Get all indices of objectives.
/// </summary>
public uint[] Objectives
{
get
{
var objectives = new uint[indices.Count];
indices.CopyTo(objectives, 0);
return objectives;
}
}
/// <summary>
/// Assert a constraint (or multiple) into the optimize solver.
@ -91,21 +113,28 @@ namespace Microsoft.Z3
/// <summary>
/// Assert soft constraint
/// </summary>
public void AssertSoft(BoolExpr constraint, uint weight, string group)
/// <remarks>
/// Return an objective which associates with the group of constraints.
/// </remarks>
public uint 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);
Symbol s = Context.MkSymbol(group);
uint index = Native.Z3_optimize_assert_soft(Context.nCtx, NativeObject, constraint.NativeObject, weight.ToString(), s.NativeObject);
indices.Add(index);
return index;
}
public Status Check() {
Z3_lbool r = (Z3_lbool)Native.Z3_optimize_check(Context.nCtx, 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;
case Z3_lbool.Z3_L_TRUE:
return Status.SATISFIABLE;
case Z3_lbool.Z3_L_FALSE:
return Status.UNSATISFIABLE;
default:
return Status.UNKNOWN;
}
}
@ -127,22 +156,31 @@ namespace Microsoft.Z3
return new Model(Context, x);
}
}
public uint MkMaximize(ArithExpr e)
{
uint index = Native.Z3_optimize_maximize(Context.nCtx, NativeObject, e.NativeObject);
indices.Add(index);
return index;
}
public void Maximize(ArithExpr e) {
Native.Z3_optimize_maximize(Context.nCtx, NativeObject, e.NativeObject);
}
public uint MkMinimize(ArithExpr e)
{
uint index = Native.Z3_optimize_minimize(Context.nCtx, NativeObject, e.NativeObject);
indices.Add(index);
return index;
}
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 GetLower(uint index)
{
Contract.Requires(indices.Contains(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));
public ArithExpr GetUpper(uint index)
{
Contract.Requires(indices.Contains(index));
return new ArithExpr(Context, Native.Z3_optimize_get_upper(Context.nCtx, NativeObject, index));
}
#region Internal
@ -150,11 +188,13 @@ namespace Microsoft.Z3
: base(ctx, obj)
{
Contract.Requires(ctx != null);
indices = new HashSet<uint>();
}
internal Optimize(Context ctx)
: base(ctx, Native.Z3_mk_optimize(ctx.nCtx))
{
Contract.Requires(ctx != null);
indices = new HashSet<uint>();
}
internal class DecRefQueue : IDecRefQueue

12
src/api/z3_api.h
View file

@ -5987,9 +5987,9 @@ END_MLAPI_EXCLUDE
\param weight - a positive weight, penalty for violating soft constraint
\param id - optional identifier to group soft constraints
def_API('Z3_optimize_assert_soft', VOID, (_in(CONTEXT), _in(OPTIMIZE), _in(AST), _in(STRING), _in(SYMBOL)))
def_API('Z3_optimize_assert_soft', UINT, (_in(CONTEXT), _in(OPTIMIZE), _in(AST), _in(STRING), _in(SYMBOL)))
*/
void Z3_API Z3_optimize_assert_soft(Z3_context c, Z3_optimize o, Z3_ast a, Z3_string weight, Z3_symbol id);
unsigned Z3_API Z3_optimize_assert_soft(Z3_context c, Z3_optimize o, Z3_ast a, Z3_string weight, Z3_symbol id);
/**
@ -5997,9 +5997,9 @@ END_MLAPI_EXCLUDE
\param c - context
\param o - optimization context
\param a - arithmetical term
def_API('Z3_optimize_maximize', VOID, (_in(CONTEXT), _in(OPTIMIZE), _in(AST)))
def_API('Z3_optimize_maximize', UINT, (_in(CONTEXT), _in(OPTIMIZE), _in(AST)))
*/
void Z3_API Z3_optimize_maximize(Z3_context, Z3_optimize o, Z3_ast t);
unsigned Z3_API Z3_optimize_maximize(Z3_context, Z3_optimize o, Z3_ast t);
/**
\brief Add a minimiztion constraint.
@ -6007,9 +6007,9 @@ END_MLAPI_EXCLUDE
\param o - optimization context
\param a - arithmetical term
def_API('Z3_optimize_minimize', VOID, (_in(CONTEXT), _in(OPTIMIZE), _in(AST)))
def_API('Z3_optimize_minimize', UINT, (_in(CONTEXT), _in(OPTIMIZE), _in(AST)))
*/
void Z3_API Z3_optimize_minimize(Z3_context, Z3_optimize o, Z3_ast t);
unsigned Z3_API Z3_optimize_minimize(Z3_context, Z3_optimize o, Z3_ast t);
/**
\brief Check consistency and produce optimal values.

10
src/opt/opt_context.cpp
View file

@ -42,21 +42,25 @@ namespace opt {
}
}
void context::add_soft_constraint(expr* f, rational const& w, symbol const& id) {
unsigned context::add_soft_constraint(expr* f, rational const& w, symbol const& id) {
maxsmt* ms;
if (!m_maxsmts.find(id, ms)) {
ms = alloc(maxsmt, m);
m_maxsmts.insert(id, ms);
m_objectives.push_back(objective(m, id));
m_indices.insert(id, m_objectives.size() - 1);
}
ms->add(f, w);
ms->add(f, w);
SASSERT(m_indices.contains(id));
return m_indices[id];
}
void context::add_objective(app* t, bool is_max) {
unsigned context::add_objective(app* t, bool is_max) {
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));
return index;
}
lbool context::optimize() {

6
src/opt/opt_context.h
View file

@ -36,6 +36,7 @@ namespace opt {
class context {
typedef map<symbol, maxsmt*, symbol_hash_proc, symbol_eq_proc> map_t;
typedef map<symbol, unsigned, symbol_hash_proc, symbol_eq_proc> map_id;
enum objective_t {
O_MAXIMIZE,
O_MINIMIZE,
@ -65,13 +66,14 @@ namespace opt {
params_ref m_params;
optsmt m_optsmt;
map_t m_maxsmts;
map_id m_indices;
vector<objective> m_objectives;
model_ref m_model;
public:
context(ast_manager& m);
~context();
void add_soft_constraint(expr* f, rational const& w, symbol const& id);
void add_objective(app* t, bool is_max);
unsigned add_soft_constraint(expr* f, rational const& w, symbol const& id);
unsigned add_objective(app* t, bool is_max);
void add_hard_constraint(expr* f) { m_hard_constraints.push_back(f); }
lbool optimize();