diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2019-05-16 00:18:48 +0000 |
---|---|---|
committer | Aina Niemetz <aina.niemetz@gmail.com> | 2019-05-15 17:18:48 -0700 |
commit | 62d361071ea54c9b7cba882313ab4dedef6f1286 (patch) | |
tree | 2e721a2fb77769a2824955a2b47fdf8b86203da3 /src/bindings | |
parent | fc8907afc08d7b418471a537f9c23e9964df82df (diff) |
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.
Diffstat (limited to 'src/bindings')
-rw-r--r-- | src/bindings/java/CMakeLists.txt | 1 | ||||
-rw-r--r-- | src/bindings/java_iterator_adapter.h | 38 |
2 files changed, 23 insertions, 16 deletions
diff --git a/src/bindings/java/CMakeLists.txt b/src/bindings/java/CMakeLists.txt index 573c2ee91..7b7d93f1d 100644 --- 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 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 */ |