0

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

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

我对花在与算术相关的子求解器上的时间特别感兴趣,更准确地说,是那些产生统计数据grobnernonlinear-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 回答