Erstellen Sie ein Array mit fester Größe und initialisieren Sie es

Question

Ich werde ein Array mit fester Größe erstellen und es mit einigen Werten initialisieren.

Zum Beispiel die folgende C++ Code:

a[0] = 10; 
a[1] = 23; 
a[2] = 27; 
a[3] = 12; 
a[4] = 19; 
a[5] = 31; 
a[6] = 41; 
a[7] = 7; 

Gibt es einige Dienstprogramme in Z3 es zu modellieren?

Answer 1

Z3 unterstützt die Array-Theorie, wird aber normalerweise verwendet, um unbegrenzte oder sehr große Arrays zu kodieren. Mit "groß" meine ich, dass die Anzahl von Array-Zugriffen (d. H. Auswahlen) in Ihrer Formel viel kleiner ist als die tatsächliche Größe des Arrays. Wir sollten uns fragen: "Brauchen wir wirklich Arrays zum Modellieren/Lösen von Problem X?". Für Arrays mit fester Größe wie in Ihrem Beispiel können wir für jede Array-Position eine andere Variable verwenden. Beispiel: a0 für a[0], a1 für a[1] usw. Natürlich, wenn wir Theorien nicht verwenden, dann codieren, das einen Array-Zugriff wie a[i] muss als großer if-then-else Begriff wie

(ite (= i 0) a0 (ite (= i 1) a1 ...))

codiert werden

Wenn die Array-Größe bekannt und klein ist, ist dies normalerweise der effizienteste Ansatz zum Codieren eines Problems.

Auf der anderen Seite, wenn Sie die Array-Theorie verwenden entscheiden, können Sie die Initialisierung in Ihrer Frage kodieren als:

(declare-const a (Array Int Int)) 
(assert (= (select a 0) 10)) 
... 
(assert (= (select a 7) 7)) 

Hier wird das ganze Beispiel in SMT 2.0-Format codiert ist:

http://rise4fun.com/Z3/iwo

Beachten Sie, dass ein Update für dieses Array zu codieren. Zum Beispiel die C-Anweisung a[3] = 5, wir müssen eine neue Array-Variable erstellen, die das Array nach dieser Zuweisung darstellt. Die kompakteste Art und Weise verwendet den store Ausdruck:

(declare-const a1 (Array Int Int)) 
(assert (= a1 (store a 3 5))) 

Hier ist das vollständige Beispiel mit dem Update.

http://rise4fun.com/Z3/Kpln

Sie können sich auch die Python/C++ /. Net APIs. Sie ermöglichen es uns, Beispiele wie Ihre in einer kompakteren Weise zu kodieren. Die Idee besteht darin, Funktionen zu implementieren, die häufig verwendete Muster wie die Array-Initialisierung kodieren. Hier ist Ihre Feldinitialisierung Beispiel in Python:

http://rise4fun.com/Z3Py/AAD