src/util/ite_removal.cpp

   1 /*********************                                                        */
   2 /*! \file ite_removal.cpp
   3  ** \verbatim
   4  ** Original author: Dejan Jovanovic
   5  ** Major contributors: Andrew Reynolds, Morgan Deters
   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 "theory/rewriter.h"
  21 #include "expr/command.h"
  22 #include "theory/quantifiers/options.h"
  23
  24 using namespace CVC4;
  25 using namespace std;
  26
  27 namespace CVC4 {
  28
  29 void RemoveITE::run(std::vector<Node>& output, IteSkolemMap& iteSkolemMap)
  30 {
  31   for (unsigned i = 0, i_end = output.size(); i < i_end; ++ i) {
  32     std::vector<Node> quantVar;
  33     // Do this in two steps to avoid Node problems(?)
  34     // Appears related to bug 512, splitting this into two lines
  35     // fixes the bug on clang on Mac OS
  36     Node itesRemoved = run(output[i], output, iteSkolemMap, quantVar);
  37     output[i] = itesRemoved;
  38   }
  39 }
  40
  41 Node RemoveITE::run(TNode node, std::vector<Node>& output,
  42                     IteSkolemMap& iteSkolemMap, std::vector<Node>& quantVar) {
  43   // Current node
  44   Debug("ite") << "removeITEs(" << node << ")" << endl;
  45
  46   // The result may be cached already
  47   NodeManager *nodeManager = NodeManager::currentNM();
  48   ITECache::iterator i = d_iteCache.find(node);
  49   if(i != d_iteCache.end()) {
  50     Node cachedRewrite = (*i).second;
  51     Debug("ite") << "removeITEs: in-cache: " << cachedRewrite << endl;
  52     return cachedRewrite.isNull() ? Node(node) : cachedRewrite;
  53   }
  54
  55   // If an ITE replace it
  56   if(node.getKind() == kind::ITE) {
  57     TypeNode nodeType = node.getType();
  58     if(!nodeType.isBoolean()) {
  59       Node skolem;
  60       // Make the skolem to represent the ITE
  61       if( quantVar.empty() ){
  62         skolem = nodeManager->mkSkolem("termITE_$$", nodeType, "a variable introduced due to term-level ITE removal");
  63       }else{
  64         //if in the scope of free variables, make a skolem operator
  65         vector< TypeNode > argTypes;
  66         for( size_t i=0; i<quantVar.size(); i++ ){
  67           argTypes.push_back( quantVar[i].getType() );
  68         }
  69         TypeNode typ = NodeManager::currentNM()->mkFunctionType( argTypes, nodeType );
  70         Node op = NodeManager::currentNM()->mkSkolem( "termITEop_$$", typ, "a function variable introduced due to term-level ITE removal" );
  71         vector< Node > funcArgs;
  72         funcArgs.push_back( op );
  73         funcArgs.insert( funcArgs.end(), quantVar.begin(), quantVar.end() );
  74         skolem = NodeManager::currentNM()->mkNode( kind::APPLY_UF, funcArgs );
  75       }
  76
  77       // The new assertion
  78       Node newAssertion =
  79         nodeManager->mkNode(kind::ITE, node[0], skolem.eqNode(node[1]),
  80                             skolem.eqNode(node[2]));
  81       Debug("ite") << "removeITEs(" << node << ") => " << newAssertion << endl;
  82
  83       // Attach the skolem
  84       d_iteCache[node] = skolem;
  85
  86       // Remove ITEs from the new assertion, rewrite it and push it to the output
  87       newAssertion = run(newAssertion, output, iteSkolemMap, quantVar);
  88
  89       if( !quantVar.empty() ){
  90         //if in the scope of free variables, it is a quantified assertion
  91         vector< Node > children;
  92         children.push_back( NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST, quantVar ) );
  93         children.push_back( newAssertion );
  94         newAssertion = NodeManager::currentNM()->mkNode( kind::FORALL, children );
  95       }
  96
  97       iteSkolemMap[skolem] = output.size();
  98       output.push_back(newAssertion);
  99
 100       // The representation is now the skolem
 101       return skolem;
 102     }
 103   }
 104
 105   // If not an ITE, go deep
 106   if( ( node.getKind() != kind::FORALL || options::iteRemoveQuant() ) &&
 107       node.getKind() != kind::EXISTS &&
 108       node.getKind() != kind::REWRITE_RULE ) {
 109     std::vector< Node > newQuantVar;
 110     newQuantVar.insert( newQuantVar.end(), quantVar.begin(), quantVar.end() );
 111     if( node.getKind()==kind::FORALL ){
 112       for( size_t i=0; i<node[0].getNumChildren(); i++ ){
 113         newQuantVar.push_back( node[0][i] );
 114       }
 115     }
 116     vector<Node> newChildren;
 117     bool somethingChanged = false;
 118     if(node.getMetaKind() == kind::metakind::PARAMETERIZED) {
 119       newChildren.push_back(node.getOperator());
 120     }
 121     // Remove the ITEs from the children
 122     for(TNode::const_iterator it = node.begin(), end = node.end(); it != end; ++it) {
 123       Node newChild = run(*it, output, iteSkolemMap, newQuantVar);
 124       somethingChanged |= (newChild != *it);
 125       newChildren.push_back(newChild);
 126     }
 127
 128     // If changes, we rewrite
 129     if(somethingChanged) {
 130       Node cachedRewrite = nodeManager->mkNode(node.getKind(), newChildren);
 131       d_iteCache[node] = cachedRewrite;
 132       return cachedRewrite;
 133     } else {
 134       d_iteCache[node] = Node::null();
 135       return node;
 136     }
 137   } else {
 138     d_iteCache[node] = Node::null();
 139     return node;
 140   }
 141 }
 142
 143 }/* CVC4 namespace */