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 "theory/substitutions.h"
  21
  22 #include <sstream>
  23
  24 namespace CVC4 {
  25 namespace printer {
  26
  27 DagificationVisitor::DagificationVisitor(unsigned threshold, std::string letVarPrefix) :
  28   d_threshold(threshold),
  29   d_letVarPrefix(letVarPrefix),
  30   d_nodeCount(),
  31   d_top(),
  32   d_context(new context::Context()),
  33   d_substitutions(new theory::SubstitutionMap(d_context)),
  34   d_letVar(0),
  35   d_done(false),
  36   d_uniqueParent(),
  37   d_substNodes() {
  38
  39   // 0 doesn't make sense
  40   AlwaysAssertArgument(threshold > 0, threshold);
  41 }
  42
  43 DagificationVisitor::~DagificationVisitor() {
  44   delete d_substitutions;
  45   delete d_context;
  46 }
  47
  48 bool DagificationVisitor::alreadyVisited(TNode current, TNode parent) {
  49   Kind ck = current.getKind();
  50   if (ck == kind::FORALL || ck == kind::EXISTS || ck == kind::LAMBDA
  51       || ck == kind::CHOICE)
  52   {
  53     // for quantifiers, we visit them but we don't recurse on them
  54     visit(current, parent);
  55     return true;
  56   }
  57   // don't visit variables, constants, or those exprs that we've
  58   // already seen more than the threshold: if we've increased
  59   // the count beyond the threshold already, we've done the same
  60   // for all subexpressions, so it isn't useful to traverse and
  61   // increment again (they'll be dagified anyway).
  62   return current.isVar() || current.getMetaKind() == kind::metakind::CONSTANT
  63          || current.getNumChildren() == 0
  64          || ((ck == kind::NOT || ck == kind::UMINUS)
  65              && (current[0].isVar()
  66                  || current[0].getMetaKind() == kind::metakind::CONSTANT))
  67          || ck == kind::SORT_TYPE || d_nodeCount[current] > d_threshold;
  68 }
  69
  70 void DagificationVisitor::visit(TNode current, TNode parent) {
  71
  72 #ifdef CVC4_TRACING
  73 #  ifdef CVC4_DEBUG
  74   // turn off dagification for Debug stream while we're doing this work
  75   Node::dag::Scope scopeDebug(Debug.getStream(), false);
  76 #  endif /* CVC4_DEBUG */
  77   // turn off dagification for Trace stream while we're doing this work
  78   Node::dag::Scope scopeTrace(Trace.getStream(), false);
  79 #endif /* CVC4_TRACING */
  80
  81   if(d_uniqueParent.find(current) != d_uniqueParent.end()) {
  82     // we've seen this expr before
  83
  84     TNode& uniqueParent = d_uniqueParent[current];
  85
  86     if(!uniqueParent.isNull() && uniqueParent != parent) {
  87       // there is not a unique parent for this expr, mark it
  88       uniqueParent = TNode::null();
  89     }
  90
  91     // increase the count
  92     const unsigned count = ++d_nodeCount[current];
  93
  94     if(count > d_threshold) {
  95       // candidate for a let binder
  96       d_substNodes.push_back(current);
  97     }
  98   } else {
  99     // we haven't seen this expr before
 100     Assert(d_nodeCount[current] == 0);
 101     d_nodeCount[current] = 1;
 102     d_uniqueParent[current] = parent;
 103   }
 104 }
 105
 106 void DagificationVisitor::start(TNode node) {
 107   AlwaysAssert(!d_done, "DagificationVisitor cannot be re-used");
 108   d_top = node;
 109 }
 110
 111 void DagificationVisitor::done(TNode node) {
 112   AlwaysAssert(!d_done);
 113
 114   d_done = true;
 115
 116 #ifdef CVC4_TRACING
 117 #  ifdef CVC4_DEBUG
 118   // turn off dagification for Debug stream while we're doing this work
 119   Node::dag::Scope scopeDebug(Debug.getStream(), false);
 120 #  endif /* CVC4_DEBUG */
 121   // turn off dagification for Trace stream while we're doing this work
 122   Node::dag::Scope scopeTrace(Trace.getStream(), false);
 123 #endif /* CVC4_TRACING */
 124
 125   // letify subexprs before parents (cascading LETs)
 126   std::sort(d_substNodes.begin(), d_substNodes.end());
 127
 128   for(std::vector<TNode>::iterator i = d_substNodes.begin();
 129       i != d_substNodes.end();
 130       ++i) {
 131     Assert(d_nodeCount[*i] > d_threshold);
 132     TNode parent = d_uniqueParent[*i];
 133     if(!parent.isNull() && d_nodeCount[parent] > d_threshold) {
 134       // no need to letify this expr, because it only occurs in
 135       // a single super-expression, and that one will be letified
 136       continue;
 137     }
 138
 139     // construct the let binder
 140     std::stringstream ss;
 141     ss << d_letVarPrefix << d_letVar++;
 142     Node letvar = NodeManager::currentNM()->mkSkolem(ss.str(), (*i).getType(), "dagification", NodeManager::SKOLEM_NO_NOTIFY | NodeManager::SKOLEM_EXACT_NAME);
 143
 144     // apply previous substitutions to the rhs, enabling cascading LETs
 145     Node n = d_substitutions->apply(*i);
 146     Assert(! d_substitutions->hasSubstitution(n));
 147     d_substitutions->addSubstitution(n, letvar);
 148   }
 149 }
 150
 151 const theory::SubstitutionMap& DagificationVisitor::getLets() {
 152   AlwaysAssert(d_done, "DagificationVisitor must be used as a visitor before getting the dagified version out!");
 153   return *d_substitutions;
 154 }
 155
 156 Node DagificationVisitor::getDagifiedBody() {
 157   AlwaysAssert(d_done, "DagificationVisitor must be used as a visitor before getting the dagified version out!");
 158
 159 #ifdef CVC4_TRACING
 160 #  ifdef CVC4_DEBUG
 161   // turn off dagification for Debug stream while we're doing this work
 162   Node::dag::Scope scopeDebug(Debug.getStream(), false);
 163 #  endif /* CVC4_DEBUG */
 164   // turn off dagification for Trace stream while we're doing this work
 165   Node::dag::Scope scopeTrace(Trace.getStream(), false);
 166 #endif /* CVC4_TRACING */
 167
 168   return d_substitutions->apply(d_top);
 169 }
 170
 171 }/* CVC4::printer namespace */
 172 }/* CVC4 namespace */