src/printer/dagification_visitor.h

   1 /*********************                                                        */
   2 /*! \file dagification_visitor.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Morgan Deters, Andres Noetzli, Mathias Preiner
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
   8  ** in the top-level source directory) and their institutional affiliations.
   9  ** All rights reserved.  See the file COPYING in the top-level source
  10  ** directory for licensing information.\endverbatim
  11  **
  12  ** \brief A dagifier for CVC4 expressions
  13  **
  14  ** A dagifier for CVC4 expressions.
  15  **/
  16
  17 #include "cvc4_private.h"
  18
  19 #ifndef CVC4__PRINTER__DAGIFICATION_VISITOR_H
  20 #define CVC4__PRINTER__DAGIFICATION_VISITOR_H
  21
  22 #include <string>
  23 #include <unordered_map>
  24 #include <unordered_set>
  25 #include <vector>
  26
  27 #include "expr/node.h"
  28 #include "util/hash.h"
  29
  30 namespace CVC4 {
  31
  32 namespace context {
  33   class Context;
  34 }/* CVC4::context namespace */
  35
  36 namespace theory {
  37   class SubstitutionMap;
  38 }/* CVC4::theory namespace */
  39
  40 namespace printer {
  41
  42 /**
  43  * This is a visitor class (intended to be used with CVC4's NodeVisitor)
  44  * that visits an expression looking for common subexpressions that appear
  45  * more than N times, where N is a configurable threshold.  Afterward,
  46  * let bindings can be extracted from this visitor and applied to the
  47  * expression.
  48  *
  49  * This dagifier never introduces let bindings for variables, constants,
  50  * unary-minus exprs over variables or constants, or NOT exprs over
  51  * variables or constants.  This dagifier never introduces let bindings
  52  * for types.
  53  */
  54 class DagificationVisitor {
  55
  56   /**
  57    * The threshold for dagification.  Subexprs occurring more than this
  58    * number of times are dagified.
  59    */
  60   const unsigned d_threshold;
  61
  62   /**
  63    * The prefix for introduced let bindings.
  64    */
  65   const std::string d_letVarPrefix;
  66
  67   /**
  68    * A map of subexprs to their occurrence count.
  69    */
  70   std::unordered_map<TNode, unsigned, TNodeHashFunction> d_nodeCount;
  71
  72   /**
  73    * The set of variable names with the let prefix that appear in the
  74    * expression.
  75    */
  76   std::unordered_set<std::string> d_reservedLetNames;
  77
  78   /**
  79    * The top-most node we are visiting.
  80    */
  81   TNode d_top;
  82
  83   /**
  84    * This class doesn't operate in a context-dependent fashion, but
  85    * SubstitutionMap does, so we need a context.
  86    */
  87   context::Context* d_context;
  88
  89   /**
  90    * A map of subexprs to their newly-introduced let bindings.
  91    */
  92   theory::SubstitutionMap* d_substitutions;
  93
  94   /**
  95    * The current count of let bindings.  Used to build unique names
  96    * for the bindings.
  97    */
  98   unsigned d_letVar;
  99
 100   /**
 101    * Keep track of whether we are done yet (for assertions---this visitor
 102    * can only be used one time).
 103    */
 104   bool d_done;
 105
 106   /**
 107    * If a subexpr occurs uniquely in one parent expr, this map points to
 108    * it.  An expr not occurring as a key in this map means we haven't
 109    * seen it yet (and its occurrence count should be zero).  If an expr
 110    * points to the null expr in this map, it means we've seen more than
 111    * one parent, so the subexpr doesn't have a unique parent.
 112    *
 113    * This information is kept because if a subexpr occurs more than the
 114    * threshold, it is normally subject to dagification.  But if it occurs
 115    * only in one unique parent expression, and the parent meets the
 116    * threshold too, then the parent will be dagified and there's no point
 117    * in independently dagifying the child.  (If it is beyond the threshold
 118    * and occurs in more than one parent, we'll independently dagify.)
 119    */
 120   std::unordered_map<TNode, TNode, TNodeHashFunction> d_uniqueParent;
 121
 122   /**
 123    * A list of all nodes that meet the occurrence threshold and therefore
 124    * *may* be subject to dagification, except for the unique-parent rule
 125    * mentioned above.
 126    */
 127   std::vector<TNode> d_substNodes;
 128
 129 public:
 130
 131   /** Our visitor doesn't return anything. */
 132   typedef void return_type;
 133
 134   /**
 135    * Construct a dagification visitor with the given threshold and let
 136    * binding prefix.
 137    *
 138    * @param threshold the threshold to apply for dagification (must be > 0)
 139    * @param letVarPrefix prefix for let bindings (by default, "_let_")
 140    */
 141   DagificationVisitor(unsigned threshold, std::string letVarPrefix = "_let_");
 142
 143   /**
 144    * Simple destructor, clean up memory.
 145    */
 146   ~DagificationVisitor();
 147
 148   /**
 149    * Returns true if "current" has already been visited a sufficient
 150    * number of times to make it a candidate for dagification, or if
 151    * it cannot ever be subject to dagification.
 152    */
 153   bool alreadyVisited(TNode current, TNode parent);
 154
 155   /**
 156    * Visit the expr "current", it might be a candidate for a let binder.
 157    */
 158   void visit(TNode current, TNode parent);
 159
 160   /**
 161    * Marks the node as the starting literal.
 162    */
 163   void start(TNode node);
 164
 165   /**
 166    * Called when we're done with all visitation.  Does postprocessing.
 167    */
 168   void done(TNode node);
 169
 170   /**
 171    * Get the let substitutions.
 172    */
 173   const theory::SubstitutionMap& getLets();
 174
 175   /**
 176    * Return the let-substituted expression.
 177    */
 178   Node getDagifiedBody();
 179
 180 };/* class DagificationVisitor */
 181
 182 }/* CVC4::printer namespace */
 183 }/* CVC4 namespace */
 184
 185 #endif /* CVC4__PRINTER__DAGIFICATION_VISITOR_H */