- libgmp-dev
- libhamcrest-java
- openjdk-8-jdk
+ - python3
+ - python3-pip
+ - python3-setuptools
- swig3.0
before_install:
- eval "${MATRIX_EVAL}"
- 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')"
# 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
# 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
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
#
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:"
)
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"
--- /dev/null
+#.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)
+
--- /dev/null
+#.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()
+
--- /dev/null
+#.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()
+
--- /dev/null
+#
+# - 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()
+
--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
unit_testing=default
python2=default
python3=default
+python_bindings=default
valgrind=default
profiling=default
readline=default
--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;;
&& 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 ] \
&& 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"
--- /dev/null
+#!/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())
--- /dev/null
+#!/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))
--- /dev/null
+#!/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()
--- /dev/null
+#!/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)
--- /dev/null
+#!/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))
--- /dev/null
+#!/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))
--- /dev/null
+#!/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()
--- /dev/null
+#!/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)))
--- /dev/null
+#!/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))
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; }
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)
{
{
}
+// Nullary constructor for Cython
+Datatype::Datatype() {}
+
Datatype::~Datatype() {}
DatatypeConstructor Datatype::operator[](size_t idx) 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);
d_idx = begin ? 0 : cons->size();
}
+Datatype::const_iterator::const_iterator() {}
+
Datatype::const_iterator& Datatype::const_iterator::operator=(
const Datatype::const_iterator& it)
{
friend class DatatypeConstructorArg;
friend class Solver;
public:
+ /**
+ * Nullary constructor for Cython
+ */
+ DatatypeDecl();
+
/**
* Destructor.
*/
/** Is this Datatype declaration parametric? */
bool isParametric() const;
+ bool isNull() const;
+
/**
* @return a string representation of this datatype declaration
*/
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
friend class DatatypeConstructor; // to access constructor
public:
+ /** Nullary constructor (required for Cython). */
+ const_iterator();
+
/**
* Assignment operator.
* @param it the iterator to assign to
*/
Datatype(const CVC4::Datatype& dtype);
+ // Nullary constructor for Cython
+ Datatype();
+
/**
* Destructor.
*/
friend class Datatype; // to access constructor
public:
+ /** Nullary constructor (required for Cython). */
+ const_iterator();
+
/**
* Assignment operator.
* @param it the iterator to assign to
--- /dev/null
+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)
--- /dev/null
+# 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
--- /dev/null
+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
--- /dev/null
+#!/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")
--- /dev/null
+include "cvc4kinds.pxi"
+include "cvc4.pxi"
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
${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()
if(ENABLE_UNIT_TESTING)
add_subdirectory(unit EXCLUDE_FROM_ALL)
- if(BUILD_BINDINGS_JAVA)
+ if(BUILD_SWIG_BINDINGS_JAVA)
add_subdirectory(java)
endif()
endif()
projects / cvc5.git / commitdiff