19 package com.microsoft.z3;
60 getContext().checkContextMatch(constraints);
78 public static class Handle {
81 private final int handle;
92 public Expr getLower()
94 return opt.GetLower(handle);
100 public Expr getUpper()
102 return opt.GetUpper(handle);
113 public Expr[] getUpperAsVector()
115 return opt.GetUpperAsVector(handle);
123 public Expr[] getLowerAsVector()
125 return opt.GetLowerAsVector(handle);
131 public Expr getValue()
142 return getValue().toString();
154 getContext().checkContextMatch(constraint);
156 return new Handle(
this,
Native.
optimizeAssertSoft(getContext().nCtx(), getNativeObject(), constraint.getNativeObject(), Integer.toString(weight), s.getNativeObject()));
167 if (assumptions ==
null) {
171 getNativeObject(), 0,
null));
222 return new Model(getContext(), x);
248 return new Handle(
this,
Native.
optimizeMaximize(getContext().nCtx(), getNativeObject(), e.getNativeObject()));
257 return new Handle(
this,
Native.
optimizeMinimize(getContext().nCtx(), getNativeObject(), e.getNativeObject()));
263 private Expr GetLower(
int index)
271 private Expr GetUpper(
int index)
273 return Expr.create(getContext(), Native.optimizeGetUpper(getContext().nCtx(), getNativeObject(), index));
281 private Expr[] GetUpperAsVector(
int index) {
282 return unpackObjectiveValueVector(
283 Native.optimizeGetUpperAsVector(
284 getContext().nCtx(), getNativeObject(), index
294 private Expr[] GetLowerAsVector(
int index) {
295 return unpackObjectiveValueVector(
296 Native.optimizeGetLowerAsVector(
297 getContext().nCtx(), getNativeObject(), index
302 private Expr[] unpackObjectiveValueVector(
long nativeVec) {
303 ASTVector vec =
new ASTVector(
304 getContext(), nativeVec
307 (Expr) vec.get(0), (Expr) vec.get(1), (Expr) vec.get(2)
378 Optimize(Context ctx)
throws Z3Exception
380 super(ctx, Native.mkOptimize(ctx.nCtx()));
385 Native.optimizeIncRef(getContext().nCtx(), getNativeObject());
389 void addToReferenceQueue() {