0

Q1：可以查询Z3在不同子求解器中花费的时间吗？

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

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


Q2：此外，是否可以在子求解器上设置超时？

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

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

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

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

4

1 回答 1

1

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

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

于 2015-01-21T13:21:46.980 回答