Find centralized, trusted content and collaborate around the technologies you use most.
Teams
Q&A for work
Connect and share knowledge within a single location that is structured and easy to search.
在 Z3 api 中,FuncDecl 有一个 DeclKind() 来指示它是否是重写规则。但是如何在 Z3 java API 中创建重写规则呢?
我不确定我是否正确理解了您的问题。你指的是Z3_OP_PR_REWRITE?如果是这种情况,这是用于在 Z3 证明中注释重写规则证明步骤的声明类型。它对应于本文(第 3.2 节)中描述的重写步骤。我们不应将此声明类型与用户定义的重写规则混淆。
Z3_OP_PR_REWRITE