Merge remote-tracking branch 'origin/master'

7 files changed, 128 insertions, 163 deletions

diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 87d1f6517..65514180d 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -62,6 +62,7 @@ TheoryDatatypes::TheoryDatatypes(Context* c, UserContext* u, OutputChannel& out,
   d_equalityEngine.addFunctionKind(kind::APPLY_UF);
 
   d_true = NodeManager::currentNM()->mkConst( true );
+  d_dtfCounter = 0;
 }
 
 TheoryDatatypes::~TheoryDatatypes() {
@@ -194,8 +195,8 @@ void TheoryDatatypes::check(Effort e) {
                 }
               }
             }
-
-            if( !needSplit && options::dtForceAssignment() ){
+            //d_dtfCounter++;
+            if( !needSplit && options::dtForceAssignment() && d_dtfCounter%2==0 ){
               //for the sake of termination, we must choose the constructor of a ground term
               //NEED GUARENTEE: groundTerm should not contain any subterms of the same type
               // TODO: this is probably not good enough, actually need fair enumeration strategy
diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h
index 132077e29..3592dbe30 100644
--- a/src/theory/datatypes/theory_datatypes.h
+++ b/src/theory/datatypes/theory_datatypes.h
@@ -174,6 +174,8 @@ private:
   context::CDList<TNode> d_consTerms;
   /** All the selector terms that the theory has seen */
   context::CDList<TNode> d_selTerms;
+  /** counter for forcing assignments (ensures fairness) */
+  unsigned d_dtfCounter;
 private:
   /** assert fact */
   void assertFact( Node fact, Node exp );
diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp
index a7c67a5e4..c775bb558 100644
--- a/src/theory/quantifiers/conjecture_generator.cpp
+++ b/src/theory/quantifiers/conjecture_generator.cpp
@@ -81,7 +81,7 @@ d_ee_conjectures( c ){
   d_fullEffortCount = 0;

   d_uequalityEngine.addFunctionKind( kind::APPLY_UF );

   d_uequalityEngine.addFunctionKind( kind::APPLY_CONSTRUCTOR );

-  

+

 }

 

 void ConjectureGenerator::eqNotifyNewClass( TNode t ){

@@ -214,7 +214,7 @@ bool ConjectureGenerator::isUniversalLessThan( TNode rt1, TNode rt2 ) {
   Assert( d_pattern_is_normal.find( rt2 )!=d_pattern_is_normal.end() );

   Assert( d_pattern_fun_sum.find( rt1 )!=d_pattern_fun_sum.end() );

   Assert( d_pattern_fun_sum.find( rt2 )!=d_pattern_fun_sum.end() );

-  

+

   if( d_pattern_is_normal[rt1] && !d_pattern_is_normal[rt2] ){

     Trace("thm-ee-debug") << "UEE : LT due to normal." << std::endl;

     return true;

@@ -232,8 +232,8 @@ bool ConjectureGenerator::isUniversalLessThan( TNode rt1, TNode rt2 ) {
 }

 

 

-bool ConjectureGenerator::isReportedCanon( TNode n ) { 

-  return std::find( d_ue_canon.begin(), d_ue_canon.end(), n )==d_ue_canon.end(); 

+bool ConjectureGenerator::isReportedCanon( TNode n ) {

+  return std::find( d_ue_canon.begin(), d_ue_canon.end(), n )==d_ue_canon.end();

 }

 

 void ConjectureGenerator::markReportedCanon( TNode n ) {

@@ -545,7 +545,7 @@ void ConjectureGenerator::check( Theory::Effort e, unsigned quant_e ) {
         if( it->first.isNull() ){

           Trace("sg-gen-tg-debug") << "In this order : ";

           for( unsigned i=0; i<it->second.size(); i++ ){

-            Trace("sg-gen-tg-debug") << it->second[i] << " ";            

+            Trace("sg-gen-tg-debug") << it->second[i] << " ";

           }

           Trace("sg-gen-tg-debug") << std::endl;

         }

@@ -663,10 +663,10 @@ void ConjectureGenerator::check( Theory::Effort e, unsigned quant_e ) {
       d_rel_pattern_var_sum.clear();

       d_rel_pattern_typ_index.clear();

       d_rel_pattern_subs_index.clear();

-      d_gen_lat_maximal.clear();

-      d_gen_lat_child.clear();

-      d_gen_lat_parent.clear();

-      d_gen_depth.clear();

+      //d_gen_lat_maximal.clear();

+      //d_gen_lat_child.clear();

+      //d_gen_lat_parent.clear();

+      //d_gen_depth.clear();

 

       //the following generates a set of relevant terms

       d_use_ccand_eqc = true;

@@ -682,6 +682,8 @@ void ConjectureGenerator::check( Theory::Effort e, unsigned quant_e ) {
       }

       std::map< TypeNode, unsigned > rt_var_max;

       std::vector< TypeNode > rt_types;

+      std::map< int, std::vector< Node > > conj_lhs;

+      std::map< int, std::vector< Node > > conj_rhs;

       //map from generalization depth to maximum depth

       //std::map< unsigned, unsigned > gdepth_to_tdepth;

       for( unsigned depth=1; depth<3; depth++ ){

@@ -693,7 +695,7 @@ void ConjectureGenerator::check( Theory::Effort e, unsigned quant_e ) {
         d_var_limit.clear();

         d_tg_id = 0;

         d_tg_gdepth = 0;

-        d_tg_gdepth_limit = -1;

+        d_tg_gdepth_limit = depth;

         //consider all types

         d_tg_alloc[0].reset( this, TypeNode::null() );

         while( d_tg_alloc[0].getNextTerm( this, depth ) ){

@@ -708,16 +710,16 @@ void ConjectureGenerator::check( Theory::Effort e, unsigned quant_e ) {
               Trace("sg-rel-term") << std::endl;

 

               for( unsigned r=0; r<2; r++ ){

-                Trace("sg-gen-tg-eqc") << "...from equivalence classes (" << r << ") : ";

+                Trace("sg-rel-term-debug") << "...from equivalence classes (" << r << ") : ";

                 int index = d_ccand_eqc[r].size()-1;

                 for( unsigned j=0; j<d_ccand_eqc[r][index].size(); j++ ){

-                  Trace("sg-gen-tg-eqc") << "e" << d_em[d_ccand_eqc[r][index][j]] << " ";

+                  Trace("sg-rel-term-debug") << "e" << d_em[d_ccand_eqc[r][index][j]] << " ";

                 }

-                Trace("sg-gen-tg-eqc") << std::endl;

+                Trace("sg-rel-term-debug") << std::endl;

               }

               TypeNode tnn = nn.getType();

               Trace("sg-gen-tg-debug") << "...term is " << nn << std::endl;

-              Assert( getUniversalRepresentative( nn )==nn );

+              conj_lhs[depth].push_back( nn );

 

               //add information about pattern

               Trace("sg-gen-tg-debug") << "Collect pattern information..." << std::endl;

@@ -742,38 +744,6 @@ void ConjectureGenerator::check( Theory::Effort e, unsigned quant_e ) {
               Assert( d_pattern_is_normal[nn] );

               Trace("sg-gen-tg-debug") << "...done collect pattern information" << std::endl;

 

-              //compute generalization relation

-              Trace("sg-gen-tg-debug") << "Build generalization information..." << std::endl;

-              std::map< TNode, bool > patProc;

-              int maxGenDepth = -1;

-              unsigned i = d_rel_patterns[tnn].size()-1;

-              for( int j=(int)(i-1); j>=0; j-- ){

-                TNode np = d_rel_patterns[tnn][j];

-                if( patProc.find( np )==patProc.end() ){

-                  Trace("sg-gen-tg-debug2") << "Check if generalized by " << np << "..." << std::endl;

-                  if( isGeneralization( np, nn ) ){

-                    Trace("sg-rel-terms-debug") << "  is generalized by : " << np << std::endl;

-                    d_gen_lat_child[np].push_back( nn );

-                    d_gen_lat_parent[nn].push_back( np );

-                    if( d_gen_depth[np]>maxGenDepth ){

-                      maxGenDepth = d_gen_depth[np];

-                    }

-                    //don't consider the transitive closure of generalizes

-                    Trace("sg-gen-tg-debug2") << "Add generalizations" << std::endl;

-                    addGeneralizationsOf( np, patProc );

-                    Trace("sg-gen-tg-debug2") << "Done add generalizations" << std::endl;

-                  }else{

-                    Trace("sg-gen-tg-debug2") << "  is not generalized by : " << np << std::endl;

-                  }

-                }

-              }

-              if( d_gen_lat_parent[nn].empty() ){

-                d_gen_lat_maximal[tnn].push_back( nn );

-              }

-              d_gen_depth[nn] = maxGenDepth+1;

-              Trace("sg-rel-term-debug") << "  -> generalization depth is " << d_gen_depth[nn] << " <> " << depth << std::endl;

-              Trace("sg-gen-tg-debug") << "...done build generalization information" << std::endl;

-

               //record information about types

               Trace("sg-gen-tg-debug") << "Collect type information..." << std::endl;

               PatternTypIndex * pti = &d_rel_pattern_typ_index;

@@ -796,7 +766,7 @@ void ConjectureGenerator::check( Theory::Effort e, unsigned quant_e ) {
               int index = d_ccand_eqc[1].size()-1;

               for( unsigned j=0; j<d_ccand_eqc[1][index].size(); j++ ){

                 TNode r = d_ccand_eqc[1][index][j];

-                Trace("sg-gen-tg-eqc") << "  Matches for e" << d_em[r] << ", which is ground term " << d_ground_eqc_map[r] << ":" << std::endl;

+                Trace("sg-rel-term-debug") << "  Matches for e" << d_em[r] << ", which is ground term " << d_ground_eqc_map[r] << ":" << std::endl;

                 std::map< TypeNode, std::map< unsigned, TNode > > subs;

                 std::map< TNode, bool > rev_subs;

                 //only get ground terms

@@ -809,17 +779,17 @@ void ConjectureGenerator::check( Theory::Effort e, unsigned quant_e ) {
                     unsigned tindex = typ_to_subs_index[it->first];

                     for( std::map< unsigned, TNode >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){

                       if( !firstTime ){

-                        Trace("sg-gen-tg-eqc") << ", ";

+                        Trace("sg-rel-term-debug") << ", ";

                       }else{

                         firstTime = false;

-                        Trace("sg-gen-tg-eqc") << "    ";

+                        Trace("sg-rel-term-debug") << "    ";

                       }

-                      Trace("sg-gen-tg-eqc") << it->first << ":x" << it2->first << " -> " << it2->second;

+                      Trace("sg-rel-term-debug") << it->first << ":x" << it2->first << " -> " << it2->second;

                       Assert( tindex+it2->first<gsubs_terms.size() );

                       gsubs_terms[tindex+it2->first] = it2->second;

                     }

                   }

-                  Trace("sg-gen-tg-eqc") << std::endl;

+                  Trace("sg-rel-term-debug") << std::endl;

                   d_rel_pattern_subs_index[nn].addSubstitution( r, gsubs_vars, gsubs_terms );

                 }

               }

@@ -834,8 +804,7 @@ void ConjectureGenerator::check( Theory::Effort e, unsigned quant_e ) {
           }

         }

         Trace("sg-proc") << "...done generate terms at depth " << depth << std::endl;

-    

-        

+

         //now generate right hand sides

 

 

@@ -852,11 +821,11 @@ void ConjectureGenerator::check( Theory::Effort e, unsigned quant_e ) {
         d_var_limit[ it->first ] = it->second;

       }

       //set up environment for candidate conjectures

-      d_cconj_at_depth.clear();

-      for( unsigned i=0; i<2; i++ ){

-        d_cconj[i].clear();

-      }

-      d_cconj_rhs_paired.clear();

+      //d_cconj_at_depth.clear();

+      //for( unsigned i=0; i<2; i++ ){

+      //  d_cconj[i].clear();

+      //}

+      //d_cconj_rhs_paired.clear();

       unsigned totalCount = 0;

       for( unsigned depth=0; depth<5; depth++ ){

         //consider types from relevant terms

@@ -865,19 +834,17 @@ void ConjectureGenerator::check( Theory::Effort e, unsigned quant_e ) {
           Assert( d_tg_alloc.empty() );

           Trace("sg-proc") << "Generate relevant RHS terms of type " << rt_types[i] << " at depth " << depth << "..." << std::endl;

           d_tg_id = 0;

+          d_tg_gdepth = 0;

+          d_tg_gdepth_limit = -1;

           d_tg_alloc[0].reset( this, rt_types[i] );

           while( d_tg_alloc[0].getNextTerm( this, depth ) && totalCount<100 ){

             if( d_tg_alloc[0].getDepth( this )==depth ){

               Node rhs = d_tg_alloc[0].getTerm( this );

               Trace("sg-rel-prop") << "Relevant RHS : " << rhs << std::endl;

+              conj_rhs[depth].push_back( rhs );

               //register pattern

               Assert( rhs.getType()==rt_types[i] );

               registerPattern( rhs, rt_types[i] );

-              //for each maximal node of type rt_types[i] in generalization lattice

-              for( unsigned j=0; j<d_gen_lat_maximal[rt_types[i]].size(); j++ ){

-                //add candidate conjecture

-                addCandidateConjecture( d_gen_lat_maximal[rt_types[i]][j], rhs, 0 );

-              }

               totalCount++;

             }

           }

@@ -885,14 +852,13 @@ void ConjectureGenerator::check( Theory::Effort e, unsigned quant_e ) {
           d_tg_alloc.clear();

         }

         Trace("sg-proc") << "Process candidate conjectures up to RHS term depth " << depth << "..." << std::endl;

-        for( unsigned conj_depth=0; conj_depth<depth; conj_depth++ ){

-          //process all conjectures waiting at depth

-          unsigned sz = d_cconj_at_depth[conj_depth].size();

-          for( int i=(int)(sz-1); i>=0; i-- ){

-            processCandidateConjecture( d_cconj_at_depth[conj_depth][i], conj_depth );

+        for( int rhs_d=depth; rhs_d>=0; rhs_d-- ){

+          int lhs_d = (depth-rhs_d)+1;

+          for( unsigned i=0; i<conj_rhs[rhs_d].size(); i++ ){

+            for( unsigned j=0; j<conj_lhs[lhs_d].size(); j++ ){

+              processCandidateConjecture( conj_lhs[lhs_d][j], conj_rhs[rhs_d][i], lhs_d, rhs_d );

+            }

           }

-          Assert( d_cconj_at_depth[conj_depth].size()==sz );

-          d_cconj_at_depth[conj_depth].clear();

         }

         Trace("sg-proc") << "...done process candidate conjectures at RHS term depth " << depth << std::endl;

       }

@@ -985,23 +951,23 @@ TNode ConjectureGenerator::getTgFunc( TypeNode tn, unsigned i ) {
 

 bool ConjectureGenerator::considerCurrentTerm() {

   Assert( !d_tg_alloc.empty() );

-  

+

   //if generalization depth is too large, don't consider it

   unsigned i = d_tg_alloc.size();

   Trace("sg-gen-tg-debug") << "Consider term ";

   d_tg_alloc[0].debugPrint( this, "sg-gen-tg-debug", "sg-gen-tg-debug" );

   Trace("sg-gen-tg-debug") << "?  curr term size = " << d_tg_alloc.size() << ", last status = " << d_tg_alloc[i-1].d_status;

   Trace("sg-gen-tg-debug") << std::endl;

-  

+

   Assert( d_tg_alloc[0].getGeneralizationDepth( this )==d_tg_gdepth );

-  

+

   if( d_tg_gdepth_limit>=0 && d_tg_gdepth>(unsigned)d_tg_gdepth_limit ){

     Trace("sg-gen-consider-term") << "-> generalization depth of ";

     d_tg_alloc[0].debugPrint( this, "sg-gen-consider-term", "sg-gen-tg-debug" );

     Trace("sg-gen-consider-term") << " is too high " << d_tg_gdepth << " " << d_tg_alloc[0].getGeneralizationDepth( this ) << ", do not consider." << std::endl;

     return false;

   }

-  

+

   //----optimizations

   if( d_tg_alloc[i-1].d_status==1 ){

   }else if( d_tg_alloc[i-1].d_status==2 ){

@@ -1034,9 +1000,10 @@ bool ConjectureGenerator::considerCurrentTerm() {
         std::map< TNode, bool > rev_subs;

         unsigned mode;

         if( r==0 ){

-          mode = optReqDistinctVarPatterns() ? 1 : 0;

+          mode = optReqDistinctVarPatterns() ? ( 1 << 0 ) : 0;

+          mode = mode | (1 << 2 );

         }else{

-          mode = (optFilterConfirmation() && optFilterConfirmationOnlyGround() ) ? 2 : 0;

+          mode = (optFilterConfirmation() && optFilterConfirmationOnlyGround() ) ? ( 1 << 1 ) : 0;

         }

         d_tg_alloc[0].resetMatching( this, d_ccand_eqc[r][i-1][j], mode );

         if( d_tg_alloc[0].getNextMatch( this, d_ccand_eqc[r][i-1][j], subs, rev_subs ) ){

@@ -1202,40 +1169,13 @@ bool ConjectureGenerator::isGeneralization( TNode patg, TNode pat, std::map< TNo
   }

 }

 

-void ConjectureGenerator::addGeneralizationsOf( TNode pat, std::map< TNode, bool >& patProc ) {

-  patProc[pat] = true;

-  for( unsigned k=0; k<d_gen_lat_parent[pat].size(); k++ ){

-    addGeneralizationsOf( d_gen_lat_parent[pat][k], patProc );

-  }

-}

-

-void ConjectureGenerator::addCandidateConjecture( TNode lhs, TNode rhs, unsigned depth ) {

-  if( std::find( d_cconj_rhs_paired[rhs].begin(), d_cconj_rhs_paired[rhs].end(), lhs )==d_cconj_rhs_paired[rhs].end() ){

-    //add conjecture to list to process

-    d_cconj_at_depth[depth].push_back( d_cconj[0].size() );

-    //define conjecture

-    d_cconj[0].push_back( lhs );

-    d_cconj[1].push_back( rhs );

-    d_cconj_rhs_paired[rhs].push_back( lhs );

-  }

-}

-

-void ConjectureGenerator::processCandidateConjecture( unsigned cid, unsigned depth ) {

+void ConjectureGenerator::processCandidateConjecture( TNode lhs, TNode rhs, unsigned lhs_depth, unsigned rhs_depth ) {

   if( d_waiting_conjectures.size()>=optFullCheckConjectures() ){

     return;

   }

-  TNode lhs = d_cconj[0][cid];

-  TNode rhs = d_cconj[1][cid];

-  if( !considerCandidateConjecture( lhs, rhs ) ){

-    //push to children of generalization lattice

-    for( unsigned i=0; i<d_gen_lat_child[lhs].size(); i++ ){

-      if( d_gen_depth[lhs]+1==d_gen_depth[d_gen_lat_child[lhs][i]] ){

-        addCandidateConjecture( d_gen_lat_child[lhs][i], rhs, depth+1 );

-      }

-    }

-  }else{

+  if( considerCandidateConjecture( lhs, rhs ) ){

     Trace("sg-conjecture") << "* Candidate conjecture : " << lhs << " == " << rhs << std::endl;

-    Trace("sg-conjecture-debug") << "     LHS generalization depth : " << d_gen_depth[lhs] << std::endl;

+    Trace("sg-conjecture-debug") << "     LHS, RHS generalization depth : " << lhs_depth << ", " << rhs_depth << std::endl;

     if( optFilterConfirmation() || optFilterFalsification() ){

       Trace("sg-conjecture-debug") << "     confirmed = " << d_subs_confirmCount << ", #witnesses range = " << d_subs_confirmWitnessRange.size() << "." << std::endl;

       Trace("sg-conjecture-debug") << "     #witnesses for ";

@@ -1251,6 +1191,7 @@ void ConjectureGenerator::processCandidateConjecture( unsigned cid, unsigned dep
         firstTime = false;

       }

       Trace("sg-conjecture-debug") << std::endl;

+      Trace("sg-conjecture-debug") << "     unknown = " << d_subs_unkCount << std::endl;

     }

     Assert( getUniversalRepresentative( rhs )==rhs );

     Assert( getUniversalRepresentative( lhs )==lhs );

@@ -1313,6 +1254,7 @@ bool ConjectureGenerator::considerCandidateConjecture( TNode lhs, TNode rhs ) {
       d_subs_confirmCount = 0;

       d_subs_confirmWitnessRange.clear();

       d_subs_confirmWitnessDomain.clear();

+      d_subs_unkCount = 0;

       if( !d_rel_pattern_subs_index[lhs].notifySubstitutions( this, subs, rhs, d_rel_pattern_var_sum[lhs] ) ){

         Trace("sg-cconj") << "  -> found witness that falsifies the conjecture." << std::endl;

         return false;

@@ -1349,7 +1291,7 @@ bool ConjectureGenerator::considerCandidateConjecture( TNode lhs, TNode rhs ) {
           TNode srhsr = getUniversalRepresentative( srhs, true );

           if( areUniversalEqual( slhsr, srhsr ) ){

             Trace("sg-cconj") << "  -> all ground witnesses can be proven by other theorems." << std::endl;

-            return false; 

+            return false;

           }else{

             Trace("sg-cconj-debug") << "Checked if " << slhsr << " and " << srhsr << " were equal." << std::endl;

           }

@@ -1364,7 +1306,7 @@ bool ConjectureGenerator::considerCandidateConjecture( TNode lhs, TNode rhs ) {
         Trace("sg-cconj") << "     #witnesses for " << it->first << " : " << it->second.size() << std::endl;

       }

     }

-    

+

     /*

     if( getUniversalRepresentative( lhs )!=lhs ){

       std::cout << "bad universal representative LHS : " << lhs << " " << getUniversalRepresentative( lhs ) << std::endl;

@@ -1375,12 +1317,12 @@ bool ConjectureGenerator::considerCandidateConjecture( TNode lhs, TNode rhs ) {
       exit(0);

     }

     */

-    

+

     //check if still canonical representation (should be, but for efficiency this is not guarenteed)

     if( getUniversalRepresentative( lhs )!=lhs || getUniversalRepresentative( rhs )!=rhs ){

       Trace("sg-cconj") << "  -> after processing, not canonical." << std::endl;

     }

-    

+

     return true;

   }

 }

@@ -1414,6 +1356,11 @@ bool ConjectureGenerator::notifySubstitution( TNode glhs, std::map< TNode, TNode
                 Trace("sg-cconj-witness") << "    " << it->first << " -> " << it->second << std::endl;

               }

               return false;

+            }else{

+              d_subs_unkCount++;

+              if( optFilterUnknown() ){

+                return false;

+              }

             }

           }

         }

@@ -1592,9 +1539,16 @@ void TermGenerator::resetMatching( ConjectureGenerator * s, TNode eqc, unsigned
   d_match_children.clear();

   d_match_children_end.clear();

   d_match_mode = mode;

+  //if this term generalizes, it must generalize a non-ground term

+  //if( (d_match_mode & ( 1 << 2 ))!=0 && s->isGroundEqc( eqc ) && d_status==5 ){

+  //  d_match_status = -1;

+  //}

 }

 

 bool TermGenerator::getNextMatch( ConjectureGenerator * s, TNode eqc, std::map< TypeNode, std::map< unsigned, TNode > >& subs, std::map< TNode, bool >& rev_subs ) {

+  if( d_match_status<0 ){

+    return false;

+  }

   if( Trace.isOn("sg-gen-tg-match") ){

     Trace("sg-gen-tg-match") << "Matching ";

     debugPrint( s, "sg-gen-tg-match", "sg-gen-tg-match" );

@@ -1619,13 +1573,19 @@ bool TermGenerator::getNextMatch( ConjectureGenerator * s, TNode eqc, std::map<
     //a variable

     if( d_match_status==0 ){

       d_match_status++;

-      if( d_match_mode>=2 ){

+      if( (d_match_mode & ( 1 << 1 ))!=0 ){

         //only ground terms

         if( !s->isGroundEqc( eqc ) ){

           return false;

         }

+      }else if( (d_match_mode & ( 1 << 2 ))!=0 ){

+        //only non-ground terms

+        //if( s->isGroundEqc( eqc ) ){

+        //  return false;

+        //}

       }

-      if( d_match_mode%2==1 ){

+      //store the match : restricted if match_mode.0 = 1

+      if( (d_match_mode & ( 1 << 0 ))!=0 ){

         std::map< TNode, bool >::iterator it = rev_subs.find( eqc );

         if( it==rev_subs.end() ){

           rev_subs[eqc] = true;

@@ -1639,7 +1599,7 @@ bool TermGenerator::getNextMatch( ConjectureGenerator * s, TNode eqc, std::map<
     }else{

       //clean up

       subs[d_typ].erase( d_status_num );

-      if( d_match_mode%2==1 ){

+      if( (d_match_mode & ( 1 << 0 ))!=0 ){

         rev_subs.erase( eqc );

       }

       return false;

@@ -1940,12 +1900,13 @@ void TheoremIndex::debugPrint( const char * c, unsigned ind ) {
 

 bool ConjectureGenerator::optReqDistinctVarPatterns() { return false; }

 bool ConjectureGenerator::optFilterFalsification() { return true; }

+bool ConjectureGenerator::optFilterUnknown() { return true; }  //may change

 bool ConjectureGenerator::optFilterConfirmation() { return true; }

 bool ConjectureGenerator::optFilterConfirmationDomain() { return true; }

 bool ConjectureGenerator::optFilterConfirmationOnlyGround() { return true; }//false; }

 bool ConjectureGenerator::optFilterConfirmationNonCanonical() { return false; }//true; }

 unsigned ConjectureGenerator::optFullCheckFrequency() { return 1; }

-unsigned ConjectureGenerator::optFullCheckConjectures() { return 1; }

+unsigned ConjectureGenerator::optFullCheckConjectures() { return options::conjectureGenPerRound(); }

 

 }

 

diff --git a/src/theory/quantifiers/conjecture_generator.h b/src/theory/quantifiers/conjecture_generator.h
index afdd9e018..93cda7311 100644
--- a/src/theory/quantifiers/conjecture_generator.h
+++ b/src/theory/quantifiers/conjecture_generator.h
@@ -81,16 +81,14 @@ public:
   int d_status_child_num;

   //children (pointers to TermGenerators)

   std::vector< unsigned > d_children;

-  //possible eqc for this term

-  //std::vector< TNode > d_eqc;

 

   //match status

-  unsigned d_match_status;

+  int d_match_status;

   int d_match_status_child_num;

-  //match mode

-  //1 : different variables must have different matches

-  //2 : variables must map to ground terms

-  //3 : both 1 and 2

+  //match mode bits

+  //0 : different variables must have different matches

+  //1 : variables must map to ground terms

+  //2 : variables must map to non-ground terms

   unsigned d_match_mode;

   //children

   std::vector< std::map< TNode, TermArgTrie >::iterator > d_match_children;

@@ -213,14 +211,14 @@ private:
   void setUniversalRelevant( TNode n );

   /** ordering for universal terms */

   bool isUniversalLessThan( TNode rt1, TNode rt2 );

-  

+

   /** the nodes we have reported as canonical representative */

   std::vector< TNode > d_ue_canon;

   /** is reported canon */

   bool isReportedCanon( TNode n );

   /** mark that term has been reported as canonical rep */

   void markReportedCanon( TNode n );

-  

+

 private:  //information regarding the conjectures

   /** list of all conjectures */

   std::vector< Node > d_conjectures;

@@ -297,7 +295,6 @@ public:  //environment for term enumeration
   std::map< unsigned, TermGenerator > d_tg_alloc;

   unsigned d_tg_gdepth;

   int d_tg_gdepth_limit;

-  //std::vector< std::vector< unsigned > > d_var_eq_tg;

   //access functions

   unsigned getNumTgVars( TypeNode tn );

   bool allowVar( TypeNode tn );

@@ -308,37 +305,16 @@ public:  //environment for term enumeration
   bool considerCurrentTerm();

   bool considerTermCanon( unsigned tg_id );

   void changeContext( bool add );

-public:  //for generalization lattice

-  //id of maximal nodes

-  std::map< TypeNode, std::vector< TNode > > d_gen_lat_maximal;

-  //generalization lattice

-  std::map< TNode, std::vector< TNode > > d_gen_lat_child;

-  std::map< TNode, std::vector< TNode > > d_gen_lat_parent;

-  //generalization depth

-  std::map< TNode, int > d_gen_depth;

+public:  //for generalization

   //generalizations

   bool isGeneralization( TNode patg, TNode pat ) {

     std::map< TNode, TNode > subs;

     return isGeneralization( patg, pat, subs );

   }

   bool isGeneralization( TNode patg, TNode pat, std::map< TNode, TNode >& subs );

-  void addGeneralizationsOf( TNode pat, std::map< TNode, bool >& patProc );

-  

-  //from generalization depth to relevant patterns

-  std::map< TypeNode, std::map< unsigned, std::vector< TNode > > > d_rel_patterns_at_depth;

-  

-  

 public:  //for property enumeration

-  //conjectures to process at a particular depth

-  std::map< unsigned, std::vector< unsigned > > d_cconj_at_depth;

-  //RHS, LHS

-  std::vector< TNode > d_cconj[2];

-  // RHS paired

-  std::map< TNode, std::vector< TNode > > d_cconj_rhs_paired;

-  //add candidate conjecture

-  void addCandidateConjecture( TNode lhs, TNode rhs, unsigned depth );

-  //process candidate conjecture at depth

-  void processCandidateConjecture( unsigned cid, unsigned depth );

+  //process this candidate conjecture

+  void processCandidateConjecture( TNode lhs, TNode rhs, unsigned lhs_depth, unsigned rhs_depth );

   //whether it should be considered

   bool considerCandidateConjecture( TNode lhs, TNode rhs );

   //notified of a substitution

@@ -349,6 +325,8 @@ public:  //for property enumeration
   std::vector< TNode > d_subs_confirmWitnessRange;

   //individual witnesses (for domain)

   std::map< TNode, std::vector< TNode > > d_subs_confirmWitnessDomain;

+  //number of ground substitutions whose equality is unknown

+  unsigned d_subs_unkCount;

 public:  //for ground equivalence classes

   eq::EqualityEngine * getEqualityEngine();

   bool areDisequal( TNode n1, TNode n2 );

@@ -386,6 +364,7 @@ public:
 private:

   bool optReqDistinctVarPatterns();

   bool optFilterFalsification();

+  bool optFilterUnknown();

   bool optFilterConfirmation();

   bool optFilterConfirmationDomain();

   bool optFilterConfirmationOnlyGround();

diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index 2b4ce9aef..d30e5de4a 100644
--- a/src/theory/quantifiers/options
+++ b/src/theory/quantifiers/options
@@ -26,7 +26,7 @@ option prenexQuant /--disable-prenex-quant bool :default true
 #   forall y. P( c, y )
 option varElimQuant /--disable-var-elim-quant bool :default true
  disable simple variable elimination for quantified formulas
-option dtVarExpandQuant --dt-var-exp-quant bool :default false
+option dtVarExpandQuant --dt-var-exp-quant bool :default true
  expand datatype variables bound to one constructor in quantifiers
 
 option simpleIteLiftQuant /--disable-ite-lift-quant bool :default true
@@ -158,5 +158,8 @@ option intWfInduction --int-wf-ind bool :read-write :default false
  apply strengthening for integers based on well-founded induction
 option conjectureGen --conjecture-gen bool :read-write :default false
  generate candidate conjectures for inductive proofs
+ 
+option conjectureGenPerRound --conjecture-gen-per-round=N int :default 1
+ number of conjectures to generate per instantiation round
 
 endmodule
diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index 504c3dcff..ee4464f87 100755
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -2010,9 +2010,9 @@ void QuantConflictFind::check( Theory::Effort level, unsigned quant_e ) {
             //try to make a matches making the body false

             Trace("qcf-check-debug") << "Get next match..." << std::endl;

             while( qi->d_mg->getNextMatch( this, qi ) ){

-              Trace("qcf-check") << "*** Produced match at effort " << e << " : " << std::endl;

-              qi->debugPrintMatch("qcf-check");

-              Trace("qcf-check") << std::endl;

+              Trace("qcf-inst") << "*** Produced match at effort " << e << " : " << std::endl;

+              qi->debugPrintMatch("qcf-inst");

+              Trace("qcf-inst") << std::endl;

               std::vector< int > assigned;

               if( !qi->isMatchSpurious( this ) ){

                 if( qi->completeMatch( this, assigned ) ){

@@ -2042,7 +2042,7 @@ void QuantConflictFind::check( Theory::Effort level, unsigned quant_e ) {
                         ++(d_statistics.d_prop_inst);

                       }

                     }else{

-                      Trace("qcf-check") << "   ... Failed to add instantiation" << std::endl;

+                      Trace("qcf-inst") << "   ... Failed to add instantiation" << std::endl;

                       //Assert( false );

                     }

                   }

@@ -2050,10 +2050,10 @@ void QuantConflictFind::check( Theory::Effort level, unsigned quant_e ) {
                   qi->revertMatch( assigned );

                   d_tempCache.clear();

                 }else{

-                  Trace("qcf-check") << "   ... Spurious instantiation (cannot assign unassigned variables)" << std::endl;

+                  Trace("qcf-inst") << "   ... Spurious instantiation (cannot assign unassigned variables)" << std::endl;

                 }

               }else{

-                Trace("qcf-check") << "   ... Spurious instantiation (match is inconsistent)" << std::endl;

+                Trace("qcf-inst") << "   ... Spurious instantiation (match is inconsistent)" << std::endl;

               }

             }

             if( d_conflict ){

diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index 624856671..754bfacb1 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -368,7 +368,7 @@ Node QuantifiersRewriter::computeVarElimination( Node body, std::vector< Node >&
   for( std::map< Node, bool >::iterator it = qpr.d_phase_reqs.begin(); it != qpr.d_phase_reqs.end(); ++it ){
     //Notice() << "   " << it->first << " -> " << ( it->second ? "true" : "false" ) << std::endl;
     if( it->first.getKind()==EQUAL ){
-      if( it->second ){
+      if( it->second && options::varElimQuant() ){
         for( int i=0; i<2; i++ ){
           int j = i==0 ? 1 : 0;
           std::vector< Node >::iterator ita = std::find( args.begin(), args.end(), it->first[i] );
@@ -388,14 +388,33 @@ Node QuantifiersRewriter::computeVarElimination( Node body, std::vector< Node >&
         }
       }
     }
-    /*
-    else if( options::dtVarExpandQuant() && it->first.getKind()==APPLY_TESTER && it->first[0].getKind()==BOUND_VARIABLE ){
-      if( it->second ){
+    else if( it->first.getKind()==APPLY_TESTER ){
+      if( options::dtVarExpandQuant() && it->second && it->first[0].getKind()==BOUND_VARIABLE ){
         Trace("dt-var-expand") << "Expand datatype variable based on : " << it->first << std::endl;
         std::vector< Node >::iterator ita = std::find( args.begin(), args.end(), it->first[0] );
+        if( ita!=args.end() ){
+          vars.push_back( it->first[0] );
+          Expr testerExpr = it->first.getOperator().toExpr();
+          int index = Datatype::indexOf( testerExpr );
+          const Datatype& dt = Datatype::datatypeOf(testerExpr);
+          const DatatypeConstructor& c = dt[index];
+          std::vector< Node > newChildren;
+          newChildren.push_back( Node::fromExpr( c.getConstructor() ) );
+          std::vector< Node > newVars;
+          for( unsigned j=0; j<c.getNumArgs(); j++ ){
+            TypeNode tn = TypeNode::fromType( c[j].getSelector().getType() );
+            tn = tn[1];
+            Node v = NodeManager::currentNM()->mkBoundVar( tn );
+            newChildren.push_back( v );
+            newVars.push_back( v );
+          }
+          subs.push_back( NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, newChildren ) );
+          Trace("dt-var-expand") << "...apply substitution " << subs[0] << "/" << vars[0] << std::endl;
+          args.erase( ita );
+          args.insert( args.end(), newVars.begin(), newVars.end() );
+        }
       }
     }
-    */
   }
   if( !vars.empty() ){
     Trace("var-elim-quant") << "VE " << vars.size() << "/" << args.size() << std::endl;
@@ -933,7 +952,7 @@ bool QuantifiersRewriter::doOperation( Node f, bool isNested, int computeOption
   }else if( computeOption==COMPUTE_PRENEX ){
     return options::prenexQuant() && !options::aggressiveMiniscopeQuant();
   }else if( computeOption==COMPUTE_VAR_ELIMINATION ){
-    return options::varElimQuant();
+    return options::varElimQuant() || options::dtVarExpandQuant();
   }else if( computeOption==COMPUTE_CNF ){
     return false;//return options::cnfQuant() ; FIXME
   }else if( computeOption==COMPUTE_SPLIT ){