Minor cleanup and additions to quantifiers statistics.

1 files changed, 24 insertions, 6 deletions

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(){