+++ /dev/null
-/********************* */
-/*! \file dagification_visitor.cpp
- ** \verbatim
- ** Top contributors (to current version):
- ** Morgan Deters, Andres Noetzli, Mathias Preiner
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory and their institutional affiliations.
- ** All rights reserved. See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief Implementation of a dagifier for CVC4 expressions
- **
- ** Implementation of a dagifier for CVC4 expressions.
- **/
-
-#include "printer/dagification_visitor.h"
-
-#include "context/context.h"
-#include "expr/node_algorithm.h"
-#include "expr/node_manager_attributes.h"
-#include "theory/substitutions.h"
-
-#include <sstream>
-
-namespace CVC4 {
-namespace printer {
-
-DagificationVisitor::DagificationVisitor(unsigned threshold,
- std::string letVarPrefix)
- : d_threshold(threshold),
- d_letVarPrefix(letVarPrefix),
- d_nodeCount(),
- d_reservedLetNames(),
- 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
- AlwaysAssertArgument(threshold > 0, threshold);
-}
-
-DagificationVisitor::~DagificationVisitor() {
- delete d_substitutions;
- delete d_context;
-}
-
-bool DagificationVisitor::alreadyVisited(TNode current, TNode parent) {
- Kind ck = current.getKind();
- if (current.isClosure())
- {
- // for quantifiers, we visit them but we don't recurse on them
- visit(current, parent);
-
- // search for variables that start with the let prefix
- std::unordered_set<TNode, TNodeHashFunction> vs;
- expr::getVariables(current, vs);
- for (const TNode v : vs)
- {
- const std::string name = v.getAttribute(expr::VarNameAttr());
- if (name.compare(0, d_letVarPrefix.size(), d_letVarPrefix) == 0)
- {
- d_reservedLetNames.insert(name);
- }
- }
- return true;
- }
- else if (current.isVar())
- {
- const std::string name = current.getAttribute(expr::VarNameAttr());
- if (name.compare(0, d_letVarPrefix.size(), d_letVarPrefix) == 0)
- {
- d_reservedLetNames.insert(name);
- }
- }
- // 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.isVar() || current.getMetaKind() == kind::metakind::CONSTANT
- || current.getNumChildren() == 0
- || ((ck == kind::NOT || ck == kind::UMINUS)
- && (current[0].isVar()
- || current[0].getMetaKind() == kind::metakind::CONSTANT))
- || ck == kind::SORT_TYPE || d_nodeCount[current] > d_threshold;
-}
-
-void DagificationVisitor::visit(TNode current, TNode parent) {
-
-#ifdef CVC4_TRACING
-# ifdef CVC4_DEBUG
- // turn off dagification for Debug stream while we're doing this work
- Node::dag::Scope scopeDebug(Debug.getStream(), false);
-# endif /* CVC4_DEBUG */
- // turn off dagification for Trace stream while we're doing this work
- Node::dag::Scope scopeTrace(Trace.getStream(), false);
-#endif /* CVC4_TRACING */
-
- if(d_uniqueParent.find(current) != d_uniqueParent.end()) {
- // we've seen this expr before
-
- TNode& uniqueParent = d_uniqueParent[current];
-
- // We restrict this optimization to nodes with arity 1 since otherwise we
- // may run into issues with tree traverals. Without this restriction
- // dumping regress3/pp-regfile increases the file size by a factor of 5000.
- if (!uniqueParent.isNull()
- && (uniqueParent != parent || parent.getNumChildren() > 1))
- {
- // there is not a unique parent for this expr, mark it
- uniqueParent = TNode::null();
- }
-
- // increase the count
- const unsigned count = ++d_nodeCount[current];
-
- if(count > d_threshold) {
- // candidate for a let binder
- d_substNodes.push_back(current);
- }
- } else {
- // we haven't seen this expr before
- Assert(d_nodeCount[current] == 0);
- d_nodeCount[current] = 1;
- d_uniqueParent[current] = parent;
- }
-}
-
-void DagificationVisitor::start(TNode node) {
- AlwaysAssert(!d_done) << "DagificationVisitor cannot be re-used";
- d_top = node;
-}
-
-void DagificationVisitor::done(TNode node) {
- AlwaysAssert(!d_done);
-
- d_done = true;
-
-#ifdef CVC4_TRACING
-# ifdef CVC4_DEBUG
- // turn off dagification for Debug stream while we're doing this work
- Node::dag::Scope scopeDebug(Debug.getStream(), false);
-# endif /* CVC4_DEBUG */
- // turn off dagification for Trace stream while we're doing this work
- Node::dag::Scope scopeTrace(Trace.getStream(), false);
-#endif /* CVC4_TRACING */
-
- // 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;
- }
-
- // construct the let binder
- std::stringstream ss;
- do
- {
- ss.str("");
- ss << d_letVarPrefix << d_letVar++;
- } while (d_reservedLetNames.find(ss.str()) != d_reservedLetNames.end());
- Node letvar = NodeManager::currentNM()->mkSkolem(ss.str(), (*i).getType(), "dagification", NodeManager::SKOLEM_NO_NOTIFY | NodeManager::SKOLEM_EXACT_NAME);
-
- // apply previous substitutions to the rhs, enabling cascading LETs
- Node n = d_substitutions->apply(*i);
- Assert(!d_substitutions->hasSubstitution(n));
- d_substitutions->addSubstitution(n, letvar);
- }
-}
-
-const theory::SubstitutionMap& DagificationVisitor::getLets() {
- AlwaysAssert(d_done)
- << "DagificationVisitor must be used as a visitor before "
- "getting the dagified version out!";
- return *d_substitutions;
-}
-
-Node DagificationVisitor::getDagifiedBody() {
- AlwaysAssert(d_done)
- << "DagificationVisitor must be used as a visitor before "
- "getting the dagified version out!";
-
-#ifdef CVC4_TRACING
-# ifdef CVC4_DEBUG
- // turn off dagification for Debug stream while we're doing this work
- Node::dag::Scope scopeDebug(Debug.getStream(), false);
-# endif /* CVC4_DEBUG */
- // turn off dagification for Trace stream while we're doing this work
- Node::dag::Scope scopeTrace(Trace.getStream(), false);
-#endif /* CVC4_TRACING */
-
- return d_substitutions->apply(d_top);
-}
-
-}/* CVC4::printer namespace */
-}/* CVC4 namespace */
+++ /dev/null
-/********************* */
-/*! \file dagification_visitor.h
- ** \verbatim
- ** Top contributors (to current version):
- ** Morgan Deters, Andres Noetzli, Mathias Preiner
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory and their institutional affiliations.
- ** All rights reserved. See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief A dagifier for CVC4 expressions
- **
- ** A dagifier for CVC4 expressions.
- **/
-
-#include "cvc4_private.h"
-
-#ifndef CVC4__PRINTER__DAGIFICATION_VISITOR_H
-#define CVC4__PRINTER__DAGIFICATION_VISITOR_H
-
-#include <string>
-#include <unordered_map>
-#include <unordered_set>
-#include <vector>
-
-#include "expr/node.h"
-#include "util/hash.h"
-
-namespace CVC4 {
-
-namespace context {
- class Context;
-}/* CVC4::context namespace */
-
-namespace theory {
- class SubstitutionMap;
-}/* CVC4::theory namespace */
-
-namespace printer {
-
-/**
- * This is a visitor class (intended to be used with CVC4's NodeVisitor)
- * that visits an expression looking for common subexpressions that appear
- * more than N times, where N is a configurable threshold. Afterward,
- * let bindings can be extracted from this visitor and applied to the
- * expression.
- *
- * This dagifier never introduces let bindings for variables, constants,
- * unary-minus exprs over variables or constants, or NOT exprs over
- * variables or constants. This dagifier never introduces let bindings
- * for types.
- */
-class DagificationVisitor {
-
- /**
- * The threshold for dagification. Subexprs occurring more than this
- * number of times are dagified.
- */
- const unsigned d_threshold;
-
- /**
- * The prefix for introduced let bindings.
- */
- const std::string d_letVarPrefix;
-
- /**
- * A map of subexprs to their occurrence count.
- */
- std::unordered_map<TNode, unsigned, TNodeHashFunction> d_nodeCount;
-
- /**
- * The set of variable names with the let prefix that appear in the
- * expression.
- */
- std::unordered_set<std::string> d_reservedLetNames;
-
- /**
- * The top-most node we are visiting.
- */
- TNode d_top;
-
- /**
- * This class doesn't operate in a context-dependent fashion, but
- * SubstitutionMap does, so we need a context.
- */
- context::Context* d_context;
-
- /**
- * A map of subexprs to their newly-introduced let bindings.
- */
- theory::SubstitutionMap* d_substitutions;
-
- /**
- * The current count of let bindings. Used to build unique names
- * for the bindings.
- */
- unsigned d_letVar;
-
- /**
- * Keep track of whether we are done yet (for assertions---this visitor
- * can only be used one time).
- */
- bool d_done;
-
- /**
- * If a subexpr occurs uniquely in one parent expr, this map points to
- * it. An expr not occurring as a key in this map means we haven't
- * seen it yet (and its occurrence count should be zero). If an expr
- * points to the null expr in this map, it means we've seen more than
- * one parent, so the subexpr doesn't have a unique parent.
- *
- * This information is kept because if a subexpr occurs more than the
- * threshold, it is normally subject to dagification. But if it occurs
- * only in one unique parent expression, and the parent meets the
- * threshold too, then the parent will be dagified and there's no point
- * in independently dagifying the child. (If it is beyond the threshold
- * and occurs in more than one parent, we'll independently dagify.)
- */
- std::unordered_map<TNode, TNode, TNodeHashFunction> d_uniqueParent;
-
- /**
- * A list of all nodes that meet the occurrence threshold and therefore
- * *may* be subject to dagification, except for the unique-parent rule
- * mentioned above.
- */
- std::vector<TNode> d_substNodes;
-
-public:
-
- /** Our visitor doesn't return anything. */
- typedef void return_type;
-
- /**
- * Construct a dagification visitor with the given threshold and let
- * binding prefix.
- *
- * @param threshold the threshold to apply for dagification (must be > 0)
- * @param letVarPrefix prefix for let bindings (by default, "_let_")
- */
- DagificationVisitor(unsigned threshold, std::string letVarPrefix = "_let_");
-
- /**
- * Simple destructor, clean up memory.
- */
- ~DagificationVisitor();
-
- /**
- * Returns true if "current" has already been visited a sufficient
- * number of times to make it a candidate for dagification, or if
- * it cannot ever be subject to dagification.
- */
- bool alreadyVisited(TNode current, TNode parent);
-
- /**
- * Visit the expr "current", it might be a candidate for a let binder.
- */
- void visit(TNode current, TNode parent);
-
- /**
- * Marks the node as the starting literal.
- */
- void start(TNode node);
-
- /**
- * Called when we're done with all visitation. Does postprocessing.
- */
- void done(TNode node);
-
- /**
- * Get the let substitutions.
- */
- const theory::SubstitutionMap& getLets();
-
- /**
- * Return the let-substituted expression.
- */
- Node getDagifiedBody();
-
-};/* class DagificationVisitor */
-
-}/* CVC4::printer namespace */
-}/* CVC4 namespace */
-
-#endif /* CVC4__PRINTER__DAGIFICATION_VISITOR_H */
projects / cvc5.git / commitdiff