* 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.

1 files changed, 38 insertions, 19 deletions

diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp
index d02272320..2e901dc92 100644
--- 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);
 }