considerable bindings interface work, some improvements to build

3 files changed, 33 insertions, 31 deletions

diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h
index e95e434fe..616a7c8ff 100644
--- a/src/expr/expr_template.h
+++ b/src/expr/expr_template.h
@@ -506,7 +506,7 @@ protected:
   friend class ExprManager;
   friend class NodeManager;
   friend class TypeCheckingException;
-  friend std::ostream& operator<<(std::ostream& out, const Expr& e);
+  friend std::ostream& CVC4::operator<<(std::ostream& out, const Expr& e);
   template <bool ref_count> friend class NodeTemplate;
 
 };/* class Expr */
diff --git a/src/expr/kind.i b/src/expr/kind.i
index 1c17f3ff9..95c350cf3 100644
--- a/src/expr/kind.i
+++ b/src/expr/kind.i
@@ -8,4 +8,6 @@
 
 %ignore CVC4::theory::operator++(TheoryId&);
 
+%rename(Kind) CVC4::kind::Kind_t;
+
 %include "expr/kind.h"
diff --git a/src/expr/type.cpp b/src/expr/type.cpp
index ff47c6eae..0edc7579b 100644
--- a/src/expr/type.cpp
+++ b/src/expr/type.cpp
@@ -184,7 +184,7 @@ bool Type::isBoolean() const {
 /** Cast to a Boolean type */
 Type::operator BooleanType() const throw(AssertionException) {
   NodeManagerScope nms(d_nodeManager);
-  Assert(isBoolean());
+  Assert(isNull() || isBoolean());
   return BooleanType(*this);
 }
 
@@ -197,7 +197,7 @@ bool Type::isInteger() const {
 /** Cast to a integer type */
 Type::operator IntegerType() const throw(AssertionException) {
   NodeManagerScope nms(d_nodeManager);
-  Assert(isInteger());
+  Assert(isNull() || isInteger());
   return IntegerType(*this);
 }
 
@@ -210,7 +210,7 @@ bool Type::isReal() const {
 /** Cast to a real type */
 Type::operator RealType() const throw(AssertionException) {
   NodeManagerScope nms(d_nodeManager);
-  Assert(isReal());
+  Assert(isNull() || isReal());
   return RealType(*this);
 }
 
@@ -223,7 +223,7 @@ bool Type::isPseudoboolean() const {
 /** Cast to a pseudoboolean type */
 Type::operator PseudobooleanType() const throw(AssertionException) {
   NodeManagerScope nms(d_nodeManager);
-  Assert(isPseudoboolean());
+  Assert(isNull() || isPseudoboolean());
   return PseudobooleanType(*this);
 }
 
@@ -236,14 +236,14 @@ bool Type::isBitVector() const {
 /** Cast to a bit-vector type */
 Type::operator BitVectorType() const throw(AssertionException) {
   NodeManagerScope nms(d_nodeManager);
-  Assert(isBitVector());
+  Assert(isNull() || isBitVector());
   return BitVectorType(*this);
 }
 
 /** Cast to a Constructor type */
 Type::operator DatatypeType() const throw(AssertionException) {
   NodeManagerScope nms(d_nodeManager);
-  Assert(isDatatype());
+  Assert(isNull() || isDatatype());
   return DatatypeType(*this);
 }
 
@@ -256,7 +256,7 @@ bool Type::isDatatype() const {
 /** Cast to a Constructor type */
 Type::operator ConstructorType() const throw(AssertionException) {
   NodeManagerScope nms(d_nodeManager);
-  Assert(isConstructor());
+  Assert(isNull() || isConstructor());
   return ConstructorType(*this);
 }
 
@@ -269,7 +269,7 @@ bool Type::isConstructor() const {
 /** Cast to a Selector type */
 Type::operator SelectorType() const throw(AssertionException) {
   NodeManagerScope nms(d_nodeManager);
-  Assert(isSelector());
+  Assert(isNull() || isSelector());
   return SelectorType(*this);
 }
 
@@ -282,7 +282,7 @@ bool Type::isSelector() const {
 /** Cast to a Tester type */
 Type::operator TesterType() const throw(AssertionException) {
   NodeManagerScope nms(d_nodeManager);
-  Assert(isTester());
+  Assert(isNull() || isTester());
   return TesterType(*this);
 }
 
@@ -310,7 +310,7 @@ bool Type::isPredicate() const {
 /** Cast to a function type */
 Type::operator FunctionType() const throw(AssertionException) {
   NodeManagerScope nms(d_nodeManager);
-  Assert(isFunction());
+  Assert(isNull() || isFunction());
   return FunctionType(*this);
 }
 
@@ -323,7 +323,7 @@ bool Type::isTuple() const {
 /** Cast to a tuple type */
 Type::operator TupleType() const throw(AssertionException) {
   NodeManagerScope nms(d_nodeManager);
-  Assert(isTuple());
+  Assert(isNull() || isTuple());
   return TupleType(*this);
 }
 
@@ -348,7 +348,7 @@ bool Type::isSort() const {
 /** Cast to a sort type */
 Type::operator SortType() const throw(AssertionException) {
   NodeManagerScope nms(d_nodeManager);
-  Assert(isSort());
+  Assert(isNull() || isSort());
   return SortType(*this);
 }
 
@@ -361,7 +361,7 @@ bool Type::isSortConstructor() const {
 /** Cast to a sort type */
 Type::operator SortConstructorType() const throw(AssertionException) {
   NodeManagerScope nms(d_nodeManager);
-  Assert(isSortConstructor());
+  Assert(isNull() || isSortConstructor());
   return SortConstructorType(*this);
 }
 
@@ -374,7 +374,7 @@ bool Type::isKind() const {
 /** Cast to a kind type */
 Type::operator KindType() const throw(AssertionException) {
   NodeManagerScope nms(d_nodeManager);
-  Assert(isKind());
+  Assert(isNull() || isKind());
   return KindType(*this);
 }
 
@@ -392,7 +392,7 @@ vector<Type> FunctionType::getArgTypes() const {
 
 Type FunctionType::getRangeType() const {
   NodeManagerScope nms(d_nodeManager);
-  Assert(isFunction());
+  Assert(isNull() || isFunction());
   return makeType(d_typeNode->getRangeType());
 }
 
@@ -447,78 +447,78 @@ SortType SortConstructorType::instantiate(const std::vector<Type>& params) const
 
 BooleanType::BooleanType(const Type& t) throw(AssertionException) :
   Type(t) {
-  Assert(isBoolean());
+  Assert(isNull() || isBoolean());
 }
 
 IntegerType::IntegerType(const Type& t) throw(AssertionException) :
   Type(t) {
-  Assert(isInteger());
+  Assert(isNull() || isInteger());
 }
 
 RealType::RealType(const Type& t) throw(AssertionException) :
   Type(t) {
-  Assert(isReal());
+  Assert(isNull() || isReal());
 }
 
 PseudobooleanType::PseudobooleanType(const Type& t) throw(AssertionException) :
   Type(t) {
-  Assert(isPseudoboolean());
+  Assert(isNull() || isPseudoboolean());
 }
 
 BitVectorType::BitVectorType(const Type& t) throw(AssertionException) :
   Type(t) {
-  Assert(isBitVector());
+  Assert(isNull() || isBitVector());
 }
 
 DatatypeType::DatatypeType(const Type& t) throw(AssertionException) :
   Type(t) {
-  Assert(isDatatype());
+  Assert(isNull() || isDatatype());
 }
 
 ConstructorType::ConstructorType(const Type& t) throw(AssertionException) :
   Type(t) {
-  Assert(isConstructor());
+  Assert(isNull() || isConstructor());
 }
 
 SelectorType::SelectorType(const Type& t) throw(AssertionException) :
   Type(t) {
-  Assert(isSelector());
+  Assert(isNull() || isSelector());
 }
 
 TesterType::TesterType(const Type& t) throw(AssertionException) :
   Type(t) {
-  Assert(isTester());
+  Assert(isNull() || isTester());
 }
 
 FunctionType::FunctionType(const Type& t) throw(AssertionException) :
   Type(t) {
-  Assert(isFunction());
+  Assert(isNull() || isFunction());
 }
 
 TupleType::TupleType(const Type& t) throw(AssertionException) :
   Type(t) {
-  Assert(isTuple());
+  Assert(isNull() || isTuple());
 }
 
 ArrayType::ArrayType(const Type& t) throw(AssertionException) :
   Type(t) {
-  Assert(isArray());
+  Assert(isNull() || isArray());
 }
 
 KindType::KindType(const Type& t) throw(AssertionException) :
   Type(t) {
-  Assert(isKind());
+  Assert(isNull() || isKind());
 }
 
 SortType::SortType(const Type& t) throw(AssertionException) :
   Type(t) {
-  Assert(isSort());
+  Assert(isNull() || isSort());
 }
 
 SortConstructorType::SortConstructorType(const Type& t)
   throw(AssertionException) :
   Type(t) {
-  Assert(isSortConstructor());
+  Assert(isNull() || isSortConstructor());
 }
 
 unsigned BitVectorType::getSize() const {