在Z3 api中，FuncDecl有一个DeclKind()来指示它是否是重写规则。但是如何在 Z3 java API 中创建重写规则呢？
最佳答案
我不确定我是否正确理解了你的问题。
您指的是Z3_OP_PR_REWRITE吗？
如果是这种情况，则这是用于注释 Z3 证明中重写规则证明步骤的声明类型。它对应于this article中描述的重写步骤。 (第 3.2 节)。
我们不应该将这种声明类型与用户定义的重写规则混淆。
关于java - 如何在Z3 Java API中编写公理？，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/15215603/