ini-option CASE_SPLIT produce un modello strano

Question

Mentre lavoro sulla mia tesi di master con z3 ho trovato qualcosa di strano che non riesco a capire. Spero che tu possa aiutarmi. :)

SMT-file che ho scritto si presenta così:

(set-logic QF_UF) 
(set-info :smt-lib-version 2.0) 

;Declare sort Node and its objects. 
(declare-sort Node 0) 
(declare-fun n0() Node) 
(declare-fun n1() Node) 

;Predicate 
(declare-fun dead_0 (Node) Bool) 
;Abbreviation 
(declare-fun I() Bool) 

;initial configuration 
(assert(= I (and 
(not(= n0 n1)) 
(not(dead_0 n0)) 
(dead_0 n1)))) 

;Predicate 
(declare-fun dead_1 (Node) Bool) 
;variable 
(declare-fun m0_1() Node) 

;Abbreviation for Transformation 
(declare-fun TL1_1() Bool) 

;Transformation1neuerKnoten1 
(assert(or (= m0_1 n0)(= m0_1 n1))) 

;Is the whole formula satisfiable? 
(assert(= (and I TL1_1) true)) 
(check-sat) 
(get-model) 

Tutto funziona abbastanza bene durante l'utilizzo Z3 come uno strumento a riga di comando con il default-opzioni. Il modello generato contiene:

;; universe for Node: 
;; Node!val!0 Node!val!1 
;; ----------- 

e

(define-fun n0() Node 
Node!val!0) 
(define-fun n1() Node 
Node!val!1) 
(define-fun m0_1() Node 
Node!val!0) 

Quindi il mio m0_1 variabile è legata al n0 nodo.

Quindi ho usato z3 con un file ini contenente solo CASE_SPLIT=5. Il risultato è stato uno strano modello. A mio avviso la differenza è in pratica che la mia variabile m0_1 NON è associata a nessuno dei miei nodi n0 o n1. Il modello prodotto contiene:

;; universe for Node: 
;; Node!val!2 Node!val!0 Node!val!1 
;; ----------- 

e

(define-fun n0() Node 
Node!val!0) 
(define-fun n1() Node 
Node!val!1) 
(define-fun m0_1() Node 
Node!val!2) 

Quindi la mia domanda è questa: perché Z3 creare un altro nodo (Node!val!2) e perché è la mia variabile m0_1 legato a questo nuovo nodo? Ho pensato che una delle mie asserzioni ((assert(or (= m0_1 n0)(= m0_1 n1)))) lo avrebbe proibito.

Grazie in anticipo! :)

Answer 1

Z3 ha una funzionalità chiamata "propagazione della pertinenza". Questa caratteristica è molto efficace per problemi contenenti quantificatori, ma di solito è un sovraccarico per problemi quantificatori. L'opzione da riga di comando RELEVANCY=0 disabilita la propagazione della pertinenza e lo consente RELEVANCY=2 o RELEVANCY=1. L'opzione CASE_SPLIT=5 presuppone che la propagazione della pertinenza sia abilitata. Se forniamo CASE_SPLIT=5 RELEVANCY=0, quindi Z3 genererà un messaggio di avviso

WARNING: relevacy must be enabled to use option CASE_SPLIT=3, 4 or 5 

e, ignora l'opzione.

Inoltre, per impostazione predefinita, Z3 utilizza una funzionalità di "configurazione automatica". Questa funzione analizza la formula di input e regola la configurazione Z3 per l'istanza specificata. Quindi, nel tuo esempio, accade quanto segue:

1. offrono la possibilità CASE_SPLIT=5
2. Quando Z3 convalida le opzioni della riga di comando, la pertinenza di propagazione è disattivato e non viene generato alcun messaggio di avviso.
3. Z3 esegue la procedura di configurazione automatica e, poiché l'esempio è privo di quantificatori, disabilita la propagazione della pertinenza RELEVANCY=0. Ora, viene utilizzata una configurazione incoerente e Z3 produce il risultato errato.

Per evitare questo problema, se si utilizza CASE_SPLIT=5, allora si dovrebbe anche usare AUTO_CONFIG=false (disabilita la configurazione automatica) e RELEVANCY=2 (abilita pertinenza di propagazione). Così, la linea di comando dovrebbe essere:

z3 CASE_SPLIT=5 AUTO_CONFIG=false RELEVANCY=2 file.smt2 

Nella prossima release (Z3 4.2), farò Z3 per visualizzare il messaggio di avviso se l'utente tenta di impostare CASE_SPLIT=5 quando la configurazione automatica è abilitata.