readme update

readme.md

@@ -12,17 +12,24 @@ For the compilation the following prerequisities are needed.
 
 - C++17 compiler and a POSIX shell.
 - [cmake](https://cmake.org/) of version at least 3.0.2
-- [glucose](https://www.labri.fr/perso/lsimon/glucose/) compiled as a library
-  (`lib_release.a`) with incremental capabilities. For more details see [glucose](#glucose) subsection below.
 - [Boost libraries](https://www.boost.org) of version at least 1.64.0. Some of the
   boost libraries have their own dependencies within the boost library.
     - [Boost Graph Library](https://www.boost.org/doc/libs/1_71_0/libs/graph/doc/index.html),
     in this library, only the header files are needed.
     - [Boost.Program_options](https://www.boost.org/doc/libs/1_77_0/doc/html/program_options.html)
     is needed as a compiled library.
-- (OPTIONAL) [kissat](https://github.com/arminbiere/kissat) -- Kissat solver
+- (OPTIONAL) [Glucose](https://www.labri.fr/perso/lsimon/glucose/) compiled as a library
+  (`lib_release.a`) with incremental capabilities. For more details see [glucose](#glucose) subsection below.
+- (OPTIONAL) [CaDiCaL](https://github.com/arminbiere/cadical) -- CaDiCaL solver
+  for using as a general solver (also as an incremental solver)
+- (OPTIONAL) [Kissat](https://github.com/arminbiere/kissat) -- Kissat solver
   for checking propagation completeness as an option
 
+Note that although the solvers listed above are marked as optional, to compile
+the project, at least one of the solvers with incremental capabilities must be
+present. In particular, this applies to Glucose and CaDiCaL, so at least one of
+them must be available.
+
 ### Options parsing
 
 Until version 2.4, the programs needed library
@@ -35,9 +42,10 @@ config files and makes thus easy to use different sets of parameters.
 
 ## Compilation
 
-### Glucose
+### Glucose (OPTIONAL)
 
-Glucose solver can be downloaded at https://www.labri.fr/perso/lsimon/glucose
+Glucose solver can be downloaded at
+[https://www.labri.fr/perso/lsimon/glucose](https://www.labri.fr/perso/lsimon/glucose)
 If you want to make the compilation a bit simpler for yourself, then see below a
 [note on the patched version](#patched-version).
 
@@ -85,6 +93,22 @@ To simplify the matter, a patched version is
 configured for the incremental solving. In this version only `make libr` in the
 `simp` subdirectory should be sufficient.
 
+### CaDiCaL (OPTIONAL)
+
+Project can be compiled with CaDiCaL support. In order to do that, it
+is enough to have correctly set path to the CaDiCaL home directory and have it
+compiled (i.e. `libcadical.a` must exist in the `build` subdirectory).
+
+- The CaDiCaL home directory is the one with subdirectories `src` and `build`.
+- The default path to the CaDiCaL home directory is set to `solvers/cadical`
+  relative to the main project directory. A different path can be specified
+  using `CADICAL_HOME` shell variable during the configuration using cmake.
+- It is possible to avoid compilation of CaDiCaL support even if `libcadical.a`
+  is compiled and prace at the correct location, just use parameter
+  `-DUSE_CADICAL=OFF` when invoking cmake. Alternatively, call `make cmake
+  USE_CADICAL=OFF` in the main project directory to call cmake with the right
+  parameters.
+
 ### Kissat (OPTIONAL)
 
 Project can be optionally compiled with Kissat support. In order to do that, it
@@ -100,14 +124,6 @@ compiled (i.e. `libkissat.a` must exist in the `build` subdirectory).
   `-DUSE_KISSAT=OFF` when invoking cmake. Alternatively, call `make cmake
   USE_KISSAT=OFF` in the main project directory to call cmake with the right
   parameters.
-- If `pccompile` or `pccheck` are compiled with Kissat support, then Kissat can
-  be selected using option `--pccheck-solver`.
-
-#### Kissat on macOS
-
-Currently, Kissat calls may fail (with `bus error`) under macOS and thus using
-Kissat with pccompile on macOS is not recommended, it should be fine under
-Linux.
 
 ### The subool library and programs
 
@@ -140,13 +156,24 @@ main project directory
 
 # Programs
 
-The program main files are in the `bin` subdirectory. All programs should admit
+The program main files are in the `bin` subdirectory. All programs admit
 options `--version` giving a one line program description and `--help` giving
 the description of available parameters.
 
 In all utilities a CNF is expected in the DIMACS format, a DNNF is expected in
 the format used by [c2d](http://reasoning.cs.ucla.edu/c2d/) compiler.
 
+Programs that use a SAT solver for some task, allow choosing a general purpose
+(incremental) solver using `--solver` option and a nonincremental solver using
+`--nonincremental` option. If nonincremental solver is not specified
+explicitly, the general purpose solver is used also as a nonicremental solver.
+If the two solver types are specified, then the incremental solver is used in
+all algorithms which take advantage of incremental capabilities of a solver
+(e.g. computing a prime CNF, finding backbone literals, etc.), the
+nonicremental solver is used in queries that do not require incremental
+approach (e.g. SAT based check of propagation completeness in `pccompile` and
+`pccheck`).
+
 ## pccompile, pccheck, and pcminimize
 
 The program `pccompile` implements a compiler of a CNF into a PC (or URC)