Canonical sources for HOL4 theorem-proving system. Branch develop is where “mainline development” occurs; when develop passes our regression tests, master is merged forward to catch up.
This is just a couple of minor improvements to allow some more HolSmt self-tests to be enabled and ensure that we don't regress on future improvements. In total, 21 more tests were enabled for cvc5 and Z3, including Z3 with proof reconstruction (although no proof reconstruction improvements were made).
It basically rewrites goals containing some terms not available in SMT-LIB into something SMT provers can understand, by simplifying using existing theorems. However, I think that in the future, a better solution would be for HolSmt to try to find the most appropriate theorems (based on the terms it finds in the assumptions and goal) and translate those theorems to SMT-LIB, so that SMT solvers can reason about them. This would allow solving more goals.
This will be especially important for function definitions, which currently are simply converted into uninterpreted symbols (thus functions are completely opaque to SMT solvers, leading to the impossibility of solving most goals containing them).
I think this concludes my low-hanging fruit improvements for HolSmt, for now. I think there's more that could be done (e.g. fix integer div and mod) but I think that could be done better if/when the work mentioned above is done first.
For now I'd like to focus on trying to add support for proof reconstruction for the most recent version of Z3, which I expect to be a hard and lengthy endeavor, so I don't expect to send PRs any time soon...
mn200
commented
5 months ago
This is just a couple of minor improvements to allow some more HolSmt self-tests to be enabled and ensure that we don't regress on future improvements. In total, 21 more tests were enabled for cvc5 and Z3, including Z3 with proof reconstruction (although no proof reconstruction improvements were made).
It basically rewrites goals containing some terms not available in SMT-LIB into something SMT provers can understand, by simplifying using existing theorems. However, I think that in the future, a better solution would be for HolSmt to try to find the most appropriate theorems (based on the terms it finds in the assumptions and goal) and translate those theorems to SMT-LIB, so that SMT solvers can reason about them. This would allow solving more goals.
This will be especially important for function definitions, which currently are simply converted into uninterpreted symbols (thus functions are completely opaque to SMT solvers, leading to the impossibility of solving most goals containing them).
I think this concludes my low-hanging fruit improvements for HolSmt, for now. I think there's more that could be done (e.g. fix integer div and mod) but I think that could be done better if/when the work mentioned above is done first.
For now I'd like to focus on trying to add support for proof reconstruction for the most recent version of Z3, which I expect to be a hard and lengthy endeavor, so I don't expect to send PRs any time soon...
Thanks!