Z3
Data Structures | Public Member Functions | Properties
Optimize Class Reference

Object for managing optimization context More...

+ Inheritance diagram for Optimize:

Data Structures

class  DecRefQueue
 
class  Handle
 Handle to objectives returned by objective functions. More...
 

Public Member Functions

void Set (string name, bool value)
 Sets parameter on the optimize solver More...
 
void Set (string name, uint value)
 Sets parameter on the optimize solver More...
 
void Set (string name, double value)
 Sets parameter on the optimize solver More...
 
void Set (string name, string value)
 Sets parameter on the optimize solver More...
 
void Set (string name, Symbol value)
 Sets parameter on the optimize solver More...
 
void Set (Symbol name, bool value)
 Sets parameter on the optimize solver More...
 
void Set (Symbol name, uint value)
 Sets parameter on the optimize solver More...
 
void Set (Symbol name, double value)
 Sets parameter on the optimize solver More...
 
void Set (Symbol name, string value)
 Sets parameter on the optimize solver More...
 
void Set (Symbol name, Symbol value)
 Sets parameter on the optimize solver More...
 
void Assert (params BoolExpr[] constraints)
 Assert a constraint (or multiple) into the optimize solver. More...
 
void Assert (IEnumerable< BoolExpr > constraints)
 Assert a constraint (or multiple) into the optimize solver. More...
 
void Add (params BoolExpr[] constraints)
 Alias for Assert. More...
 
void Add (IEnumerable< BoolExpr > constraints)
 Alias for Assert. More...
 
Handle AssertSoft (BoolExpr constraint, uint weight, string group)
 Assert soft constraint More...
 
