diff options
| -rw-r--r-- | .travis.yml | 20 | ||||
| -rw-r--r-- | CMakeLists.txt | 116 | ||||
| -rw-r--r-- | cmake/FindCython.cmake | 77 | ||||
| -rw-r--r-- | cmake/FindPythonExtensions.cmake | 503 | ||||
| -rw-r--r-- | cmake/UseCython.cmake | 403 | ||||
| -rw-r--r-- | cmake/targetLinkLibrariesWithDynamicLookup.cmake | 478 | ||||
| -rwxr-xr-x | configure.sh | 11 | ||||
| -rwxr-xr-x | examples/api/python/bitvectors.py | 121 | ||||
| -rwxr-xr-x | examples/api/python/bitvectors_and_arrays.py | 91 | ||||
| -rwxr-xr-x | examples/api/python/combination.py | 99 | ||||
| -rwxr-xr-x | examples/api/python/datatypes.py | 137 | ||||
| -rwxr-xr-x | examples/api/python/extract.py | 51 | ||||
| -rwxr-xr-x | examples/api/python/helloworld.py | 21 | ||||
| -rwxr-xr-x | examples/api/python/linear_arith.py | 70 | ||||
| -rwxr-xr-x | examples/api/python/sets.py | 85 | ||||
| -rwxr-xr-x | examples/api/python/strings.py | 87 | ||||
| -rw-r--r-- | src/api/cvc4cpp.cpp | 25 | ||||
| -rw-r--r-- | src/api/cvc4cpp.h | 20 | ||||
| -rw-r--r-- | src/api/python/CMakeLists.txt | 42 | ||||
| -rw-r--r-- | src/api/python/cvc4.pxd | 274 | ||||
| -rw-r--r-- | src/api/python/cvc4.pxi | 1181 | ||||
| -rwxr-xr-x | src/api/python/genkinds.py | 255 | ||||
| -rw-r--r-- | src/api/python/pycvc4.pyx | 2 | ||||
| -rw-r--r-- | src/bindings/CMakeLists.txt | 10 | ||||
| -rw-r--r-- | test/CMakeLists.txt | 2 |
25 files changed, 4116 insertions, 65 deletions
diff --git a/.travis.yml b/.travis.yml index fbf0d2bb9..1f646f0de 100644 --- a/.travis.yml +++ b/.travis.yml @@ -23,6 +23,9 @@ addons: - libgmp-dev - libhamcrest-java - openjdk-8-jdk + - python3 + - python3-pip + - python3-setuptools - swig3.0 before_install: - eval "${MATRIX_EVAL}" @@ -43,7 +46,8 @@ script: - ccache -z - ${CC} --version - ${CXX} --version - - sudo pip install toml + - sudo ${TRAVIS_PYTHON} -m pip install toml + - sudo ${TRAVIS_PYTHON} -m pip install Cython==0.29 --install-option="--no-cython-compile" - | echo "travis_fold:start:load_script" normal="$(echo -e '\033[0m')" red="$normal$(echo -e '\033[01;31m')" green="$normal$(echo -e '\033[01;32m')" @@ -103,16 +107,22 @@ matrix: # Test with GCC - compiler: gcc env: - - TRAVIS_CVC4=yes TRAVIS_WITH_LFSC=yes TRAVIS_CVC4_CONFIG='production --language-bindings=java --lfsc' + - TRAVIS_CVC4=yes TRAVIS_WITH_LFSC=yes TRAVIS_CVC4_CONFIG='production --language-bindings=java --lfsc' TRAVIS_PYTHON="python" - compiler: gcc env: - - TRAVIS_CVC4=yes TRAVIS_WITH_LFSC=yes TRAVIS_CVC4_CONFIG='debug --symfpu --lfsc --no-debug-symbols' - + - TRAVIS_CVC4=yes TRAVIS_WITH_LFSC=yes TRAVIS_CVC4_CONFIG='debug --symfpu --lfsc --no-debug-symbols' TRAVIS_PYTHON="python" + # Test python bindings + - compiler: gcc + env: + - TRAVIS_CVC4=yes TRAVIS_WITH_LFSC=yes TRAVIS_CVC4_CONFIG="production --python-bindings --python2" TRAVIS_PYTHON="python" + - compiler: gcc + env: + - TRAVIS_CVC4=yes TRAVIS_WITH_LFSC=yes TRAVIS_CVC4_CONFIG="production --python-bindings --python3" TRAVIS_PYTHON="python3" # # Test with Clang - compiler: clang env: - - TRAVIS_CVC4=yes TRAVIS_WITH_LFSC=yes TRAVIS_CVC4_CONFIG='debug --symfpu --cln --gpl --no-debug-symbols --no-proofs' + - TRAVIS_CVC4=yes TRAVIS_WITH_LFSC=yes TRAVIS_CVC4_CONFIG='debug --symfpu --cln --gpl --no-debug-symbols --no-proofs' TRAVIS_PYTHON="python" notifications: email: on_success: change diff --git a/CMakeLists.txt b/CMakeLists.txt index 1582a3bde..0cc1174d9 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -174,9 +174,12 @@ set(SYMFPU_DIR "" CACHE STRING "Set SymFPU install directory") # Prepend binaries with prefix on make install set(PROGRAM_PREFIX "" CACHE STRING "Program prefix on make install") -# Supported language bindings -option(BUILD_BINDINGS_JAVA "Build Java bindings") -option(BUILD_BINDINGS_PYTHON "Build Python bindings") +# Supported SWIG language bindings +option(BUILD_SWIG_BINDINGS_JAVA "Build Java bindings with SWIG") +option(BUILD_SWIG_BINDINGS_PYTHON "Build Python bindings with SWIG") + +# Supprted language bindings based on new C++ API +option(BUILD_BINDINGS_PYTHON "Build Python bindings based on new C++ API ") #-----------------------------------------------------------------------------# # Internal cmake variables @@ -531,10 +534,14 @@ add_subdirectory(doc) add_subdirectory(src) add_subdirectory(test) -if(BUILD_BINDINGS_JAVA OR BUILD_BINDINGS_PYTHON) +if(BUILD_SWIG_BINDINGS_JAVA OR BUILD_SWIG_BINDINGS_PYTHON) add_subdirectory(src/bindings) endif() +if(BUILD_BINDINGS_PYTHON) + add_subdirectory(src/api/python) +endif() + #-----------------------------------------------------------------------------# # Package configuration # @@ -585,89 +592,90 @@ else() message("Build profile : ${CVC4_BUILD_PROFILE_STRING}") endif() message("") -print_config("GPL :" ENABLE_GPL) -print_config("Best configuration :" ENABLE_BEST) -print_config("Optimization level :" OPTIMIZATION_LEVEL) +print_config("GPL :" ENABLE_GPL) +print_config("Best configuration :" ENABLE_BEST) +print_config("Optimization level :" OPTIMIZATION_LEVEL) message("") -print_config("Assertions :" ENABLE_ASSERTIONS) -print_config("Debug symbols :" ENABLE_DEBUG_SYMBOLS) -print_config("Debug context mem mgr:" ENABLE_DEBUG_CONTEXT_MM) +print_config("Assertions :" ENABLE_ASSERTIONS) +print_config("Debug symbols :" ENABLE_DEBUG_SYMBOLS) +print_config("Debug context mem mgr :" ENABLE_DEBUG_CONTEXT_MM) message("") -print_config("Dumping :" ENABLE_DUMPING) -print_config("Muzzle :" ENABLE_MUZZLE) -print_config("Proofs :" ENABLE_PROOFS) -print_config("Replay :" ENABLE_REPLAY) -print_config("Statistics :" ENABLE_STATISTICS) -print_config("Tracing :" ENABLE_TRACING) +print_config("Dumping :" ENABLE_DUMPING) +print_config("Muzzle :" ENABLE_MUZZLE) +print_config("Proofs :" ENABLE_PROOFS) +print_config("Replay :" ENABLE_REPLAY) +print_config("Statistics :" ENABLE_STATISTICS) +print_config("Tracing :" ENABLE_TRACING) message("") -print_config("ASan :" ENABLE_ASAN) -print_config("UBSan :" ENABLE_UBSAN) -print_config("TSan :" ENABLE_TSAN) -print_config("Coverage (gcov) :" ENABLE_COVERAGE) -print_config("Profiling (gprof) :" ENABLE_PROFILING) -print_config("Unit tests :" ENABLE_UNIT_TESTING) -print_config("Valgrind :" ENABLE_VALGRIND) +print_config("ASan :" ENABLE_ASAN) +print_config("UBSan :" ENABLE_UBSAN) +print_config("TSan :" ENABLE_TSAN) +print_config("Coverage (gcov) :" ENABLE_COVERAGE) +print_config("Profiling (gprof) :" ENABLE_PROFILING) +print_config("Unit tests :" ENABLE_UNIT_TESTING) +print_config("Valgrind :" ENABLE_VALGRIND) message("") -print_config("Shared libs :" ENABLE_SHARED) -print_config("Static binary :" ENABLE_STATIC_BINARY) -print_config("Java bindings :" BUILD_BINDINGS_JAVA) -print_config("Python bindings :" BUILD_BINDINGS_PYTHON) -print_config("Python2 :" USE_PYTHON2) -print_config("Python3 :" USE_PYTHON3) +print_config("Shared libs :" ENABLE_SHARED) +print_config("Static binary :" ENABLE_STATIC_BINARY) +print_config("Java SWIG bindings :" BUILD_SWIG_BINDINGS_JAVA) +print_config("Python SWIG bindings :" BUILD_SWIG_BINDINGS_PYTHON) +print_config("Python bindings :" BUILD_BINDINGS_PYTHON) +print_config("Python2 :" USE_PYTHON2) +print_config("Python3 :" USE_PYTHON3) message("") -print_config("ABC :" USE_ABC) -print_config("CaDiCaL :" USE_CADICAL) -print_config("CryptoMiniSat :" USE_CRYPTOMINISAT) -print_config("drat2er :" USE_DRAT2ER) -print_config("GLPK :" USE_GLPK) -print_config("LFSC :" USE_LFSC) +print_config("ABC :" USE_ABC) +print_config("CaDiCaL :" USE_CADICAL) +print_config("CryptoMiniSat :" USE_CRYPTOMINISAT) +print_config("drat2er :" USE_DRAT2ER) +print_config("GLPK :" USE_GLPK) +print_config("LFSC :" USE_LFSC) if(CVC4_USE_CLN_IMP) - message("MP library : cln") + message("MP library : cln") else() - message("MP library : gmp") + message("MP library : gmp") endif() -print_config("Readline :" ${USE_READLINE}) -print_config("SymFPU :" ${USE_SYMFPU}) +print_config("Readline :" ${USE_READLINE}) +print_config("SymFPU :" ${USE_SYMFPU}) message("") if(ABC_DIR) - message("ABC dir : ${ABC_DIR}") + message("ABC dir : ${ABC_DIR}") endif() if(ANTLR_DIR) - message("ANTLR dir : ${ANTLR_DIR}") + message("ANTLR dir : ${ANTLR_DIR}") endif() if(CADICAL_DIR) - message("CADICAL dir : ${CADICAL_DIR}") + message("CADICAL dir : ${CADICAL_DIR}") endif() if(CRYPTOMINISAT_DIR) - message("CRYPTOMINISAT dir : ${CRYPTOMINISAT_DIR}") + message("CRYPTOMINISAT dir : ${CRYPTOMINISAT_DIR}") endif() if(DRAT2ER_DIR) - message("DRAT2ER dir : ${DRAT2ER_DIR}") + message("DRAT2ER dir : ${DRAT2ER_DIR}") endif() if(GLPK_DIR) - message("GLPK dir : ${GLPK_DIR}") + message("GLPK dir : ${GLPK_DIR}") endif() if(GMP_DIR) - message("GMP dir : ${GMP_DIR}") + message("GMP dir : ${GMP_DIR}") endif() if(LFSC_DIR) - message("LFSC dir : ${LFSC_DIR}") + message("LFSC dir : ${LFSC_DIR}") endif() if(SYMFPU_DIR) - message("SYMFPU dir : ${SYMFPU_DIR}") + message("SYMFPU dir : ${SYMFPU_DIR}") endif() message("") -message("CPPLAGS (-D...) : ${CVC4_DEFINITIONS}") -message("CXXFLAGS : ${CMAKE_CXX_FLAGS}") -message("CFLAGS : ${CMAKE_C_FLAGS}") +message("CPPLAGS (-D...) : ${CVC4_DEFINITIONS}") +message("CXXFLAGS : ${CMAKE_CXX_FLAGS}") +message("CFLAGS : ${CMAKE_C_FLAGS}") message("") -message("Install prefix : ${CMAKE_INSTALL_PREFIX}") +message("Install prefix : ${CMAKE_INSTALL_PREFIX}") message("") if(GPL_LIBS) message( - "CVC4 license : GPLv3 (due to optional libraries; see below)" + "CVC4 license : GPLv3 (due to optional libraries; see below)" "\n" "\n" "Please note that CVC4 will be built against the following GPLed libraries:" @@ -684,7 +692,7 @@ if(GPL_LIBS) ) else() message( - "CVC4 license : modified BSD" + "CVC4 license : modified BSD" "\n" "\n" "Note that this configuration is NOT built against any GPL'ed libraries, so" diff --git a/cmake/FindCython.cmake b/cmake/FindCython.cmake new file mode 100644 index 000000000..6294d2429 --- /dev/null +++ b/cmake/FindCython.cmake @@ -0,0 +1,77 @@ +#.rst: +# FindCython +# ---------- +# +# Find ``cython`` executable. +# +# This module defines the following variables: +# +# ``CYTHON_EXECUTABLE`` +# path to the ``cython`` program +# +# ``CYTHON_VERSION`` +# version of ``cython`` +# +# ``CYTHON_FOUND`` +# true if the program was found +# +# See also UseCython.cmake +# +#============================================================================= +# Copyright 2011 Kitware, Inc. +# +# Licensed under the Apache License, Version 2.0 (the "License"); +# you may not use this file except in compliance with the License. +# You may obtain a copy of the License at +# +# http://www.apache.org/licenses/LICENSE-2.0 +# +# Unless required by applicable law or agreed to in writing, software +# distributed under the License is distributed on an "AS IS" BASIS, +# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +# See the License for the specific language governing permissions and +# limitations under the License. +#============================================================================= + +# Use the Cython executable that lives next to the Python executable +# if it is a local installation. +find_package(PythonInterp) +if(PYTHONINTERP_FOUND) + get_filename_component(_python_path ${PYTHON_EXECUTABLE} PATH) + find_program(CYTHON_EXECUTABLE + NAMES cython cython.bat cython3 + HINTS ${_python_path} + DOC "path to the cython executable") +else() + find_program(CYTHON_EXECUTABLE + NAMES cython cython.bat cython3 + DOC "path to the cython executable") +endif() + +if(CYTHON_EXECUTABLE) + set(CYTHON_version_command ${CYTHON_EXECUTABLE} --version) + + execute_process(COMMAND ${CYTHON_version_command} + OUTPUT_VARIABLE CYTHON_version_output + ERROR_VARIABLE CYTHON_version_error + RESULT_VARIABLE CYTHON_version_result + OUTPUT_STRIP_TRAILING_WHITESPACE) + + if(NOT ${CYTHON_version_result} EQUAL 0) + set(_error_msg "Command \"${CYTHON_version_command}\" failed with") + set(_error_msg "${_error_msg} output:\n${CYTHON_version_error}") + message(SEND_ERROR "${_error_msg}") + else() + if("${CYTHON_version_output}" MATCHES "^[Cc]ython version ([^,]+)") + set(CYTHON_VERSION "${CMAKE_MATCH_1}") + endif() + endif() +endif() + +include(FindPackageHandleStandardArgs) +FIND_PACKAGE_HANDLE_STANDARD_ARGS(Cython REQUIRED_VARS CYTHON_EXECUTABLE) + +mark_as_advanced(CYTHON_EXECUTABLE) + +include(UseCython) + diff --git a/cmake/FindPythonExtensions.cmake b/cmake/FindPythonExtensions.cmake new file mode 100644 index 000000000..892e17c08 --- /dev/null +++ b/cmake/FindPythonExtensions.cmake @@ -0,0 +1,503 @@ +#.rst +# Define functions to create Python modules and executables. +# +# This file defines CMake functions to build Python extension modules and +# stand-alone executables. To use it, first include this file. +# +# find_package(PythonExtensions) +# +# The following variables are defined: +# :: +# +# PYTHON_PREFIX - absolute path to the current Python +# distribution's prefix +# PYTHON_SITE_PACKAGES_DIR - absolute path to the current Python +# distribution's site-packages directory +# PYTHON_RELATIVE_SITE_PACKAGES_DIR - path to the current Python +# distribution's site-packages directory +# relative to its prefix +# PYTHON_SEPARATOR - separator string for file path +# components. Equivalent to ``os.sep`` in +# Python. +# PYTHON_PATH_SEPARATOR - separator string for PATH-style +# environment variables. Equivalent to +# ``os.pathsep`` in Python. +# +# The following functions are defined: +# +# python_extension_module(<Target> +# [LINKED_MODULES_VAR <LinkedModVar>] +# [FORWARD_DECL_MODULES_VAR <ForwardDeclModVar>]) +# +# For libraries meant to be used as Python extension modules, either dynamically +# loaded or directly linked. Amend the configuration of the library target +# (created using ``add_library``) with additional options needed to build and +# use the referenced library as a Python extension module. +# +# Only extension modules that are configured to be built as MODULE libraries can +# be runtime-loaded through the standard Python import mechanism. All other +# modules can only be included in standalone applications that are written to +# expect their presence. In addition to being linked against the libraries for +# these modules, such applications must forward declare their entry points and +# initialize them prior to use. To generate these forward declarations and +# initializations, see ``python_modules_header``. +# +# If ``<Target>`` does not refer to a target, then it is assumed to refer to an +# extension module that is not linked at all, but compiled along with other +# source files directly into an executable. Adding these modules does not cause +# any library configuration modifications, and they are not added to the list of +# linked modules. They still must be forward declared and initialized, however, +# and so are added to the forward declared modules list. +# +# Options: +# +# ``LINKED_MODULES_VAR <LinkedModVar>`` +# Name of the variable referencing a list of extension modules whose libraries +# must be linked into the executables of any stand-alone applications that use +# them. By default, the global property ``PY_LINKED_MODULES_LIST`` is used. +# +# ``FORWARD_DECL_MODULES_VAR <ForwardDeclModVar>`` +# Name of the variable referencing a list of extension modules whose entry +# points must be forward declared and called by any stand-alone applications +# that use them. By default, the global property +# ``PY_FORWARD_DECL_MODULES_LIST`` is used. +# +# +# python_standalone_executable(<Target>) +# +# For standalone executables that initialize their own Python runtime +# (such as when building source files that include one generated by Cython with +# the --embed option). Amend the configuration of the executable target +# (created using ``add_executable``) with additional options needed to properly +# build the referenced executable. +# +# python_modules_header(<Name> [HeaderFilename] +# [FORWARD_DECL_MODULES_LIST <ForwardDeclModList>] +# [HEADER_OUTPUT_VAR <HeaderOutputVar>] +# [INCLUDE_DIR_OUTPUT_VAR <IncludeDirOutputVar>]) +# +# Generate a header file that contains the forward declarations and +# initialization routines for the given list of Python extension modules. +# ``<Name>`` is the logical name for the header file (no file extensions). +# ``<HeaderFilename>`` is the actual destination filename for the header file +# (e.g.: decl_modules.h). +# +# If only ``<Name>`` is provided, and it ends in the ".h" extension, then it +# is assumed to be the ``<HeaderFilename>``. The filename of the header file +# without the extension is used as the logical name. If only ``<Name>`` is +# provided, and it does not end in the ".h" extension, then the +# ``<HeaderFilename>`` is assumed to ``<Name>.h``. +# +# The exact contents of the generated header file depend on the logical +# ``<Name>``. It should be set to a value that corresponds to the target +# application, or for the case of multiple applications, some identifier that +# conveyes its purpose. It is featured in the generated multiple inclusion +# guard as well as the names of the generated initialization routines. +# +# The generated header file includes forward declarations for all listed +# modules, as well as implementations for the following class of routines: +# +# ``int <Name>_<Module>(void)`` +# Initializes the python extension module, ``<Module>``. Returns an integer +# handle to the module. +# +# ``void <Name>_LoadAllPythonModules(void)`` +# Initializes all listed python extension modules. +# +# ``void CMakeLoadAllPythonModules(void);`` +# Alias for ``<Name>_LoadAllPythonModules`` whose name does not depend on +# ``<Name>``. This function is excluded during preprocessing if the +# preprocessing macro ``EXCLUDE_LOAD_ALL_FUNCTION`` is defined. +# +# ``void Py_Initialize_Wrapper();`` +# Wrapper arpund ``Py_Initialize()`` that initializes all listed python +# extension modules. This function is excluded during preprocessing if the +# preprocessing macro ``EXCLUDE_PY_INIT_WRAPPER`` is defined. If this +# function is generated, then ``Py_Initialize()`` is redefined to a macro +# that calls this function. +# +# Options: +# +# ``FORWARD_DECL_MODULES_LIST <ForwardDeclModList>`` +# List of extension modules for which to generate forward declarations of +# their entry points and their initializations. By default, the global +# property ``PY_FORWARD_DECL_MODULES_LIST`` is used. + +# ``HEADER_OUTPUT_VAR <HeaderOutputVar>`` +# Name of the variable to set to the path to the generated header file. By +# default, ``<Name>`` is used. +# +# ``INCLUDE_DIR_OUTPUT_VAR <IncludeDirOutputVar>`` +# Name of the variable to set to the path to the directory containing the +# generated header file. By default, ``<Name>_INCLUDE_DIRS`` is used. +# +# Defined variables: +# +# ``<HeaderOutputVar>`` +# The path to the generated header file +# +# ``<IncludeDirOutputVar>`` +# Directory containing the generated header file +# +# Example usage: +# +# .. code-block:: cmake +# +# find_package(PythonInterp) +# find_package(PythonLibs) +# find_package(PythonExtensions) +# find_package(Cython) +# find_package(Boost COMPONENTS python) +# +# # Simple Cython Module -- no executables +# add_cython_target(_module.pyx) +# add_library(_module MODULE ${_module}) +# python_extension_module(_module) +# +# # Mix of Cython-generated code and C++ code using Boost Python +# # Stand-alone executable -- no modules +# include_directories(${Boost_INCLUDE_DIRS}) +# add_cython_target(main.pyx CXX EMBED_MAIN) +# add_executable(main boost_python_module.cxx ${main}) +# target_link_libraries(main ${Boost_LIBRARIES}) +# python_standalone_executable(main) +# +# # stand-alone executable with three extension modules: +# # one statically linked, one dynamically linked, and one loaded at runtime +# # +# # Freely mixes Cython-generated code, code using Boost-Python, and +# # hand-written code using the CPython API. +# +# # module1 -- statically linked +# add_cython_target(module1.pyx) +# add_library(module1 STATIC ${module1}) +# python_extension_module(module1 +# LINKED_MODULES_VAR linked_module_list +# FORWARD_DECL_MODULES_VAR fdecl_module_list) +# +# # module2 -- dynamically linked +# include_directories({Boost_INCLUDE_DIRS}) +# add_library(module2 SHARED boost_module2.cxx) +# target_link_libraries(module2 ${Boost_LIBRARIES}) +# python_extension_module(module2 +# LINKED_MODULES_VAR linked_module_list +# FORWARD_DECL_MODULES_VAR fdecl_module_list) +# +# # module3 -- loaded at runtime +# add_cython_target(module3a.pyx) +# add_library(module1 MODULE ${module3a} module3b.cxx) +# target_link_libraries(module3 ${Boost_LIBRARIES}) +# python_extension_module(module3 +# LINKED_MODULES_VAR linked_module_list +# FORWARD_DECL_MODULES_VAR fdecl_module_list) +# +# # application executable -- generated header file + other source files +# python_modules_header(modules +# FORWARD_DECL_MODULES_LIST ${fdecl_module_list}) +# include_directories(${modules_INCLUDE_DIRS}) +# +# add_cython_target(mainA) +# add_cython_target(mainC) +# add_executable(main ${mainA} mainB.cxx ${mainC} mainD.c) +# +# target_link_libraries(main ${linked_module_list} ${Boost_LIBRARIES}) +# python_standalone_executable(main) +# +#============================================================================= +# Copyright 2011 Kitware, Inc. +# +# Licensed under the Apache License, Version 2.0 (the "License"); +# you may not use this file except in compliance with the License. +# You may obtain a copy of the License at +# +# http://www.apache.org/licenses/LICENSE-2.0 +# +# Unless required by applicable law or agreed to in writing, software +# distributed under the License is distributed on an "AS IS" BASIS, +# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +# See the License for the specific language governing permissions and +# limitations under the License. +#============================================================================= + +find_package(PythonInterp REQUIRED) +find_package(PythonLibs) +include(targetLinkLibrariesWithDynamicLookup) + +set(_command " +import distutils.sysconfig +import itertools +import os +import os.path +import site +import sys + +result = None +rel_result = None +candidate_lists = [] + +try: + candidate_lists.append((distutils.sysconfig.get_python_lib(),)) +except AttributeError: pass + +try: + candidate_lists.append(site.getsitepackages()) +except AttributeError: pass + +try: + candidate_lists.append((site.getusersitepackages(),)) +except AttributeError: pass + +candidates = itertools.chain.from_iterable(candidate_lists) + +for candidate in candidates: + rel_candidate = os.path.relpath( + candidate, sys.prefix) + if not rel_candidate.startswith(\"..\"): + result = candidate + rel_result = rel_candidate + break + +sys.stdout.write(\";\".join(( + os.sep, + os.pathsep, + sys.prefix, + result, + rel_result, +))) +") + +execute_process(COMMAND "${PYTHON_EXECUTABLE}" -c "${_command}" + OUTPUT_VARIABLE _list + RESULT_VARIABLE _result) + +list(GET _list 0 _item) +set(PYTHON_SEPARATOR "${_item}") +mark_as_advanced(PYTHON_SEPARATOR) + +list(GET _list 1 _item) +set(PYTHON_PATH_SEPARATOR "${_item}") +mark_as_advanced(PYTHON_PATH_SEPARATOR) + +list(GET _list 2 _item) +set(PYTHON_PREFIX "${_item}") +mark_as_advanced(PYTHON_PREFIX) + +list(GET _list 3 _item) +set(PYTHON_SITE_PACKAGES_DIR "${_item}") +mark_as_advanced(PYTHON_SITE_PACKAGES_DIR) + +list(GET _list 4 _item) +set(PYTHON_RELATIVE_SITE_PACKAGES_DIR "${_item}") +mark_as_advanced(PYTHON_RELATIVE_SITE_PACKAGES_DIR) + +function(python_extension_module _target) + set(one_ops LINKED_MODULES_VAR FORWARD_DECL_MODULES_VAR) + cmake_parse_arguments(_args "" "${one_ops}" "" ${ARGN}) + + set(_lib_type "NA") + if(TARGET ${_target}) + get_property(_lib_type TARGET ${_target} PROPERTY TYPE) + endif() + + set(_is_non_lib TRUE) + + set(_is_static_lib FALSE) + if(_lib_type STREQUAL "STATIC_LIBRARY") + set(_is_static_lib TRUE) + set(_is_non_lib FALSE) + endif() + + set(_is_shared_lib FALSE) + if(_lib_type STREQUAL "SHARED_LIBRARY") + set(_is_shared_lib TRUE) + set(_is_non_lib FALSE) + endif() + + set(_is_module_lib FALSE) + if(_lib_type STREQUAL "MODULE_LIBRARY") + set(_is_module_lib TRUE) + set(_is_non_lib FALSE) + endif() + + if(_is_static_lib OR _is_shared_lib OR _is_non_lib) + + if(_is_static_lib OR _is_shared_lib) + if(_args_LINKED_MODULES_VAR) + set(${_args_LINKED_MODULES_VAR} + ${${_args_LINKED_MODULES_VAR}} ${_target} PARENT_SCOPE) + else() + set_property(GLOBAL APPEND PROPERTY PY_LINKED_MODULES_LIST ${_target}) + endif() + endif() + + if(_args_FORWARD_DECL_MODULES_VAR) + set(${_args_FORWARD_DECL_MODULES_VAR} + ${${_args_FORWARD_DECL_MODULES_VAR}} ${_target} PARENT_SCOPE) + else() + set_property(GLOBAL APPEND PROPERTY + PY_FORWARD_DECL_MODULES_LIST ${_target}) + endif() + endif() + + if(NOT _is_non_lib) + include_directories("${PYTHON_INCLUDE_DIRS}") + endif() + + if(_is_module_lib) + set_target_properties(${_target} PROPERTIES + PREFIX "${PYTHON_MODULE_PREFIX}") + endif() + + if(_is_module_lib OR _is_shared_lib) + if(_is_module_lib AND WIN32 AND NOT CYGWIN) + set_target_properties(${_target} PROPERTIES SUFFIX ".pyd") + endif() + + target_link_libraries_with_dynamic_lookup(${_target} ${PYTHON_LIBRARIES}) + endif() +endfunction() + +function(python_standalone_executable _target) + include_directories(${PYTHON_INCLUDE_DIRS}) + target_link_libraries(${_target} ${PYTHON_LIBRARIES}) +endfunction() + +function(python_modules_header _name) + set(one_ops FORWARD_DECL_MODULES_LIST + HEADER_OUTPUT_VAR + INCLUDE_DIR_OUTPUT_VAR) + cmake_parse_arguments(_args "" "${one_ops}" "" ${ARGN}) + + list(GET _args_UNPARSED_ARGUMENTS 0 _arg0) + # if present, use arg0 as the input file path + if(_arg0) + set(_source_file ${_arg0}) + + # otherwise, must determine source file from name, or vice versa + else() + get_filename_component(_name_ext "${_name}" EXT) + + # if extension provided, _name is the source file + if(_name_ext) + set(_source_file ${_name}) + get_filename_component(_name "${_source_file}" NAME_WE) + + # otherwise, assume the source file is ${_name}.h + else() + set(_source_file ${_name}.h) + endif() + endif() + + if(_args_FORWARD_DECL_MODULES_LIST) + set(static_mod_list ${_args_FORWARD_DECL_MODULES_LIST}) + else() + get_property(static_mod_list GLOBAL PROPERTY PY_FORWARD_DECL_MODULES_LIST) + endif() + + string(REPLACE "." "_" _header_name "${_name}") + string(TOUPPER ${_header_name} _header_name_upper) + set(_header_name_upper "_${_header_name_upper}_H") + set(generated_file ${CMAKE_CURRENT_BINARY_DIR}/${_source_file}) + + set(generated_file_tmp "${generated_file}.in") + file(WRITE ${generated_file_tmp} + "/* Created by CMake. DO NOT EDIT; changes will be lost. */\n") + + set(_chunk "") + set(_chunk "${_chunk}#ifndef ${_header_name_upper}\n") + set(_chunk "${_chunk}#define ${_header_name_upper}\n") + set(_chunk "${_chunk}\n") + set(_chunk "${_chunk}#include <Python.h>\n") + set(_chunk "${_chunk}\n") + set(_chunk "${_chunk}#ifdef __cplusplus\n") + set(_chunk "${_chunk}extern \"C\" {\n") + set(_chunk "${_chunk}#endif /* __cplusplus */\n") + set(_chunk "${_chunk}\n") + set(_chunk "${_chunk}#if PY_MAJOR_VERSION < 3\n") + file(APPEND ${generated_file_tmp} "${_chunk}") + + foreach(_module ${static_mod_list}) + file(APPEND ${generated_file_tmp} + "PyMODINIT_FUNC init${PYTHON_MODULE_PREFIX}${_module}(void);\n") + endforeach() + + file(APPEND ${generated_file_tmp} "#else /* PY_MAJOR_VERSION >= 3*/\n") + + foreach(_module ${static_mod_list}) + file(APPEND ${generated_file_tmp} + "PyMODINIT_FUNC PyInit_${PYTHON_MODULE_PREFIX}${_module}(void);\n") + endforeach() + + set(_chunk "") + set(_chunk "${_chunk}#endif /* PY_MAJOR_VERSION >= 3*/\n\n") + set(_chunk "${_chunk}#ifdef __cplusplus\n") + set(_chunk "${_chunk}}\n") + set(_chunk "${_chunk}#endif /* __cplusplus */\n") + set(_chunk "${_chunk}\n") + file(APPEND ${generated_file_tmp} "${_chunk}") + + foreach(_module ${static_mod_list}) + set(_import_function "${_header_name}_${_module}") + set(_prefixed_module "${PYTHON_MODULE_PREFIX}${_module}") + + set(_chunk "") + set(_chunk "${_chunk}int ${_import_function}(void)\n") + set(_chunk "${_chunk}{\n") + set(_chunk "${_chunk} static char name[] = \"${_prefixed_module}\";\n") + set(_chunk "${_chunk} #if PY_MAJOR_VERSION < 3\n") + set(_chunk "${_chunk} return PyImport_AppendInittab(") + set(_chunk "${_chunk}name, init${_prefixed_module});\n") + set(_chunk "${_chunk} #else /* PY_MAJOR_VERSION >= 3 */\n") + set(_chunk "${_chunk} return PyImport_AppendInittab(") + set(_chunk "${_chunk}name, PyInit_${_prefixed_module});\n") + set(_chunk "${_chunk} #endif /* PY_MAJOR_VERSION >= 3 */\n") + set(_chunk "${_chunk}}\n\n") + file(APPEND ${generated_file_tmp} "${_chunk}") + endforeach() + + file(APPEND ${generated_file_tmp} + "void ${_header_name}_LoadAllPythonModules(void)\n{\n") + foreach(_module ${static_mod_list}) + file(APPEND ${generated_file_tmp} " ${_header_name}_${_module}();\n") + endforeach() + file(APPEND ${generated_file_tmp} "}\n\n") + + set(_chunk "") + set(_chunk "${_chunk}#ifndef EXCLUDE_LOAD_ALL_FUNCTION\n") + set(_chunk "${_chunk}void CMakeLoadAllPythonModules(void)\n") + set(_chunk "${_chunk}{\n") + set(_chunk "${_chunk} ${_header_name}_LoadAllPythonModules();\n") + set(_chunk "${_chunk}}\n") + set(_chunk "${_chunk}#endif /* !EXCLUDE_LOAD_ALL_FUNCTION */\n\n") + + set(_chunk "${_chunk}#ifndef EXCLUDE_PY_INIT_WRAPPER\n") + set(_chunk "${_chunk}static void Py_Initialize_Wrapper()\n") + set(_chunk "${_chunk}{\n") + set(_chunk "${_chunk} ${_header_name}_LoadAllPythonModules();\n") + set(_chunk "${_chunk} Py_Initialize();\n") + set(_chunk "${_chunk}}\n") + set(_chunk "${_chunk}#define Py_Initialize Py_Initialize_Wrapper\n") + set(_chunk "${_chunk}#endif /* !EXCLUDE_PY_INIT_WRAPPER */\n\n") + + set(_chunk "${_chunk}#endif /* !${_header_name_upper} */\n") + file(APPEND ${generated_file_tmp} "${_chunk}") + + # with configure_file() cmake complains that you may not use a file created + # using file(WRITE) as input file for configure_file() + execute_process(COMMAND ${CMAKE_COMMAND} -E copy_if_different + "${generated_file_tmp}" "${generated_file}" + OUTPUT_QUIET ERROR_QUIET) + + set(_header_output_var ${_name}) + if(_args_HEADER_OUTPUT_VAR) + set(_header_output_var ${_args_HEADER_OUTPUT_VAR}) + endif() + set(${_header_output_var} ${generated_file} PARENT_SCOPE) + + set(_include_dir_var ${_name}_INCLUDE_DIRS) + if(_args_INCLUDE_DIR_OUTPUT_VAR) + set(_include_dir_var ${_args_INCLUDE_DIR_OUTPUT_VAR}) + endif() + set(${_include_dirs_var} ${CMAKE_CURRENT_BINARY_DIR} PARENT_SCOPE) +endfunction() + diff --git a/cmake/UseCython.cmake b/cmake/UseCython.cmake new file mode 100644 index 000000000..7ff4a276b --- /dev/null +++ b/cmake/UseCython.cmake @@ -0,0 +1,403 @@ +#.rst +# Define a function to create Cython modules. +# +# For more information on the Cython project, see http://cython.org/. +# "Cython is a language that makes writing C extensions for the Python language +# as easy as Python itself." +# +# This file defines a CMake function to build a Cython Python module. +# To use it, first include this file. +# +# include(UseCython) +# +# The following functions are defined: +# +# add_cython_target(<Name> [<CythonInput>] +# [EMBED_MAIN] +# [C | CXX] +# [PY2 | PY3] +# [OUTPUT_VAR <OutputVar>]) +# +# Create a custom rule to generate the source code for a Python extension module +# using cython. ``<Name>`` is the name of the new target, and ``<CythonInput>`` +# is the path to a cython source file. Note that, despite the name, no new +# targets are created by this function. Instead, see ``OUTPUT_VAR`` for +# retrieving the path to the generated source for subsequent targets. +# +# If only ``<Name>`` is provided, and it ends in the ".pyx" extension, then it +# is assumed to be the ``<CythonInput>``. The name of the input without the +# extension is used as the target name. If only ``<Name>`` is provided, and it +# does not end in the ".pyx" extension, then the ``<CythonInput>`` is assumed to +# be ``<Name>.pyx``. +# +# The Cython include search path is amended with any entries found in the +# ``INCLUDE_DIRECTORIES`` property of the directory containing the +# ``<CythonInput>`` file. Use ``iunclude_directories`` to add to the Cython +# include search path. +# +# Options: +# +# ``EMBED_MAIN`` +# Embed a main() function in the generated output (for stand-alone +# applications that initialize their own Python runtime). +# +# ``C | CXX`` +# Force the generation of either a C or C++ file. By default, a C file is +# generated, unless the C language is not enabled for the project; in this +# case, a C++ file is generated by default. +# +# ``PY2 | PY3`` +# Force compilation using either Python-2 or Python-3 syntax and code +# semantics. By default, Python-2 syntax and semantics are used if the major +# version of Python found is 2. Otherwise, Python-3 syntax and sematics are +# used. +# +# ``OUTPUT_VAR <OutputVar>`` +# Set the variable ``<OutputVar>`` in the parent scope to the path to the +# generated source file. By default, ``<Name>`` is used as the output +# variable name. +# +# Defined variables: +# +# ``<OutputVar>`` +# The path of the generated source file. +# +# +# Example usage: +# +# .. code-block:: cmake +# +# find_package(Cython) +# +# # Note: In this case, either one of these arguments may be omitted; their +# # value would have been inferred from that of the other. +# add_cython_target(cy_code cy_code.pyx) +# +# add_library(cy_code MODULE ${cy_code}) +# target_link_libraries(cy_code ...) +# +# Cache variables that effect the behavior include: +# +# ``CYTHON_ANNOTATE`` +# whether to create an annotated .html file when compiling +# +# ``CYTHON_FLAGS`` +# additional flags to pass to the Cython compiler +# +# See also FindCython.cmake +# +#============================================================================= +# Copyright 2011 Kitware, Inc. +# +# Licensed under the Apache License, Version 2.0 (the "License"); +# you may not use this file except in compliance with the License. +# You may obtain a copy of the License at +# +# http://www.apache.org/licenses/LICENSE-2.0 +# +# Unless required by applicable law or agreed to in writing, software +# distributed under the License is distributed on an "AS IS" BASIS, +# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +# See the License for the specific language governing permissions and +# limitations under the License. +#============================================================================= + +# Configuration options. +set(CYTHON_ANNOTATE OFF + CACHE BOOL "Create an annotated .html file when compiling *.pyx.") + +set(CYTHON_FLAGS "" CACHE STRING + "Extra flags to the cython compiler.") +mark_as_advanced(CYTHON_ANNOTATE CYTHON_FLAGS) + +find_package(PythonLibs REQUIRED) + +set(CYTHON_CXX_EXTENSION "cxx") +set(CYTHON_C_EXTENSION "c") + +get_property(languages GLOBAL PROPERTY ENABLED_LANGUAGES) + +function(add_cython_target _name) + set(options EMBED_MAIN C CXX PY2 PY3) + set(options1 OUTPUT_VAR) + cmake_parse_arguments(_args "${options}" "${options1}" "" ${ARGN}) + + list(GET _args_UNPARSED_ARGUMENTS 0 _arg0) + + # if provided, use _arg0 as the input file path + if(_arg0) + set(_source_file ${_arg0}) + + # otherwise, must determine source file from name, or vice versa + else() + get_filename_component(_name_ext "${_name}" EXT) + + # if extension provided, _name is the source file + if(_name_ext) + set(_source_file ${_name}) + get_filename_component(_name "${_source_file}" NAME_WE) + + # otherwise, assume the source file is ${_name}.pyx + else() + set(_source_file ${_name}.pyx) + endif() + endif() + + set(_embed_main FALSE) + + if("C" IN_LIST languages) + set(_output_syntax "C") + elseif("CXX" IN_LIST languages) + set(_output_syntax "CXX") + else() + message(FATAL_ERROR "Either C or CXX must be enabled to use Cython") + endif() + + if("${PYTHONLIBS_VERSION_STRING}" MATCHES "^2.") + set(_input_syntax "PY2") + else() + set(_input_syntax "PY3") + endif() + + if(_args_EMBED_MAIN) + set(_embed_main TRUE) + endif() + + if(_args_C) + set(_output_syntax "C") + endif() + + if(_args_CXX) + set(_output_syntax "CXX") + endif() + + if(_args_PY2) + set(_input_syntax "PY2") + endif() + + if(_args_PY3) + set(_input_syntax "PY3") + endif() + + set(embed_arg "") + if(_embed_main) + set(embed_arg "--embed") + endif() + + set(cxx_arg "") + set(extension "c") + if(_output_syntax STREQUAL "CXX") + set(cxx_arg "--cplus") + set(extension "cxx") + endif() + + set(py_version_arg "") + if(_input_syntax STREQUAL "PY2") + set(py_version_arg "-2") + elseif(_input_syntax STREQUAL "PY3") + set(py_version_arg "-3") + endif() + + set(generated_file "${CMAKE_CURRENT_BINARY_DIR}/${_name}.${extension}") + set_source_files_properties(${generated_file} PROPERTIES GENERATED TRUE) + + set(_output_var ${_name}) + if(_args_OUTPUT_VAR) + set(_output_var ${_args_OUTPUT_VAR}) + endif() + set(${_output_var} ${generated_file} PARENT_SCOPE) + + file(RELATIVE_PATH generated_file_relative + ${CMAKE_BINARY_DIR} ${generated_file}) + + set(comment "Generating ${_output_syntax} source ${generated_file_relative}") + set(cython_include_directories "") + set(pxd_dependencies "") + set(c_header_dependencies "") + + # Get the include directories. + get_source_file_property(pyx_location ${_source_file} LOCATION) + get_filename_component(pyx_path ${pyx_location} PATH) + get_directory_property(cmake_include_directories + DIRECTORY ${pyx_path} + INCLUDE_DIRECTORIES) + list(APPEND cython_include_directories ${cmake_include_directories}) + + # Determine dependencies. + # Add the pxd file with the same basename as the given pyx file. + get_filename_component(pyx_file_basename ${_source_file} NAME_WE) + unset(corresponding_pxd_file CACHE) + find_file(corresponding_pxd_file ${pyx_file_basename}.pxd + PATHS "${pyx_path}" ${cmake_include_directories} + NO_DEFAULT_PATH) + if(corresponding_pxd_file) + list(APPEND pxd_dependencies "${corresponding_pxd_file}") + endif() + + # pxd files to check for additional dependencies + set(pxds_to_check "${_source_file}" "${pxd_dependencies}") + set(pxds_checked "") + set(number_pxds_to_check 1) + while(number_pxds_to_check GREATER 0) + foreach(pxd ${pxds_to_check}) + list(APPEND pxds_checked "${pxd}") + list(REMOVE_ITEM pxds_to_check "${pxd}") + + # look for C headers + file(STRINGS "${pxd}" extern_from_statements + REGEX "cdef[ ]+extern[ ]+from.*$") + foreach(statement ${extern_from_statements}) + # Had trouble getting the quote in the regex + string(REGEX REPLACE + "cdef[ ]+extern[ ]+from[ ]+[\"]([^\"]+)[\"].*" "\\1" + header "${statement}") + unset(header_location CACHE) + find_file(header_location ${header} PATHS ${cmake_include_directories}) + if(header_location) + list(FIND c_header_dependencies "${header_location}" header_idx) + if(${header_idx} LESS 0) + list(APPEND c_header_dependencies "${header_location}") + endif() + endif() + endforeach() + + # check for pxd dependencies + # Look for cimport statements. + set(module_dependencies "") + file(STRINGS "${pxd}" cimport_statements REGEX cimport) + foreach(statement ${cimport_statements}) + if(${statement} MATCHES from) + string(REGEX REPLACE + "from[ ]+([^ ]+).*" "\\1" + module "${statement}") + else() + string(REGEX REPLACE + "cimport[ ]+([^ ]+).*" "\\1" + module "${statement}") + endif() + list(APPEND module_dependencies ${module}) + endforeach() + + # check for pxi dependencies + # Look for include statements. + set(include_dependencies "") + file(STRINGS "${pxd}" include_statements REGEX include) + foreach(statement ${include_statements}) + string(REGEX REPLACE + "include[ ]+[\"]([^\"]+)[\"].*" "\\1" + module "${statement}") + list(APPEND include_dependencies ${module}) + endforeach() + + list(REMOVE_DUPLICATES module_dependencies) + list(REMOVE_DUPLICATES include_dependencies) + + # Add modules to the files to check, if appropriate. + foreach(module ${module_dependencies}) + unset(pxd_location CACHE) + find_file(pxd_location ${module}.pxd + PATHS "${pyx_path}" ${cmake_include_directories} + NO_DEFAULT_PATH) + if(pxd_location) + list(FIND pxds_checked ${pxd_location} pxd_idx) + if(${pxd_idx} LESS 0) + list(FIND pxds_to_check ${pxd_location} pxd_idx) + if(${pxd_idx} LESS 0) + list(APPEND pxds_to_check ${pxd_location}) + list(APPEND pxd_dependencies ${pxd_location}) + endif() # if it is not already going to be checked + endif() # if it has not already been checked + endif() # if pxd file can be found + endforeach() # for each module dependency discovered + + # Add includes to the files to check, if appropriate. + foreach(_include ${include_dependencies}) + unset(pxi_location CACHE) + find_file(pxi_location ${_include} + PATHS "${pyx_path}" ${cmake_include_directories} + NO_DEFAULT_PATH) + if(pxi_location) + list(FIND pxds_checked ${pxi_location} pxd_idx) + if(${pxd_idx} LESS 0) + list(FIND pxds_to_check ${pxi_location} pxd_idx) + if(${pxd_idx} LESS 0) + list(APPEND pxds_to_check ${pxi_location}) + list(APPEND pxd_dependencies ${pxi_location}) + endif() # if it is not already going to be checked + endif() # if it has not already been checked + endif() # if include file can be found + endforeach() # for each include dependency discovered + endforeach() # for each include file to check + + list(LENGTH pxds_to_check number_pxds_to_check) + endwhile() + + # Set additional flags. + set(annotate_arg "") + if(CYTHON_ANNOTATE) + set(annotate_arg "--annotate") + endif() + + set(no_docstrings_arg "") + if(CMAKE_BUILD_TYPE STREQUAL "Release" OR + CMAKE_BUILD_TYPE STREQUAL "MinSizeRel") + set(no_docstrings_arg "--no-docstrings") + endif() + + set(cython_debug_arg "") + set(embed_pos_arg "") + set(line_directives_arg "") + if(CMAKE_BUILD_TYPE STREQUAL "Debug" OR + CMAKE_BUILD_TYPE STREQUAL "RelWithDebInfo") + set(cython_debug_arg "--gdb") + set(embed_pos_arg "--embed-positions") + set(line_directives_arg "--line-directives") + endif() + + # Include directory arguments. + list(REMOVE_DUPLICATES cython_include_directories) + set(include_directory_arg "") + foreach(_include_dir ${cython_include_directories}) + set(include_directory_arg + ${include_directory_arg} "--include-dir" "${_include_dir}") + endforeach() + + list(REMOVE_DUPLICATES pxd_dependencies) + list(REMOVE_DUPLICATES c_header_dependencies) + + # Add the command to run the compiler. + add_custom_command(OUTPUT ${generated_file} + COMMAND ${CYTHON_EXECUTABLE} + ARGS ${cxx_arg} ${include_directory_arg} ${py_version_arg} + ${embed_arg} ${annotate_arg} ${no_docstrings_arg} + ${cython_debug_arg} ${embed_pos_arg} + ${line_directives_arg} ${CYTHON_FLAGS} ${pyx_location} + --output-file ${generated_file} + DEPENDS ${_source_file} + ${pxd_dependencies} + IMPLICIT_DEPENDS ${_output_syntax} + ${c_header_dependencies} + COMMENT ${comment}) + + # NOTE(opadron): I thought about making a proper target, but after trying it + # out, I decided that it would be far too convenient to use the same name as + # the target for the extension module (e.g.: for single-file modules): + # + # ... + # add_cython_target(_module.pyx) + # add_library(_module ${_module}) + # ... + # + # The above example would not be possible since the "_module" target name + # would already be taken by the cython target. Since I can't think of a + # reason why someone would need the custom target instead of just using the + # generated file directly, I decided to leave this commented out. + # + # add_custom_target(${_name} DEPENDS ${generated_file}) + + # Remove their visibility to the user. + set(corresponding_pxd_file "" CACHE INTERNAL "") + set(header_location "" CACHE INTERNAL "") + set(pxd_location "" CACHE INTERNAL "") +endfunction() + diff --git a/cmake/targetLinkLibrariesWithDynamicLookup.cmake b/cmake/targetLinkLibrariesWithDynamicLookup.cmake new file mode 100644 index 000000000..60a0a1956 --- /dev/null +++ b/cmake/targetLinkLibrariesWithDynamicLookup.cmake @@ -0,0 +1,478 @@ +# +# - This module provides the function +# target_link_libraries_with_dynamic_lookup which can be used to +# "weakly" link a loadable module. +# +# Link a library to a target such that the symbols are resolved at +# run-time not link-time. This should be used when compiling a +# loadable module when the symbols should be resolve from the run-time +# environment where the module is loaded, and not a specific system +# library. +# +# Specifically, for OSX it uses undefined dynamic_lookup. This is +# similar to using "-shared" on Linux where undefined symbols are +# ignored. +# +# Additionally, the linker is checked to see if it supports undefined +# symbols when linking a shared library. If it does then the library +# is not linked when specified with this function. +# +# http://blog.tim-smith.us/2015/09/python-extension-modules-os-x/ +# +# +# The following functions are defined: +# +# _get_target_type(<ResultVar> <Target>) +# +# **INTERNAL** Shorthand for querying an abbreviated version of the target type +# of the given ``<Target>``. ``<ResultVar>`` is set to "STATIC" for a +# STATIC_LIBRARY, "SHARED" for a SHARED_LIBRARY, "MODULE" for a MODULE_LIBRARY, +# and "EXE" for an EXECUTABLE. +# +# Defined variables: +# +# ``<ResultVar>`` +# The abbreviated version of the ``<Target>``'s type. +# +# +# _test_weak_link_project(<TargetType> +# <LibType> +# <ResultVar> +# <LinkFlagsVar>) +# +# **INTERNAL** Attempt to compile and run a test project where a target of type +# ``<TargetType>`` is weakly-linked against a dependency of type ``<LibType>``. +# ``<TargetType>`` can be one of "STATIC", "SHARED", "MODULE", or "EXE". +# ``<LibType>`` can be one of "STATIC", "SHARED", or "MODULE". +# +# Defined variables: +# +# ``<ResultVar>`` +# Whether the current C toolchain can produce a working target binary of type +# ``<TargetType>`` that is weakly-linked against a dependency target of type +# ``<LibType>``. +# +# ``<LinkFlagsVar>`` +# List of flags to add to the linker command to produce a working target +# binary of type ``<TargetType>`` that is weakly-linked against a dependency +# target of type ``<LibType>``. +# +# +# check_dynamic_lookup(<TargetType> +# <LibType> +# <ResultVar> +# <LinkFlagsVar>) +# +# Check if the linker requires a command line flag to allow leaving symbols +# unresolved when producing a target of type ``<TargetType>`` that is +# weakly-linked against a dependency of type ``<LibType>``. ``<TargetType>`` +# can be one of "STATIC", "SHARED", "MODULE", or "EXE". ``<LibType>`` can be +# one of "STATIC", "SHARED", or "MODULE". The result is cached between +# invocations and recomputed only when the value of CMake's linker flag list +# changes; ``CMAKE_STATIC_LINKER_FLAGS`` if ``<TargetType>`` is "STATIC", and +# ``CMAKE_SHARED_LINKER_FLAGS`` otherwise. +# +# +# Defined variables: +# +# ``<ResultVar>`` +# Whether the current C toolchain supports weak-linking for target binaries of +# type ``<TargetType>`` that are weakly-linked against a dependency target of +# type ``<LibType>``. +# +# ``<LinkFlagsVar>`` +# List of flags to add to the linker command to produce a working target +# binary of type ``<TargetType>`` that is weakly-linked against a dependency +# target of type ``<LibType>``. +# +# ``HAS_DYNAMIC_LOOKUP_<TargetType>_<LibType>`` +# Cached, global alias for ``<ResultVar>`` +# +# ``DYNAMIC_LOOKUP_FLAGS_<TargetType>_<LibType>`` +# Cached, global alias for ``<LinkFlagsVar>`` +# +# +# target_link_libraries_with_dynamic_lookup(<Target> [<Libraries>]) +# +# Like proper linking, except that the given ``<Libraries>`` are not necessarily +# linked. Instead, the ``<Target>`` is produced in a manner that allows for +# symbols unresolved within it to be resolved at runtime, presumably by the +# given ``<Libraries>``. If such a target can be produced, the provided +# ``<Libraries>`` are not actually linked. On platforms that do not support +# weak-linking, this function works just like ``target_link_libraries``. + +function(_get_target_type result_var target) + set(target_type "SHARED_LIBRARY") + if(TARGET ${target}) + get_property(target_type TARGET ${target} PROPERTY TYPE) + endif() + + set(result "STATIC") + + if(target_type STREQUAL "STATIC_LIBRARY") + set(result "STATIC") + endif() + + if(target_type STREQUAL "SHARED_LIBRARY") + set(result "SHARED") + endif() + + if(target_type STREQUAL "MODULE_LIBRARY") + set(result "MODULE") + endif() + + if(target_type STREQUAL "EXECUTABLE") + set(result "EXE") + endif() + + set(${result_var} ${result} PARENT_SCOPE) +endfunction() + + +function(_test_weak_link_project + target_type + lib_type + can_weak_link_var + project_name) + + set(gnu_ld_ignore "-Wl,--unresolved-symbols=ignore-all") + set(osx_dynamic_lookup "-undefined dynamic_lookup") + set(no_flag "") + + foreach(link_flag_spec gnu_ld_ignore osx_dynamic_lookup no_flag) + set(link_flag "${${link_flag_spec}}") + + set(test_project_dir "${PROJECT_BINARY_DIR}/CMakeTmp") + set(test_project_dir "${test_project_dir}/${project_name}") + set(test_project_dir "${test_project_dir}/${link_flag_spec}") + set(test_project_dir "${test_project_dir}/${target_type}") + set(test_project_dir "${test_project_dir}/${lib_type}") + + set(test_project_src_dir "${test_project_dir}/src") + set(test_project_bin_dir "${test_project_dir}/build") + + file(MAKE_DIRECTORY ${test_project_src_dir}) + file(MAKE_DIRECTORY ${test_project_bin_dir}) + + set(mod_type "STATIC") + set(link_mod_lib TRUE) + set(link_exe_lib TRUE) + set(link_exe_mod FALSE) + + if("${target_type}" STREQUAL "EXE") + set(link_exe_lib FALSE) + set(link_exe_mod TRUE) + else() + set(mod_type "${target_type}") + endif() + + if("${mod_type}" STREQUAL "MODULE") + set(link_mod_lib FALSE) + endif() + + + file(WRITE "${test_project_src_dir}/CMakeLists.txt" " + cmake_minimum_required(VERSION ${CMAKE_VERSION}) + project(${project_name} C) + + include_directories(${test_project_src_dir}) + + add_library(number ${lib_type} number.c) + add_library(counter ${mod_type} counter.c) + ") + + if("${mod_type}" STREQUAL "MODULE") + file(APPEND "${test_project_src_dir}/CMakeLists.txt" " + set_target_properties(counter PROPERTIES PREFIX \"\") + ") + endif() + + if(link_mod_lib) + file(APPEND "${test_project_src_dir}/CMakeLists.txt" " + target_link_libraries(counter number) + ") + elseif(NOT link_flag STREQUAL "") + file(APPEND "${test_project_src_dir}/CMakeLists.txt" " + set_target_properties(counter PROPERTIES LINK_FLAGS \"${link_flag}\") + ") + endif() + + file(APPEND "${test_project_src_dir}/CMakeLists.txt" " + add_executable(main main.c) + ") + + if(link_exe_lib) + file(APPEND "${test_project_src_dir}/CMakeLists.txt" " + target_link_libraries(main number) + ") + elseif(NOT link_flag STREQUAL "") + file(APPEND "${test_project_src_dir}/CMakeLists.txt" " + target_link_libraries(main \"${link_flag}\") + ") + endif() + + if(link_exe_mod) + file(APPEND "${test_project_src_dir}/CMakeLists.txt" " + target_link_libraries(main counter) + ") + else() + file(APPEND "${test_project_src_dir}/CMakeLists.txt" " + target_link_libraries(main \"${CMAKE_DL_LIBS}\") + ") + endif() + + file(WRITE "${test_project_src_dir}/number.c" " + #include <number.h> + + static int _number; + void set_number(int number) { _number = number; } + int get_number() { return _number; } + ") + + file(WRITE "${test_project_src_dir}/number.h" " + #ifndef _NUMBER_H + #define _NUMBER_H + extern void set_number(int); + extern int get_number(void); + #endif + ") + + file(WRITE "${test_project_src_dir}/counter.c" " + #include <number.h> + int count() { + int result = get_number(); + set_number(result + 1); + return result; + } + ") + + file(WRITE "${test_project_src_dir}/counter.h" " + #ifndef _COUNTER_H + #define _COUNTER_H + extern int count(void); + #endif + ") + + file(WRITE "${test_project_src_dir}/main.c" " + #include <stdlib.h> + #include <stdio.h> + #include <number.h> + ") + + if(NOT link_exe_mod) + file(APPEND "${test_project_src_dir}/main.c" " + #include <dlfcn.h> + ") + endif() + + file(APPEND "${test_project_src_dir}/main.c" " + int my_count() { + int result = get_number(); + set_number(result + 1); + return result; + } + + int main(int argc, char **argv) { + int result; + ") + + if(NOT link_exe_mod) + file(APPEND "${test_project_src_dir}/main.c" " + void *counter_module; + int (*count)(void); + + counter_module = dlopen(\"./counter.so\", RTLD_LAZY | RTLD_GLOBAL); + if(!counter_module) goto error; + + count = dlsym(counter_module, \"count\"); + if(!count) goto error; + ") + endif() + + file(APPEND "${test_project_src_dir}/main.c" " + result = count() != 0 ? EXIT_FAILURE : + my_count() != 1 ? EXIT_FAILURE : + my_count() != 2 ? EXIT_FAILURE : + count() != 3 ? EXIT_FAILURE : + count() != 4 ? EXIT_FAILURE : + count() != 5 ? EXIT_FAILURE : + my_count() != 6 ? EXIT_FAILURE : EXIT_SUCCESS; + ") + + if(NOT link_exe_mod) + file(APPEND "${test_project_src_dir}/main.c" " + goto done; + error: + fprintf(stderr, \"Error occured:\\n %s\\n\", dlerror()); + result = 1; + + done: + if(counter_module) dlclose(counter_module); + ") + endif() + + file(APPEND "${test_project_src_dir}/main.c" " + return result; + } + ") + + set(_rpath_arg) + if(APPLE AND ${CMAKE_VERSION} VERSION_GREATER 2.8.11) + set(_rpath_arg "-DCMAKE_MACOSX_RPATH='${CMAKE_MACOSX_RPATH}'") + endif() + + try_compile(project_compiles + "${test_project_bin_dir}" + "${test_project_src_dir}" + "${project_name}" + CMAKE_FLAGS + "-DCMAKE_SHARED_LINKER_FLAGS='${CMAKE_SHARED_LINKER_FLAGS}'" + ${_rpath_arg} + OUTPUT_VARIABLE compile_output) + + set(project_works 1) + set(run_output) + + if(project_compiles) + execute_process(COMMAND ${CMAKE_CROSSCOMPILING_EMULATOR} + "${test_project_bin_dir}/main" + WORKING_DIRECTORY "${test_project_bin_dir}" + RESULT_VARIABLE project_works + OUTPUT_VARIABLE run_output + ERROR_VARIABLE run_output) + endif() + + set(test_description + "Weak Link ${target_type} -> ${lib_type} (${link_flag_spec})") + + if(project_works EQUAL 0) + set(project_works TRUE) + message(STATUS "Performing Test ${test_description} - Success") + else() + set(project_works FALSE) + message(STATUS "Performing Test ${test_description} - Failed") + file(APPEND ${CMAKE_BINARY_DIR}/${CMAKE_FILES_DIRECTORY}/CMakeError.log + "Performing Test ${test_description} failed with the " + "following output:\n" + "BUILD\n-----\n${compile_output}\nRUN\n---\n${run_output}\n") + endif() + + set(${can_weak_link_var} ${project_works} PARENT_SCOPE) + if(project_works) + set(${project_name} ${link_flag} PARENT_SCOPE) + break() + endif() + endforeach() +endfunction() + + +function(check_dynamic_lookup + target_type + lib_type + has_dynamic_lookup_var + link_flags_var) + + # hash the CMAKE_FLAGS passed and check cache to know if we need to rerun + if("${target_type}" STREQUAL "STATIC") + string(MD5 cmake_flags_hash "${CMAKE_STATIC_LINKER_FLAGS}") + else() + string(MD5 cmake_flags_hash "${CMAKE_SHARED_LINKER_FLAGS}") + endif() + + set(cache_var "HAS_DYNAMIC_LOOKUP_${target_type}_${lib_type}") + set(cache_hash_var "HAS_DYNAMIC_LOOKUP_${target_type}_${lib_type}_hash") + set(result_var "DYNAMIC_LOOKUP_FLAGS_${target_type}_${lib_type}") + + if( NOT DEFINED ${cache_hash_var} + OR NOT "${${cache_hash_var}}" STREQUAL "${cmake_flags_hash}") + unset(${cache_var} CACHE) + endif() + + if(NOT DEFINED ${cache_var}) + set(skip_test FALSE) + + if(NOT CMAKE_CROSSCOMPILING) + set(skip_test TRUE) + elseif(CMAKE_CROSSCOMPILING AND CMAKE_CROSSCOMPILING_EMULATOR) + set(skip_test TRUE) + endif() + + if(skip_test) + set(has_dynamic_lookup FALSE) + set(link_flags) + else() + _test_weak_link_project(${target_type} + ${lib_type} + has_dynamic_lookup + link_flags) + endif() + + set(caveat " (when linking ${target_type} against ${lib_type})") + + set(${cache_var} "${has_dynamic_lookup}" + CACHE BOOL + "linker supports dynamic lookup for undefined symbols${caveat}") + + set(${result_var} "${link_flags}" + CACHE BOOL + "linker flags for dynamic lookup${caveat}") + + set(${cache_hash_var} "${cmake_flags_hash}" + CACHE INTERNAL "hashed flags for ${cache_var} check") + endif() + + set(${has_dynamic_lookup_var} "${${cache_var}}" PARENT_SCOPE) + set(${link_flags_var} "${${result_var}}" PARENT_SCOPE) +endfunction() + + +function(target_link_libraries_with_dynamic_lookup target) + _get_target_type(target_type ${target}) + + set(link_props) + set(link_items) + set(link_libs) + + foreach(lib ${ARGN}) + _get_target_type(lib_type ${lib}) + check_dynamic_lookup(${target_type} + ${lib_type} + has_dynamic_lookup + dynamic_lookup_flags) + + if(has_dynamic_lookup) + if(dynamic_lookup_flags) + if("${target_type}" STREQUAL "EXE") + list(APPEND link_items "${dynamic_lookup_flags}") + else() + list(APPEND link_props "${dynamic_lookup_flags}") + endif() + endif() + else() + list(APPEND link_libs "${lib}") + endif() + endforeach() + + if(link_props) + list(REMOVE_DUPLICATES link_props) + endif() + + if(link_items) + list(REMOVE_DUPLICATES link_items) + endif() + + if(link_libs) + list(REMOVE_DUPLICATES link_libs) + endif() + + if(link_props) + set_target_properties(${target} + PROPERTIES LINK_FLAGS "${link_props}") + endif() + + set(links "${link_items}" "${link_libs}") + if(links) + target_link_libraries(${target} "${links}") + endif() +endfunction() + diff --git a/configure.sh b/configure.sh index 5763fa7ce..611ac54ad 100755 --- a/configure.sh +++ b/configure.sh @@ -44,6 +44,7 @@ The following flags enable optional features (disable with --no-<option name>). --unit-testing support for unit testing --python2 prefer using Python 2 (also for Python bindings) --python3 prefer using Python 3 (also for Python bindings) + --python-bindings build Python bindings based on new C++ API --asan build with ASan instrumentation --ubsan build with UBSan instrumentation --tsan build with TSan instrumentation @@ -141,6 +142,7 @@ tracing=default unit_testing=default python2=default python3=default +python_bindings=default valgrind=default profiling=default readline=default @@ -279,6 +281,9 @@ do --python3) python3=ON;; --no-python3) python3=OFF;; + --python-bindings) python_bindings=ON;; + --no-python-bindings) python_bindings=OFF;; + --valgrind) valgrind=ON;; --no-valgrind) valgrind=OFF;; @@ -404,6 +409,8 @@ cmake_opts="" && cmake_opts="$cmake_opts -DUSE_PYTHON2=$python2" [ $python3 != default ] \ && cmake_opts="$cmake_opts -DUSE_PYTHON3=$python3" +[ $python_bindings != default ] \ + && cmake_opts="$cmake_opts -DBUILD_BINDINGS_PYTHON=$python_bindings" [ $valgrind != default ] \ && cmake_opts="$cmake_opts -DENABLE_VALGRIND=$valgrind" [ $profiling != default ] \ @@ -428,9 +435,9 @@ cmake_opts="" && cmake_opts="$cmake_opts -DUSE_SYMFPU=$symfpu" [ $language_bindings_java != default ] \ - && cmake_opts="$cmake_opts -DBUILD_BINDINGS_JAVA=$language_bindings_java" + && cmake_opts="$cmake_opts -DBUILD_SWIG_BINDINGS_JAVA=$language_bindings_java" [ $language_bindings_python != default ] \ - && cmake_opts="$cmake_opts -DBUILD_BINDINGS_PYTHON=$language_bindings_python" + && cmake_opts="$cmake_opts -DBUILD_SWIG_BINDINGS_PYTHON=$language_bindings_python" [ "$abc_dir" != default ] \ && cmake_opts="$cmake_opts -DABC_DIR=$abc_dir" diff --git a/examples/api/python/bitvectors.py b/examples/api/python/bitvectors.py new file mode 100755 index 000000000..773974cc7 --- /dev/null +++ b/examples/api/python/bitvectors.py @@ -0,0 +1,121 @@ +#!/usr/bin/env python + +##################### +#! \file bitvectors.py + ## \verbatim + ## Top contributors (to current version): + ## Makai Mann + ## This file is part of the CVC4 project. + ## Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ## in the top-level source directory) and their institutional affiliations. + ## All rights reserved. See the file COPYING in the top-level source + ## directory for licensing information.\endverbatim + ## + ## \brief A simple demonstration of the solving capabilities of the CVC4 + ## bit-vector solver through the Python API. This is a direct translation + ## of bitvectors-new.cpp. +import pycvc4 +from pycvc4 import kinds + +if __name__ == "__main__": + slv = pycvc4.Solver() + slv.setLogic("QF_BV") # Set the logic + # The following example has been adapted from the book A Hacker's Delight by + # Henry S. Warren. + # + # Given a variable x that can only have two values, a or b. We want to + # assign to x a value other than the current one. The straightforward code + # to do that is: + # + #(0) if (x == a ) x = b; + # else x = a; + # + # Two more efficient yet equivalent methods are: + # + #(1) x = a xor b xor x; + # + #(2) x = a + b - x; + # + # We will use CVC4 to prove that the three pieces of code above are all + # equivalent by encoding the problem in the bit-vector theory. + + # Creating a bit-vector type of width 32 + bitvector32 = slv.mkBitVectorSort(32) + + # Variables + x = slv.mkConst(bitvector32, "x") + a = slv.mkConst(bitvector32, "a") + b = slv.mkConst(bitvector32, "b") + + # First encode the assumption that x must be equal to a or b + x_eq_a = slv.mkTerm(kinds.Equal, x, a) + x_eq_b = slv.mkTerm(kinds.Equal, x, b) + assumption = slv.mkTerm(kinds.Or, x_eq_a, x_eq_b) + + # Assert the assumption + slv.assertFormula(assumption) + + # Introduce a new variable for the new value of x after assignment. + # x after executing code (0) + new_x = slv.mkConst(bitvector32, "new_x") + # x after executing code (1) or (2) + new_x_ = slv.mkConst(bitvector32, "new_x_") + + # Encoding code (0) + # new_x = x == a ? b : a + ite = slv.mkTerm(kinds.Ite, x_eq_a, b, a) + assignment0 = slv.mkTerm(kinds.Equal, new_x, ite) + + # Assert the encoding of code (0) + print("Asserting {} to CVC4".format(assignment0)) + slv.assertFormula(assignment0) + print("Pushing a new context.") + slv.push() + + # Encoding code (1) + # new_x_ = a xor b xor x + a_xor_b_xor_x = slv.mkTerm(kinds.BVXor, a, b, x) + assignment1 = slv.mkTerm(kinds.Equal, new_x_, a_xor_b_xor_x) + + # Assert encoding to CVC4 in current context + print("Asserting {} to CVC4".format(assignment1)) + slv.assertFormula(assignment1) + new_x_eq_new_x_ = slv.mkTerm(kinds.Equal, new_x, new_x_) + + print("Checking validity assuming:", new_x_eq_new_x_) + print("Expect valid.") + print("CVC4:", slv.checkValidAssuming(new_x_eq_new_x_)) + print("Popping context.") + slv.pop() + + # Encoding code (2) + # new_x_ = a + b - x + a_plus_b = slv.mkTerm(kinds.BVPlus, a, b) + a_plus_b_minus_x = slv.mkTerm(kinds.BVSub, a_plus_b, x) + assignment2 = slv.mkTerm(kinds.Equal, new_x_, a_plus_b_minus_x) + + # Assert encoding to CVC4 in current context + print("Asserting {} to CVC4".format(assignment2)) + slv.assertFormula(assignment2) + + print("Checking validity assuming:", new_x_eq_new_x_) + print("Expect valid.") + print("CVC4:", slv.checkValidAssuming(new_x_eq_new_x_)) + + + x_neq_x = slv.mkTerm(kinds.Equal, x, x).notTerm() + v = [new_x_eq_new_x_, x_neq_x] + print("Check Validity Assuming: ", v) + print("Expect invalid.") + print("CVC4:", slv.checkValidAssuming(v)) + + # Assert that a is odd + extract_op = slv.mkOp(kinds.BVExtract, 0, 0) + lsb_of_a = slv.mkTerm(extract_op, a) + print("Sort of {} is {}".format(lsb_of_a, lsb_of_a.getSort())) + a_odd = slv.mkTerm(kinds.Equal, lsb_of_a, slv.mkBitVector(1, 1)) + print("Assert", a_odd) + print("Check satisifiability") + slv.assertFormula(a_odd) + print("Expect sat") + print("CVC4:", slv.checkSat()) diff --git a/examples/api/python/bitvectors_and_arrays.py b/examples/api/python/bitvectors_and_arrays.py new file mode 100755 index 000000000..7e3d8f478 --- /dev/null +++ b/examples/api/python/bitvectors_and_arrays.py @@ -0,0 +1,91 @@ +#!/usr/bin/env python + +##################### +#! \file bitvectors_and_arrays.py + ## \verbatim + ## Top contributors (to current version): + ## Makai Mann + ## This file is part of the CVC4 project. + ## Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ## in the top-level source directory) and their institutional affiliations. + ## All rights reserved. See the file COPYING in the top-level source + ## directory for licensing information.\endverbatim + ## + ## \brief A simple demonstration of the solving capabilities of the CVC4 + ## bit-vector and array solvers through the Python API. This is a direct + ## translation of bitvectors_and_arrays-new.cpp. +import pycvc4 +from pycvc4 import kinds + +import math + +if __name__ == "__main__": + slv = pycvc4.Solver() + slv.setOption("produce-models", "true") + slv.setOption("output-language", "smtlib") + slv.setLogic("QF_AUFBV") + + # Consider the following code (where size is some previously defined constant): + # + # + # Assert (current_array[0] > 0); + # for (unsigned i = 1; i < k; ++i) { + # current_array[i] = 2 * current_array[i - 1]; + # Assert (current_array[i-1] < current_array[i]); + # } + # + # We want to check whether the assertion in the body of the for loop holds + # throughout the loop. + + # Setting up the problem parameters + k = 4 + index_size = int(math.ceil(math.log(k, 2))) + + # Sorts + elementSort = slv.mkBitVectorSort(32) + indexSort = slv.mkBitVectorSort(index_size) + arraySort = slv.mkArraySort(indexSort, elementSort) + + # Variables + current_array = slv.mkConst(arraySort, "current_array") + + # Making a bit-vector constant + zero = slv.mkBitVector(index_size, 0) + + # Test making a constant array + constarr0 = slv.mkConstArray(arraySort, slv.mkBitVector(32, 0)) + + # Asserting that current_array[0] > 0 + current_array0 = slv.mkTerm(kinds.Select, current_array, zero) + current_array0_gt_0 = slv.mkTerm(kinds.BVSgt, + current_array0, + slv.mkBitVector(32, 0)) + slv.assertFormula(current_array0_gt_0) + + # Building the assertions in the loop unrolling + index = slv.mkBitVector(index_size, 0) + old_current = slv.mkTerm(kinds.Select, current_array, index) + two = slv.mkBitVector(32, 2) + + assertions = [] + for i in range(1, k): + index = slv.mkBitVector(index_size, i) + new_current = slv.mkTerm(kinds.BVMult, two, old_current) + # current[i] = 2*current[i-1] + current_array = slv.mkTerm(kinds.Store, current_array, index, new_current) + # current[i-1] < current[i] + current_slt_new_current = slv.mkTerm(kinds.BVSlt, old_current, new_current) + assertions.append(current_slt_new_current) + old_current = slv.mkTerm(kinds.Select, current_array, index) + + query = slv.mkTerm(kinds.Not, slv.mkTerm(kinds.And, assertions)) + + print("Asserting {} to CVC4".format(query)) + slv.assertFormula(query) + print("Expect sat.") + print("CVC4:", slv.checkSatAssuming(slv.mkTrue())) + + # Getting the model + print("The satisfying model is: ") + print(" current_array =", slv.getValue(current_array)) + print(" current_array[0]", slv.getValue(current_array0)) diff --git a/examples/api/python/combination.py b/examples/api/python/combination.py new file mode 100755 index 000000000..1b488d7d5 --- /dev/null +++ b/examples/api/python/combination.py @@ -0,0 +1,99 @@ +#!/usr/bin/env python + +##################### +#! \file combination.py + ## \verbatim + ## Top contributors (to current version): + ## Makai Mann + ## This file is part of the CVC4 project. + ## Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ## in the top-level source directory) and their institutional affiliations. + ## All rights reserved. See the file COPYING in the top-level source + ## directory for licensing information.\endverbatim + ## + ## \brief A simple demonstration of the solving capabilities of the CVC4 + ## combination solver through the Python API. This is a direct translation + ## of combination-new.cpp. +import pycvc4 +from pycvc4 import kinds + +def prefixPrintGetValue(slv, t, level=0): + print("slv.getValue({}): {}".format(t, slv.getValue(t))) + for c in t: + prefixPrintGetValue(slv, c, level + 1) + +if __name__ == "__main__": + slv = pycvc4.Solver() + slv.setOption("produce-models", "true") # Produce Models + slv.setOption("output-language", "cvc4") # Set the output-language to CVC's + slv.setOption("default-dag-thresh", "0") # Disable dagifying the output + slv.setOption("output-language", "smt2") # use smt-lib v2 as output language + slv.setLogic("QF_UFLIRA") + + # Sorts + u = slv.mkUninterpretedSort("u") + integer = slv.getIntegerSort() + boolean = slv.getBooleanSort() + uToInt = slv.mkFunctionSort(u, integer) + intPred = slv.mkFunctionSort(integer, boolean) + + # Variables + x = slv.mkConst(u, "x") + y = slv.mkConst(u, "y") + + # Functions + f = slv.mkConst(uToInt, "f") + p = slv.mkConst(intPred, "p") + + # Constants + zero = slv.mkReal(0) + one = slv.mkReal(1) + + # Terms + f_x = slv.mkTerm(kinds.ApplyUf, f, x) + f_y = slv.mkTerm(kinds.ApplyUf, f, y) + sum_ = slv.mkTerm(kinds.Plus, f_x, f_y) + p_0 = slv.mkTerm(kinds.ApplyUf, p, zero) + p_f_y = slv.mkTerm(kinds.ApplyUf, p, f_y) + + # Construct the assertions + assertions = slv.mkTerm(kinds.And, + [ + slv.mkTerm(kinds.Leq, zero, f_x), # 0 <= f(x) + slv.mkTerm(kinds.Leq, zero, f_y), # 0 <= f(y) + slv.mkTerm(kinds.Leq, sum_, one), # f(x) + f(y) <= 1 + p_0.notTerm(), # not p(0) + p_f_y # p(f(y)) + ]) + + slv.assertFormula(assertions) + + print("Given the following assertions:", assertions, "\n") + print("Prove x /= y is valid.\nCVC4: ", + slv.checkValidAssuming(slv.mkTerm(kinds.Distinct, x, y)), "\n") + + print("Call checkSat to show that the assertions are satisfiable") + print("CVC4:", slv.checkSat(), "\n") + + print("Call slv.getValue(...) on terms of interest") + print("slv.getValue({}): {}".format(f_x, slv.getValue(f_x))) + print("slv.getValue({}): {}".format(f_y, slv.getValue(f_y))) + print("slv.getValue({}): {}".format(sum_, slv.getValue(sum_))) + print("slv.getValue({}): {}".format(p_0, slv.getValue(p_0))) + print("slv.getValue({}): {}".format(p_f_y, slv.getValue(p_f_y)), "\n") + + print("Alternatively, iterate over assertions and call" + " slv.getValue(...) on all terms") + prefixPrintGetValue(slv, assertions) + + print("Alternatively, print the model", "\n") + slv.printModel() + + print() + print("You can also use nested loops to iterate over terms") + for a in assertions: + print("term:", a) + for t in a: + print(" + child: ", t) + + print() diff --git a/examples/api/python/datatypes.py b/examples/api/python/datatypes.py new file mode 100755 index 000000000..c5eda1741 --- /dev/null +++ b/examples/api/python/datatypes.py @@ -0,0 +1,137 @@ +#!/usr/bin/env python + +##################### +#! \file datatypes.py + ## \verbatim + ## Top contributors (to current version): + ## Makai Mann + ## This file is part of the CVC4 project. + ## Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ## in the top-level source directory) and their institutional affiliations. + ## All rights reserved. See the file COPYING in the top-level source + ## directory for licensing information.\endverbatim + ## + ## \brief A simple demonstration of the solving capabilities of the CVC4 + ## datatypes solver through the Python API. This is a direct translation + ## of datatypes-new.cpp. + +import pycvc4 +from pycvc4 import kinds + +def test(slv, consListSort): + # Now our old "consListSpec" is useless--the relevant information + # has been copied out, so we can throw that spec away. We can get + # the complete spec for the datatype from the DatatypeSort, and + # this Datatype object has constructor symbols (and others) filled in. + + consList = consListSort.getDatatype() + + # t = cons 0 nil + # + # Here, consList["cons"] gives you the DatatypeConstructor. To get + # the constructor symbol for application, use .getConstructor("cons"), + # which is equivalent to consList["cons"].getConstructor(). Note that + # "nil" is a constructor too + + t = slv.mkTerm(kinds.ApplyConstructor, consList.getConstructorTerm("cons"), + slv.mkReal(0), + slv.mkTerm(kinds.ApplyConstructor, consList.getConstructorTerm("nil"))) + + print("t is {}\nsort of cons is {}\n sort of nil is {}".format( + t, + consList.getConstructorTerm("cons").getSort(), + consList.getConstructorTerm("nil").getSort())) + + # t2 = head(cons 0 nil), and of course this can be evaluated + # + # Here we first get the DatatypeConstructor for cons (with + # consList["cons"]) in order to get the "head" selector symbol + # to apply. + + t2 = slv.mkTerm(kinds.ApplySelector, consList["cons"].getSelectorTerm("head"), t) + + print("t2 is {}\nsimplify(t2) is {}\n\n".format(t2, slv.simplify(t2))) + + # You can also iterate over a Datatype to get all its constructors, + # and over a DatatypeConstructor to get all its "args" (selectors) + for i in consList: + print("ctor:", i) + for j in i: + print(" + args:", j) + print() + + # You can also define parameterized datatypes. + # This example builds a simple parameterized list of sort T, with one + # constructor "cons". + sort = slv.mkParamSort("T") + paramConsListSpec = slv.mkDatatypeDecl("paramlist", sort) + paramCons = pycvc4.DatatypeConstructorDecl("cons") + paramNil = pycvc4.DatatypeConstructorDecl("nil") + paramHead = pycvc4.DatatypeSelectorDecl("head", sort) + paramTail = pycvc4.DatatypeSelectorDecl("tail", pycvc4.DatatypeDeclSelfSort()) + paramCons.addSelector(paramHead) + paramCons.addSelector(paramTail) + paramConsListSpec.addConstructor(paramCons) + paramConsListSpec.addConstructor(paramNil) + + paramConsListSort = slv.mkDatatypeSort(paramConsListSpec) + paramConsIntListSort = paramConsListSort.instantiate([slv.getIntegerSort()]) + paramConsList = paramConsListSort.getDatatype() + + a = slv.mkConst(paramConsIntListSort, "a") + print("term {} is of sort {}".format(a, a.getSort())) + + head_a = slv.mkTerm(kinds.ApplySelector, paramConsList["cons"].getSelectorTerm("head"), a) + print("head_a is {} of sort {}".format(head_a, head_a.getSort())) + print("sort of cons is", paramConsList.getConstructorTerm("cons").getSort()) + + assertion = slv.mkTerm(kinds.Gt, head_a, slv.mkReal(50)) + print("Assert", assertion) + slv.assertFormula(assertion) + print("Expect sat.") + print("CVC4:", slv.checkSat()) + + +if __name__ == "__main__": + slv = pycvc4.Solver() + + # This example builds a simple "cons list" of integers, with + # two constructors, "cons" and "nil." + + # Building a datatype consists of two steps. + # First, the datatype is specified. + # Second, it is "resolved" to an actual sort, at which point function + # symbols are assigned to its constructors, selectors, and testers. + + consListSpec = slv.mkDatatypeDecl("list") # give the datatype a name + cons = pycvc4.DatatypeConstructorDecl("cons") + head = pycvc4.DatatypeSelectorDecl("head", slv.getIntegerSort()) + tail = pycvc4.DatatypeSelectorDecl("tail", pycvc4.DatatypeDeclSelfSort()) + cons.addSelector(head) + cons.addSelector(tail) + consListSpec.addConstructor(cons) + nil = pycvc4.DatatypeConstructorDecl("nil") + consListSpec.addConstructor(nil) + + print("spec is {}".format(consListSpec)) + + # Keep in mind that "DatatypeDecl" is the specification class for + # datatypes---"DatatypeDecl" is not itself a CVC4 Sort. + # Now that our Datatype is fully specified, we can get a Sort for it. + # This step resolves the "SelfSort" reference and creates + # symbols for all the constructors, etc. + + consListSort = slv.mkDatatypeSort(consListSpec) + test(slv, consListSort) + + print("### Alternatively, use declareDatatype") + + cons2 = pycvc4.DatatypeConstructorDecl("cons") + head2 = pycvc4.DatatypeSelectorDecl("head", slv.getIntegerSort()) + tail2 = pycvc4.DatatypeSelectorDecl("tail", pycvc4.DatatypeDeclSelfSort()) + cons2.addSelector(head2) + cons2.addSelector(tail2) + nil2 = pycvc4.DatatypeConstructorDecl("nil") + ctors = [cons2, nil2] + consListSort2 = slv.declareDatatype("list2", ctors) + test(slv, consListSort2) diff --git a/examples/api/python/extract.py b/examples/api/python/extract.py new file mode 100755 index 000000000..1bfdf652a --- /dev/null +++ b/examples/api/python/extract.py @@ -0,0 +1,51 @@ +#!/usr/bin/env python + +##################### +#! \file extract.py + ## \verbatim + ## Top contributors (to current version): + ## Makai Mann + ## This file is part of the CVC4 project. + ## Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ## in the top-level source directory) and their institutional affiliations. + ## All rights reserved. See the file COPYING in the top-level source + ## directory for licensing information.\endverbatim + ## + ## \brief A simple demonstration of the solving capabilities of the CVC4 + ## bit-vector solver through the Python API. This is a direct translation + ## of extract-new.cpp. + +from pycvc4 import Solver +from pycvc4.kinds import BVExtract, Equal + +if __name__ == "__main__": + slv = Solver() + slv.setLogic("QF_BV") + + bitvector32 = slv.mkBitVectorSort(32) + + x = slv.mkConst(bitvector32, "a") + + ext_31_1 = slv.mkOp(BVExtract, 31, 1) + x_31_1 = slv.mkTerm(ext_31_1, x) + + ext_30_0 = slv.mkOp(BVExtract, 30, 0) + x_30_0 = slv.mkTerm(ext_30_0, x) + + ext_31_31 = slv.mkOp(BVExtract, 31, 31) + x_31_31 = slv.mkTerm(ext_31_31, x) + + ext_0_0 = slv.mkOp(BVExtract, 0, 0) + x_0_0 = slv.mkTerm(ext_0_0, x) + + # test getting indices + assert ext_30_0.getIndices() == (30, 0) + + eq = slv.mkTerm(Equal, x_31_1, x_30_0) + print("Asserting:", eq) + slv.assertFormula(eq) + + eq2 = slv.mkTerm(Equal, x_31_31, x_0_0) + print("Check validity assuming:", eq2) + print("Expect valid") + print("CVC4:", slv.checkValidAssuming(eq2)) diff --git a/examples/api/python/helloworld.py b/examples/api/python/helloworld.py new file mode 100755 index 000000000..472cf945b --- /dev/null +++ b/examples/api/python/helloworld.py @@ -0,0 +1,21 @@ +#!/usr/bin/env python + +##################### +#! \file helloworld.py +## \verbatim +## Top contributors (to current version): +## Makai Mann +## This file is part of the CVC4 project. +## Copyright (c) 2009-2018 by the authors listed in the file AUTHORS +## in the top-level source directory) and their institutional affiliations. +## All rights reserved. See the file COPYING in the top-level source +## directory for licensing information.\endverbatim +## +## \brief A very simple CVC4 tutorial example, adapted from helloworld-new.cpp +import pycvc4 +from pycvc4 import kinds + +if __name__ == "__main__": + slv = pycvc4.Solver() + helloworld = slv.mkConst(slv.getBooleanSort(), "Hello World!") + print(helloworld, "is", slv.checkValidAssuming(helloworld)) diff --git a/examples/api/python/linear_arith.py b/examples/api/python/linear_arith.py new file mode 100755 index 000000000..6ae6427b1 --- /dev/null +++ b/examples/api/python/linear_arith.py @@ -0,0 +1,70 @@ +#!/usr/bin/env python + +##################### +#! \file linear_arith.py +## \verbatim +## Top contributors (to current version): +## Makai Mann +## This file is part of the CVC4 project. +## Copyright (c) 2009-2018 by the authors listed in the file AUTHORS +## in the top-level source directory) and their institutional affiliations. +## All rights reserved. See the file COPYING in the top-level source +## directory for licensing information.\endverbatim +## +## \brief A simple demonstration of the solving capabilities of the CVC4 +## linear arithmetic solver through the Python API. This is a direct +## translation of linear_arith-new.cpp. +import pycvc4 +from pycvc4 import kinds + +if __name__ == "__main__": + slv = pycvc4.Solver() + slv.setLogic("QF_LIRA") + + # Prove that if given x (Integer) and y (Real) and some constraints + # then the maximum value of y - x is 2/3 + + # Sorts + real = slv.getRealSort() + integer = slv.getIntegerSort() + + # Variables + x = slv.mkConst(integer, "x") + y = slv.mkConst(real, "y") + + # Constants + three = slv.mkReal(3) + neg2 = slv.mkReal(-2) + two_thirds = slv.mkReal(2, 3) + + # Terms + three_y = slv.mkTerm(kinds.Mult, three, y) + diff = slv.mkTerm(kinds.Minus, y, x) + + # Formulas + x_geq_3y = slv.mkTerm(kinds.Geq, x, three_y) + x_leq_y = slv.mkTerm(kinds.Leq, x ,y) + neg2_lt_x = slv.mkTerm(kinds.Lt, neg2, x) + + assertions = slv.mkTerm(kinds.And, x_geq_3y, x_leq_y, neg2_lt_x) + + print("Given the assertions", assertions) + slv.assertFormula(assertions) + + slv.push() + diff_leq_two_thirds = slv.mkTerm(kinds.Leq, diff, two_thirds) + print("Prove that", diff_leq_two_thirds, "with CVC4") + print("CVC4 should report VALID") + print("Result from CVC4 is:", + slv.checkValidAssuming(diff_leq_two_thirds)) + slv.pop() + + print() + + slv.push() + diff_is_two_thirds = slv.mkTerm(kinds.Equal, diff, two_thirds) + slv.assertFormula(diff_is_two_thirds) + print("Show that the assertions are consistent with\n", diff_is_two_thirds, "with CVC4") + print("CVC4 should report SAT") + print("Result from CVC4 is:", slv.checkSat()) + slv.pop() diff --git a/examples/api/python/sets.py b/examples/api/python/sets.py new file mode 100755 index 000000000..584880b2b --- /dev/null +++ b/examples/api/python/sets.py @@ -0,0 +1,85 @@ +#!/usr/bin/env python + +##################### +#! \file sets.py +## \verbatim +## Top contributors (to current version): +## Makai Mann +## This file is part of the CVC4 project. +## Copyright (c) 2009-2018 by the authors listed in the file AUTHORS +## in the top-level source directory) and their institutional affiliations. +## All rights reserved. See the file COPYING in the top-level source +## directory for licensing information.\endverbatim +## +## \brief A simple demonstration of the solving capabilities of the CVC4 +## sets solver through the Python API. This is a direct translation +## of sets-new.cpp. +import pycvc4 +from pycvc4 import kinds + +if __name__ == "__main__": + slv = pycvc4.Solver() + + # Optionally, set the logic. We need at least UF for equality predicate, + # integers (LIA) and sets (FS). + slv.setLogic("QF_UFLIAFS") + + # Produce models + slv.setOption("produce-models", "true") + slv.setOption("output-language", "smt2") + + integer = slv.getIntegerSort() + set_ = slv.mkSetSort(integer) + + # Verify union distributions over intersection + # (A union B) intersection C = (A intersection C) union (B intersection C) + + A = slv.mkConst(set_, "A") + B = slv.mkConst(set_, "B") + C = slv.mkConst(set_, "C") + + unionAB = slv.mkTerm(kinds.Union, A, B) + lhs = slv.mkTerm(kinds.Intersection, unionAB, C) + + intersectionAC = slv.mkTerm(kinds.Intersection, A, C) + intersectionBC = slv.mkTerm(kinds.Intersection, B, C) + rhs = slv.mkTerm(kinds.Union, intersectionAC, intersectionBC) + + theorem = slv.mkTerm(kinds.Equal, lhs, rhs) + + print("CVC4 reports: {} is {}".format(theorem, + slv.checkValidAssuming(theorem))) + + # Verify emptset is a subset of any set + + A = slv.mkConst(set_, "A") + emptyset = slv.mkEmptySet(set_) + + theorem = slv.mkTerm(kinds.Subset, emptyset, A) + + print("CVC4 reports: {} is {}".format(theorem, + slv.checkValidAssuming(theorem))) + + # Find me an element in 1, 2 intersection 2, 3, if there is one. + + one = slv.mkReal(1) + two = slv.mkReal(2) + three = slv.mkReal(3) + + singleton_one = slv.mkTerm(kinds.Singleton, one) + singleton_two = slv.mkTerm(kinds.Singleton, two) + singleton_three = slv.mkTerm(kinds.Singleton, three) + one_two = slv.mkTerm(kinds.Union, singleton_one, singleton_two) + two_three = slv.mkTerm(kinds.Union, singleton_two, singleton_three) + intersection = slv.mkTerm(kinds.Intersection, one_two, two_three) + + x = slv.mkConst(integer, "x") + + e = slv.mkTerm(kinds.Member, x, intersection) + + result = slv.checkSatAssuming(e) + + print("CVC4 reports: {} is {}".format(e, result)) + + if result: + print("For instance, {} is a member".format(slv.getValue(x))) diff --git a/examples/api/python/strings.py b/examples/api/python/strings.py new file mode 100755 index 000000000..5c8e91997 --- /dev/null +++ b/examples/api/python/strings.py @@ -0,0 +1,87 @@ +#!/usr/bin/env python + +##################### +#! \file strings.py +## \verbatim +## Top contributors (to current version): +## Makai Mann +## This file is part of the CVC4 project. +## Copyright (c) 2009-2018 by the authors listed in the file AUTHORS +## in the top-level source directory) and their institutional affiliations. +## All rights reserved. See the file COPYING in the top-level source +## directory for licensing information.\endverbatim +## +## \brief A simple demonstration of the solving capabilities of the CVC4 +## strings solver through the Python API. This is a direct translation +## of strings-new.cpp. +import pycvc4 +from pycvc4 import kinds + +if __name__ == "__main__": + slv = pycvc4.Solver() + # Set the logic + slv.setLogic("S") + # Produce models + slv.setOption("produce-models", "true") + # The option strings-exp is needed + slv.setOption("strings-exp", "true") + # Set output language to SMTLIB2 + slv.setOption("output-language", "smt2") + + # String type + string = slv.getStringSort() + + # std::string + str_ab = "ab" + # String constants + ab = slv.mkString(str_ab) + abc = slv.mkString("abc") + # String variables + x = slv.mkConst(string, "x") + y = slv.mkConst(string, "y") + z = slv.mkConst(string, "z") + + # String concatenation: x.ab.y + lhs = slv.mkTerm(kinds.StringConcat, x, ab, y) + # String concatenation: abc.z + rhs = slv.mkTerm(kinds.StringConcat, abc, z) + # x.ab.y = abc.z + formula1 = slv.mkTerm(kinds.Equal, lhs, rhs) + + # Length of y: |y| + leny = slv.mkTerm(kinds.StringLength, y) + # |y| >= 0 + formula2 = slv.mkTerm(kinds.Geq, leny, slv.mkReal(0)) + + # Regular expression: (ab[c-e]*f)|g|h + r = slv.mkTerm(kinds.RegexpUnion, + slv.mkTerm(kinds.RegexpConcat, + slv.mkTerm(kinds.StringToRegexp, slv.mkString("ab")), + slv.mkTerm(kinds.RegexpStar, + slv.mkTerm(kinds.RegexpRange, slv.mkString("c"), slv.mkString("e"))), + slv.mkTerm(kinds.StringToRegexp, slv.mkString("f"))), + slv.mkTerm(kinds.StringToRegexp, slv.mkString("g")), + slv.mkTerm(kinds.StringToRegexp, slv.mkString("h"))) + + # String variables + s1 = slv.mkConst(string, "s1") + s2 = slv.mkConst(string, "s2") + # String concatenation: s1.s2 + s = slv.mkTerm(kinds.StringConcat, s1, s2) + + # s1.s2 in (ab[c-e]*f)|g|h + formula3 = slv.mkTerm(kinds.StringInRegexp, s, r) + + # Make a query + q = slv.mkTerm(kinds.And, + formula1, + formula2, + formula3) + + # check sat + result = slv.checkSatAssuming(q) + print("CVC4 reports:", q, "is", result) + + if result: + print("x = ", slv.getValue(x)) + print(" s1.s2 =", slv.getValue(s)) diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index f4ca1147f..7bdc5008b 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -1755,27 +1755,40 @@ DatatypeDecl::DatatypeDecl(const Solver* s, new CVC4::Datatype(s->getExprManager(), name, tparams, isCoDatatype)); } +bool DatatypeDecl::isNullHelper() const { return !d_dtype; } + +DatatypeDecl::DatatypeDecl() {} + DatatypeDecl::~DatatypeDecl() {} void DatatypeDecl::addConstructor(const DatatypeConstructorDecl& ctor) { + CVC4_API_CHECK_NOT_NULL; d_dtype->addConstructor(*ctor.d_ctor); } size_t DatatypeDecl::getNumConstructors() const { + CVC4_API_CHECK_NOT_NULL; return d_dtype->getNumConstructors(); } -bool DatatypeDecl::isParametric() const { return d_dtype->isParametric(); } +bool DatatypeDecl::isParametric() const +{ + CVC4_API_CHECK_NOT_NULL; + return d_dtype->isParametric(); +} std::string DatatypeDecl::toString() const { + CVC4_API_CHECK_NOT_NULL; std::stringstream ss; ss << *d_dtype; return ss.str(); } +bool DatatypeDecl::isNull() const { return isNullHelper(); } + // !!! This is only temporarily available until the parser is fully migrated // to the new API. !!! const CVC4::Datatype& DatatypeDecl::getDatatype(void) const { return *d_dtype; } @@ -1895,6 +1908,9 @@ DatatypeConstructor::const_iterator::const_iterator( d_idx = begin ? 0 : sels->size(); } +// Nullary constructor for Cython +DatatypeConstructor::const_iterator::const_iterator() {} + DatatypeConstructor::const_iterator& DatatypeConstructor::const_iterator:: operator=(const DatatypeConstructor::const_iterator& it) { @@ -1969,6 +1985,9 @@ Datatype::Datatype(const CVC4::Datatype& dtype) { } +// Nullary constructor for Cython +Datatype::Datatype() {} + Datatype::~Datatype() {} DatatypeConstructor Datatype::operator[](size_t idx) const @@ -2007,6 +2026,8 @@ size_t Datatype::getNumConstructors() const bool Datatype::isParametric() const { return d_dtype->isParametric(); } +std::string Datatype::toString() const { return d_dtype->getName(); } + Datatype::const_iterator Datatype::begin() const { return Datatype::const_iterator(*d_dtype, true); @@ -2035,6 +2056,8 @@ Datatype::const_iterator::const_iterator(const CVC4::Datatype& dtype, d_idx = begin ? 0 : cons->size(); } +Datatype::const_iterator::const_iterator() {} + Datatype::const_iterator& Datatype::const_iterator::operator=( const Datatype::const_iterator& it) { diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h index f7f16832a..79c02c031 100644 --- a/src/api/cvc4cpp.h +++ b/src/api/cvc4cpp.h @@ -1096,6 +1096,11 @@ class CVC4_PUBLIC DatatypeDecl friend class Solver; public: /** + * Nullary constructor for Cython + */ + DatatypeDecl(); + + /** * Destructor. */ ~DatatypeDecl(); @@ -1112,6 +1117,8 @@ class CVC4_PUBLIC DatatypeDecl /** Is this Datatype declaration parametric? */ bool isParametric() const; + bool isNull() const; + /** * @return a string representation of this datatype declaration */ @@ -1158,6 +1165,10 @@ class CVC4_PUBLIC DatatypeDecl const std::string& name, const std::vector<Sort>& params, bool isCoDatatype = false); + + // helper for isNull() to avoid calling API functions from other API functions + bool isNullHelper() const; + /* The internal (intermediate) datatype wrapped by this datatype * declaration * This is a shared_ptr rather than a unique_ptr since CVC4::Datatype is @@ -1295,6 +1306,9 @@ class CVC4_PUBLIC DatatypeConstructor friend class DatatypeConstructor; // to access constructor public: + /** Nullary constructor (required for Cython). */ + const_iterator(); + /** * Assignment operator. * @param it the iterator to assign to @@ -1398,6 +1412,9 @@ class CVC4_PUBLIC Datatype */ Datatype(const CVC4::Datatype& dtype); + // Nullary constructor for Cython + Datatype(); + /** * Destructor. */ @@ -1447,6 +1464,9 @@ class CVC4_PUBLIC Datatype friend class Datatype; // to access constructor public: + /** Nullary constructor (required for Cython). */ + const_iterator(); + /** * Assignment operator. * @param it the iterator to assign to diff --git a/src/api/python/CMakeLists.txt b/src/api/python/CMakeLists.txt new file mode 100644 index 000000000..166a728de --- /dev/null +++ b/src/api/python/CMakeLists.txt @@ -0,0 +1,42 @@ +if(POLICY CMP0057) + # For cmake >= 3.3 this policy changed the behavior of IN_LIST + # if the policy exists, we use the NEW behavior + cmake_policy(SET CMP0057 NEW) +endif() + +find_package(PythonExtensions REQUIRED) +find_package(Cython 0.29 REQUIRED) + +include_directories(${PYTHON_INCLUDE_DIRS}) +include_directories(${CMAKE_CURRENT_LIST_DIR}) # cvc4kinds.pxd +include_directories(${PROJECT_SOURCE_DIR}/src) +include_directories(${PROJECT_SOURCE_DIR}/src/include) +include_directories(${CMAKE_CURRENT_BINARY_DIR}) +# TEMP: Only needed while expr/kind.h is public in the C++ api +include_directories("${CMAKE_BINARY_DIR}/src/") + +# Generate cvc4kinds.{pxd,pyx} +add_custom_target( + gen-pycvc4-kinds + ALL + COMMAND + "${PYTHON_EXECUTABLE}" + "${CMAKE_CURRENT_LIST_DIR}/genkinds.py" + --kinds-header "${PROJECT_SOURCE_DIR}/src/api/cvc4cppkind.h" + --kinds-file-prefix "cvc4kinds" + DEPENDS + genkinds.py + COMMENT + "Generate cvc4kinds.{pxd,pyx}" +) + +add_cython_target(pycvc4 CXX) + +add_library(pycvc4 + MODULE + ${pycvc4}) + +target_link_libraries(pycvc4 cvc4 ${PYTHON_LIBRARIES}) + +python_extension_module(pycvc4) +install(TARGETS pycvc4 DESTINATION lib) diff --git a/src/api/python/cvc4.pxd b/src/api/python/cvc4.pxd new file mode 100644 index 000000000..b8bf009af --- /dev/null +++ b/src/api/python/cvc4.pxd @@ -0,0 +1,274 @@ +# import dereference and increment operators +from cython.operator cimport dereference as deref, preincrement as inc +from libc.stdint cimport int32_t, int64_t, uint32_t, uint64_t +from libcpp.string cimport string +from libcpp.vector cimport vector +from libcpp.pair cimport pair +from cvc4kinds cimport Kind + + +cdef extern from "<iostream>" namespace "std": + cdef cppclass ostream: + pass + ostream cout + + +cdef extern from "api/cvc4cpp.h" namespace "CVC4": + cdef cppclass Options: + pass + + +cdef extern from "api/cvc4cpp.h" namespace "CVC4::api": + cdef cppclass Datatype: + Datatype() except + + DatatypeConstructor operator[](const string& name) except + + DatatypeConstructor getConstructor(const string& name) except + + Term getConstructorTerm(const string& name) except + + size_t getNumConstructors() except + + bint isParametric() except + + string toString() except + + cppclass const_iterator: + const_iterator() except + + bint operator==(const const_iterator& it) except + + bint operator!=(const const_iterator& it) except + + const_iterator& operator++(); + const DatatypeConstructor& operator*() except + + const_iterator begin() except + + const_iterator end() except + + + + cdef cppclass DatatypeConstructor: + DatatypeConstructor() except + + DatatypeSelector operator[](const string& name) except + + DatatypeSelector getSelector(const string& name) except + + Term getSelectorTerm(const string& name) except + + string toString() except + + cppclass const_iterator: + const_iterator() except + + bint operator==(const const_iterator& it) except + + bint operator!=(const const_iterator& it) except + + const_iterator& operator++(); + const DatatypeSelector& operator*() except + + const_iterator begin() except + + const_iterator end() except + + + + cdef cppclass DatatypeConstructorDecl: + DatatypeConstructorDecl(const string& name) except + + void addSelector(const DatatypeSelectorDecl& stor) except + + string toString() except + + + + cdef cppclass DatatypeDecl: + void addConstructor(const DatatypeConstructorDecl& ctor) except + + bint isParametric() except + + string toString() except + + + + cdef cppclass DatatypeDeclSelfSort: + DatatypeDeclSelfSort() except + + + + cdef cppclass DatatypeSelector: + DatatypeSelector() except + + string toString() except + + + + cdef cppclass DatatypeSelectorDecl: + DatatypeSelectorDecl(const string& name, Sort sort) except + + DatatypeSelectorDecl(const string& name, DatatypeDeclSelfSort sort) except + + string toString() except + + + + cdef cppclass Op: + Op() except + + bint operator==(const Op&) except + + bint operator!=(const Op&) except + + Kind getKind() except + + Sort getSort() except + + bint isNull() except + + T getIndices[T]() except + + string toString() except + + + + cdef cppclass Result: + # Note: don't even need constructor + bint isSat() except + + bint isUnsat() except + + bint isSatUnknown() except + + bint isValid() except + + bint isInvalid() except + + bint isValidUnknown() except + + string getUnknownExplanation() except + + string toString() except + + + + cdef cppclass RoundingMode: + pass + + + cdef cppclass Solver: + Solver(Options*) except + + Sort getBooleanSort() except + + Sort getIntegerSort() except + + Sort getRealSort() except + + Sort getRegExpSort() except + + Sort getRoundingmodeSort() except + + Sort getStringSort() except + + Sort mkArraySort(Sort indexSort, Sort elemSort) except + + Sort mkBitVectorSort(uint32_t size) except + + Sort mkFloatingPointSort(uint32_t exp, uint32_t sig) except + + Sort mkDatatypeSort(DatatypeDecl dtypedecl) except + + Sort mkFunctionSort(Sort domain, Sort codomain) except + + Sort mkFunctionSort(const vector[Sort]& sorts, Sort codomain) except + + Sort mkParamSort(const string& symbol) except + + Sort mkPredicateSort(const vector[Sort]& sorts) except + + Sort mkRecordSort(const vector[pair[string, Sort]]& fields) except + + Sort mkSetSort(Sort elemSort) except + + Sort mkUninterpretedSort(const string& symbol) except + + Sort mkSortConstructorSort(const string& symbol, size_t arity) except + + Sort mkTupleSort(const vector[Sort]& sorts) except + + Term mkTerm(Op op) except + + Term mkTerm(Op op, const vector[Term]& children) except + + Op mkOp(Kind kind) except + + Op mkOp(Kind kind, Kind k) except + + Op mkOp(Kind kind, const string& arg) except + + Op mkOp(Kind kind, uint32_t arg) except + + Op mkOp(Kind kind, uint32_t arg1, uint32_t arg2) except + + Term mkTrue() except + + Term mkFalse() except + + Term mkBoolean(bint val) except + + Term mkPi() except + + Term mkReal(const string& s) except + + Term mkRegexpEmpty() except + + Term mkRegexpSigma() except + + Term mkEmptySet(Sort s) except + + Term mkSepNil(Sort sort) except + + Term mkString(const string& s) except + + Term mkString(const vector[unsigned]& s) except + + Term mkUniverseSet(Sort sort) except + + Term mkBitVector(uint32_t size) except + + Term mkBitVector(uint32_t size, uint64_t val) except + + Term mkBitVector(const string& s) except + + Term mkBitVector(const string& s, uint32_t base) except + + Term mkConstArray(Sort sort, Term val) except + + Term mkPosInf(uint32_t exp, uint32_t sig) except + + Term mkNegInf(uint32_t exp, uint32_t sig) except + + Term mkNaN(uint32_t exp, uint32_t sig) except + + Term mkPosZero(uint32_t exp, uint32_t sig) except + + Term mkNegZero(uint32_t exp, uint32_t sig) except + + Term mkRoundingMode(RoundingMode rm) except + + Term mkUninterpretedConst(Sort sort, int32_t index) except + + Term mkAbstractValue(const string& index) except + + Term mkFloatingPoint(uint32_t exp, uint32_t sig, Term val) except + + Term mkConst(Sort sort, const string& symbol) except + + # default value for symbol defined in cvc4cpp.h + Term mkConst(Sort sort) except + + Term mkVar(Sort sort, const string& symbol) except + + DatatypeDecl mkDatatypeDecl(const string& name) except + + DatatypeDecl mkDatatypeDecl(const string& name, bint isCoDatatype) except + + DatatypeDecl mkDatatypeDecl(const string& name, Sort param) except + + DatatypeDecl mkDatatypeDecl(const string& name, Sort param, bint isCoDatatype) except + + DatatypeDecl mkDatatypeDecl(const string& name, vector[Sort]& params) except + + DatatypeDecl mkDatatypeDecl(const string& name, vector[Sort]& params, bint isCoDatatype) except + + # default value for symbol defined in cvc4cpp.h + Term mkVar(Sort sort) except + + Term simplify(const Term& t) except + + void assertFormula(Term term) except + + Result checkSat() except + + Result checkSatAssuming(const vector[Term]& assumptions) except + + Result checkValid() except + + Result checkValidAssuming(const vector[Term]& assumptions) except + + Sort declareDatatype(const string& symbol, const vector[DatatypeConstructorDecl]& ctors) + Term declareFun(const string& symbol, Sort sort) except + + Term declareFun(const string& symbol, const vector[Sort]& sorts, Sort sort) except + + Sort declareSort(const string& symbol, uint32_t arity) except + + Term defineFun(const string& symbol, const vector[Term]& bound_vars, + Sort sort, Term term) except + + Term defineFun(Term fun, const vector[Term]& bound_vars, Term term) except + + Term defineFunRec(const string& symbol, const vector[Term]& bound_vars, + Sort sort, Term term) except + + Term defineFunRec(Term fun, const vector[Term]& bound_vars, + Term term) except + + Term defineFunsRec(vector[Term]& funs, vector[vector[Term]]& bound_vars, + vector[Term]& terms) except + + vector[Term] getAssertions() except + + vector[pair[Term, Term]] getAssignment() except + + string getInfo(const string& flag) except + + string getOption(string& option) except + + vector[Term] getUnsatAssumptions() except + + vector[Term] getUnsatCore() except + + Term getValue(Term term) except + + vector[Term] getValue(const vector[Term]& terms) except + + void pop(uint32_t nscopes) except + + void printModel(ostream& out) + void push(uint32_t nscopes) except + + void reset() except + + void resetAssertions() except + + void setInfo(string& keyword, const string& value) except + + void setLogic(const string& logic) except + + void setOption(const string& option, const string& value) except + + + + cdef cppclass Sort: + Sort() except + + bint operator==(const Sort&) except + + bint operator!=(const Sort&) except + + bint isBoolean() except + + bint isInteger() except + + bint isReal() except + + bint isString() except + + bint isRegExp() except + + bint isRoundingMode() except + + bint isBitVector() except + + bint isFloatingPoint() except + + bint isDatatype() except + + bint isParametricDatatype() except + + bint isFunction() except + + bint isPredicate() except + + bint isTuple() except + + bint isRecord() except + + bint isArray() except + + bint isSet() except + + bint isUninterpretedSort() except + + bint isSortConstructor() except + + bint isFirstClass() except + + bint isFunctionLike() except + + Datatype getDatatype() except + + Sort instantiate(const vector[Sort]& params) except + + bint isUninterpretedSortParameterized() except + + string toString() except + + + cdef cppclass Term: + Term() + bint operator==(const Term&) except + + bint operator!=(const Term&) except + + Kind getKind() except + + Sort getSort() except + + bint hasOp() except + + Op getOp() except + + bint isNull() except + + Term notTerm() except + + Term andTerm(const Term& t) except + + Term orTerm(const Term& t) except + + Term xorTerm(const Term& t) except + + Term eqTerm(const Term& t) except + + Term impTerm(const Term& t) except + + Term iteTerm(const Term& then_t, const Term& else_t) except + + string toString() except + + cppclass const_iterator: + const_iterator() except + + bint operator==(const const_iterator& it) except + + bint operator!=(const const_iterator& it) except + + const_iterator& operator++(); + Term operator*() except + + const_iterator begin() except + + const_iterator end() except + + + +cdef extern from "api/cvc4cpp.h" namespace "CVC4::api::RoundingMode": + cdef RoundingMode ROUND_NEAREST_TIES_TO_EVEN, + cdef RoundingMode ROUND_TOWARD_POSITIVE, + cdef RoundingMode ROUND_TOWARD_NEGATIVE, + cdef RoundingMode ROUND_TOWARD_ZERO, + cdef RoundingMode ROUND_NEAREST_TIES_TO_AWAY diff --git a/src/api/python/cvc4.pxi b/src/api/python/cvc4.pxi new file mode 100644 index 000000000..39d9d4686 --- /dev/null +++ b/src/api/python/cvc4.pxi @@ -0,0 +1,1181 @@ +import sys + +from libc.stdint cimport int32_t, int64_t, uint32_t, uint64_t + +from libcpp.pair cimport pair +from libcpp.string cimport string +from libcpp.vector cimport vector + +from cvc4 cimport cout +from cvc4 cimport Datatype as c_Datatype +from cvc4 cimport DatatypeConstructor as c_DatatypeConstructor +from cvc4 cimport DatatypeConstructorDecl as c_DatatypeConstructorDecl +from cvc4 cimport DatatypeDecl as c_DatatypeDecl +from cvc4 cimport DatatypeDeclSelfSort as c_DatatypeDeclSelfSort +from cvc4 cimport DatatypeSelector as c_DatatypeSelector +from cvc4 cimport DatatypeSelectorDecl as c_DatatypeSelectorDecl +from cvc4 cimport Result as c_Result +from cvc4 cimport RoundingMode as c_RoundingMode +from cvc4 cimport Op as c_Op +from cvc4 cimport Solver as c_Solver +from cvc4 cimport Sort as c_Sort +from cvc4 cimport ROUND_NEAREST_TIES_TO_EVEN, ROUND_TOWARD_POSITIVE +from cvc4 cimport ROUND_TOWARD_ZERO, ROUND_NEAREST_TIES_TO_AWAY +from cvc4 cimport Term as c_Term + +from cvc4kinds cimport Kind as c_Kind + +################################## DECORATORS ################################# +def expand_list_arg(num_req_args=0): + ''' + Creates a decorator that looks at index num_req_args of the args, + if it's a list, it expands it before calling the function. + ''' + def decorator(func): + def wrapper(owner, *args): + if len(args) == num_req_args + 1 and \ + isinstance(args[num_req_args], list): + args = list(args[:num_req_args]) + args[num_req_args] + return func(owner, *args) + return wrapper + return decorator +############################################################################### + +# Style Guidelines +### Using PEP-8 spacing recommendations +### Limit linewidth to 79 characters +### Break before binary operators +### surround top level functions and classes with two spaces +### separate methods by one space +### use spaces in functions sparingly to separate logical blocks +### can omit spaces between unrelated oneliners +### always use c++ default arguments +#### only use default args of None at python level +#### Result class can have default because it's pure python + + +cdef class Datatype: + cdef c_Datatype cd + def __cinit__(self): + pass + + def __getitem__(self, str name): + cdef DatatypeConstructor dc = DatatypeConstructor() + dc.cdc = self.cd[name.encode()] + return dc + + def getConstructor(self, str name): + cdef DatatypeConstructor dc = DatatypeConstructor() + dc.cdc = self.cd.getConstructor(name.encode()) + return dc + + def getConstructorTerm(self, str name): + cdef Term term = Term() + term.cterm = self.cd.getConstructorTerm(name.encode()) + return term + + def getNumConstructors(self): + return self.cd.getNumConstructors() + + def isParametric(self): + return self.cd.isParametric() + + def __str__(self): + return self.cd.toString().decode() + + def __repr__(self): + return self.cd.toString().decode() + + def __iter__(self): + for ci in self.cd: + dc = DatatypeConstructor() + dc.cdc = ci + yield dc + + +cdef class DatatypeConstructor: + cdef c_DatatypeConstructor cdc + def __cinit__(self): + self.cdc = c_DatatypeConstructor() + + def __getitem__(self, str name): + cdef DatatypeSelector ds = DatatypeSelector() + ds.cds = self.cdc[name.encode()] + return ds + + def getSelector(self, str name): + cdef DatatypeSelector ds = DatatypeSelector() + ds.cds = self.cdc.getSelector(name.encode()) + return ds + + def getSelectorTerm(self, str name): + cdef Term term = Term() + term.cterm = self.cdc.getSelectorTerm(name.encode()) + return term + + def __str__(self): + return self.cdc.toString().decode() + + def __repr__(self): + return self.cdc.toString().decode() + + def __iter__(self): + for ci in self.cdc: + ds = DatatypeSelector() + ds.cds = ci + yield ds + + +cdef class DatatypeConstructorDecl: + cdef c_DatatypeConstructorDecl* cddc + def __cinit__(self, str name): + self.cddc = new c_DatatypeConstructorDecl(name.encode()) + + def addSelector(self, DatatypeSelectorDecl stor): + self.cddc.addSelector(stor.cdsd[0]) + + def __str__(self): + return self.cddc.toString().decode() + + def __repr__(self): + return self.cddc.toString().decode() + + +cdef class DatatypeDecl: + cdef c_DatatypeDecl cdd + def __cinit__(self): + pass + + def addConstructor(self, DatatypeConstructorDecl ctor): + self.cdd.addConstructor(ctor.cddc[0]) + + def isParametric(self): + return self.cdd.isParametric() + + def __str__(self): + return self.cdd.toString().decode() + + def __repr__(self): + return self.cdd.toString().decode() + + +cdef class DatatypeDeclSelfSort: + cdef c_DatatypeDeclSelfSort cddss + def __cinit__(self): + self.cddss = c_DatatypeDeclSelfSort() + + +cdef class DatatypeSelector: + cdef c_DatatypeSelector cds + def __cinit__(self): + self.cds = c_DatatypeSelector() + + def __str__(self): + return self.cds.toString().decode() + + def __repr__(self): + return self.cds.toString().decode() + + +cdef class DatatypeSelectorDecl: + cdef c_DatatypeSelectorDecl* cdsd + def __cinit__(self, str name, sort): + if isinstance(sort, Sort): + self.cdsd = new c_DatatypeSelectorDecl( + <const string &> name.encode(), (<Sort?> sort).csort) + elif isinstance(sort, DatatypeDeclSelfSort): + self.cdsd = new c_DatatypeSelectorDecl( + <const string &> name.encode(), + (<DatatypeDeclSelfSort?> sort).cddss) + + def __str__(self): + return self.cdsd.toString().decode() + + def __repr__(self): + return self.cdsd.toString().decode() + + +cdef class Op: + cdef c_Op cop + def __cinit__(self): + self.cop = c_Op() + + def __eq__(self, Op other): + return self.cop == other.cop + + def __ne__(self, Op other): + return self.cop != other.cop + + def __str__(self): + return self.cop.toString().decode() + + def __repr__(self): + return self.cop.toString().decode() + + def getKind(self): + return kind(<int> self.cop.getKind()) + + def getSort(self): + cdef Sort sort = Sort() + sort.csort = self.cop.getSort() + return sort + + def isNull(self): + return self.cop.isNull() + + def getIndices(self): + indices = None + try: + indices = self.cop.getIndices[string]() + except: + pass + + try: + indices = kind(<int> self.cop.getIndices[c_Kind]()) + except: + pass + + try: + indices = self.cop.getIndices[uint32_t]() + except: + pass + + try: + indices = self.cop.getIndices[pair[uint32_t, uint32_t]]() + except: + pass + + if indices is None: + raise RuntimeError("Unable to retrieve indices from {}".format(self)) + + return indices + + +class Result: + def __init__(self, name, explanation=""): + name = name.lower() + incomplete = False + if "(incomplete)" in name: + incomplete = True + name = name.replace("(incomplete)", "").strip() + assert name in {"sat", "unsat", "valid", "invalid", "unknown"}, \ + "can't interpret result = {}".format(name) + + self._name = name + self._explanation = explanation + self._incomplete = incomplete + + def __bool__(self): + if self._name in {"sat", "valid"}: + return True + elif self._name in {"unsat", "invalid"}: + return False + elif self._name == "unknown": + raise RuntimeError("Cannot interpret 'unknown' result as a Boolean") + else: + assert False, "Unhandled result=%s"%self._name + + def __eq__(self, other): + if not isinstance(other, Result): + return False + + return self._name == other._name + + def __ne__(self, other): + return not self.__eq__(other) + + def __str__(self): + return self._name + + def __repr__(self): + return self._name + + def isUnknown(self): + return self._name == "unknown" + + def isIncomplete(self): + return self._incomplete + + @property + def explanation(self): + return self._explanation + + +cdef class RoundingMode: + cdef c_RoundingMode crm + cdef str name + def __cinit__(self, int rm): + # crm always assigned externally + self.crm = <c_RoundingMode> rm + self.name = __rounding_modes[rm] + + def __eq__(self, RoundingMode other): + return (<int> self.crm) == (<int> other.crm) + + def __ne__(self, RoundingMode other): + return not self.__eq__(other) + + def __hash__(self): + return hash((<int> self.crm, self.name)) + + def __str__(self): + return self.name + + def __repr__(self): + return self.name + + +cdef class Solver: + cdef c_Solver* csolver + + def __cinit__(self): + self.csolver = new c_Solver(NULL) + + def getBooleanSort(self): + cdef Sort sort = Sort() + sort.csort = self.csolver.getBooleanSort() + return sort + + def getIntegerSort(self): + cdef Sort sort = Sort() + sort.csort = self.csolver.getIntegerSort() + return sort + + def getRealSort(self): + cdef Sort sort = Sort() + sort.csort = self.csolver.getRealSort() + return sort + + def getRegExpSort(self): + cdef Sort sort = Sort() + sort.csort = self.csolver.getRegExpSort() + return sort + + def getRoundingmodeSort(self): + cdef Sort sort = Sort() + sort.csort = self.csolver.getRoundingmodeSort() + return sort + + def getStringSort(self): + cdef Sort sort = Sort() + sort.csort = self.csolver.getStringSort() + return sort + + def mkArraySort(self, Sort indexSort, Sort elemSort): + cdef Sort sort = Sort() + sort.csort = self.csolver.mkArraySort(indexSort.csort, elemSort.csort) + return sort + + def mkBitVectorSort(self, uint32_t size): + cdef Sort sort = Sort() + sort.csort = self.csolver.mkBitVectorSort(size) + return sort + + def mkFloatingPointSort(self, uint32_t exp, uint32_t sig): + cdef Sort sort = Sort() + sort.csort = self.csolver.mkFloatingPointSort(exp, sig) + return sort + + def mkDatatypeSort(self, DatatypeDecl dtypedecl): + cdef Sort sort = Sort() + sort.csort = self.csolver.mkDatatypeSort(dtypedecl.cdd) + return sort + + def mkFunctionSort(self, sorts, Sort codomain): + + cdef Sort sort = Sort() + # populate a vector with dereferenced c_Sorts + cdef vector[c_Sort] v + + if isinstance(sorts, Sort): + sort.csort = self.csolver.mkFunctionSort((<Sort?> sorts).csort, + codomain.csort) + elif isinstance(sorts, list): + for s in sorts: + v.push_back((<Sort?>s).csort) + + sort.csort = self.csolver.mkFunctionSort(<const vector[c_Sort]&> v, + codomain.csort) + return sort + + def mkParamSort(self, symbolname): + cdef Sort sort = Sort() + sort.csort = self.csolver.mkParamSort(symbolname.encode()) + return sort + + @expand_list_arg(num_req_args=0) + def mkPredicateSort(self, *sorts): + ''' + Supports the following arguments: + Sort mkPredicateSort(List[Sort] sorts) + + where sorts can also be comma-separated arguments of + type Sort + ''' + cdef Sort sort = Sort() + cdef vector[c_Sort] v + for s in sorts: + v.push_back((<Sort?> s).csort) + sort.csort = self.csolver.mkPredicateSort(<const vector[c_Sort]&> v) + return sort + + @expand_list_arg(num_req_args=0) + def mkRecordSort(self, *fields): + ''' + Supports the following arguments: + Sort mkRecordSort(List[Tuple[str, Sort]] fields) + + where fields can also be comma-separated arguments of + type Tuple[str, Sort] + ''' + cdef Sort sort = Sort() + cdef vector[pair[string, c_Sort]] v + cdef pair[string, c_Sort] p + for f in fields: + name, sortarg = f + name = name.encode() + p = pair[string, c_Sort](<string?> name, (<Sort?> sortarg).csort) + v.push_back(p) + sort.csort = self.csolver.mkRecordSort( + <const vector[pair[string, c_Sort]] &> v) + return sort + + def mkSetSort(self, Sort elemSort): + cdef Sort sort = Sort() + sort.csort = self.csolver.mkSetSort(elemSort.csort) + return sort + + def mkUninterpretedSort(self, str name): + cdef Sort sort = Sort() + sort.csort = self.csolver.mkUninterpretedSort(name.encode()) + return sort + + def mkSortConstructorSort(self, str symbol, size_t arity): + cdef Sort sort = Sort() + sort.csort =self.csolver.mkSortConstructorSort(symbol.encode(), arity) + return sort + + @expand_list_arg(num_req_args=0) + def mkTupleSort(self, *sorts): + ''' + Supports the following arguments: + Sort mkTupleSort(List[Sort] sorts) + + where sorts can also be comma-separated arguments of + type Sort + ''' + cdef Sort sort = Sort() + cdef vector[c_Sort] v + for s in sorts: + v.push_back((<Sort?> s).csort) + sort.csort = self.csolver.mkTupleSort(v) + return sort + + @expand_list_arg(num_req_args=1) + def mkTerm(self, kind_or_op, *args): + ''' + Supports the following arguments: + Term mkTerm(Kind kind) + Term mkTerm(Kind kind, Op child1, List[Term] children) + Term mkTerm(Kind kind, List[Term] children) + + where List[Term] can also be comma-separated arguments + ''' + cdef Term term = Term() + cdef vector[c_Term] v + + op = kind_or_op + if isinstance(kind_or_op, kind): + op = self.mkOp(kind_or_op) + + if len(args) == 0: + term.cterm = self.csolver.mkTerm((<Op?> op).cop) + else: + for a in args: + v.push_back((<Term?> a).cterm) + term.cterm = self.csolver.mkTerm((<Op?> op).cop, v) + return term + + def mkOp(self, kind k, arg0=None, arg1 = None): + ''' + Supports the following uses: + Op mkOp(Kind kind) + Op mkOp(Kind kind, Kind k) + Op mkOp(Kind kind, const string& arg) + Op mkOp(Kind kind, uint32_t arg) + Op mkOp(Kind kind, uint32_t arg0, uint32_t arg1) + ''' + cdef Op op = Op() + + if arg0 is None: + op.cop = self.csolver.mkOp(k.k) + elif arg1 is None: + if isinstance(arg0, kind): + op.cop = self.csolver.mkOp(k.k, (<kind?> arg0).k) + elif isinstance(arg0, str): + op.cop = self.csolver.mkOp(k.k, + <const string &> + arg0.encode()) + elif isinstance(arg0, int): + op.cop = self.csolver.mkOp(k.k, <int?> arg0) + else: + raise ValueError("Unsupported signature" + " mkOp: {}".format(" X ".join([k, arg0]))) + else: + if isinstance(arg0, int) and isinstance(arg1, int): + op.cop = self.csolver.mkOp(k.k, <int> arg0, + <int> arg1) + else: + raise ValueError("Unsupported signature" + " mkOp: {}".format(" X ".join([k, arg0, arg1]))) + return op + + def mkTrue(self): + cdef Term term = Term() + term.cterm = self.csolver.mkTrue() + return term + + def mkFalse(self): + cdef Term term = Term() + term.cterm = self.csolver.mkFalse() + return term + + def mkBoolean(self, bint val): + cdef Term term = Term() + term.cterm = self.csolver.mkBoolean(val) + return term + + def mkPi(self): + cdef Term term = Term() + term.cterm = self.csolver.mkPi() + return term + + def mkReal(self, val, den=None): + cdef Term term = Term() + if den is None: + try: + term.cterm = self.csolver.mkReal(str(val).encode()) + except Exception as e: + raise ValueError("Expecting a number" + " or a string representing a number" + " but got: {}".format(val)) + else: + if not isinstance(val, int) or not isinstance(den, int): + raise ValueError("Expecting integers when" + " constructing a rational" + " but got: {}".format((val, den))) + term.cterm = self.csolver.mkReal("{}/{}".format(val, den).encode()) + return term + + def mkRegexpEmpty(self): + cdef Term term = Term() + term.cterm = self.csolver.mkRegexpEmpty() + return term + + def mkRegexpSigma(self): + cdef Term term = Term() + term.cterm = self.csolver.mkRegexpSigma() + return term + + def mkEmptySet(self, Sort s): + cdef Term term = Term() + term.cterm = self.csolver.mkEmptySet(s.csort) + return term + + def mkSepNil(self, Sort sort): + cdef Term term = Term() + term.cterm = self.csolver.mkSepNil(sort.csort) + return term + + def mkString(self, str_or_vec): + cdef Term term = Term() + cdef vector[unsigned] v + if isinstance(str_or_vec, str): + term.cterm = self.csolver.mkString(<string &> str_or_vec.encode()) + elif isinstance(str_or_vec, list): + for u in str_or_vec: + if not isinstance(u, int): + raise ValueError("List should contain ints but got: {}" + .format(str_or_vec)) + v.push_back(<unsigned> u) + term.cterm = self.csolver.mkString(<const vector[unsigned]&> v) + else: + raise ValueError("Expected string or vector of ASCII codes" + " but got: {}".format(str_or_vec)) + return term + + def mkUniverseSet(self, Sort sort): + cdef Term term = Term() + term.cterm = self.csolver.mkUniverseSet(sort.csort) + return term + + def mkBitVector(self, size_or_str, val = None): + cdef Term term = Term() + if isinstance(size_or_str, int): + if val is None: + term.cterm = self.csolver.mkBitVector(<int> size_or_str) + else: + term.cterm = self.csolver.mkBitVector(<int> size_or_str, + <int> val) + elif isinstance(size_or_str, str): + # handle default value + if val is None: + term.cterm = self.csolver.mkBitVector( + <const string &> size_or_str.encode()) + else: + term.cterm = self.csolver.mkBitVector( + <const string &> size_or_str.encode(), <int> val) + else: + raise ValueError("Unexpected inputs {} to" + " mkBitVector".format((size_or_str, val))) + return term + + def mkConstArray(self, Sort sort, Term val): + cdef Term term = Term() + term.cterm = self.csolver.mkConstArray(sort.csort, val.cterm) + return term + + def mkPosInf(self, int exp, int sig): + cdef Term term = Term() + term.cterm = self.csolver.mkPosInf(exp, sig) + return term + + def mkNegInf(self, int exp, int sig): + cdef Term term = Term() + term.cterm = self.csolver.mkNegInf(exp, sig) + return term + + def mkNaN(self, int exp, int sig): + cdef Term term = Term() + term.cterm = self.csolver.mkNaN(exp, sig) + return term + + def mkPosZero(self, int exp, int sig): + cdef Term term = Term() + term.cterm = self.csolver.mkPosZero(exp, sig) + return term + + def mkNegZero(self, int exp, int sig): + cdef Term term = Term() + term.cterm = self.csolver.mkNegZero(exp, sig) + return term + + def mkRoundingMode(self, RoundingMode rm): + cdef Term term = Term() + term.cterm = self.csolver.mkRoundingMode(<c_RoundingMode> rm.crm) + return term + + def mkUninterpretedConst(self, Sort sort, int index): + cdef Term term = Term() + term.cterm = self.csolver.mkUninterpretedConst(sort.csort, index) + return term + + def mkAbstractValue(self, index): + cdef Term term = Term() + try: + term.cterm = self.csolver.mkAbstractValue(str(index).encode()) + except: + raise ValueError("mkAbstractValue expects a str representing a number" + " or an int, but got{}".format(index)) + return term + + def mkFloatingPoint(self, int exp, int sig, Term val): + cdef Term term = Term() + term.cterm = self.csolver.mkFloatingPoint(exp, sig, val.cterm) + return term + + def mkConst(self, Sort sort, symbol=None): + cdef Term term = Term() + if symbol is None: + term.cterm = self.csolver.mkConst(sort.csort) + else: + term.cterm = self.csolver.mkConst(sort.csort, + (<str?> symbol).encode()) + return term + + def mkVar(self, Sort sort, symbol=None): + cdef Term term = Term() + if symbol is None: + term.cterm = self.csolver.mkVar(sort.csort) + else: + term.cterm = self.csolver.mkVar(sort.csort, + (<str?> symbol).encode()) + return term + + def mkDatatypeDecl(self, str name, sorts_or_bool=None, isCoDatatype=None): + cdef DatatypeDecl dd = DatatypeDecl() + cdef vector[c_Sort] v + + # argument cases + if sorts_or_bool is None and isCoDatatype is None: + dd.cdd = self.csolver.mkDatatypeDecl(name.encode()) + elif sorts_or_bool is not None and isCoDatatype is None: + if isinstance(sorts_or_bool, bool): + dd.cdd = self.csolver.mkDatatypeDecl(<const string &> name.encode(), + <bint> sorts_or_bool) + elif isinstance(sorts_or_bool, Sort): + dd.cdd = self.csolver.mkDatatypeDecl(<const string &> name.encode(), + (<Sort> sorts_or_bool).csort) + elif isinstance(sorts_or_bool, list): + for s in sorts_or_bool: + v.push_back((<Sort?> s).csort) + dd.cdd = self.csolver.mkDatatypeDecl(<const string &> name.encode(), + <const vector[c_Sort]&> v) + else: + raise ValueError("Unhandled second argument type {}" + .format(type(sorts_or_bool))) + elif sorts_or_bool is not None and isCoDatatype is not None: + if isinstance(sorts_or_bool, Sort): + dd.cdd = self.csolver.mkDatatypeDecl(<const string &> name.encode(), + (<Sort> sorts_or_bool).csort, + <bint> isCoDatatype) + elif isinstance(sorts_or_bool, list): + for s in sorts_or_bool: + v.push_back((<Sort?> s).csort) + dd.cdd = self.csolver.mkDatatypeDecl(<const string &> name.encode(), + <const vector[c_Sort]&> v, + <bint> isCoDatatype) + else: + raise ValueError("Unhandled second argument type {}" + .format(type(sorts_or_bool))) + else: + raise ValueError("Can't create DatatypeDecl with {}".format([type(a) + for a in [name, + sorts_or_bool, + isCoDatatype]])) + + return dd + + def simplify(self, Term t): + cdef Term term = Term() + term.cterm = self.csolver.simplify(t.cterm) + return term + + def assertFormula(self, Term term): + self.csolver.assertFormula(term.cterm) + + def checkSat(self): + cdef c_Result r = self.csolver.checkSat() + name = r.toString().decode() + explanation = "" + if r.isSatUnknown(): + explanation = r.getUnknownExplanation().decode() + return Result(name, explanation) + + @expand_list_arg(num_req_args=0) + def checkSatAssuming(self, *assumptions): + ''' + Supports the following arguments: + Result checkSatAssuming(List[Term] assumptions) + + where assumptions can also be comma-separated arguments of + type (boolean) Term + ''' + cdef c_Result r + # used if assumptions is a list of terms + cdef vector[c_Term] v + for a in assumptions: + v.push_back((<Term?> a).cterm) + r = self.csolver.checkSatAssuming(<const vector[c_Term]&> v) + name = r.toString().decode() + explanation = "" + if r.isSatUnknown(): + explanation = r.getUnknownExplanation().decode() + return Result(name, explanation) + + def checkValid(self): + cdef c_Result r = self.csolver.checkValid() + name = r.toString().decode() + explanation = "" + if r.isValidUnknown(): + explanation = r.getUnknownExplanation().decode() + return Result(name, explanation) + + @expand_list_arg(num_req_args=0) + def checkValidAssuming(self, *assumptions): + ''' + Supports the following arguments: + Result checkValidAssuming(List[Term] assumptions) + + where assumptions can also be comma-separated arguments of + type (boolean) Term + ''' + cdef c_Result r + # used if assumptions is a list of terms + cdef vector[c_Term] v + for a in assumptions: + v.push_back((<Term?> a).cterm) + r = self.csolver.checkValidAssuming(<const vector[c_Term]&> v) + name = r.toString().decode() + explanation = "" + if r.isValidUnknown(): + explanation = r.getUnknownExplanation().decode() + return Result(name, explanation) + + @expand_list_arg(num_req_args=1) + def declareDatatype(self, str symbol, *ctors): + ''' + Supports the following arguments: + Sort declareDatatype(str symbol, List[Term] ctors) + + where ctors can also be comma-separated arguments of + type DatatypeConstructorDecl + ''' + cdef Sort sort = Sort() + cdef vector[c_DatatypeConstructorDecl] v + + for c in ctors: + v.push_back((<DatatypeConstructorDecl?> c).cddc[0]) + sort.csort = self.csolver.declareDatatype(symbol.encode(), v) + return sort + + def declareFun(self, str symbol, list sorts, Sort sort): + cdef Term term = Term() + cdef vector[c_Sort] v + for s in sorts: + v.push_back((<Sort?> s).csort) + term.cterm = self.csolver.declareFun(symbol.encode(), + <const vector[c_Sort]&> v, + sort.csort) + return term + + def declareSort(self, str symbol, int arity): + cdef Sort sort = Sort() + sort.csort = self.csolver.declareSort(symbol.encode(), arity) + return sort + + def defineFun(self, sym_or_fun, bound_vars, sort_or_term, t=None): + ''' + Supports two uses: + Term defineFun(str symbol, List[Term] bound_vars, + Sort sort, Term term) + Term defineFun(Term fun, List[Term] bound_vars, + Term term) + ''' + cdef Term term = Term() + cdef vector[c_Term] v + for bv in bound_vars: + v.push_back((<Term?> bv).cterm) + + if t is not None: + term.cterm = self.csolver.defineFun((<str?> sym_or_fun).encode(), + <const vector[c_Term] &> v, + (<Sort?> sort_or_term).csort, + (<Term?> t).cterm) + else: + term.cterm = self.csolver.defineFun((<Term?> sym_or_fun).cterm, + <const vector[c_Term]&> v, + (<Term?> sort_or_term).cterm) + + return term + + def defineFunRec(self, sym_or_fun, bound_vars, sort_or_term, t=None): + ''' + Supports two uses: + Term defineFunRec(str symbol, List[Term] bound_vars, + Sort sort, Term term) + Term defineFunRec(Term fun, List[Term] bound_vars, + Term term) + ''' + cdef Term term = Term() + cdef vector[c_Term] v + for bv in bound_vars: + v.push_back((<Term?> bv).cterm) + + if t is not None: + term.cterm = self.csolver.defineFunRec((<str?> sym_or_fun).encode(), + <const vector[c_Term] &> v, + (<Sort?> sort_or_term).csort, + (<Term?> t).cterm) + else: + term.cterm = self.csolver.defineFunRec((<Term?> sym_or_fun).cterm, + <const vector[c_Term]&> v, + (<Term?> sort_or_term).cterm) + + return term + + def defineFunsRec(self, funs, bound_vars, terms): + cdef vector[c_Term] vf + cdef vector[vector[c_Term]] vbv + cdef vector[c_Term] vt + + for f in funs: + vf.push_back((<Term?> f).cterm) + + cdef vector[c_Term] temp + for v in bound_vars: + for t in v: + temp.push_back((<Term?> t).cterm) + vbv.push_back(temp) + temp.clear() + + for t in terms: + vf.push_back((<Term?> t).cterm) + + def getAssertions(self): + assertions = [] + for a in self.csolver.getAssertions(): + term = Term() + term.cterm = a + assertions.append(term) + return assertions + + def getAssignment(self): + ''' + Gives the assignment of *named* formulas as a dictionary. + ''' + assignments = {} + for a in self.csolver.getAssignment(): + varterm = Term() + valterm = Term() + varterm.cterm = a.first + valterm.cterm = a.second + assignments[varterm] = valterm + return assignments + + def getInfo(self, str flag): + return self.csolver.getInfo(flag.encode()) + + def getOption(self, str option): + return self.csolver.getOption(option.encode()) + + def getUnsatAssumptions(self): + assumptions = [] + for a in self.csolver.getUnsatAssumptions(): + term = Term() + term.cterm = a + assumptions.append(term) + return assumptions + + def getUnsatCore(self): + core = [] + for a in self.csolver.getUnsatCore(): + term = Term() + term.cterm = a + core.append(term) + return core + + def getValue(self, Term t): + cdef Term term = Term() + term.cterm = self.csolver.getValue(t.cterm) + return term + + def pop(self, nscopes=1): + self.csolver.pop(nscopes) + + def printModel(self): + self.csolver.printModel(cout) + + def push(self, nscopes=1): + self.csolver.push(nscopes) + + def reset(self): + self.csolver.reset() + + def resetAssertions(self): + self.csolver.resetAssertions() + + def setInfo(self, str keyword, str value): + self.csolver.setInfo(keyword.encode(), value.encode()) + + def setLogic(self, str logic): + self.csolver.setLogic(logic.encode()) + + def setOption(self, str option, str value): + self.csolver.setOption(option.encode(), value.encode()) + + +cdef class Sort: + cdef c_Sort csort + def __cinit__(self): + # csort always set by Solver + pass + + def __eq__(self, Sort other): + return self.csort == other.csort + + def __ne__(self, Sort other): + return self.csort != other.csort + + def __str__(self): + return self.csort.toString().decode() + + def __repr__(self): + return self.csort.toString().decode() + + def isBoolean(self): + return self.csort.isBoolean() + + def isInteger(self): + return self.csort.isInteger() + + def isReal(self): + return self.csort.isReal() + + def isString(self): + return self.csort.isString() + + def isRegExp(self): + return self.csort.isRegExp() + + def isRoundingMode(self): + return self.csort.isRoundingMode() + + def isBitVector(self): + return self.csort.isBitVector() + + def isFloatingPoint(self): + return self.csort.isFloatingPoint() + + def isDatatype(self): + return self.csort.isDatatype() + + def isParametricDatatype(self): + return self.csort.isParametricDatatype() + + def isFunction(self): + return self.csort.isFunction() + + def isPredicate(self): + return self.csort.isPredicate() + + def isTuple(self): + return self.csort.isTuple() + + def isRecord(self): + return self.csort.isRecord() + + def isArray(self): + return self.csort.isArray() + + def isSet(self): + return self.csort.isSet() + + def isUninterpretedSort(self): + return self.csort.isUninterpretedSort() + + def isSortConstructor(self): + return self.csort.isSortConstructor() + + def isFirstClass(self): + return self.csort.isFirstClass() + + def isFunctionLike(self): + return self.csort.isFunctionLike() + + def getDatatype(self): + cdef Datatype d = Datatype() + d.cd = self.csort.getDatatype() + return d + + def instantiate(self, params): + cdef Sort sort = Sort() + cdef vector[c_Sort] v + for s in params: + v.push_back((<Sort?> s).csort) + sort.csort = self.csort.instantiate(v) + return sort + + def isUninterpretedSortParameterized(self): + return self.csort.isUninterpretedSortParameterized() + + +cdef class Term: + cdef c_Term cterm + def __cinit__(self): + # cterm always set in the Solver object + pass + + def __eq__(self, Term other): + return self.cterm == other.cterm + + def __ne__(self, Term other): + return self.cterm != other.cterm + + def __str__(self): + return self.cterm.toString().decode() + + def __repr__(self): + return self.cterm.toString().decode() + + def __iter__(self): + for ci in self.cterm: + term = Term() + term.cterm = ci + yield term + + def getKind(self): + return kind(<int> self.cterm.getKind()) + + def getSort(self): + cdef Sort sort = Sort() + sort.csort = self.cterm.getSort() + return sort + + def hasOp(self): + return self.cterm.hasOp() + + def getOp(self): + cdef Op op = Op() + op.cop = self.cterm.getOp() + return op + + def isNull(self): + return self.cterm.isNull() + + def notTerm(self): + cdef Term term = Term() + term.cterm = self.cterm.notTerm() + return term + + def andTerm(self, Term t): + cdef Term term = Term() + term.cterm = self.cterm.andTerm((<Term> t).cterm) + return term + + def orTerm(self, Term t): + cdef Term term = Term() + term.cterm = self.cterm.orTerm(t.cterm) + return term + + def xorTerm(self, Term t): + cdef Term term = Term() + term.cterm = self.cterm.xorTerm(t.cterm) + return term + + def eqTerm(self, Term t): + cdef Term term = Term() + term.cterm = self.cterm.eqTerm(t.cterm) + return term + + def impTerm(self, Term t): + cdef Term term = Term() + term.cterm = self.cterm.impTerm(t.cterm) + return term + + def iteTerm(self, Term then_t, Term else_t): + cdef Term term = Term() + term.cterm = self.cterm.iteTerm(then_t.cterm, else_t.cterm) + return term + + +# Generate rounding modes +cdef __rounding_modes = { + <int> ROUND_NEAREST_TIES_TO_EVEN: "RoundNearestTiesToEven", + <int> ROUND_TOWARD_POSITIVE: "RoundTowardPositive", + <int> ROUND_TOWARD_ZERO: "RoundTowardZero", + <int> ROUND_NEAREST_TIES_TO_AWAY: "RoundNearestTiesToAway" +} + +mod_ref = sys.modules[__name__] +for rm_int, name in __rounding_modes.items(): + r = RoundingMode(rm_int) + + if name in dir(mod_ref): + raise RuntimeError("Redefinition of Python RoundingMode %s."%name) + + setattr(mod_ref, name, r) + +del r +del rm_int +del name diff --git a/src/api/python/genkinds.py b/src/api/python/genkinds.py new file mode 100755 index 000000000..1e22875e7 --- /dev/null +++ b/src/api/python/genkinds.py @@ -0,0 +1,255 @@ +#!/usr/bin/env python +""" +This script reads CVC4/src/api/cvc4cppkind.h and generates +.pxd and .pxi files which declare all the CVC4 kinds and +implement a Python wrapper for kinds, respectively. The +default names are kinds.pxd / kinds.pxi, but the name is +configurable from the command line with --kinds-file-prefix. + +The script is aware of the '#if 0' pattern and will ignore +kinds declared between '#if 0' and '#endif'. It can also +handle nested '#if 0' pairs. +""" + +import argparse +from collections import OrderedDict + +#################### Default Filenames ################ +DEFAULT_HEADER = 'cvc4cppkind.h' +DEFAULT_PREFIX = 'kinds' + +##################### Useful Constants ################ +OCB = '{' +CCB = '}' +SC = ';' +EQ = '=' +C = ',' +US = '_' +NL = '\n' + +#################### Enum Declarations ################ +ENUM_START = 'enum CVC4_PUBLIC Kind' +ENUM_END = CCB+SC + +################ Comments and Macro Tokens ############ +PYCOMMENT = '#' +COMMENT = '//' +BLOCK_COMMENT_BEGIN = '/*' +BLOCK_COMMENT_END = '*/' +MACRO_BLOCK_BEGIN = '#if 0' +MACRO_BLOCK_END = '#endif' + +#################### Format Kind Names ################ +# special cases for format_name +_IS = '_IS' +# replacements after some preprocessing +replacements = { + 'Bitvector' : 'BV', + 'Floatingpoint': 'FP' +} + +####################### Code Blocks ################### +CDEF_KIND = " cdef Kind " + +KINDS_PXD_TOP = \ +r"""cdef extern from "api/cvc4cppkind.h" namespace "CVC4::api": + cdef cppclass Kind: + pass + + +# Kind declarations: See cvc4cppkind.h for additional information +cdef extern from "api/cvc4cppkind.h" namespace "CVC4::api::Kind": +""" + +KINDS_PXI_TOP = \ +r"""# distutils: language = c++ +# distutils: extra_compile_args = -std=c++11 + +from cvc4kinds cimport * +import sys +from types import ModuleType + +cdef class kind: + cdef Kind k + cdef str name + def __cinit__(self, str name): + self.name = name + + def __eq__(self, kind other): + return (<int> self.k) == (<int> other.k) + + def __ne__(self, kind other): + return (<int> self.k) != (<int> other.k) + + def __hash__(self): + return hash((<int> self.k, self.name)) + + def __str__(self): + return self.name + + def __repr__(self): + return self.name + + def as_int(self): + return <int> self.k + +# create a kinds submodule +kinds = ModuleType('kinds') +# fake a submodule for dotted imports, e.g. from pycvc4.kinds import * +sys.modules['%s.%s'%(__name__, kinds.__name__)] = kinds +kinds.__file__ = kinds.__name__ + ".py" +""" + +KINDS_ATTR_TEMPLATE = \ +r""" +cdef kind {name} = kind("{name}") +{name}.k = {kind} +setattr(kinds, "{name}", {name}) +""" + +class KindsParser: + tokenmap = { + BLOCK_COMMENT_BEGIN : BLOCK_COMMENT_END, + MACRO_BLOCK_BEGIN : MACRO_BLOCK_END + } + + def __init__(self): + self.kinds = OrderedDict() + self.endtoken = None + self.endtoken_stack = [] + self.in_kinds = False + + def format_name(self, name): + ''' + In the Python API, each Kind name is reformatted for easier use + + The naming scheme is: + 1. capitalize the first letter of each word (delimited by underscores) + 2. make the rest of the letters lowercase + 3. replace Floatingpoint with FP + 4. replace Bitvector with BV + + There is one exception: + FLOATINGPOINT_ISNAN --> FPIsNan + + For every "_IS" in the name, there's an underscore added before step 1, + so that the word after "Is" is capitalized + + Examples: + BITVECTOR_PLUS --> BVPlus + APPLY_SELECTOR --> ApplySelector + FLOATINGPOINT_ISNAN --> FPIsNan + SETMINUS --> Setminus + + See the generated .pxi file for an explicit mapping + ''' + name = name.replace(_IS, _IS+US) + words = [w.capitalize() for w in name.lower().split(US)] + name = "".join(words) + + for og, new in replacements.items(): + name = name.replace(og, new) + + return name + + def ignore_block(self, line): + ''' + Returns a boolean telling self.parse whether to ignore a line or not. + It also updates all the necessary state to track comments and macro + blocks + ''' + + # check if entering block comment or macro block + for token in self.tokenmap: + if token in line: + if self.tokenmap[token] not in line: + if self.endtoken is not None: + self.endtoken_stack.append(self.endtoken) + self.endtoken = self.tokenmap[token] + return True + + # check if currently in block comment or macro block + if self.endtoken is not None: + # check if reached the end of block comment or macro block + if self.endtoken in line: + if self.endtoken_stack: + self.endtoken = self.endtoken_stack.pop() + else: + self.endtoken =None + return True + + return False + + def parse(self, filename): + f = open(filename, "r") + + for line in f.read().split(NL): + line = line.strip() + if COMMENT in line: + line = line[:line.find(COMMENT)] + if not line: + continue + + if self.ignore_block(line): + continue + + if ENUM_END in line: + self.in_kinds = False + break + elif self.in_kinds: + if line == OCB: + continue + if EQ in line: + line = line[:line.find(EQ)].strip() + elif C in line: + line = line[:line.find(C)].strip() + self.kinds[line] = self.format_name(line) + elif ENUM_START in line: + self.in_kinds = True + continue + + f.close() + + def gen_pxd(self, filename): + f = open(filename, "w") + f.write(KINDS_PXD_TOP) + # include the format_name docstring in the generated file + # could be helpful for users to see the formatting rules + for line in self.format_name.__doc__.split(NL): + f.write(PYCOMMENT) + if not line.isspace(): + f.write(line) + f.write(NL) + for kind in self.kinds: + f.write(CDEF_KIND + kind + NL) + f.close() + + def gen_pxi(self, filename): + f = open(filename, "w") + pxi = KINDS_PXI_TOP + for kind, name in self.kinds.items(): + pxi += KINDS_ATTR_TEMPLATE.format(name=name, kind=kind) + f.write(pxi) + f.close() + + +if __name__ == "__main__": + parser = argparse.ArgumentParser('Read a kinds header file and generate a ' + 'corresponding pxd file, with simplified kind names.') + parser.add_argument('--kinds-header', metavar='<KINDS_HEADER>', + help='The header file to read kinds from', + default=DEFAULT_HEADER) + parser.add_argument('--kinds-file-prefix', metavar='<KIND_FILE_PREFIX>', + help='The prefix for the .pxd and .pxi files to write ' + 'the Cython declarations to.', + default=DEFAULT_PREFIX) + + args = parser.parse_args() + kinds_header = args.kinds_header + kinds_file_prefix = args.kinds_file_prefix + + kp = KindsParser() + kp.parse(kinds_header) + + kp.gen_pxd(kinds_file_prefix + ".pxd") + kp.gen_pxi(kinds_file_prefix + ".pxi") diff --git a/src/api/python/pycvc4.pyx b/src/api/python/pycvc4.pyx new file mode 100644 index 000000000..40766341a --- /dev/null +++ b/src/api/python/pycvc4.pyx @@ -0,0 +1,2 @@ +include "cvc4kinds.pxi" +include "cvc4.pxi" diff --git a/src/bindings/CMakeLists.txt b/src/bindings/CMakeLists.txt index 135331e54..ac2fadd95 100644 --- a/src/bindings/CMakeLists.txt +++ b/src/bindings/CMakeLists.txt @@ -3,6 +3,12 @@ if(NOT ENABLE_SHARED) endif() find_package(SWIG 3.0.0 REQUIRED) +if(POLICY CMP0078) + cmake_policy(SET CMP0078 OLD) +endif() +if(POLICY CMP0086) + cmake_policy(SET CMP0086 OLD) +endif() if(USE_PYTHON3 AND (SWIG_VERSION VERSION_EQUAL 3.0.8)) message(FATAL_ERROR @@ -21,9 +27,9 @@ include_directories( ${PROJECT_SOURCE_DIR}/src/include ${CMAKE_BINARY_DIR}/src) -if(BUILD_BINDINGS_JAVA) +if(BUILD_SWIG_BINDINGS_JAVA) add_subdirectory(java) endif() -if(BUILD_BINDINGS_PYTHON) +if(BUILD_SWIG_BINDINGS_PYTHON) add_subdirectory(python) endif() diff --git a/test/CMakeLists.txt b/test/CMakeLists.txt index 447d4909f..ad946e3ca 100644 --- a/test/CMakeLists.txt +++ b/test/CMakeLists.txt @@ -27,7 +27,7 @@ add_subdirectory(system EXCLUDE_FROM_ALL) if(ENABLE_UNIT_TESTING) add_subdirectory(unit EXCLUDE_FROM_ALL) - if(BUILD_BINDINGS_JAVA) + if(BUILD_SWIG_BINDINGS_JAVA) add_subdirectory(java) endif() endif() |