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/quant_conflict_find.cpp | |
parent | fe72120c20dc211c7fdf02af7ff1a89527366a47 (diff) |
Minor cleanup and additions to quantifiers statistics.
Diffstat (limited to 'src/theory/quantifiers/quant_conflict_find.cpp')
-rw-r--r-- | src/theory/quantifiers/quant_conflict_find.cpp | 11 |
1 files changed, 3 insertions, 8 deletions
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); } |