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 | |
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')
-rw-r--r-- | src/bindings/java/CMakeLists.txt | 1 | ||||
-rw-r--r-- | src/bindings/java_iterator_adapter.h | 38 | ||||
-rw-r--r-- | src/expr/datatype.i | 45 | ||||
-rw-r--r-- | src/expr/expr.i | 21 | ||||
-rw-r--r-- | src/proof/unsat_core.i | 31 | ||||
-rw-r--r-- | src/smt/command.i | 22 | ||||
-rw-r--r-- | src/util/statistics.i | 46 |
7 files changed, 98 insertions, 106 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 */ diff --git a/src/expr/datatype.i b/src/expr/datatype.i index a903e0241..6bd5eb82c 100644 --- 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 1d5207c93..b172f60ed 100644 --- 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 cee78da06..d3fd615ce 100644 --- 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 32bda7bba..ff8094165 100644 --- 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 9ff6757d8..8d1086dcc 100644 --- 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 */ |