我知道我可以在Z3中聲明一個z3.Real的矩陣，通過單獨聲明它的元素（可能通過列表理解）。有沒有辦法來表示一個未知大小的矩陣？在Z3中聲明大小未知的矩陣
例如，考慮下面的例子： 在圖像濾波，給定的size [X,Y]的圖像I和濾波器核的size [M,N]K，圖像I和濾波器內核K是I*K之間的卷積。我想Z3來證明（或反駁）存在任何大小的過濾器F1和F2，例如I*K == I*F1*F2。
問題本身是完全組成的，可能沒有意義。我的想法是，我是否可以要求Z3找到未知大小的矩陣，以使矩陣滿足可以用線性函數表示的某個特性。謝謝！
Z3支持簡單鍵入的一階邏輯規範。從某種意義上說，第一個問題是你如何表達你對邏輯感興趣的屬性。 對於有界大小的模型，您可以實例化X，Y，M，N大小，併爲合適的有限域表達反例查詢。如果你想要參數大小，你可以將*的行爲表達爲三元關係。例如，您可以使用函數I，K，I_K，它們帶有兩個參數並表示I_K（x，y）與I，K中的條目之間的關係。然後，您將遇到諸如證明確實需要歸納的問題。良好的互動支持環境，如精益，PVS，Coq，Isabelle或Dafny等環境，更適合建立證明。
尼古拉斯的答案似乎在腦子裏打了個毛病。我認爲Z3（或任何SMT解算器）不會成爲解決此類問題的最佳工具，因爲您希望根據您的理解推導「未知」尺寸的矩陣。當你有這個問題的具體實例時，我認爲Z3可以非常有效;但不是在一般的「全部大小」情況下。這些索賠通常需要歸納證明，並且更適合其他工具。
但是，您可能會忽略未解釋的函數。如果您將矩陣和濾波器表示爲未解釋的函數，並按照這種方式對您的卷積進行編碼。您可能必須假定N×M的上限（即，N < 100，M < 100;或類似），並相應地進行編碼，以便任何超出範圍的結果產生合適的結果。 （這意味着將，當然，取決於手頭的問題是什麼。）
你可能會驚訝Z3如何冷靜可以根據該設置，因爲我懷疑它會給你相當不錯的成績。如果您嘗試這種方法，我很樂意聽到您發現的內容。