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 unordered_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 */
44 #include <unordered_map>
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"
64 #include "bindings/java_stream_adapters.h"
65 std::set<JavaInputStreamAdapter*> CVC4::JavaInputStreamAdapter::s_adapters;
70 %pythonappend CVC4::SmtEngine::SmtEngine %{
73 %pythonappend CVC4::ExprManager::ExprManager %{
76 #endif /* SWIGPYTHON */
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 >;
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.
98 #include "bindings/java_iterator_adapter.h"
99 #include "bindings/java_stream_adapters.h"
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());
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";
117 size_t i = name.find("::");
118 if(i != std::string::npos) {
119 size_t j = name.rfind("::");
121 name.replace(i, j - i + 2, "/");
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);
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("::");
139 name.replace(i, j - i + 2, "/");
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);
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;
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;
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;
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"
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[]
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"
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)"
192 %typemap(jni) std::istream& "jlong"
193 %typemap(jtype) std::istream& "long"
194 %typemap(jstype) std::istream& "java.io.InputStream"
196 pre=" edu.nyu.acsys.CVC4.JavaInputStreamAdapter temp$javainput = edu.nyu.acsys.CVC4.JavaInputStreamAdapter.get($javainput);", pgcppname="temp$javainput",
198 std::istream& "edu.nyu.acsys.CVC4.JavaInputStreamAdapter.getCPtr(temp$javainput)"
199 %typemap(in) jobject inputStream %{
200 $1 = jenv->NewGlobalRef($input);
202 %typemap(out) CVC4::JavaInputStreamAdapter* %{
204 *(CVC4::JavaInputStreamAdapter **)&$result = $1;
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);
213 JavaInputStreamAdapter adapter = new JavaInputStreamAdapter(is);
214 streams.put(is, adapter);
218 %typemap(javafinalize) CVC4::JavaInputStreamAdapter %{
219 protected void finalize() {
220 streams.remove(getInputStream());
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";
230 %exception CVC4::parser::Parser::nextCommand() %{
232 CVC4::JavaInputStreamAdapter::pullAdapters(jenv);
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());
241 %exception CVC4::parser::Parser::nextExpression() %{
243 CVC4::JavaInputStreamAdapter::pullAdapters(jenv);
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());
252 %exception CVC4::JavaInputStreamAdapter::~JavaInputStreamAdapter() %{
254 jenv->DeleteGlobalRef(arg1->getInputStream());
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());
264 /* Copied (and modified) from java.swg; the standard swig version causes
265 * negative BigInteger to be interpreted unsigned. Here we throw an
267 %typemap(in) unsigned long long {
276 SWIG_JavaThrowException(jenv, SWIG_JavaNullPointerException, "BigInteger null");
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.");
288 if(sz > 1 && bae[0] == 0) {
291 if(test_sz > sizeof(unsigned long long)) {
292 SWIG_JavaThrowException(jenv, SWIG_JavaRuntimeException, "BigInteger argument out of bounds.");
295 for(i=0; i<sz; i++) {
296 $1 = ($1 << 8) | ($1_type)(unsigned char)bae[i];
298 JCALL3(ReleaseByteArrayElements, jenv, ba, bae, 0);
301 #endif /* SWIGJAVA */
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"
310 %include "options/language.i"
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"
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"
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"
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"
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"
359 // Tim: This should come after "theory/logic_info.i".
360 %include "smt/smt_engine.i"