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 (BoolExpr ... constraints)
 
void Add (BoolExpr ... constraints)
 
Handle AssertSoft (BoolExpr constraint, int weight, String group)
 
Status Check (Expr... assumptions)
 
void Push ()
 
void Pop ()
 
Model getModel ()
 
BoolExpr[] getUnsatCore ()
 
Handle MkMaximize (Expr e)
 
Handle MkMinimize (Expr e)
 
String getReasonUnknown ()
 
String toString ()
 
void fromFile (String file)
 
void fromString (String s)
 
BoolExpr[] getAssertions ()
 
Expr[] getObjectives ()
 
Statistics getStatistics ()
 

Detailed Description

Object for managing optimization context

Definition at line 27 of file Optimize.java.

Member Function Documentation

◆ Add()

void Add ( BoolExpr ...  constraints)
inline

Alias for Assert.

Definition at line 70 of file Optimize.java.

71 {
72 Assert(constraints);
73 }
void Assert(BoolExpr ... constraints)
Definition: Optimize.java:58

◆ Assert()

void Assert ( BoolExpr ...  constraints)
inline

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

Definition at line 58 of file Optimize.java.

59 {
60 getContext().checkContextMatch(constraints);
61 for (BoolExpr a : constraints)
62 {
63 Native.optimizeAssert(getContext().nCtx(), getNativeObject(), a.getNativeObject());
64 }
65 }

Referenced by Optimize.Add().

◆ AssertSoft()

Handle AssertSoft ( BoolExpr  constraint,
int  weight,
String  group 
)
inline

Assert soft constraint

Return an objective which associates with the group of constraints.

Definition at line 152 of file Optimize.java.

153 {
154 getContext().checkContextMatch(constraint);
155 Symbol s = getContext().mkSymbol(group);
156 return new Handle(this, Native.optimizeAssertSoft(getContext().nCtx(), getNativeObject(), constraint.getNativeObject(), Integer.toString(weight), s.getNativeObject()));
157 }
IntSymbol mkSymbol(int i)
Definition: Context.java:93

◆ Check()

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

165 {
166 Z3_lbool r;
167 if (assumptions == null) {
168 r = Z3_lbool.fromInt(
169 Native.optimizeCheck(
170 getContext().nCtx(),
171 getNativeObject(), 0, null));
172 }
173 else {
174 r = Z3_lbool.fromInt(
175 Native.optimizeCheck(
176 getContext().nCtx(),
177 getNativeObject(),
178 assumptions.length,
179 AST.arrayToNative(assumptions)));
180 }
181 switch (r) {
182 case Z3_L_TRUE:
183 return Status.SATISFIABLE;
184 case Z3_L_FALSE:
185 return Status.UNSATISFIABLE;
186 default:
187 return Status.UNKNOWN;
188 }
189 }
Z3_lbool
Lifted Boolean type: false, undefined, true.
Definition: z3_api.h:100
@ Z3_L_TRUE
Definition: z3_api.h:103
@ Z3_L_FALSE
Definition: z3_api.h:101

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

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

◆ fromString()

void fromString ( String  s)
inline

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

Definition at line 341 of file Optimize.java.

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

◆ getAssertions()

BoolExpr[] getAssertions ( )
inline

The set of asserted formulas.

Definition at line 349 of file Optimize.java.

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

◆ getHelp()

String getHelp ( )
inline

A string that describes all available optimize solver parameters.

Definition at line 32 of file Optimize.java.

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

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

217 {
218 long x = Native.optimizeGetModel(getContext().nCtx(), getNativeObject());
219 if (x == 0) {
220 return null;
221 } else {
222 return new Model(getContext(), x);
223 }
224 }
def Model(ctx=None)
Definition: z3py.py:6236

◆ getObjectives()

Expr[] getObjectives ( )
inline

The set of asserted formulas.

Definition at line 358 of file Optimize.java.

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

◆ getParameterDescriptions()

ParamDescrs getParameterDescriptions ( )
inline

Retrieves parameter descriptions for Optimize solver.

Definition at line 50 of file Optimize.java.

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

◆ getReasonUnknown()

String getReasonUnknown ( )
inline

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

Definition at line 315 of file Optimize.java.

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

◆ getStatistics()

Statistics getStatistics ( )
inline

Optimize statistics.

Definition at line 367 of file Optimize.java.

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

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

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

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

Definition at line 246 of file Optimize.java.

247 {
248 return new Handle(this, Native.optimizeMaximize(getContext().nCtx(), getNativeObject(), e.getNativeObject()));
249 }

◆ MkMinimize()

Handle MkMinimize ( Expr  e)
inline

Declare an arithmetical minimization objective. Similar to MkMaximize.

Definition at line 255 of file Optimize.java.

256 {
257 return new Handle(this, Native.optimizeMinimize(getContext().nCtx(), getNativeObject(), e.getNativeObject()));
258 }

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

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

◆ Push()

void Push ( )
inline

Creates a backtracking point.

Definition at line 194 of file Optimize.java.

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

◆ setParameters()

void setParameters ( Params  value)
inline

Sets the optimize solver parameters.

Exceptions
Z3Exception

Definition at line 42 of file Optimize.java.

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

◆ toString()

String toString ( )
inline

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

Definition at line 324 of file Optimize.java.

325 {
326 return Native.optimizeToString(getContext().nCtx(), getNativeObject());
327 }