Benutzerdefinierte Vereinfacher
Früher (dh im letzten Jahr) konnten wir Theorie-Plugins als Hack verwenden, um benutzerdefinierte Vereinfacher zu implementieren. Das Z3-Dokument enthielt sogarein Beispiel für "prozedurale Anhänge".
Meine Frage ist sehr einfach; Gibt es eine Möglichkeit, mit Z3 4.x dasselbe Ziel zu erreichen?
Insbesondere bin ich daran interessiert, Z3 extern berechnete Auswertungen für Grundbegriffe zur Verfügung zu stellen.