z3 运行时：直接调用常量 VS 作为参数传递

Question

我在 z3 中遇到了一些异常的运行时行为，我想问一下为什么会这样：

示例 1：

(set-info :smt-lib-version 2.6)

(set-info :status unknown)
(define-sort FPN () (Float32))

(declare-const a1 FPN)
(assert (fp.eq a1 ((_ to_fp 8 24) RNE 1)))
(declare-const a2 FPN)
(assert (fp.eq a2 ((_ to_fp 8 24) RNE -1)))
(declare-const a3 FPN)
(assert (fp.eq a3 ((_ to_fp 8 24) RNE 0.5)))

(define-fun afun ((x FPN) (a1Param FPN) (a2Param FPN) (a3Param FPN)) FPN (fp.mul RNE (fp.add RNE (fp.mul RNE a1Param x) a2Param) a3Param ))

(assert
  (forall ((x0 FPN)) (not (fp.geq (afun x0 a1 a2 a3) x0)))
)

(check-sat)
(get-model)
(exit)

示例 2：

(set-info :smt-lib-version 2.6)

(set-info :status unknown)
(define-sort FPN () (Float32))

(declare-const a1 FPN)
(assert (fp.eq a1 ((_ to_fp 8 24) RNE 1)))
(declare-const a2 FPN)
(assert (fp.eq a2 ((_ to_fp 8 24) RNE -1)))
(declare-const a3 FPN)
(assert (fp.eq a3 ((_ to_fp 8 24) RNE 0.5)))

(define-fun afun ((x FPN)) FPN (fp.mul RNE (fp.add RNE (fp.mul RNE a1 x) a2) a3 ))

(assert
  (forall ((x0 FPN)) (not (fp.geq (afun x0) x0)))
)

(check-sat)
(get-model)
(exit)

示例 1 的运行时间约为 0.26 秒，示例 2 的运行时间约为 0.35 秒，尽管唯一的区别是在函数 afun 中我要么直接调用常量，要么将它们作为参数传递。我还注意到有时会发生相反的情况（直接调用常量比将其作为参数传递更快）。

我不明白为什么会这样，所以想在这里问一下。非常感谢您的回复！

Answer 1

这些问题被重写为布尔逻辑，fp.mul 简直难以分析，就像许多其他理论中的乘法一样。您基本上受 SAT 求解器的支配，它使用各种启发式方法快速解决许多问题，但对于任何给定的问题，预测它的行为并不容易。输入的微小变化导致求解时间发生巨大变化是很常见的。您可以运行 Z3 和 -v:10 查看应用了哪些策略并查看 SAT 求解器的一些统计数据。

z3 运行时：直接调用常量 VS 作为参数传递

z3 runtime: Calling constant directly VS passing as parameter

z3