保存并重新加载 z3py 求解器约束

Question

我可以保存为 z3 求解器创建的约束，然后重新加载它们以继续寻找更多解决方案吗？

我了解到此类内容有 SMT-LIB2 格式，并且 z3 和 z3py 具有用于以该格式保存和加载的 API。不幸的是我不能让它工作。

这是我的示例程序，它毫无意义地保存和重新加载：

import z3

filename = 'z3test.smt'

# Make a solver with some arbitrary useless constraint
solver = z3.Solver()
solver.add(True)

# Save to file
smt2 = solver.sexpr()
with open(filename, mode='w', encoding='ascii') as f: # overwrite
    f.write(smt2)
    f.close()

# Load from file
solver.reset()
solver.from_file(filename)

它失败了：

Exception has occurred: ctypes.ArgumentError
argument 3: <class 'TypeError'>: wrong type
  File "C:\Users\Marian Aldenhövel\Desktop\FridgeIQ\z3\z3-4.8.4.d6df51951f4c-x64-win\bin\python\z3\z3core.py", line 3449, in Z3_solver_from_file
    _elems.f(a0, a1, _to_ascii(a2))
  File "C:\Users\Marian Aldenhövel\Desktop\FridgeIQ\z3\z3-4.8.4.d6df51951f4c-x64-win\bin\python\z3\z3.py", line 6670, in from_file
    _handle_parse_error(e, self.ctx)
  File "C:\Users\Marian Aldenhövel\Desktop\FridgeIQ\src\z3test.py", line 17, in <module>
    solver.from_file(filename)

这是我的理解问题还是我的代码有问题？可以这样做吗？ sexpr() 和 from_file() 是正确的 API 调用对吗？

我在 Windows 10 64 位上使用来自 https://github.com/z3prover/z3/releases 的 z3 和 z3py 4.8.4。

如果需要，请提供更多详细信息：

我正在使用 Python 中的 z3 来寻找大型解剖难题的解决方案。

要找到我打电话给solver.check() 的所有解决方案。当它返回 sat 判决时，我将模型解释为我的拼图解决方案的图像。然后我添加一个阻止条款排除该特定解决方案并再次致电solver.check()。

这很好用，我很高兴。

找到所有解决方案的运行时间大约需要很多天，或者直到我感到无聊为止。我担心我的机器不会连续运行那么长时间。它可能会崩溃、没电或因其他原因重新启动。

我可以轻松地重新创建初始约束，这是程序的重点。但是阻塞子句是一个运行时产品，是我们已经取得了多远的函数。

我想我可以保存求解器的状态，如果在运行时我发现这样的文件重新启动，方法是加载完整的阻塞子句，然后继续寻找更多解决方案，而不必重新开始。

感谢您花时间阅读和思考。

玛丽安

Answer 1

使用z3 4.4.1 和z3 4.8.5，我将以smt2 格式转储（并重新加载）约束，如下所示：

import z3

filename = "z3test.smt2"

x1 = z3.Real("x1")
x2 = z3.Real("x2")

solver = z3.Solver()
solver.add(x1 != x2)

#
# STORE
#

with open(filename, mode='w') as f:
    f.write(solver.to_smt2())

#
# RELOAD
#

solver.reset()

constraints = z3.parse_smt2_file(filename, sorts={}, decls={})
solver.add(constraints)
print(solver)

输出：

~$ python t.py 
[And(x1 != x2, True)]

文件z3test.smt2:

(set-info :status unknown)
(declare-fun x2 () Real)
(declare-fun x1 () Real)
(assert
 (and (distinct x1 x2) true))
(check-sat)

我不知道 API 在您使用的版本中是否发生了变化。欢迎反馈。