Recommit revision 365 (undoing revision 375, which reverted revision 365).

Fix the case in NodeBuilderBlack that triggered bug #82.  (Fixes bug #82.)

This also fixes regression failures from this morning (2010 Apr 4), in
the optimized builds, for which a fix was included in 365 and reverted
in 375.  They looked like this:

  In ExprBlack::testGetConst:
  /usr/local/share/cvc4/src/cvc4-2010-04-04/builds/x86_64-unknown-linux-gnu/production/../../../test/unit/expr/expr_black.h:377: Error: Expected (a->getConst<Kind>()) to throw (IllegalArgumentException) but it didn't throw
  /usr/local/share/cvc4/src/cvc4-2010-04-04/builds/x86_64-unknown-linux-gnu/production/../../../test/unit/expr/expr_black.h:378: Error: Expected (b->getConst<Kind>()) to throw (IllegalArgumentException) but it didn't throw
  [etc..]

diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index fa1a1a6af17832956039737d9d6674cb696425b4..6a2640080f4867660290809e550b52dd05c8fa9f 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;

diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp
index 4d4061bd08e10c4e3640c18c0afe26ae21904550..7c723d338e6bba42035f68338fe7bc8aaa750788 100644 (file)
--- a/src/expr/expr_template.cpp
+++ b/src/expr/expr_template.cpp
@@ -123,13 +123,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();
 }
 
@@ -178,51 +179,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 d94513bee64190f9a96f611ea79ba75e76dc5b61..851c440b6217721c0ea4bf6aad4ecd16666350ba 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 9ab229024804b2c2ac2ca50d0f1648d91f14af2e..8a9d6cd704cc0234907c9b8f95f87577f8afb742 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());

diff --git a/test/unit/expr/node_builder_black.h b/test/unit/expr/node_builder_black.h
index 2af5988a617253e8ea26a5919cd4a6d87c257919..81aa424f8a6a4a71f461aac34b196d43ac653130 100644 (file)
--- a/test/unit/expr/node_builder_black.h
+++ b/test/unit/expr/node_builder_black.h
@@ -465,7 +465,7 @@ public:
     Node z = d_nm->mkVar();
     Node m = d_nm->mkNode(AND, y, z, x);
     Node n = d_nm->mkNode(OR, d_nm->mkNode(NOT, x), y, z);
-    Node o = d_nm->mkNode(XOR, y, x, z);
+    Node o = d_nm->mkNode(XOR, y, x);
     Node p = d_nm->mkNode(PLUS, z, d_nm->mkNode(UMINUS, x), z);
     Node q = d_nm->mkNode(AND, x, z, d_nm->mkNode(NOT, y));