From 479aebfc657eb9bc90fad550f51ec3b3d2efec76 Mon Sep 17 00:00:00 2001
From: Mathias Preiner <mathias.preiner@gmail.com>
Date: Wed, 12 Sep 2018 11:10:01 -0700
Subject: [PATCH] cmake: Add make install rule.

---
 CMakeLists.txt                     |  25 +++---
 configure.sh                       |   8 ++
 doc/CMakeLists.txt                 |  13 +++
 proofs/signatures/CMakeLists.txt   |   1 +
 src/CMakeLists.txt                 | 130 +++++++++++++++++++++++++++++
 src/bindings/CMakeLists.txt        |   4 +
 src/bindings/python/CMakeLists.txt |  26 +++++-
 src/main/CMakeLists.txt            |   2 +
 src/parser/CMakeLists.txt          |   4 +-
 9 files changed, 200 insertions(+), 13 deletions(-)

diff --git a/CMakeLists.txt b/CMakeLists.txt
index 7c7715ad3..b72d097b8 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -8,15 +8,16 @@ endif()
 
 project(cvc4)
 
-# Major component of the version of CVC4.
-set(CVC4_MAJOR 1)
-# Minor component of the version of CVC4.
-set(CVC4_MINOR 7)
-# Release component of the version of CVC4.
-set(CVC4_RELEASE 0)
+set(CVC4_MAJOR   1) # Major component of the version of CVC4.
+set(CVC4_MINOR   7) # Minor component of the version of CVC4.
+set(CVC4_RELEASE 0) # Release component of the version of CVC4.
+
 # Extraversion component of the version of CVC4.
 set(CVC4_EXTRAVERSION "-prerelease")
 
+# Shared library versioning. Increment SOVERSION for every new CVC4 release.
+set(CVC4_SOVERSION 5)
+
 # Full release string for CVC4.
 if(CVC4_RELEASE)
   set(CVC4_RELEASE_STRING
@@ -28,10 +29,6 @@ endif()
 # Define to the full name of this package.
 set(PACKAGE_NAME "${PROJECT_NAME}")
 
-# Shared library versioning. Increment SOVERSION for every new CVC4 release.
-set(CVC4_VERSION "${CVC4_MAJOR}.${CVC4_MINOR}.${CVC4_RELEASE}")
-set(CVC4_SOVERSION 5)
-
 #### These defines are only use in autotools make files, will likely be 
 #### replaced with corresponding CPack stuff
 ## Define to the full name and version of this package.
@@ -250,6 +247,7 @@ option(USE_CADICAL       "Use CaDiCaL SAT solver")
 option(USE_CRYPTOMINISAT "Use CryptoMiniSat SAT solver")
 option(USE_LFSC          "Use LFSC proof checker")
 option(USE_SYMFPU        "Use SymFPU for floating point support")
+option(USE_PYTHON2       "Prefer using Python 2 (for Python bindings)")
 
 # Custom install directories for dependencies
 # If no directory is provided by the user, we first check if the dependency was
@@ -358,6 +356,13 @@ enable_testing()
 
 #-----------------------------------------------------------------------------#
 
+if(USE_PYTHON2)
+  find_package(PythonInterp 2.7 REQUIRED)
+else()
+  find_package(PythonInterp 3)
+  find_package(PythonInterp REQUIRED)
+endif()
+
 set(GMP_HOME ${GMP_DIR})
 find_package(GMP REQUIRED)
 libcvc4_link_libraries(${GMP_LIBRARIES})
diff --git a/configure.sh b/configure.sh
index 00b958f4c..8e31c5da7 100755
--- a/configure.sh
+++ b/configure.sh
@@ -36,6 +36,7 @@ The following flags enable optional features (disable with --no-<option name>).
   --coverage               support for gcov coverage testing
   --profiling              support for gprof profiling
   --unit-testing           support for unit testing
+  --python2                prefer using Python 2 (for Python bindings)
 
 The following options configure parameterized features.
 
@@ -119,6 +120,7 @@ statistics=default
 symfpu=default
 tracing=default
 unit_testing=default
+python2=default
 valgrind=default
 profiling=default
 readline=default
@@ -217,6 +219,9 @@ do
     --unit-testing) unit_testing=ON;;
     --no-unit-testing) unit_testing=OFF;;
 
+    --python2) python2=ON;;
+    --no-python2) python2=OFF;;
+
     --valgrind) valgrind=ON;;
     --no-valgrind) valgrind=OFF;;
 
@@ -335,6 +340,9 @@ cmake_opts=""
 [ $unit_testing != default ] \
   && cmake_opts="$cmake_opts -DENABLE_UNIT_TESTING=$unit_testing" \
   && [ $unit_testing = ON ] && builddir="$builddir-unit_testing"
+[ $python2 != default ] \
+  && cmake_opts="$cmake_opts -DUSE_PYTHON2=$python2" \
+  && [ $python2 = ON ] && builddir="$builddir-python2"
 [ $valgrind != default ] \
   && cmake_opts="$cmake_opts -DENABLE_VALGRIND=$valgrind" \
   && [ $valgrind = ON ] && builddir="$builddir-valgrind"
diff --git a/doc/CMakeLists.txt b/doc/CMakeLists.txt
index 6e9ba73fd..ffa8b7725 100644
--- a/doc/CMakeLists.txt
+++ b/doc/CMakeLists.txt
@@ -25,3 +25,16 @@ configure_file(
 configure_file(
   ${CMAKE_CURRENT_SOURCE_DIR}/options.3cvc_template.in
   ${CMAKE_CURRENT_BINARY_DIR}/options.3cvc_template)
+
+install(FILES ${CMAKE_CURRENT_BINARY_DIR}/cvc4.1 DESTINATION share/man/man1)
+install(FILES ${CMAKE_CURRENT_BINARY_DIR}/cvc4.5 DESTINATION share/man/man5)
+if(ENABLE_PORTFOLIO)
+  install(FILES ${CMAKE_CURRENT_BINARY_DIR}/cvc4.1 DESTINATION share/man/man1
+          RENAME pcvc4.1)
+endif()
+install(FILES
+        ${CMAKE_CURRENT_BINARY_DIR}/libcvc4.3
+        ${CMAKE_CURRENT_BINARY_DIR}/libcvc4parser.3
+        ${CMAKE_CURRENT_BINARY_DIR}/options.3cvc
+        ${CMAKE_CURRENT_BINARY_DIR}/SmtEngine.3cvc
+        DESTINATION share/man/man3)
diff --git a/proofs/signatures/CMakeLists.txt b/proofs/signatures/CMakeLists.txt
index 7ef94c388..8af026952 100644
--- a/proofs/signatures/CMakeLists.txt
+++ b/proofs/signatures/CMakeLists.txt
@@ -31,3 +31,4 @@ configure_file(
   ${CMAKE_CURRENT_BINARY_DIR}/signatures.cpp)
 
 libcvc4_add_sources(GENERATED signatures.cpp)
+install(FILES ${core_signature_files} DESTINATION share/cvc4)
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)
-- 
2.30.2