Switching to types-as-attributes in parser

diff --git a/src/expr/expr.cpp b/src/expr/expr.cpp
index c29b7e448657cff6e097c0f1329b513e3cb80e19..7dc8c8f9649e08bcdf31d2720ddbe83be172462a 100644 (file)
--- a/src/expr/expr.cpp
+++ b/src/expr/expr.cpp
@@ -27,19 +27,19 @@ std::ostream& operator<<(std::ostream& out, const Expr& e) {
 }
 
 Expr::Expr() :
-  d_node(new Node()), d_em(NULL) {
+  d_node(new Node()), d_exprManager(NULL) {
 }
 
 Expr::Expr(ExprManager* em, Node* node) :
-  d_node(node), d_em(em) {
+  d_node(node), d_exprManager(em) {
 }
 
 Expr::Expr(const Expr& e) :
-  d_node(new Node(*e.d_node)), d_em(e.d_em) {
+  d_node(new Node(*e.d_node)), d_exprManager(e.d_exprManager) {
 }
 
 ExprManager* Expr::getExprManager() const {
-  return d_em;
+  return d_exprManager;
 }
 
 Expr::~Expr() {
@@ -52,13 +52,13 @@ Expr& Expr::operator=(const Expr& e) {
     ExprManagerScope ems(*this);
     delete d_node;
     d_node = new Node(*e.d_node);
-    d_em = e.d_em;
+    d_exprManager = e.d_exprManager;
   }
   return *this;
 }
 
 bool Expr::operator==(const Expr& e) const {
-  if(d_em != e.d_em){
+  if(d_exprManager != e.d_exprManager){
     return false;
   }
   Assert(d_node != NULL, "Unexpected NULL expression pointer!");
@@ -73,7 +73,7 @@ bool Expr::operator!=(const Expr& e) const {
 bool Expr::operator<(const Expr& e) const {
   Assert(d_node != NULL, "Unexpected NULL expression pointer!");
   Assert(e.d_node != NULL, "Unexpected NULL expression pointer!");
-  if(d_em != e.d_em){
+  if(d_exprManager != e.d_exprManager){
     return false;
   }
   return *d_node < *e.d_node;
@@ -94,6 +94,11 @@ size_t Expr::getNumChildren() const {
   return d_node->getNumChildren();
 }
 
+const Type* Expr::getType() const {
+  ExprManagerScope ems(*this);
+  return d_node->getType();
+}
+
 std::string Expr::toString() const {
   ExprManagerScope ems(*this);
   Assert(d_node != NULL, "Unexpected NULL expression pointer!");
@@ -126,52 +131,52 @@ BoolExpr::BoolExpr(const Expr& e) :
 }
 
 BoolExpr BoolExpr::notExpr() const {
-  Assert(d_em != NULL, "Don't have an expression manager for this expression!");
-  return d_em->mkExpr(NOT, *this);
+  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_em != NULL, "Don't have an expression manager for this expression!");
-  Assert(d_em == e.d_em, "Different expression managers!");
-  return d_em->mkExpr(AND, *this, e);
+  Assert(d_exprManager != NULL, "Don't have an expression manager for this expression!");
+  Assert(d_exprManager == e.d_exprManager, "Different expression managers!");
+  return d_exprManager->mkExpr(AND, *this, e);
 }
 
 BoolExpr BoolExpr::orExpr(const BoolExpr& e) const {
-  Assert(d_em != NULL, "Don't have an expression manager for this expression!");
-  Assert(d_em == e.d_em, "Different expression managers!");
-  return d_em->mkExpr(OR, *this, e);
+  Assert(d_exprManager != NULL, "Don't have an expression manager for this expression!");
+  Assert(d_exprManager == e.d_exprManager, "Different expression managers!");
+  return d_exprManager->mkExpr(OR, *this, e);
 }
 
 BoolExpr BoolExpr::xorExpr(const BoolExpr& e) const {
-  Assert(d_em != NULL, "Don't have an expression manager for this expression!");
-  Assert(d_em == e.d_em, "Different expression managers!");
-  return d_em->mkExpr(XOR, *this, e);
+  Assert(d_exprManager != NULL, "Don't have an expression manager for this expression!");
+  Assert(d_exprManager == e.d_exprManager, "Different expression managers!");
+  return d_exprManager->mkExpr(XOR, *this, e);
 }
 
 BoolExpr BoolExpr::iffExpr(const BoolExpr& e) const {
-  Assert(d_em != NULL, "Don't have an expression manager for this expression!");
-  Assert(d_em == e.d_em, "Different expression managers!");
-  return d_em->mkExpr(IFF, *this, e);
+  Assert(d_exprManager != NULL, "Don't have an expression manager for this expression!");
+  Assert(d_exprManager == e.d_exprManager, "Different expression managers!");
+  return d_exprManager->mkExpr(IFF, *this, e);
 }
 
 BoolExpr BoolExpr::impExpr(const BoolExpr& e) const {
-  Assert(d_em != NULL, "Don't have an expression manager for this expression!");
-  Assert(d_em == e.d_em, "Different expression managers!");
-  return d_em->mkExpr(IMPLIES, *this, e);
+  Assert(d_exprManager != NULL, "Don't have an expression manager for this expression!");
+  Assert(d_exprManager == e.d_exprManager, "Different expression managers!");
+  return d_exprManager->mkExpr(IMPLIES, *this, e);
 }
 
 BoolExpr BoolExpr::iteExpr(const BoolExpr& then_e, const BoolExpr& else_e) const {
-  Assert(d_em != NULL, "Don't have an expression manager for this expression!");
-  Assert(d_em == then_e.d_em, "Different expression managers!");
-  Assert(d_em == else_e.d_em, "Different expression managers!");
-  return d_em->mkExpr(ITE, *this, then_e, else_e);
+  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!");
+  return d_exprManager->mkExpr(ITE, *this, then_e, else_e);
 }
 
 Expr BoolExpr::iteExpr(const Expr& then_e, const Expr& else_e) const {
-  Assert(d_em != NULL, "Don't have an expression manager for this expression!");
-  Assert(d_em == then_e.getExprManager(), "Different expression managers!");
-  Assert(d_em == else_e.getExprManager(), "Different expression managers!");
-  return d_em->mkExpr(ITE, *this, then_e, else_e);
+  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!");
+  return d_exprManager->mkExpr(ITE, *this, then_e, else_e);
 }
 
 void Expr::printAst(std::ostream & o, int indent) const{

diff --git a/src/expr/expr.h b/src/expr/expr.h
index 096094aff56906afd9c3c3e563482bbbc3728d3a..27b7846db33d6b4a3fae806c181071d6d708eb50 100644 (file)
--- a/src/expr/expr.h
+++ b/src/expr/expr.h
@@ -108,6 +108,11 @@ public:
    */
   size_t getNumChildren() const;
 
+  /** Returns the type of the expression, if it has been computed.
+   * Returns NULL if the type of the expression is not known.
+   */
+  const Type* getType() const;
+
   /**
    * Returns the string representation of the expression.
    * @return a string representation of the expression
@@ -162,7 +167,7 @@ protected:
   Node* d_node;
 
   /** The responsible expression manager */
-  ExprManager* d_em;
+  ExprManager* d_exprManager;
 
   /**
    * Returns the actual internal node.

diff --git a/src/expr/expr_manager.cpp b/src/expr/expr_manager.cpp
index 71368c101d8841c0c196e11090e9f27b9e478a32..6231d5a8abeb4dbe95471c210ad5c42a5d414524 100644 (file)
--- a/src/expr/expr_manager.cpp
+++ b/src/expr/expr_manager.cpp
@@ -31,50 +31,50 @@ using namespace std;
 namespace CVC4 {
 
 ExprManager::ExprManager() :
-  d_nm(new NodeManager()) {
+  d_nodeManager(new NodeManager()) {
 }
 
 ExprManager::~ExprManager() {
-  delete d_nm;
+  delete d_nodeManager;
 }
 
 const BooleanType* ExprManager::booleanType() {
-  NodeManagerScope nms(d_nm);
+  NodeManagerScope nms(d_nodeManager);
   return BooleanType::getInstance();
 }
 
 const KindType* ExprManager::kindType() {
-  NodeManagerScope nms(d_nm);
+  NodeManagerScope nms(d_nodeManager);
   return KindType::getInstance();
 }
 
 Expr ExprManager::mkExpr(Kind kind) {
-  NodeManagerScope nms(d_nm);
-  return Expr(this, new Node(d_nm->mkNode(kind)));
+  NodeManagerScope nms(d_nodeManager);
+  return Expr(this, new Node(d_nodeManager->mkNode(kind)));
 }
 
 Expr ExprManager::mkExpr(Kind kind, const Expr& child1) {
-  NodeManagerScope nms(d_nm);
-  return Expr(this, new Node(d_nm->mkNode(kind, child1.getNode())));
+  NodeManagerScope nms(d_nodeManager);
+  return Expr(this, new Node(d_nodeManager->mkNode(kind, child1.getNode())));
 }
 
 Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2) {
-  NodeManagerScope nms(d_nm);
-  return Expr(this, new Node(d_nm->mkNode(kind, child1.getNode(),
+  NodeManagerScope nms(d_nodeManager);
+  return Expr(this, new Node(d_nodeManager->mkNode(kind, child1.getNode(),
                                           child2.getNode())));
 }
 
 Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2,
                          const Expr& child3) {
-  NodeManagerScope nms(d_nm);
-  return Expr(this, new Node(d_nm->mkNode(kind, child1.getNode(),
+  NodeManagerScope nms(d_nodeManager);
+  return Expr(this, new Node(d_nodeManager->mkNode(kind, child1.getNode(),
                                           child2.getNode(), child3.getNode())));
 }
 
 Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2,
                          const Expr& child3, const Expr& child4) {
-  NodeManagerScope nms(d_nm);
-  return Expr(this, new Node(d_nm->mkNode(kind, child1.getNode(),
+  NodeManagerScope nms(d_nodeManager);
+  return Expr(this, new Node(d_nodeManager->mkNode(kind, child1.getNode(),
                                           child2.getNode(), child3.getNode(),
                                           child4.getNode())));
 }
@@ -82,14 +82,14 @@ Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2,
 Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2,
                          const Expr& child3, const Expr& child4,
                          const Expr& child5) {
-  NodeManagerScope nms(d_nm);
-  return Expr(this, new Node(d_nm->mkNode(kind, child1.getNode(),
+  NodeManagerScope nms(d_nodeManager);
+  return Expr(this, new Node(d_nodeManager->mkNode(kind, child1.getNode(),
                                           child2.getNode(), child3.getNode(),
                                           child5.getNode())));
 }
 
 Expr ExprManager::mkExpr(Kind kind, const vector<Expr>& children) {
-  NodeManagerScope nms(d_nm);
+  NodeManagerScope nms(d_nodeManager);
 
   vector<Node> nodes;
   vector<Expr>::const_iterator it = children.begin();
@@ -98,14 +98,14 @@ Expr ExprManager::mkExpr(Kind kind, const vector<Expr>& children) {
     nodes.push_back(it->getNode());
     ++it;
   }
-  return Expr(this, new Node(d_nm->mkNode(kind, nodes)));
+  return Expr(this, new Node(d_nodeManager->mkNode(kind, nodes)));
 }
 
 /** Make a function type from domain to range. */
 const FunctionType* 
 ExprManager::mkFunctionType(const Type* domain, 
                             const Type* range) {
-  NodeManagerScope nms(d_nm);
+  NodeManagerScope nms(d_nodeManager);
   return FunctionType::getInstance(this, domain, range);
 }
 
@@ -113,28 +113,28 @@ ExprManager::mkFunctionType(const Type* domain,
 const FunctionType* 
 ExprManager::mkFunctionType(const std::vector<const Type*>& argTypes, 
                             const Type* range) {
-  NodeManagerScope nms(d_nm);
+  NodeManagerScope nms(d_nodeManager);
   return FunctionType::getInstance(this, argTypes, range);
 }
 
 const Type* ExprManager::mkSort(std::string name) {
   // FIXME: Sorts should be unique per-ExprManager
-  NodeManagerScope nms(d_nm);
+  NodeManagerScope nms(d_nodeManager);
   return new SortType(this, name);
 }
 
 Expr ExprManager::mkVar(const Type* type, string name) {
-  NodeManagerScope nms(d_nm);
-  return Expr(this, new Node(d_nm->mkVar(type, name)));
+  NodeManagerScope nms(d_nodeManager);
+  return Expr(this, new Node(d_nodeManager->mkVar(type, name)));
 }
 
 Expr ExprManager::mkVar(const Type* type) {
-  NodeManagerScope nms(d_nm);
-  return Expr(this, new Node(d_nm->mkVar(type)));
+  NodeManagerScope nms(d_nodeManager);
+  return Expr(this, new Node(d_nodeManager->mkVar(type)));
 }
 
 NodeManager* ExprManager::getNodeManager() const {
-  return d_nm;
+  return d_nodeManager;
 }
 
 } // End namespace CVC4

diff --git a/src/expr/expr_manager.h b/src/expr/expr_manager.h
index d84cf76be325632dd8ea917336659419ee10c027..4b00c27fc5084206cffbfcdbf9e5cd46da4698d4 100644 (file)
--- a/src/expr/expr_manager.h
+++ b/src/expr/expr_manager.h
@@ -108,7 +108,7 @@ public:
 
 private:
   /** The internal node manager */
-  NodeManager* d_nm;
+  NodeManager* d_nodeManager;
   
   /**
    * Returns the internal node manager. This should only be used by internal

diff --git a/src/expr/node.cpp b/src/expr/node.cpp
index 90dd867129dc23ee8ead5d732d1cf76200f6cfaa..080623e21e63c7a04342f9e89e3893ea4c50d6df 100644 (file)
--- a/src/expr/node.cpp
+++ b/src/expr/node.cpp
@@ -160,6 +160,13 @@ Node Node::xorExpr(const Node& right) const {
   return NodeManager::currentNM()->mkNode(XOR, *this, right);
 }
 
+const Type* Node::getType() const {
+  Assert( NodeManager::currentNM() != NULL,
+          "There is no current CVC4::NodeManager associated to this thread.\n"
+          "Perhaps a public-facing function is missing a NodeManagerScope ?" );
+  return NodeManager::currentNM()->getType(*this);
+}
+
 static void indent(ostream & o, int indent) {
   for(int i=0; i < indent; i++) {
     o << ' ';

diff --git a/src/expr/node.h b/src/expr/node.h
index 517a9eb7fddc6a920dd082283c76d95b2828e7fc..77f9141f1ac91bb7593a26dc5ed1093382fb2ade 100644 (file)
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -35,6 +35,7 @@ class Node;
 inline std::ostream& operator<<(std::ostream&, const Node&);
 
 class NodeManager;
+class Type;
 
 namespace expr {
   class NodeValue;
@@ -139,6 +140,7 @@ public:
   inline Kind getKind() const;
 
   inline size_t getNumChildren() const;
+  const Type* getType() const;
 
   static Node null();
 

diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index c6aee3dea0681f5a6e98a11a3e0506d8649ad3a6..ae6bdbd299ddc4dbb6bcd63db6e9c99b935da3ee 100644 (file)
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -73,8 +73,7 @@ Node NodeManager::mkNode(Kind kind, const vector<Node>& children) {
 }
 
 Node NodeManager::mkVar(const Type* type, string name) {
-  Node n = NodeBuilder<>(this, VARIABLE);
-  n.setAttribute(TypeAttr(), type);
+  Node n = mkVar(type);
   n.setAttribute(VarNameAttr(), name);
   return n;
 }

diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index d6d54bd5d65637f3dde4f161017abfe864d70a7f..29c738c10ace12da0c19d5f871ec01b4405627c3 100644 (file)
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -14,6 +14,7 @@
  **/
 
 /* circular dependency; force node.h first */
+#include "expr/attribute.h"
 #include "expr/node.h"
 
 #ifndef __CVC4__NODE_MANAGER_H
@@ -47,7 +48,7 @@ class NodeManager {
   typedef __gnu_cxx::hash_set<NodeValue*, __gnu_cxx::hash<NodeValue*>, NodeValue::NodeValueEq> NodeValueSet;
   NodeValueSet d_nodeValueSet;
 
-  expr::AttributeManager d_am;
+  expr::AttributeManager d_attrManager;
 
   NodeValue* poolLookup(NodeValue* nv) const;
   void poolInsert(NodeValue* nv);
@@ -56,7 +57,7 @@ class NodeManager {
 
 public:
 
-  NodeManager() : d_am(this) {
+  NodeManager() : d_attrManager(this) {
     poolInsert( &NodeValue::s_null );
   }
 
@@ -90,6 +91,8 @@ public:
   inline void setAttribute(const Node& n,
                            const AttrKind&,
                            const typename AttrKind::value_type& value);
+
+  inline const Type* getType(const Node& n);
 };
 
 class NodeManagerScope {
@@ -111,21 +114,25 @@ public:
 template <class AttrKind>
 inline typename AttrKind::value_type NodeManager::getAttribute(const Node& n,
                                                                const AttrKind&) const {
-  return d_am.getAttribute(n, AttrKind());
+  return d_attrManager.getAttribute(n, AttrKind());
 }
 
 template <class AttrKind>
 inline bool NodeManager::hasAttribute(const Node& n,
                                       const AttrKind&,
                                       typename AttrKind::value_type* ret) const {
-  return d_am.hasAttribute(n, AttrKind(), ret);
+  return d_attrManager.hasAttribute(n, AttrKind(), ret);
 }
 
 template <class AttrKind>
 inline void NodeManager::setAttribute(const Node& n,
                                       const AttrKind&,
                                       const typename AttrKind::value_type& value) {
-  d_am.setAttribute(n, AttrKind(), value);
+  d_attrManager.setAttribute(n, AttrKind(), value);
+}
+
+inline const Type* NodeManager::getType(const Node& n) {
+  return getAttribute(n,CVC4::expr::TypeAttr());
 }
 
 }/* CVC4 namespace */

diff --git a/src/parser/antlr_parser.cpp b/src/parser/antlr_parser.cpp
index 0fdde07ff2753befe9f3ec56aaed533da79a9f95..28cee62e752764937df3da04bc59ee681ddb9b59 100644 (file)
--- a/src/parser/antlr_parser.cpp
+++ b/src/parser/antlr_parser.cpp
@@ -10,7 +10,7 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.
  **
- ** [[ Add file-specific comments here ]]
+ ** A super-class for ANTLR-generated input language parsers
  **/
 
 /*
@@ -75,7 +75,7 @@ const Type*
 AntlrParser::getType(std::string var_name, 
                      SymbolType type) {
   Assert( isDeclared(var_name, type) );
-  const Type* t = d_varTypeTable.getObject(var_name);
+  const Type* t = getSymbol(var_name,type).getType();
   return t;
 }
 
@@ -173,7 +173,6 @@ AntlrParser::mkVar(const std::string name, const Type* type) {
   Assert( !isDeclared(name) ) ;
   Expr expr = d_exprManager->mkVar(type, name);
   d_varSymbolTable.bindName(name, expr);
-  d_varTypeTable.bindName(name,type);
   Assert( isDeclared(name) ) ;
   return expr;
 }

diff --git a/src/parser/antlr_parser.h b/src/parser/antlr_parser.h
index 5c3f2f1f1ffb40fc788917463f730be9b2bb82f1..cab0a4f386ba6a855ba1b810067b9311901ad748 100644 (file)
--- a/src/parser/antlr_parser.h
+++ b/src/parser/antlr_parser.h
@@ -332,10 +332,6 @@ private:
   /** The symbol table lookup */
   SymbolTable<Expr> d_varSymbolTable;
 
-  /** A temporary hack: keep all the variable types in their own special
-      table. These should actually be Expr attributes. */
-  SymbolTable<const Type*> d_varTypeTable;
-
   /** The sort table */
   SymbolTable<const Type*> d_sortTable;
 

diff --git a/test/unit/expr/node_white.h b/test/unit/expr/node_white.h
index e2e1a94fddb8f911c85d31798dca3f1ea23ef500..788c71d9bd52aeaad330cfed8a200e9e58ff8737 100644 (file)
--- a/test/unit/expr/node_white.h
+++ b/test/unit/expr/node_white.h
@@ -93,7 +93,7 @@ public:
   }
 
   void testAttributes() {
-    AttributeManager& am = d_nm->d_am;
+    AttributeManager& am = d_nm->d_attrManager;
 
     //Debug.on("boolattr");