src/util/ite_removal.cpp

   1 /*********************                                                        */
   2 /*! \file ite_removal.cpp
   3  ** \verbatim
   4  ** Original author: Dejan Jovanovic
   5  ** Major contributors: Tim King, Morgan Deters
   6  ** Minor contributors (to current version): Kshitij Bansal, Andrew Reynolds, Clark Barrett
   7  ** This file is part of the CVC4 project.
   8  ** Copyright (c) 2009-2014  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 Removal of term ITEs
  13  **
  14  ** Removal of term ITEs.
  15  **/
  16
  17 #include <vector>
  18
  19 #include "util/ite_removal.h"
  20 #include "expr/command.h"
  21 #include "theory/ite_utilities.h"
  22 #include "proof/proof_manager.h"
  23
  24 using namespace CVC4;
  25 using namespace std;
  26
  27 namespace CVC4 {
  28
  29 RemoveITE::RemoveITE(context::UserContext* u)
  30   : d_iteCache(u)
  31 {
  32   d_containsVisitor = new theory::ContainsTermITEVisitor();
  33 }
  34
  35 RemoveITE::~RemoveITE(){
  36   delete d_containsVisitor;
  37 }
  38
  39 void RemoveITE::garbageCollect(){
  40   d_containsVisitor->garbageCollect();
  41 }
  42
  43 theory::ContainsTermITEVisitor* RemoveITE::getContainsVisitor() {
  44   return d_containsVisitor;
  45 }
  46
  47 size_t RemoveITE::collectedCacheSizes() const{
  48   return d_containsVisitor->cache_size() + d_iteCache.size();
  49 }
  50
  51 void RemoveITE::run(std::vector<Node>& output, IteSkolemMap& iteSkolemMap, bool reportDeps)
  52 {
  53   size_t n = output.size();
  54   for (unsigned i = 0, i_end = output.size(); i < i_end; ++ i) {
  55     // Do this in two steps to avoid Node problems(?)
  56     // Appears related to bug 512, splitting this into two lines
  57     // fixes the bug on clang on Mac OS
  58     Node itesRemoved = run(output[i], output, iteSkolemMap, false);
  59     // In some calling contexts, not necessary to report dependence information.
  60     if(reportDeps && options::unsatCores()) {
  61       // new assertions have a dependence on the node
  62       PROOF( ProofManager::currentPM()->addDependence(itesRemoved, output[i]); )
  63       while(n < output.size()) {
  64         PROOF( ProofManager::currentPM()->addDependence(output[n], output[i]); )
  65         ++n;
  66       }
  67     }
  68     output[i] = itesRemoved;
  69   }
  70 }
  71
  72 bool RemoveITE::containsTermITE(TNode e) const {
  73   return d_containsVisitor->containsTermITE(e);
  74 }
  75
  76 Node RemoveITE::run(TNode node, std::vector<Node>& output,
  77                     IteSkolemMap& iteSkolemMap, bool inQuant) {
  78   // Current node
  79   Debug("ite") << "removeITEs(" << node << ")" << endl;
  80
  81   if(node.isVar() || node.isConst() ||
  82      (options::biasedITERemoval() && !containsTermITE(node))){
  83     return Node(node);
  84   }
  85
  86   // The result may be cached already
  87   std::pair<Node, bool> cacheKey(node, inQuant);
  88   NodeManager *nodeManager = NodeManager::currentNM();
  89   ITECache::const_iterator i = d_iteCache.find(cacheKey);
  90   if(i != d_iteCache.end()) {
  91     Node cached = (*i).second;
  92     Debug("ite") << "removeITEs: in-cache: " << cached << endl;
  93     return cached.isNull() ? Node(node) : cached;
  94   }
  95
  96   // Remember that we're inside a quantifier
  97   if(node.getKind() == kind::FORALL || node.getKind() == kind::EXISTS) {
  98     inQuant = true;
  99   }
 100
 101   // If an ITE replace it
 102   if(node.getKind() == kind::ITE) {
 103     TypeNode nodeType = node.getType();
 104     if(!nodeType.isBoolean() && (!inQuant || !node.hasBoundVar())) {
 105       Node skolem;
 106       // Make the skolem to represent the ITE
 107       skolem = nodeManager->mkSkolem("termITE", nodeType, "a variable introduced due to term-level ITE removal");
 108
 109       // The new assertion
 110       Node newAssertion =
 111         nodeManager->mkNode(kind::ITE, node[0], skolem.eqNode(node[1]),
 112                             skolem.eqNode(node[2]));
 113       Debug("ite") << "removeITEs(" << node << ") => " << newAssertion << endl;
 114
 115       // Attach the skolem
 116       d_iteCache.insert(cacheKey, skolem);
 117
 118       // Remove ITEs from the new assertion, rewrite it and push it to the output
 119       newAssertion = run(newAssertion, output, iteSkolemMap, inQuant);
 120
 121       iteSkolemMap[skolem] = output.size();
 122       output.push_back(newAssertion);
 123
 124       // The representation is now the skolem
 125       return skolem;
 126     }
 127   }
 128
 129   // If not an ITE, go deep
 130   vector<Node> newChildren;
 131   bool somethingChanged = false;
 132   if(node.getMetaKind() == kind::metakind::PARAMETERIZED) {
 133     newChildren.push_back(node.getOperator());
 134   }
 135   // Remove the ITEs from the children
 136   for(TNode::const_iterator it = node.begin(), end = node.end(); it != end; ++it) {
 137     Node newChild = run(*it, output, iteSkolemMap, inQuant);
 138     somethingChanged |= (newChild != *it);
 139     newChildren.push_back(newChild);
 140   }
 141
 142   // If changes, we rewrite
 143   if(somethingChanged) {
 144     Node cached = nodeManager->mkNode(node.getKind(), newChildren);
 145     d_iteCache.insert(cacheKey, cached);
 146     return cached;
 147   } else {
 148     d_iteCache.insert(cacheKey, Node::null());
 149     return node;
 150   }
 151 }
 152
 153 Node RemoveITE::replace(TNode node, bool inQuant) const {
 154   if(node.isVar() || node.isConst() ||
 155      (options::biasedITERemoval() && !containsTermITE(node))){
 156     return Node(node);
 157   }
 158
 159   // Check the cache
 160   NodeManager *nodeManager = NodeManager::currentNM();
 161   ITECache::const_iterator i = d_iteCache.find(make_pair(node, inQuant));
 162   if(i != d_iteCache.end()) {
 163     Node cached = (*i).second;
 164     return cached.isNull() ? Node(node) : cached;
 165   }
 166
 167   // Remember that we're inside a quantifier
 168   if(node.getKind() == kind::FORALL || node.getKind() == kind::EXISTS) {
 169     inQuant = true;
 170   }
 171
 172   vector<Node> newChildren;
 173   bool somethingChanged = false;
 174   if(node.getMetaKind() == kind::metakind::PARAMETERIZED) {
 175     newChildren.push_back(node.getOperator());
 176   }
 177   // Replace in children
 178   for(TNode::const_iterator it = node.begin(), end = node.end(); it != end; ++it) {
 179     Node newChild = replace(*it, inQuant);
 180     somethingChanged |= (newChild != *it);
 181     newChildren.push_back(newChild);
 182   }
 183
 184   // If changes, we rewrite
 185   if(somethingChanged) {
 186     return nodeManager->mkNode(node.getKind(), newChildren);
 187   } else {
 188     return node;
 189   }
 190 }
 191
 192 }/* CVC4 namespace */