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       Node skolem;
  95       // Make the skolem to represent the ITE
  96       skolem = nodeManager->mkSkolem("termITE_$$", nodeType, "a variable introduced due to term-level ITE removal");
  97
  98       // The new assertion
  99       Node newAssertion =
 100         nodeManager->mkNode(kind::ITE, node[0], skolem.eqNode(node[1]),
 101                             skolem.eqNode(node[2]));
 102       Debug("ite") << "removeITEs(" << node << ") => " << newAssertion << endl;
 103
 104       // Attach the skolem
 105       d_iteCache.insert(cacheKey, skolem);
 106
 107       // Remove ITEs from the new assertion, rewrite it and push it to the output
 108       newAssertion = run(newAssertion, output, iteSkolemMap, inQuant);
 109
 110       iteSkolemMap[skolem] = output.size();
 111       output.push_back(newAssertion);
 112
 113       // The representation is now the skolem
 114       return skolem;
 115     }
 116   }
 117
 118   // If not an ITE, go deep
 119   vector<Node> newChildren;
 120   bool somethingChanged = false;
 121   if(node.getMetaKind() == kind::metakind::PARAMETERIZED) {
 122     newChildren.push_back(node.getOperator());
 123   }
 124   // Remove the ITEs from the children
 125   for(TNode::const_iterator it = node.begin(), end = node.end(); it != end; ++it) {
 126     Node newChild = run(*it, output, iteSkolemMap, inQuant);
 127     somethingChanged |= (newChild != *it);
 128     newChildren.push_back(newChild);
 129   }
 130
 131   // If changes, we rewrite
 132   if(somethingChanged) {
 133     Node cached = nodeManager->mkNode(node.getKind(), newChildren);
 134     d_iteCache.insert(cacheKey, cached);
 135     return cached;
 136   } else {
 137     d_iteCache.insert(cacheKey, Node::null());
 138     return node;
 139   }
 140 }
 141
 142 Node RemoveITE::replace(TNode node, bool inQuant) const {
 143   if(node.isVar() || node.isConst() ||
 144      (options::biasedITERemoval() && !containsTermITE(node))){
 145     return Node(node);
 146   }
 147
 148   // Check the cache
 149   NodeManager *nodeManager = NodeManager::currentNM();
 150   ITECache::const_iterator i = d_iteCache.find(make_pair(node, inQuant));
 151   if(i != d_iteCache.end()) {
 152     Node cached = (*i).second;
 153     return cached.isNull() ? Node(node) : cached;
 154   }
 155
 156   // Remember that we're inside a quantifier
 157   if(node.getKind() == kind::FORALL || node.getKind() == kind::EXISTS) {
 158     inQuant = true;
 159   }
 160
 161   vector<Node> newChildren;
 162   bool somethingChanged = false;
 163   if(node.getMetaKind() == kind::metakind::PARAMETERIZED) {
 164     newChildren.push_back(node.getOperator());
 165   }
 166   // Replace in children
 167   for(TNode::const_iterator it = node.begin(), end = node.end(); it != end; ++it) {
 168     Node newChild = replace(*it, inQuant);
 169     somethingChanged |= (newChild != *it);
 170     newChildren.push_back(newChild);
 171   }
 172
 173   // If changes, we rewrite
 174   if(somethingChanged) {
 175     return nodeManager->mkNode(node.getKind(), newChildren);
 176   } else {
 177     return node;
 178   }
 179 }
 180
 181 }/* CVC4 namespace */