测量和限制在算术子求解器中花费的时间

问题描述

Q1:是否可以查询Z3在不同子求解器中花费的时间?

Q1: Is it possible to query the times Z3 spent in different sub-solvers?

调用 (get-info :all-statistics) 给出了 Z3 的整体运行时间，但我想将其分解为单独的子求解器.

Calling (get-info :all-statistics) gives the overall run time of Z3, but I would like to break it down into individual sub-solvers.

我对花在算术相关的子求解器上的时间特别感兴趣，更准确地说，是那些产生统计 grobner 和 nonlinear-horner 的时间.

I am particularly interested in the time spent in arithmetic-related sub-solver, more precisely, in those that give rise to the statistics grobner and nonlinear-horner.

Q2:此外，是否可以在 sub-solver 上设置超时?

Q2: Furthermore, is it possible to put a timeout on sub-solver?

我可以想象一些事情，比如为每个 check-sat 和 sub-solver 定义一个超时，它限制了 Z3 可以在该 sub-solver 中花费的时间.Z3会反复调用n个不同的子求解器，如果达到其中一个的时间限制，它会继续，但只使用剩余的n-1个子求解器.

I could imagine something like defining a timeout per check-sat and sub-solver that bounds the time Z3 can spent in that sub-solver. Z3 would repeatedly call n different sub-solvers, and if the time bound of one of them is reached it continues, but only uses the remaining n-1 sub-solvers.

我阅读了战术教程，并得到了这样的印象:这实际上可能是通过类似的方式实现的

I read the tactics tutorial and got the impression that this might actually be possible by something along the lines of

(repeat
  (par-or
    (try-for <arithmetic-solvers> 500)
    <all-other-solvers>))

但我不知道要使用哪些求解器.

but I couldn't figure out which solvers to use.

推荐答案

对于 Q1:不，您必须在其上添加自己的计时器，我希望这不是微不足道的，因为不清楚究竟应该和应该做什么不算.

For Q1: No, you'd have to add your own timers on that and I would expect this to be nontrivial as it's not clear what exactly should and shouldn't be counted.

Q2:是的，您可以构建自己的自定义策略/战术.请注意， par-or 意味着 parallel 或者，即，它将尝试并行运行提供的策略.并非我们称为求解器"的所有东西都有自己的策略，因此这可能需要一些摆弄.请注意，此上下文中的求解器"不一定与称为求解器"的 Z3 C++ 对象相同.一些求解器"也是 SMT 内核的组成部分.

Q2: Yes, you can build your own custom strategies/tactics. Note that par-or means parallel or, i.e., it will try to run the provided tactics in parallel.Not everything we call a "solver" has it's own tactic, so this might require some fiddling. Note that "solver" in this context is not necessarily the same as the Z3 C++ object called "solver". Some "solvers" are also integral parts of the SMT kernel.

这篇关于测量和限制在算术子求解器中花费的时间的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持！