Как вызвать Z3 для входного файла - PullRequest
Новая
       7

Как вызвать Z3 для входного файла

1 голос
/ 22 января 2012

У меня есть файл, содержащий: 

(declare-const a Int)
(declare-const b Int)
(declare-const c Int)
(declare-const d Real)
(declare-const e Real)
(assert (> a (+ b 2)))
(assert (= a (+ (* 2 c) 10)))
(assert (<= (+ c b) 1000))
(assert (>= d e))
(check-sat)
(get-model)

и, согласно онлайн-руководству, запуск z3 для этого файла должен вернуть: 

sat
(model
    (define-fun c () Int
        (- 5))
    (define-fun a () Int
        0)
    (define-fun b () Int
        (- 3))
    (define-fun d ()
        Real 0.0)
    (define-fun e ()
        Real 0.0)
)

Так что я знаю, что это законный ввод Z3. Однако всякий раз, когда я запускаю «z3 [option]», все, что я получаю, это сообщения об ошибках, независимо от того, какую опцию я выберу, включая ни одной. Может кто-нибудь сказать мне, как правильно вызвать Z3 на входной файл?

Привет.

1 Ответ

5 голосов
/ 22 января 2012

Z3 поддерживает множество форматов ввода. Он использует расширение файла, чтобы угадать, какой парсер будет использоваться. Если расширение .smt2. Он будет использовать парсер SMT 2.0. Вы также можете указать, какой парсер следует использовать. Опция -smt2 заставит Z3 использовать синтаксический анализатор SMT 2.0. Наконец, Z3 не включает построение модели по умолчанию. Поэтому вам следует использовать опцию MODEL=true или добавить команду (set-option :produce-models true) в начале вашего скрипта.

Если вы хотите использовать очень старую версию Z3, вам придется использовать формат SMT 1.0. Этот формат описан в: http://goedel.cs.uiowa.edu/smtlib/papers/format-v1.2-r06.08.30.pdf

При этом я настоятельно рекомендую вам обновить. SMT 1.0 не очень удобен для пользователя, и большинство документации / учебных пособий по SMT представлены в формате SMT 2.0.

Вот ваш пример в этом формате: 

(benchmark file
  :extrafuns ((a Int) (b Int) (c Int) (d Real) (e Real))
  :assumption (> a (+ b 2))
  :assumption (= a (+ (* 2 c) 10))
  :assumption (<= (+ c b) 1000)
  :assumption (>= d e)
  :formula true)
...