summaryrefslogtreecommitdiff
path: root/src/smt
diff options
context:
space:
mode:
Diffstat (limited to 'src/smt')
-rw-r--r--src/smt/smt_engine.cpp92
-rw-r--r--src/smt/smt_engine.h2
-rw-r--r--src/smt/smt_engine_check_proof.cpp2
-rw-r--r--src/smt/smt_engine_scope.h11
-rw-r--r--src/smt/smt_statistics_registry.cpp29
-rw-r--r--src/smt/smt_statistics_registry.h61
6 files changed, 149 insertions, 48 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 */
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 531b499ac..2f222790c 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -28,7 +28,6 @@
#include "context/cdlist_forward.h"
#include "expr/expr.h"
#include "expr/expr_manager.h"
-#include "expr/statistics.h"
#include "options/options.h"
#include "proof/unsat_core.h"
#include "smt/logic_exception.h"
@@ -38,6 +37,7 @@
#include "util/proof.h"
#include "util/result.h"
#include "util/sexpr.h"
+#include "util/statistics.h"
#include "util/unsafe_interrupt_exception.h"
// In terms of abstraction, this is below (and provides services to)
diff --git a/src/smt/smt_engine_check_proof.cpp b/src/smt/smt_engine_check_proof.cpp
index da01b9863..c4747d724 100644
--- a/src/smt/smt_engine_check_proof.cpp
+++ b/src/smt/smt_engine_check_proof.cpp
@@ -27,9 +27,9 @@
#include "base/cvc4_assert.h"
#include "base/output.h"
-#include "expr/statistics_registry.h"
#include "smt/smt_engine.h"
#include "util/configuration_private.h"
+#include "util/statistics_registry.h"
using namespace CVC4;
using namespace std;
diff --git a/src/smt/smt_engine_scope.h b/src/smt/smt_engine_scope.h
index 1dd69abc9..83da5a159 100644
--- a/src/smt/smt_engine_scope.h
+++ b/src/smt/smt_engine_scope.h
@@ -73,7 +73,18 @@ public:
s_smtEngine_current = d_oldSmtEngine;
Debug("current") << "smt scope: returning to " << s_smtEngine_current << std::endl;
}
+
+ /**
+ * This returns the StatisticsRegistry attached to the currently in scope
+ * SmtEngine.
+ */
+ static StatisticsRegistry* currentStatisticsRegistry() {
+ Assert(smtEngineInScope());
+ return s_smtEngine_current->d_statisticsRegistry;
+ }
+
};/* class SmtScope */
+
}/* CVC4::smt namespace */
}/* CVC4 namespace */
diff --git a/src/smt/smt_statistics_registry.cpp b/src/smt/smt_statistics_registry.cpp
new file mode 100644
index 000000000..5aa9085f5
--- /dev/null
+++ b/src/smt/smt_statistics_registry.cpp
@@ -0,0 +1,29 @@
+/********************* */
+/*! \file smt_statistic_registry.cpp
+ ** \verbatim
+ ** Original author: Tim King
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2016 New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Accessor for the SmtEngine's StatisticsRegistry.
+ **
+ ** Accessor for the SmtEngine's StatisticsRegistry.
+ **/
+
+
+#include "smt/smt_statistics_registry.h"
+
+#include "smt/smt_engine_scope.h"
+#include "util/statistics_registry.h"
+
+namespace CVC4 {
+
+StatisticsRegistry* smtStatisticsRegistry() {
+ return smt::SmtScope::currentStatisticsRegistry();
+}
+
+}/* CVC4 namespace */
diff --git a/src/smt/smt_statistics_registry.h b/src/smt/smt_statistics_registry.h
new file mode 100644
index 000000000..60a5e7c53
--- /dev/null
+++ b/src/smt/smt_statistics_registry.h
@@ -0,0 +1,61 @@
+/********************* */
+/*! \file smt_statistic_registry.h
+ ** \verbatim
+ ** Original author: Tim King
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2016 New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Accessor for the SmtEngine's StatisticsRegistry.
+ **
+ ** Accessor for the SmtEngine's StatisticsRegistry.
+ **/
+
+#include "cvc4_private.h"
+
+#pragma once
+
+#include "util/statistics_registry.h"
+
+namespace CVC4 {
+
+/**
+ * This returns the StatisticsRegistry attached to the currently in scope
+ * SmtEngine. This is a synonym for smt::SmtScope::currentStatisticsRegistry().
+ */
+StatisticsRegistry* smtStatisticsRegistry();
+
+
+/**
+ * To use a statistic, you need to declare it, initialize it in your
+ * constructor, register it in your constructor, and deregister it in
+ * your destructor. Instead, this macro does it all for you (and
+ * therefore also keeps the statistic type, field name, and output
+ * string all in the same place in your class's header. Its use is
+ * like in this example, which takes the place of the declaration of a
+ * statistics field "d_checkTimer":
+ *
+ * KEEP_STATISTIC(TimerStat, d_checkTimer, "theory::uf::checkTime");
+ *
+ * If any args need to be passed to the constructor, you can specify
+ * them after the string.
+ *
+ * The macro works by creating a nested class type, derived from the
+ * statistic type you give it, which declares a registry-aware
+ * constructor/destructor pair.
+ */
+#define KEEP_STATISTIC(_StatType, _StatField, _StatName, _CtorArgs...) \
+ struct Statistic_##_StatField : public _StatType { \
+ Statistic_##_StatField() : _StatType(_StatName, ## _CtorArgs) { \
+ smtStatisticsRegistry()->registerStat(this); \
+ } \
+ ~Statistic_##_StatField() { \
+ smtStatisticsRegistry()->unregisterStat(this); \
+ } \
+ } _StatField
+
+
+}/* CVC4 namespace */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback