Reverting r365

7 files changed, 50 insertions, 118 deletions

diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 6a2640080..fa1a1a6af 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -57,34 +57,16 @@ KindType* ExprManager::kindType() const {
 }
 
 Expr ExprManager::mkExpr(Kind kind) {
-  const unsigned n = 0;
-  CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
-                "Exprs with kind %s must have at least %u children and "
-                "at most %u children (the one under construction has %u)",
-                kind::kindToString(kind).c_str(),
-                minArity(kind), maxArity(kind), n);
   NodeManagerScope nms(d_nodeManager);
   return Expr(this, new Node(d_nodeManager->mkNode(kind)));
 }
 
 Expr ExprManager::mkExpr(Kind kind, const Expr& child1) {
-  const unsigned n = 1;
-  CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
-                "Exprs with kind %s must have at least %u children and "
-                "at most %u children (the one under construction has %u)",
-                kind::kindToString(kind).c_str(),
-                minArity(kind), maxArity(kind), n);
   NodeManagerScope nms(d_nodeManager);
   return Expr(this, new Node(d_nodeManager->mkNode(kind, child1.getNode())));
 }
 
 Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2) {
-  const unsigned n = 2;
-  CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
-                "Exprs with kind %s must have at least %u children and "
-                "at most %u children (the one under construction has %u)",
-                kind::kindToString(kind).c_str(),
-                minArity(kind), maxArity(kind), n);
   NodeManagerScope nms(d_nodeManager);
   return Expr(this, new Node(d_nodeManager->mkNode(kind, child1.getNode(),
                                           child2.getNode())));
@@ -92,12 +74,6 @@ Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2) {
 
 Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2,
                          const Expr& child3) {
-  const unsigned n = 3;
-  CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
-                "Exprs with kind %s must have at least %u children and "
-                "at most %u children (the one under construction has %u)",
-                kind::kindToString(kind).c_str(),
-                minArity(kind), maxArity(kind), n);
   NodeManagerScope nms(d_nodeManager);
   return Expr(this, new Node(d_nodeManager->mkNode(kind, child1.getNode(),
                                           child2.getNode(), child3.getNode())));
