search

kino-mc / rsmt2

A generic library to interact with SMT-LIB 2 compliant solvers running in a separate system process, such as Z3 and CVC4.
Apache License 2.0
65 stars 14 forks source link

Support for `get-proof` #6

Open AdrienChampion opened 7 years ago

AdrienChampion commented 7 years ago

Everything is basically in place, just need to do it.

ya0guang commented 1 year ago

I need this functionality and I'll be happy to see it coming out!

ya0guang commented 1 year ago

Thanks a lot for open souce such a great project! I'm trying to do some experimental work to get the proof from SMT solver and would like to make some modifications to the project.

Is it possible to get the raw output from the solver after print_get_proof?

I found this interface and it seems like a parser needs to be implemented for the proof. The ProofParser is already there but it seems some additional work needs to be done to make it usable. Is it possible to just take the unparsed output from the solver when inputting get-proof?