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

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

0 голосов
/ 07 мая 2020

Я пишу кодировку 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

Q:

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

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

1 Ответ

1 голос
/ 07 мая 2020

SMTLib действительно определяет bv2nat и nat2bv:

bv2nat, который принимает битовый вектор b: [0, m) → {0, 1} с 0 

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

o nat2bv [m], где 0 

   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 - это определенно c «знак» битового вектора; он не присваивает знак данному вектору, но вместо этого предоставляет подписанные и неподписанные версии операторов arithmeti c, когда они различны. (Например, существует только одна версия сложения, поскольку не имеет значения, есть ли у вас битовые векторы со знаком или без знака для этой операции, но для сравнения мы получаем bvult, bvslt et c.)

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

(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 не позволяет пользователям определять функции size-polymorphi c. Однако вы можете сгенерировать столько таких функций, сколько захотите, объявив их на лету, или просто сгенерируйте соответствующие выражения, когда это необходимо.

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

...