Restrict LtePartialInst instantiations based on E-matching, promote to quantifiers module. Refactor QuantifiersEngine registration and check.

1 files changed, 0 insertions, 139 deletions

diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp
index 088ba093f..f73bc7bb2 100644
--- a/src/theory/quantifiers/quant_util.cpp
+++ b/src/theory/quantifiers/quant_util.cpp
@@ -255,142 +255,3 @@ void QuantPhaseReq::getPolarity( Node n, int child, bool hasPol, bool pol, bool&
     }
   }
 }
-
-
-QuantLtePartialInst::QuantLtePartialInst( QuantifiersEngine * qe, context::Context* c ) : d_wasInvoked( false ), d_qe( qe ), d_lte_asserts( c ){
-
-}
-
-/** add quantifier */
-bool QuantLtePartialInst::addQuantifier( Node q ) {
-  if( d_do_inst.find( q )!=d_do_inst.end() ){
-    if( d_do_inst[q] ){
-      d_lte_asserts.push_back( q );
-      return true;
-    }else{
-      return false;
-    }
-  }else{
-    d_vars[q].clear();
-    //check if this quantified formula is eligible for partial instantiation
-    std::map< Node, bool > vars;
-    for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
-      vars[q[0][i]] = true;
-    }
-    getEligibleInstVars( q[1], vars );
-
-    //TODO : instantiate only if we would force ground instances?
-    bool doInst = true;
-    for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
-      if( vars[q[0][i]] ){
-        d_vars[q].push_back( q[0][i] );
-      }else{
-        doInst = false;
-        break;
-      }
-    }
-    Trace("lte-partial-inst") << "LTE: ...will " << ( doInst ? "" : "not ") << "instantiate " << q << std::endl;
-    d_do_inst[q] = doInst;
-    if( doInst ){
-      d_lte_asserts.push_back( q );
-    }
-    return doInst;
-  }
-}
-
-void QuantLtePartialInst::getEligibleInstVars( Node n, std::map< Node, bool >& vars ) {
-  if( n.getKind()!=APPLY_UF || n.getType().isBoolean() ){
-    for( unsigned i=0; i<n.getNumChildren(); i++ ){
-      if( vars.find( n[i] )!=vars.end() ){
-        vars[n[i]] = false;
-      }
-    }
-  }
-  for( unsigned i=0; i<n.getNumChildren(); i++ ){
-    getEligibleInstVars( n[i], vars );
-  }
-}
-
-void QuantLtePartialInst::reset() {
-  d_reps.clear();
-  eq::EqualityEngine* ee = d_qe->getMasterEqualityEngine();
-  eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee );
-  while( !eqcs_i.isFinished() ){
-    TNode r = (*eqcs_i);
-    TypeNode tn = r.getType();
-    d_reps[tn].push_back( r );
-    ++eqcs_i;
-  }
-}
-
-/** get instantiations */
-void QuantLtePartialInst::getInstantiations( std::vector< Node >& lemmas ) {
-  Trace("lte-partial-inst") << "LTE : get instantiations, # quant = " << d_lte_asserts.size() << std::endl;
-  reset();
-  for( unsigned i=0; i<d_lte_asserts.size(); i++ ){
-    Node q = d_lte_asserts[i];
-    Assert( d_do_inst.find( q )!=d_do_inst.end() && d_do_inst[q] );
-    if( d_inst.find( q )==d_inst.end() ){
-      Trace("lte-partial-inst") << "LTE : Get partial instantiations for " << q << "..." << std::endl;
-      d_inst[q] = true;
-      Assert( !d_vars[q].empty() );
-      //make bound list
-      Node bvl;
-      std::vector< Node > bvs;
-      for( unsigned j=0; j<q[0].getNumChildren(); j++ ){
-        if( std::find( d_vars[q].begin(), d_vars[q].end(), q[0][j] )==d_vars[q].end() ){
-          bvs.push_back( q[0][j] );
-        }
-      }
-      if( !bvs.empty() ){
-        bvl = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, bvs );
-      }
-      std::vector< Node > conj;
-      std::vector< Node > terms;
-      std::vector< TypeNode > types;
-      for( unsigned j=0; j<d_vars[q].size(); j++ ){
-        types.push_back( d_vars[q][j].getType() );
-      }
-      getPartialInstantiations( conj, q, bvl, d_vars[q], terms, types, 0 );
-      Assert( !conj.empty() );
-      lemmas.push_back( NodeManager::currentNM()->mkNode( OR, q.negate(), conj.size()==1 ? conj[0] : NodeManager::currentNM()->mkNode( AND, conj ) ) );
-      d_wasInvoked = true;
-    }
-  }
-}
-
-void QuantLtePartialInst::getPartialInstantiations( std::vector< Node >& conj, Node q, Node bvl,
-                                                    std::vector< Node >& vars, std::vector< Node >& terms, std::vector< TypeNode >& types, unsigned index ){
-  if( index==vars.size() ){
-    Node body = q[1].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() );
-    if( bvl.isNull() ){
-      conj.push_back( body );
-      Trace("lte-partial-inst") << " - ground conjunct : " << body << std::endl;
-    }else{
-      Node nq;
-      if( q.getNumChildren()==3 ){
-        Node ipl = q[2].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() );
-        nq = NodeManager::currentNM()->mkNode( FORALL, bvl, body, ipl );
-      }else{
-        nq = NodeManager::currentNM()->mkNode( FORALL, bvl, body );
-      }
-      Trace("lte-partial-inst") << " - quantified conjunct : " << nq << std::endl;
-      LtePartialInstAttribute ltpia;
-      nq.setAttribute(ltpia,true);
-      conj.push_back( nq );
-    }
-  }else{
-    std::map< TypeNode, std::vector< Node > >::iterator it = d_reps.find( types[index] );
-    if( it!=d_reps.end() ){
-      terms.push_back( Node::null() );
-      Trace("lte-partial-inst-debug") << it->second.size() << " reps of type " << types[index] << std::endl;
-      for( unsigned i=0; i<it->second.size(); i++ ){
-        terms[index] = it->second[i];
-        getPartialInstantiations( conj, q, bvl, vars, terms, types, index+1 );
-      }
-      terms.pop_back();
-    }else{
-      Trace("lte-partial-inst-debug") << "No reps found of type " << types[index] << std::endl;
-    }
-  }
-}