Add --lte-restrict-inst-closure option. Push dt.size fairness constraints inside splitting lemmas for sygus.

7 files changed, 247 insertions, 175 deletions

diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp
index c7b3e69c4..ee8169db7 100644
--- a/src/theory/datatypes/datatypes_sygus.cpp
+++ b/src/theory/datatypes/datatypes_sygus.cpp
@@ -110,6 +110,7 @@ void SygusSplit::getSygusSplits( Node n, const Datatype& dt, std::vector< Node >
     Node arg1;
     Kind parentKind = UNDEFINED_KIND;
     TypeNode tnnp;
+    Node ptest;
     if( n.getKind()==APPLY_SELECTOR_TOTAL ){
       Node op = n.getOperator();
       Expr selectorExpr = op.toExpr();
@@ -133,13 +134,13 @@ void SygusSplit::getSygusSplits( Node n, const Datatype& dt, std::vector< Node >
           }
         }
       }
-      
+
       // we are splitting on a term that may later have no semantics : guard this case
-      Node ptest = DatatypesRewriter::mkTester( n[0], csIndex, pdt ).negate();
+      ptest = DatatypesRewriter::mkTester( n[0], csIndex, pdt );
       Trace("sygus-split-debug") << "Parent guard : " << ptest << std::endl;
-      d_splits[n].push_back( ptest );
     }
-
+    std::vector< Node > ptest_c;
+    bool narrow = false;
     for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
       Trace("sygus-split-debug2") << "Add split " << n << " : constructor " << i << " : ";
       Assert( d_sygus_nred.find( tnn )!=d_sygus_nred.end() );
@@ -151,7 +152,7 @@ void SygusSplit::getSygusSplits( Node n, const Datatype& dt, std::vector< Node >
         }
         if( addSplit ){
           Node test = DatatypesRewriter::mkTester( n, i, dt );
-          
+
           //check if we can strengthen the first argument
           if( !arg1.isNull() ){
             std::map< int, std::vector< int > >::iterator it = d_sygus_pc_arg_pos[tnn][csIndex].find( i );
@@ -164,24 +165,48 @@ void SygusSplit::getSygusSplits( Node n, const Datatype& dt, std::vector< Node >
               Node argStr = lem_c.size()==1 ? lem_c[0] : NodeManager::currentNM()->mkNode( OR, lem_c );
               Trace("sygus-str") << "...strengthen corresponding first argument of " << test << " : " << argStr << std::endl;
               test = NodeManager::currentNM()->mkNode( AND, test, argStr );
+              narrow = true;
             }
           }
+          //add fairness constraint
+          if( options::ceGuidedInstFair()==quantifiers::CEGQI_FAIR_DT_SIZE ){
+            Node szl = NodeManager::currentNM()->mkNode( DT_SIZE, n );
+            Node szr = NodeManager::currentNM()->mkNode( DT_SIZE, DatatypesRewriter::getInstCons( n, dt, i ) );
+            szr = Rewriter::rewrite( szr );
+            test = NodeManager::currentNM()->mkNode( AND, test, szl.eqNode( szr ) );
+          }
           d_splits[n].push_back( test );
           Trace("sygus-split-debug2") << "SUCCESS" << std::endl;
           Trace("sygus-split") << "Disjunct #" << d_splits[n].size() << " : " << test << std::endl;
         }else{
           Trace("sygus-split-debug2") << "redundant argument" << std::endl;
+          narrow = true;
         }
       }else{
         Trace("sygus-split-debug2") << "redundant operator" << std::endl;
+        narrow = true;
+      }
+      if( !ptest.isNull() ){
+        ptest_c.push_back( DatatypesRewriter::mkTester( n, i, dt ) );
       }
     }
-    
     if( d_splits[n].empty() ){
       //possible
-      
+      exit( 3 );
+
       Assert( false );
     }
+    if( narrow && !ptest.isNull() ){
+      Node split = d_splits[n].size()==1 ? d_splits[n][0] : NodeManager::currentNM()->mkNode( OR, d_splits[n] );
+      d_splits[n].clear();
+      split = NodeManager::currentNM()->mkNode( AND, ptest, split );
+      d_splits[n].push_back( split );
+      if( !ptest_c.empty() ){
+        ptest = NodeManager::currentNM()->mkNode( AND, ptest.negate(), NodeManager::currentNM()->mkNode( OR, ptest_c ) );
+      }
+      d_splits[n].push_back( ptest );
+    }
+
   }
   //copy to splits
   splits.insert( splits.end(), d_splits[n].begin(), d_splits[n].end() );
