Java datatype API fixups, datatype API examples
[cvc5.git] / 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
58 #ifdef SWIGJAVA
59 #include "bindings/java_stream_adapters.h"
60 std::set<JavaInputStreamAdapter*> CVC4::JavaInputStreamAdapter::s_adapters;
61 #endif
62 %}
63
64 %template(vectorCommandPtr) std::vector< CVC4::Command* >;
65 %template(vectorType) std::vector< CVC4::Type >;
66 %template(vectorExpr) std::vector< CVC4::Expr >;
67 %template(vectorUnsignedInt) std::vector< unsigned int >;
68 %template(vectorVectorExpr) std::vector< std::vector< CVC4::Expr > >;
69 %template(vectorDatatypeType) std::vector< CVC4::DatatypeType >;
70 %template(vectorSExpr) std::vector< CVC4::SExpr >;
71 %template(vectorString) std::vector< std::string >;
72 %template(vectorPairStringType) std::vector< std::pair< std::string, CVC4::Type > >;
73 %template(pairStringType) std::pair< std::string, CVC4::Type >;
74 %template(setType) std::set< CVC4::Type >;
75 %template(hashmapExpr) std::hash_map< CVC4::Expr, CVC4::Expr, CVC4::ExprHashFunction >;
76
77 // This is unfortunate, but seems to be necessary; if we leave NULL
78 // defined, swig will expand it to "(void*) 0", and some of swig's
79 // helper functions won't compile properly.
80 #undef NULL
81
82 #ifdef SWIGJAVA
83
84 #include "bindings/java_iterator_adapter.h"
85 #include "bindings/java_stream_adapters.h"
86
87 %exception %{
88 try {
89 $action
90 } catch(CVC4::Exception& e) {
91 std::stringstream ss;
92 ss << e.what() << ": " << e.getMessage();
93 std::string explanation = ss.str();
94 SWIG_JavaThrowException(jenv, SWIG_JavaRuntimeException, explanation.c_str());
95 }
96 %}
97
98 // Create a mapping from C++ Exceptions to Java Exceptions.
99 // This is in a couple of throws typemaps, simply because it's sensitive to SWIG's concept of which namespace we're in.
100 %typemap(throws) Exception %{
101 std::string name = "edu/nyu/acsys/CVC4/$1_type";
102 /*
103 size_t i = name.find("::");
104 if(i != std::string::npos) {
105 size_t j = name.rfind("::");
106 assert(i <= j);
107 name.replace(i, j - i + 2, "/");
108 }
109 */
110 jclass clazz = jenv->FindClass(name.c_str());
111 assert(clazz != NULL && jenv->ExceptionOccurred() == NULL);
112 jmethodID method = jenv->GetMethodID(clazz, "<init>", "(JZ)V");
113 assert(method != NULL && jenv->ExceptionOccurred() == NULL);
114 jthrowable t = static_cast<jthrowable>(jenv->NewObject(clazz, method, reinterpret_cast<long>(new $1_type($1)), true));
115 assert(t != NULL && jenv->ExceptionOccurred() == NULL);
116 int status = jenv->Throw(t);
117 assert(status == 0);
118 %}
119 %typemap(throws) CVC4::Exception %{
120 std::string name = "edu/nyu/acsys/$1_type";
121 size_t i = name.find("::");
122 if(i != std::string::npos) {
123 size_t j = name.rfind("::");
124 assert(i <= j);
125 name.replace(i, j - i + 2, "/");
126 }
127 jclass clazz = jenv->FindClass(name.c_str());
128 assert(clazz != NULL && jenv->ExceptionOccurred() == NULL);
129 jmethodID method = jenv->GetMethodID(clazz, "<init>", "(JZ)V");
130 assert(method != NULL && jenv->ExceptionOccurred() == NULL);
131 jthrowable t = static_cast<jthrowable>(jenv->NewObject(clazz, method, reinterpret_cast<long>(new $1_type($1)), true));
132 assert(t != NULL && jenv->ExceptionOccurred() == NULL);
133 int status = jenv->Throw(t);
134 assert(status == 0);
135 %}
136
137 %typemap(throws) ModalException = Exception;
138 %typemap(throws) LogicException = Exception;
139 %typemap(throws) OptionException = Exception;
140 %typemap(throws) IllegalArgumentException = Exception;
141 %typemap(throws) AssertionException = Exception;
142
143 %typemap(throws) CVC4::TypeCheckingException = CVC4::Exception;
144 %typemap(throws) CVC4::ScopeException = CVC4::Exception;
145 %typemap(throws) CVC4::IllegalArgumentException = CVC4::Exception;
146 %typemap(throws) CVC4::AssertionException = CVC4::Exception;
147 %typemap(throws) CVC4::parser::InputStreamException = CVC4::Exception;
148 %typemap(throws) CVC4::parser::ParserException = CVC4::Exception;
149
150 // Generate an error if the mapping from C++ CVC4 Exception to Java CVC4 Exception doesn't exist above
151 %typemap(throws) SWIGTYPE, SWIGTYPE &, SWIGTYPE *, SWIGTYPE [], SWIGTYPE [ANY] %{
152 #error "exception $1_type doesn't map to Java correctly---please edit src/cvc4.i and add it"
153 %}
154
155 %include "java/typemaps.i" // primitive pointers and references
156 %include "java/std_string.i" // map std::string to java.lang.String
157 %include "java/arrays_java.i" // C arrays to Java arrays
158 %include "java/various.i" // map char** to java.lang.String[]
159
160 // Functions on the C++ side taking std::ostream& should on the Java side
161 // take a java.io.OutputStream. A JavaOutputStreamAdapter is created in
162 // the wrapper which creates and passes on a std::stringstream to the C++
163 // function. Then on exit, the string from the stringstream is dumped to
164 // the Java-side OutputStream.
165 %typemap(jni) std::ostream& "jlong"
166 %typemap(jtype) std::ostream& "long"
167 %typemap(jstype) std::ostream& "java.io.OutputStream"
168 %typemap(javain,
169 pre=" edu.nyu.acsys.CVC4.JavaOutputStreamAdapter temp$javainput = new edu.nyu.acsys.CVC4.JavaOutputStreamAdapter();", pgcppname="temp$javainput",
170 post=" new java.io.PrintStream($javainput).print(temp$javainput.toString());")
171 std::ostream& "edu.nyu.acsys.CVC4.JavaOutputStreamAdapter.getCPtr(temp$javainput)"
172
173 %typemap(jni) std::istream& "jlong"
174 %typemap(jtype) std::istream& "long"
175 %typemap(jstype) std::istream& "java.io.InputStream"
176 %typemap(javain,
177 pre=" edu.nyu.acsys.CVC4.JavaInputStreamAdapter temp$javainput = edu.nyu.acsys.CVC4.JavaInputStreamAdapter.get($javainput);", pgcppname="temp$javainput",
178 post="")
179 std::istream& "edu.nyu.acsys.CVC4.JavaInputStreamAdapter.getCPtr(temp$javainput)"
180 %typemap(in) jobject inputStream %{
181 $1 = jenv->NewGlobalRef($input);
182 %}
183 %typemap(out) CVC4::JavaInputStreamAdapter* %{
184 $1->pull(jenv);
185 *(CVC4::JavaInputStreamAdapter **)&$result = $1;
186 %}
187 %typemap(javacode) CVC4::JavaInputStreamAdapter %{
188 private static java.util.HashMap<java.io.InputStream, JavaInputStreamAdapter> streams =
189 new java.util.HashMap<java.io.InputStream, JavaInputStreamAdapter>();
190 public static JavaInputStreamAdapter get(java.io.InputStream is) {
191 if(streams.containsKey(is)) {
192 return (JavaInputStreamAdapter) streams.get(is);
193 }
194 JavaInputStreamAdapter adapter = new JavaInputStreamAdapter(is);
195 streams.put(is, adapter);
196 return adapter;
197 }
198 %}
199 %typemap(javafinalize) CVC4::JavaInputStreamAdapter %{
200 protected void finalize() {
201 streams.remove(getInputStream());
202 delete();
203 }
204 %}
205 %ignore CVC4::JavaInputStreamAdapter::init(JNIEnv*);
206 %ignore CVC4::JavaInputStreamAdapter::pullAdapters(JNIEnv*);
207 %ignore CVC4::JavaInputStreamAdapter::pull(JNIEnv*);
208 %javamethodmodifiers CVC4::JavaInputStreamAdapter::getInputStream() const "private";
209 %javamethodmodifiers CVC4::JavaInputStreamAdapter::JavaInputStreamAdapter(jobject) "private";
210
211 %exception CVC4::parser::Parser::nextCommand() %{
212 try {
213 CVC4::JavaInputStreamAdapter::pullAdapters(jenv);
214 $action
215 } catch(CVC4::Exception& e) {
216 std::stringstream ss;
217 ss << e.what() << ": " << e.getMessage();
218 std::string explanation = ss.str();
219 SWIG_JavaThrowException(jenv, SWIG_JavaRuntimeException, explanation.c_str());
220 }
221 %}
222 %exception CVC4::parser::Parser::nextExpression() %{
223 try {
224 CVC4::JavaInputStreamAdapter::pullAdapters(jenv);
225 $action
226 } catch(CVC4::Exception& e) {
227 std::stringstream ss;
228 ss << e.what() << ": " << e.getMessage();
229 std::string explanation = ss.str();
230 SWIG_JavaThrowException(jenv, SWIG_JavaRuntimeException, explanation.c_str());
231 }
232 %}
233 %exception CVC4::JavaInputStreamAdapter::~JavaInputStreamAdapter() %{
234 try {
235 jenv->DeleteGlobalRef(arg1->getInputStream());
236 $action
237 } catch(CVC4::Exception& e) {
238 std::stringstream ss;
239 ss << e.what() << ": " << e.getMessage();
240 std::string explanation = ss.str();
241 SWIG_JavaThrowException(jenv, SWIG_JavaRuntimeException, explanation.c_str());
242 }
243 %}
244
245 #endif /* SWIGJAVA */
246
247 %include "util/integer.i"
248 %include "util/rational.i"
249 %include "util/exception.i"
250 %include "util/language.i"
251 %include "util/cardinality.i"
252 %include "util/bool.i"
253 %include "util/sexpr.i"
254 %include "options/options.i"
255 %include "util/statistics.i"
256 %include "util/result.i"
257 %include "util/configuration.i"
258 %include "util/bitvector.i"
259 %include "util/subrange_bound.i"
260 %include "util/array.i"
261 %include "util/array_store_all.i"
262 %include "util/predicate.i"
263 %include "util/hash.i"
264
265 %include "expr/type.i"
266 %include "util/ascription_type.i"
267 %include "util/datatype.i"
268 %include "util/tuple.i"
269 %include "util/record.i"
270 %include "util/regexp.i"
271 %include "util/uninterpreted_constant.i"
272 %include "util/proof.i"
273
274 %include "expr/kind.i"
275 %include "expr/expr.i"
276 %include "expr/command.i"
277 %include "expr/symbol_table.i"
278 %include "expr/expr_manager.i"
279 %include "expr/expr_stream.i"
280 %include "expr/variable_type_map.i"
281
282 %include "theory/logic_info.i"
283
284 %include "smt/smt_engine.i"
285 %include "smt/modal_exception.i"
286 %include "smt/logic_exception.i"
287
288 %include "options/options.i"
289 %include "options/option_exception.i"
290
291 %include "parser/cvc4parser.i"