Merge branch 'master' of git@github.com:CVC4/CVC4.git

13 files changed, 243 insertions, 100 deletions

diff --git a/src/Makefile.am b/src/Makefile.am
index b505750d4..1dbf77451 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -137,7 +137,7 @@ gitinfo: gitinfo.tmp
 # .PHONY ensures the .tmp version is always rebuilt (to check for any changes)
 .PHONY: gitinfo.tmp
 gitinfo.tmp:
-	$(AM_V_GEN)(cd "$(top_srcdir)"; if ! grep -q '^ref: refs/heads/' .git/HEAD; then echo; fi; sed 's,^ref: refs/heads/,,' .git/HEAD; git show-ref refs/heads/`sed 's,^ref: refs/heads/,,' .git/HEAD`; echo "Modifications: `test -z \"\`git status -s -uno\`\" && echo false || echo true`") >"$@" 2>/dev/null || true
+	$(AM_V_GEN)(cd "$(top_srcdir)"; if test -e .git/HEAD; then if ! grep -q '^ref: refs/heads/' .git/HEAD; then echo; fi; sed 's,^ref: refs/heads/,,' .git/HEAD; git show-ref refs/heads/`sed 's,^ref: refs/heads/,,' .git/HEAD`; echo "Modifications: `test -z \"\`git status -s -uno\`\" && echo false || echo true`"; fi) >"$@" 2>/dev/null || true
 
 install-data-local:
 	(echo include/cvc4.h; \
diff --git a/src/bindings/Makefile.am b/src/bindings/Makefile.am
index 301150b12..dcc4bc858 100644
--- a/src/bindings/Makefile.am
+++ b/src/bindings/Makefile.am
@@ -163,7 +163,7 @@ CLEANFILES = \
 EXTRA_DIST = \
 	swig.h \
 	java_iterator_adapter.h \
-	java_output_stream_adapter.h
+	java_stream_adapters.h
 
 MOSTLYCLEANFILES = \
         .swig_deps \
diff --git a/src/bindings/java_output_stream_adapter.h b/src/bindings/java_output_stream_adapter.h
deleted file mode 100644
index 6830e508d..000000000
--- a/src/bindings/java_output_stream_adapter.h
+++ /dev/null
@@ -1,50 +0,0 @@
-/*********************                                                        */
-/*! \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 {
-  std::stringstream d_ss;
-
-public:
-  JavaOutputStreamAdapter() { }
-
-  std::string toString() { return d_ss.str(); }
-
-};/* class JavaOutputStreamAdapter */
-
-}/* CVC4 namespace */
-
-#endif /* __CVC4__BINDINGS__JAVA_OUTPUT_STREAM_ADAPTER_H */
diff --git a/src/bindings/java_stream_adapters.h b/src/bindings/java_stream_adapters.h
new file mode 100644
index 000000000..daeb06e18
--- /dev/null
+++ b/src/bindings/java_stream_adapters.h
@@ -0,0 +1,113 @@
+/*********************                                                        */
+/*! \file java_stream_adapters.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 */
+
+#include <sstream>
+#include <set>
+#include <cassert>
+#include <iostream>
+#include <string>
+#include <jni.h>
+
+#ifndef __CVC4__BINDINGS__JAVA_STREAM_ADAPTERS_H
+#define __CVC4__BINDINGS__JAVA_STREAM_ADAPTERS_H
+
+namespace CVC4 {
+
+class JavaOutputStreamAdapter {
+  std::stringstream d_ss;
+
+public:
+  JavaOutputStreamAdapter() { }
+
+  std::string toString() { return d_ss.str(); }
+
+};/* class JavaOutputStreamAdapter */
+
+class JavaInputStreamAdapter : public std::stringstream {
+  static std::set<JavaInputStreamAdapter*> s_adapters;
+  jobject inputStream;
+
+  JavaInputStreamAdapter& operator=(const JavaInputStreamAdapter&);
+  JavaInputStreamAdapter(const JavaInputStreamAdapter&);
+
+public:
+  JavaInputStreamAdapter(jobject inputStream) : inputStream(inputStream) {
+    s_adapters.insert(this);
+  }
+
+  ~JavaInputStreamAdapter() {
+    s_adapters.erase(this);
+  }
+
+  static void pullAdapters(JNIEnv* jenv) {
+    for(std::set<JavaInputStreamAdapter*>::iterator i = s_adapters.begin();
+        i != s_adapters.end();
+        ++i) {
+      (*i)->pull(jenv);
+    }
+  }
+
+  jobject getInputStream() const {
+    return inputStream;
+  }
+
+  void pull(JNIEnv* jenv) {
+    if(fail() || eof()) {
+      clear();
+    }
+    jclass clazz = jenv->FindClass("java/io/InputStream");
+    assert(clazz != NULL && jenv->ExceptionOccurred() == NULL);
+    jmethodID method = jenv->GetMethodID(clazz, "available", "()I");
+    assert(method != NULL && jenv->ExceptionOccurred() == NULL);
+    jint available = jenv->CallIntMethod(inputStream, method);
+    assert(jenv->ExceptionOccurred() == NULL);
+    jbyteArray bytes = jenv->NewByteArray(available);
+    assert(bytes != NULL && jenv->ExceptionOccurred() == NULL);
+    method = jenv->GetMethodID(clazz, "read", "([B)I");
+    assert(method != NULL && jenv->ExceptionOccurred() == NULL);
+    jint nread = jenv->CallIntMethod(inputStream, method, bytes);
+    assert(jenv->ExceptionOccurred() == NULL);
+    jbyte* bptr = jenv->GetByteArrayElements(bytes, NULL);
+    assert(jenv->ExceptionOccurred() == NULL);
+    std::copy(bptr, bptr + nread, std::ostream_iterator<char>(*this));
+    *this << std::flush;
+    jenv->ReleaseByteArrayElements(bytes, bptr, 0);
+    assert(jenv->ExceptionOccurred() == NULL);
+    assert(good());
+    assert(!eof());
+  }
+
+};/* class JavaInputStreamAdapter */
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__BINDINGS__JAVA_STREAM_ADAPTERS_H */
diff --git a/src/cvc4.i b/src/cvc4.i
index 3f11fafc2..925152248 100644
--- a/src/cvc4.i
+++ b/src/cvc4.i
@@ -54,6 +54,9 @@ using namespace CVC4;
 #include "expr/expr.h"
 #include "util/datatype.h"
 #include "expr/command.h"
+#include "bindings/java_stream_adapters.h"
+
+std::set<JavaInputStreamAdapter*> CVC4::JavaInputStreamAdapter::s_adapters;
 %}
 
 %template(vectorCommandPtr) std::vector< CVC4::Command* >;
