z3 - Z3 在执行过程中添加新变量

Question

我正在尝试向 Z3 添加新功能。此功能要求我在执行期间和预处理后添加新的松弛变量。我找不到合适的方法，我担心尝试通过添加新列来强制它会“破坏”求解器。

有没有一种常见的推荐方法来做到这一点？

谢谢， 奥马尔

Answer 1

您可以在文件中找到一个示例src/smt/theory_arith_int.h，方法：mk_gomory_cut. 在这个方法的最后，一个新的多项式约束被创建，并存储在变量 中bound。然后，以下代码用于“内部化”约束：

    literal l     = null_literal;
    context & ctx = get_context();
    ctx.internalize(bound, true);
    l = ctx.get_literal(bound);

该方法internalize将回调 theory_arith，并创建一个新的 slack。注：该方法internalize假设存储的多项式约束bound为简化形式。