From 94af13b18b10d6092981848fbae1b9c35b27b31d Mon Sep 17 00:00:00 2001
From: Mathias Preiner <mathias.preiner@gmail.com>
Date: Wed, 14 Aug 2019 10:56:26 -0700
Subject: [PATCH] cmake: Export CVC4 library interface. (#3179)

---
 CMakeLists.txt            | 31 +++++++++++++++++++++++++++++++
 cmake/CVC4Config.cmake.in |  5 +++++
 src/CMakeLists.txt        | 32 +++++++++++++++++++++-----------
 src/parser/CMakeLists.txt |  4 +++-
 4 files changed, 60 insertions(+), 12 deletions(-)
 create mode 100644 cmake/CVC4Config.cmake.in

diff --git a/CMakeLists.txt b/CMakeLists.txt
index 0748c8075..e9e684b6e 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -481,6 +481,37 @@ if(BUILD_BINDINGS_JAVA OR BUILD_BINDINGS_PYTHON)
   add_subdirectory(src/bindings)
 endif()
 
+#-----------------------------------------------------------------------------#
+# Package configuration
+#
+# Export CVC4 targets to support find_package(CVC4) in other cmake projects.
+
+include(CMakePackageConfigHelpers)
+
+install(EXPORT cvc4-targets
+  FILE CVC4Targets.cmake
+  NAMESPACE CVC4::
+  DESTINATION lib/cmake/CVC4)
+
+configure_package_config_file(
+  ${CMAKE_SOURCE_DIR}/cmake/CVC4Config.cmake.in
+  ${CMAKE_BINARY_DIR}/cmake/CVC4Config.cmake
+  INSTALL_DESTINATION lib/cmake/CVC4
+)
+
+write_basic_package_version_file(
+  ${CMAKE_CURRENT_BINARY_DIR}/CVC4ConfigVersion.cmake
+  VERSION ${CVC4_RELEASE_STRING}
+  COMPATIBILITY SameMinorVersion
+)
+
+install(FILES
+  ${CMAKE_BINARY_DIR}/cmake/CVC4Config.cmake
+  ${CMAKE_BINARY_DIR}/CVC4ConfigVersion.cmake
+  DESTINATION lib/cmake/CVC4
+)
+
+
 #-----------------------------------------------------------------------------#
 # Print build configuration
 
diff --git a/cmake/CVC4Config.cmake.in b/cmake/CVC4Config.cmake.in
new file mode 100644
index 000000000..f2eec75c6
--- /dev/null
+++ b/cmake/CVC4Config.cmake.in
@@ -0,0 +1,5 @@
+@PACKAGE_INIT@
+
+if(NOT TARGET CVC4::cvc4)
+  include(${CMAKE_CURRENT_LIST_DIR}/CVC4Targets.cmake)
+endif()
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 30594e269..16feace50 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -737,7 +737,16 @@ add_subdirectory(util)
 
 set_source_files_properties(${LIBCVC4_GEN_SRCS} PROPERTIES GENERATED TRUE)
 add_library(cvc4 ${LIBCVC4_SRCS} ${LIBCVC4_GEN_SRCS})
-install(TARGETS cvc4 DESTINATION lib)
+target_include_directories(cvc4
+  PUBLIC
+    $<BUILD_INTERFACE:${CMAKE_CURRENT_SOURCE_DIR}>
+    $<INSTALL_INTERFACE:include>
+)
+
+install(TARGETS cvc4
+  EXPORT cvc4-targets
+  LIBRARY DESTINATION lib
+  ARCHIVE DESTINATION lib)
 
 set_target_properties(cvc4 PROPERTIES SOVERSION ${CVC4_SOVERSION})
 target_compile_definitions(cvc4
@@ -751,44 +760,45 @@ add_dependencies(cvc4 gen-expr gen-gitinfo gen-options gen-tags gen-theory)
 
 # Add library/include dependencies
 if(ENABLE_VALGRIND)
-  target_include_directories(cvc4 PUBLIC ${Valgrind_INCLUDE_DIR})
+  target_include_directories(cvc4 PRIVATE ${Valgrind_INCLUDE_DIR})
 endif()
 if(USE_ABC)
   target_link_libraries(cvc4 ${ABC_LIBRARIES})
-  target_include_directories(cvc4 PUBLIC ${ABC_INCLUDE_DIR})
+  target_include_directories(cvc4 PRIVATE ${ABC_INCLUDE_DIR})
 endif()
 if(USE_CADICAL)
   target_link_libraries(cvc4 ${CaDiCaL_LIBRARIES})
-  target_include_directories(cvc4 PUBLIC ${CaDiCaL_INCLUDE_DIR})
+  target_include_directories(cvc4 PRIVATE ${CaDiCaL_INCLUDE_DIR})
 endif()
 if(USE_CLN)
   target_link_libraries(cvc4 ${CLN_LIBRARIES})
-  target_include_directories(cvc4 PUBLIC ${CLN_INCLUDE_DIR})
+  target_include_directories(cvc4 PUBLIC $<BUILD_INTERFACE:${CLN_INCLUDE_DIR}>)
 endif()
 if(USE_CRYPTOMINISAT)
   target_link_libraries(cvc4 ${CryptoMiniSat_LIBRARIES})
-  target_include_directories(cvc4 PUBLIC ${CryptoMiniSat_INCLUDE_DIR})
+  target_include_directories(cvc4 PRIVATE ${CryptoMiniSat_INCLUDE_DIR})
 endif()
 if(USE_DRAT2ER)
   target_link_libraries(cvc4 ${Drat2Er_LIBRARIES})
-  target_include_directories(cvc4 PUBLIC ${Drat2Er_INCLUDE_DIR})
+  target_include_directories(cvc4 PRIVATE ${Drat2Er_INCLUDE_DIR})
 endif()
 if(USE_GLPK)
   target_link_libraries(cvc4 ${GLPK_LIBRARIES})
-  target_include_directories(cvc4 PUBLIC ${GLPK_INCLUDE_DIR})
+  target_include_directories(cvc4 PRIVATE ${GLPK_INCLUDE_DIR})
 endif()
 if(USE_LFSC)
   target_link_libraries(cvc4 ${LFSC_LIBRARIES})
-  target_include_directories(cvc4 PUBLIC ${LFSC_INCLUDE_DIR})
+  target_include_directories(cvc4 PRIVATE ${LFSC_INCLUDE_DIR})
 endif()
 if(USE_SYMFPU)
-  target_include_directories(cvc4 PUBLIC ${SymFPU_INCLUDE_DIR})
+  target_include_directories(cvc4
+    PUBLIC $<BUILD_INTERFACE:${SymFPU_INCLUDE_DIR}>)
 endif()
 
 # Note: When linked statically GMP needs to be linked after CLN since CLN
 # depends on GMP.
 target_link_libraries(cvc4 ${GMP_LIBRARIES})
-target_include_directories(cvc4 PUBLIC ${GMP_INCLUDE_DIR})
+target_include_directories(cvc4 PUBLIC $<BUILD_INTERFACE:${GMP_INCLUDE_DIR}>)
 
 # Add rt library
 # Note: For glibc < 2.17 we have to additionally link against rt (man clock_gettime).
diff --git a/src/parser/CMakeLists.txt b/src/parser/CMakeLists.txt
index 8ac8baf1b..96790f834 100644
--- a/src/parser/CMakeLists.txt
+++ b/src/parser/CMakeLists.txt
@@ -100,7 +100,9 @@ set_target_properties(cvc4parser PROPERTIES SOVERSION ${CVC4_SOVERSION})
 target_compile_definitions(cvc4parser PRIVATE -D__BUILDING_CVC4PARSERLIB)
 target_link_libraries(cvc4parser cvc4 ${ANTLR_LIBRARIES})
 target_include_directories(cvc4parser PRIVATE ${ANTLR_INCLUDE_DIR})
-install(TARGETS cvc4parser DESTINATION lib)
+install(TARGETS cvc4parser
+  EXPORT cvc4-targets
+  DESTINATION lib)
 
 # The generated lexer/parser files define some functions as
 # __declspec(dllexport) via the ANTLR3_API macro, which leads to lots of
-- 
2.30.2