在Z3的API定义，相当于乐趣 [英] Equivalent of define-fun in Z3 API

问题描述

使用Z3的文本格式，我可以使用定义乐趣稍后定义重用的功能。例如：

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＃），而不是到处重复函数体。我想用它来避免重复和调试公式更容易。我试着用 Context.MkFuncDecl ，但它似乎产生uninter preTED函数只。

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.

推荐答案

的定义乐趣命令只是创建宏。注意，SMT 2.0标准不允许递归定义。
Z3将解析时间内展开我-DIV 的每次出现。
命令定义乐趣可用于使输入文件更简单，更易于阅读，但是在内部它并没有真正帮助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.

一替代方法是使用量词。你可以声明uninter preTED功能我-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))))

现在，您可以使用uninter preTED函数来创建公式 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. 使用宏取景器：此preprocessing步识别基本上是定义宏量词和扩大。然而，扩张仅在preprocessing时有发生，而不是解析（即式建设期）期间。为了使模型取景器，你必须使用 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定义，相当于乐趣的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！