14

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

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

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

4

1 回答 1

15

该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可以处理这种量化公式。实际上，有两种方法可以处理这种量词：

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

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

于 2011-10-12T18:53:47.323 回答