Minor fixes to language bindings. (Resolves #607.)

diff --git a/src/expr/expr_manager.i b/src/expr/expr_manager.i
index fccadf43cf6e7e7f669738276942ba6d56a176d9..66930cf55eb859480f1786c820d32935d24e7674 100644 (file)
--- a/src/expr/expr_manager.i
+++ b/src/expr/expr_manager.i
@@ -52,6 +52,18 @@
 %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::IntToBitVector>;
+//%template(mkConst) CVC4::ExprManager::mkConst<CVC4::FloatingPoint>;
+//%template(mkConst) CVC4::ExprManager::mkConst<CVC4::RoundingMode>;
+//%template(mkConst) CVC4::ExprManager::mkConst<CVC4::FloatingPointSize>;
+//%template(mkConst) CVC4::ExprManager::mkConst<CVC4::FloatingPointToFPIEEEBitVector>;
+//%template(mkConst) CVC4::ExprManager::mkConst<CVC4::FloatingPointToFPFloatingPoint>;
+//%template(mkConst) CVC4::ExprManager::mkConst<CVC4::FloatingPointToFPReal>;
+//%template(mkConst) CVC4::ExprManager::mkConst<CVC4::FloatingPointToFPSignedBitVector>;
+//%template(mkConst) CVC4::ExprManager::mkConst<CVC4::FloatingPointToFPUnsignedBitVector>;
+//%template(mkConst) CVC4::ExprManager::mkConst<CVC4::FloatingPointToFPGeneric>;
+//%template(mkConst) CVC4::ExprManager::mkConst<CVC4::FloatingPointToUBV>;
+//%template(mkConst) CVC4::ExprManager::mkConst<CVC4::FloatingPointToSBV>;
 %template(mkConst) CVC4::ExprManager::mkConst<CVC4::UninterpretedConstant>;
 %template(mkConst) CVC4::ExprManager::mkConst<CVC4::kind::Kind_t>;
 %template(mkConst) CVC4::ExprManager::mkConst<CVC4::Datatype>;
@@ -63,6 +75,7 @@
 %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<CVC4::EmptySet>;
 %template(mkConst) CVC4::ExprManager::mkConst<CVC4::String>;
 %template(mkConst) CVC4::ExprManager::mkConst<CVC4::RegExp>;
 %template(mkConst) CVC4::ExprManager::mkConst<bool>;

diff --git a/src/util/unsat_core.i b/src/util/unsat_core.i
index 060ee3300f5a640fb2940ee09de382b9523c3683..c69dade8f782dfe274afcbd0d5efc2676f10476e 100644 (file)
--- a/src/util/unsat_core.i
+++ b/src/util/unsat_core.i
@@ -9,6 +9,8 @@
 #endif /* SWIGJAVA */
 %}
 
+%ignore CVC4::operator<<(std::ostream&, const UnsatCore&);
+
 #ifdef SWIGJAVA
 
 // Instead of UnsatCore::begin() and end(), create an