summaryrefslogtreecommitdiff
path: root/src/util
diff options
context:
space:
mode:
Diffstat (limited to 'src/util')
-rw-r--r--src/util/Assert.cpp3
-rw-r--r--src/util/Assert.h4
-rw-r--r--src/util/Makefile.am3
-rw-r--r--src/util/bool.h37
-rw-r--r--src/util/configuration.cpp102
-rw-r--r--src/util/configuration.h107
-rw-r--r--src/util/debug.h2
-rw-r--r--src/util/decision_engine.h1
-rw-r--r--src/util/exception.h3
-rw-r--r--src/util/integer.cpp21
-rw-r--r--src/util/integer.h6
-rw-r--r--src/util/model.h2
-rw-r--r--src/util/options.h4
-rw-r--r--src/util/output.cpp2
-rw-r--r--src/util/output.h4
-rw-r--r--src/util/rational.cpp14
-rw-r--r--src/util/rational.h6
-rw-r--r--src/util/result.h2
18 files changed, 225 insertions, 98 deletions
diff --git a/src/util/Assert.cpp b/src/util/Assert.cpp
index f992032ee..06be4ab7c 100644
--- a/src/util/Assert.cpp
+++ b/src/util/Assert.cpp
@@ -16,10 +16,9 @@
#include <new>
#include <cstdarg>
#include <cstdio>
+
#include "util/Assert.h"
#include "util/exception.h"
-#include "cvc4_config.h"
-#include "config.h"
using namespace std;
diff --git a/src/util/Assert.h b/src/util/Assert.h
index ad3f4b1d3..744782ba2 100644
--- a/src/util/Assert.h
+++ b/src/util/Assert.h
@@ -13,6 +13,8 @@
** Assertion utility classes, functions, exceptions, and macros.
**/
+#include "cvc4_public.h"
+
#ifndef __CVC4__ASSERT_H
#define __CVC4__ASSERT_H
@@ -22,8 +24,6 @@
#include <cstdlib>
#include <cstdarg>
-#include "config.h"
-#include "cvc4_config.h"
#include "util/exception.h"
#include "util/output.h"
diff --git a/src/util/Makefile.am b/src/util/Makefile.am
index f6f8323be..5e8dfd2a4 100644
--- a/src/util/Makefile.am
+++ b/src/util/Makefile.am
@@ -20,7 +20,8 @@ libutil_la_SOURCES = \
output.h \
result.h \
unique_id.h \
- configuration.ha \
+ configuration.h \
+ configuration.cpp \
rational.h \
rational.cpp \
integer.h \
diff --git a/src/util/bool.h b/src/util/bool.h
new file mode 100644
index 000000000..edd45b8a0
--- /dev/null
+++ b/src/util/bool.h
@@ -0,0 +1,37 @@
+/********************* */
+/** bool.h
+ ** Original author: mdeters
+ ** 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.
+ **
+ ** A multiprecision rational constant.
+ ** This stores the rational as a pair of multiprecision integers,
+ ** one for the numerator and one for the denominator.
+ ** The number is always stored so that the gcd of the numerator and denominator
+ ** is 1. (This is referred to as referred to as canonical form in GMP's
+ ** literature.) A consquence is that that the numerator and denominator may be
+ ** different than the values used to construct the Rational.
+ **/
+
+#include "cvc4_public.h"
+
+#ifndef __CVC4__BOOL_H
+#define __CVC4__BOOL_H
+
+namespace CVC4 {
+
+struct BoolHashStrategy {
+ static inline size_t hash(bool b) {
+ return b;
+ }
+};/* struct BoolHashStrategy */
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__BOOL_H */
diff --git a/src/util/configuration.cpp b/src/util/configuration.cpp
new file mode 100644
index 000000000..f4ce30968
--- /dev/null
+++ b/src/util/configuration.cpp
@@ -0,0 +1,102 @@
+/********************* */
+/** configuration.cpp
+ ** Original author: mdeters
+ ** 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.
+ **
+ ** Implementation of Configuration class, which provides compile-time
+ ** configuration information about the CVC4 library.
+ **/
+
+#include "util/configuration.h"
+#include "cvc4autoconfig.h"
+
+using namespace std;
+
+namespace CVC4 {
+
+bool Configuration::isDebugBuild() {
+#ifdef CVC4_DEBUG
+ return true;
+#else /* CVC4_DEBUG */
+ return false;
+#endif /* CVC4_DEBUG */
+}
+
+bool Configuration::isTracingBuild() {
+#ifdef CVC4_TRACING
+ return true;
+#else /* CVC4_TRACING */
+ return false;
+#endif /* CVC4_TRACING */
+}
+
+bool Configuration::isMuzzledBuild() {
+#ifdef CVC4_MUZZLE
+ return true;
+#else /* CVC4_MUZZLE */
+ return false;
+#endif /* CVC4_MUZZLE */
+}
+
+bool Configuration::isAssertionBuild() {
+#ifdef CVC4_ASSERTIONS
+ return true;
+#else /* CVC4_ASSERTIONS */
+ return false;
+#endif /* CVC4_ASSERTIONS */
+}
+
+bool Configuration::isCoverageBuild() {
+#ifdef CVC4_COVERAGE
+ return true;
+#else /* CVC4_COVERAGE */
+ return false;
+#endif /* CVC4_COVERAGE */
+}
+
+bool Configuration::isProfilingBuild() {
+#ifdef CVC4_PROFILING
+ return true;
+#else /* CVC4_PROFILING */
+ return false;
+#endif /* CVC4_PROFILING */
+}
+
+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;
+}
+
+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");
+}
+
+}/* CVC4 namespace */
diff --git a/src/util/configuration.h b/src/util/configuration.h
index 20d00a5f8..f939d8981 100644
--- a/src/util/configuration.h
+++ b/src/util/configuration.h
@@ -10,14 +10,16 @@
** See the file COPYING in the top-level source directory for licensing
** information.
**
- ** SmtEngine: the main public entry point of libcvc4.
+ ** 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 "config.h"
-#include "cvc4_config.h"
+#include <string>
namespace CVC4 {
@@ -31,84 +33,29 @@ class CVC4_PUBLIC Configuration {
public:
- static bool isDebugBuild() {
-#ifdef CVC4_DEBUG
- return true;
-#else /* CVC4_DEBUG */
- return false;
-#endif /* CVC4_DEBUG */
- }
-
- static bool isTracingBuild() {
-#ifdef CVC4_TRACING
- return true;
-#else /* CVC4_TRACING */
- return false;
-#endif /* CVC4_TRACING */
- }
-
- static bool isMuzzledBuild() {
-#ifdef CVC4_MUZZLE
- return true;
-#else /* CVC4_MUZZLE */
- return false;
-#endif /* CVC4_MUZZLE */
- }
-
- static bool isAssertionBuild() {
-#ifdef CVC4_ASSERTIONS
- return true;
-#else /* CVC4_ASSERTIONS */
- return false;
-#endif /* CVC4_ASSERTIONS */
- }
-
- static bool isCoverageBuild() {
-#ifdef CVC4_COVERAGE
- return true;
-#else /* CVC4_COVERAGE */
- return false;
-#endif /* CVC4_COVERAGE */
- }
-
- static bool isProfilingBuild() {
-#ifdef CVC4_PROFILING
- return true;
-#else /* CVC4_PROFILING */
- return false;
-#endif /* CVC4_PROFILING */
- }
-
- static std::string getPackageName() {
- return PACKAGE;
- }
-
- static std::string getVersionString() {
- return VERSION;
- }
-
- static unsigned getVersionMajor() {
- return 0;
- }
-
- static unsigned getVersionMinor() {
- return 0;
- }
-
- static unsigned getVersionRelease() {
- return 0;
- }
-
- static std::string about() {
- return std::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");
- }
+ static bool isDebugBuild();
+
+ static bool isTracingBuild();
+
+ static bool isMuzzledBuild();
+
+ static bool isAssertionBuild();
+
+ static bool isCoverageBuild();
+
+ static bool isProfilingBuild();
+
+ static std::string getPackageName();
+
+ static std::string getVersionString();
+
+ static unsigned getVersionMajor();
+
+ static unsigned getVersionMinor();
+
+ static unsigned getVersionRelease();
+ static std::string about();
};
}/* CVC4 namespace */
diff --git a/src/util/debug.h b/src/util/debug.h
index 13b097955..a99652661 100644
--- a/src/util/debug.h
+++ b/src/util/debug.h
@@ -20,8 +20,6 @@
#ifndef __CVC4__DEBUG_H
#define __CVC4__DEBUG_H
-#include "cvc4_config.h"
-
#include <cassert>
#ifdef CVC4_ASSERTIONS
diff --git a/src/util/decision_engine.h b/src/util/decision_engine.h
index fd757b734..84ace55b2 100644
--- a/src/util/decision_engine.h
+++ b/src/util/decision_engine.h
@@ -18,7 +18,6 @@
#ifndef __CVC4__DECISION_ENGINE_H
#define __CVC4__DECISION_ENGINE_H
-#include "cvc4_config.h"
#include "expr/node.h"
namespace CVC4 {
diff --git a/src/util/exception.h b/src/util/exception.h
index ff88b5d81..862597bae 100644
--- a/src/util/exception.h
+++ b/src/util/exception.h
@@ -13,11 +13,12 @@
** CVC4's exception base class and some associated utilities.
**/
+#include "cvc4_public.h"
+
#ifndef __CVC4__EXCEPTION_H
#define __CVC4__EXCEPTION_H
#include <string>
-#include "cvc4_config.h"
namespace CVC4 {
diff --git a/src/util/integer.cpp b/src/util/integer.cpp
index 8fc788eb8..41291cc42 100644
--- a/src/util/integer.cpp
+++ b/src/util/integer.cpp
@@ -1,3 +1,24 @@
+/********************* */
+/** integer.cpp
+ ** Original author: taking
+ ** 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.
+ **
+ ** A multiprecision rational constant.
+ ** This stores the rational as a pair of multiprecision integers,
+ ** one for the numerator and one for the denominator.
+ ** The number is always stored so that the gcd of the numerator and denominator
+ ** is 1. (This is referred to as referred to as canonical form in GMP's
+ ** literature.) A consquence is that that the numerator and denominator may be
+ ** different than the values used to construct the Rational.
+ **/
+
#include "util/integer.h"
using namespace CVC4;
diff --git a/src/util/integer.h b/src/util/integer.h
index c86e836c7..ffba5543a 100644
--- a/src/util/integer.h
+++ b/src/util/integer.h
@@ -13,6 +13,8 @@
** A multiprecision integer constant.
**/
+#include "cvc4_public.h"
+
#ifndef __CVC4__INTEGER_H
#define __CVC4__INTEGER_H
@@ -148,11 +150,11 @@ public:
friend class CVC4::Rational;
};/* class Integer */
-struct IntegerHashFcn {
+struct IntegerHashStrategy {
static inline size_t hash(const CVC4::Integer& i) {
return i.hash();
}
-};
+};/* struct IntegerHashStrategy */
std::ostream& operator<<(std::ostream& os, const Integer& n);
diff --git a/src/util/model.h b/src/util/model.h
index d2a51e447..f807ff963 100644
--- a/src/util/model.h
+++ b/src/util/model.h
@@ -13,6 +13,8 @@
** A model.
**/
+#include "cvc4_public.h"
+
#ifndef __CVC4__MODEL_H
#define __CVC4__MODEL_H
diff --git a/src/util/options.h b/src/util/options.h
index 8e2d46e99..c8c95dd11 100644
--- a/src/util/options.h
+++ b/src/util/options.h
@@ -13,12 +13,14 @@
** Global (command-line or equivalent) tuning parameters.
**/
+#include "cvc4_public.h"
+
#ifndef __CVC4__OPTIONS_H
#define __CVC4__OPTIONS_H
#include <iostream>
#include <string>
-#include "cvc4_config.h"
+
#include "parser/parser_options.h"
namespace CVC4 {
diff --git a/src/util/output.cpp b/src/util/output.cpp
index e7ac3de90..5d09e1d93 100644
--- a/src/util/output.cpp
+++ b/src/util/output.cpp
@@ -13,8 +13,6 @@
** Output utility classes and functions.
**/
-#include "cvc4_config.h"
-
#include <iostream>
#include "util/output.h"
diff --git a/src/util/output.h b/src/util/output.h
index 77b755ad5..6315389e8 100644
--- a/src/util/output.h
+++ b/src/util/output.h
@@ -13,11 +13,11 @@
** Output utility classes and functions.
**/
+#include "cvc4_public.h"
+
#ifndef __CVC4__OUTPUT_H
#define __CVC4__OUTPUT_H
-#include "cvc4_config.h"
-
#include <iostream>
#include <string>
#include <cstdio>
diff --git a/src/util/rational.cpp b/src/util/rational.cpp
index 2f33ed859..f3584e8f3 100644
--- a/src/util/rational.cpp
+++ b/src/util/rational.cpp
@@ -1,3 +1,17 @@
+/********************* */
+/** rational.cpp
+ ** Original author: taking
+ ** 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.
+ **
+ ** A multiprecision rational constant.
+ **/
#include "util/rational.h"
diff --git a/src/util/rational.h b/src/util/rational.h
index fdd125587..37d0c08cb 100644
--- a/src/util/rational.h
+++ b/src/util/rational.h
@@ -19,6 +19,8 @@
** different than the values used to construct the Rational.
**/
+#include "cvc4_public.h"
+
#ifndef __CVC4__RATIONAL_H
#define __CVC4__RATIONAL_H
@@ -181,11 +183,11 @@ public:
};/* class Rational */
-struct RationalHashFcn {
+struct RationalHashStrategy {
static inline size_t hash(const CVC4::Rational& r) {
return r.hash();
}
-};
+};/* struct RationalHashStrategy */
std::ostream& operator<<(std::ostream& os, const Rational& n);
diff --git a/src/util/result.h b/src/util/result.h
index 7557cece8..679e68763 100644
--- a/src/util/result.h
+++ b/src/util/result.h
@@ -13,6 +13,8 @@
** Encapsulation of the result of a query.
**/
+#include "cvc4_public.h"
+
#ifndef __CVC4__RESULT_H
#define __CVC4__RESULT_H
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback