z3 - API を介して Z3 式の構造を照会またはアクセスする方法はありますか

Question

F# からマネージ API にアクセスしています。ctx.MkFalse、MkImplies、MkMul などを使用して Z3 式を作成できますが、Z3 式をトラバースしてその構造を見つけるにはどうすればよいですか? e.Op や e.IsFalse、e.IsImplies などのようなものはありますか?

Answer 1

Expr.csのドキュメントをご覧ください。

式をトラバースする単純な F# の例を次に示します。

let traverse (expr: Expr) =
    printfn "num args: %O" expr.NumArgs
    printfn "children: %A" expr.Args
    printfn "1st child: %O" expr.Args.[0]
    printfn "2nd child: %O" expr.Args.[1]
    printfn "operator: %O" expr.FuncDecl
    printfn "op name: %O" expr.FuncDecl.Name

Exprクラスは、式の構造を発見するために必要なIsTrue、IsAnd、isImplies などを含むすべての Term Kind テストも公開します。F# では、一連のアクティブ パターンを定義する必要があります。

let (|True|_|) (expr: Expr) = if expr.IsTrue then Some() else None
let (|False|_|) (expr: Expr) = if expr.IsFalse then Some() else None

let (|And|_|) (expr: Expr) = if expr.IsAnd then Some expr.Args else None
let (|Or|_|) (expr: Expr) = if expr.IsOr then Some expr.Args else None
let (|Not|_|) (expr: Expr) = if expr.IsNot && expr.NumArgs = 1u 
                             then Some(expr.Args.[0]) else None

let (|Iff|_|) (expr: Expr) = if expr.IsIff && expr.NumArgs = 2u 
                             then Some(expr.Args.[0], expr.Args.[1]) else None
let (|Implies|_|) (expr: Expr) = if expr.IsImplies && expr.NumArgs = 2u 
                                 then Some(expr.Args.[0], expr.Args.[1]) else None

そのため、再帰的な方法であっても、パターン マッチングによって式の構造を簡単にクエリできます。

match e with
| True -> (* boolean literal *)
| False -> (* boolean literal *)
| And es -> (* query es; possibly by pattern matching *)
| Or es -> (* query es; possibly by pattern matching *)
| Not e' -> (* query e; possibly by pattern matching *)
| Iff(e1, e2) -> (* query e1, e2; possibly by pattern matching *)
| Implies(e1, e2) -> (* query e1, e2; possibly by pattern matching *)
| _ -> (* Not a boolean expression; do something else *)