HolSmt: add support for the cvc5 SMT solver + doc update

[someplaceguy]

This PR adds support for the cvc5 SMT solver. It also updates HolSmt's documentation and enables more tests for the Z3 SMT solver.

It is split into 4 commits:

• The first commit is just a small fix to a couple of HolSmt's tests. These tests seemed to expect the goals to be theorems, but in fact they are false.
  • The first one was demonstrated to be false when cvc5 gave me the x=-127 and y=127 counterexample, which I subsequently verified purely in HOL4 just to be sure.
  • The second one was already marked as false and commented out (with a counterexample), but I uncommented it (with an empty list of provers) in preparation for adding a cvc5 satisfiable test (which succeeds when the goal is false) in a subsequent commit.

This minor fix to these two tests was put into a separate commit for two reasons: 1) it's independent of the other improvements/commits, and 2) just to make sure that this reversal in the expected behavior wasn't lost in the noise.

• The second commit adds proper support for the cvc5 SMT solver. Adding support for it was extremely straightforward, exactly as HolSmt's documentation suggested it would be.

The only very minor issue was that cvc5 printed out a warning that performance will not be optimal if a specific logic was not specified. To avoid this warning, I modified HolSmt to prepend a (set-logic <logic>) command to the generated file.

Currently, and just like before this PR, no attempt is being made to determine what is the optimal logic for a query. Instead, Z3 passes NONE (which instructs SmtLib.sml to not generate a set-logic command) and cvc5 passes SOME "ALL" in order to generate a (set-logic ALL) command, as that is what cvc5 suggests should be done in this case.

The HOL4_CVC_EXECUTABLE environment variable is used to find the cvc5 executable, following the same pattern as for the other SMT solvers.

• The third commit updates HolSmt's documentation:
  • URLs were updated and/or changed from http->https.
  • Documentation for the cvc5 solver was added.
  • It is now mentioned that a modern version of Z3 has been tested to work as an oracle (version 4.8.17 specifically, as that's the one I've been testing).
  • It is now clarified that only Z3 2.19 supports proof reconstruction.
  • I've also added a note that Z3 2.19.1 does not work with reals due to an apparent bug in parsing real literals. That said, this note is kind of buried in the download instructions, not sure if it should be mentioned more prominently.
    • As a side note, I've added a workaround to fix this, but then HolSmt failed elsewhere in reconstructing a Z3 2.19.1 proof, and since I'm not familiar with proof reconstruction I decided to scrap the workaround and just document the issue for now.
  • The example session was updated to the newer syntax.

Note: I don't know what are the build commands to generate the documentation PDFs since (ironically) I couldn't find documentation for that. I also have zero LaTeX experience, so I have no idea if the changes I've made to the documentation are correct or how they actually look in rendered form.

• The fourth commit simply enables (or re-enables) tests for Z3 that I've confirmed to be working for both Z3 2.19 (which HolSmt supports for proof reconstruction) and Z3 4.8.17 (a modern version of Z3).

There are a couple of related questions that I haven't dealt with (at least, not yet):

• Does HOL4 run the HolSmt self tests as part of some kind of CI? If so, I wonder which Z3 version is being used.

More importantly, I wonder if support for cvc5 should also be added to the CI pipeline (assuming it exists?). In theory, all that's needed is to install cvc5 and set the HOL4_CVC_EXECUTABLE environment variable to point to it.

• SMT solver reliability.

I know that Z3 (and I believe cvc5 as well) support deterministic queries, by setting a specific random seed and by setting the search limit to be a specific number of steps rather than a time limit.

However, HolSmt currently does not attempt to do this at all, so I'm guessing that SMT solvers default to using a random seed and running with a time limit as the criteria for giving up when the query is too difficult.

Given that, I wonder if anyone has experienced HolSmt tests to fail occasionally, due to the non-deterministic nature of these time limits and random seeds or if this hasn't been an issue at all?

[mn200]

Thanks for all your work on this. I'd certainly like to get this tested automatically. We have a docker image setup for the CI runs done on Github (@binghe set these up). I also run -t3 tests on a cron job every 24 hours. I'd like to have one or both of these augmented with an appropriate set of SMT installs.

[binghe]

In next days, I will modify our CI docker image with Z3, Yices and latest cvc5 solver installed, and make each of them separately switchable. Besides, it's definitely possible to switch between different versions of each solver.

P. S. I ever reported some test issues with a version of Yices (#1010), thus by default Yices should be disabled. Then perhaps it's time to take a deeper look and see if the problem is HOL itself or Yices.

[binghe]

See #1179