src/cvc4.i

   1 %import "bindings/swig.h"
   2
   3 %include "stdint.i"
   4 %include "stl.i"
   5
   6 %module CVC4
   7 // nspace completely broken with Java packaging
   8 //%nspace;
   9
  10 namespace std {
  11   class istream;
  12   class ostream;
  13   template <class T> class set {};
  14   template <class K, class V, class H> class hash_map {};
  15 }
  16
  17 %{
  18 // Perl's headers define "seed" to Perl_seed, which breaks
  19 // gmpxx.h; undo the damage for our CVC4 module.
  20 #ifdef SWIGPERL
  21 #  undef seed
  22 #endif /* SWIGPERL */
  23
  24 // OCaml's headers define "invalid_argument" and "flush" to
  25 // caml_invalid_argument and caml_flush, which breaks C++
  26 // standard headers; undo this damage
  27 //
  28 // Unfortunately, this code isn't inserted early enough.  swig puts
  29 // an include <stdexcept> very early, which breaks linking due to a
  30 // nonexistent std::caml_invalid_argument symbol.. ridiculous!
  31 //
  32 #ifdef SWIGOCAML
  33 #  if defined(flush) || defined(invalid_argument)
  34 #    error "flush" or "invalid_argument" (or both) is defined by the ocaml headers.  You must #undef it above before inclusion of <stdexcept>.
  35 #  endif /* flush */
  36 #  undef flush
  37 #  undef invalid_argument
  38 #endif /* SWIGOCAML */
  39
  40 namespace CVC4 {}
  41 using namespace CVC4;
  42
  43 #include <iostream>
  44 #include <vector>
  45 #include <set>
  46 #include <string>
  47 #include <ext/hash_map>
  48 #include <typeinfo>
  49 #include <cassert>
  50
  51 #include "util/sexpr.h"
  52 #include "util/exception.h"
  53 #include "expr/type.h"
  54 #include "expr/expr.h"
  55 #include "util/datatype.h"
  56 #include "expr/command.h"
  57 #include "bindings/java_stream_adapters.h"
  58
  59 std::set<JavaInputStreamAdapter*> CVC4::JavaInputStreamAdapter::s_adapters;
  60 %}
  61
  62 %template(vectorCommandPtr) std::vector< CVC4::Command* >;
  63 %template(vectorType) std::vector< CVC4::Type >;
  64 %template(vectorExpr) std::vector< CVC4::Expr >;
  65 %template(vectorVectorExpr) std::vector< std::vector< CVC4::Expr > >;
  66 %template(vectorDatatypeType) std::vector< CVC4::DatatypeType >;
  67 %template(vectorSExpr) std::vector< CVC4::SExpr >;
  68 %template(vectorString) std::vector< std::string >;
  69 %template(setType) std::set< CVC4::Type >;
  70 %template(hashmapExpr) std::hash_map< CVC4::Expr, CVC4::Expr, CVC4::ExprHashFunction >;
  71
  72 // This is unfortunate, but seems to be necessary; if we leave NULL
  73 // defined, swig will expand it to "(void*) 0", and some of swig's
  74 // helper functions won't compile properly.
  75 #undef NULL
  76
  77 #ifdef SWIGJAVA
  78
  79 #include "bindings/java_iterator_adapter.h"
  80 #include "bindings/java_stream_adapters.h"
  81
  82 %exception %{
  83   try {
  84     $action
  85   } catch(CVC4::Exception& e) {
  86     std::stringstream ss;
  87     ss << e.what() << ": " << e.getMessage();
  88     std::string explanation = ss.str();
  89     SWIG_JavaThrowException(jenv, SWIG_JavaRuntimeException, explanation.c_str());
  90   }
  91 %}
  92
  93 // Create a mapping from C++ Exceptions to Java Exceptions.
  94 // This is in a couple of throws typemaps, simply because it's sensitive to SWIG's concept of which namespace we're in.
  95 %typemap(throws) Exception %{
  96   std::string name = "edu/nyu/acsys/$1_type";
  97   size_t i = name.find("::");
  98   if(i != std::string::npos) {
  99     size_t j = name.rfind("::");
 100     assert(i <= j);
 101     name.replace(i, j - i + 2, "/");
 102   }
 103   jclass clazz = jenv->FindClass(name.c_str());
 104   assert(clazz != NULL && jenv->ExceptionOccurred() == NULL);
 105   jmethodID method = jenv->GetMethodID(clazz, "<init>", "(JZ)V");
 106   assert(method != NULL && jenv->ExceptionOccurred() == NULL);
 107   jthrowable t = static_cast<jthrowable>(jenv->NewObject(clazz, method, reinterpret_cast<long>(new $1_type($1)), true));
 108   assert(t != NULL && jenv->ExceptionOccurred() == NULL);
 109   int status = jenv->Throw(t);
 110   assert(status == 0);
 111 %}
 112 %typemap(throws) CVC4::Exception %{
 113   std::string name = "edu/nyu/acsys/$1_type";
 114   size_t i = name.find("::");
 115   if(i != std::string::npos) {
 116     size_t j = name.rfind("::");
 117     assert(i <= j);
 118     name.replace(i, j - i + 2, "/");
 119   }
 120   jclass clazz = jenv->FindClass(name.c_str());
 121   assert(clazz != NULL && jenv->ExceptionOccurred() == NULL);
 122   jmethodID method = jenv->GetMethodID(clazz, "<init>", "(JZ)V");
 123   assert(method != NULL && jenv->ExceptionOccurred() == NULL);
 124   jthrowable t = static_cast<jthrowable>(jenv->NewObject(clazz, method, reinterpret_cast<long>(new $1_type($1)), true));
 125   assert(t != NULL && jenv->ExceptionOccurred() == NULL);
 126   int status = jenv->Throw(t);
 127   assert(status == 0);
 128 %}
 129
 130 %typemap(throws) ModalException = Exception;
 131 %typemap(throws) LogicException = Exception;
 132 %typemap(throws) OptionException = Exception;
 133 %typemap(throws) IllegalArgumentException = Exception;
 134 %typemap(throws) AssertionException = Exception;
 135
 136 %typemap(throws) CVC4::TypeCheckingException = CVC4::Exception;
 137 %typemap(throws) CVC4::ScopeException = CVC4::Exception;
 138 %typemap(throws) CVC4::IllegalArgumentException = CVC4::Exception;
 139 %typemap(throws) CVC4::AssertionException = CVC4::Exception;
 140 %typemap(throws) CVC4::parser::InputStreamException = CVC4::Exception;
 141 %typemap(throws) CVC4::parser::ParserException = CVC4::Exception;
 142
 143 // Generate an error if the mapping from C++ CVC4 Exception to Java CVC4 Exception doesn't exist above
 144 %typemap(throws) SWIGTYPE, SWIGTYPE &, SWIGTYPE *, SWIGTYPE [], SWIGTYPE [ANY] %{
 145 #error "exception $1_type doesn't map to Java correctly---please edit src/cvc4.i and add it"
 146 %}
 147
 148 %include "java/typemaps.i" // primitive pointers and references
 149 %include "java/std_string.i" // map std::string to java.lang.String
 150 %include "java/arrays_java.i" // C arrays to Java arrays
 151 %include "java/various.i" // map char** to java.lang.String[]
 152
 153 // Functions on the C++ side taking std::ostream& should on the Java side
 154 // take a java.io.OutputStream.  A JavaOutputStreamAdapter is created in
 155 // the wrapper which creates and passes on a std::stringstream to the C++
 156 // function.  Then on exit, the string from the stringstream is dumped to
 157 // the Java-side OutputStream.
 158 %typemap(jni) std::ostream& "jlong"
 159 %typemap(jtype) std::ostream& "long"
 160 %typemap(jstype) std::ostream& "java.io.OutputStream"
 161 %typemap(javain,
 162          pre="    edu.nyu.acsys.CVC4.JavaOutputStreamAdapter temp$javainput = new edu.nyu.acsys.CVC4.JavaOutputStreamAdapter();", pgcppname="temp$javainput",
 163          post="    new java.io.PrintStream($javainput).print(temp$javainput.toString());")
 164          std::ostream& "edu.nyu.acsys.CVC4.JavaOutputStreamAdapter.getCPtr(temp$javainput)"
 165
 166 %typemap(jni) std::istream& "jlong"
 167 %typemap(jtype) std::istream& "long"
 168 %typemap(jstype) std::istream& "java.io.InputStream"
 169 %typemap(javain,
 170          pre="    edu.nyu.acsys.CVC4.JavaInputStreamAdapter temp$javainput = edu.nyu.acsys.CVC4.JavaInputStreamAdapter.get($javainput);", pgcppname="temp$javainput",
 171          post="")
 172          std::istream& "edu.nyu.acsys.CVC4.JavaInputStreamAdapter.getCPtr(temp$javainput)"
 173 %typemap(in) jobject inputStream %{
 174   $1 = jenv->NewGlobalRef($input);
 175 %}
 176 %typemap(out) CVC4::JavaInputStreamAdapter* %{
 177   $1->pull(jenv);
 178   *(CVC4::JavaInputStreamAdapter **)&$result = $1;
 179 %}
 180 %typemap(javacode) CVC4::JavaInputStreamAdapter %{
 181   private static java.util.HashMap<java.io.InputStream, JavaInputStreamAdapter> streams =
 182     new java.util.HashMap<java.io.InputStream, JavaInputStreamAdapter>();
 183   public static JavaInputStreamAdapter get(java.io.InputStream is) {
 184     if(streams.containsKey(is)) {
 185       return (JavaInputStreamAdapter) streams.get(is);
 186     }
 187     JavaInputStreamAdapter adapter = new JavaInputStreamAdapter(is);
 188     streams.put(is, adapter);
 189     return adapter;
 190   }
 191 %}
 192 %typemap(javafinalize) CVC4::JavaInputStreamAdapter %{
 193   protected void finalize() {
 194     streams.remove(getInputStream());
 195     delete();
 196   }
 197 %}
 198 %ignore CVC4::JavaInputStreamAdapter::init(JNIEnv*);
 199 %ignore CVC4::JavaInputStreamAdapter::pullAdapters(JNIEnv*);
 200 %ignore CVC4::JavaInputStreamAdapter::pull(JNIEnv*);
 201 %javamethodmodifiers CVC4::JavaInputStreamAdapter::getInputStream() const "private";
 202 %javamethodmodifiers CVC4::JavaInputStreamAdapter::JavaInputStreamAdapter(jobject) "private";
 203
 204 %exception CVC4::parser::Parser::nextCommand() %{
 205   try {
 206     CVC4::JavaInputStreamAdapter::pullAdapters(jenv);
 207     $action
 208   } catch(CVC4::Exception& e) {
 209     std::stringstream ss;
 210     ss << e.what() << ": " << e.getMessage();
 211     std::string explanation = ss.str();
 212     SWIG_JavaThrowException(jenv, SWIG_JavaRuntimeException, explanation.c_str());
 213   }
 214 %}
 215 %exception CVC4::parser::Parser::nextExpression() %{
 216   try {
 217     CVC4::JavaInputStreamAdapter::pullAdapters(jenv);
 218     $action
 219   } catch(CVC4::Exception& e) {
 220     std::stringstream ss;
 221     ss << e.what() << ": " << e.getMessage();
 222     std::string explanation = ss.str();
 223     SWIG_JavaThrowException(jenv, SWIG_JavaRuntimeException, explanation.c_str());
 224   }
 225 %}
 226 %exception CVC4::JavaInputStreamAdapter::~JavaInputStreamAdapter() %{
 227   try {
 228     jenv->DeleteGlobalRef(arg1->getInputStream());
 229     $action
 230   } catch(CVC4::Exception& e) {
 231     std::stringstream ss;
 232     ss << e.what() << ": " << e.getMessage();
 233     std::string explanation = ss.str();
 234     SWIG_JavaThrowException(jenv, SWIG_JavaRuntimeException, explanation.c_str());
 235   }
 236 %}
 237
 238 #endif /* SWIGJAVA */
 239
 240 %include "util/integer.i"
 241 %include "util/rational.i"
 242 %include "util/exception.i"
 243 %include "util/language.i"
 244 %include "options/options.i"
 245 %include "util/cardinality.i"
 246 %include "util/bool.i"
 247 %include "util/sexpr.i"
 248 %include "util/statistics.i"
 249 %include "util/output.i"
 250 %include "util/result.i"
 251 %include "util/configuration.i"
 252 %include "util/bitvector.i"
 253 %include "util/subrange_bound.i"
 254 %include "util/array.i"
 255 %include "util/array_store_all.i"
 256 %include "util/predicate.i"
 257 %include "util/hash.i"
 258
 259 %include "expr/type.i"
 260 %include "util/ascription_type.i"
 261 %include "util/datatype.i"
 262 %include "util/tuple.i"
 263 %include "util/record.i"
 264 %include "util/uninterpreted_constant.i"
 265
 266 %include "expr/kind.i"
 267 %include "expr/expr.i"
 268 %include "expr/command.i"
 269 %include "expr/symbol_table.i"
 270 %include "expr/expr_manager.i"
 271 %include "expr/expr_stream.i"
 272 %include "expr/variable_type_map.i"
 273
 274 %include "theory/logic_info.i"
 275
 276 %include "smt/smt_engine.i"
 277 %include "smt/modal_exception.i"
 278 %include "smt/logic_exception.i"
 279
 280 %include "options/options.i"
 281 %include "options/option_exception.i"
 282
 283 %include "parser/cvc4parser.i"