The proof checker uses the standard parser for reading the smt2 input and a new parser for the proofs. The proof parser uses currently a lot of duplicated code, since java-cup files cannot build on one another. It may be possible to factor out some larger code blocks, e.g., the side condition checking for match terms.
Error handling is not very sophisticated, yet. Some errors in the proof result in thrown exceptions that are not caught. Terms that don't type-check may lead to null pointer exceptions.
Known Bugs in SMTInterpol proofs: 1. SMTInterpol currently produces proofs with undeclared free variables when a quantifier is instantiated but not all variables are used in the subformula. 2. The unletter may rename bounded variables (in case of name clashes), which may result in a perfectly valid proof to be reported as invalid, because the variable names in the input formula differ. Also the produced proof by SMTInterpol may be wrong due to the renaming.
This adds a tool to parse and check the proofs given by SMTInterpol. It also extends the webinterface and adds a new page to compute and check proofs.
The web page is already online: https://ultimate.informatik.uni-freiburg.de/smtinterpol/online/proof.html
The proof checker uses the standard parser for reading the smt2 input and a new parser for the proofs. The proof parser uses currently a lot of duplicated code, since java-cup files cannot build on one another. It may be possible to factor out some larger code blocks, e.g., the side condition checking for match terms. Error handling is not very sophisticated, yet. Some errors in the proof result in thrown exceptions that are not caught. Terms that don't type-check may lead to null pointer exceptions.
Known Bugs in SMTInterpol proofs: 1. SMTInterpol currently produces proofs with undeclared free variables when a quantifier is instantiated but not all variables are used in the subformula. 2. The unletter may rename bounded variables (in case of name clashes), which may result in a perfectly valid proof to be reported as invalid, because the variable names in the input formula differ. Also the produced proof by SMTInterpol may be wrong due to the renaming.