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>))
但我不知道要使用哪些求解器。