Неявная и явная количественная оценка существования в формулах SMT

Учитывая следующий код:

from z3 import *
a,b,c = BitVecs('a b c', 32)
f1 = Exists([a, b, c], And(a + b == c, a < b, c == 1337))
f2 = And(a + b == c, a < b, c == 1337)
prove(f1 == f2)

Я бы предположил, что в этом примере z3 неявно экзистенциально определяет a, b и c. Почему две формулы не равны, в чем разница?


z3 smt z3py
person n4ph1    schedule 09.02.2016    source источник

Ответы (1)


arrow_upward
1
arrow_downward

То, как вы сформулировали свой запрос, на самом деле не проверяет, равно ли f1 f2. Ваш запрос, по сути, просит решатель найти a, b, c так, чтобы следующее не выполнялось:

      Exists([a, b, c], And(a + b == c, a < b, c == 1337))
              =          
      And(a + b == c, a < b, c == 1337))

И действительно, вы можете создать внешние a, b и c так, чтобы правая часть была ложной; но левая сторона является экзистенциальной, которая истинна; таким образом, не достигается эквивалентность, о которой вы просили.

Это может быть проще увидеть на более простом примере; только с одной булевой переменной. Вы по существу спрашиваете:

     x == (Exists [x], x)

Вы видите, что эти x на самом деле разные, поэтому мы можем переименовать внутреннюю, скажем, в y; мы получили:

      x == (Exist [y]. y)

Теперь правая часть явно истинна, поскольку есть y, делающий (Exist [y]. y) истинным. Таким образом, вы, по сути, просите доказывающего установить, что независимо от того, какое x вы выберете, это правда. Это определенно не тот случай, когда вы выбираете x как ложь.

Действительно, вы можете попросить Z3 дать вам формулу, которую он пытается доказать, и вот что он возвращает для исходного запроса:

(set-info :status unknown)
(declare-fun c () (_ BitVec 32))
(declare-fun b () (_ BitVec 32))
(declare-fun a () (_ BitVec 32))
(assert
 (let (($x24 (exists ((a (_ BitVec 32)) 
                      (b (_ BitVec 32)) 
                      (c (_ BitVec 32)) )
      (and (= (bvadd a b) c) (bvslt a b) (= c (_ bv1337 32))))))
 (let (($x57 (= $x24 (and (= (bvadd a b) c) (bvslt a b) (= c (_ bv1337 32))))))
(and $x57))))
(check-sat)

Что, очевидно, выполнимо в силу приведенных выше рассуждений.

(См. Z3: преобразовать выражение Z3py в SMT-LIB2 из объекта Solver для кода, преобразующего запрос z3-python в smt-lib.)

person alias    schedule 10.02.2016