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  }

◆ 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  }

◆ 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); }

◆ 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 395 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 36 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 268 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  }

◆ Objectives

Expr [] Objectives
get

The set of asserted formulas.

Definition at line 408 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 101 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 47 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 358 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 422 of file Optimize.cs.

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

◆ 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 288 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  }
Microsoft.Z3.Context.MkSymbol
IntSymbol MkSymbol(int i)
Creates a new symbol using an integer.
Definition: Context.cs:90
Microsoft.Z3.Optimize.Parameters
Params Parameters
Sets the optimize solver parameters.
Definition: Optimize.cs:47
Z3_lbool
Z3_lbool
Lifted Boolean type: false, undefined, true.
Definition: z3_api.h:101
Microsoft.Z3.Optimize.Model
Model Model
The model of the last Check.
Definition: Optimize.cs:268
Microsoft.Z3.Params.Add
Params Add(Symbol name, bool value)
Adds a parameter setting.
Definition: Params.cs:33
Microsoft.Z3.Optimize.Statistics
Statistics Statistics
Optimize statistics.
Definition: Optimize.cs:422
Microsoft.Z3.Status
Status
Status values.
Definition: Status.cs:28
Microsoft.Z3.Context.MkParams
Params MkParams()
Creates a new ParameterSet.
Definition: Context.cs:3290