Z3 可以应用位宽缩减技术来解决位向量等价吗？

编程问答 2022-05-27

问题描述

在 program synthesis task 期间，我遇到了以下等价，它基于混合布尔算术逻辑，而且我似乎无法在合理的时间内（几秒或几秒）用 Z3 证明分钟）。我正在遵循反例驱动方法 (CEGIS)，将原始表达式和综合候选提供给不同查询：如果没有找到反例，则综合是正确的。

(set-logic QF_BV)
(declare-fun y () (_ BitVec 64))
(declare-fun x () (_ BitVec 64))
(assert (let ((a!1 (bvsub (bvsub (bvsub x #x0000000000000002) y)
                  (bvshl (bvor x (bvnot y)) #x0000000000000001))))
(let ((a!2 (bvmul (bvand (bvxor a!1 x) (bvnot y))
                  (bvand y (bvnot (bvxor a!1 x))))))
(let ((a!3 (bvadd (bvmul (bvor (bvxor a!1 x) y) (bvand (bvxor a!1 x) y)) a!2)))
  (distinct a!3 (bvmul y y))))))
(check-sat)

我知道对于减少的位宽位向量（例如 8 或 16）保持良好的等效性，所以我想知道 Z3 是否使用任何技术来首先证明查询的位宽减少版本，然后将结果扩展到全角版本。

我尝试了 Z3 bv-size-reduction 策略，但它似乎不符合我的要求，因为它旨在减少常量的大小，而不是符号位向量的大小。此外，加速量化比特向量解决位宽减少和扩展论文的implementation似乎不适用于这种特定情况，因为没有有用的反模型生成，保持问题的大小不变。

我不是 SAT/SMT 人，因为我几乎不使用 Z3 之类的工具作为黑匣子来解决综合问题，所以我想知道：

  • 我能做些什么来减少位向量的位宽、证明减少的查询并将结果扩展到全宽查询？
  • 是否还有其他可行的方法来证明上述查询的不可满足性？

解决方法

暂无找到可以解决该程序问题的有效方法，小编努力寻找整理中！

如果你已经找到好的解决方法，欢迎将解决方案带上本链接一起发送给小编。

小编邮箱:dio#foxmail.com (将#修改为@）

smttheorem-provingz3