c++ - 如何在 Z3 中实现自定义简化策略？

Question

在我的工具中，我使用条件将常量与整数变量进行比较(例如 y < 100)。通常，一个变量有多个条件，我想简化这些情况。例如:y < 100 && y != 99 应该变成 y < 99。 simplify 策略不会这样做，而且 simplify 的论据都没有听起来有帮助。

在代码中:

context c;
goal g(c);
expr x = c.int_const("x");
expr y = c.int_const("y");
solver s(c);
expr F = y < 100 && y != 99;
g.add(F);
tactic t = tactic(c, "simplify");
apply_result r = t(g);
for (unsigned i = 0; i < r.size(); i++) {
    std::cout << "subgoal " << i << "\n" << r[i] << "\n";
}

最后的输出返回:subgoal 0
(goal
(not (<= 100 y))
(not (= y 99)))

而不是 subgoal 0(goal(not(<= 99 y))或类似我想要的东西。

因此我想实现我自己的简化策略。不幸的是我找不到如何做到这一点。我知道，该策略需要在 C++ 中实现，但如何将我的策略引入 Z3？

Answer 1

Z3战术存放在目录:src/tactic。与算术相关的策略在子目录arith 中。您应该使用现有策略作为实现策略的"template"。一个很好的例子是 https://z3.codeplex.com/SourceControl/latest#src/tactic/arith/normalize_bounds_tactic.cpp

为了使新策略在 API 和 SMT 2.0 前端可用，我们必须包含一个包含 ADD_TACTIC 命令的注释。此命令指示 Z3 mk_make 脚本将所有内容粘合在一起。参数是:策略的名称、描述和用于创建策略的 C++ 代码。

/*
  ADD_TACTIC("normalize-bounds",
             "replace a variable x with lower bound k <= x with x' = x - k.",
             "mk_normalize_bounds_tactic(m, p)")
*/

顺便说一句，您还可以尝试通过扩展现有策略来实现新功能，例如: https://z3.codeplex.com/SourceControl/latest#src/tactic/arith/propagate_ineqs_tactic.cpp