Restore compatibility with cmake 3.9 (#7329)

This goes back to the new cmake setup and makes it compatible again with cmake 3.9.
It mostly means we can not link object libraries and also not link other libraries to object libraries.

I've tested these changes within docker on `ubuntu:18-04` with a manually installed `cmake-3.9.6`.

diff --git a/cmake/FindANTLR3.cmake b/cmake/FindANTLR3.cmake
index 37318290426fdba7fc5a3b9b9b0708d8ad002539..6ef555bacae8e1278010c873bbd2f23261cf4d05 100644 (file)
--- a/cmake/FindANTLR3.cmake
+++ b/cmake/FindANTLR3.cmake
@@ -33,6 +33,15 @@ if(ANTLR3_JAR AND ANTLR3_INCLUDE_DIR AND ANTLR3_RUNTIME)
     check_system_version("ANTLR3")
 endif()
 
+if(ENABLE_STATIC_LIBRARY AND ANTLR3_FOUND_SYSTEM)
+  force_static_library()
+  find_library(ANTLR3_STATIC_LIBRARIES NAMES antlr3c)
+  if(NOT ANTLR3_STATIC_LIBRARIES)
+    set(ANTLR3_FOUND_SYSTEM FALSE)
+  endif()
+  reset_force_static_library()
+endif()
+
 if(NOT ANTLR3_FOUND_SYSTEM)
     check_ep_downloaded("ANTLR3-EP-jar")
     if(NOT ANTLR3-EP-jar_DOWNLOADED)
@@ -114,7 +123,7 @@ if(NOT ANTLR3_FOUND_SYSTEM)
             --prefix=<INSTALL_DIR>
             --libdir=<INSTALL_DIR>/${CMAKE_INSTALL_LIBDIR}
             --srcdir=<SOURCE_DIR>
-            --disable-shared
+            --enable-shared
             --enable-static
             ${64bit}
             --host=${TOOLCHAIN_PREFIX}
@@ -123,7 +132,8 @@ if(NOT ANTLR3_FOUND_SYSTEM)
 
     set(ANTLR3_JAR "${DEPS_BASE}/share/java/antlr-3.4-complete.jar")
     set(ANTLR3_INCLUDE_DIR "${DEPS_BASE}/include/")
-    set(ANTLR3_RUNTIME "${DEPS_BASE}/${CMAKE_INSTALL_LIBDIR}/libantlr3c.a")
+    set(ANTLR3_RUNTIME "${DEPS_BASE}/${CMAKE_INSTALL_LIBDIR}/libantlr3c${CMAKE_SHARED_LIBRARY_SUFFIX}")
+    set(ANTLR3_STATIC_RUNTIME "${DEPS_BASE}/${CMAKE_INSTALL_LIBDIR}/libantlr3c.a")
 endif()
 
 find_package(Java COMPONENTS Runtime REQUIRED)
@@ -135,9 +145,19 @@ set(ANTLR3_FOUND TRUE)
 set(ANTLR3_COMMAND ${Java_JAVA_EXECUTABLE} -cp "${ANTLR3_JAR}" org.antlr.Tool
     CACHE STRING "run ANTLR3" FORCE)
 
-add_library(ANTLR3 STATIC IMPORTED GLOBAL)
-set_target_properties(ANTLR3 PROPERTIES IMPORTED_LOCATION "${ANTLR3_RUNTIME}")
-set_target_properties(ANTLR3 PROPERTIES INTERFACE_INCLUDE_DIRECTORIES "${ANTLR3_INCLUDE_DIR}")
+add_library(ANTLR3_SHARED SHARED IMPORTED GLOBAL)
+set_target_properties(ANTLR3_SHARED PROPERTIES
+    IMPORTED_LOCATION "${ANTLR3_RUNTIME}"
+    INTERFACE_INCLUDE_DIRECTORIES "${ANTLR3_INCLUDE_DIR}"
+)
+
+if(ENABLE_STATIC_LIBRARY)
+    add_library(ANTLR3_STATIC STATIC IMPORTED GLOBAL)
+    set_target_properties(ANTLR3_STATIC PROPERTIES
+        IMPORTED_LOCATION "${ANTLR3_STATIC_RUNTIME}"
+        INTERFACE_INCLUDE_DIRECTORIES "${ANTLR3_INCLUDE_DIR}"
+    )
+endif()
 
 mark_as_advanced(ANTLR3_BINARY)
 mark_as_advanced(ANTLR3_COMMAND)
@@ -153,5 +173,8 @@ if(ANTLR3_FOUND_SYSTEM)
 else()
     message(STATUS "Building ANTLR3 runtime: ${ANTLR3_RUNTIME}")
     message(STATUS "Downloading ANTLR3 JAR: ${ANTLR3_JAR}")
-    add_dependencies(ANTLR3 ANTLR3-EP-runtime ANTLR3-EP-jar)
+    add_dependencies(ANTLR3_SHARED ANTLR3-EP-runtime ANTLR3-EP-jar)
+    if(ENABLE_STATIC_LIBRARY)
+        add_dependencies(ANTLR3_STATIC ANTLR3-EP-runtime ANTLR3-EP-jar)
+    endif()
 endif()

diff --git a/cmake/FindGMP.cmake b/cmake/FindGMP.cmake
index d6780ed249fad961c3b7c0fbb95f930691be0ccc..bd51e8686bc4b702200bd120fc56f94309e0556f 100644 (file)
--- a/cmake/FindGMP.cmake
+++ b/cmake/FindGMP.cmake
@@ -69,11 +69,12 @@ if(NOT GMP_FOUND_SYSTEM)
     CONFIGURE_COMMAND
       <SOURCE_DIR>/configure --prefix=<INSTALL_DIR> --enable-cxx --with-pic
       --enable-shared --enable-static --host=${TOOLCHAIN_PREFIX}
-    BUILD_BYPRODUCTS <INSTALL_DIR>/lib/libgmp.a <INSTALL_DIR>/lib/libgmp.so
+    BUILD_BYPRODUCTS <INSTALL_DIR>/lib/libgmp.a
+                     <INSTALL_DIR>/lib/libgmp${CMAKE_SHARED_LIBRARY_SUFFIX}
   )
 
   set(GMP_INCLUDE_DIR "${DEPS_BASE}/include/")
