fixes for java bindings

diff --git a/src/cvc4.i b/src/cvc4.i
index bc9f5a5afc447ae0ee0faffe461bb798b1208322..b13a555e6a5ddb1ce073ca32ad8a69a038f14452 100644 (file)
--- 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 9b6c557032d2964ccd30bf36abed3a3bdc6b524f..34f074a6dd45f2ebaa5c51aa0a6bbc54001a3859 100644 (file)
--- 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 178f00ccd53dd7b29e452827f9b5b1d22c6b9a1e..0d82c7aa8fa8b1cae9c9fa7bb5cf5dcb2ee26db6 100644 (file)
--- 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 8b0b2164f42d6914e5e183920f2eb1ae7079bd91..432e6ef2608042f9773b97e093fd1da29e2a16a3 100644 (file)
--- 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 (file)
index 0000000..afc14d0
--- /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"