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

11 files changed, 216 insertions, 66 deletions

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index a83299d3b..81e93ebe6 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -2002,8 +2002,6 @@ builtinOp[CVC4::Kind& kind]
   
   | FMFCARD_TOK    { $kind = CVC4::kind::CARDINALITY_CONSTRAINT; }
   
-  | INST_CLOSURE_TOK  { $kind = CVC4::kind::INST_CLOSURE; }
-
   | FP_TOK        { $kind = CVC4::kind::FLOATINGPOINT_FP; }
   | FP_EQ_TOK     { $kind = CVC4::kind::FLOATINGPOINT_EQ; }
   | FP_ABS_TOK    { $kind = CVC4::kind::FLOATINGPOINT_ABS; }
@@ -2472,8 +2470,6 @@ DTSIZE_TOK : 'dt.size';
 
 FMFCARD_TOK : 'fmf.card';
 
-INST_CLOSURE_TOK : 'inst-closure';
-
 EMPTYSET_TOK: { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_SETS) }? 'emptyset';
 // Other set theory operators are not
 // tokenized and handled directly when
diff --git a/src/theory/quantifiers/kinds b/src/theory/quantifiers/kinds
index 793e4a611..a8774440e 100644
--- a/src/theory/quantifiers/kinds
+++ b/src/theory/quantifiers/kinds
@@ -44,8 +44,6 @@ sort INST_PATTERN_LIST_TYPE \
 # a list of instantiation patterns
 operator INST_PATTERN_LIST 1: "a list of instantiation patterns"
 
-operator INST_CLOSURE 1 "predicate for specifying term in instantiation closure."
-
 typerule FORALL ::CVC4::theory::quantifiers::QuantifierForallTypeRule 
 typerule EXISTS ::CVC4::theory::quantifiers::QuantifierExistsTypeRule 
 typerule BOUND_VAR_LIST ::CVC4::theory::quantifiers::QuantifierBoundVarListTypeRule 
@@ -53,7 +51,6 @@ typerule INST_PATTERN ::CVC4::theory::quantifiers::QuantifierInstPatternTypeRule
 typerule INST_NO_PATTERN ::CVC4::theory::quantifiers::QuantifierInstNoPatternTypeRule 
 typerule INST_ATTRIBUTE ::CVC4::theory::quantifiers::QuantifierInstAttributeTypeRule 
 typerule INST_PATTERN_LIST ::CVC4::theory::quantifiers::QuantifierInstPatternListTypeRule 
-typerule INST_CLOSURE ::CVC4::theory::quantifiers::QuantifierInstClosureTypeRule 
 
 # for rewrite rules
 # types...
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index afa894473..009a0ada6 100644
--- a/src/theory/quantifiers/options
+++ b/src/theory/quantifiers/options
@@ -205,7 +205,7 @@ option sygusNormalFormArg --sygus-nf-arg bool :default true
 
 option localTheoryExt --local-t-ext bool :default false
   do instantiation based on local theory extensions
-option termDbInstClosure --term-db-inst-closure bool :default false
-  only consider inst closure terms for E-matching
+option ltePartialInst --lte-partial-inst bool :default false
+  partially instantiate local theory quantifiers
  
 endmodule
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;
+    }
+  }
+}
diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h
index 575a7237d..c1c39fa0f 100644
--- a/src/theory/quantifiers/quant_util.h
+++ b/src/theory/quantifiers/quant_util.h
@@ -27,7 +27,8 @@
 namespace CVC4 {
 namespace theory {
 
-
+class QuantifiersEngine;
+  
 class QuantArith
 {
 public:
@@ -109,6 +110,34 @@ public:
   virtual void setLiberal( bool l ) = 0;
 };/* class EqualityQuery */
 
+class QuantLtePartialInst {
+private:
+  std::map< TypeNode, std::vector< Node > > d_reps;
+  // should we instantiate quantifier
+  std::map< Node, bool > d_do_inst;
+  // have we instantiated quantifier
+  std::map< Node, bool > d_inst;
+  std::map< Node, std::vector< Node > > d_vars;
+  /** pointer to quant engine */
+  QuantifiersEngine * d_qe;
+  /** list of relevant quantifiers asserted in the current context */
+  context::CDList<Node> d_lte_asserts;
+  /** reset */
+  void reset();
+  /** get instantiations */
+  void getPartialInstantiations( std::vector< Node >& conj, Node q, Node bvl, 
+                                 std::vector< Node >& vars, std::vector< Node >& inst, std::vector< TypeNode >& types, unsigned index );
+  /** get eligible inst variables */
+  void getEligibleInstVars( Node n, std::map< Node, bool >& vars );
+public:
+  QuantLtePartialInst( QuantifiersEngine * qe, context::Context* c );
+  /** add quantifier */
+  bool addQuantifier( Node q );
+  /** get instantiations */
+  void getInstantiations( std::vector< Node >& lemmas );
+};
+
+
 }
 }
 
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index efa12b893..bb0b3248d 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -111,7 +111,7 @@ Node TermDb::getOperator( Node n ) {
   }
 }
 
