Z3：使用位向量时出现 iz3proof_itp::proof_error 和 iz3translation::unsupported 错误

Question

我在 Z3 的最新（不稳定分支）版本上使用内置插值功能。它适用于包含整数的 SMT2 公式。但是，它确实为以下 SMT2 程序 -

抛出 iz3proof_itp::proof_error 和随后的 iz3translate::unsupported error（见下文）

(set-option :produce-models true)
(set-logic QF_AUFBV)
(declare-fun a () (_ BitVec 32))
(declare-fun b () (_ BitVec 32))
(declare-fun x1 () (_ BitVec 32))
(declare-fun x2 () (_ BitVec 32))
(declare-fun x3 () (_ BitVec 32))
(declare-fun y1 () (_ BitVec 32))
(declare-fun y2 () (_ BitVec 32))
(compute-interpolant
 (= a (_ bv0 32))
 (= b (bvneg (_ bv2 32)))
 (= x1 (_ bv1 32))
 (= y1 (_ bv0 32))
 (= x2 (bvadd x1 a))
 (= x3 (bvadd x2 b))
 (= y2 (bvadd y1 a))
 (bvsge x3 (_ bv0 32))
)

我在rise4fun上试过在线版，效果不错。所以经过一些调试，我发现错误是从文件 iz3proof_itp.cpp 中的函数 find_congruence_position 内部抛出的。

所以我对函数进行了以下简单（可能是危险的）更改以至少暂时处理 proof_error -

在第 2431 行更改 if(x == arg(arg(con,0),i) && (y == arg(arg(con,1),i))

到if((x == arg(arg(con,0),i) && (y == arg(arg(con,1),i))) || (y == arg(arg(con,0),i) && (x == arg(arg(con,1),i))))

我简单地将条件与它的 x 和 y 互换的副本进行或运算 - 我发现 x 和 y 有时会互换它们的值，这可能是由于某些证明技术。

这确实解决了问题，我发现在计算插值时使用等式和非等式，以及 bvadd 或 bvneg 和 BitVecs 工作。例如，以下文件有效 -

(set-option :produce-models true)
(set-logic QF_AUFBV)
(declare-fun a () (_ BitVec 32))
(declare-fun b () (_ BitVec 32))
(compute-interpolant
 (= a (_ bv0 32))
 (= b (bvadd a (_ bv1 32)))
 (= b (_ bv0 32))
)

但后来我尝试使用关系运算符，如 bvsgt 或 bvsge，它引发了一个新错误 -

terminate called after throwing an instance of 'iz3translation::unsupported'

我仔细研究了一下，发现导致问题的表达式是 -

(not ((_ bit2bool 2) x2)) - 它被指定为 PR_TH_LEMMA 类型和 UNKNOWN_THEORY 类型。好像不支持这样的操作

由于在线版本可以使用，我想知道是否可以获取该版本。我在 Whosebug 上阅读了之前的问题和答案，我有点困惑。有人说不支持 BitVec 理论（虽然这些帖子很旧），但是在线版本如何工作？还是我做错了什么？非常感谢任何帮助。

Answer 1

实际上，不支持位向量运算的插值。有趣的是它适用于网络版本。然而，那个版本很旧，我认为它早于 Z3 的源代码可用版本。我可以想到它起作用的两个可能原因：

1) 该版本的插值 Z3 使用 "foci" 证明器作为备份。每当它遇到它不理解的证明部分时，它就会将该部分打包为一个引理，并使用 foci 对其进行反驳。当前版本没有使用foci（源码中没有的第三方工具），完全依赖Z3生成的证明。

2) 旧版本可能以不同的方式进行位爆破。如果所有非局部证明步骤都是纯命题的（仅使用解析规则），那么很容易计算插值。

然而，据我所知，从高效位向量求解器（使用所有已知的预处理技巧）计算插值是一个悬而未决的问题。

Z3：使用位向量时出现 iz3proof_itp::proof_error 和 iz3translation::unsupported 错误

Z3: iz3proof_itp::proof_error and iz3translation::unsupported error when using bitvectors

z3