get_proof() doesn't work for all solvers

[marino-mrc]

Hello Alexey, as requested, I added a new commit in my fork in order to implement a test for the get_proof() function.

At the moment, I left some "print" call in the test for debugging purpose (I'll remove them in a successive commit) because in my opinion the get_proof() function doesn't work for some solvers.

More specifically, here is the result of the test on my laptop:

Here is a short analysis (just a personal opinion):

The problem is:

1. Cadical103 and Cadical153 return an empty proof. This seems to be wrong
2. maplesat has a problem when prints the variables. Indeed, the variable "3" doesn't exist (I think it should add a "-1" in the function that prints the proof)
3. lingeling is probably fine (but there are 2 variables. It could depend on how the solver handles the UNSAT)
4. I don't know if the output produced by maplecm is ok (I haven't had the time to go further)
5. MinisatGH, Minisat22, Minicard don't support the get_proof() function

Please, check my commit and let me know your ideas.

Thank you. Regards, Marco

[alexeyignatiev]

Thanks for the update, Marco! This surely requires further attention

1. I am not sure why both versions of CaDiCaL report an empty proof. It may be that the formula is a bit too simple I guess, but still...
2. All the Maple* solvers should be working fine as well - again, this needs to be analysed. I will have a look when I get a chance.
3. Lingeling looks okay to me at first glance.
4. MapleCM looks okay to me at first glance.
5. MiniSat does not support proof logging - this is known and so it does not need to be tested here. :)

Again, thanks a lot! Alexey