Object for managing optimization context. More...

Inheritance diagram for Optimize:

Data Structures
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.

void	Set (string name, uint value)
	Sets parameter on the optimize solver.

void	Set (string name, double value)
	Sets parameter on the optimize solver.

void	Set (string name, string value)
	Sets parameter on the optimize solver.

void	Set (string name, Symbol value)
	Sets parameter on the optimize solver.

void	Set (Symbol name, bool value)
	Sets parameter on the optimize solver.

void	Set (Symbol name, uint value)
	Sets parameter on the optimize solver.

void	Set (Symbol name, double value)
	Sets parameter on the optimize solver.

void	Set (Symbol name, string value)
	Sets parameter on the optimize solver.

void	Set (Symbol name, Symbol value)
	Sets parameter on the optimize solver.

void	Assert (params BoolExpr[] constraints)
	Assert a constraint (or multiple) into the optimize solver.

void	Assert (IEnumerable< BoolExpr > constraints)
	Assert a constraint (or multiple) into the optimize solver.

void	Add (params BoolExpr[] constraints)
	Alias for Assert.

void	Add (IEnumerable< BoolExpr > constraints)
	Alias for Assert.

void	AssertAndTrack (BoolExpr constraint, BoolExpr p)
	Assert a constraint into the optimize solver, and track it (in the unsat) core using the Boolean constant p.

Handle	AssertSoft (BoolExpr constraint, uint weight, string group)
	Assert soft constraint.

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) is optimal.

void	Push ()
	Creates a backtracking point.

void	Pop ()
	Backtrack one backtracking point.

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.

Handle	MkMinimize (Expr e)
	Declare an arithmetical minimization objective. Similar to MkMaximize.

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 objectives are added to the optimization context.

void	FromString (string s)
	Similar to FromFile. Instead it takes as argument a string.

Public Member Functions inherited from Z3Object
void	Dispose ()
	Disposes of the underlying native Z3 object.

Properties
string	Help `[get]`
	A string that describes all available optimize solver parameters.

Params	Parameters `[set]`
	Sets the optimize solver parameters.

ParamDescrs	ParameterDescriptions `[get]`
	Retrieves parameter descriptions for Optimize solver.

Model	Model `[get]`
	The model of the last `Check`.

BoolExpr[]	UnsatCore `[get]`
	The unsat core of the last `Check`.

String	ReasonUnknown `[get]`
	Return a string the describes why the last to check returned unknown.

BoolExpr[]	Assertions `[get]`
	The set of asserted formulas.

Expr[]	Objectives `[get]`
	The set of asserted formulas.

Statistics	Statistics `[get]`
	Optimize statistics.

Properties inherited from Z3Object
Context	Context `[get]`
	Access Context object.

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.

        {
            AddConstraints(constraints);
        }

◆ Add() [2/2]

void Add ( params BoolExpr[] constraints )

inline

Alias for Assert.

Definition at line 124 of file Optimize.cs.

        {
            AddConstraints(constraints);
        }

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

        {
            AddConstraints(constraints);
        }

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

        {
            AddConstraints(constraints);
        }

◆ AssertAndTrack()

void AssertAndTrack	(	BoolExpr	constraint,
		BoolExpr	p
	)

inline

Assert a constraint into the optimize solver, and track it (in the unsat) core using the Boolean constant p.

This API is an alternative to Check(Expr[]) with assumptions for extracting unsat cores. Both APIs can be used in the same solver. The unsat core will contain a combination of the Boolean variables provided using AssertAndTrack(BoolExpr,BoolExpr) and the Boolean literals provided using Check(Expr[]) with assumptions.

Definition at line 163 of file Optimize.cs.

        {
            Debug.Assert(constraint != null);
            Debug.Assert(p != null);
            Context.CheckContextMatch(constraint);
            Context.CheckContextMatch(p);
                        
            Native.Z3_optimize_assert_and_track(Context.nCtx, NativeObject, constraint.NativeObject, p.NativeObject);
        }

◆ 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 234 of file Optimize.cs.

        {
            Context.CheckContextMatch(constraint);
            using Symbol s = Context.MkSymbol(group);
            return new Handle(this, Native.Z3_optimize_assert_soft(Context.nCtx, NativeObject, constraint.NativeObject, weight.ToString(), s.NativeObject));
        }

◆ 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) is optimal.

Definition at line 248 of file Optimize.cs.

        {
            Z3_lbool r = (Z3_lbool)Native.Z3_optimize_check(Context.nCtx, NativeObject, (uint)assumptions.Length, AST.ArrayToNative(assumptions));
            switch (r)
            {
                case Z3_lbool.Z3_L_TRUE:
                    return Status.SATISFIABLE;
                case Z3_lbool.Z3_L_FALSE:
                    return Status.UNSATISFIABLE;
                default:
                    return Status.UNKNOWN;
            }
        }

