resolve bug 32; public-facing interface functions in expr package must set current NodeManager

6 files changed, 44 insertions, 6 deletions

diff --git a/src/expr/expr.cpp b/src/expr/expr.cpp
index 032735ff0..18c0fdbab 100644
--- a/src/expr/expr.cpp
+++ b/src/expr/expr.cpp
@@ -43,11 +43,13 @@ ExprManager* Expr::getExprManager() const {
 }
 
 Expr::~Expr() {
+  ExprManagerScope ems(*this);
   delete d_node;
 }
 
 Expr& Expr::operator=(const Expr& e) {
   if(this != &e) {
+    ExprManagerScope ems(*this);
     delete d_node;
     d_node = new Node(*e.d_node);
     d_em = e.d_em;
@@ -79,7 +81,7 @@ bool Expr::operator<(const Expr& e) const {
 
 size_t Expr::hash() const {
   Assert(d_node != NULL, "Unexpected NULL expression pointer!");
-  return (d_node->isNull());
+  return (d_node->hash());
 }
 
 Kind Expr::getKind() const {
@@ -93,6 +95,7 @@ size_t Expr::getNumChildren() const {
 }
 
 std::string Expr::toString() const {
+  ExprManagerScope ems(*this);
   Assert(d_node != NULL, "Unexpected NULL expression pointer!");
   return d_node->toString();
 }
@@ -107,6 +110,7 @@ Expr::operator bool() const {
 }
 
 void Expr::toStream(std::ostream& out) const {
+  ExprManagerScope ems(*this);
   d_node->toStream(out);
 }
 
diff --git a/src/expr/expr.h b/src/expr/expr.h
index 0943c13e4..dd4d0e9d7 100644
--- a/src/expr/expr.h
+++ b/src/expr/expr.h
@@ -13,11 +13,13 @@
  ** Public-facing expression interface.
  **/
 
+// circular dependency: force expr_manager.h first
+#include "expr/expr_manager.h"
+
 #ifndef __CVC4__EXPR_H
 #define __CVC4__EXPR_H
 
 #include "cvc4_config.h"
-#include "expr/expr_manager.h"
 
 #include <string>
 #include <iostream>
diff --git a/src/expr/expr_manager.h b/src/expr/expr_manager.h
index 5bfef2aa7..edfc18c8d 100644
--- a/src/expr/expr_manager.h
+++ b/src/expr/expr_manager.h
@@ -18,6 +18,7 @@
 
 #include "cvc4_config.h"
 #include "expr/kind.h"
+#include "expr/node_manager.h"
 #include <vector>
 
 namespace CVC4 {
@@ -27,7 +28,6 @@ class Type;
 class BooleanType; 
 class FunctionType; 
 class KindType;
-class NodeManager;
 class SmtEngine;
 
 class CVC4_PUBLIC ExprManager {
@@ -118,8 +118,31 @@ private:
 
   /** SmtEngine will use all the internals, so it will grab the node manager */
   friend class SmtEngine;
+
+  /** ExprManagerScope reaches in to get the NodeManager */
+  friend class ExprManagerScope;
 };
 
-}
+}/* CVC4 namespace */
+
+#include "expr/expr.h"
+
+namespace CVC4 {
+
+/**
+ * A wrapper (essentially) for NodeManagerScope.  Without this, we'd
+ * need Expr to be a friend of ExprManager.
+ */
+class ExprManagerScope {
+  NodeManagerScope d_nms;
+public:
+  inline ExprManagerScope(const Expr& e) :
+    d_nms(e.getExprManager() == NULL ?
+          NodeManager::currentNM() : e.getExprManager()->getNodeManager()) {
+  }
+};
+
+}/* CVC4 namespace */
 
 #endif /* __CVC4__EXPR_MANAGER_H */
+
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 2862203db..18a95f041 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -13,6 +13,9 @@
  ** A manager for Nodes.
  **/
 
+/* circular dependency; force node.h first */
+#include "expr/node.h"
+
 #ifndef __CVC4__NODE_MANAGER_H
 #define __CVC4__NODE_MANAGER_H
 
@@ -20,7 +23,6 @@
 #include <string>
 #include <ext/hash_set>
 
-#include "expr/node.h"
 #include "expr/kind.h"
 
 namespace __gnu_cxx {
diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index 5ec24400d..421f94418 100644
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -1,7 +1,8 @@
 SUBDIRS = precedence
 
 TESTS_ENVIRONMENT = @srcdir@/../run_regression @top_builddir@/../../bin/cvc4
-TESTS =	hole6.cvc \
+TESTS =	bug32.cvc \
+	hole6.cvc \
 	logops.01.cvc \
 	logops.02.cvc \
 	logops.03.cvc \
diff --git a/test/regress/regress0/bug32.cvc b/test/regress/regress0/bug32.cvc
new file mode 100644
index 000000000..8d113d785
--- /dev/null
+++ b/test/regress/regress0/bug32.cvc
@@ -0,0 +1,6 @@
+% EXPECT: VALID
+a:BOOLEAN;
+b:BOOLEAN;
+ASSERT(a);
+QUERY(a OR b);
+