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     if(!uniqueParent.isNull() && uniqueParent != parent) {
 110       // there is not a unique parent for this expr, mark it
 111       uniqueParent = TNode::null();
 112     }
 113
 114     // increase the count
 115     const unsigned count = ++d_nodeCount[current];
 116
 117     if(count > d_threshold) {
 118       // candidate for a let binder
 119       d_substNodes.push_back(current);
 120     }
 121   } else {
 122     // we haven't seen this expr before
 123     Assert(d_nodeCount[current] == 0);
 124     d_nodeCount[current] = 1;
 125     d_uniqueParent[current] = parent;
 126   }
 127 }
 128
 129 void DagificationVisitor::start(TNode node) {
 130   AlwaysAssert(!d_done, "DagificationVisitor cannot be re-used");
 131   d_top = node;
 132 }
 133
 134 void DagificationVisitor::done(TNode node) {
 135   AlwaysAssert(!d_done);
 136
 137   d_done = true;
 138
 139 #ifdef CVC4_TRACING
 140 #  ifdef CVC4_DEBUG
 141   // turn off dagification for Debug stream while we're doing this work
 142   Node::dag::Scope scopeDebug(Debug.getStream(), false);
 143 #  endif /* CVC4_DEBUG */
 144   // turn off dagification for Trace stream while we're doing this work
 145   Node::dag::Scope scopeTrace(Trace.getStream(), false);
 146 #endif /* CVC4_TRACING */
 147
 148   // letify subexprs before parents (cascading LETs)
 149   std::sort(d_substNodes.begin(), d_substNodes.end());
 150
 151   for(std::vector<TNode>::iterator i = d_substNodes.begin();
 152       i != d_substNodes.end();
 153       ++i) {
 154     Assert(d_nodeCount[*i] > d_threshold);
 155     TNode parent = d_uniqueParent[*i];
 156     if(!parent.isNull() && d_nodeCount[parent] > d_threshold) {
 157       // no need to letify this expr, because it only occurs in
 158       // a single super-expression, and that one will be letified
 159       continue;
 160     }
 161
 162     // construct the let binder
 163     std::stringstream ss;
 164     do
 165     {
 166       ss.str("");
 167       ss << d_letVarPrefix << d_letVar++;
 168     } while (d_reservedLetNames.find(ss.str()) != d_reservedLetNames.end());
 169     Node letvar = NodeManager::currentNM()->mkSkolem(ss.str(), (*i).getType(), "dagification", NodeManager::SKOLEM_NO_NOTIFY | NodeManager::SKOLEM_EXACT_NAME);
 170
 171     // apply previous substitutions to the rhs, enabling cascading LETs
 172     Node n = d_substitutions->apply(*i);
 173     Assert(! d_substitutions->hasSubstitution(n));
 174     d_substitutions->addSubstitution(n, letvar);
 175   }
 176 }
 177
 178 const theory::SubstitutionMap& DagificationVisitor::getLets() {
 179   AlwaysAssert(d_done, "DagificationVisitor must be used as a visitor before getting the dagified version out!");
 180   return *d_substitutions;
 181 }
 182
 183 Node DagificationVisitor::getDagifiedBody() {
 184   AlwaysAssert(d_done, "DagificationVisitor must be used as a visitor before getting the dagified version out!");
 185
 186 #ifdef CVC4_TRACING
 187 #  ifdef CVC4_DEBUG
 188   // turn off dagification for Debug stream while we're doing this work
 189   Node::dag::Scope scopeDebug(Debug.getStream(), false);
 190 #  endif /* CVC4_DEBUG */
 191   // turn off dagification for Trace stream while we're doing this work
 192   Node::dag::Scope scopeTrace(Trace.getStream(), false);
 193 #endif /* CVC4_TRACING */
 194
 195   return d_substitutions->apply(d_top);
 196 }
 197
 198 }/* CVC4::printer namespace */
 199 }/* CVC4 namespace */