Z3 Forall con array

Question

Z3 fornisce sconosciuto per il semplice problema:

(assert
(forall ((y (Array Int Int)))
   (= (select y 1) 0))
 )
(check-sat)

Ho scoperto che diventa sat se si nega il forall, ma questa sembra una cosa particolarmente semplice da non essere in grado di risolvere.

Questo sta causando problemi perché la classe di problemi che voglio risolvere è più simile a,

(declare-fun u () Int)
(assert
 (forall ((y (Array Int Int)) )
     (=> 
        (= u 0) (<= (select y 1) 0))
 )
)
(check-sat)

Dove negare il forall da solo non è lo stesso problema, quindi non è possibile farlo qui. C'è un modo per porre questo tipo di problema a Z3 per ottenere un risultato un / sat?

Answer 1

I problemi con i quantificatori sono sempre problematici con i risolutori SMT, soprattutto se coinvolgono array e quantificatori alternati come nel tuo esempio. Essenzialmente hai exits u. forall y. P(u, y). Z3, o qualsiasi altro risolutore SMT, avrà difficoltà a gestire questo tipo di problemi.

Quando si dispone di un'asserzione quantificata come si fa in cui si trova forallal livello superiore o annidata con exists, la logica diventa semi-decidibile. Z3 utilizza MBQI (istanziazione del quantificatore basata su modello) per risolvere euristicamente tali problemi, ma il più delle volte non riesce a farlo. Il problema non è solo che z3 non è in grado: non esiste una procedura decisionale per tali problemi e z3 fa del suo meglio.

Puoi provare a fornire schemi quantificatori per tali problemi per aiutare z3, ma non vedo un modo semplice per applicarlo nel tuo problema. (I modelli quantificatori si applicano quando si hanno funzioni non interpretate e assiomi quantificati. Vederehttps://rise4fun.com/z3/tutorialcontent/guide#h28). Quindi, non credo che funzionerà per te. Anche se lo facesse, i pattern sono molto difficili da programmare e non sono robusti rispetto ai cambiamenti nelle specifiche che altrimenti potrebbero sembrare innocui.

Se hai a che fare con questi quantificatori, i risolutori SMT probabilmente non sono adatti. Esamina i dimostratori di teoremi semi-automatici come Lean, Isabelle, Coq, ecc., Che sono progettati per gestire i quantificatori in un modo molto più disciplinato. Ovviamente si perde la piena automazione, ma la maggior parte di questi strumenti può utilizzare un risolutore SMT per eliminare gli obiettivi secondari che sono abbastanza "facili". In questo modo, esegui comunque il "sollevamento di carichi pesanti" manualmente, ma la maggior parte degli obiettivi secondari viene gestita automaticamente da z3. (Soprattutto nel caso di Lean, vedi qui:https://leanprover.github.io/)

Answer 2

C'è una parentesi di chiusura (destra) in più, che deve essere rimossa. Inoltre, aggiungi assert prima dell'istruzione forall.

(assert ( forall ( (y (Array Int Int) ) ) 
   (= (select y 1) 0) 
))
(check-sat)

Esegui il codice sopra e dovresti ottenere unsat come risposta.

Per il secondo programma, la risposta alias potrebbe esserti utile.