src/theory/substitutions.cpp

   1 /*********************                                                        */
   2 /*! \file substitutions.cpp
   3  ** \verbatim
   4  ** Original author: dejan
   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  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 A substitution mapping for theory simplification
  15  **
  16  ** A substitution mapping for theory simplification.
  17  **/
  18
  19 #include "theory/substitutions.h"
  20
  21 using namespace std;
  22
  23 namespace CVC4 {
  24 namespace theory {
  25
  26 struct substitution_stack_element {
  27   TNode node;
  28   bool children_added;
  29   substitution_stack_element(TNode node)
  30   : node(node), children_added(false) {}
  31 };
  32
  33 Node SubstitutionMap::internalSubstitute(TNode t, NodeCache& substitutionCache) {
  34
  35   Debug("substitution::internal") << "SubstitutionMap::internalSubstitute(" << t << ")" << std::endl;
  36
  37   // If nothing to substitute just return the node
  38   if (substitutionCache.empty()) {
  39     return t;
  40   }
  41
  42   // Do a topological sort of the subexpressions and substitute them
  43   vector<substitution_stack_element> toVisit;
  44   toVisit.push_back((TNode) t);
  45
  46   while (!toVisit.empty())
  47   {
  48     // The current node we are processing
  49     substitution_stack_element& stackHead = toVisit.back();
  50     TNode current = stackHead.node;
  51
  52     Debug("substitution::internal") << "SubstitutionMap::internalSubstitute(" << t << "): processing " << current << std::endl;
  53
  54     // If node already in the cache we're done, pop from the stack
  55     NodeCache::iterator find = substitutionCache.find(current);
  56     if (find != substitutionCache.end()) {
  57       toVisit.pop_back();
  58       continue;
  59     }
  60
  61     // Not yet substituted, so process
  62     if (stackHead.children_added) {
  63       // Children have been processed, so substitute
  64       NodeBuilder<> builder(current.getKind());
  65       if (current.getMetaKind() == kind::metakind::PARAMETERIZED) {
  66         builder << current.getOperator();
  67       }
  68       for (unsigned i = 0; i < current.getNumChildren(); ++ i) {
  69         Assert(substitutionCache.find(current[i]) != substitutionCache.end());
  70         builder << Node(substitutionCache[current[i]]);
  71       }
  72       // Mark the substitution and continue
  73       Node result = builder;
  74       Debug("substitution::internal") << "SubstitutionMap::internalSubstitute(" << t << "): setting " << current << " -> " << result << std::endl;
  75       substitutionCache[current] = result;
  76       toVisit.pop_back();
  77     } else {
  78       // Mark that we have added the children if any
  79       if (current.getNumChildren() > 0) {
  80         stackHead.children_added = true;
  81         // We need to add the children
  82         for(TNode::iterator child_it = current.begin(); child_it != current.end(); ++ child_it) {
  83           TNode childNode = *child_it;
  84           NodeCache::iterator childFind = substitutionCache.find(childNode);
  85           if (childFind == substitutionCache.end()) {
  86             toVisit.push_back(childNode);
  87           }
  88         }
  89       } else {
  90         // No children, so we're done
  91         Debug("substitution::internal") << "SubstitutionMap::internalSubstitute(" << t << "): setting " << current << " -> " << current << std::endl;
  92         substitutionCache[current] = current;
  93         toVisit.pop_back();
  94       }
  95     }
  96   }
  97
  98   // Return the substituted version
  99   return substitutionCache[t];
 100 }
 101
 102 void SubstitutionMap::addSubstitution(TNode x, TNode t, bool invalidateCache) {
 103   Debug("substitution") << "SubstitutionMap::addSubstitution(" << x << ", " << t << ")" << std::endl;
 104   Assert(d_substitutions.find(x) == d_substitutions.end());
 105
 106   // Temporary substitution cache
 107   NodeCache tempCache;
 108   tempCache[x] = t;
 109
 110   // Put in the new substitutions into the old ones
 111   NodeMap::iterator it = d_substitutions.begin();
 112   NodeMap::iterator it_end = d_substitutions.end();
 113   for(; it != it_end; ++ it) {
 114     d_substitutions[(*it).first] = internalSubstitute((*it).second, tempCache);
 115   }
 116
 117   // Put the new substitution in
 118   d_substitutions[x] = t;
 119
 120   // Also invalidate the cache
 121   if (invalidateCache) {
 122     d_cacheInvalidated = true;
 123   }
 124 }
 125
 126 static bool check(TNode node, const SubstitutionMap::NodeMap& substitutions) CVC4_UNUSED;
 127 static bool check(TNode node, const SubstitutionMap::NodeMap& substitutions) {
 128   SubstitutionMap::NodeMap::const_iterator it = substitutions.begin();
 129   SubstitutionMap::NodeMap::const_iterator it_end = substitutions.end();
 130   Debug("substitution") << "checking " << node << std::endl;
 131   for (; it != it_end; ++ it) {
 132     Debug("substitution") << "-- hasSubterm( " << (*it).first << " ) ?" << std::endl;
 133     if (node.hasSubterm((*it).first)) {
 134       Debug("substitution") << "-- FAIL" << std::endl;
 135       return false;
 136     }
 137   }
 138   Debug("substitution") << "-- SUCCEED" << std::endl;
 139   return true;
 140 }
 141
 142 Node SubstitutionMap::apply(TNode t) {
 143
 144   Debug("substitution") << "SubstitutionMap::apply(" << t << ")" << std::endl;
 145
 146   // Setup the cache
 147   if (d_cacheInvalidated) {
 148     SubstitutionMap::NodeMap::const_iterator it = d_substitutions.begin();
 149     SubstitutionMap::NodeMap::const_iterator it_end = d_substitutions.end();
 150     d_substitutionCache.clear();
 151     for (; it != it_end; ++ it) {
 152       d_substitutionCache[(*it).first] = (*it).second;
 153     }
 154     d_cacheInvalidated = false;
 155     Debug("substitution") << "-- reset the cache" << std::endl;
 156   }
 157
 158   // Perform the substitution
 159   Node result = internalSubstitute(t, d_substitutionCache);
 160   Debug("substitution") << "SubstitutionMap::apply(" << t << ") => " << result << std::endl;
 161
 162   Assert(check(result, d_substitutions));
 163
 164   return result;
 165 }
 166
 167 void SubstitutionMap::print(ostream& out) const {
 168   NodeMap::const_iterator it = d_substitutions.begin();
 169   NodeMap::const_iterator it_end = d_substitutions.end();
 170   for (; it != it_end; ++ it) {
 171     out << (*it).first << " -> " << (*it).second << endl;
 172   }
 173 }
 174
 175 }/* CVC4::theory namespace */
 176
 177 std::ostream& operator<<(std::ostream& out, const theory::SubstitutionMap::iterator& i) {
 178   return out << "[CDMap-iterator]";
 179 }
 180
 181 }/* CVC4 namespace */