Ich möchte sehen, welche Muster Z3 für einige Quantifizierer in meinen Formeln verwendet.Zeigen Sie, welche Muster Z3 für Quantoren ergibt
This comment schlägt vor, dass es möglich sein könnte, aber ich konnte keine weiteren Details finden.
Wie bekomme ich Z3, um diese Informationen zu drucken?
Basierend auf einem helpful comment von Christoph, fand ich, dass in den Debug-Modus den Aufbau Z3 (-d zu mk_make.py während des Erstellungsprozesses passieren) und dann -v:10 auf der Befehlszeile auf die resultierenden Drucke Z3 gefolgert Muster verläuft.
Der Ausdruck der abgeleiteten Muster war eine neue Ergänzung und nur zum Debuggen. Der Weg, dies zu ermöglichen, und das Format der Ausgabe werden sich sehr wahrscheinlich sehr bald ändern, also hänge nicht davon ab. (Außerdem werden nur die abgeleiteten Muster und möglicherweise nicht alle davon gedruckt.) –
Danke für die Warnung. Ich plane, dies nur zum Debuggen zu verwenden, daher sind diese Einschränkungen keine große Sache. –
Derzeit können Sie diese Informationen nur über Debug-Traces im Debug-Modus drucken. Es gibt keine praktische Möglichkeit, diese Informationen lesbar anzuzeigen. Es ist immer noch auf der Todo-Liste und ich habe begonnen, einige Dinge dazu in einem separaten Zweig hinzuzufügen, aber es wird noch einige Zeit dauern, um das bequem zu verwenden. –
@ChristophWintersteiger Kannst du mir sagen, wie man es im Debug-Modus macht (auch wenn es nicht lesbar ist)? –
Ich habe einen Weg gefunden, es mit einem Debug Build von Z3 zu tun. Ich bin zuversichtlich, dass dies in normalen Builds eines Tages möglich sein wird. –