1 %import "bindings/swig.h"
7 // nspace completely broken with Java packaging
13 template <class T> class set {};
14 template <class K, class V, class H> class hash_map {};
18 // Perl's headers define "seed" to Perl_seed, which breaks
19 // gmpxx.h; undo the damage for our CVC4 module.
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
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!
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>.
37 # undef invalid_argument
38 #endif /* SWIGOCAML */
47 #include <ext/hash_map>
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"
59 %template(vectorCommandPtr) std::vector< CVC4::Command* >;
60 %template(vectorType) std::vector< CVC4::Type >;
61 %template(vectorExpr) std::vector< CVC4::Expr >;
62 %template(vectorDatatypeType) std::vector< CVC4::DatatypeType >;
63 %template(vectorSExpr) std::vector< CVC4::SExpr >;
64 %template(vectorString) std::vector< std::string >;
65 %template(setType) std::set< CVC4::Type >;
66 %template(hashmapExpr) std::hash_map< CVC4::Expr, CVC4::Expr, CVC4::ExprHashFunction >;
68 // This is unfortunate, but seems to be necessary; if we leave NULL
69 // defined, swig will expand it to "(void*) 0", and some of swig's
70 // helper functions won't compile properly.
78 } catch(CVC4::Exception& e) {
80 ss << e.what() << ": " << e.getMessage();
81 std::string explanation = ss.str();
82 SWIG_JavaThrowException(jenv, SWIG_JavaRuntimeException, explanation.c_str());
86 // Create a mapping from C++ Exceptions to Java Exceptions.
87 // This is in a couple of throws typemaps, simply because it's sensitive to SWIG's concept of which namespace we're in.
88 %typemap(throws) Exception %{
89 jclass clazz = jenv->FindClass("edu/nyu/acsys/CVC4/$1_type");
90 assert(clazz != NULL && jenv->ExceptionOccurred() == NULL);
91 jmethodID method = jenv->GetMethodID(clazz, "<init>", "(JZ)V");
92 assert(method != NULL && jenv->ExceptionOccurred() == NULL);
93 jthrowable t = static_cast<jthrowable>(jenv->NewObject(clazz, method, reinterpret_cast<long>(new $1_type($1)), true));
94 assert(t != NULL && jenv->ExceptionOccurred() == NULL);
95 int status = jenv->Throw(t);
98 %typemap(throws) CVC4::Exception %{
99 std::string name = "edu/nyu/acsys/$1_type";
100 for(size_t i = name.find("::"); i != std::string::npos; i = name.find("::")) {
101 name.replace(i, 2, "/");
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);
113 %typemap(throws) ModalException = Exception;
114 %typemap(throws) OptionException = Exception;
115 %typemap(throws) IllegalArgumentException = Exception;
116 %typemap(throws) AssertionException = Exception;
118 %typemap(throws) CVC4::TypeCheckingException = CVC4::Exception;
119 %typemap(throws) CVC4::ScopeException = CVC4::Exception;
120 %typemap(throws) CVC4::IllegalArgumentException = CVC4::Exception;
121 %typemap(throws) CVC4::AssertionException = CVC4::Exception;
122 %typemap(throws) CVC4::parser::InputStreamException = CVC4::Exception;
123 %typemap(throws) CVC4::parser::ParserException = CVC4::Exception;
125 // Generate an error if the mapping from C++ CVC4 Exception to Java CVC4 Exception doesn't exist above
126 %typemap(throws) SWIGTYPE, SWIGTYPE &, SWIGTYPE *, SWIGTYPE [], SWIGTYPE [ANY] %{
127 #error "exception $1_type doesn't map to Java correctly"
130 %include "java/typemaps.i" // primitive pointers and references
131 %include "java/std_string.i" // map std::string to java.lang.String
132 %include "java/arrays_java.i" // C arrays to Java arrays
133 %include "java/various.i" // map char** to java.lang.String[]
135 #endif /* SWIGJAVA */
137 %include "util/integer.i"
138 %include "util/rational.i"
139 %include "util/statistics.i"
140 %include "util/exception.i"
141 %include "util/language.i"
142 %include "options/options.i"
143 %include "util/cardinality.i"
144 %include "util/bool.i"
145 %include "util/sexpr.i"
146 %include "util/output.i"
147 %include "util/result.i"
148 %include "util/configuration.i"
149 %include "util/Assert.i"
150 %include "util/bitvector.i"
151 %include "util/subrange_bound.i"
152 %include "util/array.i"
153 %include "util/array_store_all.i"
154 %include "util/hash.i"
156 %include "expr/type.i"
157 %include "util/ascription_type.i"
158 %include "util/datatype.i"
160 %include "expr/kind.i"
161 %include "expr/expr.i"
162 %include "expr/command.i"
163 %include "expr/symbol_table.i"
164 %include "expr/expr_manager.i"
165 %include "expr/expr_stream.i"
167 %include "smt/smt_engine.i"
168 %include "smt/modal_exception.i"
170 %include "options/options.i"
171 %include "options/option_exception.i"
173 %include "parser/cvc4parser.i"