src/printer/dagification_visitor.cpp

   1 /*********************                                                        */
   2 /*! \file dagification_visitor.cpp
   3  ** \verbatim
   4  ** Original author: mdeters
   5  ** Major contributors: none
   6  ** Minor contributors (to current version): none
   7  ** This file is part of the CVC4 prototype.
   8  ** Copyright (c) 2009, 2010, 2011, 2012  The Analysis of Computer Systems Group (ACSys)
   9  ** Courant Institute of Mathematical Sciences
  10  ** New York University
  11  ** See the file COPYING in the top-level source directory for licensing
  12  ** information.\endverbatim
  13  **
  14  ** \brief Implementation of a dagifier for CVC4 expressions
  15  **
  16  ** Implementation of a dagifier for CVC4 expressions.
  17  **/
  18
  19 #include "printer/dagification_visitor.h"
  20
  21 #include "context/context.h"
  22 #include "theory/substitutions.h"
  23
  24 #include <sstream>
  25
  26 namespace CVC4 {
  27 namespace printer {
  28
  29 DagificationVisitor::DagificationVisitor(unsigned threshold, std::string letVarPrefix) :
  30   d_threshold(threshold),
  31   d_letVarPrefix(letVarPrefix),
  32   d_nodeCount(),
  33   d_top(),
  34   d_context(new context::Context()),
  35   d_substitutions(new theory::SubstitutionMap(d_context)),
  36   d_letVar(0),
  37   d_done(false),
  38   d_uniqueParent(),
  39   d_substNodes() {
  40
  41   // 0 doesn't make sense
  42   CheckArgument(threshold > 0, threshold);
  43 }
  44
  45 DagificationVisitor::~DagificationVisitor() {
  46   delete d_substitutions;
  47   delete d_context;
  48 }
  49
  50 bool DagificationVisitor::alreadyVisited(TNode current, TNode parent) {
  51   // don't visit variables, constants, or those exprs that we've
  52   // already seen more than the threshold: if we've increased
  53   // the count beyond the threshold already, we've done the same
  54   // for all subexpressions, so it isn't useful to traverse and
  55   // increment again (they'll be dagified anyway).
  56   return current.isVar() ||
  57          current.isConst() ||
  58          ( ( current.getKind() == kind::NOT ||
  59              current.getKind() == kind::UMINUS ) &&
  60            ( current[0].isVar() ||
  61              current[0].isConst() ) ) ||
  62          current.getKind() == kind::SORT_TYPE ||
  63          d_nodeCount[current] > d_threshold;
  64 }
  65
  66 void DagificationVisitor::visit(TNode current, TNode parent) {
  67
  68 #ifdef CVC4_TRACING
  69 #  ifdef CVC4_DEBUG
  70   // turn off dagification for Debug stream while we're doing this work
  71   Node::dag::Scope scopeDebug(Debug.getStream(), false);
  72 #  endif /* CVC4_DEBUG */
  73   // turn off dagification for Trace stream while we're doing this work
  74   Node::dag::Scope scopeTrace(Trace.getStream(), false);
  75 #endif /* CVC4_TRACING */
  76
  77   if(d_uniqueParent.find(current) != d_uniqueParent.end()) {
  78     // we've seen this expr before
  79
  80     TNode& uniqueParent = d_uniqueParent[current];
  81
  82     if(!uniqueParent.isNull() && uniqueParent != parent) {
  83       // there is not a unique parent for this expr, mark it
  84       uniqueParent = TNode::null();
  85     }
  86
  87     // increase the count
  88     const unsigned count = ++d_nodeCount[current];
  89
  90     if(count > d_threshold) {
  91       // candidate for a let binder
  92       d_substNodes.push_back(current);
  93     }
  94   } else {
  95     // we haven't seen this expr before
  96     Assert(d_nodeCount[current] == 0);
  97     d_nodeCount[current] = 1;
  98     d_uniqueParent[current] = parent;
  99   }
 100 }
 101
 102 void DagificationVisitor::start(TNode node) {
 103   AlwaysAssert(!d_done, "DagificationVisitor cannot be re-used");
 104   d_top = node;
 105 }
 106
 107 void DagificationVisitor::done(TNode node) {
 108   AlwaysAssert(!d_done);
 109
 110   d_done = true;
 111
 112 #ifdef CVC4_TRACING
 113 #  ifdef CVC4_DEBUG
 114   // turn off dagification for Debug stream while we're doing this work
 115   Node::dag::Scope scopeDebug(Debug.getStream(), false);
 116 #  endif /* CVC4_DEBUG */
 117   // turn off dagification for Trace stream while we're doing this work
 118   Node::dag::Scope scopeTrace(Trace.getStream(), false);
 119 #endif /* CVC4_TRACING */
 120
 121   // letify subexprs before parents (cascading LETs)
 122   std::sort(d_substNodes.begin(), d_substNodes.end());
 123
 124   for(std::vector<TNode>::iterator i = d_substNodes.begin();
 125       i != d_substNodes.end();
 126       ++i) {
 127     Assert(d_nodeCount[*i] > d_threshold);
 128     TNode parent = d_uniqueParent[*i];
 129     if(!parent.isNull() && d_nodeCount[parent] > d_threshold) {
 130       // no need to letify this expr, because it only occurs in
 131       // a single super-expression, and that one will be letified
 132       continue;
 133     }
 134
 135     // construct the let binder
 136     std::stringstream ss;
 137     ss << d_letVarPrefix << d_letVar++;
 138     Node letvar = NodeManager::currentNM()->mkVar(ss.str(), (*i).getType());
 139
 140     // apply previous substitutions to the rhs, enabling cascading LETs
 141     Node n = d_substitutions->apply(*i);
 142     Assert(! d_substitutions->hasSubstitution(n));
 143     d_substitutions->addSubstitution(n, letvar);
 144   }
 145 }
 146
 147 const theory::SubstitutionMap& DagificationVisitor::getLets() {
 148   AlwaysAssert(d_done, "DagificationVisitor must be used as a visitor before getting the dagified version out!");
 149   return *d_substitutions;
 150 }
 151
 152 Node DagificationVisitor::getDagifiedBody() {
 153   AlwaysAssert(d_done, "DagificationVisitor must be used as a visitor before getting the dagified version out!");
 154
 155 #ifdef CVC4_TRACING
 156 #  ifdef CVC4_DEBUG
 157   // turn off dagification for Debug stream while we're doing this work
 158   Node::dag::Scope scopeDebug(Debug.getStream(), false);
 159 #  endif /* CVC4_DEBUG */
 160   // turn off dagification for Trace stream while we're doing this work
 161   Node::dag::Scope scopeTrace(Trace.getStream(), false);
 162 #endif /* CVC4_TRACING */
 163
 164   return d_substitutions->apply(d_top);
 165 }
 166
 167 }/* CVC4::printer namespace */
 168 }/* CVC4 namespace */