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       find = substitutionCache.find(result);
  75       if (find != substitutionCache.end()) {
  76         result = find->second;
  77       }
  78       Debug("substitution::internal") << "SubstitutionMap::internalSubstitute(" << t << "): setting " << current << " -> " << result << std::endl;
  79       substitutionCache[current] = result;
  80       toVisit.pop_back();
  81     } else {
  82       // Mark that we have added the children if any
  83       if (current.getNumChildren() > 0) {
  84         stackHead.children_added = true;
  85         // We need to add the children
  86         for(TNode::iterator child_it = current.begin(); child_it != current.end(); ++ child_it) {
  87           TNode childNode = *child_it;
  88           NodeCache::iterator childFind = substitutionCache.find(childNode);
  89           if (childFind == substitutionCache.end()) {
  90             toVisit.push_back(childNode);
  91           }
  92         }
  93       } else {
  94         // No children, so we're done
  95         Debug("substitution::internal") << "SubstitutionMap::internalSubstitute(" << t << "): setting " << current << " -> " << current << std::endl;
  96         substitutionCache[current] = current;
  97         toVisit.pop_back();
  98       }
  99     }
 100   }
 101
 102   // Return the substituted version
 103   return substitutionCache[t];
 104 }
 105
 106 void SubstitutionMap::addSubstitution(TNode x, TNode t, bool invalidateCache) {
 107   Debug("substitution") << "SubstitutionMap::addSubstitution(" << x << ", " << t << ")" << std::endl;
 108   Assert(d_substitutions.find(x) == d_substitutions.end());
 109
 110   // Temporary substitution cache
 111   NodeCache tempCache;
 112   tempCache[x] = t;
 113
 114   // Put in the new substitutions into the old ones
 115   NodeMap::iterator it = d_substitutions.begin();
 116   NodeMap::iterator it_end = d_substitutions.end();
 117   for(; it != it_end; ++ it) {
 118     d_substitutions[(*it).first] = internalSubstitute((*it).second, tempCache);
 119   }
 120
 121   // Put the new substitution in, but apply existing substitutions to rhs first
 122   d_substitutions[x] = apply(t);
 123
 124   // Also invalidate the cache
 125   if (invalidateCache) {
 126     d_cacheInvalidated = true;
 127   }
 128   else {
 129     d_substitutionCache[x] = d_substitutions[x];
 130   }
 131 }
 132
 133 static bool check(TNode node, const SubstitutionMap::NodeMap& substitutions) CVC4_UNUSED;
 134 static bool check(TNode node, const SubstitutionMap::NodeMap& substitutions) {
 135   SubstitutionMap::NodeMap::const_iterator it = substitutions.begin();
 136   SubstitutionMap::NodeMap::const_iterator it_end = substitutions.end();
 137   Debug("substitution") << "checking " << node << std::endl;
 138   for (; it != it_end; ++ it) {
 139     Debug("substitution") << "-- hasSubterm( " << (*it).first << " ) ?" << std::endl;
 140     if (node.hasSubterm((*it).first)) {
 141       Debug("substitution") << "-- FAIL" << std::endl;
 142       return false;
 143     }
 144   }
 145   Debug("substitution") << "-- SUCCEED" << std::endl;
 146   return true;
 147 }
 148
 149 Node SubstitutionMap::apply(TNode t) {
 150
 151   Debug("substitution") << "SubstitutionMap::apply(" << t << ")" << std::endl;
 152
 153   // Setup the cache
 154   if (d_cacheInvalidated) {
 155     SubstitutionMap::NodeMap::const_iterator it = d_substitutions.begin();
 156     SubstitutionMap::NodeMap::const_iterator it_end = d_substitutions.end();
 157     d_substitutionCache.clear();
 158     for (; it != it_end; ++ it) {
 159       d_substitutionCache[(*it).first] = (*it).second;
 160     }
 161     d_cacheInvalidated = false;
 162     Debug("substitution") << "-- reset the cache" << std::endl;
 163   }
 164
 165   // Perform the substitution
 166   Node result = internalSubstitute(t, d_substitutionCache);
 167   Debug("substitution") << "SubstitutionMap::apply(" << t << ") => " << result << std::endl;
 168
 169   Assert(check(result, d_substitutions));
 170
 171   return result;
 172 }
 173
 174 void SubstitutionMap::print(ostream& out) const {
 175   NodeMap::const_iterator it = d_substitutions.begin();
 176   NodeMap::const_iterator it_end = d_substitutions.end();
 177   for (; it != it_end; ++ it) {
 178     out << (*it).first << " -> " << (*it).second << endl;
 179   }
 180 }
 181
 182 }/* CVC4::theory namespace */
 183
 184 std::ostream& operator<<(std::ostream& out, const theory::SubstitutionMap::iterator& i) {
 185   return out << "[CDMap-iterator]";
 186 }
 187
 188 }/* CVC4 namespace */