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 unordered_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 <cassert>
  44 #include <unordered_map>
  45 #include <iosfwd>
  46 #include <set>
  47 #include <string>
  48 #include <typeinfo>
  49 #include <vector>
  50
  51 #include "base/exception.h"
  52 #include "base/modal_exception.h"
  53 #include "expr/datatype.h"
  54 #include "expr/expr.h"
  55 #include "expr/type.h"
  56 #include "options/option_exception.h"
  57 #include "smt/command.h"
  58 #include "util/bitvector.h"
  59 #include "util/integer.h"
  60 #include "util/sexpr.h"
  61 #include "util/unsafe_interrupt_exception.h"
  62
  63 #ifdef SWIGJAVA
  64 #include "bindings/java_stream_adapters.h"
  65 std::set<JavaInputStreamAdapter*> CVC4::JavaInputStreamAdapter::s_adapters;
  66 #endif
  67 %}
  68
  69 #ifdef SWIGPYTHON
  70 %pythonappend CVC4::SmtEngine::SmtEngine %{
  71   self.thisown = 0
  72 %}
  73 %pythonappend CVC4::ExprManager::ExprManager %{
  74   self.thisown = 0
  75 %}
  76 #endif /* SWIGPYTHON */
  77
  78 %template(vectorCommandPtr) std::vector< CVC4::Command* >;
  79 %template(vectorType) std::vector< CVC4::Type >;
  80 %template(vectorExpr) std::vector< CVC4::Expr >;
  81 %template(vectorUnsignedInt) std::vector< unsigned int >;
  82 %template(vectorVectorExpr) std::vector< std::vector< CVC4::Expr > >;
  83 %template(vectorDatatypeType) std::vector< CVC4::DatatypeType >;
  84 %template(vectorSExpr) std::vector< CVC4::SExpr >;
  85 %template(vectorString) std::vector< std::string >;
  86 %template(vectorPairStringType) std::vector< std::pair< std::string, CVC4::Type > >;
  87 %template(pairStringType) std::pair< std::string, CVC4::Type >;
  88 %template(setOfType) std::set< CVC4::Type >;
  89 %template(hashmapExpr) std::unordered_map< CVC4::Expr, CVC4::Expr, CVC4::ExprHashFunction >;
  90
  91 // This is unfortunate, but seems to be necessary; if we leave NULL
  92 // defined, swig will expand it to "(void*) 0", and some of swig's
  93 // helper functions won't compile properly.
  94 #undef NULL
  95
  96 #ifdef SWIGJAVA
  97
  98 #include "bindings/java_iterator_adapter.h"
  99 #include "bindings/java_stream_adapters.h"
 100
 101 %exception %{
 102   try {
 103     $action
 104   } catch(CVC4::Exception& e) {
 105     std::stringstream ss;
 106     ss << e.what() << ": " << e.getMessage();
 107     std::string explanation = ss.str();
 108     SWIG_JavaThrowException(jenv, SWIG_JavaRuntimeException, explanation.c_str());
 109   }
 110 %}
 111
 112 // Create a mapping from C++ Exceptions to Java Exceptions.
 113 // This is in a couple of throws typemaps, simply because it's sensitive to SWIG's concept of which namespace we're in.
 114 %typemap(throws) Exception %{
 115   std::string name = "edu/nyu/acsys/CVC4/$1_type";
 116   /*
 117   size_t i = name.find("::");
 118   if(i != std::string::npos) {
 119     size_t j = name.rfind("::");
 120     assert(i <= j);
 121     name.replace(i, j - i + 2, "/");
 122   }
 123   */
 124   jclass clazz = jenv->FindClass(name.c_str());
 125   assert(clazz != NULL && jenv->ExceptionOccurred() == NULL);
 126   jmethodID method = jenv->GetMethodID(clazz, "<init>", "(JZ)V");
 127   assert(method != NULL && jenv->ExceptionOccurred() == NULL);
 128   jthrowable t = static_cast<jthrowable>(jenv->NewObject(clazz, method, reinterpret_cast<uintptr_t>(new $1_type($1)), true));
 129   assert(t != NULL && jenv->ExceptionOccurred() == NULL);
 130   int status = jenv->Throw(t);
 131   assert(status == 0);
 132 %}
 133 %typemap(throws) CVC4::Exception %{
 134   std::string name = "edu/nyu/acsys/$1_type";
 135   size_t i = name.find("::");
 136   if(i != std::string::npos) {
 137     size_t j = name.rfind("::");
 138     assert(i <= j);
 139     name.replace(i, j - i + 2, "/");
 140   }
 141   jclass clazz = jenv->FindClass(name.c_str());
 142   assert(clazz != NULL && jenv->ExceptionOccurred() == NULL);
 143   jmethodID method = jenv->GetMethodID(clazz, "<init>", "(JZ)V");
 144   assert(method != NULL && jenv->ExceptionOccurred() == NULL);
 145   jthrowable t = static_cast<jthrowable>(jenv->NewObject(clazz, method, reinterpret_cast<uintptr_t>(new $1_type($1)), true));
 146   assert(t != NULL && jenv->ExceptionOccurred() == NULL);
 147   int status = jenv->Throw(t);
 148   assert(status == 0);
 149 %}
 150
 151 %typemap(throws) CVC4::ModalException = CVC4::Exception;
 152 %typemap(throws) CVC4::LogicException = CVC4::Exception;
 153 %typemap(throws) CVC4::OptionException = CVC4::Exception;
 154 %typemap(throws) CVC4::IllegalArgumentException = CVC4::Exception;
 155 %typemap(throws) CVC4::AssertionException = CVC4::Exception;
 156
 157 %typemap(throws) CVC4::TypeCheckingException = CVC4::Exception;
 158 %typemap(throws) CVC4::ScopeException = CVC4::Exception;
 159 %typemap(throws) CVC4::IllegalArgumentException = CVC4::Exception;
 160 %typemap(throws) IllegalArgumentException = Exception;
 161 %typemap(throws) CVC4::AssertionException = CVC4::Exception;
 162
 163 // TIM: Really unclear why both of these are required
 164 %typemap(throws) CVC4::UnsafeInterruptException = CVC4::Exception;
 165 %typemap(throws) UnsafeInterruptException = CVC4::Exception;
 166 %typemap(throws) CVC4::parser::InputStreamException = CVC4::Exception;
 167 %typemap(throws) CVC4::parser::ParserException = CVC4::Exception;
 168
 169 // Generate an error if the mapping from C++ CVC4 Exception to Java CVC4 Exception doesn't exist above
 170 %typemap(throws) SWIGTYPE, SWIGTYPE &, SWIGTYPE *, SWIGTYPE [], SWIGTYPE [ANY] %{
 171 #error "exception $1_type doesn't map to Java correctly---please edit src/cvc4.i and add it"
 172 %}
 173
 174 %include "java/typemaps.i" // primitive pointers and references
 175 %include "java/std_string.i" // map std::string to java.lang.String
 176 %include "java/arrays_java.i" // C arrays to Java arrays
 177 %include "java/various.i" // map char** to java.lang.String[]
 178
 179 // Functions on the C++ side taking std::ostream& should on the Java side
 180 // take a java.io.OutputStream.  A JavaOutputStreamAdapter is created in
 181 // the wrapper which creates and passes on a std::stringstream to the C++
 182 // function.  Then on exit, the string from the stringstream is dumped to
 183 // the Java-side OutputStream.
 184 %typemap(jni) std::ostream& "jlong"
 185 %typemap(jtype) std::ostream& "long"
 186 %typemap(jstype) std::ostream& "java.io.OutputStream"
 187 %typemap(javain,
 188          pre="    edu.nyu.acsys.CVC4.JavaOutputStreamAdapter temp$javainput = new edu.nyu.acsys.CVC4.JavaOutputStreamAdapter();", pgcppname="temp$javainput",
 189          post="    new java.io.PrintStream($javainput).print(temp$javainput.toString());")
 190          std::ostream& "edu.nyu.acsys.CVC4.JavaOutputStreamAdapter.getCPtr(temp$javainput)"
 191
 192 %typemap(jni) std::istream& "jlong"
 193 %typemap(jtype) std::istream& "long"
 194 %typemap(jstype) std::istream& "java.io.InputStream"
 195 %typemap(javain,
 196          pre="    edu.nyu.acsys.CVC4.JavaInputStreamAdapter temp$javainput = edu.nyu.acsys.CVC4.JavaInputStreamAdapter.get($javainput);", pgcppname="temp$javainput",
 197          post="")
 198          std::istream& "edu.nyu.acsys.CVC4.JavaInputStreamAdapter.getCPtr(temp$javainput)"
 199 %typemap(in) jobject inputStream %{
 200   $1 = jenv->NewGlobalRef($input);
 201 %}
 202 %typemap(out) CVC4::JavaInputStreamAdapter* %{
 203   $1->pull(jenv);
 204   *(CVC4::JavaInputStreamAdapter **)&$result = $1;
 205 %}
 206 %typemap(javacode) CVC4::JavaInputStreamAdapter %{
 207   private static java.util.HashMap<java.io.InputStream, JavaInputStreamAdapter> streams =
 208     new java.util.HashMap<java.io.InputStream, JavaInputStreamAdapter>();
 209   public static JavaInputStreamAdapter get(java.io.InputStream is) {
 210     if(streams.containsKey(is)) {
 211       return (JavaInputStreamAdapter) streams.get(is);
 212     }
 213     JavaInputStreamAdapter adapter = new JavaInputStreamAdapter(is);
 214     streams.put(is, adapter);
 215     return adapter;
 216   }
 217 %}
 218 %typemap(javafinalize) CVC4::JavaInputStreamAdapter %{
 219   protected void finalize() {
 220     streams.remove(getInputStream());
 221     delete();
 222   }
 223 %}
 224 %ignore CVC4::JavaInputStreamAdapter::init(JNIEnv*);
 225 %ignore CVC4::JavaInputStreamAdapter::pullAdapters(JNIEnv*);
 226 %ignore CVC4::JavaInputStreamAdapter::pull(JNIEnv*);
 227 %javamethodmodifiers CVC4::JavaInputStreamAdapter::getInputStream() const "private";
 228 %javamethodmodifiers CVC4::JavaInputStreamAdapter::JavaInputStreamAdapter(jobject) "private";
 229
 230 %exception CVC4::parser::Parser::nextCommand() %{
 231   try {
 232     CVC4::JavaInputStreamAdapter::pullAdapters(jenv);
 233     $action
 234   } catch(CVC4::Exception& e) {
 235     std::stringstream ss;
 236     ss << e.what() << ": " << e.getMessage();
 237     std::string explanation = ss.str();
 238     SWIG_JavaThrowException(jenv, SWIG_JavaRuntimeException, explanation.c_str());
 239   }
 240 %}
 241 %exception CVC4::parser::Parser::nextExpression() %{
 242   try {
 243     CVC4::JavaInputStreamAdapter::pullAdapters(jenv);
 244     $action
 245   } catch(CVC4::Exception& e) {
 246     std::stringstream ss;
 247     ss << e.what() << ": " << e.getMessage();
 248     std::string explanation = ss.str();
 249     SWIG_JavaThrowException(jenv, SWIG_JavaRuntimeException, explanation.c_str());
 250   }
 251 %}
 252 %exception CVC4::JavaInputStreamAdapter::~JavaInputStreamAdapter() %{
 253   try {
 254     jenv->DeleteGlobalRef(arg1->getInputStream());
 255     $action
 256   } catch(CVC4::Exception& e) {
 257     std::stringstream ss;
 258     ss << e.what() << ": " << e.getMessage();
 259     std::string explanation = ss.str();
 260     SWIG_JavaThrowException(jenv, SWIG_JavaRuntimeException, explanation.c_str());
 261   }
 262 %}
 263
 264 /* Copied (and modified) from java.swg; the standard swig version causes
 265  * negative BigInteger to be interpreted unsigned.  Here we throw an
 266  * exception. */
 267 %typemap(in) unsigned long long {
 268   jclass clazz;
 269   jmethodID mid;
 270   jbyteArray ba;
 271   jbyte* bae;
 272   jsize sz;
 273   int i;
 274
 275   if (!$input) {
 276     SWIG_JavaThrowException(jenv, SWIG_JavaNullPointerException, "BigInteger null");
 277     return $null;
 278   }
 279   clazz = JCALL1(GetObjectClass, jenv, $input);
 280   mid = JCALL3(GetMethodID, jenv, clazz, "toByteArray", "()[B");
 281   ba = (jbyteArray)JCALL2(CallObjectMethod, jenv, $input, mid);
 282   bae = JCALL2(GetByteArrayElements, jenv, ba, 0);
 283   sz = JCALL1(GetArrayLength, jenv, ba);
 284   if((bae[0] & 0x80) != 0) {
 285     SWIG_JavaThrowException(jenv, SWIG_JavaRuntimeException, "BigInteger argument must be nonnegative.");
 286   }
 287   jsize test_sz = sz;
 288   if(sz > 1 && bae[0] == 0) {
 289     --test_sz;
 290   }
 291   if(test_sz > sizeof(unsigned long long)) {
 292     SWIG_JavaThrowException(jenv, SWIG_JavaRuntimeException, "BigInteger argument out of bounds.");
 293   }
 294   $1 = 0;
 295   for(i=0; i<sz; i++) {
 296     $1 = ($1 << 8) | ($1_type)(unsigned char)bae[i];
 297   }
 298   JCALL3(ReleaseByteArrayElements, jenv, ba, bae, 0);
 299 }
 300
 301 #endif /* SWIGJAVA */
 302
 303 // TIM:
 304 // At the moment, the header includes seem to need to follow a special order.
 305 // I don't know why. I am following the build order
 306 %include "base/configuration.i"
 307 %include "base/exception.i"
 308 %include "base/modal_exception.i"
 309
 310 %include "options/language.i"
 311
 312 // Tim: "util/integer.i" must come before util/{rational.i,bitvector.i}.
 313 %include "util/integer.i"
 314 %include "util/rational.i"
 315 %include "util/bitvector.i"
 316
 317 // Tim: The remainder of util/.
 318 %include "util/bool.i"
 319 %include "util/cardinality.i"
 320 %include "util/hash.i"
 321 %include "util/proof.i"
 322 %include "util/regexp.i"
 323 %include "util/resource_manager.i"
 324 %include "util/result.i"
 325 %include "util/sexpr.i"
 326 %include "util/statistics.i"
 327 %include "util/tuple.i"
 328 %include "util/unsafe_interrupt_exception.i"
 329
 330 %include "expr/uninterpreted_constant.i"
 331 %include "expr/array_store_all.i"
 332 %include "expr/ascription_type.i"
 333 %include "expr/emptyset.i"
 334 %include "expr/datatype.i"
 335 %include "expr/record.i"
 336 %include "proof/unsat_core.i"
 337
 338 // TIM:
 339 // Have these before the rest of expr/.
 340 // Again, no clue why.
 341 %include "expr/array.i"
 342 %include "expr/kind.i"
 343 %include "expr/type.i"
 344
 345 // TIM:
 346 // The remainder of the includes:
 347 %include "expr/expr.i"
 348 %include "expr/expr_manager.i"
 349 %include "expr/expr_stream.i"
 350 %include "expr/symbol_table.i"
 351 %include "expr/variable_type_map.i"
 352 %include "options/option_exception.i"
 353 %include "options/options.i"
 354 %include "parser/cvc4parser.i"
 355 %include "smt/command.i"
 356 %include "smt/logic_exception.i"
 357 %include "theory/logic_info.i"
 358
 359 // Tim: This should come after "theory/logic_info.i".
 360 %include "smt/smt_engine.i"