From: Clark Barrett <barrett@cs.nyu.edu>
Date: Fri, 15 Apr 2016 20:31:55 +0000 (-0700)
Subject: Fixes for python bindings
X-Git-Tag: cvc5-1.0.0~6049^2~67
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=5ae7ee3df2cc0bd5644a0391bb22be291fb65abc;p=cvc5.git

Fixes for python bindings
---

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 {