From: Clark Barrett <barrett@cs.nyu.edu>
Date: Mon, 18 Apr 2016 23:06:45 +0000 (-0700)
Subject: More fixes for python interface
X-Git-Tag: cvc5-1.0.0~6049^2~64
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d60204229552bc9009f86c6fbc809dbd42dd6ef4;p=cvc5.git

More fixes for python interface
---

diff --git a/src/expr/expr.i b/src/expr/expr.i
index b50686f52..ae8b85560 100644
--- a/src/expr/expr.i
+++ b/src/expr/expr.i
@@ -130,7 +130,14 @@ namespace CVC4 {
 
 %include "expr/expr.h"
 
+#ifdef SWIGPYTHON
+/* The python bindings on Mac OS X have trouble with this one - leave it
+ * out for now. */
+*/
+//%template(getConstTypeConstant) CVC4::Expr::getConst<CVC4::TypeConstant>;
+#else
 %template(getConstTypeConstant) CVC4::Expr::getConst<CVC4::TypeConstant>;
+#endif
 %template(getConstArrayStoreAll) CVC4::Expr::getConst<CVC4::ArrayStoreAll>;
 %template(getConstBitVectorSize) CVC4::Expr::getConst<CVC4::BitVectorSize>;
 %template(getConstAscriptionType) CVC4::Expr::getConst<CVC4::AscriptionType>;
diff --git a/src/expr/expr_manager.i b/src/expr/expr_manager.i
index 0158df3bd..11c1e284d 100644
--- a/src/expr/expr_manager.i
+++ b/src/expr/expr_manager.i
@@ -40,7 +40,6 @@
 
 %include "expr/expr_manager.h"
 
-%template(mkConst) CVC4::ExprManager::mkConst<CVC4::TypeConstant>;
 %template(mkConst) CVC4::ExprManager::mkConst<CVC4::ArrayStoreAll>;
 %template(mkConst) CVC4::ExprManager::mkConst<CVC4::BitVectorSize>;
 %template(mkConst) CVC4::ExprManager::mkConst<CVC4::AscriptionType>;
@@ -83,15 +82,17 @@
 %template(mkBoolConst) CVC4::ExprManager::mkConst<bool>;
 
 // These cases have trouble too.  Remove them for now.
+//%template(mkConst) CVC4::ExprManager::mkConst<CVC4::TypeConstant>;
 //%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::TypeConstant>;
 %template(mkConst) CVC4::ExprManager::mkConst<CVC4::TupleSelect>;
 %template(mkConst) CVC4::ExprManager::mkConst<CVC4::Record>;
 %template(mkConst) CVC4::ExprManager::mkConst<CVC4::RecordSelect>;
+%template(mkConst) CVC4::ExprManager::mkConst<bool>;
 #endif
 
 %include "expr/expr_manager.h"