od obecnej wersji, jest pewien problem w "uproszczeniu ctx-solvera", tak jak w przykładzie http://rise4fun.com/Z3/CqRv Z3 daje złą odpowiedź. Zastępuję "uproszczenie ctx-solvera" przez "uprość" jak http://rise4fun.com/Z3/x9X4 Zastanawiam się, jaka jest różnica pomiędzy tymi dwiema taktykami "upraszczaj" i "upraszczaj ctx-solver"?Jaka jest różnica między "uproszczeniem" i "uproszczeniem ctx-solvera" w Z3
Taktyka simplify wykonuje tylko "lokalne uproszczenia". Dla każdego terminu t mamy, że simplify(t) to nowy termin równoważny t. Ponadto wynik simplify(t) nie zależy od kontekstu, w którym występuje t. W kontekście miałem na myśli stwierdzenie F, gdzie występuje t i wszystkie inne asercje. Ponieważ simplify jest lokalny, jest bardzo wydajny. Wdrożenie zasadniczo opiera się na oddolnym stosowaniu zasad uproszczenia. Ponadto, ponieważ wynik simplify(t) nie zależy od informacji kontekstowych, możemy go buforować. Tak więc, nawet jeśli t występuje N razy w formule F, musimy tylko uprościć go raz. Wszystkie wbudowane solvery w Z3 stosują tego rodzaju uproszczenie. Tak więc, taktyki takie jak simplify zostały dokładnie przetestowane.
Taktyka ctx-solver-simplify używa kontekstu, w którym występuje t w celu zastosowania uproszczeń. Podstawową ideą jest uproszczenie formuły F poprzez przechodzenie jej za pomocą solwerera S. Solver S zasadniczo zawiera "kontekst". Ilekroć S.check() zwraca unsat, wiemy, że obecny kontekst jest niespójny, wtedy możemy zastąpić bieżącą formułę przez false. Model ctx-solver-simplify jest znacznie droższy. Najpierw wykonuje wiele połączeń z numerem S.check(). Każde z tych połączeń jest potencjalnie bardzo drogie. O wiele trudniejsze jest buforowanie wyników pośrednich. Z3 może wielokrotnie upraszczać podformularz t, ponieważ występuje w różnych kontekstach.
Błąd, który zgłosiłeś w swoim pytaniu został naprawiony. Poprawka będzie dostępna w następnym wydaniu (wersja 4.1). Jeśli potrzebujesz, możemy dostarczyć Ci wstępną wersję Z3 4.1