Z3 |

Data Structures | Public Member Functions
Optimize Class Reference
Inheritance diagram for Optimize:

## Data Structures
class | Handle

## Public Member Functions
String | getHelp ()
void | setParameters (Params value)
ParamDescrs | getParameterDescriptions ()
void | Assert (Expr< BoolSort > ... constraints)
void | Add (Expr< BoolSort > ... constraints)
void | AssertAndTrack (Expr< BoolSort > constraint, Expr< BoolSort > p)
Handle<?> | AssertSoft (Expr< BoolSort > constraint, int weight, String group)
Status | Check (Expr< BoolSort >... assumptions)
void | Push ()
void | Pop ()
Model | getModel ()
BoolExpr[] | getUnsatCore ()
String | getReasonUnknown ()
String | toString ()
void | fromFile (String file)
void | fromString (String s)
BoolExpr[] | getAssertions ()
Expr<?>[] | getObjectives ()
Statistics | getStatistics ()

## Additional Inherited Members
Static Public Member Functions inherited from Z3Object
static long[] | arrayToNative (Z3Object[] a)
static int | arrayLength (Z3Object[] a)

## Detailed Description

Object for managing optimization context

Definition at line 28 of file Optimize.java.

## Member Function Documentation

## ◆ Add()

void Add | ( | Expr< BoolSort > ... | constraints | ) |
| inline

Alias for Assert.

Definition at line 71 of file Optimize.java.

72 {
73 Assert(constraints);
74 }
com.microsoft.z3.Optimize.Assert
void Assert(Expr< BoolSort > ... constraints)
Definition: Optimize.java:59

## ◆ Assert()

void Assert | ( | Expr< BoolSort > ... | constraints | ) |
| inline

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

Definition at line 59 of file Optimize.java.

60 {
61 getContext().checkContextMatch(constraints);
62 for (Expr<BoolSort> a : constraints)
63 {
64 Native.optimizeAssert(getContext().nCtx(), getNativeObject(), a.getNativeObject());
65 }
66 }

## ◆ AssertAndTrack()

void AssertAndTrack | ( | Expr< BoolSort > | constraint,
|  | Expr< BoolSort > | p
| ) |  |
| inline

Assert a constraint into the optimizer, and track it (in the unsat) core using the Boolean constant p.

Remarks: This API is an alternative to `check` with assumptions for extracting unsat cores. Both APIs can be used in the same solver. The unsat core will contain a combination of the Boolean variables provided using `assertAndTrack` and the Boolean literals provided using `check` with assumptions.

Definition at line 89 of file Optimize.java.

90 {
91 getContext().checkContextMatch(constraint);
92 getContext().checkContextMatch(p);
93
94 Native.optimizeAssertAndTrack(getContext().nCtx(), getNativeObject(),
95 constraint.getNativeObject(), p.getNativeObject());
96 }

## ◆ AssertSoft()

Handle<?> AssertSoft | ( | Expr< BoolSort > | constraint,
|  | int | weight,
|  | String | group
| ) |  |
| inline

Assert soft constraint

Return an objective which associates with the group of constraints.

Definition at line 175 of file Optimize.java.

176 {
177 getContext().checkContextMatch(constraint);
178 Symbol s = getContext().mkSymbol(group);
179 return new Handle<>(this, Native.optimizeAssertSoft(getContext().nCtx(), getNativeObject(), constraint.getNativeObject(), Integer.toString(weight), s.getNativeObject()));
180 }
com.microsoft.z3.Context.mkSymbol
IntSymbol mkSymbol(int i)
Definition: Context.java:94
com.microsoft.z3.Expr.toString
String toString()
Definition: Expr.java:208

## ◆ Check()

