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
  49 #include "util/sexpr.h"
  50 #include "util/exception.h"
  51 #include "expr/type.h"
  52 #include "expr/expr.h"
  53 #include "util/datatype.h"
  54 #include "expr/command.h"
  55 %}
  56
  57 %template(vectorCommandPtr) std::vector< CVC4::Command* >;
  58 %template(vectorType) std::vector< CVC4::Type >;
  59 %template(vectorExpr) std::vector< CVC4::Expr >;
  60 %template(vectorDatatypeType) std::vector< CVC4::DatatypeType >;
  61 %template(vectorSExpr) std::vector< CVC4::SExpr >;
  62 %template(vectorString) std::vector< std::string >;
  63 %template(setType) std::set< CVC4::Type >;
  64 %template(hashmapExpr) std::hash_map< CVC4::Expr, CVC4::Expr, CVC4::ExprHashFunction >;
  65
  66 // This is unfortunate, but seems to be necessary; if we leave NULL
  67 // defined, swig will expand it to "(void*) 0", and some of swig's
  68 // helper functions won't compile properly.
  69 #undef NULL
  70
  71 #ifdef SWIGJAVA
  72
  73 %exception {
  74   try {
  75     $action
  76   } catch(CVC4::Exception& e) {
  77     ::std::cerr << e << ::std::endl;
  78     jclass clazz = jenv->FindClass("java/lang/RuntimeException");
  79     jenv->ThrowNew(clazz, e.toString().c_str());
  80   }
  81 }
  82
  83 %include "java/typemaps.i" // primitive pointers and references
  84 %include "java/std_string.i" // map std::string to java.lang.String
  85 %include "java/arrays_java.i" // C arrays to Java arrays
  86 %include "java/various.i" // map char** to java.lang.String[]
  87
  88 #endif /* SWIGJAVA */
  89
  90 %include "util/integer.i"
  91 %include "util/rational.i"
  92 %include "util/stats.i"
  93 %include "util/exception.i"
  94 %include "util/language.i"
  95 %include "util/options.i"
  96 %include "util/cardinality.i"
  97 %include "util/bool.i"
  98 %include "util/sexpr.i"
  99 %include "util/output.i"
 100 %include "util/result.i"
 101 %include "util/configuration.i"
 102 %include "util/Assert.i"
 103 %include "util/bitvector.i"
 104 %include "util/subrange_bound.i"
 105 %include "util/array.i"
 106 %include "util/hash.i"
 107
 108 %include "expr/type.i"
 109 %include "util/ascription_type.i"
 110 %include "util/datatype.i"
 111
 112 %include "expr/kind.i"
 113 %include "expr/expr.i"
 114 %include "expr/command.i"
 115 %include "expr/declaration_scope.i"
 116 %include "expr/expr_manager.i"
 117 %include "expr/expr_stream.i"
 118
 119 %include "smt/smt_engine.i"
 120 %include "smt/bad_option_exception.i"
 121 %include "smt/no_such_function_exception.i"
 122 %include "smt/modal_exception.i"
 123
 124 %include "parser/cvc4parser.i"