summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/expr/node_manager.h5
-rw-r--r--src/util/Makefile.am1
-rw-r--r--src/util/configuration.cpp73
-rw-r--r--src/util/configuration_private.h96
4 files changed, 111 insertions, 64 deletions
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 <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 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 */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback