20 package com.microsoft.z3;
61 getContext().checkContextMatch(constraints);
94 return opt.GetLower(handle);
102 return opt.GetUpper(handle);
132 getContext().checkContextMatch(constraint);
133 Symbol s = getContext().mkSymbol(group);
134 return new Handle(
this,
Native.
optimizeAssertSoft(getContext().nCtx(), getNativeObject(), constraint.getNativeObject(), Integer.toString(weight), s.getNativeObject()));
190 return new Model(getContext(), x);
274 void addToReferenceQueue() {
275 getContext().getOptimizeDRQ().storeReference(getContext(),
this);
static long optimizeGetUpper(long a0, long a1, int a2)
void Assert(BoolExpr ... constraints)
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 String optimizeGetHelp(long a0, long a1)
static String optimizeToString(long a0, long a1)
ParamDescrs getParameterDescriptions()
static int optimizeMaximize(long a0, long a1, long a2)
Handle MkMaximize(ArithExpr e)
Statistics getStatistics()
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)
void setParameters(Params value)
Handle MkMinimize(ArithExpr e)
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()