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 #include "theory/rewriter.h"
  21
  22 using namespace std;
  23
  24 namespace CVC4 {
  25 namespace theory {
  26
  27 struct substitution_stack_element {
  28   TNode node;
  29   bool children_added;
  30   substitution_stack_element(TNode node)
  31   : node(node), children_added(false) {}
  32 };
  33
  34 Node SubstitutionMap::internalSubstitute(TNode t, NodeCache& substitutionCache) {
  35
  36   Debug("substitution::internal") << "SubstitutionMap::internalSubstitute(" << t << ")" << std::endl;
  37
  38   // If nothing to substitute just return the node
  39   if (substitutionCache.empty()) {
  40     return t;
  41   }
  42
  43   // Do a topological sort of the subexpressions and substitute them
  44   vector<substitution_stack_element> toVisit;
  45   toVisit.push_back((TNode) t);
  46
  47   while (!toVisit.empty())
  48   {
  49     // The current node we are processing
  50     substitution_stack_element& stackHead = toVisit.back();
  51     TNode current = stackHead.node;
  52
  53     Debug("substitution::internal") << "SubstitutionMap::internalSubstitute(" << t << "): processing " << current << std::endl;
  54
  55     // If node already in the cache we're done, pop from the stack
  56     NodeCache::iterator find = substitutionCache.find(current);
  57     if (find != substitutionCache.end()) {
  58       toVisit.pop_back();
  59       continue;
  60     }
  61
  62     // Not yet substituted, so process
  63     if (stackHead.children_added) {
  64       // Children have been processed, so substitute
  65       NodeBuilder<> builder(current.getKind());
  66       if (current.getMetaKind() == kind::metakind::PARAMETERIZED) {
  67         builder << current.getOperator();
  68       }
  69       for (unsigned i = 0; i < current.getNumChildren(); ++ i) {
  70         Assert(substitutionCache.find(current[i]) != substitutionCache.end());
  71         builder << Node(substitutionCache[current[i]]);
  72       }
  73       // Mark the substitution and continue
  74       Node result = builder;
  75       find = substitutionCache.find(result);
  76       if (find != substitutionCache.end()) {
  77         result = find->second;
  78       }
  79       Debug("substitution::internal") << "SubstitutionMap::internalSubstitute(" << t << "): setting " << current << " -> " << result << std::endl;
  80       substitutionCache[current] = result;
  81       toVisit.pop_back();
  82     } else {
  83       // Mark that we have added the children if any
  84       if (current.getNumChildren() > 0) {
  85         stackHead.children_added = true;
  86         // We need to add the children
  87         for(TNode::iterator child_it = current.begin(); child_it != current.end(); ++ child_it) {
  88           TNode childNode = *child_it;
  89           NodeCache::iterator childFind = substitutionCache.find(childNode);
  90           if (childFind == substitutionCache.end()) {
  91             toVisit.push_back(childNode);
  92           }
  93         }
  94       } else {
  95         // No children, so we're done
  96         Debug("substitution::internal") << "SubstitutionMap::internalSubstitute(" << t << "): setting " << current << " -> " << current << std::endl;
  97         substitutionCache[current] = current;
  98         toVisit.pop_back();
  99       }
 100     }
 101   }
 102
 103   // Return the substituted version
 104   return substitutionCache[t];
 105 }
 106
 107
 108 void SubstitutionMap::simplifyRHS(const SubstitutionMap& subMap)
 109 {
 110   // Put 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] = subMap.apply((*it).second);
 115   }
 116 }
 117
 118
 119 void SubstitutionMap::simplifyRHS(TNode x, TNode t) {
 120   // Temporary substitution cache
 121   NodeCache tempCache;
 122   tempCache[x] = t;
 123
 124   // Put the new substitution into the old ones
 125   NodeMap::iterator it = d_substitutions.begin();
 126   NodeMap::iterator it_end = d_substitutions.end();
 127   for(; it != it_end; ++ it) {
 128     d_substitutions[(*it).first] = internalSubstitute((*it).second, tempCache);
 129   }
 130 }
 131
 132
 133 /* We use subMap to simplify the left-hand sides of the current substitution map.  If rewrite is true,
 134  * we also apply the rewriter to the result.
 135  * We want to maintain the invariant that all lhs are distinct from each other and from all rhs.
 136  * If for some l -> r, l reduces to l', we try to add a new rule l' -> r.  There are two cases
 137  * where this fails
 138  *   (i) if l' is equal to some ll (in a rule ll -> rr), then if r != rr we add (r,rr) to the equation list
 139  *   (i) if l' is equalto some rr (in a rule ll -> rr), then if r != rr we add (r,rr) to the equation list
 140  */
 141 void SubstitutionMap::simplifyLHS(const SubstitutionMap& subMap, vector<pair<Node, Node> >& equalities, bool rewrite)
 142 {
 143   Assert(d_worklist.empty());
 144   // First, apply subMap to every LHS in d_substitutions
 145   NodeMap::iterator it = d_substitutions.begin();
 146   NodeMap::iterator it_end = d_substitutions.end();
 147   Node newLeft;
 148   for(; it != it_end; ++ it) {
 149     newLeft = subMap.apply((*it).first);
 150     if (newLeft != (*it).first) {
 151       if (rewrite) {
 152         newLeft = Rewriter::rewrite(newLeft);
 153       }
 154       d_worklist.push_back(pair<Node,Node>(newLeft, (*it).second));
 155     }
 156   }
 157   processWorklist(equalities, rewrite);
 158   Assert(d_worklist.empty());
 159 }
 160
 161
 162 void SubstitutionMap::simplifyLHS(TNode lhs, TNode rhs, vector<pair<Node,Node> >& equalities, bool rewrite)
 163 {
 164   Assert(d_worklist.empty());
 165   d_worklist.push_back(pair<Node,Node>(lhs,rhs));
 166   processWorklist(equalities, rewrite);
 167   Assert(d_worklist.empty());
 168 }
 169
 170
 171 void SubstitutionMap::processWorklist(vector<pair<Node, Node> >& equalities, bool rewrite)
 172 {
 173   // Add each new rewrite rule, taking care not to invalidate invariants and looking
 174   // for any new rewrite rules we can learn
 175   Node newLeft, newRight;
 176   while (!d_worklist.empty()) {
 177     newLeft = d_worklist.back().first;
 178     newRight = d_worklist.back().second;
 179     d_worklist.pop_back();
 180
 181     NodeCache tempCache;
 182     tempCache[newLeft] = newRight;
 183
 184     Node newLeft2;
 185     unsigned size = d_worklist.size();
 186     bool addThisRewrite = true;
 187     NodeMap::iterator it = d_substitutions.begin();
 188     NodeMap::iterator it_end = d_substitutions.end();
 189
 190     for(; it != it_end; ++ it) {
 191
 192       // Check for invariant violation.  If new rewrite is redundant, do nothing
 193       // Otherwise, add an equality to the output equalities
 194       // In either case undo any work done by this rewrite
 195       if (newLeft == (*it).first || newLeft == (*it).second) {
 196         if ((*it).second != newRight) {
 197           equalities.push_back(pair<Node,Node>((*it).second, newRight));
 198         }
 199         while (d_worklist.size() > size) {
 200           d_worklist.pop_back();
 201         }
 202         addThisRewrite = false;
 203         break;
 204       }
 205
 206       newLeft2 = internalSubstitute((*it).first, tempCache);
 207       if (newLeft2 != (*it).first) {
 208         if (rewrite) {
 209           newLeft2 = Rewriter::rewrite(newLeft2);
 210         }
 211         d_worklist.push_back(pair<Node,Node>(newLeft2, (*it).second));
 212       }
 213     }
 214     if (addThisRewrite) {
 215       d_substitutions[newLeft] = newRight;
 216       d_cacheInvalidated = true;
 217     }
 218   }
 219 }
 220
 221
 222 void SubstitutionMap::addSubstitution(TNode x, TNode t, bool invalidateCache, bool backSub, bool forwardSub) {
 223   Debug("substitution") << "SubstitutionMap::addSubstitution(" << x << ", " << t << ")" << std::endl;
 224   Assert(d_substitutions.find(x) == d_substitutions.end());
 225
 226   if (backSub) {
 227     simplifyRHS(x, t);
 228   }
 229
 230   // Put the new substitution in
 231   d_substitutions[x] = forwardSub ? apply(t) : Node(t);
 232
 233   // Also invalidate the cache if necessary
 234   if (invalidateCache) {
 235     d_cacheInvalidated = true;
 236   }
 237   else {
 238     d_substitutionCache[x] = d_substitutions[x];
 239   }
 240 }
 241
 242 static bool check(TNode node, const SubstitutionMap::NodeMap& substitutions) CVC4_UNUSED;
 243 static bool check(TNode node, const SubstitutionMap::NodeMap& substitutions) {
 244   SubstitutionMap::NodeMap::const_iterator it = substitutions.begin();
 245   SubstitutionMap::NodeMap::const_iterator it_end = substitutions.end();
 246   Debug("substitution") << "checking " << node << std::endl;
 247   for (; it != it_end; ++ it) {
 248     Debug("substitution") << "-- hasSubterm( " << (*it).first << " ) ?" << std::endl;
 249     if (node.hasSubterm((*it).first)) {
 250       Debug("substitution") << "-- FAIL" << std::endl;
 251       return false;
 252     }
 253   }
 254   Debug("substitution") << "-- SUCCEED" << std::endl;
 255   return true;
 256 }
 257
 258 Node SubstitutionMap::apply(TNode t) {
 259
 260   Debug("substitution") << "SubstitutionMap::apply(" << t << ")" << std::endl;
 261
 262   // Setup the cache
 263   if (d_cacheInvalidated) {
 264     SubstitutionMap::NodeMap::const_iterator it = d_substitutions.begin();
 265     SubstitutionMap::NodeMap::const_iterator it_end = d_substitutions.end();
 266     d_substitutionCache.clear();
 267     for (; it != it_end; ++ it) {
 268       d_substitutionCache[(*it).first] = (*it).second;
 269     }
 270     d_cacheInvalidated = false;
 271     Debug("substitution") << "-- reset the cache" << std::endl;
 272   }
 273
 274   // Perform the substitution
 275   Node result = internalSubstitute(t, d_substitutionCache);
 276   Debug("substitution") << "SubstitutionMap::apply(" << t << ") => " << result << std::endl;
 277
 278 //  Assert(check(result, d_substitutions));
 279
 280   return result;
 281 }
 282
 283 void SubstitutionMap::print(ostream& out) const {
 284   NodeMap::const_iterator it = d_substitutions.begin();
 285   NodeMap::const_iterator it_end = d_substitutions.end();
 286   for (; it != it_end; ++ it) {
 287     out << (*it).first << " -> " << (*it).second << endl;
 288   }
 289 }
 290
 291 void SubstitutionMap::debugPrint() const {
 292   print(std::cout);
 293 }
 294
 295 }/* CVC4::theory namespace */
 296
 297 std::ostream& operator<<(std::ostream& out, const theory::SubstitutionMap::iterator& i) {
 298   return out << "[CDMap-iterator]";
 299 }
 300
 301 }/* CVC4 namespace */