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: Minor fixes to language bindings. (Resolves #607.)

---
 src/expr/expr_manager.i | 13 +++++++++++++
 1 file changed, 13 insertions(+)

(limited to 'src/expr')

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>;
-- 
cgit v1.2.3