From 704b56f3f5bdba6601dd687c8e649e36de50a6e7 Mon Sep 17 00:00:00 2001 From: "Christopher L. Conway" Date: Thu, 29 Jul 2010 18:33:33 +0000 Subject: [PATCH] Adding configuration_private.h to allow inlining of configuration checks --- src/expr/node_manager.h | 5 +- src/util/Makefile.am | 1 + src/util/configuration.cpp | 73 ++++-------------------- src/util/configuration_private.h | 96 ++++++++++++++++++++++++++++++++ 4 files changed, 111 insertions(+), 64 deletions(-) create mode 100644 src/util/configuration_private.h diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index b7c7f871e..dcfb14b7a 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -37,6 +37,7 @@ #include "expr/metakind.h" #include "expr/node_value.h" #include "context/context.h" +#include "util/configuration_private.h" namespace CVC4 { @@ -788,7 +789,7 @@ inline TypeNode NodeManager::mkSort(const std::string& name) { template inline Node NodeManager::doMkNode(NodeBuilder& nb) { Node n = nb.constructNode(); - if( Configuration::isDebugBuild() ) { + if( IS_DEBUG_BUILD ) { // force an immediate type check getType(n,true); } @@ -798,7 +799,7 @@ inline Node NodeManager::doMkNode(NodeBuilder& nb) { template inline Node* NodeManager::doMkNodePtr(NodeBuilder& nb) { Node* np = nb.constructNodePtr(); - if( Configuration::isDebugBuild() ) { + if( IS_DEBUG_BUILD ) { // force an immediate type check getType(*np,true); } diff --git a/src/util/Makefile.am b/src/util/Makefile.am index a690f7432..e41c6effc 100644 --- a/src/util/Makefile.am +++ b/src/util/Makefile.am @@ -24,6 +24,7 @@ libutil_la_SOURCES = \ result.h \ unique_id.h \ configuration.h \ + configuration_private.h \ configuration.cpp \ rational.h \ integer.h \ diff --git a/src/util/configuration.cpp b/src/util/configuration.cpp index 0b751429b..072a93b18 100644 --- a/src/util/configuration.cpp +++ b/src/util/configuration.cpp @@ -19,66 +19,38 @@ **/ #include "util/configuration.h" -#include "cvc4autoconfig.h" +#include "util/configuration_private.h" using namespace std; namespace CVC4 { bool Configuration::isDebugBuild() { -#ifdef CVC4_DEBUG - return true; -#else /* CVC4_DEBUG */ - return false; -#endif /* CVC4_DEBUG */ + return IS_DEBUG_BUILD; } bool Configuration::isTracingBuild() { -#ifdef CVC4_TRACING - return true; -#else /* CVC4_TRACING */ - return false; -#endif /* CVC4_TRACING */ + return IS_TRACING_BUILD; } bool Configuration::isMuzzledBuild() { -#ifdef CVC4_MUZZLE - return true; -#else /* CVC4_MUZZLE */ - return false; -#endif /* CVC4_MUZZLE */ + return IS_MUZZLED_BUILD; } bool Configuration::isAssertionBuild() { -#ifdef CVC4_ASSERTIONS - return true; -#else /* CVC4_ASSERTIONS */ - return false; -#endif /* CVC4_ASSERTIONS */ + return IS_ASSERTIONS_BUILD; } bool Configuration::isCoverageBuild() { -#ifdef CVC4_COVERAGE - return true; -#else /* CVC4_COVERAGE */ - return false; -#endif /* CVC4_COVERAGE */ + return IS_COVERAGE_BUILD; } bool Configuration::isProfilingBuild() { -#ifdef CVC4_PROFILING - return true; -#else /* CVC4_PROFILING */ - return false; -#endif /* CVC4_PROFILING */ + return IS_PROFILING_BUILD; } bool Configuration::isCompetitionBuild() { -#ifdef CVC4_COMPETITION_MODE - return true; -#else /* CVC4_COMPETITION_MODE */ - return false; -#endif /* CVC4_COMPETITION_MODE */ + return IS_COMPETITION_BUILD; } string Configuration::getPackageName() { @@ -102,38 +74,15 @@ unsigned Configuration::getVersionRelease() { } string Configuration::about() { - return string("\ -This is a pre-release of CVC4.\n\ -Copyright (C) 2009, 2010\n\ - The ACSys Group\n\ - Courant Institute of Mathematical Sciences\n\ - New York University\n\ - New York, NY 10012 USA\n\n") + - (isBuiltWithCln() ? "\ -This CVC4 library uses CLN as its multi-precision arithmetic library.\n\n\ -CVC4 is open-source and is covered by the BSD license (modified).\n\ -However, CLN, the Class Library for Numbers, is covered by the GPL. Thus\n\ -this CVC4 library cannot be used in proprietary applications. Please\n\ -consult the CVC4 documentation for instructions about building a version\n\ -of CVC4 that links against GMP, and can be used in such applications.\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"); + return CVC4_ABOUT_STRING; } bool Configuration::isBuiltWithGmp() { -#ifdef CVC4_GMP_IMP - return true; -#else /* CVC4_GMP_IMP */ - return false; -#endif /* CVC4_GMP_IMP */ + return IS_GMP_BUILD; } bool Configuration::isBuiltWithCln() { -#ifdef CVC4_CLN_IMP - return true; -#else /* CVC4_CLN_IMP */ - return false; -#endif /* CVC4_CLN_IMP */ + return IS_CLN_BUILD; } }/* CVC4 namespace */ diff --git a/src/util/configuration_private.h b/src/util/configuration_private.h new file mode 100644 index 000000000..913fcc3e9 --- /dev/null +++ b/src/util/configuration_private.h @@ -0,0 +1,96 @@ +/********************* */ +/*! \file configuration_private.h + ** \verbatim + ** Original author: cconway + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 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 Provides compile-time configuration information about the + ** CVC4 library. + **/ + +#include "cvc4autoconfig.h" + +using namespace std; + +namespace CVC4 { + +#ifdef CVC4_DEBUG +#define IS_DEBUG_BUILD true +#else /* CVC4_DEBUG */ +#define IS_DEBUG_BUILD false +#endif /* CVC4_DEBUG */ + +#ifdef CVC4_TRACING +#define IS_TRACING_BUILD true +#else /* CVC4_TRACING */ +#define IS_TRACING_BUILD false +#endif /* CVC4_TRACING */ + +#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_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 */ + +#define CVC4_ABOUT_STRING string("\ +This is a pre-release of CVC4.\n\ +Copyright (C) 2009, 2010\n\ + The ACSys Group\n\ + Courant Institute of Mathematical Sciences\n\ + New York University\n\ + New York, NY 10012 USA\n\n") + \ + (IS_CLN_BUILD ? "\ +This CVC4 library uses CLN as its multi-precision arithmetic library.\n\n\ +CVC4 is open-source and is covered by the BSD license (modified).\n\ +However, CLN, the Class Library for Numbers, is covered by the GPL. Thus\n\ +this CVC4 library cannot be used in proprietary applications. Please\n\ +consult the CVC4 documentation for instructions about building a version\n\ +of CVC4 that links against GMP, and can be used in such applications.\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") + + +}/* CVC4 namespace */ -- 2.30.2