Quantifiers and patterns (formula QBF)

Question

Sto provando a codificare un QBF nella sintassi smt-lib 2 per z3. Esecuzione risultati Z3 in un avvertimento

ATTENZIONE: non è riuscito a trovare un modello per quantificatore (quantificatore id: k 14)

e il risultato soddisfacibilità è "sconosciuto".

Il codice è il seguente:

(declare-fun R (Bool Bool Bool Bool) Bool) 
(assert 
    (forall ((x2 Bool) (x3 Bool)) 
    (exists ((y Bool)) 
     (forall ((x1 Bool)) 
     (R x1 x2 x3 y) 
    ) 
    ) 
) 
) 
(check-sat) 

mi sono liberato del warning riscrivendo il codice per

(set-option :auto-config false) 
(set-option :mbqi false) 
(declare-fun R (Bool Bool Bool Bool) Bool) 
(declare-fun x1() Bool) 
(declare-fun x2() Bool) 
(declare-fun x3() Bool) 
(declare-fun y() Bool) 
(assert 
    (forall ((x2 Bool) (x3 Bool)) 
    (! 
    (exists ((y Bool)) 
    (! 
     (forall ((x1 Bool)) 
     (! 
     (R x1 x2 x3 y) 
     :pattern((R x1 x2 x3 y))) 
    ) 
    :pattern((R x1 x2 x3 y))) 
    ) 
    :pattern((R x1 x2 x3 y))) 
) 
) 
(check-sat) 

Il risultato del-query satellitare, tuttavia, resta "sconosciuto".

Immagino di dover ottenere gli schemi giusti? Come posso specificarli per quantificatori annidati? Tuttavia, gli esempi più semplici con quantificatori sembrano funzionare senza annotazioni di modello.

La risposta a What is the reason behind the warning message in Z3: "failed to find a pattern for quantifier (quantifier id: k!18) " e la guida z3 non mi hanno aiutato troppo, purtroppo.

Answer 1

Questo messaggio di avviso può essere ignorato. Si tratta solo di informarvi che il motore di corrispondenza elettronica non sarà in grado di elaborare questa formula quantificata.

L'abbinamento elettronico è efficace solo per mostrare che un problema non è soddisfacente. Dal momento che il tuo esempio è soddisfacente, l'E-matching non sarà molto utile. Cioè, Z3 non sarà in grado di restituire sat utilizzando il motore di corrispondenza elettronica. La quantificazione di quantificatori basata su modello (MBQI) è l'unico motore in Z3 in grado di dimostrare che i problemi che contengono i quantificatori sono soddisfacenti.

Utilizzando la configurazione predefinita, Z3 restituirà sat per l'esempio. Restituisce unknown perché è stato disabilitato il modulo MBQI.

Il motore MBQI garantisce che Z3 sia una procedura di decisione per molti frammenti (vedere http://rise4fun.com/Z3/tutorial/guide). Tuttavia, è molto costoso in generale e dovrebbe essere disabilitato quando sono sufficienti risposte rapide e approssimative. In questo caso, unknown può essere letto come probably sat. Strumenti di verifica come VCC disabilitano il modulo MBQI poiché non è in grado di decidere le formule da loro prodotte. Cioè, le formule prodotte da VCC non sono in nessuno dei frammenti che possono essere decisi dal motore MBQI. Diciamo che un frammento può essere deciso da Z3 quando per qualsiasi formula nel frammento Z3 restituirà sat o unsat (ad esempio, non restituisce unknown). Naturalmente, questa affermazione presuppone che abbiamo una quantità illimitata di risorse. Cioè, Z3 può anche fallire (ad esempio, restituire unknown) per i frammenti decidibili quando esaurisce la memoria, o è stato specificato un timeout dall'utente.

Infine, Z3 3.2 ha un bug nel motore MBQI. Il bug è stato corretto e non ha alcun problema. Se ti serve posso darti una versione preliminare di Z3 4.0 che contiene la correzione del bug.