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  public String toString()
117  {
118  return getValue().toString();
119  }
120  }
121 
129  public Handle AssertSoft(BoolExpr constraint, int weight, String group)
130  {
131  getContext().checkContextMatch(constraint);
132  Symbol s = getContext().mkSymbol(group);
133  return new Handle(this, Native.optimizeAssertSoft(getContext().nCtx(), getNativeObject(), constraint.getNativeObject(), Integer.toString(weight), s.getNativeObject()));
134  }
135 
136 
143  public Status Check()
144  {
145  Z3_lbool r = Z3_lbool.fromInt(Native.optimizeCheck(getContext().nCtx(), getNativeObject()));
146  switch (r) {
147  case Z3_L_TRUE:
148  return Status.SATISFIABLE;
149  case Z3_L_FALSE:
150  return Status.UNSATISFIABLE;
151  default:
152  return Status.UNKNOWN;
153  }
154  }
155 
159  public void Push()
160  {
161  Native.optimizePush(getContext().nCtx(), getNativeObject());
162  }
163 
164 
171  public void Pop()
172  {
173  Native.optimizePop(getContext().nCtx(), getNativeObject());
174  }
175 
176 
183  public Model getModel()
184  {
185  long x = Native.optimizeGetModel(getContext().nCtx(), getNativeObject());
186  if (x == 0)
187  return null;
188  else
189  return new Model(getContext(), x);
190  }
191 
198  {
199  return new Handle(this, Native.optimizeMaximize(getContext().nCtx(), getNativeObject(), e.getNativeObject()));
200  }
201 
207  {
208  return new Handle(this, Native.optimizeMinimize(getContext().nCtx(), getNativeObject(), e.getNativeObject()));
209  }
210 
214  private ArithExpr GetLower(int index)
215  {
216  return (ArithExpr)Expr.create(getContext(), Native.optimizeGetLower(getContext().nCtx(), getNativeObject(), index));
217  }
218 
219 
223  private ArithExpr GetUpper(int index)
224  {
225  return (ArithExpr)Expr.create(getContext(), Native.optimizeGetUpper(getContext().nCtx(), getNativeObject(), index));
226  }
227 
231  public String getReasonUnknown()
232  {
233  return Native.optimizeGetReasonUnknown(getContext().nCtx(),
234  getNativeObject());
235  }
236 
237 
241  public String toString()
242  {
243  return Native.optimizeToString(getContext().nCtx(), getNativeObject());
244  }
245 
250  {
251  return new Statistics(getContext(), Native.optimizeGetStatistics(getContext().nCtx(), getNativeObject()));
252  }
253 
254 
255  Optimize(Context ctx, long obj) throws Z3Exception
256  {
257  super(ctx, obj);
258  }
259 
260  Optimize(Context ctx) throws Z3Exception
261  {
262  super(ctx, Native.mkOptimize(ctx.nCtx()));
263  }
264 
265 
266  void incRef(long o)
267  {
268  getContext().getOptimizeDRQ().incAndClear(getContext(), o);
269  super.incRef(o);
270  }
271 
272  void decRef(long o)
273  {
274  getContext().getOptimizeDRQ().add(o);
275  super.decRef(o);
276  }
277 
278 }
static long optimizeGetUpper(long a0, long a1, int a2)
Definition: Native.java:3695
void Add(BoolExpr...constraints)
Definition: Optimize.java:71
static void optimizePop(long a0, long a1)
Definition: Native.java:3634
static void optimizeSetParams(long a0, long a1, long a2)
Definition: Native.java:3669
static int optimizeAssertSoft(long a0, long a1, long a2, String a3, long a4)
Definition: Native.java:3599
static void optimizePush(long a0, long a1)
Definition: Native.java:3626
static long optimizeGetStatistics(long a0, long a1)
Definition: Native.java:3722
static String optimizeGetReasonUnknown(long a0, long a1)
Definition: Native.java:3651
static long optimizeGetModel(long a0, long a1)
Definition: Native.java:3660
static void optimizeAssert(long a0, long a1, long a2)
Definition: Native.java:3591
static int optimizeMinimize(long a0, long a1, long a2)
Definition: Native.java:3617
static String optimizeGetHelp(long a0, long a1)
Definition: Native.java:3713
static String optimizeToString(long a0, long a1)
Definition: Native.java:3704
ParamDescrs getParameterDescriptions()
Definition: Optimize.java:51
static int optimizeMaximize(long a0, long a1, long a2)
Definition: Native.java:3608
Handle MkMaximize(ArithExpr e)
Definition: Optimize.java:197
String toString()
Definition: Expr.java:209
Statistics getStatistics()
Definition: Optimize.java:249
static long optimizeGetLower(long a0, long a1, int a2)
Definition: Native.java:3686
Handle AssertSoft(BoolExpr constraint, int weight, String group)
Definition: Optimize.java:129
static long optimizeGetParamDescrs(long a0, long a1)
Definition: Native.java:3677
void setParameters(Params value)
Definition: Optimize.java:43
void Assert(BoolExpr...constraints)
Definition: Optimize.java:59
Handle MkMinimize(ArithExpr e)
Definition: Optimize.java:206
static int optimizeCheck(long a0, long a1)
Definition: Native.java:3642
static long mkOptimize(long a0)
Definition: Native.java:3566
static final Z3_lbool fromInt(int v)
Definition: Z3_lbool.java:21