@@ -72,7 +75,10 @@ using namespace CVC4;
 
 #ifdef SWIGJAVA
 
-%exception {
+#include "bindings/java_iterator_adapter.h"
+#include "bindings/java_stream_adapters.h"
+
+%exception %{
   try {
     $action
   } catch(CVC4::Exception& e) {
@@ -81,12 +87,19 @@ using namespace CVC4;
     std::string explanation = ss.str();
     SWIG_JavaThrowException(jenv, SWIG_JavaRuntimeException, explanation.c_str());
   }
-}
+%}
 
 // Create a mapping from C++ Exceptions to Java Exceptions.
 // This is in a couple of throws typemaps, simply because it's sensitive to SWIG's concept of which namespace we're in.
 %typemap(throws) Exception %{
-  jclass clazz = jenv->FindClass("edu/nyu/acsys/CVC4/$1_type");
+  std::string name = "edu/nyu/acsys/$1_type";
+  size_t i = name.find("::");
+  if(i != std::string::npos) {
+    size_t j = name.rfind("::");
+    assert(i <= j);
+    name.replace(i, j - i + 2, "/");
+  }
+  jclass clazz = jenv->FindClass(name.c_str());
   assert(clazz != NULL && jenv->ExceptionOccurred() == NULL);
   jmethodID method = jenv->GetMethodID(clazz, "<init>", "(JZ)V");
   assert(method != NULL && jenv->ExceptionOccurred() == NULL);
@@ -97,8 +110,11 @@ using namespace CVC4;
 %}
 %typemap(throws) CVC4::Exception %{
   std::string name = "edu/nyu/acsys/$1_type";
-  for(size_t i = name.find("::"); i != std::string::npos; i = name.find("::")) {
-    name.replace(i, 2, "/");
+  size_t i = name.find("::");
+  if(i != std::string::npos) {
+    size_t j = name.rfind("::");
+    assert(i <= j);
+    name.replace(i, j - i + 2, "/");
   }
   jclass clazz = jenv->FindClass(name.c_str());
   assert(clazz != NULL && jenv->ExceptionOccurred() == NULL);
@@ -146,6 +162,76 @@ using namespace CVC4;
          post="    new java.io.PrintStream($javainput).print(temp$javainput.toString());")
          std::ostream& "edu.nyu.acsys.CVC4.JavaOutputStreamAdapter.getCPtr(temp$javainput)"
 
+%typemap(jni) std::istream& "jlong"
+%typemap(jtype) std::istream& "long"
+%typemap(jstype) std::istream& "java.io.InputStream"
+%typemap(javain,
+         pre="    edu.nyu.acsys.CVC4.JavaInputStreamAdapter temp$javainput = edu.nyu.acsys.CVC4.JavaInputStreamAdapter.get($javainput);", pgcppname="temp$javainput",
+         post="")
+         std::istream& "edu.nyu.acsys.CVC4.JavaInputStreamAdapter.getCPtr(temp$javainput)"
+%typemap(in) jobject inputStream %{
+  $1 = jenv->NewGlobalRef($input);
+%}
+%typemap(out) CVC4::JavaInputStreamAdapter* %{
+  $1->pull(jenv);
+  *(CVC4::JavaInputStreamAdapter **)&$result = $1;
+%}
+%typemap(javacode) CVC4::JavaInputStreamAdapter %{
+  private static java.util.HashMap streams = new java.util.HashMap();
+  public static JavaInputStreamAdapter get(java.io.InputStream is) {
+    if(streams.containsKey(is)) {
+      return (JavaInputStreamAdapter) streams.get(is);
+    }
+    JavaInputStreamAdapter adapter = new JavaInputStreamAdapter(is);
+    streams.put(is, adapter);
+    return adapter;
+  }
+%}
+%typemap(javafinalize) CVC4::JavaInputStreamAdapter %{
+  protected void finalize() {
+    streams.remove(getInputStream());
+    delete();
+  }
+%}
+%ignore CVC4::JavaInputStreamAdapter::init(JNIEnv*);
+%ignore CVC4::JavaInputStreamAdapter::pullAdapters(JNIEnv*);
+%javamethodmodifiers CVC4::JavaInputStreamAdapter::getInputStream() const "private";
+%javamethodmodifiers CVC4::JavaInputStreamAdapter::JavaInputStreamAdapter(jobject) "private";
+
+%exception CVC4::parser::Parser::nextCommand() %{
+  try {
+    CVC4::JavaInputStreamAdapter::pullAdapters(jenv);
+    $action
+  } catch(CVC4::Exception& e) {
+    std::stringstream ss;
+    ss << e.what() << ": " << e.getMessage();
+    std::string explanation = ss.str();
+    SWIG_JavaThrowException(jenv, SWIG_JavaRuntimeException, explanation.c_str());
+  }
+%}
+%exception CVC4::parser::Parser::nextExpression() %{
+  try {
+    CVC4::JavaInputStreamAdapter::pullAdapters(jenv);
+    $action
+  } catch(CVC4::Exception& e) {
+    std::stringstream ss;
+    ss << e.what() << ": " << e.getMessage();
+    std::string explanation = ss.str();
+    SWIG_JavaThrowException(jenv, SWIG_JavaRuntimeException, explanation.c_str());
+  }
+%}
+%exception CVC4::JavaInputStreamAdapter::~JavaInputStreamAdapter() %{
+  try {
+    jenv->DeleteGlobalRef(arg1->getInputStream());
+    $action
+  } catch(CVC4::Exception& e) {
+    std::stringstream ss;
+    ss << e.what() << ": " << e.getMessage();
+    std::string explanation = ss.str();
+    SWIG_JavaThrowException(jenv, SWIG_JavaRuntimeException, explanation.c_str());
+  }
+%}
+
 #endif /* SWIGJAVA */
 
 %include "util/integer.i"
diff --git a/src/main/options b/src/main/options
index 9c630270f..14a7a9f3f 100644
--- a/src/main/options
+++ b/src/main/options
@@ -31,8 +31,6 @@ option threadArgv std::vector<std::string> :include <vector> <string>
  Thread configuration (a string to be passed to parseOptions)
 option thread_id int :default -1
  Thread ID, for internal use in case of multi-threaded run
-#option separateOutput bool :default false
-# In multi-threaded setting print output of each thread at the end of run, separated by a divider ("----").
 option sharingFilterByLength --filter-lemma-length=N int :default -1 :read-write
  don't share (among portfolio threads) lemmas strictly longer than N
 option fallbackSequential  --fallback-sequential bool :default false
diff --git a/src/parser/antlr_input.h b/src/parser/antlr_input.h
index 020db0d50..89f6c8db5 100644
--- a/src/parser/antlr_input.h
+++ b/src/parser/antlr_input.h
@@ -185,8 +185,9 @@ public:
   std::string getUnparsedText();
 
   /** Get the ANTLR3 lexer for this input. */
-  pANTLR3_LEXER getAntlr3Lexer(){ return d_lexer; };
+  pANTLR3_LEXER getAntlr3Lexer() { return d_lexer; }
 
+  pANTLR3_INPUT_STREAM getAntlr3InputStream() { return d_antlr3InputStream; }
 protected:
   /** Create an input. This input takes ownership of the given input stream,
    * and will delete it at destruction time.
diff --git a/src/parser/antlr_line_buffered_input.cpp b/src/parser/antlr_line_buffered_input.cpp
index 8c4f1b0be..46853056b 100644
--- a/src/parser/antlr_line_buffered_input.cpp
+++ b/src/parser/antlr_line_buffered_input.cpp
@@ -21,15 +21,11 @@
 #include <cassert>
 
 #include "util/output.h"
+#include "parser/antlr_line_buffered_input.h"
 
 namespace CVC4 {
 namespace parser {
 
-typedef struct ANTLR3_LINE_BUFFERED_INPUT_STREAM {
-  ANTLR3_INPUT_STREAM antlr;
-  std::istream* in;
-} *pANTLR3_LINE_BUFFERED_INPUT_STREAM;
-
 static pANTLR3_INPUT_STREAM    antlr3CreateLineBufferedStream(std::istream& in);
 
 static void
@@ -213,7 +209,9 @@ myLA(pANTLR3_INT_STREAM is, ANTLR3_INT32 la) {
     Debug("pipe") << "LA" << std::endl;
     if	(( ((pANTLR3_UINT8)input->nextChar) + la - 1) >= (((pANTLR3_UINT8)input->data) + input->sizeBuf))
     {
-      std::istream& in = *((pANTLR3_LINE_BUFFERED_INPUT_STREAM)input)->in;
+      std::istream& in = *((CVC4::parser::pANTLR3_LINE_BUFFERED_INPUT_STREAM)input)->in;
+      //MGD
+      // in.clear();
       if(!in) {
         Debug("pipe") << "EOF" << std::endl;
         return	ANTLR3_CHARSTREAM_EOF;
@@ -246,7 +244,7 @@ myLA(pANTLR3_INT_STREAM is, ANTLR3_INT32 la) {
       ++input->sizeBuf;
     }
 
-    Debug("pipe") << "READ POINTER[" << la << "] AT: >>" << std::string(((char*)input->nextChar), input->sizeBuf - (((char*)input->nextChar) - (char*)input->data) + 1) << "<< returning '" << (char)(*((pANTLR3_UINT8)input->nextChar + la - 1)) << "' (" << (unsigned)(*((pANTLR3_UINT8)input->nextChar + la - 1)) << ")" << std::endl;
+    Debug("pipe") << "READ POINTER[" << la << "] AT: >>" << std::string(((char*)input->nextChar), input->sizeBuf - (((char*)input->nextChar) - (char*)input->data)) << "<< returning '" << (char)(*((pANTLR3_UINT8)input->nextChar + la - 1)) << "' (" << (unsigned)(*((pANTLR3_UINT8)input->nextChar + la - 1)) << ")" << std::endl;
     return	(ANTLR3_UCHAR)(*((pANTLR3_UINT8)input->nextChar + la - 1));
 }
 
@@ -356,7 +354,6 @@ antlr3CreateLineBufferedStream(std::istream& in)
         input->isAllocated	= ANTLR3_FALSE;
 
         ((pANTLR3_LINE_BUFFERED_INPUT_STREAM)input)->in = &in;
-
 	// Call the common 8 bit input stream handler
 	// initialization.
 	//
diff --git a/src/parser/antlr_line_buffered_input.h b/src/parser/antlr_line_buffered_input.h
index 83df19a2d..fb0c16dbe 100644
--- a/src/parser/antlr_line_buffered_input.h
+++ b/src/parser/antlr_line_buffered_input.h
@@ -25,6 +25,11 @@
 namespace CVC4 {
 namespace parser {
 
+typedef struct ANTLR3_LINE_BUFFERED_INPUT_STREAM {
+  ANTLR3_INPUT_STREAM antlr;
+  std::istream* in;
+} *pANTLR3_LINE_BUFFERED_INPUT_STREAM;
+
 pANTLR3_INPUT_STREAM
 antlr3LineBufferedStreamNew(std::istream& in, ANTLR3_UINT32 encoding, pANTLR3_UINT8 name);
 
diff --git a/src/parser/bounded_token_buffer.cpp b/src/parser/bounded_token_buffer.cpp
index 6a6ae8609..108b67307 100644
--- a/src/parser/bounded_token_buffer.cpp
+++ b/src/parser/bounded_token_buffer.cpp
@@ -473,9 +473,11 @@ static pANTLR3_COMMON_TOKEN nextToken(pBOUNDED_TOKEN_BUFFER buffer) {
 
   tokenStream = buffer->commonTstream;
 
+  /*
   if( buffer->done == ANTLR3_TRUE ) {
     return &(tokenStream->tstream->tokenSource->eofToken);
   }
+  */
 
   /* Pick out the next token from the token source
    * Remember we just get a pointer (reference if you like) here
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index 8b77362b2..90f17426b 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -446,26 +446,20 @@ Command* Parser::nextCommand() throw(ParserException) {
   if(!d_commandQueue.empty()) {
     cmd = d_commandQueue.front();
     d_commandQueue.pop_front();
-    if(cmd == NULL) {
-      setDone();
-    }
+    setDone(cmd == NULL);
   } else {
-    if(!done()) {
-      try {
-        cmd = d_input->parseCommand();
-        d_commandQueue.push_back(cmd);
-        cmd = d_commandQueue.front();
-        d_commandQueue.pop_front();
-        if(cmd == NULL) {
-          setDone();
-        }
-      } catch(ParserException& e) {
-        setDone();
-        throw;
-      } catch(exception& e) {
-        setDone();
-        parseError(e.what());
-      }
+    try {
+      cmd = d_input->parseCommand();
+      d_commandQueue.push_back(cmd);
+      cmd = d_commandQueue.front();
+      d_commandQueue.pop_front();
+      setDone(cmd == NULL);
+    } catch(ParserException& e) {
+      setDone();
+      throw;
+    } catch(exception& e) {
+      setDone();
+      parseError(e.what());
     }
   }
   Debug("parser") << "nextCommand() => " << cmd << std::endl;
@@ -478,9 +472,7 @@ Expr Parser::nextExpression() throw(ParserException) {
   if(!done()) {
     try {
       result = d_input->parseExpr();
-      if(result.isNull()) {
-        setDone();
-      }
+      setDone(result.isNull());
     } catch(ParserException& e) {
       setDone();
       throw;
diff --git a/src/parser/parser.i b/src/parser/parser.i
index 5e10973d4..5b23555ea 100644
--- a/src/parser/parser.i
+++ b/src/parser/parser.i
@@ -9,14 +9,13 @@ namespace CVC4 {
     %ignore operator<<(std::ostream&, DeclarationCheck);
     %ignore operator<<(std::ostream&, SymbolType);
 
-  class ParserExprStream : public CVC4::ExprStream {
-    Parser* d_parser;
-  public:
-    ParserExprStream(Parser* parser) : d_parser(parser) {}
-    ~ParserExprStream() { delete d_parser; }
-    Expr nextExpr() { return d_parser->nextExpression(); }
-  };/* class Parser::ExprStream */
-
+    class ParserExprStream : public CVC4::ExprStream {
+      Parser* d_parser;
+    public:
+      ParserExprStream(Parser* parser) : d_parser(parser) {}
+      ~ParserExprStream() { delete d_parser; }
+      Expr nextExpr() { return d_parser->nextExpression(); }
+    };/* class Parser::ExprStream */
   }/* namespace CVC4::parser */
 }/* namespace CVC4 */
 
diff --git a/src/util/statistics.i b/src/util/statistics.i
index 74cee5f37..7f3bbe526 100644
--- a/src/util/statistics.i
+++ b/src/util/statistics.i
@@ -4,7 +4,7 @@
 #ifdef SWIGJAVA
 
 #include "bindings/java_iterator_adapter.h"
-#include "bindings/java_output_stream_adapter.h"
+#include "bindings/java_stream_adapters.h"
 
 #endif /* SWIGJAVA */
 %}
@@ -72,7 +72,7 @@
 #ifdef SWIGJAVA
 
 %include "bindings/java_iterator_adapter.h"
-%include "bindings/java_output_stream_adapter.h"
+%include "bindings/java_stream_adapters.h"
 
 %template(JavaIteratorAdapter_StatisticsBase) CVC4::JavaIteratorAdapter<CVC4::StatisticsBase>;