21using System.Collections.Generic;
22using System.Diagnostics;
39 return Native.Z3_optimize_get_help(
Context.nCtx, NativeObject);
50 Debug.Assert(value !=
null);
51 Context.CheckContextMatch(value);
52 Native.Z3_optimize_set_params(
Context.nCtx, NativeObject, value.NativeObject);
110 AddConstraints(constraints);
116 public void Assert(IEnumerable<BoolExpr> constraints)
118 AddConstraints(constraints);
126 AddConstraints(constraints);
132 public void Add(IEnumerable<BoolExpr> constraints)
134 AddConstraints(constraints);
140 private void AddConstraints(IEnumerable<BoolExpr> constraints)
142 Debug.Assert(constraints !=
null);
143 Debug.Assert(constraints.All(c => c !=
null));
145 Context.CheckContextMatch(constraints);
148 Native.Z3_optimize_assert(
Context.nCtx, NativeObject, a.NativeObject);
169 get {
return opt.GetLower(handle); }
177 get {
return opt.GetUpper(handle); }
185 get {
return Lower; }
193 get {
return opt.GetLowerAsVector(handle); }
201 get {
return opt.GetUpperAsVector(handle); }
214 Context.CheckContextMatch(constraint);
216 return new Handle(
this, Native.Z3_optimize_assert_soft(
Context.nCtx, NativeObject, constraint.NativeObject, weight.ToString(), s.NativeObject));
228 Z3_lbool r = (
Z3_lbool)Native.Z3_optimize_check(
Context.nCtx, NativeObject, (uint)assumptions.Length,
AST.ArrayToNative(assumptions));
232 return Status.SATISFIABLE;
234 return Status.UNSATISFIABLE;
246 Native.Z3_optimize_push(
Context.nCtx, NativeObject);
256 Native.Z3_optimize_pop(
Context.nCtx, NativeObject);
271 IntPtr x = Native.Z3_optimize_get_model(
Context.nCtx, NativeObject);
272 if (x == IntPtr.Zero)
305 return new Handle(
this, Native.Z3_optimize_maximize(
Context.nCtx, NativeObject, e.NativeObject));
314 return new Handle(
this, Native.Z3_optimize_minimize(
Context.nCtx, NativeObject, e.NativeObject));
321 private Expr GetLower(uint index)
323 return Expr.Create(
Context, Native.Z3_optimize_get_lower(
Context.nCtx, NativeObject, index));
330 private Expr GetUpper(uint index)
332 return Expr.Create(Context, Native.Z3_optimize_get_upper(Context.nCtx, NativeObject, index));
338 private Expr[] GetLowerAsVector(uint index)
340 ASTVector v =
new ASTVector(Context, Native.Z3_optimize_get_lower_as_vector(Context.nCtx, NativeObject, index));
341 return v.ToExprArray();
348 private Expr[] GetUpperAsVector(uint index)
350 ASTVector v =
new ASTVector(Context, Native.Z3_optimize_get_upper_as_vector(Context.nCtx, NativeObject, index));
351 return v.ToExprArray();
361 return Native.Z3_optimize_get_reason_unknown(
Context.nCtx, NativeObject);
371 return Native.Z3_optimize_to_string(
Context.nCtx, NativeObject);
380 Native.Z3_optimize_from_file(
Context.nCtx, NativeObject, file);
388 Native.Z3_optimize_from_string(
Context.nCtx, NativeObject, s);
435 Debug.Assert(ctx !=
null);
437 internal Optimize(Context ctx)
440 Debug.Assert(ctx !=
null);
443 internal class DecRefQueue : IDecRefQueue
445 public DecRefQueue() : base() { }
446 public DecRefQueue(uint move_limit) : base(move_limit) { }
447 internal override void IncRef(Context ctx, IntPtr obj)
449 Native.Z3_optimize_inc_ref(ctx.nCtx, obj);
452 internal override void DecRef(Context ctx, IntPtr obj)
454 Native.Z3_optimize_dec_ref(ctx.nCtx, obj);
458 internal override void IncRef(IntPtr o)
464 internal override void DecRef(IntPtr o)
The abstract syntax tree (AST) class.
BoolExpr[] ToBoolExprArray()
Translates an ASTVector into a BoolExpr[]
Expr[] ToExprArray()
Translates an ASTVector into an Expr[]
The main interaction with Z3 happens via the Context.
IDecRefQueue Optimize_DRQ
Optimize DRQ
Params MkParams()
Creates a new ParameterSet.
IntSymbol MkSymbol(int i)
Creates a new symbol using an integer.
A Model contains interpretations (assignments) of constants and functions.
Handle to objectives returned by objective functions.
Expr[] UpperAsVector
Retrieve an upper bound for the objective handle.
Expr[] LowerAsVector
Retrieve a lower bound for the objective handle.
Expr Upper
Retrieve an upper bound for the objective handle.
Expr Value
Retrieve the value of an objective.
Expr Lower
Retrieve a lower bound for the objective handle.
Object for managing optimization context
void Set(string name, uint value)
Sets parameter on the optimize solver
BoolExpr[] Assertions
The set of asserted formulas.
void Set(string name, double value)
Sets parameter on the optimize solver
Model Model
The model of the last Check.
string Help
A string that describes all available optimize solver parameters.
void Set(string name, string value)
Sets parameter on the optimize solver
void Add(IEnumerable< BoolExpr > constraints)
Alias for Assert.
void Set(Symbol name, Symbol value)
Sets parameter on the optimize solver
void Push()
Creates a backtracking point.
Handle MkMaximize(Expr e)
Declare an arithmetical maximization objective. Return a handle to the objective. The handle is used ...
void Assert(params BoolExpr[] constraints)
Assert a constraint (or multiple) into the optimize solver.
void FromString(string s)
Similar to FromFile. Instead it takes as argument a string.
Params Parameters
Sets the optimize solver parameters.
Statistics Statistics
Optimize statistics.
void Pop()
Backtrack one backtracking point.
Handle MkMinimize(Expr e)
Declare an arithmetical minimization objective. Similar to MkMaximize.
void Set(Symbol name, string value)
Sets parameter on the optimize solver
ParamDescrs ParameterDescriptions
Retrieves parameter descriptions for Optimize solver.
Expr[] Objectives
The set of asserted formulas.
Status Check(params Expr[] assumptions)
Check satisfiability of asserted constraints. Produce a model that (when the objectives are bounded a...
BoolExpr[] UnsatCore
The unsat core of the last Check.
void Assert(IEnumerable< BoolExpr > constraints)
Assert a constraint (or multiple) into the optimize solver.
override string ToString()
Print the context to a string (SMT-LIB parseable benchmark).
void FromFile(string file)
Parse an SMT-LIB2 file with optimization objectives and constraints. The parsed constraints and objec...
void Set(string name, bool value)
Sets parameter on the optimize solver
void Set(Symbol name, double value)
Sets parameter on the optimize solver
void Set(Symbol name, bool value)
Sets parameter on the optimize solver
void Add(params BoolExpr[] constraints)
Alias for Assert.
Handle AssertSoft(BoolExpr constraint, uint weight, string group)
Assert soft constraint
void Set(string name, Symbol value)
Sets parameter on the optimize solver
void Set(Symbol name, uint value)
Sets parameter on the optimize solver
String ReasonUnknown
Return a string the describes why the last to check returned unknown
A ParamDescrs describes a set of parameters.
A Params objects represents a configuration in the form of Symbol/value pairs.
Params Add(Symbol name, bool value)
Adds a parameter setting.
Objects of this class track statistical information about solvers.
Symbols are used to name several term and type constructors.
Internal base class for interfacing with native Z3 objects. Should not be used externally.
def String(name, ctx=None)
Z3_lbool
Lifted Boolean type: false, undefined, true.
Z3_optimize Z3_API Z3_mk_optimize(Z3_context c)
Create a new optimize context.