檢查Z3模型是否滿足約束條件的最快方法？ BitVectors，Z3 3.2，C＃API，x64，多線程

給定Z3中的一組約束（斷言）我想知道檢查一個我已經滿足這些斷言的模型是否是最有效的方法。該模型是從相似的一組約束中獲得的。我需要一個是/否的答案，而不是像Specifying initial model values for Z3那樣的軟約束。檢查Z3模型是否滿足約束條件的最快方法？ BitVectors，Z3 3.2，C＃API，x64，多線程

我正在使用x64版本的Z3 3.2在位矢量上使用Windows 7 x64上的C＃API。我通過實例化多個Z3 Context對象來實現多線程，每個線程一個。由於缺乏對多線程的支持，我沒有使用Z3 4.0。

我目前的方法是使用Context.AssertCnstr(Term)然後簡單地調用Context.Check()來聲明模型爲附加約束集。

來源

2012-08-04 Konrad Jamrozik

Z3 3.2不是線程安全的。也就是說，在不同步的情況下在不同的線程中使用不同的Z3'Context'對象是不安全的。 Z3 4.0修復了這個問題。順便說一句，你爲什麼說Z3 4.0缺乏對多線程的支持。 – 2012-08-04 17:57:05

@LeonardodeMoura經過多次試驗和錯誤之後，我發現解決方案「每個線程一個上下文」實際上是唯一允許我並行使用所有8個內核並且不會拋出任何異常的解決方案。如果您願意，我可以爲您提供一個展示此功能的代碼片段（並且也不要使用示例）。我說Z3 4.0缺乏對多線程的支持，因爲Z3 4.0發行說明狀態爲「此版本中禁用了Parallel Z3」。並且我無法在Z3 4.0安裝中找到「x64_mt \ Microsoft.Z3.dll」。「x64_mt」目錄丟失。它在Z3 3.2中可用 – 2012-08-04 22:22:47

Z3公開了一種名爲「Z3_model_eval」或「Model.Eval」（來自C＃）的方法，該方法需要一個模型和一個表達式。如果表達式包含量詞並且評估者無法確定量化公式模型的真值，則評估可能失敗。如果模型評估成功，您可以檢查返回的值以確定模型強制斷言是否爲真。爲Z3_model_eval文檔詳細說明中更詳細的合同：

http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga86670c291a16640b932e7892176a9d1b

模型評估將不會檢測到重言，所以序列化模型作爲式和具有Z3檢查模型之間的含義和斷言可能更適合用於某些用途。

來源

2012-08-04 21:01:42

檢查Z3模型是否滿足約束條件的最快方法？ BitVectors，Z3 3.2，C＃API，x64，多線程

回答

相關問題