Class Z3Solver

Inheritance
System.Object
SolverBase
GenericSolverBase<Z3SolverConfiguration>
Z3Solver
Inherited Members
Namespace: OPTANO.Modeling.Optimization.Solver.Z3
Assembly: Optimization.Solver.Z3.dll
Syntax
public class Z3Solver : GenericSolverBase<Z3SolverConfiguration>, ISolver, ICanSolve<Model, Solution>, IAbortable, IDisposable

Constructors

Z3Solver(Z3SolverConfiguration)

Creates a new Z3-Solver.

Declaration
public Z3Solver(Z3SolverConfiguration config = null)
Parameters
Type Name Description
Z3SolverConfiguration config

Methods

Abort()

Declaration
public override void Abort()
Overrides
Implements

AddConstraint(Constraint)

Add MIP-Constraint Method.

Declaration
protected void AddConstraint(Constraint constraint)
Parameters
Type Name Description
Constraint constraint

The constraint to add.

AddObjective(Objective)

Adds a objective to Z3.

Declaration
protected override void AddObjective(Objective objective)
Parameters
Type Name Description
Objective objective

The OPTANO objective to add.
Overrides

BuildSolverModelAdapterSpecific(Int32)

Declaration
protected override void BuildSolverModelAdapterSpecific(int prioLevel = 0)
Parameters
Type Name Description
System.Int32 prioLevel
Overrides

ClearLastModel()

Declaration
public override void ClearLastModel()
Overrides
Implements

RemoveConstraint(String)

Declaration
protected override void RemoveConstraint(string name)
Parameters
Type Name Description
System.String name
Overrides

SetConfigurationAdapterSpecific()

Declaration
protected override void SetConfigurationAdapterSpecific()
Overrides

SolveAdapterSpecific(Int32, IDictionary<Variable, Double>)

This method ist called by SolverBase and retuns the soltuions.

Declaration
protected override Solution SolveAdapterSpecific(int prioLevel = 0, IDictionary<Variable, double> variableValues = null)
Parameters
Type Name Description
System.Int32 prioLevel

Not used.
IDictionary<Variable, System.Double> variableValues

Not used.
Returns
Type Description
Solution

Returns the OPTANO solution of the model.

Extension Methods