Отключение введения функции Скулема в доказательство линейной арифметики

Учитывая следующий сценарий SMT2:

(set-option :produce-proofs true)
(set-logic AUFLIRA)
(declare-sort Complex$ 0)
(declare-fun r$ () Real)
(declare-fun s$ () Complex$)
(declare-fun re$ (Complex$) Real)
(declare-fun norm$ (Complex$) Real)
(assert (! (not (=> (and (forall ((?v0 Complex$)) (<= (ite (< (re$ ?v0) 0.0) (- (re$ ?v0)) (re$ ?v0)) (norm$ ?v0))) (<= (norm$ s$) r$)) (<= (ite (< (re$ s$) 0.0) (- (re$ s$)) (re$ s$)) (+ r$ 1.0)))) :named a0))
(check-sat)
(get-proof)

Z3 (нестабильная версия) выдает доказательство, содержащее функцию Скулема «норма $0». Эта функция вводится на шаге перезаписи:

(ALL v0. (if 0 <= Re v0 then Re v0 else - 1 * Re v0) <= cmod v0) =
((ALL v0. cmod v0 = (if 0 <= Re v0 then Re v0 else - 1 * Re v0) + norm_0 v0) & (ALL v0. 0 <= norm_0 v0))

Можно ли подавить это поведение с помощью переключателя командной строки? То есть есть ли такой вариант, что Z3 выдает доказательство без такой функции Скулема? В принципе, это должно быть возможно, поскольку Z3 версии 3.2 находит доказательство, не требующее функции Скулема.


z3
person bhms    schedule 29.09.2014    source источник

Ответы (1)


arrow_upward
0
arrow_downward

Константа skolem вводится модулем MBQI (реализация квантора на основе модели). Это, вероятно, «новая часть», которая заставляет вас видеть другое поведение. MBQI намного мощнее, чем создание экземпляров квантификатора на основе шаблонов. Однако для вашего примера работает стратегия создания экземпляра квантификатора на основе шаблона. Так что вы можете попробовать это.

Другими словами, запустите Z3 для подавления MBQI следующим образом:

z3 skolem-example.smt2 smt.mbqi=false auto-config=false

person Nikolaj Bjorner    schedule 03.10.2014