如何解决Scala-Z3:如何对对象执行成员访问
我已使用Java API在Scala中定义了以下圆圈Sort:
(其中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
的{{1}}成员?
我尝试将C
与ctx.mkApp
函数一起使用,但是不知道如何引用getX
常量?
解决方法
我知道了。 要访问圆常量,只需使用代码中定义的变量,如下所示:
val A = ctx.mkMul(ctx.mkApp(getX,constCirlce).asInstanceOf[ArithExpr])
.asInstanceOf[ArithExpr]
用于将mkApp
的结果强制转换为ArithExpr
,因为mkMul
期望Expr
。
我不知道如何避免这种显式转换。
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。