diff options
| -rw-r--r-- | src/bindings/java_iterator_adapter.h | 34 | ||||
| -rw-r--r-- | src/bindings/java_output_stream_adapter.h | 37 | ||||
| -rw-r--r-- | src/cvc4.i | 10 | ||||
| -rw-r--r-- | src/util/statistics.i | 17 | ||||
| -rw-r--r-- | test/regress/regress0/datatypes/Makefile.am | 6 |
5 files changed, 97 insertions, 7 deletions
diff --git a/src/bindings/java_iterator_adapter.h b/src/bindings/java_iterator_adapter.h index 16c968a47..61bc68330 100644 --- a/src/bindings/java_iterator_adapter.h +++ b/src/bindings/java_iterator_adapter.h @@ -1,3 +1,35 @@ +/********************* */ +/*! \file java_iterator_adapter.h + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief An iterator adapter for the Java bindings, giving Java iterators + ** the ability to access elements from STL iterators. + ** + ** An iterator adapter for the Java bindings, giving Java iterators the + ** ability to access elements from STL iterators. This class is mapped + ** into Java by SWIG, where it implements Iterator (some additional + ** Java-side functions are added by the SWIG layer to implement the full + ** interface). + ** + ** The functionality requires significant assistance from the ".i" SWIG + ** interface files, applying a variety of typemaps. + **/ + +// private to the bindings layer +#ifndef SWIGJAVA +# error This should only be included from the Java bindings layer. +#endif /* SWIGJAVA */ + +#ifndef __CVC4__BINDINGS__JAVA_ITERATOR_ADAPTER_H +#define __CVC4__BINDINGS__JAVA_ITERATOR_ADAPTER_H + namespace CVC4 { template <class T> @@ -23,3 +55,5 @@ public: };/* class JavaIteratorAdapter<T> */ }/* CVC4 namespace */ + +#endif /* __CVC4__BINDINGS__JAVA_ITERATOR_ADAPTER_H */ diff --git a/src/bindings/java_output_stream_adapter.h b/src/bindings/java_output_stream_adapter.h index e6f7d6786..6830e508d 100644 --- a/src/bindings/java_output_stream_adapter.h +++ b/src/bindings/java_output_stream_adapter.h @@ -1,3 +1,38 @@ +/********************* */ +/*! \file java_output_stream_adapter.h + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief An OutputStream adapter for the Java bindings + ** + ** An OutputStream adapter for the Java bindings. This works with a lot + ** of help from SWIG, and custom typemaps in the ".i" SWIG interface files + ** for CVC4. The basic idea is that, when a CVC4 function with a + ** std::ostream& parameter is called, a Java-side binding is generated + ** taking a java.io.OutputStream. Now, the problem is that std::ostream + ** has no Java equivalent, and java.io.OutputStream has no C++ equivalent, + ** so we use this class (which exists on both sides) as the go-between. + ** The wrapper connecting the Java function (taking an OutputStream) and + ** the C++ function (taking an ostream) creates a JavaOutputStreamAdapter, + ** and call the C++ function with the stringstream inside. After the call, + ** the generated stream material is collected and output to the Java-side + ** OutputStream. + **/ + +// private to the bindings layer +#ifndef SWIGJAVA +# error This should only be included from the Java bindings layer. +#endif /* SWIGJAVA */ + +#ifndef __CVC4__BINDINGS__JAVA_OUTPUT_STREAM_ADAPTER_H +#define __CVC4__BINDINGS__JAVA_OUTPUT_STREAM_ADAPTER_H + namespace CVC4 { class JavaOutputStreamAdapter { @@ -11,3 +46,5 @@ public: };/* class JavaOutputStreamAdapter */ }/* CVC4 namespace */ + +#endif /* __CVC4__BINDINGS__JAVA_OUTPUT_STREAM_ADAPTER_H */ diff --git a/src/cvc4.i b/src/cvc4.i index 5264ff606..3f11fafc2 100644 --- a/src/cvc4.i +++ b/src/cvc4.i @@ -133,10 +133,18 @@ using namespace CVC4; %include "java/arrays_java.i" // C arrays to Java arrays %include "java/various.i" // map char** to java.lang.String[] +// Functions on the C++ side taking std::ostream& should on the Java side +// take a java.io.OutputStream. A JavaOutputStreamAdapter is created in +// the wrapper which creates and passes on a std::stringstream to the C++ +// function. Then on exit, the string from the stringstream is dumped to +// the Java-side OutputStream. %typemap(jni) std::ostream& "jlong" %typemap(jtype) std::ostream& "long" %typemap(jstype) std::ostream& "java.io.OutputStream" -%typemap(javain, pre=" edu.nyu.acsys.CVC4.JavaOutputStreamAdapter temp$javainput = new edu.nyu.acsys.CVC4.JavaOutputStreamAdapter();", pgcppname="temp$javainput", post=" new java.io.PrintStream($javainput).print(temp$javainput.toString());") std::ostream& "edu.nyu.acsys.CVC4.JavaOutputStreamAdapter.getCPtr(temp$javainput)" +%typemap(javain, + pre=" edu.nyu.acsys.CVC4.JavaOutputStreamAdapter temp$javainput = new edu.nyu.acsys.CVC4.JavaOutputStreamAdapter();", pgcppname="temp$javainput", + post=" new java.io.PrintStream($javainput).print(temp$javainput.toString());") + std::ostream& "edu.nyu.acsys.CVC4.JavaOutputStreamAdapter.getCPtr(temp$javainput)" #endif /* SWIGJAVA */ 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[]"; diff --git a/test/regress/regress0/datatypes/Makefile.am b/test/regress/regress0/datatypes/Makefile.am index aca663e18..458b42843 100644 --- a/test/regress/regress0/datatypes/Makefile.am +++ b/test/regress/regress0/datatypes/Makefile.am @@ -19,7 +19,9 @@ MAKEFLAGS = -k TESTS = \ tuple.cvc \ rec1.cvc \ + rec2.cvc \ rec4.cvc \ + rec5.cvc \ datatype.cvc \ datatype0.cvc \ datatype1.cvc \ @@ -40,11 +42,9 @@ TESTS = \ v3l60006.cvc \ v5l30058.cvc \ bug286.cvc \ - wrong-sel-simp.cvc \ - rec2.cvc + wrong-sel-simp.cvc FAILING_TESTS = \ - rec5.cvc \ datatype-dump.cvc EXTRA_DIST = $(TESTS) |