Add Python bindings using Cython -- see below for more details (#2879)

1 files changed, 62 insertions, 54 deletions

diff --git a/CMakeLists.txt b/CMakeLists.txt
index 1582a3bde..0cc1174d9 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -174,9 +174,12 @@ set(SYMFPU_DIR        "" CACHE STRING "Set SymFPU install directory")
 # Prepend binaries with prefix on make install
 set(PROGRAM_PREFIX    "" CACHE STRING "Program prefix on make install")
 
-# Supported language bindings
-option(BUILD_BINDINGS_JAVA   "Build Java bindings")
-option(BUILD_BINDINGS_PYTHON "Build Python bindings")
+# Supported SWIG language bindings
+option(BUILD_SWIG_BINDINGS_JAVA   "Build Java bindings with SWIG")
+option(BUILD_SWIG_BINDINGS_PYTHON "Build Python bindings with SWIG")
+
+# Supprted language bindings based on new C++ API
+option(BUILD_BINDINGS_PYTHON "Build Python bindings based on new C++ API ")
 
 #-----------------------------------------------------------------------------#
 # Internal cmake variables
@@ -531,10 +534,14 @@ add_subdirectory(doc)
 add_subdirectory(src)
 add_subdirectory(test)
 
-if(BUILD_BINDINGS_JAVA OR BUILD_BINDINGS_PYTHON)
+if(BUILD_SWIG_BINDINGS_JAVA OR BUILD_SWIG_BINDINGS_PYTHON)
   add_subdirectory(src/bindings)
 endif()
 
+if(BUILD_BINDINGS_PYTHON)
+  add_subdirectory(src/api/python)
+endif()
+
 #-----------------------------------------------------------------------------#
 # Package configuration
 #
@@ -585,89 +592,90 @@ else()
   message("Build profile        : ${CVC4_BUILD_PROFILE_STRING}")
 endif()
 message("")
-print_config("GPL                  :" ENABLE_GPL)
-print_config("Best configuration   :" ENABLE_BEST)
-print_config("Optimization level   :" OPTIMIZATION_LEVEL)
+print_config("GPL                       :" ENABLE_GPL)
+print_config("Best configuration        :" ENABLE_BEST)
+print_config("Optimization level        :" OPTIMIZATION_LEVEL)
 message("")
-print_config("Assertions           :" ENABLE_ASSERTIONS)
-print_config("Debug symbols        :" ENABLE_DEBUG_SYMBOLS)
-print_config("Debug context mem mgr:" ENABLE_DEBUG_CONTEXT_MM)
+print_config("Assertions                :" ENABLE_ASSERTIONS)
+print_config("Debug symbols             :" ENABLE_DEBUG_SYMBOLS)
+print_config("Debug context mem mgr     :" ENABLE_DEBUG_CONTEXT_MM)
 message("")
-print_config("Dumping              :" ENABLE_DUMPING)
-print_config("Muzzle               :" ENABLE_MUZZLE)
-print_config("Proofs               :" ENABLE_PROOFS)
-print_config("Replay               :" ENABLE_REPLAY)
-print_config("Statistics           :" ENABLE_STATISTICS)
-print_config("Tracing              :" ENABLE_TRACING)
+print_config("Dumping                   :" ENABLE_DUMPING)
+print_config("Muzzle                    :" ENABLE_MUZZLE)
+print_config("Proofs                    :" ENABLE_PROOFS)
+print_config("Replay                    :" ENABLE_REPLAY)
+print_config("Statistics                :" ENABLE_STATISTICS)
+print_config("Tracing                   :" ENABLE_TRACING)
 message("")
-print_config("ASan                 :" ENABLE_ASAN)
-print_config("UBSan                :" ENABLE_UBSAN)
-print_config("TSan                 :" ENABLE_TSAN)
-print_config("Coverage (gcov)      :" ENABLE_COVERAGE)
-print_config("Profiling (gprof)    :" ENABLE_PROFILING)
-print_config("Unit tests           :" ENABLE_UNIT_TESTING)
-print_config("Valgrind             :" ENABLE_VALGRIND)
+print_config("ASan                      :" ENABLE_ASAN)
+print_config("UBSan                     :" ENABLE_UBSAN)
+print_config("TSan                      :" ENABLE_TSAN)
+print_config("Coverage (gcov)           :" ENABLE_COVERAGE)
+print_config("Profiling (gprof)         :" ENABLE_PROFILING)
+print_config("Unit tests                :" ENABLE_UNIT_TESTING)
+print_config("Valgrind                  :" ENABLE_VALGRIND)
 message("")
-print_config("Shared libs          :" ENABLE_SHARED)
-print_config("Static binary        :" ENABLE_STATIC_BINARY)
-print_config("Java bindings        :" BUILD_BINDINGS_JAVA)
-print_config("Python bindings      :" BUILD_BINDINGS_PYTHON)
-print_config("Python2              :" USE_PYTHON2)
-print_config("Python3              :" USE_PYTHON3)
+print_config("Shared libs               :" ENABLE_SHARED)
+print_config("Static binary             :" ENABLE_STATIC_BINARY)
+print_config("Java SWIG bindings        :" BUILD_SWIG_BINDINGS_JAVA)
+print_config("Python SWIG bindings      :" BUILD_SWIG_BINDINGS_PYTHON)
+print_config("Python bindings           :" BUILD_BINDINGS_PYTHON)
+print_config("Python2                   :" USE_PYTHON2)
+print_config("Python3                   :" USE_PYTHON3)
 message("")
-print_config("ABC                  :" USE_ABC)
-print_config("CaDiCaL              :" USE_CADICAL)
-print_config("CryptoMiniSat        :" USE_CRYPTOMINISAT)
-print_config("drat2er              :" USE_DRAT2ER)
-print_config("GLPK                 :" USE_GLPK)
-print_config("LFSC                 :" USE_LFSC)
+print_config("ABC                       :" USE_ABC)
+print_config("CaDiCaL                   :" USE_CADICAL)
+print_config("CryptoMiniSat             :" USE_CRYPTOMINISAT)
+print_config("drat2er                   :" USE_DRAT2ER)
+print_config("GLPK                      :" USE_GLPK)
+print_config("LFSC                      :" USE_LFSC)
 
 if(CVC4_USE_CLN_IMP)
-  message("MP library           : cln")
+  message("MP library                   : cln")
 else()
-  message("MP library           : gmp")
+  message("MP library                   : gmp")
 endif()
-print_config("Readline             :" ${USE_READLINE})
-print_config("SymFPU               :" ${USE_SYMFPU})
+print_config("Readline                  :" ${USE_READLINE})
+print_config("SymFPU                    :" ${USE_SYMFPU})
 message("")
 if(ABC_DIR)
-  message("ABC dir              : ${ABC_DIR}")
+  message("ABC dir                      : ${ABC_DIR}")
 endif()
 if(ANTLR_DIR)
-  message("ANTLR dir            : ${ANTLR_DIR}")
+  message("ANTLR dir                    : ${ANTLR_DIR}")
 endif()
 if(CADICAL_DIR)
-  message("CADICAL dir          : ${CADICAL_DIR}")
+  message("CADICAL dir                  : ${CADICAL_DIR}")
 endif()
 if(CRYPTOMINISAT_DIR)
-  message("CRYPTOMINISAT dir    : ${CRYPTOMINISAT_DIR}")
+  message("CRYPTOMINISAT dir            : ${CRYPTOMINISAT_DIR}")
 endif()
 if(DRAT2ER_DIR)
-  message("DRAT2ER dir          : ${DRAT2ER_DIR}")
+  message("DRAT2ER dir                  : ${DRAT2ER_DIR}")
 endif()
 if(GLPK_DIR)
-  message("GLPK dir             : ${GLPK_DIR}")
+  message("GLPK dir                     : ${GLPK_DIR}")
 endif()
 if(GMP_DIR)
-  message("GMP dir              : ${GMP_DIR}")
+  message("GMP dir                      : ${GMP_DIR}")
 endif()
 if(LFSC_DIR)
-  message("LFSC dir             : ${LFSC_DIR}")
+  message("LFSC dir                     : ${LFSC_DIR}")
 endif()
 if(SYMFPU_DIR)
-  message("SYMFPU dir           : ${SYMFPU_DIR}")
+  message("SYMFPU dir                   : ${SYMFPU_DIR}")
 endif()
 message("")
-message("CPPLAGS (-D...)      : ${CVC4_DEFINITIONS}")
-message("CXXFLAGS             : ${CMAKE_CXX_FLAGS}")
-message("CFLAGS               : ${CMAKE_C_FLAGS}")
+message("CPPLAGS (-D...)                : ${CVC4_DEFINITIONS}")
+message("CXXFLAGS                       : ${CMAKE_CXX_FLAGS}")
+message("CFLAGS                         : ${CMAKE_C_FLAGS}")
 message("")
-message("Install prefix       : ${CMAKE_INSTALL_PREFIX}")
+message("Install prefix                 : ${CMAKE_INSTALL_PREFIX}")
 message("")
 
 if(GPL_LIBS)
   message(
-  "CVC4 license         : GPLv3 (due to optional libraries; see below)"
+  "CVC4 license                         : GPLv3 (due to optional libraries; see below)"
   "\n"
   "\n"
   "Please note that CVC4 will be built against the following GPLed libraries:"
@@ -684,7 +692,7 @@ if(GPL_LIBS)
   )
 else()
   message(
-  "CVC4 license         : modified BSD"
+  "CVC4 license                         : modified BSD"
   "\n"
   "\n"
   "Note that this configuration is NOT built against any GPL'ed libraries, so"