在z3py中，可以使用z3.Solver()来创建一个求解器，并使用solver.add()方法将约束添加到求解器中。要保存和重新加载求解器的约束，可以使用solver.to_smt2()方法将求解器的约束保存到一个文件中，然后使用z3.Solver()和solver.from_string()方法来重新加载约束。

下面是一个示例代码：

from z3 import *

# 创建一个求解器
solver = Solver()

# 添加约束
x = Int('x')
y = Int('y')
solver.add(x > 0)
solver.add(y < 10)

# 保存约束
solver.to_smt2("constraints.smt2")

# 重新加载约束
solver = Solver()
solver.from_string(open("constraints.smt2").read())

# 解决约束
if solver.check() == sat:
    model = solver.model()
    print("x =", model[x])
    print("y =", model[y])
else:
    print("No solution")

在上面的示例中，首先创建了一个求解器solver，然后添加了两个约束x > 0和y < 10。然后，使用solver.to_smt2()方法将约束保存到文件constraints.smt2中。

接下来，使用z3.Solver()创建一个新的求解器solver，然后使用solver.from_string()方法从文件constraints.smt2中重新加载约束。

最后，使用solver.check()方法检查约束的可满足性，并使用solver.model()方法获取满足约束的解。如果存在解，则打印解的值；否则，打印"No solution"。

这样就实现了保存和重新加载z3py求解器的约束。