summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/expr/expr.cpp69
-rw-r--r--src/expr/expr.h7
-rw-r--r--src/expr/expr_manager.cpp52
-rw-r--r--src/expr/expr_manager.h2
-rw-r--r--src/expr/node.cpp7
-rw-r--r--src/expr/node.h2
-rw-r--r--src/expr/node_manager.cpp3
-rw-r--r--src/expr/node_manager.h17
-rw-r--r--src/parser/antlr_parser.cpp5
-rw-r--r--src/parser/antlr_parser.h4
-rw-r--r--test/unit/expr/node_white.h2
11 files changed, 95 insertions, 75 deletions
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<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 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<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 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*, __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 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<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 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");
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback