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.

3 files changed, 66 insertions, 1 deletions

diff --git a/test/java/BitVectorsAndArrays.java b/test/java/BitVectorsAndArrays.java
index dc78f89c2..c60c49696 100644
--- a/test/java/BitVectorsAndArrays.java
+++ b/test/java/BitVectorsAndArrays.java
@@ -76,7 +76,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)));
diff --git a/test/java/CMakeLists.txt b/test/java/CMakeLists.txt
index 169013b84..213c6ab8e 100644
--- a/test/java/CMakeLists.txt
+++ b/test/java/CMakeLists.txt
@@ -7,6 +7,7 @@ set(java_test_src_files
   BitVectorsAndArrays.java
   Combination.java
   HelloWorld.java
+  Issue2846.java
   LinearArith.java
 )
 
diff --git a/test/java/Issue2846.java b/test/java/Issue2846.java
new file mode 100644
index 000000000..b41258c29
--- /dev/null
+++ b/test/java/Issue2846.java
@@ -0,0 +1,64 @@
+/*********************                                                        */
+/*! \file BitVectorsAndArrays.java
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andres Noetzli
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Test case for issue #2846
+ **
+ ** This test case tests whether the dependency information for keeping the
+ ** ExprManager alive is maintained correctly.
+ **/
+
+import edu.stanford.CVC4.*;
+import org.junit.Test;
+
+public class Issue2846 {
+  static {
+    System.loadLibrary("cvc4jni");
+  }
+
+  @Test
+  public void test() throws InterruptedException {
+    testInternal();
+    gc("h");
+  }
+
+  private static void testInternal() throws InterruptedException {
+    ExprManager em = new ExprManager();
+    SmtEngine smt = new SmtEngine(em);
+    smt.setOption("produce-models", new SExpr(true));
+    Expr x = em.mkVar("x", em.integerType());
+    Expr y = em.mkVar("y", em.integerType());
+    Expr z = em.mkVar("z", em.integerType());
+    gc("a");
+    Expr a1 = em.mkExpr(Kind.GT, x, em.mkExpr(Kind.PLUS, y, z));
+    gc("b");
+    smt.assertFormula(a1);
+    gc("c");
+    Expr a2 = em.mkExpr(Kind.LT, y, z);
+    gc("d");
+    smt.assertFormula(a2);
+    gc("e");
+    System.out.println(a1);
+    System.out.println(a2);
+    gc("f");
+    Result res = smt.checkSat();
+    gc("g");
+    System.out.println("Res = " + res);
+    System.out.println("x =  " + smt.getValue(x));
+    System.out.println("y =  " + smt.getValue(y));
+    System.out.println("z =  " + smt.getValue(z));
+  }
+
+  private static void gc(String msg) throws InterruptedException {
+    System.out.println("calling gc " + msg);
+    Thread.sleep(100);
+    System.gc();
+  }
+}