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);
155 Symbol s = getContext().mkSymbol(group);
156 return new Handle(
this,
Native.
optimizeAssertSoft(getContext().nCtx(), getNativeObject(), constraint.getNativeObject(), Integer.toString(weight), s.getNativeObject()));
208 return new Model(getContext(), x);
219 return new Handle(
this,
Native.
optimizeMaximize(getContext().nCtx(), getNativeObject(), e.getNativeObject()));
228 return new Handle(
this,
Native.
optimizeMinimize(getContext().nCtx(), getNativeObject(), e.getNativeObject()));
234 private Expr GetLower(
int index)
242 private Expr GetUpper(
int index)
252 private Expr[] GetUpperAsVector(
int index) {
253 return unpackObjectiveValueVector(
255 getContext().nCtx(), getNativeObject(), index
265 private Expr[] GetLowerAsVector(
int index) {
266 return unpackObjectiveValueVector(
268 getContext().nCtx(), getNativeObject(), index
273 private Expr[] unpackObjectiveValueVector(
long nativeVec) {
275 getContext(), nativeVec
343 void addToReferenceQueue() {
344 getContext().getOptimizeDRQ().storeReference(getContext(),
this);
static long optimizeGetUpper(long a0, long a1, int a2)
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 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)
static long optimizeGetLowerAsVector(long a0, long a1, int a2)
static String optimizeGetHelp(long a0, long a1)
void fromString(String s)
static String optimizeToString(long a0, long a1)
ParamDescrs getParameterDescriptions()
static int optimizeMaximize(long a0, long a1, long a2)
static long optimizeGetUpperAsVector(long a0, long a1, int a2)
Handle MkMaximize(Expr e)
Statistics getStatistics()
Handle MkMinimize(Expr e)
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)
void setParameters(Params value)
static void optimizeFromFile(long a0, long a1, String a2)
static int optimizeCheck(long a0, long a1)
static void optimizeIncRef(long a0, long a1)
static long mkOptimize(long a0)
def String(name, ctx=None)
static final Z3_lbool fromInt(int v)
String getReasonUnknown()