Minor cleanup and additions to quantifiers statistics.

9 files changed, 40 insertions, 47 deletions

diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp
index 165c9904d..f432817fd 100644
--- a/src/theory/quantifiers/inst_strategy_cbqi.cpp
+++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp
@@ -689,6 +689,7 @@ bool InstStrategyCegqi::doAddInstantiation( std::vector< Node >& subs ) {
     //check if we need virtual term substitution (if used delta or infinity)
     bool used_vts = d_quantEngine->getTermDatabase()->containsVtsTerm( subs, false );
     if( d_quantEngine->addInstantiation( d_curr_quant, subs, false, false, used_vts ) ){
+      ++(d_quantEngine->d_statistics.d_instantiations_cbqi);
       //d_added_inst.insert( d_curr_quant );
       return true;
     }else{
diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp
index f46d08f08..afeed1e5d 100644
--- a/src/theory/quantifiers/instantiation_engine.cpp
+++ b/src/theory/quantifiers/instantiation_engine.cpp
@@ -114,6 +114,7 @@ void InstantiationEngine::reset_round( Theory::Effort e ){
 }
 
 void InstantiationEngine::check( Theory::Effort e, unsigned quant_e ){
+  CodeTimer codeTimer(d_quantEngine->d_statistics.d_ematching_time);
   if( quant_e==QuantifiersEngine::QEFFORT_STANDARD ){
     double clSet = 0;
     if( Trace.isOn("inst-engine") ){
diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp
index 7f560b74c..9c09371c4 100644
--- a/src/theory/quantifiers/model_engine.cpp
+++ b/src/theory/quantifiers/model_engine.cpp
@@ -73,7 +73,6 @@ void ModelEngine::check( Theory::Effort e, unsigned quant_e ){
       Trace("model-engine") << "---Model Engine Round---" << std::endl;
       clSet = double(clock())/double(CLOCKS_PER_SEC);
     }
-    ++(d_statistics.d_inst_rounds);
 
     Trace("model-engine-debug") << "Verify uf ss is minimal..." << std::endl;
     //let the strong solver verify that the model is minimal
@@ -275,7 +274,7 @@ void ModelEngine::exhaustiveInstantiate( Node f, int effort ){
     }
     d_triedLemmas += mb->d_triedLemmas;
     d_addedLemmas += mb->d_addedLemmas;
-    d_statistics.d_mbqi_inst_lemmas += mb->d_addedLemmas;
+    d_quantEngine->d_statistics.d_instantiations_fmf_mbqi += mb->d_addedLemmas;
   }else{
     if( Trace.isOn("fmf-exh-inst-debug") ){
       Trace("fmf-exh-inst-debug") << "   Instantiation Constants: ";
@@ -312,7 +311,7 @@ void ModelEngine::exhaustiveInstantiate( Node f, int effort ){
         }
         d_addedLemmas += addedLemmas;
         d_triedLemmas += triedLemmas;
-        d_statistics.d_exh_inst_lemmas += addedLemmas;
+        d_quantEngine->d_statistics.d_instantiations_fmf_exh += addedLemmas;
       }
     }else{
       Trace("fmf-exh-inst") << "...exhaustive instantiation did set, incomplete=" << riter.isIncomplete() << "..." << std::endl;
@@ -339,18 +338,3 @@ void ModelEngine::debugPrint( const char* c ){
   //d_quantEngine->getModel()->debugPrint( c );
 }
 
-ModelEngine::Statistics::Statistics():
-  d_inst_rounds("ModelEngine::Inst_Rounds", 0),
-  d_exh_inst_lemmas("ModelEngine::Instantiations_Exhaustive", 0 ),
-  d_mbqi_inst_lemmas("ModelEngine::Instantiations_Mbqi", 0 )
-{
-  smtStatisticsRegistry()->registerStat(&d_inst_rounds);
-  smtStatisticsRegistry()->registerStat(&d_exh_inst_lemmas);
-  smtStatisticsRegistry()->registerStat(&d_mbqi_inst_lemmas);
-}
-
-ModelEngine::Statistics::~Statistics(){
-  smtStatisticsRegistry()->unregisterStat(&d_inst_rounds);
-  smtStatisticsRegistry()->unregisterStat(&d_exh_inst_lemmas);
-  smtStatisticsRegistry()->unregisterStat(&d_mbqi_inst_lemmas);
-}
diff --git a/src/theory/quantifiers/model_engine.h b/src/theory/quantifiers/model_engine.h
index 8575792b4..e89be8d2b 100644
--- a/src/theory/quantifiers/model_engine.h
+++ b/src/theory/quantifiers/model_engine.h
@@ -61,17 +61,6 @@ public:
   void assertNode( Node f );
   Node explain(TNode n){ return Node::null(); }
   void debugPrint( const char* c );
-public:
-  /** statistics class */
-  class Statistics {
-  public:
-    IntStat d_inst_rounds;
-    IntStat d_exh_inst_lemmas;
-    IntStat d_mbqi_inst_lemmas;
-    Statistics();
-    ~Statistics();
-  };
-  Statistics d_statistics;
   /** Identify this module */
   std::string identify() const { return "ModelEngine"; }
 };/* class ModelEngine */
diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index 31831d73b..9b25e27d4 100644
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -2024,6 +2024,7 @@ void QuantConflictFind::setIrrelevantFunction( TNode f ) {
 
 /** check */
 void QuantConflictFind::check( Theory::Effort level, unsigned quant_e ) {
+  CodeTimer codeTimer(d_quantEngine->d_statistics.d_qcf_time);
   if( quant_e==QuantifiersEngine::QEFFORT_CONFLICT ){
     Trace("qcf-check") << "QCF : check : " << level << std::endl;
     if( d_conflict ){
@@ -2098,7 +2099,7 @@ void QuantConflictFind::check( Theory::Effort level, unsigned quant_e ) {
                           ++addedLemmas;
                           if( e==effort_conflict ){
                             d_quantEngine->markRelevant( q );
-                            ++(d_statistics.d_conflict_inst);
+                            ++(d_quantEngine->d_statistics.d_instantiations_qcf);
                             if( options::qcfAllConflict() ){
                               isConflict = true;
                             }else{
@@ -2107,7 +2108,7 @@ void QuantConflictFind::check( Theory::Effort level, unsigned quant_e ) {
                             break;
                           }else if( e==effort_prop_eq ){
                             d_quantEngine->markRelevant( q );
-                            ++(d_statistics.d_prop_inst);
+                            ++(d_quantEngine->d_statistics.d_instantiations_qcf);
                           }
                         }else{
                           Trace("qcf-inst") << "   ... Failed to add instantiation" << std::endl;
@@ -2234,20 +2235,14 @@ void QuantConflictFind::debugPrintQuantBody( const char * c, Node q, Node n, boo
 
 QuantConflictFind::Statistics::Statistics():
   d_inst_rounds("QuantConflictFind::Inst_Rounds", 0),
-  d_conflict_inst("QuantConflictFind::Instantiations_Conflict_Find", 0 ),
-  d_prop_inst("QuantConflictFind::Instantiations_Prop", 0 ),
   d_entailment_checks("QuantConflictFind::Entailment_Checks",0)
 {
   smtStatisticsRegistry()->registerStat(&d_inst_rounds);
-  smtStatisticsRegistry()->registerStat(&d_conflict_inst);
-  smtStatisticsRegistry()->registerStat(&d_prop_inst);
   smtStatisticsRegistry()->registerStat(&d_entailment_checks);
 }
 
 QuantConflictFind::Statistics::~Statistics(){
   smtStatisticsRegistry()->unregisterStat(&d_inst_rounds);
-  smtStatisticsRegistry()->unregisterStat(&d_conflict_inst);
-  smtStatisticsRegistry()->unregisterStat(&d_prop_inst);
   smtStatisticsRegistry()->unregisterStat(&d_entailment_checks);
 }
 
diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h
index 47a66b1b1..dc8a9acb2 100644
--- a/src/theory/quantifiers/quant_conflict_find.h
+++ b/src/theory/quantifiers/quant_conflict_find.h
@@ -260,8 +260,6 @@ public:
   class Statistics {
   public:
     IntStat d_inst_rounds;
-    IntStat d_conflict_inst;
-    IntStat d_prop_inst;
     IntStat d_entailment_checks;
     Statistics();
     ~Statistics();
diff --git a/src/theory/quantifiers/rewrite_engine.cpp b/src/theory/quantifiers/rewrite_engine.cpp
index a2a2e99c6..ec1b41a98 100644
--- a/src/theory/quantifiers/rewrite_engine.cpp
+++ b/src/theory/quantifiers/rewrite_engine.cpp
@@ -205,6 +205,7 @@ int RewriteEngine::checkRewriteRule( Node f, Theory::Effort e ) {
       Trace("rewrite-engine-inst-debug") << "...No qinfo." << std::endl;
     }
   }
+  d_quantEngine->d_statistics.d_instantiations_rr += addedLemmas;
   Trace("rewrite-engine-inst") << "-> Generated " << addedLemmas << " lemmas." << std::endl;
   return addedLemmas;
 }
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index ec20d1ede..08faa8dc7 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -1512,6 +1512,8 @@ Node QuantifiersEngine::getInstantiatedConjunction( Node q ) {
 
 QuantifiersEngine::Statistics::Statistics()
     : d_time("theory::QuantifiersEngine::time"),
+      d_qcf_time("theory::QuantifiersEngine::time_qcf"),
+      d_ematching_time("theory::QuantifiersEngine::time_ematching"),
       d_num_quant("QuantifiersEngine::Num_Quantifiers", 0),
       d_instantiation_rounds("QuantifiersEngine::Rounds_Instantiation_Full", 0),
       d_instantiation_rounds_lc("QuantifiersEngine::Rounds_Instantiation_Last_Call", 0),
@@ -1523,13 +1525,19 @@ QuantifiersEngine::Statistics::Statistics()
       d_multi_triggers("QuantifiersEngine::Triggers_Multi", 0),
       d_multi_trigger_instantiations("QuantifiersEngine::Multi_Trigger_Instantiations", 0),
       d_red_alpha_equiv("QuantifiersEngine::Reductions_Alpha_Equivalence", 0),
-      d_red_lte_partial_inst("QuantifiersEngine::Reductions_Lte_Partial_Inst", 0),
       d_instantiations_user_patterns("QuantifiersEngine::Instantiations_User_Patterns", 0),
       d_instantiations_auto_gen("QuantifiersEngine::Instantiations_Auto_Gen", 0),
       d_instantiations_guess("QuantifiersEngine::Instantiations_Guess", 0),
-      d_instantiations_cbqi_arith("QuantifiersEngine::Instantiations_Cbqi_Arith", 0)
+      d_instantiations_qcf("QuantifiersEngine::Instantiations_Qcf_Conflict", 0),
+      d_instantiations_qcf_prop("QuantifiersEngine::Instantiations_Qcf_Prop", 0),
+      d_instantiations_fmf_exh("QuantifiersEngine::Instantiations_Fmf_Exh", 0),
+      d_instantiations_fmf_mbqi("QuantifiersEngine::Instantiations_Fmf_Mbqi", 0),
+      d_instantiations_cbqi("QuantifiersEngine::Instantiations_Cbqi", 0),
+      d_instantiations_rr("QuantifiersEngine::Instantiations_Rewrite_Rules", 0)
 {
   smtStatisticsRegistry()->registerStat(&d_time);
+  smtStatisticsRegistry()->registerStat(&d_qcf_time);
+  smtStatisticsRegistry()->registerStat(&d_ematching_time);
   smtStatisticsRegistry()->registerStat(&d_num_quant);
   smtStatisticsRegistry()->registerStat(&d_instantiation_rounds);
   smtStatisticsRegistry()->registerStat(&d_instantiation_rounds_lc);
@@ -1541,15 +1549,21 @@ QuantifiersEngine::Statistics::Statistics()
   smtStatisticsRegistry()->registerStat(&d_multi_triggers);
   smtStatisticsRegistry()->registerStat(&d_multi_trigger_instantiations);
   smtStatisticsRegistry()->registerStat(&d_red_alpha_equiv);
-  smtStatisticsRegistry()->registerStat(&d_red_lte_partial_inst);
   smtStatisticsRegistry()->registerStat(&d_instantiations_user_patterns);
   smtStatisticsRegistry()->registerStat(&d_instantiations_auto_gen);
   smtStatisticsRegistry()->registerStat(&d_instantiations_guess);
-  smtStatisticsRegistry()->registerStat(&d_instantiations_cbqi_arith);
+  smtStatisticsRegistry()->registerStat(&d_instantiations_qcf);
+  smtStatisticsRegistry()->registerStat(&d_instantiations_qcf_prop);
+  smtStatisticsRegistry()->registerStat(&d_instantiations_fmf_exh);
+  smtStatisticsRegistry()->registerStat(&d_instantiations_fmf_mbqi);
+  smtStatisticsRegistry()->registerStat(&d_instantiations_cbqi);
+  smtStatisticsRegistry()->registerStat(&d_instantiations_rr);
 }
 
 QuantifiersEngine::Statistics::~Statistics(){
   smtStatisticsRegistry()->unregisterStat(&d_time);
+  smtStatisticsRegistry()->unregisterStat(&d_qcf_time);
+  smtStatisticsRegistry()->unregisterStat(&d_ematching_time);
   smtStatisticsRegistry()->unregisterStat(&d_num_quant);
   smtStatisticsRegistry()->unregisterStat(&d_instantiation_rounds);
   smtStatisticsRegistry()->unregisterStat(&d_instantiation_rounds_lc);
@@ -1561,11 +1575,15 @@ QuantifiersEngine::Statistics::~Statistics(){
   smtStatisticsRegistry()->unregisterStat(&d_multi_triggers);
   smtStatisticsRegistry()->unregisterStat(&d_multi_trigger_instantiations);
   smtStatisticsRegistry()->unregisterStat(&d_red_alpha_equiv);
-  smtStatisticsRegistry()->unregisterStat(&d_red_lte_partial_inst);
   smtStatisticsRegistry()->unregisterStat(&d_instantiations_user_patterns);
   smtStatisticsRegistry()->unregisterStat(&d_instantiations_auto_gen);
   smtStatisticsRegistry()->unregisterStat(&d_instantiations_guess);
-  smtStatisticsRegistry()->unregisterStat(&d_instantiations_cbqi_arith);
+  smtStatisticsRegistry()->unregisterStat(&d_instantiations_qcf);
+  smtStatisticsRegistry()->unregisterStat(&d_instantiations_qcf_prop);
+  smtStatisticsRegistry()->unregisterStat(&d_instantiations_fmf_exh);
+  smtStatisticsRegistry()->unregisterStat(&d_instantiations_fmf_mbqi);
+  smtStatisticsRegistry()->unregisterStat(&d_instantiations_cbqi);
+  smtStatisticsRegistry()->unregisterStat(&d_instantiations_rr);
 }
 
 eq::EqualityEngine* QuantifiersEngine::getMasterEqualityEngine(){
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index 25542e49e..d501cfc76 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -388,6 +388,8 @@ public:
   class Statistics {
   public:
     TimerStat d_time;
+    TimerStat d_qcf_time;
+    TimerStat d_ematching_time;
     IntStat d_num_quant;
     IntStat d_instantiation_rounds;
     IntStat d_instantiation_rounds_lc;
@@ -399,11 +401,15 @@ public:
     IntStat d_multi_triggers;
     IntStat d_multi_trigger_instantiations;
     IntStat d_red_alpha_equiv;
-    IntStat d_red_lte_partial_inst;
     IntStat d_instantiations_user_patterns;
     IntStat d_instantiations_auto_gen;
     IntStat d_instantiations_guess;
-    IntStat d_instantiations_cbqi_arith;
+    IntStat d_instantiations_qcf;
+    IntStat d_instantiations_qcf_prop;
+    IntStat d_instantiations_fmf_exh;
+    IntStat d_instantiations_fmf_mbqi;
+    IntStat d_instantiations_cbqi;
+    IntStat d_instantiations_rr;
     Statistics();
     ~Statistics();
   };/* class QuantifiersEngine::Statistics */