Other software that smt-switch depends on can come from various different sources, and not all of these are handled correctly at the moment. There is also some inconsistency between the different solvers. Here are the primary cases:
- A dependency is installed at the system level, e.g. by
apt-get on Ubuntu, pacman on Arch Linux, provided by the base system or XCode on macOS, etc. These should be picked up automatically by smt-switch using the mechanism provided by each (CMake preferred, then pkg-config, falling back to manual detection of header and library files).
- A dependency is manually downloaded, built, and installed by the user at a custom location. If provided, this should take precedence over system-level instances of the dependency. To make it easier to use custom versions of dependencies, the configure script should have an argument to add extra paths to the dependency search process. This is called
--dep-path for cvc5, and I think we should use that too.
- A special case of this is dependencies installed with Homebrew. Since that is the semi-official way to install non-Apple software on macOS, we should support libraries installed via Homebrew out of the box.
- A dependency is not installed locally. In this case, we should fall back to transparently downloading and building it as part of the smt-switch build. We should use
FetchContent for CMake-based dependencies and ExternalProject for everything else. This obviates the need to run any sort of extra script on the side of the user. We should provide an argument called --no-auto-download to those that want to disable this behavior (in this case configuring will just fail).I believe all of this behavior should be implemented via find modules. Then we can just use find_package in the main CMake files, which makes them much easier to read and results in a separation of concerns.
Other software that smt-switch depends on can come from various different sources, and not all of these are handled correctly at the moment. There is also some inconsistency between the different solvers. Here are the primary cases:
apt-geton Ubuntu,pacmanon Arch Linux, provided by the base system or XCode on macOS, etc. These should be picked up automatically by smt-switch using the mechanism provided by each (CMake preferred, then pkg-config, falling back to manual detection of header and library files).--dep-pathfor cvc5, and I think we should use that too.FetchContentfor CMake-based dependencies andExternalProjectfor everything else. This obviates the need to run any sort of extra script on the side of the user. We should provide an argument called--no-auto-downloadto those that want to disable this behavior (in this case configuring will just fail).I believe all of this behavior should be implemented via find modules. Then we can just usefind_packagein the main CMake files, which makes them much easier to read and results in a separation of concerns.