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