* 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.)

diff --git a/src/bindings/java_iterator_adapter.h b/src/bindings/java_iterator_adapter.h
index 16c968a478abe8be0be1b56e87e90831f3335111..61bc683300c263c148cc0e45433eda44b1bad614 100644 (file)
--- 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 e6f7d6786d95f6715069245a417cd47f81ad6880..6830e508d3f72af7da67cccd83f2641ebb58e7fb 100644 (file)
--- 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 5264ff6066ef4aecc841e27503d8d4c6e869f689..3f11fafc25092cc777713ed9fa839c1c200909c7 100644 (file)
--- 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 7356b0ed5390898414a3bade52a95d71839612bd..74cee5f373860be6953f09d3a18c0316179d74f9 100644 (file)
--- 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 aca663e1801ca5a1a64c459c6dbb8c1a22896235..458b42843c6056e7c07586e0e955bfdbdb99bf86 100644 (file)
--- 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)