(get-unsat-core) Z3: ядро ​​unsat недоступно - PullRequest
Новая
       33

(get-unsat-core) Z3: ядро ​​unsat недоступно

0 голосов
/ 07 сентября 2018

Вот моя программа, которая возвращает SAT, когда на графике существует цикл, и UNSAT, когда цикла нет: 

(set-option :fixedpoint.engine datalog) 

(define-sort s () Int) 

(declare-rel edge (s s)) 
(declare-rel path (s s)) 

(declare-var a s) 
(declare-var b s) 
(declare-var c s) 

(rule (=> (edge a b) (path a b)))
(rule (=> (and (path a b) (path b c)) (path a c)))

(rule (edge 1 2))
(rule (edge 2 3))


(declare-rel cycle (s))
(rule (=> (path a a) (cycle a)))
(query cycle :print-answer true)

Я хочу получить модель, когда нет цикла (UNSAT). Я понял, что должен использовать команду (get-unsat-core) и установить опцию в (set-option: yield-unsat-cores true): 

(set-option :fixedpoint.engine datalog) 
(set-option :produce-unsat-cores true)
(define-sort s () Int) 

(declare-rel edge (s s)) 
(declare-rel path (s s)) 

(declare-var a s) 
(declare-var b s) 
(declare-var c s) 

(rule (=> (edge a b) (path a b)) P-1)
(rule (=> (and (path a b) (path b c)) (path a c)) P-2)

(rule (edge 1 2) E-1)
(rule (edge 2 3) E-2)
(rule (edge 3 1) E-3)

(declare-rel cycle (s))
(rule (=> (path a a) (cycle a)))
(query cycle :print-answer true)


(get-unsat-core)

Я получаю эту ошибку: 

unsat
(error "line 24 column 15: unsat core is not available")

Ответы [ 2 ]

0 голосов
/ 08 сентября 2018

Если я могу вмешаться, AFAIK нужно назвать ограничения, когда кто-то хочет получить unsat core.

На сайте smtlib приведен следующий пример: 

; Getting unsatisfiable cores
(set-option :produce-unsat-cores true)
(set-logic QF_UF)
(declare-const p Bool) (declare-const q Bool) (declare-const r Bool)
(declare-const s Bool) (declare-const t Bool)
(assert (! (=> p q) :named PQ))
(assert (! (=> q r) :named QR))
(assert (! (=> r s) :named RS))
(assert (! (=> s t) :named ST))
(assert (! (not (=> q s)) :named NQS))
(check-sat)
; unsat
(get-unsat-core)
; (QR RS NQS)
(exit)

Как указывает @ LeventErkok , модель доступна только тогда, когда формула sat, а unsat core доступна только тогда, когда формула unsat.

0 голосов
/ 07 сентября 2018

Получение модели в случае unsat не имеет смысла. Неудовлетворенный буквально означает, что нет модели, которая удовлетворяла бы вашим ограничениям. Пожалуйста, оставьте более четкий вопрос о том, чего именно вы пытаетесь достичь.

Несоответствующее ядро ​​- это подмножество противоречивых утверждений. Этот набор по определению не является удовлетворительным и не представляет собой модель, которую вы ищете. Кроме того, я очень сомневаюсь, что движок с фиксированной запятой поддерживает ненасыщенные ядра, поэтому сообщение об ошибке, которое вы получаете, просто означает, что они не вычисляются.

...