È possibile utilizzare Z3 per ragionare su sottostringhe?

Question

Sto cercando di utilizzare Z3 per ragionare sulle sottostringhe e ho riscontrato un comportamento non intuitivo. Z3 restituisce 'sat' quando viene richiesto di determinare se 'xy' appare all'interno di 'xy', ma restituisce 'unknown' quando viene chiesto se 'x' è in 'x' o 'x' è in 'xy'.

Ho commentato il seguente codice per illustrare questo comportamento:

(set-logic AUFLIA) 
(declare-sort Char 0) 

;characters to build strings are _x_ and _y_ 
(declare-fun _x_() Char) 
(declare-fun _y_() Char) 
(assert (distinct _x_ _y_)) 

;string literals 
(declare-fun findMeX() (Array Int Char)) 
(declare-fun findMeXY() (Array Int Char)) 
(declare-fun x() (Array Int Char)) 
(declare-fun xy() (Array Int Char)) 
(declare-fun length ((Array Int Char)) Int) 

;set findMeX = 'x' 
(assert (= (select findMeX 0) _x_)) 
(assert (= (length findMeX) 1)) 

;set findMeXY = 'xy' 
(assert (= (select findMeXY 0) _x_)) 
(assert (= (select findMeXY 1) _y_)) 
(assert (= (length findMeXY) 2)) 

;set x = 'x' 
(assert (= (select x 0) _x_)) 
(assert (= (length x) 1)) 

;set xy = 'xy' 
(assert (= (select xy 0) _x_)) 
(assert (= (select xy 1) _y_)) 
(assert (= (length xy) 2)) 

Ora che il problema è impostato, cerchiamo di trovare le stringhe:

;search for findMeX='x' in x='x' 

(push 1) 
(assert 
    (exists 
    ((offset Int)) 
    (and 
     (<= offset (- (length x) (length findMeX))) 
     (>= offset 0) 
     (forall 
     ((index Int)) 
     (=> 
      (and 
      (< index (length findMeX)) 
      (>= index 0)) 
      (= 
      (select x (+ index offset)) 
      (select findMeX index))))))) 

(check-sat) ;'sat' expected, 'unknown' returned 
(pop 1) 

Se noi invece cerchiamo findMeXY in xy, il risolutore restituisce 'sat', come previsto. Sembrerebbe che dal momento che il risolutore può gestire questa query per 'xy', dovrebbe essere in grado di gestirlo per 'x'. Inoltre, se si cerca findMeX='x' in 'xy='xy', viene restituito "sconosciuto".

Qualcuno può suggerire una spiegazione, o forse un modello alternativo per esprimere questo problema all'interno di un risolutore SMT?

Answer 1

La risposta breve per il comportamento osservato è: Z3 restituisce "sconosciuto" perché le asserzioni contengono quantificatori.

Z3 contiene molte procedure ed euristiche per il trattamento dei quantificatori. Z3 utilizza una tecnica chiamata Quantificazione basata sui modelli (Instant Quantum Instantiation, MBQI) per la creazione di modelli per la soddisfazione di query come la vostra. Il primo passo è che questa procedura consiste nel creare un'interpretazione del candidato basata su un'interpretazione che soddisfi le asserzioni libere del quantificatore. Sfortunatamente, nell'attuale Z3, questo passaggio non interagisce in modo fluido con la teoria dell'array. Il problema di base è che l'interpretazione costruita dalla teoria dell'array non può essere modificata da questo modulo.

Una domanda equa è: perché funziona quando rimuoviamo i comandi push/pop? Funziona perché Z3 utilizza passaggi di semplificazione (preelaborazione) più aggressivi quando non vengono utilizzati comandi di risoluzione incrementale (come i comandi push e pop).

Vedo due possibili soluzioni per il problema.

• È possibile evitare i quantificatori e continuare a utilizzare la teoria degli array. Questo è fattibile nel tuo esempio, dal momento che conosci la lunghezza di tutte le "stringhe". Quindi, puoi espandere il quantificatore. Sebbene questo approccio possa sembrare scomodo, viene utilizzato nella pratica e in molti strumenti di verifica e test.

• È possibile evitare la teoria dell'array. Dichiarate la stringa come un tipo non interpretato, come avete fatto per Char. Quindi, dichiarate una funzione char, che dovrebbe restituire il carattere i-esimo di una stringa. È possibile assiomatizzare questa operazione. Ad esempio, si può dire che due stringhe sono uguali se hanno la stessa lunghezza e contengono gli stessi caratteri:

(assert (forall ((s1 String) (s2 String)) 
       (=> (and 
        (= (length s1) (length s2)) 
        (forall ((i Int)) 
          (=> (and (<= 0 i) (< i (length s1))) 
           (= (char-of s1 i) (char-of s2 i))))) 
        (= s1 s2)))) 

Il seguente link contiene lo script codificato utilizzando il secondo approccio: http://rise4fun.com/Z3/yD3

Il secondo approccio è più attraente e ti consentirà di dimostrare proprietà più complesse sulle stringhe. Tuttavia, è molto facile scrivere formule quantificate soddisfacenti che Z3 non sarà in grado di costruire un modello. Il Z3 Guide descrive le principali funzionalità e limitazioni del modulo MBQI. Contiene frammenti decidibili che possono essere gestiti da Z3. BTW, si noti che l'eliminazione della teoria dell'array non sarà un grosso problema se si dispone di quantificatori. La guida mostra come codificare gli array utilizzando quantificatori e funzioni.

Potete trovare ulteriori informazioni su come MBQI opera nei seguenti documenti:

• Complete instantiation for quantified SMT formulas

• Efficiently Solving Quantified Bit-Vector Formula