EXTRA_DIST = \
swig.h \
java_iterator_adapter.h \
- java_output_stream_adapter.h
+ java_stream_adapters.h
MOSTLYCLEANFILES = \
.swig_deps \
+++ /dev/null
-/********************* */
-/*! \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 */
--- /dev/null
+/********************* */
+/*! \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 */
#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* >;
#ifdef SWIGJAVA
-%exception {
+#include "bindings/java_iterator_adapter.h"
+#include "bindings/java_stream_adapters.h"
+
+%exception %{
try {
$action
} catch(CVC4::Exception& e) {
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);
%}
%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);
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"
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.
#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
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;
++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));
}
input->isAllocated = ANTLR3_FALSE;
((pANTLR3_LINE_BUFFERED_INPUT_STREAM)input)->in = ∈
-
// Call the common 8 bit input stream handler
// initialization.
//
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);
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
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;
if(!done()) {
try {
result = d_input->parseExpr();
- if(result.isNull()) {
- setDone();
- }
+ setDone(result.isNull());
} catch(ParserException& e) {
setDone();
throw;
%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 */
#ifdef SWIGJAVA
#include "bindings/java_iterator_adapter.h"
-#include "bindings/java_output_stream_adapter.h"
+#include "bindings/java_stream_adapters.h"
#endif /* SWIGJAVA */
%}
#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>;
projects / cvc5.git / commitdiff