使用 Z3 确定 BV 查询的量词消除难度答案

【问题标题】：Use Z3 to determine difficulty of quantifier elimination for BV-queries使用 Z3 确定 BV 查询的量词消除难度
【发布时间】：2015-12-02 02:47:11
【问题描述】：

我目前正在使用 Z3 C++ API 来解决对位向量的查询。某些查询可能在顶层包含存在量词。

量词消除通常很简单，可以由 Z3 快速执行。但是，在量词消除回退到枚举数千个可行解决方案的情况下，我想中止这种策略并自己以其他方式处理查询。

我已经尝试用 'try-for' 策略包装 'qe' 策略，希望如果量词消除失败（比如 100 毫秒）我会知道我最好用其他方式处理查询大大地。不幸的是，“尝试”策略无法取消量词消除（对于任何时间限制）。

在old post 中讨论了一个类似的问题，并指责“smt”策略没有响应。相同的推理是否适用于“qe”策略？同一篇文章表明“未来”版本应该更具响应性。 是否有任何方法或启发式方法来确定量词消除是否需要很长时间（除了在单独的线程中运行求解器并在超时时终止它）？

我附上了一个小例子，你可以自己试试：

z3::context ctx;

z3::expr bv1 = ctx.bv_const("bv1", 10);
z3::expr bv2 = ctx.bv_const("bv2", 10);
z3::goal goal(ctx);
goal.add(z3::exists(bv1, bv1 != bv2));

z3::tactic t = z3::try_for(z3::tactic(ctx,"qe"), 100);    
auto res = t.apply(goal);
std::cout << res << std::endl;

谢谢！

【问题讨论】：

标签： z3 smt quantifiers

【解决方案1】：

必须通过正在运行的策略定期检查超时取消。我们基本上必须确保代码检查取消，并且不会在没有检查的情况下陷入长时间运行的循环。您可以通过在调试器中运行代码、中断然后确定它所在的过程来识别无法检查取消的代码段。然后在 GitHub 上提交一个错误，以便在有帮助的地方检查取消标志。总的来说，当涉及到位向量时，量词消除策略目前相当简单，因此除了简单的情况外，最好避免使用 qe。

【讨论】：