Add documentation on alternative SAT solvers

This adds documentation on alternativer SAT solvers and how to compile
them using different builds processed and linking methods. In particular
this not documents the make and cmake build processes for CaDiCaL and
glucose, as well as general IPASIR linking.

Author: TGWDB

COMPILING.md

@@ -380,7 +380,44 @@ For the packaged builds of CBMC on our release page we currently build CBMC
 with the MiniSat2 SAT solver statically linked at compile time. However it is
 also possible to build CBMC using alternative SAT solvers.
 
-### Compiling with CaDiCaL
+### Compiling with CBMC Wrapper
+
+The following solvers are supported by CBMC using custom interfaces and can
+by downloaded and compiled by the build process: MiniSAT2, CaDiCaL, and Glucose.
+
+For `make` alternatives to the default (i.e. not MiniSAT) can be built with the
+following commands for CaDiCaL:
+```
+make -C src cadical-download
+make -C src CADICAL=../../cadical
+```
+and for glucose
+```
+make -C src glucose-download
+make -C src GLUCOSE=../../glucose-syrup
+```
+
+For `cmake` the alternatives can be built with the following arguments to `cmake`
+for CaDiCaL `-Dsat_impl=cadical` and for glucose `-Dsat_impl=glucose`.
+
+
+### Compiling with IPASIR Interface
+
+The below compiling instructions allow linking of an arbitrary IPASIR
+compatible SAT solver when compiling CBMC.
+
+The general command using `make` is to compile with
+```
+make -C src LIBS="$PWD/SATOBJ SATLINKFLAGS" IPASIR=$PWD/SATPATH
+```
+Where `SATOBJ` is the pre-compiled IPASIR compatible SAT binary,
+`SATLINKFLAGS` are any flags required by the SAT object file, and
+`SATPATH` is the path to the SAT interface.
+
+The rest of this section provides detailed instructions for some example
+SAT solvers.
+
+#### Compiling with CaDiCaL
 
 The [CaDiCaL](https://github.com/arminbiere/cadical) solver supports the
 [IPASIR](https://github.com/biotomas/ipasir) C interface to incremental SAT
@@ -421,7 +458,7 @@ Note that at the time of writing this has been tested to work with the CaDiCaL
    the IPASIR headers, which is needed for the cbmc includes of `ipasir.h`. The
    compiled binary will be placed in `cbmc/src/cbmc/cbmc`.
 
-### Compiling with Riss
+#### Compiling with Riss
 
 The [Riss](https://github.com/conp-solutions/riss) solver supports the
 [IPASIR](https://github.com/biotomas/ipasir) C interface to incremental SAT