Как получить представление о запросе z3, когда не в Windows

Question

На вики-странице https://github.com/FStarLang/FStar/wiki/Profiling-Z3-queries предлагается использовать Z3 Axiom Profiler; однако Z3 Axiom Profiler надежно работает только на Windows.

Как я могу легко получить квантификаторы, которые стреляют больше всего без Z3 Axiom Profiler?

Answer 1

Этот вызов командной строки работает достаточно хорошо для меня, опирается только на функцию qi.profile в z3 и оставляет основных нарушителей в нижней части.

z3 smt.qi.profile=true queries-EverCrypt.Hash.Incremental-33.smt2 |& grep quantifier_instances | sort -t : -k 2 -n

(отредактировано после ответа Nik для удаления параметров z3, теперь встроенных в файл smt2)

Answer 2

Связанный с ответом Джонатана:

После этой фиксации: https://github.com/FStarLang/FStar/commit/c4ce03c3709b44600d66b8c2ee55a0e1aa9f75a3

Достаточно просто запустить:

z3 smt.qi.profile=true queries-Foo.smt2

поскольку другие F*-специфичные параметры теперь встроены в файл.smt2.

Answer 3

Я был в состоянии использовать профиль аксиомы в Linux через mono но это действительно занимает много часов (кажется, что во время этого процесса он зависает в течение длительного времени, но он действительно работает). Как только он закончил свой анализ, интерфейс стал довольно отзывчивым (хотя я бы рекомендовал держаться подальше от некоторых опций в меню "Файл", которые вызывают его сбой).

Поскольку мне нужно было бы оставить его на ночь для нетривиальных трассировок, я раскручиваю его на сервере и использую перенаправление X через xpra (что позволяет мне отключаться и повторно подключаться к серверу).

---

Если проблема заключается только в поиске запросов, которые плохо запускаются, и если fstar работает быстрее с подсказками, то у меня также есть полезный скрипт fstar-profile-queries что я написал несколько месяцев назад, что может быть полезно. Оно использует qprofdiff чтобы найти оскорбительные запросы, но делает это намного приятнее.