Z3
Optimize.java
Go to the documentation of this file.
1
19package com.microsoft.z3;
20
21import com.microsoft.z3.enumerations.Z3_lbool;
22
23
27@SuppressWarnings("unchecked")
28public 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(Expr<BoolSort> ... constraints)
60 {
61 getContext().checkContextMatch(constraints);
62 for (Expr<BoolSort> a : constraints)
63 {
64 Native.optimizeAssert(getContext().nCtx(), getNativeObject(), a.getNativeObject());
65 }
66 }
67
71 public void Add(Expr<BoolSort> ... constraints)
72 {
73 Assert(constraints);
74 }
75
89 public void AssertAndTrack(Expr<BoolSort> constraint, Expr<BoolSort> p)
90 {
91 getContext().checkContextMatch(constraint);
92 getContext().checkContextMatch(p);
93
94 Native.optimizeAssertAndTrack(getContext().nCtx(), getNativeObject(),
95 constraint.getNativeObject(), p.getNativeObject());
96 }
97
101 public static class Handle<R extends Sort> {
102
103 private final Optimize opt;
104 private final int handle;
105
106 Handle(Optimize opt, int h)
107 {
108 this.opt = opt;
109 this.handle = h;
110 }
111
115 public Expr<R> getLower()
116 {
117 return opt.GetLower(handle);
118 }
119
123 public Expr<R> getUpper()
124 {
125 return opt.GetUpper(handle);
126 }
127
136 public Expr<?>[] getUpperAsVector()
137 {
138 return opt.GetUpperAsVector(handle);
139 }
140
146 public Expr<?>[] getLowerAsVector()
147 {
148 return opt.GetLowerAsVector(handle);
149 }
150
154 public Expr<R> getValue()
155 {
156 return getLower();
157 }
158
162 @Override
163 public String toString()
164 {
165 return getValue().toString();
166 }
167 }
168
175 public Handle<?> AssertSoft(Expr<BoolSort> constraint, int weight, String group)
176 {
177 getContext().checkContextMatch(constraint);
178 Symbol s = getContext().mkSymbol(group);
179 return new Handle<>(this, Native.optimizeAssertSoft(getContext().nCtx(), getNativeObject(), constraint.getNativeObject(), Integer.toString(weight), s.getNativeObject()));
180 }
181
187 public Status Check(Expr<BoolSort>... assumptions)
188 {
189 Z3_lbool r;
190 if (assumptions == null) {
191 r = Z3_lbool.fromInt(
192 Native.optimizeCheck(
193 getContext().nCtx(),
194 getNativeObject(), 0, null));
195 }
196 else {
197 r = Z3_lbool.fromInt(
198 Native.optimizeCheck(
199 getContext().nCtx(),
200 getNativeObject(),
201 assumptions.length,
202 AST.arrayToNative(assumptions)));
203 }
204 switch (r) {
205 case Z3_L_TRUE:
206 return Status.SATISFIABLE;
207 case Z3_L_FALSE:
208 return Status.UNSATISFIABLE;
209 default:
210 return Status.UNKNOWN;
211 }
212 }
213
217 public void Push()
218 {
219 Native.optimizePush(getContext().nCtx(), getNativeObject());
220 }
221
227 public void Pop()
228 {
229 Native.optimizePop(getContext().nCtx(), getNativeObject());
230 }
231
232
240 {
241 long x = Native.optimizeGetModel(getContext().nCtx(), getNativeObject());
242 if (x == 0) {
243 return null;
244 } else {
245 return new Model(getContext(), x);
246 }
247 }
248
259 {
260 ASTVector core = new ASTVector(getContext(), Native.optimizeGetUnsatCore(getContext().nCtx(), getNativeObject()));
261 return core.ToBoolExprArray();
262 }
263
269 public <R extends Sort> Handle<R> MkMaximize(Expr<R> e)
270 {
271 return new Handle<>(this, Native.optimizeMaximize(getContext().nCtx(), getNativeObject(), e.getNativeObject()));
272 }
273
278 public <R extends Sort> Handle<R> MkMinimize(Expr<R> e)
279 {
280 return new Handle<>(this, Native.optimizeMinimize(getContext().nCtx(), getNativeObject(), e.getNativeObject()));
281 }
282
286 private <R extends Sort> Expr<R> GetLower(int index)
287 {
288 return (Expr<R>) Expr.create(getContext(), Native.optimizeGetLower(getContext().nCtx(), getNativeObject(), index));
289 }
290
294 private <R extends Sort> Expr<R> GetUpper(int index)
295 {
296 return (Expr<R>) Expr.create(getContext(), Native.optimizeGetUpper(getContext().nCtx(), getNativeObject(), index));
297 }
298
304 private Expr<?>[] GetUpperAsVector(int index) {
305 return unpackObjectiveValueVector(
306 Native.optimizeGetUpperAsVector(
307 getContext().nCtx(), getNativeObject(), index
308 )
309 );
310 }
311
317 private Expr<?>[] GetLowerAsVector(int index) {
318 return unpackObjectiveValueVector(
319 Native.optimizeGetLowerAsVector(
320 getContext().nCtx(), getNativeObject(), index
321 )
322 );
323 }
324
325 private Expr<?>[] unpackObjectiveValueVector(long nativeVec) {
326 ASTVector vec = new ASTVector(
327 getContext(), nativeVec
328 );
329 return new Expr[] {
330 (Expr<?>) vec.get(0), (Expr<?>) vec.get(1), (Expr<?>) vec.get(2)
331 };
332
333 }
334
339 {
340 return Native.optimizeGetReasonUnknown(getContext().nCtx(), getNativeObject());
341 }
342
346 @Override
348 {
349 return Native.optimizeToString(getContext().nCtx(), getNativeObject());
350 }
351
356 public void fromFile(String file)
357 {
358 Native.optimizeFromFile(getContext().nCtx(), getNativeObject(), file);
359 }
360
364 public void fromString(String s)
365 {
366 Native.optimizeFromString(getContext().nCtx(), getNativeObject(), s);
367 }
368
373 {
374 ASTVector assertions = new ASTVector(getContext(), Native.optimizeGetAssertions(getContext().nCtx(), getNativeObject()));
375 return assertions.ToBoolExprArray();
376 }
377
382 {
383 ASTVector objectives = new ASTVector(getContext(), Native.optimizeGetObjectives(getContext().nCtx(), getNativeObject()));
384 return objectives.ToExprArray();
385 }
386
391 {
392 return new Statistics(getContext(), Native.optimizeGetStatistics(getContext().nCtx(), getNativeObject()));
393 }
394
395
396 Optimize(Context ctx, long obj) throws Z3Exception
397 {
398 super(ctx, obj);
399 }
400
401 Optimize(Context ctx) throws Z3Exception
402 {
403 super(ctx, Native.mkOptimize(ctx.nCtx()));
404 }
405
406 @Override
407 void incRef() {
408 Native.optimizeIncRef(getContext().nCtx(), getNativeObject());
409 }
410
411 @Override
412 void addToReferenceQueue() {
413 getContext().getOptimizeDRQ().storeReference(getContext(), this);
414 }
415}
BoolExpr[] ToBoolExprArray()
Definition: ASTVector.java:140
String toString()
Definition: Expr.java:208
Status Check(Expr< BoolSort >... assumptions)
Definition: Optimize.java:187
void AssertAndTrack(Expr< BoolSort > constraint, Expr< BoolSort > p)
Definition: Optimize.java:89
ParamDescrs getParameterDescriptions()
Definition: Optimize.java:51
void fromString(String s)
Definition: Optimize.java:364
void setParameters(Params value)
Definition: Optimize.java:43
BoolExpr[] getUnsatCore()
Definition: Optimize.java:258
Handle<?> AssertSoft(Expr< BoolSort > constraint, int weight, String group)
Definition: Optimize.java:175
void Assert(Expr< BoolSort > ... constraints)
Definition: Optimize.java:59
BoolExpr[] getAssertions()
Definition: Optimize.java:372
void Add(Expr< BoolSort > ... constraints)
Definition: Optimize.java:71
void fromFile(String file)
Definition: Optimize.java:356
Statistics getStatistics()
Definition: Optimize.java:390
static long[] arrayToNative(Z3Object[] a)
Definition: Z3Object.java:73
def String(name, ctx=None)
Definition: z3py.py:10693
def Model(ctx=None)
Definition: z3py.py:6579
Z3_lbool
Lifted Boolean type: false, undefined, true.
Definition: z3_api.h:102
@ Z3_L_TRUE
Definition: z3_api.h:105
@ Z3_L_FALSE
Definition: z3_api.h:103