C++参数 :logic 和 :timeout 是否在 Z3 不稳定分支中被弃用

Are C++ parameters :logic and :timeout deprecated in Z3 unstable branch?

本文关键字：分支 不稳定 Z3 logic 参数 timeout 是否 C++      更新时间：2023-10-16

对于我的应用程序代码，我为求解器的 z3 参数使用了以下设置

   z3::params p(context);
   p.set(":relevancy", static_cast<unsigned>(1));
   p.set(":logic", QF_ABV);
   p.set(":timeout", timeout); 
   solver.set(p);

更新到最新的 Z# 不稳定后，我得到了C++异常，基本上说明逻辑和超时不是有效参数。我没有找到任何等效的逻辑选项，所以我假设它是自动推导的。但是，对于超时，有两个选项soft_timout和solver2_timeout。我知道solver2_timeout用于增量求解器（即使用推送/弹出），因此我将代码更改为使用以下参数。

 z3::params p(context);
 p.set(":relevancy", static_cast<unsigned>(1));
 p.set(":soft_timeout", yices_timeout); 
 solver.set(p)

更改是否正确？soft_timeout与超时有何不同？是否有在某处维护的有效"z3：:p arams"的文档？

参数的文档是通过运行 z3 -p 获得的。有关特定选项的详细信息可通过运行 z3 -pp:option_name 获得。

参数

基础结构在 4.3.2 中发生了重大变化;现在有参数模块，soft_timeout驻留在 smt 模块中，即正确的名称是 smt.soft_timeout 。逻辑没有设置，但我们不能假设它会自动确定（仅适用于其中一些）。相反，我们现在可以为特定逻辑构建求解器对象（通过solver::solver(context & c, char const * logic) C++），或使用预定义的 SMT 策略之一（例如，请参阅策略教程）

相关文章：