diff options
| -rw-r--r-- | CMakeLists.txt | 25 | ||||
| -rwxr-xr-x | configure.sh | 8 | ||||
| -rw-r--r-- | doc/CMakeLists.txt | 13 | ||||
| -rw-r--r-- | proofs/signatures/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | src/CMakeLists.txt | 130 | ||||
| -rw-r--r-- | src/bindings/CMakeLists.txt | 4 | ||||
| -rw-r--r-- | src/bindings/python/CMakeLists.txt | 26 | ||||
| -rw-r--r-- | src/main/CMakeLists.txt | 2 | ||||
| -rw-r--r-- | 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) |