some api changes

diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 18b7bff0ffce230026685dd8c9203fd334d77b96..5e1ec02217aa370a96fb54608ce5039976ffb6a9 100644 (file)
--- 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 8c964a5eb114af67c0ae3868736e73ac5d2ba63e..e20edfb42eb268f1e2bd7321024590e15ca1c5ac 100644 (file)
--- 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 c607ca0a7bb7d64e28da06cd3a2cee410b597a89..5070c852ffc52d5c23543f0ae5f67c0c0df459ed 100644 (file)
--- 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 e26e99ded7e5f7942313f9d0a6f6a9946e0ab155..96c7cfadfb67a5f72f6de96700d9621bc034a9b0 100644 (file)
--- 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;
@@ -416,13 +419,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.
    *
@@ -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 893fde64bda5403707e57d449c012a752b863c98..4a05b174df7ea7178d49348f6f3a51cb8f33401c 100644 (file)
--- 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 d67aa1fe3f0f91f13a0528d16609d47df4064b54..b55d33dcf1dda2a045023334583b70b045eac719 100644 (file)
--- 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 29b0ac128b4fc1a01000e3e7a4a4625943e290ed..513a4d60a0b870a58c4971b1b6ff55db66b42255 100644 (file)
--- 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;
@@ -427,18 +426,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
@@ -618,17 +605,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.
  */

diff --git a/src/expr/type_checker_template.cpp b/src/expr/type_checker_template.cpp
index d559477f19984e2276333f556447e3925da6836f..450baf505007570a5589bbe0a61b184646687d6a 100644 (file)
--- 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 e848cf9a93a4f564307aee7a466b5020ebcb7aeb..af073457520c0bb6a217ff1ff56424228634a0a2 100644 (file)
--- 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 35a85e681809f294c4e33a06e1e98c24636630e2..a6693dd2271249fdcba7c479d73b436e4ee3484c 100644 (file)
--- 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 6e8cc9b5d0c38c9e542555516f1188334dea3684..cedd866f977e9943c20f3f1c1c82c42c2f359987 100644 (file)
--- 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 cbb97f9f74cf45073ac85341ef856d5ff09c0ec2..0214cddd3ce31497e63b5a5ab859e490aa503c8c 100644 (file)
--- 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 da31d157fb29b93a9f294ddc16ff2fea6f81ff8f..8eff22ed45d99d471dcbc4f356ff8ac0b0300744 100644 (file)
--- 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 2ec558f201672285bde745134deb0e8adbc17035..aca663e1801ca5a1a64c459c6dbb8c1a22896235 100644 (file)
--- 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 75c3618ff1467ea3f7f87b738d8999f2aaf67c4d..18dc96c9874f66910a59f0db17a83c3f081a52d5 100644 (file)
--- 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() );