Z3中的简单字节数组（SMT）

Question

我尝试做一个简单的例子来检查固定数组中的字节。我还阅读了 Z3 教程，但无法正常工作。这是可能的情况：

我有长度为 16 的固定字节数组：T(16)

我有这些条件要检查：

A = (T(16) + 1) And 0x0F
T(A) = 0x76
0x01 <= A <= 0x7F

意思是从T(16) 中取字节加上1，使AND 和0x0F，并将结果编号分配给变量A。 现在检查数组T 中位置A T(A) 是否是数字0x76。 A 也可以介于值 0x01 和 0x7F 之间。

这些条件在数组中的更多位置重复，但我需要让它只在第一种情况下工作。这样做的目的是：根据给定的方程找到固定数组中已知字节的正确顺序。

我用这个脚本试了一下，但没有用。

错误：运算符应用于错误排序的参数。

(declare-const t (Array Int Int))
(declare-const a Int)
; A = (t(16) + 1) And 0x0F
(assert (= a (bvand (+ (select t 16) 1) #x0F)))
; t(A) = 0x76
(assert (= (select t a) #x76))
(check-sat)
;(get-model)

例子：

T(16) 上的值是 0x14，+ 1 = 0x15，AND 0x0F = 0x05，T(0x05) 上的值应该是 0x76。

谢谢。

Answer 1

你不能像那样混合整数和位向量，也没有必要。在所有情况下都使用大小为 8 的位向量。不要使用Int。

除此之外，这将起作用。

您可能会发现不使用数组而只使用位向量会更快。这是要试验的东西。