diff options
Diffstat (limited to 'src')
35 files changed, 180 insertions, 107 deletions
diff --git a/src/Makefile.am b/src/Makefile.am index a805f8c85..97c66ac89 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -14,7 +14,7 @@ LIBCVC4_VERSION = @CVC4_LIBRARY_VERSION@ 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) SUBDIRS = expr util context theory prop smt . parser main diff --git a/src/context/Makefile.am b/src/context/Makefile.am index 3d912e685..7a40bab1b 100644 --- a/src/context/Makefile.am +++ b/src/context/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 = libcontext.la diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am index 225624a8b..db863440c 100644 --- a/src/expr/Makefile.am +++ b/src/expr/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 = libexpr.la diff --git a/src/include/cvc4_public.h b/src/include/cvc4_public.h index e1b515ba5..8375f7571 100644 --- a/src/include/cvc4_public.h +++ b/src/include/cvc4_public.h @@ -21,6 +21,8 @@ #ifndef __CVC4_PUBLIC_H #define __CVC4_PUBLIC_H +#include <stdint.h> + #if defined _WIN32 || defined __CYGWIN__ # ifdef BUILDING_DLL # ifdef __GNUC__ diff --git a/src/main/Makefile.am b/src/main/Makefile.am index 9ffa43ca0..82ff00a60 100644 --- a/src/main/Makefile.am +++ b/src/main/Makefile.am @@ -1,5 +1,5 @@ AM_CPPFLAGS = \ - -I@srcdir@/../include -I@srcdir@/.. $(ANTLR_INCLUDES) + -I@srcdir@/../include -I@srcdir@/.. -I@builddir@/.. $(ANTLR_INCLUDES) AM_CXXFLAGS = -Wall -Wno-unknown-pragmas bin_PROGRAMS = cvc4 diff --git a/src/parser/Makefile.am b/src/parser/Makefile.am index a323ec3cb..b1f265b56 100644 --- a/src/parser/Makefile.am +++ b/src/parser/Makefile.am @@ -14,7 +14,7 @@ LIBCVC4PARSER_VERSION = @CVC4_PARSER_LIBRARY_VERSION@ AM_CPPFLAGS = \ -D__BUILDING_CVC4PARSERLIB \ - -I@srcdir@/../include -I@srcdir@/.. $(ANTLR_INCLUDES) + -I@srcdir@/../include -I@srcdir@/.. -I@builddir@/.. $(ANTLR_INCLUDES) AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) SUBDIRS = smt smt2 cvc diff --git a/src/parser/cvc/Makefile.am b/src/parser/cvc/Makefile.am index 9754c1063..cfe983727 100644 --- a/src/parser/cvc/Makefile.am +++ b/src/parser/cvc/Makefile.am @@ -1,6 +1,6 @@ AM_CPPFLAGS = \ -D__BUILDING_CVC4PARSERLIB \ - -I@srcdir@/../../include -I@srcdir@/../.. $(ANTLR_INCLUDES) + -I@srcdir@/../../include -I@srcdir@/../.. -I@builddir@/../.. $(ANTLR_INCLUDES) AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) -Wno-unused-function -Wno-unused-variable # Compile generated C files using C++ compiler diff --git a/src/parser/smt/Makefile.am b/src/parser/smt/Makefile.am index 418b204dc..f5ea3aae3 100644 --- a/src/parser/smt/Makefile.am +++ b/src/parser/smt/Makefile.am @@ -1,6 +1,6 @@ AM_CPPFLAGS = \ -D__BUILDING_CVC4PARSERLIB \ - -I@srcdir@/../../include -I@srcdir@/../.. $(ANTLR_INCLUDES) + -I@srcdir@/../../include -I@srcdir@/../.. -I@builddir@/../.. $(ANTLR_INCLUDES) AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) -Wno-unused-function -Wno-unused-variable # Compile generated C files using C++ compiler diff --git a/src/parser/smt2/Makefile.am b/src/parser/smt2/Makefile.am index 3066f2247..aabae5352 100644 --- a/src/parser/smt2/Makefile.am +++ b/src/parser/smt2/Makefile.am @@ -1,6 +1,6 @@ AM_CPPFLAGS = \ -D__BUILDING_CVC4PARSERLIB \ - -I@srcdir@/../../include -I@srcdir@/../.. $(ANTLR_INCLUDES) + -I@srcdir@/../../include -I@srcdir@/../.. -I@builddir@/../.. $(ANTLR_INCLUDES) AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) -Wno-unused-function -Wno-unused-variable # Compile generated C files using C++ compiler diff --git a/src/prop/Makefile.am b/src/prop/Makefile.am index 48c9c3fd2..06504e73c 100644 --- a/src/prop/Makefile.am +++ b/src/prop/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 = libprop.la diff --git a/src/prop/minisat/Makefile.am b/src/prop/minisat/Makefile.am index 77d1d602e..56f61adad 100644 --- a/src/prop/minisat/Makefile.am +++ b/src/prop/minisat/Makefile.am @@ -1,6 +1,6 @@ AM_CPPFLAGS = \ -D__BUILDING_CVC4LIB \ - -I@srcdir@/mtl -I@srcdir@/core -I@srcdir@/../.. -I@srcdir@/../../include + -I@srcdir@/mtl -I@srcdir@/core -I@srcdir@/../.. -I@builddir@/../.. -I@srcdir@/../../include AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) -DNDEBUG noinst_LTLIBRARIES = libminisat.la diff --git a/src/smt/Makefile.am b/src/smt/Makefile.am index 72dd8f3df..90d58904a 100644 --- a/src/smt/Makefile.am +++ b/src/smt/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 = libsmt.la diff --git a/src/theory/Makefile.am b/src/theory/Makefile.am index bb9d19b25..a2a206d40 100644 --- a/src/theory/Makefile.am +++ b/src/theory/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 = libtheory.la diff --git a/src/theory/arith/Makefile.am b/src/theory/arith/Makefile.am index 541426ac3..4d299e8af 100644 --- a/src/theory/arith/Makefile.am +++ b/src/theory/arith/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 = libarith.la diff --git a/src/theory/arrays/Makefile.am b/src/theory/arrays/Makefile.am index 0c6e9006f..8a0a180db 100644 --- a/src/theory/arrays/Makefile.am +++ b/src/theory/arrays/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 = libarrays.la diff --git a/src/theory/booleans/Makefile.am b/src/theory/booleans/Makefile.am index 478fca1cf..3bd8b5a39 100644 --- a/src/theory/booleans/Makefile.am +++ b/src/theory/booleans/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 = libbooleans.la diff --git a/src/theory/builtin/Makefile.am b/src/theory/builtin/Makefile.am index 5694dea84..d1df0e425 100644 --- a/src/theory/builtin/Makefile.am +++ b/src/theory/builtin/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 = libbuiltin.la diff --git a/src/theory/bv/Makefile.am b/src/theory/bv/Makefile.am index 94941d406..cab90bbdb 100644 --- a/src/theory/bv/Makefile.am +++ b/src/theory/bv/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 = libbv.la diff --git a/src/theory/uf/Makefile.am b/src/theory/uf/Makefile.am index 39586345b..4e399aeb7 100644 --- a/src/theory/uf/Makefile.am +++ b/src/theory/uf/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 = libuf.la 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 |