Должно ли присвоение имени утверждению влиять на выполнимость проверки в Z3? - PullRequest
Новая
       5

Должно ли присвоение имени утверждению влиять на выполнимость проверки в Z3?

0 голосов
/ 28 ноября 2018

Мы столкнулись с ограничениями, для которых Z3 возвращает sat, но если мы затем добавим определенное именованное утверждение, тогда Z3 вернет unknown.Один из примеров: 

  (declare-fun a () Real)
  (declare-fun b () Bool)
  (assert (and (<= 0.1 a) (<= a 10.0)))
  (assert (= b (= 1.0 (/ 1.0 a))))
  (check-sat)

Z3 сообщает, что это вполне возможно.Кроме того, мы можем утверждать, что b является либо true, либо false, оба из которых являются ожидаемыми.Однако, если мы используем именованное утверждение для значения b, то результат проверки выполнимости может стать unknown в зависимости от значения.Со значением true Z3 по-прежнему возвращает sat: 

  (set-option :produce-unsat-cores true)
  (declare-fun a () Real)
  (declare-fun b () Bool)
  (assert (and (<= 0.1 a) (<= a 10.0)))
  (assert (= b (= 1.0 (/ 1.0 a))))
  (assert (! (= b true) :named c))
  (check-sat)

Используя значение false, Z3 возвращает unknown: 

  (set-option :produce-unsat-cores true)
  (declare-fun a () Real)
  (declare-fun b () Bool)
  (assert (and (<= 0.1 a) (<= a 10.0)))
  (assert (= b (= 1.0 (/ 1.0 a))))
  (assert (! (= b false) :named c))
  (check-sat)

Проверка причины дляunknown результат (с (get-info :reason-unknown)) возвращает (incomplete (theory arithmetic)).

1 Ответ

0 голосов
/ 28 ноября 2018

Похоже, что z3 просто выбирает неправильную тактику в последнем случае.Замените ваш check-sat вызов на: 

 (check-sat-using qfnra-nlsat)

И z3 говорит sat в обоих случаях.

Почему z3 заканчивает тем, что выбрал другую тактику, трудно ответить;Я бы порекомендовал подать это как билет на их сайте github;возможно, им не хватает эвристики.

Примечание: я нашел это, запустив оба случая с -v:10 и просматривая подробный вывод.Это не плохой способ увидеть, что делает z3 для достаточно коротких тестов.

...