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)
 
Handle<?> AssertSoft (Expr< BoolSort > constraint, String 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  }
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() [1/2]

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  return AssertSoft(constraint, Integer.toString(weight), group);
178  }
Handle<?> AssertSoft(Expr< BoolSort > constraint, int weight, String group)
Definition: Optimize.java:175

◆ AssertSoft() [2/2]

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

Assert soft constraint

Return an objective which associates with the group of constraints.

Definition at line 186 of file Optimize.java.

187  {
188  getContext().checkContextMatch(constraint);
189  Symbol s = getContext().mkSymbol(group);
190  return new Handle<>(this, Native.optimizeAssertSoft(getContext().nCtx(), getNativeObject(), constraint.getNativeObject(), weight, s.getNativeObject()));
191  }
IntSymbol mkSymbol(int i)
Definition: Context.java:94

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

199  {
200  Z3_lbool r;
201  if (assumptions == null) {
202  r = Z3_lbool.fromInt(
203  Native.optimizeCheck(
204  getContext().nCtx(),
205  getNativeObject(), 0, null));
206  }
207  else {
208  r = Z3_lbool.fromInt(
209  Native.optimizeCheck(
210  getContext().nCtx(),
211  getNativeObject(),
212  assumptions.length,
213  AST.arrayToNative(assumptions)));
214  }
215  switch (r) {
216  case Z3_L_TRUE:
217  return Status.SATISFIABLE;
218  case Z3_L_FALSE:
219  return Status.UNSATISFIABLE;
220  default:
221  return Status.UNKNOWN;
222  }
223  }
Z3_lbool
Lifted Boolean type: false, undefined, true.
Definition: z3_api.h:60
@ Z3_L_TRUE
Definition: z3_api.h:63
@ Z3_L_FALSE
Definition: z3_api.h:61
Status
Status values.
Definition: Status.cs:29

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

368  {
369  Native.optimizeFromFile(getContext().nCtx(), getNativeObject(), file);
370  }

◆ fromString()

void fromString ( String  s)
inline

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

Definition at line 375 of file Optimize.java.

376  {
377  Native.optimizeFromString(getContext().nCtx(), getNativeObject(), s);
378  }

◆ getAssertions()

BoolExpr [] getAssertions ( )
inline

The set of asserted formulas.

Definition at line 383 of file Optimize.java.

384  {
385  ASTVector assertions = new ASTVector(getContext(), Native.optimizeGetAssertions(getContext().nCtx(), getNativeObject()));
386  return assertions.ToBoolExprArray();
387  }

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

251  {
252  long x = Native.optimizeGetModel(getContext().nCtx(), getNativeObject());
253  if (x == 0) {
254  return null;
255  } else {
256  return new Model(getContext(), x);
257  }
258  }
def Model(ctx=None)
Definition: z3py.py:6689

◆ getObjectives()

Expr<?> [] getObjectives ( )
inline

The set of asserted formulas.

Definition at line 392 of file Optimize.java.

393  {
394  ASTVector objectives = new ASTVector(getContext(), Native.optimizeGetObjectives(getContext().nCtx(), getNativeObject()));
395  return objectives.ToExprArray();
396  }

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

350  {
351  return Native.optimizeGetReasonUnknown(getContext().nCtx(), getNativeObject());
352  }

◆ getStatistics()

Statistics getStatistics ( )
inline

Optimize statistics.

Definition at line 401 of file Optimize.java.

402  {
403  return new Statistics(getContext(), Native.optimizeGetStatistics(getContext().nCtx(), getNativeObject()));
404  }

◆ getUnsatCore()

BoolExpr [] getUnsatCore ( )
inline

The unsat core of the last

Status Check(Expr< BoolSort >... assumptions)
Definition: Optimize.java:198

. Remarks: The unsat core is a subset of

Assumptions

The result is empty if

was not invoked before, if its results was not

@ UNSATISFIABLE
Used to signify an unsatisfiable status.

, or if core production is disabled.

Exceptions
Z3Exception

Definition at line 269 of file Optimize.java.

270  {
271  ASTVector core = new ASTVector(getContext(), Native.optimizeGetUnsatCore(getContext().nCtx(), getNativeObject()));
272  return core.ToBoolExprArray();
273  }

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

239  {
240  Native.optimizePop(getContext().nCtx(), getNativeObject());
241  }

◆ Push()

void Push ( )
inline

Creates a backtracking point.

Definition at line 228 of file Optimize.java.

229  {
230  Native.optimizePush(getContext().nCtx(), getNativeObject());
231  }

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

359  {
360  return Native.optimizeToString(getContext().nCtx(), getNativeObject());
361  }