相当于Z3 API中的define-fun

Question

使用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,但它似乎只生成未解释的函数.

Answer 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处理.实际上,有两种方法可以处理这种量词:

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

当然,解决时间可能在很大程度上取决于您使用的方法.例如,如果您的公式不能满足"意义" mydiv,那么方法2可能更好.