2

我有一个文件包含：

(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 吗？

问候。

4

1 回答 1

5

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)
于 2012-01-22T03:08:25.403 回答