21 using System.Collections.Generic;
22 using System.Diagnostics.Contracts;
29 [ContractVerification(
true)]
39 Contract.Ensures(Contract.Result<
string>() != null);
51 Contract.Requires(value != null);
52 Context.CheckContextMatch(value);
70 Contract.Requires(constraints != null);
71 Contract.Requires(Contract.ForAll(constraints, c => c != null));
73 Context.CheckContextMatch(constraints);
106 get {
return opt.GetLower(handle); }
114 get {
return opt.GetUpper(handle); }
122 get {
return Lower; }
134 Context.CheckContextMatch(constraint);
152 return Status.SATISFIABLE;
154 return Status.UNSATISFIABLE;
192 if (x == IntPtr.Zero)
240 Contract.Ensures(Contract.Result<
string>() != null);
260 Contract.Ensures(Contract.Result<
Statistics>() != null);
271 Contract.Requires(ctx != null);
276 Contract.Requires(ctx != null);
281 public DecRefQueue() : base() { }
282 public DecRefQueue(uint move_limit) : base(move_limit) { }
283 internal override void IncRef(
Context ctx, IntPtr obj)
288 internal override void DecRef(
Context ctx, IntPtr obj)
294 internal override void IncRef(IntPtr o)
300 internal override void DecRef(IntPtr o)
override string ToString()
Print the context to a string (SMT-LIB parseable benchmark).
Object for managing optimizization context
static void Z3_optimize_pop(Z3_context a0, Z3_optimize a1)
IDecRefQueue Optimize_DRQ
Optimize DRQ
static Z3_optimize Z3_mk_optimize(Z3_context a0)
void Push()
Creates a backtracking point.
static Z3_ast Z3_optimize_get_lower(Z3_context a0, Z3_optimize a1, uint a2)
Objects of this class track statistical information about solvers.
Handle MkMinimize(ArithExpr e)
Declare an arithmetical minimization objective. Similar to MkMaximize.
Handle MkMaximize(ArithExpr e)
Declare an arithmetical maximization objective. Return a handle to the objective. The handle is used ...
void Pop()
Backtrack one backtracking point.
String getReasonUnknown()
Return a string the describes why the last to check returned unknown
static void Z3_optimize_push(Z3_context a0, Z3_optimize a1)
Handle to objectives returned by objective functions.
static string Z3_optimize_to_string(Z3_context a0, Z3_optimize a1)
void Assert(params BoolExpr[] constraints)
Assert a constraint (or multiple) into the optimize solver.
Z3_lbool
Lifted Boolean type: false, undefined, true.
static uint Z3_optimize_assert_soft(Z3_context a0, Z3_optimize a1, Z3_ast a2, string a3, IntPtr a4)
static void Z3_optimize_inc_ref(Z3_context a0, Z3_optimize a1)
static Z3_model Z3_optimize_get_model(Z3_context a0, Z3_optimize a1)
Handle AssertSoft(BoolExpr constraint, uint weight, string group)
Assert soft constraint
A Params objects represents a configuration in the form of Symbol/value pairs.
A ParamDescrs describes a set of parameters.
static Z3_stats Z3_optimize_get_statistics(Z3_context a0, Z3_optimize a1)
A Model contains interpretations (assignments) of constants and functions.
static uint Z3_optimize_maximize(Z3_context a0, Z3_optimize a1, Z3_ast a2)
IntSymbol MkSymbol(int i)
Creates a new symbol using an integer.
static void Z3_optimize_dec_ref(Z3_context a0, Z3_optimize a1)
static string Z3_optimize_get_reason_unknown(Z3_context a0, Z3_optimize a1)
The main interaction with Z3 happens via the Context.
Status Check()
Check satisfiability of asserted constraints. Produce a model that (when the objectives are bounded a...
Arithmetic expressions (int/real)
static void Z3_optimize_set_params(Z3_context a0, Z3_optimize a1, Z3_params a2)
static Z3_param_descrs Z3_optimize_get_param_descrs(Z3_context a0, Z3_optimize a1)
void Add(params BoolExpr[] constraints)
Alias for Assert.
static string Z3_optimize_get_help(Z3_context a0, Z3_optimize a1)
Internal base class for interfacing with native Z3 objects. Should not be used externally.
Symbols are used to name several term and type constructors.
static void Z3_optimize_assert(Z3_context a0, Z3_optimize a1, Z3_ast a2)
static Z3_ast Z3_optimize_get_upper(Z3_context a0, Z3_optimize a1, uint a2)
static int Z3_optimize_check(Z3_context a0, Z3_optimize a1)
static uint Z3_optimize_minimize(Z3_context a0, Z3_optimize a1, Z3_ast a2)