smtprofiling

Narzędzie do profilowania zapytań SMT wysyłanych przez F* do solvera Z3. Pozwala zidentyfikować przyczyny niestabilności dowodów i problemów wydajnościowych, szczególnie gdy dowody wymagają wysokich limitów zasobów lub zawodzą nieprzewidywalnie. Zbierasz plik .smt2 z problematycznego fragmentu kodu, uruchamiasz go niezależnie w Z3 z opcjami profilowania, a następnie analizujesz, które kwantyfikatory są nadmiernie aktywne i dlaczego.

1. Otwórz plik F* (.fst lub .fsti) zawierający dowód, który chcesz debugować. Otocz problematyczną definicję dyrektywami opcji: #push-options "--log_queries --z3refresh --query_stats --split_queries always" przed kodem i #pop-options po nim. Te flagi instruują F*, aby zbierał szczegółowe informacje o zapytaniach wysyłanych do Z3.

2. Uruchom F* na pliku za pomocą polecenia fstar.exe Module.fst (dostosuj ścieżki include jeśli jest to konieczne). F* wypisze komunikaty zawierające nazwy plików .smt2 wygenerowanych dla każdego wariantu dowodu.

3. Zlokalizuj Z3 w swoim systemie — może być nazwany z3, z3-4.13.3, z3-4.15.1 lub inną wersją. Uruchom Z3 bezpośrednio na wygenerowanym pliku .smt2 poleceniem z3 queries-myquery.smt2, aby zweryfikować zapytanie niezależnie od F*.

4. Dodaj opcję profilowania Z3: z3 queries-myquery.smt2 smt.qi.profile=true. Z3 wyświetli statystyki dotyczące tego, które kwantyfikatory były instancjonowane i jak często.

5. Przeanalizuj wynik profilu. Kwantyfikatory z nazw takich jak Box_bool_proj_0 lub z modułów Prims i FStar.Pervasives naturalnie aktywują się często. Szukaj kwantyfikatorów z Twoich własnych modułów, które aktywują się nadmiernie — to sygnał, że powinieneś napisać dla nich wzorzec lub jawnie kontrolować ich instancjonowanie.

6. Aby pogłębić wiedzę, zapoznaj się z dokumentacją w repozytorium PoP-in-FStar (https://github.com/FStarLang/PoP-in-FStar), szczególnie sekcją under_the_hood/uth_smt.rst, która wyjaśnia kodowanie SMT w F* i techniki profilowania.