diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-10-07 07:16:49 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-10-07 07:16:49 +0000 |
commit | 2d7ff62cd52c5c56f29b6567489310cc45767236 (patch) | |
tree | afb975f93b219e7b7a670a4dfc2897e425fd9bf7 /src/expr/node.h | |
parent | ce4a5fe6a2529f11eaff66b6cdcdb32ef5309323 (diff) |
SMT-LIBv2 (define-fun...) command now functional; does eager expansion at preprocessing time
Diffstat (limited to 'src/expr/node.h')
-rw-r--r-- | src/expr/node.h | 67 |
1 files changed, 67 insertions, 0 deletions
diff --git a/src/expr/node.h b/src/expr/node.h index 67d46a977..bd6b53522 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -380,6 +380,20 @@ public: throw (CVC4::TypeCheckingExceptionPrivate, CVC4::AssertionException); /** + * Substitution of Nodes. + */ + Node substitute(TNode node, TNode replacement) const; + + /** + * Simultaneous substitution of Nodes. + */ + template <class Iterator1, class Iterator2> + Node substitute(Iterator1 nodesBegin, + Iterator1 nodesEnd, + Iterator2 replacementsBegin, + Iterator2 replacementsEnd) const; + + /** * Returns the kind of this node. * @return the kind */ @@ -1035,6 +1049,59 @@ TypeNode NodeTemplate<ref_count>::getType(bool check) const return NodeManager::currentNM()->getType(*this, check); } +template <bool ref_count> +Node NodeTemplate<ref_count>::substitute(TNode node, + TNode replacement) const { + NodeBuilder<> nb(getKind()); + if(getMetaKind() == kind::metakind::PARAMETERIZED) { + // push the operator + nb << getOperator(); + } + for(TNode::const_iterator i = begin(), + iend = end(); + i != iend; + ++i) { + if(*i == node) { + nb << replacement; + } else { + (*i).substitute(node, replacement); + } + } + Node n = nb; + return n; +} + +template <bool ref_count> +template <class Iterator1, class Iterator2> +Node NodeTemplate<ref_count>::substitute(Iterator1 nodesBegin, + Iterator1 nodesEnd, + Iterator2 replacementsBegin, + Iterator2 replacementsEnd) const { + Assert( nodesEnd - nodesBegin == replacementsEnd - replacementsBegin, + "Substitution iterator ranges must be equal size" ); + Iterator1 j = find(nodesBegin, nodesEnd, *this); + if(j != nodesEnd) { + return *(replacementsBegin + (j - nodesBegin)); + } else if(getNumChildren() == 0) { + return *this; + } else { + NodeBuilder<> nb(getKind()); + if(getMetaKind() == kind::metakind::PARAMETERIZED) { + // push the operator + nb << getOperator(); + } + for(TNode::const_iterator i = begin(), + iend = end(); + i != iend; + ++i) { + nb << (*i).substitute(nodesBegin, nodesEnd, + replacementsBegin, replacementsEnd); + } + Node n = nb; + return n; + } +} + #ifdef CVC4_DEBUG /** * Pretty printer for use within gdb. This is not intended to be used |