19package com.microsoft.z3;
21import com.microsoft.z3.enumerations.Z3_lbool;
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));
179 AST.arrayToNative(assumptions)));
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() {
BoolExpr[] ToBoolExprArray()
IDecRefQueue< Optimize > getOptimizeDRQ()
IntSymbol mkSymbol(int i)
void storeReference(Context ctx, T obj)
static int optimizeMinimize(long a0, long a1, long a2)
static int optimizeAssertSoft(long a0, long a1, long a2, String a3, long a4)
static void optimizeSetParams(long a0, long a1, long a2)
static long optimizeGetUnsatCore(long a0, long a1)
static void optimizeFromString(long a0, long a1, String a2)
static long optimizeGetLower(long a0, long a1, int a2)
static void optimizeAssert(long a0, long a1, long a2)
static String optimizeGetHelp(long a0, long a1)
static void optimizePush(long a0, long a1)
static void optimizePop(long a0, long a1)
static String optimizeGetReasonUnknown(long a0, long a1)
static long optimizeGetStatistics(long a0, long a1)
static long optimizeGetAssertions(long a0, long a1)
static long optimizeGetObjectives(long a0, long a1)
static int optimizeMaximize(long a0, long a1, long a2)
static long optimizeGetModel(long a0, long a1)
static long optimizeGetParamDescrs(long a0, long a1)
static String optimizeToString(long a0, long a1)
static int optimizeCheck(long a0, long a1, int a2, long[] a3)
static void optimizeFromFile(long a0, long a1, String a2)
ParamDescrs getParameterDescriptions()
Handle AssertSoft(BoolExpr constraint, int weight, String group)
void fromString(String s)
Handle MkMaximize(Expr e)
void Add(BoolExpr ... constraints)
void setParameters(Params value)
BoolExpr[] getUnsatCore()
Status Check(Expr... assumptions)
Handle MkMinimize(Expr e)
void Assert(BoolExpr ... constraints)
BoolExpr[] getAssertions()
void fromFile(String file)
String getReasonUnknown()
Statistics getStatistics()
static final Z3_lbool fromInt(int v)
def String(name, ctx=None)