Crear una matriz con tamaño fijo e inicializarla

Question

Voy a crear una matriz con tamaño fijo e inicializarla con algunos valores.

Por ejemplo, el siguiente código 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; 

¿Hay algunas utilidades en Z3 modelarlo?

Answer 1

Z3 admite la teoría de matrices, pero generalmente se utiliza para codificar matrices ilimitadas o matrices que son muy grandes. En general, me refiero a la cantidad de accesos de matriz (es decir, seleccionados) en su fórmula es mucho menor que el tamaño real de la matriz. Deberíamos preguntarnos: "¿realmente necesitamos arreglos para modelar/resolver el problema X?". Para matrices de tamaño fijo como en su ejemplo, podemos usar una variable diferente para cada posición de matriz. Ejemplo: a0 para a[0], a1 para a[1], etc. Por supuesto, si no utilizamos teorías, a continuación, que codifica un acceso a una matriz tal como a[i] debe ser codificada como una gran término if-then-else tales como

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

Si el tamaño de la matriz es pequeño y conocido, este suele ser el método más eficiente para codificar un problema.

Por otro lado, si se decide utilizar la teoría de matriz, puede codificar la inicialización en su pregunta como:

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

Aquí es todo el ejemplo codificado en SMT formato 2.0:

http://rise4fun.com/Z3/iwo

Tenga en cuenta que para codificar una actualización en esta matriz. Por ejemplo, la instrucción C a[3] = 5, debemos crear una nueva variable de matriz que represente la matriz después de esta asignación. La forma más compacta utiliza la expresión store:

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

Aquí está el ejemplo completo con la actualización.

http://rise4fun.com/Z3/Kpln

También puede considerar los/C++. API Python/NET. Nos permiten codificar ejemplos como los tuyos de una forma mucho más compacta. La idea es implementar funciones que codifiquen patrones comúnmente utilizados, como la inicialización de matrices. Aquí está el ejemplo inicialización de la matriz en Python:

http://rise4fun.com/Z3Py/AAD