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

【问题标题】：Scala-Z3: How to perform member access on objectsScala-Z3：如何对对象执行成员访问
【发布时间】：2020-08-25 09:41:03
【问题描述】：

我在 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)

如何访问x 圈子成员C？

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

【问题讨论】：

标签： scala z3

【解决方案1】：

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

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

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

【讨论】：