fix exceptions and mkConst() in java binding

diff --git a/src/expr/expr_manager.i b/src/expr/expr_manager.i
index 960ba8f84e76ebb95a6786eda01825df748528fa..178f00ccd53dd7b29e452827f9b5b1d22c6b9a1e 100644 (file)
--- a/src/expr/expr_manager.i
+++ b/src/expr/expr_manager.i
@@ -19,4 +19,26 @@
 
 %template(mkConst) CVC4::ExprManager::mkConst< CVC4::Rational >;
 
+
+%template(mkConst) CVC4::ExprManager::mkConst<CVC4::TypeConstant>;
+%template(mkConst) CVC4::ExprManager::mkConst<CVC4::ArrayStoreAll>;
+%template(mkConst) CVC4::ExprManager::mkConst<CVC4::BitVectorSize>;
+%template(mkConst) CVC4::ExprManager::mkConst<CVC4::AscriptionType>;
+%template(mkConst) CVC4::ExprManager::mkConst<CVC4::BitVectorBitOf>;
+%template(mkConst) CVC4::ExprManager::mkConst<CVC4::SubrangeBounds>;
+%template(mkConst) CVC4::ExprManager::mkConst<CVC4::BitVectorRepeat>;
+%template(mkConst) CVC4::ExprManager::mkConst<CVC4::BitVectorExtract>;
+%template(mkConst) CVC4::ExprManager::mkConst<CVC4::BitVectorRotateLeft>;
+%template(mkConst) CVC4::ExprManager::mkConst<CVC4::BitVectorSignExtend>;
+%template(mkConst) CVC4::ExprManager::mkConst<CVC4::BitVectorZeroExtend>;
+%template(mkConst) CVC4::ExprManager::mkConst<CVC4::BitVectorRotateRight>;
+%template(mkConst) CVC4::ExprManager::mkConst<CVC4::UninterpretedConstant>;
+%template(mkConst) CVC4::ExprManager::mkConst<CVC4::kind::Kind_t>;
+%template(mkConst) CVC4::ExprManager::mkConst<CVC4::Datatype>;
+%template(mkConst) CVC4::ExprManager::mkConst<CVC4::Rational>;
+%template(mkConst) CVC4::ExprManager::mkConst<CVC4::BitVector>;
+%template(mkConst) CVC4::ExprManager::mkConst<CVC4::Predicate>;
+%template(mkConst) CVC4::ExprManager::mkConst<std::string>;
+%template(mkConst) CVC4::ExprManager::mkConst<bool>;
+
 %include "expr/expr_manager.h"

diff --git a/src/util/exception.i b/src/util/exception.i
index ab62846333ac5c4be40c1ddc55d6491597c32ab4..c5daadec0f5b83229b3ffef1fd30aa71f09db7cb 100644 (file)
--- a/src/util/exception.i
+++ b/src/util/exception.i
@@ -4,5 +4,6 @@
 
 %ignore CVC4::operator<<(std::ostream&, const Exception&) throw();
 %ignore CVC4::Exception::Exception(const char*) throw();
+%typemap(javabase) CVC4::Exception "java.lang.RuntimeException";
 
 %include "util/exception.h"