有没有办法通过 API 查询或访问 Z3 表达式的结构 [英] Is there a way of querying or accessing the structure of a Z3 expression via the API
问题描述
我正在从 F# 访问托管 API.我可以使用 ctx.MkFalse、MkImplies、MkMul 等构造 Z3 表达式,但我如何遍历 Z3 表达式以发现其结构?是否有类似 e.Op 或 e.IsFalse、e.IsImplies 等的东西.
I am accessing the managed API from F#. I can construct Z3 expressions using ctx.MkFalse, MkImplies, MkMul etc. but how do i traverse a Z3 expression to discover its structure? Is there something like e.Op or e.IsFalse, e.IsImplies etc.
推荐答案
您应该查看 Expr.cs.
这是一个遍历表达式的简单 F# 示例:
Here is a simple F# example that traverses through an expression:
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 等,这是发现表达式结构所必需的.在 F# 中,您应该定义一组活动模式:
Expr
class also exposes all Term Kind Tests including IsTrue, IsAnd, isImplies, etc which are necessary to discover the structure of an expression. In F# you should define a set of active patterns:
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
这样您就可以通过模式匹配轻松查询表达式的结构,即使是以递归方式:
So that you can easily query an expression's structure by pattern matching, even in a recursive way:
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 *)
这篇关于有没有办法通过 API 查询或访问 Z3 表达式的结构的文章就介绍到这了,希望我们推荐的答案对大家有所帮助,也希望大家多多支持IT屋!