Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
Optimize.java
Go to the documentation of this file.
1 
19 package com.microsoft.z3;
20 
22 
23 
27 public class Optimize extends Z3Object {
28 
32  public String getHelp()
33  {
34  return Native.optimizeGetHelp(getContext().nCtx(), getNativeObject());
35  }
36 
42  public void setParameters(Params value)
43  {
44  Native.optimizeSetParams(getContext().nCtx(), getNativeObject(), value.getNativeObject());
45  }
46 
51  {
52  return new ParamDescrs(getContext(), Native.optimizeGetParamDescrs(getContext().nCtx(), getNativeObject()));
53  }
54 
58  public void Assert(BoolExpr ... constraints)
59  {
60  getContext().checkContextMatch(constraints);
61  for (BoolExpr a : constraints)
62  {
63  Native.optimizeAssert(getContext().nCtx(), getNativeObject(), a.getNativeObject());
64  }
65  }
66 
70  public void Add(BoolExpr ... constraints)
71  {
72  Assert(constraints);
73  }
74 
78  public static class Handle {
79 
80  private final Optimize opt;
81  private final int handle;
82 
83  Handle(Optimize opt, int h)
84  {
85  this.opt = opt;
86  this.handle = h;
87  }
88 
92  public Expr getLower()
93  {
94  return opt.GetLower(handle);
95  }
96 
100  public Expr getUpper()
101  {
102  return opt.GetUpper(handle);
103  }
104 
113  public Expr[] getUpperAsVector()
114  {
115  return opt.GetUpperAsVector(handle);
116  }
117 
123  public Expr[] getLowerAsVector()
124  {
125  return opt.GetLowerAsVector(handle);
126  }
127 
131  public Expr getValue()
132  {
133  return getLower();
134  }
135 
139  @Override
140  public String toString()
141  {
142  return getValue().toString();
143  }
144  }
145 
152  public Handle AssertSoft(BoolExpr constraint, int weight, String group)
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  }
158 
164  public Status Check(Expr... assumptions)
165  {
166  Z3_lbool r;
167  if (assumptions == null) {
168  r = Z3_lbool.fromInt(
170  getContext().nCtx(),
171  getNativeObject(), 0, null));
172  }
173  else {
174  r = Z3_lbool.fromInt(
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  }
190 
194  public void Push()
195  {
196  Native.optimizePush(getContext().nCtx(), getNativeObject());
197  }
198 
204  public void Pop()
205  {
206  Native.optimizePop(getContext().nCtx(), getNativeObject());
207  }
208 
209 
216  public Model getModel()
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  }
225 
236  {
237  ASTVector core = new ASTVector(getContext(), Native.optimizeGetUnsatCore(getContext().nCtx(), getNativeObject()));
238  return core.ToBoolExprArray();
239  }
240 
246  public Handle MkMaximize(Expr e)
247  {
248  return new Handle(this, Native.optimizeMaximize(getContext().nCtx(), getNativeObject(), e.getNativeObject()));
249  }
250 
255  public Handle MkMinimize(Expr e)
256  {
257  return new Handle(this, Native.optimizeMinimize(getContext().nCtx(), getNativeObject(), e.getNativeObject()));
258  }
259 
263  private Expr GetLower(int index)
264  {
265  return Expr.create(getContext(), Native.optimizeGetLower(getContext().nCtx(), getNativeObject(), index));
266  }
267 
271  private Expr GetUpper(int index)
272  {
273  return Expr.create(getContext(), Native.optimizeGetUpper(getContext().nCtx(), getNativeObject(), index));
274  }
275 
281  private Expr[] GetUpperAsVector(int index) {
282  return unpackObjectiveValueVector(
283  Native.optimizeGetUpperAsVector(
284  getContext().nCtx(), getNativeObject(), index
285  )
286  );
287  }
288 
294  private Expr[] GetLowerAsVector(int index) {
295  return unpackObjectiveValueVector(
296  Native.optimizeGetLowerAsVector(
297  getContext().nCtx(), getNativeObject(), index
298  )
299  );
300  }
301 
302  private Expr[] unpackObjectiveValueVector(long nativeVec) {
303  ASTVector vec = new ASTVector(
304  getContext(), nativeVec
305  );
306  return new Expr[] {
307  (Expr) vec.get(0), (Expr) vec.get(1), (Expr) vec.get(2)
308  };
309 
310  }
311 
316  {
317  return Native.optimizeGetReasonUnknown(getContext().nCtx(), getNativeObject());
318  }
319 
323  @Override
324  public String toString()
325  {
326  return Native.optimizeToString(getContext().nCtx(), getNativeObject());
327  }
328 
333  public void fromFile(String file)
334  {
335  Native.optimizeFromFile(getContext().nCtx(), getNativeObject(), file);
336  }
337 
341  public void fromString(String s)
342  {
343  Native.optimizeFromString(getContext().nCtx(), getNativeObject(), s);
344  }
345 
350  {
351  ASTVector assertions = new ASTVector(getContext(), Native.optimizeGetAssertions(getContext().nCtx(), getNativeObject()));
352  return assertions.ToBoolExprArray();
353  }
354 
358  public Expr[] getObjectives()
359  {
360  ASTVector objectives = new ASTVector(getContext(), Native.optimizeGetObjectives(getContext().nCtx(), getNativeObject()));
361  return objectives.ToExprArray();
362  }
363 
368  {
369  return new Statistics(getContext(), Native.optimizeGetStatistics(getContext().nCtx(), getNativeObject()));
370  }
371 
372 
373  Optimize(Context ctx, long obj) throws Z3Exception
374  {
375  super(ctx, obj);
376  }
377 
378  Optimize(Context ctx) throws Z3Exception
379  {
380  super(ctx, Native.mkOptimize(ctx.nCtx()));
381  }
382 
383  @Override
384  void incRef() {
385  Native.optimizeIncRef(getContext().nCtx(), getNativeObject());
386  }
387 
388  @Override
389  void addToReferenceQueue() {
390  getContext().getOptimizeDRQ().storeReference(getContext(), this);
391  }
392 }
void Add(BoolExpr...constraints)
Definition: Optimize.java:70
void fromFile(String file)
Definition: Optimize.java:333
static void optimizePop(long a0, long a1)
Definition: Native.java:5715
static void optimizeSetParams(long a0, long a1, long a2)
Definition: Native.java:5759
static int optimizeAssertSoft(long a0, long a1, long a2, String a3, long a4)
Definition: Native.java:5680
static void optimizePush(long a0, long a1)
Definition: Native.java:5707
static long optimizeGetStatistics(long a0, long a1)
Definition: Native.java:5846
static long optimizeGetUnsatCore(long a0, long a1)
Definition: Native.java:5750
static String optimizeGetReasonUnknown(long a0, long a1)
Definition: Native.java:5732
static long optimizeGetModel(long a0, long a1)
Definition: Native.java:5741
static void optimizeAssert(long a0, long a1, long a2)
Definition: Native.java:5664
static int optimizeMinimize(long a0, long a1, long a2)
Definition: Native.java:5698
def String
Definition: z3py.py:10043
BoolExpr[] ToBoolExprArray()
Definition: ASTVector.java:140
static String optimizeGetHelp(long a0, long a1)
Definition: Native.java:5837
static int optimizeCheck(long a0, long a1, int a2, long[] a3)
Definition: Native.java:5723
void fromString(String s)
Definition: Optimize.java:341
static String optimizeToString(long a0, long a1)
Definition: Native.java:5812
ParamDescrs getParameterDescriptions()
Definition: Optimize.java:50
static int optimizeMaximize(long a0, long a1, long a2)
Definition: Native.java:5689
IDecRefQueue< Optimize > getOptimizeDRQ()
Definition: Context.java:4101
BoolExpr[] getUnsatCore()
Definition: Optimize.java:235
Handle MkMaximize(Expr e)
Definition: Optimize.java:246
Statistics getStatistics()
Definition: Optimize.java:367
static long optimizeGetObjectives(long a0, long a1)
Definition: Native.java:5864
Handle MkMinimize(Expr e)
Definition: Optimize.java:255
Status Check(Expr...assumptions)
Definition: Optimize.java:164
static long optimizeGetAssertions(long a0, long a1)
Definition: Native.java:5855
static long optimizeGetLower(long a0, long a1, int a2)
Definition: Native.java:5776
Handle AssertSoft(BoolExpr constraint, int weight, String group)
Definition: Optimize.java:152
def Model
Definition: z3py.py:6216
static long optimizeGetParamDescrs(long a0, long a1)
Definition: Native.java:5767
static void optimizeFromString(long a0, long a1, String a2)
Definition: Native.java:5821
IntSymbol mkSymbol(int i)
Definition: Context.java:93
void setParameters(Params value)
Definition: Optimize.java:42
void Assert(BoolExpr...constraints)
Definition: Optimize.java:58
BoolExpr[] getAssertions()
Definition: Optimize.java:349
static void optimizeFromFile(long a0, long a1, String a2)
Definition: Native.java:5829
static final Z3_lbool fromInt(int v)
Definition: Z3_lbool.java:34