Save and Restore solver state

[MarianAldenhoevel]

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

I have read #2095 and #1044 but I am not sure they talking are about the same thing. If so, feel free to ignore this question. I am very new to Z3 and SAT-solvers in general, so excuse me in that case.

My program generates a large set of constraints and lets solver.check() work on it. If the verdict is sat it interprets the model in my problem-space (as an image), adds a blocking clause and then calls solver.check() again to try and find another solution.

The total runtime is expected to be many days. If my machine dies or needs a reboot I currently have to start over. While I can easily create the initial constraints the blocking clauses are only found while working the problem. If possible I would like to create savepoints during the run capturing the state of the solver or at least the blocking clauses added so far.

I have learned there is the SMT-LIB2 format for stating the problem in a portable way 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)

For me 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 here ([https://github.com/z3prover/z3/releases]) on Windows 10 64bit.

[NikolajBjorner]

1. there is a bug in the _handle_parse_error code that causes another error. This is fixed in latest builds from what I can see.
2. the string that is saved is for whatever reason not reparsed. It is easier to see the parse error by reading z3test.smt from the command line. The error messages will be easier to digest.

[MarianAldenhoevel]

Thank you very much Nikolaj,

1) I am using 4.8.4 from https://github.com/z3prover/z3/releases on Windows 10. Are there newer binaries available? I don't quite feel up to building from source.

2) By "reading from the command line" do you suggest doing:

.\z3.exe -smt2 .\z3test.smt2

This just returns without printing any output

[MarianAldenhoevel]

I have found the nightly builds, shame on me for not doing so earlier.

using z3-4.8.5.8c177c019b6c-x64-win my test-program works fine.

[NikolajBjorner]

Regarding "reading from command-line".

• Z3 doesn't print "(check-sat)". It only prints the assertions. If you want it to check satisfiability you would have to append this string. Perhaps this is my design mistake because checking satisfiability of these outputs could be the common use case.

[KennethAdamMiller]

I think it is absurd that the SMT module houses a function for which does not do what the name implies without even so much as a comment on the interface. Why would a parse_smtlib_file not put every single last thing that is in the file into the AST? If the user doesn't want something, they can go delete it. As it is, optimize has some functionality and so does Fixedpoint. Functionality that should be straightforward is scattered around inside different modules. Lots of the submodules have to_string, but no easy way to parse that back out.