diff options
Diffstat (limited to 'src/util')
-rw-r--r-- | src/util/Assert.cpp | 3 | ||||
-rw-r--r-- | src/util/Assert.h | 4 | ||||
-rw-r--r-- | src/util/Makefile.am | 3 | ||||
-rw-r--r-- | src/util/bool.h | 37 | ||||
-rw-r--r-- | src/util/configuration.cpp | 102 | ||||
-rw-r--r-- | src/util/configuration.h | 107 | ||||
-rw-r--r-- | src/util/debug.h | 2 | ||||
-rw-r--r-- | src/util/decision_engine.h | 1 | ||||
-rw-r--r-- | src/util/exception.h | 3 | ||||
-rw-r--r-- | src/util/integer.cpp | 21 | ||||
-rw-r--r-- | src/util/integer.h | 6 | ||||
-rw-r--r-- | src/util/model.h | 2 | ||||
-rw-r--r-- | src/util/options.h | 4 | ||||
-rw-r--r-- | src/util/output.cpp | 2 | ||||
-rw-r--r-- | src/util/output.h | 4 | ||||
-rw-r--r-- | src/util/rational.cpp | 14 | ||||
-rw-r--r-- | src/util/rational.h | 6 | ||||
-rw-r--r-- | src/util/result.h | 2 |
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 |