如何調用Z3上輸入文件

我有一個包含文件：如何調用Z3上輸入文件

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

問候。

來源

2012-01-22 Schemer

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-22 03:08:25

我加入（設置選項：產生的模型真）在我的劇本的開頭，但所有的解析選項仍然只能產生錯誤消息。特別是-smt2是一個無法識別的選項（如果有幫助，我使用2.3版本）。什麼解析器適用於我顯示的輸入文件？ – Schemer

此文件採用SMT 2.0格式。 Z3 2.3是一個非常舊的版本。它甚至不支持SMT 2.0。你應該從http://research.microsoft.com/en-us/um/redmond/projects/z3/download.html下載最新的3.2版本。 –

不幸的是，這是一個學校作業，我被迫使用任何版本的安裝在大學實驗室。 – Schemer

如何調用Z3上輸入文件

回答

相關問題