scala - z3.scala.dsl API を使用して Z3Context をトラバースする

Question

私は、(とりわけ) a の制約をZ3Contextラテックス形式で出力する小さなライブラリに scala^Z3 ツールを使用しています。文字列比較によって式をトラバースしてラテックス化することは可能ですが、パッケージZ3ASTのオブジェクト構造を使用する方がはるかに優れています。からz3.scala.dslを取得する方法はありますか?z3.scala.dsl.TreeZ3AST

Answer 1

DSL が現在「書き込み専用」であることは事実です。DSL を使用してツリーを作成し、それらを Z3 に出荷することはできますが、それらを読み戻すことはできません。

Z3 ツリーを読み取る標準的な方法は、getASTKindとgetDeclKindfromを使用することZ3Contextです。結果を表すクラスは、それぞれZ3ASTKindおよびZ3DeclKindです。(ほとんどのツリーはアプリケーションであるため、後者はほとんどの情報がある場所です)。