diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-09-29 16:01:34 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-09-29 16:01:34 -0500 |
commit | bf1597c53ef6b3d5e6ce6b5601d0b3f97fbea9d9 (patch) | |
tree | ec121429b7af1fbae0fb24de9032b5a88ad9d3e3 /src/theory/quantifiers_engine.cpp | |
parent | fe72120c20dc211c7fdf02af7ff1a89527366a47 (diff) |
Minor cleanup and additions to quantifiers statistics.
Diffstat (limited to 'src/theory/quantifiers_engine.cpp')
-rw-r--r-- | src/theory/quantifiers_engine.cpp | 30 |
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(){ |