Простой массив байтов в 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 в позиции 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.

Кроме того, это сработает.

Возможно, вы обнаружили, что не используете массивы, а только битвекторы быстрее. Это то, с чем можно поэкспериментировать.