使用Z3混凝土陣列

Question

我想用Z3來解決這個問題：

給定兩個數組a和b，大小相等混凝土值，選擇滿足這些約束指標：

0 < selection < [length of array] 
forall i, a[selection] <= a[i] 
forall i, b[selection] >= b[i] 

我z3py程序是這樣的：

def selectIndex(array1, array2): 
    n= len(a) #assume both lists are same size 
    s = Solver() 
    selection = Int('selection') 
    i = Int('i') 
    j = Int('j') 
    a= Array('a', IntSort(), IntSort()) 
    b= Array('b', IntSort(), RealSort()) 

    for idx in range(n): 
     Store(a, idx, array1[idx]) 
     Store(b, idx, array2[idx]) 

    constraint1 = And(selection >= 0, selection <= n) 
    constraint2 = And(i >= 0, i <= n) 
    constraint3 = And(j >= 0, j <= n) 
    constraint4 = ForAll([i], a[selection] <= a[i]) 
    constraint5 = ForAll([j], b[selection] >= b[j]) 

    s.add(And(constraint1, constraint2, constraint3, constraint4, constraint5)) 

    s.check() 
    m = s.model() 
    return m[selection].as_long() 

模型總是返回0，即使在給定的輸入陣列爲其中只有一個滿足約束條件選擇。我不認爲它使用數組a和b中的具體值。我該如何解決？

Answer 1

這個例子有很多問題，但關鍵的一點是Store(...)表達式什麼都不做。 Store(...)的結果是一個新的數組表達式，它表示舊數組（a,b），其中一個索引（idx）更新爲新值（array1[idx]，array2[idx]）。目前，這些新的陣列被丟棄，但我們可以將它們保存：

for idx in range(n): 
    a = Store(a, idx, array1[idx]) 
    b = Store(b, idx, array2[idx]) 

此外，我認爲

constraint1 = And(selection >= 0, selection <= n) 

應該不包括指數n，即<=應該<和約束i和j

constraint2 = And(i >= 0, i <= n) 
constraint3 = And(j >= 0, j <= n) 

是不必要的。