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): barrett
   7  ** This file is part of the CVC4 prototype.
   8  ** Copyright (c) 2009-2012  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     output[i] = run(output[i], output, iteSkolemMap, quantVar);
  34   }
  35 }
  36
  37 Node RemoveITE::run(TNode node, std::vector<Node>& output,
  38                     IteSkolemMap& iteSkolemMap, std::vector<Node>& quantVar) {
  39   // Current node
  40   Debug("ite") << "removeITEs(" << node << ")" << endl;
  41
  42   // The result may be cached already
  43   NodeManager *nodeManager = NodeManager::currentNM();
  44   ITECache::iterator i = d_iteCache.find(node);
  45   if(i != d_iteCache.end()) {
  46     Node cachedRewrite = (*i).second;
  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       Node skolem;
  56       // Make the skolem to represent the ITE
  57       if( quantVar.empty() ){
  58         skolem = nodeManager->mkSkolem("termITE_$$", nodeType, "a variable introduced due to term-level ITE removal");
  59       }else{
  60         //if in the scope of free variables, make a skolem operator
  61         vector< TypeNode > argTypes;
  62         for( size_t i=0; i<quantVar.size(); i++ ){
  63           argTypes.push_back( quantVar[i].getType() );
  64         }
  65         TypeNode typ = NodeManager::currentNM()->mkFunctionType( argTypes, nodeType );
  66         Node op = NodeManager::currentNM()->mkSkolem( "termITEop_$$", typ, "a function variable introduced due to term-level ITE removal" );
  67         vector< Node > funcArgs;
  68         funcArgs.push_back( op );
  69         funcArgs.insert( funcArgs.end(), quantVar.begin(), quantVar.end() );
  70         skolem = NodeManager::currentNM()->mkNode( kind::APPLY_UF, funcArgs );
  71       }
  72
  73       // The new assertion
  74       Node newAssertion =
  75         nodeManager->mkNode(kind::ITE, node[0], skolem.eqNode(node[1]),
  76                             skolem.eqNode(node[2]));
  77       Debug("ite") << "removeITEs(" << node << ") => " << newAssertion << endl;
  78
  79       // Attach the skolem
  80       d_iteCache[node] = skolem;
  81
  82       // Remove ITEs from the new assertion, rewrite it and push it to the output
  83       newAssertion = run(newAssertion, output, iteSkolemMap, quantVar);
  84
  85       if( !quantVar.empty() ){
  86         //if in the scope of free variables, it is a quantified assertion
  87         vector< Node > children;
  88         children.push_back( NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST, quantVar ) );
  89         children.push_back( newAssertion );
  90         newAssertion = NodeManager::currentNM()->mkNode( kind::FORALL, children );
  91       }
  92
  93       iteSkolemMap[skolem] = output.size();
  94       output.push_back(newAssertion);
  95
  96       // The representation is now the skolem
  97       return skolem;
  98     }
  99   }
 100
 101   // If not an ITE, go deep
 102   if( ( node.getKind() != kind::FORALL || options::iteRemoveQuant() ) &&
 103       node.getKind() != kind::EXISTS &&
 104       node.getKind() != kind::REWRITE_RULE ) {
 105     std::vector< Node > newQuantVar;
 106     newQuantVar.insert( newQuantVar.end(), quantVar.begin(), quantVar.end() );
 107     if( node.getKind()==kind::FORALL ){
 108       for( size_t i=0; i<node[0].getNumChildren(); i++ ){
 109         newQuantVar.push_back( node[0][i] );
 110       }
 111     }
 112     vector<Node> newChildren;
 113     bool somethingChanged = false;
 114     if(node.getMetaKind() == kind::metakind::PARAMETERIZED) {
 115       newChildren.push_back(node.getOperator());
 116     }
 117     // Remove the ITEs from the children
 118     for(TNode::const_iterator it = node.begin(), end = node.end(); it != end; ++it) {
 119       Node newChild = run(*it, output, iteSkolemMap, newQuantVar);
 120       somethingChanged |= (newChild != *it);
 121       newChildren.push_back(newChild);
 122     }
 123
 124     // If changes, we rewrite
 125     if(somethingChanged) {
 126       Node cachedRewrite = nodeManager->mkNode(node.getKind(), newChildren);
 127       d_iteCache[node] = cachedRewrite;
 128       return cachedRewrite;
 129     } else {
 130       d_iteCache[node] = Node::null();
 131       return node;
 132     }
 133   } else {
 134     d_iteCache[node] = Node::null();
 135     return node;
 136   }
 137 }
 138
 139 }/* CVC4 namespace */