cmake: Add make install rule.

5 files changed, 163 insertions, 3 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index a0bb3b0cf..17d7fd814 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -674,3 +674,133 @@ target_compile_definitions(cvc4
 add_dependencies(cvc4 gen-expr gen-options gen-tags gen-theory)
 target_link_libraries(cvc4 ${LIBCVC4_LIBRARIES})
 target_include_directories(cvc4 PUBLIC ${LIBCVC4_INCLUDES})
+install(TARGETS cvc4 DESTINATION lib)
+
+# Note:
+# We define all install commands for all public headers here in one
+# place so that we can easily remove them as soon as we enforce the new
+# C++ API.
+#
+# All (generated) headers that either include cvc4_public.h or
+# cvc4parser_public.h need to be listed explicitly here.
+#
+install(FILES
+          api/cvc4cpp.h
+          api/cvc4cppkind.h
+        DESTINATION
+          include/api)
+install(FILES
+          base/configuration.h
+          base/exception.h
+          base/listener.h
+          base/modal_exception.h
+        DESTINATION
+          include/base)
+install(FILES
+          context/cdhashmap_forward.h
+          context/cdhashset_forward.h
+          context/cdinsert_hashmap_forward.h
+          context/cdlist_forward.h
+        DESTINATION
+          include/context)
+install(FILES
+          include/cvc4.h
+          include/cvc4_public.h
+          include/cvc4parser_public.h
+        DESTINATION
+          include)
+install(FILES
+          expr/array.h
+          expr/array_store_all.h
+          expr/ascription_type.h
+          expr/chain.h
+          expr/datatype.h
+          expr/emptyset.h
+          expr/expr_iomanip.h
+          expr/expr_stream.h
+          expr/pickler.h
+          expr/record.h
+          expr/symbol_table.h
+          expr/type.h
+          expr/uninterpreted_constant.h
+          expr/variable_type_map.h
+          ${CMAKE_CURRENT_BINARY_DIR}/expr/expr.h
+          ${CMAKE_CURRENT_BINARY_DIR}/expr/kind.h
+          ${CMAKE_CURRENT_BINARY_DIR}/expr/expr_manager.h
+        DESTINATION
+          include/expr)
+install(FILES
+          options/argument_extender.h
+          options/arith_heuristic_pivot_rule.h
+          options/arith_propagation_mode.h
+          options/arith_unate_lemma_mode.h
+          options/datatypes_modes.h
+          options/language.h
+          options/option_exception.h
+          options/options.h
+          options/printer_modes.h
+          options/quantifiers_modes.h
+          options/set_language.h
+          options/simplification_mode.h
+          options/sygus_out_mode.h
+          options/theoryof_mode.h
+        DESTINATION
+          include/options)
+install(FILES
+          parser/input.h
+          parser/parser.h
+          parser/parser_builder.h
+          parser/parser_exception.h
+        DESTINATION
+          include/parser)
+install(FILES
+          printer/sygus_print_callback.h
+        DESTINATION
+          include/printer)
+install(FILES
+          proof/unsat_core.h
+        DESTINATION
+          include/proof)
+install(FILES
+          smt/command.h
+          smt/logic_exception.h
+          smt/smt_engine.h
+        DESTINATION
+          include/smt)
+install(FILES
+          smt_util/lemma_channels.h
+          smt_util/lemma_input_channel.h
+          smt_util/lemma_output_channel.h
+        DESTINATION
+          include/smt_util)
+install(FILES
+          theory/logic_info.h
+        DESTINATION
+          include/theory)
+install(FILES
+        util/abstract_value.h
+        util/bitvector.h
+        util/bool.h
+        util/cardinality.h
+        util/channel.h
+        util/divisible.h
+        util/gmp_util.h
+        util/hash.h
+        util/integer_cln_imp.h
+        util/integer_gmp_imp.h
+        util/maybe.h
+        util/proof.h
+        util/rational_cln_imp.h
+        util/rational_gmp_imp.h
+        util/regexp.h
+        util/resource_manager.h
+        util/result.h
+        util/sexpr.h
+        util/statistics.h
+        util/tuple.h
+        util/unsafe_interrupt_exception.h
+        ${CMAKE_CURRENT_BINARY_DIR}/util/floatingpoint.h
+        ${CMAKE_CURRENT_BINARY_DIR}/util/integer.h
+        ${CMAKE_CURRENT_BINARY_DIR}/util/rational.h
+        DESTINATION
+          include/util)
diff --git a/src/bindings/CMakeLists.txt b/src/bindings/CMakeLists.txt
index a9032b0d9..1c62ecd58 100644
--- a/src/bindings/CMakeLists.txt
+++ b/src/bindings/CMakeLists.txt
@@ -1,3 +1,7 @@
+if(NOT ENABLE_SHARED)
+  message(FATAL_ERROR "Can't build language bindings for static CVC4 build.")
+endif()
+
 find_package(SWIG 3.0.0 REQUIRED)
 include(${SWIG_USE_FILE})
 
diff --git a/src/bindings/python/CMakeLists.txt b/src/bindings/python/CMakeLists.txt
index 2c2c50126..44d64fb29 100644
--- a/src/bindings/python/CMakeLists.txt
+++ b/src/bindings/python/CMakeLists.txt
@@ -1,4 +1,10 @@
-find_package(PythonLibs REQUIRED)
+# Make sure that interpreter and libraries have a compatible version.
+# Note: We use the Python interpreter to determine the install path for Python
+# modules.  If the interpreter and library have different version, the module
+# will be installed for the wrong Python version. Hence, we require the library
+# version to match the Python interpreter's version.
+find_package(PythonLibs
+             ${PYTHON_VERSION_MAJOR}.${PYTHON_VERSION_MINOR} REQUIRED)
 include_directories(${PYTHON_INCLUDE_DIRS})
 
 set(SWIG_MODULE_CVC4_EXTRA_DEPS cvc4 cvc4parser)
@@ -17,3 +23,21 @@ else()
   swig_add_library(CVC4 LANGUAGE Python SOURCES ${CVC4_SWIG_INTERFACE})
 endif()
 swig_link_libraries(CVC4 cvc4 cvc4parser ${PYTHON_LIBRARIES})
+
+
+# Install Python bindings to the corresponding python-*/site-packages
+# directory.  Lookup Python module directory and store path in
+# PYTHON_MODULE_PATH.
+execute_process(COMMAND
+                  ${PYTHON_EXECUTABLE} -c
+                    "from distutils.sysconfig import get_python_lib;\
+                     print(get_python_lib(plat_specific=True,\
+                             prefix='${CMAKE_INSTALL_PREFIX}'))"
+                OUTPUT_VARIABLE PYTHON_MODULE_PATH
+                OUTPUT_STRIP_TRAILING_WHITESPACE)
+
+# Copy _CVC4.so and CVC4.py to PYTHON_MODULE_PATH
+install(TARGETS ${SWIG_MODULE_CVC4_REAL_NAME}
+        DESTINATION ${PYTHON_MODULE_PATH})
+install(FILES ${CMAKE_CURRENT_BINARY_DIR}/CVC4.py
+        DESTINATION ${PYTHON_MODULE_PATH})
diff --git a/src/main/CMakeLists.txt b/src/main/CMakeLists.txt
index a95517929..a0cbd3b77 100644
--- a/src/main/CMakeLists.txt
+++ b/src/main/CMakeLists.txt
@@ -36,6 +36,7 @@ set_target_properties(cvc4-bin
     OUTPUT_NAME cvc4
     RUNTIME_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/bin)
 target_link_libraries(cvc4-bin cvc4 cvc4parser)
+install(TARGETS cvc4-bin DESTINATION bin)
 
 if(ENABLE_PORTFOLIO)
   set(pcvc4_src_files
@@ -56,6 +57,7 @@ if(ENABLE_PORTFOLIO)
       RUNTIME_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/bin)
   target_link_libraries(pcvc4-bin cvc4 cvc4parser ${Boost_LIBRARIES})
   target_include_directories(pcvc4-bin PRIVATE ${Boost_INCLUDE_DIRS})
+  install(TARGETS pcvc4-bin DESTINATION bin)
 endif()
 
 if(USE_READLINE)
diff --git a/src/parser/CMakeLists.txt b/src/parser/CMakeLists.txt
index c2b3d76ad..d78068f6b 100644
--- a/src/parser/CMakeLists.txt
+++ b/src/parser/CMakeLists.txt
@@ -78,8 +78,8 @@ foreach(lang Cvc Smt1 Smt2 Tptp)
 endforeach()
 
 add_library(cvc4parser ${cvc4parser_src_files})
-set_target_properties(cvc4parser
-  PROPERTIES VERSION ${CVC4_VERSION} SOVERSION ${CVC4_SOVERSION})
+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)