Z3 Java API 定义一个函数

Question

我需要你的帮助，用 Z3 Java API 定义一个函数。我尝试解决这样的问题（在 z3.exe 进程中工作正常）：

(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Bool)

(define-fun max2 ((x Real) (y Real)) Real (ite (<= x y) y x))

(assert (and (>= a 0.0) (<= a 100.0)))
(assert (or (= (max2 (+ 100.0 (* (- 1.0) a)) (/ 1.0 1000.0)) 0.0) c (not (= b 0.0))))

(check-sat-using (then simplify bit-blast qfnra))
(get-model)

此 smt 文件的结果是：

sat
(model
  (define-fun a () Real
    1.0)
  (define-fun c () Bool
    false)
  (define-fun b () Real
    1.0)
)

现在的问题是：没有选择，用 java API 定义一个函数。在另一篇文章中（相当于 Z3 API 中的define-fun），我注意到在 java API 中使用了以下语句：

(declare-fun max2 (Real Real) Real)
(assert (forall ((y Real) (x Real)) (= (max2 y x) (ite (<= x y) y x))))

所以我在我的 smt 文件中替换了(define-fun max2 ((x Real) (y Real)) Real (ite (<= xy) yx))并再次启动了 z3.exe 进程。结果如下：

unknown
(model
  (define-fun b () Real
    0.0)
)

因此，如您所见，不再有可满足的结果。在 java 中翻译它，将得到相同的结果UNKNOWN。

任何想法，我能做什么？

Answer 1

没有与函数定义等效的东西，因为它们不是必需的，就像 Def​​ine-fun 宏一样。在 API 中要做的等效事情是为函数构建一个表达式，然后对于该函数的每个应用程序，只需用参数值替换输入值，例如，通过使用 Expr.Substitute。

就像 Leo 在您引用的帖子中提到的那样，可以使用量词来达到此目的，但求解器通常会放弃并返回，unknown因为它认为公式太难求解。我们可以通过使用宏查找器（参见引用的帖子）来解决这个问题，它将准确识别这种宏。