Remove SWIG bindings (#4683)

This commit removes support for SWIG bindings for the legacy API. The
bindings were already broken by 19054b3b1d427e662d30d4322df2b2f2361353da
and we are not planning on using SWIG for the Java API for the new API.

8 files changed, 0 insertions, 763 deletions

diff --git a/src/bindings/CMakeLists.txt b/src/bindings/CMakeLists.txt
deleted file mode 100644
index ac2fadd95..000000000
--- a/src/bindings/CMakeLists.txt
+++ /dev/null
@@ -1,35 +0,0 @@
-if(NOT ENABLE_SHARED)
-  message(FATAL_ERROR "Can't build language bindings for static CVC4 build.")
-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
-    "\nSWIG ${SWIG_VERSION} is not supported for python3 bindings because of the following bug: https://github.com/swig/swig/issues/588
-Please downgrade to 3.0.0-3.0.7 or upgrade.")
-endif()
-
-include(${SWIG_USE_FILE})
-
-set(CVC4_SWIG_INTERFACE ${PROJECT_SOURCE_DIR}/src/cvc4.i)
-
-set_property(SOURCE ${CVC4_SWIG_INTERFACE} PROPERTY CPLUSPLUS ON)
-
-include_directories(
-    ${PROJECT_SOURCE_DIR}/src
-    ${PROJECT_SOURCE_DIR}/src/include
-    ${CMAKE_BINARY_DIR}/src)
-
-if(BUILD_SWIG_BINDINGS_JAVA)
-  add_subdirectory(java)
-endif()
-if(BUILD_SWIG_BINDINGS_PYTHON)
-  add_subdirectory(python)
-endif()
diff --git a/src/bindings/java/CMakeLists.txt b/src/bindings/java/CMakeLists.txt
deleted file mode 100644
index 8159b8ee0..000000000
--- a/src/bindings/java/CMakeLists.txt
+++ /dev/null
@@ -1,196 +0,0 @@
-find_package(Java REQUIRED)
-find_package(JNI REQUIRED)
-include(UseJava)
-
-include_directories(${JNI_INCLUDE_DIRS})
-
-set(SWIG_MODULE_cvc4jni_EXTRA_DEPS cvc4 cvc4parser)
-set_property(SOURCE ${CVC4_SWIG_INTERFACE} PROPERTY CPLUSPLUS ON)
-set(CMAKE_SWIG_FLAGS -package edu.stanford.CVC4)
-
-if(${CMAKE_VERSION} VERSION_LESS "3.8.0")
-  swig_add_module(cvc4jni Java ${CVC4_SWIG_INTERFACE})
-else()
-  swig_add_library(cvc4jni LANGUAGE Java SOURCES ${CVC4_SWIG_INTERFACE})
-endif()
-swig_link_libraries(cvc4jni cvc4 cvc4parser ${JNI_LIBRARIRES})
-
-# Create CVC4.jar from all generated *.java files.
-set(gen_java_files
-  ${CMAKE_CURRENT_BINARY_DIR}/ArrayStoreAll.java
-  ${CMAKE_CURRENT_BINARY_DIR}/ArrayStoreAllHashFunction.java
-  ${CMAKE_CURRENT_BINARY_DIR}/ArrayType.java
-  ${CMAKE_CURRENT_BINARY_DIR}/AscriptionType.java
-  ${CMAKE_CURRENT_BINARY_DIR}/AscriptionTypeHashFunction.java
-  ${CMAKE_CURRENT_BINARY_DIR}/BitVector.java
-  ${CMAKE_CURRENT_BINARY_DIR}/BitVectorBitOf.java
-  ${CMAKE_CURRENT_BINARY_DIR}/BitVectorBitOfHashFunction.java
-  ${CMAKE_CURRENT_BINARY_DIR}/BitVectorExtract.java
-  ${CMAKE_CURRENT_BINARY_DIR}/BitVectorExtractHashFunction.java
-  ${CMAKE_CURRENT_BINARY_DIR}/BitVectorHashFunction.java
-  ${CMAKE_CURRENT_BINARY_DIR}/BitVectorRepeat.java
-  ${CMAKE_CURRENT_BINARY_DIR}/BitVectorRotateLeft.java
-  ${CMAKE_CURRENT_BINARY_DIR}/BitVectorRotateRight.java
-  ${CMAKE_CURRENT_BINARY_DIR}/BitVectorSignExtend.java
-  ${CMAKE_CURRENT_BINARY_DIR}/BitVectorSize.java
-  ${CMAKE_CURRENT_BINARY_DIR}/BitVectorType.java
-  ${CMAKE_CURRENT_BINARY_DIR}/BitVectorZeroExtend.java
-  ${CMAKE_CURRENT_BINARY_DIR}/BoolHashFunction.java
-  ${CMAKE_CURRENT_BINARY_DIR}/BooleanType.java
-  ${CMAKE_CURRENT_BINARY_DIR}/CVC4.java
-  ${CMAKE_CURRENT_BINARY_DIR}/CVC4IllegalArgumentException.java
-  ${CMAKE_CURRENT_BINARY_DIR}/CVC4JNI.java
-  ${CMAKE_CURRENT_BINARY_DIR}/CVC4String.java
-  ${CMAKE_CURRENT_BINARY_DIR}/CVC4StringHashFunction.java
-  ${CMAKE_CURRENT_BINARY_DIR}/Cardinality.java
-  ${CMAKE_CURRENT_BINARY_DIR}/CardinalityBeth.java
-  ${CMAKE_CURRENT_BINARY_DIR}/CardinalityUnknown.java
-  ${CMAKE_CURRENT_BINARY_DIR}/Configuration.java
-  ${CMAKE_CURRENT_BINARY_DIR}/ConstructorType.java
-  ${CMAKE_CURRENT_BINARY_DIR}/Datatype.java
-  ${CMAKE_CURRENT_BINARY_DIR}/DatatypeConstructor.java
-  ${CMAKE_CURRENT_BINARY_DIR}/DatatypeConstructorArg.java
-  ${CMAKE_CURRENT_BINARY_DIR}/DatatypeHashFunction.java
-  ${CMAKE_CURRENT_BINARY_DIR}/DatatypeIndexConstant.java
-  ${CMAKE_CURRENT_BINARY_DIR}/DatatypeIndexConstantHashFunction.java
-  ${CMAKE_CURRENT_BINARY_DIR}/DatatypeResolutionException.java
-  ${CMAKE_CURRENT_BINARY_DIR}/DatatypeSelfType.java
-  ${CMAKE_CURRENT_BINARY_DIR}/DatatypeType.java
-  ${CMAKE_CURRENT_BINARY_DIR}/DatatypeUnresolvedType.java
-  ${CMAKE_CURRENT_BINARY_DIR}/EmptySet.java
-  ${CMAKE_CURRENT_BINARY_DIR}/EmptySetHashFunction.java
-  ${CMAKE_CURRENT_BINARY_DIR}/Exception.java
-  ${CMAKE_CURRENT_BINARY_DIR}/ExportUnsupportedException.java
-  ${CMAKE_CURRENT_BINARY_DIR}/Expr.java
-  ${CMAKE_CURRENT_BINARY_DIR}/ExprHashFunction.java
-  ${CMAKE_CURRENT_BINARY_DIR}/ExprManager.java
-  ${CMAKE_CURRENT_BINARY_DIR}/ExprManagerMapCollection.java
-  ${CMAKE_CURRENT_BINARY_DIR}/ExprSequence.java
-  ${CMAKE_CURRENT_BINARY_DIR}/FloatingPoint.java
-  ${CMAKE_CURRENT_BINARY_DIR}/FloatingPointConvertSort.java
-  ${CMAKE_CURRENT_BINARY_DIR}/FloatingPointSize.java
-  ${CMAKE_CURRENT_BINARY_DIR}/FloatingPointToBV.java
-  ${CMAKE_CURRENT_BINARY_DIR}/FloatingPointToFPFloatingPoint.java
-  ${CMAKE_CURRENT_BINARY_DIR}/FloatingPointToFPGeneric.java
-  ${CMAKE_CURRENT_BINARY_DIR}/FloatingPointToFPIEEEBitVector.java
-  ${CMAKE_CURRENT_BINARY_DIR}/FloatingPointToFPReal.java
-  ${CMAKE_CURRENT_BINARY_DIR}/FloatingPointToFPSignedBitVector.java
-  ${CMAKE_CURRENT_BINARY_DIR}/FloatingPointToFPUnsignedBitVector.java
-  ${CMAKE_CURRENT_BINARY_DIR}/FloatingPointToSBV.java
-  ${CMAKE_CURRENT_BINARY_DIR}/FloatingPointToUBV.java
-  ${CMAKE_CURRENT_BINARY_DIR}/FloatingPointType.java
-  ${CMAKE_CURRENT_BINARY_DIR}/FunctionType.java
-  ${CMAKE_CURRENT_BINARY_DIR}/InputLanguage.java
-  ${CMAKE_CURRENT_BINARY_DIR}/IntAnd.java
-  ${CMAKE_CURRENT_BINARY_DIR}/IntToBitVector.java
-  ${CMAKE_CURRENT_BINARY_DIR}/Integer.java
-  ${CMAKE_CURRENT_BINARY_DIR}/IntegerHashFunction.java
-  ${CMAKE_CURRENT_BINARY_DIR}/IntegerType.java
-  ${CMAKE_CURRENT_BINARY_DIR}/JavaInputStreamAdapter.java
-  ${CMAKE_CURRENT_BINARY_DIR}/JavaIteratorAdapter_Datatype.java
-  ${CMAKE_CURRENT_BINARY_DIR}/JavaIteratorAdapter_DatatypeConstructor.java
-  ${CMAKE_CURRENT_BINARY_DIR}/JavaIteratorAdapter_Expr.java
-  ${CMAKE_CURRENT_BINARY_DIR}/JavaIteratorAdapter_StatisticsBase.java
-  ${CMAKE_CURRENT_BINARY_DIR}/JavaIteratorAdapter_UnsatCore.java
-  ${CMAKE_CURRENT_BINARY_DIR}/JavaOutputStreamAdapter.java
-  ${CMAKE_CURRENT_BINARY_DIR}/Kind.java
-  ${CMAKE_CURRENT_BINARY_DIR}/KindHashFunction.java
-  ${CMAKE_CURRENT_BINARY_DIR}/LastExceptionBuffer.java
-  ${CMAKE_CURRENT_BINARY_DIR}/LogicException.java
-  ${CMAKE_CURRENT_BINARY_DIR}/LogicInfo.java
-  ${CMAKE_CURRENT_BINARY_DIR}/ModalException.java
-  ${CMAKE_CURRENT_BINARY_DIR}/OptionException.java
-  ${CMAKE_CURRENT_BINARY_DIR}/Options.java
-  ${CMAKE_CURRENT_BINARY_DIR}/OutputLanguage.java
-  ${CMAKE_CURRENT_BINARY_DIR}/PrettySExprs.java
-  ${CMAKE_CURRENT_BINARY_DIR}/Proof.java
-  ${CMAKE_CURRENT_BINARY_DIR}/Rational.java
-  ${CMAKE_CURRENT_BINARY_DIR}/RationalHashFunction.java
-  ${CMAKE_CURRENT_BINARY_DIR}/RealType.java
-  ${CMAKE_CURRENT_BINARY_DIR}/RecoverableModalException.java
-  ${CMAKE_CURRENT_BINARY_DIR}/RegExpLoop.java
-  ${CMAKE_CURRENT_BINARY_DIR}/RegExpRepeat.java
-  ${CMAKE_CURRENT_BINARY_DIR}/RegExpType.java
-  ${CMAKE_CURRENT_BINARY_DIR}/Result.java
-  ${CMAKE_CURRENT_BINARY_DIR}/RoundingMode.java
-  ${CMAKE_CURRENT_BINARY_DIR}/RoundingModeType.java
-  ${CMAKE_CURRENT_BINARY_DIR}/SExpr.java
-  ${CMAKE_CURRENT_BINARY_DIR}/SExprKeyword.java
-  ${CMAKE_CURRENT_BINARY_DIR}/SExprType.java
-  ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_CVC4__Model.java
-  ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_CVC4__options__InstFormatMode.java
-  ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_MaybeT_CVC4__Rational_t.java
-  ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_Type.java
-  ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_std__istream.java
-  ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_std__ostream.java
-  ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_std__shared_ptrT_CVC4__SygusPrintCallback_t.java
-  ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_std__string.java
-  ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_std__vectorT_CVC4__DatatypeConstructorArg_t.java
-  ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_std__vectorT_std__pairT_CVC4__Expr_CVC4__Expr_t_t.java
-  ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_std__vectorT_std__vectorT_std__string_t_t.java
-  ${CMAKE_CURRENT_BINARY_DIR}/SelectorType.java
-  ${CMAKE_CURRENT_BINARY_DIR}/SequenceType.java
-  ${CMAKE_CURRENT_BINARY_DIR}/SetType.java
-  ${CMAKE_CURRENT_BINARY_DIR}/SmtEngine.java
-  ${CMAKE_CURRENT_BINARY_DIR}/SortConstructorType.java
-  ${CMAKE_CURRENT_BINARY_DIR}/SortType.java
-  ${CMAKE_CURRENT_BINARY_DIR}/Statistic.java
-  ${CMAKE_CURRENT_BINARY_DIR}/Statistics.java
-  ${CMAKE_CURRENT_BINARY_DIR}/StatisticsBase.java
-  ${CMAKE_CURRENT_BINARY_DIR}/StringType.java
-  ${CMAKE_CURRENT_BINARY_DIR}/TesterType.java
-  ${CMAKE_CURRENT_BINARY_DIR}/TheoryId.java
-  ${CMAKE_CURRENT_BINARY_DIR}/TupleUpdate.java
-  ${CMAKE_CURRENT_BINARY_DIR}/TupleUpdateHashFunction.java
-  ${CMAKE_CURRENT_BINARY_DIR}/Type.java
-  ${CMAKE_CURRENT_BINARY_DIR}/TypeCheckingException.java
-  ${CMAKE_CURRENT_BINARY_DIR}/TypeConstant.java
-  ${CMAKE_CURRENT_BINARY_DIR}/TypeConstantHashFunction.java
-  ${CMAKE_CURRENT_BINARY_DIR}/TypeHashFunction.java
-  ${CMAKE_CURRENT_BINARY_DIR}/UninterpretedConstant.java
-  ${CMAKE_CURRENT_BINARY_DIR}/UninterpretedConstantHashFunction.java
-  ${CMAKE_CURRENT_BINARY_DIR}/UnrecognizedOptionException.java
-  ${CMAKE_CURRENT_BINARY_DIR}/UnsafeInterruptException.java
-  ${CMAKE_CURRENT_BINARY_DIR}/UnsatCore.java
-  ${CMAKE_CURRENT_BINARY_DIR}/VariableTypeMap.java
-  ${CMAKE_CURRENT_BINARY_DIR}/setOfType.java
-  ${CMAKE_CURRENT_BINARY_DIR}/vectorDatatype.java
-  ${CMAKE_CURRENT_BINARY_DIR}/vectorDatatypeType.java
-  ${CMAKE_CURRENT_BINARY_DIR}/vectorExpr.java
-  ${CMAKE_CURRENT_BINARY_DIR}/vectorSExpr.java
-  ${CMAKE_CURRENT_BINARY_DIR}/vectorString.java
-  ${CMAKE_CURRENT_BINARY_DIR}/vectorType.java
-  ${CMAKE_CURRENT_BINARY_DIR}/vectorUnsignedInt.java
-  ${CMAKE_CURRENT_BINARY_DIR}/vectorVectorExpr.java
-)
-
-if(CVC4_USE_CLN_IMP)
-  list(APPEND gen_java_files
-    ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_cln__cl_I.java
-    ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_cln__cl_RA.java
-  )
-elseif(CVC4_USE_GMP_IMP)
-  list(APPEND gen_java_files
-    ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_mpq_class.java
-    ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_mpz_class.java
-  )
-endif()
-
-set(CMAKE_JNI_TARGET TRUE)
-add_jar(cvc4jar
-        SOURCES ${gen_java_files}
-        VERSION ${CVC4_MAJOR}.${CVC4_MINOR}.${CVC4_RELEASE}
-        OUTPUT_NAME CVC4)
-add_dependencies(cvc4jar cvc4jni)
-install_jar(cvc4jar DESTINATION share/java/cvc4)
-install_jni_symlink(cvc4jar DESTINATION share/java/cvc4)
-install(TARGETS cvc4jni
-  EXPORT cvc4-targets
-  DESTINATION ${LIBRARY_INSTALL_DIR})
-
-install_jar_exports(
-  TARGETS cvc4jar
-  NAMESPACE CVC4::
-  FILE CVC4JavaTargets.cmake
-  DESTINATION ${LIBRARY_INSTALL_DIR}/cmake/CVC4
-)
diff --git a/src/bindings/java/cvc4_std_vector.i b/src/bindings/java/cvc4_std_vector.i
deleted file mode 100644
index e032426a0..000000000
--- a/src/bindings/java/cvc4_std_vector.i
+++ /dev/null
@@ -1,206 +0,0 @@
-/**
- * The following file is based on
- * https://github.com/swig/swig/blob/master/Lib/java/std_vector.i
- *
- * Note: The SWIG library is under a different license than SWIG itself. See
- * https://github.com/swig/swig/blob/master/LICENSE for details.
- *
- * This file defines the macro SWIG_STD_VECTOR_EM to wrap a C++ std::vector for
- * Java, similar to the SWIG library. The core difference is that the utilities
- * in this file add a reference to an ExprManager to keep it alive as long as
- * the vector lives.
- */
-
-%include <std_common.i>
-
-%{
-#include <vector>
-#include <stdexcept>
-%}
-
-%fragment("SWIG_VectorSize", "header", fragment="SWIG_JavaIntFromSize_t") {
-SWIGINTERN jint SWIG_VectorSize(size_t size) {
-  static const jint JINT_MAX = 0x7FFFFFFF;
-  if (size > static_cast<size_t>(JINT_MAX))
-  {
-    throw std::out_of_range("vector size is too large to fit into a Java int");
-  }
-  return static_cast<jint>(size);
-}
-}
-
-%define SWIG_STD_VECTOR_EM(CTYPE, CONST_REFERENCE)
-
-namespace std {
-  template<> class vector<CTYPE> {
-
-%typemap(javabase) std::vector< CTYPE > "java.util.AbstractList<$typemap(jstype, CTYPE)>"
-%typemap(javainterfaces) std::vector< CTYPE > "java.util.RandomAccess"
-
-%typemap(javabody) std::vector< CTYPE > %{
-  private long swigCPtr;
-  protected boolean swigCMemOwn;
-  private ExprManager em;
-
-  protected $javaclassname(ExprManager em, long cPtr, boolean cMemoryOwn) {
-    swigCMemOwn = cMemoryOwn;
-    swigCPtr = cPtr;
-    this.em = em;
-  }
-
-  public $javaclassname(ExprManager em) {
-    this();
-    this.em = em;
-  }
-
-  protected static long getCPtr($javaclassname obj) {
-    return (obj == null) ? 0 : obj.swigCPtr;
-  }
-%}
-
-%typemap(javaconstruct) std::vector<CTYPE> {
-  this(null, $imcall, true);
-}
-
-%javamethodmodifiers vector() "private";
-
-%proxycode %{
-  public $javaclassname(ExprManager em, $typemap(jstype, CTYPE)[] initialElements) {
-    this(em);
-    reserve(initialElements.length);
-
-    for ($typemap(jstype, CTYPE) element : initialElements) {
-      add(element);
-    }
-  }
-
-  public $javaclassname(ExprManager em, Iterable<$typemap(jstype, CTYPE)> initialElements) {
-    this(em);
-    for ($typemap(jstype, CTYPE) element : initialElements) {
-      add(element);
-    }
-  }
-
-  public $typemap(jstype, CTYPE) get(int index) {
-    return doGet(index);
-  }
-
-  public $typemap(jstype, CTYPE) set(int index, $typemap(jstype, CTYPE) e) {
-    return doSet(index, e);
-  }
-
-  public boolean add($typemap(jstype, CTYPE) e) {
-    modCount++;
-    doAdd(e);
-    return true;
-  }
-
-  public void add(int index, $typemap(jstype, CTYPE) e) {
-    modCount++;
-    doAdd(index, e);
-  }
-
-  public $typemap(jstype, CTYPE) remove(int index) {
-    modCount++;
-    return doRemove(index);
-  }
-
-  protected void removeRange(int fromIndex, int toIndex) {
-    modCount++;
-    doRemoveRange(fromIndex, toIndex);
-  }
-
-  public int size() {
-    return doSize();
-  }
-%}
-
-  public:
-    typedef size_t size_type;
-    typedef ptrdiff_t difference_type;
-    typedef CTYPE value_type;
-    typedef CTYPE *pointer;
-    typedef CTYPE const *const_pointer;
-    typedef CTYPE &reference;
-    typedef CONST_REFERENCE const_reference;
-
-    vector();
-    size_type capacity() const;
-    void reserve(size_type n) throw (std::length_error);
-    %rename(isEmpty) empty;
-    bool empty() const;
-    void clear();
-    %extend {
-      %fragment("SWIG_VectorSize");
-
-      vector(jint count, const CTYPE &value) throw (std::out_of_range) {
-        if (count < 0)
-          throw std::out_of_range("vector count must be positive");
-        return new std::vector< CTYPE >(static_cast<std::vector< CTYPE >::size_type>(count), value);
-      }
-
-      jint doSize() const throw (std::out_of_range) {
-        return SWIG_VectorSize(self->size());
-      }
-
-      void doAdd(const value_type& x) {
-        self->push_back(x);
-      }
-
-      void doAdd(jint index, const value_type& x) throw (std::out_of_range) {
-        jint size = static_cast<jint>(self->size());
-        if (0 <= index && index <= size) {
-          self->insert(self->begin() + index, x);
-        } else {
-          throw std::out_of_range("vector index out of range");
-        }
-      }
-
-      value_type doRemove(jint index) throw (std::out_of_range) {
-        jint size = static_cast<jint>(self->size());
-        if (0 <= index && index < size) {
-          CTYPE const old_value = (*self)[index];
-          self->erase(self->begin() + index);
-          return old_value;
-        } else {
-          throw std::out_of_range("vector index out of range");
-        }
-      }
-
-      CONST_REFERENCE doGet(jint index) throw (std::out_of_range) {
-        jint size = static_cast<jint>(self->size());
-        if (index >= 0 && index < size)
-          return (*self)[index];
-        else
-          throw std::out_of_range("vector index out of range");
-      }
-
-      value_type doSet(jint index, const value_type& val) throw (std::out_of_range) {
-        jint size = static_cast<jint>(self->size());
-        if (index >= 0 && index < size) {
-          CTYPE const old_value = (*self)[index];
-          (*self)[index] = val;
-          return old_value;
-        }
-        else
-          throw std::out_of_range("vector index out of range");
-      }
-
-      void doRemoveRange(jint fromIndex, jint toIndex) throw (std::out_of_range) {
-        jint size = static_cast<jint>(self->size());
-        if (0 <= fromIndex && fromIndex <= toIndex && toIndex <= size) {
-          self->erase(self->begin() + fromIndex, self->begin() + toIndex);
-        } else {
-          throw std::out_of_range("vector index out of range");
-        }
-      }
-    }
-  };
-}
-
-// Workaround for https://github.com/swig/swig/commit/63a5a8af88271559a7b170794b4c61c30b8934ea
-%typemap(javaconstruct) vector<CTYPE> {
-  this(null, $imcall, true);
-}
-
-%enddef
diff --git a/src/bindings/java_iterator_adapter.h b/src/bindings/java_iterator_adapter.h
deleted file mode 100644
index 864619004..000000000
--- a/src/bindings/java_iterator_adapter.h
+++ /dev/null
@@ -1,67 +0,0 @@
-/*********************                                                        */
-/*! \file java_iterator_adapter.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Andres Noetzli, Morgan Deters, Mathias Preiner
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 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 An iterator adapter for the Java bindings, giving Java iterators
- ** the ability to access elements from STL iterators.
- **
- ** An iterator adapter for the Java bindings, giving Java iterators the
- ** ability to access elements from STL iterators.  This class is mapped
- ** into Java by SWIG, where it implements Iterator (some additional
- ** Java-side functions are added by the SWIG layer to implement the full
- ** interface).
- **
- ** The functionality requires significant assistance from the ".i" SWIG
- ** interface files, applying a variety of typemaps.
- **/
-
-// private to the bindings layer
-#ifndef SWIGJAVA
-#  error This should only be included from the Java bindings layer.
-#endif /* SWIGJAVA */
-
-#ifndef CVC4__BINDINGS__JAVA_ITERATOR_ADAPTER_H
-#define CVC4__BINDINGS__JAVA_ITERATOR_ADAPTER_H
-
-#include <type_traits>
-
-namespace CVC4 {
-
-template <class T, class value_type>
-class JavaIteratorAdapter
-{
- public:
-  JavaIteratorAdapter(const T& t) : d_t(t), d_it(d_t.begin())
-  {
-    static_assert(
-        std::is_convertible<typename T::const_iterator::value_type,
-                            value_type>(),
-        "value_type must be convertible from T::const_iterator::value_type");
-  }
-
-  JavaIteratorAdapter() = delete;
-
-  bool hasNext() { return d_it != d_t.end(); }
-
-  value_type getNext()
-  {
-    value_type ret = *d_it;
-    ++d_it;
-    return ret;
-  }
-
- private:
-  const T& d_t;
-  typename T::const_iterator d_it;
-}; /* class JavaIteratorAdapter<T, value_type> */
-
-}  // namespace CVC4
-
-#endif /* CVC4__BINDINGS__JAVA_ITERATOR_ADAPTER_H */
diff --git a/src/bindings/java_iterator_adapter.i b/src/bindings/java_iterator_adapter.i
deleted file mode 100644
index 5f814edd7..000000000
--- a/src/bindings/java_iterator_adapter.i
+++ /dev/null
@@ -1,75 +0,0 @@
-%{
-#include "bindings/java_iterator_adapter.h"
-%}
-
-#ifdef SWIGJAVA
-
-%define SWIG_JAVA_ITERATOR_ADAPTER(TTYPE, VTYPE)
-
-%typemap(javabody) CVC4::JavaIteratorAdapter %{
-  private long swigCPtr;
-  protected boolean swigCMemOwn;
-  private ExprManager em;
-
-  protected $javaclassname(ExprManager em, long cPtr, boolean cMemoryOwn) {
-    swigCMemOwn = cMemoryOwn;
-    swigCPtr = cPtr;
-    this.em = em;
-  }
-
-  public $javaclassname(ExprManager em, $typemap(jstype, TTYPE) t) {
-    this(t);
-    this.em = em;
-  }
-
-  protected static long getCPtr($javaclassname obj) {
-    return (obj == null) ? 0 : obj.swigCPtr;
-  }
-%}
-
-// Workaround for https://github.com/swig/swig/commit/63a5a8af88271559a7b170794b4c61c30b8934ea
-%typemap(javaconstruct) JavaIteratorAdapter<TTYPE, VTYPE> {
-  this(null, $imcall, true);
-}
-
-%typemap(javaconstruct) CVC4::JavaIteratorAdapter<TTYPE, VTYPE> {
-  this(null, $imcall, true);
-}
-
-%feature("valuewrapper") CVC4::JavaIteratorAdapter<TTYPE, VTYPE>;
-
-// the JavaIteratorAdapter should not be public, and implements Iterator
-%typemap(javaclassmodifiers) CVC4::JavaIteratorAdapter<TTYPE, VTYPE> "class";
-%typemap(javainterfaces) CVC4::JavaIteratorAdapter< TTYPE, VTYPE > "java.util.Iterator<$typemap(jstype, VTYPE)>";
-
-// add some functions to the Java side (do it here because there's no way to do these in C++)
-%typemap(javacode) CVC4::JavaIteratorAdapter<TTYPE, VTYPE> "
-  public void remove() {
-    throw new java.lang.UnsupportedOperationException();
-  }
-
-  public $typemap(jstype, VTYPE) next() {
-    if(hasNext()) {
-      return getNext();
-    } else {
-      throw new java.util.NoSuchElementException();
-    }
-  }
-"
-
-// getNext() just allows C++ iterator access from Java-side next(), make it private
-%javamethodmodifiers CVC4::JavaIteratorAdapter<TTYPE, VTYPE>::getNext() "private";
-
-%javamethodmodifiers CVC4::JavaIteratorAdapter<TTYPE, VTYPE>::JavaIteratorAdapter(const TTYPE& t) "private";
-
-%enddef
-
-%include "bindings/java_iterator_adapter.h"
-
-namespace CVC4 {
-  template<class T, class V> class JavaIteratorAdapter {
-    SWIG_JAVA_ITERATOR_ADAPTER(T, V)
-  };
-}
-
-#endif
diff --git a/src/bindings/java_stream_adapters.h b/src/bindings/java_stream_adapters.h
deleted file mode 100644
index 2f3c8093f..000000000
--- a/src/bindings/java_stream_adapters.h
+++ /dev/null
@@ -1,108 +0,0 @@
-/*********************                                                        */
-/*! \file java_stream_adapters.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Morgan Deters, Mathias Preiner
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 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 An OutputStream adapter for the Java bindings
- **
- ** An OutputStream adapter for the Java bindings.  This works with a lot
- ** of help from SWIG, and custom typemaps in the ".i" SWIG interface files
- ** for CVC4.  The basic idea is that, when a CVC4 function with a
- ** std::ostream& parameter is called, a Java-side binding is generated
- ** taking a java.io.OutputStream.  Now, the problem is that std::ostream
- ** has no Java equivalent, and java.io.OutputStream has no C++ equivalent,
- ** so we use this class (which exists on both sides) as the go-between.
- ** The wrapper connecting the Java function (taking an OutputStream) and
- ** the C++ function (taking an ostream) creates a JavaOutputStreamAdapter,
- ** and call the C++ function with the stringstream inside.  After the call,
- ** the generated stream material is collected and output to the Java-side
- ** OutputStream.
- **/
-
-// private to the bindings layer
-#ifndef SWIGJAVA
-#  error This should only be included from the Java bindings layer.
-#endif /* SWIGJAVA */
-
-#include <sstream>
-#include <set>
-#include <cassert>
-#include <iosfwd>
-#include <string>
-#include <jni.h>
-
-#ifndef CVC4__BINDINGS__JAVA_STREAM_ADAPTERS_H
-#define CVC4__BINDINGS__JAVA_STREAM_ADAPTERS_H
-
-namespace CVC4 {
-
-class JavaOutputStreamAdapter : public std::ostringstream {
-public:
-  std::string toString() { return str(); }
-};/* class JavaOutputStreamAdapter */
-
-class JavaInputStreamAdapter : public std::stringstream {
-  static std::set<JavaInputStreamAdapter*> s_adapters;
-  jobject inputStream;
-
-  JavaInputStreamAdapter& operator=(const JavaInputStreamAdapter&);
-  JavaInputStreamAdapter(const JavaInputStreamAdapter&);
-
-public:
-  JavaInputStreamAdapter(jobject inputStream) : inputStream(inputStream) {
-    s_adapters.insert(this);
-  }
-
-  ~JavaInputStreamAdapter() {
-    s_adapters.erase(this);
-  }
-
-  static void pullAdapters(JNIEnv* jenv) {
-    for(std::set<JavaInputStreamAdapter*>::iterator i = s_adapters.begin();
-        i != s_adapters.end();
-        ++i) {
-      (*i)->pull(jenv);
-    }
-  }
-
-  jobject getInputStream() const {
-    return inputStream;
-  }
-
-  void pull(JNIEnv* jenv) {
-    if(fail() || eof()) {
-      clear();
-    }
-    jclass clazz = jenv->FindClass("java/io/InputStream");
-    assert(clazz != NULL && jenv->ExceptionOccurred() == NULL);
-    jmethodID method = jenv->GetMethodID(clazz, "available", "()I");
-    assert(method != NULL && jenv->ExceptionOccurred() == NULL);
-    jint available = jenv->CallIntMethod(inputStream, method);
-    assert(jenv->ExceptionOccurred() == NULL);
-    jbyteArray bytes = jenv->NewByteArray(available);
-    assert(bytes != NULL && jenv->ExceptionOccurred() == NULL);
-    method = jenv->GetMethodID(clazz, "read", "([B)I");
-    assert(method != NULL && jenv->ExceptionOccurred() == NULL);
-    jint nread = jenv->CallIntMethod(inputStream, method, bytes);
-    assert(jenv->ExceptionOccurred() == NULL);
-    jbyte* bptr = jenv->GetByteArrayElements(bytes, NULL);
-    assert(jenv->ExceptionOccurred() == NULL);
-    std::copy(bptr, bptr + nread, std::ostream_iterator<char>(*this));
-    *this << std::flush;
-    jenv->ReleaseByteArrayElements(bytes, bptr, 0);
-    assert(jenv->ExceptionOccurred() == NULL);
-    assert(good());
-    assert(!eof());
-  }
-
-};/* class JavaInputStreamAdapter */
-
-}/* CVC4 namespace */
-
-#endif /* CVC4__BINDINGS__JAVA_STREAM_ADAPTERS_H */
diff --git a/src/bindings/python/CMakeLists.txt b/src/bindings/python/CMakeLists.txt
deleted file mode 100644
index d03924680..000000000
--- a/src/bindings/python/CMakeLists.txt
+++ /dev/null
@@ -1,43 +0,0 @@
-# Make sure that interpreter and libraries have a compatible version.
-# Note: We use the Python interpreter to determine the install path for Python
-# modules.  If the interpreter and library have different versions, the module
-# will be installed for the wrong Python version. Hence, we require the library
-# version to match the Python interpreter's version.
-find_package(PythonLibs
-             ${PYTHON_VERSION_MAJOR}.${PYTHON_VERSION_MINOR} REQUIRED)
-include_directories(${PYTHON_INCLUDE_DIRS})
-
-set(SWIG_MODULE_CVC4_EXTRA_DEPS cvc4 cvc4parser)
-set_property(SOURCE ${CVC4_SWIG_INTERFACE} PROPERTY CPLUSPLUS ON)
-
-# Suppress -Wsuggest-override warnings for generated code
-set_property(
-  SOURCE ${CMAKE_CURRENT_BINARY_DIR}/cvc4PYTHON_wrap.cxx
-  PROPERTY COMPILE_OPTIONS -Wno-suggest-override)
-
-# The generated module should have the name _CVC4.so, hence we use CVC4 as
-# target name.
-if(${CMAKE_VERSION} VERSION_LESS "3.8.0")
-  swig_add_module(CVC4 Python ${CVC4_SWIG_INTERFACE})
-else()
-  swig_add_library(CVC4 LANGUAGE Python SOURCES ${CVC4_SWIG_INTERFACE})
-endif()
-swig_link_libraries(CVC4 cvc4 cvc4parser ${PYTHON_LIBRARIES})
-
-
-# Install Python bindings to the corresponding python-*/site-packages
-# directory.  Lookup Python module directory and store path in
-# PYTHON_MODULE_PATH.
-execute_process(COMMAND
-                  ${PYTHON_EXECUTABLE} -c
-                    "from distutils.sysconfig import get_python_lib;\
-                     print(get_python_lib(plat_specific=True,\
-                             prefix='${CMAKE_INSTALL_PREFIX}'))"
-                OUTPUT_VARIABLE PYTHON_MODULE_PATH
-                OUTPUT_STRIP_TRAILING_WHITESPACE)
-
-# Copy _CVC4.so and CVC4.py to PYTHON_MODULE_PATH
-install(TARGETS ${SWIG_MODULE_CVC4_REAL_NAME}
-        DESTINATION ${PYTHON_MODULE_PATH})
-install(FILES ${CMAKE_CURRENT_BINARY_DIR}/CVC4.py
-        DESTINATION ${PYTHON_MODULE_PATH})
diff --git a/src/bindings/swig.h b/src/bindings/swig.h
deleted file mode 100644
index ed401ad18..000000000
--- a/src/bindings/swig.h
+++ /dev/null
@@ -1,33 +0,0 @@
-/*********************                                                        */
-/*! \file swig.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Morgan Deters, Mathias Preiner, Andres Noetzli
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 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 Common swig checks and definitions
- **
- ** Common swig checks and definitions, when generating swig interfaces.
- **/
-
-#ifndef CVC4__BINDINGS__SWIG_H
-#define CVC4__BINDINGS__SWIG_H
-
-#ifndef SWIG
-#  error This file should only be included when generating swig interfaces.
-#endif /* SWIG */
-
-#if !defined(SWIG_VERSION) || SWIG_VERSION < 0x030000
-#  error CVC4 bindings require swig version 3.0.0 or later, sorry.
-#endif /* SWIG_VERSION */
-
-%import "cvc4_public.h"
-
-// swig doesn't like GCC attributes
-#define __attribute__(x)
-
-#endif /* CVC4__BINDINGS__SWIG_H */