如何在 Z3 中实现自定义简化策略? [英] How to implement a custom simplify tactic in Z3?

问题描述

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

In my tool, I use conditions that compare constants to integer variables (for example y < 100). Often, there are multiple conditions for one variable and I want to simplify those cases. For example: y < 100 && y != 99 should become y < 99. The simplify tactic does not do this and none of the arguments for simplify sound like they can help.

在代码中:

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(目标(不是(<= 100 年))(不是(= y 99)))

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

and not subgoal 0(goal(not(<= 99 y)) or something similar as I want it to be.

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

Therefore I want to implement my own simplify tactic. Unfortunately I cannot find how to do this. I am aware, that the tactic needs to be implemented in C++, but how can I introduce my tactic to Z3?

推荐答案

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

The Z3 tactics are stored in the directory: src/tactic. The arithmetic related tactics are in the subdirectory arith. You should use an existing tactic as a "template" for implementing your tactic. A good example is https://z3.codeplex.com/SourceControl/latest#src/tactic/arith/normalize_bounds_tactic.cpp

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

To make the new tactic available in the API and SMT 2.0 front-end, we have to include a comment containing a ADD_TACTIC command. This command instructs the Z3 mk_make script to glue everything together. The arguments are: name of the tactic, description, and C++ code for creating the tactic.

/*
  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

BTW, you may also try to implement the new feature by extending an existing tactic such as: https://z3.codeplex.com/SourceControl/latest#src/tactic/arith/propagate_ineqs_tactic.cpp

这篇关于如何在 Z3 中实现自定义简化策略?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！