src/theory/quantifiers/alpha_equivalence.cpp

   1 /*********************                                                        */
   2 /*! \file alpha_equivalence.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds, Tim King
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
   8  ** in the top-level source directory) and their institutional affiliations.
   9  ** All rights reserved.  See the file COPYING in the top-level source
  10  ** directory for licensing information.\endverbatim
  11  **
  12  ** \brief Alpha equivalence checking
  13  **
  14  **/
  15
  16 #include "theory/quantifiers/alpha_equivalence.h"
  17 #include "theory/quantifiers/term_database.h"
  18
  19 using namespace CVC4;
  20 using namespace std;
  21 using namespace CVC4::theory;
  22 using namespace CVC4::theory::quantifiers;
  23 using namespace CVC4::kind;
  24
  25 struct sortTypeOrder {
  26   TermDb* d_tdb;
  27   bool operator() (TypeNode i, TypeNode j) {
  28     return d_tdb->getIdForType( i )<d_tdb->getIdForType( j );
  29   }
  30 };
  31
  32 bool AlphaEquivalenceNode::registerNode( AlphaEquivalenceNode* aen, QuantifiersEngine* qe, Node q, std::vector< Node >& tt, std::vector< int >& arg_index ) {
  33   while( !tt.empty() ){
  34     if( tt.size()==arg_index.size()+1 ){
  35       Node t = tt.back();
  36       Node op = t.hasOperator() ? t.getOperator() : t;
  37       arg_index.push_back( 0 );
  38       Trace("aeq-debug") << op << " ";
  39       aen = &(aen->d_children[op][t.getNumChildren()]);
  40     }else{
  41       Node t = tt.back();
  42       int i = arg_index.back();
  43       if( i==(int)t.getNumChildren() ){
  44         tt.pop_back();
  45         arg_index.pop_back();
  46       }else{
  47         tt.push_back( t[i] );
  48         arg_index[arg_index.size()-1]++;
  49       }
  50     }
  51   }
  52   Trace("aeq-debug") << std::endl;
  53   if( aen->d_quant.isNull() ){
  54     aen->d_quant = q;
  55     return true;
  56   }else{
  57     if( q.getNumChildren()==2 ){
  58       //lemma ( q <=> d_quant )
  59       Trace("quant-ae") << "Alpha equivalent : " << std::endl;
  60       Trace("quant-ae") << "  " << q << std::endl;
  61       Trace("quant-ae") << "  " << aen->d_quant << std::endl;
  62       qe->getOutputChannel().lemma( q.iffNode( aen->d_quant ) );
  63       return false;
  64     }else{
  65       //do not reduce annotated quantified formulas based on alpha equivalence
  66       return true;
  67     }
  68   }
  69 }
  70
  71 bool AlphaEquivalenceTypeNode::registerNode( AlphaEquivalenceTypeNode* aetn,
  72                                              QuantifiersEngine* qe, Node q, Node t, std::vector< TypeNode >& typs, std::map< TypeNode, int >& typ_count, int index ){
  73   while( index<(int)typs.size() ){
  74     TypeNode curr = typs[index];
  75     Assert( typ_count.find( curr )!=typ_count.end() );
  76     Trace("aeq-debug") << "[" << curr << " " << typ_count[curr] << "] ";
  77     aetn = &(aetn->d_children[curr][typ_count[curr]]);
  78     index = index + 1;
  79   }
  80   std::vector< Node > tt;
  81   std::vector< int > arg_index;
  82   tt.push_back( t );
  83   Trace("aeq-debug") << " : ";
  84   return AlphaEquivalenceNode::registerNode( &(aetn->d_data), qe, q, tt, arg_index );
  85 }
  86
  87 bool AlphaEquivalence::reduceQuantifier( Node q ) {
  88   Assert( q.getKind()==FORALL );
  89   Trace("aeq") << "Alpha equivalence : register " << q << std::endl;
  90   //construct canonical quantified formula
  91   Node t = d_qe->getTermDatabase()->getCanonicalTerm( q[1], true );
  92   Trace("aeq") << "  canonical form: " << t << std::endl;
  93   //compute variable type counts
  94   std::map< TypeNode, int > typ_count;
  95   std::vector< TypeNode > typs;
  96   for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
  97     TypeNode tn = q[0][i].getType();
  98     typ_count[tn]++;
  99     if( std::find( typs.begin(), typs.end(), tn )==typs.end() ){
 100       typs.push_back( tn );
 101     }
 102   }
 103   sortTypeOrder sto;
 104   sto.d_tdb = d_qe->getTermDatabase();
 105   std::sort( typs.begin(), typs.end(), sto );
 106   Trace("aeq-debug") << "  ";
 107   bool ret = !AlphaEquivalenceTypeNode::registerNode( &d_ae_typ_trie, d_qe, q, t, typs, typ_count );
 108   Trace("aeq") << "  ...result : " << ret << std::endl;
 109   return ret;
 110 }