Ich versuche, einige imperative Programm mit HORN-Logik von Z3 (Set-Logik HORN) zu kodieren, aber einige Schwierigkeiten der Definition Klausel (mit SMT2). Kann mir jemand sagen, wo ich eine gute Quelle für Dokumentationen für diese Funktion von Z3 finden kann?HORN Klausel Z3 Dokumentation
Nun, es gibt mehr, wenn es darum geht, ein Programm in Hornklauseln zu "codieren". Zuerst müssen Sie eine entsprechende Beweisregel überprüfen: Hat das Programm rekursive Funktionen, sollten Sie Funktion Zusammenfassung tun? und so weiter.
Es gibt ein paar Papiere zu diesem Thema, aber ich glaube nicht, dass es ein Tutorial über VC Gen gibt. Sie können auch einige Benchmarks im Horn SMT-Format betrachten, um Inspiration zu ziehen: https://svn.sosy-lab.org/software/sv-benchmarks/trunk/clauses/
Fühlen Sie sich frei zu fragen, wenn Sie eine bestimmte Frage haben.