This commit removes the dead psuedoboolean code.

1 files changed, 4 insertions, 10 deletions

diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index 4aac76eac..431c82476 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -112,31 +112,25 @@ private:
 
   /**
    * (For the moment) the type hierarchy goes as:
-   * PsuedoBoolean <: Integer <: Real
+   * Integer <: Real
    * The type number of a variable is an integer representing the most specific
    * type of the variable. The possible values of type number are:
    */
   enum ArithType
     {
       ATReal = 0,
-      ATInteger = 1,
-      ATPsuedoBoolean = 2
+      ATInteger = 1
    };
 
   std::vector<ArithType> d_variableTypes;
   inline ArithType nodeToArithType(TNode x) const {
-    return x.getType().isPseudoboolean() ? ATPsuedoBoolean :
-      (x.getType().isInteger() ? ATInteger : ATReal);
+    return (x.getType().isInteger() ? ATInteger : ATReal);
   }
 
-  /** Returns true if x is of type Integer or PsuedoBoolean. */
+  /** Returns true if x is of type Integer. */
   inline bool isInteger(ArithVar x) const {
     return d_variableTypes[x] >= ATInteger;
   }
-  /** Returns true if x is of type PsuedoBoolean. */
-  inline bool isPsuedoBoolean(ArithVar x) const {
-    return d_variableTypes[x] == ATPsuedoBoolean;
-  }
 
   /** This is the set of variables initially introduced as slack variables. */
   std::vector<bool> d_slackVars;