Hack to support global variables for CVC language extended to export mechanism.

- Adds GlobalVarAttr node attribute

(this commit was certified error- and warning-free by the test-and-commit script.)

diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp
index ed643b830736e4512bfe1009777f62ffaa219e5c..a3204f00f7d56515e694f9a1e9f54eecdbf75cee 100644 (file)
--- a/src/expr/expr_template.cpp
+++ b/src/expr/expr_template.cpp
@@ -138,12 +138,15 @@ Node exportInternal(TNode n, ExprManager* from, ExprManager* to, ExprManagerMapC
       if(Node::fromExpr(from_e).getAttribute(VarNameAttr(), name)) {
         // temporarily set the node manager to NULL; this gets around
         // a check that mkVar isn't called internally
-        NodeManagerScope nullScope(NULL);
 
         if(n.getKind() == kind::BOUND_VAR_LIST || n.getKind() == kind::BOUND_VARIABLE) {
+          NodeManagerScope nullScope(NULL);
           to_e = to->mkBoundVar(name, type);// FIXME thread safety
         } else if(n.getKind() == kind::VARIABLE) {
-          to_e = to->mkVar(name, type);// FIXME thread safety
+          bool isGlobal;
+          Node::fromExpr(from_e).getAttribute(GlobalVarAttr(), isGlobal);
+          NodeManagerScope nullScope(NULL);
+          to_e = to->mkVar(name, type, isGlobal);// FIXME thread safety
         } else if(n.getKind() == kind::SKOLEM) {
           // skolems are only available at the Node level (not the Expr level)
           TypeNode typeNode = TypeNode::fromType(type);

diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 5cf591f9de2cc96541e6758542fc4320c37a44b9..2cda23f2d4985258eb32764bb7e97d44a16b0f3c 100644 (file)
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -52,12 +52,14 @@ class TypeChecker;
 // TODO: hide this attribute behind a NodeManager interface.
 namespace attr {
   struct VarNameTag { };
+  struct GlobalVarTag { };
   struct SortArityTag { };
   struct DatatypeTupleTag { };
   struct DatatypeRecordTag { };
 }/* CVC4::expr::attr namespace */
 
 typedef Attribute<attr::VarNameTag, std::string> VarNameAttr;
+typedef Attribute<attr::GlobalVarTag(), bool> GlobalVarAttr;
 typedef Attribute<attr::SortArityTag, uint64_t> SortArityAttr;
 /** Attribute true for datatype types that are replacements for tuple types */
 typedef expr::Attribute<expr::attr::DatatypeTupleTag, TypeNode> DatatypeTupleAttr;
@@ -1479,6 +1481,7 @@ inline Node NodeManager::mkVar(const std::string& name, const TypeNode& type, bo
   setAttribute(n, TypeAttr(), type);
   setAttribute(n, TypeCheckedAttr(), true);
   setAttribute(n, expr::VarNameAttr(), name);
+  setAttribute(n, expr::GlobalVarAttr(), isGlobal);
   for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) {
     (*i)->nmNotifyNewVar(n, isGlobal);
   }
@@ -1491,6 +1494,7 @@ inline Node* NodeManager::mkVarPtr(const std::string& name,
   setAttribute(*n, TypeAttr(), type);
   setAttribute(*n, TypeCheckedAttr(), true);
   setAttribute(*n, expr::VarNameAttr(), name);
+  setAttribute(*n, expr::GlobalVarAttr(), isGlobal);
   for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) {
     (*i)->nmNotifyNewVar(*n, isGlobal);
   }
@@ -1514,6 +1518,7 @@ inline Node NodeManager::mkVar(const TypeNode& type, bool isGlobal) {
   Node n = NodeBuilder<0>(this, kind::VARIABLE);
   setAttribute(n, TypeAttr(), type);
   setAttribute(n, TypeCheckedAttr(), true);
+  setAttribute(n, expr::GlobalVarAttr(), isGlobal);
   for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) {
     (*i)->nmNotifyNewVar(n, isGlobal);
   }
@@ -1524,6 +1529,7 @@ inline Node* NodeManager::mkVarPtr(const TypeNode& type, bool isGlobal) {
   Node* n = NodeBuilder<0>(this, kind::VARIABLE).constructNodePtr();
   setAttribute(*n, TypeAttr(), type);
   setAttribute(*n, TypeCheckedAttr(), true);
+  setAttribute(*n, expr::GlobalVarAttr(), isGlobal);
   for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) {
     (*i)->nmNotifyNewVar(*n, isGlobal);
   }