From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Thu, 11 Dec 2014 22:04:29 +0000 (-0500)
Subject: Minor fixes to language bindings. (Resolves #607.)
X-Git-Tag: cvc5-1.0.0~6463
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=69c092f9e2ac6d9628f4de3e0038c1f021b3c7c6;p=cvc5.git

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

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