src/util/ite_removal.cpp

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