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

diff --git a/src/expr/expr.cpp b/src/expr/expr.cpp
index 032735ff0eeb2e4d3a0624766c89df2c397faed0..18c0fdbab850f2176bf06cdc273a73f906effe40 100644 (file)
--- 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 0943c13e4261fbab14aef97b2616db2122992879..dd4d0e9d73a138d060b27ffdc7599d4fd97d2ab6 100644 (file)
--- 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 5bfef2aa74c63187fde5cb7db6a5d0d26493117b..edfc18c8d793fc6687d96547e38a44e38267abc3 100644 (file)
--- 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 2862203db8fa90e0cad0a33fdc78a53cfef2e167..18a95f041d9f893a01e9bcc83f7ed44eccbcbffe 100644 (file)
--- 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 5ec24400d6842fa0d4708c9126dd7969efc8d772..421f9441854fd0990dee9bb153ccca4123fea173 100644 (file)
--- 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 (file)
index 0000000..8d113d7
--- /dev/null
+++ b/test/regress/regress0/bug32.cvc
@@ -0,0 +1,6 @@
+% EXPECT: VALID
+a:BOOLEAN;
+b:BOOLEAN;
+ASSERT(a);
+QUERY(a OR b);
+