Z3
Optimize.java
Go to the documentation of this file.
1 
20 package com.microsoft.z3;
21 
23 
24 
28 public class Optimize extends Z3Object
29 {
33  public String getHelp()
34  {
35  return Native.optimizeGetHelp(getContext().nCtx(), getNativeObject());
36  }
37 
43  public void setParameters(Params value)
44  {
45  Native.optimizeSetParams(getContext().nCtx(), getNativeObject(), value.getNativeObject());
46  }
47 
52  {
53  return new ParamDescrs(getContext(), Native.optimizeGetParamDescrs(getContext().nCtx(), getNativeObject()));
54  }
55 
59  public void Assert(BoolExpr ... constraints)
60  {
61  getContext().checkContextMatch(constraints);
62  for (BoolExpr a : constraints)
63  {
64  Native.optimizeAssert(getContext().nCtx(), getNativeObject(), a.getNativeObject());
65  }
66  }
67 
71  public void Add(BoolExpr ... constraints)
72  {
73  Assert(constraints);
74  }
75 
79  public class Handle
80  {
81  Optimize opt;
82  int handle;
83  Handle(Optimize opt, int h)
84  {
85  this.opt = opt;
86  this.handle = h;
87  }
88 
93  {
94  return opt.GetLower(handle);
95  }
96 
101  {
102  return opt.GetUpper(handle);
103  }
104 
109  {
110  return getLower();
111  }
112 
116  @Override
117  public String toString()
118  {
119  return getValue().toString();
120  }
121  }
122 
130  public Handle AssertSoft(BoolExpr constraint, int weight, String group)
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  }
136 
137 
144  public Status Check()
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  }
156 
160  public void Push()
161  {
162  Native.optimizePush(getContext().nCtx(), getNativeObject());
163  }
164 
165 
172  public void Pop()
173  {
174  Native.optimizePop(getContext().nCtx(), getNativeObject());
175  }
176 
177 
184  public Model getModel()
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  }
193 
200  {
201  return new Handle(this, Native.optimizeMaximize(getContext().nCtx(), getNativeObject(), e.getNativeObject()));
202  }
203 
209  {
210  return new Handle(this, Native.optimizeMinimize(getContext().nCtx(), getNativeObject(), e.getNativeObject()));
211  }
212 
216  private ArithExpr GetLower(int index)
217  {
218  return (ArithExpr)Expr.create(getContext(), Native.optimizeGetLower(getContext().nCtx(), getNativeObject(), index));
219  }
220 
221 
225  private ArithExpr GetUpper(int index)
226  {
227  return (ArithExpr)Expr.create(getContext(), Native.optimizeGetUpper(getContext().nCtx(), getNativeObject(), index));
228  }
229 
234  {
235  return Native.optimizeGetReasonUnknown(getContext().nCtx(),
236  getNativeObject());
237  }
238 
239 
243  @Override
244  public String toString()
245  {
246  return Native.optimizeToString(getContext().nCtx(), getNativeObject());
247  }
248 
253  {
254  return new Statistics(getContext(), Native.optimizeGetStatistics(getContext().nCtx(), getNativeObject()));
255  }
256 
257 
258  Optimize(Context ctx, long obj) throws Z3Exception
259  {
260  super(ctx, obj);
261  }
262 
263  Optimize(Context ctx) throws Z3Exception
264  {
265  super(ctx, Native.mkOptimize(ctx.nCtx()));
266  }
267 
268  @Override
269  void incRef() {
270  Native.optimizeIncRef(getContext().nCtx(), getNativeObject());
271  }
272 
273  @Override
274  void addToReferenceQueue() {
275  getContext().getOptimizeDRQ().storeReference(getContext(), this);
276  }
277 }
static long optimizeGetUpper(long a0, long a1, int a2)
Definition: Native.java:5376
void Assert(BoolExpr ... constraints)
Definition: Optimize.java:59
static void optimizePop(long a0, long a1)
Definition: Native.java:5315
static void optimizeSetParams(long a0, long a1, long a2)
Definition: Native.java:5350
static int optimizeAssertSoft(long a0, long a1, long a2, String a3, long a4)
Definition: Native.java:5280
static void optimizePush(long a0, long a1)
Definition: Native.java:5307
static long optimizeGetStatistics(long a0, long a1)
Definition: Native.java:5419
static String optimizeGetReasonUnknown(long a0, long a1)
Definition: Native.java:5332
static long optimizeGetModel(long a0, long a1)
Definition: Native.java:5341
static void optimizeAssert(long a0, long a1, long a2)
Definition: Native.java:5272
static int optimizeMinimize(long a0, long a1, long a2)
Definition: Native.java:5298
static String optimizeGetHelp(long a0, long a1)
Definition: Native.java:5410
static String optimizeToString(long a0, long a1)
Definition: Native.java:5385
ParamDescrs getParameterDescriptions()
Definition: Optimize.java:51
static int optimizeMaximize(long a0, long a1, long a2)
Definition: Native.java:5289
Handle MkMaximize(ArithExpr e)
Definition: Optimize.java:199
String toString()
Definition: Expr.java:211
Statistics getStatistics()
Definition: Optimize.java:252
static long optimizeGetLower(long a0, long a1, int a2)
Definition: Native.java:5367
void Add(BoolExpr ... constraints)
Definition: Optimize.java:71
Handle AssertSoft(BoolExpr constraint, int weight, String group)
Definition: Optimize.java:130
static long optimizeGetParamDescrs(long a0, long a1)
Definition: Native.java:5358
void setParameters(Params value)
Definition: Optimize.java:43
Handle MkMinimize(ArithExpr e)
Definition: Optimize.java:208
static int optimizeCheck(long a0, long a1)
Definition: Native.java:5323
static void optimizeIncRef(long a0, long a1)
Definition: Native.java:5256
static long mkOptimize(long a0)
Definition: Native.java:5247
def String(name, ctx=None)
Definition: z3py.py:9443
static final Z3_lbool fromInt(int v)
Definition: Z3_lbool.java:34