src/printer/dagification_visitor.cpp

   1 /*********************                                                        */
   2 /*! \file dagification_visitor.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Morgan Deters, Tim King, Andrew Reynolds
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2016 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   // don't visit variables, constants, or those exprs that we've
  50   // already seen more than the threshold: if we've increased
  51   // the count beyond the threshold already, we've done the same
  52   // for all subexpressions, so it isn't useful to traverse and
  53   // increment again (they'll be dagified anyway).
  54   return current.isVar() ||
  55          current.getMetaKind() == kind::metakind::CONSTANT ||
  56          current.getNumChildren()==0 ||
  57          ( ( current.getKind() == kind::NOT ||
  58              current.getKind() == kind::UMINUS ) &&
  59            ( current[0].isVar() ||
  60              current[0].getMetaKind() == kind::metakind::CONSTANT ) ) ||
  61          current.getKind() == kind::SORT_TYPE ||
  62          d_nodeCount[current] > d_threshold;
  63 }
  64
  65 void DagificationVisitor::visit(TNode current, TNode parent) {
  66
  67 #ifdef CVC4_TRACING
  68 #  ifdef CVC4_DEBUG
  69   // turn off dagification for Debug stream while we're doing this work
  70   Node::dag::Scope scopeDebug(Debug.getStream(), false);
  71 #  endif /* CVC4_DEBUG */
  72   // turn off dagification for Trace stream while we're doing this work
  73   Node::dag::Scope scopeTrace(Trace.getStream(), false);
  74 #endif /* CVC4_TRACING */
  75
  76   if(d_uniqueParent.find(current) != d_uniqueParent.end()) {
  77     // we've seen this expr before
  78
  79     TNode& uniqueParent = d_uniqueParent[current];
  80
  81     if(!uniqueParent.isNull() && uniqueParent != parent) {
  82       // there is not a unique parent for this expr, mark it
  83       uniqueParent = TNode::null();
  84     }
  85
  86     // increase the count
  87     const unsigned count = ++d_nodeCount[current];
  88
  89     if(count > d_threshold) {
  90       // candidate for a let binder
  91       d_substNodes.push_back(current);
  92     }
  93   } else {
  94     // we haven't seen this expr before
  95     Assert(d_nodeCount[current] == 0);
  96     d_nodeCount[current] = 1;
  97     d_uniqueParent[current] = parent;
  98   }
  99 }
 100
 101 void DagificationVisitor::start(TNode node) {
 102   AlwaysAssert(!d_done, "DagificationVisitor cannot be re-used");
 103   d_top = node;
 104 }
 105
 106 void DagificationVisitor::done(TNode node) {
 107   AlwaysAssert(!d_done);
 108
 109   d_done = true;
 110
 111 #ifdef CVC4_TRACING
 112 #  ifdef CVC4_DEBUG
 113   // turn off dagification for Debug stream while we're doing this work
 114   Node::dag::Scope scopeDebug(Debug.getStream(), false);
 115 #  endif /* CVC4_DEBUG */
 116   // turn off dagification for Trace stream while we're doing this work
 117   Node::dag::Scope scopeTrace(Trace.getStream(), false);
 118 #endif /* CVC4_TRACING */
 119
 120   // letify subexprs before parents (cascading LETs)
 121   std::sort(d_substNodes.begin(), d_substNodes.end());
 122
 123   for(std::vector<TNode>::iterator i = d_substNodes.begin();
 124       i != d_substNodes.end();
 125       ++i) {
 126     Assert(d_nodeCount[*i] > d_threshold);
 127     TNode parent = d_uniqueParent[*i];
 128     if(!parent.isNull() && d_nodeCount[parent] > d_threshold) {
 129       // no need to letify this expr, because it only occurs in
 130       // a single super-expression, and that one will be letified
 131       continue;
 132     }
 133
 134     // construct the let binder
 135     std::stringstream ss;
 136     ss << d_letVarPrefix << d_letVar++;
 137     Node letvar = NodeManager::currentNM()->mkSkolem(ss.str(), (*i).getType(), "dagification", NodeManager::SKOLEM_NO_NOTIFY | NodeManager::SKOLEM_EXACT_NAME);
 138
 139     // apply previous substitutions to the rhs, enabling cascading LETs
 140     Node n = d_substitutions->apply(*i);
 141     Assert(! d_substitutions->hasSubstitution(n));
 142     d_substitutions->addSubstitution(n, letvar);
 143   }
 144 }
 145
 146 const theory::SubstitutionMap& DagificationVisitor::getLets() {
 147   AlwaysAssert(d_done, "DagificationVisitor must be used as a visitor before getting the dagified version out!");
 148   return *d_substitutions;
 149 }
 150
 151 Node DagificationVisitor::getDagifiedBody() {
 152   AlwaysAssert(d_done, "DagificationVisitor must be used as a visitor before getting the dagified version out!");
 153
 154 #ifdef CVC4_TRACING
 155 #  ifdef CVC4_DEBUG
 156   // turn off dagification for Debug stream while we're doing this work
 157   Node::dag::Scope scopeDebug(Debug.getStream(), false);
 158 #  endif /* CVC4_DEBUG */
 159   // turn off dagification for Trace stream while we're doing this work
 160   Node::dag::Scope scopeTrace(Trace.getStream(), false);
 161 #endif /* CVC4_TRACING */
 162
 163   return d_substitutions->apply(d_top);
 164 }
 165
 166 }/* CVC4::printer namespace */
 167 }/* CVC4 namespace */