Some fixes to GC order in Java.

diff --git a/src/expr/expr.i b/src/expr/expr.i
index 31788f06b0a4630592efc9941a3c7b7493fe4b50..b50686f522b32c3e8e1418651de7a8686345563c 100644 (file)
--- a/src/expr/expr.i
+++ b/src/expr/expr.i
@@ -15,6 +15,50 @@
 %rename(apply) CVC4::ExprHashFunction::operator()(CVC4::Expr) const;
 #endif /* SWIGPYTHON */
 
+#ifdef SWIGJAVA
+%typemap(javabody) CVC4::Expr %{
+  private long swigCPtr;
+  protected boolean swigCMemOwn;
+
+  protected $javaclassname(long cPtr, boolean cMemoryOwn) {
+    swigCMemOwn = cMemoryOwn;
+    swigCPtr = cPtr;
+    this.em = SmtEngine.mkRef(getExprManager()); // 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;
+  }
+%}
+%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 */
+
 %ignore CVC4::operator<<(std::ostream&, const Expr&);
 %ignore CVC4::operator<<(std::ostream&, const TypeCheckingException&);
 
@@ -23,7 +67,7 @@
 %ignore CVC4::expr::operator<<(std::ostream&, ExprDag);
 %ignore CVC4::expr::operator<<(std::ostream&, ExprSetLanguage);
 
-%rename(assign) CVC4::Expr::operator=(const Expr&);
+%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;

diff --git a/src/expr/expr_manager.i b/src/expr/expr_manager.i
index b29f59621b52c712904021e0d508fa11c5eb8614..fccadf43cf6e7e7f669738276942ba6d56a176d9 100644 (file)
--- a/src/expr/expr_manager.i
+++ b/src/expr/expr_manager.i
@@ -7,7 +7,7 @@
   // before the ExprManager
   private Object options;
 %}
-%typemap(javaconstruct) CVC4::ExprManager {
+%typemap(javaconstruct) ExprManager {
     this($imcall, true);
     this.options = SmtEngine.mkRef(options); // keep ref to options in SWIG proxy class
   }

diff --git a/src/expr/type.i b/src/expr/type.i
index 6394dda67ea0839f5867563599fcb4ff3c67798a..16d059eac40f9a6a26db339c7a34132fdc609ab0 100644 (file)
--- a/src/expr/type.i
+++ b/src/expr/type.i
@@ -8,9 +8,52 @@
 %rename(apply) CVC4::TypeHashFunction::operator()(const CVC4::Type&) const;
 #endif /* SWIGPYTHON */
 
+#ifdef SWIGJAVA
+%typemap(javabody) CVC4::Type %{
+  private long swigCPtr;
+  protected boolean swigCMemOwn;
+
+  protected $javaclassname(long cPtr, boolean cMemoryOwn) {
+    swigCMemOwn = cMemoryOwn;
+    swigCPtr = cPtr;
+    this.em = SmtEngine.mkRef(getExprManager()); // keep ref to em in SWIG proxy class
+  }
+
+  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;
+  }
+%}
+%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;
+    }
+  }
+#endif /* SWIGJAVA */
 %ignore CVC4::operator<<(std::ostream&, const Type&);
 
-%rename(assign) CVC4::Type::operator=(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;

diff --git a/src/smt/smt_engine.i b/src/smt/smt_engine.i
index 7bece21b3371efb7720d0d956c5b72884998a3d2..9cf4467a81198a60fe8cbb9636c04e37f5db9d09 100644 (file)
--- a/src/smt/smt_engine.i
+++ b/src/smt/smt_engine.i
@@ -27,7 +27,7 @@ SWIGEXPORT void JNICALL Java_edu_nyu_acsys_CVC4_SmtEngine_dlRef(JNIEnv* jenv, jc
 }
 }
 %}
-%typemap(javaconstruct) CVC4::SmtEngine {
+%typemap(javaconstruct) SmtEngine {
     this($imcall, true);
     emRef = mkRef(em); // keep ref to expr manager in SWIG proxy class
   }