From: Christopher L. Conway Date: Mon, 22 Feb 2010 21:28:25 +0000 (+0000) Subject: Switching to types-as-attributes in parser X-Git-Tag: cvc5-1.0.0~9231 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c5872ac197a68ea0686c90f3a8bd1e7cc993532d;p=cvc5.git Switching to types-as-attributes in parser --- diff --git a/src/expr/expr.cpp b/src/expr/expr.cpp index c29b7e448..7dc8c8f96 100644 --- 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 096094aff..27b7846db 100644 --- 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 71368c101..6231d5a8a 100644 --- 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& children) { - NodeManagerScope nms(d_nm); + NodeManagerScope nms(d_nodeManager); vector nodes; vector::const_iterator it = children.begin(); @@ -98,14 +98,14 @@ Expr ExprManager::mkExpr(Kind kind, const vector& 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& 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 d84cf76be..4b00c27fc 100644 --- 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 90dd86712..080623e21 100644 --- 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 517a9eb7f..77f9141f1 100644 --- 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 c6aee3dea..ae6bdbd29 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -73,8 +73,7 @@ Node NodeManager::mkNode(Kind kind, const vector& 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 d6d54bd5d..29c738c10 100644 --- 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::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 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 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 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 0fdde07ff..28cee62e7 100644 --- 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 5c3f2f1f1..cab0a4f38 100644 --- a/src/parser/antlr_parser.h +++ b/src/parser/antlr_parser.h @@ -332,10 +332,6 @@ private: /** The symbol table lookup */ SymbolTable d_varSymbolTable; - /** A temporary hack: keep all the variable types in their own special - table. These should actually be Expr attributes. */ - SymbolTable d_varTypeTable; - /** The sort table */ SymbolTable d_sortTable; diff --git a/test/unit/expr/node_white.h b/test/unit/expr/node_white.h index e2e1a94fd..788c71d9b 100644 --- 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");