diff options
Diffstat (limited to 'src/cvc4.i')
-rw-r--r-- | src/cvc4.i | 255 |
1 files changed, 0 insertions, 255 deletions
diff --git a/src/cvc4.i b/src/cvc4.i deleted file mode 100644 index 9fc8ed60e..000000000 --- a/src/cvc4.i +++ /dev/null @@ -1,255 +0,0 @@ -// Declare that all functions in the interface can throw exceptions of type -// CVC4::Exception and exceptions in general. SWIG catches those exceptions and -// turns them into target language exceptions via "throws" typemaps. -%catches(CVC4::Exception,...); - -%import "bindings/swig.h" - -%include "stdint.i" -%include "stl.i" - -%module CVC4 -// nspace completely broken with Java packaging -//%nspace; - -namespace std { - class istream; - class ostream; - template <class T> class set {}; - template <class K, class V, class H> class unordered_map {}; -} - -%{ -namespace CVC4 {} -using namespace CVC4; - -#include <cassert> -#include <unordered_map> -#include <iosfwd> -#include <set> -#include <string> -#include <typeinfo> -#include <vector> - -#include "base/exception.h" -#include "base/modal_exception.h" -#include "expr/datatype.h" -#include "expr/expr.h" -#include "expr/type.h" -#include "options/option_exception.h" -#include "smt/command.h" -#include "util/bitvector.h" -#include "util/floatingpoint.h" -#include "util/iand.h" -#include "util/integer.h" -#include "util/sexpr.h" -#include "util/unsafe_interrupt_exception.h" - -#ifdef SWIGJAVA -#include "bindings/java_stream_adapters.h" -std::set<JavaInputStreamAdapter*> CVC4::JavaInputStreamAdapter::s_adapters; -#endif -%} - -#ifdef SWIGPYTHON -%pythonappend CVC4::SmtEngine::SmtEngine %{ - self.thisown = 0 -%} -%pythonappend CVC4::ExprManager::ExprManager %{ - self.thisown = 0 -%} -#endif /* SWIGPYTHON */ - -%template(vectorUnsignedInt) std::vector< unsigned int >; -%template(vectorSExpr) std::vector< CVC4::SExpr >; -%template(vectorString) std::vector< std::string >; -%template(setOfType) std::set< CVC4::Type >; - -// This is unfortunate, but seems to be necessary; if we leave NULL -// defined, swig will expand it to "(void*) 0", and some of swig's -// helper functions won't compile properly. -#undef NULL - -#ifdef SWIGJAVA - -// Map C++ exceptions of type CVC4::Exception to Java exceptions of type -// edu.stanford.CVC4.Exception -// -// As suggested in: -// http://www.swig.org/Doc3.0/SWIGDocumentation.html#Java_exception_typemap -%typemap(throws, throws="edu.stanford.CVC4.Exception") CVC4::Exception { - jclass excep = jenv->FindClass("edu/stanford/CVC4/Exception"); - if (excep) - jenv->ThrowNew(excep, $1.what()); - return $null; -} - -%include "bindings/java_iterator_adapter.i" -%include "java/typemaps.i" // primitive pointers and references -%include "java/std_string.i" // map std::string to java.lang.String -%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.stanford.CVC4.JavaOutputStreamAdapter temp$javainput = new edu.stanford.CVC4.JavaOutputStreamAdapter();", pgcppname="temp$javainput", - post=" new java.io.PrintStream($javainput).print(temp$javainput.toString());") - std::ostream& "edu.stanford.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.stanford.CVC4.JavaInputStreamAdapter temp$javainput = edu.stanford.CVC4.JavaInputStreamAdapter.get($javainput);", pgcppname="temp$javainput", - post="") - std::istream& "edu.stanford.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<java.io.InputStream, JavaInputStreamAdapter> streams = - new java.util.HashMap<java.io.InputStream, JavaInputStreamAdapter>(); - 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*); -%ignore CVC4::JavaInputStreamAdapter::pull(JNIEnv*); -%javamethodmodifiers CVC4::JavaInputStreamAdapter::getInputStream() const "private"; -%javamethodmodifiers CVC4::JavaInputStreamAdapter::JavaInputStreamAdapter(jobject) "private"; - -%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()); - } -%} - -/* Copied (and modified) from java.swg; the standard swig version causes - * negative BigInteger to be interpreted unsigned. Here we throw an - * exception. */ -%typemap(in) unsigned long long { - jclass clazz; - jmethodID mid; - jbyteArray ba; - jbyte* bae; - jsize sz; - int i; - - if (!$input) { - SWIG_JavaThrowException(jenv, SWIG_JavaNullPointerException, "BigInteger null"); - return $null; - } - clazz = JCALL1(GetObjectClass, jenv, $input); - mid = JCALL3(GetMethodID, jenv, clazz, "toByteArray", "()[B"); - ba = (jbyteArray)JCALL2(CallObjectMethod, jenv, $input, mid); - bae = JCALL2(GetByteArrayElements, jenv, ba, 0); - sz = JCALL1(GetArrayLength, jenv, ba); - if((bae[0] & 0x80) != 0) { - SWIG_JavaThrowException(jenv, SWIG_JavaRuntimeException, "BigInteger argument must be nonnegative."); - } - jsize test_sz = sz; - if(sz > 1 && bae[0] == 0) { - --test_sz; - } - if(test_sz > sizeof(unsigned long long)) { - SWIG_JavaThrowException(jenv, SWIG_JavaRuntimeException, "BigInteger argument out of bounds."); - } - $1 = 0; - for(i=0; i<sz; i++) { - $1 = ($1 << 8) | ($1_type)(unsigned char)bae[i]; - } - JCALL3(ReleaseByteArrayElements, jenv, ba, bae, 0); -} - -%include "bindings/java_stream_adapters.h" - -#endif /* SWIGJAVA */ - -// TIM: -// At the moment, the header includes seem to need to follow a special order. -// I don't know why. I am following the build order -%include "base/configuration.i" -%include "base/exception.i" -%include "base/modal_exception.i" - -%include "options/language.i" - -// Tim: "util/integer.i" must come before util/{rational.i,bitvector.i}. -%include "util/integer.i" -%include "util/rational.i" -%include "util/bitvector.i" -%include "util/iand.i" -%include "util/floatingpoint.i" - -// Tim: The remainder of util/. -%include "util/bool.i" -%include "util/cardinality.i" -%include "util/hash.i" -%include "util/proof.i" -%include "util/regexp.i" -%include "util/result.i" -%include "util/sexpr.i" -%include "util/statistics.i" -%include "util/string.i" -%include "util/tuple.i" -%include "util/unsafe_interrupt_exception.i" - -%include "expr/uninterpreted_constant.i" -%include "expr/array_store_all.i" -%include "expr/ascription_type.i" -%include "expr/emptyset.i" -%include "expr/expr_sequence.i" -%include "proof/unsat_core.i" - -// TIM: -// Have these before the rest of expr/. -// Again, no clue why. -%include "expr/array.i" -%include "expr/kind.i" -%include "expr/type.i" - -// TIM: -// The remainder of the includes: -%include "expr/datatype.i" -%include "expr/expr.i" -%include "expr/expr_manager.i" -%include "expr/variable_type_map.i" -%include "options/option_exception.i" -%include "options/options.i" -%include "smt/logic_exception.i" -%include "theory/logic_info.i" -%include "theory/theory_id.i" - -%include "expr/array_store_all.i" - -// Tim: This should come after "theory/logic_info.i". -%include "smt/smt_engine.i" |