drukowanie formuł wewnętrznych solver w z3

Question

Narzędzie do sprawdzania twierdzeń z3 zajmuje dużo czasu, aby rozwiązać formułę, która moim zdaniem powinna być w stanie poradzić sobie z łatwością. Aby to lepiej zrozumieć i ewentualnie zoptymalizować moje dane wejściowe do Z3, chciałem zobaczyć wewnętrzne ograniczenia, które z3 generuje jako część procesu rozwiązywania. Jak wydrukować formułę, którą z3 tworzy dla swoich solverów, gdy używasz z3 z wiersza poleceń?

Answer 1

Narzędzie wiersza poleceń Z3 nie ma takiej opcji. Co więcej, Z3 zawiera kilka solverów i etapów wstępnego przetwarzania. Nie jest jasne, który krok byłby dla ciebie przydatny. Kod źródłowy Z3 jest dostępny pod adresem https://github.com/Z3Prover/z3. Kiedy Z3 jest kompilowany w trybie debugowania, zapewnia dodatkową opcję linii poleceń: -tr:<tag>. Ta opcja może być używana do selektywnego zrzucania informacji. Na przykład, plik źródłowy nlsat_solver.cpp zawiera następującą instrukcję:

TRACE("nlsat", tout << "starting search...\n"; display(tout); 
       tout << "\nvar order:\n"; 
       display_vars(tout);); 

Polecenie opcja wiersza -tr:nlsat poinstruuje Z3 do wykonania instrukcji powyżej. tout to strumień wyjściowy śledzenia. Zostanie on zapisany w pliku .z3-trace. Źródło Z3 jest pełne tych poleceń TRACE. Ponieważ kod jest dostępny, możemy również dodać własne komendy śledzenia w kodzie.

Jeśli umieścisz swój przykład, mogę powiedzieć, które komponenty Z3 są używane do wstępnego przetworzenia i rozwiązania. Następnie możemy wybrać, które "tagi" powinniśmy włączyć do śledzenia.

EDIT (po constraints zostały wysłane): Twój przykład jest w mieszanym całkowitą & rzeczywistym nieliniowej arytmetyki. Nowy nieliniowy moduł arytmetyczny (nlsat) w Z3 nie obsługuje to_int. W ten sposób do rozwiązywania problemu służy rozwiązany ogólnego przeznaczenia Z3. Chociaż ten solver akceptuje prawie wszystko, nie jest on nawet kompletny dla nieliniowej rzeczywistej arytmetyki. Nieliniowe wsparcie dla tego solver opiera się na: analizie przedziałowej i obliczeniach Grobnera. Ten solver jest zaimplementowany w folderze src/smt (w unstable branch). Moduł arytmetyczny jest zaimplementowany w plikach theory_arith*. Opcja dobrej linii poleceń śledzenia to -tr:after_reduce. Wyświetli zestaw wiązań po wstępnym przetworzeniu. Wąskim gardłem jest moduł arytmetyczny (theory_arith*).

Uwagi dodatkowe

• problem jest w nierozstrzygalnym fragmentu: mieszany całkowitą & rzeczywistym nieliniowe arytmetycznych. Oznacza to, że niemożliwe jest napisanie dźwięku i pełne rozwiązanie dla tego fragmentu. Oczywiście możemy napisać rozwiązanie, które rozwiązuje przypadki, które znajdziemy w praktyce. Uważam, że możliwe jest rozszerzenie nlsat w celu obsługi to_int.

• Jeśli unikniesz to_int, będziesz mógł użyć nlsat. Problem tkwi w nieliniowym rzeczywistym fragmencie arytmetycznym. Rozumiem, że może to być trudne, ponieważ kodowanie to_int wydaje się być kluczową rzeczą.

• Kod w gałęzi "niestabilny" na stronie z3.codeplex.com jest znacznie lepiej zorganizowany niż wersja oficjalna w gałęzi "master". Wkrótce połączę to z oddziałem "master".Możesz pobrać gałąź "niestabilną", jeśli chcesz grać z kodem źródłowym.

• Oddział "niestabilny" korzysta z nowego systemu kompilacji. Możesz zbudować wersję Release ze wsparciem śledzenia. Po wygenerowaniu pliku Makefile wystarczy użyć opcji -t.

skrypty python/mk_make.py -t

• Kiedy Z3 jest skompilowany w trybie debugowania, opcja AUTO_CONFIG=false domyślnie. Aby odtworzyć zachowanie trybu "Release", należy podać opcję wiersza poleceń: AUTO_CONFIG=true.