我目前正在使用z3c++ API来解决对位向量的查询。有些查询可能在顶层包含存在量词。
通常量词消去很简单，可以用Z3快速完成。然而，在那些量词消除回到枚举数千个可行解决方案的情况下，我想放弃这种策略，并以其他方式自己处理查询。
我试过用'try-for'策略包装'qe'策略，希望如果量词消除失败(在100毫秒内)，我知道我最好以其他方式处理查询。不幸的是，"try-for"策略无法取消量词的消除(对于任何时间限制)。
在一个旧的帖子中讨论了类似的问题，并且"smt"策略被指责为没有响应。同样的道理也适用于"量化宽松"策略吗?同一篇文章指出，"未来的"版本应该响应更快。是否有任何方法或启发式来确定量词消除是否需要很长时间(除了在单独的线程中运行求解器并在超时时杀死它)?
我附上了一个最小的例子，所以你可以自己尝试:
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;
谢谢!
必须由正在运行的策略定期检查超时取消。我们基本上必须确保代码检查取消，并且不会在没有检查的情况下陷入长时间运行的循环。您可以通过在调试器中运行代码来识别无法检查取消的代码段，然后确定它在哪个过程中。然后在GitHub上提交一个bug，以便在有帮助的地方检查取消标志。总的来说，当涉及到位向量时，量词消除策略目前是相当简单的，所以除了简单的情况外，最好避免使用qe。