diff options
Diffstat (limited to 'src/util/integer.h.in')
-rw-r--r-- | src/util/integer.h.in | 33 |
1 files changed, 33 insertions, 0 deletions
diff --git a/src/util/integer.h.in b/src/util/integer.h.in new file mode 100644 index 000000000..7e1b9a1aa --- /dev/null +++ b/src/util/integer.h.in @@ -0,0 +1,33 @@ +/********************* */ +/*! \file integer.h.in + ** \verbatim + ** Original author: taking + ** Major contributors: none + ** Minor contributors (to current version): dejan, cconway, 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 + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief A multiprecision integer constant. + ** + ** A multiprecision integer constant. + **/ + +// 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 */ |