使用带有文本格式的 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
,但它似乎只生成未解释的函数。
该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 可能更好。