Support Python2

CMakeLists.txt

@@ -117,14 +117,20 @@ option (USE_PYTHON2
 # Decide on Python version before setting up googletest
 # Otherwise might use wrong version
 if (BUILD_PYTHON_BINDINGS)
-  # We currently use FindPythonInterp even though it is deprecated since 3.12
-  # This is because the scikit-build files still use this version and it will
-  # not interact well with the latest Python finding cmake modules
-  # https://cmake.org/cmake/help/v3.12/module/FindPython.html
-  # in the future, we can switch to FindPython3 once it has become more standard
-  # i.e. when the following issue is resolved:
-  # https://github.com/scikit-build/scikit-build/issues/506
-  find_package(PythonInterp 3.5 REQUIRED)
+  if (USE_PYTHON2)
+    message(WARNING "Python 2 has been officially deprecated. This option is not
+                     maintained or tested and will likely be removed eventually.")
+    find_package(PythonInterp 2.7 REQUIRED)
+  else()
+    # We currently use FindPythonInterp even though it is deprecated since 3.12
+    # This is because the scikit-build files still use this version and it will
+    # not interact well with the latest Python finding cmake modules
+    # https://cmake.org/cmake/help/v3.12/module/FindPython.html
+    # in the future, we can switch to FindPython3 once it has become more standard
+    # i.e. when the following issue is resolved:
+    # https://github.com/scikit-build/scikit-build/issues/506
+    find_package(PythonInterp 3.5 REQUIRED)
+  endif()
 endif()
 
 if (BUILD_BITWUZLA OR BUILD_CVC5 OR BUILD_MSAT OR BUILD_YICES2 OR BUILD_Z3)

configure.sh

@@ -28,6 +28,7 @@ Configures the CMAKE build environment.
 --debug                 build debug with debug symbols (default: off)
 --static                create static libaries (default: off)
 --python                compile with python bindings (default: off)
+--use-python2           use python2.7 with python bindings (default: off)
 --smtlib-reader         include the smt-lib reader - requires bison/flex (default:off)
 --bison-dir=STR         custom bison installation directory
 --flex-dir=STR          custom flex installation directory
@@ -59,6 +60,7 @@ yices2_home=default
 z3_home=default
 static=default
 python=default
+python2=default
 smtlib_reader=default
 bison_dir=default
 flex_dir=default
@@ -178,6 +180,10 @@ do
         --python)
             python=yes
             ;;
+        --python2)
+            python=yes
+            python2=yes
+            ;;
         --smtlib-reader)
             smtlib_reader=yes
             ;;
@@ -273,6 +279,9 @@ cmake_opts="$cmake_opts -DCMAKE_BUILD_TYPE=$build_type"
 [ $python != default ] \
     && cmake_opts="$cmake_opts -DBUILD_PYTHON_BINDINGS=ON"
 
+[ $python2 != default ] \
+    && cmake_opts="$cmake_opts -DUSE_PYTHON2=ON"
+
 [ $smtlib_reader != default ] \
     && cmake_opts="$cmake_opts -DSMTLIB_READER=ON"
 

python/setup.py.in

@@ -13,7 +13,8 @@ setup(name=PACKAGE_NAME,
       url='http://github.com/makaimann/smt-switch',
       license='BSD',
       zip_safe=False,
-      package_data={'': [f'{PACKAGE_NAME}.so']},
+      package_data={'': [PACKAGE_NAME+'.so']},
+      install_requires=['six'],
       extras_require={
           'pysmt': PYSMT_REQUIRES,
           'test': TEST_REQUIRES,

python/smt_switch/smt_switch_imp.pxi

@@ -1,4 +1,5 @@
-from abc import ABC, abstractmethod
+from abc import ABCMeta, abstractmethod
+import six
 
 from cython.operator cimport dereference as dref
 from libcpp.string cimport string
@@ -532,7 +533,8 @@ def conjunctive_partition(Term term, bint include_bvand=False):
 
     return python_out_list
 
-class TermDagVisitor(ABC):
+@six.add_metaclass(ABCMeta)
+class TermDagVisitor(object):
     def __init__(self):
         pass