src/printer/dagification_visitor.cpp

   1 /*********************                                                        */
   2 /*! \file dagification_visitor.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Morgan Deters, Andrew Reynolds
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2019 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 Implementation of a dagifier for CVC4 expressions
  13  **
  14  ** Implementation of a dagifier for CVC4 expressions.
  15  **/
  16
  17 #include "printer/dagification_visitor.h"
  18
  19 #include "context/context.h"
  20 #include "expr/node_algorithm.h"
  21 #include "expr/node_manager_attributes.h"
  22 #include "theory/substitutions.h"
  23
  24 #include <sstream>
  25
  26 namespace CVC4 {
  27 namespace printer {
  28
  29 DagificationVisitor::DagificationVisitor(unsigned threshold,
  30                                          std::string letVarPrefix)
  31     : d_threshold(threshold),
  32       d_letVarPrefix(letVarPrefix),
  33       d_nodeCount(),
  34       d_reservedLetNames(),
  35       d_top(),
  36       d_context(new context::Context()),
  37       d_substitutions(new theory::SubstitutionMap(d_context)),
  38       d_letVar(0),
  39       d_done(false),
  40       d_uniqueParent(),
  41       d_substNodes()
  42 {
  43   // 0 doesn't make sense
  44   AlwaysAssertArgument(threshold > 0, threshold);
  45 }
  46
  47 DagificationVisitor::~DagificationVisitor() {
  48   delete d_substitutions;
  49   delete d_context;
  50 }
  51
  52 bool DagificationVisitor::alreadyVisited(TNode current, TNode parent) {
  53   Kind ck = current.getKind();
  54   if (current.isClosure())
  55   {
  56     // for quantifiers, we visit them but we don't recurse on them
  57     visit(current, parent);
  58
  59     // search for variables that start with the let prefix
  60     std::unordered_set<TNode, TNodeHashFunction> vs;
  61     expr::getVariables(current, vs);
  62     for (const TNode v : vs)
  63     {
  64       const std::string name = v.getAttribute(expr::VarNameAttr());
  65       if (name.compare(0, d_letVarPrefix.size(), d_letVarPrefix) == 0)
  66       {
  67         d_reservedLetNames.insert(name);
  68       }
  69     }
  70     return true;
  71   }
  72   else if (current.isVar())
  73   {
  74     const std::string name = current.getAttribute(expr::VarNameAttr());
  75     if (name.compare(0, d_letVarPrefix.size(), d_letVarPrefix) == 0)
  76     {
  77       d_reservedLetNames.insert(name);
  78     }
  79   }
  80   // don't visit variables, constants, or those exprs that we've
  81   // already seen more than the threshold: if we've increased
  82   // the count beyond the threshold already, we've done the same
  83   // for all subexpressions, so it isn't useful to traverse and
  84   // increment again (they'll be dagified anyway).
  85   return current.isVar() || current.getMetaKind() == kind::metakind::CONSTANT
  86          || current.getNumChildren() == 0
  87          || ((ck == kind::NOT || ck == kind::UMINUS)
  88              && (current[0].isVar()
  89                  || current[0].getMetaKind() == kind::metakind::CONSTANT))
  90          || ck == kind::SORT_TYPE || d_nodeCount[current] > d_threshold;
  91 }
  92
  93 void DagificationVisitor::visit(TNode current, TNode parent) {
  94
  95 #ifdef CVC4_TRACING
  96 #  ifdef CVC4_DEBUG
  97   // turn off dagification for Debug stream while we're doing this work
  98   Node::dag::Scope scopeDebug(Debug.getStream(), false);
  99 #  endif /* CVC4_DEBUG */
 100   // turn off dagification for Trace stream while we're doing this work
 101   Node::dag::Scope scopeTrace(Trace.getStream(), false);
 102 #endif /* CVC4_TRACING */
 103
 104   if(d_uniqueParent.find(current) != d_uniqueParent.end()) {
 105     // we've seen this expr before
 106
 107     TNode& uniqueParent = d_uniqueParent[current];
 108
 109     // We restrict this optimization to nodes with arity 1 since otherwise we
 110     // may run into issues with tree traverals. Without this restriction
 111     // dumping regress3/pp-regfile increases the file size by a factor of 5000.
 112     if (!uniqueParent.isNull()
 113         && (uniqueParent != parent || parent.getNumChildren() > 1))
 114     {
 115       // there is not a unique parent for this expr, mark it
 116       uniqueParent = TNode::null();
 117     }
 118
 119     // increase the count
 120     const unsigned count = ++d_nodeCount[current];
 121
 122     if(count > d_threshold) {
 123       // candidate for a let binder
 124       d_substNodes.push_back(current);
 125     }
 126   } else {
 127     // we haven't seen this expr before
 128     Assert(d_nodeCount[current] == 0);
 129     d_nodeCount[current] = 1;
 130     d_uniqueParent[current] = parent;
 131   }
 132 }
 133
 134 void DagificationVisitor::start(TNode node) {
 135   AlwaysAssert(!d_done) << "DagificationVisitor cannot be re-used";
 136   d_top = node;
 137 }
 138
 139 void DagificationVisitor::done(TNode node) {
 140   AlwaysAssert(!d_done);
 141
 142   d_done = true;
 143
 144 #ifdef CVC4_TRACING
 145 #  ifdef CVC4_DEBUG
 146   // turn off dagification for Debug stream while we're doing this work
 147   Node::dag::Scope scopeDebug(Debug.getStream(), false);
 148 #  endif /* CVC4_DEBUG */
 149   // turn off dagification for Trace stream while we're doing this work
 150   Node::dag::Scope scopeTrace(Trace.getStream(), false);
 151 #endif /* CVC4_TRACING */
 152
 153   // letify subexprs before parents (cascading LETs)
 154   std::sort(d_substNodes.begin(), d_substNodes.end());
 155
 156   for(std::vector<TNode>::iterator i = d_substNodes.begin();
 157       i != d_substNodes.end();
 158       ++i) {
 159     Assert(d_nodeCount[*i] > d_threshold);
 160     TNode parent = d_uniqueParent[*i];
 161     if(!parent.isNull() && d_nodeCount[parent] > d_threshold) {
 162       // no need to letify this expr, because it only occurs in
 163       // a single super-expression, and that one will be letified
 164       continue;
 165     }
 166
 167     // construct the let binder
 168     std::stringstream ss;
 169     do
 170     {
 171       ss.str("");
 172       ss << d_letVarPrefix << d_letVar++;
 173     } while (d_reservedLetNames.find(ss.str()) != d_reservedLetNames.end());
 174     Node letvar = NodeManager::currentNM()->mkSkolem(ss.str(), (*i).getType(), "dagification", NodeManager::SKOLEM_NO_NOTIFY | NodeManager::SKOLEM_EXACT_NAME);
 175
 176     // apply previous substitutions to the rhs, enabling cascading LETs
 177     Node n = d_substitutions->apply(*i);
 178     Assert(!d_substitutions->hasSubstitution(n));
 179     d_substitutions->addSubstitution(n, letvar);
 180   }
 181 }
 182
 183 const theory::SubstitutionMap& DagificationVisitor::getLets() {
 184   AlwaysAssert(d_done)
 185       << "DagificationVisitor must be used as a visitor before "
 186          "getting the dagified version out!";
 187   return *d_substitutions;
 188 }
 189
 190 Node DagificationVisitor::getDagifiedBody() {
 191   AlwaysAssert(d_done)
 192       << "DagificationVisitor must be used as a visitor before "
 193          "getting the dagified version out!";
 194
 195 #ifdef CVC4_TRACING
 196 #  ifdef CVC4_DEBUG
 197   // turn off dagification for Debug stream while we're doing this work
 198   Node::dag::Scope scopeDebug(Debug.getStream(), false);
 199 #  endif /* CVC4_DEBUG */
 200   // turn off dagification for Trace stream while we're doing this work
 201   Node::dag::Scope scopeTrace(Trace.getStream(), false);
 202 #endif /* CVC4_TRACING */
 203
 204   return d_substitutions->apply(d_top);
 205 }
 206
 207 }/* CVC4::printer namespace */
 208 }/* CVC4 namespace */