z3 - 复制 Z3 解算器

Question

我在帖子中看到过：Is it possible to clone Z3_context? 计划在 Z3 中添加复制/克隆求解器的功能，以促进一些回溯行为。我查看了 C API 文档，但目前找不到执行此操作的方法。

现在是否可以通过 C API 复制求解器？

Answer 1

API 没有复制 Solver 对象的方法，但可以使用Z3_solver_get_assertions和进行模拟Z3_solver_assert。这个想法是创建一个新的 Solver 对象，并将断言从旧的复制到新的。