1

在 Z3 api 中,FuncDecl 有一个 DeclKind() 来指示它是否是重写规则。但是如何在 Z3 java API 中创建重写规则呢?

4

1 回答 1

1

我不确定我是否正确理解了您的问题。你指的是Z3_OP_PR_REWRITE?如果是这种情况,这是用于在 Z3 证明中注释重写规则证明步骤的声明类型。它对应于本文(第 3.2 节)中描述的重写步骤。我们不应将此声明类型与用户定义的重写规则混淆。

于 2013-03-06T01:28:31.267 回答