@@ -105,12 +81,6 @@ Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2,
 
 Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2,
                          const Expr& child3, const Expr& child4) {
-  const unsigned n = 4;
-  CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
-                "Exprs with kind %s must have at least %u children and "
-                "at most %u children (the one under construction has %u)",
-                kind::kindToString(kind).c_str(),
-                minArity(kind), maxArity(kind), n);
   NodeManagerScope nms(d_nodeManager);
   return Expr(this, new Node(d_nodeManager->mkNode(kind, child1.getNode(),
                                           child2.getNode(), child3.getNode(),
@@ -120,12 +90,6 @@ Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2,
 Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2,
                          const Expr& child3, const Expr& child4,
                          const Expr& child5) {
-  const unsigned n = 5;
-  CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
-                "Exprs with kind %s must have at least %u children and "
-                "at most %u children (the one under construction has %u)",
-                kind::kindToString(kind).c_str(),
-                minArity(kind), maxArity(kind), n);
   NodeManagerScope nms(d_nodeManager);
   return Expr(this, new Node(d_nodeManager->mkNode(kind, child1.getNode(),
                                           child2.getNode(), child3.getNode(),
@@ -133,13 +97,6 @@ Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2,
 }
 
 Expr ExprManager::mkExpr(Kind kind, const vector<Expr>& children) {
-  const unsigned n = children.size();
-  CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
-                "Exprs with kind %s must have at least %u children and "
-                "at most %u children (the one under construction has %u)",
-                kind::kindToString(kind).c_str(),
-                minArity(kind), maxArity(kind), n);
-
   NodeManagerScope nms(d_nodeManager);
 
   vector<Node> nodes;
diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp
index 7c723d338..4d4061bd0 100644
--- a/src/expr/expr_template.cpp
+++ b/src/expr/expr_template.cpp
@@ -123,14 +123,13 @@ bool Expr::hasOperator() const {
 Expr Expr::getOperator() const {
   ExprManagerScope ems(*this);
   Assert(d_node != NULL, "Unexpected NULL expression pointer!");
-  CheckArgument(d_node->hasOperator(), *this,
+  CheckArgument(d_node->hasOperator(),
                 "Expr::getOperator() called on an Expr with no operator");
   return Expr(d_exprManager, new Node(d_node->getOperator()));
 }
 
 Type* Expr::getType() const {
   ExprManagerScope ems(*this);
-  Assert(d_node != NULL, "Unexpected NULL expression pointer!");
   return d_node->getType();
 }
 
@@ -179,69 +178,51 @@ BoolExpr::BoolExpr(const Expr& e) :
 }
 
 BoolExpr BoolExpr::notExpr() const {
-  Assert(d_exprManager != NULL,
-         "Don't have an expression manager for this expression!");
+  Assert(d_exprManager != NULL, "Don't have an expression manager for this expression!");
   return d_exprManager->mkExpr(NOT, *this);
 }
 
 BoolExpr BoolExpr::andExpr(const BoolExpr& e) const {
-  Assert(d_exprManager != NULL,
-         "Don't have an expression manager for this expression!");
-  CheckArgument(d_exprManager == e.d_exprManager, e,
-                "Different expression managers!");
+  Assert(d_exprManager != NULL, "Don't have an expression manager for this expression!");
+  Assert(d_exprManager == e.d_exprManager, "Different expression managers!");
   return d_exprManager->mkExpr(AND, *this, e);
 }
 
 BoolExpr BoolExpr::orExpr(const BoolExpr& e) const {
-  Assert(d_exprManager != NULL,
-         "Don't have an expression manager for this expression!");
-  CheckArgument(d_exprManager == e.d_exprManager, e,
-                "Different expression managers!");
+  Assert(d_exprManager != NULL, "Don't have an expression manager for this expression!");
+  Assert(d_exprManager == e.d_exprManager, "Different expression managers!");
   return d_exprManager->mkExpr(OR, *this, e);
 }
 
 BoolExpr BoolExpr::xorExpr(const BoolExpr& e) const {
-  Assert(d_exprManager != NULL,
-         "Don't have an expression manager for this expression!");
-  CheckArgument(d_exprManager == e.d_exprManager, e,
-                "Different expression managers!");
+  Assert(d_exprManager != NULL, "Don't have an expression manager for this expression!");
+  Assert(d_exprManager == e.d_exprManager, "Different expression managers!");
   return d_exprManager->mkExpr(XOR, *this, e);
 }
 
 BoolExpr BoolExpr::iffExpr(const BoolExpr& e) const {
-  Assert(d_exprManager != NULL,
-         "Don't have an expression manager for this expression!");
-  CheckArgument(d_exprManager == e.d_exprManager, e,
-                "Different expression managers!");
+  Assert(d_exprManager != NULL, "Don't have an expression manager for this expression!");
+  Assert(d_exprManager == e.d_exprManager, "Different expression managers!");
   return d_exprManager->mkExpr(IFF, *this, e);
 }
 
 BoolExpr BoolExpr::impExpr(const BoolExpr& e) const {
-  Assert(d_exprManager != NULL,
-         "Don't have an expression manager for this expression!");
-  CheckArgument(d_exprManager == e.d_exprManager, e,
-                "Different expression managers!");
+  Assert(d_exprManager != NULL, "Don't have an expression manager for this expression!");
+  Assert(d_exprManager == e.d_exprManager, "Different expression managers!");
   return d_exprManager->mkExpr(IMPLIES, *this, e);
 }
 
-BoolExpr BoolExpr::iteExpr(const BoolExpr& then_e,
-                           const BoolExpr& else_e) const {
-  Assert(d_exprManager != NULL,
-         "Don't have an expression manager for this expression!");
-  CheckArgument(d_exprManager == then_e.d_exprManager, then_e,
-                "Different expression managers!");
-  CheckArgument(d_exprManager == else_e.d_exprManager, else_e,
-                "Different expression managers!");
+BoolExpr BoolExpr::iteExpr(const BoolExpr& then_e, const BoolExpr& else_e) const {
+  Assert(d_exprManager != NULL, "Don't have an expression manager for this expression!");
+  Assert(d_exprManager == then_e.d_exprManager, "Different expression managers!");
+  Assert(d_exprManager == else_e.d_exprManager, "Different expression managers!");
   return d_exprManager->mkExpr(ITE, *this, then_e, else_e);
 }
 
 Expr BoolExpr::iteExpr(const Expr& then_e, const Expr& else_e) const {
-  Assert(d_exprManager != NULL,
-         "Don't have an expression manager for this expression!");
-  CheckArgument(d_exprManager == then_e.getExprManager(), then_e,
-                "Different expression managers!");
-  CheckArgument(d_exprManager == else_e.getExprManager(), else_e,
-                "Different expression managers!");
+  Assert(d_exprManager != NULL, "Don't have an expression manager for this expression!");
+  Assert(d_exprManager == then_e.getExprManager(), "Different expression managers!");
+  Assert(d_exprManager == else_e.getExprManager(), "Different expression managers!");
   return d_exprManager->mkExpr(ITE, *this, then_e, else_e);
 }
 
diff --git a/src/expr/mkexpr b/src/expr/mkexpr
index 6508f8121..de6de014d 100755
--- a/src/expr/mkexpr
+++ b/src/expr/mkexpr
@@ -129,9 +129,6 @@ $2 const & Expr::getConst< $2 >() const;
   getConst_implementations="${getConst_implementations}
 template <>
 $2 const & Expr::getConst() const {
-  // check even for production builds
-  CheckArgument(getKind() == ::CVC4::kind::$1, *this,
-                \"Improper kind for getConst<$2>()\");
   return d_node->getConst< $2 >();
 }
 "
diff --git a/src/expr/type.cpp b/src/expr/type.cpp
index 851c440b6..d94513bee 100644
--- a/src/expr/type.cpp
+++ b/src/expr/type.cpp
@@ -49,7 +49,8 @@ BooleanType::BooleanType() :
 BooleanType::~BooleanType() {
 }
 
-BooleanType* BooleanType::getInstance() {
+BooleanType*
+BooleanType::getInstance() {
   return &s_instance;
 }
 
@@ -116,7 +117,8 @@ bool KindType::isKind() const {
   return true;
 }
 
-KindType* KindType::getInstance() {
+KindType*
+KindType::getInstance() {
   return &s_instance;
 }
 
@@ -127,4 +129,4 @@ SortType::SortType(std::string name) :
 SortType::~SortType() {
 }
 
-}/* CVC4 namespace */
+}
diff --git a/src/expr/type.h b/src/expr/type.h
index 8a9d6cd70..9ab229024 100644
--- a/src/expr/type.h
+++ b/src/expr/type.h
@@ -10,7 +10,7 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.
  **
- ** Interface for expression types
+ ** Interface for expression types 
  **/
 
 #include "cvc4_public.h"
@@ -44,11 +44,11 @@ protected:
 
 public:
 
-  /** Comparison for equality */
-  //bool operator==(const Type& t) const;
+  /** Comparision for equality */
+  bool operator==(const Type& t) const;
 
   /** Comparison for disequality */
-  //bool operator!=(const Type& e) const;
+  bool operator!=(const Type& e) const;
 
   /** Get the name of this type. May be empty for composite types. */
   std::string getName() const;
@@ -59,7 +59,7 @@ public:
   }
 
   /** Is this a function type? */
-  virtual bool isFunction() const {
+  virtual bool isFunction() const { 
     return false;
   }
 
@@ -135,20 +135,17 @@ private:
   /** Create a type associated with nodeManager. */
   BooleanType();
 
-  /**
-   * Do-nothing private copy constructor operator, to prevent
-   * copy-construction.
-   */
-  BooleanType(const BooleanType&);
+  /** Do-nothing private copy constructor operator, to prevent
+      copy-construction. */
+  BooleanType(const BooleanType&); 
 
   /** Destructor */
   ~BooleanType();
 
-  /**
-   * Do-nothing private assignment operator, to prevent assignment.
-   */
+  /** Do-nothing private assignment operator, to prevent
+     assignment. */
   BooleanType& operator=(const BooleanType&);
-
+  
   /** The singleton instance */
   static BooleanType s_instance;
 };
@@ -165,7 +162,7 @@ public:
 
   /** Get the range type (i.e., the type of the result). */
   Type* getRangeType() const;
-
+  
   /** Is this as function type? (Returns true.) */
   bool isFunction() const;
 
@@ -173,17 +170,14 @@ public:
       boolean.) */
   bool isPredicate() const;
 
-  /**
-   * Outputs a string representation of this type to the stream,
-   * in the format "D -> R" or "(A, B, C) -> R".
-   */
+  /** Outputs a string representation of this type to the stream,
+      in the format "D -> R" or "(A, B, C) -> R". */
   void toStream(std::ostream& out) const;
 
 private:
 
-  /**
-   * Construct a function type associated with nodeManager, given a
-   * vector of argument types and the range type.
+  /** Construct a function type associated with nodeManager,
+   * given a vector of argument types and the range type.
 
    * @param argTypes a non-empty vector of input types
    * @param range the result type
@@ -193,7 +187,7 @@ private:
 
   /** Destructor */
   ~FunctionType();
-
+  
   /** The list of input types. */
   const std::vector<Type*> d_argTypes;
 
@@ -204,7 +198,7 @@ private:
 };
 
 
-/** Class encapsulating the kind type (the type of types).
+/** Class encapsulating the kind type (the type of types). 
 */
 class KindType : public Type {
 
@@ -219,21 +213,22 @@ private:
 
   KindType();
 
-  /* Do-nothing private copy constructor, to prevent copy
-     construction. */
-  KindType(const KindType&);
+  /* Do-nothing private copy constructor, to prevent
+     copy construction. */
+  KindType(const KindType&); 
 
   /** Destructor */
   ~KindType();
 
-  /* Do-nothing private assignment operator, to prevent assignment. */
+  /* Do-nothing private assignment operator, to prevent
+     assignment. */
   KindType& operator=(const KindType&);
 
   /** The singleton instance */
   static KindType s_instance;
 };
 
-/** Class encapsulating a user-defined sort.
+/** Class encapsulating a user-defined sort. 
     TODO: Should sort be uniquely named per-nodeManager and not conflict
     with any builtins? */
 class SortType : public Type {
diff --git a/src/theory/booleans/kinds b/src/theory/booleans/kinds
index bd85af69d..5fcf9299a 100644
--- a/src/theory/booleans/kinds
+++ b/src/theory/booleans/kinds
@@ -19,5 +19,5 @@ nonatomic_operator AND 2: "logical and"
 nonatomic_operator IFF 2 "logical equivalence"
 nonatomic_operator IMPLIES 2 "logical implication"
 nonatomic_operator OR 2: "logical or"
-nonatomic_operator XOR 2 "exclusive or"
+nonatomic_operator XOR 2: "exclusive or"
 nonatomic_operator ITE 3 "if-then-else"
diff --git a/test/unit/expr/expr_black.h b/test/unit/expr/expr_black.h
index e253b4a24..b08b5c6aa 100644
--- a/test/unit/expr/expr_black.h
+++ b/test/unit/expr/expr_black.h
@@ -362,7 +362,7 @@ public:
     TS_ASSERT(r2->isAtomic());
 
     Expr x = d_em->mkExpr(AND, *a, *b);
-    Expr y = d_em->mkExpr(ITE, *a, *b, *c);
+    Expr y = d_em->mkExpr(XOR, *a, *b, *c);
     Expr z = d_em->mkExpr(IFF, x, y);
 
     TS_ASSERT(!x.isAtomic());