mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-02 12:21:21 +00:00
Code Activity

Formatting

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2015-05-19 12:43:25 +01:00
parent f0b699f03a
commit a41a9c94dd
1 changed files with 49 additions and 49 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -85,43 +85,43 @@ namespace Microsoft.Z3
Assert(constraints); Assert(constraints);
} }
/// <summary> /// <summary>
/// Handle to objectives returned by objective functions. /// Handle to objectives returned by objective functions.
/// </summary> /// </summary>
public class Handle public class Handle
{ {
Optimize opt; Optimize opt;
uint handle; uint handle;
internal Handle(Optimize opt, uint h) internal Handle(Optimize opt, uint h)
{ {
this.opt = opt; this.opt = opt;
this.handle = h; this.handle = h;
} }
/// <summary> /// <summary>
/// Retrieve a lower bound for the objective handle. /// Retrieve a lower bound for the objective handle.
/// </summary> /// </summary>
public ArithExpr Lower public ArithExpr Lower
{ {
get { return opt.GetLower(handle); } get { return opt.GetLower(handle); }
} }
/// <summary> /// <summary>
/// Retrieve an upper bound for the objective handle. /// Retrieve an upper bound for the objective handle.
/// </summary> /// </summary>
public ArithExpr Upper public ArithExpr Upper
{ {
get { return opt.GetUpper(handle); } get { return opt.GetUpper(handle); }
} }
/// <summary> /// <summary>
/// Retrieve the value of an objective. /// Retrieve the value of an objective.
/// </summary> /// </summary>
public ArithExpr Value public ArithExpr Value
{ {
get { return Lower; } get { return Lower; }
} }
} }
/// <summary> /// <summary>
/// Assert soft constraint /// Assert soft constraint
@ -132,29 +132,29 @@ namespace Microsoft.Z3
public Handle AssertSoft(BoolExpr constraint, uint weight, string group) public Handle AssertSoft(BoolExpr constraint, uint weight, string group)
{ {
Context.CheckContextMatch(constraint); Context.CheckContextMatch(constraint);
Symbol s = Context.MkSymbol(group); Symbol s = Context.MkSymbol(group);
return new Handle(this, 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));
} }
/// /// <summary>
/// <summary> /// Check satisfiability of asserted constraints.
/// Check satisfiability of asserted constraints. /// Produce a model that (when the objectives are bounded and
/// Produce a model that (when the objectives are bounded and /// don't use strict inequalities) meets the objectives.
/// don't use strict inequalities) meets the objectives. /// </summary>
/// </summary> ///
/// public Status Check()
public Status Check() { {
Z3_lbool r = (Z3_lbool)Native.Z3_optimize_check(Context.nCtx, NativeObject); Z3_lbool r = (Z3_lbool)Native.Z3_optimize_check(Context.nCtx, NativeObject);
switch (r) switch (r)
{ {
case Z3_lbool.Z3_L_TRUE: case Z3_lbool.Z3_L_TRUE:
return Status.SATISFIABLE; return Status.SATISFIABLE;
case Z3_lbool.Z3_L_FALSE: case Z3_lbool.Z3_L_FALSE:
return Status.UNSATISFIABLE; return Status.UNSATISFIABLE;
default: default:
return Status.UNKNOWN; return Status.UNKNOWN;
} }
} }
/// <summary> /// <summary>
@ -198,27 +198,27 @@ namespace Microsoft.Z3
/// <summary> /// <summary>
/// Declare an arithmetical maximization objective. /// Declare an arithmetical maximization objective.
/// Return a handle to the objective. The handle is used as /// Return a handle to the objective. The handle is used as
/// to retrieve the values of objectives after calling Check. /// to retrieve the values of objectives after calling Check.
/// </summary> /// </summary>
public Handle MkMaximize(ArithExpr e) public Handle MkMaximize(ArithExpr e)
{ {
return new Handle(this, Native.Z3_optimize_maximize(Context.nCtx, NativeObject, e.NativeObject)); return new Handle(this, Native.Z3_optimize_maximize(Context.nCtx, NativeObject, e.NativeObject));
} }
/// <summary> /// <summary>
/// Declare an arithmetical minimization objective. /// Declare an arithmetical minimization objective.
/// Similar to MkMaximize. /// Similar to MkMaximize.
/// </summary> /// </summary>
public Handle MkMinimize(ArithExpr e) public Handle MkMinimize(ArithExpr e)
{ {
return new Handle(this, Native.Z3_optimize_minimize(Context.nCtx, NativeObject, e.NativeObject)); return new Handle(this, Native.Z3_optimize_minimize(Context.nCtx, NativeObject, e.NativeObject));
} }
/// <summary> /// <summary>
/// Retrieve a lower bound for the objective handle. /// Retrieve a lower bound for the objective handle.
/// </summary> /// </summary>
private ArithExpr GetLower(uint index) private ArithExpr GetLower(uint index)
{ {
return (ArithExpr)Expr.Create(Context, Native.Z3_optimize_get_lower(Context.nCtx, NativeObject, index)); return (ArithExpr)Expr.Create(Context, Native.Z3_optimize_get_lower(Context.nCtx, NativeObject, index));
} }
@ -236,7 +236,7 @@ namespace Microsoft.Z3
/// <summary> /// <summary>
/// Print the context to a string (SMT-LIB parseable benchmark). /// Print the context to a string (SMT-LIB parseable benchmark).
/// </summary> /// </summary>
public override string ToString() public override string ToString()
{ {
return Native.Z3_optimize_to_string(Context.nCtx, NativeObject); return Native.Z3_optimize_to_string(Context.nCtx, NativeObject);
} }