From b63e4a11733051728397f7d4ecb3b205fbd81dab Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@gmail.com>
Date: Thu, 7 Oct 2010 22:54:43 +0000
Subject: type checking for define-fun in production builds; related to (and
 might resolve) bug 212

---
 src/expr/expr_template.h |  2 ++
 src/expr/node.h          |  2 +-
 src/expr/node_manager.h  | 14 +++++---------
 3 files changed, 8 insertions(+), 10 deletions(-)

(limited to 'src/expr')

diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h
index bb227f92f..29164ffa5 100644
--- a/src/expr/expr_template.h
+++ b/src/expr/expr_template.h
@@ -60,6 +60,8 @@ namespace expr {
  */
 class CVC4_PUBLIC TypeCheckingException : public Exception {
 
+  friend class SmtEngine;
+
 private:
 
   /** The expression responsible for the error */
diff --git a/src/expr/node.h b/src/expr/node.h
index bd6b53522..871f1e0d7 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -53,7 +53,7 @@ class TypeCheckingExceptionPrivate : public Exception {
 
 private:
 
-  /** The node repsonsible for the failure */
+  /** The node responsible for the failure */
   NodeTemplate<true>* d_node;
 
 protected:
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index c0f489d7a..0860365bc 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -789,15 +789,11 @@ inline TypeNode NodeManager::mkSort(TypeNode constructor,
          constructor.getNumChildren() == 0,
          "expected a sort constructor");
   Assert(children.size() > 0, "expected non-zero # of children");
-  uint64_t arity;
-  std::string name;
-  bool hasArityAttribute =
-    getAttribute(constructor.d_nv, expr::SortArityAttr(), arity);
-  Assert(hasArityAttribute, "expected a sort constructor");
-  bool hasNameAttribute =
-    getAttribute(constructor.d_nv, expr::VarNameAttr(), name);
-  Assert(hasNameAttribute, "expected a sort constructor");
-  Assert(arity == children.size(),
+  Assert( hasAttribute(constructor.d_nv, expr::SortArityAttr()) &&
+          hasAttribute(constructor.d_nv, expr::VarNameAttr()),
+          "expected a sort constructor" );
+  std::string name = getAttribute(constructor.d_nv, expr::VarNameAttr());
+  Assert(getAttribute(constructor.d_nv, expr::SortArityAttr()) == children.size(),
          "arity mismatch in application of sort constructor");
   NodeBuilder<> nb(this, kind::SORT_TYPE);
   Node sortTag = Node(constructor.d_nv->d_children[0]);
-- 
cgit v1.2.3