Z3 Java API：FuncDecl 和 Expr

Question

我有一个现有的 smt2 文件，并使用 z3 java api 解析了这个并解决了问题。但是我有一个关于如何将 FuncDecl 转换为 Expr 的问题，因为我想通过使用 z3 java api 构建一些简单的公式。由于我的原始公式纯粹是用 smt2 文本文件编写的，并且所有内容都被解析为单个 BoolExpr。现在，我成功地提取了常量，并且需要用新的公式来操作它们。我该怎么做？基本上，我正在寻找的是如何从 FuncDecl 构建 Expr 或者有没有办法可以将它转换为 Expr？有没有官方的java api文档可用？我知道有一个使用z3 java api的例子，但是在这么大的例子中寻找具体的api描述是相当痛苦的。

Answer 1

FuncDecl 是函数声明，它们不能直接转换为表达式，但它们表示的函数可以应用于（某些参数）以产生表达式。这就是FuncDecl.apply(...) 所做的。常量当然是一种特殊情况，函数不接受任何参数。