-  set(GMP_LIBRARIES "${DEPS_BASE}/lib/libgmp.so")
+  set(GMP_LIBRARIES "${DEPS_BASE}/lib/libgmp${CMAKE_SHARED_LIBRARY_SUFFIX}")
   set(GMP_STATIC_LIBRARIES "${DEPS_BASE}/lib/libgmp.a")
 endif()
 

diff --git a/cmake/version.cmake b/cmake/version.cmake
index fcc6c085a7dbf5505e629744adf08536a0f6962d..49b57ed6d190b1a156037f23f21f3de0884763ae 100644 (file)
--- a/cmake/version.cmake
+++ b/cmake/version.cmake
@@ -99,10 +99,18 @@ if(GIT_FOUND)
         list(LENGTH VERSION_LIST VERSION_LIST_LENGTH)
       endwhile()
       # increment patch part
-      list(POP_BACK VERSION_LIST VERSION_LAST_NUMBER)
+      list(GET VERSION_LIST 2 VERSION_LAST_NUMBER)
+      list(REMOVE_AT VERSION_LIST 2)
       math(EXPR VERSION_LAST_NUMBER "${VERSION_LAST_NUMBER} + 1")
       list(APPEND VERSION_LIST ${VERSION_LAST_NUMBER})
-      string(JOIN "." GIT_LAST_TAG ${VERSION_LIST})
+      # join version string into GIT_LAST_TAG
+      list(GET VERSION_LIST 0 GIT_LAST_TAG)
+      while(VERSION_LIST_LENGTH GREATER "1")
+        list(REMOVE_AT VERSION_LIST 0)
+        list(GET VERSION_LIST 0 TMP)
+        set(GIT_LAST_TAG "${GIT_LAST_TAG}.${TMP}")
+        list(LENGTH VERSION_LIST VERSION_LIST_LENGTH)
+      endwhile()
 
       set(CVC5_VERSION "${GIT_LAST_TAG}-dev")
       set(CVC5_FULL_VERSION "${GIT_LAST_TAG}-dev.${GIT_COMMITS_SINCE_TAG}.${GIT_COMMIT}")

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 67347bbf46e52633e57125519873fa3ccb24e6fc..4c418d9284fe73e48a1c9ea673f7d95f52f86970 100644 (file)
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -1304,15 +1304,13 @@ set_source_files_properties(${LIBCVC5_GEN_SRCS} PROPERTIES GENERATED TRUE)
 add_library(cvc5-obj OBJECT ${LIBCVC5_SRCS} ${LIBCVC5_GEN_SRCS})
 target_compile_definitions(cvc5-obj PRIVATE -D__BUILDING_CVC5LIB)
 set_target_properties(cvc5-obj PROPERTIES POSITION_INDEPENDENT_CODE ON)
