Adding configuration_private.h to allow inlining of configuration checks

diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index b7c7f871e8ff59107142f5c5695c8843256370a8..dcfb14b7a30135cbbb6945afcb2554851734f5bb 100644 (file)
--- 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 <unsigned nchild_thresh>
 inline Node NodeManager::doMkNode(NodeBuilder<nchild_thresh>& 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<nchild_thresh>& nb) {
 template <unsigned nchild_thresh>
 inline Node* NodeManager::doMkNodePtr(NodeBuilder<nchild_thresh>& 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 a690f743278f825b184779ce817a1fdee6d5a62d..e41c6effcbbe0101fb076c1d89c8c9fd1d6eb235 100644 (file)
--- 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 0b751429ba3938ee96bcf55130a05f0a5d3b7c1c..072a93b18ea3bf59249fcb35fb707e059ff5f1c2 100644 (file)
--- 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 (file)
index 0000000..913fcc3
--- /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 */