Quando una formula in Z3 è unsat e (get-proof) viene specificata, esiste un'uscita che non trovo alcuna informazione su cosa sia. Dove posso trovare documentazione a riguardo?Output di controesempio di Z3
A me sembra del tutto illeggibile, è possibile che qualche strumento lo prenda come input?
Cheers, Matt
Le "prove" prodotte dalla Z3 non sono per il consumo umano. Una versione obsoleta del formato è descritta nel documento: Proofs and Refutations, and Z3. Il file z3_api.h ha una lunga descrizione di ciascuna delle regole di prova. Gli identificatori delle regole di prova iniziano con Z3_OP_PR. Sono a conoscenza di due applicazioni che utilizzano gli oggetti prova Z3. I seguenti documenti contengono molti esempi e descrivono come gli oggetti di prova possono essere utilizzati.
1- Test di Teorema interattivo di Isabelle: le prove Z3 vengono ricostruite all'interno di Isabelle utilizzando un nucleo fidato. È possibile trovare diversi documenti che descrivono questo lavoro e il formato di prova Z3 a Sascha Bohme's homepage
Come pad detto, unsat-cores sono molto più semplici da usare.
Grazie mille per i tuoi link. Darò un'occhiata a entrambi i metodi. Quindi grazie anche a @pad! – MattKay
Il comando '(get-unsat-core)' sembra essere quello che vuoi. Esempio ufficiale: http://rise4fun.com/Z3/smtc_core – pad