From: Morgan Deters Date: Sat, 22 Sep 2012 21:10:51 +0000 (+0000) Subject: Separate public-facing and internal-facing interfaces to Statistics. X-Git-Tag: cvc5-1.0.0~7791 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e2611a54c5479086df0c4a80f56597aae80b5c4e;p=cvc5.git Separate public-facing and internal-facing interfaces to Statistics. The external interface (e.g., what's answered by ExprManager::getStatistics() and SmtEngine::getStatistics()) is a snapshot of the current statistics (rather than a reference to the actual StatisticsRegistry). The StatisticsRegistry is now internal-only. However, it's built as a convenience library so that the parser and driver can use it too (by re-linking against it). This is part of the ongoing effort to clean up the public interface. (this commit was certified error- and warning-free by the test-and-commit script.) --- diff --git a/AUTHORS b/AUTHORS index c99aa6395..19eac8dce 100644 --- a/AUTHORS +++ b/AUTHORS @@ -2,12 +2,10 @@ The core authors and designers of CVC4 are: Kshitij Bansal , New York University Clark Barrett , New York University - François Bobot , Paris-Sud University + Francois Bobot , Paris-Sud University Christopher Conway , New York University Morgan Deters , New York University - Yeting Ge , New York University Liana Hadarean , New York University - Mina Jeong , New York University Dejan Jovanovic , New York University Tim King , New York University Andrew Reynolds , University of Iowa diff --git a/README b/README index 37c285639..65c2d6fec 100644 --- a/README +++ b/README @@ -2,13 +2,14 @@ This is a prerelease version of CVC4. *** Quick-start instructions -To build, you'll need reasonably new automake, autoconf, and libtool -installed (see below). Execute, - - ./autogen.sh ./configure make +(To build from a Subversion checkout, you'll need reasonably new +automake, autoconf, and libtool installed (see below). The +"configure" script isn't in the repository, so run "./autogen.sh" +first to produce it. Then proceed as above.) + You can then "make install" to install in the prefix you gave to the configure script (/usr/local by default). ** You should run "make check" ** before installation to ensure that CVC4 has been @@ -20,14 +21,14 @@ easily detects this problem (by showing a number of FAILed test cases). It is ok if the unit tests aren't run as part of "make check", but all system tests and regression tests should pass without incident. +To build API documentation, use "make doc". Documentation is produced +under doc/ but is not installed by "make install". + To build a source release, use "make dist"; this will include the configure script and all the bits of automake/autoconf/libtool that are necessary for an independent install. You'll find the resulting tarball in builds/cvc4-${VERSION}.tar.gz. -To build documentation, use "make doc". Documentation is produced -under doc/ but is not installed by "make install". - *** Dependencies The following tools and libraries are required to run CVC4. Versions @@ -37,7 +38,17 @@ GNU C and C++ (gcc and g++), reasonably recent versions GNU Make GNU Bash GMP v4.2 (GNU Multi-Precision arithmetic library) -libantlr3c v3.2 (ANTLR parser generator) +libantlr3c v3.2 or v3.4 (ANTLR parser generator) +The Boost C++ base libraries + +For libantlr3c, you can use the convenience script in +contrib/get-antlr-3.4 --this will download, patch, and install +libantlr3c. On a 32-bit machine, or if you have difficulty +building libantlr3c (or difficulty getting CVC4 to link against +it later), you may need to remove the --enable-64bit part in the +script. (If you're curious, the manual instructions are at +http://church.cims.nyu.edu/wiki/Developer%27s_Guide#ANTLR3 .) + Optional: CLN v1.3 (Class Library for Numbers) Optional: CUDD v2.4.2 (Colorado University Decision Diagram package) Optional: GNU Readline library (for an improved interactive experience) @@ -80,7 +91,7 @@ includes a diff of all changes made to cudd makefiles. *** Build dependencies The following tools and libraries are required to build CVC4 from -scratch. +scratch (i.e., from the repository rather than from a source tarball). Automake v1.11 Autoconf v2.61 diff --git a/src/Makefile.am b/src/Makefile.am index 232d8dd94..190a1b1bf 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -67,6 +67,7 @@ CLEANFILES = \ svninfo EXTRA_DIST = \ + include/cvc4_private_library.h \ include/cvc4parser_private.h \ include/cvc4parser_public.h \ include/cvc4_private.h \ diff --git a/src/compat/cvc3_compat.cpp b/src/compat/cvc3_compat.cpp index 4e884a9ab..2c5bc0170 100644 --- a/src/compat/cvc3_compat.cpp +++ b/src/compat/cvc3_compat.cpp @@ -2335,12 +2335,12 @@ void ValidityChecker::loadFile(std::istream& is, delete p; } -Statistics& ValidityChecker::getStatistics() { - return *d_smt->getStatisticsRegistry(); +Statistics ValidityChecker::getStatistics() { + return d_smt->getStatistics(); } void ValidityChecker::printStatistics() { - Message() << d_smt->getStatisticsRegistry(); + d_smt->getStatistics().flushInformation(Message.getStream()); } int compare(const Expr& e1, const Expr& e2) { diff --git a/src/compat/cvc3_compat.h b/src/compat/cvc3_compat.h index 39f6658ad..c140d2994 100644 --- a/src/compat/cvc3_compat.h +++ b/src/compat/cvc3_compat.h @@ -469,7 +469,7 @@ public: InputLanguage getOutputLang() const; };/* class CVC3::ExprManager */ -typedef CVC4::StatisticsRegistry Statistics; +typedef CVC4::Statistics Statistics; #define PRESENTATION_LANG ::CVC4::language::input::LANG_CVC4 #define SMTLIB_LANG ::CVC4::language::input::LANG_SMTLIB @@ -1553,7 +1553,7 @@ public: /***************************************************************************/ //! Get statistics object - virtual Statistics& getStatistics(); + virtual Statistics getStatistics(); //! Print collected statistics to stdout virtual void printStatistics(); diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp index 03f3a04b0..18b7bff0f 100644 --- a/src/expr/expr_manager_template.cpp +++ b/src/expr/expr_manager_template.cpp @@ -21,7 +21,7 @@ #include "expr/variable_type_map.h" #include "context/context.h" #include "options/options.h" -#include "util/stats.h" +#include "util/statistics_registry.h" #include @@ -906,8 +906,12 @@ Context* ExprManager::getContext() const { return d_ctxt; } -StatisticsRegistry* ExprManager::getStatisticsRegistry() const throw() { - return d_nodeManager->getStatisticsRegistry(); +Statistics ExprManager::getStatistics() const throw() { + return Statistics(*d_nodeManager->getStatisticsRegistry()); +} + +SExpr ExprManager::getStatistic(const std::string& name) const throw() { + return d_nodeManager->getStatisticsRegistry()->getStatistic(name); } namespace expr { diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h index 8e0f23c6a..8c964a5eb 100644 --- a/src/expr/expr_manager_template.h +++ b/src/expr/expr_manager_template.h @@ -27,7 +27,8 @@ #include "expr/type.h" #include "expr/expr.h" #include "util/subrange_bound.h" -#include "util/stats.h" +#include "util/statistics.h" +#include "util/sexpr.h" ${includes} @@ -35,7 +36,7 @@ ${includes} // compiler directs the user to the template file instead of the // generated one. We don't want the user to modify the generated one, // since it'll get overwritten on a later build. -#line 39 "${template}" +#line 40 "${template}" namespace CVC4 { @@ -454,7 +455,10 @@ public: Expr mkBoundVar(Type type); /** Get a reference to the statistics registry for this ExprManager */ - StatisticsRegistry* getStatisticsRegistry() const throw(); + Statistics getStatistics() const throw(); + + /** Get a reference to the statistics registry for this ExprManager */ + SExpr getStatistic(const std::string& name) const throw(); /** Export an expr to a different ExprManager */ //static Expr exportExpr(const Expr& e, ExprManager* em); diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index 82242cb1c..a66933470 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -22,7 +22,7 @@ #include "util/Assert.h" #include "options/options.h" -#include "util/stats.h" +#include "util/statistics_registry.h" #include "util/tls.h" #include "expr/type_checker.h" diff --git a/src/include/cvc4_private.h b/src/include/cvc4_private.h index 11d4a2ea9..c97398e1e 100644 --- a/src/include/cvc4_private.h +++ b/src/include/cvc4_private.h @@ -12,7 +12,7 @@ ** information.\endverbatim ** ** \brief #-inclusion of this file marks a header as private and generates a - ** warning when the file is included improperly. + ** warning when the file is included improperly ** ** #-inclusion of this file marks a header as private and generates a ** warning when the file is included improperly. diff --git a/src/include/cvc4_private_library.h b/src/include/cvc4_private_library.h new file mode 100644 index 000000000..b0aff2c64 --- /dev/null +++ b/src/include/cvc4_private_library.h @@ -0,0 +1,31 @@ +/********************* */ +/*! \file cvc4_private_library.h + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009-2012 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief #-inclusion of this file marks a header as private and generates a + ** warning when the file is included improperly + ** + ** #-inclusion of this file marks a header as private and generates a + ** warning when the file is included improperly. + **/ + +#ifndef __CVC4_PRIVATE_LIBRARY_H +#define __CVC4_PRIVATE_LIBRARY_H + +#if ! (defined(__BUILDING_CVC4LIB) || defined(__BUILDING_CVC4LIB_UNIT_TEST) || defined(__BUILDING_CVC4PARSERLIB) || defined(__BUILDING_CVC4PARSERLIB_UNIT_TEST) || defined(__BUILDING_CVC4DRIVER)) +# warning A "private library" CVC4 header was included when not building the library, driver, or private unit test code. +#endif /* ! (__BUILDING_CVC4LIB || __BUILDING_CVC4LIB_UNIT_TEST || __BUILDING_CVC4PARSERLIB || __BUILDING_CVC4PARSERLIB_UNIT_TEST || __BUILDING_CVC4DRIVER) */ + +#include "cvc4_public.h" +#include "cvc4autoconfig.h" + +#endif /* __CVC4_PRIVATE_LIBRARY_H */ diff --git a/src/main/Makefile.am b/src/main/Makefile.am index 4524929d4..aa63846cf 100644 --- a/src/main/Makefile.am +++ b/src/main/Makefile.am @@ -30,6 +30,7 @@ pcvc4_LDADD = \ libmain.a \ @builddir@/../parser/libcvc4parser.la \ @builddir@/../libcvc4.la \ + @builddir@/../util/libstatistics.la \ @builddir@/../lib/libreplacements.la \ $(READLINE_LIBS) pcvc4_CPPFLAGS = $(AM_CPPFLAGS) $(BOOST_CPPFLAGS) -DPORTFOLIO_BUILD @@ -51,6 +52,7 @@ cvc4_LDADD = \ libmain.a \ @builddir@/../parser/libcvc4parser.la \ @builddir@/../libcvc4.la \ + @builddir@/../util/libstatistics.la \ @builddir@/../lib/libreplacements.la \ $(READLINE_LIBS) diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp index 1bffd5e35..d283b2743 100644 --- a/src/main/command_executor.cpp +++ b/src/main/command_executor.cpp @@ -24,16 +24,11 @@ namespace CVC4 { namespace main { - CommandExecutor::CommandExecutor(ExprManager &exprMgr, Options &options): d_exprMgr(exprMgr), d_smtEngine(SmtEngine(&exprMgr)), - d_options(options) { - - // signal handlers need access - main::pStatistics = d_smtEngine.getStatisticsRegistry(); - d_exprMgr.getStatisticsRegistry()->setName("ExprManager"); - main::pStatistics->registerStat_(d_exprMgr.getStatisticsRegistry()); + d_options(options), + d_stats("driver") { } bool CommandExecutor::doCommand(Command* cmd) @@ -89,5 +84,5 @@ bool smtEngineInvoke(SmtEngine* smt, Command* cmd, std::ostream *out) return !cmd->fail(); } -}/*main namespace*/ -}/*CVC4 namespace*/ +}/* CVC4::main namespace */ +}/* CVC4 namespace */ diff --git a/src/main/command_executor.h b/src/main/command_executor.h index 273225e69..435299ce3 100644 --- a/src/main/command_executor.h +++ b/src/main/command_executor.h @@ -19,6 +19,12 @@ #include "expr/expr_manager.h" #include "smt/smt_engine.h" +#include "util/statistics_registry.h" +#include "options/options.h" +#include "expr/command.h" + +#include +#include namespace CVC4 { namespace main { @@ -29,6 +35,7 @@ protected: ExprManager& d_exprMgr; SmtEngine d_smtEngine; Options& d_options; + StatisticsRegistry d_stats; public: // Note: though the options are not cached (instead a reference is @@ -48,6 +55,16 @@ public: virtual std::string getSmtEngineStatus(); + StatisticsRegistry& getStatisticsRegistry() { + return d_stats; + } + + virtual void flushStatistics(std::ostream& out) const { + d_exprMgr.getStatistics().flushInformation(out); + d_smtEngine.getStatistics().flushInformation(out); + d_stats.flushInformation(out); + } + protected: /** Executes treating cmd as a singleton */ virtual bool doCommandSingleton(CVC4::Command* cmd); diff --git a/src/main/command_executor_portfolio.cpp b/src/main/command_executor_portfolio.cpp index 045cac8f1..32a507d78 100644 --- a/src/main/command_executor_portfolio.cpp +++ b/src/main/command_executor_portfolio.cpp @@ -21,6 +21,7 @@ #include #include #include +#include #include "expr/command.h" #include "expr/pickler.h" @@ -63,26 +64,10 @@ CommandExecutorPortfolio::CommandExecutorPortfolio d_smts.push_back(new SmtEngine(d_exprMgrs[i])); } - for(unsigned i = 1; i < d_numThreads; ++i) { - // Register the statistics registry of the thread - string emTag = "ExprManager thread #" - + boost::lexical_cast(d_threadOptions[i][options::thread_id]); - string smtTag = "SmtEngine thread #" - + boost::lexical_cast(d_threadOptions[i][options::thread_id]); - d_exprMgrs[i]->getStatisticsRegistry()->setName(emTag); - d_smts[i]->getStatisticsRegistry()->setName(smtTag); - pStatistics->registerStat_ - (d_exprMgrs[i]->getStatisticsRegistry() ); - pStatistics->registerStat_ - (d_smts[i]->getStatisticsRegistry() ); - } - Assert(d_vmaps.size() == 0); for(unsigned i = 0; i < d_numThreads; ++i) { d_vmaps.push_back(new ExprManagerMapCollection()); } - - } CommandExecutorPortfolio::~CommandExecutorPortfolio() @@ -116,7 +101,7 @@ void CommandExecutorPortfolio::lemmaSharingInit() for(unsigned i = 0; i < d_numThreads; ++i){ if(Debug.isOn("channel-empty")) { - d_channelsOut.push_back + d_channelsOut.push_back (new EmptySharedChannel(sharingChannelSize)); d_channelsIn.push_back (new EmptySharedChannel(sharingChannelSize)); @@ -143,7 +128,7 @@ void CommandExecutorPortfolio::lemmaSharingInit() } /* Output to string stream */ - if(d_options[options::verbosity] == 0 + if(d_options[options::verbosity] == 0 || d_options[options::separateOutput]) { Assert(d_ostringstreams.size() == 0); for(unsigned i = 0; i < d_numThreads; ++i) { @@ -152,7 +137,7 @@ void CommandExecutorPortfolio::lemmaSharingInit() } } } -} +}/* CommandExecutorPortfolio::lemmaSharingInit() */ void CommandExecutorPortfolio::lemmaSharingCleanup() { @@ -180,7 +165,8 @@ void CommandExecutorPortfolio::lemmaSharingCleanup() d_ostringstreams.clear(); } -} +}/* CommandExecutorPortfolio::lemmaSharingCleanup() */ + bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd) { @@ -200,7 +186,7 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd) // } else if(dynamic_cast(cmd) != NULL) { // mode = 2; // } - + if(mode == 0) { d_seq->addCommand(cmd->clone()); return CommandExecutor::doCommandSingleton(cmd); @@ -290,7 +276,7 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd) *d_options[options::out] << d_ostringstreams[portfolioReturn.first]->str(); } - + /* cleanup this check sat specific stuff */ lemmaSharingCleanup(); @@ -303,12 +289,30 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd) Unreachable(); } -} +}/* CommandExecutorPortfolio::doCommandSingleton() */ std::string CommandExecutorPortfolio::getSmtEngineStatus() { return d_smts[d_lastWinner]->getInfo("status").getValue(); } -}/*main namespace*/ -}/*CVC4 namespace*/ +void CommandExecutorPortfolio::flushStatistics(std::ostream& out) const { + Assert(d_numThreads == d_exprMgrs.size() && d_exprMgrs.size() == d_smts.size()); + for(size_t i = 0; i < d_numThreads; ++i) { + string emTag = "ExprManager thread #" + + boost::lexical_cast(d_threadOptions[i][options::thread_id]); + Statistics stats = d_exprMgrs[i]->getStatistics(); + stats.setPrefix(emTag); + stats.flushInformation(out); + + string smtTag = "SmtEngine thread #" + + boost::lexical_cast(d_threadOptions[i][options::thread_id]); + stats = d_smts[i]->getStatistics(); + stats.setPrefix(smtTag); + stats.flushInformation(out); + } + d_stats.flushInformation(out); +} + +}/* CVC4::main namespace */ +}/* CVC4 namespace */ diff --git a/src/main/command_executor_portfolio.h b/src/main/command_executor_portfolio.h index cc0a77698..72a677789 100644 --- a/src/main/command_executor_portfolio.h +++ b/src/main/command_executor_portfolio.h @@ -23,6 +23,11 @@ #include "main/command_executor.h" #include "main/portfolio_util.h" +#include +#include +#include +#include + namespace CVC4 { class CommandSequence; @@ -55,6 +60,9 @@ public: ~CommandExecutorPortfolio(); std::string getSmtEngineStatus(); + + void flushStatistics(std::ostream& out) const; + protected: bool doCommandSingleton(Command* cmd); private: diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp index 0c6496053..e2b1c21f0 100644 --- a/src/main/driver_unified.cpp +++ b/src/main/driver_unified.cpp @@ -20,6 +20,7 @@ #include #include #include +#include #include #include @@ -45,7 +46,6 @@ #include "util/output.h" #include "util/dump.h" #include "util/result.h" -#include "util/stats.h" using namespace std; using namespace CVC4; @@ -63,10 +63,11 @@ namespace CVC4 { /** Just the basename component of argv[0] */ const char *progName; - /** A pointer to the StatisticsRegistry (the signal handlers need it) */ - CVC4::StatisticsRegistry* pStatistics; - } -} + /** A pointer to the CommandExecutor (the signal handlers need it) */ + CVC4::main::CommandExecutor* pExecutor; + + }/* CVC4::main namespace */ +}/* CVC4 namespace */ void printUsage(Options& opts, bool full) { @@ -185,20 +186,18 @@ int runCvc4(int argc, char* argv[], Options& opts) { # ifndef PORTFOLIO_BUILD ExprManager exprMgr(opts); # else - vector threadOpts = parseThreadSpecificOptions(opts); + vector threadOpts = parseThreadSpecificOptions(opts); ExprManager exprMgr(threadOpts[0]); # endif - CommandExecutor* cmdExecutor = # ifndef PORTFOLIO_BUILD - new CommandExecutor(exprMgr, opts); + CommandExecutor cmdExecutor(exprMgr, opts); # else - new CommandExecutorPortfolio(exprMgr, opts, threadOpts); -#endif + CommandExecutorPortfolio cmdExecutor(exprMgr, opts, threadOpts); +# endif - // Create the SmtEngine - StatisticsRegistry driverStats("driver"); - pStatistics->registerStat_(&driverStats); + // give access to the signal handlers for stats output + pExecutor = &cmdExecutor; Parser* replayParser = NULL; if( opts[options::replayFilename] != "" ) { @@ -218,11 +217,11 @@ int runCvc4(int argc, char* argv[], Options& opts) { } // Timer statistic - RegisterStatistic statTotalTime(&driverStats, &s_totalTime); + RegisterStatistic statTotalTime(&cmdExecutor.getStatisticsRegistry(), &s_totalTime); // Filename statistics ReferenceStat< const char* > s_statFilename("filename", filename); - RegisterStatistic statFilenameReg(&driverStats, &s_statFilename); + RegisterStatistic statFilenameReg(&cmdExecutor.getStatisticsRegistry(), &s_statFilename); // Parse and execute commands until we are done Command* cmd; @@ -243,7 +242,7 @@ int runCvc4(int argc, char* argv[], Options& opts) { replayParser->useDeclarationsFrom(shell.getParser()); } while((cmd = shell.readCommand())) { - status = cmdExecutor->doCommand(cmd) && status; + status = cmdExecutor.doCommand(cmd) && status; delete cmd; } } else { @@ -267,7 +266,7 @@ int runCvc4(int argc, char* argv[], Options& opts) { delete cmd; break; } - status = cmdExecutor->doCommand(cmd); + status = cmdExecutor.doCommand(cmd); delete cmd; } // Remove the parser @@ -283,7 +282,7 @@ int runCvc4(int argc, char* argv[], Options& opts) { int returnValue; string result = "unknown"; if(status) { - result = cmdExecutor->getSmtEngineStatus(); + result = cmdExecutor.getSmtEngineStatus(); if(result == "sat") { returnValue = 10; @@ -298,19 +297,20 @@ int runCvc4(int argc, char* argv[], Options& opts) { } #ifdef CVC4_COMPETITION_MODE - // exit, don't return - // (don't want destructors to run) - exit(returnValue); + // exit, don't return (don't want destructors to run) + // _exit() from unistd.h doesn't run global destructors + // or other on_exit/atexit stuff. + _exit(returnValue); #endif /* CVC4_COMPETITION_MODE */ ReferenceStat< Result > s_statSatResult("sat/unsat", result); - RegisterStatistic statSatResultReg(&driverStats, &s_statSatResult); + RegisterStatistic statSatResultReg(&cmdExecutor.getStatisticsRegistry(), &s_statSatResult); s_totalTime.stop(); if(opts[options::statistics]) { - pStatistics->flushInformation(*opts[options::err]); + cmdExecutor.flushStatistics(*opts[options::err]); } - exit(returnValue); + pExecutor = NULL; return returnValue; } diff --git a/src/main/main.cpp b/src/main/main.cpp index 70f2783a5..73936526f 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -26,6 +26,7 @@ #include "main/main.h" #include "main/interactive_shell.h" +#include "main/command_executor.h" #include "parser/parser.h" #include "parser/parser_builder.h" #include "parser/parser_exception.h" @@ -38,7 +39,7 @@ #include "theory/uf/options.h" #include "util/output.h" #include "util/result.h" -#include "util/stats.h" +#include "util/statistics.h" using namespace std; using namespace CVC4; @@ -66,8 +67,8 @@ int main(int argc, char* argv[]) { *opts[options::out] << "unknown" << endl; #endif *opts[options::err] << "CVC4 Error:" << endl << e << endl; - if(opts[options::statistics] && pStatistics != NULL) { - pStatistics->flushInformation(*opts[options::err]); + if(opts[options::statistics] && pExecutor != NULL) { + pExecutor->flushStatistics(*opts[options::err]); } } exit(1); diff --git a/src/main/main.h b/src/main/main.h index 09ba60c94..8ed4da1cb 100644 --- a/src/main/main.h +++ b/src/main/main.h @@ -20,8 +20,10 @@ #include #include "options/options.h" +#include "expr/expr_manager.h" +#include "smt/smt_engine.h" #include "util/exception.h" -#include "util/stats.h" +#include "util/statistics.h" #include "util/tls.h" #include "cvc4autoconfig.h" @@ -31,14 +33,16 @@ namespace CVC4 { namespace main { +class CommandExecutor; + /** Full argv[0] */ extern const char* progPath; /** Just the basename component of argv[0] */ extern const char* progName; -/** A reference to the StatisticsRegistry for use by the signal handlers */ -extern CVC4::StatisticsRegistry* pStatistics; +/** A reference for use by the signal handlers to print statistics */ +extern CVC4::main::CommandExecutor* pExecutor; /** * If true, will not spin on segfault even when CVC4_DEBUG is on. diff --git a/src/main/util.cpp b/src/main/util.cpp index 756c7d7a9..523486f80 100644 --- a/src/main/util.cpp +++ b/src/main/util.cpp @@ -28,10 +28,12 @@ #include "util/Assert.h" #include "util/exception.h" #include "options/options.h" -#include "util/stats.h" +#include "util/statistics.h" +#include "smt/smt_engine.h" #include "cvc4autoconfig.h" #include "main/main.h" +#include "main/command_executor.h" using CVC4::Exception; using namespace std; @@ -52,8 +54,8 @@ bool segvNoSpin = false; /** Handler for SIGXCPU, i.e., timeout. */ void timeout_handler(int sig, siginfo_t* info, void*) { fprintf(stderr, "CVC4 interrupted by timeout.\n"); - if((*pOptions)[options::statistics] && pStatistics != NULL) { - pStatistics->flushInformation(cerr); + if((*pOptions)[options::statistics] && pExecutor != NULL) { + pExecutor->flushStatistics(cerr); } abort(); } @@ -61,8 +63,8 @@ void timeout_handler(int sig, siginfo_t* info, void*) { /** Handler for SIGINT, i.e., when the user hits control C. */ void sigint_handler(int sig, siginfo_t* info, void*) { fprintf(stderr, "CVC4 interrupted by user.\n"); - if((*pOptions)[options::statistics] && pStatistics != NULL) { - pStatistics->flushInformation(cerr); + if((*pOptions)[options::statistics] && pExecutor != NULL) { + pExecutor->flushStatistics(cerr); } abort(); } @@ -86,8 +88,8 @@ void segv_handler(int sig, siginfo_t* info, void* c) { if(segvNoSpin) { fprintf(stderr, "No-spin requested, aborting...\n"); - if((*pOptions)[options::statistics] && pStatistics != NULL) { - pStatistics->flushInformation(cerr); + if((*pOptions)[options::statistics] && pExecutor != NULL) { + pExecutor->flushStatistics(cerr); } abort(); } else { @@ -106,8 +108,8 @@ void segv_handler(int sig, siginfo_t* info, void* c) { } else if(addr < 10*1024) { cerr << "Looks like a NULL pointer was dereferenced." << endl; } - if((*pOptions)[options::statistics] && pStatistics != NULL) { - pStatistics->flushInformation(cerr); + if((*pOptions)[options::statistics] && pExecutor != NULL) { + pExecutor->flushStatistics(cerr); } abort(); #endif /* CVC4_DEBUG */ @@ -119,8 +121,8 @@ void ill_handler(int sig, siginfo_t* info, void*) { fprintf(stderr, "CVC4 executed an illegal instruction in DEBUG mode.\n"); if(segvNoSpin) { fprintf(stderr, "No-spin requested, aborting...\n"); - if((*pOptions)[options::statistics] && pStatistics != NULL) { - pStatistics->flushInformation(cerr); + if((*pOptions)[options::statistics] && pExecutor != NULL) { + pExecutor->flushStatistics(cerr); } abort(); } else { @@ -132,8 +134,8 @@ void ill_handler(int sig, siginfo_t* info, void*) { } #else /* CVC4_DEBUG */ fprintf(stderr, "CVC4 executed an illegal instruction.\n"); - if((*pOptions)[options::statistics] && pStatistics != NULL) { - pStatistics->flushInformation(cerr); + if((*pOptions)[options::statistics] && pExecutor != NULL) { + pExecutor->flushStatistics(cerr); } abort(); #endif /* CVC4_DEBUG */ @@ -156,8 +158,8 @@ void cvc4unexpected() { } if(segvNoSpin) { fprintf(stderr, "No-spin requested.\n"); - if((*pOptions)[options::statistics] && pStatistics != NULL) { - pStatistics->flushInformation(cerr); + if((*pOptions)[options::statistics] && pExecutor != NULL) { + pExecutor->flushStatistics(cerr); } set_terminate(default_terminator); } else { @@ -169,8 +171,8 @@ void cvc4unexpected() { } #else /* CVC4_DEBUG */ fprintf(stderr, "CVC4 threw an \"unexpected\" exception.\n"); - if((*pOptions)[options::statistics] && pStatistics != NULL) { - pStatistics->flushInformation(cerr); + if((*pOptions)[options::statistics] && pExecutor != NULL) { + pExecutor->flushStatistics(cerr); } set_terminate(default_terminator); #endif /* CVC4_DEBUG */ @@ -182,16 +184,16 @@ void cvc4terminate() { "CVC4 was terminated by the C++ runtime.\n" "Perhaps an exception was thrown during stack unwinding. " "(Don't do that.)\n"); - if((*pOptions)[options::statistics] && pStatistics != NULL) { - pStatistics->flushInformation(cerr); + if((*pOptions)[options::statistics] && pExecutor != NULL) { + pExecutor->flushStatistics(cerr); } default_terminator(); #else /* CVC4_DEBUG */ fprintf(stderr, "CVC4 was terminated by the C++ runtime.\n" "Perhaps an exception was thrown during stack unwinding.\n"); - if((*pOptions)[options::statistics] && pStatistics != NULL) { - pStatistics->flushInformation(cerr); + if((*pOptions)[options::statistics] && pExecutor != NULL) { + pExecutor->flushStatistics(cerr); } default_terminator(); #endif /* CVC4_DEBUG */ diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp index eed9842e2..222a22e34 100644 --- a/src/printer/printer.cpp +++ b/src/printer/printer.cpp @@ -95,7 +95,7 @@ void Printer::toStream(std::ostream& out, const SExpr& sexpr) const throw() { if(sexpr.isInteger()) { out << sexpr.getIntegerValue(); } else if(sexpr.isRational()) { - out << sexpr.getRationalValue(); + out << fixed << sexpr.getRationalValue().getDouble(); } else if(sexpr.isKeyword()) { out << sexpr.getValue(); } else if(sexpr.isString()) { diff --git a/src/prop/bvminisat/simp/SimpSolver.h b/src/prop/bvminisat/simp/SimpSolver.h index 378812e03..4af82b02d 100644 --- a/src/prop/bvminisat/simp/SimpSolver.h +++ b/src/prop/bvminisat/simp/SimpSolver.h @@ -23,7 +23,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "prop/bvminisat/mtl/Queue.h" #include "prop/bvminisat/core/Solver.h" -#include "util/stats.h" +#include "util/statistics_registry.h" #include "context/context.h" namespace BVMinisat { diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h index 567f897a1..a4fdd5b3a 100644 --- a/src/prop/sat_solver.h +++ b/src/prop/sat_solver.h @@ -23,7 +23,7 @@ #include #include -#include "util/stats.h" +#include "util/statistics_registry.h" #include "context/cdlist.h" #include "prop/sat_solver_types.h" diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h index e8da202bd..96332217e 100644 --- a/src/prop/theory_proxy.h +++ b/src/prop/theory_proxy.h @@ -26,7 +26,7 @@ #define __CVC4_USE_MINISAT #include "theory/theory.h" -#include "util/stats.h" +#include "util/statistics_registry.h" #include "context/cdqueue.h" diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 364a786cf..6e8cc9b5d 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -97,6 +97,76 @@ public: Node getFormula() const { return d_formula; } };/* class DefinedFunction */ +struct SmtEngineStatistics { + /** time spent in definition-expansion */ + TimerStat d_definitionExpansionTime; + /** time spent in non-clausal simplification */ + TimerStat d_nonclausalSimplificationTime; + /** Num of constant propagations found during nonclausal simp */ + IntStat d_numConstantProps; + /** time spent in static learning */ + TimerStat d_staticLearningTime; + /** time spent in simplifying ITEs */ + TimerStat d_simpITETime; + /** time spent in simplifying ITEs */ + TimerStat d_unconstrainedSimpTime; + /** time spent removing ITEs */ + TimerStat d_iteRemovalTime; + /** time spent in theory preprocessing */ + TimerStat d_theoryPreprocessTime; + /** time spent converting to CNF */ + TimerStat d_cnfConversionTime; + /** Num of assertions before ite removal */ + IntStat d_numAssertionsPre; + /** Num of assertions after ite removal */ + IntStat d_numAssertionsPost; + /** time spent in checkModel() */ + TimerStat d_checkModelTime; + + SmtEngineStatistics() : + d_definitionExpansionTime("smt::SmtEngine::definitionExpansionTime"), + d_nonclausalSimplificationTime("smt::SmtEngine::nonclausalSimplificationTime"), + d_numConstantProps("smt::SmtEngine::numConstantProps", 0), + d_staticLearningTime("smt::SmtEngine::staticLearningTime"), + d_simpITETime("smt::SmtEngine::simpITETime"), + d_unconstrainedSimpTime("smt::SmtEngine::unconstrainedSimpTime"), + d_iteRemovalTime("smt::SmtEngine::iteRemovalTime"), + d_theoryPreprocessTime("smt::SmtEngine::theoryPreprocessTime"), + d_cnfConversionTime("smt::SmtEngine::cnfConversionTime"), + d_numAssertionsPre("smt::SmtEngine::numAssertionsPreITERemoval", 0), + d_numAssertionsPost("smt::SmtEngine::numAssertionsPostITERemoval", 0), + d_checkModelTime("smt::SmtEngine::checkModelTime") { + + StatisticsRegistry::registerStat(&d_definitionExpansionTime); + StatisticsRegistry::registerStat(&d_nonclausalSimplificationTime); + 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_cnfConversionTime); + StatisticsRegistry::registerStat(&d_numAssertionsPre); + StatisticsRegistry::registerStat(&d_numAssertionsPost); + StatisticsRegistry::registerStat(&d_checkModelTime); + } + + ~SmtEngineStatistics() { + StatisticsRegistry::unregisterStat(&d_definitionExpansionTime); + StatisticsRegistry::unregisterStat(&d_nonclausalSimplificationTime); + 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_cnfConversionTime); + StatisticsRegistry::unregisterStat(&d_numAssertionsPre); + StatisticsRegistry::unregisterStat(&d_numAssertionsPost); + StatisticsRegistry::unregisterStat(&d_checkModelTime); + } +};/* struct SmtEngineStatistics */ + /** * This is an inelegant solution, but for the present, it will work. * The point of this is to separate the public and private portions of @@ -317,33 +387,10 @@ SmtEngine::SmtEngine(ExprManager* em) throw(AssertionException) : d_status(), d_private(new smt::SmtEnginePrivate(*this)), d_statisticsRegistry(new StatisticsRegistry()), - d_definitionExpansionTime("smt::SmtEngine::definitionExpansionTime"), - d_nonclausalSimplificationTime("smt::SmtEngine::nonclausalSimplificationTime"), - d_numConstantProps("smt::SmtEngine::numConstantProps", 0), - d_staticLearningTime("smt::SmtEngine::staticLearningTime"), - d_simpITETime("smt::SmtEngine::simpITETime"), - d_unconstrainedSimpTime("smt::SmtEngine::unconstrainedSimpTime"), - d_iteRemovalTime("smt::SmtEngine::iteRemovalTime"), - d_theoryPreprocessTime("smt::SmtEngine::theoryPreprocessTime"), - d_cnfConversionTime("smt::SmtEngine::cnfConversionTime"), - d_numAssertionsPre("smt::SmtEngine::numAssertionsPreITERemoval", 0), - d_numAssertionsPost("smt::SmtEngine::numAssertionsPostITERemoval", 0), - d_checkModelTime("smt::SmtEngine::checkModelTime") { + d_stats(NULL) { SmtScope smts(this); - - StatisticsRegistry::registerStat(&d_definitionExpansionTime); - StatisticsRegistry::registerStat(&d_nonclausalSimplificationTime); - 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_cnfConversionTime); - StatisticsRegistry::registerStat(&d_numAssertionsPre); - StatisticsRegistry::registerStat(&d_numAssertionsPost); - StatisticsRegistry::registerStat(&d_checkModelTime); + d_stats = new SmtEngineStatistics(); // We have mutual dependency here, so we add the prop engine to the theory // engine later (it is non-essential there) @@ -484,18 +531,7 @@ SmtEngine::~SmtEngine() throw() { d_definedFunctions->deleteSelf(); - StatisticsRegistry::unregisterStat(&d_definitionExpansionTime); - StatisticsRegistry::unregisterStat(&d_nonclausalSimplificationTime); - 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_cnfConversionTime); - StatisticsRegistry::unregisterStat(&d_numAssertionsPre); - StatisticsRegistry::unregisterStat(&d_numAssertionsPost); - StatisticsRegistry::unregisterStat(&d_checkModelTime); + delete d_stats; delete d_private; @@ -777,20 +813,20 @@ CVC4::SExpr SmtEngine::getInfo(const std::string& key) const Trace("smt") << "SMT getInfo(" << key << ")" << endl; if(key == "all-statistics") { vector stats; - for(StatisticsRegistry::const_iterator i = d_exprManager->getStatisticsRegistry()->begin_(); - i != d_exprManager->getStatisticsRegistry()->end_(); + for(StatisticsRegistry::const_iterator i = NodeManager::fromExprManager(d_exprManager)->getStatisticsRegistry()->begin(); + i != NodeManager::fromExprManager(d_exprManager)->getStatisticsRegistry()->end(); ++i) { vector v; - v.push_back((*i)->getName()); - v.push_back((*i)->getValue()); + v.push_back((*i).first); + v.push_back((*i).second); stats.push_back(v); } - for(StatisticsRegistry::const_iterator i = d_statisticsRegistry->begin_(); - i != d_statisticsRegistry->end_(); + for(StatisticsRegistry::const_iterator i = d_statisticsRegistry->begin(); + i != d_statisticsRegistry->end(); ++i) { vector v; - v.push_back((*i)->getName()); - v.push_back((*i)->getValue()); + v.push_back((*i).first); + v.push_back((*i).second); stats.push_back(v); } return stats; @@ -979,7 +1015,7 @@ void SmtEnginePrivate::removeITEs() { void SmtEnginePrivate::staticLearning() { d_smt.finalOptionsAreSet(); - TimerStat::CodeTimer staticLearningTimer(d_smt.d_staticLearningTime); + TimerStat::CodeTimer staticLearningTimer(d_smt.d_stats->d_staticLearningTime); Trace("simplify") << "SmtEnginePrivate::staticLearning()" << endl; @@ -1001,7 +1037,7 @@ void SmtEnginePrivate::staticLearning() { bool SmtEnginePrivate::nonClausalSimplify() { d_smt.finalOptionsAreSet(); - TimerStat::CodeTimer nonclausalTimer(d_smt.d_nonclausalSimplificationTime); + TimerStat::CodeTimer nonclausalTimer(d_smt.d_stats->d_nonclausalSimplificationTime); Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify()" << endl; @@ -1044,7 +1080,7 @@ bool SmtEnginePrivate::nonClausalSimplify() { if (learnedLiteralNew == learnedLiteral) { break; } - ++d_smt.d_numConstantProps; + ++d_smt.d_stats->d_numConstantProps; learnedLiteral = Rewriter::rewrite(learnedLiteralNew); } // It might just simplify to a constant @@ -1174,7 +1210,7 @@ bool SmtEnginePrivate::nonClausalSimplify() { if (assertionNew == assertion) { break; } - ++d_smt.d_numConstantProps; + ++d_smt.d_stats->d_numConstantProps; assertion = Rewriter::rewrite(assertionNew); } s.insert(assertion); @@ -1222,7 +1258,7 @@ bool SmtEnginePrivate::nonClausalSimplify() { if (learnedNew == learned) { break; } - ++d_smt.d_numConstantProps; + ++d_smt.d_stats->d_numConstantProps; learned = Rewriter::rewrite(learnedNew); } if (s.find(learned) != s.end()) { @@ -1258,9 +1294,8 @@ bool SmtEnginePrivate::nonClausalSimplify() { } -void SmtEnginePrivate::simpITE() -{ - TimerStat::CodeTimer simpITETimer(d_smt.d_simpITETime); +void SmtEnginePrivate::simpITE() { + TimerStat::CodeTimer simpITETimer(d_smt.d_stats->d_simpITETime); Trace("simplify") << "SmtEnginePrivate::simpITE()" << endl; @@ -1271,9 +1306,8 @@ void SmtEnginePrivate::simpITE() } -void SmtEnginePrivate::unconstrainedSimp() -{ - TimerStat::CodeTimer unconstrainedSimpTimer(d_smt.d_unconstrainedSimpTime); +void SmtEnginePrivate::unconstrainedSimp() { + TimerStat::CodeTimer unconstrainedSimpTimer(d_smt.d_stats->d_unconstrainedSimpTime); Trace("simplify") << "SmtEnginePrivate::unconstrainedSimp()" << endl; d_smt.d_theoryEngine->ppUnconstrainedSimp(d_assertionsToCheck); @@ -1362,7 +1396,7 @@ bool SmtEnginePrivate::simplifyAssertions() // Theory preprocessing if (d_smt.d_earlyTheoryPP) { - TimerStat::CodeTimer codeTimer(d_smt.d_theoryPreprocessTime); + TimerStat::CodeTimer codeTimer(d_smt.d_stats->d_theoryPreprocessTime); // Call the theory preprocessors d_smt.d_theoryEngine->preprocessStart(); for (unsigned i = 0; i < d_assertionsToCheck.size(); ++ i) { @@ -1503,7 +1537,7 @@ void SmtEnginePrivate::processAssertions() { { Chat() << "expanding definitions..." << endl; Trace("simplify") << "SmtEnginePrivate::simplify(): expanding definitions" << endl; - TimerStat::CodeTimer codeTimer(d_smt.d_definitionExpansionTime); + TimerStat::CodeTimer codeTimer(d_smt.d_stats->d_definitionExpansionTime); hash_map cache; for (unsigned i = 0; i < d_assertionsToPreprocess.size(); ++ i) { d_assertionsToPreprocess[i] = @@ -1535,11 +1569,11 @@ void SmtEnginePrivate::processAssertions() { { Chat() << "removing term ITEs..." << endl; - TimerStat::CodeTimer codeTimer(d_smt.d_iteRemovalTime); + TimerStat::CodeTimer codeTimer(d_smt.d_stats->d_iteRemovalTime); // Remove ITEs, updating d_iteSkolemMap - d_smt.d_numAssertionsPre += d_assertionsToCheck.size(); + d_smt.d_stats->d_numAssertionsPre += d_assertionsToCheck.size(); removeITEs(); - d_smt.d_numAssertionsPost += d_assertionsToCheck.size(); + d_smt.d_stats->d_numAssertionsPost += d_assertionsToCheck.size(); } if(options::repeatSimp()) { @@ -1585,7 +1619,7 @@ void SmtEnginePrivate::processAssertions() { { Chat() << "theory preprocessing..." << endl; - TimerStat::CodeTimer codeTimer(d_smt.d_theoryPreprocessTime); + TimerStat::CodeTimer codeTimer(d_smt.d_stats->d_theoryPreprocessTime); // Call the theory preprocessors d_smt.d_theoryEngine->preprocessStart(); for (unsigned i = 0; i < d_assertionsToCheck.size(); ++ i) { @@ -1615,7 +1649,7 @@ void SmtEnginePrivate::processAssertions() { // Push the formula to SAT { Chat() << "converting to CNF..." << endl; - TimerStat::CodeTimer codeTimer(d_smt.d_cnfConversionTime); + TimerStat::CodeTimer codeTimer(d_smt.d_stats->d_cnfConversionTime); for (unsigned i = 0; i < d_assertionsToCheck.size(); ++ i) { d_smt.d_propEngine->assertFormula(d_assertionsToCheck[i]); } @@ -2016,7 +2050,7 @@ void SmtEngine::checkModel() throw(InternalErrorException) { // so we should be ok. Assert(d_assertionList != NULL, "don't have an assertion list to check in SmtEngine::checkModel()"); - TimerStat::CodeTimer checkModelTimer(d_checkModelTime); + TimerStat::CodeTimer checkModelTimer(d_stats->d_checkModelTime); // Throughout, we use Notice() to give diagnostic output. // @@ -2321,8 +2355,12 @@ unsigned long SmtEngine::getTimeRemaining() const throw(ModalException) { d_timeBudgetCumulative - d_cumulativeTimeUsed; } -StatisticsRegistry* SmtEngine::getStatisticsRegistry() const { - return d_statisticsRegistry; +Statistics SmtEngine::getStatistics() const throw() { + return Statistics(*d_statisticsRegistry); +} + +SExpr SmtEngine::getStatistic(std::string name) const throw() { + return d_statisticsRegistry->getStatistic(name); } void SmtEngine::printModel( std::ostream& out, Model* m ){ diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 2fa60104c..cbb97f9f7 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -35,7 +35,7 @@ #include "options/options.h" #include "util/result.h" #include "util/sexpr.h" -#include "util/stats.h" +#include "util/statistics.h" #include "theory/logic_info.h" // In terms of abstraction, this is below (and provides services to) @@ -51,6 +51,7 @@ class NodeHashFunction; class Command; +class SmtEngine; class DecisionEngine; class TheoryEngine; @@ -74,6 +75,7 @@ namespace smt { */ class DefinedFunction; + class SmtEngineStatistics; class SmtEnginePrivate; class SmtScope; @@ -83,6 +85,10 @@ namespace smt { typedef context::CDList CommandList; }/* CVC4::smt namespace */ +namespace stats { + StatisticsRegistry* getStatisticsRegistry(SmtEngine*); +}/* CVC4::stats namespace */ + // TODO: SAT layer (esp. CNF- versus non-clausal solvers under the // hood): use a type parameter and have check() delegate, or subclass // SmtEngine and override check()? @@ -273,6 +279,7 @@ class CVC4_PUBLIC SmtEngine { friend class ::CVC4::smt::SmtEnginePrivate; friend class ::CVC4::smt::SmtScope; + friend ::CVC4::StatisticsRegistry* ::CVC4::stats::getStatisticsRegistry(SmtEngine*); friend void ::CVC4::smt::beforeSearch(std::string, bool, SmtEngine*) throw(ModalException); // to access d_modelCommands friend size_t ::CVC4::Model::getNumCommands() const; @@ -280,31 +287,7 @@ class CVC4_PUBLIC SmtEngine { StatisticsRegistry* d_statisticsRegistry; - // === STATISTICS === - /** time spent in definition-expansion */ - TimerStat d_definitionExpansionTime; - /** time spent in non-clausal simplification */ - TimerStat d_nonclausalSimplificationTime; - /** Num of constant propagations found during nonclausal simp */ - IntStat d_numConstantProps; - /** time spent in static learning */ - TimerStat d_staticLearningTime; - /** time spent in simplifying ITEs */ - TimerStat d_simpITETime; - /** time spent in simplifying ITEs */ - TimerStat d_unconstrainedSimpTime; - /** time spent removing ITEs */ - TimerStat d_iteRemovalTime; - /** time spent in theory preprocessing */ - TimerStat d_theoryPreprocessTime; - /** time spent converting to CNF */ - TimerStat d_cnfConversionTime; - /** Num of assertions before ite removal */ - IntStat d_numAssertionsPre; - /** Num of assertions after ite removal */ - IntStat d_numAssertionsPost; - /** time spent in checkModel() */ - TimerStat d_checkModelTime; + smt::SmtEngineStatistics* d_stats; /** * Add to Model command. This is used for recording a command that should be reported @@ -567,9 +550,14 @@ public: } /** - * Permit access to the underlying StatisticsRegistry. + * Export statistics from this SmtEngine. + */ + Statistics getStatistics() const throw(); + + /** + * Get the value of one named statistic from this SmtEngine. */ - StatisticsRegistry* getStatisticsRegistry() const; + SExpr getStatistic(std::string name) const throw(); Result getStatusOfLastCommand() const { return d_status; diff --git a/src/theory/arith/arith_priority_queue.h b/src/theory/arith/arith_priority_queue.h index 43cf54d37..b4c2ef6d3 100644 --- a/src/theory/arith/arith_priority_queue.h +++ b/src/theory/arith/arith_priority_queue.h @@ -28,7 +28,7 @@ #include "theory/arith/matrix.h" #include "theory/arith/partial_model.h" -#include "util/stats.h" +#include "util/statistics_registry.h" #include diff --git a/src/theory/arith/arith_static_learner.h b/src/theory/arith/arith_static_learner.h index 66eb4d311..db0a5f4df 100644 --- a/src/theory/arith/arith_static_learner.h +++ b/src/theory/arith/arith_static_learner.h @@ -23,7 +23,7 @@ #define __CVC4__THEORY__ARITH__ARITH_STATIC_LEARNER_H -#include "util/stats.h" +#include "util/statistics_registry.h" #include "theory/arith/arith_utilities.h" #include "theory/substitutions.h" #include diff --git a/src/theory/arith/congruence_manager.h b/src/theory/arith/congruence_manager.h index 83a5e7fb4..55c704e18 100644 --- a/src/theory/arith/congruence_manager.h +++ b/src/theory/arith/congruence_manager.h @@ -33,7 +33,7 @@ #include "context/cdtrail_queue.h" #include "context/cdmaybe.h" -#include "util/stats.h" +#include "util/statistics_registry.h" #include "util/dense_map.h" namespace CVC4 { diff --git a/src/theory/arith/dio_solver.h b/src/theory/arith/dio_solver.h index b6c9e3afb..7baa423e8 100644 --- a/src/theory/arith/dio_solver.h +++ b/src/theory/arith/dio_solver.h @@ -27,7 +27,7 @@ #include "theory/arith/partial_model.h" #include "util/rational.h" -#include "util/stats.h" +#include "util/statistics_registry.h" #include #include diff --git a/src/theory/arith/linear_equality.h b/src/theory/arith/linear_equality.h index 2553bedd0..ad6aafcac 100644 --- a/src/theory/arith/linear_equality.h +++ b/src/theory/arith/linear_equality.h @@ -38,7 +38,7 @@ #include "theory/arith/matrix.h" #include "theory/arith/constraint.h" -#include "util/stats.h" +#include "util/statistics_registry.h" namespace CVC4 { namespace theory { diff --git a/src/theory/arith/simplex.h b/src/theory/arith/simplex.h index 324f3b21b..eff969818 100644 --- a/src/theory/arith/simplex.h +++ b/src/theory/arith/simplex.h @@ -61,7 +61,7 @@ #include "util/dense_map.h" #include "options/options.h" -#include "util/stats.h" +#include "util/statistics_registry.h" #include "util/result.h" #include diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index a8c025452..c98c759f7 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -43,7 +43,7 @@ #include "theory/arith/constraint.h" -#include "util/stats.h" +#include "util/statistics_registry.h" #include "util/result.h" #include diff --git a/src/theory/arith/theory_arith_instantiator.h b/src/theory/arith/theory_arith_instantiator.h index a7602cf28..a8843bdd4 100644 --- a/src/theory/arith/theory_arith_instantiator.h +++ b/src/theory/arith/theory_arith_instantiator.h @@ -23,7 +23,7 @@ #include "theory/quantifiers_engine.h" #include "theory/arith/arithvar_node_map.h" -#include "util/stats.h" +#include "util/statistics_registry.h" namespace CVC4 { namespace theory { diff --git a/src/theory/arrays/array_info.h b/src/theory/arrays/array_info.h index e847a238d..ce34c72c4 100644 --- a/src/theory/arrays/array_info.h +++ b/src/theory/arrays/array_info.h @@ -24,7 +24,7 @@ #include "context/cdlist.h" #include "context/cdhashmap.h" #include "expr/node.h" -#include "util/stats.h" +#include "util/statistics_registry.h" #include "util/ntuple.h" #include #include diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index aebee6817..b92921be7 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -23,7 +23,7 @@ #include "theory/theory.h" #include "theory/arrays/array_info.h" -#include "util/stats.h" +#include "util/statistics_registry.h" #include "theory/uf/equality_engine.h" #include "context/cdhashmap.h" #include "context/cdhashset.h" diff --git a/src/theory/bv/bitblaster.h b/src/theory/bv/bitblaster.h index 16c50be22..2ff12bbdf 100644 --- a/src/theory/bv/bitblaster.h +++ b/src/theory/bv/bitblaster.h @@ -35,7 +35,7 @@ #include "theory/theory.h" #include "theory_bv_utils.h" -#include "util/stats.h" +#include "util/statistics_registry.h" #include "bitblast_strategies.h" #include "prop/sat_solver.h" diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index 30cf5ac52..36a542878 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -26,7 +26,7 @@ #include "context/cdlist.h" #include "context/cdhashset.h" #include "theory/bv/theory_bv_utils.h" -#include "util/stats.h" +#include "util/statistics_registry.h" #include "context/cdqueue.h" #include "theory/bv/bv_subtheory.h" #include "theory/bv/bv_subtheory_eq.h" diff --git a/src/theory/bv/theory_bv_rewrite_rules.h b/src/theory/bv/theory_bv_rewrite_rules.h index 2fd409313..ccc281d6f 100644 --- a/src/theory/bv/theory_bv_rewrite_rules.h +++ b/src/theory/bv/theory_bv_rewrite_rules.h @@ -22,7 +22,7 @@ #include "cvc4_private.h" #include "theory/theory.h" #include "context/context.h" -#include "util/stats.h" +#include "util/statistics_registry.h" #include "theory/bv/theory_bv_utils.h" #include "expr/command.h" #include diff --git a/src/theory/bv/theory_bv_rewriter.h b/src/theory/bv/theory_bv_rewriter.h index 6b885f1ed..853ccdc32 100644 --- a/src/theory/bv/theory_bv_rewriter.h +++ b/src/theory/bv/theory_bv_rewriter.h @@ -23,7 +23,7 @@ #define __CVC4__THEORY__BV__THEORY_BV_REWRITER_H #include "theory/rewriter.h" -#include "util/stats.h" +#include "util/statistics_registry.h" namespace CVC4 { namespace theory { diff --git a/src/theory/datatypes/theory_datatypes_instantiator.h b/src/theory/datatypes/theory_datatypes_instantiator.h index fe43f2cfc..ae47543ec 100644 --- a/src/theory/datatypes/theory_datatypes_instantiator.h +++ b/src/theory/datatypes/theory_datatypes_instantiator.h @@ -22,7 +22,7 @@ #include "theory/quantifiers_engine.h" -#include "util/stats.h" +#include "util/statistics_registry.h" namespace CVC4 { namespace theory { diff --git a/src/theory/ite_simplifier.h b/src/theory/ite_simplifier.h index cba5c7051..582b87b09 100644 --- a/src/theory/ite_simplifier.h +++ b/src/theory/ite_simplifier.h @@ -39,7 +39,7 @@ #include "theory/shared_terms_database.h" #include "theory/term_registration_visitor.h" #include "theory/valuation.h" -#include "util/stats.h" +#include "util/statistics_registry.h" #include "util/hash.h" #include "util/cache.h" #include "util/ite_removal.h" diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h index bc712955e..6d2290d75 100644 --- a/src/theory/quantifiers/theory_quantifiers.h +++ b/src/theory/quantifiers/theory_quantifiers.h @@ -23,7 +23,7 @@ #include "theory/theory.h" #include "util/hash.h" -#include "util/stats.h" +#include "util/statistics_registry.h" #include #include diff --git a/src/theory/quantifiers/theory_quantifiers_instantiator.h b/src/theory/quantifiers/theory_quantifiers_instantiator.h index e837811b0..2a8b8b35c 100644 --- a/src/theory/quantifiers/theory_quantifiers_instantiator.h +++ b/src/theory/quantifiers/theory_quantifiers_instantiator.h @@ -22,7 +22,7 @@ #include "theory/quantifiers_engine.h" -#include "util/stats.h" +#include "util/statistics_registry.h" namespace CVC4 { namespace theory { diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index ca5cc568e..8badb3998 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -97,7 +97,11 @@ d_active( c ){ } QuantifiersEngine::~QuantifiersEngine(){ - delete(d_term_db); + delete d_model_engine; + delete d_inst_engine; + delete d_model; + delete d_term_db; + delete d_eq_query; } Instantiator* QuantifiersEngine::getInstantiator( theory::TheoryId id ){ diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 34d9d69a2..befd12d9d 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -24,7 +24,7 @@ #include "theory/quantifiers/inst_match.h" #include "theory/rewriterules/rr_inst_match.h" -#include "util/stats.h" +#include "util/statistics_registry.h" #include #include diff --git a/src/theory/rewriterules/theory_rewriterules.h b/src/theory/rewriterules/theory_rewriterules.h index 5937c541f..e2e7c7e1a 100644 --- a/src/theory/rewriterules/theory_rewriterules.h +++ b/src/theory/rewriterules/theory_rewriterules.h @@ -30,7 +30,7 @@ #include "theory/rewriterules/rr_inst_match_impl.h" #include "theory/rewriterules/rr_trigger.h" #include "theory/rewriterules/rr_inst_match.h" -#include "util/stats.h" +#include "util/statistics_registry.h" #include "theory/rewriterules/theory_rewriterules_preprocess.h" #include "theory/model.h" diff --git a/src/theory/shared_terms_database.h b/src/theory/shared_terms_database.h index c685257ba..0c163015a 100644 --- a/src/theory/shared_terms_database.h +++ b/src/theory/shared_terms_database.h @@ -22,7 +22,7 @@ #include "expr/node.h" #include "theory/theory.h" #include "theory/uf/equality_engine.h" -#include "util/stats.h" +#include "util/statistics_registry.h" #include "context/cdhashset.h" namespace CVC4 { diff --git a/src/theory/theory.h b/src/theory/theory.h index 2f980fe2f..0ff6c1fe5 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -33,7 +33,7 @@ #include "context/cdlist.h" #include "context/cdo.h" #include "options/options.h" -#include "util/stats.h" +#include "util/statistics_registry.h" #include "util/dump.h" #include diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index d1d6bd1f3..f2324e5d2 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -38,7 +38,7 @@ #include "theory/valuation.h" #include "options/options.h" #include "smt/options.h" -#include "util/stats.h" +#include "util/statistics_registry.h" #include "util/hash.h" #include "util/cache.h" #include "theory/ite_simplifier.h" diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h index cae169081..e32a34707 100644 --- a/src/theory/uf/equality_engine.h +++ b/src/theory/uf/equality_engine.h @@ -30,7 +30,7 @@ #include "expr/kind_map.h" #include "context/cdo.h" #include "util/output.h" -#include "util/stats.h" +#include "util/statistics_registry.h" #include "theory/rewriter.h" #include "theory/theory.h" diff --git a/src/theory/uf/inst_strategy.h b/src/theory/uf/inst_strategy.h index 663720326..6369c6ba3 100644 --- a/src/theory/uf/inst_strategy.h +++ b/src/theory/uf/inst_strategy.h @@ -25,7 +25,7 @@ #include "context/context.h" #include "context/context_mm.h" -#include "util/stats.h" +#include "util/statistics_registry.h" #include "theory/uf/theory_uf.h" namespace CVC4 { diff --git a/src/theory/uf/symmetry_breaker.h b/src/theory/uf/symmetry_breaker.h index 2b7b10209..fe97e8afc 100644 --- a/src/theory/uf/symmetry_breaker.h +++ b/src/theory/uf/symmetry_breaker.h @@ -52,7 +52,7 @@ #include "expr/node.h" #include "expr/node_builder.h" -#include "util/stats.h" +#include "util/statistics_registry.h" namespace CVC4 { namespace theory { diff --git a/src/theory/uf/theory_uf_instantiator.h b/src/theory/uf/theory_uf_instantiator.h index 59b8f36a4..1929e0e47 100644 --- a/src/theory/uf/theory_uf_instantiator.h +++ b/src/theory/uf/theory_uf_instantiator.h @@ -25,7 +25,7 @@ #include "context/context_mm.h" #include "context/cdchunk_list.h" -#include "util/stats.h" +#include "util/statistics_registry.h" #include "theory/uf/theory_uf.h" #include "theory/quantifiers/trigger.h" #include "util/ntuple.h" diff --git a/src/theory/uf/theory_uf_strong_solver.h b/src/theory/uf/theory_uf_strong_solver.h index 8c63b4308..d78a43498 100644 --- a/src/theory/uf/theory_uf_strong_solver.h +++ b/src/theory/uf/theory_uf_strong_solver.h @@ -25,7 +25,7 @@ #include "context/context_mm.h" #include "context/cdchunk_list.h" -#include "util/stats.h" +#include "util/statistics_registry.h" namespace CVC4 { namespace theory { diff --git a/src/util/Makefile.am b/src/util/Makefile.am index 7d3664d47..7d9a055fd 100644 --- a/src/util/Makefile.am +++ b/src/util/Makefile.am @@ -3,13 +3,15 @@ AM_CPPFLAGS = \ -I@srcdir@/../include -I@srcdir@/.. -I@builddir@/.. AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) -noinst_LTLIBRARIES = libutil.la libutilcudd.la +noinst_LTLIBRARIES = libutil.la libutilcudd.la libstatistics.la # libutilcudd.la is a separate library so that we can pass separate # compiler flags libutilcudd_la_CPPFLAGS = $(CPPFLAGS) $(AM_CPPFLAGS) @CUDD_CPPFLAGS@ libutilcudd_la_LIBADD = @CUDD_LDFLAGS@ @CUDD_LIBS@ +libstatistics_la_CPPFLAGS = $(CPPFLAGS) $(AM_CPPFLAGS) -D__BUILDING_STATISTICS_FOR_EXPORT + # Do not list built sources (like integer.h, rational.h, and tls.h) here! # Rather, list them under BUILT_SOURCES, and their .in versions under # EXTRA_DIST. Otherwise, they're packaged up in the tarball, which is @@ -44,8 +46,10 @@ libutil_la_SOURCES = \ gmp_util.h \ sexpr.h \ sexpr.cpp \ - stats.h \ - stats.cpp \ + statistics.h \ + statistics.cpp \ + statistics_registry.h \ + statistics_registry.cpp \ dynamic_array.h \ language.h \ lemma_input_channel.h \ @@ -81,6 +85,11 @@ libutil_la_SOURCES = \ libutil_la_LIBADD = \ @builddir@/libutilcudd.la + +libstatistics_la_SOURCES = \ + statistics_registry.h \ + statistics_registry.cpp + libutilcudd_la_SOURCES = \ propositional_query.h \ propositional_query.cpp @@ -110,7 +119,7 @@ EXTRA_DIST = \ integer.h.in \ tls.h.in \ integer.i \ - stats.i \ + statistics.i \ bool.i \ sexpr.i \ datatype.i \ diff --git a/src/util/sexpr.h b/src/util/sexpr.h index 0734dec6c..4feffc18f 100644 --- a/src/util/sexpr.h +++ b/src/util/sexpr.h @@ -23,6 +23,8 @@ #include #include +#include +#include #include "util/integer.h" #include "util/rational.h" @@ -151,6 +153,12 @@ public: */ const std::vector& getChildren() const; + /** Is this S-expression equal to another? */ + bool operator==(const SExpr& s) const; + + /** Is this S-expression different from another? */ + bool operator!=(const SExpr& s) const; + };/* class SExpr */ inline bool SExpr::isAtom() const { @@ -178,8 +186,15 @@ inline std::string SExpr::getValue() const { switch(d_sexprType) { case SEXPR_INTEGER: return d_integerValue.toString(); - case SEXPR_RATIONAL: - return d_rationalValue.toString(); + case SEXPR_RATIONAL: { + // We choose to represent rationals as decimal strings rather than + // "numerator/denominator." Perhaps an additional SEXPR_DECIMAL + // could be added if we need both styles, even if it's backed by + // the same Rational object. + std::stringstream ss; + ss << std::fixed << d_rationalValue.getDouble(); + return ss.str(); + } case SEXPR_STRING: case SEXPR_KEYWORD: return d_stringValue; @@ -204,6 +219,18 @@ inline const std::vector& SExpr::getChildren() const { return d_children; } +inline bool SExpr::operator==(const SExpr& s) const { + return d_sexprType == s.d_sexprType && + d_integerValue == s.d_integerValue && + d_rationalValue == s.d_rationalValue && + d_stringValue == s.d_stringValue && + d_children == s.d_children; +} + +inline bool SExpr::operator!=(const SExpr& s) const { + return !(*this == s); +} + std::ostream& operator<<(std::ostream& out, const SExpr& sexpr) CVC4_PUBLIC; }/* CVC4 namespace */ diff --git a/src/util/statistics.cpp b/src/util/statistics.cpp new file mode 100644 index 000000000..bc6bcb53d --- /dev/null +++ b/src/util/statistics.cpp @@ -0,0 +1,134 @@ +/********************* */ +/*! \file statistics.cpp + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009-2012 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + +#include "util/statistics.h" +#include "util/statistics_registry.h" // for details about class Stat + +#include + +namespace CVC4 { + +std::string StatisticsBase::s_regDelim("::"); + +bool StatisticsBase::StatCmp::operator()(const Stat* s1, const Stat* s2) const { + return s1->getName() < s2->getName(); +} + +StatisticsBase::iterator::value_type StatisticsBase::iterator::operator*() const { + return std::make_pair((*d_it)->getName(), (*d_it)->getValue()); +} + +StatisticsBase::StatisticsBase() : + d_prefix(), + d_stats() { +} + +StatisticsBase::StatisticsBase(const StatisticsBase& stats) : + d_prefix(stats.d_prefix), + d_stats() { +} + +StatisticsBase& StatisticsBase::operator=(const StatisticsBase& stats) { + d_prefix = stats.d_prefix; + return *this; +} + +void Statistics::copyFrom(const StatisticsBase& stats) { + // This is ugly, but otherwise we have to introduce a "friend" relation for + // Base to its derived class (really obnoxious). + StatSet::const_iterator i_begin = ((const Statistics*) &stats)->d_stats.begin(); + StatSet::const_iterator i_end = ((const Statistics*) &stats)->d_stats.end(); + for(StatSet::const_iterator i = i_begin; i != i_end; ++i) { + SExprStat* p = new SExprStat((*i)->getName(), (*i)->getValue()); + d_stats.insert(p); + } +} + +void Statistics::clear() { + for(StatSet::iterator i = d_stats.begin(); i != d_stats.end(); ++i) { + delete *i; + } + d_stats.clear(); +} + +Statistics::Statistics(const StatisticsBase& stats) : + StatisticsBase(stats) { + copyFrom(stats); +} + +Statistics::Statistics(const Statistics& stats) : + StatisticsBase(stats) { + copyFrom(stats); +} + +Statistics::~Statistics() { + clear(); +} + +Statistics& Statistics::operator=(const StatisticsBase& stats) { + clear(); + this->StatisticsBase::operator=(stats); + copyFrom(stats); + + return *this; +} + +Statistics& Statistics::operator=(const Statistics& stats) { + return this->operator=((const StatisticsBase&)stats); +} + +StatisticsBase::const_iterator StatisticsBase::begin() const { + return iterator(d_stats.begin()); +} + +StatisticsBase::const_iterator StatisticsBase::end() const { + return iterator(d_stats.end()); +} + +void StatisticsBase::flushInformation(std::ostream &out) const { +#ifdef CVC4_STATISTICS_ON + for(StatSet::iterator i = d_stats.begin(); + i != d_stats.end(); + ++i) { + Stat* s = *i; + if(d_prefix != "") { + out << d_prefix << s_regDelim; + } + s->flushStat(out); + out << std::endl; + } +#endif /* CVC4_STATISTICS_ON */ +} + +SExpr StatisticsBase::getStatistic(std::string name) const { + SExpr value; + IntStat s(name, 0); + StatSet::iterator i = d_stats.find(&s); + if(i != d_stats.end()) { + return (*i)->getValue(); + } else { + return SExpr(); + } +} + +void StatisticsBase::setPrefix(const std::string& prefix) { + d_prefix = prefix; +} + +}/* CVC4 namespace */ diff --git a/src/util/statistics.h b/src/util/statistics.h new file mode 100644 index 000000000..e04db5846 --- /dev/null +++ b/src/util/statistics.h @@ -0,0 +1,129 @@ +/********************* */ +/*! \file statistics.h + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009-2012 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + +#include "cvc4_public.h" + +#ifndef __CVC4__STATISTICS_H +#define __CVC4__STATISTICS_H + +#include "util/sexpr.h" + +#include +#include +#include +#include +#include + +namespace CVC4 { + +class Stat; + +class CVC4_PUBLIC StatisticsBase { +protected: + + static std::string s_regDelim; + + /** A helper class for comparing two statistics */ + struct StatCmp { + bool operator()(const Stat* s1, const Stat* s2) const; + };/* struct StatisticsRegistry::StatCmp */ + + /** A type for a set of statistics */ + typedef std::set< Stat*, StatCmp > StatSet; + + std::string d_prefix; + + /** The set of statistics in this object */ + StatSet d_stats; + + StatisticsBase(); + StatisticsBase(const StatisticsBase& stats); + StatisticsBase& operator=(const StatisticsBase& stats); + +public: + + virtual ~StatisticsBase() { } + + class CVC4_PUBLIC iterator : public std::iterator< std::input_iterator_tag, std::pair > { + StatSet::iterator d_it; + + iterator(StatSet::iterator it) : d_it(it) { } + + friend class StatisticsBase; + + public: + value_type operator*() const; + iterator& operator++() { ++d_it; return *this; } + iterator operator++(int) { iterator old = *this; ++d_it; return old; } + bool operator==(const iterator& i) const { return d_it == i.d_it; } + bool operator!=(const iterator& i) const { return d_it != i.d_it; } + };/* class StatisticsBase::iterator */ + + /** An iterator type over a set of statistics. */ + typedef iterator const_iterator; + + /** Set the output prefix for this set of statistics. */ + virtual void setPrefix(const std::string& prefix); + + /** Flush all statistics to the given output stream. */ + void flushInformation(std::ostream& out) const; + + /** Get the value of a named statistic. */ + SExpr getStatistic(std::string name) const; + + /** + * Get an iterator to the beginning of the range of the set of + * statistics. + */ + const_iterator begin() const; + + /** + * Get an iterator to the end of the range of the set of statistics. + */ + const_iterator end() const; + +};/* class StatisticsBase */ + +class CVC4_PUBLIC Statistics : public StatisticsBase { + void clear(); + void copyFrom(const StatisticsBase&); + +public: + + /** + * Override the copy constructor to do a "deep" copy of statistics + * values. + */ + Statistics(const StatisticsBase& stats); + Statistics(const Statistics& stats); + + ~Statistics(); + + /** + * Override the assignment operator to do a "deep" copy of statistics + * values. + */ + Statistics& operator=(const StatisticsBase& stats); + Statistics& operator=(const Statistics& stats); + +};/* class Statistics */ + +}/* CVC4 namespace */ + +#endif /* __CVC4__STATISTICS_H */ diff --git a/src/util/statistics.i b/src/util/statistics.i new file mode 100644 index 000000000..7cc737d6c --- /dev/null +++ b/src/util/statistics.i @@ -0,0 +1,6 @@ +%{ +#include "util/statistics.h" +%} + +%include "util/statistics.h" + diff --git a/src/util/statistics_registry.cpp b/src/util/statistics_registry.cpp new file mode 100644 index 000000000..f2a698a48 --- /dev/null +++ b/src/util/statistics_registry.cpp @@ -0,0 +1,131 @@ +/********************* */ +/*! \file statistics_registry.cpp + ** \verbatim + ** Original author: taking + ** Major contributors: mdeters + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009-2012 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + +#include "util/statistics_registry.h" +#include "expr/node_manager.h" +#include "expr/expr_manager_scope.h" +#include "expr/expr_manager.h" +#include "lib/clock_gettime.h" +#include "smt/smt_engine_scope.h" +#include "smt/smt_engine.h" + +#ifdef CVC4_STATISTICS_ON +# define __CVC4_USE_STATISTICS true +#else +# define __CVC4_USE_STATISTICS false +#endif + +namespace CVC4 { + +namespace stats { + +// This is a friend of SmtEngine, just to reach in and get it. +// this isn't a class function because then there's a cyclic +// dependence. +inline StatisticsRegistry* getStatisticsRegistry(SmtEngine* smt) { + return smt->d_statisticsRegistry; +} + +}/* CVC4::stats namespace */ + +#ifndef __BUILDING_STATISTICS_FOR_EXPORT + +StatisticsRegistry* StatisticsRegistry::current() { + return stats::getStatisticsRegistry(smt::currentSmtEngine()); +} + +void StatisticsRegistry::registerStat(Stat* s) throw(AssertionException) { +#ifdef CVC4_STATISTICS_ON + StatSet& stats = current()->d_stats; + AlwaysAssert(stats.find(s) == stats.end(), + "Statistic `%s' was already registered with this registry.", s->getName().c_str()); + stats.insert(s); +#endif /* CVC4_STATISTICS_ON */ +}/* StatisticsRegistry::registerStat() */ + +void StatisticsRegistry::unregisterStat(Stat* s) throw(AssertionException) { +#ifdef CVC4_STATISTICS_ON + StatSet& stats = current()->d_stats; + AlwaysAssert(stats.find(s) != stats.end(), + "Statistic `%s' was not registered with this registry.", s->getName().c_str()); + stats.erase(s); +#endif /* CVC4_STATISTICS_ON */ +}/* StatisticsRegistry::unregisterStat() */ + +#endif /* ! __BUILDING_STATISTICS_FOR_EXPORT */ + +void StatisticsRegistry::registerStat_(Stat* s) throw(AssertionException) { +#ifdef CVC4_STATISTICS_ON + AlwaysAssert(d_stats.find(s) == d_stats.end()); + d_stats.insert(s); +#endif /* CVC4_STATISTICS_ON */ +}/* StatisticsRegistry::registerStat_() */ + +void StatisticsRegistry::unregisterStat_(Stat* s) throw(AssertionException) { +#ifdef CVC4_STATISTICS_ON + AlwaysAssert(d_stats.find(s) != d_stats.end()); + d_stats.erase(s); +#endif /* CVC4_STATISTICS_ON */ +}/* StatisticsRegistry::unregisterStat_() */ + +void StatisticsRegistry::flushStat(std::ostream &out) const { +#ifdef CVC4_STATISTICS_ON + flushInformation(out); +#endif /* CVC4_STATISTICS_ON */ +} + +void StatisticsRegistry::flushInformation(std::ostream &out) const { +#ifdef CVC4_STATISTICS_ON + this->StatisticsBase::flushInformation(out); +#endif /* CVC4_STATISTICS_ON */ +} + +void TimerStat::start() { + if(__CVC4_USE_STATISTICS) { + AlwaysAssert(!d_running); + clock_gettime(CLOCK_MONOTONIC, &d_start); + d_running = true; + } +}/* TimerStat::start() */ + +void TimerStat::stop() { + if(__CVC4_USE_STATISTICS) { + AlwaysAssert(d_running); + ::timespec end; + clock_gettime(CLOCK_MONOTONIC, &end); + d_data += end - d_start; + d_running = false; + } +}/* TimerStat::stop() */ + +RegisterStatistic::RegisterStatistic(ExprManager& em, Stat* stat) : + d_reg(NodeManager::fromExprManager(&em)->getStatisticsRegistry()), + d_stat(stat) { + d_reg->registerStat_(d_stat); +} + +RegisterStatistic::RegisterStatistic(SmtEngine& smt, Stat* stat) : + d_reg(stats::getStatisticsRegistry(&smt)), + d_stat(stat) { + d_reg->registerStat_(d_stat); +} + +}/* CVC4 namespace */ + +#undef __CVC4_USE_STATISTICS diff --git a/src/util/statistics_registry.h b/src/util/statistics_registry.h new file mode 100644 index 000000000..b2180ab59 --- /dev/null +++ b/src/util/statistics_registry.h @@ -0,0 +1,878 @@ +/********************* */ +/*! \file statistics_registry.h + ** \verbatim + ** Original author: taking + ** Major contributors: mdeters + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009-2012 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Statistics utility classes + ** + ** Statistics utility classes, including classes for holding (and referring + ** to) statistics, the statistics registry, and some other associated + ** classes. + **/ + +#include "cvc4_private_library.h" + +#ifndef __CVC4__STATISTICS_REGISTRY_H +#define __CVC4__STATISTICS_REGISTRY_H + +#include "util/statistics.h" + +#include +#include +#include +#include +#include + +#include "util/Assert.h" + +namespace CVC4 { + +#ifdef CVC4_STATISTICS_ON +# define __CVC4_USE_STATISTICS true +#else +# define __CVC4_USE_STATISTICS false +#endif + +class ExprManager; +class SmtEngine; + +/** + * The base class for all statistics. + * + * This base class keeps the name of the statistic and declares the (pure) + * virtual function flushInformation(). Derived classes must implement + * this function and pass their name to the base class constructor. + * + * This class also (statically) maintains the delimiter used to separate + * the name and the value when statistics are output. + */ +class Stat { +protected: + /** The name of this statistic */ + std::string d_name; + +public: + + /** Nullary constructor, does nothing */ + Stat() { } + + /** + * Construct a statistic with the given name. Debug builds of CVC4 + * will throw an assertion exception if the given name contains the + * statistic delimiter string. + */ + Stat(const std::string& name) throw(CVC4::AssertionException) : + d_name(name) { + if(__CVC4_USE_STATISTICS) { + AlwaysAssert(d_name.find(", ") == std::string::npos); + } + } + + /** Destruct a statistic. This base-class version does nothing. */ + virtual ~Stat() {} + + /** + * Flush the value of this statistic to an output stream. Should + * finish the output with an end-of-line character. + */ + virtual void flushInformation(std::ostream& out) const = 0; + + /** + * Flush the name,value pair of this statistic to an output stream. + * Uses the statistic delimiter string between name and value. + * + * May be redefined by a child class + */ + virtual void flushStat(std::ostream& out) const { + if(__CVC4_USE_STATISTICS) { + out << d_name << ", "; + flushInformation(out); + } + } + + /** Get the name of this statistic. */ + const std::string& getName() const { + return d_name; + } + + /** Get the value of this statistic as a string. */ + virtual SExpr getValue() const { + std::stringstream ss; + flushInformation(ss); + return ss.str(); + } + +};/* class Stat */ + +// A generic way of making a SExpr from templated stats code. +// for example, the uint64_t version ensures that we create +// Integer-SExprs for ReadOnlyDataStats (like those inside +// Minisat) without having to specialize the entire +// ReadOnlyDataStat class template. +template +inline SExpr mkSExpr(const T& x) { + std::stringstream ss; + ss << x; + return ss.str(); +} + +template <> +inline SExpr mkSExpr(const uint64_t& x) { + return Integer(x); +} + +template <> +inline SExpr mkSExpr(const int64_t& x) { + return Integer(x); +} + +template <> +inline SExpr mkSExpr(const int& x) { + return Integer(x); +} + +template <> +inline SExpr mkSExpr(const Integer& x) { + return x; +} + +template <> +inline SExpr mkSExpr(const double& x) { + // roundabout way to get a Rational from a double + std::stringstream ss; + ss << std::fixed << x; + return Rational::fromDecimal(ss.str()); +} + +template <> +inline SExpr mkSExpr(const Rational& x) { + return x; +} + +/** + * A class to represent a "read-only" data statistic of type T. Adds to + * the Stat base class the pure virtual function getData(), which returns + * type T, and flushInformation(), which outputs the statistic value to an + * output stream (using the same existing stream insertion operator). + * + * Template class T must have stream insertion operation defined: + * std::ostream& operator<<(std::ostream&, const T&) + */ +template +class ReadOnlyDataStat : public Stat { +public: + /** The "payload" type of this data statistic (that is, T). */ + typedef T payload_t; + + /** Construct a read-only data statistic with the given name. */ + ReadOnlyDataStat(const std::string& name) : + Stat(name) { + } + + /** Get the value of the statistic. */ + virtual const T& getData() const = 0; + + /** Flush the value of the statistic to the given output stream. */ + void flushInformation(std::ostream& out) const { + if(__CVC4_USE_STATISTICS) { + out << getData(); + } + } + + SExpr getValue() const { + return mkSExpr(getData()); + } + +};/* class ReadOnlyDataStat */ + + +/** + * A data statistic class. This class extends a read-only data statistic + * with assignment (the statistic can be set as well as read). This class + * adds to the read-only case a pure virtual function setData(), thus + * providing the basic interface for a data statistic: getData() to get the + * statistic value, and setData() to set it. + * + * As with the read-only data statistic class, template class T must have + * stream insertion operation defined: + * std::ostream& operator<<(std::ostream&, const T&) + */ +template +class DataStat : public ReadOnlyDataStat { +public: + + /** Construct a data statistic with the given name. */ + DataStat(const std::string& name) : + ReadOnlyDataStat(name) { + } + + /** Set the data statistic. */ + virtual void setData(const T&) = 0; + +};/* class DataStat */ + + +/** + * A data statistic that references a data cell of type T, + * implementing getData() by referencing that memory cell, and + * setData() by reassigning the statistic to point to the new + * data cell. The referenced data cell is kept as a const + * reference, meaning the referenced data is never actually + * modified by this class (it must be externally modified for + * a reference statistic to make sense). A common use for + * this type of statistic is to output a statistic that is kept + * outside the statistics package (for example, one that's kept + * by a theory implementation for internal heuristic purposes, + * which is important to keep even if statistics are turned off). + * + * Template class T must have an assignment operator=(). + */ +template +class ReferenceStat : public DataStat { +private: + /** The referenced data cell */ + const T* d_data; + +public: + /** + * Construct a reference stat with the given name and a reference + * to NULL. + */ + ReferenceStat(const std::string& name) : + DataStat(name), + d_data(NULL) { + } + + /** + * Construct a reference stat with the given name and a reference to + * the given data. + */ + ReferenceStat(const std::string& name, const T& data) : + DataStat(name), + d_data(NULL) { + setData(data); + } + + /** Set this reference statistic to refer to the given data cell. */ + void setData(const T& t) { + if(__CVC4_USE_STATISTICS) { + d_data = &t; + } + } + + /** Get the value of the referenced data cell. */ + const T& getData() const { + if(__CVC4_USE_STATISTICS) { + return *d_data; + } else { + Unreachable(); + } + } + +};/* class ReferenceStat */ + + +/** + * A data statistic that keeps a T and sets it with setData(). + * + * Template class T must have an operator=() and a copy constructor. + */ +template +class BackedStat : public DataStat { +protected: + /** The internally-kept statistic value */ + T d_data; + +public: + + /** Construct a backed statistic with the given name and initial value. */ + BackedStat(const std::string& name, const T& init) : + DataStat(name), + d_data(init) { + } + + /** Set the underlying data value to the given value. */ + void setData(const T& t) { + if(__CVC4_USE_STATISTICS) { + d_data = t; + } + } + + /** Identical to setData(). */ + BackedStat& operator=(const T& t) { + if(__CVC4_USE_STATISTICS) { + d_data = t; + } + return *this; + } + + /** Get the underlying data value. */ + const T& getData() const { + if(__CVC4_USE_STATISTICS) { + return d_data; + } else { + Unreachable(); + } + } + +};/* class BackedStat */ + + +/** + * A wrapper Stat for another Stat. + * + * This type of Stat is useful in cases where a module (like the + * CongruenceClosure module) might keep its own statistics, but might + * be instantiated in many contexts by many clients. This makes such + * a statistic inappopriate to register with the StatisticsRegistry + * directly, as all would be output with the same name (and may be + * unregistered too quickly anyway). A WrappedStat allows the calling + * client (say, TheoryUF) to wrap the Stat from the client module, + * giving it a globally unique name. + */ +template +class WrappedStat : public ReadOnlyDataStat { + typedef typename Stat::payload_t T; + + const ReadOnlyDataStat& d_stat; + + /** Private copy constructor undefined (no copy permitted). */ + WrappedStat(const WrappedStat&) CVC4_UNDEFINED; + /** Private assignment operator undefined (no copy permitted). */ + WrappedStat& operator=(const WrappedStat&) CVC4_UNDEFINED; + +public: + + /** + * Construct a wrapped statistic with the given name that wraps the + * given statistic. + */ + WrappedStat(const std::string& name, const ReadOnlyDataStat& stat) : + ReadOnlyDataStat(name), + d_stat(stat) { + } + + /** Get the data of the underlying (wrapped) statistic. */ + const T& getData() const { + if(__CVC4_USE_STATISTICS) { + return d_stat.getData(); + } else { + Unreachable(); + } + } + + SExpr getValue() const { + return d_stat.getValue(); + } + +};/* class WrappedStat */ + +/** + * A backed integer-valued (64-bit signed) statistic. + * This doesn't functionally differ from its base class BackedStat, + * except for adding convenience functions for dealing with integers. + */ +class IntStat : public BackedStat { +public: + + /** + * Construct an integer-valued statistic with the given name and + * initial value. + */ + IntStat(const std::string& name, int64_t init) : + BackedStat(name, init) { + } + + /** Increment the underlying integer statistic. */ + IntStat& operator++() { + if(__CVC4_USE_STATISTICS) { + ++d_data; + } + return *this; + } + + /** Increment the underlying integer statistic by the given amount. */ + IntStat& operator+=(int64_t val) { + if(__CVC4_USE_STATISTICS) { + d_data += val; + } + return *this; + } + + /** Keep the maximum of the current statistic value and the given one. */ + void maxAssign(int64_t val) { + if(__CVC4_USE_STATISTICS) { + if(d_data < val) { + d_data = val; + } + } + } + + /** Keep the minimum of the current statistic value and the given one. */ + void minAssign(int64_t val) { + if(__CVC4_USE_STATISTICS) { + if(d_data > val) { + d_data = val; + } + } + } + + SExpr getValue() const { + return SExpr(Integer(d_data)); + } + +};/* class IntStat */ + +template +class SizeStat : public Stat { +private: + const T& d_sized; +public: + SizeStat(const std::string&name, const T& sized) : + Stat(name), d_sized(sized) {} + ~SizeStat() {} + + void flushInformation(std::ostream& out) const { + out << d_sized.size(); + } + + SExpr getValue() const { + return SExpr(Integer(d_sized.size())); + } + +};/* class SizeStat */ + +/** + * The value for an AverageStat is the running average of (e1, e_2, ..., e_n), + * (e1 + e_2 + ... + e_n)/n, + * where e_i is an entry added by an addEntry(e_i) call. + * The value is initially always 0. + * (This is to avoid making parsers confused.) + * + * A call to setData() will change the running average but not reset the + * running count, so should generally be avoided. Call addEntry() to add + * an entry to the average calculation. + */ +class AverageStat : public BackedStat { +private: + /** + * The number of accumulations of the running average that we + * have seen so far. + */ + uint32_t d_count; + double d_sum; + +public: + /** Construct an average statistic with the given name. */ + AverageStat(const std::string& name) : + BackedStat(name, 0.0), d_count(0), d_sum(0.0) { + } + + /** Add an entry to the running-average calculation. */ + void addEntry(double e) { + if(__CVC4_USE_STATISTICS) { + ++d_count; + d_sum += e; + setData(d_sum / d_count); + } + } + + SExpr getValue() const { + std::stringstream ss; + ss << d_data; + return SExpr(Rational::fromDecimal(ss.str())); + } + +};/* class AverageStat */ + +/** A statistic that contains a SExpr. */ +class SExprStat : public BackedStat { +public: + + /** + * Construct a SExpr-valued statistic with the given name and + * initial value. + */ + SExprStat(const std::string& name, const SExpr& init) : + BackedStat(name, init) { + } + + SExpr getValue() const { + return d_data; + } + +};/* class SExprStat */ + +template +class ListStat : public Stat { +private: + typedef std::vector List; + List d_list; +public: + + /** + * Construct an integer-valued statistic with the given name and + * initial value. + */ + ListStat(const std::string& name) : Stat(name) {} + ~ListStat() {} + + void flushInformation(std::ostream& out) const{ + if(__CVC4_USE_STATISTICS) { + typename List::const_iterator i = d_list.begin(), end = d_list.end(); + out << "["; + if(i != end){ + out << *i; + ++i; + for(; i != end; ++i){ + out << ", " << *i; + } + } + out << "]"; + } + } + + ListStat& operator<<(const T& val){ + if(__CVC4_USE_STATISTICS) { + d_list.push_back(val); + } + return (*this); + } + +};/* class ListStat */ + +/****************************************************************************/ +/* Statistics Registry */ +/****************************************************************************/ + +/** + * The main statistics registry. This registry maintains the list of + * currently active statistics and is able to "flush" them all. + */ +class StatisticsRegistry : public StatisticsBase, public Stat { +private: + + /** Private copy constructor undefined (no copy permitted). */ + StatisticsRegistry(const StatisticsRegistry&) CVC4_UNDEFINED; + +public: + + /** Construct an nameless statistics registry */ + StatisticsRegistry() {} + + /** Construct a statistics registry */ + StatisticsRegistry(const std::string& name) throw(CVC4::AssertionException) : + Stat(name) { + d_prefix = name; + if(__CVC4_USE_STATISTICS) { + AlwaysAssert(d_name.find(s_regDelim) == std::string::npos); + } + } + + /** + * Set the name of this statistic registry, used as prefix during + * output. (This version overrides StatisticsBase::setPrefix().) + */ + void setPrefix(const std::string& name) { + d_prefix = d_name = name; + } + +#if (defined(__BUILDING_CVC4LIB) || defined(__BUILDING_CVC4LIB_UNIT_TEST)) && !defined(__BUILDING_STATISTICS_FOR_EXPORT) + /** Get a pointer to the current statistics registry */ + static StatisticsRegistry* current(); +#endif /* (__BUILDING_CVC4LIB || __BUILDING_CVC4LIB_UNIT_TEST) && ! __BUILDING_STATISTICS_FOR_EXPORT */ + + /** Overridden to avoid the name being printed */ + void flushStat(std::ostream &out) const; + + virtual void flushInformation(std::ostream& out) const; + + SExpr getValue() const { + std::vector v; + for(StatSet::iterator i = d_stats.begin(); i != d_stats.end(); ++i) { + std::vector w; + w.push_back((*i)->getName()); + w.push_back((*i)->getValue()); + v.push_back(SExpr(w)); + } + return SExpr(v); + } + +#if (defined(__BUILDING_CVC4LIB) || defined(__BUILDING_CVC4LIB_UNIT_TEST)) && !defined(__BUILDING_STATISTICS_FOR_EXPORT) + /** Register a new statistic, making it active. */ + static void registerStat(Stat* s) throw(AssertionException); + + /** Unregister an active statistic, making it inactive. */ + static void unregisterStat(Stat* s) throw(AssertionException); +#endif /* (__BUILDING_CVC4LIB || __BUILDING_CVC4LIB) && ! __BUILDING_STATISTICS_FOR_EXPORT */ + + /** Register a new statistic */ + void registerStat_(Stat* s) throw(AssertionException); + + /** Unregister a new statistic */ + void unregisterStat_(Stat* s) throw(AssertionException); + +};/* class StatisticsRegistry */ + +/****************************************************************************/ +/* Some utility functions for timespec */ +/****************************************************************************/ + +/** Compute the sum of two timespecs. */ +inline timespec& operator+=(timespec& a, const timespec& b) { + // assumes a.tv_nsec and b.tv_nsec are in range + const long nsec_per_sec = 1000000000L; // one thousand million + Assert(a.tv_nsec >= 0 && a.tv_nsec < nsec_per_sec); + Assert(b.tv_nsec >= 0 && b.tv_nsec < nsec_per_sec); + a.tv_sec += b.tv_sec; + long nsec = a.tv_nsec + b.tv_nsec; + Assert(nsec >= 0); + if(nsec < 0) { + nsec += nsec_per_sec; + --a.tv_sec; + } + if(nsec >= nsec_per_sec) { + nsec -= nsec_per_sec; + ++a.tv_sec; + } + Assert(nsec >= 0 && nsec < nsec_per_sec); + a.tv_nsec = nsec; + return a; +} + +/** Compute the difference of two timespecs. */ +inline timespec& operator-=(timespec& a, const timespec& b) { + // assumes a.tv_nsec and b.tv_nsec are in range + const long nsec_per_sec = 1000000000L; // one thousand million + Assert(a.tv_nsec >= 0 && a.tv_nsec < nsec_per_sec); + Assert(b.tv_nsec >= 0 && b.tv_nsec < nsec_per_sec); + a.tv_sec -= b.tv_sec; + long nsec = a.tv_nsec - b.tv_nsec; + if(nsec < 0) { + nsec += nsec_per_sec; + --a.tv_sec; + } + if(nsec >= nsec_per_sec) { + nsec -= nsec_per_sec; + ++a.tv_sec; + } + Assert(nsec >= 0 && nsec < nsec_per_sec); + a.tv_nsec = nsec; + return a; +} + +/** Add two timespecs. */ +inline timespec operator+(const timespec& a, const timespec& b) { + timespec result = a; + return result += b; +} + +/** Subtract two timespecs. */ +inline timespec operator-(const timespec& a, const timespec& b) { + timespec result = a; + return result -= b; +} + +/** Compare two timespecs for equality. */ +inline bool operator==(const timespec& a, const timespec& b) { + // assumes a.tv_nsec and b.tv_nsec are in range + return a.tv_sec == b.tv_sec && a.tv_nsec == b.tv_nsec; +} + +/** Compare two timespecs for disequality. */ +inline bool operator!=(const timespec& a, const timespec& b) { + // assumes a.tv_nsec and b.tv_nsec are in range + return !(a == b); +} + +/** Compare two timespecs, returning true iff a < b. */ +inline bool operator<(const timespec& a, const timespec& b) { + // assumes a.tv_nsec and b.tv_nsec are in range + return a.tv_sec < b.tv_sec || + (a.tv_sec == b.tv_sec && a.tv_nsec < b.tv_nsec); +} + +/** Compare two timespecs, returning true iff a > b. */ +inline bool operator>(const timespec& a, const timespec& b) { + // assumes a.tv_nsec and b.tv_nsec are in range + return a.tv_sec > b.tv_sec || + (a.tv_sec == b.tv_sec && a.tv_nsec > b.tv_nsec); +} + +/** Compare two timespecs, returning true iff a <= b. */ +inline bool operator<=(const timespec& a, const timespec& b) { + // assumes a.tv_nsec and b.tv_nsec are in range + return !(a > b); +} + +/** Compare two timespecs, returning true iff a >= b. */ +inline bool operator>=(const timespec& a, const timespec& b) { + // assumes a.tv_nsec and b.tv_nsec are in range + return !(a < b); +} + +/** Output a timespec on an output stream. */ +inline std::ostream& operator<<(std::ostream& os, const timespec& t) { + // assumes t.tv_nsec is in range + return os << t.tv_sec << "." + << std::setfill('0') << std::setw(8) << std::right << t.tv_nsec; +} + +class CodeTimer; + +/** + * A timer statistic. The timer can be started and stopped + * arbitrarily, like a stopwatch; the value of the statistic at the + * end is the accumulated time over all (start,stop) pairs. + */ +class TimerStat : public BackedStat { + + // strange: timespec isn't placed in 'std' namespace ?! + /** The last start time of this timer */ + timespec d_start; + + /** Whether this timer is currently running */ + bool d_running; + +public: + + typedef CVC4::CodeTimer CodeTimer; + + /** + * Construct a timer statistic with the given name. Newly-constructed + * timers have a 0.0 value and are not running. + */ + TimerStat(const std::string& name) : + BackedStat< timespec >(name, timespec()), + d_running(false) { + /* timespec is POD and so may not be initialized to zero; + * here, ensure it is */ + d_data.tv_sec = d_data.tv_nsec = 0; + } + + /** Start the timer. */ + void start(); + + /** + * Stop the timer and update the statistic value with the + * accumulated time. + */ + void stop(); + + SExpr getValue() const { + std::stringstream ss; + ss << std::fixed << d_data; + return SExpr(Rational::fromDecimal(ss.str())); + } + +};/* class TimerStat */ + + +/** + * Utility class to make it easier to call stop() at the end of a + * code block. When constructed, it starts the timer. When + * destructed, it stops the timer. + */ +class CodeTimer { + TimerStat& d_timer; + + /** Private copy constructor undefined (no copy permitted). */ + CodeTimer(const CodeTimer& timer) CVC4_UNDEFINED; + /** Private assignment operator undefined (no copy permitted). */ + CodeTimer& operator=(const CodeTimer& timer) CVC4_UNDEFINED; + +public: + CodeTimer(TimerStat& timer) : d_timer(timer) { + d_timer.start(); + } + ~CodeTimer() { + d_timer.stop(); + } +};/* class CodeTimer */ + + +/** + * 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::morgan::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) { \ + StatisticsRegistry::registerStat(this); \ + } \ + ~Statistic_##_StatField() { \ + StatisticsRegistry::unregisterStat(this); \ + } \ + } _StatField + +/** + * Resource-acquisition-is-initialization idiom for statistics + * registry. Useful for stack-based statistics (like in the driver). + * Generally, for statistics kept in a member field of class, it's + * better to use the above KEEP_STATISTIC(), which does declaration of + * the member, construction of the statistic, and + * registration/unregistration. This RAII class only does + * registration and unregistration. + */ +class RegisterStatistic { + + StatisticsRegistry* d_reg; + Stat* d_stat; + +public: + +#if (defined(__BUILDING_CVC4LIB) || defined(__BUILDING_CVC4LIB_UNIT_TEST)) && ! defined(__BUILDING_STATISTICS_FOR_EXPORT) + RegisterStatistic(Stat* stat) : + d_reg(StatisticsRegistry::current()), + d_stat(stat) { + Assert(d_reg != NULL, "There is no current statistics registry!"); + StatisticsRegistry::registerStat(d_stat); + } +#endif /* (__BUILDING_CVC4LIB || __BUILDING_CVC4LIB_UNIT_TEST) && ! __BUILDING_STATISTICS_FOR_EXPORT */ + + RegisterStatistic(StatisticsRegistry* reg, Stat* stat) : + d_reg(reg), + d_stat(stat) { + Assert(d_reg != NULL, + "You need to specify a statistics registry" + "on which to set the statistic"); + d_reg->registerStat_(d_stat); + } + + RegisterStatistic(ExprManager& em, Stat* stat); + + RegisterStatistic(SmtEngine& smt, Stat* stat); + + ~RegisterStatistic() { + d_reg->unregisterStat_(d_stat); + } + +};/* class RegisterStatistic */ + +#undef __CVC4_USE_STATISTICS + +}/* CVC4 namespace */ + +#endif /* __CVC4__STATISTICS_REGISTRY_H */ diff --git a/src/util/stats.cpp b/src/util/stats.cpp deleted file mode 100644 index 7ac430da8..000000000 --- a/src/util/stats.cpp +++ /dev/null @@ -1,141 +0,0 @@ -/********************* */ -/*! \file stats.cpp - ** \verbatim - ** Original author: taking - ** Major contributors: mdeters - ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ - -#include "util/stats.h" -#include "expr/node_manager.h" -#include "expr/expr_manager_scope.h" -#include "expr/expr_manager.h" -#include "lib/clock_gettime.h" -#include "smt/smt_engine_scope.h" -#include "smt/smt_engine.h" - -#ifdef CVC4_STATISTICS_ON -# define __CVC4_USE_STATISTICS true -#else -# define __CVC4_USE_STATISTICS false -#endif - -using namespace CVC4; - -std::string Stat::s_delim(","); -std::string StatisticsRegistry::s_regDelim("::"); - -StatisticsRegistry* StatisticsRegistry::current() { - return smt::currentSmtEngine()->getStatisticsRegistry(); -} - -void StatisticsRegistry::registerStat(Stat* s) throw(AssertionException) { -#ifdef CVC4_STATISTICS_ON - StatSet& registeredStats = current()->d_registeredStats; - AlwaysAssert(registeredStats.find(s) == registeredStats.end(), - "Statistic `%s' was already registered with this registry.", s->getName().c_str()); - registeredStats.insert(s); -#endif /* CVC4_STATISTICS_ON */ -}/* StatisticsRegistry::registerStat() */ - -void StatisticsRegistry::registerStat_(Stat* s) throw(AssertionException) { -#ifdef CVC4_STATISTICS_ON - AlwaysAssert(d_registeredStats.find(s) == d_registeredStats.end()); - d_registeredStats.insert(s); -#endif /* CVC4_STATISTICS_ON */ -}/* StatisticsRegistry::registerStat_() */ - -void StatisticsRegistry::unregisterStat(Stat* s) throw(AssertionException) { -#ifdef CVC4_STATISTICS_ON - StatSet& registeredStats = current()->d_registeredStats; - AlwaysAssert(registeredStats.find(s) != registeredStats.end(), - "Statistic `%s' was not registered with this registry.", s->getName().c_str()); - registeredStats.erase(s); -#endif /* CVC4_STATISTICS_ON */ -}/* StatisticsRegistry::unregisterStat() */ - -void StatisticsRegistry::unregisterStat_(Stat* s) throw(AssertionException) { -#ifdef CVC4_STATISTICS_ON - AlwaysAssert(d_registeredStats.find(s) != d_registeredStats.end()); - d_registeredStats.erase(s); -#endif /* CVC4_STATISTICS_ON */ -}/* StatisticsRegistry::unregisterStat_() */ - -void StatisticsRegistry::flushInformation(std::ostream& out) const { -#ifdef CVC4_STATISTICS_ON - for(StatSet::iterator i = d_registeredStats.begin(); - i != d_registeredStats.end(); - ++i) { - Stat* s = *i; - if(d_name != "") { - out << d_name << s_regDelim; - } - s->flushStat(out); - out << std::endl; - } -#endif /* CVC4_STATISTICS_ON */ -}/* StatisticsRegistry::flushInformation() */ - -void StatisticsRegistry::flushStat(std::ostream &out) const {; -#ifdef CVC4_STATISTICS_ON - flushInformation(out); -#endif /* CVC4_STATISTICS_ON */ -} - -StatisticsRegistry::const_iterator StatisticsRegistry::begin_() const { - return d_registeredStats.begin(); -}/* StatisticsRegistry::begin() */ - -StatisticsRegistry::const_iterator StatisticsRegistry::begin() { - return current()->d_registeredStats.begin(); -}/* StatisticsRegistry::begin() */ - -StatisticsRegistry::const_iterator StatisticsRegistry::end_() const { - return d_registeredStats.end(); -}/* StatisticsRegistry::end() */ - -StatisticsRegistry::const_iterator StatisticsRegistry::end() { - return current()->d_registeredStats.end(); -}/* StatisticsRegistry::end() */ - -void TimerStat::start() { - if(__CVC4_USE_STATISTICS) { - AlwaysAssert(!d_running); - clock_gettime(CLOCK_MONOTONIC, &d_start); - d_running = true; - } -}/* TimerStat::start() */ - -void TimerStat::stop() { - if(__CVC4_USE_STATISTICS) { - AlwaysAssert(d_running); - ::timespec end; - clock_gettime(CLOCK_MONOTONIC, &end); - d_data += end - d_start; - d_running = false; - } -}/* TimerStat::stop() */ - -RegisterStatistic::RegisterStatistic(ExprManager& em, Stat* stat) : - d_reg(em.getStatisticsRegistry()), - d_stat(stat) { - d_reg->registerStat_(d_stat); -} - -RegisterStatistic::RegisterStatistic(SmtEngine& smt, Stat* stat) : - d_reg(smt.getStatisticsRegistry()), - d_stat(stat) { - d_reg->registerStat_(d_stat); -} - diff --git a/src/util/stats.h b/src/util/stats.h deleted file mode 100644 index 082bdfeaa..000000000 --- a/src/util/stats.h +++ /dev/null @@ -1,833 +0,0 @@ -/********************* */ -/*! \file stats.h - ** \verbatim - ** Original author: taking - ** Major contributors: mdeters, kshitij - ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief Statistics utility classes - ** - ** Statistics utility classes, including classes for holding (and referring - ** to) statistics, the statistics registry, and some other associated - ** classes. - **/ - -#include "cvc4_public.h" - -#ifndef __CVC4__STATS_H -#define __CVC4__STATS_H - -#include -#include -#include -#include -#include -#include -#include -#include - -#include "util/Assert.h" - -namespace CVC4 { - -#ifdef CVC4_STATISTICS_ON -# define __CVC4_USE_STATISTICS true -#else -# define __CVC4_USE_STATISTICS false -#endif - -class ExprManager; -class SmtEngine; - -class CVC4_PUBLIC Stat; - -/** - * The base class for all statistics. - * - * This base class keeps the name of the statistic and declares the (pure) - * virtual function flushInformation(). Derived classes must implement - * this function and pass their name to the base class constructor. - * - * This class also (statically) maintains the delimiter used to separate - * the name and the value when statistics are output. - */ -class CVC4_PUBLIC Stat { -private: - /** - * The delimiter between name and value to use when outputting a - * statistic. - */ - static std::string s_delim; - -protected: - /** The name of this statistic */ - std::string d_name; - -public: - - /** Nullary constructor, does nothing */ - Stat() { } - - /** - * Construct a statistic with the given name. Debug builds of CVC4 - * will throw an assertion exception if the given name contains the - * statistic delimiter string. - */ - Stat(const std::string& name) throw(CVC4::AssertionException) : - d_name(name) { - if(__CVC4_USE_STATISTICS) { - AlwaysAssert(d_name.find(s_delim) == std::string::npos); - } - } - - /** Destruct a statistic. This base-class version does nothing. */ - virtual ~Stat() {} - - /** - * Flush the value of this statistic to an output stream. Should - * finish the output with an end-of-line character. - */ - virtual void flushInformation(std::ostream& out) const = 0; - - /** - * Flush the name,value pair of this statistic to an output stream. - * Uses the statistic delimiter string between name and value. - * - * May be redefined by a child class - */ - virtual void flushStat(std::ostream& out) const { - if(__CVC4_USE_STATISTICS) { - out << d_name << s_delim; - flushInformation(out); - } - } - - /** Get the name of this statistic. */ - const std::string& getName() const { - return d_name; - } - - /** Get the value of this statistic as a string. */ - std::string getValue() const { - std::stringstream ss; - flushInformation(ss); - return ss.str(); - } - -};/* class Stat */ - -/** - * A class to represent a "read-only" data statistic of type T. Adds to - * the Stat base class the pure virtual function getData(), which returns - * type T, and flushInformation(), which outputs the statistic value to an - * output stream (using the same existing stream insertion operator). - * - * Template class T must have stream insertion operation defined: - * std::ostream& operator<<(std::ostream&, const T&) - */ -template -class CVC4_PUBLIC ReadOnlyDataStat : public Stat { -public: - /** The "payload" type of this data statistic (that is, T). */ - typedef T payload_t; - - /** Construct a read-only data statistic with the given name. */ - ReadOnlyDataStat(const std::string& name) : - Stat(name) { - } - - /** Get the value of the statistic. */ - virtual const T& getData() const = 0; - - /** Flush the value of the statistic to the given output stream. */ - void flushInformation(std::ostream& out) const { - if(__CVC4_USE_STATISTICS) { - out << getData(); - } - } - -};/* class ReadOnlyDataStat */ - - -/** - * A data statistic class. This class extends a read-only data statistic - * with assignment (the statistic can be set as well as read). This class - * adds to the read-only case a pure virtual function setData(), thus - * providing the basic interface for a data statistic: getData() to get the - * statistic value, and setData() to set it. - * - * As with the read-only data statistic class, template class T must have - * stream insertion operation defined: - * std::ostream& operator<<(std::ostream&, const T&) - */ -template -class CVC4_PUBLIC DataStat : public ReadOnlyDataStat { -public: - - /** Construct a data statistic with the given name. */ - DataStat(const std::string& name) : - ReadOnlyDataStat(name) { - } - - /** Set the data statistic. */ - virtual void setData(const T&) = 0; - -};/* class DataStat */ - - -/** - * A data statistic that references a data cell of type T, - * implementing getData() by referencing that memory cell, and - * setData() by reassigning the statistic to point to the new - * data cell. The referenced data cell is kept as a const - * reference, meaning the referenced data is never actually - * modified by this class (it must be externally modified for - * a reference statistic to make sense). A common use for - * this type of statistic is to output a statistic that is kept - * outside the statistics package (for example, one that's kept - * by a theory implementation for internal heuristic purposes, - * which is important to keep even if statistics are turned off). - * - * Template class T must have an assignment operator=(). - */ -template -class CVC4_PUBLIC ReferenceStat : public DataStat { -private: - /** The referenced data cell */ - const T* d_data; - -public: - /** - * Construct a reference stat with the given name and a reference - * to NULL. - */ - ReferenceStat(const std::string& name) : - DataStat(name), - d_data(NULL) { - } - - /** - * Construct a reference stat with the given name and a reference to - * the given data. - */ - ReferenceStat(const std::string& name, const T& data) : - DataStat(name), - d_data(NULL) { - setData(data); - } - - /** Set this reference statistic to refer to the given data cell. */ - void setData(const T& t) { - if(__CVC4_USE_STATISTICS) { - d_data = &t; - } - } - - /** Get the value of the referenced data cell. */ - const T& getData() const { - if(__CVC4_USE_STATISTICS) { - return *d_data; - } else { - Unreachable(); - } - } - -};/* class ReferenceStat */ - - -/** - * A data statistic that keeps a T and sets it with setData(). - * - * Template class T must have an operator=() and a copy constructor. - */ -template -class CVC4_PUBLIC BackedStat : public DataStat { -protected: - /** The internally-kept statistic value */ - T d_data; - -public: - - /** Construct a backed statistic with the given name and initial value. */ - BackedStat(const std::string& name, const T& init) : - DataStat(name), - d_data(init) { - } - - /** Set the underlying data value to the given value. */ - void setData(const T& t) { - if(__CVC4_USE_STATISTICS) { - d_data = t; - } - } - - /** Identical to setData(). */ - BackedStat& operator=(const T& t) { - if(__CVC4_USE_STATISTICS) { - d_data = t; - } - return *this; - } - - /** Get the underlying data value. */ - const T& getData() const { - if(__CVC4_USE_STATISTICS) { - return d_data; - } else { - Unreachable(); - } - } - -};/* class BackedStat */ - - -/** - * A wrapper Stat for another Stat. - * - * This type of Stat is useful in cases where a module (like the - * CongruenceClosure module) might keep its own statistics, but might - * be instantiated in many contexts by many clients. This makes such - * a statistic inappopriate to register with the StatisticsRegistry - * directly, as all would be output with the same name (and may be - * unregistered too quickly anyway). A WrappedStat allows the calling - * client (say, TheoryUF) to wrap the Stat from the client module, - * giving it a globally unique name. - */ -template -class CVC4_PUBLIC WrappedStat : public ReadOnlyDataStat { - typedef typename Stat::payload_t T; - - const ReadOnlyDataStat& d_stat; - - /** Private copy constructor undefined (no copy permitted). */ - WrappedStat(const WrappedStat&) CVC4_UNDEFINED; - /** Private assignment operator undefined (no copy permitted). */ - WrappedStat& operator=(const WrappedStat&) CVC4_UNDEFINED; - -public: - - /** - * Construct a wrapped statistic with the given name that wraps the - * given statistic. - */ - WrappedStat(const std::string& name, const ReadOnlyDataStat& stat) : - ReadOnlyDataStat(name), - d_stat(stat) { - } - - /** Get the data of the underlying (wrapped) statistic. */ - const T& getData() const { - if(__CVC4_USE_STATISTICS) { - return d_stat.getData(); - } else { - Unreachable(); - } - } - -};/* class WrappedStat */ - -/** - * A backed integer-valued (64-bit signed) statistic. - * This doesn't functionally differ from its base class BackedStat, - * except for adding convenience functions for dealing with integers. - */ -class CVC4_PUBLIC IntStat : public BackedStat { -public: - - /** - * Construct an integer-valued statistic with the given name and - * initial value. - */ - IntStat(const std::string& name, int64_t init) : - BackedStat(name, init) { - } - - /** Increment the underlying integer statistic. */ - IntStat& operator++() { - if(__CVC4_USE_STATISTICS) { - ++d_data; - } - return *this; - } - - /** Increment the underlying integer statistic by the given amount. */ - IntStat& operator+=(int64_t val) { - if(__CVC4_USE_STATISTICS) { - d_data+= val; - } - return *this; - } - - /** Keep the maximum of the current statistic value and the given one. */ - void maxAssign(int64_t val) { - if(__CVC4_USE_STATISTICS) { - if(d_data < val) { - d_data = val; - } - } - } - - /** Keep the minimum of the current statistic value and the given one. */ - void minAssign(int64_t val) { - if(__CVC4_USE_STATISTICS) { - if(d_data > val) { - d_data = val; - } - } - } - -};/* class IntStat */ - -template -class SizeStat : public Stat { -private: - const T& d_sized; -public: - SizeStat(const std::string&name, const T& sized) : - Stat(name), d_sized(sized) {} - ~SizeStat() {} - - void flushInformation(std::ostream& out) const { - out<< d_sized.size(); - } - std::string getValue() const { - std::stringstream ss; - flushInformation(ss); - return ss.str(); - } -};/* class SizeStat */ - -/** - * The value for an AverageStat is the running average of (e1, e_2, ..., e_n), - * (e1 + e_2 + ... + e_n)/n, - * where e_i is an entry added by an addEntry(e_i) call. - * The value is initially always 0. - * (This is to avoid making parsers confused.) - * - * A call to setData() will change the running average but not reset the - * running count, so should generally be avoided. Call addEntry() to add - * an entry to the average calculation. - */ -class CVC4_PUBLIC AverageStat : public BackedStat { -private: - /** - * The number of accumulations of the running average that we - * have seen so far. - */ - uint32_t d_count; - double d_sum; - -public: - /** Construct an average statistic with the given name. */ - AverageStat(const std::string& name) : - BackedStat(name, 0.0), d_count(0), d_sum(0.0) { - } - - /** Add an entry to the running-average calculation. */ - void addEntry(double e) { - if(__CVC4_USE_STATISTICS) { - ++d_count; - d_sum += e; - setData(d_sum / d_count); - } - } - -};/* class AverageStat */ - -template -class CVC4_PUBLIC ListStat : public Stat{ -private: - typedef std::vector List; - List d_list; -public: - - /** - * Construct an integer-valued statistic with the given name and - * initial value. - */ - ListStat(const std::string& name) : Stat(name) {} - ~ListStat() {} - - void flushInformation(std::ostream& out) const{ - if(__CVC4_USE_STATISTICS) { - typename List::const_iterator i = d_list.begin(), end = d_list.end(); - out << "["; - if(i != end){ - out << *i; - ++i; - for(; i != end; ++i){ - out << ", " << *i; - } - } - out << "]"; - } - } - - ListStat& operator<<(const T& val){ - if(__CVC4_USE_STATISTICS) { - d_list.push_back(val); - } - return (*this); - } - -};/* class ListStat */ - -/****************************************************************************/ -/* Statistics Registry */ -/****************************************************************************/ - -/** - * The main statistics registry. This registry maintains the list of - * currently active statistics and is able to "flush" them all. - */ -class CVC4_PUBLIC StatisticsRegistry : public Stat { -private: - /** A helper class for comparing two statistics */ - struct StatCmp { - inline bool operator()(const Stat* s1, const Stat* s2) const; - };/* class StatisticsRegistry::StatCmp */ - - /** A type for a set of statistics */ - typedef std::set< Stat*, StatCmp > StatSet; - - /** The set of currently active statistics */ - StatSet d_registeredStats; - - /** Private copy constructor undefined (no copy permitted). */ - StatisticsRegistry(const StatisticsRegistry&) CVC4_UNDEFINED; - - static std::string s_regDelim; -public: - - /** Construct an nameless statistics registry */ - StatisticsRegistry() {} - - /** Construct a statistics registry */ - StatisticsRegistry(const std::string& name) throw(CVC4::AssertionException) : - Stat(name) { - if(__CVC4_USE_STATISTICS) { - AlwaysAssert(d_name.find(s_regDelim) == std::string::npos); - } - } - - /** - * Set the name of this statistic registry, used as prefix during - * output. - * - * TODO: Get rid of this function once we have ability to set the - * name of StatisticsRegistry at creation time. - */ - void setName(const std::string& name) { - d_name = name; - } - - /** An iterator type over a set of statistics */ - typedef StatSet::const_iterator const_iterator; - - /** Get a pointer to the current statistics registry */ - static StatisticsRegistry* current(); - - /** Flush all statistics to the given output stream. */ - void flushInformation(std::ostream& out) const; - - /** Obsolete flushStatistics -- use flushInformation */ - //void flushStatistics(std::ostream& out) const; - - /** Overridden to avoid the name being printed */ - void flushStat(std::ostream &out) const; - - /** Register a new statistic, making it active. */ - static void registerStat(Stat* s) throw(AssertionException); - - /** Register a new statistic */ - void registerStat_(Stat* s) throw(AssertionException); - - /** Unregister an active statistic, making it inactive. */ - static void unregisterStat(Stat* s) throw(AssertionException); - - /** Unregister a new statistic */ - void unregisterStat_(Stat* s) throw(AssertionException); - - /** - * Get an iterator to the beginning of the range of the set of active - * (registered) statistics. - */ - const_iterator begin_() const; - - /** - * Get an iterator to the beginning of the range of the set of active - * (registered) statistics. This version uses the "current" - * statistics registry. - */ - static const_iterator begin(); - - /** - * Get an iterator to the end of the range of the set of active - * (registered) statistics. - */ - const_iterator end_() const; - - /** - * Get an iterator to the end of the range of the set of active - * (registered) statistics. This version uses the "current" - * statistics registry. - */ - static const_iterator end(); - -};/* class StatisticsRegistry */ - -inline bool StatisticsRegistry::StatCmp::operator()(const Stat* s1, - const Stat* s2) const { - return s1->getName() < s2->getName(); -} - -/****************************************************************************/ -/* Some utility functions for timespec */ -/****************************************************************************/ - -/** Compute the sum of two timespecs. */ -inline timespec& operator+=(timespec& a, const timespec& b) { - // assumes a.tv_nsec and b.tv_nsec are in range - const long nsec_per_sec = 1000000000L; // one thousand million - Assert(a.tv_nsec >= 0 && a.tv_nsec < nsec_per_sec); - Assert(b.tv_nsec >= 0 && b.tv_nsec < nsec_per_sec); - a.tv_sec += b.tv_sec; - long nsec = a.tv_nsec + b.tv_nsec; - Assert(nsec >= 0); - if(nsec < 0) { - nsec += nsec_per_sec; - --a.tv_sec; - } - if(nsec >= nsec_per_sec) { - nsec -= nsec_per_sec; - ++a.tv_sec; - } - Assert(nsec >= 0 && nsec < nsec_per_sec); - a.tv_nsec = nsec; - return a; -} - -/** Compute the difference of two timespecs. */ -inline timespec& operator-=(timespec& a, const timespec& b) { - // assumes a.tv_nsec and b.tv_nsec are in range - const long nsec_per_sec = 1000000000L; // one thousand million - Assert(a.tv_nsec >= 0 && a.tv_nsec < nsec_per_sec); - Assert(b.tv_nsec >= 0 && b.tv_nsec < nsec_per_sec); - a.tv_sec -= b.tv_sec; - long nsec = a.tv_nsec - b.tv_nsec; - if(nsec < 0) { - nsec += nsec_per_sec; - --a.tv_sec; - } - if(nsec >= nsec_per_sec) { - nsec -= nsec_per_sec; - ++a.tv_sec; - } - Assert(nsec >= 0 && nsec < nsec_per_sec); - a.tv_nsec = nsec; - return a; -} - -/** Add two timespecs. */ -inline timespec operator+(const timespec& a, const timespec& b) { - timespec result = a; - return result += b; -} - -/** Subtract two timespecs. */ -inline timespec operator-(const timespec& a, const timespec& b) { - timespec result = a; - return result -= b; -} - -/** Compare two timespecs for equality. */ -inline bool operator==(const timespec& a, const timespec& b) { - // assumes a.tv_nsec and b.tv_nsec are in range - return a.tv_sec == b.tv_sec && a.tv_nsec == b.tv_nsec; -} - -/** Compare two timespecs for disequality. */ -inline bool operator!=(const timespec& a, const timespec& b) { - // assumes a.tv_nsec and b.tv_nsec are in range - return !(a == b); -} - -/** Compare two timespecs, returning true iff a < b. */ -inline bool operator<(const timespec& a, const timespec& b) { - // assumes a.tv_nsec and b.tv_nsec are in range - return a.tv_sec < b.tv_sec || - (a.tv_sec == b.tv_sec && a.tv_nsec < b.tv_nsec); -} - -/** Compare two timespecs, returning true iff a > b. */ -inline bool operator>(const timespec& a, const timespec& b) { - // assumes a.tv_nsec and b.tv_nsec are in range - return a.tv_sec > b.tv_sec || - (a.tv_sec == b.tv_sec && a.tv_nsec > b.tv_nsec); -} - -/** Compare two timespecs, returning true iff a <= b. */ -inline bool operator<=(const timespec& a, const timespec& b) { - // assumes a.tv_nsec and b.tv_nsec are in range - return !(a > b); -} - -/** Compare two timespecs, returning true iff a >= b. */ -inline bool operator>=(const timespec& a, const timespec& b) { - // assumes a.tv_nsec and b.tv_nsec are in range - return !(a < b); -} - -/** Output a timespec on an output stream. */ -inline std::ostream& operator<<(std::ostream& os, const timespec& t) CVC4_PUBLIC; -inline std::ostream& operator<<(std::ostream& os, const timespec& t) { - // assumes t.tv_nsec is in range - return os << t.tv_sec << "." - << std::setfill('0') << std::setw(8) << std::right << t.tv_nsec; -} - -class CVC4_PUBLIC CodeTimer; - -/** - * A timer statistic. The timer can be started and stopped - * arbitrarily, like a stopwatch; the value of the statistic at the - * end is the accumulated time over all (start,stop) pairs. - */ -class CVC4_PUBLIC TimerStat : public BackedStat { - - // strange: timespec isn't placed in 'std' namespace ?! - /** The last start time of this timer */ - timespec d_start; - - /** Whether this timer is currently running */ - bool d_running; - -public: - - typedef CVC4::CodeTimer CodeTimer; - - /** - * Construct a timer statistic with the given name. Newly-constructed - * timers have a 0.0 value and are not running. - */ - TimerStat(const std::string& name) : - BackedStat< timespec >(name, timespec()), - d_running(false) { - /* timespec is POD and so may not be initialized to zero; - * here, ensure it is */ - d_data.tv_sec = d_data.tv_nsec = 0; - } - - /** Start the timer. */ - void start(); - - /** - * Stop the timer and update the statistic value with the - * accumulated time. - */ - void stop(); - -};/* class TimerStat */ - - -/** - * Utility class to make it easier to call stop() at the end of a - * code block. When constructed, it starts the timer. When - * destructed, it stops the timer. - */ -class CVC4_PUBLIC CodeTimer { - TimerStat& d_timer; - - /** Private copy constructor undefined (no copy permitted). */ - CodeTimer(const CodeTimer& timer) CVC4_UNDEFINED; - /** Private assignment operator undefined (no copy permitted). */ - CodeTimer& operator=(const CodeTimer& timer) CVC4_UNDEFINED; - -public: - CodeTimer(TimerStat& timer) : d_timer(timer) { - d_timer.start(); - } - ~CodeTimer() { - d_timer.stop(); - } -};/* class CodeTimer */ - - -/** - * 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::morgan::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) { \ - StatisticsRegistry::registerStat(this); \ - } \ - ~Statistic_##_StatField() { \ - StatisticsRegistry::unregisterStat(this); \ - } \ - } _StatField - -/** - * Resource-acquisition-is-initialization idiom for statistics - * registry. Useful for stack-based statistics (like in the driver). - * Generally, for statistics kept in a member field of class, it's - * better to use the above KEEP_STATISTIC(), which does declaration of - * the member, construction of the statistic, and - * registration/unregistration. This RAII class only does - * registration and unregistration. - */ -class CVC4_PUBLIC RegisterStatistic { - StatisticsRegistry* d_reg; - Stat* d_stat; -public: - RegisterStatistic(Stat* stat) : - d_reg(StatisticsRegistry::current()), - d_stat(stat) { - Assert(d_reg != NULL, "There is no current statistics registry!"); - StatisticsRegistry::registerStat(d_stat); - } - - RegisterStatistic(StatisticsRegistry* reg, Stat* stat) : - d_reg(reg), - d_stat(stat) { - Assert(d_reg != NULL, - "You need to specify a statistics registry" - "on which to set the statistic"); - d_reg->registerStat_(d_stat); - } - - RegisterStatistic(ExprManager& em, Stat* stat); - - RegisterStatistic(SmtEngine& smt, Stat* stat); - - ~RegisterStatistic() { - d_reg->unregisterStat_(d_stat); - } - -};/* class RegisterStatistic */ - -#undef __CVC4_USE_STATISTICS - -}/* CVC4 namespace */ - -#endif /* __CVC4__STATS_H */ diff --git a/src/util/stats.i b/src/util/stats.i deleted file mode 100644 index 6f1ef5367..000000000 --- a/src/util/stats.i +++ /dev/null @@ -1,30 +0,0 @@ -%{ -#include "util/stats.h" -%} - -namespace CVC4 { - template class CVC4_PUBLIC BackedStat; - - %template(int64_t_BackedStat) BackedStat; - %template(double_BackedStat) BackedStat; - %template(timespec_BackedStat) BackedStat; -}/* CVC4 namespace */ - -%ignore CVC4::operator<<(std::ostream&, const timespec&); - -%rename(increment) CVC4::IntStat::operator++(); -%rename(plusAssign) CVC4::IntStat::operator+=(int64_t); - -%rename(plusAssign) CVC4::operator+=(timespec&, const timespec&); -%rename(minusAssign) CVC4::operator-=(timespec&, const timespec&); -%rename(plus) CVC4::operator+(const timespec&, const timespec&); -%rename(minus) CVC4::operator-(const timespec&, const timespec&); -%rename(equals) CVC4::operator==(const timespec&, const timespec&); -%ignore CVC4::operator!=(const timespec&, const timespec&); -%rename(less) CVC4::operator<(const timespec&, const timespec&); -%rename(lessEqual) CVC4::operator<=(const timespec&, const timespec&); -%rename(greater) CVC4::operator>(const timespec&, const timespec&); -%rename(greaterEqual) CVC4::operator>=(const timespec&, const timespec&); - -%include "util/stats.h" - diff --git a/test/system/Makefile.am b/test/system/Makefile.am index 836189991..2e1657777 100644 --- a/test/system/Makefile.am +++ b/test/system/Makefile.am @@ -4,7 +4,8 @@ CPLUSPLUS_TESTS = \ boilerplate \ ouroborous \ two_smt_engines \ - smt2_compliance + smt2_compliance \ + statistics if CVC4_BUILD_LIBCOMPAT CPLUSPLUS_TESTS += \ diff --git a/test/system/statistics.cpp b/test/system/statistics.cpp new file mode 100644 index 000000000..d4a958499 --- /dev/null +++ b/test/system/statistics.cpp @@ -0,0 +1,72 @@ +/********************* */ +/*! \file statistics.cpp + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009-2012 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief A simple statistics test for CVC4. + ** + ** This simple test just makes sure that the statistics interface is + ** minimally functional. + **/ + +#include +#include + +#include "expr/expr.h" +#include "smt/smt_engine.h" +#include "util/statistics.h" + +using namespace CVC4; +using namespace std; + +int main() { + ExprManager em; + Options opts; + SmtEngine smt(&em); + smt.setOption("incremental", SExpr("true")); + Expr x = em.mkVar("x", em.integerType()); + Expr y = em.mkVar("y", em.integerType()); + smt.assertFormula(em.mkExpr(kind::GT, em.mkExpr(kind::PLUS, x, y), em.mkConst(Rational(5)))); + Expr q = em.mkExpr(kind::GT, x, em.mkConst(Rational(0))); + Result r = smt.query(q); + + if(r != Result::INVALID) { + exit(1); + } + + Statistics stats = smt.getStatistics(); + for(Statistics::iterator i = stats.begin(); i != stats.end(); ++i) { + cout << "stat " << (*i).first << " is " << (*i).second << endl; + } + + smt.assertFormula(em.mkExpr(kind::LT, y, em.mkConst(Rational(5)))); + r = smt.query(q); + Statistics stats2 = smt.getStatistics(); + bool different = false; + for(Statistics::iterator i = stats2.begin(); i != stats2.end(); ++i) { + cout << "stat1 " << (*i).first << " is " << stats.getStatistic((*i).first) << endl; + cout << "stat2 " << (*i).first << " is " << (*i).second << endl; + if(smt.getStatistic((*i).first) != (*i).second) { + cout << "SMT engine reports different value for statistic " << (*i).first << ": " << smt.getStatistic((*i).first) << endl; + exit(1); + } + different = different || stats.getStatistic((*i).first) != (*i).second; + } + + if(!different) { + cout << "stats are the same! bailing.." << endl; + exit(1); + } + + return r == Result::VALID ? 0 : 1; +} + + diff --git a/test/unit/util/stats_black.h b/test/unit/util/stats_black.h index 7ba88edc6..00dfe98a2 100644 --- a/test/unit/util/stats_black.h +++ b/test/unit/util/stats_black.h @@ -21,7 +21,7 @@ #include #include -#include "util/stats.h" +#include "util/statistics_registry.h" using namespace CVC4; using namespace std;