From 62d361071ea54c9b7cba882313ab4dedef6f1286 Mon Sep 17 00:00:00 2001
From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Thu, 16 May 2019 00:18:48 +0000
Subject: 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.
---
 src/bindings/java_iterator_adapter.h | 38 +++++++++++++++++++++---------------
 1 file changed, 22 insertions(+), 16 deletions(-)

(limited to 'src/bindings/java_iterator_adapter.h')

diff --git a/src/bindings/java_iterator_adapter.h b/src/bindings/java_iterator_adapter.h
index bf1b22e1b..270fe7baa 100644
--- 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 */
-- 
cgit v1.2.3