src/theory/substitutions.cpp

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