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)
 
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  }

◆ 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  }

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

154  {
155  getContext().checkContextMatch(constraint);
156  Symbol s = getContext().mkSymbol(group);
157  return new Handle<>(this, Native.optimizeAssertSoft(getContext().nCtx(), getNativeObject(), constraint.getNativeObject(), Integer.toString(weight), s.getNativeObject()));
158  }

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

166  {
167  Z3_lbool r;
168  if (assumptions == null) {
169  r = Z3_lbool.fromInt(
170  Native.optimizeCheck(
171  getContext().nCtx(),
172  getNativeObject(), 0, null));
173  }
174  else {
175  r = Z3_lbool.fromInt(
176  Native.optimizeCheck(
177  getContext().nCtx(),
178  getNativeObject(),
179  assumptions.length,
180  AST.arrayToNative(assumptions)));
181  }
182  switch (r) {
183  case Z3_L_TRUE:
184  return Status.SATISFIABLE;
185  case Z3_L_FALSE:
186  return Status.UNSATISFIABLE;
187  default:
188  return Status.UNKNOWN;
189  }
190  }

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

335  {
336  Native.optimizeFromFile(getContext().nCtx(), getNativeObject(), file);
337  }

◆ fromString()

void fromString ( String  s)
inline

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

Definition at line 342 of file Optimize.java.

343  {
344  Native.optimizeFromString(getContext().nCtx(), getNativeObject(), s);
345  }

◆ getAssertions()

BoolExpr [] getAssertions ( )
inline

The set of asserted formulas.

Definition at line 350 of file Optimize.java.

351  {
352  ASTVector assertions = new ASTVector(getContext(), Native.optimizeGetAssertions(getContext().nCtx(), getNativeObject()));
353  return assertions.ToBoolExprArray();
354  }

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

218  {
219  long x = Native.optimizeGetModel(getContext().nCtx(), getNativeObject());
220  if (x == 0) {
221  return null;
222  } else {
223  return new Model(getContext(), x);
224  }
225  }

◆ getObjectives()

Expr<?> [] getObjectives ( )
inline

The set of asserted formulas.

Definition at line 359 of file Optimize.java.

360  {
361  ASTVector objectives = new ASTVector(getContext(), Native.optimizeGetObjectives(getContext().nCtx(), getNativeObject()));
362  return objectives.ToExprArray();
363  }

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

317  {
318  return Native.optimizeGetReasonUnknown(getContext().nCtx(), getNativeObject());
319  }

◆ getStatistics()

Statistics getStatistics ( )
inline

Optimize statistics.

Definition at line 368 of file Optimize.java.

369  {
370  return new Statistics(getContext(), Native.optimizeGetStatistics(getContext().nCtx(), getNativeObject()));
371  }

◆ getUnsatCore()

BoolExpr [] getUnsatCore ( )
inline

The unsat core of the last

. Remarks: The unsat core is a subset of

Assumptions

The result is empty if

was not invoked before, if its results was not

, or if core production is disabled.

Exceptions
Z3Exception

Definition at line 236 of file Optimize.java.

237  {
238  ASTVector core = new ASTVector(getContext(), Native.optimizeGetUnsatCore(getContext().nCtx(), getNativeObject()));
239  return core.ToBoolExprArray();
240  }

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

206  {
207  Native.optimizePop(getContext().nCtx(), getNativeObject());
208  }

◆ Push()

void Push ( )
inline

Creates a backtracking point.

Definition at line 195 of file Optimize.java.

196  {
197  Native.optimizePush(getContext().nCtx(), getNativeObject());
198  }

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

326  {
327  return Native.optimizeToString(getContext().nCtx(), getNativeObject());
328  }
com.microsoft.z3.Context.mkSymbol
IntSymbol mkSymbol(int i)
Definition: Context.java:94
com.microsoft.z3.Optimize.Assert
void Assert(Expr< BoolSort > ... constraints)
Definition: Optimize.java:59
Microsoft.Z3.Status.UNSATISFIABLE
Used to signify an unsatisfiable status.
Z3_L_TRUE
Definition: z3_api.h:105
Z3_lbool
Z3_lbool
Lifted Boolean type: false, undefined, true.
Definition: z3_api.h:101
z3py.Model
def Model(ctx=None)
Definition: z3py.py:6277
com.microsoft.z3.Optimize.Check
Status Check(Expr< BoolSort >... assumptions)
Definition: Optimize.java:165
com.microsoft.z3.Expr.toString
String toString()
Definition: Expr.java:205
Microsoft.Z3.Status
Status
Status values.
Definition: Status.cs:28
Z3_L_FALSE
Definition: z3_api.h:103