some api changes

15 files changed, 14 insertions, 127 deletions

diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 18b7bff0f..5e1ec0221 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -140,11 +140,6 @@ StringType ExprManager::stringType() const {
   return StringType(Type(d_nodeManager, new TypeNode(d_nodeManager->stringType())));
 }
 
-KindType ExprManager::kindType() const {
-  NodeManagerScope nms(d_nodeManager);
-  return KindType(Type(d_nodeManager, new TypeNode(d_nodeManager->kindType())));
-}
-
 RealType ExprManager::realType() const {
   NodeManagerScope nms(d_nodeManager);
   return RealType(Type(d_nodeManager, new TypeNode(d_nodeManager->realType())));
diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h
index 8c964a5eb..e20edfb42 100644
--- a/src/expr/expr_manager_template.h
+++ b/src/expr/expr_manager_template.h
@@ -133,9 +133,6 @@ public:
   /** Get the type for strings. */
   StringType stringType() const;
 
-  /** Get the type for sorts. */
-  KindType kindType() const;
-
   /** Get the type for reals. */
   RealType realType() const;
 
diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp
index c607ca0a7..5070c852f 100644
--- a/src/expr/expr_template.cpp
+++ b/src/expr/expr_template.cpp
@@ -436,10 +436,6 @@ bool Expr::isNull() const {
   return d_node->isNull();
 }
 
-Expr::operator bool() const {
-  return !isNull();
-}
-
 bool Expr::isVariable() const {
   ExprManagerScope ems(*this);
   Assert(d_node != NULL, "Unexpected NULL expression pointer!");
diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h
index e26e99ded..96c7cfadf 100644
--- a/src/expr/expr_template.h
+++ b/src/expr/expr_template.h
@@ -148,12 +148,15 @@ struct ExprHashFunction {
   size_t operator()(CVC4::Expr e) const;
 };/* struct ExprHashFunction */
 
+class BoolExpr;
+
 /**
  * Class encapsulating CVC4 expressions and methods for constructing new
  * expressions.
  */
 class CVC4_PUBLIC Expr {
-protected:
+
+  friend class BoolExpr;
 
   /** The internal expression representation */
   NodeTemplate<true>* d_node;
@@ -417,13 +420,6 @@ public:
   bool isNull() const;
 
   /**
-   * Check if this is a null expression.
-   *
-   * @return true if NOT a null expression
-   */
-  operator bool() const;
-
-  /**
    * Check if this is an expression representing a variable.
    *
    * @return true if a variable expression
@@ -526,8 +522,6 @@ private:
    */
   void debugPrint();
 
-protected:
-
   /**
    * Returns the actual internal node.
    * @return the internal node
@@ -961,7 +955,7 @@ public:
 
 ${getConst_instantiations}
 
-#line 965 "${template}"
+#line 959 "${template}"
 
 namespace expr {
 
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 893fde64b..4a05b174d 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -658,9 +658,6 @@ public:
   /** Get the (singleton) type for strings. */
   inline TypeNode stringType();
 
-  /** Get the (singleton) type for sorts. */
-  inline TypeNode kindType();
-
   /** Get the bound var list type. */
   inline TypeNode boundVarListType();
 
@@ -983,11 +980,6 @@ inline TypeNode NodeManager::stringType() {
   return TypeNode(mkTypeConst<TypeConstant>(STRING_TYPE));
 }
 
-/** Get the (singleton) type for sorts. */
-inline TypeNode NodeManager::kindType() {
-  return TypeNode(mkTypeConst<TypeConstant>(KIND_TYPE));
-}
-
 /** Get the bound var list type. */
 inline TypeNode NodeManager::boundVarListType() {
   return TypeNode(mkTypeConst<TypeConstant>(BOUND_VAR_LIST_TYPE));
diff --git a/src/expr/type.cpp b/src/expr/type.cpp
index d67aa1fe3..b55d33dcf 100644
--- a/src/expr/type.cpp
+++ b/src/expr/type.cpp
@@ -411,19 +411,6 @@ Type::operator SubrangeType() const throw(AssertionException) {
   return SubrangeType(*this);
 }
 
-/** Is this a kind type (i.e., the type of a type)? */
-bool Type::isKind() const {
-  NodeManagerScope nms(d_nodeManager);
-  return d_typeNode->isKind();
-}
-
-/** Cast to a kind type */
-Type::operator KindType() const throw(AssertionException) {
-  NodeManagerScope nms(d_nodeManager);
-  Assert(isNull() || isKind());
-  return KindType(*this);
-}
-
 vector<Type> FunctionType::getArgTypes() const {
   NodeManagerScope nms(d_nodeManager);
   vector<Type> args;
@@ -551,11 +538,6 @@ ArrayType::ArrayType(const Type& t) throw(AssertionException) :
   Assert(isNull() || isArray());
 }
 
-KindType::KindType(const Type& t) throw(AssertionException) :
-  Type(t) {
-  Assert(isNull() || isKind());
-}
-
 SortType::SortType(const Type& t) throw(AssertionException) :
   Type(t) {
   Assert(isNull() || isSort());
diff --git a/src/expr/type.h b/src/expr/type.h
index 29b0ac128..513a4d60a 100644
--- a/src/expr/type.h
+++ b/src/expr/type.h
@@ -57,7 +57,6 @@ class SelectorType;
 class TesterType;
 class FunctionType;
 class TupleType;
-class KindType;
 class SortType;
 class SortConstructorType;
 class PredicateSubtype;
@@ -428,18 +427,6 @@ public:
   operator SubrangeType() const throw(AssertionException);
 
   /**
-   * Is this a kind type (i.e., the type of a type)?
-   * @return true if this is a kind type
-   */
-  bool isKind() const;
-
-  /**
-   * Cast to a kind type
-   * @return the kind type
-   */
-  operator KindType() const throw(AssertionException);
-
-  /**
    * Outputs a string representation of this type to the stream.
    * @param out the stream to output to
    */
@@ -619,17 +606,6 @@ public:
 };/* class SubrangeType */
 
 /**
- * Class encapsulating the kind type (the type of types).
- */
-class CVC4_PUBLIC KindType : public Type {
-
-public:
-
-  /** Construct from the base type */
-  KindType(const Type& type = Type()) throw(AssertionException);
-};/* class KindType */
-
-/**
  * Class encapsulating the bit-vector type.
  */
 class CVC4_PUBLIC BitVectorType : public Type {
diff --git a/src/expr/type_checker_template.cpp b/src/expr/type_checker_template.cpp
index d559477f1..450baf505 100644
--- a/src/expr/type_checker_template.cpp
+++ b/src/expr/type_checker_template.cpp
@@ -41,13 +41,10 @@ TypeNode TypeChecker::computeType(NodeManager* nodeManager, TNode n, bool check)
   case kind::BUILTIN:
     typeNode = nodeManager->builtinOperatorType();
     break;
-  case kind::SORT_TYPE:
-    typeNode = nodeManager->kindType();
-    break;
 
 ${typerules}
 
-#line 51 "${template}"
+#line 48 "${template}"
 
   default:
     Debug("getType") << "FAILURE" << std::endl;
@@ -70,7 +67,7 @@ bool TypeChecker::computeIsConst(NodeManager* nodeManager, TNode n)
   switch(n.getKind()) {
 ${construles}
 
-#line 74 "${template}"
+#line 71 "${template}"
 
   default:;
   }
diff --git a/src/expr/type_node.h b/src/expr/type_node.h
index e848cf9a9..af0734575 100644
--- a/src/expr/type_node.h
+++ b/src/expr/type_node.h
@@ -592,10 +592,6 @@ public:
   /** Get the bounds defining this subrange */
   const SubrangeBounds& getSubrangeBounds() const;
 
-  /** Is this a kind type (i.e., the type of a type)? */
-  bool isKind() const;
-
-
   /**
    * Returns the leastUpperBound in the extended type lattice of the two types.
    * If this is \top, i.e. there is no inhabited type that contains both,
@@ -899,12 +895,6 @@ inline bool TypeNode::isSubrange() const {
     ( isPredicateSubtype() && getSubtypeBaseType().isSubrange() );
 }
 
-/** Is this a kind type (i.e., the type of a type)? */
-inline bool TypeNode::isKind() const {
-  return getKind() == kind::TYPE_CONSTANT &&
-    getConst<TypeConstant>() == KIND_TYPE;
-}
-
 /** Is this a bit-vector type */
 inline bool TypeNode::isBitVector() const {
   return getKind() == kind::BITVECTOR_TYPE ||
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index 35a85e681..a6693dd22 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -150,9 +150,6 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo
       case BOOLEAN_TYPE:
         out << "BOOLEAN";
         break;
-      case KIND_TYPE:
-        out << "TYPE";
-        break;
       default:
         out << tc;
         break;
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 6e8cc9b5d..cedd866f9 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1888,7 +1888,7 @@ Expr SmtEngine::getValue(const Expr& e)
       "Cannot get value unless immediately preceded by SAT/INVALID or UNKNOWN response.";
     throw ModalException(msg);
   }
-  if(type.isKind() || type.isSortConstructor()) {
+  if(type.isSort() || type.isSortConstructor()) {
     const char* msg =
       "Cannot get value of a sort.";
     throw ModalException(msg);
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index cbb97f9f7..0214cddd3 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -559,7 +559,10 @@ public:
    */
   SExpr getStatistic(std::string name) const throw();
 
-  Result getStatusOfLastCommand() const {
+  /**
+   * Returns the most recent result of checkSat/query or (set-info :status).
+   */
+  Result getStatusOfLastCommand() const throw() {
     return d_status;
   }
 
diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds
index da31d157f..8eff22ed4 100644
--- a/src/theory/builtin/kinds
+++ b/src/theory/builtin/kinds
@@ -251,13 +251,6 @@ sort BUILTIN_OPERATOR_TYPE \
     not-well-founded \
     "Built in type for built in operators"
 
-# Justified because we can have an unbounded-but-finite number of
-# sorts.  Assuming we have |Z| is probably ok for now..
-sort KIND_TYPE \
-    Cardinality::INTEGERS \
-    not-well-founded \
-    "Uninterpreted Sort"
-
 variable SORT_TAG "sort tag"
 parameterized SORT_TYPE SORT_TAG 0: "sort type"
 # This is really "unknown" cardinality, but maybe this will be good
diff --git a/test/regress/regress0/datatypes/Makefile.am b/test/regress/regress0/datatypes/Makefile.am
index 2ec558f20..aca663e18 100644
--- a/test/regress/regress0/datatypes/Makefile.am
+++ b/test/regress/regress0/datatypes/Makefile.am
@@ -40,10 +40,10 @@ TESTS =	\
 	v3l60006.cvc \
 	v5l30058.cvc \
 	bug286.cvc \
-	wrong-sel-simp.cvc
+	wrong-sel-simp.cvc \
+	rec2.cvc
 
 FAILING_TESTS = \
-	rec2.cvc \
 	rec5.cvc \
 	datatype-dump.cvc
 
diff --git a/test/unit/expr/node_manager_black.h b/test/unit/expr/node_manager_black.h
index 75c3618ff..18dc96c98 100644
--- a/test/unit/expr/node_manager_black.h
+++ b/test/unit/expr/node_manager_black.h
@@ -180,7 +180,6 @@ public:
     TypeNode t3 = d_nodeManager->mkSort("T");
     TS_ASSERT( t.isBoolean() );
     TS_ASSERT( !t.isFunction() );
-    TS_ASSERT( !t.isKind() );
     TS_ASSERT( !t.isNull() );
     TS_ASSERT( !t.isPredicate() );
     TS_ASSERT( !t.isSort() );
@@ -191,26 +190,6 @@ public:
     TS_ASSERT_EQUALS( bt, t);
   }
 
-  void testKindType() {
-    TypeNode t = d_nodeManager->kindType();
-    TypeNode t2 = d_nodeManager->kindType();
-    TypeNode t3 = d_nodeManager->mkSort("T");
-
-    TS_ASSERT( !t.isBoolean() );
-    TS_ASSERT( !t.isFunction() );
-    TS_ASSERT( t.isKind() );
-    TS_ASSERT( !t.isNull() );
-    TS_ASSERT( !t.isPredicate() );
-    TS_ASSERT( !t.isSort() );
-
-    TS_ASSERT_EQUALS(t, t2);
-    TS_ASSERT( t != t3);
-
-    TypeNode kt = t;
-    TS_ASSERT_EQUALS( kt, t );
-    // TODO: Is there a way to get the type of otherType (it should == t)?
-  }
-
   void testMkFunctionTypeBoolToBool() {
     TypeNode booleanType = d_nodeManager->booleanType();
     TypeNode t = d_nodeManager->mkFunctionType(booleanType,booleanType);
@@ -218,7 +197,6 @@ public:
 
     TS_ASSERT( !t.isBoolean() );
     TS_ASSERT( t.isFunction() );
-    TS_ASSERT( !t.isKind() );
     TS_ASSERT( !t.isNull() );
     TS_ASSERT( t.isPredicate() );
     TS_ASSERT( !t.isSort() );
@@ -247,7 +225,6 @@ public:
 
     TS_ASSERT( !t.isBoolean() );
     TS_ASSERT( t.isFunction() );
-    TS_ASSERT( !t.isKind() );
     TS_ASSERT( !t.isNull() );
     TS_ASSERT( !t.isPredicate() );
     TS_ASSERT( !t.isSort() );
@@ -278,7 +255,6 @@ public:
 
     TS_ASSERT( !t.isBoolean() );
     TS_ASSERT( t.isFunction() );
-    TS_ASSERT( !t.isKind() );
     TS_ASSERT( !t.isNull() );
     TS_ASSERT( !t.isPredicate() );
     TS_ASSERT( !t.isSort() );
@@ -309,7 +285,6 @@ public:
 
     TS_ASSERT( !t.isBoolean() );
     TS_ASSERT( t.isFunction() );
-    TS_ASSERT( !t.isKind() );
     TS_ASSERT( !t.isNull() );
     TS_ASSERT( t.isPredicate() );
     TS_ASSERT( !t.isSort() );