diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-06-09 00:35:38 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-06-09 00:35:38 +0000 |
commit | 700689a4e4ed42b5198816611eac5bcc1278284d (patch) | |
tree | 0d6029f9bc4f46a721930a27a47ac487771c452e /src/printer/dagification_visitor.h | |
parent | a0411d4baad389ce88d4bd26edc8ed811625887c (diff) |
Dagification of output expressions.
By default, common subexpressions are dagified if they appear > 1 time and are not constants or variables.
This can be changed with --default-expr-dag=N --- N is a threshold such that if the subexpression occurs > N
times, it is dagified; a setting of 0 turns off dagification entirely.
If you notice strange dumping behavior (taking too long to print anything, e.g.), revert to the old behavior
with --default-expr-dag=0 and let me know of the problem.
Diffstat (limited to 'src/printer/dagification_visitor.h')
-rw-r--r-- | src/printer/dagification_visitor.h | 180 |
1 files changed, 180 insertions, 0 deletions
diff --git a/src/printer/dagification_visitor.h b/src/printer/dagification_visitor.h new file mode 100644 index 000000000..8e17f6027 --- /dev/null +++ b/src/printer/dagification_visitor.h @@ -0,0 +1,180 @@ +/********************* */ +/*! \file dagification_visitor.h + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011, 2012 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__PRINTER__DAGIFICATION_VISITOR_H +#define __CVC4__PRINTER__DAGIFICATION_VISITOR_H + +#include "context/context.h" +#include "theory/substitutions.h" +#include "expr/node.h" +#include "util/hash.h" + +#include <vector> +#include <string> +#include <sstream> + +namespace CVC4 { +namespace printer { + +class DagificationVisitor { + + unsigned d_threshold; + std::string d_letVarPrefix; + std::hash_map<TNode, unsigned, TNodeHashFunction> d_nodeCount; + TNode d_top; + context::Context* d_context; + theory::SubstitutionMap* d_substitutions; + unsigned d_letVar; + bool d_done; + std::hash_map<TNode, TNode, TNodeHashFunction> d_uniqueParent; + std::vector<TNode> d_substNodes; + +public: + + typedef void return_type; + + DagificationVisitor(unsigned threshold, std::string letVarPrefix = "_let_") : + d_threshold(threshold), + d_letVarPrefix(letVarPrefix), + d_nodeCount(), + d_top(), + d_context(new context::Context()), + d_substitutions(new theory::SubstitutionMap(d_context)), + d_letVar(0), + d_done(false), + d_uniqueParent(), + d_substNodes() { + + // 0 doesn't make sense + CheckArgument(threshold > 0, threshold); + } + + ~DagificationVisitor() { + delete d_substitutions; + delete d_context; + } + + /** + * Returns true if current has already been dagified. + */ + bool alreadyVisited(TNode current, TNode parent) { + // don't visit variables, constants, or those exprs that we've + // already seen more than the threshold: if we've increased + // the count beyond the threshold already, we've done the same + // for all subexpressions, so it isn't useful to traverse and + // increment again (they'll be dagified anyway). + return current.getMetaKind() == kind::metakind::VARIABLE || + current.getMetaKind() == kind::metakind::CONSTANT || + ( ( current.getKind() == kind::NOT || + current.getKind() == kind::UMINUS ) && + ( current[0].getMetaKind() == kind::metakind::VARIABLE || + current[0].getMetaKind() == kind::metakind::CONSTANT ) ) || + current.getKind() == kind::SORT_TYPE || + d_nodeCount[current] > d_threshold; + } + + /** + * Dagify the "current" expression. + */ + void visit(TNode current, TNode parent) { + if(d_uniqueParent.find(current) != d_uniqueParent.end()) { + TNode& uniqueParent = d_uniqueParent[current]; + + if(!uniqueParent.isNull() && uniqueParent != parent) { + // there is not a unique parent for this expr + uniqueParent = TNode::null(); + } + + unsigned count = ++d_nodeCount[current]; + + if(count > d_threshold) { + d_substNodes.push_back(current); + } + } else { + Assert(d_nodeCount[current] == 0); + d_nodeCount[current] = 1; + d_uniqueParent[current] = parent; + } + } + + /** + * Marks the node as the starting literal. + */ + void start(TNode node) { + Assert(!d_done, "DagificationVisitor cannot be re-used"); + d_top = node; + } + + /** + * Called when we're done with all visitation. + */ + void done(TNode node) { + Assert(!d_done); + + d_done = true; + + // letify subexprs before parents (cascading LETs) + std::sort(d_substNodes.begin(), d_substNodes.end()); + + for(std::vector<TNode>::iterator i = d_substNodes.begin(); + i != d_substNodes.end(); + ++i) { + Assert(d_nodeCount[*i] > d_threshold); + TNode parent = d_uniqueParent[*i]; + if(!parent.isNull() && d_nodeCount[parent] > d_threshold) { + // no need to letify this expr, because it only occurs in + // a single super-expression, and that one will be letified + continue; + } + + std::stringstream ss; + ss << d_letVarPrefix << d_letVar++; + Node letvar = NodeManager::currentNM()->mkVar(ss.str(), (*i).getType()); + + Node n = d_substitutions->apply(*i); + // the three last arguments to addSubstitution are: + // invalidateCache -- the rhs of our substitution is a letvar, + // we're not going to use it on lhs so no cache problem + // backSub - no need for SubstitutionMap to do internal substitution, + // we did our own above + // forwardSub - ditto + Assert(! d_substitutions->hasSubstitution(n)); + d_substitutions->addSubstitution(n, letvar); + } + } + + /** + * Get the let substitutions. + */ + const theory::SubstitutionMap& getLets() { + Assert(d_done, "DagificationVisitor must be used as a visitor before getting the dagified version out!"); + return *d_substitutions; + } + + /** + * Return the let-substituted expression. + */ + Node getDagifiedBody() { + Assert(d_done, "DagificationVisitor must be used as a visitor before getting the dagified version out!"); + return d_substitutions->apply(d_top); + } + +};/* class DagificationVisitor */ + +}/* CVC4::printer namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__PRINTER__DAGIFICATION_VISITOR_H */ |