Fix iterators in Java API (#3000)

Fixes #2989. SWIG 3 seems to have an issue properly resolving
`T::const_iterator::value_type` if that type itself is a `typedef`.
This is for example the case in the `UnsatCore` class, which `typedef`s
`const_iterator` to `std::vector<Expr>::const_iterator`. As a
workaround, this commit changes the `JavaIteratorAdapter` class to take
two template parameters, one of which is the `value_type`. The commit
also adds a compile-time assertion that `T::const_iterator::value_type`
can be converted to `value_type` to avoid nasty surprises. A nice
side-effect of this solution is that explicit `typemap`s are not
necessary anymore, so they are removed. Additionally, the commit adds a
`toString()` method for the Java API of `UnsatCore` and adds examples
that show and test the iteration over the unsat core and the statistics.
Iterating over `Statistics` now returns instances of `Statistic` instead
of `Object[]`, which is a bit cleaner and requires less glue code.

3 files changed, 101 insertions, 0 deletions

diff --git a/examples/api/java/CMakeLists.txt b/examples/api/java/CMakeLists.txt
index 76a55151e..108ab8614 100644
--- a/examples/api/java/CMakeLists.txt
+++ b/examples/api/java/CMakeLists.txt
@@ -12,7 +12,9 @@ set(EXAMPLES_API_JAVA
   LinearArith
   ## disabled until bindings for the new API are in place (issue #2284)
   #PipedInput
+  Statistics
   Strings
+  UnsatCores
 )
 
 foreach(example ${EXAMPLES_API_JAVA})
diff --git a/examples/api/java/Statistics.java b/examples/api/java/Statistics.java
new file mode 100644
index 000000000..0dda91aee
--- /dev/null
+++ b/examples/api/java/Statistics.java
@@ -0,0 +1,45 @@
+/*********************                                                        */
+/*! \file Statistics.java
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andres Noetzli
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 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 An example of accessing CVC4's statistics using the Java API
+ **
+ ** An example of accessing CVC4's statistics using the Java API.
+ **/
+
+import edu.nyu.acsys.CVC4.*;
+import java.util.Iterator;
+
+public class Statistics {
+  public static void main(String[] args) {
+    System.loadLibrary("cvc4jni");
+
+    ExprManager em = new ExprManager();
+    SmtEngine smt = new SmtEngine(em);
+
+    Type boolType = em.booleanType();
+    Expr a = em.mkVar("A", boolType);
+    Expr b = em.mkVar("B", boolType);
+
+    // A ^ B
+    smt.assertFormula(em.mkExpr(Kind.AND, a, b));
+
+    Result res = smt.checkSat();
+
+    // Get the statistics from the `SmtEngine` and iterate over them. The
+    // `Statistics` class implements the `Iterable<Statistic>` interface. A
+    // `Statistic` is a pair that consists of a name and an `SExpr` that stores
+    // the value of the statistic.
+    edu.nyu.acsys.CVC4.Statistics stats = smt.getStatistics();
+    for (Statistic stat : stats) {
+      System.out.println(stat.getFirst() + " = " + stat.getSecond());
+    }
+  }
+}
diff --git a/examples/api/java/UnsatCores.java b/examples/api/java/UnsatCores.java
new file mode 100644
index 000000000..65c01cf5a
--- /dev/null
+++ b/examples/api/java/UnsatCores.java
@@ -0,0 +1,54 @@
+/*********************                                                        */
+/*! \file UnsatCore.java
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andres Noetzli
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 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 An example of interacting with unsat cores using CVC4's Java API
+ **
+ ** An example of interacting with unsat cores using CVC4's Java API.
+ **/
+
+import edu.nyu.acsys.CVC4.*;
+import java.util.Iterator;
+
+public class UnsatCores {
+  public static void main(String[] args) {
+    System.loadLibrary("cvc4jni");
+
+    ExprManager em = new ExprManager();
+    SmtEngine smt = new SmtEngine(em);
+
+    // Enable the production of unsat cores
+    smt.setOption("produce-unsat-cores", new SExpr(true));
+
+    Type boolType = em.booleanType();
+    Expr a = em.mkVar("A", boolType);
+    Expr b = em.mkVar("B", boolType);
+
+    // A ^ B
+    smt.assertFormula(em.mkExpr(Kind.AND, a, b));
+    // ~(A v B)
+    smt.assertFormula(em.mkExpr(Kind.NOT, em.mkExpr(Kind.OR, a, b)));
+
+    Result res = smt.checkSat(); // result is unsat
+
+    // Retrieve the unsat core
+    UnsatCore unsatCore = smt.getUnsatCore();
+    
+    // Print the unsat core
+    System.out.println("Unsat Core: " + unsatCore);
+
+    // Iterate over expressions in the unsat core. The `UnsatCore` class
+    // implements the `Iterable<Expr>` interface.
+    System.out.println("--- Unsat Core ---");
+    for (Expr e : unsatCore) {
+      System.out.println(e);
+    }
+  }
+}