Смешивание вещественных чисел и бит-векторов

Question

У меня есть два скрипта SMT2-Lib, использующие реалы, которые морально эквивалентны. Разница лишь в том, что один использует битовые векторы, а другой - нет.

Вот версия, которая использует как реалы, так и битовые векторы:

; uses both reals and bit-vectors
(set-option :produce-models true)
(define-fun s2 () Real (root-obj (+ (^ x 2) (- 2)) 2))
(define-fun s3 () Real 0.0)
(define-fun s6 () Real (/ 1.0 1.0))
(declare-fun s0 () (_ BitVec 1))
(declare-fun s1 () (_ BitVec 1))
(assert
   (let ((s4 (- s3 s2)))
   (let ((s5 (ite (= #b1 s1) s2 s4)))
   (let ((s7 (+ s5 s6)))
   (let ((s8 (- s5 s6)))
   (let ((s9 (ite (= #b1 s0) s7 s8)))
   (let ((s10 (ite (>= s9 s3) #b1 #b0)))
   (= s10 #b1))))))))

(check-sat)
(get-model)

Вот морально эквивалентный сценарий, используя Bool вместо битового вектора размера 1, в остальном он по сути тот же:

; uses reals only
(set-option :produce-models true)
(define-fun s2 () Real (root-obj (+ (^ x 2) (- 2)) 2))
(define-fun s3 () Real 0.0)
(define-fun s6 () Real (/ 1.0 1.0))
(declare-fun s0 () (Bool))
(declare-fun s1 () (Bool))
(assert
   (let ((s4 (- s3 s2)))
   (let ((s5 (ite s1 s2 s4)))
   (let ((s7 (+ s5 s6)))
   (let ((s8 (- s5 s6)))
   (let ((s9 (ite s0 s7 s8)))
   (let ((s10 (ite (>= s9 s3) #b1 #b0)))
   (= s10 #b1))))))))

(check-sat)
(get-model)

Для первого я получаю unknown от z3 (v4.1 на Mac), в то время как последний приятно производит sat и модель.

Хотя SMT-Lib2 не позволяет смешивать реалы и битовые векторы, я думал, что Z3 отлично справляется с этими комбинациями. Я ошибаюсь? Есть ли обходной путь?

(Обратите внимание, что это сгенерированные скрипты, поэтому просто Bool вместо (_ BitVec 1) является довольно дорогостоящим, так как требует совсем немного изменений в другом месте.)

Answer 1

Новый нелинейный решатель еще не интегрирован с другими теориями. Он поддерживает только реальные переменные и логические значения. На самом деле, он также допускает целочисленные переменные, но их поддержка очень ограничена. Он фактически решает нелинейные целочисленные задачи как реальные проблемы и просто проверяет в конце концов, присваивается ли каждой целочисленной переменной целочисленное значение. Более того, этот решатель является единственной полной процедурой для нелинейной (действительной) арифметики, доступной в Z3.

Поскольку ваша первая задача содержит бит-векторы, нелинейный решатель не используется Z3. Вместо этого Z3 использует универсальный решатель, который объединяет многие теории, но он не является полным для нелинейной арифметики.

При этом я понимаю, что это ограничение, и я работаю над этим. В ближайшем будущем Z3 будет иметь новый решатель, который объединяет нелинейную арифметику, массивы, битовые векторы и т. Д.

Наконец, теория битовых векторов является очень частным случаем, так как мы можем легко свести ее к логике высказываний в Z3. Z3 имеет тактику bit-blast это относится это сокращение. Эта тактика может превратить любую нелинейную проблему + бит-вектор в проблему, которая содержит только вещественные и логические значения. Вот пример ( http://rise4fun.com/Z3/0xl).

; uses both reals and bit-vectors
(set-option :produce-models true)
(define-fun s2 () Real (root-obj (+ (^ x 2) (- 2)) 2))
(define-fun s3 () Real 0.0)
(define-fun s6 () Real (/ 1.0 1.0))
(declare-fun s0 () (_ BitVec 1))
(declare-fun s1 () (_ BitVec 1))
(declare-fun v2 () (_ BitVec 8))
(assert
   (let ((s4 (- s3 s2)))
   (let ((s5 (ite (= #b1 s1) s2 s4)))
   (let ((s7 (+ s5 s6)))
   (let ((s8 (- s5 s6)))
   (let ((s9 (ite (= #b1 s0) s7 s8)))
   (let ((s10 (ite (>= s9 s3) #b1 #b0)))
   (= s10 #b1))))))))

(assert (or (and (not (= v2 #x00)) (not (= v2 #x01))) (bvslt v2 #x00)))
(assert (distinct (bvnot v2) #x00))
(check-sat-using (then simplify bit-blast qfnra))
(get-model)