CODEWITHSUNDEEP
z3z3py
Marian Aldenhövel
Marian Aldenhövel

Reputation: 727

Save and reload z3py solver constraints

Can I save the constraints I created for a z3 solver and later reload them to continue looking for more solutions?

I have learned there is the SMT-LIB2 format for such things and that z3 and z3py have an API for saving and loading in that format. Unfortunately I cannot make it work.

Here's my example program which pointlessly saves and reloads:

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)

It fails with:

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)

Is this a problem with my understanding or my code? Can it be done like this? Are sexpr() and from_file() the right pair of API calls?

I am using z3 and z3py 4.8.4 from https://github.com/z3prover/z3/releases on Windows 10 64bit.

More detail if required:

I am playing with z3 in Python to find solutions for a large disection-puzzle.

To find all solutions I am calling solver.check(). When it returns a sat verdict I interpret the model as image of my puzzle solution. I then add a blocking clause ruling out that specific solution and call solver.check() again.

This works fine and I am delighted.

The runtime to find all solutions will be on the order of many days or until I get bored. I am concerned that my machine will not be running continuously for that long. It may crash, run out of power, or be rebooted for other reasons.

I can easily recreate the initial constraints which is the whole point of the program. But the blocking clauses are a runtime product and a function of how far we have gotten.

I thought I could save the state of the solver and if at runtime I find such a file restart by loading that with the blocking clauses intact and go on finding more solutions instead of having to start over.

Thank you for taking your time reading and thinking.

Marian

Upvotes: 4

Views: 1746

Answers (1)

Patrick Trentin
Patrick Trentin

Reputation: 7342

With z3 4.4.1 and z3 4.8.5, I would dump (and reload) the constraints in smt2 format as follows:

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)

output:

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

file z3test.smt2:

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

I have no idea whether the API changed in the version you are using. Feedback is welcome.

Upvotes: 4

Related Questions