相当于 Z3 API 中的define-fun [英] Equivalent of define-fun in Z3 API

问题描述

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

Using Z3 with the textual format, I can use define-fun to define functions for reuse later on. For example:

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

我想知道如何使用 Z3 API(我使用 F#)创建 define-fun 而不是在任何地方重复函数体.我想用它来避免重复和更轻松地调试公式.我尝试使用 Context.MkFuncDecl，但它似乎只生成未解释的函数.

I wonder how to create define-fun with Z3 API (I use F#) instead of repeating the body of the function everywhere. I want to use it to avoid duplication and debug formulas easier. I tried with Context.MkFuncDecl, but it seems to generate uninterpreted functions only.

推荐答案

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

The define-fun command is just creating a macro. Note that the SMT 2.0 standard doesn’t allow recursive definitions. Z3 will expand every occurrence of my-div during parsing time. The command define-fun may be used to make the input file simpler and easier to read, but internally it does not really help Z3.

在当前的 API 中，不支持创建宏.这并不是真正的限制，因为我们可以定义创建宏实例的 C 或 F# 函数.但是，您似乎想要显示(并手动检查)使用 Z3 API 创建的公式.在这种情况下，宏将无济于事.

In the current API, there is no support for creating macros. This is not a real limitation, since we can define a C or F# function that creates instances of a macro. However, it seems you want to display (and manually inspect) formulas created using the Z3 API. In this case, macros will not help you.

另一种选择是使用量词.您可以声明一个未解释的函数 my-div 并断言通用量化公式:

One alternative is to use quantifiers. You can declare an uninterpreted function my-div and assert the universally quantified formula:

(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 创建公式.

Now, you can create your formula using the uninterpreted function mydiv.

这种量化的公式可以用Z3来处理.实际上，处理这种量词有两种选择:

This kind of quantified formula can be handled by Z3. Actually, there are two options to handle this kind of quantifier:

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

1. Use the macro finder: this preprocessing step identifies quantifiers that are essentially defining macros and expand them. However, the expansion only happens during preprocessing time, not during parsing (i.e., formula construction time). To enable the model finder, you have to use MACRO_FINDER=true
2. The other option is to use MBQI (model based quantifier instantiation). This module can also handle this kind of quantifier. However, the quantifiers will be expanded on demand.

当然，求解时间可能在很大程度上取决于您使用的方法.例如，如果您的公式与 mydiv 的含义"无关，则无法满足，那么方法 2 可能更好.

Of course, the solving time may heavily depend on which approach you use. For example, if your formula is unsatisfiable independently of the "meaning" of mydiv, then approach 2 is probably better.

这篇关于相当于 Z3 API 中的define-fun的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！