Was ist die C++ - Datei und Methode, wo der DPLL-Algorithmus die Struktur zurückführt?

Question

Ich versuche, die C++ - Datei für Z3 zu finden, wo der Algorithmus zurück verfolgt, wenn es keine Lösung für den aktuellen Zweig finden kann. Ich habe alle Dateien durchgesehen und den Debug-Modus für die Python-Dateien ausprobiert, aber bisher kein Glück. Ich möchte der Methode nur eine print-Anweisung hinzufügen, damit ich weiß, wann sie zu einem vorherigen Knoten zurückkehrt und einen neuen Pfad ausprobiert.

Danke!

Answer 1

Es hängt davon ab, welchen Löser Z3 für Ihr Problem verwendet. Es verwendet normalerweise smt_context.cpp in src/smt. Der relevante Backjump kann in der context :: pop_scope-Methode verfolgt werden. Es gibt auch andere Löser: Der src/sat/sat_solver wird für Bitvektor- und Boolesche Probleme verwendet. Es hat eine ähnliche Pop-Methode. Schließlich wird nlsat für nichtlineare Polynomarithmetik über die Realen verwendet.