Improve support for writing checkpoints in aspif format

[rkaminsk]

This PR adds support to write checkpoints in aspif format, which can afterward be read again using a dedicated function.

from clingo.control import Control, BackendType

# create cp1
ctl = Control()
ctl.register_backend(BackendType.Aspif, "cp1.aspif", True)
ctl.add("1 {a; b} 1.")
ctl.ground()
ctl.solve()

# create cp2
ctl = Control()
# can alternatively use load_aspif
ctl.load("cp1.aspif")
# the backend is deliberately registered later here to avoid dumping cp1 again
ctl.register_backend(BackendType.Aspif, "cp2.aspif", True)
ctl.add("c :- a. d :- b.")
ctl.ground()
ctl.solve()

# load cp1 and cp2 combined
ctl = Control(["0"])
# function load cannot be used here
ctl.load_aspif(["cp1.aspif", "cp2.aspif"])
print(ctl.solve(on_model=print))

The output is

a c
b d
SAT

@teiesti and @thojat, let me know what you think of this...

[BenKaufmann]

Nitpick: this (mostly) duplicated code is inconsistent regarding the use of begin/end. At least, I'd suggest dropping the (unnecessary) using declarations from the previous version.

[rkaminsk]

It does not compile without the using declarations. I admit, I did not check why.

[rkaminsk]

(The duplication will stay there for clingo series 5 but it will not stay like this in the upcoming 6.)

[BenKaufmann]

Nitpick: inconsistent spacing

[rkaminsk]

I don't even see where the inconsistent spacing is anymore. In another project I switched to 100% relying on clang-format. I should setup clang-format at some point but will leave it out of this PR.

[thojat]

I think this adds a lot of convenience for reusing already grounded programs. In the future this feature might also become an easy way to retract programs added with multishot solving, e.g.,

ctl.ground([("base", [])], checkpoint=“checkpoint1”)
ctl.ground([(“p1”, [])], checkpoint=“checkpoint2”)
ctl.solve()
ctl.restore(checkpoint=“checkpoint1”)

As far as I understand the backend is basically an observer that generates the aspif file during grounding, right? Do you think in the future it might be possible to also store the nogoods learned during solving?

[rkaminsk]

I think this adds a lot of convenience for reusing already grounded programs. In the future this feature might also become an easy way to retract programs added with multishot solving, e.g.,

ctl.ground([("base", [])], checkpoint=“checkpoint1”)
ctl.ground([(“p1”, [])], checkpoint=“checkpoint2”)
ctl.solve()
ctl.restore(checkpoint=“checkpoint1”)

Restoring the same control object to a previous state is difficult. Especially, if there shall be guarantees regarding determinism, propagators, etc. The idea here was to at least make writing and loading aspif easy.

As far as I understand the backend is basically an observer that generates the aspif file during grounding, right?

Yes, it uses the same classes that clingo uses internally.

Do you think in the future it might be possible to also store the nogoods learned during solving?

To some extend it is already possible to store/restore learned nogoods. There are clasp's lemma-in and lemma-out options. However, this has to be used with care. The options can only be used if the underlying pogram is exactly the same.

[rkaminsk]

If you want perfect checkpoint/restore functionality, you might want to consider https://criu.org. It should run on any linux system.

[rkaminsk]

Going to merge. In case that further refinements are necessary let's just open a new issue.