Improve memory management in Java bindings (#4629)

Fixes #2846. One of the challenges of the Java bindings is that the
garbage collector can delete unused objects at any time in any order.
This is an issue with CVC4's API because we require all `Expr`s to be
deleted before the corresponding `ExprManager`. In the past, we were
using `NewGlobalRef`/`DeleteGlobalRef` on the wrapper object of
`ExprManager`. The problem is that we can have multiple instances of the
wrapper that internally all refer to the same `ExprManager`. This commit
implements a different approach where the Java wrappers hold an explicit
reference to the `ExprManager`. The commit also removes some unused or
unimportant API bits from the bindings.

20 files changed, 1291 insertions, 385 deletions

diff --git a/src/bindings/java/CMakeLists.txt b/src/bindings/java/CMakeLists.txt
index 4e1b96af9..8e919db86 100644
--- a/src/bindings/java/CMakeLists.txt
+++ b/src/bindings/java/CMakeLists.txt
@@ -97,7 +97,6 @@ set(gen_java_files
   ${CMAKE_CURRENT_BINARY_DIR}/LastExceptionBuffer.java
   ${CMAKE_CURRENT_BINARY_DIR}/LogicException.java
   ${CMAKE_CURRENT_BINARY_DIR}/LogicInfo.java
-  ${CMAKE_CURRENT_BINARY_DIR}/Map_ExprExpr.java
   ${CMAKE_CURRENT_BINARY_DIR}/ModalException.java
   ${CMAKE_CURRENT_BINARY_DIR}/OptionException.java
   ${CMAKE_CURRENT_BINARY_DIR}/Options.java
@@ -107,10 +106,6 @@ set(gen_java_files
   ${CMAKE_CURRENT_BINARY_DIR}/Rational.java
   ${CMAKE_CURRENT_BINARY_DIR}/RationalHashFunction.java
   ${CMAKE_CURRENT_BINARY_DIR}/RealType.java
-  ${CMAKE_CURRENT_BINARY_DIR}/Record.java
-  ${CMAKE_CURRENT_BINARY_DIR}/RecordHashFunction.java
-  ${CMAKE_CURRENT_BINARY_DIR}/RecordUpdate.java
-  ${CMAKE_CURRENT_BINARY_DIR}/RecordUpdateHashFunction.java
   ${CMAKE_CURRENT_BINARY_DIR}/RecoverableModalException.java
   ${CMAKE_CURRENT_BINARY_DIR}/RegExpLoop.java
   ${CMAKE_CURRENT_BINARY_DIR}/RegExpRepeat.java
@@ -122,19 +117,14 @@ set(gen_java_files
   ${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__Printer.java
   ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_CVC4__options__InstFormatMode.java
-  ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_Listener.java
-  ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_ListenerCollection__Registration.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__unordered_mapT_CVC4__Expr_CVC4__ProofLetCount_CVC4__ExprHashFunction_t.java
   ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_std__vectorT_CVC4__DatatypeConstructorArg_t.java
-  ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_std__vectorT_CVC4__DatatypeConstructor_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
@@ -147,7 +137,6 @@ set(gen_java_files
   ${CMAKE_CURRENT_BINARY_DIR}/Statistics.java
   ${CMAKE_CURRENT_BINARY_DIR}/StatisticsBase.java
   ${CMAKE_CURRENT_BINARY_DIR}/StringType.java
-  ${CMAKE_CURRENT_BINARY_DIR}/SygusPrintCallback.java
   ${CMAKE_CURRENT_BINARY_DIR}/TesterType.java
   ${CMAKE_CURRENT_BINARY_DIR}/TheoryId.java
   ${CMAKE_CURRENT_BINARY_DIR}/TupleUpdate.java
@@ -163,13 +152,10 @@ set(gen_java_files
   ${CMAKE_CURRENT_BINARY_DIR}/UnsafeInterruptException.java
   ${CMAKE_CURRENT_BINARY_DIR}/UnsatCore.java
   ${CMAKE_CURRENT_BINARY_DIR}/VariableTypeMap.java
-  ${CMAKE_CURRENT_BINARY_DIR}/hashmapExpr.java
-  ${CMAKE_CURRENT_BINARY_DIR}/pairStringType.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}/vectorPairStringType.java
   ${CMAKE_CURRENT_BINARY_DIR}/vectorSExpr.java
   ${CMAKE_CURRENT_BINARY_DIR}/vectorString.java
   ${CMAKE_CURRENT_BINARY_DIR}/vectorType.java
diff --git a/src/bindings/java/cvc4_std_vector.i b/src/bindings/java/cvc4_std_vector.i
new file mode 100644
index 000000000..e032426a0
--- /dev/null
+++ b/src/bindings/java/cvc4_std_vector.i
@@ -0,0 +1,206 @@
+/**
+ * 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
index a4966debf..864619004 100644
--- a/src/bindings/java_iterator_adapter.h
+++ b/src/bindings/java_iterator_adapter.h
@@ -46,6 +46,8 @@ class JavaIteratorAdapter
         "value_type must be convertible from T::const_iterator::value_type");
   }
 
+  JavaIteratorAdapter() = delete;
+
   bool hasNext() { return d_it != d_t.end(); }
 
   value_type getNext()
diff --git a/src/bindings/java_iterator_adapter.i b/src/bindings/java_iterator_adapter.i
new file mode 100644
index 000000000..5f814edd7
--- /dev/null
+++ b/src/bindings/java_iterator_adapter.i
@@ -0,0 +1,75 @@
+%{
+#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/cvc4.i b/src/cvc4.i
index 32bdd0887..f62611e8f 100644
--- a/src/cvc4.i
+++ b/src/cvc4.i
@@ -58,17 +58,10 @@ std::set<JavaInputStreamAdapter*> CVC4::JavaInputStreamAdapter::s_adapters;
 %}
 #endif /* SWIGPYTHON */
 
-%template(vectorType) std::vector< CVC4::Type >;
-%template(vectorExpr) std::vector< CVC4::Expr >;
 %template(vectorUnsignedInt) std::vector< unsigned int >;
-%template(vectorVectorExpr) std::vector< std::vector< CVC4::Expr > >;
-%template(vectorDatatypeType) std::vector< CVC4::DatatypeType >;
 %template(vectorSExpr) std::vector< CVC4::SExpr >;
 %template(vectorString) std::vector< std::string >;
-%template(vectorPairStringType) std::vector< std::pair< std::string, CVC4::Type > >;
-%template(pairStringType) std::pair< std::string, CVC4::Type >;
 %template(setOfType) std::set< CVC4::Type >;
-%template(hashmapExpr) std::unordered_map< CVC4::Expr, CVC4::Expr, CVC4::ExprHashFunction >;
 
 // This is unfortunate, but seems to be necessary; if we leave NULL
 // defined, swig will expand it to "(void*) 0", and some of swig's
@@ -77,9 +70,6 @@ std::set<JavaInputStreamAdapter*> CVC4::JavaInputStreamAdapter::s_adapters;
 
 #ifdef SWIGJAVA
 
-#include "bindings/java_iterator_adapter.h"
-#include "bindings/java_stream_adapters.h"
-
 // Map C++ exceptions of type CVC4::Exception to Java exceptions of type
 // edu.stanford.CVC4.Exception
 // 
@@ -92,6 +82,7 @@ std::set<JavaInputStreamAdapter*> CVC4::JavaInputStreamAdapter::s_adapters;
   return $null;
 }
 
+%include "bindings/java_iterator_adapter.i"
 %include "java/typemaps.i" // primitive pointers and references
 %include "java/std_string.i" // map std::string to java.lang.String
 %include "java/arrays_java.i" // C arrays to Java arrays
@@ -197,6 +188,8 @@ std::set<JavaInputStreamAdapter*> CVC4::JavaInputStreamAdapter::s_adapters;
   JCALL3(ReleaseByteArrayElements, jenv, ba, bae, 0);
 }
 
+%include "bindings/java_stream_adapters.h"
+
 #endif /* SWIGJAVA */
 
 // TIM:
@@ -232,8 +225,6 @@ std::set<JavaInputStreamAdapter*> CVC4::JavaInputStreamAdapter::s_adapters;
 %include "expr/ascription_type.i"
 %include "expr/emptyset.i"
 %include "expr/expr_sequence.i"
-%include "expr/datatype.i"
-%include "expr/record.i"
 %include "proof/unsat_core.i"
 
 // TIM:
@@ -245,6 +236,7 @@ std::set<JavaInputStreamAdapter*> CVC4::JavaInputStreamAdapter::s_adapters;
 
 // TIM:
 // The remainder of the includes:
+%include "expr/datatype.i"
 %include "expr/expr.i"
 %include "expr/expr_manager.i"
 %include "expr/variable_type_map.i"
@@ -254,5 +246,7 @@ std::set<JavaInputStreamAdapter*> CVC4::JavaInputStreamAdapter::s_adapters;
 %include "theory/logic_info.i"
 %include "theory/theory_id.i"
 
+%include "expr/array_store_all.i"
+
 // Tim: This should come after "theory/logic_info.i".
 %include "smt/smt_engine.i"
diff --git a/src/expr/array_store_all.i b/src/expr/array_store_all.i
index b66e4a178..5158a21d9 100644
--- a/src/expr/array_store_all.i
+++ b/src/expr/array_store_all.i
@@ -2,15 +2,63 @@
 #include "expr/array_store_all.h"
 %}
 
+#ifdef SWIGJAVA
+
+%typemap(javabody) CVC4::ArrayStoreAll %{
+  private long swigCPtr;
+  protected boolean swigCMemOwn;
+  private ExprManager em;
+
+  protected $javaclassname(ExprManager em, long cPtr, boolean cMemoryOwn) {
+    swigCMemOwn = cMemoryOwn;
+    swigCPtr = cPtr;
+    this.em = em;
+  }
+
+  protected static long getCPtr($javaclassname obj) {
+    return (obj == null) ? 0 : obj.swigCPtr;
+  }
+
+  public $javaclassname(ExprManager em, ArrayType type, Expr expr) {
+    this(type, expr);
+    this.em = em;
+  }
+%}
+
+// Workaround for https://github.com/swig/swig/commit/63a5a8af88271559a7b170794b4c61c30b8934ea
+%typemap(javaconstruct) ArrayStoreAll {
+  this(null, $imcall, true);
+}
+
+%typemap(javaconstruct) CVC4::ArrayStoreAll {
+  this(null, $imcall, true);
+}
+
+%typemap(javaout) const CVC4::Expr& {
+  return new Expr(this.em, $jnicall, false);
+}
+
+%typemap(javaout) const CVC4::ArrayType& {
+  return new ArrayType(this.em, $jnicall, false);
+}
+
+%typemap(javaout) const CVC4::ArrayStoreAll& {
+  return new ArrayStoreAll(this.em, $jnicall, false);
+}
+
+%javamethodmodifiers CVC4::ArrayStoreAll::ArrayStoreAll(const ArrayType& type, const Expr& expr) "private";
+
+#endif /* SWIGJAVA */
+
+%ignore CVC4::ArrayStoreAll::ArrayStoreAll(const ArrayStoreAll& other);
 %rename(equals) CVC4::ArrayStoreAll::operator==(const ArrayStoreAll&) const;
 %ignore CVC4::ArrayStoreAll::operator!=(const ArrayStoreAll&) const;
+%ignore CVC4::ArrayStoreAll::operator=(const ArrayStoreAll&);
 %rename(less) CVC4::ArrayStoreAll::operator<(const ArrayStoreAll&) const;
 %rename(lessEqual) CVC4::ArrayStoreAll::operator<=(const ArrayStoreAll&) const;
 %rename(greater) CVC4::ArrayStoreAll::operator>(const ArrayStoreAll&) const;
 %rename(greaterEqual) CVC4::ArrayStoreAll::operator>=(const ArrayStoreAll&) const;
-
 %rename(apply) CVC4::ArrayStoreAllHashFunction::operator()(const ArrayStoreAll&) const;
-
 %ignore CVC4::operator<<(std::ostream&, const ArrayStoreAll&);
 
 %include "expr/type.i"
diff --git a/src/expr/ascription_type.i b/src/expr/ascription_type.i
index 57d8f97fe..c2499c00e 100644
--- a/src/expr/ascription_type.i
+++ b/src/expr/ascription_type.i
@@ -2,6 +2,42 @@
 #include "expr/ascription_type.h"
 %}
 
+#ifdef SWIGJAVA
+
+%typemap(javabody) CVC4::AscriptionType %{
+  private long swigCPtr;
+  protected boolean swigCMemOwn;
+  private ExprManager em;
+
+  protected $javaclassname(ExprManager em, long cPtr, boolean cMemoryOwn) {
+    swigCMemOwn = cMemoryOwn;
+    swigCPtr = cPtr;
+    this.em = em; // keep ref to em in SWIG proxy class
+  }
+
+  protected static long getCPtr($javaclassname obj) {
+    return (obj == null) ? 0 : obj.swigCPtr;
+  }
+
+  public $javaclassname(ExprManager em, Type t) {
+    this(t);
+    this.em = em;
+  }
+%}
+
+// Workaround for https://github.com/swig/swig/commit/63a5a8af88271559a7b170794b4c61c30b8934ea
+%typemap(javaconstruct) AscriptionType {
+  this(null, $imcall, true);
+}
+
+%typemap(javaconstruct) CVC4::AscriptionType {
+  this(null, $imcall, true);
+}
+
+%javamethodmodifiers CVC4::AscriptionType::AscriptionType(Type t) "private";
+
+#endif
+
 %rename(equals) CVC4::AscriptionType::operator==(const AscriptionType&) const;
 %ignore CVC4::AscriptionType::operator!=(const AscriptionType&) const;
 
diff --git a/src/expr/datatype.i b/src/expr/datatype.i
index 1ac89efcb..56dd6dad4 100644
--- a/src/expr/datatype.i
+++ b/src/expr/datatype.i
@@ -1,93 +1,183 @@
 %{
 #include "expr/datatype.h"
-
-#ifdef SWIGJAVA
-
-#include "bindings/java_iterator_adapter.h"
-#include "bindings/java_stream_adapters.h"
-
-#endif /* SWIGJAVA */
 %}
 
-%include "expr/kind.i"
-
-%extend std::vector< CVC4::Datatype > {
-  %ignore vector(size_type);// java/python/perl/others?
-  %ignore resize(size_type);// java/python/perl/others?
-  %ignore set(int i, const CVC4::Datatype& x);
-  %ignore to_array();
-};
-%template(vectorDatatype) std::vector< CVC4::Datatype >;
-
-%extend std::vector< CVC4::DatatypeConstructor > {
-  %ignore vector(size_type);// java/python/perl/others?
-  %ignore resize(size_type);// java/python/perl/others?
-  %ignore set(int i, const CVC4::Datatype::Constructor& x);
-  %ignore to_array();
-};
-//%template(vectorDatatypeConstructor) std::vector< CVC4::DatatypeConstructor >;
-
-%rename(equals) CVC4::Datatype::operator==(const Datatype&) const;
+%ignore CVC4::Datatype::setRecord();
+%ignore CVC4::Datatype::isRecord() const;
+%ignore CVC4::Datatype::getRecord() const;
 %ignore CVC4::Datatype::operator!=(const Datatype&) const;
-
 %ignore CVC4::Datatype::begin();
 %ignore CVC4::Datatype::end();
 %ignore CVC4::Datatype::begin() const;
 %ignore CVC4::Datatype::end() const;
-
+%ignore CVC4::Datatype::getConstructors() const;
+%rename(equals) CVC4::Datatype::operator==(const Datatype&) const;
 %rename(get) CVC4::Datatype::operator[](size_t) const;
 %rename(get) CVC4::Datatype::operator[](std::string) const;
 
+%ignore CVC4::SygusPrintCallback;
+
 %rename(apply) CVC4::DatatypeHashFunction::operator()(const Datatype&) const;
 %ignore CVC4::DatatypeHashFunction::operator()(const Datatype*) const;
 %rename(apply) CVC4::DatatypeHashFunction::operator()(const DatatypeConstructor&) const;
 %ignore CVC4::DatatypeHashFunction::operator()(const DatatypeConstructor*) const;
 
+%ignore CVC4::DatatypeConstructor::DatatypeConstructor();
 %ignore CVC4::DatatypeConstructor::begin();
 %ignore CVC4::DatatypeConstructor::end();
 %ignore CVC4::DatatypeConstructor::begin() const;
 %ignore CVC4::DatatypeConstructor::end() const;
-
 %rename(get) CVC4::DatatypeConstructor::operator[](size_t) const;
 %rename(get) CVC4::DatatypeConstructor::operator[](std::string) const;
 
 %ignore CVC4::operator<<(std::ostream&, const Datatype&);
 %ignore CVC4::operator<<(std::ostream&, const DatatypeConstructor&);
 %ignore CVC4::operator<<(std::ostream&, const DatatypeConstructorArg&);
+%ignore CVC4::operator<<(std::ostream& out, const DatatypeIndexConstant& es);
 
 %ignore CVC4::DatatypeConstructorIterator;
 %ignore CVC4::DatatypeConstructorArgIterator;
 
-%feature("valuewrapper") CVC4::DatatypeUnresolvedType;
-%feature("valuewrapper") CVC4::DatatypeConstructor;
-
-
-%rename(equals) CVC4::DatatypeIndexConstant::operator==(const DatatypeIndexConstant&) const;
 %ignore CVC4::DatatypeIndexConstant::operator!=(const DatatypeIndexConstant&) const;
-
+%rename(equals) CVC4::DatatypeIndexConstant::operator==(const DatatypeIndexConstant&) const;
 %rename(less) CVC4::DatatypeIndexConstant::operator<(const DatatypeIndexConstant&) const;
 %rename(lessEqual) CVC4::DatatypeIndexConstant::operator<=(const DatatypeIndexConstant&) const;
 %rename(greater) CVC4::DatatypeIndexConstant::operator>(const DatatypeIndexConstant&) const;
 %rename(greaterEqual) CVC4::DatatypeIndexConstant::operator>=(const DatatypeIndexConstant&) const;
-
 %rename(apply) CVC4::DatatypeIndexConstantFunction::operator()(const DatatypeIndexConstant&) const;
 
-%ignore CVC4::operator<<(std::ostream& out, const DatatypeIndexConstant& es);
+#ifdef SWIGJAVA
 
+%typemap(javaout) CVC4::Expr {
+  return new Expr(this.em, $jnicall, true);
+}
 
-#ifdef SWIGJAVA
+%typemap(javaout) CVC4::DatatypeType {
+  return new DatatypeType(this.em, $jnicall, true);
+}
+
+%typemap(javabody) CVC4::Datatype %{
+  private long swigCPtr;
+  protected boolean swigCMemOwn;
+  private ExprManager em;
+
+  protected $javaclassname(ExprManager em, long cPtr, boolean cMemoryOwn) {
+    swigCMemOwn = cMemoryOwn;
+    swigCPtr = cPtr;
+    this.em = em;
+  }
+
+  protected static long getCPtr($javaclassname obj) {
+    return (obj == null) ? 0 : obj.swigCPtr;
+  }
+
+  public static $javaclassname datatypeOf(Expr item) throws edu.stanford.CVC4.Exception {
+    $javaclassname result = datatypeOfInternal(item);
+    result.em = item.getExprManager();
+    return result;
+  }
+
+  public JavaIteratorAdapter_Datatype iterator() {
+    return new JavaIteratorAdapter_Datatype(this.em, this);
+  }
+%}
+
+%javamethodmodifiers CVC4::Datatype::datatypeOf(Expr item) "private";
+%rename(datatypeOfInternal) CVC4::Datatype::datatypeOf(Expr item);
+
+%include "bindings/java/cvc4_std_vector.i"
+
+SWIG_STD_VECTOR_EM(CVC4::Datatype, const CVC4::Datatype&)
 
-// Instead of Datatype::begin() and end(), create an
-// iterator() method on the Java side that returns a Java-style
-// Iterator.
 %extend CVC4::Datatype {
-  CVC4::JavaIteratorAdapter<CVC4::Datatype, CVC4::DatatypeConstructor>
-  iterator()
-  {
-    return CVC4::JavaIteratorAdapter<CVC4::Datatype, CVC4::DatatypeConstructor>(
-        *$self);
+%typemap(javaout) const CVC4::Datatype& {
+  return new Datatype(null, $jnicall, false);
+}
+}
+
+%typemap(javaout) CVC4::Datatype {
+  return new Datatype(this.em, $jnicall, true);
+}
+%typemap(javaout) const CVC4::Datatype& {
+  return new Datatype(this.em, $jnicall, false);
+}
+%template(vectorDatatype) std::vector<CVC4::Datatype>;
+
+%typemap(javaout) typeVector {
+  return new typeVector(this.em, $jnicall, true);
+}
+
+%typemap(javaout) const CVC4::DatatypeConstructor& {
+  return new DatatypeConstructor(this.em, $jnicall, false);
+}
+
+%typemap(javabody) CVC4::DatatypeConstructor %{
+  private long swigCPtr;
+  protected boolean swigCMemOwn;
+  private ExprManager em;
+
+  protected $javaclassname(ExprManager em, long cPtr, boolean cMemoryOwn) {
+    swigCMemOwn = cMemoryOwn;
+    swigCPtr = cPtr;
+    this.em = em;
+  }
+
+  protected static long getCPtr($javaclassname obj) {
+    return (obj == null) ? 0 : obj.swigCPtr;
+  }
+
+  public DatatypeConstructor(ExprManager em, String name) {
+    this(name);
+    this.em = em;
+  }
+
+  public DatatypeConstructor(ExprManager em, String name, long weight) {
+    this(name, weight);
+    this.em = em;
+  }
+
+  public JavaIteratorAdapter_DatatypeConstructor iterator() {
+    return new JavaIteratorAdapter_DatatypeConstructor(this.em, this);
+  }
+%}
+
+// Workaround for https://github.com/swig/swig/commit/63a5a8af88271559a7b170794b4c61c30b8934ea
+%typemap(javaconstruct) DatatypeConstructor {
+  this(null, $imcall, true);
+}
+
+%typemap(javaconstruct) CVC4::DatatypeConstructor {
+  this(null, $imcall, true);
+}
+
+%javamethodmodifiers CVC4::DatatypeConstructor::DatatypeConstructor(std::string) "private";
+%javamethodmodifiers CVC4::DatatypeConstructor::DatatypeConstructor(std::string, unsigned weight) "private";
+
+%typemap(javaout) const CVC4::DatatypeConstructorArg& {
+  return new DatatypeConstructorArg(this.em, $jnicall, false);
+}
+
+%typemap(javabody) CVC4::DatatypeConstructorArg %{
+  private long swigCPtr;
+  protected boolean swigCMemOwn;
+  private ExprManager em;
+
+  protected $javaclassname(ExprManager em, long cPtr, boolean cMemoryOwn) {
+    swigCMemOwn = cMemoryOwn;
+    swigCPtr = cPtr;
+    this.em = em;
   }
 
+  protected static long getCPtr($javaclassname obj) {
+    return (obj == null) ? 0 : obj.swigCPtr;
+  }
+%}
+
+%typemap(javaout) CVC4::SelectorType {
+  return new SelectorType(this.em, $jnicall, true);
+}
+
+%extend CVC4::Datatype {
   std::string toString() const {
     std::stringstream ss;
     ss << *$self;
@@ -95,14 +185,6 @@
   }
 }
 %extend CVC4::DatatypeConstructor {
-  CVC4::JavaIteratorAdapter<CVC4::DatatypeConstructor,
-                            CVC4::DatatypeConstructorArg>
-  iterator()
-  {
-    return CVC4::JavaIteratorAdapter<CVC4::DatatypeConstructor,
-                                     CVC4::DatatypeConstructorArg>(*$self);
-  }
-
   std::string toString() const {
     std::stringstream ss;
     ss << *$self;
@@ -117,56 +199,28 @@
   }
 }
 
-// Datatype is "iterable" on the Java side
-%typemap(javainterfaces) CVC4::Datatype "java.lang.Iterable<DatatypeConstructor>";
-%typemap(javainterfaces) CVC4::DatatypeConstructor "java.lang.Iterable<DatatypeConstructorArg>";
-
-// the JavaIteratorAdapter should not be public, and implements Iterator
-%typemap(javaclassmodifiers) CVC4::JavaIteratorAdapter<CVC4::Datatype, CVC4::DatatypeConstructor> "class";
-%typemap(javaclassmodifiers) CVC4::JavaIteratorAdapter<CVC4::DatatypeConstructor, CVC4::DatatypeConstructorArg> "class";
-%typemap(javainterfaces) CVC4::JavaIteratorAdapter<CVC4::Datatype, CVC4::DatatypeConstructor> "java.util.Iterator<DatatypeConstructor>";
-%typemap(javainterfaces) CVC4::JavaIteratorAdapter<CVC4::DatatypeConstructor, CVC4::DatatypeConstructorArg> "java.util.Iterator<DatatypeConstructorArg>";
-// add some functions to the Java side (do it here because there's no way to do these in C++)
-%typemap(javacode) CVC4::JavaIteratorAdapter<CVC4::Datatype, CVC4::DatatypeConstructor> "
-  public void remove() {
-    throw new java.lang.UnsupportedOperationException();
-  }
-
-  public DatatypeConstructor next() {
-    if(hasNext()) {
-      return getNext();
-    } else {
-      throw new java.util.NoSuchElementException();
-    }
-  }
-"
-%typemap(javacode) CVC4::JavaIteratorAdapter<CVC4::DatatypeConstructor, CVC4::DatatypeConstructorArg> "
-  public void remove() {
-    throw new java.lang.UnsupportedOperationException();
-  }
-
-  public DatatypeConstructorArg 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<CVC4::Datatype, CVC4::DatatypeConstructor>::getNext() "private";
-%javamethodmodifiers CVC4::JavaIteratorAdapter<CVC4::DatatypeConstructor, CVC4::DatatypeConstructorArg>::getNext() "private";
-
-#endif /* SWIGJAVA */
+// Workaround for https://github.com/swig/swig/commit/63a5a8af88271559a7b170794b4c61c30b8934ea
+%typemap(javaconstruct) Datatype {
+  this(null, $imcall, true);
+}
 
-%include "expr/datatype.h"
+%typemap(javaconstruct) CVC4::Datatype {
+  this(em, $imcall, true);
+}
 
-#ifdef SWIGJAVA
+%typemap(javaout) CVC4::DatatypeConstructor {
+  return new DatatypeConstructor(this.em, $jnicall, true);
+}
 
-%include "bindings/java_iterator_adapter.h"
-%include "bindings/java_stream_adapters.h"
+%typemap(javaout) CVC4::DatatypeConstructorArg {
+  return new DatatypeConstructorArg(this.em, $jnicall, true);
+}
 
+SWIG_JAVA_ITERATOR_ADAPTER(CVC4::Datatype, CVC4::DatatypeConstructor)
 %template(JavaIteratorAdapter_Datatype) CVC4::JavaIteratorAdapter<CVC4::Datatype, CVC4::DatatypeConstructor>;
+SWIG_JAVA_ITERATOR_ADAPTER(CVC4::DatatypeConstructor, CVC4::DatatypeConstructorArg)
 %template(JavaIteratorAdapter_DatatypeConstructor) CVC4::JavaIteratorAdapter<CVC4::DatatypeConstructor, CVC4::DatatypeConstructorArg>;
 
 #endif /* SWIGJAVA */
+
+%include "expr/datatype.h"
diff --git a/src/expr/emptyset.i b/src/expr/emptyset.i
index ada3dd583..bcd3a0a92 100644
--- a/src/expr/emptyset.i
+++ b/src/expr/emptyset.i
@@ -2,6 +2,48 @@
 #include "expr/emptyset.h"
 %}
 
+#ifdef SWIGJAVA
+
+%typemap(javabody) CVC4::EmptySet %{
+  private long swigCPtr;
+  protected boolean swigCMemOwn;
+  private ExprManager em;
+
+  protected $javaclassname(ExprManager em, long cPtr, boolean cMemoryOwn) {
+    swigCMemOwn = cMemoryOwn;
+    swigCPtr = cPtr;
+    this.em = em; // keep ref to em in SWIG proxy class
+  }
+
+  protected static long getCPtr($javaclassname obj) {
+    return (obj == null) ? 0 : obj.swigCPtr;
+  }
+
+  public $javaclassname(ExprManager em, SetType t) {
+    this(t);
+    this.em = em;
+  }
+%}
+
+// Workaround for https://github.com/swig/swig/commit/63a5a8af88271559a7b170794b4c61c30b8934ea
+%typemap(javaconstruct) EmptySet {
+  this(null, $imcall, true);
+}
+
+%typemap(javaconstruct) CVC4::EmptySet {
+  this(null, $imcall, true);
+}
+
+%javamethodmodifiers CVC4::EmptySet::EmptySet(Type t) "private";
+
+%typemap(javaout) const CVC4::SetType& {
+  return new SetType(this.em, $jnicall, false);
+}
+
+#endif
+
+%ignore CVC4::EmptySet::EmptySet(const CVC4::EmptySet& other);
+
 %rename(equals) CVC4::EmptySet::operator==(const EmptySet&) const;
 %ignore CVC4::EmptySet::operator!=(const EmptySet&) const;
 
diff --git a/src/expr/expr.i b/src/expr/expr.i
index 14228d7c5..7e79d4c1d 100644
--- a/src/expr/expr.i
+++ b/src/expr/expr.i
@@ -1,102 +1,108 @@
 %{
 #include "expr/expr.h"
+%}
 
-#ifdef SWIGJAVA
+%ignore CVC4::Expr::Expr(const Expr&);
+// This is currently the only function that would require bindings for
+// `std::unordered_map<Expr, Expr, ExprHashFunction>` and is better implemented
+// at the Java/Python level if needed. Thus, we ignore it here.
+%ignore CVC4::Expr::substitute(const std::unordered_map<Expr, Expr, ExprHashFunction> map) const;
+%ignore CVC4::operator<<(std::ostream&, const Expr&);
+%ignore CVC4::operator<<(std::ostream&, const TypeCheckingException&);
+// Ignore because we would not know which ExprManager the Expr belongs to
+%ignore CVC4::TypeCheckingException::getExpression() const;
+%ignore CVC4::expr::operator<<(std::ostream&, ExprSetDepth);
+%ignore CVC4::expr::operator<<(std::ostream&, ExprPrintTypes);
+%ignore CVC4::expr::operator<<(std::ostream&, ExprDag);
+%ignore CVC4::expr::operator<<(std::ostream&, ExprSetLanguage);
+%ignore CVC4::Expr::operator=(const Expr&);
+%ignore CVC4::Expr::operator!=(const Expr&) const;
+%ignore CVC4::Expr::operator bool() const;// can just use isNull()
 
-#include "bindings/java_iterator_adapter.h"
-#include "bindings/java_stream_adapters.h"
+%rename(equals) CVC4::Expr::operator==(const Expr&) const;
+%rename(less) CVC4::Expr::operator<(const Expr&) const;
+%rename(lessEqual) CVC4::Expr::operator<=(const Expr&) const;
+%rename(greater) CVC4::Expr::operator>(const Expr&) const;
+%rename(greaterEqual) CVC4::Expr::operator>=(const Expr&) const;
 
-#endif /* SWIGJAVA */
-%}
+%rename(getChild) CVC4::Expr::operator[](unsigned i) const;
 
-#ifdef SWIGPYTHON
-%rename(doApply) CVC4::ExprHashFunction::operator()(CVC4::Expr) const;
-#else /* SWIGPYTHON */
+#ifdef SWIGJAVA
+
+// For the Java bindings, we implement `getExprManager()` at the Java level
+// because we can't map back the C++ point to the Java object
+%ignore CVC4::Expr::getExprManager() const;
 %rename(apply) CVC4::ExprHashFunction::operator()(CVC4::Expr) const;
-#endif /* SWIGPYTHON */
 
-#ifdef SWIGJAVA
 %typemap(javabody) CVC4::Expr %{
   private long swigCPtr;
   protected boolean swigCMemOwn;
+  private ExprManager em;
 
-  protected $javaclassname(long cPtr, boolean cMemoryOwn) {
+  protected $javaclassname(ExprManager em, long cPtr, boolean cMemoryOwn) {
     swigCMemOwn = cMemoryOwn;
     swigCPtr = cPtr;
-    this.em = SmtEngine.mkRef(getExprManager()); // keep ref to em in SWIG proxy class
+    this.em = em; // keep ref to em in SWIG proxy class
   }
 
   protected static long getCPtr($javaclassname obj) {
     return (obj == null) ? 0 : obj.swigCPtr;
   }
-%}
-%javamethodmodifiers CVC4::Expr::operator=(const Expr&) "protected";
-%typemap(javacode) CVC4::Expr %{
-  // a ref is kept here to keep Java GC from collecting the ExprManager
-  // before the Expr
-  private Object em;
-
-  public Expr assign(Expr e) {
-    Expr r = assignInternal(e);
-    this.em = SmtEngine.mkRef(getExprManager()); // keep ref to em in SWIG proxy class
-    return r;
+
+  public ExprManager getExprManager() throws edu.stanford.CVC4.Exception {
+    return this.em;
+  }
+
+  public JavaIteratorAdapter_Expr iterator() {
+    return new JavaIteratorAdapter_Expr(this.em, this);
   }
 %}
+
+// Workaround for https://github.com/swig/swig/commit/63a5a8af88271559a7b170794b4c61c30b8934ea
 %typemap(javaconstruct) Expr {
-    this($imcall, true);
-    this.em = SmtEngine.mkRef(getExprManager()); // keep ref to em in SWIG proxy class
-  }
-%typemap(javadestruct, methodname="delete", methodmodifiers="public synchronized") CVC4::Expr {
-    SmtEngine.dlRef(em);
-    em = null;
-    if (swigCPtr != 0) {
-      if (swigCMemOwn) {
-        swigCMemOwn = false;
-        CVC4JNI.delete_Expr(swigCPtr);
-      }
-      swigCPtr = 0;
-    }
-  }
-#endif /* SWIGJAVA */
+  this(null, $imcall, true);
+}
 
-%ignore CVC4::operator<<(std::ostream&, const Expr&);
-%ignore CVC4::operator<<(std::ostream&, const TypeCheckingException&);
+%typemap(javaconstruct) CVC4::Expr {
+  this(null, $imcall, true);
+}
 
-%ignore CVC4::expr::operator<<(std::ostream&, ExprSetDepth);
-%ignore CVC4::expr::operator<<(std::ostream&, ExprPrintTypes);
-%ignore CVC4::expr::operator<<(std::ostream&, ExprDag);
-%ignore CVC4::expr::operator<<(std::ostream&, ExprSetLanguage);
+%typemap(javaout) CVC4::Expr {
+  return new Expr(this.em, $jnicall, true);
+}
 
-%rename(assignInternal) CVC4::Expr::operator=(const Expr&);
-%rename(equals) CVC4::Expr::operator==(const Expr&) const;
-%ignore CVC4::Expr::operator!=(const Expr&) const;
-%rename(less) CVC4::Expr::operator<(const Expr&) const;
-%rename(lessEqual) CVC4::Expr::operator<=(const Expr&) const;
-%rename(greater) CVC4::Expr::operator>(const Expr&) const;
-%rename(greaterEqual) CVC4::Expr::operator>=(const Expr&) const;
+SWIG_STD_VECTOR_EM(CVC4::Expr, const CVC4::Expr&)
+SWIG_STD_VECTOR_EM(std::vector<CVC4::Expr>, const std::vector<CVC4::Expr>&)
 
-%rename(getChild) CVC4::Expr::operator[](unsigned i) const;
-%ignore CVC4::Expr::operator bool() const;// can just use isNull()
+%template(vectorExpr) std::vector<CVC4::Expr>;
+%typemap(javaout) std::vector<CVC4::Expr> {
+  return new vectorExpr(this.em, $jnicall, true);
+}
+%typemap(javaout) const std::vector<CVC4::Expr>& {
+  return new vectorExpr(this.em, $jnicall, false);
+}
+%template(vectorVectorExpr) std::vector<std::vector<CVC4::Expr>>;
 
-namespace CVC4 {
-  namespace expr {
-    %ignore exportInternal;
-  }/* CVC4::expr namespace */
-}/* CVC4 namespace */
+%javamethodmodifiers CVC4::Expr::operator=(const Expr&) "protected";
 
-#ifdef SWIGJAVA
+%typemap(javaout) const CVC4::AscriptionType& {
+  return new AscriptionType(this.em, $jnicall, $owner);
+}
+
+%typemap(javaout) const CVC4::EmptySet& {
+  return new EmptySet(this.em, $jnicall, $owner);
+}
+
+%typemap(javaout) const CVC4::ExprSequence& {
+  return new ExprSequence(this.em, $jnicall, $owner);
+}
 
 // Instead of Expr::begin() and end(), create an
 // iterator() method on the Java side that returns a Java-style
 // Iterator.
 %ignore CVC4::Expr::begin() const;
 %ignore CVC4::Expr::end() const;
-%extend CVC4::Expr {
-  CVC4::JavaIteratorAdapter<CVC4::Expr, CVC4::Expr> iterator()
-  {
-    return CVC4::JavaIteratorAdapter<CVC4::Expr, CVC4::Expr>(*$self);
-  }
-}
+%ignore CVC4::Expr::const_iterator;
 
 // Expr is "iterable" on the Java side
 %typemap(javainterfaces) CVC4::Expr "java.lang.Iterable<edu.stanford.CVC4.Expr>";
@@ -123,6 +129,10 @@ namespace CVC4 {
 
 #endif /* SWIGJAVA */
 
+#ifdef SWIGPYTHON
+%rename(doApply) CVC4::ExprHashFunction::operator()(CVC4::Expr) const;
+#endif /* SWIGPYTHON */
+
 %include "expr/expr.h"
 
 #ifdef SWIGPYTHON
@@ -156,11 +166,7 @@ namespace CVC4 {
 
 #ifdef SWIGJAVA
 
-%include "bindings/java_iterator_adapter.h"
-%include "bindings/java_stream_adapters.h"
-
+SWIG_JAVA_ITERATOR_ADAPTER(CVC4::Expr, CVC4::Expr)
 %template(JavaIteratorAdapter_Expr) CVC4::JavaIteratorAdapter<CVC4::Expr, CVC4::Expr>;
 
 #endif /* SWIGJAVA */
-
-%include "expr/expr.h"
diff --git a/src/expr/expr_manager.i b/src/expr/expr_manager.i
index 5a5e7a9d4..d8ed7f6a6 100644
--- a/src/expr/expr_manager.i
+++ b/src/expr/expr_manager.i
@@ -2,29 +2,105 @@
 #include "expr/expr_manager.h"
 %}
 
-%typemap(javacode) CVC4::ExprManager %{
-  // a ref is kept here to keep Java GC from collecting the Options
-  // before the ExprManager
-  private Object options;
-%}
-%typemap(javaconstruct) ExprManager {
-    this($imcall, true);
-    this.options = SmtEngine.mkRef(options); // keep ref to options in SWIG proxy class
-  }
-%typemap(javadestruct, methodname="delete", methodmodifiers="public synchronized") CVC4::ExprManager {
-    SmtEngine.dlRef(options);
-    options = null;
-    if (swigCPtr != 0) {
-      if (swigCMemOwn) {
-        swigCMemOwn = false;
-        CVC4JNI.delete_ExprManager(swigCPtr);
-      }
-      swigCPtr = 0;
-    }
-  }
-
+%ignore CVC4::ExprManager::exportType(const Type& t, ExprManager* em, ExprManagerMapCollection& vmap);
 %ignore CVC4::stats::getStatisticsRegistry(ExprManager*);
 %ignore CVC4::ExprManager::getResourceManager();
+%ignore CVC4::ExprManager::mkRecordType(const Record& rec);
+%ignore CVC4::ExprManager::safeFlushStatistics(int fd) const;
+
+#ifdef SWIGJAVA
+
+%typemap(javaout) CVC4::Expr {
+  return new Expr(this, $jnicall, true);
+}
+
+%typemap(javaout) CVC4::Type {
+  return new Type(this, $jnicall, true);
+}
+
+%typemap(javaout) CVC4::ArrayType {
+  return new ArrayType(this, $jnicall, true);
+}
+
+%typemap(javaout) CVC4::BitVectorType {
+  return new BitVectorType(this, $jnicall, true);
+}
+
+%typemap(javaout) CVC4::BooleanType {
+  return new BooleanType(this, $jnicall, true);
+}
+
+%typemap(javaout) CVC4::ConstructorType {
+  return new ConstructorType(this, $jnicall, true);
+}
+
+%typemap(javaout) const CVC4::Datatype& {
+  return new Datatype(this, $jnicall, false);
+}
+
+%typemap(javaout) CVC4::DatatypeType {
+  return new DatatypeType(this, $jnicall, true);
+}
+
+%typemap(javaout) std::vector<CVC4::DatatypeType> {
+  return new vectorDatatypeType(this, $jnicall, true);
+}
+
+%typemap(javaout) CVC4::FloatingPointType {
+  return new FloatingPointType(this, $jnicall, true);
+}
+
+%typemap(javaout) CVC4::FunctionType {
+  return new FunctionType(this, $jnicall, true);
+}
+
+%typemap(javaout) CVC4::SelectorType {
+  return new SelectorType(this, $jnicall, true);
+}
+
+%typemap(javaout) CVC4::StringType {
+  return new StringType(this, $jnicall, true);
+}
+
+%typemap(javaout) CVC4::RegExpType {
+  return new RegExpType(this, $jnicall, true);
+}
+
+%typemap(javaout) CVC4::RealType {
+  return new RealType(this, $jnicall, true);
+}
+
+%typemap(javaout) CVC4::SetType {
+  return new SetType(this, $jnicall, true);
+}
+
+%typemap(javaout) CVC4::SExprType {
+  return new SExprType(this, $jnicall, true);
+}
+
+%typemap(javaout) CVC4::SortType {
+  return new SortType(this, $jnicall, true);
+}
+
+%typemap(javaout) CVC4::SortConstructorType {
+  return new SortConstructorType(this, $jnicall, true);
+}
+
+%typemap(javaout) CVC4::TesterType {
+  return new TesterType(this, $jnicall, true);
+}
+
+%typemap(javaout) CVC4::IntegerType {
+  return new IntegerType(this, $jnicall, true);
+}
+
+%typemap(javaout) CVC4::RoundingModeType {
+  return new RoundingModeType(this, $jnicall, true);
+}
+
+%javamethodmodifiers CVC4::ExprManager::exportType(const Type& t, ExprManager* em, ExprManagerMapCollection& vmap) "public";
+
+#endif /* SWIGJAVA */
 
 %include "expr/expr_manager.h"
 
@@ -53,7 +129,6 @@
 %template(mkConst) CVC4::ExprManager::mkConst<CVC4::kind::Kind_t>;
 %template(mkConst) CVC4::ExprManager::mkConst<CVC4::DatatypeIndexConstant>;
 %template(mkConst) CVC4::ExprManager::mkConst<CVC4::TupleUpdate>;
-%template(mkConst) CVC4::ExprManager::mkConst<CVC4::RecordUpdate>;
 %template(mkConst) CVC4::ExprManager::mkConst<CVC4::Rational>;
 %template(mkConst) CVC4::ExprManager::mkConst<CVC4::BitVector>;
 %template(mkConst) CVC4::ExprManager::mkConst<CVC4::EmptySet>;
@@ -74,5 +149,3 @@
 %template(mkConst) CVC4::ExprManager::mkConst<bool>;
 %template(mkConst) CVC4::ExprManager::mkConst<CVC4::RoundingMode>;
 #endif
-
-%include "expr/expr_manager.h"
diff --git a/src/expr/expr_sequence.i b/src/expr/expr_sequence.i
index 42e130466..294937024 100644
--- a/src/expr/expr_sequence.i
+++ b/src/expr/expr_sequence.i
@@ -2,6 +2,42 @@
 #include "expr/expr_sequence.h"
 %}
 
+#ifdef SWIGJAVA
+
+%typemap(javabody) CVC4::ExprSequence %{
+  private long swigCPtr;
+  protected boolean swigCMemOwn;
+  private ExprManager em;
+
+  protected $javaclassname(ExprManager em, long cPtr, boolean cMemoryOwn) {
+    swigCMemOwn = cMemoryOwn;
+    swigCPtr = cPtr;
+    this.em = em; // keep ref to em in SWIG proxy class
+  }
+
+  protected static long getCPtr($javaclassname obj) {
+    return (obj == null) ? 0 : obj.swigCPtr;
+  }
+
+  public $javaclassname(ExprManager em, Type type, vectorExpr seq) {
+    this(type, seq);
+    this.em = em;
+  }
+%}
+
+// Workaround for https://github.com/swig/swig/commit/63a5a8af88271559a7b170794b4c61c30b8934ea
+%typemap(javaconstruct) ExprSequence {
+  this(null, $imcall, true);
+}
+
+%typemap(javaconstruct) CVC4::ExprSequence {
+  this(null, $imcall, true);
+}
+
+%javamethodmodifiers CVC4::ExprSequence::ExprSequence(Type type, vectorExpr seq) "private";
+
+#endif
+
 %rename(equals) CVC4::ExprSequence::operator==(const ExprSequence&) const;
 %ignore CVC4::ExprSequence::operator!=(const ExprSequence&) const;
 %ignore CVC4::ExprSequence::getSequence() const;
diff --git a/src/expr/record.i b/src/expr/record.i
deleted file mode 100644
index dce785ea3..000000000
--- a/src/expr/record.i
+++ /dev/null
@@ -1,55 +0,0 @@
-%{
-#include "expr/record.h"
-
-#ifdef SWIGJAVA
-
-#include "bindings/java_iterator_adapter.h"
-#include "bindings/java_stream_adapters.h"
-
-#endif /* SWIGJAVA */
-%}
-
-%include "stdint.i"
-
-%rename(equals) CVC4::RecordUpdate::operator==(const RecordUpdate&) const;
-%ignore CVC4::RecordUpdate::operator!=(const RecordUpdate&) const;
-
-%rename(equals) CVC4::Record::operator==(const Record&) const;
-%ignore CVC4::Record::operator!=(const Record&) const;
-%rename(getField) CVC4::Record::operator[](size_t) const;
-
-%rename(apply) CVC4::RecordHashFunction::operator()(const Record&) const;
-%rename(apply) CVC4::RecordUpdateHashFunction::operator()(const RecordUpdate&) const;
-
-%ignore CVC4::operator<<(std::ostream&, const Record&);
-%ignore CVC4::operator<<(std::ostream&, const RecordUpdate&);
-
-#ifdef SWIGJAVA
-
-// These Object arrays are always of two elements, the first is a String and the second a
-// Type.  (On the C++ side, it is a std::pair<std::string, Type>.)
-%typemap(jni) std::pair<std::string, CVC4::Type> "jobjectArray";
-%typemap(jtype) std::pair<std::string, CVC4::Type> "java.lang.Object[]";
-%typemap(jstype) std::pair<std::string, CVC4::Type> "java.lang.Object[]";
-%typemap(javaout) std::pair<std::string, CVC4::Type> { return $jnicall; }
-%typemap(out) std::pair<std::string, CVC4::Type> {
-      $result = jenv->NewObjectArray(2, jenv->FindClass("java/lang/Object"), $null);
-      jenv->SetObjectArrayElement($result, 0, jenv->NewStringUTF($1.first.c_str()));
-      jclass clazz = jenv->FindClass("edu/stanford/CVC4/Type");
-      jmethodID methodid = jenv->GetMethodID(clazz, "<init>", "(JZ)V");
-      jenv->SetObjectArrayElement($result, 1, jenv->NewObject(clazz, methodid, reinterpret_cast<uintptr_t>(new CVC4::Type($1.second)), true));
-    };
-
-
-
-#endif /* SWIGJAVA */
-
-%include "expr/record.h"
-
-#ifdef SWIGJAVA
-
-%include "bindings/java_iterator_adapter.h"
-%include "bindings/java_stream_adapters.h"
-
-
-#endif /* SWIGJAVA */
diff --git a/src/expr/type.i b/src/expr/type.i
index 16d059eac..8262c4cea 100644
--- a/src/expr/type.i
+++ b/src/expr/type.i
@@ -2,6 +2,77 @@
 #include "expr/type.h"
 %}
 
+%ignore CVC4::expr::exportTypeInternal(TypeNode n, NodeManager* from, NodeManager* nm, ExprManagerMapCollection& vmap);
+
+%ignore CVC4::Type::Type(const Type&);
+%ignore CVC4::Type::operator=(const Type&);
+%ignore CVC4::Type::operator!=(const Type&) const;
+%rename(equals) CVC4::Type::operator==(const Type&) const;
+%rename(less) CVC4::Type::operator<(const Type&) const;
+%rename(lessEqual) CVC4::Type::operator<=(const Type&) const;
+%rename(greater) CVC4::Type::operator>(const Type&) const;
+%rename(greaterEqual) CVC4::Type::operator>=(const Type&) const;
+
+%ignore CVC4::BitVectorType::BitVectorType();
+%ignore CVC4::BitVectorType::BitVectorType(const Type&);
+
+%ignore CVC4::BooleanType::BooleanType();
+%ignore CVC4::BooleanType::BooleanType(const Type&);
+
+%ignore CVC4::ConstructorType::ConstructorType();
+%ignore CVC4::ConstructorType::ConstructorType(const Type&);
+
+%ignore CVC4::FloatingPointType::FloatingPointType();
+%ignore CVC4::FloatingPointType::FloatingPointType(const Type&);
+
+%ignore CVC4::DatatypeType::DatatypeType();
+%ignore CVC4::DatatypeType::DatatypeType(const Type&);
+%ignore CVC4::DatatypeType::getRecord() const;
+
+%ignore CVC4::FunctionType::FunctionType();
+%ignore CVC4::FunctionType::FunctionType(const Type&);
+
+%ignore CVC4::IntegerType::IntegerType();
+%ignore CVC4::IntegerType::IntegerType(const Type&);
+
+%ignore CVC4::RealType::RealType();
+%ignore CVC4::RealType::RealType(const Type&);
+
+%ignore CVC4::RegExpType::RegExpType();
+%ignore CVC4::RegExpType::RegExpType(const Type&);
+
+%ignore CVC4::RoundingModeType::RoundingModeType();
+%ignore CVC4::RoundingModeType::RoundingModeType(const Type&);
+
+%ignore CVC4::SelectorType::SelectorType();
+%ignore CVC4::SelectorType::SelectorType(const Type&);
+
+%ignore CVC4::SequenceType::SequenceType();
+%ignore CVC4::SequenceType::SequenceType(const Type&);
+
+%ignore CVC4::SExprType::SExprType();
+%ignore CVC4::SExprType::SExprType(const Type&);
+
+%ignore CVC4::SortType::SortType();
+%ignore CVC4::SortType::SortType(const Type&);
+
+%ignore CVC4::SortConstructorType::SortConstructorType();
+%ignore CVC4::SortConstructorType::SortConstructorType(const Type&);
+
+%ignore CVC4::StringType::StringType();
+%ignore CVC4::StringType::StringType(const Type&);
+
+%ignore CVC4::TesterType::TesterType();
+%ignore CVC4::TesterType::TesterType(const Type&);
+
+%ignore CVC4::ArrayType::ArrayType();
+%ignore CVC4::ArrayType::ArrayType(const Type&);
+
+%ignore CVC4::SetType::SetType();
+%ignore CVC4::SetType::SetType(const Type&);
+
+%ignore CVC4::operator<<(std::ostream&, const Type&);
+
 #ifdef SWIGPYTHON
 %rename(doApply) CVC4::TypeHashFunction::operator()(const CVC4::Type&) const;
 #else /* SWIGPYTHON */
@@ -9,62 +80,358 @@
 #endif /* SWIGPYTHON */
 
 #ifdef SWIGJAVA
+
+%include "bindings/java/cvc4_std_vector.i"
+
+%typemap(javaout) CVC4::Expr {
+  return new Expr(this.em, $jnicall, true);
+}
+
+%typemap(javaout) std::vector<CVC4::Type> {
+  return new vectorType(this.em, $jnicall, true);
+}
+
 %typemap(javabody) CVC4::Type %{
   private long swigCPtr;
   protected boolean swigCMemOwn;
+  // Prevent ExprManager from being garbage collected before this instance
+  protected ExprManager em;
 
-  protected $javaclassname(long cPtr, boolean cMemoryOwn) {
+  protected $javaclassname(ExprManager em, long cPtr, boolean cMemoryOwn) {
     swigCMemOwn = cMemoryOwn;
     swigCPtr = cPtr;
-    this.em = SmtEngine.mkRef(getExprManager()); // keep ref to em in SWIG proxy class
+    this.em = em;
   }
 
   protected static long getCPtr($javaclassname obj) {
     return (obj == null) ? 0 : obj.swigCPtr;
   }
 %}
-%javamethodmodifiers CVC4::Type::operator=(const Type&) "protected";
-%typemap(javacode) CVC4::Type %{
-  // a ref is kept here to keep Java GC from collecting the ExprManager
-  // before the Type
-  private Object em;
 
-  public Type assign(Type t) {
-    Type r = assignInternal(t);
-    this.em = SmtEngine.mkRef(getExprManager()); // keep ref to em in SWIG proxy class
-    return r;
+// Workaround for https://github.com/swig/swig/commit/63a5a8af88271559a7b170794b4c61c30b8934ea
+%typemap(javaconstruct) Type {
+  this(null, $imcall, true);
+}
+
+%typemap(javaconstruct) CVC4::Type {
+  this(null, $imcall, true);
+}
+
+
+%typemap(javaout) CVC4::Type {
+  return new Type(this.em, $jnicall, true);
+}
+
+SWIG_STD_VECTOR_EM(CVC4::Type, const CVC4::Type&)
+
+%typemap(javaout) CVC4::Type {
+  return new Type(this.em, $jnicall, true);
+}
+%typemap(javaout) const CVC4::Type& {
+  return new Type(this.em, $jnicall, false);
+}
+%template(vectorType) std::vector<CVC4::Type>;
+
+%typemap(javabody_derived) CVC4::BitVectorType %{
+  private transient long swigCPtr;
+
+  protected $javaclassname(ExprManager em, long cPtr, boolean cMemoryOwn) {
+    super(em, CVC4JNI.$javaclassname_SWIGUpcast(cPtr), cMemoryOwn);
+    swigCPtr = cPtr;
+    swigCMemOwn = cMemoryOwn;
+  }
+
+  protected static long getCPtr($javaclassname obj) {
+    return (obj == null) ? 0 : obj.swigCPtr;
   }
 %}
-%typemap(javaconstruct) Type {
-    this($imcall, true);
-    this.em = SmtEngine.mkRef(getExprManager()); // keep ref to em in SWIG proxy class
-  }
-%typemap(javadestruct, methodname="delete", methodmodifiers="public synchronized") CVC4::Type {
-    SmtEngine.dlRef(em);
-    em = null;
-    if (swigCPtr != 0) {
-      if (swigCMemOwn) {
-        swigCMemOwn = false;
-        CVC4JNI.delete_Type(swigCPtr);
-      }
-      swigCPtr = 0;
-    }
+
+%typemap(javabody_derived) CVC4::BooleanType %{
+  private transient long swigCPtr;
+
+  protected $javaclassname(ExprManager em, long cPtr, boolean cMemoryOwn) {
+    super(em, CVC4JNI.$javaclassname_SWIGUpcast(cPtr), cMemoryOwn);
+    swigCPtr = cPtr;
+    swigCMemOwn = cMemoryOwn;
   }
-#endif /* SWIGJAVA */
-%ignore CVC4::operator<<(std::ostream&, const Type&);
 
-%rename(assignInternal) CVC4::Type::operator=(const Type&);
-%rename(equals) CVC4::Type::operator==(const Type&) const;
-%ignore CVC4::Type::operator!=(const Type&) const;
-%rename(less) CVC4::Type::operator<(const Type&) const;
-%rename(lessEqual) CVC4::Type::operator<=(const Type&) const;
-%rename(greater) CVC4::Type::operator>(const Type&) const;
-%rename(greaterEqual) CVC4::Type::operator>=(const Type&) const;
+  protected static long getCPtr($javaclassname obj) {
+    return (obj == null) ? 0 : obj.swigCPtr;
+  }
+%}
+
+%typemap(javabody_derived) CVC4::ConstructorType %{
+  private transient long swigCPtr;
+
+  protected $javaclassname(ExprManager em, long cPtr, boolean cMemoryOwn) {
+    super(em, CVC4JNI.$javaclassname_SWIGUpcast(cPtr), cMemoryOwn);
+    swigCPtr = cPtr;
+    swigCMemOwn = cMemoryOwn;
+  }
 
-namespace CVC4 {
-  namespace expr {
-    %ignore exportTypeInternal;
-  }/* CVC4::expr namespace */
-}/* CVC4 namespace */
+  protected static long getCPtr($javaclassname obj) {
+    return (obj == null) ? 0 : obj.swigCPtr;
+  }
+%}
+
+%typemap(javabody_derived) CVC4::FloatingPointType %{
+  private transient long swigCPtr;
+
+  protected $javaclassname(ExprManager em, long cPtr, boolean cMemoryOwn) {
+    super(em, CVC4JNI.$javaclassname_SWIGUpcast(cPtr), cMemoryOwn);
+    swigCPtr = cPtr;
+    swigCMemOwn = cMemoryOwn;
+  }
+
+  protected static long getCPtr($javaclassname obj) {
+    return (obj == null) ? 0 : obj.swigCPtr;
+  }
+%}
+
+%typemap(javabody_derived) CVC4::DatatypeType %{
+  private transient long swigCPtr;
+
+  protected $javaclassname(ExprManager em, long cPtr, boolean cMemoryOwn) {
+    super(em, CVC4JNI.$javaclassname_SWIGUpcast(cPtr), cMemoryOwn);
+    swigCPtr = cPtr;
+    swigCMemOwn = cMemoryOwn;
+  }
+
+  protected static long getCPtr($javaclassname obj) {
+    return (obj == null) ? 0 : obj.swigCPtr;
+  }
+%}
+
+SWIG_STD_VECTOR_EM(CVC4::DatatypeType, const CVC4::DatatypeType&)
+
+%typemap(javaout) CVC4::DatatypeType {
+  return new DatatypeType(this.em, $jnicall, true);
+}
+%typemap(javaout) const CVC4::DatatypeType& {
+  return new DatatypeType(this.em, $jnicall, false);
+}
+%template(vectorDatatypeType) std::vector<CVC4::DatatypeType>;
+
+%typemap(javabody_derived) CVC4::FunctionType %{
+  private transient long swigCPtr;
+
+  protected $javaclassname(ExprManager em, long cPtr, boolean cMemoryOwn) {
+    super(em, CVC4JNI.$javaclassname_SWIGUpcast(cPtr), cMemoryOwn);
+    swigCPtr = cPtr;
+    swigCMemOwn = cMemoryOwn;
+  }
+
+  protected static long getCPtr($javaclassname obj) {
+    return (obj == null) ? 0 : obj.swigCPtr;
+  }
+%}
+
+%typemap(javabody_derived) CVC4::IntegerType %{
+  private transient long swigCPtr;
+
+  protected $javaclassname(ExprManager em, long cPtr, boolean cMemoryOwn) {
+    super(em, CVC4JNI.$javaclassname_SWIGUpcast(cPtr), cMemoryOwn);
+    swigCPtr = cPtr;
+    swigCMemOwn = cMemoryOwn;
+  }
+
+  protected static long getCPtr($javaclassname obj) {
+    return (obj == null) ? 0 : obj.swigCPtr;
+  }
+%}
+
+%typemap(javabody_derived) CVC4::RealType %{
+  private transient long swigCPtr;
+
+  protected $javaclassname(ExprManager em, long cPtr, boolean cMemoryOwn) {
+    super(em, CVC4JNI.$javaclassname_SWIGUpcast(cPtr), cMemoryOwn);
+    swigCPtr = cPtr;
+    swigCMemOwn = cMemoryOwn;
+  }
+
+  protected static long getCPtr($javaclassname obj) {
+    return (obj == null) ? 0 : obj.swigCPtr;
+  }
+%}
+
+%typemap(javabody_derived) CVC4::RegExpType %{
+  private transient long swigCPtr;
+
+  protected $javaclassname(ExprManager em, long cPtr, boolean cMemoryOwn) {
+    super(em, CVC4JNI.$javaclassname_SWIGUpcast(cPtr), cMemoryOwn);
+    swigCPtr = cPtr;
+    swigCMemOwn = cMemoryOwn;
+  }
+
+  protected static long getCPtr($javaclassname obj) {
+    return (obj == null) ? 0 : obj.swigCPtr;
+  }
+%}
+
+%typemap(javabody_derived) CVC4::RoundingModeType %{
+  private transient long swigCPtr;
+
+  protected $javaclassname(ExprManager em, long cPtr, boolean cMemoryOwn) {
+    super(em, CVC4JNI.$javaclassname_SWIGUpcast(cPtr), cMemoryOwn);
+    swigCPtr = cPtr;
+    swigCMemOwn = cMemoryOwn;
+  }
+
+  protected static long getCPtr($javaclassname obj) {
+    return (obj == null) ? 0 : obj.swigCPtr;
+  }
+%}
+
+%typemap(javabody_derived) CVC4::SelectorType %{
+  private transient long swigCPtr;
+
+  protected $javaclassname(ExprManager em, long cPtr, boolean cMemoryOwn) {
+    super(em, CVC4JNI.$javaclassname_SWIGUpcast(cPtr), cMemoryOwn);
+    swigCPtr = cPtr;
+    swigCMemOwn = cMemoryOwn;
+  }
+
+  protected static long getCPtr($javaclassname obj) {
+    return (obj == null) ? 0 : obj.swigCPtr;
+  }
+%}
+
+%typemap(javabody_derived) CVC4::SequenceType %{
+  private transient long swigCPtr;
+
+  protected $javaclassname(ExprManager em, long cPtr, boolean cMemoryOwn) {
+    super(em, CVC4JNI.$javaclassname_SWIGUpcast(cPtr), cMemoryOwn);
+    swigCPtr = cPtr;
+    swigCMemOwn = cMemoryOwn;
+  }
+
+  protected static long getCPtr($javaclassname obj) {
+    return (obj == null) ? 0 : obj.swigCPtr;
+  }
+%}
+
+%typemap(javabody_derived) CVC4::SExprType %{
+  private transient long swigCPtr;
+
+  protected $javaclassname(ExprManager em, long cPtr, boolean cMemoryOwn) {
+    super(em, CVC4JNI.$javaclassname_SWIGUpcast(cPtr), cMemoryOwn);
+    swigCPtr = cPtr;
+    swigCMemOwn = cMemoryOwn;
+  }
+
+  protected static long getCPtr($javaclassname obj) {
+    return (obj == null) ? 0 : obj.swigCPtr;
+  }
+%}
+
+%typemap(javabody_derived) CVC4::SortType %{
+  private transient long swigCPtr;
+
+  protected $javaclassname(ExprManager em, long cPtr, boolean cMemoryOwn) {
+    super(em, CVC4JNI.$javaclassname_SWIGUpcast(cPtr), cMemoryOwn);
+    swigCPtr = cPtr;
+    swigCMemOwn = cMemoryOwn;
+  }
+
+  protected static long getCPtr($javaclassname obj) {
+    return (obj == null) ? 0 : obj.swigCPtr;
+  }
+%}
+
+%typemap(javabody_derived) CVC4::SortConstructorType %{
+  private transient long swigCPtr;
+
+  protected $javaclassname(ExprManager em, long cPtr, boolean cMemoryOwn) {
+    super(em, CVC4JNI.$javaclassname_SWIGUpcast(cPtr), cMemoryOwn);
+    swigCPtr = cPtr;
+    swigCMemOwn = cMemoryOwn;
+  }
+
+  protected static long getCPtr($javaclassname obj) {
+    return (obj == null) ? 0 : obj.swigCPtr;
+  }
+%}
+
+%typemap(javabody_derived) CVC4::StringType %{
+  private transient long swigCPtr;
+
+  protected $javaclassname(ExprManager em, long cPtr, boolean cMemoryOwn) {
+    super(em, CVC4JNI.$javaclassname_SWIGUpcast(cPtr), cMemoryOwn);
+    swigCPtr = cPtr;
+    swigCMemOwn = cMemoryOwn;
+  }
+
+  protected static long getCPtr($javaclassname obj) {
+    return (obj == null) ? 0 : obj.swigCPtr;
+  }
+%}
+
+%typemap(javabody_derived) CVC4::TesterType %{
+  private transient long swigCPtr;
+
+  protected $javaclassname(ExprManager em, long cPtr, boolean cMemoryOwn) {
+    super(em, CVC4JNI.$javaclassname_SWIGUpcast(cPtr), cMemoryOwn);
+    swigCPtr = cPtr;
+    swigCMemOwn = cMemoryOwn;
+  }
+
+  protected static long getCPtr($javaclassname obj) {
+    return (obj == null) ? 0 : obj.swigCPtr;
+  }
+%}
+
+%typemap(javabody_derived) CVC4::ArrayType %{
+  private transient long swigCPtr;
+
+  protected $javaclassname(ExprManager em, long cPtr, boolean cMemoryOwn) {
+    super(em, CVC4JNI.$javaclassname_SWIGUpcast(cPtr), cMemoryOwn);
+    swigCPtr = cPtr;
+    swigCMemOwn = cMemoryOwn;
+  }
+
+  protected static long getCPtr($javaclassname obj) {
+    return (obj == null) ? 0 : obj.swigCPtr;
+  }
+%}
+
+%typemap(javabody_derived) CVC4::SetType %{
+  private transient long swigCPtr;
+
+  protected $javaclassname(ExprManager em, long cPtr, boolean cMemoryOwn) {
+    super(em, CVC4JNI.$javaclassname_SWIGUpcast(cPtr), cMemoryOwn);
+    swigCMemOwn = cMemoryOwn;
+    swigCPtr = cPtr;
+  }
+
+  protected static long getCPtr($javaclassname obj) {
+    return (obj == null) ? 0 : obj.swigCPtr;
+  }
+%}
+
+%typemap(javaout) CVC4::SetType {
+  return new SetType(this.em, $jnicall, true);
+}
+
+%typemap(javaout) CVC4::BooleanType {
+  return new BooleanType(this.em, $jnicall, true);
+}
+
+%typemap(javaout) const CVC4::Datatype& {
+  return new Datatype(this.em, $jnicall, true);
+}
+
+%typemap(javaout) CVC4::DatatypeType {
+  return new DatatypeType(this.em, $jnicall, true);
+}
+
+%typemap(javaout) CVC4::SortType {
+  return new SortType(this.em, $jnicall, true);
+}
+
+%typemap(javaout) typeVector {
+  return new typeVector(this.em, $jnicall, true);
+}
+
+#endif /* SWIGJAVA */
 
 %include "expr/type.h"
diff --git a/src/expr/variable_type_map.i b/src/expr/variable_type_map.i
index 95c705c1e..17ca6a110 100644
--- a/src/expr/variable_type_map.i
+++ b/src/expr/variable_type_map.i
@@ -2,6 +2,50 @@
 #include "expr/variable_type_map.h"
 %}
 
+#if SWIGJAVA
+
+%typemap(javabody) CVC4::VariableTypeMap %{
+  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 VariableTypeMap(ExprManager em) {
+    this();
+    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) VariableTypeMap {
+  this(null, $imcall, true);
+}
+
+%typemap(javaconstruct) CVC4::VariableTypeMap {
+  this(null, $imcall, true);
+}
+
+%typemap(javaout) CVC4::Expr& {
+  return new Expr(this.em, $jnicall, false);
+}
+
+%typemap(javaout) CVC4::Type& {
+  return new Type(this.em, $jnicall, false);
+}
+
+%javamethodmodifiers CVC4::VariableTypeMap::VariableTypeMap() "private";
+
+#endif /* SWIGJAVA */
+
 %rename(get) CVC4::VariableTypeMap::operator[](Expr);
 %rename(get) CVC4::VariableTypeMap::operator[](Type);
 
diff --git a/src/options/options.i b/src/options/options.i
index ba98c4fc4..319b4addb 100644
--- a/src/options/options.i
+++ b/src/options/options.i
@@ -2,6 +2,21 @@
 #include "options/options.h"
 %}
 
+%ignore CVC4::Options::registerAndNotify(ListenerCollection& collection, Listener* listener, bool notify);
+%ignore CVC4::Options::registerBeforeSearchListener(Listener* listener);
+%ignore CVC4::Options::registerTlimitListener(Listener* listener, bool notifyIfSet);
+%ignore CVC4::Options::registerTlimitPerListener(Listener* listener, bool notifyIfSet);
+%ignore CVC4::Options::registerRlimitListener(Listener* listener, bool notifyIfSet);
+%ignore CVC4::Options::registerRlimitPerListener(Listener* listener, bool notifyIfSet);
+%ignore CVC4::Options::registerSetDefaultExprDepthListener(Listener* listener, bool notifyIfSet);
+%ignore CVC4::Options::registerSetDefaultExprDagListener(Listener* listener, bool notifyIfSet);
+%ignore CVC4::Options::registerSetPrintExprTypesListener(Listener* listener, bool notifyIfSet);
+%ignore CVC4::Options::registerSetDumpModeListener(Listener* listener, bool notifyIfSet);
+%ignore CVC4::Options::registerSetPrintSuccessListener(Listener* listener, bool notifyIfSet);
+%ignore CVC4::Options::registerDumpToFileNameListener(Listener* listener, bool notifyIfSet);
+%ignore CVC4::Options::registerSetRegularOutputChannelListener(Listener* listener, bool notifyIfSet);
+%ignore CVC4::Options::registerSetDiagnosticOutputChannelListener(Listener* listener, bool notifyIfSet);
+
 %apply char** STRING_ARRAY { char* argv[] }
 %include "options/options.h"
 %clear char* argv[];
diff --git a/src/proof/unsat_core.i b/src/proof/unsat_core.i
index c37c8551d..780a75996 100644
--- a/src/proof/unsat_core.i
+++ b/src/proof/unsat_core.i
@@ -1,17 +1,37 @@
 %{
 #include "proof/unsat_core.h"
+%}
+
+%ignore CVC4::operator<<(std::ostream&, const UnsatCore&);
 
 #ifdef SWIGJAVA
 
-#include "bindings/java_iterator_adapter.h"
-#include "bindings/java_stream_adapters.h"
+%typemap(javabody) CVC4::UnsatCore %{
+  private long swigCPtr;
+  protected boolean swigCMemOwn;
+  private ExprManager em;
 
-#endif /* SWIGJAVA */
+  protected $javaclassname(ExprManager em, long cPtr, boolean cMemoryOwn) {
+    swigCMemOwn = cMemoryOwn;
+    swigCPtr = cPtr;
+    this.em = em;
+  }
+
+  protected static long getCPtr($javaclassname obj) {
+    return (obj == null) ? 0 : obj.swigCPtr;
+  }
+
+  public JavaIteratorAdapter_UnsatCore iterator() {
+    return new JavaIteratorAdapter_UnsatCore(this.em, this);
+  }
 %}
 
-%ignore CVC4::operator<<(std::ostream&, const UnsatCore&);
+%typemap(javaout) CVC4::Expr {
+  return new Expr(this.em, $jnicall, true);
+}
 
-#ifdef SWIGJAVA
+%ignore CVC4::UnsatCore::UnsatCore();
+%ignore CVC4::UnsatCore::UnsatCore(SmtEngine* smt, std::vector<Expr> core);
 
 // Instead of UnsatCore::begin() and end(), create an
 // iterator() method on the Java side that returns a Java-style
@@ -20,12 +40,8 @@
 %ignore CVC4::UnsatCore::end();
 %ignore CVC4::UnsatCore::begin() const;
 %ignore CVC4::UnsatCore::end() const;
-%extend CVC4::UnsatCore {
-  CVC4::JavaIteratorAdapter<CVC4::UnsatCore, CVC4::Expr> iterator()
-  {
-    return CVC4::JavaIteratorAdapter<CVC4::UnsatCore, CVC4::Expr>(*$self);
-  }
 
+%extend CVC4::UnsatCore {
   std::string toString()
   {
     std::stringstream ss;
@@ -37,36 +53,13 @@
 // UnsatCore is "iterable" on the Java side
 %typemap(javainterfaces) CVC4::UnsatCore "java.lang.Iterable<edu.stanford.CVC4.Expr>";
 
-// the JavaIteratorAdapter should not be public, and implements Iterator
-%typemap(javaclassmodifiers) CVC4::JavaIteratorAdapter<CVC4::UnsatCore, CVC4::Expr> "class";
-%typemap(javainterfaces) CVC4::JavaIteratorAdapter<CVC4::UnsatCore, CVC4::Expr> "java.util.Iterator<edu.stanford.CVC4.Expr>";
-// add some functions to the Java side (do it here because there's no way to do these in C++)
-%typemap(javacode) CVC4::JavaIteratorAdapter<CVC4::UnsatCore, CVC4::Expr> "
-  public void remove() {
-    throw new java.lang.UnsupportedOperationException();
-  }
-
-  public edu.stanford.CVC4.Expr 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<CVC4::UnsatCore, CVC4::Expr>::getNext() "private";
-
 #endif /* SWIGJAVA */
 
 %include "proof/unsat_core.h"
 
 #ifdef SWIGJAVA
 
-%include <std_vector.i>
-
-%include "bindings/java_iterator_adapter.h"
-
+SWIG_JAVA_ITERATOR_ADAPTER(CVC4::UnsatCore, CVC4::Expr)
 %template(JavaIteratorAdapter_UnsatCore) CVC4::JavaIteratorAdapter<CVC4::UnsatCore, CVC4::Expr>;
 
 #endif /* SWIGJAVA */
diff --git a/src/smt/smt_engine.i b/src/smt/smt_engine.i
index 635e593bb..95a5f4f3b 100644
--- a/src/smt/smt_engine.i
+++ b/src/smt/smt_engine.i
@@ -3,51 +3,33 @@
 %}
 
 #ifdef SWIGJAVA
+
 %typemap(javacode) CVC4::SmtEngine %{
   // a ref is kept here to keep Java GC from collecting the EM
   // before the SmtEngine
-  private Object emRef;
-  static final native Object mkRef(Object obj);
-  static final native void dlRef(Object obj);
+  private ExprManager em;
 %}
-%native (mkRef) jobject SmtEngine::mkRef(jobject);
-%native (dlRef) void SmtEngine::dlRef(jobject);
-%{
-extern "C" {
-SWIGEXPORT jobject JNICALL Java_edu_stanford_CVC4_SmtEngine_mkRef(JNIEnv* jenv, jclass jcls, jobject o) {
-  if(o == NULL) {
-    return NULL;
-  }
-  return jenv->NewGlobalRef(o);
+
+%typemap(javaconstruct) SmtEngine {
+  this($imcall, true);
+  this.em = em; // keep ref to expr manager in SWIG proxy class
 }
-SWIGEXPORT void JNICALL Java_edu_stanford_CVC4_SmtEngine_dlRef(JNIEnv* jenv, jclass jcls, jobject o) {
-  if(o != NULL) {
-    jenv->DeleteGlobalRef(o);
-  }
+
+%typemap(javaout) CVC4::Expr {
+  return new Expr(this.em, $jnicall, true);
 }
+
+%typemap(javaout) CVC4::UnsatCore {
+  return new UnsatCore(this.em, $jnicall, true);
 }
-%}
-%typemap(javaconstruct) SmtEngine {
-    this($imcall, true);
-    emRef = mkRef(em); // keep ref to expr manager in SWIG proxy class
-  }
-%typemap(javadestruct, methodname="delete", methodmodifiers="public synchronized") CVC4::SmtEngine {
-    dlRef(emRef);
-    emRef = null;
-    if (swigCPtr != 0) {
-      if (swigCMemOwn) {
-        swigCMemOwn = false;
-        CVC4JNI.delete_SmtEngine(swigCPtr);
-      }
-      swigCPtr = 0;
-    }
-  }
-
-%template(Map_ExprExpr) std::map<CVC4::Expr, CVC4::Expr>;
+
+// %template(Map_ExprExpr) std::map<CVC4::Expr, CVC4::Expr>;
+%ignore CVC4::SmtEngine::getSynthSolutions(std::map<Expr, Expr>& sol_map);
 
 #endif // SWIGJAVA
 
 %ignore CVC4::SmtEngine::setLogic(const char*);
+%ignore CVC4::SmtEngine::setReplayStream(ExprStream* exprStream);
 %ignore CVC4::smt::currentProofManager();
 
 %include "smt/smt_engine.h"
diff --git a/src/util/proof.i b/src/util/proof.i
index 22dff1043..59a524a0f 100644
--- a/src/util/proof.i
+++ b/src/util/proof.i
@@ -2,4 +2,6 @@
 #include "util/proof.h"
 %}
 
+%ignore CVC4::Proof::toStream(std::ostream& out, const ProofLetMap& map) const;
+
 %include "util/proof.h"
diff --git a/src/util/statistics.i b/src/util/statistics.i
index 8d1086dcc..7dfc7ec39 100644
--- a/src/util/statistics.i
+++ b/src/util/statistics.i
@@ -64,12 +64,12 @@
 
 %include <std_pair.i>
 %include <std_string.i>
-%include <std_vector.i>
 
-%include "bindings/java_iterator_adapter.h"
 %include "util/sexpr.h"
 
 %template(Statistic) std::pair<std::string, CVC4::SExpr>;
+
+%feature("valuewrapper") CVC4::JavaIteratorAdapter<CVC4::StatisticsBase, std::pair<std::string, CVC4::SExpr> >;
 %template(JavaIteratorAdapter_StatisticsBase) CVC4::JavaIteratorAdapter<CVC4::StatisticsBase, std::pair<std::string, CVC4::SExpr> >;
 
 #endif /* SWIGJAVA */