Remove dagification visitor (#5574)

This has fully been replaced by the new let binding.

4 files changed, 0 insertions, 396 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index e56379f0c..4b5c37d9e 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -122,8 +122,6 @@ libcvc4_add_sources(
   printer/ast/ast_printer.h
   printer/cvc/cvc_printer.cpp
   printer/cvc/cvc_printer.h
-  printer/dagification_visitor.cpp
-  printer/dagification_visitor.h
   printer/let_binding.cpp
   printer/let_binding.h
   printer/printer.cpp
diff --git a/src/printer/dagification_visitor.cpp b/src/printer/dagification_visitor.cpp
deleted file mode 100644
index 89fbe786d..000000000
--- a/src/printer/dagification_visitor.cpp
+++ /dev/null
@@ -1,208 +0,0 @@
-/*********************                                                        */
-/*! \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 */
diff --git a/src/printer/dagification_visitor.h b/src/printer/dagification_visitor.h
deleted file mode 100644
index 7c6f57af8..000000000
--- a/src/printer/dagification_visitor.h
+++ /dev/null
@@ -1,185 +0,0 @@
-/*********************                                                        */
-/*! \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 */
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index d3e9b48e4..6f03553ae 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -30,7 +30,6 @@
 #include "options/language.h"
 #include "options/printer_options.h"
 #include "options/smt_options.h"
-#include "printer/dagification_visitor.h"
 #include "printer/let_binding.h"
 #include "proof/unsat_core.h"
 #include "smt/command.h"