Какие операторы преобразования доступны в Z3 и CVC4 для битовых векторов?

Я пишу BV-кодировку проблемы, которая требует преобразования некоторых Int в BitVec и наоборот.

В mathsat/optimathsat можно использовать:

((_ to_bv BITS) <int_term>) ; Int => BitVec
(sbv_to_int <bv_term>)      ; Signed BitVec => Int
(ubv_to_int <bv_term>)      ; Unsigned BitVec => Int

В z3 можно использовать:

((_ int2bv BITS) <int_term>) ; Int => BitVec
???                          ; Signed BitVec => Int   
(bv2int <bv_term>)           ; Unsigned BitVec => Int

В CVC4 можно использовать:

((_ int2bv BITS) <int_term>) ; Int => BitVec
???                          ; Signed BitVec => Int   
???                          ; Unsigned BitVec => Int

Вопрос:

  • есть ли у z3 функция bv2int для Signed BitVec? (Похоже, нет.)
  • CVC4 вообще имеет какую-либо функцию bv2int? (Понятия не имею.)
  • есть ли место, где задокументированы эти функции преобразования? (Похоже, что на веб-странице SMT-LIB, посвященной логикам/теориям, нет никакой информации о них.)

примечание. Я ограничен текстовым интерфейсом SMT-LIB (без решения API).


z3 smt optimathsat cvc4 mathsat
person Patrick Trentin    schedule 07.05.2020    source источник

Ответы (1)


arrow_upward
1
arrow_downward

SMTLib определяет bv2nat и nat2bv:

bv2nat, который принимает битовый вектор b: [0, m) → {0, 1}, где 0 ‹ m, и возвращает целое число в диапазоне [0, 2^m), и определяется следующим образом:

   bv2nat(b) := b(m-1)*2^{m-1} + b(m-2)*2^{m-2} + ⋯ + b(0)*2^0

o nat2bv[m] с 0 ‹ m, который принимает неотрицательное целое число n и возвращает (уникальный) битовый вектор b: [0, m) → {0, 1} такой, что

   b(m-1)*2^{m-1} + ⋯ + b(0)*2^0 = n rem 2^m

См. здесь: http://smtlib.cs.uiowa.edu/theories-FixedSizeBitVectors.shtml

И CVC4, и z3 должны поддерживать эти две операции. (Если нет, вы должны сообщить об этом им!)

Для всего остального вам придется сделать математику самостоятельно. SMTLib явно не зависит от «знака» битового вектора; он не приписывает знак данному вектору, но вместо этого предоставляет подписанную и беззнаковую версии арифметических операторов, когда они различны. (Например, существует только одна версия сложения, поскольку не имеет значения, есть ли у вас битовые векторы со знаком или без знака для этой операции, но для сравнения мы получаем bvult, bvslt и т. д.)

Из этих двух функций вы можете определить другие варианты. Например, чтобы сделать подписанный битовый вектор x длины 8 целым числом, я бы пошел:

(ite (= ((_ extract 7 7) x) #b0)
           (bv2nat ((_ extract 6 0) x))
        (- (bv2nat ((_ extract 6 0) x)) 128)))

То есть вы проверяете верхний бит x:

  • Если это 0, то вы просто конвертируете его, используя bv2nat. (Вы можете пропустить верхний бит, поскольку вы знаете, что он равен 0, в качестве небольшой оптимизации.)

  • Если верхний бит равен 1, то значение — это то, что вы преобразовали, пропустив верхний бит, и вы вычли из него 128 (= 2 ^ (8-1)). Как правило, вы вычитаете 2 ^ (m-1), где m — размер битового вектора.

Одна ошибка: вы не можете создать функцию SMTLib, которая сделает это за вас для всех размеров битового вектора. Это связано с тем, что SMTLib не позволяет пользователям определять полиморфные по размеру функции. Однако вы можете генерировать столько таких функций, сколько хотите, объявляя их на лету, или просто генерировать соответствующие выражения, когда это необходимо.

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

person alias    schedule 07.05.2020
comment
Спасибо! Я надеялся на какое-то более прямое решение, потому что именно по указанным вами причинам необходимо создавать экземпляр специальной операции преобразования для каждого размера BV. Давайте начнем собирать некоторые махинации с регулярными выражениями.. - person Patrick Trentin; 07.05.2020