在 Python (Collab) 中，我有以下變量c：
array([x_1 > 1000, y_1 < x_1 + 1], dtype=object)
z3 (py) 變量/謂詞在哪里x_1 > 1000和y_1 < x_1 + 1在哪裡。我想完全訪問它的“第一個元素”： array / list [x_1 > 1000, y_1 < x_1 + 1]，但我沒有能力。
這些是我所做的嘗試：
c[0]產量x_1 > 1000（當然還有c[1]產量y_1 < x_1 + 1）。a, b = c 再次產生a成為x_1 > 1000和b成為y_1 < x_1 + 1。c.0產生錯誤（顯然，也是如此c.1）。我想訪問數組元素的原因是我想以自動方式執行以下 z3 計算：
And([x_1 > 1000, y_1 < x_1 + 1]). 所以製作類似的東西會很好And(c[0])。
這可能是初學者的錯誤，但我看不到。有什麼幫助嗎？
編輯：
請注意，詢問的問題And(c[0])是我正在做And(x_1 > 1000)，而我想執行:（And(x_1 > 1000, y_1 < x_1 + 1)即，顯然And(c[0],c[1]).
最好張貼完整的代碼段，即那些可以被讀者加載和執行而無需填補缺失部分的代碼段。否則真的很難復制/理解你正在嘗試做什麼以及你遇到了什麼錯誤。
我不使用 collab （不確定它是什麼），但如果c是一個列表，您可以使用該*符號將其內容轉換為參數。像這樣的東西：
from z3 import *
x_1, y_1 = Ints('x_1 y_1')
c = [x_1 > 1000, y_1 < x_1 + 1]
s = Solver()
s.add(And(*c))
print(s.sexpr())
這打印：
(declare-fun x_1 () Int)
(declare-fun y_1 () Int)
(assert (and (> x_1 1000) (< y_1 (+ x_1 1))))
無論您在 list 中有多少個元素，這都會正常工作c。請注意，這與 z3 無關，但它是 Python 習語。
我不確定你的array構造；但如果它可以變成一個列表，上面的技巧應該可以工作。這是你要找的嗎？
本文收集自互联网，转载请注明来源。
如有侵权，请联系 [email protected] 删除。
我来说两句