diff options
Diffstat (limited to 'src/theory/quantifiers')
-rw-r--r-- | src/theory/quantifiers/cegqi/ceg_instantiator.h | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/cegqi/inst_strategy_cegqi.h | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/instantiate.cpp | 24 | ||||
-rw-r--r-- | src/theory/quantifiers/instantiate.h | 3 | ||||
-rw-r--r-- | src/theory/quantifiers/quant_conflict_find.cpp | 15 | ||||
-rw-r--r-- | src/theory/quantifiers/quant_conflict_find.h | 1 | ||||
-rw-r--r-- | src/theory/quantifiers/quantifiers_inference_manager.cpp | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/quantifiers_statistics.cpp | 55 | ||||
-rw-r--r-- | src/theory/quantifiers/quantifiers_statistics.h | 4 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_stats.cpp | 50 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_stats.h | 3 | ||||
-rw-r--r-- | src/theory/quantifiers/term_tuple_enumerator.cpp | 2 |
12 files changed, 58 insertions, 105 deletions
diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.h b/src/theory/quantifiers/cegqi/ceg_instantiator.h index 2264127cf..0279a72ca 100644 --- a/src/theory/quantifiers/cegqi/ceg_instantiator.h +++ b/src/theory/quantifiers/cegqi/ceg_instantiator.h @@ -22,7 +22,7 @@ #include "expr/node.h" #include "theory/inference_id.h" -#include "util/statistics_registry.h" +#include "util/statistics_stats.h" namespace cvc5 { namespace theory { diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h index 7ab0f1b8f..266de9a53 100644 --- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h +++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h @@ -25,7 +25,7 @@ #include "theory/quantifiers/cegqi/vts_term_cache.h" #include "theory/quantifiers/instantiate.h" #include "theory/quantifiers/quant_module.h" -#include "util/statistics_registry.h" +#include "util/statistics_stats.h" namespace cvc5 { namespace theory { diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp index 5f83578df..0415d4271 100644 --- a/src/theory/quantifiers/instantiate.cpp +++ b/src/theory/quantifiers/instantiate.cpp @@ -742,23 +742,15 @@ InstLemmaList* Instantiate::getOrMkInstLemmaList(TNode q) } Instantiate::Statistics::Statistics() - : d_instantiations("Instantiate::Instantiations_Total", 0), - d_inst_duplicate("Instantiate::Duplicate_Inst", 0), - d_inst_duplicate_eq("Instantiate::Duplicate_Inst_Eq", 0), - d_inst_duplicate_ent("Instantiate::Duplicate_Inst_Entailed", 0) + : d_instantiations(smtStatisticsRegistry().registerInt( + "Instantiate::Instantiations_Total")), + d_inst_duplicate( + smtStatisticsRegistry().registerInt("Instantiate::Duplicate_Inst")), + d_inst_duplicate_eq(smtStatisticsRegistry().registerInt( + "Instantiate::Duplicate_Inst_Eq")), + d_inst_duplicate_ent(smtStatisticsRegistry().registerInt( + "Instantiate::Duplicate_Inst_Entailed")) { - smtStatisticsRegistry()->registerStat(&d_instantiations); - smtStatisticsRegistry()->registerStat(&d_inst_duplicate); - smtStatisticsRegistry()->registerStat(&d_inst_duplicate_eq); - smtStatisticsRegistry()->registerStat(&d_inst_duplicate_ent); -} - -Instantiate::Statistics::~Statistics() -{ - smtStatisticsRegistry()->unregisterStat(&d_instantiations); - smtStatisticsRegistry()->unregisterStat(&d_inst_duplicate); - smtStatisticsRegistry()->unregisterStat(&d_inst_duplicate_eq); - smtStatisticsRegistry()->unregisterStat(&d_inst_duplicate_ent); } } // namespace quantifiers diff --git a/src/theory/quantifiers/instantiate.h b/src/theory/quantifiers/instantiate.h index f420c0f62..42bff316a 100644 --- a/src/theory/quantifiers/instantiate.h +++ b/src/theory/quantifiers/instantiate.h @@ -26,7 +26,7 @@ #include "theory/inference_id.h" #include "theory/quantifiers/inst_match_trie.h" #include "theory/quantifiers/quant_util.h" -#include "util/statistics_registry.h" +#include "util/statistics_stats.h" namespace cvc5 { @@ -290,7 +290,6 @@ class Instantiate : public QuantifiersUtil IntStat d_inst_duplicate_eq; IntStat d_inst_duplicate_ent; Statistics(); - ~Statistics(); }; /* class Instantiate::Statistics */ Statistics d_statistics; diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index 791f843fa..cff9fde0b 100644 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -2270,17 +2270,12 @@ void QuantConflictFind::debugPrintQuantBody( const char * c, Node q, Node n, boo } } -QuantConflictFind::Statistics::Statistics(): - d_inst_rounds("QuantConflictFind::Inst_Rounds", 0), - d_entailment_checks("QuantConflictFind::Entailment_Checks",0) +QuantConflictFind::Statistics::Statistics() + : d_inst_rounds( + smtStatisticsRegistry().registerInt("QuantConflictFind::Inst_Rounds")), + d_entailment_checks(smtStatisticsRegistry().registerInt( + "QuantConflictFind::Entailment_Checks")) { - smtStatisticsRegistry()->registerStat(&d_inst_rounds); - smtStatisticsRegistry()->registerStat(&d_entailment_checks); -} - -QuantConflictFind::Statistics::~Statistics(){ - smtStatisticsRegistry()->unregisterStat(&d_inst_rounds); - smtStatisticsRegistry()->unregisterStat(&d_entailment_checks); } TNode QuantConflictFind::getZero( Kind k ) { diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h index b533a3f12..5a36452fe 100644 --- a/src/theory/quantifiers/quant_conflict_find.h +++ b/src/theory/quantifiers/quant_conflict_find.h @@ -287,7 +287,6 @@ public: IntStat d_inst_rounds; IntStat d_entailment_checks; Statistics(); - ~Statistics(); }; Statistics d_statistics; /** Identify this module */ diff --git a/src/theory/quantifiers/quantifiers_inference_manager.cpp b/src/theory/quantifiers/quantifiers_inference_manager.cpp index 0f7c65924..67f8f6f8e 100644 --- a/src/theory/quantifiers/quantifiers_inference_manager.cpp +++ b/src/theory/quantifiers/quantifiers_inference_manager.cpp @@ -28,7 +28,7 @@ QuantifiersInferenceManager::QuantifiersInferenceManager( QuantifiersRegistry& qr, TermRegistry& tr, ProofNodeManager* pnm) - : InferenceManagerBuffered(t, state, pnm, "theory::quantifiers"), + : InferenceManagerBuffered(t, state, pnm, "theory::quantifiers::"), d_instantiate(new Instantiate(state, *this, qr, tr, pnm)), d_skolemize(new Skolemize(state, tr, pnm)) { diff --git a/src/theory/quantifiers/quantifiers_statistics.cpp b/src/theory/quantifiers/quantifiers_statistics.cpp index e3c17fd77..59fdb1808 100644 --- a/src/theory/quantifiers/quantifiers_statistics.cpp +++ b/src/theory/quantifiers/quantifiers_statistics.cpp @@ -22,42 +22,27 @@ namespace theory { namespace quantifiers { QuantifiersStatistics::QuantifiersStatistics() - : 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), - d_triggers("QuantifiersEngine::Triggers", 0), - d_simple_triggers("QuantifiersEngine::Triggers_Simple", 0), - d_multi_triggers("QuantifiersEngine::Triggers_Multi", 0), - d_red_alpha_equiv("QuantifiersEngine::Reductions_Alpha_Equivalence", 0) + : d_time(smtStatisticsRegistry().registerTimer( + "theory::QuantifiersEngine::time")), + d_qcf_time(smtStatisticsRegistry().registerTimer( + "theory::QuantifiersEngine::time_qcf")), + d_ematching_time(smtStatisticsRegistry().registerTimer( + "theory::QuantifiersEngine::time_ematching")), + d_num_quant(smtStatisticsRegistry().registerInt( + "QuantifiersEngine::Num_Quantifiers")), + d_instantiation_rounds(smtStatisticsRegistry().registerInt( + "QuantifiersEngine::Rounds_Instantiation_Full")), + d_instantiation_rounds_lc(smtStatisticsRegistry().registerInt( + "QuantifiersEngine::Rounds_Instantiation_Last_Call")), + d_triggers( + smtStatisticsRegistry().registerInt("QuantifiersEngine::Triggers")), + d_simple_triggers(smtStatisticsRegistry().registerInt( + "QuantifiersEngine::Triggers_Simple")), + d_multi_triggers(smtStatisticsRegistry().registerInt( + "QuantifiersEngine::Triggers_Multi")), + d_red_alpha_equiv(smtStatisticsRegistry().registerInt( + "QuantifiersEngine::Reductions_Alpha_Equivalence")) { - 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); - smtStatisticsRegistry()->registerStat(&d_triggers); - smtStatisticsRegistry()->registerStat(&d_simple_triggers); - smtStatisticsRegistry()->registerStat(&d_multi_triggers); - smtStatisticsRegistry()->registerStat(&d_red_alpha_equiv); -} - -QuantifiersStatistics::~QuantifiersStatistics() -{ - 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); - smtStatisticsRegistry()->unregisterStat(&d_triggers); - smtStatisticsRegistry()->unregisterStat(&d_simple_triggers); - smtStatisticsRegistry()->unregisterStat(&d_multi_triggers); - smtStatisticsRegistry()->unregisterStat(&d_red_alpha_equiv); } } // namespace quantifiers diff --git a/src/theory/quantifiers/quantifiers_statistics.h b/src/theory/quantifiers/quantifiers_statistics.h index f03d27ee3..438efd30f 100644 --- a/src/theory/quantifiers/quantifiers_statistics.h +++ b/src/theory/quantifiers/quantifiers_statistics.h @@ -18,8 +18,7 @@ #ifndef CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_STATISTICS_H #define CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_STATISTICS_H -#include "util/statistics_registry.h" -#include "util/stats_timer.h" +#include "util/statistics_stats.h" namespace cvc5 { namespace theory { @@ -33,7 +32,6 @@ class QuantifiersStatistics { public: QuantifiersStatistics(); - ~QuantifiersStatistics(); TimerStat d_time; TimerStat d_qcf_time; TimerStat d_ematching_time; diff --git a/src/theory/quantifiers/sygus/sygus_stats.cpp b/src/theory/quantifiers/sygus/sygus_stats.cpp index 4fe0e9bbc..19d799eb3 100644 --- a/src/theory/quantifiers/sygus/sygus_stats.cpp +++ b/src/theory/quantifiers/sygus/sygus_stats.cpp @@ -22,40 +22,26 @@ namespace theory { namespace quantifiers { SygusStatistics::SygusStatistics() - : d_cegqi_lemmas_ce("SynthEngine::cegqi_lemmas_ce", 0), - d_cegqi_lemmas_refine("SynthEngine::cegqi_lemmas_refine", 0), - d_cegqi_si_lemmas("SynthEngine::cegqi_lemmas_si", 0), - d_solutions("SynthConjecture::solutions", 0), - d_filtered_solutions("SynthConjecture::filtered_solutions", 0), - d_candidate_rewrites_print("SynthConjecture::candidate_rewrites_print", - 0), - d_enumTermsRewrite("SygusEnumerator::enumTermsRewrite", 0), - d_enumTermsExampleEval("SygusEnumerator::enumTermsEvalExamples", 0), - d_enumTerms("SygusEnumerator::enumTerms", 0) + : d_cegqi_lemmas_ce( + smtStatisticsRegistry().registerInt("SynthEngine::cegqi_lemmas_ce")), + d_cegqi_lemmas_refine(smtStatisticsRegistry().registerInt( + "SynthEngine::cegqi_lemmas_refine")), + d_cegqi_si_lemmas( + smtStatisticsRegistry().registerInt("SynthEngine::cegqi_lemmas_si")), + d_solutions( + smtStatisticsRegistry().registerInt("SynthConjecture::solutions")), + d_filtered_solutions(smtStatisticsRegistry().registerInt( + "SynthConjecture::filtered_solutions")), + d_candidate_rewrites_print(smtStatisticsRegistry().registerInt( + "SynthConjecture::candidate_rewrites_print")), + d_enumTermsRewrite(smtStatisticsRegistry().registerInt( + "SygusEnumerator::enumTermsRewrite")), + d_enumTermsExampleEval(smtStatisticsRegistry().registerInt( + "SygusEnumerator::enumTermsEvalExamples")), + d_enumTerms( + smtStatisticsRegistry().registerInt("SygusEnumerator::enumTerms")) { - smtStatisticsRegistry()->registerStat(&d_cegqi_lemmas_ce); - smtStatisticsRegistry()->registerStat(&d_cegqi_lemmas_refine); - smtStatisticsRegistry()->registerStat(&d_cegqi_si_lemmas); - smtStatisticsRegistry()->registerStat(&d_solutions); - smtStatisticsRegistry()->registerStat(&d_filtered_solutions); - smtStatisticsRegistry()->registerStat(&d_candidate_rewrites_print); - smtStatisticsRegistry()->registerStat(&d_enumTermsRewrite); - smtStatisticsRegistry()->registerStat(&d_enumTermsExampleEval); - smtStatisticsRegistry()->registerStat(&d_enumTerms); -} - -SygusStatistics::~SygusStatistics() -{ - smtStatisticsRegistry()->unregisterStat(&d_cegqi_lemmas_ce); - smtStatisticsRegistry()->unregisterStat(&d_cegqi_lemmas_refine); - smtStatisticsRegistry()->unregisterStat(&d_cegqi_si_lemmas); - smtStatisticsRegistry()->unregisterStat(&d_solutions); - smtStatisticsRegistry()->unregisterStat(&d_filtered_solutions); - smtStatisticsRegistry()->unregisterStat(&d_candidate_rewrites_print); - smtStatisticsRegistry()->unregisterStat(&d_enumTermsRewrite); - smtStatisticsRegistry()->unregisterStat(&d_enumTermsExampleEval); - smtStatisticsRegistry()->unregisterStat(&d_enumTerms); } } // namespace quantifiers diff --git a/src/theory/quantifiers/sygus/sygus_stats.h b/src/theory/quantifiers/sygus/sygus_stats.h index 20b0633aa..6236547f9 100644 --- a/src/theory/quantifiers/sygus/sygus_stats.h +++ b/src/theory/quantifiers/sygus/sygus_stats.h @@ -18,7 +18,7 @@ #ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_STATS_H #define CVC5__THEORY__QUANTIFIERS__SYGUS_STATS_H -#include "util/statistics_registry.h" +#include "util/statistics_stats.h" namespace cvc5 { namespace theory { @@ -31,7 +31,6 @@ class SygusStatistics { public: SygusStatistics(); - ~SygusStatistics(); /** Number of counterexample lemmas */ IntStat d_cegqi_lemmas_ce; /** Number of refinement lemmas */ diff --git a/src/theory/quantifiers/term_tuple_enumerator.cpp b/src/theory/quantifiers/term_tuple_enumerator.cpp index 4b714419f..2f21a50e1 100644 --- a/src/theory/quantifiers/term_tuple_enumerator.cpp +++ b/src/theory/quantifiers/term_tuple_enumerator.cpp @@ -31,7 +31,7 @@ #include "theory/quantifiers/term_pools.h" #include "theory/quantifiers/term_registry.h" #include "theory/quantifiers/term_util.h" -#include "util/statistics_registry.h" +#include "util/statistics_stats.h" namespace cvc5 { |