Я использую Z3 версии 3.0. Я хочу присвоить значение переменной битового вектора, как показано ниже. Но Z3 сообщает об ошибке «недопустимое приложение функции, несоответствие сортировки аргумента в позиции 2 в строке 3».
Кажется, моя константа #x0a неверна? Как я могу это исправить?
Спасибо
(set-logic QF_BV)
(declare-fun a () (_ BitVec 32))
(assert (= a #x0a))
(check-sat)
В стандарте SMT-LIB 2.0 #x0a — это битовый вектор размера 8. Вы получаете ошибку несоответствия сортировки, потому что константа a — это битовый вектор размера 32. Вы можете избежать сообщения об ошибке типа/сортировки, переписав свой пример следующим образом:
(set-logic QF_BV)
(declare-fun a () (_ BitVec 32))
(assert (= a #x0000000a))
(check-sat)
SMT-LIB также поддерживает литералы битового вектора в форме (_ bv[num] [size]), где [num] — десятичная запись, а [size] — размер битового вектора. Таким образом, вы также можете записать литерал битового вектора #x0000000a как (_ bv10 32).
Кстати, SMT-LIB также поддерживает литералы битовых векторов в двоичной записи. Например, #b010 — это битовый вектор размера 3.
