Битвекторная функция Z3

Question

Я хочу решить эту проблему в решателе z3 с битовым вектором 48:

(declare-fun x () Int)
(declare-fun y () Int)
(assert (= *someNumber* (* x y)))
(assert (> x 1))
(assert (> y 1))
(check-sat)
(get-model)
(exit)

Я пытаюсь выяснить, как использовать функцию арифметики c, однако она работает не очень хорошо. Проблемы с этим (для меня) заключаются в правильном синтаксисе функций && как установить значения там.

(set-option :produce-models true)
(set-logic QF_BV)

;; Declaring all the variables
(declare-const a (_ BitVec 48))
(declare-const b (_ BitVec 48))
(declare-const c (_ BitVec 48))

;; Soft constraints to limit reuse
(assert (= c #xnumberInHex))
(assert-soft (not (= a b)))

(check-sat-using (then simplify solve-eqs bit-blast sat))
(simplify (= c (bvmul a b)) 
(simplify (bvugt a #b000000000001))  
(simplify (bvugt b #b000000000001)) 
(check-sat)
(get-model)

Любая помощь очень ценится. Синтаксис / как написать правильный битовый вектор там

Answer 1

Похоже, у вас есть почти все части, но, возможно, не совсем правильный синтаксис. Вот полное кодирование с c = 18:

(set-option :produce-models true)
(set-logic ALL)

;; Declaring all the variables
(declare-const a (_ BitVec 48))
(declare-const b (_ BitVec 48))
(declare-const c (_ BitVec 48))

(assert (= c #x000000000012)) ; 18 is 0x12 in hex
(assert (= c (bvmul a b)))

; don't allow overflow
(assert (bvumul_noovfl a b))
(assert (bvult #x000000000001 a))
(assert (bvult #x000000000001 b))

;; Soft constraints to limit reuse
(assert-soft (not (= a b)))

(check-sat)
(get-model)

Обратите внимание на использование ALL logi c и функции bvumul_noovfl, которая обнаруживает переполнение умножения на битовый вектор без знака. (Эта функция имеет спецификацию z3 c и доступна только в том случае, если для логики c выбрано значение ALL.) Поскольку вы выполняете арифметику битовых векторов c, она может быть изменена, и я думаю, это то, что вы хотели бы избежать. Явно заявляя, что мы не хотим, чтобы умножение a и b переполнялось, мы достигаем этой цели.

Для этого ввода z3 говорит:

sat
(model
  (define-fun b () (_ BitVec 48)
    #x000000000009)
  (define-fun a () (_ BitVec 48)
    #x000000000002)
  (define-fun c () (_ BitVec 48)
    #x000000000012)
)

, что правильно подставляет число 18 (записанное здесь в шестнадцатеричном виде как 12) в 2 и 9.

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

Но не бойтесь: битовая векторная логика c завершена: это означает, что z3 всегда будет способен вычислять, хотя и медленно, если вы сначала не исчерпаете память или терпение!

Answer 2

Это то, что я сделал сейчас. Это может помочь другим в будущем:

(set-option :produce-models true)
(set-logic ALL)

;; Declaring all the variables
(declare-const a (_ BitVec 48))
(declare-const b (_ BitVec 48))
(declare-const c (_ BitVec 48))

(assert (= c #x00000000affe)) 
(assert (= c (bvmul a b)))

; don't allow overflow
(assert (= c (bvumul_noovfl a b)))
(assert (bvult #x000000000001 a))
(assert (bvult a c))
(assert (bvult #x000000000001 b))
(assert (bvult b c))

;; Soft constraints to limit reuse
(assert-soft (not (= a b)))

(check-sat)
(get-model)

Я добавил еще два утверждения, чтобы убедиться, что a или b не превышает c (ввод в шестнадцатеричном формате), в этом примере я использовал «affe», это 45054 в десятичном виде. он должен работать и для больших.

Вывод:

sat
(model 
  (define-fun b () (_ BitVec 48)
    #x00000000138e)
  (define-fun a () (_ BitVec 48)
    #x000000000009)
  (define-fun c () (_ BitVec 48)
    #x00000000affe)
)

hex: 138e * 9 = affe

de c: 5006 * 9 = 45054

Надеюсь, что это поможет кому-то еще в будущем.