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

Question

我目前使用Z3 C++ API解决位向量查询问题。一些查询可能包含顶级的存在量词。

量词消除通常很简单，可以通过Z3快速执行。然而，在那些量词消去回归到数千种可行解决方案的情况下，我想放弃这种策略并以其他方式自己处理查询。

我试着用'尝试'的策略来包装'qe'-tactic，希望如果量词消除失败（比如说100ms），我会知道我最好在一些情况下处理查询另一种方式。不幸的是，'尝试'的策略未能消除量词消除（任何时间限制）。

在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; 

谢谢！

Answer 1

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