copilot-theorem: Update examples to compile with copilot-theorem >= 3.0. Refs #692.

[chathhorn-galois]

Some example programs in the copilot-theorem/example subdirectory have bitrotted, as they depend on a Copilot.Theorem.Prover.Z3 module that is no longer included in copilot-theorem.cabal (as of 6a67d89). Attempting to build any of these examples results in compilation failures.

This PR updates the examples to use the Copilot.Theorem.Prover.SMT module in place of the deprecated Copilot.Theorem.Prover.Z3 module. With these updates, all of the examples now compile, but with many warnings and not all of the proofs succeed.

Fixes #692.

[ivanperez-keera]

Change Manager: Can you please alphabetize these imports?

[ivanperez-keera]

Change Manager:

• Please address the comments in the review.
• Please change the first line of the first commit message to:

copilot-theorem: Update examples to compile with copilot-theorem >= 3.0. Refs #692.

• Please rebase your commits on top of the current HEAD in the master branch.

[chathhorn-galois]

Implementor: Fix implemented, review requested.

[ivanperez-keera]

Change Manager: Verified that:

• Solution is implemented:
  • The code proposed compiles and passes all tests. Details:
    Build log: https://app.travis-ci.com/github/Copilot-Language/copilot/builds/278077300
  • The solution proposed produces the expected result. Details:
    The following Dockerfile checks that all the examples that used the removed module Z3 can now be compiled, after which it prints the message "Success":

    FROM ubuntu:jammy
    
    WORKDIR /root
    SHELL ["/bin/bash", "-c"]
    
    ENV DEBIAN_FRONTEND=noninteractive
    RUN apt-get update
    
    RUN apt-get install --yes \
          libz-dev \
          git \
          curl \
          gcc \
          g++ \
          make \
          libgmp3-dev  \
          pkg-config
    
    RUN mkdir -p $HOME/.ghcup/bin
    RUN curl https://downloads.haskell.org/~ghcup/0.1.40.0/x86_64-linux-ghcup-0.1.40.0 -o $HOME/.ghcup/bin/ghcup
    RUN chmod a+x $HOME/.ghcup/bin/ghcup
    ENV PATH=$PATH:/root/.ghcup/bin/
    ENV PATH=$PATH:/root/.cabal/bin/
    
    RUN ghcup install ghc 9.8.4
    RUN ghcup install cabal 3.2
    RUN ghcup set ghc 9.8.4
    RUN cabal update
    
    CMD git clone $REPO && cd $NAME && git checkout $COMMIT && cd .. \
      && cabal v1-sandbox init \
      && cabal v1-install alex happy --constraint='happy <= 2' \
      && cabal v1-install \
           $NAME/copilot/ \
           $NAME/copilot-c99/ \
           $NAME/copilot-core/ \
           $NAME/copilot-prettyprinter/ \
           $NAME/copilot-interpreter/ \
           $NAME/copilot-language/ \
           $NAME/copilot-libraries/ \
           $NAME/copilot-theorem/ \
      && cabal v1-exec -- ghc -XGADTs -c $NAME/copilot-theorem/examples/BoyerMoore.hs \
      && cabal v1-exec -- ghc -XGADTs -c $NAME/copilot-theorem/examples/Grey.hs \
      && cabal v1-exec -- ghc -XGADTs -c $NAME/copilot-theorem/examples/Incr.hs \
      && cabal v1-exec -- ghc -XGADTs -c $NAME/copilot-theorem/examples/SerialBoyerMoore.hs \
      && cabal v1-exec -- ghc -XGADTs -c $NAME/copilot-theorem/examples/SphericalWCV.hs \
      && cabal v1-exec -- ghc -XGADTs -c $NAME/copilot-theorem/examples/WCV.hs \
      && echo "Success"

    Command (substitute variables based on new path after merge):

    $ docker run -e REPO=https://github.com/GaloisInc/copilot-1 -e NAME=copilot-1 -e COMMIT=579b124a56146f563e620ca9df5d9b1c70640a84 copilot-verify-692
    

• Implementation is documented. Details:
  No updates needed; the changes are minimal maintenance updates to examples.
• Change history is clear.
• Commit messages are clear.
• Changelogs are updated.
• Examples are updated. Details:
  The change is to the examples.
• Required version bumps are evaluated. Details:
  Bump not required; change affects examples only.