z3 игнорирует некоторые из моих ограничений?

Question

Stackru-ERS (?),

Я играю с z3 и пытаюсь решить следующие ограничения:

(declare-const A (_ BitVec 32))
(declare-const B (_ BitVec 32))
(declare-const C (_ BitVec 32))
(declare-const D (_ BitVec 32))
(declare-const E (_ BitVec 32))
(declare-const F (_ BitVec 32))

(assert (<= A #xFFFFFFFF))
(assert (<= B #xFFFFFFFF))
(assert (<= C #xFFFFFFFF))


(assert (> A #x00000000))

;(Commented) Restriction #1 (assert (> B #x00000000))
(assert (> C #x00000000))

(assert (= D (bvand (bvmul (bvmul A B) #x00000008) #xFFFFFFFF) ))
(assert (<= D #xFFFFFFFF))

(assert (= E (bvand (bvmul (bvmul A C) #x00000008) #xFFFFFFFF)))
(assert (<= D E))

(assert (= F (bvand (bvmul A #x00000008) #xFFFFFFFF)))    

;(Uncommented) Restriction #2
(assert (> (bvand (bvmul F B) #xFFFFFFFF) D))

(assert (< (bvand (bvmul A B) #xFFFFFFFF) #x7FFFFFFF))
(assert (< (bvand (bvmul A C) #xFFFFFFFF) #x7FFFFFFF))


(assert (< D #x01000000))

(check-sat)

(get-value(A))
(get-value(B))
(get-value(C))
(get-value(D))
(get-value(F))

У меня есть некоторые проблемы с этими ограничениями: а) Первая проблема заключается в том, что z3 игнорирует "Ограничение № 2"

(assert (> (bvand (bvmul F B) #xFFFFFFFF) D))

я получаю следующие значения:

A: #x000070e0
B: #x0000000a
C: #x00000014
D: #x00234600
F: #x00038700

и F*B = D, несмотря на ограничение.

б) если я раскомментирую "Ограничение № 1"

(assert (> B #x00000000))

Я получаю следующий результат:

A: #x0000a000
B: #x00000007
C: #x00000000

это ошибка интерфейса "стул - клавиатура"? Что я делаю неправильно?

Запустите это на Z3 онлайн.

Заранее спасибо!

Answer 1

Для сравнения бит-векторов вы всегда должны использовать соответствующие варианты со знаком / без знака: bvult, bvugt, bvule, bvuge для неподписанных и bvslt, bvsgt, bvsle, bvsge для подписи. Использование <, > и т.д. не действует. Таким образом, ваши "ограничения" на самом деле просто игнорируются. Если я запускаю ваш тест в командной строке, я получаю следующий вывод:

(error "line 8 column 24: Sort mismatch at argument #1 for function (declare-fun <= (Int Int) Bool) supplied sort is (_ BitVec 32)")
(error "line 9 column 24: Sort mismatch at argument #1 for function (declare-fun <= (Int Int) Bool) supplied sort is (_ BitVec 32)")
(error "line 10 column 24: Sort mismatch at argument #1 for function (declare-fun <= (Int Int) Bool) supplied sort is (_ BitVec 32)")
(error "line 13 column 23: Sort mismatch at argument #1 for function (declare-fun > (Int Int) Bool) supplied sort is (_ BitVec 32)")
(error "line 16 column 24: Sort mismatch at argument #1 for function (declare-fun > (Int Int) Bool) supplied sort is (_ BitVec 32)")
(error "line 19 column 24: Sort mismatch at argument #1 for function (declare-fun <= (Int Int) Bool) supplied sort is (_ BitVec 32)")
(error "line 22 column 15: Sort mismatch at argument #1 for function (declare-fun <= (Int Int) Bool) supplied sort is (_ BitVec 32)")
(error "line 27 column 44: Sort mismatch at argument #1 for function (declare-fun > (Int Int) Bool) supplied sort is (_ BitVec 32)")
(error "line 29 column 52: Sort mismatch at argument #1 for function (declare-fun < (Int Int) Bool) supplied sort is (_ BitVec 32)")
(error "line 30 column 52: Sort mismatch at argument #1 for function (declare-fun < (Int Int) Bool) supplied sort is (_ BitVec 32)")
(error "line 33 column 23: Sort mismatch at argument #1 for function (declare-fun < (Int Int) Bool) supplied sort is (_ BitVec 32)")
sat
((A #x00000000))
((B #x00000000))
((C #x00000000))
((D #x00000000))
((F #x00000000))

Я не уверен, почему "онлайн" решатель не так жалуется.