Z3 |

Optimize.java
Go to the documentation of this file.
1
19 package com.microsoft.z3;
20
21 import 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
51 public ParamDescrs getParameterDescriptions()
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
239 public Model getModel()
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
258 public BoolExpr[] getUnsatCore()
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
338 public String getReasonUnknown()
339 {
340 return Native.optimizeGetReasonUnknown(getContext().nCtx(), getNativeObject());
341 }
342
346 @Override
347 public String toString()
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
372 public BoolExpr[] getAssertions()
373 {
374 ASTVector assertions = new ASTVector(getContext(), Native.optimizeGetAssertions(getContext().nCtx(), getNativeObject()));
375 return assertions.ToBoolExprArray();
376 }
377
381 public Expr<?>[] getObjectives()
382 {
383 ASTVector objectives = new ASTVector(getContext(), Native.optimizeGetObjectives(getContext().nCtx(), getNativeObject()));
384 return objectives.ToExprArray();
385 }
386
390 public Statistics getStatistics()
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}
com.microsoft.z3.AST
Definition: AST.java:26
com.microsoft.z3.ASTVector
Definition: ASTVector.java:23
com.microsoft.z3.ASTVector.ToBoolExprArray
BoolExpr[] ToBoolExprArray()
Definition: ASTVector.java:140
com.microsoft.z3.ASTVector.ToExprArray
Expr<?>[] ToExprArray()
Definition: ASTVector.java:129
com.microsoft.z3.BoolExpr
Definition: BoolExpr.java:23
com.microsoft.z3.Context
Definition: Context.java:36
com.microsoft.z3.Expr< BoolSort >
com.microsoft.z3.Expr.toString
String toString()
Definition: Expr.java:208
com.microsoft.z3.Model
Definition: Model.java:26
com.microsoft.z3.Optimize
Definition: Optimize.java:28
com.microsoft.z3.Optimize.Check
Status Check(Expr< BoolSort >... assumptions)
Definition: Optimize.java:187
com.microsoft.z3.Optimize.getObjectives
Expr<?>[] getObjectives()
Definition: Optimize.java:381
com.microsoft.z3.Optimize.AssertAndTrack
void AssertAndTrack(Expr< BoolSort > constraint, Expr< BoolSort > p)
Definition: Optimize.java:89
com.microsoft.z3.Optimize.getParameterDescriptions
ParamDescrs getParameterDescriptions()
Definition: Optimize.java:51
com.microsoft.z3.Optimize.fromString
void fromString(String s)
Definition: Optimize.java:364
com.microsoft.z3.Optimize.Push
void Push()
Definition: Optimize.java:217
com.microsoft.z3.Optimize.setParameters
void setParameters(Params value)
Definition: Optimize.java:43
com.microsoft.z3.Optimize.getUnsatCore
BoolExpr[] getUnsatCore()
Definition: Optimize.java:258
com.microsoft.z3.Optimize.AssertSoft
Handle<?> AssertSoft(Expr< BoolSort > constraint, int weight, String group)
Definition: Optimize.java:175
com.microsoft.z3.Optimize.Pop
void Pop()
Definition: Optimize.java:227
com.microsoft.z3.Optimize.getHelp
String getHelp()
Definition: Optimize.java:33
com.microsoft.z3.Optimize.getModel
Model getModel()
Definition: Optimize.java:239
com.microsoft.z3.Optimize.Assert
void Assert(Expr< BoolSort > ... constraints)
Definition: Optimize.java:59
com.microsoft.z3.Optimize.getAssertions
BoolExpr[] getAssertions()
Definition: Optimize.java:372
com.microsoft.z3.Optimize.Add
void Add(Expr< BoolSort > ... constraints)
Definition: Optimize.java:71
com.microsoft.z3.Optimize.toString
String toString()
Definition: Optimize.java:347
com.microsoft.z3.Optimize.fromFile
void fromFile(String file)
Definition: Optimize.java:356
com.microsoft.z3.Optimize.getReasonUnknown
String getReasonUnknown()
Definition: Optimize.java:338
com.microsoft.z3.Optimize.getStatistics
Statistics getStatistics()
Definition: Optimize.java:390
com.microsoft.z3.ParamDescrs
Definition: ParamDescrs.java:25
com.microsoft.z3.Params
Definition: Params.java:24
com.microsoft.z3.Sort
Definition: Sort.java:27
com.microsoft.z3.Statistics
Definition: Statistics.java:23
com.microsoft.z3.Symbol
Definition: Symbol.java:25
com.microsoft.z3.Z3Exception
Definition: Z3Exception.java:26
com.microsoft.z3.Z3Object
Definition: Z3Object.java:24
com.microsoft.z3.Z3Object.arrayToNative
static long[] arrayToNative(Z3Object[] a)
Definition: Z3Object.java:73
com.microsoft.z3.Status
Definition: Status.java:24
com.microsoft.z3.Status.SATISFIABLE
SATISFIABLE
Definition: Status.java:32
com.microsoft.z3.Status.UNSATISFIABLE
UNSATISFIABLE
Definition: Status.java:26
com.microsoft.z3.Status.UNKNOWN
UNKNOWN
Definition: Status.java:29
z3py.String
def String(name, ctx=None)
Definition: z3py.py:10693
z3py.Model
def Model(ctx=None)
Definition: z3py.py:6579
Z3_lbool
Z3_lbool
Lifted Boolean type: false, undefined, true.
Definition: z3_api.h:102
Z3_L_TRUE
@ Z3_L_TRUE
Definition: z3_api.h:105
Z3_L_FALSE
@ Z3_L_FALSE
Definition: z3_api.h:103