From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 2 Nov 2012 20:54:11 +0000 (+0000)
Subject: more minor updates to inst gen and representative selection, clean up of equality... 
X-Git-Tag: cvc5-1.0.0~7652
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=1c779966545190efa59b019572237562eea66dbf;p=cvc5.git

more minor updates to inst gen and representative selection, clean up of equality query
---

diff --git a/src/theory/quantifiers/inst_gen.cpp b/src/theory/quantifiers/inst_gen.cpp
index 428a224ee..932a00185 100755
--- a/src/theory/quantifiers/inst_gen.cpp
+++ b/src/theory/quantifiers/inst_gen.cpp
@@ -19,7 +19,7 @@
 #include "theory/quantifiers/model_builder.h"
 #include "theory/quantifiers/first_order_model.h"
 
-#define RECONSIDER_FUNC_CONSTANT
+//#define CHILD_USE_CONSIDER
 
 using namespace std;
 using namespace CVC4;
@@ -55,6 +55,7 @@ void InstGenProcess::addMatchValue( QuantifiersEngine* qe, Node f, Node val, Ins
 }
 
 void InstGenProcess::calculateMatches( QuantifiersEngine* qe, Node f, std::vector< Node >& considerVal, bool useConsider ){
+  Trace("inst-gen-cm") << "* Calculate matches " << d_node << std::endl;
   //whether we are doing a product or sum or matches
   bool doProduct = true;
   //get the model
@@ -64,32 +65,25 @@ void InstGenProcess::calculateMatches( QuantifiersEngine* qe, Node f, std::vecto
   std::vector< Node > considerTerms;
   std::vector< std::vector< Node > > newConsiderVal;
   std::vector< bool > newUseConsider;
+  std::map< Node, InstMatch > considerTermsMatch[2];
+  std::map< Node, bool > considerTermsSuccess[2];
   newConsiderVal.resize( d_children.size() );
-  newUseConsider.resize( d_children.size(), false );
+  newUseConsider.resize( d_children.size(), useConsider );
   if( d_node.getKind()==APPLY_UF ){
     Node op = d_node.getOperator();
     if( useConsider ){
+#ifndef CHILD_USE_CONSIDER
+      for( size_t i=0; i<newUseConsider.size(); i++ ){
+        newUseConsider[i] = false;
+      }
+#endif
       for( size_t i=0; i<considerVal.size(); i++ ){
         eq::EqClassIterator eqc( qe->getEqualityQuery()->getEngine()->getRepresentative( considerVal[i] ),
                                  qe->getEqualityQuery()->getEngine() );
         while( !eqc.isFinished() ){
           Node en = (*eqc);
           if( en.getKind()==APPLY_UF && en.getOperator()==op ){
-            bool isSelected = qe->getModelEngine()->getModelBuilder()->isTermSelected( en );
-            bool isActive = !en.getAttribute(NoMatchAttribute());
-            //check if we need to consider it
-            if( isSelected || isActive ){
               considerTerms.push_back( en );
-#if 0
-              for( int i=0; i<(int)d_children.size(); i++ ){
-                int childIndex = d_children_index[i];
-                Node n = qe->getModel()->getRepresentative( n );
-                if( std::find( newConsiderVal[i].begin(), newConsiderVal[i].end(), n )==newConsiderVal[i].end() ){
-                  newConsiderVal[i].push_back( n );
-                }
-              }
-#endif
-            }
           }
           ++eqc;
         }
@@ -97,23 +91,92 @@ void InstGenProcess::calculateMatches( QuantifiersEngine* qe, Node f, std::vecto
     }else{
       considerTerms.insert( considerTerms.begin(), fm->d_uf_terms[op].begin(), fm->d_uf_terms[op].end() );
     }
-  }else if( d_node.getType().isBoolean() ){
-    if( useConsider ){
-      Assert( considerVal.size()==1 );
-      bool reqPol = considerVal[0]==fm->d_true;
-      if( d_node.getKind()==NOT ){
-        if( !newConsiderVal.empty() ){
-          newConsiderVal[0].push_back( reqPol ? fm->d_false : fm->d_true );
-          newUseConsider[0] = true;
+    //for each term we consider, calculate a current match
+    for( size_t i=0; i<considerTerms.size(); i++ ){
+      Node n = considerTerms[i];
+      bool isSelected = qe->getModelEngine()->getModelBuilder()->isTermSelected( n );
+      bool hadSuccess = false;
+      for( int t=(isSelected ? 0 : 1); t<2; t++ ){
+        if( t==0 || !n.getAttribute(NoMatchAttribute()) ){
+          considerTermsMatch[t][n] = InstMatch();
+          considerTermsSuccess[t][n] = true;
+          for( size_t j=0; j<d_node.getNumChildren(); j++ ){
+            if( d_children_map.find( j )==d_children_map.end() ){
+              if( t!=0 || !n[j].getAttribute(ModelBasisAttribute()) ){
+                if( d_node[j].getKind()==INST_CONSTANT ){
+                  if( !considerTermsMatch[t][n].setMatch( qe->getEqualityQuery(), d_node[j], n[j] ) ){
+                    Trace("inst-gen-cm") << "fail match: " << n[j] << " is not equal to ";
+                    Trace("inst-gen-cm") << considerTermsMatch[t][n].getValue( d_node[j] ) << std::endl;
+                    considerTermsSuccess[t][n] = false;
+                    break;
+                  }
+                }else if( !qe->getEqualityQuery()->areEqual( d_node[j], n[j] ) ){
+                  Trace("inst-gen-cm") << "fail arg: " << n[j] << " is not equal to " << d_node[j] << std::endl;
+                  considerTermsSuccess[t][n] = false;
+                  break;
+                }
+              }
+            }
+          }
+          //if successful, store it
+          if( considerTermsSuccess[t][n] ){
+#ifdef CHILD_USE_CONSIDER
+            if( !hadSuccess ){
+              hadSuccess = true;
+              for( size_t k=0; k<d_children.size(); k++ ){
+                if( newUseConsider[k] ){
+                  int childIndex = d_children_index[k];
+                  //determine if we are restricted or not
+                  if( t!=0 || !n[childIndex].getAttribute(ModelBasisAttribute()) ){
+                    Node r = qe->getModel()->getRepresentative( n[childIndex] );
+                    if( std::find( newConsiderVal[k].begin(), newConsiderVal[k].end(), r )==newConsiderVal[k].end() ){
+                      newConsiderVal[k].push_back( r );
+                      //check if we now need to consider the entire domain
+                      TypeNode tn = r.getType();
+                      if( qe->getModel()->d_rep_set.hasType( tn ) ){
+                        if( (int)newConsiderVal[k].size()>=qe->getModel()->d_rep_set.getNumRepresentatives( tn ) ){
+                          newConsiderVal[k].clear();
+                          newUseConsider[k] = false;
+                        }
+                      }
+                    }
+                  }else{
+                    //matching against selected term, will need to consider all values
+                    newConsiderVal[k].clear();
+                    newUseConsider[k] = false;
+                  }
+                }
+              }
+            }
+#endif
+          }
         }
-      }else if( d_node.getKind()==AND || d_node.getKind()==OR ){
-        for( size_t i=0; i<newConsiderVal.size(); i++ ){
-          newConsiderVal[i].push_back( considerVal[0] );
-          newUseConsider[i] = true;
+      }
+    }
+  }else{
+    //the interpretted case
+    if( d_node.getType().isBoolean() ){
+      if( useConsider ){
+        //if( considerVal.size()!=1 ) { std::cout << "consider val = " << considerVal.size() << std::endl; }
+        Assert( considerVal.size()==1 );
+        bool reqPol = considerVal[0]==fm->d_true;
+        Node ncv = considerVal[0];
+        if( d_node.getKind()==NOT ){
+          ncv = reqPol ? fm->d_false : fm->d_true;
         }
-        //instead we will do a sum
-        if( ( d_node.getKind()==AND && !reqPol ) || ( d_node.getKind()==OR && reqPol )  ){
-          doProduct = false;
+        if( d_node.getKind()==NOT || d_node.getKind()==AND || d_node.getKind()==OR ){
+          for( size_t i=0; i<newConsiderVal.size(); i++ ){
+            newConsiderVal[i].push_back( ncv );
+          }
+          //instead we will do a sum
+          if( ( d_node.getKind()==AND && !reqPol ) || ( d_node.getKind()==OR && reqPol )  ){
+            doProduct = false;
+          }
+        }else{
+          //do not use consider
+          for( size_t i=0; i<newUseConsider.size(); i++ ){
+            newUseConsider[i] = false;
+          }
         }
       }
     }
@@ -126,7 +189,6 @@ void InstGenProcess::calculateMatches( QuantifiersEngine* qe, Node f, std::vecto
       return;
     }
   }
-  Trace("inst-gen-cm") << "* Calculate matches " << d_node << std::endl;
   if( d_node.getKind()==APPLY_UF ){
     //if this is an uninterpreted function
     Node op = d_node.getOperator();
@@ -138,35 +200,13 @@ void InstGenProcess::calculateMatches( QuantifiersEngine* qe, Node f, std::vecto
         //do not consider ground case if it is already congruent to another ground term
         if( t==0 || !n.getAttribute(NoMatchAttribute()) ){
           Trace("inst-gen-cm") << "calculate for " << n << ", selected = " << (t==0) << std::endl;
-          bool success = true;
-          InstMatch curr;
-          for( size_t j=0; j<d_node.getNumChildren(); j++ ){
-            if( d_children_map.find( j )==d_children_map.end() ){
-              if( t!=0 || !n[j].getAttribute(ModelBasisAttribute()) ){
-                if( d_node[j].getKind()==INST_CONSTANT ){
-                  //FIXME: is this correct?
-                  if( !curr.setMatch( qe->getEqualityQuery(), d_node[j], n[j] ) ){
-                    Trace("inst-gen-cm") << "fail match: " << n[j] << " is not equal to " << curr.get( d_node[j] ) << std::endl;
-                    Trace("inst-gen-cm") << "  are equal : " << qe->getEqualityQuery()->areEqual( n[j], curr.get( d_node[j] ) ) << std::endl;
-                    success = false;
-                    break;
-                  }
-                }else if( !qe->getEqualityQuery()->areEqual( d_node[j], n[j] ) ){
-                  Trace("inst-gen-cm") << "fail arg: " << n[j] << " is not equal to " << d_node[j] << std::endl;
-                  success = false;
-                  break;
-                }
-              }
-            }
-          }
-          if( success ){
+          if( considerTermsSuccess[t][n] ){
             //try to find unifier for d_node = n
-            calculateMatchesUninterpreted( qe, f, curr, n, 0, t==0 );
+            calculateMatchesUninterpreted( qe, f, considerTermsMatch[t][n], n, 0, t==0 );
           }
         }
       }
     }
-
   }else{
     //if this is an interpreted function
     if( doProduct ){
diff --git a/src/theory/quantifiers/inst_match.cpp b/src/theory/quantifiers/inst_match.cpp
index 4a89a4dd3..16f06017e 100644
--- a/src/theory/quantifiers/inst_match.cpp
+++ b/src/theory/quantifiers/inst_match.cpp
@@ -54,9 +54,11 @@ bool InstMatch::setMatch( EqualityQuery* q, TNode v, TNode m ){
 
 bool InstMatch::add( InstMatch& m ){
   for( std::map< Node, Node >::iterator it = m.d_map.begin(); it != m.d_map.end(); ++it ){
-    std::map< Node, Node >::iterator itf = d_map.find( it->first );
-    if( itf==d_map.end() || itf->second.isNull() ){
-      d_map[it->first] = it->second;
+    if( !it->second.isNull() ){
+      std::map< Node, Node >::iterator itf = d_map.find( it->first );
+      if( itf==d_map.end() || itf->second.isNull() ){
+        d_map[it->first] = it->second;
+      }
     }
   }
   return true;
@@ -91,7 +93,7 @@ void InstMatch::debugPrint( const char* c ){
   //  Debug( c ) << std::endl;
   //}
 }
-/*
+
 void InstMatch::makeComplete( Node f, QuantifiersEngine* qe ){
   for( size_t i=0; i<f[0].getNumChildren(); i++ ){
     Node ic = qe->getTermDatabase()->getInstantiationConstant( f, i );
@@ -101,27 +103,18 @@ void InstMatch::makeComplete( Node f, QuantifiersEngine* qe ){
   }
 }
 
-void InstMatch::makeInternal( QuantifiersEngine* qe ){
-  if( options::cbqi() ){
-    for( std::map< Node, Node >::iterator it = d_map.begin(); it != d_map.end(); ++it ){
-      if( it->second.hasAttribute(InstConstantAttribute()) ){
-        d_map[ it->first ] = qe->getEqualityQuery()->getInternalRepresentative( it->second );
-        if( it->second.hasAttribute(InstConstantAttribute()) ){
-          d_map[ it->first ] = qe->getTermDatabase()->getFreeVariableForInstConstant( it->first );
-        }
-      }
-    }
+void InstMatch::makeInternalRepresentative( QuantifiersEngine* qe ){
+  EqualityQueryQuantifiersEngine* eqqe = (EqualityQueryQuantifiersEngine*)qe->getEqualityQuery();
+  for( std::map< Node, Node >::iterator it = d_map.begin(); it != d_map.end(); ++it ){
+    d_map[ it->first ] = eqqe->getInternalRepresentative( it->second );
   }
 }
-*/
+
 void InstMatch::makeRepresentative( QuantifiersEngine* qe ){
   for( std::map< Node, Node >::iterator it = d_map.begin(); it != d_map.end(); ++it ){
     if( qe->getEqualityQuery()->getEngine()->hasTerm( it->second ) ){
       d_map[ it->first ] = qe->getEqualityQuery()->getEngine()->getRepresentative( it->second );
     }
-    //if( options::cbqi() && it->second.hasAttribute(InstConstantAttribute()) ){
-    //  d_map[ it->first ] = qe->getTermDatabase()->getFreeVariableForInstConstant( it->first );
-    //}
   }
 }
 
@@ -132,8 +125,8 @@ void InstMatch::applyRewrite(){
 }
 
 /** get value */
-Node InstMatch::getValue( Node var ){
-  std::map< Node, Node >::iterator it = d_map.find( var );
+Node InstMatch::getValue( Node var ) const{
+  std::map< Node, Node >::const_iterator it = d_map.find( var );
   if( it!=d_map.end() ){
     return it->second;
   }else{
@@ -145,7 +138,7 @@ Node InstMatch::getValue( Node var ){
 void InstMatchTrie::addInstMatch2( QuantifiersEngine* qe, Node f, InstMatch& m, int index, ImtIndexOrder* imtio ){
   if( long(index)<long(f[0].getNumChildren()) && ( !imtio || long(index)<long(imtio->d_order.size()) ) ){
     int i_index = imtio ? imtio->d_order[index] : index;
-    Node n = m.get( qe->getTermDatabase()->getInstantiationConstant( f, i_index ) );
+    Node n = m.getValue( qe->getTermDatabase()->getInstantiationConstant( f, i_index ) );
     d_data[n].addInstMatch2( qe, f, m, index+1, imtio );
   }
 }
@@ -156,7 +149,7 @@ bool InstMatchTrie::existsInstMatch2( QuantifiersEngine* qe, Node f, InstMatch&
     return true;
   }else{
     int i_index = imtio ? imtio->d_order[index] : index;
-    Node n = m.get( qe->getTermDatabase()->getInstantiationConstant( f, i_index ) );
+    Node n = m.getValue( qe->getTermDatabase()->getInstantiationConstant( f, i_index ) );
     std::map< Node, InstMatchTrie >::iterator it = d_data.find( n );
     if( it!=d_data.end() ){
       if( it->second.existsInstMatch2( qe, f, m, modEq, modInst, index+1, imtio ) ){
diff --git a/src/theory/quantifiers/inst_match.h b/src/theory/quantifiers/inst_match.h
index 43c0d26c7..41ebb63d2 100644
--- a/src/theory/quantifiers/inst_match.h
+++ b/src/theory/quantifiers/inst_match.h
@@ -55,13 +55,13 @@ public:
   /** is complete? */
   bool isComplete( Node f ) { return d_map.size()==f[0].getNumChildren(); }
   /** make complete */
-  //void makeComplete( Node f, QuantifiersEngine* qe );
-  /** make internal: ensure that no term in d_map contains instantiation constants */
-  //void makeInternal( QuantifiersEngine* qe );
+  void makeComplete( Node f, QuantifiersEngine* qe );
+  /** make internal representative */
+  void makeInternalRepresentative( QuantifiersEngine* qe );
   /** make representative */
   void makeRepresentative( QuantifiersEngine* qe );
   /** get value */
-  Node getValue( Node var );
+  Node getValue( Node var ) const;
   /** clear */
   void clear(){ d_map.clear(); }
   /** is_empty */
diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp
index 8b34a3a12..c7e68acb1 100644
--- a/src/theory/quantifiers/model_builder.cpp
+++ b/src/theory/quantifiers/model_builder.cpp
@@ -59,6 +59,35 @@ d_qe( qe ), d_curr_model( c, NULL ){
   d_considerAxioms = true;
 }
 
+void ModelEngineBuilder::debugModel( FirstOrderModel* fm ){
+  //debug the model: cycle through all instantiations for all quantifiers, report ones that are not true
+  if( Trace.isOn("quant-model-warn") ){
+    for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
+      Node f = fm->getAssertedQuantifier( i );
+      std::vector< Node > vars;
+      for( int j=0; j<(int)f[0].getNumChildren(); j++ ){
+        vars.push_back( f[0][j] );
+      }
+      RepSetIterator riter( &(fm->d_rep_set) );
+      riter.setQuantifier( f );
+      while( !riter.isFinished() ){
+        std::vector< Node > terms;
+        for( int i=0; i<riter.getNumTerms(); i++ ){
+          terms.push_back( riter.getTerm( i ) );
+        }
+        Node n = d_qe->getInstantiation( f, vars, terms );
+        Node val = fm->getValue( n );
+        if( val!=fm->d_true ){
+          Trace("quant-model-warn") << "*******  Instantiation " << n << " for " << std::endl;
+          Trace("quant-model-warn") << "         " << f << std::endl;
+          Trace("quant-model-warn") << "         Evaluates to " << val << std::endl;
+        }
+        riter.increment();
+      }
+    }
+  }
+}
+
 void ModelEngineBuilder::processBuildModel( TheoryModel* m, bool fullModel ) {
   FirstOrderModel* fm = (FirstOrderModel*)m;
   if( fullModel ){
@@ -73,33 +102,8 @@ void ModelEngineBuilder::processBuildModel( TheoryModel* m, bool fullModel ) {
     TheoryEngineModelBuilder::processBuildModel( m, fullModel );
     //mark that the model has been set
     fm->markModelSet();
-    //FOR DEBUGGING
-    if( Trace.isOn("quant-model-warn") ){
-      for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
-        Node f = fm->getAssertedQuantifier( i );
-        std::vector< Node > vars;
-        for( int j=0; j<(int)f[0].getNumChildren(); j++ ){
-          vars.push_back( f[0][j] );
-        }
-        RepSetIterator riter( &(fm->d_rep_set) );
-        riter.setQuantifier( f );
-        while( !riter.isFinished() ){
-          std::vector< Node > terms;
-          for( int i=0; i<riter.getNumTerms(); i++ ){
-            terms.push_back( riter.getTerm( i ) );
-          }
-          Node n = d_qe->getInstantiation( f, vars, terms );
-          Node val = fm->getValue( n );
-          if( val!=fm->d_true ){
-            Trace("quant-model-warn") << "*******  Instantiation " << n << " for " << std::endl;
-            Trace("quant-model-warn") << "         " << f << std::endl;
-            Trace("quant-model-warn") << "         Evaluates to " << val << std::endl;
-          }
-          riter.increment();
-        }
-      }
-    }
-    //END FOR DEBUGGING
+    //debug the model
+    debugModel( fm );
   }else{
     d_curr_model = fm;
     d_addedLemmas = 0;
@@ -113,7 +117,9 @@ void ModelEngineBuilder::processBuildModel( TheoryModel* m, bool fullModel ) {
       for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
         Node f = fm->getAssertedQuantifier( i );
         if( isQuantifierActive( f ) ){
-          d_addedLemmas += initializeQuantifier( f, f );
+          int lems = initializeQuantifier( f, f );
+          d_statistics.d_init_inst_gen_lemmas += lems;
+          d_addedLemmas += lems;
         }
       }
       if( d_addedLemmas>0 ){
@@ -128,14 +134,14 @@ void ModelEngineBuilder::processBuildModel( TheoryModel* m, bool fullModel ) {
         Trace("model-engine-debug") << "Analyzing quantifiers..." << std::endl;
         d_quant_sat.clear();
         d_uf_prefs.clear();
-
         for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
           Node f = fm->getAssertedQuantifier( i );
           if( isQuantifierActive( f ) ){
             analyzeQuantifier( fm, f );
           }
         }
-        //if applicable, find exceptions
+
+        //if applicable, find exceptions to model via inst-gen
         if( optInstGen() ){
           d_didInstGen = true;
           d_instGenMatches = 0;
@@ -148,10 +154,11 @@ void ModelEngineBuilder::processBuildModel( TheoryModel* m, bool fullModel ) {
           for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
             Node f = fm->getAssertedQuantifier( i );
             if( isQuantifierActive( f ) ){
-              int addedLemmas = doInstGen( fm, f );
-              d_addedLemmas += addedLemmas;
+              int lems = doInstGen( fm, f );
+              d_statistics.d_inst_gen_lemmas += lems;
+              d_addedLemmas += lems;
               //temporary
-              if( addedLemmas>0 ){
+              if( lems>0 ){
                 d_numQuantInstGen++;
               }else if( d_quant_sat.find( f )!=d_quant_sat.end() ){
                 d_numQuantSat++;
@@ -160,7 +167,7 @@ void ModelEngineBuilder::processBuildModel( TheoryModel* m, bool fullModel ) {
               }else{
                 d_numQuantNoSelForm++;
               }
-              if( optOneQuantPerRoundInstGen() && addedLemmas>0 ){
+              if( optOneQuantPerRoundInstGen() && lems>0 ){
                 break;
               }
             }else if( d_quant_sat.find( f )!=d_quant_sat.end() ){
@@ -208,7 +215,7 @@ int ModelEngineBuilder::initializeQuantifier( Node f, Node fp ){
   if( d_quant_basis_match_added.find( f )==d_quant_basis_match_added.end() ){
     //create the basis match if necessary
     if( d_quant_basis_match.find( f )==d_quant_basis_match.end() ){
-      Trace("inst-fmf-init") << "Initialize " << f << ", parent = " << fp << std::endl;
+      Trace("inst-fmf-init") << "Initialize " << f << std::endl;
       //add the model basis instantiation
       // This will help produce the necessary information for model completion.
       // We do this by extending distinguish ground assertions (those
@@ -236,7 +243,6 @@ int ModelEngineBuilder::initializeQuantifier( Node f, Node fp ){
       //add model basis instantiation
       if( d_qe->addInstantiation( fp, d_quant_basis_match[f], false, false, false ) ){
         d_quant_basis_match_added[f] = true;
-        ++(d_statistics.d_num_quants_init_success);
         return 1;
       }else{
         //shouldn't happen usually, but will occur if x != y is a required literal for f.
@@ -322,22 +328,22 @@ void ModelEngineBuilder::setEffort( int effort ){
 }
 
 ModelEngineBuilder::Statistics::Statistics():
-  d_pre_sat_quant("ModelEngineBuilder::Status_quant_pre_sat", 0),
-  d_pre_nsat_quant("ModelEngineBuilder::Status_quant_pre_non_sat", 0),
-  d_num_quants_init("ModelEngine::Num_Quants", 0 ),
-  d_num_quants_init_success("ModelEngine::Num_Quants_Inst_Gen_Success", 0 )
+  d_num_quants_init("ModelEngineBuilder::Number_Quantifiers", 0),
+  d_num_partial_quants_init("ModelEngineBuilder::Number_Partial_Quantifiers", 0),
+  d_init_inst_gen_lemmas("ModelEngineBuilder::Initialize_Inst_Gen_Lemmas", 0 ),
+  d_inst_gen_lemmas("ModelEngineBuilder::Inst_Gen_Lemmas", 0 )
 {
-  StatisticsRegistry::registerStat(&d_pre_sat_quant);
-  StatisticsRegistry::registerStat(&d_pre_nsat_quant);
   StatisticsRegistry::registerStat(&d_num_quants_init);
-  StatisticsRegistry::registerStat(&d_num_quants_init_success);
+  StatisticsRegistry::registerStat(&d_num_partial_quants_init);
+  StatisticsRegistry::registerStat(&d_init_inst_gen_lemmas);
+  StatisticsRegistry::registerStat(&d_inst_gen_lemmas);
 }
 
 ModelEngineBuilder::Statistics::~Statistics(){
-  StatisticsRegistry::unregisterStat(&d_pre_sat_quant);
-  StatisticsRegistry::unregisterStat(&d_pre_nsat_quant);
   StatisticsRegistry::unregisterStat(&d_num_quants_init);
-  StatisticsRegistry::unregisterStat(&d_num_quants_init_success);
+  StatisticsRegistry::unregisterStat(&d_num_partial_quants_init);
+  StatisticsRegistry::unregisterStat(&d_init_inst_gen_lemmas);
+  StatisticsRegistry::unregisterStat(&d_inst_gen_lemmas);
 }
 
 bool ModelEngineBuilder::isQuantifierActive( Node f ){
@@ -470,9 +476,7 @@ void ModelEngineBuilderDefault::analyzeQuantifier( FirstOrderModel* fm, Node f )
       d_uf_prefs[ selectionLitTerms[i].getOperator() ].d_reconsiderModel = false;
     }
     Debug("fmf-model-prefs") << std::endl;
-    ++(d_statistics.d_pre_sat_quant);
   }else{
-    ++(d_statistics.d_pre_nsat_quant);
     //note quantifier's value preferences to models
     for( int k=0; k<2; k++ ){
       for( int j=0; j<(int)pro_con[k].size(); j++ ){
@@ -604,12 +608,14 @@ void ModelEngineBuilderDefault::constructModelUf( FirstOrderModel* fm, Node op )
 
 
 
-
+//////////////////////  Inst-Gen style Model Builder ///////////
 
 void ModelEngineBuilderInstGen::reset( FirstOrderModel* fm ){
   //for new inst gen
   d_quant_selection_formula.clear();
   d_term_selected.clear();
+
+  //d_sub_quant_inst_trie.clear();//*
 }
 
 int ModelEngineBuilderInstGen::initializeQuantifier( Node f, Node fp ){
@@ -621,6 +627,9 @@ int ModelEngineBuilderInstGen::initializeQuantifier( Node f, Node fp ){
 }
 
 void ModelEngineBuilderInstGen::analyzeQuantifier( FirstOrderModel* fm, Node f ){
+  //Node fp = getParentQuantifier( f );//*
+  //bool quantRedundant = ( f!=fp && d_sub_quant_inst_trie[fp].addInstMatch( d_qe, fp, d_sub_quant_inst[ f ], true ) );
+  //if( f==fp || d_sub_quant_inst_trie[fp].addInstMatch( d_qe, fp, d_sub_quant_inst[ f ], true ) ){//*
   Trace("sel-form-debug") << "* Analyze " << f << std::endl;
   //determine selection formula, set terms in selection formula as being selected
   Node s = getSelectionFormula( d_qe->getTermDatabase()->getInstConstantBody( f ),
@@ -659,9 +668,7 @@ int ModelEngineBuilderInstGen::doInstGen( FirstOrderModel* fm, Node f ){
     Trace("inst-gen") << "Do Inst-Gen for " << f << std::endl;
     if( fp!=f ) Trace("inst-gen") << "   ";
     Trace("inst-gen") << "Sel Form :      " << d_quant_selection_formula[f] << std::endl;
-    //we wish to add all known exceptions to our selection literal for f. this will help to refine our current model.
-    //This step is advantageous over exhaustive instantiation, since we are adding instantiations that involve model basis terms,
-    //  effectively acting as partial instantiations instead of pointwise instantiations.
+    //we wish to add all known exceptions to our selection formula for f. this will help to refine our current model.
     if( !d_quant_selection_formula[f].isNull() ){
       //first, try on sub quantifiers
       bool subQuantSat = true;
@@ -688,6 +695,7 @@ int ModelEngineBuilderInstGen::doInstGen( FirstOrderModel* fm, Node f ){
           if( igp.getMatchValue( i )!=fm->d_true ){
             InstMatch m;
             igp.getMatch( d_qe->getEqualityQuery(), i, m );
+            //Trace("inst-gen-debug") << "Inst Gen : " << m << std::endl;
             //we only consider matches that are non-empty
             //  matches that are empty should trigger other instances that are non-empty
             if( !m.empty() ){
@@ -695,9 +703,12 @@ int ModelEngineBuilderInstGen::doInstGen( FirstOrderModel* fm, Node f ){
               //translate to be in terms match in terms of fp
               InstMatch mp;
               getParentQuantifierMatch( mp, fp, m, f );
-
               //if this is a partial instantion
               if( !m.isComplete( f ) ){
+                //need to make it internal here
+                //Trace("mkInternal") << "Make internal representative " << mp << std::endl;
+                //mp.makeInternalRepresentative( d_qe );
+                //Trace("mkInternal") << "Got " << mp << std::endl;
                 //if the instantiation does not yet exist
                 if( d_sub_quant_inst_trie[fp].addInstMatch( d_qe, fp, mp, true ) ){
                   //also add it to children
@@ -709,9 +720,11 @@ int ModelEngineBuilderInstGen::doInstGen( FirstOrderModel* fm, Node f ){
                   d_sub_quants[ f ].push_back( pf );
                   d_sub_quant_inst[ pf ] = InstMatch( &mp );
                   d_sub_quant_parent[ pf ] = fp;
-                  //now make the match mp complete
+                  //now make mp a complete match
                   mp.add( d_quant_basis_match[ fp ] );
                   d_quant_basis_match[ pf ] = InstMatch( &mp );
+                  ++(d_statistics.d_num_quants_init);
+                  ++(d_statistics.d_num_partial_quants_init);
                   addedLemmas += initializeQuantifier( pf, fp );
                   Trace("inst-gen-pi") << "Done adding partial instantiation" << std::endl;
                   subQuantSat = false;
@@ -979,5 +992,5 @@ void ModelEngineBuilderInstGen::constructModelUf( FirstOrderModel* fm, Node op )
 }
 
 bool ModelEngineBuilderInstGen::existsInstantiation( Node f, InstMatch& m, bool modEq, bool modInst ){
-  return d_child_sub_quant_inst_trie[f].existsInstMatch( d_qe, f, m, modEq, modInst );
+  return d_child_sub_quant_inst_trie[f].existsInstMatch( d_qe, f, m, modEq, true );
 }
\ No newline at end of file
diff --git a/src/theory/quantifiers/model_builder.h b/src/theory/quantifiers/model_builder.h
index 7331daf8e..908cfca2b 100644
--- a/src/theory/quantifiers/model_builder.h
+++ b/src/theory/quantifiers/model_builder.h
@@ -69,7 +69,7 @@ protected:
 protected:
   //reset
   virtual void reset( FirstOrderModel* fm ) = 0;
-  //initialize quantifiers, return number of lemmas produced, fp is the parent of quantifier f
+  //initialize quantifiers, return number of lemmas produced
   virtual int initializeQuantifier( Node f, Node fp );
   //analyze model
   virtual void analyzeModel( FirstOrderModel* fm );
@@ -98,6 +98,8 @@ public:
   bool d_considerAxioms;
   // set effort
   void setEffort( int effort );
+  //debug model
+  void debugModel( FirstOrderModel* fm );
 public:
   //whether to construct model
   virtual bool optUseModel();
@@ -110,10 +112,10 @@ public:
   /** statistics class */
   class Statistics {
   public:
-    IntStat d_pre_sat_quant;
-    IntStat d_pre_nsat_quant;
     IntStat d_num_quants_init;
-    IntStat d_num_quants_init_success;
+    IntStat d_num_partial_quants_init;
+    IntStat d_init_inst_gen_lemmas;
+    IntStat d_inst_gen_lemmas;
     Statistics();
     ~Statistics();
   };
@@ -180,7 +182,7 @@ private:    ///information for (new) InstGen
   std::map< Node, bool > d_term_selected;
   //a collection of (complete) InstMatch structures produced for each root quantifier
   std::map< Node, inst::InstMatchTrie > d_sub_quant_inst_trie;
-  //a collection of InstMatch structures, representing the children for each quantifier
+  //for each quantifier, a collection of InstMatch structures, representing the children
   std::map< Node, inst::InstMatchTrie > d_child_sub_quant_inst_trie;
   //children quantifiers for each quantifier, each is an instance
   std::map< Node, std::vector< Node > > d_sub_quants;
diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp
index 87f842862..defb58bf2 100644
--- a/src/theory/quantifiers/model_engine.cpp
+++ b/src/theory/quantifiers/model_engine.cpp
@@ -153,19 +153,6 @@ bool ModelEngine::optExhInstEvalSkipMultiple(){
 #endif
 }
 
-bool containsNN( Node n, Node nc ){
-  if( n==nc ){
-    return true;
-  }else{
-    for( int i=0; i<(int)n.getNumChildren(); i++ ){
-      if( containsNN( n[i], nc ) ){
-        return true;
-      }
-    }
-    return false;
-  }
-}
-
 int ModelEngine::checkModel( int checkOption ){
   int addedLemmas = 0;
   FirstOrderModel* fm = d_quantEngine->getModel();
@@ -177,20 +164,11 @@ int ModelEngine::checkModel( int checkOption ){
         Trace("model-engine") << "Cardinality( " << it->first << " )" << " = " << it->second.size() << std::endl;
         Trace("model-engine-debug") << "   ";
         for( size_t i=0; i<it->second.size(); i++ ){
-          Trace("model-engine-debug") << it->second[i] << "  ";
+          //Trace("model-engine-debug") << it->second[i] << "  ";
+          Node r = ((EqualityQueryQuantifiersEngine*)d_quantEngine->getEqualityQuery())->getInternalRepresentative( it->second[i] );
+          Trace("model-engine-debug") << r << " ";
         }
         Trace("model-engine-debug") << std::endl;
-        for( size_t i=0; i<it->second.size(); i++ ){
-          std::vector< Node > eqc;
-          d_quantEngine->getEqualityQuery()->getEquivalenceClass( it->second[i], eqc );
-          Trace("model-engine-debug-eqc") << "      " << it->second[i] << " : { ";
-          for( size_t j=0; j<eqc.size(); j++ ){
-            if( it->second[i]!=eqc[j] && containsNN( it->second[i], eqc[j] ) ){
-              Trace("model-engine-debug-eqc") << eqc[j] << " ";
-            }
-          }
-          Trace("model-engine-debug-eqc") << "}" << std::endl;
-        }
       }
     }
   }
@@ -242,6 +220,7 @@ int ModelEngine::checkModel( int checkOption ){
     Trace("model-engine") << "Added Lemmas = " << addedLemmas << " / " << d_triedLemmas << " / ";
     Trace("model-engine") << d_testLemmas << " / " << d_relevantLemmas << " / " << d_totalLemmas << std::endl;
   }
+  d_statistics.d_exh_inst_lemmas += addedLemmas;
   return addedLemmas;
 }
 
@@ -361,13 +340,15 @@ ModelEngine::Statistics::Statistics():
   d_eval_formulas("ModelEngine::Eval_Formulas", 0 ),
   d_eval_uf_terms("ModelEngine::Eval_Uf_Terms", 0 ),
   d_eval_lits("ModelEngine::Eval_Lits", 0 ),
-  d_eval_lits_unknown("ModelEngine::Eval_Lits_Unknown", 0 )
+  d_eval_lits_unknown("ModelEngine::Eval_Lits_Unknown", 0 ),
+  d_exh_inst_lemmas("ModelEngine::Exhaustive_Instantiation_Lemmas", 0 )
 {
   StatisticsRegistry::registerStat(&d_inst_rounds);
   StatisticsRegistry::registerStat(&d_eval_formulas);
   StatisticsRegistry::registerStat(&d_eval_uf_terms);
   StatisticsRegistry::registerStat(&d_eval_lits);
   StatisticsRegistry::registerStat(&d_eval_lits_unknown);
+  StatisticsRegistry::registerStat(&d_exh_inst_lemmas);
 }
 
 ModelEngine::Statistics::~Statistics(){
@@ -376,6 +357,7 @@ ModelEngine::Statistics::~Statistics(){
   StatisticsRegistry::unregisterStat(&d_eval_uf_terms);
   StatisticsRegistry::unregisterStat(&d_eval_lits);
   StatisticsRegistry::unregisterStat(&d_eval_lits_unknown);
+  StatisticsRegistry::unregisterStat(&d_exh_inst_lemmas);
 }
 
 
diff --git a/src/theory/quantifiers/model_engine.h b/src/theory/quantifiers/model_engine.h
index 2560cf50e..394ceaf42 100644
--- a/src/theory/quantifiers/model_engine.h
+++ b/src/theory/quantifiers/model_engine.h
@@ -78,6 +78,7 @@ public:
     IntStat d_eval_uf_terms;
     IntStat d_eval_lits;
     IntStat d_eval_lits_unknown;
+    IntStat d_exh_inst_lemmas;
     Statistics();
     ~Statistics();
   };
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index d637fa25f..591270ab0 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -161,27 +161,29 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){
    }
    for( int i=0; i<2; i++ ){
      Node n = NodeManager::currentNM()->mkConst( i==1 );
-     eq::EqClassIterator eqc( d_quantEngine->getEqualityQuery()->getRepresentative( n ),
-                              d_quantEngine->getEqualityQuery()->getEngine() );
-     while( !eqc.isFinished() ){
-       Node en = (*eqc);
-       computeModelBasisArgAttribute( en );
-       if( en.getKind()==APPLY_UF && !en.hasAttribute(InstConstantAttribute()) ){
-         if( !en.getAttribute(NoMatchAttribute()) ){
-           Node op = en.getOperator();
-           if( !d_pred_map_trie[i][op].addTerm( d_quantEngine, en ) ){
-             NoMatchAttribute nma;
-             en.setAttribute(nma,true);
-             congruentCount++;
+     if( d_quantEngine->getEqualityQuery()->getEngine()->hasTerm( n ) ){
+       eq::EqClassIterator eqc( d_quantEngine->getEqualityQuery()->getEngine()->getRepresentative( n ),
+                                d_quantEngine->getEqualityQuery()->getEngine() );
+       while( !eqc.isFinished() ){
+         Node en = (*eqc);
+         computeModelBasisArgAttribute( en );
+         if( en.getKind()==APPLY_UF && !en.hasAttribute(InstConstantAttribute()) ){
+           if( !en.getAttribute(NoMatchAttribute()) ){
+             Node op = en.getOperator();
+             if( !d_pred_map_trie[i][op].addTerm( d_quantEngine, en ) ){
+               NoMatchAttribute nma;
+               en.setAttribute(nma,true);
+               congruentCount++;
+             }else{
+               nonCongruentCount++;
+               d_op_count[ op ]++;
+             }
            }else{
-             nonCongruentCount++;
-             d_op_count[ op ]++;
+             alreadyCongruentCount++;
            }
-         }else{
-           alreadyCongruentCount++;
          }
+         ++eqc;
        }
-       ++eqc;
      }
    }
    Debug("term-db-cong") << "TermDb: Reset" << std::endl;
@@ -300,6 +302,25 @@ void TermDb::setInstantiationConstantAttr( Node n, Node f ){
   }
 }
 
+/** get the i^th instantiation constant of f */
+Node TermDb::getInstantiationConstant( Node f, int i ) const {
+  std::map< Node, std::vector< Node > >::const_iterator it = d_inst_constants.find( f );
+  if( it!=d_inst_constants.end() ){
+    return it->second[i];
+  }else{
+    return Node::null();
+  }
+}
+
+/** get number of instantiation constants for f */
+int TermDb::getNumInstantiationConstants( Node f ) const {
+  std::map< Node, std::vector< Node > >::const_iterator it = d_inst_constants.find( f );
+  if( it!=d_inst_constants.end() ){
+    return (int)it->second.size();
+  }else{
+    return 0;
+  }
+}
 
 Node TermDb::getInstConstantBody( Node f ){
   std::map< Node, Node >::iterator it = d_inst_const_body.find( f );
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index e1786d44c..5060ac1a7 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -154,9 +154,9 @@ private:
   void makeInstantiationConstantsFor( Node f );
 public:
   /** get the i^th instantiation constant of f */
-  Node getInstantiationConstant( Node f, int i ) { return d_inst_constants[f][i]; }
+  Node getInstantiationConstant( Node f, int i ) const;
   /** get number of instantiation constants for f */
-  int getNumInstantiationConstants( Node f ) { return (int)d_inst_constants[f].size(); }
+  int getNumInstantiationConstants( Node f ) const;
   /** get the ce body f[e/x] */
   Node getInstConstantBody( Node f );
   /** get counterexample literal (for cbqi) */
diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp
index c64a75ec4..553189d13 100644
--- a/src/theory/quantifiers/trigger.cpp
+++ b/src/theory/quantifiers/trigger.cpp
@@ -85,7 +85,6 @@ void Trigger::reset( Node eqc ){
 
 bool Trigger::getNextMatch( InstMatch& m ){
   bool retVal = d_mg->getNextMatch( m, d_quantEngine );
-  //m.makeInternal( d_quantEngine->getEqualityQuery() );
   return retVal;
 }
 
@@ -98,10 +97,6 @@ int Trigger::addTerm( Node t ){
   return d_mg->addTerm( d_f, t, d_quantEngine );
 }
 
-//bool Trigger::nonunifiable( TNode t, const std::vector<Node> & vars){
-//  return d_mg->nonunifiable(t,vars);
-//}
-
 int Trigger::addInstantiations( InstMatch& baseMatch ){
   int addedLemmas = d_mg->addInstantiations( d_f, baseMatch, d_quantEngine );
   if( addedLemmas>0 ){
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index ebd6d32ea..3f6ba8a0f 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -719,6 +719,22 @@ Node EqualityQueryQuantifiersEngine::getInstance( Node n, std::vector< Node >& e
   }
 }
 
+int getDepth( Node n ){
+  if( n.getNumChildren()==0 ){
+    return 0;
+  }else{
+    int maxDepth = -1;
+    for( int i=0; i<(int)n.getNumChildren(); i++ ){
+      int depth = getDepth( n[i] );
+      if( depth>maxDepth ){
+        maxDepth = depth;
+      }
+    }
+    return maxDepth;
+  }
+}
+
 int EqualityQueryQuantifiersEngine::getRepScore( Node n ){
-  return d_rep_score.find( n )==d_rep_score.end() ? -1 : d_rep_score[n];
+  return d_rep_score.find( n )==d_rep_score.end() ? -1 : d_rep_score[n];          //initial
+  //return ( d_rep_score.find( n )==d_rep_score.end() ? 100 : 0 ) + getDepth( n );    //term depth
 }
diff --git a/src/theory/uf/inst_strategy.cpp b/src/theory/uf/inst_strategy.cpp
index 4fe5772de..433ceee85 100644
--- a/src/theory/uf/inst_strategy.cpp
+++ b/src/theory/uf/inst_strategy.cpp
@@ -322,34 +322,6 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){
   }
 }
 
-#if 0
-
-void InstStrategyAddFailSplits::processResetInstantiationRound( Theory::Effort effort ){
-}
-
-int InstStrategyAddFailSplits::process( Node f, Theory::Effort effort, int e ){
-  if( e<4 ){
-    return STATUS_UNFINISHED;
-  }else{
-    for( std::map< Node, std::map< Node, std::vector< InstMatchGenerator* > > >::iterator it = InstMatchGenerator::d_match_fails.begin();
-         it != InstMatchGenerator::d_match_fails.end(); ++it ){
-      for( std::map< Node, std::vector< InstMatchGenerator* > >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){
-        if( !it2->second.empty() ){
-          Node n1 = it->first;
-          Node n2 = it2->first;
-          if( !d_quantEngine->getEqualityQuery()->areEqual( n1, n2 ) && !d_quantEngine->getEqualityQuery()->areDisequal( n1, n2 ) ){
-            d_quantEngine->addSplitEquality( n1, n2, true );
-          }
-          it2->second.clear();
-        }
-      }
-    }
-    return STATUS_UNKNOWN;
-  }
-}
-
-#endif /* 0 */
-
 void InstStrategyFreeVariable::processResetInstantiationRound( Theory::Effort effort ){
 }
 
diff --git a/src/theory/uf/inst_strategy.h b/src/theory/uf/inst_strategy.h
index 5a3b9cc3d..aaa5f27a1 100644
--- a/src/theory/uf/inst_strategy.h
+++ b/src/theory/uf/inst_strategy.h
@@ -116,25 +116,6 @@ public:
   void setGenerateAdditional( bool val ) { d_generate_additional = val; }
 };/* class InstStrategyAutoGenTriggers */
 
-#if 0
-
-class InstStrategyAddFailSplits : public InstStrategy{
-private:
-  /** InstantiatorTheoryUf class */
-  InstantiatorTheoryUf* d_th;
-  /** process functions */
-  void processResetInstantiationRound( Theory::Effort effort );
-  int process( Node f, Theory::Effort effort, int e );
-public:
-  InstStrategyAddFailSplits( InstantiatorTheoryUf* th, QuantifiersEngine* ie ) :
-      InstStrategy( ie ), d_th( th ){}
-  ~InstStrategyAddFailSplits(){}
-  /** identify */
-  std::string identify() const { return std::string("AddFailSplits"); }
-};/* class InstStrategyAddFailSplits */
-
-#endif /* 0 */
-
 class InstStrategyFreeVariable : public InstStrategy{
 private:
   /** InstantiatorTheoryUf class */