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, 6 insertions, 12 deletions

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"