From bf1597c53ef6b3d5e6ce6b5601d0b3f97fbea9d9 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Thu, 29 Sep 2016 16:01:34 -0500 Subject: [PATCH] Minor cleanup and additions to quantifiers statistics. --- src/theory/quantifiers/inst_strategy_cbqi.cpp | 1 + .../quantifiers/instantiation_engine.cpp | 1 + src/theory/quantifiers/model_engine.cpp | 20 ++----------- src/theory/quantifiers/model_engine.h | 11 ------- .../quantifiers/quant_conflict_find.cpp | 11 ++----- src/theory/quantifiers/quant_conflict_find.h | 2 -- src/theory/quantifiers/rewrite_engine.cpp | 1 + src/theory/quantifiers_engine.cpp | 30 +++++++++++++++---- src/theory/quantifiers_engine.h | 10 +++++-- 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 */ -- 2.30.2