Creare un array con dimensioni fisse e inizializzarlo

Question

Creerò un array con dimensioni fisse e lo inizializzerò con alcuni valori.

Ad esempio, il seguente codice C++:

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

Ci sono alcuni programmi di utilità in Z3 al modello IT?

Answer 1

Z3 supporta la teoria dell'array, ma viene solitamente utilizzata per codificare array illimitati o array molto grandi. Per grandi, intendo il numero di accessi alla matrice (cioè, seleziona) nella formula è molto più piccolo della dimensione effettiva della matrice. Dovremmo chiederci: "abbiamo davvero bisogno di matrici per modellare/risolvere il problema X?". Per matrici di dimensioni fisse come nell'esempio, possiamo usare una variabile diversa per ogni posizione dell'array. Esempio: a0 per a[0], a1 per a[1], ecc Naturalmente, se non usiamo teorie, quindi codificante un accesso array come a[i] deve essere codificato come un grande termine come

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

if-then-else

Se la dimensione dell'array è nota e piccola, questo è solitamente l'approccio più efficiente per la codifica di un problema.

D'altra parte, se si decide di utilizzare la teoria matrice, è possibile codificare l'inizializzazione nella sua domanda come:

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

Ecco l'intero esempio codificato in formato SMT 2.0:

http://rise4fun.com/Z3/iwo

Si noti che per codificare un aggiornamento su questo array. Ad esempio, l'istruzione C a[3] = 5, dobbiamo creare una nuova variabile di matrice che rappresenta l'array dopo questo compito. Il modo più compatto utilizza l'espressione store:

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

Ecco l'esempio completo con l'aggiornamento.

http://rise4fun.com/Z3/Kpln

Si può anche considerare i/C /. Net API Python ++. Ci permettono di codificare esempi come il tuo in un modo molto più compatto. L'idea è di implementare funzioni che codificano schemi comunemente usati come l'inizializzazione dell'array. Ecco l'array esempio di inizializzazione in Python:

http://rise4fun.com/Z3Py/AAD