Está abordando una pregunta que se presenta de forma regular: ¿cómo puedo mezclar tipos de datos y matrices (como conjuntos, conjuntos múltiples o tipos de datos en el rango)?
Como se indicó anteriormente, Z3 no admite mezclar tipos de datos y matrices en una sola declaración. Una solución es desarrollar un solucionador personalizado para la teoría de matriz de datos mixtos . Z3 contiene API programáticas para desarrollar solucionadores personalizados.
Aún es útil desarrollar este ejemplo para ilustrar las capacidades y limitaciones de las teorías de codificación con cuantificadores y disparadores. Déjeme simplificar su ejemplo simplemente usando A. Como solución alternativa, puede definir una ordenación auxiliar. La solución no es ideal, sin embargo. Ilustra algo de axioma 'hacking'. Se basa en la semántica operacional de cómo se instancian los cuantificadores durante la búsqueda.
(set-option :model true) ; We are going to display models.
(set-option :auto-config false)
(set-option :mbqi false) ; Model-based quantifier instantiation is too powerful here
(declare-sort SetA) ; Declare a custom fresh sort SetA
(declare-datatypes() ((A f1 (cons (value Int) (a SetA)))))
(define-sort Set (T) (Array T Bool))
A continuación, defina las biyecciones entre (Conjunto A), SetA.
(declare-fun injSA ((Set A)) SetA)
(declare-fun projSA (SetA) (Set A))
(assert (forall ((x SetA)) (= (injSA (projSA x)) x)))
(assert (forall ((x (Set A))) (= (projSA (injSA x)) x)))
Esto es casi lo que declara la declaración de tipo de datos. Hacer cumplir bien fundado puede asociar un ordinal con miembros de una y hacer cumplir que los miembros de SETA son más pequeños en la ordenación fundados:
(declare-const v Int)
(declare-const s1 SetA)
(declare-const a1 A)
(declare-const sa1 (Set A))
(declare-const s2 SetA)
(declare-const a2 A)
(declare-const sa2 (Set A))
Con los axiomas hasta ahora, a1 puede ser un miembro de sí mismo.
(push)
(assert (select sa1 a1))
(assert (= s1 (injSA sa1)))
(assert (= a1 (cons v s1)))
(check-sat)
(get-model)
(pop)
ahora Asociamos un número ordinal con los miembros de A.
(declare-fun ord (A) Int)
(assert (forall ((x SetA) (v Int) (a A))
(=> (select (projSA x) a)
(> (ord (cons v x)) (ord a)))))
(assert (forall ((x A)) (> (ord x) 0)))
Por instanciación cuantificador defecto en Z3 es basado en patrones. La primera afirmación cuantificada anterior no se instanciará en todas las instancias relevantes de . en su lugar se puede plantear:
(assert (forall ((x1 SetA) (x2 (Set A)) (v Int) (a A))
(! (=> (and (= (projSA x1) x2) (select x2 a))
(> (ord (cons v x1)) (ord a)))
:pattern ((select x2 a) (cons v x1)))))
axiomas como estos, que utilizan dos patrones (llamados un multi-patrón) son bastante caros. Generan instancias para cada par de (seleccione x2 a) y (contra v x1)
La restricción de membresía anterior no es satisfactoria.
(push)
(assert (select sa1 a1))
(assert (= s1 (injSA sa1)))
(assert (= a1 (cons v s1)))
(check-sat)
(pop)
pero los modelos no están necesariamente bien formados todavía. el valor predeterminado del conjunto es 'verdadero', que significa que el modelo implica que hay un ciclo de membresía cuando no hay uno.
(push)
(assert (not (= (cons v s1) a1)))
(assert (= (projSA s1) sa1))
(assert (select sa1 a1))
(check-sat)
(get-model)
(pop)
Podemos aproximar modelos más fieles mediante el uso de el siguiente enfoque para hacer cumplir que los conjuntos que se utilizan en tipos de datos son finitos. Por ejemplo, siempre que haya una verificación de membresía en un conjunto x2, , exigimos que el valor 'predeterminado' del conjunto sea 'falso'.
(assert (forall ((x2 (Set A)) (a A))
(! (not (default x2))
:pattern ((select x2 a)))))
Alternativamente, siempre que se produce un conjunto en un constructor de tipo de datos es finito
(assert (forall ((v Int) (x1 SetA))
(! (not (default (projSA x1)))
:pattern ((cons v x1)))))
(push)
(assert (not (= (cons v s1) a1)))
(assert (= (projSA s1) sa1))
(assert (select sa1 a1))
(check-sat)
(get-model)
(pop)
A lo largo de la inclusión de axiomas adicionales, Z3 produce la respuesta 'desconocido' y además el modelo que se produce indica que el dominio SetA es finito (un singleton). Entonces, si bien pudimos corregir los valores predeterminados , este modelo aún no satisface los axiomas. Satisface la instanciación del módulo de axiomas solamente.