From 5ae7ee3df2cc0bd5644a0391bb22be291fb65abc Mon Sep 17 00:00:00 2001
From: Clark Barrett <barrett@cs.nyu.edu>
Date: Fri, 15 Apr 2016 13:31:55 -0700
Subject: [PATCH] Fixes for python bindings

---
 src/expr/expr_manager.i | 22 ++++++++++++++++++----
 src/util/sexpr.i        |  1 +
 2 files changed, 19 insertions(+), 4 deletions(-)

diff --git a/src/expr/expr_manager.i b/src/expr/expr_manager.i
index 66930cf55..0158df3bd 100644
--- a/src/expr/expr_manager.i
+++ b/src/expr/expr_manager.i
@@ -67,10 +67,7 @@
 %template(mkConst) CVC4::ExprManager::mkConst<CVC4::UninterpretedConstant>;
 %template(mkConst) CVC4::ExprManager::mkConst<CVC4::kind::Kind_t>;
 %template(mkConst) CVC4::ExprManager::mkConst<CVC4::Datatype>;
-%template(mkConst) CVC4::ExprManager::mkConst<CVC4::TupleSelect>;
 %template(mkConst) CVC4::ExprManager::mkConst<CVC4::TupleUpdate>;
-%template(mkConst) CVC4::ExprManager::mkConst<CVC4::Record>;
-%template(mkConst) CVC4::ExprManager::mkConst<CVC4::RecordSelect>;
 %template(mkConst) CVC4::ExprManager::mkConst<CVC4::RecordUpdate>;
 %template(mkConst) CVC4::ExprManager::mkConst<CVC4::Rational>;
 %template(mkConst) CVC4::ExprManager::mkConst<CVC4::BitVector>;
@@ -78,6 +75,23 @@
 %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>;
+#ifdef SWIGPYTHON
+/* The python bindings cannot differentiate between bool and other basic
+ * types like enum and int. Therefore, we rename mkConst for the bool
+ * case into mkBoolConst.
+*/
+%template(mkBoolConst) CVC4::ExprManager::mkConst<bool>;
+
+// These cases have trouble too.  Remove them for now.
+//%template(mkConst) CVC4::ExprManager::mkConst<CVC4::TupleSelect>;
+//%template(mkConst) CVC4::ExprManager::mkConst<CVC4::Record>;
+//%template(mkConst) CVC4::ExprManager::mkConst<CVC4::RecordSelect>;
+
+#else
+%template(mkConst) CVC4::ExprManager::mkConst<bool>;		  %template(mkConst) CVC4::ExprManager::mkConst<bool>;
+%template(mkConst) CVC4::ExprManager::mkConst<CVC4::TupleSelect>;
+%template(mkConst) CVC4::ExprManager::mkConst<CVC4::Record>;
+%template(mkConst) CVC4::ExprManager::mkConst<CVC4::RecordSelect>;
+#endif
 
 %include "expr/expr_manager.h"
diff --git a/src/util/sexpr.i b/src/util/sexpr.i
index 4c89c5019..3c865c097 100644
--- a/src/util/sexpr.i
+++ b/src/util/sexpr.i
@@ -4,6 +4,7 @@
 
 %ignore CVC4::operator<<(std::ostream&, const SExpr&);
 %ignore CVC4::operator<<(std::ostream&, SExpr::SexprTypes);
+%ignore CVC4::operator<<(std::ostream&, PrettySExprs);
 
 // for Java and the like
 %extend CVC4::SExpr {
-- 
2.30.2