相当于 Z3 API 中的 define-fun

Posted 2023-02-25

【中文标题】相当于 Z3 API 中的 define-fun

【英文标题】：Equivalent of define-fun in Z3 API

【发布时间】：2011-12-06 03:14:03

【问题描述】：

使用带有文本格式的 Z3，我可以使用 define-fun 来定义函数以供以后重用。例如：

(define-fun mydiv ((x Real) (y Real)) Real
  (if (not (= y 0.0))
      (/ x y)
      0.0))

我想知道如何使用 Z3 API（我使用 F#）创建 define-fun，而不是到处重复函数体。我想用它来避免重复和更容易调试公式。我尝试使用Context.MkFuncDecl，但它似乎只生成未解释的函数。

【参考方案1】：

define-fun 命令只是创建一个宏。请注意，SMT 2.0 标准不允许递归定义。 Z3 将在解析期间扩展每次出现的my-div。 命令define-fun 可用于使输入文件更简单、更易于阅读，但在内部它并不能真正帮助 Z3。

在当前的 API 中，不支持创建宏。 这不是真正的限制，因为我们可以定义创建宏实例的 C 或 F# 函数。 但是，您似乎想要显示（并手动检查）使用 Z3 API 创建的公式。在这种情况下，宏对您没有帮助。

另一种方法是使用量词。您可以声明一个未解释的函数my-div 并断言通用量化公式：

(declare-fun mydiv (Real Real) Real)
(assert (forall ((x Real) (y Real))
                (= (mydiv x y)
                   (if (not (= y 0.0))
                       (/ x y)
                       0.0))))

现在，您可以使用未解释的函数 mydiv 创建公式。

这种量化公式是Z3可以处理的。实际上，处理这种量词有两种选择：

使用宏查找器：此预处理步骤识别本质上定义宏的量词并扩展它们。但是，扩展只发生在预处理期间，而不是在解析期间（即公式构建时间）。要启用模型查找器，您必须使用 MACRO_FINDER=true 另一个选项是使用MBQI（基于模型的量词实例化）。这个模块也可以处理这种量词。但是，量词将按需扩展。

当然，求解时间可能在很大程度上取决于您使用的方法。例如，如果您的公式独立于mydiv 的“含义”而无法满足，那么方法 2 可能更好。

【讨论】：

感谢您的详细解答。使用通用量词绝对是一个巧妙的技巧。我想知道使用通用量词和未解释函数的成本。我的量化 LIA 形式的约束现在变成了量化的 UFLIA 公式。这种变化是否严重影响了 Z3 的求解时间？

是的，公式将在UFLIA 中，但它在 UFLIA 的可判定片段中。如果您使用选项 1 (MACRO_FINDER=true)，那么对性能的影响应该很小。 Z3 会将这些量词检测为宏，并将消除量词和所有出现的辅助未解释函数。因此，在预处理之后，产生的问题将在QF_LIA 中。选项 2 (MBQI) 的性能影响尚不清楚，在某些问题中 Z3 可能更快，但在其他问题中则慢得多。

谢谢！澄清一下，我的原始公式是带量词的 LIA，我想使用 LIA 量词消除来解决它们。选项 1 似乎对我来说更有吸引力，我很快就会尝试它。