19package com.microsoft.z3;
21import com.microsoft.z3.enumerations.Z3_lbool;
27@SuppressWarnings(
"unchecked")
35 return Native.optimizeGetHelp(getContext().nCtx(), getNativeObject());
45 Native.optimizeSetParams(getContext().nCtx(), getNativeObject(), value.getNativeObject());
53 return new ParamDescrs(getContext(), Native.optimizeGetParamDescrs(getContext().nCtx(), getNativeObject()));
61 getContext().checkContextMatch(constraints);
64 Native.optimizeAssert(getContext().nCtx(), getNativeObject(), a.getNativeObject());
91 getContext().checkContextMatch(constraint);
92 getContext().checkContextMatch(p);
94 Native.optimizeAssertAndTrack(getContext().nCtx(), getNativeObject(),
95 constraint.getNativeObject(), p.getNativeObject());
101 public static class Handle<R
extends Sort> {
104 private final int handle;
115 public Expr<R> getLower()
117 return opt.GetLower(handle);
123 public Expr<R> getUpper()
125 return opt.GetUpper(handle);
136 public Expr<?>[] getUpperAsVector()
138 return opt.GetUpperAsVector(handle);
146 public Expr<?>[] getLowerAsVector()
148 return opt.GetLowerAsVector(handle);
154 public Expr<R> getValue()
165 return getValue().toString();
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()));
190 if (assumptions ==
null) {
192 Native.optimizeCheck(
194 getNativeObject(), 0,
null));
198 Native.optimizeCheck(
219 Native.optimizePush(getContext().nCtx(), getNativeObject());
229 Native.optimizePop(getContext().nCtx(), getNativeObject());
241 long x = Native.optimizeGetModel(getContext().nCtx(), getNativeObject());
245 return new Model(getContext(), x);
260 ASTVector core =
new ASTVector(getContext(), Native.optimizeGetUnsatCore(getContext().nCtx(), getNativeObject()));
269 public <R extends Sort> Handle<R> MkMaximize(
Expr<R> e)
271 return new Handle<>(
this, Native.optimizeMaximize(getContext().nCtx(), getNativeObject(), e.getNativeObject()));
278 public <R extends Sort> Handle<R> MkMinimize(Expr<R> e)
280 return new Handle<>(
this, Native.optimizeMinimize(getContext().nCtx(), getNativeObject(), e.getNativeObject()));
286 private <R extends Sort> Expr<R> GetLower(
int index)
288 return (Expr<R>) Expr.create(getContext(), Native.optimizeGetLower(getContext().nCtx(), getNativeObject(), index));
294 private <R extends Sort> Expr<R> GetUpper(
int index)
296 return (Expr<R>) Expr.create(getContext(), Native.optimizeGetUpper(getContext().nCtx(), getNativeObject(), index));
304 private Expr<?>[] GetUpperAsVector(
int index) {
305 return unpackObjectiveValueVector(
306 Native.optimizeGetUpperAsVector(
307 getContext().nCtx(), getNativeObject(), index
317 private Expr<?>[] GetLowerAsVector(
int index) {
318 return unpackObjectiveValueVector(
319 Native.optimizeGetLowerAsVector(
320 getContext().nCtx(), getNativeObject(), index
325 private Expr<?>[] unpackObjectiveValueVector(
long nativeVec) {
326 ASTVector vec =
new ASTVector(
327 getContext(), nativeVec
330 (Expr<?>) vec.get(0), (Expr<?>) vec.get(1), (Expr<?>) vec.get(2)
340 return Native.optimizeGetReasonUnknown(getContext().nCtx(), getNativeObject());
349 return Native.optimizeToString(getContext().nCtx(), getNativeObject());
358 Native.optimizeFromFile(getContext().nCtx(), getNativeObject(), file);
366 Native.optimizeFromString(getContext().nCtx(), getNativeObject(), s);
374 ASTVector assertions =
new ASTVector(getContext(), Native.optimizeGetAssertions(getContext().nCtx(), getNativeObject()));
383 ASTVector objectives =
new ASTVector(getContext(), Native.optimizeGetObjectives(getContext().nCtx(), getNativeObject()));
392 return new Statistics(getContext(), Native.optimizeGetStatistics(getContext().nCtx(), getNativeObject()));
401 Optimize(Context ctx)
throws Z3Exception
403 super(ctx, Native.mkOptimize(ctx.nCtx()));
408 Native.optimizeIncRef(getContext().nCtx(), getNativeObject());
412 void addToReferenceQueue() {
413 getContext().getOptimizeDRQ().storeReference(getContext(),
this);
BoolExpr[] ToBoolExprArray()
Status Check(Expr< BoolSort >... assumptions)
Expr<?>[] getObjectives()
void AssertAndTrack(Expr< BoolSort > constraint, Expr< BoolSort > p)
ParamDescrs getParameterDescriptions()
void fromString(String s)
void setParameters(Params value)
BoolExpr[] getUnsatCore()
Handle<?> AssertSoft(Expr< BoolSort > constraint, int weight, String group)
void Assert(Expr< BoolSort > ... constraints)
BoolExpr[] getAssertions()
void Add(Expr< BoolSort > ... constraints)
void fromFile(String file)
String getReasonUnknown()
Statistics getStatistics()
static long[] arrayToNative(Z3Object[] a)
def String(name, ctx=None)
Z3_lbool
Lifted Boolean type: false, undefined, true.