Z3 |

Data Structures | Public Member Functions | Properties
Optimize Class Reference

Object for managing optimization context More...

Inheritance diagram for Optimize:

## Data Structures
class | DecRefQueue
class | Handle
| Handle to objectives returned by objective functions. More...

## Public Member Functions
void | Set (string name, bool value)
| Sets parameter on the optimize solver More...
void | Set (string name, uint value)
| Sets parameter on the optimize solver More...
void | Set (string name, double value)
| Sets parameter on the optimize solver More...
void | Set (string name, string value)
| Sets parameter on the optimize solver More...
void | Set (string name, Symbol value)
| Sets parameter on the optimize solver More...
void | Set (Symbol name, bool value)
| Sets parameter on the optimize solver More...
void | Set (Symbol name, uint value)
| Sets parameter on the optimize solver More...
void | Set (Symbol name, double value)
| Sets parameter on the optimize solver More...
void | Set (Symbol name, string value)
| Sets parameter on the optimize solver More...
void | Set (Symbol name, Symbol value)
| Sets parameter on the optimize solver More...
void | Assert (params BoolExpr[] constraints)
| Assert a constraint (or multiple) into the optimize solver. More...
void | Assert (IEnumerable< BoolExpr > constraints)
| Assert a constraint (or multiple) into the optimize solver. More...
void | Add (params BoolExpr[] constraints)
| Alias for Assert. More...
void | Add (IEnumerable< BoolExpr > constraints)
| Alias for Assert. More...
Handle | AssertSoft (BoolExpr constraint, uint weight, string group)
| Assert soft constraint More...
Status | Check (params Expr[] assumptions)
| Check satisfiability of asserted constraints. Produce a model that (when the objectives are bounded and don't use strict inequalities) meets the objectives. More...
void | Push ()
| Creates a backtracking point. More...
void | Pop ()
| Backtrack one backtracking point. More...
Handle | MkMaximize (Expr e)
| Declare an arithmetical maximization objective. Return a handle to the objective. The handle is used as to retrieve the values of objectives after calling Check. The expression can be either an arithmetical expression or bit-vector. More...
Handle | MkMinimize (Expr e)
| Declare an arithmetical minimization objective. Similar to MkMaximize. More...
override string | ToString ()
| Print the context to a string (SMT-LIB parseable benchmark). More...
void | FromFile (string file)
| Parse an SMT-LIB2 file with optimization objectives and constraints. The parsed constraints and objectives are added to the optimization context. More...
void | FromString (string s)
| Similar to FromFile. Instead it takes as argument a string. More...
Public Member Functions inherited from Z3Object
void | Dispose ()
| Disposes of the underlying native Z3 object. More...

## Properties
string | Help`[get]`
| A string that describes all available optimize solver parameters. More...
Params | Parameters`[set]`
| Sets the optimize solver parameters. More...
ParamDescrs | ParameterDescriptions`[get]`
| Retrieves parameter descriptions for Optimize solver. More...
Model | Model`[get]`
| The model of the last `Check`. More...
BoolExpr[] | UnsatCore`[get]`
| The unsat core of the last `Check`. More...
String | ReasonUnknown`[get]`
| Return a string the describes why the last to check returned unknown More...
BoolExpr[] | Assertions`[get]`
| The set of asserted formulas. More...
Expr[] | Objectives`[get]`
| The set of asserted formulas. More...
Statistics | Statistics`[get]`
| Optimize statistics. More...

## Detailed Description

Object for managing optimization context

Definition at line 30 of file Optimize.cs.

## Member Function Documentation

## ◆ Add() [1/2]

void Add | ( | IEnumerable< BoolExpr > | constraints | ) |
| inline

Alias for Assert.

Definition at line 132 of file Optimize.cs.

133 {
134 AddConstraints(constraints);
135 }

## ◆ Add() [2/2]

void Add | ( | params BoolExpr[] | constraints | ) |
| inline

Alias for Assert.

Definition at line 124 of file Optimize.cs.

125 {
126 AddConstraints(constraints);
127 }

## ◆ Assert() [1/2]

void Assert | ( | IEnumerable< BoolExpr > | constraints | ) |
| inline

Assert a constraint (or multiple) into the optimize solver.

Definition at line 116 of file Optimize.cs.

117 {
118 AddConstraints(constraints);
119 }

## ◆ Assert() [2/2]

void Assert | ( | params BoolExpr[] | constraints | ) |
| inline

Assert a constraint (or multiple) into the optimize solver.

Definition at line 108 of file Optimize.cs.

109 {
110 AddConstraints(constraints);
111 }

## ◆ AssertSoft()

Handle AssertSoft | ( | BoolExpr | constraint,
|  | uint | weight,
|  | string | group
| ) |  |
| inline

Assert soft constraint

Return an objective which associates with the group of constraints.

Definition at line 212 of file Optimize.cs.

213 {
214 Context.CheckContextMatch(constraint);
215 Symbol s = Context.MkSymbol(group);
216 return new Handle(this, Native.Z3_optimize_assert_soft(Context.nCtx, NativeObject, constraint.NativeObject, weight.ToString(), s.NativeObject));
217 }
Microsoft.Z3.Context.MkSymbol
IntSymbol MkSymbol(int i)
Creates a new symbol using an integer.
Definition: Context.cs:90

## ◆ Check()

Status Check | ( | params Expr[] | assumptions | ) |
| inline

Check satisfiability of asserted constraints. Produce a model that (when the objectives are bounded and don't use strict inequalities) meets the objectives.

Definition at line 226 of file Optimize.cs.

227 {
228 Z3_lbool r = (Z3_lbool)Native.Z3_optimize_check(Context.nCtx, NativeObject, (uint)assumptions.Length, AST.ArrayToNative(assumptions));
229 switch (r)
230 {
231 case Z3_lbool.Z3_L_TRUE:
232 return Status.SATISFIABLE;
233 case Z3_lbool.Z3_L_FALSE:
234 return Status.UNSATISFIABLE;
235 default:
236 return Status.UNKNOWN;
237 }
238 }
Microsoft.Z3.Status
Status
Status values.
Definition: Status.cs:29
Z3_lbool
Z3_lbool
Lifted Boolean type: false, undefined, true.
Definition: z3_api.h:102

## ◆ FromFile()

void FromFile | ( | string | file | ) |
| inline

Parse an SMT-LIB2 file with optimization objectives and constraints. The parsed constraints and objectives are added to the optimization context.

Definition at line 378 of file Optimize.cs.

379 {
380 Native.Z3_optimize_from_file(Context.nCtx, NativeObject, file);
381 }

## ◆ FromString()

void FromString | ( | string | s | ) |
| inline

Similar to FromFile. Instead it takes as argument a string.

Definition at line 386 of file Optimize.cs.

387 {
388 Native.Z3_optimize_from_string(Context.nCtx, NativeObject, s);
389 }

## ◆ MkMaximize()

Handle MkMaximize | ( | Expr | e | ) |
| inline

Declare an arithmetical maximization objective. Return a handle to the objective. The handle is used as to retrieve the values of objectives after calling Check. The expression can be either an arithmetical expression or bit-vector.

Definition at line 303 of file Optimize.cs.

304 {
305 return new Handle(this, Native.Z3_optimize_maximize(Context.nCtx, NativeObject, e.NativeObject));
306 }

## ◆ MkMinimize()

Handle MkMinimize | ( | Expr | e | ) |
| inline

Declare an arithmetical minimization objective. Similar to MkMaximize.

Definition at line 312 of file Optimize.cs.

313 {
314 return new Handle(this, Native.Z3_optimize_minimize(Context.nCtx, NativeObject, e.NativeObject));
315 }

## ◆ Pop()

void Pop | ( |  | ) |
| inline

Backtrack one backtracking point.

Note that an exception is thrown if Pop is called without a corresponding `Push`

See also
  Push

Definition at line 254 of file Optimize.cs.

255 {
256 Native.Z3_optimize_pop(Context.nCtx, NativeObject);
257 }

## ◆ Push()

void Push | ( |  | ) |
| inline

Creates a backtracking point.

See also
  Pop

Definition at line 244 of file Optimize.cs.

245 {
246 Native.Z3_optimize_push(Context.nCtx, NativeObject);
247 }

## ◆ Set() [1/10]

void Set | ( | string | name,
|  | bool | value
| ) |  |
| inline

Sets parameter on the optimize solver

Definition at line 59 of file Optimize.cs.

59{ Parameters = Context.MkParams().Add(name, value); }
Microsoft.Z3.Context.MkParams
Params MkParams()
Creates a new ParameterSet.
Definition: Context.cs:3290
Microsoft.Z3.Optimize.Parameters
Params Parameters
Sets the optimize solver parameters.
Definition: Optimize.cs:47
Microsoft.Z3.Params.Add
Params Add(Symbol name, bool value)
Adds a parameter setting.
Definition: Params.cs:33

## ◆ Set() [2/10]

void Set | ( | string | name,
|  | double | value
| ) |  |
| inline

Sets parameter on the optimize solver

Definition at line 67 of file Optimize.cs.

67{ Parameters = Context.MkParams().Add(name, value); }

## ◆ Set() [3/10]

void Set | ( | string | name,
|  | string | value
| ) |  |
| inline

Sets parameter on the optimize solver

Definition at line 71 of file Optimize.cs.

71{ Parameters = Context.MkParams().Add(name, value); }

## ◆ Set() [4/10]

void Set | ( | string | name,
|  | Symbol | value
| ) |  |
| inline

Sets parameter on the optimize solver

Definition at line 75 of file Optimize.cs.

75{ Parameters = Context.MkParams().Add(name, value); }

## ◆ Set() [5/10]

void Set | ( | string | name,
|  | uint | value
| ) |  |
| inline

Sets parameter on the optimize solver

Definition at line 63 of file Optimize.cs.

63{ Parameters = Context.MkParams().Add(name, value); }

## ◆ Set() [6/10]

void Set | ( | Symbol | name,
|  | bool | value
| ) |  |
| inline

Sets parameter on the optimize solver

Definition at line 79 of file Optimize.cs.

79{ Parameters = Context.MkParams().Add(name, value); }

## ◆ Set() [7/10]

void Set | ( | Symbol | name,
|  | double | value
| ) |  |
| inline

Sets parameter on the optimize solver

Definition at line 87 of file Optimize.cs.

87{ Parameters = Context.MkParams().Add(name, value); }

## ◆ Set() [8/10]

void Set | ( | Symbol | name,
|  | string | value
| ) |  |
| inline

Sets parameter on the optimize solver

Definition at line 91 of file Optimize.cs.

91{ Parameters = Context.MkParams().Add(name, value); }

## ◆ Set() [9/10]

void Set | ( | Symbol | name,
|  | Symbol | value
| ) |  |
| inline

Sets parameter on the optimize solver

Definition at line 95 of file Optimize.cs.

95{ Parameters = Context.MkParams().Add(name, value); }

## ◆ Set() [10/10]

void Set | ( | Symbol | name,
|  | uint | value
| ) |  |
| inline

Sets parameter on the optimize solver

Definition at line 83 of file Optimize.cs.

83{ Parameters = Context.MkParams().Add(name, value); }

## ◆ ToString()

override string ToString | ( |  | ) |
| inline

Print the context to a string (SMT-LIB parseable benchmark).

Definition at line 369 of file Optimize.cs.

370 {
371 return Native.Z3_optimize_to_string(Context.nCtx, NativeObject);
372 }

## Property Documentation

## ◆ Assertions

BoolExpr [] Assertions
| get

The set of asserted formulas.

Definition at line 394 of file Optimize.cs.

395 {
396 get
397 {
398
399 ASTVector assertions = new ASTVector(Context, Native.Z3_optimize_get_assertions(Context.nCtx, NativeObject));
400 return assertions.ToBoolExprArray();
401 }
402 }

## ◆ Help

string Help
| get

A string that describes all available optimize solver parameters.

Definition at line 35 of file Optimize.cs.

36 {
37 get
38 {
39 return Native.Z3_optimize_get_help(Context.nCtx, NativeObject);
40 }
41 }

## ◆ Model

Model Model
| get

The model of the last `Check`.

The result is `null` if `Check` was not invoked before, if its results was not `SATISFIABLE`, or if model production is not enabled.

Definition at line 267 of file Optimize.cs.

268 {
269 get
270 {
271 IntPtr x = Native.Z3_optimize_get_model(Context.nCtx, NativeObject);
272 if (x == IntPtr.Zero)
273 return null;
274 else
275 return new Model(Context, x);
276 }
277 }
Microsoft.Z3.Optimize.Model
Model Model
The model of the last Check.
Definition: Optimize.cs:268

## ◆ Objectives

Expr [] Objectives
| get

The set of asserted formulas.

Definition at line 407 of file Optimize.cs.

408 {
409 get
410 {
411
412 ASTVector objectives = new ASTVector(Context, Native.Z3_optimize_get_objectives(Context.nCtx, NativeObject));
413 return objectives.ToExprArray();
414 }
415 }

## ◆ ParameterDescriptions

ParamDescrs ParameterDescriptions
| get

Retrieves parameter descriptions for Optimize solver.

Definition at line 100 of file Optimize.cs.

101 {
102 get { return new ParamDescrs(Context, Native.Z3_optimize_get_param_descrs(Context.nCtx, NativeObject)); }
103 }

## ◆ Parameters

Params Parameters
| set

Sets the optimize solver parameters.

Definition at line 46 of file Optimize.cs.

47 {
48 set
49 {
50 Debug.Assert(value != null);
51 Context.CheckContextMatch(value);
52 Native.Z3_optimize_set_params(Context.nCtx, NativeObject, value.NativeObject);
53 }
54 }

Referenced by Optimize.Set().

## ◆ ReasonUnknown

String ReasonUnknown
| get

Return a string the describes why the last to check returned unknown

Definition at line 357 of file Optimize.cs.

358 {
359 get
360 {
361 return Native.Z3_optimize_get_reason_unknown(Context.nCtx, NativeObject);
362 }
363 }

## ◆ Statistics

Statistics Statistics
| get

Optimize statistics.

Definition at line 421 of file Optimize.cs.

422 {
423 get
424 {
425
426 return new Statistics(Context, Native.Z3_optimize_get_statistics(Context.nCtx, NativeObject));
427 }
428 }
Microsoft.Z3.Optimize.Statistics
Statistics Statistics
Optimize statistics.
Definition: Optimize.cs:422

## ◆ UnsatCore

BoolExpr [] UnsatCore
| get

The unsat core of the last `Check`.

The unsat core is a subset of `assumptions` The result is empty if `Check` was not invoked before, if its results was not `UNSATISFIABLE`, or if core production is disabled.

Definition at line 287 of file Optimize.cs.

288 {
289 get
290 {
291
292 ASTVector core = new ASTVector(Context, Native.Z3_optimize_get_unsat_core(Context.nCtx, NativeObject));
293 return core.ToBoolExprArray();
294 }
295 }