Есть несколько сообщений, касающихся преобразования битовых векторов в целые числа (и наоборот) в z3. См., Например, здесь, здесь и здесь.
В документации говорится, что Z3_mk_bv2int не интерпретируется:
«... Эта функция, по сути, считается неинтерпретируемой. Поэтому нельзя ожидать, что Z3 точно отразит семантику этой функции при решении ограничений с помощью этой функции ...»
Однако я не смог найти простого примера, где он не соответствует ожидаемой семантике. Например, всякий раз, когда я использую такие запросы:
(declare-const s String)
(declare-const someBitVec10 (_ BitVec 10))
(assert (= s "74g\x00!!#2#$$"))
(assert (str.in.re (str.at s (bv2int someBitVec10)) (re.range "1" "3")))
(check-sat)
(get-value (s someBitVec10))
Я получаю правильный ответ (в индексе должно быть 7, и это так)
sat
((s "74g\x00!!#2#$$")
(someBitVec10 #b0000000111))
Может ли кто-нибудь предоставить простой пример, когда z3 bv2int и / или int2bv терпят неудачу ?? Благодарность!
