保存并重新加载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 64bit上使用来自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是否已更改。欢迎反馈。