Ich werde ein Array mit fester Größe erstellen und es mit einigen Werten initialisieren.
Zum Beispiel der folgende C ++ Code:
%Vor%Gibt es in Z3 einige Dienstprogramme, um es zu modellieren?
Z3 unterstützt die Array-Theorie, wird aber normalerweise verwendet, um unbegrenzte Arrays oder Arrays, die sehr groß sind, zu codieren. 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 keine Theorien verwenden, muss die Codierung eines Array-Zugriffs wie a[i] als großes Wenn-dann-Format codiert werden. sonst Begriff wie
(ite (= i 0) a0 (ite (= i 1) a1 ...))
Wenn die Array-Größe bekannt und klein ist, ist dies normalerweise der effizienteste Ansatz zum Codieren eines Problems.
Wenn Sie sich andererseits dazu entschließen, die Array-Theorie zu verwenden, können Sie die Initialisierung in Ihrer Frage wie folgt codieren:
%Vor%Hier ist das ganze Beispiel im SMT 2.0-Format:
Beachten Sie, dass Sie ein Update für dieses Array codieren müssen. 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 Methode verwendet den Ausdruck store :
Hier ist das vollständige Beispiel mit dem Update.
Sie können auch die Python / C ++ /. Net-APIs in Betracht ziehen. 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 Ihr Array-Initialisierungsbeispiel in Python:
Tags und Links z3