Метка на утверждениях SMT-LIB 2.0 в z3 - PullRequest
Новая
       22

Метка на утверждениях SMT-LIB 2.0 в z3

2 голосов
/ 18 октября 2011

Не могли бы вы рассказать, как назвать утверждения в тесте z3 SMT-LIB 2.0? Я бы предпочел использовать стандартный синтаксис SMT-LIB, но поскольку z3, кажется, не понимает этого, я просто ищу один, работающий с z3. Нужно получить ненасыщенные ядра с метками.

Вот пример теста, который я тестировал: 

(set-option enable-cores)
(set-logic AUFLIA)
(declare-fun x () Int)
(declare-fun y () Int)
(declare-fun z () Int)
(assert (! (<= 0 x) :named hyp1))
(assert (! (<= 0 y) :named hyp2))
(assert (! (<= 0 z) :named hyp3))
(assert (! (< x y) :named hyp4))
(assert (! (and (<= 0 y) (<= y x)) :named hyp5))
(assert (! (not (= x z)) :named goal))
(check-sat)
(get-unsat-core)

Я ожидаю несогласованное ядро ​​{hyp4, hyp5} из-за противоречия (x 

(error "ERROR: line 10 column 31: could not locate id  hyp1.")
(error "ERROR: line 11 column 31: could not locate id  hyp2.")
(error "ERROR: line 12 column 31: could not locate id  hyp3.")
(error "ERROR: line 13 column 30: could not locate id  hyp4.")
(error "ERROR: line 16 column 36: could not locate id  hyp5.")
(error "ERROR: line 18 column 35: could not locate id  goal.")
sat
()

Я понимаю, что z3 не понимает этот способ именования, но я не смог найти другой способ в документации z3.

Не могли бы вы помочь мне, пожалуйста?

1 Ответ

3 голосов
/ 18 октября 2011

Если я изменю вашу первую команду с 

(set-option enable-cores)

до 

(set-option :produce-unsat-cores true)

и что я тогда запускаю твой скрипт: 

z3 -smt2 script.smt2

получаю в качестве вывода 

unsat
(hyp4 hyp5)

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

...