Class Z3Visitor
This is a helper class to create an expression for the Z3 Solver visiting all nodes of an Expression.
Inheritance
System.Object
Z3Visitor
Namespace: OPTANO.Modeling.Optimization.Solver.Z3
Assembly: Optimization.Solver.Z3.dll
Syntax
public class Z3Visitor : object, IExpressionVisitor<ArithExpr>Constructors
Z3Visitor(Dictionary<String, ArithExpr>, Context)
Initializes a new instance of the Z3Visitor class.
Initializes a new instance of of the
Declaration
public Z3Visitor(Dictionary<string, ArithExpr> variables, Context ctx)Parameters
| Type | Name | Description |
|---|---|---|
| Dictionary<System.String, ArithExpr> | variables | All variables of a model in Z3. |
| Context | ctx | The ctx. |
Methods
VisitExpression(Expression)
The visit expression.
Declaration
public ArithExpr VisitExpression(Expression exp)Parameters
| Type | Name | Description |
|---|---|---|
| Expression | exp | The exp. |
Returns
| Type | Description |
|---|---|
| ArithExpr | The |
Explicit Interface Implementations
IExpressionVisitor<ArithExpr>.Visit(Expression)
Returns the corresponding expression of the Z3 Solver.
Declaration
ArithExpr IExpressionVisitor<ArithExpr>.Visit(Expression exp)Parameters
| Type | Name | Description |
|---|---|---|
| Expression | exp | The Expression. |
Returns
| Type | Description |
|---|---|
| ArithExpr | The expression of the Z3 Solver. |