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

在Z3 api中，FuncDecl有一个DeclKind（）来指示它是否是重写规则。但如何在Z3 java API中创建重写规则？如何在Z3 Java API中编写公理？

2013-03-05 Betsy

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

来源

2013-03-06 01:28:31

正如Leo所说，直接不支持自定义重写规则。但是，在Z3内部实现特定的重写器作为一种策略，或者使用Expr.update（）函数从外部实现它是相当简单的。请参阅http://stackoverflow.com/questions/15236450/substitution-function-symbols-in-z3-formulas，其中Leo解释了如何在Python中执行此操作。 – 2013-03-06 13:08:14

真的很有帮助！ – Betsy 2013-03-07 03:52:13

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

回答

相关问题