formule di risolutore interno in z3

Question

Lo strumento di dimostrazione del teorema z3 impiega molto tempo per risolvere una formula, che ritengo dovrebbe essere in grado di gestire facilmente. Per capire meglio e possibilmente ottimizzare il mio input per z3, volevo vedere i vincoli interni che z3 genera come parte del suo processo di risoluzione. Come si stampa la formula che z3 produce per i suoi risolutori back-end, quando si usa z3 dalla riga di comando?

Answer 1

Lo strumento da riga di comando Z3 non ha questa opzione. Inoltre, Z3 contiene diversi solutori e fasi di pre-elaborazione. Non è chiaro quale passaggio sarebbe utile per te. Il codice sorgente Z3 è disponibile al numero https://github.com/Z3Prover/z3. Quando Z3 è compilato in modalità di debug, fornisce un'opzione di riga di comando aggiuntiva -tr:<tag>. Questa opzione può essere utilizzata per scaricare in modo selettivo le informazioni. Ad esempio, il file di origine nlsat_solver.cpp contiene le seguenti istruzioni:

TRACE("nlsat", tout << "starting search...\n"; display(tout); 
       tout << "\nvar order:\n"; 
       display_vars(tout);); 

Il comando opzione della riga di -tr:nlsat istruirà Z3 per eseguire le istruzioni di cui sopra. tout è il flusso di output di traccia. Sarà memorizzato nel file .z3-trace. La sorgente Z3 è piena di questi comandi TRACE. Poiché il codice è disponibile, possiamo anche aggiungere i nostri comandi di tracciamento nel codice.

Se pubblichi il tuo esempio, posso dirti quali componenti Z3 sono usati per pre-processare e risolvere. Quindi, possiamo selezionare quali "tag" dovremmo abilitare per la traccia.

EDIT (dopo la constraints sono state inviate): Il tuo esempio è nel misto intero & reale aritmetica non lineare. Il nuovo risolutore aritmetico non lineare (nlsat) in Z3 non supporta to_int. Pertanto, il risolutore generico Z3 viene utilizzato per risolvere il problema. Sebbene questo risolutore accetti quasi tutto, non è nemmeno completo per l'aritmetica reale non lineare. Il supporto non lineare su questo risolutore si basa su: analisi a intervalli e calcoli di base di Grobner. Questo risolutore è implementato nella cartella src/smt (nello unstable branch). Il modulo aritmetico è implementato nei file theory_arith*. Un'opzione da riga di comando buona traccia è -tr:after_reduce. Visualizzerà l'insieme di vincoli dopo la pre-elaborazione. Il collo di bottiglia è il modulo aritmetico (theory_arith*).

Osservazioni supplementari:

• il problema è in un frammento indecidibile: mixed integer & reale aritmetica lineare. Cioè, è impossibile scrivere un suono e un risolutore completo per questo frammento. Naturalmente, possiamo scrivere un solutore che risolva le situazioni che troviamo in pratica. Credo che sia possibile estendere lo nlsat per gestire lo to_int.

• Se si evita lo to_int, sarà possibile utilizzare nlsat. Il problema sarà nel vero frammento aritmetico reale non lineare. Capisco che questo può essere difficile, dal momento che il to_int sembra essere un elemento chiave nella codifica.

• Il codice nel ramo "unstable" su z3.codeplex.com è molto meglio organizzato rispetto alla versione ufficiale nel ramo "master". Lo fonderò presto con il ramo "master".Puoi recuperare il ramo "unstable" se vuoi giocare con il codice sorgente.

• Il ramo "unstable" utilizza un nuovo sistema di generazione. È possibile creare la versione di rilascio con il supporto di traccia. Devi solo usare l'opzione -t durante la generazione del Makefile.

script python/mk_make.py -t

• Quando Z3 viene compilato in modalità debug, l'opzione AUTO_CONFIG=false per impostazione predefinita. Pertanto, per riprodurre il comportamento della modalità "rilascio", è necessario fornire l'opzione della riga di comando AUTO_CONFIG=true.