diff options
Diffstat (limited to 'src/base')
-rw-r--r-- | src/base/Makefile.am | 44 | ||||
-rw-r--r-- | src/base/configuration.cpp | 293 | ||||
-rw-r--r-- | src/base/configuration.h | 135 | ||||
-rw-r--r-- | src/base/configuration.i | 7 | ||||
-rw-r--r-- | src/base/configuration_private.h | 164 | ||||
-rw-r--r-- | src/base/exception.cpp | 2 | ||||
-rw-r--r-- | src/base/exception.h | 6 | ||||
-rw-r--r-- | src/base/listener.cpp | 39 | ||||
-rw-r--r-- | src/base/listener.h | 112 | ||||
-rwxr-xr-x | src/base/mktagheaders | 24 | ||||
-rwxr-xr-x | src/base/mktags | 35 | ||||
-rw-r--r-- | src/base/output.h | 24 |
12 files changed, 847 insertions, 38 deletions
diff --git a/src/base/Makefile.am b/src/base/Makefile.am index f2fe3f306..bda063176 100644 --- a/src/base/Makefile.am +++ b/src/base/Makefile.am @@ -15,6 +15,9 @@ noinst_LTLIBRARIES = libbase.la libbase_la_SOURCES = \ Makefile.am \ Makefile.in \ + configuration.cpp \ + configuration.h \ + configuration_private.h \ cvc4_assert.cpp \ cvc4_assert.h \ exception.cpp \ @@ -30,11 +33,52 @@ libbase_la_SOURCES = \ BUILT_SOURCES = \ tls.h +# listing {Debug,Trace}_tags too ensures that make doesn't auto-remove it +# after building (if it does, we don't get the "cached" effect with +# the .tmp files below, and we have to re-compile and re-link each +# time, even when there are no changes). +BUILT_SOURCES += \ + Debug_tags.h \ + Debug_tags \ + Trace_tags.h \ + Trace_tags + +MOSTLYCLEANFILES = \ + Debug_tags \ + Trace_tags \ + Debug_tags.tmp \ + Trace_tags.tmp \ + Debug_tags.h \ + Trace_tags.h + EXTRA_DIST = \ + configuration.i \ exception.i \ + mktagheaders \ + mktags \ modal_exception.i \ tls.h.in DISTCLEANFILES = \ tls.h.tmp \ tls.h + +%_tags.h: %_tags mktagheaders + $(AM_V_at)chmod +x @srcdir@/mktagheaders + $(AM_V_GEN)( @srcdir@/mktagheaders "$<" "$<" ) >"$@" + +# This .tmp business is to keep from having to re-compile options.cpp +# (and then re-link the libraries) if nothing has changed. +%_tags: %_tags.tmp + $(AM_V_GEN)\ + diff -q "$^" "$@" &>/dev/null || mv "$^" "$@" || true +# .PHONY ensures the .tmp version is always rebuilt (to check for any changes) +.PHONY: Debug_tags.tmp Trace_tags.tmp +# The "sed" invocation below is particularly obnoxious, but it works around +# inconsistencies in REs on different platforms, using only a basic regular +# expression (no |, no \<, ...). +Debug_tags.tmp Trace_tags.tmp: mktags + $(AM_V_at)chmod +x @srcdir@/mktags + $(AM_V_GEN)(@srcdir@/mktags \ + '$(@:_tags.tmp=)' \ + "$$(find @srcdir@/../ -name '*.cpp' -o -name '*.h' -o -name '*.cc' -o -name '*.g')") >"$@" diff --git a/src/base/configuration.cpp b/src/base/configuration.cpp new file mode 100644 index 000000000..c3ba39075 --- /dev/null +++ b/src/base/configuration.cpp @@ -0,0 +1,293 @@ +/********************* */ +/*! \file configuration.cpp + ** \verbatim + ** Original author: Morgan Deters + ** Major contributors: none + ** Minor contributors (to current version): Liana Hadarean, Tim King, ACSYS, Christopher L. Conway, Dejan Jovanovic, Francois Bobot + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Implementation of Configuration class, which provides compile-time + ** configuration information about the CVC4 library + ** + ** Implementation of Configuration class, which provides compile-time + ** configuration information about the CVC4 library. + **/ +#include "base/configuration.h" + +#include <stdlib.h> +#include <string.h> + +#include <sstream> +#include <string> + +#include "cvc4autoconfig.h" +#include "base/configuration_private.h" + +#if defined(CVC4_DEBUG) && defined(CVC4_TRACING) +# include "base/Debug_tags.h" +#endif /* CVC4_DEBUG && CVC4_TRACING */ + +#ifdef CVC4_TRACING +# include "base/Trace_tags.h" +#endif /* CVC4_TRACING */ + +using namespace std; + +namespace CVC4 { + +string Configuration::getName() { + return PACKAGE_NAME; +} + +bool Configuration::isDebugBuild() { + return IS_DEBUG_BUILD; +} + +bool Configuration::isStatisticsBuild() { + return IS_STATISTICS_BUILD; +} + +bool Configuration::isReplayBuild() { + return IS_REPLAY_BUILD; +} + +bool Configuration::isTracingBuild() { + return IS_TRACING_BUILD; +} + +bool Configuration::isDumpingBuild() { + return IS_DUMPING_BUILD; +} + +bool Configuration::isMuzzledBuild() { + return IS_MUZZLED_BUILD; +} + +bool Configuration::isAssertionBuild() { + return IS_ASSERTIONS_BUILD; +} + +bool Configuration::isProofBuild() { + return IS_PROOFS_BUILD; +} + +bool Configuration::isCoverageBuild() { + return IS_COVERAGE_BUILD; +} + +bool Configuration::isProfilingBuild() { + return IS_PROFILING_BUILD; +} + +bool Configuration::isCompetitionBuild() { + return IS_COMPETITION_BUILD; +} + +string Configuration::getPackageName() { + return PACKAGE_NAME; +} + +string Configuration::getVersionString() { + return CVC4_RELEASE_STRING; +} + +unsigned Configuration::getVersionMajor() { + return CVC4_MAJOR; +} + +unsigned Configuration::getVersionMinor() { + return CVC4_MINOR; +} + +unsigned Configuration::getVersionRelease() { + return CVC4_RELEASE; +} + +std::string Configuration::getVersionExtra() { + return CVC4_EXTRAVERSION; +} + +std::string Configuration::about() { + return CVC4_ABOUT_STRING; +} + +bool Configuration::licenseIsGpl() { + return IS_GPL_BUILD; +} + +bool Configuration::isBuiltWithGmp() { + return IS_GMP_BUILD; +} + +bool Configuration::isBuiltWithCln() { + return IS_CLN_BUILD; +} + +bool Configuration::isBuiltWithGlpk() { + return IS_GLPK_BUILD; +} + +bool Configuration::isBuiltWithAbc() { + return IS_ABC_BUILD; +} + +bool Configuration::isBuiltWithReadline() { + return IS_READLINE_BUILD; +} + +bool Configuration::isBuiltWithCudd() { + return false; +} + +bool Configuration::isBuiltWithTlsSupport() { + return USING_TLS; +} + +unsigned Configuration::getNumDebugTags() { +#if defined(CVC4_DEBUG) && defined(CVC4_TRACING) + /* -1 because a NULL pointer is inserted as the last value */ + return (sizeof(Debug_tags) / sizeof(Debug_tags[0])) - 1; +#else /* CVC4_DEBUG && CVC4_TRACING */ + return 0; +#endif /* CVC4_DEBUG && CVC4_TRACING */ +} + +char const* const* Configuration::getDebugTags() { +#if defined(CVC4_DEBUG) && defined(CVC4_TRACING) + return Debug_tags; +#else /* CVC4_DEBUG && CVC4_TRACING */ + static char const* no_tags[] = { NULL }; + return no_tags; +#endif /* CVC4_DEBUG && CVC4_TRACING */ +} + +int strcmpptr(const char **s1, const char **s2){ + return strcmp(*s1,*s2); +} + +bool Configuration::isDebugTag(char const *tag){ +#if defined(CVC4_DEBUG) && defined(CVC4_TRACING) + unsigned ntags = getNumDebugTags(); + char const* const* tags = getDebugTags(); + for (unsigned i = 0; i < ntags; ++ i) { + if (strcmp(tag, tags[i]) == 0) { + return true; + } + } +#endif /* CVC4_DEBUG && CVC4_TRACING */ + return false; +} + +unsigned Configuration::getNumTraceTags() { +#if CVC4_TRACING + /* -1 because a NULL pointer is inserted as the last value */ + return sizeof(Trace_tags) / sizeof(Trace_tags[0]) - 1; +#else /* CVC4_TRACING */ + return 0; +#endif /* CVC4_TRACING */ +} + +char const* const* Configuration::getTraceTags() { +#if CVC4_TRACING + return Trace_tags; +#else /* CVC4_TRACING */ + static char const* no_tags[] = { NULL }; + return no_tags; +#endif /* CVC4_TRACING */ +} + +bool Configuration::isTraceTag(char const * tag){ +#if CVC4_TRACING + unsigned ntags = getNumTraceTags(); + char const* const* tags = getTraceTags(); + for (unsigned i = 0; i < ntags; ++ i) { + if (strcmp(tag, tags[i]) == 0) { + return true; + } + } +#endif /* CVC4_TRACING */ + return false; +} + +bool Configuration::isGitBuild() { + return IS_GIT_BUILD; +} + +const char* Configuration::getGitBranchName() { + return GIT_BRANCH_NAME; +} + +const char* Configuration::getGitCommit() { + return GIT_COMMIT; +} + +bool Configuration::hasGitModifications() { + return GIT_HAS_MODIFICATIONS; +} + +std::string Configuration::getGitId() { + if(! isGitBuild()) { + return ""; + } + + const char* branchName = getGitBranchName(); + if(*branchName == '\0') { + branchName = "-"; + } + + stringstream ss; + ss << "git " << branchName << " " << string(getGitCommit()).substr(0, 8) + << ( ::CVC4::Configuration::hasGitModifications() ? " (with modifications)" : "" ); + return ss.str(); +} + +bool Configuration::isSubversionBuild() { + return IS_SUBVERSION_BUILD; +} + +const char* Configuration::getSubversionBranchName() { + return SUBVERSION_BRANCH_NAME; +} + +unsigned Configuration::getSubversionRevision() { + return SUBVERSION_REVISION; +} + +bool Configuration::hasSubversionModifications() { + return SUBVERSION_HAS_MODIFICATIONS; +} + +std::string Configuration::getSubversionId() { + if(! isSubversionBuild()) { + return ""; + } + + stringstream ss; + ss << "subversion " << getSubversionBranchName() << " r" << getSubversionRevision() + << ( ::CVC4::Configuration::hasSubversionModifications() ? " (with modifications)" : "" ); + return ss.str(); +} + +std::string Configuration::getCompiler() { + stringstream ss; +#ifdef __GNUC__ + ss << "GCC"; +#else /* __GNUC__ */ + ss << "unknown compiler"; +#endif /* __GNUC__ */ +#ifdef __VERSION__ + ss << " version " << __VERSION__; +#else /* __VERSION__ */ + ss << ", unknown version"; +#endif /* __VERSION__ */ + return ss.str(); +} + +std::string Configuration::getCompiledDateTime() { + return __DATE__ " " __TIME__; +} + +}/* CVC4 namespace */ diff --git a/src/base/configuration.h b/src/base/configuration.h new file mode 100644 index 000000000..818652db0 --- /dev/null +++ b/src/base/configuration.h @@ -0,0 +1,135 @@ +/********************* */ +/*! \file configuration.h + ** \verbatim + ** Original author: Morgan Deters + ** Major contributors: none + ** Minor contributors (to current version): ACSYS, Liana Hadarean, Tim King, Francois Bobot + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Interface to a public class that provides compile-time information + ** about the CVC4 library. + ** + ** Interface to a public class that provides compile-time information + ** about the CVC4 library. + **/ + +#include "cvc4_public.h" + +#ifndef __CVC4__CONFIGURATION_H +#define __CVC4__CONFIGURATION_H + +#include <string> + +namespace CVC4 { + +/** + * Represents the (static) configuration of CVC4. + */ +class CVC4_PUBLIC Configuration { +private: + /** Private default ctor: Disallow construction of this class */ + Configuration(); + + // these constants are filled in by the build system + static const bool IS_SUBVERSION_BUILD; + static const char* const SUBVERSION_BRANCH_NAME; + static const unsigned SUBVERSION_REVISION; + static const bool SUBVERSION_HAS_MODIFICATIONS; + static const bool IS_GIT_BUILD; + static const char* const GIT_BRANCH_NAME; + static const char* const GIT_COMMIT; + static const bool GIT_HAS_MODIFICATIONS; + +public: + + static std::string getName(); + + static bool isDebugBuild(); + + static bool isStatisticsBuild(); + + static bool isReplayBuild(); + + static bool isTracingBuild(); + + static bool isDumpingBuild(); + + static bool isMuzzledBuild(); + + static bool isAssertionBuild(); + + static bool isProofBuild(); + + static bool isCoverageBuild(); + + static bool isProfilingBuild(); + + static bool isCompetitionBuild(); + + static std::string getPackageName(); + + static std::string getVersionString(); + + static unsigned getVersionMajor(); + + static unsigned getVersionMinor(); + + static unsigned getVersionRelease(); + + static std::string getVersionExtra(); + + static std::string about(); + + static bool licenseIsGpl(); + + static bool isBuiltWithGmp(); + + static bool isBuiltWithCln(); + + static bool isBuiltWithGlpk(); + + static bool isBuiltWithAbc(); + + static bool isBuiltWithReadline(); + + static bool isBuiltWithCudd(); + + static bool isBuiltWithTlsSupport(); + + /* Return the number of debug tags */ + static unsigned getNumDebugTags(); + /* Return a sorted array of the debug tags name */ + static char const* const* getDebugTags(); + /* Test if the given argument is a known debug tag name */ + static bool isDebugTag(char const *); + + /* Return the number of trace tags */ + static unsigned getNumTraceTags(); + /* Return a sorted array of the trace tags name */ + static char const* const* getTraceTags(); + /* Test if the given argument is a known trace tag name */ + static bool isTraceTag(char const *); + + static bool isGitBuild(); + static const char* getGitBranchName(); + static const char* getGitCommit(); + static bool hasGitModifications(); + static std::string getGitId(); + + static bool isSubversionBuild(); + static const char* getSubversionBranchName(); + static unsigned getSubversionRevision(); + static bool hasSubversionModifications(); + static std::string getSubversionId(); + + static std::string getCompiler(); + static std::string getCompiledDateTime(); + +};/* class Configuration */ + +}/* CVC4 namespace */ + +#endif /* __CVC4__CONFIGURATION_H */ diff --git a/src/base/configuration.i b/src/base/configuration.i new file mode 100644 index 000000000..3b92e2438 --- /dev/null +++ b/src/base/configuration.i @@ -0,0 +1,7 @@ +%{ +#include "base/configuration.h" +%} + +%apply char **STRING_ARRAY { char const* const* } +%include "base/configuration.h" +%clear char const* const*; diff --git a/src/base/configuration_private.h b/src/base/configuration_private.h new file mode 100644 index 000000000..902fdad09 --- /dev/null +++ b/src/base/configuration_private.h @@ -0,0 +1,164 @@ +/********************* */ +/*! \file configuration_private.h + ** \verbatim + ** Original author: Christopher L. Conway + ** Major contributors: ACSYS, Morgan Deters + ** Minor contributors (to current version): Liana Hadarean, Tim King + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Provides compile-time configuration information about the + ** CVC4 library. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__CONFIGURATION_PRIVATE_H +#define __CVC4__CONFIGURATION_PRIVATE_H + +#include <string> + +#include "base/configuration.h" + +namespace CVC4 { + +#ifdef CVC4_DEBUG +# define IS_DEBUG_BUILD true +#else /* CVC4_DEBUG */ +# define IS_DEBUG_BUILD false +#endif /* CVC4_DEBUG */ + +#ifdef CVC4_STATISTICS_ON +# define IS_STATISTICS_BUILD true +#else /* CVC4_STATISTICS_ON */ +# define IS_STATISTICS_BUILD false +#endif /* CVC4_STATISTICS_ON */ + +#ifdef CVC4_REPLAY +# define IS_REPLAY_BUILD true +#else /* CVC4_REPLAY */ +# define IS_REPLAY_BUILD false +#endif /* CVC4_REPLAY */ + +#ifdef CVC4_TRACING +# define IS_TRACING_BUILD true +#else /* CVC4_TRACING */ +# define IS_TRACING_BUILD false +#endif /* CVC4_TRACING */ + +#ifdef CVC4_DUMPING +# define IS_DUMPING_BUILD true +#else /* CVC4_DUMPING */ +# define IS_DUMPING_BUILD false +#endif /* CVC4_DUMPING */ + +#ifdef CVC4_MUZZLE +# define IS_MUZZLED_BUILD true +#else /* CVC4_MUZZLE */ +# define IS_MUZZLED_BUILD false +#endif /* CVC4_MUZZLE */ + +#ifdef CVC4_ASSERTIONS +# define IS_ASSERTIONS_BUILD true +#else /* CVC4_ASSERTIONS */ +# define IS_ASSERTIONS_BUILD false +#endif /* CVC4_ASSERTIONS */ + +#ifdef CVC4_PROOF +# define IS_PROOFS_BUILD true +#else /* CVC4_PROOF */ +# define IS_PROOFS_BUILD false +#endif /* CVC4_PROOF */ + +#ifdef CVC4_COVERAGE +# define IS_COVERAGE_BUILD true +#else /* CVC4_COVERAGE */ +# define IS_COVERAGE_BUILD false +#endif /* CVC4_COVERAGE */ + +#ifdef CVC4_PROFILING +# define IS_PROFILING_BUILD true +#else /* CVC4_PROFILING */ +# define IS_PROFILING_BUILD false +#endif /* CVC4_PROFILING */ + +#ifdef CVC4_COMPETITION_MODE +# define IS_COMPETITION_BUILD true +#else /* CVC4_COMPETITION_MODE */ +# define IS_COMPETITION_BUILD false +#endif /* CVC4_COMPETITION_MODE */ + +#ifdef CVC4_GMP_IMP +# define IS_GMP_BUILD true +#else /* CVC4_GMP_IMP */ +# define IS_GMP_BUILD false +#endif /* CVC4_GMP_IMP */ + +#ifdef CVC4_CLN_IMP +# define IS_CLN_BUILD true +#else /* CVC4_CLN_IMP */ +# define IS_CLN_BUILD false +#endif /* CVC4_CLN_IMP */ + +#if CVC4_USE_GLPK +# define IS_GLPK_BUILD true +#else /* CVC4_USE_GLPK */ +# define IS_GLPK_BUILD false +#endif /* CVC4_USE_GLPK */ + +#if CVC4_USE_ABC +# define IS_ABC_BUILD true +#else /* CVC4_USE_ABC */ +# define IS_ABC_BUILD false +#endif /* CVC4_USE_ABC */ + +#ifdef HAVE_LIBREADLINE +# define IS_READLINE_BUILD true +#else /* HAVE_LIBREADLINE */ +# define IS_READLINE_BUILD false +#endif /* HAVE_LIBREADLINE */ + +#if CVC4_GPL_DEPS +# define IS_GPL_BUILD true +#else /* CVC4_GPL_DEPS */ +# define IS_GPL_BUILD false +#endif /* CVC4_GPL_DEPS */ + +#ifdef TLS +# define USING_TLS true +#else /* TLS */ +# define USING_TLS false +#endif /* TLS */ + +#define CVC4_ABOUT_STRING ( ::std::string("\ +This is CVC4 version " CVC4_RELEASE_STRING ) + \ + ( ::CVC4::Configuration::isGitBuild() \ + ? ( ::std::string(" [") + ::CVC4::Configuration::getGitId() + "]" ) \ + : \ + ( ::CVC4::Configuration::isSubversionBuild() \ + ? ( ::std::string(" [") + ::CVC4::Configuration::getSubversionId() + "]" ) \ + : ::std::string("") \ + )) + "\n\ +compiled with " + ::CVC4::Configuration::getCompiler() + "\n\ +on " + ::CVC4::Configuration::getCompiledDateTime() + "\n\n\ +Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014\n\ + New York University and The University of Iowa\n\n" + \ + ( IS_GPL_BUILD ? "\ +This build of CVC4 uses GPLed libraries, and is thus covered by the GNU\n\ +General Public License (GPL) version 3. Versions of CVC4 are available\n\ +that are covered by the (modified) BSD license. If you want to license\n\ +CVC4 under this license, please configure CVC4 with the \"--bsd\" option\n\ +before building from sources.\n\ +" : \ +"This CVC4 library uses GMP as its multi-precision arithmetic library.\n\n\ +CVC4 is open-source and is covered by the BSD license (modified).\n\n\ +" ) + "\ +THIS SOFTWARE PROVIDED AS-IS, WITHOUT ANY WARRANTIES. USE AT YOUR OWN RISK.\n\n\ +See the file COPYING (distributed with the source code, and with all binaries)\n\ +for the full CVC4 copyright, licensing, and (lack of) warranty information.\n" ) + +}/* CVC4 namespace */ + +#endif /* __CVC4__CONFIGURATION_PRIVATE_H */ diff --git a/src/base/exception.cpp b/src/base/exception.cpp index e1486e5bc..cdad92d5d 100644 --- a/src/base/exception.cpp +++ b/src/base/exception.cpp @@ -50,7 +50,7 @@ void LastExceptionBuffer::setContents(const char* string) { } } -char* IllegalArgumentException::s_header = "Illegal argument detected"; +const char* IllegalArgumentException::s_header = "Illegal argument detected"; std::string IllegalArgumentException::formatVariadic() { return std::string(); diff --git a/src/base/exception.h b/src/base/exception.h index 02384b6cb..38bbe47a4 100644 --- a/src/base/exception.h +++ b/src/base/exception.h @@ -90,7 +90,7 @@ protected: static std::string format_extra(const char* condStr, const char* argDesc); - static char* s_header; + static const char* s_header; public: @@ -155,8 +155,8 @@ public: private: /* Disallow copies */ - LastExceptionBuffer(const LastExceptionBuffer&) CVC4_UNUSED; - LastExceptionBuffer& operator=(const LastExceptionBuffer&) CVC4_UNUSED; + LastExceptionBuffer(const LastExceptionBuffer&) CVC4_UNDEFINED; + LastExceptionBuffer& operator=(const LastExceptionBuffer&) CVC4_UNDEFINED; char* d_contents; diff --git a/src/base/listener.cpp b/src/base/listener.cpp index 62bec5990..2daced1f5 100644 --- a/src/base/listener.cpp +++ b/src/base/listener.cpp @@ -49,8 +49,8 @@ void ListenerCollection::notify() { bool ListenerCollection::empty() const { return d_listeners.empty(); } -RegisterListener::RegisterListener(ListenerCollection* collection, - Listener* listener) +ListenerCollection::Registration::Registration( + ListenerCollection* collection, Listener* listener) : d_listener(listener) , d_position() , d_collection(collection) @@ -58,9 +58,42 @@ RegisterListener::RegisterListener(ListenerCollection* collection, d_position = d_collection->addListener(d_listener); } -RegisterListener::~RegisterListener() { +ListenerCollection::Registration::~Registration() { d_collection->removeListener(d_position); delete d_listener; } + ListenerCollection::Registration* ListenerCollection::registerListener( + Listener* listener) +{ + return new Registration(this, listener); +} + + +ListenerRegistrationList::ListenerRegistrationList() + : d_registrations() +{} + +ListenerRegistrationList::~ListenerRegistrationList() { + clear(); +} + +void ListenerRegistrationList::add( + ListenerCollection::Registration* registration) +{ + d_registrations.push_back(registration); +} + +void ListenerRegistrationList::clear(){ + typedef std::list<ListenerCollection::Registration*>::iterator iterator; + for(iterator i = d_registrations.begin(), iend = d_registrations.end(); + i != iend; ++i) + { + ListenerCollection::Registration* current = *i; + delete current; + } + d_registrations.clear(); +} + + }/* CVC4 namespace */ diff --git a/src/base/listener.h b/src/base/listener.h index d6828818c..8094c634d 100644 --- a/src/base/listener.h +++ b/src/base/listener.h @@ -14,8 +14,8 @@ ** Utilities for the development of a Listener interface class. This class ** provides a single notification that must be overwritten. This file also ** provides a utility class for a collection of listeners and an RAII style - ** RegisterListener class for managing the relationship between Listeners - ** and the manager. + ** Registration class for managing the relationship between Listeners + ** and the collection. **/ #include "cvc4_public.h" @@ -54,45 +54,111 @@ public: typedef std::list<Listener*> ListenerList; typedef ListenerList::iterator iterator; + /** Creates an empty listener collection. */ ListenerCollection(); + /** + * Destroys an iterator collection. + * If assertions are on, this throws an AssertionException if the collection + * is not empty(). + */ ~ListenerCollection(); + /** + * This adds a listener to the current collection and returns + * an iterator to the listener in the collection. + * The user of the collection must call removeListener() using + * this iterator. + * The collection does not take over the memory for the listener. + */ iterator addListener(Listener* listener); + /** + * Remove an listener using the iterator distributed when adding the + * listener. + */ void removeListener(iterator position); + /** Calls notify() on all listeners in the collection. */ void notify(); + /** Returns true if the collection contains no listeners. */ bool empty() const; + /** + * Registration is an RAII utility function for using Listener + * with ListenerCollection. + * + * On construction, the Registration takes a ListenerCollection, + * collection, + * and a Listener*, listener. It takes over the memory for listener. It then + * adds listener to collection. On destruction it removes listener and calls + * delete on listener. + * + * Because of this usage, a Registration must be destroyed before the + * ListenerCollection it is attached to. + */ + class CVC4_PUBLIC Registration { + public: + Registration(ListenerCollection* collection, Listener* listener); + ~Registration(); + + private: + Listener* d_listener; + ListenerCollection::iterator d_position; + ListenerCollection* d_collection; + };/* class CVC4::ListenerCollection::Registration */ + + + /** + * Returns a new Registration given a Listener that is attached to this + * ListenerCollection. Management of the memory is handed to the user of + * this function. To remove the listener, call the destructor for the + * Registration. + */ + Registration* registerListener(Listener* listener); + private: + + /** + * Disabling the copy-constructor. + * The user of the class must be know to remove listeners on the collection. + * Allowing copies will only cause confusion. + */ + ListenerCollection(const ListenerCollection& copy) CVC4_UNDEFINED; + + /** + * Disabling the assignment operator. + * The user of the class must be know to remove listeners on the collection. + * Allowing copies will only cause confusion. + */ + ListenerCollection& operator=(const ListenerCollection& copy) CVC4_UNDEFINED; + + /** A list of the listeners in the collection.*/ ListenerList d_listeners; -}; +};/* class CVC4::ListenerCollection */ /** - * RegisterListener is an RAII utility function for using Listener - * with ListenerCollection. + * A list of ListenerCollection::Registration* pointers. * - * On construction, the RegisterListener takes a ListenerCollection, collection, - * and a Listener*, listener. It takes over the memory for listener. It then - * add listener to collection. On destruction it removes listener and calls - * delete on listener. - * - * Because of this usage, a RegisterListener must be destroyed before - * collection. + * This list assumes it has control over all of the memory of the registrations. */ -class CVC4_PUBLIC RegisterListener { -public: - RegisterListener(ListenerCollection* collection, Listener* listener); - ~RegisterListener(); - -private: - Listener* d_listener; - ListenerCollection::iterator d_position; - ListenerCollection* d_collection; -}; - +class ListenerRegistrationList { + public: + ListenerRegistrationList(); + ~ListenerRegistrationList(); + + void add(ListenerCollection::Registration* registration); + void clear(); + + private: + /** Disallow copying.*/ + ListenerRegistrationList(const ListenerRegistrationList&) CVC4_UNDEFINED; + /** Disallow assignment.*/ + ListenerRegistrationList operator=(const ListenerRegistrationList&) + CVC4_UNDEFINED; + std::list<ListenerCollection::Registration*> d_registrations; +};/* class CVC4::ListenerRegistrationList */ }/* CVC4 namespace */ diff --git a/src/base/mktagheaders b/src/base/mktagheaders new file mode 100755 index 000000000..af44cee8d --- /dev/null +++ b/src/base/mktagheaders @@ -0,0 +1,24 @@ +#!/bin/bash +# +# mktagheaders +# +# The purpose of this script is to generate the *_tag.h header file from the +# *_tags file. +# +# Invocation: +# +# mktagheaders <tag-name> <tag-file> +# +# <tag-name> will be the name of the generated array. +# <tag-file> each line of this file is turned into a string in the generated +# array. + +TAG_NAME=$1 +TAG_FILE=$2 + +echo 'static char const* const '$TAG_NAME'[] = {'; +for tag in `cat $TAG_FILE`; do + echo "\"$tag\","; +done; +echo 'NULL'; +echo '};' diff --git a/src/base/mktags b/src/base/mktags new file mode 100755 index 000000000..090e57014 --- /dev/null +++ b/src/base/mktags @@ -0,0 +1,35 @@ +#!/bin/bash +# +# mktags +# +# The purpose of this script is to create Debug_tags and Trace_tags files. +# Note that in the Makefile workflow these are first stored in a *_tags.tmp +# file. This file contains a list of all of the strings that occur in things +# like Debug("foo") or Debug.isOn("bar") in a given directory. The list is +# seperated by newlines. The expected Debug_tags file for the previous two +# tags would be: +# bar +# foo +# +# Invocation: +# +# mktags {Debug,Trace} <input-files> +# +# <input-files> is expected to be passed a single space separated list of files. +# One can use quotes to achieve this. This is one reason to use "$(...)" +# instead of back ticks `...`. + +DebugOrTrace=$1 +InputFiles=$2 + +grep -h '\<'$DebugOrTrace'\(\.isOn\)* *( *\".*\" *)' \ + $InputFiles | \ + sed 's/\/\/.*//;s/^'$DebugOrTrace'\(\.isOn\)* *( *\"\([^"]*\)\".*/\2/;s/.*[^a-zA-Z0-9_]'$DebugOrTrace'\(\.isOn\)* *( *\"\([^"]*\)\".*/\2/' | \ + LC_ALL=C sort | \ + uniq + + +# Reference copy of what this is replacing. +# grep -h '\<$(@:_tags.tmp=)\(\.isOn\)* *( *\".*\" *)' \ +# `find @srcdir@/../ -name "*.cpp" -o -name "*.h" -o -name "*.cc" -o -name "*.g"` | \ +# sed 's/\/\/.*//;s/^$(@:_tags.tmp=)\(\.isOn\)* *( *\"\([^"]*\)\".*/\2/;s/.*[^a-zA-Z0-9_]$(@:_tags.tmp=)\(\.isOn\)* *( *\"\([^"]*\)\".*/\2/' | LC_ALL=C sort | uniq diff --git a/src/base/output.h b/src/base/output.h index 0974591db..4bffad85f 100644 --- a/src/base/output.h +++ b/src/base/output.h @@ -212,11 +212,12 @@ public: bool off(std::string tag) { d_tags.erase (tag); return false; } bool off() { d_tags.clear(); return false; } - bool isOn(const char* tag) { return d_tags.find(std::string(tag)) != d_tags.end(); } + bool isOn(const char* tag) { return d_tags.find(std::string(tag)) != d_tags.end(); } bool isOn(std::string tag) { return d_tags.find(tag) != d_tags.end(); } - std::ostream& setStream(std::ostream& os) { d_os = &os; return os; } + std::ostream& setStream(std::ostream* os) { d_os = os; return *os; } std::ostream& getStream() { return *d_os; } + std::ostream* getStreamPointer() { return d_os; } };/* class DebugC */ /** The warning output class */ @@ -231,8 +232,9 @@ public: CVC4ostream operator()() { return CVC4ostream(d_os); } - std::ostream& setStream(std::ostream& os) { d_os = &os; return os; } + std::ostream& setStream(std::ostream* os) { d_os = os; return *d_os; } std::ostream& getStream() { return *d_os; } + std::ostream* getStreamPointer() { return d_os; } bool isOn() const { return d_os != &null_os; } @@ -264,8 +266,9 @@ public: CVC4ostream operator()() { return CVC4ostream(d_os); } - std::ostream& setStream(std::ostream& os) { d_os = &os; return os; } + std::ostream& setStream(std::ostream* os) { d_os = os; return *d_os; } std::ostream& getStream() { return *d_os; } + std::ostream* getStreamPointer() { return d_os; } bool isOn() const { return d_os != &null_os; } };/* class MessageC */ @@ -281,8 +284,9 @@ public: CVC4ostream operator()() { return CVC4ostream(d_os); } - std::ostream& setStream(std::ostream& os) { d_os = &os; return os; } + std::ostream& setStream(std::ostream* os) { d_os = os; return *d_os; } std::ostream& getStream() { return *d_os; } + std::ostream* getStreamPointer() { return d_os; } bool isOn() const { return d_os != &null_os; } };/* class NoticeC */ @@ -298,8 +302,9 @@ public: CVC4ostream operator()() { return CVC4ostream(d_os); } - std::ostream& setStream(std::ostream& os) { d_os = &os; return os; } + std::ostream& setStream(std::ostream* os) { d_os = os; return *d_os; } std::ostream& getStream() { return *d_os; } + std::ostream* getStreamPointer() { return d_os; } bool isOn() const { return d_os != &null_os; } };/* class ChatC */ @@ -340,8 +345,10 @@ public: bool isOn(const char* tag) { return d_tags.find(std::string(tag)) != d_tags.end(); } bool isOn(std::string tag) { return d_tags.find(tag) != d_tags.end(); } - std::ostream& setStream(std::ostream& os) { d_os = &os; return os; } + std::ostream& setStream(std::ostream* os) { d_os = os; return *d_os; } std::ostream& getStream() { return *d_os; } + std::ostream* getStreamPointer() { return d_os; } + };/* class TraceC */ /** The dump output class */ @@ -385,8 +392,9 @@ public: bool isOn(const char* tag) { return d_tags.find(std::string(tag)) != d_tags.end(); } bool isOn(std::string tag) { return d_tags.find(tag) != d_tags.end(); } - std::ostream& setStream(std::ostream& os) { d_os = &os; return os; } + std::ostream& setStream(std::ostream* os) { d_os = os; return *d_os; } std::ostream& getStream() { return *d_os; } + std::ostream* getStreamPointer() { return d_os; } };/* class DumpOutC */ /** The debug output singleton */ |