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 ()
 
void Push ()
 
void Pop ()
 
Model getModel ()
 
Handle MkMaximize (ArithExpr e)
 
Handle MkMinimize (ArithExpr e)
 
String getReasonUnknown ()
 
String toString ()
 
Statistics getStatistics ()
 

Detailed Description

Object for managing optimizization context

Definition at line 28 of file Optimize.java.

Member Function Documentation

§ Add()

void Add ( BoolExpr ...  constraints)
inline

Alias for Assert.

Definition at line 71 of file Optimize.java.

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

§ Assert()

void Assert ( BoolExpr ...  constraints)
inline

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

Definition at line 59 of file Optimize.java.

Referenced by Optimize.Add().

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

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

131  {
132  getContext().checkContextMatch(constraint);
133  Symbol s = getContext().mkSymbol(group);
134  return new Handle(this, Native.optimizeAssertSoft(getContext().nCtx(), getNativeObject(), constraint.getNativeObject(), Integer.toString(weight), s.getNativeObject()));
135  }
IntSymbol mkSymbol(int i)
Definition: Context.java:81

§ Check()

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

145  {
146  Z3_lbool r = Z3_lbool.fromInt(Native.optimizeCheck(getContext().nCtx(), getNativeObject()));
147  switch (r) {
148  case Z3_L_TRUE:
149  return Status.SATISFIABLE;
150  case Z3_L_FALSE:
151  return Status.UNSATISFIABLE;
152  default:
153  return Status.UNKNOWN;
154  }
155  }
Z3_lbool
Lifted Boolean type: false, undefined, true.
Definition: z3_api.h:105
Status
Status values.
Definition: Status.cs:27

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

185  {
186  long x = Native.optimizeGetModel(getContext().nCtx(), getNativeObject());
187  if (x == 0) {
188  return null;
189  } else {
190  return new Model(getContext(), x);
191  }
192  }

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

234  {
235  return Native.optimizeGetReasonUnknown(getContext().nCtx(),
236  getNativeObject());
237  }

§ getStatistics()

Statistics getStatistics ( )
inline

Optimize statistics.

Definition at line 252 of file Optimize.java.

253  {
254  return new Statistics(getContext(), Native.optimizeGetStatistics(getContext().nCtx(), getNativeObject()));
255  }

§ MkMaximize()

Handle MkMaximize ( ArithExpr  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 199 of file Optimize.java.

200  {
201  return new Handle(this, Native.optimizeMaximize(getContext().nCtx(), getNativeObject(), e.getNativeObject()));
202  }

§ MkMinimize()

Handle MkMinimize ( ArithExpr  e)
inline

Declare an arithmetical minimization objective. Similar to MkMaximize.

Definition at line 208 of file Optimize.java.

209  {
210  return new Handle(this, Native.optimizeMinimize(getContext().nCtx(), getNativeObject(), e.getNativeObject()));
211  }

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

173  {
174  Native.optimizePop(getContext().nCtx(), getNativeObject());
175  }

§ Push()

void Push ( )
inline

Creates a backtracking point.

Definition at line 160 of file Optimize.java.

161  {
162  Native.optimizePush(getContext().nCtx(), getNativeObject());
163  }

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

245  {
246  return Native.optimizeToString(getContext().nCtx(), getNativeObject());
247  }