функция для получения полубайтов с использованием Z3 и теории битового вектора

Я пытаюсь немного узнать о z3 и теории битовых векторов. Я намерен создать функцию для получения полубайта из позиции битового вектора

Этот код возвращает кусочек:

(define-fun g_nibble(
   (l ( _ BitVec 12))
   (idx (Int))
) ( _ BitVec 4)

(ite
    (= idx 1) ((_ extract 11 8) l)
    (ite
        (= idx 2) ((_ extract 7 4) l)
        (ite
            (= idx 3) ((_ extract 3 0) l)     
            (_ bv0 4)
        )
    )
))

проблема в том, что я хочу избежать многократных вызовов ite. Я попытался заменить ((_ extract 3 0) l) чем-то вроде ((_ extract (+ 4 idx) idx l), но это не сработало.

Спасибо

P.S: Идея состоит в том, чтобы использовать z3 из командной строки (без использования какой-либо библиотеки).


z3 smt sat-solvers
person user4547829    schedule 10.02.2015    source источник

Ответы (1)


arrow_upward
1
arrow_downward

Функция извлечения принимает в качестве аргументов только числа, а не произвольные выражения. Однако мы можем сдвинуть выражение в одном направлении, а затем извлечь первые или последние четыре бита, например по линиям

((_ extract 11 8) (bvshl l (bvmul idx four)))

(где idx и четыре - это битовые векторные выражения размера 12).

person Christoph Wintersteiger    schedule 10.02.2015
comment
спасибо, я полагаю, что idx должен быть битовым вектором, потому что обе теории (Int и битовый вектор) не могут использоваться вместе, верно? - person user4547829; 10.02.2015
comment
Да, индекс должен быть битовым вектором. Эти теории можно использовать вместе, но для функции bvshl требуется битовый вектор. - person Christoph Wintersteiger; 11.02.2015