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.

4 files changed, 9 insertions, 10 deletions

diff --git a/examples/SimpleVC.java b/examples/SimpleVC.java
index 943ac3aa0..81e7a1f64 100644
--- a/examples/SimpleVC.java
+++ b/examples/SimpleVC.java
@@ -52,8 +52,7 @@ public class SimpleVC {
     Expr twox_plus_y_geq_3 = em.mkExpr(Kind.GEQ, twox_plus_y, three);
 
     Expr formula =
-      new Expr(em.mkExpr(Kind.AND, x_positive, y_positive)).
-      impExpr(new Expr(twox_plus_y_geq_3));
+        em.mkExpr(Kind.AND, x_positive, y_positive).impExpr(twox_plus_y_geq_3);
 
     System.out.println(
         "Checking entailment of formula " + formula + " with CVC4.");
diff --git a/examples/api/java/BitVectorsAndArrays.java b/examples/api/java/BitVectorsAndArrays.java
index 8283794a5..6adb2a61d 100644
--- a/examples/api/java/BitVectorsAndArrays.java
+++ b/examples/api/java/BitVectorsAndArrays.java
@@ -69,7 +69,7 @@ public class BitVectorsAndArrays {
     Expr old_current = em.mkExpr(Kind.SELECT, current_array, index);
     Expr two = em.mkConst(new BitVector(32, 2));
 
-    vectorExpr assertions = new vectorExpr();
+    vectorExpr assertions = new vectorExpr(em);
     for (int i = 1; i < k; ++i) {
       index = em.mkConst(new BitVector(index_size, new edu.stanford.CVC4.Integer(i)));
       Expr new_current = em.mkExpr(Kind.BITVECTOR_MULT, two, old_current);
diff --git a/examples/api/java/Datatypes.java b/examples/api/java/Datatypes.java
index 7ef05f7e1..5c9b0ef72 100644
--- a/examples/api/java/Datatypes.java
+++ b/examples/api/java/Datatypes.java
@@ -32,11 +32,11 @@ public class Datatypes {
     // symbols are assigned to its constructors, selectors, and testers.
 
     Datatype consListSpec = new Datatype(em, "list"); // give a name
-    DatatypeConstructor cons = new DatatypeConstructor("cons");
+    DatatypeConstructor cons = new DatatypeConstructor(em, "cons");
     cons.addArg("head", em.integerType());
     cons.addArg("tail", new DatatypeSelfType()); // a list
     consListSpec.addConstructor(cons);
-    DatatypeConstructor nil = new DatatypeConstructor("nil");
+    DatatypeConstructor nil = new DatatypeConstructor(em, "nil");
     consListSpec.addConstructor(nil);
 
     System.out.println("spec is:");
diff --git a/examples/api/java/Relations.java b/examples/api/java/Relations.java
index 20e27d33b..f5c5db8a7 100644
--- a/examples/api/java/Relations.java
+++ b/examples/api/java/Relations.java
@@ -82,7 +82,7 @@ public class Relations {
 
     // (declare-sort Person 0)
     Type personType = manager.mkSort("Person", 0);
-    vectorType vector1 = new vectorType();
+    vectorType vector1 = new vectorType(manager);
     vector1.add(personType);
 
     // (Tuple Person)
@@ -90,7 +90,7 @@ public class Relations {
     // (Set (Tuple Person))
     SetType relationArity1 = manager.mkSetType(tupleArity1);
 
-    vectorType vector2 = new vectorType();
+    vectorType vector2 = new vectorType(manager);
     vector2.add(personType);
     vector2.add(personType);
     // (Tuple Person Person)
@@ -99,11 +99,11 @@ public class Relations {
     SetType relationArity2 = manager.mkSetType(tupleArity2);
 
     // empty set
-    EmptySet emptySet = new EmptySet(relationArity1);
+    EmptySet emptySet = new EmptySet(manager, relationArity1);
     Expr emptySetExpr = manager.mkConst(emptySet);
 
     // empty relation
-    EmptySet emptyRelation = new EmptySet(relationArity2);
+    EmptySet emptyRelation = new EmptySet(manager, relationArity2);
     Expr emptyRelationExpr = manager.mkConst(emptyRelation);
 
     // universe set
@@ -174,7 +174,7 @@ public class Relations {
     Expr xxTuple = manager.mkExpr(Kind.APPLY_CONSTRUCTOR, constructor, x, x);
     Expr member = manager.mkExpr(Kind.MEMBER, xxTuple, ancestor);
     Expr notMember = manager.mkExpr(Kind.NOT, member);
-    vectorExpr vectorExpr = new vectorExpr();
+    vectorExpr vectorExpr = new vectorExpr(manager);
     vectorExpr.add(x);
     Expr quantifiedVariables = manager.mkExpr(Kind.BOUND_VAR_LIST, x);
     Expr noSelfAncestor =