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.

10 files changed, 940 insertions, 289 deletions

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);