diff options
65 files changed, 928 insertions, 433 deletions
@@ -2,12 +2,10 @@ The core authors and designers of CVC4 are: Kshitij Bansal <kshitij@cs.nyu.edu>, New York University Clark Barrett <barrett@cs.nyu.edu>, New York University - François Bobot <bobot@lri.fr>, Paris-Sud University + Francois Bobot <bobot@lri.fr>, Paris-Sud University Christopher Conway <cconway@cs.nyu.edu>, New York University Morgan Deters <mdeters@cs.nyu.edu>, New York University - Yeting Ge <yeting@cs.nyu.edu>, New York University Liana Hadarean <lianah@cs.nyu.edu>, New York University - Mina Jeong <mjeong@cs.nyu.edu>, New York University Dejan Jovanovic <dejan@cs.nyu.edu>, New York University Tim King <taking@cs.nyu.edu>, New York University Andrew Reynolds <andrew.j.reynolds@gmail.com>, University of Iowa @@ -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 <map> @@ -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 <string> +#include <iostream> 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 <boost/thread/condition.hpp> #include <boost/exception_ptr.hpp> #include <boost/lexical_cast.hpp> +#include <string> #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<string>(d_threadOptions[i][options::thread_id]); - string smtTag = "SmtEngine thread #" - + boost::lexical_cast<string>(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<ChannelFormat>(sharingChannelSize)); d_channelsIn.push_back (new EmptySharedChannel<ChannelFormat>(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<GetValueCommand*>(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<string>(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<string>(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 <vector> +#include <string> +#include <iostream> +#include <sstream> + 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 <fstream> #include <iostream> #include <new> +#include <unistd.h> #include <stdio.h> #include <unistd.h> @@ -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<Options> threadOpts = parseThreadSpecificOptions(opts); + vector<Options> 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 <string> #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 <string> #include <stdint.h> -#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<SExpr> 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<SExpr> 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<SExpr> 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<Node, Node, NodeHashFunction> 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<Command*, CommandCleanup> 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 <vector> 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 <set> 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 <vector> #include <utility> 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 <queue> 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 <vector> 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 <ext/hash_set> #include <ext/hash_map> 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 <sstream> 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 <ext/hash_set> #include <iostream> 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 <ext/hash_set> #include <iostream> 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 <string> 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 <vector> #include <string> +#include <iomanip> +#include <sstream> #include "util/integer.h" #include "util/rational.h" @@ -151,6 +153,12 @@ public: */ const std::vector<SExpr>& 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>& 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 <typeinfo> + +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 <string> +#include <ostream> +#include <set> +#include <iterator> +#include <utility> + +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<std::string, SExpr> > { + 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/stats.cpp b/src/util/statistics_registry.cpp index 7ac430da8..f2a698a48 100644 --- a/src/util/stats.cpp +++ b/src/util/statistics_registry.cpp @@ -1,11 +1,11 @@ /********************* */ -/*! \file stats.cpp +/*! \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, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** 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 @@ -17,7 +17,7 @@ ** \todo document this file **/ -#include "util/stats.h" +#include "util/statistics_registry.h" #include "expr/node_manager.h" #include "expr/expr_manager_scope.h" #include "expr/expr_manager.h" @@ -31,83 +31,70 @@ # define __CVC4_USE_STATISTICS false #endif -using namespace CVC4; +namespace CVC4 { -std::string Stat::s_delim(","); -std::string StatisticsRegistry::s_regDelim("::"); +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 smt::currentSmtEngine()->getStatisticsRegistry(); + return stats::getStatisticsRegistry(smt::currentSmtEngine()); } void StatisticsRegistry::registerStat(Stat* s) throw(AssertionException) { #ifdef CVC4_STATISTICS_ON - StatSet& registeredStats = current()->d_registeredStats; - AlwaysAssert(registeredStats.find(s) == registeredStats.end(), + StatSet& stats = current()->d_stats; + AlwaysAssert(stats.find(s) == stats.end(), "Statistic `%s' was already registered with this registry.", s->getName().c_str()); - registeredStats.insert(s); + stats.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(), + StatSet& stats = current()->d_stats; + AlwaysAssert(stats.find(s) != stats.end(), "Statistic `%s' was not registered with this registry.", s->getName().c_str()); - registeredStats.erase(s); + stats.erase(s); #endif /* CVC4_STATISTICS_ON */ }/* StatisticsRegistry::unregisterStat() */ -void StatisticsRegistry::unregisterStat_(Stat* s) throw(AssertionException) { +#endif /* ! __BUILDING_STATISTICS_FOR_EXPORT */ + +void StatisticsRegistry::registerStat_(Stat* s) throw(AssertionException) { #ifdef CVC4_STATISTICS_ON - AlwaysAssert(d_registeredStats.find(s) != d_registeredStats.end()); - d_registeredStats.erase(s); + AlwaysAssert(d_stats.find(s) == d_stats.end()); + d_stats.insert(s); #endif /* CVC4_STATISTICS_ON */ -}/* StatisticsRegistry::unregisterStat_() */ +}/* StatisticsRegistry::registerStat_() */ -void StatisticsRegistry::flushInformation(std::ostream& out) const { +void StatisticsRegistry::unregisterStat_(Stat* s) throw(AssertionException) { #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; - } + AlwaysAssert(d_stats.find(s) != d_stats.end()); + d_stats.erase(s); #endif /* CVC4_STATISTICS_ON */ -}/* StatisticsRegistry::flushInformation() */ +}/* StatisticsRegistry::unregisterStat_() */ -void StatisticsRegistry::flushStat(std::ostream &out) const {; +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 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) { @@ -128,14 +115,17 @@ void TimerStat::stop() { }/* TimerStat::stop() */ RegisterStatistic::RegisterStatistic(ExprManager& em, Stat* stat) : - d_reg(em.getStatisticsRegistry()), + d_reg(NodeManager::fromExprManager(&em)->getStatisticsRegistry()), d_stat(stat) { d_reg->registerStat_(d_stat); } RegisterStatistic::RegisterStatistic(SmtEngine& smt, Stat* stat) : - d_reg(smt.getStatisticsRegistry()), + d_reg(stats::getStatisticsRegistry(&smt)), d_stat(stat) { d_reg->registerStat_(d_stat); } +}/* CVC4 namespace */ + +#undef __CVC4_USE_STATISTICS diff --git a/src/util/stats.h b/src/util/statistics_registry.h index 082bdfeaa..b2180ab59 100644 --- a/src/util/stats.h +++ b/src/util/statistics_registry.h @@ -1,11 +1,11 @@ /********************* */ -/*! \file stats.h +/*! \file statistics_registry.h ** \verbatim ** Original author: taking - ** Major contributors: mdeters, kshitij + ** 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) + ** 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 @@ -18,16 +18,15 @@ ** classes. **/ -#include "cvc4_public.h" +#include "cvc4_private_library.h" -#ifndef __CVC4__STATS_H -#define __CVC4__STATS_H +#ifndef __CVC4__STATISTICS_REGISTRY_H +#define __CVC4__STATISTICS_REGISTRY_H + +#include "util/statistics.h" -#include <string> -#include <ostream> #include <sstream> #include <iomanip> -#include <set> #include <ctime> #include <vector> #include <stdint.h> @@ -45,8 +44,6 @@ namespace CVC4 { class ExprManager; class SmtEngine; -class CVC4_PUBLIC Stat; - /** * The base class for all statistics. * @@ -57,14 +54,7 @@ class CVC4_PUBLIC Stat; * 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; - +class Stat { protected: /** The name of this statistic */ std::string d_name; @@ -82,7 +72,7 @@ public: Stat(const std::string& name) throw(CVC4::AssertionException) : d_name(name) { if(__CVC4_USE_STATISTICS) { - AlwaysAssert(d_name.find(s_delim) == std::string::npos); + AlwaysAssert(d_name.find(", ") == std::string::npos); } } @@ -103,7 +93,7 @@ public: */ virtual void flushStat(std::ostream& out) const { if(__CVC4_USE_STATISTICS) { - out << d_name << s_delim; + out << d_name << ", "; flushInformation(out); } } @@ -114,7 +104,7 @@ public: } /** Get the value of this statistic as a string. */ - std::string getValue() const { + virtual SExpr getValue() const { std::stringstream ss; flushInformation(ss); return ss.str(); @@ -122,6 +112,51 @@ public: };/* 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 <class T> +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 @@ -132,7 +167,7 @@ public: * std::ostream& operator<<(std::ostream&, const T&) */ template <class T> -class CVC4_PUBLIC ReadOnlyDataStat : public Stat { +class ReadOnlyDataStat : public Stat { public: /** The "payload" type of this data statistic (that is, T). */ typedef T payload_t; @@ -152,6 +187,10 @@ public: } } + SExpr getValue() const { + return mkSExpr(getData()); + } + };/* class ReadOnlyDataStat<T> */ @@ -167,7 +206,7 @@ public: * std::ostream& operator<<(std::ostream&, const T&) */ template <class T> -class CVC4_PUBLIC DataStat : public ReadOnlyDataStat<T> { +class DataStat : public ReadOnlyDataStat<T> { public: /** Construct a data statistic with the given name. */ @@ -197,7 +236,7 @@ public: * Template class T must have an assignment operator=(). */ template <class T> -class CVC4_PUBLIC ReferenceStat : public DataStat<T> { +class ReferenceStat : public DataStat<T> { private: /** The referenced data cell */ const T* d_data; @@ -247,7 +286,7 @@ public: * Template class T must have an operator=() and a copy constructor. */ template <class T> -class CVC4_PUBLIC BackedStat : public DataStat<T> { +class BackedStat : public DataStat<T> { protected: /** The internally-kept statistic value */ T d_data; @@ -300,7 +339,7 @@ public: * giving it a globally unique name. */ template <class Stat> -class CVC4_PUBLIC WrappedStat : public ReadOnlyDataStat<typename Stat::payload_t> { +class WrappedStat : public ReadOnlyDataStat<typename Stat::payload_t> { typedef typename Stat::payload_t T; const ReadOnlyDataStat<T>& d_stat; @@ -330,6 +369,10 @@ public: } } + SExpr getValue() const { + return d_stat.getValue(); + } + };/* class WrappedStat<T> */ /** @@ -337,7 +380,7 @@ public: * This doesn't functionally differ from its base class BackedStat<int64_t>, * except for adding convenience functions for dealing with integers. */ -class CVC4_PUBLIC IntStat : public BackedStat<int64_t> { +class IntStat : public BackedStat<int64_t> { public: /** @@ -359,7 +402,7 @@ public: /** Increment the underlying integer statistic by the given amount. */ IntStat& operator+=(int64_t val) { if(__CVC4_USE_STATISTICS) { - d_data+= val; + d_data += val; } return *this; } @@ -382,6 +425,10 @@ public: } } + SExpr getValue() const { + return SExpr(Integer(d_data)); + } + };/* class IntStat */ template <class T> @@ -394,13 +441,13 @@ public: ~SizeStat() {} void flushInformation(std::ostream& out) const { - out<< d_sized.size(); + out << d_sized.size(); } - std::string getValue() const { - std::stringstream ss; - flushInformation(ss); - return ss.str(); + + SExpr getValue() const { + return SExpr(Integer(d_sized.size())); } + };/* class SizeStat */ /** @@ -414,7 +461,7 @@ public: * running count, so should generally be avoided. Call addEntry() to add * an entry to the average calculation. */ -class CVC4_PUBLIC AverageStat : public BackedStat<double> { +class AverageStat : public BackedStat<double> { private: /** * The number of accumulations of the running average that we @@ -438,10 +485,34 @@ public: } } + 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<SExpr> { +public: + + /** + * Construct a SExpr-valued statistic with the given name and + * initial value. + */ + SExprStat(const std::string& name, const SExpr& init) : + BackedStat<SExpr>(name, init) { + } + + SExpr getValue() const { + return d_data; + } + +};/* class SExprStat */ + template <class T> -class CVC4_PUBLIC ListStat : public Stat{ +class ListStat : public Stat { private: typedef std::vector<T> List; List d_list; @@ -486,23 +557,12 @@ public: * 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 { +class StatisticsRegistry : public StatisticsBase, 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 */ @@ -511,82 +571,57 @@ public: /** 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. - * - * TODO: Get rid of this function once we have ability to set the - * name of StatisticsRegistry at creation time. + * output. (This version overrides StatisticsBase::setPrefix().) */ - void setName(const std::string& name) { - d_name = name; + void setPrefix(const std::string& name) { + d_prefix = d_name = name; } - /** An iterator type over a set of statistics */ - typedef StatSet::const_iterator const_iterator; - +#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(); - - /** Flush all statistics to the given output stream. */ - void flushInformation(std::ostream& out) const; - - /** Obsolete flushStatistics -- use flushInformation */ - //void flushStatistics(std::ostream& out) const; +#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<SExpr> v; + for(StatSet::iterator i = d_stats.begin(); i != d_stats.end(); ++i) { + std::vector<SExpr> 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); - /** Register a new statistic */ - 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); - /** - * 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 */ /****************************************************************************/ @@ -685,21 +720,20 @@ inline bool operator>=(const timespec& a, const timespec& 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; +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 CVC4_PUBLIC TimerStat : public BackedStat<timespec> { +class TimerStat : public BackedStat<timespec> { // strange: timespec isn't placed in 'std' namespace ?! /** The last start time of this timer */ @@ -733,6 +767,12 @@ public: */ void stop(); + SExpr getValue() const { + std::stringstream ss; + ss << std::fixed << d_data; + return SExpr(Rational::fromDecimal(ss.str())); + } + };/* class TimerStat */ @@ -741,7 +781,7 @@ public: * code block. When constructed, it starts the timer. When * destructed, it stops the timer. */ -class CVC4_PUBLIC CodeTimer { +class CodeTimer { TimerStat& d_timer; /** Private copy constructor undefined (no copy permitted). */ @@ -796,16 +836,21 @@ public: * registration/unregistration. This RAII class only does * registration and unregistration. */ -class CVC4_PUBLIC RegisterStatistic { +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), @@ -830,4 +875,4 @@ public: }/* CVC4 namespace */ -#endif /* __CVC4__STATS_H */ +#endif /* __CVC4__STATISTICS_REGISTRY_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 T> class CVC4_PUBLIC BackedStat; - - %template(int64_t_BackedStat) BackedStat<int64_t>; - %template(double_BackedStat) BackedStat<double>; - %template(timespec_BackedStat) BackedStat<timespec>; -}/* 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 <iostream> +#include <sstream> + +#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 <string> #include <ctime> -#include "util/stats.h" +#include "util/statistics_registry.h" using namespace CVC4; using namespace std; |