Status Check (params Expr[] assumptions)
 Check satisfiability of asserted constraints. Produce a model that (when the objectives are bounded and don't use strict inequalities) meets the objectives. More...
 
void Push ()
 Creates a backtracking point. More...
 
void Pop ()
 Backtrack one backtracking point. More...
 
Handle MkMaximize (Expr e)
 Declare an arithmetical maximization objective. Return a handle to the objective. The handle is used as to retrieve the values of objectives after calling Check. The expression can be either an arithmetical expression or bit-vector. More...
 
Handle MkMinimize (Expr e)
 Declare an arithmetical minimization objective. Similar to MkMaximize. More...
 
override string ToString ()
 Print the context to a string (SMT-LIB parseable benchmark). More...
 
void FromFile (string file)
 Parse an SMT-LIB2 file with optimization objectives and constraints. The parsed constraints and objectives are added to the optimization context. More...
 
void FromString (string s)
 Similar to FromFile. Instead it takes as argument a string. More...
 
- Public Member Functions inherited from Z3Object
void Dispose ()
 Disposes of the underlying native Z3 object. More...
 

Properties

string Help [get]
 A string that describes all available optimize solver parameters. More...
 
Params Parameters [set]
 Sets the optimize solver parameters. More...
 
ParamDescrs ParameterDescriptions [get]
 Retrieves parameter descriptions for Optimize solver. More...
 
Model Model [get]
 The model of the last Check. More...
 
BoolExpr[] UnsatCore [get]
 The unsat core of the last Check. More...
 
String ReasonUnknown [get]
 Return a string the describes why the last to check returned unknown More...
 
BoolExpr[] Assertions [get]
 The set of asserted formulas. More...
 
Expr[] Objectives [get]
 The set of asserted formulas. More...
 
Statistics Statistics [get]
 Optimize statistics. More...
 

Detailed Description

Object for managing optimization context

Definition at line 30 of file Optimize.cs.

Member Function Documentation

◆ Add() [1/2]

void Add ( IEnumerable< BoolExpr constraints)
inline

Alias for Assert.


Definition at line 132 of file Optimize.cs.

133 {
134 AddConstraints(constraints);
135 }

◆ Add() [2/2]

void Add ( params BoolExpr[]  constraints)
inline

Alias for Assert.


Definition at line 124 of file Optimize.cs.

125 {
126 AddConstraints(constraints);
127 }

◆ Assert() [1/2]

void Assert ( IEnumerable< BoolExpr constraints)
inline

Assert a constraint (or multiple) into the optimize solver.


Definition at line 116 of file Optimize.cs.

117 {
118 AddConstraints(constraints);
119 }

◆ Assert() [2/2]

void Assert ( params BoolExpr[]  constraints)
inline

Assert a constraint (or multiple) into the optimize solver.


Definition at line 108 of file Optimize.cs.

109 {
110 AddConstraints(constraints);
111 }

◆ AssertSoft()

Handle AssertSoft ( BoolExpr  constraint,
uint  weight,
string  group 
)
inline

Assert soft constraint


Return an objective which associates with the group of constraints.

Definition at line 212 of file Optimize.cs.

213 {
214 Context.CheckContextMatch(constraint);
215 Symbol s = Context.MkSymbol(group);
216 return new Handle(this, Native.Z3_optimize_assert_soft(Context.nCtx, NativeObject, constraint.NativeObject, weight.ToString(), s.NativeObject));
217 }
IntSymbol MkSymbol(int i)
Creates a new symbol using an integer.
Definition: Context.cs:90

◆ Check()

Status Check ( params Expr[]  assumptions)
inline

Check satisfiability of asserted constraints. Produce a model that (when the objectives are bounded and don't use strict inequalities) meets the objectives.

Definition at line 226 of file Optimize.cs.

227 {
228 Z3_lbool r = (Z3_lbool)Native.Z3_optimize_check(Context.nCtx, NativeObject, (uint)assumptions.Length, AST.ArrayToNative(assumptions));
229 switch (r)
230 {
231 case Z3_lbool.Z3_L_TRUE:
232 return Status.SATISFIABLE;
233 case Z3_lbool.Z3_L_FALSE:
234 return Status.UNSATISFIABLE;
235 default:
236 return Status.UNKNOWN;
237 }
238 }
Status
Status values.
Definition: Status.cs:29
Z3_lbool
Lifted Boolean type: false, undefined, true.
Definition: z3_api.h:102

◆ FromFile()

void FromFile ( string  file)
inline

Parse an SMT-LIB2 file with optimization objectives and constraints. The parsed constraints and objectives are added to the optimization context.


Definition at line 378 of file Optimize.cs.

379 {
380 Native.Z3_optimize_from_file(Context.nCtx, NativeObject, file);
381 }

◆ FromString()

void FromString ( string  s)
inline

Similar to FromFile. Instead it takes as argument a string.

Definition at line 386 of file Optimize.cs.

387 {
388 Native.Z3_optimize_from_string(Context.nCtx, NativeObject, s);
389 }

◆ MkMaximize()

Handle MkMaximize ( Expr  e)
inline

Declare an arithmetical maximization objective. Return a handle to the objective. The handle is used as to retrieve the values of objectives after calling Check. The expression can be either an arithmetical expression or bit-vector.


Definition at line 303 of file Optimize.cs.

304 {
305 return new Handle(this, Native.Z3_optimize_maximize(Context.nCtx, NativeObject, e.NativeObject));
306 }

◆ MkMinimize()

Handle MkMinimize ( Expr  e)
inline

Declare an arithmetical minimization objective. Similar to MkMaximize.


Definition at line 312 of file Optimize.cs.

313 {
314 return new Handle(this, Native.Z3_optimize_minimize(Context.nCtx, NativeObject, e.NativeObject));
315 }

◆ Pop()

void Pop ( )
inline

Backtrack one backtracking point.

Note that an exception is thrown if Pop is called without a corresponding Push

See also
Push

Definition at line 254 of file Optimize.cs.

255 {
256 Native.Z3_optimize_pop(Context.nCtx, NativeObject);
257 }

◆ Push()

void Push ( )
inline

Creates a backtracking point.

See also
Pop

Definition at line 244 of file Optimize.cs.

245 {
246 Native.Z3_optimize_push(Context.nCtx, NativeObject);
247 }

◆ Set() [1/10]

void Set ( string  name,
bool  value 
)
inline

Sets parameter on the optimize solver

Definition at line 59 of file Optimize.cs.

59{ Parameters = Context.MkParams().Add(name, value); }
Params MkParams()
Creates a new ParameterSet.
Definition: Context.cs:3290
Params Parameters
Sets the optimize solver parameters.
Definition: Optimize.cs:47
Params Add(Symbol name, bool value)
Adds a parameter setting.
Definition: Params.cs:33

◆ Set() [2/10]

void Set ( string  name,
double  value 
)
inline

Sets parameter on the optimize solver

Definition at line 67 of file Optimize.cs.

67{ Parameters = Context.MkParams().Add(name, value); }

◆ Set() [3/10]

void Set ( string  name,
string  value 
)
inline

Sets parameter on the optimize solver

Definition at line 71 of file Optimize.cs.

71{ Parameters = Context.MkParams().Add(name, value); }

◆ Set() [4/10]

void Set ( string  name,
Symbol  value 
)
inline

Sets parameter on the optimize solver

Definition at line 75 of file Optimize.cs.

75{ Parameters = Context.MkParams().Add(name, value); }

◆ Set() [5/10]

void Set ( string  name,
uint  value 
)
inline

Sets parameter on the optimize solver

Definition at line 63 of file Optimize.cs.

63{ Parameters = Context.MkParams().Add(name, value); }

◆ Set() [6/10]

void Set ( Symbol  name,
bool  value 
)
inline

Sets parameter on the optimize solver

Definition at line 79 of file Optimize.cs.

79{ Parameters = Context.MkParams().Add(name, value); }

◆ Set() [7/10]

void Set ( Symbol  name,
double  value 
)
inline

Sets parameter on the optimize solver

Definition at line 87 of file Optimize.cs.

87{ Parameters = Context.MkParams().Add(name, value); }

◆ Set() [8/10]

void Set ( Symbol  name,
string  value 
)
inline

Sets parameter on the optimize solver

Definition at line 91 of file Optimize.cs.

91{ Parameters = Context.MkParams().Add(name, value); }

◆ Set() [9/10]

void Set ( Symbol  name,
Symbol  value 
)
inline

Sets parameter on the optimize solver

Definition at line 95 of file Optimize.cs.

95{ Parameters = Context.MkParams().Add(name, value); }

◆ Set() [10/10]

void Set ( Symbol  name,
uint  value 
)
inline

Sets parameter on the optimize solver

Definition at line 83 of file Optimize.cs.

83{ Parameters = Context.MkParams().Add(name, value); }

◆ ToString()

override string ToString ( )
inline

Print the context to a string (SMT-LIB parseable benchmark).


Definition at line 369 of file Optimize.cs.

370 {
371 return Native.Z3_optimize_to_string(Context.nCtx, NativeObject);
372 }

Property Documentation

◆ Assertions

BoolExpr [] Assertions
get

The set of asserted formulas.

Definition at line 394 of file Optimize.cs.

395 {
396 get
397 {
398
399 ASTVector assertions = new ASTVector(Context, Native.Z3_optimize_get_assertions(Context.nCtx, NativeObject));
400 return assertions.ToBoolExprArray();
401 }
402 }

◆ Help

string Help
get

A string that describes all available optimize solver parameters.

Definition at line 35 of file Optimize.cs.

36 {
37 get
38 {
39 return Native.Z3_optimize_get_help(Context.nCtx, NativeObject);
40 }
41 }

◆ Model

Model Model
get

The model of the last Check.

The result is null if Check was not invoked before, if its results was not SATISFIABLE, or if model production is not enabled.

Definition at line 267 of file Optimize.cs.

268 {
269 get
270 {
271 IntPtr x = Native.Z3_optimize_get_model(Context.nCtx, NativeObject);
272 if (x == IntPtr.Zero)
273 return null;
274 else
275 return new Model(Context, x);
276 }
277 }
Model Model
The model of the last Check.
Definition: Optimize.cs:268

◆ Objectives

Expr [] Objectives
get

The set of asserted formulas.

Definition at line 407 of file Optimize.cs.

408 {
409 get
410 {
411
412 ASTVector objectives = new ASTVector(Context, Native.Z3_optimize_get_objectives(Context.nCtx, NativeObject));
413 return objectives.ToExprArray();
414 }
415 }

◆ ParameterDescriptions

ParamDescrs ParameterDescriptions
get

Retrieves parameter descriptions for Optimize solver.

Definition at line 100 of file Optimize.cs.

101 {
102 get { return new ParamDescrs(Context, Native.Z3_optimize_get_param_descrs(Context.nCtx, NativeObject)); }
103 }

◆ Parameters

Params Parameters
set

Sets the optimize solver parameters.

Definition at line 46 of file Optimize.cs.

47 {
48 set
49 {
50 Debug.Assert(value != null);
51 Context.CheckContextMatch(value);
52 Native.Z3_optimize_set_params(Context.nCtx, NativeObject, value.NativeObject);
53 }
54 }

Referenced by Optimize.Set().

◆ ReasonUnknown

String ReasonUnknown
get

Return a string the describes why the last to check returned unknown


Definition at line 357 of file Optimize.cs.

358 {
359 get
360 {
361 return Native.Z3_optimize_get_reason_unknown(Context.nCtx, NativeObject);
362 }
363 }

◆ Statistics

Optimize statistics.

Definition at line 421 of file Optimize.cs.

422 {
423 get
424 {
425
426 return new Statistics(Context, Native.Z3_optimize_get_statistics(Context.nCtx, NativeObject));
427 }
428 }
Statistics Statistics
Optimize statistics.
Definition: Optimize.cs:422

◆ UnsatCore

BoolExpr [] UnsatCore
get

The unsat core of the last Check.

The unsat core is a subset of assumptions The result is empty if Check was not invoked before, if its results was not UNSATISFIABLE, or if core production is disabled.

Definition at line 287 of file Optimize.cs.

288 {
289 get
290 {
291
292 ASTVector core = new ASTVector(Context, Native.Z3_optimize_get_unsat_core(Context.nCtx, NativeObject));
293 return core.ToBoolExprArray();
294 }
295 }