Z3結果中的隨機性

我使用Z3 Python接口作爲我正在編寫的研究工具的一部分，當我在同一個查詢中反覆運行Z3解算器時，我注意到一些非常奇怪的行爲：特別是，我似乎即使我在運行前明確重置解算器，每次都不會得到相同的結果。作爲參考，這裏是我的代碼：Z3結果中的隨機性

import z3 

with open("query.smt", "r") as smt_reader: 
    query_lines = "".join(smt_reader.readlines()) 
    for i in xrange(3): 
     solver = z3.Solver() 
     solver.reset() 

     queryExpr = z3.parse_smt2_string(query_lines) 
     equivalences = queryExpr.children()[:-1] 
     for equivalence in equivalences: 
      solver.add(equivalence) 

     # Obtain the Boolean variables associated with the constraints. 
     constraintVars = [equivalence.children()[0] for equivalence 
          in equivalences] 
     # Check the satisfiability of the query. 
     querySatResult = solver.check(*constraintVars) 

     print solver.model().sexpr() 
     print solver.statistics() 
     print ""

上面的代碼重新創建Z3求解三次，檢查同一查詢的滿足性。查詢是located here。

儘管上面的代碼部分並不完全如何使用Z3 Python接口，但問題源於這樣的認識：Z3解算器在相同查詢上代碼的不同點處調用兩次時返回的值不同結果。我想知道這是否是故意的，以及是否有任何方法來解決這個問題或確保決定論。

來源

2013-03-31 Jon Kotker

我假設你的意思是不同的模型。如果結果從坐位變爲不合格，那麼這是一個錯誤。這就是說，如果我們在相同的執行路徑中兩次解決相同的問題，那麼Z3可以產生不同的模型。 Z3將內部唯一ID分配給表達式。內部ID用於在Z3使用的一些啓發式中斷開關係。請注意，程序中的循環正在創建/刪除表達式。因此，在每次迭代中，表示約束的表達式可能具有不同的內部標識，因此解算器可能會產生不同的解決方案。

請參閱以下相關問題：

Z3 timing variation

來源

2013-03-31 16:38:44

HM哦，沒關係，這是有道理的。有沒有辦法解決這個問題呢？我應該以不同的方式使用Z3 Python接口嗎？ –

是的，我確實意味着「不同」的不同模型。抱歉，模棱兩可。 –

喬恩，我沒有看到任何解決方法。我意識到這是一個問題。我一直在嘗試修改代碼以使用文件src/ast/ast_lt.cpp中定義的表達式的總順序來打破關係。但是，這也不是一個完美的解決方案，因爲當我們簡單地重命名一個變量時，我們就開始獲得不同的解決方案如果您有意見/建議，請隨時在http://z3.codeplex.com/discussions –

Z3結果中的隨機性

回答

相關問題