* Minor code formatting stuff in src/expr/type.{h,cpp}. Concluded

  Type code review and closed bug #25.

* Do assertions on Expr creation (public library interface) even when
  assertions are off.  Also a similar check for proper kind (in public
  interface) when Expr::getConst<>() is called.  This fixes a unit
  test that was failing in production builds (an exception wasn't
  thrown but should have been).

* kind::XOR must have exactly 2 arguments, not 2-or-more.

diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 2e25b4574c4f79a24a7f87e8d7ec0ab008e0b920..a2c90937b602efff367e85a1a5f2c99caff8123a 100644 (file)
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -57,16 +57,34 @@ 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())));
@@ -74,6 +92,12 @@ 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())));
@@ -81,6 +105,12 @@ 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(),
@@ -90,6 +120,12 @@ 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(),
@@ -97,6 +133,13 @@ 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;
@@ -171,6 +214,7 @@ unsigned ExprManager::minArity(Kind kind) {
   case IFF:
   case IMPLIES:
   case PLUS:
+  case MULT:
   case XOR:
     return 2;
 
@@ -207,6 +251,7 @@ unsigned ExprManager::maxArity(Kind kind) {
   case APPLY_UF:
   case DISTINCT:
   case PLUS:
+  case MULT:
   case OR:
     return UINT_MAX;
 

diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp
index d02272320e275cadd83ca4846c04e48e40e8c87b..2e901dc920acfe29819e0c4d7e9565ebc20c1207 100644 (file)
--- a/src/expr/expr_template.cpp
+++ b/src/expr/expr_template.cpp
@@ -134,13 +134,14 @@ bool Expr::hasOperator() const {
 Expr Expr::getOperator() const {
   ExprManagerScope ems(*this);
   Assert(d_node != NULL, "Unexpected NULL expression pointer!");
-  CheckArgument(d_node->hasOperator(),
+  CheckArgument(d_node->hasOperator(), *this,
                 "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();
 }
 
@@ -189,51 +190,69 @@ 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!");
-  Assert(d_exprManager == e.d_exprManager, "Different expression managers!");
+  Assert(d_exprManager != NULL,
+         "Don't have an expression manager for this expression!");
+  CheckArgument(d_exprManager == e.d_exprManager, e,
+                "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!");
-  Assert(d_exprManager == e.d_exprManager, "Different expression managers!");
+  Assert(d_exprManager != NULL,
+         "Don't have an expression manager for this expression!");
+  CheckArgument(d_exprManager == e.d_exprManager, e,
+                "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!");
-  Assert(d_exprManager == e.d_exprManager, "Different expression managers!");
+  Assert(d_exprManager != NULL,
+         "Don't have an expression manager for this expression!");
+  CheckArgument(d_exprManager == e.d_exprManager, e,
+                "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!");
-  Assert(d_exprManager == e.d_exprManager, "Different expression managers!");
+  Assert(d_exprManager != NULL,
+         "Don't have an expression manager for this expression!");
+  CheckArgument(d_exprManager == e.d_exprManager, e,
+                "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!");
-  Assert(d_exprManager == e.d_exprManager, "Different expression managers!");
+  Assert(d_exprManager != NULL,
+         "Don't have an expression manager for this expression!");
+  CheckArgument(d_exprManager == e.d_exprManager, e,
+                "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!");
-  Assert(d_exprManager == then_e.d_exprManager, "Different expression managers!");
-  Assert(d_exprManager == else_e.d_exprManager, "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!");
+  CheckArgument(d_exprManager == then_e.d_exprManager, then_e,
+                "Different expression managers!");
+  CheckArgument(d_exprManager == else_e.d_exprManager, else_e,
+                "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!");
-  Assert(d_exprManager == then_e.getExprManager(), "Different expression managers!");
-  Assert(d_exprManager == else_e.getExprManager(), "Different expression managers!");
+  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!");
   return d_exprManager->mkExpr(ITE, *this, then_e, else_e);
 }
 

diff --git a/src/expr/mkexpr b/src/expr/mkexpr
index de6de014d8d83bc4ba88ca5e9a895bfc94b88f28..6508f81218f84f20fb465654d80af033b5bc2d16 100755 (executable)
--- a/src/expr/mkexpr
+++ b/src/expr/mkexpr
@@ -129,6 +129,9 @@ $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 2fa21c8a60f73a565f1385d799f80eabbd2a796d..569becab1597e115d30a8dd77566feec740b5be0 100644 (file)
--- a/src/expr/type.cpp
+++ b/src/expr/type.cpp
@@ -49,8 +49,7 @@ BooleanType::BooleanType() :
 BooleanType::~BooleanType() {
 }
 
-BooleanType*
-BooleanType::getInstance() {
+BooleanType* BooleanType::getInstance() {
   return &s_instance;
 }
 
@@ -117,8 +116,7 @@ bool KindType::isKind() const {
   return true;
 }
 
-KindType*
-KindType::getInstance() {
+KindType* KindType::getInstance() {
   return &s_instance;
 }
 
@@ -129,4 +127,4 @@ SortType::SortType(std::string name) :
 SortType::~SortType() {
 }
 
-}
+}/* CVC4 namespace */

diff --git a/src/expr/type.h b/src/expr/type.h
index 9e6596e84497f14e234a28ef1163a13e28cd0c8c..767ea122e3c3188d2ca724b7382d1a24a2e459a4 100644 (file)
--- 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:
 
-  /** Comparision for equality */
-  bool operator==(const Type& t) const;
+  /** Comparison 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,17 +135,20 @@ 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;
 };
@@ -162,7 +165,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;
 
@@ -170,14 +173,17 @@ 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
@@ -187,7 +193,7 @@ private:
 
   /** Destructor */
   ~FunctionType();
-  
+
   /** The list of input types. */
   const std::vector<Type*> d_argTypes;
 
@@ -198,7 +204,7 @@ private:
 };
 
 
-/** Class encapsulating the kind type (the type of types). 
+/** Class encapsulating the kind type (the type of types).
 */
 class KindType : public Type {
 
@@ -213,22 +219,21 @@ 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 5fcf9299a44b3097e90237bfd21dd19a0338dba3..bd85af69d06aaf1eaf3d1efcc85c3fb985f72af1 100644 (file)
--- 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 b08b5c6aae557785d7b14c6e2fa23fe8538c6ad1..e253b4a24ba7474778d4d19fcccee50a637fd61d 100644 (file)
--- 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(XOR, *a, *b, *c);
+    Expr y = d_em->mkExpr(ITE, *a, *b, *c);
     Expr z = d_em->mkExpr(IFF, x, y);
 
     TS_ASSERT(!x.isAtomic());