Status Check | ( | Expr< BoolSort >... | 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 187 of file Optimize.java.

188 {
189 Z3_lbool r;
190 if (assumptions == null) {
191 r = Z3_lbool.fromInt(
192 Native.optimizeCheck(
193 getContext().nCtx(),
194 getNativeObject(), 0, null));
195 }
196 else {
197 r = Z3_lbool.fromInt(
198 Native.optimizeCheck(
199 getContext().nCtx(),
200 getNativeObject(),
201 assumptions.length,
202 AST.arrayToNative(assumptions)));
203 }
204 switch (r) {
205 case Z3_L_TRUE:
206 return Status.SATISFIABLE;
207 case Z3_L_FALSE:
208 return Status.UNSATISFIABLE;
209 default:
210 return Status.UNKNOWN;
211 }
212 }
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
Z3_L_TRUE
@ Z3_L_TRUE
Definition: z3_api.h:105
Z3_L_FALSE
@ Z3_L_FALSE
Definition: z3_api.h:103

## ◆ 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 356 of file Optimize.java.

357 {
358 Native.optimizeFromFile(getContext().nCtx(), getNativeObject(), file);
359 }

## ◆ fromString()

void fromString | ( | String | s | ) |
| inline

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

Definition at line 364 of file Optimize.java.

365 {
366 Native.optimizeFromString(getContext().nCtx(), getNativeObject(), s);
367 }

## ◆ getAssertions()

BoolExpr[] getAssertions | ( |  | ) |
| inline

The set of asserted formulas.

Definition at line 372 of file Optimize.java.

373 {
374 ASTVector assertions = new ASTVector(getContext(), Native.optimizeGetAssertions(getContext().nCtx(), getNativeObject()));
375 return assertions.ToBoolExprArray();
376 }

## ◆ getHelp()

String getHelp | ( |  | ) |
| inline

A string that describes all available optimize solver parameters.

Definition at line 33 of file Optimize.java.

34 {
35 return Native.optimizeGetHelp(getContext().nCtx(), getNativeObject());
36 }

## ◆ getModel()

Model getModel | ( |  | ) |
| inline

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 239 of file Optimize.java.

240 {
241 long x = Native.optimizeGetModel(getContext().nCtx(), getNativeObject());
242 if (x == 0) {
243 return null;
244 } else {
245 return new Model(getContext(), x);
246 }
247 }
z3py.Model
def Model(ctx=None)
Definition: z3py.py:6579

## ◆ getObjectives()

Expr<?>[] getObjectives | ( |  | ) |
| inline

The set of asserted formulas.

Definition at line 381 of file Optimize.java.

382 {
383 ASTVector objectives = new ASTVector(getContext(), Native.optimizeGetObjectives(getContext().nCtx(), getNativeObject()));
384 return objectives.ToExprArray();
385 }

## ◆ getParameterDescriptions()

ParamDescrs getParameterDescriptions | ( |  | ) |
| inline

Retrieves parameter descriptions for Optimize solver.

Definition at line 51 of file Optimize.java.

52 {
53 return new ParamDescrs(getContext(), Native.optimizeGetParamDescrs(getContext().nCtx(), getNativeObject()));
54 }

## ◆ getReasonUnknown()

String getReasonUnknown | ( |  | ) |
| inline

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

Definition at line 338 of file Optimize.java.

339 {
340 return Native.optimizeGetReasonUnknown(getContext().nCtx(), getNativeObject());
341 }

## ◆ getStatistics()

Statistics getStatistics | ( |  | ) |
| inline

Optimize statistics.

Definition at line 390 of file Optimize.java.

391 {
392 return new Statistics(getContext(), Native.optimizeGetStatistics(getContext().nCtx(), getNativeObject()));
393 }

## ◆ getUnsatCore()

BoolExpr[] getUnsatCore | ( |  | ) |
| inline

The unsat core of the last `Check`. Remarks: 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.

Exceptions

  Z3Exception |

Definition at line 258 of file Optimize.java.

259 {
260 ASTVector core = new ASTVector(getContext(), Native.optimizeGetUnsatCore(getContext().nCtx(), getNativeObject()));
261 return core.ToBoolExprArray();
262 }

## ◆ Pop()

void Pop | ( |  | ) |
| inline

Backtrack one backtracking point.

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

Definition at line 227 of file Optimize.java.

228 {
229 Native.optimizePop(getContext().nCtx(), getNativeObject());
230 }

## ◆ Push()

void Push | ( |  | ) |
| inline

Creates a backtracking point.

Definition at line 217 of file Optimize.java.

218 {
219 Native.optimizePush(getContext().nCtx(), getNativeObject());
220 }

## ◆ setParameters()

void setParameters | ( | Params | value | ) |
| inline

Sets the optimize solver parameters.

Exceptions

  Z3Exception |

Definition at line 43 of file Optimize.java.

44 {
45 Native.optimizeSetParams(getContext().nCtx(), getNativeObject(), value.getNativeObject());
46 }

## ◆ toString()

String toString | ( |  | ) |
| inline

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

Definition at line 347 of file Optimize.java.

348 {
349 return Native.optimizeToString(getContext().nCtx(), getNativeObject());
350 }