时间戳

首页 > 解决方案 > z3运行时：直接调用常量VS作为参数传递

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

问题描述

我在 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 中我要么直接调用常量，要么将它们作为参数传递。我还注意到有时会发生相反的情况（直接调用常量比将其作为参数传递要快）。

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

标签： z3

解决方案

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

推荐阅读