From 69c092f9e2ac6d9628f4de3e0038c1f021b3c7c6 Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Thu, 11 Dec 2014 17:04:29 -0500
Subject: [PATCH] Minor fixes to language bindings. (Resolves #607.)

---
 src/expr/expr_manager.i | 13 +++++++++++++
 src/util/unsat_core.i   |  2 ++
 2 files changed, 15 insertions(+)

diff --git a/src/expr/expr_manager.i b/src/expr/expr_manager.i
index fccadf43c..66930cf55 100644
--- 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 060ee3300..c69dade8f 100644
--- 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
-- 
2.30.2