scala - 使用 z3.scala.dsl API 遍历 Z3Context

Question

我正在将 scala^Z3 工具用于一个小型库，该库（除其他外）Z3Context以乳胶格式打印 a 的约束。虽然可以Z3AST通过字符串比较来遍历和乳胶化表达式，但使用包的对象结构会更好z3.scala.dsl。有没有办法z3.scala.dsl.Tree从 a 获得 a Z3AST？

Answer 1

确实，DSL 当前是“只写”的，因为您可以使用它来创建树并将它们发送到 Z3，但不能将它们读回。

读取 Z3 树的标准方法是使用getASTKindand getDeclKindfrom Z3Context。代表结果的类分别是Z3ASTKind和Z3DeclKind。（由于大多数树都是应用程序，后者是大部分信息所在的位置）。

Answer 2

看起来这样做的方法是使用创建原始约束z3.scala.dsl，然后使用添加每个约束Z3Context.assertCnstr (tree: Tree[BoolSort])。这样我就拥有了整个 DSL 树，以便轻松转换为乳胶。出于某种原因，scala^Z3 网站上的示例完全不使用 DSL 组装 AST，因此这种替代方案并不明显。