z3能否讀取MathSAT的輸出文件作爲其輸入文件？

我需要使用z3和mathsat進行一些實驗。我已經完成了mathsat的實驗。編寫mathsat的輸入文件需要很長時間，我不想再爲z3編寫輸入文件。 Mathsat支持從'msat'文件生成'smt'文件。轉換命令如下所示：z3能否讀取MathSAT的輸出文件作爲其輸入文件？

/home/xdb/mathsat/mathsat-4.2.17-linux-x86_64/bin/mathsat -input=msat -output=smt -logic=QF_LRA /home/xdb/satcase/sample/sample.msat>>/home/xdb/satcase/sample/sample.smt

我的問題是，z3能識別這個'smt'文件嗎？

來源

2013-01-04 Dingbao Xie

Z3可以讀取SMT 1.0和2.0文件。格式定義爲http://www.smtlib.org。如果MathSAT生成的公式符合標準，那麼您應該沒有問題。你有沒有試過用Z3讀取生成的文件？如果它不起作用，那麼Z3產生的錯誤信息是什麼？

來源

2013-01-04 14:38:49

我已經試過了，它在4.2版本上無法使用。但是，它可以在最新版本的4.3版上運行。我只是想知道結果是否正確。雖然z3 v4.3可以工作並打印結果，這是否意味着它可以識別這個'smt'文件。爲什麼z3 v4.2不能識別這個'smt'文件？ –

Z3 v4.2也支持smt文件。你可以添加一個由MathSAT生成的SMT文件的鏈接嗎？ –

http://seg.nju.edu.cn/BACH/Demo/sample_100.smt感謝您的幫助。 –

z3能否讀取MathSAT的輸出文件作爲其輸入文件？

回答

相關問題