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

Question

我试着举一个简单的例子来检查固定数组中的字节。我也读了Z3的教程，但我无法得到它的工作。这里是5月情形：

我有固定字节数组16的长度：T（16）

我具备这些条件的检查：

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

它意味着从T(16)采取字节添加1，使AND与0x0F，并将结果编号分配给变量A。 现在检查上的位置AT(A)是否是0x76。 A也可以在值0x01和0x7F之间。

这些条件对数组中的更多位置重复，但我需要为第一种情况才能使用它。这样做的目标是：根据给定的等式在固定数组中找到已知字节的正确顺序。

我试着用这个脚本，但不起作用。

Error: operator is applied to arguments of the wrong sort.

(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，AND0x0F = 0x05，上T(0x05)应值0x76。

谢谢。

Answer 1

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

此外，这将工作。

你可能会发现不使用数组，而只使用bitvector的速度更快。这是可以尝试的。