В статье this paper (раздел 3.2) говорится, что z3 применяет переписывание/упрощение формул до того, как он выполнит какие-либо другие шаги.Переписывание формул
Предположим, что у меня есть формула в QF_UF, которая состоит из нескольких операторов assert. Существует ли какое-либо правило перезаписи, которое каким-то образом «нарушит барьер» между различными утверждениями assert? Или, задавая другой вопрос: могу ли я быть уверенным, что правила перезаписи применяются только локально, «внутри» одного утверждения?
Для примера рассмотрим следующую формулу:
(set-logic QF_UF)
(set-option :auto-config false)
(set-option :PROOF_MODE 2)
(declare-fun a() Bool)
(assert a)
(assert (not a))
(check-sat)
(get-proof)
Могу ли я быть уверен, что доказательство будет содержать шаг разрешения доказать False, или это возможно, что False будет заключен путем перезаписи/шаг упрощения ?
Причина, по которой я спрашиваю, заключается в том, что для моего приложения каждое заявление assert имеет специальную семантику. Переписывание/упрощение по нескольким операциям assert сделало бы результатом доказательство неудовлетворительной непригодности (или, по крайней мере, очень сложного в использовании) для меня.
Не могли бы вы описать то, что вы пытаясь сделать? Почему переписывание/упрощение нескольких утверждений сделает результаты непригодными для использования? Обратите внимание, что во время поиска Z3 будет выполнять шаги анализа нескольких утверждений. Это также сделает доказательства непригодными для использования? –
Я пытаюсь переписать доказательство на «чистое» разрешение. По причинам, связанным с конкретными приложениями, упрощения и перезаписи, которые происходят внутри одного утверждения, меня не интересуют. Я., я просто предполагаю, что утверждение assert содержит уже упрощенный вариант формулы. Меня интересуют все аргументационные шаги по заявлениям со стороны, и я должен как-то разобраться с ними. Если бы я мог быть уверен, что никакое упрощение не происходит через утверждения, у меня есть один (трудный) случай, с которым приходится иметь дело, пока я переписываю. Надеюсь, это станет немного более ясным. – Georg