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

Question

对于我的应用程序代码，我为求解器使用了以下 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# unstable 后，我得到了 C++ 异常，本质上表明逻辑和超时不是有效参数。我没有找到任何等效的逻辑选项，所以我假设这是自动推导出来的。但是，对于超时，有两个选项 soft_timout 和 solver2_timeout。我知道 solver2_timeout 用于增量求解器（即 push/pops），因此我更改了代码以使用以下参数。

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

修改是否正确？ soft_timeout 与超时有何不同？是否在某处维护了有效 "z3::params" 的文档？

Answer 1

参数文档由运行z3 -p获取。运行 z3 -pp:option_name 获取有关特定选项的更多信息。

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

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

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

c++

api

z3