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.

1 files changed, 27 insertions, 34 deletions

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 */