如何在Ubuntu上使用Z3運行smtLib文件？

例如，我有一個smtLib文件'encoding.smt'。現在我想在z3上運行這個文件（standalone exe），在Ubuntu機器上給定超時和內存分配。像：如何在Ubuntu上使用Z3運行smtLib文件？

$./z3 encoding.smt 240(sec) 6(GB)

我已經從Z3下載頁面下載了ubuntu 32位zip文件。我現在要做什麼？ 'bin'文件夾中有一個z3應用程序。我需要更改任何環境變量 - 如果我想在Ubuntu下編寫任何Z3py腳本？

任何一個可以給我兩個步驟（運行.smt文件通過獨立Z3與給定的超時和內存並運行從z3py腳本.smt文件與給定的超時和內存）

感謝您的建議

來源

2013-11-27 user1770051

我使用help命令$ ./z3 -h獲得了超時選項，z3（可執行文件）的內存。但是，有誰能告訴我如何在Z3py腳本中設置選項？像 - solver.set（'timeout'，240）solver.set（'memory'，6）!!我不知道如何設置這些選項。我看過一些關於超時的帖子，但我怎麼設置內存限制。謝謝 – user1770051

這些選項分別被稱爲timeout和memory_max_size。

set_option(timeout='60') 
set_option(memory_max_size='1000')

的（全局和模塊）選項列表可以通過運行z3 -p來獲得：在Python接口，它們可以如下進行設置。這些選項也可以在命令行上設置，例如，

z3 encoding.smt2 timeout=60 memory_max_size=1000

來源

2013-12-13 13:50:06

如何在Ubuntu上使用Z3運行smtLib文件？

回答

相關問題