fstar - 不在 Windows 上时如何获得有关 z3 查询的见解

Question

https://github.com/FStarLang/FStar/wiki/Profiling-Z3-queries的 wiki 页面建议使用 Z3 Axiom Profiler；但是，Z3 Axiom Profiler 似乎只能在 Windows 上可靠地工作。

在没有 Z3 Axiom Profiler 的情况下，如何轻松获得最触发的量词？

Answer 1

与乔纳森的回复相关：

自此提交以来：https ://github.com/FStarLang/FStar/commit/c4ce03c3709b44600d66b8c2ee55a0e1aa9f75a3

运行就足够了：

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

因为其他 F* 特定选项现在嵌入在 .smt2 文件中。

Answer 2

这个命令行调用对我来说已经足够好了，只依赖于 z3 的 qi.profile 特性，并将最严重的违规者留在了底部。

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

（根据 Nik 的回答编辑，删除现在嵌入在 smt2 文件中的 z3 选项）

Answer 3

我已经能够通过在 Linux 上使用公理分析器，mono但它确实需要很多小时（在这个过程中它似乎挂了很长时间，但它确实有效）。一旦完成分析，界面就会非常灵敏（尽管我建议远离“文件”菜单下的一些导致它崩溃的选项）。

由于我基本上需要将其放置一夜以进行重要的跟踪，因此我在服务器上启动它并通过xpra使用 X 转发（这允许我断开连接并重新连接到服务器）。

---

如果问题纯粹是为了查找触发不良的查询，并且如果 fstar 使用提示可以更快地工作，那么我还有fstar-profile-queries 几个月前编写的一个有用的脚本，它可能很有用。它用于qprofdiff查找有问题的查询，但以一种更易于使用的方式进行。