Add option --lte-partial-inst. Remove inst-closure.

1 files changed, 140 insertions, 1 deletions

diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp
index 62a87bb99..2a9a764b9 100644
--- a/src/theory/quantifiers/quant_util.cpp
+++ b/src/theory/quantifiers/quant_util.cpp
@@ -15,6 +15,7 @@
 #include "theory/quantifiers/quant_util.h"
 #include "theory/quantifiers/inst_match.h"
 #include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers_engine.h"
 
 using namespace std;
 using namespace CVC4;
@@ -253,4 +254,142 @@ void QuantPhaseReq::getPolarity( Node n, int child, bool hasPol, bool pol, bool&
       newHasPol = false;
     }
   }
-}
\ No newline at end of file
+}
+
+
+QuantLtePartialInst::QuantLtePartialInst( QuantifiersEngine * qe, context::Context* c ) : 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 ) ) );
+    }
+  }
+}
+
+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;
+    }
+  }
+}