在 Z3 (Python) 中，假設我得到一個具有以下形狀的模型：
[c_0 = True, c_3 = False, c_1 = False, c_2 = False]
如何對變數進行排序，以便分配按字母順序排列？
[c_0 = True, c_1 = False, c_2 = False, c_3 = False]如何訪問模型的任何元素？我的意思是，如果我這樣做：
m = s.model() #equivalent to [c_0 = True, c_3 = False, c_1 = False, c_2 = False]
a = m[0]
print(a)
我得到了c_0，而不是預期的c_0 = True。
為了使這篇文章盡可能簡單，我不再添加任何代碼，c變數只是示例。
我的最終目標是一種方法，給定[c_0 = True, c_3 = False, c_1 = False, c_2 = False]回傳一個陣列a=[True, False, False, False]，其中a[0]對應于 的值c_0，a[1]對應于 的值c_1，等等。
編輯
對于 (1)，我嘗試過sorted(m, key=str.lower)，但出現以下錯誤：descriptor 'lower' requires a 'str' object but received a 'FuncDeclRef'. 這意味著我應該將每個元素轉換為str，這是我不想要的。
我更喜歡 Z3 的“本機”方法，它不會對變數的型別進行修改。
uj5u.com熱心網友回復：
如果您想按鍵對模型進行排序，則必須將其轉換為不同的資料結構。（這實際上與 z3 沒有太大關系，而是字典內部如何完成。）您嘗試的幾乎就在那里，您只需要確保同時保留變數和值。下面是一個例子：
from z3 import *
a, b = Bools('a b')
s = Solver()
s.add(And(a, Not(b)))
print(s.check())
m = s.model()
nicer = sorted ([(d, m[d]) for d in m], key = lambda x: str(x[0]))
print(nicer)
這列印：
sat
[(a, True), (b, False)]
請注意，它保持原樣，即您不會丟失物件屬性：
print(type(nicer[0][0]))
print(type(nicer[0][1]))
印刷：
<class 'z3.z3.FuncDeclRef'>
<class 'z3.z3.BoolRef'>
對于您的第二個問題，您可以通過變數本身訪問：請注意，模型是字典，因此可以通過變數查找它們。對于上面的程式，你可以說：
print(m[a])
print(m[b])
這列印：
True
False
獲得對串列后，您可以簡單地獲取值：
print([v for (d, v) in nicer])
這列印：
[True, False]
現在你有了一個對的串列，你可以隨心所欲地用它做任何事情。
旁注：我理解在你的問題中加入“最少”代碼的動機；這很誘人，我已經在自己之前做過了！但是最好提供一個最小完整的示例，即本論壇的讀者可以按原樣運行的示例。這可確保他們不必猜測您可能正在做的其他事情，或導致誤解。盡可能多地發布一個最小完整的示例來展示您面臨的問題。此外，如果您在每個帖子中只問一個問題，則堆疊溢位效果最佳；否則細節會變得模糊。最好的辦法是用一個最小完整的例子來提出一個特定的問題，盡管我知道這可能并不總是可行的。謝謝！
轉載請註明出處，本文鏈接：https://www.uj5u.com/qiye/399277.html