summaryrefslogtreecommitdiff
path: root/src/smt/smt_engine.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/smt/smt_engine.cpp')
-rw-r--r--src/smt/smt_engine.cpp92
1 files changed, 46 insertions, 46 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 3571ae0cb..1999930d1 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -244,55 +244,55 @@ struct SmtEngineStatistics {
d_resourceUnitsUsed("smt::SmtEngine::resourceUnitsUsed")
{
- StatisticsRegistry::registerStat(&d_definitionExpansionTime);
- StatisticsRegistry::registerStat(&d_rewriteBooleanTermsTime);
- StatisticsRegistry::registerStat(&d_nonclausalSimplificationTime);
- StatisticsRegistry::registerStat(&d_miplibPassTime);
- StatisticsRegistry::registerStat(&d_numMiplibAssertionsRemoved);
- StatisticsRegistry::registerStat(&d_numConstantProps);
- StatisticsRegistry::registerStat(&d_staticLearningTime);
- StatisticsRegistry::registerStat(&d_simpITETime);
- StatisticsRegistry::registerStat(&d_unconstrainedSimpTime);
- StatisticsRegistry::registerStat(&d_iteRemovalTime);
- StatisticsRegistry::registerStat(&d_theoryPreprocessTime);
- StatisticsRegistry::registerStat(&d_rewriteApplyToConstTime);
- StatisticsRegistry::registerStat(&d_cnfConversionTime);
- StatisticsRegistry::registerStat(&d_numAssertionsPre);
- StatisticsRegistry::registerStat(&d_numAssertionsPost);
- StatisticsRegistry::registerStat(&d_checkModelTime);
- StatisticsRegistry::registerStat(&d_checkProofTime);
- StatisticsRegistry::registerStat(&d_checkUnsatCoreTime);
- StatisticsRegistry::registerStat(&d_solveTime);
- StatisticsRegistry::registerStat(&d_pushPopTime);
- StatisticsRegistry::registerStat(&d_processAssertionsTime);
- StatisticsRegistry::registerStat(&d_simplifiedToFalse);
- StatisticsRegistry::registerStat(&d_resourceUnitsUsed);
+ smtStatisticsRegistry()->registerStat(&d_definitionExpansionTime);
+ smtStatisticsRegistry()->registerStat(&d_rewriteBooleanTermsTime);
+ smtStatisticsRegistry()->registerStat(&d_nonclausalSimplificationTime);
+ smtStatisticsRegistry()->registerStat(&d_miplibPassTime);
+ smtStatisticsRegistry()->registerStat(&d_numMiplibAssertionsRemoved);
+ smtStatisticsRegistry()->registerStat(&d_numConstantProps);
+ smtStatisticsRegistry()->registerStat(&d_staticLearningTime);
+ smtStatisticsRegistry()->registerStat(&d_simpITETime);
+ smtStatisticsRegistry()->registerStat(&d_unconstrainedSimpTime);
+ smtStatisticsRegistry()->registerStat(&d_iteRemovalTime);
+ smtStatisticsRegistry()->registerStat(&d_theoryPreprocessTime);
+ smtStatisticsRegistry()->registerStat(&d_rewriteApplyToConstTime);
+ smtStatisticsRegistry()->registerStat(&d_cnfConversionTime);
+ smtStatisticsRegistry()->registerStat(&d_numAssertionsPre);
+ smtStatisticsRegistry()->registerStat(&d_numAssertionsPost);
+ smtStatisticsRegistry()->registerStat(&d_checkModelTime);
+ smtStatisticsRegistry()->registerStat(&d_checkProofTime);
+ smtStatisticsRegistry()->registerStat(&d_checkUnsatCoreTime);
+ smtStatisticsRegistry()->registerStat(&d_solveTime);
+ smtStatisticsRegistry()->registerStat(&d_pushPopTime);
+ smtStatisticsRegistry()->registerStat(&d_processAssertionsTime);
+ smtStatisticsRegistry()->registerStat(&d_simplifiedToFalse);
+ smtStatisticsRegistry()->registerStat(&d_resourceUnitsUsed);
}
~SmtEngineStatistics() {
- StatisticsRegistry::unregisterStat(&d_definitionExpansionTime);
- StatisticsRegistry::unregisterStat(&d_rewriteBooleanTermsTime);
- StatisticsRegistry::unregisterStat(&d_nonclausalSimplificationTime);
- StatisticsRegistry::unregisterStat(&d_miplibPassTime);
- StatisticsRegistry::unregisterStat(&d_numMiplibAssertionsRemoved);
- StatisticsRegistry::unregisterStat(&d_numConstantProps);
- StatisticsRegistry::unregisterStat(&d_staticLearningTime);
- StatisticsRegistry::unregisterStat(&d_simpITETime);
- StatisticsRegistry::unregisterStat(&d_unconstrainedSimpTime);
- StatisticsRegistry::unregisterStat(&d_iteRemovalTime);
- StatisticsRegistry::unregisterStat(&d_theoryPreprocessTime);
- StatisticsRegistry::unregisterStat(&d_rewriteApplyToConstTime);
- StatisticsRegistry::unregisterStat(&d_cnfConversionTime);
- StatisticsRegistry::unregisterStat(&d_numAssertionsPre);
- StatisticsRegistry::unregisterStat(&d_numAssertionsPost);
- StatisticsRegistry::unregisterStat(&d_checkModelTime);
- StatisticsRegistry::unregisterStat(&d_checkProofTime);
- StatisticsRegistry::unregisterStat(&d_checkUnsatCoreTime);
- StatisticsRegistry::unregisterStat(&d_solveTime);
- StatisticsRegistry::unregisterStat(&d_pushPopTime);
- StatisticsRegistry::unregisterStat(&d_processAssertionsTime);
- StatisticsRegistry::unregisterStat(&d_simplifiedToFalse);
- StatisticsRegistry::unregisterStat(&d_resourceUnitsUsed);
+ smtStatisticsRegistry()->unregisterStat(&d_definitionExpansionTime);
+ smtStatisticsRegistry()->unregisterStat(&d_rewriteBooleanTermsTime);
+ smtStatisticsRegistry()->unregisterStat(&d_nonclausalSimplificationTime);
+ smtStatisticsRegistry()->unregisterStat(&d_miplibPassTime);
+ smtStatisticsRegistry()->unregisterStat(&d_numMiplibAssertionsRemoved);
+ smtStatisticsRegistry()->unregisterStat(&d_numConstantProps);
+ smtStatisticsRegistry()->unregisterStat(&d_staticLearningTime);
+ smtStatisticsRegistry()->unregisterStat(&d_simpITETime);
+ smtStatisticsRegistry()->unregisterStat(&d_unconstrainedSimpTime);
+ smtStatisticsRegistry()->unregisterStat(&d_iteRemovalTime);
+ smtStatisticsRegistry()->unregisterStat(&d_theoryPreprocessTime);
+ smtStatisticsRegistry()->unregisterStat(&d_rewriteApplyToConstTime);
+ smtStatisticsRegistry()->unregisterStat(&d_cnfConversionTime);
+ smtStatisticsRegistry()->unregisterStat(&d_numAssertionsPre);
+ smtStatisticsRegistry()->unregisterStat(&d_numAssertionsPost);
+ smtStatisticsRegistry()->unregisterStat(&d_checkModelTime);
+ smtStatisticsRegistry()->unregisterStat(&d_checkProofTime);
+ smtStatisticsRegistry()->unregisterStat(&d_checkUnsatCoreTime);
+ smtStatisticsRegistry()->unregisterStat(&d_solveTime);
+ smtStatisticsRegistry()->unregisterStat(&d_pushPopTime);
+ smtStatisticsRegistry()->unregisterStat(&d_processAssertionsTime);
+ smtStatisticsRegistry()->unregisterStat(&d_simplifiedToFalse);
+ smtStatisticsRegistry()->unregisterStat(&d_resourceUnitsUsed);
}
};/* struct SmtEngineStatistics */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback