summaryrefslogtreecommitdiff
path: root/src/expr/node_manager.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/expr/node_manager.cpp')
-rw-r--r--src/expr/node_manager.cpp164
1 files changed, 159 insertions, 5 deletions
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index cc890b9b9..f6424cfe0 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -17,7 +17,9 @@
**/
#include "expr/node_manager.h"
+#include "expr/node_manager_attributes.h"
+#include "expr/attribute.h"
#include "util/cvc4_assert.h"
#include "options/options.h"
#include "util/statistics_registry.h"
@@ -83,7 +85,7 @@ NodeManager::NodeManager(context::Context* ctxt,
d_options(new Options()),
d_statisticsRegistry(new StatisticsRegistry()),
next_id(0),
- d_attrManager(ctxt),
+ d_attrManager(new expr::attr::AttributeManager(ctxt)),
d_exprManager(exprManager),
d_nodeUnderDeletion(NULL),
d_inReclaimZombies(false),
@@ -97,7 +99,7 @@ NodeManager::NodeManager(context::Context* ctxt,
d_options(new Options(options)),
d_statisticsRegistry(new StatisticsRegistry()),
next_id(0),
- d_attrManager(ctxt),
+ d_attrManager(new expr::attr::AttributeManager(ctxt)),
d_exprManager(exprManager),
d_nodeUnderDeletion(NULL),
d_inReclaimZombies(false),
@@ -105,7 +107,7 @@ NodeManager::NodeManager(context::Context* ctxt,
init();
}
-inline void NodeManager::init() {
+void NodeManager::init() {
poolInsert( &expr::NodeValue::s_null );
for(unsigned i = 0; i < unsigned(kind::LAST_KIND); ++i) {
@@ -125,7 +127,7 @@ NodeManager::~NodeManager() {
{
ScopedBool dontGC(d_inReclaimZombies);
- d_attrManager.deleteAllAttributes();
+ d_attrManager->deleteAllAttributes();
}
for(unsigned i = 0; i < unsigned(kind::LAST_KIND); ++i) {
@@ -153,6 +155,7 @@ NodeManager::~NodeManager() {
}
delete d_statisticsRegistry;
+ delete d_attrManager;
delete d_options;
}
@@ -216,7 +219,7 @@ void NodeManager::reclaimZombies() {
d_nodeUnderDeletion = nv;
// remove attributes
- d_attrManager.deleteAllAttributes(nv);
+ d_attrManager->deleteAllAttributes(nv);
// decr ref counts of children
nv->decrRefCounts();
@@ -432,4 +435,155 @@ TypeNode NodeManager::getDatatypeForTupleRecord(TypeNode t) {
return dtt;
}
+TypeNode NodeManager::mkSort(uint32_t flags) {
+ NodeBuilder<1> nb(this, kind::SORT_TYPE);
+ Node sortTag = NodeBuilder<0>(this, kind::SORT_TAG);
+ nb << sortTag;
+ TypeNode tn = nb.constructTypeNode();
+ for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) {
+ (*i)->nmNotifyNewSort(tn, flags);
+ }
+ return tn;
+}
+
+TypeNode NodeManager::mkSort(const std::string& name, uint32_t flags) {
+ NodeBuilder<1> nb(this, kind::SORT_TYPE);
+ Node sortTag = NodeBuilder<0>(this, kind::SORT_TAG);
+ nb << sortTag;
+ TypeNode tn = nb.constructTypeNode();
+ setAttribute(tn, expr::VarNameAttr(), name);
+ for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) {
+ (*i)->nmNotifyNewSort(tn, flags);
+ }
+ return tn;
+}
+
+TypeNode NodeManager::mkSort(TypeNode constructor,
+ const std::vector<TypeNode>& children,
+ uint32_t flags) {
+ Assert(constructor.getKind() == kind::SORT_TYPE &&
+ constructor.getNumChildren() == 0,
+ "expected a sort constructor");
+ Assert(children.size() > 0, "expected non-zero # of children");
+ Assert( hasAttribute(constructor.d_nv, expr::SortArityAttr()) &&
+ hasAttribute(constructor.d_nv, expr::VarNameAttr()),
+ "expected a sort constructor" );
+ std::string name = getAttribute(constructor.d_nv, expr::VarNameAttr());
+ Assert(getAttribute(constructor.d_nv, expr::SortArityAttr()) == children.size(),
+ "arity mismatch in application of sort constructor");
+ NodeBuilder<> nb(this, kind::SORT_TYPE);
+ Node sortTag = Node(constructor.d_nv->d_children[0]);
+ nb << sortTag;
+ nb.append(children);
+ TypeNode type = nb.constructTypeNode();
+ setAttribute(type, expr::VarNameAttr(), name);
+ for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) {
+ (*i)->nmNotifyInstantiateSortConstructor(constructor, type, flags);
+ }
+ return type;
+}
+
+TypeNode NodeManager::mkSortConstructor(const std::string& name,
+ size_t arity) {
+ Assert(arity > 0);
+ NodeBuilder<> nb(this, kind::SORT_TYPE);
+ Node sortTag = NodeBuilder<0>(this, kind::SORT_TAG);
+ nb << sortTag;
+ TypeNode type = nb.constructTypeNode();
+ setAttribute(type, expr::VarNameAttr(), name);
+ setAttribute(type, expr::SortArityAttr(), arity);
+ for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) {
+ (*i)->nmNotifyNewSortConstructor(type);
+ }
+ return type;
+}
+
+Node NodeManager::mkVar(const std::string& name, const TypeNode& type, uint32_t flags) {
+ Node n = NodeBuilder<0>(this, kind::VARIABLE);
+ setAttribute(n, TypeAttr(), type);
+ setAttribute(n, TypeCheckedAttr(), true);
+ setAttribute(n, expr::VarNameAttr(), name);
+ setAttribute(n, expr::GlobalVarAttr(), flags & ExprManager::VAR_FLAG_GLOBAL);
+ for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) {
+ (*i)->nmNotifyNewVar(n, flags);
+ }
+ return n;
+}
+
+Node* NodeManager::mkVarPtr(const std::string& name,
+ const TypeNode& type, uint32_t flags) {
+ Node* n = NodeBuilder<0>(this, kind::VARIABLE).constructNodePtr();
+ setAttribute(*n, TypeAttr(), type);
+ setAttribute(*n, TypeCheckedAttr(), true);
+ setAttribute(*n, expr::VarNameAttr(), name);
+ setAttribute(*n, expr::GlobalVarAttr(), flags & ExprManager::VAR_FLAG_GLOBAL);
+ for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) {
+ (*i)->nmNotifyNewVar(*n, flags);
+ }
+ return n;
+}
+
+Node NodeManager::mkBoundVar(const std::string& name, const TypeNode& type) {
+ Node n = mkBoundVar(type);
+ setAttribute(n, expr::VarNameAttr(), name);
+ return n;
+}
+
+Node* NodeManager::mkBoundVarPtr(const std::string& name,
+ const TypeNode& type) {
+ Node* n = mkBoundVarPtr(type);
+ setAttribute(*n, expr::VarNameAttr(), name);
+ return n;
+}
+
+Node NodeManager::mkVar(const TypeNode& type, uint32_t flags) {
+ Node n = NodeBuilder<0>(this, kind::VARIABLE);
+ setAttribute(n, TypeAttr(), type);
+ setAttribute(n, TypeCheckedAttr(), true);
+ setAttribute(n, expr::GlobalVarAttr(), flags & ExprManager::VAR_FLAG_GLOBAL);
+ for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) {
+ (*i)->nmNotifyNewVar(n, flags);
+ }
+ return n;
+}
+
+Node* NodeManager::mkVarPtr(const TypeNode& type, uint32_t flags) {
+ Node* n = NodeBuilder<0>(this, kind::VARIABLE).constructNodePtr();
+ setAttribute(*n, TypeAttr(), type);
+ setAttribute(*n, TypeCheckedAttr(), true);
+ setAttribute(*n, expr::GlobalVarAttr(), flags & ExprManager::VAR_FLAG_GLOBAL);
+ for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) {
+ (*i)->nmNotifyNewVar(*n, flags);
+ }
+ return n;
+}
+
+Node NodeManager::mkBoundVar(const TypeNode& type) {
+ Node n = NodeBuilder<0>(this, kind::BOUND_VARIABLE);
+ setAttribute(n, TypeAttr(), type);
+ setAttribute(n, TypeCheckedAttr(), true);
+ return n;
+}
+
+Node* NodeManager::mkBoundVarPtr(const TypeNode& type) {
+ Node* n = NodeBuilder<0>(this, kind::BOUND_VARIABLE).constructNodePtr();
+ setAttribute(*n, TypeAttr(), type);
+ setAttribute(*n, TypeCheckedAttr(), true);
+ return n;
+}
+
+Node NodeManager::mkInstConstant(const TypeNode& type) {
+ Node n = NodeBuilder<0>(this, kind::INST_CONSTANT);
+ n.setAttribute(TypeAttr(), type);
+ n.setAttribute(TypeCheckedAttr(), true);
+ return n;
+}
+
+Node NodeManager::mkAbstractValue(const TypeNode& type) {
+ Node n = mkConst(AbstractValue(++d_abstractValueCount));
+ n.setAttribute(TypeAttr(), type);
+ n.setAttribute(TypeCheckedAttr(), true);
+ return n;
+}
+
}/* CVC4 namespace */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback