z3 smt求解器採用什麼形式的輸入??我們可以使用一個文件來讀取需要解決的等式嗎？如果是，請告訴我們如何？

from z3 import * 
x = Int('x') 
y = Int('y') 
s = Solver() 
try: 
    f = open("read.txt","r") 
    try: 
     str = f.read() 
     length = len(str) 
     s.add(str) 
    finally: 
     f.close() 
except IOError: 
    pass

我寫了上面的代碼，但它不工作。它不會將字符串作爲輸入，並且我無法找到它接受的輸入類型。請幫忙。z3 smt求解器採用什麼形式的輸入??我們可以使用一個文件來讀取需要解決的等式嗎？如果是，請告訴我們如何？

來源

2013-06-29 user2534232

'read.txt'看起來怎麼樣？你有沒有試圖找出你是否可以加載SMTLib2格式的斷言？ –

嘗試做一些像'eval（'s.add（{}）'.format（str.strip（）））'。順便說一句，'str'是內置的名稱，不應該用作變量的名稱。 – martineau

read.txt包含形式爲x + y == 2的方程 – user2534232

我們基本上可以做到martineau建議的內容。請記住，這是一個很大的破解和不安全因爲文件read.txt可能包含任意的Python命令。無論如何，下面這段代碼將評估輸入文件的每一行，並將結果對象添加到求解器s中。如果文件read.txt包含x + y == 2，那麼輸出將是：

sat 
[y = 0, x = 2]

下面是更新後的代碼：

from z3 import * 
x = Int('x') 
y = Int('y') 
s = Solver() 
try: 
    f = open("read.txt","r") 
    try: 
     for l in f: 
      s.add(eval(l)) 
    finally: 
     f.close() 
except IOError: 
    pass 
print s.check() 
print s.model()

另一種解決方案是在SMT-LIB 2.0格式創建的文件，以及使用的方法在以下描述的帖子：

來源

2013-07-09 01:06:11

z3 smt求解器採用什麼形式的輸入??我們可以使用一個文件來讀取需要解決的等式嗎？如果是，請告訴我們如何？

回答

相關問題