java - 如何在 Z3 Java API 中编写公理？

Question

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

Answer 1

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