summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers')
-rw-r--r--src/theory/quantifiers/cegqi/ceg_instantiator.h2
-rw-r--r--src/theory/quantifiers/cegqi/inst_strategy_cegqi.h2
-rw-r--r--src/theory/quantifiers/instantiate.cpp24
-rw-r--r--src/theory/quantifiers/instantiate.h3
-rw-r--r--src/theory/quantifiers/quant_conflict_find.cpp15
-rw-r--r--src/theory/quantifiers/quant_conflict_find.h1
-rw-r--r--src/theory/quantifiers/quantifiers_inference_manager.cpp2
-rw-r--r--src/theory/quantifiers/quantifiers_statistics.cpp55
-rw-r--r--src/theory/quantifiers/quantifiers_statistics.h4
-rw-r--r--src/theory/quantifiers/sygus/sygus_stats.cpp50
-rw-r--r--src/theory/quantifiers/sygus/sygus_stats.h3
-rw-r--r--src/theory/quantifiers/term_tuple_enumerator.cpp2
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 {
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback