與Z3

Question

並行求解公式比方說，我有一定數量的斷言約束是滿足的一個Z3求解。設S是一組約束，我想驗證S中的每個約束是否在將約束添加到求解器時公式仍然可滿足。這可以很容易地以這樣的方式順序進行：

results = [] 

for constraint in S: 
    solver.push() 
    solver.add(constraint) 
    results.append(solver.check() == z3.sat) 
    solver.pop() 

print all(results) 

現在，我想這個並行加快速度，但我不知道如何與Z3做正確。

這是一種嘗試。考慮下面的簡單例子。所有變量都是非負整數，並必須總和爲1。現在我想驗證是否每個變量x可以獨立地由> 0。顯然，這是如此;讓x = 1並將0賦值給其他變量。這裏是一個可能的並行實現：

from multiprocessing import Pool 
from functools import partial 
import z3 

def parallel_function(f): 
    def easy_parallize(f, sequence): 
     pool = Pool(processes=4) 
     result = pool.map(f, sequence) 

     pool.close() 
     pool.join() 

     return result 

    return partial(easy_parallize, f) 

def check(v): 
    global solver 
    global variables 

    solver.push() 
    solver.add(variables[v] > 0) 
    result = solver.check() == z3.sat 
    solver.pop() 

    return result 

RANGE = range(1000) 
solver = z3.Solver() 
variables = [z3.Int('x_{}'.format(i)) for i in RANGE] 

solver.add([var >= 0 for var in variables]) 
solver.add(z3.Sum(variables) == 1) 

check.parallel = parallel_function(check) 
results = check.parallel(RANGE) 
print all(results) 

令人驚訝的這個完美的作品在我的機器上：結果是健全的，它的速度要快得多。然而，我懷疑這是安全的，因爲我正在研究一個單一的全局求解器，並且我可以很容易想象push/pops會同時發生。有沒有任何干淨/安全的方式來實現這與z3py？

Answer 1

事實上，這可能工作的第一次測試，而不是一般。不支持在單個Context上進行並行解決，稍後會有數據競爭和段錯誤。

在Python中，Context對象是隱藏的，所以大多數用戶不需要處理它，但是爲了並行運行，我們需要爲每個線程設置一個Context，然後將正確的一個傳遞給所有其他函數（隱式地使用隱藏的Context之前）。請注意，所有表情，解算器，戰術等，都依賴於一個特定的語境，所以如果對象需要跨越這一邊界，我們需要把它們翻譯（見翻譯（...）在AstRef和類似）。

參見Multi-threaded Z3?和When will the Z3 parallel version be reactivated?