diff options
Diffstat (limited to 'src/theory/quantifiers')
-rw-r--r-- | src/theory/quantifiers/ce_guided_instantiation.cpp | 13 | ||||
-rw-r--r-- | src/theory/quantifiers/ceg_instantiator.h | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/inst_strategy_cbqi.h | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/inst_strategy_e_matching.h | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/model_builder.cpp | 32 | ||||
-rw-r--r-- | src/theory/quantifiers/model_engine.cpp | 12 | ||||
-rw-r--r-- | src/theory/quantifiers/quant_conflict_find.cpp | 17 | ||||
-rw-r--r-- | src/theory/quantifiers/theory_quantifiers.h | 2 |
8 files changed, 42 insertions, 40 deletions
diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp index 81fe00674..cc0b18ffe 100644 --- a/src/theory/quantifiers/ce_guided_instantiation.cpp +++ b/src/theory/quantifiers/ce_guided_instantiation.cpp @@ -16,6 +16,7 @@ #include "expr/datatype.h" #include "options/quantifiers_options.h" +#include "smt/smt_statistics_registry.h" #include "theory/datatypes/datatypes_rewriter.h" #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/term_database.h" @@ -696,15 +697,15 @@ CegInstantiation::Statistics::Statistics(): d_cegqi_lemmas_refine("CegInstantiation::cegqi_lemmas_refine", 0), d_cegqi_si_lemmas("CegInstantiation::cegqi_lemmas_si", 0) { - StatisticsRegistry::registerStat(&d_cegqi_lemmas_ce); - StatisticsRegistry::registerStat(&d_cegqi_lemmas_refine); - StatisticsRegistry::registerStat(&d_cegqi_si_lemmas); + smtStatisticsRegistry()->registerStat(&d_cegqi_lemmas_ce); + smtStatisticsRegistry()->registerStat(&d_cegqi_lemmas_refine); + smtStatisticsRegistry()->registerStat(&d_cegqi_si_lemmas); } CegInstantiation::Statistics::~Statistics(){ - StatisticsRegistry::unregisterStat(&d_cegqi_lemmas_ce); - StatisticsRegistry::unregisterStat(&d_cegqi_lemmas_refine); - StatisticsRegistry::unregisterStat(&d_cegqi_si_lemmas); + smtStatisticsRegistry()->unregisterStat(&d_cegqi_lemmas_ce); + smtStatisticsRegistry()->unregisterStat(&d_cegqi_lemmas_refine); + smtStatisticsRegistry()->unregisterStat(&d_cegqi_si_lemmas); } diff --git a/src/theory/quantifiers/ceg_instantiator.h b/src/theory/quantifiers/ceg_instantiator.h index 5b3c5263f..9504bd407 100644 --- a/src/theory/quantifiers/ceg_instantiator.h +++ b/src/theory/quantifiers/ceg_instantiator.h @@ -18,8 +18,8 @@ #ifndef __CVC4__CEG_INSTANTIATOR_H #define __CVC4__CEG_INSTANTIATOR_H -#include "expr/statistics_registry.h" #include "theory/quantifiers_engine.h" +#include "util/statistics_registry.h" namespace CVC4 { namespace theory { diff --git a/src/theory/quantifiers/inst_strategy_cbqi.h b/src/theory/quantifiers/inst_strategy_cbqi.h index 2105007e2..5511af209 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.h +++ b/src/theory/quantifiers/inst_strategy_cbqi.h @@ -18,10 +18,10 @@ #ifndef __CVC4__INST_STRATEGY_CBQI_H #define __CVC4__INST_STRATEGY_CBQI_H -#include "expr/statistics_registry.h" #include "theory/arith/arithvar.h" #include "theory/quantifiers/ceg_instantiator.h" #include "theory/quantifiers/instantiation_engine.h" +#include "util/statistics_registry.h" namespace CVC4 { namespace theory { diff --git a/src/theory/quantifiers/inst_strategy_e_matching.h b/src/theory/quantifiers/inst_strategy_e_matching.h index a19bcca76..4e7afad5d 100644 --- a/src/theory/quantifiers/inst_strategy_e_matching.h +++ b/src/theory/quantifiers/inst_strategy_e_matching.h @@ -19,10 +19,10 @@ #include "context/context.h" #include "context/context_mm.h" -#include "expr/statistics_registry.h" #include "theory/quantifiers/instantiation_engine.h" #include "theory/quantifiers/trigger.h" #include "theory/quantifiers_engine.h" +#include "util/statistics_registry.h" namespace CVC4 { namespace theory { diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp index dc18548a5..95b674cca 100644 --- a/src/theory/quantifiers/model_builder.cpp +++ b/src/theory/quantifiers/model_builder.cpp @@ -352,25 +352,25 @@ QModelBuilderIG::Statistics::Statistics(): d_eval_lits("QModelBuilderIG::Eval_Lits", 0 ), d_eval_lits_unknown("QModelBuilderIG::Eval_Lits_Unknown", 0 ) { - StatisticsRegistry::registerStat(&d_num_quants_init); - StatisticsRegistry::registerStat(&d_num_partial_quants_init); - StatisticsRegistry::registerStat(&d_init_inst_gen_lemmas); - StatisticsRegistry::registerStat(&d_inst_gen_lemmas); - StatisticsRegistry::registerStat(&d_eval_formulas); - StatisticsRegistry::registerStat(&d_eval_uf_terms); - StatisticsRegistry::registerStat(&d_eval_lits); - StatisticsRegistry::registerStat(&d_eval_lits_unknown); + smtStatisticsRegistry()->registerStat(&d_num_quants_init); + smtStatisticsRegistry()->registerStat(&d_num_partial_quants_init); + smtStatisticsRegistry()->registerStat(&d_init_inst_gen_lemmas); + smtStatisticsRegistry()->registerStat(&d_inst_gen_lemmas); + smtStatisticsRegistry()->registerStat(&d_eval_formulas); + smtStatisticsRegistry()->registerStat(&d_eval_uf_terms); + smtStatisticsRegistry()->registerStat(&d_eval_lits); + smtStatisticsRegistry()->registerStat(&d_eval_lits_unknown); } QModelBuilderIG::Statistics::~Statistics(){ - StatisticsRegistry::unregisterStat(&d_num_quants_init); - StatisticsRegistry::unregisterStat(&d_num_partial_quants_init); - StatisticsRegistry::unregisterStat(&d_init_inst_gen_lemmas); - StatisticsRegistry::unregisterStat(&d_inst_gen_lemmas); - StatisticsRegistry::unregisterStat(&d_eval_formulas); - StatisticsRegistry::unregisterStat(&d_eval_uf_terms); - StatisticsRegistry::unregisterStat(&d_eval_lits); - StatisticsRegistry::unregisterStat(&d_eval_lits_unknown); + smtStatisticsRegistry()->unregisterStat(&d_num_quants_init); + smtStatisticsRegistry()->unregisterStat(&d_num_partial_quants_init); + smtStatisticsRegistry()->unregisterStat(&d_init_inst_gen_lemmas); + smtStatisticsRegistry()->unregisterStat(&d_inst_gen_lemmas); + smtStatisticsRegistry()->unregisterStat(&d_eval_formulas); + smtStatisticsRegistry()->unregisterStat(&d_eval_uf_terms); + smtStatisticsRegistry()->unregisterStat(&d_eval_lits); + smtStatisticsRegistry()->unregisterStat(&d_eval_lits_unknown); } bool QModelBuilderIG::isQuantifierActive( Node f ){ diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp index 6a21a50e5..eb827edc3 100644 --- a/src/theory/quantifiers/model_engine.cpp +++ b/src/theory/quantifiers/model_engine.cpp @@ -326,13 +326,13 @@ ModelEngine::Statistics::Statistics(): d_exh_inst_lemmas("ModelEngine::Instantiations_Exhaustive", 0 ), d_mbqi_inst_lemmas("ModelEngine::Instantiations_Mbqi", 0 ) { - StatisticsRegistry::registerStat(&d_inst_rounds); - StatisticsRegistry::registerStat(&d_exh_inst_lemmas); - StatisticsRegistry::registerStat(&d_mbqi_inst_lemmas); + smtStatisticsRegistry()->registerStat(&d_inst_rounds); + smtStatisticsRegistry()->registerStat(&d_exh_inst_lemmas); + smtStatisticsRegistry()->registerStat(&d_mbqi_inst_lemmas); } ModelEngine::Statistics::~Statistics(){ - StatisticsRegistry::unregisterStat(&d_inst_rounds); - StatisticsRegistry::unregisterStat(&d_exh_inst_lemmas); - StatisticsRegistry::unregisterStat(&d_mbqi_inst_lemmas); + smtStatisticsRegistry()->unregisterStat(&d_inst_rounds); + smtStatisticsRegistry()->unregisterStat(&d_exh_inst_lemmas); + smtStatisticsRegistry()->unregisterStat(&d_mbqi_inst_lemmas); } diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index b6256980a..a890276f7 100644 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -18,6 +18,7 @@ #include <vector> #include "options/quantifiers_options.h" +#include "smt/smt_statistics_registry.h" #include "theory/quantifiers/quant_util.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/trigger.h" @@ -2227,17 +2228,17 @@ QuantConflictFind::Statistics::Statistics(): d_prop_inst("QuantConflictFind::Instantiations_Prop", 0 ), d_entailment_checks("QuantConflictFind::Entailment_Checks",0) { - StatisticsRegistry::registerStat(&d_inst_rounds); - StatisticsRegistry::registerStat(&d_conflict_inst); - StatisticsRegistry::registerStat(&d_prop_inst); - StatisticsRegistry::registerStat(&d_entailment_checks); + smtStatisticsRegistry()->registerStat(&d_inst_rounds); + smtStatisticsRegistry()->registerStat(&d_conflict_inst); + smtStatisticsRegistry()->registerStat(&d_prop_inst); + smtStatisticsRegistry()->registerStat(&d_entailment_checks); } QuantConflictFind::Statistics::~Statistics(){ - StatisticsRegistry::unregisterStat(&d_inst_rounds); - StatisticsRegistry::unregisterStat(&d_conflict_inst); - StatisticsRegistry::unregisterStat(&d_prop_inst); - StatisticsRegistry::unregisterStat(&d_entailment_checks); + smtStatisticsRegistry()->unregisterStat(&d_inst_rounds); + smtStatisticsRegistry()->unregisterStat(&d_conflict_inst); + smtStatisticsRegistry()->unregisterStat(&d_prop_inst); + smtStatisticsRegistry()->unregisterStat(&d_entailment_checks); } TNode QuantConflictFind::getZero( Kind k ) { diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h index f24c10fc0..63f3379b8 100644 --- a/src/theory/quantifiers/theory_quantifiers.h +++ b/src/theory/quantifiers/theory_quantifiers.h @@ -24,9 +24,9 @@ #include <map> #include "context/cdhashmap.h" -#include "expr/statistics_registry.h" #include "theory/theory.h" #include "util/hash.h" +#include "util/statistics_registry.h" namespace CVC4 { class TheoryEngine; |