diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-11-17 18:57:16 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-11-17 18:57:16 +0000 |
commit | 2cc71c7863a0c481cf6a4a9e18a59d17b62a905d (patch) | |
tree | e53df57a7c44171edd7494da7a840060fda37543 /src/util/statistics.i | |
parent | 943870920431bf1d6f6f1eb163eb82fb26bdad58 (diff) |
* enable previously-failing (now succeeding) datatype example that uses records
* some bindings cleanup
(this commit was certified error- and warning-free by the test-and-commit script.)
Diffstat (limited to 'src/util/statistics.i')
-rw-r--r-- | src/util/statistics.i | 17 |
1 files changed, 14 insertions, 3 deletions
diff --git a/src/util/statistics.i b/src/util/statistics.i index 7356b0ed5..74cee5f37 100644 --- a/src/util/statistics.i +++ b/src/util/statistics.i @@ -14,6 +14,9 @@ #ifdef SWIGJAVA +// Instead of StatisticsBase::begin() and end(), create an +// iterator() method on the Java side that returns a Java-style +// Iterator. %ignore CVC4::StatisticsBase::begin(); %ignore CVC4::StatisticsBase::end(); %ignore CVC4::StatisticsBase::begin() const; @@ -24,16 +27,19 @@ } } -%typemap(javainterfaces) CVC4::StatisticsBase "java.lang.Iterable<Object>"; +// StatisticsBase is "iterable" on the Java side +%typemap(javainterfaces) CVC4::StatisticsBase "java.lang.Iterable<Object[]>"; +// 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"; +%typemap(javainterfaces) CVC4::JavaIteratorAdapter<CVC4::StatisticsBase> "java.util.Iterator<Object[]>"; +// 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> " public void remove() { throw new java.lang.UnsupportedOperationException(); } - public Object next() { + public Object[] next() { if(hasNext()) { return getNext(); } else { @@ -41,7 +47,12 @@ } } " +// 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[]"; |