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

Object for managing optimizization context More...

+ Inheritance diagram for Optimize:

Data Structures

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

Public Member Functions

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 ()
 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 (ArithExpr 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. More...
 
Handle MkMinimize (ArithExpr 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...
 
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 optimizization context

Definition at line 30 of file Optimize.cs.

Member Function Documentation

§ Add() [1/2]

void Add ( params BoolExpr []  constraints)
inline

Alias for Assert.

Definition at line 84 of file Optimize.cs.

85  {
86  AddConstraints(constraints);
87  }

§ Add() [2/2]

void Add ( IEnumerable< BoolExpr constraints)
inline

Alias for Assert.

Definition at line 92 of file Optimize.cs.

93  {
94  AddConstraints(constraints);
95  }

§ Assert() [1/2]

void Assert ( params BoolExpr []  constraints)
inline

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

Definition at line 68 of file Optimize.cs.

69  {
70  AddConstraints(constraints);
71  }

§ Assert() [2/2]

void Assert ( IEnumerable< BoolExpr constraints)
inline

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

Definition at line 76 of file Optimize.cs.

77  {
78  AddConstraints(constraints);
79  }

§ 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 155 of file Optimize.cs.

156  {
157  Context.CheckContextMatch(constraint);
158  Symbol s = Context.MkSymbol(group);
159  return new Handle(this, Native.Z3_optimize_assert_soft(Context.nCtx, NativeObject, constraint.NativeObject, weight.ToString(), s.NativeObject));
160  }
IntSymbol MkSymbol(int i)
Creates a new symbol using an integer.
Definition: Context.cs:91

§ Check()

Status Check ( )
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 169 of file Optimize.cs.

170  {
171  Z3_lbool r = (Z3_lbool)Native.Z3_optimize_check(Context.nCtx, NativeObject);
172  switch (r)
173  {
174  case Z3_lbool.Z3_L_TRUE:
175  return Status.SATISFIABLE;
176  case Z3_lbool.Z3_L_FALSE:
177  return Status.UNSATISFIABLE;
178  default:
179  return Status.UNKNOWN;
180  }
181  }
Z3_lbool
Lifted Boolean type: false, undefined, true.
Definition: z3_api.h:105
Status
Status values.
Definition: Status.cs:27

§ 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 283 of file Optimize.cs.

284  {
285  Native.Z3_optimize_from_file(Context.nCtx, NativeObject, file);
286  }

§ FromString()

void FromString ( string  s)
inline

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

Definition at line 291 of file Optimize.cs.

292  {
293  Native.Z3_optimize_from_string(Context.nCtx, NativeObject, s);
294  }

§ MkMaximize()

Handle MkMaximize ( ArithExpr  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.

Definition at line 227 of file Optimize.cs.

228  {
229  return new Handle(this, Native.Z3_optimize_maximize(Context.nCtx, NativeObject, e.NativeObject));
230  }

§ MkMinimize()

Handle MkMinimize ( ArithExpr  e)
inline

Declare an arithmetical minimization objective. Similar to MkMaximize.

Definition at line 236 of file Optimize.cs.

237  {
238  return new Handle(this, Native.Z3_optimize_minimize(Context.nCtx, NativeObject, e.NativeObject));
239  }

§ 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 197 of file Optimize.cs.

198  {
199  Native.Z3_optimize_pop(Context.nCtx, NativeObject);
200  }

§ Push()

void Push ( )
inline

Creates a backtracking point.

See also
Pop

Definition at line 187 of file Optimize.cs.

188  {
189  Native.Z3_optimize_push(Context.nCtx, NativeObject);
190  }

§ ToString()

override string ToString ( )
inline

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

Definition at line 274 of file Optimize.cs.

275  {
276  return Native.Z3_optimize_to_string(Context.nCtx, NativeObject);
277  }

Property Documentation

§ Assertions

BoolExpr [] Assertions
get

The set of asserted formulas.

Definition at line 300 of file Optimize.cs.

§ Help

string Help
get

A string that describes all available optimize solver parameters.

Definition at line 36 of file Optimize.cs.

§ 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 211 of file Optimize.cs.

§ Objectives

Expr [] Objectives
get

The set of asserted formulas.

Definition at line 314 of file Optimize.cs.

§ ParameterDescriptions

ParamDescrs ParameterDescriptions
get

Retrieves parameter descriptions for Optimize solver.

Definition at line 61 of file Optimize.cs.

§ Parameters

Params Parameters
set

Sets the optimize solver parameters.

Definition at line 48 of file Optimize.cs.

§ ReasonUnknown

String ReasonUnknown
get

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

Definition at line 262 of file Optimize.cs.

§ Statistics

Optimize statistics.

Definition at line 329 of file Optimize.cs.