summaryrefslogtreecommitdiff
path: root/src/expr/node_manager.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/expr/node_manager.h')
-rw-r--r--src/expr/node_manager.h174
1 files changed, 114 insertions, 60 deletions
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 0c62d31c5..31f6d75d9 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -75,12 +75,12 @@ typedef expr::Attribute<expr::attr::DatatypeRecordTag, TypeNode> DatatypeRecordA
class NodeManagerListener {
public:
virtual ~NodeManagerListener() { }
- virtual void nmNotifyNewSort(TypeNode tn) { }
+ virtual void nmNotifyNewSort(TypeNode tn, uint32_t flags) { }
virtual void nmNotifyNewSortConstructor(TypeNode tn) { }
- virtual void nmNotifyInstantiateSortConstructor(TypeNode ctor, TypeNode sort) { }
+ virtual void nmNotifyInstantiateSortConstructor(TypeNode ctor, TypeNode sort, uint32_t flags) { }
virtual void nmNotifyNewDatatypes(const std::vector<DatatypeType>& datatypes) { }
- virtual void nmNotifyNewVar(TNode n, bool isGlobal) { }
- virtual void nmNotifyNewSkolem(TNode n, const std::string& comment, bool isGlobal) { }
+ virtual void nmNotifyNewVar(TNode n, uint32_t flags) { }
+ virtual void nmNotifyNewSkolem(TNode n, const std::string& comment, uint32_t flags) { }
};/* class NodeManagerListener */
class NodeManager {
@@ -90,8 +90,8 @@ class NodeManager {
friend class expr::TypeChecker;
// friends so they can access mkVar() here, which is private
- friend Expr ExprManager::mkVar(const std::string&, Type, bool isGlobal);
- friend Expr ExprManager::mkVar(Type, bool isGlobal);
+ friend Expr ExprManager::mkVar(const std::string&, Type, uint32_t flags);
+ friend Expr ExprManager::mkVar(Type, uint32_t flags);
// friend so it can access NodeManager's d_listeners and notify clients
friend std::vector<DatatypeType> ExprManager::mkMutualDatatypeTypes(const std::vector<Datatype>&, const std::set<Type>&);
@@ -309,12 +309,12 @@ class NodeManager {
* version of this is private to avoid internal uses of mkVar() from
* within CVC4. Such uses should employ mkSkolem() instead.
*/
- Node mkVar(const std::string& name, const TypeNode& type, bool isGlobal = false);
- Node* mkVarPtr(const std::string& name, const TypeNode& type, bool isGlobal = false);
+ Node mkVar(const std::string& name, const TypeNode& type, uint32_t flags = ExprManager::VAR_FLAG_NONE);
+ Node* mkVarPtr(const std::string& name, const TypeNode& type, uint32_t flags = ExprManager::VAR_FLAG_NONE);
/** Create a variable with the given type. */
- Node mkVar(const TypeNode& type, bool isGlobal = false);
- Node* mkVarPtr(const TypeNode& type, bool isGlobal = false);
+ Node mkVar(const TypeNode& type, uint32_t flags = ExprManager::VAR_FLAG_NONE);
+ Node* mkVarPtr(const TypeNode& type, uint32_t flags = ExprManager::VAR_FLAG_NONE);
public:
@@ -353,6 +353,9 @@ public:
d_listeners.erase(elt);
}
+ /** Get a Kind from an operator expression */
+ static inline Kind operatorToKind(TNode n);
+
// general expression-builders
/** Create a node with one child. */
@@ -680,6 +683,9 @@ public:
/** Get the (singleton) type for strings. */
inline TypeNode stringType();
+ /** Get the (singleton) type for RegExp. */
+ inline TypeNode regexpType();
+
/** Get the bound var list type. */
inline TypeNode boundVarListType();
@@ -775,14 +781,15 @@ public:
inline TypeNode mkTesterType(TypeNode domain);
/** Make a new (anonymous) sort of arity 0. */
- inline TypeNode mkSort();
+ inline TypeNode mkSort(uint32_t flags = ExprManager::SORT_FLAG_NONE);
/** Make a new sort with the given name of arity 0. */
- inline TypeNode mkSort(const std::string& name);
+ inline TypeNode mkSort(const std::string& name, uint32_t flags = ExprManager::SORT_FLAG_NONE);
/** Make a new sort by parameterizing the given sort constructor. */
inline TypeNode mkSort(TypeNode constructor,
- const std::vector<TypeNode>& children);
+ const std::vector<TypeNode>& children,
+ uint32_t flags = ExprManager::SORT_FLAG_NONE);
/** Make a new sort with the given name and arity. */
inline TypeNode mkSortConstructor(const std::string& name, size_t arity);
@@ -1026,6 +1033,11 @@ inline TypeNode NodeManager::stringType() {
return TypeNode(mkTypeConst<TypeConstant>(STRING_TYPE));
}
+/** Get the (singleton) type for regexps. */
+inline TypeNode NodeManager::regexpType() {
+ return TypeNode(mkTypeConst<TypeConstant>(REGEXP_TYPE));
+}
+
/** Get the bound var list type. */
inline TypeNode NodeManager::boundVarListType() {
return TypeNode(mkTypeConst<TypeConstant>(BOUND_VAR_LIST_TYPE));
@@ -1087,7 +1099,6 @@ NodeManager::mkPredicateType(const std::vector<TypeNode>& sorts) {
}
inline TypeNode NodeManager::mkTupleType(const std::vector<TypeNode>& types) {
- Assert(types.size() >= 1);
std::vector<TypeNode> typeNodes;
for (unsigned i = 0; i < types.size(); ++ i) {
CheckArgument(!types[i].isFunctionLike(), types,
@@ -1218,31 +1229,32 @@ inline bool NodeManager::hasOperator(Kind k) {
}
}
-inline TypeNode NodeManager::mkSort() {
+inline 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);
+ (*i)->nmNotifyNewSort(tn, flags);
}
return tn;
}
-inline TypeNode NodeManager::mkSort(const std::string& name) {
+inline 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);
+ (*i)->nmNotifyNewSort(tn, flags);
}
return tn;
}
inline TypeNode NodeManager::mkSort(TypeNode constructor,
- const std::vector<TypeNode>& children) {
+ const std::vector<TypeNode>& children,
+ uint32_t flags) {
Assert(constructor.getKind() == kind::SORT_TYPE &&
constructor.getNumChildren() == 0,
"expected a sort constructor");
@@ -1260,7 +1272,7 @@ inline TypeNode NodeManager::mkSort(TypeNode constructor,
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);
+ (*i)->nmNotifyInstantiateSortConstructor(constructor, type, flags);
}
return type;
}
@@ -1280,6 +1292,10 @@ inline TypeNode NodeManager::mkSortConstructor(const std::string& name,
return type;
}
+inline Kind NodeManager::operatorToKind(TNode n) {
+ return kind::operatorToKind(n.d_nv);
+}
+
inline Node NodeManager::mkNode(Kind kind, TNode child1) {
NodeBuilder<1> nb(this, kind);
nb << child1;
@@ -1367,80 +1383,114 @@ inline Node* NodeManager::mkNodePtr(Kind kind,
// for operators
inline Node NodeManager::mkNode(TNode opNode) {
- NodeBuilder<1> nb(this, kind::operatorKindToKind(opNode.getKind()));
- nb << opNode;
+ NodeBuilder<1> nb(this, operatorToKind(opNode));
+ if(opNode.getKind() != kind::BUILTIN) {
+ nb << opNode;
+ }
return nb.constructNode();
}
inline Node* NodeManager::mkNodePtr(TNode opNode) {
- NodeBuilder<1> nb(this, kind::operatorKindToKind(opNode.getKind()));
- nb << opNode;
+ NodeBuilder<1> nb(this, operatorToKind(opNode));
+ if(opNode.getKind() != kind::BUILTIN) {
+ nb << opNode;
+ }
return nb.constructNodePtr();
}
inline Node NodeManager::mkNode(TNode opNode, TNode child1) {
- NodeBuilder<2> nb(this, kind::operatorKindToKind(opNode.getKind()));
- nb << opNode << child1;
+ NodeBuilder<2> nb(this, operatorToKind(opNode));
+ if(opNode.getKind() != kind::BUILTIN) {
+ nb << opNode;
+ }
+ nb << child1;
return nb.constructNode();
}
inline Node* NodeManager::mkNodePtr(TNode opNode, TNode child1) {
- NodeBuilder<2> nb(this, kind::operatorKindToKind(opNode.getKind()));
- nb << opNode << child1;
+ NodeBuilder<2> nb(this, operatorToKind(opNode));
+ if(opNode.getKind() != kind::BUILTIN) {
+ nb << opNode;
+ }
+ nb << child1;
return nb.constructNodePtr();
}
inline Node NodeManager::mkNode(TNode opNode, TNode child1, TNode child2) {
- NodeBuilder<3> nb(this, kind::operatorKindToKind(opNode.getKind()));
- nb << opNode << child1 << child2;
+ NodeBuilder<3> nb(this, operatorToKind(opNode));
+ if(opNode.getKind() != kind::BUILTIN) {
+ nb << opNode;
+ }
+ nb << child1 << child2;
return nb.constructNode();
}
inline Node* NodeManager::mkNodePtr(TNode opNode, TNode child1, TNode child2) {
- NodeBuilder<3> nb(this, kind::operatorKindToKind(opNode.getKind()));
- nb << opNode << child1 << child2;
+ NodeBuilder<3> nb(this, operatorToKind(opNode));
+ if(opNode.getKind() != kind::BUILTIN) {
+ nb << opNode;
+ }
+ nb << child1 << child2;
return nb.constructNodePtr();
}
inline Node NodeManager::mkNode(TNode opNode, TNode child1, TNode child2,
TNode child3) {
- NodeBuilder<4> nb(this, kind::operatorKindToKind(opNode.getKind()));
- nb << opNode << child1 << child2 << child3;
+ NodeBuilder<4> nb(this, operatorToKind(opNode));
+ if(opNode.getKind() != kind::BUILTIN) {
+ nb << opNode;
+ }
+ nb << child1 << child2 << child3;
return nb.constructNode();
}
inline Node* NodeManager::mkNodePtr(TNode opNode, TNode child1, TNode child2,
TNode child3) {
- NodeBuilder<4> nb(this, kind::operatorKindToKind(opNode.getKind()));
- nb << opNode << child1 << child2 << child3;
+ NodeBuilder<4> nb(this, operatorToKind(opNode));
+ if(opNode.getKind() != kind::BUILTIN) {
+ nb << opNode;
+ }
+ nb << child1 << child2 << child3;
return nb.constructNodePtr();
}
inline Node NodeManager::mkNode(TNode opNode, TNode child1, TNode child2,
TNode child3, TNode child4) {
- NodeBuilder<5> nb(this, kind::operatorKindToKind(opNode.getKind()));
- nb << opNode << child1 << child2 << child3 << child4;
+ NodeBuilder<5> nb(this, operatorToKind(opNode));
+ if(opNode.getKind() != kind::BUILTIN) {
+ nb << opNode;
+ }
+ nb << child1 << child2 << child3 << child4;
return nb.constructNode();
}
inline Node* NodeManager::mkNodePtr(TNode opNode, TNode child1, TNode child2,
TNode child3, TNode child4) {
- NodeBuilder<5> nb(this, kind::operatorKindToKind(opNode.getKind()));
- nb << opNode << child1 << child2 << child3 << child4;
+ NodeBuilder<5> nb(this, operatorToKind(opNode));
+ if(opNode.getKind() != kind::BUILTIN) {
+ nb << opNode;
+ }
+ nb << child1 << child2 << child3 << child4;
return nb.constructNodePtr();
}
inline Node NodeManager::mkNode(TNode opNode, TNode child1, TNode child2,
TNode child3, TNode child4, TNode child5) {
- NodeBuilder<6> nb(this, kind::operatorKindToKind(opNode.getKind()));
- nb << opNode << child1 << child2 << child3 << child4 << child5;
+ NodeBuilder<6> nb(this, operatorToKind(opNode));
+ if(opNode.getKind() != kind::BUILTIN) {
+ nb << opNode;
+ }
+ nb << child1 << child2 << child3 << child4 << child5;
return nb.constructNode();
}
inline Node* NodeManager::mkNodePtr(TNode opNode, TNode child1, TNode child2,
TNode child3, TNode child4, TNode child5) {
- NodeBuilder<6> nb(this, kind::operatorKindToKind(opNode.getKind()));
- nb << opNode << child1 << child2 << child3 << child4 << child5;
+ NodeBuilder<6> nb(this, operatorToKind(opNode));
+ if(opNode.getKind() != kind::BUILTIN) {
+ nb << opNode;
+ }
+ nb << child1 << child2 << child3 << child4 << child5;
return nb.constructNodePtr();
}
@@ -1449,8 +1499,10 @@ template <bool ref_count>
inline Node NodeManager::mkNode(TNode opNode,
const std::vector<NodeTemplate<ref_count> >&
children) {
- NodeBuilder<> nb(this, kind::operatorKindToKind(opNode.getKind()));
- nb << opNode;
+ NodeBuilder<> nb(this, operatorToKind(opNode));
+ if(opNode.getKind() != kind::BUILTIN) {
+ nb << opNode;
+ }
nb.append(children);
return nb.constructNode();
}
@@ -1459,8 +1511,10 @@ template <bool ref_count>
inline Node* NodeManager::mkNodePtr(TNode opNode,
const std::vector<NodeTemplate<ref_count> >&
children) {
- NodeBuilder<> nb(this, kind::operatorKindToKind(opNode.getKind()));
- nb << opNode;
+ NodeBuilder<> nb(this, operatorToKind(opNode));
+ if(opNode.getKind() != kind::BUILTIN) {
+ nb << opNode;
+ }
nb.append(children);
return nb.constructNodePtr();
}
@@ -1487,27 +1541,27 @@ inline TypeNode NodeManager::mkTypeNode(Kind kind,
}
-inline Node NodeManager::mkVar(const std::string& name, const TypeNode& type, bool isGlobal) {
+inline 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(), isGlobal);
+ 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, isGlobal);
+ (*i)->nmNotifyNewVar(n, flags);
}
return n;
}
inline Node* NodeManager::mkVarPtr(const std::string& name,
- const TypeNode& type, bool isGlobal) {
+ 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(), isGlobal);
+ 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, isGlobal);
+ (*i)->nmNotifyNewVar(*n, flags);
}
return n;
}
@@ -1525,24 +1579,24 @@ inline Node* NodeManager::mkBoundVarPtr(const std::string& name,
return n;
}
-inline Node NodeManager::mkVar(const TypeNode& type, bool isGlobal) {
+inline 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(), isGlobal);
+ 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, isGlobal);
+ (*i)->nmNotifyNewVar(n, flags);
}
return n;
}
-inline Node* NodeManager::mkVarPtr(const TypeNode& type, bool isGlobal) {
+inline 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(), isGlobal);
+ 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, isGlobal);
+ (*i)->nmNotifyNewVar(*n, flags);
}
return n;
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback