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.

diff --git a/examples/api/java/CMakeLists.txt b/examples/api/java/CMakeLists.txt
index 76a55151eb777e5fd348ea6ee62636617c74df16..108ab86148f2890bb068ae159086f9739a7e1fe5 100644 (file)
--- 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 (file)
index 0000000..0dda91a
--- /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 (file)
index 0000000..65c01cf
--- /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);
+    }
+  }
+}

diff --git a/src/bindings/java/CMakeLists.txt b/src/bindings/java/CMakeLists.txt
index 573c2ee91ce4ac0dbe4a64c733cd9d614b7b3250..7b7d93f1da95ba67b3bccbc3bd0e59475740c7e6 100644 (file)
--- a/src/bindings/java/CMakeLists.txt
+++ b/src/bindings/java/CMakeLists.txt
@@ -165,6 +165,7 @@ set(gen_java_files
   ${CMAKE_CURRENT_BINARY_DIR}/SExpr.java
   ${CMAKE_CURRENT_BINARY_DIR}/SExprKeyword.java
   ${CMAKE_CURRENT_BINARY_DIR}/SExprType.java
+  ${CMAKE_CURRENT_BINARY_DIR}/Statistic.java
   ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_CVC4__Model.java
   ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_CVC4__Printer.java
   ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_CVC4__api__Solver.java

diff --git a/src/bindings/java_iterator_adapter.h b/src/bindings/java_iterator_adapter.h
index bf1b22e1b3b5f0b4729a9b8af912f7c27203062f..270fe7baa1e9087e662d9c90e67ca4fe49e9ea62 100644 (file)
--- a/src/bindings/java_iterator_adapter.h
+++ b/src/bindings/java_iterator_adapter.h
@@ -30,30 +30,36 @@
 #ifndef CVC4__BINDINGS__JAVA_ITERATOR_ADAPTER_H
 #define CVC4__BINDINGS__JAVA_ITERATOR_ADAPTER_H
 
-namespace CVC4 {
+#include <type_traits>
 
-template <class T>
-class JavaIteratorAdapter {
-  const T& d_t;
-  typename T::const_iterator d_it;
+namespace CVC4 {
 
-public:
-  JavaIteratorAdapter(const T& t) :
-    d_t(t),
-    d_it(d_t.begin()) {
+template <class T, class value_type>
+class JavaIteratorAdapter
+{
+ public:
+  JavaIteratorAdapter(const T& t) : d_t(t), d_it(d_t.begin())
+  {
+    static_assert(
+        std::is_convertible<typename T::const_iterator::value_type,
+                            value_type>(),
+        "value_type must be convertible from T::const_iterator::value_type");
   }
 
-  bool hasNext() {
-    return d_it != d_t.end();
-  }
+  bool hasNext() { return d_it != d_t.end(); }
 
-  typename T::const_iterator::value_type getNext() {
-    typename T::const_iterator::value_type ret = *d_it;
+  value_type getNext()
+  {
+    value_type ret = *d_it;
     ++d_it;
     return ret;
   }
-};/* class JavaIteratorAdapter<T> */
 
-}/* CVC4 namespace */
+ private:
+  const T& d_t;
+  typename T::const_iterator d_it;
+}; /* class JavaIteratorAdapter<T, value_type> */
+
+}  // namespace CVC4
 
 #endif /* CVC4__BINDINGS__JAVA_ITERATOR_ADAPTER_H */

diff --git a/src/expr/datatype.i b/src/expr/datatype.i
index a903e0241dc5236edf35dd3d0a95aca160ae9cad..6bd5eb82c7825fc5dab9d07b1343e809c205625e 100644 (file)
--- a/src/expr/datatype.i
+++ b/src/expr/datatype.i
@@ -95,8 +95,11 @@
 // iterator() method on the Java side that returns a Java-style
 // Iterator.
 %extend CVC4::Datatype {
-  CVC4::JavaIteratorAdapter<CVC4::Datatype> iterator() {
-    return CVC4::JavaIteratorAdapter<CVC4::Datatype>(*$self);
+  CVC4::JavaIteratorAdapter<CVC4::Datatype, CVC4::DatatypeConstructor>
+  iterator()
+  {
+    return CVC4::JavaIteratorAdapter<CVC4::Datatype, CVC4::DatatypeConstructor>(
+        *$self);
   }
 
   std::string toString() const {
@@ -106,8 +109,12 @@
   }
 }
 %extend CVC4::DatatypeConstructor {
-  CVC4::JavaIteratorAdapter<CVC4::DatatypeConstructor> iterator() {
-    return CVC4::JavaIteratorAdapter<CVC4::DatatypeConstructor>(*$self);
+  CVC4::JavaIteratorAdapter<CVC4::DatatypeConstructor,
+                            CVC4::DatatypeConstructorArg>
+  iterator()
+  {
+    return CVC4::JavaIteratorAdapter<CVC4::DatatypeConstructor,
+                                     CVC4::DatatypeConstructorArg>(*$self);
   }
 
   std::string toString() const {
@@ -129,12 +136,12 @@
 %typemap(javainterfaces) CVC4::DatatypeConstructor "java.lang.Iterable<DatatypeConstructorArg>";
 
 // the JavaIteratorAdapter should not be public, and implements Iterator
-%typemap(javaclassmodifiers) CVC4::JavaIteratorAdapter<CVC4::Datatype> "class";
-%typemap(javaclassmodifiers) CVC4::JavaIteratorAdapter<CVC4::DatatypeConstructor> "class";
-%typemap(javainterfaces) CVC4::JavaIteratorAdapter<CVC4::Datatype> "java.util.Iterator<DatatypeConstructor>";
-%typemap(javainterfaces) CVC4::JavaIteratorAdapter<CVC4::DatatypeConstructor> "java.util.Iterator<DatatypeConstructorArg>";
+%typemap(javaclassmodifiers) CVC4::JavaIteratorAdapter<CVC4::Datatype, CVC4::DatatypeConstructor> "class";
+%typemap(javaclassmodifiers) CVC4::JavaIteratorAdapter<CVC4::DatatypeConstructor, CVC4::DatatypeConstructorArg> "class";
+%typemap(javainterfaces) CVC4::JavaIteratorAdapter<CVC4::Datatype, CVC4::DatatypeConstructor> "java.util.Iterator<DatatypeConstructor>";
+%typemap(javainterfaces) CVC4::JavaIteratorAdapter<CVC4::DatatypeConstructor, CVC4::DatatypeConstructorArg> "java.util.Iterator<DatatypeConstructorArg>";
 // add some functions to the Java side (do it here because there's no way to do these in C++)
-%typemap(javacode) CVC4::JavaIteratorAdapter<CVC4::Datatype> "
+%typemap(javacode) CVC4::JavaIteratorAdapter<CVC4::Datatype, CVC4::DatatypeConstructor> "
   public void remove() {
     throw new java.lang.UnsupportedOperationException();
   }
@@ -147,7 +154,7 @@
     }
   }
 "
-%typemap(javacode) CVC4::JavaIteratorAdapter<CVC4::DatatypeConstructor> "
+%typemap(javacode) CVC4::JavaIteratorAdapter<CVC4::DatatypeConstructor, CVC4::DatatypeConstructorArg> "
   public void remove() {
     throw new java.lang.UnsupportedOperationException();
   }
@@ -161,18 +168,8 @@
   }
 "
 // getNext() just allows C++ iterator access from Java-side next(), make it private
-%javamethodmodifiers CVC4::JavaIteratorAdapter<CVC4::Datatype>::getNext() "private";
-%javamethodmodifiers CVC4::JavaIteratorAdapter<CVC4::DatatypeConstructor>::getNext() "private";
-
-// map the types appropriately.
-%typemap(jni) CVC4::Datatype::iterator::value_type "jobject";
-%typemap(jtype) CVC4::Datatype::iterator::value_type "edu.nyu.acsys.CVC4.DatatypeConstructor";
-%typemap(jstype) CVC4::Datatype::iterator::value_type "edu.nyu.acsys.CVC4.DatatypeConstructor";
-%typemap(javaout) CVC4::Datatype::iterator::value_type { return $jnicall; }
-%typemap(jni) CVC4::DatatypeConstructor::iterator::value_type "jobject";
-%typemap(jtype) CVC4::DatatypeConstructor::iterator::value_type "edu.nyu.acsys.CVC4.DatatypeConstructorArg";
-%typemap(jstype) CVC4::DatatypeConstructor::iterator::value_type "edu.nyu.acsys.CVC4.DatatypeConstructorArg";
-%typemap(javaout) CVC4::DatatypeConstructor::iterator::value_type { return $jnicall; }
+%javamethodmodifiers CVC4::JavaIteratorAdapter<CVC4::Datatype, CVC4::DatatypeConstructor>::getNext() "private";
+%javamethodmodifiers CVC4::JavaIteratorAdapter<CVC4::DatatypeConstructor, CVC4::DatatypeConstructorArg>::getNext() "private";
 
 #endif /* SWIGJAVA */
 
@@ -183,7 +180,7 @@
 %include "bindings/java_iterator_adapter.h"
 %include "bindings/java_stream_adapters.h"
 
-%template(JavaIteratorAdapter_Datatype) CVC4::JavaIteratorAdapter<CVC4::Datatype>;
-%template(JavaIteratorAdapter_DatatypeConstructor) CVC4::JavaIteratorAdapter<CVC4::DatatypeConstructor>;
+%template(JavaIteratorAdapter_Datatype) CVC4::JavaIteratorAdapter<CVC4::Datatype, CVC4::DatatypeConstructor>;
+%template(JavaIteratorAdapter_DatatypeConstructor) CVC4::JavaIteratorAdapter<CVC4::DatatypeConstructor, CVC4::DatatypeConstructorArg>;
 
 #endif /* SWIGJAVA */

diff --git a/src/expr/expr.i b/src/expr/expr.i
index 1d5207c93b3ea1818da1dd03c208e0ff8e3babbf..b172f60ed2076df9730be1de556d40835cfc3913 100644 (file)
--- a/src/expr/expr.i
+++ b/src/expr/expr.i
@@ -92,8 +92,9 @@ namespace CVC4 {
 %ignore CVC4::Expr::begin() const;
 %ignore CVC4::Expr::end() const;
 %extend CVC4::Expr {
-  CVC4::JavaIteratorAdapter<CVC4::Expr> iterator() {
-    return CVC4::JavaIteratorAdapter<CVC4::Expr>(*$self);
+  CVC4::JavaIteratorAdapter<CVC4::Expr, CVC4::Expr> iterator()
+  {
+    return CVC4::JavaIteratorAdapter<CVC4::Expr, CVC4::Expr>(*$self);
   }
 }
 
@@ -101,10 +102,10 @@ namespace CVC4 {
 %typemap(javainterfaces) CVC4::Expr "java.lang.Iterable<edu.nyu.acsys.CVC4.Expr>";
 
 // the JavaIteratorAdapter should not be public, and implements Iterator
-%typemap(javaclassmodifiers) CVC4::JavaIteratorAdapter<CVC4::Expr> "class";
-%typemap(javainterfaces) CVC4::JavaIteratorAdapter<CVC4::Expr> "java.util.Iterator<edu.nyu.acsys.CVC4.Expr>";
+%typemap(javaclassmodifiers) CVC4::JavaIteratorAdapter<CVC4::Expr, CVC4::Expr> "class";
+%typemap(javainterfaces) CVC4::JavaIteratorAdapter<CVC4::Expr, CVC4::Expr> "java.util.Iterator<edu.nyu.acsys.CVC4.Expr>";
 // add some functions to the Java side (do it here because there's no way to do these in C++)
-%typemap(javacode) CVC4::JavaIteratorAdapter<CVC4::Expr> "
+%typemap(javacode) CVC4::JavaIteratorAdapter<CVC4::Expr, CVC4::Expr> "
   public void remove() {
     throw new java.lang.UnsupportedOperationException();
   }
@@ -118,13 +119,7 @@ namespace CVC4 {
   }
 "
 // getNext() just allows C++ iterator access from Java-side next(), make it private
-%javamethodmodifiers CVC4::JavaIteratorAdapter<CVC4::Expr>::getNext() "private";
-
-// map the types appropriately
-%typemap(jni) CVC4::Expr::const_iterator::value_type "jobject";
-%typemap(jtype) CVC4::Expr::const_iterator::value_type "edu.nyu.acsys.CVC4.Expr";
-%typemap(jstype) CVC4::Expr::const_iterator::value_type "edu.nyu.acsys.CVC4.Expr";
-%typemap(javaout) CVC4::Expr::const_iterator::value_type { return $jnicall; }
+%javamethodmodifiers CVC4::JavaIteratorAdapter<CVC4::Expr, CVC4::Expr>::getNext() "private";
 
 #endif /* SWIGJAVA */
 
@@ -161,7 +156,7 @@ namespace CVC4 {
 %include "bindings/java_iterator_adapter.h"
 %include "bindings/java_stream_adapters.h"
 
-%template(JavaIteratorAdapter_Expr) CVC4::JavaIteratorAdapter<CVC4::Expr>;
+%template(JavaIteratorAdapter_Expr) CVC4::JavaIteratorAdapter<CVC4::Expr, CVC4::Expr>;
 
 #endif /* SWIGJAVA */
 

diff --git a/src/proof/unsat_core.i b/src/proof/unsat_core.i
index cee78da0684ccf3f6d51b9a8d33e09f6268de830..d3fd615cecb5c88d04d5d02fc9564cf982227ca8 100644 (file)
--- a/src/proof/unsat_core.i
+++ b/src/proof/unsat_core.i
@@ -21,8 +21,16 @@
 %ignore CVC4::UnsatCore::begin() const;
 %ignore CVC4::UnsatCore::end() const;
 %extend CVC4::UnsatCore {
-  CVC4::JavaIteratorAdapter<CVC4::UnsatCore> iterator() {
-    return CVC4::JavaIteratorAdapter<CVC4::UnsatCore>(*$self);
+  CVC4::JavaIteratorAdapter<CVC4::UnsatCore, CVC4::Expr> iterator()
+  {
+    return CVC4::JavaIteratorAdapter<CVC4::UnsatCore, CVC4::Expr>(*$self);
+  }
+
+  std::string toString()
+  {
+    std::stringstream ss;
+    ss << (*$self);
+    return ss.str();
   }
 }
 
@@ -30,10 +38,10 @@
 %typemap(javainterfaces) CVC4::UnsatCore "java.lang.Iterable<edu.nyu.acsys.CVC4.Expr>";
 
 // the JavaIteratorAdapter should not be public, and implements Iterator
-%typemap(javaclassmodifiers) CVC4::JavaIteratorAdapter<CVC4::UnsatCore> "class";
-%typemap(javainterfaces) CVC4::JavaIteratorAdapter<CVC4::UnsatCore> "java.util.Iterator<edu.nyu.acsys.CVC4.Expr>";
+%typemap(javaclassmodifiers) CVC4::JavaIteratorAdapter<CVC4::UnsatCore, CVC4::Expr> "class";
+%typemap(javainterfaces) CVC4::JavaIteratorAdapter<CVC4::UnsatCore, CVC4::Expr> "java.util.Iterator<edu.nyu.acsys.CVC4.Expr>";
 // add some functions to the Java side (do it here because there's no way to do these in C++)
-%typemap(javacode) CVC4::JavaIteratorAdapter<CVC4::UnsatCore> "
+%typemap(javacode) CVC4::JavaIteratorAdapter<CVC4::UnsatCore, CVC4::Expr> "
   public void remove() {
     throw new java.lang.UnsupportedOperationException();
   }
@@ -47,13 +55,7 @@
   }
 "
 // getNext() just allows C++ iterator access from Java-side next(), make it private
-%javamethodmodifiers CVC4::JavaIteratorAdapter<CVC4::UnsatCore>::getNext() "private";
-
-// map the types appropriately
-%typemap(jni) CVC4::UnsatCore::const_iterator::value_type "jobject";
-%typemap(jtype) CVC4::UnsatCore::const_iterator::value_type "edu.nyu.acsys.CVC4.Expr";
-%typemap(jstype) CVC4::UnsatCore::const_iterator::value_type "edu.nyu.acsys.CVC4.Expr";
-%typemap(javaout) CVC4::UnsatCore::const_iterator::value_type { return $jnicall; }
+%javamethodmodifiers CVC4::JavaIteratorAdapter<CVC4::UnsatCore, CVC4::Expr>::getNext() "private";
 
 #endif /* SWIGJAVA */
 
@@ -61,9 +63,10 @@
 
 #ifdef SWIGJAVA
 
+%include <std_vector.i>
+
 %include "bindings/java_iterator_adapter.h"
-%include "bindings/java_stream_adapters.h"
 
-%template(JavaIteratorAdapter_UnsatCore) CVC4::JavaIteratorAdapter<CVC4::UnsatCore>;
+%template(JavaIteratorAdapter_UnsatCore) CVC4::JavaIteratorAdapter<CVC4::UnsatCore, CVC4::Expr>;
 
 #endif /* SWIGJAVA */

diff --git a/src/smt/command.i b/src/smt/command.i
index 32bda7bbaee9dc52b382e63a8a129ebe3a594b97..ff8094165c840f212440ca4b6fd052e488783427 100644 (file)
--- a/src/smt/command.i
+++ b/src/smt/command.i
@@ -28,8 +28,10 @@
 %ignore CVC4::CommandSequence::begin() const;
 %ignore CVC4::CommandSequence::end() const;
 %extend CVC4::CommandSequence {
-  CVC4::JavaIteratorAdapter<CVC4::CommandSequence> iterator() {
-    return CVC4::JavaIteratorAdapter<CVC4::CommandSequence>(*$self);
+  CVC4::JavaIteratorAdapter<CVC4::CommandSequence, CVC4::Command*> iterator()
+  {
+    return CVC4::JavaIteratorAdapter<CVC4::CommandSequence, CVC4::Command*>(
+        *$self);
   }
 }
 
@@ -37,10 +39,10 @@
 %typemap(javainterfaces) CVC4::CommandSequence "java.lang.Iterable<edu.nyu.acsys.CVC4.Command>";
 
 // the JavaIteratorAdapter should not be public, and implements Iterator
-%typemap(javaclassmodifiers) CVC4::JavaIteratorAdapter<CVC4::CommandSequence> "class";
-%typemap(javainterfaces) CVC4::JavaIteratorAdapter<CVC4::CommandSequence> "java.util.Iterator<edu.nyu.acsys.CVC4.Command>";
+%typemap(javaclassmodifiers) CVC4::JavaIteratorAdapter<CVC4::CommandSequence, CVC4::Command*> "class";
+%typemap(javainterfaces) CVC4::JavaIteratorAdapter<CVC4::CommandSequence, CVC4::Command*> "java.util.Iterator<edu.nyu.acsys.CVC4.Command>";
 // add some functions to the Java side (do it here because there's no way to do these in C++)
-%typemap(javacode) CVC4::JavaIteratorAdapter<CVC4::CommandSequence> "
+%typemap(javacode) CVC4::JavaIteratorAdapter<CVC4::CommandSequence, CVC4::Command*> "
   public void remove() {
     throw new java.lang.UnsupportedOperationException();
   }
@@ -54,13 +56,7 @@
   }
 "
 // getNext() just allows C++ iterator access from Java-side next(), make it private
-%javamethodmodifiers CVC4::JavaIteratorAdapter<CVC4::CommandSequence>::getNext() "private";
-
-// map the types appropriately
-%typemap(jni) CVC4::CommandSequence::const_iterator::value_type "jobject";
-%typemap(jtype) CVC4::CommandSequence::const_iterator::value_type "edu.nyu.acsys.CVC4.Command";
-%typemap(jstype) CVC4::CommandSequence::const_iterator::value_type "edu.nyu.acsys.CVC4.Command";
-%typemap(javaout) CVC4::CommandSequence::const_iterator::value_type { return $jnicall; }
+%javamethodmodifiers CVC4::JavaIteratorAdapter<CVC4::CommandSequence, CVC4::Command*>::getNext() "private";
 
 #endif /* SWIGJAVA */
 
@@ -71,6 +67,6 @@
 %include "bindings/java_iterator_adapter.h"
 %include "bindings/java_stream_adapters.h"
 
-%template(JavaIteratorAdapter_CommandSequence) CVC4::JavaIteratorAdapter<CVC4::CommandSequence>;
+%template(JavaIteratorAdapter_CommandSequence) CVC4::JavaIteratorAdapter<CVC4::CommandSequence, CVC4::Command*>;
 
 #endif /* SWIGJAVA */

diff --git a/src/util/statistics.i b/src/util/statistics.i
index 9ff6757d85b4c01e18ce35016f9f91dde456b479..8d1086dcc4407b37b0604c627a9f780f6da4ec9e 100644 (file)
--- a/src/util/statistics.i
+++ b/src/util/statistics.i
@@ -4,7 +4,6 @@
 #ifdef SWIGJAVA
 
 #include "bindings/java_iterator_adapter.h"
-#include "bindings/java_stream_adapters.h"
 
 #endif /* SWIGJAVA */
 %}
@@ -24,24 +23,29 @@
 %ignore CVC4::StatisticsBase::begin() const;
 %ignore CVC4::StatisticsBase::end() const;
 %extend CVC4::StatisticsBase {
-  CVC4::JavaIteratorAdapter<CVC4::StatisticsBase> iterator() {
-    return CVC4::JavaIteratorAdapter<CVC4::StatisticsBase>(*$self);
+  CVC4::JavaIteratorAdapter<CVC4::StatisticsBase,
+                            std::pair<std::string, CVC4::SExpr> >
+  iterator()
+  {
+    return CVC4::JavaIteratorAdapter<CVC4::StatisticsBase,
+                                     std::pair<std::string, CVC4::SExpr> >(
+        *$self);
   }
 }
 
 // StatisticsBase is "iterable" on the Java side
-%typemap(javainterfaces) CVC4::StatisticsBase "java.lang.Iterable<Object[]>";
+%typemap(javainterfaces) CVC4::StatisticsBase "java.lang.Iterable<Statistic>";
 
 // the JavaIteratorAdapter should not be public, and implements Iterator
-%typemap(javaclassmodifiers) CVC4::JavaIteratorAdapter<CVC4::StatisticsBase> "class";
-%typemap(javainterfaces) CVC4::JavaIteratorAdapter<CVC4::StatisticsBase> "java.util.Iterator<Object[]>";
+%typemap(javaclassmodifiers) CVC4::JavaIteratorAdapter<CVC4::StatisticsBase, std::pair<std::string, CVC4::SExpr> > "class";
+%typemap(javainterfaces) CVC4::JavaIteratorAdapter<CVC4::StatisticsBase, std::pair<std::string, CVC4::SExpr> > "java.util.Iterator<Statistic>";
 // add some functions to the Java side (do it here because there's no way to do these in C++)
-%typemap(javacode) CVC4::JavaIteratorAdapter<CVC4::StatisticsBase> "
+%typemap(javacode) CVC4::JavaIteratorAdapter<CVC4::StatisticsBase, std::pair<std::string, CVC4::SExpr> > "
   public void remove() {
     throw new java.lang.UnsupportedOperationException();
   }
 
-  public Object[] next() {
+  public Statistic next() {
     if(hasNext()) {
       return getNext();
     } else {
@@ -50,22 +54,7 @@
   }
 "
 // getNext() just allows C++ iterator access from Java-side next(), make it private
-%javamethodmodifiers CVC4::JavaIteratorAdapter<CVC4::StatisticsBase>::getNext() "private";
-
-// map the types appropriately.  for statistics, the "payload" of the iterator is an Object[].
-// These Object arrays are always of two elements, the first is a String and the second an
-// SExpr.  (On the C++ side, it is a std::pair<std::string, SExpr>.)
-%typemap(jni) CVC4::StatisticsBase::const_iterator::value_type "jobjectArray";
-%typemap(jtype) CVC4::StatisticsBase::const_iterator::value_type "java.lang.Object[]";
-%typemap(jstype) CVC4::StatisticsBase::const_iterator::value_type "java.lang.Object[]";
-%typemap(javaout) CVC4::StatisticsBase::const_iterator::value_type { return $jnicall; }
-%typemap(out) CVC4::StatisticsBase::const_iterator::value_type {
-      $result = jenv->NewObjectArray(2, jenv->FindClass("java/lang/Object"), $null);
-      jenv->SetObjectArrayElement($result, 0, jenv->NewStringUTF($1.first.c_str()));
-      jclass clazz = jenv->FindClass("edu/nyu/acsys/CVC4/SExpr");
-      jmethodID methodid = jenv->GetMethodID(clazz, "<init>", "(JZ)V");
-      jenv->SetObjectArrayElement($result, 1, jenv->NewObject(clazz, methodid, reinterpret_cast<uintptr_t>(new CVC4::SExpr($1.second)), true));
-    };
+%javamethodmodifiers CVC4::JavaIteratorAdapter<CVC4::StatisticsBase, std::pair<std::string, CVC4::SExpr> >::getNext() "private";
 
 #endif /* SWIGJAVA */
 
@@ -73,9 +62,14 @@
 
 #ifdef SWIGJAVA
 
+%include <std_pair.i>
+%include <std_string.i>
+%include <std_vector.i>
+
 %include "bindings/java_iterator_adapter.h"
-%include "bindings/java_stream_adapters.h"
+%include "util/sexpr.h"
 
-%template(JavaIteratorAdapter_StatisticsBase) CVC4::JavaIteratorAdapter<CVC4::StatisticsBase>;
+%template(Statistic) std::pair<std::string, CVC4::SExpr>;
+%template(JavaIteratorAdapter_StatisticsBase) CVC4::JavaIteratorAdapter<CVC4::StatisticsBase, std::pair<std::string, CVC4::SExpr> >;
 
 #endif /* SWIGJAVA */