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

Question

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

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

Answer 1

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

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

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