21 using System.Collections.Generic;
39 Contract.Ensures(Contract.Result<
string>() != null);
40 return Native.Z3_optimize_get_help(
Context.nCtx, NativeObject);
51 Contract.Requires(value != null);
52 Context.CheckContextMatch(value);
53 Native.Z3_optimize_set_params(
Context.nCtx, NativeObject, value.NativeObject);
70 AddConstraints(constraints);
76 public void Assert(IEnumerable<BoolExpr> constraints)
78 AddConstraints(constraints);
86 AddConstraints(constraints);
92 public void Add(IEnumerable<BoolExpr> constraints)
94 AddConstraints(constraints);
100 private void AddConstraints(IEnumerable<BoolExpr> constraints)
102 Contract.Requires(constraints != null);
103 Contract.Requires(Contract.ForAll(constraints, c => c != null));
105 Context.CheckContextMatch(constraints);
108 Native.Z3_optimize_assert(
Context.nCtx, NativeObject, a.NativeObject);
129 get {
return opt.GetLower(handle); }
137 get {
return opt.GetUpper(handle); }
145 get {
return Lower; }
157 Context.CheckContextMatch(constraint);
159 return new Handle(
this, Native.Z3_optimize_assert_soft(
Context.nCtx, NativeObject, constraint.NativeObject, weight.ToString(), s.NativeObject));
175 return Status.SATISFIABLE;
177 return Status.UNSATISFIABLE;
189 Native.Z3_optimize_push(
Context.nCtx, NativeObject);
199 Native.Z3_optimize_pop(
Context.nCtx, NativeObject);
214 IntPtr x = Native.Z3_optimize_get_model(
Context.nCtx, NativeObject);
215 if (x == IntPtr.Zero)
229 return new Handle(
this, Native.Z3_optimize_maximize(
Context.nCtx, NativeObject, e.NativeObject));
238 return new Handle(
this, Native.Z3_optimize_minimize(
Context.nCtx, NativeObject, e.NativeObject));
261 public String ReasonUnknown
265 Contract.Ensures(Contract.Result<
string>() != null);
266 return Native.Z3_optimize_get_reason_unknown(
Context.nCtx, NativeObject);
276 return Native.Z3_optimize_to_string(
Context.nCtx, NativeObject);
285 Native.Z3_optimize_from_file(
Context.nCtx, NativeObject, file);
293 Native.Z3_optimize_from_string(
Context.nCtx, NativeObject, s);
303 Contract.Ensures(Contract.Result<
BoolExpr[]>() != null);
313 public Expr[] Objectives
317 Contract.Ensures(Contract.Result<
Expr[]>() != null);
332 Contract.Ensures(Contract.Result<
Statistics>() != null);
343 Contract.Requires(ctx != null);
346 : base(ctx, Native.Z3_mk_optimize(ctx.nCtx))
348 Contract.Requires(ctx != null);
353 public DecRefQueue() : base() { }
354 public DecRefQueue(uint move_limit) : base(move_limit) { }
355 internal override void IncRef(
Context ctx, IntPtr obj)
357 Native.Z3_optimize_inc_ref(ctx.nCtx, obj);
360 internal override void DecRef(
Context ctx, IntPtr obj)
362 Native.Z3_optimize_dec_ref(ctx.nCtx, obj);
366 internal override void IncRef(IntPtr o)
372 internal override void DecRef(IntPtr o)
override string ToString()
Print the context to a string (SMT-LIB parseable benchmark).
Object for managing optimizization context
IDecRefQueue Optimize_DRQ
Optimize DRQ
void Push()
Creates a backtracking point.
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.
void Assert(IEnumerable< BoolExpr > constraints)
Assert a constraint (or multiple) into the optimize solver.
void Add(IEnumerable< BoolExpr > constraints)
Alias for Assert.
Handle to objectives returned by objective functions.
void FromFile(string file)
Parse an SMT-LIB2 file with optimization objectives and constraints. The parsed constraints and objec...
void Assert(params BoolExpr[] constraints)
Assert a constraint (or multiple) into the optimize solver.
Z3_lbool
Lifted Boolean type: false, undefined, true.
BoolExpr [] ToBoolExprArray()
Translates an ASTVector into a BoolExpr[]
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.
A Model contains interpretations (assignments) of constants and functions.
IntSymbol MkSymbol(int i)
Creates a new symbol using an integer.
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)
Expr [] ToExprArray()
Translates an ASTVector into an Expr[]
void Add(params BoolExpr[] constraints)
Alias for Assert.
Internal base class for interfacing with native Z3 objects. Should not be used externally.
Symbols are used to name several term and type constructors.
def String(name, ctx=None)
void FromString(string s)
Similar to FromFile. Instead it takes as argument a string.