-target_link_libraries(cvc5-obj PUBLIC $<TARGET_OBJECTS:cvc5base> $<TARGET_OBJECTS:cvc5context>)
 # add_dependencies() is necessary for cmake versions before 3.21
 add_dependencies(cvc5-obj cvc5base cvc5context)
 # Add libcvc5 dependencies for generated sources.
 add_dependencies(cvc5-obj gen-expr gen-versioninfo gen-options gen-tags gen-theory)
 
 # Link the shared library
-add_library(cvc5-shared SHARED)
-target_link_libraries(cvc5-shared PRIVATE cvc5-obj)
+add_library(cvc5-shared SHARED $<TARGET_OBJECTS:cvc5-obj> $<TARGET_OBJECTS:cvc5base> $<TARGET_OBJECTS:cvc5context>)
 set_target_properties(cvc5-shared PROPERTIES SOVERSION ${CVC5_SOVERSION})
 set_target_properties(cvc5-shared PROPERTIES OUTPUT_NAME cvc5)
 target_include_directories(cvc5-shared
@@ -1327,15 +1325,14 @@ install(TARGETS cvc5-shared
 )
 
 if(ENABLE_STATIC_LIBRARY)
-  add_library(cvc5-static STATIC)
-  target_link_libraries(cvc5-static PRIVATE cvc5-obj)
+  add_library(cvc5-static STATIC $<TARGET_OBJECTS:cvc5-obj> $<TARGET_OBJECTS:cvc5base> $<TARGET_OBJECTS:cvc5context>)
   set_target_properties(cvc5-static PROPERTIES OUTPUT_NAME cvc5)
   target_include_directories(cvc5-static
     PUBLIC
       $<BUILD_INTERFACE:${CMAKE_CURRENT_SOURCE_DIR}>
       $<INSTALL_INTERFACE:include>
   )
-  install(TARGETS cvc5-obj cvc5-static
+  install(TARGETS cvc5-static
     EXPORT cvc5-targets
     LIBRARY DESTINATION ${CMAKE_INSTALL_LIBDIR}
     ARCHIVE DESTINATION ${CMAKE_INSTALL_LIBDIR})
@@ -1345,6 +1342,7 @@ include(GenerateExportHeader)
 generate_export_header(cvc5-obj BASE_NAME cvc5)
 
 # Add library/include dependencies
+add_dependencies(cvc5-obj GMP_SHARED)
 target_include_directories(cvc5-obj PRIVATE ${GMP_INCLUDE_DIR})
 target_link_libraries(cvc5-shared PRIVATE GMP_SHARED)
 if(ENABLE_STATIC_LIBRARY)
@@ -1359,9 +1357,15 @@ if(USE_ABC)
   target_link_libraries(cvc5-obj PUBLIC ${ABC_LIBRARIES})
 endif()
 
-target_link_libraries(cvc5-obj PUBLIC CaDiCaL)
+add_dependencies(cvc5-obj CaDiCaL)
+target_include_directories(cvc5-obj PRIVATE ${CaDiCaL_INCLUDE_DIR})
+target_link_libraries(cvc5-shared PRIVATE CaDiCaL)
+if(ENABLE_STATIC_LIBRARY)
+  target_link_libraries(cvc5-static PUBLIC CaDiCaL)
+endif()
 
 if(USE_CLN)
+  add_dependencies(cvc5-obj CLN_SHARED)
   target_include_directories(cvc5-obj PRIVATE ${CLN_INCLUDE_DIR})
   target_link_libraries(cvc5-shared PRIVATE CLN_SHARED)
   if(ENABLE_STATIC_LIBRARY)
@@ -1369,16 +1373,27 @@ if(USE_CLN)
   endif()
 endif()
 if(USE_CRYPTOMINISAT)
-  target_link_libraries(cvc5-obj PUBLIC CryptoMiniSat)
+  add_dependencies(cvc5-obj CryptoMiniSat)
+  target_include_directories(cvc5-obj PRIVATE ${CryptoMiniSat_INCLUDE_DIR})
+  target_link_libraries(cvc5-shared PRIVATE CryptoMiniSat)
+  if(ENABLE_STATIC_LIBRARY)
+    target_link_libraries(cvc5-static PUBLIC CryptoMiniSat)
+  endif()
 endif()
 if(USE_KISSAT)
-  target_link_libraries(cvc5-obj PUBLIC Kissat)
+  add_dependencies(cvc5-obj Kissat)
+  target_include_directories(cvc5-obj PRIVATE ${Kissat_INCLUDE_DIR})
+  target_link_libraries(cvc5-shared PRIVATE Kissat)
+  if(ENABLE_STATIC_LIBRARY)
+    target_link_libraries(cvc5-static PUBLIC Kissat)
+  endif()
 endif()
 if(USE_GLPK)
   target_link_libraries(cvc5-obj PUBLIC ${GLPK_LIBRARIES})
   target_include_directories(cvc5-obj PUBLIC ${GLPK_INCLUDE_DIR})
 endif()
 if(USE_POLY)
+  add_dependencies(cvc5-obj Polyxx_SHARED)
   target_include_directories(cvc5-obj PRIVATE ${Poly_INCLUDE_DIR})
   target_link_libraries(cvc5-shared PRIVATE Polyxx_SHARED)
   if(ENABLE_STATIC_LIBRARY)
@@ -1386,10 +1401,20 @@ if(USE_POLY)
   endif()
 endif()
 if(USE_COCOA)
-  target_link_libraries(cvc5-obj PUBLIC CoCoA)
+  add_dependencies(cvc5-obj CoCoA)
+  target_include_directories(cvc5-obj PRIVATE ${CoCoA_INCLUDE_DIR})
+  target_link_libraries(cvc5-shared PRIVATE CoCoA)
+  if(ENABLE_STATIC_LIBRARY)
+    target_link_libraries(cvc5-static PUBLIC CoCoA)
+  endif()
 endif()
 
-target_link_libraries(cvc5-obj PUBLIC SymFPU)
+add_dependencies(cvc5-obj SymFPU)
+target_include_directories(cvc5-obj PRIVATE ${SymFPU_INCLUDE_DIR})
+target_link_libraries(cvc5-shared PRIVATE SymFPU)
+if(ENABLE_STATIC_LIBRARY)
+  target_link_libraries(cvc5-static PUBLIC SymFPU)
+endif()
 
 #-----------------------------------------------------------------------------#
 # Visit main subdirectory after creating target cvc5. For target main, we have

diff --git a/src/main/CMakeLists.txt b/src/main/CMakeLists.txt
index 8cd96b3f19ba018dc97c1d4b70371874bed5ad62..a16baeb73e8b64b3fdd3cd22d639343920d1e3d6 100644 (file)
--- a/src/main/CMakeLists.txt
+++ b/src/main/CMakeLists.txt
@@ -38,13 +38,7 @@ add_library(main OBJECT ${libmain_src_files} ${libmain_gen_src_files})
 target_compile_definitions(main PRIVATE -D__BUILDING_CVC5DRIVER)
 set_target_properties(main PROPERTIES POSITION_INDEPENDENT_CODE ON)
 
-if(ENABLE_STATIC_BINARY)
-  target_link_libraries(main PUBLIC cvc5-static cvc5parser-static)
-else()
-  target_link_libraries(main PUBLIC cvc5-shared cvc5parser-shared)
-endif()
-
-add_dependencies(main gen-tokens)
+add_dependencies(main gen-tokens cvc5-obj)
 
 # main-test library is only used for linking against api and unit tests so
 # that we don't have to include all object files of main into each api/unit
@@ -62,8 +56,7 @@ endif()
 #-----------------------------------------------------------------------------#
 # cvc5 binary configuration
 
-add_executable(cvc5-bin driver_unified.cpp main.cpp)
-target_link_libraries(cvc5-bin PRIVATE main)
+add_executable(cvc5-bin driver_unified.cpp main.cpp $<TARGET_OBJECTS:main>)
 target_compile_definitions(cvc5-bin PRIVATE -D__BUILDING_CVC5DRIVER)
 set_target_properties(cvc5-bin
   PROPERTIES
@@ -90,6 +83,9 @@ if(ENABLE_STATIC_BINARY)
     set_target_properties(cvc5-bin PROPERTIES LINK_SEARCH_END_STATIC ON)
   endif()
   set_target_properties(cvc5-bin PROPERTIES INSTALL_RPATH "")
+  target_link_libraries(cvc5-bin PUBLIC cvc5-static cvc5parser-static)
+else()
+  target_link_libraries(cvc5-bin PUBLIC cvc5-shared cvc5parser-shared)
 endif()
 
 if(USE_EDITLINE)

diff --git a/src/parser/CMakeLists.txt b/src/parser/CMakeLists.txt
index 32ddfee52501219bbfa88d9cb2714080f59560fd..eed5b53c949a10c336ad3ca04dceac8fbee32701 100644 (file)
--- a/src/parser/CMakeLists.txt
+++ b/src/parser/CMakeLists.txt
@@ -101,24 +101,25 @@ endforeach()
 add_library(cvc5parser-objs OBJECT ${libcvc5parser_src_files})
 set_target_properties(cvc5parser-objs PROPERTIES POSITION_INDEPENDENT_CODE ON)
 target_compile_definitions(cvc5parser-objs PUBLIC -D__BUILDING_CVC5PARSERLIB)
-target_link_libraries(cvc5parser-objs PRIVATE ANTLR3)
 
+add_dependencies(cvc5parser-objs ANTLR3_SHARED)
+target_include_directories(cvc5parser-objs PRIVATE ${ANTLR3_INCLUDE_DIR})
 
-add_library(cvc5parser-shared SHARED)
+add_library(cvc5parser-shared SHARED $<TARGET_OBJECTS:cvc5parser-objs>)
 set_target_properties(cvc5parser-shared PROPERTIES SOVERSION ${CVC5_SOVERSION})
 set_target_properties(cvc5parser-shared PROPERTIES OUTPUT_NAME cvc5parser)
 target_link_libraries(cvc5parser-shared PRIVATE cvc5-shared)
-target_link_libraries(cvc5parser-shared PRIVATE cvc5parser-objs)
+target_link_libraries(cvc5parser-shared PRIVATE ANTLR3_SHARED)
 
 install(TARGETS cvc5parser-shared
   EXPORT cvc5-targets
   DESTINATION ${CMAKE_INSTALL_LIBDIR})
 
 if(ENABLE_STATIC_LIBRARY)
-  add_library(cvc5parser-static STATIC)
+  add_library(cvc5parser-static STATIC $<TARGET_OBJECTS:cvc5parser-objs>)
   set_target_properties(cvc5parser-static PROPERTIES OUTPUT_NAME cvc5parser)
-  target_link_libraries(cvc5parser-static PRIVATE cvc5parser-objs)
   target_link_libraries(cvc5parser-static PRIVATE cvc5-static)
+  target_link_libraries(cvc5parser-static PRIVATE ANTLR3_STATIC)
 
   install(TARGETS cvc5parser-objs cvc5parser-static
     EXPORT cvc5-targets