В этой статье (раздел 3.2) говорится, что z3 применяется переписывание/упрощение формул перед выполнением каких-либо других шагов.
Предположим, у меня есть формула в QF_UF, состоящая из нескольких операторов 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 сделало бы результирующее доказательство неудовлетворительности непригодным для использования (или, по крайней мере, очень трудным для использования) для меня.
