Add CMake support for building and linking against CaDiCaL using the IPASIR interface

[NlightNFotis]

Expand the CMake build to be able to link against IPASIR supporting solvers. Two
new solver configurations have been added:

• CaDiCaL, which should be easy to compile against (-Dsat_impl=ipasir_cadical will handle downloading, building and linking against the solver), and
• Any arbitrary solver supporting the IPASIR interface (for the more adventurous demanding users, who may want to link against a different variety of solvers). This is more involved as an option (requires a number of different flags to be passed to CMake).

This expands our configuration options significantly. Previously, we could do one of two things:

• Build with cmake using the internal CaDiCaL interface (satcheck_cadical), or
• Build with make using the IPASIR interface.

This now allows us to build using both of the build systems, and link with a number of different solvers, for both testing and production use.

• Each commit message has a non-empty body, explaining why the change was made.
• Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
• The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
• Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
• My commit message includes data points confirming performance improvements (if claimed).
• My PR is restricted to a single feature or bugfix.
• White-space or formatting changes outside the feature-related changed lines are in commits of their own.

[TGWDB]

This uses CaDiCaL 1.4.0 and the non-IPASIR path uses CaDiCaL 1.3.0, can these by made the same version?

[NlightNFotis]

Yes, I have it on my todo list, though it needs to be submitted as a different PR - I prefer PRs to be isolated to single feature changes.

[tautschnig]

I'd have the commit accomplishing this at tautschnig@330542a, but thus far held back on creating a PR as performance needs to be evaluated (I vaguely recall a regression).

[TGWDB]

I'm curious how much of the IPASIR building configuration is specific to CaDiCaL and how much is generic? Is it easy to link against another IPASIR compatible solver if one already has the correct path information to pass in to cmake? If this is a small addition/extension, this might be nice to include here.

[codecov]

Codecov Report

Merging #6075 (9bc54a2) into develop (0e34169) will increase coverage by 0.28%.
The diff coverage is 71.61%.

@@             Coverage Diff             @@
##           develop    #6075      +/-   ##
===========================================
+ Coverage    74.25%   74.53%   +0.28%     
===========================================
  Files         1445     1447       +2     
  Lines       157479   157761     +282     
===========================================
+ Hits        116933   117587     +654     
+ Misses       40546    40174     -372     

Impacted Files	Coverage Δ
src/ansi-c/expr2c.cpp	69.10% <ø> (+10.62%)	⬆️
src/goto-checker/properties.cpp	72.56% <ø> (+5.32%)	⬆️
src/util/format_expr.cpp	84.93% <ø> (-0.72%)	⬇️
src/util/pointer_expr.h	77.34% <0.00%> (-22.66%)	⬇️
src/util/simplify_expr_class.h	100.00% <ø> (ø)
...riable-sensitivity/abstract_object/index_range.cpp	100.00% <ø> (ø)
src/util/pointer_expr.cpp	72.82% <5.26%> (-18.96%)	⬇️
src/solvers/flattening/bv_pointers.cpp	81.26% <13.04%> (-3.36%)	⬇️
src/util/simplify_expr.cpp	77.72% <69.23%> (-6.77%)	⬇️
src/ansi-c/c_typecheck_expr.cpp	61.70% <75.00%> (-13.47%)	⬇️
... and 702 more

---

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update 598c554...9bc54a2. Read the comment docs.

[TGWDB]

I've checked this on Ubuntu 20.04 with the CaDiCaL and also linked to SATCOMP via the IPASIR path, all worked for me.

[chrisr-diffblue]

Looks good to me. Thanks for the clear instructions!