From: Morgan Deters <mdeters@gmail.com>
Date: Mon, 20 Aug 2012 19:37:30 +0000 (+0000)
Subject: fixes for java bindings
X-Git-Tag: cvc5-1.0.0~7861
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e18075c0b0aaf637b32a4bee54bff1adb6c218ee;p=cvc5.git

fixes for java bindings
---

diff --git a/src/cvc4.i b/src/cvc4.i
index bc9f5a5af..b13a555e6 100644
--- a/src/cvc4.i
+++ b/src/cvc4.i
@@ -103,6 +103,7 @@ using namespace CVC4;
 %include "util/bitvector.i"
 %include "util/subrange_bound.i"
 %include "util/array.i"
+%include "util/array_store_all.i"
 %include "util/hash.i"
 
 %include "expr/type.i"
diff --git a/src/expr/expr.i b/src/expr/expr.i
index 9b6c55703..34f074a6d 100644
--- a/src/expr/expr.i
+++ b/src/expr/expr.i
@@ -30,3 +30,26 @@ namespace CVC4 {
 }/* CVC4 namespace */
 
 %include "expr/expr.h"
+
+%template(getConstTypeConstant) CVC4::Expr::getConst<CVC4::TypeConstant>;
+%template(getConstArrayStoreAll) CVC4::Expr::getConst<CVC4::ArrayStoreAll>;
+%template(getConstBitVectorSize) CVC4::Expr::getConst<CVC4::BitVectorSize>;
+%template(getConstAscriptionType) CVC4::Expr::getConst<CVC4::AscriptionType>;
+%template(getConstBitVectorBitOf) CVC4::Expr::getConst<CVC4::BitVectorBitOf>;
+%template(getConstSubrangeBounds) CVC4::Expr::getConst<CVC4::SubrangeBounds>;
+%template(getConstBitVectorRepeat) CVC4::Expr::getConst<CVC4::BitVectorRepeat>;
+%template(getConstBitVectorExtract) CVC4::Expr::getConst<CVC4::BitVectorExtract>;
+%template(getConstBitVectorRotateLeft) CVC4::Expr::getConst<CVC4::BitVectorRotateLeft>;
+%template(getConstBitVectorSignExtend) CVC4::Expr::getConst<CVC4::BitVectorSignExtend>;
+%template(getConstBitVectorZeroExtend) CVC4::Expr::getConst<CVC4::BitVectorZeroExtend>;
+%template(getConstBitVectorRotateRight) CVC4::Expr::getConst<CVC4::BitVectorRotateRight>;
+%template(getConstUninterpretedConstant) CVC4::Expr::getConst<CVC4::UninterpretedConstant>;
+%template(getConstKind) CVC4::Expr::getConst<CVC4::kind::Kind_t>;
+%template(getConstDatatype) CVC4::Expr::getConst<CVC4::Datatype>;
+%template(getConstRational) CVC4::Expr::getConst<CVC4::Rational>;
+%template(getConstBitVector) CVC4::Expr::getConst<CVC4::BitVector>;
+%template(getConstPredicate) CVC4::Expr::getConst<CVC4::Predicate>;
+%template(getConstString) CVC4::Expr::getConst<std::string>;
+%template(getConstBoolean) CVC4::Expr::getConst<bool>;
+
+%include "expr/expr.h"
diff --git a/src/expr/expr_manager.i b/src/expr/expr_manager.i
index 178f00ccd..0d82c7aa8 100644
--- a/src/expr/expr_manager.i
+++ b/src/expr/expr_manager.i
@@ -17,9 +17,6 @@
 
 %include "expr/expr_manager.h"
 
-%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>;
diff --git a/src/util/Makefile.am b/src/util/Makefile.am
index 8b0b2164f..432e6ef26 100644
--- a/src/util/Makefile.am
+++ b/src/util/Makefile.am
@@ -170,6 +170,7 @@ EXTRA_DIST = \
 	exception.i \
 	language.i \
 	array.i \
+	array_store_all.i \
 	ascription_type.i \
 	rational.i \
 	hash.i
diff --git a/src/util/array_store_all.i b/src/util/array_store_all.i
new file mode 100644
index 000000000..afc14d089
--- /dev/null
+++ b/src/util/array_store_all.i
@@ -0,0 +1,6 @@
+%{
+#include "util/array_store_all.h"
+%}
+
+%include "expr/type.i"
+%include "util/array_store_all.h"