src/util/ite_removal.cpp

   1 /*********************                                                        */
   2 /*! \file ite_removal.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 Representation of cardinality
  15  **
  16  ** Simple class to represent a cardinality; used by the CVC4 type system
  17  ** give the cardinality of sorts.
  18  **/
  19
  20 #include <vector>
  21
  22 #include "util/ite_removal.h"
  23 #include "theory/rewriter.h"
  24
  25 using namespace CVC4;
  26 using namespace std;
  27
  28 struct IteRewriteAttrTag {};
  29 typedef expr::Attribute<IteRewriteAttrTag, Node> IteRewriteAttr;
  30
  31 void RemoveITE::run(std::vector<Node>& output) {
  32   for (unsigned i = 0, i_end = output.size(); i < i_end; ++ i) {
  33     output[i] = run(output[i], output);
  34   }
  35 }
  36
  37 Node RemoveITE::run(TNode node, std::vector<Node>& output)
  38 {
  39   // Current node
  40   Debug("ite") << "removeITEs(" << node << ")" << endl;
  41
  42   // The result may be cached already
  43   Node cachedRewrite;
  44   NodeManager *nodeManager = NodeManager::currentNM();
  45   if(nodeManager->getAttribute(node, IteRewriteAttr(), cachedRewrite)) {
  46     Debug("ite") << "removeITEs: in-cache: " << cachedRewrite << endl;
  47     return cachedRewrite.isNull() ? Node(node) : cachedRewrite;
  48   }
  49
  50   // If an ITE replace it
  51   if(node.getKind() == kind::ITE) {
  52     TypeNode nodeType = node.getType();
  53     if(!nodeType.isBoolean()) {
  54       // Make the skolem to represent the ITE
  55       Node skolem = nodeManager->mkVar(nodeType);
  56
  57       // The new assertion
  58       Node newAssertion = nodeManager->mkNode(kind::ITE, node[0], skolem.eqNode(node[1]), skolem.eqNode(node[2]));
  59       Debug("ite") << "removeITEs(" << node << ") => " << newAssertion << endl;
  60
  61       // Attach the skolem
  62       nodeManager->setAttribute(node, IteRewriteAttr(), skolem);
  63
  64       // Remove ITEs from the new assertion, rewrite it and push it to the output
  65       output.push_back(run(newAssertion, output));
  66
  67       // The representation is now the skolem
  68       return skolem;
  69     }
  70   }
  71
  72   // If not an ITE, go deep
  73   vector<Node> newChildren;
  74   bool somethingChanged = false;
  75   if(node.getMetaKind() == kind::metakind::PARAMETERIZED) {
  76     newChildren.push_back(node.getOperator());
  77   }
  78   // Remove the ITEs from the children
  79   for(TNode::const_iterator it = node.begin(), end = node.end(); it != end; ++it) {
  80     Node newChild = run(*it, output);
  81     somethingChanged |= (newChild != *it);
  82     newChildren.push_back(newChild);
  83   }
  84
  85   // If changes, we rewrite
  86   if(somethingChanged) {
  87     cachedRewrite = nodeManager->mkNode(node.getKind(), newChildren);
  88     nodeManager->setAttribute(node, IteRewriteAttr(), cachedRewrite);
  89     return cachedRewrite;
  90   } else {
  91     nodeManager->setAttribute(node, IteRewriteAttr(), Node::null());
  92     return node;
  93   }
  94 };