Add option to only build library (#4801)

This PR would add an option to only build the CVC4 library and not the parser or executable. This can be used for projects that only intend to use CVC4 through the API.

It seems to be working now, but it's not necessarily the cleanest solution. In particular, if you'd like the polarity to be different I'm happy to change that. Polarity meaning something like "${WITH_BINARY}" STREQUAL "YES" instead of NOT "${LIB_ONLY} STREQUAL "YES" which is admittedly a little strange.

diff --git a/CMakeLists.txt b/CMakeLists.txt
index 2d658ee3193af558ca8abc7383eb703364889a86..5b1d1e2921059212252d6efd9d7ff844b98e216a 100644 (file)
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -174,6 +174,9 @@ set(PROGRAM_PREFIX    "" CACHE STRING "Program prefix on make install")
 option(BUILD_BINDINGS_PYTHON "Build Python bindings based on new C++ API ")
 option(BUILD_BINDINGS_JAVA "Build Java bindings based on new C++ API ")
 
+# Build limitations
+option(BUILD_LIB_ONLY         "Only build the library")
+
 #-----------------------------------------------------------------------------#
 # Internal cmake variables
 
@@ -709,6 +712,8 @@ print_config("GLPK                      :" USE_GLPK)
 print_config("Kissat                    :" USE_KISSAT)
 print_config("LFSC                      :" USE_LFSC)
 print_config("LibPoly                   :" USE_POLY)
+message("")
+print_config("BUILD_LIB_ONLY            :" BUILD_LIB_ONLY)
 
 if(CVC4_USE_CLN_IMP)
   message("MP library                : cln")

diff --git a/configure.sh b/configure.sh
index 3bce5a54801d836d0fddc19ce9be678cc3970861..48d1b82b234300ef17e69478e456a02ef12f2c83 100755 (executable)
--- a/configure.sh
+++ b/configure.sh
@@ -80,6 +80,10 @@ Optional Path to Optional Packages:
   --poly-dir=PATH          path to top level of LibPoly source tree
   --symfpu-dir=PATH        path to top level of SymFPU source tree
 
+Build limitations:
+  --lib-only               only build the library, but not the executable or
+                           the parser (default: off)
+
 EOF
   exit 0
 }
@@ -161,6 +165,8 @@ lfsc_dir=default
 poly_dir=default
 symfpu_dir=default
 
+lib_only=default
+
 #--------------------------------------------------------------------------#
 
 while [ $# -gt 0 ]
@@ -334,6 +340,8 @@ do
     --symfpu-dir) die "missing argument to $1 (try -h)" ;;
     --symfpu-dir=*) symfpu_dir=${1##*=} ;;
 
+    --lib-only) lib_only=ON ;;
+
     -*) die "invalid option '$1' (try -h)";;
 
     *) case $1 in
@@ -455,6 +463,8 @@ cmake_opts=""
   && cmake_opts="$cmake_opts -DPOLY_DIR=$poly_dir"
 [ "$symfpu_dir" != default ] \
   && cmake_opts="$cmake_opts -DSYMFPU_DIR=$symfpu_dir"
+[ "$lib_only" != default ] \
+    && cmake_opts="$cmake_opts -DBUILD_LIB_ONLY=$lib_only"
 [ "$install_prefix" != default ] \
   && cmake_opts="$cmake_opts -DCMAKE_INSTALL_PREFIX=$install_prefix"
 [ -n "$program_prefix" ] \

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 2a5639e9ecf7f066de2474958ef5aed4ea56a9e3..67692f5c0bc2cb099fa1e8592b80add6404f849d 100644 (file)
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -867,7 +867,9 @@ set(KINDS_FILES
 add_subdirectory(base)
 add_subdirectory(expr)
 add_subdirectory(options)
-add_subdirectory(parser)
+if (NOT BUILD_LIB_ONLY)
+  add_subdirectory(parser)
+endif()
 add_subdirectory(theory)
 add_subdirectory(util)
 
@@ -959,7 +961,9 @@ target_link_libraries(cvc4 ${RT_LIBRARIES})
 # target_link_libraries(...) with object libraries for cmake versions <= 3.12.
 # Thus, we can only visit main as soon as all dependencies for cvc4 are set up.
 
-add_subdirectory(main)
+if (NOT BUILD_LIB_ONLY)
+  add_subdirectory(main)
+endif()
 
 #-----------------------------------------------------------------------------#
 # Note:

diff --git a/test/CMakeLists.txt b/test/CMakeLists.txt
index 52a999c1b5500b224eb65f4564c73aa2da1368f7..cc05aff4311bdc4d3024734aeb7683d8dbecbc52 100644 (file)
--- a/test/CMakeLists.txt
+++ b/test/CMakeLists.txt
@@ -21,7 +21,9 @@ add_custom_target(check
 #-----------------------------------------------------------------------------#
 # Add subdirectories
 
-add_subdirectory(regress)
+if (NOT BUILD_LIB_ONLY)
+  add_subdirectory(regress)
+endif()
 add_subdirectory(system EXCLUDE_FROM_ALL)
 
 if(ENABLE_UNIT_TESTING)