From: Morgan Deters <mdeters@gmail.com>
Date: Thu, 16 Aug 2012 01:58:41 +0000 (+0000)
Subject: fix exceptions and mkConst() in java binding
X-Git-Tag: cvc5-1.0.0~7867
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3e07620deae66ac9efaad3566186462356436011;p=cvc5.git

fix exceptions and mkConst() in java binding
---

diff --git a/src/expr/expr_manager.i b/src/expr/expr_manager.i
index 960ba8f84..178f00ccd 100644
--- 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 ab6284633..c5daadec0 100644
--- 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"