This commit removes the dead psuedoboolean code.

6 files changed, 1 insertions, 65 deletions

diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 593f3f715..2bcf5e18c 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -890,11 +890,6 @@ inline TypeNode NodeManager::realType() {
   return TypeNode(mkTypeConst<TypeConstant>(REAL_TYPE));
 }
 
-/** Get the (singleton) type for pseudobooleans. */
-inline TypeNode NodeManager::pseudobooleanType() {
-  return TypeNode(mkTypeConst<TypeConstant>(PSEUDOBOOLEAN_TYPE));
-}
-
 /** Get the (singleton) type for strings. */
 inline TypeNode NodeManager::stringType() {
   return TypeNode(mkTypeConst<TypeConstant>(STRING_TYPE));
diff --git a/src/expr/type.cpp b/src/expr/type.cpp
index eaf10ba20..df222b684 100644
--- a/src/expr/type.cpp
+++ b/src/expr/type.cpp
@@ -224,19 +224,6 @@ Type::operator RealType() const throw(AssertionException) {
   return RealType(*this);
 }
 
-/** Is this the pseudoboolean type? */
-bool Type::isPseudoboolean() const {
-  NodeManagerScope nms(d_nodeManager);
-  return d_typeNode->isPseudoboolean();
-}
-
-/** Cast to a pseudoboolean type */
-Type::operator PseudobooleanType() const throw(AssertionException) {
-  NodeManagerScope nms(d_nodeManager);
-  Assert(isNull() || isPseudoboolean());
-  return PseudobooleanType(*this);
-}
-
 /** Is this the string type? */
 bool Type::isString() const {
   NodeManagerScope nms(d_nodeManager);
@@ -509,11 +496,6 @@ RealType::RealType(const Type& t) throw(AssertionException) :
   Assert(isNull() || isReal());
 }
 
-PseudobooleanType::PseudobooleanType(const Type& t) throw(AssertionException) :
-  Type(t) {
-  Assert(isNull() || isPseudoboolean());
-}
-
 StringType::StringType(const Type& t) throw(AssertionException) :
   Type(t) {
   Assert(isNull() || isString());
diff --git a/src/expr/type.h b/src/expr/type.h
index 76fccb37b..8e9190ac5 100644
--- a/src/expr/type.h
+++ b/src/expr/type.h
@@ -48,7 +48,6 @@ class NodeTemplate;
 class BooleanType;
 class IntegerType;
 class RealType;
-class PseudobooleanType;
 class StringType;
 class BitVectorType;
 class ArrayType;
@@ -257,18 +256,6 @@ public:
   operator RealType() const throw(AssertionException);
 
   /**
-   * Is this the pseudoboolean type?
-   * @return true if the type is the pseudoboolean type
-   */
-  bool isPseudoboolean() const;
-
-  /**
-   * Cast this type to a pseudoboolean type
-   * @return the PseudobooleanType
-   */
-  operator PseudobooleanType() const throw(AssertionException);
-
-  /**
    * Is this the string type?
    * @return true if the type is the string type
    */
@@ -489,17 +476,6 @@ public:
 };/* class RealType */
 
 /**
- * Singleton class encapsulating the pseudoboolean type.
- */
-class CVC4_PUBLIC PseudobooleanType : public Type {
-
-public:
-
-  /** Construct from the base type */
-  PseudobooleanType(const Type& type) throw(AssertionException);
-};/* class PseudobooleanType */
-
-/**
  * Singleton class encapsulating the string type.
  */
 class CVC4_PUBLIC StringType : public Type {
diff --git a/src/expr/type.i b/src/expr/type.i
index 13ae9663e..0646ec8cd 100644
--- a/src/expr/type.i
+++ b/src/expr/type.i
@@ -17,7 +17,6 @@
 %rename(toBooleanType) CVC4::Type::operator BooleanType() const;
 %rename(toIntegerType) CVC4::Type::operator IntegerType() const;
 %rename(toRealType) CVC4::Type::operator RealType() const;
-%rename(toPseudobooleanType) CVC4::Type::operator PseudobooleanType() const;
 %rename(toStringType) CVC4::Type::operator StringType() const;
 %rename(toBitVectorType) CVC4::Type::operator BitVectorType() const;
 %rename(toFunctionType) CVC4::Type::operator FunctionType() const;
diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
index 4ddb01974..3f5c3a032 100644
--- a/src/expr/type_node.cpp
+++ b/src/expr/type_node.cpp
@@ -77,10 +77,6 @@ bool TypeNode::isSubtypeOf(TypeNode t) const {
   }
   if(getKind() == kind::TYPE_CONSTANT) {
     switch(getConst<TypeConstant>()) {
-    case PSEUDOBOOLEAN_TYPE:
-      return t.getKind() == kind::TYPE_CONSTANT &&
-        ( t.getConst<TypeConstant>() == BOOLEAN_TYPE ||
-          t.getConst<TypeConstant>() == INTEGER_TYPE );
     case INTEGER_TYPE:
       return t.getKind() == kind::TYPE_CONSTANT && t.getConst<TypeConstant>() == REAL_TYPE;
     default:
diff --git a/src/expr/type_node.h b/src/expr/type_node.h
index 7fe3bc75e..25b5e4bb3 100644
--- a/src/expr/type_node.h
+++ b/src/expr/type_node.h
@@ -465,9 +465,6 @@ public:
   /** Is this the Real type? */
   bool isReal() const;
 
-  /** Is this the Pseudoboolean type? */
-  bool isPseudoboolean() const;
-
   /** Is this the String type? */
   bool isString() const;
 
@@ -792,7 +789,6 @@ inline void TypeNode::printAst(std::ostream& out, int indent) const {
 inline bool TypeNode::isBoolean() const {
   return
     ( getKind() == kind::TYPE_CONSTANT && getConst<TypeConstant>() == BOOLEAN_TYPE ) ||
-      isPseudoboolean() ||
     ( isPredicateSubtype() && getSubtypeBaseType().isBoolean() );
 }
 
@@ -800,7 +796,6 @@ inline bool TypeNode::isInteger() const {
   return
     ( getKind() == kind::TYPE_CONSTANT && getConst<TypeConstant>() == INTEGER_TYPE ) ||
     isSubrange() ||
-    isPseudoboolean() ||
     ( isPredicateSubtype() && getSubtypeBaseType().isInteger() );
 }
 
@@ -811,20 +806,13 @@ inline bool TypeNode::isReal() const {
     ( isPredicateSubtype() && getSubtypeBaseType().isReal() );
 }
 
-inline bool TypeNode::isPseudoboolean() const {
-  return
-    ( getKind() == kind::TYPE_CONSTANT && getConst<TypeConstant>() == PSEUDOBOOLEAN_TYPE ) ||
-    ( isPredicateSubtype() && getSubtypeBaseType().isPseudoboolean() );
-}
-
 inline bool TypeNode::isString() const {
   return getKind() == kind::TYPE_CONSTANT &&
     getConst<TypeConstant>() == STRING_TYPE;
 }
 
 inline bool TypeNode::isArray() const {
-  return getKind() == kind::ARRAY_TYPE ||
-    ( isPredicateSubtype() && getSubtypeBaseType().isPseudoboolean() );
+  return getKind() == kind::ARRAY_TYPE;
 }
 
 inline TypeNode TypeNode::getArrayIndexType() const {