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