Z3 отключить упрощение утверждений для доказательств

Question

Есть ли способ отключить упрощение / переписывание утверждений в Z3 (версия 4.8.8)?

В настоящее время я работаю над воспроизведением доказательств Z3 в KeY ( https://www.key-project.org). Однако, чтобы иметь возможность воспроизвести "утвержденное" правило Z3, мне нужно точное утверждение, указанное во входных данных SMT-LIB для Z3, а не его упрощенная версия.

В качестве крайнего примера того, что может случиться, рассмотрим ввод SMT-LIB:

(set-option :produce-proofs true)

(assert
  (not
    (forall ((y Int))
      (exists ((x Int))
        (= x (+ y 1))
      )
    )
  )
)
(check-sat)
(get-proof)

Запуск Z3 4.8.8 приводит к следующему выводу:

unsat
((proof
(asserted false)))

Очевидно, что утверждение было упрощено, что делает доказательство бесполезным. Есть ли способ полностью отключить это упрощение (и таким образом получить "настоящее" доказательство от Z3, которое я могу воспроизвести в нашем инструменте)?

Answer 1

Возможно, вам будет удобнее использовать более новую версию z3. Например, учитывая ваш пример, недавно скомпилированная версия из github-master производит:

((proof
(let (($x88 (not true)))
 (let (($x48 (forall ((y Int) )(! (exists ((x Int) )(! (= x (+ 1 y)) :qid k!8))
  :qid k!9))
 ))
 (let (($x54 (not $x48)))
 (let ((@x36 (rewrite (= $x54 $x54))))
 (let (($x30 (forall ((y Int) )(! (exists ((x Int) )(! (= x (+ y 1)) :qid k!8))
  :qid k!9))
 ))
 (let (($x31 (not $x30)))
 (let ((@x32 (asserted $x31)))
 (let ((@x45 (mp (mp (mp @x32 (rewrite (= $x31 $x54)) $x54) @x36 $x54) @x36 $x54)))
 (let ((@x53 (mp (mp (mp @x45 @x36 $x54) @x36 $x54) (rewrite (= $x54 $x88)) $x88)))
 (mp @x53 (rewrite (= $x88 false)) false))))))))))))

Формат остается недокументированным, и в целом z3 будет действительно сложно создавать детальные доказательства при наличии кванторов. Прямая цитата из: https://theory.stanford.edu/%7Enikolaj/programmingz3.html#sec-proofs говорит:

Детализация объектов доказательства основана на максимальных возможностях. Доказательства для SMT Core относительно мелкозернистые, в то время как доказательства для процедур, выполняющих исключение квантора, например QSAT, описанного в разделе 6.4, представлены как большие непрозрачные шаги.