summaryrefslogtreecommitdiff
path: root/src/util
diff options
context:
space:
mode:
Diffstat (limited to 'src/util')
-rw-r--r--src/util/Makefile.am35
-rw-r--r--src/util/bitvector.h3
-rw-r--r--src/util/configuration.cpp27
-rw-r--r--src/util/configuration.h4
-rw-r--r--src/util/gmp_util.h26
-rw-r--r--src/util/integer.h.in (renamed from src/util/integer.h)23
-rw-r--r--src/util/integer_cln_imp.cpp13
-rw-r--r--src/util/integer_cln_imp.h15
-rw-r--r--src/util/integer_gmp_imp.cpp14
-rw-r--r--src/util/integer_gmp_imp.h14
-rw-r--r--src/util/rational.h.in (renamed from src/util/rational.h)23
-rw-r--r--src/util/rational_cln_imp.cpp13
-rw-r--r--src/util/rational_cln_imp.h12
-rw-r--r--src/util/rational_gmp_imp.cpp13
-rw-r--r--src/util/rational_gmp_imp.h12
-rw-r--r--src/util/sexpr.h2
16 files changed, 160 insertions, 89 deletions
diff --git a/src/util/Makefile.am b/src/util/Makefile.am
index 1446412ce..b6ca5bcc6 100644
--- a/src/util/Makefile.am
+++ b/src/util/Makefile.am
@@ -1,6 +1,6 @@
AM_CPPFLAGS = \
-D__BUILDING_CVC4LIB \
- -I@srcdir@/../include -I@srcdir@/..
+ -I@srcdir@/../include -I@srcdir@/.. -I@builddir@/..
AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN)
noinst_LTLIBRARIES = libutil.la
@@ -26,6 +26,30 @@ libutil_la_SOURCES = \
configuration.cpp \
rational.h \
integer.h \
+ bitvector.h \
+ bitvector.cpp \
+ gmp_util.h \
+ sexpr.h \
+ stats.h \
+ stats.cpp \
+ triple.h
+
+BUILT_SOURCES = \
+ rational.h \
+ integer.h
+
+if CVC4_CLN_IMP
+libutil_la_SOURCES += \
+ integer_cln_imp.cpp \
+ rational_cln_imp.cpp
+endif
+if CVC4_GMP_IMP
+libutil_la_SOURCES += \
+ integer_gmp_imp.cpp \
+ rational_gmp_imp.cpp
+endif
+
+EXTRA_DIST = \
rational_cln_imp.h \
integer_cln_imp.h \
rational_cln_imp.cpp \
@@ -34,10 +58,5 @@ libutil_la_SOURCES = \
integer_gmp_imp.h \
rational_gmp_imp.cpp \
integer_gmp_imp.cpp \
- bitvector.h \
- bitvector.cpp \
- gmp_util.h \
- sexpr.h \
- stats.h \
- stats.cpp \
- triple.h
+ rational.h.in \
+ integer.h.in
diff --git a/src/util/bitvector.h b/src/util/bitvector.h
index 928592d9e..0b5952481 100644
--- a/src/util/bitvector.h
+++ b/src/util/bitvector.h
@@ -3,7 +3,7 @@
** \verbatim
** Original author: dejan
** Major contributors: cconway
- ** Minor contributors (to current version): taking, mdeters
+ ** Minor contributors (to current version): mdeters
** This file is part of the CVC4 prototype.
** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
** Courant Institute of Mathematical Sciences
@@ -24,7 +24,6 @@
#include <iostream>
#include "util/Assert.h"
-#include "util/gmp_util.h"
#include "util/integer.h"
namespace CVC4 {
diff --git a/src/util/configuration.cpp b/src/util/configuration.cpp
index 2a7563f82..12908c672 100644
--- a/src/util/configuration.cpp
+++ b/src/util/configuration.cpp
@@ -100,7 +100,32 @@ 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");
+ 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");
+}
+
+bool Configuration::isBuiltWithGmp() {
+#ifdef CVC4_GMP_IMP
+ return true;
+#else /* CVC4_GMP_IMP */
+ return false;
+#endif /* CVC4_GMP_IMP */
+}
+
+bool Configuration::isBuiltWithCln() {
+#ifdef CVC4_CLN_IMP
+ return true;
+#else /* CVC4_CLN_IMP */
+ return false;
+#endif /* CVC4_CLN_IMP */
}
}/* CVC4 namespace */
diff --git a/src/util/configuration.h b/src/util/configuration.h
index 00651202d..6d5ac12a1 100644
--- a/src/util/configuration.h
+++ b/src/util/configuration.h
@@ -60,6 +60,10 @@ public:
static unsigned getVersionRelease();
static std::string about();
+
+ static bool isBuiltWithGmp();
+
+ static bool isBuiltWithCln();
};
}/* CVC4 namespace */
diff --git a/src/util/gmp_util.h b/src/util/gmp_util.h
index a425690a5..87102e644 100644
--- a/src/util/gmp_util.h
+++ b/src/util/gmp_util.h
@@ -17,24 +17,24 @@
** \todo document this file
**/
-#ifndef __CVC4__GMP_H_
-#define __CVC4__GMP_H_
+#ifndef __CVC4__GMP_UTIL_H
+#define __CVC4__GMP_UTIL_H
#include <gmpxx.h>
namespace CVC4 {
- /** Hashes the gmp integer primitive in a word by word fashion. */
- inline size_t gmpz_hash(const mpz_t toHash) {
- size_t hash = 0;
- for (int i=0, n=mpz_size(toHash); i<n; ++i){
- mp_limb_t limb = mpz_getlimbn(toHash, i);
- hash = hash * 2;
- hash = hash xor limb;
- }
- return hash;
+/** Hashes the gmp integer primitive in a word by word fashion. */
+inline size_t gmpz_hash(const mpz_t toHash) {
+ size_t hash = 0;
+ for (int i = 0, n = mpz_size(toHash); i < n; ++i){
+ mp_limb_t limb = mpz_getlimbn(toHash, i);
+ hash = hash * 2;
+ hash = hash xor limb;
}
+ return hash;
+}/* gmpz_hash() */
-}
+}/* CVC4 namespace */
-#endif /* __CVC4__GMP_H_ */
+#endif /* __CVC4__GMP_UTIL_H */
diff --git a/src/util/integer.h b/src/util/integer.h.in
index c57450d5f..7e1b9a1aa 100644
--- a/src/util/integer.h
+++ b/src/util/integer.h.in
@@ -1,5 +1,5 @@
/********************* */
-/*! \file integer.h
+/*! \file integer.h.in
** \verbatim
** Original author: taking
** Major contributors: none
@@ -16,9 +16,18 @@
** A multiprecision integer constant.
**/
-#ifdef __CVC4__USE_GMP_IMP
-#include "util/integer_gmp_imp.h"
-#endif
-#ifdef __CVC4__USE_CLN_IMP
-#include "util/integer_cln_imp.h"
-#endif
+// this is used to avoid a public header dependence on cvc4autoconfig.h
+#if /* use CLN */ @CVC4_USE_CLN_IMP@
+# define CVC4_CLN_IMP
+#endif /* @CVC4_USE_CLN_IMP@ */
+#if /* use GMP */ @CVC4_USE_GMP_IMP@
+# define CVC4_GMP_IMP
+#endif /* @CVC4_USE_GMP_IMP@ */
+
+#ifdef CVC4_CLN_IMP
+# include "util/integer_cln_imp.h"
+#endif /* CVC4_CLN_IMP */
+
+#ifdef CVC4_GMP_IMP
+# include "util/integer_gmp_imp.h"
+#endif /* CVC4_GMP_IMP */
diff --git a/src/util/integer_cln_imp.cpp b/src/util/integer_cln_imp.cpp
index 35293bb84..a6cad96d1 100644
--- a/src/util/integer_cln_imp.cpp
+++ b/src/util/integer_cln_imp.cpp
@@ -1,9 +1,9 @@
/********************* */
-/*! \file integer.cpp
+/*! \file integer_cln_imp.cpp
** \verbatim
** Original author: taking
- ** Major contributors: mdeters
- ** Minor contributors (to current version): dejan
+ ** 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
@@ -21,14 +21,17 @@
** literature.) A consquence is that that the numerator and denominator may be
** different than the values used to construct the Rational.
**/
-#ifdef __CVC4__USE_CLN_IMP
+#include "cvc4autoconfig.h"
#include "util/integer.h"
+#ifndef CVC4_CLN_IMP
+# error "This source should only ever be built if CVC4_CLN_IMP is on !"
+#endif /* CVC4_CLN_IMP */
+
using namespace CVC4;
std::ostream& CVC4::operator<<(std::ostream& os, const Integer& n) {
return os << n.toString();
}
-#endif /* __CVC4__USE_CLN_IMP */
diff --git a/src/util/integer_cln_imp.h b/src/util/integer_cln_imp.h
index 2154952f0..8551d0a6a 100644
--- a/src/util/integer_cln_imp.h
+++ b/src/util/integer_cln_imp.h
@@ -1,9 +1,9 @@
/********************* */
-/*! \file integer.h
+/*! \file integer_cln_imp.h
** \verbatim
** Original author: taking
- ** Major contributors: mdeters
- ** Minor contributors (to current version): dejan, 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
@@ -11,13 +11,12 @@
** See the file COPYING in the top-level source directory for licensing
** information.\endverbatim
**
- ** \brief A multiprecision integer constant.
+ ** \brief A multiprecision integer constant; wraps a CLN multiprecision
+ ** integer.
**
- ** A multiprecision integer constant.
+ ** A multiprecision integer constant; wraps a CLN multiprecision integer.
**/
-#ifdef __CVC4__USE_CLN_IMP
-
#include "cvc4_public.h"
#ifndef __CVC4__INTEGER_H
@@ -30,7 +29,6 @@
#include <cln/input.h>
#include <cln/integer_io.h>
#include "util/Assert.h"
-#include "util/gmp_util.h"
namespace CVC4 {
@@ -226,4 +224,3 @@ std::ostream& operator<<(std::ostream& os, const Integer& n);
#endif /* __CVC4__INTEGER_H */
-#endif /* __CVC4__USE_CLN_IMP */
diff --git a/src/util/integer_gmp_imp.cpp b/src/util/integer_gmp_imp.cpp
index 7bda7f02a..112713aa5 100644
--- a/src/util/integer_gmp_imp.cpp
+++ b/src/util/integer_gmp_imp.cpp
@@ -1,9 +1,9 @@
/********************* */
-/*! \file integer.cpp
+/*! \file integer_gmp_imp.cpp
** \verbatim
** Original author: taking
- ** Major contributors: mdeters
- ** Minor contributors (to current version): dejan
+ ** 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
@@ -22,12 +22,16 @@
** different than the values used to construct the Rational.
**/
-#ifdef __CVC4__USE_GMP_IMP
+#include "cvc4autoconfig.h"
#include "util/integer.h"
+#ifndef CVC4_GMP_IMP
+# error "This source should only ever be built if CVC4_GMP_IMP is on !"
+#endif /* CVC4_GMP_IMP */
+
using namespace CVC4;
std::ostream& CVC4::operator<<(std::ostream& os, const Integer& n) {
return os << n.toString();
}
-#endif /* __CVC4__USE_GMP_IMP */
+
diff --git a/src/util/integer_gmp_imp.h b/src/util/integer_gmp_imp.h
index 7217d0c5a..b065dca23 100644
--- a/src/util/integer_gmp_imp.h
+++ b/src/util/integer_gmp_imp.h
@@ -1,9 +1,9 @@
/********************* */
-/*! \file integer.h
+/*! \file integer_gmp_imp.h
** \verbatim
** Original author: taking
- ** Major contributors: mdeters
- ** Minor contributors (to current version): dejan, 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
@@ -11,12 +11,12 @@
** See the file COPYING in the top-level source directory for licensing
** information.\endverbatim
**
- ** \brief A multiprecision integer constant.
+ ** \brief A multiprecision integer constant; wraps a GMP multiprecision
+ ** integer.
**
- ** A multiprecision integer constant.
+ ** A multiprecision integer constant; wraps a GMP multiprecision integer.
**/
-#ifdef __CVC4__USE_GMP_IMP
#include "cvc4_public.h"
#ifndef __CVC4__INTEGER_H
@@ -165,4 +165,4 @@ std::ostream& operator<<(std::ostream& os, const Integer& n);
}/* CVC4 namespace */
#endif /* __CVC4__INTEGER_H */
-#endif /* __CVC4__USE_GMP_IMP */
+
diff --git a/src/util/rational.h b/src/util/rational.h.in
index 73fcb73a3..88c488290 100644
--- a/src/util/rational.h
+++ b/src/util/rational.h.in
@@ -1,5 +1,5 @@
/********************* */
-/*! \file rational.h
+/*! \file rational.h.in
** \verbatim
** Original author: taking
** Major contributors: none
@@ -16,9 +16,18 @@
** Multi-precision rational constants.
**/
-#ifdef __CVC4__USE_GMP_IMP
-#include "util/rational_gmp_imp.h"
-#endif
-#ifdef __CVC4__USE_CLN_IMP
-#include "util/rational_cln_imp.h"
-#endif
+// this is used to avoid a public header dependence on cvc4autoconfig.h
+#if /* use CLN */ @CVC4_USE_CLN_IMP@
+# define CVC4_CLN_IMP
+#endif /* @CVC4_USE_CLN_IMP@ */
+#if /* use GMP */ @CVC4_USE_GMP_IMP@
+# define CVC4_GMP_IMP
+#endif /* @CVC4_USE_GMP_IMP@ */
+
+#ifdef CVC4_CLN_IMP
+# include "util/rational_cln_imp.h"
+#endif /* CVC4_CLN_IMP */
+
+#ifdef CVC4_GMP_IMP
+# include "util/rational_gmp_imp.h"
+#endif /* CVC4_GMP_IMP */
diff --git a/src/util/rational_cln_imp.cpp b/src/util/rational_cln_imp.cpp
index 0960b79b9..7baf8d3bf 100644
--- a/src/util/rational_cln_imp.cpp
+++ b/src/util/rational_cln_imp.cpp
@@ -2,7 +2,7 @@
/*! \file rational_cln_imp.cpp
** \verbatim
** Original author: taking
- ** Major contributors: mdeters, 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)
@@ -16,13 +16,15 @@
** A multi-precision rational constant.
**/
-#ifdef __CVC4__USE_CLN_IMP
-
-
-#include "util/integer.h"
+#include "cvc4autoconfig.h"
#include "util/rational.h"
+#include "util/integer.h"
#include <string>
+#ifndef CVC4_CLN_IMP
+# error "This source should only ever be built if CVC4_CLN_IMP is on !"
+#endif /* CVC4_CLN_IMP */
+
using namespace std;
using namespace CVC4;
@@ -51,4 +53,3 @@ std::ostream& CVC4::operator<<(std::ostream& os, const Rational& q){
return os << q.toString();
}
-#endif /* __CVC4__USE_CLN_IMP */
diff --git a/src/util/rational_cln_imp.h b/src/util/rational_cln_imp.h
index 347c1d195..ae172f262 100644
--- a/src/util/rational_cln_imp.h
+++ b/src/util/rational_cln_imp.h
@@ -1,9 +1,9 @@
/********************* */
-/*! \file rational.h
+/*! \file rational_cln_imp.h
** \verbatim
** Original author: taking
** Major contributors: none
- ** Minor contributors (to current version): dejan, mdeters, cconway
+ ** 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
@@ -11,13 +11,12 @@
** See the file COPYING in the top-level source directory for licensing
** information.\endverbatim
**
- ** \brief Multi-precision rational constants.
+ ** \brief Multiprecision rational constants; wraps a CLN multiprecision
+ ** rational.
**
- ** Multi-precision rational constants.
+ ** Multiprecision rational constants; wraps a CLN multiprecision rational.
**/
-#ifdef __CVC4__USE_CLN_IMP
-
#include "cvc4_public.h"
#ifndef __CVC4__RATIONAL_H
@@ -283,4 +282,3 @@ std::ostream& operator<<(std::ostream& os, const Rational& n);
#endif /* __CVC4__RATIONAL_H */
-#endif /* __CVC4__USE_CLN_IMP */
diff --git a/src/util/rational_gmp_imp.cpp b/src/util/rational_gmp_imp.cpp
index e5ff11c07..a0af69b4c 100644
--- a/src/util/rational_gmp_imp.cpp
+++ b/src/util/rational_gmp_imp.cpp
@@ -1,8 +1,8 @@
/********************* */
-/*! \file rational.cpp
+/*! \file rational_gmp_imp.cpp
** \verbatim
** Original author: taking
- ** Major contributors: mdeters, 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)
@@ -15,12 +15,16 @@
**
** A multi-precision rational constant.
**/
-#ifdef __CVC4__USE_GMP_IMP
-#include "util/integer.h"
+#include "cvc4autoconfig.h"
#include "util/rational.h"
+#include "util/integer.h"
#include <string>
+#ifndef CVC4_GMP_IMP
+# error "This source should only ever be built if CVC4_GMP_IMP is on !"
+#endif /* CVC4_GMP_IMP */
+
using namespace std;
using namespace CVC4;
@@ -49,4 +53,3 @@ std::ostream& CVC4::operator<<(std::ostream& os, const Rational& q){
return os << q.toString();
}
-#endif /* __CVC4__USE_GMP_IMP */
diff --git a/src/util/rational_gmp_imp.h b/src/util/rational_gmp_imp.h
index ab88a0d52..ce94dfe24 100644
--- a/src/util/rational_gmp_imp.h
+++ b/src/util/rational_gmp_imp.h
@@ -1,9 +1,9 @@
/********************* */
-/*! \file rational.h
+/*! \file rational_gmp_imp.h
** \verbatim
** Original author: taking
** Major contributors: none
- ** Minor contributors (to current version): dejan, mdeters, cconway
+ ** 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
@@ -11,11 +11,11 @@
** See the file COPYING in the top-level source directory for licensing
** information.\endverbatim
**
- ** \brief Multi-precision rational constants.
+ ** \brief Multiprecision rational constants; wraps a GMP multiprecision
+ ** rational.
**
- ** Multi-precision rational constants.
+ ** Multiprecision rational constants; wraps a GMP multiprecision rational.
**/
-#ifdef __CVC4__USE_GMP_IMP
#include "cvc4_public.h"
@@ -259,4 +259,4 @@ std::ostream& operator<<(std::ostream& os, const Rational& n);
}/* CVC4 namespace */
#endif /* __CVC4__RATIONAL_H */
-#endif /* __CVC4__USE_GMP_IMP */
+
diff --git a/src/util/sexpr.h b/src/util/sexpr.h
index 6b32c46bb..607075658 100644
--- a/src/util/sexpr.h
+++ b/src/util/sexpr.h
@@ -3,7 +3,7 @@
** \verbatim
** Original author: cconway
** Major contributors: none
- ** Minor contributors (to current version): taking, mdeters
+ ** Minor contributors (to current version): mdeters
** This file is part of the CVC4 prototype.
** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
** Courant Institute of Mathematical Sciences
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback