20 package com.microsoft.z3;
61 getContext().checkContextMatch(constraints);
94 return opt.GetLower(handle);
102 return opt.GetUpper(handle);
131 getContext().checkContextMatch(constraint);
132 Symbol s = getContext().mkSymbol(group);
133 return new Handle(
this,
Native.
optimizeAssertSoft(getContext().nCtx(), getNativeObject(), constraint.getNativeObject(), Integer.toString(weight), s.getNativeObject()));
189 return new Model(getContext(), x);
268 getContext().getOptimizeDRQ().incAndClear(getContext(), o);
274 getContext().getOptimizeDRQ().add(o);
static long optimizeGetUpper(long a0, long a1, int a2)
void Add(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)
Handle AssertSoft(BoolExpr constraint, int weight, String group)
static long optimizeGetParamDescrs(long a0, long a1)
void setParameters(Params value)
void Assert(BoolExpr...constraints)
Handle MkMinimize(ArithExpr e)
static int optimizeCheck(long a0, long a1)
static long mkOptimize(long a0)
static final Z3_lbool fromInt(int v)
String getReasonUnknown()