Z3
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()
165  {
166  Z3_lbool r = Z3_lbool.fromInt(Native.optimizeCheck(getContext().nCtx(), getNativeObject()));
167  switch (r) {
168  case Z3_L_TRUE:
169  return Status.SATISFIABLE;
170  case Z3_L_FALSE:
171  return Status.UNSATISFIABLE;
172  default:
173  return Status.UNKNOWN;
174  }
175  }
176 
180  public void Push()
181  {
182  Native.optimizePush(getContext().nCtx(), getNativeObject());
183  }
184 
190  public void Pop()
191  {
192  Native.optimizePop(getContext().nCtx(), getNativeObject());
193  }
194 
195 
202  public Model getModel()
203  {
204  long x = Native.optimizeGetModel(getContext().nCtx(), getNativeObject());
205  if (x == 0) {
206  return null;
207  } else {
208  return new Model(getContext(), x);
209  }
210  }
211 
217  public Handle MkMaximize(Expr e)
218  {
219  return new Handle(this, Native.optimizeMaximize(getContext().nCtx(), getNativeObject(), e.getNativeObject()));
220  }
221 
226  public Handle MkMinimize(Expr e)
227  {
228  return new Handle(this, Native.optimizeMinimize(getContext().nCtx(), getNativeObject(), e.getNativeObject()));
229  }
230 
234  private Expr GetLower(int index)
235  {
236  return Expr.create(getContext(), Native.optimizeGetLower(getContext().nCtx(), getNativeObject(), index));
237  }
238 
242  private Expr GetUpper(int index)
243  {
244  return Expr.create(getContext(), Native.optimizeGetUpper(getContext().nCtx(), getNativeObject(), index));
245  }
246 
252  private Expr[] GetUpperAsVector(int index) {
253  return unpackObjectiveValueVector(
255  getContext().nCtx(), getNativeObject(), index
256  )
257  );
258  }
259 
265  private Expr[] GetLowerAsVector(int index) {
266  return unpackObjectiveValueVector(
268  getContext().nCtx(), getNativeObject(), index
269  )
270  );
271  }
272 
273  private Expr[] unpackObjectiveValueVector(long nativeVec) {
274  ASTVector vec = new ASTVector(
275  getContext(), nativeVec
276  );
277  return new Expr[] {
278  (Expr) vec.get(0), (Expr) vec.get(1), (Expr) vec.get(2)
279  };
280 
281  }
282 
287  {
288  return Native.optimizeGetReasonUnknown(getContext().nCtx(), getNativeObject());
289  }
290 
294  @Override
295  public String toString()
296  {
297  return Native.optimizeToString(getContext().nCtx(), getNativeObject());
298  }
299 
304  public void fromFile(String file)
305  {
306  Native.optimizeFromFile(getContext().nCtx(), getNativeObject(), file);
307  }
308 
312  public void fromString(String s)
313  {
314  Native.optimizeFromString(getContext().nCtx(), getNativeObject(), s);
315  }
316 
317 
322  {
323  return new Statistics(getContext(), Native.optimizeGetStatistics(getContext().nCtx(), getNativeObject()));
324  }
325 
326 
327  Optimize(Context ctx, long obj) throws Z3Exception
328  {
329  super(ctx, obj);
330  }
331 
332  Optimize(Context ctx) throws Z3Exception
333  {
334  super(ctx, Native.mkOptimize(ctx.nCtx()));
335  }
336 
337  @Override
338  void incRef() {
339  Native.optimizeIncRef(getContext().nCtx(), getNativeObject());
340  }
341 
342  @Override
343  void addToReferenceQueue() {
344  getContext().getOptimizeDRQ().storeReference(getContext(), this);
345  }
346 }
static long optimizeGetUpper(long a0, long a1, int a2)
Definition: Native.java:5535
void Assert(BoolExpr ... constraints)
Definition: Optimize.java:58
void fromFile(String file)
Definition: Optimize.java:304
static void optimizePop(long a0, long a1)
Definition: Native.java:5474
static void optimizeSetParams(long a0, long a1, long a2)
Definition: Native.java:5509
static int optimizeAssertSoft(long a0, long a1, long a2, String a3, long a4)
Definition: Native.java:5439
static void optimizePush(long a0, long a1)
Definition: Native.java:5466
static long optimizeGetStatistics(long a0, long a1)
Definition: Native.java:5596
static String optimizeGetReasonUnknown(long a0, long a1)
Definition: Native.java:5491
static long optimizeGetModel(long a0, long a1)
Definition: Native.java:5500
static void optimizeAssert(long a0, long a1, long a2)
Definition: Native.java:5431
static int optimizeMinimize(long a0, long a1, long a2)
Definition: Native.java:5457
static long optimizeGetLowerAsVector(long a0, long a1, int a2)
Definition: Native.java:5544
static String optimizeGetHelp(long a0, long a1)
Definition: Native.java:5587
void fromString(String s)
Definition: Optimize.java:312
static String optimizeToString(long a0, long a1)
Definition: Native.java:5562
ParamDescrs getParameterDescriptions()
Definition: Optimize.java:50
static int optimizeMaximize(long a0, long a1, long a2)
Definition: Native.java:5448
static long optimizeGetUpperAsVector(long a0, long a1, int a2)
Definition: Native.java:5553
Handle MkMaximize(Expr e)
Definition: Optimize.java:217
Statistics getStatistics()
Definition: Optimize.java:321
Handle MkMinimize(Expr e)
Definition: Optimize.java:226
static long optimizeGetLower(long a0, long a1, int a2)
Definition: Native.java:5526
void Add(BoolExpr ... constraints)
Definition: Optimize.java:70
Handle AssertSoft(BoolExpr constraint, int weight, String group)
Definition: Optimize.java:152
static long optimizeGetParamDescrs(long a0, long a1)
Definition: Native.java:5517
static void optimizeFromString(long a0, long a1, String a2)
Definition: Native.java:5571
void setParameters(Params value)
Definition: Optimize.java:42
static void optimizeFromFile(long a0, long a1, String a2)
Definition: Native.java:5579
static int optimizeCheck(long a0, long a1)
Definition: Native.java:5482
static void optimizeIncRef(long a0, long a1)
Definition: Native.java:5415
static long mkOptimize(long a0)
Definition: Native.java:5406
def String(name, ctx=None)
Definition: z3py.py:9821
static final Z3_lbool fromInt(int v)
Definition: Z3_lbool.java:34