◆ 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 400 of file Optimize.cs.

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

◆ FromString()

void FromString ( string s )

inline

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

Definition at line 408 of file Optimize.cs.

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

◆ 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 325 of file Optimize.cs.

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

◆ MkMinimize()

Handle MkMinimize ( Expr e )

inline

Declare an arithmetical minimization objective. Similar to MkMaximize.

Definition at line 334 of file Optimize.cs.

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

◆ 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 276 of file Optimize.cs.

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

◆ Push()

void Push ( )

inline

Creates a backtracking point.

See also: Pop

Definition at line 266 of file Optimize.cs.

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

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

Microsoft.Z3.Context.MkParams

Params MkParams()

Creates a new ParameterSet.

Definition Context.cs:3465

Microsoft.Z3.Optimize.Parameters

Params Parameters

Sets the optimize solver parameters.

Definition Optimize.cs:47

Microsoft.Z3.Params.Add

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

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

Property Documentation

◆ Assertions

BoolExpr [] Assertions

get

The set of asserted formulas.

Definition at line 416 of file Optimize.cs.

        {
            get
            {
 
                using ASTVector assertions = new ASTVector(Context, Native.Z3_optimize_get_assertions(Context.nCtx, NativeObject));
                return assertions.ToBoolExprArray();
            }
        }

◆ Help

string Help

get

A string that describes all available optimize solver parameters.

Definition at line 35 of file Optimize.cs.

        {
            get
            {
                return Native.Z3_optimize_get_help(Context.nCtx, NativeObject);
            }
        }

◆ 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 289 of file Optimize.cs.

        {
            get
            {
                IntPtr x = Native.Z3_optimize_get_model(Context.nCtx, NativeObject);
                if (x == IntPtr.Zero)
                    return null;
                else
                    return new Model(Context, x);
            }
        }

◆ Objectives

Expr [] Objectives

get

The set of asserted formulas.

Definition at line 429 of file Optimize.cs.

        {
            get
            {
 
                using ASTVector objectives = new ASTVector(Context, Native.Z3_optimize_get_objectives(Context.nCtx, NativeObject));
                return objectives.ToExprArray();
            }
        }

◆ ParameterDescriptions

ParamDescrs ParameterDescriptions

get

Retrieves parameter descriptions for Optimize solver.

Definition at line 100 of file Optimize.cs.

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

◆ Parameters

Params Parameters

set

Sets the optimize solver parameters.

Definition at line 46 of file Optimize.cs.

        {
            set
            {
                Debug.Assert(value != null);
                Context.CheckContextMatch(value);
                Native.Z3_optimize_set_params(Context.nCtx, NativeObject, value.NativeObject);
            }
        }

Referenced by Optimize.Set(), Optimize.Set(), Optimize.Set(), Optimize.Set(), Optimize.Set(), Optimize.Set(), Optimize.Set(), Optimize.Set(), Optimize.Set(), and Optimize.Set().

◆ ReasonUnknown

String ReasonUnknown

get

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

Definition at line 379 of file Optimize.cs.

        {
            get 
            {
                return Native.Z3_optimize_get_reason_unknown(Context.nCtx, NativeObject);
            }
        }

◆ Statistics

Statistics Statistics

get

Optimize statistics.

Definition at line 443 of file Optimize.cs.

        {
            get
            {
 
                return new Statistics(Context, Native.Z3_optimize_get_statistics(Context.nCtx, NativeObject));
            }
        }

◆ 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 309 of file Optimize.cs.

        {
            get
            {
 
                using ASTVector core = new ASTVector(Context, Native.Z3_optimize_get_unsat_core(Context.nCtx, NativeObject));                
                return core.ToBoolExprArray();
            }
        }

Data Structures

Public Member Functions

Properties

Detailed Description

Member Function Documentation

◆ Add() [1/2]

◆ Add() [2/2]

◆ Assert() [1/2]

◆ Assert() [2/2]

◆ AssertAndTrack()

◆ AssertSoft()

◆ Check()

◆ FromFile()

◆ FromString()

◆ MkMaximize()

◆ MkMinimize()

◆ Pop()

◆ Push()

◆ Set() [1/10]

◆ Set() [2/10]

◆ Set() [3/10]

◆ Set() [4/10]

◆ Set() [5/10]

◆ Set() [6/10]

◆ Set() [7/10]

◆ Set() [8/10]

◆ Set() [9/10]

◆ Set() [10/10]

◆ ToString()

Property Documentation

◆ Assertions

◆ Help

◆ Model

◆ Objectives

◆ ParameterDescriptions

◆ Parameters

◆ ReasonUnknown

◆ Statistics

◆ UnsatCore