diff --git a/src/api/dotnet/Optimize.cs b/src/api/dotnet/Optimize.cs
index a9499570b..eb8281e5f 100644
--- a/src/api/dotnet/Optimize.cs
+++ b/src/api/dotnet/Optimize.cs
@@ -85,17 +85,55 @@ namespace Microsoft.Z3
Assert(constraints);
}
+ ///
+ /// Handle to objectives returned by objective functions.
+ ///
+ public class Handle
+ {
+ Optimize opt;
+ uint handle;
+ internal Handle(Optimize opt, uint h)
+ {
+ this.opt = opt;
+ this.handle = h;
+ }
+
+ ///
+ /// Retrieve a lower bound for the objective handle.
+ ///
+ public ArithExpr Lower()
+ {
+ return opt.GetLower(handle);
+ }
+
+ ///
+ /// Retrieve an upper bound for the objective handle.
+ ///
+ public ArithExpr Upper()
+ {
+ return opt.GetUpper(handle);
+ }
+
+ ///
+ /// Retrieve the value of an objective.
+ ///
+ public ArithExpr Value()
+ {
+ return Lower();
+ }
+ }
+
///
/// Assert soft constraint
///
///
/// Return an objective which associates with the group of constraints.
///
- public uint AssertSoft(BoolExpr constraint, uint weight, string group)
+ public Handle AssertSoft(BoolExpr constraint, uint weight, string group)
{
Context.CheckContextMatch(constraint);
Symbol s = Context.MkSymbol(group);
- return Native.Z3_optimize_assert_soft(Context.nCtx, NativeObject, constraint.NativeObject, weight.ToString(), s.NativeObject);
+ return new Handle(this, Native.Z3_optimize_assert_soft(Context.nCtx, NativeObject, constraint.NativeObject, weight.ToString(), s.NativeObject));
}
@@ -161,26 +199,26 @@ namespace Microsoft.Z3
///
/// Declare an arithmetical maximization objective.
/// Return a handle to the objective. The handle is used as
- /// an argument to GetLower and GetUpper.
+ /// to retrieve the values of objectives after calling Check.
///
- public uint MkMaximize(ArithExpr e)
+ public Handle MkMaximize(ArithExpr e)
{
- return Native.Z3_optimize_maximize(Context.nCtx, NativeObject, e.NativeObject);
+ return new Handle(this, Native.Z3_optimize_maximize(Context.nCtx, NativeObject, e.NativeObject));
}
///
/// Declare an arithmetical minimization objective.
/// Similar to MkMaximize.
///
- public uint MkMinimize(ArithExpr e)
+ public Handle MkMinimize(ArithExpr e)
{
- return Native.Z3_optimize_minimize(Context.nCtx, NativeObject, e.NativeObject);
+ return new Handle(this, Native.Z3_optimize_minimize(Context.nCtx, NativeObject, e.NativeObject));
}
///
/// Retrieve a lower bound for the objective handle.
///
- public ArithExpr GetLower(uint index)
+ private ArithExpr GetLower(uint index)
{
return (ArithExpr)Expr.Create(Context, Native.Z3_optimize_get_lower(Context.nCtx, NativeObject, index));
}
@@ -189,7 +227,7 @@ namespace Microsoft.Z3
///
/// Retrieve an upper bound for the objective handle.
///
- public ArithExpr GetUpper(uint index)
+ private ArithExpr GetUpper(uint index)
{
return (ArithExpr)Expr.Create(Context, Native.Z3_optimize_get_upper(Context.nCtx, NativeObject, index));
}