Я хочу определить функцию, которая принимает битовый вектор и возвращает истину, если биты в определенной позиции удовлетворяют некоторым значениям.Например: мне нужно вернуть true, если bitvector равен 1x00x01x, где x обозначает неважно.
Моя текущая реализация:
(define-fun function_i ((i (_ BitVec 8))) Bool
(and true
(= #b1 ((_ extract 1 1) i))
(= #b0 ((_ extract 2 2) i))
(= #b0 ((_ extract 4 4) i))
(= #b0 ((_ extract 5 5) i))
(= #b1 ((_ extract 7 7) i))
)
)
Это для одной переменной и может быть много переменныхс 32 размерами битвекторов.Я беспокоюсь, что такого рода реализация замедляет z3.Будет ли функция извлечения замедлять решатель?Есть ли лучший способ реализовать это?