Fixes for python bindings

diff --git a/src/expr/expr_manager.i b/src/expr/expr_manager.i
index 66930cf55eb859480f1786c820d32935d24e7674..0158df3bdd19971d3764632395e9c696d21d3fd6 100644 (file)
--- 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 4c89c501929a5ad4ba7f23e9c4bfec4566976f38..3c865c09770a1066ab9132acad665c53ca460395 100644 (file)
--- 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 {