如何在 Z3 中实现自定义简化策略？答案

【问题标题】：How to implement a custom simplify tactic in Z3?如何在 Z3 中实现自定义简化策略？
【发布时间】：2023-03-08 01:07:01
【问题描述】：

在我的工具中，我使用将常量与整数变量进行比较的条件（例如 y

在代码中：

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？

【问题讨论】：

标签： c++ z3 simplify

【解决方案1】：

Z3战术存放在目录：src/tactic。算术相关的策略在子目录arith 中。您应该使用现有策略作为实施策略的“模板”。一个很好的例子是 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

【讨论】：