Scala-Z3：如何对对象执行成员访问

Question

我在 Scala 中使用 java API 定义了以下圆圈排序：（其中 ctx 是 Z3 上下文）

val circleConstructor = ctx.mkConstructor(
    "Circle",
    "Circle",
    Array("x", "y", "r"),
    Array(ctx.mkRealSort, ctx.mkRealSort, ctx.mkRealSort),
    null)

val circleSort: DatatypeSort = ctx.mkDatatypeSort(
    ctx.mkSymbol("Circle"), Array(circleConstructor))

val getX: FuncDecl = circleSort.getAccessors()(0)(0)

val constCirlce: FuncDecl = ctx.mkConstDecl("C", circleSort)

如何访问 C 圈子的 x 成员？

我试过将 ctx.mkApp 与 getX 函数一起使用，但不知道如何引用 C 常量？

Answer 1

我想通了。要访问圆常数，您只需使用代码中定义的变量，如下所示：

val A = ctx.mkMul(ctx.mkApp(getX, constCirlce).asInstanceOf[ArithExpr])

.asInstanceOf[ArithExpr] 用于将 mkApp 的结果转换为 ArithExpr，因为 mkMul 期望 Expr。我不知道如何避免这种显式转换。

Scala-Z3：如何对对象执行成员访问

Scala-Z3: How to perform member access on objects

scala

z3