@@ -213,33 +238,35 @@ void SygusSplit::registerSygusType( TypeNode tn, const Datatype& dt ) {
     //compute the redundant operators
     for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
       bool nred = true;
-      std::map< int, Kind >::iterator it = d_arg_kind[tn].find( i );
-      if( it!=d_arg_kind[tn].end() ){
-        Kind dk;
-        if( isAntisymmetric( it->second, dk ) ){
-          std::map< Kind, int >::iterator ita = d_kinds[tn].find( dk );
-          if( ita!=d_kinds[tn].end() ){
-            Trace("sygus-split-debug") << "Possible redundant operator : " << it->second << " with " << dk << std::endl;
-            //check for type mismatches
-            bool success = true;
-            unsigned j = ita->second;
-            for( unsigned k=0; k<2; k++ ){
-              unsigned ko = k==0 ? 1 : 0;
-              TypeNode tni = TypeNode::fromType( ((SelectorType)dt[i][k].getType()).getRangeType() );
-              TypeNode tnj = TypeNode::fromType( ((SelectorType)dt[j][ko].getType()).getRangeType() );
-              if( tni!=tnj ){
-                Trace("sygus-split-debug") << "Argument types " << tni << " and " << tnj << " are not equal." << std::endl;
-                success = false;
-                break;
+      if( options::sygusNormalForm() ){
+        std::map< int, Kind >::iterator it = d_arg_kind[tn].find( i );
+        if( it!=d_arg_kind[tn].end() ){
+          Kind dk;
+          if( isAntisymmetric( it->second, dk ) ){
+            std::map< Kind, int >::iterator ita = d_kinds[tn].find( dk );
+            if( ita!=d_kinds[tn].end() ){
+              Trace("sygus-split-debug") << "Possible redundant operator : " << it->second << " with " << dk << std::endl;
+              //check for type mismatches
+              bool success = true;
+              unsigned j = ita->second;
+              for( unsigned k=0; k<2; k++ ){
+                unsigned ko = k==0 ? 1 : 0;
+                TypeNode tni = TypeNode::fromType( ((SelectorType)dt[i][k].getType()).getRangeType() );
+                TypeNode tnj = TypeNode::fromType( ((SelectorType)dt[j][ko].getType()).getRangeType() );
+                if( tni!=tnj ){
+                  Trace("sygus-split-debug") << "Argument types " << tni << " and " << tnj << " are not equal." << std::endl;
+                  success = false;
+                  break;
+                }
+              }
+              if( success ){
+                Trace("sygus-nf") << "* Sygus norm " << dt.getName() << " : do not consider any " << d_arg_kind[tn][i] << " terms." << std::endl;
+                nred = false;
               }
-            }
-            if( success ){
-              Trace("sygus-nf") << "* Sygus norm " << dt.getName() << " : do not consider any " << d_arg_kind[tn][i] << " terms." << std::endl;
-              nred = false;
             }
           }
+          //NAND,NOR
         }
-        //NAND,NOR
       }
       d_sygus_nred[tn].push_back( nred );
     }
@@ -251,85 +278,92 @@ void SygusSplit::registerSygusTypeConstructorArg( TypeNode tnn, const Datatype&
   if( it==d_sygus_pc_nred[tnn][csIndex].end() ){
     registerSygusType( tnnp, pdt );
     Trace("sygus-split") << "Register type constructor arg " << dt.getName() << " " << csIndex << " " << sIndex << std::endl;
-    //get parent kind
-    bool hasParentKind = false;
-    Kind parentKind;
-    if( isKindArg( tnnp, csIndex ) ){
-      hasParentKind = true;
-      parentKind = d_arg_kind[tnnp][csIndex];
-    }
-    for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
-      bool addSplit = d_sygus_nred[tnn][i];
-      if( addSplit && hasParentKind ){
-        if( d_arg_kind.find( tnn )!=d_arg_kind.end() && d_arg_kind[tnn].find( i )!=d_arg_kind[tnn].end() ){
-          addSplit = considerSygusSplitKind( dt, pdt, tnn, tnnp, d_arg_kind[tnn][i], parentKind, sIndex );
-          if( !addSplit ){
-            Trace("sygus-nf") << "* Sygus norm " << pdt.getName() << " : do not consider " << dt.getName() << "::" << d_arg_kind[tnn][i];
-            Trace("sygus-nf") << " as argument " << sIndex << " of " << parentKind << "." << std::endl;
-          }
-        }else if( d_arg_const.find( tnn )!=d_arg_const.end() && d_arg_const[tnn].find( i )!=d_arg_const[tnn].end() ){
-          addSplit = considerSygusSplitConst( dt, pdt, tnn, tnnp, d_arg_const[tnn][i], parentKind, sIndex );
-          if( !addSplit ){
-            Trace("sygus-nf") << "* Sygus norm " << pdt.getName() << " : do not consider constant " << dt.getName() << "::" << d_arg_const[tnn][i];
-            Trace("sygus-nf") << " as argument " << sIndex << " of " << parentKind << "." << std::endl;
+    if( !options::sygusNormalForm() ){
+      for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
+        d_sygus_pc_nred[tnn][csIndex][sIndex].push_back( true );
+      }
+    }else{
+      // calculate which constructors we should consider based on normal form for terms
+      //get parent kind
+      bool hasParentKind = false;
+      Kind parentKind;
+      if( isKindArg( tnnp, csIndex ) ){
+        hasParentKind = true;
+        parentKind = d_arg_kind[tnnp][csIndex];
+      }
+      for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
+        bool addSplit = d_sygus_nred[tnn][i];
+        if( addSplit && hasParentKind ){
+          if( d_arg_kind.find( tnn )!=d_arg_kind.end() && d_arg_kind[tnn].find( i )!=d_arg_kind[tnn].end() ){
+            addSplit = considerSygusSplitKind( dt, pdt, tnn, tnnp, d_arg_kind[tnn][i], parentKind, sIndex );
+            if( !addSplit ){
+              Trace("sygus-nf") << "* Sygus norm " << pdt.getName() << " : do not consider " << dt.getName() << "::" << d_arg_kind[tnn][i];
+              Trace("sygus-nf") << " as argument " << sIndex << " of " << parentKind << "." << std::endl;
+            }
+          }else if( d_arg_const.find( tnn )!=d_arg_const.end() && d_arg_const[tnn].find( i )!=d_arg_const[tnn].end() ){
+            addSplit = considerSygusSplitConst( dt, pdt, tnn, tnnp, d_arg_const[tnn][i], parentKind, sIndex );
+            if( !addSplit ){
+              Trace("sygus-nf") << "* Sygus norm " << pdt.getName() << " : do not consider constant " << dt.getName() << "::" << d_arg_const[tnn][i];
+              Trace("sygus-nf") << " as argument " << sIndex << " of " << parentKind << "." << std::endl;
+            }
           }
         }
+        d_sygus_pc_nred[tnn][csIndex][sIndex].push_back( addSplit );
       }
-      d_sygus_pc_nred[tnn][csIndex][sIndex].push_back( addSplit );
-    }
-    //also compute argument relationships
-    if( options::sygusNormalFormArg() ){
-      if( isKindArg( tnnp, csIndex ) && pdt[csIndex].getNumArgs()==2 ){
-        int osIndex = sIndex==0 ? 1 : 0;
-        if( isArgDatatype( pdt[csIndex], osIndex, dt ) ){
-          registerSygusTypeConstructorArg( tnn, dt, tnnp, pdt, csIndex, osIndex );
-          if( sIndex==0 ){
-            Assert( d_sygus_pc_nred[tnn][csIndex].find( sIndex )!=d_sygus_pc_nred[tnn][csIndex].end() );
-            Assert( d_sygus_pc_nred[tnn][csIndex].find( osIndex )!=d_sygus_pc_nred[tnn][csIndex].end() );
-            
-            Kind parentKind = d_arg_kind[tnnp][csIndex];
-            bool isPComm = isComm( parentKind );
-            for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
-              if( d_sygus_pc_nred[tnn][csIndex][osIndex][i] ){
-                //arguments that can be removed
-                std::map< int, bool > rem_arg;
-                if( isComm( parentKind ) ){
-                  for( unsigned j=0; j<dt.getNumConstructors(); j++ ){
-                    if( d_sygus_pc_nred[tnn][csIndex][sIndex][j] ){
-                      if( isPComm && j>i ){
-                        //based on commutativity 
-                        // use term ordering : constructor index of first argument is not greater than constructor index of second argument
-                        rem_arg[j] = true;
-                      }else{
-                        if( parentKind!=UNDEFINED_KIND && dt[i].getNumArgs()==0 && dt[j].getNumArgs()==0 ){
-                          Node nr = NodeManager::currentNM()->mkNode( parentKind, dt[j].getSygusOp(), dt[i].getSygusOp() );
-                          Node nrr = Rewriter::rewrite( nr );
-                          Trace("sygus-split-debug") << "  Test constant args : " << nr << " rewrites to " << nrr << std::endl;
-                          //based on rewriting
-                          // if rewriting the two arguments gives an operator that is in the parent syntax, remove the redundancy
-                          if( hasOp( tnnp, nrr ) ){
-                            Trace("sygus-nf") << "* Sygus norm : simplify based on rewrite " << nr << " -> " << nrr << std::endl;
-                            rem_arg[j] = true;
-                          }                                                          
+      //also compute argument relationships
+      if( options::sygusNormalFormArg() ){
+        if( isKindArg( tnnp, csIndex ) && pdt[csIndex].getNumArgs()==2 ){
+          int osIndex = sIndex==0 ? 1 : 0;
+          if( isArgDatatype( pdt[csIndex], osIndex, dt ) ){
+            registerSygusTypeConstructorArg( tnn, dt, tnnp, pdt, csIndex, osIndex );
+            if( sIndex==0 ){
+              Assert( d_sygus_pc_nred[tnn][csIndex].find( sIndex )!=d_sygus_pc_nred[tnn][csIndex].end() );
+              Assert( d_sygus_pc_nred[tnn][csIndex].find( osIndex )!=d_sygus_pc_nred[tnn][csIndex].end() );
+
+              Kind parentKind = d_arg_kind[tnnp][csIndex];
+              bool isPComm = isComm( parentKind );
+              for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
+                if( d_sygus_pc_nred[tnn][csIndex][osIndex][i] ){
+                  //arguments that can be removed
+                  std::map< int, bool > rem_arg;
+                  if( isComm( parentKind ) ){
+                    for( unsigned j=0; j<dt.getNumConstructors(); j++ ){
+                      if( d_sygus_pc_nred[tnn][csIndex][sIndex][j] ){
+                        if( isPComm && j>i ){
+                          //based on commutativity
+                          // use term ordering : constructor index of first argument is not greater than constructor index of second argument
+                          rem_arg[j] = true;
+                        }else{
+                          if( parentKind!=UNDEFINED_KIND && dt[i].getNumArgs()==0 && dt[j].getNumArgs()==0 ){
+                            Node nr = NodeManager::currentNM()->mkNode( parentKind, dt[j].getSygusOp(), dt[i].getSygusOp() );
+                            Node nrr = Rewriter::rewrite( nr );
+                            Trace("sygus-split-debug") << "  Test constant args : " << nr << " rewrites to " << nrr << std::endl;
+                            //based on rewriting
+                            // if rewriting the two arguments gives an operator that is in the parent syntax, remove the redundancy
+                            if( hasOp( tnnp, nrr ) ){
+                              Trace("sygus-nf") << "* Sygus norm : simplify based on rewrite " << nr << " -> " << nrr << std::endl;
+                              rem_arg[j] = true;
+                            }
+                          }
                         }
                       }
                     }
                   }
-                }
-                if( !rem_arg.empty() ){
-                  d_sygus_pc_arg_pos[tnn][csIndex][i].clear();
-                  Trace("sygus-split-debug") << "Possibilities for first argument of " << parentKind << ", when second argument is " << dt[i].getName() << " : " << std::endl;
-                  for( unsigned j=0; j<dt.getNumConstructors(); j++ ){
-                    if( d_sygus_pc_nred[tnn][csIndex][sIndex][j] && rem_arg.find( j )==rem_arg.end() ){
-                      d_sygus_pc_arg_pos[tnn][csIndex][i].push_back( j );
-                      Trace("sygus-split-debug") << "  " << dt[j].getName() << std::endl;
+                  if( !rem_arg.empty() ){
+                    d_sygus_pc_arg_pos[tnn][csIndex][i].clear();
+                    Trace("sygus-split-debug") << "Possibilities for first argument of " << parentKind << ", when second argument is " << dt[i].getName() << " : " << std::endl;
+                    for( unsigned j=0; j<dt.getNumConstructors(); j++ ){
+                      if( d_sygus_pc_nred[tnn][csIndex][sIndex][j] && rem_arg.find( j )==rem_arg.end() ){
+                        d_sygus_pc_arg_pos[tnn][csIndex][i].push_back( j );
+                        Trace("sygus-split-debug") << "  " << dt[j].getName() << std::endl;
+                      }
+                    }
+                    //if there are no possibilities for first argument, then this child is redundant
+                    if( d_sygus_pc_arg_pos[tnn][csIndex][i].empty() ){
+                      Trace("sygus-nf") << "* Sygus norm " << pdt.getName() << " : do not consider constant " << dt.getName() << "::" << dt[i].getName();
+                      Trace("sygus-nf") << " as argument " << osIndex << " of " << parentKind << " (based on arguments)." << std::endl;
+                      d_sygus_pc_nred[tnn][csIndex][osIndex][i] = false;
                     }
-                  }
-                  //if there are no possibilities for first argument, then this child is redundant
-                  if( d_sygus_pc_arg_pos[tnn][csIndex][i].empty() ){
-                    Trace("sygus-nf") << "* Sygus norm " << pdt.getName() << " : do not consider constant " << dt.getName() << "::" << dt[i].getName();
-                    Trace("sygus-nf") << " as argument " << osIndex << " of " << parentKind << " (based on arguments)." << std::endl;
-                    d_sygus_pc_nred[tnn][csIndex][osIndex][i] = false;
                   }
                 }
               }
@@ -477,24 +511,24 @@ bool SygusSplit::considerSygusSplitKind( const Datatype& dt, const Datatype& pdt
     Kind reqk = UNDEFINED_KIND;
     std::map< int, Kind > reqk_arg; //TODO
     if( parent==NOT ){
-      if( k==AND ) { 
+      if( k==AND ) {
         nk = OR;reqk = NOT;
-      }else if( k==OR ){ 
+      }else if( k==OR ){
         nk = AND;reqk = NOT;
-      }else if( k==IFF ) { 
+      }else if( k==IFF ) {
         nk = XOR;
-      }else if( k==XOR ) { 
+      }else if( k==XOR ) {
         nk = IFF;
       }
     }
     if( parent==BITVECTOR_NOT ){
-      if( k==BITVECTOR_AND ) { 
+      if( k==BITVECTOR_AND ) {
         nk = BITVECTOR_OR;reqk = BITVECTOR_NOT;
-      }else if( k==BITVECTOR_OR ){ 
+      }else if( k==BITVECTOR_OR ){
         nk = BITVECTOR_AND;reqk = BITVECTOR_NOT;
-      }else if( k==BITVECTOR_XNOR ) { 
+      }else if( k==BITVECTOR_XNOR ) {
         nk = BITVECTOR_XOR;
-      }else if( k==BITVECTOR_XOR ) { 
+      }else if( k==BITVECTOR_XOR ) {
         nk = BITVECTOR_XNOR;
       }
     }
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 501b3d86e..f9a451459 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -66,8 +66,8 @@ TheoryDatatypes::TheoryDatatypes(Context* c, UserContext* u, OutputChannel& out,
 
   d_true = NodeManager::currentNM()->mkConst( true );
   d_dtfCounter = 0;
-  
-  if( options::sygusNormalForm() ){
+
+  if( options::ceGuidedInst() ){
     d_sygus_split = new SygusSplit;
   }else{
     d_sygus_split = NULL;
@@ -360,6 +360,9 @@ void TheoryDatatypes::assertFact( Node fact, Node exp ){
   doPendingMerges();
   //add to tester if applicable
   if( atom.getKind()==kind::APPLY_TESTER ){
+    if( polarity ){
+      Trace("dt-tester") << "Assert tester : " << atom << std::endl;
+    }
     Node rep = getRepresentative( atom[0] );
     EqcInfo* eqc = getOrMakeEqcInfo( rep, true );
     addTester( fact, eqc, rep );
@@ -1070,26 +1073,30 @@ void TheoryDatatypes::collapseSelector( Node s, Node c ) {
     //  r = NodeManager::currentNM()->mkNode( kind::APPLY_UF, d_exp_def_skolem[s.getOperator().toExpr()], s[0] );
     //}else{
     r = NodeManager::currentNM()->mkNode( kind::APPLY_SELECTOR_TOTAL, s.getOperator(), c );
-  }else if( s.getKind()==DT_SIZE ){
-    r = NodeManager::currentNM()->mkNode( DT_SIZE, c );
-  }else if( s.getKind()==DT_HEIGHT_BOUND ){
-    r = NodeManager::currentNM()->mkNode( DT_HEIGHT_BOUND, c, s[1] );
-    if( r==d_true ){
-      return;
+  }else{
+    if( s.getKind()==DT_SIZE ){
+      r = NodeManager::currentNM()->mkNode( DT_SIZE, c );
+    }else if( s.getKind()==DT_HEIGHT_BOUND ){
+      r = NodeManager::currentNM()->mkNode( DT_HEIGHT_BOUND, c, s[1] );
+      if( r==d_true ){
+        return;
+      }
     }
   }
-  Node rr = Rewriter::rewrite( r );
-  if( s!=rr ){
-    Node eq_exp = c.eqNode( s[0] );
-    Node eq = rr.getType().isBoolean() ? s.iffNode( rr ) : s.eqNode( rr );
-    Trace("datatypes-infer") << "DtInfer : collapse sel";
-    Trace("datatypes-infer") << ( wrong ? " wrong" : "");
-    Trace("datatypes-infer") << " : " << eq << " by " << eq_exp << std::endl;
+  if( !r.isNull() ){
+    Node rr = Rewriter::rewrite( r );
+    if( s!=rr ){
+      Node eq_exp = c.eqNode( s[0] );
+      Node eq = rr.getType().isBoolean() ? s.iffNode( rr ) : s.eqNode( rr );
+      Trace("datatypes-infer") << "DtInfer : collapse sel";
+      Trace("datatypes-infer") << ( wrong ? " wrong" : "");
+      Trace("datatypes-infer") << " : " << eq << " by " << eq_exp << std::endl;
 
-    d_pending.push_back( eq );
-    d_pending_exp[ eq ] = eq_exp;
-    d_infer.push_back( eq );
-    d_infer_exp.push_back( eq_exp );
+      d_pending.push_back( eq );
+      d_pending_exp[ eq ] = eq_exp;
+      d_infer.push_back( eq );
+      d_infer_exp.push_back( eq_exp );
+    }
   }
 }
 
@@ -1116,8 +1123,8 @@ void TheoryDatatypes::computeCareGraph(){
       for( unsigned j=i+1; j<functionTerms; j++ ){
         TNode f2 = r==0 ? d_consTerms[j] : d_selTerms[j];
         Trace("dt-cg-debug") << "dt-cg: " << f1 << " and " << f2 << " " << (f1.getOperator()==f2.getOperator()) << " " << areEqual( f1, f2 ) << std::endl;
-        if( f1.getOperator()==f2.getOperator() && 
-            ( ( f1.getKind()!=DT_SIZE && f1.getKind()!=DT_HEIGHT_BOUND ) || f1[0].getType()==f2[0].getType() ) && 
+        if( f1.getOperator()==f2.getOperator() &&
+            ( ( f1.getKind()!=DT_SIZE && f1.getKind()!=DT_HEIGHT_BOUND ) || f1[0].getType()==f2[0].getType() ) &&
             !areEqual( f1, f2 ) ){
           Trace("dt-cg") << "Check " << f1 << " and " << f2 << std::endl;
           bool somePairIsDisequal = false;
@@ -1377,11 +1384,6 @@ void TheoryDatatypes::collectTerms( Node n ) {
       d_selTerms.push_back( n );
       //we must also record which selectors exist
       Trace("dt-collapse-sel") << "  Found selector " << n << endl;
-      //if (n.getType().isBoolean()) {
-      //  d_equalityEngine.addTriggerPredicate( n );
-      //}else{
-      //  d_equalityEngine.addTerm( n );
-      //}
       Node rep = getRepresentative( n[0] );
       //record it in the selectors
       EqcInfo* eqc = getOrMakeEqcInfo( rep, true );
@@ -1395,7 +1397,7 @@ void TheoryDatatypes::collectTerms( Node n ) {
         d_pending.push_back( conc );
         d_pending_exp[ conc ] = d_true;
         d_infer.push_back( conc );
-
+/*
         //add size = 0 lemma
         Node nn = n.eqNode( NodeManager::currentNM()->mkConst( Rational(0) ) );
         std::vector< Node > children;
@@ -1412,7 +1414,10 @@ void TheoryDatatypes::collectTerms( Node n ) {
         d_pending.push_back( conc );
         d_pending_exp[ conc ] = d_true;
         d_infer.push_back( conc );
-      }else if( n.getKind() == DT_HEIGHT_BOUND ){
+*/
+      }
+
+      if( n.getKind() == DT_HEIGHT_BOUND ){
         if( n[1].getConst<Rational>().isZero() ){
           std::vector< Node > children;
           const Datatype& dt = ((DatatypeType)(n[0].getType()).toType()).getDatatype();
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index 560e29c3b..b47c98aa3 100644
--- a/src/theory/quantifiers/options
+++ b/src/theory/quantifiers/options
@@ -207,5 +207,7 @@ option localTheoryExt --local-t-ext bool :default false
   do instantiation based on local theory extensions
 option ltePartialInst --lte-partial-inst bool :default false
   partially instantiate local theory quantifiers
+option lteRestrictInstClosure --lte-restrict-inst-closure bool :default false
+  treat arguments of inst closure as restricted terms for instantiation
  
 endmodule
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 69271e021..fb28974a9 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -322,15 +322,19 @@ bool TermDb::isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep,
   return false;
 }
 
-bool TermDb::hasTermCurrent( Node n ) {
-  //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 ){
+bool TermDb::hasTermCurrent( Node n, bool useMode ) {
+  if( !useMode ){
     return d_has_map.find( n )!=d_has_map.end();
   }else{
-    Assert( false );
-    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{
+      Assert( false );
+      return false;
+    }
   }
 }
 
@@ -364,7 +368,12 @@ Node TermDb::getHasTermEqc( Node r ) {
   }
 }
 
+bool TermDb::isInstClosure( Node r ) {
+  return d_iclosure_processed.find( r )!=d_iclosure_processed.end();
+}
+
 void TermDb::setHasTerm( Node n ) {
+  Trace("term-db-debug2") << "hasTerm : " << n  << std::endl;
   //if( inst::Trigger::isAtomicTrigger( n ) ){
   if( d_has_map.find( n )==d_has_map.end() ){
     d_has_map[n] = true;
@@ -391,9 +400,9 @@ void TermDb::reset( Theory::Effort effort ){
   d_func_map_trie.clear();
   d_func_map_eqc_trie.clear();
 
-  eq::EqualityEngine* ee = d_quantEngine->getMasterEqualityEngine(); 
+  eq::EqualityEngine* ee = d_quantEngine->getMasterEqualityEngine();
   //compute has map
-  if( options::termDbMode()==TERM_DB_RELEVANT ){
+  if( options::termDbMode()==TERM_DB_RELEVANT || options::lteRestrictInstClosure() ){
     d_has_map.clear();
     d_has_eqc.clear();
     eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee );
@@ -423,7 +432,9 @@ void TermDb::reset( Theory::Effort effort ){
       if (theory && d_quantEngine->getTheoryEngine()->d_logicInfo.isTheoryEnabled(theoryId)) {
         context::CDList<Assertion>::const_iterator it = theory->facts_begin(), it_end = theory->facts_end();
         for (unsigned i = 0; it != it_end; ++ it, ++i) {
-          setHasTerm( (*it).assertion );
+          if( (*it).assertion.getKind()!=INST_CLOSURE ){
+            setHasTerm( (*it).assertion );
+          }
         }
       }
     }
@@ -443,7 +454,7 @@ void TermDb::reset( Theory::Effort effort ){
             computeModelBasisArgAttribute( n );
           }
           computeArgReps( n );
-          
+
           if( Trace.isOn("term-db-debug") ){
             Trace("term-db-debug") << "Adding term " << n << " with arg reps : ";
             for( unsigned i=0; i<d_arg_reps[n].size(); i++ ){
@@ -451,7 +462,7 @@ void TermDb::reset( Theory::Effort effort ){
             }
             Trace("term-db-debug") << std::endl;
           }
-          
+
           if( !d_func_map_trie[ it->first ].addTerm( n, d_arg_reps[n] ) ){
             NoMatchAttribute nma;
             n.setAttribute(nma,true);
@@ -1157,7 +1168,7 @@ void TermDb::computeAttributes( Node q ) {
           //not necessarily nested existential
           //Assert( q[1].getKind()==NOT );
           //Assert( q[1][0].getKind()==FORALL );
-          
+
           Trace("quant-attr") << "Attribute : sygus : " << q << std::endl;
           d_qattr_sygus[q] = true;
           if( d_quantEngine->getCegInstantiation()==NULL ){
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index f841bb2d8..8a20d6b41 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -33,7 +33,7 @@ typedef expr::Attribute< AxiomAttributeId, bool > AxiomAttribute;
 /** Attribute true for quantifiers that are conjecture */
 struct ConjectureAttributeId {};
 typedef expr::Attribute< ConjectureAttributeId, bool > ConjectureAttribute;
-  
+
 /** Attribute true for function definition quantifiers */
 struct FunDefAttributeId {};
 typedef expr::Attribute< FunDefAttributeId, bool > FunDefAttribute;
@@ -183,10 +183,11 @@ public:
   /** is entailed (incomplete check) */
   bool isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool pol );
   /** has term */
-  bool hasTermCurrent( Node n );
+  bool hasTermCurrent( Node n, bool useMode = true );
   /** get has term eqc */
   Node getHasTermEqc( Node r );
-  
+  /** is inst closure */
+  bool isInstClosure( Node r );
 //for model basis
 private:
   //map from types to model basis terms
@@ -252,8 +253,8 @@ public:
 public:
   //get bound variables in n
   static void getBoundVars( Node n, std::vector< Node >& bvs);
-  
-  
+
+
 //for skolem
 private:
   /** map from universal quantifiers to their skolemized body */
@@ -268,9 +269,9 @@ public:
   Node getSkolemizedBody( Node f);
   /** is induction variable */
   static bool isInductionTerm( Node n );
-  
+
 //for ground term enumeration
-private:  
+private:
   /** ground terms enumerated for types */
   std::map< TypeNode, std::vector< Node > > d_enum_terms;
   //type enumerators
@@ -278,8 +279,8 @@ private:
   std::vector< TypeEnumerator > d_typ_enum;
 public:
   //get nth term for type
-  Node getEnumerateTerm( TypeNode tn, unsigned index );  
-  
+  Node getEnumerateTerm( TypeNode tn, unsigned index );
+
 //miscellaneous
 public:
   /** map from universal quantifiers to the list of variables */
@@ -353,7 +354,7 @@ public:
   int getQAttrQuantInstLevel( Node q );
   /** get rewrite rule priority */
   int getQAttrRewriteRulePriority( Node q );
-  
+
 };/* class TermDb */
 
 }/* CVC4::theory::quantifiers namespace */
diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp
index 12edaa31c..951a6b545 100644
--- a/src/theory/quantifiers/theory_quantifiers.cpp
+++ b/src/theory/quantifiers/theory_quantifiers.cpp
@@ -131,6 +131,9 @@ void TheoryQuantifiers::check(Effort e) {
       break;
     case kind::INST_CLOSURE:
       getQuantifiersEngine()->addTermToDatabase( assertion[0], false, true );
+      if( !options::lteRestrictInstClosure() ){
+        getQuantifiersEngine()->getMasterEqualityEngine()->addTerm( assertion[0] );
+      }
       break;
     case kind::EQUAL:
       //do nothing
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 52b4fd17d..13822eb98 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -80,9 +80,9 @@ d_lemmas_produced_c(u){
   //d_rr_tr_trie = new rrinst::TriggerTrie;
   //d_eem = new EfficientEMatcher( this );
   d_hasAddedLemma = false;
-  
+
   bool needsBuilder = false;
-  
+
   Trace("quant-engine-debug") << "Initialize model, mbqi : " << options::mbqiMode() << std::endl;
 
   //the model object
@@ -158,7 +158,7 @@ d_lemmas_produced_c(u){
   }else{
     d_lte_part_inst = NULL;
   }
-  
+
   if( needsBuilder ){
     Trace("quant-engine-debug") << "Initialize model engine, mbqi : " << options::mbqiMode() << " " << options::fmfBoundInt() << std::endl;
     if( options::mbqiMode()==quantifiers::MBQI_FMC || options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL ||
@@ -604,21 +604,35 @@ void QuantifiersEngine::setInstantiationLevelAttr( Node n, uint64_t level ){
 }
 
 bool QuantifiersEngine::isTermEligibleForInstantiation( Node n, Node f, bool print ) {
-  if( n.hasAttribute(InstLevelAttribute()) ){
-    int fml = d_term_db->getQAttrQuantInstLevel( f );
-    unsigned ml = fml>=0 ? fml : options::instMaxLevel();
-
-    if( n.getAttribute(InstLevelAttribute())>ml ){
-      Trace("inst-add-debug") << "Term " << n << " has instantiation level " << n.getAttribute(InstLevelAttribute());
-      Trace("inst-add-debug") << ", which is more than maximum allowed level " << ml << " for this quantified formula." << std::endl;
+  if( options::lteRestrictInstClosure() ){
+    //has to be both in inst closure and in ground assertions
+    if( !d_term_db->isInstClosure( n ) ){
+      Trace("inst-add-debug") << "Term " << n << " is not an inst-closure term." << std::endl;
       return false;
     }
-  }else{
-    if( options::instLevelInputOnly() ){
-      Trace("inst-add-debug") << "Term " << n << " does not have an instantiation level." << std::endl;
+    // hack : since theories preregister terms not in assertions, we are using hasTermCurrent to approximate this
+    if( !d_term_db->hasTermCurrent( n, false ) ){
+      Trace("inst-add-debug") << "Term " << n << " is not in a ground assertion." << std::endl;
       return false;
     }
   }
+  if( options::instMaxLevel()!=-1 ){
+    if( n.hasAttribute(InstLevelAttribute()) ){
+      int fml = d_term_db->getQAttrQuantInstLevel( f );
+      unsigned ml = fml>=0 ? fml : options::instMaxLevel();
+
+      if( n.getAttribute(InstLevelAttribute())>ml ){
+        Trace("inst-add-debug") << "Term " << n << " has instantiation level " << n.getAttribute(InstLevelAttribute());
+        Trace("inst-add-debug") << ", which is more than maximum allowed level " << ml << " for this quantified formula." << std::endl;
+        return false;
+      }
+    }else{
+      if( options::instLevelInputOnly() ){
+        Trace("inst-add-debug") << "Term " << n << " does not have an instantiation level." << std::endl;
+        return false;
+      }
+    }
+  }
   return true;
 }
 
@@ -775,7 +789,7 @@ bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& terms, bo
   Trace("inst-add-debug") << std::endl;
 
   //check based on instantiation level
-  if( options::instMaxLevel()!=-1 ){
+  if( options::instMaxLevel()!=-1 || options::lteRestrictInstClosure() ){
     for( unsigned i=0; i<terms.size(); i++ ){
       if( !isTermEligibleForInstantiation( terms[i], f, true ) ){
         return false;
@@ -1247,7 +1261,9 @@ int getDepth( Node n ){
 //smaller the score, the better
 int EqualityQueryQuantifiersEngine::getRepScore( Node n, Node f, int index ){
   int s;
-  if( options::instMaxLevel()!=-1 ){
+  if( options::lteRestrictInstClosure() && ( !d_qe->getTermDatabase()->isInstClosure( n ) || !d_qe->getTermDatabase()->hasTermCurrent( n, false ) ) ){
+    return -1;
+  }else if( options::instMaxLevel()!=-1 ){
     //score prefer lowest instantiation level
     if( n.hasAttribute(InstLevelAttribute()) ){
       s = n.getAttribute(InstLevelAttribute());