A RetroSearch Logo

Home - News ( United States | United Kingdom | Italy | Germany ) - Football scores

Search Query:

Showing content from https://z3prover.github.io/api/html/class_microsoft_1_1_z3_1_1_optimize.html below:

Z3: Optimize Class Reference

Object for managing optimization context More...

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) is optimal. 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...
  void  Dispose ()   Disposes of the underlying native Z3 object. More...
 

Object for managing optimization context

Definition at line 30 of file Optimize.cs.

◆ Add() [1/2] void Add ( IEnumerable< BoolExpr >  constraints ) inline

Alias for Assert.

Definition at line 132 of file Optimize.cs.

134

AddConstraints(constraints);

◆ Add() [2/2] void Add ( params BoolExpr[]  constraints ) inline

Alias for Assert.

Definition at line 124 of file Optimize.cs.

126

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.

118

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.

110

AddConstraints(constraints);

◆ AssertSoft()

Assert soft constraint

Return an objective which associates with the group of constraints.

Definition at line 212 of file Optimize.cs.

214  Context

.CheckContextMatch(constraint);

216  return new

Handle(

this

, Native.Z3_optimize_assert_soft(

Context

.nCtx, NativeObject, constraint.NativeObject, weight.ToString(), s.NativeObject));

IntSymbol MkSymbol(int i)

Creates a new symbol using an integer.

Context Context

Access Context object

◆ Check()

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

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;

Z3_lbool

Lifted Boolean type: false, undefined, true.

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

380

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

388

Native.Z3_optimize_from_string(

Context

.nCtx, NativeObject, s);

◆ MkMaximize()

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.

305  return new

Handle(

this

, Native.Z3_optimize_maximize(

Context

.nCtx, NativeObject, e.NativeObject));

◆ MkMinimize()

Declare an arithmetical minimization objective. Similar to MkMaximize.

Definition at line 312 of file Optimize.cs.

314  return new

Handle(

this

, Native.Z3_optimize_minimize(

Context

.nCtx, NativeObject, e.NativeObject));

◆ Pop()

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.

256

Native.Z3_optimize_pop(

Context

.nCtx, NativeObject);

◆ Push()

Creates a backtracking point.

See also
Pop

Definition at line 244 of file Optimize.cs.

246

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.

Params MkParams()

Creates a new ParameterSet.

Params Parameters

Sets the optimize solver parameters.

Params Add(Symbol name, bool value)

Adds a parameter setting.

◆ Set() [2/10] void Set ( string  name, double  value  ) inline

Sets parameter on the optimize solver

Definition at line 67 of file Optimize.cs.

◆ Set() [3/10] void Set ( string  name, string  value  ) inline

Sets parameter on the optimize solver

Definition at line 71 of file Optimize.cs.

◆ Set() [4/10] void Set ( string  name, Symbol  value  ) inline

Sets parameter on the optimize solver

Definition at line 75 of file Optimize.cs.

◆ Set() [5/10] void Set ( string  name, uint  value  ) inline

Sets parameter on the optimize solver

Definition at line 63 of file Optimize.cs.

◆ Set() [6/10] void Set ( Symbol  name, bool  value  ) inline

Sets parameter on the optimize solver

Definition at line 79 of file Optimize.cs.

◆ Set() [7/10] void Set ( Symbol  name, double  value  ) inline

Sets parameter on the optimize solver

Definition at line 87 of file Optimize.cs.

◆ Set() [8/10] void Set ( Symbol  name, string  value  ) inline

Sets parameter on the optimize solver

Definition at line 91 of file Optimize.cs.

◆ Set() [9/10]

Sets parameter on the optimize solver

Definition at line 95 of file Optimize.cs.

◆ Set() [10/10] void Set ( Symbol  name, uint  value  ) inline

Sets parameter on the optimize solver

Definition at line 83 of file Optimize.cs.

◆ ToString() override string ToString ( ) inline

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

Definition at line 369 of file Optimize.cs.

371  return

Native.Z3_optimize_to_string(

Context

.nCtx, NativeObject);

◆ Assertions

The set of asserted formulas.

Definition at line 394 of file Optimize.cs.

399  using

ASTVector assertions =

new

ASTVector(

Context

, Native.Z3_optimize_get_assertions(

Context

.nCtx, NativeObject));

400  return

assertions.ToBoolExprArray();

◆ Help

A string that describes all available optimize solver parameters.

Definition at line 35 of file Optimize.cs.

39  return

Native.Z3_optimize_get_help(

Context

.nCtx, NativeObject);

◆ Model

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.

271

IntPtr x = Native.Z3_optimize_get_model(

Context

.nCtx, NativeObject);

272  if

(x == IntPtr.Zero)

Model Model

The model of the last Check.

◆ Objectives

The set of asserted formulas.

Definition at line 407 of file Optimize.cs.

412  using

ASTVector objectives =

new

ASTVector(

Context

, Native.Z3_optimize_get_objectives(

Context

.nCtx, NativeObject));

413  return

objectives.ToExprArray();

◆ ParameterDescriptions

Retrieves parameter descriptions for Optimize solver.

Definition at line 100 of file Optimize.cs.

102  get

{

return new

ParamDescrs(

Context

, Native.Z3_optimize_get_param_descrs(

Context

.nCtx, NativeObject)); }

◆ Parameters

Sets the optimize solver parameters.

Definition at line 46 of file Optimize.cs.

50

Debug.Assert(value !=

null

);

51  Context

.CheckContextMatch(value);

52

Native.Z3_optimize_set_params(

Context

.nCtx, NativeObject, value.NativeObject);

Referenced by Optimize.Set().

◆ ReasonUnknown

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

Definition at line 357 of file Optimize.cs.

361  return

Native.Z3_optimize_get_reason_unknown(

Context

.nCtx, NativeObject);

◆ Statistics ◆ UnsatCore

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.

292  using

ASTVector core =

new

ASTVector(

Context

, Native.Z3_optimize_get_unsat_core(

Context

.nCtx, NativeObject));

293  return

core.ToBoolExprArray();

RetroSearch is an open source project built by @garambo | Open a GitHub Issue

Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo

HTML: 3.2 | Encoding: UTF-8 | Version: 0.7.4