src/theory/substitutions.cpp

   1 /*********************                                                        */
   2 /*! \file substitutions.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Dejan Jovanovic, Clark Barrett, Morgan Deters
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2020 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 A substitution mapping for theory simplification
  13  **
  14  ** A substitution mapping for theory simplification.
  15  **/
  16
  17 #include "theory/substitutions.h"
  18 #include "expr/node_algorithm.h"
  19 #include "theory/rewriter.h"
  20
  21 using namespace std;
  22
  23 namespace CVC4 {
  24 namespace theory {
  25
  26 struct substitution_stack_element {
  27   TNode d_node;
  28   bool d_children_added;
  29   substitution_stack_element(TNode node) : d_node(node), d_children_added(false)
  30   {
  31   }
  32 };/* struct substitution_stack_element */
  33
  34 Node SubstitutionMap::internalSubstitute(TNode t, NodeCache& cache) {
  35
  36   Debug("substitution::internal") << "SubstitutionMap::internalSubstitute(" << t << ")" << endl;
  37
  38   if (d_substitutions.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.d_node;
  51
  52     Debug("substitution::internal") << "SubstitutionMap::internalSubstitute(" << t << "): processing " << current << endl;
  53
  54     // If node already in the cache we're done, pop from the stack
  55     NodeCache::iterator find = cache.find(current);
  56     if (find != cache.end()) {
  57       toVisit.pop_back();
  58       continue;
  59     }
  60
  61     if (!d_substituteUnderQuantifiers && current.isClosure())
  62     {
  63       Debug("substitution::internal") << "--not substituting under quantifier" << endl;
  64       cache[current] = current;
  65       toVisit.pop_back();
  66       continue;
  67     }
  68
  69     NodeMap::iterator find2 = d_substitutions.find(current);
  70     if (find2 != d_substitutions.end()) {
  71       Node rhs = (*find2).second;
  72       Assert(rhs != current);
  73       internalSubstitute(rhs, cache);
  74       d_substitutions[current] = cache[rhs];
  75       cache[current] = cache[rhs];
  76       toVisit.pop_back();
  77       continue;
  78     }
  79
  80     // Not yet substituted, so process
  81     if (stackHead.d_children_added)
  82     {
  83       // Children have been processed, so substitute
  84       NodeBuilder<> builder(current.getKind());
  85       if (current.getMetaKind() == kind::metakind::PARAMETERIZED) {
  86         builder << Node(cache[current.getOperator()]);
  87       }
  88       for (unsigned i = 0; i < current.getNumChildren(); ++ i) {
  89         Assert(cache.find(current[i]) != cache.end());
  90         builder << Node(cache[current[i]]);
  91       }
  92       // Mark the substitution and continue
  93       Node result = builder;
  94       if (result != current) {
  95         find = cache.find(result);
  96         if (find != cache.end()) {
  97           result = find->second;
  98         }
  99         else {
 100           find2 = d_substitutions.find(result);
 101           if (find2 != d_substitutions.end()) {
 102             Node rhs = (*find2).second;
 103             Assert(rhs != result);
 104             internalSubstitute(rhs, cache);
 105             d_substitutions[result] = cache[rhs];
 106             cache[result] = cache[rhs];
 107             result = cache[rhs];
 108           }
 109         }
 110       }
 111       Debug("substitution::internal") << "SubstitutionMap::internalSubstitute(" << t << "): setting " << current << " -> " << result << endl;
 112       cache[current] = result;
 113       toVisit.pop_back();
 114     }
 115     else
 116     {
 117       // Mark that we have added the children if any
 118       if (current.getNumChildren() > 0 || current.getMetaKind() == kind::metakind::PARAMETERIZED) {
 119         stackHead.d_children_added = true;
 120         // We need to add the operator, if any
 121         if(current.getMetaKind() == kind::metakind::PARAMETERIZED) {
 122           TNode opNode = current.getOperator();
 123           NodeCache::iterator opFind = cache.find(opNode);
 124           if (opFind == cache.end()) {
 125             toVisit.push_back(opNode);
 126           }
 127         }
 128         // We need to add the children
 129         for(TNode::iterator child_it = current.begin(); child_it != current.end(); ++ child_it) {
 130           TNode childNode = *child_it;
 131           NodeCache::iterator childFind = cache.find(childNode);
 132           if (childFind == cache.end()) {
 133             toVisit.push_back(childNode);
 134           }
 135         }
 136       } else {
 137         // No children, so we're done
 138         Debug("substitution::internal") << "SubstitutionMap::internalSubstitute(" << t << "): setting " << current << " -> " << current << endl;
 139         cache[current] = current;
 140         toVisit.pop_back();
 141       }
 142     }
 143   }
 144
 145   // Return the substituted version
 146   return cache[t];
 147 }/* SubstitutionMap::internalSubstitute() */
 148
 149
 150 void SubstitutionMap::addSubstitution(TNode x, TNode t, bool invalidateCache)
 151 {
 152   Debug("substitution") << "SubstitutionMap::addSubstitution(" << x << ", " << t << ")" << endl;
 153   Assert(d_substitutions.find(x) == d_substitutions.end());
 154
 155   // this causes a later assert-fail (the rhs != current one, above) anyway
 156   // putting it here is easier to diagnose
 157   Assert(x != t) << "cannot substitute a term for itself";
 158
 159   d_substitutions[x] = t;
 160
 161   // Also invalidate the cache if necessary
 162   if (invalidateCache) {
 163     d_cacheInvalidated = true;
 164   }
 165   else {
 166     d_substitutionCache[x] = d_substitutions[x];
 167   }
 168 }
 169
 170
 171 void SubstitutionMap::addSubstitutions(SubstitutionMap& subMap, bool invalidateCache)
 172 {
 173   SubstitutionMap::NodeMap::const_iterator it = subMap.begin();
 174   SubstitutionMap::NodeMap::const_iterator it_end = subMap.end();
 175   for (; it != it_end; ++ it) {
 176     Assert(d_substitutions.find((*it).first) == d_substitutions.end());
 177     d_substitutions[(*it).first] = (*it).second;
 178     if (!invalidateCache) {
 179       d_substitutionCache[(*it).first] = d_substitutions[(*it).first];
 180     }
 181   }
 182   if (invalidateCache) {
 183     d_cacheInvalidated = true;
 184   }
 185 }
 186
 187 Node SubstitutionMap::apply(TNode t) {
 188
 189   Debug("substitution") << "SubstitutionMap::apply(" << t << ")" << endl;
 190
 191   // Setup the cache
 192   if (d_cacheInvalidated) {
 193     d_substitutionCache.clear();
 194     d_cacheInvalidated = false;
 195     Debug("substitution") << "-- reset the cache" << endl;
 196   }
 197
 198   // Perform the substitution
 199   Node result = internalSubstitute(t, d_substitutionCache);
 200   Debug("substitution") << "SubstitutionMap::apply(" << t << ") => " << result << endl;
 201
 202   return result;
 203 }
 204
 205 void SubstitutionMap::print(ostream& out) const {
 206   NodeMap::const_iterator it = d_substitutions.begin();
 207   NodeMap::const_iterator it_end = d_substitutions.end();
 208   for (; it != it_end; ++ it) {
 209     out << (*it).first << " -> " << (*it).second << endl;
 210   }
 211 }
 212
 213 void SubstitutionMap::debugPrint() const { print(CVC4Message.getStream()); }
 214
 215 }/* CVC4::theory namespace */
 216
 217 std::ostream& operator<<(std::ostream& out, const theory::SubstitutionMap::iterator& i) {
 218   return out << "[CDMap-iterator]";
 219 }
 220
 221 }/* CVC4 namespace */