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.26s，示例2的运行时间为0.35s，尽管唯一的区别是在函数afun中，我要么直接调用常量，要么将它们作为参数传递。我还注意到，有时会发生相反的情况(直接调用常量比将其作为参数传递更快(。

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

Answer 1

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