Uso della riscrittura dei termini nelle procedure decisionali per aritmetica bit-vettoriale

Question

Sto lavorando a un progetto il cui obiettivo è l'uso della riscrittura dei termini per risolvere/semplificare i problemi aritmetici bit-vector a dimensione fissa, che è qualcosa di utile da fare passo precedente ad alcune procedure decisionali come quelle basate sul bit-blasting. Il termine riscrittura può risolvere il problema o produrre in altro modo un problema equivalente molto più semplice, quindi la combinazione di entrambi può portare ad una notevole accelerazione.

Sono consapevole che molti solutori SMT implementano questa strategia (ad esempio, Boolector, Beaver, Alt-Ergo o Z3), ma è difficile trovare documenti/relazioni tecniche/ecc in cui questi passaggi di riscrittura sono descritti in dettaglio . In generale, ho trovato solo documenti in cui gli autori descrivono tali passaggi di semplificazione in alcuni paragrafi. Vorrei trovare un documento che spieghi in dettaglio l'uso della riscrittura a termine: fornire esempi di regole, discutere la convenienza della riscrittura AC e/o altri assiomi equazionali, uso di strategie di riscrittura, ecc.

Per ora, ho solo ho trovato il rapporto tecnico A Decision Procedure for Fixed-Width Bit-Vectors che descrive i passaggi di normalizzazione/semplificazione eseguiti da CVC Lite, e vorrei trovare altri rapporti tecnici come questo! Ho anche trovato un poster su Term rewriting in STP ma è solo un breve riassunto.

Ho già visitato i siti web di questi solutori SMT e ho cercato nei loro Pubblicazioni pagine ...

Gradirei qualsiasi riferimento, o qualsiasi spiegazione di come riscrittura termine viene utilizzato nelle versioni attuali di noti risolutori SMT. Sono particolarmente interessato a Z3 perché sembra avere una delle fasi di semplificazione più intelligenti. Ad esempio, Z3 3. * ha introdotto una nuova procedura di decisione del vettore di bit ma, sfortunatamente, non sono riuscito a trovare alcun documento che lo descrivesse.

Answer 1

Sono d'accordo con te. È difficile trovare documenti che descrivono le fasi di pre-elaborazione utilizzate nei moderni risolutori SMT. Molti sviluppatori di solutori SMT concordano sul fatto che questi passaggi di pre-elaborazione sono molto importanti per la teoria del Bit-Vector. Credo che queste tecniche non vengano pubblicate per diversi motivi: la maggior parte di loro è un piccolo trucco che di per sé non rappresenta un contributo scientifico significativo; la maggior parte delle tecniche funziona solo nel contesto di un particolare sistema; una tecnica che può sembrare funzionare molto bene con il risolutore A, non funziona con il risolutore B. Credo che avere risolutori SMT open source sia l'unico modo per risolvere questo problema. Anche se pubblichiamo le tecniche utilizzate in un risolutore specifico A, sarebbe molto difficile riprodurre il comportamento effettivo del risolutore A senza vederne il codice sorgente.

In ogni caso, ecco un riepilogo della preelaborazione eseguita da Z3 e dettagli importanti.

• Diverse regole di semplificazione possono ridurre questa dimensione localmente, ma aumentarla globalmente. Un semplice strumento deve evitare l'accumulo di memoria causato da questo tipo di semplificazione. Puoi trovare esempi a: http://research.microsoft.com/en-us/um/people/leonardo/mit2011.pdf

• Il primo passaggio di semplificazione esegue solo semplificazioni locali che preservano l'equivalenza. Esempi:

2*x - x -> x 
x and x -> x 

• Avanti, Z3 esegue costante di propagazione. Data un'uguaglianza t = v dove v è un valore. Sostituisce t ovunque con v.

t = 0 and F[t] -> t = 0 and F[0] 

• Successivamente, esegui eliminazione gaussiana per Bit-vettori. Tuttavia, vengono eliminate solo le variabili che si verificano al massimo due volte nelle espressioni aritmetiche. Questa restrizione viene utilizzata per impedire un aumento del numero di sommatori e moltiplicatori nella formula. Ad esempio, supponiamo di avere x = y+z+w e x a p(x+z), p(x+2*z), p(x+3*z) e p(x+4*z). Quindi, dopo aver eliminato x, avremmo p(y+2*z+w), p(y+3*z+w), p(y+4*z+w) e p(y+5*z+w). Sebbene abbiamo eliminato x, abbiamo più adduttori che la formula originale.

• Successivamente, elimina le variabili non vincolate. Questo approccio è descritto nella tesi di dottorato di Robert Brummayer e Roberto Brutomesso.

• Quindi, viene eseguito un altro ciclo di semplificazione. Questa volta, vengono eseguite semplificazioni contestuali locali. Queste semplificazioni sono potenzialmente molto costose. Quindi, viene utilizzata una soglia sul numero massimo di nodi da visitare (il valore predefinito è 10 milioni). locale contesto semplificazione contiene norme quali

(x != 0 or y = x+1) -> (x != 0 or y = 1) 

• Avanti, cerca di minimizzare il numero di moltiplicatori che utilizzano distributività. Esempio:

a b + un c -> (b + c) * una

• Poi, si cerca di ridurre al minimo il numero di vipere e moltiplicatori applicando associatività e commutatività. Supponiamo che la formula contenga i termini a + (b + c) e a + (b + d). Quindi, Z3 li riscriverà a: (a+b)+c e (a+b)+d. Prima della trasformazione, Z3 avrebbe dovuto codificare 4 sommatori. Dopo, solo tre sommatori devono essere codificati poiché Z3 utilizza espressioni completamente condivise.

• Se la formula contiene solo l'uguaglianza, la concatenazione, l'estrazione e operatori simili. Quindi, Z3 utilizza un risolutore specializzato basato sulla chiusura di unione e congruenza.

• In caso contrario, blocca tutto, utilizza AIG per ridurre al minimo la formula booleana e invoca il relativo solutore SAT.

Answer 2

Z3 utilizza la riscrittura per molti la semplificazione eseguita durante la pre-elaborazione. Molte delle regole di riscrittura utilizzati per la strategia UFBV (con quantificatori) sono descritte al dettaglio nel seguente articolo:

Wintersteiger, Hamadi, de Moura: Efficiently Solving Quantified Bit-Vector Formulas, FMCAD, 2010