Ich versuche Z3 zu verwenden, um über Teilstrings nachzudenken, und bin auf ein nicht intuitives Verhalten gestoßen. Z3 gibt 'sat' zurück, wenn er gefragt wird, ob 'xy' in 'xy' erscheint, aber es gibt 'unbekannt' zurück, wenn gefragt wird, ob 'x' in 'x' oder 'x' in 'xy' steht.
Ich habe den folgenden Code zur Veranschaulichung dieses Verhaltens kommentiert:
%Vor%Nun, da das Problem besteht, versuchen wir, die Teilstrings zu finden:
%Vor% Wenn wir stattdessen nach findMeXY in xy suchen, gibt der Solver wie erwartet 'sat' zurück. Es scheint, dass, da der Löser diese Abfrage für 'xy' verarbeiten kann, es in der Lage sein sollte, es für 'x' zu handhaben. Wenn Sie nach findMeX='x' in 'xy='xy' suchen, wird 'unbekannt' zurückgegeben.
Kann jemand eine Erklärung oder vielleicht ein alternatives Modell vorschlagen, um dieses Problem in einem SMT-Solver auszudrücken?
Die kurze Antwort für das beobachtete Verhalten ist: Z3 gibt 'unbekannt' zurück, weil Ihre Behauptungen Quantifizierer enthalten.
Z3 enthält viele Prozeduren und Heuristiken für den Umgang mit Quantifizierern. Z3 verwendet eine Methode namens Model-Based Quantifier Instantiation (MBQI) zur Erstellung von Modellen zur Befriedigung von Abfragen wie Ihrer. Der erste Schritt besteht darin, eine Kandidateninterpretation zu erstellen, die auf einer Interpretation basiert, die die quantifiziererfreien Behauptungen erfüllt. Unglücklicherweise tritt dieser Schritt in der aktuellen Z3 nicht reibungslos mit der Array-Theorie zusammen. Das grundlegende Problem ist, dass die von der Array-Theorie aufgebaute Interpretation von diesem Modul nicht modifiziert werden kann.
Eine faire Frage ist: Warum funktioniert es, wenn wir die Push / Pop-Befehle entfernen? Es funktioniert, weil Z3 aggressivere Vereinfachungsschritte (Preprocessing) verwendet, wenn inkrementelle Lösungsbefehle (wie Push- und Pop-Befehle) nicht verwendet werden.
Ich sehe zwei mögliche Problemumgehungen für Ihr Problem.
Sie können Quantifikatoren vermeiden und weiterhin die Array-Theorie verwenden. Dies ist in Ihrem Beispiel möglich, da Sie die Länge aller "Strings" kennen. Daher können Sie den Quantifizierer erweitern. Obwohl dieser Ansatz umständlich erscheint, wird er in der Praxis und in vielen Verifikations- und Testwerkzeugen verwendet.
Sie können Array-Theorie vermeiden. Sie deklarieren String als eine nicht interpretierte Sortierung, wie Sie es für Char getan haben. Dann deklarieren Sie eine Funktion char-of, die das i-te Zeichen einer Zeichenfolge zurückgeben soll. Sie können diese Operation axiomatisieren. Zum Beispiel können Sie sagen, dass zwei Strings gleich sind, wenn sie die gleiche Länge haben und dieselben Zeichen enthalten:
Der folgende Link enthält Ihr Skript, das mit dem zweiten Ansatz codiert wurde: Ссылка
Der zweite Ansatz ist attraktiver und ermöglicht es Ihnen, kompliziertere Eigenschaften von Strings zu beweisen. Es ist jedoch sehr einfach, erfüllbare quantifizierte Formeln zu schreiben, so dass Z3 kein Modell erstellen kann. Der Z3-Leitfaden beschreibt die wichtigsten Funktionen und Einschränkungen des MBQI-Moduls. Es enthält möglicherweise entscheidbare Fragmente, die von Z3 gehandhabt werden können. BTW, beachten Sie, dass das Löschen der Array-Theorie kein großes Problem sein wird, wenn Sie Quantifizierer haben. Die Anleitung zeigt, wie Arrays mithilfe von Quantifizierern und Funktionen codiert werden.
Weitere Informationen zur Funktionsweise von MBQI finden Sie in den folgenden Artikeln: