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
27public 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
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
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}
BoolExpr[] ToBoolExprArray()
Definition: ASTVector.java:140
IDecRefQueue< Optimize > getOptimizeDRQ()
Definition: Context.java:4103
IntSymbol mkSymbol(int i)
Definition: Context.java:93
void storeReference(Context ctx, T obj)
static int optimizeMinimize(long a0, long a1, long a2)
Definition: Native.java:5737
static int optimizeAssertSoft(long a0, long a1, long a2, String a3, long a4)
Definition: Native.java:5719
static void optimizeSetParams(long a0, long a1, long a2)
Definition: Native.java:5798
static long optimizeGetUnsatCore(long a0, long a1)
Definition: Native.java:5789
static void optimizeFromString(long a0, long a1, String a2)
Definition: Native.java:5860
static long optimizeGetLower(long a0, long a1, int a2)
Definition: Native.java:5815
static void optimizeAssert(long a0, long a1, long a2)
Definition: Native.java:5703
static String optimizeGetHelp(long a0, long a1)
Definition: Native.java:5876
static void optimizePush(long a0, long a1)
Definition: Native.java:5746
static void optimizePop(long a0, long a1)
Definition: Native.java:5754
static String optimizeGetReasonUnknown(long a0, long a1)
Definition: Native.java:5771
static long optimizeGetStatistics(long a0, long a1)
Definition: Native.java:5885
static long optimizeGetAssertions(long a0, long a1)
Definition: Native.java:5894
static long optimizeGetObjectives(long a0, long a1)
Definition: Native.java:5903
static int optimizeMaximize(long a0, long a1, long a2)
Definition: Native.java:5728
static long optimizeGetModel(long a0, long a1)
Definition: Native.java:5780
static long optimizeGetParamDescrs(long a0, long a1)
Definition: Native.java:5806
static String optimizeToString(long a0, long a1)
Definition: Native.java:5851
static int optimizeCheck(long a0, long a1, int a2, long[] a3)
Definition: Native.java:5762
static void optimizeFromFile(long a0, long a1, String a2)
Definition: Native.java:5868
ParamDescrs getParameterDescriptions()
Definition: Optimize.java:50
Handle AssertSoft(BoolExpr constraint, int weight, String group)
Definition: Optimize.java:152
void fromString(String s)
Definition: Optimize.java:341
Handle MkMaximize(Expr e)
Definition: Optimize.java:246
void Add(BoolExpr ... constraints)
Definition: Optimize.java:70
void setParameters(Params value)
Definition: Optimize.java:42
BoolExpr[] getUnsatCore()
Definition: Optimize.java:235
Status Check(Expr... assumptions)
Definition: Optimize.java:164
Handle MkMinimize(Expr e)
Definition: Optimize.java:255
void Assert(BoolExpr ... constraints)
Definition: Optimize.java:58
BoolExpr[] getAssertions()
Definition: Optimize.java:349
void fromFile(String file)
Definition: Optimize.java:333
Statistics getStatistics()
Definition: Optimize.java:367
static final Z3_lbool fromInt(int v)
Definition: Z3_lbool.java:34
def String(name, ctx=None)
Definition: z3py.py:10085
def Model(ctx=None)
Definition: z3py.py:6236
@ Z3_L_TRUE
Definition: z3_api.h:103
@ Z3_L_FALSE
Definition: z3_api.h:101