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.)
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
*** 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
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
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)
*** 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
svninfo
EXTRA_DIST = \
+ include/cvc4_private_library.h \
include/cvc4parser_private.h \
include/cvc4parser_public.h \
include/cvc4_private.h \
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) {
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
/***************************************************************************/
//! Get statistics object
- virtual Statistics& getStatistics();
+ virtual Statistics getStatistics();
//! Print collected statistics to stdout
virtual void printStatistics();
#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>
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 {
#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}
// 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 {
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);
#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"
** 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.
--- /dev/null
+/********************* */
+/*! \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 */
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
libmain.a \
@builddir@/../parser/libcvc4parser.la \
@builddir@/../libcvc4.la \
+ @builddir@/../util/libstatistics.la \
@builddir@/../lib/libreplacements.la \
$(READLINE_LIBS)
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)
return !cmd->fail();
}
-}/*main namespace*/
-}/*CVC4 namespace*/
+}/* CVC4::main namespace */
+}/* CVC4 namespace */
#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 {
ExprManager& d_exprMgr;
SmtEngine d_smtEngine;
Options& d_options;
+ StatisticsRegistry d_stats;
public:
// Note: though the options are not cached (instead a reference is
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);
#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"
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()
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));
}
/* 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) {
}
}
}
-}
+}/* CommandExecutorPortfolio::lemmaSharingInit() */
void CommandExecutorPortfolio::lemmaSharingCleanup()
{
d_ostringstreams.clear();
}
-}
+}/* CommandExecutorPortfolio::lemmaSharingCleanup() */
+
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);
*d_options[options::out]
<< d_ostringstreams[portfolioReturn.first]->str();
}
-
+
/* cleanup this check sat specific stuff */
lemmaSharingCleanup();
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 */
#include "main/command_executor.h"
#include "main/portfolio_util.h"
+#include <vector>
+#include <string>
+#include <iostream>
+#include <sstream>
+
namespace CVC4 {
class CommandSequence;
~CommandExecutorPortfolio();
std::string getSmtEngineStatus();
+
+ void flushStatistics(std::ostream& out) const;
+
protected:
bool doCommandSingleton(Command* cmd);
private:
#include <fstream>
#include <iostream>
#include <new>
+#include <unistd.h>
#include <stdio.h>
#include <unistd.h>
#include "util/output.h"
#include "util/dump.h"
#include "util/result.h"
-#include "util/stats.h"
using namespace std;
using 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) {
# 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] != "" ) {
}
// 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;
replayParser->useDeclarationsFrom(shell.getParser());
}
while((cmd = shell.readCommand())) {
- status = cmdExecutor->doCommand(cmd) && status;
+ status = cmdExecutor.doCommand(cmd) && status;
delete cmd;
}
} else {
delete cmd;
break;
}
- status = cmdExecutor->doCommand(cmd);
+ status = cmdExecutor.doCommand(cmd);
delete cmd;
}
// Remove the parser
int returnValue;
string result = "unknown";
if(status) {
- result = cmdExecutor->getSmtEngineStatus();
+ result = cmdExecutor.getSmtEngineStatus();
if(result == "sat") {
returnValue = 10;
}
#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;
}
#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"
#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;
*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);
#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"
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.
#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;
/** 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();
}
/** 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();
}
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 {
} 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 */
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 {
}
#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 */
}
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 {
}
#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 */
"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 */
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()) {
#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 {
#include <string>
#include <stdint.h>
-#include "util/stats.h"
+#include "util/statistics_registry.h"
#include "context/cdlist.h"
#include "prop/sat_solver_types.h"
#define __CVC4_USE_MINISAT
#include "theory/theory.h"
-#include "util/stats.h"
+#include "util/statistics_registry.h"
#include "context/cdqueue.h"
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
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)
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;
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;
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;
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;
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
if (assertionNew == assertion) {
break;
}
- ++d_smt.d_numConstantProps;
+ ++d_smt.d_stats->d_numConstantProps;
assertion = Rewriter::rewrite(assertionNew);
}
s.insert(assertion);
if (learnedNew == learned) {
break;
}
- ++d_smt.d_numConstantProps;
+ ++d_smt.d_stats->d_numConstantProps;
learned = Rewriter::rewrite(learnedNew);
}
if (s.find(learned) != s.end()) {
}
-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;
}
-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);
// 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) {
{
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] =
{
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()) {
{
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) {
// 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]);
}
// 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.
//
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 ){
#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)
class Command;
+class SmtEngine;
class DecisionEngine;
class TheoryEngine;
*/
class DefinedFunction;
+ class SmtEngineStatistics;
class SmtEnginePrivate;
class SmtScope;
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()?
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;
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
}
/**
- * 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;
#include "theory/arith/matrix.h"
#include "theory/arith/partial_model.h"
-#include "util/stats.h"
+#include "util/statistics_registry.h"
#include <vector>
#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>
#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 {
#include "theory/arith/partial_model.h"
#include "util/rational.h"
-#include "util/stats.h"
+#include "util/statistics_registry.h"
#include <vector>
#include <utility>
#include "theory/arith/matrix.h"
#include "theory/arith/constraint.h"
-#include "util/stats.h"
+#include "util/statistics_registry.h"
namespace CVC4 {
namespace theory {
#include "util/dense_map.h"
#include "options/options.h"
-#include "util/stats.h"
+#include "util/statistics_registry.h"
#include "util/result.h"
#include <queue>
#include "theory/arith/constraint.h"
-#include "util/stats.h"
+#include "util/statistics_registry.h"
#include "util/result.h"
#include <vector>
#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 {
#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>
#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"
#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"
#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"
#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>
#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 {
#include "theory/quantifiers_engine.h"
-#include "util/stats.h"
+#include "util/statistics_registry.h"
namespace CVC4 {
namespace theory {
#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"
#include "theory/theory.h"
#include "util/hash.h"
-#include "util/stats.h"
+#include "util/statistics_registry.h"
#include <ext/hash_set>
#include <iostream>
#include "theory/quantifiers_engine.h"
-#include "util/stats.h"
+#include "util/statistics_registry.h"
namespace CVC4 {
namespace theory {
}
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 ){
#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>
#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"
#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 {
#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>
#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"
#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"
#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 {
#include "expr/node.h"
#include "expr/node_builder.h"
-#include "util/stats.h"
+#include "util/statistics_registry.h"
namespace CVC4 {
namespace theory {
#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"
#include "context/context_mm.h"
#include "context/cdchunk_list.h"
-#include "util/stats.h"
+#include "util/statistics_registry.h"
namespace CVC4 {
namespace theory {
-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
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 \
libutil_la_LIBADD = \
@builddir@/libutilcudd.la
+
+libstatistics_la_SOURCES = \
+ statistics_registry.h \
+ statistics_registry.cpp
+
libutilcudd_la_SOURCES = \
propositional_query.h \
propositional_query.cpp
integer.h.in \
tls.h.in \
integer.i \
- stats.i \
+ statistics.i \
bool.i \
sexpr.i \
datatype.i \
#include <vector>
#include <string>
+#include <iomanip>
+#include <sstream>
#include "util/integer.h"
#include "util/rational.h"
*/
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 {
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;
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 */
--- /dev/null
+/********************* */
+/*! \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 */
--- /dev/null
+/********************* */
+/*! \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 */
--- /dev/null
+%{
+#include "util/statistics.h"
+%}
+
+%include "util/statistics.h"
+
--- /dev/null
+/********************* */
+/*! \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
--- /dev/null
+/********************* */
+/*! \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 <sstream>
+#include <iomanip>
+#include <ctime>
+#include <vector>
+#include <stdint.h>
+
+#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 <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
+ * 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 T>
+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<T> */
+
+
+/**
+ * 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 T>
+class DataStat : public ReadOnlyDataStat<T> {
+public:
+
+ /** Construct a data statistic with the given name. */
+ DataStat(const std::string& name) :
+ ReadOnlyDataStat<T>(name) {
+ }
+
+ /** Set the data statistic. */
+ virtual void setData(const T&) = 0;
+
+};/* class DataStat<T> */
+
+
+/**
+ * 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 T>
+class ReferenceStat : public DataStat<T> {
+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<T>(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<T>(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<T> */
+
+
+/**
+ * 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 T>
+class BackedStat : public DataStat<T> {
+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<T>(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<T>& 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<T> */
+
+
+/**
+ * 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 Stat>
+class WrappedStat : public ReadOnlyDataStat<typename Stat::payload_t> {
+ typedef typename Stat::payload_t T;
+
+ const ReadOnlyDataStat<T>& d_stat;
+
+ /** Private copy constructor undefined (no copy permitted). */
+ WrappedStat(const WrappedStat&) CVC4_UNDEFINED;
+ /** Private assignment operator undefined (no copy permitted). */
+ WrappedStat<T>& 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<T>& stat) :
+ ReadOnlyDataStat<T>(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<T> */
+
+/**
+ * A backed integer-valued (64-bit signed) statistic.
+ * This doesn't functionally differ from its base class BackedStat<int64_t>,
+ * except for adding convenience functions for dealing with integers.
+ */
+class IntStat : public BackedStat<int64_t> {
+public:
+
+ /**
+ * Construct an integer-valued statistic with the given name and
+ * initial value.
+ */
+ IntStat(const std::string& name, int64_t init) :
+ BackedStat<int64_t>(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 T>
+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<double> {
+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<double>(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<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 ListStat : public Stat {
+private:
+ typedef std::vector<T> 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<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);
+
+ /** 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<timespec> {
+
+ // 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 */
+++ /dev/null
-/********************* */
-/*! \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);
-}
-
+++ /dev/null
-/********************* */
-/*! \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 <string>
-#include <ostream>
-#include <sstream>
-#include <iomanip>
-#include <set>
-#include <ctime>
-#include <vector>
-#include <stdint.h>
-
-#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 T>
-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<T> */
-
-
-/**
- * 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 T>
-class CVC4_PUBLIC DataStat : public ReadOnlyDataStat<T> {
-public:
-
- /** Construct a data statistic with the given name. */
- DataStat(const std::string& name) :
- ReadOnlyDataStat<T>(name) {
- }
-
- /** Set the data statistic. */
- virtual void setData(const T&) = 0;
-
-};/* class DataStat<T> */
-
-
-/**
- * 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 T>
-class CVC4_PUBLIC ReferenceStat : public DataStat<T> {
-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<T>(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<T>(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<T> */
-
-
-/**
- * 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 T>
-class CVC4_PUBLIC BackedStat : public DataStat<T> {
-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<T>(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<T>& 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<T> */
-
-
-/**
- * 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 Stat>
-class CVC4_PUBLIC WrappedStat : public ReadOnlyDataStat<typename Stat::payload_t> {
- typedef typename Stat::payload_t T;
-
- const ReadOnlyDataStat<T>& d_stat;
-
- /** Private copy constructor undefined (no copy permitted). */
- WrappedStat(const WrappedStat&) CVC4_UNDEFINED;
- /** Private assignment operator undefined (no copy permitted). */
- WrappedStat<T>& 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<T>& stat) :
- ReadOnlyDataStat<T>(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<T> */
-
-/**
- * A backed integer-valued (64-bit signed) statistic.
- * 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> {
-public:
-
- /**
- * Construct an integer-valued statistic with the given name and
- * initial value.
- */
- IntStat(const std::string& name, int64_t init) :
- BackedStat<int64_t>(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 T>
-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<double> {
-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<double>(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 T>
-class CVC4_PUBLIC ListStat : public Stat{
-private:
- typedef std::vector<T> 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<timespec> {
-
- // 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 */
+++ /dev/null
-%{
-#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"
-
boilerplate \
ouroborous \
two_smt_engines \
- smt2_compliance
+ smt2_compliance \
+ statistics
if CVC4_BUILD_LIBCOMPAT
CPLUSPLUS_TESTS += \
--- /dev/null
+/********************* */
+/*! \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;
+}
+
+
#include <string>
#include <ctime>
-#include "util/stats.h"
+#include "util/statistics_registry.h"
using namespace CVC4;
using namespace std;
projects / cvc5.git / commitdiff