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
# 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.
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
#-----------------------------------------------------------------------------#
+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})
--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.
symfpu=default
tracing=default
unit_testing=default
+python2=default
valgrind=default
profiling=default
readline=default
--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;;
[ $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"
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)
${CMAKE_CURRENT_BINARY_DIR}/signatures.cpp)
libcvc4_add_sources(GENERATED signatures.cpp)
+install(FILES ${core_signature_files} DESTINATION share/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)
+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})
-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)
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})
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
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)
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)
projects / cvc5.git / commitdiff