src/util/ite_removal.cpp

   1 /*********************                                                        */
   2 /*! \file ite_removal.cpp
   3  ** \verbatim
   4  ** Original author: dejan
   5  ** Major contributors: mdeters
   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 Removal of term ITEs
  15  **
  16  ** Removal of term ITEs.
  17  **/
  18
  19 #include <vector>
  20
  21 #include "util/ite_removal.h"
  22 #include "theory/rewriter.h"
  23 #include "expr/command.h"
  24
  25 using namespace CVC4;
  26 using namespace std;
  27
  28 namespace CVC4 {
  29
  30 struct IteRewriteAttrTag {};
  31 typedef expr::Attribute<IteRewriteAttrTag, Node> IteRewriteAttr;
  32
  33 void RemoveITE::run(std::vector<Node>& output) {
  34   for (unsigned i = 0, i_end = output.size(); i < i_end; ++ i) {
  35     output[i] = run(output[i], output);
  36   }
  37 }
  38
  39 Node RemoveITE::run(TNode node, std::vector<Node>& output) {
  40   // Current node
  41   Debug("ite") << "removeITEs(" << node << ")" << endl;
  42
  43   // The result may be cached already
  44   Node cachedRewrite;
  45   NodeManager *nodeManager = NodeManager::currentNM();
  46   if(nodeManager->getAttribute(node, IteRewriteAttr(), cachedRewrite)) {
  47     Debug("ite") << "removeITEs: in-cache: " << cachedRewrite << endl;
  48     return cachedRewrite.isNull() ? Node(node) : cachedRewrite;
  49   }
  50
  51   // If an ITE replace it
  52   if(node.getKind() == kind::ITE) {
  53     TypeNode nodeType = node.getType();
  54     if(!nodeType.isBoolean()) {
  55       // Make the skolem to represent the ITE
  56       Node skolem = nodeManager->mkVar(nodeType);
  57
  58       if(Dump.isOn("declarations")) {
  59         stringstream kss;
  60         kss << Expr::setlanguage(Expr::setlanguage::getLanguage(Dump("declarations"))) << skolem;
  61         string ks = kss.str();
  62         Dump("declarations") << CommentCommand(ks + " is a variable introduced due to term-level ITE removal") << endl
  63                              << DeclareFunctionCommand(ks, nodeType.toType()) << endl;
  64       }
  65
  66       // The new assertion
  67       Node newAssertion =
  68         nodeManager->mkNode(kind::ITE, node[0], skolem.eqNode(node[1]),
  69                             skolem.eqNode(node[2]));
  70       Debug("ite") << "removeITEs(" << node << ") => " << newAssertion << endl;
  71
  72       // Attach the skolem
  73       nodeManager->setAttribute(node, IteRewriteAttr(), skolem);
  74
  75       // Remove ITEs from the new assertion, rewrite it and push it to the output
  76       output.push_back(run(newAssertion, output));
  77
  78       // The representation is now the skolem
  79       return skolem;
  80     }
  81   }
  82
  83   // If not an ITE, go deep
  84   vector<Node> newChildren;
  85   bool somethingChanged = false;
  86   if(node.getMetaKind() == kind::metakind::PARAMETERIZED) {
  87     newChildren.push_back(node.getOperator());
  88   }
  89   // Remove the ITEs from the children
  90   for(TNode::const_iterator it = node.begin(), end = node.end(); it != end; ++it) {
  91     Node newChild = run(*it, output);
  92     somethingChanged |= (newChild != *it);
  93     newChildren.push_back(newChild);
  94   }
  95
  96   // If changes, we rewrite
  97   if(somethingChanged) {
  98     cachedRewrite = nodeManager->mkNode(node.getKind(), newChildren);
  99     nodeManager->setAttribute(node, IteRewriteAttr(), cachedRewrite);
 100     return cachedRewrite;
 101   } else {
 102     nodeManager->setAttribute(node, IteRewriteAttr(), Node::null());
 103     return node;
 104   }
 105 }
 106
 107 }/* CVC4 namespace */