-void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant, bool withinInstClosure ){
+void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){
   //don't add terms in quantifier bodies
   if( withinQuant && !options::registerQuantBodyTerms() ){
     return;
@@ -119,9 +119,6 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant, bool wi
   bool rec = false;
   if( d_processed.find( n )==d_processed.end() ){
     d_processed.insert(n);
-    if( withinInstClosure ){
-      d_iclosure_processed.insert( n );
-    }
     d_type_map[ n.getType() ].push_back( n );
     //if this is an atomic trigger, consider adding it
     //Call the children?
@@ -154,13 +151,10 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant, bool wi
       }
     }
     rec = true;
-  }else if( withinInstClosure && d_iclosure_processed.find( n )==d_iclosure_processed.end() ){
-    d_iclosure_processed.insert( n );
-    rec = true;
   }
   if( rec ){
     for( size_t i=0; i<n.getNumChildren(); i++ ){
-      addTerm( n[i], added, withinQuant, withinInstClosure );
+      addTerm( n[i], added, withinQuant );
     }
   }
 }
@@ -325,18 +319,14 @@ bool TermDb::isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep,
 }
 
 bool TermDb::hasTermCurrent( Node n ) {
-  if( options::termDbInstClosure() && d_iclosure_processed.find( n )==d_iclosure_processed.end() ){
-    return false;
+  //return d_quantEngine->getMasterEqualityEngine()->hasTerm( n ); //some assertions are not sent to EE
+  if( options::termDbMode()==TERM_DB_ALL ){
+    return true;
+  }else if( options::termDbMode()==TERM_DB_RELEVANT ){
+    return d_has_map.find( n )!=d_has_map.end();
   }else{
-    //return d_quantEngine->getMasterEqualityEngine()->hasTerm( n ); //some assertions are not sent to EE
-    if( options::termDbMode()==TERM_DB_ALL ){
-      return true;
-    }else if( options::termDbMode()==TERM_DB_RELEVANT ){
-      return d_has_map.find( n )!=d_has_map.end();
-    }else{
-      Assert( false );
-      return false;
-    }
+    Assert( false );
+    return false;
   }
 }
 
@@ -344,6 +334,7 @@ Node TermDb::getHasTermEqc( Node r ) {
   if( hasTermCurrent( r ) ){
     return r;
   }else{
+    /*
     if( options::termDbInstClosure()  ){
       std::map< Node, Node >::iterator it = d_has_eqc.find( r );
       if( it==d_has_eqc.end() ){
@@ -362,10 +353,10 @@ Node TermDb::getHasTermEqc( Node r ) {
       }else{
         return it->second;
       }
-    }else{
-      //if not using inst closure, then either all are relevant, or it is a singleton irrelevant eqc
-      return Node::null();
     }
+    */
+    //if not using inst closure, then either all are relevant, or it is a singleton irrelevant eqc
+    return Node::null();
   }
 }
 
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index cb9f5eeef..fca2e1261 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -84,6 +84,10 @@ typedef expr::Attribute<QuantInstLevelAttributeId, uint64_t> QuantInstLevelAttri
 struct RrPriorityAttributeId {};
 typedef expr::Attribute<RrPriorityAttributeId, uint64_t> RrPriorityAttribute;
 
+/** Attribute true for quantifiers that do not need to be partially instantiated */
+struct LtePartialInstAttributeId {};
+typedef expr::Attribute< LtePartialInstAttributeId, bool > LtePartialInstAttribute;
+
 class QuantifiersEngine;
 
 namespace inst{
@@ -123,8 +127,6 @@ private:
   QuantifiersEngine* d_quantEngine;
   /** terms processed */
   std::hash_set< Node, NodeHashFunction > d_processed;
-  /** terms processed */
-  std::hash_set< Node, NodeHashFunction > d_iclosure_processed;
 private:
   /** select op map */
   std::map< Node, std::map< TypeNode, Node > > d_par_op_map;
@@ -156,7 +158,7 @@ public:
   /** map from type nodes to terms of that type */
   std::map< TypeNode, std::vector< Node > > d_type_map;
   /** add a term to the database */
-  void addTerm( Node n, std::set< Node >& added, bool withinQuant = false, bool withinInstClosure = false );
+  void addTerm( Node n, std::set< Node >& added, bool withinQuant = false );
   /** reset (calculate which terms are active) */
   void reset( Theory::Effort effort );
   /** get operator*/
diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp
index de0f98af6..89549a71b 100644
--- a/src/theory/quantifiers/theory_quantifiers.cpp
+++ b/src/theory/quantifiers/theory_quantifiers.cpp
@@ -129,22 +129,12 @@ void TheoryQuantifiers::check(Effort e) {
     case kind::FORALL:
       assertUniversal( assertion );
       break;
-    case kind::INST_CLOSURE:
-      getQuantifiersEngine()->addTermToDatabase( assertion[0], false, true );
-      break;
-    case kind::EQUAL:
-      //do nothing
-      break;
     case kind::NOT:
       {
         switch( assertion[0].getKind()) {
         case kind::FORALL:
           assertExistential( assertion );
           break;
-        case kind::EQUAL:
-          //do nothing
-          break;
-        case kind::INST_CLOSURE: //cannot negate inst closure
         default:
           Unhandled(assertion[0].getKind());
           break;
diff --git a/src/theory/quantifiers/theory_quantifiers_type_rules.h b/src/theory/quantifiers/theory_quantifiers_type_rules.h
index 341e656c7..2d5cce6ed 100644
--- a/src/theory/quantifiers/theory_quantifiers_type_rules.h
+++ b/src/theory/quantifiers/theory_quantifiers_type_rules.h
@@ -125,21 +125,6 @@ struct QuantifierInstPatternListTypeRule {
   }
 };/* struct QuantifierInstPatternListTypeRule */
 
-
-struct QuantifierInstClosureTypeRule {
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-    throw(TypeCheckingExceptionPrivate) {
-    Assert(n.getKind() == kind::INST_CLOSURE );
-    if( check ){
-      TypeNode tn = n[0].getType(check);
-      if( tn.isBoolean() ){
-        throw TypeCheckingExceptionPrivate(n, "argument of inst-closure must be non-boolean");
-      }
-    }
-    return nodeManager->booleanType();
-  }
-};/* struct QuantifierInstClosureTypeRule */
-
 class RewriteRuleTypeRule {
 public:
 
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index d6c6f4667..3ef5b4a65 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -153,6 +153,11 @@ d_lemmas_produced_c(u){
   }else{
     d_ceg_inst = NULL;
   }
+  if( options::ltePartialInst() ){
+    d_lte_part_inst = new QuantLtePartialInst( this, c );
+  }else{
+    d_lte_part_inst = NULL;
+  }
   
   if( needsBuilder ){
     Trace("quant-engine-debug") << "Initialize model engine, mbqi : " << options::mbqiMode() << " " << options::fmfBoundInt() << std::endl;
@@ -191,6 +196,7 @@ QuantifiersEngine::~QuantifiersEngine(){
   delete d_eq_query;
   delete d_sg_gen;
   delete d_ceg_inst;
+  delete d_lte_part_inst;
   for(std::map< Node, QuantPhaseReq* >::iterator i = d_phase_reqs.begin(); i != d_phase_reqs.end(); ++i) {
     delete (*i).second;
   }
@@ -254,10 +260,14 @@ void QuantifiersEngine::check( Theory::Effort e ){
   }
   if( e==Theory::EFFORT_FULL ){
     d_ierCounter++;
+    //process partial instantiations for LTE
+    if( d_lte_part_inst ){
+      d_lte_part_inst->getInstantiations( d_lemmas_waiting );
+    }
   }else if( e==Theory::EFFORT_LAST_CALL ){
     d_ierCounter_lc++;
   }
-  bool needsCheck = false;
+  bool needsCheck = !d_lemmas_waiting.empty();
   bool needsModel = false;
   bool needsFullModel = false;
   std::vector< QuantifiersModule* > qm;
@@ -285,6 +295,9 @@ void QuantifiersEngine::check( Theory::Effort e ){
     }
     Trace("quant-engine-debug") << std::endl;
     Trace("quant-engine-debug") << "  # quantified formulas = " << d_model->getNumAssertedQuantifiers() << std::endl;
+    if( !d_lemmas_waiting.empty() ){
+      Trace("quant-engine-debug") << "  lemmas waiting = " << d_lemmas_waiting.size() << std::endl;
+    }
     Trace("quant-engine-debug") << "  Theory engine finished : " << !d_te->needCheck() << std::endl;
 
     Trace("quant-engine-ee") << "Equality engine : " << std::endl;
@@ -295,7 +308,7 @@ void QuantifiersEngine::check( Theory::Effort e ){
     d_conflict = false;
     d_hasAddedLemma = false;
 
-    //flush previous lemmas (for instance, if was interupted)
+    //flush previous lemmas (for instance, if was interupted), or other lemmas to process
     flushLemmas();
     if( d_hasAddedLemma ){
       return;
@@ -450,6 +463,12 @@ void QuantifiersEngine::assertQuantifier( Node f, bool pol ){
   }
   //assert to modules TODO : handle !pol
   if( pol ){
+    if( d_lte_part_inst && !f.getAttribute(LtePartialInstAttribute()) ){
+      Trace("lte-partial-inst") << "LTE: Partially instantiate " << f << "?" << std::endl;
+      if( d_lte_part_inst->addQuantifier( f ) ){
+        return;
+      }
+    }
     //register the quantifier
     registerQuantifier( f );
     //assert it to each module
@@ -478,9 +497,9 @@ Node QuantifiersEngine::getNextDecisionRequest(){
   return Node::null();
 }
 
-void QuantifiersEngine::addTermToDatabase( Node n, bool withinQuant, bool withinInstClosure ){
+void QuantifiersEngine::addTermToDatabase( Node n, bool withinQuant ){
   std::set< Node > added;
-  getTermDatabase()->addTerm( n, added, withinQuant, withinInstClosure );
+  getTermDatabase()->addTerm( n, added, withinQuant );
   //maybe have triggered instantiations if we are doing eager instantiation
   if( options::eagerInstQuant() ){
     flushLemmas();
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index ac782a536..2fc479f4c 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -134,6 +134,8 @@ private:
   quantifiers::ConjectureGenerator * d_sg_gen;
   /** ceg instantiation */
   quantifiers::CegInstantiation * d_ceg_inst;
+  /** lte partial instantiation */
+  QuantLtePartialInst * d_lte_part_inst;
 public: //effort levels
   enum {
     QEFFORT_CONFLICT,
@@ -295,7 +297,7 @@ public:
   /** get trigger database */
   inst::TriggerTrie* getTriggerDatabase() { return d_tr_trie; }
   /** add term to database */
-  void addTermToDatabase( Node n, bool withinQuant = false, bool withinInstClosure = false );
+  void addTermToDatabase( Node n, bool withinQuant = false );
   /** get the master equality engine */
   eq::EqualityEngine* getMasterEqualityEngine() ;
   /** debug print equality engine */