如何在输入文件上调用Z3

Question

我有一个文件包含:

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

问候.

Answer 1

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)