Improve memory management in Java bindings (#4629)
authorAndres Noetzli <andres.noetzli@gmail.com>
Thu, 18 Jun 2020 19:21:02 +0000 (12:21 -0700)
committerGitHub <noreply@github.com>
Thu, 18 Jun 2020 19:21:02 +0000 (12:21 -0700)
commit7d16d25dc9c527848eddac8414db22fe63b38e59
treef56c6c16ad424bd6b90c629aa25584a72e6d5acf
parentc752258539ddb4c97b4fcbe7481cb1151ad182d0
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.
27 files changed:
examples/SimpleVC.java
examples/api/java/BitVectorsAndArrays.java
examples/api/java/Datatypes.java
examples/api/java/Relations.java
src/bindings/java/CMakeLists.txt
src/bindings/java/cvc4_std_vector.i [new file with mode: 0644]
src/bindings/java_iterator_adapter.h
src/bindings/java_iterator_adapter.i [new file with mode: 0644]
src/cvc4.i
src/expr/array_store_all.i
src/expr/ascription_type.i
src/expr/datatype.i
src/expr/emptyset.i
src/expr/expr.i
src/expr/expr_manager.i
src/expr/expr_sequence.i
src/expr/record.i [deleted file]
src/expr/type.i
src/expr/variable_type_map.i
src/options/options.i
src/proof/unsat_core.i
src/smt/smt_engine.i
src/util/proof.i
src/util/statistics.i
test/java/BitVectorsAndArrays.java
test/java/CMakeLists.txt
test/java/Issue2846.java [new file with mode: 0644]