src/theory/quantifiers/first_order_reasoning.cpp

   1 /*********************                                                        */
   2 /*! \file first_order_reasoning.cpp
   3  ** \verbatim
   4  ** Original author: Andrew Reynolds
   5  ** Major contributors: Morgan Deters
   6  ** Minor contributors (to current version): none
   7  ** This file is part of the CVC4 project.
   8  ** Copyright (c) 2009-2014  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 first order reasoning module
  13  **
  14  **/
  15
  16 #include <vector>
  17
  18 #include "theory/quantifiers/first_order_reasoning.h"
  19 #include "theory/rewriter.h"
  20 #include "proof/proof_manager.h"
  21
  22 using namespace CVC4;
  23 using namespace std;
  24 using namespace CVC4::theory;
  25 using namespace CVC4::theory::quantifiers;
  26 using namespace CVC4::kind;
  27
  28
  29 void FirstOrderPropagation::collectLits( Node n, std::vector<Node> & lits ){
  30   if( n.getKind()==FORALL ){
  31     collectLits( n[1], lits );
  32   }else if( n.getKind()==OR ){
  33     for(unsigned j=0; j<n.getNumChildren(); j++) {
  34       collectLits(n[j], lits );
  35     }
  36   }else{
  37     lits.push_back( n );
  38   }
  39 }
  40
  41 void FirstOrderPropagation::simplify( std::vector< Node >& assertions ){
  42   for( unsigned i=0; i<assertions.size(); i++) {
  43     Trace("fo-rsn") << "Assert : " << assertions[i] << std::endl;
  44   }
  45
  46   //process all assertions
  47   int num_processed;
  48   int num_true = 0;
  49   int num_rounds = 0;
  50   do {
  51     num_processed = 0;
  52     for( unsigned i=0; i<assertions.size(); i++ ){
  53       if( d_assertion_true.find(assertions[i])==d_assertion_true.end() ){
  54         std::vector< Node > fo_lits;
  55         collectLits( assertions[i], fo_lits );
  56         Node unitLit = process( assertions[i], fo_lits );
  57         if( !unitLit.isNull() ){
  58           Trace("fo-rsn-debug") << "...possible unit literal : " << unitLit << " from " << assertions[i] << std::endl;
  59           bool pol = unitLit.getKind()!=NOT;
  60           unitLit = unitLit.getKind()==NOT ? unitLit[0] : unitLit;
  61           if( unitLit.getKind()==EQUAL ){
  62
  63           }else if( unitLit.getKind()==APPLY_UF ){
  64             //make sure all are unique vars;
  65             bool success = true;
  66             std::vector< Node > unique_vars;
  67             for( unsigned j=0; j<unitLit.getNumChildren(); j++) {
  68               if( unitLit[j].getKind()==BOUND_VARIABLE ){
  69                 if( std::find(unique_vars.begin(), unique_vars.end(), unitLit[j])==unique_vars.end() ){
  70                   unique_vars.push_back( unitLit[j] );
  71                 }else{
  72                   success = false;
  73                   break;
  74                 }
  75               }else{
  76                 success = false;
  77                 break;
  78               }
  79             }
  80             if( success ){
  81               d_const_def[unitLit.getOperator()] = NodeManager::currentNM()->mkConst(pol);
  82               Trace("fo-rsn") << "Propagate : " << unitLit.getOperator() << " == " << pol << std::endl;
  83               Trace("fo-rsn") << "    from : " << assertions[i] << std::endl;
  84               d_assertion_true[assertions[i]] = true;
  85               num_processed++;
  86             }
  87           }else if( unitLit.getKind()==VARIABLE ){
  88             d_const_def[unitLit] = NodeManager::currentNM()->mkConst(pol);
  89             Trace("fo-rsn") << "Propagate variable : " << unitLit << " == " << pol << std::endl;
  90             Trace("fo-rsn") << "    from : " << assertions[i] << std::endl;
  91             d_assertion_true[assertions[i]] = true;
  92             num_processed++;
  93           }
  94         }
  95         if( d_assertion_true.find(assertions[i])!=d_assertion_true.end() ){
  96           num_true++;
  97         }
  98       }
  99     }
 100     num_rounds++;
 101   }while( num_processed>0 );
 102   Trace("fo-rsn-sum") << "Simplified " << num_true << " / " << assertions.size() << " in " << num_rounds << " rounds." << std::endl;
 103   for( unsigned i=0; i<assertions.size(); i++ ){
 104     Node curr = simplify( assertions[i] );
 105     if( curr!=assertions[i] ){
 106       curr = Rewriter::rewrite( curr );
 107       PROOF( ProofManager::currentPM()->addDependence(curr, assertions[i]); );
 108       assertions[i] = curr;
 109     }
 110   }
 111 }
 112
 113 Node FirstOrderPropagation::process(Node a, std::vector< Node > & lits) {
 114   int index = -1;
 115   for( unsigned i=0; i<lits.size(); i++) {
 116     bool pol = lits[i].getKind()!=NOT;
 117     Node n = lits[i].getKind()==NOT ? lits[i][0] : lits[i];
 118     Node litDef;
 119     if( n.getKind()==APPLY_UF ){
 120       if( d_const_def.find(n.getOperator())!=d_const_def.end() ){
 121         litDef = d_const_def[n.getOperator()];
 122       }
 123     }else if( n.getKind()==VARIABLE ){
 124       if( d_const_def.find(n)!=d_const_def.end() ){
 125         litDef = d_const_def[n];
 126       }
 127     }
 128     if( !litDef.isNull() ){
 129       Node poln = NodeManager::currentNM()->mkConst( pol );
 130       if( litDef==poln ){
 131         Trace("fo-rsn-debug") << "Assertion " << a << " is true because of " << lits[i] << std::endl;
 132         d_assertion_true[a] = true;
 133         return Node::null();
 134       }
 135     }
 136     if( litDef.isNull() ){
 137       if( index==-1 ){
 138         //store undefined index
 139         index = i;
 140       }else{
 141         //two undefined, return null
 142         return Node::null();
 143       }
 144     }
 145   }
 146   if( index!=-1 ){
 147     return lits[index];
 148   }else{
 149     return Node::null();
 150   }
 151 }
 152
 153 Node FirstOrderPropagation::simplify( Node n ) {
 154   if( n.getKind()==VARIABLE ){
 155     if( d_const_def.find(n)!=d_const_def.end() ){
 156       return d_const_def[n];
 157     }
 158   }else if( n.getKind()==APPLY_UF ){
 159     if( d_const_def.find(n.getOperator())!=d_const_def.end() ){
 160       return d_const_def[n.getOperator()];
 161     }
 162   }
 163   if( n.getNumChildren()==0 ){
 164     return n;
 165   }else{
 166     std::vector< Node > children;
 167     if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
 168       children.push_back( n.getOperator() );
 169     }
 170     for(unsigned i=0; i<n.getNumChildren(); i++) {
 171       children.push_back( simplify(n[i]) );
 172     }
 173     return NodeManager::currentNM()->mkNode( n.getKind(), children );
 174   }
 175 }