Si sta rispondendo a una domanda che si presenta regolarmente: come posso mescolare i tipi di dati e gli array (come set, multi-set o tipi di dati nell'intervallo)?
Come detto sopra, Z3 non supporta la miscelazione dei tipi di dati e le matrici in un'unica dichiarazione. Una soluzione è lo sviluppo di un risolutore personalizzato per la teoria di matrice dati + array mista . Z3 contiene le API programmatiche per lo sviluppo di solutori personalizzati.
È ancora utile sviluppare questo esempio per illustrare le funzionalità e le limitazioni delle teorie di codifica con quantificatori e trigger. Consentitemi di semplificare il vostro esempio usando semplicemente A. Come soluzione, potete definire un ordinamento ausiliario. Tuttavia, la soluzione alternativa non è l'ideale. Illustra un po 'di' hacking 'dell'assioma . Si basa sulla semantica operativa di come i quantificatori vengono istanziati durante la ricerca.
(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))
Quindi definire le biiezioni tra (Set 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)))
Questo è quasi ciò che afferma la dichiarazione del tipo di dati. Per far rispettare fondatezza è possibile associare un numero ordinale con i membri di A e far rispettare che i membri del SetA sono più piccoli in ordine fondato:
(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 gli assiomi finora, a1 può essere un membro di si.
(push)
(assert (select sa1 a1))
(assert (= s1 (injSA sa1)))
(assert (= a1 (cons v s1)))
(check-sat)
(get-model)
(pop)
Ora associare un numero ordinale con i membri di 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)))
per esemplificazione quantifier impostazione predefinita in Z3 è pattern-based. La prima affermazione quantificata sopra non verrà istanziata su tutte le istanze rilevanti . Si può invece affermare:
(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)))))
Assiomi come questi, che utilizzano due modelli (chiamati un multi-pattern) sono piuttosto costosi. Producono istanze per ogni coppia di (selezionare x2 a) e (contro v x1)
Il vincolo di appartenenza di prima è ora insoddisfacibile.
(push)
(assert (select sa1 a1))
(assert (= s1 (injSA sa1)))
(assert (= a1 (cons v s1)))
(check-sat)
(pop)
ma i modelli non sono necessariamente ancora ben formati. il valore predefinito del set è 'true', che significherebbe che il modello implica che esiste un ciclo di appartenenza quando non ce n'è uno.
(push)
(assert (not (= (cons v s1) a1)))
(assert (= (projSA s1) sa1))
(assert (select sa1 a1))
(check-sat)
(get-model)
(pop)
Siamo in grado di approssimare modelli più fedeli utilizzando il seguente approccio per imporre che le serie che vengono utilizzati in tipi di dati sono finite. Ad esempio, ogni volta che c'è un controllo di appartenenza su un set x2, , applichiamo che il valore "predefinito" dell'insieme è "falso".
(assert (forall ((x2 (Set A)) (a A))
(! (not (default x2))
:pattern ((select x2 a)))))
In alternativa, quando si verifica un insieme in un costruttore di dati di tipo è finita
(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)
Durante l'inserimento di assiomi aggiuntivi, Z3 produce la risposta 'ignoto' e inoltre modello che viene prodotto indica che il dominio SetA è finito (un singleton). Quindi, mentre potevamo applicare le patch di default , questo modello non soddisfa ancora gli assiomi. Soddisfa lo solo per l'istanza modulo assiomi.